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:
 Complexity 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
   max_matrix:
    1
    interpretation:
     [i](x0) = x0,
     
     [e] = 0,
     
     [:](x0, x1) = x0 + x1 + 1
    orientation:
     :(x,x) = 2x + 1 >= 0 = e()
     
     :(x,e()) = x + 1 >= x = x
     
     i(:(x,y)) = x + y + 1 >= x + y + 1 = :(y,x)
     
     :(:(x,y),z) = x + y + z + 2 >= x + y + z + 2 = :(x,:(z,i(y)))
     
     :(e(),x) = x + 1 >= x = i(x)
     
     i(i(x)) = x >= x = x
     
     i(e()) = 0 >= 0 = e()
     
     :(x,:(y,i(x))) = 2x + y + 2 >= y = i(y)
     
     :(x,:(y,:(i(x),z))) = 2x + y + z + 3 >= y + z + 1 = :(i(z),y)
     
     :(i(x),:(y,x)) = 2x + y + 2 >= y = i(y)
     
     :(i(x),:(y,:(x,z))) = 2x + y + z + 3 >= y + z + 1 = :(i(z),y)
    problem:
     strict:
      i(:(x,y)) -> :(y,x)
      :(:(x,y),z) -> :(x,:(z,i(y)))
      i(i(x)) -> x
      i(e()) -> e()
     weak:
      :(x,x) -> e()
      :(x,e()) -> x
      :(e(),x) -> i(x)
      :(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