YES Time: 0.009 Problem: Equations: TRS: fAC(x,one()) -> x Proof: AC-KBO Processor: precedence: one > fAC weight function: w0 = 4 w(one) = 4 w(fAC) = 0 problem: Equations: TRS: Qed