MAYBE
(ignored inputs)COMMENT translated from Cops 197
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ or(T,?x) -> T,
     or(?x,F) -> ?x,
     or(or(?x,?y),?z) -> or(?x,or(?y,?z)),
     or(?x,?y) -> or(?y,?x) ]
Constructors: {F,T,or}
Defined function symbols: {}
Constructor subsystem:
   [ or(T,?x) -> T,
     or(?x,F) -> ?x,
     or(or(?x,?y),?z) -> or(?x,or(?y,?z)) ]
Rule part & Conj Part:
   [ or(T,?x) -> T,
     or(?x,F) -> ?x,
     or(or(?x,?y),?z) -> or(?x,or(?y,?z)) ]
   [ or(?x,?y) -> or(?y,?x) ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Bool}
Signature:
   [ F : Bool,
     T : Bool,
     or : Bool,Bool -> Bool ]
Rule Part:
   [ or(T,?x) -> T,
     or(?x,F) -> ?x,
     or(or(?x,?y),?z) -> or(?x,or(?y,?z)) ]
Conjecture Part:
   [ or(?x,?y) = or(?y,?x) ]
Termination proof failed.
examples/fromCops/cr/197.trs: Failure(unknown)
(7 msec.)