begin_problem(pizza).

list_of_descriptions.
name({* http://www.co-ode.org/ontologies/pizza, version 2.0.0 *}).
author({* left empty as auto-generated from OWL file *}).
status(satisfiable).
description({* obtained from OWL file pizza.owl through its standard FOL translation *}).
end_of_list.

list_of_symbols.
predicates[
  (hasBase, 2),
  (hasIngredient, 2),
  (hasSpiciness, 2),
  (hasTopping, 2),
  (_A1, 1),
  (_A2, 1),
  (_A3, 1),
  (_A4, 1),
  (_A5, 1),
  (_A6, 1),
  (American, 1),
  (AmericanHot, 1),
  (AnchoviesTopping, 1),
  (ArtichokeTopping, 1),
  (AsparagusTopping, 1),
  (Cajun, 1),
  (CajunSpiceTopping, 1),
  (CaperTopping, 1),
  (Capricciosa, 1),
  (Caprina, 1),
  (CheeseTopping, 1),
  (CheeseyPizza, 1),
  (CheeseyVegetableTopping, 1),
  (ChickenTopping, 1),
  (DeepPanBase, 1),
  (DomainConcept, 1),
  (Fiorentina, 1),
  (FishTopping, 1),
  (Food, 1),
  (FourCheesesTopping, 1),
  (FourSeasons, 1),
  (FruitTopping, 1),
  (FruttiDiMare, 1),
  (GarlicTopping, 1),
  (Giardiniera, 1),
  (GoatsCheeseTopping, 1),
  (GorgonzolaTopping, 1),
  (GreenPepperTopping, 1),
  (HamTopping, 1),
  (HerbSpiceTopping, 1),
  (Hot, 1),
  (HotGreenPepperTopping, 1),
  (HotSpicedBeefTopping, 1),
  (IceCream, 1),
  (JalapenoPepperTopping, 1),
  (LaReine, 1),
  (LeekTopping, 1),
  (Margherita, 1),
  (MeatTopping, 1),
  (MeatyPizza, 1),
  (Medium, 1),
  (Mild, 1),
  (MixedSeafoodTopping, 1),
  (MozzarellaTopping, 1),
  (Mushroom, 1),
  (MushroomTopping, 1),
  (NamedPizza, 1),
  (Napoletana, 1),
  (NutTopping, 1),
  (OliveTopping, 1),
  (OnionTopping, 1),
  (ParmaHamTopping, 1),
  (Parmense, 1),
  (ParmesanTopping, 1),
  (PeperonataTopping, 1),
  (PeperoniSausageTopping, 1),
  (PepperTopping, 1),
  (PetitPoisTopping, 1),
  (PineKernels, 1),
  (Pizza, 1),
  (PizzaBase, 1),
  (PizzaTopping, 1),
  (PolloAdAstra, 1),
  (PrawnsTopping, 1),
  (PrinceCarlo, 1),
  (QuattroFormaggi, 1),
  (RedOnionTopping, 1),
  (RocketTopping, 1),
  (Rosa, 1),
  (RosemaryTopping, 1),
  (SauceTopping, 1),
  (Siciliana, 1),
  (SlicedTomatoTopping, 1),
  (SloppyGiuseppe, 1),
  (Soho, 1),
  (Spiciness, 1),
  (SpicyPizza, 1),
  (SpicyPizzaEquivalent, 1),
  (SpicyTopping, 1),
  (SpinachTopping, 1),
  (SultanaTopping, 1),
  (SundriedTomatoTopping, 1),
  (SweetPepperTopping, 1),
  (ThinAndCrispyBase, 1),
  (TobascoPepperSauce, 1),
  (TomatoTopping, 1),
  (UnclosedPizza, 1),
  (ValuePartition, 1),
  (VegetableTopping, 1),
  (Veneziana, 1),
  (Thing, 1)
].
end_of_list.

list_of_formulae(axioms).
formula(forall([X1], implies(PetitPoisTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Mild(X2)))))).
formula(forall([X1], implies(Veneziana(X1), exists([X2], and(hasTopping(X1, X2), OliveTopping(X2)))))).
formula(forall([X1], implies(Caprina(X1), exists([X2], and(hasTopping(X1, X2), GoatsCheeseTopping(X2)))))).
formula(forall([X1], implies(GoatsCheeseTopping(X1), CheeseTopping(X1)))).
formula(forall([X1], implies(SpicyPizzaEquivalent(X1), exists([X2], and(hasTopping(X1, X2), _A4(X2)))))).
formula(forall([X1], implies(Siciliana(X1), exists([X2], and(hasTopping(X1, X2), HamTopping(X2)))))).
formula(forall([X1], implies(SpicyPizza(X1), exists([X2], and(hasTopping(X1, X2), SpicyTopping(X2)))))).
formula(forall([X1], implies(PrawnsTopping(X1), FishTopping(X1)))).
formula(forall([X1], implies(Caprina(X1), exists([X2], and(hasTopping(X1, X2), SundriedTomatoTopping(X2)))))).
formula(forall([X1], implies(FruttiDiMare(X1), exists([X2], and(hasTopping(X1, X2), GarlicTopping(X2)))))).
formula(forall([X1], implies(AsparagusTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Mild(X2)))))).
formula(forall([X1], implies(LaReine(X1), exists([X2], and(hasTopping(X1, X2), MozzarellaTopping(X2)))))).
formula(forall([X1], implies(RosemaryTopping(X1), HerbSpiceTopping(X1)))).
formula(forall([X1], implies(Fiorentina(X1), exists([X2], and(hasTopping(X1, X2), SpinachTopping(X2)))))).
formula(forall([X1], implies(Giardiniera(X1), exists([X2], and(hasTopping(X1, X2), MushroomTopping(X2)))))).
formula(forall([X1], implies(Pizza(X1), exists([X2], and(hasBase(X1, X2), PizzaBase(X2)))))).
formula(forall([X1], implies(Capricciosa(X1), exists([X2], and(hasTopping(X1, X2), AnchoviesTopping(X2)))))).
formula(forall([X1], implies(Spiciness(X1), ValuePartition(X1)))).
formula(forall([X1], implies(Cajun(X1), exists([X2], and(hasTopping(X1, X2), PeperonataTopping(X2)))))).
formula(forall([X1], implies(American(X1), NamedPizza(X1)))).
formula(forall([X1], implies(AnchoviesTopping(X1), FishTopping(X1)))).
formula(forall([X1], implies(LaReine(X1), exists([X2], and(hasTopping(X1, X2), OliveTopping(X2)))))).
formula(forall([X1], implies(CheeseyVegetableTopping(X1), VegetableTopping(X1)))).
formula(forall([X1], implies(Soho(X1), exists([X2], and(hasTopping(X1, X2), MozzarellaTopping(X2)))))).
formula(forall([X1], implies(Food(X1), DomainConcept(X1)))).
formula(forall([X1], implies(CheeseTopping(X1), PizzaTopping(X1)))).
formula(forall([X1], implies(ChickenTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Mild(X2)))))).
formula(forall([X1], implies(Siciliana(X1), exists([X2], and(hasTopping(X1, X2), TomatoTopping(X2)))))).
formula(forall([X1], implies(GorgonzolaTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Mild(X2)))))).
formula(forall([X1], implies(Giardiniera(X1), exists([X2], and(hasTopping(X1, X2), SlicedTomatoTopping(X2)))))).
formula(forall([X1], implies(SloppyGiuseppe(X1), exists([X2], and(hasTopping(X1, X2), MozzarellaTopping(X2)))))).
formula(forall([X1], implies(Veneziana(X1), exists([X2], and(hasTopping(X1, X2), CaperTopping(X2)))))).
formula(forall([X1], implies(ArtichokeTopping(X1), VegetableTopping(X1)))).
formula(forall([X1], implies(Giardiniera(X1), exists([X2], and(hasTopping(X1, X2), MozzarellaTopping(X2)))))).
formula(forall([X1], implies(exists([X2], and(hasTopping(X1, X2), MeatTopping(X2))), _A3(X1)))).
formula(forall([X1], implies(PeperonataTopping(X1), PepperTopping(X1)))).
formula(forall([X1], implies(PrinceCarlo(X1), exists([X2], and(hasTopping(X1, X2), MozzarellaTopping(X2)))))).
formula(forall([X1], implies(PolloAdAstra(X1), exists([X2], and(hasTopping(X1, X2), SweetPepperTopping(X2)))))).
formula(forall([X1], implies(MushroomTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Mild(X2)))))).
formula(forall([X1], implies(CheeseyPizza(X1), exists([X2], and(hasTopping(X1, X2), CheeseTopping(X2)))))).
formula(forall([X1], implies(Giardiniera(X1), NamedPizza(X1)))).
formula(forall([X1], implies(CajunSpiceTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Hot(X2)))))).
formula(forall([X1], implies(TomatoTopping(X1), VegetableTopping(X1)))).
formula(forall([X1], implies(Hot(X1), Spiciness(X1)))).
formula(forall([X1], implies(Soho(X1), NamedPizza(X1)))).
formula(forall([X1], implies(RocketTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Medium(X2)))))).
formula(forall([X1], implies(ArtichokeTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Mild(X2)))))).
formula(forall([X1], implies(CheeseyPizza(X1), Pizza(X1)))).
formula(forall([X1], implies(_A4(X1), PizzaTopping(X1)))).
formula(forall([X1], implies(AmericanHot(X1), exists([X2], and(hasTopping(X1, X2), MozzarellaTopping(X2)))))).
formula(forall([X1], implies(Rosa(X1), NamedPizza(X1)))).
formula(forall([X1], implies(Mushroom(X1), NamedPizza(X1)))).
formula(forall([X1], implies(FourSeasons(X1), exists([X2], and(hasTopping(X1, X2), PeperoniSausageTopping(X2)))))).
formula(forall([X1], implies(Capricciosa(X1), NamedPizza(X1)))).
formula(forall([X1], implies(exists([X2], and(hasTopping(X1, X2), SpicyTopping(X2))), _A6(X1)))).
formula(forall([X1], implies(TomatoTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Mild(X2)))))).
formula(forall([X1], implies(LeekTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Mild(X2)))))).
formula(forall([X1], implies(_A4(X1), exists([X2], and(hasSpiciness(X1, X2), Hot(X2)))))).
formula(forall([X1], implies(NutTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Mild(X2)))))).
formula(forall([X1], implies(Capricciosa(X1), exists([X2], and(hasTopping(X1, X2), HamTopping(X2)))))).
formula(forall([X1], implies(Napoletana(X1), exists([X2], and(hasTopping(X1, X2), CaperTopping(X2)))))).
formula(forall([X1], implies(SpicyTopping(X1), PizzaTopping(X1)))).
formula(forall([X1], implies(Cajun(X1), NamedPizza(X1)))).
formula(forall([X1], implies(GreenPepperTopping(X1), PepperTopping(X1)))).
formula(forall([X1], implies(HotSpicedBeefTopping(X1), MeatTopping(X1)))).
formula(forall([X1], implies(FourSeasons(X1), exists([X2], and(hasTopping(X1, X2), OliveTopping(X2)))))).
formula(forall([X1], implies(QuattroFormaggi(X1), exists([X2], and(hasTopping(X1, X2), FourCheesesTopping(X2)))))).
formula(forall([X1], implies(NamedPizza(X1), Pizza(X1)))).
formula(forall([X1], implies(SweetPepperTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Mild(X2)))))).
formula(forall([X1], implies(Caprina(X1), exists([X2], and(hasTopping(X1, X2), TomatoTopping(X2)))))).
formula(forall([X1], implies(CaperTopping(X1), VegetableTopping(X1)))).
formula(forall([X1], implies(PolloAdAstra(X1), exists([X2], and(hasTopping(X1, X2), RedOnionTopping(X2)))))).
formula(forall([X1], implies(Parmense(X1), exists([X2], and(hasTopping(X1, X2), MozzarellaTopping(X2)))))).
formula(forall([X1], implies(Mushroom(X1), exists([X2], and(hasTopping(X1, X2), MozzarellaTopping(X2)))))).
formula(forall([X1], implies(Capricciosa(X1), exists([X2], and(hasTopping(X1, X2), MozzarellaTopping(X2)))))).
formula(forall([X1], implies(AmericanHot(X1), exists([X2], and(hasTopping(X1, X2), TomatoTopping(X2)))))).
formula(forall([X1], implies(OnionTopping(X1), VegetableTopping(X1)))).
formula(forall([X1], implies(Soho(X1), exists([X2], and(hasTopping(X1, X2), ParmesanTopping(X2)))))).
formula(forall([X1], implies(Giardiniera(X1), exists([X2], and(hasTopping(X1, X2), LeekTopping(X2)))))).
formula(forall([X1], implies(RosemaryTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Mild(X2)))))).
formula(forall([X1], implies(Siciliana(X1), exists([X2], and(hasTopping(X1, X2), MozzarellaTopping(X2)))))).
formula(forall([X1], implies(FourCheesesTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Mild(X2)))))).
formula(forall([X1], implies(PrinceCarlo(X1), exists([X2], and(hasTopping(X1, X2), LeekTopping(X2)))))).
formula(forall([X1], implies(Siciliana(X1), exists([X2], and(hasTopping(X1, X2), AnchoviesTopping(X2)))))).
formula(forall([X1], implies(Capricciosa(X1), exists([X2], and(hasTopping(X1, X2), TomatoTopping(X2)))))).
formula(forall([X1], implies(PolloAdAstra(X1), exists([X2], and(hasTopping(X1, X2), MozzarellaTopping(X2)))))).
formula(forall([X1], implies(exists([X2], and(hasBase(X1, X2), true)), Pizza(X1)))).
formula(forall([X1], implies(Rosa(X1), exists([X2], and(hasTopping(X1, X2), MozzarellaTopping(X2)))))).
formula(forall([X1], implies(TobascoPepperSauce(X1), SauceTopping(X1)))).
formula(forall([X1], implies(SlicedTomatoTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Mild(X2)))))).
formula(forall([X1], implies(PeperonataTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Medium(X2)))))).
formula(forall([X1], implies(GorgonzolaTopping(X1), CheeseTopping(X1)))).
formula(forall([X1], implies(Soho(X1), exists([X2], and(hasTopping(X1, X2), GarlicTopping(X2)))))).
formula(forall([X1], implies(HotGreenPepperTopping(X1), GreenPepperTopping(X1)))).
formula(forall([X1], implies(Veneziana(X1), exists([X2], and(hasTopping(X1, X2), TomatoTopping(X2)))))).
formula(forall([X1], implies(Mild(X1), Spiciness(X1)))).
formula(forall([X1], implies(and(_A2(X1), Pizza(X1)), CheeseyPizza(X1)))).
formula(forall([X1], implies(PepperTopping(X1), VegetableTopping(X1)))).
formula(forall([X1], implies(SweetPepperTopping(X1), PepperTopping(X1)))).
formula(forall([X1], implies(LaReine(X1), exists([X2], and(hasTopping(X1, X2), MushroomTopping(X2)))))).
formula(forall([X1], implies(HotGreenPepperTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Hot(X2)))))).
formula(forall([X1], implies(FourSeasons(X1), exists([X2], and(hasTopping(X1, X2), CaperTopping(X2)))))).
formula(forall([X1], implies(MozzarellaTopping(X1), CheeseTopping(X1)))).
formula(forall([X1], implies(American(X1), exists([X2], and(hasTopping(X1, X2), MozzarellaTopping(X2)))))).
formula(forall([X1], implies(Pizza(X1), Food(X1)))).
formula(forall([X1], implies(SultanaTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Medium(X2)))))).
formula(forall([X1], implies(Giardiniera(X1), exists([X2], and(hasTopping(X1, X2), PeperonataTopping(X2)))))).
formula(forall([X1], implies(CheeseyVegetableTopping(X1), CheeseTopping(X1)))).
formula(forall([X1], implies(and(_A6(X1), Pizza(X1)), SpicyPizza(X1)))).
formula(forall([X1], implies(HerbSpiceTopping(X1), PizzaTopping(X1)))).
formula(forall([X1], implies(PolloAdAstra(X1), exists([X2], and(hasTopping(X1, X2), ChickenTopping(X2)))))).
formula(forall([X1], implies(Medium(X1), Spiciness(X1)))).
formula(forall([X1], implies(AmericanHot(X1), exists([X2], and(hasTopping(X1, X2), HotGreenPepperTopping(X2)))))).
formula(forall([X1], implies(Parmense(X1), exists([X2], and(hasTopping(X1, X2), ParmesanTopping(X2)))))).
formula(forall([X1], implies(Soho(X1), exists([X2], and(hasTopping(X1, X2), TomatoTopping(X2)))))).
formula(forall([X1], implies(SpinachTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Mild(X2)))))).
formula(forall([X1], implies(MozzarellaTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Mild(X2)))))).
formula(forall([X1], implies(FishTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Mild(X2)))))).
formula(forall([X1], implies(Capricciosa(X1), exists([X2], and(hasTopping(X1, X2), PeperonataTopping(X2)))))).
formula(forall([X1], implies(PeperoniSausageTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Medium(X2)))))).
formula(forall([X1], implies(ParmesanTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Mild(X2)))))).
formula(forall([X1], implies(HotSpicedBeefTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Hot(X2)))))).
formula(forall([X1], implies(FourSeasons(X1), exists([X2], and(hasTopping(X1, X2), MozzarellaTopping(X2)))))).
formula(forall([X1], implies(Veneziana(X1), exists([X2], and(hasTopping(X1, X2), MozzarellaTopping(X2)))))).
formula(forall([X1], implies(Soho(X1), exists([X2], and(hasTopping(X1, X2), OliveTopping(X2)))))).
formula(forall([X1], implies(MeatyPizza(X1), exists([X2], and(hasTopping(X1, X2), MeatTopping(X2)))))).
formula(forall([X1], implies(JalapenoPepperTopping(X1), PepperTopping(X1)))).
formula(forall([X1], implies(PeperoniSausageTopping(X1), MeatTopping(X1)))).
formula(forall([X1], implies(Napoletana(X1), NamedPizza(X1)))).
formula(forall([X1], implies(PrinceCarlo(X1), exists([X2], and(hasTopping(X1, X2), RosemaryTopping(X2)))))).
formula(forall([X1], implies(and(_A1(X1), PizzaTopping(X1)), SpicyTopping(X1)))).
formula(forall([X1], implies(SpicyPizza(X1), Pizza(X1)))).
formula(forall([X1], implies(Siciliana(X1), exists([X2], and(hasTopping(X1, X2), GarlicTopping(X2)))))).
formula(forall([X1], implies(PizzaBase(X1), Food(X1)))).
formula(forall([X1], implies(Giardiniera(X1), exists([X2], and(hasTopping(X1, X2), TomatoTopping(X2)))))).
formula(forall([X1], implies(SultanaTopping(X1), FruitTopping(X1)))).
formula(forall([X1], implies(Napoletana(X1), exists([X2], and(hasTopping(X1, X2), TomatoTopping(X2)))))).
formula(forall([X1], implies(TobascoPepperSauce(X1), exists([X2], and(hasSpiciness(X1, X2), Hot(X2)))))).
formula(forall([X1], implies(MeatTopping(X1), PizzaTopping(X1)))).
formula(forall([X1], implies(RedOnionTopping(X1), OnionTopping(X1)))).
formula(forall([X1], implies(Giardiniera(X1), exists([X2], and(hasTopping(X1, X2), PetitPoisTopping(X2)))))).
formula(forall([X1], implies(PolloAdAstra(X1), NamedPizza(X1)))).
formula(forall([X1], implies(Mushroom(X1), exists([X2], and(hasTopping(X1, X2), TomatoTopping(X2)))))).
formula(forall([X1], implies(PrinceCarlo(X1), exists([X2], and(hasTopping(X1, X2), ParmesanTopping(X2)))))).
formula(forall([X1], implies(GarlicTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Medium(X2)))))).
formula(forall([X1], implies(Margherita(X1), exists([X2], and(hasTopping(X1, X2), MozzarellaTopping(X2)))))).
formula(forall([X1], implies(Capricciosa(X1), exists([X2], and(hasTopping(X1, X2), CaperTopping(X2)))))).
formula(forall([X1], implies(FourSeasons(X1), exists([X2], and(hasTopping(X1, X2), AnchoviesTopping(X2)))))).
formula(forall([X1], implies(SloppyGiuseppe(X1), exists([X2], and(hasTopping(X1, X2), HotSpicedBeefTopping(X2)))))).
formula(forall([X1], implies(UnclosedPizza(X1), Pizza(X1)))).
formula(forall([X1], implies(Napoletana(X1), exists([X2], and(hasTopping(X1, X2), MozzarellaTopping(X2)))))).
formula(forall([X1], implies(FishTopping(X1), PizzaTopping(X1)))).
formula(forall([X1], implies(AsparagusTopping(X1), VegetableTopping(X1)))).
formula(forall([X1], implies(PolloAdAstra(X1), exists([X2], and(hasTopping(X1, X2), GarlicTopping(X2)))))).
formula(forall([X1], implies(OliveTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Mild(X2)))))).
formula(forall([X1], implies(SpicyTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Hot(X2)))))).
formula(forall([X1], implies(exists([X2], and(hasIngredient(X1, X2), true)), Food(X1)))).
formula(forall([X1], implies(Veneziana(X1), exists([X2], and(hasTopping(X1, X2), PineKernels(X2)))))).
formula(forall([X1], implies(OnionTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Medium(X2)))))).
formula(forall([X1], implies(Fiorentina(X1), exists([X2], and(hasTopping(X1, X2), GarlicTopping(X2)))))).
formula(forall([X1], implies(Siciliana(X1), exists([X2], and(hasTopping(X1, X2), OliveTopping(X2)))))).
formula(forall([X1], implies(LaReine(X1), exists([X2], and(hasTopping(X1, X2), HamTopping(X2)))))).
formula(forall([X1], implies(SloppyGiuseppe(X1), exists([X2], and(hasTopping(X1, X2), GreenPepperTopping(X2)))))).
formula(forall([X1], implies(Giardiniera(X1), exists([X2], and(hasTopping(X1, X2), OliveTopping(X2)))))).
formula(forall([X1], implies(Rosa(X1), exists([X2], and(hasTopping(X1, X2), GorgonzolaTopping(X2)))))).
formula(forall([X1], implies(SloppyGiuseppe(X1), exists([X2], and(hasTopping(X1, X2), OnionTopping(X2)))))).
formula(forall([X1], implies(Veneziana(X1), exists([X2], and(hasTopping(X1, X2), SultanaTopping(X2)))))).
formula(forall([X1], implies(LaReine(X1), exists([X2], and(hasTopping(X1, X2), TomatoTopping(X2)))))).
formula(forall([X1], implies(Fiorentina(X1), exists([X2], and(hasTopping(X1, X2), ParmesanTopping(X2)))))).
formula(forall([X1], implies(QuattroFormaggi(X1), NamedPizza(X1)))).
formula(forall([X1], implies(Cajun(X1), exists([X2], and(hasTopping(X1, X2), OnionTopping(X2)))))).
formula(forall([X1], implies(Veneziana(X1), NamedPizza(X1)))).
formula(forall([X1], implies(ParmesanTopping(X1), CheeseTopping(X1)))).
formula(forall([X1], implies(Fiorentina(X1), exists([X2], and(hasTopping(X1, X2), OliveTopping(X2)))))).
formula(forall([X1], implies(FourSeasons(X1), exists([X2], and(hasTopping(X1, X2), MushroomTopping(X2)))))).
formula(forall([X1], implies(GoatsCheeseTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Mild(X2)))))).
formula(forall([X1], implies(CaperTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Mild(X2)))))).
formula(forall([X1], implies(Soho(X1), exists([X2], and(hasTopping(X1, X2), RocketTopping(X2)))))).
formula(forall([X1], implies(SloppyGiuseppe(X1), NamedPizza(X1)))).
formula(forall([X1], implies(MushroomTopping(X1), VegetableTopping(X1)))).
formula(forall([X1], implies(SpinachTopping(X1), VegetableTopping(X1)))).
formula(forall([X1], implies(Mushroom(X1), exists([X2], and(hasTopping(X1, X2), MushroomTopping(X2)))))).
formula(forall([X1], implies(FruitTopping(X1), PizzaTopping(X1)))).
formula(forall([X1], implies(AmericanHot(X1), NamedPizza(X1)))).
formula(forall([X1], implies(Caprina(X1), NamedPizza(X1)))).
formula(forall([X1], implies(Margherita(X1), NamedPizza(X1)))).
formula(forall([X1], implies(DeepPanBase(X1), PizzaBase(X1)))).
formula(forall([X1], implies(AmericanHot(X1), exists([X2], and(hasTopping(X1, X2), PeperoniSausageTopping(X2)))))).
formula(forall([X1], implies(Fiorentina(X1), exists([X2], and(hasTopping(X1, X2), MozzarellaTopping(X2)))))).
formula(forall([X1], implies(MeatyPizza(X1), Pizza(X1)))).
formula(forall([X1], implies(Fiorentina(X1), exists([X2], and(hasTopping(X1, X2), TomatoTopping(X2)))))).
formula(forall([X1], implies(and(_A1(X1), PizzaTopping(X1)), _A4(X1)))).
formula(forall([X1], implies(Capricciosa(X1), exists([X2], and(hasTopping(X1, X2), OliveTopping(X2)))))).
formula(forall([X1], implies(VegetableTopping(X1), PizzaTopping(X1)))).
formula(forall([X1], implies(GarlicTopping(X1), VegetableTopping(X1)))).
formula(forall([X1], implies(American(X1), exists([X2], and(hasTopping(X1, X2), TomatoTopping(X2)))))).
formula(forall([X1], implies(Cajun(X1), exists([X2], and(hasTopping(X1, X2), PrawnsTopping(X2)))))).
formula(forall([X1], implies(OliveTopping(X1), VegetableTopping(X1)))).
formula(forall([X1], implies(Siciliana(X1), NamedPizza(X1)))).
formula(forall([X1], implies(exists([X2], and(hasTopping(X1, X2), _A4(X2))), _A5(X1)))).
formula(forall([X1], implies(Napoletana(X1), exists([X2], and(hasTopping(X1, X2), AnchoviesTopping(X2)))))).
formula(forall([X1], implies(Veneziana(X1), exists([X2], and(hasTopping(X1, X2), OnionTopping(X2)))))).
formula(forall([X1], implies(LaReine(X1), NamedPizza(X1)))).
formula(forall([X1], implies(HamTopping(X1), MeatTopping(X1)))).
formula(forall([X1], implies(Napoletana(X1), exists([X2], and(hasTopping(X1, X2), OliveTopping(X2)))))).
formula(forall([X1], implies(UnclosedPizza(X1), exists([X2], and(hasTopping(X1, X2), MozzarellaTopping(X2)))))).
formula(forall([X1], implies(ThinAndCrispyBase(X1), PizzaBase(X1)))).
formula(forall([X1], implies(SundriedTomatoTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Mild(X2)))))).
formula(forall([X1], implies(PetitPoisTopping(X1), VegetableTopping(X1)))).
formula(forall([X1], implies(Rosa(X1), exists([X2], and(hasTopping(X1, X2), TomatoTopping(X2)))))).
formula(forall([X1], implies(SlicedTomatoTopping(X1), TomatoTopping(X1)))).
formula(forall([X1], implies(SpicyPizzaEquivalent(X1), Pizza(X1)))).
formula(forall([X1], implies(Margherita(X1), exists([X2], and(hasTopping(X1, X2), TomatoTopping(X2)))))).
formula(forall([X1], implies(ParmaHamTopping(X1), HamTopping(X1)))).
formula(forall([X1], implies(PizzaTopping(X1), Food(X1)))).
formula(forall([X1], implies(Fiorentina(X1), NamedPizza(X1)))).
formula(forall([X1], implies(Cajun(X1), exists([X2], and(hasTopping(X1, X2), MozzarellaTopping(X2)))))).
formula(forall([X1], implies(PineKernels(X1), NutTopping(X1)))).
formula(forall([X1], implies(SloppyGiuseppe(X1), exists([X2], and(hasTopping(X1, X2), TomatoTopping(X2)))))).
formula(forall([X1], implies(ChickenTopping(X1), MeatTopping(X1)))).
formula(forall([X1], implies(FourSeasons(X1), NamedPizza(X1)))).
formula(forall([X1], implies(CajunSpiceTopping(X1), HerbSpiceTopping(X1)))).
formula(forall([X1], implies(American(X1), exists([X2], and(hasTopping(X1, X2), PeperoniSausageTopping(X2)))))).
formula(forall([X1], implies(LeekTopping(X1), VegetableTopping(X1)))).
formula(forall([X1], implies(Parmense(X1), exists([X2], and(hasTopping(X1, X2), TomatoTopping(X2)))))).
formula(forall([X1], implies(Cajun(X1), exists([X2], and(hasTopping(X1, X2), TobascoPepperSauce(X2)))))).
formula(forall([X1], implies(MixedSeafoodTopping(X1), FishTopping(X1)))).
formula(forall([X1], implies(SauceTopping(X1), PizzaTopping(X1)))).
formula(forall([X1], implies(and(_A3(X1), Pizza(X1)), MeatyPizza(X1)))).
formula(forall([X1], implies(PrinceCarlo(X1), NamedPizza(X1)))).
formula(forall([X1], implies(Caprina(X1), exists([X2], and(hasTopping(X1, X2), MozzarellaTopping(X2)))))).
formula(forall([X1], implies(Parmense(X1), exists([X2], and(hasTopping(X1, X2), HamTopping(X2)))))).
formula(forall([X1], implies(FruttiDiMare(X1), exists([X2], and(hasTopping(X1, X2), TomatoTopping(X2)))))).
formula(forall([X1], implies(QuattroFormaggi(X1), exists([X2], and(hasTopping(X1, X2), TomatoTopping(X2)))))).
formula(forall([X1], implies(PrinceCarlo(X1), exists([X2], and(hasTopping(X1, X2), TomatoTopping(X2)))))).
formula(forall([X1], implies(AmericanHot(X1), exists([X2], and(hasTopping(X1, X2), JalapenoPepperTopping(X2)))))).
formula(forall([X1], implies(PolloAdAstra(X1), exists([X2], and(hasTopping(X1, X2), TomatoTopping(X2)))))).
formula(forall([X1], implies(IceCream(X1), Food(X1)))).
formula(forall([X1], implies(and(_A5(X1), Pizza(X1)), SpicyPizzaEquivalent(X1)))).
formula(forall([X1], implies(PolloAdAstra(X1), exists([X2], and(hasTopping(X1, X2), CajunSpiceTopping(X2)))))).
formula(forall([X1], implies(Parmense(X1), NamedPizza(X1)))).
formula(forall([X1], implies(FruttiDiMare(X1), NamedPizza(X1)))).
formula(forall([X1], implies(FourSeasons(X1), exists([X2], and(hasTopping(X1, X2), TomatoTopping(X2)))))).
formula(forall([X1], implies(exists([X2], and(hasTopping(X1, X2), true)), Pizza(X1)))).
formula(forall([X1], implies(FruttiDiMare(X1), exists([X2], and(hasTopping(X1, X2), MixedSeafoodTopping(X2)))))).
formula(forall([X1], implies(Parmense(X1), exists([X2], and(hasTopping(X1, X2), AsparagusTopping(X2)))))).
formula(forall([X1], implies(Cajun(X1), exists([X2], and(hasTopping(X1, X2), TomatoTopping(X2)))))).
formula(forall([X1], implies(FourCheesesTopping(X1), CheeseTopping(X1)))).
formula(forall([X1], implies(ParmaHamTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Mild(X2)))))).
formula(forall([X1], implies(NutTopping(X1), PizzaTopping(X1)))).
formula(forall([X1], implies(Siciliana(X1), exists([X2], and(hasTopping(X1, X2), ArtichokeTopping(X2)))))).
formula(forall([X1], implies(exists([X2], and(hasSpiciness(X1, X2), Hot(X2))), _A1(X1)))).
formula(forall([X1], implies(RocketTopping(X1), VegetableTopping(X1)))).
formula(forall([X1], implies(SundriedTomatoTopping(X1), TomatoTopping(X1)))).
formula(forall([X1], implies(exists([X2], and(hasTopping(X1, X2), CheeseTopping(X2))), _A2(X1)))).
formula(forall([X1], implies(IceCream(X1), exists([X2], and(hasTopping(X1, X2), FruitTopping(X2)))))).
formula(forall([X1], implies(JalapenoPepperTopping(X1), exists([X2], and(hasSpiciness(X1, X2), Hot(X2)))))).
end_of_list.

end_problem.

