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()
   Church Rosser Transformation Processor (kb):
    a1() -> b1()
    a1() -> c1()
    b1() -> b2()
    c1() -> c2()
    b2() -> b3()
    c2() -> c3()
    b3() -> b4()
    c3() -> c4()
    b4() -> b5()
    c4() -> c5()
    b5() -> b6()
    c5() -> b6()
    critical peaks: joinable
    Matrix Interpretation Processor: dim=3
     
     interpretation:
             [0]
      [b6] = [0]
             [0],
      
             [0]
      [c5] = [0]
             [0],
      
             [0]
      [b5] = [0]
             [0],
      
             [0]
      [c4] = [0]
             [0],
      
             [0]
      [b4] = [0]
             [0],
      
             [0]
      [c3] = [0]
             [0],
      
             [0]
      [b3] = [0]
             [0],
      
             [0]
      [c2] = [0]
             [0],
      
             [0]
      [b2] = [0]
             [0],
      
             [0]
      [c1] = [0]
             [0],
      
             [0]
      [b1] = [0]
             [0],
      
             [1]
      [a1] = [0]
             [0]
     orientation:
             [1]    [0]       
      a1() = [0] >= [0] = b1()
             [0]    [0]       
      
             [1]    [0]       
      a1() = [0] >= [0] = c1()
             [0]    [0]       
      
             [0]    [0]       
      b1() = [0] >= [0] = b2()
             [0]    [0]       
      
             [0]    [0]       
      c1() = [0] >= [0] = c2()
             [0]    [0]       
      
             [0]    [0]       
      b2() = [0] >= [0] = b3()
             [0]    [0]       
      
             [0]    [0]       
      c2() = [0] >= [0] = c3()
             [0]    [0]       
      
             [0]    [0]       
      b3() = [0] >= [0] = b4()
             [0]    [0]       
      
             [0]    [0]       
      c3() = [0] >= [0] = c4()
             [0]    [0]       
      
             [0]    [0]       
      b4() = [0] >= [0] = b5()
             [0]    [0]       
      
             [0]    [0]       
      c4() = [0] >= [0] = c5()
             [0]    [0]       
      
             [0]    [0]       
      b5() = [0] >= [0] = b6()
             [0]    [0]       
      
             [0]    [0]       
      c5() = [0] >= [0] = b6()
             [0]    [0]       
     problem:
      b1() -> b2()
      c1() -> c2()
      b2() -> b3()
      c2() -> c3()
      b3() -> b4()
      c3() -> c4()
      b4() -> b5()
      c4() -> c5()
      b5() -> b6()
      c5() -> b6()
     Matrix Interpretation Processor: dim=3
      
      interpretation:
              [0]
       [b6] = [0]
              [0],
       
              [0]
       [c5] = [0]
              [0],
       
              [0]
       [b5] = [0]
              [0],
       
              [0]
       [c4] = [0]
              [0],
       
              [0]
       [b4] = [0]
              [0],
       
              [0]
       [c3] = [0]
              [0],
       
              [0]
       [b3] = [0]
              [0],
       
              [0]
       [c2] = [0]
              [0],
       
              [0]
       [b2] = [0]
              [0],
       
              [1]
       [c1] = [0]
              [0],
       
              [1]
       [b1] = [0]
              [0]
      orientation:
              [1]    [0]       
       b1() = [0] >= [0] = b2()
              [0]    [0]       
       
              [1]    [0]       
       c1() = [0] >= [0] = c2()
              [0]    [0]       
       
              [0]    [0]       
       b2() = [0] >= [0] = b3()
              [0]    [0]       
       
              [0]    [0]       
       c2() = [0] >= [0] = c3()
              [0]    [0]       
       
              [0]    [0]       
       b3() = [0] >= [0] = b4()
              [0]    [0]       
       
              [0]    [0]       
       c3() = [0] >= [0] = c4()
              [0]    [0]       
       
              [0]    [0]       
       b4() = [0] >= [0] = b5()
              [0]    [0]       
       
              [0]    [0]       
       c4() = [0] >= [0] = c5()
              [0]    [0]       
       
              [0]    [0]       
       b5() = [0] >= [0] = b6()
              [0]    [0]       
       
              [0]    [0]       
       c5() = [0] >= [0] = b6()
              [0]    [0]       
      problem:
       b2() -> b3()
       c2() -> c3()
       b3() -> b4()
       c3() -> c4()
       b4() -> b5()
       c4() -> c5()
       b5() -> b6()
       c5() -> b6()
      Matrix Interpretation Processor: dim=3
       
       interpretation:
               [0]
        [b6] = [0]
               [0],
        
               [0]
        [c5] = [0]
               [0],
        
               [0]
        [b5] = [0]
               [0],
        
               [0]
        [c4] = [0]
               [0],
        
               [0]
        [b4] = [0]
               [0],
        
               [0]
        [c3] = [0]
               [0],
        
               [0]
        [b3] = [0]
               [0],
        
               [1]
        [c2] = [0]
               [0],
        
               [1]
        [b2] = [0]
               [0]
       orientation:
               [1]    [0]       
        b2() = [0] >= [0] = b3()
               [0]    [0]       
        
               [1]    [0]       
        c2() = [0] >= [0] = c3()
               [0]    [0]       
        
               [0]    [0]       
        b3() = [0] >= [0] = b4()
               [0]    [0]       
        
               [0]    [0]       
        c3() = [0] >= [0] = c4()
               [0]    [0]       
        
               [0]    [0]       
        b4() = [0] >= [0] = b5()
               [0]    [0]       
        
               [0]    [0]       
        c4() = [0] >= [0] = c5()
               [0]    [0]       
        
               [0]    [0]       
        b5() = [0] >= [0] = b6()
               [0]    [0]       
        
               [0]    [0]       
        c5() = [0] >= [0] = b6()
               [0]    [0]       
       problem:
        b3() -> b4()
        c3() -> c4()
        b4() -> b5()
        c4() -> c5()
        b5() -> b6()
        c5() -> b6()
       Matrix Interpretation Processor: dim=3
        
        interpretation:
                [0]
         [b6] = [0]
                [0],
         
                [0]
         [c5] = [0]
                [0],
         
                [0]
         [b5] = [0]
                [0],
         
                [0]
         [c4] = [0]
                [0],
         
                [0]
         [b4] = [0]
                [0],
         
                [1]
         [c3] = [0]
                [0],
         
                [1]
         [b3] = [0]
                [0]
        orientation:
                [1]    [0]       
         b3() = [0] >= [0] = b4()
                [0]    [0]       
         
                [1]    [0]       
         c3() = [0] >= [0] = c4()
                [0]    [0]       
         
                [0]    [0]       
         b4() = [0] >= [0] = b5()
                [0]    [0]       
         
                [0]    [0]       
         c4() = [0] >= [0] = c5()
                [0]    [0]       
         
                [0]    [0]       
         b5() = [0] >= [0] = b6()
                [0]    [0]       
         
                [0]    [0]       
         c5() = [0] >= [0] = b6()
                [0]    [0]       
        problem:
         b4() -> b5()
         c4() -> c5()
         b5() -> b6()
         c5() -> b6()
        Matrix Interpretation Processor: dim=3
         
         interpretation:
                 [0]
          [b6] = [0]
                 [0],
          
                 [0]
          [c5] = [0]
                 [0],
          
                 [0]
          [b5] = [0]
                 [0],
          
                 [1]
          [c4] = [0]
                 [0],
          
                 [1]
          [b4] = [0]
                 [0]
         orientation:
                 [1]    [0]       
          b4() = [0] >= [0] = b5()
                 [0]    [0]       
          
                 [1]    [0]       
          c4() = [0] >= [0] = c5()
                 [0]    [0]       
          
                 [0]    [0]       
          b5() = [0] >= [0] = b6()
                 [0]    [0]       
          
                 [0]    [0]       
          c5() = [0] >= [0] = b6()
                 [0]    [0]       
         problem:
          b5() -> b6()
          c5() -> b6()
         Matrix Interpretation Processor: dim=3
          
          interpretation:
                  [0]
           [b6] = [0]
                  [0],
           
                  [1]
           [c5] = [0]
                  [0],
           
                  [1]
           [b5] = [0]
                  [0]
          orientation:
                  [1]    [0]       
           b5() = [0] >= [0] = b6()
                  [0]    [0]       
           
                  [1]    [0]       
           c5() = [0] >= [0] = b6()
                  [0]    [0]       
          problem:
           
          Qed


