↑ Up

FMB4J---0.1.SAT-FMo.s

View TPTP
Problem
Process solution in
SystemOnTSTP
Download .tgz
%------------------------------------------------------------------------------
% File     : FMB4J---0.1
% Problem  : SYN913-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300

% Computer : n014.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 7.87s 7.82s
% Output   : FiniteModel 9.67s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
fof(domain,interpretation-domains,
    ! [X] :
      ( X = "d2"
      | X = "d1"
      | X = "d0" ) ).

fof(mappings,interpretation-mappings,
    ( skf35("d0") = "d1"
    & skf38("d2") = "d0"
    & skf37("d2") = "d0"
    & skf35("d1") = "d1"
    & skf36("d1") = "d0"
    & skf36("d0") = "d2"
    & skf37("d0") = "d1"
    & skf36("d2") = "d0"
    & skf38("d0") = "d0"
    & skf37("d1") = "d0"
    & skf38("d1") = "d0"
    & skf35("d2") = "d0"
    & skf39("d1") = "d0"
    & skf39("d0") = "d0"
    & skf39("d2") = "d0"
    & skf63("d2") = "d0"
    & skf61("d1") = "d1"
    & skf60("d0") = "d1"
    & skf62("d2") = "d0"
    & skf61("d0") = "d1"
    & skf60("d1") = "d1"
    & skf63("d1") = "d1"
    & skf62("d0") = "d1"
    & skf61("d2") = "d0"
    & skf63("d0") = "d1"
    & skf60("d2") = "d0"
    & skf62("d1") = "d1"
    & skf67("d2") = "d0"
    & skf65("d1") = "d1"
    & skf64("d0") = "d1"
    & skf66("d2") = "d0"
    & skf65("d0") = "d1"
    & skf64("d1") = "d1"
    & skf67("d1") = "d1"
    & skf66("d0") = "d1"
    & skf65("d2") = "d0"
    & skf67("d0") = "d1"
    & skf66("d1") = "d1"
    & skf64("d2") = "d0"
    & skf69("d1") = "d1"
    & skf68("d0") = "d1"
    & skf69("d0") = "d1"
    & skf68("d1") = "d1"
    & skf69("d2") = "d1"
    & skf68("d2") = "d0"
    & skf41("d2") = "d0"
    & skf40("d2") = "d0"
    & skf40("d1") = "d0"
    & skf41("d0") = "d1"
    & skf41("d1") = "d0"
    & skf40("d0") = "d0"
    & skf43("d0") = "d0"
    & skf45("d2") = "d0"
    & skf42("d1") = "d0"
    & skf43("d1") = "d0"
    & skf42("d0") = "d0"
    & skf44("d2") = "d0"
    & skf43("d2") = "d0"
    & skf45("d1") = "d1"
    & skf45("d0") = "d0"
    & skf42("d2") = "d0"
    & skf44("d1") = "d1"
    & skf44("d0") = "d0"
    & skf49("d2") = "d0"
    & skf47("d1") = "d1"
    & skf47("d0") = "d0"
    & skf48("d2") = "d0"
    & skf46("d1") = "d1"
    & skf46("d0") = "d0"
    & skf49("d0") = "d0"
    & skf49("d1") = "d1"
    & skf47("d2") = "d0"
    & skf48("d1") = "d1"
    & skf48("d0") = "d0"
    & skf46("d2") = "d0"
    & skf52("d2") = "d0"
    & skf50("d1") = "d1"
    & skf50("d0") = "d0"
    & skf51("d2") = "d0"
    & skf52("d1") = "d1"
    & skf50("d2") = "d0"
    & skf52("d0") = "d1"
    & skf51("d1") = "d1"
    & skf51("d0") = "d0"
    & skf56("d2") = "d0"
    & skf54("d1") = "d1"
    & skf53("d0") = "d1"
    & skf55("d2") = "d0"
    & skf54("d0") = "d1"
    & skf53("d1") = "d1"
    & skf55("d0") = "d1"
    & skf56("d1") = "d1"
    & skf54("d2") = "d0"
    & skf55("d1") = "d1"
    & skf56("d0") = "d1"
    & skf53("d2") = "d0"
    & skf58("d1") = "d1"
    & skf57("d0") = "d1"
    & skf59("d2") = "d0"
    & skf57("d1") = "d1"
    & skf58("d0") = "d1"
    & skf59("d0") = "d1"
    & skf58("d2") = "d0"
    & skf59("d1") = "d1"
    & skf57("d2") = "d0"
    & skc59 = "d2"
    & skc58 = "d2"
    & skc57 = "d2"
    & skc56 = "d2"
    & skc55 = "d2"
    & skc54 = "d2"
    & skc53 = "d2"
    & skc52 = "d2"
    & skc51 = "d2"
    & skc100 = "d2"
    & skc101 = "d0"
    & skc69 = "d2"
    & skc68 = "d2"
    & skc67 = "d2"
    & skc66 = "d2"
    & skc65 = "d2"
    & skc64 = "d2"
    & skc63 = "d2"
    & skc62 = "d2"
    & skc61 = "d2"
    & skc60 = "d2"
    & skc79 = "d2"
    & skc78 = "d2"
    & skc77 = "d2"
    & skc76 = "d2"
    & skc75 = "d2"
    & skc74 = "d2"
    & skc73 = "d2"
    & skc72 = "d2"
    & skc71 = "d2"
    & skc70 = "d2"
    & skc89 = "d2"
    & skc88 = "d2"
    & skc87 = "d2"
    & skc86 = "d2"
    & skc85 = "d2"
    & skc84 = "d2"
    & skc83 = "d2"
    & skc82 = "d2"
    & skc81 = "d2"
    & skc80 = "d2"
    & skc99 = "d2"
    & skc98 = "d2"
    & skc97 = "d2"
    & skc96 = "d2"
    & skc95 = "d2"
    & skc94 = "d2"
    & skc93 = "d2"
    & skc92 = "d2"
    & skc91 = "d2"
    & skc90 = "d2" ) ).

