YES Rewrite Rules: [ f(?x,?y) -> ?x, f(?x,?y) -> f(?x,g(?y)), g(?x) -> h(?x), F(g(?x),?x) -> F(?x,g(?x)), F(h(?x),?x) -> F(?x,h(?x)) ] Apply Direct Methods... Inner CPs: [ F(h(?x_2),?x_2) = F(?x_2,g(?x_2)) ] Outer CPs: [ ?x = f(?x,g(?y)) ] unknown Terminating not Left-Linear, not Right-Linear unknown Gomi&Oyamaguchi&Ohta check Non-Confluence...Unknown Direct Methods: Can't judge Try Persistent Decomposition for... [ f(?x,?y) -> ?x, f(?x,?y) -> f(?x,g(?y)), g(?x) -> h(?x), F(g(?x),?x) -> F(?x,g(?x)), F(h(?x),?x) -> F(?x,h(?x)) ] Sort Assignment: F : 9*9=>18 f : 21*9=>21 g : 9=>9 h : 9=>9 maximal types: {9,18}{9,21} {9,18} (ps)Rewrite Rules: [ g(?x) -> h(?x), F(g(?x),?x) -> F(?x,g(?x)), F(h(?x),?x) -> F(?x,h(?x)) ] Apply Direct Methods... Inner CPs: [ F(h(?x),?x) = F(?x,g(?x)) ] Outer CPs: [ ] Terminating, WCR: CR {9,21} (ps)Rewrite Rules: [ f(?x,?y) -> ?x, f(?x,?y) -> f(?x,g(?y)), g(?x) -> h(?x) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ?x = f(?x,g(?y)) ] Overlay, check Innermost Termination... unknown Innermost Terminating Linear Development Closed Direct Methods: CR Result by Persistent Decomposition: CR Final result: CR 1.trs: YES (8 msec.)