YES Time: 0.012 Problem: Equations: 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: TRS: Qed