fof(predicate_mappings,interpretation-mappings,
    ( ~ ssPv20("d2")
    & ssPv20("d1")
    & ~ ssPv20("d0")
    & ~ ssPv14("d2")
    & ssPv15("d1")
    & ~ ssPv16("d0")
    & ~ ssPv13("d2")
    & ~ ssPv15("d0")
    & ssPv16("d1")
    & ssPv13("d1")
    & ~ ssPv14("d0")
    & ~ ssPv16("d2")
    & ~ ssPv13("d0")
    & ssPv14("d1")
    & ~ ssPv15("d2")
    & ~ ssPv19("d1")
    & ~ ssPv18("d2")
    & ~ ssPv19("d0")
    & ~ ssPv17("d2")
    & ~ ssPv18("d0")
    & ssPv17("d1")
    & ~ ssPv19("d2")
    & ~ ssPv18("d1")
    & ssPv17("d0")
    & ssPv11("d1")
    & ssPv12("d0")
    & ~ ssPv10("d2")
    & ssPv11("d0")
    & ssPv12("d1")
    & ~ ssPv12("d2")
    & ssPv10("d0")
    & ~ ssPv11("d2")
    & ssPv10("d1")
    & ssSkP300("d1")
    & ssSkP300("d0")
    & ~ ssSkP300("d2")
    & ssSkP301("d2")
    & ~ ssSkP304("d1")
    & ~ ssSkP304("d0")
    & ~ ssSkP301("d0")
    & ~ ssSkP301("d1")
    & ~ ssSkP304("d2")
    & ~ ssSkP417("d2","d2")
    & ssSkP417("d1","d1")
    & ssSkP417("d0","d0")
    & ssSkP418("d0","d1")
    & ssSkP418("d1","d0")
    & ssSkP417("d1","d0")
    & ssSkP417("d0","d1")
    & ~ ssSkP418("d2","d2")
    & ssSkP418("d1","d1")
    & ssSkP418("d0","d0")
    & ~ ssSkP417("d2","d0")
    & ~ ssSkP417("d0","d2")
    & ~ ssSkP418("d1","d2")
    & ~ ssSkP418("d2","d1")
    & ~ ssSkP417("d2","d1")
    & ~ ssSkP417("d1","d2")
    & ~ ssSkP418("d0","d2")
    & ~ ssSkP418("d2","d0")
    & ~ ssSkP209("d1")
    & ~ ssSkP208("d0")
    & ~ ssSkP206("d2")
    & ~ ssSkP209("d0")
    & ~ ssSkP208("d1")
    & ~ ssSkP207("d2")
    & ~ ssSkP208("d2")
    & ~ ssSkP206("d0")
    & ~ ssSkP207("d1")
    & ~ ssSkP209("d2")
    & ssSkP206("d1")
    & ~ ssSkP207("d0")
    & ssSkP1076("d1","d0")
    & ssSkP1076("d0","d1")
    & ~ ssSkP212("d1")
    & ~ ssSkP211("d0")
    & ~ ssSkP1076("d2","d2")
    & ssSkP1076("d1","d1")
    & ssSkP1076("d0","d0")
    & ~ ssSkP212("d0")
    & ~ ssSkP211("d1")
    & ~ ssSkP210("d2")
    & ~ ssSkP1076("d2","d1")
    & ~ ssSkP1076("d1","d2")
    & ~ ssSkP211("d2")
    & ~ ssSkP210("d1")
    & ~ ssSkP1076("d2","d0")
    & ~ ssSkP1076("d0","d2")
    & ~ ssSkP212("d2")
    & ~ ssSkP210("d0")
    & ~ ssSkP213("d2")
    & ~ ssSkP215("d0")
    & ~ ssSkP214("d2")
    & ~ ssSkP215("d1")
    & ~ ssSkP214("d1")
    & ~ ssSkP213("d0")
    & ssSkP215("d2")
    & ~ ssSkP214("d0")
    & ~ ssSkP213("d1")
    & ssSkP219("d0")
    & ssSkP219("d1")
    & ~ ssSkP218("d2")
    & ~ ssSkP219("d2")
    & ~ ssSkP218("d1")
    & ssSkP218("d0")
    & ssSkP222("d0")
    & ssSkP223("d1")
    & ~ ssSkP220("d2")
    & ssSkP222("d1")
    & ssSkP223("d0")
    & ~ 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")
    & ssSkP1085("d1","d2")
    & ~ ssSkP1085("d2","d1")
    & ~ ssSkP201("d1")
    & ~ ssSkP200("d0")
    & ssSkP1085("d0","d2")
    & ~ ssSkP1085("d2","d0")
    & ~ ssSkP201("d0")
    & ~ ssSkP200("d1")
    & ssSkP1085("d0","d1")
    & ssSkP1085("d1","d0")
    & ~ ssSkP200("d2")
    & ~ ssSkP1085("d2","d2")
    & ssSkP1085("d1","d1")
    & ssSkP1085("d0","d0")
    & ~ 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")
    & ssSkP352("d0","d2")
    & ~ ssSkP352("d2","d0")
    & ~ ssSkP252("d1")
    & ~ ssSkP251("d0")
    & ssSkP352("d1","d2")
    & ~ ssSkP352("d2","d1")
    & ~ ssSkP252("d0")
    & ~ ssSkP251("d1")
    & ~ ssSkP250("d2")
    & ~ ssSkP352("d2","d2")
    & ssSkP352("d1","d1")
    & ssSkP352("d0","d0")
    & ~ ssSkP251("d2")
    & ~ ssSkP250("d1")
    & ssSkP352("d0","d1")
    & ssSkP352("d1","d0")
    & ~ ssSkP252("d2")
    & ~ ssSkP250("d0")
    & ssSkP351("d1","d0")
    & ssSkP351("d0","d1")
    & ~ ssSkP256("d1")
    & ~ ssSkP255("d0")
    & ~ ssSkP253("d2")
    & ~ ssSkP351("d2","d2")
    & ssSkP351("d1","d1")
    & ssSkP351("d0","d0")
    & ~ ssSkP256("d0")
    & ~ ssSkP255("d1")
    & ~ ssSkP254("d2")
    & ~ ssSkP351("d2","d1")
    & ~ ssSkP351("d1","d2")
    & ~ ssSkP255("d2")
    & ~ ssSkP254("d1")
    & ~ ssSkP253("d0")
    & ~ ssSkP351("d2","d0")
    & ~ ssSkP351("d0","d2")
    & ~ ssSkP256("d2")
    & ~ ssSkP254("d0")
    & ~ ssSkP253("d1")
    & ~ ssSkP259("d0")
    & ~ ssSkP257("d2")
    & ~ ssSkP259("d1")
    & ~ ssSkP258("d2")
    & ~ ssSkP259("d2")
    & ~ ssSkP258("d1")
    & ~ ssSkP257("d0")
    & ~ ssSkP258("d0")
    & ~ ssSkP257("d1")
    & ~ ssSkC4
    & ~ ssSkC3
    & ~ ssSkC6
    & ~ ssSkC5
    & ~ ssSkC8
    & ~ ssSkC7
    & ~ ssSkC9
    & ~ ssSkC0
    & ~ ssSkC2
    & ~ ssSkC1
    & ~ ssSkP1028("d2","d0")
    & ~ ssSkP1028("d0","d2")
    & ssSkP1029("d0","d1")
    & ssSkP1029("d1","d0")
    & ~ ssSkP1028("d2","d1")
    & ~ ssSkP1028("d1","d2")
    & ~ ssSkP1029("d2","d2")
    & ssSkP1029("d1","d1")
    & ssSkP1029("d0","d0")
    & ~ ssSkP1028("d2","d2")
    & ssSkP1028("d1","d1")
    & ssSkP1028("d0","d0")
    & ssSkP1029("d1","d2")
    & ~ ssSkP1029("d2","d1")
    & ssSkP1028("d1","d0")
    & ssSkP1028("d0","d1")
    & ssSkP1029("d0","d2")
    & ~ ssSkP1029("d2","d0")
    & ~ ssSkP260("d2")
    & ssSkP261("d2")
    & ~ ssSkP260("d0")
    & ~ ssSkP261("d1")
    & ~ ssSkP260("d1")
    & ~ ssSkP261("d0")
    & ~ ssSkP267("d1")
    & ~ ssSkP266("d0")
    & ~ ssSkP264("d2")
    & ~ ssSkP267("d0")
    & ~ ssSkP266("d1")
    & ~ ssSkP265("d2")
    & ~ ssSkP266("d2")
    & ~ ssSkP265("d1")
    & ~ 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")
    & ~ ssSkP376("d2","d2")
    & ssSkP376("d1","d1")
    & ssSkP376("d0","d0")
    & ssSkP377("d0","d1")
    & ssSkP377("d1","d0")
    & ssSkP230("d1")
    & ssSkP376("d1","d0")
    & ssSkP376("d0","d1")
    & ~ ssSkP377("d2","d2")
    & ssSkP377("d1","d1")
    & ssSkP377("d0","d0")
    & ssSkP230("d0")
    & ~ ssSkP376("d2","d0")
    & ~ ssSkP376("d0","d2")
    & ~ ssSkP377("d1","d2")
    & ~ ssSkP377("d2","d1")
    & ~ ssSkP376("d2","d1")
    & ~ ssSkP376("d1","d2")
    & ~ ssSkP377("d0","d2")
    & ~ ssSkP377("d2","d0")
    & ~ ssSkP230("d2")
    & ~ ssSkP1053("d2","d0")
    & ~ ssSkP1053("d0","d2")
    & ssSkP1054("d0","d1")
    & ssSkP1054("d1","d0")
    & ssSkP234("d1")
    & ssSkP233("d0")
    & ~ ssSkP231("d2")
    & ~ ssSkP1053("d2","d1")
    & ~ ssSkP1053("d1","d2")
    & ~ ssSkP1054("d2","d2")
    & ssSkP1054("d1","d1")
    & ssSkP1054("d0","d0")
    & ssSkP234("d0")
    & ssSkP233("d1")
    & ~ ssSkP232("d2")
    & ~ ssSkP1053("d2","d2")
    & ssSkP1053("d1","d1")
    & ssSkP1053("d0","d0")
    & ssSkP1054("d1","d2")
    & ~ ssSkP1054("d2","d1")
    & ~ ssSkP233("d2")
    & ssSkP232("d1")
    & ssSkP231("d0")
    & ssSkP1053("d1","d0")
    & ssSkP1053("d0","d1")
    & ssSkP1054("d0","d2")
    & ~ ssSkP1054("d2","d0")
    & ~ ssSkP234("d2")
    & ssSkP232("d0")
    & ssSkP231("d1")
    & ~ ssSkP235("d2")
    & ~ ssSkP237("d0")
    & ~ ssSkP236("d2")
    & ~ ssSkP237("d1")
    & ssSkP236("d1")
    & ssSkP235("d0")
    & ssSkP237("d2")
    & ssSkP236("d0")
    & ssSkP235("d1")
    & ~ ssSkP241("d1")
    & ~ ssSkP240("d0")
    & ~ ssSkP241("d0")
    & ~ ssSkP240("d1")
    & ~ ssSkP240("d2")
    & ~ ssSkP241("d2")
    & ~ ssSkP245("d1")
    & ~ ssSkP244("d0")
    & ~ ssSkP242("d2")
    & ~ ssSkP245("d0")
    & ~ ssSkP243("d2")
    & ~ ssSkP244("d1")
    & ~ ssSkP243("d1")
    & ~ ssSkP244("d2")
    & ~ ssSkP242("d0")
    & ~ ssSkP245("d2")
    & ssSkP243("d0")
    & ~ ssSkP242("d1")
    & ~ ssSkP249("d1")
    & ~ ssSkP248("d0")
    & ~ ssSkP246("d2")
    & ~ ssSkP249("d0")
    & ~ ssSkP248("d1")
    & ~ ssSkP247("d2")
    & ~ ssSkP248("d2")
    & ssSkP246("d0")
    & ~ ssSkP247("d1")
    & ~ ssSkP249("d2")
    & ~ ssSkP246("d1")
    & ~ ssSkP247("d0")
    & ssSkP292("d1")
    & ssSkP291("d0")
    & ssSkP292("d0")
    & ~ ssSkP290("d2")
    & ssSkP291("d1")
    & ssSkP290("d1")
    & ~ ssSkP291("d2")
    & ~ ssSkP292("d2")
    & ssSkP290("d0")
    & ssSkP295("d0")
    & ssSkP296("d1")
    & ~ ssSkP293("d2")
    & ssSkP295("d1")
    & ssSkP296("d0")
    & ~ ssSkP294("d2")
    & ~ ssSkP295("d2")
    & ~ ssSkP294("d1")
    & ssSkP293("d0")
    & ~ ssSkP296("d2")
    & ssSkP294("d0")
    & ssSkP293("d1")
    & ~ ssSkP392("d2","d0")
    & ~ ssSkP392("d0","d2")
    & ssSkP393("d1","d2")
    & ssSkP299("d0")
    & ~ ssSkP297("d2")
    & ~ ssSkP393("d2","d1")
    & ~ ssSkP392("d2","d1")
    & ~ ssSkP392("d1","d2")
    & ~ ssSkP393("d2","d0")
    & ssSkP299("d1")
    & ~ ssSkP298("d2")
    & ssSkP393("d0","d2")
    & ~ ssSkP392("d2","d2")
    & ssSkP392("d0","d0")
    & ssSkP392("d1","d1")
    & ssSkP393("d0","d1")
    & ssSkP393("d1","d0")
    & ~ ssSkP299("d2")
    & ssSkP297("d0")
    & ssSkP298("d1")
    & ssSkP392("d0","d1")
    & ~ ssSkP393("d2","d2")
    & ssSkP393("d1","d1")
    & ssSkP393("d0","d0")
    & ssSkP392("d1","d0")
    & ssSkP297("d1")
    & ssSkP298("d0")
    & ssSkP1009("d1","d2")
    & ~ ssSkP1009("d2","d1")
    & ssSkP1009("d0","d2")
    & ~ ssSkP1009("d2","d0")
    & ssSkP1009("d0","d1")
    & ssSkP1009("d1","d0")
    & ~ ssSkP1009("d2","d2")
    & ssSkP1009("d1","d1")
    & ssSkP1009("d0","d0")
    & ~ ssSkP270("d1")
    & ~ ssSkP270("d0")
    & ~ ssSkP270("d2")
    & ~ ssSkP274("d1")
    & ~ ssSkP273("d0")
    & ~ ssSkP271("d2")
    & ~ ssSkP274("d0")
    & ~ ssSkP273("d1")
    & ~ ssSkP272("d2")
    & ~ ssSkP273("d2")
    & ~ ssSkP272("d1")
    & ~ ssSkP271("d0")
    & ~ ssSkP274("d2")
    & ~ ssSkP272("d0")
    & ~ ssSkP271("d1")
    & ~ ssSkP278("d1")
    & ~ ssSkP277("d0")
    & ~ ssSkP275("d2")
    & ~ ssSkP278("d0")
    & ~ ssSkP277("d1")
    & ~ ssSkP276("d2")
    & ~ ssSkP277("d2")
    & ~ ssSkP276("d1")
    & ~ ssSkP275("d0")
    & ~ ssSkP278("d2")
    & ~ ssSkP276("d0")
    & ~ ssSkP275("d1")
    & ~ ssSkP279("d2")
    & ~ ssSkP279("d0")
    & ~ ssSkP279("d1")
    & ~ ssSkP1008("d2","d2")
    & ssSkP1008("d1","d1")
    & ssSkP1008("d0","d0")
    & ssSkP281("d1")
    & ssSkP280("d0")
    & ssSkP1008("d1","d0")
    & ssSkP1008("d0","d1")
    & ssSkP281("d0")
    & ssSkP280("d1")
    & ~ ssSkP1008("d2","d0")
    & ~ ssSkP1008("d0","d2")
    & ~ ssSkP280("d2")
    & ~ ssSkP1008("d2","d1")
    & ~ ssSkP1008("d1","d2")
    & ~ ssSkP281("d2")
    & ssSkP282("d2")
    & ~ ssSkP285("d1")
    & ~ ssSkP285("d0")
    & ~ ssSkP282("d0")
    & ~ ssSkP282("d1")
    & ~ ssSkP285("d2")
    & ~ ssSkP289("d1")
    & ~ ssSkP288("d0")
    & ~ ssSkP286("d2")
    & ~ ssSkP289("d0")
    & ~ ssSkP288("d1")
    & ~ ssSkP287("d2")
    & ~ ssSkP288("d2")
    & ~ ssSkP287("d1")
    & ~ ssSkP286("d0")
    & ~ ssSkP289("d2")
    & ~ ssSkP287("d0")
    & ~ ssSkP286("d1")
    & ~ ssSkC50
    & 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")
    & ~ ssSkC39
    & ~ ssSkC38
    & ~ ssSkC35
    & ~ ssSkC34
    & ~ ssSkC37
    & ~ ssSkC36
    & ~ ssSkC31
    & ~ ssSkC30
    & ~ ssSkC33
    & ~ ssSkC32
    & ~ ssSkC49
    & ~ ssSkP500("d2","d1")
    & ~ ssSkP500("d1","d2")
    & ~ ssSkP501("d2","d2")
    & ssSkP501("d1","d1")
    & ssSkP501("d0","d0")
    & ~ ssSkC46
    & ~ ssSkP500("d2","d0")
    & ~ ssSkP500("d0","d2")
    & ssSkP501("d0","d1")
    & ssSkP501("d1","d0")
    & ~ ssSkC45
    & ssSkP500("d1","d0")
    & ssSkP500("d0","d1")
    & ssSkP501("d0","d2")
    & ~ ssSkP501("d2","d0")
    & ~ ssSkC48
    & ~ ssSkP500("d2","d2")
    & ssSkP500("d1","d1")
    & ssSkP500("d0","d0")
    & ssSkP501("d1","d2")
    & ~ ssSkP501("d2","d1")
    & ~ ssSkC47
    & ~ ssSkC42
    & ~ ssSkC41
    & ~ ssSkC44
    & ~ ssSkC43
    & ~ ssSkC40
    & ~ ssSkP519("d2","d1")
    & ~ ssSkP519("d1","d2")
    & ~ ssSkP519("d2","d0")
    & ~ ssSkP519("d0","d2")
    & ssSkP519("d1","d0")
    & ssSkP519("d0","d1")
    & ~ ssSkP519("d2","d2")
    & ssSkP519("d1","d1")
    & ssSkP519("d0","d0")
    & ssSkP520("d0","d1")
    & ssSkP520("d1","d0")
    & ~ ssSkP520("d2","d2")
    & ssSkP520("d1","d1")
    & ssSkP520("d0","d0")
    & ssSkP520("d1","d2")
    & ~ ssSkP520("d2","d1")
    & ssSkP520("d0","d2")
    & ~ ssSkP520("d2","d0")
    & ~ ssSkP538("d2","d2")
    & ssSkP538("d1","d1")
    & ssSkP538("d0","d0")
    & ssSkP539("d0","d1")
    & ssSkP539("d1","d0")
    & ssSkP538("d1","d0")
    & ssSkP538("d0","d1")
    & ~ ssSkP539("d2","d2")
    & ssSkP539("d1","d1")
    & ssSkP539("d0","d0")
    & ~ ssSkP538("d2","d0")
    & ~ ssSkP538("d0","d2")
    & ~ ssSkP539("d1","d2")
    & ~ ssSkP539("d2","d1")
    & ~ ssSkP538("d2","d1")
    & ~ ssSkP538("d1","d2")
    & ~ ssSkP539("d0","d2")
    & ~ ssSkP539("d2","d0")
    & ~ ssSkP438("d2","d1")
    & ~ ssSkP438("d1","d2")
    & ~ ssSkP439("d2","d2")
    & ssSkP439("d1","d1")
    & ssSkP439("d0","d0")
    & ~ ssSkP438("d2","d0")
    & ~ ssSkP438("d0","d2")
    & ssSkP439("d0","d1")
    & ssSkP439("d1","d0")
    & ssSkP438("d1","d0")
    & ssSkP438("d0","d1")
    & ssSkP439("d0","d2")
    & ~ ssSkP439("d2","d0")
    & ~ ssSkP438("d2","d2")
    & ssSkP438("d1","d1")
    & ssSkP438("d0","d0")
    & ssSkP439("d1","d2")
    & ~ ssSkP439("d2","d1")
    & ssSkP102("d1")
    & ssSkP101("d0")
    & ~ ssSkP102("d0")
    & ssSkP101("d1")
    & ~ ssSkP100("d2")
    & ~ ssSkP101("d2")
    & ssSkP100("d1")
    & ~ ssSkP102("d2")
    & ssSkP100("d0")
    & ssSkP106("d1")
    & ssSkP105("d0")
    & ~ ssSkP103("d2")
    & ssSkP106("d0")
    & ssSkP105("d1")
    & ~ ssSkP104("d2")
    & ~ ssSkP105("d2")
    & ssSkP103("d0")
    & ssSkP104("d1")
    & ~ ssSkP106("d2")
    & ssSkP103("d1")
    & ssSkP104("d0")
    & ~ ssSkP457("d2","d2")
    & ssSkP457("d1","d1")
    & ssSkP457("d0","d0")
    & ssSkP458("d0","d1")
    & ssSkP458("d1","d0")
    & ssSkP457("d1","d0")
    & ssSkP457("d0","d1")
    & ~ ssSkP458("d2","d2")
    & ssSkP458("d1","d1")
    & ssSkP458("d0","d0")
    & ~ ssSkP457("d2","d0")
    & ~ ssSkP457("d0","d2")
    & ssSkP458("d1","d2")
    & ~ ssSkP458("d2","d1")
    & ~ ssSkP457("d2","d1")
    & ~ ssSkP457("d1","d2")
    & ssSkP458("d0","d2")
    & ~ ssSkP458("d2","d0")
    & ssSkP129("d2")
    & ~ ssSkP129("d0")
    & ~ ssSkP129("d1")
    & ~ ssSkC17
    & ~ ssSkC16
    & ~ ssSkC19
    & ~ ssSkC18
    & ssSkP477("d0","d2")
    & ~ ssSkP477("d2","d0")
    & ~ ssSkC13
    & ssSkP477("d1","d2")
    & ~ ssSkP477("d2","d1")
    & ~ ssSkC12
    & ~ ssSkP477("d2","d2")
    & ssSkP477("d1","d1")
    & ssSkP477("d0","d0")
    & ~ ssSkC15
    & ssSkP477("d0","d1")
    & ssSkP477("d1","d0")
    & ~ ssSkC14
    & ssSkP476("d1","d0")
    & ssSkP476("d0","d1")
    & ~ ssSkP476("d2","d2")
    & ssSkP476("d1","d1")
    & ssSkP476("d0","d0")
    & ~ ssSkP476("d2","d1")
    & ~ ssSkP476("d1","d2")
    & ~ ssSkC11
    & ~ ssSkP476("d2","d0")
    & ~ ssSkP476("d0","d2")
    & ~ ssSkC10
    & ~ ssSkP135("d1")
    & ~ ssSkP134("d0")
    & ~ ssSkP132("d2")
    & ~ ssSkP135("d0")
    & ~ ssSkP134("d1")
    & ~ ssSkP133("d2")
    & ~ ssSkP134("d2")
    & ~ ssSkP133("d1")
    & ~ ssSkP132("d0")
    & ~ ssSkP135("d2")
    & ~ ssSkP133("d0")
    & ~ ssSkP132("d1")
    & ~ ssSkP138("d0")
    & ~ ssSkP139("d1")
    & ~ ssSkP136("d2")
    & ~ ssSkP138("d1")
    & ~ ssSkP139("d0")
    & ~ ssSkP137("d2")
    & ~ ssSkP138("d2")
    & ~ ssSkP137("d1")
    & ~ ssSkP136("d0")
    & ~ ssSkP139("d2")
    & ~ ssSkP137("d0")
    & ~ ssSkP136("d1")
    & ~ ssSkC28
    & ~ ssSkC27
    & ~ ssSkC29
    & ~ ssSkC24
    & ~ ssSkC23
    & ~ ssSkC26
    & ~ ssSkC25
    & ~ ssSkC20
    & ~ ssSkP142("d1")
    & ~ ssSkP141("d0")
    & ~ ssSkP142("d0")
    & ~ ssSkP141("d1")
    & ~ ssSkP140("d2")
    & ~ ssSkC22
    & ~ ssSkP141("d2")
    & ~ ssSkP140("d1")
    & ~ ssSkC21
    & ~ ssSkP142("d2")
    & ~ ssSkP140("d0")
    & ssSkP146("d1")
    & ssSkP145("d0")
    & ~ ssSkP143("d2")
    & ssSkP146("d0")
    & ssSkP145("d1")
    & ~ ssSkP144("d2")
    & ~ ssSkP145("d2")
    & ssSkP143("d0")
    & ssSkP144("d1")
    & ~ ssSkP146("d2")
    & ssSkP143("d1")
    & ssSkP144("d0")
    & ssSkP147("d2")
    & ~ ssSkP147("d0")
    & ~ ssSkP147("d1")
    & ssSkP109("d0")
    & ~ ssSkP107("d2")
    & ~ ssSkP108("d2")
    & ssSkP109("d1")
    & ~ ssSkP109("d2")
    & ssSkP108("d1")
    & ssSkP107("d0")
    & ~ ssSkP108("d0")
    & ssSkP107("d1")
    & ssSkP110("d2")
    & ~ ssSkP113("d1")
    & ~ ssSkP113("d0")
    & ~ ssSkP110("d0")
    & ~ ssSkP110("d1")
    & ~ ssSkP113("d2")
    & ~ ssSkP117("d1")
    & ~ ssSkP116("d0")
    & ~ ssSkP114("d2")
    & ~ ssSkP117("d0")
    & ~ ssSkP116("d1")
    & ~ ssSkP115("d2")
    & ~ ssSkP116("d2")
    & ~ ssSkP114("d0")
    & ~ ssSkP115("d1")
    & ~ ssSkP117("d2")
    & ~ ssSkP114("d1")
    & ~ ssSkP115("d0")
    & ~ 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")
    & ssSkP127("d1")
    & ssSkP128("d0")
    & ~ ssSkP126("d2")
    & ~ ssSkP127("d2")
    & ssSkP126("d1")
    & ssSkP125("d0")
    & ~ ssSkP128("d2")
    & ssSkP126("d0")
    & ssSkP125("d1")
    & ~ ssSkP171("d1")
    & ~ ssSkP171("d0")
    & ~ 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")
    & ~ ssSkP181("d0")
    & ~ ssSkP182("d1")
    & ~ ssSkP182("d0")
    & ~ ssSkP180("d2")
    & ~ ssSkP181("d1")
    & ~ ssSkP180("d1")
    & ~ ssSkP181("d2")
    & ~ ssSkP182("d2")
    & ~ ssSkP180("d0")
    & ~ ssSkP186("d1")
    & ~ ssSkP185("d0")
    & ~ ssSkP183("d2")
    & ~ ssSkP186("d0")
    & ~ ssSkP185("d1")
    & ~ ssSkP184("d2")
    & ~ ssSkP185("d2")
    & ~ ssSkP183("d0")
    & ~ ssSkP184("d1")
    & ~ ssSkP186("d2")
    & ssSkP183("d1")
    & ~ ssSkP184("d0")
    & ~ ssSkP189("d0")
    & ~ ssSkP187("d2")
    & ~ ssSkP189("d1")
    & ~ ssSkP188("d2")
    & ~ ssSkP189("d2")
    & ssSkP187("d0")
    & ~ ssSkP188("d1")
    & ~ ssSkP187("d1")
    & ~ ssSkP188("d0")
    & ~ ssSkP153("d1")
    & ~ ssSkP152("d0")
    & ~ ssSkP150("d2")
    & ~ ssSkP153("d0")
    & ~ ssSkP152("d1")
    & ~ ssSkP151("d2")
    & ~ ssSkP152("d2")
    & ~ ssSkP151("d1")
    & ~ ssSkP150("d0")
    & ~ ssSkP153("d2")
    & ~ ssSkP151("d0")
    & ~ ssSkP150("d1")
    & ssSkP157("d1")
    & ssSkP156("d0")
    & ~ ssSkP154("d2")
    & ssSkP157("d0")
    & ssSkP156("d1")
    & ~ ssSkP155("d2")
    & ~ ssSkP156("d2")
    & ssSkP154("d0")
    & ssSkP155("d1")
    & ~ ssSkP157("d2")
    & ssSkP154("d1")
    & ssSkP155("d0")
    & ~ ssSkP158("d2")
    & ~ ssSkP159("d2")
    & ssSkP159("d1")
    & ssSkP158("d0")
    & ssSkP159("d0")
    & ssSkP158("d1")
    & ssSkP160("d1")
    & ssSkP160("d0")
    & ~ ssSkP160("d2")
    & ssSkP164("d1")
    & ssSkP163("d0")
    & ~ ssSkP161("d2")
    & ssSkP164("d0")
    & ~ ssSkP162("d2")
    & ssSkP163("d1")
    & ssSkP162("d1")
    & ~ ssSkP163("d2")
    & ssSkP161("d0")
    & ~ ssSkP164("d2")
    & ssSkP162("d0")
    & ~ ssSkP161("d1")
    & ssSkP167("d0")
    & ~ ssSkP168("d1")
    & ~ ssSkP165("d2")
    & ssSkP167("d1")
    & ~ ssSkP166("d2")
    & ~ ssSkP168("d0")
    & ~ ssSkP167("d2")
    & ssSkP166("d1")
    & ssSkP165("d0")
    & ssSkP166("d0")
    & ssSkP168("d2")
    & ssSkP165("d1")
    & ~ ssSkP192("d0")
    & ~ ssSkP193("d1")
    & ~ ssSkP190("d2")
    & ~ ssSkP192("d1")
    & ~ ssSkP191("d2")
    & ~ ssSkP193("d0")
    & ~ ssSkP192("d2")
    & ~ ssSkP191("d1")
    & ~ ssSkP190("d0")
    & ~ ssSkP191("d0")
    & ssSkP193("d2")
    & ~ ssSkP190("d1")
    & ~ ssSkP197("d1")
    & ~ ssSkP196("d0")
    & ~ ssSkP197("d0")
    & ~ ssSkP196("d1")
    & ~ ssSkP196("d2")
    & ~ ssSkP197("d2")
    & ~ ssSkP198("d2")
    & ~ ssSkP199("d2")
    & ~ ssSkP198("d0")
    & ~ ssSkP199("d1")
    & ~ ssSkP198("d1")
    & ~ ssSkP199("d0")
    & ~ ssSkP9("d0")
    & ~ ssSkP8("d1")
    & ~ ssSkP9("d1")
    & ~ ssSkP8("d0")
    & ~ ssSkP9("d2")
    & ~ ssSkP8("d2")
    & ~ ssSkP502("d1")
    & ~ ssSkP502("d0")
    & ~ ssSkP502("d2")
    & ~ 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")
    & ~ ssSkP528("d1")
    & ~ ssSkP527("d0")
    & ~ ssSkP525("d2")
    & ~ ssSkP528("d0")
    & ~ ssSkP526("d2")
    & ~ ssSkP527("d1")
    & ~ ssSkP526("d1")
    & ~ ssSkP527("d2")
    & ~ ssSkP525("d0")
    & ~ ssSkP528("d2")
    & ~ ssSkP526("d0")
    & ~ ssSkP525("d1")
    & ~ ssSkP529("d2")
    & ~ ssSkP529("d0")
    & ~ ssSkP529("d1")
    & ~ ssSkP531("d1")
    & ~ ssSkP530("d0")
    & ssSkP531("d0")
    & ~ ssSkP530("d1")
    & ~ ssSkP530("d2")
    & ~ ssSkP531("d2")
    & ssSkP535("d1")
    & ssSkP534("d0")
    & ~ ssSkP532("d2")
    & ssSkP535("d0")
    & ~ ssSkP533("d2")
    & ssSkP534("d1")
    & ssSkP533("d1")
    & ~ ssSkP534("d2")
    & ~ ssSkP532("d0")
    & ~ ssSkP535("d2")
    & ssSkP533("d0")
    & ~ ssSkP532("d1")
    & ~ ssSkP536("d2")
    & ssSkP537("d2")
    & ssSkP536("d0")
    & ~ ssSkP537("d1")
    & ssSkP536("d1")
    & ~ ssSkP537("d0")
    & ~ ssSkP542("d1")
    & ~ ssSkP541("d0")
    & ~ ssSkP542("d0")
    & ~ ssSkP541("d1")
    & ~ ssSkP540("d2")
    & ~ ssSkP541("d2")
    & ~ ssSkP540("d1")
    & ~ ssSkP542("d2")
    & ~ ssSkP540("d0")
    & ~ ssSkP546("d1")
    & ~ ssSkP545("d0")
    & ~ ssSkP543("d2")
    & ~ ssSkP546("d0")
    & ~ ssSkP544("d2")
    & ~ ssSkP545("d1")
    & ~ ssSkP544("d1")
    & ~ ssSkP545("d2")
    & ~ ssSkP543("d0")
    & ~ ssSkP546("d2")
    & ~ ssSkP544("d0")
    & ~ ssSkP543("d1")
    & ~ ssSkP505("d0")
    & ~ ssSkP506("d1")
    & ~ ssSkP503("d2")
    & ~ ssSkP505("d1")
    & ~ ssSkP506("d0")
    & ~ 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")
    & ~ ssSkP512("d0")
    & ~ ssSkP513("d1")
    & ~ ssSkP510("d2")
    & ssSkP512("d1")
    & ~ ssSkP513("d0")
    & ~ 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")
    & ssSkP514("d0")
    & ssSkP515("d1")
    & ~ ssSkP517("d2")
    & ssSkP514("d1")
    & ssSkP515("d0")
    & ssSkP518("d2")
    & ~ ssSkP518("d0")
    & ~ ssSkP518("d1")
    & ~ ssSkP524("d1")
    & ~ ssSkP523("d0")
    & ~ ssSkP521("d2")
    & ~ ssSkP524("d0")
    & ~ ssSkP523("d1")
    & ~ 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")
    & ssSkP453("d0")
    & ssSkP454("d1")
    & ~ ssSkP451("d2")
    & ssSkP453("d1")
    & ssSkP454("d0")
    & ~ ssSkP452("d2")
    & ~ ssSkP453("d2")
    & ssSkP451("d0")
    & ssSkP452("d1")
    & ~ ssSkP454("d2")
    & ssSkP451("d1")
    & ssSkP452("d0")
    & ~ ssSkP455("d2")
    & ssSkP456("d2")
    & ssSkP455("d0")
    & ~ ssSkP456("d1")
    & ssSkP455("d1")
    & ~ ssSkP456("d0")
    & ~ ssSkP459("d2")
    & ~ ssSkP459("d0")
    & ~ ssSkP459("d1")
    & ~ ssSkP461("d1")
    & ~ ssSkP460("d0")
    & ~ ssSkP461("d0")
    & ~ ssSkP460("d1")
    & ~ ssSkP460("d2")
    & ~ ssSkP461("d2")
    & ~ ssSkP465("d1")
    & ~ ssSkP464("d0")
    & ~ ssSkP462("d2")
    & ~ ssSkP465("d0")
    & ~ ssSkP464("d1")
    & ~ ssSkP463("d2")
    & ~ ssSkP464("d2")
    & ~ ssSkP463("d1")
    & ~ ssSkP462("d0")
    & ~ ssSkP465("d2")
    & ~ ssSkP463("d0")
    & ~ ssSkP462("d1")
    & ~ ssSkP469("d1")
    & ~ ssSkP468("d0")
    & ~ ssSkP466("d2")
    & ~ ssSkP469("d0")
    & ~ ssSkP467("d2")
    & ~ ssSkP468("d1")
    & ssSkP467("d1")
    & ~ ssSkP468("d2")
    & ~ ssSkP466("d0")
    & ~ ssSkP469("d2")
    & ~ ssSkP467("d0")
    & ~ ssSkP466("d1")
    & ~ ssSkP429("d1")
    & ~ ssSkP428("d0")
    & ~ ssSkP426("d2")
    & ~ ssSkP429("d0")
    & ~ ssSkP428("d1")
    & ~ ssSkP427("d2")
    & ~ ssSkP428("d2")
    & ~ ssSkP426("d0")
    & ~ ssSkP427("d1")
    & ~ ssSkP429("d2")
    & ~ 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")
    & ~ ssSkP434("d2")
    & ~ ssSkP435("d1")
    & ~ ssSkP434("d1")
    & ~ ssSkP435("d2")
    & ~ ssSkP433("d0")
    & ~ ssSkP436("d2")
    & ~ ssSkP434("d0")
    & ~ ssSkP433("d1")
    & ssSkP437("d2")
    & ~ ssSkP437("d0")
    & ~ ssSkP437("d1")
    & ~ 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")
    & ~ ssSkP446("d1")
    & ~ ssSkP445("d2")
    & ~ ssSkP446("d2")
    & ~ ssSkP445("d1")
    & ~ ssSkP444("d0")
    & ~ ssSkP447("d2")
    & ~ ssSkP445("d0")
    & ~ ssSkP444("d1")
    & ~ ssSkP490("d1")
    & ~ ssSkP490("d0")
    & ~ ssSkP490("d2")
    & ~ ssSkP111("d2","d1")
    & ~ ssSkP111("d1","d2")
    & ~ ssSkP112("d2","d2")
    & ssSkP112("d1","d1")
    & ssSkP112("d0","d0")
    & ~ ssSkP494("d1")
    & ~ ssSkP493("d0")
    & ~ ssSkP491("d2")
    & ~ ssSkP111("d2","d0")
    & ~ ssSkP111("d0","d2")
    & ssSkP112("d0","d1")
    & ssSkP112("d1","d0")
    & ~ ssSkP494("d0")
    & ~ ssSkP493("d1")
    & ~ ssSkP492("d2")
    & ssSkP111("d1","d0")
    & ssSkP111("d0","d1")
    & ssSkP112("d0","d2")
    & ~ ssSkP112("d2","d0")
    & ~ ssSkP493("d2")
    & ~ ssSkP492("d1")
    & ~ ssSkP491("d0")
    & ~ ssSkP111("d2","d2")
    & ssSkP111("d1","d1")
    & ssSkP111("d0","d0")
    & ssSkP112("d1","d2")
    & ~ ssSkP112("d2","d1")
    & ~ ssSkP494("d2")
    & ~ ssSkP492("d0")
    & ~ ssSkP491("d1")
    & ssSkP498("d1")
    & ssSkP497("d0")
    & ~ ssSkP495("d2")
    & ssSkP498("d0")
    & ~ ssSkP496("d2")
    & ssSkP497("d1")
    & ssSkP496("d1")
    & ~ ssSkP497("d2")
    & ~ ssSkP495("d0")
    & ~ ssSkP498("d2")
    & ssSkP496("d0")
    & ~ ssSkP495("d1")
    & ssSkP499("d2")
    & ~ ssSkP499("d0")
    & ~ ssSkP499("d1")
    & ssSkP472("d1")
    & ~ ssSkP471("d0")
    & ssSkP472("d0")
    & ~ ssSkP470("d2")
    & ~ ssSkP471("d1")
    & ~ ssSkP470("d1")
    & ~ ssSkP471("d2")
    & ~ ssSkP472("d2")
    & ~ ssSkP470("d0")
    & ~ ssSkP130("d2","d2")
    & ssSkP130("d1","d1")
    & ssSkP130("d0","d0")
    & ssSkP131("d0","d1")
    & ssSkP131("d1","d0")
    & ~ ssSkP475("d0")
    & ~ ssSkP473("d2")
    & ssSkP130("d1","d0")
    & ssSkP130("d0","d1")
    & ~ ssSkP131("d2","d2")
    & ssSkP131("d1","d1")
    & ssSkP131("d0","d0")
    & ~ ssSkP474("d2")
    & ~ ssSkP475("d1")
    & ~ ssSkP130("d2","d0")
    & ~ ssSkP130("d0","d2")
    & ssSkP131("d1","d2")
    & ~ ssSkP131("d2","d1")
    & ssSkP474("d1")
    & ssSkP475("d2")
    & ssSkP473("d0")
    & ~ ssSkP130("d2","d1")
    & ~ ssSkP130("d1","d2")
    & ssSkP131("d0","d2")
    & ~ ssSkP131("d2","d0")
    & ssSkP474("d0")
    & ssSkP473("d1")
    & ~ ssSkP479("d0")
    & ~ ssSkP479("d1")
    & ~ ssSkP478("d2")
    & ~ ssSkP479("d2")
    & ~ ssSkP478("d1")
    & ~ ssSkP478("d0")
    & ~ ssSkP148("d2","d1")
    & ~ ssSkP148("d1","d2")
    & ~ ssSkP149("d2","d2")
    & ssSkP149("d1","d1")
    & ssSkP149("d0","d0")
    & ~ ssSkP148("d2","d0")
    & ~ ssSkP148("d0","d2")
    & ssSkP149("d0","d1")
    & ssSkP149("d1","d0")
    & ssSkP148("d1","d0")
    & ssSkP148("d0","d1")
    & ssSkP149("d0","d2")
    & ~ ssSkP149("d2","d0")
    & ~ ssSkP148("d2","d2")
    & ssSkP148("d1","d1")
    & ssSkP148("d0","d0")
    & ssSkP149("d1","d2")
    & ~ ssSkP149("d2","d1")
    & ~ ssSkP483("d1")
    & ~ ssSkP482("d0")
    & ~ ssSkP480("d2")
    & ~ ssSkP483("d0")
    & ~ ssSkP482("d1")
    & ~ ssSkP481("d2")
    & ~ ssSkP482("d2")
    & ~ ssSkP481("d1")
    & ~ ssSkP480("d0")
    & ~ ssSkP483("d2")
    & ~ ssSkP481("d0")
    & ~ ssSkP480("d1")
    & ~ ssSkP487("d1")
    & ~ ssSkP486("d0")
    & ~ ssSkP484("d2")
    & ~ ssSkP487("d0")
    & ~ ssSkP485("d2")
    & ~ ssSkP486("d1")
    & ssSkP485("d1")
    & ~ ssSkP486("d2")
    & ~ ssSkP484("d0")
    & ~ ssSkP487("d2")
    & ~ ssSkP485("d0")
    & ~ ssSkP484("d1")
    & ~ ssSkP488("d2")
    & ~ ssSkP489("d2")
    & ~ ssSkP489("d1")
    & ~ ssSkP488("d0")
    & ~ ssSkP489("d0")
    & ~ ssSkP488("d1")
    & ~ ssSkP169("d2","d0")
    & ~ ssSkP169("d0","d2")
    & ~ ssSkP169("d2","d1")
    & ~ ssSkP169("d1","d2")
    & ~ ssSkP169("d2","d2")
    & ssSkP169("d1","d1")
    & ssSkP169("d0","d0")
    & ssSkP169("d1","d0")
    & ssSkP169("d0","d1")
    & ~ ssSkP170("d2","d2")
    & ssSkP170("d1","d1")
    & ssSkP170("d0","d0")
    & ssSkP170("d0","d1")
    & ssSkP170("d1","d0")
    & ~ ssSkP170("d0","d2")
    & ~ ssSkP170("d2","d0")
    & ~ ssSkP170("d1","d2")
    & ~ ssSkP170("d2","d1")
    & ~ ssSkP194("d2","d0")
    & ~ ssSkP194("d0","d2")
    & ~ ssSkP195("d1","d2")
    & ~ ssSkP195("d2","d1")
    & ~ ssSkP194("d2","d1")
    & ~ ssSkP194("d1","d2")
    & ~ ssSkP195("d0","d2")
    & ~ ssSkP195("d2","d0")
    & ~ ssSkP194("d2","d2")
    & ssSkP194("d1","d1")
    & ssSkP194("d0","d0")
    & ssSkP195("d0","d1")
    & ssSkP195("d1","d0")
    & ssSkP194("d1","d0")
    & ssSkP194("d0","d1")
    & ~ ssSkP195("d2","d2")
    & ssSkP195("d1","d1")
    & ssSkP195("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")
    & ssSkP413("d0")
    & ssSkP414("d1")
    & ~ ssSkP411("d2")
    & ssSkP413("d1")
    & ssSkP414("d0")
    & ~ ssSkP412("d2")
    & ~ ssSkP413("d2")
    & ssSkP412("d1")
    & ssSkP411("d0")
    & ~ ssSkP414("d2")
    & ssSkP412("d0")
    & ssSkP411("d1")
    & ~ ssSkP415("d2")
    & ssSkP416("d2")
    & ssSkP415("d0")
    & ~ ssSkP416("d1")
    & ssSkP415("d1")
    & ~ ssSkP416("d0")
    & ~ ssSkP419("d2")
    & ~ ssSkP419("d0")
    & ~ ssSkP419("d1")
    & ~ ssSkP421("d1")
    & ~ ssSkP420("d0")
    & ~ ssSkP421("d0")
    & ~ ssSkP420("d1")
    & ~ ssSkP420("d2")
    & ~ ssSkP421("d2")
    & ~ ssSkP425("d1")
    & ~ ssSkP424("d0")
    & ~ ssSkP422("d2")
    & ~ ssSkP425("d0")
    & ~ ssSkP424("d1")
    & ~ ssSkP423("d2")
    & ~ ssSkP424("d2")
    & ~ ssSkP422("d0")
    & ~ ssSkP423("d1")
    & ~ ssSkP425("d2")
    & ~ ssSkP422("d1")
    & ~ ssSkP423("d0")
    & ~ ssSkP302("d2","d1")
    & ~ ssSkP302("d1","d2")
    & ~ ssSkP303("d2","d2")
    & ssSkP303("d1","d1")
    & ssSkP303("d0","d0")
    & ~ ssSkP302("d2","d0")
    & ~ ssSkP302("d0","d2")
    & ssSkP303("d0","d1")
    & ssSkP303("d1","d0")
    & ssSkP302("d1","d0")
    & ssSkP302("d0","d1")
    & ssSkP303("d0","d2")
    & ~ ssSkP303("d2","d0")
    & ~ ssSkP302("d2","d2")
    & ssSkP302("d1","d1")
    & ssSkP302("d0","d0")
    & ssSkP303("d1","d2")
    & ~ ssSkP303("d2","d1")
    & ssSkP403("d1")
    & ssSkP402("d0")
    & ~ ssSkP400("d2")
    & ssSkP403("d0")
    & ssSkP402("d1")
    & ~ ssSkP401("d2")
    & ~ ssSkP402("d2")
    & ssSkP400("d0")
    & ssSkP401("d1")
    & ~ ssSkP403("d2")
    & ssSkP400("d1")
    & ssSkP401("d0")
    & ~ ssSkP329("d0")
    & ~ ssSkP329("d1")
    & ~ ssSkP329("d2")
    & ssSkP1090("d1")
    & ~ ssSkP1091("d0")
    & ~ ssSkP1090("d0")
    & ssSkP1091("d1")
    & ~ ssSkP1091("d2")
    & ~ ssSkP1090("d2")
    & ~ ssSkP1093("d2")
    & ssSkP1094("d1")
    & ssSkP1095("d0")
    & ~ ssSkP1092("d2")
    & ~ ssSkP1094("d0")
    & ssSkP1095("d1")
    & ~ ssSkP1093("d0")
    & ssSkP1092("d1")
    & ~ ssSkP1095("d2")
    & ssSkP1093("d1")
    & ~ ssSkP1092("d0")
    & ~ ssSkP1094("d2")
    & ~ ssSkP1099("d0")
    & ssSkP1098("d1")
    & ~ ssSkP1097("d2")
    & ssSkP1099("d1")
    & ~ ssSkP1098("d0")
    & ~ ssSkP1096("d2")
    & ~ ssSkP1099("d2")
    & ~ ssSkP1097("d0")
    & ssSkP1096("d1")
    & ~ ssSkP1098("d2")
    & ssSkP1097("d1")
    & ~ ssSkP1096("d0")
    & ssSkP332("d0")
    & ~ ssSkP333("d1")
    & ~ ssSkP330("d2")
    & ~ ssSkP332("d1")
    & ~ ssSkP333("d0")
    & ~ ssSkP331("d2")
    & ~ ssSkP332("d2")
    & ~ ssSkP331("d1")
    & ~ ssSkP330("d0")
    & ~ ssSkP333("d2")
    & ~ ssSkP331("d0")
    & ~ ssSkP330("d1")
    & ~ 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")
    & ~ ssSkP1082("d2")
    & ~ ssSkP1084("d0")
    & ssSkP1083("d1")
    & ssSkP1084("d1")
    & ~ ssSkP1081("d2")
    & ~ ssSkP1083("d0")
    & ~ ssSkP1082("d0")
    & ~ ssSkP1084("d2")
    & ssSkP1081("d1")
    & ssSkP1082("d1")
    & ~ ssSkP1081("d0")
    & ~ ssSkP1083("d2")
    & ssSkP1087("d1")
    & ~ ssSkP1088("d0")
    & ~ ssSkP1086("d2")
    & ~ ssSkP340("d1")
    & ~ ssSkP1087("d0")
    & ssSkP1088("d1")
    & ~ ssSkP340("d0")
    & ~ ssSkP1088("d2")
    & ~ ssSkP1086("d0")
    & ~ ssSkP1087("d2")
    & ssSkP1086("d1")
    & ~ ssSkP340("d2")
    & ~ ssSkP344("d1")
    & ~ ssSkP343("d0")
    & ~ ssSkP341("d2")
    & ~ ssSkP1089("d2")
    & ~ ssSkP344("d0")
    & ~ ssSkP342("d2")
    & ~ ssSkP343("d1")
    & ssSkP1089("d1")
    & ~ ssSkP342("d1")
    & ~ ssSkP343("d2")
    & ~ ssSkP341("d0")
    & ~ ssSkP1089("d0")
    & ~ ssSkP344("d2")
    & ~ ssSkP342("d0")
    & ~ ssSkP341("d1")
    & ssSkP348("d1")
    & ~ ssSkP347("d0")
    & ~ ssSkP345("d2")
    & ssSkP348("d0")
    & ~ ssSkP347("d1")
    & ~ ssSkP346("d2")
    & ~ ssSkP347("d2")
    & ~ ssSkP346("d1")
    & ~ ssSkP345("d0")
    & ~ ssSkP348("d2")
    & ~ ssSkP346("d0")
    & ~ ssSkP345("d1")
    & ~ ssSkP308("d1")
    & ~ ssSkP307("d0")
    & ~ ssSkP305("d2")
    & ~ ssSkP308("d0")
    & ~ ssSkP307("d1")
    & ~ ssSkP306("d2")
    & ~ ssSkP307("d2")
    & ~ ssSkP306("d1")
    & ~ ssSkP305("d0")
    & ~ ssSkP308("d2")
    & ~ ssSkP306("d0")
    & ~ ssSkP305("d1")
    & ~ ssSkP309("d2")
    & ~ ssSkP309("d0")
    & ~ ssSkP309("d1")
    & ssSkP216("d1","d0")
    & ssSkP216("d0","d1")
    & ssSkP1073("d0")
    & ssSkP1072("d1")
    & ~ ssSkP1071("d2")
    & ~ ssSkP216("d2","d2")
    & ssSkP216("d1","d1")
    & ssSkP216("d0","d0")
    & ssSkP1073("d1")
    & ssSkP1072("d0")
    & ~ ssSkP1070("d2")
    & ~ ssSkP216("d2","d1")
    & ~ ssSkP216("d1","d2")
    & ~ ssSkP1073("d2")
    & ssSkP1071("d0")
    & ssSkP1070("d1")
    & ~ ssSkP216("d2","d0")
    & ~ ssSkP216("d0","d2")
    & ~ ssSkP1072("d2")
    & ssSkP1071("d1")
    & ssSkP1070("d0")
    & ~ ssSkP1077("d0")
    & ~ ssSkP1075("d2")
    & ssSkP1077("d1")
    & ssSkP1074("d2")
    & ~ ssSkP1077("d2")
    & ~ ssSkP1074("d1")
    & ssSkP1075("d0")
    & ~ ssSkP1074("d0")
    & ssSkP1075("d1")
    & ~ ssSkP1079("d2")
    & ~ ssSkP311("d1")
    & ~ ssSkP310("d0")
    & ~ ssSkP1078("d2")
    & ~ ssSkP311("d0")
    & ~ ssSkP310("d1")
    & ssSkP1078("d1")
    & ~ ssSkP1079("d0")
    & ~ ssSkP310("d2")
    & ~ ssSkP1078("d0")
    & ssSkP1079("d1")
    & ~ ssSkP311("d2")
    & ~ ssSkP315("d1")
    & ~ ssSkP314("d0")
    & ~ ssSkP312("d2")
    & ~ ssSkP315("d0")
    & ~ ssSkP314("d1")
    & ~ ssSkP313("d2")
    & ~ ssSkP314("d2")
    & ~ ssSkP313("d1")
    & ~ ssSkP312("d0")
    & ~ ssSkP315("d2")
    & ~ ssSkP313("d0")
    & ~ ssSkP312("d1")
    & ~ ssSkP319("d1")
    & ~ ssSkP318("d0")
    & ~ ssSkP316("d2")
    & ~ ssSkP319("d0")
    & ~ ssSkP317("d2")
    & ~ ssSkP318("d1")
    & ssSkP317("d1")
    & ~ ssSkP318("d2")
    & ~ ssSkP316("d0")
    & ~ ssSkP319("d2")
    & ~ ssSkP317("d0")
    & ~ ssSkP316("d1")
    & ssSkP217("d0","d2")
    & ~ ssSkP217("d2","d0")
    & ssSkP217("d1","d2")
    & ~ ssSkP217("d2","d1")
    & ~ ssSkP217("d2","d2")
    & ssSkP217("d1","d1")
    & ssSkP217("d0","d0")
    & ssSkP217("d0","d1")
    & ssSkP217("d1","d0")
    & ssSkP1062("d0")
    & ssSkP1061("d1")
    & ~ ssSkP1060("d2")
    & ssSkP1062("d1")
    & ssSkP1061("d0")
    & ~ ssSkP1062("d2")
    & ssSkP1060("d0")
    & ~ ssSkP1061("d2")
    & ssSkP1060("d1")
    & ssSkP1066("d0")
    & ssSkP1065("d1")
    & ~ ssSkP1064("d2")
    & ssSkP1066("d1")
    & ssSkP1065("d0")
    & ~ 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")
    & ~ ssSkP320("d2")
    & ~ ssSkP321("d1")
    & ssSkP1068("d0")
    & ssSkP1067("d1")
    & ~ ssSkP320("d1")
    & ~ ssSkP321("d2")
    & ~ ssSkP1069("d2")
    & ssSkP1068("d1")
    & ssSkP1067("d0")
    & ~ ssSkP322("d2")
    & ssSkP320("d0")
    & ssSkP325("d0")
    & ~ ssSkP326("d1")
    & ~ ssSkP323("d2")
    & ssSkP325("d1")
    & ~ ssSkP324("d2")
    & ~ ssSkP326("d0")
    & ~ ssSkP325("d2")
    & ssSkP324("d1")
    & ~ ssSkP323("d0")
    & ssSkP324("d0")
    & ssSkP326("d2")
    & ~ ssSkP323("d1")
    & ssSkP238("d1","d0")
    & ssSkP238("d0","d1")
    & ssSkP1051("d0")
    & ssSkP1050("d1")
    & ~ ssSkP238("d2","d2")
    & ssSkP238("d1","d1")
    & ssSkP238("d0","d0")
    & ssSkP1051("d1")
    & ssSkP1050("d0")
    & ~ ssSkP238("d2","d1")
    & ~ ssSkP238("d1","d2")
    & ~ ssSkP1051("d2")
    & ~ ssSkP238("d2","d0")
    & ~ ssSkP238("d0","d2")
    & ~ ssSkP1050("d2")
    & ssSkP373("d1")
    & ssSkP372("d0")
    & ~ ssSkP370("d2")
    & ssSkP1055("d0")
    & ssSkP373("d0")
    & ssSkP1052("d2")
    & ssSkP372("d1")
    & ~ ssSkP371("d2")
    & ~ ssSkP1055("d1")
    & ~ ssSkP1052("d1")
    & ~ ssSkP372("d2")
    & ssSkP371("d1")
    & ssSkP370("d0")
    & ~ ssSkP1055("d2")
    & ~ ssSkP373("d2")
    & ~ ssSkP1052("d0")
    & ssSkP371("d0")
    & ssSkP370("d1")
    & ~ ssSkP374("d2")
    & ssSkP1058("d1")
    & ssSkP1059("d0")
    & ~ ssSkP1057("d2")
    & ssSkP375("d2")
    & ssSkP1058("d0")
    & ssSkP1059("d1")
    & ~ ssSkP1056("d2")
    & ssSkP374("d0")
    & ~ ssSkP375("d1")
    & ~ ssSkP1059("d2")
    & ssSkP1056("d1")
    & ~ ssSkP1057("d0")
    & ssSkP374("d1")
    & ~ ssSkP375("d0")
    & ~ ssSkP1058("d2")
    & ssSkP1056("d0")
    & ssSkP1057("d1")
    & ~ ssSkP378("d2")
    & ~ ssSkP379("d2")
    & ~ ssSkP379("d1")
    & ~ ssSkP378("d0")
    & ~ ssSkP379("d0")
    & ~ ssSkP378("d1")
    & ~ ssSkP239("d0","d2")
    & ~ ssSkP239("d2","d0")
    & ~ ssSkP239("d1","d2")
    & ~ ssSkP239("d2","d1")
    & ~ ssSkP239("d2","d2")
    & ssSkP239("d1","d1")
    & ssSkP239("d0","d0")
    & ssSkP239("d0","d1")
    & ssSkP239("d1","d0")
    & ssSkP1040("d0")
    & ~ ssSkP380("d1")
    & ssSkP1040("d1")
    & ~ ssSkP380("d0")
    & ~ ssSkP1040("d2")
    & ~ ssSkP380("d2")
    & ssSkP1044("d0")
    & ssSkP1043("d1")
    & ~ ssSkP1042("d2")
    & ~ ssSkP384("d1")
    & ~ ssSkP383("d0")
    & ~ ssSkP381("d2")
    & ssSkP1044("d1")
    & ssSkP1043("d0")
    & ~ ssSkP1041("d2")
    & ssSkP384("d0")
    & ~ ssSkP383("d1")
    & ~ ssSkP382("d2")
    & ~ ssSkP1044("d2")
    & ssSkP1041("d1")
    & ssSkP1042("d0")
    & ~ ssSkP383("d2")
    & ~ ssSkP381("d0")
    & ~ ssSkP382("d1")
    & ~ ssSkP1043("d2")
    & ssSkP1041("d0")
    & ssSkP1042("d1")
    & ~ ssSkP384("d2")
    & ssSkP381("d1")
    & ~ ssSkP382("d0")
    & ssSkP1048("d0")
    & ssSkP1047("d1")
    & ~ ssSkP1046("d2")
    & ~ ssSkP388("d1")
    & ~ ssSkP387("d0")
    & ~ ssSkP385("d2")
    & ssSkP1048("d1")
    & ssSkP1047("d0")
    & ~ ssSkP1045("d2")
    & ~ ssSkP388("d0")
    & ~ ssSkP387("d1")
    & ~ ssSkP386("d2")
    & ~ ssSkP1048("d2")
    & ssSkP1046("d0")
    & ssSkP1045("d1")
    & ~ ssSkP387("d2")
    & ~ ssSkP386("d1")
    & ~ ssSkP385("d0")
    & ~ ssSkP1047("d2")
    & ssSkP1046("d1")
    & ssSkP1045("d0")
    & ~ ssSkP388("d2")
    & ~ ssSkP386("d0")
    & ~ ssSkP385("d1")
    & ~ ssSkP389("d2")
    & ~ ssSkP1049("d2")
    & ssSkP1049("d1")
    & ~ ssSkP389("d0")
    & ssSkP1049("d0")
    & ~ ssSkP389("d1")
    & ~ ssSkP349("d2")
    & ssSkP349("d0")
    & ssSkP349("d1")
    & ~ ssSkP350("d0")
    & ssSkP1033("d0")
    & ssSkP1032("d1")
    & ~ ssSkP1031("d2")
    & ~ ssSkP350("d1")
    & ~ ssSkP1033("d1")
    & ssSkP1032("d0")
    & ~ ssSkP1030("d2")
    & ssSkP350("d2")
    & ~ ssSkP1033("d2")
    & ssSkP1031("d0")
    & ssSkP1030("d1")
    & ~ ssSkP1032("d2")
    & ssSkP1031("d1")
    & ssSkP1030("d0")
    & ssSkP1036("d1")
    & ssSkP1037("d0")
    & ~ ssSkP1035("d2")
    & ssSkP355("d1")
    & ssSkP354("d0")
    & ssSkP1036("d0")
    & ssSkP1037("d1")
    & ~ ssSkP1034("d2")
    & ssSkP355("d0")
    & ssSkP354("d1")
    & ~ ssSkP353("d2")
    & ~ ssSkP1037("d2")
    & ssSkP1034("d1")
    & ssSkP1035("d0")
    & ~ ssSkP354("d2")
    & ssSkP353("d1")
    & ~ ssSkP1036("d2")
    & ssSkP1034("d0")
    & ssSkP1035("d1")
    & ~ ssSkP355("d2")
    & ssSkP353("d0")
    & ~ ssSkP1039("d2")
    & ssSkP358("d0")
    & ssSkP359("d1")
    & ~ ssSkP356("d2")
    & ~ ssSkP1038("d2")
    & ssSkP358("d1")
    & ssSkP359("d0")
    & ~ ssSkP357("d2")
    & ssSkP1039("d0")
    & ssSkP1038("d1")
    & ~ ssSkP358("d2")
    & ~ ssSkP357("d1")
    & ssSkP356("d0")
    & ssSkP1039("d1")
    & ssSkP1038("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")
    & ssSkP262("d0","d0")
    & ssSkP263("d0","d1")
    & ssSkP262("d1","d1")
    & ssSkP263("d1","d0")
    & ssSkP1026("d0")
    & ssSkP1025("d1")
    & ~ ssSkP1024("d2")
    & ~ ssSkP262("d2","d2")
    & ssSkP366("d1")
    & ~ ssSkP363("d2")
    & ssSkP365("d0")
    & ssSkP262("d0","d1")
    & ~ ssSkP263("d2","d2")
    & ssSkP262("d1","d0")
    & ssSkP263("d1","d1")
    & ssSkP263("d0","d0")
    & ssSkP1026("d1")
    & ssSkP1025("d0")
    & ~ ssSkP1023("d2")
    & ssSkP366("d0")
    & ~ ssSkP364("d2")
    & ~ ssSkP365("d1")
    & ~ ssSkP262("d0","d2")
    & ssSkP263("d1","d2")
    & ~ ssSkP263("d2","d1")
    & ~ ssSkP1026("d2")
    & ssSkP1024("d0")
    & ssSkP1023("d1")
    & ssSkP364("d1")
    & ~ ssSkP262("d2","d0")
    & ssSkP363("d0")
    & ~ ssSkP365("d2")
    & ~ ssSkP262("d1","d2")
    & ~ ssSkP262("d2","d1")
    & ssSkP263("d0","d2")
    & ~ ssSkP263("d2","d0")
    & ~ ssSkP1025("d2")
    & ssSkP1024("d1")
    & ssSkP1023("d0")
    & ~ ssSkP366("d2")
    & ssSkP363("d1")
    & ssSkP364("d0")
    & ssSkP369("d0")
    & ~ ssSkP367("d2")
    & ssSkP1027("d2")
    & ssSkP369("d1")
    & ~ ssSkP368("d2")
    & ~ ssSkP1027("d1")
    & ~ ssSkP369("d2")
    & ssSkP368("d1")
    & ssSkP367("d0")
    & ~ ssSkP1027("d0")
    & ssSkP368("d0")
    & ssSkP367("d1")
    & ~ ssSkP1011("d0")
    & ~ ssSkP1010("d1")
    & ~ ssSkP1011("d1")
    & ~ ssSkP1010("d0")
    & ~ ssSkP1011("d2")
    & ~ ssSkP1010("d2")
    & ssSkP1015("d0")
    & ~ ssSkP1014("d1")
    & ~ ssSkP1013("d2")
    & ssSkP1015("d1")
    & ~ ssSkP1014("d0")
    & ~ ssSkP1012("d2")
    & ~ ssSkP1015("d2")
    & ssSkP1012("d1")
    & ~ ssSkP1013("d0")
    & ~ ssSkP1014("d2")
    & ~ ssSkP1012("d0")
    & ~ ssSkP1013("d1")
    & ssSkP1018("d1")
    & ssSkP1019("d0")
    & ~ ssSkP1017("d2")
    & ssSkP1018("d0")
    & ssSkP1019("d1")
    & ~ ssSkP1016("d2")
    & ~ ssSkP1019("d2")
    & ssSkP1017("d0")
    & ssSkP1016("d1")
    & ~ ssSkP1018("d2")
    & ssSkP1017("d1")
    & ssSkP1016("d0")
    & ssSkP1000("d0")
    & ssSkP1000("d1")
    & ~ ssSkP1000("d2")
    & ~ ssSkP283("d2","d1")
    & ~ ssSkP283("d1","d2")
    & ~ ssSkP284("d2","d2")
    & ssSkP284("d1","d1")
    & ssSkP284("d0","d0")
    & ssSkP1004("d0")
    & ssSkP1003("d1")
    & ~ ssSkP1002("d2")
    & ~ ssSkP283("d2","d0")
    & ~ ssSkP283("d0","d2")
    & ssSkP284("d0","d1")
    & ssSkP284("d1","d0")
    & ssSkP1004("d1")
    & ssSkP1003("d0")
    & ~ ssSkP1001("d2")
    & ssSkP283("d1","d0")
    & ssSkP283("d0","d1")
    & ssSkP284("d0","d2")
    & ~ ssSkP284("d2","d0")
    & ~ ssSkP1004("d2")
    & ssSkP1002("d0")
    & ssSkP1001("d1")
    & ~ ssSkP283("d2","d2")
    & ssSkP283("d1","d1")
    & ssSkP283("d0","d0")
    & ssSkP284("d1","d2")
    & ~ ssSkP284("d2","d1")
    & ~ ssSkP1003("d2")
    & ssSkP1002("d1")
    & ssSkP1001("d0")
    & ~ ssSkP1006("d2")
    & ~ ssSkP1007("d1")
    & ~ ssSkP1007("d0")
    & ~ ssSkP1005("d2")
    & ssSkP1006("d0")
    & ssSkP1005("d1")
    & ssSkP1006("d1")
    & ssSkP1007("d2")
    & ssSkP1005("d0")
    & ~ ssSkP390("d0")
    & ~ ssSkP391("d1")
    & ~ ssSkP390("d1")
    & ~ ssSkP391("d0")
    & ~ ssSkP390("d2")
    & ssSkP391("d2")
    & ssSkP395("d1")
    & ssSkP394("d0")
    & ssSkP395("d0")
    & ssSkP394("d1")
    & ~ ssSkP394("d2")
    & ~ ssSkP395("d2")
    & ssSkP399("d1")
    & ssSkP398("d0")
    & ~ ssSkP396("d2")
    & ~ ssSkP399("d0")
    & ssSkP398("d1")
    & ~ ssSkP397("d2")
    & ~ ssSkP398("d2")
    & ssSkP397("d1")
    & ssSkP396("d0")
    & ~ ssSkP399("d2")
    & ssSkP397("d0")
    & ssSkP396("d1")
    & ssSkP88("d0","d1")
    & ssSkP88("d1","d0")
    & ~ ssSkP88("d2","d2")
    & ssSkP88("d1","d1")
    & ssSkP88("d0","d0")
    & ssSkP88("d1","d2")
    & ~ ssSkP88("d2","d1")
    & ssSkP88("d0","d2")
    & ~ ssSkP88("d2","d0")
    & ~ ssSkP87("d2","d0")
    & ~ ssSkP87("d0","d2")
    & ~ ssSkP87("d2","d1")
    & ~ ssSkP87("d1","d2")
    & ~ ssSkP87("d2","d2")
    & ssSkP87("d1","d1")
    & ssSkP87("d0","d0")
    & ssSkP87("d1","d0")
    & ssSkP87("d0","d1")
    & ssSkP66("d0","d1")
    & ssSkP66("d1","d0")
    & ~ ssSkP66("d2","d2")
    & ssSkP66("d1","d1")
    & ssSkP66("d0","d0")
    & ssSkP66("d1","d2")
    & ~ ssSkP66("d2","d1")
    & ssSkP66("d0","d2")
    & ~ ssSkP66("d2","d0")
    & ~ ssSkP65("d2","d0")
    & ~ ssSkP65("d0","d2")
    & ~ ssSkP65("d2","d1")
    & ~ ssSkP65("d1","d2")
    & ~ ssSkP65("d2","d2")
    & ssSkP65("d1","d1")
    & ssSkP65("d0","d0")
    & ssSkP65("d1","d0")
    & ssSkP65("d0","d1")
    & ~ ssSkP45("d2","d2")
    & ssSkP45("d1","d1")
    & ssSkP45("d0","d0")
    & ssSkP46("d1","d2")
    & ~ ssSkP46("d2","d1")
    & ssSkP45("d1","d0")
    & ssSkP45("d0","d1")
    & ssSkP46("d0","d2")
    & ~ ssSkP46("d2","d0")
    & ~ ssSkP45("d2","d0")
    & ~ ssSkP45("d0","d2")
    & ssSkP46("d0","d1")
    & ssSkP46("d1","d0")
    & ~ ssSkP45("d2","d1")
    & ~ ssSkP45("d1","d2")
    & ~ ssSkP46("d2","d2")
    & ssSkP46("d1","d1")
    & ssSkP46("d0","d0")
    & ssSkP22("d0","d1")
    & ssSkP22("d1","d0")
    & ~ ssSkP22("d2","d2")
    & ssSkP22("d1","d1")
    & ssSkP22("d0","d0")
    & ssSkP22("d1","d2")
    & ~ ssSkP22("d2","d1")
    & ssSkP22("d0","d2")
    & ~ ssSkP22("d2","d0")
    & ~ ssSkP21("d2","d0")
    & ~ ssSkP21("d0","d2")
    & ~ ssSkP21("d2","d1")
    & ~ ssSkP21("d1","d2")
    & ~ ssSkP21("d2","d2")
    & ssSkP21("d1","d1")
    & ssSkP21("d0","d0")
    & ssSkP21("d1","d0")
    & ssSkP21("d0","d1")
    & ~ ssSkP50("d2")
    & ~ ssSkP50("d0")
    & ~ ssSkP50("d1")
    & ~ ssSkP54("d2")
    & ~ ssSkP52("d0")
    & ~ ssSkP51("d1")
    & ~ ssSkP53("d2")
    & ~ ssSkP52("d1")
    & ~ ssSkP51("d0")
    & ~ ssSkP54("d0")
    & ~ ssSkP53("d1")
    & ~ ssSkP52("d2")
    & ~ ssSkP54("d1")
    & ~ ssSkP53("d0")
    & ~ ssSkP51("d2")
    & ~ ssSkP58("d2")
    & ~ ssSkP56("d0")
    & ~ ssSkP55("d1")
    & ~ ssSkP56("d1")
    & ~ ssSkP57("d2")
    & ~ ssSkP55("d0")
    & ~ ssSkP58("d0")
    & ~ ssSkP56("d2")
    & ~ ssSkP57("d1")
    & ~ ssSkP58("d1")
    & ~ ssSkP57("d0")
    & ~ ssSkP55("d2")
    & ssSkP59("d1")
    & ssSkP59("d0")
    & ~ ssSkP59("d2")
    & ~ ssSkP61("d2")
    & ~ ssSkP60("d2")
    & ssSkP61("d0")
    & ssSkP60("d1")
    & ssSkP61("d1")
    & ssSkP60("d0")
    & ssSkP62("d1")
    & ssSkP63("d0")
    & ssSkP63("d1")
    & ~ ssSkP62("d0")
    & ssSkP64("d2")
    & ~ ssSkP63("d2")
    & ~ ssSkP64("d1")
    & ~ ssSkP62("d2")
    & ~ ssSkP64("d0")
    & ~ ssSkP69("d2")
    & ssSkP67("d0")
    & ~ ssSkP68("d2")
    & ~ ssSkP67("d1")
    & ssSkP68("d1")
    & ssSkP69("d0")
    & ~ ssSkP67("d2")
    & ssSkP68("d0")
    & ssSkP69("d1")
    & ~ ssSkP72("d2")
    & ssSkP70("d0")
    & ~ ssSkP71("d2")
    & ssSkP70("d1")
    & ssSkP72("d0")
    & ssSkP71("d1")
    & ~ ssSkP70("d2")
    & ssSkP72("d1")
    & ssSkP71("d0")
    & ~ ssSkP76("d2")
    & ssSkP74("d0")
    & ssSkP73("d1")
    & ~ ssSkP75("d2")
    & ssSkP74("d1")
    & ssSkP73("d0")
    & ssSkP76("d0")
    & ssSkP75("d1")
    & ~ ssSkP74("d2")
    & ssSkP76("d1")
    & ssSkP75("d0")
    & ~ ssSkP73("d2")
    & 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")
    & ssSkP84("d1")
    & ssSkP85("d0")
    & ssSkP85("d1")
    & ~ ssSkP84("d0")
    & ssSkP86("d2")
    & ~ ssSkP85("d2")
    & ~ ssSkP86("d1")
    & ~ ssSkP84("d2")
    & ~ ssSkP86("d0")
    & ssSkP89("d0")
    & ssSkP89("d1")
    & ~ ssSkP89("d2")
    & ~ ssSkP94("d2")
    & ssSkP92("d0")
    & ssSkP91("d1")
    & ssSkP92("d1")
    & ~ ssSkP93("d2")
    & ~ ssSkP91("d0")
    & ssSkP94("d0")
    & ~ ssSkP92("d2")
    & ssSkP93("d1")
    & ssSkP94("d1")
    & ssSkP93("d0")
    & ~ ssSkP91("d2")
    & ~ ssSkP98("d2")
    & ssSkP96("d0")
    & ssSkP95("d1")
    & ~ ssSkP97("d2")
    & ssSkP96("d1")
    & ssSkP95("d0")
    & ssSkP98("d0")
    & ssSkP97("d1")
    & ~ ssSkP96("d2")
    & ssSkP98("d1")
    & ssSkP97("d0")
    & ~ 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")
    & ~ ssSkP12("d1")
    & ~ ssSkP13("d2")
    & ~ ssSkP11("d0")
    & ~ ssSkP14("d0")
    & ~ ssSkP12("d2")
    & ~ ssSkP13("d1")
    & ~ 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")
    & ssSkP20("d2")
    & ~ ssSkP20("d1")
    & ~ ssSkP20("d0")
    & ~ ssSkP25("d2")
    & ssSkP23("d0")
    & ~ ssSkP24("d2")
    & ssSkP23("d1")
    & ssSkP25("d0")
    & ssSkP24("d1")
    & ~ ssSkP23("d2")
    & ~ ssSkP25("d1")
    & ssSkP24("d0")
    & ~ ssSkP29("d2")
    & ssSkP26("d1")
    & ssSkP27("d0")
    & ~ ssSkP28("d2")
    & ssSkP26("d0")
    & ~ ssSkP27("d1")
    & ssSkP28("d1")
    & ssSkP29("d0")
    & ~ ssSkP27("d2")
    & ssSkP28("d0")
    & ssSkP29("d1")
    & ~ ssSkP26("d2")
    & ssSkP19("d1")
    & ~ ssSkP19("d0")
    & ~ ssSkP19("d2")
    & ~ ssSkP32("d2")
    & ssSkP30("d0")
    & ~ ssSkP31("d2")
    & ssSkP30("d1")
    & ssSkP32("d0")
    & ssSkP31("d1")
    & ~ ssSkP30("d2")
    & ssSkP32("d1")
    & ssSkP31("d0")
    & ~ ssSkP36("d2")
    & ssSkP34("d0")
    & ssSkP33("d1")
    & ~ ssSkP35("d2")
    & ssSkP34("d1")
    & ssSkP33("d0")
    & ssSkP36("d0")
    & ssSkP35("d1")
    & ~ ssSkP34("d2")
    & ssSkP36("d1")
    & ssSkP35("d0")
    & ~ ssSkP33("d2")
    & ssSkP38("d0")
    & ssSkP37("d1")
    & ~ ssSkP39("d2")
    & ssSkP38("d1")
    & ssSkP37("d0")
    & ssSkP39("d1")
    & ~ ssSkP38("d2")
    & ssSkP39("d0")
    & ~ ssSkP37("d2")
    & ~ ssSkP43("d2")
    & ssSkP41("d0")
    & ssSkP40("d1")
    & ~ ssSkP42("d2")
    & ssSkP41("d1")
    & ssSkP40("d0")
    & ssSkP42("d1")
    & ssSkP43("d0")
    & ~ ssSkP41("d2")
    & ssSkP43("d1")
    & ssSkP42("d0")
    & ~ ssSkP40("d2")
    & ~ ssSkP44("d1")
    & ~ ssSkP47("d2")
    & ~ ssSkP44("d0")
    & ~ ssSkP47("d0")
    & ssSkP44("d2")
    & ~ ssSkP47("d1")
    & ~ ssSkP49("d0")
    & ~ ssSkP48("d1")
    & ~ ssSkP49("d1")
    & ~ ssSkP48("d0")
    & ~ ssSkP49("d2")
    & ~ ssSkP48("d2")
    & ssPv9("d1")
    & ~ ssPv8("d0")
    & ~ ssPv6("d2")
    & ssPv9("d0")
    & ~ ssPv7("d2")
    & ssPv8("d1")
    & ssPv7("d1")
    & ~ ssPv8("d2")
    & ~ ssPv6("d0")
    & ~ ssPv9("d2")
    & ~ ssPv7("d0")
    & ssPv6("d1")
    & ~ ssPv4("d0")
    & ~ ssPv2("d2")
    & ssPv5("d1")
    & ~ ssPv3("d2")
    & ~ ssPv4("d1")
    & ~ ssPv5("d0")
    & ssPv3("d1")
    & ~ ssPv4("d2")
    & ~ ssPv2("d0")
    & ssPv3("d0")
    & ~ ssPv2("d1")
    & ~ ssPv5("d2")
    & ssPv1("d1")
    & ssPv1("d0")
    & ~ ssPv1("d2")
    & ssSkP700("d0")
    & ssSkP700("d1")
    & ~ ssSkP700("d2")
    & ~ ssSkP805("d2","d0")
    & ~ ssSkP805("d0","d2")
    & ssSkP806("d0","d1")
    & ssSkP806("d1","d0")
    & ~ ssSkP805("d2","d1")
    & ~ ssSkP805("d1","d2")
    & ~ ssSkP806("d2","d2")
    & ssSkP806("d1","d1")
    & ssSkP806("d0","d0")
    & ~ ssSkP805("d2","d2")
    & ssSkP805("d1","d1")
    & ssSkP805("d0","d0")
    & ssSkP806("d1","d2")
    & ~ ssSkP806("d2","d1")
    & ssSkP805("d1","d0")
    & ssSkP805("d0","d1")
    & ssSkP806("d0","d2")
    & ~ ssSkP806("d2","d0")
    & ssSkP724("d2")
    & ~ ssSkP723("d2")
    & ssSkP723("d1")
    & ~ ssSkP724("d0")
    & ssSkP723("d0")
    & ~ ssSkP724("d1")
    & ~ ssSkP728("d2")
    & ssSkP729("d1")
    & ssSkP729("d0")
    & ~ ssSkP727("d2")
    & ssSkP728("d0")
    & ssSkP727("d1")
    & ssSkP728("d1")
    & ~ ssSkP729("d2")
    & ssSkP727("d0")
    & ssSkP828("d1","d0")
    & ssSkP828("d0","d1")
    & ~ ssSkP829("d2","d2")
    & ssSkP829("d1","d1")
    & ssSkP829("d0","d0")
    & ~ ssSkP828("d2","d2")
    & ssSkP828("d1","d1")
    & ssSkP828("d0","d0")
    & ssSkP829("d0","d1")
    & ssSkP829("d1","d0")
    & ~ ssSkP828("d2","d1")
    & ~ ssSkP828("d1","d2")
    & ssSkP829("d0","d2")
    & ~ ssSkP829("d2","d0")
    & ~ ssSkP828("d2","d0")
    & ~ ssSkP828("d0","d2")
    & ssSkP829("d1","d2")
    & ~ ssSkP829("d2","d1")
    & ssSkP733("d0")
    & ssSkP732("d1")
    & ~ ssSkP731("d2")
    & ssSkP733("d1")
    & ssSkP732("d0")
    & ~ ssSkP730("d2")
    & ~ ssSkP733("d2")
    & ssSkP731("d0")
    & ssSkP730("d1")
    & ~ ssSkP732("d2")
    & ssSkP731("d1")
    & ssSkP730("d0")
    & ssSkP737("d0")
    & ssSkP736("d1")
    & ~ ssSkP735("d2")
    & ssSkP737("d1")
    & ssSkP736("d0")
    & ~ ssSkP734("d2")
    & ~ ssSkP737("d2")
    & ssSkP735("d0")
    & ssSkP734("d1")
    & ~ ssSkP736("d2")
    & ssSkP735("d1")
    & ssSkP734("d0")
    & ~ 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")
    & ssSkP741("d1")
    & ssSkP742("d0")
    & ~ ssSkP743("d2")
    & ssSkP741("d0")
    & ssSkP742("d1")
    & ssSkP704("d0")
    & ssSkP703("d1")
    & ~ ssSkP702("d2")
    & ssSkP704("d1")
    & ssSkP703("d0")
    & ~ ssSkP701("d2")
    & ~ ssSkP704("d2")
    & ssSkP702("d0")
    & ssSkP701("d1")
    & ~ ssSkP703("d2")
    & ssSkP702("d1")
    & ssSkP701("d0")
    & ~ ssSkP708("d0")
    & ssSkP705("d2")
    & ~ ssSkP708("d1")
    & ~ ssSkP705("d1")
    & ~ ssSkP708("d2")
    & ~ ssSkP705("d0")
    & ~ ssSkP709("d2")
    & ~ ssSkP709("d1")
    & ~ ssSkP709("d0")
    & ssSkP846("d1","d0")
    & ssSkP846("d0","d1")
    & ~ ssSkP847("d2","d2")
    & ssSkP847("d1","d1")
    & ssSkP847("d0","d0")
    & ~ ssSkP846("d2","d2")
    & ssSkP846("d1","d1")
    & ssSkP846("d0","d0")
    & ssSkP847("d0","d1")
    & ssSkP847("d1","d0")
    & ~ ssSkP846("d2","d1")
    & ~ ssSkP846("d1","d2")
    & ssSkP847("d0","d2")
    & ~ ssSkP847("d2","d0")
    & ~ ssSkP846("d2","d0")
    & ~ ssSkP846("d0","d2")
    & ssSkP847("d1","d2")
    & ~ ssSkP847("d2","d1")
    & ~ ssSkP710("d1")
    & ~ ssSkP711("d0")
    & ~ ssSkP710("d0")
    & ~ ssSkP711("d1")
    & ~ ssSkP711("d2")
    & ~ ssSkP710("d2")
    & ssSkP715("d0")
    & ssSkP714("d1")
    & ~ ssSkP713("d2")
    & ssSkP715("d1")
    & ssSkP714("d0")
    & ~ ssSkP712("d2")
    & ~ ssSkP715("d2")
    & ssSkP712("d1")
    & ssSkP713("d0")
    & ~ ssSkP714("d2")
    & ssSkP712("d0")
    & ssSkP713("d1")
    & ssSkP719("d0")
    & ssSkP718("d1")
    & ~ ssSkP717("d2")
    & ssSkP719("d1")
    & ssSkP718("d0")
    & ~ ssSkP716("d2")
    & ~ ssSkP719("d2")
    & ssSkP717("d0")
    & ssSkP716("d1")
    & ~ ssSkP718("d2")
    & ssSkP717("d1")
    & ssSkP716("d0")
    & ssSkP722("d0")
    & ssSkP721("d1")
    & ~ ssSkP720("d2")
    & ssSkP722("d1")
    & ssSkP721("d0")
    & ~ ssSkP722("d2")
    & ssSkP720("d0")
    & ~ ssSkP721("d2")
    & ssSkP720("d1")
    & ssSkP769("d1")
    & ~ ssSkP768("d2")
    & ssSkP769("d0")
    & ~ ssSkP767("d2")
    & ssSkP767("d1")
    & ssSkP768("d0")
    & ~ ssSkP769("d2")
    & ssSkP767("d0")
    & ssSkP768("d1")
    & ~ ssSkP870("d2","d0")
    & ~ ssSkP870("d0","d2")
    & ssSkP871("d0","d1")
    & ssSkP871("d1","d0")
    & ~ ssSkP870("d2","d1")
    & ~ ssSkP870("d1","d2")
    & ~ ssSkP871("d2","d2")
    & ssSkP871("d1","d1")
    & ssSkP871("d0","d0")
    & ~ ssSkP870("d2","d2")
    & ssSkP870("d1","d1")
    & ssSkP870("d0","d0")
    & ssSkP871("d1","d2")
    & ~ ssSkP871("d2","d1")
    & ssSkP870("d1","d0")
    & ssSkP870("d0","d1")
    & ssSkP871("d0","d2")
    & ~ ssSkP871("d2","d0")
    & ssSkP773("d0")
    & ssSkP772("d1")
    & ~ ssSkP771("d2")
    & ssSkP773("d1")
    & ssSkP772("d0")
    & ~ ssSkP770("d2")
    & ~ ssSkP773("d2")
    & ssSkP771("d0")
    & ssSkP770("d1")
    & ~ ssSkP772("d2")
    & ssSkP771("d1")
    & ssSkP770("d0")
    & ssSkP777("d0")
    & ~ ssSkP776("d1")
    & ~ ssSkP775("d2")
    & ssSkP777("d1")
    & ssSkP776("d0")
    & ~ ssSkP774("d2")
    & ~ ssSkP777("d2")
    & ssSkP775("d0")
    & ssSkP774("d1")
    & ~ ssSkP776("d2")
    & ssSkP775("d1")
    & ssSkP774("d0")
    & ~ ssSkP779("d2")
    & ~ ssSkP778("d2")
    & ssSkP779("d0")
    & ssSkP778("d1")
    & ~ ssSkP779("d1")
    & ssSkP778("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")
    & ssSkP786("d2")
    & ~ ssSkP785("d2")
    & ssSkP785("d1")
    & ~ ssSkP786("d0")
    & ssSkP785("d0")
    & ~ ssSkP786("d1")
    & ~ ssSkP746("d2")
    & ~ ssSkP747("d1")
    & ~ ssSkP747("d0")
    & ~ ssSkP745("d2")
    & ssSkP746("d0")
    & ssSkP745("d1")
    & ssSkP746("d1")
    & ssSkP747("d2")
    & ssSkP745("d0")
    & ssSkP893("d1","d0")
    & ssSkP893("d0","d1")
    & ~ ssSkP894("d2","d2")
    & ssSkP894("d1","d1")
    & ssSkP894("d0","d0")
    & ~ ssSkP893("d2","d2")
    & ssSkP893("d1","d1")
    & ssSkP893("d0","d0")
    & ssSkP894("d0","d1")
    & ssSkP894("d1","d0")
    & ~ ssSkP893("d2","d1")
    & ~ ssSkP893("d1","d2")
    & ssSkP894("d0","d2")
    & ~ ssSkP894("d2","d0")
    & ~ ssSkP893("d2","d0")
    & ~ ssSkP893("d0","d2")
    & ssSkP894("d1","d2")
    & ~ ssSkP894("d2","d1")
    & ~ ssSkP751("d0")
    & ~ ssSkP750("d1")
    & ~ ssSkP751("d1")
    & ~ ssSkP750("d0")
    & ~ ssSkP751("d2")
    & ~ ssSkP750("d2")
    & ssSkP755("d0")
    & ssSkP754("d1")
    & ~ ssSkP753("d2")
    & ssSkP755("d1")
    & ssSkP754("d0")
    & ~ ssSkP752("d2")
    & ~ ssSkP755("d2")
    & ssSkP752("d1")
    & ssSkP753("d0")
    & ~ ssSkP754("d2")
    & ssSkP752("d0")
    & ssSkP753("d1")
    & ssSkP759("d0")
    & ~ ssSkP757("d2")
    & ssSkP758("d1")
    & ssSkP759("d1")
    & ssSkP758("d0")
    & ~ ssSkP756("d2")
    & ~ ssSkP759("d2")
    & ssSkP757("d0")
    & ~ ssSkP756("d1")
    & ssSkP757("d1")
    & ~ ssSkP758("d2")
    & ssSkP756("d0")
    & ssSkP762("d0")
    & ssSkP761("d1")
    & ~ ssSkP760("d2")
    & ssSkP762("d1")
    & ssSkP761("d0")
    & ~ ssSkP762("d2")
    & ssSkP760("d0")
    & ~ ssSkP761("d2")
    & ssSkP760("d1")
    & ~ ssSkP766("d0")
    & ssSkP763("d2")
    & ~ ssSkP766("d1")
    & ~ ssSkP763("d1")
    & ~ ssSkP766("d2")
    & ~ ssSkP763("d0")
    & ssSkP692("d0")
    & ssSkP691("d1")
    & ~ ssSkP690("d2")
    & ssSkP692("d1")
    & ssSkP691("d0")
    & ~ ssSkP692("d2")
    & ssSkP690("d0")
    & ~ ssSkP691("d2")
    & ssSkP690("d1")
    & ssSkP696("d0")
    & ~ ssSkP694("d2")
    & ssSkP695("d1")
    & ssSkP696("d1")
    & ssSkP695("d0")
    & ~ ssSkP693("d2")
    & ~ ssSkP696("d2")
    & ssSkP694("d0")
    & ssSkP693("d1")
    & ssSkP694("d1")
    & ~ ssSkP695("d2")
    & ssSkP693("d0")
    & ssSkP699("d1")
    & ~ ssSkP698("d2")
    & ssSkP699("d0")
    & ~ ssSkP697("d2")
    & ssSkP698("d0")
    & ssSkP697("d1")
    & ~ ssSkP699("d2")
    & ssSkP698("d1")
    & ssSkP697("d0")
    & ~ ssSkP669("d2")
    & ~ ssSkP668("d2")
    & ssSkP669("d0")
    & ssSkP668("d1")
    & ssSkP669("d1")
    & ssSkP668("d0")
    & ssSkP670("d0")
    & ssSkP670("d1")
    & ~ ssSkP670("d2")
    & ssSkP674("d0")
    & ~ ssSkP672("d2")
    & ssSkP673("d1")
    & ssSkP674("d1")
    & ssSkP673("d0")
    & ~ ssSkP671("d2")
    & ~ ssSkP674("d2")
    & ssSkP672("d0")
    & ssSkP671("d1")
    & ssSkP672("d1")
    & ~ ssSkP673("d2")
    & ssSkP671("d0")
    & ssSkP678("d0")
    & ssSkP677("d1")
    & ~ ssSkP676("d2")
    & ssSkP678("d1")
    & ssSkP677("d0")
    & ~ ssSkP675("d2")
    & ~ ssSkP678("d2")
    & ssSkP675("d1")
    & ssSkP676("d0")
    & ~ ssSkP677("d2")
    & ssSkP675("d0")
    & ssSkP676("d1")
    & ~ ssSkP679("d2")
    & ssSkP679("d1")
    & ssSkP679("d0")
    & ~ ssSkP680("d1")
    & ~ ssSkP680("d0")
    & ssSkP680("d2")
    & ssSkP685("d0")
    & ssSkP684("d1")
    & ~ ssSkP683("d2")
    & ssSkP685("d1")
    & ssSkP684("d0")
    & ~ ssSkP685("d2")
    & ssSkP683("d0")
    & ~ ssSkP684("d2")
    & ssSkP683("d1")
    & ssSkP688("d1")
    & ssSkP689("d0")
    & ~ ssSkP687("d2")
    & ssSkP688("d0")
    & ssSkP689("d1")
    & ~ ssSkP686("d2")
    & ~ ssSkP689("d2")
    & ssSkP687("d0")
    & ssSkP686("d1")
    & ~ ssSkP688("d2")
    & ~ ssSkP687("d1")
    & ssSkP686("d0")
    & ssSkP1143("d0")
    & ~ ssSkP1141("d2")
    & ssSkP1142("d1")
    & ssSkP1143("d1")
    & ssSkP1142("d0")
    & ~ ssSkP1140("d2")
    & ~ ssSkP1143("d2")
    & ssSkP1141("d0")
    & ssSkP1140("d1")
    & ssSkP1141("d1")
    & ~ ssSkP1142("d2")
    & ssSkP1140("d0")
    & ~ ssSkP1146("d1")
    & ~ ssSkP1145("d2")
    & ssSkP1147("d0")
    & ssSkP1146("d0")
    & ~ ssSkP1144("d2")
    & ~ ssSkP1147("d1")
    & ssSkP1144("d1")
    & ssSkP1145("d0")
    & ~ ssSkP1147("d2")
    & ssSkP1146("d2")
    & ssSkP1145("d1")
    & ssSkP1144("d0")
    & ssSkP1131("d1")
    & ssSkP1132("d0")
    & ~ ssSkP1130("d2")
    & ssSkP1131("d0")
    & ssSkP1132("d1")
    & ~ ssSkP1132("d2")
    & ssSkP1130("d0")
    & ~ ssSkP1131("d2")
    & ssSkP1130("d1")
    & ssSkP1135("d1")
    & ssSkP1136("d0")
    & ~ ssSkP1134("d2")
    & ssSkP1135("d0")
    & ssSkP1136("d1")
    & ~ ssSkP1133("d2")
    & ~ ssSkP1136("d2")
    & ssSkP1133("d1")
    & ssSkP1134("d0")
    & ~ ssSkP1135("d2")
    & ssSkP1133("d0")
    & ssSkP1134("d1")
    & ssSkP1139("d1")
    & ~ ssSkP1138("d2")
    & ssSkP1139("d0")
    & ~ ssSkP1137("d2")
    & ssSkP1137("d1")
    & ssSkP1138("d0")
    & ~ ssSkP1139("d2")
    & ssSkP1137("d0")
    & ssSkP1138("d1")
    & ~ ssSkP1119("d2")
    & ssSkP1119("d1")
    & ssSkP1119("d0")
    & ssSkP1121("d0")
    & ssSkP1120("d1")
    & ssSkP1121("d1")
    & ssSkP1120("d0")
    & ~ ssSkP1121("d2")
    & ~ ssSkP1120("d2")
    & ssSkP1125("d0")
    & ~ ssSkP1123("d2")
    & ssSkP1124("d1")
    & ssSkP1125("d1")
    & ssSkP1124("d0")
    & ~ ssSkP1122("d2")
    & ~ ssSkP1125("d2")
    & ssSkP1123("d0")
    & ssSkP1122("d1")
    & ssSkP1123("d1")
    & ~ ssSkP1124("d2")
    & ssSkP1122("d0")
    & ssSkP1129("d0")
    & ~ ssSkP1127("d2")
    & ssSkP1128("d1")
    & ssSkP1129("d1")
    & ssSkP1128("d0")
    & ~ ssSkP1126("d2")
    & ~ ssSkP1129("d2")
    & ssSkP1127("d0")
    & ssSkP1126("d1")
    & ssSkP1127("d1")
    & ~ ssSkP1128("d2")
    & ssSkP1126("d0")
    & ~ ssSkP1109("d2")
    & ~ ssSkP1108("d2")
    & ssSkP1108("d1")
    & ssSkP1109("d0")
    & ssSkP1108("d0")
    & ssSkP1109("d1")
    & ssSkP1110("d0")
    & ssSkP1110("d1")
    & ~ ssSkP1110("d2")
    & ssSkP1113("d1")
    & ssSkP1114("d0")
    & ~ ssSkP1112("d2")
    & ~ ssSkP1111("d2")
    & ssSkP1113("d0")
    & ssSkP1114("d1")
    & ssSkP1111("d1")
    & ~ ssSkP1114("d2")
    & ssSkP1112("d0")
    & ssSkP1111("d0")
    & ~ ssSkP1113("d2")
    & ssSkP1112("d1")
    & ssSkP1117("d1")
    & ssSkP1118("d0")
    & ~ ssSkP1116("d2")
    & ssSkP1117("d0")
    & ssSkP1118("d1")
    & ~ ssSkP1115("d2")
    & ~ ssSkP1118("d2")
    & ssSkP1115("d1")
    & ssSkP1116("d0")
    & ~ ssSkP1117("d2")
    & ssSkP1115("d0")
    & ssSkP1116("d1")
    & ssSkP1102("d1")
    & ~ ssSkP1101("d2")
    & ssSkP1103("d0")
    & ~ ssSkP1102("d0")
    & ~ ssSkP1100("d2")
    & ssSkP1103("d1")
    & ~ ssSkP1101("d0")
    & ssSkP1100("d1")
    & ~ ssSkP1103("d2")
    & ~ ssSkP1102("d2")
    & ssSkP1101("d1")
    & ~ ssSkP1100("d0")
    & ~ ssSkP1105("d2")
    & ssSkP1106("d1")
    & ssSkP1107("d0")
    & ~ ssSkP1104("d2")
    & ssSkP1106("d0")
    & ssSkP1107("d1")
    & ssSkP1104("d1")
    & ssSkP1105("d0")
    & ~ ssSkP1107("d2")
    & ssSkP1104("d0")
    & ssSkP1105("d1")
    & ~ ssSkP1106("d2")
    & ssSkP918("d1","d2")
    & ~ ssSkP918("d2","d1")
    & ssSkP918("d0","d2")
    & ~ ssSkP918("d2","d0")
    & ssSkP918("d0","d1")
    & ssSkP918("d1","d0")
    & ~ ssSkP918("d2","d2")
    & ssSkP918("d1","d1")
    & ssSkP918("d0","d0")
    & ~ ssSkP917("d2","d2")
    & ssSkP917("d1","d1")
    & ssSkP917("d0","d0")
    & ssSkP917("d1","d0")
    & ssSkP917("d0","d1")
    & ~ ssSkP917("d2","d0")
    & ~ ssSkP917("d0","d2")
    & ~ ssSkP917("d2","d1")
    & ~ ssSkP917("d1","d2")
    & ssSkP938("d1","d0")
    & ssSkP938("d0","d1")
    & ~ ssSkP939("d2","d2")
    & ssSkP939("d1","d1")
    & ssSkP939("d0","d0")
    & ~ ssSkP938("d2","d2")
    & ssSkP938("d1","d1")
    & ssSkP938("d0","d0")
    & ssSkP939("d0","d1")
    & ssSkP939("d1","d0")
    & ~ ssSkP938("d2","d1")
    & ~ ssSkP938("d1","d2")
    & ~ ssSkP939("d0","d2")
    & ~ ssSkP939("d2","d0")
    & ~ ssSkP938("d2","d0")
    & ~ ssSkP938("d0","d2")
    & ~ ssSkP939("d1","d2")
    & ~ ssSkP939("d2","d1")
    & ~ ssSkP605("d0")
    & ~ ssSkP604("d1")
    & ~ ssSkP603("d2")
    & ~ ssSkP605("d1")
    & ~ ssSkP604("d0")
    & ~ ssSkP602("d2")
    & ~ ssSkP605("d2")
    & ~ ssSkP603("d0")
    & ~ ssSkP602("d1")
    & ~ ssSkP604("d2")
    & ~ ssSkP603("d1")
    & ~ ssSkP602("d0")
    & ~ ssSkP609("d0")
    & ~ ssSkP608("d1")
    & ~ ssSkP607("d2")
    & ~ ssSkP609("d1")
    & ~ ssSkP608("d0")
    & ~ ssSkP606("d2")
    & ~ ssSkP609("d2")
    & ~ ssSkP606("d1")
    & ~ ssSkP607("d0")
    & ~ ssSkP608("d2")
    & ssSkP606("d0")
    & ~ ssSkP607("d1")
    & ~ ssSkP612("d0")
    & ~ ssSkP610("d2")
    & ~ ssSkP611("d1")
    & ~ ssSkP612("d1")
    & ~ ssSkP611("d0")
    & ~ ssSkP612("d2")
    & ~ ssSkP610("d0")
    & ~ ssSkP610("d1")
    & ~ ssSkP611("d2")
    & ~ ssSkP616("d0")
    & ~ ssSkP615("d1")
    & ~ ssSkP614("d2")
    & ~ ssSkP616("d1")
    & ~ ssSkP615("d0")
    & ~ ssSkP613("d2")
    & ~ ssSkP616("d2")
    & ~ ssSkP614("d0")
    & ~ ssSkP613("d1")
    & ~ ssSkP615("d2")
    & ~ ssSkP614("d1")
    & ~ ssSkP613("d0")
    & ~ ssSkP618("d2")
    & ~ ssSkP619("d1")
    & ~ ssSkP619("d0")
    & ~ ssSkP617("d2")
    & ~ ssSkP618("d0")
    & ~ ssSkP617("d1")
    & ssSkP618("d1")
    & ~ ssSkP619("d2")
    & ~ ssSkP617("d0")
    & ssSkP961("d1","d2")
    & ~ ssSkP961("d2","d1")
    & ssSkP961("d0","d2")
    & ~ ssSkP961("d2","d0")
    & ssSkP961("d0","d1")
    & ssSkP961("d1","d0")
    & ~ ssSkP961("d2","d2")
    & ssSkP961("d1","d1")
    & ssSkP961("d0","d0")
    & ~ ssSkP960("d2","d2")
    & ssSkP960("d1","d1")
    & ssSkP960("d0","d0")
    & ssSkP960("d1","d0")
    & ssSkP960("d0","d1")
    & ~ ssSkP960("d2","d0")
    & ~ ssSkP960("d0","d2")
    & ~ ssSkP960("d2","d1")
    & ~ ssSkP960("d1","d2")
    & ~ ssSkP622("d1")
    & ~ ssSkP623("d0")
    & ~ ssSkP621("d2")
    & ~ ssSkP622("d0")
    & ~ ssSkP623("d1")
    & ~ ssSkP620("d2")
    & ssSkP623("d2")
    & ~ ssSkP621("d0")
    & ~ ssSkP620("d1")
    & ~ ssSkP622("d2")
    & ~ ssSkP621("d1")
    & ~ ssSkP620("d0")
    & ~ ssSkP983("d2","d1")
    & ~ ssSkP983("d1","d2")
    & ssSkP984("d0","d2")
    & ~ ssSkP984("d2","d0")
    & ~ ssSkP983("d2","d0")
    & ~ ssSkP983("d0","d2")
    & ssSkP984("d1","d2")
    & ~ ssSkP984("d2","d1")
    & ssSkP983("d1","d0")
    & ssSkP983("d0","d1")
    & ~ ssSkP984("d2","d2")
    & ssSkP984("d1","d1")
    & ssSkP984("d0","d0")
    & ~ ssSkP983("d2","d2")
    & ssSkP983("d1","d1")
    & ssSkP983("d0","d0")
    & ssSkP984("d0","d1")
    & ssSkP984("d1","d0")
    & ssSkP648("d1")
    & ~ ssSkP649("d0")
    & ~ ssSkP647("d2")
    & ~ ssSkP648("d0")
    & ~ ssSkP649("d1")
    & ~ ssSkP646("d2")
    & ~ ssSkP649("d2")
    & ~ ssSkP647("d0")
    & ~ ssSkP646("d1")
    & ~ ssSkP648("d2")
    & ~ ssSkP647("d1")
    & ~ ssSkP646("d0")
    & ~ ssSkP651("d1")
    & ~ ssSkP652("d0")
    & ~ ssSkP650("d2")
    & ssSkP651("d0")
    & ~ ssSkP652("d1")
    & ~ ssSkP652("d2")
    & ~ ssSkP650("d0")
    & ~ ssSkP651("d2")
    & ~ ssSkP650("d1")
    & ~ ssSkP655("d1")
    & ~ ssSkP656("d0")
    & ~ ssSkP654("d2")
    & ~ ssSkP655("d0")
    & ~ ssSkP656("d1")
    & ~ ssSkP653("d2")
    & ssSkP656("d2")
    & ~ ssSkP654("d0")
    & ~ ssSkP653("d1")
    & ~ ssSkP655("d2")
    & ~ ssSkP654("d1")
    & ~ ssSkP653("d0")
    & ssSkP659("d1")
    & ssSkP659("d0")
    & ~ ssSkP659("d2")
    & ssSkP663("d0")
    & ssSkP662("d1")
    & ~ ssSkP661("d2")
    & ssSkP663("d1")
    & ssSkP662("d0")
    & ~ ssSkP660("d2")
    & ~ ssSkP663("d2")
    & ssSkP661("d0")
    & ssSkP660("d1")
    & ~ ssSkP662("d2")
    & ssSkP661("d1")
    & ssSkP660("d0")
    & ssSkP667("d0")
    & ssSkP666("d1")
    & ~ ssSkP665("d2")
    & ssSkP667("d1")
    & ssSkP666("d0")
    & ~ ssSkP664("d2")
    & ~ ssSkP667("d2")
    & ssSkP665("d0")
    & ssSkP664("d1")
    & ~ ssSkP666("d2")
    & ssSkP665("d1")
    & ssSkP664("d0")
    & ssSkP627("d0")
    & ssSkP626("d1")
    & ssSkP627("d1")
    & ssSkP626("d0")
    & ~ ssSkP627("d2")
    & ~ ssSkP626("d2")
    & ~ ssSkP629("d2")
    & ~ ssSkP628("d2")
    & ssSkP628("d1")
    & ssSkP629("d0")
    & ssSkP628("d0")
    & ssSkP629("d1")
    & ssSkP630("d0")
    & ssSkP630("d1")
    & ~ ssSkP630("d2")
    & ssSkP634("d0")
    & ~ ssSkP632("d2")
    & ssSkP633("d1")
    & ssSkP634("d1")
    & ssSkP633("d0")
    & ~ ssSkP631("d2")
    & ~ ssSkP634("d2")
    & ssSkP632("d0")
    & ssSkP631("d1")
    & ssSkP632("d1")
    & ~ ssSkP633("d2")
    & 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")
    & ~ ssSkP645("d0")
    & ~ ssSkP644("d1")
    & ~ ssSkP643("d2")
    & ~ ssSkP645("d1")
    & ~ ssSkP644("d0")
    & ~ ssSkP642("d2")
    & ~ ssSkP645("d2")
    & ~ ssSkP643("d0")
    & ~ ssSkP642("d1")
    & ~ ssSkP644("d2")
    & ~ ssSkP643("d1")
    & ~ ssSkP642("d0")
    & ~ ssSkP569("d2")
    & ssSkP569("d1")
    & ssSkP569("d0")
    & ssSkP571("d0")
    & ssSkP570("d1")
    & ssSkP571("d1")
    & ssSkP570("d0")
    & ~ ssSkP571("d2")
    & ~ ssSkP570("d2")
    & ssSkP575("d0")
    & ssSkP574("d1")
    & ~ ssSkP573("d2")
    & ssSkP575("d1")
    & ssSkP574("d0")
    & ~ ssSkP572("d2")
    & ~ ssSkP575("d2")
    & ssSkP572("d1")
    & ssSkP573("d0")
    & ~ ssSkP574("d2")
    & ssSkP572("d0")
    & ssSkP573("d1")
    & ssSkP579("d0")
    & ssSkP576("d2")
    & ssSkP579("d1")
    & ~ ssSkP576("d1")
    & ~ ssSkP579("d2")
    & ~ ssSkP576("d0")
    & ssSkP582("d0")
    & ssSkP581("d1")
    & ~ ssSkP580("d2")
    & ssSkP582("d1")
    & ssSkP581("d0")
    & ~ ssSkP582("d2")
    & ssSkP580("d0")
    & ~ ssSkP581("d2")
    & ssSkP580("d1")
    & ssSkP586("d0")
    & ssSkP585("d1")
    & ~ ssSkP584("d2")
    & ssSkP586("d1")
    & ssSkP585("d0")
    & ~ ssSkP583("d2")
    & ~ ssSkP586("d2")
    & ssSkP584("d0")
    & ssSkP583("d1")
    & ~ ssSkP585("d2")
    & ssSkP584("d1")
    & ssSkP583("d0")
    & ~ ssSkP588("d2")
    & ssSkP589("d1")
    & ssSkP589("d0")
    & ~ ssSkP587("d2")
    & ssSkP588("d0")
    & ssSkP587("d1")
    & ssSkP588("d1")
    & ~ ssSkP589("d2")
    & ssSkP587("d0")
    & ~ ssSkP549("d1")
    & ~ ssSkP548("d2")
    & ~ ssSkP549("d0")
    & ~ ssSkP547("d2")
    & ~ ssSkP548("d0")
    & ~ ssSkP547("d1")
    & ~ ssSkP549("d2")
    & ~ ssSkP548("d1")
    & ~ ssSkP547("d0")
    & ssSkP553("d0")
    & ~ ssSkP552("d1")
    & ~ ssSkP551("d2")
    & ~ ssSkP553("d1")
    & ~ ssSkP552("d0")
    & ~ ssSkP550("d2")
    & ~ ssSkP553("d2")
    & ~ ssSkP551("d0")
    & ~ ssSkP550("d1")
    & ~ ssSkP552("d2")
    & ~ ssSkP551("d1")
    & ~ ssSkP550("d0")
    & ~ ssSkP557("d0")
    & ~ ssSkP555("d2")
    & ~ ssSkP556("d1")
    & ~ ssSkP557("d1")
    & ~ ssSkP556("d0")
    & ~ ssSkP554("d2")
    & ~ ssSkP557("d2")
    & ~ ssSkP555("d0")
    & ~ ssSkP554("d1")
    & ~ ssSkP555("d1")
    & ~ ssSkP556("d2")
    & ~ ssSkP554("d0")
    & ssSkP559("d2")
    & ~ ssSkP558("d2")
    & ~ ssSkP558("d1")
    & ~ ssSkP559("d0")
    & ~ ssSkP558("d0")
    & ~ ssSkP559("d1")
    & ssSkP564("d0")
    & ssSkP563("d1")
    & ~ ssSkP562("d2")
    & ssSkP564("d1")
    & ssSkP563("d0")
    & ~ ssSkP564("d2")
    & ssSkP562("d0")
    & ~ ssSkP563("d2")
    & ssSkP562("d1")
    & ssSkP567("d1")
    & ssSkP568("d0")
    & ~ ssSkP566("d2")
    & ssSkP567("d0")
    & ~ ssSkP568("d1")
    & ~ ssSkP565("d2")
    & ~ ssSkP568("d2")
    & ssSkP566("d0")
    & ssSkP565("d1")
    & ~ ssSkP567("d2")
    & ~ ssSkP566("d1")
    & ssSkP565("d0")
    & ssSkP593("d0")
    & ~ ssSkP591("d2")
    & ssSkP592("d1")
    & ~ ssSkP593("d1")
    & ssSkP592("d0")
    & ~ ssSkP590("d2")
    & ~ ssSkP593("d2")
    & ssSkP591("d0")
    & ~ ssSkP590("d1")
    & ssSkP591("d1")
    & ~ ssSkP592("d2")
    & ssSkP590("d0")
    & ssSkP597("d0")
    & ssSkP596("d1")
    & ~ ssSkP595("d2")
    & ssSkP597("d1")
    & ssSkP596("d0")
    & ~ ssSkP594("d2")
    & ~ ssSkP597("d2")
    & ssSkP594("d1")
    & ssSkP595("d0")
    & ~ ssSkP596("d2")
    & ssSkP594("d0")
    & ssSkP595("d1")
    & ssSkP599("d2")
    & ~ ssSkP598("d2")
    & ssSkP598("d1")
    & ~ ssSkP599("d0")
    & ssSkP598("d0")
    & ~ ssSkP599("d1")
    & ~ ssSkP924("d0")
    & ~ ssSkP923("d1")
    & ~ ssSkP922("d2")
    & ~ ssSkP924("d1")
    & ~ ssSkP923("d0")
    & ~ ssSkP921("d2")
    & ~ ssSkP924("d2")
    & ~ ssSkP922("d0")
    & ~ ssSkP921("d1")
    & ~ ssSkP923("d2")
    & ~ ssSkP922("d1")
    & ~ ssSkP921("d0")
    & ssSkP927("d1")
    & ssSkP928("d0")
    & ~ ssSkP926("d2")
    & ssSkP927("d0")
    & ssSkP928("d1")
    & ~ ssSkP925("d2")
    & ~ ssSkP928("d2")
    & ~ ssSkP925("d1")
    & ~ ssSkP926("d0")
    & ~ ssSkP927("d2")
    & ~ ssSkP925("d0")
    & ~ ssSkP926("d1")
    & ~ ssSkP929("d2")
    & ssSkP929("d1")
    & ssSkP929("d0")
    & ssSkP930("d1")
    & ssSkP931("d0")
    & ssSkP930("d0")
    & ssSkP931("d1")
    & ~ ssSkP931("d2")
    & ~ ssSkP930("d2")
    & ssSkP935("d0")
    & ssSkP934("d1")
    & ~ ssSkP933("d2")
    & ssSkP935("d1")
    & ssSkP934("d0")
    & ~ ssSkP932("d2")
    & ~ ssSkP935("d2")
    & ssSkP933("d0")
    & ssSkP932("d1")
    & ~ ssSkP934("d2")
    & ssSkP933("d1")
    & ssSkP932("d0")
    & ssSkP937("d2")
    & ~ ssSkP936("d2")
    & ssSkP936("d1")
    & ~ ssSkP937("d0")
    & ssSkP936("d0")
    & ~ ssSkP937("d1")
    & ~ ssSkP942("d0")
    & ~ ssSkP941("d1")
    & ~ ssSkP940("d2")
    & ~ ssSkP942("d1")
    & ~ ssSkP941("d0")
    & ~ ssSkP942("d2")
    & ~ ssSkP940("d0")
    & ~ ssSkP941("d2")
    & ~ ssSkP940("d1")
    & ssSkP902("d0")
    & ~ ssSkP901("d1")
    & ~ ssSkP900("d2")
    & ssSkP902("d1")
    & ~ ssSkP901("d0")
    & ~ ssSkP902("d2")
    & ~ ssSkP900("d0")
    & ~ ssSkP901("d2")
    & ~ ssSkP900("d1")
    & ssSkP906("d0")
    & ssSkP905("d1")
    & ~ ssSkP904("d2")
    & ssSkP906("d1")
    & ssSkP905("d0")
    & ~ ssSkP903("d2")
    & ~ ssSkP906("d2")
    & ssSkP904("d0")
    & ssSkP903("d1")
    & ~ ssSkP905("d2")
    & ssSkP904("d1")
    & ssSkP903("d0")
    & ssSkP909("d1")
    & ~ ssSkP908("d2")
    & ssSkP909("d0")
    & ~ ssSkP907("d2")
    & ssSkP907("d1")
    & ssSkP908("d0")
    & ~ ssSkP909("d2")
    & ssSkP907("d0")
    & ssSkP908("d1")
    & ssSkP913("d0")
    & ssSkP912("d1")
    & ~ ssSkP911("d2")
    & ssSkP913("d1")
    & ssSkP912("d0")
    & ~ ssSkP910("d2")
    & ~ ssSkP913("d2")
    & ssSkP911("d0")
    & ssSkP910("d1")
    & ~ ssSkP912("d2")
    & ssSkP911("d1")
    & ssSkP910("d0")
    & ~ ssSkP915("d2")
    & ~ ssSkP916("d1")
    & ~ ssSkP916("d0")
    & ~ ssSkP914("d2")
    & ssSkP915("d0")
    & ssSkP914("d1")
    & ssSkP915("d1")
    & ssSkP916("d2")
    & ssSkP914("d0")
    & ~ ssSkP919("d2")
    & ~ ssSkP919("d0")
    & ~ ssSkP919("d1")
    & ~ ssSkP920("d0")
    & ~ ssSkP920("d1")
    & ~ ssSkP920("d2")
    & ssSkP967("d1")
    & ssSkP968("d0")
    & ~ ssSkP966("d2")
    & ssSkP967("d0")
    & ssSkP968("d1")
    & ~ ssSkP965("d2")
    & ~ ssSkP968("d2")
    & ssSkP966("d0")
    & ssSkP965("d1")
    & ~ ssSkP967("d2")
    & ~ ssSkP966("d1")
    & ssSkP965("d0")
    & ~ ssSkP969("d2")
    & ssSkP969("d1")
    & ssSkP969("d0")
    & ssSkP971("d0")
    & ssSkP970("d1")
    & ssSkP971("d1")
    & ssSkP970("d0")
    & ~ ssSkP971("d2")
    & ~ ssSkP970("d2")
    & ssSkP974("d1")
    & ssSkP975("d0")
    & ~ ssSkP973("d2")
    & ssSkP974("d0")
    & ssSkP975("d1")
    & ~ ssSkP972("d2")
    & ~ ssSkP975("d2")
    & ssSkP973("d0")
    & ssSkP972("d1")
    & ~ ssSkP974("d2")
    & ~ ssSkP973("d1")
    & ssSkP972("d0")
    & ssSkP979("d0")
    & ssSkP978("d1")
    & ~ ssSkP977("d2")
    & ssSkP979("d1")
    & ssSkP978("d0")
    & ~ ssSkP976("d2")
    & ~ ssSkP979("d2")
    & ssSkP977("d0")
    & ssSkP976("d1")
    & ~ ssSkP978("d2")
    & ssSkP977("d1")
    & ssSkP976("d0")
    & ssSkP600("d1","d0")
    & ssSkP600("d0","d1")
    & ~ ssSkP601("d2","d2")
    & ssSkP601("d1","d1")
    & ssSkP601("d0","d0")
    & ~ ssSkP600("d2","d2")
    & ssSkP600("d1","d1")
    & ssSkP600("d0","d0")
    & ssSkP601("d0","d1")
    & ssSkP601("d1","d0")
    & ~ ssSkP600("d2","d1")
    & ~ ssSkP600("d1","d2")
    & ~ ssSkP601("d0","d2")
    & ~ ssSkP601("d2","d0")
    & ~ ssSkP600("d2","d0")
    & ~ ssSkP600("d0","d2")
    & ~ ssSkP601("d1","d2")
    & ~ ssSkP601("d2","d1")
    & ssSkP981("d1")
    & ~ ssSkP982("d0")
    & ~ ssSkP980("d2")
    & ssSkP981("d0")
    & ~ ssSkP982("d1")
    & ssSkP982("d2")
    & ssSkP980("d0")
    & ~ ssSkP981("d2")
    & ssSkP980("d1")
    & ~ ssSkP986("d0")
    & ~ ssSkP985("d1")
    & ~ ssSkP986("d1")
    & ~ ssSkP985("d0")
    & ~ ssSkP986("d2")
    & ~ ssSkP985("d2")
    & ~ ssSkP946("d0")
    & ~ ssSkP944("d2")
    & ~ ssSkP945("d1")
    & ~ ssSkP946("d1")
    & ~ ssSkP945("d0")
    & ~ ssSkP943("d2")
    & ~ ssSkP946("d2")
    & ~ ssSkP944("d0")
    & ~ ssSkP943("d1")
    & ssSkP944("d1")
    & ~ ssSkP945("d2")
    & ~ ssSkP943("d0")
    & ~ ssSkP949("d1")
    & ~ ssSkP948("d2")
    & ~ ssSkP949("d0")
    & ~ ssSkP947("d2")
    & ~ ssSkP948("d0")
    & ~ ssSkP947("d1")
    & ~ ssSkP949("d2")
    & ~ ssSkP948("d1")
    & ~ ssSkP947("d0")
    & ~ 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")
    & ~ ssSkP956("d1")
    & ~ ssSkP955("d2")
    & ~ ssSkP957("d1")
    & ~ ssSkP956("d0")
    & ~ ssSkP954("d2")
    & ~ ssSkP957("d2")
    & ~ ssSkP955("d0")
    & ~ ssSkP954("d1")
    & ~ ssSkP956("d2")
    & ~ ssSkP955("d1")
    & ~ ssSkP954("d0")
    & ssSkP959("d2")
    & ~ ssSkP958("d2")
    & ~ ssSkP958("d1")
    & ~ ssSkP959("d0")
    & ~ ssSkP958("d0")
    & ~ ssSkP959("d1")
    & ssSkP963("d1")
    & ssSkP964("d0")
    & ~ ssSkP962("d2")
    & ssSkP963("d0")
    & ssSkP964("d1")
    & ~ ssSkP964("d2")
    & ~ ssSkP962("d0")
    & ~ ssSkP963("d2")
    & ~ ssSkP962("d1")
    & ~ ssSkP624("d2","d1")
    & ~ ssSkP624("d1","d2")
    & ssSkP625("d0","d2")
    & ~ ssSkP625("d2","d0")
    & ~ ssSkP624("d2","d0")
    & ~ ssSkP624("d0","d2")
    & ssSkP625("d1","d2")
    & ~ ssSkP625("d2","d1")
    & ssSkP624("d1","d0")
    & ssSkP624("d0","d1")
    & ~ ssSkP625("d2","d2")
    & ssSkP625("d1","d1")
    & ssSkP625("d0","d0")
    & ~ ssSkP624("d2","d2")
    & ssSkP624("d1","d1")
    & ssSkP624("d0","d0")
    & ssSkP625("d0","d1")
    & ssSkP625("d1","d0")
    & ssSkP640("d1","d0")
    & ssSkP640("d0","d1")
    & ~ ssSkP641("d2","d2")
    & ssSkP641("d1","d1")
    & ssSkP641("d0","d0")
    & ~ ssSkP640("d2","d2")
    & ssSkP640("d1","d1")
    & ssSkP640("d0","d0")
    & ssSkP641("d0","d1")
    & ssSkP641("d1","d0")
    & ~ ssSkP640("d2","d1")
    & ~ ssSkP640("d1","d2")
    & ~ ssSkP641("d0","d2")
    & ~ ssSkP641("d2","d0")
    & ~ ssSkP640("d2","d0")
    & ~ ssSkP640("d0","d2")
    & ~ ssSkP641("d1","d2")
    & ~ ssSkP641("d2","d1")
    & ~ ssSkP988("d2")
    & ssSkP989("d1")
    & ssSkP989("d0")
    & ~ ssSkP987("d2")
    & ssSkP988("d0")
    & ~ ssSkP987("d1")
    & ssSkP988("d1")
    & ~ ssSkP989("d2")
    & ~ ssSkP987("d0")
    & ssSkP993("d0")
    & ~ ssSkP991("d2")
    & ssSkP992("d1")
    & ssSkP993("d1")
    & ssSkP992("d0")
    & ~ ssSkP990("d2")
    & ~ ssSkP993("d2")
    & ssSkP991("d0")
    & ~ ssSkP990("d1")
    & ssSkP991("d1")
    & ~ ssSkP992("d2")
    & ssSkP990("d0")
    & ssSkP997("d0")
    & ssSkP996("d1")
    & ~ ssSkP995("d2")
    & ssSkP997("d1")
    & ssSkP996("d0")
    & ~ ssSkP994("d2")
    & ~ ssSkP997("d2")
    & ssSkP995("d0")
    & ssSkP994("d1")
    & ~ ssSkP996("d2")
    & ssSkP995("d1")
    & ssSkP994("d0")
    & ~ ssSkP999("d2")
    & ~ ssSkP998("d2")
    & ssSkP999("d0")
    & ~ ssSkP998("d1")
    & ssSkP999("d1")
    & ssSkP998("d0")
    & ~ ssSkP657("d2","d1")
    & ~ ssSkP657("d1","d2")
    & ssSkP658("d0","d2")
    & ~ ssSkP658("d2","d0")
    & ~ ssSkP657("d2","d0")
    & ~ ssSkP657("d0","d2")
    & ssSkP658("d1","d2")
    & ~ ssSkP658("d2","d1")
    & ssSkP657("d1","d0")
    & ssSkP657("d0","d1")
    & ~ ssSkP658("d2","d2")
    & ssSkP658("d1","d1")
    & ssSkP658("d0","d0")
    & ~ ssSkP657("d2","d2")
    & ssSkP657("d1","d1")
    & ssSkP657("d0","d0")
    & ssSkP658("d0","d1")
    & ssSkP658("d1","d0")
    & ssSkP561("d1","d2")
    & ~ ssSkP561("d2","d1")
    & ssSkP561("d0","d2")
    & ~ ssSkP561("d2","d0")
    & ssSkP561("d0","d1")
    & ssSkP561("d1","d0")
    & ~ ssSkP561("d2","d2")
    & ssSkP561("d1","d1")
    & ssSkP561("d0","d0")
    & ~ ssSkP560("d2","d2")
    & ssSkP560("d1","d1")
    & ssSkP560("d0","d0")
    & ssSkP560("d1","d0")
    & ssSkP560("d0","d1")
    & ~ ssSkP560("d2","d0")
    & ~ ssSkP560("d0","d2")
    & ~ ssSkP560("d2","d1")
    & ~ ssSkP560("d1","d2")
    & ~ ssSkP577("d2","d0")
    & ~ ssSkP577("d0","d2")
    & ssSkP578("d0","d1")
    & ssSkP578("d1","d0")
    & ~ ssSkP577("d2","d1")
    & ~ ssSkP577("d1","d2")
    & ~ ssSkP578("d2","d2")
    & ssSkP578("d1","d1")
    & ssSkP578("d0","d0")
    & ~ ssSkP577("d2","d2")
    & ssSkP577("d1","d1")
    & ssSkP577("d0","d0")
    & ssSkP578("d1","d2")
    & ~ ssSkP578("d2","d1")
    & ssSkP577("d1","d0")
    & ssSkP577("d0","d1")
    & ssSkP578("d0","d2")
    & ~ ssSkP578("d2","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")
    & ~ ssSkP803("d0")
    & ~ ssSkP802("d1")
    & ~ ssSkP801("d2")
    & ~ ssSkP803("d1")
    & ~ ssSkP802("d0")
    & ~ ssSkP800("d2")
    & ~ ssSkP803("d2")
    & ~ ssSkP801("d0")
    & ~ ssSkP800("d1")
    & ~ ssSkP802("d2")
    & ~ ssSkP801("d1")
    & ~ ssSkP800("d0")
    & ssSkP807("d0")
    & ssSkP804("d2")
    & ssSkP807("d1")
    & ~ ssSkP804("d1")
    & ~ ssSkP807("d2")
    & ~ ssSkP804("d0")
    & ~ ssSkP809("d2")
    & ~ ssSkP808("d2")
    & ssSkP809("d0")
    & ssSkP808("d1")
    & ssSkP809("d1")
    & ssSkP808("d0")
    & ssSkP810("d0")
    & ~ ssSkP810("d1")
    & ~ ssSkP810("d2")
    & ssSkP814("d0")
    & ssSkP813("d1")
    & ~ ssSkP812("d2")
    & ssSkP814("d1")
    & ssSkP813("d0")
    & ~ ssSkP811("d2")
    & ~ ssSkP814("d2")
    & ssSkP811("d1")
    & ssSkP812("d0")
    & ~ ssSkP813("d2")
    & ssSkP811("d0")
    & ssSkP812("d1")
    & ssSkP818("d0")
    & ~ ssSkP816("d2")
    & ssSkP817("d1")
    & ssSkP818("d1")
    & ssSkP817("d0")
    & ~ ssSkP815("d2")
    & ~ ssSkP818("d2")
    & ssSkP816("d0")
    & ssSkP815("d1")
    & ssSkP816("d1")
    & ~ ssSkP817("d2")
    & ssSkP815("d0")
    & ~ ssSkP819("d2")
    & ssSkP819("d1")
    & ssSkP819("d0")
    & ssSkP821("d0")
    & ~ ssSkP820("d1")
    & ssSkP821("d1")
    & ssSkP820("d0")
    & ~ ssSkP821("d2")
    & ~ ssSkP820("d2")
    & ssSkP845("d2")
    & ~ ssSkP844("d2")
    & ssSkP844("d1")
    & ~ ssSkP845("d0")
    & ssSkP844("d0")
    & ~ ssSkP845("d1")
    & ~ ssSkP849("d2")
    & ~ ssSkP848("d2")
    & ssSkP849("d0")
    & ssSkP848("d1")
    & ssSkP849("d1")
    & ssSkP848("d0")
    & ~ ssSkP706("d2","d0")
    & ~ ssSkP706("d0","d2")
    & ssSkP707("d0","d1")
    & ssSkP707("d1","d0")
    & ~ ssSkP706("d2","d1")
    & ~ ssSkP706("d1","d2")
    & ~ ssSkP707("d2","d2")
    & ssSkP707("d1","d1")
    & ssSkP707("d0","d0")
    & ~ ssSkP706("d2","d2")
    & ssSkP706("d1","d1")
    & ssSkP706("d0","d0")
    & ssSkP707("d1","d2")
    & ~ ssSkP707("d2","d1")
    & ssSkP706("d1","d0")
    & ssSkP706("d0","d1")
    & ssSkP707("d0","d2")
    & ~ ssSkP707("d2","d0")
    & ssSkP850("d0")
    & ~ ssSkP850("d1")
    & ~ ssSkP850("d2")
    & ssSkP854("d0")
    & ssSkP853("d1")
    & ~ ssSkP852("d2")
    & ssSkP854("d1")
    & ssSkP853("d0")
    & ~ ssSkP851("d2")
    & ~ ssSkP854("d2")
    & ssSkP851("d1")
    & ssSkP852("d0")
    & ~ ssSkP853("d2")
    & ssSkP851("d0")
    & ssSkP852("d1")
    & ssSkP858("d0")
    & ~ ssSkP856("d2")
    & ssSkP857("d1")
    & ssSkP858("d1")
    & ssSkP857("d0")
    & ~ ssSkP855("d2")
    & ~ ssSkP858("d2")
    & ssSkP856("d0")
    & ssSkP855("d1")
    & ssSkP856("d1")
    & ~ ssSkP857("d2")
    & ssSkP855("d0")
    & ~ ssSkP859("d2")
    & ssSkP859("d1")
    & ssSkP859("d0")
    & ssSkP861("d0")
    & ssSkP860("d1")
    & ssSkP861("d1")
    & ssSkP860("d0")
    & ~ ssSkP861("d2")
    & ~ ssSkP860("d2")
    & ssSkP865("d0")
    & ~ ssSkP863("d2")
    & ssSkP864("d1")
    & ssSkP865("d1")
    & ssSkP864("d0")
    & ~ ssSkP862("d2")
    & ~ ssSkP865("d2")
    & ssSkP863("d0")
    & ssSkP862("d1")
    & ssSkP863("d1")
    & ~ ssSkP864("d2")
    & ssSkP862("d0")
    & ssSkP825("d0")
    & ssSkP824("d1")
    & ~ ssSkP823("d2")
    & ssSkP825("d1")
    & ssSkP824("d0")
    & ~ ssSkP822("d2")
    & ~ ssSkP825("d2")
    & ssSkP823("d0")
    & ssSkP822("d1")
    & ~ ssSkP824("d2")
    & ssSkP823("d1")
    & ssSkP822("d0")
    & ssSkP827("d2")
    & ~ ssSkP826("d2")
    & ssSkP826("d1")
    & ~ ssSkP827("d0")
    & ssSkP826("d0")
    & ~ ssSkP827("d1")
    & ssSkP725("d1","d0")
    & ssSkP725("d0","d1")
    & ~ ssSkP726("d2","d2")
    & ssSkP726("d1","d1")
    & ssSkP726("d0","d0")
    & ~ ssSkP725("d2","d2")
    & ssSkP725("d1","d1")
    & ssSkP725("d0","d0")
    & ssSkP726("d0","d1")
    & ssSkP726("d1","d0")
    & ~ ssSkP725("d2","d1")
    & ~ ssSkP725("d1","d2")
    & ssSkP726("d0","d2")
    & ~ ssSkP726("d2","d0")
    & ~ ssSkP725("d2","d0")
    & ~ ssSkP725("d0","d2")
    & ssSkP726("d1","d2")
    & ~ ssSkP726("d2","d1")
    & ~ ssSkP832("d0")
    & ~ ssSkP831("d1")
    & ~ ssSkP830("d2")
    & ~ ssSkP832("d1")
    & ~ ssSkP831("d0")
    & ~ ssSkP832("d2")
    & ~ ssSkP830("d0")
    & ~ ssSkP831("d2")
    & ~ ssSkP830("d1")
    & ssSkP836("d0")
    & ~ ssSkP834("d2")
    & ssSkP835("d1")
    & ssSkP836("d1")
    & ssSkP835("d0")
    & ~ ssSkP833("d2")
    & ~ ssSkP836("d2")
    & ssSkP834("d0")
    & ~ ssSkP833("d1")
    & ssSkP834("d1")
    & ~ ssSkP835("d2")
    & ~ ssSkP833("d0")
    & ssSkP839("d1")
    & ~ ssSkP838("d2")
    & ssSkP839("d0")
    & ~ ssSkP837("d2")
    & ssSkP838("d0")
    & ssSkP837("d1")
    & ~ ssSkP839("d2")
    & ssSkP838("d1")
    & ssSkP837("d0")
    & ssSkP843("d0")
    & ssSkP842("d1")
    & ~ ssSkP841("d2")
    & ssSkP843("d1")
    & ssSkP842("d0")
    & ~ ssSkP840("d2")
    & ~ ssSkP843("d2")
    & ssSkP841("d0")
    & ssSkP840("d1")
    & ~ ssSkP842("d2")
    & ssSkP841("d1")
    & ssSkP840("d0")
    & ~ ssSkP889("d2")
    & ~ ssSkP888("d2")
    & ssSkP889("d0")
    & ssSkP888("d1")
    & ssSkP889("d1")
    & ssSkP888("d0")
    & ssSkP749("d1","d2")
    & ~ ssSkP749("d2","d1")
    & ssSkP749("d0","d2")
    & ~ ssSkP749("d2","d0")
    & ssSkP749("d0","d1")
    & ssSkP749("d1","d0")
    & ~ ssSkP749("d2","d2")
    & ssSkP749("d1","d1")
    & ssSkP749("d0","d0")
    & ~ ssSkP748("d2","d2")
    & ssSkP748("d1","d1")
    & ssSkP748("d0","d0")
    & ssSkP748("d1","d0")
    & ssSkP748("d0","d1")
    & ~ ssSkP748("d2","d0")
    & ~ ssSkP748("d0","d2")
    & ~ ssSkP748("d2","d1")
    & ~ ssSkP748("d1","d2")
    & ssSkP890("d0")
    & ssSkP890("d1")
    & ~ ssSkP890("d2")
    & ssSkP892("d2")
    & ~ ssSkP891("d2")
    & ssSkP891("d1")
    & ~ ssSkP892("d0")
    & ssSkP891("d0")
    & ~ ssSkP892("d1")
    & ~ 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")
    & ~ ssSkP764("d2","d0")
    & ~ ssSkP764("d0","d2")
    & ssSkP765("d0","d1")
    & ssSkP765("d1","d0")
    & ~ ssSkP764("d2","d1")
    & ~ ssSkP764("d1","d2")
    & ~ ssSkP765("d2","d2")
    & ssSkP765("d1","d1")
    & ssSkP765("d0","d0")
    & ~ ssSkP764("d2","d2")
    & ssSkP764("d1","d1")
    & ssSkP764("d0","d0")
    & ssSkP765("d1","d2")
    & ~ ssSkP765("d2","d1")
    & ssSkP764("d1","d0")
    & ssSkP764("d0","d1")
    & ssSkP765("d0","d2")
    & ~ ssSkP765("d2","d0")
    & ssSkP868("d1")
    & ~ ssSkP869("d0")
    & ~ ssSkP867("d2")
    & ssSkP868("d0")
    & ~ ssSkP869("d1")
    & ~ ssSkP866("d2")
    & ssSkP869("d2")
    & ssSkP867("d0")
    & ssSkP866("d1")
    & ~ ssSkP868("d2")
    & ssSkP867("d1")
    & ssSkP866("d0")
    & ssSkP872("d0")
    & ssSkP872("d1")
    & ~ ssSkP872("d2")
    & ssSkP876("d0")
    & ~ ssSkP874("d2")
    & ssSkP875("d1")
    & ssSkP876("d1")
    & ssSkP875("d0")
    & ~ ssSkP873("d2")
    & ~ ssSkP876("d2")
    & ssSkP874("d0")
    & ~ ssSkP873("d1")
    & ssSkP874("d1")
    & ~ ssSkP875("d2")
    & ssSkP873("d0")
    & ssSkP879("d1")
    & ~ ssSkP878("d2")
    & ssSkP879("d0")
    & ~ ssSkP877("d2")
    & ssSkP878("d0")
    & ssSkP877("d1")
    & ~ ssSkP879("d2")
    & ssSkP878("d1")
    & ssSkP877("d0")
    & ssSkP787("d1","d0")
    & ssSkP787("d0","d1")
    & ~ ssSkP788("d2","d2")
    & ssSkP788("d1","d1")
    & ssSkP788("d0","d0")
    & ~ ssSkP787("d2","d2")
    & ssSkP787("d1","d1")
    & ssSkP787("d0","d0")
    & ssSkP788("d0","d1")
    & ssSkP788("d1","d0")
    & ~ ssSkP787("d2","d1")
    & ~ ssSkP787("d1","d2")
    & ~ ssSkP788("d0","d2")
    & ~ ssSkP788("d2","d0")
    & ~ ssSkP787("d2","d0")
    & ~ ssSkP787("d0","d2")
    & ~ ssSkP788("d1","d2")
    & ~ ssSkP788("d2","d1")
    & ssSkP883("d0")
    & ~ ssSkP881("d2")
    & ssSkP882("d1")
    & ssSkP883("d1")
    & ssSkP882("d0")
    & ~ ssSkP880("d2")
    & ~ ssSkP883("d2")
    & ssSkP881("d0")
    & ssSkP880("d1")
    & ssSkP881("d1")
    & ~ ssSkP882("d2")
    & ssSkP880("d0")
    & ssSkP887("d0")
    & ~ ssSkP885("d2")
    & ssSkP886("d1")
    & ssSkP887("d1")
    & ssSkP886("d0")
    & ~ ssSkP884("d2")
    & ~ ssSkP887("d2")
    & ssSkP885("d0")
    & ~ ssSkP884("d1")
    & ssSkP885("d1")
    & ~ ssSkP886("d2")
    & ssSkP884("d0")
    & ssSkP682("d1","d2")
    & ~ ssSkP682("d2","d1")
    & ssSkP682("d0","d2")
    & ~ ssSkP682("d2","d0")
    & ssSkP682("d0","d1")
    & ssSkP682("d1","d0")
    & ~ ssSkP682("d2","d2")
    & ssSkP682("d1","d1")
    & ssSkP682("d0","d0")
    & ~ ssSkP681("d2","d2")
    & ssSkP681("d1","d1")
    & ssSkP681("d0","d0")
    & ssSkP681("d1","d0")
    & ssSkP681("d0","d1")
    & ~ ssSkP681("d2","d0")
    & ~ ssSkP681("d0","d2")
    & ~ ssSkP681("d2","d1")
    & ~ ssSkP681("d1","d2")
    & ~ ssSkP789("d2")
    & ~ ssSkP789("d1")
    & ~ ssSkP789("d0")
    & ~ ssSkP790("d1")
    & ~ ssSkP791("d0")
    & ~ ssSkP790("d0")
    & ~ ssSkP791("d1")
    & ~ ssSkP791("d2")
    & ~ ssSkP790("d2")
    & ~ ssSkP795("d0")
    & ~ ssSkP793("d2")
    & ~ ssSkP794("d1")
    & ~ ssSkP795("d1")
    & ~ ssSkP794("d0")
    & ~ ssSkP792("d2")
    & ~ ssSkP795("d2")
    & ~ ssSkP793("d0")
    & ~ ssSkP792("d1")
    & ~ ssSkP793("d1")
    & ~ ssSkP794("d2")
    & ~ ssSkP792("d0")
    & ssSkP798("d1")
    & ~ ssSkP799("d0")
    & ~ ssSkP797("d2")
    & ~ ssSkP798("d0")
    & ~ ssSkP799("d1")
    & ~ ssSkP796("d2")
    & ~ ssSkP799("d2")
    & ~ ssSkP797("d0")
    & ~ ssSkP796("d1")
    & ~ ssSkP798("d2")
    & ~ ssSkP797("d1")
    & ~ ssSkP796("d0") ) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05  % Problem  : SYN913-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.07  % Command  : run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.17/5.46  % Computer : n014.cluster.edu
% 0.17/5.46  % Model    : x86_64 x86_64
% 0.17/5.46  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/5.46  % Memory   : 8046.5625MB
% 0.17/5.46  % OS       : Linux 6.8.0-71-generic
% 0.17/5.46  % CPULimit : 300
% 0.17/5.47  % WCLimit  : 300
% 0.17/5.47  % DateTime : Fri Sep 25 02:32:53 UTC 2026
% 0.17/5.47  % CPUTime  : 
% 0.17/5.47  Running run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.23/5.67  Running: java -jar /export/starexec/sandbox2/solver/bin/FMB4J.jar /export/starexec/sandbox2/tmp/tmp.0FCHrLDgzN/theBenchmark.cnf 300
% 2.04/6.35  % domain size: 1
% 2.97/6.60  % domain size: 2
% 4.20/7.02  % domain size: 3
% 7.46/7.80  % model found for domain size 3
% 7.87/7.82  % SZS status CounterSatisfiable for theBenchmark
% 7.87/7.82  % SZS output start FiniteModel for theBenchmark
% See solution above
% 10.06/8.36  % FMB4L exiting
%------------------------------------------------------------------------------