MAYBE
(ignored inputs)COMMENT translated from Cops 130
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ and3(?x,?y,F) -> F,
     and3(T,T,T) -> T,
     and3(?x,?y,?z) -> and3(?y,?z,?x) ]
Constructors: {F,T,and3}
Defined function symbols: {}
Constructor subsystem:
   [ and3(?x,?y,F) -> F,
     and3(T,T,T) -> T ]
Rule part & Conj Part:
   [ and3(?x,?y,F) -> F,
     and3(T,T,T) -> T ]
   [ and3(?x,?y,?z) -> and3(?y,?z,?x) ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Bool}
Signature:
   [ F : Bool,
     T : Bool,
     and3 : Bool,Bool,Bool -> Bool ]
Rule Part:
   [ and3(?x,?y,F) -> F,
     and3(T,T,T) -> T ]
Conjecture Part:
   [ and3(?x,?y,?z) = and3(?y,?z,?x) ]
Precedence (by weight): {(F,2),(T,0),(and3,1)}
Rule part is confluent.
R0 is ground confluent.
Check conj part consists of inductive theorems of R0.
Rules:
   [ and3(?x,?y,F) -> F,
     and3(T,T,T) -> T ]
Conjectures:
   [ and3(?x,?y,?z) = and3(?y,?z,?x) ]
STEP 0
ES:
   [ and3(?x,?y,?z) = and3(?y,?z,?x) ]
HS:
   [ ]
ES0:
   [ and3(?x,?y,?z) = and3(?y,?z,?x) ]
HS0:
   [ ]
ES1:
   [ and3(?x,?y,?z) = and3(?y,?z,?x) ]
HS1:
   [ ]
No equation to expand
Failed to prove conj part consists of inductive theorems of R0.
examples/fromCops/cr/130.trs: Failure(unknown)
(5 msec.)