TRS:
 {       implies(not(x), y) -> or(x, y),
  implies(not(x), or(y, z)) -> implies(y, or(x, z)),
       implies(x, or(y, z)) -> or(y, implies(x, z))}
 Cdiprover:
  Interpretation class: pizerosimplemixed
  Complexity bound: POLYTIME COMPUTABLE
  not(X4) = + 1*X4 + 3
  implies(X3, X2) = + 1*X3^2 + 1*X2^2 + 3*X3 + 0 + 2*X2 + 2*X2*X3
  or(X1, X0) = + 1*X0 + 1*X1 + 3
  
  Qed