%------------------------------------------------------------------------------
% File : Refute---2015
% Problem : SWB036+1 : TPTP v6.4.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : isabelle tptp_refute %d %s
% Computer : n114.star.cs.uiowa.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory : 32218.75MB
% OS : Linux 3.10.0-327.10.1.el7.x86_64
% CPULimit : 300s
% DateTime : Thu Apr 14 04:36:03 EDT 2016
% Result : Timeout 300.10s
% Output : None
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB036+1 : TPTP v6.4.0. Released v5.2.0.
% 0.00/0.04 % Command : isabelle tptp_refute %d %s
% 0.02/0.23 % Computer : n114.star.cs.uiowa.edu
% 0.02/0.23 % Model : x86_64 x86_64
% 0.02/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.02/0.23 % Memory : 32218.75MB
% 0.02/0.23 % OS : Linux 3.10.0-327.10.1.el7.x86_64
% 0.02/0.23 % CPULimit : 300
% 0.02/0.23 % DateTime : Fri Apr 8 05:24:09 CDT 2016
% 0.02/0.23 % CPUTime :
% 6.30/5.85 > val it = (): unit
% 7.02/6.52 Trying to find a model that refutes: True
% 16.52/16.05 Unfolded term: [| ((((((((~ bnd_iFrance = bnd_iItaly & ~ bnd_iFrance = bnd_iGermany) &
% 16.52/16.05 ~ bnd_iFrance = bnd_iEngland) &
% 16.52/16.05 ~ bnd_iFrance = bnd_iAmerica) &
% 16.52/16.05 ~ bnd_iItaly = bnd_iGermany) &
% 16.52/16.05 ~ bnd_iItaly = bnd_iEngland) &
% 16.52/16.05 ~ bnd_iItaly = bnd_iAmerica) &
% 16.52/16.05 ~ bnd_iGermany = bnd_iEngland) &
% 16.52/16.05 ~ bnd_iGermany = bnd_iAmerica) &
% 16.52/16.05 ~ bnd_iEngland = bnd_iAmerica;
% 16.52/16.05 ALL X Y. bnd_ihasTopping X Y --> bnd_ihasIngredient X Y;
% 16.52/16.05 ALL X Y. bnd_ihasBase X Y --> bnd_ihasIngredient X Y;
% 16.52/16.05 ALL X Y. bnd_iisBaseOf X Y --> bnd_iisIngredientOf X Y;
% 16.52/16.05 ALL X Y. bnd_iisToppingOf X Y --> bnd_iisIngredientOf X Y;
% 16.52/16.05 ALL X. ~ (bnd_iOliveTopping X & bnd_iMushroomTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iPepperTopping X & bnd_iAsparagusTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iAmericanHot X & bnd_iAmerican X);
% 16.52/16.05 ALL X. ~ (bnd_iGiardiniera X & bnd_iSiciliana X);
% 16.52/16.05 ALL X. ~ (bnd_iFourCheesesTopping X & bnd_iParmesanTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iMargherita X & bnd_iFiorentina X);
% 16.52/16.05 ALL X. ~ (bnd_iCaprina X & bnd_iAmericanHot X);
% 16.52/16.05 ALL X. ~ (bnd_iPepperTopping X & bnd_iArtichokeTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iVeneziana X & bnd_iGiardiniera X);
% 16.52/16.05 ALL X. ~ (bnd_iUnclosedPizza X & bnd_iAmericanHot X);
% 16.52/16.05 ALL X. ~ (bnd_iPolloAdAstra X & bnd_iSloppyGiuseppe X);
% 16.52/16.05 ALL X. ~ (bnd_iQuattroFormaggi X & bnd_iCapricciosa X);
% 16.52/16.05 ALL X. ~ (bnd_iPetitPoisTopping X & bnd_iPepperTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iCheeseTopping X & bnd_iFruitTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iMeatTopping X & bnd_iNutTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iOnionTopping X & bnd_iAsparagusTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iRocketTopping X & bnd_iAsparagusTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iFourSeasons X & bnd_iFiorentina X);
% 16.52/16.05 ALL X. ~ (bnd_iQuattroFormaggi X & bnd_iRosa X);
% 16.52/16.05 ALL X. ~ (bnd_iFourSeasons X & bnd_iMargherita X);
% 16.52/16.05 ALL X. ~ (bnd_iAmericanHot X & bnd_iPrinceCarlo X);
% 16.52/16.05 ALL X. ~ (bnd_iSpinachTopping X & bnd_iArtichokeTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iFruttiDiMare X & bnd_iSoho X);
% 16.52/16.05 ALL X. ~ (bnd_iPetitPoisTopping X & bnd_iSpinachTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iGoatsCheeseTopping X & bnd_iGorgonzolaTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iSloppyGiuseppe X & bnd_iGiardiniera X);
% 16.52/16.05 ALL X. ~ (bnd_iAmerican X & bnd_iFiorentina X);
% 16.52/16.05 ALL X. ~ (bnd_iMargherita X & bnd_iAmerican X);
% 16.52/16.05 ALL X. ~ (bnd_iGreenPepperTopping X & bnd_iPeperonataTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iSloppyGiuseppe X & bnd_iCajun X);
% 16.52/16.05 ALL X. ~ (bnd_iAmericanHot X & bnd_iLaReine X);
% 16.52/16.05 ALL X. ~ (bnd_iCaprina X & bnd_iFiorentina X);
% 16.52/16.05 ALL X. ~ (bnd_iUnclosedPizza X & bnd_iFiorentina X);
% 16.52/16.05 ALL X. ~ (bnd_iPolloAdAstra X & bnd_iGiardiniera X);
% 16.52/16.05 ALL X. ~ (bnd_iCaprina X & bnd_iMargherita X);
% 16.52/16.05 ALL X. ~ (bnd_iUnclosedPizza X & bnd_iMargherita X);
% 16.52/16.05 ALL X. ~ (bnd_iNapoletana X & bnd_iSoho X);
% 16.52/16.05 ALL X. ~ (bnd_iQuattroFormaggi X & bnd_iCajun X);
% 16.52/16.05 ALL X. ~ (bnd_iFourSeasons X & bnd_iAmerican X);
% 16.52/16.05 ALL X. ~ (bnd_iSauceTopping X & bnd_iFishTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iAmericanHot X & bnd_iParmense X);
% 16.52/16.05 ALL X. ~ (bnd_iNutTopping X & bnd_iHerbSpiceTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iGarlicTopping X & bnd_iMushroomTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iPepperTopping X & bnd_iSpinachTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iFiorentina X & bnd_iPrinceCarlo X);
% 16.52/16.05 ALL X. ~ (bnd_iFourSeasons X & bnd_iCaprina X);
% 16.52/16.05 ALL X. ~ (bnd_iUnclosedPizza X & bnd_iFourSeasons X);
% 16.52/16.05 ALL X. ~ (bnd_iMargherita X & bnd_iPrinceCarlo X);
% 16.52/16.05 ALL X. ~ (bnd_iSiciliana X & bnd_iQuattroFormaggi X);
% 16.52/16.05 ALL X. ~ (bnd_iPizza X & bnd_iPizzaTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iVeneziana X & bnd_iQuattroFormaggi X);
% 16.52/16.05 ALL X. ~ (bnd_iOnionTopping X & bnd_iArtichokeTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iRocketTopping X & bnd_iArtichokeTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iFourSeasons X & bnd_iPrinceCarlo X);
% 16.52/16.05 ALL X. ~ (bnd_iCaprina X & bnd_iAmerican X);
% 16.52/16.05 ALL X. ~ (bnd_iLaReine X & bnd_iFiorentina X);
% 16.52/16.05 ALL X. ~ (bnd_iSoho X & bnd_iCapricciosa X);
% 16.52/16.05 ALL X. ~ (bnd_iUnclosedPizza X & bnd_iAmerican X);
% 16.52/16.05 ALL X. ~ (bnd_iPetitPoisTopping X & bnd_iOnionTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iPetitPoisTopping X & bnd_iRocketTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iLaReine X & bnd_iMargherita X);
% 16.52/16.05 ALL X. ~ (bnd_iCaprina X & bnd_iUnclosedPizza X);
% 16.52/16.05 ALL X. ~ (bnd_iSoho X & bnd_iRosa X);
% 16.52/16.05 ALL X. ~ (bnd_iParmense X & bnd_iFiorentina X);
% 16.52/16.05 ALL X. ~ (bnd_iLaReine X & bnd_iMushroom X);
% 16.52/16.05 ALL X. ~ (bnd_iMargherita X & bnd_iParmense X);
% 16.52/16.05 ALL X. ~ (bnd_iAmerican X & bnd_iPrinceCarlo X);
% 16.52/16.05 ALL X. ~ (bnd_iHerbSpiceTopping X & bnd_iFruitTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iFourSeasons X & bnd_iLaReine X);
% 16.52/16.05 ALL X. ~ (bnd_iTomatoTopping X & bnd_iAsparagusTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iSloppyGiuseppe X & bnd_iQuattroFormaggi X);
% 16.52/16.05 ALL X. ~ (bnd_iVegetableTopping X & bnd_iSauceTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iCaprina X & bnd_iPrinceCarlo X);
% 16.52/16.05 ALL X. ~ (bnd_iUnclosedPizza X & bnd_iPrinceCarlo X);
% 16.52/16.05 ALL X. ~ (bnd_iFruttiDiMare X & bnd_iMushroom X);
% 16.52/16.05 ALL X. ~ (bnd_iOnionTopping X & bnd_iPepperTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iFourSeasons X & bnd_iParmense X);
% 16.52/16.05 ALL X. ~ (bnd_iPepperTopping X & bnd_iRocketTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iOliveTopping X & bnd_iAsparagusTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iFruitTopping X & bnd_iFishTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iLaReine X & bnd_iAmerican X);
% 16.52/16.05 ALL X. ~ (bnd_iPolloAdAstra X & bnd_iQuattroFormaggi X);
% 16.52/16.05 ALL X. ~ (bnd_iCheeseTopping X & bnd_iNutTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iSoho X & bnd_iCajun X);
% 16.52/16.05 ALL X. ~ (bnd_iCaprina X & bnd_iLaReine X);
% 16.52/16.05 ALL X. ~ (bnd_iUnclosedPizza X & bnd_iLaReine X);
% 16.52/16.05 ALL X. ~ (bnd_iAmerican X & bnd_iParmense X);
% 16.52/16.05 ALL X. ~ (bnd_iNapoletana X & bnd_iMushroom X);
% 16.52/16.05 ALL X. ~ (bnd_iOnionTopping X & bnd_iSpinachTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iSpinachTopping X & bnd_iRocketTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iCaprina X & bnd_iParmense X);
% 16.52/16.05 ALL X. ~ (bnd_iUnclosedPizza X & bnd_iParmense X);
% 16.52/16.05 ALL X. ~ (bnd_iSoho X & bnd_iSiciliana X);
% 16.52/16.05 ALL X. ~ (bnd_iGiardiniera X & bnd_iRosa X);
% 16.52/16.05 ALL X. ~ (bnd_iGiardiniera X & bnd_iQuattroFormaggi X);
% 16.52/16.05 ALL X. ~ (bnd_iLaReine X & bnd_iPrinceCarlo X);
% 16.52/16.05 ALL X. ~ (bnd_iPizza X & bnd_iPizzaBase X);
% 16.52/16.05 ALL X. ~ (bnd_iVeneziana X & bnd_iSoho X);
% 16.52/16.05 ALL X. ~ (bnd_iParmense X & bnd_iPrinceCarlo X);
% 16.52/16.05 ALL X. ~ (bnd_iMushroom X & bnd_iCapricciosa X);
% 16.52/16.05 ALL X. ~ (bnd_iSweetPepperTopping X & bnd_iJalapenoPepperTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iPeperoniSausageTopping X & bnd_iChickenTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iTomatoTopping X & bnd_iArtichokeTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iParmesanTopping X & bnd_iMozzarellaTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iPetitPoisTopping X & bnd_iTomatoTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iMushroom X & bnd_iRosa X);
% 16.52/16.05 ALL X. ~ (bnd_iCaperTopping X & bnd_iLeekTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iLaReine X & bnd_iParmense X);
% 16.52/16.05 ALL X. ~ (bnd_iSloppyGiuseppe X & bnd_iSoho X);
% 16.52/16.05 ALL X. ~ (bnd_iOliveTopping X & bnd_iArtichokeTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iIceCream X & bnd_iPizzaBase X);
% 16.52/16.05 ALL X. ~ (bnd_iGarlicTopping X & bnd_iAsparagusTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iDeepPanBase X & bnd_iThinAndCrispyBase X);
% 16.52/16.05 ALL X. ~ (bnd_iPetitPoisTopping X & bnd_iOliveTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iOnionTopping X & bnd_iRocketTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iPolloAdAstra X & bnd_iSoho X);
% 16.52/16.05 ALL X. ~ (bnd_iPepperTopping X & bnd_iTomatoTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iAmericanHot X & bnd_iFruttiDiMare X);
% 16.52/16.05 ALL X. ~ (bnd_iMushroom X & bnd_iCajun X);
% 16.52/16.05 ALL X. ~ (bnd_iPepperTopping X & bnd_iOliveTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iSoho X & bnd_iGiardiniera X);
% 16.52/16.05 ALL X. ~ (bnd_iMushroom X & bnd_iSiciliana X);
% 16.52/16.05 ALL X. ~ (bnd_iMeatTopping X & bnd_iHerbSpiceTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iParmesanTopping X & bnd_iGoatsCheeseTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iPrawnsTopping X & bnd_iMixedSeafoodTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iSpinachTopping X & bnd_iTomatoTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iAmericanHot X & bnd_iNapoletana X);
% 16.52/16.05 ALL X. ~ (bnd_iNutTopping X & bnd_iFishTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iFourCheesesTopping X & bnd_iMozzarellaTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iVeneziana X & bnd_iMushroom X);
% 16.52/16.05 ALL X. ~ (bnd_iOliveTopping X & bnd_iSpinachTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iFruttiDiMare X & bnd_iFiorentina X);
% 16.52/16.05 ALL X. ~ (bnd_iSauceTopping X & bnd_iFruitTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iGarlicTopping X & bnd_iArtichokeTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iFruttiDiMare X & bnd_iMargherita X);
% 16.52/16.05 ALL X. ~ (bnd_iPetitPoisTopping X & bnd_iGarlicTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iFruttiDiMare X & bnd_iQuattroFormaggi X);
% 16.52/16.05 ALL X. ~ (bnd_iSloppyGiuseppe X & bnd_iMushroom X);
% 16.52/16.05 ALL X. ~ (bnd_iAmericanHot X & bnd_iCapricciosa X);
% 16.52/16.05 ALL X. ~ (bnd_iMushroomTopping X & bnd_iLeekTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iFourSeasons X & bnd_iFruttiDiMare X);
% 16.52/16.05 ALL X. ~ (bnd_iNapoletana X & bnd_iFiorentina X);
% 16.52/16.05 ALL X. ~ (bnd_iPolloAdAstra X & bnd_iCajun X);
% 16.52/16.05 ALL X. ~ (bnd_iAmericanHot X & bnd_iRosa X);
% 16.52/16.05 ALL X. ~ (bnd_iNapoletana X & bnd_iMargherita X);
% 16.52/16.05 ALL X. ~ (bnd_iPolloAdAstra X & bnd_iMushroom X);
% 16.52/16.05 ALL X. ~ (bnd_iOnionTopping X & bnd_iTomatoTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iRocketTopping X & bnd_iTomatoTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iPepperTopping X & bnd_iGarlicTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iFruttiDiMare X & bnd_iAmerican X);
% 16.52/16.05 ALL X. ~ (bnd_iVegetableTopping X & bnd_iFruitTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iFourCheesesTopping X & bnd_iGoatsCheeseTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iFourSeasons X & bnd_iNapoletana X);
% 16.52/16.05 ALL X. ~ (bnd_iCheeseTopping X & bnd_iMeatTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iSloppyGiuseppe X & bnd_iSiciliana X);
% 16.52/16.05 ALL X. ~ (bnd_iOnionTopping X & bnd_iOliveTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iOliveTopping X & bnd_iRocketTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iSoho X & bnd_iQuattroFormaggi X);
% 16.52/16.05 ALL X. ~ (bnd_iMushroom X & bnd_iParmense X);
% 16.52/16.05 ALL X. ~ (bnd_iFruttiDiMare X & bnd_iCaprina X);
% 16.52/16.05 ALL X. ~ (bnd_iFruttiDiMare X & bnd_iUnclosedPizza X);
% 16.52/16.05 ALL X. ~ (bnd_iFiorentina X & bnd_iCapricciosa X);
% 16.52/16.05 ALL X. ~ (bnd_iSweetPepperTopping X & bnd_iGreenPepperTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iMushroom X & bnd_iGiardiniera X);
% 16.52/16.05 ALL X. ~ (bnd_iCaperTopping X & bnd_iMushroomTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iAmericanHot X & bnd_iFiorentina X);
% 16.52/16.05 ALL X. ~ (bnd_iMargherita X & bnd_iCapricciosa X);
% 16.52/16.05 ALL X. ~ (bnd_iHotSpicedBeefTopping X & bnd_iHamTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iGarlicTopping X & bnd_iSpinachTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iAmericanHot X & bnd_iCajun X);
% 16.52/16.05 ALL X. ~ (bnd_iNapoletana X & bnd_iAmerican X);
% 16.52/16.05 ALL X. ~ (bnd_iIceCream X & bnd_iPizzaTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iFiorentina X & bnd_iRosa X);
% 16.52/16.05 ALL X. ~ (bnd_iFruttiDiMare X & bnd_iPrinceCarlo X);
% 16.52/16.05 ALL X. ~ (bnd_iMedium X & bnd_iHot X);
% 16.52/16.05 ALL X. ~ (bnd_iMargherita X & bnd_iRosa X);
% 16.52/16.05 ALL X. ~ (bnd_iCaprina X & bnd_iNapoletana X);
% 16.52/16.05 ALL X. ~ (bnd_iUnclosedPizza X & bnd_iNapoletana X);
% 16.52/16.05 ALL X. ~ (bnd_iFourSeasons X & bnd_iCapricciosa X);
% 16.52/16.05 ALL X. ~ (bnd_iAmericanHot X & bnd_iSiciliana X);
% 16.52/16.05 ALL X. ~ (bnd_iAmericanHot X & bnd_iVeneziana X);
% 16.52/16.05 ALL X. ~ (bnd_iFourSeasons X & bnd_iRosa X);
% 16.52/16.05 ALL X. ~ (bnd_iFruttiDiMare X & bnd_iLaReine X);
% 16.52/16.05 ALL X. ~ (bnd_iCheeseTopping X & bnd_iHerbSpiceTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iNapoletana X & bnd_iPrinceCarlo X);
% 16.52/16.05 ALL X. ~ (bnd_iAmerican X & bnd_iCapricciosa X);
% 16.52/16.05 ALL X. ~ (bnd_iFruttiDiMare X & bnd_iParmense X);
% 16.52/16.05 ALL X. ~ (bnd_iFiorentina X & bnd_iCajun X);
% 16.52/16.05 ALL X. ~ (bnd_iSpinachTopping X & bnd_iAsparagusTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iCaprina X & bnd_iCapricciosa X);
% 16.52/16.05 ALL X. ~ (bnd_iUnclosedPizza X & bnd_iCapricciosa X);
% 16.52/16.05 ALL X. ~ (bnd_iRosemaryTopping X & bnd_iCajunSpiceTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iAmerican X & bnd_iRosa X);
% 16.52/16.05 ALL X. ~ (bnd_iMargherita X & bnd_iCajun X);
% 16.52/16.05 ALL X. ~ (bnd_iLaReine X & bnd_iNapoletana X);
% 16.52/16.05 ALL X. ~ (bnd_iCaprina X & bnd_iRosa X);
% 16.52/16.05 ALL X. ~ (bnd_iAmericanHot X & bnd_iSloppyGiuseppe X);
% 16.52/16.05 ALL X. ~ (bnd_iOnionTopping X & bnd_iGarlicTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iUnclosedPizza X & bnd_iRosa X);
% 16.52/16.05 ALL X. ~ (bnd_iGarlicTopping X & bnd_iRocketTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iNutTopping X & bnd_iSauceTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iSiciliana X & bnd_iFiorentina X);
% 16.52/16.05 ALL X. ~ (bnd_iPrinceCarlo X & bnd_iCapricciosa X);
% 16.52/16.05 ALL X. ~ (bnd_iFourSeasons X & bnd_iCajun X);
% 16.52/16.05 ALL X. ~ (bnd_iMargherita X & bnd_iSiciliana X);
% 16.52/16.05 ALL X. ~ (bnd_iNapoletana X & bnd_iParmense X);
% 16.52/16.05 ALL X. ~ (bnd_iVeneziana X & bnd_iFiorentina X);
% 16.52/16.05 ALL X. ~ (bnd_iMushroom X & bnd_iQuattroFormaggi X);
% 16.52/16.05 ALL X. ~ (bnd_iAmericanHot X & bnd_iPolloAdAstra X);
% 16.52/16.05 ALL X. ~ (bnd_iVeneziana X & bnd_iMargherita X);
% 16.52/16.05 ALL X. ~ (bnd_iPrinceCarlo X & bnd_iRosa X);
% 16.52/16.05 ALL X. ~ (bnd_iFourSeasons X & bnd_iSiciliana X);
% 16.52/16.05 ALL X. ~ (bnd_iOliveTopping X & bnd_iTomatoTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iAmericanHot X & bnd_iMargherita X);
% 16.52/16.05 ALL X. ~ (bnd_iAmerican X & bnd_iCajun X);
% 16.52/16.05 ALL X. ~ (bnd_iLaReine X & bnd_iCapricciosa X);
% 16.52/16.05 ALL X. ~ (bnd_iLeekTopping X & bnd_iAsparagusTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iFourSeasons X & bnd_iVeneziana X);
% 16.52/16.05 ALL X. ~ (bnd_iCaprina X & bnd_iCajun X);
% 16.52/16.05 ALL X. ~ (bnd_iUnclosedPizza X & bnd_iCajun X);
% 16.52/16.05 ALL X. ~ (bnd_iDomainConcept X & bnd_iValuePartition X);
% 16.52/16.05 ALL X. ~ (bnd_iLaReine X & bnd_iRosa X);
% 16.52/16.05 ALL X. ~ (bnd_iNutTopping X & bnd_iVegetableTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iParmense X & bnd_iCapricciosa X);
% 16.52/16.05 ALL X. ~ (bnd_iSloppyGiuseppe X & bnd_iFiorentina X);
% 16.52/16.05 ALL X. ~ (bnd_iMeatTopping X & bnd_iFishTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iAmerican X & bnd_iSiciliana X);
% 16.52/16.05 ALL X. ~ (bnd_iAmericanHot X & bnd_iGiardiniera X);
% 16.52/16.05 ALL X. ~ (bnd_iSloppyGiuseppe X & bnd_iMargherita X);
% 16.52/16.05 ALL X. ~ (bnd_iVeneziana X & bnd_iAmerican X);
% 16.52/16.05 ALL X. ~ (bnd_iCaprina X & bnd_iSiciliana X);
% 16.52/16.05 ALL X. ~ (bnd_iUnclosedPizza X & bnd_iSiciliana X);
% 16.52/16.05 ALL X. ~ (bnd_iParmense X & bnd_iRosa X);
% 16.52/16.05 ALL X. ~ (bnd_iPrinceCarlo X & bnd_iCajun X);
% 16.52/16.05 ALL X. ~ (bnd_iPolloAdAstra X & bnd_iFiorentina X);
% 16.52/16.05 ALL X. ~ (bnd_iCaprina X & bnd_iVeneziana X);
% 16.52/16.05 ALL X. ~ (bnd_iPolloAdAstra X & bnd_iMargherita X);
% 16.52/16.05 ALL X. ~ (bnd_iVeneziana X & bnd_iUnclosedPizza X);
% 16.52/16.05 ALL X. ~ (bnd_iFourSeasons X & bnd_iSloppyGiuseppe X);
% 16.52/16.05 ALL X. ~ (bnd_iVeneziana X & bnd_iSloppyGiuseppe X);
% 16.52/16.05 ALL X. ~ (bnd_iSiciliana X & bnd_iPrinceCarlo X);
% 16.52/16.05 ALL X. ~ (bnd_iChickenTopping X & bnd_iHamTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iCaperTopping X & bnd_iAsparagusTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iLaReine X & bnd_iCajun X);
% 16.52/16.05 ALL X. ~ (bnd_iFourSeasons X & bnd_iPolloAdAstra X);
% 16.52/16.05 ALL X. ~ (bnd_iVeneziana X & bnd_iPrinceCarlo X);
% 16.52/16.05 ALL X. ~ (bnd_iPrawnsTopping X & bnd_iAnchoviesTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iAnchoviesTopping X & bnd_iMixedSeafoodTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iSloppyGiuseppe X & bnd_iAmerican X);
% 16.52/16.05 ALL X. ~ (bnd_iGiardiniera X & bnd_iFiorentina X);
% 16.52/16.05 ALL X. ~ (bnd_iMargherita X & bnd_iGiardiniera X);
% 16.52/16.05 ALL X. ~ (bnd_iParmense X & bnd_iCajun X);
% 16.52/16.05 ALL X. ~ (bnd_iHerbSpiceTopping X & bnd_iFishTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iCaprina X & bnd_iSloppyGiuseppe X);
% 16.52/16.05 ALL X. ~ (bnd_iUnclosedPizza X & bnd_iSloppyGiuseppe X);
% 16.52/16.05 ALL X. ~ (bnd_iLaReine X & bnd_iSiciliana X);
% 16.52/16.05 ALL X. ~ (bnd_iMushroom X & bnd_iSoho X);
% 16.52/16.05 ALL X. ~ (bnd_iGarlicTopping X & bnd_iTomatoTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iPolloAdAstra X & bnd_iAmerican X);
% 16.52/16.05 ALL X. ~ (bnd_iIceCream X & bnd_iPizza X);
% 16.52/16.05 ALL X. ~ (bnd_iArtichokeTopping X & bnd_iLeekTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iVeneziana X & bnd_iLaReine X);
% 16.52/16.05 ALL X. ~ (bnd_iSundriedTomatoTopping X & bnd_iSlicedTomatoTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iPetitPoisTopping X & bnd_iLeekTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iFourSeasons X & bnd_iGiardiniera X);
% 16.52/16.05 ALL X. ~ (bnd_iParmense X & bnd_iSiciliana X);
% 16.52/16.05 ALL X. ~ (bnd_iGoatsCheeseTopping X & bnd_iMozzarellaTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iCaprina X & bnd_iPolloAdAstra X);
% 16.52/16.05 ALL X. ~ (bnd_iUnclosedPizza X & bnd_iPolloAdAstra X);
% 16.52/16.05 ALL X. ~ (bnd_iOliveTopping X & bnd_iGarlicTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iSloppyGiuseppe X & bnd_iPrinceCarlo X);
% 16.52/16.05 ALL X. ~ (bnd_iVeneziana X & bnd_iParmense X);
% 16.52/16.05 ALL X. ~ (bnd_iAmericanHot X & bnd_iQuattroFormaggi X);
% 16.52/16.05 ALL X. ~ (bnd_iAmerican X & bnd_iGiardiniera X);
% 16.52/16.05 ALL X. ~ (bnd_iPolloAdAstra X & bnd_iPrinceCarlo X);
% 16.52/16.05 ALL X. ~ (bnd_iLaReine X & bnd_iSloppyGiuseppe X);
% 16.52/16.05 ALL X. ~ (bnd_iCaprina X & bnd_iGiardiniera X);
% 16.52/16.05 ALL X. ~ (bnd_iUnclosedPizza X & bnd_iGiardiniera X);
% 16.52/16.05 ALL X. ~ (bnd_iPepperTopping X & bnd_iLeekTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iSloppyGiuseppe X & bnd_iParmense X);
% 16.52/16.05 ALL X. ~ (bnd_iCaperTopping X & bnd_iArtichokeTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iPolloAdAstra X & bnd_iLaReine X);
% 16.52/16.05 ALL X. ~ (bnd_iPetitPoisTopping X & bnd_iCaperTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iGiardiniera X & bnd_iPrinceCarlo X);
% 16.52/16.05 ALL X. ~ (bnd_iJalapenoPepperTopping X & bnd_iGreenPepperTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iPeperoniSausageTopping X & bnd_iHotSpicedBeefTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iCheeseTopping X & bnd_iFishTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iPolloAdAstra X & bnd_iParmense X);
% 16.52/16.05 ALL X. ~ (bnd_iQuattroFormaggi X & bnd_iFiorentina X);
% 16.52/16.05 ALL X. ~ (bnd_iSpinachTopping X & bnd_iLeekTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iSweetPepperTopping X & bnd_iPeperonataTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iGarlicTopping X & bnd_iCaperTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iMargherita X & bnd_iQuattroFormaggi X);
% 16.52/16.05 ALL X. ~ (bnd_iMushroomTopping X & bnd_iAsparagusTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iPolloAdAstra X & bnd_iSiciliana X);
% 16.52/16.05 ALL X. ~ (bnd_iFruttiDiMare X & bnd_iNapoletana X);
% 16.52/16.05 ALL X. ~ (bnd_iLaReine X & bnd_iGiardiniera X);
% 16.52/16.05 ALL X. ~ (bnd_iMeatTopping X & bnd_iSauceTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iFourSeasons X & bnd_iQuattroFormaggi X);
% 16.52/16.05 ALL X. ~ (bnd_iPepperTopping X & bnd_iCaperTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iParmense X & bnd_iGiardiniera X);
% 16.52/16.05 ALL X. ~ (bnd_iNutTopping X & bnd_iFruitTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iAmericanHot X & bnd_iSoho X);
% 16.52/16.05 ALL X. ~ (bnd_iAmerican X & bnd_iQuattroFormaggi X);
% 16.52/16.05 ALL X. ~ (bnd_iFruttiDiMare X & bnd_iCapricciosa X);
% 16.52/16.05 ALL X. ~ (bnd_iParmesanTopping X & bnd_iGorgonzolaTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iSpinachTopping X & bnd_iCaperTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iCaprina X & bnd_iQuattroFormaggi X);
% 16.52/16.05 ALL X. ~ (bnd_iUnclosedPizza X & bnd_iQuattroFormaggi X);
% 16.52/16.05 ALL X. ~ (bnd_iFruttiDiMare X & bnd_iRosa X);
% 16.52/16.05 ALL X. ~ (bnd_iOnionTopping X & bnd_iLeekTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iRocketTopping X & bnd_iLeekTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iMeatTopping X & bnd_iVegetableTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iHerbSpiceTopping X & bnd_iSauceTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iNapoletana X & bnd_iCapricciosa X);
% 16.52/16.05 ALL X. ~ (bnd_iPetitPoisTopping X & bnd_iArtichokeTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iQuattroFormaggi X & bnd_iPrinceCarlo X);
% 16.52/16.05 ALL X. ~ (bnd_iHotSpicedBeefTopping X & bnd_iChickenTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iMushroomTopping X & bnd_iArtichokeTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iSoho X & bnd_iFiorentina X);
% 16.52/16.05 ALL X. ~ (bnd_iNapoletana X & bnd_iRosa X);
% 16.52/16.05 ALL X. ~ (bnd_iPetitPoisTopping X & bnd_iMushroomTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iMargherita X & bnd_iSoho X);
% 16.52/16.05 ALL X. ~ (bnd_iFruttiDiMare X & bnd_iCajun X);
% 16.52/16.05 ALL X. ~ (bnd_iLaReine X & bnd_iQuattroFormaggi X);
% 16.52/16.05 ALL X. ~ (bnd_iHot X & bnd_iMild X);
% 16.52/16.05 ALL X. ~ (bnd_iFourSeasons X & bnd_iSoho X);
% 16.52/16.05 ALL X. ~ (bnd_iOnionTopping X & bnd_iCaperTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iCaperTopping X & bnd_iRocketTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iParmense X & bnd_iQuattroFormaggi X);
% 16.52/16.05 ALL X. ~ (bnd_iHerbSpiceTopping X & bnd_iVegetableTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iFruttiDiMare X & bnd_iSiciliana X);
% 16.52/16.05 ALL X. ~ (bnd_iFourCheesesTopping X & bnd_iGorgonzolaTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iPizzaBase X & bnd_iPizzaTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iTomatoTopping X & bnd_iMushroomTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iRosa X & bnd_iCapricciosa X);
% 16.52/16.05 ALL X. ~ (bnd_iPepperTopping X & bnd_iMushroomTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iNapoletana X & bnd_iCajun X);
% 16.52/16.05 ALL X. ~ (bnd_iFruttiDiMare X & bnd_iVeneziana X);
% 16.52/16.05 ALL X. ~ (bnd_iFourSeasons X & bnd_iAmericanHot X);
% 16.52/16.05 ALL X. ~ (bnd_iAmerican X & bnd_iSoho X);
% 16.52/16.05 ALL X. ~ (bnd_iAmericanHot X & bnd_iMushroom X);
% 16.52/16.05 ALL X. ~ (bnd_iNapoletana X & bnd_iQuattroFormaggi X);
% 16.52/16.05 ALL X. ~ (bnd_iCaprina X & bnd_iSoho X);
% 16.52/16.05 ALL X. ~ (bnd_iUnclosedPizza X & bnd_iSoho X);
% 16.52/16.05 ALL X. ~ (bnd_iNapoletana X & bnd_iSiciliana X);
% 16.52/16.05 ALL X. ~ (bnd_iNonVegetarianPizza X & bnd_iVegetarianPizza X);
% 16.52/16.05 ALL X. ~ (bnd_iCheeseTopping X & bnd_iSauceTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iSpinachTopping X & bnd_iMushroomTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iVeneziana X & bnd_iNapoletana X);
% 16.52/16.05 ALL X. ~ (bnd_iGorgonzolaTopping X & bnd_iMozzarellaTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iFruttiDiMare X & bnd_iSloppyGiuseppe X);
% 16.52/16.05 ALL X. ~ (bnd_iCajun X & bnd_iCapricciosa X);
% 16.52/16.05 ALL X. ~ (bnd_iSoho X & bnd_iPrinceCarlo X);
% 16.52/16.05 ALL X. ~ (bnd_iVegetableTopping X & bnd_iFishTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iVeneziana X & bnd_iPolloAdAstra X);
% 16.52/16.05 ALL X. ~ (bnd_iTomatoTopping X & bnd_iLeekTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iMedium X & bnd_iMild X);
% 16.52/16.05 ALL X. ~ (bnd_iCajun X & bnd_iRosa X);
% 16.52/16.05 ALL X. ~ (bnd_iFruttiDiMare X & bnd_iPolloAdAstra X);
% 16.52/16.05 ALL X. ~ (bnd_iSiciliana X & bnd_iCapricciosa X);
% 16.52/16.05 ALL X. ~ (bnd_iMushroom X & bnd_iFiorentina X);
% 16.52/16.05 ALL X. ~ (bnd_iOliveTopping X & bnd_iLeekTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iMargherita X & bnd_iMushroom X);
% 16.52/16.05 ALL X. ~ (bnd_iLaReine X & bnd_iSoho X);
% 16.52/16.05 ALL X. ~ (bnd_iSloppyGiuseppe X & bnd_iNapoletana X);
% 16.52/16.05 ALL X. ~ (bnd_iVeneziana X & bnd_iCapricciosa X);
% 16.52/16.05 ALL X. ~ (bnd_iCheeseTopping X & bnd_iVegetableTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iSiciliana X & bnd_iRosa X);
% 16.52/16.05 ALL X. ~ (bnd_iSoho X & bnd_iParmense X);
% 16.52/16.05 ALL X. ~ (bnd_iVeneziana X & bnd_iRosa X);
% 16.52/16.05 ALL X. ~ (bnd_iFourSeasons X & bnd_iMushroom X);
% 16.52/16.05 ALL X. ~ (bnd_iPolloAdAstra X & bnd_iNapoletana X);
% 16.52/16.05 ALL X. ~ (bnd_iFruttiDiMare X & bnd_iGiardiniera X);
% 16.52/16.05 ALL X. ~ (bnd_iGiardiniera X & bnd_iCajun X);
% 16.52/16.05 ALL X. ~ (bnd_iOnionTopping X & bnd_iMushroomTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iMushroomTopping X & bnd_iRocketTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iCaperTopping X & bnd_iTomatoTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iPeperoniSausageTopping X & bnd_iHamTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iSloppyGiuseppe X & bnd_iCapricciosa X);
% 16.52/16.05 ALL X. ~ (bnd_iMushroom X & bnd_iAmerican X);
% 16.52/16.05 ALL X. ~ (bnd_iMeatTopping X & bnd_iFruitTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iOliveTopping X & bnd_iCaperTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iAsparagusTopping X & bnd_iArtichokeTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iSiciliana X & bnd_iCajun X);
% 16.52/16.05 ALL X. ~ (bnd_iNapoletana X & bnd_iGiardiniera X);
% 16.52/16.05 ALL X. ~ (bnd_iCaprina X & bnd_iMushroom X);
% 16.52/16.05 ALL X. ~ (bnd_iUnclosedPizza X & bnd_iMushroom X);
% 16.52/16.05 ALL X. ~ (bnd_iSloppyGiuseppe X & bnd_iRosa X);
% 16.52/16.05 ALL X. ~ (bnd_iPetitPoisTopping X & bnd_iAsparagusTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iJalapenoPepperTopping X & bnd_iPeperonataTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iPolloAdAstra X & bnd_iCapricciosa X);
% 16.52/16.05 ALL X. ~ (bnd_iVeneziana X & bnd_iCajun X);
% 16.52/16.05 ALL X. ~ (bnd_iPolloAdAstra X & bnd_iRosa X);
% 16.52/16.05 ALL X. ~ (bnd_iMushroom X & bnd_iPrinceCarlo X);
% 16.52/16.05 ALL X. ~ (bnd_iVeneziana X & bnd_iSiciliana X);
% 16.52/16.05 ALL X. ~ (bnd_iGarlicTopping X & bnd_iLeekTopping X);
% 16.52/16.05 ALL X. ~ (bnd_iGiardiniera X & bnd_iCapricciosa X);
% 16.52/16.05 bnd_iowlThing bnd_iItaly; bnd_iCountry bnd_iItaly;
% 16.52/16.05 bnd_iowlThing bnd_iGermany; bnd_iCountry bnd_iGermany;
% 16.52/16.05 bnd_iowlThing bnd_iFrance; bnd_iCountry bnd_iFrance;
% 16.52/16.05 bnd_iowlThing bnd_iEngland; bnd_iCountry bnd_iEngland;
% 16.52/16.05 bnd_iowlThing bnd_iAmerica; bnd_iCountry bnd_iAmerica;
% 16.52/16.05 ALL X Y. bnd_iisToppingOf X Y = bnd_ihasTopping Y X;
% 16.52/16.05 ALL X Y. bnd_iisToppingOf X Y --> bnd_iPizza Y;
% 16.52/16.05 ALL X Y. bnd_iisToppingOf X Y --> bnd_iPizzaTopping X;
% 16.52/16.05 ALL X Y Z. bnd_iisToppingOf X Y & bnd_iisToppingOf X Z --> Y = Z;
% 16.52/16.05 ALL X Y.
% 16.52/16.05 bnd_iisToppingOf X Y --> bnd_abstractDomain X & bnd_abstractDomain Y;
% 16.52/16.05 ALL X Y. bnd_iisIngredientOf X Y = bnd_ihasIngredient Y X;
% 16.52/16.05 ALL X Y. bnd_iisIngredientOf X Y --> bnd_iFood Y;
% 16.52/16.05 ALL X Y. bnd_iisIngredientOf X Y --> bnd_iFood X;
% 16.52/16.05 ALL X Y Z.
% 16.52/16.05 bnd_iisIngredientOf X Y & bnd_iisIngredientOf Y Z -->
% 16.52/16.05 bnd_iisIngredientOf X Z;
% 16.52/16.05 ALL X Y.
% 16.52/16.05 bnd_iisIngredientOf X Y -->
% 16.52/16.05 bnd_abstractDomain X & bnd_abstractDomain Y;
% 16.52/16.05 ALL X Y. bnd_iisBaseOf X Y = bnd_ihasBase Y X;
% 16.52/16.05 ALL X Y. bnd_iisBaseOf X Y --> bnd_iPizza Y;
% 16.52/16.05 ALL X Y. bnd_iisBaseOf X Y --> bnd_iPizzaBase X;
% 16.52/16.05 ALL X Y Z. bnd_iisBaseOf Y X & bnd_iisBaseOf Z X --> Y = Z;
% 16.52/16.05 ALL X Y Z. bnd_iisBaseOf X Y & bnd_iisBaseOf X Z --> Y = Z;
% 16.52/16.05 ALL X Y.
% 16.52/16.05 bnd_iisBaseOf X Y --> bnd_abstractDomain X & bnd_abstractDomain Y;
% 16.52/16.05 ALL X Y. bnd_ihasTopping X Y = bnd_iisToppingOf Y X;
% 16.52/16.05 ALL X Y. bnd_ihasTopping X Y --> bnd_iPizzaTopping Y;
% 16.52/16.05 ALL X Y. bnd_ihasTopping X Y --> bnd_iPizza X;
% 16.52/16.05 ALL X Y Z. bnd_ihasTopping Y X & bnd_ihasTopping Z X --> Y = Z;
% 16.52/16.05 ALL X Y.
% 16.52/16.05 bnd_ihasTopping X Y --> bnd_abstractDomain X & bnd_abstractDomain Y;
% 16.52/16.05 ALL X Y. bnd_ihasSpiciness X Y --> bnd_iSpiciness Y;
% 16.52/16.05 ALL X Y Z. bnd_ihasSpiciness X Y & bnd_ihasSpiciness X Z --> Y = Z;
% 16.52/16.05 ALL X Y.
% 16.52/16.05 bnd_ihasSpiciness X Y --> bnd_abstractDomain X & bnd_abstractDomain Y;
% 16.52/16.05 ALL X Y. bnd_ihasIngredient X Y = bnd_iisIngredientOf Y X;
% 16.52/16.05 ALL X Y. bnd_ihasIngredient X Y --> bnd_iFood Y;
% 16.52/16.05 ALL X Y. bnd_ihasIngredient X Y --> bnd_iFood X;
% 16.52/16.05 ALL X Y Z.
% 16.52/16.05 bnd_ihasIngredient X Y & bnd_ihasIngredient Y Z -->
% 16.52/16.05 bnd_ihasIngredient X Z;
% 16.52/16.05 ALL X Y.
% 16.52/16.05 bnd_ihasIngredient X Y -->
% 16.52/16.05 bnd_abstractDomain X & bnd_abstractDomain Y;
% 16.52/16.05 ALL X Y.
% 16.52/16.05 bnd_ihasCountryOfOrigin X Y -->
% 16.52/16.05 bnd_abstractDomain X & bnd_abstractDomain Y;
% 16.52/16.05 ALL X Y. bnd_ihasBase X Y = bnd_iisBaseOf Y X;
% 16.52/16.05 ALL X Y. bnd_ihasBase X Y --> bnd_iPizzaBase Y;
% 16.52/16.05 ALL X Y. bnd_ihasBase X Y --> bnd_iPizza X;
% 16.52/16.05 ALL X Y Z. bnd_ihasBase Y X & bnd_ihasBase Z X --> Y = Z;
% 16.52/16.05 ALL X Y Z. bnd_ihasBase X Y & bnd_ihasBase X Z --> Y = Z;
% 16.52/16.05 ALL X Y.
% 16.52/16.05 bnd_ihasBase X Y --> bnd_abstractDomain X & bnd_abstractDomain Y;
% 16.52/16.05 ALL X. bnd_iowlThing X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iVeneziana X -->
% 16.52/16.05 bnd_abstractDomain X &
% 16.52/16.05 (ALL Y.
% 16.52/16.05 bnd_ihasTopping X Y -->
% 16.52/16.05 (((((bnd_iOnionTopping Y | bnd_iSultanaTopping Y) |
% 16.52/16.05 bnd_iPineKernels Y) |
% 16.52/16.05 bnd_iOliveTopping Y) |
% 16.52/16.05 bnd_iMozzarellaTopping Y) |
% 16.52/16.05 bnd_iCaperTopping Y) |
% 16.52/16.05 bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iVeneziana X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iVeneziana X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iSultanaTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iVeneziana X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iOnionTopping Y);
% 16.52/16.05 ALL X. bnd_iVeneziana X --> bnd_ihasCountryOfOrigin X bnd_iItaly;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iVeneziana X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iOliveTopping Y);
% 16.52/16.05 ALL X. bnd_iVeneziana X --> bnd_iNamedPizza X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iVeneziana X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMozzarellaTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iVeneziana X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iCaperTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iVeneziana X --> (EX Y. bnd_ihasTopping X Y & bnd_iPineKernels Y);
% 16.52/16.05 ALL X. bnd_iVeneziana X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iVegetarianTopping X =
% 16.52/16.05 ((((((bnd_iCheeseTopping X | bnd_iNutTopping X) |
% 16.52/16.05 bnd_iHerbSpiceTopping X) |
% 16.52/16.05 bnd_iVegetableTopping X) |
% 16.52/16.05 bnd_iSauceTopping X) |
% 16.52/16.05 bnd_iFruitTopping X) &
% 16.52/16.05 bnd_iPizzaTopping X);
% 16.52/16.05 ALL X. bnd_iVegetarianTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iVegetarianPizzaEquivalent2 X =
% 16.52/16.05 ((bnd_iPizza X & bnd_abstractDomain X) &
% 16.52/16.05 (ALL Y.
% 16.52/16.05 bnd_ihasTopping X Y -->
% 16.52/16.05 ((((bnd_iCheeseTopping Y | bnd_iNutTopping Y) |
% 16.52/16.05 bnd_iHerbSpiceTopping Y) |
% 16.52/16.05 bnd_iVegetableTopping Y) |
% 16.52/16.05 bnd_iSauceTopping Y) |
% 16.52/16.05 bnd_iFruitTopping Y));
% 16.52/16.05 ALL X. bnd_iVegetarianPizzaEquivalent2 X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iVegetarianPizzaEquivalent1 X =
% 16.52/16.05 ((bnd_iPizza X & bnd_abstractDomain X) &
% 16.52/16.05 (ALL Y. bnd_ihasTopping X Y --> bnd_iVegetarianTopping Y));
% 16.52/16.05 ALL X. bnd_iVegetarianPizzaEquivalent1 X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iVegetarianPizza X =
% 16.52/16.05 ((((bnd_abstractDomain X &
% 16.52/16.05 ~ (EX Y. bnd_ihasTopping X Y & bnd_iMeatTopping Y)) &
% 16.52/16.05 bnd_iPizza X) &
% 16.52/16.05 bnd_abstractDomain X) &
% 16.52/16.05 ~ (EX Y. bnd_ihasTopping X Y & bnd_iFishTopping Y));
% 16.52/16.05 ALL X. bnd_iVegetarianPizza X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iVegetableTopping X --> bnd_iPizzaTopping X;
% 16.52/16.05 ALL X. bnd_iVegetableTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iValuePartition X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iUnclosedPizza X --> bnd_iNamedPizza X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iUnclosedPizza X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMozzarellaTopping Y);
% 16.52/16.05 ALL X. bnd_iUnclosedPizza X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iTomatoTopping X --> bnd_iVegetableTopping X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iTomatoTopping X --> (EX Y. bnd_ihasSpiciness X Y & bnd_iMild Y);
% 16.52/16.05 ALL X. bnd_iTomatoTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iTobascoPepperSauce X --> bnd_iSauceTopping X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iTobascoPepperSauce X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iHot Y);
% 16.52/16.05 ALL X. bnd_iTobascoPepperSauce X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iThinAndCrispyPizza X =
% 16.52/16.05 ((bnd_iPizza X & bnd_abstractDomain X) &
% 16.52/16.05 (ALL Y. bnd_ihasBase X Y --> bnd_iThinAndCrispyBase Y));
% 16.52/16.05 ALL X. bnd_iThinAndCrispyPizza X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iThinAndCrispyBase X --> bnd_iPizzaBase X;
% 16.52/16.05 ALL X. bnd_iThinAndCrispyBase X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iSweetPepperTopping X --> bnd_iPepperTopping X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSweetPepperTopping X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iMild Y);
% 16.52/16.05 ALL X. bnd_iSweetPepperTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iSundriedTomatoTopping X --> bnd_iTomatoTopping X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSundriedTomatoTopping X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iMild Y);
% 16.52/16.05 ALL X. bnd_iSundriedTomatoTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iSultanaTopping X --> bnd_iFruitTopping X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSultanaTopping X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iMedium Y);
% 16.52/16.05 ALL X. bnd_iSultanaTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iSpinachTopping X --> bnd_iVegetableTopping X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSpinachTopping X --> (EX Y. bnd_ihasSpiciness X Y & bnd_iMild Y);
% 16.52/16.05 ALL X. bnd_iSpinachTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSpicyTopping X =
% 16.52/16.05 ((EX Y. bnd_ihasSpiciness X Y & bnd_iHot Y) & bnd_iPizzaTopping X);
% 16.52/16.05 ALL X. bnd_iSpicyTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSpicyPizzaEquivalent X =
% 16.52/16.05 (bnd_iPizza X &
% 16.52/16.05 (EX Y. (bnd_ihasTopping X Y &
% 16.52/16.05 (EX Z. bnd_ihasSpiciness Y Z & bnd_iHot Z)) &
% 16.52/16.05 bnd_iPizzaTopping Y));
% 16.52/16.05 ALL X. bnd_iSpicyPizzaEquivalent X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSpicyPizza X =
% 16.52/16.05 ((EX Y. bnd_ihasTopping X Y & bnd_iSpicyTopping Y) & bnd_iPizza X);
% 16.52/16.05 ALL X. bnd_iSpicyPizza X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iSpiciness X --> bnd_iValuePartition X;
% 16.52/16.05 ALL X. bnd_iSpiciness X = ((bnd_iMedium X | bnd_iHot X) | bnd_iMild X);
% 16.52/16.05 ALL X. bnd_iSpiciness X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSoho X --> (EX Y. bnd_ihasTopping X Y & bnd_iRocketTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSoho X --> (EX Y. bnd_ihasTopping X Y & bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSoho X -->
% 16.52/16.05 bnd_abstractDomain X &
% 16.52/16.05 (ALL Y.
% 16.52/16.05 bnd_ihasTopping X Y -->
% 16.52/16.05 ((((bnd_iParmesanTopping Y | bnd_iOliveTopping Y) |
% 16.52/16.05 bnd_iMozzarellaTopping Y) |
% 16.52/16.05 bnd_iGarlicTopping Y) |
% 16.52/16.05 bnd_iTomatoTopping Y) |
% 16.52/16.05 bnd_iRocketTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSoho X --> (EX Y. bnd_ihasTopping X Y & bnd_iGarlicTopping Y);
% 16.52/16.05 ALL X. bnd_iSoho X --> bnd_iNamedPizza X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSoho X --> (EX Y. bnd_ihasTopping X Y & bnd_iParmesanTopping Y);
% 16.52/16.05 ALL X. bnd_iSoho X --> (EX Y. bnd_ihasTopping X Y & bnd_iOliveTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSoho X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMozzarellaTopping Y);
% 16.52/16.05 ALL X. bnd_iSoho X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSloppyGiuseppe X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSloppyGiuseppe X -->
% 16.52/16.05 bnd_abstractDomain X &
% 16.52/16.05 (ALL Y.
% 16.52/16.05 bnd_ihasTopping X Y -->
% 16.52/16.05 (((bnd_iOnionTopping Y | bnd_iHotSpicedBeefTopping Y) |
% 16.52/16.05 bnd_iGreenPepperTopping Y) |
% 16.52/16.05 bnd_iMozzarellaTopping Y) |
% 16.52/16.05 bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSloppyGiuseppe X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iHotSpicedBeefTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSloppyGiuseppe X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iOnionTopping Y);
% 16.52/16.05 ALL X. bnd_iSloppyGiuseppe X --> bnd_iNamedPizza X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSloppyGiuseppe X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMozzarellaTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSloppyGiuseppe X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iGreenPepperTopping Y);
% 16.52/16.05 ALL X. bnd_iSloppyGiuseppe X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iSlicedTomatoTopping X --> bnd_iTomatoTopping X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSlicedTomatoTopping X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iMild Y);
% 16.52/16.05 ALL X. bnd_iSlicedTomatoTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSiciliana X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iAnchoviesTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSiciliana X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSiciliana X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iGarlicTopping Y);
% 16.52/16.05 ALL X. bnd_iSiciliana X --> bnd_iNamedPizza X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSiciliana X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iOliveTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSiciliana X --> (EX Y. bnd_ihasTopping X Y & bnd_iHamTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSiciliana X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iArtichokeTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSiciliana X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMozzarellaTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iSiciliana X -->
% 16.52/16.05 bnd_abstractDomain X &
% 16.52/16.05 (ALL Y.
% 16.52/16.05 bnd_ihasTopping X Y -->
% 16.52/16.05 (((((bnd_iHamTopping Y | bnd_iAnchoviesTopping Y) |
% 16.52/16.05 bnd_iOliveTopping Y) |
% 16.52/16.05 bnd_iMozzarellaTopping Y) |
% 16.52/16.05 bnd_iGarlicTopping Y) |
% 16.52/16.05 bnd_iTomatoTopping Y) |
% 16.52/16.05 bnd_iArtichokeTopping Y);
% 16.52/16.05 ALL X. bnd_iSiciliana X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iSauceTopping X --> bnd_iPizzaTopping X;
% 16.52/16.05 ALL X. bnd_iSauceTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iRosemaryTopping X --> bnd_iHerbSpiceTopping X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iRosemaryTopping X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iMild Y);
% 16.52/16.05 ALL X. bnd_iRosemaryTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iRosa X --> (EX Y. bnd_ihasTopping X Y & bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iRosa X -->
% 16.52/16.05 bnd_abstractDomain X &
% 16.52/16.05 (ALL Y.
% 16.52/16.05 bnd_ihasTopping X Y -->
% 16.52/16.05 (bnd_iGorgonzolaTopping Y | bnd_iMozzarellaTopping Y) |
% 16.52/16.05 bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X. bnd_iRosa X --> bnd_iNamedPizza X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iRosa X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMozzarellaTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iRosa X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iGorgonzolaTopping Y);
% 16.52/16.05 ALL X. bnd_iRosa X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iRocketTopping X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iMedium Y);
% 16.52/16.05 ALL X. bnd_iRocketTopping X --> bnd_iVegetableTopping X;
% 16.52/16.05 ALL X. bnd_iRocketTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iRedOnionTopping X --> bnd_iOnionTopping X;
% 16.52/16.05 ALL X. bnd_iRedOnionTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iRealItalianPizza X -->
% 16.52/16.05 bnd_abstractDomain X &
% 16.52/16.05 (ALL Y. bnd_ihasBase X Y --> bnd_iThinAndCrispyBase Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iRealItalianPizza X =
% 16.52/16.05 (bnd_ihasCountryOfOrigin X bnd_iItaly & bnd_iPizza X);
% 16.52/16.05 ALL X. bnd_iRealItalianPizza X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iQuattroFormaggi X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iQuattroFormaggi X -->
% 16.52/16.05 bnd_abstractDomain X &
% 16.52/16.05 (ALL Y.
% 16.52/16.05 bnd_ihasTopping X Y -->
% 16.52/16.05 bnd_iFourCheesesTopping Y | bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X. bnd_iQuattroFormaggi X --> bnd_iNamedPizza X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iQuattroFormaggi X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iFourCheesesTopping Y);
% 16.52/16.05 ALL X. bnd_iQuattroFormaggi X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iPrinceCarlo X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iPrinceCarlo X -->
% 16.52/16.05 bnd_abstractDomain X &
% 16.52/16.05 (ALL Y.
% 16.52/16.05 bnd_ihasTopping X Y -->
% 16.52/16.05 (((bnd_iParmesanTopping Y | bnd_iRosemaryTopping Y) |
% 16.52/16.05 bnd_iMozzarellaTopping Y) |
% 16.52/16.05 bnd_iTomatoTopping Y) |
% 16.52/16.05 bnd_iLeekTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iPrinceCarlo X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iLeekTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iPrinceCarlo X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iRosemaryTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iPrinceCarlo X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iParmesanTopping Y);
% 16.52/16.05 ALL X. bnd_iPrinceCarlo X --> bnd_iNamedPizza X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iPrinceCarlo X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMozzarellaTopping Y);
% 16.52/16.05 ALL X. bnd_iPrinceCarlo X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iPrawnsTopping X --> bnd_iFishTopping X;
% 16.52/16.05 ALL X. bnd_iPrawnsTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iPolloAdAstra X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iSweetPepperTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iPolloAdAstra X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iChickenTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iPolloAdAstra X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iPolloAdAstra X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iGarlicTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iPolloAdAstra X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iRedOnionTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iPolloAdAstra X -->
% 16.52/16.05 bnd_abstractDomain X &
% 16.52/16.05 (ALL Y.
% 16.52/16.05 bnd_ihasTopping X Y -->
% 16.52/16.05 (((((bnd_iSweetPepperTopping Y | bnd_iChickenTopping Y) |
% 16.52/16.05 bnd_iRedOnionTopping Y) |
% 16.52/16.05 bnd_iMozzarellaTopping Y) |
% 16.52/16.05 bnd_iGarlicTopping Y) |
% 16.52/16.05 bnd_iTomatoTopping Y) |
% 16.52/16.05 bnd_iCajunSpiceTopping Y);
% 16.52/16.05 ALL X. bnd_iPolloAdAstra X --> bnd_iNamedPizza X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iPolloAdAstra X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iCajunSpiceTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iPolloAdAstra X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMozzarellaTopping Y);
% 16.52/16.05 ALL X. bnd_iPolloAdAstra X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iPizzaTopping X --> bnd_iFood X;
% 16.52/16.05 ALL X. bnd_iPizzaTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iPizzaBase X --> bnd_iFood X;
% 16.52/16.05 ALL X. bnd_iPizzaBase X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iPizza X --> bnd_iFood X;
% 16.52/16.05 ALL X. bnd_iPizza X --> (EX Y. bnd_ihasBase X Y & bnd_iPizzaBase Y);
% 16.52/16.05 ALL X. bnd_iPizza X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iPineKernels X --> bnd_iNutTopping X;
% 16.52/16.05 ALL X. bnd_iPineKernels X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iPetitPoisTopping X --> bnd_iVegetableTopping X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iPetitPoisTopping X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iMild Y);
% 16.52/16.05 ALL X. bnd_iPetitPoisTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iPepperTopping X --> bnd_iVegetableTopping X;
% 16.52/16.05 ALL X. bnd_iPepperTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iPeperoniSausageTopping X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iMedium Y);
% 16.52/16.05 ALL X. bnd_iPeperoniSausageTopping X --> bnd_iMeatTopping X;
% 16.52/16.05 ALL X. bnd_iPeperoniSausageTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iPeperonataTopping X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iMedium Y);
% 16.52/16.05 ALL X. bnd_iPeperonataTopping X --> bnd_iPepperTopping X;
% 16.52/16.05 ALL X. bnd_iPeperonataTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iParmesanTopping X --> bnd_iCheeseTopping X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iParmesanTopping X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iMild Y);
% 16.52/16.05 ALL X. bnd_iParmesanTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iParmense X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iParmense X -->
% 16.52/16.05 bnd_abstractDomain X &
% 16.52/16.05 (ALL Y.
% 16.52/16.05 bnd_ihasTopping X Y -->
% 16.52/16.05 (((bnd_iParmesanTopping Y | bnd_iHamTopping Y) |
% 16.52/16.05 bnd_iMozzarellaTopping Y) |
% 16.52/16.05 bnd_iTomatoTopping Y) |
% 16.52/16.05 bnd_iAsparagusTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iParmense X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iAsparagusTopping Y);
% 16.52/16.05 ALL X. bnd_iParmense X --> bnd_iNamedPizza X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iParmense X --> (EX Y. bnd_ihasTopping X Y & bnd_iHamTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iParmense X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iParmesanTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iParmense X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMozzarellaTopping Y);
% 16.52/16.05 ALL X. bnd_iParmense X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iParmaHamTopping X --> bnd_iHamTopping X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iParmaHamTopping X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iMild Y);
% 16.52/16.05 ALL X. bnd_iParmaHamTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iOnionTopping X --> (EX Y. bnd_ihasSpiciness X Y & bnd_iMedium Y);
% 16.52/16.05 ALL X. bnd_iOnionTopping X --> bnd_iVegetableTopping X;
% 16.52/16.05 ALL X. bnd_iOnionTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iOliveTopping X --> bnd_iVegetableTopping X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iOliveTopping X --> (EX Y. bnd_ihasSpiciness X Y & bnd_iMild Y);
% 16.52/16.05 ALL X. bnd_iOliveTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iNutTopping X --> bnd_iPizzaTopping X;
% 16.52/16.05 ALL X. bnd_iNutTopping X --> (EX Y. bnd_ihasSpiciness X Y & bnd_iMild Y);
% 16.52/16.05 ALL X. bnd_iNutTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iNonVegetarianPizza X =
% 16.52/16.05 ((bnd_abstractDomain X & ~ bnd_iVegetarianPizza X) & bnd_iPizza X);
% 16.52/16.05 ALL X. bnd_iNonVegetarianPizza X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iNapoletana X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iNapoletana X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iAnchoviesTopping Y);
% 16.52/16.05 ALL X. bnd_iNapoletana X --> bnd_ihasCountryOfOrigin X bnd_iItaly;
% 16.52/16.05 ALL X. bnd_iNapoletana X --> bnd_iNamedPizza X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iNapoletana X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iOliveTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iNapoletana X -->
% 16.52/16.05 bnd_abstractDomain X &
% 16.52/16.05 (ALL Y.
% 16.52/16.05 bnd_ihasTopping X Y -->
% 16.52/16.05 (((bnd_iAnchoviesTopping Y | bnd_iOliveTopping Y) |
% 16.52/16.05 bnd_iMozzarellaTopping Y) |
% 16.52/16.05 bnd_iCaperTopping Y) |
% 16.52/16.05 bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iNapoletana X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMozzarellaTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iNapoletana X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iCaperTopping Y);
% 16.52/16.05 ALL X. bnd_iNapoletana X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iNamedPizza X --> bnd_iPizza X;
% 16.52/16.05 ALL X. bnd_iNamedPizza X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iMushroomTopping X --> bnd_iVegetableTopping X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iMushroomTopping X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iMild Y);
% 16.52/16.05 ALL X. bnd_iMushroomTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iMushroom X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iMushroom X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMushroomTopping Y);
% 16.52/16.05 ALL X. bnd_iMushroom X --> bnd_iNamedPizza X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iMushroom X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMozzarellaTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iMushroom X -->
% 16.52/16.05 bnd_abstractDomain X &
% 16.52/16.05 (ALL Y.
% 16.52/16.05 bnd_ihasTopping X Y -->
% 16.52/16.05 (bnd_iMozzarellaTopping Y | bnd_iTomatoTopping Y) |
% 16.52/16.05 bnd_iMushroomTopping Y);
% 16.52/16.05 ALL X. bnd_iMushroom X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iMozzarellaTopping X --> bnd_ihasCountryOfOrigin X bnd_iItaly;
% 16.52/16.05 ALL X. bnd_iMozzarellaTopping X --> bnd_iCheeseTopping X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iMozzarellaTopping X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iMild Y);
% 16.52/16.05 ALL X. bnd_iMozzarellaTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iMixedSeafoodTopping X --> bnd_iFishTopping X;
% 16.52/16.05 ALL X. bnd_iMixedSeafoodTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iMild X --> bnd_iSpiciness X;
% 16.52/16.05 ALL X. bnd_iMild X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iMedium X --> bnd_iSpiciness X;
% 16.52/16.05 ALL X. bnd_iMedium X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iMeatyPizza X =
% 16.52/16.05 (bnd_iPizza X & (EX Y. bnd_ihasTopping X Y & bnd_iMeatTopping Y));
% 16.52/16.05 ALL X. bnd_iMeatyPizza X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iMeatTopping X --> bnd_iPizzaTopping X;
% 16.52/16.05 ALL X. bnd_iMeatTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iMargherita X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X. bnd_iMargherita X --> bnd_iNamedPizza X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iMargherita X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMozzarellaTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iMargherita X -->
% 16.52/16.05 bnd_abstractDomain X &
% 16.52/16.05 (ALL Y.
% 16.52/16.05 bnd_ihasTopping X Y -->
% 16.52/16.05 bnd_iMozzarellaTopping Y | bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X. bnd_iMargherita X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iLeekTopping X --> bnd_iVegetableTopping X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iLeekTopping X --> (EX Y. bnd_ihasSpiciness X Y & bnd_iMild Y);
% 16.52/16.05 ALL X. bnd_iLeekTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iLaReine X --> (EX Y. bnd_ihasTopping X Y & bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iLaReine X -->
% 16.52/16.05 bnd_abstractDomain X &
% 16.52/16.05 (ALL Y.
% 16.52/16.05 bnd_ihasTopping X Y -->
% 16.52/16.05 (((bnd_iHamTopping Y | bnd_iOliveTopping Y) |
% 16.52/16.05 bnd_iMozzarellaTopping Y) |
% 16.52/16.05 bnd_iTomatoTopping Y) |
% 16.52/16.05 bnd_iMushroomTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iLaReine X --> (EX Y. bnd_ihasTopping X Y & bnd_iHamTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iLaReine X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMushroomTopping Y);
% 16.52/16.05 ALL X. bnd_iLaReine X --> bnd_iNamedPizza X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iLaReine X --> (EX Y. bnd_ihasTopping X Y & bnd_iOliveTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iLaReine X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMozzarellaTopping Y);
% 16.52/16.05 ALL X. bnd_iLaReine X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iJalapenoPepperTopping X --> bnd_iPepperTopping X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iJalapenoPepperTopping X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iHot Y);
% 16.52/16.05 ALL X. bnd_iJalapenoPepperTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iInterestingPizza X =
% 16.52/16.05 (bnd_iPizza X &
% 16.52/16.05 (EX Y0 Y1 Y2.
% 16.52/16.05 ((((bnd_ihasTopping X Y0 & bnd_ihasTopping X Y1) &
% 16.52/16.05 bnd_ihasTopping X Y2) &
% 16.52/16.05 ~ Y0 = Y1) &
% 16.52/16.05 ~ Y0 = Y2) &
% 16.52/16.05 ~ Y1 = Y2));
% 16.52/16.05 ALL X. bnd_iInterestingPizza X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iIceCream X --> bnd_iFood X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iIceCream X --> (EX Y. bnd_ihasTopping X Y & bnd_iFruitTopping Y);
% 16.52/16.05 ALL X. bnd_iIceCream X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iHotSpicedBeefTopping X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iHot Y);
% 16.52/16.05 ALL X. bnd_iHotSpicedBeefTopping X --> bnd_iMeatTopping X;
% 16.52/16.05 ALL X. bnd_iHotSpicedBeefTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iHotGreenPepperTopping X --> bnd_iGreenPepperTopping X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iHotGreenPepperTopping X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iHot Y);
% 16.52/16.05 ALL X. bnd_iHotGreenPepperTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iHot X --> bnd_iSpiciness X;
% 16.52/16.05 ALL X. bnd_iHot X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iHerbSpiceTopping X --> bnd_iPizzaTopping X;
% 16.52/16.05 ALL X. bnd_iHerbSpiceTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iHamTopping X --> bnd_iMeatTopping X;
% 16.52/16.05 ALL X. bnd_iHamTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iGreenPepperTopping X --> bnd_iPepperTopping X;
% 16.52/16.05 ALL X. bnd_iGreenPepperTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iGorgonzolaTopping X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iMild Y);
% 16.52/16.05 ALL X. bnd_iGorgonzolaTopping X --> bnd_iCheeseTopping X;
% 16.52/16.05 ALL X. bnd_iGorgonzolaTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iGoatsCheeseTopping X --> bnd_iCheeseTopping X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iGoatsCheeseTopping X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iMild Y);
% 16.52/16.05 ALL X. bnd_iGoatsCheeseTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iGiardiniera X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iGiardiniera X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iLeekTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iGiardiniera X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iOliveTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iGiardiniera X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMushroomTopping Y);
% 16.52/16.05 ALL X. bnd_iGiardiniera X --> bnd_iNamedPizza X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iGiardiniera X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iSlicedTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iGiardiniera X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMozzarellaTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iGiardiniera X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iPetitPoisTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iGiardiniera X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iPeperonataTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iGiardiniera X -->
% 16.52/16.05 bnd_abstractDomain X &
% 16.52/16.05 (ALL Y.
% 16.52/16.05 bnd_ihasTopping X Y -->
% 16.52/16.05 ((((((bnd_iPetitPoisTopping Y | bnd_iSlicedTomatoTopping Y) |
% 16.52/16.05 bnd_iOliveTopping Y) |
% 16.52/16.05 bnd_iMozzarellaTopping Y) |
% 16.52/16.05 bnd_iPeperonataTopping Y) |
% 16.52/16.05 bnd_iTomatoTopping Y) |
% 16.52/16.05 bnd_iMushroomTopping Y) |
% 16.52/16.05 bnd_iLeekTopping Y);
% 16.52/16.05 ALL X. bnd_iGiardiniera X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iGarlicTopping X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iMedium Y);
% 16.52/16.05 ALL X. bnd_iGarlicTopping X --> bnd_iVegetableTopping X;
% 16.52/16.05 ALL X. bnd_iGarlicTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iFruttiDiMare X -->
% 16.52/16.05 bnd_abstractDomain X &
% 16.52/16.05 (ALL Y.
% 16.52/16.05 bnd_ihasTopping X Y -->
% 16.52/16.05 (bnd_iGarlicTopping Y | bnd_iTomatoTopping Y) |
% 16.52/16.05 bnd_iMixedSeafoodTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iFruttiDiMare X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iFruttiDiMare X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iGarlicTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iFruttiDiMare X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMixedSeafoodTopping Y);
% 16.52/16.05 ALL X. bnd_iFruttiDiMare X --> bnd_iNamedPizza X;
% 16.52/16.05 ALL X. bnd_iFruttiDiMare X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iFruitTopping X --> bnd_iPizzaTopping X;
% 16.52/16.05 ALL X. bnd_iFruitTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iFourSeasons X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iFourSeasons X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iAnchoviesTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iFourSeasons X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iPeperoniSausageTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iFourSeasons X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iOliveTopping Y);
% 16.52/16.05 ALL X. bnd_iFourSeasons X --> bnd_iNamedPizza X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iFourSeasons X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMushroomTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iFourSeasons X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMozzarellaTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iFourSeasons X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iCaperTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iFourSeasons X -->
% 16.52/16.05 bnd_abstractDomain X &
% 16.52/16.05 (ALL Y.
% 16.52/16.05 bnd_ihasTopping X Y -->
% 16.52/16.05 (((((bnd_iPeperoniSausageTopping Y | bnd_iAnchoviesTopping Y) |
% 16.52/16.05 bnd_iOliveTopping Y) |
% 16.52/16.05 bnd_iMozzarellaTopping Y) |
% 16.52/16.05 bnd_iCaperTopping Y) |
% 16.52/16.05 bnd_iTomatoTopping Y) |
% 16.52/16.05 bnd_iMushroomTopping Y);
% 16.52/16.05 ALL X. bnd_iFourSeasons X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iFourCheesesTopping X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iMild Y);
% 16.52/16.05 ALL X. bnd_iFourCheesesTopping X --> bnd_iCheeseTopping X;
% 16.52/16.05 ALL X. bnd_iFourCheesesTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iFood X --> bnd_iDomainConcept X;
% 16.52/16.05 ALL X. bnd_iFood X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iFishTopping X --> bnd_iPizzaTopping X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iFishTopping X --> (EX Y. bnd_ihasSpiciness X Y & bnd_iMild Y);
% 16.52/16.05 ALL X. bnd_iFishTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iFiorentina X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iFiorentina X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iSpinachTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iFiorentina X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iGarlicTopping Y);
% 16.52/16.05 ALL X. bnd_iFiorentina X --> bnd_iNamedPizza X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iFiorentina X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iOliveTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iFiorentina X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iParmesanTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iFiorentina X -->
% 16.52/16.05 bnd_abstractDomain X &
% 16.52/16.05 (ALL Y.
% 16.52/16.05 bnd_ihasTopping X Y -->
% 16.52/16.05 ((((bnd_iParmesanTopping Y | bnd_iOliveTopping Y) |
% 16.52/16.05 bnd_iMozzarellaTopping Y) |
% 16.52/16.05 bnd_iGarlicTopping Y) |
% 16.52/16.05 bnd_iSpinachTopping Y) |
% 16.52/16.05 bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iFiorentina X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMozzarellaTopping Y);
% 16.52/16.05 ALL X. bnd_iFiorentina X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iDomainConcept X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iDeepPanBase X --> bnd_iPizzaBase X;
% 16.52/16.05 ALL X. bnd_iDeepPanBase X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCountry X =
% 16.52/16.05 (bnd_iDomainConcept X &
% 16.52/16.05 ((((X = bnd_iFrance | X = bnd_iItaly) | X = bnd_iGermany) |
% 16.52/16.05 X = bnd_iEngland) |
% 16.52/16.05 X = bnd_iAmerica));
% 16.52/16.05 ALL X. bnd_iCountry X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iChickenTopping X --> bnd_iMeatTopping X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iChickenTopping X --> (EX Y. bnd_ihasSpiciness X Y & bnd_iMild Y);
% 16.52/16.05 ALL X. bnd_iChickenTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iCheeseyVegetableTopping X --> bnd_iVegetableTopping X;
% 16.52/16.05 ALL X. bnd_iCheeseyVegetableTopping X --> bnd_iCheeseTopping X;
% 16.52/16.05 ALL X. bnd_iCheeseyVegetableTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCheeseyPizza X =
% 16.52/16.05 (bnd_iPizza X & (EX Y. bnd_ihasTopping X Y & bnd_iCheeseTopping Y));
% 16.52/16.05 ALL X. bnd_iCheeseyPizza X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iCheeseTopping X --> bnd_iPizzaTopping X;
% 16.52/16.05 ALL X. bnd_iCheeseTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCaprina X --> (EX Y. bnd_ihasTopping X Y & bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X. bnd_iCaprina X --> bnd_iNamedPizza X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCaprina X -->
% 16.52/16.05 bnd_abstractDomain X &
% 16.52/16.05 (ALL Y.
% 16.52/16.05 bnd_ihasTopping X Y -->
% 16.52/16.05 ((bnd_iGoatsCheeseTopping Y | bnd_iSundriedTomatoTopping Y) |
% 16.52/16.05 bnd_iMozzarellaTopping Y) |
% 16.52/16.05 bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCaprina X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMozzarellaTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCaprina X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iGoatsCheeseTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCaprina X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iSundriedTomatoTopping Y);
% 16.52/16.05 ALL X. bnd_iCaprina X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCapricciosa X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iAnchoviesTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCapricciosa X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCapricciosa X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iOliveTopping Y);
% 16.52/16.05 ALL X. bnd_iCapricciosa X --> bnd_iNamedPizza X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCapricciosa X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iHamTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCapricciosa X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMozzarellaTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCapricciosa X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iCaperTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCapricciosa X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iPeperonataTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCapricciosa X -->
% 16.52/16.05 bnd_abstractDomain X &
% 16.52/16.05 (ALL Y.
% 16.52/16.05 bnd_ihasTopping X Y -->
% 16.52/16.05 (((((bnd_iHamTopping Y | bnd_iAnchoviesTopping Y) |
% 16.52/16.05 bnd_iOliveTopping Y) |
% 16.52/16.05 bnd_iMozzarellaTopping Y) |
% 16.52/16.05 bnd_iPeperonataTopping Y) |
% 16.52/16.05 bnd_iCaperTopping Y) |
% 16.52/16.05 bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X. bnd_iCapricciosa X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iCaperTopping X --> bnd_iVegetableTopping X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCaperTopping X --> (EX Y. bnd_ihasSpiciness X Y & bnd_iMild Y);
% 16.52/16.05 ALL X. bnd_iCaperTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCajunSpiceTopping X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iHot Y);
% 16.52/16.05 ALL X. bnd_iCajunSpiceTopping X --> bnd_iHerbSpiceTopping X;
% 16.52/16.05 ALL X. bnd_iCajunSpiceTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCajun X --> (EX Y. bnd_ihasTopping X Y & bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCajun X --> (EX Y. bnd_ihasTopping X Y & bnd_iPrawnsTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCajun X --> (EX Y. bnd_ihasTopping X Y & bnd_iOnionTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCajun X -->
% 16.52/16.05 bnd_abstractDomain X &
% 16.52/16.05 (ALL Y.
% 16.52/16.05 bnd_ihasTopping X Y -->
% 16.52/16.05 ((((bnd_iOnionTopping Y | bnd_iPrawnsTopping Y) |
% 16.52/16.05 bnd_iTobascoPepperSauce Y) |
% 16.52/16.05 bnd_iMozzarellaTopping Y) |
% 16.52/16.05 bnd_iPeperonataTopping Y) |
% 16.52/16.05 bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X. bnd_iCajun X --> bnd_iNamedPizza X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCajun X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMozzarellaTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCajun X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iTobascoPepperSauce Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iCajun X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iPeperonataTopping Y);
% 16.52/16.05 ALL X. bnd_iCajun X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iAsparagusTopping X --> bnd_iVegetableTopping X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iAsparagusTopping X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iMild Y);
% 16.52/16.05 ALL X. bnd_iAsparagusTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iArtichokeTopping X --> bnd_iVegetableTopping X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iArtichokeTopping X -->
% 16.52/16.05 (EX Y. bnd_ihasSpiciness X Y & bnd_iMild Y);
% 16.52/16.05 ALL X. bnd_iArtichokeTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iAnchoviesTopping X --> bnd_iFishTopping X;
% 16.52/16.05 ALL X. bnd_iAnchoviesTopping X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iAmericanHot X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iJalapenoPepperTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iAmericanHot X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iAmericanHot X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iHotGreenPepperTopping Y);
% 16.52/16.05 ALL X. bnd_iAmericanHot X --> bnd_ihasCountryOfOrigin X bnd_iAmerica;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iAmericanHot X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iPeperoniSausageTopping Y);
% 16.52/16.05 ALL X. bnd_iAmericanHot X --> bnd_iNamedPizza X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iAmericanHot X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMozzarellaTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iAmericanHot X -->
% 16.52/16.05 bnd_abstractDomain X &
% 16.52/16.05 (ALL Y.
% 16.52/16.05 bnd_ihasTopping X Y -->
% 16.52/16.05 (((bnd_iPeperoniSausageTopping Y | bnd_iJalapenoPepperTopping Y) |
% 16.52/16.05 bnd_iMozzarellaTopping Y) |
% 16.52/16.05 bnd_iHotGreenPepperTopping Y) |
% 16.52/16.05 bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X. bnd_iAmericanHot X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iAmerican X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X. bnd_iAmerican X --> bnd_ihasCountryOfOrigin X bnd_iAmerica;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iAmerican X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iPeperoniSausageTopping Y);
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iAmerican X -->
% 16.52/16.05 bnd_abstractDomain X &
% 16.52/16.05 (ALL Y.
% 16.52/16.05 bnd_ihasTopping X Y -->
% 16.52/16.05 (bnd_iPeperoniSausageTopping Y | bnd_iMozzarellaTopping Y) |
% 16.52/16.05 bnd_iTomatoTopping Y);
% 16.52/16.05 ALL X. bnd_iAmerican X --> bnd_iNamedPizza X;
% 16.52/16.05 ALL X.
% 16.52/16.05 bnd_iAmerican X -->
% 16.52/16.05 (EX Y. bnd_ihasTopping X Y & bnd_iMozzarellaTopping Y);
% 16.52/16.05 ALL X. bnd_iAmerican X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_dataDomain X --> ~ (bnd_xsd_string X & bnd_xsd_integer X);
% 16.52/16.05 ALL X. bnd_xsd_integer X --> bnd_dataDomain X;
% 16.52/16.05 ALL X. bnd_xsd_string X --> bnd_dataDomain X; ALL X. ~ bnd_iowlNothing X;
% 16.52/16.05 ALL X. bnd_abstractDomain X --> bnd_iowlThing X;
% 16.52/16.05 ALL X. bnd_iowlNothing X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. bnd_iowlThing X --> bnd_abstractDomain X;
% 16.52/16.05 ALL X. ~ (bnd_abstractDomain X & bnd_dataDomain X); Ex bnd_dataDomain;
% 16.52/16.05 Ex bnd_abstractDomain; ALL X. bnd_abstractDomain X | bnd_dataDomain X |]
% 16.52/16.05 ==> True
% 16.52/16.05 Adding axioms...
% 16.52/16.06 Typedef.type_definition_def
% 59.91/59.40 ...done.
% 60.01/59.46 Ground types: ?'b, TPTP_Interpret.ind
% 60.01/59.46 Translating term (sizes: 1, 1) ...
% 100.82/100.14 Invoking SAT solver...
% 100.82/100.14 No model exists.
% 100.82/100.14 Translating term (sizes: 2, 1) ...
% 142.45/141.60 Invoking SAT solver...
% 142.45/141.60 No model exists.
% 142.45/141.60 Translating term (sizes: 1, 2) ...
% 226.85/225.61 Invoking SAT solver...
% 226.85/225.61 No model exists.
% 226.85/225.61 Translating term (sizes: 3, 1) ...
% 270.95/269.49 Invoking SAT solver...
% 270.95/269.49 No model exists.
% 270.95/269.49 Translating term (sizes: 2, 2) ...
% 300.10/298.33 /export/starexec/sandbox2/solver/lib/scripts/run-polyml-5.5.2: line 82: 42786 CPU time limit exceeded (core dumped) "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS
% 300.10/298.33 42787 (core dumped) | { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
% 300.10/298.35 /export/starexec/sandbox2/solver/src/HOL/TPTP/lib/Tools/tptp_refute: line 26: 42630 Exit 152 "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP
% 300.10/298.35 42631 CPU time limit exceeded (core dumped) | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
%------------------------------------------------------------------------------