YES 1: or(true(),true()) -> true() 2: or(x2,x1) -> or(x1,x2) @Jouannaud and Kirchner's criterion --- R 1: or(true(),true()) -> true() 2: or(x2,x1) -> or(x1,x2) --- S 1: or(true(),true()) -> true() 2: or(x2,x1) -> or(x1,x2)