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