MAYBE MAYBE TRS: { sum(0()) -> 0(), sum(s(x)) -> +(sqr(s(x)), sum(x)), sum(s(x)) -> +(*(s(x), s(x)), sum(x)), sqr(x) -> *(x, x) } DUP: We consider a duplicating system. Trs: { sum(0()) -> 0(), sum(s(x)) -> +(sqr(s(x)), sum(x)), sum(s(x)) -> +(*(s(x), s(x)), sum(x)), sqr(x) -> *(x, x) } Fail