MAYBE

Problem:
 f(s(x)) -> s(f(f(p(s(x)))))
 f(0()) -> 0()
 p(s(x)) -> x

Proof:
 RT Transformation Processor:
  strict:
   f(s(x)) -> s(f(f(p(s(x)))))
   f(0()) -> 0()
   p(s(x)) -> x
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [0] = 0,
    
    [p](x0) = x0 + 10,
    
    [f](x0) = x0 + 24,
    
    [s](x0) = x0 + 1
   orientation:
    f(s(x)) = x + 25 >= x + 60 = s(f(f(p(s(x)))))
    
    f(0()) = 24 >= 0 = 0()
    
    p(s(x)) = x + 11 >= x = x
   problem:
    strict:
     f(s(x)) -> s(f(f(p(s(x)))))
    weak:
     f(0()) -> 0()
     p(s(x)) -> x
   Open