YES
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ le(0,?y) -> true,
     le(s(?x),0) -> false,
     le(s(?x),s(?y)) -> le(?x,?y),
     or(true,?y) -> true,
     or(?x,true) -> true,
     or(false,false) -> false,
     le(?x,?x) -> true,
     or(?x,?y) -> or(?y,?x),
     or(le(?x,?y),le(?y,?x)) -> true ]
Constructors: {0,s,true,false}
Defined function symbols: {le,or}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ le(0,?y) -> true,
     le(s(?x),0) -> false,
     le(s(?x),s(?y)) -> le(?x,?y),
     or(true,?y) -> true,
     or(?x,true) -> true,
     or(false,false) -> false ]
   [ le(?x,?x) -> true,
     or(?x,?y) -> or(?y,?x),
     or(le(?x,?y),le(?y,?x)) -> true ]
Trying with:
R:
   [ le(0,?y) -> true,
     le(s(?x),0) -> false,
     le(s(?x),s(?y)) -> le(?x,?y),
     or(true,?y) -> true,
     or(?x,true) -> true,
     or(false,false) -> false ]
E:
   [ le(?x,?x) = true,
     or(?x,?y) = or(?y,?x),
     or(le(?x,?y),le(?y,?x)) = true ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat,Bool}
Signature:
   [ le : Nat,Nat -> Bool,
     or : Bool,Bool -> Bool,
     true : Bool,
     false : Bool,
     s : Nat -> Nat,
     0 : Nat ]
Rule Part:
   [ le(0,?y) -> true,
     le(s(?x),0) -> false,
     le(s(?x),s(?y)) -> le(?x,?y),
     or(true,?y) -> true,
     or(?x,true) -> true,
     or(false,false) -> false ]
Conjecture Part:
   [ le(?x,?x) = true,
     or(?x,?y) = or(?y,?x),
     or(le(?x,?y),le(?y,?x)) = true ]
Precedence (by weight): {(0,6),(s,3),(le,0),(or,1),(true,4),(false,2)}
Rule part is confluent.
R0 is ground confluent.
Check conj part consists of inductive theorems of R0.
Rules:
   [ le(0,?y) -> true,
     le(s(?x),0) -> false,
     le(s(?x),s(?y)) -> le(?x,?y),
     or(true,?y) -> true,
     or(?x,true) -> true,
     or(false,false) -> false ]
Conjectures:
   [ le(?x,?x) = true,
     or(?x,?y) = or(?y,?x),
     or(le(?x,?y),le(?y,?x)) = true ]
STEP 0
ES:
   [ le(?x,?x) = true,
     or(?x,?y) = or(?y,?x),
     or(le(?x,?y),le(?y,?x)) = true ]
HS:
   [ ]
ES0:
   [ le(?x,?x) = true,
     or(?x,?y) = or(?y,?x),
     or(le(?x,?y),le(?y,?x)) = true ]
HS0:
   [ ]
ES1:
   [ le(?x,?x) = true,
     or(?x,?y) = or(?y,?x),
     or(le(?x,?y),le(?y,?x)) = true ]
HS1:
   [ ]
Expand le(?x,?x) = true
   [ true = true,
     le(?y_3,?y_3) = true ]
ES2:
   [ true = true,
     le(?y_3,?y_3) = true,
     or(le(?x,?y),le(?y,?x)) = true,
     or(?x,?y) = or(?y,?x) ]
HS2:
   [ le(?x,?x) -> true ]
STEP 1
ES:
   [ true = true,
     le(?y_3,?y_3) = true,
     or(le(?x,?y),le(?y,?x)) = true,
     or(?x,?y) = or(?y,?x) ]
HS:
   [ le(?x,?x) -> true ]
ES0:
   [ true = true,
     le(?y_3,?y_3) = true,
     or(le(?x,?y),le(?y,?x)) = true,
     or(?x,?y) = or(?y,?x) ]
HS0:
   [ le(?x,?x) -> true ]
ES1:
   [ or(le(?x,?y),le(?y,?x)) = true,
     or(?x,?y) = or(?y,?x) ]
HS1:
   [ le(?x,?x) -> true ]
Expand or(?x,?y) = or(?y,?x)
   [ true = or(?y_4,true),
     true = or(true,?x_5),
     false = or(false,false) ]
ES2:
   [ true = or(?y_4,true),
     true = or(true,?x_5),
     false = or(false,false),
     or(le(?x,?y),le(?y,?x)) = true ]
HS2:
   [ or(?x,?y) -> or(?y,?x),
     le(?x,?x) -> true ]
STEP 2
ES:
   [ true = or(?y_4,true),
     true = or(true,?x_5),
     false = or(false,false),
     or(le(?x,?y),le(?y,?x)) = true ]
HS:
   [ or(?x,?y) -> or(?y,?x),
     le(?x,?x) -> true ]
ES0:
   [ true = true,
     true = true,
     false = false,
     or(le(?x,?y),le(?y,?x)) = true ]
HS0:
   [ or(?x,?y) -> or(?y,?x),
     le(?x,?x) -> true ]
ES1:
   [ or(le(?x,?y),le(?y,?x)) = true ]
HS1:
   [ or(?x,?y) -> or(?y,?x),
     le(?x,?x) -> true ]
Expand or(le(?x,?y),le(?y,?x)) = true
   [ or(true,le(?y_1,0)) = true,
     or(false,le(0,s(?x_2))) = true,
     or(le(?x_3,?y_3),le(s(?y_3),s(?x_3))) = true ]
ES2:
   [ true = true,
     true = true,
     or(le(?x_3,?y_3),le(?y_3,?x_3)) = true ]
HS2:
   [ or(le(?x,?y),le(?y,?x)) -> true,
     or(?x,?y) -> or(?y,?x),
     le(?x,?x) -> true ]
STEP 3
ES:
   [ true = true,
     true = true,
     or(le(?x_3,?y_3),le(?y_3,?x_3)) = true ]
HS:
   [ or(le(?x,?y),le(?y,?x)) -> true,
     or(?x,?y) -> or(?y,?x),
     le(?x,?x) -> true ]
ES0:
   [ true = true,
     true = true,
     or(le(?x_3,?y_3),le(?y_3,?x_3)) = true ]
HS0:
   [ or(le(?x,?y),le(?y,?x)) -> true,
     or(?x,?y) -> or(?y,?x),
     le(?x,?x) -> true ]
ES1:
   [ ]
HS1:
   [ or(le(?x,?y),le(?y,?x)) -> true,
     or(?x,?y) -> or(?y,?x),
     le(?x,?x) -> true ]
Conj part consisits of inductive theorems of R0.
new/le2.trs: Success(GCR)
(16 msec.)