(ignored inputs)COMMENT due to Sivakumar , from p.287 of \cite{DJ90} 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 unknown Knuth&Bendix not Left-Linear, not Right-Linear unknown Strongly Depth-Preserving & Non-E-Overlapping check by Reduction-Preserving Completion... failure(empty P) unknown Reduction-Preserving Completion 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 (not left-linear): Can't judge No further decomposition possible Final result: Can't judge /local-scratch/hzankl/2012/cops2012/16.trs: Failure(unknown) (12 msec.)