fof(reflexivity,conjecture,! [X] : r1(X,X) ).
fof(main,conjecture,~(~ ( ? [X] : ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ p1(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) & ~ p1(X) ) | p1(X) ) ) )).
