YES Time: 0.020 Problem: Equations: TRS: fAC(x,one()) -> x fAC(i(x),x) -> one() Proof: AC-KBO Processor: precedence: fAC > i ~ one weight function: w0 = 1 w(one) = 15 w(fAC) = 12 w(i) = 1 problem: Equations: TRS: Qed