1:a2() -> b2()
  a2() -> c2()
  b2() -> b3()
  c2() -> c3()
  b3() -> b4()
  c3() -> c4()
  b4() -> b5()
  c4() -> c5()
  b5() -> b6()
  c5() -> b6()
  Church Rosser Transformation Processor (kb):
   a2() -> b2()
   a2() -> c2()
   b2() -> b3()
   c2() -> c3()
   b3() -> b4()
   c3() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> b6()
   critical peaks: joinable
   Matrix Interpretation Processor: dim=3
    
    interpretation:
            [0]
     [b6] = [0]
            [0],
     
            [0]
     [c5] = [0]
            [0],
     
            [0]
     [b5] = [0]
            [0],
     
            [0]
     [c4] = [0]
            [0],
     
            [0]
     [b4] = [0]
            [0],
     
            [0]
     [c3] = [0]
            [0],
     
            [0]
     [b3] = [0]
            [0],
     
            [1]
     [a2] = [0]
            [0],
     
            [0]
     [c2] = [0]
            [0],
     
            [0]
     [b2] = [0]
            [0]
    orientation:
            [1]    [0]       
     a2() = [0] >= [0] = b2()
            [0]    [0]       
     
            [1]    [0]       
     a2() = [0] >= [0] = c2()
            [0]    [0]       
     
            [0]    [0]       
     b2() = [0] >= [0] = b3()
            [0]    [0]       
     
            [0]    [0]       
     c2() = [0] >= [0] = c3()
            [0]    [0]       
     
            [0]    [0]       
     b3() = [0] >= [0] = b4()
            [0]    [0]       
     
            [0]    [0]       
     c3() = [0] >= [0] = c4()
            [0]    [0]       
     
            [0]    [0]       
     b4() = [0] >= [0] = b5()
            [0]    [0]       
     
            [0]    [0]       
     c4() = [0] >= [0] = c5()
            [0]    [0]       
     
            [0]    [0]       
     b5() = [0] >= [0] = b6()
            [0]    [0]       
     
            [0]    [0]       
     c5() = [0] >= [0] = b6()
            [0]    [0]       
    problem:
     b2() -> b3()
     c2() -> c3()
     b3() -> b4()
     c3() -> c4()
     b4() -> b5()
     c4() -> c5()
     b5() -> b6()
     c5() -> b6()
    Matrix Interpretation Processor: dim=3
     
     interpretation:
             [0]
      [b6] = [0]
             [0],
      
             [0]
      [c5] = [0]
             [0],
      
             [0]
      [b5] = [0]
             [0],
      
             [0]
      [c4] = [0]
             [0],
      
             [0]
      [b4] = [0]
             [0],
      
             [0]
      [c3] = [0]
             [0],
      
             [0]
      [b3] = [0]
             [0],
      
             [1]
      [c2] = [0]
             [0],
      
             [1]
      [b2] = [0]
             [0]
     orientation:
             [1]    [0]       
      b2() = [0] >= [0] = b3()
             [0]    [0]       
      
             [1]    [0]       
      c2() = [0] >= [0] = c3()
             [0]    [0]       
      
             [0]    [0]       
      b3() = [0] >= [0] = b4()
             [0]    [0]       
      
             [0]    [0]       
      c3() = [0] >= [0] = c4()
             [0]    [0]       
      
             [0]    [0]       
      b4() = [0] >= [0] = b5()
             [0]    [0]       
      
             [0]    [0]       
      c4() = [0] >= [0] = c5()
             [0]    [0]       
      
             [0]    [0]       
      b5() = [0] >= [0] = b6()
             [0]    [0]       
      
             [0]    [0]       
      c5() = [0] >= [0] = b6()
             [0]    [0]       
     problem:
      b3() -> b4()
      c3() -> c4()
      b4() -> b5()
      c4() -> c5()
      b5() -> b6()
      c5() -> b6()
     Matrix Interpretation Processor: dim=3
      
      interpretation:
              [0]
       [b6] = [0]
              [0],
       
              [0]
       [c5] = [0]
              [0],
       
              [0]
       [b5] = [0]
              [0],
       
              [0]
       [c4] = [0]
              [0],
       
              [0]
       [b4] = [0]
              [0],
       
              [1]
       [c3] = [0]
              [0],
       
              [1]
       [b3] = [0]
              [0]
      orientation:
              [1]    [0]       
       b3() = [0] >= [0] = b4()
              [0]    [0]       
       
              [1]    [0]       
       c3() = [0] >= [0] = c4()
              [0]    [0]       
       
              [0]    [0]       
       b4() = [0] >= [0] = b5()
              [0]    [0]       
       
              [0]    [0]       
       c4() = [0] >= [0] = c5()
              [0]    [0]       
       
              [0]    [0]       
       b5() = [0] >= [0] = b6()
              [0]    [0]       
       
              [0]    [0]       
       c5() = [0] >= [0] = b6()
              [0]    [0]       
      problem:
       b4() -> b5()
       c4() -> c5()
       b5() -> b6()
       c5() -> b6()
      Matrix Interpretation Processor: dim=3
       
       interpretation:
               [0]
        [b6] = [0]
               [0],
        
               [0]
        [c5] = [0]
               [0],
        
               [0]
        [b5] = [0]
               [0],
        
               [1]
        [c4] = [0]
               [0],
        
               [1]
        [b4] = [0]
               [0]
       orientation:
               [1]    [0]       
        b4() = [0] >= [0] = b5()
               [0]    [0]       
        
               [1]    [0]       
        c4() = [0] >= [0] = c5()
               [0]    [0]       
        
               [0]    [0]       
        b5() = [0] >= [0] = b6()
               [0]    [0]       
        
               [0]    [0]       
        c5() = [0] >= [0] = b6()
               [0]    [0]       
       problem:
        b5() -> b6()
        c5() -> b6()
       Matrix Interpretation Processor: dim=3
        
        interpretation:
                [0]
         [b6] = [0]
                [0],
         
                [1]
         [c5] = [0]
                [0],
         
                [1]
         [b5] = [0]
                [0]
        orientation:
                [1]    [0]       
         b5() = [0] >= [0] = b6()
                [0]    [0]       
         
                [1]    [0]       
         c5() = [0] >= [0] = b6()
                [0]    [0]       
        problem:
         
        Qed


