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