%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : SWB036+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n009.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:04:14 PM UTC 2026
% Result : Satisfiable 5.76s 2.31s
% Output : FiniteModel 5.76s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(domain,interpretation-domains,
! [X] :
( X = "d5"
| X = "d4"
| X = "d3"
| X = "d2"
| X = "d1"
| X = "d0" ) ).
fof(mappings,interpretation-mappings,
( iItaly = "d3"
& iAmerica = "d0"
& iGermany = "d2"
& iFrance = "d4"
& iEngland = "d1" ) ).
fof(predicate_mappings,interpretation-mappings,
( ~ dataDomain("d1")
& ~ dataDomain("d0")
& ~ dataDomain("d3")
& ~ iPizzaBase("d5")
& ~ dataDomain("d2")
& ~ iPizzaBase("d4")
& dataDomain("d5")
& ~ iPizzaBase("d3")
& ~ dataDomain("d4")
& ~ iPizzaBase("d2")
& ~ iPizzaBase("d1")
& ~ iPizzaBase("d0")
& ~ iHot("d0")
& ~ iHot("d1")
& ~ iHot("d2")
& ~ iHot("d3")
& ~ iHot("d4")
& ~ iHot("d5")
& ~ iDomainConcept("d5")
& iDomainConcept("d4")
& ~ iisToppingOf("d5","d4")
& ~ iisToppingOf("d4","d5")
& ~ iisToppingOf("d2","d3")
& ~ iisToppingOf("d3","d2")
& ~ iisToppingOf("d0","d1")
& ~ iisToppingOf("d1","d0")
& ~ iisToppingOf("d5","d5")
& ~ iisToppingOf("d4","d4")
& ~ iisToppingOf("d3","d3")
& ~ iisToppingOf("d2","d2")
& ~ iisToppingOf("d1","d1")
& ~ iisToppingOf("d0","d0")
& ~ iisToppingOf("d0","d3")
& ~ iisToppingOf("d1","d2")
& ~ iisToppingOf("d2","d1")
& ~ iisToppingOf("d3","d0")
& ~ iisToppingOf("d1","d3")
& ~ iisToppingOf("d0","d2")
& ~ iisToppingOf("d3","d1")
& ~ iisToppingOf("d2","d0")
& ~ iisToppingOf("d0","d5")
& ~ iisToppingOf("d1","d4")
& ~ iisToppingOf("d4","d1")
& ~ iisToppingOf("d5","d0")
& ~ iisToppingOf("d1","d5")
& ~ iisToppingOf("d0","d4")
& ~ iisToppingOf("d5","d1")
& ~ iisToppingOf("d4","d0")
& ~ iisToppingOf("d2","d5")
& ~ iisToppingOf("d3","d4")
& ~ iisToppingOf("d4","d3")
& ~ iisToppingOf("d5","d2")
& ~ iisToppingOf("d2","d4")
& ~ iisToppingOf("d3","d5")
& ~ iisToppingOf("d5","d3")
& ~ iisToppingOf("d4","d2")
& iDomainConcept("d1")
& iDomainConcept("d0")
& iDomainConcept("d3")
& iDomainConcept("d2")
& ~ iSpicyTopping("d3")
& ~ iSpicyTopping("d2")
& ~ iSpicyTopping("d1")
& ~ iSpicyTopping("d0")
& ~ iSpicyTopping("d5")
& ~ iSpicyTopping("d4")
& ~ iPizza("d2")
& ~ iPizza("d3")
& ~ iPizza("d0")
& ~ iPizza("d1")
& ~ iPizza("d4")
& ~ iPizza("d5")
& ~ ihasTopping("d1","d3")
& ~ ihasTopping("d0","d2")
& ~ ihasTopping("d3","d1")
& ~ ihasTopping("d2","d0")
& ~ ihasTopping("d0","d3")
& ~ ihasTopping("d1","d2")
& ~ ihasTopping("d2","d1")
& ~ ihasTopping("d3","d0")
& ~ ihasTopping("d5","d5")
& ~ ihasTopping("d4","d4")
& ~ ihasTopping("d3","d3")
& ~ ihasTopping("d2","d2")
& ~ ihasTopping("d1","d1")
& ~ ihasTopping("d0","d0")
& ~ ihasTopping("d4","d5")
& ~ ihasTopping("d5","d4")
& ~ ihasTopping("d2","d3")
& ~ ihasTopping("d3","d2")
& ~ ihasTopping("d0","d1")
& ~ ihasTopping("d1","d0")
& ~ iSpiciness("d4")
& ~ iSpiciness("d5")
& ~ iSpiciness("d0")
& ~ iSpiciness("d1")
& ~ iSpiciness("d2")
& ~ iSpiciness("d3")
& ~ ihasTopping("d3","d5")
& ~ ihasTopping("d2","d4")
& ~ ihasTopping("d5","d3")
& ~ ihasTopping("d4","d2")
& ~ ihasTopping("d2","d5")
& ~ ihasTopping("d3","d4")
& ~ ihasTopping("d4","d3")
& ~ ihasTopping("d5","d2")
& ~ ihasTopping("d1","d5")
& ~ ihasTopping("d0","d4")
& ~ ihasTopping("d5","d1")
& ~ ihasTopping("d4","d0")
& ~ ihasTopping("d0","d5")
& ~ ihasTopping("d1","d4")
& ~ ihasTopping("d4","d1")
& ~ ihasTopping("d5","d0")
& ~ iMeatyPizza("d3")
& ~ iMeatyPizza("d2")
& ~ iMeatyPizza("d1")
& ~ iMeatyPizza("d0")
& ~ iMeatyPizza("d5")
& ~ iMeatyPizza("d4")
& ~ ihasIngredient("d1","d5")
& ~ ihasIngredient("d0","d4")
& ~ ihasIngredient("d5","d1")
& ~ ihasIngredient("d4","d0")
& ~ ihasIngredient("d0","d5")
& ~ ihasIngredient("d1","d4")
& ~ ihasIngredient("d4","d1")
& ~ ihasIngredient("d5","d0")
& ~ ihasIngredient("d3","d5")
& ~ ihasIngredient("d2","d4")
& ~ ihasIngredient("d5","d3")
& ~ ihasIngredient("d4","d2")
& ~ ihasIngredient("d2","d5")
& ~ ihasIngredient("d3","d4")
& ~ ihasIngredient("d4","d3")
& ~ ihasIngredient("d5","d2")
& ~ ihasIngredient("d5","d5")
& ~ ihasIngredient("d4","d4")
& ~ ihasIngredient("d3","d3")
& ~ ihasIngredient("d2","d2")
& ~ ihasIngredient("d1","d1")
& ~ ihasIngredient("d0","d0")
& ~ ihasIngredient("d4","d5")
& ~ ihasIngredient("d5","d4")
& ~ ihasIngredient("d2","d3")
& ~ ihasIngredient("d3","d2")
& ~ ihasIngredient("d0","d1")
& ~ ihasIngredient("d1","d0")
& ~ ihasIngredient("d1","d3")
& ~ ihasIngredient("d0","d2")
& ~ ihasIngredient("d3","d1")
& ~ ihasIngredient("d2","d0")
& ~ ihasIngredient("d0","d3")
& ~ ihasIngredient("d1","d2")
& ~ ihasIngredient("d2","d1")
& ~ ihasIngredient("d3","d0")
& ~ iVegetarianPizzaEquivalent1("d4")
& ~ iVegetarianPizzaEquivalent2("d5")
& ~ iVegetarianPizzaEquivalent1("d5")
& ~ iVegetarianPizzaEquivalent2("d4")
& ~ iMedium("d5")
& ~ iMedium("d4")
& ~ iMedium("d3")
& ~ iMedium("d2")
& ~ iMedium("d1")
& ~ iMedium("d0")
& ~ iVegetarianPizzaEquivalent1("d0")
& ~ iVegetarianPizzaEquivalent2("d1")
& ~ iVegetarianPizzaEquivalent1("d1")
& ~ iVegetarianPizzaEquivalent2("d0")
& ~ iVegetarianPizzaEquivalent1("d2")
& ~ iVegetarianPizzaEquivalent2("d3")
& ~ iVegetarianPizzaEquivalent1("d3")
& ~ iVegetarianPizzaEquivalent2("d2")
& ~ iValuePartition("d4")
& ~ iValuePartition("d5")
& abstractDomain("d4")
& ~ iThinAndCrispyPizza("d5")
& ~ abstractDomain("d5")
& ~ iThinAndCrispyPizza("d4")
& abstractDomain("d0")
& ~ iThinAndCrispyPizza("d1")
& abstractDomain("d1")
& ~ iThinAndCrispyPizza("d0")
& abstractDomain("d2")
& ~ iThinAndCrispyPizza("d3")
& abstractDomain("d3")
& ~ iThinAndCrispyPizza("d2")
& ~ iValuePartition("d0")
& ~ iValuePartition("d1")
& ~ iValuePartition("d2")
& ~ iValuePartition("d3")
& iCountry("d4")
& ~ iCountry("d5")
& ~ iVegetarianPizza("d5")
& ~ iVegetarianPizza("d4")
& ~ iVegetarianPizza("d1")
& ~ iVegetarianPizza("d0")
& ~ iVegetarianPizza("d3")
& ~ iVegetarianPizza("d2")
& iCountry("d2")
& iCountry("d3")
& iCountry("d0")
& iCountry("d1")
& ~ iMeatTopping("d1")
& ~ iMeatTopping("d0")
& ~ iMeatTopping("d3")
& ~ iMeatTopping("d2")
& ~ iMeatTopping("d5")
& ~ iMeatTopping("d4")
& ~ iPizzaTopping("d1")
& ~ iPizzaTopping("d0")
& iowlThing("d4")
& ~ iPizzaTopping("d3")
& ~ iowlThing("d5")
& ~ iPizzaTopping("d2")
& ~ iMild("d1")
& ~ iMild("d0")
& ~ iMild("d3")
& ~ iMild("d2")
& ~ iMild("d5")
& ~ iMild("d4")
& iowlThing("d2")
& ~ iPizzaTopping("d5")
& iowlThing("d3")
& ~ iPizzaTopping("d4")
& iowlThing("d0")
& iowlThing("d1")
& ~ iInterestingPizza("d5")
& ~ iInterestingPizza("d4")
& ~ iInterestingPizza("d1")
& ~ iInterestingPizza("d0")
& ~ iInterestingPizza("d3")
& ~ iInterestingPizza("d2")
& ~ iFood("d4")
& ~ iFood("d5")
& ~ iFood("d2")
& ~ iFood("d3")
& ~ iFood("d0")
& ~ iFood("d1")
& ~ iSpicyPizzaEquivalent("d1")
& ~ iSpicyPizzaEquivalent("d0")
& ~ iSpicyPizzaEquivalent("d3")
& ~ iSpicyPizzaEquivalent("d2")
& ~ iisIngredientOf("d0","d5")
& ~ iisIngredientOf("d1","d4")
& ~ iisIngredientOf("d4","d1")
& ~ iisIngredientOf("d5","d0")
& ~ iisIngredientOf("d1","d5")
& ~ iisIngredientOf("d0","d4")
& ~ iisIngredientOf("d5","d1")
& ~ iisIngredientOf("d4","d0")
& ~ iisIngredientOf("d2","d5")
& ~ iisIngredientOf("d3","d4")
& ~ iisIngredientOf("d4","d3")
& ~ iisIngredientOf("d5","d2")
& ~ iisIngredientOf("d3","d5")
& ~ iisIngredientOf("d2","d4")
& ~ iisIngredientOf("d5","d3")
& ~ iisIngredientOf("d4","d2")
& ~ iisIngredientOf("d4","d5")
& ~ iisIngredientOf("d5","d4")
& ~ iisIngredientOf("d2","d3")
& ~ iisIngredientOf("d3","d2")
& ~ iisIngredientOf("d0","d1")
& ~ iisIngredientOf("d1","d0")
& ~ iisIngredientOf("d5","d5")
& ~ iisIngredientOf("d4","d4")
& ~ iisIngredientOf("d3","d3")
& ~ iisIngredientOf("d2","d2")
& ~ iisIngredientOf("d1","d1")
& ~ iisIngredientOf("d0","d0")
& ~ iisIngredientOf("d0","d3")
& ~ iisIngredientOf("d1","d2")
& ~ iisIngredientOf("d2","d1")
& ~ iisIngredientOf("d3","d0")
& ~ iisIngredientOf("d1","d3")
& ~ iisIngredientOf("d0","d2")
& ~ iisIngredientOf("d3","d1")
& ~ iisIngredientOf("d2","d0")
& ~ iSpicyPizzaEquivalent("d5")
& ~ iSpicyPizzaEquivalent("d4")
& ~ ihasSpiciness("d2","d5")
& ~ ihasSpiciness("d3","d4")
& ~ ihasSpiciness("d4","d3")
& ~ ihasSpiciness("d5","d2")
& ~ ihasSpiciness("d3","d5")
& ~ ihasSpiciness("d2","d4")
& ~ ihasSpiciness("d5","d3")
& ~ ihasSpiciness("d4","d2")
& ~ ihasSpiciness("d0","d5")
& ~ ihasSpiciness("d1","d4")
& ~ ihasSpiciness("d4","d1")
& ~ ihasSpiciness("d5","d0")
& ~ ihasSpiciness("d1","d5")
& ~ ihasSpiciness("d0","d4")
& ~ ihasSpiciness("d5","d1")
& ~ ihasSpiciness("d4","d0")
& ~ ihasSpiciness("d0","d3")
& ~ ihasSpiciness("d1","d2")
& ~ ihasSpiciness("d2","d1")
& ~ ihasSpiciness("d3","d0")
& ~ ihasSpiciness("d1","d3")
& ~ ihasSpiciness("d0","d2")
& ~ ihasSpiciness("d3","d1")
& ~ ihasSpiciness("d2","d0")
& ~ ihasSpiciness("d4","d5")
& ~ ihasSpiciness("d5","d4")
& ~ ihasSpiciness("d2","d3")
& ~ ihasSpiciness("d3","d2")
& ~ ihasSpiciness("d0","d1")
& ~ ihasSpiciness("d1","d0")
& ~ ihasSpiciness("d5","d5")
& ~ ihasSpiciness("d4","d4")
& ~ ihasSpiciness("d3","d3")
& ~ ihasSpiciness("d2","d2")
& ~ ihasSpiciness("d1","d1")
& ~ ihasSpiciness("d0","d0")
& ~ iisBaseOf("d4","d5")
& ~ iisBaseOf("d5","d4")
& ~ iisBaseOf("d2","d3")
& ~ iisBaseOf("d3","d2")
& ~ iisBaseOf("d0","d1")
& ~ iisBaseOf("d1","d0")
& ~ iisBaseOf("d5","d5")
& ~ iisBaseOf("d4","d4")
& ~ iisBaseOf("d3","d3")
& ~ iisBaseOf("d2","d2")
& ~ iisBaseOf("d1","d1")
& ~ iisBaseOf("d0","d0")
& ~ iisBaseOf("d0","d3")
& ~ iisBaseOf("d1","d2")
& ~ iisBaseOf("d2","d1")
& ~ iisBaseOf("d3","d0")
& ~ iisBaseOf("d1","d3")
& ~ iisBaseOf("d0","d2")
& ~ iisBaseOf("d3","d1")
& ~ iisBaseOf("d2","d0")
& ~ iisBaseOf("d0","d5")
& ~ iisBaseOf("d1","d4")
& ~ iisBaseOf("d4","d1")
& ~ iisBaseOf("d5","d0")
& ~ iisBaseOf("d1","d5")
& ~ iisBaseOf("d0","d4")
& ~ iisBaseOf("d5","d1")
& ~ iisBaseOf("d4","d0")
& ~ iisBaseOf("d2","d5")
& ~ iisBaseOf("d3","d4")
& ~ iisBaseOf("d4","d3")
& ~ iisBaseOf("d5","d2")
& ~ iisBaseOf("d3","d5")
& ~ iisBaseOf("d2","d4")
& ~ iisBaseOf("d5","d3")
& ~ iisBaseOf("d4","d2")
& ~ iNonVegetarianPizza("d5")
& ~ iNonVegetarianPizza("d4")
& ~ iSpicyPizza("d4")
& ~ iSpicyPizza("d5")
& ~ iSpicyPizza("d2")
& ~ iSpicyPizza("d3")
& ~ iSpicyPizza("d0")
& ~ iSpicyPizza("d1")
& ~ iNonVegetarianPizza("d3")
& ~ iNonVegetarianPizza("d2")
& ~ iNonVegetarianPizza("d1")
& ~ iNonVegetarianPizza("d0")
& ~ iFishTopping("d3")
& ~ iFishTopping("d2")
& ~ iFishTopping("d1")
& ~ iFishTopping("d0")
& ~ iFishTopping("d5")
& ~ iFishTopping("d4")
& ~ ihasBase("d0","d3")
& ~ ihasBase("d1","d2")
& ~ ihasBase("d2","d1")
& ~ ihasBase("d3","d0")
& ~ ihasBase("d1","d3")
& ~ ihasBase("d0","d2")
& ~ ihasBase("d3","d1")
& ~ ihasBase("d2","d0")
& ~ ihasBase("d4","d5")
& ~ ihasBase("d5","d4")
& ~ ihasBase("d2","d3")
& ~ ihasBase("d3","d2")
& ~ ihasBase("d0","d1")
& ~ ihasBase("d1","d0")
& ~ ihasBase("d5","d5")
& ~ ihasBase("d4","d4")
& ~ ihasBase("d3","d3")
& ~ ihasBase("d2","d2")
& ~ ihasBase("d1","d1")
& ~ ihasBase("d0","d0")
& ~ ihasBase("d2","d5")
& ~ ihasBase("d3","d4")
& ~ ihasBase("d4","d3")
& ~ ihasBase("d5","d2")
& ~ ihasBase("d3","d5")
& ~ ihasBase("d2","d4")
& ~ ihasBase("d5","d3")
& ~ ihasBase("d4","d2")
& ~ ihasBase("d0","d5")
& ~ ihasBase("d1","d4")
& ~ ihasBase("d4","d1")
& ~ ihasBase("d5","d0")
& ~ ihasBase("d1","d5")
& ~ ihasBase("d0","d4")
& ~ ihasBase("d5","d1")
& ~ ihasBase("d4","d0") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWB036+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.35 % Computer : n009.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Thu Sep 24 15:38:43 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.12/0.43 Running: java -jar /export/starexec/sandbox/solver/bin/FMB4J.jar /export/starexec/sandbox/tmp/tmp.bqUUxI65K0/theBenchmark.cnf 300
% 0.59/0.75 % domain size: 1
% 0.87/0.84 % domain size: 2
% 0.87/0.87 % domain size: 3
% 1.22/0.91 % domain size: 4
% 1.73/1.06 % domain size: 5
% 3.56/1.50 % domain size: 6
% 5.63/2.29 % model found for domain size 6
% 5.76/2.31 % SZS status Satisfiable for theBenchmark
% 5.76/2.31 % SZS output start FiniteModel for theBenchmark
% See solution above
% 6.17/2.45 % FMB4L exiting
%------------------------------------------------------------------------------