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