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