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
   [0>6, 1>6, 2>6, 3>6, 4>6, 5>6]
 sort attachment (non-strict)
   a1 : 0
   b1 : 6
   c1 : 6
   b2 : 6
   c2 : 6
   a2 : 1
   b3 : 6
   c3 : 6
   a3 : 2
   b4 : 6
   c4 : 6
   a4 : 3
   b5 : 6
   c5 : 6
   a5 : 4
   b6 : 6
   c6 : 6
   a6 : 5
   b7 : 6
 -----
 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()
   Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
    b1() -> b2()
    b2() -> b3()
    b3() -> b4()
    b4() -> b5()
    b5() -> b6()
    b6() -> b7()
    c1() -> c2()
    c2() -> c3()
    c3() -> c4()
    c4() -> c5()
    c5() -> c6()
    c6() -> b7()
    critical peaks: joinable
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [b7] = 0,
      
      [c6] = 0,
      
      [b6] = 0,
      
      [c5] = 0,
      
      [b5] = 0,
      
      [c4] = 1,
      
      [b4] = 0,
      
      [c3] = 4,
      
      [b3] = 0,
      
      [c2] = 4,
      
      [b2] = 0,
      
      [c1] = 4,
      
      [b1] = 0
     orientation:
      b1() = 0 >= 0 = b2()
      
      b2() = 0 >= 0 = b3()
      
      b3() = 0 >= 0 = b4()
      
      b4() = 0 >= 0 = b5()
      
      b5() = 0 >= 0 = b6()
      
      b6() = 0 >= 0 = b7()
      
      c1() = 4 >= 4 = c2()
      
      c2() = 4 >= 4 = c3()
      
      c3() = 4 >= 1 = c4()
      
      c4() = 1 >= 0 = c5()
      
      c5() = 0 >= 0 = c6()
      
      c6() = 0 >= 0 = b7()
     problem:
      b1() -> b2()
      b2() -> b3()
      b3() -> b4()
      b4() -> b5()
      b5() -> b6()
      b6() -> b7()
      c1() -> c2()
      c2() -> c3()
      c5() -> c6()
      c6() -> b7()
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [b7] = 0,
       
       [c6] = 4,
       
       [b6] = 0,
       
       [c5] = 4,
       
       [b5] = 0,
       
       [b4] = 0,
       
       [c3] = 0,
       
       [b3] = 0,
       
       [c2] = 0,
       
       [b2] = 0,
       
       [c1] = 0,
       
       [b1] = 0
      orientation:
       b1() = 0 >= 0 = b2()
       
       b2() = 0 >= 0 = b3()
       
       b3() = 0 >= 0 = b4()
       
       b4() = 0 >= 0 = b5()
       
       b5() = 0 >= 0 = b6()
       
       b6() = 0 >= 0 = b7()
       
       c1() = 0 >= 0 = c2()
       
       c2() = 0 >= 0 = c3()
       
       c5() = 4 >= 4 = c6()
       
       c6() = 4 >= 0 = b7()
      problem:
       b1() -> b2()
       b2() -> b3()
       b3() -> b4()
       b4() -> b5()
       b5() -> b6()
       b6() -> b7()
       c1() -> c2()
       c2() -> c3()
       c5() -> c6()
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [b7] = 0,
        
        [c6] = 0,
        
        [b6] = 0,
        
        [c5] = 1,
        
        [b5] = 0,
        
        [b4] = 0,
        
        [c3] = 0,
        
        [b3] = 0,
        
        [c2] = 0,
        
        [b2] = 0,
        
        [c1] = 0,
        
        [b1] = 0
       orientation:
        b1() = 0 >= 0 = b2()
        
        b2() = 0 >= 0 = b3()
        
        b3() = 0 >= 0 = b4()
        
        b4() = 0 >= 0 = b5()
        
        b5() = 0 >= 0 = b6()
        
        b6() = 0 >= 0 = b7()
        
        c1() = 0 >= 0 = c2()
        
        c2() = 0 >= 0 = c3()
        
        c5() = 1 >= 0 = c6()
       problem:
        b1() -> b2()
        b2() -> b3()
        b3() -> b4()
        b4() -> b5()
        b5() -> b6()
        b6() -> b7()
        c1() -> c2()
        c2() -> c3()
       Matrix Interpretation Processor: dim=1
        
        interpretation:
         [b7] = 0,
         
         [b6] = 0,
         
         [b5] = 0,
         
         [b4] = 0,
         
         [c3] = 0,
         
         [b3] = 0,
         
         [c2] = 4,
         
         [b2] = 0,
         
         [c1] = 4,
         
         [b1] = 0
        orientation:
         b1() = 0 >= 0 = b2()
         
         b2() = 0 >= 0 = b3()
         
         b3() = 0 >= 0 = b4()
         
         b4() = 0 >= 0 = b5()
         
         b5() = 0 >= 0 = b6()
         
         b6() = 0 >= 0 = b7()
         
         c1() = 4 >= 4 = c2()
         
         c2() = 4 >= 0 = c3()
        problem:
         b1() -> b2()
         b2() -> b3()
         b3() -> b4()
         b4() -> b5()
         b5() -> b6()
         b6() -> b7()
         c1() -> c2()
        Matrix Interpretation Processor: dim=1
         
         interpretation:
          [b7] = 0,
          
          [b6] = 0,
          
          [b5] = 0,
          
          [b4] = 0,
          
          [b3] = 0,
          
          [c2] = 0,
          
          [b2] = 0,
          
          [c1] = 1,
          
          [b1] = 0
         orientation:
          b1() = 0 >= 0 = b2()
          
          b2() = 0 >= 0 = b3()
          
          b3() = 0 >= 0 = b4()
          
          b4() = 0 >= 0 = b5()
          
          b5() = 0 >= 0 = b6()
          
          b6() = 0 >= 0 = b7()
          
          c1() = 1 >= 0 = c2()
         problem:
          b1() -> b2()
          b2() -> b3()
          b3() -> b4()
          b4() -> b5()
          b5() -> b6()
          b6() -> b7()
         Matrix Interpretation Processor: dim=1
          
          interpretation:
           [b7] = 0,
           
           [b6] = 0,
           
           [b5] = 4,
           
           [b4] = 4,
           
           [b3] = 4,
           
           [b2] = 4,
           
           [b1] = 4
          orientation:
           b1() = 4 >= 4 = b2()
           
           b2() = 4 >= 4 = b3()
           
           b3() = 4 >= 4 = b4()
           
           b4() = 4 >= 4 = b5()
           
           b5() = 4 >= 0 = b6()
           
           b6() = 0 >= 0 = b7()
          problem:
           b1() -> b2()
           b2() -> b3()
           b3() -> b4()
           b4() -> b5()
           b6() -> b7()
          Matrix Interpretation Processor: dim=1
           
           interpretation:
            [b7] = 0,
            
            [b6] = 1,
            
            [b5] = 0,
            
            [b4] = 0,
            
            [b3] = 0,
            
            [b2] = 0,
            
            [b1] = 0
           orientation:
            b1() = 0 >= 0 = b2()
            
            b2() = 0 >= 0 = b3()
            
            b3() = 0 >= 0 = b4()
            
            b4() = 0 >= 0 = b5()
            
            b6() = 1 >= 0 = b7()
           problem:
            b1() -> b2()
            b2() -> b3()
            b3() -> b4()
            b4() -> b5()
           Matrix Interpretation Processor: dim=1
            
            interpretation:
             [b5] = 0,
             
             [b4] = 0,
             
             [b3] = 4,
             
             [b2] = 4,
             
             [b1] = 4
            orientation:
             b1() = 4 >= 4 = b2()
             
             b2() = 4 >= 4 = b3()
             
             b3() = 4 >= 0 = b4()
             
             b4() = 0 >= 0 = b5()
            problem:
             b1() -> b2()
             b2() -> b3()
             b4() -> b5()
            Matrix Interpretation Processor: dim=1
             
             interpretation:
              [b5] = 0,
              
              [b4] = 1,
              
              [b3] = 0,
              
              [b2] = 0,
              
              [b1] = 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:
               [b3] = 0,
               
               [b2] = 4,
               
               [b1] = 4
              orientation:
               b1() = 4 >= 4 = b2()
               
               b2() = 4 >= 0 = b3()
              problem:
               b1() -> b2()
              Matrix Interpretation Processor: dim=1
               
               interpretation:
                [b2] = 0,
                
                [b1] = 1
               orientation:
                b1() = 1 >= 0 = b2()
               problem:
                
               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()
   Ground Confluence Processor:
    confluent by decision procedure.


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()
  Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
   b3() -> b4()
   b4() -> b5()
   b5() -> b6()
   b6() -> b7()
   c3() -> c4()
   c4() -> c5()
   c5() -> c6()
   c6() -> b7()
   b1() -> b2()
   b2() -> b3()
   c1() -> c2()
   c2() -> c3()
   critical peaks: joinable
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [b7] = 0,
     
     [c6] = 0,
     
     [b6] = 0,
     
     [c5] = 0,
     
     [b5] = 0,
     
     [c4] = 0,
     
     [b4] = 0,
     
     [c3] = 0,
     
     [b3] = 0,
     
     [c2] = 4,
     
     [b2] = 0,
     
     [c1] = 4,
     
     [b1] = 0
    orientation:
     b3() = 0 >= 0 = b4()
     
     b4() = 0 >= 0 = b5()
     
     b5() = 0 >= 0 = b6()
     
     b6() = 0 >= 0 = b7()
     
     c3() = 0 >= 0 = c4()
     
     c4() = 0 >= 0 = c5()
     
     c5() = 0 >= 0 = c6()
     
     c6() = 0 >= 0 = b7()
     
     b1() = 0 >= 0 = b2()
     
     b2() = 0 >= 0 = b3()
     
     c1() = 4 >= 4 = c2()
     
     c2() = 4 >= 0 = c3()
    problem:
     b3() -> b4()
     b4() -> b5()
     b5() -> b6()
     b6() -> b7()
     c3() -> c4()
     c4() -> c5()
     c5() -> c6()
     c6() -> b7()
     b1() -> b2()
     b2() -> b3()
     c1() -> c2()
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [b7] = 0,
      
      [c6] = 0,
      
      [b6] = 0,
      
      [c5] = 0,
      
      [b5] = 0,
      
      [c4] = 0,
      
      [b4] = 0,
      
      [c3] = 0,
      
      [b3] = 0,
      
      [c2] = 0,
      
      [b2] = 0,
      
      [c1] = 1,
      
      [b1] = 0
     orientation:
      b3() = 0 >= 0 = b4()
      
      b4() = 0 >= 0 = b5()
      
      b5() = 0 >= 0 = b6()
      
      b6() = 0 >= 0 = b7()
      
      c3() = 0 >= 0 = c4()
      
      c4() = 0 >= 0 = c5()
      
      c5() = 0 >= 0 = c6()
      
      c6() = 0 >= 0 = b7()
      
      b1() = 0 >= 0 = b2()
      
      b2() = 0 >= 0 = b3()
      
      c1() = 1 >= 0 = c2()
     problem:
      b3() -> b4()
      b4() -> b5()
      b5() -> b6()
      b6() -> b7()
      c3() -> c4()
      c4() -> c5()
      c5() -> c6()
      c6() -> b7()
      b1() -> b2()
      b2() -> b3()
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [b7] = 0,
       
       [c6] = 0,
       
       [b6] = 0,
       
       [c5] = 0,
       
       [b5] = 0,
       
       [c4] = 0,
       
       [b4] = 0,
       
       [c3] = 0,
       
       [b3] = 0,
       
       [b2] = 4,
       
       [b1] = 4
      orientation:
       b3() = 0 >= 0 = b4()
       
       b4() = 0 >= 0 = b5()
       
       b5() = 0 >= 0 = b6()
       
       b6() = 0 >= 0 = b7()
       
       c3() = 0 >= 0 = c4()
       
       c4() = 0 >= 0 = c5()
       
       c5() = 0 >= 0 = c6()
       
       c6() = 0 >= 0 = b7()
       
       b1() = 4 >= 4 = b2()
       
       b2() = 4 >= 0 = b3()
      problem:
       b3() -> b4()
       b4() -> b5()
       b5() -> b6()
       b6() -> b7()
       c3() -> c4()
       c4() -> c5()
       c5() -> c6()
       c6() -> b7()
       b1() -> b2()
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [b7] = 0,
        
        [c6] = 0,
        
        [b6] = 0,
        
        [c5] = 0,
        
        [b5] = 0,
        
        [c4] = 0,
        
        [b4] = 0,
        
        [c3] = 0,
        
        [b3] = 0,
        
        [b2] = 0,
        
        [b1] = 1
       orientation:
        b3() = 0 >= 0 = b4()
        
        b4() = 0 >= 0 = b5()
        
        b5() = 0 >= 0 = b6()
        
        b6() = 0 >= 0 = b7()
        
        c3() = 0 >= 0 = c4()
        
        c4() = 0 >= 0 = c5()
        
        c5() = 0 >= 0 = c6()
        
        c6() = 0 >= 0 = b7()
        
        b1() = 1 >= 0 = b2()
       problem:
        b3() -> b4()
        b4() -> b5()
        b5() -> b6()
        b6() -> b7()
        c3() -> c4()
        c4() -> c5()
        c5() -> c6()
        c6() -> b7()
       Matrix Interpretation Processor: dim=1
        
        interpretation:
         [b7] = 0,
         
         [c6] = 0,
         
         [b6] = 0,
         
         [c5] = 1,
         
         [b5] = 0,
         
         [c4] = 4,
         
         [b4] = 0,
         
         [c3] = 4,
         
         [b3] = 0
        orientation:
         b3() = 0 >= 0 = b4()
         
         b4() = 0 >= 0 = b5()
         
         b5() = 0 >= 0 = b6()
         
         b6() = 0 >= 0 = b7()
         
         c3() = 4 >= 4 = c4()
         
         c4() = 4 >= 1 = c5()
         
         c5() = 1 >= 0 = c6()
         
         c6() = 0 >= 0 = b7()
        problem:
         b3() -> b4()
         b4() -> b5()
         b5() -> b6()
         b6() -> b7()
         c3() -> c4()
         c6() -> b7()
        Matrix Interpretation Processor: dim=1
         
         interpretation:
          [b7] = 0,
          
          [c6] = 1,
          
          [b6] = 0,
          
          [b5] = 0,
          
          [c4] = 0,
          
          [b4] = 0,
          
          [c3] = 0,
          
          [b3] = 0
         orientation:
          b3() = 0 >= 0 = b4()
          
          b4() = 0 >= 0 = b5()
          
          b5() = 0 >= 0 = b6()
          
          b6() = 0 >= 0 = b7()
          
          c3() = 0 >= 0 = c4()
          
          c6() = 1 >= 0 = b7()
         problem:
          b3() -> b4()
          b4() -> b5()
          b5() -> b6()
          b6() -> b7()
          c3() -> c4()
         Matrix Interpretation Processor: dim=1
          
          interpretation:
           [b7] = 0,
           
           [b6] = 0,
           
           [b5] = 0,
           
           [c4] = 0,
           
           [b4] = 0,
           
           [c3] = 1,
           
           [b3] = 0
          orientation:
           b3() = 0 >= 0 = b4()
           
           b4() = 0 >= 0 = b5()
           
           b5() = 0 >= 0 = b6()
           
           b6() = 0 >= 0 = b7()
           
           c3() = 1 >= 0 = c4()
          problem:
           b3() -> b4()
           b4() -> b5()
           b5() -> b6()
           b6() -> b7()
          Matrix Interpretation Processor: dim=1
           
           interpretation:
            [b7] = 0,
            
            [b6] = 0,
            
            [b5] = 4,
            
            [b4] = 4,
            
            [b3] = 4
           orientation:
            b3() = 4 >= 4 = b4()
            
            b4() = 4 >= 4 = b5()
            
            b5() = 4 >= 0 = b6()
            
            b6() = 0 >= 0 = b7()
           problem:
            b3() -> b4()
            b4() -> b5()
            b6() -> b7()
           Matrix Interpretation Processor: dim=1
            
            interpretation:
             [b7] = 0,
             
             [b6] = 1,
             
             [b5] = 0,
             
             [b4] = 0,
             
             [b3] = 0
            orientation:
             b3() = 0 >= 0 = b4()
             
             b4() = 0 >= 0 = b5()
             
             b6() = 1 >= 0 = b7()
            problem:
             b3() -> b4()
             b4() -> b5()
            Matrix Interpretation Processor: dim=1
             
             interpretation:
              [b5] = 0,
              
              [b4] = 4,
              
              [b3] = 4
             orientation:
              b3() = 4 >= 4 = b4()
              
              b4() = 4 >= 0 = b5()
             problem:
              b3() -> b4()
             Matrix Interpretation Processor: dim=1
              
              interpretation:
               [b4] = 0,
               
               [b3] = 1
              orientation:
               b3() = 1 >= 0 = b4()
              problem:
               
              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()
  Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
   b4() -> b5()
   b5() -> b6()
   b6() -> b7()
   c4() -> c5()
   c5() -> c6()
   c6() -> b7()
   b1() -> b2()
   b2() -> b3()
   b3() -> b4()
   c1() -> c2()
   c2() -> c3()
   c3() -> c4()
   critical peaks: joinable
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [b7] = 0,
     
     [c6] = 0,
     
     [b6] = 0,
     
     [c5] = 0,
     
     [b5] = 0,
     
     [c4] = 0,
     
     [b4] = 0,
     
     [c3] = 0,
     
     [b3] = 0,
     
     [c2] = 4,
     
     [b2] = 0,
     
     [c1] = 4,
     
     [b1] = 0
    orientation:
     b4() = 0 >= 0 = b5()
     
     b5() = 0 >= 0 = b6()
     
     b6() = 0 >= 0 = b7()
     
     c4() = 0 >= 0 = c5()
     
     c5() = 0 >= 0 = c6()
     
     c6() = 0 >= 0 = b7()
     
     b1() = 0 >= 0 = b2()
     
     b2() = 0 >= 0 = b3()
     
     b3() = 0 >= 0 = b4()
     
     c1() = 4 >= 4 = c2()
     
     c2() = 4 >= 0 = c3()
     
     c3() = 0 >= 0 = c4()
    problem:
     b4() -> b5()
     b5() -> b6()
     b6() -> b7()
     c4() -> c5()
     c5() -> c6()
     c6() -> b7()
     b1() -> b2()
     b2() -> b3()
     b3() -> b4()
     c1() -> c2()
     c3() -> c4()
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [b7] = 0,
      
      [c6] = 0,
      
      [b6] = 0,
      
      [c5] = 0,
      
      [b5] = 0,
      
      [c4] = 0,
      
      [b4] = 0,
      
      [c3] = 1,
      
      [b3] = 0,
      
      [c2] = 0,
      
      [b2] = 0,
      
      [c1] = 0,
      
      [b1] = 0
     orientation:
      b4() = 0 >= 0 = b5()
      
      b5() = 0 >= 0 = b6()
      
      b6() = 0 >= 0 = b7()
      
      c4() = 0 >= 0 = c5()
      
      c5() = 0 >= 0 = c6()
      
      c6() = 0 >= 0 = b7()
      
      b1() = 0 >= 0 = b2()
      
      b2() = 0 >= 0 = b3()
      
      b3() = 0 >= 0 = b4()
      
      c1() = 0 >= 0 = c2()
      
      c3() = 1 >= 0 = c4()
     problem:
      b4() -> b5()
      b5() -> b6()
      b6() -> b7()
      c4() -> c5()
      c5() -> c6()
      c6() -> b7()
      b1() -> b2()
      b2() -> b3()
      b3() -> b4()
      c1() -> c2()
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [b7] = 0,
       
       [c6] = 0,
       
       [b6] = 0,
       
       [c5] = 0,
       
       [b5] = 0,
       
       [c4] = 0,
       
       [b4] = 0,
       
       [b3] = 0,
       
       [c2] = 0,
       
       [b2] = 0,
       
       [c1] = 1,
       
       [b1] = 0
      orientation:
       b4() = 0 >= 0 = b5()
       
       b5() = 0 >= 0 = b6()
       
       b6() = 0 >= 0 = b7()
       
       c4() = 0 >= 0 = c5()
       
       c5() = 0 >= 0 = c6()
       
       c6() = 0 >= 0 = b7()
       
       b1() = 0 >= 0 = b2()
       
       b2() = 0 >= 0 = b3()
       
       b3() = 0 >= 0 = b4()
       
       c1() = 1 >= 0 = c2()
      problem:
       b4() -> b5()
       b5() -> b6()
       b6() -> b7()
       c4() -> c5()
       c5() -> c6()
       c6() -> b7()
       b1() -> b2()
       b2() -> b3()
       b3() -> b4()
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [b7] = 0,
        
        [c6] = 0,
        
        [b6] = 0,
        
        [c5] = 0,
        
        [b5] = 0,
        
        [c4] = 0,
        
        [b4] = 0,
        
        [b3] = 0,
        
        [b2] = 4,
        
        [b1] = 4
       orientation:
        b4() = 0 >= 0 = b5()
        
        b5() = 0 >= 0 = b6()
        
        b6() = 0 >= 0 = b7()
        
        c4() = 0 >= 0 = c5()
        
        c5() = 0 >= 0 = c6()
        
        c6() = 0 >= 0 = b7()
        
        b1() = 4 >= 4 = b2()
        
        b2() = 4 >= 0 = b3()
        
        b3() = 0 >= 0 = b4()
       problem:
        b4() -> b5()
        b5() -> b6()
        b6() -> b7()
        c4() -> c5()
        c5() -> c6()
        c6() -> b7()
        b1() -> b2()
        b3() -> b4()
       Matrix Interpretation Processor: dim=1
        
        interpretation:
         [b7] = 0,
         
         [c6] = 0,
         
         [b6] = 0,
         
         [c5] = 0,
         
         [b5] = 0,
         
         [c4] = 0,
         
         [b4] = 0,
         
         [b3] = 1,
         
         [b2] = 0,
         
         [b1] = 0
        orientation:
         b4() = 0 >= 0 = b5()
         
         b5() = 0 >= 0 = b6()
         
         b6() = 0 >= 0 = b7()
         
         c4() = 0 >= 0 = c5()
         
         c5() = 0 >= 0 = c6()
         
         c6() = 0 >= 0 = b7()
         
         b1() = 0 >= 0 = b2()
         
         b3() = 1 >= 0 = b4()
        problem:
         b4() -> b5()
         b5() -> b6()
         b6() -> b7()
         c4() -> c5()
         c5() -> c6()
         c6() -> b7()
         b1() -> b2()
        Matrix Interpretation Processor: dim=1
         
         interpretation:
          [b7] = 0,
          
          [c6] = 0,
          
          [b6] = 0,
          
          [c5] = 0,
          
          [b5] = 0,
          
          [c4] = 0,
          
          [b4] = 0,
          
          [b2] = 0,
          
          [b1] = 1
         orientation:
          b4() = 0 >= 0 = b5()
          
          b5() = 0 >= 0 = b6()
          
          b6() = 0 >= 0 = b7()
          
          c4() = 0 >= 0 = c5()
          
          c5() = 0 >= 0 = c6()
          
          c6() = 0 >= 0 = b7()
          
          b1() = 1 >= 0 = b2()
         problem:
          b4() -> b5()
          b5() -> b6()
          b6() -> b7()
          c4() -> c5()
          c5() -> c6()
          c6() -> b7()
         Matrix Interpretation Processor: dim=1
          
          interpretation:
           [b7] = 0,
           
           [c6] = 0,
           
           [b6] = 0,
           
           [c5] = 4,
           
           [b5] = 0,
           
           [c4] = 4,
           
           [b4] = 0
          orientation:
           b4() = 0 >= 0 = b5()
           
           b5() = 0 >= 0 = b6()
           
           b6() = 0 >= 0 = b7()
           
           c4() = 4 >= 4 = c5()
           
           c5() = 4 >= 0 = c6()
           
           c6() = 0 >= 0 = b7()
          problem:
           b4() -> b5()
           b5() -> b6()
           b6() -> b7()
           c4() -> c5()
           c6() -> b7()
          Matrix Interpretation Processor: dim=1
           
           interpretation:
            [b7] = 0,
            
            [c6] = 1,
            
            [b6] = 0,
            
            [c5] = 0,
            
            [b5] = 0,
            
            [c4] = 0,
            
            [b4] = 0
           orientation:
            b4() = 0 >= 0 = b5()
            
            b5() = 0 >= 0 = b6()
            
            b6() = 0 >= 0 = b7()
            
            c4() = 0 >= 0 = c5()
            
            c6() = 1 >= 0 = b7()
           problem:
            b4() -> b5()
            b5() -> b6()
            b6() -> b7()
            c4() -> c5()
           Matrix Interpretation Processor: dim=1
            
            interpretation:
             [b7] = 0,
             
             [b6] = 0,
             
             [c5] = 0,
             
             [b5] = 0,
             
             [c4] = 1,
             
             [b4] = 0
            orientation:
             b4() = 0 >= 0 = b5()
             
             b5() = 0 >= 0 = b6()
             
             b6() = 0 >= 0 = b7()
             
             c4() = 1 >= 0 = c5()
            problem:
             b4() -> b5()
             b5() -> b6()
             b6() -> b7()
            Matrix Interpretation Processor: dim=1
             
             interpretation:
              [b7] = 0,
              
              [b6] = 0,
              
              [b5] = 4,
              
              [b4] = 4
             orientation:
              b4() = 4 >= 4 = b5()
              
              b5() = 4 >= 0 = b6()
              
              b6() = 0 >= 0 = b7()
             problem:
              b4() -> b5()
              b6() -> b7()
             Matrix Interpretation Processor: dim=1
              
              interpretation:
               [b7] = 0,
               
               [b6] = 1,
               
               [b5] = 0,
               
               [b4] = 0
              orientation:
               b4() = 0 >= 0 = b5()
               
               b6() = 1 >= 0 = b7()
              problem:
               b4() -> b5()
              Matrix Interpretation Processor: dim=1
               
               interpretation:
                [b5] = 0,
                
                [b4] = 1
               orientation:
                b4() = 1 >= 0 = b5()
               problem:
                
               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()
  Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
   b5() -> b6()
   b6() -> b7()
   c5() -> c6()
   c6() -> b7()
   b1() -> b2()
   b2() -> b3()
   b3() -> b4()
   b4() -> b5()
   c1() -> c2()
   c2() -> c3()
   c3() -> c4()
   c4() -> c5()
   critical peaks: joinable
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [b7] = 0,
     
     [c6] = 0,
     
     [b6] = 0,
     
     [c5] = 0,
     
     [b5] = 0,
     
     [c4] = 0,
     
     [b4] = 0,
     
     [c3] = 0,
     
     [b3] = 0,
     
     [c2] = 4,
     
     [b2] = 0,
     
     [c1] = 4,
     
     [b1] = 0
    orientation:
     b5() = 0 >= 0 = b6()
     
     b6() = 0 >= 0 = b7()
     
     c5() = 0 >= 0 = c6()
     
     c6() = 0 >= 0 = b7()
     
     b1() = 0 >= 0 = b2()
     
     b2() = 0 >= 0 = b3()
     
     b3() = 0 >= 0 = b4()
     
     b4() = 0 >= 0 = b5()
     
     c1() = 4 >= 4 = c2()
     
     c2() = 4 >= 0 = c3()
     
     c3() = 0 >= 0 = c4()
     
     c4() = 0 >= 0 = c5()
    problem:
     b5() -> b6()
     b6() -> b7()
     c5() -> c6()
     c6() -> b7()
     b1() -> b2()
     b2() -> b3()
     b3() -> b4()
     b4() -> b5()
     c1() -> c2()
     c3() -> c4()
     c4() -> c5()
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [b7] = 0,
      
      [c6] = 0,
      
      [b6] = 0,
      
      [c5] = 0,
      
      [b5] = 0,
      
      [c4] = 4,
      
      [b4] = 0,
      
      [c3] = 4,
      
      [b3] = 0,
      
      [c2] = 0,
      
      [b2] = 0,
      
      [c1] = 0,
      
      [b1] = 0
     orientation:
      b5() = 0 >= 0 = b6()
      
      b6() = 0 >= 0 = b7()
      
      c5() = 0 >= 0 = c6()
      
      c6() = 0 >= 0 = b7()
      
      b1() = 0 >= 0 = b2()
      
      b2() = 0 >= 0 = b3()
      
      b3() = 0 >= 0 = b4()
      
      b4() = 0 >= 0 = b5()
      
      c1() = 0 >= 0 = c2()
      
      c3() = 4 >= 4 = c4()
      
      c4() = 4 >= 0 = c5()
     problem:
      b5() -> b6()
      b6() -> b7()
      c5() -> c6()
      c6() -> b7()
      b1() -> b2()
      b2() -> b3()
      b3() -> b4()
      b4() -> b5()
      c1() -> c2()
      c3() -> c4()
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [b7] = 0,
       
       [c6] = 0,
       
       [b6] = 0,
       
       [c5] = 0,
       
       [b5] = 0,
       
       [c4] = 0,
       
       [b4] = 0,
       
       [c3] = 1,
       
       [b3] = 0,
       
       [c2] = 0,
       
       [b2] = 0,
       
       [c1] = 0,
       
       [b1] = 0
      orientation:
       b5() = 0 >= 0 = b6()
       
       b6() = 0 >= 0 = b7()
       
       c5() = 0 >= 0 = c6()
       
       c6() = 0 >= 0 = b7()
       
       b1() = 0 >= 0 = b2()
       
       b2() = 0 >= 0 = b3()
       
       b3() = 0 >= 0 = b4()
       
       b4() = 0 >= 0 = b5()
       
       c1() = 0 >= 0 = c2()
       
       c3() = 1 >= 0 = c4()
      problem:
       b5() -> b6()
       b6() -> b7()
       c5() -> c6()
       c6() -> b7()
       b1() -> b2()
       b2() -> b3()
       b3() -> b4()
       b4() -> b5()
       c1() -> c2()
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [b7] = 0,
        
        [c6] = 0,
        
        [b6] = 0,
        
        [c5] = 0,
        
        [b5] = 0,
        
        [b4] = 0,
        
        [b3] = 0,
        
        [c2] = 0,
        
        [b2] = 0,
        
        [c1] = 1,
        
        [b1] = 0
       orientation:
        b5() = 0 >= 0 = b6()
        
        b6() = 0 >= 0 = b7()
        
        c5() = 0 >= 0 = c6()
        
        c6() = 0 >= 0 = b7()
        
        b1() = 0 >= 0 = b2()
        
        b2() = 0 >= 0 = b3()
        
        b3() = 0 >= 0 = b4()
        
        b4() = 0 >= 0 = b5()
        
        c1() = 1 >= 0 = c2()
       problem:
        b5() -> b6()
        b6() -> b7()
        c5() -> c6()
        c6() -> b7()
        b1() -> b2()
        b2() -> b3()
        b3() -> b4()
        b4() -> b5()
       Matrix Interpretation Processor: dim=1
        
        interpretation:
         [b7] = 0,
         
         [c6] = 0,
         
         [b6] = 0,
         
         [c5] = 0,
         
         [b5] = 0,
         
         [b4] = 0,
         
         [b3] = 1,
         
         [b2] = 4,
         
         [b1] = 4
        orientation:
         b5() = 0 >= 0 = b6()
         
         b6() = 0 >= 0 = b7()
         
         c5() = 0 >= 0 = c6()
         
         c6() = 0 >= 0 = b7()
         
         b1() = 4 >= 4 = b2()
         
         b2() = 4 >= 1 = b3()
         
         b3() = 1 >= 0 = b4()
         
         b4() = 0 >= 0 = b5()
        problem:
         b5() -> b6()
         b6() -> b7()
         c5() -> c6()
         c6() -> b7()
         b1() -> b2()
         b4() -> b5()
        Matrix Interpretation Processor: dim=1
         
         interpretation:
          [b7] = 0,
          
          [c6] = 0,
          
          [b6] = 0,
          
          [c5] = 0,
          
          [b5] = 0,
          
          [b4] = 1,
          
          [b2] = 0,
          
          [b1] = 0
         orientation:
          b5() = 0 >= 0 = b6()
          
          b6() = 0 >= 0 = b7()
          
          c5() = 0 >= 0 = c6()
          
          c6() = 0 >= 0 = b7()
          
          b1() = 0 >= 0 = b2()
          
          b4() = 1 >= 0 = b5()
         problem:
          b5() -> b6()
          b6() -> b7()
          c5() -> c6()
          c6() -> b7()
          b1() -> b2()
         Matrix Interpretation Processor: dim=1
          
          interpretation:
           [b7] = 0,
           
           [c6] = 0,
           
           [b6] = 0,
           
           [c5] = 0,
           
           [b5] = 0,
           
           [b2] = 0,
           
           [b1] = 1
          orientation:
           b5() = 0 >= 0 = b6()
           
           b6() = 0 >= 0 = b7()
           
           c5() = 0 >= 0 = c6()
           
           c6() = 0 >= 0 = b7()
           
           b1() = 1 >= 0 = b2()
          problem:
           b5() -> b6()
           b6() -> b7()
           c5() -> c6()
           c6() -> b7()
          Matrix Interpretation Processor: dim=1
           
           interpretation:
            [b7] = 0,
            
            [c6] = 4,
            
            [b6] = 0,
            
            [c5] = 4,
            
            [b5] = 0
           orientation:
            b5() = 0 >= 0 = b6()
            
            b6() = 0 >= 0 = b7()
            
            c5() = 4 >= 4 = c6()
            
            c6() = 4 >= 0 = b7()
           problem:
            b5() -> b6()
            b6() -> b7()
            c5() -> c6()
           Matrix Interpretation Processor: dim=1
            
            interpretation:
             [b7] = 0,
             
             [c6] = 0,
             
             [b6] = 0,
             
             [c5] = 1,
             
             [b5] = 0
            orientation:
             b5() = 0 >= 0 = b6()
             
             b6() = 0 >= 0 = b7()
             
             c5() = 1 >= 0 = c6()
            problem:
             b5() -> b6()
             b6() -> b7()
            Matrix Interpretation Processor: dim=1
             
             interpretation:
              [b7] = 0,
              
              [b6] = 4,
              
              [b5] = 4
             orientation:
              b5() = 4 >= 4 = b6()
              
              b6() = 4 >= 0 = b7()
             problem:
              b5() -> b6()
             Matrix Interpretation Processor: dim=1
              
              interpretation:
               [b6] = 0,
               
               [b5] = 1
              orientation:
               b5() = 1 >= 0 = b6()
              problem:
               
              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()
  Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
   b6() -> b7()
   c6() -> b7()
   b1() -> b2()
   b2() -> b3()
   b3() -> b4()
   b4() -> b5()
   b5() -> b6()
   c1() -> c2()
   c2() -> c3()
   c3() -> c4()
   c4() -> c5()
   c5() -> c6()
   critical peaks: joinable
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [b7] = 0,
     
     [c6] = 0,
     
     [b6] = 0,
     
     [c5] = 0,
     
     [b5] = 0,
     
     [c4] = 0,
     
     [b4] = 0,
     
     [c3] = 4,
     
     [b3] = 0,
     
     [c2] = 4,
     
     [b2] = 0,
     
     [c1] = 4,
     
     [b1] = 0
    orientation:
     b6() = 0 >= 0 = b7()
     
     c6() = 0 >= 0 = b7()
     
     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 >= 4 = c3()
     
     c3() = 4 >= 0 = c4()
     
     c4() = 0 >= 0 = c5()
     
     c5() = 0 >= 0 = c6()
    problem:
     b6() -> b7()
     c6() -> b7()
     b1() -> b2()
     b2() -> b3()
     b3() -> b4()
     b4() -> b5()
     b5() -> b6()
     c1() -> c2()
     c2() -> c3()
     c4() -> c5()
     c5() -> c6()
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [b7] = 0,
      
      [c6] = 0,
      
      [b6] = 0,
      
      [c5] = 4,
      
      [b5] = 0,
      
      [c4] = 4,
      
      [b4] = 0,
      
      [c3] = 0,
      
      [b3] = 0,
      
      [c2] = 0,
      
      [b2] = 0,
      
      [c1] = 0,
      
      [b1] = 0
     orientation:
      b6() = 0 >= 0 = b7()
      
      c6() = 0 >= 0 = b7()
      
      b1() = 0 >= 0 = b2()
      
      b2() = 0 >= 0 = b3()
      
      b3() = 0 >= 0 = b4()
      
      b4() = 0 >= 0 = b5()
      
      b5() = 0 >= 0 = b6()
      
      c1() = 0 >= 0 = c2()
      
      c2() = 0 >= 0 = c3()
      
      c4() = 4 >= 4 = c5()
      
      c5() = 4 >= 0 = c6()
     problem:
      b6() -> b7()
      c6() -> b7()
      b1() -> b2()
      b2() -> b3()
      b3() -> b4()
      b4() -> b5()
      b5() -> b6()
      c1() -> c2()
      c2() -> c3()
      c4() -> c5()
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [b7] = 0,
       
       [c6] = 0,
       
       [b6] = 0,
       
       [c5] = 0,
       
       [b5] = 0,
       
       [c4] = 1,
       
       [b4] = 0,
       
       [c3] = 0,
       
       [b3] = 0,
       
       [c2] = 0,
       
       [b2] = 0,
       
       [c1] = 0,
       
       [b1] = 0
      orientation:
       b6() = 0 >= 0 = b7()
       
       c6() = 0 >= 0 = b7()
       
       b1() = 0 >= 0 = b2()
       
       b2() = 0 >= 0 = b3()
       
       b3() = 0 >= 0 = b4()
       
       b4() = 0 >= 0 = b5()
       
       b5() = 0 >= 0 = b6()
       
       c1() = 0 >= 0 = c2()
       
       c2() = 0 >= 0 = c3()
       
       c4() = 1 >= 0 = c5()
      problem:
       b6() -> b7()
       c6() -> b7()
       b1() -> b2()
       b2() -> b3()
       b3() -> b4()
       b4() -> b5()
       b5() -> b6()
       c1() -> c2()
       c2() -> c3()
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [b7] = 0,
        
        [c6] = 0,
        
        [b6] = 0,
        
        [b5] = 0,
        
        [b4] = 0,
        
        [c3] = 0,
        
        [b3] = 0,
        
        [c2] = 4,
        
        [b2] = 0,
        
        [c1] = 4,
        
        [b1] = 0
       orientation:
        b6() = 0 >= 0 = b7()
        
        c6() = 0 >= 0 = b7()
        
        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()
       problem:
        b6() -> b7()
        c6() -> b7()
        b1() -> b2()
        b2() -> b3()
        b3() -> b4()
        b4() -> b5()
        b5() -> b6()
        c1() -> c2()
       Matrix Interpretation Processor: dim=1
        
        interpretation:
         [b7] = 0,
         
         [c6] = 0,
         
         [b6] = 0,
         
         [b5] = 0,
         
         [b4] = 0,
         
         [b3] = 0,
         
         [c2] = 0,
         
         [b2] = 0,
         
         [c1] = 1,
         
         [b1] = 0
        orientation:
         b6() = 0 >= 0 = b7()
         
         c6() = 0 >= 0 = b7()
         
         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:
         b6() -> b7()
         c6() -> b7()
         b1() -> b2()
         b2() -> b3()
         b3() -> b4()
         b4() -> b5()
         b5() -> b6()
        Matrix Interpretation Processor: dim=1
         
         interpretation:
          [b7] = 0,
          
          [c6] = 0,
          
          [b6] = 0,
          
          [b5] = 0,
          
          [b4] = 1,
          
          [b3] = 4,
          
          [b2] = 4,
          
          [b1] = 4
         orientation:
          b6() = 0 >= 0 = b7()
          
          c6() = 0 >= 0 = b7()
          
          b1() = 4 >= 4 = b2()
          
          b2() = 4 >= 4 = b3()
          
          b3() = 4 >= 1 = b4()
          
          b4() = 1 >= 0 = b5()
          
          b5() = 0 >= 0 = b6()
         problem:
          b6() -> b7()
          c6() -> b7()
          b1() -> b2()
          b2() -> b3()
          b5() -> b6()
         Matrix Interpretation Processor: dim=1
          
          interpretation:
           [b7] = 0,
           
           [c6] = 0,
           
           [b6] = 0,
           
           [b5] = 1,
           
           [b3] = 0,
           
           [b2] = 0,
           
           [b1] = 0
          orientation:
           b6() = 0 >= 0 = b7()
           
           c6() = 0 >= 0 = b7()
           
           b1() = 0 >= 0 = b2()
           
           b2() = 0 >= 0 = b3()
           
           b5() = 1 >= 0 = b6()
          problem:
           b6() -> b7()
           c6() -> b7()
           b1() -> b2()
           b2() -> b3()
          Matrix Interpretation Processor: dim=1
           
           interpretation:
            [b7] = 0,
            
            [c6] = 0,
            
            [b6] = 0,
            
            [b3] = 0,
            
            [b2] = 4,
            
            [b1] = 4
           orientation:
            b6() = 0 >= 0 = b7()
            
            c6() = 0 >= 0 = b7()
            
            b1() = 4 >= 4 = b2()
            
            b2() = 4 >= 0 = b3()
           problem:
            b6() -> b7()
            c6() -> b7()
            b1() -> b2()
           Matrix Interpretation Processor: dim=1
            
            interpretation:
             [b7] = 0,
             
             [c6] = 0,
             
             [b6] = 0,
             
             [b2] = 0,
             
             [b1] = 1
            orientation:
             b6() = 0 >= 0 = b7()
             
             c6() = 0 >= 0 = b7()
             
             b1() = 1 >= 0 = b2()
            problem:
             b6() -> b7()
             c6() -> b7()
            Matrix Interpretation Processor: dim=1
             
             interpretation:
              [b7] = 0,
              
              [c6] = 1,
              
              [b6] = 0
             orientation:
              b6() = 0 >= 0 = b7()
              
              c6() = 1 >= 0 = b7()
             problem:
              b6() -> b7()
             Matrix Interpretation Processor: dim=1
              
              interpretation:
               [b7] = 0,
               
               [b6] = 1
              orientation:
               b6() = 1 >= 0 = b7()
              problem:
               
              Qed