%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : SYN906-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n006.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:38 PM UTC 2026
% Result : Satisfiable 1.56s 0.99s
% Output : FiniteModel 2.16s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(domain,interpretation-domains,
! [X] :
( X = "d1"
| X = "d0" ) ).
fof(mappings,interpretation-mappings,
( skc23 = "d1"
& skc24 = "d1"
& skc25 = "d0"
& skc26 = "d1"
& skc21 = "d1"
& skc22 = "d1"
& skc28 = "d1"
& skc29 = "d1"
& skc35 = "d0"
& skc34 = "d0"
& skc36 = "d0"
& skc30 = "d1"
& skc31 = "d1"
& skc32 = "d1"
& skc33 = "d0"
& skc41 = "d0"
& skc40 = "d0"
& skf35("d0") = "d1"
& skf36("d0") = "d1"
& skf36("d1") = "d0"
& skf35("d1") = "d1"
& skf38("d0") = "d0"
& skf37("d0") = "d1"
& skf37("d1") = "d0"
& skf38("d1") = "d0"
& skf39("d1") = "d0"
& skf39("d0") = "d0"
& skf61("d1") = "d1"
& skf60("d0") = "d1"
& skf61("d0") = "d1"
& skf60("d1") = "d1"
& skf63("d1") = "d1"
& skf62("d0") = "d1"
& skf63("d0") = "d1"
& skf62("d1") = "d1"
& skf65("d1") = "d1"
& skf64("d0") = "d1"
& skf65("d0") = "d1"
& skf64("d1") = "d1"
& skf67("d1") = "d1"
& skf66("d0") = "d1"
& skf67("d0") = "d1"
& skf66("d1") = "d1"
& skf69("d1") = "d1"
& skf68("d0") = "d1"
& skf69("d0") = "d1"
& skf68("d1") = "d1"
& skf40("d0") = "d1"
& skf40("d1") = "d0"
& skf41("d0") = "d1"
& skf41("d1") = "d0"
& skf43("d0") = "d0"
& skf42("d1") = "d0"
& skf43("d1") = "d0"
& skf42("d0") = "d0"
& skf45("d1") = "d1"
& skf45("d0") = "d0"
& skf44("d1") = "d1"
& skf44("d0") = "d0"
& skf47("d1") = "d1"
& skf47("d0") = "d1"
& skf46("d1") = "d1"
& skf46("d0") = "d0"
& skf49("d1") = "d1"
& skf49("d0") = "d0"
& skf48("d1") = "d1"
& skf48("d0") = "d0"
& skf50("d1") = "d1"
& skf50("d0") = "d0"
& skf52("d1") = "d1"
& skf52("d0") = "d1"
& skf51("d1") = "d1"
& skf51("d0") = "d0"
& skf54("d1") = "d1"
& skf53("d0") = "d1"
& skf54("d0") = "d1"
& skf53("d1") = "d1"
& skf56("d1") = "d1"
& skf55("d0") = "d1"
& skf56("d0") = "d1"
& skf55("d1") = "d1"
& skf58("d1") = "d1"
& skf57("d0") = "d1"
& skf58("d0") = "d1"
& skf57("d1") = "d1"
& skf59("d0") = "d1"
& skf59("d1") = "d1" ) ).
fof(predicate_mappings,interpretation-mappings,
( ssPv20("d1")
& ssPv20("d0")
& ssPv15("d1")
& ~ ssPv16("d0")
& ~ ssPv15("d0")
& ssPv16("d1")
& ssPv13("d1")
& ~ ssPv14("d0")
& ~ ssPv13("d0")
& ssPv14("d1")
& ssPv19("d1")
& ssPv19("d0")
& ~ ssPv17("d1")
& ~ ssPv18("d0")
& ~ ssPv17("d0")
& ~ ssPv18("d1")
& ssPv11("d1")
& ssPv11("d0")
& ~ ssPv8("d0")
& ssPv8("d1")
& ssPv7("d1")
& ~ ssPv6("d0")
& ~ ssPv7("d0")
& ssPv6("d1")
& ssPv5("d1")
& ~ ssPv5("d0")
& ~ ssPv2("d0")
& ~ ssPv2("d1")
& ~ ssPv1("d1")
& ~ ssPv1("d0")
& ssSkP300("d1")
& ssSkP300("d0")
& ssSkP304("d1")
& ssSkP303("d0")
& ssSkP304("d0")
& ssSkP303("d1")
& ssSkP302("d1")
& ssSkP301("d0")
& ssSkP302("d0")
& ssSkP301("d1")
& ssSkP413("d1","d1")
& ssSkP413("d0","d0")
& ssSkP413("d1","d0")
& ssSkP413("d0","d1")
& ssSkP422("d1","d1")
& ssSkP422("d0","d0")
& ssSkP422("d0","d1")
& ssSkP422("d1","d0")
& ~ ssSkP208("d0")
& ~ ssSkP209("d1")
& ~ ssSkP208("d1")
& ~ ssSkP209("d0")
& ~ ssSkP207("d1")
& ~ ssSkP206("d0")
& ~ ssSkP207("d0")
& ~ ssSkP206("d1")
& ~ ssSkP212("d1")
& ~ ssSkP211("d0")
& ~ ssSkP212("d0")
& ~ ssSkP211("d1")
& ~ ssSkP210("d1")
& ~ ssSkP210("d0")
& ssSkP215("d0")
& ssSkP216("d1")
& ssSkP215("d1")
& ssSkP216("d0")
& ssSkP213("d0")
& ssSkP214("d1")
& ssSkP213("d1")
& ssSkP214("d0")
& ssSkP217("d0")
& ssSkP218("d1")
& ssSkP217("d1")
& ~ ssSkP218("d0")
& ~ ssSkP223("d1")
& ~ ssSkP222("d0")
& ~ ssSkP223("d0")
& ~ ssSkP222("d1")
& ~ ssSkP221("d1")
& ~ ssSkP221("d0")
& ~ ssSkP227("d1")
& ~ ssSkP226("d0")
& ~ ssSkP227("d0")
& ~ ssSkP226("d1")
& ~ ssSkP225("d1")
& ~ ssSkP224("d0")
& ssSkP225("d0")
& ~ ssSkP224("d1")
& ~ ssSkP201("d1")
& ~ ssSkP201("d0")
& ~ ssSkP205("d1")
& ~ ssSkP204("d0")
& ~ ssSkP205("d0")
& ~ ssSkP204("d1")
& ~ ssSkP203("d1")
& ~ ssSkP202("d0")
& ~ ssSkP203("d0")
& ~ ssSkP202("d1")
& ssSkP252("d1")
& ssSkP251("d0")
& ssSkP252("d0")
& ssSkP251("d1")
& ssSkP250("d1")
& ssSkP250("d0")
& ssSkP256("d1")
& ssSkP255("d0")
& ssSkP256("d0")
& ssSkP255("d1")
& ssSkP254("d1")
& ssSkP253("d0")
& ssSkP254("d0")
& ssSkP253("d1")
& ssSkP259("d0")
& ssSkP259("d1")
& ~ ssSkP258("d1")
& ssSkP257("d0")
& ssSkP258("d0")
& ssSkP257("d1")
& ~ ssSkC4
& ~ ssSkC3
& ~ ssSkC5
& ~ ssSkC8
& ~ ssSkC7
& ~ ssSkC9
& ~ ssSkC0
& ~ ssSkC2
& ~ ssSkC1
& ssSkP263("d1")
& ssSkP262("d0")
& ssSkP263("d0")
& ssSkP262("d1")
& ssSkP261("d1")
& ssSkP260("d0")
& ssSkP261("d0")
& ~ ssSkP260("d1")
& ssSkP266("d0")
& ~ ssSkP267("d1")
& ssSkP266("d1")
& ssSkP267("d0")
& ssSkP265("d1")
& ssSkP264("d0")
& ssSkP265("d0")
& ssSkP264("d1")
& ~ ssSkP229("d1")
& ~ ssSkP228("d0")
& ~ ssSkP229("d0")
& ~ ssSkP228("d1")
& ~ ssSkP230("d1")
& ~ ssSkP230("d0")
& ssSkP233("d0")
& ~ ssSkP234("d1")
& ~ ssSkP233("d1")
& ~ ssSkP234("d0")
& ~ ssSkP232("d1")
& ~ ssSkP231("d0")
& ~ ssSkP232("d0")
& ~ ssSkP231("d1")
& ssSkP238("d1")
& ~ ssSkP237("d0")
& ssSkP238("d0")
& ~ ssSkP237("d1")
& ~ ssSkP236("d1")
& ~ ssSkP235("d0")
& ~ ssSkP236("d0")
& ~ ssSkP235("d1")
& ssSkP239("d0")
& ssSkP239("d1")
& ssSkP387("d1","d1")
& ssSkP387("d0","d0")
& ssSkP241("d1")
& ssSkP388("d0","d1")
& ssSkP388("d1","d0")
& ssSkP240("d0")
& ssSkP387("d1","d0")
& ssSkP387("d0","d1")
& ssSkP241("d0")
& ssSkP388("d1","d1")
& ssSkP388("d0","d0")
& ssSkP240("d1")
& ~ ssSkP245("d1")
& ~ ssSkP245("d0")
& ssSkP242("d0")
& ~ ssSkP242("d1")
& ssSkP249("d1")
& ssSkP248("d0")
& ssSkP249("d0")
& ssSkP248("d1")
& ssSkP246("d0")
& ssSkP247("d1")
& ssSkP246("d1")
& ssSkP247("d0")
& ssSkP291("d0")
& ~ ssSkP291("d1")
& ssSkP290("d1")
& ssSkP290("d0")
& ssSkP295("d0")
& ssSkP296("d1")
& ssSkP295("d1")
& ssSkP296("d0")
& ssSkP294("d1")
& ssSkP294("d0")
& ssSkP299("d0")
& ssSkP299("d1")
& ssSkP298("d1")
& ssSkP297("d0")
& ssSkP298("d0")
& ssSkP297("d1")
& ssSkP270("d1")
& ssSkP270("d0")
& ssSkP274("d1")
& ssSkP273("d0")
& ssSkP274("d0")
& ssSkP273("d1")
& ssSkP272("d1")
& ssSkP271("d0")
& ssSkP272("d0")
& ssSkP271("d1")
& ssSkP278("d1")
& ssSkP277("d0")
& ssSkP278("d0")
& ssSkP277("d1")
& ssSkP276("d1")
& ssSkP275("d0")
& ssSkP276("d0")
& ~ ssSkP275("d1")
& ssSkP279("d0")
& ssSkP279("d1")
& ssSkP280("d0")
& ssSkP281("d1")
& ssSkP280("d1")
& ssSkP281("d0")
& ssSkP284("d0")
& ssSkP285("d1")
& ssSkP284("d1")
& ssSkP285("d0")
& ~ ssSkP283("d1")
& ssSkP282("d0")
& ssSkP283("d0")
& ssSkP282("d1")
& ssSkP289("d1")
& ssSkP288("d0")
& ssSkP289("d0")
& ssSkP288("d1")
& ssSkP287("d1")
& ssSkP286("d0")
& ssSkP287("d0")
& ssSkP286("d1")
& ssSkP79("d1","d0")
& ssSkP79("d0","d1")
& ssSkP79("d1","d1")
& ssSkP79("d0","d0")
& ssSkP80("d0","d1")
& ssSkP80("d1","d0")
& ssSkP80("d1","d1")
& ssSkP80("d0","d0")
& ssSkP62("d0","d1")
& ssSkP62("d1","d0")
& ssSkP62("d1","d1")
& ssSkP62("d0","d0")
& ssSkP61("d1","d1")
& ssSkP61("d0","d0")
& ssSkP61("d1","d0")
& ssSkP61("d0","d1")
& ssSkP0("d1","d0")
& ssSkP0("d0","d1")
& ssSkP1("d1","d1")
& ssSkP1("d0","d0")
& ssSkP0("d1","d1")
& ssSkP0("d0","d0")
& ssSkP1("d0","d1")
& ssSkP1("d1","d0")
& ssSkP41("d1","d1")
& ssSkP41("d0","d0")
& ssSkP41("d1","d0")
& ssSkP41("d0","d1")
& ssSkP42("d0","d1")
& ssSkP42("d1","d0")
& ssSkP42("d1","d1")
& ssSkP42("d0","d0")
& ssSkP20("d1","d0")
& ssSkP20("d0","d1")
& ssSkP21("d1","d1")
& ssSkP21("d0","d0")
& ssSkP20("d1","d1")
& ssSkP20("d0","d0")
& ssSkP21("d0","d1")
& ssSkP21("d1","d0")
& ssSkP101("d0")
& ~ ssSkP102("d1")
& ssSkP101("d1")
& ssSkP102("d0")
& ~ ssSkP100("d1")
& ~ ssSkP100("d0")
& ~ ssSkP106("d1")
& ~ ssSkP105("d0")
& ~ ssSkP106("d0")
& ~ ssSkP105("d1")
& ~ ssSkC19
& ~ ssSkC13
& ~ ssSkC12
& ~ ssSkC15
& ~ ssSkC14
& ~ ssSkC11
& ~ ssSkC10
& ~ ssSkP138("d0")
& ~ ssSkP139("d1")
& ~ ssSkP138("d1")
& ~ ssSkP139("d0")
& ~ ssSkP137("d1")
& ~ ssSkP137("d0")
& ~ ssSkC20
& ssSkP142("d1")
& ~ ssSkP141("d0")
& ssSkP142("d0")
& ~ ssSkP141("d1")
& ~ ssSkP140("d1")
& ~ ssSkP140("d0")
& ssSkP145("d0")
& ssSkP146("d1")
& ssSkP145("d1")
& ~ ssSkP146("d0")
& ssSkP144("d1")
& ssSkP143("d0")
& ssSkP144("d0")
& ssSkP143("d1")
& ~ ssSkP149("d0")
& ~ ssSkP149("d1")
& ~ ssSkP109("d0")
& ~ ssSkP109("d1")
& ~ ssSkP108("d1")
& ~ ssSkP107("d0")
& ~ ssSkP108("d0")
& ~ ssSkP107("d1")
& ssSkP113("d1")
& ssSkP112("d0")
& ssSkP112("d1")
& ssSkP113("d0")
& ssSkP110("d0")
& ssSkP111("d1")
& ssSkP110("d1")
& ssSkP111("d0")
& ~ ssSkP114("d0")
& ssSkP114("d1")
& ~ ssSkP171("d1")
& ~ ssSkP170("d0")
& ~ ssSkP171("d0")
& ~ ssSkP170("d1")
& ssSkP175("d1")
& ~ ssSkP174("d0")
& ~ ssSkP175("d0")
& ~ ssSkP174("d1")
& ~ ssSkP173("d1")
& ~ ssSkP172("d0")
& ~ ssSkP173("d0")
& ~ ssSkP172("d1")
& ~ ssSkP179("d1")
& ~ ssSkP178("d0")
& ~ ssSkP179("d0")
& ~ ssSkP178("d1")
& ~ ssSkP177("d1")
& ~ ssSkP176("d0")
& ~ ssSkP177("d0")
& ~ ssSkP176("d1")
& ssSkP182("d1")
& ssSkP181("d0")
& ssSkP182("d0")
& ssSkP181("d1")
& ~ ssSkP180("d1")
& ~ ssSkP180("d0")
& ssSkP186("d1")
& ssSkP186("d0")
& ~ ssSkP183("d0")
& ssSkP183("d1")
& ssSkP189("d0")
& ~ ssSkP189("d1")
& ssSkP188("d1")
& ~ ssSkP187("d0")
& ssSkP188("d0")
& ssSkP187("d1")
& ~ ssSkP152("d0")
& ~ ssSkP153("d1")
& ~ ssSkP152("d1")
& ~ ssSkP153("d0")
& ~ ssSkP151("d1")
& ~ ssSkP150("d0")
& ~ ssSkP151("d0")
& ~ ssSkP150("d1")
& ssSkP157("d1")
& ~ ssSkP156("d0")
& ssSkP157("d0")
& ~ ssSkP156("d1")
& ~ ssSkP154("d0")
& ~ ssSkP155("d1")
& ~ ssSkP154("d1")
& ~ ssSkP155("d0")
& ssSkP158("d0")
& ssSkP159("d1")
& ssSkP158("d1")
& ~ ssSkP159("d0")
& ~ ssSkP164("d1")
& ~ ssSkP163("d0")
& ~ ssSkP164("d0")
& ~ ssSkP163("d1")
& ~ ssSkP162("d1")
& ~ ssSkP162("d0")
& ~ ssSkP167("d0")
& ~ ssSkP168("d1")
& ~ ssSkP167("d1")
& ~ ssSkP168("d0")
& ~ ssSkP166("d1")
& ~ ssSkP165("d0")
& ~ ssSkP166("d0")
& ~ ssSkP165("d1")
& ~ ssSkP169("d0")
& ~ ssSkP169("d1")
& ssSkP193("d1")
& ssSkP192("d0")
& ssSkP193("d0")
& ssSkP192("d1")
& ssSkP190("d0")
& ssSkP191("d1")
& ssSkP190("d1")
& ssSkP191("d0")
& ssSkP197("d1")
& ssSkP196("d0")
& ssSkP197("d0")
& ssSkP196("d1")
& ssSkP195("d1")
& ssSkP194("d0")
& ssSkP195("d0")
& ssSkP194("d1")
& ~ ssSkP198("d0")
& ssSkP198("d1")
& ~ ssSkP50("d0")
& ~ ssSkP50("d1")
& ~ ssSkP52("d0")
& ~ ssSkP51("d1")
& ~ ssSkP52("d1")
& ~ ssSkP51("d0")
& ~ ssSkP53("d1")
& ~ ssSkP54("d0")
& ~ ssSkP53("d0")
& ~ ssSkP54("d1")
& ~ ssSkP55("d1")
& ~ ssSkP56("d0")
& ~ ssSkP55("d0")
& ~ ssSkP56("d1")
& ~ ssSkP58("d0")
& ~ ssSkP57("d1")
& ~ ssSkP58("d1")
& ~ ssSkP57("d0")
& ssSkP59("d1")
& ssSkP59("d0")
& ssSkP60("d1")
& ~ ssSkP60("d0")
& ~ ssSkP63("d0")
& ~ ssSkP63("d1")
& ~ ssSkP65("d0")
& ~ ssSkP64("d1")
& ~ ssSkP65("d1")
& ~ ssSkP64("d0")
& ~ ssSkP66("d1")
& ~ ssSkP67("d0")
& ~ ssSkP66("d0")
& ~ ssSkP67("d1")
& ~ ssSkP69("d0")
& ~ ssSkP68("d1")
& ~ ssSkP69("d1")
& ~ ssSkP68("d0")
& ~ ssSkP70("d0")
& ~ ssSkP70("d1")
& ~ ssSkP71("d1")
& ~ ssSkP72("d0")
& ~ ssSkP71("d0")
& ~ ssSkP72("d1")
& ~ ssSkP74("d0")
& ~ ssSkP73("d1")
& ~ ssSkP74("d1")
& ~ ssSkP73("d0")
& ~ ssSkP76("d0")
& ~ ssSkP75("d1")
& ~ ssSkP76("d1")
& ~ ssSkP75("d0")
& ssSkP77("d1")
& ~ ssSkP78("d0")
& ssSkP77("d0")
& ssSkP78("d1")
& ~ ssSkP81("d0")
& ~ ssSkP81("d1")
& ~ ssSkP83("d0")
& ~ ssSkP82("d1")
& ~ ssSkP83("d1")
& ~ ssSkP82("d0")
& ssSkP85("d0")
& ~ ssSkP84("d1")
& ~ ssSkP85("d1")
& ~ ssSkP84("d0")
& ~ ssSkP87("d0")
& ~ ssSkP86("d1")
& ~ ssSkP87("d1")
& ~ ssSkP86("d0")
& ~ ssSkP89("d0")
& ~ ssSkP88("d1")
& ~ ssSkP89("d1")
& ~ ssSkP88("d0")
& ~ ssSkP92("d0")
& ~ ssSkP91("d1")
& ~ ssSkP92("d1")
& ~ ssSkP91("d0")
& ~ ssSkP93("d1")
& ~ ssSkP94("d0")
& ssSkP93("d0")
& ~ ssSkP94("d1")
& ~ ssSkP96("d0")
& ~ ssSkP95("d1")
& ~ ssSkP96("d1")
& ~ ssSkP95("d0")
& ~ ssSkP98("d0")
& ~ ssSkP97("d1")
& ~ ssSkP98("d1")
& ~ ssSkP97("d0")
& ~ ssSkP99("d1")
& ~ ssSkP99("d0")
& ~ ssSkP90("d0")
& ~ ssSkP90("d1")
& ~ ssSkP9("d0")
& ~ ssSkP8("d1")
& ~ ssSkP9("d1")
& ~ ssSkP8("d0")
& ~ ssSkP5("d0")
& ~ ssSkP4("d1")
& ~ ssSkP5("d1")
& ~ ssSkP4("d0")
& ~ ssSkP7("d0")
& ~ ssSkP6("d1")
& ~ ssSkP7("d1")
& ~ ssSkP6("d0")
& ~ ssSkP3("d0")
& ~ ssSkP2("d1")
& ~ ssSkP3("d1")
& ~ ssSkP2("d0")
& ~ ssSkP10("d0")
& ~ ssSkP10("d1")
& ~ ssSkP12("d0")
& ~ ssSkP11("d1")
& ~ ssSkP12("d1")
& ~ ssSkP11("d0")
& ~ ssSkP14("d0")
& ~ ssSkP13("d1")
& ~ ssSkP14("d1")
& ~ ssSkP13("d0")
& ~ ssSkP16("d0")
& ~ ssSkP15("d1")
& ~ ssSkP16("d1")
& ~ ssSkP15("d0")
& ~ ssSkP17("d1")
& ssSkP18("d0")
& ssSkP18("d1")
& ~ ssSkP17("d0")
& ~ ssSkP23("d0")
& ~ ssSkP22("d1")
& ~ ssSkP23("d1")
& ~ ssSkP22("d0")
& ~ ssSkP25("d0")
& ~ ssSkP24("d1")
& ~ ssSkP25("d1")
& ~ ssSkP24("d0")
& ~ ssSkP27("d0")
& ~ ssSkP26("d1")
& ~ ssSkP27("d1")
& ~ ssSkP26("d0")
& ~ ssSkP29("d0")
& ~ ssSkP28("d1")
& ~ ssSkP29("d1")
& ~ ssSkP28("d0")
& ssSkP19("d1")
& ~ ssSkP19("d0")
& ~ ssSkP30("d0")
& ~ ssSkP30("d1")
& ~ ssSkP32("d0")
& ~ ssSkP31("d1")
& ~ ssSkP32("d1")
& ~ ssSkP31("d0")
& ~ ssSkP34("d0")
& ~ ssSkP33("d1")
& ~ ssSkP34("d1")
& ~ ssSkP33("d0")
& ~ ssSkP36("d0")
& ~ ssSkP35("d1")
& ~ ssSkP36("d1")
& ~ ssSkP35("d0")
& ~ ssSkP38("d0")
& ~ ssSkP37("d1")
& ~ ssSkP38("d1")
& ~ ssSkP37("d0")
& ssSkP39("d1")
& ssSkP39("d0")
& ssSkP40("d1")
& ~ ssSkP40("d0")
& ~ ssSkP43("d0")
& ~ ssSkP43("d1")
& ~ ssSkP45("d0")
& ~ ssSkP44("d1")
& ~ ssSkP45("d1")
& ~ ssSkP44("d0")
& ~ ssSkP47("d0")
& ~ ssSkP46("d1")
& ~ ssSkP47("d1")
& ~ ssSkP46("d0")
& ~ ssSkP49("d0")
& ~ ssSkP48("d1")
& ~ ssSkP49("d1")
& ~ ssSkP48("d0")
& ssSkP448("d0")
& ssSkP449("d1")
& ssSkP448("d1")
& ssSkP449("d0")
& ssSkP450("d1")
& ssSkP450("d0")
& ssSkP454("d1")
& ssSkP453("d0")
& ssSkP454("d0")
& ssSkP453("d1")
& ssSkP452("d1")
& ssSkP451("d0")
& ssSkP452("d0")
& ssSkP451("d1")
& ssSkP458("d1")
& ssSkP457("d0")
& ssSkP458("d0")
& ssSkP457("d1")
& ssSkP456("d1")
& ssSkP455("d0")
& ssSkP456("d0")
& ssSkP455("d1")
& ssSkP459("d0")
& ssSkP459("d1")
& ssSkP460("d0")
& ssSkP461("d1")
& ssSkP460("d1")
& ssSkP461("d0")
& ssSkP464("d0")
& ssSkP465("d1")
& ssSkP464("d1")
& ssSkP465("d0")
& ssSkP462("d0")
& ssSkP463("d1")
& ssSkP462("d1")
& ssSkP463("d0")
& ssSkP468("d0")
& ssSkP469("d1")
& ssSkP468("d1")
& ssSkP469("d0")
& ssSkP466("d0")
& ssSkP467("d1")
& ssSkP466("d1")
& ssSkP467("d0")
& ssSkP429("d1")
& ~ ssSkP428("d0")
& ~ ssSkP429("d0")
& ssSkP428("d1")
& ssSkP427("d1")
& ~ ssSkP426("d0")
& ~ ssSkP427("d0")
& ssSkP426("d1")
& ~ ssSkP431("d0")
& ssSkP432("d1")
& ssSkP431("d1")
& ssSkP432("d0")
& ssSkP430("d1")
& ~ ssSkP430("d0")
& ssSkP436("d1")
& ~ ssSkP435("d0")
& ~ ssSkP436("d0")
& ssSkP435("d1")
& ssSkP434("d1")
& ~ ssSkP433("d0")
& ~ ssSkP434("d0")
& ssSkP433("d1")
& ~ ssSkP439("d0")
& ssSkP439("d1")
& ssSkP438("d1")
& ~ ssSkP437("d0")
& ~ ssSkP438("d0")
& ssSkP437("d1")
& ssSkP103("d1","d1")
& ssSkP103("d0","d0")
& ssSkP104("d0","d1")
& ssSkP104("d1","d0")
& ssSkP103("d1","d0")
& ssSkP103("d0","d1")
& ssSkP104("d1","d1")
& ssSkP104("d0","d0")
& ssSkP442("d0")
& ssSkP443("d1")
& ssSkP442("d1")
& ssSkP443("d0")
& ssSkP441("d1")
& ssSkP440("d0")
& ssSkP441("d0")
& ssSkP440("d1")
& ssSkP446("d0")
& ssSkP447("d1")
& ssSkP446("d1")
& ssSkP447("d0")
& ssSkP444("d0")
& ssSkP445("d1")
& ssSkP444("d1")
& ssSkP445("d0")
& ssSkP136("d1","d1")
& ssSkP136("d0","d0")
& ssSkP136("d0","d1")
& ssSkP136("d1","d0")
& ssSkP135("d1","d0")
& ssSkP135("d0","d1")
& ssSkP472("d1")
& ssSkP471("d0")
& ssSkP135("d1","d1")
& ssSkP135("d0","d0")
& ssSkP472("d0")
& ssSkP471("d1")
& ssSkP470("d1")
& ssSkP470("d0")
& ssSkP476("d1")
& ssSkP475("d0")
& ssSkP476("d0")
& ssSkP475("d1")
& ssSkP474("d1")
& ssSkP473("d0")
& ssSkP474("d0")
& ssSkP473("d1")
& ssSkP479("d0")
& ssSkP479("d1")
& ssSkP478("d1")
& ssSkP477("d0")
& ssSkP478("d0")
& ssSkP477("d1")
& ssSkP147("d1","d1")
& ssSkP147("d0","d0")
& ssSkP148("d0","d1")
& ssSkP148("d1","d0")
& ssSkP147("d1","d0")
& ssSkP147("d0","d1")
& ssSkP148("d1","d1")
& ssSkP148("d0","d0")
& ~ ssSkP483("d1")
& ssSkP482("d0")
& ssSkP483("d0")
& ssSkP482("d1")
& ssSkP481("d1")
& ssSkP480("d0")
& ssSkP481("d0")
& ssSkP480("d1")
& ssSkP484("d0")
& ~ ssSkP484("d1")
& ssSkP161("d1","d1")
& ssSkP161("d0","d0")
& ssSkP161("d0","d1")
& ssSkP161("d1","d0")
& ssSkP160("d1","d0")
& ssSkP160("d0","d1")
& ssSkP160("d1","d1")
& ssSkP160("d0","d0")
& ssSkP185("d1","d1")
& ssSkP185("d0","d0")
& ssSkP185("d0","d1")
& ssSkP185("d1","d0")
& ssSkP184("d1","d0")
& ssSkP184("d0","d1")
& ssSkP184("d1","d1")
& ssSkP184("d0","d0")
& ssSkP199("d1","d0")
& ssSkP199("d0","d1")
& ssSkP199("d1","d1")
& ssSkP199("d0","d0")
& ssRr("d1","d1")
& ~ ssRr("d0","d0")
& ssRr("d0","d1")
& ssRr("d1","d0")
& ssSkP407("d1")
& ssSkP406("d0")
& ssSkP407("d0")
& ssSkP406("d1")
& ssSkP405("d1")
& ssSkP404("d0")
& ssSkP405("d0")
& ssSkP404("d1")
& ssSkP409("d1")
& ssSkP408("d0")
& ssSkP409("d0")
& ssSkP408("d1")
& ssSkP410("d1")
& ssSkP410("d0")
& ssSkP414("d1")
& ~ ssSkP414("d0")
& ssSkP411("d0")
& ssSkP412("d1")
& ~ ssSkP411("d1")
& ssSkP412("d0")
& ssSkP418("d1")
& ~ ssSkP417("d0")
& ~ ssSkP418("d0")
& ssSkP417("d1")
& ~ ssSkP415("d0")
& ssSkP416("d1")
& ssSkP415("d1")
& ~ ssSkP416("d0")
& ~ ssSkP419("d0")
& ssSkP419("d1")
& ssSkP421("d1")
& ~ ssSkP420("d0")
& ~ ssSkP421("d0")
& ssSkP420("d1")
& ~ ssSkP424("d0")
& ssSkP425("d1")
& ssSkP424("d1")
& ~ ssSkP425("d0")
& ssSkP423("d1")
& ~ ssSkP423("d0")
& ssSkP403("d1")
& ssSkP402("d0")
& ssSkP403("d0")
& ssSkP402("d1")
& ssSkP401("d1")
& ssSkP400("d0")
& ssSkP401("d0")
& ssSkP400("d1")
& ssSkP200("d1","d1")
& ssSkP200("d0","d0")
& ssSkP200("d0","d1")
& ssSkP200("d1","d0")
& ssSkP307("d0")
& ssSkP308("d1")
& ssSkP307("d1")
& ~ ssSkP308("d0")
& ssSkP306("d1")
& ssSkP305("d0")
& ~ ssSkP306("d0")
& ssSkP305("d1")
& ssSkP309("d0")
& ssSkP309("d1")
& ssSkP311("d1")
& ssSkP310("d0")
& ssSkP311("d0")
& ssSkP310("d1")
& ssSkP315("d1")
& ssSkP314("d0")
& ssSkP315("d0")
& ssSkP314("d1")
& ssSkP313("d1")
& ssSkP312("d0")
& ssSkP313("d0")
& ssSkP312("d1")
& ssSkP316("d0")
& ~ ssSkP316("d1")
& ssSkP219("d1","d1")
& ssSkP219("d0","d0")
& ssSkP219("d1","d0")
& ssSkP219("d0","d1")
& ssSkP220("d1","d1")
& ssSkP220("d0","d0")
& ssSkP220("d0","d1")
& ssSkP220("d1","d0")
& ssSkP244("d1","d1")
& ssSkP244("d0","d0")
& ssSkP244("d0","d1")
& ssSkP244("d1","d0")
& ssSkP243("d1","d0")
& ssSkP243("d0","d1")
& ssSkP243("d1","d1")
& ssSkP243("d0","d0")
& ssSkP389("d0")
& ssSkP389("d1")
& ssSkP268("d1","d1")
& ssSkP268("d0","d0")
& ssSkP269("d0","d1")
& ssSkP269("d1","d0")
& ssSkP268("d1","d0")
& ssSkP268("d0","d1")
& ssSkP269("d1","d1")
& ssSkP269("d0","d0")
& ssSkP390("d0")
& ssSkP391("d1")
& ssSkP390("d1")
& ssSkP391("d0")
& ssSkP394("d0")
& ssSkP395("d1")
& ssSkP394("d1")
& ~ ssSkP395("d0")
& ~ ssSkP393("d1")
& ssSkP392("d0")
& ssSkP393("d0")
& ssSkP392("d1")
& ssSkP399("d1")
& ssSkP398("d0")
& ssSkP399("d0")
& ssSkP398("d1")
& ssSkP293("d1","d1")
& ssSkP293("d0","d0")
& ssSkP396("d0")
& ssSkP397("d1")
& ssSkP293("d0","d1")
& ssSkP293("d1","d0")
& ssSkP396("d1")
& ssSkP397("d0")
& ssSkP292("d1","d0")
& ssSkP292("d0","d1")
& ssSkP292("d1","d1")
& ssSkP292("d0","d0") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN906-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.07/0.36 % Computer : n006.cluster.edu
% 0.07/0.36 % Model : x86_64 x86_64
% 0.07/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.36 % Memory : 8046.5625MB
% 0.07/0.36 % OS : Linux 6.8.0-71-generic
% 0.07/0.36 % CPULimit : 300
% 0.07/0.36 % WCLimit : 300
% 0.07/0.36 % DateTime : Fri Sep 25 02:32:11 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.07/0.36 Running run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.07/0.44 Running: java -jar /export/starexec/sandbox/solver/bin/FMB4J.jar /export/starexec/sandbox/tmp/tmp.hcvTZDzMJN/theBenchmark.cnf 300
% 0.66/0.78 % domain size: 1
% 1.56/0.90 % domain size: 2
% 1.56/0.98 % model found for domain size 2
% 1.56/0.99 % SZS status CounterSatisfiable for theBenchmark
% 1.56/0.99 % SZS output start FiniteModel for theBenchmark
% See solution above
% 2.16/1.13 % FMB4L exiting
%------------------------------------------------------------------------------