Rewrite Rules: [ F(?x,A(G(?x))) -> G(F(?x,?x)), F(?x,G(?x)) -> G(F(?x,?x)), A(?x) -> ?x, H(?x) -> H(B(H(?x))) ] Apply Direct Methods... Inner CPs: [ F(?x,G(?x)) = G(F(?x,?x)) ] Outer CPs: [ ] not Overlay, check Termination... unknown/not 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,A(G(?x))) -> G(F(?x,?x)), F(?x,G(?x)) -> G(F(?x,?x)), A(?x) -> ?x, H(?x) -> H(B(H(?x))) ] Sort Assignment: A : 17=>17 B : 7=>14 F : 17*17=>17 G : 17=>17 H : 14=>7 maximal types: {7,14}{17} {7,14} (ps)Rewrite Rules: [ H(?x) -> H(B(H(?x))) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... unknown Innermost Terminating unknown Knuth&Bendix Linear Development Closed Direct Methods: CR {17} (ps)Rewrite Rules: [ F(?x,A(G(?x))) -> G(F(?x,?x)), F(?x,G(?x)) -> G(F(?x,?x)), A(?x) -> ?x ] Apply Direct Methods... Inner CPs: [ F(?x,G(?x)) = G(F(?x,?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth&Bendix Direct Methods: CR Result by Persistent Decomposition: CR Final result: CR /local-scratch/hzankl/2012/cops2012/97.trs: Success(CR) (6 msec.)