(ignored inputs)COMMENT Example 9 from [KH12] doi: http://dx.doi.org/10.1007/978-3-642-28717-6_21 Rewrite Rules: [ f(?x,?x) -> s(s(?x)), infty -> s(infty) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... unknown Innermost Terminating unknown Knuth&Bendix not Left-Linear, Right-Linear unknown Simple-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) -> s(s(?x)), infty -> s(infty) ] Sort Assignment: f : 8*8=>8 s : 8=>8 infty : =>8 maximal types: {8} Persistent Decomposition failed: Can't judge Try Layer Preserving Decomposition for... [ f(?x,?x) -> s(s(?x)), infty -> s(infty) ] Layer Preserving Decomposition failed: Can't judge Try Commutative Decomposition for... [ f(?x,?x) -> s(s(?x)), infty -> s(infty) ] Commutative Decomposition failed (not left-linear): Can't judge No further decomposition possible Final result: Can't judge /local-scratch/hzankl/2012/cops2012/119.trs: Failure(unknown) (1 msec.)