(VAR x0 x1 x2 x3)
(RULES
  p(p(b(a(x0)),x1),p(x2,x3)) -> p(p(x3,a(x2)),p(b(a(x1)),b(x0)))
)