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-sorted)
 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
   [0>1, 0>2, 1>5, 2>4, 3>4, 3>5, 4>7, 5>8, 6>7, 6>8, 7>10, 8>11, 9>10, 9>11, 10>13, 11>12, 12>15,
    13>15, 14>15]
 sort attachment (non-strict)
   a1 : 0
   b1 : 1
   c1 : 2
   b2 : 5
   c2 : 4
   a2 : 3
   b3 : 8
   c3 : 7
   a3 : 6
   b4 : 11
   c4 : 10
   a4 : 9
   b5 : 12
   c5 : 13
   a5 : 14
   b6 : 15
 -----
 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:
    b1() -> b2()
    b2() -> b3()
    b3() -> b4()
    b4() -> b5()
    b5() -> b6()
    c1() -> c2()
    c2() -> c3()
    c3() -> c4()
    c4() -> c5()
    c5() -> b6()
    critical peaks: joinable
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [c2] = 4,
      
      [b6] = 0,
      
      [b1] = 0,
      
      [b2] = 0,
      
      [c4] = 0,
      
      [c3] = 0,
      
      [b5] = 0,
      
      [b4] = 0,
      
      [c5] = 0,
      
      [b3] = 0,
      
      [c1] = 4
     orientation:
      b1() = 0 >= 0 = b2()
      
      b2() = 0 >= 0 = b3()
      
      b3() = 0 >= 0 = b4()
      
      b4() = 0 >= 0 = b5()
      
      b5() = 0 >= 0 = b6()
      
      c1() = 4 >= 4 = c2()
      
      c2() = 4 >= 0 = c3()
      
      c3() = 0 >= 0 = c4()
      
      c4() = 0 >= 0 = c5()
      
      c5() = 0 >= 0 = b6()
     problem:
      b1() -> b2()
      b2() -> b3()
      b3() -> b4()
      b4() -> b5()
      b5() -> b6()
      c1() -> c2()
      c3() -> c4()
      c4() -> c5()
      c5() -> b6()
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [c2] = 0,
       
       [b6] = 0,
       
       [b1] = 0,
       
       [b2] = 0,
       
       [c4] = 4,
       
       [c3] = 4,
       
       [b5] = 0,
       
       [b4] = 0,
       
       [c5] = 0,
       
       [b3] = 0,
       
       [c1] = 0
      orientation:
       b1() = 0 >= 0 = b2()
       
       b2() = 0 >= 0 = b3()
       
       b3() = 0 >= 0 = b4()
       
       b4() = 0 >= 0 = b5()
       
       b5() = 0 >= 0 = b6()
       
       c1() = 0 >= 0 = c2()
       
       c3() = 4 >= 4 = c4()
       
       c4() = 4 >= 0 = c5()
       
       c5() = 0 >= 0 = b6()
      problem:
       b1() -> b2()
       b2() -> b3()
       b3() -> b4()
       b4() -> b5()
       b5() -> b6()
       c1() -> c2()
       c3() -> c4()
       c5() -> b6()
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [c2] = 0,
        
        [b6] = 0,
        
        [b1] = 0,
        
        [b2] = 0,
        
        [c4] = 0,
        
        [c3] = 0,
        
        [b5] = 0,
        
        [b4] = 0,
        
        [c5] = 1,
        
        [b3] = 0,
        
        [c1] = 0
       orientation:
        b1() = 0 >= 0 = b2()
        
        b2() = 0 >= 0 = b3()
        
        b3() = 0 >= 0 = b4()
        
        b4() = 0 >= 0 = b5()
        
        b5() = 0 >= 0 = b6()
        
        c1() = 0 >= 0 = c2()
        
        c3() = 0 >= 0 = c4()
        
        c5() = 1 >= 0 = b6()
       problem:
        b1() -> b2()
        b2() -> b3()
        b3() -> b4()
        b4() -> b5()
        b5() -> b6()
        c1() -> c2()
        c3() -> c4()
       Matrix Interpretation Processor: dim=1
        
        interpretation:
         [c2] = 0,
         
         [b6] = 0,
         
         [b1] = 0,
         
         [b2] = 0,
         
         [c4] = 0,
         
         [c3] = 1,
         
         [b5] = 0,
         
         [b4] = 0,
         
         [b3] = 0,
         
         [c1] = 0
        orientation:
         b1() = 0 >= 0 = b2()
         
         b2() = 0 >= 0 = b3()
         
         b3() = 0 >= 0 = b4()
         
         b4() = 0 >= 0 = b5()
         
         b5() = 0 >= 0 = b6()
         
         c1() = 0 >= 0 = c2()
         
         c3() = 1 >= 0 = c4()
        problem:
         b1() -> b2()
         b2() -> b3()
         b3() -> b4()
         b4() -> b5()
         b5() -> b6()
         c1() -> c2()
        Matrix Interpretation Processor: dim=1
         
         interpretation:
          [c2] = 0,
          
          [b6] = 0,
          
          [b1] = 0,
          
          [b2] = 0,
          
          [b5] = 0,
          
          [b4] = 0,
          
          [b3] = 0,
          
          [c1] = 1
         orientation:
          b1() = 0 >= 0 = b2()
          
          b2() = 0 >= 0 = b3()
          
          b3() = 0 >= 0 = b4()
          
          b4() = 0 >= 0 = b5()
          
          b5() = 0 >= 0 = b6()
          
          c1() = 1 >= 0 = c2()
         problem:
          b1() -> b2()
          b2() -> b3()
          b3() -> b4()
          b4() -> b5()
          b5() -> b6()
         Matrix Interpretation Processor: dim=1
          
          interpretation:
           [b6] = 0,
           
           [b1] = 4,
           
           [b2] = 4,
           
           [b5] = 0,
           
           [b4] = 0,
           
           [b3] = 4
          orientation:
           b1() = 4 >= 4 = b2()
           
           b2() = 4 >= 4 = b3()
           
           b3() = 4 >= 0 = b4()
           
           b4() = 0 >= 0 = b5()
           
           b5() = 0 >= 0 = b6()
          problem:
           b1() -> b2()
           b2() -> b3()
           b4() -> b5()
           b5() -> b6()
          Matrix Interpretation Processor: dim=1
           
           interpretation:
            [b6] = 0,
            
            [b1] = 0,
            
            [b2] = 0,
            
            [b5] = 4,
            
            [b4] = 4,
            
            [b3] = 0
           orientation:
            b1() = 0 >= 0 = b2()
            
            b2() = 0 >= 0 = b3()
            
            b4() = 4 >= 4 = b5()
            
            b5() = 4 >= 0 = b6()
           problem:
            b1() -> b2()
            b2() -> b3()
            b4() -> b5()
           Matrix Interpretation Processor: dim=1
            
            interpretation:
             [b1] = 0,
             
             [b2] = 0,
             
             [b5] = 0,
             
             [b4] = 1,
             
             [b3] = 0
            orientation:
             b1() = 0 >= 0 = b2()
             
             b2() = 0 >= 0 = b3()
             
             b4() = 1 >= 0 = b5()
            problem:
             b1() -> b2()
             b2() -> b3()
            Matrix Interpretation Processor: dim=1
             
             interpretation:
              [b1] = 4,
              
              [b2] = 4,
              
              [b3] = 0
             orientation:
              b1() = 4 >= 4 = b2()
              
              b2() = 4 >= 0 = b3()
             problem:
              b1() -> b2()
             Matrix Interpretation Processor: dim=1
              
              interpretation:
               [b1] = 1,
               
               [b2] = 0
              orientation:
               b1() = 1 >= 0 = b2()
              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:
   b2() -> b3()
   b3() -> b4()
   b4() -> b5()
   b5() -> b6()
   c2() -> c3()
   c3() -> c4()
   c4() -> c5()
   c5() -> b6()
   critical peaks: joinable
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [c2] = 4,
     
     [b6] = 0,
     
     [b2] = 0,
     
     [c4] = 1,
     
     [c3] = 4,
     
     [b5] = 0,
     
     [b4] = 0,
     
     [c5] = 0,
     
     [b3] = 0
    orientation:
     b2() = 0 >= 0 = b3()
     
     b3() = 0 >= 0 = b4()
     
     b4() = 0 >= 0 = b5()
     
     b5() = 0 >= 0 = b6()
     
     c2() = 4 >= 4 = c3()
     
     c3() = 4 >= 1 = c4()
     
     c4() = 1 >= 0 = c5()
     
     c5() = 0 >= 0 = b6()
    problem:
     b2() -> b3()
     b3() -> b4()
     b4() -> b5()
     b5() -> b6()
     c2() -> c3()
     c5() -> b6()
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [c2] = 0,
      
      [b6] = 0,
      
      [b2] = 0,
      
      [c3] = 0,
      
      [b5] = 0,
      
      [b4] = 0,
      
      [c5] = 1,
      
      [b3] = 0
     orientation:
      b2() = 0 >= 0 = b3()
      
      b3() = 0 >= 0 = b4()
      
      b4() = 0 >= 0 = b5()
      
      b5() = 0 >= 0 = b6()
      
      c2() = 0 >= 0 = c3()
      
      c5() = 1 >= 0 = b6()
     problem:
      b2() -> b3()
      b3() -> b4()
      b4() -> b5()
      b5() -> b6()
      c2() -> c3()
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [c2] = 1,
       
       [b6] = 0,
       
       [b2] = 0,
       
       [c3] = 0,
       
       [b5] = 0,
       
       [b4] = 0,
       
       [b3] = 0
      orientation:
       b2() = 0 >= 0 = b3()
       
       b3() = 0 >= 0 = b4()
       
       b4() = 0 >= 0 = b5()
       
       b5() = 0 >= 0 = b6()
       
       c2() = 1 >= 0 = c3()
      problem:
       b2() -> b3()
       b3() -> b4()
       b4() -> b5()
       b5() -> b6()
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [b6] = 0,
        
        [b2] = 4,
        
        [b5] = 0,
        
        [b4] = 4,
        
        [b3] = 4
       orientation:
        b2() = 4 >= 4 = b3()
        
        b3() = 4 >= 4 = b4()
        
        b4() = 4 >= 0 = b5()
        
        b5() = 0 >= 0 = b6()
       problem:
        b2() -> b3()
        b3() -> b4()
        b5() -> b6()
       Matrix Interpretation Processor: dim=1
        
        interpretation:
         [b6] = 0,
         
         [b2] = 0,
         
         [b5] = 1,
         
         [b4] = 0,
         
         [b3] = 0
        orientation:
         b2() = 0 >= 0 = b3()
         
         b3() = 0 >= 0 = b4()
         
         b5() = 1 >= 0 = b6()
        problem:
         b2() -> b3()
         b3() -> b4()
        Matrix Interpretation Processor: dim=1
         
         interpretation:
          [b2] = 4,
          
          [b4] = 0,
          
          [b3] = 4
         orientation:
          b2() = 4 >= 4 = b3()
          
          b3() = 4 >= 0 = b4()
         problem:
          b2() -> b3()
         Matrix Interpretation Processor: dim=1
          
          interpretation:
           [b2] = 1,
           
           [b3] = 0
          orientation:
           b2() = 1 >= 0 = b3()
          problem:
           
          Qed


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


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


4:a5() -> b6()
  Church Rosser Transformation Processor:
   
   critical peaks: joinable
   Qed