NO
af/ONE-SORTED/511.trs
Input rules:
   [ b -> a,
     b -> c,
     c -> c,
     d -> c,
     d -> e,
     f(?x:o,a) -> A,
     f(?x:o,e) -> A,
     f(?x:o,A) -> A,
     f(c,?x:o) -> A ]
Sorts having no ground terms: 
Rules applicable to ground terms:
   [ b -> a,
     b -> c,
     c -> c,
     d -> c,
     d -> e,
     f(?x:o,a) -> A,
     f(?x:o,e) -> A,
     f(?x:o,A) -> A,
     f(c,?x:o) -> A ]
Constructor pattern: [a,e,A]
Defined pattern: [f(?x_2,?x_3),d,c,b]
Constructor subsystem:
   [ ]
Modified Constructor subsystem:
   [ ]
candidate for f(?x_2,?x_3):
   [ f(?x,a) -> A,
     f(?x,e) -> A,
     f(?x,A) -> A ]
candidate for d:
   [ d -> c ]
   [ d -> e ]
No orientable rules for c. Add rules, and retry...
failed to construct defining rules
Retry with a different D/C-partition.
Constructor pattern: [a,e,A,c]
Defined pattern: [f(?x_2,?x_3),d,b]
Constructor subsystem:
   [ c -> c ]
c -> c
{}
   [  ]
Modified Constructor subsystem:
   [ ]
candidate for f(?x_2,?x_3):
No canditates. Supplement rules, and retry...
patlist: 
{?x,a}
{?x,e}
{?x,A}
{c,?x}
Required Patterns: {f(e,c),f(A,c),f(a,c)}
failed to construct defining rules
Retry with a different D/C-partition.
Constructor pattern: [a,e,A,c,f(?x_2,?x_3)]
Defined pattern: [d,b]
Constructor subsystem:
   [ c -> c,
     f(?x,a) -> A,
     f(?x,e) -> A,
     f(?x,A) -> A,
     f(c,?x) -> A ]
c -> c
{}
   [  ]
Modified Constructor subsystem:
   [ f(?x,a) -> A,
     f(?x,e) -> A,
     f(?x,A) -> A,
     f(c,?x) -> A ]
candidate for d:
   [ d -> c ]
   [ d -> e ]
candidate for b:
   [ b -> a ]
   [ b -> c ]
Find a quasi-ordering ...
order successfully found
Precedence:
 e : Mul;
 d : Mul,  b : Mul,  a : Mul;
 A : Mul;
 c : Mul;
 f : Mul;
Rules:
   [ d -> c,
     b -> c,
     f(?x,a) -> A,
     f(?x,e) -> A,
     f(?x,A) -> A ]
Check confluence of constructor subsystem...
Check Termination...
Terminating, WCR: CR
Conjectures:
   [ b = a,
     d = e,
     f(c,?x) = A ]
STEP 0
ES:
   [ b = a,
     d = e,
     f(c,?x) = A ]
HS:
   [ ]
ES0:
   [ c = a,
     c = e,
     f(c,?x) = A ]
HS0:
   [ ]
ES1:
   [ c = a,
     c = e,
     f(c,?x) = A ]
HS1:
   [ ]
: Success(not GCR)
(4 msec.)
0.02