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