2:a3() -> b3()
  a3() -> c3()
  b3() -> b4()
  c3() -> c4()
  b4() -> b5()
  c4() -> c5()
  b5() -> b6()
  c5() -> b6()
  Church Rosser Transformation Processor (kb):
   a3() -> b3()
   a3() -> c3()
   b3() -> b4()
   c3() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> b6()
   critical peaks: joinable
   Matrix Interpretation Processor: dim=3
    
    interpretation:
            [0]
     [b6] = [0]
            [0],
     
            [0]
     [c5] = [0]
            [0],
     
            [0]
     [b5] = [0]
            [0],
     
            [0]
     [c4] = [0]
            [0],
     
            [0]
     [b4] = [0]
            [0],
     
            [1]
     [a3] = [0]
            [0],
     
            [0]
     [c3] = [0]
            [0],
     
            [0]
     [b3] = [0]
            [0]
    orientation:
            [1]    [0]       
     a3() = [0] >= [0] = b3()
            [0]    [0]       
     
            [1]    [0]       
     a3() = [0] >= [0] = c3()
            [0]    [0]       
     
            [0]    [0]       
     b3() = [0] >= [0] = b4()
            [0]    [0]       
     
            [0]    [0]       
     c3() = [0] >= [0] = c4()
            [0]    [0]       
     
            [0]    [0]       
     b4() = [0] >= [0] = b5()
            [0]    [0]       
     
            [0]    [0]       
     c4() = [0] >= [0] = c5()
            [0]    [0]       
     
            [0]    [0]       
     b5() = [0] >= [0] = b6()
            [0]    [0]       
     
            [0]    [0]       
     c5() = [0] >= [0] = b6()
            [0]    [0]       
    problem:
     b3() -> b4()
     c3() -> c4()
     b4() -> b5()
     c4() -> c5()
     b5() -> b6()
     c5() -> b6()
    Matrix Interpretation Processor: dim=3
     
     interpretation:
             [0]
      [b6] = [0]
             [0],
      
             [0]
      [c5] = [0]
             [0],
      
             [0]
      [b5] = [0]
             [0],
      
             [0]
      [c4] = [0]
             [0],
      
             [0]
      [b4] = [0]
             [0],
      
             [1]
      [c3] = [0]
             [0],
      
             [1]
      [b3] = [0]
             [0]
     orientation:
             [1]    [0]       
      b3() = [0] >= [0] = b4()
             [0]    [0]       
      
             [1]    [0]       
      c3() = [0] >= [0] = c4()
             [0]    [0]       
      
             [0]    [0]       
      b4() = [0] >= [0] = b5()
             [0]    [0]       
      
             [0]    [0]       
      c4() = [0] >= [0] = c5()
             [0]    [0]       
      
             [0]    [0]       
      b5() = [0] >= [0] = b6()
             [0]    [0]       
      
             [0]    [0]       
      c5() = [0] >= [0] = b6()
             [0]    [0]       
     problem:
      b4() -> b5()
      c4() -> c5()
      b5() -> b6()
      c5() -> b6()
     Matrix Interpretation Processor: dim=3
      
      interpretation:
              [0]
       [b6] = [0]
              [0],
       
              [0]
       [c5] = [0]
              [0],
       
              [0]
       [b5] = [0]
              [0],
       
              [1]
       [c4] = [0]
              [0],
       
              [1]
       [b4] = [0]
              [0]
      orientation:
              [1]    [0]       
       b4() = [0] >= [0] = b5()
              [0]    [0]       
       
              [1]    [0]       
       c4() = [0] >= [0] = c5()
              [0]    [0]       
       
              [0]    [0]       
       b5() = [0] >= [0] = b6()
              [0]    [0]       
       
              [0]    [0]       
       c5() = [0] >= [0] = b6()
              [0]    [0]       
      problem:
       b5() -> b6()
       c5() -> b6()
      Matrix Interpretation Processor: dim=3
       
       interpretation:
               [0]
        [b6] = [0]
               [0],
        
               [1]
        [c5] = [0]
               [0],
        
               [1]
        [b5] = [0]
               [0]
       orientation:
               [1]    [0]       
        b5() = [0] >= [0] = b6()
               [0]    [0]       
        
               [1]    [0]       
        c5() = [0] >= [0] = b6()
               [0]    [0]       
       problem:
        
       Qed


