YES Time: 0.011 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-RPO Processor: precedence: b > a > pAC > zero > i status: problem: Equations: TRS: Qed