YES Rewrite Rules: [ f(?x,a(g(?x))) -> g(f(?x,?x)), f(?x,g(?x)) -> g(f(?x,?x)), a(?x) -> ?x, h(?x) -> h(a(h(?x))) ] Apply Direct Methods... Inner CPs: [ f(?x,g(?x)) = g(f(?x,?x)) ] Outer CPs: [ ] 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,a(g(?x))) -> g(f(?x,?x)), f(?x,g(?x)) -> g(f(?x,?x)), a(?x) -> ?x, h(?x) -> h(a(h(?x))) ] Sort Assignment: a : 12=>12 f : 12*12=>12 g : 12=>12 h : 12=>12 maximal types: {12} Persistent Decomposition failed: Can't judge Try Layer Preserving Decomposition for... [ f(?x,a(g(?x))) -> g(f(?x,?x)), f(?x,g(?x)) -> g(f(?x,?x)), a(?x) -> ?x, h(?x) -> h(a(h(?x))) ] (lp) [ f(?x,a(g(?x))) -> g(f(?x,?x)), f(?x,g(?x)) -> g(f(?x,?x)), a(?x) -> ?x ] Rewrite Rules: [ f(?x,a(g(?x))) -> g(f(?x,?x)), f(?x,g(?x)) -> g(f(?x,?x)), a(?x) -> ?x ] Apply Direct Methods... Inner CPs: [ f(?x,g(?x)) = g(f(?x,?x)) ] Outer CPs: [ ] Terminating, WCR: CR (lp) [ a(?x) -> ?x, h(?x) -> h(a(h(?x))) ] Rewrite Rules: [ a(?x) -> ?x, h(?x) -> h(a(h(?x))) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... unknown Innermost Terminating Linear Development Closed Direct Methods: CR Result by Layer Preserving Decomposition: CR Final result: CR 89.trs: YES (12 msec.)