3:a4() -> b4()
  a4() -> c4()
  b4() -> b5()
  c4() -> c5()
  b5() -> b6()
  c5() -> b6()
  Church Rosser Transformation Processor (kb):
   a4() -> b4()
   a4() -> c4()
   b4() -> b5()
   c4() -> c5()
   b5() -> b6()
   c5() -> b6()
   critical peaks: joinable
   Matrix Interpretation Processor: dim=3
    
    interpretation:
            [0]
     [b6] = [0]
            [0],
     
            [0]
     [c5] = [0]
            [0],
     
            [0]
     [b5] = [0]
            [0],
     
            [1]
     [a4] = [0]
            [0],
     
            [0]
     [c4] = [0]
            [0],
     
            [0]
     [b4] = [0]
            [0]
    orientation:
            [1]    [0]       
     a4() = [0] >= [0] = b4()
            [0]    [0]       
     
            [1]    [0]       
     a4() = [0] >= [0] = c4()
            [0]    [0]       
     
            [0]    [0]       
     b4() = [0] >= [0] = b5()
            [0]    [0]       
     
            [0]    [0]       
     c4() = [0] >= [0] = c5()
            [0]    [0]       
     
            [0]    [0]       
     b5() = [0] >= [0] = b6()
            [0]    [0]       
     
            [0]    [0]       
     c5() = [0] >= [0] = b6()
            [0]    [0]       
    problem:
     b4() -> b5()
     c4() -> c5()
     b5() -> b6()
     c5() -> b6()
    Matrix Interpretation Processor: dim=3
     
     interpretation:
             [0]
      [b6] = [0]
             [0],
      
             [0]
      [c5] = [0]
             [0],
      
             [0]
      [b5] = [0]
             [0],
      
             [1]
      [c4] = [0]
             [0],
      
             [1]
      [b4] = [0]
             [0]
     orientation:
             [1]    [0]       
      b4() = [0] >= [0] = b5()
             [0]    [0]       
      
             [1]    [0]       
      c4() = [0] >= [0] = c5()
             [0]    [0]       
      
             [0]    [0]       
      b5() = [0] >= [0] = b6()
             [0]    [0]       
      
             [0]    [0]       
      c5() = [0] >= [0] = b6()
             [0]    [0]       
     problem:
      b5() -> b6()
      c5() -> b6()
     Matrix Interpretation Processor: dim=3
      
      interpretation:
              [0]
       [b6] = [0]
              [0],
       
              [1]
       [c5] = [0]
              [0],
       
              [1]
       [b5] = [0]
              [0]
      orientation:
              [1]    [0]       
       b5() = [0] >= [0] = b6()
              [0]    [0]       
       
              [1]    [0]       
       c5() = [0] >= [0] = b6()
              [0]    [0]       
      problem:
       
      Qed


4:a5() -> b6()
  Church Rosser Transformation Processor:
   
   strict:
    
   weak:
    
   critical peaks: 0
   Qed