MAYBE (ignored inputs)COMMENT The first rule is redundant; it can be simulated by the second rule. Confluent by feeble orthogonality ( van Oostrom ) or Okui's simultaneous critical pair criterion. Rewrite Rules: [ f(a,f(a,f(a,f(a,?y)))) -> f(a,f(a,f(a,g(?y,f(a,?y))))), f(?x,?y) -> g(?y,f(?x,?y)) ] Apply Direct Methods... Inner CPs: [ f(a,g(f(a,f(a,?y)),f(a,f(a,f(a,?y))))) = f(a,f(a,f(a,g(?y,f(a,?y))))), f(a,f(a,g(f(a,?y),f(a,f(a,?y))))) = f(a,f(a,f(a,g(?y,f(a,?y))))), f(a,f(a,f(a,g(?y_1,f(a,?y_1))))) = f(a,f(a,f(a,g(?y_1,f(a,?y_1))))), f(a,f(a,f(a,f(a,g(?y,f(a,?y)))))) = f(a,f(a,f(a,g(f(a,?y),f(a,f(a,?y)))))), f(a,f(a,f(a,f(a,f(a,g(?y,f(a,?y))))))) = f(a,f(a,f(a,g(f(a,f(a,?y)),f(a,f(a,f(a,?y))))))), f(a,f(a,f(a,f(a,f(a,f(a,g(?y,f(a,?y)))))))) = f(a,f(a,f(a,g(f(a,f(a,f(a,?y))),f(a,f(a,f(a,f(a,?y)))))))) ] Outer CPs: [ f(a,f(a,f(a,g(?y,f(a,?y))))) = g(f(a,f(a,f(a,?y))),f(a,f(a,f(a,f(a,?y))))) ] not Overlay, check Termination... unknown/not Terminating unknown Knuth & Bendix Left-Linear, not Right-Linear unknown Development Closed unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow unknown Upside-Parallel-Closed/Outside-Closed (inner) Parallel CPs: [ f(a,f(a,f(a,g(?y_12,f(?x_12,?y_12))))) = f(a,f(a,f(a,g(?y_12,f(a,?y_12))))) {?y_12}, f(a,f(a,f(a,f(a,f(a,f(a,g(?y_9,f(a,?y_9)))))))) = f(a,f(a,f(a,g(f(a,f(a,f(a,?y_9))),f(a,f(a,f(a,f(a,?y_9)))))))) {?y_9}, f(a,f(a,g(?y_7,f(?x_7,?y_7)))) = f(a,f(a,f(a,g(?y,f(a,?y))))) {?y}, f(a,f(a,f(a,f(a,f(a,g(?y_4,f(a,?y_4))))))) = f(a,f(a,f(a,g(f(a,f(a,?y_4)),f(a,f(a,f(a,?y_4))))))) {?y_4}, f(a,g(f(a,f(a,?y)),f(a,f(a,f(a,?y))))) = f(a,f(a,f(a,g(?y,f(a,?y))))) {?y}, f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))) = f(a,f(a,f(a,g(f(a,?y_1),f(a,f(a,?y_1)))))) {?y_1} ] unknown Toyama (Parallel CPs) Simultaneous CPs: [ g(g(g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1))))))),f(a,g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1))))))))),f(a,g(g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1))))))),f(a,g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1))))))))))) = f(a,f(a,f(a,g(f(a,f(a,f(a,?y_1))),f(a,f(a,f(a,f(a,?y_1)))))))), g(g(g(g(?y,f(a,?y)),f(a,g(?y,f(a,?y)))),f(a,g(g(?y,f(a,?y)),f(a,g(?y,f(a,?y)))))),f(a,g(g(g(?y,f(a,?y)),f(a,g(?y,f(a,?y)))),f(a,g(g(?y,f(a,?y)),f(a,g(?y,f(a,?y)))))))) = f(a,f(a,f(a,g(?y,f(a,?y))))), g(g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1))))))),f(a,g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1))))))))) = f(a,f(a,f(a,g(f(a,f(a,?y_1)),f(a,f(a,f(a,?y_1))))))), g(g(g(f(a,?y),f(a,f(a,?y))),f(a,g(f(a,?y),f(a,f(a,?y))))),f(a,g(g(f(a,?y),f(a,f(a,?y))),f(a,g(f(a,?y),f(a,f(a,?y))))))) = f(a,f(a,f(a,g(?y,f(a,?y))))), g(g(f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))),f(a,f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))))),f(a,g(f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))),f(a,f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))))))) = f(a,f(a,f(a,g(f(a,f(a,f(a,?y_1))),f(a,f(a,f(a,f(a,?y_1)))))))), g(g(f(a,g(?y,f(a,?y))),f(a,f(a,g(?y,f(a,?y))))),f(a,g(f(a,g(?y,f(a,?y))),f(a,f(a,g(?y,f(a,?y))))))) = f(a,f(a,f(a,g(?y,f(a,?y))))), g(f(a,g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))))),f(a,f(a,g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))))))) = f(a,f(a,f(a,g(f(a,f(a,f(a,?y_1))),f(a,f(a,f(a,f(a,?y_1)))))))), g(f(a,g(g(?y,f(a,?y)),f(a,g(?y,f(a,?y))))),f(a,f(a,g(g(?y,f(a,?y)),f(a,g(?y,f(a,?y))))))) = f(a,f(a,f(a,g(?y,f(a,?y))))), f(a,g(g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1))))))),f(a,g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))))))) = f(a,f(a,f(a,g(f(a,f(a,f(a,?y_1))),f(a,f(a,f(a,f(a,?y_1)))))))), f(a,g(g(g(?y,f(a,?y)),f(a,g(?y,f(a,?y)))),f(a,g(g(?y,f(a,?y)),f(a,g(?y,f(a,?y))))))) = f(a,f(a,f(a,g(?y,f(a,?y))))), g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1))))))) = f(a,f(a,f(a,g(f(a,?y_1),f(a,f(a,?y_1)))))), g(g(f(a,f(a,?y)),f(a,f(a,f(a,?y)))),f(a,g(f(a,f(a,?y)),f(a,f(a,f(a,?y)))))) = f(a,f(a,f(a,g(?y,f(a,?y))))), g(f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))),f(a,f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))))) = f(a,f(a,f(a,g(f(a,f(a,?y_1)),f(a,f(a,f(a,?y_1))))))), g(f(a,g(f(a,?y),f(a,f(a,?y)))),f(a,f(a,g(f(a,?y),f(a,f(a,?y)))))) = f(a,f(a,f(a,g(?y,f(a,?y))))), g(f(a,f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1))))))),f(a,f(a,f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1))))))))) = f(a,f(a,f(a,g(f(a,f(a,f(a,?y_1))),f(a,f(a,f(a,f(a,?y_1)))))))), g(f(a,f(a,g(?y,f(a,?y)))),f(a,f(a,f(a,g(?y,f(a,?y)))))) = f(a,f(a,f(a,g(?y,f(a,?y))))), f(a,g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))))) = f(a,f(a,f(a,g(f(a,f(a,?y_1)),f(a,f(a,f(a,?y_1))))))), f(a,g(g(f(a,?y),f(a,f(a,?y))),f(a,g(f(a,?y),f(a,f(a,?y)))))) = f(a,f(a,f(a,g(?y,f(a,?y))))), f(a,g(f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))),f(a,f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1))))))))) = f(a,f(a,f(a,g(f(a,f(a,f(a,?y_1))),f(a,f(a,f(a,f(a,?y_1)))))))), f(a,g(f(a,g(?y,f(a,?y))),f(a,f(a,g(?y,f(a,?y)))))) = f(a,f(a,f(a,g(?y,f(a,?y))))), f(a,f(a,g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1))))))))) = f(a,f(a,f(a,g(f(a,f(a,f(a,?y_1))),f(a,f(a,f(a,f(a,?y_1)))))))), f(a,f(a,g(g(?y,f(a,?y)),f(a,g(?y,f(a,?y)))))) = f(a,f(a,f(a,g(?y,f(a,?y))))), g(f(a,f(a,f(a,?y))),f(a,f(a,f(a,f(a,?y))))) = f(a,f(a,f(a,g(?y,f(a,?y))))), f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))) = f(a,f(a,f(a,g(f(a,?y_1),f(a,f(a,?y_1)))))), f(a,g(f(a,f(a,?y)),f(a,f(a,f(a,?y))))) = f(a,f(a,f(a,g(?y,f(a,?y))))), f(a,f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1))))))) = f(a,f(a,f(a,g(f(a,f(a,?y_1)),f(a,f(a,f(a,?y_1))))))), f(a,f(a,g(f(a,?y),f(a,f(a,?y))))) = f(a,f(a,f(a,g(?y,f(a,?y))))), f(a,f(a,f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))))) = f(a,f(a,f(a,g(f(a,f(a,f(a,?y_1))),f(a,f(a,f(a,f(a,?y_1)))))))), f(a,f(a,f(a,g(?y,f(a,?y))))) = f(a,f(a,f(a,g(?y,f(a,?y))))), f(a,f(a,f(a,g(g(g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1))))))),f(a,g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1))))))))),f(a,g(g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1))))))),f(a,g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))))))))))) = f(a,f(a,f(a,f(a,f(a,f(a,g(f(a,f(a,f(a,?y_1))),f(a,f(a,f(a,f(a,?y_1))))))))))), f(a,f(a,f(a,g(g(g(g(?y,f(a,?y)),f(a,g(?y,f(a,?y)))),f(a,g(g(?y,f(a,?y)),f(a,g(?y,f(a,?y)))))),f(a,g(g(g(?y,f(a,?y)),f(a,g(?y,f(a,?y)))),f(a,g(g(?y,f(a,?y)),f(a,g(?y,f(a,?y))))))))))) = f(a,f(a,f(a,f(a,f(a,f(a,g(?y,f(a,?y)))))))), f(a,f(a,f(a,g(g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1))))))),f(a,g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))))))))) = f(a,f(a,f(a,f(a,f(a,g(f(a,f(a,f(a,?y_1))),f(a,f(a,f(a,f(a,?y_1)))))))))), f(a,f(a,f(a,g(g(g(?y,f(a,?y)),f(a,g(?y,f(a,?y)))),f(a,g(g(?y,f(a,?y)),f(a,g(?y,f(a,?y))))))))) = f(a,f(a,f(a,f(a,f(a,g(?y,f(a,?y))))))), f(a,f(a,f(a,g(g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1))))))),f(a,g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))))))))) = f(a,f(a,f(a,f(a,f(a,f(a,g(f(a,f(a,?y_1)),f(a,f(a,f(a,?y_1)))))))))), f(a,f(a,f(a,g(g(g(f(a,?y),f(a,f(a,?y))),f(a,g(f(a,?y),f(a,f(a,?y))))),f(a,g(g(f(a,?y),f(a,f(a,?y))),f(a,g(f(a,?y),f(a,f(a,?y)))))))))) = f(a,f(a,f(a,f(a,f(a,f(a,g(?y,f(a,?y)))))))), f(a,f(a,f(a,g(g(f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))),f(a,f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))))),f(a,g(f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))),f(a,f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1))))))))))))) = f(a,f(a,f(a,f(a,f(a,f(a,g(f(a,f(a,f(a,?y_1))),f(a,f(a,f(a,f(a,?y_1))))))))))), f(a,f(a,f(a,g(g(f(a,g(?y,f(a,?y))),f(a,f(a,g(?y,f(a,?y))))),f(a,g(f(a,g(?y,f(a,?y))),f(a,f(a,g(?y,f(a,?y)))))))))) = f(a,f(a,f(a,f(a,f(a,f(a,g(?y,f(a,?y)))))))), f(a,f(a,f(a,g(f(a,g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))))),f(a,f(a,g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1))))))))))))) = f(a,f(a,f(a,f(a,f(a,f(a,g(f(a,f(a,f(a,?y_1))),f(a,f(a,f(a,f(a,?y_1))))))))))), f(a,f(a,f(a,g(f(a,g(g(?y,f(a,?y)),f(a,g(?y,f(a,?y))))),f(a,f(a,g(g(?y,f(a,?y)),f(a,g(?y,f(a,?y)))))))))) = f(a,f(a,f(a,f(a,f(a,f(a,g(?y,f(a,?y)))))))), f(a,f(a,f(a,g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))))))) = f(a,f(a,f(a,f(a,g(f(a,f(a,f(a,?y_1))),f(a,f(a,f(a,f(a,?y_1))))))))), f(a,f(a,f(a,g(g(?y,f(a,?y)),f(a,g(?y,f(a,?y))))))) = f(a,f(a,f(a,f(a,g(?y,f(a,?y)))))), f(a,f(a,f(a,g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))))))) = f(a,f(a,f(a,f(a,f(a,g(f(a,f(a,?y_1)),f(a,f(a,f(a,?y_1))))))))), f(a,f(a,f(a,g(g(f(a,?y),f(a,f(a,?y))),f(a,g(f(a,?y),f(a,f(a,?y)))))))) = f(a,f(a,f(a,f(a,f(a,g(?y,f(a,?y))))))), f(a,f(a,f(a,g(f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))),f(a,f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1))))))))))) = f(a,f(a,f(a,f(a,f(a,g(f(a,f(a,f(a,?y_1))),f(a,f(a,f(a,f(a,?y_1)))))))))), f(a,f(a,f(a,g(f(a,g(?y,f(a,?y))),f(a,f(a,g(?y,f(a,?y)))))))) = f(a,f(a,f(a,f(a,f(a,g(?y,f(a,?y))))))), f(a,f(a,f(a,g(f(a,f(a,f(a,g(?y_1,f(a,?y_1))))),f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))))))) = f(a,f(a,f(a,f(a,f(a,f(a,g(f(a,?y_1),f(a,f(a,?y_1))))))))), f(a,f(a,f(a,g(g(f(a,f(a,?y)),f(a,f(a,f(a,?y)))),f(a,g(f(a,f(a,?y)),f(a,f(a,f(a,?y))))))))) = f(a,f(a,f(a,f(a,f(a,f(a,g(?y,f(a,?y)))))))), f(a,f(a,f(a,g(f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))),f(a,f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1))))))))))) = f(a,f(a,f(a,f(a,f(a,f(a,g(f(a,f(a,?y_1)),f(a,f(a,f(a,?y_1)))))))))), f(a,f(a,f(a,g(f(a,g(f(a,?y),f(a,f(a,?y)))),f(a,f(a,g(f(a,?y),f(a,f(a,?y))))))))) = f(a,f(a,f(a,f(a,f(a,f(a,g(?y,f(a,?y)))))))), f(a,f(a,f(a,g(f(a,f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1))))))),f(a,f(a,f(a,f(a,f(a,f(a,g(?y_1,f(a,?y_1)))))))))))) = f(a,f(a,f(a,f(a,f(a,f(a,g(f(a,f(a,f(a,?y_1))),f(a,f(a,f(a,f(a,?y_1))))))))))), f(a,f(a,f(a,g(f(a,f(a,g(?y,f(a,?y)))),f(a,f(a,f(a,g(?y,f(a,?y))))))))) = f(a,f(a,f(a,f(a,f(a,f(a,g(?y,f(a,?y)))))))), f(a,f(a,f(a,g(f(a,?y),f(a,f(a,?y)))))) = f(a,f(a,f(a,f(a,g(?y,f(a,?y)))))), f(a,f(a,f(a,g(f(a,f(a,?y)),f(a,f(a,f(a,?y))))))) = f(a,f(a,f(a,f(a,f(a,g(?y,f(a,?y))))))), f(a,f(a,f(a,g(f(a,f(a,f(a,?y))),f(a,f(a,f(a,f(a,?y)))))))) = f(a,f(a,f(a,f(a,f(a,f(a,g(?y,f(a,?y)))))))), f(a,f(a,f(a,g(?y_1,f(a,?y_1))))) = g(f(a,f(a,f(a,?y_1))),f(a,f(a,f(a,f(a,?y_1))))), f(a,f(a,f(a,g(?y_2,f(a,?y_2))))) = f(a,g(f(a,f(a,?y_2)),f(a,f(a,f(a,?y_2))))), f(a,f(a,f(a,g(?y_2,f(a,?y_2))))) = f(a,f(a,g(f(a,?y_2),f(a,f(a,?y_2))))) ] 425.trs: Failure(timeout) (110293 msec.)