MAYBE
af/ONE-SORTED/740.trs
Input rules:
   [ f(a,f(?x:o,a)) -> f(a,f(f(a,a),a)) ]
Sorts having no ground terms: 
Rules applicable to ground terms:
   [ f(a,f(?x:o,a)) -> f(a,f(f(a,a),a)) ]
Constructor pattern: [f(?x_1,?x_2),a]
Defined pattern: []
Constructor subsystem:
   [ f(a,f(?x,a)) -> f(a,f(f(a,a),a)) ]
f(a,f(?x,a)) -> f(a,f(f(a,a),a))
{?x:=f(a,a)}
   [ {?x:=f(a,f(?x_1,?x_2))};
     {?x:=f(f(?x_1,?x_2),a)};
     {?x:=f(f(?x_1,?x_2),f(?x_3,?x_4))};
     {?x:=a} ]
Modified Constructor subsystem:
   [ f(a,f(f(a,f(?x_1,?x_2)),a)) -> f(a,f(f(a,a),a)),
     f(a,f(f(f(?x_1,?x_2),a),a)) -> f(a,f(f(a,a),a)),
     f(a,f(f(f(?x_1,?x_2),f(?x_3,?x_4)),a)) -> f(a,f(f(a,a),a)),
     f(a,f(a,a)) -> f(a,f(f(a,a),a)) ]
Find a quasi-ordering ...
order successfully found
Precedence:
 f : Mul;
 a : Mul;
Rules:
   [ f(a,f(f(a,f(?x_1,?x_2)),a)) -> f(a,f(f(a,a),a)),
     f(a,f(f(f(?x_1,?x_2),a),a)) -> f(a,f(f(a,a),a)),
     f(a,f(f(f(?x_1,?x_2),f(?x_3,?x_4)),a)) -> f(a,f(f(a,a),a)) ]
Check confluence of constructor subsystem...
Check Termination...
Terminating, WCR: CR
Conjectures:
   [ f(a,f(a,a)) = f(a,f(f(a,a),a)) ]
STEP 0
ES:
   [ f(a,f(a,a)) = f(a,f(f(a,a),a)) ]
HS:
   [ ]
ES0:
   [ f(a,f(a,a)) = f(a,f(f(a,a),a)) ]
HS0:
   [ ]
ES1:
   [ f(a,f(a,a)) = f(a,f(f(a,a),a)) ]
HS1:
   [ ]
No equation to expand
check Non-Ground-Confluence...
ground constructor terms for instantiation: {a,f(a,a)}
ground terms for instantiation: {a:o,f(a,a):o}
obtain 1 rules by 3 steps unfolding
obtain 0 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (failure)
check by Interpretation(mod2) (failure)
check by Descendants-Approximation, check by Ordering(poly) (failure)
: Failure(unknown)
(10 msec.)
0.02