MAYBE

Problem:
 g(c(x1)) -> g(f(c(x1)))
 g(f(c(x1))) -> g(f(f(c(x1))))
 g(g(x1)) -> g(f(g(x1)))
 f(f(g(x1))) -> g(f(x1))

Proof:
 RT Transformation Processor:
  strict:
   g(c(x1)) -> g(f(c(x1)))
   g(f(c(x1))) -> g(f(f(c(x1))))
   g(g(x1)) -> g(f(g(x1)))
   f(f(g(x1))) -> g(f(x1))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [f](x0) = x0 + 7,
    
    [g](x0) = x0 + 1,
    
    [c](x0) = x0 + 28
   orientation:
    g(c(x1)) = x1 + 29 >= x1 + 36 = g(f(c(x1)))
    
    g(f(c(x1))) = x1 + 36 >= x1 + 43 = g(f(f(c(x1))))
    
    g(g(x1)) = x1 + 2 >= x1 + 9 = g(f(g(x1)))
    
    f(f(g(x1))) = x1 + 15 >= x1 + 8 = g(f(x1))
   problem:
    strict:
     g(c(x1)) -> g(f(c(x1)))
     g(f(c(x1))) -> g(f(f(c(x1))))
     g(g(x1)) -> g(f(g(x1)))
    weak:
     f(f(g(x1))) -> g(f(x1))
   Matrix Interpretation Processor:
    dimension: 2
    interpretation:
               [1 0]  
     [f](x0) = [0 0]x0,
     
               [1 8]  
     [g](x0) = [0 1]x0,
     
               [1 3]     [9]
     [c](x0) = [0 0]x0 + [1]
    orientation:
                [1 3]     [17]    [1 3]     [9]              
     g(c(x1)) = [0 0]x1 + [1 ] >= [0 0]x1 + [0] = g(f(c(x1)))
     
                   [1 3]     [9]    [1 3]     [9]                 
     g(f(c(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = g(f(f(c(x1))))
     
                [1  16]      [1 8]                
     g(g(x1)) = [0  1 ]x1 >= [0 0]x1 = g(f(g(x1)))
     
                   [1 8]      [1 0]             
     f(f(g(x1))) = [0 0]x1 >= [0 0]x1 = g(f(x1))
    problem:
     strict:
      g(f(c(x1))) -> g(f(f(c(x1))))
      g(g(x1)) -> g(f(g(x1)))
     weak:
      g(c(x1)) -> g(f(c(x1)))
      f(f(g(x1))) -> g(f(x1))
    Matrix Interpretation Processor:
     dimension: 3
     interpretation:
                [1 0 0]  
      [f](x0) = [0 0 1]x0
                [0 0 0]  ,
      
                [1 2 2]  
      [g](x0) = [0 0 0]x0
                [0 0 0]  ,
      
                [1 2 1]     [0]
      [c](x0) = [0 0 0]x0 + [5]
                [0 0 0]     [2]
     orientation:
                    [1 2 1]     [4]    [1 2 1]                   
      g(f(c(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = g(f(f(c(x1))))
                    [0 0 0]     [0]    [0 0 0]                   
      
                 [1 2 2]      [1 2 2]                
      g(g(x1)) = [0 0 0]x1 >= [0 0 0]x1 = g(f(g(x1)))
                 [0 0 0]      [0 0 0]                
      
                 [1 2 1]     [14]    [1 2 1]     [4]              
      g(c(x1)) = [0 0 0]x1 + [0 ] >= [0 0 0]x1 + [0] = g(f(c(x1)))
                 [0 0 0]     [0 ]    [0 0 0]     [0]              
      
                    [1 2 2]      [1 0 2]             
      f(f(g(x1))) = [0 0 0]x1 >= [0 0 0]x1 = g(f(x1))
                    [0 0 0]      [0 0 0]             
     problem:
      strict:
       g(g(x1)) -> g(f(g(x1)))
      weak:
       g(f(c(x1))) -> g(f(f(c(x1))))
       g(c(x1)) -> g(f(c(x1)))
       f(f(g(x1))) -> g(f(x1))
     Open