YES

Problem:
 op(i(x),op(y,z)) -> op(x,op(i(i(y)),z))
 op(i(x),op(y,op(z,w))) -> op(x,op(z,op(y,w)))
 i(x) -> x

Proof:
 KBO Processor:
  weight function:
   w0 = 1
   w(op) = w(i) = 0
  precedence:
   i > op
  problem:
   
  Qed