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