fof(reflexivity,conjecture,! [X] : r1(X,X) ).
fof(transitivity,conjecture,! [X] : ! [Y] : ! [Z] : ( ( r1(X,Y) & r1(Y,Z) ) => r1(X,Z) ) ).
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) ) ) )).
