MAYBE

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

Proof:
 RT Transformation Processor:
  strict:
   f(a(),x) -> f(b(),f(c(),x))
   f(a(),f(b(),x)) -> f(b(),f(a(),x))
   f(d(),f(c(),x)) -> f(d(),f(a(),x))
   f(a(),f(c(),x)) -> f(c(),f(a(),x))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [d] = 16,
    
    [c] = 0,
    
    [b] = 5,
    
    [f](x0, x1) = x0 + x1,
    
    [a] = 10
   orientation:
    f(a(),x) = x + 10 >= x + 5 = f(b(),f(c(),x))
    
    f(a(),f(b(),x)) = x + 15 >= x + 15 = f(b(),f(a(),x))
    
    f(d(),f(c(),x)) = x + 16 >= x + 26 = f(d(),f(a(),x))
    
    f(a(),f(c(),x)) = x + 10 >= x + 10 = f(c(),f(a(),x))
   problem:
    strict:
     f(a(),f(b(),x)) -> f(b(),f(a(),x))
     f(d(),f(c(),x)) -> f(d(),f(a(),x))
     f(a(),f(c(),x)) -> f(c(),f(a(),x))
    weak:
     f(a(),x) -> f(b(),f(c(),x))
   Open