MAYBE

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

Proof:
 RT Transformation Processor:
  strict:
   f(a(),f(a(),f(b(),f(x,y)))) -> f(b(),f(c(),f(b(),f(a(),f(a(),f(a(),f(x,y)))))))
   f(a(),f(c(),f(x,y))) -> f(b(),f(x,y))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [c] = 16,
    
    [f](x0, x1) = x0 + x1 + 1,
    
    [b] = 14,
    
    [a] = 0
   orientation:
    f(a(),f(a(),f(b(),f(x,y)))) = x + y + 18 >= x + y + 51 = f(b(),f(c(),f(b(),f(a(),f(a(),f(a(),f(x,y)))))))
    
    f(a(),f(c(),f(x,y))) = x + y + 19 >= x + y + 16 = f(b(),f(x,y))
   problem:
    strict:
     f(a(),f(a(),f(b(),f(x,y)))) -> f(b(),f(c(),f(b(),f(a(),f(a(),f(a(),f(x,y)))))))
    weak:
     f(a(),f(c(),f(x,y))) -> f(b(),f(x,y))
   Open