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() -> b5()
 a5() -> c5()
 b5() -> b6()
 c5() -> c6()
 a6() -> b6()
 a6() -> c6()
 b6() -> b7()
 c6() -> b7()
 b7() -> b1()
 b7() -> c1()

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() -> c6()
   b6() -> b7()
   c6() -> b7()
   b7() -> b1()
   b7() -> c1()
 1:b1() -> b2()
   c1() -> c2()
   a2() -> b2()
   a2() -> c2()
   b2() -> b3()
   c2() -> c3()
   b3() -> b4()
   c3() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> c6()
   b6() -> b7()
   c6() -> b7()
   b7() -> b1()
   b7() -> c1()
 2:b1() -> b2()
   c1() -> c2()
   b2() -> b3()
   c2() -> c3()
   a3() -> b3()
   a3() -> c3()
   b3() -> b4()
   c3() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> c6()
   b6() -> b7()
   c6() -> b7()
   b7() -> b1()
   b7() -> c1()
 3:b1() -> b2()
   c1() -> c2()
   b2() -> b3()
   c2() -> c3()
   b3() -> b4()
   c3() -> c4()
   a4() -> b4()
   a4() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> c6()
   b6() -> b7()
   c6() -> b7()
   b7() -> b1()
   b7() -> c1()
 4:b1() -> b2()
   c1() -> c2()
   b2() -> b3()
   c2() -> c3()
   b3() -> b4()
   c3() -> c4()
   b4() -> b5()
   c4() -> c5()
   a5() -> b5()
   a5() -> c5()
   b5() -> b6()
   c5() -> c6()
   b6() -> b7()
   c6() -> b7()
   b7() -> b1()
   b7() -> c1()
 5:b1() -> b2()
   c1() -> c2()
   b2() -> b3()
   c2() -> c3()
   b3() -> b4()
   c3() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> c6()
   a6() -> b6()
   a6() -> c6()
   b6() -> b7()
   c6() -> b7()
   b7() -> b1()
   b7() -> c1()
 -----
 sorts
   [1>7, 2>7, 3>7, 4>7, 5>7, 6>7]
 sort attachment (non-strict)
   a1 : 1
   b1 : 7
   c1 : 7
   b2 : 7
   c2 : 7
   a2 : 2
   b3 : 7
   c3 : 7
   a3 : 3
   b4 : 7
   c4 : 7
   a4 : 4
   b5 : 7
   c5 : 7
   a5 : 5
   b6 : 7
   c6 : 7
   a6 : 6
   b7 : 7
 -----
 0:a1() -> b1()
   a1() -> c1()
   b1() -> b2()
   c1() -> c2()
   b2() -> b3()
   c2() -> c3()
   b3() -> b4()
   c3() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> c6()
   b6() -> b7()
   c6() -> b7()
   b7() -> b1()
   b7() -> c1()
   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() -> c6()
    b6() -> b7()
    c6() -> b7()
    b7() -> b1()
    b7() -> c1()
    Church Rosser Transformation Processor:
     
     strict:
      
     weak:
      
     critical peaks: 0
     Qed
 
 
 1:b1() -> b2()
   c1() -> c2()
   a2() -> b2()
   a2() -> c2()
   b2() -> b3()
   c2() -> c3()
   b3() -> b4()
   c3() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> c6()
   b6() -> b7()
   c6() -> b7()
   b7() -> b1()
   b7() -> c1()
   Uncurry Processor:
    b1() -> b2()
    c1() -> c2()
    a2() -> b2()
    a2() -> c2()
    b2() -> b3()
    c2() -> c3()
    b3() -> b4()
    c3() -> c4()
    b4() -> b5()
    c4() -> c5()
    b5() -> b6()
    c5() -> c6()
    b6() -> b7()
    c6() -> b7()
    b7() -> b1()
    b7() -> c1()
    Church Rosser Transformation Processor:
     
     strict:
      
     weak:
      
     critical peaks: 0
     Qed
 
 
 2:b1() -> b2()
   c1() -> c2()
   b2() -> b3()
   c2() -> c3()
   a3() -> b3()
   a3() -> c3()
   b3() -> b4()
   c3() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> c6()
   b6() -> b7()
   c6() -> b7()
   b7() -> b1()
   b7() -> c1()
   Uncurry Processor:
    b1() -> b2()
    c1() -> c2()
    b2() -> b3()
    c2() -> c3()
    a3() -> b3()
    a3() -> c3()
    b3() -> b4()
    c3() -> c4()
    b4() -> b5()
    c4() -> c5()
    b5() -> b6()
    c5() -> c6()
    b6() -> b7()
    c6() -> b7()
    b7() -> b1()
    b7() -> c1()
    Church Rosser Transformation Processor:
     
     strict:
      
     weak:
      
     critical peaks: 0
     Qed
 
 
 3:b1() -> b2()
   c1() -> c2()
   b2() -> b3()
   c2() -> c3()
   b3() -> b4()
   c3() -> c4()
   a4() -> b4()
   a4() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> c6()
   b6() -> b7()
   c6() -> b7()
   b7() -> b1()
   b7() -> c1()
   Uncurry Processor:
    b1() -> b2()
    c1() -> c2()
    b2() -> b3()
    c2() -> c3()
    b3() -> b4()
    c3() -> c4()
    a4() -> b4()
    a4() -> c4()
    b4() -> b5()
    c4() -> c5()
    b5() -> b6()
    c5() -> c6()
    b6() -> b7()
    c6() -> b7()
    b7() -> b1()
    b7() -> c1()
    Church Rosser Transformation Processor:
     
     strict:
      
     weak:
      
     critical peaks: 0
     Qed
 
 
 4:b1() -> b2()
   c1() -> c2()
   b2() -> b3()
   c2() -> c3()
   b3() -> b4()
   c3() -> c4()
   b4() -> b5()
   c4() -> c5()
   a5() -> b5()
   a5() -> c5()
   b5() -> b6()
   c5() -> c6()
   b6() -> b7()
   c6() -> b7()
   b7() -> b1()
   b7() -> c1()
   Uncurry Processor:
    b1() -> b2()
    c1() -> c2()
    b2() -> b3()
    c2() -> c3()
    b3() -> b4()
    c3() -> c4()
    b4() -> b5()
    c4() -> c5()
    a5() -> b5()
    a5() -> c5()
    b5() -> b6()
    c5() -> c6()
    b6() -> b7()
    c6() -> b7()
    b7() -> b1()
    b7() -> c1()
    Church Rosser Transformation Processor:
     
     strict:
      
     weak:
      
     critical peaks: 0
     Qed
 
 
 5:b1() -> b2()
   c1() -> c2()
   b2() -> b3()
   c2() -> c3()
   b3() -> b4()
   c3() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> c6()
   a6() -> b6()
   a6() -> c6()
   b6() -> b7()
   c6() -> b7()
   b7() -> b1()
   b7() -> c1()
   Uncurry Processor:
    b1() -> b2()
    c1() -> c2()
    b2() -> b3()
    c2() -> c3()
    b3() -> b4()
    c3() -> c4()
    b4() -> b5()
    c4() -> c5()
    b5() -> b6()
    c5() -> c6()
    a6() -> b6()
    a6() -> c6()
    b6() -> b7()
    c6() -> b7()
    b7() -> b1()
    b7() -> c1()
    Church Rosser Transformation Processor:
     
     strict:
      
     weak:
      
     critical peaks: 0
     Qed