MAYBE

Problem:
 a12(a12(x1)) -> x1
 a13(a13(x1)) -> x1
 a14(a14(x1)) -> x1
 a15(a15(x1)) -> x1
 a16(a16(x1)) -> x1
 a23(a23(x1)) -> x1
 a24(a24(x1)) -> x1
 a25(a25(x1)) -> x1
 a26(a26(x1)) -> x1
 a34(a34(x1)) -> x1
 a35(a35(x1)) -> x1
 a36(a36(x1)) -> x1
 a45(a45(x1)) -> x1
 a46(a46(x1)) -> x1
 a56(a56(x1)) -> x1
 a13(x1) -> a12(a23(a12(x1)))
 a14(x1) -> a12(a23(a34(a23(a12(x1)))))
 a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1)))))))
 a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
 a24(x1) -> a23(a34(a23(x1)))
 a25(x1) -> a23(a34(a45(a34(a23(x1)))))
 a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1)))))))
 a35(x1) -> a34(a45(a34(x1)))
 a36(x1) -> a34(a45(a56(a45(a34(x1)))))
 a46(x1) -> a45(a56(a45(x1)))
 a12(a23(a12(a23(a12(a23(x1)))))) -> x1
 a23(a34(a23(a34(a23(a34(x1)))))) -> x1
 a34(a45(a34(a45(a34(a45(x1)))))) -> x1
 a45(a56(a45(a56(a45(a56(x1)))))) -> x1
 a12(a34(x1)) -> a34(a12(x1))
 a12(a45(x1)) -> a45(a12(x1))
 a12(a56(x1)) -> a56(a12(x1))
 a23(a45(x1)) -> a45(a23(x1))
 a23(a56(x1)) -> a56(a23(x1))
 a34(a56(x1)) -> a56(a34(x1))

