YES Time: 0.010 Problem: Equations: TRS: fAC(x,one()) -> x fAC(x,x) -> x Proof: AC-RPO Processor: precedence: one > fAC status: problem: Equations: TRS: Qed