%------------------------------------------------------------------------------
% File : Mace4---2026-6A
% Problem : SYN912-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : mace4 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 09:36:03 AM UTC 2026
% Result : Satisfiable 1.20s 0.60s
% Output : FiniteModel 1.20s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(interp_domain,interpretation-domains,
! [X] :
( X = "d1"
| X = "d0" ) ).
fof(interp_functions,interpretation-mappings,
( skf99("d1") = "d0"
& skf99("d0") = "d1"
& skf98("d1") = "d0"
& skf98("d0") = "d1"
& skf97("d1") = "d0"
& skf97("d0") = "d1"
& skf96("d1") = "d0"
& skf96("d0") = "d1"
& skf95("d1") = "d0"
& skf95("d0") = "d1"
& skf94("d1") = "d0"
& skf94("d0") = "d1"
& skf93("d1") = "d0"
& skf93("d0") = "d1"
& skf92("d1") = "d0"
& skf92("d0") = "d1"
& skf91("d1") = "d0"
& skf91("d0") = "d1"
& skf90("d1") = "d0"
& skf90("d0") = "d1"
& skf89("d1") = "d0"
& skf89("d0") = "d1"
& skf88("d1") = "d0"
& skf88("d0") = "d1"
& skf87("d1") = "d0"
& skf87("d0") = "d1"
& skf86("d1") = "d1"
& skf86("d0") = "d0"
& skf85("d1") = "d0"
& skf85("d0") = "d1"
& skf84("d1") = "d1"
& skf84("d0") = "d0"
& skf83("d1") = "d1"
& skf83("d0") = "d0"
& skf82("d1") = "d1"
& skf82("d0") = "d0"
& skf81("d1") = "d1"
& skf81("d0") = "d0"
& skf80("d1") = "d0"
& skf80("d0") = "d1"
& skf79("d1") = "d1"
& skf79("d0") = "d0"
& skf78("d1") = "d1"
& skf78("d0") = "d0"
& skf77("d1") = "d0"
& skf77("d0") = "d1"
& skf76("d1") = "d1"
& skf76("d0") = "d0"
& skf75("d1") = "d1"
& skf75("d0") = "d0"
& skf74("d1") = "d1"
& skf74("d0") = "d0"
& skf73("d1") = "d1"
& skf73("d0") = "d0"
& skf72("d1") = "d1"
& skf72("d0") = "d0"
& skf71("d1") = "d1"
& skf71("d0") = "d0"
& skf70("d1") = "d0"
& skf70("d0") = "d0"
& skf139("d1") = "d0"
& skf139("d0") = "d0"
& skf138("d1") = "d0"
& skf138("d0") = "d0"
& skf137("d1") = "d0"
& skf137("d0") = "d0"
& skf136("d1") = "d0"
& skf136("d0") = "d0"
& skf135("d1") = "d0"
& skf135("d0") = "d0"
& skf134("d1") = "d0"
& skf134("d0") = "d0"
& skf133("d1") = "d0"
& skf133("d0") = "d0"
& skf132("d1") = "d0"
& skf132("d0") = "d0"
& skf131("d1") = "d0"
& skf131("d0") = "d0"
& skf130("d1") = "d0"
& skf130("d0") = "d0"
& skf129("d1") = "d0"
& skf129("d0") = "d0"
& skf128("d1") = "d0"
& skf128("d0") = "d0"
& skf127("d1") = "d0"
& skf127("d0") = "d0"
& skf126("d1") = "d0"
& skf126("d0") = "d0"
& skf125("d1") = "d0"
& skf125("d0") = "d0"
& skf124("d1") = "d0"
& skf124("d0") = "d0"
& skf123("d1") = "d0"
& skf123("d0") = "d0"
& skf122("d1") = "d0"
& skf122("d0") = "d0"
& skf121("d1") = "d0"
& skf121("d0") = "d0"
& skf120("d1") = "d0"
& skf120("d0") = "d0"
& skf119("d1") = "d0"
& skf119("d0") = "d0"
& skf118("d1") = "d0"
& skf118("d0") = "d0"
& skf117("d1") = "d0"
& skf117("d0") = "d0"
& skf116("d1") = "d0"
& skf116("d0") = "d0"
& skf115("d1") = "d0"
& skf115("d0") = "d0"
& skf114("d1") = "d0"
& skf114("d0") = "d0"
& skf113("d1") = "d0"
& skf113("d0") = "d0"
& skf112("d1") = "d0"
& skf112("d0") = "d0"
& skf111("d1") = "d0"
& skf111("d0") = "d0"
& skf110("d1") = "d0"
& skf110("d0") = "d0"
& skf109("d1") = "d0"
& skf109("d0") = "d0"
& skf108("d1") = "d0"
& skf108("d0") = "d0"
& skf107("d1") = "d0"
& skf107("d0") = "d0"
& skf106("d1") = "d0"
& skf106("d0") = "d0"
& skf105("d1") = "d0"
& skf105("d0") = "d0"
& skf104("d1") = "d0"
& skf104("d0") = "d0"
& skf103("d1") = "d0"
& skf103("d0") = "d0"
& skf102("d1") = "d0"
& skf102("d0") = "d0"
& skf101("d1") = "d0"
& skf101("d0") = "d0"
& skf100("d1") = "d0"
& skf100("d0") = "d0"
& skc81 = "d0"
& skc80 = "d0"
& skc79 = "d0"
& skc78 = "d0"
& skc77 = "d0"
& skc76 = "d0"
& skc75 = "d0"
& skc74 = "d0"
& skc73 = "d0"
& skc72 = "d0"
& skc71 = "d0"
& skc70 = "d0"
& skc69 = "d0"
& skc68 = "d0"
& skc67 = "d0"
& skc66 = "d0"
& skc65 = "d0"
& skc64 = "d0"
& skc63 = "d0"
& skc62 = "d0"
& skc61 = "d0"
& skc60 = "d0"
& skc59 = "d0"
& skc58 = "d0"
& skc57 = "d0"
& skc56 = "d0"
& skc55 = "d0"
& skc54 = "d0"
& skc53 = "d0"
& skc52 = "d0"
& skc51 = "d0"
& skc50 = "d0"
& skc49 = "d0"
& skc48 = "d0"
& skc47 = "d0"
& skc46 = "d0"
& skc45 = "d0"
& skc44 = "d0"
& skc43 = "d0"
& skc42 = "d0"
& skc41 = "d0" ) ).
fof(interp_relations,interpretation-mappings,
( ssSkP988("d1","d1")
& ssSkP988("d1","d0")
& ssSkP988("d0","d1")
& ssSkP988("d0","d0")
& ssSkP987("d1","d1")
& ssSkP987("d1","d0")
& ssSkP987("d0","d1")
& ssSkP987("d0","d0")
& ssSkP956("d1","d1")
& ssSkP956("d1","d0")
& ssSkP956("d0","d1")
& ssSkP956("d0","d0")
& ssSkP955("d1","d1")
& ssSkP955("d1","d0")
& ssSkP955("d0","d1")
& ssSkP955("d0","d0")
& ssSkP915("d1","d1")
& ssSkP915("d1","d0")
& ssSkP915("d0","d1")
& ssSkP915("d0","d0")
& ssSkP914("d1","d1")
& ssSkP914("d1","d0")
& ssSkP914("d0","d1")
& ssSkP914("d0","d0")
& ssSkP88("d1","d1")
& ssSkP88("d1","d0")
& ssSkP88("d0","d1")
& ssSkP88("d0","d0")
& ssSkP875("d1","d1")
& ssSkP875("d1","d0")
& ssSkP875("d0","d1")
& ssSkP875("d0","d0")
& ssSkP874("d1","d1")
& ssSkP874("d1","d0")
& ssSkP874("d0","d1")
& ssSkP874("d0","d0")
& ssSkP87("d1","d1")
& ssSkP87("d1","d0")
& ssSkP87("d0","d1")
& ssSkP87("d0","d0")
& ssSkP834("d1","d1")
& ssSkP834("d1","d0")
& ssSkP834("d0","d1")
& ssSkP834("d0","d0")
& ssSkP833("d1","d1")
& ssSkP833("d1","d0")
& ssSkP833("d0","d1")
& ssSkP833("d0","d0")
& ssSkP793("d1","d1")
& ssSkP793("d1","d0")
& ssSkP793("d0","d1")
& ssSkP793("d0","d0")
& ssSkP792("d1","d1")
& ssSkP792("d1","d0")
& ssSkP792("d0","d1")
& ssSkP792("d0","d0")
& ssSkP749("d1","d1")
& ssSkP749("d1","d0")
& ssSkP749("d0","d1")
& ssSkP749("d0","d0")
& ssSkP748("d1","d1")
& ssSkP748("d1","d0")
& ssSkP748("d0","d1")
& ssSkP748("d0","d0")
& ssSkP712("d1","d1")
& ssSkP712("d1","d0")
& ssSkP712("d0","d1")
& ssSkP712("d0","d0")
& ssSkP711("d1","d1")
& ssSkP711("d1","d0")
& ssSkP711("d0","d1")
& ssSkP711("d0","d0")
& ssSkP668("d1","d1")
& ssSkP668("d1","d0")
& ssSkP668("d0","d1")
& ssSkP668("d0","d0")
& ssSkP667("d1","d1")
& ssSkP667("d1","d0")
& ssSkP667("d0","d1")
& ssSkP667("d0","d0")
& ssSkP646("d1","d1")
& ssSkP646("d1","d0")
& ssSkP646("d0","d1")
& ssSkP646("d0","d0")
& ssSkP645("d1","d1")
& ssSkP645("d1","d0")
& ssSkP645("d0","d1")
& ssSkP645("d0","d0")
& ssSkP607("d1","d1")
& ssSkP607("d1","d0")
& ssSkP607("d0","d1")
& ssSkP607("d0","d0")
& ssSkP606("d1","d1")
& ssSkP606("d1","d0")
& ssSkP606("d0","d1")
& ssSkP606("d0","d0")
& ssSkP573("d1","d1")
& ssSkP573("d1","d0")
& ssSkP573("d0","d1")
& ssSkP573("d0","d0")
& ssSkP572("d1","d1")
& ssSkP572("d1","d0")
& ssSkP572("d0","d1")
& ssSkP572("d0","d0")
& ssSkP57("d1","d1")
& ssSkP57("d1","d0")
& ssSkP57("d0","d1")
& ssSkP57("d0","d0")
& ssSkP56("d1","d1")
& ssSkP56("d1","d0")
& ssSkP56("d0","d1")
& ssSkP56("d0","d0")
& ssSkP531("d1","d1")
& ssSkP531("d1","d0")
& ssSkP531("d0","d1")
& ssSkP531("d0","d0")
& ssSkP530("d1","d1")
& ssSkP530("d1","d0")
& ssSkP530("d0","d1")
& ssSkP530("d0","d0")
& ssSkP496("d1","d1")
& ssSkP496("d1","d0")
& ssSkP496("d0","d1")
& ssSkP496("d0","d0")
& ssSkP495("d1","d1")
& ssSkP495("d1","d0")
& ssSkP495("d0","d1")
& ssSkP495("d0","d0")
& ssSkP458("d1","d1")
& ssSkP458("d1","d0")
& ssSkP458("d0","d1")
& ssSkP458("d0","d0")
& ssSkP457("d1","d1")
& ssSkP457("d1","d0")
& ssSkP457("d0","d1")
& ssSkP457("d0","d0")
& ssSkP419("d1","d1")
& ssSkP419("d1","d0")
& ssSkP419("d0","d1")
& ssSkP419("d0","d0")
& ssSkP418("d1","d1")
& ssSkP418("d1","d0")
& ssSkP418("d0","d1")
& ssSkP418("d0","d0")
& ssSkP387("d1","d1")
& ssSkP387("d1","d0")
& ssSkP387("d0","d1")
& ssSkP387("d0","d0")
& ssSkP386("d1","d1")
& ssSkP386("d1","d0")
& ssSkP386("d0","d1")
& ssSkP386("d0","d0")
& ssSkP366("d1","d1")
& ssSkP366("d1","d0")
& ssSkP366("d0","d1")
& ssSkP366("d0","d0")
& ssSkP365("d1","d1")
& ssSkP365("d1","d0")
& ssSkP365("d0","d1")
& ssSkP365("d0","d0")
& ssSkP326("d1","d1")
& ssSkP326("d1","d0")
& ssSkP326("d0","d1")
& ssSkP326("d0","d0")
& ssSkP325("d1","d1")
& ssSkP325("d1","d0")
& ssSkP325("d0","d1")
& ssSkP325("d0","d0")
& ssSkP288("d1","d1")
& ssSkP288("d1","d0")
& ssSkP288("d0","d1")
& ssSkP288("d0","d0")
& ssSkP287("d1","d1")
& ssSkP287("d1","d0")
& ssSkP287("d0","d1")
& ssSkP287("d0","d0")
& ssSkP265("d1","d1")
& ssSkP265("d1","d0")
& ssSkP265("d0","d1")
& ssSkP265("d0","d0")
& ssSkP264("d1","d1")
& ssSkP264("d1","d0")
& ssSkP264("d0","d1")
& ssSkP264("d0","d0")
& ssSkP230("d1","d1")
& ssSkP230("d1","d0")
& ssSkP230("d0","d1")
& ssSkP230("d0","d0")
& ssSkP229("d1","d1")
& ssSkP229("d1","d0")
& ssSkP229("d0","d1")
& ssSkP229("d0","d0")
& ssSkP21("d1","d1")
& ssSkP21("d1","d0")
& ssSkP21("d0","d1")
& ssSkP21("d0","d0")
& ssSkP20("d1","d1")
& ssSkP20("d1","d0")
& ssSkP20("d0","d1")
& ssSkP20("d0","d0")
& ssSkP190("d1","d1")
& ssSkP190("d1","d0")
& ssSkP190("d0","d1")
& ssSkP190("d0","d0")
& ssSkP189("d1","d1")
& ssSkP189("d1","d0")
& ssSkP189("d0","d1")
& ssSkP189("d0","d0")
& ssSkP157("d1","d1")
& ssSkP157("d1","d0")
& ssSkP157("d0","d1")
& ssSkP157("d0","d0")
& ssSkP156("d1","d1")
& ssSkP156("d1","d0")
& ssSkP156("d0","d1")
& ssSkP156("d0","d0")
& ssSkP1471("d1","d1")
& ssSkP1471("d1","d0")
& ssSkP1471("d0","d1")
& ssSkP1471("d0","d0")
& ssSkP1454("d1","d1")
& ssSkP1454("d1","d0")
& ssSkP1454("d0","d1")
& ssSkP1454("d0","d0")
& ssSkP1420("d1","d1")
& ssSkP1420("d1","d0")
& ssSkP1420("d0","d1")
& ssSkP1420("d0","d0")
& ssSkP1419("d1","d1")
& ssSkP1419("d1","d0")
& ssSkP1419("d0","d1")
& ssSkP1419("d0","d0")
& ssSkP1381("d1","d1")
& ssSkP1381("d1","d0")
& ssSkP1381("d0","d1")
& ssSkP1381("d0","d0")
& ssSkP1380("d1","d1")
& ssSkP1380("d1","d0")
& ssSkP1380("d0","d1")
& ssSkP1380("d0","d0")
& ssSkP1337("d1","d1")
& ssSkP1337("d1","d0")
& ssSkP1337("d0","d1")
& ssSkP1337("d0","d0")
& ssSkP1336("d1","d1")
& ssSkP1336("d1","d0")
& ssSkP1336("d0","d1")
& ssSkP1336("d0","d0")
& ssSkP1299("d1","d1")
& ssSkP1299("d1","d0")
& ssSkP1299("d0","d1")
& ssSkP1299("d0","d0")
& ssSkP1298("d1","d1")
& ssSkP1298("d1","d0")
& ssSkP1298("d0","d1")
& ssSkP1298("d0","d0")
& ssSkP1265("d1","d1")
& ssSkP1265("d1","d0")
& ssSkP1265("d0","d1")
& ssSkP1265("d0","d0")
& ssSkP1264("d1","d1")
& ssSkP1264("d1","d0")
& ssSkP1264("d0","d1")
& ssSkP1264("d0","d0")
& ssSkP1233("d1","d1")
& ssSkP1233("d1","d0")
& ssSkP1233("d0","d1")
& ssSkP1233("d0","d0")
& ssSkP1232("d1","d1")
& ssSkP1232("d1","d0")
& ssSkP1232("d0","d1")
& ssSkP1232("d0","d0")
& ssSkP123("d1","d1")
& ssSkP123("d1","d0")
& ssSkP123("d0","d1")
& ssSkP123("d0","d0")
& ssSkP122("d1","d1")
& ssSkP122("d1","d0")
& ssSkP122("d0","d1")
& ssSkP122("d0","d0")
& ssSkP1189("d1","d1")
& ssSkP1189("d1","d0")
& ssSkP1189("d0","d1")
& ssSkP1189("d0","d0")
& ssSkP1188("d1","d1")
& ssSkP1188("d1","d0")
& ssSkP1188("d0","d1")
& ssSkP1188("d0","d0")
& ssSkP1146("d1","d1")
& ssSkP1146("d1","d0")
& ssSkP1146("d0","d1")
& ssSkP1146("d0","d0")
& ssSkP1145("d1","d1")
& ssSkP1145("d1","d0")
& ssSkP1145("d0","d1")
& ssSkP1145("d0","d0")
& ssSkP1102("d1","d1")
& ssSkP1102("d1","d0")
& ssSkP1102("d0","d1")
& ssSkP1102("d0","d0")
& ssSkP1101("d1","d1")
& ssSkP1101("d1","d0")
& ssSkP1101("d0","d1")
& ssSkP1101("d0","d0")
& ssSkP1059("d1","d1")
& ssSkP1059("d1","d0")
& ssSkP1059("d0","d1")
& ssSkP1059("d0","d0")
& ssSkP1058("d1","d1")
& ssSkP1058("d1","d0")
& ssSkP1058("d0","d1")
& ssSkP1058("d0","d0")
& ssSkP1017("d1","d1")
& ssSkP1017("d1","d0")
& ssSkP1017("d0","d1")
& ssSkP1017("d0","d0")
& ssSkP1016("d1","d1")
& ssSkP1016("d1","d0")
& ssSkP1016("d0","d1")
& ssSkP1016("d0","d0")
& ssSkP1("d1","d1")
& ssSkP1("d1","d0")
& ssSkP1("d0","d1")
& ssSkP1("d0","d0")
& ssSkP0("d1","d1")
& ssSkP0("d1","d0")
& ssSkP0("d0","d1")
& ssSkP0("d0","d0")
& ssRr("d1","d1")
& ssRr("d1","d0")
& ssRr("d0","d1")
& ssRr("d0","d0")
& ~ ssSkP999("d1")
& ssSkP999("d0")
& ssSkP998("d1")
& ssSkP998("d0")
& ssSkP997("d1")
& ssSkP997("d0")
& ssSkP996("d1")
& ssSkP996("d0")
& ssSkP995("d1")
& ssSkP995("d0")
& ssSkP994("d1")
& ssSkP994("d0")
& ~ ssSkP993("d1")
& ~ ssSkP993("d0")
& ~ ssSkP992("d1")
& ~ ssSkP992("d0")
& ~ ssSkP991("d1")
& ~ ssSkP991("d0")
& ~ ssSkP990("d1")
& ~ ssSkP990("d0")
& ~ ssSkP99("d1")
& ~ ssSkP99("d0")
& ~ ssSkP989("d1")
& ~ ssSkP989("d0")
& ~ ssSkP986("d1")
& ssSkP986("d0")
& ssSkP985("d1")
& ssSkP985("d0")
& ssSkP984("d1")
& ssSkP984("d0")
& ssSkP983("d1")
& ssSkP983("d0")
& ssSkP982("d1")
& ssSkP982("d0")
& ssSkP981("d1")
& ssSkP981("d0")
& ssSkP980("d1")
& ssSkP980("d0")
& ~ ssSkP98("d1")
& ~ ssSkP98("d0")
& ssSkP979("d1")
& ssSkP979("d0")
& ssSkP978("d1")
& ssSkP978("d0")
& ssSkP977("d1")
& ssSkP977("d0")
& ssSkP976("d1")
& ssSkP976("d0")
& ssSkP975("d1")
& ssSkP975("d0")
& ~ ssSkP974("d1")
& ssSkP974("d0")
& ssSkP973("d1")
& ssSkP973("d0")
& ssSkP972("d1")
& ssSkP972("d0")
& ssSkP971("d1")
& ssSkP971("d0")
& ssSkP970("d1")
& ssSkP970("d0")
& ~ ssSkP97("d1")
& ~ ssSkP97("d0")
& ssSkP969("d1")
& ssSkP969("d0")
& ssSkP968("d1")
& ssSkP968("d0")
& ssSkP967("d1")
& ssSkP967("d0")
& ~ ssSkP966("d1")
& ~ ssSkP966("d0")
& ~ ssSkP965("d1")
& ~ ssSkP965("d0")
& ~ ssSkP964("d1")
& ~ ssSkP964("d0")
& ~ ssSkP963("d1")
& ~ ssSkP963("d0")
& ~ ssSkP962("d1")
& ~ ssSkP962("d0")
& ~ ssSkP961("d1")
& ~ ssSkP961("d0")
& ~ ssSkP960("d1")
& ~ ssSkP960("d0")
& ~ ssSkP96("d1")
& ~ ssSkP96("d0")
& ~ ssSkP959("d1")
& ~ ssSkP959("d0")
& ~ ssSkP958("d1")
& ~ ssSkP958("d0")
& ~ ssSkP957("d1")
& ~ ssSkP957("d0")
& ~ ssSkP954("d1")
& ssSkP954("d0")
& ssSkP953("d1")
& ssSkP953("d0")
& ssSkP952("d1")
& ssSkP952("d0")
& ssSkP951("d1")
& ssSkP951("d0")
& ssSkP950("d1")
& ssSkP950("d0")
& ~ ssSkP95("d1")
& ~ ssSkP95("d0")
& ssSkP949("d1")
& ssSkP949("d0")
& ssSkP948("d1")
& ssSkP948("d0")
& ssSkP947("d1")
& ssSkP947("d0")
& ssSkP946("d1")
& ssSkP946("d0")
& ssSkP945("d1")
& ssSkP945("d0")
& ssSkP944("d1")
& ssSkP944("d0")
& ssSkP943("d1")
& ssSkP943("d0")
& ~ ssSkP942("d1")
& ssSkP942("d0")
& ssSkP941("d1")
& ssSkP941("d0")
& ssSkP940("d1")
& ssSkP940("d0")
& ~ ssSkP94("d1")
& ~ ssSkP94("d0")
& ssSkP939("d1")
& ssSkP939("d0")
& ssSkP938("d1")
& ssSkP938("d0")
& ssSkP937("d1")
& ssSkP937("d0")
& ssSkP936("d1")
& ssSkP936("d0")
& ~ ssSkP935("d1")
& ~ ssSkP935("d0")
& ~ ssSkP934("d1")
& ~ ssSkP934("d0")
& ~ ssSkP933("d1")
& ~ ssSkP933("d0")
& ~ ssSkP932("d1")
& ~ ssSkP932("d0")
& ~ ssSkP931("d1")
& ~ ssSkP931("d0")
& ~ ssSkP930("d1")
& ~ ssSkP930("d0")
& ~ ssSkP93("d1")
& ~ ssSkP93("d0")
& ~ ssSkP929("d1")
& ~ ssSkP929("d0")
& ~ ssSkP928("d1")
& ~ ssSkP928("d0")
& ~ ssSkP927("d1")
& ~ ssSkP927("d0")
& ~ ssSkP926("d1")
& ~ ssSkP926("d0")
& ~ ssSkP925("d1")
& ~ ssSkP925("d0")
& ~ ssSkP924("d1")
& ~ ssSkP924("d0")
& ~ ssSkP923("d1")
& ~ ssSkP923("d0")
& ~ ssSkP922("d1")
& ~ ssSkP922("d0")
& ~ ssSkP921("d1")
& ~ ssSkP921("d0")
& ~ ssSkP920("d1")
& ~ ssSkP920("d0")
& ~ ssSkP92("d1")
& ~ ssSkP92("d0")
& ~ ssSkP919("d1")
& ~ ssSkP919("d0")
& ~ ssSkP918("d1")
& ~ ssSkP918("d0")
& ~ ssSkP917("d1")
& ~ ssSkP917("d0")
& ~ ssSkP916("d1")
& ~ ssSkP916("d0")
& ~ ssSkP913("d1")
& ssSkP913("d0")
& ssSkP912("d1")
& ssSkP912("d0")
& ssSkP911("d1")
& ssSkP911("d0")
& ssSkP910("d1")
& ssSkP910("d0")
& ~ ssSkP91("d1")
& ~ ssSkP91("d0")
& ssSkP909("d1")
& ssSkP909("d0")
& ssSkP908("d1")
& ssSkP908("d0")
& ssSkP907("d1")
& ssSkP907("d0")
& ssSkP906("d1")
& ssSkP906("d0")
& ssSkP905("d1")
& ssSkP905("d0")
& ssSkP904("d1")
& ssSkP904("d0")
& ssSkP903("d1")
& ssSkP903("d0")
& ssSkP902("d1")
& ssSkP902("d0")
& ssSkP901("d1")
& ~ ssSkP901("d0")
& ssSkP900("d1")
& ssSkP900("d0")
& ~ ssSkP90("d1")
& ~ ssSkP90("d0")
& ~ ssSkP9("d1")
& ~ ssSkP9("d0")
& ssSkP899("d1")
& ssSkP899("d0")
& ssSkP898("d1")
& ssSkP898("d0")
& ssSkP897("d1")
& ssSkP897("d0")
& ssSkP896("d1")
& ssSkP896("d0")
& ssSkP895("d1")
& ssSkP895("d0")
& ssSkP894("d1")
& ssSkP894("d0")
& ssSkP893("d1")
& ssSkP893("d0")
& ssSkP892("d1")
& ssSkP892("d0")
& ssSkP891("d1")
& ssSkP891("d0")
& ssSkP890("d1")
& ssSkP890("d0")
& ~ ssSkP89("d1")
& ~ ssSkP89("d0")
& ssSkP889("d1")
& ssSkP889("d0")
& ssSkP888("d1")
& ssSkP888("d0")
& ~ ssSkP887("d1")
& ~ ssSkP887("d0")
& ~ ssSkP886("d1")
& ~ ssSkP886("d0")
& ~ ssSkP885("d1")
& ~ ssSkP885("d0")
& ~ ssSkP884("d1")
& ~ ssSkP884("d0")
& ~ ssSkP883("d1")
& ~ ssSkP883("d0")
& ~ ssSkP882("d1")
& ~ ssSkP882("d0")
& ~ ssSkP881("d1")
& ~ ssSkP881("d0")
& ~ ssSkP880("d1")
& ~ ssSkP880("d0")
& ~ ssSkP879("d1")
& ~ ssSkP879("d0")
& ~ ssSkP878("d1")
& ~ ssSkP878("d0")
& ~ ssSkP877("d1")
& ~ ssSkP877("d0")
& ~ ssSkP876("d1")
& ~ ssSkP876("d0")
& ~ ssSkP873("d1")
& ssSkP873("d0")
& ssSkP872("d1")
& ssSkP872("d0")
& ssSkP871("d1")
& ssSkP871("d0")
& ssSkP870("d1")
& ssSkP870("d0")
& ssSkP869("d1")
& ssSkP869("d0")
& ssSkP868("d1")
& ssSkP868("d0")
& ssSkP867("d1")
& ssSkP867("d0")
& ssSkP866("d1")
& ssSkP866("d0")
& ssSkP865("d1")
& ssSkP865("d0")
& ssSkP864("d1")
& ssSkP864("d0")
& ~ ssSkP863("d1")
& ssSkP863("d0")
& ssSkP862("d1")
& ssSkP862("d0")
& ssSkP861("d1")
& ssSkP861("d0")
& ssSkP860("d1")
& ssSkP860("d0")
& ~ ssSkP86("d1")
& ssSkP86("d0")
& ssSkP859("d1")
& ssSkP859("d0")
& ssSkP858("d1")
& ssSkP858("d0")
& ssSkP857("d1")
& ssSkP857("d0")
& ssSkP856("d1")
& ssSkP856("d0")
& ssSkP855("d1")
& ssSkP855("d0")
& ssSkP854("d1")
& ssSkP854("d0")
& ssSkP853("d1")
& ssSkP853("d0")
& ssSkP852("d1")
& ssSkP852("d0")
& ssSkP851("d1")
& ssSkP851("d0")
& ssSkP850("d1")
& ssSkP850("d0")
& ssSkP85("d1")
& ssSkP85("d0")
& ssSkP849("d1")
& ssSkP849("d0")
& ssSkP848("d1")
& ssSkP848("d0")
& ssSkP847("d1")
& ssSkP847("d0")
& ssSkP846("d1")
& ssSkP846("d0")
& ssSkP845("d1")
& ~ ssSkP845("d0")
& ssSkP844("d1")
& ssSkP844("d0")
& ssSkP843("d1")
& ssSkP843("d0")
& ssSkP842("d1")
& ssSkP842("d0")
& ssSkP841("d1")
& ssSkP841("d0")
& ssSkP840("d1")
& ssSkP840("d0")
& ~ ssSkP84("d1")
& ~ ssSkP84("d0")
& ssSkP839("d1")
& ssSkP839("d0")
& ssSkP838("d1")
& ssSkP838("d0")
& ssSkP837("d1")
& ssSkP837("d0")
& ssSkP836("d1")
& ssSkP836("d0")
& ssSkP835("d1")
& ssSkP835("d0")
& ~ ssSkP832("d1")
& ssSkP832("d0")
& ssSkP831("d1")
& ssSkP831("d0")
& ssSkP830("d1")
& ssSkP830("d0")
& ~ ssSkP83("d1")
& ~ ssSkP83("d0")
& ssSkP829("d1")
& ssSkP829("d0")
& ssSkP828("d1")
& ssSkP828("d0")
& ssSkP827("d1")
& ssSkP827("d0")
& ssSkP826("d1")
& ssSkP826("d0")
& ssSkP825("d1")
& ssSkP825("d0")
& ssSkP824("d1")
& ssSkP824("d0")
& ssSkP823("d1")
& ssSkP823("d0")
& ~ ssSkP822("d1")
& ssSkP822("d0")
& ssSkP821("d1")
& ssSkP821("d0")
& ~ ssSkP820("d1")
& ssSkP820("d0")
& ~ ssSkP82("d1")
& ~ ssSkP82("d0")
& ssSkP819("d1")
& ssSkP819("d0")
& ssSkP818("d1")
& ssSkP818("d0")
& ssSkP817("d1")
& ssSkP817("d0")
& ssSkP816("d1")
& ssSkP816("d0")
& ssSkP815("d1")
& ssSkP815("d0")
& ssSkP814("d1")
& ssSkP814("d0")
& ssSkP813("d1")
& ssSkP813("d0")
& ssSkP812("d1")
& ssSkP812("d0")
& ssSkP811("d1")
& ssSkP811("d0")
& ssSkP810("d1")
& ssSkP810("d0")
& ~ ssSkP81("d1")
& ~ ssSkP81("d0")
& ssSkP809("d1")
& ssSkP809("d0")
& ssSkP808("d1")
& ssSkP808("d0")
& ssSkP807("d1")
& ssSkP807("d0")
& ssSkP806("d1")
& ssSkP806("d0")
& ssSkP805("d1")
& ssSkP805("d0")
& ssSkP804("d1")
& ssSkP804("d0")
& ssSkP803("d1")
& ssSkP803("d0")
& ssSkP802("d1")
& ssSkP802("d0")
& ssSkP801("d1")
& ssSkP801("d0")
& ssSkP800("d1")
& ssSkP800("d0")
& ~ ssSkP80("d1")
& ~ ssSkP80("d0")
& ~ ssSkP8("d1")
& ~ ssSkP8("d0")
& ssSkP799("d1")
& ssSkP799("d0")
& ssSkP798("d1")
& ssSkP798("d0")
& ssSkP797("d1")
& ssSkP797("d0")
& ssSkP796("d1")
& ssSkP796("d0")
& ~ ssSkP795("d1")
& ~ ssSkP795("d0")
& ~ ssSkP794("d1")
& ~ ssSkP794("d0")
& ~ ssSkP791("d1")
& ssSkP791("d0")
& ssSkP790("d1")
& ssSkP790("d0")
& ~ ssSkP79("d1")
& ~ ssSkP79("d0")
& ssSkP789("d1")
& ssSkP789("d0")
& ssSkP788("d1")
& ssSkP788("d0")
& ssSkP787("d1")
& ssSkP787("d0")
& ssSkP786("d1")
& ssSkP786("d0")
& ssSkP785("d1")
& ssSkP785("d0")
& ssSkP784("d1")
& ssSkP784("d0")
& ssSkP783("d1")
& ssSkP783("d0")
& ssSkP782("d1")
& ssSkP782("d0")
& ssSkP781("d1")
& ~ ssSkP781("d0")
& ssSkP780("d1")
& ssSkP780("d0")
& ~ ssSkP78("d1")
& ~ ssSkP78("d0")
& ssSkP779("d1")
& ssSkP779("d0")
& ssSkP778("d1")
& ssSkP778("d0")
& ssSkP777("d1")
& ssSkP777("d0")
& ssSkP776("d1")
& ssSkP776("d0")
& ssSkP775("d1")
& ssSkP775("d0")
& ssSkP774("d1")
& ssSkP774("d0")
& ssSkP773("d1")
& ssSkP773("d0")
& ssSkP772("d1")
& ssSkP772("d0")
& ~ ssSkP771("d1")
& ~ ssSkP771("d0")
& ~ ssSkP770("d1")
& ~ ssSkP770("d0")
& ~ ssSkP77("d1")
& ~ ssSkP77("d0")
& ~ ssSkP769("d1")
& ~ ssSkP769("d0")
& ~ ssSkP768("d1")
& ~ ssSkP768("d0")
& ~ ssSkP767("d1")
& ~ ssSkP767("d0")
& ~ ssSkP766("d1")
& ~ ssSkP766("d0")
& ~ ssSkP765("d1")
& ~ ssSkP765("d0")
& ~ ssSkP764("d1")
& ~ ssSkP764("d0")
& ~ ssSkP763("d1")
& ~ ssSkP763("d0")
& ~ ssSkP762("d1")
& ~ ssSkP762("d0")
& ~ ssSkP761("d1")
& ~ ssSkP761("d0")
& ~ ssSkP760("d1")
& ~ ssSkP760("d0")
& ~ ssSkP76("d1")
& ~ ssSkP76("d0")
& ~ ssSkP759("d1")
& ~ ssSkP759("d0")
& ~ ssSkP758("d1")
& ~ ssSkP758("d0")
& ~ ssSkP757("d1")
& ~ ssSkP757("d0")
& ~ ssSkP756("d1")
& ~ ssSkP756("d0")
& ~ ssSkP755("d1")
& ~ ssSkP755("d0")
& ~ ssSkP754("d1")
& ~ ssSkP754("d0")
& ~ ssSkP753("d1")
& ~ ssSkP753("d0")
& ~ ssSkP752("d1")
& ~ ssSkP752("d0")
& ~ ssSkP751("d1")
& ~ ssSkP751("d0")
& ~ ssSkP750("d1")
& ~ ssSkP750("d0")
& ~ ssSkP75("d1")
& ~ ssSkP75("d0")
& ~ ssSkP747("d1")
& ssSkP747("d0")
& ssSkP746("d1")
& ssSkP746("d0")
& ssSkP745("d1")
& ssSkP745("d0")
& ssSkP744("d1")
& ssSkP744("d0")
& ssSkP743("d1")
& ssSkP743("d0")
& ssSkP742("d1")
& ssSkP742("d0")
& ssSkP741("d1")
& ssSkP741("d0")
& ssSkP740("d1")
& ssSkP740("d0")
& ~ ssSkP74("d1")
& ~ ssSkP74("d0")
& ssSkP739("d1")
& ssSkP739("d0")
& ssSkP738("d1")
& ssSkP738("d0")
& ssSkP737("d1")
& ssSkP737("d0")
& ssSkP736("d1")
& ssSkP736("d0")
& ssSkP735("d1")
& ~ ssSkP735("d0")
& ssSkP734("d1")
& ssSkP734("d0")
& ssSkP733("d1")
& ssSkP733("d0")
& ssSkP732("d1")
& ssSkP732("d0")
& ssSkP731("d1")
& ssSkP731("d0")
& ssSkP730("d1")
& ssSkP730("d0")
& ~ ssSkP73("d1")
& ~ ssSkP73("d0")
& ssSkP729("d1")
& ssSkP729("d0")
& ssSkP728("d1")
& ssSkP728("d0")
& ssSkP727("d1")
& ssSkP727("d0")
& ssSkP726("d1")
& ssSkP726("d0")
& ssSkP725("d1")
& ssSkP725("d0")
& ssSkP724("d1")
& ssSkP724("d0")
& ssSkP723("d1")
& ssSkP723("d0")
& ~ ssSkP722("d1")
& ~ ssSkP722("d0")
& ~ ssSkP721("d1")
& ~ ssSkP721("d0")
& ~ ssSkP720("d1")
& ~ ssSkP720("d0")
& ~ ssSkP72("d1")
& ~ ssSkP72("d0")
& ~ ssSkP719("d1")
& ~ ssSkP719("d0")
& ~ ssSkP718("d1")
& ~ ssSkP718("d0")
& ~ ssSkP717("d1")
& ~ ssSkP717("d0")
& ~ ssSkP716("d1")
& ~ ssSkP716("d0")
& ~ ssSkP715("d1")
& ~ ssSkP715("d0")
& ~ ssSkP714("d1")
& ~ ssSkP714("d0")
& ~ ssSkP713("d1")
& ~ ssSkP713("d0")
& ~ ssSkP710("d1")
& ssSkP710("d0")
& ~ ssSkP71("d1")
& ~ ssSkP71("d0")
& ssSkP709("d1")
& ssSkP709("d0")
& ssSkP708("d1")
& ssSkP708("d0")
& ssSkP707("d1")
& ssSkP707("d0")
& ssSkP706("d1")
& ssSkP706("d0")
& ssSkP705("d1")
& ssSkP705("d0")
& ssSkP704("d1")
& ssSkP704("d0")
& ssSkP703("d1")
& ssSkP703("d0")
& ssSkP702("d1")
& ssSkP702("d0")
& ~ ssSkP701("d1")
& ~ ssSkP701("d0")
& ~ ssSkP700("d1")
& ~ ssSkP700("d0")
& ~ ssSkP70("d1")
& ~ ssSkP70("d0")
& ~ ssSkP7("d1")
& ~ ssSkP7("d0")
& ~ ssSkP699("d1")
& ~ ssSkP699("d0")
& ~ ssSkP698("d1")
& ~ ssSkP698("d0")
& ~ ssSkP697("d1")
& ~ ssSkP697("d0")
& ~ ssSkP696("d1")
& ~ ssSkP696("d0")
& ~ ssSkP695("d1")
& ~ ssSkP695("d0")
& ~ ssSkP694("d1")
& ~ ssSkP694("d0")
& ~ ssSkP693("d1")
& ~ ssSkP693("d0")
& ~ ssSkP692("d1")
& ~ ssSkP692("d0")
& ~ ssSkP691("d1")
& ~ ssSkP691("d0")
& ~ ssSkP690("d1")
& ~ ssSkP690("d0")
& ~ ssSkP69("d1")
& ~ ssSkP69("d0")
& ~ ssSkP689("d1")
& ~ ssSkP689("d0")
& ~ ssSkP688("d1")
& ~ ssSkP688("d0")
& ~ ssSkP687("d1")
& ~ ssSkP687("d0")
& ~ ssSkP686("d1")
& ~ ssSkP686("d0")
& ~ ssSkP685("d1")
& ~ ssSkP685("d0")
& ~ ssSkP684("d1")
& ~ ssSkP684("d0")
& ~ ssSkP683("d1")
& ~ ssSkP683("d0")
& ~ ssSkP682("d1")
& ~ ssSkP682("d0")
& ~ ssSkP681("d1")
& ~ ssSkP681("d0")
& ~ ssSkP680("d1")
& ~ ssSkP680("d0")
& ~ ssSkP68("d1")
& ~ ssSkP68("d0")
& ~ ssSkP679("d1")
& ~ ssSkP679("d0")
& ~ ssSkP678("d1")
& ~ ssSkP678("d0")
& ~ ssSkP677("d1")
& ~ ssSkP677("d0")
& ~ ssSkP676("d1")
& ~ ssSkP676("d0")
& ~ ssSkP675("d1")
& ~ ssSkP675("d0")
& ~ ssSkP674("d1")
& ~ ssSkP674("d0")
& ~ ssSkP673("d1")
& ~ ssSkP673("d0")
& ~ ssSkP672("d1")
& ~ ssSkP672("d0")
& ~ ssSkP671("d1")
& ~ ssSkP671("d0")
& ~ ssSkP670("d1")
& ~ ssSkP670("d0")
& ~ ssSkP67("d1")
& ~ ssSkP67("d0")
& ~ ssSkP669("d1")
& ~ ssSkP669("d0")
& ~ ssSkP666("d1")
& ssSkP666("d0")
& ssSkP665("d1")
& ssSkP665("d0")
& ssSkP664("d1")
& ssSkP664("d0")
& ssSkP663("d1")
& ssSkP663("d0")
& ssSkP662("d1")
& ssSkP662("d0")
& ssSkP661("d1")
& ssSkP661("d0")
& ssSkP660("d1")
& ssSkP660("d0")
& ~ ssSkP66("d1")
& ~ ssSkP66("d0")
& ssSkP659("d1")
& ssSkP659("d0")
& ssSkP658("d1")
& ssSkP658("d0")
& ~ ssSkP657("d1")
& ~ ssSkP657("d0")
& ~ ssSkP656("d1")
& ~ ssSkP656("d0")
& ~ ssSkP655("d1")
& ~ ssSkP655("d0")
& ~ ssSkP654("d1")
& ~ ssSkP654("d0")
& ~ ssSkP653("d1")
& ~ ssSkP653("d0")
& ~ ssSkP652("d1")
& ~ ssSkP652("d0")
& ~ ssSkP651("d1")
& ~ ssSkP651("d0")
& ~ ssSkP650("d1")
& ~ ssSkP650("d0")
& ~ ssSkP65("d1")
& ~ ssSkP65("d0")
& ~ ssSkP649("d1")
& ~ ssSkP649("d0")
& ~ ssSkP648("d1")
& ~ ssSkP648("d0")
& ~ ssSkP647("d1")
& ~ ssSkP647("d0")
& ~ ssSkP644("d1")
& ssSkP644("d0")
& ssSkP643("d1")
& ssSkP643("d0")
& ssSkP642("d1")
& ssSkP642("d0")
& ssSkP641("d1")
& ssSkP641("d0")
& ssSkP640("d1")
& ssSkP640("d0")
& ~ ssSkP64("d1")
& ~ ssSkP64("d0")
& ssSkP639("d1")
& ssSkP639("d0")
& ssSkP638("d1")
& ssSkP638("d0")
& ssSkP637("d1")
& ssSkP637("d0")
& ~ ssSkP636("d1")
& ~ ssSkP636("d0")
& ~ ssSkP635("d1")
& ~ ssSkP635("d0")
& ~ ssSkP634("d1")
& ~ ssSkP634("d0")
& ~ ssSkP633("d1")
& ~ ssSkP633("d0")
& ~ ssSkP632("d1")
& ~ ssSkP632("d0")
& ~ ssSkP631("d1")
& ~ ssSkP631("d0")
& ~ ssSkP630("d1")
& ~ ssSkP630("d0")
& ~ ssSkP63("d1")
& ~ ssSkP63("d0")
& ~ ssSkP629("d1")
& ~ ssSkP629("d0")
& ~ ssSkP628("d1")
& ~ ssSkP628("d0")
& ~ ssSkP627("d1")
& ~ ssSkP627("d0")
& ~ ssSkP626("d1")
& ~ ssSkP626("d0")
& ~ ssSkP625("d1")
& ~ ssSkP625("d0")
& ~ ssSkP624("d1")
& ~ ssSkP624("d0")
& ~ ssSkP623("d1")
& ~ ssSkP623("d0")
& ~ ssSkP622("d1")
& ~ ssSkP622("d0")
& ~ ssSkP621("d1")
& ~ ssSkP621("d0")
& ~ ssSkP620("d1")
& ~ ssSkP620("d0")
& ~ ssSkP62("d1")
& ~ ssSkP62("d0")
& ~ ssSkP619("d1")
& ~ ssSkP619("d0")
& ~ ssSkP618("d1")
& ~ ssSkP618("d0")
& ~ ssSkP617("d1")
& ~ ssSkP617("d0")
& ~ ssSkP616("d1")
& ~ ssSkP616("d0")
& ~ ssSkP615("d1")
& ~ ssSkP615("d0")
& ~ ssSkP614("d1")
& ~ ssSkP614("d0")
& ~ ssSkP613("d1")
& ~ ssSkP613("d0")
& ~ ssSkP612("d1")
& ~ ssSkP612("d0")
& ~ ssSkP611("d1")
& ~ ssSkP611("d0")
& ~ ssSkP610("d1")
& ~ ssSkP610("d0")
& ~ ssSkP61("d1")
& ~ ssSkP61("d0")
& ~ ssSkP609("d1")
& ~ ssSkP609("d0")
& ~ ssSkP608("d1")
& ~ ssSkP608("d0")
& ~ ssSkP605("d1")
& ssSkP605("d0")
& ssSkP604("d1")
& ssSkP604("d0")
& ssSkP603("d1")
& ssSkP603("d0")
& ssSkP602("d1")
& ssSkP602("d0")
& ssSkP601("d1")
& ssSkP601("d0")
& ssSkP600("d1")
& ssSkP600("d0")
& ~ ssSkP60("d1")
& ~ ssSkP60("d0")
& ~ ssSkP6("d1")
& ~ ssSkP6("d0")
& ~ ssSkP599("d1")
& ~ ssSkP599("d0")
& ~ ssSkP598("d1")
& ~ ssSkP598("d0")
& ~ ssSkP597("d1")
& ~ ssSkP597("d0")
& ~ ssSkP596("d1")
& ~ ssSkP596("d0")
& ~ ssSkP595("d1")
& ~ ssSkP595("d0")
& ~ ssSkP594("d1")
& ~ ssSkP594("d0")
& ~ ssSkP593("d1")
& ~ ssSkP593("d0")
& ~ ssSkP592("d1")
& ~ ssSkP592("d0")
& ~ ssSkP591("d1")
& ~ ssSkP591("d0")
& ~ ssSkP590("d1")
& ~ ssSkP590("d0")
& ~ ssSkP59("d1")
& ~ ssSkP59("d0")
& ~ ssSkP589("d1")
& ~ ssSkP589("d0")
& ~ ssSkP588("d1")
& ~ ssSkP588("d0")
& ~ ssSkP587("d1")
& ~ ssSkP587("d0")
& ~ ssSkP586("d1")
& ~ ssSkP586("d0")
& ~ ssSkP585("d1")
& ~ ssSkP585("d0")
& ~ ssSkP584("d1")
& ~ ssSkP584("d0")
& ~ ssSkP583("d1")
& ~ ssSkP583("d0")
& ~ ssSkP582("d1")
& ~ ssSkP582("d0")
& ~ ssSkP581("d1")
& ~ ssSkP581("d0")
& ~ ssSkP580("d1")
& ~ ssSkP580("d0")
& ~ ssSkP58("d1")
& ~ ssSkP58("d0")
& ~ ssSkP579("d1")
& ~ ssSkP579("d0")
& ~ ssSkP578("d1")
& ~ ssSkP578("d0")
& ~ ssSkP577("d1")
& ~ ssSkP577("d0")
& ~ ssSkP576("d1")
& ~ ssSkP576("d0")
& ~ ssSkP575("d1")
& ~ ssSkP575("d0")
& ~ ssSkP574("d1")
& ~ ssSkP574("d0")
& ~ ssSkP571("d1")
& ssSkP571("d0")
& ssSkP570("d1")
& ssSkP570("d0")
& ssSkP569("d1")
& ssSkP569("d0")
& ssSkP568("d1")
& ssSkP568("d0")
& ssSkP567("d1")
& ssSkP567("d0")
& ssSkP566("d1")
& ssSkP566("d0")
& ~ ssSkP565("d1")
& ~ ssSkP565("d0")
& ~ ssSkP564("d1")
& ~ ssSkP564("d0")
& ~ ssSkP563("d1")
& ~ ssSkP563("d0")
& ~ ssSkP562("d1")
& ~ ssSkP562("d0")
& ~ ssSkP561("d1")
& ~ ssSkP561("d0")
& ~ ssSkP560("d1")
& ~ ssSkP560("d0")
& ~ ssSkP559("d1")
& ~ ssSkP559("d0")
& ~ ssSkP558("d1")
& ~ ssSkP558("d0")
& ~ ssSkP557("d1")
& ~ ssSkP557("d0")
& ~ ssSkP556("d1")
& ~ ssSkP556("d0")
& ~ ssSkP555("d1")
& ~ ssSkP555("d0")
& ~ ssSkP554("d1")
& ~ ssSkP554("d0")
& ~ ssSkP553("d1")
& ~ ssSkP553("d0")
& ~ ssSkP552("d1")
& ~ ssSkP552("d0")
& ~ ssSkP551("d1")
& ~ ssSkP551("d0")
& ~ ssSkP550("d1")
& ~ ssSkP550("d0")
& ~ ssSkP55("d1")
& ssSkP55("d0")
& ~ ssSkP549("d1")
& ~ ssSkP549("d0")
& ~ ssSkP548("d1")
& ~ ssSkP548("d0")
& ~ ssSkP547("d1")
& ~ ssSkP547("d0")
& ~ ssSkP546("d1")
& ~ ssSkP546("d0")
& ~ ssSkP545("d1")
& ~ ssSkP545("d0")
& ~ ssSkP544("d1")
& ~ ssSkP544("d0")
& ~ ssSkP543("d1")
& ~ ssSkP543("d0")
& ~ ssSkP542("d1")
& ~ ssSkP542("d0")
& ~ ssSkP541("d1")
& ~ ssSkP541("d0")
& ~ ssSkP540("d1")
& ~ ssSkP540("d0")
& ssSkP54("d1")
& ssSkP54("d0")
& ~ ssSkP539("d1")
& ~ ssSkP539("d0")
& ~ ssSkP538("d1")
& ~ ssSkP538("d0")
& ~ ssSkP537("d1")
& ~ ssSkP537("d0")
& ~ ssSkP536("d1")
& ~ ssSkP536("d0")
& ~ ssSkP535("d1")
& ~ ssSkP535("d0")
& ~ ssSkP534("d1")
& ~ ssSkP534("d0")
& ~ ssSkP533("d1")
& ~ ssSkP533("d0")
& ~ ssSkP532("d1")
& ~ ssSkP532("d0")
& ~ ssSkP53("d1")
& ~ ssSkP53("d0")
& ~ ssSkP529("d1")
& ssSkP529("d0")
& ssSkP528("d1")
& ssSkP528("d0")
& ssSkP527("d1")
& ssSkP527("d0")
& ssSkP526("d1")
& ssSkP526("d0")
& ssSkP525("d1")
& ssSkP525("d0")
& ssSkP524("d1")
& ssSkP524("d0")
& ~ ssSkP523("d1")
& ~ ssSkP523("d0")
& ~ ssSkP522("d1")
& ~ ssSkP522("d0")
& ~ ssSkP521("d1")
& ~ ssSkP521("d0")
& ~ ssSkP520("d1")
& ~ ssSkP520("d0")
& ~ ssSkP52("d1")
& ~ ssSkP52("d0")
& ~ ssSkP519("d1")
& ~ ssSkP519("d0")
& ~ ssSkP518("d1")
& ~ ssSkP518("d0")
& ~ ssSkP517("d1")
& ~ ssSkP517("d0")
& ~ ssSkP516("d1")
& ~ ssSkP516("d0")
& ~ ssSkP515("d1")
& ~ ssSkP515("d0")
& ~ ssSkP514("d1")
& ~ ssSkP514("d0")
& ~ ssSkP513("d1")
& ~ ssSkP513("d0")
& ~ ssSkP512("d1")
& ~ ssSkP512("d0")
& ~ ssSkP511("d1")
& ~ ssSkP511("d0")
& ~ ssSkP510("d1")
& ~ ssSkP510("d0")
& ~ ssSkP51("d1")
& ~ ssSkP51("d0")
& ~ ssSkP509("d1")
& ~ ssSkP509("d0")
& ~ ssSkP508("d1")
& ~ ssSkP508("d0")
& ~ ssSkP507("d1")
& ~ ssSkP507("d0")
& ~ ssSkP506("d1")
& ~ ssSkP506("d0")
& ~ ssSkP505("d1")
& ~ ssSkP505("d0")
& ~ ssSkP504("d1")
& ~ ssSkP504("d0")
& ~ ssSkP503("d1")
& ~ ssSkP503("d0")
& ~ ssSkP502("d1")
& ~ ssSkP502("d0")
& ~ ssSkP501("d1")
& ~ ssSkP501("d0")
& ~ ssSkP500("d1")
& ~ ssSkP500("d0")
& ~ ssSkP50("d1")
& ~ ssSkP50("d0")
& ~ ssSkP5("d1")
& ~ ssSkP5("d0")
& ~ ssSkP499("d1")
& ~ ssSkP499("d0")
& ~ ssSkP498("d1")
& ~ ssSkP498("d0")
& ~ ssSkP497("d1")
& ~ ssSkP497("d0")
& ~ ssSkP494("d1")
& ssSkP494("d0")
& ssSkP493("d1")
& ssSkP493("d0")
& ssSkP492("d1")
& ssSkP492("d0")
& ssSkP491("d1")
& ssSkP491("d0")
& ssSkP490("d1")
& ssSkP490("d0")
& ~ ssSkP49("d1")
& ~ ssSkP49("d0")
& ssSkP489("d1")
& ssSkP489("d0")
& ~ ssSkP488("d1")
& ~ ssSkP488("d0")
& ~ ssSkP487("d1")
& ~ ssSkP487("d0")
& ~ ssSkP486("d1")
& ~ ssSkP486("d0")
& ~ ssSkP485("d1")
& ~ ssSkP485("d0")
& ~ ssSkP484("d1")
& ~ ssSkP484("d0")
& ~ ssSkP483("d1")
& ~ ssSkP483("d0")
& ~ ssSkP482("d1")
& ~ ssSkP482("d0")
& ~ ssSkP481("d1")
& ~ ssSkP481("d0")
& ~ ssSkP480("d1")
& ~ ssSkP480("d0")
& ~ ssSkP48("d1")
& ~ ssSkP48("d0")
& ~ ssSkP479("d1")
& ~ ssSkP479("d0")
& ~ ssSkP478("d1")
& ~ ssSkP478("d0")
& ~ ssSkP477("d1")
& ~ ssSkP477("d0")
& ~ ssSkP476("d1")
& ~ ssSkP476("d0")
& ~ ssSkP475("d1")
& ~ ssSkP475("d0")
& ~ ssSkP474("d1")
& ~ ssSkP474("d0")
& ~ ssSkP473("d1")
& ~ ssSkP473("d0")
& ~ ssSkP472("d1")
& ~ ssSkP472("d0")
& ~ ssSkP471("d1")
& ~ ssSkP471("d0")
& ~ ssSkP470("d1")
& ~ ssSkP470("d0")
& ~ ssSkP47("d1")
& ~ ssSkP47("d0")
& ~ ssSkP469("d1")
& ~ ssSkP469("d0")
& ~ ssSkP468("d1")
& ~ ssSkP468("d0")
& ~ ssSkP467("d1")
& ~ ssSkP467("d0")
& ~ ssSkP466("d1")
& ~ ssSkP466("d0")
& ~ ssSkP465("d1")
& ~ ssSkP465("d0")
& ~ ssSkP464("d1")
& ~ ssSkP464("d0")
& ~ ssSkP463("d1")
& ~ ssSkP463("d0")
& ~ ssSkP462("d1")
& ~ ssSkP462("d0")
& ~ ssSkP461("d1")
& ~ ssSkP461("d0")
& ~ ssSkP460("d1")
& ~ ssSkP460("d0")
& ~ ssSkP46("d1")
& ~ ssSkP46("d0")
& ~ ssSkP459("d1")
& ~ ssSkP459("d0")
& ~ ssSkP456("d1")
& ssSkP456("d0")
& ssSkP455("d1")
& ssSkP455("d0")
& ssSkP454("d1")
& ssSkP454("d0")
& ssSkP453("d1")
& ssSkP453("d0")
& ssSkP452("d1")
& ssSkP452("d0")
& ~ ssSkP451("d1")
& ~ ssSkP451("d0")
& ~ ssSkP450("d1")
& ~ ssSkP450("d0")
& ~ ssSkP45("d1")
& ~ ssSkP45("d0")
& ~ ssSkP449("d1")
& ~ ssSkP449("d0")
& ~ ssSkP448("d1")
& ~ ssSkP448("d0")
& ~ ssSkP447("d1")
& ~ ssSkP447("d0")
& ~ ssSkP446("d1")
& ~ ssSkP446("d0")
& ~ ssSkP445("d1")
& ~ ssSkP445("d0")
& ~ ssSkP444("d1")
& ~ ssSkP444("d0")
& ~ ssSkP443("d1")
& ~ ssSkP443("d0")
& ~ ssSkP442("d1")
& ~ ssSkP442("d0")
& ~ ssSkP441("d1")
& ~ ssSkP441("d0")
& ~ ssSkP440("d1")
& ~ ssSkP440("d0")
& ~ ssSkP44("d1")
& ~ ssSkP44("d0")
& ~ ssSkP439("d1")
& ~ ssSkP439("d0")
& ~ ssSkP438("d1")
& ~ ssSkP438("d0")
& ~ ssSkP437("d1")
& ~ ssSkP437("d0")
& ~ ssSkP436("d1")
& ~ ssSkP436("d0")
& ~ ssSkP435("d1")
& ~ ssSkP435("d0")
& ~ ssSkP434("d1")
& ~ ssSkP434("d0")
& ~ ssSkP433("d1")
& ~ ssSkP433("d0")
& ~ ssSkP432("d1")
& ~ ssSkP432("d0")
& ~ ssSkP431("d1")
& ~ ssSkP431("d0")
& ~ ssSkP430("d1")
& ~ ssSkP430("d0")
& ~ ssSkP43("d1")
& ~ ssSkP43("d0")
& ~ ssSkP429("d1")
& ~ ssSkP429("d0")
& ~ ssSkP428("d1")
& ~ ssSkP428("d0")
& ~ ssSkP427("d1")
& ~ ssSkP427("d0")
& ~ ssSkP426("d1")
& ~ ssSkP426("d0")
& ~ ssSkP425("d1")
& ~ ssSkP425("d0")
& ~ ssSkP424("d1")
& ~ ssSkP424("d0")
& ~ ssSkP423("d1")
& ~ ssSkP423("d0")
& ~ ssSkP422("d1")
& ~ ssSkP422("d0")
& ~ ssSkP421("d1")
& ~ ssSkP421("d0")
& ~ ssSkP420("d1")
& ~ ssSkP420("d0")
& ~ ssSkP42("d1")
& ~ ssSkP42("d0")
& ~ ssSkP417("d1")
& ssSkP417("d0")
& ssSkP416("d1")
& ssSkP416("d0")
& ssSkP415("d1")
& ssSkP415("d0")
& ssSkP414("d1")
& ssSkP414("d0")
& ssSkP413("d1")
& ssSkP413("d0")
& ~ ssSkP412("d1")
& ~ ssSkP412("d0")
& ~ ssSkP411("d1")
& ~ ssSkP411("d0")
& ~ ssSkP410("d1")
& ~ ssSkP410("d0")
& ~ ssSkP41("d1")
& ~ ssSkP41("d0")
& ~ ssSkP409("d1")
& ~ ssSkP409("d0")
& ~ ssSkP408("d1")
& ~ ssSkP408("d0")
& ~ ssSkP407("d1")
& ~ ssSkP407("d0")
& ~ ssSkP406("d1")
& ~ ssSkP406("d0")
& ~ ssSkP405("d1")
& ~ ssSkP405("d0")
& ~ ssSkP404("d1")
& ~ ssSkP404("d0")
& ~ ssSkP403("d1")
& ~ ssSkP403("d0")
& ~ ssSkP402("d1")
& ~ ssSkP402("d0")
& ~ ssSkP401("d1")
& ~ ssSkP401("d0")
& ~ ssSkP400("d1")
& ~ ssSkP400("d0")
& ~ ssSkP40("d1")
& ~ ssSkP40("d0")
& ~ ssSkP4("d1")
& ~ ssSkP4("d0")
& ~ ssSkP399("d1")
& ~ ssSkP399("d0")
& ~ ssSkP398("d1")
& ~ ssSkP398("d0")
& ~ ssSkP397("d1")
& ~ ssSkP397("d0")
& ~ ssSkP396("d1")
& ~ ssSkP396("d0")
& ~ ssSkP395("d1")
& ~ ssSkP395("d0")
& ~ ssSkP394("d1")
& ~ ssSkP394("d0")
& ~ ssSkP393("d1")
& ~ ssSkP393("d0")
& ~ ssSkP392("d1")
& ~ ssSkP392("d0")
& ~ ssSkP391("d1")
& ~ ssSkP391("d0")
& ~ ssSkP390("d1")
& ~ ssSkP390("d0")
& ~ ssSkP39("d1")
& ~ ssSkP39("d0")
& ~ ssSkP389("d1")
& ~ ssSkP389("d0")
& ~ ssSkP388("d1")
& ~ ssSkP388("d0")
& ~ ssSkP385("d1")
& ssSkP385("d0")
& ssSkP384("d1")
& ssSkP384("d0")
& ssSkP383("d1")
& ssSkP383("d0")
& ssSkP382("d1")
& ssSkP382("d0")
& ssSkP381("d1")
& ssSkP381("d0")
& ~ ssSkP380("d1")
& ~ ssSkP380("d0")
& ~ ssSkP38("d1")
& ~ ssSkP38("d0")
& ~ ssSkP379("d1")
& ~ ssSkP379("d0")
& ~ ssSkP378("d1")
& ~ ssSkP378("d0")
& ~ ssSkP377("d1")
& ~ ssSkP377("d0")
& ~ ssSkP376("d1")
& ~ ssSkP376("d0")
& ~ ssSkP375("d1")
& ~ ssSkP375("d0")
& ~ ssSkP374("d1")
& ~ ssSkP374("d0")
& ~ ssSkP373("d1")
& ~ ssSkP373("d0")
& ~ ssSkP372("d1")
& ~ ssSkP372("d0")
& ~ ssSkP371("d1")
& ~ ssSkP371("d0")
& ~ ssSkP370("d1")
& ~ ssSkP370("d0")
& ~ ssSkP37("d1")
& ~ ssSkP37("d0")
& ~ ssSkP369("d1")
& ~ ssSkP369("d0")
& ~ ssSkP368("d1")
& ~ ssSkP368("d0")
& ~ ssSkP367("d1")
& ~ ssSkP367("d0")
& ~ ssSkP364("d1")
& ssSkP364("d0")
& ssSkP363("d1")
& ssSkP363("d0")
& ssSkP362("d1")
& ssSkP362("d0")
& ssSkP361("d1")
& ssSkP361("d0")
& ssSkP360("d1")
& ssSkP360("d0")
& ~ ssSkP36("d1")
& ~ ssSkP36("d0")
& ssSkP359("d1")
& ssSkP359("d0")
& ssSkP358("d1")
& ssSkP358("d0")
& ssSkP357("d1")
& ssSkP357("d0")
& ssSkP356("d1")
& ssSkP356("d0")
& ssSkP355("d1")
& ssSkP355("d0")
& ssSkP354("d1")
& ssSkP354("d0")
& ssSkP353("d1")
& ssSkP353("d0")
& ssSkP352("d1")
& ssSkP352("d0")
& ssSkP351("d1")
& ssSkP351("d0")
& ssSkP350("d1")
& ssSkP350("d0")
& ~ ssSkP35("d1")
& ~ ssSkP35("d0")
& ssSkP349("d1")
& ssSkP349("d0")
& ssSkP348("d1")
& ssSkP348("d0")
& ssSkP347("d1")
& ssSkP347("d0")
& ~ ssSkP346("d1")
& ssSkP346("d0")
& ssSkP345("d1")
& ssSkP345("d0")
& ssSkP344("d1")
& ssSkP344("d0")
& ssSkP343("d1")
& ssSkP343("d0")
& ssSkP342("d1")
& ssSkP342("d0")
& ssSkP341("d1")
& ssSkP341("d0")
& ssSkP340("d1")
& ssSkP340("d0")
& ~ ssSkP34("d1")
& ~ ssSkP34("d0")
& ssSkP339("d1")
& ssSkP339("d0")
& ssSkP338("d1")
& ssSkP338("d0")
& ssSkP337("d1")
& ssSkP337("d0")
& ssSkP336("d1")
& ssSkP336("d0")
& ssSkP335("d1")
& ssSkP335("d0")
& ssSkP334("d1")
& ~ ssSkP334("d0")
& ssSkP333("d1")
& ssSkP333("d0")
& ssSkP332("d1")
& ssSkP332("d0")
& ssSkP331("d1")
& ssSkP331("d0")
& ssSkP330("d1")
& ssSkP330("d0")
& ~ ssSkP33("d1")
& ~ ssSkP33("d0")
& ssSkP329("d1")
& ssSkP329("d0")
& ssSkP328("d1")
& ssSkP328("d0")
& ssSkP327("d1")
& ssSkP327("d0")
& ~ ssSkP324("d1")
& ssSkP324("d0")
& ssSkP323("d1")
& ssSkP323("d0")
& ssSkP322("d1")
& ssSkP322("d0")
& ssSkP321("d1")
& ssSkP321("d0")
& ssSkP320("d1")
& ssSkP320("d0")
& ~ ssSkP32("d1")
& ~ ssSkP32("d0")
& ssSkP319("d1")
& ssSkP319("d0")
& ssSkP318("d1")
& ssSkP318("d0")
& ssSkP317("d1")
& ssSkP317("d0")
& ssSkP316("d1")
& ssSkP316("d0")
& ssSkP315("d1")
& ssSkP315("d0")
& ssSkP314("d1")
& ssSkP314("d0")
& ~ ssSkP313("d1")
& ssSkP313("d0")
& ssSkP312("d1")
& ssSkP312("d0")
& ssSkP311("d1")
& ssSkP311("d0")
& ~ ssSkP310("d1")
& ssSkP310("d0")
& ~ ssSkP31("d1")
& ~ ssSkP31("d0")
& ssSkP309("d1")
& ssSkP309("d0")
& ssSkP308("d1")
& ssSkP308("d0")
& ssSkP307("d1")
& ssSkP307("d0")
& ssSkP306("d1")
& ssSkP306("d0")
& ssSkP305("d1")
& ssSkP305("d0")
& ssSkP304("d1")
& ssSkP304("d0")
& ssSkP303("d1")
& ssSkP303("d0")
& ssSkP302("d1")
& ssSkP302("d0")
& ssSkP301("d1")
& ssSkP301("d0")
& ssSkP300("d1")
& ssSkP300("d0")
& ~ ssSkP30("d1")
& ~ ssSkP30("d0")
& ~ ssSkP3("d1")
& ~ ssSkP3("d0")
& ssSkP299("d1")
& ssSkP299("d0")
& ssSkP298("d1")
& ssSkP298("d0")
& ssSkP297("d1")
& ssSkP297("d0")
& ssSkP296("d1")
& ssSkP296("d0")
& ssSkP295("d1")
& ssSkP295("d0")
& ssSkP294("d1")
& ssSkP294("d0")
& ssSkP293("d1")
& ssSkP293("d0")
& ssSkP292("d1")
& ssSkP292("d0")
& ssSkP291("d1")
& ssSkP291("d0")
& ssSkP290("d1")
& ssSkP290("d0")
& ~ ssSkP29("d1")
& ~ ssSkP29("d0")
& ssSkP289("d1")
& ssSkP289("d0")
& ~ ssSkP286("d1")
& ssSkP286("d0")
& ssSkP285("d1")
& ssSkP285("d0")
& ssSkP284("d1")
& ssSkP284("d0")
& ssSkP283("d1")
& ssSkP283("d0")
& ~ ssSkP282("d1")
& ~ ssSkP282("d0")
& ~ ssSkP281("d1")
& ~ ssSkP281("d0")
& ~ ssSkP280("d1")
& ~ ssSkP280("d0")
& ~ ssSkP28("d1")
& ~ ssSkP28("d0")
& ~ ssSkP279("d1")
& ~ ssSkP279("d0")
& ~ ssSkP278("d1")
& ~ ssSkP278("d0")
& ~ ssSkP277("d1")
& ~ ssSkP277("d0")
& ~ ssSkP276("d1")
& ~ ssSkP276("d0")
& ~ ssSkP275("d1")
& ~ ssSkP275("d0")
& ~ ssSkP274("d1")
& ~ ssSkP274("d0")
& ~ ssSkP273("d1")
& ~ ssSkP273("d0")
& ~ ssSkP272("d1")
& ~ ssSkP272("d0")
& ~ ssSkP271("d1")
& ~ ssSkP271("d0")
& ~ ssSkP270("d1")
& ~ ssSkP270("d0")
& ~ ssSkP27("d1")
& ~ ssSkP27("d0")
& ~ ssSkP269("d1")
& ~ ssSkP269("d0")
& ~ ssSkP268("d1")
& ~ ssSkP268("d0")
& ~ ssSkP267("d1")
& ~ ssSkP267("d0")
& ~ ssSkP266("d1")
& ~ ssSkP266("d0")
& ~ ssSkP263("d1")
& ssSkP263("d0")
& ssSkP262("d1")
& ssSkP262("d0")
& ssSkP261("d1")
& ssSkP261("d0")
& ssSkP260("d1")
& ssSkP260("d0")
& ~ ssSkP26("d1")
& ~ ssSkP26("d0")
& ~ ssSkP259("d1")
& ~ ssSkP259("d0")
& ~ ssSkP258("d1")
& ~ ssSkP258("d0")
& ~ ssSkP257("d1")
& ~ ssSkP257("d0")
& ~ ssSkP256("d1")
& ~ ssSkP256("d0")
& ~ ssSkP255("d1")
& ~ ssSkP255("d0")
& ~ ssSkP254("d1")
& ~ ssSkP254("d0")
& ~ ssSkP253("d1")
& ~ ssSkP253("d0")
& ~ ssSkP252("d1")
& ~ ssSkP252("d0")
& ~ ssSkP251("d1")
& ~ ssSkP251("d0")
& ~ ssSkP250("d1")
& ~ ssSkP250("d0")
& ~ ssSkP25("d1")
& ~ ssSkP25("d0")
& ~ ssSkP249("d1")
& ~ ssSkP249("d0")
& ~ ssSkP248("d1")
& ~ ssSkP248("d0")
& ~ ssSkP247("d1")
& ~ ssSkP247("d0")
& ~ ssSkP246("d1")
& ~ ssSkP246("d0")
& ~ ssSkP245("d1")
& ~ ssSkP245("d0")
& ~ ssSkP244("d1")
& ~ ssSkP244("d0")
& ~ ssSkP243("d1")
& ~ ssSkP243("d0")
& ~ ssSkP242("d1")
& ~ ssSkP242("d0")
& ~ ssSkP241("d1")
& ~ ssSkP241("d0")
& ~ ssSkP240("d1")
& ~ ssSkP240("d0")
& ~ ssSkP24("d1")
& ~ ssSkP24("d0")
& ~ ssSkP239("d1")
& ~ ssSkP239("d0")
& ~ ssSkP238("d1")
& ~ ssSkP238("d0")
& ~ ssSkP237("d1")
& ~ ssSkP237("d0")
& ~ ssSkP236("d1")
& ~ ssSkP236("d0")
& ~ ssSkP235("d1")
& ~ ssSkP235("d0")
& ~ ssSkP234("d1")
& ~ ssSkP234("d0")
& ~ ssSkP233("d1")
& ~ ssSkP233("d0")
& ~ ssSkP232("d1")
& ~ ssSkP232("d0")
& ~ ssSkP231("d1")
& ~ ssSkP231("d0")
& ~ ssSkP23("d1")
& ~ ssSkP23("d0")
& ~ ssSkP228("d1")
& ssSkP228("d0")
& ssSkP227("d1")
& ssSkP227("d0")
& ssSkP226("d1")
& ssSkP226("d0")
& ssSkP225("d1")
& ssSkP225("d0")
& ssSkP224("d1")
& ssSkP224("d0")
& ssSkP223("d1")
& ssSkP223("d0")
& ssSkP222("d1")
& ssSkP222("d0")
& ssSkP221("d1")
& ssSkP221("d0")
& ssSkP220("d1")
& ssSkP220("d0")
& ~ ssSkP22("d1")
& ~ ssSkP22("d0")
& ssSkP219("d1")
& ssSkP219("d0")
& ssSkP218("d1")
& ssSkP218("d0")
& ssSkP217("d1")
& ssSkP217("d0")
& ssSkP216("d1")
& ssSkP216("d0")
& ssSkP215("d1")
& ssSkP215("d0")
& ssSkP214("d1")
& ssSkP214("d0")
& ssSkP213("d1")
& ssSkP213("d0")
& ssSkP212("d1")
& ssSkP212("d0")
& ssSkP211("d1")
& ~ ssSkP211("d0")
& ssSkP210("d1")
& ssSkP210("d0")
& ssSkP209("d1")
& ssSkP209("d0")
& ssSkP208("d1")
& ssSkP208("d0")
& ssSkP207("d1")
& ssSkP207("d0")
& ssSkP206("d1")
& ssSkP206("d0")
& ssSkP205("d1")
& ssSkP205("d0")
& ssSkP204("d1")
& ssSkP204("d0")
& ssSkP203("d1")
& ssSkP203("d0")
& ssSkP202("d1")
& ssSkP202("d0")
& ssSkP201("d1")
& ssSkP201("d0")
& ssSkP200("d1")
& ssSkP200("d0")
& ~ ssSkP2("d1")
& ~ ssSkP2("d0")
& ssSkP199("d1")
& ssSkP199("d0")
& ssSkP198("d1")
& ssSkP198("d0")
& ~ ssSkP197("d1")
& ssSkP197("d0")
& ssSkP196("d1")
& ssSkP196("d0")
& ssSkP195("d1")
& ssSkP195("d0")
& ssSkP194("d1")
& ssSkP194("d0")
& ssSkP193("d1")
& ssSkP193("d0")
& ssSkP192("d1")
& ssSkP192("d0")
& ssSkP191("d1")
& ssSkP191("d0")
& ~ ssSkP19("d1")
& ssSkP19("d0")
& ~ ssSkP188("d1")
& ssSkP188("d0")
& ssSkP187("d1")
& ssSkP187("d0")
& ssSkP186("d1")
& ssSkP186("d0")
& ~ ssSkP185("d1")
& ~ ssSkP185("d0")
& ~ ssSkP184("d1")
& ~ ssSkP184("d0")
& ~ ssSkP183("d1")
& ~ ssSkP183("d0")
& ~ ssSkP182("d1")
& ~ ssSkP182("d0")
& ~ ssSkP181("d1")
& ~ ssSkP181("d0")
& ~ ssSkP180("d1")
& ~ ssSkP180("d0")
& ssSkP18("d1")
& ssSkP18("d0")
& ~ ssSkP179("d1")
& ~ ssSkP179("d0")
& ~ ssSkP178("d1")
& ~ ssSkP178("d0")
& ~ ssSkP177("d1")
& ~ ssSkP177("d0")
& ~ ssSkP176("d1")
& ~ ssSkP176("d0")
& ~ ssSkP175("d1")
& ~ ssSkP175("d0")
& ~ ssSkP174("d1")
& ~ ssSkP174("d0")
& ~ ssSkP173("d1")
& ~ ssSkP173("d0")
& ~ ssSkP172("d1")
& ~ ssSkP172("d0")
& ~ ssSkP171("d1")
& ~ ssSkP171("d0")
& ~ ssSkP170("d1")
& ~ ssSkP170("d0")
& ssSkP17("d1")
& ssSkP17("d0")
& ~ ssSkP169("d1")
& ~ ssSkP169("d0")
& ~ ssSkP168("d1")
& ~ ssSkP168("d0")
& ~ ssSkP167("d1")
& ~ ssSkP167("d0")
& ~ ssSkP166("d1")
& ~ ssSkP166("d0")
& ~ ssSkP165("d1")
& ~ ssSkP165("d0")
& ~ ssSkP164("d1")
& ~ ssSkP164("d0")
& ~ ssSkP163("d1")
& ~ ssSkP163("d0")
& ~ ssSkP162("d1")
& ~ ssSkP162("d0")
& ~ ssSkP161("d1")
& ~ ssSkP161("d0")
& ~ ssSkP160("d1")
& ~ ssSkP160("d0")
& ssSkP16("d1")
& ssSkP16("d0")
& ~ ssSkP1595("d1")
& ssSkP1595("d0")
& ~ ssSkP1594("d1")
& ssSkP1594("d0")
& ssSkP1593("d1")
& ssSkP1593("d0")
& ssSkP1592("d1")
& ssSkP1592("d0")
& ssSkP1591("d1")
& ssSkP1591("d0")
& ssSkP1590("d1")
& ssSkP1590("d0")
& ~ ssSkP159("d1")
& ~ ssSkP159("d0")
& ssSkP1589("d1")
& ssSkP1589("d0")
& ssSkP1588("d1")
& ssSkP1588("d0")
& ssSkP1587("d1")
& ssSkP1587("d0")
& ssSkP1586("d1")
& ssSkP1586("d0")
& ssSkP1585("d1")
& ssSkP1585("d0")
& ssSkP1584("d1")
& ssSkP1584("d0")
& ssSkP1583("d1")
& ssSkP1583("d0")
& ssSkP1582("d1")
& ssSkP1582("d0")
& ssSkP1581("d1")
& ssSkP1581("d0")
& ssSkP1580("d1")
& ssSkP1580("d0")
& ~ ssSkP158("d1")
& ~ ssSkP158("d0")
& ssSkP1579("d1")
& ssSkP1579("d0")
& ssSkP1578("d1")
& ssSkP1578("d0")
& ssSkP1577("d1")
& ssSkP1577("d0")
& ssSkP1576("d1")
& ssSkP1576("d0")
& ssSkP1575("d1")
& ssSkP1575("d0")
& ssSkP1574("d1")
& ssSkP1574("d0")
& ssSkP1573("d1")
& ssSkP1573("d0")
& ssSkP1572("d1")
& ssSkP1572("d0")
& ssSkP1571("d1")
& ssSkP1571("d0")
& ssSkP1570("d1")
& ssSkP1570("d0")
& ssSkP1569("d1")
& ssSkP1569("d0")
& ssSkP1568("d1")
& ssSkP1568("d0")
& ssSkP1567("d1")
& ssSkP1567("d0")
& ssSkP1566("d1")
& ssSkP1566("d0")
& ssSkP1565("d1")
& ssSkP1565("d0")
& ssSkP1564("d1")
& ssSkP1564("d0")
& ssSkP1563("d1")
& ssSkP1563("d0")
& ssSkP1562("d1")
& ssSkP1562("d0")
& ssSkP1561("d1")
& ssSkP1561("d0")
& ssSkP1560("d1")
& ssSkP1560("d0")
& ssSkP1559("d1")
& ssSkP1559("d0")
& ssSkP1558("d1")
& ssSkP1558("d0")
& ssSkP1557("d1")
& ssSkP1557("d0")
& ssSkP1556("d1")
& ssSkP1556("d0")
& ssSkP1555("d1")
& ssSkP1555("d0")
& ssSkP1554("d1")
& ssSkP1554("d0")
& ssSkP1553("d1")
& ssSkP1553("d0")
& ssSkP1552("d1")
& ssSkP1552("d0")
& ssSkP1551("d1")
& ssSkP1551("d0")
& ssSkP1550("d1")
& ssSkP1550("d0")
& ~ ssSkP155("d1")
& ssSkP155("d0")
& ssSkP1549("d1")
& ssSkP1549("d0")
& ssSkP1548("d1")
& ssSkP1548("d0")
& ssSkP1547("d1")
& ssSkP1547("d0")
& ssSkP1546("d1")
& ssSkP1546("d0")
& ssSkP1545("d1")
& ssSkP1545("d0")
& ssSkP1544("d1")
& ssSkP1544("d0")
& ssSkP1543("d1")
& ssSkP1543("d0")
& ssSkP1542("d1")
& ssSkP1542("d0")
& ssSkP1541("d1")
& ssSkP1541("d0")
& ssSkP1540("d1")
& ssSkP1540("d0")
& ssSkP154("d1")
& ssSkP154("d0")
& ssSkP1539("d1")
& ssSkP1539("d0")
& ssSkP1538("d1")
& ssSkP1538("d0")
& ssSkP1537("d1")
& ssSkP1537("d0")
& ssSkP1536("d1")
& ssSkP1536("d0")
& ssSkP1535("d1")
& ssSkP1535("d0")
& ssSkP1534("d1")
& ssSkP1534("d0")
& ssSkP1533("d1")
& ssSkP1533("d0")
& ssSkP1532("d1")
& ssSkP1532("d0")
& ssSkP1531("d1")
& ssSkP1531("d0")
& ssSkP1530("d1")
& ssSkP1530("d0")
& ~ ssSkP153("d1")
& ~ ssSkP153("d0")
& ssSkP1529("d1")
& ssSkP1529("d0")
& ssSkP1528("d1")
& ssSkP1528("d0")
& ssSkP1527("d1")
& ssSkP1527("d0")
& ssSkP1526("d1")
& ssSkP1526("d0")
& ssSkP1525("d1")
& ssSkP1525("d0")
& ssSkP1524("d1")
& ssSkP1524("d0")
& ssSkP1523("d1")
& ssSkP1523("d0")
& ssSkP1522("d1")
& ssSkP1522("d0")
& ssSkP1521("d1")
& ssSkP1521("d0")
& ssSkP1520("d1")
& ssSkP1520("d0")
& ~ ssSkP152("d1")
& ~ ssSkP152("d0")
& ssSkP1519("d1")
& ssSkP1519("d0")
& ssSkP1518("d1")
& ssSkP1518("d0")
& ssSkP1517("d1")
& ssSkP1517("d0")
& ssSkP1516("d1")
& ssSkP1516("d0")
& ssSkP1515("d1")
& ssSkP1515("d0")
& ssSkP1514("d1")
& ssSkP1514("d0")
& ssSkP1513("d1")
& ssSkP1513("d0")
& ssSkP1512("d1")
& ssSkP1512("d0")
& ssSkP1511("d1")
& ssSkP1511("d0")
& ssSkP1510("d1")
& ssSkP1510("d0")
& ~ ssSkP151("d1")
& ~ ssSkP151("d0")
& ssSkP1509("d1")
& ssSkP1509("d0")
& ssSkP1508("d1")
& ssSkP1508("d0")
& ssSkP1507("d1")
& ssSkP1507("d0")
& ssSkP1506("d1")
& ssSkP1506("d0")
& ssSkP1505("d1")
& ssSkP1505("d0")
& ~ ssSkP1504("d1")
& ssSkP1504("d0")
& ~ ssSkP1503("d1")
& ssSkP1503("d0")
& ~ ssSkP1502("d1")
& ssSkP1502("d0")
& ~ ssSkP1501("d1")
& ssSkP1501("d0")
& ~ ssSkP1500("d1")
& ssSkP1500("d0")
& ~ ssSkP150("d1")
& ~ ssSkP150("d0")
& ~ ssSkP15("d1")
& ~ ssSkP15("d0")
& ~ ssSkP1499("d1")
& ssSkP1499("d0")
& ~ ssSkP1498("d1")
& ssSkP1498("d0")
& ~ ssSkP1497("d1")
& ssSkP1497("d0")
& ~ ssSkP1496("d1")
& ssSkP1496("d0")
& ~ ssSkP1495("d1")
& ssSkP1495("d0")
& ~ ssSkP1494("d1")
& ssSkP1494("d0")
& ~ ssSkP1493("d1")
& ssSkP1493("d0")
& ~ ssSkP1492("d1")
& ssSkP1492("d0")
& ~ ssSkP1491("d1")
& ssSkP1491("d0")
& ~ ssSkP1490("d1")
& ssSkP1490("d0")
& ~ ssSkP149("d1")
& ~ ssSkP149("d0")
& ssSkP1489("d1")
& ssSkP1489("d0")
& ~ ssSkP1488("d1")
& ssSkP1488("d0")
& ~ ssSkP1487("d1")
& ssSkP1487("d0")
& ~ ssSkP1486("d1")
& ssSkP1486("d0")
& ~ ssSkP1485("d1")
& ssSkP1485("d0")
& ~ ssSkP1484("d1")
& ssSkP1484("d0")
& ~ ssSkP1483("d1")
& ssSkP1483("d0")
& ~ ssSkP1482("d1")
& ssSkP1482("d0")
& ~ ssSkP1481("d1")
& ssSkP1481("d0")
& ~ ssSkP1480("d1")
& ssSkP1480("d0")
& ~ ssSkP148("d1")
& ~ ssSkP148("d0")
& ~ ssSkP1479("d1")
& ssSkP1479("d0")
& ~ ssSkP1478("d1")
& ssSkP1478("d0")
& ~ ssSkP1477("d1")
& ssSkP1477("d0")
& ~ ssSkP1476("d1")
& ssSkP1476("d0")
& ~ ssSkP1475("d1")
& ssSkP1475("d0")
& ~ ssSkP1474("d1")
& ssSkP1474("d0")
& ~ ssSkP1473("d1")
& ssSkP1473("d0")
& ~ ssSkP1472("d1")
& ssSkP1472("d0")
& ssSkP1470("d1")
& ~ ssSkP1470("d0")
& ~ ssSkP147("d1")
& ~ ssSkP147("d0")
& ~ ssSkP1469("d1")
& ssSkP1469("d0")
& ssSkP1468("d1")
& ~ ssSkP1468("d0")
& ssSkP1467("d1")
& ~ ssSkP1467("d0")
& ssSkP1466("d1")
& ~ ssSkP1466("d0")
& ssSkP1465("d1")
& ~ ssSkP1465("d0")
& ~ ssSkP1464("d1")
& ssSkP1464("d0")
& ssSkP1463("d1")
& ~ ssSkP1463("d0")
& ssSkP1462("d1")
& ~ ssSkP1462("d0")
& ~ ssSkP1461("d1")
& ssSkP1461("d0")
& ssSkP1460("d1")
& ~ ssSkP1460("d0")
& ~ ssSkP146("d1")
& ~ ssSkP146("d0")
& ssSkP1459("d1")
& ~ ssSkP1459("d0")
& ssSkP1458("d1")
& ~ ssSkP1458("d0")
& ssSkP1457("d1")
& ~ ssSkP1457("d0")
& ssSkP1456("d1")
& ~ ssSkP1456("d0")
& ssSkP1455("d1")
& ~ ssSkP1455("d0")
& ssSkP1453("d1")
& ssSkP1453("d0")
& ~ ssSkP1452("d1")
& ssSkP1452("d0")
& ssSkP1451("d1")
& ssSkP1451("d0")
& ssSkP1450("d1")
& ssSkP1450("d0")
& ~ ssSkP145("d1")
& ~ ssSkP145("d0")
& ssSkP1449("d1")
& ssSkP1449("d0")
& ssSkP1448("d1")
& ssSkP1448("d0")
& ssSkP1447("d1")
& ssSkP1447("d0")
& ssSkP1446("d1")
& ssSkP1446("d0")
& ssSkP1445("d1")
& ssSkP1445("d0")
& ssSkP1444("d1")
& ssSkP1444("d0")
& ssSkP1443("d1")
& ssSkP1443("d0")
& ssSkP1442("d1")
& ssSkP1442("d0")
& ssSkP1441("d1")
& ssSkP1441("d0")
& ssSkP1440("d1")
& ssSkP1440("d0")
& ~ ssSkP144("d1")
& ~ ssSkP144("d0")
& ssSkP1439("d1")
& ssSkP1439("d0")
& ssSkP1438("d1")
& ssSkP1438("d0")
& ssSkP1437("d1")
& ssSkP1437("d0")
& ssSkP1436("d1")
& ssSkP1436("d0")
& ssSkP1435("d1")
& ssSkP1435("d0")
& ssSkP1434("d1")
& ssSkP1434("d0")
& ssSkP1433("d1")
& ssSkP1433("d0")
& ~ ssSkP1432("d1")
& ~ ssSkP1432("d0")
& ~ ssSkP1431("d1")
& ~ ssSkP1431("d0")
& ~ ssSkP1430("d1")
& ~ ssSkP1430("d0")
& ~ ssSkP143("d1")
& ~ ssSkP143("d0")
& ~ ssSkP1429("d1")
& ~ ssSkP1429("d0")
& ~ ssSkP1428("d1")
& ~ ssSkP1428("d0")
& ~ ssSkP1427("d1")
& ~ ssSkP1427("d0")
& ~ ssSkP1426("d1")
& ~ ssSkP1426("d0")
& ~ ssSkP1425("d1")
& ~ ssSkP1425("d0")
& ~ ssSkP1424("d1")
& ~ ssSkP1424("d0")
& ~ ssSkP1423("d1")
& ~ ssSkP1423("d0")
& ~ ssSkP1422("d1")
& ~ ssSkP1422("d0")
& ~ ssSkP1421("d1")
& ~ ssSkP1421("d0")
& ~ ssSkP142("d1")
& ~ ssSkP142("d0")
& ~ ssSkP1418("d1")
& ssSkP1418("d0")
& ssSkP1417("d1")
& ssSkP1417("d0")
& ssSkP1416("d1")
& ssSkP1416("d0")
& ssSkP1415("d1")
& ssSkP1415("d0")
& ssSkP1414("d1")
& ssSkP1414("d0")
& ssSkP1413("d1")
& ssSkP1413("d0")
& ssSkP1412("d1")
& ssSkP1412("d0")
& ssSkP1411("d1")
& ssSkP1411("d0")
& ssSkP1410("d1")
& ssSkP1410("d0")
& ~ ssSkP141("d1")
& ~ ssSkP141("d0")
& ssSkP1409("d1")
& ssSkP1409("d0")
& ssSkP1408("d1")
& ssSkP1408("d0")
& ssSkP1407("d1")
& ssSkP1407("d0")
& ssSkP1406("d1")
& ssSkP1406("d0")
& ssSkP1405("d1")
& ssSkP1405("d0")
& ssSkP1404("d1")
& ssSkP1404("d0")
& ssSkP1403("d1")
& ssSkP1403("d0")
& ssSkP1402("d1")
& ssSkP1402("d0")
& ssSkP1401("d1")
& ssSkP1401("d0")
& ~ ssSkP1400("d1")
& ~ ssSkP1400("d0")
& ~ ssSkP140("d1")
& ~ ssSkP140("d0")
& ~ ssSkP14("d1")
& ~ ssSkP14("d0")
& ~ ssSkP1399("d1")
& ~ ssSkP1399("d0")
& ~ ssSkP1398("d1")
& ~ ssSkP1398("d0")
& ~ ssSkP1397("d1")
& ~ ssSkP1397("d0")
& ~ ssSkP1396("d1")
& ~ ssSkP1396("d0")
& ~ ssSkP1395("d1")
& ~ ssSkP1395("d0")
& ~ ssSkP1394("d1")
& ~ ssSkP1394("d0")
& ~ ssSkP1393("d1")
& ~ ssSkP1393("d0")
& ~ ssSkP1392("d1")
& ~ ssSkP1392("d0")
& ~ ssSkP1391("d1")
& ~ ssSkP1391("d0")
& ~ ssSkP1390("d1")
& ~ ssSkP1390("d0")
& ~ ssSkP139("d1")
& ~ ssSkP139("d0")
& ~ ssSkP1389("d1")
& ~ ssSkP1389("d0")
& ~ ssSkP1388("d1")
& ~ ssSkP1388("d0")
& ~ ssSkP1387("d1")
& ~ ssSkP1387("d0")
& ~ ssSkP1386("d1")
& ~ ssSkP1386("d0")
& ~ ssSkP1385("d1")
& ~ ssSkP1385("d0")
& ~ ssSkP1384("d1")
& ~ ssSkP1384("d0")
& ~ ssSkP1383("d1")
& ~ ssSkP1383("d0")
& ~ ssSkP1382("d1")
& ~ ssSkP1382("d0")
& ~ ssSkP138("d1")
& ~ ssSkP138("d0")
& ~ ssSkP1379("d1")
& ssSkP1379("d0")
& ssSkP1378("d1")
& ssSkP1378("d0")
& ssSkP1377("d1")
& ssSkP1377("d0")
& ssSkP1376("d1")
& ssSkP1376("d0")
& ssSkP1375("d1")
& ssSkP1375("d0")
& ssSkP1374("d1")
& ssSkP1374("d0")
& ssSkP1373("d1")
& ssSkP1373("d0")
& ssSkP1372("d1")
& ssSkP1372("d0")
& ssSkP1371("d1")
& ssSkP1371("d0")
& ssSkP1370("d1")
& ssSkP1370("d0")
& ~ ssSkP137("d1")
& ~ ssSkP137("d0")
& ssSkP1369("d1")
& ssSkP1369("d0")
& ssSkP1368("d1")
& ssSkP1368("d0")
& ssSkP1367("d1")
& ssSkP1367("d0")
& ssSkP1366("d1")
& ssSkP1366("d0")
& ssSkP1365("d1")
& ssSkP1365("d0")
& ssSkP1364("d1")
& ssSkP1364("d0")
& ~ ssSkP1363("d1")
& ssSkP1363("d0")
& ssSkP1362("d1")
& ssSkP1362("d0")
& ssSkP1361("d1")
& ssSkP1361("d0")
& ssSkP1360("d1")
& ssSkP1360("d0")
& ~ ssSkP136("d1")
& ~ ssSkP136("d0")
& ssSkP1359("d1")
& ssSkP1359("d0")
& ssSkP1358("d1")
& ssSkP1358("d0")
& ssSkP1357("d1")
& ssSkP1357("d0")
& ssSkP1356("d1")
& ssSkP1356("d0")
& ssSkP1355("d1")
& ssSkP1355("d0")
& ssSkP1354("d1")
& ssSkP1354("d0")
& ssSkP1353("d1")
& ssSkP1353("d0")
& ssSkP1352("d1")
& ssSkP1352("d0")
& ssSkP1351("d1")
& ssSkP1351("d0")
& ssSkP1350("d1")
& ~ ssSkP1350("d0")
& ~ ssSkP135("d1")
& ~ ssSkP135("d0")
& ssSkP1349("d1")
& ssSkP1349("d0")
& ssSkP1348("d1")
& ssSkP1348("d0")
& ssSkP1347("d1")
& ssSkP1347("d0")
& ssSkP1346("d1")
& ssSkP1346("d0")
& ssSkP1345("d1")
& ssSkP1345("d0")
& ssSkP1344("d1")
& ssSkP1344("d0")
& ssSkP1343("d1")
& ssSkP1343("d0")
& ssSkP1342("d1")
& ssSkP1342("d0")
& ssSkP1341("d1")
& ssSkP1341("d0")
& ssSkP1340("d1")
& ssSkP1340("d0")
& ~ ssSkP134("d1")
& ~ ssSkP134("d0")
& ssSkP1339("d1")
& ssSkP1339("d0")
& ssSkP1338("d1")
& ssSkP1338("d0")
& ~ ssSkP1335("d1")
& ssSkP1335("d0")
& ssSkP1334("d1")
& ssSkP1334("d0")
& ssSkP1333("d1")
& ssSkP1333("d0")
& ssSkP1332("d1")
& ssSkP1332("d0")
& ssSkP1331("d1")
& ssSkP1331("d0")
& ssSkP1330("d1")
& ssSkP1330("d0")
& ~ ssSkP133("d1")
& ~ ssSkP133("d0")
& ssSkP1329("d1")
& ssSkP1329("d0")
& ssSkP1328("d1")
& ssSkP1328("d0")
& ssSkP1327("d1")
& ssSkP1327("d0")
& ssSkP1326("d1")
& ssSkP1326("d0")
& ssSkP1325("d1")
& ssSkP1325("d0")
& ssSkP1324("d1")
& ssSkP1324("d0")
& ssSkP1323("d1")
& ssSkP1323("d0")
& ssSkP1322("d1")
& ssSkP1322("d0")
& ssSkP1321("d1")
& ssSkP1321("d0")
& ~ ssSkP1320("d1")
& ssSkP1320("d0")
& ~ ssSkP132("d1")
& ~ ssSkP132("d0")
& ssSkP1319("d1")
& ssSkP1319("d0")
& ssSkP1318("d1")
& ssSkP1318("d0")
& ssSkP1317("d1")
& ssSkP1317("d0")
& ssSkP1316("d1")
& ssSkP1316("d0")
& ssSkP1315("d1")
& ssSkP1315("d0")
& ssSkP1314("d1")
& ssSkP1314("d0")
& ssSkP1313("d1")
& ssSkP1313("d0")
& ssSkP1312("d1")
& ssSkP1312("d0")
& ssSkP1311("d1")
& ssSkP1311("d0")
& ssSkP1310("d1")
& ssSkP1310("d0")
& ~ ssSkP131("d1")
& ~ ssSkP131("d0")
& ssSkP1309("d1")
& ssSkP1309("d0")
& ssSkP1308("d1")
& ssSkP1308("d0")
& ssSkP1307("d1")
& ssSkP1307("d0")
& ssSkP1306("d1")
& ssSkP1306("d0")
& ssSkP1305("d1")
& ssSkP1305("d0")
& ssSkP1304("d1")
& ssSkP1304("d0")
& ssSkP1303("d1")
& ssSkP1303("d0")
& ssSkP1302("d1")
& ssSkP1302("d0")
& ssSkP1301("d1")
& ~ ssSkP1301("d0")
& ssSkP1300("d1")
& ssSkP1300("d0")
& ~ ssSkP130("d1")
& ~ ssSkP130("d0")
& ~ ssSkP13("d1")
& ~ ssSkP13("d0")
& ~ ssSkP1297("d1")
& ssSkP1297("d0")
& ssSkP1296("d1")
& ssSkP1296("d0")
& ssSkP1295("d1")
& ssSkP1295("d0")
& ssSkP1294("d1")
& ssSkP1294("d0")
& ssSkP1293("d1")
& ssSkP1293("d0")
& ssSkP1292("d1")
& ssSkP1292("d0")
& ssSkP1291("d1")
& ssSkP1291("d0")
& ssSkP1290("d1")
& ssSkP1290("d0")
& ~ ssSkP129("d1")
& ~ ssSkP129("d0")
& ssSkP1289("d1")
& ssSkP1289("d0")
& ssSkP1288("d1")
& ssSkP1288("d0")
& ssSkP1287("d1")
& ssSkP1287("d0")
& ssSkP1286("d1")
& ssSkP1286("d0")
& ssSkP1285("d1")
& ssSkP1285("d0")
& ssSkP1284("d1")
& ssSkP1284("d0")
& ssSkP1283("d1")
& ssSkP1283("d0")
& ~ ssSkP1282("d1")
& ssSkP1282("d0")
& ssSkP1281("d1")
& ssSkP1281("d0")
& ssSkP1280("d1")
& ssSkP1280("d0")
& ~ ssSkP128("d1")
& ~ ssSkP128("d0")
& ssSkP1279("d1")
& ssSkP1279("d0")
& ssSkP1278("d1")
& ssSkP1278("d0")
& ssSkP1277("d1")
& ssSkP1277("d0")
& ssSkP1276("d1")
& ssSkP1276("d0")
& ssSkP1275("d1")
& ssSkP1275("d0")
& ssSkP1274("d1")
& ssSkP1274("d0")
& ssSkP1273("d1")
& ssSkP1273("d0")
& ssSkP1272("d1")
& ssSkP1272("d0")
& ~ ssSkP1271("d1")
& ~ ssSkP1271("d0")
& ~ ssSkP1270("d1")
& ~ ssSkP1270("d0")
& ~ ssSkP127("d1")
& ~ ssSkP127("d0")
& ~ ssSkP1269("d1")
& ~ ssSkP1269("d0")
& ~ ssSkP1268("d1")
& ~ ssSkP1268("d0")
& ~ ssSkP1267("d1")
& ~ ssSkP1267("d0")
& ~ ssSkP1266("d1")
& ~ ssSkP1266("d0")
& ~ ssSkP1263("d1")
& ssSkP1263("d0")
& ssSkP1262("d1")
& ssSkP1262("d0")
& ssSkP1261("d1")
& ssSkP1261("d0")
& ssSkP1260("d1")
& ssSkP1260("d0")
& ~ ssSkP126("d1")
& ~ ssSkP126("d0")
& ssSkP1259("d1")
& ssSkP1259("d0")
& ssSkP1258("d1")
& ssSkP1258("d0")
& ssSkP1257("d1")
& ssSkP1257("d0")
& ssSkP1256("d1")
& ssSkP1256("d0")
& ssSkP1255("d1")
& ssSkP1255("d0")
& ssSkP1254("d1")
& ssSkP1254("d0")
& ssSkP1253("d1")
& ssSkP1253("d0")
& ssSkP1252("d1")
& ssSkP1252("d0")
& ssSkP1251("d1")
& ssSkP1251("d0")
& ssSkP1250("d1")
& ssSkP1250("d0")
& ~ ssSkP125("d1")
& ~ ssSkP125("d0")
& ssSkP1249("d1")
& ssSkP1249("d0")
& ~ ssSkP1248("d1")
& ssSkP1248("d0")
& ssSkP1247("d1")
& ssSkP1247("d0")
& ssSkP1246("d1")
& ssSkP1246("d0")
& ssSkP1245("d1")
& ssSkP1245("d0")
& ssSkP1244("d1")
& ssSkP1244("d0")
& ssSkP1243("d1")
& ssSkP1243("d0")
& ssSkP1242("d1")
& ssSkP1242("d0")
& ssSkP1241("d1")
& ssSkP1241("d0")
& ssSkP1240("d1")
& ssSkP1240("d0")
& ~ ssSkP124("d1")
& ~ ssSkP124("d0")
& ~ ssSkP1239("d1")
& ~ ssSkP1239("d0")
& ~ ssSkP1238("d1")
& ~ ssSkP1238("d0")
& ~ ssSkP1237("d1")
& ~ ssSkP1237("d0")
& ~ ssSkP1236("d1")
& ~ ssSkP1236("d0")
& ~ ssSkP1235("d1")
& ~ ssSkP1235("d0")
& ~ ssSkP1234("d1")
& ~ ssSkP1234("d0")
& ~ ssSkP1231("d1")
& ssSkP1231("d0")
& ssSkP1230("d1")
& ssSkP1230("d0")
& ssSkP1229("d1")
& ssSkP1229("d0")
& ssSkP1228("d1")
& ssSkP1228("d0")
& ssSkP1227("d1")
& ssSkP1227("d0")
& ssSkP1226("d1")
& ssSkP1226("d0")
& ssSkP1225("d1")
& ssSkP1225("d0")
& ssSkP1224("d1")
& ssSkP1224("d0")
& ssSkP1223("d1")
& ssSkP1223("d0")
& ssSkP1222("d1")
& ssSkP1222("d0")
& ssSkP1221("d1")
& ssSkP1221("d0")
& ssSkP1220("d1")
& ssSkP1220("d0")
& ssSkP1219("d1")
& ssSkP1219("d0")
& ssSkP1218("d1")
& ssSkP1218("d0")
& ssSkP1217("d1")
& ssSkP1217("d0")
& ~ ssSkP1216("d1")
& ssSkP1216("d0")
& ssSkP1215("d1")
& ssSkP1215("d0")
& ssSkP1214("d1")
& ssSkP1214("d0")
& ssSkP1213("d1")
& ~ ssSkP1213("d0")
& ssSkP1212("d1")
& ssSkP1212("d0")
& ssSkP1211("d1")
& ssSkP1211("d0")
& ssSkP1210("d1")
& ssSkP1210("d0")
& ~ ssSkP121("d1")
& ssSkP121("d0")
& ssSkP1209("d1")
& ssSkP1209("d0")
& ssSkP1208("d1")
& ssSkP1208("d0")
& ssSkP1207("d1")
& ssSkP1207("d0")
& ssSkP1206("d1")
& ssSkP1206("d0")
& ssSkP1205("d1")
& ssSkP1205("d0")
& ~ ssSkP1204("d1")
& ~ ssSkP1204("d0")
& ~ ssSkP1203("d1")
& ~ ssSkP1203("d0")
& ~ ssSkP1202("d1")
& ~ ssSkP1202("d0")
& ~ ssSkP1201("d1")
& ~ ssSkP1201("d0")
& ~ ssSkP1200("d1")
& ~ ssSkP1200("d0")
& ssSkP120("d1")
& ssSkP120("d0")
& ~ ssSkP12("d1")
& ~ ssSkP12("d0")
& ~ ssSkP1199("d1")
& ~ ssSkP1199("d0")
& ~ ssSkP1198("d1")
& ~ ssSkP1198("d0")
& ~ ssSkP1197("d1")
& ~ ssSkP1197("d0")
& ~ ssSkP1196("d1")
& ~ ssSkP1196("d0")
& ~ ssSkP1195("d1")
& ~ ssSkP1195("d0")
& ~ ssSkP1194("d1")
& ~ ssSkP1194("d0")
& ~ ssSkP1193("d1")
& ~ ssSkP1193("d0")
& ~ ssSkP1192("d1")
& ~ ssSkP1192("d0")
& ~ ssSkP1191("d1")
& ~ ssSkP1191("d0")
& ~ ssSkP1190("d1")
& ~ ssSkP1190("d0")
& ~ ssSkP119("d1")
& ~ ssSkP119("d0")
& ~ ssSkP1187("d1")
& ssSkP1187("d0")
& ssSkP1186("d1")
& ssSkP1186("d0")
& ssSkP1185("d1")
& ssSkP1185("d0")
& ssSkP1184("d1")
& ssSkP1184("d0")
& ssSkP1183("d1")
& ssSkP1183("d0")
& ssSkP1182("d1")
& ssSkP1182("d0")
& ssSkP1181("d1")
& ssSkP1181("d0")
& ssSkP1180("d1")
& ssSkP1180("d0")
& ~ ssSkP118("d1")
& ~ ssSkP118("d0")
& ssSkP1179("d1")
& ssSkP1179("d0")
& ssSkP1178("d1")
& ssSkP1178("d0")
& ssSkP1177("d1")
& ssSkP1177("d0")
& ssSkP1176("d1")
& ssSkP1176("d0")
& ssSkP1175("d1")
& ssSkP1175("d0")
& ssSkP1174("d1")
& ssSkP1174("d0")
& ssSkP1173("d1")
& ssSkP1173("d0")
& ~ ssSkP1172("d1")
& ssSkP1172("d0")
& ssSkP1171("d1")
& ssSkP1171("d0")
& ~ ssSkP1170("d1")
& ssSkP1170("d0")
& ~ ssSkP117("d1")
& ~ ssSkP117("d0")
& ssSkP1169("d1")
& ssSkP1169("d0")
& ssSkP1168("d1")
& ssSkP1168("d0")
& ssSkP1167("d1")
& ssSkP1167("d0")
& ssSkP1166("d1")
& ssSkP1166("d0")
& ssSkP1165("d1")
& ssSkP1165("d0")
& ssSkP1164("d1")
& ssSkP1164("d0")
& ssSkP1163("d1")
& ssSkP1163("d0")
& ssSkP1162("d1")
& ssSkP1162("d0")
& ssSkP1161("d1")
& ssSkP1161("d0")
& ssSkP1160("d1")
& ssSkP1160("d0")
& ~ ssSkP116("d1")
& ~ ssSkP116("d0")
& ssSkP1159("d1")
& ssSkP1159("d0")
& ssSkP1158("d1")
& ssSkP1158("d0")
& ssSkP1157("d1")
& ssSkP1157("d0")
& ssSkP1156("d1")
& ssSkP1156("d0")
& ssSkP1155("d1")
& ssSkP1155("d0")
& ssSkP1154("d1")
& ssSkP1154("d0")
& ssSkP1153("d1")
& ssSkP1153("d0")
& ssSkP1152("d1")
& ssSkP1152("d0")
& ssSkP1151("d1")
& ssSkP1151("d0")
& ssSkP1150("d1")
& ssSkP1150("d0")
& ~ ssSkP115("d1")
& ~ ssSkP115("d0")
& ssSkP1149("d1")
& ssSkP1149("d0")
& ssSkP1148("d1")
& ssSkP1148("d0")
& ssSkP1147("d1")
& ssSkP1147("d0")
& ~ ssSkP1144("d1")
& ssSkP1144("d0")
& ssSkP1143("d1")
& ssSkP1143("d0")
& ssSkP1142("d1")
& ssSkP1142("d0")
& ssSkP1141("d1")
& ssSkP1141("d0")
& ssSkP1140("d1")
& ssSkP1140("d0")
& ~ ssSkP114("d1")
& ~ ssSkP114("d0")
& ssSkP1139("d1")
& ssSkP1139("d0")
& ssSkP1138("d1")
& ssSkP1138("d0")
& ssSkP1137("d1")
& ssSkP1137("d0")
& ssSkP1136("d1")
& ssSkP1136("d0")
& ssSkP1135("d1")
& ssSkP1135("d0")
& ssSkP1134("d1")
& ssSkP1134("d0")
& ssSkP1133("d1")
& ssSkP1133("d0")
& ssSkP1132("d1")
& ssSkP1132("d0")
& ssSkP1131("d1")
& ssSkP1131("d0")
& ssSkP1130("d1")
& ~ ssSkP1130("d0")
& ~ ssSkP113("d1")
& ~ ssSkP113("d0")
& ssSkP1129("d1")
& ssSkP1129("d0")
& ssSkP1128("d1")
& ssSkP1128("d0")
& ssSkP1127("d1")
& ssSkP1127("d0")
& ssSkP1126("d1")
& ssSkP1126("d0")
& ssSkP1125("d1")
& ssSkP1125("d0")
& ssSkP1124("d1")
& ssSkP1124("d0")
& ssSkP1123("d1")
& ssSkP1123("d0")
& ssSkP1122("d1")
& ssSkP1122("d0")
& ssSkP1121("d1")
& ssSkP1121("d0")
& ssSkP1120("d1")
& ssSkP1120("d0")
& ~ ssSkP112("d1")
& ~ ssSkP112("d0")
& ssSkP1119("d1")
& ssSkP1119("d0")
& ssSkP1118("d1")
& ssSkP1118("d0")
& ssSkP1117("d1")
& ssSkP1117("d0")
& ssSkP1116("d1")
& ssSkP1116("d0")
& ssSkP1115("d1")
& ssSkP1115("d0")
& ssSkP1114("d1")
& ssSkP1114("d0")
& ssSkP1113("d1")
& ssSkP1113("d0")
& ssSkP1112("d1")
& ssSkP1112("d0")
& ssSkP1111("d1")
& ssSkP1111("d0")
& ~ ssSkP1110("d1")
& ssSkP1110("d0")
& ~ ssSkP111("d1")
& ~ ssSkP111("d0")
& ssSkP1109("d1")
& ssSkP1109("d0")
& ssSkP1108("d1")
& ssSkP1108("d0")
& ssSkP1107("d1")
& ssSkP1107("d0")
& ssSkP1106("d1")
& ssSkP1106("d0")
& ssSkP1105("d1")
& ssSkP1105("d0")
& ~ ssSkP1104("d1")
& ~ ssSkP1104("d0")
& ~ ssSkP1103("d1")
& ~ ssSkP1103("d0")
& ~ ssSkP1100("d1")
& ssSkP1100("d0")
& ~ ssSkP110("d1")
& ~ ssSkP110("d0")
& ~ ssSkP11("d1")
& ~ ssSkP11("d0")
& ssSkP1099("d1")
& ssSkP1099("d0")
& ssSkP1098("d1")
& ssSkP1098("d0")
& ssSkP1097("d1")
& ssSkP1097("d0")
& ssSkP1096("d1")
& ssSkP1096("d0")
& ssSkP1095("d1")
& ssSkP1095("d0")
& ssSkP1094("d1")
& ssSkP1094("d0")
& ssSkP1093("d1")
& ssSkP1093("d0")
& ssSkP1092("d1")
& ssSkP1092("d0")
& ssSkP1091("d1")
& ssSkP1091("d0")
& ssSkP1090("d1")
& ssSkP1090("d0")
& ~ ssSkP109("d1")
& ~ ssSkP109("d0")
& ssSkP1089("d1")
& ssSkP1089("d0")
& ssSkP1088("d1")
& ssSkP1088("d0")
& ssSkP1087("d1")
& ssSkP1087("d0")
& ssSkP1086("d1")
& ~ ssSkP1086("d0")
& ssSkP1085("d1")
& ssSkP1085("d0")
& ssSkP1084("d1")
& ssSkP1084("d0")
& ssSkP1083("d1")
& ssSkP1083("d0")
& ssSkP1082("d1")
& ssSkP1082("d0")
& ssSkP1081("d1")
& ssSkP1081("d0")
& ssSkP1080("d1")
& ssSkP1080("d0")
& ~ ssSkP108("d1")
& ~ ssSkP108("d0")
& ssSkP1079("d1")
& ssSkP1079("d0")
& ssSkP1078("d1")
& ssSkP1078("d0")
& ssSkP1077("d1")
& ssSkP1077("d0")
& ssSkP1076("d1")
& ssSkP1076("d0")
& ssSkP1075("d1")
& ssSkP1075("d0")
& ~ ssSkP1074("d1")
& ~ ssSkP1074("d0")
& ~ ssSkP1073("d1")
& ~ ssSkP1073("d0")
& ~ ssSkP1072("d1")
& ~ ssSkP1072("d0")
& ~ ssSkP1071("d1")
& ~ ssSkP1071("d0")
& ~ ssSkP1070("d1")
& ~ ssSkP1070("d0")
& ~ ssSkP107("d1")
& ~ ssSkP107("d0")
& ~ ssSkP1069("d1")
& ~ ssSkP1069("d0")
& ~ ssSkP1068("d1")
& ~ ssSkP1068("d0")
& ~ ssSkP1067("d1")
& ~ ssSkP1067("d0")
& ~ ssSkP1066("d1")
& ~ ssSkP1066("d0")
& ~ ssSkP1065("d1")
& ~ ssSkP1065("d0")
& ~ ssSkP1064("d1")
& ~ ssSkP1064("d0")
& ~ ssSkP1063("d1")
& ~ ssSkP1063("d0")
& ~ ssSkP1062("d1")
& ~ ssSkP1062("d0")
& ~ ssSkP1061("d1")
& ~ ssSkP1061("d0")
& ~ ssSkP1060("d1")
& ~ ssSkP1060("d0")
& ~ ssSkP106("d1")
& ~ ssSkP106("d0")
& ~ ssSkP1057("d1")
& ssSkP1057("d0")
& ssSkP1056("d1")
& ssSkP1056("d0")
& ssSkP1055("d1")
& ssSkP1055("d0")
& ssSkP1054("d1")
& ssSkP1054("d0")
& ssSkP1053("d1")
& ssSkP1053("d0")
& ssSkP1052("d1")
& ssSkP1052("d0")
& ssSkP1051("d1")
& ssSkP1051("d0")
& ssSkP1050("d1")
& ssSkP1050("d0")
& ~ ssSkP105("d1")
& ~ ssSkP105("d0")
& ssSkP1049("d1")
& ssSkP1049("d0")
& ssSkP1048("d1")
& ssSkP1048("d0")
& ssSkP1047("d1")
& ssSkP1047("d0")
& ssSkP1046("d1")
& ssSkP1046("d0")
& ssSkP1045("d1")
& ssSkP1045("d0")
& ~ ssSkP1044("d1")
& ssSkP1044("d0")
& ssSkP1043("d1")
& ssSkP1043("d0")
& ssSkP1042("d1")
& ssSkP1042("d0")
& ssSkP1041("d1")
& ssSkP1041("d0")
& ssSkP1040("d1")
& ssSkP1040("d0")
& ~ ssSkP104("d1")
& ~ ssSkP104("d0")
& ssSkP1039("d1")
& ssSkP1039("d0")
& ssSkP1038("d1")
& ssSkP1038("d0")
& ssSkP1037("d1")
& ssSkP1037("d0")
& ssSkP1036("d1")
& ssSkP1036("d0")
& ssSkP1035("d1")
& ssSkP1035("d0")
& ssSkP1034("d1")
& ssSkP1034("d0")
& ssSkP1033("d1")
& ssSkP1033("d0")
& ssSkP1032("d1")
& ssSkP1032("d0")
& ssSkP1031("d1")
& ssSkP1031("d0")
& ssSkP1030("d1")
& ssSkP1030("d0")
& ~ ssSkP103("d1")
& ~ ssSkP103("d0")
& ssSkP1029("d1")
& ssSkP1029("d0")
& ssSkP1028("d1")
& ~ ssSkP1028("d0")
& ssSkP1027("d1")
& ssSkP1027("d0")
& ssSkP1026("d1")
& ssSkP1026("d0")
& ssSkP1025("d1")
& ssSkP1025("d0")
& ssSkP1024("d1")
& ssSkP1024("d0")
& ssSkP1023("d1")
& ssSkP1023("d0")
& ssSkP1022("d1")
& ssSkP1022("d0")
& ssSkP1021("d1")
& ssSkP1021("d0")
& ssSkP1020("d1")
& ssSkP1020("d0")
& ~ ssSkP102("d1")
& ~ ssSkP102("d0")
& ssSkP1019("d1")
& ssSkP1019("d0")
& ssSkP1018("d1")
& ssSkP1018("d0")
& ~ ssSkP1015("d1")
& ssSkP1015("d0")
& ssSkP1014("d1")
& ssSkP1014("d0")
& ssSkP1013("d1")
& ssSkP1013("d0")
& ssSkP1012("d1")
& ssSkP1012("d0")
& ssSkP1011("d1")
& ssSkP1011("d0")
& ssSkP1010("d1")
& ssSkP1010("d0")
& ~ ssSkP101("d1")
& ~ ssSkP101("d0")
& ssSkP1009("d1")
& ssSkP1009("d0")
& ssSkP1008("d1")
& ssSkP1008("d0")
& ssSkP1007("d1")
& ssSkP1007("d0")
& ssSkP1006("d1")
& ssSkP1006("d0")
& ssSkP1005("d1")
& ssSkP1005("d0")
& ssSkP1004("d1")
& ssSkP1004("d0")
& ssSkP1003("d1")
& ssSkP1003("d0")
& ssSkP1002("d1")
& ~ ssSkP1002("d0")
& ssSkP1001("d1")
& ssSkP1001("d0")
& ssSkP1000("d1")
& ssSkP1000("d0")
& ~ ssSkP100("d1")
& ~ ssSkP100("d0")
& ~ ssSkP10("d1")
& ~ ssSkP10("d0")
& ~ ssPv9("d1")
& ssPv9("d0")
& ~ ssPv8("d1")
& ~ ssPv8("d0")
& ~ ssPv7("d1")
& ~ ssPv7("d0")
& ssPv6("d1")
& ssPv6("d0")
& ssPv5("d1")
& ssPv5("d0")
& ~ ssPv40("d1")
& ~ ssPv40("d0")
& ~ ssPv4("d1")
& ~ ssPv4("d0")
& ssPv39("d1")
& ssPv39("d0")
& ssPv38("d1")
& ssPv38("d0")
& ~ ssPv37("d1")
& ~ ssPv37("d0")
& ssPv36("d1")
& ssPv36("d0")
& ~ ssPv34("d1")
& ~ ssPv34("d0")
& ssPv33("d1")
& ssPv33("d0")
& ~ ssPv32("d1")
& ssPv32("d0")
& ~ ssPv31("d1")
& ssPv31("d0")
& ~ ssPv30("d1")
& ssPv30("d0")
& ~ ssPv3("d1")
& ~ ssPv3("d0")
& ~ ssPv29("d1")
& ssPv29("d0")
& ~ ssPv28("d1")
& ssPv28("d0")
& ~ ssPv27("d1")
& ssPv27("d0")
& ~ ssPv26("d1")
& ssPv26("d0")
& ~ ssPv25("d1")
& ssPv25("d0")
& ~ ssPv24("d1")
& ~ ssPv24("d0")
& ~ ssPv23("d1")
& ~ ssPv23("d0")
& ssPv22("d1")
& ssPv22("d0")
& ~ ssPv21("d1")
& ~ ssPv21("d0")
& ~ ssPv20("d1")
& ~ ssPv20("d0")
& ~ ssPv2("d1")
& ~ ssPv2("d0")
& ~ ssPv19("d1")
& ~ ssPv19("d0")
& ~ ssPv18("d1")
& ~ ssPv18("d0")
& ssPv17("d1")
& ssPv17("d0")
& ~ ssPv16("d1")
& ssPv16("d0")
& ~ ssPv15("d1")
& ssPv15("d0")
& ~ ssPv14("d1")
& ssPv14("d0")
& ~ ssPv13("d1")
& ssPv13("d0")
& ~ ssPv12("d1")
& ssPv12("d0")
& ~ ssPv11("d1")
& ssPv11("d0")
& ~ ssPv10("d1")
& ssPv10("d0")
& ~ ssSkC9
& ~ ssSkC8
& ~ ssSkC7
& ~ ssSkC6
& ~ ssSkC5
& ~ ssSkC40
& ~ ssSkC4
& ~ ssSkC39
& ~ ssSkC38
& ~ ssSkC37
& ~ ssSkC36
& ~ ssSkC35
& ~ ssSkC34
& ~ ssSkC33
& ~ ssSkC32
& ~ ssSkC31
& ~ ssSkC30
& ~ ssSkC3
& ~ ssSkC29
& ~ ssSkC28
& ~ ssSkC27
& ~ ssSkC26
& ~ ssSkC25
& ~ ssSkC24
& ~ ssSkC23
& ~ ssSkC22
& ~ ssSkC21
& ~ ssSkC20
& ~ ssSkC2
& ~ ssSkC19
& ~ ssSkC18
& ~ ssSkC17
& ~ ssSkC16
& ~ ssSkC15
& ~ ssSkC14
& ~ ssSkC13
& ~ ssSkC12
& ~ ssSkC11
& ~ ssSkC10
& ~ ssSkC1
& ~ ssSkC0 ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN912-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : mace4 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n002.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sat Sep 26 18:51:39 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.37 % Mace4 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.37 % Process 2427970 was started by sandbox2 on n002,
% 0.11/0.37 % Sat Sep 26 18:51:39 2026
% 0.11/0.37 % The command was "/export/starexec/sandbox2/solver/bin/mace4 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 1.20/0.60
% 1.20/0.60 % SZS status Satisfiable for theBenchmark
% 1.20/0.60 % SZS output start FiniteModel for theBenchmark
% See solution above
%------------------------------------------------------------------------------