include('Saturations/LCL665+1.020/Saturations/iProver-SAT---3.7.CSA-Sat.s.ax').
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) | p216(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | p212(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | p214(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | p212(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p216(Y) ) & ~ p206(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p216(Y) ) & ~ p204(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p216(Y) ) & ~ p202(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p214(Y) ) & ~ p206(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p214(Y) ) & ~ p204(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p214(Y) ) & ~ p202(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p212(Y) ) & ~ p206(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p212(Y) ) & ~ p204(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p212(Y) ) & ~ p202(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p206(X) ) & ~ p196(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p206(X) ) & ~ p194(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p215(Y) ) & ~ p205(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p212(Y) ) & ~ p205(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p213(Y) ) & ~ p205(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p211(Y) ) & ~ p205(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p204(X) ) & ~ p196(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p204(X) ) & ~ p194(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p215(Y) ) & ~ p203(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p213(Y) ) & ~ p203(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p211(Y) ) & ~ p203(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p202(X) ) & ~ p196(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p202(X) ) & ~ p194(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p215(Y) ) & ~ p201(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p213(Y) ) & ~ p201(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p211(Y) ) & ~ p201(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p196(Y) ) & ~ p186(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p196(Y) ) & ~ p184(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p196(Y) ) & ~ p182(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p203(X) ) & ~ p195(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p201(X) ) & ~ p195(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p194(Y) ) & ~ p186(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p194(Y) ) & ~ p184(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p194(Y) ) & ~ p182(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p203(X) ) & ~ p193(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p201(X) ) & ~ p193(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p192(Y) ) & ~ p186(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p192(Y) ) & ~ p184(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p192(Y) ) & ~ p182(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p205(X) ) & ~ p192(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p203(X) ) & ~ p191(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p201(X) ) & ~ p191(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p186(X) ) & ~ p176(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p186(X) ) & ~ p174(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p195(Y) ) & ~ p185(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p192(Y) ) & ~ p185(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p193(Y) ) & ~ p185(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p191(Y) ) & ~ p185(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p184(X) ) & ~ p176(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p184(X) ) & ~ p174(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p195(Y) ) & ~ p183(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p193(Y) ) & ~ p183(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p191(Y) ) & ~ p183(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p182(X) ) & ~ p176(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p182(X) ) & ~ p174(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p195(Y) ) & ~ p181(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p193(Y) ) & ~ p181(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p191(Y) ) & ~ p181(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p176(Y) ) & ~ p166(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p176(Y) ) & ~ p164(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p176(Y) ) & ~ p162(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p183(X) ) & ~ p175(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p181(X) ) & ~ p175(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p174(Y) ) & ~ p166(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p174(Y) ) & ~ p164(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p174(Y) ) & ~ p162(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p183(X) ) & ~ p173(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p181(X) ) & ~ p173(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p172(Y) ) & ~ p166(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p172(Y) ) & ~ p164(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p172(Y) ) & ~ p162(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p185(X) ) & ~ p172(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p183(X) ) & ~ p171(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p181(X) ) & ~ p171(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p166(X) ) & ~ p156(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p166(X) ) & ~ p154(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p175(Y) ) & ~ p165(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p172(Y) ) & ~ p165(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p173(Y) ) & ~ p165(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p171(Y) ) & ~ p165(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p164(X) ) & ~ p156(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p164(X) ) & ~ p154(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p175(Y) ) & ~ p163(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p173(Y) ) & ~ p163(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p171(Y) ) & ~ p163(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p162(X) ) & ~ p156(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p162(X) ) & ~ p154(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p175(Y) ) & ~ p161(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p173(Y) ) & ~ p161(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p171(Y) ) & ~ p161(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p156(Y) ) & ~ p146(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p156(Y) ) & ~ p144(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p156(Y) ) & ~ p142(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p163(X) ) & ~ p155(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p161(X) ) & ~ p155(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p154(Y) ) & ~ p146(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p154(Y) ) & ~ p144(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p154(Y) ) & ~ p142(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p163(X) ) & ~ p153(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p161(X) ) & ~ p153(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p152(Y) ) & ~ p146(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p152(Y) ) & ~ p144(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p152(Y) ) & ~ p142(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p165(X) ) & ~ p152(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p163(X) ) & ~ p151(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p161(X) ) & ~ p151(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p146(X) ) & ~ p136(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p146(X) ) & ~ p134(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p155(Y) ) & ~ p145(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p152(Y) ) & ~ p145(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p153(Y) ) & ~ p145(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p151(Y) ) & ~ p145(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p144(X) ) & ~ p136(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p144(X) ) & ~ p134(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p155(Y) ) & ~ p143(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p153(Y) ) & ~ p143(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p151(Y) ) & ~ p143(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p142(X) ) & ~ p136(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p142(X) ) & ~ p134(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p155(Y) ) & ~ p141(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p153(Y) ) & ~ p141(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p151(Y) ) & ~ p141(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p136(Y) ) & ~ p126(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p136(Y) ) & ~ p124(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p136(Y) ) & ~ p122(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p143(X) ) & ~ p135(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p141(X) ) & ~ p135(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p134(Y) ) & ~ p126(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p134(Y) ) & ~ p124(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p134(Y) ) & ~ p122(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p143(X) ) & ~ p133(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p141(X) ) & ~ p133(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p132(Y) ) & ~ p126(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p132(Y) ) & ~ p124(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p132(Y) ) & ~ p122(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p145(X) ) & ~ p132(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p143(X) ) & ~ p131(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p141(X) ) & ~ p131(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p126(X) ) & ~ p116(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p126(X) ) & ~ p114(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p135(Y) ) & ~ p125(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p132(Y) ) & ~ p125(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p133(Y) ) & ~ p125(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p131(Y) ) & ~ p125(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p124(X) ) & ~ p116(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p124(X) ) & ~ p114(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p135(Y) ) & ~ p123(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p133(Y) ) & ~ p123(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p131(Y) ) & ~ p123(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p122(X) ) & ~ p116(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p122(X) ) & ~ p114(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p135(Y) ) & ~ p121(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p133(Y) ) & ~ p121(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p131(Y) ) & ~ p121(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p116(Y) ) & ~ p106(X) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p116(Y) ) & ~ p104(X) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p116(Y) ) & ~ p102(X) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p123(X) ) & ~ p115(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p121(X) ) & ~ p115(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p114(Y) ) & ~ p106(X) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p114(Y) ) & ~ p104(X) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p114(Y) ) & ~ p102(X) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p123(X) ) & ~ p113(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p121(X) ) & ~ p113(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p112(Y) ) & ~ p106(X) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p112(Y) ) & ~ p104(X) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p112(Y) ) & ~ p102(X) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p125(X) ) & ~ p112(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p123(X) ) & ~ p111(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p121(X) ) & ~ p111(Y) ) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p106(X) ) & ~ p94(Y) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p106(X) ) & ~ p92(Y) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p115(Y) ) & ~ p105(X) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p113(Y) ) & ~ p105(X) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p111(Y) ) & ~ p105(X) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p104(X) ) & ~ p94(Y) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p104(X) ) & ~ p92(Y) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p115(Y) ) & ~ p103(X) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p113(Y) ) & ~ p103(X) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p111(Y) ) & ~ p103(X) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p102(X) ) & ~ p94(Y) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p102(X) ) & ~ p92(Y) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p115(Y) ) & ~ p101(X) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p113(Y) ) & ~ p101(X) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p111(Y) ) & ~ p101(X) ) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p96(Y) ) & ~ p86(X) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p96(Y) ) & ~ p84(X) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p96(Y) ) & ~ p82(X) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p105(X) ) & ~ p96(Y) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p103(X) ) & ~ p95(Y) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p101(X) ) & ~ p95(Y) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p94(Y) ) & ~ p86(X) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p94(Y) ) & ~ p84(X) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p94(Y) ) & ~ p82(X) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p103(X) ) & ~ p93(Y) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p101(X) ) & ~ p93(Y) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p92(Y) ) & ~ p86(X) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p92(Y) ) & ~ p84(X) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p92(Y) ) & ~ p82(X) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p103(X) ) & ~ p91(Y) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p101(X) ) & ~ p91(Y) ) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p86(X) ) & ~ p76(Y) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p86(X) ) & ~ p74(Y) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p95(Y) ) & ~ p85(X) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p93(Y) ) & ~ p85(X) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p91(Y) ) & ~ p85(X) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p84(X) ) & ~ p76(Y) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p84(X) ) & ~ p74(Y) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p95(Y) ) & ~ p83(X) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p93(Y) ) & ~ p83(X) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p91(Y) ) & ~ p83(X) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p82(X) ) & ~ p76(Y) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p82(X) ) & ~ p74(Y) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p95(Y) ) & ~ p81(X) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p96(Y) ) & ~ p81(X) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p93(Y) ) & ~ p81(X) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p91(Y) ) & ~ p81(X) ) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p76(Y) ) & ~ p66(X) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p76(Y) ) & ~ p64(X) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p76(Y) ) & ~ p62(X) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p85(X) ) & ~ p75(Y) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p83(X) ) & ~ p75(Y) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p74(Y) ) & ~ p66(X) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p74(Y) ) & ~ p64(X) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p74(Y) ) & ~ p62(X) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p85(X) ) & ~ p73(Y) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p83(X) ) & ~ p73(Y) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p72(Y) ) & ~ p66(X) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p72(Y) ) & ~ p64(X) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p72(Y) ) & ~ p62(X) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p81(X) ) & ~ p72(Y) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p85(X) ) & ~ p71(Y) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p83(X) ) & ~ p71(Y) ) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p66(X) ) & ~ p56(Y) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p66(X) ) & ~ p52(Y) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p75(Y) ) & ~ p65(X) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p73(Y) ) & ~ p65(X) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p71(Y) ) & ~ p65(X) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p64(X) ) & ~ p56(Y) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p64(X) ) & ~ p52(Y) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p75(Y) ) & ~ p63(X) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p72(Y) ) & ~ p63(X) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p73(Y) ) & ~ p63(X) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p71(Y) ) & ~ p63(X) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p62(X) ) & ~ p56(Y) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p62(X) ) & ~ p52(Y) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p75(Y) ) & ~ p61(X) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p73(Y) ) & ~ p61(X) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p71(Y) ) & ~ p61(X) ) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p56(Y) ) & ~ p46(X) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p56(Y) ) & ~ p44(X) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p56(Y) ) & ~ p42(X) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p65(X) ) & ~ p55(Y) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p61(X) ) & ~ p55(Y) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p54(Y) ) & ~ p46(X) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p54(Y) ) & ~ p44(X) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p54(Y) ) & ~ p42(X) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p63(X) ) & ~ p54(Y) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p65(X) ) & ~ p53(Y) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p61(X) ) & ~ p53(Y) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p52(Y) ) & ~ p46(X) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p52(Y) ) & ~ p44(X) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p52(Y) ) & ~ p42(X) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p65(X) ) & ~ p51(Y) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p61(X) ) & ~ p51(Y) ) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p46(X) ) & ~ p34(Y) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p46(X) ) & ~ p32(Y) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p55(Y) ) & ~ p45(X) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p54(Y) ) & ~ p45(X) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p53(Y) ) & ~ p45(X) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p51(Y) ) & ~ p45(X) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p44(X) ) & ~ p34(Y) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p44(X) ) & ~ p32(Y) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p55(Y) ) & ~ p43(X) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p53(Y) ) & ~ p43(X) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p51(Y) ) & ~ p43(X) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p42(X) ) & ~ p34(Y) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p42(X) ) & ~ p32(Y) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p55(Y) ) & ~ p41(X) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p53(Y) ) & ~ p41(X) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p51(Y) ) & ~ p41(X) ) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p36(Y) ) & ~ p26(X) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p36(Y) ) & ~ p24(X) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p36(Y) ) & ~ p22(X) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p45(X) ) & ~ p36(Y) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p43(X) ) & ~ p35(Y) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p41(X) ) & ~ p35(Y) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p34(Y) ) & ~ p26(X) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p34(Y) ) & ~ p24(X) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p34(Y) ) & ~ p22(X) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p43(X) ) & ~ p33(Y) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p41(X) ) & ~ p33(Y) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p32(Y) ) & ~ p26(X) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p32(Y) ) & ~ p24(X) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p32(Y) ) & ~ p22(X) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p43(X) ) & ~ p31(Y) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p41(X) ) & ~ p31(Y) ) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p26(X) ) & ~ p16(Y) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p26(X) ) & ~ p14(Y) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p35(Y) ) & ~ p25(X) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p33(Y) ) & ~ p25(X) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p31(Y) ) & ~ p25(X) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p24(X) ) & ~ p16(Y) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p24(X) ) & ~ p14(Y) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p35(Y) ) & ~ p23(X) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p33(Y) ) & ~ p23(X) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p31(Y) ) & ~ p23(X) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p22(X) ) & ~ p16(Y) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p22(X) ) & ~ p14(Y) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p35(Y) ) & ~ p21(X) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p36(Y) ) & ~ p21(X) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p33(Y) ) & ~ p21(X) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p31(Y) ) & ~ p21(X) ) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p25(X) ) & ~ p15(Y) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p23(X) ) & ~ p15(Y) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p25(X) ) & ~ p13(Y) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p23(X) ) & ~ p13(Y) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p21(X) ) & ~ p12(Y) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p25(X) ) & ~ p11(Y) ) ) ) | ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ! [X] : ( ~ r1(Y,X) | p23(X) ) & ~ p11(Y) ) ) ) | ! [Y] : ( ~ r1(X,Y) | p15(Y) ) | ! [Y] : ( ~ r1(X,Y) | p13(Y) ) | ! [Y] : ( ~ r1(X,Y) | p12(Y) ) | ! [Y] : ( ~ r1(X,Y) | p11(Y) ) ) ) )).
