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