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