Proof:
 Complexity Transformation Processor:
  strict:
   a12(a12(x1)) -> x1
   a13(a13(x1)) -> x1
   a14(a14(x1)) -> x1
   a15(a15(x1)) -> x1
   a16(a16(x1)) -> x1
   a23(a23(x1)) -> x1
   a24(a24(x1)) -> x1
   a25(a25(x1)) -> x1
   a26(a26(x1)) -> x1
   a34(a34(x1)) -> x1
   a35(a35(x1)) -> x1
   a36(a36(x1)) -> x1
   a45(a45(x1)) -> x1
   a46(a46(x1)) -> x1
   a56(a56(x1)) -> x1
   a13(x1) -> a12(a23(a12(x1)))
   a14(x1) -> a12(a23(a34(a23(a12(x1)))))
   a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1)))))))
   a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
   a24(x1) -> a23(a34(a23(x1)))
   a25(x1) -> a23(a34(a45(a34(a23(x1)))))
   a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1)))))))
   a35(x1) -> a34(a45(a34(x1)))
   a36(x1) -> a34(a45(a56(a45(a34(x1)))))
   a46(x1) -> a45(a56(a45(x1)))
   a12(a23(a12(a23(a12(a23(x1)))))) -> x1
   a23(a34(a23(a34(a23(a34(x1)))))) -> x1
   a34(a45(a34(a45(a34(a45(x1)))))) -> x1
   a45(a56(a45(a56(a45(a56(x1)))))) -> x1
   a12(a34(x1)) -> a34(a12(x1))
   a12(a45(x1)) -> a45(a12(x1))
   a12(a56(x1)) -> a56(a12(x1))
   a23(a45(x1)) -> a45(a23(x1))
   a23(a56(x1)) -> a56(a23(x1))
   a34(a56(x1)) -> a56(a34(x1))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [a56](x0) = x0,
     
     [a46](x0) = x0,
     
     [a45](x0) = x0,
     
     [a36](x0) = x0,
     
     [a35](x0) = x0,
     
     [a34](x0) = x0,
     
     [a26](x0) = x0 + 1,
     
     [a25](x0) = x0,
     
     [a24](x0) = x0,
     
     [a23](x0) = x0,
     
     [a16](x0) = x0,
     
     [a15](x0) = x0,
     
     [a14](x0) = x0,
     
     [a13](x0) = x0,
     
     [a12](x0) = x0
    orientation:
     a12(a12(x1)) = x1 >= x1 = x1
     
     a13(a13(x1)) = x1 >= x1 = x1
     
     a14(a14(x1)) = x1 >= x1 = x1
     
     a15(a15(x1)) = x1 >= x1 = x1
     
     a16(a16(x1)) = x1 >= x1 = x1
     
     a23(a23(x1)) = x1 >= x1 = x1
     
     a24(a24(x1)) = x1 >= x1 = x1
     
     a25(a25(x1)) = x1 >= x1 = x1
     
     a26(a26(x1)) = x1 + 2 >= x1 = x1
     
     a34(a34(x1)) = x1 >= x1 = x1
     
     a35(a35(x1)) = x1 >= x1 = x1
     
     a36(a36(x1)) = x1 >= x1 = x1
     
     a45(a45(x1)) = x1 >= x1 = x1
     
     a46(a46(x1)) = x1 >= x1 = x1
     
     a56(a56(x1)) = x1 >= x1 = x1
     
     a13(x1) = x1 >= x1 = a12(a23(a12(x1)))
     
     a14(x1) = x1 >= x1 = a12(a23(a34(a23(a12(x1)))))
     
     a15(x1) = x1 >= x1 = a12(a23(a34(a45(a34(a23(a12(x1)))))))
     
     a16(x1) = x1 >= x1 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
     
     a24(x1) = x1 >= x1 = a23(a34(a23(x1)))
     
     a25(x1) = x1 >= x1 = a23(a34(a45(a34(a23(x1)))))
     
     a26(x1) = x1 + 1 >= x1 = a23(a34(a45(a56(a45(a34(a23(x1)))))))
     
     a35(x1) = x1 >= x1 = a34(a45(a34(x1)))
     
     a36(x1) = x1 >= x1 = a34(a45(a56(a45(a34(x1)))))
     
     a46(x1) = x1 >= x1 = a45(a56(a45(x1)))
     
     a12(a23(a12(a23(a12(a23(x1)))))) = x1 >= x1 = x1
     
     a23(a34(a23(a34(a23(a34(x1)))))) = x1 >= x1 = x1
     
     a34(a45(a34(a45(a34(a45(x1)))))) = x1 >= x1 = x1
     
     a45(a56(a45(a56(a45(a56(x1)))))) = x1 >= x1 = x1
     
     a12(a34(x1)) = x1 >= x1 = a34(a12(x1))
     
     a12(a45(x1)) = x1 >= x1 = a45(a12(x1))
     
     a12(a56(x1)) = x1 >= x1 = a56(a12(x1))
     
     a23(a45(x1)) = x1 >= x1 = a45(a23(x1))
     
     a23(a56(x1)) = x1 >= x1 = a56(a23(x1))
     
     a34(a56(x1)) = x1 >= x1 = a56(a34(x1))
    problem:
     strict:
      a12(a12(x1)) -> x1
      a13(a13(x1)) -> x1
      a14(a14(x1)) -> x1
      a15(a15(x1)) -> x1
      a16(a16(x1)) -> x1
      a23(a23(x1)) -> x1
      a24(a24(x1)) -> x1
      a25(a25(x1)) -> x1
      a34(a34(x1)) -> x1
      a35(a35(x1)) -> x1
      a36(a36(x1)) -> x1
      a45(a45(x1)) -> x1
      a46(a46(x1)) -> x1
      a56(a56(x1)) -> x1
      a13(x1) -> a12(a23(a12(x1)))
      a14(x1) -> a12(a23(a34(a23(a12(x1)))))
      a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1)))))))
      a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
      a24(x1) -> a23(a34(a23(x1)))
      a25(x1) -> a23(a34(a45(a34(a23(x1)))))
      a35(x1) -> a34(a45(a34(x1)))
      a36(x1) -> a34(a45(a56(a45(a34(x1)))))
      a46(x1) -> a45(a56(a45(x1)))
      a12(a23(a12(a23(a12(a23(x1)))))) -> x1
      a23(a34(a23(a34(a23(a34(x1)))))) -> x1
      a34(a45(a34(a45(a34(a45(x1)))))) -> x1
      a45(a56(a45(a56(a45(a56(x1)))))) -> x1
      a12(a34(x1)) -> a34(a12(x1))
      a12(a45(x1)) -> a45(a12(x1))
      a12(a56(x1)) -> a56(a12(x1))
      a23(a45(x1)) -> a45(a23(x1))
      a23(a56(x1)) -> a56(a23(x1))
      a34(a56(x1)) -> a56(a34(x1))
     weak:
      a26(a26(x1)) -> x1
      a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1)))))))
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [a56](x0) = x0,
       
       [a46](x0) = x0,
       
       [a45](x0) = x0,
       
       [a36](x0) = x0 + 1,
       
       [a35](x0) = x0,
       
       [a34](x0) = x0,
       
       [a26](x0) = x0,
       
       [a25](x0) = x0,
       
       [a24](x0) = x0,
       
       [a23](x0) = x0,
       
       [a16](x0) = x0,
       
       [a15](x0) = x0,
       
       [a14](x0) = x0,
       
       [a13](x0) = x0,
       
       [a12](x0) = x0
      orientation:
       a12(a12(x1)) = x1 >= x1 = x1
       
       a13(a13(x1)) = x1 >= x1 = x1
       
       a14(a14(x1)) = x1 >= x1 = x1
       
       a15(a15(x1)) = x1 >= x1 = x1
       
       a16(a16(x1)) = x1 >= x1 = x1
       
       a23(a23(x1)) = x1 >= x1 = x1
       
       a24(a24(x1)) = x1 >= x1 = x1
       
       a25(a25(x1)) = x1 >= x1 = x1
       
       a34(a34(x1)) = x1 >= x1 = x1
       
       a35(a35(x1)) = x1 >= x1 = x1
       
       a36(a36(x1)) = x1 + 2 >= x1 = x1
       
       a45(a45(x1)) = x1 >= x1 = x1
       
       a46(a46(x1)) = x1 >= x1 = x1
       
       a56(a56(x1)) = x1 >= x1 = x1
       
       a13(x1) = x1 >= x1 = a12(a23(a12(x1)))
       
       a14(x1) = x1 >= x1 = a12(a23(a34(a23(a12(x1)))))
       
       a15(x1) = x1 >= x1 = a12(a23(a34(a45(a34(a23(a12(x1)))))))
       
       a16(x1) = x1 >= x1 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
       
       a24(x1) = x1 >= x1 = a23(a34(a23(x1)))
       
       a25(x1) = x1 >= x1 = a23(a34(a45(a34(a23(x1)))))
       
       a35(x1) = x1 >= x1 = a34(a45(a34(x1)))
       
       a36(x1) = x1 + 1 >= x1 = a34(a45(a56(a45(a34(x1)))))
       
       a46(x1) = x1 >= x1 = a45(a56(a45(x1)))
       
       a12(a23(a12(a23(a12(a23(x1)))))) = x1 >= x1 = x1
       
       a23(a34(a23(a34(a23(a34(x1)))))) = x1 >= x1 = x1
       
       a34(a45(a34(a45(a34(a45(x1)))))) = x1 >= x1 = x1
       
       a45(a56(a45(a56(a45(a56(x1)))))) = x1 >= x1 = x1
       
       a12(a34(x1)) = x1 >= x1 = a34(a12(x1))
       
       a12(a45(x1)) = x1 >= x1 = a45(a12(x1))
       
       a12(a56(x1)) = x1 >= x1 = a56(a12(x1))
       
       a23(a45(x1)) = x1 >= x1 = a45(a23(x1))
       
       a23(a56(x1)) = x1 >= x1 = a56(a23(x1))
       
       a34(a56(x1)) = x1 >= x1 = a56(a34(x1))
       
       a26(a26(x1)) = x1 >= x1 = x1
       
       a26(x1) = x1 >= x1 = a23(a34(a45(a56(a45(a34(a23(x1)))))))
      problem:
       strict:
        a12(a12(x1)) -> x1
        a13(a13(x1)) -> x1
        a14(a14(x1)) -> x1
        a15(a15(x1)) -> x1
        a16(a16(x1)) -> x1
        a23(a23(x1)) -> x1
        a24(a24(x1)) -> x1
        a25(a25(x1)) -> x1
        a34(a34(x1)) -> x1
        a35(a35(x1)) -> x1
        a45(a45(x1)) -> x1
        a46(a46(x1)) -> x1
        a56(a56(x1)) -> x1
        a13(x1) -> a12(a23(a12(x1)))
        a14(x1) -> a12(a23(a34(a23(a12(x1)))))
        a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1)))))))
        a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
        a24(x1) -> a23(a34(a23(x1)))
        a25(x1) -> a23(a34(a45(a34(a23(x1)))))
        a35(x1) -> a34(a45(a34(x1)))
        a46(x1) -> a45(a56(a45(x1)))
        a12(a23(a12(a23(a12(a23(x1)))))) -> x1
        a23(a34(a23(a34(a23(a34(x1)))))) -> x1
        a34(a45(a34(a45(a34(a45(x1)))))) -> x1
        a45(a56(a45(a56(a45(a56(x1)))))) -> x1
        a12(a34(x1)) -> a34(a12(x1))
        a12(a45(x1)) -> a45(a12(x1))
        a12(a56(x1)) -> a56(a12(x1))
        a23(a45(x1)) -> a45(a23(x1))
        a23(a56(x1)) -> a56(a23(x1))
        a34(a56(x1)) -> a56(a34(x1))
       weak:
        a36(a36(x1)) -> x1
        a36(x1) -> a34(a45(a56(a45(a34(x1)))))
        a26(a26(x1)) -> x1
        a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1)))))))
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [a56](x0) = x0,
         
         [a46](x0) = x0,
         
         [a45](x0) = x0,
         
         [a36](x0) = x0 + 1,
         
         [a35](x0) = x0 + 1,
         
         [a34](x0) = x0,
         
         [a26](x0) = x0,
         
         [a25](x0) = x0,
         
         [a24](x0) = x0,
         
         [a23](x0) = x0,
         
         [a16](x0) = x0,
         
         [a15](x0) = x0,
         
         [a14](x0) = x0,
         
         [a13](x0) = x0,
         
         [a12](x0) = x0
        orientation:
         a12(a12(x1)) = x1 >= x1 = x1
         
         a13(a13(x1)) = x1 >= x1 = x1
         
         a14(a14(x1)) = x1 >= x1 = x1
         
         a15(a15(x1)) = x1 >= x1 = x1
         
         a16(a16(x1)) = x1 >= x1 = x1
         
         a23(a23(x1)) = x1 >= x1 = x1
         
         a24(a24(x1)) = x1 >= x1 = x1
         
         a25(a25(x1)) = x1 >= x1 = x1
         
         a34(a34(x1)) = x1 >= x1 = x1
         
         a35(a35(x1)) = x1 + 2 >= x1 = x1
         
         a45(a45(x1)) = x1 >= x1 = x1
         
         a46(a46(x1)) = x1 >= x1 = x1
         
         a56(a56(x1)) = x1 >= x1 = x1
         
         a13(x1) = x1 >= x1 = a12(a23(a12(x1)))
         
         a14(x1) = x1 >= x1 = a12(a23(a34(a23(a12(x1)))))
         
         a15(x1) = x1 >= x1 = a12(a23(a34(a45(a34(a23(a12(x1)))))))
         
         a16(x1) = x1 >= x1 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
         
         a24(x1) = x1 >= x1 = a23(a34(a23(x1)))
         
         a25(x1) = x1 >= x1 = a23(a34(a45(a34(a23(x1)))))
         
         a35(x1) = x1 + 1 >= x1 = a34(a45(a34(x1)))
         
         a46(x1) = x1 >= x1 = a45(a56(a45(x1)))
         
         a12(a23(a12(a23(a12(a23(x1)))))) = x1 >= x1 = x1
         
         a23(a34(a23(a34(a23(a34(x1)))))) = x1 >= x1 = x1
         
         a34(a45(a34(a45(a34(a45(x1)))))) = x1 >= x1 = x1
         
         a45(a56(a45(a56(a45(a56(x1)))))) = x1 >= x1 = x1
         
         a12(a34(x1)) = x1 >= x1 = a34(a12(x1))
         
         a12(a45(x1)) = x1 >= x1 = a45(a12(x1))
         
         a12(a56(x1)) = x1 >= x1 = a56(a12(x1))
         
         a23(a45(x1)) = x1 >= x1 = a45(a23(x1))
         
         a23(a56(x1)) = x1 >= x1 = a56(a23(x1))
         
         a34(a56(x1)) = x1 >= x1 = a56(a34(x1))
         
         a36(a36(x1)) = x1 + 2 >= x1 = x1
         
         a36(x1) = x1 + 1 >= x1 = a34(a45(a56(a45(a34(x1)))))
         
         a26(a26(x1)) = x1 >= x1 = x1
         
         a26(x1) = x1 >= x1 = a23(a34(a45(a56(a45(a34(a23(x1)))))))
        problem:
         strict:
          a12(a12(x1)) -> x1
          a13(a13(x1)) -> x1
          a14(a14(x1)) -> x1
          a15(a15(x1)) -> x1
          a16(a16(x1)) -> x1
          a23(a23(x1)) -> x1
          a24(a24(x1)) -> x1
          a25(a25(x1)) -> x1
          a34(a34(x1)) -> x1
          a45(a45(x1)) -> x1
          a46(a46(x1)) -> x1
          a56(a56(x1)) -> x1
          a13(x1) -> a12(a23(a12(x1)))
          a14(x1) -> a12(a23(a34(a23(a12(x1)))))
          a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1)))))))
          a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
          a24(x1) -> a23(a34(a23(x1)))
          a25(x1) -> a23(a34(a45(a34(a23(x1)))))
          a46(x1) -> a45(a56(a45(x1)))
          a12(a23(a12(a23(a12(a23(x1)))))) -> x1
          a23(a34(a23(a34(a23(a34(x1)))))) -> x1
          a34(a45(a34(a45(a34(a45(x1)))))) -> x1
          a45(a56(a45(a56(a45(a56(x1)))))) -> x1
          a12(a34(x1)) -> a34(a12(x1))
          a12(a45(x1)) -> a45(a12(x1))
          a12(a56(x1)) -> a56(a12(x1))
          a23(a45(x1)) -> a45(a23(x1))
          a23(a56(x1)) -> a56(a23(x1))
          a34(a56(x1)) -> a56(a34(x1))
         weak:
          a35(a35(x1)) -> x1
          a35(x1) -> a34(a45(a34(x1)))
          a36(a36(x1)) -> x1
          a36(x1) -> a34(a45(a56(a45(a34(x1)))))
          a26(a26(x1)) -> x1
          a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1)))))))
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [a56](x0) = x0,
           
           [a46](x0) = x0,
           
           [a45](x0) = x0,
           
           [a36](x0) = x0,
           
           [a35](x0) = x0,
           
           [a34](x0) = x0,
           
           [a26](x0) = x0 + 1,
           
           [a25](x0) = x0,
           
           [a24](x0) = x0,
           
           [a23](x0) = x0,
           
           [a16](x0) = x0,
           
           [a15](x0) = x0,
           
           [a14](x0) = x0,
           
           [a13](x0) = x0,
           
           [a12](x0) = x0 + 1
          orientation:
           a12(a12(x1)) = x1 + 2 >= x1 = x1
           
           a13(a13(x1)) = x1 >= x1 = x1
           
           a14(a14(x1)) = x1 >= x1 = x1
           
           a15(a15(x1)) = x1 >= x1 = x1
           
           a16(a16(x1)) = x1 >= x1 = x1
           
           a23(a23(x1)) = x1 >= x1 = x1
           
           a24(a24(x1)) = x1 >= x1 = x1
           
           a25(a25(x1)) = x1 >= x1 = x1
           
           a34(a34(x1)) = x1 >= x1 = x1
           
           a45(a45(x1)) = x1 >= x1 = x1
           
           a46(a46(x1)) = x1 >= x1 = x1
           
           a56(a56(x1)) = x1 >= x1 = x1
           
           a13(x1) = x1 >= x1 + 2 = a12(a23(a12(x1)))
           
           a14(x1) = x1 >= x1 + 2 = a12(a23(a34(a23(a12(x1)))))
           
           a15(x1) = x1 >= x1 + 2 = a12(a23(a34(a45(a34(a23(a12(x1)))))))
           
           a16(x1) = x1 >= x1 + 2 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
           
           a24(x1) = x1 >= x1 = a23(a34(a23(x1)))
           
           a25(x1) = x1 >= x1 = a23(a34(a45(a34(a23(x1)))))
           
           a46(x1) = x1 >= x1 = a45(a56(a45(x1)))
           
           a12(a23(a12(a23(a12(a23(x1)))))) = x1 + 3 >= x1 = x1
           
           a23(a34(a23(a34(a23(a34(x1)))))) = x1 >= x1 = x1
           
           a34(a45(a34(a45(a34(a45(x1)))))) = x1 >= x1 = x1
           
           a45(a56(a45(a56(a45(a56(x1)))))) = x1 >= x1 = x1
           
           a12(a34(x1)) = x1 + 1 >= x1 + 1 = a34(a12(x1))
           
           a12(a45(x1)) = x1 + 1 >= x1 + 1 = a45(a12(x1))
           
           a12(a56(x1)) = x1 + 1 >= x1 + 1 = a56(a12(x1))
           
           a23(a45(x1)) = x1 >= x1 = a45(a23(x1))
           
           a23(a56(x1)) = x1 >= x1 = a56(a23(x1))
           
           a34(a56(x1)) = x1 >= x1 = a56(a34(x1))
           
           a35(a35(x1)) = x1 >= x1 = x1
           
           a35(x1) = x1 >= x1 = a34(a45(a34(x1)))
           
           a36(a36(x1)) = x1 >= x1 = x1
           
           a36(x1) = x1 >= x1 = a34(a45(a56(a45(a34(x1)))))
           
           a26(a26(x1)) = x1 + 2 >= x1 = x1
           
           a26(x1) = x1 + 1 >= x1 = a23(a34(a45(a56(a45(a34(a23(x1)))))))
          problem:
           strict:
            a13(a13(x1)) -> x1
            a14(a14(x1)) -> x1
            a15(a15(x1)) -> x1
            a16(a16(x1)) -> x1
            a23(a23(x1)) -> x1
            a24(a24(x1)) -> x1
            a25(a25(x1)) -> x1
            a34(a34(x1)) -> x1
            a45(a45(x1)) -> x1
            a46(a46(x1)) -> x1
            a56(a56(x1)) -> x1
            a13(x1) -> a12(a23(a12(x1)))
            a14(x1) -> a12(a23(a34(a23(a12(x1)))))
            a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1)))))))
            a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
            a24(x1) -> a23(a34(a23(x1)))
            a25(x1) -> a23(a34(a45(a34(a23(x1)))))
            a46(x1) -> a45(a56(a45(x1)))
            a23(a34(a23(a34(a23(a34(x1)))))) -> x1
            a34(a45(a34(a45(a34(a45(x1)))))) -> x1
            a45(a56(a45(a56(a45(a56(x1)))))) -> x1
            a12(a34(x1)) -> a34(a12(x1))
            a12(a45(x1)) -> a45(a12(x1))
            a12(a56(x1)) -> a56(a12(x1))
            a23(a45(x1)) -> a45(a23(x1))
            a23(a56(x1)) -> a56(a23(x1))
            a34(a56(x1)) -> a56(a34(x1))
           weak:
            a12(a12(x1)) -> x1
            a12(a23(a12(a23(a12(a23(x1)))))) -> x1
            a35(a35(x1)) -> x1
            a35(x1) -> a34(a45(a34(x1)))
            a36(a36(x1)) -> x1
            a36(x1) -> a34(a45(a56(a45(a34(x1)))))
            a26(a26(x1)) -> x1
            a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1)))))))
          Matrix Interpretation Processor:
           dimension: 1
           max_matrix:
            1
            interpretation:
             [a56](x0) = x0 + 1,
             
             [a46](x0) = x0,
             
             [a45](x0) = x0,
             
             [a36](x0) = x0 + 1,
             
             [a35](x0) = x0,
             
             [a34](x0) = x0,
             
             [a26](x0) = x0 + 1,
             
             [a25](x0) = x0 + 1,
             
             [a24](x0) = x0,
             
             [a23](x0) = x0,
             
             [a16](x0) = x0,
             
             [a15](x0) = x0,
             
             [a14](x0) = x0,
             
             [a13](x0) = x0,
             
             [a12](x0) = x0
            orientation:
             a13(a13(x1)) = x1 >= x1 = x1
             
             a14(a14(x1)) = x1 >= x1 = x1
             
             a15(a15(x1)) = x1 >= x1 = x1
             
             a16(a16(x1)) = x1 >= x1 = x1
             
             a23(a23(x1)) = x1 >= x1 = x1
             
             a24(a24(x1)) = x1 >= x1 = x1
             
             a25(a25(x1)) = x1 + 2 >= x1 = x1
             
             a34(a34(x1)) = x1 >= x1 = x1
             
             a45(a45(x1)) = x1 >= x1 = x1
             
             a46(a46(x1)) = x1 >= x1 = x1
             
             a56(a56(x1)) = x1 + 2 >= x1 = x1
             
             a13(x1) = x1 >= x1 = a12(a23(a12(x1)))
             
             a14(x1) = x1 >= x1 = a12(a23(a34(a23(a12(x1)))))
             
             a15(x1) = x1 >= x1 = a12(a23(a34(a45(a34(a23(a12(x1)))))))
             
             a16(x1) = x1 >= x1 + 1 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
             
             a24(x1) = x1 >= x1 = a23(a34(a23(x1)))
             
             a25(x1) = x1 + 1 >= x1 = a23(a34(a45(a34(a23(x1)))))
             
             a46(x1) = x1 >= x1 + 1 = a45(a56(a45(x1)))
             
             a23(a34(a23(a34(a23(a34(x1)))))) = x1 >= x1 = x1
             
             a34(a45(a34(a45(a34(a45(x1)))))) = x1 >= x1 = x1
             
             a45(a56(a45(a56(a45(a56(x1)))))) = x1 + 3 >= x1 = x1
             
             a12(a34(x1)) = x1 >= x1 = a34(a12(x1))
             
             a12(a45(x1)) = x1 >= x1 = a45(a12(x1))
             
             a12(a56(x1)) = x1 + 1 >= x1 + 1 = a56(a12(x1))
             
             a23(a45(x1)) = x1 >= x1 = a45(a23(x1))
             
             a23(a56(x1)) = x1 + 1 >= x1 + 1 = a56(a23(x1))
             
             a34(a56(x1)) = x1 + 1 >= x1 + 1 = a56(a34(x1))
             
             a12(a12(x1)) = x1 >= x1 = x1
             
             a12(a23(a12(a23(a12(a23(x1)))))) = x1 >= x1 = x1
             
             a35(a35(x1)) = x1 >= x1 = x1
             
             a35(x1) = x1 >= x1 = a34(a45(a34(x1)))
             
             a36(a36(x1)) = x1 + 2 >= x1 = x1
             
             a36(x1) = x1 + 1 >= x1 + 1 = a34(a45(a56(a45(a34(x1)))))
             
             a26(a26(x1)) = x1 + 2 >= x1 = x1
             
             a26(x1) = x1 + 1 >= x1 + 1 = a23(a34(a45(a56(a45(a34(a23(x1)))))))
            problem:
             strict:
              a13(a13(x1)) -> x1
              a14(a14(x1)) -> x1
              a15(a15(x1)) -> x1
              a16(a16(x1)) -> x1
              a23(a23(x1)) -> x1
              a24(a24(x1)) -> x1
              a34(a34(x1)) -> x1
              a45(a45(x1)) -> x1
              a46(a46(x1)) -> x1
              a13(x1) -> a12(a23(a12(x1)))
              a14(x1) -> a12(a23(a34(a23(a12(x1)))))
              a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1)))))))
              a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
              a24(x1) -> a23(a34(a23(x1)))
              a46(x1) -> a45(a56(a45(x1)))
              a23(a34(a23(a34(a23(a34(x1)))))) -> x1
              a34(a45(a34(a45(a34(a45(x1)))))) -> x1
              a12(a34(x1)) -> a34(a12(x1))
              a12(a45(x1)) -> a45(a12(x1))
              a12(a56(x1)) -> a56(a12(x1))
              a23(a45(x1)) -> a45(a23(x1))
              a23(a56(x1)) -> a56(a23(x1))
              a34(a56(x1)) -> a56(a34(x1))
             weak:
              a25(a25(x1)) -> x1
              a56(a56(x1)) -> x1
              a25(x1) -> a23(a34(a45(a34(a23(x1)))))
              a45(a56(a45(a56(a45(a56(x1)))))) -> x1
              a12(a12(x1)) -> x1
              a12(a23(a12(a23(a12(a23(x1)))))) -> x1
              a35(a35(x1)) -> x1
              a35(x1) -> a34(a45(a34(x1)))
              a36(a36(x1)) -> x1
              a36(x1) -> a34(a45(a56(a45(a34(x1)))))
              a26(a26(x1)) -> x1
              a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1)))))))
            Matrix Interpretation Processor:
             dimension: 1
             max_matrix:
              1
              interpretation:
               [a56](x0) = x0,
               
               [a46](x0) = x0 + 1,
               
               [a45](x0) = x0,
               
               [a36](x0) = x0,
               
               [a35](x0) = x0 + 1,
               
               [a34](x0) = x0,
               
               [a26](x0) = x0 + 1,
               
               [a25](x0) = x0 + 1,
               
               [a24](x0) = x0,
               
               [a23](x0) = x0,
               
               [a16](x0) = x0,
               
               [a15](x0) = x0,
               
               [a14](x0) = x0,
               
               [a13](x0) = x0,
               
               [a12](x0) = x0
              orientation:
               a13(a13(x1)) = x1 >= x1 = x1
               
               a14(a14(x1)) = x1 >= x1 = x1
               
               a15(a15(x1)) = x1 >= x1 = x1
               
               a16(a16(x1)) = x1 >= x1 = x1
               
               a23(a23(x1)) = x1 >= x1 = x1
               
               a24(a24(x1)) = x1 >= x1 = x1
               
               a34(a34(x1)) = x1 >= x1 = x1
               
               a45(a45(x1)) = x1 >= x1 = x1
               
               a46(a46(x1)) = x1 + 2 >= x1 = x1
               
               a13(x1) = x1 >= x1 = a12(a23(a12(x1)))
               
               a14(x1) = x1 >= x1 = a12(a23(a34(a23(a12(x1)))))
               
               a15(x1) = x1 >= x1 = a12(a23(a34(a45(a34(a23(a12(x1)))))))
               
               a16(x1) = x1 >= x1 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
               
               a24(x1) = x1 >= x1 = a23(a34(a23(x1)))
               
               a46(x1) = x1 + 1 >= x1 = a45(a56(a45(x1)))
               
               a23(a34(a23(a34(a23(a34(x1)))))) = x1 >= x1 = x1
               
               a34(a45(a34(a45(a34(a45(x1)))))) = x1 >= x1 = x1
               
               a12(a34(x1)) = x1 >= x1 = a34(a12(x1))
               
               a12(a45(x1)) = x1 >= x1 = a45(a12(x1))
               
               a12(a56(x1)) = x1 >= x1 = a56(a12(x1))
               
               a23(a45(x1)) = x1 >= x1 = a45(a23(x1))
               
               a23(a56(x1)) = x1 >= x1 = a56(a23(x1))
               
               a34(a56(x1)) = x1 >= x1 = a56(a34(x1))
               
               a25(a25(x1)) = x1 + 2 >= x1 = x1
               
               a56(a56(x1)) = x1 >= x1 = x1
               
               a25(x1) = x1 + 1 >= x1 = a23(a34(a45(a34(a23(x1)))))
               
               a45(a56(a45(a56(a45(a56(x1)))))) = x1 >= x1 = x1
               
               a12(a12(x1)) = x1 >= x1 = x1
               
               a12(a23(a12(a23(a12(a23(x1)))))) = x1 >= x1 = x1
               
               a35(a35(x1)) = x1 + 2 >= x1 = x1
               
               a35(x1) = x1 + 1 >= x1 = a34(a45(a34(x1)))
               
               a36(a36(x1)) = x1 >= x1 = x1
               
               a36(x1) = x1 >= x1 = a34(a45(a56(a45(a34(x1)))))
               
               a26(a26(x1)) = x1 + 2 >= x1 = x1
               
               a26(x1) = x1 + 1 >= x1 = a23(a34(a45(a56(a45(a34(a23(x1)))))))
              problem:
               strict:
                a13(a13(x1)) -> x1
                a14(a14(x1)) -> x1
                a15(a15(x1)) -> x1
                a16(a16(x1)) -> x1
                a23(a23(x1)) -> x1
                a24(a24(x1)) -> x1
                a34(a34(x1)) -> x1
                a45(a45(x1)) -> x1
                a13(x1) -> a12(a23(a12(x1)))
                a14(x1) -> a12(a23(a34(a23(a12(x1)))))
                a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1)))))))
                a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
                a24(x1) -> a23(a34(a23(x1)))
                a23(a34(a23(a34(a23(a34(x1)))))) -> x1
                a34(a45(a34(a45(a34(a45(x1)))))) -> x1
                a12(a34(x1)) -> a34(a12(x1))
                a12(a45(x1)) -> a45(a12(x1))
                a12(a56(x1)) -> a56(a12(x1))
                a23(a45(x1)) -> a45(a23(x1))
                a23(a56(x1)) -> a56(a23(x1))
                a34(a56(x1)) -> a56(a34(x1))
               weak:
                a46(a46(x1)) -> x1
                a46(x1) -> a45(a56(a45(x1)))
                a25(a25(x1)) -> x1
                a56(a56(x1)) -> x1
                a25(x1) -> a23(a34(a45(a34(a23(x1)))))
                a45(a56(a45(a56(a45(a56(x1)))))) -> x1
                a12(a12(x1)) -> x1
                a12(a23(a12(a23(a12(a23(x1)))))) -> x1
                a35(a35(x1)) -> x1
                a35(x1) -> a34(a45(a34(x1)))
                a36(a36(x1)) -> x1
                a36(x1) -> a34(a45(a56(a45(a34(x1)))))
                a26(a26(x1)) -> x1
                a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1)))))))
              Matrix Interpretation Processor:
               dimension: 1
               max_matrix:
                1
                interpretation:
                 [a56](x0) = x0,
                 
                 [a46](x0) = x0,
                 
                 [a45](x0) = x0,
                 
                 [a36](x0) = x0,
                 
                 [a35](x0) = x0,
                 
                 [a34](x0) = x0,
                 
                 [a26](x0) = x0 + 1,
                 
                 [a25](x0) = x0 + 1,
                 
                 [a24](x0) = x0 + 1,
                 
                 [a23](x0) = x0,
                 
                 [a16](x0) = x0,
                 
                 [a15](x0) = x0,
                 
                 [a14](x0) = x0,
                 
                 [a13](x0) = x0,
                 
                 [a12](x0) = x0
                orientation:
                 a13(a13(x1)) = x1 >= x1 = x1
                 
                 a14(a14(x1)) = x1 >= x1 = x1
                 
                 a15(a15(x1)) = x1 >= x1 = x1
                 
                 a16(a16(x1)) = x1 >= x1 = x1
                 
                 a23(a23(x1)) = x1 >= x1 = x1
                 
                 a24(a24(x1)) = x1 + 2 >= x1 = x1
                 
                 a34(a34(x1)) = x1 >= x1 = x1
                 
                 a45(a45(x1)) = x1 >= x1 = x1
                 
                 a13(x1) = x1 >= x1 = a12(a23(a12(x1)))
                 
                 a14(x1) = x1 >= x1 = a12(a23(a34(a23(a12(x1)))))
                 
                 a15(x1) = x1 >= x1 = a12(a23(a34(a45(a34(a23(a12(x1)))))))
                 
                 a16(x1) = x1 >= x1 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
                 
                 a24(x1) = x1 + 1 >= x1 = a23(a34(a23(x1)))
                 
                 a23(a34(a23(a34(a23(a34(x1)))))) = x1 >= x1 = x1
                 
                 a34(a45(a34(a45(a34(a45(x1)))))) = x1 >= x1 = x1
                 
                 a12(a34(x1)) = x1 >= x1 = a34(a12(x1))
                 
                 a12(a45(x1)) = x1 >= x1 = a45(a12(x1))
                 
                 a12(a56(x1)) = x1 >= x1 = a56(a12(x1))
                 
                 a23(a45(x1)) = x1 >= x1 = a45(a23(x1))
                 
                 a23(a56(x1)) = x1 >= x1 = a56(a23(x1))
                 
                 a34(a56(x1)) = x1 >= x1 = a56(a34(x1))
                 
                 a46(a46(x1)) = x1 >= x1 = x1
                 
                 a46(x1) = x1 >= x1 = a45(a56(a45(x1)))
                 
                 a25(a25(x1)) = x1 + 2 >= x1 = x1
                 
                 a56(a56(x1)) = x1 >= x1 = x1
                 
                 a25(x1) = x1 + 1 >= x1 = a23(a34(a45(a34(a23(x1)))))
                 
                 a45(a56(a45(a56(a45(a56(x1)))))) = x1 >= x1 = x1
                 
                 a12(a12(x1)) = x1 >= x1 = x1
                 
                 a12(a23(a12(a23(a12(a23(x1)))))) = x1 >= x1 = x1
                 
                 a35(a35(x1)) = x1 >= x1 = x1
                 
                 a35(x1) = x1 >= x1 = a34(a45(a34(x1)))
                 
                 a36(a36(x1)) = x1 >= x1 = x1
                 
                 a36(x1) = x1 >= x1 = a34(a45(a56(a45(a34(x1)))))
                 
                 a26(a26(x1)) = x1 + 2 >= x1 = x1
                 
                 a26(x1) = x1 + 1 >= x1 = a23(a34(a45(a56(a45(a34(a23(x1)))))))
                problem:
                 strict:
                  a13(a13(x1)) -> x1
                  a14(a14(x1)) -> x1
                  a15(a15(x1)) -> x1
                  a16(a16(x1)) -> x1
                  a23(a23(x1)) -> x1
                  a34(a34(x1)) -> x1
                  a45(a45(x1)) -> x1
                  a13(x1) -> a12(a23(a12(x1)))
                  a14(x1) -> a12(a23(a34(a23(a12(x1)))))
                  a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1)))))))
                  a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
                  a23(a34(a23(a34(a23(a34(x1)))))) -> x1
                  a34(a45(a34(a45(a34(a45(x1)))))) -> x1
                  a12(a34(x1)) -> a34(a12(x1))
                  a12(a45(x1)) -> a45(a12(x1))
                  a12(a56(x1)) -> a56(a12(x1))
                  a23(a45(x1)) -> a45(a23(x1))
                  a23(a56(x1)) -> a56(a23(x1))
                  a34(a56(x1)) -> a56(a34(x1))
                 weak:
                  a24(a24(x1)) -> x1
                  a24(x1) -> a23(a34(a23(x1)))
                  a46(a46(x1)) -> x1
                  a46(x1) -> a45(a56(a45(x1)))
                  a25(a25(x1)) -> x1
                  a56(a56(x1)) -> x1
                  a25(x1) -> a23(a34(a45(a34(a23(x1)))))
                  a45(a56(a45(a56(a45(a56(x1)))))) -> x1
                  a12(a12(x1)) -> x1
                  a12(a23(a12(a23(a12(a23(x1)))))) -> x1
                  a35(a35(x1)) -> x1
                  a35(x1) -> a34(a45(a34(x1)))
                  a36(a36(x1)) -> x1
                  a36(x1) -> a34(a45(a56(a45(a34(x1)))))
                  a26(a26(x1)) -> x1
                  a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1)))))))
                Matrix Interpretation Processor:
                 dimension: 1
                 max_matrix:
                  1
                  interpretation:
                   [a56](x0) = x0,
                   
                   [a46](x0) = x0,
                   
                   [a45](x0) = x0,
                   
                   [a36](x0) = x0 + 1,
                   
                   [a35](x0) = x0,
                   
                   [a34](x0) = x0,
                   
                   [a26](x0) = x0,
                   
                   [a25](x0) = x0,
                   
                   [a24](x0) = x0,
                   
                   [a23](x0) = x0,
                   
                   [a16](x0) = x0,
                   
                   [a15](x0) = x0,
                   
                   [a14](x0) = x0 + 1,
                   
                   [a13](x0) = x0,
                   
                   [a12](x0) = x0
                  orientation:
                   a13(a13(x1)) = x1 >= x1 = x1
                   
                   a14(a14(x1)) = x1 + 2 >= x1 = x1
                   
                   a15(a15(x1)) = x1 >= x1 = x1
                   
                   a16(a16(x1)) = x1 >= x1 = x1
                   
                   a23(a23(x1)) = x1 >= x1 = x1
                   
                   a34(a34(x1)) = x1 >= x1 = x1
                   
                   a45(a45(x1)) = x1 >= x1 = x1
                   
                   a13(x1) = x1 >= x1 = a12(a23(a12(x1)))
                   
                   a14(x1) = x1 + 1 >= x1 = a12(a23(a34(a23(a12(x1)))))
                   
                   a15(x1) = x1 >= x1 = a12(a23(a34(a45(a34(a23(a12(x1)))))))
                   
                   a16(x1) = x1 >= x1 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
                   
                   a23(a34(a23(a34(a23(a34(x1)))))) = x1 >= x1 = x1
                   
                   a34(a45(a34(a45(a34(a45(x1)))))) = x1 >= x1 = x1
                   
                   a12(a34(x1)) = x1 >= x1 = a34(a12(x1))
                   
                   a12(a45(x1)) = x1 >= x1 = a45(a12(x1))
                   
                   a12(a56(x1)) = x1 >= x1 = a56(a12(x1))
                   
                   a23(a45(x1)) = x1 >= x1 = a45(a23(x1))
                   
                   a23(a56(x1)) = x1 >= x1 = a56(a23(x1))
                   
                   a34(a56(x1)) = x1 >= x1 = a56(a34(x1))
                   
                   a24(a24(x1)) = x1 >= x1 = x1
                   
                   a24(x1) = x1 >= x1 = a23(a34(a23(x1)))
                   
                   a46(a46(x1)) = x1 >= x1 = x1
                   
                   a46(x1) = x1 >= x1 = a45(a56(a45(x1)))
                   
                   a25(a25(x1)) = x1 >= x1 = x1
                   
                   a56(a56(x1)) = x1 >= x1 = x1
                   
                   a25(x1) = x1 >= x1 = a23(a34(a45(a34(a23(x1)))))
                   
                   a45(a56(a45(a56(a45(a56(x1)))))) = x1 >= x1 = x1
                   
                   a12(a12(x1)) = x1 >= x1 = x1
                   
                   a12(a23(a12(a23(a12(a23(x1)))))) = x1 >= x1 = x1
                   
                   a35(a35(x1)) = x1 >= x1 = x1
                   
                   a35(x1) = x1 >= x1 = a34(a45(a34(x1)))
                   
                   a36(a36(x1)) = x1 + 2 >= x1 = x1
                   
                   a36(x1) = x1 + 1 >= x1 = a34(a45(a56(a45(a34(x1)))))
                   
                   a26(a26(x1)) = x1 >= x1 = x1
                   
                   a26(x1) = x1 >= x1 = a23(a34(a45(a56(a45(a34(a23(x1)))))))
                  problem:
                   strict:
                    a13(a13(x1)) -> x1
                    a15(a15(x1)) -> x1
                    a16(a16(x1)) -> x1
                    a23(a23(x1)) -> x1
                    a34(a34(x1)) -> x1
                    a45(a45(x1)) -> x1
                    a13(x1) -> a12(a23(a12(x1)))
                    a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1)))))))
                    a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
                    a23(a34(a23(a34(a23(a34(x1)))))) -> x1
                    a34(a45(a34(a45(a34(a45(x1)))))) -> x1
                    a12(a34(x1)) -> a34(a12(x1))
                    a12(a45(x1)) -> a45(a12(x1))
                    a12(a56(x1)) -> a56(a12(x1))
                    a23(a45(x1)) -> a45(a23(x1))
                    a23(a56(x1)) -> a56(a23(x1))
                    a34(a56(x1)) -> a56(a34(x1))
                   weak:
                    a14(a14(x1)) -> x1
                    a14(x1) -> a12(a23(a34(a23(a12(x1)))))
                    a24(a24(x1)) -> x1
                    a24(x1) -> a23(a34(a23(x1)))
                    a46(a46(x1)) -> x1
                    a46(x1) -> a45(a56(a45(x1)))
                    a25(a25(x1)) -> x1
                    a56(a56(x1)) -> x1
                    a25(x1) -> a23(a34(a45(a34(a23(x1)))))
                    a45(a56(a45(a56(a45(a56(x1)))))) -> x1
                    a12(a12(x1)) -> x1
                    a12(a23(a12(a23(a12(a23(x1)))))) -> x1
                    a35(a35(x1)) -> x1
                    a35(x1) -> a34(a45(a34(x1)))
                    a36(a36(x1)) -> x1
                    a36(x1) -> a34(a45(a56(a45(a34(x1)))))
                    a26(a26(x1)) -> x1
                    a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1)))))))
                  Matrix Interpretation Processor:
                   dimension: 1
                   max_matrix:
                    1
                    interpretation:
                     [a56](x0) = x0,
                     
                     [a46](x0) = x0 + 1,
                     
                     [a45](x0) = x0,
                     
                     [a36](x0) = x0,
                     
                     [a35](x0) = x0,
                     
                     [a34](x0) = x0,
                     
                     [a26](x0) = x0,
                     
                     [a25](x0) = x0,
                     
                     [a24](x0) = x0,
                     
                     [a23](x0) = x0,
                     
                     [a16](x0) = x0 + 1,
                     
                     [a15](x0) = x0,
                     
                     [a14](x0) = x0,
                     
                     [a13](x0) = x0,
                     
                     [a12](x0) = x0
                    orientation:
                     a13(a13(x1)) = x1 >= x1 = x1
                     
                     a15(a15(x1)) = x1 >= x1 = x1
                     
                     a16(a16(x1)) = x1 + 2 >= x1 = x1
                     
                     a23(a23(x1)) = x1 >= x1 = x1
                     
                     a34(a34(x1)) = x1 >= x1 = x1
                     
                     a45(a45(x1)) = x1 >= x1 = x1
                     
                     a13(x1) = x1 >= x1 = a12(a23(a12(x1)))
                     
                     a15(x1) = x1 >= x1 = a12(a23(a34(a45(a34(a23(a12(x1)))))))
                     
                     a16(x1) = x1 + 1 >= x1 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
                     
                     a23(a34(a23(a34(a23(a34(x1)))))) = x1 >= x1 = x1
                     
                     a34(a45(a34(a45(a34(a45(x1)))))) = x1 >= x1 = x1
                     
                     a12(a34(x1)) = x1 >= x1 = a34(a12(x1))
                     
                     a12(a45(x1)) = x1 >= x1 = a45(a12(x1))
                     
                     a12(a56(x1)) = x1 >= x1 = a56(a12(x1))
                     
                     a23(a45(x1)) = x1 >= x1 = a45(a23(x1))
                     
                     a23(a56(x1)) = x1 >= x1 = a56(a23(x1))
                     
                     a34(a56(x1)) = x1 >= x1 = a56(a34(x1))
                     
                     a14(a14(x1)) = x1 >= x1 = x1
                     
                     a14(x1) = x1 >= x1 = a12(a23(a34(a23(a12(x1)))))
                     
                     a24(a24(x1)) = x1 >= x1 = x1
                     
                     a24(x1) = x1 >= x1 = a23(a34(a23(x1)))
                     
                     a46(a46(x1)) = x1 + 2 >= x1 = x1
                     
                     a46(x1) = x1 + 1 >= x1 = a45(a56(a45(x1)))
                     
                     a25(a25(x1)) = x1 >= x1 = x1
                     
                     a56(a56(x1)) = x1 >= x1 = x1
                     
                     a25(x1) = x1 >= x1 = a23(a34(a45(a34(a23(x1)))))
                     
                     a45(a56(a45(a56(a45(a56(x1)))))) = x1 >= x1 = x1
                     
                     a12(a12(x1)) = x1 >= x1 = x1
                     
                     a12(a23(a12(a23(a12(a23(x1)))))) = x1 >= x1 = x1
                     
                     a35(a35(x1)) = x1 >= x1 = x1
                     
                     a35(x1) = x1 >= x1 = a34(a45(a34(x1)))
                     
                     a36(a36(x1)) = x1 >= x1 = x1
                     
                     a36(x1) = x1 >= x1 = a34(a45(a56(a45(a34(x1)))))
                     
                     a26(a26(x1)) = x1 >= x1 = x1
                     
                     a26(x1) = x1 >= x1 = a23(a34(a45(a56(a45(a34(a23(x1)))))))
                    problem:
                     strict:
                      a13(a13(x1)) -> x1
                      a15(a15(x1)) -> x1
                      a23(a23(x1)) -> x1
                      a34(a34(x1)) -> x1
                      a45(a45(x1)) -> x1
                      a13(x1) -> a12(a23(a12(x1)))
                      a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1)))))))
                      a23(a34(a23(a34(a23(a34(x1)))))) -> x1
                      a34(a45(a34(a45(a34(a45(x1)))))) -> x1
                      a12(a34(x1)) -> a34(a12(x1))
                      a12(a45(x1)) -> a45(a12(x1))
                      a12(a56(x1)) -> a56(a12(x1))
                      a23(a45(x1)) -> a45(a23(x1))
                      a23(a56(x1)) -> a56(a23(x1))
                      a34(a56(x1)) -> a56(a34(x1))
                     weak:
                      a16(a16(x1)) -> x1
                      a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
                      a14(a14(x1)) -> x1
                      a14(x1) -> a12(a23(a34(a23(a12(x1)))))
                      a24(a24(x1)) -> x1
                      a24(x1) -> a23(a34(a23(x1)))
                      a46(a46(x1)) -> x1
                      a46(x1) -> a45(a56(a45(x1)))
                      a25(a25(x1)) -> x1
                      a56(a56(x1)) -> x1
                      a25(x1) -> a23(a34(a45(a34(a23(x1)))))
                      a45(a56(a45(a56(a45(a56(x1)))))) -> x1
                      a12(a12(x1)) -> x1
                      a12(a23(a12(a23(a12(a23(x1)))))) -> x1
                      a35(a35(x1)) -> x1
                      a35(x1) -> a34(a45(a34(x1)))
                      a36(a36(x1)) -> x1
                      a36(x1) -> a34(a45(a56(a45(a34(x1)))))
                      a26(a26(x1)) -> x1
                      a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1)))))))
                    Matrix Interpretation Processor:
                     dimension: 1
                     max_matrix:
                      1
                      interpretation:
                       [a56](x0) = x0 + 1,
                       
                       [a46](x0) = x0 + 1,
                       
                       [a45](x0) = x0,
                       
                       [a36](x0) = x0 + 1,
                       
                       [a35](x0) = x0 + 1,
                       
                       [a34](x0) = x0,
                       
                       [a26](x0) = x0 + 1,
                       
                       [a25](x0) = x0,
                       
                       [a24](x0) = x0,
                       
                       [a23](x0) = x0,
                       
                       [a16](x0) = x0 + 1,
                       
                       [a15](x0) = x0 + 1,
                       
                       [a14](x0) = x0,
                       
                       [a13](x0) = x0,
                       
                       [a12](x0) = x0
                      orientation:
                       a13(a13(x1)) = x1 >= x1 = x1
                       
                       a15(a15(x1)) = x1 + 2 >= x1 = x1
                       
                       a23(a23(x1)) = x1 >= x1 = x1
                       
                       a34(a34(x1)) = x1 >= x1 = x1
                       
                       a45(a45(x1)) = x1 >= x1 = x1
                       
                       a13(x1) = x1 >= x1 = a12(a23(a12(x1)))
                       
                       a15(x1) = x1 + 1 >= x1 = a12(a23(a34(a45(a34(a23(a12(x1)))))))
                       
                       a23(a34(a23(a34(a23(a34(x1)))))) = x1 >= x1 = x1
                       
                       a34(a45(a34(a45(a34(a45(x1)))))) = x1 >= x1 = x1
                       
                       a12(a34(x1)) = x1 >= x1 = a34(a12(x1))
                       
                       a12(a45(x1)) = x1 >= x1 = a45(a12(x1))
                       
                       a12(a56(x1)) = x1 + 1 >= x1 + 1 = a56(a12(x1))
                       
                       a23(a45(x1)) = x1 >= x1 = a45(a23(x1))
                       
                       a23(a56(x1)) = x1 + 1 >= x1 + 1 = a56(a23(x1))
                       
                       a34(a56(x1)) = x1 + 1 >= x1 + 1 = a56(a34(x1))
                       
                       a16(a16(x1)) = x1 + 2 >= x1 = x1
                       
                       a16(x1) = x1 + 1 >= x1 + 1 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
                       
                       a14(a14(x1)) = x1 >= x1 = x1
                       
                       a14(x1) = x1 >= x1 = a12(a23(a34(a23(a12(x1)))))
                       
                       a24(a24(x1)) = x1 >= x1 = x1
                       
                       a24(x1) = x1 >= x1 = a23(a34(a23(x1)))
                       
                       a46(a46(x1)) = x1 + 2 >= x1 = x1
                       
                       a46(x1) = x1 + 1 >= x1 + 1 = a45(a56(a45(x1)))
                       
                       a25(a25(x1)) = x1 >= x1 = x1
                       
                       a56(a56(x1)) = x1 + 2 >= x1 = x1
                       
                       a25(x1) = x1 >= x1 = a23(a34(a45(a34(a23(x1)))))
                       
                       a45(a56(a45(a56(a45(a56(x1)))))) = x1 + 3 >= x1 = x1
                       
                       a12(a12(x1)) = x1 >= x1 = x1
                       
                       a12(a23(a12(a23(a12(a23(x1)))))) = x1 >= x1 = x1
                       
                       a35(a35(x1)) = x1 + 2 >= x1 = x1
                       
                       a35(x1) = x1 + 1 >= x1 = a34(a45(a34(x1)))
                       
                       a36(a36(x1)) = x1 + 2 >= x1 = x1
                       
                       a36(x1) = x1 + 1 >= x1 + 1 = a34(a45(a56(a45(a34(x1)))))
                       
                       a26(a26(x1)) = x1 + 2 >= x1 = x1
                       
                       a26(x1) = x1 + 1 >= x1 + 1 = a23(a34(a45(a56(a45(a34(a23(x1)))))))
                      problem:
                       strict:
                        a13(a13(x1)) -> x1
                        a23(a23(x1)) -> x1
                        a34(a34(x1)) -> x1
                        a45(a45(x1)) -> x1
                        a13(x1) -> a12(a23(a12(x1)))
                        a23(a34(a23(a34(a23(a34(x1)))))) -> x1
                        a34(a45(a34(a45(a34(a45(x1)))))) -> x1
                        a12(a34(x1)) -> a34(a12(x1))
                        a12(a45(x1)) -> a45(a12(x1))
                        a12(a56(x1)) -> a56(a12(x1))
                        a23(a45(x1)) -> a45(a23(x1))
                        a23(a56(x1)) -> a56(a23(x1))
                        a34(a56(x1)) -> a56(a34(x1))
                       weak:
                        a15(a15(x1)) -> x1
                        a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1)))))))
                        a16(a16(x1)) -> x1
                        a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
                        a14(a14(x1)) -> x1
                        a14(x1) -> a12(a23(a34(a23(a12(x1)))))
                        a24(a24(x1)) -> x1
                        a24(x1) -> a23(a34(a23(x1)))
                        a46(a46(x1)) -> x1
                        a46(x1) -> a45(a56(a45(x1)))
                        a25(a25(x1)) -> x1
                        a56(a56(x1)) -> x1
                        a25(x1) -> a23(a34(a45(a34(a23(x1)))))
                        a45(a56(a45(a56(a45(a56(x1)))))) -> x1
                        a12(a12(x1)) -> x1
                        a12(a23(a12(a23(a12(a23(x1)))))) -> x1
                        a35(a35(x1)) -> x1
                        a35(x1) -> a34(a45(a34(x1)))
                        a36(a36(x1)) -> x1
                        a36(x1) -> a34(a45(a56(a45(a34(x1)))))
                        a26(a26(x1)) -> x1
                        a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1)))))))
                      Matrix Interpretation Processor:
                       dimension: 1
                       max_matrix:
                        1
                        interpretation:
                         [a56](x0) = x0,
                         
                         [a46](x0) = x0 + 1,
                         
                         [a45](x0) = x0,
                         
                         [a36](x0) = x0,
                         
                         [a35](x0) = x0,
                         
                         [a34](x0) = x0,
                         
                         [a26](x0) = x0 + 1,
                         
                         [a25](x0) = x0,
                         
                         [a24](x0) = x0,
                         
                         [a23](x0) = x0,
                         
                         [a16](x0) = x0,
                         
                         [a15](x0) = x0,
                         
                         [a14](x0) = x0,
                         
                         [a13](x0) = x0 + 1,
                         
                         [a12](x0) = x0
                        orientation:
                         a13(a13(x1)) = x1 + 2 >= x1 = x1
                         
                         a23(a23(x1)) = x1 >= x1 = x1
                         
                         a34(a34(x1)) = x1 >= x1 = x1
                         
                         a45(a45(x1)) = x1 >= x1 = x1
                         
                         a13(x1) = x1 + 1 >= x1 = a12(a23(a12(x1)))
                         
                         a23(a34(a23(a34(a23(a34(x1)))))) = x1 >= x1 = x1
                         
                         a34(a45(a34(a45(a34(a45(x1)))))) = x1 >= x1 = x1
                         
                         a12(a34(x1)) = x1 >= x1 = a34(a12(x1))
                         
                         a12(a45(x1)) = x1 >= x1 = a45(a12(x1))
                         
                         a12(a56(x1)) = x1 >= x1 = a56(a12(x1))
                         
                         a23(a45(x1)) = x1 >= x1 = a45(a23(x1))
                         
                         a23(a56(x1)) = x1 >= x1 = a56(a23(x1))
                         
                         a34(a56(x1)) = x1 >= x1 = a56(a34(x1))
                         
                         a15(a15(x1)) = x1 >= x1 = x1
                         
                         a15(x1) = x1 >= x1 = a12(a23(a34(a45(a34(a23(a12(x1)))))))
                         
                         a16(a16(x1)) = x1 >= x1 = x1
                         
                         a16(x1) = x1 >= x1 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
                         
                         a14(a14(x1)) = x1 >= x1 = x1
                         
                         a14(x1) = x1 >= x1 = a12(a23(a34(a23(a12(x1)))))
                         
                         a24(a24(x1)) = x1 >= x1 = x1
                         
                         a24(x1) = x1 >= x1 = a23(a34(a23(x1)))
                         
                         a46(a46(x1)) = x1 + 2 >= x1 = x1
                         
                         a46(x1) = x1 + 1 >= x1 = a45(a56(a45(x1)))
                         
                         a25(a25(x1)) = x1 >= x1 = x1
                         
                         a56(a56(x1)) = x1 >= x1 = x1
                         
                         a25(x1) = x1 >= x1 = a23(a34(a45(a34(a23(x1)))))
                         
                         a45(a56(a45(a56(a45(a56(x1)))))) = x1 >= x1 = x1
                         
                         a12(a12(x1)) = x1 >= x1 = x1
                         
                         a12(a23(a12(a23(a12(a23(x1)))))) = x1 >= x1 = x1
                         
                         a35(a35(x1)) = x1 >= x1 = x1
                         
                         a35(x1) = x1 >= x1 = a34(a45(a34(x1)))
                         
                         a36(a36(x1)) = x1 >= x1 = x1
                         
                         a36(x1) = x1 >= x1 = a34(a45(a56(a45(a34(x1)))))
                         
                         a26(a26(x1)) = x1 + 2 >= x1 = x1
                         
                         a26(x1) = x1 + 1 >= x1 = a23(a34(a45(a56(a45(a34(a23(x1)))))))
                        problem:
                         strict:
                          a23(a23(x1)) -> x1
                          a34(a34(x1)) -> x1
                          a45(a45(x1)) -> x1
                          a23(a34(a23(a34(a23(a34(x1)))))) -> x1
                          a34(a45(a34(a45(a34(a45(x1)))))) -> x1
                          a12(a34(x1)) -> a34(a12(x1))
                          a12(a45(x1)) -> a45(a12(x1))
                          a12(a56(x1)) -> a56(a12(x1))
                          a23(a45(x1)) -> a45(a23(x1))
                          a23(a56(x1)) -> a56(a23(x1))
                          a34(a56(x1)) -> a56(a34(x1))
                         weak:
                          a13(a13(x1)) -> x1
                          a13(x1) -> a12(a23(a12(x1)))
                          a15(a15(x1)) -> x1
                          a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1)))))))
                          a16(a16(x1)) -> x1
                          a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
                          a14(a14(x1)) -> x1
                          a14(x1) -> a12(a23(a34(a23(a12(x1)))))
                          a24(a24(x1)) -> x1
                          a24(x1) -> a23(a34(a23(x1)))
                          a46(a46(x1)) -> x1
                          a46(x1) -> a45(a56(a45(x1)))
                          a25(a25(x1)) -> x1
                          a56(a56(x1)) -> x1
                          a25(x1) -> a23(a34(a45(a34(a23(x1)))))
                          a45(a56(a45(a56(a45(a56(x1)))))) -> x1
                          a12(a12(x1)) -> x1
                          a12(a23(a12(a23(a12(a23(x1)))))) -> x1
                          a35(a35(x1)) -> x1
                          a35(x1) -> a34(a45(a34(x1)))
                          a36(a36(x1)) -> x1
                          a36(x1) -> a34(a45(a56(a45(a34(x1)))))
                          a26(a26(x1)) -> x1
                          a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1)))))))
                        Open