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