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