MAYBE
(ignored inputs)COMMENT translated from Cops 112
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ nats -> cons(0,inc(nats)),
     inc(cons(?x,?ys)) -> cons(s(?x),inc(?ys)),
     inc(tl(nats)) -> tl(inc(nats)),
     hd(cons(?x,?ys)) -> ?x,
     tl(cons(?x,?ys)) -> ?ys,
     d(cons(?x,?ys)) -> cons(?x,cons(?x,d(?ys))) ]
Constructors: {0,s,cons}
Defined function symbols: {d,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,
     d(cons(?x,?ys)) -> cons(?x,cons(?x,d(?ys))) ]
   [ inc(tl(nats)) -> tl(inc(nats)) ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat,List}
Signature:
   [ nats : List,
     inc : List -> List,
     d : List -> List,
     hd : List -> Nat,
     tl : List -> List,
     cons : Nat,List -> List,
     s : Nat -> Nat,
     0 : Nat ]
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,
     d(cons(?x,?ys)) -> cons(?x,cons(?x,d(?ys))) ]
Conjecture Part:
   [ inc(tl(nats)) = tl(inc(nats)) ]
Termination proof failed.
examples/fromCops/cr/112.trs: Failure(unknown)
(13 msec.)