%------------------------------------------------------------------------------ % File : Z3---4.15.1 % Problem : SWB036+1 : TPTP v9.0.0. Released v5.2.0. % Transfm : none % Format : tptp % Command : run_E %s %d THM % Computer : n015.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 : 300s % DateTime : Sat Jun 21 05:29:43 AM UTC 2025 % Result : Satisfiable 1.15s 1.32s % Output : Model 1.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : SWB036+1 : TPTP v9.0.0. Released v5.2.0. % 0.08/0.13 % Command : run_E %s %d THM % 0.12/0.34 % Computer : n015.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 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Jun 20 07:53:26 EDT 2025 % 0.12/0.34 % CPUTime : % 1.15/1.32 % SZS status Satisfiable % 1.15/1.32 % SZS output start Model % 1.15/1.32 tff(tptp_fun__i_val_3_type, type, ( % 1.15/1.32 tptp_fun__i_val_3: $i)). % 1.15/1.32 tff(iEngland_type, type, ( % 1.15/1.32 iEngland: $i)). % 1.15/1.32 tff(tptp_fun__i_val_2_type, type, ( % 1.15/1.32 tptp_fun__i_val_2: $i)). % 1.15/1.32 tff(iAmerica_type, type, ( % 1.15/1.32 iAmerica: $i)). % 1.15/1.32 tff(tptp_fun__i_val_4_type, type, ( % 1.15/1.32 tptp_fun__i_val_4: $i)). % 1.15/1.32 tff(iFrance_type, type, ( % 1.15/1.32 iFrance: $i)). % 1.15/1.32 tff(tptp_fun__i_val_6_type, type, ( % 1.15/1.32 tptp_fun__i_val_6: $i)). % 1.15/1.32 tff(iItaly_type, type, ( % 1.15/1.32 iItaly: $i)). % 1.15/1.32 tff(tptp_fun__i_val_5_type, type, ( % 1.15/1.32 tptp_fun__i_val_5: $i)). % 1.15/1.32 tff(iGermany_type, type, ( % 1.15/1.32 iGermany: $i)). % 1.15/1.32 tff(tptp_fun__i_val_13_type, type, ( % 1.15/1.32 tptp_fun__i_val_13: $i)). % 1.15/1.32 tff(k!1968_type, type, ( % 1.15/1.32 k!1968: $i > $i)). % 1.15/1.32 tff(tptp_fun__i_val_16_type, type, ( % 1.15/1.32 tptp_fun__i_val_16: $i)). % 1.15/1.32 tff(tptp_fun__i_val_9_type, type, ( % 1.15/1.32 tptp_fun__i_val_9: $i)). % 1.15/1.32 tff(tptp_fun__i_val_15_type, type, ( % 1.15/1.32 tptp_fun__i_val_15: $i)). % 1.15/1.32 tff(tptp_fun__i_val_7_type, type, ( % 1.15/1.32 tptp_fun__i_val_7: $i)). % 1.15/1.32 tff(tptp_fun__i_val_11_type, type, ( % 1.15/1.32 tptp_fun__i_val_11: $i)). % 1.15/1.32 tff(tptp_fun__i_val_19_type, type, ( % 1.15/1.32 tptp_fun__i_val_19: $i)). % 1.15/1.32 tff(tptp_fun__i_val_10_type, type, ( % 1.15/1.32 tptp_fun__i_val_10: $i)). % 1.15/1.32 tff(tptp_fun__i_val_14_type, type, ( % 1.15/1.32 tptp_fun__i_val_14: $i)). % 1.15/1.32 tff(tptp_fun__i_val_17_type, type, ( % 1.15/1.32 tptp_fun__i_val_17: $i)). % 1.15/1.32 tff(tptp_fun__i_val_18_type, type, ( % 1.15/1.32 tptp_fun__i_val_18: $i)). % 1.15/1.32 tff(tptp_fun__i_val_12_type, type, ( % 1.15/1.32 tptp_fun__i_val_12: $i)). % 1.15/1.32 tff(tptp_fun__i_val_1_type, type, ( % 1.15/1.32 tptp_fun__i_val_1: $i)). % 1.15/1.32 tff(tptp_fun__i_val_8_type, type, ( % 1.15/1.32 tptp_fun__i_val_8: $i)). % 1.15/1.32 tff(tptp_fun__i_val_0_type, type, ( % 1.15/1.32 tptp_fun__i_val_0: $i)). % 1.15/1.32 tff(iCountry_type, type, ( % 1.15/1.32 iCountry: $i > $o)). % 1.15/1.32 tff(iNamedPizza_type, type, ( % 1.15/1.32 iNamedPizza: $i > $o)). % 1.15/1.32 tff(iArtichokeTopping_type, type, ( % 1.15/1.32 iArtichokeTopping: $i > $o)). % 1.15/1.32 tff(iSpicyPizzaEquivalent_type, type, ( % 1.15/1.32 iSpicyPizzaEquivalent: $i > $o)). % 1.15/1.32 tff(dataDomain_type, type, ( % 1.15/1.32 dataDomain: $i > $o)). % 1.15/1.32 tff(iTobascoPepperSauce_type, type, ( % 1.15/1.32 iTobascoPepperSauce: $i > $o)). % 1.15/1.32 tff(iSloppyGiuseppe_type, type, ( % 1.15/1.32 iSloppyGiuseppe: $i > $o)). % 1.15/1.32 tff(iMild_type, type, ( % 1.15/1.32 iMild: $i > $o)). % 1.15/1.32 tff(iDeepPanBase_type, type, ( % 1.15/1.32 iDeepPanBase: $i > $o)). % 1.15/1.32 tff(iPineKernels_type, type, ( % 1.15/1.32 iPineKernels: $i > $o)). % 1.15/1.32 tff(iDomainConcept_type, type, ( % 1.15/1.32 iDomainConcept: $i > $o)). % 1.15/1.32 tff(iCapricciosa_type, type, ( % 1.15/1.32 iCapricciosa: $i > $o)). % 1.15/1.32 tff(iChickenTopping_type, type, ( % 1.15/1.32 iChickenTopping: $i > $o)). % 1.15/1.32 tff(iisIngredientOf_type, type, ( % 1.15/1.32 iisIngredientOf: ( $i * $i ) > $o)). % 1.15/1.32 tff(iRocketTopping_type, type, ( % 1.15/1.32 iRocketTopping: $i > $o)). % 1.15/1.32 tff(iTomatoTopping_type, type, ( % 1.15/1.32 iTomatoTopping: $i > $o)). % 1.15/1.32 tff(ihasCountryOfOrigin_type, type, ( % 1.15/1.32 ihasCountryOfOrigin: ( $i * $i ) > $o)). % 1.15/1.32 tff(iRosemaryTopping_type, type, ( % 1.15/1.32 iRosemaryTopping: $i > $o)). % 1.15/1.32 tff(iRosa_type, type, ( % 1.15/1.32 iRosa: $i > $o)). % 1.15/1.32 tff(iisToppingOf_type, type, ( % 1.15/1.32 iisToppingOf: ( $i * $i ) > $o)). % 1.15/1.32 tff(ihasSpiciness_type, type, ( % 1.15/1.32 ihasSpiciness: ( $i * $i ) > $o)). % 1.15/1.32 tff(iSpiciness_type, type, ( % 1.15/1.32 iSpiciness: $i > $o)). % 1.15/1.32 tff(iFruitTopping_type, type, ( % 1.15/1.32 iFruitTopping: $i > $o)). % 1.15/1.32 tff(abstractDomain_type, type, ( % 1.15/1.32 abstractDomain: $i > $o)). % 1.15/1.32 tff(iPrawnsTopping_type, type, ( % 1.15/1.32 iPrawnsTopping: $i > $o)). % 1.15/1.32 tff(iSpicyPizza_type, type, ( % 1.15/1.32 iSpicyPizza: $i > $o)). % 1.15/1.32 tff(iLaReine_type, type, ( % 1.15/1.32 iLaReine: $i > $o)). % 1.15/1.32 tff(iOnionTopping_type, type, ( % 1.15/1.32 iOnionTopping: $i > $o)). % 1.15/1.32 tff(iGiardiniera_type, type, ( % 1.15/1.32 iGiardiniera: $i > $o)). % 1.15/1.32 tff(iFourCheesesTopping_type, type, ( % 1.15/1.32 iFourCheesesTopping: $i > $o)). % 1.15/1.32 tff(iMozzarellaTopping_type, type, ( % 1.15/1.32 iMozzarellaTopping: $i > $o)). % 1.15/1.32 tff(iHerbSpiceTopping_type, type, ( % 1.15/1.32 iHerbSpiceTopping: $i > $o)). % 1.15/1.32 tff(iHotSpicedBeefTopping_type, type, ( % 1.15/1.32 iHotSpicedBeefTopping: $i > $o)). % 1.15/1.32 tff(iValuePartition_type, type, ( % 1.15/1.32 iValuePartition: $i > $o)). % 1.15/1.32 tff(ihasBase_type, type, ( % 1.15/1.32 ihasBase: ( $i * $i ) > $o)). % 1.15/1.32 tff(iNutTopping_type, type, ( % 1.15/1.32 iNutTopping: $i > $o)). % 1.15/1.32 tff(iIceCream_type, type, ( % 1.15/1.32 iIceCream: $i > $o)). % 1.15/1.32 tff(iNapoletana_type, type, ( % 1.15/1.32 iNapoletana: $i > $o)). % 1.15/1.32 tff(iAsparagusTopping_type, type, ( % 1.15/1.32 iAsparagusTopping: $i > $o)). % 1.15/1.32 tff(iVegetarianPizzaEquivalent2_type, type, ( % 1.15/1.32 iVegetarianPizzaEquivalent2: $i > $o)). % 1.15/1.32 tff(iFruttiDiMare_type, type, ( % 1.15/1.32 iFruttiDiMare: $i > $o)). % 1.15/1.32 tff(iPrinceCarlo_type, type, ( % 1.15/1.32 iPrinceCarlo: $i > $o)). % 1.15/1.32 tff(iInterestingPizza_type, type, ( % 1.15/1.32 iInterestingPizza: $i > $o)). % 1.15/1.32 tff(iParmense_type, type, ( % 1.15/1.32 iParmense: $i > $o)). % 1.15/1.32 tff(iGorgonzolaTopping_type, type, ( % 1.15/1.32 iGorgonzolaTopping: $i > $o)). % 1.15/1.32 tff(iGarlicTopping_type, type, ( % 1.15/1.32 iGarlicTopping: $i > $o)). % 1.15/1.32 tff(iVeneziana_type, type, ( % 1.15/1.32 iVeneziana: $i > $o)). % 1.15/1.32 tff(xsd_integer_type, type, ( % 1.15/1.32 xsd_integer: $i > $o)). % 1.15/1.32 tff(iPepperTopping_type, type, ( % 1.15/1.32 iPepperTopping: $i > $o)). % 1.15/1.32 tff(iFourSeasons_type, type, ( % 1.15/1.32 iFourSeasons: $i > $o)). % 1.15/1.32 tff(iowlThing_type, type, ( % 1.15/1.32 iowlThing: $i > $o)). % 1.15/1.32 tff(iCajun_type, type, ( % 1.15/1.32 iCajun: $i > $o)). % 1.15/1.32 tff(iCheeseTopping_type, type, ( % 1.15/1.32 iCheeseTopping: $i > $o)). % 1.15/1.32 tff(iMixedSeafoodTopping_type, type, ( % 1.15/1.32 iMixedSeafoodTopping: $i > $o)). % 1.15/1.32 tff(iThinAndCrispyBase_type, type, ( % 1.15/1.32 iThinAndCrispyBase: $i > $o)). % 1.15/1.32 tff(iMeatTopping_type, type, ( % 1.15/1.32 iMeatTopping: $i > $o)). % 1.15/1.32 tff(iOliveTopping_type, type, ( % 1.15/1.32 iOliveTopping: $i > $o)). % 1.15/1.32 tff(iPolloAdAstra_type, type, ( % 1.15/1.32 iPolloAdAstra: $i > $o)). % 1.15/1.32 tff(iPetitPoisTopping_type, type, ( % 1.15/1.32 iPetitPoisTopping: $i > $o)). % 1.15/1.32 tff(iPizzaBase_type, type, ( % 1.15/1.32 iPizzaBase: $i > $o)). % 1.15/1.32 tff(iPeperonataTopping_type, type, ( % 1.15/1.32 iPeperonataTopping: $i > $o)). % 1.15/1.32 tff(iCheeseyPizza_type, type, ( % 1.15/1.32 iCheeseyPizza: $i > $o)). % 1.15/1.32 tff(iJalapenoPepperTopping_type, type, ( % 1.15/1.32 iJalapenoPepperTopping: $i > $o)). % 1.15/1.32 tff(iNonVegetarianPizza_type, type, ( % 1.15/1.32 iNonVegetarianPizza: $i > $o)). % 1.15/1.32 tff(iMargherita_type, type, ( % 1.15/1.32 iMargherita: $i > $o)). % 1.15/1.32 tff(iSultanaTopping_type, type, ( % 1.15/1.32 iSultanaTopping: $i > $o)). % 1.15/1.32 tff(iRedOnionTopping_type, type, ( % 1.15/1.32 iRedOnionTopping: $i > $o)). % 1.15/1.32 tff(iRealItalianPizza_type, type, ( % 1.15/1.32 iRealItalianPizza: $i > $o)). % 1.15/1.32 tff(iGoatsCheeseTopping_type, type, ( % 1.15/1.32 iGoatsCheeseTopping: $i > $o)). % 1.15/1.32 tff(iFood_type, type, ( % 1.15/1.32 iFood: $i > $o)). % 1.15/1.32 tff(iMushroom_type, type, ( % 1.15/1.32 iMushroom: $i > $o)). % 1.15/1.32 tff(iSpinachTopping_type, type, ( % 1.15/1.32 iSpinachTopping: $i > $o)). % 1.15/1.32 tff(iHot_type, type, ( % 1.15/1.32 iHot: $i > $o)). % 1.15/1.32 tff(iSiciliana_type, type, ( % 1.15/1.32 iSiciliana: $i > $o)). % 1.15/1.32 tff(iPizzaTopping_type, type, ( % 1.15/1.32 iPizzaTopping: $i > $o)). % 1.15/1.32 tff(iHamTopping_type, type, ( % 1.15/1.32 iHamTopping: $i > $o)). % 1.15/1.32 tff(iVegetarianTopping_type, type, ( % 1.15/1.32 iVegetarianTopping: $i > $o)). % 1.15/1.32 tff(iMushroomTopping_type, type, ( % 1.15/1.32 iMushroomTopping: $i > $o)). % 1.15/1.32 tff(iSundriedTomatoTopping_type, type, ( % 1.15/1.32 iSundriedTomatoTopping: $i > $o)). % 1.15/1.32 tff(iCheeseyVegetableTopping_type, type, ( % 1.15/1.32 iCheeseyVegetableTopping: $i > $o)). % 1.15/1.32 tff(iSoho_type, type, ( % 1.15/1.32 iSoho: $i > $o)). % 1.15/1.32 tff(iowlNothing_type, type, ( % 1.15/1.32 iowlNothing: $i > $o)). % 1.15/1.32 tff(iMedium_type, type, ( % 1.15/1.32 iMedium: $i > $o)). % 1.15/1.32 tff(iVegetarianPizzaEquivalent1_type, type, ( % 1.15/1.32 iVegetarianPizzaEquivalent1: $i > $o)). % 1.15/1.32 tff(iSweetPepperTopping_type, type, ( % 1.15/1.32 iSweetPepperTopping: $i > $o)). % 1.15/1.32 tff(iAmerican_type, type, ( % 1.15/1.32 iAmerican: $i > $o)). % 1.15/1.32 tff(iThinAndCrispyPizza_type, type, ( % 1.15/1.32 iThinAndCrispyPizza: $i > $o)). % 1.15/1.32 tff(iSlicedTomatoTopping_type, type, ( % 1.15/1.32 iSlicedTomatoTopping: $i > $o)). % 1.15/1.32 tff(iPeperoniSausageTopping_type, type, ( % 1.15/1.32 iPeperoniSausageTopping: $i > $o)). % 1.15/1.32 tff(iParmesanTopping_type, type, ( % 1.15/1.32 iParmesanTopping: $i > $o)). % 1.15/1.32 tff(iSauceTopping_type, type, ( % 1.15/1.32 iSauceTopping: $i > $o)). % 1.15/1.32 tff(iPizza_type, type, ( % 1.15/1.32 iPizza: $i > $o)). % 1.15/1.32 tff(iVegetableTopping_type, type, ( % 1.15/1.32 iVegetableTopping: $i > $o)). % 1.15/1.32 tff(iSpicyTopping_type, type, ( % 1.15/1.32 iSpicyTopping: $i > $o)). % 1.15/1.32 tff(iLeekTopping_type, type, ( % 1.15/1.32 iLeekTopping: $i > $o)). % 1.15/1.32 tff(iisBaseOf_type, type, ( % 1.15/1.32 iisBaseOf: ( $i * $i ) > $o)). % 1.15/1.32 tff(iFishTopping_type, type, ( % 1.15/1.32 iFishTopping: $i > $o)). % 1.15/1.32 tff(iUnclosedPizza_type, type, ( % 1.15/1.32 iUnclosedPizza: $i > $o)). % 1.15/1.32 tff(iMeatyPizza_type, type, ( % 1.15/1.32 iMeatyPizza: $i > $o)). % 1.15/1.32 tff(iCajunSpiceTopping_type, type, ( % 1.15/1.32 iCajunSpiceTopping: $i > $o)). % 1.15/1.32 tff(iQuattroFormaggi_type, type, ( % 1.15/1.32 iQuattroFormaggi: $i > $o)). % 1.15/1.32 tff(iAmericanHot_type, type, ( % 1.15/1.32 iAmericanHot: $i > $o)). % 1.15/1.32 tff(iHotGreenPepperTopping_type, type, ( % 1.15/1.32 iHotGreenPepperTopping: $i > $o)). % 1.15/1.32 tff(iFiorentina_type, type, ( % 1.15/1.32 iFiorentina: $i > $o)). % 1.15/1.32 tff(ihasTopping_type, type, ( % 1.15/1.32 ihasTopping: ( $i * $i ) > $o)). % 1.15/1.32 tff(iGreenPepperTopping_type, type, ( % 1.15/1.32 iGreenPepperTopping: $i > $o)). % 1.15/1.32 tff(iCaprina_type, type, ( % 1.15/1.32 iCaprina: $i > $o)). % 1.15/1.32 tff(ihasIngredient_type, type, ( % 1.15/1.32 ihasIngredient: ( $i * $i ) > $o)). % 1.15/1.32 tff(iCaperTopping_type, type, ( % 1.15/1.32 iCaperTopping: $i > $o)). % 1.15/1.32 tff(iParmaHamTopping_type, type, ( % 1.15/1.32 iParmaHamTopping: $i > $o)). % 1.15/1.32 tff(iVegetarianPizza_type, type, ( % 1.15/1.32 iVegetarianPizza: $i > $o)). % 1.15/1.32 tff(xsd_string_type, type, ( % 1.15/1.32 xsd_string: $i > $o)). % 1.15/1.32 tff(iAnchoviesTopping_type, type, ( % 1.15/1.32 iAnchoviesTopping: $i > $o)). % 1.15/1.32 tff(formula1, axiom, % 1.15/1.32 iEngland = $i!val!3). % 1.15/1.32 tff(formula2, axiom, % 1.15/1.32 iAmerica = $i!val!2). % 1.15/1.32 tff(formula3, axiom, % 1.15/1.32 iFrance = $i!val!4). % 1.15/1.32 tff(formula4, axiom, % 1.15/1.32 iItaly = $i!val!6). % 1.15/1.32 tff(formula5, axiom, % 1.15/1.32 iGermany = $i!val!5). % 1.15/1.32 tff(formula6, axiom, % 1.15/1.32 k!1968($i!val!13) = $i!val!13). % 1.15/1.32 tff(formula7, axiom, % 1.15/1.32 k!1968($i!val!16) = $i!val!16). % 1.15/1.32 tff(formula8, axiom, % 1.15/1.32 k!1968($i!val!9) = $i!val!9). % 1.15/1.32 tff(formula9, axiom, % 1.15/1.32 k!1968($i!val!3) = $i!val!3). % 1.15/1.32 tff(formula10, axiom, % 1.15/1.32 k!1968($i!val!2) = $i!val!2). % 1.15/1.32 tff(formula11, axiom, % 1.15/1.32 k!1968($i!val!4) = $i!val!4). % 1.15/1.32 tff(formula12, axiom, % 1.15/1.32 k!1968($i!val!15) = $i!val!15). % 1.15/1.32 tff(formula13, axiom, % 1.15/1.32 k!1968($i!val!7) = $i!val!7). % 1.15/1.32 tff(formula14, axiom, % 1.15/1.32 k!1968($i!val!11) = $i!val!11). % 1.15/1.32 tff(formula15, axiom, % 1.15/1.32 k!1968($i!val!19) = $i!val!19). % 1.15/1.32 tff(formula16, axiom, % 1.15/1.32 k!1968($i!val!6) = $i!val!6). % 1.15/1.32 tff(formula17, axiom, % 1.15/1.32 k!1968($i!val!10) = $i!val!10). % 1.15/1.32 tff(formula18, axiom, % 1.15/1.32 k!1968($i!val!14) = $i!val!14). % 1.15/1.32 tff(formula19, axiom, % 1.15/1.32 k!1968($i!val!5) = $i!val!5). % 1.15/1.32 tff(formula20, axiom, % 1.15/1.32 k!1968($i!val!17) = $i!val!17). % 1.15/1.32 tff(formula21, axiom, % 1.15/1.32 k!1968($i!val!18) = $i!val!18). % 1.15/1.32 tff(formula22, axiom, % 1.15/1.32 k!1968($i!val!12) = $i!val!12). % 1.15/1.32 tff(formula23, axiom, % 1.15/1.32 k!1968($i!val!1) = $i!val!1). % 1.15/1.32 tff(formula24, axiom, % 1.15/1.32 k!1968($i!val!8) = $i!val!8). % 1.15/1.32 tff(formula25, axiom, % 1.15/1.32 ![X0: $i] : ((~((($i!val!13 = X0)) | (($i!val!16 = X0)) | (($i!val!9 = X0)) | (($i!val!3 = X0)) | (($i!val!2 = X0)) | (($i!val!4 = X0)) | (($i!val!15 = X0)) | (($i!val!7 = X0)) | (($i!val!11 = X0)) | (($i!val!19 = X0)) | (($i!val!6 = X0)) | (($i!val!10 = X0)) | (($i!val!14 = X0)) | (($i!val!5 = X0)) | (($i!val!17 = X0)) | (($i!val!18 = X0)) | (($i!val!12 = X0)) | (($i!val!1 = X0)) | (($i!val!8 = X0)))) => (k!1968(X0) = $i!val!0))). % 1.15/1.32 tff(formula26, axiom, % 1.15/1.32 ![X0: $i] : (iCountry(X0) <=> ((k!1968(X0) = $i!val!5) | (k!1968(X0) = $i!val!3) | (k!1968(X0) = $i!val!2) | (k!1968(X0) = $i!val!4) | (k!1968(X0) = $i!val!6)))). % 1.15/1.32 tff(formula27, axiom, % 1.15/1.32 ![X0: $i] : (iNamedPizza(X0) <=> $false)). % 1.15/1.32 tff(formula28, axiom, % 1.15/1.32 ![X0: $i] : (iArtichokeTopping(X0) <=> $false)). % 1.15/1.32 tff(formula29, axiom, % 1.15/1.32 ![X0: $i] : (iSpicyPizzaEquivalent(X0) <=> $false)). % 1.15/1.32 tff(formula30, axiom, % 1.15/1.32 ![X0: $i] : (dataDomain(X0) <=> (k!1968(X0) = $i!val!1))). % 1.15/1.32 tff(formula31, axiom, % 1.15/1.32 ![X0: $i] : (iTobascoPepperSauce(X0) <=> $false)). % 1.15/1.32 tff(formula32, axiom, % 1.15/1.32 ![X0: $i] : (iSloppyGiuseppe(X0) <=> $false)). % 1.15/1.32 tff(formula33, axiom, % 1.15/1.32 ![X0: $i] : (iMild(X0) <=> ((k!1968(X0) = $i!val!14) | (k!1968(X0) = $i!val!18)))). % 1.15/1.32 tff(formula34, axiom, % 1.15/1.32 ![X0: $i] : (iDeepPanBase(X0) <=> $false)). % 1.15/1.32 tff(formula35, axiom, % 1.15/1.32 ![X0: $i] : (iPineKernels(X0) <=> $false)). % 1.15/1.32 tff(formula36, axiom, % 1.15/1.32 ![X0: $i] : (iDomainConcept(X0) <=> ((~(k!1968(X0) = $i!val!18)) & (~(k!1968(X0) = $i!val!14)) & (~(k!1968(X0) = $i!val!1))))). % 1.15/1.32 tff(formula37, axiom, % 1.15/1.32 ![X0: $i] : (iCapricciosa(X0) <=> $false)). % 1.15/1.32 tff(formula38, axiom, % 1.15/1.32 ![X0: $i] : (iChickenTopping(X0) <=> $false)). % 1.15/1.32 tff(formula39, axiom, % 1.15/1.32 ![X0: $i, X1: $i] : (iisIngredientOf(X0, X1) <=> (((k!1968(X1) = $i!val!8) & (k!1968(X0) = $i!val!4)) | ((k!1968(X1) = $i!val!16) & (k!1968(X0) = $i!val!4)) | ((k!1968(X1) = $i!val!15) & (k!1968(X0) = $i!val!4)) | ((k!1968(X1) = $i!val!17) & (k!1968(X0) = $i!val!4)) | ((k!1968(X1) = $i!val!7) & (k!1968(X0) = $i!val!4)) | ((k!1968(X1) = $i!val!10) & (k!1968(X0) = $i!val!4)) | ((k!1968(X1) = $i!val!12) & (k!1968(X0) = $i!val!4))))). % 1.15/1.32 tff(formula40, axiom, % 1.15/1.32 ![X0: $i] : (iRocketTopping(X0) <=> $false)). % 1.15/1.32 tff(formula41, axiom, % 1.15/1.32 ![X0: $i] : (iTomatoTopping(X0) <=> $false)). % 1.15/1.32 tff(formula42, axiom, % 1.15/1.32 ![X0: $i, X1: $i] : (ihasCountryOfOrigin(X0, X1) <=> $false)). % 1.15/1.32 tff(formula43, axiom, % 1.15/1.32 ![X0: $i] : (iRosemaryTopping(X0) <=> $false)). % 1.15/1.32 tff(formula44, axiom, % 1.15/1.32 ![X0: $i] : (iRosa(X0) <=> $false)). % 1.15/1.32 tff(formula45, axiom, % 1.15/1.32 ![X0: $i, X1: $i] : (iisToppingOf(X0, X1) <=> (((k!1968(X1) = $i!val!8) & (k!1968(X0) = $i!val!4)) | ((k!1968(X1) = $i!val!16) & (k!1968(X0) = $i!val!4)) | ((k!1968(X1) = $i!val!15) & (k!1968(X0) = $i!val!4)) | ((k!1968(X1) = $i!val!17) & (k!1968(X0) = $i!val!4)) | ((k!1968(X1) = $i!val!7) & (k!1968(X0) = $i!val!4)) | ((k!1968(X1) = $i!val!10) & (k!1968(X0) = $i!val!4))))). % 1.15/1.32 tff(formula46, axiom, % 1.15/1.32 ![X0: $i, X1: $i] : (ihasSpiciness(X0, X1) <=> (((k!1968(X1) = $i!val!10) & (k!1968(X0) = $i!val!14)) | ((k!1968(X1) = $i!val!15) & (k!1968(X0) = $i!val!18))))). % 1.15/1.32 tff(formula47, axiom, % 1.15/1.32 ![X0: $i] : (iSpiciness(X0) <=> ((k!1968(X0) = $i!val!14) | (k!1968(X0) = $i!val!18)))). % 1.15/1.32 tff(formula48, axiom, % 1.15/1.32 ![X0: $i] : (iFruitTopping(X0) <=> $false)). % 1.15/1.32 tff(formula49, axiom, % 1.15/1.32 ![X0: $i] : (abstractDomain(X0) <=> (~(k!1968(X0) = $i!val!1)))). % 1.15/1.32 tff(formula50, axiom, % 1.15/1.32 ![X0: $i] : (iPrawnsTopping(X0) <=> $false)). % 1.15/1.32 tff(formula51, axiom, % 1.15/1.32 ![X0: $i] : (iSpicyPizza(X0) <=> $false)). % 1.15/1.32 tff(formula52, axiom, % 1.15/1.32 ![X0: $i] : (iLaReine(X0) <=> $false)). % 1.15/1.32 tff(formula53, axiom, % 1.15/1.32 ![X0: $i] : (iOnionTopping(X0) <=> $false)). % 1.15/1.32 tff(formula54, axiom, % 1.15/1.32 ![X0: $i] : (iGiardiniera(X0) <=> $false)). % 1.15/1.32 tff(formula55, axiom, % 1.15/1.32 ![X0: $i] : (iFourCheesesTopping(X0) <=> $false)). % 1.15/1.32 tff(formula56, axiom, % 1.15/1.32 ![X0: $i] : (iMozzarellaTopping(X0) <=> $false)). % 1.15/1.32 tff(formula57, axiom, % 1.15/1.32 ![X0: $i] : (iHerbSpiceTopping(X0) <=> $false)). % 1.15/1.32 tff(formula58, axiom, % 1.15/1.32 ![X0: $i] : (iHotSpicedBeefTopping(X0) <=> $false)). % 1.15/1.32 tff(formula59, axiom, % 1.15/1.32 ![X0: $i] : (iValuePartition(X0) <=> ((k!1968(X0) = $i!val!14) | (k!1968(X0) = $i!val!18)))). % 1.15/1.32 tff(formula60, axiom, % 1.15/1.32 ![X0: $i, X1: $i] : (ihasBase(X0, X1) <=> ((k!1968(X1) = $i!val!4) & (k!1968(X0) = $i!val!12)))). % 1.15/1.32 tff(formula61, axiom, % 1.15/1.32 ![X0: $i] : (iNutTopping(X0) <=> (k!1968(X0) = $i!val!15))). % 1.15/1.32 tff(formula62, axiom, % 1.15/1.32 ![X0: $i] : (iIceCream(X0) <=> $false)). % 1.15/1.32 tff(formula63, axiom, % 1.15/1.32 ![X0: $i] : (iNapoletana(X0) <=> $false)). % 1.15/1.32 tff(formula64, axiom, % 1.15/1.32 ![X0: $i] : (iAsparagusTopping(X0) <=> $false)). % 1.15/1.32 tff(formula65, axiom, % 1.15/1.32 ![X0: $i] : (iVegetarianPizzaEquivalent2(X0) <=> $false)). % 1.15/1.32 tff(formula66, axiom, % 1.15/1.32 ![X0: $i] : (iFruttiDiMare(X0) <=> $false)). % 1.15/1.32 tff(formula67, axiom, % 1.15/1.32 ![X0: $i] : (iPrinceCarlo(X0) <=> $false)). % 1.15/1.32 tff(formula68, axiom, % 1.15/1.32 ![X0: $i] : (iInterestingPizza(X0) <=> (k!1968(X0) = $i!val!4))). % 1.15/1.32 tff(formula69, axiom, % 1.15/1.32 ![X0: $i] : (iParmense(X0) <=> $false)). % 1.15/1.32 tff(formula70, axiom, % 1.15/1.32 ![X0: $i] : (iGorgonzolaTopping(X0) <=> $false)). % 1.15/1.32 tff(formula71, axiom, % 1.15/1.32 ![X0: $i] : (iGarlicTopping(X0) <=> $false)). % 1.15/1.32 tff(formula72, axiom, % 1.15/1.32 ![X0: $i] : (iVeneziana(X0) <=> $false)). % 1.15/1.32 tff(formula73, axiom, % 1.15/1.32 ![X0: $i] : (xsd_integer(X0) <=> $false)). % 1.15/1.32 tff(formula74, axiom, % 1.15/1.32 ![X0: $i] : (iPepperTopping(X0) <=> $false)). % 1.15/1.32 tff(formula75, axiom, % 1.15/1.32 ![X0: $i] : (iFourSeasons(X0) <=> $false)). % 1.15/1.32 tff(formula76, axiom, % 1.15/1.32 ![X0: $i] : (iowlThing(X0) <=> (~(k!1968(X0) = $i!val!1)))). % 1.15/1.32 tff(formula77, axiom, % 1.15/1.32 ![X0: $i] : (iCajun(X0) <=> $false)). % 1.15/1.32 tff(formula78, axiom, % 1.15/1.32 ![X0: $i] : (iCheeseTopping(X0) <=> $false)). % 1.15/1.32 tff(formula79, axiom, % 1.15/1.32 ![X0: $i] : (iMixedSeafoodTopping(X0) <=> $false)). % 1.15/1.32 tff(formula80, axiom, % 1.15/1.32 ![X0: $i] : (iThinAndCrispyBase(X0) <=> (k!1968(X0) = $i!val!12))). % 1.15/1.32 tff(formula81, axiom, % 1.15/1.32 ![X0: $i] : (iMeatTopping(X0) <=> $false)). % 1.15/1.32 tff(formula82, axiom, % 1.15/1.32 ![X0: $i] : (iOliveTopping(X0) <=> $false)). % 1.15/1.32 tff(formula83, axiom, % 1.15/1.32 ![X0: $i] : (iPolloAdAstra(X0) <=> $false)). % 1.15/1.32 tff(formula84, axiom, % 1.15/1.32 ![X0: $i] : (iPetitPoisTopping(X0) <=> $false)). % 1.15/1.32 tff(formula85, axiom, % 1.15/1.32 ![X0: $i] : (iPizzaBase(X0) <=> (k!1968(X0) = $i!val!12))). % 1.15/1.32 tff(formula86, axiom, % 1.15/1.32 ![X0: $i] : (iPeperonataTopping(X0) <=> $false)). % 1.15/1.32 tff(formula87, axiom, % 1.15/1.32 ![X0: $i] : (iCheeseyPizza(X0) <=> $false)). % 1.15/1.32 tff(formula88, axiom, % 1.15/1.32 ![X0: $i] : (iJalapenoPepperTopping(X0) <=> $false)). % 1.15/1.32 tff(formula89, axiom, % 1.15/1.32 ![X0: $i] : (iNonVegetarianPizza(X0) <=> (k!1968(X0) = $i!val!4))). % 1.15/1.32 tff(formula90, axiom, % 1.15/1.32 ![X0: $i] : (iMargherita(X0) <=> $false)). % 1.15/1.32 tff(formula91, axiom, % 1.15/1.32 ![X0: $i] : (iSultanaTopping(X0) <=> $false)). % 1.15/1.32 tff(formula92, axiom, % 1.15/1.32 ![X0: $i] : (iRedOnionTopping(X0) <=> $false)). % 1.15/1.32 tff(formula93, axiom, % 1.15/1.32 ![X0: $i] : (iRealItalianPizza(X0) <=> $false)). % 1.15/1.32 tff(formula94, axiom, % 1.15/1.32 ![X0: $i] : (iGoatsCheeseTopping(X0) <=> $false)). % 1.15/1.32 tff(formula95, axiom, % 1.15/1.32 ![X0: $i] : (iFood(X0) <=> ((~(k!1968(X0) = $i!val!18)) & (~(k!1968(X0) = $i!val!14)) & (~(k!1968(X0) = $i!val!1))))). % 1.15/1.32 tff(formula96, axiom, % 1.15/1.32 ![X0: $i] : (iMushroom(X0) <=> $false)). % 1.15/1.32 tff(formula97, axiom, % 1.15/1.32 ![X0: $i] : (iSpinachTopping(X0) <=> $false)). % 1.15/1.32 tff(formula98, axiom, % 1.15/1.32 ![X0: $i] : (iHot(X0) <=> $false)). % 1.15/1.32 tff(formula99, axiom, % 1.15/1.32 ![X0: $i] : (iSiciliana(X0) <=> $false)). % 1.15/1.32 tff(formula100, axiom, % 1.15/1.32 ![X0: $i] : (iPizzaTopping(X0) <=> ((~(k!1968(X0) = $i!val!18)) & (~(k!1968(X0) = $i!val!14)) & (~(k!1968(X0) = $i!val!4)) & (~(k!1968(X0) = $i!val!12)) & (~(k!1968(X0) = $i!val!1))))). % 1.15/1.32 tff(formula101, axiom, % 1.15/1.32 ![X0: $i] : (iHamTopping(X0) <=> $false)). % 1.15/1.32 tff(formula102, axiom, % 1.15/1.32 ![X0: $i] : (iVegetarianTopping(X0) <=> (k!1968(X0) = $i!val!15))). % 1.15/1.32 tff(formula103, axiom, % 1.15/1.32 ![X0: $i] : (iMushroomTopping(X0) <=> $false)). % 1.15/1.32 tff(formula104, axiom, % 1.15/1.32 ![X0: $i] : (iSundriedTomatoTopping(X0) <=> $false)). % 1.15/1.32 tff(formula105, axiom, % 1.15/1.32 ![X0: $i] : (iCheeseyVegetableTopping(X0) <=> $false)). % 1.15/1.32 tff(formula106, axiom, % 1.15/1.32 ![X0: $i] : (iSoho(X0) <=> $false)). % 1.15/1.32 tff(formula107, axiom, % 1.15/1.32 ![X0: $i] : (iowlNothing(X0) <=> $false)). % 1.15/1.32 tff(formula108, axiom, % 1.15/1.32 ![X0: $i] : (iMedium(X0) <=> $false)). % 1.15/1.32 tff(formula109, axiom, % 1.15/1.32 ![X0: $i] : (iVegetarianPizzaEquivalent1(X0) <=> $false)). % 1.15/1.32 tff(formula110, axiom, % 1.15/1.32 ![X0: $i] : (iSweetPepperTopping(X0) <=> $false)). % 1.15/1.32 tff(formula111, axiom, % 1.15/1.32 ![X0: $i] : (iAmerican(X0) <=> $false)). % 1.15/1.32 tff(formula112, axiom, % 1.15/1.32 ![X0: $i] : (iThinAndCrispyPizza(X0) <=> (k!1968(X0) = $i!val!4))). % 1.15/1.32 tff(formula113, axiom, % 1.15/1.32 ![X0: $i] : (iSlicedTomatoTopping(X0) <=> $false)). % 1.15/1.32 tff(formula114, axiom, % 1.15/1.32 ![X0: $i] : (iPeperoniSausageTopping(X0) <=> $false)). % 1.15/1.32 tff(formula115, axiom, % 1.15/1.32 ![X0: $i] : (iParmesanTopping(X0) <=> $false)). % 1.15/1.32 tff(formula116, axiom, % 1.15/1.32 ![X0: $i] : (iSauceTopping(X0) <=> $false)). % 1.15/1.32 tff(formula117, axiom, % 1.15/1.32 ![X0: $i] : (iPizza(X0) <=> (k!1968(X0) = $i!val!4))). % 1.15/1.32 tff(formula118, axiom, % 1.15/1.32 ![X0: $i] : (iVegetableTopping(X0) <=> $false)). % 1.15/1.32 tff(formula119, axiom, % 1.15/1.32 ![X0: $i] : (iSpicyTopping(X0) <=> $false)). % 1.15/1.32 tff(formula120, axiom, % 1.15/1.32 ![X0: $i] : (iLeekTopping(X0) <=> $false)). % 1.15/1.32 tff(formula121, axiom, % 1.15/1.32 ![X0: $i, X1: $i] : (iisBaseOf(X0, X1) <=> ((k!1968(X1) = $i!val!12) & (k!1968(X0) = $i!val!4)))). % 1.15/1.32 tff(formula122, axiom, % 1.15/1.32 ![X0: $i] : (iFishTopping(X0) <=> (k!1968(X0) = $i!val!10))). % 1.15/1.32 tff(formula123, axiom, % 1.15/1.32 ![X0: $i] : (iUnclosedPizza(X0) <=> $false)). % 1.15/1.32 tff(formula124, axiom, % 1.15/1.32 ![X0: $i] : (iMeatyPizza(X0) <=> $false)). % 1.15/1.32 tff(formula125, axiom, % 1.15/1.32 ![X0: $i] : (iCajunSpiceTopping(X0) <=> $false)). % 1.15/1.32 tff(formula126, axiom, % 1.15/1.32 ![X0: $i] : (iQuattroFormaggi(X0) <=> $false)). % 1.15/1.32 tff(formula127, axiom, % 1.15/1.32 ![X0: $i] : (iAmericanHot(X0) <=> $false)). % 1.15/1.32 tff(formula128, axiom, % 1.15/1.32 ![X0: $i] : (iHotGreenPepperTopping(X0) <=> $false)). % 1.15/1.32 tff(formula129, axiom, % 1.15/1.32 ![X0: $i] : (iFiorentina(X0) <=> $false)). % 1.15/1.32 tff(formula130, axiom, % 1.15/1.32 ![X0: $i, X1: $i] : (ihasTopping(X0, X1) <=> (((k!1968(X1) = $i!val!4) & (k!1968(X0) = $i!val!17)) | ((k!1968(X1) = $i!val!4) & (k!1968(X0) = $i!val!10)) | ((k!1968(X1) = $i!val!4) & (k!1968(X0) = $i!val!8)) | ((k!1968(X1) = $i!val!4) & (k!1968(X0) = $i!val!15)) | ((k!1968(X1) = $i!val!4) & (k!1968(X0) = $i!val!7)) | ((k!1968(X1) = $i!val!4) & (k!1968(X0) = $i!val!16))))). % 1.15/1.32 tff(formula131, axiom, % 1.15/1.32 ![X0: $i] : (iGreenPepperTopping(X0) <=> $false)). % 1.15/1.32 tff(formula132, axiom, % 1.15/1.32 ![X0: $i] : (iCaprina(X0) <=> $false)). % 1.15/1.32 tff(formula133, axiom, % 1.15/1.32 ![X0: $i, X1: $i] : (ihasIngredient(X0, X1) <=> (((k!1968(X1) = $i!val!4) & (k!1968(X0) = $i!val!17)) | ((k!1968(X1) = $i!val!4) & (k!1968(X0) = $i!val!12)) | ((k!1968(X1) = $i!val!4) & (k!1968(X0) = $i!val!10)) | ((k!1968(X1) = $i!val!4) & (k!1968(X0) = $i!val!8)) | ((k!1968(X1) = $i!val!4) & (k!1968(X0) = $i!val!15)) | ((k!1968(X1) = $i!val!4) & (k!1968(X0) = $i!val!7)) | ((k!1968(X1) = $i!val!4) & (k!1968(X0) = $i!val!16))))). % 1.15/1.33 tff(formula134, axiom, % 1.15/1.33 ![X0: $i] : (iCaperTopping(X0) <=> $false)). % 1.15/1.33 tff(formula135, axiom, % 1.15/1.33 ![X0: $i] : (iParmaHamTopping(X0) <=> $false)). % 1.15/1.33 tff(formula136, axiom, % 1.15/1.33 ![X0: $i] : (iVegetarianPizza(X0) <=> $false)). % 1.15/1.33 tff(formula137, axiom, % 1.15/1.33 ![X0: $i] : (xsd_string(X0) <=> $false)). % 1.15/1.33 tff(formula138, axiom, % 1.15/1.33 ![X0: $i] : (iAnchoviesTopping(X0) <=> $false)). % 1.15/1.33 % SZS output end Model % 1.15/1.34 % E exiting %------------------------------------------------------------------------------