YES Rewrite Rules: [ f(a(?x),?x) -> f(?x,a(?x)), f(b(?x),?x) -> f(?x,b(?x)), g(b(?x),?y) -> g(a(a(?x)),?y), g(c(?x),?y) -> ?y, a(?x) -> b(?x) ] Apply Direct Methods... Inner CPs: [ f(b(?x_4),?x_4) = f(?x_4,a(?x_4)) ] 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(a(?x),?x) -> f(?x,a(?x)), f(b(?x),?x) -> f(?x,b(?x)), g(b(?x),?y) -> g(a(a(?x)),?y), g(c(?x),?y) -> ?y, a(?x) -> b(?x) ] Sort Assignment: a : 20=>20 b : 20=>20 c : 12=>20 f : 20*20=>23 g : 20*21=>21 maximal types: {12,20,21}{12,20,23} {12,20,21} (ps)Rewrite Rules: [ g(b(?x),?y) -> g(a(a(?x)),?y), g(c(?x),?y) -> ?y, a(?x) -> b(?x) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... unknown Innermost Terminating Linear Development Closed Direct Methods: CR {12,20,23} (ps)Rewrite Rules: [ f(a(?x),?x) -> f(?x,a(?x)), f(b(?x),?x) -> f(?x,b(?x)), a(?x) -> b(?x) ] Apply Direct Methods... Inner CPs: [ f(b(?x_2),?x_2) = f(?x_2,a(?x_2)) ] Outer CPs: [ ] Terminating, WCR: CR Result by Persistent Decomposition: CR Final result: CR 3.trs: YES (52 msec.)