%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWB036+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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:51 PM UTC 2026
% Result : Satisfiable 0.07s 0.37s
% Output : Saturation 0.07s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1866,axiom,
iItaly != iGermany ).
cnf(u1751,axiom,
( ~ iPizza(X0)
| iPizzaBase(sK4(X0)) ) ).
cnf(u1761,axiom,
( ~ iHot(X0)
| iSpiciness(X0) ) ).
cnf(u1818,axiom,
( ~ iisBaseOf(X0,X1)
| X1 = X2
| ~ iisBaseOf(X0,X2) ) ).
cnf(u1844,axiom,
iCountry(iGermany) ).
cnf(u1878,axiom,
( ~ iMeatTopping(X1)
| ~ ihasTopping(X0,X1)
| iMeatyPizza(X0) ) ).
cnf(u1738,axiom,
( ~ iInterestingPizza(X0)
| abstractDomain(X0) ) ).
cnf(u1764,axiom,
( ~ iSpicyPizza(X0)
| abstractDomain(X0) ) ).
cnf(u1733,axiom,
( ~ iFishTopping(X0)
| iPizzaTopping(X0) ) ).
cnf(u1837,axiom,
( ~ ihasTopping(X1,X0)
| iisToppingOf(X0,X1) ) ).
cnf(u1823,axiom,
( ~ ihasBase(X1,X0)
| iisBaseOf(X0,X1) ) ).
cnf(u1874,axiom,
( ~ iPizza(X0)
| ~ abstractDomain(X0)
| ihasTopping(X0,sK6(X0))
| sP0(X0)
| ihasTopping(X0,sK7(X0)) ) ).
cnf(u1833,axiom,
( ~ iisToppingOf(X0,X1)
| X1 = X2
| ~ iisToppingOf(X0,X2) ) ).
cnf(u1717,axiom,
dataDomain(sK2) ).
cnf(u1786,axiom,
( ~ iPizza(X0)
| iVegetarianPizzaEquivalent1(X0)
| ~ abstractDomain(X0)
| ihasTopping(X0,sK8(X0)) ) ).
cnf(u1718,axiom,
( ~ dataDomain(X0)
| ~ abstractDomain(X0) ) ).
cnf(u1821,axiom,
( ~ iisBaseOf(X0,X1)
| iPizza(X1) ) ).
cnf(u1879,axiom,
( ~ ihasTopping(X0,X1)
| iInterestingPizza(X0)
| ~ ihasTopping(X0,X2)
| ~ ihasTopping(X0,X3)
| X1 = X2
| X1 = X3
| X2 = X3 ) ).
cnf(u1759,axiom,
( ~ iSpiciness(X0)
| iHot(X0)
| iMild(X0)
| iMedium(X0) ) ).
cnf(u1773,axiom,
( ~ iVegetarianPizza(X0)
| abstractDomain(X0) ) ).
cnf(u1830,axiom,
( ~ ihasIngredient(X1,X0)
| iisIngredientOf(X0,X1) ) ).
cnf(u1886,axiom,
abstractDomain(iItaly) ).
cnf(u1817,axiom,
( ~ iisBaseOf(X0,X1)
| abstractDomain(X0) ) ).
cnf(u1826,axiom,
( ~ iisIngredientOf(X0,X1)
| iisIngredientOf(X0,X2)
| ~ iisIngredientOf(X1,X2) ) ).
cnf(u1788,axiom,
( ~ iPizza(X0)
| iVegetarianPizzaEquivalent2(X0)
| ~ abstractDomain(X0)
| ihasTopping(X0,sK9(X0)) ) ).
cnf(u1728,axiom,
( ~ iDomainConcept(X0)
| iCountry(X0)
| iFrance != X0 ) ).
cnf(u1861,axiom,
iAmerica != iEngland ).
cnf(u1746,axiom,
( ~ iMild(X0)
| abstractDomain(X0) ) ).
cnf(u1812,axiom,
( ~ ihasTopping(X0,X1)
| iPizza(X0) ) ).
cnf(u1819,axiom,
( ~ iisBaseOf(X1,X0)
| X1 = X2
| ~ iisBaseOf(X2,X0) ) ).
cnf(u1845,axiom,
iowlThing(iGermany) ).
cnf(u1831,axiom,
( ~ iisToppingOf(X0,X1)
| abstractDomain(X1) ) ).
cnf(u1887,axiom,
abstractDomain(iGermany) ).
cnf(u1755,axiom,
( ~ iPizzaBase(X0)
| iFood(X0) ) ).
cnf(u1820,axiom,
( ~ iisBaseOf(X0,X1)
| iPizzaBase(X0) ) ).
cnf(u1838,axiom,
iCountry(iAmerica) ).
cnf(u1816,axiom,
( ~ iisBaseOf(X0,X1)
| abstractDomain(X1) ) ).
cnf(u1795,axiom,
( ~ ihasBase(X0,X1)
| iPizzaBase(X1) ) ).
cnf(u1740,axiom,
( ~ iMeatTopping(X0)
| abstractDomain(X0) ) ).
cnf(u1758,axiom,
( ~ iSpiciness(X0)
| abstractDomain(X0) ) ).
cnf(u1736,axiom,
( ~ iHot(X0)
| abstractDomain(X0) ) ).
cnf(u1890,axiom,
iDomainConcept(iAmerica) ).
cnf(u1792,axiom,
( ~ ihasBase(X0,X1)
| X1 = X2
| ~ ihasBase(X0,X2) ) ).
cnf(u1827,axiom,
( ~ iisIngredientOf(X0,X1)
| iFood(X0) ) ).
cnf(u1720,axiom,
( ~ abstractDomain(X0)
| iowlThing(X0) ) ).
cnf(u1857,axiom,
( ~ iisToppingOf(X0,X1)
| iisIngredientOf(X0,X1) ) ).
cnf(u1735,axiom,
( ~ iFood(X0)
| iDomainConcept(X0) ) ).
cnf(u1776,axiom,
( ~ sP0(X0)
| iPizza(X0) ) ).
cnf(u1802,axiom,
( ~ ihasIngredient(X0,X1)
| iFood(X1) ) ).
cnf(u1766,axiom,
( ~ iSpicyPizzaEquivalent(X0)
| abstractDomain(X0) ) ).
cnf(u1800,axiom,
( ~ ihasIngredient(X0,X1)
| ihasIngredient(X0,X2)
| ~ ihasIngredient(X1,X2) ) ).
cnf(u1884,axiom,
abstractDomain(iAmerica) ).
cnf(u1785,axiom,
( ~ iVegetarianPizzaEquivalent1(X0)
| abstractDomain(X0) ) ).
cnf(u1807,axiom,
( ~ ihasSpiciness(X0,X1)
| X1 = X2
| ~ ihasSpiciness(X0,X2) ) ).
cnf(u1721,axiom,
( ~ iCountry(X0)
| abstractDomain(X0) ) ).
cnf(u1880,axiom,
( ~ iHot(X2)
| ~ ihasTopping(X0,X1)
| ~ ihasSpiciness(X1,X2)
| iSpicyPizzaEquivalent(X0) ) ).
cnf(u1748,axiom,
( ~ iNonVegetarianPizza(X0)
| abstractDomain(X0) ) ).
cnf(u1731,axiom,
( ~ iFishTopping(X0)
| iMild(sK3(X0)) ) ).
cnf(u1724,axiom,
( ~ iDomainConcept(X0)
| iCountry(X0)
| iAmerica != X0 ) ).
cnf(u1757,axiom,
( ~ iPizzaTopping(X0)
| iFood(X0) ) ).
cnf(u1891,axiom,
iDomainConcept(iFrance) ).
cnf(u1784,axiom,
( ~ sP0(X0)
| iVegetarianPizza(X0) ) ).
cnf(u1810,axiom,
( ~ ihasTopping(X0,X1)
| abstractDomain(X0) ) ).
cnf(u1727,axiom,
( ~ iDomainConcept(X0)
| iCountry(X0)
| iItaly != X0 ) ).
cnf(u1809,axiom,
( ~ ihasTopping(X0,X1)
| abstractDomain(X1) ) ).
cnf(u1834,axiom,
( ~ iisToppingOf(X0,X1)
| iPizzaTopping(X0) ) ).
cnf(u1730,axiom,
( ~ iFishTopping(X0)
| abstractDomain(X0) ) ).
cnf(u1805,axiom,
( ~ ihasSpiciness(X0,X1)
| abstractDomain(X1) ) ).
cnf(u1783,axiom,
( ~ iVegetarianPizza(X0)
| sP0(X0) ) ).
cnf(u1863,axiom,
iGermany != iEngland ).
cnf(u1829,axiom,
( ~ iisIngredientOf(X0,X1)
| ihasIngredient(X1,X0) ) ).
cnf(u1850,axiom,
( ~ iPizzaBase(X0)
| ~ iPizzaTopping(X0) ) ).
cnf(u1870,axiom,
iFrance != iItaly ).
cnf(u1801,axiom,
( ~ ihasIngredient(X0,X1)
| iFood(X0) ) ).
cnf(u1885,axiom,
abstractDomain(iFrance) ).
cnf(u1770,axiom,
( ~ iThinAndCrispyPizza(X0)
| abstractDomain(X0) ) ).
cnf(u1722,axiom,
( ~ iCountry(X0)
| iItaly = X0
| iGermany = X0
| iEngland = X0
| iAmerica = X0
| iFrance = X0 ) ).
cnf(u1881,axiom,
~ abstractDomain(sK2) ).
cnf(u1777,axiom,
( ~ sP0(X0)
| ~ iMeatTopping(X3)
| ~ ihasTopping(X0,X3) ) ).
cnf(u1822,axiom,
( ~ iisBaseOf(X0,X1)
| ihasBase(X1,X0) ) ).
cnf(u1855,axiom,
( ~ iPizzaBase(X0)
| ~ iPizza(X0) ) ).
cnf(u1723,axiom,
( ~ iCountry(X0)
| iDomainConcept(X0) ) ).
cnf(u1798,axiom,
( ~ ihasIngredient(X0,X1)
| abstractDomain(X1) ) ).
cnf(u1742,axiom,
( ~ iMeatyPizza(X0)
| abstractDomain(X0) ) ).
cnf(u1856,axiom,
( ~ iPizza(X0)
| ~ iPizzaTopping(X0) ) ).
cnf(u1769,axiom,
( ~ iPizzaTopping(X0)
| ~ ihasSpiciness(X0,X1)
| ~ iHot(X1)
| iSpicyTopping(X0) ) ).
cnf(u1793,axiom,
( ~ ihasBase(X1,X0)
| X1 = X2
| ~ ihasBase(X2,X0) ) ).
cnf(u1794,axiom,
( ~ ihasBase(X0,X1)
| iPizza(X0) ) ).
cnf(u1791,axiom,
( ~ ihasBase(X0,X1)
| abstractDomain(X0) ) ).
cnf(u1840,axiom,
iCountry(iEngland) ).
cnf(u1774,axiom,
( ~ sP0(X0)
| ~ iFishTopping(X4)
| ~ ihasTopping(X0,X4) ) ).
cnf(u1867,axiom,
iAmerica != iFrance ).
cnf(u1760,axiom,
( ~ iMild(X0)
| iSpiciness(X0) ) ).
cnf(u1893,axiom,
iDomainConcept(iGermany) ).
cnf(u1806,axiom,
( ~ ihasSpiciness(X0,X1)
| abstractDomain(X0) ) ).
cnf(u1851,axiom,
( ~ iHot(X0)
| ~ iMild(X0) ) ).
cnf(u1860,axiom,
( ~ ihasTopping(X0,X1)
| ihasIngredient(X0,X1) ) ).
cnf(u1873,axiom,
( ~ iPizza(X0)
| ~ abstractDomain(X0)
| ihasTopping(X0,sK6(X0))
| sP0(X0)
| iFishTopping(sK7(X0)) ) ).
cnf(u1868,axiom,
iFrance != iEngland ).
cnf(u1750,axiom,
( ~ iPizza(X0)
| abstractDomain(X0) ) ).
cnf(u1864,axiom,
iAmerica != iItaly ).
cnf(u1787,axiom,
( ~ iVegetarianPizzaEquivalent2(X0)
| abstractDomain(X0) ) ).
cnf(u1852,axiom,
( ~ iMeatTopping(X0)
| ~ iFishTopping(X0) ) ).
cnf(u1848,axiom,
( ~ iMedium(X0)
| ~ iMild(X0) ) ).
cnf(u1871,axiom,
( ~ iPizza(X0)
| ~ abstractDomain(X0)
| iMeatTopping(sK6(X0))
| sP0(X0)
| iFishTopping(sK7(X0)) ) ).
cnf(u1772,axiom,
( ~ iValuePartition(X0)
| abstractDomain(X0) ) ).
cnf(u1741,axiom,
( ~ iMeatTopping(X0)
| iPizzaTopping(X0) ) ).
cnf(u1790,axiom,
( ~ ihasBase(X0,X1)
| abstractDomain(X1) ) ).
cnf(u1768,axiom,
( ~ iSpicyTopping(X0)
| abstractDomain(X0) ) ).
cnf(u1841,axiom,
iowlThing(iEngland) ).
cnf(u1729,axiom,
( ~ iDomainConcept(X0)
| abstractDomain(X0) ) ).
cnf(u1894,axiom,
iDomainConcept(iEngland) ).
cnf(u1808,axiom,
( ~ ihasSpiciness(X0,X1)
| iSpiciness(X1) ) ).
cnf(u1732,axiom,
( ~ iFishTopping(X0)
| ihasSpiciness(X0,sK3(X0)) ) ).
cnf(u1876,axiom,
( ~ iSpicyTopping(X1)
| ~ ihasTopping(X0,X1)
| iSpicyPizza(X0) ) ).
cnf(u1813,axiom,
( ~ ihasTopping(X0,X1)
| iPizzaTopping(X1) ) ).
cnf(u1799,axiom,
( ~ ihasIngredient(X0,X1)
| abstractDomain(X0) ) ).
cnf(u1828,axiom,
( ~ iisIngredientOf(X0,X1)
| iFood(X1) ) ).
cnf(u1775,axiom,
( ~ sP0(X0)
| abstractDomain(X0) ) ).
cnf(u1869,axiom,
iFrance != iGermany ).
cnf(u1754,axiom,
( ~ iPizzaBase(X0)
| abstractDomain(X0) ) ).
cnf(u1865,axiom,
iItaly != iEngland ).
cnf(u1853,axiom,
( ~ iValuePartition(X0)
| ~ iDomainConcept(X0) ) ).
cnf(u1839,axiom,
iowlThing(iAmerica) ).
cnf(u1883,axiom,
iowlThing(sK1) ).
cnf(u1849,axiom,
( ~ iVegetarianPizza(X0)
| ~ iNonVegetarianPizza(X0) ) ).
cnf(u1716,axiom,
abstractDomain(sK1) ).
cnf(u1862,axiom,
iAmerica != iGermany ).
cnf(u1763,axiom,
( ~ iSpiciness(X0)
| iValuePartition(X0) ) ).
cnf(u1858,axiom,
( ~ iisBaseOf(X0,X1)
| iisIngredientOf(X0,X1) ) ).
cnf(u1789,axiom,
( ~ iowlThing(X0)
| abstractDomain(X0) ) ).
cnf(u1846,axiom,
iCountry(iItaly) ).
cnf(u1824,axiom,
( ~ iisIngredientOf(X0,X1)
| abstractDomain(X1) ) ).
cnf(u1842,axiom,
iCountry(iFrance) ).
cnf(u1744,axiom,
( ~ iMedium(X0)
| abstractDomain(X0) ) ).
cnf(u1877,axiom,
( ~ iPizza(X0)
| iVegetarianPizza(X0)
| iNonVegetarianPizza(X0) ) ).
cnf(u1762,axiom,
( ~ iMedium(X0)
| iSpiciness(X0) ) ).
cnf(u1872,axiom,
( ~ iPizza(X0)
| ~ abstractDomain(X0)
| iMeatTopping(sK6(X0))
| sP0(X0)
| ihasTopping(X0,sK7(X0)) ) ).
cnf(u1835,axiom,
( ~ iisToppingOf(X0,X1)
| iPizza(X1) ) ).
cnf(u1847,axiom,
iowlThing(iItaly) ).
cnf(u1715,axiom,
( dataDomain(X0)
| abstractDomain(X0) ) ).
cnf(u1811,axiom,
( ~ ihasTopping(X1,X0)
| X1 = X2
| ~ ihasTopping(X2,X0) ) ).
cnf(u1892,axiom,
iDomainConcept(iItaly) ).
cnf(u1734,axiom,
( ~ iFood(X0)
| abstractDomain(X0) ) ).
cnf(u1726,axiom,
( ~ iDomainConcept(X0)
| iCountry(X0)
| iGermany != X0 ) ).
cnf(u1771,axiom,
( ~ iPizza(X0)
| iThinAndCrispyPizza(X0)
| ~ abstractDomain(X0)
| ihasBase(X0,sK5(X0)) ) ).
cnf(u1836,axiom,
( ~ iisToppingOf(X0,X1)
| ihasTopping(X1,X0) ) ).
cnf(u1753,axiom,
( ~ iPizza(X0)
| iFood(X0) ) ).
cnf(u1854,axiom,
( ~ iMedium(X0)
| ~ iHot(X0) ) ).
cnf(u1832,axiom,
( ~ iisToppingOf(X0,X1)
| abstractDomain(X0) ) ).
cnf(u1725,axiom,
( ~ iDomainConcept(X0)
| iCountry(X0)
| iEngland != X0 ) ).
cnf(u1756,axiom,
( ~ iPizzaTopping(X0)
| abstractDomain(X0) ) ).
cnf(u1859,axiom,
( ~ ihasBase(X0,X1)
| ihasIngredient(X0,X1) ) ).
cnf(u1888,axiom,
abstractDomain(iEngland) ).
cnf(u1825,axiom,
( ~ iisIngredientOf(X0,X1)
| abstractDomain(X0) ) ).
cnf(u1843,axiom,
iowlThing(iFrance) ).
cnf(u1752,axiom,
( ~ iPizza(X0)
| ihasBase(X0,sK4(X0)) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWB036+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.03/0.31 % Computer : n012.cluster.edu
% 0.03/0.31 % Model : x86_64 x86_64
% 0.03/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.31 % Memory : 8046.5625MB
% 0.03/0.31 % OS : Linux 6.8.0-71-generic
% 0.03/0.31 % CPULimit : 300
% 0.03/0.31 % WCLimit : 300
% 0.03/0.31 % DateTime : Mon Sep 28 07:10:19 UTC 2026
% 0.03/0.31 % CPUTime :
% 0.03/0.31 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.33 Running first-order model finding
% 0.07/0.33 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.37 % (3206824)Will run a generic schedule for satisfiability detection.
% 0.07/0.37 % (3206830)% WARNING: option uhcvi not known.
% 0.07/0.37 % (3206829)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1847553116_2999 on theBenchmark for (2999ds/0Mi)
% 0.07/0.37 % (3206830)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3148436630:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.07/0.37 % (3206832)dis+10_1_sil=32000:sp=arity:random_seed=925802522:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.07/0.37 % (3206831)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3872117312:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.07/0.37 % (3206833)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2072928859:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.07/0.37 % (3206834)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=310638483:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.07/0.37 % (3206835)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1940214743:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.07/0.37 % Detected minimum model sizes of [5]
% 0.07/0.37 % Detected maximum model sizes of [max]
% 0.07/0.37 % TRYING [5]
% 0.07/0.37 % (3206834) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3206824-3206834"...
% 0.07/0.37 % TRYING [6]
% 0.07/0.37 % (3206834)...printing done.
% 0.07/0.37 % (3206831) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3206824-3206831"...
% 0.07/0.37 % SZS status Satisfiable for theBenchmark
% 0.07/0.37 % SZS output start Saturation.
% See solution above
% 0.07/0.37 % SZS output start Definitions and Model Updates.
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iowlNothing(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define xsd_string(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define xsd_integer(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iVegetarianTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iVegetableTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iTomatoTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iCheeseyPizza(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iCheeseTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iThinAndCrispyBase(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iRealItalianPizza(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define ihasCountryOfOrigin(X0,X1) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iMozzarellaTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iPeperoniSausageTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iNamedPizza(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iAmerican(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iPepperTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iGreenPepperTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iHotGreenPepperTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iJalapenoPepperTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iAmericanHot(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iPeperonataTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iSauceTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iTobascoPepperSauce(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iPrawnsTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iOnionTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iCajun(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iAnchoviesTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iHamTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iCaperTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iOliveTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iCapricciosa(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iGoatsCheeseTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iSundriedTomatoTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iCaprina(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iCheeseyVegetableTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iDeepPanBase(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iSpinachTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iParmesanTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iGarlicTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iFiorentina(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iMushroomTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iFourSeasons(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iMixedSeafoodTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iFruttiDiMare(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iSlicedTomatoTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iPetitPoisTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iLeekTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iGiardiniera(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iFruitTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iIceCream(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iLaReine(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iMargherita(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iMushroom(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iNapoletana(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iParmaHamTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iAsparagusTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iParmense(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iHerbSpiceTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iCajunSpiceTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iRedOnionTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iChickenTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iSweetPepperTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iPolloAdAstra(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iRosemaryTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iPrinceCarlo(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iFourCheesesTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iQuattroFormaggi(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iGorgonzolaTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iRosa(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iArtichokeTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iSiciliana(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iHotSpicedBeefTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iSloppyGiuseppe(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iRocketTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iSoho(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iUnclosedPizza(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iNutTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iPineKernels(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iSultanaTopping(X0) := $false
% 0.07/0.37 for all inputs,
% 0.07/0.37 define iVeneziana(X0) := $false
% 0.07/0.37 for all groundings,
% 0.07/0.37 whenever iPizza(X0) & ? [X1] : (ihasTopping(X0,X1) & iCheeseTopping(X1)) is false, set ~iCheeseyPizza(X0) to true
% 0.07/0.37 for all groundings,
% 0.07/0.37 whenever iPizza(X0) & ? [X1,X2,X3] : (ihasTopping(X0,X1) & ihasTopping(X0,X2) & ihasTopping(X0,X3) & X1 != X2 & X1 != X3 & X2 != X3) is false, set ~iInterestingPizza(X0) to true
% 0.07/0.37 for all groundings,
% 0.07/0.37 whenever iPizza(X0) & ? [X1] : (ihasTopping(X0,X1) & iMeatTopping(X1)) is false, set ~iMeatyPizza(X0) to true
% 0.07/0.37 for all groundings,
% 0.07/0.37 whenever abstractDomain(X0) & ~iVegetarianPizza(X0) & iPizza(X0) is false, set ~iNonVegetarianPizza(X0) to true
% 0.07/0.37 for all groundings,
% 0.07/0.37 whenever ihasCountryOfOrigin(X0,iItaly) & iPizza(X0) is false, set ~iRealItalianPizza(X0) to true
% 0.07/0.37 for all groundings,
% 0.07/0.37 whenever ? [X1] : (ihasSpiciness(X0,X1) & iHot(X1)) & iPizzaTopping(X0) is false, set ~iSpicyTopping(X0) to true
% 0.07/0.37 for all groundings,
% 0.07/0.37 whenever ? [X1] : (ihasTopping(X0,X1) & iSpicyTopping(X1)) & iPizza(X0) is false, set ~iSpicyPizza(X0) to true
% 0.07/0.37 for all groundings,
% 0.07/0.37 whenever iPizza(X0) & ? [X1] : (ihasTopping(X0,X1) & ? [X2] : (ihasSpiciness(X1,X2) & iHot(X2)) & iPizzaTopping(X1)) is false, set ~iSpicyPizzaEquivalent(X0) to true
% 0.07/0.37 for all groundings,
% 0.07/0.37 whenever iPizza(X0) & abstractDomain(X0) & ! [X1] : (ihasBase(X0,X1) => iThinAndCrispyBase(X1)) is false, set ~iThinAndCrispyPizza(X0) to true
% 0.07/0.37 for all groundings,
% 0.07/0.37 whenever (iCheeseTopping(X0) | iNutTopping(X0) | iHerbSpiceTopping(X0) | iVegetableTopping(X0) | iSauceTopping(X0) | iFruitTopping(X0)) & iPizzaTopping(X0) is false, set ~iVegetarianTopping(X0) to true
% 0.07/0.37 for all groundings,
% 0.07/0.37 whenever iPizza(X0) & abstractDomain(X0) & ! [X1] : (ihasTopping(X0,X1) => iVegetarianTopping(X1)) is false, set ~iVegetarianPizzaEquivalent1(X0) to true
% 0.07/0.37 for all groundings,
% 0.07/0.37 whenever iPizza(X0) & abstractDomain(X0) & ! [X1] : (ihasTopping(X0,X1) => (iCheeseTopping(X1) | iNutTopping(X1) | iHerbSpiceTopping(X1) | iVegetableTopping(X1) | iSauceTopping(X1) | iFruitTopping(X1))) is false, set ~iVegetarianPizzaEquivalent2(X0) to true
% 0.07/0.37 % SZS output end Definitions and Model Updates.
% 0.07/0.37 % (3206834)------------------------------
% 0.07/0.37 % (3206834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.07/0.37 % (3206834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.07/0.37 % (3206834)CaDiCaL version: 2.1.3
% 0.07/0.37 % (3206834)Termination reason: Satisfiable
% 0.07/0.37 % (3206834)Time elapsed: 0.005 s
% 0.07/0.37 % (3206834)Peak memory usage: 13 MB
% 0.07/0.37 % (3206834)Instructions burned: 12 (million)
% 0.07/0.37 % (3206824)Success in time 0.035 s
% 0.07/0.37 % Vampire exiting
%------------------------------------------------------------------------------