include('Saturations/LCL681+1.015/Saturations/iProver-SAT---3.7.CSA-Sat.s.ax').
fof(main,conjecture,~(~ ( ? [X] : ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p2(X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( p2(Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) | p1(X) ) ) )).
