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