(ignored inputs)COMMENT R_2 of \cite{GOO96} Rewrite Rules: [ f(?x,?x) -> a, c -> h(c,g(c)), h(?x,g(?x)) -> f(?x,h(?x,g(c))) ] 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) -> a, c -> h(c,g(c)), h(?x,g(?x)) -> f(?x,h(?x,g(c))) ] Sort Assignment: a : =>6 c : =>6 f : 6*6=>6 g : 6=>11 h : 6*11=>6 maximal types: {6,11} Persistent Decomposition failed: Can't judge Try Layer Preserving Decomposition for... [ f(?x,?x) -> a, c -> h(c,g(c)), h(?x,g(?x)) -> f(?x,h(?x,g(c))) ] Layer Preserving Decomposition failed: Can't judge Try Commutative Decomposition for... [ f(?x,?x) -> a, c -> h(c,g(c)), h(?x,g(?x)) -> f(?x,h(?x,g(c))) ] Commutative Decomposition failed (not left-linear): Can't judge No further decomposition possible Final result: Can't judge /local-scratch/hzankl/2012/cops2012/24.trs: Failure(unknown) (1 msec.)