fof(reflexivity,conjecture,! [X] : r1(X,X) ).
fof(transitivity,conjecture,! [X] : ! [Y] : ! [Z] : ( ( r1(X,Y) & r1(Y,Z) ) => r1(X,Z) ) ).
fof(main,conjecture,~(~ ( ? [X] : ~ ( ~ ( ! [Y] : ( ~ r1(X,Y) | ~ ( ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1615(X) & p1515(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1615(X) & ! [Y] : ( ~ r1(X,Y) | p1415(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1515(X) & ! [Y] : ( ~ r1(X,Y) | p1415(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1615(X) & ! [Y] : ( ~ r1(X,Y) | p1315(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1515(X) & ! [Y] : ( ~ r1(X,Y) | p1315(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1415(Y) ) & ! [Y] : ( ~ r1(X,Y) | p1315(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1615(X) & ! [Y] : ( ~ r1(X,Y) | p1215(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1515(X) & ! [Y] : ( ~ r1(X,Y) | p1215(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1415(Y) ) & ! [Y] : ( ~ r1(X,Y) | p1215(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1315(Y) ) & ! [Y] : ( ~ r1(X,Y) | p1215(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1615(X) & ! [Y] : ( ~ r1(X,Y) | p1115(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1515(X) & ! [Y] : ( ~ r1(X,Y) | p1115(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1415(Y) ) & ! [Y] : ( ~ r1(X,Y) | p1115(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1315(Y) ) & ! [Y] : ( ~ r1(X,Y) | p1115(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1215(Y) ) & ! [Y] : ( ~ r1(X,Y) | p1115(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1615(X) & ! [Y] : ( ~ r1(X,Y) | p1015(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1515(X) & ! [Y] : ( ~ r1(X,Y) | p1015(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1415(Y) ) & ! [Y] : ( ~ r1(X,Y) | p1015(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1315(Y) ) & ! [Y] : ( ~ r1(X,Y) | p1015(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1215(Y) ) & ! [Y] : ( ~ r1(X,Y) | p1015(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1115(Y) ) & ! [Y] : ( ~ r1(X,Y) | p1015(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1615(X) & ! [Y] : ( ~ r1(X,Y) | p915(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1515(X) & ! [Y] : ( ~ r1(X,Y) | p915(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1415(Y) ) & ! [Y] : ( ~ r1(X,Y) | p915(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1315(Y) ) & ! [Y] : ( ~ r1(X,Y) | p915(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1215(Y) ) & ! [Y] : ( ~ r1(X,Y) | p915(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1115(Y) ) & ! [Y] : ( ~ r1(X,Y) | p915(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1015(Y) ) & ! [Y] : ( ~ r1(X,Y) | p915(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1615(X) & ! [Y] : ( ~ r1(X,Y) | p815(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1515(X) & ! [Y] : ( ~ r1(X,Y) | p815(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1415(Y) ) & ! [Y] : ( ~ r1(X,Y) | p815(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1315(Y) ) & ! [Y] : ( ~ r1(X,Y) | p815(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1215(Y) ) & ! [Y] : ( ~ r1(X,Y) | p815(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1115(Y) ) & ! [Y] : ( ~ r1(X,Y) | p815(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1015(Y) ) & ! [Y] : ( ~ r1(X,Y) | p815(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p915(Y) ) & ! [Y] : ( ~ r1(X,Y) | p815(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1615(X) & ! [Y] : ( ~ r1(X,Y) | p715(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1515(X) & ! [Y] : ( ~ r1(X,Y) | p715(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1415(Y) ) & ! [Y] : ( ~ r1(X,Y) | p715(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1315(Y) ) & ! [Y] : ( ~ r1(X,Y) | p715(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1215(Y) ) & ! [Y] : ( ~ r1(X,Y) | p715(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1115(Y) ) & ! [Y] : ( ~ r1(X,Y) | p715(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1015(Y) ) & ! [Y] : ( ~ r1(X,Y) | p715(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p915(Y) ) & ! [Y] : ( ~ r1(X,Y) | p715(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p815(Y) ) & ! [Y] : ( ~ r1(X,Y) | p715(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1615(X) & ! [Y] : ( ~ r1(X,Y) | p615(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1515(X) & ! [Y] : ( ~ r1(X,Y) | p615(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1415(Y) ) & ! [Y] : ( ~ r1(X,Y) | p615(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1315(Y) ) & ! [Y] : ( ~ r1(X,Y) | p615(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1215(Y) ) & ! [Y] : ( ~ r1(X,Y) | p615(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1115(Y) ) & ! [Y] : ( ~ r1(X,Y) | p615(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1015(Y) ) & ! [Y] : ( ~ r1(X,Y) | p615(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p915(Y) ) & ! [Y] : ( ~ r1(X,Y) | p615(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p815(Y) ) & ! [Y] : ( ~ r1(X,Y) | p615(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p715(Y) ) & ! [Y] : ( ~ r1(X,Y) | p615(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1615(X) & ! [Y] : ( ~ r1(X,Y) | p515(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1515(X) & ! [Y] : ( ~ r1(X,Y) | p515(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1415(Y) ) & ! [Y] : ( ~ r1(X,Y) | p515(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1315(Y) ) & ! [Y] : ( ~ r1(X,Y) | p515(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1215(Y) ) & ! [Y] : ( ~ r1(X,Y) | p515(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1115(Y) ) & ! [Y] : ( ~ r1(X,Y) | p515(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1015(Y) ) & ! [Y] : ( ~ r1(X,Y) | p515(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p915(Y) ) & ! [Y] : ( ~ r1(X,Y) | p515(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p815(Y) ) & ! [Y] : ( ~ r1(X,Y) | p515(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p715(Y) ) & ! [Y] : ( ~ r1(X,Y) | p515(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p615(Y) ) & ! [Y] : ( ~ r1(X,Y) | p515(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1615(X) & ! [Y] : ( ~ r1(X,Y) | p415(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1515(X) & ! [Y] : ( ~ r1(X,Y) | p415(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1415(Y) ) & ! [Y] : ( ~ r1(X,Y) | p415(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1315(Y) ) & ! [Y] : ( ~ r1(X,Y) | p415(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1215(Y) ) & ! [Y] : ( ~ r1(X,Y) | p415(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1115(Y) ) & ! [Y] : ( ~ r1(X,Y) | p415(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1015(Y) ) & ! [Y] : ( ~ r1(X,Y) | p415(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p915(Y) ) & ! [Y] : ( ~ r1(X,Y) | p415(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p815(Y) ) & ! [Y] : ( ~ r1(X,Y) | p415(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p715(Y) ) & ! [Y] : ( ~ r1(X,Y) | p415(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p615(Y) ) & ! [Y] : ( ~ r1(X,Y) | p415(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p515(Y) ) & ! [Y] : ( ~ r1(X,Y) | p415(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1615(X) & ! [Y] : ( ~ r1(X,Y) | p315(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1515(X) & ! [Y] : ( ~ r1(X,Y) | p315(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1415(Y) ) & ! [Y] : ( ~ r1(X,Y) | p315(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1315(Y) ) & ! [Y] : ( ~ r1(X,Y) | p315(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1215(Y) ) & ! [Y] : ( ~ r1(X,Y) | p315(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1115(Y) ) & ! [Y] : ( ~ r1(X,Y) | p315(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1015(Y) ) & ! [Y] : ( ~ r1(X,Y) | p315(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p915(Y) ) & ! [Y] : ( ~ r1(X,Y) | p315(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p815(Y) ) & ! [Y] : ( ~ r1(X,Y) | p315(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p715(Y) ) & ! [Y] : ( ~ r1(X,Y) | p315(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p615(Y) ) & ! [Y] : ( ~ r1(X,Y) | p315(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p515(Y) ) & ! [Y] : ( ~ r1(X,Y) | p315(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p415(Y) ) & ! [Y] : ( ~ r1(X,Y) | p315(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1615(X) & ! [Y] : ( ~ r1(X,Y) | p215(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1515(X) & ! [Y] : ( ~ r1(X,Y) | p215(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1415(Y) ) & ! [Y] : ( ~ r1(X,Y) | p215(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1315(Y) ) & ! [Y] : ( ~ r1(X,Y) | p215(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1215(Y) ) & ! [Y] : ( ~ r1(X,Y) | p215(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1115(Y) ) & ! [Y] : ( ~ r1(X,Y) | p215(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1015(Y) ) & ! [Y] : ( ~ r1(X,Y) | p215(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p915(Y) ) & ! [Y] : ( ~ r1(X,Y) | p215(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p815(Y) ) & ! [Y] : ( ~ r1(X,Y) | p215(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p715(Y) ) & ! [Y] : ( ~ r1(X,Y) | p215(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p615(Y) ) & ! [Y] : ( ~ r1(X,Y) | p215(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p515(Y) ) & ! [Y] : ( ~ r1(X,Y) | p215(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p415(Y) ) & ! [Y] : ( ~ r1(X,Y) | p215(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p315(Y) ) & ! [Y] : ( ~ r1(X,Y) | p215(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1615(X) & ! [Y] : ( ~ r1(X,Y) | p115(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1515(X) & ! [Y] : ( ~ r1(X,Y) | p115(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1415(Y) ) & ! [Y] : ( ~ r1(X,Y) | p115(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1315(Y) ) & ! [Y] : ( ~ r1(X,Y) | p115(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1215(Y) ) & ! [Y] : ( ~ r1(X,Y) | p115(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1115(Y) ) & ! [Y] : ( ~ r1(X,Y) | p115(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1015(Y) ) & ! [Y] : ( ~ r1(X,Y) | p115(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p915(Y) ) & ! [Y] : ( ~ r1(X,Y) | p115(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p815(Y) ) & ! [Y] : ( ~ r1(X,Y) | p115(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p715(Y) ) & ! [Y] : ( ~ r1(X,Y) | p115(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p615(Y) ) & ! [Y] : ( ~ r1(X,Y) | p115(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p515(Y) ) & ! [Y] : ( ~ r1(X,Y) | p115(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p415(Y) ) & ! [Y] : ( ~ r1(X,Y) | p115(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p315(Y) ) & ! [Y] : ( ~ r1(X,Y) | p115(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p215(Y) ) & ! [Y] : ( ~ r1(X,Y) | p115(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1614(X) & p1514(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1614(X) & p1414(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1514(X) & p1414(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1614(X) & ! [Y] : ( ~ r1(X,Y) | p1314(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1514(X) & ! [Y] : ( ~ r1(X,Y) | p1314(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1414(X) & ! [Y] : ( ~ r1(X,Y) | p1314(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1614(X) & ! [Y] : ( ~ r1(X,Y) | p1214(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1514(X) & ! [Y] : ( ~ r1(X,Y) | p1214(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1414(X) & ! [Y] : ( ~ r1(X,Y) | p1214(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1314(Y) ) & ! [Y] : ( ~ r1(X,Y) | p1214(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1614(X) & ! [Y] : ( ~ r1(X,Y) | p1114(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1514(X) & ! [Y] : ( ~ r1(X,Y) | p1114(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1414(X) & ! [Y] : ( ~ r1(X,Y) | p1114(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1314(Y) ) & ! [Y] : ( ~ r1(X,Y) | p1114(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1214(Y) ) & ! [Y] : ( ~ r1(X,Y) | p1114(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1614(X) & ! [Y] : ( ~ r1(X,Y) | p1014(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1514(X) & ! [Y] : ( ~ r1(X,Y) | p1014(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1414(X) & ! [Y] : ( ~ r1(X,Y) | p1014(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1314(Y) ) & ! [Y] : ( ~ r1(X,Y) | p1014(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1214(Y) ) & ! [Y] : ( ~ r1(X,Y) | p1014(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1114(Y) ) & ! [Y] : ( ~ r1(X,Y) | p1014(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1614(X) & ! [Y] : ( ~ r1(X,Y) | p914(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1514(X) & ! [Y] : ( ~ r1(X,Y) | p914(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1414(X) & ! [Y] : ( ~ r1(X,Y) | p914(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1314(Y) ) & ! [Y] : ( ~ r1(X,Y) | p914(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1214(Y) ) & ! [Y] : ( ~ r1(X,Y) | p914(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1114(Y) ) & ! [Y] : ( ~ r1(X,Y) | p914(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1014(Y) ) & ! [Y] : ( ~ r1(X,Y) | p914(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1614(X) & ! [Y] : ( ~ r1(X,Y) | p814(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1514(X) & ! [Y] : ( ~ r1(X,Y) | p814(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1414(X) & ! [Y] : ( ~ r1(X,Y) | p814(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1314(Y) ) & ! [Y] : ( ~ r1(X,Y) | p814(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1214(Y) ) & ! [Y] : ( ~ r1(X,Y) | p814(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1114(Y) ) & ! [Y] : ( ~ r1(X,Y) | p814(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1014(Y) ) & ! [Y] : ( ~ r1(X,Y) | p814(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p914(Y) ) & ! [Y] : ( ~ r1(X,Y) | p814(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1614(X) & ! [Y] : ( ~ r1(X,Y) | p714(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1514(X) & ! [Y] : ( ~ r1(X,Y) | p714(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1414(X) & ! [Y] : ( ~ r1(X,Y) | p714(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1314(Y) ) & ! [Y] : ( ~ r1(X,Y) | p714(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1214(Y) ) & ! [Y] : ( ~ r1(X,Y) | p714(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1114(Y) ) & ! [Y] : ( ~ r1(X,Y) | p714(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1014(Y) ) & ! [Y] : ( ~ r1(X,Y) | p714(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p914(Y) ) & ! [Y] : ( ~ r1(X,Y) | p714(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p814(Y) ) & ! [Y] : ( ~ r1(X,Y) | p714(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1614(X) & ! [Y] : ( ~ r1(X,Y) | p614(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1514(X) & ! [Y] : ( ~ r1(X,Y) | p614(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1414(X) & ! [Y] : ( ~ r1(X,Y) | p614(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1314(Y) ) & ! [Y] : ( ~ r1(X,Y) | p614(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1214(Y) ) & ! [Y] : ( ~ r1(X,Y) | p614(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1114(Y) ) & ! [Y] : ( ~ r1(X,Y) | p614(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1014(Y) ) & ! [Y] : ( ~ r1(X,Y) | p614(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p914(Y) ) & ! [Y] : ( ~ r1(X,Y) | p614(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p814(Y) ) & ! [Y] : ( ~ r1(X,Y) | p614(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p714(Y) ) & ! [Y] : ( ~ r1(X,Y) | p614(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1614(X) & ! [Y] : ( ~ r1(X,Y) | p514(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1514(X) & ! [Y] : ( ~ r1(X,Y) | p514(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1414(X) & ! [Y] : ( ~ r1(X,Y) | p514(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1314(Y) ) & ! [Y] : ( ~ r1(X,Y) | p514(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1214(Y) ) & ! [Y] : ( ~ r1(X,Y) | p514(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1114(Y) ) & ! [Y] : ( ~ r1(X,Y) | p514(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1014(Y) ) & ! [Y] : ( ~ r1(X,Y) | p514(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p914(Y) ) & ! [Y] : ( ~ r1(X,Y) | p514(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p814(Y) ) & ! [Y] : ( ~ r1(X,Y) | p514(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p714(Y) ) & ! [Y] : ( ~ r1(X,Y) | p514(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p614(Y) ) & ! [Y] : ( ~ r1(X,Y) | p514(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1614(X) & ! [Y] : ( ~ r1(X,Y) | p414(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1514(X) & ! [Y] : ( ~ r1(X,Y) | p414(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1414(X) & ! [Y] : ( ~ r1(X,Y) | p414(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1314(Y) ) & ! [Y] : ( ~ r1(X,Y) | p414(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1214(Y) ) & ! [Y] : ( ~ r1(X,Y) | p414(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1114(Y) ) & ! [Y] : ( ~ r1(X,Y) | p414(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1014(Y) ) & ! [Y] : ( ~ r1(X,Y) | p414(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p914(Y) ) & ! [Y] : ( ~ r1(X,Y) | p414(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p814(Y) ) & ! [Y] : ( ~ r1(X,Y) | p414(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p714(Y) ) & ! [Y] : ( ~ r1(X,Y) | p414(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p614(Y) ) & ! [Y] : ( ~ r1(X,Y) | p414(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p514(Y) ) & ! [Y] : ( ~ r1(X,Y) | p414(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1614(X) & ! [Y] : ( ~ r1(X,Y) | p314(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1514(X) & ! [Y] : ( ~ r1(X,Y) | p314(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1414(X) & ! [Y] : ( ~ r1(X,Y) | p314(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1314(Y) ) & ! [Y] : ( ~ r1(X,Y) | p314(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1214(Y) ) & ! [Y] : ( ~ r1(X,Y) | p314(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1114(Y) ) & ! [Y] : ( ~ r1(X,Y) | p314(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1014(Y) ) & ! [Y] : ( ~ r1(X,Y) | p314(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p914(Y) ) & ! [Y] : ( ~ r1(X,Y) | p314(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p814(Y) ) & ! [Y] : ( ~ r1(X,Y) | p314(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p714(Y) ) & ! [Y] : ( ~ r1(X,Y) | p314(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p614(Y) ) & ! [Y] : ( ~ r1(X,Y) | p314(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p514(Y) ) & ! [Y] : ( ~ r1(X,Y) | p314(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p414(Y) ) & ! [Y] : ( ~ r1(X,Y) | p314(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1614(X) & ! [Y] : ( ~ r1(X,Y) | p214(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1514(X) & ! [Y] : ( ~ r1(X,Y) | p214(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1414(X) & ! [Y] : ( ~ r1(X,Y) | p214(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1314(Y) ) & ! [Y] : ( ~ r1(X,Y) | p214(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1214(Y) ) & ! [Y] : ( ~ r1(X,Y) | p214(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1114(Y) ) & ! [Y] : ( ~ r1(X,Y) | p214(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1014(Y) ) & ! [Y] : ( ~ r1(X,Y) | p214(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p914(Y) ) & ! [Y] : ( ~ r1(X,Y) | p214(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p814(Y) ) & ! [Y] : ( ~ r1(X,Y) | p214(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p714(Y) ) & ! [Y] : ( ~ r1(X,Y) | p214(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p614(Y) ) & ! [Y] : ( ~ r1(X,Y) | p214(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p514(Y) ) & ! [Y] : ( ~ r1(X,Y) | p214(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p414(Y) ) & ! [Y] : ( ~ r1(X,Y) | p214(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p314(Y) ) & ! [Y] : ( ~ r1(X,Y) | p214(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1614(X) & ! [Y] : ( ~ r1(X,Y) | p114(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1514(X) & ! [Y] : ( ~ r1(X,Y) | p114(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1414(X) & ! [Y] : ( ~ r1(X,Y) | p114(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1314(Y) ) & ! [Y] : ( ~ r1(X,Y) | p114(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1214(Y) ) & ! [Y] : ( ~ r1(X,Y) | p114(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1114(Y) ) & ! [Y] : ( ~ r1(X,Y) | p114(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1014(Y) ) & ! [Y] : ( ~ r1(X,Y) | p114(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p914(Y) ) & ! [Y] : ( ~ r1(X,Y) | p114(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p814(Y) ) & ! [Y] : ( ~ r1(X,Y) | p114(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p714(Y) ) & ! [Y] : ( ~ r1(X,Y) | p114(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p614(Y) ) & ! [Y] : ( ~ r1(X,Y) | p114(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p514(Y) ) & ! [Y] : ( ~ r1(X,Y) | p114(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p414(Y) ) & ! [Y] : ( ~ r1(X,Y) | p114(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p314(Y) ) & ! [Y] : ( ~ r1(X,Y) | p114(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p214(Y) ) & ! [Y] : ( ~ r1(X,Y) | p114(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1613(X) & p1513(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1613(X) & p1413(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1513(X) & p1413(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1613(X) & p1313(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1513(X) & p1313(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1413(X) & p1313(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1613(X) & ! [Y] : ( ~ r1(X,Y) | p1213(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1513(X) & ! [Y] : ( ~ r1(X,Y) | p1213(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1413(X) & ! [Y] : ( ~ r1(X,Y) | p1213(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1313(X) & ! [Y] : ( ~ r1(X,Y) | p1213(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1613(X) & ! [Y] : ( ~ r1(X,Y) | p1113(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1513(X) & ! [Y] : ( ~ r1(X,Y) | p1113(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1413(X) & ! [Y] : ( ~ r1(X,Y) | p1113(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1313(X) & ! [Y] : ( ~ r1(X,Y) | p1113(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1213(Y) ) & ! [Y] : ( ~ r1(X,Y) | p1113(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1613(X) & ! [Y] : ( ~ r1(X,Y) | p1013(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1513(X) & ! [Y] : ( ~ r1(X,Y) | p1013(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1413(X) & ! [Y] : ( ~ r1(X,Y) | p1013(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1313(X) & ! [Y] : ( ~ r1(X,Y) | p1013(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1213(Y) ) & ! [Y] : ( ~ r1(X,Y) | p1013(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1113(Y) ) & ! [Y] : ( ~ r1(X,Y) | p1013(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1613(X) & ! [Y] : ( ~ r1(X,Y) | p913(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1513(X) & ! [Y] : ( ~ r1(X,Y) | p913(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1413(X) & ! [Y] : ( ~ r1(X,Y) | p913(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1313(X) & ! [Y] : ( ~ r1(X,Y) | p913(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1213(Y) ) & ! [Y] : ( ~ r1(X,Y) | p913(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1113(Y) ) & ! [Y] : ( ~ r1(X,Y) | p913(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1013(Y) ) & ! [Y] : ( ~ r1(X,Y) | p913(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1613(X) & ! [Y] : ( ~ r1(X,Y) | p813(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1513(X) & ! [Y] : ( ~ r1(X,Y) | p813(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1413(X) & ! [Y] : ( ~ r1(X,Y) | p813(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1313(X) & ! [Y] : ( ~ r1(X,Y) | p813(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1213(Y) ) & ! [Y] : ( ~ r1(X,Y) | p813(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1113(Y) ) & ! [Y] : ( ~ r1(X,Y) | p813(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1013(Y) ) & ! [Y] : ( ~ r1(X,Y) | p813(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p913(Y) ) & ! [Y] : ( ~ r1(X,Y) | p813(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1613(X) & ! [Y] : ( ~ r1(X,Y) | p713(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1513(X) & ! [Y] : ( ~ r1(X,Y) | p713(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1413(X) & ! [Y] : ( ~ r1(X,Y) | p713(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1313(X) & ! [Y] : ( ~ r1(X,Y) | p713(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1213(Y) ) & ! [Y] : ( ~ r1(X,Y) | p713(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1113(Y) ) & ! [Y] : ( ~ r1(X,Y) | p713(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1013(Y) ) & ! [Y] : ( ~ r1(X,Y) | p713(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p913(Y) ) & ! [Y] : ( ~ r1(X,Y) | p713(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p813(Y) ) & ! [Y] : ( ~ r1(X,Y) | p713(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1613(X) & ! [Y] : ( ~ r1(X,Y) | p613(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1513(X) & ! [Y] : ( ~ r1(X,Y) | p613(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1413(X) & ! [Y] : ( ~ r1(X,Y) | p613(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1313(X) & ! [Y] : ( ~ r1(X,Y) | p613(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1213(Y) ) & ! [Y] : ( ~ r1(X,Y) | p613(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1113(Y) ) & ! [Y] : ( ~ r1(X,Y) | p613(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1013(Y) ) & ! [Y] : ( ~ r1(X,Y) | p613(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p913(Y) ) & ! [Y] : ( ~ r1(X,Y) | p613(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p813(Y) ) & ! [Y] : ( ~ r1(X,Y) | p613(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p713(Y) ) & ! [Y] : ( ~ r1(X,Y) | p613(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1613(X) & ! [Y] : ( ~ r1(X,Y) | p513(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1513(X) & ! [Y] : ( ~ r1(X,Y) | p513(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1413(X) & ! [Y] : ( ~ r1(X,Y) | p513(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1313(X) & ! [Y] : ( ~ r1(X,Y) | p513(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1213(Y) ) & ! [Y] : ( ~ r1(X,Y) | p513(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1113(Y) ) & ! [Y] : ( ~ r1(X,Y) | p513(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1013(Y) ) & ! [Y] : ( ~ r1(X,Y) | p513(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p913(Y) ) & ! [Y] : ( ~ r1(X,Y) | p513(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p813(Y) ) & ! [Y] : ( ~ r1(X,Y) | p513(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p713(Y) ) & ! [Y] : ( ~ r1(X,Y) | p513(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p613(Y) ) & ! [Y] : ( ~ r1(X,Y) | p513(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1613(X) & ! [Y] : ( ~ r1(X,Y) | p413(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1513(X) & ! [Y] : ( ~ r1(X,Y) | p413(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1413(X) & ! [Y] : ( ~ r1(X,Y) | p413(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1313(X) & ! [Y] : ( ~ r1(X,Y) | p413(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1213(Y) ) & ! [Y] : ( ~ r1(X,Y) | p413(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1113(Y) ) & ! [Y] : ( ~ r1(X,Y) | p413(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1013(Y) ) & ! [Y] : ( ~ r1(X,Y) | p413(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p913(Y) ) & ! [Y] : ( ~ r1(X,Y) | p413(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p813(Y) ) & ! [Y] : ( ~ r1(X,Y) | p413(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p713(Y) ) & ! [Y] : ( ~ r1(X,Y) | p413(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p613(Y) ) & ! [Y] : ( ~ r1(X,Y) | p413(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p513(Y) ) & ! [Y] : ( ~ r1(X,Y) | p413(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1613(X) & ! [Y] : ( ~ r1(X,Y) | p313(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1513(X) & ! [Y] : ( ~ r1(X,Y) | p313(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1413(X) & ! [Y] : ( ~ r1(X,Y) | p313(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1313(X) & ! [Y] : ( ~ r1(X,Y) | p313(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1213(Y) ) & ! [Y] : ( ~ r1(X,Y) | p313(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1113(Y) ) & ! [Y] : ( ~ r1(X,Y) | p313(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1013(Y) ) & ! [Y] : ( ~ r1(X,Y) | p313(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p913(Y) ) & ! [Y] : ( ~ r1(X,Y) | p313(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p813(Y) ) & ! [Y] : ( ~ r1(X,Y) | p313(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p713(Y) ) & ! [Y] : ( ~ r1(X,Y) | p313(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p613(Y) ) & ! [Y] : ( ~ r1(X,Y) | p313(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p513(Y) ) & ! [Y] : ( ~ r1(X,Y) | p313(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p413(Y) ) & ! [Y] : ( ~ r1(X,Y) | p313(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1613(X) & ! [Y] : ( ~ r1(X,Y) | p213(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1513(X) & ! [Y] : ( ~ r1(X,Y) | p213(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1413(X) & ! [Y] : ( ~ r1(X,Y) | p213(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1313(X) & ! [Y] : ( ~ r1(X,Y) | p213(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1213(Y) ) & ! [Y] : ( ~ r1(X,Y) | p213(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1113(Y) ) & ! [Y] : ( ~ r1(X,Y) | p213(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1013(Y) ) & ! [Y] : ( ~ r1(X,Y) | p213(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p913(Y) ) & ! [Y] : ( ~ r1(X,Y) | p213(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p813(Y) ) & ! [Y] : ( ~ r1(X,Y) | p213(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p713(Y) ) & ! [Y] : ( ~ r1(X,Y) | p213(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p613(Y) ) & ! [Y] : ( ~ r1(X,Y) | p213(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p513(Y) ) & ! [Y] : ( ~ r1(X,Y) | p213(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p413(Y) ) & ! [Y] : ( ~ r1(X,Y) | p213(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p313(Y) ) & ! [Y] : ( ~ r1(X,Y) | p213(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1613(X) & ! [Y] : ( ~ r1(X,Y) | p113(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1513(X) & ! [Y] : ( ~ r1(X,Y) | p113(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1413(X) & ! [Y] : ( ~ r1(X,Y) | p113(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1313(X) & ! [Y] : ( ~ r1(X,Y) | p113(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1213(Y) ) & ! [Y] : ( ~ r1(X,Y) | p113(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1113(Y) ) & ! [Y] : ( ~ r1(X,Y) | p113(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1013(Y) ) & ! [Y] : ( ~ r1(X,Y) | p113(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p913(Y) ) & ! [Y] : ( ~ r1(X,Y) | p113(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p813(Y) ) & ! [Y] : ( ~ r1(X,Y) | p113(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p713(Y) ) & ! [Y] : ( ~ r1(X,Y) | p113(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p613(Y) ) & ! [Y] : ( ~ r1(X,Y) | p113(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p513(Y) ) & ! [Y] : ( ~ r1(X,Y) | p113(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p413(Y) ) & ! [Y] : ( ~ r1(X,Y) | p113(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p313(Y) ) & ! [Y] : ( ~ r1(X,Y) | p113(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p213(Y) ) & ! [Y] : ( ~ r1(X,Y) | p113(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1612(X) & p1512(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1612(X) & p1412(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1512(X) & p1412(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1612(X) & p1312(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1512(X) & p1312(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1412(X) & p1312(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1612(X) & p1212(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1512(X) & p1212(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1412(X) & p1212(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1312(X) & p1212(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1612(X) & ! [Y] : ( ~ r1(X,Y) | p1112(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1512(X) & ! [Y] : ( ~ r1(X,Y) | p1112(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1412(X) & ! [Y] : ( ~ r1(X,Y) | p1112(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1312(X) & ! [Y] : ( ~ r1(X,Y) | p1112(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1212(X) & ! [Y] : ( ~ r1(X,Y) | p1112(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1612(X) & ! [Y] : ( ~ r1(X,Y) | p1012(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1512(X) & ! [Y] : ( ~ r1(X,Y) | p1012(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1412(X) & ! [Y] : ( ~ r1(X,Y) | p1012(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1312(X) & ! [Y] : ( ~ r1(X,Y) | p1012(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1212(X) & ! [Y] : ( ~ r1(X,Y) | p1012(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1112(Y) ) & ! [Y] : ( ~ r1(X,Y) | p1012(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1612(X) & ! [Y] : ( ~ r1(X,Y) | p912(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1512(X) & ! [Y] : ( ~ r1(X,Y) | p912(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1412(X) & ! [Y] : ( ~ r1(X,Y) | p912(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1312(X) & ! [Y] : ( ~ r1(X,Y) | p912(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1212(X) & ! [Y] : ( ~ r1(X,Y) | p912(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1112(Y) ) & ! [Y] : ( ~ r1(X,Y) | p912(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1012(Y) ) & ! [Y] : ( ~ r1(X,Y) | p912(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1612(X) & ! [Y] : ( ~ r1(X,Y) | p812(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1512(X) & ! [Y] : ( ~ r1(X,Y) | p812(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1412(X) & ! [Y] : ( ~ r1(X,Y) | p812(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1312(X) & ! [Y] : ( ~ r1(X,Y) | p812(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1212(X) & ! [Y] : ( ~ r1(X,Y) | p812(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1112(Y) ) & ! [Y] : ( ~ r1(X,Y) | p812(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1012(Y) ) & ! [Y] : ( ~ r1(X,Y) | p812(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p912(Y) ) & ! [Y] : ( ~ r1(X,Y) | p812(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1612(X) & ! [Y] : ( ~ r1(X,Y) | p712(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1512(X) & ! [Y] : ( ~ r1(X,Y) | p712(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1412(X) & ! [Y] : ( ~ r1(X,Y) | p712(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1312(X) & ! [Y] : ( ~ r1(X,Y) | p712(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1212(X) & ! [Y] : ( ~ r1(X,Y) | p712(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1112(Y) ) & ! [Y] : ( ~ r1(X,Y) | p712(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1012(Y) ) & ! [Y] : ( ~ r1(X,Y) | p712(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p912(Y) ) & ! [Y] : ( ~ r1(X,Y) | p712(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p812(Y) ) & ! [Y] : ( ~ r1(X,Y) | p712(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1612(X) & ! [Y] : ( ~ r1(X,Y) | p612(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1512(X) & ! [Y] : ( ~ r1(X,Y) | p612(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1412(X) & ! [Y] : ( ~ r1(X,Y) | p612(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1312(X) & ! [Y] : ( ~ r1(X,Y) | p612(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1212(X) & ! [Y] : ( ~ r1(X,Y) | p612(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1112(Y) ) & ! [Y] : ( ~ r1(X,Y) | p612(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1012(Y) ) & ! [Y] : ( ~ r1(X,Y) | p612(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p912(Y) ) & ! [Y] : ( ~ r1(X,Y) | p612(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p812(Y) ) & ! [Y] : ( ~ r1(X,Y) | p612(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p712(Y) ) & ! [Y] : ( ~ r1(X,Y) | p612(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1612(X) & ! [Y] : ( ~ r1(X,Y) | p512(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1512(X) & ! [Y] : ( ~ r1(X,Y) | p512(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1412(X) & ! [Y] : ( ~ r1(X,Y) | p512(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1312(X) & ! [Y] : ( ~ r1(X,Y) | p512(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1212(X) & ! [Y] : ( ~ r1(X,Y) | p512(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1112(Y) ) & ! [Y] : ( ~ r1(X,Y) | p512(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1012(Y) ) & ! [Y] : ( ~ r1(X,Y) | p512(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p912(Y) ) & ! [Y] : ( ~ r1(X,Y) | p512(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p812(Y) ) & ! [Y] : ( ~ r1(X,Y) | p512(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p712(Y) ) & ! [Y] : ( ~ r1(X,Y) | p512(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p612(Y) ) & ! [Y] : ( ~ r1(X,Y) | p512(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1612(X) & ! [Y] : ( ~ r1(X,Y) | p412(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1512(X) & ! [Y] : ( ~ r1(X,Y) | p412(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1412(X) & ! [Y] : ( ~ r1(X,Y) | p412(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1312(X) & ! [Y] : ( ~ r1(X,Y) | p412(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1212(X) & ! [Y] : ( ~ r1(X,Y) | p412(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1112(Y) ) & ! [Y] : ( ~ r1(X,Y) | p412(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1012(Y) ) & ! [Y] : ( ~ r1(X,Y) | p412(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p912(Y) ) & ! [Y] : ( ~ r1(X,Y) | p412(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p812(Y) ) & ! [Y] : ( ~ r1(X,Y) | p412(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p712(Y) ) & ! [Y] : ( ~ r1(X,Y) | p412(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p612(Y) ) & ! [Y] : ( ~ r1(X,Y) | p412(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p512(Y) ) & ! [Y] : ( ~ r1(X,Y) | p412(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1612(X) & ! [Y] : ( ~ r1(X,Y) | p312(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1512(X) & ! [Y] : ( ~ r1(X,Y) | p312(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1412(X) & ! [Y] : ( ~ r1(X,Y) | p312(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1312(X) & ! [Y] : ( ~ r1(X,Y) | p312(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1212(X) & ! [Y] : ( ~ r1(X,Y) | p312(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1112(Y) ) & ! [Y] : ( ~ r1(X,Y) | p312(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1012(Y) ) & ! [Y] : ( ~ r1(X,Y) | p312(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p912(Y) ) & ! [Y] : ( ~ r1(X,Y) | p312(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p812(Y) ) & ! [Y] : ( ~ r1(X,Y) | p312(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p712(Y) ) & ! [Y] : ( ~ r1(X,Y) | p312(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p612(Y) ) & ! [Y] : ( ~ r1(X,Y) | p312(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p512(Y) ) & ! [Y] : ( ~ r1(X,Y) | p312(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p412(Y) ) & ! [Y] : ( ~ r1(X,Y) | p312(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1612(X) & ! [Y] : ( ~ r1(X,Y) | p212(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1512(X) & ! [Y] : ( ~ r1(X,Y) | p212(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1412(X) & ! [Y] : ( ~ r1(X,Y) | p212(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1312(X) & ! [Y] : ( ~ r1(X,Y) | p212(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1212(X) & ! [Y] : ( ~ r1(X,Y) | p212(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1112(Y) ) & ! [Y] : ( ~ r1(X,Y) | p212(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1012(Y) ) & ! [Y] : ( ~ r1(X,Y) | p212(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p912(Y) ) & ! [Y] : ( ~ r1(X,Y) | p212(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p812(Y) ) & ! [Y] : ( ~ r1(X,Y) | p212(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p712(Y) ) & ! [Y] : ( ~ r1(X,Y) | p212(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p612(Y) ) & ! [Y] : ( ~ r1(X,Y) | p212(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p512(Y) ) & ! [Y] : ( ~ r1(X,Y) | p212(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p412(Y) ) & ! [Y] : ( ~ r1(X,Y) | p212(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p312(Y) ) & ! [Y] : ( ~ r1(X,Y) | p212(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1612(X) & ! [Y] : ( ~ r1(X,Y) | p112(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1512(X) & ! [Y] : ( ~ r1(X,Y) | p112(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1412(X) & ! [Y] : ( ~ r1(X,Y) | p112(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1312(X) & ! [Y] : ( ~ r1(X,Y) | p112(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1212(X) & ! [Y] : ( ~ r1(X,Y) | p112(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1112(Y) ) & ! [Y] : ( ~ r1(X,Y) | p112(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1012(Y) ) & ! [Y] : ( ~ r1(X,Y) | p112(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p912(Y) ) & ! [Y] : ( ~ r1(X,Y) | p112(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p812(Y) ) & ! [Y] : ( ~ r1(X,Y) | p112(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p712(Y) ) & ! [Y] : ( ~ r1(X,Y) | p112(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p612(Y) ) & ! [Y] : ( ~ r1(X,Y) | p112(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p512(Y) ) & ! [Y] : ( ~ r1(X,Y) | p112(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p412(Y) ) & ! [Y] : ( ~ r1(X,Y) | p112(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p312(Y) ) & ! [Y] : ( ~ r1(X,Y) | p112(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p212(Y) ) & ! [Y] : ( ~ r1(X,Y) | p112(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1611(X) & p1511(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1611(X) & p1411(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1511(X) & p1411(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1611(X) & p1311(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1511(X) & p1311(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1411(X) & p1311(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1611(X) & p1211(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1511(X) & p1211(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1411(X) & p1211(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1311(X) & p1211(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1611(X) & ~ p1111(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1511(X) & ~ p1111(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1411(X) & ~ p1111(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1311(X) & ~ p1111(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1211(X) & ~ p1111(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1611(X) & ! [Y] : ( ~ r1(X,Y) | p1011(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1511(X) & ! [Y] : ( ~ r1(X,Y) | p1011(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1411(X) & ! [Y] : ( ~ r1(X,Y) | p1011(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1311(X) & ! [Y] : ( ~ r1(X,Y) | p1011(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1211(X) & ! [Y] : ( ~ r1(X,Y) | p1011(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ~ p1111(X) & ! [Y] : ( ~ r1(X,Y) | p1011(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1611(X) & ! [Y] : ( ~ r1(X,Y) | p911(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1511(X) & ! [Y] : ( ~ r1(X,Y) | p911(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1411(X) & ! [Y] : ( ~ r1(X,Y) | p911(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1311(X) & ! [Y] : ( ~ r1(X,Y) | p911(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1211(X) & ! [Y] : ( ~ r1(X,Y) | p911(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ~ p1111(X) & ! [Y] : ( ~ r1(X,Y) | p911(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1011(Y) ) & ! [Y] : ( ~ r1(X,Y) | p911(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1611(X) & ! [Y] : ( ~ r1(X,Y) | p811(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1511(X) & ! [Y] : ( ~ r1(X,Y) | p811(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1411(X) & ! [Y] : ( ~ r1(X,Y) | p811(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1311(X) & ! [Y] : ( ~ r1(X,Y) | p811(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1211(X) & ! [Y] : ( ~ r1(X,Y) | p811(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ~ p1111(X) & ! [Y] : ( ~ r1(X,Y) | p811(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1011(Y) ) & ! [Y] : ( ~ r1(X,Y) | p811(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p911(Y) ) & ! [Y] : ( ~ r1(X,Y) | p811(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1611(X) & ! [Y] : ( ~ r1(X,Y) | p711(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1511(X) & ! [Y] : ( ~ r1(X,Y) | p711(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1411(X) & ! [Y] : ( ~ r1(X,Y) | p711(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1311(X) & ! [Y] : ( ~ r1(X,Y) | p711(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1211(X) & ! [Y] : ( ~ r1(X,Y) | p711(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ~ p1111(X) & ! [Y] : ( ~ r1(X,Y) | p711(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1011(Y) ) & ! [Y] : ( ~ r1(X,Y) | p711(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p911(Y) ) & ! [Y] : ( ~ r1(X,Y) | p711(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p811(Y) ) & ! [Y] : ( ~ r1(X,Y) | p711(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1611(X) & ! [Y] : ( ~ r1(X,Y) | p611(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1511(X) & ! [Y] : ( ~ r1(X,Y) | p611(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1411(X) & ! [Y] : ( ~ r1(X,Y) | p611(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1311(X) & ! [Y] : ( ~ r1(X,Y) | p611(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1211(X) & ! [Y] : ( ~ r1(X,Y) | p611(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ~ p1111(X) & ! [Y] : ( ~ r1(X,Y) | p611(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1011(Y) ) & ! [Y] : ( ~ r1(X,Y) | p611(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p911(Y) ) & ! [Y] : ( ~ r1(X,Y) | p611(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p811(Y) ) & ! [Y] : ( ~ r1(X,Y) | p611(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p711(Y) ) & ! [Y] : ( ~ r1(X,Y) | p611(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1611(X) & ! [Y] : ( ~ r1(X,Y) | p511(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1511(X) & ! [Y] : ( ~ r1(X,Y) | p511(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1411(X) & ! [Y] : ( ~ r1(X,Y) | p511(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1311(X) & ! [Y] : ( ~ r1(X,Y) | p511(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1211(X) & ! [Y] : ( ~ r1(X,Y) | p511(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ~ p1111(X) & ! [Y] : ( ~ r1(X,Y) | p511(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1011(Y) ) & ! [Y] : ( ~ r1(X,Y) | p511(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p911(Y) ) & ! [Y] : ( ~ r1(X,Y) | p511(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p811(Y) ) & ! [Y] : ( ~ r1(X,Y) | p511(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p711(Y) ) & ! [Y] : ( ~ r1(X,Y) | p511(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p611(Y) ) & ! [Y] : ( ~ r1(X,Y) | p511(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1611(X) & ! [Y] : ( ~ r1(X,Y) | p411(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1511(X) & ! [Y] : ( ~ r1(X,Y) | p411(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1411(X) & ! [Y] : ( ~ r1(X,Y) | p411(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1311(X) & ! [Y] : ( ~ r1(X,Y) | p411(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1211(X) & ! [Y] : ( ~ r1(X,Y) | p411(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ~ p1111(X) & ! [Y] : ( ~ r1(X,Y) | p411(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1011(Y) ) & ! [Y] : ( ~ r1(X,Y) | p411(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p911(Y) ) & ! [Y] : ( ~ r1(X,Y) | p411(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p811(Y) ) & ! [Y] : ( ~ r1(X,Y) | p411(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p711(Y) ) & ! [Y] : ( ~ r1(X,Y) | p411(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p611(Y) ) & ! [Y] : ( ~ r1(X,Y) | p411(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p511(Y) ) & ! [Y] : ( ~ r1(X,Y) | p411(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1611(X) & ! [Y] : ( ~ r1(X,Y) | p311(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1511(X) & ! [Y] : ( ~ r1(X,Y) | p311(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1411(X) & ! [Y] : ( ~ r1(X,Y) | p311(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1311(X) & ! [Y] : ( ~ r1(X,Y) | p311(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1211(X) & ! [Y] : ( ~ r1(X,Y) | p311(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ~ p1111(X) & ! [Y] : ( ~ r1(X,Y) | p311(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1011(Y) ) & ! [Y] : ( ~ r1(X,Y) | p311(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p911(Y) ) & ! [Y] : ( ~ r1(X,Y) | p311(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p811(Y) ) & ! [Y] : ( ~ r1(X,Y) | p311(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p711(Y) ) & ! [Y] : ( ~ r1(X,Y) | p311(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p611(Y) ) & ! [Y] : ( ~ r1(X,Y) | p311(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p511(Y) ) & ! [Y] : ( ~ r1(X,Y) | p311(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p411(Y) ) & ! [Y] : ( ~ r1(X,Y) | p311(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1611(X) & ! [Y] : ( ~ r1(X,Y) | p211(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1511(X) & ! [Y] : ( ~ r1(X,Y) | p211(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1411(X) & ! [Y] : ( ~ r1(X,Y) | p211(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1311(X) & ! [Y] : ( ~ r1(X,Y) | p211(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1211(X) & ! [Y] : ( ~ r1(X,Y) | p211(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ~ p1111(X) & ! [Y] : ( ~ r1(X,Y) | p211(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1011(Y) ) & ! [Y] : ( ~ r1(X,Y) | p211(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p911(Y) ) & ! [Y] : ( ~ r1(X,Y) | p211(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p811(Y) ) & ! [Y] : ( ~ r1(X,Y) | p211(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p711(Y) ) & ! [Y] : ( ~ r1(X,Y) | p211(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p611(Y) ) & ! [Y] : ( ~ r1(X,Y) | p211(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p511(Y) ) & ! [Y] : ( ~ r1(X,Y) | p211(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p411(Y) ) & ! [Y] : ( ~ r1(X,Y) | p211(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p311(Y) ) & ! [Y] : ( ~ r1(X,Y) | p211(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1611(X) & ! [Y] : ( ~ r1(X,Y) | p111(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1511(X) & ! [Y] : ( ~ r1(X,Y) | p111(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1411(X) & ! [Y] : ( ~ r1(X,Y) | p111(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1311(X) & ! [Y] : ( ~ r1(X,Y) | p111(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1211(X) & ! [Y] : ( ~ r1(X,Y) | p111(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ~ p1111(X) & ! [Y] : ( ~ r1(X,Y) | p111(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p1011(Y) ) & ! [Y] : ( ~ r1(X,Y) | p111(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p911(Y) ) & ! [Y] : ( ~ r1(X,Y) | p111(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p811(Y) ) & ! [Y] : ( ~ r1(X,Y) | p111(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p711(Y) ) & ! [Y] : ( ~ r1(X,Y) | p111(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p611(Y) ) & ! [Y] : ( ~ r1(X,Y) | p111(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p511(Y) ) & ! [Y] : ( ~ r1(X,Y) | p111(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p411(Y) ) & ! [Y] : ( ~ r1(X,Y) | p111(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p311(Y) ) & ! [Y] : ( ~ r1(X,Y) | p111(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p211(Y) ) & ! [Y] : ( ~ r1(X,Y) | p111(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1610(X) & p1510(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1610(X) & p1410(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1510(X) & p1410(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1610(X) & p1310(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1510(X) & p1310(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1410(X) & p1310(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1610(X) & p1210(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1510(X) & p1210(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1410(X) & p1210(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1310(X) & p1210(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1610(X) & p1110(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1510(X) & p1110(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1410(X) & p1110(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1310(X) & p1110(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1210(X) & p1110(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1610(X) & p1010(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1510(X) & p1010(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1410(X) & p1010(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1310(X) & p1010(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1210(X) & p1010(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1110(X) & p1010(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1610(X) & ! [Y] : ( ~ r1(X,Y) | p910(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1510(X) & ! [Y] : ( ~ r1(X,Y) | p910(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1410(X) & ! [Y] : ( ~ r1(X,Y) | p910(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1310(X) & ! [Y] : ( ~ r1(X,Y) | p910(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1210(X) & ! [Y] : ( ~ r1(X,Y) | p910(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1110(X) & ! [Y] : ( ~ r1(X,Y) | p910(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1010(X) & ! [Y] : ( ~ r1(X,Y) | p910(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1610(X) & ! [Y] : ( ~ r1(X,Y) | p810(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1510(X) & ! [Y] : ( ~ r1(X,Y) | p810(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1410(X) & ! [Y] : ( ~ r1(X,Y) | p810(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1310(X) & ! [Y] : ( ~ r1(X,Y) | p810(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1210(X) & ! [Y] : ( ~ r1(X,Y) | p810(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1110(X) & ! [Y] : ( ~ r1(X,Y) | p810(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1010(X) & ! [Y] : ( ~ r1(X,Y) | p810(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p910(Y) ) & ! [Y] : ( ~ r1(X,Y) | p810(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1610(X) & ! [Y] : ( ~ r1(X,Y) | p710(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1510(X) & ! [Y] : ( ~ r1(X,Y) | p710(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1410(X) & ! [Y] : ( ~ r1(X,Y) | p710(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1310(X) & ! [Y] : ( ~ r1(X,Y) | p710(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1210(X) & ! [Y] : ( ~ r1(X,Y) | p710(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1110(X) & ! [Y] : ( ~ r1(X,Y) | p710(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1010(X) & ! [Y] : ( ~ r1(X,Y) | p710(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p910(Y) ) & ! [Y] : ( ~ r1(X,Y) | p710(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p810(Y) ) & ! [Y] : ( ~ r1(X,Y) | p710(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1610(X) & ! [Y] : ( ~ r1(X,Y) | p610(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1510(X) & ! [Y] : ( ~ r1(X,Y) | p610(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1410(X) & ! [Y] : ( ~ r1(X,Y) | p610(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1310(X) & ! [Y] : ( ~ r1(X,Y) | p610(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1210(X) & ! [Y] : ( ~ r1(X,Y) | p610(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1110(X) & ! [Y] : ( ~ r1(X,Y) | p610(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1010(X) & ! [Y] : ( ~ r1(X,Y) | p610(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p910(Y) ) & ! [Y] : ( ~ r1(X,Y) | p610(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p810(Y) ) & ! [Y] : ( ~ r1(X,Y) | p610(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p710(Y) ) & ! [Y] : ( ~ r1(X,Y) | p610(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1610(X) & ! [Y] : ( ~ r1(X,Y) | p510(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1510(X) & ! [Y] : ( ~ r1(X,Y) | p510(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1410(X) & ! [Y] : ( ~ r1(X,Y) | p510(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1310(X) & ! [Y] : ( ~ r1(X,Y) | p510(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1210(X) & ! [Y] : ( ~ r1(X,Y) | p510(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1110(X) & ! [Y] : ( ~ r1(X,Y) | p510(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1010(X) & ! [Y] : ( ~ r1(X,Y) | p510(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p910(Y) ) & ! [Y] : ( ~ r1(X,Y) | p510(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p810(Y) ) & ! [Y] : ( ~ r1(X,Y) | p510(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p710(Y) ) & ! [Y] : ( ~ r1(X,Y) | p510(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p610(Y) ) & ! [Y] : ( ~ r1(X,Y) | p510(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1610(X) & ! [Y] : ( ~ r1(X,Y) | p410(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1510(X) & ! [Y] : ( ~ r1(X,Y) | p410(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1410(X) & ! [Y] : ( ~ r1(X,Y) | p410(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1310(X) & ! [Y] : ( ~ r1(X,Y) | p410(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1210(X) & ! [Y] : ( ~ r1(X,Y) | p410(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1110(X) & ! [Y] : ( ~ r1(X,Y) | p410(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1010(X) & ! [Y] : ( ~ r1(X,Y) | p410(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p910(Y) ) & ! [Y] : ( ~ r1(X,Y) | p410(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p810(Y) ) & ! [Y] : ( ~ r1(X,Y) | p410(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p710(Y) ) & ! [Y] : ( ~ r1(X,Y) | p410(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p610(Y) ) & ! [Y] : ( ~ r1(X,Y) | p410(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p510(Y) ) & ! [Y] : ( ~ r1(X,Y) | p410(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1610(X) & ! [Y] : ( ~ r1(X,Y) | p310(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1510(X) & ! [Y] : ( ~ r1(X,Y) | p310(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1410(X) & ! [Y] : ( ~ r1(X,Y) | p310(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1310(X) & ! [Y] : ( ~ r1(X,Y) | p310(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1210(X) & ! [Y] : ( ~ r1(X,Y) | p310(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1110(X) & ! [Y] : ( ~ r1(X,Y) | p310(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1010(X) & ! [Y] : ( ~ r1(X,Y) | p310(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p910(Y) ) & ! [Y] : ( ~ r1(X,Y) | p310(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p810(Y) ) & ! [Y] : ( ~ r1(X,Y) | p310(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p710(Y) ) & ! [Y] : ( ~ r1(X,Y) | p310(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p610(Y) ) & ! [Y] : ( ~ r1(X,Y) | p310(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p510(Y) ) & ! [Y] : ( ~ r1(X,Y) | p310(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p410(Y) ) & ! [Y] : ( ~ r1(X,Y) | p310(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1610(X) & ! [Y] : ( ~ r1(X,Y) | p210(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1510(X) & ! [Y] : ( ~ r1(X,Y) | p210(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1410(X) & ! [Y] : ( ~ r1(X,Y) | p210(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1310(X) & ! [Y] : ( ~ r1(X,Y) | p210(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1210(X) & ! [Y] : ( ~ r1(X,Y) | p210(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1110(X) & ! [Y] : ( ~ r1(X,Y) | p210(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1010(X) & ! [Y] : ( ~ r1(X,Y) | p210(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p910(Y) ) & ! [Y] : ( ~ r1(X,Y) | p210(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p810(Y) ) & ! [Y] : ( ~ r1(X,Y) | p210(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p710(Y) ) & ! [Y] : ( ~ r1(X,Y) | p210(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p610(Y) ) & ! [Y] : ( ~ r1(X,Y) | p210(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p510(Y) ) & ! [Y] : ( ~ r1(X,Y) | p210(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p410(Y) ) & ! [Y] : ( ~ r1(X,Y) | p210(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p310(Y) ) & ! [Y] : ( ~ r1(X,Y) | p210(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1610(X) & ! [Y] : ( ~ r1(X,Y) | p110(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1510(X) & ! [Y] : ( ~ r1(X,Y) | p110(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1410(X) & ! [Y] : ( ~ r1(X,Y) | p110(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1310(X) & ! [Y] : ( ~ r1(X,Y) | p110(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1210(X) & ! [Y] : ( ~ r1(X,Y) | p110(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1110(X) & ! [Y] : ( ~ r1(X,Y) | p110(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1010(X) & ! [Y] : ( ~ r1(X,Y) | p110(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p910(Y) ) & ! [Y] : ( ~ r1(X,Y) | p110(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p810(Y) ) & ! [Y] : ( ~ r1(X,Y) | p110(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p710(Y) ) & ! [Y] : ( ~ r1(X,Y) | p110(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p610(Y) ) & ! [Y] : ( ~ r1(X,Y) | p110(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p510(Y) ) & ! [Y] : ( ~ r1(X,Y) | p110(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p410(Y) ) & ! [Y] : ( ~ r1(X,Y) | p110(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p310(Y) ) & ! [Y] : ( ~ r1(X,Y) | p110(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p210(Y) ) & ! [Y] : ( ~ r1(X,Y) | p110(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1609(X) & p1509(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1609(X) & p1409(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1509(X) & p1409(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1609(X) & p1309(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1509(X) & p1309(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1409(X) & p1309(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1609(X) & p1209(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1509(X) & p1209(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1409(X) & p1209(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1309(X) & p1209(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1609(X) & p1109(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1509(X) & p1109(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1409(X) & p1109(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1309(X) & p1109(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1209(X) & p1109(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1609(X) & p1009(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1509(X) & p1009(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1409(X) & p1009(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1309(X) & p1009(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1209(X) & p1009(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1109(X) & p1009(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1609(X) & p909(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1509(X) & p909(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1409(X) & p909(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1309(X) & p909(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1209(X) & p909(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1109(X) & p909(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1009(X) & p909(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1609(X) & ! [Y] : ( ~ r1(X,Y) | p809(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1509(X) & ! [Y] : ( ~ r1(X,Y) | p809(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1409(X) & ! [Y] : ( ~ r1(X,Y) | p809(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1309(X) & ! [Y] : ( ~ r1(X,Y) | p809(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1209(X) & ! [Y] : ( ~ r1(X,Y) | p809(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1109(X) & ! [Y] : ( ~ r1(X,Y) | p809(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1009(X) & ! [Y] : ( ~ r1(X,Y) | p809(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p909(X) & ! [Y] : ( ~ r1(X,Y) | p809(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1609(X) & ! [Y] : ( ~ r1(X,Y) | p709(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1509(X) & ! [Y] : ( ~ r1(X,Y) | p709(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1409(X) & ! [Y] : ( ~ r1(X,Y) | p709(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1309(X) & ! [Y] : ( ~ r1(X,Y) | p709(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1209(X) & ! [Y] : ( ~ r1(X,Y) | p709(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1109(X) & ! [Y] : ( ~ r1(X,Y) | p709(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1009(X) & ! [Y] : ( ~ r1(X,Y) | p709(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p909(X) & ! [Y] : ( ~ r1(X,Y) | p709(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p809(Y) ) & ! [Y] : ( ~ r1(X,Y) | p709(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1609(X) & ! [Y] : ( ~ r1(X,Y) | p609(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1509(X) & ! [Y] : ( ~ r1(X,Y) | p609(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1409(X) & ! [Y] : ( ~ r1(X,Y) | p609(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1309(X) & ! [Y] : ( ~ r1(X,Y) | p609(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1209(X) & ! [Y] : ( ~ r1(X,Y) | p609(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1109(X) & ! [Y] : ( ~ r1(X,Y) | p609(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1009(X) & ! [Y] : ( ~ r1(X,Y) | p609(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p909(X) & ! [Y] : ( ~ r1(X,Y) | p609(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p809(Y) ) & ! [Y] : ( ~ r1(X,Y) | p609(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p709(Y) ) & ! [Y] : ( ~ r1(X,Y) | p609(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1609(X) & ! [Y] : ( ~ r1(X,Y) | p509(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1509(X) & ! [Y] : ( ~ r1(X,Y) | p509(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1409(X) & ! [Y] : ( ~ r1(X,Y) | p509(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1309(X) & ! [Y] : ( ~ r1(X,Y) | p509(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1209(X) & ! [Y] : ( ~ r1(X,Y) | p509(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1109(X) & ! [Y] : ( ~ r1(X,Y) | p509(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1009(X) & ! [Y] : ( ~ r1(X,Y) | p509(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p909(X) & ! [Y] : ( ~ r1(X,Y) | p509(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p809(Y) ) & ! [Y] : ( ~ r1(X,Y) | p509(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p709(Y) ) & ! [Y] : ( ~ r1(X,Y) | p509(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p609(Y) ) & ! [Y] : ( ~ r1(X,Y) | p509(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1609(X) & ! [Y] : ( ~ r1(X,Y) | p409(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1509(X) & ! [Y] : ( ~ r1(X,Y) | p409(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1409(X) & ! [Y] : ( ~ r1(X,Y) | p409(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1309(X) & ! [Y] : ( ~ r1(X,Y) | p409(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1209(X) & ! [Y] : ( ~ r1(X,Y) | p409(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1109(X) & ! [Y] : ( ~ r1(X,Y) | p409(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1009(X) & ! [Y] : ( ~ r1(X,Y) | p409(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p909(X) & ! [Y] : ( ~ r1(X,Y) | p409(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p809(Y) ) & ! [Y] : ( ~ r1(X,Y) | p409(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p709(Y) ) & ! [Y] : ( ~ r1(X,Y) | p409(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p609(Y) ) & ! [Y] : ( ~ r1(X,Y) | p409(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p509(Y) ) & ! [Y] : ( ~ r1(X,Y) | p409(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1609(X) & ! [Y] : ( ~ r1(X,Y) | p309(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1509(X) & ! [Y] : ( ~ r1(X,Y) | p309(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1409(X) & ! [Y] : ( ~ r1(X,Y) | p309(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1309(X) & ! [Y] : ( ~ r1(X,Y) | p309(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1209(X) & ! [Y] : ( ~ r1(X,Y) | p309(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1109(X) & ! [Y] : ( ~ r1(X,Y) | p309(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1009(X) & ! [Y] : ( ~ r1(X,Y) | p309(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p909(X) & ! [Y] : ( ~ r1(X,Y) | p309(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p809(Y) ) & ! [Y] : ( ~ r1(X,Y) | p309(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p709(Y) ) & ! [Y] : ( ~ r1(X,Y) | p309(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p609(Y) ) & ! [Y] : ( ~ r1(X,Y) | p309(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p509(Y) ) & ! [Y] : ( ~ r1(X,Y) | p309(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p409(Y) ) & ! [Y] : ( ~ r1(X,Y) | p309(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1609(X) & ! [Y] : ( ~ r1(X,Y) | p209(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1509(X) & ! [Y] : ( ~ r1(X,Y) | p209(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1409(X) & ! [Y] : ( ~ r1(X,Y) | p209(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1309(X) & ! [Y] : ( ~ r1(X,Y) | p209(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1209(X) & ! [Y] : ( ~ r1(X,Y) | p209(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1109(X) & ! [Y] : ( ~ r1(X,Y) | p209(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1009(X) & ! [Y] : ( ~ r1(X,Y) | p209(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p909(X) & ! [Y] : ( ~ r1(X,Y) | p209(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p809(Y) ) & ! [Y] : ( ~ r1(X,Y) | p209(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p709(Y) ) & ! [Y] : ( ~ r1(X,Y) | p209(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p609(Y) ) & ! [Y] : ( ~ r1(X,Y) | p209(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p509(Y) ) & ! [Y] : ( ~ r1(X,Y) | p209(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p409(Y) ) & ! [Y] : ( ~ r1(X,Y) | p209(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p309(Y) ) & ! [Y] : ( ~ r1(X,Y) | p209(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1609(X) & ! [Y] : ( ~ r1(X,Y) | p109(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1509(X) & ! [Y] : ( ~ r1(X,Y) | p109(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1409(X) & ! [Y] : ( ~ r1(X,Y) | p109(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1309(X) & ! [Y] : ( ~ r1(X,Y) | p109(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1209(X) & ! [Y] : ( ~ r1(X,Y) | p109(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1109(X) & ! [Y] : ( ~ r1(X,Y) | p109(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1009(X) & ! [Y] : ( ~ r1(X,Y) | p109(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p909(X) & ! [Y] : ( ~ r1(X,Y) | p109(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p809(Y) ) & ! [Y] : ( ~ r1(X,Y) | p109(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p709(Y) ) & ! [Y] : ( ~ r1(X,Y) | p109(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p609(Y) ) & ! [Y] : ( ~ r1(X,Y) | p109(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p509(Y) ) & ! [Y] : ( ~ r1(X,Y) | p109(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p409(Y) ) & ! [Y] : ( ~ r1(X,Y) | p109(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p309(Y) ) & ! [Y] : ( ~ r1(X,Y) | p109(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p209(Y) ) & ! [Y] : ( ~ r1(X,Y) | p109(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1608(X) & p1508(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1608(X) & p1408(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1508(X) & p1408(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1608(X) & p1308(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1508(X) & p1308(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1408(X) & p1308(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1608(X) & p1208(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1508(X) & p1208(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1408(X) & p1208(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1308(X) & p1208(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1608(X) & p1108(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1508(X) & p1108(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1408(X) & p1108(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1308(X) & p1108(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1208(X) & p1108(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1608(X) & p1008(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1508(X) & p1008(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1408(X) & p1008(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1308(X) & p1008(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1208(X) & p1008(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1108(X) & p1008(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1608(X) & p908(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1508(X) & p908(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1408(X) & p908(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1308(X) & p908(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1208(X) & p908(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1108(X) & p908(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1008(X) & p908(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1608(X) & p808(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1508(X) & p808(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1408(X) & p808(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1308(X) & p808(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1208(X) & p808(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1108(X) & p808(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1008(X) & p808(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p908(X) & p808(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1608(X) & ! [Y] : ( ~ r1(X,Y) | p708(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1508(X) & ! [Y] : ( ~ r1(X,Y) | p708(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1408(X) & ! [Y] : ( ~ r1(X,Y) | p708(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1308(X) & ! [Y] : ( ~ r1(X,Y) | p708(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1208(X) & ! [Y] : ( ~ r1(X,Y) | p708(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1108(X) & ! [Y] : ( ~ r1(X,Y) | p708(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1008(X) & ! [Y] : ( ~ r1(X,Y) | p708(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p908(X) & ! [Y] : ( ~ r1(X,Y) | p708(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p808(X) & ! [Y] : ( ~ r1(X,Y) | p708(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1608(X) & ! [Y] : ( ~ r1(X,Y) | p608(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1508(X) & ! [Y] : ( ~ r1(X,Y) | p608(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1408(X) & ! [Y] : ( ~ r1(X,Y) | p608(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1308(X) & ! [Y] : ( ~ r1(X,Y) | p608(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1208(X) & ! [Y] : ( ~ r1(X,Y) | p608(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1108(X) & ! [Y] : ( ~ r1(X,Y) | p608(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1008(X) & ! [Y] : ( ~ r1(X,Y) | p608(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p908(X) & ! [Y] : ( ~ r1(X,Y) | p608(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p808(X) & ! [Y] : ( ~ r1(X,Y) | p608(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p708(Y) ) & ! [Y] : ( ~ r1(X,Y) | p608(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1608(X) & ! [Y] : ( ~ r1(X,Y) | p508(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1508(X) & ! [Y] : ( ~ r1(X,Y) | p508(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1408(X) & ! [Y] : ( ~ r1(X,Y) | p508(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1308(X) & ! [Y] : ( ~ r1(X,Y) | p508(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1208(X) & ! [Y] : ( ~ r1(X,Y) | p508(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1108(X) & ! [Y] : ( ~ r1(X,Y) | p508(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1008(X) & ! [Y] : ( ~ r1(X,Y) | p508(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p908(X) & ! [Y] : ( ~ r1(X,Y) | p508(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p808(X) & ! [Y] : ( ~ r1(X,Y) | p508(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p708(Y) ) & ! [Y] : ( ~ r1(X,Y) | p508(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p608(Y) ) & ! [Y] : ( ~ r1(X,Y) | p508(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1608(X) & ! [Y] : ( ~ r1(X,Y) | p408(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1508(X) & ! [Y] : ( ~ r1(X,Y) | p408(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1408(X) & ! [Y] : ( ~ r1(X,Y) | p408(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1308(X) & ! [Y] : ( ~ r1(X,Y) | p408(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1208(X) & ! [Y] : ( ~ r1(X,Y) | p408(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1108(X) & ! [Y] : ( ~ r1(X,Y) | p408(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1008(X) & ! [Y] : ( ~ r1(X,Y) | p408(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p908(X) & ! [Y] : ( ~ r1(X,Y) | p408(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p808(X) & ! [Y] : ( ~ r1(X,Y) | p408(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p708(Y) ) & ! [Y] : ( ~ r1(X,Y) | p408(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p608(Y) ) & ! [Y] : ( ~ r1(X,Y) | p408(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p508(Y) ) & ! [Y] : ( ~ r1(X,Y) | p408(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1608(X) & ! [Y] : ( ~ r1(X,Y) | p308(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1508(X) & ! [Y] : ( ~ r1(X,Y) | p308(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1408(X) & ! [Y] : ( ~ r1(X,Y) | p308(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1308(X) & ! [Y] : ( ~ r1(X,Y) | p308(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1208(X) & ! [Y] : ( ~ r1(X,Y) | p308(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1108(X) & ! [Y] : ( ~ r1(X,Y) | p308(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1008(X) & ! [Y] : ( ~ r1(X,Y) | p308(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p908(X) & ! [Y] : ( ~ r1(X,Y) | p308(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p808(X) & ! [Y] : ( ~ r1(X,Y) | p308(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p708(Y) ) & ! [Y] : ( ~ r1(X,Y) | p308(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p608(Y) ) & ! [Y] : ( ~ r1(X,Y) | p308(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p508(Y) ) & ! [Y] : ( ~ r1(X,Y) | p308(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p408(Y) ) & ! [Y] : ( ~ r1(X,Y) | p308(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1608(X) & ! [Y] : ( ~ r1(X,Y) | p208(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1508(X) & ! [Y] : ( ~ r1(X,Y) | p208(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1408(X) & ! [Y] : ( ~ r1(X,Y) | p208(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1308(X) & ! [Y] : ( ~ r1(X,Y) | p208(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1208(X) & ! [Y] : ( ~ r1(X,Y) | p208(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1108(X) & ! [Y] : ( ~ r1(X,Y) | p208(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1008(X) & ! [Y] : ( ~ r1(X,Y) | p208(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p908(X) & ! [Y] : ( ~ r1(X,Y) | p208(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p808(X) & ! [Y] : ( ~ r1(X,Y) | p208(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p708(Y) ) & ! [Y] : ( ~ r1(X,Y) | p208(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p608(Y) ) & ! [Y] : ( ~ r1(X,Y) | p208(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p508(Y) ) & ! [Y] : ( ~ r1(X,Y) | p208(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p408(Y) ) & ! [Y] : ( ~ r1(X,Y) | p208(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p308(Y) ) & ! [Y] : ( ~ r1(X,Y) | p208(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1608(X) & ! [Y] : ( ~ r1(X,Y) | p108(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1508(X) & ! [Y] : ( ~ r1(X,Y) | p108(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1408(X) & ! [Y] : ( ~ r1(X,Y) | p108(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1308(X) & ! [Y] : ( ~ r1(X,Y) | p108(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1208(X) & ! [Y] : ( ~ r1(X,Y) | p108(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1108(X) & ! [Y] : ( ~ r1(X,Y) | p108(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1008(X) & ! [Y] : ( ~ r1(X,Y) | p108(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p908(X) & ! [Y] : ( ~ r1(X,Y) | p108(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p808(X) & ! [Y] : ( ~ r1(X,Y) | p108(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p708(Y) ) & ! [Y] : ( ~ r1(X,Y) | p108(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p608(Y) ) & ! [Y] : ( ~ r1(X,Y) | p108(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p508(Y) ) & ! [Y] : ( ~ r1(X,Y) | p108(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p408(Y) ) & ! [Y] : ( ~ r1(X,Y) | p108(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p308(Y) ) & ! [Y] : ( ~ r1(X,Y) | p108(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p208(Y) ) & ! [Y] : ( ~ r1(X,Y) | p108(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1607(X) & p1507(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1607(X) & p1407(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1507(X) & p1407(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1607(X) & p1307(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1507(X) & p1307(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1407(X) & p1307(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1607(X) & p1207(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1507(X) & p1207(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1407(X) & p1207(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1307(X) & p1207(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1607(X) & p1107(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1507(X) & p1107(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1407(X) & p1107(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1307(X) & p1107(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1207(X) & p1107(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1607(X) & p1007(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1507(X) & p1007(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1407(X) & p1007(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1307(X) & p1007(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1207(X) & p1007(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1107(X) & p1007(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1607(X) & p907(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1507(X) & p907(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1407(X) & p907(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1307(X) & p907(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1207(X) & p907(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1107(X) & p907(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1007(X) & p907(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1607(X) & p807(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1507(X) & p807(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1407(X) & p807(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1307(X) & p807(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1207(X) & p807(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1107(X) & p807(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1007(X) & p807(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p907(X) & p807(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1607(X) & p707(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1507(X) & p707(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1407(X) & p707(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1307(X) & p707(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1207(X) & p707(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1107(X) & p707(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1007(X) & p707(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p907(X) & p707(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p807(X) & p707(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1607(X) & ! [Y] : ( ~ r1(X,Y) | p607(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1507(X) & ! [Y] : ( ~ r1(X,Y) | p607(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1407(X) & ! [Y] : ( ~ r1(X,Y) | p607(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1307(X) & ! [Y] : ( ~ r1(X,Y) | p607(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1207(X) & ! [Y] : ( ~ r1(X,Y) | p607(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1107(X) & ! [Y] : ( ~ r1(X,Y) | p607(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1007(X) & ! [Y] : ( ~ r1(X,Y) | p607(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p907(X) & ! [Y] : ( ~ r1(X,Y) | p607(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p807(X) & ! [Y] : ( ~ r1(X,Y) | p607(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p707(X) & ! [Y] : ( ~ r1(X,Y) | p607(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1607(X) & ! [Y] : ( ~ r1(X,Y) | p507(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1507(X) & ! [Y] : ( ~ r1(X,Y) | p507(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1407(X) & ! [Y] : ( ~ r1(X,Y) | p507(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1307(X) & ! [Y] : ( ~ r1(X,Y) | p507(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1207(X) & ! [Y] : ( ~ r1(X,Y) | p507(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1107(X) & ! [Y] : ( ~ r1(X,Y) | p507(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1007(X) & ! [Y] : ( ~ r1(X,Y) | p507(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p907(X) & ! [Y] : ( ~ r1(X,Y) | p507(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p807(X) & ! [Y] : ( ~ r1(X,Y) | p507(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p707(X) & ! [Y] : ( ~ r1(X,Y) | p507(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p607(Y) ) & ! [Y] : ( ~ r1(X,Y) | p507(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1607(X) & ! [Y] : ( ~ r1(X,Y) | p407(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1507(X) & ! [Y] : ( ~ r1(X,Y) | p407(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1407(X) & ! [Y] : ( ~ r1(X,Y) | p407(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1307(X) & ! [Y] : ( ~ r1(X,Y) | p407(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1207(X) & ! [Y] : ( ~ r1(X,Y) | p407(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1107(X) & ! [Y] : ( ~ r1(X,Y) | p407(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1007(X) & ! [Y] : ( ~ r1(X,Y) | p407(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p907(X) & ! [Y] : ( ~ r1(X,Y) | p407(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p807(X) & ! [Y] : ( ~ r1(X,Y) | p407(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p707(X) & ! [Y] : ( ~ r1(X,Y) | p407(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p607(Y) ) & ! [Y] : ( ~ r1(X,Y) | p407(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p507(Y) ) & ! [Y] : ( ~ r1(X,Y) | p407(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1607(X) & ! [Y] : ( ~ r1(X,Y) | p307(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1507(X) & ! [Y] : ( ~ r1(X,Y) | p307(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1407(X) & ! [Y] : ( ~ r1(X,Y) | p307(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1307(X) & ! [Y] : ( ~ r1(X,Y) | p307(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1207(X) & ! [Y] : ( ~ r1(X,Y) | p307(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1107(X) & ! [Y] : ( ~ r1(X,Y) | p307(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1007(X) & ! [Y] : ( ~ r1(X,Y) | p307(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p907(X) & ! [Y] : ( ~ r1(X,Y) | p307(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p807(X) & ! [Y] : ( ~ r1(X,Y) | p307(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p707(X) & ! [Y] : ( ~ r1(X,Y) | p307(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p607(Y) ) & ! [Y] : ( ~ r1(X,Y) | p307(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p507(Y) ) & ! [Y] : ( ~ r1(X,Y) | p307(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p407(Y) ) & ! [Y] : ( ~ r1(X,Y) | p307(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1607(X) & ! [Y] : ( ~ r1(X,Y) | p207(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1507(X) & ! [Y] : ( ~ r1(X,Y) | p207(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1407(X) & ! [Y] : ( ~ r1(X,Y) | p207(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1307(X) & ! [Y] : ( ~ r1(X,Y) | p207(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1207(X) & ! [Y] : ( ~ r1(X,Y) | p207(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1107(X) & ! [Y] : ( ~ r1(X,Y) | p207(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1007(X) & ! [Y] : ( ~ r1(X,Y) | p207(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p907(X) & ! [Y] : ( ~ r1(X,Y) | p207(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p807(X) & ! [Y] : ( ~ r1(X,Y) | p207(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p707(X) & ! [Y] : ( ~ r1(X,Y) | p207(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p607(Y) ) & ! [Y] : ( ~ r1(X,Y) | p207(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p507(Y) ) & ! [Y] : ( ~ r1(X,Y) | p207(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p407(Y) ) & ! [Y] : ( ~ r1(X,Y) | p207(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p307(Y) ) & ! [Y] : ( ~ r1(X,Y) | p207(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1607(X) & ! [Y] : ( ~ r1(X,Y) | p107(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1507(X) & ! [Y] : ( ~ r1(X,Y) | p107(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1407(X) & ! [Y] : ( ~ r1(X,Y) | p107(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1307(X) & ! [Y] : ( ~ r1(X,Y) | p107(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1207(X) & ! [Y] : ( ~ r1(X,Y) | p107(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1107(X) & ! [Y] : ( ~ r1(X,Y) | p107(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1007(X) & ! [Y] : ( ~ r1(X,Y) | p107(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p907(X) & ! [Y] : ( ~ r1(X,Y) | p107(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p807(X) & ! [Y] : ( ~ r1(X,Y) | p107(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p707(X) & ! [Y] : ( ~ r1(X,Y) | p107(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p607(Y) ) & ! [Y] : ( ~ r1(X,Y) | p107(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p507(Y) ) & ! [Y] : ( ~ r1(X,Y) | p107(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p407(Y) ) & ! [Y] : ( ~ r1(X,Y) | p107(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p307(Y) ) & ! [Y] : ( ~ r1(X,Y) | p107(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p207(Y) ) & ! [Y] : ( ~ r1(X,Y) | p107(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1606(X) & p1506(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1606(X) & p1406(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1506(X) & p1406(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1606(X) & p1306(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1506(X) & p1306(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1406(X) & p1306(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1606(X) & p1206(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1506(X) & p1206(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1406(X) & p1206(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1306(X) & p1206(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1606(X) & p1106(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1506(X) & p1106(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1406(X) & p1106(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1306(X) & p1106(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1206(X) & p1106(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1606(X) & p1006(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1506(X) & p1006(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1406(X) & p1006(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1306(X) & p1006(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1206(X) & p1006(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1106(X) & p1006(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1606(X) & p906(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1506(X) & p906(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1406(X) & p906(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1306(X) & p906(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1206(X) & p906(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1106(X) & p906(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1006(X) & p906(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1606(X) & p806(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1506(X) & p806(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1406(X) & p806(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1306(X) & p806(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1206(X) & p806(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1106(X) & p806(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1006(X) & p806(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p906(X) & p806(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1606(X) & p706(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1506(X) & p706(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1406(X) & p706(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1306(X) & p706(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1206(X) & p706(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1106(X) & p706(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1006(X) & p706(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p906(X) & p706(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p806(X) & p706(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1606(X) & p606(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1506(X) & p606(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1406(X) & p606(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1306(X) & p606(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1206(X) & p606(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1106(X) & p606(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1006(X) & p606(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p906(X) & p606(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p806(X) & p606(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p706(X) & p606(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1606(X) & ! [Y] : ( ~ r1(X,Y) | p506(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1506(X) & ! [Y] : ( ~ r1(X,Y) | p506(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1406(X) & ! [Y] : ( ~ r1(X,Y) | p506(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1306(X) & ! [Y] : ( ~ r1(X,Y) | p506(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1206(X) & ! [Y] : ( ~ r1(X,Y) | p506(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1106(X) & ! [Y] : ( ~ r1(X,Y) | p506(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1006(X) & ! [Y] : ( ~ r1(X,Y) | p506(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p906(X) & ! [Y] : ( ~ r1(X,Y) | p506(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p806(X) & ! [Y] : ( ~ r1(X,Y) | p506(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p706(X) & ! [Y] : ( ~ r1(X,Y) | p506(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p606(X) & ! [Y] : ( ~ r1(X,Y) | p506(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1606(X) & ! [Y] : ( ~ r1(X,Y) | p406(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1506(X) & ! [Y] : ( ~ r1(X,Y) | p406(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1406(X) & ! [Y] : ( ~ r1(X,Y) | p406(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1306(X) & ! [Y] : ( ~ r1(X,Y) | p406(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1206(X) & ! [Y] : ( ~ r1(X,Y) | p406(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1106(X) & ! [Y] : ( ~ r1(X,Y) | p406(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1006(X) & ! [Y] : ( ~ r1(X,Y) | p406(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p906(X) & ! [Y] : ( ~ r1(X,Y) | p406(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p806(X) & ! [Y] : ( ~ r1(X,Y) | p406(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p706(X) & ! [Y] : ( ~ r1(X,Y) | p406(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p606(X) & ! [Y] : ( ~ r1(X,Y) | p406(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p506(Y) ) & ! [Y] : ( ~ r1(X,Y) | p406(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1606(X) & ! [Y] : ( ~ r1(X,Y) | p306(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1506(X) & ! [Y] : ( ~ r1(X,Y) | p306(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1406(X) & ! [Y] : ( ~ r1(X,Y) | p306(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1306(X) & ! [Y] : ( ~ r1(X,Y) | p306(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1206(X) & ! [Y] : ( ~ r1(X,Y) | p306(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1106(X) & ! [Y] : ( ~ r1(X,Y) | p306(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1006(X) & ! [Y] : ( ~ r1(X,Y) | p306(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p906(X) & ! [Y] : ( ~ r1(X,Y) | p306(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p806(X) & ! [Y] : ( ~ r1(X,Y) | p306(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p706(X) & ! [Y] : ( ~ r1(X,Y) | p306(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p606(X) & ! [Y] : ( ~ r1(X,Y) | p306(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p506(Y) ) & ! [Y] : ( ~ r1(X,Y) | p306(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p406(Y) ) & ! [Y] : ( ~ r1(X,Y) | p306(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1606(X) & ! [Y] : ( ~ r1(X,Y) | p206(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1506(X) & ! [Y] : ( ~ r1(X,Y) | p206(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1406(X) & ! [Y] : ( ~ r1(X,Y) | p206(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1306(X) & ! [Y] : ( ~ r1(X,Y) | p206(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1206(X) & ! [Y] : ( ~ r1(X,Y) | p206(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1106(X) & ! [Y] : ( ~ r1(X,Y) | p206(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1006(X) & ! [Y] : ( ~ r1(X,Y) | p206(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p906(X) & ! [Y] : ( ~ r1(X,Y) | p206(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p806(X) & ! [Y] : ( ~ r1(X,Y) | p206(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p706(X) & ! [Y] : ( ~ r1(X,Y) | p206(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p606(X) & ! [Y] : ( ~ r1(X,Y) | p206(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p506(Y) ) & ! [Y] : ( ~ r1(X,Y) | p206(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p406(Y) ) & ! [Y] : ( ~ r1(X,Y) | p206(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p306(Y) ) & ! [Y] : ( ~ r1(X,Y) | p206(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1606(X) & ! [Y] : ( ~ r1(X,Y) | p106(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1506(X) & ! [Y] : ( ~ r1(X,Y) | p106(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1406(X) & ! [Y] : ( ~ r1(X,Y) | p106(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1306(X) & ! [Y] : ( ~ r1(X,Y) | p106(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1206(X) & ! [Y] : ( ~ r1(X,Y) | p106(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1106(X) & ! [Y] : ( ~ r1(X,Y) | p106(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1006(X) & ! [Y] : ( ~ r1(X,Y) | p106(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p906(X) & ! [Y] : ( ~ r1(X,Y) | p106(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p806(X) & ! [Y] : ( ~ r1(X,Y) | p106(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p706(X) & ! [Y] : ( ~ r1(X,Y) | p106(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p606(X) & ! [Y] : ( ~ r1(X,Y) | p106(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p506(Y) ) & ! [Y] : ( ~ r1(X,Y) | p106(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p406(Y) ) & ! [Y] : ( ~ r1(X,Y) | p106(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p306(Y) ) & ! [Y] : ( ~ r1(X,Y) | p106(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p206(Y) ) & ! [Y] : ( ~ r1(X,Y) | p106(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1605(X) & p1505(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1605(X) & p1405(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1505(X) & p1405(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1605(X) & p1305(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1505(X) & p1305(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1405(X) & p1305(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1605(X) & p1205(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1505(X) & p1205(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1405(X) & p1205(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1305(X) & p1205(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1605(X) & p1105(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1505(X) & p1105(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1405(X) & p1105(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1305(X) & p1105(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1205(X) & p1105(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1605(X) & p1005(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1505(X) & p1005(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1405(X) & p1005(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1305(X) & p1005(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1205(X) & p1005(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1105(X) & p1005(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1605(X) & p905(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1505(X) & p905(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1405(X) & p905(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1305(X) & p905(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1205(X) & p905(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1105(X) & p905(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1005(X) & p905(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1605(X) & p805(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1505(X) & p805(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1405(X) & p805(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1305(X) & p805(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1205(X) & p805(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1105(X) & p805(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1005(X) & p805(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p905(X) & p805(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1605(X) & p705(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1505(X) & p705(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1405(X) & p705(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1305(X) & p705(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1205(X) & p705(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1105(X) & p705(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1005(X) & p705(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p905(X) & p705(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p805(X) & p705(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1605(X) & p605(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1505(X) & p605(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1405(X) & p605(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1305(X) & p605(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1205(X) & p605(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1105(X) & p605(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1005(X) & p605(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p905(X) & p605(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p805(X) & p605(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p705(X) & p605(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1605(X) & p505(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1505(X) & p505(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1405(X) & p505(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1305(X) & p505(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1205(X) & p505(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1105(X) & p505(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1005(X) & p505(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p905(X) & p505(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p805(X) & p505(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p705(X) & p505(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p605(X) & p505(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1605(X) & ! [Y] : ( ~ r1(X,Y) | p405(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1505(X) & ! [Y] : ( ~ r1(X,Y) | p405(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1405(X) & ! [Y] : ( ~ r1(X,Y) | p405(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1305(X) & ! [Y] : ( ~ r1(X,Y) | p405(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1205(X) & ! [Y] : ( ~ r1(X,Y) | p405(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1105(X) & ! [Y] : ( ~ r1(X,Y) | p405(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1005(X) & ! [Y] : ( ~ r1(X,Y) | p405(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p905(X) & ! [Y] : ( ~ r1(X,Y) | p405(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p805(X) & ! [Y] : ( ~ r1(X,Y) | p405(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p705(X) & ! [Y] : ( ~ r1(X,Y) | p405(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p605(X) & ! [Y] : ( ~ r1(X,Y) | p405(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p505(X) & ! [Y] : ( ~ r1(X,Y) | p405(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1605(X) & ! [Y] : ( ~ r1(X,Y) | p305(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1505(X) & ! [Y] : ( ~ r1(X,Y) | p305(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1405(X) & ! [Y] : ( ~ r1(X,Y) | p305(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1305(X) & ! [Y] : ( ~ r1(X,Y) | p305(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1205(X) & ! [Y] : ( ~ r1(X,Y) | p305(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1105(X) & ! [Y] : ( ~ r1(X,Y) | p305(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1005(X) & ! [Y] : ( ~ r1(X,Y) | p305(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p905(X) & ! [Y] : ( ~ r1(X,Y) | p305(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p805(X) & ! [Y] : ( ~ r1(X,Y) | p305(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p705(X) & ! [Y] : ( ~ r1(X,Y) | p305(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p605(X) & ! [Y] : ( ~ r1(X,Y) | p305(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p505(X) & ! [Y] : ( ~ r1(X,Y) | p305(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p405(Y) ) & ! [Y] : ( ~ r1(X,Y) | p305(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1605(X) & ! [Y] : ( ~ r1(X,Y) | p205(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1505(X) & ! [Y] : ( ~ r1(X,Y) | p205(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1405(X) & ! [Y] : ( ~ r1(X,Y) | p205(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1305(X) & ! [Y] : ( ~ r1(X,Y) | p205(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1205(X) & ! [Y] : ( ~ r1(X,Y) | p205(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1105(X) & ! [Y] : ( ~ r1(X,Y) | p205(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1005(X) & ! [Y] : ( ~ r1(X,Y) | p205(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p905(X) & ! [Y] : ( ~ r1(X,Y) | p205(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p805(X) & ! [Y] : ( ~ r1(X,Y) | p205(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p705(X) & ! [Y] : ( ~ r1(X,Y) | p205(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p605(X) & ! [Y] : ( ~ r1(X,Y) | p205(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p505(X) & ! [Y] : ( ~ r1(X,Y) | p205(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p405(Y) ) & ! [Y] : ( ~ r1(X,Y) | p205(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p305(Y) ) & ! [Y] : ( ~ r1(X,Y) | p205(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1605(X) & ! [Y] : ( ~ r1(X,Y) | p105(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1505(X) & ! [Y] : ( ~ r1(X,Y) | p105(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1405(X) & ! [Y] : ( ~ r1(X,Y) | p105(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1305(X) & ! [Y] : ( ~ r1(X,Y) | p105(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1205(X) & ! [Y] : ( ~ r1(X,Y) | p105(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1105(X) & ! [Y] : ( ~ r1(X,Y) | p105(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1005(X) & ! [Y] : ( ~ r1(X,Y) | p105(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p905(X) & ! [Y] : ( ~ r1(X,Y) | p105(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p805(X) & ! [Y] : ( ~ r1(X,Y) | p105(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p705(X) & ! [Y] : ( ~ r1(X,Y) | p105(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p605(X) & ! [Y] : ( ~ r1(X,Y) | p105(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p505(X) & ! [Y] : ( ~ r1(X,Y) | p105(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p405(Y) ) & ! [Y] : ( ~ r1(X,Y) | p105(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p305(Y) ) & ! [Y] : ( ~ r1(X,Y) | p105(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p205(Y) ) & ! [Y] : ( ~ r1(X,Y) | p105(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1604(X) & p1504(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1604(X) & p1404(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1504(X) & p1404(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1604(X) & p1304(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1504(X) & p1304(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1404(X) & p1304(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1604(X) & p1204(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1504(X) & p1204(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1404(X) & p1204(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1304(X) & p1204(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1604(X) & p1104(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1504(X) & p1104(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1404(X) & p1104(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1304(X) & p1104(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1204(X) & p1104(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1604(X) & p1004(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1504(X) & p1004(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1404(X) & p1004(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1304(X) & p1004(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1204(X) & p1004(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1104(X) & p1004(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1604(X) & p904(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1504(X) & p904(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1404(X) & p904(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1304(X) & p904(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1204(X) & p904(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1104(X) & p904(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1004(X) & p904(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1604(X) & p804(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1504(X) & p804(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1404(X) & p804(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1304(X) & p804(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1204(X) & p804(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1104(X) & p804(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1004(X) & p804(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p904(X) & p804(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1604(X) & p704(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1504(X) & p704(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1404(X) & p704(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1304(X) & p704(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1204(X) & p704(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1104(X) & p704(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1004(X) & p704(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p904(X) & p704(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p804(X) & p704(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1604(X) & p604(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1504(X) & p604(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1404(X) & p604(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1304(X) & p604(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1204(X) & p604(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1104(X) & p604(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1004(X) & p604(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p904(X) & p604(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p804(X) & p604(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p704(X) & p604(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1604(X) & p504(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1504(X) & p504(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1404(X) & p504(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1304(X) & p504(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1204(X) & p504(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1104(X) & p504(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1004(X) & p504(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p904(X) & p504(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p804(X) & p504(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p704(X) & p504(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p604(X) & p504(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1604(X) & p404(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1504(X) & p404(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1404(X) & p404(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1304(X) & p404(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1204(X) & p404(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1104(X) & p404(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1004(X) & p404(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p904(X) & p404(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p804(X) & p404(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p704(X) & p404(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p604(X) & p404(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p504(X) & p404(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1604(X) & ! [Y] : ( ~ r1(X,Y) | p304(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1504(X) & ! [Y] : ( ~ r1(X,Y) | p304(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1404(X) & ! [Y] : ( ~ r1(X,Y) | p304(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1304(X) & ! [Y] : ( ~ r1(X,Y) | p304(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1204(X) & ! [Y] : ( ~ r1(X,Y) | p304(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1104(X) & ! [Y] : ( ~ r1(X,Y) | p304(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1004(X) & ! [Y] : ( ~ r1(X,Y) | p304(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p904(X) & ! [Y] : ( ~ r1(X,Y) | p304(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p804(X) & ! [Y] : ( ~ r1(X,Y) | p304(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p704(X) & ! [Y] : ( ~ r1(X,Y) | p304(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p604(X) & ! [Y] : ( ~ r1(X,Y) | p304(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p504(X) & ! [Y] : ( ~ r1(X,Y) | p304(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p404(X) & ! [Y] : ( ~ r1(X,Y) | p304(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1604(X) & ! [Y] : ( ~ r1(X,Y) | p204(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1504(X) & ! [Y] : ( ~ r1(X,Y) | p204(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1404(X) & ! [Y] : ( ~ r1(X,Y) | p204(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1304(X) & ! [Y] : ( ~ r1(X,Y) | p204(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1204(X) & ! [Y] : ( ~ r1(X,Y) | p204(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1104(X) & ! [Y] : ( ~ r1(X,Y) | p204(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1004(X) & ! [Y] : ( ~ r1(X,Y) | p204(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p904(X) & ! [Y] : ( ~ r1(X,Y) | p204(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p804(X) & ! [Y] : ( ~ r1(X,Y) | p204(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p704(X) & ! [Y] : ( ~ r1(X,Y) | p204(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p604(X) & ! [Y] : ( ~ r1(X,Y) | p204(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p504(X) & ! [Y] : ( ~ r1(X,Y) | p204(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p404(X) & ! [Y] : ( ~ r1(X,Y) | p204(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p304(Y) ) & ! [Y] : ( ~ r1(X,Y) | p204(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1604(X) & ! [Y] : ( ~ r1(X,Y) | p104(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1504(X) & ! [Y] : ( ~ r1(X,Y) | p104(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1404(X) & ! [Y] : ( ~ r1(X,Y) | p104(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1304(X) & ! [Y] : ( ~ r1(X,Y) | p104(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1204(X) & ! [Y] : ( ~ r1(X,Y) | p104(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1104(X) & ! [Y] : ( ~ r1(X,Y) | p104(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1004(X) & ! [Y] : ( ~ r1(X,Y) | p104(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p904(X) & ! [Y] : ( ~ r1(X,Y) | p104(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p804(X) & ! [Y] : ( ~ r1(X,Y) | p104(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p704(X) & ! [Y] : ( ~ r1(X,Y) | p104(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p604(X) & ! [Y] : ( ~ r1(X,Y) | p104(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p504(X) & ! [Y] : ( ~ r1(X,Y) | p104(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p404(X) & ! [Y] : ( ~ r1(X,Y) | p104(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p304(Y) ) & ! [Y] : ( ~ r1(X,Y) | p104(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p204(Y) ) & ! [Y] : ( ~ r1(X,Y) | p104(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1603(X) & p1503(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1603(X) & p1403(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1503(X) & p1403(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1603(X) & p1303(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1503(X) & p1303(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1403(X) & p1303(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1603(X) & p1203(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1503(X) & p1203(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1403(X) & p1203(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1303(X) & p1203(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1603(X) & p1103(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1503(X) & p1103(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1403(X) & p1103(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1303(X) & p1103(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1203(X) & p1103(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1603(X) & p1003(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1503(X) & p1003(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1403(X) & p1003(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1303(X) & p1003(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1203(X) & p1003(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1103(X) & p1003(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1603(X) & p903(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1503(X) & p903(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1403(X) & p903(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1303(X) & p903(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1203(X) & p903(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1103(X) & p903(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1003(X) & p903(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1603(X) & p803(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1503(X) & p803(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1403(X) & p803(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1303(X) & p803(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1203(X) & p803(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1103(X) & p803(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1003(X) & p803(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p903(X) & p803(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1603(X) & p703(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1503(X) & p703(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1403(X) & p703(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1303(X) & p703(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1203(X) & p703(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1103(X) & p703(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1003(X) & p703(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p903(X) & p703(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p803(X) & p703(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1603(X) & p603(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1503(X) & p603(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1403(X) & p603(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1303(X) & p603(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1203(X) & p603(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1103(X) & p603(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1003(X) & p603(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p903(X) & p603(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p803(X) & p603(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p703(X) & p603(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1603(X) & p503(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1503(X) & p503(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1403(X) & p503(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1303(X) & p503(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1203(X) & p503(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1103(X) & p503(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1003(X) & p503(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p903(X) & p503(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p803(X) & p503(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p703(X) & p503(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p603(X) & p503(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1603(X) & p403(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1503(X) & p403(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1403(X) & p403(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1303(X) & p403(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1203(X) & p403(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1103(X) & p403(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1003(X) & p403(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p903(X) & p403(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p803(X) & p403(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p703(X) & p403(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p603(X) & p403(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p503(X) & p403(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1603(X) & p303(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1503(X) & p303(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1403(X) & p303(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1303(X) & p303(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1203(X) & p303(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1103(X) & p303(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1003(X) & p303(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p903(X) & p303(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p803(X) & p303(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p703(X) & p303(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p603(X) & p303(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p503(X) & p303(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p403(X) & p303(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1603(X) & ! [Y] : ( ~ r1(X,Y) | p203(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1503(X) & ! [Y] : ( ~ r1(X,Y) | p203(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1403(X) & ! [Y] : ( ~ r1(X,Y) | p203(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1303(X) & ! [Y] : ( ~ r1(X,Y) | p203(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1203(X) & ! [Y] : ( ~ r1(X,Y) | p203(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1103(X) & ! [Y] : ( ~ r1(X,Y) | p203(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1003(X) & ! [Y] : ( ~ r1(X,Y) | p203(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p903(X) & ! [Y] : ( ~ r1(X,Y) | p203(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p803(X) & ! [Y] : ( ~ r1(X,Y) | p203(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p703(X) & ! [Y] : ( ~ r1(X,Y) | p203(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p603(X) & ! [Y] : ( ~ r1(X,Y) | p203(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p503(X) & ! [Y] : ( ~ r1(X,Y) | p203(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p403(X) & ! [Y] : ( ~ r1(X,Y) | p203(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p303(X) & ! [Y] : ( ~ r1(X,Y) | p203(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1603(X) & ! [Y] : ( ~ r1(X,Y) | p103(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1503(X) & ! [Y] : ( ~ r1(X,Y) | p103(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1403(X) & ! [Y] : ( ~ r1(X,Y) | p103(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1303(X) & ! [Y] : ( ~ r1(X,Y) | p103(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1203(X) & ! [Y] : ( ~ r1(X,Y) | p103(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1103(X) & ! [Y] : ( ~ r1(X,Y) | p103(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1003(X) & ! [Y] : ( ~ r1(X,Y) | p103(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p903(X) & ! [Y] : ( ~ r1(X,Y) | p103(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p803(X) & ! [Y] : ( ~ r1(X,Y) | p103(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p703(X) & ! [Y] : ( ~ r1(X,Y) | p103(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p603(X) & ! [Y] : ( ~ r1(X,Y) | p103(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p503(X) & ! [Y] : ( ~ r1(X,Y) | p103(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p403(X) & ! [Y] : ( ~ r1(X,Y) | p103(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p303(X) & ! [Y] : ( ~ r1(X,Y) | p103(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( ! [Y] : ( ~ r1(X,Y) | p203(Y) ) & ! [Y] : ( ~ r1(X,Y) | p103(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1602(X) & p1502(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1602(X) & p1402(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1502(X) & p1402(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1602(X) & p1302(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1502(X) & p1302(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1402(X) & p1302(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1602(X) & p1202(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1502(X) & p1202(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1402(X) & p1202(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1302(X) & p1202(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1602(X) & p1102(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1502(X) & p1102(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1402(X) & p1102(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1302(X) & p1102(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1202(X) & p1102(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1602(X) & p1002(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1502(X) & p1002(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1402(X) & p1002(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1302(X) & p1002(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1202(X) & p1002(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1102(X) & p1002(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1602(X) & p902(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1502(X) & p902(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1402(X) & p902(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1302(X) & p902(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1202(X) & p902(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1102(X) & p902(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1002(X) & p902(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1602(X) & p802(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1502(X) & p802(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1402(X) & p802(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1302(X) & p802(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1202(X) & p802(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1102(X) & p802(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1002(X) & p802(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p902(X) & p802(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1602(X) & p702(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1502(X) & p702(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1402(X) & p702(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1302(X) & p702(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1202(X) & p702(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1102(X) & p702(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1002(X) & p702(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p902(X) & p702(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p802(X) & p702(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1602(X) & p602(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1502(X) & p602(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1402(X) & p602(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1302(X) & p602(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1202(X) & p602(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1102(X) & p602(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1002(X) & p602(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p902(X) & p602(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p802(X) & p602(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p702(X) & p602(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1602(X) & p502(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1502(X) & p502(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1402(X) & p502(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1302(X) & p502(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1202(X) & p502(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1102(X) & p502(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1002(X) & p502(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p902(X) & p502(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p802(X) & p502(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p702(X) & p502(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p602(X) & p502(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1602(X) & p402(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1502(X) & p402(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1402(X) & p402(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1302(X) & p402(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1202(X) & p402(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1102(X) & p402(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1002(X) & p402(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p902(X) & p402(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p802(X) & p402(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p702(X) & p402(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p602(X) & p402(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p502(X) & p402(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1602(X) & p302(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1502(X) & p302(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1402(X) & p302(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1302(X) & p302(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1202(X) & p302(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1102(X) & p302(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1002(X) & p302(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p902(X) & p302(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p802(X) & p302(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p702(X) & p302(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p602(X) & p302(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p502(X) & p302(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p402(X) & p302(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1602(X) & p202(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1502(X) & p202(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1402(X) & p202(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1302(X) & p202(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1202(X) & p202(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1102(X) & p202(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1002(X) & p202(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p902(X) & p202(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p802(X) & p202(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p702(X) & p202(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p602(X) & p202(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p502(X) & p202(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p402(X) & p202(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p302(X) & p202(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1602(X) & ! [Y] : ( ~ r1(X,Y) | p102(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1502(X) & ! [Y] : ( ~ r1(X,Y) | p102(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1402(X) & ! [Y] : ( ~ r1(X,Y) | p102(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1302(X) & ! [Y] : ( ~ r1(X,Y) | p102(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1202(X) & ! [Y] : ( ~ r1(X,Y) | p102(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1102(X) & ! [Y] : ( ~ r1(X,Y) | p102(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1002(X) & ! [Y] : ( ~ r1(X,Y) | p102(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p902(X) & ! [Y] : ( ~ r1(X,Y) | p102(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p802(X) & ! [Y] : ( ~ r1(X,Y) | p102(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p702(X) & ! [Y] : ( ~ r1(X,Y) | p102(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p602(X) & ! [Y] : ( ~ r1(X,Y) | p102(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p502(X) & ! [Y] : ( ~ r1(X,Y) | p102(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p402(X) & ! [Y] : ( ~ r1(X,Y) | p102(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p302(X) & ! [Y] : ( ~ r1(X,Y) | p102(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p202(X) & ! [Y] : ( ~ r1(X,Y) | p102(Y) ) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1601(X) & p1501(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1601(X) & p1401(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1501(X) & p1401(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1601(X) & p1301(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1501(X) & p1301(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1401(X) & p1301(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1601(X) & p1201(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1501(X) & p1201(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1401(X) & p1201(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1301(X) & p1201(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1601(X) & p1101(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1501(X) & p1101(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1401(X) & p1101(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1301(X) & p1101(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1201(X) & p1101(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1601(X) & p1001(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1501(X) & p1001(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1401(X) & p1001(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1301(X) & p1001(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1201(X) & p1001(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1101(X) & p1001(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1601(X) & p901(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1501(X) & p901(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1401(X) & p901(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1301(X) & p901(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1201(X) & p901(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1101(X) & p901(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1001(X) & p901(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1601(X) & p801(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1501(X) & p801(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1401(X) & p801(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1301(X) & p801(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1201(X) & p801(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1101(X) & p801(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1001(X) & p801(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p901(X) & p801(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1601(X) & p701(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1501(X) & p701(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1401(X) & p701(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1301(X) & p701(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1201(X) & p701(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1101(X) & p701(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1001(X) & p701(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p901(X) & p701(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p801(X) & p701(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1601(X) & p601(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1501(X) & p601(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1401(X) & p601(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1301(X) & p601(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1201(X) & p601(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1101(X) & p601(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1001(X) & p601(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p901(X) & p601(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p801(X) & p601(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p701(X) & p601(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1601(X) & p501(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1501(X) & p501(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1401(X) & p501(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1301(X) & p501(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1201(X) & p501(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1101(X) & p501(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1001(X) & p501(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p901(X) & p501(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p801(X) & p501(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p701(X) & p501(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p601(X) & p501(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1601(X) & p401(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1501(X) & p401(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1401(X) & p401(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1301(X) & p401(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1201(X) & p401(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1101(X) & p401(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1001(X) & p401(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p901(X) & p401(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p801(X) & p401(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p701(X) & p401(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p601(X) & p401(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p501(X) & p401(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1601(X) & p301(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1501(X) & p301(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1401(X) & p301(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1301(X) & p301(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1201(X) & p301(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1101(X) & p301(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1001(X) & p301(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p901(X) & p301(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p801(X) & p301(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p701(X) & p301(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p601(X) & p301(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p501(X) & p301(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p401(X) & p301(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1601(X) & p201(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1501(X) & p201(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1401(X) & p201(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1301(X) & p201(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1201(X) & p201(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1101(X) & p201(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1001(X) & p201(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p901(X) & p201(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p801(X) & p201(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p701(X) & p201(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p601(X) & p201(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p501(X) & p201(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p401(X) & p201(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p301(X) & p201(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1601(X) & p101(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1501(X) & p101(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1401(X) & p101(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1301(X) & p101(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1201(X) & p101(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1101(X) & p101(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p1001(X) & p101(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p901(X) & p101(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p801(X) & p101(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p701(X) & p101(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p601(X) & p101(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p501(X) & p101(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p401(X) & p101(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p301(X) & p101(X) ) ) ) | ~ ( ! [X] : ( ~ r1(Y,X) | ~ ( p201(X) & p101(X) ) ) ) ) ) ) | ~ ( ( p1615(X) | p1614(X) | p1613(X) | p1612(X) | p1611(X) | p1610(X) | p1609(X) | p1608(X) | p1607(X) | p1606(X) | p1605(X) | p1604(X) | p1603(X) | p1602(X) | p1601(X) ) & ( p1515(X) | p1514(X) | p1513(X) | p1512(X) | p1511(X) | p1510(X) | p1509(X) | p1508(X) | p1507(X) | p1506(X) | p1505(X) | p1504(X) | p1503(X) | p1502(X) | p1501(X) ) & ( ! [Y] : ( ~ r1(X,Y) | p1415(Y) ) | p1414(X) | p1413(X) | p1412(X) | p1411(X) | p1410(X) | p1409(X) | p1408(X) | p1407(X) | p1406(X) | p1405(X) | p1404(X) | p1403(X) | p1402(X) | p1401(X) ) & ( ! [Y] : ( ~ r1(X,Y) | p1315(Y) ) | ! [Y] : ( ~ r1(X,Y) | p1314(Y) ) | p1313(X) | p1312(X) | p1311(X) | p1310(X) | p1309(X) | p1308(X) | p1307(X) | p1306(X) | p1305(X) | p1304(X) | p1303(X) | p1302(X) | p1301(X) ) & ( ! [Y] : ( ~ r1(X,Y) | p1215(Y) ) | ! [Y] : ( ~ r1(X,Y) | p1214(Y) ) | ! [Y] : ( ~ r1(X,Y) | p1213(Y) ) | p1212(X) | p1211(X) | p1210(X) | p1209(X) | p1208(X) | p1207(X) | p1206(X) | p1205(X) | p1204(X) | p1203(X) | p1202(X) | p1201(X) ) & ( ! [Y] : ( ~ r1(X,Y) | p1115(Y) ) | ! [Y] : ( ~ r1(X,Y) | p1114(Y) ) | ! [Y] : ( ~ r1(X,Y) | p1113(Y) ) | ! [Y] : ( ~ r1(X,Y) | p1112(Y) ) | p1111(X) | p1110(X) | p1109(X) | p1108(X) | p1107(X) | p1106(X) | p1105(X) | p1104(X) | p1103(X) | p1102(X) | p1101(X) ) & ( ! [Y] : ( ~ r1(X,Y) | p1015(Y) ) | ! [Y] : ( ~ r1(X,Y) | p1014(Y) ) | ! [Y] : ( ~ r1(X,Y) | p1013(Y) ) | ! [Y] : ( ~ r1(X,Y) | p1012(Y) ) | ! [Y] : ( ~ r1(X,Y) | p1011(Y) ) | p1010(X) | p1009(X) | p1008(X) | p1007(X) | p1006(X) | p1005(X) | p1004(X) | p1003(X) | p1002(X) | p1001(X) ) & ( ! [Y] : ( ~ r1(X,Y) | p915(Y) ) | ! [Y] : ( ~ r1(X,Y) | p914(Y) ) | ! [Y] : ( ~ r1(X,Y) | p913(Y) ) | ! [Y] : ( ~ r1(X,Y) | p912(Y) ) | ! [Y] : ( ~ r1(X,Y) | p911(Y) ) | ! [Y] : ( ~ r1(X,Y) | p910(Y) ) | p909(X) | p908(X) | p907(X) | p906(X) | p905(X) | p904(X) | p903(X) | p902(X) | p901(X) ) & ( ! [Y] : ( ~ r1(X,Y) | p815(Y) ) | ! [Y] : ( ~ r1(X,Y) | p814(Y) ) | ! [Y] : ( ~ r1(X,Y) | p813(Y) ) | ! [Y] : ( ~ r1(X,Y) | p812(Y) ) | ! [Y] : ( ~ r1(X,Y) | p811(Y) ) | ! [Y] : ( ~ r1(X,Y) | p810(Y) ) | ! [Y] : ( ~ r1(X,Y) | p809(Y) ) | p808(X) | p807(X) | p806(X) | p805(X) | p804(X) | p803(X) | p802(X) | p801(X) ) & ( ! [Y] : ( ~ r1(X,Y) | p715(Y) ) | ! [Y] : ( ~ r1(X,Y) | p714(Y) ) | ! [Y] : ( ~ r1(X,Y) | p713(Y) ) | ! [Y] : ( ~ r1(X,Y) | p712(Y) ) | ! [Y] : ( ~ r1(X,Y) | p711(Y) ) | ! [Y] : ( ~ r1(X,Y) | p710(Y) ) | ! [Y] : ( ~ r1(X,Y) | p709(Y) ) | ! [Y] : ( ~ r1(X,Y) | p708(Y) ) | p707(X) | p706(X) | p705(X) | p704(X) | p703(X) | p702(X) | p701(X) ) & ( ! [Y] : ( ~ r1(X,Y) | p615(Y) ) | ! [Y] : ( ~ r1(X,Y) | p614(Y) ) | ! [Y] : ( ~ r1(X,Y) | p613(Y) ) | ! [Y] : ( ~ r1(X,Y) | p612(Y) ) | ! [Y] : ( ~ r1(X,Y) | p611(Y) ) | ! [Y] : ( ~ r1(X,Y) | p610(Y) ) | ! [Y] : ( ~ r1(X,Y) | p609(Y) ) | ! [Y] : ( ~ r1(X,Y) | p608(Y) ) | ! [Y] : ( ~ r1(X,Y) | p607(Y) ) | p606(X) | p605(X) | p604(X) | p603(X) | p602(X) | p601(X) ) & ( ! [Y] : ( ~ r1(X,Y) | p515(Y) ) | ! [Y] : ( ~ r1(X,Y) | p514(Y) ) | ! [Y] : ( ~ r1(X,Y) | p513(Y) ) | ! [Y] : ( ~ r1(X,Y) | p512(Y) ) | ! [Y] : ( ~ r1(X,Y) | p511(Y) ) | ! [Y] : ( ~ r1(X,Y) | p510(Y) ) | ! [Y] : ( ~ r1(X,Y) | p509(Y) ) | ! [Y] : ( ~ r1(X,Y) | p508(Y) ) | ! [Y] : ( ~ r1(X,Y) | p507(Y) ) | ! [Y] : ( ~ r1(X,Y) | p506(Y) ) | p505(X) | p504(X) | p503(X) | p502(X) | p501(X) ) & ( ! [Y] : ( ~ r1(X,Y) | p415(Y) ) | ! [Y] : ( ~ r1(X,Y) | p414(Y) ) | ! [Y] : ( ~ r1(X,Y) | p413(Y) ) | ! [Y] : ( ~ r1(X,Y) | p412(Y) ) | ! [Y] : ( ~ r1(X,Y) | p411(Y) ) | ! [Y] : ( ~ r1(X,Y) | p410(Y) ) | ! [Y] : ( ~ r1(X,Y) | p409(Y) ) | ! [Y] : ( ~ r1(X,Y) | p408(Y) ) | ! [Y] : ( ~ r1(X,Y) | p407(Y) ) | ! [Y] : ( ~ r1(X,Y) | p406(Y) ) | ! [Y] : ( ~ r1(X,Y) | p405(Y) ) | p404(X) | p403(X) | p402(X) | p401(X) ) & ( ! [Y] : ( ~ r1(X,Y) | p315(Y) ) | ! [Y] : ( ~ r1(X,Y) | p314(Y) ) | ! [Y] : ( ~ r1(X,Y) | p313(Y) ) | ! [Y] : ( ~ r1(X,Y) | p312(Y) ) | ! [Y] : ( ~ r1(X,Y) | p311(Y) ) | ! [Y] : ( ~ r1(X,Y) | p310(Y) ) | ! [Y] : ( ~ r1(X,Y) | p309(Y) ) | ! [Y] : ( ~ r1(X,Y) | p308(Y) ) | ! [Y] : ( ~ r1(X,Y) | p307(Y) ) | ! [Y] : ( ~ r1(X,Y) | p306(Y) ) | ! [Y] : ( ~ r1(X,Y) | p305(Y) ) | ! [Y] : ( ~ r1(X,Y) | p304(Y) ) | p303(X) | p302(X) | p301(X) ) & ( ! [Y] : ( ~ r1(X,Y) | p215(Y) ) | ! [Y] : ( ~ r1(X,Y) | p214(Y) ) | ! [Y] : ( ~ r1(X,Y) | p213(Y) ) | ! [Y] : ( ~ r1(X,Y) | p212(Y) ) | ! [Y] : ( ~ r1(X,Y) | p211(Y) ) | ! [Y] : ( ~ r1(X,Y) | p210(Y) ) | ! [Y] : ( ~ r1(X,Y) | p209(Y) ) | ! [Y] : ( ~ r1(X,Y) | p208(Y) ) | ! [Y] : ( ~ r1(X,Y) | p207(Y) ) | ! [Y] : ( ~ r1(X,Y) | p206(Y) ) | ! [Y] : ( ~ r1(X,Y) | p205(Y) ) | ! [Y] : ( ~ r1(X,Y) | p204(Y) ) | ! [Y] : ( ~ r1(X,Y) | p203(Y) ) | p202(X) | p201(X) ) & ( ! [Y] : ( ~ r1(X,Y) | p115(Y) ) | ! [Y] : ( ~ r1(X,Y) | p114(Y) ) | ! [Y] : ( ~ r1(X,Y) | p113(Y) ) | ! [Y] : ( ~ r1(X,Y) | p112(Y) ) | ! [Y] : ( ~ r1(X,Y) | p111(Y) ) | ! [Y] : ( ~ r1(X,Y) | p110(Y) ) | ! [Y] : ( ~ r1(X,Y) | p109(Y) ) | ! [Y] : ( ~ r1(X,Y) | p108(Y) ) | ! [Y] : ( ~ r1(X,Y) | p107(Y) ) | ! [Y] : ( ~ r1(X,Y) | p106(Y) ) | ! [Y] : ( ~ r1(X,Y) | p105(Y) ) | ! [Y] : ( ~ r1(X,Y) | p104(Y) ) | ! [Y] : ( ~ r1(X,Y) | p103(Y) ) | ! [Y] : ( ~ r1(X,Y) | p102(Y) ) | p101(X) ) ) ) ) )).
