%------------------------------------------------------------------------------
% File : Paradox---4.0
% Problem : SWB036+1 : TPTP v8.1.0. Released v5.2.0.
% Transfm : none
% Format : tptp:short
% Command : paradox --no-progress --time %d --tstp --model %s
% Computer : n022.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 : 600s
% DateTime : Tue Jul 19 19:18:19 EDT 2022
% Result : Satisfiable 0.40s 0.61s
% Output : FiniteModel 0.40s
% Verified :
% SZS Type : FiniteModel
% Domain size : 6
% Comments :
%------------------------------------------------------------------------------
% domain size is 6
fof(domain,fi_domain,
! [X] :
( X = "1"
| X = "2"
| X = "3"
| X = "4"
| X = "5"
| X = "6" ) ).
fof(abstractDomain,fi_predicates,
( ( abstractDomain("1")
<=> $true )
& ( abstractDomain("2")
<=> $true )
& ( abstractDomain("3")
<=> $true )
& ( abstractDomain("4")
<=> $true )
& ( abstractDomain("5")
<=> $true )
& ( abstractDomain("6")
<=> $false ) ) ).
fof(dataDomain,fi_predicates,
( ( dataDomain("1")
<=> $false )
& ( dataDomain("2")
<=> $false )
& ( dataDomain("3")
<=> $false )
& ( dataDomain("4")
<=> $false )
& ( dataDomain("5")
<=> $false )
& ( dataDomain("6")
<=> $true ) ) ).
fof(iAmerica,fi_functors,
iAmerica = "4" ).
fof(iAmerican,fi_predicates,
! [X1] :
( iAmerican(X1)
<=> $false ) ).
fof(iAmericanHot,fi_predicates,
! [X1] :
( iAmericanHot(X1)
<=> $false ) ).
fof(iAnchoviesTopping,fi_predicates,
! [X1] :
( iAnchoviesTopping(X1)
<=> $false ) ).
fof(iArtichokeTopping,fi_predicates,
! [X1] :
( iArtichokeTopping(X1)
<=> $false ) ).
fof(iAsparagusTopping,fi_predicates,
! [X1] :
( iAsparagusTopping(X1)
<=> $false ) ).
fof(iCajun,fi_predicates,
! [X1] :
( iCajun(X1)
<=> $false ) ).
fof(iCajunSpiceTopping,fi_predicates,
! [X1] :
( iCajunSpiceTopping(X1)
<=> $false ) ).
fof(iCaperTopping,fi_predicates,
! [X1] :
( iCaperTopping(X1)
<=> $false ) ).
fof(iCapricciosa,fi_predicates,
! [X1] :
( iCapricciosa(X1)
<=> $false ) ).
fof(iCaprina,fi_predicates,
! [X1] :
( iCaprina(X1)
<=> $false ) ).
fof(iCheeseTopping,fi_predicates,
( ( iCheeseTopping("1")
<=> $false )
& ( iCheeseTopping("2")
<=> $false )
& ( iCheeseTopping("3")
<=> $false )
& ( iCheeseTopping("4")
<=> $false )
& ( iCheeseTopping("5")
<=> $false )
& ( iCheeseTopping("6")
<=> $false ) ) ).
fof(iCheeseyPizza,fi_predicates,
( ( iCheeseyPizza("1")
<=> $false )
& ( iCheeseyPizza("2")
<=> $false )
& ( iCheeseyPizza("3")
<=> $false )
& ( iCheeseyPizza("4")
<=> $false )
& ( iCheeseyPizza("5")
<=> $false )
& ( iCheeseyPizza("6")
<=> $false ) ) ).
fof(iCheeseyVegetableTopping,fi_predicates,
! [X1] :
( iCheeseyVegetableTopping(X1)
<=> $false ) ).
fof(iChickenTopping,fi_predicates,
! [X1] :
( iChickenTopping(X1)
<=> $false ) ).
fof(iCountry,fi_predicates,
( ( iCountry("1")
<=> $true )
& ( iCountry("2")
<=> $true )
& ( iCountry("3")
<=> $true )
& ( iCountry("4")
<=> $true )
& ( iCountry("5")
<=> $true )
& ( iCountry("6")
<=> $false ) ) ).
fof(iDeepPanBase,fi_predicates,
! [X1] :
( iDeepPanBase(X1)
<=> $false ) ).
fof(iDomainConcept,fi_predicates,
( ( iDomainConcept("1")
<=> $true )
& ( iDomainConcept("2")
<=> $true )
& ( iDomainConcept("3")
<=> $true )
& ( iDomainConcept("4")
<=> $true )
& ( iDomainConcept("5")
<=> $true )
& ( iDomainConcept("6")
<=> $false ) ) ).
fof(iEngland,fi_functors,
iEngland = "5" ).
fof(iFiorentina,fi_predicates,
! [X1] :
( iFiorentina(X1)
<=> $false ) ).
fof(iFishTopping,fi_predicates,
( ( iFishTopping("1")
<=> $false )
& ( iFishTopping("2")
<=> $false )
& ( iFishTopping("3")
<=> $false )
& ( iFishTopping("4")
<=> $false )
& ( iFishTopping("5")
<=> $false )
& ( iFishTopping("6")
<=> $false ) ) ).
fof(iFood,fi_predicates,
( ( iFood("1")
<=> $false )
& ( iFood("2")
<=> $false )
& ( iFood("3")
<=> $false )
& ( iFood("4")
<=> $false )
& ( iFood("5")
<=> $false )
& ( iFood("6")
<=> $false ) ) ).
fof(iFourCheesesTopping,fi_predicates,
! [X1] :
( iFourCheesesTopping(X1)
<=> $false ) ).
fof(iFourSeasons,fi_predicates,
! [X1] :
( iFourSeasons(X1)
<=> $false ) ).
fof(iFrance,fi_functors,
iFrance = "3" ).
fof(iFruitTopping,fi_predicates,
( ( iFruitTopping("1")
<=> $false )
& ( iFruitTopping("2")
<=> $false )
& ( iFruitTopping("3")
<=> $false )
& ( iFruitTopping("4")
<=> $false )
& ( iFruitTopping("5")
<=> $false )
& ( iFruitTopping("6")
<=> $false ) ) ).
fof(iFruttiDiMare,fi_predicates,
! [X1] :
( iFruttiDiMare(X1)
<=> $false ) ).
fof(iGarlicTopping,fi_predicates,
! [X1] :
( iGarlicTopping(X1)
<=> $false ) ).
fof(iGermany,fi_functors,
iGermany = "1" ).
fof(iGiardiniera,fi_predicates,
! [X1] :
( iGiardiniera(X1)
<=> $false ) ).
fof(iGoatsCheeseTopping,fi_predicates,
! [X1] :
( iGoatsCheeseTopping(X1)
<=> $false ) ).
fof(iGorgonzolaTopping,fi_predicates,
! [X1] :
( iGorgonzolaTopping(X1)
<=> $false ) ).
fof(iGreenPepperTopping,fi_predicates,
! [X1] :
( iGreenPepperTopping(X1)
<=> $false ) ).
fof(iHamTopping,fi_predicates,
! [X1] :
( iHamTopping(X1)
<=> $false ) ).
fof(iHerbSpiceTopping,fi_predicates,
( ( iHerbSpiceTopping("1")
<=> $false )
& ( iHerbSpiceTopping("2")
<=> $false )
& ( iHerbSpiceTopping("3")
<=> $false )
& ( iHerbSpiceTopping("4")
<=> $false )
& ( iHerbSpiceTopping("5")
<=> $false )
& ( iHerbSpiceTopping("6")
<=> $false ) ) ).
fof(iHot,fi_predicates,
( ( iHot("1")
<=> $false )
& ( iHot("2")
<=> $false )
& ( iHot("3")
<=> $false )
& ( iHot("4")
<=> $false )
& ( iHot("5")
<=> $false )
& ( iHot("6")
<=> $false ) ) ).
fof(iHotGreenPepperTopping,fi_predicates,
! [X1] :
( iHotGreenPepperTopping(X1)
<=> $false ) ).
fof(iHotSpicedBeefTopping,fi_predicates,
! [X1] :
( iHotSpicedBeefTopping(X1)
<=> $false ) ).
fof(iIceCream,fi_predicates,
! [X1] :
( iIceCream(X1)
<=> $false ) ).
fof(iInterestingPizza,fi_predicates,
( ( iInterestingPizza("1")
<=> $false )
& ( iInterestingPizza("2")
<=> $false )
& ( iInterestingPizza("3")
<=> $false )
& ( iInterestingPizza("4")
<=> $false )
& ( iInterestingPizza("5")
<=> $false )
& ( iInterestingPizza("6")
<=> $false ) ) ).
fof(iItaly,fi_functors,
iItaly = "2" ).
fof(iJalapenoPepperTopping,fi_predicates,
! [X1] :
( iJalapenoPepperTopping(X1)
<=> $false ) ).
fof(iLaReine,fi_predicates,
! [X1] :
( iLaReine(X1)
<=> $false ) ).
fof(iLeekTopping,fi_predicates,
! [X1] :
( iLeekTopping(X1)
<=> $false ) ).
fof(iMargherita,fi_predicates,
! [X1] :
( iMargherita(X1)
<=> $false ) ).
fof(iMeatTopping,fi_predicates,
( ( iMeatTopping("1")
<=> $false )
& ( iMeatTopping("2")
<=> $false )
& ( iMeatTopping("3")
<=> $false )
& ( iMeatTopping("4")
<=> $false )
& ( iMeatTopping("5")
<=> $false )
& ( iMeatTopping("6")
<=> $false ) ) ).
fof(iMeatyPizza,fi_predicates,
( ( iMeatyPizza("1")
<=> $false )
& ( iMeatyPizza("2")
<=> $false )
& ( iMeatyPizza("3")
<=> $false )
& ( iMeatyPizza("4")
<=> $false )
& ( iMeatyPizza("5")
<=> $false )
& ( iMeatyPizza("6")
<=> $false ) ) ).
fof(iMedium,fi_predicates,
( ( iMedium("1")
<=> $false )
& ( iMedium("2")
<=> $false )
& ( iMedium("3")
<=> $false )
& ( iMedium("4")
<=> $false )
& ( iMedium("5")
<=> $false )
& ( iMedium("6")
<=> $false ) ) ).
fof(iMild,fi_predicates,
( ( iMild("1")
<=> $false )
& ( iMild("2")
<=> $false )
& ( iMild("3")
<=> $false )
& ( iMild("4")
<=> $false )
& ( iMild("5")
<=> $false )
& ( iMild("6")
<=> $false ) ) ).
fof(iMixedSeafoodTopping,fi_predicates,
! [X1] :
( iMixedSeafoodTopping(X1)
<=> $false ) ).
fof(iMozzarellaTopping,fi_predicates,
! [X1] :
( iMozzarellaTopping(X1)
<=> $false ) ).
fof(iMushroom,fi_predicates,
! [X1] :
( iMushroom(X1)
<=> $false ) ).
fof(iMushroomTopping,fi_predicates,
! [X1] :
( iMushroomTopping(X1)
<=> $false ) ).
fof(iNamedPizza,fi_predicates,
! [X1] :
( iNamedPizza(X1)
<=> $false ) ).
fof(iNapoletana,fi_predicates,
! [X1] :
( iNapoletana(X1)
<=> $false ) ).
fof(iNonVegetarianPizza,fi_predicates,
( ( iNonVegetarianPizza("1")
<=> $false )
& ( iNonVegetarianPizza("2")
<=> $false )
& ( iNonVegetarianPizza("3")
<=> $false )
& ( iNonVegetarianPizza("4")
<=> $false )
& ( iNonVegetarianPizza("5")
<=> $false )
& ( iNonVegetarianPizza("6")
<=> $false ) ) ).
fof(iNutTopping,fi_predicates,
( ( iNutTopping("1")
<=> $false )
& ( iNutTopping("2")
<=> $false )
& ( iNutTopping("3")
<=> $false )
& ( iNutTopping("4")
<=> $false )
& ( iNutTopping("5")
<=> $false )
& ( iNutTopping("6")
<=> $false ) ) ).
fof(iOliveTopping,fi_predicates,
! [X1] :
( iOliveTopping(X1)
<=> $false ) ).
fof(iOnionTopping,fi_predicates,
! [X1] :
( iOnionTopping(X1)
<=> $false ) ).
fof(iParmaHamTopping,fi_predicates,
! [X1] :
( iParmaHamTopping(X1)
<=> $false ) ).
fof(iParmense,fi_predicates,
! [X1] :
( iParmense(X1)
<=> $false ) ).
fof(iParmesanTopping,fi_predicates,
! [X1] :
( iParmesanTopping(X1)
<=> $false ) ).
fof(iPeperonataTopping,fi_predicates,
! [X1] :
( iPeperonataTopping(X1)
<=> $false ) ).
fof(iPeperoniSausageTopping,fi_predicates,
! [X1] :
( iPeperoniSausageTopping(X1)
<=> $false ) ).
fof(iPepperTopping,fi_predicates,
! [X1] :
( iPepperTopping(X1)
<=> $false ) ).
fof(iPetitPoisTopping,fi_predicates,
! [X1] :
( iPetitPoisTopping(X1)
<=> $false ) ).
fof(iPineKernels,fi_predicates,
! [X1] :
( iPineKernels(X1)
<=> $false ) ).
fof(iPizza,fi_predicates,
( ( iPizza("1")
<=> $false )
& ( iPizza("2")
<=> $false )
& ( iPizza("3")
<=> $false )
& ( iPizza("4")
<=> $false )
& ( iPizza("5")
<=> $false )
& ( iPizza("6")
<=> $false ) ) ).
fof(iPizzaBase,fi_predicates,
( ( iPizzaBase("1")
<=> $false )
& ( iPizzaBase("2")
<=> $false )
& ( iPizzaBase("3")
<=> $false )
& ( iPizzaBase("4")
<=> $false )
& ( iPizzaBase("5")
<=> $false )
& ( iPizzaBase("6")
<=> $false ) ) ).
fof(iPizzaTopping,fi_predicates,
( ( iPizzaTopping("1")
<=> $false )
& ( iPizzaTopping("2")
<=> $false )
& ( iPizzaTopping("3")
<=> $false )
& ( iPizzaTopping("4")
<=> $false )
& ( iPizzaTopping("5")
<=> $false )
& ( iPizzaTopping("6")
<=> $false ) ) ).
fof(iPolloAdAstra,fi_predicates,
! [X1] :
( iPolloAdAstra(X1)
<=> $false ) ).
fof(iPrawnsTopping,fi_predicates,
! [X1] :
( iPrawnsTopping(X1)
<=> $false ) ).
fof(iPrinceCarlo,fi_predicates,
! [X1] :
( iPrinceCarlo(X1)
<=> $false ) ).
fof(iQuattroFormaggi,fi_predicates,
! [X1] :
( iQuattroFormaggi(X1)
<=> $false ) ).
fof(iRealItalianPizza,fi_predicates,
( ( iRealItalianPizza("1")
<=> $false )
& ( iRealItalianPizza("2")
<=> $false )
& ( iRealItalianPizza("3")
<=> $false )
& ( iRealItalianPizza("4")
<=> $false )
& ( iRealItalianPizza("5")
<=> $false )
& ( iRealItalianPizza("6")
<=> $false ) ) ).
fof(iRedOnionTopping,fi_predicates,
! [X1] :
( iRedOnionTopping(X1)
<=> $false ) ).
fof(iRocketTopping,fi_predicates,
! [X1] :
( iRocketTopping(X1)
<=> $false ) ).
fof(iRosa,fi_predicates,
! [X1] :
( iRosa(X1)
<=> $false ) ).
fof(iRosemaryTopping,fi_predicates,
! [X1] :
( iRosemaryTopping(X1)
<=> $false ) ).
fof(iSauceTopping,fi_predicates,
( ( iSauceTopping("1")
<=> $false )
& ( iSauceTopping("2")
<=> $false )
& ( iSauceTopping("3")
<=> $false )
& ( iSauceTopping("4")
<=> $false )
& ( iSauceTopping("5")
<=> $false )
& ( iSauceTopping("6")
<=> $false ) ) ).
fof(iSiciliana,fi_predicates,
! [X1] :
( iSiciliana(X1)
<=> $false ) ).
fof(iSlicedTomatoTopping,fi_predicates,
! [X1] :
( iSlicedTomatoTopping(X1)
<=> $false ) ).
fof(iSloppyGiuseppe,fi_predicates,
! [X1] :
( iSloppyGiuseppe(X1)
<=> $false ) ).
fof(iSoho,fi_predicates,
! [X1] :
( iSoho(X1)
<=> $false ) ).
fof(iSpiciness,fi_predicates,
( ( iSpiciness("1")
<=> $false )
& ( iSpiciness("2")
<=> $false )
& ( iSpiciness("3")
<=> $false )
& ( iSpiciness("4")
<=> $false )
& ( iSpiciness("5")
<=> $false )
& ( iSpiciness("6")
<=> $false ) ) ).
fof(iSpicyPizza,fi_predicates,
( ( iSpicyPizza("1")
<=> $false )
& ( iSpicyPizza("2")
<=> $false )
& ( iSpicyPizza("3")
<=> $false )
& ( iSpicyPizza("4")
<=> $false )
& ( iSpicyPizza("5")
<=> $false )
& ( iSpicyPizza("6")
<=> $false ) ) ).
fof(iSpicyPizzaEquivalent,fi_predicates,
( ( iSpicyPizzaEquivalent("1")
<=> $false )
& ( iSpicyPizzaEquivalent("2")
<=> $false )
& ( iSpicyPizzaEquivalent("3")
<=> $false )
& ( iSpicyPizzaEquivalent("4")
<=> $false )
& ( iSpicyPizzaEquivalent("5")
<=> $false )
& ( iSpicyPizzaEquivalent("6")
<=> $false ) ) ).
fof(iSpicyTopping,fi_predicates,
( ( iSpicyTopping("1")
<=> $false )
& ( iSpicyTopping("2")
<=> $false )
& ( iSpicyTopping("3")
<=> $false )
& ( iSpicyTopping("4")
<=> $false )
& ( iSpicyTopping("5")
<=> $false )
& ( iSpicyTopping("6")
<=> $false ) ) ).
fof(iSpinachTopping,fi_predicates,
! [X1] :
( iSpinachTopping(X1)
<=> $false ) ).
fof(iSultanaTopping,fi_predicates,
! [X1] :
( iSultanaTopping(X1)
<=> $false ) ).
fof(iSundriedTomatoTopping,fi_predicates,
! [X1] :
( iSundriedTomatoTopping(X1)
<=> $false ) ).
fof(iSweetPepperTopping,fi_predicates,
! [X1] :
( iSweetPepperTopping(X1)
<=> $false ) ).
fof(iThinAndCrispyBase,fi_predicates,
( ( iThinAndCrispyBase("1")
<=> $false )
& ( iThinAndCrispyBase("2")
<=> $false )
& ( iThinAndCrispyBase("3")
<=> $false )
& ( iThinAndCrispyBase("4")
<=> $false )
& ( iThinAndCrispyBase("5")
<=> $false )
& ( iThinAndCrispyBase("6")
<=> $false ) ) ).
fof(iThinAndCrispyPizza,fi_predicates,
( ( iThinAndCrispyPizza("1")
<=> $false )
& ( iThinAndCrispyPizza("2")
<=> $false )
& ( iThinAndCrispyPizza("3")
<=> $false )
& ( iThinAndCrispyPizza("4")
<=> $false )
& ( iThinAndCrispyPizza("5")
<=> $false )
& ( iThinAndCrispyPizza("6")
<=> $false ) ) ).
fof(iTobascoPepperSauce,fi_predicates,
! [X1] :
( iTobascoPepperSauce(X1)
<=> $false ) ).
fof(iTomatoTopping,fi_predicates,
! [X1] :
( iTomatoTopping(X1)
<=> $false ) ).
fof(iUnclosedPizza,fi_predicates,
! [X1] :
( iUnclosedPizza(X1)
<=> $false ) ).
fof(iValuePartition,fi_predicates,
( ( iValuePartition("1")
<=> $false )
& ( iValuePartition("2")
<=> $false )
& ( iValuePartition("3")
<=> $false )
& ( iValuePartition("4")
<=> $false )
& ( iValuePartition("5")
<=> $false )
& ( iValuePartition("6")
<=> $false ) ) ).
fof(iVegetableTopping,fi_predicates,
( ( iVegetableTopping("1")
<=> $false )
& ( iVegetableTopping("2")
<=> $false )
& ( iVegetableTopping("3")
<=> $false )
& ( iVegetableTopping("4")
<=> $false )
& ( iVegetableTopping("5")
<=> $false )
& ( iVegetableTopping("6")
<=> $false ) ) ).
fof(iVegetarianPizza,fi_predicates,
( ( iVegetarianPizza("1")
<=> $false )
& ( iVegetarianPizza("2")
<=> $false )
& ( iVegetarianPizza("3")
<=> $false )
& ( iVegetarianPizza("4")
<=> $false )
& ( iVegetarianPizza("5")
<=> $false )
& ( iVegetarianPizza("6")
<=> $false ) ) ).
fof(iVegetarianPizzaEquivalent1,fi_predicates,
( ( iVegetarianPizzaEquivalent1("1")
<=> $false )
& ( iVegetarianPizzaEquivalent1("2")
<=> $false )
& ( iVegetarianPizzaEquivalent1("3")
<=> $false )
& ( iVegetarianPizzaEquivalent1("4")
<=> $false )
& ( iVegetarianPizzaEquivalent1("5")
<=> $false )
& ( iVegetarianPizzaEquivalent1("6")
<=> $false ) ) ).
fof(iVegetarianPizzaEquivalent2,fi_predicates,
( ( iVegetarianPizzaEquivalent2("1")
<=> $false )
& ( iVegetarianPizzaEquivalent2("2")
<=> $false )
& ( iVegetarianPizzaEquivalent2("3")
<=> $false )
& ( iVegetarianPizzaEquivalent2("4")
<=> $false )
& ( iVegetarianPizzaEquivalent2("5")
<=> $false )
& ( iVegetarianPizzaEquivalent2("6")
<=> $false ) ) ).
fof(iVegetarianTopping,fi_predicates,
( ( iVegetarianTopping("1")
<=> $false )
& ( iVegetarianTopping("2")
<=> $false )
& ( iVegetarianTopping("3")
<=> $false )
& ( iVegetarianTopping("4")
<=> $false )
& ( iVegetarianTopping("5")
<=> $false )
& ( iVegetarianTopping("6")
<=> $false ) ) ).
fof(iVeneziana,fi_predicates,
! [X1] :
( iVeneziana(X1)
<=> $false ) ).
fof(ihasBase,fi_predicates,
( ( ihasBase("1","1")
<=> $false )
& ( ihasBase("1","2")
<=> $false )
& ( ihasBase("1","3")
<=> $false )
& ( ihasBase("1","4")
<=> $false )
& ( ihasBase("1","5")
<=> $false )
& ( ihasBase("1","6")
<=> $false )
& ( ihasBase("2","1")
<=> $false )
& ( ihasBase("2","2")
<=> $false )
& ( ihasBase("2","3")
<=> $false )
& ( ihasBase("2","4")
<=> $false )
& ( ihasBase("2","5")
<=> $false )
& ( ihasBase("2","6")
<=> $false )
& ( ihasBase("3","1")
<=> $false )
& ( ihasBase("3","2")
<=> $false )
& ( ihasBase("3","3")
<=> $false )
& ( ihasBase("3","4")
<=> $false )
& ( ihasBase("3","5")
<=> $false )
& ( ihasBase("3","6")
<=> $false )
& ( ihasBase("4","1")
<=> $false )
& ( ihasBase("4","2")
<=> $false )
& ( ihasBase("4","3")
<=> $false )
& ( ihasBase("4","4")
<=> $false )
& ( ihasBase("4","5")
<=> $false )
& ( ihasBase("4","6")
<=> $false )
& ( ihasBase("5","1")
<=> $false )
& ( ihasBase("5","2")
<=> $false )
& ( ihasBase("5","3")
<=> $false )
& ( ihasBase("5","4")
<=> $false )
& ( ihasBase("5","5")
<=> $false )
& ( ihasBase("5","6")
<=> $false )
& ( ihasBase("6","1")
<=> $false )
& ( ihasBase("6","2")
<=> $false )
& ( ihasBase("6","3")
<=> $false )
& ( ihasBase("6","4")
<=> $false )
& ( ihasBase("6","5")
<=> $false )
& ( ihasBase("6","6")
<=> $false ) ) ).
fof(ihasCountryOfOrigin,fi_predicates,
( ( ihasCountryOfOrigin("1","1")
<=> $true )
& ( ihasCountryOfOrigin("1","2")
<=> $false )
& ( ihasCountryOfOrigin("1","3")
<=> $true )
& ( ihasCountryOfOrigin("1","4")
<=> $true )
& ( ihasCountryOfOrigin("1","5")
<=> $true )
& ( ihasCountryOfOrigin("1","6")
<=> $false )
& ( ihasCountryOfOrigin("2","1")
<=> $true )
& ( ihasCountryOfOrigin("2","2")
<=> $false )
& ( ihasCountryOfOrigin("2","3")
<=> $false )
& ( ihasCountryOfOrigin("2","4")
<=> $true )
& ( ihasCountryOfOrigin("2","5")
<=> $true )
& ( ihasCountryOfOrigin("2","6")
<=> $false )
& ( ihasCountryOfOrigin("3","1")
<=> $false )
& ( ihasCountryOfOrigin("3","2")
<=> $false )
& ( ihasCountryOfOrigin("3","3")
<=> $false )
& ( ihasCountryOfOrigin("3","4")
<=> $false )
& ( ihasCountryOfOrigin("3","5")
<=> $true )
& ( ihasCountryOfOrigin("3","6")
<=> $false )
& ( ihasCountryOfOrigin("4","1")
<=> $true )
& ( ihasCountryOfOrigin("4","2")
<=> $false )
& ( ihasCountryOfOrigin("4","3")
<=> $false )
& ( ihasCountryOfOrigin("4","4")
<=> $true )
& ( ihasCountryOfOrigin("4","5")
<=> $true )
& ( ihasCountryOfOrigin("4","6")
<=> $false )
& ( ihasCountryOfOrigin("5","1")
<=> $false )
& ( ihasCountryOfOrigin("5","2")
<=> $false )
& ( ihasCountryOfOrigin("5","3")
<=> $false )
& ( ihasCountryOfOrigin("5","4")
<=> $false )
& ( ihasCountryOfOrigin("5","5")
<=> $true )
& ( ihasCountryOfOrigin("5","6")
<=> $false )
& ( ihasCountryOfOrigin("6","1")
<=> $false )
& ( ihasCountryOfOrigin("6","2")
<=> $false )
& ( ihasCountryOfOrigin("6","3")
<=> $false )
& ( ihasCountryOfOrigin("6","4")
<=> $false )
& ( ihasCountryOfOrigin("6","5")
<=> $false )
& ( ihasCountryOfOrigin("6","6")
<=> $false ) ) ).
fof(ihasIngredient,fi_predicates,
( ( ihasIngredient("1","1")
<=> $false )
& ( ihasIngredient("1","2")
<=> $false )
& ( ihasIngredient("1","3")
<=> $false )
& ( ihasIngredient("1","4")
<=> $false )
& ( ihasIngredient("1","5")
<=> $false )
& ( ihasIngredient("1","6")
<=> $false )
& ( ihasIngredient("2","1")
<=> $false )
& ( ihasIngredient("2","2")
<=> $false )
& ( ihasIngredient("2","3")
<=> $false )
& ( ihasIngredient("2","4")
<=> $false )
& ( ihasIngredient("2","5")
<=> $false )
& ( ihasIngredient("2","6")
<=> $false )
& ( ihasIngredient("3","1")
<=> $false )
& ( ihasIngredient("3","2")
<=> $false )
& ( ihasIngredient("3","3")
<=> $false )
& ( ihasIngredient("3","4")
<=> $false )
& ( ihasIngredient("3","5")
<=> $false )
& ( ihasIngredient("3","6")
<=> $false )
& ( ihasIngredient("4","1")
<=> $false )
& ( ihasIngredient("4","2")
<=> $false )
& ( ihasIngredient("4","3")
<=> $false )
& ( ihasIngredient("4","4")
<=> $false )
& ( ihasIngredient("4","5")
<=> $false )
& ( ihasIngredient("4","6")
<=> $false )
& ( ihasIngredient("5","1")
<=> $false )
& ( ihasIngredient("5","2")
<=> $false )
& ( ihasIngredient("5","3")
<=> $false )
& ( ihasIngredient("5","4")
<=> $false )
& ( ihasIngredient("5","5")
<=> $false )
& ( ihasIngredient("5","6")
<=> $false )
& ( ihasIngredient("6","1")
<=> $false )
& ( ihasIngredient("6","2")
<=> $false )
& ( ihasIngredient("6","3")
<=> $false )
& ( ihasIngredient("6","4")
<=> $false )
& ( ihasIngredient("6","5")
<=> $false )
& ( ihasIngredient("6","6")
<=> $false ) ) ).
fof(ihasSpiciness,fi_predicates,
( ( ihasSpiciness("1","1")
<=> $false )
& ( ihasSpiciness("1","2")
<=> $false )
& ( ihasSpiciness("1","3")
<=> $false )
& ( ihasSpiciness("1","4")
<=> $false )
& ( ihasSpiciness("1","5")
<=> $false )
& ( ihasSpiciness("1","6")
<=> $false )
& ( ihasSpiciness("2","1")
<=> $false )
& ( ihasSpiciness("2","2")
<=> $false )
& ( ihasSpiciness("2","3")
<=> $false )
& ( ihasSpiciness("2","4")
<=> $false )
& ( ihasSpiciness("2","5")
<=> $false )
& ( ihasSpiciness("2","6")
<=> $false )
& ( ihasSpiciness("3","1")
<=> $false )
& ( ihasSpiciness("3","2")
<=> $false )
& ( ihasSpiciness("3","3")
<=> $false )
& ( ihasSpiciness("3","4")
<=> $false )
& ( ihasSpiciness("3","5")
<=> $false )
& ( ihasSpiciness("3","6")
<=> $false )
& ( ihasSpiciness("4","1")
<=> $false )
& ( ihasSpiciness("4","2")
<=> $false )
& ( ihasSpiciness("4","3")
<=> $false )
& ( ihasSpiciness("4","4")
<=> $false )
& ( ihasSpiciness("4","5")
<=> $false )
& ( ihasSpiciness("4","6")
<=> $false )
& ( ihasSpiciness("5","1")
<=> $false )
& ( ihasSpiciness("5","2")
<=> $false )
& ( ihasSpiciness("5","3")
<=> $false )
& ( ihasSpiciness("5","4")
<=> $false )
& ( ihasSpiciness("5","5")
<=> $false )
& ( ihasSpiciness("5","6")
<=> $false )
& ( ihasSpiciness("6","1")
<=> $false )
& ( ihasSpiciness("6","2")
<=> $false )
& ( ihasSpiciness("6","3")
<=> $false )
& ( ihasSpiciness("6","4")
<=> $false )
& ( ihasSpiciness("6","5")
<=> $false )
& ( ihasSpiciness("6","6")
<=> $false ) ) ).
fof(ihasTopping,fi_predicates,
( ( ihasTopping("1","1")
<=> $false )
& ( ihasTopping("1","2")
<=> $false )
& ( ihasTopping("1","3")
<=> $false )
& ( ihasTopping("1","4")
<=> $false )
& ( ihasTopping("1","5")
<=> $false )
& ( ihasTopping("1","6")
<=> $false )
& ( ihasTopping("2","1")
<=> $false )
& ( ihasTopping("2","2")
<=> $false )
& ( ihasTopping("2","3")
<=> $false )
& ( ihasTopping("2","4")
<=> $false )
& ( ihasTopping("2","5")
<=> $false )
& ( ihasTopping("2","6")
<=> $false )
& ( ihasTopping("3","1")
<=> $false )
& ( ihasTopping("3","2")
<=> $false )
& ( ihasTopping("3","3")
<=> $false )
& ( ihasTopping("3","4")
<=> $false )
& ( ihasTopping("3","5")
<=> $false )
& ( ihasTopping("3","6")
<=> $false )
& ( ihasTopping("4","1")
<=> $false )
& ( ihasTopping("4","2")
<=> $false )
& ( ihasTopping("4","3")
<=> $false )
& ( ihasTopping("4","4")
<=> $false )
& ( ihasTopping("4","5")
<=> $false )
& ( ihasTopping("4","6")
<=> $false )
& ( ihasTopping("5","1")
<=> $false )
& ( ihasTopping("5","2")
<=> $false )
& ( ihasTopping("5","3")
<=> $false )
& ( ihasTopping("5","4")
<=> $false )
& ( ihasTopping("5","5")
<=> $false )
& ( ihasTopping("5","6")
<=> $false )
& ( ihasTopping("6","1")
<=> $false )
& ( ihasTopping("6","2")
<=> $false )
& ( ihasTopping("6","3")
<=> $false )
& ( ihasTopping("6","4")
<=> $false )
& ( ihasTopping("6","5")
<=> $false )
& ( ihasTopping("6","6")
<=> $false ) ) ).
fof(iisBaseOf,fi_predicates,
( ( iisBaseOf("1","1")
<=> $false )
& ( iisBaseOf("1","2")
<=> $false )
& ( iisBaseOf("1","3")
<=> $false )
& ( iisBaseOf("1","4")
<=> $false )
& ( iisBaseOf("1","5")
<=> $false )
& ( iisBaseOf("1","6")
<=> $false )
& ( iisBaseOf("2","1")
<=> $false )
& ( iisBaseOf("2","2")
<=> $false )
& ( iisBaseOf("2","3")
<=> $false )
& ( iisBaseOf("2","4")
<=> $false )
& ( iisBaseOf("2","5")
<=> $false )
& ( iisBaseOf("2","6")
<=> $false )
& ( iisBaseOf("3","1")
<=> $false )
& ( iisBaseOf("3","2")
<=> $false )
& ( iisBaseOf("3","3")
<=> $false )
& ( iisBaseOf("3","4")
<=> $false )
& ( iisBaseOf("3","5")
<=> $false )
& ( iisBaseOf("3","6")
<=> $false )
& ( iisBaseOf("4","1")
<=> $false )
& ( iisBaseOf("4","2")
<=> $false )
& ( iisBaseOf("4","3")
<=> $false )
& ( iisBaseOf("4","4")
<=> $false )
& ( iisBaseOf("4","5")
<=> $false )
& ( iisBaseOf("4","6")
<=> $false )
& ( iisBaseOf("5","1")
<=> $false )
& ( iisBaseOf("5","2")
<=> $false )
& ( iisBaseOf("5","3")
<=> $false )
& ( iisBaseOf("5","4")
<=> $false )
& ( iisBaseOf("5","5")
<=> $false )
& ( iisBaseOf("5","6")
<=> $false )
& ( iisBaseOf("6","1")
<=> $false )
& ( iisBaseOf("6","2")
<=> $false )
& ( iisBaseOf("6","3")
<=> $false )
& ( iisBaseOf("6","4")
<=> $false )
& ( iisBaseOf("6","5")
<=> $false )
& ( iisBaseOf("6","6")
<=> $false ) ) ).
fof(iisIngredientOf,fi_predicates,
( ( iisIngredientOf("1","1")
<=> $false )
& ( iisIngredientOf("1","2")
<=> $false )
& ( iisIngredientOf("1","3")
<=> $false )
& ( iisIngredientOf("1","4")
<=> $false )
& ( iisIngredientOf("1","5")
<=> $false )
& ( iisIngredientOf("1","6")
<=> $false )
& ( iisIngredientOf("2","1")
<=> $false )
& ( iisIngredientOf("2","2")
<=> $false )
& ( iisIngredientOf("2","3")
<=> $false )
& ( iisIngredientOf("2","4")
<=> $false )
& ( iisIngredientOf("2","5")
<=> $false )
& ( iisIngredientOf("2","6")
<=> $false )
& ( iisIngredientOf("3","1")
<=> $false )
& ( iisIngredientOf("3","2")
<=> $false )
& ( iisIngredientOf("3","3")
<=> $false )
& ( iisIngredientOf("3","4")
<=> $false )
& ( iisIngredientOf("3","5")
<=> $false )
& ( iisIngredientOf("3","6")
<=> $false )
& ( iisIngredientOf("4","1")
<=> $false )
& ( iisIngredientOf("4","2")
<=> $false )
& ( iisIngredientOf("4","3")
<=> $false )
& ( iisIngredientOf("4","4")
<=> $false )
& ( iisIngredientOf("4","5")
<=> $false )
& ( iisIngredientOf("4","6")
<=> $false )
& ( iisIngredientOf("5","1")
<=> $false )
& ( iisIngredientOf("5","2")
<=> $false )
& ( iisIngredientOf("5","3")
<=> $false )
& ( iisIngredientOf("5","4")
<=> $false )
& ( iisIngredientOf("5","5")
<=> $false )
& ( iisIngredientOf("5","6")
<=> $false )
& ( iisIngredientOf("6","1")
<=> $false )
& ( iisIngredientOf("6","2")
<=> $false )
& ( iisIngredientOf("6","3")
<=> $false )
& ( iisIngredientOf("6","4")
<=> $false )
& ( iisIngredientOf("6","5")
<=> $false )
& ( iisIngredientOf("6","6")
<=> $false ) ) ).
fof(iisToppingOf,fi_predicates,
( ( iisToppingOf("1","1")
<=> $false )
& ( iisToppingOf("1","2")
<=> $false )
& ( iisToppingOf("1","3")
<=> $false )
& ( iisToppingOf("1","4")
<=> $false )
& ( iisToppingOf("1","5")
<=> $false )
& ( iisToppingOf("1","6")
<=> $false )
& ( iisToppingOf("2","1")
<=> $false )
& ( iisToppingOf("2","2")
<=> $false )
& ( iisToppingOf("2","3")
<=> $false )
& ( iisToppingOf("2","4")
<=> $false )
& ( iisToppingOf("2","5")
<=> $false )
& ( iisToppingOf("2","6")
<=> $false )
& ( iisToppingOf("3","1")
<=> $false )
& ( iisToppingOf("3","2")
<=> $false )
& ( iisToppingOf("3","3")
<=> $false )
& ( iisToppingOf("3","4")
<=> $false )
& ( iisToppingOf("3","5")
<=> $false )
& ( iisToppingOf("3","6")
<=> $false )
& ( iisToppingOf("4","1")
<=> $false )
& ( iisToppingOf("4","2")
<=> $false )
& ( iisToppingOf("4","3")
<=> $false )
& ( iisToppingOf("4","4")
<=> $false )
& ( iisToppingOf("4","5")
<=> $false )
& ( iisToppingOf("4","6")
<=> $false )
& ( iisToppingOf("5","1")
<=> $false )
& ( iisToppingOf("5","2")
<=> $false )
& ( iisToppingOf("5","3")
<=> $false )
& ( iisToppingOf("5","4")
<=> $false )
& ( iisToppingOf("5","5")
<=> $false )
& ( iisToppingOf("5","6")
<=> $false )
& ( iisToppingOf("6","1")
<=> $false )
& ( iisToppingOf("6","2")
<=> $false )
& ( iisToppingOf("6","3")
<=> $false )
& ( iisToppingOf("6","4")
<=> $false )
& ( iisToppingOf("6","5")
<=> $false )
& ( iisToppingOf("6","6")
<=> $false ) ) ).
fof(iowlNothing,fi_predicates,
! [X1] :
( iowlNothing(X1)
<=> $false ) ).
fof(iowlThing,fi_predicates,
( ( iowlThing("1")
<=> $true )
& ( iowlThing("2")
<=> $true )
& ( iowlThing("3")
<=> $true )
& ( iowlThing("4")
<=> $true )
& ( iowlThing("5")
<=> $true )
& ( iowlThing("6")
<=> $false ) ) ).
fof(sK104_axiom_70_Y,fi_functors,
( sK104_axiom_70_Y("1") = "1"
& sK104_axiom_70_Y("2") = "1"
& sK104_axiom_70_Y("3") = "2"
& sK104_axiom_70_Y("4") = "3"
& sK104_axiom_70_Y("5") = "4"
& sK104_axiom_70_Y("6") = "5" ) ).
fof(sK136_axiom_92_Y,fi_functors,
( sK136_axiom_92_Y("1") = "1"
& sK136_axiom_92_Y("2") = "1"
& sK136_axiom_92_Y("3") = "2"
& sK136_axiom_92_Y("4") = "3"
& sK136_axiom_92_Y("5") = "4"
& sK136_axiom_92_Y("6") = "5" ) ).
fof(sK1_axiom_1_X,fi_functors,
sK1_axiom_1_X = "2" ).
fof(sK228_axiom_155_Y0,fi_functors,
( sK228_axiom_155_Y0("1") = "1"
& sK228_axiom_155_Y0("2") = "1"
& sK228_axiom_155_Y0("3") = "2"
& sK228_axiom_155_Y0("4") = "3"
& sK228_axiom_155_Y0("5") = "4"
& sK228_axiom_155_Y0("6") = "5" ) ).
fof(sK229_axiom_155_Y1,fi_functors,
( sK229_axiom_155_Y1("1") = "1"
& sK229_axiom_155_Y1("2") = "1"
& sK229_axiom_155_Y1("3") = "2"
& sK229_axiom_155_Y1("4") = "3"
& sK229_axiom_155_Y1("5") = "4"
& sK229_axiom_155_Y1("6") = "5" ) ).
fof(sK230_axiom_155_Y2,fi_functors,
( sK230_axiom_155_Y2("1") = "1"
& sK230_axiom_155_Y2("2") = "1"
& sK230_axiom_155_Y2("3") = "2"
& sK230_axiom_155_Y2("4") = "3"
& sK230_axiom_155_Y2("5") = "4"
& sK230_axiom_155_Y2("6") = "5" ) ).
fof(sK268_axiom_178_Y,fi_functors,
( sK268_axiom_178_Y("1") = "1"
& sK268_axiom_178_Y("2") = "1"
& sK268_axiom_178_Y("3") = "2"
& sK268_axiom_178_Y("4") = "3"
& sK268_axiom_178_Y("5") = "4"
& sK268_axiom_178_Y("6") = "5" ) ).
fof(sK2_axiom_2_X,fi_functors,
sK2_axiom_2_X = "6" ).
fof(sK316_axiom_212_Y,fi_functors,
( sK316_axiom_212_Y("1") = "1"
& sK316_axiom_212_Y("2") = "1"
& sK316_axiom_212_Y("3") = "2"
& sK316_axiom_212_Y("4") = "3"
& sK316_axiom_212_Y("5") = "4"
& sK316_axiom_212_Y("6") = "5" ) ).
fof(sK366_axiom_248_Y,fi_functors,
( sK366_axiom_248_Y("1") = "1"
& sK366_axiom_248_Y("2") = "1"
& sK366_axiom_248_Y("3") = "2"
& sK366_axiom_248_Y("4") = "3"
& sK366_axiom_248_Y("5") = "4"
& sK366_axiom_248_Y("6") = "5" ) ).
fof(sK497_axiom_332_Y,fi_functors,
( sK497_axiom_332_Y("1") = "1"
& sK497_axiom_332_Y("2") = "1"
& sK497_axiom_332_Y("3") = "2"
& sK497_axiom_332_Y("4") = "3"
& sK497_axiom_332_Y("5") = "4"
& sK497_axiom_332_Y("6") = "5" ) ).
fof(sK501_axiom_334_Y,fi_functors,
( sK501_axiom_334_Y("1") = "1"
& sK501_axiom_334_Y("2") = "1"
& sK501_axiom_334_Y("3") = "2"
& sK501_axiom_334_Y("4") = "3"
& sK501_axiom_334_Y("5") = "4"
& sK501_axiom_334_Y("6") = "5" ) ).
fof(sK502_axiom_334_Z,fi_functors,
( sK502_axiom_334_Z("1") = "1"
& sK502_axiom_334_Z("2") = "1"
& sK502_axiom_334_Z("3") = "2"
& sK502_axiom_334_Z("4") = "3"
& sK502_axiom_334_Z("5") = "4"
& sK502_axiom_334_Z("6") = "5" ) ).
fof(sK507_axiom_336_Y,fi_functors,
( sK507_axiom_336_Y("1") = "1"
& sK507_axiom_336_Y("2") = "1"
& sK507_axiom_336_Y("3") = "2"
& sK507_axiom_336_Y("4") = "3"
& sK507_axiom_336_Y("5") = "4"
& sK507_axiom_336_Y("6") = "5" ) ).
fof(sK529_axiom_352_Y,fi_functors,
( sK529_axiom_352_Y("1") = "1"
& sK529_axiom_352_Y("2") = "1"
& sK529_axiom_352_Y("3") = "2"
& sK529_axiom_352_Y("4") = "3"
& sK529_axiom_352_Y("5") = "4"
& sK529_axiom_352_Y("6") = "5" ) ).
fof(sK548_axiom_366_Y,fi_functors,
( sK548_axiom_366_Y("1") = "1"
& sK548_axiom_366_Y("2") = "1"
& sK548_axiom_366_Y("3") = "2"
& sK548_axiom_366_Y("4") = "3"
& sK548_axiom_366_Y("5") = "4"
& sK548_axiom_366_Y("6") = "5" ) ).
fof(sK549_axiom_366_Y,fi_functors,
( sK549_axiom_366_Y("1") = "1"
& sK549_axiom_366_Y("2") = "1"
& sK549_axiom_366_Y("3") = "2"
& sK549_axiom_366_Y("4") = "3"
& sK549_axiom_366_Y("5") = "4"
& sK549_axiom_366_Y("6") = "5" ) ).
fof(sK554_axiom_368_Y,fi_functors,
( sK554_axiom_368_Y("1") = "1"
& sK554_axiom_368_Y("2") = "1"
& sK554_axiom_368_Y("3") = "2"
& sK554_axiom_368_Y("4") = "3"
& sK554_axiom_368_Y("5") = "4"
& sK554_axiom_368_Y("6") = "5" ) ).
fof(sK558_axiom_370_Y,fi_functors,
( sK558_axiom_370_Y("1") = "1"
& sK558_axiom_370_Y("2") = "1"
& sK558_axiom_370_Y("3") = "2"
& sK558_axiom_370_Y("4") = "3"
& sK558_axiom_370_Y("5") = "4"
& sK558_axiom_370_Y("6") = "5" ) ).
fof(xsd_integer,fi_predicates,
! [X1] :
( xsd_integer(X1)
<=> $false ) ).
fof(xsd_string,fi_predicates,
! [X1] :
( xsd_string(X1)
<=> $false ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWB036+1 : TPTP v8.1.0. Released v5.2.0.
% 0.07/0.12 % Command : paradox --no-progress --time %d --tstp --model %s
% 0.13/0.34 % Computer : n022.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Wed Jun 1 12:23:52 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.13/0.34 Paradox, version 4.0, 2010-06-29.
% 0.13/0.34 +++ PROBLEM: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.34 Reading '/export/starexec/sandbox2/benchmark/theBenchmark.p' ... OK
% 0.20/0.52 +++ SOLVING: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.40/0.60 +++ BEGIN MODEL
% 0.40/0.60 SZS output start FiniteModel for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 0.40/0.61 +++ END MODEL
% 0.40/0.61 +++ RESULT: Satisfiable
% 0.40/0.61 SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------