YES
(ignored inputs)COMMENT doi:10.1007/3-540-45744-5_49 [153] Example 21 submitted by: Raul Gutierrez and Salvador Lucas
Rewrite Rules:
   [ g(a,?y) -> ?y,
     f(?x,a) -> f(?x,g(?x,b)),
     g(h(?x),?y) -> g(?x,h(?y)) ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR
Knuth & Bendix
Direct Methods: CR

Combined result: CR
803.trs: Success(CR)
(12 msec.)