MAYBE Time: 0.070 Problem: Equations: unionAC(unionAC(x3,x4),x5) -> unionAC(x3,unionAC(x4,x5)) unionAC(x3,x4) -> unionAC(x4,x3) interAC(interAC(x3,x4),x5) -> interAC(x3,interAC(x4,x5)) interAC(x3,x4) -> interAC(x4,x3) unionAC(x3,unionAC(x4,x5)) -> unionAC(unionAC(x3,x4),x5) unionAC(x4,x3) -> unionAC(x3,x4) interAC(x3,interAC(x4,x5)) -> interAC(interAC(x3,x4),x5) interAC(x4,x3) -> interAC(x3,x4) TRS: if(true(),x,y) -> x if(false(),x,y) -> y eq(0(),0()) -> true() eq(0(),s(x)) -> false() eq(s(x),s(y)) -> eq(x,y) unionAC(empty(),x) -> x interAC(x,empty()) -> empty() interAC(x,unionAC(y,z)) -> unionAC(interAC(x,y),interAC(x,z)) interAC(single(x),single(y)) -> if(eq(x,y),single(x),empty()) Proof: Open