YES Rewrite Rules: [ f(?x,?x,?y) -> h(?y,c), g(?x) -> f(?x,c,g(c)), c -> h(c,c) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... unknown Innermost Terminating not Left-Linear, Right-Linear Ohta&Oyamaguchi&Toyama Direct Methods: CR Final result: CR 79.trs: YES (0 msec.)