YES Time: 0.014 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,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 ~ a ~ i ~ zero weight function: w0 = 1 w(a) = 15 w(b) = w(zero) = 7 w(i) = 3 w(pAC) = 2 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