YES Time: 1.107 Problem: Equations: TRS: pAC(x,i(x)) -> zero() pAC(i(x),x) -> zero() pAC(zero(),x) -> x pAC(x,zero()) -> x pAC(a(),pAC(a(),pAC(a(),pAC(a(),pAC(a(),pAC(a(),a())))))) -> zero() pAC(b(),pAC(b(),pAC(b(),pAC(b(),pAC(b(),pAC(b(),b())))))) -> zero() pAC(a(),pAC(b(),pAC(a(),b()))) -> zero() pAC(i(a()),pAC(b(),pAC(i(a()),pAC(b(),pAC(i(a()),b()))))) -> zero() Proof: AC-KBO Processor: precedence: b ~ a ~ zero ~ i ~ pAC weight function: [b] = 1, [a] = 4, [zero] = 4, [i](x0) = 6x0 + 6, [pAC](x0, x1) = x0 + x1 + 1 problem: Equations: TRS: Qed