We consider the following Problem: Strict Trs: {p(a(x0), p(a(b(x1)), x2)) -> p(a(b(a(x2))), p(a(a(x1)), x2))} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict Trs: {p(a(x0), p(a(b(x1)), x2)) -> p(a(b(a(x2))), p(a(a(x1)), x2))} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict Trs: {p(a(x0), p(a(b(x1)), x2)) -> p(a(b(a(x2))), p(a(a(x1)), x2))} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The following argument positions are usable: Uargs(p) = {2}, Uargs(a) = {}, Uargs(b) = {} We have the following constructor-based EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: p(x1, x2) = [0 0] x1 + [1 1] x2 + [0] [2 2] [0 1] [0] a(x1) = [0 2] x1 + [0] [0 0] [0] b(x1) = [0 0] x1 + [0] [0 0] [2] Hurray, we answered YES(?,O(n^1))