Rewrite Rules: [ I(?x) -> I(B(?x)), F(E(?x),?x) -> G(?x), E(?x) -> ?x ] Apply Direct Methods... Inner CPs: [ F(?x_2,?x_2) = G(?x_2) ] Outer CPs: [ ] not Overlay, check Termination... unknown/not 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...Find Non-Joinable CP reducts: from F(E(E(?x_1)),?x_1) Not Confluent Direct Methods: not CR Final result: not CR /local-scratch/hzankl/2012/cops2012/98.trs: Success(not CR) (1 msec.)