YES Time: 0.044 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-KBO Processor: precedence: zero > pAC > b > a weight function: w0 = 1 w(a) = 8 w(b) = 4 w(zero) = 1 w(pAC) = 0 problem: Equations: TRS: Qed