YES Time: 0.019 Problem: Equations: TRS: pAC(x,zero()) -> x pAC(x,i(x)) -> zero() pAC(i(x),x) -> zero() a(a(x)) -> x b(b(x)) -> x a(b(a(b(a(b(x)))))) -> x Proof: AC-KBO Processor: precedence: pAC > b > i > zero > a weight function: w0 = 6 w(b) = w(a) = 15 w(zero) = 13 w(i) = 1 w(pAC) = 0 problem: Equations: TRS: Qed