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