MAYBE

Problem:
 :(x,x) -> e()
 :(x,e()) -> x
 i(:(x,y)) -> :(y,x)
 :(:(x,y),z) -> :(x,:(z,i(y)))
 :(e(),x) -> i(x)
 i(i(x)) -> x
 i(e()) -> e()
 :(x,:(y,i(x))) -> i(y)
 :(x,:(y,:(i(x),z))) -> :(i(z),y)
 :(i(x),:(y,x)) -> i(y)
 :(i(x),:(y,:(x,z))) -> :(i(z),y)

Proof:
 RT Transformation Processor:
  strict:
   :(x,x) -> e()
   :(x,e()) -> x
   i(:(x,y)) -> :(y,x)
   :(:(x,y),z) -> :(x,:(z,i(y)))
   :(e(),x) -> i(x)
   i(i(x)) -> x
   i(e()) -> e()
   :(x,:(y,i(x))) -> i(y)
   :(x,:(y,:(i(x),z))) -> :(i(z),y)
   :(i(x),:(y,x)) -> i(y)
   :(i(x),:(y,:(x,z))) -> :(i(z),y)
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [i](x0) = x0 + 23,
    
    [e] = 12,
    
    [:](x0, x1) = x0 + x1 + 1
   orientation:
    :(x,x) = 2x + 1 >= 12 = e()
    
    :(x,e()) = x + 13 >= x = x
    
    i(:(x,y)) = x + y + 24 >= x + y + 1 = :(y,x)
    
    :(:(x,y),z) = x + y + z + 2 >= x + y + z + 25 = :(x,:(z,i(y)))
    
    :(e(),x) = x + 13 >= x + 23 = i(x)
    
    i(i(x)) = x + 46 >= x = x
    
    i(e()) = 35 >= 12 = e()
    
    :(x,:(y,i(x))) = 2x + y + 25 >= y + 23 = i(y)
    
    :(x,:(y,:(i(x),z))) = 2x + y + z + 26 >= y + z + 24 = :(i(z),y)
    
    :(i(x),:(y,x)) = 2x + y + 25 >= y + 23 = i(y)
    
    :(i(x),:(y,:(x,z))) = 2x + y + z + 26 >= y + z + 24 = :(i(z),y)
   problem:
    strict:
     :(x,x) -> e()
     :(:(x,y),z) -> :(x,:(z,i(y)))
     :(e(),x) -> i(x)
    weak:
     :(x,e()) -> x
     i(:(x,y)) -> :(y,x)
     i(i(x)) -> x
     i(e()) -> e()
     :(x,:(y,i(x))) -> i(y)
     :(x,:(y,:(i(x),z))) -> :(i(z),y)
     :(i(x),:(y,x)) -> i(y)
     :(i(x),:(y,:(x,z))) -> :(i(z),y)
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [i](x0) = x0 + 9,
     
     [e] = 26,
     
     [:](x0, x1) = x0 + x1 + 9
    orientation:
     :(x,x) = 2x + 9 >= 26 = e()
     
     :(:(x,y),z) = x + y + z + 18 >= x + y + z + 27 = :(x,:(z,i(y)))
     
     :(e(),x) = x + 35 >= x + 9 = i(x)
     
     :(x,e()) = x + 35 >= x = x
     
     i(:(x,y)) = x + y + 18 >= x + y + 9 = :(y,x)
     
     i(i(x)) = x + 18 >= x = x
     
     i(e()) = 35 >= 26 = e()
     
     :(x,:(y,i(x))) = 2x + y + 27 >= y + 9 = i(y)
     
     :(x,:(y,:(i(x),z))) = 2x + y + z + 36 >= y + z + 18 = :(i(z),y)
     
     :(i(x),:(y,x)) = 2x + y + 27 >= y + 9 = i(y)
     
     :(i(x),:(y,:(x,z))) = 2x + y + z + 36 >= y + z + 18 = :(i(z),y)
    problem:
     strict:
      :(x,x) -> e()
      :(:(x,y),z) -> :(x,:(z,i(y)))
     weak:
      :(e(),x) -> i(x)
      :(x,e()) -> x
      i(:(x,y)) -> :(y,x)
      i(i(x)) -> x
      i(e()) -> e()
      :(x,:(y,i(x))) -> i(y)
      :(x,:(y,:(i(x),z))) -> :(i(z),y)
      :(i(x),:(y,x)) -> i(y)
      :(i(x),:(y,:(x,z))) -> :(i(z),y)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [i](x0) = x0 + 11,
      
      [e] = 5,
      
      [:](x0, x1) = x0 + x1 + 10
     orientation:
      :(x,x) = 2x + 10 >= 5 = e()
      
      :(:(x,y),z) = x + y + z + 20 >= x + y + z + 31 = :(x,:(z,i(y)))
      
      :(e(),x) = x + 15 >= x + 11 = i(x)
      
      :(x,e()) = x + 15 >= x = x
      
      i(:(x,y)) = x + y + 21 >= x + y + 10 = :(y,x)
      
      i(i(x)) = x + 22 >= x = x
      
      i(e()) = 16 >= 5 = e()
      
      :(x,:(y,i(x))) = 2x + y + 31 >= y + 11 = i(y)
      
      :(x,:(y,:(i(x),z))) = 2x + y + z + 41 >= y + z + 21 = :(i(z),y)
      
      :(i(x),:(y,x)) = 2x + y + 31 >= y + 11 = i(y)
      
      :(i(x),:(y,:(x,z))) = 2x + y + z + 41 >= y + z + 21 = :(i(z),y)
     problem:
      strict:
       :(:(x,y),z) -> :(x,:(z,i(y)))
      weak:
       :(x,x) -> e()
       :(e(),x) -> i(x)
       :(x,e()) -> x
       i(:(x,y)) -> :(y,x)
       i(i(x)) -> x
       i(e()) -> e()
       :(x,:(y,i(x))) -> i(y)
       :(x,:(y,:(i(x),z))) -> :(i(z),y)
       :(i(x),:(y,x)) -> i(y)
       :(i(x),:(y,:(x,z))) -> :(i(z),y)
     Open