YES
(ignored inputs)COMMENT translated from Cops 4
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ or(true,true) -> true,
     or(?x,?y) -> or(?y,?x) ]
Constructors: {true}
Defined function symbols: {or}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ or(true,true) -> true ]
   [ or(?x,?y) -> or(?y,?x) ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Bool}
Signature:
   [ or : Bool,Bool -> Bool,
     true : Bool ]
Rule Part:
   [ or(true,true) -> true ]
Conjecture Part:
   [ or(?x,?y) = or(?y,?x) ]
Precedence (by weight): {(or,0),(true,1)}
Rule part is confluent.
R0 is ground confluent.
Check conj part consists of inductive theorems of R0.
Rules:
   [ or(true,true) -> true ]
Conjectures:
   [ or(?x,?y) = or(?y,?x) ]
STEP 0
ES:
   [ or(?x,?y) = or(?y,?x) ]
HS:
   [ ]
ES0:
   [ or(?x,?y) = or(?y,?x) ]
HS0:
   [ ]
ES1:
   [ or(?x,?y) = or(?y,?x) ]
HS1:
   [ ]
Expand or(?x,?y) = or(?y,?x)
   [ true = or(true,true) ]
ES2:
   [ true = or(true,true) ]
HS2:
   [ or(?x,?y) -> or(?y,?x) ]
STEP 1
ES:
   [ true = or(true,true) ]
HS:
   [ or(?x,?y) -> or(?y,?x) ]
ES0:
   [ true = true ]
HS0:
   [ or(?x,?y) -> or(?y,?x) ]
ES1:
   [ ]
HS1:
   [ or(?x,?y) -> or(?y,?x) ]
Conj part consisits of inductive theorems of R0.
examples/fromCops/cr/4.trs: Success(GCR)
(8 msec.)