YES Time: 0.015 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 > zero > b > i > a weight function: w0 = 1 w(b) = 15 w(zero) = 6 w(i) = 4 w(a) = 3 w(pAC) = 0 problem: Equations: TRS: Qed