YES Time: 0.117 Problem: Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) 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: w0 = 8 w(zero) = 12 w(a) = 10 w(i) = 9 w(b) = 8 w(pAC) = 6 problem: Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) TRS: Qed