(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))) )