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(f(f(f(?x)))) -> f(f(f(g(?x,f(?x))))), f(?x) -> g(?x,f(?x)) ] Apply Direct Methods... Inner CPs: [ f(g(f(f(?x)),f(f(f(?x))))) = f(f(f(g(?x,f(?x))))), f(f(g(f(?x),f(f(?x))))) = f(f(f(g(?x,f(?x))))), f(f(f(g(?x_1,f(?x_1))))) = f(f(f(g(?x_1,f(?x_1))))), f(f(f(f(g(?x,f(?x)))))) = f(f(f(g(f(?x),f(f(?x)))))), f(f(f(f(f(g(?x,f(?x))))))) = f(f(f(g(f(f(?x)),f(f(f(?x))))))), f(f(f(f(f(f(g(?x,f(?x)))))))) = f(f(f(g(f(f(f(?x))),f(f(f(f(?x)))))))) ] Outer CPs: [ f(f(f(g(?x,f(?x))))) = g(f(f(f(?x))),f(f(f(f(?x))))) ] 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(f(f(g(?x_12,f(?x_12))))) = f(f(f(g(?x_12,f(?x_12))))) {?x_12}, f(f(f(f(f(f(g(?x_9,f(?x_9)))))))) = f(f(f(g(f(f(f(?x_9))),f(f(f(f(?x_9)))))))) {?x_9}, f(f(g(?x_7,f(?x_7)))) = f(f(f(g(?x,f(?x))))) {?x}, f(f(f(f(f(g(?x_4,f(?x_4))))))) = f(f(f(g(f(f(?x_4)),f(f(f(?x_4))))))) {?x_4}, f(g(f(f(?x)),f(f(f(?x))))) = f(f(f(g(?x,f(?x))))) {?x}, f(f(f(f(g(?x_1,f(?x_1)))))) = f(f(f(g(f(?x_1),f(f(?x_1)))))) {?x_1} ] unknown Toyama (Parallel CPs) Simultaneous CPs: [ g(g(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1))))))),f(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1))))))))),f(g(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1))))))),f(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1))))))))))) = f(f(f(g(f(f(f(?x_1))),f(f(f(f(?x_1)))))))), g(g(g(g(?x,f(?x)),f(g(?x,f(?x)))),f(g(g(?x,f(?x)),f(g(?x,f(?x)))))),f(g(g(g(?x,f(?x)),f(g(?x,f(?x)))),f(g(g(?x,f(?x)),f(g(?x,f(?x)))))))) = f(f(f(g(?x,f(?x))))), g(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1))))))),f(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1))))))))) = f(f(f(g(f(f(?x_1)),f(f(f(?x_1))))))), g(g(g(f(?x),f(f(?x))),f(g(f(?x),f(f(?x))))),f(g(g(f(?x),f(f(?x))),f(g(f(?x),f(f(?x))))))) = f(f(f(g(?x,f(?x))))), g(g(f(f(f(f(g(?x_1,f(?x_1)))))),f(f(f(f(f(g(?x_1,f(?x_1)))))))),f(g(f(f(f(f(g(?x_1,f(?x_1)))))),f(f(f(f(f(g(?x_1,f(?x_1)))))))))) = f(f(f(g(f(f(f(?x_1))),f(f(f(f(?x_1)))))))), g(g(f(g(?x,f(?x))),f(f(g(?x,f(?x))))),f(g(f(g(?x,f(?x))),f(f(g(?x,f(?x))))))) = f(f(f(g(?x,f(?x))))), g(f(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1)))))))),f(f(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1)))))))))) = f(f(f(g(f(f(f(?x_1))),f(f(f(f(?x_1)))))))), g(f(g(g(?x,f(?x)),f(g(?x,f(?x))))),f(f(g(g(?x,f(?x)),f(g(?x,f(?x))))))) = f(f(f(g(?x,f(?x))))), f(g(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1))))))),f(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1)))))))))) = f(f(f(g(f(f(f(?x_1))),f(f(f(f(?x_1)))))))), f(g(g(g(?x,f(?x)),f(g(?x,f(?x)))),f(g(g(?x,f(?x)),f(g(?x,f(?x))))))) = f(f(f(g(?x,f(?x))))), g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1))))))) = f(f(f(g(f(?x_1),f(f(?x_1)))))), g(g(f(f(?x)),f(f(f(?x)))),f(g(f(f(?x)),f(f(f(?x)))))) = f(f(f(g(?x,f(?x))))), g(f(f(f(f(g(?x_1,f(?x_1)))))),f(f(f(f(f(g(?x_1,f(?x_1)))))))) = f(f(f(g(f(f(?x_1)),f(f(f(?x_1))))))), g(f(g(f(?x),f(f(?x)))),f(f(g(f(?x),f(f(?x)))))) = f(f(f(g(?x,f(?x))))), g(f(f(f(f(f(g(?x_1,f(?x_1))))))),f(f(f(f(f(f(g(?x_1,f(?x_1))))))))) = f(f(f(g(f(f(f(?x_1))),f(f(f(f(?x_1)))))))), g(f(f(g(?x,f(?x)))),f(f(f(g(?x,f(?x)))))) = f(f(f(g(?x,f(?x))))), f(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1)))))))) = f(f(f(g(f(f(?x_1)),f(f(f(?x_1))))))), f(g(g(f(?x),f(f(?x))),f(g(f(?x),f(f(?x)))))) = f(f(f(g(?x,f(?x))))), f(g(f(f(f(f(g(?x_1,f(?x_1)))))),f(f(f(f(f(g(?x_1,f(?x_1))))))))) = f(f(f(g(f(f(f(?x_1))),f(f(f(f(?x_1)))))))), f(g(f(g(?x,f(?x))),f(f(g(?x,f(?x)))))) = f(f(f(g(?x,f(?x))))), f(f(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1))))))))) = f(f(f(g(f(f(f(?x_1))),f(f(f(f(?x_1)))))))), f(f(g(g(?x,f(?x)),f(g(?x,f(?x)))))) = f(f(f(g(?x,f(?x))))), g(f(f(f(?x))),f(f(f(f(?x))))) = f(f(f(g(?x,f(?x))))), f(f(f(f(g(?x_1,f(?x_1)))))) = f(f(f(g(f(?x_1),f(f(?x_1)))))), f(g(f(f(?x)),f(f(f(?x))))) = f(f(f(g(?x,f(?x))))), f(f(f(f(f(g(?x_1,f(?x_1))))))) = f(f(f(g(f(f(?x_1)),f(f(f(?x_1))))))), f(f(g(f(?x),f(f(?x))))) = f(f(f(g(?x,f(?x))))), f(f(f(f(f(f(g(?x_1,f(?x_1)))))))) = f(f(f(g(f(f(f(?x_1))),f(f(f(f(?x_1)))))))), f(f(f(g(?x,f(?x))))) = f(f(f(g(?x,f(?x))))), f(f(f(g(g(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1))))))),f(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1))))))))),f(g(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1))))))),f(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1)))))))))))))) = f(f(f(f(f(f(g(f(f(f(?x_1))),f(f(f(f(?x_1))))))))))), f(f(f(g(g(g(g(?x,f(?x)),f(g(?x,f(?x)))),f(g(g(?x,f(?x)),f(g(?x,f(?x)))))),f(g(g(g(?x,f(?x)),f(g(?x,f(?x)))),f(g(g(?x,f(?x)),f(g(?x,f(?x))))))))))) = f(f(f(f(f(f(g(?x,f(?x)))))))), f(f(f(g(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1))))))),f(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1)))))))))))) = f(f(f(f(f(g(f(f(f(?x_1))),f(f(f(f(?x_1)))))))))), f(f(f(g(g(g(?x,f(?x)),f(g(?x,f(?x)))),f(g(g(?x,f(?x)),f(g(?x,f(?x))))))))) = f(f(f(f(f(g(?x,f(?x))))))), f(f(f(g(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1))))))),f(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1)))))))))))) = f(f(f(f(f(f(g(f(f(?x_1)),f(f(f(?x_1)))))))))), f(f(f(g(g(g(f(?x),f(f(?x))),f(g(f(?x),f(f(?x))))),f(g(g(f(?x),f(f(?x))),f(g(f(?x),f(f(?x)))))))))) = f(f(f(f(f(f(g(?x,f(?x)))))))), f(f(f(g(g(f(f(f(f(g(?x_1,f(?x_1)))))),f(f(f(f(f(g(?x_1,f(?x_1)))))))),f(g(f(f(f(f(g(?x_1,f(?x_1)))))),f(f(f(f(f(g(?x_1,f(?x_1))))))))))))) = f(f(f(f(f(f(g(f(f(f(?x_1))),f(f(f(f(?x_1))))))))))), f(f(f(g(g(f(g(?x,f(?x))),f(f(g(?x,f(?x))))),f(g(f(g(?x,f(?x))),f(f(g(?x,f(?x)))))))))) = f(f(f(f(f(f(g(?x,f(?x)))))))), f(f(f(g(f(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1)))))))),f(f(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1))))))))))))) = f(f(f(f(f(f(g(f(f(f(?x_1))),f(f(f(f(?x_1))))))))))), f(f(f(g(f(g(g(?x,f(?x)),f(g(?x,f(?x))))),f(f(g(g(?x,f(?x)),f(g(?x,f(?x)))))))))) = f(f(f(f(f(f(g(?x,f(?x)))))))), f(f(f(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1)))))))))) = f(f(f(f(g(f(f(f(?x_1))),f(f(f(f(?x_1))))))))), f(f(f(g(g(?x,f(?x)),f(g(?x,f(?x))))))) = f(f(f(f(g(?x,f(?x)))))), f(f(f(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1)))))))))) = f(f(f(f(f(g(f(f(?x_1)),f(f(f(?x_1))))))))), f(f(f(g(g(f(?x),f(f(?x))),f(g(f(?x),f(f(?x)))))))) = f(f(f(f(f(g(?x,f(?x))))))), f(f(f(g(f(f(f(f(g(?x_1,f(?x_1)))))),f(f(f(f(f(g(?x_1,f(?x_1))))))))))) = f(f(f(f(f(g(f(f(f(?x_1))),f(f(f(f(?x_1)))))))))), f(f(f(g(f(g(?x,f(?x))),f(f(g(?x,f(?x)))))))) = f(f(f(f(f(g(?x,f(?x))))))), f(f(f(g(f(f(f(g(?x_1,f(?x_1))))),f(f(f(f(g(?x_1,f(?x_1)))))))))) = f(f(f(f(f(f(g(f(?x_1),f(f(?x_1))))))))), f(f(f(g(g(f(f(?x)),f(f(f(?x)))),f(g(f(f(?x)),f(f(f(?x))))))))) = f(f(f(f(f(f(g(?x,f(?x)))))))), f(f(f(g(f(f(f(f(g(?x_1,f(?x_1)))))),f(f(f(f(f(g(?x_1,f(?x_1))))))))))) = f(f(f(f(f(f(g(f(f(?x_1)),f(f(f(?x_1)))))))))), f(f(f(g(f(g(f(?x),f(f(?x)))),f(f(g(f(?x),f(f(?x))))))))) = f(f(f(f(f(f(g(?x,f(?x)))))))), f(f(f(g(f(f(f(f(f(g(?x_1,f(?x_1))))))),f(f(f(f(f(f(g(?x_1,f(?x_1)))))))))))) = f(f(f(f(f(f(g(f(f(f(?x_1))),f(f(f(f(?x_1))))))))))), f(f(f(g(f(f(g(?x,f(?x)))),f(f(f(g(?x,f(?x))))))))) = f(f(f(f(f(f(g(?x,f(?x)))))))), f(f(f(g(f(?x),f(f(?x)))))) = f(f(f(f(g(?x,f(?x)))))), f(f(f(g(f(f(?x)),f(f(f(?x))))))) = f(f(f(f(f(g(?x,f(?x))))))), f(f(f(g(f(f(f(?x))),f(f(f(f(?x)))))))) = f(f(f(f(f(f(g(?x,f(?x)))))))), f(f(f(g(?x_1,f(?x_1))))) = g(f(f(f(?x_1))),f(f(f(f(?x_1))))), f(f(f(g(?x_2,f(?x_2))))) = f(g(f(f(?x_2)),f(f(f(?x_2))))), f(f(f(g(?x_2,f(?x_2))))) = f(f(g(f(?x_2),f(f(?x_2))))) ] 424.trs: Failure(timeout) (114980 msec.)