MAYBE

Problem:
 g(x,x) -> g(a(),b())
 g(c(),g(c(),x)) -> g(e(),g(d(),x))
 g(d(),g(d(),x)) -> g(c(),g(e(),x))
 g(e(),g(e(),x)) -> g(d(),g(c(),x))
 f(g(x,y)) -> g(y,g(f(f(x)),a()))

Proof:
 RT Transformation Processor:
  strict:
   g(x,x) -> g(a(),b())
   g(c(),g(c(),x)) -> g(e(),g(d(),x))
   g(d(),g(d(),x)) -> g(c(),g(e(),x))
   g(e(),g(e(),x)) -> g(d(),g(c(),x))
   f(g(x,y)) -> g(y,g(f(f(x)),a()))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [f](x0) = x0 + 1,
    
    [d] = 0,
    
    [e] = 7,
    
    [c] = 24,
    
    [b] = 26,
    
    [a] = 18,
    
    [g](x0, x1) = x0 + x1
   orientation:
    g(x,x) = 2x >= 44 = g(a(),b())
    
    g(c(),g(c(),x)) = x + 48 >= x + 7 = g(e(),g(d(),x))
    
    g(d(),g(d(),x)) = x >= x + 31 = g(c(),g(e(),x))
    
    g(e(),g(e(),x)) = x + 14 >= x + 24 = g(d(),g(c(),x))
    
    f(g(x,y)) = x + y + 1 >= x + y + 20 = g(y,g(f(f(x)),a()))
   problem:
    strict:
     g(x,x) -> g(a(),b())
     g(d(),g(d(),x)) -> g(c(),g(e(),x))
     g(e(),g(e(),x)) -> g(d(),g(c(),x))
     f(g(x,y)) -> g(y,g(f(f(x)),a()))
    weak:
     g(c(),g(c(),x)) -> g(e(),g(d(),x))
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [f](x0) = x0 + 16,
     
     [d] = 3,
     
     [e] = 8,
     
     [c] = 8,
     
     [b] = 13,
     
     [a] = 16,
     
     [g](x0, x1) = x0 + x1 + 1
    orientation:
     g(x,x) = 2x + 1 >= 30 = g(a(),b())
     
     g(d(),g(d(),x)) = x + 8 >= x + 18 = g(c(),g(e(),x))
     
     g(e(),g(e(),x)) = x + 18 >= x + 13 = g(d(),g(c(),x))
     
     f(g(x,y)) = x + y + 17 >= x + y + 50 = g(y,g(f(f(x)),a()))
     
     g(c(),g(c(),x)) = x + 18 >= x + 13 = g(e(),g(d(),x))
    problem:
     strict:
      g(x,x) -> g(a(),b())
      g(d(),g(d(),x)) -> g(c(),g(e(),x))
      f(g(x,y)) -> g(y,g(f(f(x)),a()))
     weak:
      g(e(),g(e(),x)) -> g(d(),g(c(),x))
      g(c(),g(c(),x)) -> g(e(),g(d(),x))
    Open