%------------------------------------------------------------------------------ % File : Nitpick---2016 % Problem : SWB036+1 : TPTP v6.4.0. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : isabelle tptp_nitpick %d %s % Computer : n042.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32218.75MB % OS : Linux 3.10.0-327.36.3.el7.x86_64 % CPULimit : 300s % DateTime : Wed Jan 18 15:08:57 EST 2017 % Result : Satisfiable 38.35s % Output : FiniteModel 38.35s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWB036+1 : TPTP v6.4.0. Released v5.2.0. % 0.00/0.04 % Command : isabelle tptp_nitpick %d %s % 0.03/0.23 % Computer : n042.star.cs.uiowa.edu % 0.03/0.23 % Model : x86_64 x86_64 % 0.03/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.03/0.23 % Memory : 32218.75MB % 0.03/0.23 % OS : Linux 3.10.0-327.36.3.el7.x86_64 % 0.03/0.23 % CPULimit : 300 % 0.03/0.23 % DateTime : Sun Jan 15 06:28:03 CST 2017 % 0.03/0.23 % CPUTime : % 38.35/19.72 Nitpicking formula... % 38.35/19.72 Timestamp: 06:28:13 % 38.35/19.72 Using SAT solver "Lingeling_JNI" The following solvers are configured: % 38.35/19.72 "Lingeling_JNI", "CryptoMiniSat_JNI", "MiniSat_JNI", "SAT4J", "SAT4J_Light" % 38.35/19.72 Batch 1 of 20: Trying 5 scopes: % 38.35/19.72 card TPTP_Interpret.ind = 1 % 38.35/19.72 card TPTP_Interpret.ind = 2 % 38.35/19.72 card TPTP_Interpret.ind = 3 % 38.35/19.72 card TPTP_Interpret.ind = 4 % 38.35/19.72 card TPTP_Interpret.ind = 5 % 38.35/19.72 Batch 2 of 20: Trying 5 scopes: % 38.35/19.72 card TPTP_Interpret.ind = 6 % 38.35/19.72 card TPTP_Interpret.ind = 7 % 38.35/19.72 card TPTP_Interpret.ind = 8 % 38.35/19.72 card TPTP_Interpret.ind = 9 % 38.35/19.72 card TPTP_Interpret.ind = 10 % 38.35/19.72 % SZS status Satisfiable % SZS output start FiniteModel % 38.35/19.72 Nitpick found a model for card TPTP_Interpret.ind = 6: % 38.35/19.72 % 38.35/19.72 Constants: % 38.35/19.72 bnd_abstractDomain = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := False, % 38.35/19.72 i6 := True) % 38.35/19.72 bnd_dataDomain = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := True, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iAmerica = i2 % 38.35/19.72 bnd_iAmerican = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iAmericanHot = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iAnchoviesTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iArtichokeTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iAsparagusTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iCajun = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iCajunSpiceTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iCaperTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iCapricciosa = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iCaprina = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iCheeseTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iCheeseyPizza = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iCheeseyVegetableTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iChickenTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iCountry = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := False, % 38.35/19.72 i6 := True) % 38.35/19.72 bnd_iDeepPanBase = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iDomainConcept = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := False, % 38.35/19.72 i6 := True) % 38.35/19.72 bnd_iEngland = i6 % 38.35/19.72 bnd_iFiorentina = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iFishTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iFood = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := False, % 38.35/19.72 i6 := True) % 38.35/19.72 bnd_iFourCheesesTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iFourSeasons = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iFrance = i4 % 38.35/19.72 bnd_iFruitTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iFruttiDiMare = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iGarlicTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iGermany = i1 % 38.35/19.72 bnd_iGiardiniera = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iGoatsCheeseTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iGorgonzolaTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iGreenPepperTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iHamTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iHerbSpiceTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iHot = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iHotGreenPepperTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iHotSpicedBeefTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iIceCream = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iInterestingPizza = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iItaly = i3 % 38.35/19.72 bnd_iJalapenoPepperTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iLaReine = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iLeekTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iMargherita = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iMeatTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iMeatyPizza = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iMedium = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iMild = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iMixedSeafoodTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iMozzarellaTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iMushroom = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iMushroomTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iNamedPizza = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iNapoletana = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iNonVegetarianPizza = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iNutTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iOliveTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iOnionTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iParmaHamTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iParmense = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iParmesanTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iPeperonataTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iPeperoniSausageTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iPepperTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iPetitPoisTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iPineKernels = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iPizza = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iPizzaBase = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iPizzaTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := False, % 38.35/19.72 i6 := True) % 38.35/19.72 bnd_iPolloAdAstra = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iPrawnsTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iPrinceCarlo = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iQuattroFormaggi = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iRealItalianPizza = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iRedOnionTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iRocketTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iRosa = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iRosemaryTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iSauceTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iSiciliana = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iSlicedTomatoTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iSloppyGiuseppe = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iSoho = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iSpiciness = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iSpicyPizza = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iSpicyPizzaEquivalent = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iSpicyTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iSpinachTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iSultanaTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iSundriedTomatoTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iSweetPepperTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iThinAndCrispyBase = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iThinAndCrispyPizza = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iTobascoPepperSauce = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iTomatoTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iUnclosedPizza = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iValuePartition = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iVegetableTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iVegetarianPizza = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iVegetarianPizzaEquivalent1 = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iVegetarianPizzaEquivalent2 = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iVegetarianTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iVeneziana = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_ihasBase = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i2 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i3 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i4 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i5 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i6 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False)) % 38.35/19.72 bnd_ihasCountryOfOrigin = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := True, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i2 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := True, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i3 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := True, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i4 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := True, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i5 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i6 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := True, i4 := False, i5 := False, % 38.35/19.72 i6 := False)) % 38.35/19.72 bnd_ihasIngredient = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i2 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i3 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i4 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i5 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i6 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False)) % 38.35/19.72 bnd_ihasSpiciness = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i2 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i3 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i4 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i5 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i6 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False)) % 38.35/19.72 bnd_ihasTopping = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i2 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i3 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i4 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i5 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i6 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False)) % 38.35/19.72 bnd_iisBaseOf = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i2 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i3 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i4 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i5 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i6 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False)) % 38.35/19.72 bnd_iisIngredientOf = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i2 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i3 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i4 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i5 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i6 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False)) % 38.35/19.72 bnd_iisToppingOf = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i2 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i3 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i4 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i5 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False), % 38.35/19.72 i6 := (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False)) % 38.35/19.72 bnd_iowlNothing = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_iowlThing = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := True, i2 := True, i3 := True, i4 := True, i5 := False, % 38.35/19.72 i6 := True) % 38.35/19.72 bnd_xsd_integer = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := True, % 38.35/19.72 i6 := False) % 38.35/19.72 bnd_xsd_string = % 38.35/19.72 (\<lambda>x. _) % 38.35/19.72 (i1 := False, i2 := False, i3 := False, i4 := False, i5 := False, % 38.35/19.72 i6 := False) % 38.35/19.72 % SZS output end FiniteModel % 38.35/19.72 Total time: 9.6 s %------------------------------------------------------------------------------