YES 2 decompositions #1 ----------- 7: and(x1,T()) -> x1 8: and(x1,F()) -> F() 9: and(x1,x2) -> and(x2,x1) 10: and(and(x1,x2),x3) -> and(x1,and(x2,x3)) #2 ----------- 1: not(T()) -> F() 2: not(F()) -> T() 3: or(x1,T()) -> T() 4: or(x1,F()) -> x1 5: or(x1,x2) -> or(x2,x1) 6: or(or(x1,x2),x3) -> or(x1,or(x2,x3)) 11: imply(x1,x2) -> or(not(x1),x2) @Jouannaud and Kirchner's criterion --- R 7: and(x1,T()) -> x1 8: and(x1,F()) -> F() 9: and(x1,x2) -> and(x2,x1) 10: and(and(x1,x2),x3) -> and(x1,and(x2,x3)) --- S 7: and(x1,T()) -> x1 8: and(x1,F()) -> F() 9: and(x1,x2) -> and(x2,x1) 10: and(and(x1,x2),x3) -> and(x1,and(x2,x3)) @Jouannaud and Kirchner's criterion --- R 1: not(T()) -> F() 2: not(F()) -> T() 3: or(x1,T()) -> T() 4: or(x1,F()) -> x1 5: or(x1,x2) -> or(x2,x1) 6: or(or(x1,x2),x3) -> or(x1,or(x2,x3)) 11: imply(x1,x2) -> or(not(x1),x2) --- S 1: not(T()) -> F() 2: not(F()) -> T() 3: or(x1,T()) -> T() 4: or(x1,F()) -> x1 5: or(x1,x2) -> or(x2,x1) 6: or(or(x1,x2),x3) -> or(x1,or(x2,x3)) 11: imply(x1,x2) -> or(not(x1),x2)