NO Rewrite Rules: [ subseteq(nil,?ys) -> true, subseteq(cons(?x,?xs),?ys) -> and(member(?x,?ys),subseteq(?xs,?ys)), member(?x,nil) -> false, member(?x,cons(?y,?ys)) -> or(eq(?x,?y),member(?x,?ys)), eq(0,0) -> true, eq(0,s(?y)) -> false, eq(s(?x),0) -> false, eq(s(?x),s(?y)) -> eq(?x,?y), and(true,true) -> true, and(?x,false) -> false, and(false,?y) -> false, or(true,?y) -> true, or(?x,true) -> true, or(false,false) -> false, subseteq(?xs,?xs) -> true ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ true = true, and(member(?x_1,cons(?x_1,?xs_1)),subseteq(?xs_1,cons(?x_1,?xs_1))) = true, false = false, true = true ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), not WCR Knuth & Bendix Direct Methods: not CR Final result: not CR new/subseteq.trs: Success(not CR) (18 msec.)