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