%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PRD001+1 : TPTP v9.3.1. Released v6.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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 : Thu Sep 24 01:59:11 PM UTC 2026
% Result : Theorem 15.59s 2.48s
% Output : CNFRefutation 15.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 313
% Syntax : Number of formulae : 1173 ( 298 unt; 104 def)
% Number of atoms : 2593 ( 0 equ)
% Maximal formula atoms : 85 ( 2 avg)
% Number of connectives : 2597 (1177 ~; 973 |; 197 &)
% ( 104 <=>; 146 =>; 0 <=; 0 <~>)
% Maximal formula depth : 183 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 265 ( 264 usr; 105 prp; 0-2 aty)
% Number of functors : 49 ( 49 usr; 49 con; 0-0 aty)
% Number of variables : 1198 (1004 !; 194 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f42,axiom,
hascolor_aux(selaksicewine,white),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f137,axiom,
hasmaker_aux(sevreetmainemuscadet,sevreetmaine),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f138,axiom,
hassugar_aux(pulignymontrachetwhiteburgundy,dry),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f161,axiom,
hassugar_aux(whitehalllaneprimavera,sweet),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f173,axiom,
hassugar_aux(formancabernetsauvignon,dry),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f177,axiom,
hassugar_aux(selakssauvignonblanc,dry),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f178,axiom,
locatedin_aux(californiaregion,usregion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f181,axiom,
locatedin_aux(stgenevievetexaswhite,centraltexasregion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f197,axiom,
locatedin_aux(centraltexasregion,texasregion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f203,axiom,
locatedin_aux(centralcoastregion,californiaregion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f220,axiom,
locatedin_aux(texasregion,usregion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f232,axiom,
locatedin_aux(ventanacheninblanc,centralcoastregion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f235,axiom,
locatedin_aux(schlossvolradtrochenbierenausleseriesling,germanyregion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f243,axiom,
madefromgrape_aux(chateaudychemsauterne,semillongrape),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f244,axiom,
madefromgrape_aux(chateaudychemsauterne,sauvignonblancgrape),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f245,axiom,
ot____nom1_aux(sweet),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f246,axiom,
ot____nom10_aux(texasregion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f248,axiom,
ot____nom12_aux(dry),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f251,axiom,
ot____nom15_aux(californiaregion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f253,axiom,
ot____nom17_aux(germanyregion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f280,axiom,
ot____nom38_aux(usregion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f331,axiom,
wineflavor_aux(delicate),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f350,axiom,
winesugar_aux(sweet),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f395,axiom,
winery_aux(foxen),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f396,axiom,
zinfandel_aux(elysezinfandel),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f401,axiom,
winebody_aux(light),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f403,axiom,
winebody_aux(medium),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f407,axiom,
whiteburgundy_aux(pulignymontrachetwhiteburgundy),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f408,axiom,
whiteburgundy_aux(cortonmontrachetwhiteburgundy),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f409,axiom,
whitewine_aux(stgenevievetexaswhite),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f410,axiom,
muscadet_aux(sevreetmainemuscadet),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f411,axiom,
meursault_aux(chateaudemeursaultmeursault),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f412,axiom,
meritage_aux(kathrynkennedylateral),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f413,axiom,
margaux_aux(chateaumargaux),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f414,axiom,
icewine_aux(selaksicewine),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f415,axiom,
dryriesling_aux(mountadamriesling),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f416,axiom,
dessertwine_aux(whitehalllaneprimavera),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f420,axiom,
cabernetsauvignon_aux(formancabernetsauvignon),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f421,axiom,
cabernetfranc_aux(whitehalllanecabernetfranc),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f422,axiom,
beaujolais_aux(chateaumorgonbeaujolais),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f423,axiom,
anjou_aux(rosedanjou),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f429,axiom,
cheninblanc_aux(foxencheninblanc),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f430,axiom,
cheninblanc_aux(ventanacheninblanc),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f431,axiom,
chianti_aux(chianticlassico),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f432,axiom,
cotesdor_aux(closdevougeotcotesdor),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f435,axiom,
pauillac_aux(chateaulafiterothschildpauillac),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f436,axiom,
petitesyrah_aux(mariettapetitesyrah),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f441,axiom,
port_aux(taylorport),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f442,axiom,
redtablewine_aux(mariettaoldvinesred),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f480,axiom,
sancerre_aux(closdelapoussiesancerre),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f481,axiom,
sauternes_aux(chateaudychemsauterne),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f482,axiom,
sauvignonblanc_aux(corbansprivatebinsauvignonblanc),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f485,axiom,
sauvignonblanc_aux(selakssauvignonblanc),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f486,axiom,
semillon_aux(congressspringssemillon),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f488,axiom,
stemilion_aux(chateauchevalblancstemilion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f489,axiom,
sweetriesling_aux(schlossrothermeltrochenbierenausleseriesling),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f490,axiom,
sweetriesling_aux(schlossvolradtrochenbierenausleseriesling),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f514,axiom,
kaon2namedobjects(whitehalllaneprimavera),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f611,axiom,
kaon2namedobjects(chateaumargaux),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f624,axiom,
kaon2namedobjects(closdevougeotcotesdor),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f652,axiom,
vintageyear_aux(year1998),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f653,axiom,
hasvintageyear_aux(saucelitocanyonzinfandel1998,year1998),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f654,axiom,
! [X,Y] :
( madefromgrape_aux(X,Y)
=> madefromgrape(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f655,axiom,
! [X,Y] :
( locatedin_aux(X,Y)
=> locatedin(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f656,axiom,
! [X,Y] :
( hassugar_aux(X,Y)
=> hassugar(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f657,axiom,
! [X,Y] :
( hasmaker_aux(X,Y)
=> hasmaker(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f659,axiom,
! [X,Y] :
( hascolor_aux(X,Y)
=> hascolor(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f662,axiom,
! [Y,X] :
( hasvintageyear_aux(Y,X)
=> hasvintageyear(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f663,axiom,
! [X] :
( ot____nom1_aux(X)
=> ot____nom1(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f664,axiom,
! [X] :
( ot____nom10_aux(X)
=> ot____nom10(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f666,axiom,
! [X] :
( ot____nom12_aux(X)
=> ot____nom12(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f669,axiom,
! [X] :
( ot____nom15_aux(X)
=> ot____nom15(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f671,axiom,
! [X] :
( ot____nom17_aux(X)
=> ot____nom17(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f694,axiom,
! [X] :
( ot____nom38_aux(X)
=> ot____nom38(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f727,axiom,
! [X] :
( zinfandel_aux(X)
=> zinfandel(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f728,axiom,
! [X] :
( winery_aux(X)
=> winery(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f730,axiom,
! [X] :
( winesugar_aux(X)
=> winesugar(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f731,axiom,
! [X] :
( wineflavor_aux(X)
=> wineflavor(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f732,axiom,
! [X] :
( anjou_aux(X)
=> anjou(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f733,axiom,
! [X] :
( beaujolais_aux(X)
=> beaujolais(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f734,axiom,
! [X] :
( cabernetfranc_aux(X)
=> cabernetfranc(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f735,axiom,
! [X] :
( cabernetsauvignon_aux(X)
=> cabernetsauvignon(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f737,axiom,
! [X] :
( cheninblanc_aux(X)
=> cheninblanc(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f738,axiom,
! [X] :
( chianti_aux(X)
=> chianti(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f739,axiom,
! [X] :
( cotesdor_aux(X)
=> cotesdor(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f740,axiom,
! [X] :
( dessertwine_aux(X)
=> dessertwine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f741,axiom,
! [X] :
( dryriesling_aux(X)
=> dryriesling(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f742,axiom,
! [X] :
( icewine_aux(X)
=> icewine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f743,axiom,
! [X] :
( margaux_aux(X)
=> margaux(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f744,axiom,
! [X] :
( meritage_aux(X)
=> meritage(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f746,axiom,
! [X] :
( meursault_aux(X)
=> meursault(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f747,axiom,
! [X] :
( muscadet_aux(X)
=> muscadet(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f748,axiom,
! [X] :
( pauillac_aux(X)
=> pauillac(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f749,axiom,
! [X] :
( petitesyrah_aux(X)
=> petitesyrah(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f751,axiom,
! [X] :
( port_aux(X)
=> port(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f752,axiom,
! [X] :
( redtablewine_aux(X)
=> redtablewine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f755,axiom,
! [X] :
( sancerre_aux(X)
=> sancerre(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f756,axiom,
! [X] :
( sauternes_aux(X)
=> sauternes(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f757,axiom,
! [X] :
( sauvignonblanc_aux(X)
=> sauvignonblanc(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f758,axiom,
! [X] :
( semillon_aux(X)
=> semillon(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f759,axiom,
! [X] :
( stemilion_aux(X)
=> stemilion(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f760,axiom,
! [X] :
( sweetriesling_aux(X)
=> sweetriesling(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f761,axiom,
! [X] :
( vintageyear_aux(X)
=> vintageyear(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f762,axiom,
! [X] :
( whiteburgundy_aux(X)
=> whiteburgundy(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f763,axiom,
! [X] :
( whitewine_aux(X)
=> whitewine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f764,axiom,
! [X] :
( winebody_aux(X)
=> winebody(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f772,axiom,
! [X] :
( medoc(X)
=> q0(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f773,axiom,
! [X] :
( cabernetsauvignon(X)
=> q0(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f792,axiom,
! [X] :
( cheninblanc(X)
=> q12(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f793,axiom,
! [X] :
( chardonnay(X)
=> q12(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f794,axiom,
! [X] :
( pinotblanc(X)
=> q12(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f797,axiom,
! [X] :
( sauternes(X)
=> q12(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f798,axiom,
! [X] :
( semillonorsauvignonblanc(X)
=> q12(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f799,axiom,
! [X] :
( riesling(X)
=> q12(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f801,axiom,
! [X] :
( margaux(X)
=> q13(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f805,axiom,
! [X] :
( beaujolais(X)
=> q14(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f807,axiom,
! [X] :
( anjou(X)
=> q15(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f830,axiom,
! [X] :
( margaux(X)
=> q20(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f832,axiom,
! [X] :
( q12(X)
=> q21(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f842,axiom,
! [X] :
( muscadet(X)
=> q24(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f845,axiom,
! [X,Y] :
( ( q27(Y)
& locatedin(X,Y) )
=> q26(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f847,axiom,
! [X] :
( q26(X)
=> q27(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f848,axiom,
! [X,Y] :
( ( ot____nom38(Y)
& locatedin(X,Y) )
=> q27(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f881,axiom,
! [X] :
( cabernetsauvignon(X)
=> q31(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f906,axiom,
! [X] :
( meursault(X)
=> q35(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f911,axiom,
! [X] :
( cheninblanc(X)
=> q36(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f925,axiom,
! [X] :
( cotesdor(X)
=> q4(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f930,axiom,
! [X] :
( q0(X)
=> q41(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f947,axiom,
! [X,Y] :
( ( ot____nom12(Y)
& hassugar(X,Y) )
=> q46(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f950,axiom,
! [X,Y] :
( ( q48(Y)
& locatedin(X,Y) )
=> q47(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f952,axiom,
! [X] :
( q47(X)
=> q48(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f953,axiom,
! [X,Y] :
( ( ot____nom15(Y)
& locatedin(X,Y) )
=> q48(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f982,axiom,
! [X,Y] :
( ( ot____nom17(Y)
& locatedin(X,Y) )
=> q50(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1018,axiom,
! [X] :
( whiteburgundy(X)
=> q63(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1035,axiom,
! [X] :
( pauillac(X)
=> q69(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1049,axiom,
! [X,Y] :
( ( ot____nom1(Y)
& hassugar(X,Y) )
=> q71(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1052,axiom,
! [X] :
( redburgundy(X)
=> q72(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1055,axiom,
! [X,Y] :
( ( q74(Y)
& locatedin(X,Y) )
=> q73(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1057,axiom,
! [X] :
( q73(X)
=> q74(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1058,axiom,
! [X,Y] :
( ( ot____nom10(Y)
& locatedin(X,Y) )
=> q74(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1065,axiom,
! [X] :
( ( wine(X)
& q27(X) )
=> americanwine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1071,axiom,
! [X] :
( sauternes(X)
=> bordeaux(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1072,axiom,
! [X] :
( medoc(X)
=> bordeaux(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1075,axiom,
! [X] :
( whitebordeaux(X)
=> bordeaux(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1079,axiom,
! [X] :
( redburgundy(X)
=> burgundy(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1084,axiom,
! [X] :
( q69(X)
=> cabernetsauvignon(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1087,axiom,
! [X] :
( ( wine(X)
& q48(X) )
=> californiawine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1089,axiom,
! [X] :
( q63(X)
=> chardonnay(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1099,axiom,
! [X] :
( icewine(X)
=> dessertwine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1101,axiom,
! [X] :
( ( redwine(X)
& drywine(X) )
=> dryredwine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1105,axiom,
! [X] :
( ( whitewine(X)
& drywine(X) )
=> drywhitewine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1109,axiom,
! [X] :
( ( wine(X)
& q46(X) )
=> drywine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1114,axiom,
! [X] :
( q35(X)
=> fullbodiedwine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1117,axiom,
! [X] :
( q14(X)
=> gamay(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1120,axiom,
! [X] :
( ( wine(X)
& q50(X) )
=> germanwine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1122,axiom,
! [X] :
( winegrape(X)
=> grape(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1126,axiom,
! [X] :
( chianti(X)
=> italianwine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1129,axiom,
! [X] :
( icewine(X)
=> lateharvest(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1134,axiom,
! [X] :
( whiteloire(X)
=> loire(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1136,axiom,
! [X] :
( muscadet(X)
=> loire(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1142,axiom,
! [X] :
( margaux(X)
=> medoc(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1147,axiom,
! [X] :
( q13(X)
=> merlot(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1158,axiom,
! [X] :
( q24(X)
=> pinotblanc(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1161,axiom,
! [X] :
( q72(X)
=> pinotnoir(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1165,axiom,
! [X] :
( wine(X)
=> potableliquid(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1167,axiom,
! [X] :
( ( bordeaux(X)
& redwine(X) )
=> redbordeaux(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1169,axiom,
! [X] :
( cotesdor(X)
=> redburgundy(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1177,axiom,
! [X] :
( port(X)
=> redwine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1178,axiom,
! [X] :
( ( wine(X)
& q41(X) )
=> redwine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1181,axiom,
! [X,Y] :
( locatedin(X,Y)
=> region(Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1186,axiom,
! [X] :
( sweetriesling(X)
=> riesling(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1189,axiom,
! [X] :
( q15(X)
=> rosewine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1200,axiom,
! [X] :
( semillon(X)
=> semillonorsauvignonblanc(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1201,axiom,
! [X] :
( sauvignonblanc(X)
=> semillonorsauvignonblanc(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1209,axiom,
! [X] :
( ( wine(X)
& q71(X) )
=> sweetwine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1211,axiom,
! [X] :
( whitetablewine(X)
=> tablewine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1213,axiom,
! [X] :
( ( wine(X)
& q46(X) )
=> tablewine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1215,axiom,
! [X] :
( ( wine(X)
& q74(X) )
=> texaswine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1219,axiom,
! [X,Y] :
( hasvintageyear(X,Y)
=> vintage(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1223,axiom,
! [X] :
( ( whitewine(X)
& bordeaux(X) )
=> whitebordeaux(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1225,axiom,
! [X] :
( meursault(X)
=> whiteburgundy(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1228,axiom,
! [X] :
( ( whitewine(X)
& loire(X) )
=> whiteloire(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1231,axiom,
! [X] :
( ( whitewine(X)
& q36(X) )
=> whitenonsweetwine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1234,axiom,
! [X] :
( ( tablewine(X)
& q21(X) )
=> whitetablewine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1237,axiom,
! [X] :
( whiteburgundy(X)
=> whitewine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1241,axiom,
! [X] :
( ( wine(X)
& q21(X) )
=> whitewine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1246,axiom,
! [X] :
( q20(X)
=> wine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1249,axiom,
! [X] :
( q31(X)
=> wine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1256,axiom,
! [X] :
( q0(X)
=> wine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1259,axiom,
! [X] :
( semillonorsauvignonblanc(X)
=> wine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1264,axiom,
! [X] :
( q12(X)
=> wine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1280,axiom,
! [X] :
( whitewine(X)
=> wine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1281,axiom,
! [X] :
( dessertwine(X)
=> wine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1306,axiom,
! [X] :
( winedescriptor(X)
=> winecolor(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1309,axiom,
! [X] :
( winetaste(X)
=> winedescriptor(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1310,axiom,
! [X,Y] :
( haswinedescriptor(X,Y)
=> winedescriptor(Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1315,axiom,
! [X,Y] :
( madefromgrape(X,Y)
=> winegrape(Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1322,axiom,
! [X] :
( winebody(X)
=> winetaste(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1323,axiom,
! [X] :
( winedescriptor(X)
=> winetaste(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1475,axiom,
! [X] :
( ( kaon2namedobjects(X)
& wine(X) )
=> hasbody(X,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1482,axiom,
! [X] :
( ( kaon2namedobjects(X)
& wine(X) )
=> hascolor(X,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1486,axiom,
! [X] :
( ( kaon2namedobjects(X)
& q4(X) )
=> hasflavor(X,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1492,axiom,
! [X,Y] :
( produceswine(X,Y)
=> hasmaker(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1496,axiom,
! [X] :
( ( kaon2namedobjects(X)
& wine(X) )
=> hassugar(X,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1507,axiom,
! [X,Y] :
( hascolor(X,Y)
=> haswinedescriptor(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1541,axiom,
! [X,Y] :
( madefromgrape(X,Y)
=> madefromfruit(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1564,axiom,
! [X,Y] :
( madefromgrape(X,Y)
=> madeintowine(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1567,axiom,
! [X,Y] :
( hasmaker(X,Y)
=> produceswine(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1615,conjecture,
( ? [Y,X] : produceswine(X,Y)
& ? [Y,X] : madeintowine(X,Y)
& ? [Y,X] : madefromfruit(X,Y)
& ? [Y,X] : madefromgrape(X,Y)
& ? [Y,X] : locatedin(X,Y)
& ? [Y,X] : haswinedescriptor(X,Y)
& ? [Y,X] : hasvintageyear(X,Y)
& ? [Y,X] : hassugar(X,Y)
& ? [Y,X] : hasmaker(X,Y)
& ? [Y,X] : hasflavor(X,Y)
& ? [Y,X] : hascolor(X,Y)
& ? [Y,X] : hasbody(X,Y)
& ? [X] : zinfandel(X)
& ? [X] : winetaste(X)
& ? [X] : winery(X)
& ? [X] : winesugar(X)
& ? [X] : winegrape(X)
& ? [X] : wineflavor(X)
& ? [X] : winedescriptor(X)
& ? [X] : winecolor(X)
& ? [X] : winebody(X)
& ? [X] : wine(X)
& ? [X] : whitewine(X)
& ? [X] : whitetablewine(X)
& ? [X] : whitenonsweetwine(X)
& ? [X] : whiteloire(X)
& ? [X] : whiteburgundy(X)
& ? [X] : whitebordeaux(X)
& ? [X] : vintageyear(X)
& ? [X] : vintage(X)
& ? [X] : texaswine(X)
& ? [X] : tablewine(X)
& ? [X] : sweetwine(X)
& ? [X] : sweetriesling(X)
& ? [X] : stemilion(X)
& ? [X] : semillonorsauvignonblanc(X)
& ? [X] : semillon(X)
& ? [X] : sauvignonblanc(X)
& ? [X] : sauternes(X)
& ? [X] : sancerre(X)
& ? [X] : rosewine(X)
& ? [X] : riesling(X)
& ? [X] : region(X)
& ? [X] : redwine(X)
& ? [X] : redtablewine(X)
& ? [X] : redburgundy(X)
& ? [X] : redbordeaux(X)
& ? [X] : potableliquid(X)
& ? [X] : port(X)
& ? [X] : pinotnoir(X)
& ? [X] : pinotblanc(X)
& ? [X] : petitesyrah(X)
& ? [X] : pauillac(X)
& ? [X] : muscadet(X)
& ? [X] : meursault(X)
& ? [X] : merlot(X)
& ? [X] : meritage(X)
& ? [X] : medoc(X)
& ? [X] : margaux(X)
& ? [X] : loire(X)
& ? [X] : lateharvest(X)
& ? [X] : italianwine(X)
& ? [X] : icewine(X)
& ? [X] : grape(X)
& ? [X] : germanwine(X)
& ? [X] : gamay(X)
& ? [X] : fullbodiedwine(X)
& ? [X] : drywine(X)
& ? [X] : drywhitewine(X)
& ? [X] : dryredwine(X)
& ? [X] : dryriesling(X)
& ? [X] : dessertwine(X)
& ? [X] : cotesdor(X)
& ? [X] : chianti(X)
& ? [X] : cheninblanc(X)
& ? [X] : chardonnay(X)
& ? [X] : californiawine(X)
& ? [X] : cabernetsauvignon(X)
& ? [X] : cabernetfranc(X)
& ? [X] : beaujolais(X)
& ? [X] : anjou(X)
& ? [X] : burgundy(X)
& ? [X] : bordeaux(X)
& ? [X] : americanwine(X)
& ? [X] : californiawine(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1616,negated_conjecture,
~ ( ? [Y,X] : produceswine(X,Y)
& ? [Y,X] : madeintowine(X,Y)
& ? [Y,X] : madefromfruit(X,Y)
& ? [Y,X] : madefromgrape(X,Y)
& ? [Y,X] : locatedin(X,Y)
& ? [Y,X] : haswinedescriptor(X,Y)
& ? [Y,X] : hasvintageyear(X,Y)
& ? [Y,X] : hassugar(X,Y)
& ? [Y,X] : hasmaker(X,Y)
& ? [Y,X] : hasflavor(X,Y)
& ? [Y,X] : hascolor(X,Y)
& ? [Y,X] : hasbody(X,Y)
& ? [X] : zinfandel(X)
& ? [X] : winetaste(X)
& ? [X] : winery(X)
& ? [X] : winesugar(X)
& ? [X] : winegrape(X)
& ? [X] : wineflavor(X)
& ? [X] : winedescriptor(X)
& ? [X] : winecolor(X)
& ? [X] : winebody(X)
& ? [X] : wine(X)
& ? [X] : whitewine(X)
& ? [X] : whitetablewine(X)
& ? [X] : whitenonsweetwine(X)
& ? [X] : whiteloire(X)
& ? [X] : whiteburgundy(X)
& ? [X] : whitebordeaux(X)
& ? [X] : vintageyear(X)
& ? [X] : vintage(X)
& ? [X] : texaswine(X)
& ? [X] : tablewine(X)
& ? [X] : sweetwine(X)
& ? [X] : sweetriesling(X)
& ? [X] : stemilion(X)
& ? [X] : semillonorsauvignonblanc(X)
& ? [X] : semillon(X)
& ? [X] : sauvignonblanc(X)
& ? [X] : sauternes(X)
& ? [X] : sancerre(X)
& ? [X] : rosewine(X)
& ? [X] : riesling(X)
& ? [X] : region(X)
& ? [X] : redwine(X)
& ? [X] : redtablewine(X)
& ? [X] : redburgundy(X)
& ? [X] : redbordeaux(X)
& ? [X] : potableliquid(X)
& ? [X] : port(X)
& ? [X] : pinotnoir(X)
& ? [X] : pinotblanc(X)
& ? [X] : petitesyrah(X)
& ? [X] : pauillac(X)
& ? [X] : muscadet(X)
& ? [X] : meursault(X)
& ? [X] : merlot(X)
& ? [X] : meritage(X)
& ? [X] : medoc(X)
& ? [X] : margaux(X)
& ? [X] : loire(X)
& ? [X] : lateharvest(X)
& ? [X] : italianwine(X)
& ? [X] : icewine(X)
& ? [X] : grape(X)
& ? [X] : germanwine(X)
& ? [X] : gamay(X)
& ? [X] : fullbodiedwine(X)
& ? [X] : drywine(X)
& ? [X] : drywhitewine(X)
& ? [X] : dryredwine(X)
& ? [X] : dryriesling(X)
& ? [X] : dessertwine(X)
& ? [X] : cotesdor(X)
& ? [X] : chianti(X)
& ? [X] : cheninblanc(X)
& ? [X] : chardonnay(X)
& ? [X] : californiawine(X)
& ? [X] : cabernetsauvignon(X)
& ? [X] : cabernetfranc(X)
& ? [X] : beaujolais(X)
& ? [X] : anjou(X)
& ? [X] : burgundy(X)
& ? [X] : bordeaux(X)
& ? [X] : americanwine(X)
& ? [X] : californiawine(X) ),
inference(negated_conjecture,[status(cth)],[f1615]) ).
fof(f1658,plain,
hascolor_aux(selaksicewine,white),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f1753,plain,
hasmaker_aux(sevreetmainemuscadet,sevreetmaine),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f1754,plain,
hassugar_aux(pulignymontrachetwhiteburgundy,dry),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f1777,plain,
hassugar_aux(whitehalllaneprimavera,sweet),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f1789,plain,
hassugar_aux(formancabernetsauvignon,dry),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f1793,plain,
hassugar_aux(selakssauvignonblanc,dry),
inference(cnf_transformation,[status(thm)],[f177]) ).
fof(f1794,plain,
locatedin_aux(californiaregion,usregion),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f1797,plain,
locatedin_aux(stgenevievetexaswhite,centraltexasregion),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f1813,plain,
locatedin_aux(centraltexasregion,texasregion),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f1819,plain,
locatedin_aux(centralcoastregion,californiaregion),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f1836,plain,
locatedin_aux(texasregion,usregion),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f1848,plain,
locatedin_aux(ventanacheninblanc,centralcoastregion),
inference(cnf_transformation,[status(thm)],[f232]) ).
fof(f1851,plain,
locatedin_aux(schlossvolradtrochenbierenausleseriesling,germanyregion),
inference(cnf_transformation,[status(thm)],[f235]) ).
fof(f1859,plain,
madefromgrape_aux(chateaudychemsauterne,semillongrape),
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f1860,plain,
madefromgrape_aux(chateaudychemsauterne,sauvignonblancgrape),
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f1861,plain,
ot____nom1_aux(sweet),
inference(cnf_transformation,[status(thm)],[f245]) ).
fof(f1862,plain,
ot____nom10_aux(texasregion),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f1864,plain,
ot____nom12_aux(dry),
inference(cnf_transformation,[status(thm)],[f248]) ).
fof(f1867,plain,
ot____nom15_aux(californiaregion),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f1869,plain,
ot____nom17_aux(germanyregion),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f1896,plain,
ot____nom38_aux(usregion),
inference(cnf_transformation,[status(thm)],[f280]) ).
fof(f1947,plain,
wineflavor_aux(delicate),
inference(cnf_transformation,[status(thm)],[f331]) ).
fof(f1966,plain,
winesugar_aux(sweet),
inference(cnf_transformation,[status(thm)],[f350]) ).
fof(f2011,plain,
winery_aux(foxen),
inference(cnf_transformation,[status(thm)],[f395]) ).
fof(f2012,plain,
zinfandel_aux(elysezinfandel),
inference(cnf_transformation,[status(thm)],[f396]) ).
fof(f2017,plain,
winebody_aux(light),
inference(cnf_transformation,[status(thm)],[f401]) ).
fof(f2019,plain,
winebody_aux(medium),
inference(cnf_transformation,[status(thm)],[f403]) ).
fof(f2023,plain,
whiteburgundy_aux(pulignymontrachetwhiteburgundy),
inference(cnf_transformation,[status(thm)],[f407]) ).
fof(f2024,plain,
whiteburgundy_aux(cortonmontrachetwhiteburgundy),
inference(cnf_transformation,[status(thm)],[f408]) ).
fof(f2025,plain,
whitewine_aux(stgenevievetexaswhite),
inference(cnf_transformation,[status(thm)],[f409]) ).
fof(f2026,plain,
muscadet_aux(sevreetmainemuscadet),
inference(cnf_transformation,[status(thm)],[f410]) ).
fof(f2027,plain,
meursault_aux(chateaudemeursaultmeursault),
inference(cnf_transformation,[status(thm)],[f411]) ).
fof(f2028,plain,
meritage_aux(kathrynkennedylateral),
inference(cnf_transformation,[status(thm)],[f412]) ).
fof(f2029,plain,
margaux_aux(chateaumargaux),
inference(cnf_transformation,[status(thm)],[f413]) ).
fof(f2030,plain,
icewine_aux(selaksicewine),
inference(cnf_transformation,[status(thm)],[f414]) ).
fof(f2031,plain,
dryriesling_aux(mountadamriesling),
inference(cnf_transformation,[status(thm)],[f415]) ).
fof(f2032,plain,
dessertwine_aux(whitehalllaneprimavera),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f2036,plain,
cabernetsauvignon_aux(formancabernetsauvignon),
inference(cnf_transformation,[status(thm)],[f420]) ).
fof(f2037,plain,
cabernetfranc_aux(whitehalllanecabernetfranc),
inference(cnf_transformation,[status(thm)],[f421]) ).
fof(f2038,plain,
beaujolais_aux(chateaumorgonbeaujolais),
inference(cnf_transformation,[status(thm)],[f422]) ).
fof(f2039,plain,
anjou_aux(rosedanjou),
inference(cnf_transformation,[status(thm)],[f423]) ).
fof(f2045,plain,
cheninblanc_aux(foxencheninblanc),
inference(cnf_transformation,[status(thm)],[f429]) ).
fof(f2046,plain,
cheninblanc_aux(ventanacheninblanc),
inference(cnf_transformation,[status(thm)],[f430]) ).
fof(f2047,plain,
chianti_aux(chianticlassico),
inference(cnf_transformation,[status(thm)],[f431]) ).
fof(f2048,plain,
cotesdor_aux(closdevougeotcotesdor),
inference(cnf_transformation,[status(thm)],[f432]) ).
fof(f2051,plain,
pauillac_aux(chateaulafiterothschildpauillac),
inference(cnf_transformation,[status(thm)],[f435]) ).
fof(f2052,plain,
petitesyrah_aux(mariettapetitesyrah),
inference(cnf_transformation,[status(thm)],[f436]) ).
fof(f2057,plain,
port_aux(taylorport),
inference(cnf_transformation,[status(thm)],[f441]) ).
fof(f2058,plain,
redtablewine_aux(mariettaoldvinesred),
inference(cnf_transformation,[status(thm)],[f442]) ).
fof(f2096,plain,
sancerre_aux(closdelapoussiesancerre),
inference(cnf_transformation,[status(thm)],[f480]) ).
fof(f2097,plain,
sauternes_aux(chateaudychemsauterne),
inference(cnf_transformation,[status(thm)],[f481]) ).
fof(f2098,plain,
sauvignonblanc_aux(corbansprivatebinsauvignonblanc),
inference(cnf_transformation,[status(thm)],[f482]) ).
fof(f2101,plain,
sauvignonblanc_aux(selakssauvignonblanc),
inference(cnf_transformation,[status(thm)],[f485]) ).
fof(f2102,plain,
semillon_aux(congressspringssemillon),
inference(cnf_transformation,[status(thm)],[f486]) ).
fof(f2104,plain,
stemilion_aux(chateauchevalblancstemilion),
inference(cnf_transformation,[status(thm)],[f488]) ).
fof(f2105,plain,
sweetriesling_aux(schlossrothermeltrochenbierenausleseriesling),
inference(cnf_transformation,[status(thm)],[f489]) ).
fof(f2106,plain,
sweetriesling_aux(schlossvolradtrochenbierenausleseriesling),
inference(cnf_transformation,[status(thm)],[f490]) ).
fof(f2130,plain,
kaon2namedobjects(whitehalllaneprimavera),
inference(cnf_transformation,[status(thm)],[f514]) ).
fof(f2227,plain,
kaon2namedobjects(chateaumargaux),
inference(cnf_transformation,[status(thm)],[f611]) ).
fof(f2240,plain,
kaon2namedobjects(closdevougeotcotesdor),
inference(cnf_transformation,[status(thm)],[f624]) ).
fof(f2268,plain,
vintageyear_aux(year1998),
inference(cnf_transformation,[status(thm)],[f652]) ).
fof(f2269,plain,
hasvintageyear_aux(saucelitocanyonzinfandel1998,year1998),
inference(cnf_transformation,[status(thm)],[f653]) ).
fof(f2270,plain,
! [X,Y] :
( madefromgrape(X,Y)
| ~ madefromgrape_aux(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f654]) ).
fof(f2271,plain,
! [X0,X1] :
( madefromgrape(X0,X1)
| ~ madefromgrape_aux(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2270]) ).
fof(f2272,plain,
! [X,Y] :
( locatedin(X,Y)
| ~ locatedin_aux(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f655]) ).
fof(f2273,plain,
! [X0,X1] :
( locatedin(X0,X1)
| ~ locatedin_aux(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2272]) ).
fof(f2274,plain,
! [X,Y] :
( hassugar(X,Y)
| ~ hassugar_aux(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f656]) ).
fof(f2275,plain,
! [X0,X1] :
( hassugar(X0,X1)
| ~ hassugar_aux(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2274]) ).
fof(f2276,plain,
! [X,Y] :
( hasmaker(X,Y)
| ~ hasmaker_aux(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f657]) ).
fof(f2277,plain,
! [X0,X1] :
( hasmaker(X0,X1)
| ~ hasmaker_aux(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2276]) ).
fof(f2280,plain,
! [X,Y] :
( hascolor(X,Y)
| ~ hascolor_aux(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f659]) ).
fof(f2281,plain,
! [X0,X1] :
( hascolor(X0,X1)
| ~ hascolor_aux(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2280]) ).
fof(f2286,plain,
! [Y,X] :
( hasvintageyear(Y,X)
| ~ hasvintageyear_aux(Y,X) ),
inference(pre_NNF_transformation,[status(thm)],[f662]) ).
fof(f2287,plain,
! [X0,X1] :
( hasvintageyear(X0,X1)
| ~ hasvintageyear_aux(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2286]) ).
fof(f2288,plain,
! [X] :
( ot____nom1(X)
| ~ ot____nom1_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f663]) ).
fof(f2289,plain,
! [X0] :
( ot____nom1(X0)
| ~ ot____nom1_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2288]) ).
fof(f2290,plain,
! [X] :
( ot____nom10(X)
| ~ ot____nom10_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f664]) ).
fof(f2291,plain,
! [X0] :
( ot____nom10(X0)
| ~ ot____nom10_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2290]) ).
fof(f2294,plain,
! [X] :
( ot____nom12(X)
| ~ ot____nom12_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f666]) ).
fof(f2295,plain,
! [X0] :
( ot____nom12(X0)
| ~ ot____nom12_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2294]) ).
fof(f2300,plain,
! [X] :
( ot____nom15(X)
| ~ ot____nom15_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f669]) ).
fof(f2301,plain,
! [X0] :
( ot____nom15(X0)
| ~ ot____nom15_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2300]) ).
fof(f2304,plain,
! [X] :
( ot____nom17(X)
| ~ ot____nom17_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f671]) ).
fof(f2305,plain,
! [X0] :
( ot____nom17(X0)
| ~ ot____nom17_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2304]) ).
fof(f2350,plain,
! [X] :
( ot____nom38(X)
| ~ ot____nom38_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f694]) ).
fof(f2351,plain,
! [X0] :
( ot____nom38(X0)
| ~ ot____nom38_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2350]) ).
fof(f2416,plain,
! [X] :
( zinfandel(X)
| ~ zinfandel_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f727]) ).
fof(f2417,plain,
! [X0] :
( zinfandel(X0)
| ~ zinfandel_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2416]) ).
fof(f2418,plain,
! [X] :
( winery(X)
| ~ winery_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f728]) ).
fof(f2419,plain,
! [X0] :
( winery(X0)
| ~ winery_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2418]) ).
fof(f2422,plain,
! [X] :
( winesugar(X)
| ~ winesugar_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f730]) ).
fof(f2423,plain,
! [X0] :
( winesugar(X0)
| ~ winesugar_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2422]) ).
fof(f2424,plain,
! [X] :
( wineflavor(X)
| ~ wineflavor_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f731]) ).
fof(f2425,plain,
! [X0] :
( wineflavor(X0)
| ~ wineflavor_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2424]) ).
fof(f2426,plain,
! [X] :
( anjou(X)
| ~ anjou_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f732]) ).
fof(f2427,plain,
! [X0] :
( anjou(X0)
| ~ anjou_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2426]) ).
fof(f2428,plain,
! [X] :
( beaujolais(X)
| ~ beaujolais_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f733]) ).
fof(f2429,plain,
! [X0] :
( beaujolais(X0)
| ~ beaujolais_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2428]) ).
fof(f2430,plain,
! [X] :
( cabernetfranc(X)
| ~ cabernetfranc_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f734]) ).
fof(f2431,plain,
! [X0] :
( cabernetfranc(X0)
| ~ cabernetfranc_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2430]) ).
fof(f2432,plain,
! [X] :
( cabernetsauvignon(X)
| ~ cabernetsauvignon_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f735]) ).
fof(f2433,plain,
! [X0] :
( cabernetsauvignon(X0)
| ~ cabernetsauvignon_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2432]) ).
fof(f2436,plain,
! [X] :
( cheninblanc(X)
| ~ cheninblanc_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f737]) ).
fof(f2437,plain,
! [X0] :
( cheninblanc(X0)
| ~ cheninblanc_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2436]) ).
fof(f2438,plain,
! [X] :
( chianti(X)
| ~ chianti_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f738]) ).
fof(f2439,plain,
! [X0] :
( chianti(X0)
| ~ chianti_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2438]) ).
fof(f2440,plain,
! [X] :
( cotesdor(X)
| ~ cotesdor_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f739]) ).
fof(f2441,plain,
! [X0] :
( cotesdor(X0)
| ~ cotesdor_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2440]) ).
fof(f2442,plain,
! [X] :
( dessertwine(X)
| ~ dessertwine_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f740]) ).
fof(f2443,plain,
! [X0] :
( dessertwine(X0)
| ~ dessertwine_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2442]) ).
fof(f2444,plain,
! [X] :
( dryriesling(X)
| ~ dryriesling_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f741]) ).
fof(f2445,plain,
! [X0] :
( dryriesling(X0)
| ~ dryriesling_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2444]) ).
fof(f2446,plain,
! [X] :
( icewine(X)
| ~ icewine_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f742]) ).
fof(f2447,plain,
! [X0] :
( icewine(X0)
| ~ icewine_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2446]) ).
fof(f2448,plain,
! [X] :
( margaux(X)
| ~ margaux_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f743]) ).
fof(f2449,plain,
! [X0] :
( margaux(X0)
| ~ margaux_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2448]) ).
fof(f2450,plain,
! [X] :
( meritage(X)
| ~ meritage_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f744]) ).
fof(f2451,plain,
! [X0] :
( meritage(X0)
| ~ meritage_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2450]) ).
fof(f2454,plain,
! [X] :
( meursault(X)
| ~ meursault_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f746]) ).
fof(f2455,plain,
! [X0] :
( meursault(X0)
| ~ meursault_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2454]) ).
fof(f2456,plain,
! [X] :
( muscadet(X)
| ~ muscadet_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f747]) ).
fof(f2457,plain,
! [X0] :
( muscadet(X0)
| ~ muscadet_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2456]) ).
fof(f2458,plain,
! [X] :
( pauillac(X)
| ~ pauillac_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f748]) ).
fof(f2459,plain,
! [X0] :
( pauillac(X0)
| ~ pauillac_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2458]) ).
fof(f2460,plain,
! [X] :
( petitesyrah(X)
| ~ petitesyrah_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f749]) ).
fof(f2461,plain,
! [X0] :
( petitesyrah(X0)
| ~ petitesyrah_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2460]) ).
fof(f2464,plain,
! [X] :
( port(X)
| ~ port_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f751]) ).
fof(f2465,plain,
! [X0] :
( port(X0)
| ~ port_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2464]) ).
fof(f2466,plain,
! [X] :
( redtablewine(X)
| ~ redtablewine_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f752]) ).
fof(f2467,plain,
! [X0] :
( redtablewine(X0)
| ~ redtablewine_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2466]) ).
fof(f2472,plain,
! [X] :
( sancerre(X)
| ~ sancerre_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f755]) ).
fof(f2473,plain,
! [X0] :
( sancerre(X0)
| ~ sancerre_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2472]) ).
fof(f2474,plain,
! [X] :
( sauternes(X)
| ~ sauternes_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f756]) ).
fof(f2475,plain,
! [X0] :
( sauternes(X0)
| ~ sauternes_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2474]) ).
fof(f2476,plain,
! [X] :
( sauvignonblanc(X)
| ~ sauvignonblanc_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f757]) ).
fof(f2477,plain,
! [X0] :
( sauvignonblanc(X0)
| ~ sauvignonblanc_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2476]) ).
fof(f2478,plain,
! [X] :
( semillon(X)
| ~ semillon_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f758]) ).
fof(f2479,plain,
! [X0] :
( semillon(X0)
| ~ semillon_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2478]) ).
fof(f2480,plain,
! [X] :
( stemilion(X)
| ~ stemilion_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f759]) ).
fof(f2481,plain,
! [X0] :
( stemilion(X0)
| ~ stemilion_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2480]) ).
fof(f2482,plain,
! [X] :
( sweetriesling(X)
| ~ sweetriesling_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f760]) ).
fof(f2483,plain,
! [X0] :
( sweetriesling(X0)
| ~ sweetriesling_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2482]) ).
fof(f2484,plain,
! [X] :
( vintageyear(X)
| ~ vintageyear_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f761]) ).
fof(f2485,plain,
! [X0] :
( vintageyear(X0)
| ~ vintageyear_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2484]) ).
fof(f2486,plain,
! [X] :
( whiteburgundy(X)
| ~ whiteburgundy_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f762]) ).
fof(f2487,plain,
! [X0] :
( whiteburgundy(X0)
| ~ whiteburgundy_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2486]) ).
fof(f2488,plain,
! [X] :
( whitewine(X)
| ~ whitewine_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f763]) ).
fof(f2489,plain,
! [X0] :
( whitewine(X0)
| ~ whitewine_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2488]) ).
fof(f2490,plain,
! [X] :
( winebody(X)
| ~ winebody_aux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f764]) ).
fof(f2491,plain,
! [X0] :
( winebody(X0)
| ~ winebody_aux(X0) ),
inference(cnf_transformation,[status(thm)],[f2490]) ).
fof(f2506,plain,
! [X] :
( q0(X)
| ~ medoc(X) ),
inference(pre_NNF_transformation,[status(thm)],[f772]) ).
fof(f2507,plain,
! [X0] :
( q0(X0)
| ~ medoc(X0) ),
inference(cnf_transformation,[status(thm)],[f2506]) ).
fof(f2508,plain,
! [X] :
( q0(X)
| ~ cabernetsauvignon(X) ),
inference(pre_NNF_transformation,[status(thm)],[f773]) ).
fof(f2509,plain,
! [X0] :
( q0(X0)
| ~ cabernetsauvignon(X0) ),
inference(cnf_transformation,[status(thm)],[f2508]) ).
fof(f2552,plain,
! [X] :
( q12(X)
| ~ cheninblanc(X) ),
inference(pre_NNF_transformation,[status(thm)],[f792]) ).
fof(f2553,plain,
! [X0] :
( q12(X0)
| ~ cheninblanc(X0) ),
inference(cnf_transformation,[status(thm)],[f2552]) ).
fof(f2554,plain,
! [X] :
( q12(X)
| ~ chardonnay(X) ),
inference(pre_NNF_transformation,[status(thm)],[f793]) ).
fof(f2555,plain,
! [X0] :
( q12(X0)
| ~ chardonnay(X0) ),
inference(cnf_transformation,[status(thm)],[f2554]) ).
fof(f2556,plain,
! [X] :
( q12(X)
| ~ pinotblanc(X) ),
inference(pre_NNF_transformation,[status(thm)],[f794]) ).
fof(f2557,plain,
! [X0] :
( q12(X0)
| ~ pinotblanc(X0) ),
inference(cnf_transformation,[status(thm)],[f2556]) ).
fof(f2562,plain,
! [X] :
( q12(X)
| ~ sauternes(X) ),
inference(pre_NNF_transformation,[status(thm)],[f797]) ).
fof(f2563,plain,
! [X0] :
( q12(X0)
| ~ sauternes(X0) ),
inference(cnf_transformation,[status(thm)],[f2562]) ).
fof(f2564,plain,
! [X] :
( q12(X)
| ~ semillonorsauvignonblanc(X) ),
inference(pre_NNF_transformation,[status(thm)],[f798]) ).
fof(f2565,plain,
! [X0] :
( q12(X0)
| ~ semillonorsauvignonblanc(X0) ),
inference(cnf_transformation,[status(thm)],[f2564]) ).
fof(f2566,plain,
! [X] :
( q12(X)
| ~ riesling(X) ),
inference(pre_NNF_transformation,[status(thm)],[f799]) ).
fof(f2567,plain,
! [X0] :
( q12(X0)
| ~ riesling(X0) ),
inference(cnf_transformation,[status(thm)],[f2566]) ).
fof(f2571,plain,
! [X] :
( q13(X)
| ~ margaux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f801]) ).
fof(f2572,plain,
! [X0] :
( q13(X0)
| ~ margaux(X0) ),
inference(cnf_transformation,[status(thm)],[f2571]) ).
fof(f2580,plain,
! [X] :
( q14(X)
| ~ beaujolais(X) ),
inference(pre_NNF_transformation,[status(thm)],[f805]) ).
fof(f2581,plain,
! [X0] :
( q14(X0)
| ~ beaujolais(X0) ),
inference(cnf_transformation,[status(thm)],[f2580]) ).
fof(f2585,plain,
! [X] :
( q15(X)
| ~ anjou(X) ),
inference(pre_NNF_transformation,[status(thm)],[f807]) ).
fof(f2586,plain,
! [X0] :
( q15(X0)
| ~ anjou(X0) ),
inference(cnf_transformation,[status(thm)],[f2585]) ).
fof(f2642,plain,
! [X] :
( q20(X)
| ~ margaux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f830]) ).
fof(f2643,plain,
! [X0] :
( q20(X0)
| ~ margaux(X0) ),
inference(cnf_transformation,[status(thm)],[f2642]) ).
fof(f2647,plain,
! [X] :
( q21(X)
| ~ q12(X) ),
inference(pre_NNF_transformation,[status(thm)],[f832]) ).
fof(f2648,plain,
! [X0] :
( q21(X0)
| ~ q12(X0) ),
inference(cnf_transformation,[status(thm)],[f2647]) ).
fof(f2673,plain,
! [X] :
( q24(X)
| ~ muscadet(X) ),
inference(pre_NNF_transformation,[status(thm)],[f842]) ).
fof(f2674,plain,
! [X0] :
( q24(X0)
| ~ muscadet(X0) ),
inference(cnf_transformation,[status(thm)],[f2673]) ).
fof(f2680,plain,
! [X,Y] :
( q26(X)
| ~ q27(Y)
| ~ locatedin(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f845]) ).
fof(f2681,plain,
! [X] :
( q26(X)
| ! [Y] :
( ~ q27(Y)
| ~ locatedin(X,Y) ) ),
inference(miniscoping,[status(thm)],[f2680]) ).
fof(f2682,plain,
! [X0,X1] :
( q26(X0)
| ~ q27(X1)
| ~ locatedin(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2681]) ).
fof(f2686,plain,
! [X] :
( q27(X)
| ~ q26(X) ),
inference(pre_NNF_transformation,[status(thm)],[f847]) ).
fof(f2687,plain,
! [X0] :
( q27(X0)
| ~ q26(X0) ),
inference(cnf_transformation,[status(thm)],[f2686]) ).
fof(f2688,plain,
! [X,Y] :
( q27(X)
| ~ ot____nom38(Y)
| ~ locatedin(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f848]) ).
fof(f2689,plain,
! [X] :
( q27(X)
| ! [Y] :
( ~ ot____nom38(Y)
| ~ locatedin(X,Y) ) ),
inference(miniscoping,[status(thm)],[f2688]) ).
fof(f2690,plain,
! [X0,X1] :
( q27(X0)
| ~ ot____nom38(X1)
| ~ locatedin(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2689]) ).
fof(f2761,plain,
! [X] :
( q31(X)
| ~ cabernetsauvignon(X) ),
inference(pre_NNF_transformation,[status(thm)],[f881]) ).
fof(f2762,plain,
! [X0] :
( q31(X0)
| ~ cabernetsauvignon(X0) ),
inference(cnf_transformation,[status(thm)],[f2761]) ).
fof(f2817,plain,
! [X] :
( q35(X)
| ~ meursault(X) ),
inference(pre_NNF_transformation,[status(thm)],[f906]) ).
fof(f2818,plain,
! [X0] :
( q35(X0)
| ~ meursault(X0) ),
inference(cnf_transformation,[status(thm)],[f2817]) ).
fof(f2828,plain,
! [X] :
( q36(X)
| ~ cheninblanc(X) ),
inference(pre_NNF_transformation,[status(thm)],[f911]) ).
fof(f2829,plain,
! [X0] :
( q36(X0)
| ~ cheninblanc(X0) ),
inference(cnf_transformation,[status(thm)],[f2828]) ).
fof(f2863,plain,
! [X] :
( q4(X)
| ~ cotesdor(X) ),
inference(pre_NNF_transformation,[status(thm)],[f925]) ).
fof(f2864,plain,
! [X0] :
( q4(X0)
| ~ cotesdor(X0) ),
inference(cnf_transformation,[status(thm)],[f2863]) ).
fof(f2876,plain,
! [X] :
( q41(X)
| ~ q0(X) ),
inference(pre_NNF_transformation,[status(thm)],[f930]) ).
fof(f2877,plain,
! [X0] :
( q41(X0)
| ~ q0(X0) ),
inference(cnf_transformation,[status(thm)],[f2876]) ).
fof(f2918,plain,
! [X,Y] :
( q46(X)
| ~ ot____nom12(Y)
| ~ hassugar(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f947]) ).
fof(f2919,plain,
! [X] :
( q46(X)
| ! [Y] :
( ~ ot____nom12(Y)
| ~ hassugar(X,Y) ) ),
inference(miniscoping,[status(thm)],[f2918]) ).
fof(f2920,plain,
! [X0,X1] :
( q46(X0)
| ~ ot____nom12(X1)
| ~ hassugar(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2919]) ).
fof(f2926,plain,
! [X,Y] :
( q47(X)
| ~ q48(Y)
| ~ locatedin(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f950]) ).
fof(f2927,plain,
! [X] :
( q47(X)
| ! [Y] :
( ~ q48(Y)
| ~ locatedin(X,Y) ) ),
inference(miniscoping,[status(thm)],[f2926]) ).
fof(f2928,plain,
! [X0,X1] :
( q47(X0)
| ~ q48(X1)
| ~ locatedin(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2927]) ).
fof(f2932,plain,
! [X] :
( q48(X)
| ~ q47(X) ),
inference(pre_NNF_transformation,[status(thm)],[f952]) ).
fof(f2933,plain,
! [X0] :
( q48(X0)
| ~ q47(X0) ),
inference(cnf_transformation,[status(thm)],[f2932]) ).
fof(f2934,plain,
! [X,Y] :
( q48(X)
| ~ ot____nom15(Y)
| ~ locatedin(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f953]) ).
fof(f2935,plain,
! [X] :
( q48(X)
| ! [Y] :
( ~ ot____nom15(Y)
| ~ locatedin(X,Y) ) ),
inference(miniscoping,[status(thm)],[f2934]) ).
fof(f2936,plain,
! [X0,X1] :
( q48(X0)
| ~ ot____nom15(X1)
| ~ locatedin(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2935]) ).
fof(f3010,plain,
! [X,Y] :
( q50(X)
| ~ ot____nom17(Y)
| ~ locatedin(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f982]) ).
fof(f3011,plain,
! [X] :
( q50(X)
| ! [Y] :
( ~ ot____nom17(Y)
| ~ locatedin(X,Y) ) ),
inference(miniscoping,[status(thm)],[f3010]) ).
fof(f3012,plain,
! [X0,X1] :
( q50(X0)
| ~ ot____nom17(X1)
| ~ locatedin(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3011]) ).
fof(f3105,plain,
! [X] :
( q63(X)
| ~ whiteburgundy(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1018]) ).
fof(f3106,plain,
! [X0] :
( q63(X0)
| ~ whiteburgundy(X0) ),
inference(cnf_transformation,[status(thm)],[f3105]) ).
fof(f3149,plain,
! [X] :
( q69(X)
| ~ pauillac(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1035]) ).
fof(f3150,plain,
! [X0] :
( q69(X0)
| ~ pauillac(X0) ),
inference(cnf_transformation,[status(thm)],[f3149]) ).
fof(f3180,plain,
! [X,Y] :
( q71(X)
| ~ ot____nom1(Y)
| ~ hassugar(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f1049]) ).
fof(f3181,plain,
! [X] :
( q71(X)
| ! [Y] :
( ~ ot____nom1(Y)
| ~ hassugar(X,Y) ) ),
inference(miniscoping,[status(thm)],[f3180]) ).
fof(f3182,plain,
! [X0,X1] :
( q71(X0)
| ~ ot____nom1(X1)
| ~ hassugar(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3181]) ).
fof(f3188,plain,
! [X] :
( q72(X)
| ~ redburgundy(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1052]) ).
fof(f3189,plain,
! [X0] :
( q72(X0)
| ~ redburgundy(X0) ),
inference(cnf_transformation,[status(thm)],[f3188]) ).
fof(f3195,plain,
! [X,Y] :
( q73(X)
| ~ q74(Y)
| ~ locatedin(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f1055]) ).
fof(f3196,plain,
! [X] :
( q73(X)
| ! [Y] :
( ~ q74(Y)
| ~ locatedin(X,Y) ) ),
inference(miniscoping,[status(thm)],[f3195]) ).
fof(f3197,plain,
! [X0,X1] :
( q73(X0)
| ~ q74(X1)
| ~ locatedin(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3196]) ).
fof(f3201,plain,
! [X] :
( q74(X)
| ~ q73(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1057]) ).
fof(f3202,plain,
! [X0] :
( q74(X0)
| ~ q73(X0) ),
inference(cnf_transformation,[status(thm)],[f3201]) ).
fof(f3203,plain,
! [X,Y] :
( q74(X)
| ~ ot____nom10(Y)
| ~ locatedin(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f1058]) ).
fof(f3204,plain,
! [X] :
( q74(X)
| ! [Y] :
( ~ ot____nom10(Y)
| ~ locatedin(X,Y) ) ),
inference(miniscoping,[status(thm)],[f3203]) ).
fof(f3205,plain,
! [X0,X1] :
( q74(X0)
| ~ ot____nom10(X1)
| ~ locatedin(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3204]) ).
fof(f3222,plain,
! [X] :
( americanwine(X)
| ~ wine(X)
| ~ q27(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1065]) ).
fof(f3223,plain,
! [X0] :
( americanwine(X0)
| ~ wine(X0)
| ~ q27(X0) ),
inference(cnf_transformation,[status(thm)],[f3222]) ).
fof(f3237,plain,
! [X] :
( bordeaux(X)
| ~ sauternes(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1071]) ).
fof(f3238,plain,
! [X0] :
( bordeaux(X0)
| ~ sauternes(X0) ),
inference(cnf_transformation,[status(thm)],[f3237]) ).
fof(f3239,plain,
! [X] :
( bordeaux(X)
| ~ medoc(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1072]) ).
fof(f3240,plain,
! [X0] :
( bordeaux(X0)
| ~ medoc(X0) ),
inference(cnf_transformation,[status(thm)],[f3239]) ).
fof(f3245,plain,
! [X] :
( bordeaux(X)
| ~ whitebordeaux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1075]) ).
fof(f3246,plain,
! [X0] :
( bordeaux(X0)
| ~ whitebordeaux(X0) ),
inference(cnf_transformation,[status(thm)],[f3245]) ).
fof(f3254,plain,
! [X] :
( burgundy(X)
| ~ redburgundy(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1079]) ).
fof(f3255,plain,
! [X0] :
( burgundy(X0)
| ~ redburgundy(X0) ),
inference(cnf_transformation,[status(thm)],[f3254]) ).
fof(f3267,plain,
! [X] :
( cabernetsauvignon(X)
| ~ q69(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1084]) ).
fof(f3268,plain,
! [X0] :
( cabernetsauvignon(X0)
| ~ q69(X0) ),
inference(cnf_transformation,[status(thm)],[f3267]) ).
fof(f3275,plain,
! [X] :
( californiawine(X)
| ~ wine(X)
| ~ q48(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1087]) ).
fof(f3276,plain,
! [X0] :
( californiawine(X0)
| ~ wine(X0)
| ~ q48(X0) ),
inference(cnf_transformation,[status(thm)],[f3275]) ).
fof(f3280,plain,
! [X] :
( chardonnay(X)
| ~ q63(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1089]) ).
fof(f3281,plain,
! [X0] :
( chardonnay(X0)
| ~ q63(X0) ),
inference(cnf_transformation,[status(thm)],[f3280]) ).
fof(f3306,plain,
! [X] :
( dessertwine(X)
| ~ icewine(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1099]) ).
fof(f3307,plain,
! [X0] :
( dessertwine(X0)
| ~ icewine(X0) ),
inference(cnf_transformation,[status(thm)],[f3306]) ).
fof(f3311,plain,
! [X] :
( dryredwine(X)
| ~ redwine(X)
| ~ drywine(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1101]) ).
fof(f3312,plain,
! [X0] :
( dryredwine(X0)
| ~ redwine(X0)
| ~ drywine(X0) ),
inference(cnf_transformation,[status(thm)],[f3311]) ).
fof(f3321,plain,
! [X] :
( drywhitewine(X)
| ~ whitewine(X)
| ~ drywine(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1105]) ).
fof(f3322,plain,
! [X0] :
( drywhitewine(X0)
| ~ whitewine(X0)
| ~ drywine(X0) ),
inference(cnf_transformation,[status(thm)],[f3321]) ).
fof(f3330,plain,
! [X] :
( drywine(X)
| ~ wine(X)
| ~ q46(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1109]) ).
fof(f3331,plain,
! [X0] :
( drywine(X0)
| ~ wine(X0)
| ~ q46(X0) ),
inference(cnf_transformation,[status(thm)],[f3330]) ).
fof(f3343,plain,
! [X] :
( fullbodiedwine(X)
| ~ q35(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1114]) ).
fof(f3344,plain,
! [X0] :
( fullbodiedwine(X0)
| ~ q35(X0) ),
inference(cnf_transformation,[status(thm)],[f3343]) ).
fof(f3351,plain,
! [X] :
( gamay(X)
| ~ q14(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1117]) ).
fof(f3352,plain,
! [X0] :
( gamay(X0)
| ~ q14(X0) ),
inference(cnf_transformation,[status(thm)],[f3351]) ).
fof(f3359,plain,
! [X] :
( germanwine(X)
| ~ wine(X)
| ~ q50(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1120]) ).
fof(f3360,plain,
! [X0] :
( germanwine(X0)
| ~ wine(X0)
| ~ q50(X0) ),
inference(cnf_transformation,[status(thm)],[f3359]) ).
fof(f3364,plain,
! [X] :
( grape(X)
| ~ winegrape(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1122]) ).
fof(f3365,plain,
! [X0] :
( grape(X0)
| ~ winegrape(X0) ),
inference(cnf_transformation,[status(thm)],[f3364]) ).
fof(f3374,plain,
! [X] :
( italianwine(X)
| ~ chianti(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1126]) ).
fof(f3375,plain,
! [X0] :
( italianwine(X0)
| ~ chianti(X0) ),
inference(cnf_transformation,[status(thm)],[f3374]) ).
fof(f3381,plain,
! [X] :
( lateharvest(X)
| ~ icewine(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1129]) ).
fof(f3382,plain,
! [X0] :
( lateharvest(X0)
| ~ icewine(X0) ),
inference(cnf_transformation,[status(thm)],[f3381]) ).
fof(f3392,plain,
! [X] :
( loire(X)
| ~ whiteloire(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1134]) ).
fof(f3393,plain,
! [X0] :
( loire(X0)
| ~ whiteloire(X0) ),
inference(cnf_transformation,[status(thm)],[f3392]) ).
fof(f3396,plain,
! [X] :
( loire(X)
| ~ muscadet(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1136]) ).
fof(f3397,plain,
! [X0] :
( loire(X0)
| ~ muscadet(X0) ),
inference(cnf_transformation,[status(thm)],[f3396]) ).
fof(f3410,plain,
! [X] :
( medoc(X)
| ~ margaux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1142]) ).
fof(f3411,plain,
! [X0] :
( medoc(X0)
| ~ margaux(X0) ),
inference(cnf_transformation,[status(thm)],[f3410]) ).
fof(f3422,plain,
! [X] :
( merlot(X)
| ~ q13(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1147]) ).
fof(f3423,plain,
! [X0] :
( merlot(X0)
| ~ q13(X0) ),
inference(cnf_transformation,[status(thm)],[f3422]) ).
fof(f3451,plain,
! [X] :
( pinotblanc(X)
| ~ q24(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1158]) ).
fof(f3452,plain,
! [X0] :
( pinotblanc(X0)
| ~ q24(X0) ),
inference(cnf_transformation,[status(thm)],[f3451]) ).
fof(f3459,plain,
! [X] :
( pinotnoir(X)
| ~ q72(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1161]) ).
fof(f3460,plain,
! [X0] :
( pinotnoir(X0)
| ~ q72(X0) ),
inference(cnf_transformation,[status(thm)],[f3459]) ).
fof(f3470,plain,
! [X] :
( potableliquid(X)
| ~ wine(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1165]) ).
fof(f3471,plain,
! [X0] :
( potableliquid(X0)
| ~ wine(X0) ),
inference(cnf_transformation,[status(thm)],[f3470]) ).
fof(f3475,plain,
! [X] :
( redbordeaux(X)
| ~ bordeaux(X)
| ~ redwine(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1167]) ).
fof(f3476,plain,
! [X0] :
( redbordeaux(X0)
| ~ bordeaux(X0)
| ~ redwine(X0) ),
inference(cnf_transformation,[status(thm)],[f3475]) ).
fof(f3480,plain,
! [X] :
( redburgundy(X)
| ~ cotesdor(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1169]) ).
fof(f3481,plain,
! [X0] :
( redburgundy(X0)
| ~ cotesdor(X0) ),
inference(cnf_transformation,[status(thm)],[f3480]) ).
fof(f3498,plain,
! [X] :
( redwine(X)
| ~ port(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1177]) ).
fof(f3499,plain,
! [X0] :
( redwine(X0)
| ~ port(X0) ),
inference(cnf_transformation,[status(thm)],[f3498]) ).
fof(f3500,plain,
! [X] :
( redwine(X)
| ~ wine(X)
| ~ q41(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1178]) ).
fof(f3501,plain,
! [X0] :
( redwine(X0)
| ~ wine(X0)
| ~ q41(X0) ),
inference(cnf_transformation,[status(thm)],[f3500]) ).
fof(f3508,plain,
! [X,Y] :
( region(Y)
| ~ locatedin(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f1181]) ).
fof(f3509,plain,
! [Y] :
( region(Y)
| ! [X] : ~ locatedin(X,Y) ),
inference(miniscoping,[status(thm)],[f3508]) ).
fof(f3510,plain,
! [X0,X1] :
( region(X1)
| ~ locatedin(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3509]) ).
fof(f3521,plain,
! [X] :
( riesling(X)
| ~ sweetriesling(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1186]) ).
fof(f3522,plain,
! [X0] :
( riesling(X0)
| ~ sweetriesling(X0) ),
inference(cnf_transformation,[status(thm)],[f3521]) ).
fof(f3529,plain,
! [X] :
( rosewine(X)
| ~ q15(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1189]) ).
fof(f3530,plain,
! [X0] :
( rosewine(X0)
| ~ q15(X0) ),
inference(cnf_transformation,[status(thm)],[f3529]) ).
fof(f3559,plain,
! [X] :
( semillonorsauvignonblanc(X)
| ~ semillon(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1200]) ).
fof(f3560,plain,
! [X0] :
( semillonorsauvignonblanc(X0)
| ~ semillon(X0) ),
inference(cnf_transformation,[status(thm)],[f3559]) ).
fof(f3561,plain,
! [X] :
( semillonorsauvignonblanc(X)
| ~ sauvignonblanc(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1201]) ).
fof(f3562,plain,
! [X0] :
( semillonorsauvignonblanc(X0)
| ~ sauvignonblanc(X0) ),
inference(cnf_transformation,[status(thm)],[f3561]) ).
fof(f3580,plain,
! [X] :
( sweetwine(X)
| ~ wine(X)
| ~ q71(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1209]) ).
fof(f3581,plain,
! [X0] :
( sweetwine(X0)
| ~ wine(X0)
| ~ q71(X0) ),
inference(cnf_transformation,[status(thm)],[f3580]) ).
fof(f3585,plain,
! [X] :
( tablewine(X)
| ~ whitetablewine(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1211]) ).
fof(f3586,plain,
! [X0] :
( tablewine(X0)
| ~ whitetablewine(X0) ),
inference(cnf_transformation,[status(thm)],[f3585]) ).
fof(f3589,plain,
! [X] :
( tablewine(X)
| ~ wine(X)
| ~ q46(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1213]) ).
fof(f3590,plain,
! [X0] :
( tablewine(X0)
| ~ wine(X0)
| ~ q46(X0) ),
inference(cnf_transformation,[status(thm)],[f3589]) ).
fof(f3594,plain,
! [X] :
( texaswine(X)
| ~ wine(X)
| ~ q74(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1215]) ).
fof(f3595,plain,
! [X0] :
( texaswine(X0)
| ~ wine(X0)
| ~ q74(X0) ),
inference(cnf_transformation,[status(thm)],[f3594]) ).
fof(f3604,plain,
! [X,Y] :
( vintage(X)
| ~ hasvintageyear(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f1219]) ).
fof(f3605,plain,
! [X] :
( vintage(X)
| ! [Y] : ~ hasvintageyear(X,Y) ),
inference(miniscoping,[status(thm)],[f3604]) ).
fof(f3606,plain,
! [X0,X1] :
( vintage(X0)
| ~ hasvintageyear(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3605]) ).
fof(f3616,plain,
! [X] :
( whitebordeaux(X)
| ~ whitewine(X)
| ~ bordeaux(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1223]) ).
fof(f3617,plain,
! [X0] :
( whitebordeaux(X0)
| ~ whitewine(X0)
| ~ bordeaux(X0) ),
inference(cnf_transformation,[status(thm)],[f3616]) ).
fof(f3621,plain,
! [X] :
( whiteburgundy(X)
| ~ meursault(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1225]) ).
fof(f3622,plain,
! [X0] :
( whiteburgundy(X0)
| ~ meursault(X0) ),
inference(cnf_transformation,[status(thm)],[f3621]) ).
fof(f3628,plain,
! [X] :
( whiteloire(X)
| ~ whitewine(X)
| ~ loire(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1228]) ).
fof(f3629,plain,
! [X0] :
( whiteloire(X0)
| ~ whitewine(X0)
| ~ loire(X0) ),
inference(cnf_transformation,[status(thm)],[f3628]) ).
fof(f3635,plain,
! [X] :
( whitenonsweetwine(X)
| ~ whitewine(X)
| ~ q36(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1231]) ).
fof(f3636,plain,
! [X0] :
( whitenonsweetwine(X0)
| ~ whitewine(X0)
| ~ q36(X0) ),
inference(cnf_transformation,[status(thm)],[f3635]) ).
fof(f3642,plain,
! [X] :
( whitetablewine(X)
| ~ tablewine(X)
| ~ q21(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1234]) ).
fof(f3643,plain,
! [X0] :
( whitetablewine(X0)
| ~ tablewine(X0)
| ~ q21(X0) ),
inference(cnf_transformation,[status(thm)],[f3642]) ).
fof(f3649,plain,
! [X] :
( whitewine(X)
| ~ whiteburgundy(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1237]) ).
fof(f3650,plain,
! [X0] :
( whitewine(X0)
| ~ whiteburgundy(X0) ),
inference(cnf_transformation,[status(thm)],[f3649]) ).
fof(f3657,plain,
! [X] :
( whitewine(X)
| ~ wine(X)
| ~ q21(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1241]) ).
fof(f3658,plain,
! [X0] :
( whitewine(X0)
| ~ wine(X0)
| ~ q21(X0) ),
inference(cnf_transformation,[status(thm)],[f3657]) ).
fof(f3668,plain,
! [X] :
( wine(X)
| ~ q20(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1246]) ).
fof(f3669,plain,
! [X0] :
( wine(X0)
| ~ q20(X0) ),
inference(cnf_transformation,[status(thm)],[f3668]) ).
fof(f3675,plain,
! [X] :
( wine(X)
| ~ q31(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1249]) ).
fof(f3676,plain,
! [X0] :
( wine(X0)
| ~ q31(X0) ),
inference(cnf_transformation,[status(thm)],[f3675]) ).
fof(f3689,plain,
! [X] :
( wine(X)
| ~ q0(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1256]) ).
fof(f3690,plain,
! [X0] :
( wine(X0)
| ~ q0(X0) ),
inference(cnf_transformation,[status(thm)],[f3689]) ).
fof(f3696,plain,
! [X] :
( wine(X)
| ~ semillonorsauvignonblanc(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1259]) ).
fof(f3697,plain,
! [X0] :
( wine(X0)
| ~ semillonorsauvignonblanc(X0) ),
inference(cnf_transformation,[status(thm)],[f3696]) ).
fof(f3706,plain,
! [X] :
( wine(X)
| ~ q12(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1264]) ).
fof(f3707,plain,
! [X0] :
( wine(X0)
| ~ q12(X0) ),
inference(cnf_transformation,[status(thm)],[f3706]) ).
fof(f3739,plain,
! [X] :
( wine(X)
| ~ whitewine(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1280]) ).
fof(f3740,plain,
! [X0] :
( wine(X0)
| ~ whitewine(X0) ),
inference(cnf_transformation,[status(thm)],[f3739]) ).
fof(f3741,plain,
! [X] :
( wine(X)
| ~ dessertwine(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1281]) ).
fof(f3742,plain,
! [X0] :
( wine(X0)
| ~ dessertwine(X0) ),
inference(cnf_transformation,[status(thm)],[f3741]) ).
fof(f3795,plain,
! [X] :
( winecolor(X)
| ~ winedescriptor(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1306]) ).
fof(f3796,plain,
! [X0] :
( winecolor(X0)
| ~ winedescriptor(X0) ),
inference(cnf_transformation,[status(thm)],[f3795]) ).
fof(f3802,plain,
! [X] :
( winedescriptor(X)
| ~ winetaste(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1309]) ).
fof(f3803,plain,
! [X0] :
( winedescriptor(X0)
| ~ winetaste(X0) ),
inference(cnf_transformation,[status(thm)],[f3802]) ).
fof(f3804,plain,
! [X,Y] :
( winedescriptor(Y)
| ~ haswinedescriptor(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f1310]) ).
fof(f3805,plain,
! [Y] :
( winedescriptor(Y)
| ! [X] : ~ haswinedescriptor(X,Y) ),
inference(miniscoping,[status(thm)],[f3804]) ).
fof(f3806,plain,
! [X0,X1] :
( winedescriptor(X1)
| ~ haswinedescriptor(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3805]) ).
fof(f3818,plain,
! [X,Y] :
( winegrape(Y)
| ~ madefromgrape(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f1315]) ).
fof(f3819,plain,
! [Y] :
( winegrape(Y)
| ! [X] : ~ madefromgrape(X,Y) ),
inference(miniscoping,[status(thm)],[f3818]) ).
fof(f3820,plain,
! [X0,X1] :
( winegrape(X1)
| ~ madefromgrape(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3819]) ).
fof(f3836,plain,
! [X] :
( winetaste(X)
| ~ winebody(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1322]) ).
fof(f3837,plain,
! [X0] :
( winetaste(X0)
| ~ winebody(X0) ),
inference(cnf_transformation,[status(thm)],[f3836]) ).
fof(f3838,plain,
! [X] :
( winetaste(X)
| ~ winedescriptor(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1323]) ).
fof(f3839,plain,
! [X0] :
( winetaste(X0)
| ~ winedescriptor(X0) ),
inference(cnf_transformation,[status(thm)],[f3838]) ).
fof(f4237,plain,
! [X] :
( hasbody(X,X)
| ~ kaon2namedobjects(X)
| ~ wine(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1475]) ).
fof(f4238,plain,
! [X0] :
( hasbody(X0,X0)
| ~ kaon2namedobjects(X0)
| ~ wine(X0) ),
inference(cnf_transformation,[status(thm)],[f4237]) ).
fof(f4253,plain,
! [X] :
( hascolor(X,X)
| ~ kaon2namedobjects(X)
| ~ wine(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1482]) ).
fof(f4254,plain,
! [X0] :
( hascolor(X0,X0)
| ~ kaon2namedobjects(X0)
| ~ wine(X0) ),
inference(cnf_transformation,[status(thm)],[f4253]) ).
fof(f4263,plain,
! [X] :
( hasflavor(X,X)
| ~ kaon2namedobjects(X)
| ~ q4(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1486]) ).
fof(f4264,plain,
! [X0] :
( hasflavor(X0,X0)
| ~ kaon2namedobjects(X0)
| ~ q4(X0) ),
inference(cnf_transformation,[status(thm)],[f4263]) ).
fof(f4277,plain,
! [X,Y] :
( hasmaker(Y,X)
| ~ produceswine(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f1492]) ).
fof(f4278,plain,
! [X0,X1] :
( hasmaker(X1,X0)
| ~ produceswine(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4277]) ).
fof(f4287,plain,
! [X] :
( hassugar(X,X)
| ~ kaon2namedobjects(X)
| ~ wine(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1496]) ).
fof(f4288,plain,
! [X0] :
( hassugar(X0,X0)
| ~ kaon2namedobjects(X0)
| ~ wine(X0) ),
inference(cnf_transformation,[status(thm)],[f4287]) ).
fof(f4313,plain,
! [X,Y] :
( haswinedescriptor(X,Y)
| ~ hascolor(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f1507]) ).
fof(f4314,plain,
! [X0,X1] :
( haswinedescriptor(X0,X1)
| ~ hascolor(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4313]) ).
fof(f4387,plain,
! [X,Y] :
( madefromfruit(X,Y)
| ~ madefromgrape(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f1541]) ).
fof(f4388,plain,
! [X0,X1] :
( madefromfruit(X0,X1)
| ~ madefromgrape(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4387]) ).
fof(f4437,plain,
! [X,Y] :
( madeintowine(Y,X)
| ~ madefromgrape(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f1564]) ).
fof(f4438,plain,
! [X0,X1] :
( madeintowine(X1,X0)
| ~ madefromgrape(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4437]) ).
fof(f4445,plain,
! [X,Y] :
( produceswine(Y,X)
| ~ hasmaker(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f1567]) ).
fof(f4446,plain,
! [X0,X1] :
( produceswine(X1,X0)
| ~ hasmaker(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4445]) ).
fof(f4551,plain,
( ! [Y,X] : ~ produceswine(X,Y)
| ! [Y,X] : ~ madeintowine(X,Y)
| ! [Y,X] : ~ madefromfruit(X,Y)
| ! [Y,X] : ~ madefromgrape(X,Y)
| ! [Y,X] : ~ locatedin(X,Y)
| ! [Y,X] : ~ haswinedescriptor(X,Y)
| ! [Y,X] : ~ hasvintageyear(X,Y)
| ! [Y,X] : ~ hassugar(X,Y)
| ! [Y,X] : ~ hasmaker(X,Y)
| ! [Y,X] : ~ hasflavor(X,Y)
| ! [Y,X] : ~ hascolor(X,Y)
| ! [Y,X] : ~ hasbody(X,Y)
| ! [X] : ~ zinfandel(X)
| ! [X] : ~ winetaste(X)
| ! [X] : ~ winery(X)
| ! [X] : ~ winesugar(X)
| ! [X] : ~ winegrape(X)
| ! [X] : ~ wineflavor(X)
| ! [X] : ~ winedescriptor(X)
| ! [X] : ~ winecolor(X)
| ! [X] : ~ winebody(X)
| ! [X] : ~ wine(X)
| ! [X] : ~ whitewine(X)
| ! [X] : ~ whitetablewine(X)
| ! [X] : ~ whitenonsweetwine(X)
| ! [X] : ~ whiteloire(X)
| ! [X] : ~ whiteburgundy(X)
| ! [X] : ~ whitebordeaux(X)
| ! [X] : ~ vintageyear(X)
| ! [X] : ~ vintage(X)
| ! [X] : ~ texaswine(X)
| ! [X] : ~ tablewine(X)
| ! [X] : ~ sweetwine(X)
| ! [X] : ~ sweetriesling(X)
| ! [X] : ~ stemilion(X)
| ! [X] : ~ semillonorsauvignonblanc(X)
| ! [X] : ~ semillon(X)
| ! [X] : ~ sauvignonblanc(X)
| ! [X] : ~ sauternes(X)
| ! [X] : ~ sancerre(X)
| ! [X] : ~ rosewine(X)
| ! [X] : ~ riesling(X)
| ! [X] : ~ region(X)
| ! [X] : ~ redwine(X)
| ! [X] : ~ redtablewine(X)
| ! [X] : ~ redburgundy(X)
| ! [X] : ~ redbordeaux(X)
| ! [X] : ~ potableliquid(X)
| ! [X] : ~ port(X)
| ! [X] : ~ pinotnoir(X)
| ! [X] : ~ pinotblanc(X)
| ! [X] : ~ petitesyrah(X)
| ! [X] : ~ pauillac(X)
| ! [X] : ~ muscadet(X)
| ! [X] : ~ meursault(X)
| ! [X] : ~ merlot(X)
| ! [X] : ~ meritage(X)
| ! [X] : ~ medoc(X)
| ! [X] : ~ margaux(X)
| ! [X] : ~ loire(X)
| ! [X] : ~ lateharvest(X)
| ! [X] : ~ italianwine(X)
| ! [X] : ~ icewine(X)
| ! [X] : ~ grape(X)
| ! [X] : ~ germanwine(X)
| ! [X] : ~ gamay(X)
| ! [X] : ~ fullbodiedwine(X)
| ! [X] : ~ drywine(X)
| ! [X] : ~ drywhitewine(X)
| ! [X] : ~ dryredwine(X)
| ! [X] : ~ dryriesling(X)
| ! [X] : ~ dessertwine(X)
| ! [X] : ~ cotesdor(X)
| ! [X] : ~ chianti(X)
| ! [X] : ~ cheninblanc(X)
| ! [X] : ~ chardonnay(X)
| ! [X] : ~ californiawine(X)
| ! [X] : ~ cabernetsauvignon(X)
| ! [X] : ~ cabernetfranc(X)
| ! [X] : ~ beaujolais(X)
| ! [X] : ~ anjou(X)
| ! [X] : ~ burgundy(X)
| ! [X] : ~ bordeaux(X)
| ! [X] : ~ americanwine(X)
| ! [X] : ~ californiawine(X) ),
inference(pre_NNF_transformation,[status(thm)],[f1616]) ).
fof(f4552,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56,X57,X58,X59,X60,X61,X62,X63,X64,X65,X66,X67,X68,X69,X70,X71,X72,X73,X74,X75,X76,X77,X78,X79,X80,X81,X82,X83,X84,X85,X86,X87,X88,X89,X90,X91,X92,X93,X94,X95,X96] :
( ~ produceswine(X95,X96)
| ~ madeintowine(X93,X94)
| ~ madefromfruit(X91,X92)
| ~ madefromgrape(X89,X90)
| ~ locatedin(X87,X88)
| ~ haswinedescriptor(X85,X86)
| ~ hasvintageyear(X83,X84)
| ~ hassugar(X81,X82)
| ~ hasmaker(X79,X80)
| ~ hasflavor(X77,X78)
| ~ hascolor(X75,X76)
| ~ hasbody(X73,X74)
| ~ zinfandel(X72)
| ~ winetaste(X71)
| ~ winery(X70)
| ~ winesugar(X69)
| ~ winegrape(X68)
| ~ wineflavor(X67)
| ~ winedescriptor(X66)
| ~ winecolor(X65)
| ~ winebody(X64)
| ~ wine(X63)
| ~ whitewine(X62)
| ~ whitetablewine(X61)
| ~ whitenonsweetwine(X60)
| ~ whiteloire(X59)
| ~ whiteburgundy(X58)
| ~ whitebordeaux(X57)
| ~ vintageyear(X56)
| ~ vintage(X55)
| ~ texaswine(X54)
| ~ tablewine(X53)
| ~ sweetwine(X52)
| ~ sweetriesling(X51)
| ~ stemilion(X50)
| ~ semillonorsauvignonblanc(X49)
| ~ semillon(X48)
| ~ sauvignonblanc(X47)
| ~ sauternes(X46)
| ~ sancerre(X45)
| ~ rosewine(X44)
| ~ riesling(X43)
| ~ region(X42)
| ~ redwine(X41)
| ~ redtablewine(X40)
| ~ redburgundy(X39)
| ~ redbordeaux(X38)
| ~ potableliquid(X37)
| ~ port(X36)
| ~ pinotnoir(X35)
| ~ pinotblanc(X34)
| ~ petitesyrah(X33)
| ~ pauillac(X32)
| ~ muscadet(X31)
| ~ meursault(X30)
| ~ merlot(X29)
| ~ meritage(X28)
| ~ medoc(X27)
| ~ margaux(X26)
| ~ loire(X25)
| ~ lateharvest(X24)
| ~ italianwine(X23)
| ~ icewine(X22)
| ~ grape(X21)
| ~ germanwine(X20)
| ~ gamay(X19)
| ~ fullbodiedwine(X18)
| ~ drywine(X17)
| ~ drywhitewine(X16)
| ~ dryredwine(X15)
| ~ dryriesling(X14)
| ~ dessertwine(X13)
| ~ cotesdor(X12)
| ~ chianti(X11)
| ~ cheninblanc(X10)
| ~ chardonnay(X9)
| ~ californiawine(X8)
| ~ cabernetsauvignon(X7)
| ~ cabernetfranc(X6)
| ~ beaujolais(X5)
| ~ anjou(X4)
| ~ burgundy(X3)
| ~ bordeaux(X2)
| ~ americanwine(X1)
| ~ californiawine(X0) ),
inference(cnf_transformation,[status(thm)],[f4551]) ).
fof(f4553,definition,
! [X0] :
( sQ0_spl
<=> ~ californiawine(X0) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f4554,plain,
! [X0] :
( ~ sQ0_spl
| ~ californiawine(X0) ),
inference(component_clause,[status(thm)],[f4553]) ).
fof(f4556,definition,
! [X1] :
( sQ1_spl
<=> ~ americanwine(X1) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f4557,plain,
! [X0] :
( ~ sQ1_spl
| ~ americanwine(X0) ),
inference(component_clause,[status(thm)],[f4556]) ).
fof(f4559,definition,
! [X2] :
( sQ2_spl
<=> ~ bordeaux(X2) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f4560,plain,
! [X0] :
( ~ sQ2_spl
| ~ bordeaux(X0) ),
inference(component_clause,[status(thm)],[f4559]) ).
fof(f4562,definition,
! [X3] :
( sQ3_spl
<=> ~ burgundy(X3) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f4563,plain,
! [X0] :
( ~ sQ3_spl
| ~ burgundy(X0) ),
inference(component_clause,[status(thm)],[f4562]) ).
fof(f4565,definition,
! [X4] :
( sQ4_spl
<=> ~ anjou(X4) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f4566,plain,
! [X0] :
( ~ sQ4_spl
| ~ anjou(X0) ),
inference(component_clause,[status(thm)],[f4565]) ).
fof(f4568,definition,
! [X5] :
( sQ5_spl
<=> ~ beaujolais(X5) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f4569,plain,
! [X0] :
( ~ sQ5_spl
| ~ beaujolais(X0) ),
inference(component_clause,[status(thm)],[f4568]) ).
fof(f4571,definition,
! [X6] :
( sQ6_spl
<=> ~ cabernetfranc(X6) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f4572,plain,
! [X0] :
( ~ sQ6_spl
| ~ cabernetfranc(X0) ),
inference(component_clause,[status(thm)],[f4571]) ).
fof(f4574,definition,
! [X7] :
( sQ7_spl
<=> ~ cabernetsauvignon(X7) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f4575,plain,
! [X0] :
( ~ sQ7_spl
| ~ cabernetsauvignon(X0) ),
inference(component_clause,[status(thm)],[f4574]) ).
fof(f4577,definition,
! [X9] :
( sQ8_spl
<=> ~ chardonnay(X9) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f4578,plain,
! [X0] :
( ~ sQ8_spl
| ~ chardonnay(X0) ),
inference(component_clause,[status(thm)],[f4577]) ).
fof(f4580,definition,
! [X10] :
( sQ9_spl
<=> ~ cheninblanc(X10) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f4581,plain,
! [X0] :
( ~ sQ9_spl
| ~ cheninblanc(X0) ),
inference(component_clause,[status(thm)],[f4580]) ).
fof(f4583,definition,
! [X11] :
( sQ10_spl
<=> ~ chianti(X11) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f4584,plain,
! [X0] :
( ~ sQ10_spl
| ~ chianti(X0) ),
inference(component_clause,[status(thm)],[f4583]) ).
fof(f4586,definition,
! [X12] :
( sQ11_spl
<=> ~ cotesdor(X12) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f4587,plain,
! [X0] :
( ~ sQ11_spl
| ~ cotesdor(X0) ),
inference(component_clause,[status(thm)],[f4586]) ).
fof(f4589,definition,
! [X13] :
( sQ12_spl
<=> ~ dessertwine(X13) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f4590,plain,
! [X0] :
( ~ sQ12_spl
| ~ dessertwine(X0) ),
inference(component_clause,[status(thm)],[f4589]) ).
fof(f4592,definition,
! [X14] :
( sQ13_spl
<=> ~ dryriesling(X14) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f4593,plain,
! [X0] :
( ~ sQ13_spl
| ~ dryriesling(X0) ),
inference(component_clause,[status(thm)],[f4592]) ).
fof(f4595,definition,
! [X15] :
( sQ14_spl
<=> ~ dryredwine(X15) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f4596,plain,
! [X0] :
( ~ sQ14_spl
| ~ dryredwine(X0) ),
inference(component_clause,[status(thm)],[f4595]) ).
fof(f4598,definition,
! [X16] :
( sQ15_spl
<=> ~ drywhitewine(X16) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f4599,plain,
! [X0] :
( ~ sQ15_spl
| ~ drywhitewine(X0) ),
inference(component_clause,[status(thm)],[f4598]) ).
fof(f4601,definition,
! [X17] :
( sQ16_spl
<=> ~ drywine(X17) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f4602,plain,
! [X0] :
( ~ sQ16_spl
| ~ drywine(X0) ),
inference(component_clause,[status(thm)],[f4601]) ).
fof(f4604,definition,
! [X18] :
( sQ17_spl
<=> ~ fullbodiedwine(X18) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f4605,plain,
! [X0] :
( ~ sQ17_spl
| ~ fullbodiedwine(X0) ),
inference(component_clause,[status(thm)],[f4604]) ).
fof(f4607,definition,
! [X19] :
( sQ18_spl
<=> ~ gamay(X19) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f4608,plain,
! [X0] :
( ~ sQ18_spl
| ~ gamay(X0) ),
inference(component_clause,[status(thm)],[f4607]) ).
fof(f4610,definition,
! [X20] :
( sQ19_spl
<=> ~ germanwine(X20) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f4611,plain,
! [X0] :
( ~ sQ19_spl
| ~ germanwine(X0) ),
inference(component_clause,[status(thm)],[f4610]) ).
fof(f4613,definition,
! [X21] :
( sQ20_spl
<=> ~ grape(X21) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f4614,plain,
! [X0] :
( ~ sQ20_spl
| ~ grape(X0) ),
inference(component_clause,[status(thm)],[f4613]) ).
fof(f4616,definition,
! [X22] :
( sQ21_spl
<=> ~ icewine(X22) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f4617,plain,
! [X0] :
( ~ sQ21_spl
| ~ icewine(X0) ),
inference(component_clause,[status(thm)],[f4616]) ).
fof(f4619,definition,
! [X23] :
( sQ22_spl
<=> ~ italianwine(X23) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f4620,plain,
! [X0] :
( ~ sQ22_spl
| ~ italianwine(X0) ),
inference(component_clause,[status(thm)],[f4619]) ).
fof(f4622,definition,
! [X24] :
( sQ23_spl
<=> ~ lateharvest(X24) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f4623,plain,
! [X0] :
( ~ sQ23_spl
| ~ lateharvest(X0) ),
inference(component_clause,[status(thm)],[f4622]) ).
fof(f4625,definition,
! [X25] :
( sQ24_spl
<=> ~ loire(X25) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f4626,plain,
! [X0] :
( ~ sQ24_spl
| ~ loire(X0) ),
inference(component_clause,[status(thm)],[f4625]) ).
fof(f4628,definition,
! [X26] :
( sQ25_spl
<=> ~ margaux(X26) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f4629,plain,
! [X0] :
( ~ sQ25_spl
| ~ margaux(X0) ),
inference(component_clause,[status(thm)],[f4628]) ).
fof(f4631,definition,
! [X27] :
( sQ26_spl
<=> ~ medoc(X27) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f4632,plain,
! [X0] :
( ~ sQ26_spl
| ~ medoc(X0) ),
inference(component_clause,[status(thm)],[f4631]) ).
fof(f4634,definition,
! [X28] :
( sQ27_spl
<=> ~ meritage(X28) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f4635,plain,
! [X0] :
( ~ sQ27_spl
| ~ meritage(X0) ),
inference(component_clause,[status(thm)],[f4634]) ).
fof(f4637,definition,
! [X29] :
( sQ28_spl
<=> ~ merlot(X29) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f4638,plain,
! [X0] :
( ~ sQ28_spl
| ~ merlot(X0) ),
inference(component_clause,[status(thm)],[f4637]) ).
fof(f4640,definition,
! [X30] :
( sQ29_spl
<=> ~ meursault(X30) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f4641,plain,
! [X0] :
( ~ sQ29_spl
| ~ meursault(X0) ),
inference(component_clause,[status(thm)],[f4640]) ).
fof(f4643,definition,
! [X31] :
( sQ30_spl
<=> ~ muscadet(X31) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f4644,plain,
! [X0] :
( ~ sQ30_spl
| ~ muscadet(X0) ),
inference(component_clause,[status(thm)],[f4643]) ).
fof(f4646,definition,
! [X32] :
( sQ31_spl
<=> ~ pauillac(X32) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f4647,plain,
! [X0] :
( ~ sQ31_spl
| ~ pauillac(X0) ),
inference(component_clause,[status(thm)],[f4646]) ).
fof(f4649,definition,
! [X33] :
( sQ32_spl
<=> ~ petitesyrah(X33) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f4650,plain,
! [X0] :
( ~ sQ32_spl
| ~ petitesyrah(X0) ),
inference(component_clause,[status(thm)],[f4649]) ).
fof(f4652,definition,
! [X34] :
( sQ33_spl
<=> ~ pinotblanc(X34) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f4653,plain,
! [X0] :
( ~ sQ33_spl
| ~ pinotblanc(X0) ),
inference(component_clause,[status(thm)],[f4652]) ).
fof(f4655,definition,
! [X35] :
( sQ34_spl
<=> ~ pinotnoir(X35) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f4656,plain,
! [X0] :
( ~ sQ34_spl
| ~ pinotnoir(X0) ),
inference(component_clause,[status(thm)],[f4655]) ).
fof(f4658,definition,
! [X36] :
( sQ35_spl
<=> ~ port(X36) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f4659,plain,
! [X0] :
( ~ sQ35_spl
| ~ port(X0) ),
inference(component_clause,[status(thm)],[f4658]) ).
fof(f4661,definition,
! [X37] :
( sQ36_spl
<=> ~ potableliquid(X37) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f4662,plain,
! [X0] :
( ~ sQ36_spl
| ~ potableliquid(X0) ),
inference(component_clause,[status(thm)],[f4661]) ).
fof(f4664,definition,
! [X38] :
( sQ37_spl
<=> ~ redbordeaux(X38) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f4665,plain,
! [X0] :
( ~ sQ37_spl
| ~ redbordeaux(X0) ),
inference(component_clause,[status(thm)],[f4664]) ).
fof(f4667,definition,
! [X39] :
( sQ38_spl
<=> ~ redburgundy(X39) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f4668,plain,
! [X0] :
( ~ sQ38_spl
| ~ redburgundy(X0) ),
inference(component_clause,[status(thm)],[f4667]) ).
fof(f4670,definition,
! [X40] :
( sQ39_spl
<=> ~ redtablewine(X40) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f4671,plain,
! [X0] :
( ~ sQ39_spl
| ~ redtablewine(X0) ),
inference(component_clause,[status(thm)],[f4670]) ).
fof(f4673,definition,
! [X41] :
( sQ40_spl
<=> ~ redwine(X41) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f4674,plain,
! [X0] :
( ~ sQ40_spl
| ~ redwine(X0) ),
inference(component_clause,[status(thm)],[f4673]) ).
fof(f4676,definition,
! [X42] :
( sQ41_spl
<=> ~ region(X42) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f4677,plain,
! [X0] :
( ~ sQ41_spl
| ~ region(X0) ),
inference(component_clause,[status(thm)],[f4676]) ).
fof(f4679,definition,
! [X43] :
( sQ42_spl
<=> ~ riesling(X43) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f4680,plain,
! [X0] :
( ~ sQ42_spl
| ~ riesling(X0) ),
inference(component_clause,[status(thm)],[f4679]) ).
fof(f4682,definition,
! [X44] :
( sQ43_spl
<=> ~ rosewine(X44) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f4683,plain,
! [X0] :
( ~ sQ43_spl
| ~ rosewine(X0) ),
inference(component_clause,[status(thm)],[f4682]) ).
fof(f4685,definition,
! [X45] :
( sQ44_spl
<=> ~ sancerre(X45) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f4686,plain,
! [X0] :
( ~ sQ44_spl
| ~ sancerre(X0) ),
inference(component_clause,[status(thm)],[f4685]) ).
fof(f4688,definition,
! [X46] :
( sQ45_spl
<=> ~ sauternes(X46) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f4689,plain,
! [X0] :
( ~ sQ45_spl
| ~ sauternes(X0) ),
inference(component_clause,[status(thm)],[f4688]) ).
fof(f4691,definition,
! [X47] :
( sQ46_spl
<=> ~ sauvignonblanc(X47) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f4692,plain,
! [X0] :
( ~ sQ46_spl
| ~ sauvignonblanc(X0) ),
inference(component_clause,[status(thm)],[f4691]) ).
fof(f4694,definition,
! [X48] :
( sQ47_spl
<=> ~ semillon(X48) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f4695,plain,
! [X0] :
( ~ sQ47_spl
| ~ semillon(X0) ),
inference(component_clause,[status(thm)],[f4694]) ).
fof(f4697,definition,
! [X49] :
( sQ48_spl
<=> ~ semillonorsauvignonblanc(X49) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f4698,plain,
! [X0] :
( ~ sQ48_spl
| ~ semillonorsauvignonblanc(X0) ),
inference(component_clause,[status(thm)],[f4697]) ).
fof(f4700,definition,
! [X50] :
( sQ49_spl
<=> ~ stemilion(X50) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f4701,plain,
! [X0] :
( ~ sQ49_spl
| ~ stemilion(X0) ),
inference(component_clause,[status(thm)],[f4700]) ).
fof(f4703,definition,
! [X51] :
( sQ50_spl
<=> ~ sweetriesling(X51) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f4704,plain,
! [X0] :
( ~ sQ50_spl
| ~ sweetriesling(X0) ),
inference(component_clause,[status(thm)],[f4703]) ).
fof(f4706,definition,
! [X52] :
( sQ51_spl
<=> ~ sweetwine(X52) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f4707,plain,
! [X0] :
( ~ sQ51_spl
| ~ sweetwine(X0) ),
inference(component_clause,[status(thm)],[f4706]) ).
fof(f4709,definition,
! [X53] :
( sQ52_spl
<=> ~ tablewine(X53) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f4710,plain,
! [X0] :
( ~ sQ52_spl
| ~ tablewine(X0) ),
inference(component_clause,[status(thm)],[f4709]) ).
fof(f4712,definition,
! [X54] :
( sQ53_spl
<=> ~ texaswine(X54) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f4713,plain,
! [X0] :
( ~ sQ53_spl
| ~ texaswine(X0) ),
inference(component_clause,[status(thm)],[f4712]) ).
fof(f4715,definition,
! [X55] :
( sQ54_spl
<=> ~ vintage(X55) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f4716,plain,
! [X0] :
( ~ sQ54_spl
| ~ vintage(X0) ),
inference(component_clause,[status(thm)],[f4715]) ).
fof(f4718,definition,
! [X56] :
( sQ55_spl
<=> ~ vintageyear(X56) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f4719,plain,
! [X0] :
( ~ sQ55_spl
| ~ vintageyear(X0) ),
inference(component_clause,[status(thm)],[f4718]) ).
fof(f4721,definition,
! [X57] :
( sQ56_spl
<=> ~ whitebordeaux(X57) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f4722,plain,
! [X0] :
( ~ sQ56_spl
| ~ whitebordeaux(X0) ),
inference(component_clause,[status(thm)],[f4721]) ).
fof(f4724,definition,
! [X58] :
( sQ57_spl
<=> ~ whiteburgundy(X58) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f4725,plain,
! [X0] :
( ~ sQ57_spl
| ~ whiteburgundy(X0) ),
inference(component_clause,[status(thm)],[f4724]) ).
fof(f4727,definition,
! [X59] :
( sQ58_spl
<=> ~ whiteloire(X59) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f4728,plain,
! [X0] :
( ~ sQ58_spl
| ~ whiteloire(X0) ),
inference(component_clause,[status(thm)],[f4727]) ).
fof(f4730,definition,
! [X60] :
( sQ59_spl
<=> ~ whitenonsweetwine(X60) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f4731,plain,
! [X0] :
( ~ sQ59_spl
| ~ whitenonsweetwine(X0) ),
inference(component_clause,[status(thm)],[f4730]) ).
fof(f4733,definition,
! [X61] :
( sQ60_spl
<=> ~ whitetablewine(X61) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f4734,plain,
! [X0] :
( ~ sQ60_spl
| ~ whitetablewine(X0) ),
inference(component_clause,[status(thm)],[f4733]) ).
fof(f4736,definition,
! [X62] :
( sQ61_spl
<=> ~ whitewine(X62) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f4737,plain,
! [X0] :
( ~ sQ61_spl
| ~ whitewine(X0) ),
inference(component_clause,[status(thm)],[f4736]) ).
fof(f4739,definition,
! [X63] :
( sQ62_spl
<=> ~ wine(X63) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f4740,plain,
! [X0] :
( ~ sQ62_spl
| ~ wine(X0) ),
inference(component_clause,[status(thm)],[f4739]) ).
fof(f4742,definition,
! [X64] :
( sQ63_spl
<=> ~ winebody(X64) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f4743,plain,
! [X0] :
( ~ sQ63_spl
| ~ winebody(X0) ),
inference(component_clause,[status(thm)],[f4742]) ).
fof(f4745,definition,
! [X65] :
( sQ64_spl
<=> ~ winecolor(X65) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f4746,plain,
! [X0] :
( ~ sQ64_spl
| ~ winecolor(X0) ),
inference(component_clause,[status(thm)],[f4745]) ).
fof(f4748,definition,
! [X66] :
( sQ65_spl
<=> ~ winedescriptor(X66) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f4749,plain,
! [X0] :
( ~ sQ65_spl
| ~ winedescriptor(X0) ),
inference(component_clause,[status(thm)],[f4748]) ).
fof(f4751,definition,
! [X67] :
( sQ66_spl
<=> ~ wineflavor(X67) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f4752,plain,
! [X0] :
( ~ sQ66_spl
| ~ wineflavor(X0) ),
inference(component_clause,[status(thm)],[f4751]) ).
fof(f4754,definition,
! [X68] :
( sQ67_spl
<=> ~ winegrape(X68) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f4755,plain,
! [X0] :
( ~ sQ67_spl
| ~ winegrape(X0) ),
inference(component_clause,[status(thm)],[f4754]) ).
fof(f4757,definition,
! [X69] :
( sQ68_spl
<=> ~ winesugar(X69) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f4758,plain,
! [X0] :
( ~ sQ68_spl
| ~ winesugar(X0) ),
inference(component_clause,[status(thm)],[f4757]) ).
fof(f4760,definition,
! [X70] :
( sQ69_spl
<=> ~ winery(X70) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f4761,plain,
! [X0] :
( ~ sQ69_spl
| ~ winery(X0) ),
inference(component_clause,[status(thm)],[f4760]) ).
fof(f4763,definition,
! [X71] :
( sQ70_spl
<=> ~ winetaste(X71) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f4764,plain,
! [X0] :
( ~ sQ70_spl
| ~ winetaste(X0) ),
inference(component_clause,[status(thm)],[f4763]) ).
fof(f4766,definition,
! [X72] :
( sQ71_spl
<=> ~ zinfandel(X72) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f4767,plain,
! [X0] :
( ~ sQ71_spl
| ~ zinfandel(X0) ),
inference(component_clause,[status(thm)],[f4766]) ).
fof(f4769,definition,
! [X73,X74] :
( sQ72_spl
<=> ~ hasbody(X73,X74) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f4770,plain,
! [X0,X1] :
( ~ sQ72_spl
| ~ hasbody(X0,X1) ),
inference(component_clause,[status(thm)],[f4769]) ).
fof(f4772,definition,
! [X75,X76] :
( sQ73_spl
<=> ~ hascolor(X75,X76) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f4773,plain,
! [X0,X1] :
( ~ sQ73_spl
| ~ hascolor(X0,X1) ),
inference(component_clause,[status(thm)],[f4772]) ).
fof(f4775,definition,
! [X77,X78] :
( sQ74_spl
<=> ~ hasflavor(X77,X78) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f4776,plain,
! [X0,X1] :
( ~ sQ74_spl
| ~ hasflavor(X0,X1) ),
inference(component_clause,[status(thm)],[f4775]) ).
fof(f4778,definition,
! [X79,X80] :
( sQ75_spl
<=> ~ hasmaker(X79,X80) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f4779,plain,
! [X0,X1] :
( ~ sQ75_spl
| ~ hasmaker(X0,X1) ),
inference(component_clause,[status(thm)],[f4778]) ).
fof(f4781,definition,
! [X81,X82] :
( sQ76_spl
<=> ~ hassugar(X81,X82) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f4782,plain,
! [X0,X1] :
( ~ sQ76_spl
| ~ hassugar(X0,X1) ),
inference(component_clause,[status(thm)],[f4781]) ).
fof(f4784,definition,
! [X83,X84] :
( sQ77_spl
<=> ~ hasvintageyear(X83,X84) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f4785,plain,
! [X0,X1] :
( ~ sQ77_spl
| ~ hasvintageyear(X0,X1) ),
inference(component_clause,[status(thm)],[f4784]) ).
fof(f4787,definition,
! [X85,X86] :
( sQ78_spl
<=> ~ haswinedescriptor(X85,X86) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f4788,plain,
! [X0,X1] :
( ~ sQ78_spl
| ~ haswinedescriptor(X0,X1) ),
inference(component_clause,[status(thm)],[f4787]) ).
fof(f4790,definition,
! [X87,X88] :
( sQ79_spl
<=> ~ locatedin(X87,X88) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f4791,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ locatedin(X0,X1) ),
inference(component_clause,[status(thm)],[f4790]) ).
fof(f4793,definition,
! [X89,X90] :
( sQ80_spl
<=> ~ madefromgrape(X89,X90) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f4794,plain,
! [X0,X1] :
( ~ sQ80_spl
| ~ madefromgrape(X0,X1) ),
inference(component_clause,[status(thm)],[f4793]) ).
fof(f4796,definition,
! [X91,X92] :
( sQ81_spl
<=> ~ madefromfruit(X91,X92) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f4797,plain,
! [X0,X1] :
( ~ sQ81_spl
| ~ madefromfruit(X0,X1) ),
inference(component_clause,[status(thm)],[f4796]) ).
fof(f4799,definition,
! [X93,X94] :
( sQ82_spl
<=> ~ madeintowine(X93,X94) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f4800,plain,
! [X0,X1] :
( ~ sQ82_spl
| ~ madeintowine(X0,X1) ),
inference(component_clause,[status(thm)],[f4799]) ).
fof(f4802,definition,
! [X95,X96] :
( sQ83_spl
<=> ~ produceswine(X95,X96) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f4803,plain,
! [X0,X1] :
( ~ sQ83_spl
| ~ produceswine(X0,X1) ),
inference(component_clause,[status(thm)],[f4802]) ).
fof(f4805,plain,
( sQ83_spl
| sQ82_spl
| sQ81_spl
| sQ80_spl
| sQ79_spl
| sQ78_spl
| sQ77_spl
| sQ76_spl
| sQ75_spl
| sQ74_spl
| sQ73_spl
| sQ72_spl
| sQ71_spl
| sQ70_spl
| sQ69_spl
| sQ68_spl
| sQ67_spl
| sQ66_spl
| sQ65_spl
| sQ64_spl
| sQ63_spl
| sQ62_spl
| sQ61_spl
| sQ60_spl
| sQ59_spl
| sQ58_spl
| sQ57_spl
| sQ56_spl
| sQ55_spl
| sQ54_spl
| sQ53_spl
| sQ52_spl
| sQ51_spl
| sQ50_spl
| sQ49_spl
| sQ48_spl
| sQ47_spl
| sQ46_spl
| sQ45_spl
| sQ44_spl
| sQ43_spl
| sQ42_spl
| sQ41_spl
| sQ40_spl
| sQ39_spl
| sQ38_spl
| sQ37_spl
| sQ36_spl
| sQ35_spl
| sQ34_spl
| sQ33_spl
| sQ32_spl
| sQ31_spl
| sQ30_spl
| sQ29_spl
| sQ28_spl
| sQ27_spl
| sQ26_spl
| sQ25_spl
| sQ24_spl
| sQ23_spl
| sQ22_spl
| sQ21_spl
| sQ20_spl
| sQ19_spl
| sQ18_spl
| sQ17_spl
| sQ16_spl
| sQ15_spl
| sQ14_spl
| sQ13_spl
| sQ12_spl
| sQ11_spl
| sQ10_spl
| sQ9_spl
| sQ8_spl
| sQ7_spl
| sQ6_spl
| sQ5_spl
| sQ4_spl
| sQ3_spl
| sQ2_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f4552,f4553,f4556,f4559,f4562,f4565,f4568,f4571,f4574,f4577,f4580,f4583,f4586,f4589,f4592,f4595,f4598,f4601,f4604,f4607,f4610,f4613,f4616,f4619,f4622,f4625,f4628,f4631,f4634,f4637,f4640,f4643,f4646,f4649,f4652,f4655,f4658,f4661,f4664,f4667,f4670,f4673,f4676,f4679,f4682,f4685,f4688,f4691,f4694,f4697,f4700,f4703,f4706,f4709,f4712,f4715,f4718,f4721,f4724,f4727,f4730,f4733,f4736,f4739,f4742,f4745,f4748,f4751,f4754,f4757,f4760,f4763,f4766,f4769,f4772,f4775,f4778,f4781,f4784,f4787,f4790,f4793,f4796,f4799,f4802]) ).
fof(f4806,plain,
ot____nom1(sweet),
inference(resolution,[status(thm)],[f2289,f1861]) ).
fof(f4807,plain,
ot____nom10(texasregion),
inference(resolution,[status(thm)],[f2291,f1862]) ).
fof(f4809,plain,
madefromgrape(chateaudychemsauterne,sauvignonblancgrape),
inference(resolution,[status(thm)],[f2271,f1860]) ).
fof(f4810,plain,
madefromgrape(chateaudychemsauterne,semillongrape),
inference(resolution,[status(thm)],[f2271,f1859]) ).
fof(f4811,plain,
ot____nom12(dry),
inference(resolution,[status(thm)],[f2295,f1864]) ).
fof(f4820,plain,
locatedin(schlossvolradtrochenbierenausleseriesling,germanyregion),
inference(resolution,[status(thm)],[f2273,f1851]) ).
fof(f4823,plain,
locatedin(ventanacheninblanc,centralcoastregion),
inference(resolution,[status(thm)],[f2273,f1848]) ).
fof(f4835,plain,
locatedin(texasregion,usregion),
inference(resolution,[status(thm)],[f2273,f1836]) ).
fof(f4852,plain,
locatedin(centralcoastregion,californiaregion),
inference(resolution,[status(thm)],[f2273,f1819]) ).
fof(f4858,plain,
locatedin(centraltexasregion,texasregion),
inference(resolution,[status(thm)],[f2273,f1813]) ).
fof(f4874,plain,
locatedin(stgenevievetexaswhite,centraltexasregion),
inference(resolution,[status(thm)],[f2273,f1797]) ).
fof(f4877,plain,
locatedin(californiaregion,usregion),
inference(resolution,[status(thm)],[f2273,f1794]) ).
fof(f4879,plain,
ot____nom15(californiaregion),
inference(resolution,[status(thm)],[f2301,f1867]) ).
fof(f4881,plain,
ot____nom17(germanyregion),
inference(resolution,[status(thm)],[f2305,f1869]) ).
fof(f4889,plain,
hascolor(selaksicewine,white),
inference(resolution,[status(thm)],[f2281,f1658]) ).
fof(f4898,plain,
hasvintageyear(saucelitocanyonzinfandel1998,year1998),
inference(resolution,[status(thm)],[f2287,f2269]) ).
fof(f4910,plain,
ot____nom38(usregion),
inference(resolution,[status(thm)],[f2351,f1896]) ).
fof(f4957,plain,
zinfandel(elysezinfandel),
inference(resolution,[status(thm)],[f2417,f2012]) ).
fof(f4960,plain,
winesugar(sweet),
inference(resolution,[status(thm)],[f2423,f1966]) ).
fof(f4963,plain,
wineflavor(delicate),
inference(resolution,[status(thm)],[f2425,f1947]) ).
fof(f4964,plain,
anjou(rosedanjou),
inference(resolution,[status(thm)],[f2427,f2039]) ).
fof(f4965,plain,
beaujolais(chateaumorgonbeaujolais),
inference(resolution,[status(thm)],[f2429,f2038]) ).
fof(f4966,plain,
cabernetfranc(whitehalllanecabernetfranc),
inference(resolution,[status(thm)],[f2431,f2037]) ).
fof(f4967,plain,
cabernetsauvignon(formancabernetsauvignon),
inference(resolution,[status(thm)],[f2433,f2036]) ).
fof(f4976,plain,
cheninblanc(ventanacheninblanc),
inference(resolution,[status(thm)],[f2437,f2046]) ).
fof(f4977,plain,
cheninblanc(foxencheninblanc),
inference(resolution,[status(thm)],[f2437,f2045]) ).
fof(f4978,plain,
chianti(chianticlassico),
inference(resolution,[status(thm)],[f2439,f2047]) ).
fof(f4979,plain,
cotesdor(closdevougeotcotesdor),
inference(resolution,[status(thm)],[f2441,f2048]) ).
fof(f4980,plain,
dessertwine(whitehalllaneprimavera),
inference(resolution,[status(thm)],[f2443,f2032]) ).
fof(f4981,plain,
dryriesling(mountadamriesling),
inference(resolution,[status(thm)],[f2445,f2031]) ).
fof(f4982,plain,
icewine(selaksicewine),
inference(resolution,[status(thm)],[f2447,f2030]) ).
fof(f4983,plain,
margaux(chateaumargaux),
inference(resolution,[status(thm)],[f2449,f2029]) ).
fof(f4984,plain,
meritage(kathrynkennedylateral),
inference(resolution,[status(thm)],[f2451,f2028]) ).
fof(f4987,plain,
meursault(chateaudemeursaultmeursault),
inference(resolution,[status(thm)],[f2455,f2027]) ).
fof(f4988,plain,
muscadet(sevreetmainemuscadet),
inference(resolution,[status(thm)],[f2457,f2026]) ).
fof(f4989,plain,
pauillac(chateaulafiterothschildpauillac),
inference(resolution,[status(thm)],[f2459,f2051]) ).
fof(f4991,plain,
petitesyrah(mariettapetitesyrah),
inference(resolution,[status(thm)],[f2461,f2052]) ).
fof(f4995,plain,
port(taylorport),
inference(resolution,[status(thm)],[f2465,f2057]) ).
fof(f4996,plain,
redtablewine(mariettaoldvinesred),
inference(resolution,[status(thm)],[f2467,f2058]) ).
fof(f4998,plain,
sancerre(closdelapoussiesancerre),
inference(resolution,[status(thm)],[f2473,f2096]) ).
fof(f4999,plain,
sauternes(chateaudychemsauterne),
inference(resolution,[status(thm)],[f2475,f2097]) ).
fof(f5000,plain,
sauvignonblanc(selakssauvignonblanc),
inference(resolution,[status(thm)],[f2477,f2101]) ).
fof(f5003,plain,
sauvignonblanc(corbansprivatebinsauvignonblanc),
inference(resolution,[status(thm)],[f2477,f2098]) ).
fof(f5005,plain,
semillon(congressspringssemillon),
inference(resolution,[status(thm)],[f2479,f2102]) ).
fof(f5006,plain,
stemilion(chateauchevalblancstemilion),
inference(resolution,[status(thm)],[f2481,f2104]) ).
fof(f5007,plain,
sweetriesling(schlossvolradtrochenbierenausleseriesling),
inference(resolution,[status(thm)],[f2483,f2106]) ).
fof(f5008,plain,
sweetriesling(schlossrothermeltrochenbierenausleseriesling),
inference(resolution,[status(thm)],[f2483,f2105]) ).
fof(f5009,plain,
vintageyear(year1998),
inference(resolution,[status(thm)],[f2485,f2268]) ).
fof(f5010,plain,
whiteburgundy(cortonmontrachetwhiteburgundy),
inference(resolution,[status(thm)],[f2487,f2024]) ).
fof(f5011,plain,
whiteburgundy(pulignymontrachetwhiteburgundy),
inference(resolution,[status(thm)],[f2487,f2023]) ).
fof(f5012,plain,
whitewine(stgenevievetexaswhite),
inference(resolution,[status(thm)],[f2489,f2025]) ).
fof(f5013,plain,
winebody(medium),
inference(resolution,[status(thm)],[f2491,f2019]) ).
fof(f5015,plain,
winebody(light),
inference(resolution,[status(thm)],[f2491,f2017]) ).
fof(f5035,plain,
q0(formancabernetsauvignon),
inference(resolution,[status(thm)],[f2509,f4967]) ).
fof(f5042,plain,
q12(foxencheninblanc),
inference(resolution,[status(thm)],[f2553,f4977]) ).
fof(f5043,plain,
q12(ventanacheninblanc),
inference(resolution,[status(thm)],[f2553,f4976]) ).
fof(f5051,plain,
q12(chateaudychemsauterne),
inference(resolution,[status(thm)],[f2563,f4999]) ).
fof(f5055,plain,
q20(chateaumargaux),
inference(resolution,[status(thm)],[f2643,f4983]) ).
fof(f5109,plain,
q31(formancabernetsauvignon),
inference(resolution,[status(thm)],[f2762,f4967]) ).
fof(f5123,plain,
! [X0,X1] :
( ~ q26(X1)
| q26(X0)
| ~ locatedin(X0,X1) ),
inference(resolution,[status(thm)],[f2682,f2687]) ).
fof(f5127,plain,
! [X0] :
( q27(X0)
| ~ locatedin(X0,usregion) ),
inference(resolution,[status(thm)],[f2690,f4910]) ).
fof(f5130,plain,
q35(chateaudemeursaultmeursault),
inference(resolution,[status(thm)],[f2818,f4987]) ).
fof(f5133,plain,
q4(closdevougeotcotesdor),
inference(resolution,[status(thm)],[f2864,f4979]) ).
fof(f5157,plain,
bordeaux(chateaudychemsauterne),
inference(resolution,[status(thm)],[f3238,f4999]) ).
fof(f5163,plain,
! [X0] :
( ~ pauillac(X0)
| cabernetsauvignon(X0) ),
inference(resolution,[status(thm)],[f3268,f3150]) ).
fof(f5164,plain,
! [X0] :
( ~ whiteburgundy(X0)
| chardonnay(X0) ),
inference(resolution,[status(thm)],[f3281,f3106]) ).
fof(f5177,plain,
loire(sevreetmainemuscadet),
inference(resolution,[status(thm)],[f3397,f4988]) ).
fof(f5182,plain,
medoc(chateaumargaux),
inference(resolution,[status(thm)],[f3411,f4983]) ).
fof(f5183,plain,
bordeaux(chateaumargaux),
inference(resolution,[status(thm)],[f5182,f3240]) ).
fof(f5185,plain,
q0(chateaumargaux),
inference(resolution,[status(thm)],[f5182,f2507]) ).
fof(f5189,plain,
! [X0] :
( ~ margaux(X0)
| merlot(X0) ),
inference(resolution,[status(thm)],[f3423,f2572]) ).
fof(f5191,plain,
! [X0] :
( ~ muscadet(X0)
| pinotblanc(X0) ),
inference(resolution,[status(thm)],[f3452,f2674]) ).
fof(f5193,plain,
! [X0] :
( ~ redburgundy(X0)
| pinotnoir(X0) ),
inference(resolution,[status(thm)],[f3460,f3189]) ).
fof(f5196,plain,
redburgundy(closdevougeotcotesdor),
inference(resolution,[status(thm)],[f3481,f4979]) ).
fof(f5203,plain,
redwine(taylorport),
inference(resolution,[status(thm)],[f3499,f4995]) ).
fof(f5210,plain,
riesling(schlossvolradtrochenbierenausleseriesling),
inference(resolution,[status(thm)],[f3522,f5007]) ).
fof(f5214,plain,
q12(schlossvolradtrochenbierenausleseriesling),
inference(resolution,[status(thm)],[f5210,f2567]) ).
fof(f5217,plain,
semillonorsauvignonblanc(congressspringssemillon),
inference(resolution,[status(thm)],[f3560,f5005]) ).
fof(f5222,plain,
semillonorsauvignonblanc(selakssauvignonblanc),
inference(resolution,[status(thm)],[f3562,f5000]) ).
fof(f5226,plain,
whiteburgundy(chateaudemeursaultmeursault),
inference(resolution,[status(thm)],[f3622,f4987]) ).
fof(f5229,plain,
whitewine(pulignymontrachetwhiteburgundy),
inference(resolution,[status(thm)],[f3650,f5011]) ).
fof(f5231,plain,
! [X0] :
( q46(X0)
| ~ hassugar(X0,dry) ),
inference(resolution,[status(thm)],[f2920,f4811]) ).
fof(f5236,plain,
wine(chateaumargaux),
inference(resolution,[status(thm)],[f3669,f5055]) ).
fof(f5262,plain,
wine(formancabernetsauvignon),
inference(resolution,[status(thm)],[f3676,f5109]) ).
fof(f5268,plain,
! [X0] :
( q48(X0)
| ~ locatedin(X0,californiaregion) ),
inference(resolution,[status(thm)],[f2936,f4879]) ).
fof(f5309,plain,
wine(selakssauvignonblanc),
inference(resolution,[status(thm)],[f3697,f5222]) ).
fof(f5324,plain,
wine(schlossvolradtrochenbierenausleseriesling),
inference(resolution,[status(thm)],[f3707,f5214]) ).
fof(f5334,plain,
wine(ventanacheninblanc),
inference(resolution,[status(thm)],[f3707,f5043]) ).
fof(f5385,plain,
wine(pulignymontrachetwhiteburgundy),
inference(resolution,[status(thm)],[f3740,f5229]) ).
fof(f5387,plain,
wine(stgenevievetexaswhite),
inference(resolution,[status(thm)],[f3740,f5012]) ).
fof(f5389,plain,
wine(whitehalllaneprimavera),
inference(resolution,[status(thm)],[f3742,f4980]) ).
fof(f5454,plain,
! [X0] :
( q50(X0)
| ~ locatedin(X0,germanyregion) ),
inference(resolution,[status(thm)],[f3012,f4881]) ).
fof(f5463,plain,
! [X0] :
( winedescriptor(X0)
| ~ winebody(X0) ),
inference(resolution,[status(thm)],[f3837,f3803]) ).
fof(f5567,plain,
chardonnay(pulignymontrachetwhiteburgundy),
inference(resolution,[status(thm)],[f5164,f5011]) ).
fof(f5568,plain,
chardonnay(cortonmontrachetwhiteburgundy),
inference(resolution,[status(thm)],[f5164,f5010]) ).
fof(f5576,plain,
q12(pulignymontrachetwhiteburgundy),
inference(resolution,[status(thm)],[f5567,f2555]) ).
fof(f5592,plain,
merlot(chateaumargaux),
inference(resolution,[status(thm)],[f5189,f4983]) ).
fof(f5601,plain,
! [X0] :
( q12(X0)
| ~ muscadet(X0) ),
inference(resolution,[status(thm)],[f5191,f2557]) ).
fof(f5612,plain,
! [X0] :
( q71(X0)
| ~ hassugar(X0,sweet) ),
inference(resolution,[status(thm)],[f3182,f4806]) ).
fof(f5638,plain,
! [X0] :
( q74(X0)
| ~ locatedin(X0,texasregion) ),
inference(resolution,[status(thm)],[f3205,f4807]) ).
fof(f5649,plain,
! [X0] :
( winecolor(X0)
| ~ winebody(X0) ),
inference(resolution,[status(thm)],[f5463,f3796]) ).
fof(f5652,plain,
q12(sevreetmainemuscadet),
inference(resolution,[status(thm)],[f5601,f4988]) ).
fof(f5663,plain,
! [X0] :
( ~ q26(X0)
| americanwine(X0)
| ~ wine(X0) ),
inference(resolution,[status(thm)],[f3223,f2687]) ).
fof(f5666,plain,
winecolor(medium),
inference(resolution,[status(thm)],[f5649,f5013]) ).
fof(f5939,plain,
! [X0,X1] :
( ~ sQ83_spl
| ~ hasmaker_aux(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f2277,f5940]) ).
fof(f5940,plain,
! [X0,X1] :
( ~ sQ83_spl
| ~ hasmaker(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f4446,f4803]) ).
fof(f5941,plain,
( ~ sQ83_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1753,f5939]) ).
fof(f5993,plain,
~ sQ83_spl,
inference(contradiction_clause,[status(thm)],[f5941]) ).
fof(f5996,plain,
! [X0,X1] :
( ~ sQ82_spl
| ~ madefromgrape(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f4438,f4800]) ).
fof(f5998,plain,
( ~ sQ82_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4810,f5996]) ).
fof(f6000,plain,
~ sQ82_spl,
inference(contradiction_clause,[status(thm)],[f5998]) ).
fof(f6121,definition,
( sQ90_spl
<=> dessertwine(selaksicewine) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f6122,plain,
( ~ sQ90_spl
| dessertwine(selaksicewine) ),
inference(component_clause,[status(thm)],[f6121]) ).
fof(f6123,plain,
( sQ90_spl
| ~ dessertwine(selaksicewine) ),
inference(component_clause,[status(thm)],[f6121]) ).
fof(f6124,definition,
( sQ91_spl
<=> lateharvest(selaksicewine) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f6125,plain,
( ~ sQ91_spl
| lateharvest(selaksicewine) ),
inference(component_clause,[status(thm)],[f6124]) ).
fof(f6126,plain,
( sQ91_spl
| ~ lateharvest(selaksicewine) ),
inference(component_clause,[status(thm)],[f6124]) ).
fof(f6133,plain,
( sQ91_spl
| ~ icewine(selaksicewine) ),
inference(resolution,[status(thm)],[f6126,f3382]) ).
fof(f6134,plain,
( sQ91_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6133,f4982]) ).
fof(f6135,plain,
sQ91_spl,
inference(contradiction_clause,[status(thm)],[f6134]) ).
fof(f6139,plain,
( sQ90_spl
| ~ icewine(selaksicewine) ),
inference(resolution,[status(thm)],[f6123,f3307]) ).
fof(f6141,plain,
( sQ90_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6139,f4982]) ).
fof(f6142,plain,
sQ90_spl,
inference(contradiction_clause,[status(thm)],[f6141]) ).
fof(f6170,plain,
q27(texasregion),
inference(resolution,[status(thm)],[f5127,f4835]) ).
fof(f6185,plain,
! [X0] :
( q26(X0)
| ~ locatedin(X0,texasregion) ),
inference(resolution,[status(thm)],[f6170,f2682]) ).
fof(f6308,plain,
! [X0] :
( ~ q0(X0)
| redwine(X0)
| ~ wine(X0) ),
inference(resolution,[status(thm)],[f3501,f2877]) ).
fof(f6309,plain,
! [X0] :
( ~ q0(X0)
| redwine(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f6308,f3690]) ).
fof(f6372,plain,
! [X0] :
( ~ hassugar_aux(X0,dry)
| q46(X0) ),
inference(resolution,[status(thm)],[f5231,f2275]) ).
fof(f6376,plain,
q48(centralcoastregion),
inference(resolution,[status(thm)],[f5268,f4852]) ).
fof(f6393,plain,
! [X0] :
( q47(X0)
| ~ locatedin(X0,centralcoastregion) ),
inference(resolution,[status(thm)],[f6376,f2928]) ).
fof(f6761,plain,
q50(schlossvolradtrochenbierenausleseriesling),
inference(resolution,[status(thm)],[f5454,f4820]) ).
fof(f6773,plain,
( germanwine(schlossvolradtrochenbierenausleseriesling)
| ~ wine(schlossvolradtrochenbierenausleseriesling) ),
inference(resolution,[status(thm)],[f6761,f3360]) ).
fof(f6775,definition,
( sQ131_spl
<=> wine(schlossvolradtrochenbierenausleseriesling) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f6777,plain,
( sQ131_spl
| ~ wine(schlossvolradtrochenbierenausleseriesling) ),
inference(component_clause,[status(thm)],[f6775]) ).
fof(f6778,definition,
( sQ132_spl
<=> germanwine(schlossvolradtrochenbierenausleseriesling) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f6779,plain,
( ~ sQ132_spl
| germanwine(schlossvolradtrochenbierenausleseriesling) ),
inference(component_clause,[status(thm)],[f6778]) ).
fof(f6781,plain,
( sQ132_spl
| ~ sQ131_spl ),
inference(split_clause,[status(thm)],[f6773,f6775,f6778]) ).
fof(f6782,plain,
( sQ131_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6777,f5324]) ).
fof(f6783,plain,
sQ131_spl,
inference(contradiction_clause,[status(thm)],[f6782]) ).
fof(f6798,plain,
! [X0] :
( ~ q12(X0)
| whitewine(X0)
| ~ wine(X0) ),
inference(resolution,[status(thm)],[f3658,f2648]) ).
fof(f6806,plain,
! [X0] :
( ~ q12(X0)
| whitewine(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f6798,f3707]) ).
fof(f6817,plain,
whitewine(sevreetmainemuscadet),
inference(resolution,[status(thm)],[f6806,f5652]) ).
fof(f6824,plain,
whitewine(chateaudychemsauterne),
inference(resolution,[status(thm)],[f6806,f5051]) ).
fof(f6832,plain,
whitewine(foxencheninblanc),
inference(resolution,[status(thm)],[f6806,f5042]) ).
fof(f6835,plain,
! [X0] :
( ~ semillonorsauvignonblanc(X0)
| whitewine(X0) ),
inference(resolution,[status(thm)],[f6806,f2565]) ).
fof(f6868,plain,
whitewine(selakssauvignonblanc),
inference(resolution,[status(thm)],[f6835,f5222]) ).
fof(f6873,plain,
whitewine(congressspringssemillon),
inference(resolution,[status(thm)],[f6835,f5217]) ).
fof(f7032,plain,
! [X0] :
( ~ hassugar_aux(X0,sweet)
| q71(X0) ),
inference(resolution,[status(thm)],[f5612,f2275]) ).
fof(f7033,plain,
q74(centraltexasregion),
inference(resolution,[status(thm)],[f5638,f4858]) ).
fof(f7036,plain,
! [X0] :
( q73(X0)
| ~ locatedin(X0,centraltexasregion) ),
inference(resolution,[status(thm)],[f7033,f3197]) ).
fof(f7072,plain,
( ~ sQ81_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4809,f7074]) ).
fof(f7074,plain,
! [X0,X1] :
( ~ sQ81_spl
| ~ madefromgrape(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f4388,f4797]) ).
fof(f7075,plain,
~ sQ81_spl,
inference(contradiction_clause,[status(thm)],[f7072]) ).
fof(f7095,plain,
( ~ sQ80_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4809,f4794]) ).
fof(f7096,plain,
~ sQ80_spl,
inference(contradiction_clause,[status(thm)],[f7095]) ).
fof(f7098,plain,
( ~ sQ79_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4877,f4791]) ).
fof(f7163,plain,
~ sQ79_spl,
inference(contradiction_clause,[status(thm)],[f7098]) ).
fof(f7166,plain,
! [X0,X1] :
( ~ sQ78_spl
| ~ hascolor(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f4314,f4788]) ).
fof(f7171,plain,
( ~ sQ78_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4889,f7166]) ).
fof(f7172,plain,
~ sQ78_spl,
inference(contradiction_clause,[status(thm)],[f7171]) ).
fof(f7174,plain,
( ~ sQ77_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4898,f4785]) ).
fof(f7175,plain,
~ sQ77_spl,
inference(contradiction_clause,[status(thm)],[f7174]) ).
fof(f7265,plain,
q26(centraltexasregion),
inference(resolution,[status(thm)],[f6185,f4858]) ).
fof(f7272,plain,
q46(selakssauvignonblanc),
inference(resolution,[status(thm)],[f6372,f1793]) ).
fof(f7275,plain,
q46(formancabernetsauvignon),
inference(resolution,[status(thm)],[f6372,f1789]) ).
fof(f7306,plain,
q46(pulignymontrachetwhiteburgundy),
inference(resolution,[status(thm)],[f6372,f1754]) ).
fof(f7308,plain,
( drywine(selakssauvignonblanc)
| ~ wine(selakssauvignonblanc) ),
inference(resolution,[status(thm)],[f7272,f3331]) ).
fof(f7310,definition,
( sQ147_spl
<=> wine(selakssauvignonblanc) ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f7312,plain,
( sQ147_spl
| ~ wine(selakssauvignonblanc) ),
inference(component_clause,[status(thm)],[f7310]) ).
fof(f7317,definition,
( sQ149_spl
<=> drywine(selakssauvignonblanc) ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f7318,plain,
( ~ sQ149_spl
| drywine(selakssauvignonblanc) ),
inference(component_clause,[status(thm)],[f7317]) ).
fof(f7320,plain,
( sQ149_spl
| ~ sQ147_spl ),
inference(split_clause,[status(thm)],[f7308,f7310,f7317]) ).
fof(f7328,plain,
( sQ147_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7312,f5309]) ).
fof(f7329,plain,
sQ147_spl,
inference(contradiction_clause,[status(thm)],[f7328]) ).
fof(f7377,plain,
( drywine(formancabernetsauvignon)
| ~ wine(formancabernetsauvignon) ),
inference(resolution,[status(thm)],[f7275,f3331]) ).
fof(f7379,definition,
( sQ162_spl
<=> wine(formancabernetsauvignon) ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f7381,plain,
( sQ162_spl
| ~ wine(formancabernetsauvignon) ),
inference(component_clause,[status(thm)],[f7379]) ).
fof(f7386,definition,
( sQ164_spl
<=> drywine(formancabernetsauvignon) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f7387,plain,
( ~ sQ164_spl
| drywine(formancabernetsauvignon) ),
inference(component_clause,[status(thm)],[f7386]) ).
fof(f7389,plain,
( sQ164_spl
| ~ sQ162_spl ),
inference(split_clause,[status(thm)],[f7377,f7379,f7386]) ).
fof(f7397,plain,
( sQ162_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7381,f5262]) ).
fof(f7398,plain,
sQ162_spl,
inference(contradiction_clause,[status(thm)],[f7397]) ).
fof(f8050,definition,
( sQ307_spl
<=> wine(stgenevievetexaswhite) ),
introduced(definition,[new_symbols(definition,[sQ307_spl])],[split_symbol_definition]) ).
fof(f8052,plain,
( sQ307_spl
| ~ wine(stgenevievetexaswhite) ),
inference(component_clause,[status(thm)],[f8050]) ).
fof(f8068,plain,
( sQ307_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8052,f5387]) ).
fof(f8069,plain,
sQ307_spl,
inference(contradiction_clause,[status(thm)],[f8068]) ).
fof(f8093,plain,
( tablewine(pulignymontrachetwhiteburgundy)
| ~ wine(pulignymontrachetwhiteburgundy) ),
inference(resolution,[status(thm)],[f7306,f3590]) ).
fof(f8094,plain,
( drywine(pulignymontrachetwhiteburgundy)
| ~ wine(pulignymontrachetwhiteburgundy) ),
inference(resolution,[status(thm)],[f7306,f3331]) ).
fof(f8096,definition,
( sQ317_spl
<=> wine(pulignymontrachetwhiteburgundy) ),
introduced(definition,[new_symbols(definition,[sQ317_spl])],[split_symbol_definition]) ).
fof(f8098,plain,
( sQ317_spl
| ~ wine(pulignymontrachetwhiteburgundy) ),
inference(component_clause,[status(thm)],[f8096]) ).
fof(f8099,definition,
( sQ318_spl
<=> tablewine(pulignymontrachetwhiteburgundy) ),
introduced(definition,[new_symbols(definition,[sQ318_spl])],[split_symbol_definition]) ).
fof(f8100,plain,
( ~ sQ318_spl
| tablewine(pulignymontrachetwhiteburgundy) ),
inference(component_clause,[status(thm)],[f8099]) ).
fof(f8102,plain,
( sQ318_spl
| ~ sQ317_spl ),
inference(split_clause,[status(thm)],[f8093,f8096,f8099]) ).
fof(f8103,definition,
( sQ319_spl
<=> drywine(pulignymontrachetwhiteburgundy) ),
introduced(definition,[new_symbols(definition,[sQ319_spl])],[split_symbol_definition]) ).
fof(f8104,plain,
( ~ sQ319_spl
| drywine(pulignymontrachetwhiteburgundy) ),
inference(component_clause,[status(thm)],[f8103]) ).
fof(f8106,plain,
( sQ319_spl
| ~ sQ317_spl ),
inference(split_clause,[status(thm)],[f8094,f8096,f8103]) ).
fof(f8114,plain,
( sQ317_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8098,f5385]) ).
fof(f8115,plain,
sQ317_spl,
inference(contradiction_clause,[status(thm)],[f8114]) ).
fof(f8601,plain,
q47(ventanacheninblanc),
inference(resolution,[status(thm)],[f6393,f4823]) ).
fof(f8663,plain,
( hasbody(whitehalllaneprimavera,whitehalllaneprimavera)
| ~ kaon2namedobjects(whitehalllaneprimavera) ),
inference(resolution,[status(thm)],[f4238,f5389]) ).
fof(f8720,definition,
( sQ322_spl
<=> kaon2namedobjects(whitehalllaneprimavera) ),
introduced(definition,[new_symbols(definition,[sQ322_spl])],[split_symbol_definition]) ).
fof(f8722,plain,
( sQ322_spl
| ~ kaon2namedobjects(whitehalllaneprimavera) ),
inference(component_clause,[status(thm)],[f8720]) ).
fof(f8723,definition,
( sQ323_spl
<=> hasbody(whitehalllaneprimavera,whitehalllaneprimavera) ),
introduced(definition,[new_symbols(definition,[sQ323_spl])],[split_symbol_definition]) ).
fof(f8724,plain,
( ~ sQ323_spl
| hasbody(whitehalllaneprimavera,whitehalllaneprimavera) ),
inference(component_clause,[status(thm)],[f8723]) ).
fof(f8726,plain,
( sQ323_spl
| ~ sQ322_spl ),
inference(split_clause,[status(thm)],[f8663,f8720,f8723]) ).
fof(f9063,definition,
( sQ420_spl
<=> kaon2namedobjects(closdevougeotcotesdor) ),
introduced(definition,[new_symbols(definition,[sQ420_spl])],[split_symbol_definition]) ).
fof(f9065,plain,
( sQ420_spl
| ~ kaon2namedobjects(closdevougeotcotesdor) ),
inference(component_clause,[status(thm)],[f9063]) ).
fof(f9084,definition,
( sQ426_spl
<=> kaon2namedobjects(chateaumargaux) ),
introduced(definition,[new_symbols(definition,[sQ426_spl])],[split_symbol_definition]) ).
fof(f9086,plain,
( sQ426_spl
| ~ kaon2namedobjects(chateaumargaux) ),
inference(component_clause,[status(thm)],[f9084]) ).
fof(f9091,plain,
( sQ426_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9086,f2227]) ).
fof(f9092,plain,
sQ426_spl,
inference(contradiction_clause,[status(thm)],[f9091]) ).
fof(f9097,plain,
( sQ420_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9065,f2240]) ).
fof(f9098,plain,
sQ420_spl,
inference(contradiction_clause,[status(thm)],[f9097]) ).
fof(f9195,plain,
( sQ322_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8722,f2130]) ).
fof(f9196,plain,
sQ322_spl,
inference(contradiction_clause,[status(thm)],[f9195]) ).
fof(f9392,plain,
( hascolor(whitehalllaneprimavera,whitehalllaneprimavera)
| ~ kaon2namedobjects(whitehalllaneprimavera) ),
inference(resolution,[status(thm)],[f4254,f5389]) ).
fof(f9449,definition,
( sQ454_spl
<=> hascolor(whitehalllaneprimavera,whitehalllaneprimavera) ),
introduced(definition,[new_symbols(definition,[sQ454_spl])],[split_symbol_definition]) ).
fof(f9450,plain,
( ~ sQ454_spl
| hascolor(whitehalllaneprimavera,whitehalllaneprimavera) ),
inference(component_clause,[status(thm)],[f9449]) ).
fof(f9452,plain,
( sQ454_spl
| ~ sQ322_spl ),
inference(split_clause,[status(thm)],[f9392,f8720,f9449]) ).
fof(f9668,plain,
( hasflavor(closdevougeotcotesdor,closdevougeotcotesdor)
| ~ kaon2namedobjects(closdevougeotcotesdor) ),
inference(resolution,[status(thm)],[f4264,f5133]) ).
fof(f9673,definition,
( sQ481_spl
<=> hasflavor(closdevougeotcotesdor,closdevougeotcotesdor) ),
introduced(definition,[new_symbols(definition,[sQ481_spl])],[split_symbol_definition]) ).
fof(f9674,plain,
( ~ sQ481_spl
| hasflavor(closdevougeotcotesdor,closdevougeotcotesdor) ),
inference(component_clause,[status(thm)],[f9673]) ).
fof(f9676,plain,
( sQ481_spl
| ~ sQ420_spl ),
inference(split_clause,[status(thm)],[f9668,f9063,f9673]) ).
fof(f10271,plain,
! [X0] :
( ~ sQ76_spl
| ~ kaon2namedobjects(X0)
| ~ wine(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4288,f4782]) ).
fof(f10324,plain,
( ~ sQ76_spl
| ~ kaon2namedobjects(chateaumargaux) ),
inference(resolution,[status(thm)],[f10271,f5236]) ).
fof(f10381,plain,
( ~ sQ76_spl
| ~ sQ426_spl ),
inference(split_clause,[status(thm)],[f10324,f9084,f4781]) ).
fof(f10382,plain,
! [X0,X1] :
( ~ sQ75_spl
| ~ produceswine(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f4278,f4779]) ).
fof(f10384,plain,
( ~ sQ75_spl
| sQ83_spl ),
inference(split_clause,[status(thm)],[f10382,f4802,f4778]) ).
fof(f10727,plain,
( ~ sQ481_spl
| ~ sQ74_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9674,f4776]) ).
fof(f10728,plain,
( ~ sQ481_spl
| ~ sQ74_spl ),
inference(contradiction_clause,[status(thm)],[f10727]) ).
fof(f10732,plain,
( ~ sQ454_spl
| ~ sQ73_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f9450,f4773]) ).
fof(f10786,plain,
( ~ sQ454_spl
| ~ sQ73_spl ),
inference(contradiction_clause,[status(thm)],[f10732]) ).
fof(f10792,plain,
( ~ sQ323_spl
| ~ sQ72_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f8724,f4770]) ).
fof(f10846,plain,
( ~ sQ323_spl
| ~ sQ72_spl ),
inference(contradiction_clause,[status(thm)],[f10792]) ).
fof(f10848,plain,
( ~ sQ71_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4957,f4767]) ).
fof(f10853,plain,
~ sQ71_spl,
inference(contradiction_clause,[status(thm)],[f10848]) ).
fof(f10854,plain,
! [X0] :
( ~ sQ70_spl
| ~ winedescriptor(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3839,f4764]) ).
fof(f10858,plain,
! [X0,X1] :
( ~ sQ70_spl
| ~ haswinedescriptor(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f3806,f10854]) ).
fof(f10863,plain,
( ~ sQ70_spl
| sQ78_spl ),
inference(split_clause,[status(thm)],[f10858,f4787,f4763]) ).
fof(f10864,plain,
! [X0] :
( ~ sQ69_spl
| ~ winery_aux(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f2419,f4761]) ).
fof(f10865,plain,
( ~ sQ69_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2011,f10864]) ).
fof(f10908,plain,
~ sQ69_spl,
inference(contradiction_clause,[status(thm)],[f10865]) ).
fof(f10911,plain,
( ~ sQ68_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4960,f4758]) ).
fof(f10914,plain,
~ sQ68_spl,
inference(contradiction_clause,[status(thm)],[f10911]) ).
fof(f10915,plain,
! [X0,X1] :
( ~ sQ67_spl
| ~ madefromgrape(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f3820,f4755]) ).
fof(f10917,plain,
( ~ sQ67_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f10915,f4793,f4754]) ).
fof(f10920,plain,
( ~ sQ66_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4963,f4752]) ).
fof(f10923,plain,
~ sQ66_spl,
inference(contradiction_clause,[status(thm)],[f10920]) ).
fof(f12500,plain,
( ~ sQ65_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5015,f12503]) ).
fof(f12503,plain,
! [X0] :
( ~ sQ65_spl
| ~ winebody(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5463,f4749]) ).
fof(f12504,plain,
~ sQ65_spl,
inference(contradiction_clause,[status(thm)],[f12500]) ).
fof(f12507,plain,
( ~ sQ64_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5666,f4746]) ).
fof(f12520,plain,
~ sQ64_spl,
inference(contradiction_clause,[status(thm)],[f12507]) ).
fof(f12521,plain,
( ~ sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5015,f4743]) ).
fof(f12522,plain,
~ sQ63_spl,
inference(contradiction_clause,[status(thm)],[f12521]) ).
fof(f12595,plain,
( ~ sQ62_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5389,f4740]) ).
fof(f12651,plain,
~ sQ62_spl,
inference(contradiction_clause,[status(thm)],[f12595]) ).
fof(f12660,plain,
( ~ sQ61_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f6873,f4737]) ).
fof(f12684,plain,
~ sQ61_spl,
inference(contradiction_clause,[status(thm)],[f12660]) ).
fof(f12685,plain,
! [X0] :
( ~ sQ60_spl
| ~ tablewine(X0)
| ~ q21(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3643,f4734]) ).
fof(f13725,plain,
! [X0] :
( ~ sQ60_spl
| ~ q12(X0)
| ~ tablewine(X0) ),
inference(resolution,[status(thm)],[f12685,f2648]) ).
fof(f13941,plain,
( ~ sQ318_spl
| ~ sQ60_spl
| ~ q12(pulignymontrachetwhiteburgundy) ),
inference(resolution,[status(thm)],[f13725,f8100]) ).
fof(f13978,plain,
( ~ sQ318_spl
| ~ sQ60_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13941,f5576]) ).
fof(f13979,plain,
( ~ sQ318_spl
| ~ sQ60_spl ),
inference(contradiction_clause,[status(thm)],[f13978]) ).
fof(f14448,plain,
q71(whitehalllaneprimavera),
inference(resolution,[status(thm)],[f7032,f1777]) ).
fof(f14518,plain,
q73(stgenevievetexaswhite),
inference(resolution,[status(thm)],[f7036,f4874]) ).
fof(f15518,plain,
( sweetwine(whitehalllaneprimavera)
| ~ wine(whitehalllaneprimavera) ),
inference(resolution,[status(thm)],[f3581,f14448]) ).
fof(f15526,definition,
( sQ839_spl
<=> wine(whitehalllaneprimavera) ),
introduced(definition,[new_symbols(definition,[sQ839_spl])],[split_symbol_definition]) ).
fof(f15528,plain,
( sQ839_spl
| ~ wine(whitehalllaneprimavera) ),
inference(component_clause,[status(thm)],[f15526]) ).
fof(f15529,definition,
( sQ840_spl
<=> sweetwine(whitehalllaneprimavera) ),
introduced(definition,[new_symbols(definition,[sQ840_spl])],[split_symbol_definition]) ).
fof(f15530,plain,
( ~ sQ840_spl
| sweetwine(whitehalllaneprimavera) ),
inference(component_clause,[status(thm)],[f15529]) ).
fof(f15532,plain,
( sQ840_spl
| ~ sQ839_spl ),
inference(split_clause,[status(thm)],[f15518,f15526,f15529]) ).
fof(f15537,plain,
( sQ839_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15528,f5389]) ).
fof(f15538,plain,
sQ839_spl,
inference(contradiction_clause,[status(thm)],[f15537]) ).
fof(f16007,plain,
! [X0] :
( ~ sQ59_spl
| ~ whitewine(X0)
| ~ q36(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3636,f4731]) ).
fof(f16009,plain,
! [X0] :
( ~ sQ59_spl
| ~ cheninblanc(X0)
| ~ whitewine(X0) ),
inference(resolution,[status(thm)],[f16007,f2829]) ).
fof(f16010,plain,
( ~ sQ59_spl
| ~ whitewine(foxencheninblanc) ),
inference(resolution,[status(thm)],[f16009,f4977]) ).
fof(f16013,plain,
( ~ sQ59_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16010,f6832]) ).
fof(f16014,plain,
~ sQ59_spl,
inference(contradiction_clause,[status(thm)],[f16013]) ).
fof(f16022,plain,
! [X0] :
( ~ sQ58_spl
| ~ whitewine(X0)
| ~ loire(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3629,f4728]) ).
fof(f16026,plain,
( ~ sQ58_spl
| ~ whitewine(sevreetmainemuscadet) ),
inference(resolution,[status(thm)],[f16022,f5177]) ).
fof(f16034,plain,
( ~ sQ57_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5226,f4725]) ).
fof(f16037,plain,
~ sQ57_spl,
inference(contradiction_clause,[status(thm)],[f16034]) ).
fof(f16056,plain,
! [X0] :
( ~ sQ56_spl
| ~ whitewine(X0)
| ~ bordeaux(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3617,f4722]) ).
fof(f16061,plain,
( ~ sQ56_spl
| ~ whitewine(chateaudychemsauterne) ),
inference(resolution,[status(thm)],[f16056,f5157]) ).
fof(f16063,plain,
( ~ sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16061,f6824]) ).
fof(f16064,plain,
~ sQ56_spl,
inference(contradiction_clause,[status(thm)],[f16063]) ).
fof(f16066,plain,
( ~ sQ55_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5009,f4719]) ).
fof(f16068,plain,
~ sQ55_spl,
inference(contradiction_clause,[status(thm)],[f16066]) ).
fof(f16069,plain,
! [X0,X1] :
( ~ sQ54_spl
| ~ hasvintageyear(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f3606,f4716]) ).
fof(f16070,plain,
( ~ sQ54_spl
| sQ77_spl ),
inference(split_clause,[status(thm)],[f16069,f4784,f4715]) ).
fof(f16071,plain,
! [X0] :
( ~ sQ53_spl
| ~ wine(X0)
| ~ q74(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3595,f4713]) ).
fof(f16165,plain,
! [X0] :
( ~ sQ53_spl
| ~ q73(X0)
| ~ wine(X0) ),
inference(resolution,[status(thm)],[f16071,f3202]) ).
fof(f16169,plain,
( ~ sQ53_spl
| ~ wine(stgenevievetexaswhite) ),
inference(resolution,[status(thm)],[f16165,f14518]) ).
fof(f16172,plain,
( ~ sQ53_spl
| ~ sQ307_spl ),
inference(split_clause,[status(thm)],[f16169,f8050,f4712]) ).
fof(f16174,plain,
! [X0] :
( ~ sQ52_spl
| ~ whitetablewine(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3586,f4710]) ).
fof(f16212,plain,
( ~ sQ52_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f16174,f4733,f4709]) ).
fof(f16215,plain,
( ~ sQ840_spl
| ~ sQ51_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f15530,f4707]) ).
fof(f16219,plain,
( ~ sQ840_spl
| ~ sQ51_spl ),
inference(contradiction_clause,[status(thm)],[f16215]) ).
fof(f16223,plain,
( ~ sQ50_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5008,f4704]) ).
fof(f16225,plain,
~ sQ50_spl,
inference(contradiction_clause,[status(thm)],[f16223]) ).
fof(f16229,plain,
( ~ sQ49_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5006,f4701]) ).
fof(f16235,plain,
( ~ sQ48_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5222,f4698]) ).
fof(f16241,plain,
~ sQ48_spl,
inference(contradiction_clause,[status(thm)],[f16235]) ).
fof(f16243,plain,
( ~ sQ47_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5005,f4695]) ).
fof(f16245,plain,
~ sQ47_spl,
inference(contradiction_clause,[status(thm)],[f16243]) ).
fof(f16247,plain,
( ~ sQ46_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5003,f4692]) ).
fof(f16251,plain,
~ sQ46_spl,
inference(contradiction_clause,[status(thm)],[f16247]) ).
fof(f16255,plain,
( ~ sQ45_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4999,f4689]) ).
fof(f16256,plain,
~ sQ45_spl,
inference(contradiction_clause,[status(thm)],[f16255]) ).
fof(f16260,plain,
( ~ sQ44_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4998,f4686]) ).
fof(f16264,plain,
! [X0] :
( ~ sQ43_spl
| ~ q15(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3530,f4683]) ).
fof(f16265,plain,
! [X0] :
( ~ sQ43_spl
| ~ anjou(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f2586,f16264]) ).
fof(f16269,plain,
( ~ sQ43_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4964,f16265]) ).
fof(f16275,plain,
( ~ sQ42_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5210,f4680]) ).
fof(f16279,plain,
~ sQ42_spl,
inference(contradiction_clause,[status(thm)],[f16275]) ).
fof(f16281,plain,
! [X0,X1] :
( ~ sQ41_spl
| ~ locatedin(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f3510,f4677]) ).
fof(f16285,plain,
( ~ sQ41_spl
| sQ79_spl ),
inference(split_clause,[status(thm)],[f16281,f4790,f4676]) ).
fof(f16292,plain,
( ~ sQ40_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5203,f4674]) ).
fof(f16297,plain,
( ~ sQ39_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4996,f4671]) ).
fof(f16298,plain,
~ sQ39_spl,
inference(contradiction_clause,[status(thm)],[f16297]) ).
fof(f16301,plain,
( ~ sQ38_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5196,f4668]) ).
fof(f16991,plain,
! [X0] :
( ~ sQ37_spl
| ~ bordeaux(X0)
| ~ redwine(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3476,f4665]) ).
fof(f16996,plain,
! [X0] :
( ~ sQ37_spl
| ~ q0(X0)
| ~ bordeaux(X0) ),
inference(resolution,[status(thm)],[f16991,f6309]) ).
fof(f17001,plain,
( ~ sQ37_spl
| ~ q0(chateaumargaux) ),
inference(resolution,[status(thm)],[f16996,f5183]) ).
fof(f17008,plain,
! [X0] :
( ~ sQ36_spl
| ~ wine(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3471,f4662]) ).
fof(f17009,plain,
( ~ sQ36_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f17008,f4739,f4661]) ).
fof(f17013,plain,
( ~ sQ35_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4995,f4659]) ).
fof(f17014,plain,
~ sQ35_spl,
inference(contradiction_clause,[status(thm)],[f17013]) ).
fof(f17015,plain,
! [X0] :
( ~ sQ34_spl
| ~ redburgundy(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f5193,f4656]) ).
fof(f17025,plain,
( ~ sQ34_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f17015,f4667,f4655]) ).
fof(f17030,plain,
! [X0] :
( ~ sQ33_spl
| ~ muscadet(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f5191,f4653]) ).
fof(f17035,plain,
( ~ sQ33_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4988,f17030]) ).
fof(f17042,plain,
( ~ sQ32_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4991,f4650]) ).
fof(f17044,plain,
~ sQ32_spl,
inference(contradiction_clause,[status(thm)],[f17042]) ).
fof(f17047,plain,
( ~ sQ31_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4989,f4647]) ).
fof(f17048,plain,
~ sQ31_spl,
inference(contradiction_clause,[status(thm)],[f17047]) ).
fof(f17060,plain,
( ~ sQ29_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4987,f4641]) ).
fof(f17061,plain,
~ sQ29_spl,
inference(contradiction_clause,[status(thm)],[f17060]) ).
fof(f17067,plain,
( ~ sQ28_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5592,f4638]) ).
fof(f17070,plain,
~ sQ28_spl,
inference(contradiction_clause,[status(thm)],[f17067]) ).
fof(f17073,plain,
( ~ sQ27_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4984,f4635]) ).
fof(f17074,plain,
~ sQ27_spl,
inference(contradiction_clause,[status(thm)],[f17073]) ).
fof(f17077,plain,
( ~ sQ26_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5182,f4632]) ).
fof(f17079,plain,
~ sQ26_spl,
inference(contradiction_clause,[status(thm)],[f17077]) ).
fof(f17081,plain,
( ~ sQ25_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4983,f4629]) ).
fof(f17082,plain,
~ sQ25_spl,
inference(contradiction_clause,[status(thm)],[f17081]) ).
fof(f17089,plain,
! [X0] :
( ~ sQ24_spl
| ~ whiteloire(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3393,f4626]) ).
fof(f17099,plain,
( ~ sQ24_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f17089,f4727,f4625]) ).
fof(f17101,plain,
( ~ sQ91_spl
| ~ sQ23_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f6125,f4623]) ).
fof(f17104,plain,
( ~ sQ91_spl
| ~ sQ23_spl ),
inference(contradiction_clause,[status(thm)],[f17101]) ).
fof(f17106,plain,
! [X0] :
( ~ sQ22_spl
| ~ chianti(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3375,f4620]) ).
fof(f17108,plain,
( ~ sQ22_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4978,f17106]) ).
fof(f17109,plain,
~ sQ22_spl,
inference(contradiction_clause,[status(thm)],[f17108]) ).
fof(f17111,plain,
( ~ sQ21_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4982,f4617]) ).
fof(f17112,plain,
~ sQ21_spl,
inference(contradiction_clause,[status(thm)],[f17111]) ).
fof(f17113,plain,
! [X0] :
( ~ sQ20_spl
| ~ winegrape(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3365,f4614]) ).
fof(f17114,plain,
( ~ sQ20_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f17113,f4754,f4613]) ).
fof(f17116,plain,
( ~ sQ132_spl
| ~ sQ19_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f6779,f4611]) ).
fof(f17118,plain,
( ~ sQ132_spl
| ~ sQ19_spl ),
inference(contradiction_clause,[status(thm)],[f17116]) ).
fof(f17121,plain,
! [X0] :
( ~ sQ18_spl
| ~ q14(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3352,f4608]) ).
fof(f17122,plain,
! [X0] :
( ~ sQ18_spl
| ~ beaujolais(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f2581,f17121]) ).
fof(f17125,plain,
( ~ sQ18_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4965,f17122]) ).
fof(f17126,plain,
~ sQ18_spl,
inference(contradiction_clause,[status(thm)],[f17125]) ).
fof(f17129,plain,
! [X0] :
( ~ sQ17_spl
| ~ q35(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3344,f4605]) ).
fof(f17131,plain,
( ~ sQ17_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5130,f17129]) ).
fof(f17136,plain,
~ sQ17_spl,
inference(contradiction_clause,[status(thm)],[f17131]) ).
fof(f17140,plain,
( ~ sQ319_spl
| ~ sQ16_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f8104,f4602]) ).
fof(f17176,plain,
( ~ sQ319_spl
| ~ sQ16_spl ),
inference(contradiction_clause,[status(thm)],[f17140]) ).
fof(f18027,plain,
! [X0] :
( ~ sQ15_spl
| ~ whitewine(X0)
| ~ drywine(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3322,f4599]) ).
fof(f18028,plain,
( ~ sQ149_spl
| ~ sQ15_spl
| ~ whitewine(selakssauvignonblanc) ),
inference(resolution,[status(thm)],[f18027,f7318]) ).
fof(f18064,plain,
( ~ sQ149_spl
| ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18028,f6868]) ).
fof(f18065,plain,
( ~ sQ149_spl
| ~ sQ15_spl ),
inference(contradiction_clause,[status(thm)],[f18064]) ).
fof(f18066,plain,
! [X0] :
( ~ sQ14_spl
| ~ redwine(X0)
| ~ drywine(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3312,f4596]) ).
fof(f18213,plain,
( ~ sQ164_spl
| ~ sQ14_spl
| ~ redwine(formancabernetsauvignon) ),
inference(resolution,[status(thm)],[f18066,f7387]) ).
fof(f18254,plain,
( ~ sQ164_spl
| ~ sQ14_spl
| ~ q0(formancabernetsauvignon) ),
inference(resolution,[status(thm)],[f18213,f6309]) ).
fof(f18255,plain,
( ~ sQ164_spl
| ~ sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18254,f5035]) ).
fof(f18256,plain,
( ~ sQ164_spl
| ~ sQ14_spl ),
inference(contradiction_clause,[status(thm)],[f18255]) ).
fof(f18259,plain,
( ~ sQ13_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4981,f4593]) ).
fof(f18260,plain,
~ sQ13_spl,
inference(contradiction_clause,[status(thm)],[f18259]) ).
fof(f18262,plain,
( ~ sQ90_spl
| ~ sQ12_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f6122,f4590]) ).
fof(f18266,plain,
( ~ sQ90_spl
| ~ sQ12_spl ),
inference(contradiction_clause,[status(thm)],[f18262]) ).
fof(f18270,plain,
( ~ sQ11_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4979,f4587]) ).
fof(f18273,plain,
( ~ sQ10_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4978,f4584]) ).
fof(f18274,plain,
~ sQ10_spl,
inference(contradiction_clause,[status(thm)],[f18273]) ).
fof(f18279,plain,
( ~ sQ9_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4977,f4581]) ).
fof(f18281,plain,
~ sQ9_spl,
inference(contradiction_clause,[status(thm)],[f18279]) ).
fof(f18287,plain,
( ~ sQ8_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5568,f4578]) ).
fof(f18296,plain,
~ sQ8_spl,
inference(contradiction_clause,[status(thm)],[f18287]) ).
fof(f18298,plain,
! [X0] :
( ~ sQ7_spl
| ~ pauillac(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f5163,f4575]) ).
fof(f18311,plain,
( ~ sQ7_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f18298,f4646,f4574]) ).
fof(f18317,plain,
( ~ sQ6_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4966,f4572]) ).
fof(f18318,plain,
~ sQ6_spl,
inference(contradiction_clause,[status(thm)],[f18317]) ).
fof(f18321,plain,
( ~ sQ5_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4965,f4569]) ).
fof(f18322,plain,
~ sQ5_spl,
inference(contradiction_clause,[status(thm)],[f18321]) ).
fof(f18325,plain,
( ~ sQ4_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4964,f4566]) ).
fof(f18327,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f18325]) ).
fof(f18328,plain,
! [X0] :
( ~ sQ3_spl
| ~ redburgundy(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3255,f4563]) ).
fof(f18334,plain,
( ~ sQ3_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f18328,f4667,f4562]) ).
fof(f18341,plain,
! [X0] :
( ~ sQ2_spl
| ~ whitebordeaux(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3246,f4560]) ).
fof(f18352,plain,
( ~ sQ2_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f18341,f4721,f4559]) ).
fof(f18354,plain,
! [X0] :
( ~ sQ0_spl
| ~ wine(X0)
| ~ q48(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3276,f4554]) ).
fof(f18764,plain,
! [X0] :
( ~ sQ0_spl
| ~ q47(X0)
| ~ wine(X0) ),
inference(resolution,[status(thm)],[f18354,f2933]) ).
fof(f18800,plain,
( ~ sQ0_spl
| ~ wine(ventanacheninblanc) ),
inference(resolution,[status(thm)],[f18764,f8601]) ).
fof(f18824,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18800,f5334]) ).
fof(f18825,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f18824]) ).
fof(f18827,plain,
! [X0] :
( ~ sQ1_spl
| ~ q26(X0)
| ~ wine(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f5663,f4557]) ).
fof(f19016,plain,
! [X0] :
( q26(X0)
| ~ locatedin(X0,centraltexasregion) ),
inference(resolution,[status(thm)],[f5123,f7265]) ).
fof(f19243,plain,
q26(stgenevievetexaswhite),
inference(resolution,[status(thm)],[f19016,f4874]) ).
fof(f19248,plain,
( ~ sQ1_spl
| ~ wine(stgenevievetexaswhite) ),
inference(resolution,[status(thm)],[f19243,f18827]) ).
fof(f19250,plain,
( ~ sQ1_spl
| ~ sQ307_spl ),
inference(split_clause,[status(thm)],[f19248,f8050,f4556]) ).
fof(f19262,plain,
( ~ sQ58_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16026,f6817]) ).
fof(f19263,plain,
~ sQ58_spl,
inference(contradiction_clause,[status(thm)],[f19262]) ).
fof(f19266,plain,
( ~ sQ30_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4988,f4644]) ).
fof(f19267,plain,
~ sQ30_spl,
inference(contradiction_clause,[status(thm)],[f19266]) ).
fof(f19269,plain,
~ sQ33_spl,
inference(contradiction_clause,[status(thm)],[f17035]) ).
fof(f19270,plain,
~ sQ44_spl,
inference(contradiction_clause,[status(thm)],[f16260]) ).
fof(f19271,plain,
~ sQ43_spl,
inference(contradiction_clause,[status(thm)],[f16269]) ).
fof(f19272,plain,
~ sQ49_spl,
inference(contradiction_clause,[status(thm)],[f16229]) ).
fof(f19273,plain,
( ~ sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17001,f5185]) ).
fof(f19274,plain,
~ sQ37_spl,
inference(contradiction_clause,[status(thm)],[f19273]) ).
fof(f19275,plain,
~ sQ38_spl,
inference(contradiction_clause,[status(thm)],[f16301]) ).
fof(f19276,plain,
~ sQ11_spl,
inference(contradiction_clause,[status(thm)],[f18270]) ).
fof(f19277,plain,
~ sQ40_spl,
inference(contradiction_clause,[status(thm)],[f16292]) ).
fof(f19278,plain,
$false,
inference(sat_refutation,[status(thm)],[f4805,f5993,f6000,f6135,f6142,f6781,f6783,f7075,f7096,f7163,f7172,f7175,f7320,f7329,f7389,f7398,f8069,f8102,f8106,f8115,f8726,f9092,f9098,f9196,f9452,f9676,f10381,f10384,f10728,f10786,f10846,f10853,f10863,f10908,f10914,f10917,f10923,f12504,f12520,f12522,f12651,f12684,f13979,f15532,f15538,f16014,f16037,f16064,f16068,f16070,f16172,f16212,f16219,f16225,f16241,f16245,f16251,f16256,f16279,f16285,f16298,f17009,f17014,f17025,f17044,f17048,f17061,f17070,f17074,f17079,f17082,f17099,f17104,f17109,f17112,f17114,f17118,f17126,f17136,f17176,f18065,f18256,f18260,f18266,f18274,f18281,f18296,f18311,f18318,f18322,f18327,f18334,f18352,f18825,f19250,f19263,f19267,f19269,f19270,f19271,f19272,f19274,f19275,f19276,f19277]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRD001+1 : TPTP v9.3.1. Released v6.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.37 % Computer : n020.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Mon Sep 21 03:40:33 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.41 % Drodi V4.1.1
% 15.59/2.48 % Refutation found
% 15.59/2.48 % SZS status Theorem for theBenchmark: Theorem is valid
% 15.59/2.48 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 15.59/2.55 % Elapsed time: 2.165040 seconds
% 15.59/2.55 % CPU time: 16.432723 seconds
% 15.59/2.55 % Total memory used: 215.114 MB
% 15.59/2.55 % Net memory used: 211.993 MB
%------------------------------------------------------------------------------