MAYBE Rewrite Rules: [ a(f(?x),?y) -> f(a(f(?y),?x)), a(b(?x),?y) -> a(?x,b(?x)), a(g(?x),?x) -> g(b(g(?x))) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... unknown Innermost Terminating not Left-Linear, not Right-Linear unknown Gomi&Oyamaguchi&Ohta check Non-Confluence...Unknown Direct Methods: Can't judge Try Persistent Decomposition for... [ a(f(?x),?y) -> f(a(f(?y),?x)), a(b(?x),?y) -> a(?x,b(?x)), a(g(?x),?x) -> g(b(g(?x))) ] Sort Assignment: a : 15*15=>15 b : 15=>15 f : 15=>15 g : 15=>15 maximal types: {15} Persistent Decomposition failed: Can't judge Try Layer Preserving Decomposition for... [ a(f(?x),?y) -> f(a(f(?y),?x)), a(b(?x),?y) -> a(?x,b(?x)), a(g(?x),?x) -> g(b(g(?x))) ] Layer Preserving Decomposition failed: Can't judge Try Commutative Decomposition for... [ a(f(?x),?y) -> f(a(f(?y),?x)), a(b(?x),?y) -> a(?x,b(?x)), a(g(?x),?x) -> g(b(g(?x))) ] Commutative Decomposition failed: Can't judge No further decomposition possible Final result: Can't judge 91.trs: MAYBE (0 msec.)