NO af/ONE-SORTED/737.trs Input rules: [ f(a,f(a,?x:o)) -> b ] Sorts having no ground terms: Rules applicable to ground terms: [ f(a,f(a,?x:o)) -> b ] Constructor pattern: [f(?x_1,?x_2),a,b] Defined pattern: [] Constructor subsystem: [ f(a,f(a,?x)) -> b ] Modified Constructor subsystem: [ f(a,f(a,?x)) -> b ] Find a quasi-ordering ... order successfully found Precedence: f : Mul; a : Mul; b : Mul; Rules: [ f(a,f(a,?x)) -> b ] Check confluence of constructor subsystem... Check Termination... Terminating, not WCR: not CR ...failed failed to find an ordering. Try to supplement auxiliary rules. {}Supplemented Rules: [ ] failed to supplement auxiliary rules check Non-Ground-Confluence... ground constructor terms for instantiation: {a,b,f(a,a),f(a,b),f(b,a),f(b,b)} ground terms for instantiation: {a:o,b:o,f(a,a):o,f(a,b):o,f(b,a):o,f(b,b):o} obtain 10 rules by 3 steps unfolding obtain 5 candidates for checking non-joinability check by TCAP-Approximation (success) Witness for Non-Confluence: b> : Success(not GCR) (22 msec.) 0.03