YES Time: 0.007 Problem: Equations: TRS: joinAC(x,meetAC(x,y)) -> x meetAC(x,joinAC(x,y)) -> x Proof: AC-KBO Processor: precedence: meetAC > joinAC weight function: w0 = 4 w(meetAC) = w(joinAC) = 0 problem: Equations: TRS: Qed