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