YES Time: 0.014 Problem: Equations: TRS: andAC(x,0()) -> 0() andAC(x,1()) -> x andAC(x,x) -> x orAC(x,0()) -> x orAC(x,1()) -> 1() orAC(x,x) -> x Proof: AC-KBO Processor: precedence: orAC ~ andAC > 1 ~ 0 weight function: w0 = 8 w(1) = w(0) = 8 w(orAC) = w(andAC) = 0 problem: Equations: TRS: Qed