YES
af/ONE-SORTED/114.trs
Input rules:
   [ a1 -> b1,
     a1 -> c1,
     b1 -> b2,
     c1 -> c2,
     a2 -> b2,
     a2 -> c2,
     b2 -> b3,
     c2 -> c3,
     a3 -> b3,
     a3 -> c3,
     b3 -> b4,
     c3 -> c4,
     a4 -> b4,
     a4 -> c4,
     b4 -> b5,
     c4 -> c5,
     a5 -> b6,
     b5 -> b6,
     c5 -> b6 ]
Sorts having no ground terms: 
Rules applicable to ground terms:
   [ a1 -> b1,
     a1 -> c1,
     b1 -> b2,
     c1 -> c2,
     a2 -> b2,
     a2 -> c2,
     b2 -> b3,
     c2 -> c3,
     a3 -> b3,
     a3 -> c3,
     b3 -> b4,
     c3 -> c4,
     a4 -> b4,
     a4 -> c4,
     b4 -> b5,
     c4 -> c5,
     a5 -> b6,
     b5 -> b6,
     c5 -> b6 ]
Constructor pattern: [b6]
Defined pattern: [a5,c5,b5,a4,c4,b4,a3,c3,b3,a2,c2,b2,c1,b1,a1]
Constructor subsystem:
   [ ]
Modified Constructor subsystem:
   [ ]
candidate for a5:
   [ a5 -> b6 ]
candidate for c5:
   [ c5 -> b6 ]
candidate for b5:
   [ b5 -> b6 ]
candidate for a4:
   [ a4 -> b4 ]
   [ a4 -> c4 ]
candidate for c4:
   [ c4 -> c5 ]
candidate for b4:
   [ b4 -> b5 ]
candidate for a3:
   [ a3 -> b3 ]
   [ a3 -> c3 ]
candidate for c3:
   [ c3 -> c4 ]
candidate for b3:
   [ b3 -> b4 ]
candidate for a2:
   [ a2 -> b2 ]
   [ a2 -> c2 ]
candidate for c2:
   [ c2 -> c3 ]
candidate for b2:
   [ b2 -> b3 ]
candidate for c1:
   [ c1 -> c2 ]
candidate for b1:
   [ b1 -> b2 ]
candidate for a1:
   [ a1 -> b1 ]
   [ a1 -> c1 ]
Find a quasi-ordering ...
order successfully found
Precedence:
 b1 : Mul,  a1 : Mul;
 c1 : Mul,  b2 : Mul,  a5 : Mul,  a4 : Mul,  a3 : Mul,  a2 : Mul;
 c2 : Mul;
 c3 : Mul,  b3 : Mul;
 c4 : Mul,  b4 : Mul;
 c5 : Mul;
 b5 : Mul;
 b6 : Mul;
Rules:
   [ a5 -> b6,
     c5 -> b6,
     b5 -> b6,
     a4 -> b4,
     c4 -> c5,
     b4 -> b5,
     a3 -> b3,
     c3 -> c4,
     b3 -> b4,
     a2 -> c2,
     c2 -> c3,
     b2 -> b3,
     c1 -> c2,
     b1 -> b2,
     a1 -> c1 ]
Conjectures:
   [ a1 = b1,
     a2 = b2,
     a3 = c3,
     a4 = c4 ]
STEP 0
ES:
   [ a1 = b1,
     a2 = b2,
     a3 = c3,
     a4 = c4 ]
HS:
   [ ]
ES0:
   [ b6 = b6,
     b6 = b6,
     b6 = b6,
     b6 = b6 ]
HS0:
   [ ]
ES1:
   [ ]
HS1:
   [ ]
: Success(GCR)
(12 msec.)
0.03