YES Time: 0.013 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(pAC(pAC(pAC(a(),a()),b()),b()),b()) -> pAC(pAC(pAC(a(),a()),a()),b()) pAC(pAC(pAC(pAC(a(),a()),a()),a()),b()) -> pAC(pAC(pAC(a(),a()),b()),b()) Proof: AC-RPO Processor: precedence: zero > pAC > a > b status: 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