Problem:
 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()

Proof:
 sorted: (order)
 0:a1() -> b1()
   a1() -> c1()
   b1() -> b2()
   c1() -> c2()
   b2() -> b3()
   c2() -> c3()
   b3() -> b4()
   c3() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> b6()
 1:a2() -> b2()
   a2() -> c2()
   b2() -> b3()
   c2() -> c3()
   b3() -> b4()
   c3() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> b6()
 2:a3() -> b3()
   a3() -> c3()
   b3() -> b4()
   c3() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> b6()
 3:a4() -> b4()
   a4() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> b6()
 4:a5() -> b6()
 -----
 sorts
   [1>2, 1>3, 2>6, 3>5, 4>5, 4>6, 5>8, 6>9, 7>8, 7>9, 8>11, 9>12, 10>11, 10>12, 11>14, 12>13,
    13>16, 14>16, 15>16]
 sort attachment (non-strict)
   a1 : 1
   b1 : 2
   c1 : 3
   b2 : 6
   c2 : 5
   a2 : 4
   b3 : 9
   c3 : 8
   a3 : 7
   b4 : 12
   c4 : 11
   a4 : 10
   b5 : 13
   c5 : 14
   a5 : 15
   b6 : 16
 -----
 0:a1() -> b1()
   a1() -> c1()
   b1() -> b2()
   c1() -> c2()
   b2() -> b3()
   c2() -> c3()
   b3() -> b4()
   c3() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> b6()
   Uncurry Processor:
    a1() -> b1()
    a1() -> c1()
    b1() -> b2()
    c1() -> c2()
    b2() -> b3()
    c2() -> c3()
    b3() -> b4()
    c3() -> c4()
    b4() -> b5()
    c4() -> c5()
    b5() -> b6()
    c5() -> b6()
    Church Rosser Transformation Processor:
     
     strict:
      
     weak:
      
     critical peaks: 0
     Qed
 
 
 1:a2() -> b2()
   a2() -> c2()
   b2() -> b3()
   c2() -> c3()
   b3() -> b4()
   c3() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> b6()
   Uncurry Processor:
    a2() -> b2()
    a2() -> c2()
    b2() -> b3()
    c2() -> c3()
    b3() -> b4()
    c3() -> c4()
    b4() -> b5()
    c4() -> c5()
    b5() -> b6()
    c5() -> b6()
    Church Rosser Transformation Processor:
     
     strict:
      
     weak:
      
     critical peaks: 0
     Qed
 
 
 2:a3() -> b3()
   a3() -> c3()
   b3() -> b4()
   c3() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> b6()
   Uncurry Processor:
    a3() -> b3()
    a3() -> c3()
    b3() -> b4()
    c3() -> c4()
    b4() -> b5()
    c4() -> c5()
    b5() -> b6()
    c5() -> b6()
    Church Rosser Transformation Processor:
     
     strict:
      
     weak:
      
     critical peaks: 0
     Qed
 
 
 3:a4() -> b4()
   a4() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> b6()
   Uncurry Processor:
    a4() -> b4()
    a4() -> c4()
    b4() -> b5()
    c4() -> c5()
    b5() -> b6()
    c5() -> b6()
    Church Rosser Transformation Processor:
     
     strict:
      
     weak:
      
     critical peaks: 0
     Qed
 
 
 4:a5() -> b6()
   Church Rosser Transformation Processor:
    
    strict:
     a5() -> b6()
    weak:
     
    critical peaks: 0
    Closedness Processor (*parallel*):
     
     strict:
      
     weak:
      
     Qed