MAYBE

Problem:
 r(e(x1)) -> w(r(x1))
 i(t(x1)) -> e(r(x1))
 e(w(x1)) -> r(i(x1))
 t(e(x1)) -> r(e(x1))
 w(r(x1)) -> i(t(x1))
 e(r(x1)) -> e(w(x1))
 r(i(t(e(r(x1))))) -> e(w(r(i(t(e(x1))))))

Proof:
 RT Transformation Processor:
  strict:
   r(e(x1)) -> w(r(x1))
   i(t(x1)) -> e(r(x1))
   e(w(x1)) -> r(i(x1))
   t(e(x1)) -> r(e(x1))
   w(r(x1)) -> i(t(x1))
   e(r(x1)) -> e(w(x1))
   r(i(t(e(r(x1))))) -> e(w(r(i(t(e(x1))))))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [i](x0) = x0,
    
    [t](x0) = x0 + 1,
    
    [w](x0) = x0 + 6,
    
    [r](x0) = x0 + 21,
    
    [e](x0) = x0 + 14
   orientation:
    r(e(x1)) = x1 + 35 >= x1 + 27 = w(r(x1))
    
    i(t(x1)) = x1 + 1 >= x1 + 35 = e(r(x1))
    
    e(w(x1)) = x1 + 20 >= x1 + 21 = r(i(x1))
    
    t(e(x1)) = x1 + 15 >= x1 + 35 = r(e(x1))
    
    w(r(x1)) = x1 + 27 >= x1 + 1 = i(t(x1))
    
    e(r(x1)) = x1 + 35 >= x1 + 20 = e(w(x1))
    
    r(i(t(e(r(x1))))) = x1 + 57 >= x1 + 56 = e(w(r(i(t(e(x1))))))
   problem:
    strict:
     i(t(x1)) -> e(r(x1))
     e(w(x1)) -> r(i(x1))
     t(e(x1)) -> r(e(x1))
    weak:
     r(e(x1)) -> w(r(x1))
     w(r(x1)) -> i(t(x1))
     e(r(x1)) -> e(w(x1))
     r(i(t(e(r(x1))))) -> e(w(r(i(t(e(x1))))))
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [i](x0) = x0,
     
     [t](x0) = x0 + 3,
     
     [w](x0) = x0 + 1,
     
     [r](x0) = x0 + 2,
     
     [e](x0) = x0 + 1
    orientation:
     i(t(x1)) = x1 + 3 >= x1 + 3 = e(r(x1))
     
     e(w(x1)) = x1 + 2 >= x1 + 2 = r(i(x1))
     
     t(e(x1)) = x1 + 4 >= x1 + 3 = r(e(x1))
     
     r(e(x1)) = x1 + 3 >= x1 + 3 = w(r(x1))
     
     w(r(x1)) = x1 + 3 >= x1 + 3 = i(t(x1))
     
     e(r(x1)) = x1 + 3 >= x1 + 2 = e(w(x1))
     
     r(i(t(e(r(x1))))) = x1 + 8 >= x1 + 8 = e(w(r(i(t(e(x1))))))
    problem:
     strict:
      i(t(x1)) -> e(r(x1))
      e(w(x1)) -> r(i(x1))
     weak:
      t(e(x1)) -> r(e(x1))
      r(e(x1)) -> w(r(x1))
      w(r(x1)) -> i(t(x1))
      e(r(x1)) -> e(w(x1))
      r(i(t(e(r(x1))))) -> e(w(r(i(t(e(x1))))))
    Matrix Interpretation Processor:
     dimension: 3
     interpretation:
                [1 0 0]  
      [i](x0) = [0 0 1]x0
                [0 0 0]  ,
      
                [1 4 4]     [1]
      [t](x0) = [0 0 0]x0 + [1]
                [0 0 0]     [1],
      
                [1 1 4]     [0]
      [w](x0) = [0 0 0]x0 + [1]
                [0 0 0]     [0],
      
                [1 4 4]     [0]
      [r](x0) = [0 0 0]x0 + [1]
                [0 0 0]     [0],
      
                [1 0 4]     [1]
      [e](x0) = [0 1 0]x0 + [0]
                [0 0 0]     [0]
     orientation:
                 [1 4 4]     [1]    [1 4 4]     [1]           
      i(t(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = e(r(x1))
                 [0 0 0]     [0]    [0 0 0]     [0]           
      
                 [1 1 4]     [1]    [1 0 4]     [0]           
      e(w(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = r(i(x1))
                 [0 0 0]     [0]    [0 0 0]     [0]           
      
                 [1 4 4]     [2]    [1 4 4]     [1]           
      t(e(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = r(e(x1))
                 [0 0 0]     [1]    [0 0 0]     [0]           
      
                 [1 4 4]     [1]    [1 4 4]     [1]           
      r(e(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = w(r(x1))
                 [0 0 0]     [0]    [0 0 0]     [0]           
      
                 [1 4 4]     [1]    [1 4 4]     [1]           
      w(r(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = i(t(x1))
                 [0 0 0]     [0]    [0 0 0]     [0]           
      
                 [1 4 4]     [1]    [1 1 4]     [1]           
      e(r(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = e(w(x1))
                 [0 0 0]     [0]    [0 0 0]     [0]           
      
                          [1 4 4]     [10]    [1 4 4]     [8]                       
      r(i(t(e(r(x1))))) = [0 0 0]x1 + [1 ] >= [0 0 0]x1 + [1] = e(w(r(i(t(e(x1))))))
                          [0 0 0]     [0 ]    [0 0 0]     [0]                       
     problem:
      strict:
       i(t(x1)) -> e(r(x1))
      weak:
       e(w(x1)) -> r(i(x1))
       t(e(x1)) -> r(e(x1))
       r(e(x1)) -> w(r(x1))
       w(r(x1)) -> i(t(x1))
       e(r(x1)) -> e(w(x1))
       r(i(t(e(r(x1))))) -> e(w(r(i(t(e(x1))))))
     Open