%------------------------------------------------------------------------------ % File : Darwin---1.4.5 % Problem : SWB036+1 : TPTP v8.1.0. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : darwin -pl 0 -pmc true -to %d %s % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 0s % DateTime : Tue Jul 19 18:54:58 EDT 2022 % Result : Satisfiable 0.20s 0.48s % Output : Model 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SWB036+1 : TPTP v8.1.0. Released v5.2.0. % 0.10/0.13 % Command : darwin -pl 0 -pmc true -to %d %s % 0.12/0.34 % Computer : n017.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % DateTime : Wed Jun 1 11:42:27 EDT 2022 % 0.12/0.34 % CPUTime : % 0.12/0.35 Defaulting to tptp format. % 0.20/0.48 SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.20/0.48 % 0.20/0.48 MODEL (CONTEXT): % 0.20/0.48 SZS output start Model for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.20/0.48 -__-v__(=0) % 0.20/0.48 +(_0 = _0) % 0.20/0.48 -(iAmerica = iFrance) % 0.20/0.48 -(iAmerica = iItaly) % 0.20/0.48 -(iAmerica = iGermany) % 0.20/0.48 -(iAmerica = iEngland) % 0.20/0.48 -(iAmerica = esk2_0) % 0.20/0.48 -(iFrance = iAmerica) % 0.20/0.48 -(iFrance = iItaly) % 0.20/0.48 -(iFrance = iGermany) % 0.20/0.48 -(iFrance = iEngland) % 0.20/0.48 -(iFrance = esk2_0) % 0.20/0.48 -(iItaly = iAmerica) % 0.20/0.48 -(iItaly = iFrance) % 0.20/0.48 -(iItaly = iGermany) % 0.20/0.48 -(iItaly = iEngland) % 0.20/0.48 -(iItaly = esk2_0) % 0.20/0.48 -(iGermany = iAmerica) % 0.20/0.48 -(iGermany = iFrance) % 0.20/0.48 -(iGermany = iItaly) % 0.20/0.48 -(iGermany = iEngland) % 0.20/0.48 -(iGermany = esk2_0) % 0.20/0.48 -(iEngland = iAmerica) % 0.20/0.48 -(iEngland = iFrance) % 0.20/0.48 -(iEngland = iItaly) % 0.20/0.48 -(iEngland = iGermany) % 0.20/0.48 -(iEngland = esk2_0) % 0.20/0.48 -(esk1_0 = esk2_0) % 0.20/0.48 -(esk2_0 = iAmerica) % 0.20/0.48 -(esk2_0 = iFrance) % 0.20/0.48 -(esk2_0 = iItaly) % 0.20/0.48 -(esk2_0 = iGermany) % 0.20/0.48 -(esk2_0 = iEngland) % 0.20/0.48 -(esk2_0 = esk1_0) % 0.20/0.48 +abstractDomain(=0) % 0.20/0.48 +abstractDomain(iAmerica) % 0.20/0.48 +abstractDomain(iFrance) % 0.20/0.48 +abstractDomain(iItaly) % 0.20/0.48 +abstractDomain(iGermany) % 0.20/0.48 +abstractDomain(iEngland) % 0.20/0.48 +abstractDomain(esk1_0) % 0.20/0.48 -abstractDomain(esk2_0) % 0.20/0.48 +dataDomain(esk2_0) % 0.20/0.48 -dataDomain(iAmerica) % 0.20/0.48 -dataDomain(iFrance) % 0.20/0.48 -dataDomain(iItaly) % 0.20/0.48 -dataDomain(iGermany) % 0.20/0.48 -dataDomain(iEngland) % 0.20/0.48 -dataDomain(esk1_0) % 0.20/0.49 -iAmerican(_0) % 0.20/0.49 -iAmericanHot(_0) % 0.20/0.49 -iAnchoviesTopping(esk2_0) % 0.20/0.49 -iArtichokeTopping(esk2_0) % 0.20/0.49 -iAsparagusTopping(esk2_0) % 0.20/0.49 -iCajun(_0) % 0.20/0.49 -iCajunSpiceTopping(esk2_0) % 0.20/0.49 -iCaperTopping(esk2_0) % 0.20/0.49 -iCapricciosa(_0) % 0.20/0.49 -iCaprina(_0) % 0.20/0.49 -iCheeseTopping(esk2_0) % 0.20/0.49 -iCheeseyPizza(esk2_0) % 0.20/0.49 -iCheeseyVegetableTopping(_0) % 0.20/0.49 -iChickenTopping(esk2_0) % 0.20/0.49 +iCountry(iAmerica) % 0.20/0.49 +iCountry(iFrance) % 0.20/0.49 +iCountry(iItaly) % 0.20/0.49 +iCountry(iGermany) % 0.20/0.49 +iCountry(iEngland) % 0.20/0.49 -iCountry(esk2_0) % 0.20/0.49 -iDeepPanBase(_0) % 0.20/0.49 +iDomainConcept(iAmerica) % 0.20/0.49 +iDomainConcept(iFrance) % 0.20/0.49 +iDomainConcept(iItaly) % 0.20/0.49 +iDomainConcept(iGermany) % 0.20/0.49 +iDomainConcept(iEngland) % 0.20/0.49 -iDomainConcept(esk2_0) % 0.20/0.49 -iFiorentina(_0) % 0.20/0.49 -iFishTopping(esk2_0) % 0.20/0.49 -iFood(esk2_0) % 0.20/0.49 -iFourCheesesTopping(esk2_0) % 0.20/0.49 -iFourSeasons(_0) % 0.20/0.49 -iFruitTopping(esk2_0) % 0.20/0.49 -iFruttiDiMare(_0) % 0.20/0.49 -iGarlicTopping(esk2_0) % 0.20/0.49 -iGiardiniera(_0) % 0.20/0.49 -iGoatsCheeseTopping(esk2_0) % 0.20/0.49 -iGorgonzolaTopping(esk2_0) % 0.20/0.49 -iGreenPepperTopping(esk2_0) % 0.20/0.49 -iHamTopping(esk2_0) % 0.20/0.49 -iHerbSpiceTopping(esk2_0) % 0.20/0.49 -iHot(iAmerica) % 0.20/0.49 -iHot(iFrance) % 0.20/0.49 -iHot(iItaly) % 0.20/0.49 -iHot(iGermany) % 0.20/0.49 -iHot(iEngland) % 0.20/0.49 -iHot(esk2_0) % 0.20/0.49 -iHotGreenPepperTopping(esk2_0) % 0.20/0.49 -iHotSpicedBeefTopping(esk2_0) % 0.20/0.49 -iIceCream(_0) % 0.20/0.49 -iInterestingPizza(esk2_0) % 0.20/0.49 -iJalapenoPepperTopping(esk2_0) % 0.20/0.49 -iLaReine(_0) % 0.20/0.49 -iLeekTopping(esk2_0) % 0.20/0.49 -iMargherita(_0) % 0.20/0.49 -iMeatTopping(esk2_0) % 0.20/0.49 -iMeatyPizza(esk2_0) % 0.20/0.49 -iMedium(iAmerica) % 0.20/0.49 -iMedium(iFrance) % 0.20/0.49 -iMedium(iItaly) % 0.20/0.49 -iMedium(iGermany) % 0.20/0.49 -iMedium(iEngland) % 0.20/0.49 -iMedium(esk2_0) % 0.20/0.49 -iMild(iAmerica) % 0.20/0.49 -iMild(iFrance) % 0.20/0.49 -iMild(iItaly) % 0.20/0.49 -iMild(iGermany) % 0.20/0.49 -iMild(iEngland) % 0.20/0.49 -iMild(esk2_0) % 0.20/0.49 -iMixedSeafoodTopping(esk2_0) % 0.20/0.49 -iMozzarellaTopping(esk2_0) % 0.20/0.49 -iMushroom(_0) % 0.20/0.49 -iMushroomTopping(esk2_0) % 0.20/0.49 -iNamedPizza(esk2_0) % 0.20/0.49 -iNapoletana(_0) % 0.20/0.49 -iNonVegetarianPizza(esk2_0) % 0.20/0.49 -iNutTopping(esk2_0) % 0.20/0.49 -iOliveTopping(esk2_0) % 0.20/0.49 -iOnionTopping(esk2_0) % 0.20/0.49 -iParmaHamTopping(_0) % 0.20/0.49 -iParmense(_0) % 0.20/0.49 -iParmesanTopping(esk2_0) % 0.20/0.49 -iPeperonataTopping(esk2_0) % 0.20/0.49 -iPeperoniSausageTopping(esk2_0) % 0.20/0.49 -iPepperTopping(esk2_0) % 0.20/0.49 -iPetitPoisTopping(esk2_0) % 0.20/0.49 -iPineKernels(esk2_0) % 0.20/0.49 -iPizza(esk2_0) % 0.20/0.49 -iPizzaBase(esk2_0) % 0.20/0.49 -iPizzaTopping(esk2_0) % 0.20/0.49 -iPolloAdAstra(_0) % 0.20/0.49 -iPrawnsTopping(esk2_0) % 0.20/0.49 -iPrinceCarlo(_0) % 0.20/0.49 -iQuattroFormaggi(_0) % 0.20/0.49 -iRealItalianPizza(esk2_0) % 0.20/0.49 -iRedOnionTopping(esk2_0) % 0.20/0.49 -iRocketTopping(esk2_0) % 0.20/0.49 -iRosa(_0) % 0.20/0.49 -iRosemaryTopping(esk2_0) % 0.20/0.49 -iSauceTopping(esk2_0) % 0.20/0.49 -iSiciliana(_0) % 0.20/0.49 -iSlicedTomatoTopping(esk2_0) % 0.20/0.49 -iSloppyGiuseppe(_0) % 0.20/0.49 -iSoho(_0) % 0.20/0.49 -iSpiciness(iAmerica) % 0.20/0.49 -iSpiciness(iFrance) % 0.20/0.49 -iSpiciness(iItaly) % 0.20/0.49 -iSpiciness(iGermany) % 0.20/0.49 -iSpiciness(iEngland) % 0.20/0.49 -iSpiciness(esk2_0) % 0.20/0.49 -iSpicyPizza(esk2_0) % 0.20/0.49 -iSpicyPizzaEquivalent(esk2_0) % 0.20/0.49 -iSpicyTopping(esk2_0) % 0.20/0.49 -iSpinachTopping(esk2_0) % 0.20/0.49 -iSultanaTopping(esk2_0) % 0.20/0.49 -iSundriedTomatoTopping(esk2_0) % 0.20/0.49 -iSweetPepperTopping(esk2_0) % 0.20/0.49 -iThinAndCrispyBase(esk2_0) % 0.20/0.49 -iThinAndCrispyPizza(esk2_0) % 0.20/0.49 -iTobascoPepperSauce(esk2_0) % 0.20/0.49 -iTomatoTopping(esk2_0) % 0.20/0.49 -iUnclosedPizza(_0) % 0.20/0.49 -iValuePartition(iAmerica) % 0.20/0.49 -iValuePartition(iFrance) % 0.20/0.49 -iValuePartition(iItaly) % 0.20/0.49 -iValuePartition(iGermany) % 0.20/0.49 -iValuePartition(iEngland) % 0.20/0.49 -iValuePartition(esk2_0) % 0.20/0.49 -iVegetableTopping(esk2_0) % 0.20/0.49 -iVegetarianPizza(esk2_0) % 0.20/0.49 -iVegetarianPizzaEquivalent1(esk2_0) % 0.20/0.49 -iVegetarianPizzaEquivalent2(esk2_0) % 0.20/0.49 -iVegetarianTopping(esk2_0) % 0.20/0.49 -iVeneziana(_0) % 0.20/0.49 -ihasBase(_0, esk2_0) % 0.20/0.49 -ihasBase(esk2_0, _0) % 0.20/0.49 -ihasCountryOfOrigin(_0, esk2_0) % 0.20/0.49 -ihasCountryOfOrigin(esk2_0, _0) % 0.20/0.49 -ihasIngredient(_0, esk2_0) % 0.20/0.49 -ihasIngredient(esk2_0, _0) % 0.20/0.49 -ihasSpiciness(_0, iAmerica) % 0.20/0.49 -ihasSpiciness(_0, iFrance) % 0.20/0.49 -ihasSpiciness(_0, iItaly) % 0.20/0.49 -ihasSpiciness(_0, iGermany) % 0.20/0.49 -ihasSpiciness(_0, iEngland) % 0.20/0.49 -ihasSpiciness(_0, esk2_0) % 0.20/0.49 -ihasSpiciness(esk2_0, _0) % 0.20/0.49 -ihasTopping(_0, esk2_0) % 0.20/0.49 -ihasTopping(esk2_0, _0) % 0.20/0.49 -iisBaseOf(_0, esk2_0) % 0.20/0.49 -iisBaseOf(esk2_0, _0) % 0.20/0.49 -iisIngredientOf(_0, esk2_0) % 0.20/0.49 -iisIngredientOf(esk2_0, _0) % 0.20/0.49 -iisToppingOf(_0, esk2_0) % 0.20/0.49 -iisToppingOf(esk2_0, _0) % 0.20/0.49 -iowlNothing(_0) % 0.20/0.49 +iowlThing(=0) % 0.20/0.49 +iowlThing(iAmerica) % 0.20/0.49 +iowlThing(iFrance) % 0.20/0.49 +iowlThing(iItaly) % 0.20/0.49 +iowlThing(iGermany) % 0.20/0.49 +iowlThing(iEngland) % 0.20/0.49 +iowlThing(esk1_0) % 0.20/0.49 -iowlThing(esk2_0) % 0.20/0.49 -xsd_integer(_0) % 0.20/0.49 -xsd_string(_0) % 0.20/0.49 SZS output end Model for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------