NO 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: [ ] unknown Terminating not Left-Linear, Right-Linear unknown Ohta&Oyamaguchi&Toyama unknown Gomi&Oyamaguchi&Ohta 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 98.trs: NO (4 msec.)