NO af/ONE-SORTED/739.trs Input rules: [ a -> a, g(g(a)) -> b, g(g(?x:o)) -> g(g(g(b))) ] Sorts having no ground terms: Rules applicable to ground terms: [ a -> a, g(g(a)) -> b, g(g(?x:o)) -> g(g(g(b))) ] Constructor pattern: [g(?x_1),b] Defined pattern: [a] Constructor subsystem: [ g(g(?x)) -> g(g(g(b))) ] g(g(?x)) -> g(g(g(b))) {?x:=g(b)} [ {?x:=g(g(?x_1))}; {?x:=b} ] Modified Constructor subsystem: [ g(g(g(g(?x_1)))) -> g(g(g(b))), g(g(b)) -> g(g(g(b))) ] No orientable rules for a. Add rules, and retry... failed to construct defining rules Retry with a different D/C-partition. Constructor pattern: [g(?x_1),b,a] Defined pattern: [] Constructor subsystem: [ a -> a, g(g(a)) -> b, g(g(?x)) -> g(g(g(b))) ] g(g(?x)) -> g(g(g(b))) {?x:=g(b)} [ {?x:=g(g(?x_1))}; {?x:=g(a)}; {?x:=b}; {?x:=a} ] a -> a {} [ ] Modified Constructor subsystem: [ g(g(a)) -> b, g(g(g(g(?x_1)))) -> g(g(g(b))), g(g(g(a))) -> g(g(g(b))), g(g(b)) -> g(g(g(b))), g(g(a)) -> g(g(g(b))) ] Find a quasi-ordering ... order successfully found Precedence: b : Mul, a : Mul; g : Mul; Rules: [ g(g(a)) -> b, g(g(g(a))) -> g(g(g(b))) ] Check confluence of constructor subsystem... Check Termination... unknown Terminating, Linear, unknown Oostrom, unknown strongly closed: Can't judge ...failed failed to find an ordering. Try to supplement auxiliary rules. {a}{}{g(b),g(g(b)),g(g(g(b)))}Supplemented Rules: [ ] failed to supplement auxiliary rules check Non-Ground-Confluence... ground constructor terms for instantiation: {b,g(b)} ground terms for instantiation: {b:o,g(b):o} obtain 3 rules by 3 steps unfolding obtain 19 candidates for checking non-joinability check by TCAP-Approximation (failure) check by Ordering(rpo), check by Tree-Automata Approximation (success) where F = {(a,0),(b,0),(g,1)} Q = {q_0,q_1,q_{g(g(b))},q_{b},q_{g(b)}} Qf = {q_0,q_1} Delta = [ b -> q_1, b -> q_{b}, g(q_{g(g(b))}) -> q_0, g(q_{g(g(b))}) -> q_{g(g(b))}, g(q_{b}) -> q_{g(b)}, g(q_{g(b)}) -> q_{g(g(b))} ] Witness for Non-Confluence: : Success(not GCR) (13 msec.) 0.03