%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWB036+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:00:17 PM UTC 2026
% Result : Satisfiable 5.77s 1.92s
% Output : Saturation 5.77s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u2577,axiom,
( ~ iFruitTopping(X0)
| ~ iMeatTopping(X0) ) ).
cnf(u2967,axiom,
iItaly != iEngland ).
cnf(u2429,axiom,
( ~ iThinAndCrispyBase(sK148(X0))
| ~ iPizza(X0)
| ~ abstractDomain(X0)
| iThinAndCrispyPizza(X0) ) ).
cnf(u2553,axiom,
iCountry(iEngland) ).
cnf(u2545,axiom,
( ~ iisToppingOf(X0,X1)
| abstractDomain(X0) ) ).
cnf(u2096,axiom,
( abstractDomain(X0)
| ~ iHot(X0) ) ).
cnf(u2156,axiom,
( abstractDomain(X0)
| ~ iMedium(X0) ) ).
cnf(u2456,axiom,
( ~ iVegetarianPizzaEquivalent1(X0)
| ~ ihasTopping(X0,X2)
| iVegetarianTopping(X2) ) ).
cnf(u2446,axiom,
( ~ iVegetarianPizza(X0)
| ~ iFishTopping(X4)
| ~ ihasTopping(X0,X4) ) ).
cnf(u2047,axiom,
( ~ iFruitTopping(X0)
| iPizzaTopping(X0) ) ).
cnf(u2115,axiom,
( ~ iInterestingPizza(X0)
| ihasTopping(X0,sK66(X0)) ) ).
cnf(u2398,axiom,
( ~ iSpicyPizzaEquivalent(X0)
| ihasTopping(X0,sK141(X0)) ) ).
cnf(u2960,axiom,
( ~ iisBaseOf(X0,X1)
| iisIngredientOf(X0,X1) ) ).
cnf(u2994,axiom,
~ iSpiciness(iEngland) ).
cnf(u1979,axiom,
( ~ iCheeseyPizza(X0)
| abstractDomain(X0) ) ).
cnf(u2661,axiom,
( ~ iSauceTopping(X0)
| ~ iMeatTopping(X0) ) ).
cnf(u3018,axiom,
abstractDomain(iGermany) ).
cnf(u2961,axiom,
( ihasIngredient(X0,X1)
| ~ ihasBase(X0,X1) ) ).
cnf(u2149,axiom,
( ~ iMeatTopping(X0)
| abstractDomain(X0) ) ).
cnf(u2542,axiom,
( ~ iisIngredientOf(X0,X1)
| ihasIngredient(X1,X0) ) ).
cnf(u2534,axiom,
( ~ iisBaseOf(X0,X1)
| iPizza(X1) ) ).
cnf(u2113,axiom,
( sK65(X0) != sK66(X0)
| ~ iInterestingPizza(X0) ) ).
cnf(u3030,axiom,
~ iHot(sK1) ).
cnf(u2475,axiom,
( ~ iFruitTopping(X0)
| iVegetarianTopping(X0)
| ~ iPizzaTopping(X0) ) ).
cnf(u2152,axiom,
( ~ iMeatyPizza(X0)
| iMeatTopping(sK77(X0)) ) ).
cnf(u2388,axiom,
( iValuePartition(X0)
| ~ iSpiciness(X0) ) ).
cnf(u2204,axiom,
( ~ iNutTopping(X0)
| iMild(sK88(X0)) ) ).
cnf(u1879,axiom,
( ~ dataDomain(X0)
| ~ abstractDomain(X0) ) ).
cnf(u2095,axiom,
( ~ iHerbSpiceTopping(X0)
| iPizzaTopping(X0) ) ).
cnf(u2504,axiom,
( ~ ihasBase(X2,X0)
| ~ ihasBase(X1,X0)
| X1 = X2 ) ).
cnf(u2706,axiom,
( ~ iHerbSpiceTopping(X0)
| ~ iFishTopping(X0) ) ).
cnf(u2979,axiom,
( ~ iPizza(X0)
| ~ abstractDomain(X0)
| iMeatTopping(sK152(X0))
| iVegetarianPizza(X0)
| ihasTopping(X0,sK153(X0)) ) ).
cnf(u2959,axiom,
( ~ iisToppingOf(X0,X1)
| iisIngredientOf(X0,X1) ) ).
cnf(u2046,axiom,
( ~ iFruitTopping(X0)
| abstractDomain(X0) ) ).
cnf(u2985,axiom,
( ~ ihasTopping(X0,X3)
| ~ ihasTopping(X0,X1)
| ~ ihasTopping(X0,X2)
| iInterestingPizza(X0)
| X1 = X2
| X1 = X3
| X2 = X3 ) ).
cnf(u2254,axiom,
( ~ iPizza(X0)
| iPizzaBase(sK101(X0)) ) ).
cnf(u2473,axiom,
( ~ iVegetarianTopping(X0)
| iPizzaTopping(X0) ) ).
cnf(u1978,axiom,
( ~ iCheeseTopping(X0)
| iPizzaTopping(X0) ) ).
cnf(u3009,axiom,
( ~ ihasBase(X1,X0)
| iFood(X0) ) ).
cnf(u2522,axiom,
( ~ ihasTopping(X0,X1)
| abstractDomain(X1) ) ).
cnf(u2465,axiom,
( ~ iPizza(X0)
| iVegetarianPizzaEquivalent2(X0)
| ~ abstractDomain(X0)
| ihasTopping(X0,sK155(X0)) ) ).
cnf(u2525,axiom,
( ~ ihasTopping(X0,X1)
| iPizza(X0) ) ).
cnf(u2997,axiom,
~ iSpiciness(iGermany) ).
cnf(u2530,axiom,
( ~ iisBaseOf(X0,X1)
| abstractDomain(X0) ) ).
cnf(u2533,axiom,
( ~ iisBaseOf(X0,X1)
| iPizzaBase(X0) ) ).
cnf(u2260,axiom,
( ~ iPizzaTopping(X0)
| iFood(X0) ) ).
cnf(u2556,axiom,
iowlThing(iFrance) ).
cnf(u3016,axiom,
abstractDomain(iFrance) ).
cnf(u2831,axiom,
( ~ iNutTopping(X0)
| ~ iFishTopping(X0) ) ).
cnf(u2503,axiom,
( ~ ihasBase(X0,X2)
| ~ ihasBase(X0,X1)
| X1 = X2 ) ).
cnf(u3003,axiom,
~ iSpiciness(iItaly) ).
cnf(u2968,axiom,
iItaly != iGermany ).
cnf(u3015,axiom,
abstractDomain(iAmerica) ).
cnf(u2402,axiom,
( ~ iSpicyTopping(X0)
| iPizzaTopping(X0) ) ).
cnf(u2477,axiom,
( ~ iPizzaTopping(X0)
| ~ iVegetableTopping(X0)
| iVegetarianTopping(X0) ) ).
cnf(u2462,axiom,
( ~ iVegetarianPizzaEquivalent2(X0)
| iNutTopping(X2)
| iHerbSpiceTopping(X2)
| iVegetableTopping(X2)
| iSauceTopping(X2)
| iFruitTopping(X2)
| ~ ihasTopping(X0,X2)
| iCheeseTopping(X2) ) ).
cnf(u2405,axiom,
( ~ iPizzaTopping(X0)
| ~ ihasSpiciness(X0,X1)
| ~ iHot(X1)
| iSpicyTopping(X0) ) ).
cnf(u2394,axiom,
( ~ iSpicyPizzaEquivalent(X0)
| abstractDomain(X0) ) ).
cnf(u2733,axiom,
( ~ iMeatTopping(X0)
| ~ iFishTopping(X0) ) ).
cnf(u2397,axiom,
( ~ iSpicyPizzaEquivalent(X0)
| ihasSpiciness(sK141(X0),sK142(X0)) ) ).
cnf(u2022,axiom,
( ~ iFood(X0)
| abstractDomain(X0) ) ).
cnf(u2672,axiom,
( ~ iCheeseTopping(X0)
| ~ iFishTopping(X0) ) ).
cnf(u2513,axiom,
( ~ ihasIngredient(X1,X2)
| ~ ihasIngredient(X0,X1)
| ihasIngredient(X0,X2) ) ).
cnf(u2443,axiom,
( ~ iVegetableTopping(X0)
| abstractDomain(X0) ) ).
cnf(u2981,axiom,
( ~ iPizza(X0)
| ~ abstractDomain(X0)
| ihasTopping(X0,sK152(X0))
| iVegetarianPizza(X0)
| ihasTopping(X0,sK153(X0)) ) ).
cnf(u2428,axiom,
( ~ iPizza(X0)
| iThinAndCrispyPizza(X0)
| ~ abstractDomain(X0)
| ihasBase(X0,sK148(X0)) ) ).
cnf(u2604,axiom,
( ~ iVegetableTopping(X0)
| ~ iFishTopping(X0) ) ).
cnf(u2552,axiom,
iowlThing(iAmerica) ).
cnf(u2996,axiom,
~ iValuePartition(iGermany) ).
cnf(u2547,axiom,
( ~ iisToppingOf(X0,X1)
| iPizzaTopping(X0) ) ).
cnf(u2964,axiom,
iAmerica != iGermany ).
cnf(u2539,axiom,
( ~ iisIngredientOf(X1,X2)
| ~ iisIngredientOf(X0,X1)
| iisIngredientOf(X0,X2) ) ).
cnf(u3007,axiom,
( ~ ihasBase(X1,X2)
| iisIngredientOf(X2,X0)
| ~ ihasIngredient(X0,X1) ) ).
cnf(u2998,axiom,
iDomainConcept(iFrance) ).
cnf(u2150,axiom,
( ~ iMeatTopping(X0)
| iPizzaTopping(X0) ) ).
cnf(u2965,axiom,
iGermany != iEngland ).
cnf(u2425,axiom,
( ~ iThinAndCrispyPizza(X0)
| ~ ihasBase(X0,X2)
| iThinAndCrispyBase(X2) ) ).
cnf(u2019,axiom,
( ~ iFishTopping(X0)
| iMild(sK39(X0)) ) ).
cnf(u2442,axiom,
( abstractDomain(X0)
| ~ iValuePartition(X0) ) ).
cnf(u2385,axiom,
( ~ iMild(X0)
| iSpiciness(X0) ) ).
cnf(u2502,axiom,
( ~ ihasBase(X0,X1)
| abstractDomain(X0) ) ).
cnf(u2018,axiom,
( ~ iFishTopping(X0)
| abstractDomain(X0) ) ).
cnf(u2521,axiom,
( ~ ihasSpiciness(X0,X1)
| iSpiciness(X1) ) ).
cnf(u2112,axiom,
( sK65(X0) != sK67(X0)
| ~ iInterestingPizza(X0) ) ).
cnf(u2836,axiom,
( ~ iMeatTopping(X0)
| ~ iHerbSpiceTopping(X0) ) ).
cnf(u2983,axiom,
( ~ iSpicyTopping(X1)
| ~ ihasTopping(X0,X1)
| iSpicyPizza(X0) ) ).
cnf(u2879,axiom,
( ~ iFruitTopping(X0)
| ~ iFishTopping(X0) ) ).
cnf(u2551,axiom,
iCountry(iAmerica) ).
cnf(u2474,axiom,
( ~ iVegetarianTopping(X0)
| iNutTopping(X0)
| iHerbSpiceTopping(X0)
| iVegetableTopping(X0)
| iSauceTopping(X0)
| iFruitTopping(X0)
| iCheeseTopping(X0) ) ).
cnf(u2259,axiom,
( ~ iPizzaTopping(X0)
| abstractDomain(X0) ) ).
cnf(u2543,axiom,
( iisIngredientOf(X0,X1)
| ~ ihasIngredient(X1,X0) ) ).
cnf(u2986,axiom,
( ~ iCheeseTopping(X1)
| ~ ihasTopping(X0,X1)
| iCheeseyPizza(X0) ) ).
cnf(u2989,axiom,
( ~ iisIngredientOf(X0,X1)
| iisIngredientOf(X0,X2)
| ~ ihasIngredient(X2,X1) ) ).
cnf(u3013,axiom,
~ abstractDomain(sK1) ).
cnf(u2805,axiom,
( ~ iMeatTopping(X0)
| ~ iCheeseTopping(X0) ) ).
cnf(u2501,axiom,
( ~ ihasBase(X0,X1)
| abstractDomain(X1) ) ).
cnf(u2257,axiom,
( ~ iPizzaBase(X0)
| abstractDomain(X0) ) ).
cnf(u2472,axiom,
( ~ iVegetarianTopping(X0)
| abstractDomain(X0) ) ).
cnf(u2423,axiom,
( ~ iThinAndCrispyBase(X0)
| iPizzaBase(X0) ) ).
cnf(u2532,axiom,
( ~ iisBaseOf(X2,X0)
| ~ iisBaseOf(X1,X0)
| X1 = X2 ) ).
cnf(u2984,axiom,
( ~ iMeatTopping(X1)
| ~ ihasTopping(X0,X1)
| iMeatyPizza(X0) ) ).
cnf(u2524,axiom,
( ~ ihasTopping(X2,X0)
| ~ ihasTopping(X1,X0)
| X1 = X2 ) ).
cnf(u2459,axiom,
( ~ iPizza(X0)
| iVegetarianPizzaEquivalent1(X0)
| ~ abstractDomain(X0)
| ihasTopping(X0,sK154(X0)) ) ).
cnf(u1991,axiom,
( ~ iCountry(X0)
| abstractDomain(X0) ) ).
cnf(u2971,axiom,
iFrance != iGermany ).
cnf(u3012,axiom,
( ~ ihasBase(X0,X1)
| iFood(X0) ) ).
cnf(u2114,axiom,
( ~ iInterestingPizza(X0)
| ihasTopping(X0,sK67(X0)) ) ).
cnf(u2558,axiom,
iowlThing(iGermany) ).
cnf(u2550,axiom,
( ~ ihasTopping(X1,X0)
| iisToppingOf(X0,X1) ) ).
cnf(u2962,axiom,
( ~ ihasTopping(X0,X1)
| ihasIngredient(X0,X1) ) ).
cnf(u2476,axiom,
( ~ iSauceTopping(X0)
| iVegetarianTopping(X0)
| ~ iPizzaTopping(X0) ) ).
cnf(u2404,axiom,
( ~ iSpicyTopping(X0)
| ihasSpiciness(X0,sK143(X0)) ) ).
cnf(u2396,axiom,
( ~ iSpicyPizzaEquivalent(X0)
| iHot(sK142(X0)) ) ).
cnf(u2111,axiom,
( sK66(X0) != sK67(X0)
| ~ iInterestingPizza(X0) ) ).
cnf(u2520,axiom,
( ~ ihasSpiciness(X0,X2)
| ~ ihasSpiciness(X0,X1)
| X1 = X2 ) ).
cnf(u2471,axiom,
( ~ iCheeseTopping(sK155(X0))
| ~ iPizza(X0)
| ~ abstractDomain(X0)
| iVegetarianPizzaEquivalent2(X0) ) ).
cnf(u2515,axiom,
( ~ ihasIngredient(X0,X1)
| iFood(X1) ) ).
cnf(u2995,axiom,
iDomainConcept(iGermany) ).
cnf(u2094,axiom,
( ~ iHerbSpiceTopping(X0)
| abstractDomain(X0) ) ).
cnf(u3019,axiom,
abstractDomain(iEngland) ).
cnf(u2966,axiom,
iAmerica != iItaly ).
cnf(u2909,axiom,
( ~ iPizza(X0)
| ~ iPizzaTopping(X0) ) ).
cnf(u2422,axiom,
( ~ iThinAndCrispyBase(X0)
| abstractDomain(X0) ) ).
cnf(u2546,axiom,
( ~ iisToppingOf(X0,X2)
| ~ iisToppingOf(X0,X1)
| X1 = X2 ) ).
cnf(u2153,axiom,
( ~ iMeatyPizza(X0)
| ihasTopping(X0,sK77(X0)) ) ).
cnf(u2538,axiom,
( ~ iisIngredientOf(X0,X1)
| abstractDomain(X0) ) ).
cnf(u1877,axiom,
abstractDomain(sK0) ).
cnf(u3032,axiom,
~ iValuePartition(sK1) ).
cnf(u2541,axiom,
( ~ iisIngredientOf(X0,X1)
| iFood(X1) ) ).
cnf(u2205,axiom,
( ~ iNutTopping(X0)
| ihasSpiciness(X0,sK88(X0)) ) ).
cnf(u2392,axiom,
( ~ iSpicyPizza(X0)
| ihasTopping(X0,sK140(X0)) ) ).
cnf(u2384,axiom,
( iMedium(X0)
| iHot(X0)
| iMild(X0)
| ~ iSpiciness(X0) ) ).
cnf(u2467,axiom,
( ~ iSauceTopping(sK155(X0))
| ~ iPizza(X0)
| ~ abstractDomain(X0)
| iVegetarianPizzaEquivalent2(X0) ) ).
cnf(u2544,axiom,
( ~ iisToppingOf(X0,X1)
| abstractDomain(X1) ) ).
cnf(u2444,axiom,
( ~ iVegetableTopping(X0)
| iPizzaTopping(X0) ) ).
cnf(u2519,axiom,
( ~ ihasSpiciness(X0,X1)
| abstractDomain(X0) ) ).
cnf(u2999,axiom,
~ iValuePartition(iFrance) ).
cnf(u3031,axiom,
~ iDomainConcept(sK1) ).
cnf(u2511,axiom,
( ~ ihasIngredient(X0,X1)
| abstractDomain(X1) ) ).
cnf(u1980,axiom,
( ~ iCheeseyPizza(X0)
| iCheeseTopping(sK31(X0)) ) ).
cnf(u2625,axiom,
( ~ iPizzaBase(X0)
| ~ iPizzaTopping(X0) ) ).
cnf(u2470,axiom,
( ~ iNutTopping(sK155(X0))
| ~ iPizza(X0)
| ~ abstractDomain(X0)
| iVegetarianPizzaEquivalent2(X0) ) ).
cnf(u2537,axiom,
( ~ iisIngredientOf(X0,X1)
| abstractDomain(X1) ) ).
cnf(u1981,axiom,
( ~ iCheeseyPizza(X0)
| ihasTopping(X0,sK31(X0)) ) ).
cnf(u2529,axiom,
( ~ iisBaseOf(X0,X1)
| abstractDomain(X1) ) ).
cnf(u3001,axiom,
iDomainConcept(iItaly) ).
cnf(u2253,axiom,
( ~ iPizza(X0)
| abstractDomain(X0) ) ).
cnf(u2555,axiom,
iCountry(iFrance) ).
cnf(u2391,axiom,
( ~ iSpicyPizza(X0)
| iSpicyTopping(sK140(X0)) ) ).
cnf(u2500,axiom,
( ~ iowlThing(X0)
| abstractDomain(X0) ) ).
cnf(u2256,axiom,
( ~ iPizza(X0)
| iFood(X0) ) ).
cnf(u2980,axiom,
( ~ iPizza(X0)
| ~ abstractDomain(X0)
| ihasTopping(X0,sK152(X0))
| iVegetarianPizza(X0)
| iFishTopping(sK153(X0)) ) ).
cnf(u2383,axiom,
( abstractDomain(X0)
| ~ iSpiciness(X0) ) ).
cnf(u2862,axiom,
( ~ iPizzaBase(X0)
| ~ iPizza(X0) ) ).
cnf(u2944,axiom,
( ~ iNutTopping(X0)
| ~ iMeatTopping(X0) ) ).
cnf(u1977,axiom,
( ~ iCheeseTopping(X0)
| abstractDomain(X0) ) ).
cnf(u2978,axiom,
( ~ iPizza(X0)
| ~ abstractDomain(X0)
| iMeatTopping(sK152(X0))
| iVegetarianPizza(X0)
| iFishTopping(sK153(X0)) ) ).
cnf(u2466,axiom,
( ~ iFruitTopping(sK155(X0))
| ~ iPizza(X0)
| ~ abstractDomain(X0)
| iVegetarianPizzaEquivalent2(X0) ) ).
cnf(u2526,axiom,
( ~ ihasTopping(X0,X1)
| iPizzaTopping(X1) ) ).
cnf(u2469,axiom,
( ~ iHerbSpiceTopping(sK155(X0))
| ~ iPizza(X0)
| ~ abstractDomain(X0)
| iVegetarianPizzaEquivalent2(X0) ) ).
cnf(u2401,axiom,
( ~ iSpicyTopping(X0)
| abstractDomain(X0) ) ).
cnf(u2518,axiom,
( ~ ihasSpiciness(X0,X1)
| abstractDomain(X1) ) ).
cnf(u2559,axiom,
iCountry(iItaly) ).
cnf(u2633,axiom,
( ~ iMild(X0)
| ~ iHot(X0) ) ).
cnf(u2990,axiom,
( ~ ihasIngredient(X2,X0)
| ~ ihasIngredient(X1,X2)
| iisIngredientOf(X0,X1) ) ).
cnf(u2206,axiom,
( ~ iNutTopping(X0)
| iPizzaTopping(X0) ) ).
cnf(u3004,axiom,
iDomainConcept(iAmerica) ).
cnf(u2919,axiom,
( ~ iSauceTopping(X0)
| ~ iFishTopping(X0) ) ).
cnf(u3028,axiom,
~ iSpiciness(sK1) ).
cnf(u2963,axiom,
iAmerica != iEngland ).
cnf(u2255,axiom,
( ~ iPizza(X0)
| ihasBase(X0,sK101(X0)) ) ).
cnf(u3002,axiom,
~ iValuePartition(iItaly) ).
cnf(u2330,axiom,
( ~ iSauceTopping(X0)
| iPizzaTopping(X0) ) ).
cnf(u2969,axiom,
iAmerica != iFrance ).
cnf(u2514,axiom,
( ~ ihasIngredient(X0,X1)
| iFood(X0) ) ).
cnf(u2506,axiom,
( ~ ihasBase(X0,X1)
| iPizzaBase(X1) ) ).
cnf(u2449,axiom,
( ~ iVegetarianPizza(X0)
| ~ iMeatTopping(X3)
| ~ ihasTopping(X0,X3) ) ).
cnf(u2548,axiom,
( ~ iisToppingOf(X0,X1)
| iPizza(X1) ) ).
cnf(u3000,axiom,
~ iSpiciness(iFrance) ).
cnf(u2480,axiom,
( ~ iPizzaTopping(X0)
| ~ iCheeseTopping(X0)
| iVegetarianTopping(X0) ) ).
cnf(u2512,axiom,
( ~ ihasIngredient(X0,X1)
| abstractDomain(X0) ) ).
cnf(u2540,axiom,
( ~ iisIngredientOf(X0,X1)
| iFood(X0) ) ).
cnf(u2992,axiom,
iDomainConcept(iEngland) ).
cnf(u3029,axiom,
~ iMedium(sK1) ).
cnf(u2987,axiom,
( ~ ihasSpiciness(X1,X2)
| ~ ihasTopping(X0,X1)
| iSpicyPizzaEquivalent(X0)
| ~ iHot(X2) ) ).
cnf(u2738,axiom,
( ~ iDomainConcept(X0)
| ~ iValuePartition(X0) ) ).
cnf(u2001,axiom,
( abstractDomain(X0)
| ~ iDomainConcept(X0) ) ).
cnf(u2386,axiom,
( ~ iHot(X0)
| iSpiciness(X0) ) ).
cnf(u2329,axiom,
( ~ iSauceTopping(X0)
| abstractDomain(X0) ) ).
cnf(u2020,axiom,
( ~ iFishTopping(X0)
| ihasSpiciness(X0,sK39(X0)) ) ).
cnf(u2389,axiom,
( ~ iSpicyPizza(X0)
| abstractDomain(X0) ) ).
cnf(u3017,axiom,
abstractDomain(iItaly) ).
cnf(u3005,axiom,
~ iValuePartition(iAmerica) ).
cnf(u2021,axiom,
( ~ iFishTopping(X0)
| iPizzaTopping(X0) ) ).
cnf(u2116,axiom,
( ~ iInterestingPizza(X0)
| ihasTopping(X0,sK65(X0)) ) ).
cnf(u2478,axiom,
( ~ iPizzaTopping(X0)
| ~ iHerbSpiceTopping(X0)
| iVegetarianTopping(X0) ) ).
cnf(u2560,axiom,
iowlThing(iItaly) ).
cnf(u2536,axiom,
( ~ ihasBase(X1,X0)
| iisBaseOf(X0,X1) ) ).
cnf(u2151,axiom,
( ~ iMeatyPizza(X0)
| abstractDomain(X0) ) ).
cnf(u2023,axiom,
( ~ iFood(X0)
| iDomainConcept(X0) ) ).
cnf(u2479,axiom,
( ~ iNutTopping(X0)
| iVegetarianTopping(X0)
| ~ iPizzaTopping(X0) ) ).
cnf(u2110,axiom,
( ~ iInterestingPizza(X0)
| abstractDomain(X0) ) ).
cnf(u2523,axiom,
( ~ ihasTopping(X0,X1)
| abstractDomain(X0) ) ).
cnf(u2991,axiom,
( ~ ihasBase(X1,X2)
| ihasIngredient(X0,X2)
| ~ ihasIngredient(X0,X1) ) ).
cnf(u2646,axiom,
( ~ iMeatTopping(X0)
| ~ iVegetableTopping(X0) ) ).
cnf(u3011,axiom,
( iSpiciness(sK143(X0))
| ~ iSpicyTopping(X0) ) ).
cnf(u2258,axiom,
( ~ iPizzaBase(X0)
| iFood(X0) ) ).
cnf(u2531,axiom,
( ~ iisBaseOf(X0,X2)
| ~ iisBaseOf(X0,X1)
| X1 = X2 ) ).
cnf(u1878,axiom,
dataDomain(sK1) ).
cnf(u2554,axiom,
iowlThing(iEngland) ).
cnf(u2557,axiom,
iCountry(iGermany) ).
cnf(u2468,axiom,
( ~ iVegetableTopping(sK155(X0))
| ~ iPizza(X0)
| ~ abstractDomain(X0)
| iVegetarianPizzaEquivalent2(X0) ) ).
cnf(u2403,axiom,
( iHot(sK143(X0))
| ~ iSpicyTopping(X0) ) ).
cnf(u2203,axiom,
( ~ iNutTopping(X0)
| abstractDomain(X0) ) ).
cnf(u2993,axiom,
~ iValuePartition(iEngland) ).
cnf(u2460,axiom,
( ~ iVegetarianTopping(sK154(X0))
| ~ iPizza(X0)
| ~ abstractDomain(X0)
| iVegetarianPizzaEquivalent1(X0) ) ).
cnf(u2395,axiom,
( ~ iSpicyPizzaEquivalent(X0)
| iPizzaTopping(sK141(X0)) ) ).
cnf(u2972,axiom,
iFrance != iItaly ).
cnf(u3006,axiom,
~ iSpiciness(iAmerica) ).
cnf(u2158,axiom,
( ~ iMild(X0)
| abstractDomain(X0) ) ).
cnf(u1993,axiom,
( ~ iCountry(X0)
| iDomainConcept(X0) ) ).
cnf(u2970,axiom,
iFrance != iEngland ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWB036+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n003.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 28 07:12:42 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.77/1.92 % (1398509)Detected formulas, will run a generic FOF schedule.
% 5.77/1.92 % (1398514)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1333389705:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.77/1.92 % (1398515)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1875901384:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.77/1.92 % (1398518)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1382441770:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.77/1.92 % (1398519)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1805485765:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.77/1.92 % (1398517)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3973439854:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.77/1.92 % (1398516)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2304954198:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.77/1.92 % (1398520)dis-21_1_sil=8000:lcm=predicate:random_seed=2053578287:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 5.77/1.92 % (1398518)Refutation not found, incomplete strategy
% 5.77/1.92 % (1398518)------------------------------
% 5.77/1.92 % (1398518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.92 % (1398518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.92 % (1398518)CaDiCaL version: 2.1.3
% 5.77/1.92 % (1398518)Termination reason: Refutation not found, incomplete strategy
% 5.77/1.92 % (1398518)Time elapsed: 0.001 s
% 5.77/1.92 % (1398517)Refutation not found, incomplete strategy
% 5.77/1.92 % (1398517)------------------------------
% 5.77/1.92 % (1398517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.92 % (1398517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.92 % (1398517)CaDiCaL version: 2.1.3
% 5.77/1.92 % (1398518)Peak memory usage: 86 MB
% 5.77/1.92 % (1398518)Instructions burned: 2 (million)
% 5.77/1.92 % (1398517)Termination reason: Refutation not found, incomplete strategy
% 5.77/1.92 % (1398517)Time elapsed: 0.002 s
% 5.77/1.92 % (1398517)Peak memory usage: 86 MB
% 5.77/1.92 % (1398517)Instructions burned: 1 (million)
% 5.77/1.92 % (1398519)Refutation not found, incomplete strategy
% 5.77/1.92 % (1398519)------------------------------
% 5.77/1.92 % (1398519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.92 % (1398519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.92 % (1398519)CaDiCaL version: 2.1.3
% 5.77/1.92 % (1398519)Termination reason: Refutation not found, incomplete strategy
% 5.77/1.92 % (1398519)Time elapsed: 0.011 s
% 5.77/1.92 % (1398519)Peak memory usage: 89 MB
% 5.77/1.92 % (1398519)Instructions burned: 16 (million)
% 5.77/1.92 % (1398520)Refutation not found, incomplete strategy
% 5.77/1.92 % (1398520)------------------------------
% 5.77/1.92 % (1398520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.92 % (1398520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.92 % (1398520)CaDiCaL version: 2.1.3
% 5.77/1.92 % (1398520)Termination reason: Refutation not found, incomplete strategy
% 5.77/1.92 % (1398520)Time elapsed: 0.023 s
% 5.77/1.92 % (1398520)Peak memory usage: 89 MB
% 5.77/1.92 % (1398520)Instructions burned: 37 (million)
% 5.77/1.92 % (1398518)------------------------------
% 5.77/1.92 % (1398518)------------------------------
% 5.77/1.92 % (1398517)------------------------------
% 5.77/1.92 % (1398517)------------------------------
% 5.77/1.92 % (1398519)------------------------------
% 5.77/1.92 % (1398519)------------------------------
% 5.77/1.92 % (1398520)------------------------------
% 5.77/1.92 % (1398520)------------------------------
% 5.77/1.92 % (1398530)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3840660898:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 5.77/1.92 % (1398528)lrs+10_1_sil=8000:sp=occurrence:random_seed=3141898726:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 5.77/1.92 % (1398529)lrs+10_1_sil=32000:urr=on:br=off:random_seed=450194499:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 5.77/1.92 % (1398528)Refutation not found, incomplete strategy
% 5.77/1.92 % (1398528)------------------------------
% 5.77/1.92 % (1398528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.92 % (1398530)Refutation not found, incomplete strategy
% 5.77/1.92 % (1398530)------------------------------
% 5.77/1.92 % (1398530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.92 % (1398528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.92 % (1398530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.92 % (1398530)CaDiCaL version: 2.1.3
% 5.77/1.92 % (1398528)CaDiCaL version: 2.1.3
% 5.77/1.92 % (1398530)Termination reason: Refutation not found, incomplete strategy
% 5.77/1.92 % (1398530)Time elapsed: 0.002 s
% 5.77/1.92 % (1398528)Termination reason: Refutation not found, incomplete strategy
% 5.77/1.92 % (1398528)Time elapsed: 0.002 s
% 5.77/1.92 % (1398530)Peak memory usage: 86 MB
% 5.77/1.92 % (1398528)Peak memory usage: 86 MB
% 5.77/1.92 % (1398530)Instructions burned: 1 (million)
% 5.77/1.92 % (1398528)Instructions burned: 1 (million)
% 5.77/1.92 % (1398529)Refutation not found, incomplete strategy
% 5.77/1.92 % (1398529)------------------------------
% 5.77/1.92 % (1398529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.92 % (1398529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.92 % (1398529)CaDiCaL version: 2.1.3
% 5.77/1.92 % (1398529)Termination reason: Refutation not found, incomplete strategy
% 5.77/1.92 % (1398529)Time elapsed: 0.003 s
% 5.77/1.92 % (1398529)Peak memory usage: 87 MB
% 5.77/1.92 % (1398529)Instructions burned: 4 (million)
% 5.77/1.92 % (1398531)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3315659543:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 5.77/1.92 % (1398531)Refutation not found, incomplete strategy
% 5.77/1.92 % (1398531)------------------------------
% 5.77/1.92 % (1398531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.92 % (1398531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.92 % (1398531)CaDiCaL version: 2.1.3
% 5.77/1.92 % (1398531)Termination reason: Refutation not found, incomplete strategy
% 5.77/1.92 % (1398531)Time elapsed: 0.012 s
% 5.77/1.92 % (1398531)Peak memory usage: 89 MB
% 5.77/1.92 % (1398531)Instructions burned: 19 (million)
% 5.77/1.92 % (1398516)Refutation not found, incomplete strategy
% 5.77/1.92 % (1398516)------------------------------
% 5.77/1.92 % (1398516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.92 % (1398516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.92 % (1398516)CaDiCaL version: 2.1.3
% 5.77/1.92 % (1398516)Termination reason: Refutation not found, incomplete strategy
% 5.77/1.92 % (1398516)Time elapsed: 0.567 s
% 5.77/1.92 % (1398516)Peak memory usage: 128 MB
% 5.77/1.92 % (1398516)Instructions burned: 849 (million)
% 5.77/1.92 % (1398529)------------------------------
% 5.77/1.92 % (1398529)------------------------------
% 5.77/1.92 % (1398530)------------------------------
% 5.77/1.92 % (1398530)------------------------------
% 5.77/1.92 % (1398528)------------------------------
% 5.77/1.92 % (1398528)------------------------------
% 5.77/1.92 % (1398515)First to succeed.
% 5.77/1.92 % (1398515)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1398509"
% 5.77/1.92 % (1398531)------------------------------
% 5.77/1.92 % (1398531)------------------------------
% 5.77/1.92 % (1398536)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1070849637:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi)
% 5.77/1.92 % (1398537)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2219660685:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 5.77/1.92 % (1398538)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=743912047:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 5.77/1.92 % (1398536)Refutation not found, incomplete strategy
% 5.77/1.92 % (1398536)------------------------------
% 5.77/1.92 % (1398536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.92 % (1398536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.92 % (1398536)CaDiCaL version: 2.1.3
% 5.77/1.92 % (1398536)Termination reason: Refutation not found, incomplete strategy
% 5.77/1.92 % (1398536)Time elapsed: 0.002 s
% 5.77/1.92 % (1398536)Peak memory usage: 86 MB
% 5.77/1.92 % (1398536)Instructions burned: 2 (million)
% 5.77/1.92 % (1398538)Refutation not found, incomplete strategy
% 5.77/1.92 % (1398538)------------------------------
% 5.77/1.92 % (1398538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.92 % (1398538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.92 % (1398538)CaDiCaL version: 2.1.3
% 5.77/1.92 % (1398538)Termination reason: Refutation not found, incomplete strategy
% 5.77/1.92 % (1398538)Time elapsed: 0.007 s
% 5.77/1.92 % (1398538)Peak memory usage: 89 MB
% 5.77/1.92 % (1398538)Instructions burned: 9 (million)
% 5.77/1.92 % (1398539)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3947430017:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 5.77/1.92 % (1398539)Refutation not found, incomplete strategy
% 5.77/1.92 % (1398539)------------------------------
% 5.77/1.92 % (1398539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.92 % (1398539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.92 % (1398539)CaDiCaL version: 2.1.3
% 5.77/1.92 % (1398539)Termination reason: Refutation not found, incomplete strategy
% 5.77/1.92 % (1398539)Time elapsed: 0.006 s
% 5.77/1.92 % (1398539)Peak memory usage: 88 MB
% 5.77/1.92 % (1398539)Instructions burned: 7 (million)
% 5.77/1.92 % (1398516)------------------------------
% 5.77/1.92 % (1398516)------------------------------
% 5.77/1.92 % SZS status Satisfiable for theBenchmark
% 5.77/1.92 % SZS output start Saturation.
% See solution above
% 5.77/1.93 % SZS output start Definitions and Model Updates.
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK150(X0)) | ~iTomatoTopping(X0) is false, set ~iTomatoTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMild(sK150(X0)) | ~iTomatoTopping(X0) is false, set ~iTomatoTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCheeseTopping(X0) | ~iVegetableTopping(X0) is false, set ~iVegetableTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iVegetableTopping(X0) | ~iTomatoTopping(X0) is false, set ~iTomatoTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iTomatoTopping(X0) is false, set ~iTomatoTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK78(X0)) | ~iMozzarellaTopping(X0) is false, set ~iMozzarellaTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iCheeseTopping(X0) | ~iMozzarellaTopping(X0) is false, set ~iMozzarellaTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~ihasCountryOfOrigin(X0,X1) is false, set ~ihasCountryOfOrigin(X0,X1) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X1) | ~ihasCountryOfOrigin(X0,X1) is false, set ~ihasCountryOfOrigin(X0,X1) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iRealItalianPizza(X0) is false, set ~iRealItalianPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iRealItalianPizza(X0) is false, set ~iRealItalianPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iThinAndCrispyBase(X1) | ~ihasBase(X0,X1) | ~iRealItalianPizza(X0) is false, set ~iRealItalianPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iRealItalianPizza(X0) | ~ihasCountryOfOrigin(X0,iItaly) | ~iPizza(X0) is false, set ~ihasCountryOfOrigin(X0,iItaly) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasCountryOfOrigin(X0,iItaly) | ~iMozzarellaTopping(X0) is false, set ~iMozzarellaTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMild(sK78(X0)) | ~iMozzarellaTopping(X0) is false, set ~iMozzarellaTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iMozzarellaTopping(X0) is false, set ~iMozzarellaTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iNamedPizza(X0) is false, set ~iNamedPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPizza(X0) | ~iNamedPizza(X0) is false, set ~iNamedPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iOliveTopping(X0) is false, set ~iOliveTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK89(X0)) | ~iOliveTopping(X0) is false, set ~iOliveTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMild(sK89(X0)) | ~iOliveTopping(X0) is false, set ~iOliveTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iVegetableTopping(X0) | ~iOliveTopping(X0) is false, set ~iOliveTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iOliveTopping(X0) | ~iTomatoTopping(X0) is false, set ~iOliveTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iFrance = X0 | iItaly = X0 | iGermany = X0 | iEngland = X0 | iAmerica = X0 | ~iCountry(X0) is false, set ~iCountry(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iGarlicTopping(X0) is false, set ~iGarlicTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iVegetableTopping(X0) | ~iGarlicTopping(X0) is false, set ~iGarlicTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK51(X0)) | ~iGarlicTopping(X0) is false, set ~iGarlicTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iSpiciness(X0) | ~iMedium(X0) is false, set ~iMedium(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iSpiciness(X0) | ~iMedium(X0) is false, set ~iMedium(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iMedium(X0) | ~iHot(X0) is false, set ~iMedium(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iMedium(X0) | ~iMild(X0) is false, set ~iMedium(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMedium(sK51(X0)) | ~iGarlicTopping(X0) is false, set ~iGarlicTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iOliveTopping(X0) | ~iGarlicTopping(X0) is false, set ~iGarlicTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iGarlicTopping(X0) | ~iTomatoTopping(X0) is false, set ~iGarlicTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iHamTopping(X0) is false, set ~iHamTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMeatTopping(X0) | ~iHamTopping(X0) is false, set ~iHamTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iAnchoviesTopping(X0) is false, set ~iAnchoviesTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iFishTopping(X0) | ~iAnchoviesTopping(X0) is false, set ~iAnchoviesTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iParmesanTopping(X0) is false, set ~iParmesanTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK97(X0)) | ~iParmesanTopping(X0) is false, set ~iParmesanTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMild(sK97(X0)) | ~iParmesanTopping(X0) is false, set ~iParmesanTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iCheeseTopping(X0) | ~iParmesanTopping(X0) is false, set ~iParmesanTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iParmesanTopping(X0) | ~iMozzarellaTopping(X0) is false, set ~iParmesanTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iMushroomTopping(X0) is false, set ~iMushroomTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMild(sK82(X0)) | ~iMushroomTopping(X0) is false, set ~iMushroomTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iCaperTopping(X0) is false, set ~iCaperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK19(X0)) | ~iCaperTopping(X0) is false, set ~iCaperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iVegetableTopping(X0) | ~iCaperTopping(X0) is false, set ~iCaperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iGarlicTopping(X0) | ~iMushroomTopping(X0) is false, set ~iMushroomTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iOliveTopping(X0) | ~iMushroomTopping(X0) is false, set ~iMushroomTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK82(X0)) | ~iMushroomTopping(X0) is false, set ~iMushroomTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iVegetableTopping(X0) | ~iMushroomTopping(X0) is false, set ~iMushroomTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iTomatoTopping(X0) | ~iMushroomTopping(X0) is false, set ~iMushroomTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCaperTopping(X0) | ~iMushroomTopping(X0) is false, set ~iMushroomTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCaperTopping(X0) | ~iTomatoTopping(X0) is false, set ~iCaperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iOliveTopping(X0) | ~iCaperTopping(X0) is false, set ~iCaperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMild(sK19(X0)) | ~iCaperTopping(X0) is false, set ~iCaperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iGarlicTopping(X0) | ~iCaperTopping(X0) is false, set ~iCaperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iOnionTopping(X0) is false, set ~iOnionTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iVegetableTopping(X0) | ~iOnionTopping(X0) is false, set ~iOnionTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK90(X0)) | ~iOnionTopping(X0) is false, set ~iOnionTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMedium(sK90(X0)) | ~iOnionTopping(X0) is false, set ~iOnionTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iOnionTopping(X0) | ~iMushroomTopping(X0) is false, set ~iOnionTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iOnionTopping(X0) | ~iCaperTopping(X0) is false, set ~iOnionTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iOnionTopping(X0) | ~iGarlicTopping(X0) is false, set ~iOnionTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iOnionTopping(X0) | ~iOliveTopping(X0) is false, set ~iOnionTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iOnionTopping(X0) | ~iTomatoTopping(X0) is false, set ~iOnionTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iVegetarianPizzaEquivalent2(X0) is false, set ~iVegetarianPizzaEquivalent2(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPizza(X0) | ~iVegetarianPizzaEquivalent2(X0) is false, set ~iVegetarianPizzaEquivalent2(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iVegetarianPizzaEquivalent2(X0) is false, set ~iVegetarianPizzaEquivalent2(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iPeperonataTopping(X0) is false, set ~iPeperonataTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPepperTopping(X0) | ~iCaperTopping(X0) is false, set ~iPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iPepperTopping(X0) is false, set ~iPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPepperTopping(X0) | ~iMushroomTopping(X0) is false, set ~iPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iVegetableTopping(X0) | ~iPepperTopping(X0) is false, set ~iPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPepperTopping(X0) | ~iGarlicTopping(X0) is false, set ~iPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPepperTopping(X0) | ~iOliveTopping(X0) is false, set ~iPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPepperTopping(X0) | ~iTomatoTopping(X0) is false, set ~iPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iOnionTopping(X0) | ~iPepperTopping(X0) is false, set ~iPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPepperTopping(X0) | ~iPeperonataTopping(X0) is false, set ~iPeperonataTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK98(X0)) | ~iPeperonataTopping(X0) is false, set ~iPeperonataTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMedium(sK98(X0)) | ~iPeperonataTopping(X0) is false, set ~iPeperonataTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iPeperoniSausageTopping(X0) is false, set ~iPeperoniSausageTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMeatTopping(X0) | ~iPeperoniSausageTopping(X0) is false, set ~iPeperoniSausageTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK99(X0)) | ~iPeperoniSausageTopping(X0) is false, set ~iPeperoniSausageTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMedium(sK99(X0)) | ~iPeperoniSausageTopping(X0) is false, set ~iPeperoniSausageTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPeperoniSausageTopping(X0) | ~iHamTopping(X0) is false, set ~iPeperoniSausageTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iVegetarianPizza(X0) is false, set ~iVegetarianPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iVegetarianPizza(X0) is false, set ~iVegetarianPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPizza(X0) | ~iVegetarianPizza(X0) is false, set ~iVegetarianPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iVegetarianPizza(X0) is false, set ~iVegetarianPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iNonVegetarianPizza(X0) | ~abstractDomain(X0) | iVegetarianPizza(X0) | ~iPizza(X0) is false, set iNonVegetarianPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPizza(X0) | ~ihasBase(X0,X1) is false, set ~ihasBase(X0,X1) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCheeseTopping(X0) | ~iHerbSpiceTopping(X0) is false, set ~iHerbSpiceTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iVegetableTopping(X0) | ~iFruitTopping(X0) is false, set ~iFruitTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iHerbSpiceTopping(X0) | ~iFruitTopping(X0) is false, set ~iFruitTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCheeseTopping(X0) | ~iFruitTopping(X0) is false, set ~iFruitTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iHerbSpiceTopping(X0) | ~iVegetableTopping(X0) is false, set ~iHerbSpiceTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK74(X0)) | ~iLeekTopping(X0) is false, set ~iLeekTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iVegetableTopping(X0) | ~iLeekTopping(X0) is false, set ~iLeekTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMild(sK74(X0)) | ~iLeekTopping(X0) is false, set ~iLeekTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iLeekTopping(X0) is false, set ~iLeekTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iOliveTopping(X0) | ~iLeekTopping(X0) is false, set ~iLeekTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iTomatoTopping(X0) | ~iLeekTopping(X0) is false, set ~iLeekTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iGarlicTopping(X0) | ~iLeekTopping(X0) is false, set ~iLeekTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iOnionTopping(X0) | ~iLeekTopping(X0) is false, set ~iLeekTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPepperTopping(X0) | ~iLeekTopping(X0) is false, set ~iLeekTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCaperTopping(X0) | ~iLeekTopping(X0) is false, set ~iLeekTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iMushroomTopping(X0) | ~iLeekTopping(X0) is false, set ~iLeekTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iNutTopping(X0) | ~iVegetableTopping(X0) is false, set ~iNutTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iNutTopping(X0) | ~iFruitTopping(X0) is false, set ~iNutTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iNutTopping(X0) | ~iHerbSpiceTopping(X0) is false, set ~iNutTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCheeseTopping(X0) | ~iNutTopping(X0) is false, set ~iNutTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iGreenPepperTopping(X0) is false, set ~iGreenPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPepperTopping(X0) | ~iGreenPepperTopping(X0) is false, set ~iGreenPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iHerbSpiceTopping(X0) | ~iSauceTopping(X0) is false, set ~iSauceTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iNutTopping(X0) | ~iSauceTopping(X0) is false, set ~iSauceTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iVegetableTopping(X0) | ~iSauceTopping(X0) is false, set ~iSauceTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCheeseTopping(X0) | ~iSauceTopping(X0) is false, set ~iSauceTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSauceTopping(X0) | ~iFruitTopping(X0) is false, set ~iSauceTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iGreenPepperTopping(X0) | ~iPeperonataTopping(X0) is false, set ~iGreenPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iLeekTopping(X0) | ~iAsparagusTopping(X0) is false, set ~iAsparagusTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iGarlicTopping(X0) | ~iAsparagusTopping(X0) is false, set ~iAsparagusTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iOliveTopping(X0) | ~iAsparagusTopping(X0) is false, set ~iAsparagusTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iTomatoTopping(X0) | ~iAsparagusTopping(X0) is false, set ~iAsparagusTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iMixedSeafoodTopping(X0) is false, set ~iMixedSeafoodTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPepperTopping(X0) | ~iAsparagusTopping(X0) is false, set ~iAsparagusTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iOnionTopping(X0) | ~iAsparagusTopping(X0) is false, set ~iAsparagusTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasBase(X1,X0) | ~iisBaseOf(X0,X1) is false, set ~iisBaseOf(X0,X1) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iChickenTopping(X0) is false, set ~iChickenTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK32(X0)) | ~iChickenTopping(X0) is false, set ~iChickenTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMild(sK32(X0)) | ~iChickenTopping(X0) is false, set ~iChickenTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasBase(X0,X1) | ~iisBaseOf(X1,X0) is false, set ~iisBaseOf(X1,X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMeatTopping(X0) | ~iChickenTopping(X0) is false, set ~iChickenTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iChickenTopping(X0) | ~iHamTopping(X0) is false, set ~iChickenTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPeperoniSausageTopping(X0) | ~iChickenTopping(X0) is false, set ~iChickenTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iPineKernels(X0) is false, set ~iPineKernels(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iNutTopping(X0) | ~iPineKernels(X0) is false, set ~iPineKernels(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iSweetPepperTopping(X0) is false, set ~iSweetPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK147(X0)) | ~iSweetPepperTopping(X0) is false, set ~iSweetPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMild(sK147(X0)) | ~iSweetPepperTopping(X0) is false, set ~iSweetPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPepperTopping(X0) | ~iSweetPepperTopping(X0) is false, set ~iSweetPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSweetPepperTopping(X0) | ~iGreenPepperTopping(X0) is false, set ~iSweetPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSweetPepperTopping(X0) | ~iPeperonataTopping(X0) is false, set ~iSweetPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iRedOnionTopping(X0) is false, set ~iRedOnionTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iOnionTopping(X0) | ~iRedOnionTopping(X0) is false, set ~iRedOnionTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iowlThing(X0) | ~abstractDomain(X0) is false, set iowlThing(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iRosemaryTopping(X0) is false, set ~iRosemaryTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK120(X0)) | ~iRosemaryTopping(X0) is false, set ~iRosemaryTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMild(sK120(X0)) | ~iRosemaryTopping(X0) is false, set ~iRosemaryTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iHerbSpiceTopping(X0) | ~iRosemaryTopping(X0) is false, set ~iRosemaryTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iTobascoPepperSauce(X0) is false, set ~iTobascoPepperSauce(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK149(X0)) | ~iTobascoPepperSauce(X0) is false, set ~iTobascoPepperSauce(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iHot(sK149(X0)) | ~iTobascoPepperSauce(X0) is false, set ~iTobascoPepperSauce(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iSauceTopping(X0) | ~iTobascoPepperSauce(X0) is false, set ~iTobascoPepperSauce(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iRocketTopping(X0) is false, set ~iRocketTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK116(X0)) | ~iRocketTopping(X0) is false, set ~iRocketTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iVegetableTopping(X0) | ~iRocketTopping(X0) is false, set ~iRocketTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iMushroomTopping(X0) | ~iRocketTopping(X0) is false, set ~iRocketTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iRocketTopping(X0) | ~iLeekTopping(X0) is false, set ~iRocketTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCaperTopping(X0) | ~iRocketTopping(X0) is false, set ~iRocketTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMedium(sK116(X0)) | ~iRocketTopping(X0) is false, set ~iRocketTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iOliveTopping(X0) | ~iRocketTopping(X0) is false, set ~iRocketTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iOnionTopping(X0) | ~iRocketTopping(X0) is false, set ~iRocketTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iRocketTopping(X0) | ~iTomatoTopping(X0) is false, set ~iRocketTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iGarlicTopping(X0) | ~iRocketTopping(X0) is false, set ~iRocketTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPepperTopping(X0) | ~iRocketTopping(X0) is false, set ~iRocketTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iRocketTopping(X0) | ~iAsparagusTopping(X0) is false, set ~iRocketTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iSpinachTopping(X0) is false, set ~iSpinachTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMild(sK144(X0)) | ~iSpinachTopping(X0) is false, set ~iSpinachTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK144(X0)) | ~iSpinachTopping(X0) is false, set ~iSpinachTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iVegetableTopping(X0) | ~iSpinachTopping(X0) is false, set ~iSpinachTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSpinachTopping(X0) | ~iMushroomTopping(X0) is false, set ~iSpinachTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSpinachTopping(X0) | ~iLeekTopping(X0) is false, set ~iSpinachTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSpinachTopping(X0) | ~iCaperTopping(X0) is false, set ~iSpinachTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSpinachTopping(X0) | ~iAsparagusTopping(X0) is false, set ~iSpinachTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iGarlicTopping(X0) | ~iSpinachTopping(X0) is false, set ~iSpinachTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSpinachTopping(X0) | ~iTomatoTopping(X0) is false, set ~iSpinachTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iOliveTopping(X0) | ~iSpinachTopping(X0) is false, set ~iSpinachTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSpinachTopping(X0) | ~iRocketTopping(X0) is false, set ~iSpinachTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iOnionTopping(X0) | ~iSpinachTopping(X0) is false, set ~iSpinachTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPepperTopping(X0) | ~iSpinachTopping(X0) is false, set ~iSpinachTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iFourCheesesTopping(X0) is false, set ~iFourCheesesTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iPrawnsTopping(X0) is false, set ~iPrawnsTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iCheeseTopping(X0) | ~iFourCheesesTopping(X0) is false, set ~iFourCheesesTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK40(X0)) | ~iFourCheesesTopping(X0) is false, set ~iFourCheesesTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iFishTopping(X0) | ~iPrawnsTopping(X0) is false, set ~iPrawnsTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPrawnsTopping(X0) | ~iAnchoviesTopping(X0) is false, set ~iPrawnsTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFourCheesesTopping(X0) | ~iMozzarellaTopping(X0) is false, set ~iFourCheesesTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFourCheesesTopping(X0) | ~iParmesanTopping(X0) is false, set ~iFourCheesesTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iCajunSpiceTopping(X0) is false, set ~iCajunSpiceTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iHerbSpiceTopping(X0) | ~iCajunSpiceTopping(X0) is false, set ~iCajunSpiceTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK18(X0)) | ~iCajunSpiceTopping(X0) is false, set ~iCajunSpiceTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iHot(sK18(X0)) | ~iCajunSpiceTopping(X0) is false, set ~iCajunSpiceTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iRosemaryTopping(X0) | ~iCajunSpiceTopping(X0) is false, set ~iCajunSpiceTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMild(sK40(X0)) | ~iFourCheesesTopping(X0) is false, set ~iFourCheesesTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iSultanaTopping(X0) is false, set ~iSultanaTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMedium(sK145(X0)) | ~iSultanaTopping(X0) is false, set ~iSultanaTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iThinAndCrispyPizza(X0) is false, set ~iThinAndCrispyPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iFruitTopping(X0) | ~iSultanaTopping(X0) is false, set ~iSultanaTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK145(X0)) | ~iSultanaTopping(X0) is false, set ~iSultanaTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iThinAndCrispyPizza(X0) is false, set ~iThinAndCrispyPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPizza(X0) | ~iThinAndCrispyPizza(X0) is false, set ~iThinAndCrispyPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iJalapenoPepperTopping(X0) is false, set ~iJalapenoPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK68(X0)) | ~iJalapenoPepperTopping(X0) is false, set ~iJalapenoPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPepperTopping(X0) | ~iJalapenoPepperTopping(X0) is false, set ~iJalapenoPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iVegetarianPizzaEquivalent1(X0) is false, set ~iVegetarianPizzaEquivalent1(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPizza(X0) | ~iVegetarianPizzaEquivalent1(X0) is false, set ~iVegetarianPizzaEquivalent1(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iVegetarianPizzaEquivalent1(X0) is false, set ~iVegetarianPizzaEquivalent1(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iHot(sK68(X0)) | ~iJalapenoPepperTopping(X0) is false, set ~iJalapenoPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iJalapenoPepperTopping(X0) | ~iPeperonataTopping(X0) is false, set ~iJalapenoPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iJalapenoPepperTopping(X0) | ~iGreenPepperTopping(X0) is false, set ~iJalapenoPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSweetPepperTopping(X0) | ~iJalapenoPepperTopping(X0) is false, set ~iJalapenoPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iHotGreenPepperTopping(X0) is false, set ~iHotGreenPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK62(X0)) | ~iHotGreenPepperTopping(X0) is false, set ~iHotGreenPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iHot(sK62(X0)) | ~iHotGreenPepperTopping(X0) is false, set ~iHotGreenPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iFishTopping(X0) | ~iMixedSeafoodTopping(X0) is false, set ~iMixedSeafoodTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAnchoviesTopping(X0) | ~iMixedSeafoodTopping(X0) is false, set ~iMixedSeafoodTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPrawnsTopping(X0) | ~iMixedSeafoodTopping(X0) is false, set ~iMixedSeafoodTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iGreenPepperTopping(X0) | ~iHotGreenPepperTopping(X0) is false, set ~iHotGreenPepperTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,X1) | ~iisToppingOf(X1,X0) is false, set ~iisToppingOf(X1,X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X1,X0) | ~iisToppingOf(X0,X1) is false, set ~iisToppingOf(X0,X1) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iPetitPoisTopping(X0) is false, set ~iPetitPoisTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMild(sK100(X0)) | ~iPetitPoisTopping(X0) is false, set ~iPetitPoisTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK100(X0)) | ~iPetitPoisTopping(X0) is false, set ~iPetitPoisTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iVegetableTopping(X0) | ~iPetitPoisTopping(X0) is false, set ~iPetitPoisTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPetitPoisTopping(X0) | ~iMushroomTopping(X0) is false, set ~iPetitPoisTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPetitPoisTopping(X0) | ~iCaperTopping(X0) is false, set ~iPetitPoisTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPetitPoisTopping(X0) | ~iLeekTopping(X0) is false, set ~iPetitPoisTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPetitPoisTopping(X0) | ~iRocketTopping(X0) is false, set ~iPetitPoisTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPetitPoisTopping(X0) | ~iTomatoTopping(X0) is false, set ~iPetitPoisTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPetitPoisTopping(X0) | ~iOliveTopping(X0) is false, set ~iPetitPoisTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPetitPoisTopping(X0) | ~iSpinachTopping(X0) is false, set ~iPetitPoisTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iSlicedTomatoTopping(X0) is false, set ~iSlicedTomatoTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPetitPoisTopping(X0) | ~iPepperTopping(X0) is false, set ~iPetitPoisTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPetitPoisTopping(X0) | ~iOnionTopping(X0) is false, set ~iPetitPoisTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPetitPoisTopping(X0) | ~iGarlicTopping(X0) is false, set ~iPetitPoisTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iTomatoTopping(X0) | ~iSlicedTomatoTopping(X0) is false, set ~iSlicedTomatoTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMild(sK128(X0)) | ~iSlicedTomatoTopping(X0) is false, set ~iSlicedTomatoTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK128(X0)) | ~iSlicedTomatoTopping(X0) is false, set ~iSlicedTomatoTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMild(sK10(X0)) | ~iArtichokeTopping(X0) is false, set ~iArtichokeTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK10(X0)) | ~iArtichokeTopping(X0) is false, set ~iArtichokeTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iArtichokeTopping(X0) is false, set ~iArtichokeTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iCheeseTopping(X0) | ~iGorgonzolaTopping(X0) is false, set ~iGorgonzolaTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMild(sK61(X0)) | ~iGorgonzolaTopping(X0) is false, set ~iGorgonzolaTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK61(X0)) | ~iGorgonzolaTopping(X0) is false, set ~iGorgonzolaTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iGorgonzolaTopping(X0) is false, set ~iGorgonzolaTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | dataDomain(X0) is false, set dataDomain(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFourCheesesTopping(X0) | ~iGorgonzolaTopping(X0) is false, set ~iGorgonzolaTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iParmesanTopping(X0) | ~iGorgonzolaTopping(X0) is false, set ~iGorgonzolaTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iGorgonzolaTopping(X0) | ~iMozzarellaTopping(X0) is false, set ~iGorgonzolaTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPetitPoisTopping(X0) | ~iArtichokeTopping(X0) is false, set ~iArtichokeTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iMushroomTopping(X0) | ~iArtichokeTopping(X0) is false, set ~iArtichokeTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iVegetableTopping(X0) | ~iArtichokeTopping(X0) is false, set ~iArtichokeTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iArtichokeTopping(X0) | ~iLeekTopping(X0) is false, set ~iArtichokeTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCaperTopping(X0) | ~iArtichokeTopping(X0) is false, set ~iArtichokeTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iGarlicTopping(X0) | ~iArtichokeTopping(X0) is false, set ~iArtichokeTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iOliveTopping(X0) | ~iArtichokeTopping(X0) is false, set ~iArtichokeTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iHotSpicedBeefTopping(X0) is false, set ~iHotSpicedBeefTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMeatTopping(X0) | ~iHotSpicedBeefTopping(X0) is false, set ~iHotSpicedBeefTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iTomatoTopping(X0) | ~iArtichokeTopping(X0) is false, set ~iArtichokeTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK63(X0)) | ~iHotSpicedBeefTopping(X0) is false, set ~iHotSpicedBeefTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iHot(sK63(X0)) | ~iHotSpicedBeefTopping(X0) is false, set ~iHotSpicedBeefTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iRocketTopping(X0) | ~iArtichokeTopping(X0) is false, set ~iArtichokeTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iHotSpicedBeefTopping(X0) | ~iChickenTopping(X0) is false, set ~iHotSpicedBeefTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPeperoniSausageTopping(X0) | ~iHotSpicedBeefTopping(X0) is false, set ~iHotSpicedBeefTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iHotSpicedBeefTopping(X0) | ~iHamTopping(X0) is false, set ~iHotSpicedBeefTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iOnionTopping(X0) | ~iArtichokeTopping(X0) is false, set ~iArtichokeTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSpinachTopping(X0) | ~iArtichokeTopping(X0) is false, set ~iArtichokeTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPepperTopping(X0) | ~iArtichokeTopping(X0) is false, set ~iArtichokeTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iSundriedTomatoTopping(X0) is false, set ~iSundriedTomatoTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMild(sK146(X0)) | ~iSundriedTomatoTopping(X0) is false, set ~iSundriedTomatoTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK146(X0)) | ~iSundriedTomatoTopping(X0) is false, set ~iSundriedTomatoTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iTomatoTopping(X0) | ~iSundriedTomatoTopping(X0) is false, set ~iSundriedTomatoTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSundriedTomatoTopping(X0) | ~iSlicedTomatoTopping(X0) is false, set ~iSundriedTomatoTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK60(X0)) | ~iGoatsCheeseTopping(X0) is false, set ~iGoatsCheeseTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iGoatsCheeseTopping(X0) is false, set ~iGoatsCheeseTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMild(sK60(X0)) | ~iGoatsCheeseTopping(X0) is false, set ~iGoatsCheeseTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iCheeseTopping(X0) | ~iGoatsCheeseTopping(X0) is false, set ~iGoatsCheeseTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFourCheesesTopping(X0) | ~iGoatsCheeseTopping(X0) is false, set ~iGoatsCheeseTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iGoatsCheeseTopping(X0) | ~iMozzarellaTopping(X0) is false, set ~iGoatsCheeseTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iParmesanTopping(X0) | ~iGoatsCheeseTopping(X0) is false, set ~iGoatsCheeseTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iGoatsCheeseTopping(X0) | ~iGorgonzolaTopping(X0) is false, set ~iGoatsCheeseTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iAsparagusTopping(X0) is false, set ~iAsparagusTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK11(X0)) | ~iAsparagusTopping(X0) is false, set ~iAsparagusTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMild(sK11(X0)) | ~iAsparagusTopping(X0) is false, set ~iAsparagusTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iVegetableTopping(X0) | ~iAsparagusTopping(X0) is false, set ~iAsparagusTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPetitPoisTopping(X0) | ~iAsparagusTopping(X0) is false, set ~iAsparagusTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAsparagusTopping(X0) | ~iArtichokeTopping(X0) is false, set ~iAsparagusTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iMushroomTopping(X0) | ~iAsparagusTopping(X0) is false, set ~iAsparagusTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCaperTopping(X0) | ~iAsparagusTopping(X0) is false, set ~iAsparagusTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iNonVegetarianPizza(X0) is false, set ~iNonVegetarianPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iVegetarianPizza(X0) | ~iNonVegetarianPizza(X0) is false, set ~iNonVegetarianPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iNonVegetarianPizza(X0) | ~iVegetarianPizza(X0) is false, set ~iNonVegetarianPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPizza(X0) | ~iNonVegetarianPizza(X0) is false, set ~iNonVegetarianPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iNonVegetarianPizza(X0) is false, set ~iNonVegetarianPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasCountryOfOrigin(X0,iItaly) | ~iRealItalianPizza(X0) is false, set ~iRealItalianPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPizza(X0) | ~iRealItalianPizza(X0) is false, set ~iRealItalianPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPizza(X0) | ~iSpicyPizza(X0) is false, set ~iSpicyPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPizza(X0) | ~iSpicyPizzaEquivalent(X0) is false, set ~iSpicyPizzaEquivalent(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPizza(X0) | ~iInterestingPizza(X0) is false, set ~iInterestingPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPizza(X0) | ~iMeatyPizza(X0) is false, set ~iMeatyPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPizza(X0) | ~iCheeseyPizza(X0) is false, set ~iCheeseyPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iParmaHamTopping(X0) is false, set ~iParmaHamTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMild(sK91(X0)) | ~iParmaHamTopping(X0) is false, set ~iParmaHamTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasSpiciness(X0,sK91(X0)) | ~iParmaHamTopping(X0) is false, set ~iParmaHamTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK13(X0)) | ~iCajun(X0) is false, set ~iCajun(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPeperonataTopping(sK12(X0)) | ~iCajun(X0) is false, set ~iCajun(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK12(X0)) | ~iCajun(X0) is false, set ~iCajun(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iParmense(X0) is false, set ~iParmense(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMozzarellaTopping(sK92(X0)) | ~iParmense(X0) is false, set ~iParmense(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK92(X0)) | ~iParmense(X0) is false, set ~iParmense(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iHamTopping(X0) | ~iParmaHamTopping(X0) is false, set ~iParmaHamTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iParmesanTopping(sK93(X0)) | ~iParmense(X0) is false, set ~iParmense(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK93(X0)) | ~iParmense(X0) is false, set ~iParmense(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK94(X0)) | ~iParmense(X0) is false, set ~iParmense(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iHamTopping(sK94(X0)) | ~iParmense(X0) is false, set ~iParmense(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iCheeseTopping(X0) | ~iCheeseyVegetableTopping(X0) is false, set ~iCheeseyVegetableTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iCheeseyVegetableTopping(X0) is false, set ~iCheeseyVegetableTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK14(X0)) | ~iCajun(X0) is false, set ~iCajun(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK95(X0)) | ~iParmense(X0) is false, set ~iParmense(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iNamedPizza(X0) | ~iParmense(X0) is false, set ~iParmense(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iParmense(X0) is false, set ~iParmense(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iAsparagusTopping(sK95(X0)) | ~iParmense(X0) is false, set ~iParmense(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iVegetableTopping(X0) | ~iCheeseyVegetableTopping(X0) is false, set ~iCheeseyVegetableTopping(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK96(X0)) | ~iParmense(X0) is false, set ~iParmense(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iParmesanTopping(X1) | iHamTopping(X1) | iMozzarellaTopping(X1) | iTomatoTopping(X1) | iAsparagusTopping(X1) | ~ihasTopping(X0,X1) | ~iParmense(X0) is false, set ~iParmense(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iTomatoTopping(sK96(X0)) | ~iParmense(X0) is false, set ~iParmense(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iNamedPizza(X0) | ~iCajun(X0) is false, set ~iCajun(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMozzarellaTopping(sK14(X0)) | ~iCajun(X0) is false, set ~iCajun(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iTobascoPepperSauce(sK13(X0)) | ~iCajun(X0) is false, set ~iCajun(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iCajun(X0) is false, set ~iCajun(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iNapoletana(X0) | ~iParmense(X0) is false, set ~iParmense(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iOnionTopping(sK15(X0)) | ~iCajun(X0) is false, set ~iCajun(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK15(X0)) | ~iCajun(X0) is false, set ~iCajun(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iOnionTopping(X1) | iPrawnsTopping(X1) | iTobascoPepperSauce(X1) | iMozzarellaTopping(X1) | iPeperonataTopping(X1) | iTomatoTopping(X1) | ~ihasTopping(X0,X1) | ~iCajun(X0) is false, set ~iCajun(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPrawnsTopping(sK16(X0)) | ~iCajun(X0) is false, set ~iCajun(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iTomatoTopping(sK17(X0)) | ~iCajun(X0) is false, set ~iCajun(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK17(X0)) | ~iCajun(X0) is false, set ~iCajun(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK16(X0)) | ~iCajun(X0) is false, set ~iCajun(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iCajun(X0) is false, set ~iCajun(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK103(X0)) | ~iPolloAdAstra(X0) is false, set ~iPolloAdAstra(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMozzarellaTopping(sK102(X0)) | ~iPolloAdAstra(X0) is false, set ~iPolloAdAstra(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK102(X0)) | ~iPolloAdAstra(X0) is false, set ~iPolloAdAstra(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iPolloAdAstra(X0) is false, set ~iPolloAdAstra(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iNamedPizza(X0) | ~iPolloAdAstra(X0) is false, set ~iPolloAdAstra(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iSweetPepperTopping(X1) | iChickenTopping(X1) | iRedOnionTopping(X1) | iMozzarellaTopping(X1) | iGarlicTopping(X1) | iTomatoTopping(X1) | iCajunSpiceTopping(X1) | ~ihasTopping(X0,X1) | ~iPolloAdAstra(X0) is false, set ~iPolloAdAstra(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iPolloAdAstra(X0) is false, set ~iPolloAdAstra(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iCajunSpiceTopping(sK103(X0)) | ~iPolloAdAstra(X0) is false, set ~iPolloAdAstra(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iRedOnionTopping(sK104(X0)) | ~iPolloAdAstra(X0) is false, set ~iPolloAdAstra(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK104(X0)) | ~iPolloAdAstra(X0) is false, set ~iPolloAdAstra(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iGarlicTopping(sK105(X0)) | ~iPolloAdAstra(X0) is false, set ~iPolloAdAstra(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK105(X0)) | ~iPolloAdAstra(X0) is false, set ~iPolloAdAstra(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iTomatoTopping(sK106(X0)) | ~iPolloAdAstra(X0) is false, set ~iPolloAdAstra(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK106(X0)) | ~iPolloAdAstra(X0) is false, set ~iPolloAdAstra(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iChickenTopping(sK107(X0)) | ~iPolloAdAstra(X0) is false, set ~iPolloAdAstra(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK107(X0)) | ~iPolloAdAstra(X0) is false, set ~iPolloAdAstra(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iDeepPanBase(X0) is false, set ~iDeepPanBase(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iSweetPepperTopping(sK108(X0)) | ~iPolloAdAstra(X0) is false, set ~iPolloAdAstra(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK108(X0)) | ~iPolloAdAstra(X0) is false, set ~iPolloAdAstra(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iDeepPanBase(X0) | ~iThinAndCrispyBase(X0) is false, set ~iDeepPanBase(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPizzaBase(X0) | ~iDeepPanBase(X0) is false, set ~iDeepPanBase(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iNapoletana(X0) | ~iCajun(X0) is false, set ~iCajun(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPolloAdAstra(X0) | ~iParmense(X0) is false, set ~iPolloAdAstra(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iParmense(X0) | ~iCajun(X0) is false, set ~iCajun(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMozzarellaTopping(sK2(X0)) | ~iAmerican(X0) is false, set ~iAmerican(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK2(X0)) | ~iAmerican(X0) is false, set ~iAmerican(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iFiorentina(X0) is false, set ~iFiorentina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMozzarellaTopping(sK33(X0)) | ~iFiorentina(X0) is false, set ~iFiorentina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK33(X0)) | ~iFiorentina(X0) is false, set ~iFiorentina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iParmesanTopping(X1) | iOliveTopping(X1) | iMozzarellaTopping(X1) | iGarlicTopping(X1) | iSpinachTopping(X1) | iTomatoTopping(X1) | ~ihasTopping(X0,X1) | ~iFiorentina(X0) is false, set ~iFiorentina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iFiorentina(X0) is false, set ~iFiorentina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK34(X0)) | ~iFiorentina(X0) is false, set ~iFiorentina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iParmesanTopping(sK34(X0)) | ~iFiorentina(X0) is false, set ~iFiorentina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iOliveTopping(sK35(X0)) | ~iFiorentina(X0) is false, set ~iFiorentina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK35(X0)) | ~iFiorentina(X0) is false, set ~iFiorentina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iPrinceCarlo(X0) is false, set ~iPrinceCarlo(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iNamedPizza(X0) | ~iFiorentina(X0) is false, set ~iFiorentina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK109(X0)) | ~iPrinceCarlo(X0) is false, set ~iPrinceCarlo(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMozzarellaTopping(sK109(X0)) | ~iPrinceCarlo(X0) is false, set ~iPrinceCarlo(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK36(X0)) | ~iFiorentina(X0) is false, set ~iFiorentina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iNamedPizza(X0) | ~iPrinceCarlo(X0) is false, set ~iPrinceCarlo(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK110(X0)) | ~iPrinceCarlo(X0) is false, set ~iPrinceCarlo(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iGarlicTopping(sK36(X0)) | ~iFiorentina(X0) is false, set ~iFiorentina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iParmesanTopping(sK110(X0)) | ~iPrinceCarlo(X0) is false, set ~iPrinceCarlo(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK111(X0)) | ~iPrinceCarlo(X0) is false, set ~iPrinceCarlo(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK37(X0)) | ~iFiorentina(X0) is false, set ~iFiorentina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iRosemaryTopping(sK111(X0)) | ~iPrinceCarlo(X0) is false, set ~iPrinceCarlo(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK112(X0)) | ~iPrinceCarlo(X0) is false, set ~iPrinceCarlo(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iSpinachTopping(sK37(X0)) | ~iFiorentina(X0) is false, set ~iFiorentina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iLeekTopping(sK112(X0)) | ~iPrinceCarlo(X0) is false, set ~iPrinceCarlo(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iPrinceCarlo(X0) is false, set ~iPrinceCarlo(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK38(X0)) | ~iFiorentina(X0) is false, set ~iFiorentina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPeperoniSausageTopping(X1) | iJalapenoPepperTopping(X1) | iMozzarellaTopping(X1) | iHotGreenPepperTopping(X1) | iTomatoTopping(X1) | ~ihasTopping(X0,X1) | ~iAmericanHot(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iAmericanHot(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iAmericanHot(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK113(X0)) | ~iPrinceCarlo(X0) is false, set ~iPrinceCarlo(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iParmesanTopping(X1) | iRosemaryTopping(X1) | iMozzarellaTopping(X1) | iTomatoTopping(X1) | iLeekTopping(X1) | ~ihasTopping(X0,X1) | ~iPrinceCarlo(X0) is false, set ~iPrinceCarlo(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iTomatoTopping(sK113(X0)) | ~iPrinceCarlo(X0) is false, set ~iPrinceCarlo(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iTomatoTopping(sK38(X0)) | ~iFiorentina(X0) is false, set ~iFiorentina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPolloAdAstra(X0) | ~iPrinceCarlo(X0) is false, set ~iPrinceCarlo(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPolloAdAstra(X0) | ~iCajun(X0) is false, set ~iCajun(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPrinceCarlo(X0) | ~iCajun(X0) is false, set ~iPrinceCarlo(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPolloAdAstra(X0) | ~iFiorentina(X0) is false, set ~iFiorentina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iNapoletana(X0) | ~iPrinceCarlo(X0) is false, set ~iPrinceCarlo(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMozzarellaTopping(sK5(X0)) | ~iAmericanHot(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iParmense(X0) | ~iPrinceCarlo(X0) is false, set ~iPrinceCarlo(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFiorentina(X0) | ~iCajun(X0) is false, set ~iFiorentina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iNapoletana(X0) | ~iFiorentina(X0) is false, set ~iFiorentina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iQuattroFormaggi(X0) is false, set ~iQuattroFormaggi(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK114(X0)) | ~iQuattroFormaggi(X0) is false, set ~iQuattroFormaggi(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iParmense(X0) | ~iFiorentina(X0) is false, set ~iFiorentina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK6(X0)) | ~iAmericanHot(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iNamedPizza(X0) | ~iAmericanHot(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK5(X0)) | ~iAmericanHot(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iAmerican(X0) is false, set ~iAmerican(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iNamedPizza(X0) | ~iQuattroFormaggi(X0) is false, set ~iQuattroFormaggi(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iFourCheesesTopping(sK114(X0)) | ~iQuattroFormaggi(X0) is false, set ~iQuattroFormaggi(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iFourCheesesTopping(X1) | iTomatoTopping(X1) | ~ihasTopping(X0,X1) | ~iQuattroFormaggi(X0) is false, set ~iQuattroFormaggi(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iQuattroFormaggi(X0) is false, set ~iQuattroFormaggi(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFiorentina(X0) | ~iPrinceCarlo(X0) is false, set ~iFiorentina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iTomatoTopping(sK115(X0)) | ~iQuattroFormaggi(X0) is false, set ~iQuattroFormaggi(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK115(X0)) | ~iQuattroFormaggi(X0) is false, set ~iQuattroFormaggi(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iNapoletana(X0) | ~iQuattroFormaggi(X0) is false, set ~iQuattroFormaggi(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iParmense(X0) | ~iQuattroFormaggi(X0) is false, set ~iQuattroFormaggi(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iQuattroFormaggi(X0) | ~iPrinceCarlo(X0) is false, set ~iQuattroFormaggi(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iQuattroFormaggi(X0) | ~iFiorentina(X0) is false, set ~iQuattroFormaggi(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmerican(X0) | ~iFiorentina(X0) is false, set ~iFiorentina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasCountryOfOrigin(X0,iAmerica) | ~iAmericanHot(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPolloAdAstra(X0) | ~iQuattroFormaggi(X0) is false, set ~iQuattroFormaggi(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iQuattroFormaggi(X0) | ~iCajun(X0) is false, set ~iQuattroFormaggi(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iHotGreenPepperTopping(sK7(X0)) | ~iAmericanHot(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK7(X0)) | ~iAmericanHot(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPeperoniSausageTopping(sK6(X0)) | ~iAmericanHot(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iTomatoTopping(sK8(X0)) | ~iAmericanHot(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK8(X0)) | ~iAmericanHot(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iGorgonzolaTopping(sK117(X0)) | ~iRosa(X0) is false, set ~iRosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK117(X0)) | ~iRosa(X0) is false, set ~iRosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iRosa(X0) is false, set ~iRosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMozzarellaTopping(sK118(X0)) | ~iRosa(X0) is false, set ~iRosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iRosa(X0) is false, set ~iRosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iNamedPizza(X0) | ~iRosa(X0) is false, set ~iRosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK118(X0)) | ~iRosa(X0) is false, set ~iRosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK119(X0)) | ~iRosa(X0) is false, set ~iRosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPolloAdAstra(X0) | ~iRosa(X0) is false, set ~iRosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iTomatoTopping(sK119(X0)) | ~iRosa(X0) is false, set ~iRosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iGorgonzolaTopping(X1) | iMozzarellaTopping(X1) | iTomatoTopping(X1) | ~ihasTopping(X0,X1) | ~iRosa(X0) is false, set ~iRosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iJalapenoPepperTopping(sK9(X0)) | ~iAmericanHot(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK9(X0)) | ~iAmericanHot(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK3(X0)) | ~iAmerican(X0) is false, set ~iAmerican(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPeperoniSausageTopping(X1) | iMozzarellaTopping(X1) | iTomatoTopping(X1) | ~ihasTopping(X0,X1) | ~iAmerican(X0) is false, set ~iAmerican(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iNamedPizza(X0) | ~iAmerican(X0) is false, set ~iAmerican(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iAmerican(X0) is false, set ~iAmerican(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCajun(X0) | ~iRosa(X0) is false, set ~iRosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iNapoletana(X0) | ~iRosa(X0) is false, set ~iRosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iParmense(X0) | ~iRosa(X0) is false, set ~iRosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPrinceCarlo(X0) | ~iRosa(X0) is false, set ~iRosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFiorentina(X0) | ~iRosa(X0) is false, set ~iRosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iQuattroFormaggi(X0) | ~iRosa(X0) is false, set ~iRosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmericanHot(X0) | ~iQuattroFormaggi(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK121(X0)) | ~iSiciliana(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iHamTopping(X1) | iAnchoviesTopping(X1) | iOliveTopping(X1) | iMozzarellaTopping(X1) | iGarlicTopping(X1) | iTomatoTopping(X1) | iArtichokeTopping(X1) | ~ihasTopping(X0,X1) | ~iSiciliana(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iSiciliana(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK122(X0)) | ~iSiciliana(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK123(X0)) | ~iSiciliana(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iArtichokeTopping(sK122(X0)) | ~iSiciliana(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMozzarellaTopping(sK121(X0)) | ~iSiciliana(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iSiciliana(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iNamedPizza(X0) | ~iSiciliana(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iOliveTopping(sK124(X0)) | ~iSiciliana(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK124(X0)) | ~iSiciliana(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iGarlicTopping(sK125(X0)) | ~iSiciliana(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iTomatoTopping(sK126(X0)) | ~iSiciliana(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK126(X0)) | ~iSiciliana(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK125(X0)) | ~iSiciliana(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iHamTopping(sK123(X0)) | ~iSiciliana(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iAnchoviesTopping(sK127(X0)) | ~iSiciliana(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSiciliana(X0) | ~iCajun(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK127(X0)) | ~iSiciliana(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSiciliana(X0) | ~iRosa(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iNapoletana(X0) | ~iSiciliana(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPeperoniSausageTopping(X1) | iAnchoviesTopping(X1) | iOliveTopping(X1) | iMozzarellaTopping(X1) | iCaperTopping(X1) | iTomatoTopping(X1) | iMushroomTopping(X1) | ~ihasTopping(X0,X1) | ~iFourSeasons(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iFourSeasons(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iFourSeasons(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iParmense(X0) | ~iSiciliana(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPolloAdAstra(X0) | ~iSiciliana(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSiciliana(X0) | ~iPrinceCarlo(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iCaperTopping(sK41(X0)) | ~iFourSeasons(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK41(X0)) | ~iFourSeasons(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMozzarellaTopping(sK42(X0)) | ~iFourSeasons(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK42(X0)) | ~iFourSeasons(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmericanHot(X0) | ~iPolloAdAstra(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSiciliana(X0) | ~iFiorentina(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMushroomTopping(sK43(X0)) | ~iFourSeasons(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSiciliana(X0) | ~iQuattroFormaggi(X0) is false, set ~iSiciliana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK44(X0)) | ~iFourSeasons(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iNamedPizza(X0) | ~iFourSeasons(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK43(X0)) | ~iFourSeasons(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK129(X0)) | ~iSloppyGiuseppe(X0) is false, set ~iSloppyGiuseppe(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iSloppyGiuseppe(X0) is false, set ~iSloppyGiuseppe(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK130(X0)) | ~iSloppyGiuseppe(X0) is false, set ~iSloppyGiuseppe(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iGreenPepperTopping(sK129(X0)) | ~iSloppyGiuseppe(X0) is false, set ~iSloppyGiuseppe(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK45(X0)) | ~iFourSeasons(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iNamedPizza(X0) | ~iSloppyGiuseppe(X0) is false, set ~iSloppyGiuseppe(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMozzarellaTopping(sK130(X0)) | ~iSloppyGiuseppe(X0) is false, set ~iSloppyGiuseppe(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK131(X0)) | ~iSloppyGiuseppe(X0) is false, set ~iSloppyGiuseppe(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iOnionTopping(sK131(X0)) | ~iSloppyGiuseppe(X0) is false, set ~iSloppyGiuseppe(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK46(X0)) | ~iFourSeasons(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPeperoniSausageTopping(sK45(X0)) | ~iFourSeasons(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iOliveTopping(sK44(X0)) | ~iFourSeasons(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmericanHot(X0) | ~iSiciliana(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iHotSpicedBeefTopping(sK132(X0)) | ~iSloppyGiuseppe(X0) is false, set ~iSloppyGiuseppe(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK132(X0)) | ~iSloppyGiuseppe(X0) is false, set ~iSloppyGiuseppe(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iOnionTopping(X1) | iHotSpicedBeefTopping(X1) | iGreenPepperTopping(X1) | iMozzarellaTopping(X1) | iTomatoTopping(X1) | ~ihasTopping(X0,X1) | ~iSloppyGiuseppe(X0) is false, set ~iSloppyGiuseppe(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iSloppyGiuseppe(X0) is false, set ~iSloppyGiuseppe(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK47(X0)) | ~iFourSeasons(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iTomatoTopping(sK133(X0)) | ~iSloppyGiuseppe(X0) is false, set ~iSloppyGiuseppe(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK133(X0)) | ~iSloppyGiuseppe(X0) is false, set ~iSloppyGiuseppe(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSloppyGiuseppe(X0) | ~iRosa(X0) is false, set ~iSloppyGiuseppe(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iTomatoTopping(sK47(X0)) | ~iFourSeasons(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iAnchoviesTopping(sK46(X0)) | ~iFourSeasons(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSloppyGiuseppe(X0) | ~iParmense(X0) is false, set ~iSloppyGiuseppe(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFourSeasons(X0) | ~iAmericanHot(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSloppyGiuseppe(X0) | ~iPrinceCarlo(X0) is false, set ~iSloppyGiuseppe(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFourSeasons(X0) | ~iQuattroFormaggi(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmericanHot(X0) | ~iFiorentina(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmericanHot(X0) | ~iCajun(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSloppyGiuseppe(X0) | ~iFiorentina(X0) is false, set ~iSloppyGiuseppe(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFourSeasons(X0) | ~iSloppyGiuseppe(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSloppyGiuseppe(X0) | ~iSiciliana(X0) is false, set ~iSloppyGiuseppe(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmericanHot(X0) | ~iSloppyGiuseppe(X0) is false, set ~iSloppyGiuseppe(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFourSeasons(X0) | ~iSiciliana(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFourSeasons(X0) | ~iPolloAdAstra(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSloppyGiuseppe(X0) | ~iCajun(X0) is false, set ~iSloppyGiuseppe(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSloppyGiuseppe(X0) | ~iQuattroFormaggi(X0) is false, set ~iSloppyGiuseppe(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPolloAdAstra(X0) | ~iSloppyGiuseppe(X0) is false, set ~iSloppyGiuseppe(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFourSeasons(X0) | ~iRosa(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFourSeasons(X0) | ~iCajun(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK134(X0)) | ~iSoho(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iSoho(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMozzarellaTopping(sK134(X0)) | ~iSoho(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK135(X0)) | ~iSoho(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFourSeasons(X0) | ~iNapoletana(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmericanHot(X0) | ~iRosa(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK136(X0)) | ~iSoho(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iOliveTopping(sK135(X0)) | ~iSoho(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iNamedPizza(X0) | ~iSoho(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iParmesanTopping(sK136(X0)) | ~iSoho(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFourSeasons(X0) | ~iParmense(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iGarlicTopping(sK137(X0)) | ~iSoho(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK137(X0)) | ~iSoho(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iSoho(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iParmesanTopping(X1) | iOliveTopping(X1) | iMozzarellaTopping(X1) | iGarlicTopping(X1) | iTomatoTopping(X1) | iRocketTopping(X1) | ~ihasTopping(X0,X1) | ~iSoho(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFourSeasons(X0) | ~iPrinceCarlo(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iTomatoTopping(sK138(X0)) | ~iSoho(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK138(X0)) | ~iSoho(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK139(X0)) | ~iSoho(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iRocketTopping(sK139(X0)) | ~iSoho(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSoho(X0) | ~iParmense(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSoho(X0) | ~iPrinceCarlo(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmericanHot(X0) | ~iNapoletana(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iTomatoTopping(sK4(X0)) | ~iAmerican(X0) is false, set ~iAmerican(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK4(X0)) | ~iAmerican(X0) is false, set ~iAmerican(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasCountryOfOrigin(X0,iAmerica) | ~iAmerican(X0) is false, set ~iAmerican(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFourSeasons(X0) | ~iSoho(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmericanHot(X0) | ~iSoho(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSoho(X0) | ~iQuattroFormaggi(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSoho(X0) | ~iFiorentina(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFourSeasons(X0) | ~iFiorentina(X0) is false, set ~iFourSeasons(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSloppyGiuseppe(X0) | ~iSoho(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPolloAdAstra(X0) | ~iSoho(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSoho(X0) | ~iCajun(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSoho(X0) | ~iRosa(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSoho(X0) | ~iSiciliana(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iNapoletana(X0) | ~iSoho(X0) is false, set ~iSoho(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmericanHot(X0) | ~iPrinceCarlo(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmericanHot(X0) | ~iParmense(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMozzarellaTopping(sK151(X0)) | ~iUnclosedPizza(X0) is false, set ~iUnclosedPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iNamedPizza(X0) | ~iUnclosedPizza(X0) is false, set ~iUnclosedPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK151(X0)) | ~iUnclosedPizza(X0) is false, set ~iUnclosedPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iUnclosedPizza(X0) is false, set ~iUnclosedPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmericanHot(X0) | ~iAmerican(X0) is false, set ~iAmericanHot(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iUnclosedPizza(X0) | ~iPolloAdAstra(X0) is false, set ~iUnclosedPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iUnclosedPizza(X0) | ~iQuattroFormaggi(X0) is false, set ~iUnclosedPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iUnclosedPizza(X0) | ~iCajun(X0) is false, set ~iUnclosedPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iUnclosedPizza(X0) | ~iSiciliana(X0) is false, set ~iUnclosedPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iUnclosedPizza(X0) | ~iSloppyGiuseppe(X0) is false, set ~iUnclosedPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iUnclosedPizza(X0) | ~iSoho(X0) is false, set ~iUnclosedPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iUnclosedPizza(X0) | ~iNapoletana(X0) is false, set ~iUnclosedPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iUnclosedPizza(X0) | ~iRosa(X0) is false, set ~iUnclosedPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iUnclosedPizza(X0) | ~iParmense(X0) is false, set ~iUnclosedPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iUnclosedPizza(X0) | ~iPrinceCarlo(X0) is false, set ~iUnclosedPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMixedSeafoodTopping(sK48(X0)) | ~iFruttiDiMare(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK48(X0)) | ~iFruttiDiMare(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iNamedPizza(X0) | ~iFruttiDiMare(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iFruttiDiMare(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmerican(X0) | ~iSoho(X0) is false, set ~iAmerican(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iUnclosedPizza(X0) | ~iFourSeasons(X0) is false, set ~iUnclosedPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iUnclosedPizza(X0) | ~iFiorentina(X0) is false, set ~iUnclosedPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iUnclosedPizza(X0) | ~iAmericanHot(X0) is false, set ~iUnclosedPizza(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iTomatoTopping(sK50(X0)) | ~iFruttiDiMare(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK50(X0)) | ~iFruttiDiMare(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iGarlicTopping(sK49(X0)) | ~iFruttiDiMare(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iGarlicTopping(X1) | iTomatoTopping(X1) | iMixedSeafoodTopping(X1) | ~ihasTopping(X0,X1) | ~iFruttiDiMare(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFruttiDiMare(X0) | ~iPolloAdAstra(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iFruttiDiMare(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK49(X0)) | ~iFruttiDiMare(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iVeneziana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPineKernels(sK156(X0)) | ~iVeneziana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK156(X0)) | ~iVeneziana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iCaperTopping(sK157(X0)) | ~iVeneziana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK157(X0)) | ~iVeneziana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK158(X0)) | ~iVeneziana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMozzarellaTopping(sK158(X0)) | ~iVeneziana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFruttiDiMare(X0) | ~iCajun(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFruttiDiMare(X0) | ~iSiciliana(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFruttiDiMare(X0) | ~iSloppyGiuseppe(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK159(X0)) | ~iVeneziana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iNamedPizza(X0) | ~iVeneziana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iOliveTopping(sK159(X0)) | ~iVeneziana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasCountryOfOrigin(X0,iItaly) | ~iVeneziana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFruttiDiMare(X0) | ~iRosa(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK160(X0)) | ~iVeneziana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iOnionTopping(sK160(X0)) | ~iVeneziana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFruttiDiMare(X0) | ~iNapoletana(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK161(X0)) | ~iVeneziana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iSultanaTopping(sK161(X0)) | ~iVeneziana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFruttiDiMare(X0) | ~iParmense(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK20(X0)) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iHamTopping(X1) | iAnchoviesTopping(X1) | iOliveTopping(X1) | iMozzarellaTopping(X1) | iPeperonataTopping(X1) | iCaperTopping(X1) | iTomatoTopping(X1) | ~ihasTopping(X0,X1) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iTomatoTopping(sK162(X0)) | ~iVeneziana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK162(X0)) | ~iVeneziana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iVeneziana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iOnionTopping(X1) | iSultanaTopping(X1) | iPineKernels(X1) | iOliveTopping(X1) | iMozzarellaTopping(X1) | iCaperTopping(X1) | iTomatoTopping(X1) | ~ihasTopping(X0,X1) | ~iVeneziana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFruttiDiMare(X0) | ~iPrinceCarlo(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iVeneziana(X0) | ~iCajun(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iVeneziana(X0) | ~iSiciliana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iVeneziana(X0) | ~iRosa(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFruttiDiMare(X0) | ~iUnclosedPizza(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK21(X0)) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iVeneziana(X0) | ~iNapoletana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iVeneziana(X0) | ~iPolloAdAstra(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFruttiDiMare(X0) | ~iVeneziana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iVeneziana(X0) | ~iParmense(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFourSeasons(X0) | ~iFruttiDiMare(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iVeneziana(X0) | ~iPrinceCarlo(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFruttiDiMare(X0) | ~iQuattroFormaggi(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iVeneziana(X0) | ~iSloppyGiuseppe(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iVeneziana(X0) | ~iUnclosedPizza(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK22(X0)) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iCaperTopping(sK21(X0)) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPeperonataTopping(sK20(X0)) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFourSeasons(X0) | ~iVeneziana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmericanHot(X0) | ~iFruttiDiMare(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFruttiDiMare(X0) | ~iFiorentina(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmericanHot(X0) | ~iVeneziana(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iVeneziana(X0) | ~iFiorentina(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iVeneziana(X0) | ~iSoho(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFruttiDiMare(X0) | ~iSoho(X0) is false, set ~iFruttiDiMare(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK23(X0)) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iVeneziana(X0) | ~iQuattroFormaggi(X0) is false, set ~iVeneziana(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iNamedPizza(X0) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iHamTopping(sK23(X0)) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMozzarellaTopping(sK22(X0)) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmerican(X0) | ~iQuattroFormaggi(X0) is false, set ~iAmerican(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPeperoniSausageTopping(sK3(X0)) | ~iAmerican(X0) is false, set ~iAmerican(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPetitPoisTopping(X1) | iSlicedTomatoTopping(X1) | iOliveTopping(X1) | iMozzarellaTopping(X1) | iPeperonataTopping(X1) | iTomatoTopping(X1) | iMushroomTopping(X1) | iLeekTopping(X1) | ~ihasTopping(X0,X1) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iTomatoTopping(sK25(X0)) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK25(X0)) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPeperonataTopping(sK52(X0)) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK52(X0)) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iPetitPoisTopping(sK53(X0)) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK53(X0)) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iAnchoviesTopping(sK26(X0)) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMozzarellaTopping(sK54(X0)) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK54(X0)) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK55(X0)) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iSlicedTomatoTopping(sK55(X0)) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPolloAdAstra(X0) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK26(X0)) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iOliveTopping(sK24(X0)) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK56(X0)) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK57(X0)) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMushroomTopping(sK56(X0)) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iNamedPizza(X0) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK58(X0)) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iOliveTopping(sK57(X0)) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iLeekTopping(sK58(X0)) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK59(X0)) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCajun(X0) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSiciliana(X0) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iVeneziana(X0) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iGiardiniera(X0) | ~iCapricciosa(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iTomatoTopping(sK59(X0)) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iGiardiniera(X0) | ~iCajun(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iNapoletana(X0) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iParmense(X0) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFruttiDiMare(X0) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iGiardiniera(X0) | ~iPrinceCarlo(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iParmense(X0) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFruttiDiMare(X0) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iRosa(X0) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSloppyGiuseppe(X0) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK24(X0)) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFourSeasons(X0) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmerican(X0) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iUnclosedPizza(X0) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iGiardiniera(X0) | ~iFiorentina(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmericanHot(X0) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iUnclosedPizza(X0) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPrinceCarlo(X0) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iGiardiniera(X0) | ~iQuattroFormaggi(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSoho(X0) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPolloAdAstra(X0) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iGiardiniera(X0) | ~iRosa(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFourSeasons(X0) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iVeneziana(X0) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSloppyGiuseppe(X0) | ~iGiardiniera(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iGiardiniera(X0) | ~iSiciliana(X0) is false, set ~iGiardiniera(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFiorentina(X0) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iQuattroFormaggi(X0) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSoho(X0) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmericanHot(X0) | ~iCapricciosa(X0) is false, set ~iCapricciosa(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmerican(X0) | ~iSiciliana(X0) is false, set ~iAmerican(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iVeneziana(X0) | ~iAmerican(X0) is false, set ~iAmerican(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iSloppyGiuseppe(X0) | ~iAmerican(X0) is false, set ~iAmerican(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmerican(X0) | ~iRosa(X0) is false, set ~iAmerican(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iSundriedTomatoTopping(sK27(X0)) | ~iCaprina(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK27(X0)) | ~iCaprina(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iGoatsCheeseTopping(sK28(X0)) | ~iCaprina(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMozzarellaTopping(sK29(X0)) | ~iCaprina(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK29(X0)) | ~iCaprina(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK28(X0)) | ~iCaprina(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iCaprina(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iGoatsCheeseTopping(X1) | iSundriedTomatoTopping(X1) | iMozzarellaTopping(X1) | iTomatoTopping(X1) | ~ihasTopping(X0,X1) | ~iCaprina(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK30(X0)) | ~iCaprina(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iNamedPizza(X0) | ~iCaprina(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iCaprina(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iIceCream(X0) is false, set ~iIceCream(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iFruitTopping(sK64(X0)) | ~iIceCream(X0) is false, set ~iIceCream(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK64(X0)) | ~iIceCream(X0) is false, set ~iIceCream(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iIceCream(X0) | ~iPizza(X0) is false, set ~iIceCream(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iFood(X0) | ~iIceCream(X0) is false, set ~iIceCream(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iIceCream(X0) | ~iPizzaTopping(X0) is false, set ~iIceCream(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iIceCream(X0) | ~iPizzaBase(X0) is false, set ~iIceCream(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCaprina(X0) | ~iQuattroFormaggi(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCaprina(X0) | ~iSoho(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iTomatoTopping(sK30(X0)) | ~iCaprina(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iNapoletana(X0) | ~iAmerican(X0) is false, set ~iAmerican(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmerican(X0) | ~iCapricciosa(X0) is false, set ~iAmerican(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iAmerican(X0) | ~iCajun(X0) is false, set ~iAmerican(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPolloAdAstra(X0) | ~iAmerican(X0) is false, set ~iAmerican(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCaprina(X0) | ~iVeneziana(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCaprina(X0) | ~iSloppyGiuseppe(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCaprina(X0) | ~iPolloAdAstra(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK69(X0)) | ~iLaReine(X0) is false, set ~iLaReine(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iLaReine(X0) is false, set ~iLaReine(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK70(X0)) | ~iLaReine(X0) is false, set ~iLaReine(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMozzarellaTopping(sK69(X0)) | ~iLaReine(X0) is false, set ~iLaReine(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCaprina(X0) | ~iCajun(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iNamedPizza(X0) | ~iLaReine(X0) is false, set ~iLaReine(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iOliveTopping(sK70(X0)) | ~iLaReine(X0) is false, set ~iLaReine(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK71(X0)) | ~iLaReine(X0) is false, set ~iLaReine(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iMushroomTopping(sK71(X0)) | ~iLaReine(X0) is false, set ~iLaReine(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCaprina(X0) | ~iCapricciosa(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCaprina(X0) | ~iRosa(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCaprina(X0) | ~iSiciliana(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCaprina(X0) | ~iGiardiniera(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iHamTopping(sK72(X0)) | ~iLaReine(X0) is false, set ~iLaReine(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iHamTopping(X1) | iOliveTopping(X1) | iMozzarellaTopping(X1) | iTomatoTopping(X1) | iMushroomTopping(X1) | ~ihasTopping(X0,X1) | ~iLaReine(X0) is false, set ~iLaReine(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever abstractDomain(X0) | ~iLaReine(X0) is false, set ~iLaReine(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK72(X0)) | ~iLaReine(X0) is false, set ~iLaReine(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever iTomatoTopping(sK73(X0)) | ~iLaReine(X0) is false, set ~iLaReine(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ihasTopping(X0,sK73(X0)) | ~iLaReine(X0) is false, set ~iLaReine(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iLaReine(X0) | ~iSoho(X0) is false, set ~iLaReine(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iLaReine(X0) | ~iQuattroFormaggi(X0) is false, set ~iLaReine(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCaprina(X0) | ~iParmense(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iFruttiDiMare(X0) | ~iCaprina(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iPolloAdAstra(X0) | ~iLaReine(X0) is false, set ~iLaReine(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iLaReine(X0) | ~iGiardiniera(X0) is false, set ~iLaReine(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iVeneziana(X0) | ~iLaReine(X0) is false, set ~iLaReine(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iLaReine(X0) | ~iSloppyGiuseppe(X0) is false, set ~iLaReine(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iCaprina(X0) | ~iUnclosedPizza(X0) is false, set ~iCaprina(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iLaReine(X0) | ~iCajun(X0) is false, set ~iLaReine(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iLaReine(X0) | ~iSiciliana(X0) is false, set ~iLaReine(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iLaReine(X0) | ~iRosa(X0) is false, set ~iLaReine(X0) to true
% 5.77/1.93 for all groundings,
% 5.77/1.93 whenever ~iLaReine(X0) | ~iCapricciosa(X0) is false, set ~iLaReine(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iFourSeasons(X0) | ~iCaprina(X0) is false, set ~iCaprina(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iCaprina(X0) | ~iPrinceCarlo(X0) is false, set ~iCaprina(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iCaprina(X0) | ~iNapoletana(X0) is false, set ~iCaprina(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iAmerican(X0) | ~iParmense(X0) is false, set ~iAmerican(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iFruttiDiMare(X0) | ~iLaReine(X0) is false, set ~iLaReine(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iLaReine(X0) | ~iPrinceCarlo(X0) is false, set ~iLaReine(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iLaReine(X0) | ~iParmense(X0) is false, set ~iLaReine(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iLaReine(X0) | ~iNapoletana(X0) is false, set ~iLaReine(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iCaprina(X0) | ~iLaReine(X0) is false, set ~iLaReine(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iUnclosedPizza(X0) | ~iLaReine(X0) is false, set ~iLaReine(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iFourSeasons(X0) | ~iLaReine(X0) is false, set ~iLaReine(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iCaprina(X0) | ~iAmericanHot(X0) is false, set ~iCaprina(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iCaprina(X0) | ~iFiorentina(X0) is false, set ~iCaprina(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iAmericanHot(X0) | ~iLaReine(X0) is false, set ~iLaReine(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iLaReine(X0) | ~iFiorentina(X0) is false, set ~iLaReine(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever abstractDomain(X0) | ~iMargherita(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ihasTopping(X0,sK75(X0)) | ~iMargherita(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever iMozzarellaTopping(X1) | iTomatoTopping(X1) | ~ihasTopping(X0,X1) | ~iMargherita(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever abstractDomain(X0) | ~iMargherita(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever iTomatoTopping(sK76(X0)) | ~iMargherita(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ihasTopping(X0,sK76(X0)) | ~iMargherita(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever iNamedPizza(X0) | ~iMargherita(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iMargherita(X0) | ~iSoho(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iMargherita(X0) | ~iGiardiniera(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iMargherita(X0) | ~iQuattroFormaggi(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever iMozzarellaTopping(sK75(X0)) | ~iMargherita(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iVeneziana(X0) | ~iMargherita(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iAmericanHot(X0) | ~iMargherita(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iSloppyGiuseppe(X0) | ~iMargherita(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iMargherita(X0) | ~iCajun(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iMargherita(X0) | ~iCapricciosa(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iMargherita(X0) | ~iRosa(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iMargherita(X0) | ~iSiciliana(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iPolloAdAstra(X0) | ~iMargherita(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iAmerican(X0) | ~iPrinceCarlo(X0) is false, set ~iAmerican(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iLaReine(X0) | ~iAmerican(X0) is false, set ~iAmerican(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iFruttiDiMare(X0) | ~iAmerican(X0) is false, set ~iAmerican(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iLaReine(X0) | ~iMargherita(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iMargherita(X0) | ~iParmense(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iUnclosedPizza(X0) | ~iMargherita(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iCaprina(X0) | ~iMargherita(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iMargherita(X0) | ~iPrinceCarlo(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iFruttiDiMare(X0) | ~iMargherita(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iMargherita(X0) | ~iFiorentina(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever abstractDomain(X0) | ~iMushroom(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever abstractDomain(X0) | ~iMushroom(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iFourSeasons(X0) | ~iMargherita(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iNapoletana(X0) | ~iMargherita(X0) is false, set ~iMargherita(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever iNamedPizza(X0) | ~iMushroom(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever iMozzarellaTopping(sK79(X0)) | ~iMushroom(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ihasTopping(X0,sK79(X0)) | ~iMushroom(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever iMushroomTopping(sK80(X0)) | ~iMushroom(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever iTomatoTopping(sK81(X0)) | ~iMushroom(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ihasTopping(X0,sK81(X0)) | ~iMushroom(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ihasTopping(X0,sK80(X0)) | ~iMushroom(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever iMozzarellaTopping(X1) | iTomatoTopping(X1) | iMushroomTopping(X1) | ~ihasTopping(X0,X1) | ~iMushroom(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iMushroom(X0) | ~iAmerican(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iCaprina(X0) | ~iMushroom(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iUnclosedPizza(X0) | ~iMushroom(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iMargherita(X0) | ~iMushroom(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iAmericanHot(X0) | ~iMushroom(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iMushroom(X0) | ~iFiorentina(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iFourSeasons(X0) | ~iMushroom(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iMushroom(X0) | ~iPrinceCarlo(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iCaprina(X0) | ~iAmerican(X0) is false, set ~iAmerican(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iUnclosedPizza(X0) | ~iAmerican(X0) is false, set ~iAmerican(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iMushroom(X0) | ~iParmense(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iMushroom(X0) | ~iGiardiniera(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iMushroom(X0) | ~iQuattroFormaggi(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iSloppyGiuseppe(X0) | ~iMushroom(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iMushroom(X0) | ~iSiciliana(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iVeneziana(X0) | ~iMushroom(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iPolloAdAstra(X0) | ~iMushroom(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iMushroom(X0) | ~iSoho(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iNapoletana(X0) | ~iMushroom(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iMushroom(X0) | ~iCapricciosa(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iMushroom(X0) | ~iRosa(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iLaReine(X0) | ~iMushroom(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ihasTopping(X0,sK83(X0)) | ~iNapoletana(X0) is false, set ~iNapoletana(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever abstractDomain(X0) | ~iNapoletana(X0) is false, set ~iNapoletana(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iFruttiDiMare(X0) | ~iMushroom(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iMushroom(X0) | ~iCajun(X0) is false, set ~iMushroom(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iFourSeasons(X0) | ~iAmerican(X0) is false, set ~iAmerican(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever abstractDomain(X0) | ~iNapoletana(X0) is false, set ~iNapoletana(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever iMozzarellaTopping(sK84(X0)) | ~iNapoletana(X0) is false, set ~iNapoletana(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ihasTopping(X0,sK84(X0)) | ~iNapoletana(X0) is false, set ~iNapoletana(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ihasTopping(X0,sK85(X0)) | ~iNapoletana(X0) is false, set ~iNapoletana(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever iNamedPizza(X0) | ~iNapoletana(X0) is false, set ~iNapoletana(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever iOliveTopping(sK85(X0)) | ~iNapoletana(X0) is false, set ~iNapoletana(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever iAnchoviesTopping(X1) | iOliveTopping(X1) | iMozzarellaTopping(X1) | iCaperTopping(X1) | iTomatoTopping(X1) | ~ihasTopping(X0,X1) | ~iNapoletana(X0) is false, set ~iNapoletana(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever iCaperTopping(sK83(X0)) | ~iNapoletana(X0) is false, set ~iNapoletana(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ihasTopping(X0,sK87(X0)) | ~iNapoletana(X0) is false, set ~iNapoletana(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever iAnchoviesTopping(sK86(X0)) | ~iNapoletana(X0) is false, set ~iNapoletana(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ihasTopping(X0,sK86(X0)) | ~iNapoletana(X0) is false, set ~iNapoletana(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iNapoletana(X0) | ~iGiardiniera(X0) is false, set ~iNapoletana(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iSloppyGiuseppe(X0) | ~iNapoletana(X0) is false, set ~iNapoletana(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iPolloAdAstra(X0) | ~iNapoletana(X0) is false, set ~iNapoletana(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever iTomatoTopping(sK87(X0)) | ~iNapoletana(X0) is false, set ~iNapoletana(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ihasCountryOfOrigin(X0,iItaly) | ~iNapoletana(X0) is false, set ~iNapoletana(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iMargherita(X0) | ~iAmerican(X0) is false, set ~iAmerican(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever dataDomain(X0) | ~xsd_integer(X0) is false, set ~xsd_integer(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~xsd_string(X0) | ~xsd_integer(X0) | ~dataDomain(X0) is false, set ~xsd_string(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever dataDomain(X0) | ~xsd_string(X0) is false, set ~xsd_string(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever ~iowlNothing(X0) is false, set ~iowlNothing(X0) to true
% 8.06/2.11 for all groundings,
% 8.06/2.11 whenever abstractDomain(X0) | ~iowlNothing(X0) is false, set ~iowlNothing(X0) to true
% 8.06/2.11 % SZS output end Definitions and Model Updates.
% 8.06/2.11 % (1398515)------------------------------
% 8.06/2.11 % (1398515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.06/2.11 % (1398515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.06/2.11 % (1398515)CaDiCaL version: 2.1.3
% 8.06/2.11 % (1398515)Termination reason: Satisfiable
% 8.06/2.11 % (1398515)Time elapsed: 0.660 s
% 8.06/2.11 % (1398515)Peak memory usage: 132 MB
% 8.06/2.11 % (1398515)Instructions burned: 993 (million)
% 8.06/2.11 % (1398515)------------------------------
% 8.06/2.11 % (1398515)------------------------------
% 8.06/2.11 % (1398509)Success in time 1.074 s
% 8.06/2.11 % Vampire exiting
%------------------------------------------------------------------------------