YES Time: 0.009 Problem: Equations: TRS: not(not(x)) -> x orAC(not(x),not(y)) -> not(andAC(x,y)) Proof: AC-RPO Processor: precedence: orAC > not > andAC status: problem: Equations: TRS: Qed