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