(ignored inputs)COMMENT Example 4.2 of \cite{Toy81}
Rewrite Rules:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     d(0) -> 0,
     d(s(?x)) -> s(s(d(?x))),
     f(0) -> 0,
     f(s(?x)) -> +(+(s(?x),s(?x)),s(?x)),
     f(g(0)) -> +(+(g(0),g(0)),g(0)),
     g(?x) -> s(d(?x)) ]
Apply Direct Methods...
Inner CPs:
   [ f(s(d(0))) = +(+(g(0),g(0)),g(0)) ]
Outer CPs:
   [  ]
not Overlay, check Termination...
Terminating, WCR
Knuth&Bendix
Direct Methods: CR

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