%------------------------------------------------------------------------------
% File : Mace4---2026-6A
% Problem : SYN905-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : mace4 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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:02 AM UTC 2026
% Result : Satisfiable 0.14s 0.45s
% Output : FiniteModel 0.14s
% 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") = "d1"
& skf92("d0") = "d0"
& skf91("d1") = "d1"
& skf91("d0") = "d0"
& skf90("d1") = "d0"
& skf90("d0") = "d1"
& skf89("d1") = "d0"
& skf89("d0") = "d1"
& skf88("d1") = "d0"
& skf88("d0") = "d1"
& skf87("d1") = "d1"
& skf87("d0") = "d0"
& skf86("d1") = "d0"
& skf86("d0") = "d1"
& skf85("d1") = "d1"
& skf85("d0") = "d0"
& skf84("d1") = "d0"
& skf84("d0") = "d1"
& skf83("d1") = "d1"
& skf83("d0") = "d0"
& skf82("d1") = "d0"
& skf82("d0") = "d1"
& skf81("d1") = "d1"
& skf81("d0") = "d0"
& skf80("d1") = "d0"
& skf80("d0") = "d0"
& skf159("d1") = "d0"
& skf159("d0") = "d0"
& skf158("d1") = "d0"
& skf158("d0") = "d0"
& skf157("d1") = "d0"
& skf157("d0") = "d0"
& skf156("d1") = "d0"
& skf156("d0") = "d0"
& skf155("d1") = "d0"
& skf155("d0") = "d0"
& skf154("d1") = "d0"
& skf154("d0") = "d0"
& skf153("d1") = "d0"
& skf153("d0") = "d0"
& skf152("d1") = "d0"
& skf152("d0") = "d0"
& skf151("d1") = "d0"
& skf151("d0") = "d0"
& skf150("d1") = "d0"
& skf150("d0") = "d0"
& skf149("d1") = "d0"
& skf149("d0") = "d0"
& skf148("d1") = "d0"
& skf148("d0") = "d0"
& skf147("d1") = "d0"
& skf147("d0") = "d0"
& skf146("d1") = "d0"
& skf146("d0") = "d0"
& skf145("d1") = "d0"
& skf145("d0") = "d0"
& skf144("d1") = "d0"
& skf144("d0") = "d0"
& skf143("d1") = "d0"
& skf143("d0") = "d0"
& skf142("d1") = "d0"
& skf142("d0") = "d0"
& skf141("d1") = "d0"
& skf141("d0") = "d0"
& skf140("d1") = "d0"
& skf140("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"
& skc21 = "d0"
& skc20 = "d0"
& skc19 = "d0"
& skc18 = "d0"
& skc17 = "d0"
& skc16 = "d0"
& skc15 = "d0"
& skc14 = "d0"
& skc13 = "d0"
& skc12 = "d0"
& skc11 = "d0" ) ).
fof(interp_relations,interpretation-mappings,
( ssSkP61("d1","d1")
& ssSkP61("d1","d0")
& ssSkP61("d0","d1")
& ssSkP61("d0","d0")
& ssSkP60("d1","d1")
& ssSkP60("d1","d0")
& ssSkP60("d0","d1")
& ssSkP60("d0","d0")
& ssSkP531("d1","d1")
& ssSkP531("d1","d0")
& ssSkP531("d0","d1")
& ssSkP531("d0","d0")
& ssSkP517("d1","d1")
& ssSkP517("d1","d0")
& ssSkP517("d0","d1")
& ssSkP517("d0","d0")
& ssSkP457("d1","d1")
& ssSkP457("d1","d0")
& ssSkP457("d0","d1")
& ssSkP457("d0","d0")
& ssSkP456("d1","d1")
& ssSkP456("d1","d0")
& ssSkP456("d0","d1")
& ssSkP456("d0","d0")
& ssSkP403("d1","d1")
& ssSkP403("d1","d0")
& ssSkP403("d0","d1")
& ssSkP403("d0","d0")
& ssSkP402("d1","d1")
& ssSkP402("d1","d0")
& ssSkP402("d0","d1")
& ssSkP402("d0","d0")
& ssSkP349("d1","d1")
& ssSkP349("d1","d0")
& ssSkP349("d0","d1")
& ssSkP349("d0","d0")
& ssSkP348("d1","d1")
& ssSkP348("d1","d0")
& ssSkP348("d0","d1")
& ssSkP348("d0","d0")
& ssSkP289("d1","d1")
& ssSkP289("d1","d0")
& ssSkP289("d0","d1")
& ssSkP289("d0","d0")
& ssSkP288("d1","d1")
& ssSkP288("d1","d0")
& ssSkP288("d0","d1")
& ssSkP288("d0","d0")
& ssSkP238("d1","d1")
& ssSkP238("d1","d0")
& ssSkP238("d0","d1")
& ssSkP238("d0","d0")
& ssSkP237("d1","d1")
& ssSkP237("d1","d0")
& ssSkP237("d0","d1")
& ssSkP237("d0","d0")
& ssSkP192("d1","d1")
& ssSkP192("d1","d0")
& ssSkP192("d0","d1")
& ssSkP192("d0","d0")
& ssSkP191("d1","d1")
& ssSkP191("d1","d0")
& ssSkP191("d0","d1")
& ssSkP191("d0","d0")
& ssSkP150("d1","d1")
& ssSkP150("d1","d0")
& ssSkP150("d0","d1")
& ssSkP150("d0","d0")
& ssSkP149("d1","d1")
& ssSkP149("d1","d0")
& ssSkP149("d0","d1")
& ssSkP149("d0","d0")
& ssSkP102("d1","d1")
& ssSkP102("d1","d0")
& ssSkP102("d0","d1")
& ssSkP102("d0","d0")
& ssSkP101("d1","d1")
& ssSkP101("d1","d0")
& ssSkP101("d0","d1")
& ssSkP101("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")
& ssSkP99("d1")
& ssSkP99("d0")
& ssSkP98("d1")
& ssSkP98("d0")
& ssSkP97("d1")
& ssSkP97("d0")
& ssSkP96("d1")
& ssSkP96("d0")
& ssSkP95("d1")
& ssSkP95("d0")
& ~ ssSkP94("d1")
& ~ ssSkP94("d0")
& ~ ssSkP93("d1")
& ~ ssSkP93("d0")
& ~ ssSkP92("d1")
& ~ ssSkP92("d0")
& ~ ssSkP91("d1")
& ~ ssSkP91("d0")
& ~ ssSkP90("d1")
& ~ ssSkP90("d0")
& ~ ssSkP9("d1")
& ~ ssSkP9("d0")
& ~ ssSkP89("d1")
& ~ ssSkP89("d0")
& ~ ssSkP88("d1")
& ~ ssSkP88("d0")
& ~ ssSkP87("d1")
& ~ ssSkP87("d0")
& ~ ssSkP86("d1")
& ~ ssSkP86("d0")
& ~ ssSkP85("d1")
& ~ ssSkP85("d0")
& ~ ssSkP84("d1")
& ~ ssSkP84("d0")
& ~ ssSkP83("d1")
& ~ ssSkP83("d0")
& ~ ssSkP82("d1")
& ~ ssSkP82("d0")
& ~ ssSkP81("d1")
& ~ ssSkP81("d0")
& ~ ssSkP80("d1")
& ~ ssSkP80("d0")
& ~ ssSkP8("d1")
& ~ ssSkP8("d0")
& ~ ssSkP79("d1")
& ~ ssSkP79("d0")
& ~ ssSkP78("d1")
& ~ ssSkP78("d0")
& ~ ssSkP77("d1")
& ~ ssSkP77("d0")
& ~ ssSkP76("d1")
& ~ ssSkP76("d0")
& ~ ssSkP75("d1")
& ~ ssSkP75("d0")
& ~ ssSkP74("d1")
& ~ ssSkP74("d0")
& ~ ssSkP73("d1")
& ~ ssSkP73("d0")
& ~ ssSkP72("d1")
& ~ ssSkP72("d0")
& ~ ssSkP71("d1")
& ~ ssSkP71("d0")
& ~ ssSkP70("d1")
& ~ ssSkP70("d0")
& ~ ssSkP7("d1")
& ~ ssSkP7("d0")
& ~ ssSkP69("d1")
& ~ ssSkP69("d0")
& ~ ssSkP68("d1")
& ~ ssSkP68("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")
& ssSkP668("d1")
& ssSkP668("d0")
& ssSkP667("d1")
& ssSkP667("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")
& ssSkP646("d1")
& ssSkP646("d0")
& ssSkP645("d1")
& ssSkP645("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")
& ssSkP609("d1")
& ssSkP609("d0")
& ssSkP608("d1")
& ssSkP608("d0")
& ssSkP607("d1")
& ssSkP607("d0")
& ssSkP606("d1")
& ssSkP606("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")
& ~ 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")
& ssSkP573("d1")
& ssSkP573("d0")
& ssSkP572("d1")
& ssSkP572("d0")
& ssSkP571("d1")
& ssSkP571("d0")
& ssSkP570("d1")
& ssSkP570("d0")
& ssSkP57("d1")
& ssSkP57("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")
& ssSkP56("d1")
& ssSkP56("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")
& ~ ssSkP530("d1")
& ssSkP530("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")
& 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")
& ssSkP496("d1")
& ssSkP496("d0")
& ssSkP495("d1")
& ssSkP495("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")
& ~ ssSkP458("d1")
& ~ ssSkP458("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")
& ssSkP419("d1")
& ssSkP419("d0")
& ssSkP418("d1")
& ssSkP418("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")
& ~ 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")
& ssSkP387("d1")
& ssSkP387("d0")
& ssSkP386("d1")
& ssSkP386("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")
& ssSkP366("d1")
& ssSkP366("d0")
& ssSkP365("d1")
& ssSkP365("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")
& ~ 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")
& ~ ssSkP326("d1")
& ~ ssSkP326("d0")
& ~ ssSkP325("d1")
& ~ ssSkP325("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")
& ~ ssSkP287("d1")
& ssSkP287("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")
& ~ ssSkP265("d1")
& ~ ssSkP265("d0")
& ~ ssSkP264("d1")
& ~ ssSkP264("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")
& ~ ssSkP236("d1")
& ssSkP236("d0")
& ssSkP235("d1")
& ssSkP235("d0")
& ssSkP234("d1")
& ssSkP234("d0")
& ssSkP233("d1")
& ssSkP233("d0")
& ssSkP232("d1")
& ssSkP232("d0")
& ssSkP231("d1")
& ssSkP231("d0")
& ssSkP230("d1")
& ssSkP230("d0")
& ~ ssSkP23("d1")
& ~ ssSkP23("d0")
& ssSkP229("d1")
& ssSkP229("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")
& ~ ssSkP21("d1")
& ~ ssSkP21("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")
& ~ ssSkP20("d1")
& ~ ssSkP20("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")
& ~ ssSkP190("d1")
& ssSkP190("d0")
& ~ ssSkP19("d1")
& ~ ssSkP19("d0")
& ssSkP189("d1")
& ssSkP189("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")
& ~ ssSkP159("d1")
& ~ ssSkP159("d0")
& ~ ssSkP158("d1")
& ~ ssSkP158("d0")
& ~ ssSkP157("d1")
& ~ ssSkP157("d0")
& ~ ssSkP156("d1")
& ~ ssSkP156("d0")
& ~ ssSkP155("d1")
& ~ ssSkP155("d0")
& ~ ssSkP154("d1")
& ~ ssSkP154("d0")
& ~ ssSkP153("d1")
& ~ ssSkP153("d0")
& ~ ssSkP152("d1")
& ~ ssSkP152("d0")
& ~ ssSkP151("d1")
& ~ ssSkP151("d0")
& ~ ssSkP15("d1")
& ~ ssSkP15("d0")
& ~ ssSkP148("d1")
& ssSkP148("d0")
& ssSkP147("d1")
& ssSkP147("d0")
& ssSkP146("d1")
& ssSkP146("d0")
& ssSkP145("d1")
& ssSkP145("d0")
& ssSkP144("d1")
& ssSkP144("d0")
& ssSkP143("d1")
& ssSkP143("d0")
& ssSkP142("d1")
& ssSkP142("d0")
& ssSkP141("d1")
& ssSkP141("d0")
& ~ ssSkP140("d1")
& ~ ssSkP140("d0")
& ~ ssSkP14("d1")
& ~ ssSkP14("d0")
& ~ ssSkP139("d1")
& ~ ssSkP139("d0")
& ~ ssSkP138("d1")
& ~ ssSkP138("d0")
& ~ ssSkP137("d1")
& ~ ssSkP137("d0")
& ~ ssSkP136("d1")
& ~ ssSkP136("d0")
& ~ ssSkP135("d1")
& ~ ssSkP135("d0")
& ~ ssSkP134("d1")
& ~ ssSkP134("d0")
& ~ ssSkP133("d1")
& ~ ssSkP133("d0")
& ~ ssSkP132("d1")
& ~ ssSkP132("d0")
& ~ ssSkP131("d1")
& ~ ssSkP131("d0")
& ~ ssSkP130("d1")
& ~ ssSkP130("d0")
& ~ ssSkP13("d1")
& ~ ssSkP13("d0")
& ~ ssSkP129("d1")
& ~ ssSkP129("d0")
& ~ ssSkP128("d1")
& ~ ssSkP128("d0")
& ~ ssSkP127("d1")
& ~ ssSkP127("d0")
& ~ ssSkP126("d1")
& ~ ssSkP126("d0")
& ~ ssSkP125("d1")
& ~ ssSkP125("d0")
& ~ ssSkP124("d1")
& ~ ssSkP124("d0")
& ~ ssSkP123("d1")
& ~ ssSkP123("d0")
& ~ ssSkP122("d1")
& ~ ssSkP122("d0")
& ~ ssSkP121("d1")
& ~ ssSkP121("d0")
& ~ ssSkP120("d1")
& ~ ssSkP120("d0")
& ~ ssSkP12("d1")
& ~ ssSkP12("d0")
& ~ ssSkP119("d1")
& ~ ssSkP119("d0")
& ~ ssSkP118("d1")
& ~ ssSkP118("d0")
& ~ ssSkP117("d1")
& ~ ssSkP117("d0")
& ~ ssSkP116("d1")
& ~ ssSkP116("d0")
& ~ ssSkP115("d1")
& ~ ssSkP115("d0")
& ~ ssSkP114("d1")
& ~ ssSkP114("d0")
& ~ ssSkP113("d1")
& ~ ssSkP113("d0")
& ~ ssSkP112("d1")
& ~ ssSkP112("d0")
& ~ ssSkP111("d1")
& ~ ssSkP111("d0")
& ~ ssSkP110("d1")
& ~ ssSkP110("d0")
& ~ ssSkP11("d1")
& ~ ssSkP11("d0")
& ~ ssSkP109("d1")
& ~ ssSkP109("d0")
& ~ ssSkP108("d1")
& ~ ssSkP108("d0")
& ~ ssSkP107("d1")
& ~ ssSkP107("d0")
& ~ ssSkP106("d1")
& ~ ssSkP106("d0")
& ~ ssSkP105("d1")
& ~ ssSkP105("d0")
& ~ ssSkP104("d1")
& ~ ssSkP104("d0")
& ~ ssSkP103("d1")
& ~ ssSkP103("d0")
& ~ ssSkP100("d1")
& ssSkP100("d0")
& ~ ssSkP10("d1")
& ~ ssSkP10("d0")
& ~ ssPv9("d1")
& ssPv9("d0")
& ~ ssPv8("d1")
& ~ ssPv8("d0")
& ssPv53("d1")
& ssPv53("d0")
& ~ ssPv52("d1")
& ~ ssPv52("d0")
& ~ ssPv50("d1")
& ~ ssPv50("d0")
& ~ ssPv48("d1")
& ssPv48("d0")
& ~ ssPv47("d1")
& ssPv47("d0")
& ~ ssPv46("d1")
& ssPv46("d0")
& ~ ssPv41("d1")
& ssPv41("d0")
& ~ ssPv39("d1")
& ~ ssPv39("d0")
& ssPv36("d1")
& ssPv36("d0")
& ~ ssPv34("d1")
& ~ ssPv34("d0")
& ~ ssPv30("d1")
& ssPv30("d0")
& ~ ssPv29("d1")
& ssPv29("d0")
& ~ ssPv28("d1")
& ssPv28("d0")
& ~ ssPv25("d1")
& ssPv25("d0")
& ~ ssPv24("d1")
& ~ ssPv24("d0")
& ~ ssPv22("d1")
& ~ ssPv22("d0")
& ~ ssPv21("d1")
& ~ ssPv21("d0")
& ~ ssPv20("d1")
& ~ ssPv20("d0")
& ~ ssPv2("d1")
& ~ ssPv2("d0")
& ~ ssPv17("d1")
& ~ ssPv17("d0")
& ~ ssPv16("d1")
& ssPv16("d0")
& ~ ssPv14("d1")
& ssPv14("d0")
& ~ ssPv12("d1")
& ssPv12("d0")
& ~ ssPv11("d1")
& ssPv11("d0")
& ~ ssSkC9
& ~ ssSkC8
& ~ ssSkC7
& ~ ssSkC6
& ~ ssSkC5
& ~ ssSkC4
& ~ ssSkC3
& ~ ssSkC2
& ~ ssSkC10
& ~ ssSkC1
& ~ ssSkC0 ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN905-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : mace4 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n015.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 18:50:29 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.14/0.36 % Mace4 (64) version 2026-6A, July 2026, CASC-J13.
% 0.14/0.36 % Process 516554 was started by sandbox on n015,
% 0.14/0.36 % Sat Sep 26 18:50:29 2026
% 0.14/0.36 % The command was "/export/starexec/sandbox/solver/bin/mace4 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.14/0.45
% 0.14/0.45 % SZS status Satisfiable for theBenchmark
% 0.14/0.45 % SZS output start FiniteModel for theBenchmark
% See solution above
%------------------------------------------------------------------------------