%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : SYN911-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n005.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 : Fri Sep 25 03:38:39 PM UTC 2026
% Result : Satisfiable 4.87s 1.83s
% Output : FiniteModel 5.33s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(domain,interpretation-domains,
! [X] :
( X = "d2"
| X = "d1"
| X = "d0" ) ).
fof(mappings,interpretation-mappings,
( skf101("d2") = "d1"
& skf101("d0") = "d1"
& skf101("d1") = "d1"
& skf100("d1") = "d1"
& skf100("d0") = "d1"
& skf100("d2") = "d0"
& skf81("d2") = "d0"
& skf80("d2") = "d0"
& skf81("d1") = "d1"
& skf80("d0") = "d1"
& skf81("d0") = "d1"
& skf80("d1") = "d1"
& skf85("d2") = "d0"
& skf82("d0") = "d1"
& skf83("d1") = "d1"
& skf84("d2") = "d0"
& skf83("d0") = "d1"
& skf82("d1") = "d1"
& skf85("d1") = "d1"
& skf84("d0") = "d1"
& skf83("d2") = "d0"
& skf85("d0") = "d1"
& skf84("d1") = "d1"
& skf82("d2") = "d0"
& skf89("d2") = "d0"
& skf86("d0") = "d1"
& skf87("d1") = "d1"
& skf88("d2") = "d0"
& skf86("d1") = "d1"
& skf87("d0") = "d1"
& skf89("d1") = "d1"
& skf88("d0") = "d1"
& skf87("d2") = "d0"
& skf89("d0") = "d1"
& skf88("d1") = "d1"
& skf86("d2") = "d0"
& skf92("d2") = "d0"
& skf90("d1") = "d1"
& skf91("d2") = "d0"
& skf90("d0") = "d1"
& skf92("d1") = "d1"
& skf91("d0") = "d1"
& skf90("d2") = "d0"
& skf92("d0") = "d1"
& skf91("d1") = "d1"
& skf96("d2") = "d0"
& skf94("d1") = "d1"
& skf93("d0") = "d1"
& skf95("d2") = "d0"
& skf94("d0") = "d1"
& skf93("d1") = "d1"
& skf96("d1") = "d1"
& skf94("d2") = "d0"
& skf95("d0") = "d1"
& skf96("d0") = "d1"
& skf95("d1") = "d1"
& skf93("d2") = "d0"
& skf98("d2") = "d2"
& skf98("d1") = "d1"
& skf97("d0") = "d1"
& skf99("d2") = "d0"
& skf98("d0") = "d1"
& skf97("d1") = "d1"
& skf99("d0") = "d1"
& skf99("d1") = "d1"
& skf97("d2") = "d0"
& skf63("d0") = "d2"
& skf63("d2") = "d0"
& skf60("d1") = "d0"
& skf62("d2") = "d0"
& skf61("d1") = "d0"
& skf60("d0") = "d0"
& skf61("d0") = "d1"
& skf62("d1") = "d0"
& skf61("d2") = "d0"
& skf63("d1") = "d0"
& skf62("d0") = "d0"
& skf60("d2") = "d0"
& skf67("d0") = "d2"
& skf67("d2") = "d0"
& skf65("d1") = "d1"
& skf65("d0") = "d0"
& skf66("d2") = "d0"
& skf64("d1") = "d1"
& skf67("d1") = "d1"
& skf65("d2") = "d0"
& skf66("d1") = "d1"
& skf66("d0") = "d0"
& skf64("d0") = "d2"
& skf64("d2") = "d0"
& skf69("d1") = "d1"
& skf69("d0") = "d0"
& skf68("d0") = "d1"
& skf68("d1") = "d1"
& skf69("d2") = "d0"
& skf68("d2") = "d0"
& skf70("d2") = "d0"
& skf70("d1") = "d1"
& skf70("d0") = "d0"
& skf74("d2") = "d0"
& skf72("d1") = "d1"
& skf72("d0") = "d0"
& skf73("d2") = "d0"
& skf71("d1") = "d1"
& skf71("d0") = "d0"
& skf74("d1") = "d1"
& skf74("d0") = "d0"
& skf72("d2") = "d0"
& skf73("d1") = "d1"
& skf71("d2") = "d0"
& skf73("d0") = "d0"
& skf78("d2") = "d0"
& skf76("d1") = "d1"
& skf77("d2") = "d0"
& skf76("d0") = "d1"
& skf75("d0") = "d0"
& skf75("d1") = "d1"
& skf78("d1") = "d1"
& skf77("d0") = "d1"
& skf76("d2") = "d0"
& skf78("d0") = "d1"
& skf77("d1") = "d1"
& skf75("d2") = "d0"
& skf79("d0") = "d1"
& skf79("d1") = "d1"
& skf79("d2") = "d0"
& skf52("d0") = "d2"
& skf52("d2") = "d0"
& skf51("d2") = "d0"
& skf51("d0") = "d1"
& skf52("d1") = "d0"
& skf51("d1") = "d1"
& skf56("d0") = "d2"
& skf56("d2") = "d0"
& skf54("d0") = "d0"
& skf53("d1") = "d0"
& skf55("d0") = "d2"
& skf55("d2") = "d0"
& skf54("d1") = "d0"
& skf53("d0") = "d0"
& skf55("d1") = "d0"
& skf54("d2") = "d0"
& skf56("d1") = "d0"
& skf53("d2") = "d0"
& skf57("d1") = "d0"
& skf57("d0") = "d1"
& skf59("d2") = "d0"
& skf58("d0") = "d1"
& skf58("d1") = "d0"
& skf59("d0") = "d1"
& skf59("d1") = "d0"
& skf58("d2") = "d0"
& skf57("d2") = "d0"
& skc46 = "d0"
& skc45 = "d0"
& skc48 = "d0"
& skc47 = "d0"
& skc41 = "d0"
& skc44 = "d0"
& skc43 = "d0"
& skc49 = "d0"
& skc57 = "d0"
& skc56 = "d0"
& skc59 = "d0"
& skc58 = "d0"
& skc53 = "d0"
& skc52 = "d0"
& skc55 = "d0"
& skc54 = "d0"
& skc50 = "d2"
& skc51 = "d0"
& skc68 = "d2"
& skc67 = "d2"
& skc63 = "d0"
& skc61 = "d0"
& skc79 = "d0"
& skc78 = "d0"
& skc75 = "d0"
& skc74 = "d0"
& skc76 = "d0"
& skc72 = "d0"
& skc81 = "d0" ) ).
fof(predicate_mappings,interpretation-mappings,
( ssPv27("d0")
& ~ ssPv26("d1")
& ~ ssPv25("d2")
& ssPv27("d1")
& ~ ssPv26("d0")
& ~ ssPv24("d2")
& ~ ssPv27("d2")
& ~ ssPv25("d0")
& ssPv24("d1")
& ~ ssPv26("d2")
& ~ ssPv25("d1")
& ~ ssPv24("d0")
& ~ ssPv28("d2")
& ~ ssPv28("d1")
& ~ ssPv28("d0")
& ~ ssPv21("d2")
& ssPv22("d1")
& ~ ssPv23("d0")
& ~ ssPv20("d2")
& ~ ssPv22("d0")
& ssPv23("d1")
& ssPv20("d1")
& ~ ssPv21("d0")
& ~ ssPv23("d2")
& ssPv20("d0")
& ssPv21("d1")
& ~ ssPv22("d2")
& ~ ssPv16("d0")
& ssPv15("d1")
& ~ ssPv14("d2")
& ssPv16("d1")
& ~ ssPv15("d0")
& ~ ssPv13("d2")
& ~ ssPv16("d2")
& ssPv13("d1")
& ~ ssPv14("d0")
& ~ ssPv15("d2")
& ~ ssPv13("d0")
& ssPv14("d1")
& ~ ssPv19("d1")
& ~ ssPv19("d0")
& ~ ssPv19("d2")
& ssPv12("d0")
& ssPv11("d1")
& ssPv12("d1")
& ssPv11("d0")
& ~ ssPv12("d2")
& ~ ssPv11("d2")
& ~ ssSkP400("d2","d0")
& ~ ssSkP400("d0","d2")
& ssSkP401("d1","d2")
& ~ ssSkP401("d2","d1")
& ~ ssSkP400("d2","d1")
& ~ ssSkP400("d1","d2")
& ssSkP401("d0","d2")
& ~ ssSkP401("d2","d0")
& ~ ssSkP400("d2","d2")
& ssSkP400("d1","d1")
& ssSkP400("d0","d0")
& ssSkP401("d0","d1")
& ssSkP401("d1","d0")
& ssSkP400("d1","d0")
& ssSkP400("d0","d1")
& ~ ssSkP401("d2","d2")
& ssSkP401("d1","d1")
& ssSkP401("d0","d0")
& ssSkP300("d1")
& ssSkP300("d0")
& ~ ssSkP300("d2")
& ssSkP304("d1")
& ssSkP303("d0")
& ~ ssSkP301("d2")
& ssSkP304("d0")
& ssSkP303("d1")
& ~ ssSkP302("d2")
& ~ ssSkP303("d2")
& ssSkP302("d1")
& ssSkP301("d0")
& ~ ssSkP304("d2")
& ssSkP302("d0")
& ssSkP301("d1")
& ~ ssSkP209("d1")
& ~ ssSkP208("d0")
& ~ ssSkP206("d2")
& ~ ssSkP209("d0")
& ~ ssSkP208("d1")
& ~ ssSkP207("d2")
& ~ ssSkP208("d2")
& ~ ssSkP207("d1")
& ~ ssSkP206("d0")
& ~ ssSkP209("d2")
& ~ ssSkP207("d0")
& ~ ssSkP206("d1")
& ~ ssSkP306("d2","d1")
& ~ ssSkP306("d1","d2")
& ~ ssSkP307("d2","d2")
& ssSkP307("d1","d1")
& ssSkP307("d0","d0")
& ~ ssSkP306("d2","d0")
& ~ ssSkP306("d0","d2")
& ssSkP307("d0","d1")
& ssSkP307("d1","d0")
& ssSkP306("d1","d0")
& ssSkP306("d0","d1")
& ssSkP307("d0","d2")
& ~ ssSkP307("d2","d0")
& ~ ssSkP306("d2","d2")
& ssSkP306("d1","d1")
& ssSkP306("d0","d0")
& ssSkP307("d1","d2")
& ~ ssSkP307("d2","d1")
& ssSkP212("d1")
& ~ ssSkP211("d0")
& ssSkP212("d0")
& ~ ssSkP210("d2")
& ~ ssSkP211("d1")
& ~ ssSkP210("d1")
& ~ ssSkP211("d2")
& ~ ssSkP212("d2")
& ~ ssSkP210("d0")
& ~ ssSkP213("d2")
& ~ ssSkP214("d2")
& ssSkP213("d0")
& ~ ssSkP214("d1")
& ssSkP213("d1")
& ssSkP214("d0")
& ssSkP219("d0")
& ~ ssSkP217("d2")
& ~ ssSkP218("d2")
& ssSkP219("d1")
& ssSkP218("d1")
& ~ ssSkP219("d2")
& ssSkP217("d0")
& ssSkP218("d0")
& ~ ssSkP217("d1")
& ssSkP223("d1")
& ssSkP222("d0")
& ~ ssSkP220("d2")
& ssSkP223("d0")
& ssSkP222("d1")
& ~ ssSkP221("d2")
& ~ ssSkP222("d2")
& ssSkP221("d1")
& ssSkP220("d0")
& ~ ssSkP223("d2")
& ssSkP221("d0")
& ssSkP220("d1")
& ssSkP227("d1")
& ssSkP226("d0")
& ~ ssSkP224("d2")
& ssSkP227("d0")
& ssSkP226("d1")
& ~ ssSkP225("d2")
& ~ ssSkP226("d2")
& ssSkP225("d1")
& ssSkP224("d0")
& ~ ssSkP227("d2")
& ssSkP225("d0")
& ssSkP224("d1")
& ~ ssSkP327("d2","d0")
& ~ ssSkP327("d0","d2")
& ssSkP328("d1","d2")
& ~ ssSkP328("d2","d1")
& ~ ssSkP327("d2","d1")
& ~ ssSkP327("d1","d2")
& ssSkP328("d0","d2")
& ~ ssSkP328("d2","d0")
& ~ ssSkP327("d2","d2")
& ssSkP327("d1","d1")
& ssSkP327("d0","d0")
& ssSkP328("d0","d1")
& ssSkP328("d1","d0")
& ssSkP327("d1","d0")
& ssSkP327("d0","d1")
& ~ ssSkP328("d2","d2")
& ssSkP328("d1","d1")
& ssSkP328("d0","d0")
& ~ ssSkP346("d2","d1")
& ~ ssSkP346("d1","d2")
& ~ ssSkP347("d2","d2")
& ssSkP347("d1","d1")
& ssSkP347("d0","d0")
& ~ ssSkP346("d2","d0")
& ~ ssSkP346("d0","d2")
& ssSkP347("d0","d1")
& ssSkP347("d1","d0")
& ssSkP346("d1","d0")
& ssSkP346("d0","d1")
& ssSkP347("d0","d2")
& ~ ssSkP347("d2","d0")
& ~ ssSkP346("d2","d2")
& ssSkP346("d1","d1")
& ssSkP346("d0","d0")
& ssSkP347("d1","d2")
& ~ ssSkP347("d2","d1")
& ssSkP1087("d1","d0")
& ssSkP1087("d0","d1")
& ~ ssSkP1088("d2","d2")
& ssSkP1088("d1","d1")
& ssSkP1088("d0","d0")
& ~ ssSkP201("d1")
& ~ ssSkP200("d0")
& ~ ssSkP1087("d2","d2")
& ssSkP1087("d1","d1")
& ssSkP1087("d0","d0")
& ssSkP1088("d0","d1")
& ssSkP1088("d1","d0")
& ~ ssSkP201("d0")
& ~ ssSkP200("d1")
& ~ ssSkP1087("d2","d1")
& ~ ssSkP1087("d1","d2")
& ssSkP1088("d0","d2")
& ~ ssSkP1088("d2","d0")
& ~ ssSkP200("d2")
& ~ ssSkP1087("d2","d0")
& ~ ssSkP1087("d0","d2")
& ssSkP1088("d1","d2")
& ~ ssSkP1088("d2","d1")
& ~ ssSkP201("d2")
& ~ ssSkP205("d1")
& ~ ssSkP204("d0")
& ~ ssSkP202("d2")
& ~ ssSkP205("d0")
& ~ ssSkP204("d1")
& ~ ssSkP203("d2")
& ~ ssSkP204("d2")
& ~ ssSkP203("d1")
& ~ ssSkP202("d0")
& ~ ssSkP205("d2")
& ~ ssSkP203("d0")
& ~ ssSkP202("d1")
& ~ ssSkP252("d1")
& ~ ssSkP251("d0")
& ~ ssSkP252("d0")
& ~ ssSkP251("d1")
& ~ ssSkP250("d2")
& ~ ssSkP251("d2")
& ~ ssSkP250("d1")
& ~ ssSkP252("d2")
& ~ ssSkP250("d0")
& ~ ssSkP256("d1")
& ~ ssSkP255("d0")
& ~ ssSkP253("d2")
& ~ ssSkP256("d0")
& ~ ssSkP255("d1")
& ~ ssSkP254("d2")
& ~ ssSkP255("d2")
& ~ ssSkP254("d1")
& ~ ssSkP253("d0")
& ~ ssSkP256("d2")
& ~ ssSkP254("d0")
& ~ ssSkP253("d1")
& ~ ssSkP259("d0")
& ~ ssSkP257("d2")
& ~ ssSkP259("d1")
& ~ ssSkP258("d2")
& ~ ssSkP259("d2")
& ~ ssSkP257("d0")
& ~ ssSkP258("d1")
& ssSkP257("d1")
& ~ ssSkP258("d0")
& ~ ssSkC4
& ~ ssSkC3
& ~ ssSkC6
& ~ ssSkC5
& ~ ssSkC8
& ~ ssSkC7
& ~ ssSkC9
& ~ ssSkC0
& ~ ssSkC2
& ~ ssSkP263("d1")
& ~ ssSkP262("d0")
& ~ ssSkP260("d2")
& ~ ssSkP263("d0")
& ~ ssSkP262("d1")
& ~ ssSkP261("d2")
& ~ ssSkP262("d2")
& ~ ssSkP261("d1")
& ~ ssSkP260("d0")
& ~ ssSkP263("d2")
& ~ ssSkP261("d0")
& ~ ssSkP260("d1")
& ~ ssSkP267("d1")
& ~ ssSkP266("d0")
& ~ ssSkP264("d2")
& ~ ssSkP267("d0")
& ~ ssSkP265("d2")
& ~ ssSkP266("d1")
& ssSkP265("d1")
& ~ ssSkP266("d2")
& ~ ssSkP264("d0")
& ~ ssSkP267("d2")
& ~ ssSkP265("d0")
& ~ ssSkP264("d1")
& ~ ssSkP268("d2")
& ~ ssSkP269("d2")
& ~ ssSkP269("d1")
& ~ ssSkP268("d0")
& ~ ssSkP269("d0")
& ~ ssSkP268("d1")
& ~ ssSkP228("d2")
& ~ ssSkP229("d2")
& ssSkP229("d1")
& ssSkP228("d0")
& ssSkP229("d0")
& ssSkP228("d1")
& ~ ssSkP1057("d2","d0")
& ~ ssSkP1057("d0","d2")
& ssSkP374("d0","d2")
& ~ ssSkP374("d2","d0")
& ssSkP1058("d0","d1")
& ssSkP1058("d1","d0")
& ssSkP230("d1")
& ~ ssSkP1057("d2","d1")
& ~ ssSkP1057("d1","d2")
& ssSkP374("d1","d2")
& ~ ssSkP374("d2","d1")
& ~ ssSkP1058("d2","d2")
& ssSkP1058("d1","d1")
& ssSkP1058("d0","d0")
& ssSkP230("d0")
& ~ ssSkP1057("d2","d2")
& ssSkP1057("d1","d1")
& ssSkP1057("d0","d0")
& ~ ssSkP374("d2","d2")
& ssSkP374("d1","d1")
& ssSkP374("d0","d0")
& ssSkP1058("d1","d2")
& ~ ssSkP1058("d2","d1")
& ssSkP1057("d1","d0")
& ssSkP1057("d0","d1")
& ssSkP374("d0","d1")
& ssSkP374("d1","d0")
& ssSkP1058("d0","d2")
& ~ ssSkP1058("d2","d0")
& ~ ssSkP230("d2")
& ssSkP373("d1","d0")
& ssSkP373("d0","d1")
& ssSkP234("d1")
& ssSkP233("d0")
& ~ ssSkP231("d2")
& ~ ssSkP373("d2","d2")
& ssSkP373("d1","d1")
& ssSkP373("d0","d0")
& ssSkP234("d0")
& ssSkP233("d1")
& ~ ssSkP232("d2")
& ~ ssSkP373("d2","d1")
& ~ ssSkP373("d1","d2")
& ~ ssSkP233("d2")
& ssSkP232("d1")
& ssSkP231("d0")
& ~ ssSkP373("d2","d0")
& ~ ssSkP373("d0","d2")
& ~ ssSkP234("d2")
& ssSkP232("d0")
& ssSkP231("d1")
& ssSkP237("d0")
& ssSkP238("d1")
& ~ ssSkP235("d2")
& ssSkP237("d1")
& ssSkP238("d0")
& ~ ssSkP236("d2")
& ~ ssSkP237("d2")
& ssSkP236("d1")
& ssSkP235("d0")
& ~ ssSkP238("d2")
& ~ ssSkP236("d0")
& ssSkP235("d1")
& ~ ssSkP239("d2")
& ssSkP239("d0")
& ssSkP239("d1")
& ssSkP241("d1")
& ssSkP240("d0")
& ssSkP241("d0")
& ssSkP240("d1")
& ~ ssSkP240("d2")
& ~ ssSkP241("d2")
& ~ ssSkP242("d2")
& ssSkP244("d0")
& ~ ssSkP243("d2")
& ~ ssSkP244("d1")
& ssSkP243("d1")
& ssSkP242("d0")
& ~ ssSkP244("d2")
& ssSkP243("d0")
& ssSkP242("d1")
& ~ ssSkP249("d1")
& ~ ssSkP248("d0")
& ~ ssSkP249("d0")
& ~ ssSkP248("d1")
& ~ ssSkP247("d2")
& ~ ssSkP248("d2")
& ~ ssSkP247("d1")
& ~ ssSkP249("d2")
& ~ ssSkP247("d0")
& ssSkP291("d0")
& ssSkP292("d1")
& ssSkP291("d1")
& ssSkP292("d0")
& ~ ssSkP290("d2")
& ~ ssSkP291("d2")
& ~ ssSkP290("d1")
& ~ ssSkP292("d2")
& ssSkP290("d0")
& ssSkP296("d1")
& ssSkP295("d0")
& ~ ssSkP293("d2")
& ssSkP296("d0")
& ssSkP295("d1")
& ~ ssSkP294("d2")
& ~ ssSkP295("d2")
& ssSkP294("d1")
& ssSkP293("d0")
& ~ ssSkP296("d2")
& ssSkP294("d0")
& ssSkP293("d1")
& ssSkP299("d0")
& ~ ssSkP297("d2")
& ssSkP299("d1")
& ~ ssSkP298("d2")
& ~ ssSkP299("d2")
& ssSkP298("d1")
& ssSkP297("d0")
& ssSkP298("d0")
& ssSkP297("d1")
& ~ ssSkP270("d1")
& ~ ssSkP270("d0")
& ~ ssSkP270("d2")
& ~ ssSkP273("d0")
& ~ ssSkP274("d1")
& ~ ssSkP271("d2")
& ~ ssSkP273("d1")
& ~ ssSkP272("d2")
& ~ ssSkP274("d0")
& ~ ssSkP273("d2")
& ~ ssSkP272("d1")
& ~ ssSkP271("d0")
& ~ ssSkP272("d0")
& ssSkP274("d2")
& ~ ssSkP271("d1")
& ssSkP278("d1")
& ssSkP277("d0")
& ssSkP278("d0")
& ssSkP277("d1")
& ~ ssSkP277("d2")
& ~ ssSkP278("d2")
& ~ ssSkP279("d2")
& ssSkP279("d0")
& ssSkP279("d1")
& ssSkP281("d1")
& ~ ssSkP280("d0")
& ssSkP281("d0")
& ssSkP280("d1")
& ~ ssSkP280("d2")
& ~ ssSkP281("d2")
& ssSkP285("d1")
& ssSkP284("d0")
& ~ ssSkP282("d2")
& ssSkP285("d0")
& ssSkP284("d1")
& ~ ssSkP283("d2")
& ~ ssSkP284("d2")
& ssSkP283("d1")
& ssSkP282("d0")
& ~ ssSkP285("d2")
& ssSkP283("d0")
& ssSkP282("d1")
& ssSkP289("d1")
& ssSkP288("d0")
& ~ ssSkP286("d2")
& ssSkP289("d0")
& ssSkP288("d1")
& ~ ssSkP287("d2")
& ~ ssSkP288("d2")
& ssSkP287("d1")
& ssSkP286("d0")
& ~ ssSkP289("d2")
& ssSkP287("d0")
& ssSkP286("d1")
& ssSkP0("d1","d0")
& ssSkP0("d0","d1")
& ~ ssSkP1("d2","d2")
& ssSkP1("d1","d1")
& ssSkP1("d0","d0")
& ~ ssSkP0("d2","d2")
& ssSkP0("d1","d1")
& ssSkP0("d0","d0")
& ssSkP1("d0","d1")
& ssSkP1("d1","d0")
& ~ ssSkP0("d2","d1")
& ~ ssSkP0("d1","d2")
& ssSkP1("d0","d2")
& ~ ssSkP1("d2","d0")
& ~ ssSkP0("d2","d0")
& ~ ssSkP0("d0","d2")
& ssSkP1("d1","d2")
& ~ ssSkP1("d2","d1")
& ~ ssSkC38
& ~ ssSkC35
& ~ ssSkC34
& ~ ssSkC37
& ~ ssSkC31
& ~ ssSkC33
& ~ ssSkC40
& ~ ssSkP428("d2","d2")
& ssSkP428("d1","d1")
& ssSkP428("d0","d0")
& ssSkP429("d0","d1")
& ssSkP429("d1","d0")
& ssSkP428("d1","d0")
& ssSkP428("d0","d1")
& ~ ssSkP429("d2","d2")
& ssSkP429("d1","d1")
& ssSkP429("d0","d0")
& ~ ssSkP428("d2","d0")
& ~ ssSkP428("d0","d2")
& ssSkP429("d1","d2")
& ~ ssSkP429("d2","d1")
& ~ ssSkP428("d2","d1")
& ~ ssSkP428("d1","d2")
& ssSkP429("d0","d2")
& ~ ssSkP429("d2","d0")
& ssSkP101("d0")
& ~ ssSkP100("d2")
& ~ ssSkP101("d1")
& ssSkP100("d1")
& ~ ssSkP101("d2")
& ssSkP100("d0")
& ~ ssSkP106("d1")
& ~ ssSkP105("d0")
& ~ ssSkP106("d0")
& ~ ssSkP105("d1")
& ~ ssSkP104("d2")
& ~ ssSkP105("d2")
& ~ ssSkP104("d1")
& ~ ssSkP106("d2")
& ~ ssSkP104("d0")
& ssSkP462("d0","d2")
& ~ ssSkP462("d2","d0")
& ssSkP462("d1","d2")
& ~ ssSkP462("d2","d1")
& ~ ssSkP462("d2","d2")
& ssSkP462("d1","d1")
& ssSkP462("d0","d0")
& ssSkP462("d0","d1")
& ssSkP462("d1","d0")
& ssSkP461("d1","d0")
& ssSkP461("d0","d1")
& ~ ssSkP461("d2","d2")
& ssSkP461("d1","d1")
& ssSkP461("d0","d0")
& ~ ssSkP461("d2","d1")
& ~ ssSkP461("d1","d2")
& ~ ssSkP461("d2","d0")
& ~ ssSkP461("d0","d2")
& ~ ssSkP129("d2")
& ~ ssSkP129("d0")
& ~ ssSkP129("d1")
& ~ ssSkC17
& ~ ssSkC16
& ~ ssSkC18
& ~ ssSkC13
& ~ ssSkC12
& ~ ssSkC15
& ~ ssSkC14
& ssSkP131("d1")
& ~ ssSkP130("d0")
& ~ ssSkP130("d1")
& ssSkP131("d0")
& ~ ssSkP130("d2")
& ~ ssSkC11
& ~ ssSkP131("d2")
& ~ ssSkC10
& ~ ssSkP132("d2")
& ssSkP135("d1")
& ~ ssSkP135("d0")
& ssSkP132("d0")
& ~ ssSkP132("d1")
& ~ ssSkP135("d2")
& ~ ssSkP138("d0")
& ~ ssSkP139("d1")
& ~ ssSkP136("d2")
& ~ ssSkP138("d1")
& ~ ssSkP139("d0")
& ~ ssSkP137("d2")
& ~ ssSkP138("d2")
& ~ ssSkP137("d1")
& ~ ssSkP136("d0")
& ~ ssSkP139("d2")
& ~ ssSkP137("d0")
& ~ ssSkP136("d1")
& ~ ssSkC27
& ~ ssSkC26
& ~ ssSkC20
& ~ ssSkP142("d1")
& ~ ssSkP141("d0")
& ~ ssSkP142("d0")
& ~ ssSkP140("d2")
& ~ ssSkP141("d1")
& ~ ssSkC22
& ssSkP140("d1")
& ~ ssSkP141("d2")
& ~ ssSkP142("d2")
& ~ ssSkP140("d0")
& ~ ssSkP146("d1")
& ~ ssSkP145("d0")
& ~ ssSkP143("d2")
& ~ ssSkP146("d0")
& ~ ssSkP145("d1")
& ~ ssSkP144("d2")
& ~ ssSkP145("d2")
& ~ ssSkP144("d1")
& ~ ssSkP143("d0")
& ~ ssSkP146("d2")
& ~ ssSkP144("d0")
& ~ ssSkP143("d1")
& ~ ssSkP149("d0")
& ~ ssSkP147("d2")
& ~ ssSkP149("d1")
& ~ ssSkP148("d2")
& ~ ssSkP149("d2")
& ~ ssSkP148("d1")
& ~ ssSkP147("d0")
& ~ ssSkP148("d0")
& ~ ssSkP147("d1")
& ~ ssSkP109("d0")
& ~ ssSkP107("d2")
& ~ ssSkP109("d1")
& ~ ssSkP108("d2")
& ~ ssSkP109("d2")
& ~ ssSkP108("d1")
& ~ ssSkP107("d0")
& ~ ssSkP108("d0")
& ~ ssSkP107("d1")
& ~ ssSkP492("d2","d1")
& ~ ssSkP492("d1","d2")
& ~ ssSkP493("d2","d2")
& ssSkP493("d1","d1")
& ssSkP493("d0","d0")
& ~ ssSkP113("d1")
& ~ ssSkP112("d0")
& ~ ssSkP110("d2")
& ~ ssSkP492("d2","d0")
& ~ ssSkP492("d0","d2")
& ssSkP493("d0","d1")
& ssSkP493("d1","d0")
& ~ ssSkP113("d0")
& ~ ssSkP112("d1")
& ~ ssSkP111("d2")
& ssSkP492("d1","d0")
& ssSkP492("d0","d1")
& ssSkP493("d0","d2")
& ~ ssSkP493("d2","d0")
& ~ ssSkP112("d2")
& ~ ssSkP111("d1")
& ~ ssSkP110("d0")
& ~ ssSkP492("d2","d2")
& ssSkP492("d1","d1")
& ssSkP492("d0","d0")
& ssSkP493("d1","d2")
& ~ ssSkP493("d2","d1")
& ~ ssSkP113("d2")
& ~ ssSkP111("d0")
& ~ ssSkP110("d1")
& ~ ssSkP117("d1")
& ~ ssSkP116("d0")
& ~ ssSkP114("d2")
& ~ ssSkP117("d0")
& ~ ssSkP116("d1")
& ~ ssSkP115("d2")
& ~ ssSkP116("d2")
& ~ ssSkP115("d1")
& ~ ssSkP114("d0")
& ~ ssSkP117("d2")
& ~ ssSkP115("d0")
& ~ ssSkP114("d1")
& ~ ssSkP118("d2")
& ~ ssSkP119("d2")
& ~ ssSkP119("d1")
& ~ ssSkP118("d0")
& ~ ssSkP119("d0")
& ~ ssSkP118("d1")
& ~ ssSkP120("d1")
& ~ ssSkP120("d0")
& ~ ssSkP120("d2")
& ~ ssSkP124("d1")
& ~ ssSkP123("d0")
& ~ ssSkP121("d2")
& ~ ssSkP124("d0")
& ~ ssSkP123("d1")
& ~ ssSkP122("d2")
& ~ ssSkP123("d2")
& ~ ssSkP122("d1")
& ~ ssSkP121("d0")
& ~ ssSkP124("d2")
& ~ ssSkP122("d0")
& ~ ssSkP121("d1")
& ~ ssSkP128("d1")
& ~ ssSkP127("d0")
& ~ ssSkP125("d2")
& ~ ssSkP128("d0")
& ~ ssSkP126("d2")
& ~ ssSkP127("d1")
& ssSkP126("d1")
& ~ ssSkP127("d2")
& ~ ssSkP125("d0")
& ~ ssSkP128("d2")
& ~ ssSkP126("d0")
& ~ ssSkP125("d1")
& ssSkP171("d1")
& ssSkP170("d0")
& ssSkP171("d0")
& ssSkP170("d1")
& ~ ssSkP170("d2")
& ~ ssSkP171("d2")
& ssSkP175("d1")
& ssSkP174("d0")
& ~ ssSkP172("d2")
& ssSkP175("d0")
& ssSkP174("d1")
& ~ ssSkP173("d2")
& ~ ssSkP174("d2")
& ssSkP173("d1")
& ssSkP172("d0")
& ~ ssSkP175("d2")
& ssSkP173("d0")
& ssSkP172("d1")
& ssSkP179("d1")
& ssSkP178("d0")
& ~ ssSkP176("d2")
& ssSkP179("d0")
& ssSkP178("d1")
& ~ ssSkP177("d2")
& ~ ssSkP178("d2")
& ssSkP177("d1")
& ssSkP176("d0")
& ~ ssSkP179("d2")
& ssSkP177("d0")
& ssSkP176("d1")
& ssSkP182("d1")
& ssSkP181("d0")
& ssSkP182("d0")
& ssSkP181("d1")
& ~ ssSkP180("d2")
& ~ ssSkP181("d2")
& ssSkP180("d1")
& ~ ssSkP182("d2")
& ssSkP180("d0")
& ssSkP185("d0")
& ~ ssSkP186("d1")
& ~ ssSkP183("d2")
& ~ ssSkP184("d2")
& ssSkP185("d1")
& ssSkP186("d0")
& ~ ssSkP185("d2")
& ~ ssSkP184("d1")
& ssSkP183("d0")
& ssSkP184("d0")
& ~ ssSkP186("d2")
& ssSkP183("d1")
& ~ ssSkP189("d0")
& ~ ssSkP189("d1")
& ~ ssSkP189("d2")
& ~ ssSkP153("d1")
& ~ ssSkP152("d0")
& ~ ssSkP150("d2")
& ~ ssSkP153("d0")
& ~ ssSkP152("d1")
& ~ ssSkP151("d2")
& ~ ssSkP152("d2")
& ~ ssSkP151("d1")
& ~ ssSkP150("d0")
& ~ ssSkP153("d2")
& ~ ssSkP151("d0")
& ~ ssSkP150("d1")
& ~ ssSkP154("d2")
& ~ ssSkP155("d2")
& ssSkP154("d0")
& ~ ssSkP155("d1")
& ssSkP154("d1")
& ssSkP155("d0")
& ~ ssSkP158("d2")
& ~ ssSkP159("d2")
& ssSkP159("d1")
& ssSkP158("d0")
& ssSkP159("d0")
& ssSkP158("d1")
& ssSkP160("d1")
& ssSkP160("d0")
& ~ ssSkP160("d2")
& ssSkP163("d0")
& ssSkP164("d1")
& ~ ssSkP161("d2")
& ssSkP163("d1")
& ssSkP164("d0")
& ~ ssSkP162("d2")
& ~ ssSkP163("d2")
& ssSkP162("d1")
& ssSkP161("d0")
& ~ ssSkP164("d2")
& ~ ssSkP162("d0")
& ssSkP161("d1")
& ssSkP168("d1")
& ssSkP167("d0")
& ~ ssSkP165("d2")
& ssSkP168("d0")
& ssSkP167("d1")
& ~ ssSkP166("d2")
& ~ ssSkP167("d2")
& ssSkP166("d1")
& ssSkP165("d0")
& ~ ssSkP168("d2")
& ssSkP166("d0")
& ssSkP165("d1")
& ~ ssSkP169("d2")
& ssSkP169("d0")
& ssSkP169("d1")
& ~ ssSkP193("d1")
& ~ ssSkP192("d0")
& ~ ssSkP190("d2")
& ~ ssSkP193("d0")
& ~ ssSkP192("d1")
& ~ ssSkP191("d2")
& ~ ssSkP192("d2")
& ~ ssSkP191("d1")
& ~ ssSkP190("d0")
& ~ ssSkP193("d2")
& ~ ssSkP191("d0")
& ~ ssSkP190("d1")
& ~ ssSkP197("d1")
& ~ ssSkP196("d0")
& ~ ssSkP194("d2")
& ~ ssSkP197("d0")
& ~ ssSkP196("d1")
& ~ ssSkP195("d2")
& ~ ssSkP196("d2")
& ~ ssSkP195("d1")
& ~ ssSkP194("d0")
& ~ ssSkP197("d2")
& ~ ssSkP195("d0")
& ~ ssSkP194("d1")
& ~ ssSkP198("d2")
& ~ ssSkP199("d2")
& ssSkP199("d1")
& ~ ssSkP198("d0")
& ~ ssSkP199("d0")
& ~ ssSkP198("d1")
& ~ ssSkP9("d0")
& ~ ssSkP8("d1")
& ~ ssSkP9("d1")
& ~ ssSkP8("d0")
& ~ ssSkP9("d2")
& ~ ssSkP8("d2")
& ~ ssSkP502("d1")
& ~ ssSkP501("d0")
& ~ ssSkP502("d0")
& ~ ssSkP501("d1")
& ~ ssSkP500("d2")
& ~ ssSkP501("d2")
& ~ ssSkP500("d1")
& ~ ssSkP502("d2")
& ~ ssSkP500("d0")
& ~ ssSkP7("d2")
& ~ ssSkP5("d0")
& ~ ssSkP4("d1")
& ~ ssSkP6("d2")
& ~ ssSkP5("d1")
& ~ ssSkP4("d0")
& ~ ssSkP7("d0")
& ~ ssSkP6("d1")
& ~ ssSkP5("d2")
& ~ ssSkP7("d1")
& ~ ssSkP6("d0")
& ~ ssSkP4("d2")
& ~ ssSkP3("d2")
& ~ ssSkP2("d2")
& ~ ssSkP3("d0")
& ~ ssSkP2("d1")
& ~ ssSkP3("d1")
& ~ ssSkP2("d0")
& ~ ssSkP506("d1")
& ~ ssSkP505("d0")
& ~ ssSkP503("d2")
& ~ ssSkP506("d0")
& ~ ssSkP505("d1")
& ~ ssSkP504("d2")
& ~ ssSkP505("d2")
& ~ ssSkP504("d1")
& ~ ssSkP503("d0")
& ~ ssSkP506("d2")
& ~ ssSkP504("d0")
& ~ ssSkP503("d1")
& ~ ssSkP509("d0")
& ~ ssSkP507("d2")
& ~ ssSkP509("d1")
& ~ ssSkP508("d2")
& ~ ssSkP509("d2")
& ~ ssSkP508("d1")
& ~ ssSkP507("d0")
& ~ ssSkP508("d0")
& ~ ssSkP507("d1")
& ~ ssSkP513("d1")
& ~ ssSkP512("d0")
& ~ ssSkP510("d2")
& ~ ssSkP513("d0")
& ~ ssSkP512("d1")
& ~ ssSkP511("d2")
& ~ ssSkP512("d2")
& ~ ssSkP511("d1")
& ~ ssSkP510("d0")
& ~ ssSkP513("d2")
& ~ ssSkP511("d0")
& ~ ssSkP510("d1")
& ~ ssSkP517("d1")
& ~ ssSkP516("d0")
& ~ ssSkP514("d2")
& ssSkP517("d0")
& ~ ssSkP516("d1")
& ~ ssSkP515("d2")
& ~ ssSkP516("d2")
& ~ ssSkP515("d1")
& ~ ssSkP514("d0")
& ~ ssSkP517("d2")
& ~ ssSkP515("d0")
& ~ ssSkP514("d1")
& ~ ssSkP518("d2")
& ~ ssSkP519("d2")
& ~ ssSkP519("d1")
& ~ ssSkP518("d0")
& ~ ssSkP519("d0")
& ~ ssSkP518("d1")
& ssSkP520("d1")
& ssSkP520("d0")
& ~ ssSkP520("d2")
& ssSkP523("d0")
& ~ ssSkP524("d1")
& ~ ssSkP521("d2")
& ssSkP523("d1")
& ssSkP524("d0")
& ~ ssSkP522("d2")
& ~ ssSkP523("d2")
& ssSkP522("d1")
& ssSkP521("d0")
& ~ ssSkP524("d2")
& ssSkP522("d0")
& ssSkP521("d1")
& ~ ssSkP448("d2")
& ~ ssSkP449("d2")
& ssSkP449("d1")
& ssSkP448("d0")
& ssSkP449("d0")
& ssSkP448("d1")
& ssSkP450("d1")
& ~ ssSkP450("d0")
& ~ ssSkP450("d2")
& ssSkP454("d1")
& ssSkP453("d0")
& ~ ssSkP451("d2")
& ssSkP454("d0")
& ssSkP453("d1")
& ~ ssSkP452("d2")
& ~ ssSkP453("d2")
& ssSkP451("d0")
& ssSkP452("d1")
& ~ ssSkP454("d2")
& ssSkP451("d1")
& ssSkP452("d0")
& ssSkP458("d1")
& ssSkP457("d0")
& ~ ssSkP455("d2")
& ssSkP458("d0")
& ~ ssSkP456("d2")
& ssSkP457("d1")
& ssSkP456("d1")
& ~ ssSkP457("d2")
& ssSkP455("d0")
& ~ ssSkP458("d2")
& ssSkP456("d0")
& ssSkP455("d1")
& ~ ssSkP459("d2")
& ssSkP459("d0")
& ssSkP459("d1")
& ssSkP460("d0")
& ~ ssSkP460("d1")
& ~ ssSkP460("d2")
& ssSkP465("d1")
& ssSkP464("d0")
& ssSkP465("d0")
& ssSkP464("d1")
& ~ ssSkP463("d2")
& ~ ssSkP464("d2")
& ssSkP463("d1")
& ~ ssSkP465("d2")
& ssSkP463("d0")
& ssSkP469("d1")
& ssSkP468("d0")
& ~ ssSkP466("d2")
& ssSkP469("d0")
& ssSkP468("d1")
& ~ ssSkP467("d2")
& ~ ssSkP468("d2")
& ssSkP467("d1")
& ssSkP466("d0")
& ~ ssSkP469("d2")
& ssSkP467("d0")
& ssSkP466("d1")
& ~ ssSkP426("d2")
& ~ ssSkP427("d2")
& ssSkP426("d0")
& ~ ssSkP427("d1")
& ssSkP426("d1")
& ssSkP427("d0")
& ssSkP432("d1")
& ssSkP431("d0")
& ssSkP432("d0")
& ssSkP431("d1")
& ~ ssSkP430("d2")
& ~ ssSkP431("d2")
& ssSkP430("d1")
& ~ ssSkP432("d2")
& ssSkP430("d0")
& ssSkP436("d1")
& ssSkP435("d0")
& ~ ssSkP433("d2")
& ssSkP436("d0")
& ssSkP435("d1")
& ~ ssSkP434("d2")
& ~ ssSkP435("d2")
& ssSkP434("d1")
& ssSkP433("d0")
& ~ ssSkP436("d2")
& ssSkP434("d0")
& ssSkP433("d1")
& ssSkP439("d0")
& ~ ssSkP437("d2")
& ssSkP439("d1")
& ~ ssSkP438("d2")
& ~ ssSkP439("d2")
& ssSkP438("d1")
& ssSkP437("d0")
& ssSkP438("d0")
& ssSkP437("d1")
& ssSkP103("d0","d2")
& ~ ssSkP103("d2","d0")
& ssSkP103("d1","d2")
& ~ ssSkP103("d2","d1")
& ~ ssSkP103("d2","d2")
& ssSkP103("d1","d1")
& ssSkP103("d0","d0")
& ssSkP103("d0","d1")
& ssSkP103("d1","d0")
& ssSkP102("d1","d0")
& ssSkP102("d0","d1")
& ~ ssSkP102("d2","d2")
& ssSkP102("d1","d1")
& ssSkP102("d0","d0")
& ~ ssSkP102("d2","d1")
& ~ ssSkP102("d1","d2")
& ~ ssSkP102("d2","d0")
& ~ ssSkP102("d0","d2")
& ssSkP443("d1")
& ssSkP442("d0")
& ~ ssSkP440("d2")
& ssSkP443("d0")
& ssSkP442("d1")
& ~ ssSkP441("d2")
& ~ ssSkP442("d2")
& ssSkP441("d1")
& ssSkP440("d0")
& ~ ssSkP443("d2")
& ssSkP441("d0")
& ssSkP440("d1")
& ssSkP447("d1")
& ssSkP446("d0")
& ~ ssSkP444("d2")
& ssSkP447("d0")
& ~ ssSkP445("d2")
& ssSkP446("d1")
& ssSkP445("d1")
& ~ ssSkP446("d2")
& ~ ssSkP444("d0")
& ~ ssSkP447("d2")
& ssSkP445("d0")
& ssSkP444("d1")
& ssSkP490("d1")
& ssSkP490("d0")
& ~ ssSkP490("d2")
& ~ ssSkP491("d2")
& ~ ssSkP494("d1")
& ~ ssSkP494("d0")
& ssSkP491("d0")
& ~ ssSkP491("d1")
& ~ ssSkP494("d2")
& ssSkP498("d1")
& ~ ssSkP497("d0")
& ~ ssSkP495("d2")
& ~ ssSkP498("d0")
& ~ ssSkP497("d1")
& ~ ssSkP496("d2")
& ~ ssSkP497("d2")
& ~ ssSkP496("d1")
& ~ ssSkP495("d0")
& ~ ssSkP498("d2")
& ~ ssSkP496("d0")
& ~ ssSkP495("d1")
& ~ ssSkP499("d2")
& ~ ssSkP499("d0")
& ~ ssSkP499("d1")
& ~ ssSkP133("d2","d1")
& ~ ssSkP133("d1","d2")
& ~ ssSkP134("d2","d2")
& ssSkP134("d1","d1")
& ssSkP134("d0","d0")
& ssSkP472("d1")
& ssSkP471("d0")
& ~ ssSkP133("d2","d0")
& ~ ssSkP133("d0","d2")
& ssSkP134("d0","d1")
& ssSkP134("d1","d0")
& ssSkP472("d0")
& ssSkP471("d1")
& ~ ssSkP470("d2")
& ssSkP133("d1","d0")
& ssSkP133("d0","d1")
& ssSkP134("d0","d2")
& ~ ssSkP134("d2","d0")
& ~ ssSkP471("d2")
& ssSkP470("d1")
& ~ ssSkP133("d2","d2")
& ssSkP133("d1","d1")
& ssSkP133("d0","d0")
& ssSkP134("d1","d2")
& ~ ssSkP134("d2","d1")
& ~ ssSkP472("d2")
& ssSkP470("d0")
& ssSkP476("d1")
& ssSkP475("d0")
& ~ ssSkP473("d2")
& ssSkP476("d0")
& ~ ssSkP474("d2")
& ssSkP475("d1")
& ssSkP474("d1")
& ~ ssSkP475("d2")
& ssSkP473("d0")
& ~ ssSkP476("d2")
& ssSkP474("d0")
& ssSkP473("d1")
& ssSkP479("d0")
& ~ ssSkP477("d2")
& ssSkP479("d1")
& ~ ssSkP478("d2")
& ~ ssSkP479("d2")
& ssSkP478("d1")
& ssSkP477("d0")
& ssSkP478("d0")
& ssSkP477("d1")
& ssSkP482("d0")
& ssSkP483("d1")
& ~ ssSkP480("d2")
& ssSkP482("d1")
& ssSkP483("d0")
& ~ ssSkP481("d2")
& ~ ssSkP482("d2")
& ssSkP481("d1")
& ssSkP480("d0")
& ~ ssSkP483("d2")
& ~ ssSkP481("d0")
& ssSkP480("d1")
& ssSkP487("d1")
& ssSkP486("d0")
& ~ ssSkP484("d2")
& ssSkP487("d0")
& ssSkP486("d1")
& ~ ssSkP485("d2")
& ~ ssSkP486("d2")
& ssSkP485("d1")
& ssSkP484("d0")
& ~ ssSkP487("d2")
& ssSkP485("d0")
& ssSkP484("d1")
& ~ ssSkP488("d2")
& ~ ssSkP489("d2")
& ssSkP489("d1")
& ssSkP488("d0")
& ssSkP489("d0")
& ssSkP488("d1")
& ~ ssSkP156("d2","d2")
& ssSkP156("d1","d1")
& ssSkP156("d0","d0")
& ssSkP157("d0","d1")
& ssSkP157("d1","d0")
& ssSkP156("d1","d0")
& ssSkP156("d0","d1")
& ~ ssSkP157("d2","d2")
& ssSkP157("d1","d1")
& ssSkP157("d0","d0")
& ~ ssSkP156("d2","d0")
& ~ ssSkP156("d0","d2")
& ssSkP157("d1","d2")
& ~ ssSkP157("d2","d1")
& ~ ssSkP156("d2","d1")
& ~ ssSkP156("d1","d2")
& ssSkP157("d0","d2")
& ~ ssSkP157("d2","d0")
& ~ ssSkP187("d2","d0")
& ~ ssSkP187("d0","d2")
& ssSkP188("d1","d2")
& ~ ssSkP188("d2","d1")
& ~ ssSkP187("d2","d1")
& ~ ssSkP187("d1","d2")
& ssSkP188("d0","d2")
& ~ ssSkP188("d2","d0")
& ~ ssSkP187("d2","d2")
& ssSkP187("d1","d1")
& ssSkP187("d0","d0")
& ssSkP188("d0","d1")
& ssSkP188("d1","d0")
& ssSkP187("d1","d0")
& ssSkP187("d0","d1")
& ~ ssSkP188("d2","d2")
& ssSkP188("d1","d1")
& ssSkP188("d0","d0")
& ~ ssSkP407("d1")
& ~ ssSkP406("d0")
& ~ ssSkP404("d2")
& ~ ssSkP407("d0")
& ~ ssSkP406("d1")
& ~ ssSkP405("d2")
& ~ ssSkP406("d2")
& ~ ssSkP405("d1")
& ~ ssSkP404("d0")
& ~ ssSkP407("d2")
& ~ ssSkP405("d0")
& ~ ssSkP404("d1")
& ~ ssSkP408("d2")
& ~ ssSkP409("d2")
& ~ ssSkP409("d1")
& ~ ssSkP408("d0")
& ~ ssSkP409("d0")
& ~ ssSkP408("d1")
& ~ ssSkP410("d1")
& ~ ssSkP410("d0")
& ~ ssSkP410("d2")
& ~ ssSkP414("d1")
& ~ ssSkP413("d0")
& ~ ssSkP411("d2")
& ~ ssSkP414("d0")
& ~ ssSkP413("d1")
& ~ ssSkP412("d2")
& ~ ssSkP413("d2")
& ~ ssSkP412("d1")
& ~ ssSkP411("d0")
& ~ ssSkP414("d2")
& ~ ssSkP412("d0")
& ~ ssSkP411("d1")
& ssSkP418("d1")
& ssSkP417("d0")
& ~ ssSkP415("d2")
& ssSkP418("d0")
& ~ ssSkP416("d2")
& ssSkP417("d1")
& ssSkP416("d1")
& ~ ssSkP417("d2")
& ~ ssSkP415("d0")
& ~ ssSkP418("d2")
& ssSkP416("d0")
& ~ ssSkP415("d1")
& ~ ssSkP419("d2")
& ssSkP419("d0")
& ~ ssSkP419("d1")
& ssSkP420("d0")
& ssSkP421("d1")
& ssSkP420("d1")
& ssSkP421("d0")
& ~ ssSkP420("d2")
& ~ ssSkP421("d2")
& ssSkP425("d1")
& ssSkP424("d0")
& ~ ssSkP422("d2")
& ssSkP425("d0")
& ~ ssSkP423("d2")
& ssSkP424("d1")
& ssSkP423("d1")
& ~ ssSkP424("d2")
& ssSkP422("d0")
& ~ ssSkP425("d2")
& ssSkP423("d0")
& ssSkP422("d1")
& ~ ssSkP403("d1")
& ~ ssSkP402("d0")
& ~ ssSkP403("d0")
& ~ ssSkP402("d1")
& ~ ssSkP402("d2")
& ~ ssSkP403("d2")
& ~ ssSkP329("d0")
& ~ ssSkP329("d1")
& ~ ssSkP329("d2")
& ssSkP1091("d0")
& ssSkP1090("d1")
& ssSkP1091("d1")
& ssSkP1090("d0")
& ~ ssSkP1091("d2")
& ~ ssSkP1090("d2")
& ssSkP1094("d1")
& ssSkP1095("d0")
& ~ ssSkP1093("d2")
& ssSkP1094("d0")
& ssSkP1095("d1")
& ~ ssSkP1092("d2")
& ~ ssSkP1095("d2")
& ssSkP1093("d0")
& ssSkP1092("d1")
& ~ ssSkP1094("d2")
& ~ ssSkP1093("d1")
& ssSkP1092("d0")
& ssSkP1098("d1")
& ssSkP1099("d0")
& ~ ssSkP1097("d2")
& ssSkP1098("d0")
& ssSkP1099("d1")
& ~ ssSkP1096("d2")
& ~ ssSkP1099("d2")
& ssSkP1097("d0")
& ssSkP1096("d1")
& ~ ssSkP1098("d2")
& ssSkP1097("d1")
& ssSkP1096("d0")
& ~ ssSkP333("d1")
& ~ ssSkP332("d0")
& ~ ssSkP330("d2")
& ~ ssSkP333("d0")
& ~ ssSkP332("d1")
& ~ ssSkP331("d2")
& ~ ssSkP332("d2")
& ~ ssSkP330("d0")
& ~ ssSkP331("d1")
& ~ ssSkP333("d2")
& ~ ssSkP330("d1")
& ~ ssSkP331("d0")
& ~ ssSkP337("d1")
& ~ ssSkP336("d0")
& ~ ssSkP334("d2")
& ~ ssSkP337("d0")
& ~ ssSkP336("d1")
& ~ ssSkP335("d2")
& ~ ssSkP336("d2")
& ~ ssSkP335("d1")
& ~ ssSkP334("d0")
& ~ ssSkP337("d2")
& ~ ssSkP335("d0")
& ~ ssSkP334("d1")
& ~ ssSkP338("d2")
& ~ ssSkP339("d2")
& ~ ssSkP339("d1")
& ~ ssSkP338("d0")
& ~ ssSkP339("d0")
& ~ ssSkP338("d1")
& ssSkP1080("d0")
& ssSkP1080("d1")
& ~ ssSkP1080("d2")
& ssSkP1084("d0")
& ssSkP1083("d1")
& ~ ssSkP1082("d2")
& ssSkP1084("d1")
& ssSkP1083("d0")
& ~ ssSkP1081("d2")
& ~ ssSkP1084("d2")
& ssSkP1082("d0")
& ssSkP1081("d1")
& ~ ssSkP1083("d2")
& ssSkP1082("d1")
& ssSkP1081("d0")
& ~ ssSkP1086("d2")
& ~ ssSkP340("d1")
& ~ ssSkP1085("d2")
& ~ ssSkP340("d0")
& ssSkP1085("d1")
& ssSkP1086("d0")
& ssSkP1085("d0")
& ~ ssSkP1086("d1")
& ~ ssSkP340("d2")
& ssSkP344("d1")
& ssSkP343("d0")
& ~ ssSkP341("d2")
& ssSkP344("d0")
& ~ ssSkP1089("d2")
& ~ ssSkP342("d2")
& ssSkP343("d1")
& ssSkP1089("d1")
& ssSkP342("d1")
& ~ ssSkP343("d2")
& ~ ssSkP341("d0")
& ~ ssSkP344("d2")
& ssSkP1089("d0")
& ssSkP342("d0")
& ~ ssSkP341("d1")
& ~ ssSkP345("d2")
& ~ ssSkP348("d1")
& ~ ssSkP348("d0")
& ssSkP345("d0")
& ~ ssSkP345("d1")
& ~ ssSkP348("d2")
& ~ ssSkP305("d2")
& ~ ssSkP308("d1")
& ~ ssSkP308("d0")
& ssSkP305("d0")
& ~ ssSkP305("d1")
& ~ ssSkP308("d2")
& ~ ssSkP309("d2")
& ~ ssSkP309("d0")
& ~ ssSkP309("d1")
& ~ ssSkP215("d2","d2")
& ssSkP215("d1","d1")
& ssSkP215("d0","d0")
& ssSkP216("d0","d1")
& ssSkP216("d1","d0")
& ssSkP1072("d1")
& ssSkP1073("d0")
& ~ ssSkP1071("d2")
& ssSkP215("d1","d0")
& ssSkP215("d0","d1")
& ~ ssSkP216("d2","d2")
& ssSkP216("d1","d1")
& ssSkP216("d0","d0")
& ssSkP1072("d0")
& ssSkP1073("d1")
& ~ ssSkP1070("d2")
& ~ ssSkP215("d2","d0")
& ~ ssSkP215("d0","d2")
& ssSkP216("d1","d2")
& ~ ssSkP216("d2","d1")
& ~ ssSkP1073("d2")
& ssSkP1071("d0")
& ssSkP1070("d1")
& ~ ssSkP215("d2","d1")
& ~ ssSkP215("d1","d2")
& ssSkP216("d0","d2")
& ~ ssSkP216("d2","d0")
& ~ ssSkP1072("d2")
& ~ ssSkP1071("d1")
& ssSkP1070("d0")
& ssSkP1077("d0")
& ssSkP1076("d1")
& ~ ssSkP1075("d2")
& ssSkP1077("d1")
& ssSkP1076("d0")
& ~ ssSkP1074("d2")
& ~ ssSkP1077("d2")
& ssSkP1075("d0")
& ssSkP1074("d1")
& ~ ssSkP1076("d2")
& ssSkP1075("d1")
& ssSkP1074("d0")
& ~ ssSkP1079("d2")
& ~ ssSkP311("d1")
& ~ ssSkP310("d0")
& ~ ssSkP1078("d2")
& ~ ssSkP311("d0")
& ~ ssSkP310("d1")
& ssSkP1079("d0")
& ssSkP1078("d1")
& ~ ssSkP310("d2")
& ssSkP1079("d1")
& ssSkP1078("d0")
& ~ ssSkP311("d2")
& ssSkP314("d0")
& ssSkP315("d1")
& ~ ssSkP312("d2")
& ssSkP314("d1")
& ssSkP315("d0")
& ~ ssSkP313("d2")
& ~ ssSkP314("d2")
& ~ ssSkP313("d1")
& ~ ssSkP312("d0")
& ~ ssSkP315("d2")
& ~ ssSkP313("d0")
& ~ ssSkP312("d1")
& ssSkP319("d1")
& ssSkP318("d0")
& ~ ssSkP316("d2")
& ssSkP319("d0")
& ~ ssSkP318("d1")
& ~ ssSkP317("d2")
& ~ ssSkP318("d2")
& ssSkP317("d1")
& ssSkP316("d0")
& ~ ssSkP319("d2")
& ssSkP317("d0")
& ssSkP316("d1")
& ssSkP1062("d0")
& ~ ssSkP1061("d1")
& ~ ssSkP1060("d2")
& ~ ssSkP1062("d1")
& ~ ssSkP1061("d0")
& ~ ssSkP1062("d2")
& ~ ssSkP1060("d0")
& ~ ssSkP1061("d2")
& ~ ssSkP1060("d1")
& ssSkP1065("d1")
& ssSkP1066("d0")
& ~ ssSkP1064("d2")
& ssSkP1065("d0")
& ssSkP1066("d1")
& ~ ssSkP1063("d2")
& ~ ssSkP1066("d2")
& ~ ssSkP1064("d0")
& ~ ssSkP1063("d1")
& ~ ssSkP1065("d2")
& ~ ssSkP1064("d1")
& ~ ssSkP1063("d0")
& ssSkP1069("d1")
& ~ ssSkP1068("d2")
& ssSkP322("d1")
& ssSkP321("d0")
& ssSkP1069("d0")
& ~ ssSkP1067("d2")
& ssSkP322("d0")
& ssSkP321("d1")
& ~ ssSkP320("d2")
& ssSkP1068("d0")
& ssSkP1067("d1")
& ~ ssSkP321("d2")
& ssSkP320("d1")
& ~ ssSkP1069("d2")
& ssSkP1068("d1")
& ssSkP1067("d0")
& ~ ssSkP322("d2")
& ssSkP320("d0")
& ssSkP325("d0")
& ~ ssSkP326("d1")
& ~ ssSkP323("d2")
& ssSkP325("d1")
& ssSkP326("d0")
& ~ ssSkP324("d2")
& ~ ssSkP325("d2")
& ssSkP323("d0")
& ssSkP324("d1")
& ~ ssSkP326("d2")
& ssSkP323("d1")
& ssSkP324("d0")
& ssSkP372("d0")
& ~ ssSkP370("d2")
& ~ ssSkP371("d2")
& ~ ssSkP372("d1")
& ssSkP371("d1")
& ~ ssSkP372("d2")
& ssSkP370("d0")
& ssSkP371("d0")
& ssSkP370("d1")
& ~ ssSkP1059("d0")
& ~ ssSkP377("d1")
& ~ ssSkP376("d0")
& ~ ssSkP1059("d1")
& ~ ssSkP377("d0")
& ~ ssSkP376("d1")
& ~ ssSkP375("d2")
& ~ ssSkP1059("d2")
& ~ ssSkP376("d2")
& ~ ssSkP375("d1")
& ~ ssSkP377("d2")
& ~ ssSkP375("d0")
& ~ ssSkP378("d2")
& ~ ssSkP379("d2")
& ~ ssSkP379("d1")
& ~ ssSkP378("d0")
& ~ ssSkP379("d0")
& ~ ssSkP378("d1")
& ~ ssSkP246("d0","d2")
& ~ ssSkP246("d2","d0")
& ~ ssSkP380("d1")
& ~ ssSkP246("d1","d2")
& ~ ssSkP246("d2","d1")
& ~ ssSkP380("d0")
& ~ ssSkP246("d2","d2")
& ssSkP246("d1","d1")
& ssSkP246("d0","d0")
& ssSkP246("d0","d1")
& ssSkP246("d1","d0")
& ~ ssSkP380("d2")
& ssSkP245("d1","d0")
& ssSkP245("d0","d1")
& ~ ssSkP383("d0")
& ~ ssSkP384("d1")
& ~ ssSkP381("d2")
& ~ ssSkP245("d2","d2")
& ssSkP245("d1","d1")
& ssSkP245("d0","d0")
& ~ ssSkP384("d0")
& ~ ssSkP382("d2")
& ~ ssSkP383("d1")
& ~ ssSkP245("d2","d1")
& ~ ssSkP245("d1","d2")
& ~ ssSkP383("d2")
& ~ ssSkP382("d1")
& ~ ssSkP381("d0")
& ~ ssSkP245("d2","d0")
& ~ ssSkP245("d0","d2")
& ~ ssSkP384("d2")
& ~ ssSkP382("d0")
& ~ ssSkP381("d1")
& ~ ssSkP388("d1")
& ~ ssSkP387("d0")
& ~ ssSkP385("d2")
& ~ ssSkP388("d0")
& ~ ssSkP387("d1")
& ~ ssSkP386("d2")
& ~ ssSkP387("d2")
& ~ ssSkP386("d1")
& ~ ssSkP385("d0")
& ~ ssSkP388("d2")
& ~ ssSkP386("d0")
& ~ ssSkP385("d1")
& ~ ssSkP389("d2")
& ~ ssSkP389("d0")
& ~ ssSkP389("d1")
& ~ ssSkP349("d2")
& ~ ssSkP349("d0")
& ~ ssSkP349("d1")
& ~ ssSkP351("d1")
& ~ ssSkP350("d0")
& ~ ssSkP351("d0")
& ~ ssSkP350("d1")
& ~ ssSkP350("d2")
& ~ ssSkP351("d2")
& ~ ssSkP355("d1")
& ~ ssSkP354("d0")
& ~ ssSkP352("d2")
& ~ ssSkP355("d0")
& ~ ssSkP354("d1")
& ~ ssSkP353("d2")
& ~ ssSkP354("d2")
& ~ ssSkP352("d0")
& ~ ssSkP353("d1")
& ~ ssSkP355("d2")
& ~ ssSkP352("d1")
& ~ ssSkP353("d0")
& ~ ssSkP359("d1")
& ~ ssSkP358("d0")
& ~ ssSkP356("d2")
& ~ ssSkP359("d0")
& ~ ssSkP358("d1")
& ~ ssSkP357("d2")
& ~ ssSkP358("d2")
& ~ ssSkP357("d1")
& ~ ssSkP356("d0")
& ~ ssSkP359("d2")
& ~ ssSkP357("d0")
& ~ ssSkP356("d1")
& ssSkP1022("d0")
& ssSkP1021("d1")
& ~ ssSkP1020("d2")
& ~ ssSkP362("d1")
& ~ ssSkP361("d0")
& ssSkP1022("d1")
& ssSkP1021("d0")
& ~ ssSkP362("d0")
& ~ ssSkP361("d1")
& ~ ssSkP360("d2")
& ~ ssSkP1022("d2")
& ssSkP1020("d0")
& ~ ssSkP361("d2")
& ~ ssSkP360("d1")
& ~ ssSkP1021("d2")
& ssSkP1020("d1")
& ~ ssSkP362("d2")
& ~ ssSkP360("d0")
& ~ ssSkP1024("d2")
& ~ ssSkP366("d1")
& ~ ssSkP365("d0")
& ~ ssSkP363("d2")
& ~ ssSkP1023("d2")
& ~ ssSkP366("d0")
& ~ ssSkP364("d2")
& ~ ssSkP365("d1")
& ssSkP1023("d1")
& ssSkP1024("d0")
& ssSkP364("d1")
& ~ ssSkP365("d2")
& ~ ssSkP363("d0")
& ssSkP1023("d0")
& ~ ssSkP1024("d1")
& ~ ssSkP366("d2")
& ~ ssSkP364("d0")
& ~ ssSkP363("d1")
& ssSkP369("d0")
& ~ ssSkP367("d2")
& ssSkP369("d1")
& ~ ssSkP368("d2")
& ~ ssSkP369("d2")
& ~ ssSkP368("d1")
& ~ ssSkP367("d0")
& ~ ssSkP368("d0")
& ~ ssSkP367("d1")
& ~ ssSkP1009("d2")
& ssSkP1009("d1")
& ssSkP1009("d0")
& ~ ssSkP275("d2","d0")
& ~ ssSkP275("d0","d2")
& ssSkP276("d1","d2")
& ~ ssSkP276("d2","d1")
& ssSkP1011("d0")
& ssSkP1010("d1")
& ~ ssSkP275("d2","d1")
& ~ ssSkP275("d1","d2")
& ssSkP276("d0","d2")
& ~ ssSkP276("d2","d0")
& ssSkP1011("d1")
& ssSkP1010("d0")
& ~ ssSkP275("d2","d2")
& ssSkP275("d1","d1")
& ssSkP275("d0","d0")
& ssSkP276("d0","d1")
& ssSkP276("d1","d0")
& ~ ssSkP1011("d2")
& ssSkP275("d1","d0")
& ssSkP275("d0","d1")
& ~ ssSkP276("d2","d2")
& ssSkP276("d1","d1")
& ssSkP276("d0","d0")
& ~ ssSkP1010("d2")
& ssSkP1015("d0")
& ssSkP1014("d1")
& ~ ssSkP1013("d2")
& ssSkP1015("d1")
& ssSkP1014("d0")
& ~ ssSkP1012("d2")
& ~ ssSkP1015("d2")
& ssSkP1013("d0")
& ssSkP1012("d1")
& ~ ssSkP1014("d2")
& ssSkP1013("d1")
& ssSkP1012("d0")
& ssSkP1019("d0")
& ssSkP1018("d1")
& ~ ssSkP1017("d2")
& ssSkP1019("d1")
& ssSkP1018("d0")
& ~ ssSkP1016("d2")
& ~ ssSkP1019("d2")
& ssSkP1017("d0")
& ssSkP1016("d1")
& ~ ssSkP1018("d2")
& ssSkP1017("d1")
& ssSkP1016("d0")
& ~ ssSkP1000("d0")
& ~ ssSkP1000("d1")
& ~ ssSkP1000("d2")
& ~ ssSkP1004("d0")
& ~ ssSkP1003("d1")
& ~ ssSkP1002("d2")
& ~ ssSkP1004("d1")
& ~ ssSkP1003("d0")
& ~ ssSkP1001("d2")
& ~ ssSkP1004("d2")
& ~ ssSkP1002("d0")
& ~ ssSkP1001("d1")
& ~ ssSkP1003("d2")
& ~ ssSkP1002("d1")
& ~ ssSkP1001("d0")
& ssSkP1008("d0")
& ssSkP1007("d1")
& ~ ssSkP1006("d2")
& ssSkP1008("d1")
& ssSkP1007("d0")
& ~ ssSkP1005("d2")
& ~ ssSkP1008("d2")
& ssSkP1005("d1")
& ssSkP1006("d0")
& ~ ssSkP1007("d2")
& ssSkP1005("d0")
& ssSkP1006("d1")
& ~ ssSkP391("d1")
& ~ ssSkP390("d0")
& ~ ssSkP391("d0")
& ~ ssSkP390("d1")
& ~ ssSkP390("d2")
& ~ ssSkP391("d2")
& ~ ssSkP395("d1")
& ~ ssSkP394("d0")
& ~ ssSkP392("d2")
& ~ ssSkP395("d0")
& ~ ssSkP394("d1")
& ~ ssSkP393("d2")
& ~ ssSkP394("d2")
& ~ ssSkP393("d1")
& ~ ssSkP392("d0")
& ~ ssSkP395("d2")
& ~ ssSkP393("d0")
& ~ ssSkP392("d1")
& ssSkP398("d0")
& ~ ssSkP399("d1")
& ~ ssSkP396("d2")
& ssSkP398("d1")
& ssSkP399("d0")
& ~ ssSkP397("d2")
& ~ ssSkP398("d2")
& ssSkP396("d0")
& ssSkP397("d1")
& ~ ssSkP399("d2")
& ssSkP396("d1")
& ssSkP397("d0")
& ssSkP73("d1","d0")
& ssSkP73("d0","d1")
& ~ ssSkP74("d2","d2")
& ssSkP74("d1","d1")
& ssSkP74("d0","d0")
& ~ ssSkP73("d2","d2")
& ssSkP73("d1","d1")
& ssSkP73("d0","d0")
& ssSkP74("d0","d1")
& ssSkP74("d1","d0")
& ~ ssSkP73("d2","d1")
& ~ ssSkP73("d1","d2")
& ssSkP74("d0","d2")
& ~ ssSkP74("d2","d0")
& ~ ssSkP73("d2","d0")
& ~ ssSkP73("d0","d2")
& ssSkP74("d1","d2")
& ~ ssSkP74("d2","d1")
& ~ ssSkP53("d2","d1")
& ~ ssSkP53("d1","d2")
& ssSkP54("d0","d2")
& ~ ssSkP54("d2","d0")
& ~ ssSkP53("d2","d0")
& ~ ssSkP53("d0","d2")
& ssSkP54("d1","d2")
& ~ ssSkP54("d2","d1")
& ssSkP53("d1","d0")
& ssSkP53("d0","d1")
& ~ ssSkP54("d2","d2")
& ssSkP54("d1","d1")
& ssSkP54("d0","d0")
& ~ ssSkP53("d2","d2")
& ssSkP53("d1","d1")
& ssSkP53("d0","d0")
& ssSkP54("d0","d1")
& ssSkP54("d1","d0")
& ~ ssSkP58("d2")
& ~ ssSkP56("d0")
& ~ ssSkP55("d1")
& ~ ssSkP57("d2")
& ~ ssSkP56("d1")
& ~ ssSkP55("d0")
& ~ ssSkP58("d0")
& ~ ssSkP57("d1")
& ~ ssSkP56("d2")
& ~ ssSkP58("d1")
& ~ ssSkP57("d0")
& ~ ssSkP55("d2")
& ~ ssSkP59("d1")
& ~ ssSkP59("d0")
& ~ ssSkP59("d2")
& ~ ssSkP61("d2")
& ~ ssSkP60("d2")
& ~ ssSkP61("d0")
& ~ ssSkP60("d1")
& ~ ssSkP61("d1")
& ~ ssSkP60("d0")
& ~ ssSkP65("d2")
& ssSkP62("d1")
& ~ ssSkP63("d0")
& ~ ssSkP64("d2")
& ~ ssSkP62("d0")
& ~ ssSkP63("d1")
& ~ ssSkP65("d0")
& ~ ssSkP64("d1")
& ~ ssSkP63("d2")
& ~ ssSkP65("d1")
& ~ ssSkP64("d0")
& ~ ssSkP62("d2")
& ~ ssSkP69("d2")
& ~ ssSkP67("d0")
& ~ ssSkP66("d1")
& ~ ssSkP68("d2")
& ~ ssSkP67("d1")
& ~ ssSkP66("d0")
& ~ ssSkP68("d1")
& ~ ssSkP69("d0")
& ~ ssSkP67("d2")
& ~ ssSkP68("d0")
& ~ ssSkP69("d1")
& ~ ssSkP66("d2")
& ~ ssSkP70("d0")
& ~ ssSkP72("d2")
& ~ ssSkP71("d2")
& ~ ssSkP70("d1")
& ~ ssSkP70("d2")
& ssSkP71("d1")
& ssSkP72("d0")
& ssSkP71("d0")
& ~ ssSkP72("d1")
& ~ ssSkP76("d2")
& ~ ssSkP75("d2")
& ~ ssSkP76("d0")
& ~ ssSkP75("d1")
& ~ ssSkP76("d1")
& ~ ssSkP75("d0")
& ~ ssSkP78("d0")
& ~ ssSkP77("d1")
& ~ ssSkP79("d2")
& ~ ssSkP78("d1")
& ~ ssSkP77("d0")
& ~ ssSkP79("d1")
& ~ ssSkP78("d2")
& ~ ssSkP79("d0")
& ~ ssSkP77("d2")
& ~ ssSkP83("d2")
& ~ ssSkP81("d0")
& ~ ssSkP80("d1")
& ~ ssSkP82("d2")
& ~ ssSkP81("d1")
& ~ ssSkP80("d0")
& ~ ssSkP83("d0")
& ~ ssSkP82("d1")
& ~ ssSkP81("d2")
& ~ ssSkP83("d1")
& ~ ssSkP82("d0")
& ~ ssSkP80("d2")
& ~ ssSkP87("d2")
& ~ ssSkP85("d0")
& ~ ssSkP84("d1")
& ~ ssSkP86("d2")
& ~ ssSkP85("d1")
& ~ ssSkP84("d0")
& ~ ssSkP86("d1")
& ~ ssSkP87("d0")
& ~ ssSkP85("d2")
& ~ ssSkP86("d0")
& ~ ssSkP87("d1")
& ~ ssSkP84("d2")
& ~ ssSkP89("d0")
& ~ ssSkP88("d1")
& ~ ssSkP89("d1")
& ~ ssSkP88("d0")
& ~ ssSkP89("d2")
& ~ ssSkP88("d2")
& ~ ssSkP94("d2")
& ~ ssSkP92("d0")
& ~ ssSkP91("d1")
& ~ ssSkP93("d2")
& ~ ssSkP92("d1")
& ~ ssSkP91("d0")
& ~ ssSkP94("d0")
& ~ ssSkP93("d1")
& ~ ssSkP92("d2")
& ~ ssSkP94("d1")
& ~ ssSkP93("d0")
& ~ ssSkP91("d2")
& ~ ssSkP98("d2")
& ~ ssSkP96("d0")
& ~ ssSkP95("d1")
& ~ ssSkP97("d2")
& ~ ssSkP96("d1")
& ~ ssSkP95("d0")
& ~ ssSkP97("d1")
& ~ ssSkP98("d0")
& ~ ssSkP96("d2")
& ~ ssSkP97("d0")
& ~ ssSkP98("d1")
& ~ ssSkP95("d2")
& ~ ssSkP99("d1")
& ~ ssSkP99("d0")
& ~ ssSkP99("d2")
& ~ ssSkP90("d2")
& ~ ssSkP90("d0")
& ~ ssSkP90("d1")
& ~ ssSkP10("d2")
& ~ ssSkP10("d0")
& ~ ssSkP10("d1")
& ~ ssSkP14("d2")
& ~ ssSkP12("d0")
& ~ ssSkP11("d1")
& ~ ssSkP13("d2")
& ~ ssSkP12("d1")
& ~ ssSkP11("d0")
& ssSkP14("d0")
& ~ ssSkP13("d1")
& ~ ssSkP12("d2")
& ssSkP14("d1")
& ~ ssSkP13("d0")
& ~ ssSkP11("d2")
& ~ ssSkP18("d2")
& ssSkP16("d0")
& ssSkP15("d1")
& ~ ssSkP17("d2")
& ssSkP16("d1")
& ssSkP15("d0")
& ssSkP18("d0")
& ssSkP17("d1")
& ~ ssSkP16("d2")
& ssSkP18("d1")
& ssSkP17("d0")
& ~ ssSkP15("d2")
& ~ ssSkP21("d2")
& ~ ssSkP20("d2")
& ssSkP20("d1")
& ssSkP21("d0")
& ssSkP20("d0")
& ssSkP21("d1")
& ~ ssSkP25("d2")
& ssSkP23("d0")
& ssSkP22("d1")
& ~ ssSkP24("d2")
& ssSkP23("d1")
& ssSkP22("d0")
& ssSkP24("d1")
& ssSkP25("d0")
& ~ ssSkP23("d2")
& ssSkP25("d1")
& ssSkP24("d0")
& ~ ssSkP22("d2")
& ~ ssSkP26("d1")
& ssSkP26("d0")
& ~ ssSkP26("d2")
& ~ ssSkP19("d1")
& ssSkP19("d0")
& ~ ssSkP19("d2")
& ssPv9("d1")
& ~ ssPv8("d0")
& ~ ssPv6("d2")
& ssPv9("d0")
& ssPv8("d1")
& ~ ssPv7("d2")
& ~ ssPv8("d2")
& ~ ssPv6("d0")
& ssPv7("d1")
& ~ ssPv9("d2")
& ssPv6("d1")
& ~ ssPv7("d0")
& ~ ssPv4("d0")
& ssPv5("d1")
& ~ ssPv4("d1")
& ~ ssPv3("d2")
& ~ ssPv5("d0")
& ~ ssPv4("d2")
& ssPv3("d1")
& ssPv3("d0")
& ~ ssPv5("d2")
& ssPv1("d1")
& ssPv1("d0")
& ~ ssPv1("d2")
& ~ ssSkP737("d0")
& ~ ssSkP737("d1")
& ~ ssSkP737("d2")
& ~ ssSkP739("d2")
& ~ ssSkP738("d2")
& ~ ssSkP739("d0")
& ~ ssSkP738("d1")
& ~ ssSkP739("d1")
& ~ ssSkP738("d0")
& ~ ssSkP740("d0")
& ~ ssSkP740("d1")
& ~ ssSkP740("d2")
& ~ ssSkP744("d0")
& ~ ssSkP743("d1")
& ~ ssSkP742("d2")
& ~ ssSkP744("d1")
& ~ ssSkP743("d0")
& ~ ssSkP741("d2")
& ~ ssSkP744("d2")
& ~ ssSkP742("d0")
& ~ ssSkP741("d1")
& ~ ssSkP743("d2")
& ~ ssSkP742("d1")
& ~ ssSkP741("d0")
& ssSkP767("d2")
& ~ ssSkP767("d1")
& ~ ssSkP767("d0")
& ~ ssSkP772("d1")
& ~ ssSkP773("d0")
& ~ ssSkP771("d2")
& ~ ssSkP772("d0")
& ~ ssSkP773("d1")
& ~ ssSkP770("d2")
& ~ ssSkP773("d2")
& ~ ssSkP771("d0")
& ~ ssSkP770("d1")
& ~ ssSkP772("d2")
& ~ ssSkP771("d1")
& ~ ssSkP770("d0")
& ~ ssSkP777("d0")
& ~ ssSkP775("d2")
& ~ ssSkP776("d1")
& ~ ssSkP777("d1")
& ~ ssSkP776("d0")
& ~ ssSkP774("d2")
& ~ ssSkP777("d2")
& ~ ssSkP775("d0")
& ~ ssSkP774("d1")
& ~ ssSkP775("d1")
& ~ ssSkP776("d2")
& ~ ssSkP774("d0")
& ~ ssSkP779("d2")
& ~ ssSkP778("d2")
& ~ ssSkP779("d0")
& ~ ssSkP778("d1")
& ~ ssSkP779("d1")
& ~ ssSkP778("d0")
& ~ ssSkP885("d2","d0")
& ~ ssSkP885("d0","d2")
& ssSkP886("d0","d1")
& ssSkP886("d1","d0")
& ~ ssSkP885("d2","d1")
& ~ ssSkP885("d1","d2")
& ~ ssSkP886("d2","d2")
& ssSkP886("d1","d1")
& ssSkP886("d0","d0")
& ~ ssSkP885("d2","d2")
& ssSkP885("d1","d1")
& ssSkP885("d0","d0")
& ssSkP886("d1","d2")
& ~ ssSkP886("d2","d1")
& ssSkP885("d1","d0")
& ssSkP885("d0","d1")
& ssSkP886("d0","d2")
& ~ ssSkP886("d2","d0")
& ~ ssSkP780("d0")
& ~ ssSkP780("d1")
& ~ ssSkP780("d2")
& ~ ssSkP784("d0")
& ~ ssSkP783("d1")
& ~ ssSkP782("d2")
& ~ ssSkP784("d1")
& ~ ssSkP783("d0")
& ~ ssSkP781("d2")
& ~ ssSkP784("d2")
& ~ ssSkP782("d0")
& ~ ssSkP781("d1")
& ~ ssSkP783("d2")
& ~ ssSkP782("d1")
& ~ ssSkP781("d0")
& ~ ssSkP788("d0")
& ~ ssSkP786("d2")
& ~ ssSkP787("d1")
& ~ ssSkP788("d1")
& ~ ssSkP787("d0")
& ~ ssSkP785("d2")
& ~ ssSkP788("d2")
& ~ ssSkP786("d0")
& ~ ssSkP785("d1")
& ssSkP786("d1")
& ~ ssSkP787("d2")
& ~ ssSkP785("d0")
& ~ ssSkP748("d0")
& ~ ssSkP747("d1")
& ~ ssSkP746("d2")
& ~ ssSkP748("d1")
& ~ ssSkP747("d0")
& ~ ssSkP745("d2")
& ~ ssSkP748("d2")
& ~ ssSkP746("d0")
& ~ ssSkP745("d1")
& ~ ssSkP747("d2")
& ~ ssSkP746("d1")
& ~ ssSkP745("d0")
& ~ ssSkP749("d2")
& ~ ssSkP749("d1")
& ~ ssSkP749("d0")
& ~ ssSkP751("d0")
& ~ ssSkP750("d1")
& ~ ssSkP751("d1")
& ~ ssSkP750("d0")
& ~ ssSkP751("d2")
& ~ ssSkP750("d2")
& ~ ssSkP755("d0")
& ~ ssSkP753("d2")
& ~ ssSkP754("d1")
& ~ ssSkP755("d1")
& ~ ssSkP754("d0")
& ~ ssSkP752("d2")
& ~ ssSkP755("d2")
& ssSkP753("d0")
& ~ ssSkP752("d1")
& ~ ssSkP753("d1")
& ~ ssSkP754("d2")
& ~ ssSkP752("d0")
& ~ ssSkP759("d0")
& ~ ssSkP758("d1")
& ~ ssSkP757("d2")
& ~ ssSkP759("d1")
& ~ ssSkP758("d0")
& ~ ssSkP756("d2")
& ~ ssSkP759("d2")
& ~ ssSkP757("d0")
& ~ ssSkP756("d1")
& ~ ssSkP758("d2")
& ~ ssSkP757("d1")
& ~ ssSkP756("d0")
& ~ ssSkP762("d0")
& ~ ssSkP760("d2")
& ~ ssSkP761("d1")
& ~ ssSkP762("d1")
& ~ ssSkP761("d0")
& ~ ssSkP762("d2")
& ssSkP760("d0")
& ~ ssSkP760("d1")
& ~ ssSkP761("d2")
& ~ ssSkP766("d0")
& ~ ssSkP765("d1")
& ~ ssSkP764("d2")
& ~ ssSkP766("d1")
& ~ ssSkP765("d0")
& ~ ssSkP763("d2")
& ~ ssSkP766("d2")
& ~ ssSkP764("d0")
& ~ ssSkP763("d1")
& ~ ssSkP765("d2")
& ~ ssSkP764("d1")
& ~ ssSkP763("d0")
& ~ ssSkP1190("d0")
& ssSkP1190("d1")
& ~ ssSkP1190("d2")
& ssSkP1193("d1")
& ssSkP1194("d0")
& ~ ssSkP1192("d2")
& ssSkP1193("d0")
& ssSkP1194("d1")
& ~ ssSkP1191("d2")
& ~ ssSkP1194("d2")
& ssSkP1191("d1")
& ssSkP1192("d0")
& ~ ssSkP1193("d2")
& ~ ssSkP1191("d0")
& ssSkP1192("d1")
& ~ ssSkP1196("d2")
& ssSkP1197("d1")
& ssSkP1198("d0")
& ~ ssSkP1195("d2")
& ssSkP1197("d0")
& ssSkP1198("d1")
& ssSkP1195("d1")
& ssSkP1196("d0")
& ~ ssSkP1198("d2")
& ssSkP1195("d0")
& ssSkP1196("d1")
& ~ ssSkP1197("d2")
& ~ ssSkP1199("d2")
& ssSkP1199("d1")
& ssSkP1199("d0")
& ~ ssSkP1183("d0")
& ssSkP1182("d1")
& ~ ssSkP1181("d2")
& ssSkP1183("d1")
& ~ ssSkP1182("d0")
& ~ ssSkP1180("d2")
& ~ ssSkP1183("d2")
& ~ ssSkP1181("d0")
& ssSkP1180("d1")
& ~ ssSkP1182("d2")
& ssSkP1181("d1")
& ~ ssSkP1180("d0")
& ~ ssSkP1187("d0")
& ssSkP1186("d1")
& ~ ssSkP1185("d2")
& ssSkP1187("d1")
& ~ ssSkP1186("d0")
& ~ ssSkP1184("d2")
& ~ ssSkP1187("d2")
& ~ ssSkP1185("d0")
& ssSkP1184("d1")
& ~ ssSkP1186("d2")
& ssSkP1185("d1")
& ~ ssSkP1184("d0")
& ~ ssSkP1189("d2")
& ~ ssSkP1188("d2")
& ~ ssSkP1189("d0")
& ssSkP1188("d1")
& ssSkP1189("d1")
& ssSkP1188("d0")
& ~ ssSkP1172("d0")
& ssSkP1171("d1")
& ~ ssSkP1170("d2")
& ssSkP1172("d1")
& ~ ssSkP1171("d0")
& ~ ssSkP1172("d2")
& ~ ssSkP1170("d0")
& ~ ssSkP1171("d2")
& ssSkP1170("d1")
& ssSkP1175("d1")
& ~ ssSkP1176("d0")
& ~ ssSkP1174("d2")
& ~ ssSkP1175("d0")
& ssSkP1176("d1")
& ~ ssSkP1173("d2")
& ~ ssSkP1176("d2")
& ssSkP1173("d1")
& ~ ssSkP1174("d0")
& ~ ssSkP1175("d2")
& ~ ssSkP1173("d0")
& ssSkP1174("d1")
& ~ ssSkP1178("d2")
& ssSkP1179("d1")
& ~ ssSkP1177("d2")
& ~ ssSkP1179("d0")
& ssSkP1177("d1")
& ~ ssSkP1178("d0")
& ~ ssSkP1177("d0")
& ssSkP1178("d1")
& ~ ssSkP1179("d2")
& ~ ssSkP1161("d0")
& ssSkP1160("d1")
& ssSkP1161("d1")
& ~ ssSkP1160("d0")
& ~ ssSkP1161("d2")
& ~ ssSkP1160("d2")
& ~ ssSkP1163("d2")
& ~ ssSkP1165("d0")
& ssSkP1164("d1")
& ~ ssSkP1162("d2")
& ssSkP1165("d1")
& ~ ssSkP1164("d0")
& ~ ssSkP1163("d0")
& ssSkP1162("d1")
& ~ ssSkP1165("d2")
& ssSkP1163("d1")
& ~ ssSkP1162("d0")
& ~ ssSkP1164("d2")
& ssSkP1168("d1")
& ~ ssSkP1169("d0")
& ~ ssSkP1167("d2")
& ~ ssSkP1168("d0")
& ssSkP1169("d1")
& ~ ssSkP1169("d2")
& ~ ssSkP1167("d0")
& ~ ssSkP1168("d2")
& ssSkP1167("d1")
& ~ ssSkP1154("d0")
& ~ ssSkP1152("d2")
& ssSkP1154("d1")
& ~ ssSkP1154("d2")
& ssSkP1152("d0")
& ssSkP1152("d1")
& ~ ssSkP1156("d2")
& ssSkP1157("d1")
& ~ ssSkP1158("d0")
& ~ ssSkP1155("d2")
& ~ ssSkP1157("d0")
& ssSkP1158("d1")
& ~ ssSkP1156("d0")
& ssSkP1155("d1")
& ~ ssSkP1158("d2")
& ssSkP1156("d1")
& ~ ssSkP1155("d0")
& ~ ssSkP1157("d2")
& ~ ssSkP1159("d2")
& ssSkP1159("d1")
& ~ ssSkP1159("d0")
& ~ ssSkP1119("d2")
& ~ ssSkP1119("d1")
& ssSkP1119("d0")
& ~ ssSkP1109("d2")
& ~ ssSkP1108("d2")
& ssSkP1109("d0")
& ssSkP1108("d1")
& ssSkP1109("d1")
& ssSkP1108("d0")
& ssSkP1110("d0")
& ssSkP1110("d1")
& ~ ssSkP1110("d2")
& ssSkP1114("d0")
& ssSkP1113("d1")
& ~ ssSkP1112("d2")
& ssSkP1114("d1")
& ssSkP1113("d0")
& ~ ssSkP1111("d2")
& ~ ssSkP1114("d2")
& ssSkP1112("d0")
& ssSkP1111("d1")
& ~ ssSkP1113("d2")
& ssSkP1112("d1")
& ssSkP1111("d0")
& ssSkP1118("d0")
& ssSkP1117("d1")
& ~ ssSkP1116("d2")
& ssSkP1118("d1")
& ssSkP1117("d0")
& ~ ssSkP1115("d2")
& ~ ssSkP1118("d2")
& ssSkP1116("d0")
& ssSkP1115("d1")
& ~ ssSkP1117("d2")
& ssSkP1116("d1")
& ssSkP1115("d0")
& ssSkP1103("d0")
& ssSkP1102("d1")
& ~ ssSkP1101("d2")
& ssSkP1103("d1")
& ssSkP1102("d0")
& ~ ssSkP1100("d2")
& ~ ssSkP1103("d2")
& ssSkP1101("d0")
& ssSkP1100("d1")
& ~ ssSkP1102("d2")
& ssSkP1101("d1")
& ssSkP1100("d0")
& ssSkP1107("d0")
& ~ ssSkP1105("d2")
& ssSkP1106("d1")
& ssSkP1107("d1")
& ssSkP1106("d0")
& ~ ssSkP1104("d2")
& ~ ssSkP1107("d2")
& ssSkP1105("d0")
& ~ ssSkP1104("d1")
& ssSkP1105("d1")
& ~ ssSkP1106("d2")
& ssSkP1104("d0")
& ssSkP947("d1","d2")
& ~ ssSkP947("d2","d1")
& ssSkP947("d0","d2")
& ~ ssSkP947("d2","d0")
& ssSkP947("d0","d1")
& ssSkP947("d1","d0")
& ~ ssSkP947("d2","d2")
& ssSkP947("d1","d1")
& ssSkP947("d0","d0")
& ~ ssSkP946("d2","d2")
& ssSkP946("d1","d1")
& ssSkP946("d0","d0")
& ssSkP946("d1","d0")
& ssSkP946("d0","d1")
& ~ ssSkP946("d2","d0")
& ~ ssSkP946("d0","d2")
& ~ ssSkP946("d2","d1")
& ~ ssSkP946("d1","d2")
& ssSkP616("d0")
& ssSkP615("d1")
& ssSkP616("d1")
& ssSkP615("d0")
& ~ ssSkP616("d2")
& ~ ssSkP615("d2")
& ssSkP619("d1")
& ~ ssSkP618("d2")
& ssSkP619("d0")
& ~ ssSkP617("d2")
& ssSkP618("d0")
& ssSkP617("d1")
& ~ ssSkP619("d2")
& ssSkP618("d1")
& ssSkP617("d0")
& ssSkP623("d0")
& ssSkP622("d1")
& ~ ssSkP621("d2")
& ssSkP623("d1")
& ssSkP622("d0")
& ~ ssSkP620("d2")
& ~ ssSkP623("d2")
& ssSkP621("d0")
& ssSkP620("d1")
& ~ ssSkP622("d2")
& ssSkP621("d1")
& ssSkP620("d0")
& ~ ssSkP969("d2","d1")
& ~ ssSkP969("d1","d2")
& ~ ssSkP969("d2","d0")
& ~ ssSkP969("d0","d2")
& ssSkP969("d1","d0")
& ssSkP969("d0","d1")
& ~ ssSkP969("d2","d2")
& ssSkP969("d1","d1")
& ssSkP969("d0","d0")
& ssSkP970("d0","d1")
& ssSkP970("d1","d0")
& ~ ssSkP970("d2","d2")
& ssSkP970("d1","d1")
& ssSkP970("d0","d0")
& ssSkP970("d1","d2")
& ~ ssSkP970("d2","d1")
& ssSkP970("d0","d2")
& ~ ssSkP970("d2","d0")
& ~ ssSkP995("d2","d0")
& ~ ssSkP995("d0","d2")
& ssSkP996("d0","d1")
& ssSkP996("d1","d0")
& ~ ssSkP995("d2","d1")
& ~ ssSkP995("d1","d2")
& ~ ssSkP996("d2","d2")
& ssSkP996("d1","d1")
& ssSkP996("d0","d0")
& ~ ssSkP995("d2","d2")
& ssSkP995("d1","d1")
& ssSkP995("d0","d0")
& ssSkP996("d1","d2")
& ~ ssSkP996("d2","d1")
& ssSkP995("d1","d0")
& ssSkP995("d0","d1")
& ssSkP996("d0","d2")
& ~ ssSkP996("d2","d0")
& ssSkP626("d1")
& ssSkP627("d0")
& ~ ssSkP625("d2")
& ssSkP626("d0")
& ssSkP627("d1")
& ~ ssSkP624("d2")
& ~ ssSkP627("d2")
& ~ ssSkP625("d0")
& ssSkP624("d1")
& ~ ssSkP626("d2")
& ssSkP625("d1")
& ssSkP624("d0")
& ~ ssSkP629("d2")
& ~ ssSkP628("d2")
& ssSkP629("d0")
& ssSkP628("d1")
& ssSkP629("d1")
& ssSkP628("d0")
& ssSkP630("d0")
& ssSkP630("d1")
& ~ ssSkP630("d2")
& ssSkP634("d0")
& ssSkP633("d1")
& ~ ssSkP632("d2")
& ssSkP634("d1")
& ssSkP633("d0")
& ~ ssSkP631("d2")
& ~ ssSkP634("d2")
& ssSkP632("d0")
& ssSkP631("d1")
& ~ ssSkP633("d2")
& ssSkP632("d1")
& ssSkP631("d0")
& ssSkP638("d0")
& ~ ssSkP637("d1")
& ~ ssSkP636("d2")
& ssSkP638("d1")
& ssSkP637("d0")
& ~ ssSkP635("d2")
& ~ ssSkP638("d2")
& ssSkP636("d0")
& ssSkP635("d1")
& ~ ssSkP637("d2")
& ssSkP636("d1")
& ssSkP635("d0")
& ~ ssSkP639("d2")
& ssSkP639("d1")
& ssSkP639("d0")
& ssSkP641("d0")
& ssSkP640("d1")
& ssSkP641("d1")
& ssSkP640("d0")
& ~ ssSkP641("d2")
& ~ ssSkP640("d2")
& ~ ssSkP643("d2")
& ~ ssSkP642("d2")
& ssSkP642("d1")
& ssSkP643("d0")
& ssSkP642("d0")
& ~ ssSkP643("d1")
& ~ ssSkP569("d2")
& ssSkP569("d1")
& ssSkP569("d0")
& ssSkP571("d0")
& ssSkP570("d1")
& ssSkP571("d1")
& ssSkP570("d0")
& ~ ssSkP571("d2")
& ~ ssSkP570("d2")
& ssSkP574("d1")
& ssSkP575("d0")
& ~ ssSkP573("d2")
& ssSkP574("d0")
& ssSkP575("d1")
& ~ ssSkP572("d2")
& ~ ssSkP575("d2")
& ssSkP573("d0")
& ssSkP572("d1")
& ~ ssSkP574("d2")
& ssSkP573("d1")
& ssSkP572("d0")
& ssSkP579("d0")
& ~ ssSkP578("d1")
& ~ ssSkP577("d2")
& ssSkP579("d1")
& ssSkP578("d0")
& ~ ssSkP576("d2")
& ~ ssSkP579("d2")
& ssSkP577("d0")
& ssSkP576("d1")
& ~ ssSkP578("d2")
& ssSkP577("d1")
& ssSkP576("d0")
& ssSkP582("d0")
& ssSkP581("d1")
& ~ ssSkP580("d2")
& ssSkP582("d1")
& ssSkP581("d0")
& ~ ssSkP582("d2")
& ssSkP580("d0")
& ~ ssSkP581("d2")
& ssSkP580("d1")
& ~ ssSkP584("d2")
& ~ ssSkP583("d2")
& ssSkP583("d1")
& ssSkP584("d0")
& ssSkP583("d0")
& ~ ssSkP584("d1")
& ~ ssSkP559("d2")
& ~ ssSkP559("d0")
& ~ ssSkP559("d1")
& ~ ssSkP560("d0")
& ~ ssSkP560("d1")
& ~ ssSkP560("d2")
& ssSkP564("d0")
& ~ ssSkP563("d1")
& ~ ssSkP562("d2")
& ssSkP564("d1")
& ~ ssSkP563("d0")
& ~ ssSkP561("d2")
& ~ ssSkP564("d2")
& ~ ssSkP562("d0")
& ~ ssSkP561("d1")
& ~ ssSkP563("d2")
& ~ ssSkP562("d1")
& ~ ssSkP561("d0")
& ssSkP568("d0")
& ssSkP567("d1")
& ~ ssSkP566("d2")
& ssSkP568("d1")
& ssSkP567("d0")
& ~ ssSkP565("d2")
& ~ ssSkP568("d2")
& ssSkP566("d0")
& ssSkP565("d1")
& ~ ssSkP567("d2")
& ssSkP566("d1")
& ssSkP565("d0")
& ssSkP1253("d0")
& ssSkP1252("d1")
& ~ ssSkP1251("d2")
& ssSkP1253("d1")
& ssSkP1252("d0")
& ~ ssSkP1250("d2")
& ~ ssSkP1253("d2")
& ssSkP1250("d1")
& ssSkP1251("d0")
& ~ ssSkP1252("d2")
& ssSkP1250("d0")
& ssSkP1251("d1")
& ssSkP1255("d2")
& ~ ssSkP1256("d1")
& ~ ssSkP1254("d2")
& ssSkP1256("d0")
& ssSkP1255("d0")
& ssSkP1254("d1")
& ~ ssSkP1255("d1")
& ssSkP1254("d0")
& ~ ssSkP1256("d2")
& ssSkP1242("d0")
& ~ ssSkP1240("d2")
& ssSkP1241("d1")
& ssSkP1242("d1")
& ssSkP1241("d0")
& ~ ssSkP1242("d2")
& ssSkP1240("d0")
& ssSkP1240("d1")
& ~ ssSkP1241("d2")
& ssSkP1246("d0")
& ~ ssSkP1244("d2")
& ssSkP1245("d1")
& ssSkP1246("d1")
& ssSkP1245("d0")
& ~ ssSkP1243("d2")
& ~ ssSkP1246("d2")
& ssSkP1244("d0")
& ssSkP1243("d1")
& ssSkP1244("d1")
& ~ ssSkP1245("d2")
& ssSkP1243("d0")
& ~ ssSkP1248("d2")
& ssSkP1249("d1")
& ssSkP1249("d0")
& ~ ssSkP1247("d2")
& ssSkP1248("d0")
& ssSkP1247("d1")
& ssSkP1248("d1")
& ~ ssSkP1249("d2")
& ssSkP1247("d0")
& ~ ssSkP1229("d2")
& ssSkP1229("d1")
& ssSkP1229("d0")
& ssSkP1230("d1")
& ssSkP1231("d0")
& ssSkP1230("d0")
& ssSkP1231("d1")
& ~ ssSkP1231("d2")
& ~ ssSkP1230("d2")
& ssSkP1234("d1")
& ssSkP1235("d0")
& ~ ssSkP1233("d2")
& ssSkP1234("d0")
& ssSkP1235("d1")
& ~ ssSkP1232("d2")
& ~ ssSkP1235("d2")
& ssSkP1232("d1")
& ssSkP1233("d0")
& ~ ssSkP1234("d2")
& ssSkP1232("d0")
& ssSkP1233("d1")
& ssSkP1238("d1")
& ssSkP1239("d0")
& ~ ssSkP1237("d2")
& ssSkP1238("d0")
& ssSkP1239("d1")
& ~ ssSkP1236("d2")
& ~ ssSkP1239("d2")
& ssSkP1236("d1")
& ssSkP1237("d0")
& ~ ssSkP1238("d2")
& ssSkP1236("d0")
& ssSkP1237("d1")
& ~ ssSkP1219("d2")
& ~ ssSkP1218("d2")
& ssSkP1218("d1")
& ssSkP1219("d0")
& ssSkP1218("d0")
& ssSkP1219("d1")
& ssSkP1220("d0")
& ssSkP1220("d1")
& ~ ssSkP1220("d2")
& ssSkP1224("d0")
& ~ ssSkP1222("d2")
& ssSkP1223("d1")
& ssSkP1224("d1")
& ssSkP1223("d0")
& ~ ssSkP1221("d2")
& ~ ssSkP1224("d2")
& ssSkP1222("d0")
& ssSkP1221("d1")
& ssSkP1222("d1")
& ~ ssSkP1223("d2")
& ssSkP1221("d0")
& ssSkP1228("d0")
& ~ ssSkP1226("d2")
& ssSkP1227("d1")
& ssSkP1228("d1")
& ssSkP1227("d0")
& ~ ssSkP1225("d2")
& ~ ssSkP1228("d2")
& ssSkP1226("d0")
& ssSkP1225("d1")
& ssSkP1226("d1")
& ~ ssSkP1227("d2")
& ssSkP1225("d0")
& ~ ssSkP1208("d2")
& ssSkP1209("d1")
& ssSkP1209("d0")
& ~ ssSkP1207("d2")
& ssSkP1208("d0")
& ssSkP1207("d1")
& ssSkP1208("d1")
& ~ ssSkP1209("d2")
& ssSkP1207("d0")
& ssSkP1212("d1")
& ssSkP1213("d0")
& ~ ssSkP1211("d2")
& ssSkP1212("d0")
& ssSkP1213("d1")
& ~ ssSkP1210("d2")
& ~ ssSkP1213("d2")
& ssSkP1210("d1")
& ssSkP1211("d0")
& ~ ssSkP1212("d2")
& ssSkP1210("d0")
& ssSkP1211("d1")
& ssSkP1216("d1")
& ssSkP1217("d0")
& ~ ssSkP1215("d2")
& ssSkP1216("d0")
& ssSkP1217("d1")
& ~ ssSkP1214("d2")
& ~ ssSkP1217("d2")
& ssSkP1214("d1")
& ssSkP1215("d0")
& ~ ssSkP1216("d2")
& ssSkP1214("d0")
& ssSkP1215("d1")
& ~ ssSkP1200("d2")
& ssSkP1201("d1")
& ssSkP1202("d0")
& ssSkP1201("d0")
& ssSkP1202("d1")
& ssSkP1200("d0")
& ~ ssSkP1202("d2")
& ssSkP1200("d1")
& ~ ssSkP1201("d2")
& ~ ssSkP1204("d2")
& ssSkP1206("d0")
& ssSkP1205("d1")
& ~ ssSkP1203("d2")
& ssSkP1206("d1")
& ssSkP1205("d0")
& ssSkP1203("d1")
& ssSkP1204("d0")
& ~ ssSkP1206("d2")
& ssSkP1203("d0")
& ssSkP1204("d1")
& ~ ssSkP1205("d2")
& ssSkP902("d0")
& ~ ssSkP901("d1")
& ~ ssSkP900("d2")
& ssSkP902("d1")
& ~ ssSkP901("d0")
& ~ ssSkP902("d2")
& ~ ssSkP900("d0")
& ~ ssSkP901("d2")
& ~ ssSkP900("d1")
& ssSkP906("d0")
& ~ ssSkP904("d2")
& ssSkP905("d1")
& ssSkP906("d1")
& ssSkP905("d0")
& ~ ssSkP903("d2")
& ~ ssSkP906("d2")
& ssSkP904("d0")
& ssSkP903("d1")
& ssSkP904("d1")
& ~ ssSkP905("d2")
& ssSkP903("d0")
& ssSkP909("d1")
& ~ ssSkP908("d2")
& ssSkP909("d0")
& ~ ssSkP907("d2")
& ssSkP908("d0")
& ssSkP907("d1")
& ~ ssSkP909("d2")
& ssSkP908("d1")
& ssSkP907("d0")
& ssSkP912("d1")
& ssSkP913("d0")
& ~ ssSkP911("d2")
& ssSkP912("d0")
& ~ ssSkP913("d1")
& ~ ssSkP910("d2")
& ~ ssSkP913("d2")
& ssSkP911("d0")
& ssSkP910("d1")
& ~ ssSkP912("d2")
& ssSkP911("d1")
& ssSkP910("d0")
& ssSkP967("d1")
& ssSkP968("d0")
& ~ ssSkP966("d2")
& ssSkP967("d0")
& ~ ssSkP968("d1")
& ~ ssSkP965("d2")
& ~ ssSkP968("d2")
& ssSkP966("d0")
& ssSkP965("d1")
& ~ ssSkP967("d2")
& ssSkP966("d1")
& ssSkP965("d0")
& ~ ssSkP971("d0")
& ~ ssSkP971("d1")
& ~ ssSkP971("d2")
& ~ ssSkP975("d0")
& ~ ssSkP974("d1")
& ~ ssSkP973("d2")
& ~ ssSkP975("d1")
& ~ ssSkP974("d0")
& ~ ssSkP972("d2")
& ~ ssSkP975("d2")
& ~ ssSkP972("d1")
& ~ ssSkP973("d0")
& ~ ssSkP974("d2")
& ~ ssSkP972("d0")
& ~ ssSkP973("d1")
& ssSkP979("d0")
& ssSkP978("d1")
& ~ ssSkP977("d2")
& ssSkP979("d1")
& ssSkP978("d0")
& ~ ssSkP976("d2")
& ~ ssSkP979("d2")
& ssSkP976("d1")
& ssSkP977("d0")
& ~ ssSkP978("d2")
& ssSkP976("d0")
& ssSkP977("d1")
& ssSkP981("d1")
& ssSkP982("d0")
& ~ ssSkP980("d2")
& ssSkP981("d0")
& ssSkP982("d1")
& ~ ssSkP982("d2")
& ssSkP980("d0")
& ~ ssSkP981("d2")
& ssSkP980("d1")
& ssSkP986("d0")
& ssSkP985("d1")
& ~ ssSkP984("d2")
& ssSkP986("d1")
& ssSkP985("d0")
& ~ ssSkP983("d2")
& ~ ssSkP986("d2")
& ssSkP984("d0")
& ssSkP983("d1")
& ~ ssSkP985("d2")
& ssSkP984("d1")
& ssSkP983("d0")
& ssSkP949("d1")
& ~ ssSkP948("d2")
& ssSkP949("d0")
& ssSkP948("d0")
& ~ ssSkP949("d2")
& ssSkP948("d1")
& ssSkP952("d1")
& ssSkP953("d0")
& ~ ssSkP951("d2")
& ssSkP952("d0")
& ssSkP953("d1")
& ~ ssSkP950("d2")
& ~ ssSkP953("d2")
& ssSkP951("d0")
& ssSkP950("d1")
& ~ ssSkP952("d2")
& ssSkP951("d1")
& ssSkP950("d0")
& ssSkP957("d0")
& ~ ssSkP955("d2")
& ssSkP956("d1")
& ssSkP957("d1")
& ssSkP956("d0")
& ~ ssSkP954("d2")
& ~ ssSkP957("d2")
& ssSkP955("d0")
& ssSkP954("d1")
& ssSkP955("d1")
& ~ ssSkP956("d2")
& ssSkP954("d0")
& ~ ssSkP959("d2")
& ~ ssSkP958("d2")
& ssSkP959("d0")
& ssSkP958("d1")
& ssSkP959("d1")
& ssSkP958("d0")
& ~ ssSkP613("d2","d1")
& ~ ssSkP613("d1","d2")
& ssSkP614("d0","d2")
& ~ ssSkP614("d2","d0")
& ~ ssSkP613("d2","d0")
& ~ ssSkP613("d0","d2")
& ssSkP614("d1","d2")
& ~ ssSkP614("d2","d1")
& ssSkP613("d1","d0")
& ssSkP613("d0","d1")
& ~ ssSkP614("d2","d2")
& ssSkP614("d1","d1")
& ssSkP614("d0","d0")
& ~ ssSkP613("d2","d2")
& ssSkP613("d1","d1")
& ssSkP613("d0","d0")
& ssSkP614("d0","d1")
& ssSkP614("d1","d0")
& ssSkP960("d0")
& ssSkP960("d1")
& ~ ssSkP960("d2")
& ssSkP964("d0")
& ssSkP963("d1")
& ~ ssSkP962("d2")
& ssSkP964("d1")
& ssSkP963("d0")
& ~ ssSkP961("d2")
& ~ ssSkP964("d2")
& ssSkP962("d0")
& ssSkP961("d1")
& ~ ssSkP963("d2")
& ssSkP962("d1")
& ssSkP961("d0")
& ssSkP989("d1")
& ~ ssSkP988("d2")
& ssSkP989("d0")
& ~ ssSkP987("d2")
& ssSkP988("d0")
& ssSkP987("d1")
& ~ ssSkP989("d2")
& ssSkP988("d1")
& ssSkP987("d0")
& ssSkP993("d0")
& ssSkP992("d1")
& ~ ssSkP991("d2")
& ssSkP993("d1")
& ssSkP992("d0")
& ~ ssSkP990("d2")
& ~ ssSkP993("d2")
& ssSkP991("d0")
& ssSkP990("d1")
& ~ ssSkP992("d2")
& ssSkP991("d1")
& ssSkP990("d0")
& ~ ssSkP997("d0")
& ~ ssSkP994("d2")
& ~ ssSkP997("d1")
& ~ ssSkP994("d1")
& ~ ssSkP997("d2")
& ssSkP994("d0")
& ~ ssSkP999("d2")
& ~ ssSkP998("d2")
& ~ ssSkP999("d0")
& ~ ssSkP998("d1")
& ~ ssSkP999("d1")
& ~ ssSkP998("d0")
& ~ ssSkP557("d2","d2")
& ssSkP557("d1","d1")
& ssSkP557("d0","d0")
& ssSkP557("d1","d0")
& ssSkP557("d0","d1")
& ~ ssSkP557("d2","d0")
& ~ ssSkP557("d0","d2")
& ~ ssSkP557("d2","d1")
& ~ ssSkP557("d1","d2")
& ssSkP558("d1","d2")
& ~ ssSkP558("d2","d1")
& ssSkP558("d0","d2")
& ~ ssSkP558("d2","d0")
& ssSkP558("d0","d1")
& ssSkP558("d1","d0")
& ~ ssSkP558("d2","d2")
& ssSkP558("d1","d1")
& ssSkP558("d0","d0")
& ~ ssRr("d0","d2")
& ~ ssRr("d2","d0")
& ~ ssRr("d1","d2")
& ~ ssRr("d2","d1")
& ~ ssRr("d2","d2")
& ssRr("d1","d1")
& ~ ssRr("d0","d0")
& ssRr("d0","d1")
& ssRr("d1","d0")
& ~ ssSkP735("d2","d0")
& ~ ssSkP735("d0","d2")
& ssSkP736("d0","d1")
& ssSkP736("d1","d0")
& ~ ssSkP735("d2","d1")
& ~ ssSkP735("d1","d2")
& ~ ssSkP736("d2","d2")
& ssSkP736("d1","d1")
& ssSkP736("d0","d0")
& ~ ssSkP735("d2","d2")
& ssSkP735("d1","d1")
& ssSkP735("d0","d0")
& ~ ssSkP736("d1","d2")
& ~ ssSkP736("d2","d1")
& ssSkP735("d1","d0")
& ssSkP735("d0","d1")
& ~ ssSkP736("d0","d2")
& ~ ssSkP736("d2","d0")
& ~ ssSkP889("d2")
& ~ ssSkP888("d2")
& ~ ssSkP889("d0")
& ~ ssSkP888("d1")
& ~ ssSkP889("d1")
& ~ ssSkP888("d0")
& ~ ssSkP890("d0")
& ~ ssSkP890("d1")
& ~ ssSkP890("d2")
& ~ ssSkP894("d0")
& ~ ssSkP893("d1")
& ~ ssSkP892("d2")
& ~ ssSkP894("d1")
& ~ ssSkP893("d0")
& ~ ssSkP891("d2")
& ~ ssSkP894("d2")
& ~ ssSkP892("d0")
& ~ ssSkP891("d1")
& ~ ssSkP893("d2")
& ~ ssSkP892("d1")
& ~ ssSkP891("d0")
& ~ ssSkP898("d0")
& ~ ssSkP897("d1")
& ~ ssSkP896("d2")
& ~ ssSkP898("d1")
& ~ ssSkP897("d0")
& ~ ssSkP895("d2")
& ~ ssSkP898("d2")
& ~ ssSkP896("d0")
& ~ ssSkP895("d1")
& ~ ssSkP897("d2")
& ~ ssSkP896("d1")
& ~ ssSkP895("d0")
& ~ ssSkP899("d2")
& ~ ssSkP899("d1")
& ~ ssSkP899("d0")
& ~ ssSkP768("d2","d0")
& ~ ssSkP768("d0","d2")
& ssSkP769("d0","d1")
& ssSkP769("d1","d0")
& ~ ssSkP768("d2","d1")
& ~ ssSkP768("d1","d2")
& ~ ssSkP769("d2","d2")
& ssSkP769("d1","d1")
& ssSkP769("d0","d0")
& ~ ssSkP768("d2","d2")
& ssSkP768("d1","d1")
& ssSkP768("d0","d0")
& ~ ssSkP769("d1","d2")
& ~ ssSkP769("d2","d1")
& ssSkP768("d1","d0")
& ssSkP768("d0","d1")
& ~ ssSkP769("d0","d2")
& ~ ssSkP769("d2","d0")
& ~ ssSkP887("d0")
& ~ ssSkP887("d1")
& ~ ssSkP887("d2")
& ~ ssSkP789("d2")
& ~ ssSkP789("d1")
& ~ ssSkP789("d0")
& ~ ssSkP791("d0")
& ~ ssSkP790("d1")
& ~ ssSkP791("d1")
& ~ ssSkP790("d0")
& ~ ssSkP791("d2")
& ~ ssSkP790("d2")
& ~ ssSkP793("d2")
& ~ ssSkP794("d1")
& ~ ssSkP794("d0")
& ~ ssSkP792("d2")
& ~ ssSkP793("d0")
& ~ ssSkP792("d1")
& ~ ssSkP793("d1")
& ssSkP794("d2")
& ~ ssSkP792("d0")
& ssSkP1153("d1","d0")
& ssSkP1153("d0","d1")
& ~ ssSkP1153("d2","d2")
& ssSkP1153("d1","d1")
& ssSkP1153("d0","d0")
& ~ ssSkP1153("d2","d1")
& ~ ssSkP1153("d1","d2")
& ~ ssSkP1153("d2","d0")
& ~ ssSkP1153("d0","d2")
& ssSkP1166("d1","d2")
& ~ ssSkP1166("d2","d1")
& ssSkP1166("d0","d2")
& ~ ssSkP1166("d2","d0")
& ssSkP1166("d0","d1")
& ssSkP1166("d1","d0")
& ~ ssSkP1166("d2","d2")
& ssSkP1166("d1","d1")
& ssSkP1166("d0","d0") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN911-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.36 % Computer : n005.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 : Fri Sep 25 02:32:34 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.18/0.50 Running: java -jar /export/starexec/sandbox/solver/bin/FMB4J.jar /export/starexec/sandbox/tmp/tmp.YIvDUX7Rz9/theBenchmark.cnf 300
% 1.13/0.98 % domain size: 1
% 1.71/1.12 % domain size: 2
% 2.83/1.36 % domain size: 3
% 4.87/1.82 % model found for domain size 3
% 4.87/1.83 % SZS status CounterSatisfiable for theBenchmark
% 4.87/1.83 % SZS output start FiniteModel for theBenchmark
% See solution above
% 5.88/2.07 % FMB4L exiting
%------------------------------------------------------------------------------