%------------------------------------------------------------------------------
% File : Mace4---2026-6A
% Problem : PRD002+1 : TPTP v9.3.1. Released v6.2.0.
% Transfm : none
% Format : tptp:raw
% Command : mace4 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:20:30 AM UTC 2026
% Result : CounterSatisfiable 0.22s 20.58s
% Output : FiniteModel 0.22s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(interp_domain,interpretation-domains,
! [X] :
( X = "d1"
| X = "d0" ) ).
fof(interp_functions,interpretation-mappings,
( zinfandelgrape = "d0"
& year1998 = "d1"
& whitehalllaneprimavera = "d1"
& whitehalllanecabernetfranc = "d1"
& whitehalllane = "d1"
& white = "d1"
& ventanacheninblanc = "d1"
& ventana = "d1"
& usregion = "d1"
& toursregion = "d0"
& texasregion = "d1"
& taylorport = "d1"
& taylor = "d1"
& sweet = "d1"
& strong = "d1"
& stonleighsauvignonblanc = "d1"
& stonleigh = "d1"
& stgenevievetexaswhite = "d1"
& stgenevieve = "d1"
& stemilionregion = "d0"
& southaustraliaregion = "d1"
& sonomaregion = "d1"
& sevreetmainemuscadet = "d1"
& sevreetmaine = "d1"
& semillongrape = "d1"
& selakssauvignonblanc = "d1"
& selaksicewine = "d1"
& selaks = "d1"
& seanthackreysiriuspetitesyrah = "d1"
& seanthackrey = "d1"
& schlossvolradtrochenbierenausleseriesling = "d1"
& schlossvolrad = "d1"
& schlossrothermeltrochenbierenausleseriesling = "d1"
& schlossrothermel = "d1"
& sauvignonblancgrape = "d1"
& sauterneregion = "d0"
& saucelitocanyonzinfandel1998 = "d1"
& saucelitocanyonzinfandel = "d1"
& saucelitocanyon = "d1"
& santacruzmountainvineyardcabernetsauvignon = "d1"
& santacruzmountainvineyard = "d1"
& santacruzmountainsregion = "d1"
& santabarbararegion = "d1"
& sangiovesegrape = "d0"
& sancerreregion = "d0"
& rosedanjou = "d1"
& rose = "d0"
& rieslinggrape = "d0"
& red = "d0"
& pulignymontrachetwhiteburgundy = "d1"
& pulignymontrachet = "d1"
& portugalregion = "d0"
& pinotnoirgrape = "d0"
& pinotblancgrape = "d0"
& petiteverdotgrape = "d0"
& petitesyrahgrape = "d0"
& petermccoychardonnay = "d1"
& petermccoy = "d1"
& pauillacregion = "d0"
& pagemillwinerycabernetsauvignon = "d1"
& pagemillwinery = "d1"
& offdry = "d1"
& newzealandregion = "d1"
& naparegion = "d1"
& muscadetregion = "d0"
& mountedenvineyardestatepinotnoir = "d1"
& mountedenvineyardednavalleychardonnay = "d1"
& mountedenvineyard = "d1"
& mountadamriesling = "d1"
& mountadampinotnoir = "d1"
& mountadamchardonnay = "d1"
& mountadam = "d1"
& moderate = "d1"
& meursaultregion = "d0"
& merlotgrape = "d0"
& mendocinoregion = "d0"
& medocregion = "d0"
& medium = "d1"
& mcguinnesso = "d1"
& mariettazinfandel = "d1"
& mariettapetitesyrah = "d1"
& mariettaoldvinesred = "d1"
& mariettacabernetsauvignon = "d1"
& marietta = "d1"
& margauxregion = "d0"
& malbecgrape = "d0"
& longridgemerlot = "d1"
& longridge = "d1"
& loireregion = "d0"
& light = "d1"
& lanetannerpinotnoir = "d1"
& lanetanner = "d1"
& kathrynkennedylateral = "d1"
& kathrynkennedy = "d1"
& kalincellarssemillon = "d1"
& kalincellars = "d1"
& italianregion = "d0"
& handley = "d0"
& germanyregion = "d1"
& garyfarrellmerlot = "d1"
& garyfarrell = "d1"
& gamaygrape = "d0"
& full = "d1"
& frenchregion = "d0"
& foxencheninblanc = "d1"
& foxen = "d1"
& formanchardonnay = "d1"
& formancabernetsauvignon = "d1"
& forman = "d1"
& elysezinfandel = "d1"
& elyse = "d1"
& ednavalleyregion = "d1"
& dry = "d1"
& delicate = "d1"
& danjou = "d1"
& cotturizinfandel = "d1"
& cotturi = "d1"
& cotesdorregion = "d0"
& cortonmontrachetwhiteburgundy = "d1"
& cortonmontrachet = "d1"
& corbanssauvignonblanc = "d1"
& corbansprivatebinsauvignonblanc = "d1"
& corbansdrywhiteriesling = "d1"
& corbans = "d1"
& congressspringssemillon = "d1"
& congresssprings = "d1"
& closdevougeotcotesdor = "d1"
& closdevougeot = "d1"
& closdelapoussiesancerre = "d1"
& closdelapoussie = "d1"
& chiantiregion = "d0"
& chianticlassico = "d1"
& cheninblancgrape = "d0"
& chateaumorgonbeaujolais = "d1"
& chateaumorgon = "d1"
& chateaumargauxwinery = "d1"
& chateaumargaux = "d1"
& chateaulafiterothschildpauillac = "d1"
& chateaulafiterothschild = "d1"
& chateaudychemsauterne = "d1"
& chateaudychem = "d1"
& chateaudemeursaultmeursault = "d1"
& chateaudemeursault = "d1"
& chateauchevalblancstemilion = "d1"
& chateauchevalblanc = "d1"
& chardonnaygrape = "d0"
& centraltexasregion = "d1"
& centralcoastregion = "d1"
& californiaregion = "d1"
& cabernetsauvignongrape = "d0"
& cabernetfrancgrape = "d0"
& bourgogneregion = "d0"
& bordeauxregion = "d0"
& beringer = "d0"
& beaujolaisregion = "d0"
& bancroftchardonnay = "d1"
& bancroft = "d1"
& australianregion = "d1"
& arroyogranderegion = "d1"
& anjouregion = "d0"
& alsaceregion = "d0" ) ).
fof(interp_relations,interpretation-mappings,
( produceswine("d1","d1")
& ~ produceswine("d1","d0")
& ~ produceswine("d0","d1")
& ~ produceswine("d0","d0")
& madeintowine("d1","d1")
& ~ madeintowine("d1","d0")
& ~ madeintowine("d0","d1")
& ~ madeintowine("d0","d0")
& madefromgrape_aux("d1","d1")
& ~ madefromgrape_aux("d1","d0")
& ~ madefromgrape_aux("d0","d1")
& ~ madefromgrape_aux("d0","d0")
& madefromgrape("d1","d1")
& ~ madefromgrape("d1","d0")
& ~ madefromgrape("d0","d1")
& ~ madefromgrape("d0","d0")
& madefromfruit("d1","d1")
& ~ madefromfruit("d1","d0")
& ~ madefromfruit("d0","d1")
& ~ madefromfruit("d0","d0")
& locatedin_aux("d1","d1")
& ~ locatedin_aux("d1","d0")
& locatedin_aux("d0","d1")
& locatedin_aux("d0","d0")
& locatedin("d1","d1")
& ~ locatedin("d1","d0")
& locatedin("d0","d1")
& locatedin("d0","d0")
& kaon2equal("d1","d1")
& ~ kaon2equal("d1","d0")
& ~ kaon2equal("d0","d1")
& kaon2equal("d0","d0")
& haswinedescriptor("d1","d1")
& ~ haswinedescriptor("d1","d0")
& ~ haswinedescriptor("d0","d1")
& ~ haswinedescriptor("d0","d0")
& hasvintageyear_aux("d1","d1")
& ~ hasvintageyear_aux("d1","d0")
& ~ hasvintageyear_aux("d0","d1")
& ~ hasvintageyear_aux("d0","d0")
& hasvintageyear("d1","d1")
& ~ hasvintageyear("d1","d0")
& ~ hasvintageyear("d0","d1")
& ~ hasvintageyear("d0","d0")
& hassugar_aux("d1","d1")
& ~ hassugar_aux("d1","d0")
& ~ hassugar_aux("d0","d1")
& ~ hassugar_aux("d0","d0")
& hassugar("d1","d1")
& ~ hassugar("d1","d0")
& ~ hassugar("d0","d1")
& ~ hassugar("d0","d0")
& hasmaker_aux("d1","d1")
& ~ hasmaker_aux("d1","d0")
& ~ hasmaker_aux("d0","d1")
& ~ hasmaker_aux("d0","d0")
& hasmaker("d1","d1")
& ~ hasmaker("d1","d0")
& ~ hasmaker("d0","d1")
& ~ hasmaker("d0","d0")
& hasflavor_aux("d1","d1")
& ~ hasflavor_aux("d1","d0")
& ~ hasflavor_aux("d0","d1")
& ~ hasflavor_aux("d0","d0")
& hasflavor("d1","d1")
& ~ hasflavor("d1","d0")
& ~ hasflavor("d0","d1")
& ~ hasflavor("d0","d0")
& hascolor_aux("d1","d1")
& ~ hascolor_aux("d1","d0")
& ~ hascolor_aux("d0","d1")
& ~ hascolor_aux("d0","d0")
& hascolor("d1","d1")
& ~ hascolor("d1","d0")
& ~ hascolor("d0","d1")
& ~ hascolor("d0","d0")
& hasbody_aux("d1","d1")
& ~ hasbody_aux("d1","d0")
& ~ hasbody_aux("d0","d1")
& ~ hasbody_aux("d0","d0")
& hasbody("d1","d1")
& ~ hasbody("d1","d0")
& ~ hasbody("d0","d1")
& ~ hasbody("d0","d0")
& ~ adjacentregion_aux("d1","d1")
& ~ adjacentregion_aux("d1","d0")
& ~ adjacentregion_aux("d0","d1")
& ~ adjacentregion_aux("d0","d0")
& ~ adjacentregion("d1","d1")
& ~ adjacentregion("d1","d0")
& ~ adjacentregion("d0","d1")
& ~ adjacentregion("d0","d0")
& zinfandel_aux("d1")
& ~ zinfandel_aux("d0")
& zinfandel("d1")
& ~ zinfandel("d0")
& winetaste("d1")
& winetaste("d0")
& winesugar_aux("d1")
& ~ winesugar_aux("d0")
& winesugar("d1")
& ~ winesugar("d0")
& winery_aux("d1")
& winery_aux("d0")
& winery("d1")
& winery("d0")
& winegrape_aux("d1")
& winegrape_aux("d0")
& winegrape("d1")
& winegrape("d0")
& wineflavor_aux("d1")
& ~ wineflavor_aux("d0")
& wineflavor("d1")
& ~ wineflavor("d0")
& winedescriptor("d1")
& winedescriptor("d0")
& winecolor_aux("d1")
& winecolor_aux("d0")
& winecolor("d1")
& winecolor("d0")
& winebody_aux("d1")
& ~ winebody_aux("d0")
& winebody("d1")
& ~ winebody("d0")
& wine("d1")
& ~ wine("d0")
& whitewine_aux("d1")
& ~ whitewine_aux("d0")
& whitewine("d1")
& ~ whitewine("d0")
& whitetablewine("d1")
& ~ whitetablewine("d0")
& whitenonsweetwine("d1")
& ~ whitenonsweetwine("d0")
& whiteloire("d1")
& ~ whiteloire("d0")
& whiteburgundy_aux("d1")
& ~ whiteburgundy_aux("d0")
& whiteburgundy("d1")
& ~ whiteburgundy("d0")
& whitebordeaux("d1")
& ~ whitebordeaux("d0")
& vintageyear_aux("d1")
& ~ vintageyear_aux("d0")
& vintageyear("d1")
& ~ vintageyear("d0")
& vintage("d1")
& ~ vintage("d0")
& ~ tours("d1")
& ~ tours("d0")
& texaswine("d1")
& ~ texaswine("d0")
& tablewine("d1")
& ~ tablewine("d0")
& sweetwine("d1")
& ~ sweetwine("d0")
& sweetriesling_aux("d1")
& ~ sweetriesling_aux("d0")
& sweetriesling("d1")
& ~ sweetriesling("d0")
& stemilion_aux("d1")
& ~ stemilion_aux("d0")
& stemilion("d1")
& ~ stemilion("d0")
& semillonorsauvignonblanc("d1")
& ~ semillonorsauvignonblanc("d0")
& semillon_aux("d1")
& ~ semillon_aux("d0")
& semillon("d1")
& ~ semillon("d0")
& sauvignonblanc_aux("d1")
& ~ sauvignonblanc_aux("d0")
& sauvignonblanc("d1")
& ~ sauvignonblanc("d0")
& sauternes_aux("d1")
& ~ sauternes_aux("d0")
& sauternes("d1")
& ~ sauternes("d0")
& sancerre_aux("d1")
& ~ sancerre_aux("d0")
& sancerre("d1")
& ~ sancerre("d0")
& rosewine("d1")
& ~ rosewine("d0")
& riesling_aux("d1")
& ~ riesling_aux("d0")
& riesling("d1")
& ~ riesling("d0")
& region_aux("d1")
& region_aux("d0")
& region("d1")
& region("d0")
& redwine("d1")
& ~ redwine("d0")
& redtablewine_aux("d1")
& ~ redtablewine_aux("d0")
& redtablewine("d1")
& ~ redtablewine("d0")
& redburgundy("d1")
& ~ redburgundy("d0")
& redbordeaux("d1")
& ~ redbordeaux("d0")
& ~ q9("d1")
& q9("d0")
& q74("d1")
& q74("d0")
& q73("d1")
& q73("d0")
& q72("d1")
& ~ q72("d0")
& q71("d1")
& ~ q71("d0")
& q70("d1")
& ~ q70("d0")
& q7("d1")
& ~ q7("d0")
& q69("d1")
& ~ q69("d0")
& q68("d1")
& ~ q68("d0")
& q67("d1")
& q67("d0")
& q66("d1")
& q66("d0")
& q65("d1")
& q65("d0")
& q64("d1")
& q64("d0")
& q63("d1")
& ~ q63("d0")
& q62("d1")
& q62("d0")
& q61("d1")
& q61("d0")
& ~ q60("d1")
& q60("d0")
& q6("d1")
& ~ q6("d0")
& ~ q59("d1")
& q59("d0")
& q58("d1")
& q58("d0")
& q57("d1")
& q57("d0")
& q56("d1")
& q56("d0")
& q55("d1")
& q55("d0")
& ~ q52("d1")
& q52("d0")
& ~ q51("d1")
& q51("d0")
& q50("d1")
& q50("d0")
& q5("d1")
& ~ q5("d0")
& q49("d1")
& q49("d0")
& q48("d1")
& q48("d0")
& q47("d1")
& q47("d0")
& q46("d1")
& ~ q46("d0")
& q45("d1")
& ~ q45("d0")
& q44("d1")
& ~ q44("d0")
& q43("d1")
& q43("d0")
& q42("d1")
& q42("d0")
& q41("d1")
& ~ q41("d0")
& q40("d1")
& q40("d0")
& q4("d1")
& ~ q4("d0")
& q39("d1")
& q39("d0")
& q38("d1")
& q38("d0")
& q37("d1")
& q37("d0")
& q36("d1")
& ~ q36("d0")
& q35("d1")
& ~ q35("d0")
& q34("d1")
& q34("d0")
& q33("d1")
& q33("d0")
& q32("d1")
& ~ q32("d0")
& q31("d1")
& ~ q31("d0")
& q30("d1")
& q30("d0")
& q3("d1")
& ~ q3("d0")
& q29("d1")
& q29("d0")
& q27("d1")
& q27("d0")
& q26("d1")
& q26("d0")
& q24("d1")
& ~ q24("d0")
& q23("d1")
& q23("d0")
& q22("d1")
& q22("d0")
& q21("d1")
& ~ q21("d0")
& q20("d1")
& ~ q20("d0")
& q2("d1")
& q2("d0")
& q19("d1")
& q19("d0")
& q18("d1")
& q18("d0")
& q17("d1")
& q17("d0")
& q16("d1")
& q16("d0")
& q15("d1")
& ~ q15("d0")
& q14("d1")
& ~ q14("d0")
& q13("d1")
& ~ q13("d0")
& q12("d1")
& ~ q12("d0")
& q11("d1")
& ~ q11("d0")
& ~ q10("d1")
& q10("d0")
& q1("d1")
& q1("d0")
& q0("d1")
& ~ q0("d0")
& potableliquid("d1")
& ~ potableliquid("d0")
& port_aux("d1")
& ~ port_aux("d0")
& port("d1")
& ~ port("d0")
& pinotnoir_aux("d1")
& ~ pinotnoir_aux("d0")
& pinotnoir("d1")
& ~ pinotnoir("d0")
& pinotblanc("d1")
& ~ pinotblanc("d0")
& petitesyrah_aux("d1")
& ~ petitesyrah_aux("d0")
& petitesyrah("d1")
& ~ petitesyrah("d0")
& pauillac_aux("d1")
& ~ pauillac_aux("d0")
& pauillac("d1")
& ~ pauillac("d0")
& ot____nom9_aux("d1")
& ot____nom9_aux("d0")
& ot____nom9("d1")
& ot____nom9("d0")
& ~ ot____nom8_aux("d1")
& ot____nom8_aux("d0")
& ot____nom8("d1")
& ot____nom8("d0")
& ot____nom7_aux("d1")
& ~ ot____nom7_aux("d0")
& ot____nom7("d1")
& ~ ot____nom7("d0")
& ot____nom6_aux("d1")
& ~ ot____nom6_aux("d0")
& ot____nom64_aux("d1")
& ~ ot____nom64_aux("d0")
& ot____nom64("d1")
& ~ ot____nom64("d0")
& ot____nom63_aux("d1")
& ot____nom63_aux("d0")
& ot____nom63("d1")
& ot____nom63("d0")
& ~ ot____nom62_aux("d1")
& ot____nom62_aux("d0")
& ot____nom62("d1")
& ot____nom62("d0")
& ~ ot____nom61_aux("d1")
& ot____nom61_aux("d0")
& ot____nom61("d1")
& ot____nom61("d0")
& ~ ot____nom60_aux("d1")
& ot____nom60_aux("d0")
& ot____nom60("d1")
& ot____nom60("d0")
& ot____nom6("d1")
& ~ ot____nom6("d0")
& ot____nom5_aux("d1")
& ~ ot____nom5_aux("d0")
& ot____nom59_aux("d1")
& ~ ot____nom59_aux("d0")
& ot____nom59("d1")
& ~ ot____nom59("d0")
& ot____nom58_aux("d1")
& ~ ot____nom58_aux("d0")
& ot____nom58("d1")
& ~ ot____nom58("d0")
& ~ ot____nom57_aux("d1")
& ot____nom57_aux("d0")
& ot____nom57("d1")
& ot____nom57("d0")
& ot____nom56_aux("d1")
& ~ ot____nom56_aux("d0")
& ot____nom56("d1")
& ~ ot____nom56("d0")
& ot____nom55_aux("d1")
& ~ ot____nom55_aux("d0")
& ot____nom55("d1")
& ~ ot____nom55("d0")
& ot____nom54_aux("d1")
& ~ ot____nom54_aux("d0")
& ot____nom54("d1")
& ~ ot____nom54("d0")
& ot____nom53_aux("d1")
& ~ ot____nom53_aux("d0")
& ot____nom53("d1")
& ~ ot____nom53("d0")
& ~ ot____nom52_aux("d1")
& ot____nom52_aux("d0")
& ot____nom52("d1")
& ot____nom52("d0")
& ot____nom51_aux("d1")
& ~ ot____nom51_aux("d0")
& ot____nom51("d1")
& ~ ot____nom51("d0")
& ot____nom50_aux("d1")
& ~ ot____nom50_aux("d0")
& ot____nom50("d1")
& ~ ot____nom50("d0")
& ot____nom5("d1")
& ~ ot____nom5("d0")
& ~ ot____nom4_aux("d1")
& ot____nom4_aux("d0")
& ot____nom49_aux("d1")
& ~ ot____nom49_aux("d0")
& ot____nom49("d1")
& ~ ot____nom49("d0")
& ot____nom48_aux("d1")
& ~ ot____nom48_aux("d0")
& ot____nom48("d1")
& ~ ot____nom48("d0")
& ~ ot____nom47_aux("d1")
& ot____nom47_aux("d0")
& ot____nom47("d1")
& ot____nom47("d0")
& ~ ot____nom46_aux("d1")
& ot____nom46_aux("d0")
& ot____nom46("d1")
& ot____nom46("d0")
& ot____nom45_aux("d1")
& ~ ot____nom45_aux("d0")
& ot____nom45("d1")
& ~ ot____nom45("d0")
& ~ ot____nom44_aux("d1")
& ot____nom44_aux("d0")
& ot____nom44("d1")
& ot____nom44("d0")
& ~ ot____nom43_aux("d1")
& ot____nom43_aux("d0")
& ot____nom43("d1")
& ot____nom43("d0")
& ~ ot____nom42_aux("d1")
& ot____nom42_aux("d0")
& ot____nom42("d1")
& ot____nom42("d0")
& ~ ot____nom41_aux("d1")
& ot____nom41_aux("d0")
& ~ ot____nom41("d1")
& ot____nom41("d0")
& ot____nom40_aux("d1")
& ~ ot____nom40_aux("d0")
& ot____nom40("d1")
& ~ ot____nom40("d0")
& ~ ot____nom4("d1")
& ot____nom4("d0")
& ~ ot____nom3_aux("d1")
& ot____nom3_aux("d0")
& ~ ot____nom39_aux("d1")
& ot____nom39_aux("d0")
& ot____nom39("d1")
& ot____nom39("d0")
& ot____nom38_aux("d1")
& ~ ot____nom38_aux("d0")
& ot____nom38("d1")
& ot____nom38("d0")
& ~ ot____nom37_aux("d1")
& ot____nom37_aux("d0")
& ot____nom37("d1")
& ot____nom37("d0")
& ~ ot____nom36_aux("d1")
& ot____nom36_aux("d0")
& ot____nom36("d1")
& ot____nom36("d0")
& ot____nom35_aux("d1")
& ~ ot____nom35_aux("d0")
& ot____nom35("d1")
& ~ ot____nom35("d0")
& ~ ot____nom34_aux("d1")
& ot____nom34_aux("d0")
& ot____nom34("d1")
& ot____nom34("d0")
& ~ ot____nom33_aux("d1")
& ot____nom33_aux("d0")
& ot____nom33("d1")
& ot____nom33("d0")
& ~ ot____nom32_aux("d1")
& ot____nom32_aux("d0")
& ot____nom32("d1")
& ot____nom32("d0")
& ~ ot____nom31_aux("d1")
& ot____nom31_aux("d0")
& ot____nom31("d1")
& ot____nom31("d0")
& ~ ot____nom30_aux("d1")
& ot____nom30_aux("d0")
& ot____nom30("d1")
& ot____nom30("d0")
& ot____nom3("d1")
& ot____nom3("d0")
& ~ ot____nom2_aux("d1")
& ot____nom2_aux("d0")
& ~ ot____nom29_aux("d1")
& ot____nom29_aux("d0")
& ot____nom29("d1")
& ot____nom29("d0")
& ~ ot____nom28_aux("d1")
& ot____nom28_aux("d0")
& ot____nom28("d1")
& ot____nom28("d0")
& ot____nom27_aux("d1")
& ~ ot____nom27_aux("d0")
& ot____nom27("d1")
& ~ ot____nom27("d0")
& ~ ot____nom26_aux("d1")
& ot____nom26_aux("d0")
& ot____nom26("d1")
& ot____nom26("d0")
& ~ ot____nom25_aux("d1")
& ot____nom25_aux("d0")
& ot____nom25("d1")
& ot____nom25("d0")
& ~ ot____nom24_aux("d1")
& ot____nom24_aux("d0")
& ot____nom24("d1")
& ot____nom24("d0")
& ~ ot____nom23_aux("d1")
& ot____nom23_aux("d0")
& ot____nom23("d1")
& ot____nom23("d0")
& ~ ot____nom22_aux("d1")
& ot____nom22_aux("d0")
& ot____nom22("d1")
& ot____nom22("d0")
& ~ ot____nom21_aux("d1")
& ot____nom21_aux("d0")
& ot____nom21("d1")
& ot____nom21("d0")
& ~ ot____nom20_aux("d1")
& ot____nom20_aux("d0")
& ot____nom20("d1")
& ot____nom20("d0")
& ot____nom2("d1")
& ot____nom2("d0")
& ot____nom1_aux("d1")
& ~ ot____nom1_aux("d0")
& ~ ot____nom19_aux("d1")
& ot____nom19_aux("d0")
& ot____nom19("d1")
& ot____nom19("d0")
& ot____nom18_aux("d1")
& ~ ot____nom18_aux("d0")
& ot____nom18("d1")
& ~ ot____nom18("d0")
& ot____nom17_aux("d1")
& ~ ot____nom17_aux("d0")
& ot____nom17("d1")
& ot____nom17("d0")
& ~ ot____nom16_aux("d1")
& ot____nom16_aux("d0")
& ot____nom16("d1")
& ot____nom16("d0")
& ot____nom15_aux("d1")
& ~ ot____nom15_aux("d0")
& ot____nom15("d1")
& ot____nom15("d0")
& ~ ot____nom14_aux("d1")
& ot____nom14_aux("d0")
& ot____nom14("d1")
& ot____nom14("d0")
& ~ ot____nom13_aux("d1")
& ot____nom13_aux("d0")
& ~ ot____nom13("d1")
& ot____nom13("d0")
& ot____nom12_aux("d1")
& ~ ot____nom12_aux("d0")
& ot____nom12("d1")
& ~ ot____nom12("d0")
& ot____nom11_aux("d1")
& ~ ot____nom11_aux("d0")
& ot____nom11("d1")
& ~ ot____nom11("d0")
& ot____nom10_aux("d1")
& ~ ot____nom10_aux("d0")
& ot____nom10("d1")
& ot____nom10("d0")
& ot____nom1("d1")
& ~ ot____nom1("d0")
& muscadet_aux("d1")
& ~ muscadet_aux("d0")
& muscadet("d1")
& ~ muscadet("d0")
& meursault_aux("d1")
& ~ meursault_aux("d0")
& meursault("d1")
& ~ meursault("d0")
& merlot_aux("d1")
& ~ merlot_aux("d0")
& merlot("d1")
& ~ merlot("d0")
& meritage_aux("d1")
& ~ meritage_aux("d0")
& meritage("d1")
& ~ meritage("d0")
& medoc("d1")
& ~ medoc("d0")
& margaux_aux("d1")
& ~ margaux_aux("d0")
& margaux("d1")
& ~ margaux("d0")
& loire("d1")
& ~ loire("d0")
& lateharvest("d1")
& ~ lateharvest("d0")
& kaon2namedobjects("d1")
& kaon2namedobjects("d0")
& kaon2hu("d1")
& kaon2hu("d0")
& italianwine("d1")
& ~ italianwine("d0")
& icewine_aux("d1")
& ~ icewine_aux("d0")
& icewine("d1")
& ~ icewine("d0")
& grape("d1")
& grape("d0")
& germanwine("d1")
& ~ germanwine("d0")
& gamay("d1")
& ~ gamay("d0")
& fullbodiedwine("d1")
& ~ fullbodiedwine("d0")
& ~ frenchwine("d1")
& ~ frenchwine("d0")
& ~ earlyharvest("d1")
& ~ earlyharvest("d0")
& drywine("d1")
& ~ drywine("d0")
& drywhitewine("d1")
& ~ drywhitewine("d0")
& dryriesling_aux("d1")
& ~ dryriesling_aux("d0")
& dryriesling("d1")
& ~ dryriesling("d0")
& dryredwine("d1")
& ~ dryredwine("d0")
& dessertwine_aux("d1")
& ~ dessertwine_aux("d0")
& dessertwine("d1")
& ~ dessertwine("d0")
& cotesdor_aux("d1")
& ~ cotesdor_aux("d0")
& cotesdor("d1")
& ~ cotesdor("d0")
& chianti_aux("d1")
& ~ chianti_aux("d0")
& chianti("d1")
& ~ chianti("d0")
& cheninblanc_aux("d1")
& ~ cheninblanc_aux("d0")
& cheninblanc("d1")
& ~ cheninblanc("d0")
& chardonnay_aux("d1")
& ~ chardonnay_aux("d0")
& chardonnay("d1")
& ~ chardonnay("d0")
& californiawine("d1")
& ~ californiawine("d0")
& cabernetsauvignon_aux("d1")
& ~ cabernetsauvignon_aux("d0")
& cabernetsauvignon("d1")
& ~ cabernetsauvignon("d0")
& cabernetfranc_aux("d1")
& ~ cabernetfranc_aux("d0")
& cabernetfranc("d1")
& ~ cabernetfranc("d0")
& burgundy("d1")
& ~ burgundy("d0")
& bordeaux("d1")
& ~ bordeaux("d0")
& beaujolais_aux("d1")
& ~ beaujolais_aux("d0")
& beaujolais("d1")
& ~ beaujolais("d0")
& anjou_aux("d1")
& ~ anjou_aux("d0")
& anjou("d1")
& ~ anjou("d0")
& americanwine("d1")
& ~ americanwine("d0")
& ~ alsatianwine("d1")
& ~ alsatianwine("d0") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRD002+1 : TPTP v9.3.1. Released v6.2.0.
% 0.00/0.03 % Command : mace4 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.38 % Computer : n016.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.07/20.33 % CPULimit : 300
% 0.07/20.33 % WCLimit : 300
% 0.07/20.33 % DateTime : Sat Sep 26 04:52:58 UTC 2026
% 0.07/20.33 % CPUTime :
% 0.07/20.33 % Mace4 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/20.33 % Process 1954758 was started by sandbox on n013,
% 0.07/20.33 % Sat Sep 26 04:52:58 2026
% 0.07/20.33 % The command was "/export/starexec/sandbox/solver/bin/mace4 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.22/20.58
% 0.22/20.58 % SZS status CounterSatisfiable for theBenchmark
% 0.22/20.58 % SZS output start FiniteModel for theBenchmark
% See solution above
%------------------------------------------------------------------------------