YES Time: 0.036 Problem: Equations: TRS: pAC(x,zero()) -> x pAC(x,i(x)) -> zero() pAC(i(x),x) -> zero() pAC(a(),a()) -> zero() pAC(b(),b()) -> zero() pAC(pAC(pAC(pAC(pAC(a(),b()),a()),b()),a()),b()) -> zero() Proof: AC-KBO Processor: precedence: pAC > zero > a > b > i weight function: w0 = 4 w(zero) = 15 w(b) = 9 w(a) = 7 w(i) = 6 w(pAC) = 1 problem: Equations: TRS: Qed