MAYBE Rewrite Rules: [ f(?x) -> g(h(?x),?x), g(?x,?x) -> a, b -> h(b) ] 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... [ f(?x) -> g(h(?x),?x), g(?x,?x) -> a, b -> h(b) ] Sort Assignment: a : =>13 b : =>12 f : 12=>13 g : 12*12=>13 h : 12=>12 maximal types: {12,13} Persistent Decomposition failed: Can't judge Try Layer Preserving Decomposition for... [ f(?x) -> g(h(?x),?x), g(?x,?x) -> a, b -> h(b) ] Layer Preserving Decomposition failed: Can't judge Try Commutative Decomposition for... [ f(?x) -> g(h(?x),?x), g(?x,?x) -> a, b -> h(b) ] Commutative Decomposition failed: Can't judge No further decomposition possible Final result: Can't judge 59.trs: MAYBE (0 msec.)