(ignored inputs)COMMENT from Example 3 of \cite{OO04}
Rewrite Rules:
   [ -(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)) ]
Apply Direct Methods...
Inner CPs:
   [ -(?x_2,?y_4) = -(s(?x_2),s(?y_4)) ]
Outer CPs:
   [ -(d(s(?x_3)),?y_1) = -(?x_3,?y_1),
     -(d(d(?x_4)),?y_1) = -(?x_4,s(s(?y_1))) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth&Bendix
Linear
unknown Development Closed
Strongly Closed
Direct Methods: CR

Final result: CR
/local-scratch/hzankl/2012/cops2012/63.trs: Success(CR)
(29 msec.)