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