%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PRD001+1 : TPTP v9.3.1. Released v6.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n008.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 : Tue Sep 29 12:30:12 PM UTC 2026
% Result : Theorem 16.32s 3.62s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 313
% Syntax : Number of formulae : 1379 ( 445 unt; 110 def)
% Number of atoms : 3192 ( 0 equ)
% Maximal formula atoms : 85 ( 2 avg)
% Number of connectives : 3182 (1369 ~;1269 |; 293 &)
% ( 110 <=>; 141 =>; 0 <=; 0 <~>)
% Maximal formula depth : 183 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 263 ( 262 usr; 111 prp; 0-2 aty)
% Number of functors : 45 ( 45 usr; 45 con; 0-0 aty)
% Number of variables : 1258 ( 0 sgn 967 !; 291 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
hasbody_aux(pulignymontrachetwhiteburgundy,medium),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula1) ).
fof(f2,axiom,
hasbody_aux(formanchardonnay,full),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula2) ).
fof(f42,axiom,
hascolor_aux(selaksicewine,white),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula42) ).
fof(f43,axiom,
hasflavor_aux(pulignymontrachetwhiteburgundy,moderate),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula43) ).
fof(f44,axiom,
hasflavor_aux(formanchardonnay,moderate),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula44) ).
fof(f54,axiom,
hasflavor_aux(bancroftchardonnay,moderate),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula54) ).
fof(f55,axiom,
hasflavor_aux(elysezinfandel,moderate),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula55) ).
fof(f86,axiom,
hasmaker_aux(pulignymontrachetwhiteburgundy,pulignymontrachet),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula86) ).
fof(f138,axiom,
hassugar_aux(pulignymontrachetwhiteburgundy,dry),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula138) ).
fof(f149,axiom,
hassugar_aux(elysezinfandel,dry),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula149) ).
fof(f178,axiom,
locatedin_aux(californiaregion,usregion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula178) ).
fof(f181,axiom,
locatedin_aux(stgenevievetexaswhite,centraltexasregion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula181) ).
fof(f189,axiom,
locatedin_aux(bancroftchardonnay,naparegion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula189) ).
fof(f191,axiom,
locatedin_aux(naparegion,californiaregion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula191) ).
fof(f197,axiom,
locatedin_aux(centraltexasregion,texasregion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula197) ).
fof(f198,axiom,
locatedin_aux(schlossrothermeltrochenbierenausleseriesling,germanyregion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula198) ).
fof(f231,axiom,
locatedin_aux(whitehalllanecabernetfranc,naparegion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula231) ).
fof(f246,axiom,
ot____nom10_aux(texasregion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula246) ).
fof(f248,axiom,
ot____nom12_aux(dry),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula248) ).
fof(f251,axiom,
ot____nom15_aux(californiaregion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula251) ).
fof(f253,axiom,
ot____nom17_aux(germanyregion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula253) ).
fof(f280,axiom,
ot____nom38_aux(usregion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula280) ).
fof(f290,axiom,
ot____nom45_aux(full),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula290) ).
fof(f396,axiom,
zinfandel_aux(elysezinfandel),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula396) ).
fof(f399,axiom,
zinfandel_aux(mariettazinfandel),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula399) ).
fof(f407,axiom,
whiteburgundy_aux(pulignymontrachetwhiteburgundy),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula407) ).
fof(f409,axiom,
whitewine_aux(stgenevievetexaswhite),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula409) ).
fof(f410,axiom,
muscadet_aux(sevreetmainemuscadet),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula410) ).
fof(f411,axiom,
meursault_aux(chateaudemeursaultmeursault),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula411) ).
fof(f412,axiom,
meritage_aux(kathrynkennedylateral),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula412) ).
fof(f413,axiom,
margaux_aux(chateaumargaux),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula413) ).
fof(f414,axiom,
icewine_aux(selaksicewine),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula414) ).
fof(f415,axiom,
dryriesling_aux(mountadamriesling),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula415) ).
fof(f417,axiom,
cabernetsauvignon_aux(mariettacabernetsauvignon),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula417) ).
fof(f421,axiom,
cabernetfranc_aux(whitehalllanecabernetfranc),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula421) ).
fof(f422,axiom,
beaujolais_aux(chateaumorgonbeaujolais),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula422) ).
fof(f423,axiom,
anjou_aux(rosedanjou),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula423) ).
fof(f424,axiom,
chardonnay_aux(formanchardonnay),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula424) ).
fof(f429,axiom,
cheninblanc_aux(foxencheninblanc),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula429) ).
fof(f431,axiom,
chianti_aux(chianticlassico),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula431) ).
fof(f432,axiom,
cotesdor_aux(closdevougeotcotesdor),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula432) ).
fof(f433,axiom,
merlot_aux(garyfarrellmerlot),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula433) ).
fof(f435,axiom,
pauillac_aux(chateaulafiterothschildpauillac),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula435) ).
fof(f436,axiom,
petitesyrah_aux(mariettapetitesyrah),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula436) ).
fof(f438,axiom,
pinotnoir_aux(mountadampinotnoir),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula438) ).
fof(f441,axiom,
port_aux(taylorport),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula441) ).
fof(f480,axiom,
sancerre_aux(closdelapoussiesancerre),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula480) ).
fof(f481,axiom,
sauternes_aux(chateaudychemsauterne),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula481) ).
fof(f482,axiom,
sauvignonblanc_aux(corbansprivatebinsauvignonblanc),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula482) ).
fof(f486,axiom,
semillon_aux(congressspringssemillon),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula486) ).
fof(f488,axiom,
stemilion_aux(chateauchevalblancstemilion),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula488) ).
fof(f489,axiom,
sweetriesling_aux(schlossrothermeltrochenbierenausleseriesling),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula489) ).
fof(f490,axiom,
sweetriesling_aux(schlossvolradtrochenbierenausleseriesling),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula490) ).
fof(f557,axiom,
kaon2namedobjects(whitehalllanecabernetfranc),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula557) ).
fof(f562,axiom,
kaon2namedobjects(stgenevievetexaswhite),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula562) ).
fof(f605,axiom,
kaon2namedobjects(chianticlassico),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula605) ).
fof(f622,axiom,
kaon2namedobjects(pulignymontrachetwhiteburgundy),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula622) ).
fof(f624,axiom,
kaon2namedobjects(closdevougeotcotesdor),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula624) ).
fof(f646,axiom,
kaon2namedobjects(sevreetmainemuscadet),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula646) ).
fof(f652,axiom,
vintageyear_aux(year1998),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula652) ).
fof(f653,axiom,
hasvintageyear_aux(saucelitocanyonzinfandel1998,year1998),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act1_formula653) ).
fof(f655,axiom,
! [X0,X1] :
( locatedin_aux(X0,X1)
=> locatedin(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula2) ).
fof(f656,axiom,
! [X0,X1] :
( hassugar_aux(X0,X1)
=> hassugar(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula3) ).
fof(f657,axiom,
! [X0,X1] :
( hasmaker_aux(X0,X1)
=> hasmaker(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula4) ).
fof(f658,axiom,
! [X0,X1] :
( hasflavor_aux(X0,X1)
=> hasflavor(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula5) ).
fof(f659,axiom,
! [X0,X1] :
( hascolor_aux(X0,X1)
=> hascolor(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula6) ).
fof(f660,axiom,
! [X0,X1] :
( hasbody_aux(X0,X1)
=> hasbody(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula7) ).
fof(f662,axiom,
! [X0,X1] :
( hasvintageyear_aux(X0,X1)
=> hasvintageyear(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula9) ).
fof(f664,axiom,
! [X0] :
( ot____nom10_aux(X0)
=> ot____nom10(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula11) ).
fof(f666,axiom,
! [X0] :
( ot____nom12_aux(X0)
=> ot____nom12(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula13) ).
fof(f669,axiom,
! [X0] :
( ot____nom15_aux(X0)
=> ot____nom15(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula16) ).
fof(f671,axiom,
! [X0] :
( ot____nom17_aux(X0)
=> ot____nom17(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula18) ).
fof(f694,axiom,
! [X0] :
( ot____nom38_aux(X0)
=> ot____nom38(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula41) ).
fof(f702,axiom,
! [X0] :
( ot____nom45_aux(X0)
=> ot____nom45(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula49) ).
fof(f727,axiom,
! [X0] :
( zinfandel_aux(X0)
=> zinfandel(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula74) ).
fof(f732,axiom,
! [X0] :
( anjou_aux(X0)
=> anjou(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula79) ).
fof(f733,axiom,
! [X0] :
( beaujolais_aux(X0)
=> beaujolais(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula80) ).
fof(f734,axiom,
! [X0] :
( cabernetfranc_aux(X0)
=> cabernetfranc(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula81) ).
fof(f735,axiom,
! [X0] :
( cabernetsauvignon_aux(X0)
=> cabernetsauvignon(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula82) ).
fof(f736,axiom,
! [X0] :
( chardonnay_aux(X0)
=> chardonnay(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula83) ).
fof(f737,axiom,
! [X0] :
( cheninblanc_aux(X0)
=> cheninblanc(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula84) ).
fof(f738,axiom,
! [X0] :
( chianti_aux(X0)
=> chianti(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula85) ).
fof(f739,axiom,
! [X0] :
( cotesdor_aux(X0)
=> cotesdor(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula86) ).
fof(f741,axiom,
! [X0] :
( dryriesling_aux(X0)
=> dryriesling(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula88) ).
fof(f742,axiom,
! [X0] :
( icewine_aux(X0)
=> icewine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula89) ).
fof(f743,axiom,
! [X0] :
( margaux_aux(X0)
=> margaux(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula90) ).
fof(f744,axiom,
! [X0] :
( meritage_aux(X0)
=> meritage(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula91) ).
fof(f745,axiom,
! [X0] :
( merlot_aux(X0)
=> merlot(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula92) ).
fof(f746,axiom,
! [X0] :
( meursault_aux(X0)
=> meursault(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula93) ).
fof(f747,axiom,
! [X0] :
( muscadet_aux(X0)
=> muscadet(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula94) ).
fof(f748,axiom,
! [X0] :
( pauillac_aux(X0)
=> pauillac(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula95) ).
fof(f749,axiom,
! [X0] :
( petitesyrah_aux(X0)
=> petitesyrah(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula96) ).
fof(f750,axiom,
! [X0] :
( pinotnoir_aux(X0)
=> pinotnoir(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula97) ).
fof(f751,axiom,
! [X0] :
( port_aux(X0)
=> port(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula98) ).
fof(f755,axiom,
! [X0] :
( sancerre_aux(X0)
=> sancerre(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula102) ).
fof(f756,axiom,
! [X0] :
( sauternes_aux(X0)
=> sauternes(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula103) ).
fof(f757,axiom,
! [X0] :
( sauvignonblanc_aux(X0)
=> sauvignonblanc(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula104) ).
fof(f758,axiom,
! [X0] :
( semillon_aux(X0)
=> semillon(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula105) ).
fof(f759,axiom,
! [X0] :
( stemilion_aux(X0)
=> stemilion(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula106) ).
fof(f760,axiom,
! [X0] :
( sweetriesling_aux(X0)
=> sweetriesling(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula107) ).
fof(f761,axiom,
! [X0] :
( vintageyear_aux(X0)
=> vintageyear(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula108) ).
fof(f762,axiom,
! [X0] :
( whiteburgundy_aux(X0)
=> whiteburgundy(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula109) ).
fof(f763,axiom,
! [X0] :
( whitewine_aux(X0)
=> whitewine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula110) ).
fof(f771,axiom,
! [X0] :
( zinfandel(X0)
=> q0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula118) ).
fof(f772,axiom,
! [X0] :
( medoc(X0)
=> q0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula119) ).
fof(f794,axiom,
! [X0] :
( pinotblanc(X0)
=> q12(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula141) ).
fof(f795,axiom,
! [X0] :
( whitewine(X0)
=> q12(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula142) ).
fof(f797,axiom,
! [X0] :
( sauternes(X0)
=> q12(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula144) ).
fof(f805,axiom,
! [X0] :
( beaujolais(X0)
=> q14(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula152) ).
fof(f807,axiom,
! [X0] :
( anjou(X0)
=> q15(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula154) ).
fof(f832,axiom,
! [X0] :
( q12(X0)
=> q21(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula179) ).
fof(f833,axiom,
! [X0,X1] :
( ( hascolor(X0,X1)
& ot____nom5(X1) )
=> q21(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula180) ).
fof(f842,axiom,
! [X0] :
( muscadet(X0)
=> q24(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula189) ).
fof(f845,axiom,
! [X0,X1] :
( ( locatedin(X0,X1)
& q27(X1) )
=> q26(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula192) ).
fof(f847,axiom,
! [X0] :
( q26(X0)
=> q27(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula194) ).
fof(f848,axiom,
! [X0,X1] :
( ( locatedin(X0,X1)
& ot____nom38(X1) )
=> q27(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula195) ).
fof(f890,axiom,
! [X0] :
( burgundy(X0)
=> q31(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula237) ).
fof(f930,axiom,
! [X0] :
( q0(X0)
=> q41(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula277) ).
fof(f947,axiom,
! [X0,X1] :
( ( hassugar(X0,X1)
& ot____nom12(X1) )
=> q46(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula294) ).
fof(f950,axiom,
! [X0,X1] :
( ( locatedin(X0,X1)
& q48(X1) )
=> q47(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula297) ).
fof(f952,axiom,
! [X0] :
( q47(X0)
=> q48(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula299) ).
fof(f953,axiom,
! [X0,X1] :
( ( locatedin(X0,X1)
& ot____nom15(X1) )
=> q48(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula300) ).
fof(f982,axiom,
! [X0,X1] :
( ( locatedin(X0,X1)
& ot____nom17(X1) )
=> q50(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula329) ).
fof(f1046,axiom,
! [X0] :
( lateharvest(X0)
=> q70(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula393) ).
fof(f1048,axiom,
! [X0] :
( q70(X0)
=> q71(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula395) ).
fof(f1055,axiom,
! [X0,X1] :
( ( locatedin(X0,X1)
& q74(X1) )
=> q73(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula402) ).
fof(f1057,axiom,
! [X0] :
( q73(X0)
=> q74(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula404) ).
fof(f1058,axiom,
! [X0,X1] :
( ( locatedin(X0,X1)
& ot____nom10(X1) )
=> q74(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula405) ).
fof(f1065,axiom,
! [X0] :
( ( q27(X0)
& wine(X0) )
=> americanwine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula412) ).
fof(f1071,axiom,
! [X0] :
( sauternes(X0)
=> bordeaux(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula418) ).
fof(f1072,axiom,
! [X0] :
( medoc(X0)
=> bordeaux(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula419) ).
fof(f1078,axiom,
! [X0] :
( whiteburgundy(X0)
=> burgundy(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula425) ).
fof(f1079,axiom,
! [X0] :
( redburgundy(X0)
=> burgundy(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula426) ).
fof(f1087,axiom,
! [X0] :
( ( q48(X0)
& wine(X0) )
=> californiawine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula434) ).
fof(f1099,axiom,
! [X0] :
( icewine(X0)
=> dessertwine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula446) ).
fof(f1101,axiom,
! [X0] :
( ( drywine(X0)
& redwine(X0) )
=> dryredwine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula448) ).
fof(f1105,axiom,
! [X0] :
( ( drywine(X0)
& whitewine(X0) )
=> drywhitewine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula452) ).
fof(f1109,axiom,
! [X0] :
( ( q46(X0)
& wine(X0) )
=> drywine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula456) ).
fof(f1116,axiom,
! [X0,X1] :
( ( wine(X0)
& hasbody(X0,X1)
& ot____nom45(X1) )
=> fullbodiedwine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula463) ).
fof(f1117,axiom,
! [X0] :
( q14(X0)
=> gamay(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula464) ).
fof(f1120,axiom,
! [X0] :
( ( q50(X0)
& wine(X0) )
=> germanwine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula467) ).
fof(f1122,axiom,
! [X0] :
( winegrape(X0)
=> grape(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula469) ).
fof(f1126,axiom,
! [X0] :
( chianti(X0)
=> italianwine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula473) ).
fof(f1129,axiom,
! [X0] :
( icewine(X0)
=> lateharvest(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula476) ).
fof(f1136,axiom,
! [X0] :
( muscadet(X0)
=> loire(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula483) ).
fof(f1141,axiom,
! [X0] :
( pauillac(X0)
=> medoc(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula488) ).
fof(f1142,axiom,
! [X0] :
( margaux(X0)
=> medoc(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula489) ).
fof(f1158,axiom,
! [X0] :
( q24(X0)
=> pinotblanc(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula505) ).
fof(f1165,axiom,
! [X0] :
( wine(X0)
=> potableliquid(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula512) ).
fof(f1167,axiom,
! [X0] :
( ( redwine(X0)
& bordeaux(X0) )
=> redbordeaux(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula514) ).
fof(f1169,axiom,
! [X0] :
( cotesdor(X0)
=> redburgundy(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula516) ).
fof(f1172,axiom,
! [X0] :
( ( q41(X0)
& tablewine(X0) )
=> redtablewine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula519) ).
fof(f1174,axiom,
! [X0] :
( redburgundy(X0)
=> redwine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula521) ).
fof(f1177,axiom,
! [X0] :
( port(X0)
=> redwine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula524) ).
fof(f1178,axiom,
! [X0] :
( ( q41(X0)
& wine(X0) )
=> redwine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula525) ).
fof(f1183,axiom,
! [X0] :
( ( wine(X0)
& kaon2namedobjects(X0) )
=> region(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula530) ).
fof(f1186,axiom,
! [X0] :
( sweetriesling(X0)
=> riesling(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula533) ).
fof(f1189,axiom,
! [X0] :
( q15(X0)
=> rosewine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula536) ).
fof(f1201,axiom,
! [X0] :
( sauvignonblanc(X0)
=> semillonorsauvignonblanc(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula548) ).
fof(f1209,axiom,
! [X0] :
( ( q71(X0)
& wine(X0) )
=> sweetwine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula556) ).
fof(f1213,axiom,
! [X0] :
( ( q46(X0)
& wine(X0) )
=> tablewine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula560) ).
fof(f1215,axiom,
! [X0] :
( ( q74(X0)
& wine(X0) )
=> texaswine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula562) ).
fof(f1219,axiom,
! [X0,X1] :
( hasvintageyear(X0,X1)
=> vintage(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula566) ).
fof(f1223,axiom,
! [X0] :
( ( bordeaux(X0)
& whitewine(X0) )
=> whitebordeaux(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula570) ).
fof(f1225,axiom,
! [X0] :
( meursault(X0)
=> whiteburgundy(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula572) ).
fof(f1228,axiom,
! [X0] :
( ( loire(X0)
& whitewine(X0) )
=> whiteloire(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula575) ).
fof(f1230,axiom,
! [X0] :
( ( whitewine(X0)
& kaon2namedobjects(X0) )
=> whitenonsweetwine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula577) ).
fof(f1234,axiom,
! [X0] :
( ( q21(X0)
& tablewine(X0) )
=> whitetablewine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula581) ).
fof(f1237,axiom,
! [X0] :
( whiteburgundy(X0)
=> whitewine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula584) ).
fof(f1241,axiom,
! [X0] :
( ( q21(X0)
& wine(X0) )
=> whitewine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula588) ).
fof(f1248,axiom,
! [X0,X1] :
( haswinedescriptor(X0,X1)
=> wine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula595) ).
fof(f1258,axiom,
! [X0] :
( cabernetfranc(X0)
=> wine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula605) ).
fof(f1262,axiom,
! [X0] :
( loire(X0)
=> wine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula609) ).
fof(f1276,axiom,
! [X0] :
( bordeaux(X0)
=> wine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula623) ).
fof(f1277,axiom,
! [X0] :
( riesling(X0)
=> wine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula624) ).
fof(f1280,axiom,
! [X0] :
( whitewine(X0)
=> wine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula627) ).
fof(f1287,axiom,
! [X0] :
( burgundy(X0)
=> wine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula634) ).
fof(f1298,axiom,
! [X0] :
( lateharvest(X0)
=> wine(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula645) ).
fof(f1302,axiom,
! [X0,X1] :
( hasbody(X0,X1)
=> winebody(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula649) ).
fof(f1305,axiom,
! [X0,X1] :
( hascolor(X0,X1)
=> winecolor(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula652) ).
fof(f1308,axiom,
! [X0] :
( winecolor(X0)
=> winedescriptor(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula655) ).
fof(f1312,axiom,
! [X0,X1] :
( hasflavor(X0,X1)
=> wineflavor(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula659) ).
fof(f1315,axiom,
! [X0,X1] :
( madefromgrape(X0,X1)
=> winegrape(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula662) ).
fof(f1318,axiom,
! [X0,X1] :
( hassugar(X0,X1)
=> winesugar(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula665) ).
fof(f1320,axiom,
! [X0] :
( wineflavor(X0)
=> winetaste(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula667) ).
fof(f1325,axiom,
! [X0,X1] :
( ( wine(X0)
& hasmaker(X0,X1) )
=> winery(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula672) ).
fof(f1335,axiom,
! [X0] :
( ( q31(X0)
& kaon2namedobjects(X0) )
=> ot____nom12(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula682) ).
fof(f1417,axiom,
! [X0] :
( ( q12(X0)
& kaon2namedobjects(X0) )
=> ot____nom5(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula764) ).
fof(f1475,axiom,
! [X0] :
( ( wine(X0)
& kaon2namedobjects(X0) )
=> hasbody(X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula822) ).
fof(f1482,axiom,
! [X0] :
( ( wine(X0)
& kaon2namedobjects(X0) )
=> hascolor(X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula829) ).
fof(f1489,axiom,
! [X0] :
( ( wine(X0)
& kaon2namedobjects(X0) )
=> hasflavor(X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula836) ).
fof(f1493,axiom,
! [X0] :
( ( wine(X0)
& kaon2namedobjects(X0) )
=> hasmaker(X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula840) ).
fof(f1496,axiom,
! [X0] :
( ( wine(X0)
& kaon2namedobjects(X0) )
=> hassugar(X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula843) ).
fof(f1498,axiom,
! [X0] :
( ( whitewine(X0)
& kaon2namedobjects(X0) )
=> hassugar(X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula845) ).
fof(f1508,axiom,
! [X0,X1] :
( hasflavor(X0,X1)
=> haswinedescriptor(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula855) ).
fof(f1509,axiom,
! [X0,X1] :
( hassugar(X0,X1)
=> haswinedescriptor(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula856) ).
fof(f1523,axiom,
! [X0] :
( ( chianti(X0)
& kaon2namedobjects(X0) )
=> locatedin(X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula870) ).
fof(f1541,axiom,
! [X0,X1] :
( madefromgrape(X0,X1)
=> madefromfruit(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula888) ).
fof(f1546,axiom,
! [X0] :
( ( wine(X0)
& kaon2namedobjects(X0) )
=> madefromgrape(X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula893) ).
fof(f1558,axiom,
! [X0] :
( ( cabernetfranc(X0)
& kaon2namedobjects(X0) )
=> madefromgrape(X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula905) ).
fof(f1564,axiom,
! [X0,X1] :
( madefromgrape(X0,X1)
=> madeintowine(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula911) ).
fof(f1567,axiom,
! [X0,X1] :
( hasmaker(X0,X1)
=> produceswine(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act2_formula914) ).
fof(f1615,conjecture,
( ? [X0] : californiawine(X0)
& ? [X0] : americanwine(X0)
& ? [X0] : bordeaux(X0)
& ? [X0] : burgundy(X0)
& ? [X0] : anjou(X0)
& ? [X0] : beaujolais(X0)
& ? [X0] : cabernetfranc(X0)
& ? [X0] : cabernetsauvignon(X0)
& ? [X0] : californiawine(X0)
& ? [X0] : chardonnay(X0)
& ? [X0] : cheninblanc(X0)
& ? [X0] : chianti(X0)
& ? [X0] : cotesdor(X0)
& ? [X0] : dessertwine(X0)
& ? [X0] : dryriesling(X0)
& ? [X0] : dryredwine(X0)
& ? [X0] : drywhitewine(X0)
& ? [X0] : drywine(X0)
& ? [X0] : fullbodiedwine(X0)
& ? [X0] : gamay(X0)
& ? [X0] : germanwine(X0)
& ? [X0] : grape(X0)
& ? [X0] : icewine(X0)
& ? [X0] : italianwine(X0)
& ? [X0] : lateharvest(X0)
& ? [X0] : loire(X0)
& ? [X0] : margaux(X0)
& ? [X0] : medoc(X0)
& ? [X0] : meritage(X0)
& ? [X0] : merlot(X0)
& ? [X0] : meursault(X0)
& ? [X0] : muscadet(X0)
& ? [X0] : pauillac(X0)
& ? [X0] : petitesyrah(X0)
& ? [X0] : pinotblanc(X0)
& ? [X0] : pinotnoir(X0)
& ? [X0] : port(X0)
& ? [X0] : potableliquid(X0)
& ? [X0] : redbordeaux(X0)
& ? [X0] : redburgundy(X0)
& ? [X0] : redtablewine(X0)
& ? [X0] : redwine(X0)
& ? [X0] : region(X0)
& ? [X0] : riesling(X0)
& ? [X0] : rosewine(X0)
& ? [X0] : sancerre(X0)
& ? [X0] : sauternes(X0)
& ? [X0] : sauvignonblanc(X0)
& ? [X0] : semillon(X0)
& ? [X0] : semillonorsauvignonblanc(X0)
& ? [X0] : stemilion(X0)
& ? [X0] : sweetriesling(X0)
& ? [X0] : sweetwine(X0)
& ? [X0] : tablewine(X0)
& ? [X0] : texaswine(X0)
& ? [X0] : vintage(X0)
& ? [X0] : vintageyear(X0)
& ? [X0] : whitebordeaux(X0)
& ? [X0] : whiteburgundy(X0)
& ? [X0] : whiteloire(X0)
& ? [X0] : whitenonsweetwine(X0)
& ? [X0] : whitetablewine(X0)
& ? [X0] : whitewine(X0)
& ? [X0] : wine(X0)
& ? [X0] : winebody(X0)
& ? [X0] : winecolor(X0)
& ? [X0] : winedescriptor(X0)
& ? [X0] : wineflavor(X0)
& ? [X0] : winegrape(X0)
& ? [X0] : winesugar(X0)
& ? [X0] : winery(X0)
& ? [X0] : winetaste(X0)
& ? [X0] : zinfandel(X0)
& ? [X1,X0] : hasbody(X0,X1)
& ? [X1,X0] : hascolor(X0,X1)
& ? [X1,X0] : hasflavor(X0,X1)
& ? [X1,X0] : hasmaker(X0,X1)
& ? [X1,X0] : hassugar(X0,X1)
& ? [X1,X0] : hasvintageyear(X0,X1)
& ? [X1,X0] : haswinedescriptor(X0,X1)
& ? [X1,X0] : locatedin(X0,X1)
& ? [X1,X0] : madefromgrape(X0,X1)
& ? [X1,X0] : madefromfruit(X0,X1)
& ? [X1,X0] : madeintowine(X0,X1)
& ? [X1,X0] : produceswine(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',all) ).
fof(f1616,negated_conjecture,
~ ( ? [X0] : californiawine(X0)
& ? [X0] : americanwine(X0)
& ? [X0] : bordeaux(X0)
& ? [X0] : burgundy(X0)
& ? [X0] : anjou(X0)
& ? [X0] : beaujolais(X0)
& ? [X0] : cabernetfranc(X0)
& ? [X0] : cabernetsauvignon(X0)
& ? [X0] : californiawine(X0)
& ? [X0] : chardonnay(X0)
& ? [X0] : cheninblanc(X0)
& ? [X0] : chianti(X0)
& ? [X0] : cotesdor(X0)
& ? [X0] : dessertwine(X0)
& ? [X0] : dryriesling(X0)
& ? [X0] : dryredwine(X0)
& ? [X0] : drywhitewine(X0)
& ? [X0] : drywine(X0)
& ? [X0] : fullbodiedwine(X0)
& ? [X0] : gamay(X0)
& ? [X0] : germanwine(X0)
& ? [X0] : grape(X0)
& ? [X0] : icewine(X0)
& ? [X0] : italianwine(X0)
& ? [X0] : lateharvest(X0)
& ? [X0] : loire(X0)
& ? [X0] : margaux(X0)
& ? [X0] : medoc(X0)
& ? [X0] : meritage(X0)
& ? [X0] : merlot(X0)
& ? [X0] : meursault(X0)
& ? [X0] : muscadet(X0)
& ? [X0] : pauillac(X0)
& ? [X0] : petitesyrah(X0)
& ? [X0] : pinotblanc(X0)
& ? [X0] : pinotnoir(X0)
& ? [X0] : port(X0)
& ? [X0] : potableliquid(X0)
& ? [X0] : redbordeaux(X0)
& ? [X0] : redburgundy(X0)
& ? [X0] : redtablewine(X0)
& ? [X0] : redwine(X0)
& ? [X0] : region(X0)
& ? [X0] : riesling(X0)
& ? [X0] : rosewine(X0)
& ? [X0] : sancerre(X0)
& ? [X0] : sauternes(X0)
& ? [X0] : sauvignonblanc(X0)
& ? [X0] : semillon(X0)
& ? [X0] : semillonorsauvignonblanc(X0)
& ? [X0] : stemilion(X0)
& ? [X0] : sweetriesling(X0)
& ? [X0] : sweetwine(X0)
& ? [X0] : tablewine(X0)
& ? [X0] : texaswine(X0)
& ? [X0] : vintage(X0)
& ? [X0] : vintageyear(X0)
& ? [X0] : whitebordeaux(X0)
& ? [X0] : whiteburgundy(X0)
& ? [X0] : whiteloire(X0)
& ? [X0] : whitenonsweetwine(X0)
& ? [X0] : whitetablewine(X0)
& ? [X0] : whitewine(X0)
& ? [X0] : wine(X0)
& ? [X0] : winebody(X0)
& ? [X0] : winecolor(X0)
& ? [X0] : winedescriptor(X0)
& ? [X0] : wineflavor(X0)
& ? [X0] : winegrape(X0)
& ? [X0] : winesugar(X0)
& ? [X0] : winery(X0)
& ? [X0] : winetaste(X0)
& ? [X0] : zinfandel(X0)
& ? [X1,X0] : hasbody(X0,X1)
& ? [X1,X0] : hascolor(X0,X1)
& ? [X1,X0] : hasflavor(X0,X1)
& ? [X1,X0] : hasmaker(X0,X1)
& ? [X1,X0] : hassugar(X0,X1)
& ? [X1,X0] : hasvintageyear(X0,X1)
& ? [X1,X0] : haswinedescriptor(X0,X1)
& ? [X1,X0] : locatedin(X0,X1)
& ? [X1,X0] : madefromgrape(X0,X1)
& ? [X1,X0] : madefromfruit(X0,X1)
& ? [X1,X0] : madeintowine(X0,X1)
& ? [X1,X0] : produceswine(X0,X1) ),
inference(negated_conjecture,[status(cth)],[f1615]) ).
fof(f1617,plain,
~ ( ? [X0] : californiawine(X0)
& ? [X1] : americanwine(X1)
& ? [X2] : bordeaux(X2)
& ? [X3] : burgundy(X3)
& ? [X4] : anjou(X4)
& ? [X5] : beaujolais(X5)
& ? [X6] : cabernetfranc(X6)
& ? [X7] : cabernetsauvignon(X7)
& ? [X8] : californiawine(X8)
& ? [X9] : chardonnay(X9)
& ? [X10] : cheninblanc(X10)
& ? [X11] : chianti(X11)
& ? [X12] : cotesdor(X12)
& ? [X13] : dessertwine(X13)
& ? [X14] : dryriesling(X14)
& ? [X15] : dryredwine(X15)
& ? [X16] : drywhitewine(X16)
& ? [X17] : drywine(X17)
& ? [X18] : fullbodiedwine(X18)
& ? [X19] : gamay(X19)
& ? [X20] : germanwine(X20)
& ? [X21] : grape(X21)
& ? [X22] : icewine(X22)
& ? [X23] : italianwine(X23)
& ? [X24] : lateharvest(X24)
& ? [X25] : loire(X25)
& ? [X26] : margaux(X26)
& ? [X27] : medoc(X27)
& ? [X28] : meritage(X28)
& ? [X29] : merlot(X29)
& ? [X30] : meursault(X30)
& ? [X31] : muscadet(X31)
& ? [X32] : pauillac(X32)
& ? [X33] : petitesyrah(X33)
& ? [X34] : pinotblanc(X34)
& ? [X35] : pinotnoir(X35)
& ? [X36] : port(X36)
& ? [X37] : potableliquid(X37)
& ? [X38] : redbordeaux(X38)
& ? [X39] : redburgundy(X39)
& ? [X40] : redtablewine(X40)
& ? [X41] : redwine(X41)
& ? [X42] : region(X42)
& ? [X43] : riesling(X43)
& ? [X44] : rosewine(X44)
& ? [X45] : sancerre(X45)
& ? [X46] : sauternes(X46)
& ? [X47] : sauvignonblanc(X47)
& ? [X48] : semillon(X48)
& ? [X49] : semillonorsauvignonblanc(X49)
& ? [X50] : stemilion(X50)
& ? [X51] : sweetriesling(X51)
& ? [X52] : sweetwine(X52)
& ? [X53] : tablewine(X53)
& ? [X54] : texaswine(X54)
& ? [X55] : vintage(X55)
& ? [X56] : vintageyear(X56)
& ? [X57] : whitebordeaux(X57)
& ? [X58] : whiteburgundy(X58)
& ? [X59] : whiteloire(X59)
& ? [X60] : whitenonsweetwine(X60)
& ? [X61] : whitetablewine(X61)
& ? [X62] : whitewine(X62)
& ? [X63] : wine(X63)
& ? [X64] : winebody(X64)
& ? [X65] : winecolor(X65)
& ? [X66] : winedescriptor(X66)
& ? [X67] : wineflavor(X67)
& ? [X68] : winegrape(X68)
& ? [X69] : winesugar(X69)
& ? [X70] : winery(X70)
& ? [X71] : winetaste(X71)
& ? [X72] : zinfandel(X72)
& ? [X73,X74] : hasbody(X74,X73)
& ? [X75,X76] : hascolor(X76,X75)
& ? [X77,X78] : hasflavor(X78,X77)
& ? [X79,X80] : hasmaker(X80,X79)
& ? [X81,X82] : hassugar(X82,X81)
& ? [X83,X84] : hasvintageyear(X84,X83)
& ? [X85,X86] : haswinedescriptor(X86,X85)
& ? [X87,X88] : locatedin(X88,X87)
& ? [X89,X90] : madefromgrape(X90,X89)
& ? [X91,X92] : madefromfruit(X92,X91)
& ? [X93,X94] : madeintowine(X94,X93)
& ? [X95,X96] : produceswine(X96,X95) ),
inference(rectify,[],[f1616]) ).
fof(f1620,plain,
! [X0,X1] :
( locatedin(X0,X1)
| ~ locatedin_aux(X0,X1) ),
inference(ennf_transformation,[],[f655]) ).
fof(f1621,plain,
! [X0,X1] :
( hassugar(X0,X1)
| ~ hassugar_aux(X0,X1) ),
inference(ennf_transformation,[],[f656]) ).
fof(f1622,plain,
! [X0,X1] :
( hasmaker(X0,X1)
| ~ hasmaker_aux(X0,X1) ),
inference(ennf_transformation,[],[f657]) ).
fof(f1623,plain,
! [X0,X1] :
( hasflavor(X0,X1)
| ~ hasflavor_aux(X0,X1) ),
inference(ennf_transformation,[],[f658]) ).
fof(f1624,plain,
! [X0,X1] :
( hascolor(X0,X1)
| ~ hascolor_aux(X0,X1) ),
inference(ennf_transformation,[],[f659]) ).
fof(f1625,plain,
! [X0,X1] :
( hasbody(X0,X1)
| ~ hasbody_aux(X0,X1) ),
inference(ennf_transformation,[],[f660]) ).
fof(f1626,plain,
! [X0,X1] :
( hasvintageyear(X0,X1)
| ~ hasvintageyear_aux(X0,X1) ),
inference(ennf_transformation,[],[f662]) ).
fof(f1628,plain,
! [X0] :
( ot____nom10(X0)
| ~ ot____nom10_aux(X0) ),
inference(ennf_transformation,[],[f664]) ).
fof(f1630,plain,
! [X0] :
( ot____nom12(X0)
| ~ ot____nom12_aux(X0) ),
inference(ennf_transformation,[],[f666]) ).
fof(f1633,plain,
! [X0] :
( ot____nom15(X0)
| ~ ot____nom15_aux(X0) ),
inference(ennf_transformation,[],[f669]) ).
fof(f1635,plain,
! [X0] :
( ot____nom17(X0)
| ~ ot____nom17_aux(X0) ),
inference(ennf_transformation,[],[f671]) ).
fof(f1658,plain,
! [X0] :
( ot____nom38(X0)
| ~ ot____nom38_aux(X0) ),
inference(ennf_transformation,[],[f694]) ).
fof(f1666,plain,
! [X0] :
( ot____nom45(X0)
| ~ ot____nom45_aux(X0) ),
inference(ennf_transformation,[],[f702]) ).
fof(f1691,plain,
! [X0] :
( zinfandel(X0)
| ~ zinfandel_aux(X0) ),
inference(ennf_transformation,[],[f727]) ).
fof(f1696,plain,
! [X0] :
( anjou(X0)
| ~ anjou_aux(X0) ),
inference(ennf_transformation,[],[f732]) ).
fof(f1697,plain,
! [X0] :
( beaujolais(X0)
| ~ beaujolais_aux(X0) ),
inference(ennf_transformation,[],[f733]) ).
fof(f1698,plain,
! [X0] :
( cabernetfranc(X0)
| ~ cabernetfranc_aux(X0) ),
inference(ennf_transformation,[],[f734]) ).
fof(f1699,plain,
! [X0] :
( cabernetsauvignon(X0)
| ~ cabernetsauvignon_aux(X0) ),
inference(ennf_transformation,[],[f735]) ).
fof(f1700,plain,
! [X0] :
( chardonnay(X0)
| ~ chardonnay_aux(X0) ),
inference(ennf_transformation,[],[f736]) ).
fof(f1701,plain,
! [X0] :
( cheninblanc(X0)
| ~ cheninblanc_aux(X0) ),
inference(ennf_transformation,[],[f737]) ).
fof(f1702,plain,
! [X0] :
( chianti(X0)
| ~ chianti_aux(X0) ),
inference(ennf_transformation,[],[f738]) ).
fof(f1703,plain,
! [X0] :
( cotesdor(X0)
| ~ cotesdor_aux(X0) ),
inference(ennf_transformation,[],[f739]) ).
fof(f1705,plain,
! [X0] :
( dryriesling(X0)
| ~ dryriesling_aux(X0) ),
inference(ennf_transformation,[],[f741]) ).
fof(f1706,plain,
! [X0] :
( icewine(X0)
| ~ icewine_aux(X0) ),
inference(ennf_transformation,[],[f742]) ).
fof(f1707,plain,
! [X0] :
( margaux(X0)
| ~ margaux_aux(X0) ),
inference(ennf_transformation,[],[f743]) ).
fof(f1708,plain,
! [X0] :
( meritage(X0)
| ~ meritage_aux(X0) ),
inference(ennf_transformation,[],[f744]) ).
fof(f1709,plain,
! [X0] :
( merlot(X0)
| ~ merlot_aux(X0) ),
inference(ennf_transformation,[],[f745]) ).
fof(f1710,plain,
! [X0] :
( meursault(X0)
| ~ meursault_aux(X0) ),
inference(ennf_transformation,[],[f746]) ).
fof(f1711,plain,
! [X0] :
( muscadet(X0)
| ~ muscadet_aux(X0) ),
inference(ennf_transformation,[],[f747]) ).
fof(f1712,plain,
! [X0] :
( pauillac(X0)
| ~ pauillac_aux(X0) ),
inference(ennf_transformation,[],[f748]) ).
fof(f1713,plain,
! [X0] :
( petitesyrah(X0)
| ~ petitesyrah_aux(X0) ),
inference(ennf_transformation,[],[f749]) ).
fof(f1714,plain,
! [X0] :
( pinotnoir(X0)
| ~ pinotnoir_aux(X0) ),
inference(ennf_transformation,[],[f750]) ).
fof(f1715,plain,
! [X0] :
( port(X0)
| ~ port_aux(X0) ),
inference(ennf_transformation,[],[f751]) ).
fof(f1719,plain,
! [X0] :
( sancerre(X0)
| ~ sancerre_aux(X0) ),
inference(ennf_transformation,[],[f755]) ).
fof(f1720,plain,
! [X0] :
( sauternes(X0)
| ~ sauternes_aux(X0) ),
inference(ennf_transformation,[],[f756]) ).
fof(f1721,plain,
! [X0] :
( sauvignonblanc(X0)
| ~ sauvignonblanc_aux(X0) ),
inference(ennf_transformation,[],[f757]) ).
fof(f1722,plain,
! [X0] :
( semillon(X0)
| ~ semillon_aux(X0) ),
inference(ennf_transformation,[],[f758]) ).
fof(f1723,plain,
! [X0] :
( stemilion(X0)
| ~ stemilion_aux(X0) ),
inference(ennf_transformation,[],[f759]) ).
fof(f1724,plain,
! [X0] :
( sweetriesling(X0)
| ~ sweetriesling_aux(X0) ),
inference(ennf_transformation,[],[f760]) ).
fof(f1725,plain,
! [X0] :
( vintageyear(X0)
| ~ vintageyear_aux(X0) ),
inference(ennf_transformation,[],[f761]) ).
fof(f1726,plain,
! [X0] :
( whiteburgundy(X0)
| ~ whiteburgundy_aux(X0) ),
inference(ennf_transformation,[],[f762]) ).
fof(f1727,plain,
! [X0] :
( whitewine(X0)
| ~ whitewine_aux(X0) ),
inference(ennf_transformation,[],[f763]) ).
fof(f1735,plain,
! [X0] :
( q0(X0)
| ~ zinfandel(X0) ),
inference(ennf_transformation,[],[f771]) ).
fof(f1736,plain,
! [X0] :
( q0(X0)
| ~ medoc(X0) ),
inference(ennf_transformation,[],[f772]) ).
fof(f1764,plain,
! [X0] :
( q12(X0)
| ~ pinotblanc(X0) ),
inference(ennf_transformation,[],[f794]) ).
fof(f1765,plain,
! [X0] :
( q12(X0)
| ~ whitewine(X0) ),
inference(ennf_transformation,[],[f795]) ).
fof(f1767,plain,
! [X0] :
( q12(X0)
| ~ sauternes(X0) ),
inference(ennf_transformation,[],[f797]) ).
fof(f1777,plain,
! [X0] :
( q14(X0)
| ~ beaujolais(X0) ),
inference(ennf_transformation,[],[f805]) ).
fof(f1780,plain,
! [X0] :
( q15(X0)
| ~ anjou(X0) ),
inference(ennf_transformation,[],[f807]) ).
fof(f1817,plain,
! [X0] :
( q21(X0)
| ~ q12(X0) ),
inference(ennf_transformation,[],[f832]) ).
fof(f1818,plain,
! [X0,X1] :
( q21(X0)
| ~ hascolor(X0,X1)
| ~ ot____nom5(X1) ),
inference(ennf_transformation,[],[f833]) ).
fof(f1819,plain,
! [X0,X1] :
( q21(X0)
| ~ hascolor(X0,X1)
| ~ ot____nom5(X1) ),
inference(flattening,[],[f1818]) ).
fof(f1833,plain,
! [X0] :
( q24(X0)
| ~ muscadet(X0) ),
inference(ennf_transformation,[],[f842]) ).
fof(f1837,plain,
! [X0,X1] :
( q26(X0)
| ~ locatedin(X0,X1)
| ~ q27(X1) ),
inference(ennf_transformation,[],[f845]) ).
fof(f1838,plain,
! [X0,X1] :
( q26(X0)
| ~ locatedin(X0,X1)
| ~ q27(X1) ),
inference(flattening,[],[f1837]) ).
fof(f1841,plain,
! [X0] :
( q27(X0)
| ~ q26(X0) ),
inference(ennf_transformation,[],[f847]) ).
fof(f1842,plain,
! [X0,X1] :
( q27(X0)
| ~ locatedin(X0,X1)
| ~ ot____nom38(X1) ),
inference(ennf_transformation,[],[f848]) ).
fof(f1843,plain,
! [X0,X1] :
( q27(X0)
| ~ locatedin(X0,X1)
| ~ ot____nom38(X1) ),
inference(flattening,[],[f1842]) ).
fof(f1892,plain,
! [X0] :
( q31(X0)
| ~ burgundy(X0) ),
inference(ennf_transformation,[],[f890]) ).
fof(f1949,plain,
! [X0] :
( q41(X0)
| ~ q0(X0) ),
inference(ennf_transformation,[],[f930]) ).
fof(f1974,plain,
! [X0,X1] :
( q46(X0)
| ~ hassugar(X0,X1)
| ~ ot____nom12(X1) ),
inference(ennf_transformation,[],[f947]) ).
fof(f1975,plain,
! [X0,X1] :
( q46(X0)
| ~ hassugar(X0,X1)
| ~ ot____nom12(X1) ),
inference(flattening,[],[f1974]) ).
fof(f1979,plain,
! [X0,X1] :
( q47(X0)
| ~ locatedin(X0,X1)
| ~ q48(X1) ),
inference(ennf_transformation,[],[f950]) ).
fof(f1980,plain,
! [X0,X1] :
( q47(X0)
| ~ locatedin(X0,X1)
| ~ q48(X1) ),
inference(flattening,[],[f1979]) ).
fof(f1983,plain,
! [X0] :
( q48(X0)
| ~ q47(X0) ),
inference(ennf_transformation,[],[f952]) ).
fof(f1984,plain,
! [X0,X1] :
( q48(X0)
| ~ locatedin(X0,X1)
| ~ ot____nom15(X1) ),
inference(ennf_transformation,[],[f953]) ).
fof(f1985,plain,
! [X0,X1] :
( q48(X0)
| ~ locatedin(X0,X1)
| ~ ot____nom15(X1) ),
inference(flattening,[],[f1984]) ).
fof(f2032,plain,
! [X0,X1] :
( q50(X0)
| ~ locatedin(X0,X1)
| ~ ot____nom17(X1) ),
inference(ennf_transformation,[],[f982]) ).
fof(f2033,plain,
! [X0,X1] :
( q50(X0)
| ~ locatedin(X0,X1)
| ~ ot____nom17(X1) ),
inference(flattening,[],[f2032]) ).
fof(f2131,plain,
! [X0] :
( q70(X0)
| ~ lateharvest(X0) ),
inference(ennf_transformation,[],[f1046]) ).
fof(f2134,plain,
! [X0] :
( q71(X0)
| ~ q70(X0) ),
inference(ennf_transformation,[],[f1048]) ).
fof(f2144,plain,
! [X0,X1] :
( q73(X0)
| ~ locatedin(X0,X1)
| ~ q74(X1) ),
inference(ennf_transformation,[],[f1055]) ).
fof(f2145,plain,
! [X0,X1] :
( q73(X0)
| ~ locatedin(X0,X1)
| ~ q74(X1) ),
inference(flattening,[],[f2144]) ).
fof(f2148,plain,
! [X0] :
( q74(X0)
| ~ q73(X0) ),
inference(ennf_transformation,[],[f1057]) ).
fof(f2149,plain,
! [X0,X1] :
( q74(X0)
| ~ locatedin(X0,X1)
| ~ ot____nom10(X1) ),
inference(ennf_transformation,[],[f1058]) ).
fof(f2150,plain,
! [X0,X1] :
( q74(X0)
| ~ locatedin(X0,X1)
| ~ ot____nom10(X1) ),
inference(flattening,[],[f2149]) ).
fof(f2162,plain,
! [X0] :
( americanwine(X0)
| ~ q27(X0)
| ~ wine(X0) ),
inference(ennf_transformation,[],[f1065]) ).
fof(f2163,plain,
! [X0] :
( americanwine(X0)
| ~ q27(X0)
| ~ wine(X0) ),
inference(flattening,[],[f2162]) ).
fof(f2174,plain,
! [X0] :
( bordeaux(X0)
| ~ sauternes(X0) ),
inference(ennf_transformation,[],[f1071]) ).
fof(f2175,plain,
! [X0] :
( bordeaux(X0)
| ~ medoc(X0) ),
inference(ennf_transformation,[],[f1072]) ).
fof(f2183,plain,
! [X0] :
( burgundy(X0)
| ~ whiteburgundy(X0) ),
inference(ennf_transformation,[],[f1078]) ).
fof(f2184,plain,
! [X0] :
( burgundy(X0)
| ~ redburgundy(X0) ),
inference(ennf_transformation,[],[f1079]) ).
fof(f2198,plain,
! [X0] :
( californiawine(X0)
| ~ q48(X0)
| ~ wine(X0) ),
inference(ennf_transformation,[],[f1087]) ).
fof(f2199,plain,
! [X0] :
( californiawine(X0)
| ~ q48(X0)
| ~ wine(X0) ),
inference(flattening,[],[f2198]) ).
fof(f2219,plain,
! [X0] :
( dessertwine(X0)
| ~ icewine(X0) ),
inference(ennf_transformation,[],[f1099]) ).
fof(f2222,plain,
! [X0] :
( dryredwine(X0)
| ~ drywine(X0)
| ~ redwine(X0) ),
inference(ennf_transformation,[],[f1101]) ).
fof(f2223,plain,
! [X0] :
( dryredwine(X0)
| ~ drywine(X0)
| ~ redwine(X0) ),
inference(flattening,[],[f2222]) ).
fof(f2230,plain,
! [X0] :
( drywhitewine(X0)
| ~ drywine(X0)
| ~ whitewine(X0) ),
inference(ennf_transformation,[],[f1105]) ).
fof(f2231,plain,
! [X0] :
( drywhitewine(X0)
| ~ drywine(X0)
| ~ whitewine(X0) ),
inference(flattening,[],[f2230]) ).
fof(f2236,plain,
! [X0] :
( drywine(X0)
| ~ q46(X0)
| ~ wine(X0) ),
inference(ennf_transformation,[],[f1109]) ).
fof(f2237,plain,
! [X0] :
( drywine(X0)
| ~ q46(X0)
| ~ wine(X0) ),
inference(flattening,[],[f2236]) ).
fof(f2249,plain,
! [X0,X1] :
( fullbodiedwine(X0)
| ~ wine(X0)
| ~ hasbody(X0,X1)
| ~ ot____nom45(X1) ),
inference(ennf_transformation,[],[f1116]) ).
fof(f2250,plain,
! [X0,X1] :
( fullbodiedwine(X0)
| ~ wine(X0)
| ~ hasbody(X0,X1)
| ~ ot____nom45(X1) ),
inference(flattening,[],[f2249]) ).
fof(f2251,plain,
! [X0] :
( gamay(X0)
| ~ q14(X0) ),
inference(ennf_transformation,[],[f1117]) ).
fof(f2256,plain,
! [X0] :
( germanwine(X0)
| ~ q50(X0)
| ~ wine(X0) ),
inference(ennf_transformation,[],[f1120]) ).
fof(f2257,plain,
! [X0] :
( germanwine(X0)
| ~ q50(X0)
| ~ wine(X0) ),
inference(flattening,[],[f2256]) ).
fof(f2260,plain,
! [X0] :
( grape(X0)
| ~ winegrape(X0) ),
inference(ennf_transformation,[],[f1122]) ).
fof(f2267,plain,
! [X0] :
( italianwine(X0)
| ~ chianti(X0) ),
inference(ennf_transformation,[],[f1126]) ).
fof(f2272,plain,
! [X0] :
( lateharvest(X0)
| ~ icewine(X0) ),
inference(ennf_transformation,[],[f1129]) ).
fof(f2280,plain,
! [X0] :
( loire(X0)
| ~ muscadet(X0) ),
inference(ennf_transformation,[],[f1136]) ).
fof(f2289,plain,
! [X0] :
( medoc(X0)
| ~ pauillac(X0) ),
inference(ennf_transformation,[],[f1141]) ).
fof(f2290,plain,
! [X0] :
( medoc(X0)
| ~ margaux(X0) ),
inference(ennf_transformation,[],[f1142]) ).
fof(f2320,plain,
! [X0] :
( pinotblanc(X0)
| ~ q24(X0) ),
inference(ennf_transformation,[],[f1158]) ).
fof(f2332,plain,
! [X0] :
( potableliquid(X0)
| ~ wine(X0) ),
inference(ennf_transformation,[],[f1165]) ).
fof(f2335,plain,
! [X0] :
( redbordeaux(X0)
| ~ redwine(X0)
| ~ bordeaux(X0) ),
inference(ennf_transformation,[],[f1167]) ).
fof(f2336,plain,
! [X0] :
( redbordeaux(X0)
| ~ redwine(X0)
| ~ bordeaux(X0) ),
inference(flattening,[],[f2335]) ).
fof(f2339,plain,
! [X0] :
( redburgundy(X0)
| ~ cotesdor(X0) ),
inference(ennf_transformation,[],[f1169]) ).
fof(f2344,plain,
! [X0] :
( redtablewine(X0)
| ~ q41(X0)
| ~ tablewine(X0) ),
inference(ennf_transformation,[],[f1172]) ).
fof(f2345,plain,
! [X0] :
( redtablewine(X0)
| ~ q41(X0)
| ~ tablewine(X0) ),
inference(flattening,[],[f2344]) ).
fof(f2348,plain,
! [X0] :
( redwine(X0)
| ~ redburgundy(X0) ),
inference(ennf_transformation,[],[f1174]) ).
fof(f2351,plain,
! [X0] :
( redwine(X0)
| ~ port(X0) ),
inference(ennf_transformation,[],[f1177]) ).
fof(f2352,plain,
! [X0] :
( redwine(X0)
| ~ q41(X0)
| ~ wine(X0) ),
inference(ennf_transformation,[],[f1178]) ).
fof(f2353,plain,
! [X0] :
( redwine(X0)
| ~ q41(X0)
| ~ wine(X0) ),
inference(flattening,[],[f2352]) ).
fof(f2359,plain,
! [X0] :
( region(X0)
| ~ wine(X0)
| ~ kaon2namedobjects(X0) ),
inference(ennf_transformation,[],[f1183]) ).
fof(f2360,plain,
! [X0] :
( region(X0)
| ~ wine(X0)
| ~ kaon2namedobjects(X0) ),
inference(flattening,[],[f2359]) ).
fof(f2364,plain,
! [X0] :
( riesling(X0)
| ~ sweetriesling(X0) ),
inference(ennf_transformation,[],[f1186]) ).
fof(f2369,plain,
! [X0] :
( rosewine(X0)
| ~ q15(X0) ),
inference(ennf_transformation,[],[f1189]) ).
fof(f2391,plain,
! [X0] :
( semillonorsauvignonblanc(X0)
| ~ sauvignonblanc(X0) ),
inference(ennf_transformation,[],[f1201]) ).
fof(f2406,plain,
! [X0] :
( sweetwine(X0)
| ~ q71(X0)
| ~ wine(X0) ),
inference(ennf_transformation,[],[f1209]) ).
fof(f2407,plain,
! [X0] :
( sweetwine(X0)
| ~ q71(X0)
| ~ wine(X0) ),
inference(flattening,[],[f2406]) ).
fof(f2412,plain,
! [X0] :
( tablewine(X0)
| ~ q46(X0)
| ~ wine(X0) ),
inference(ennf_transformation,[],[f1213]) ).
fof(f2413,plain,
! [X0] :
( tablewine(X0)
| ~ q46(X0)
| ~ wine(X0) ),
inference(flattening,[],[f2412]) ).
fof(f2416,plain,
! [X0] :
( texaswine(X0)
| ~ q74(X0)
| ~ wine(X0) ),
inference(ennf_transformation,[],[f1215]) ).
fof(f2417,plain,
! [X0] :
( texaswine(X0)
| ~ q74(X0)
| ~ wine(X0) ),
inference(flattening,[],[f2416]) ).
fof(f2424,plain,
! [X0,X1] :
( vintage(X0)
| ~ hasvintageyear(X0,X1) ),
inference(ennf_transformation,[],[f1219]) ).
fof(f2430,plain,
! [X0] :
( whitebordeaux(X0)
| ~ bordeaux(X0)
| ~ whitewine(X0) ),
inference(ennf_transformation,[],[f1223]) ).
fof(f2431,plain,
! [X0] :
( whitebordeaux(X0)
| ~ bordeaux(X0)
| ~ whitewine(X0) ),
inference(flattening,[],[f2430]) ).
fof(f2434,plain,
! [X0] :
( whiteburgundy(X0)
| ~ meursault(X0) ),
inference(ennf_transformation,[],[f1225]) ).
fof(f2439,plain,
! [X0] :
( whiteloire(X0)
| ~ loire(X0)
| ~ whitewine(X0) ),
inference(ennf_transformation,[],[f1228]) ).
fof(f2440,plain,
! [X0] :
( whiteloire(X0)
| ~ loire(X0)
| ~ whitewine(X0) ),
inference(flattening,[],[f2439]) ).
fof(f2443,plain,
! [X0] :
( whitenonsweetwine(X0)
| ~ whitewine(X0)
| ~ kaon2namedobjects(X0) ),
inference(ennf_transformation,[],[f1230]) ).
fof(f2444,plain,
! [X0] :
( whitenonsweetwine(X0)
| ~ whitewine(X0)
| ~ kaon2namedobjects(X0) ),
inference(flattening,[],[f2443]) ).
fof(f2451,plain,
! [X0] :
( whitetablewine(X0)
| ~ q21(X0)
| ~ tablewine(X0) ),
inference(ennf_transformation,[],[f1234]) ).
fof(f2452,plain,
! [X0] :
( whitetablewine(X0)
| ~ q21(X0)
| ~ tablewine(X0) ),
inference(flattening,[],[f2451]) ).
fof(f2456,plain,
! [X0] :
( whitewine(X0)
| ~ whiteburgundy(X0) ),
inference(ennf_transformation,[],[f1237]) ).
fof(f2460,plain,
! [X0] :
( whitewine(X0)
| ~ q21(X0)
| ~ wine(X0) ),
inference(ennf_transformation,[],[f1241]) ).
fof(f2461,plain,
! [X0] :
( whitewine(X0)
| ~ q21(X0)
| ~ wine(X0) ),
inference(flattening,[],[f2460]) ).
fof(f2469,plain,
! [X0,X1] :
( wine(X0)
| ~ haswinedescriptor(X0,X1) ),
inference(ennf_transformation,[],[f1248]) ).
fof(f2479,plain,
! [X0] :
( wine(X0)
| ~ cabernetfranc(X0) ),
inference(ennf_transformation,[],[f1258]) ).
fof(f2483,plain,
! [X0] :
( wine(X0)
| ~ loire(X0) ),
inference(ennf_transformation,[],[f1262]) ).
fof(f2497,plain,
! [X0] :
( wine(X0)
| ~ bordeaux(X0) ),
inference(ennf_transformation,[],[f1276]) ).
fof(f2498,plain,
! [X0] :
( wine(X0)
| ~ riesling(X0) ),
inference(ennf_transformation,[],[f1277]) ).
fof(f2501,plain,
! [X0] :
( wine(X0)
| ~ whitewine(X0) ),
inference(ennf_transformation,[],[f1280]) ).
fof(f2508,plain,
! [X0] :
( wine(X0)
| ~ burgundy(X0) ),
inference(ennf_transformation,[],[f1287]) ).
fof(f2519,plain,
! [X0] :
( wine(X0)
| ~ lateharvest(X0) ),
inference(ennf_transformation,[],[f1298]) ).
fof(f2524,plain,
! [X0,X1] :
( winebody(X1)
| ~ hasbody(X0,X1) ),
inference(ennf_transformation,[],[f1302]) ).
fof(f2528,plain,
! [X0,X1] :
( winecolor(X1)
| ~ hascolor(X0,X1) ),
inference(ennf_transformation,[],[f1305]) ).
fof(f2532,plain,
! [X0] :
( winedescriptor(X0)
| ~ winecolor(X0) ),
inference(ennf_transformation,[],[f1308]) ).
fof(f2537,plain,
! [X0,X1] :
( wineflavor(X1)
| ~ hasflavor(X0,X1) ),
inference(ennf_transformation,[],[f1312]) ).
fof(f2541,plain,
! [X0,X1] :
( winegrape(X1)
| ~ madefromgrape(X0,X1) ),
inference(ennf_transformation,[],[f1315]) ).
fof(f2545,plain,
! [X0,X1] :
( winesugar(X1)
| ~ hassugar(X0,X1) ),
inference(ennf_transformation,[],[f1318]) ).
fof(f2548,plain,
! [X0] :
( winetaste(X0)
| ~ wineflavor(X0) ),
inference(ennf_transformation,[],[f1320]) ).
fof(f2554,plain,
! [X0,X1] :
( winery(X1)
| ~ wine(X0)
| ~ hasmaker(X0,X1) ),
inference(ennf_transformation,[],[f1325]) ).
fof(f2555,plain,
! [X0,X1] :
( winery(X1)
| ~ wine(X0)
| ~ hasmaker(X0,X1) ),
inference(flattening,[],[f2554]) ).
fof(f2574,plain,
! [X0] :
( ot____nom12(X0)
| ~ q31(X0)
| ~ kaon2namedobjects(X0) ),
inference(ennf_transformation,[],[f1335]) ).
fof(f2575,plain,
! [X0] :
( ot____nom12(X0)
| ~ q31(X0)
| ~ kaon2namedobjects(X0) ),
inference(flattening,[],[f2574]) ).
fof(f2735,plain,
! [X0] :
( ot____nom5(X0)
| ~ q12(X0)
| ~ kaon2namedobjects(X0) ),
inference(ennf_transformation,[],[f1417]) ).
fof(f2736,plain,
! [X0] :
( ot____nom5(X0)
| ~ q12(X0)
| ~ kaon2namedobjects(X0) ),
inference(flattening,[],[f2735]) ).
fof(f2849,plain,
! [X0] :
( hasbody(X0,X0)
| ~ wine(X0)
| ~ kaon2namedobjects(X0) ),
inference(ennf_transformation,[],[f1475]) ).
fof(f2850,plain,
! [X0] :
( hasbody(X0,X0)
| ~ wine(X0)
| ~ kaon2namedobjects(X0) ),
inference(flattening,[],[f2849]) ).
fof(f2863,plain,
! [X0] :
( hascolor(X0,X0)
| ~ wine(X0)
| ~ kaon2namedobjects(X0) ),
inference(ennf_transformation,[],[f1482]) ).
fof(f2864,plain,
! [X0] :
( hascolor(X0,X0)
| ~ wine(X0)
| ~ kaon2namedobjects(X0) ),
inference(flattening,[],[f2863]) ).
fof(f2877,plain,
! [X0] :
( hasflavor(X0,X0)
| ~ wine(X0)
| ~ kaon2namedobjects(X0) ),
inference(ennf_transformation,[],[f1489]) ).
fof(f2878,plain,
! [X0] :
( hasflavor(X0,X0)
| ~ wine(X0)
| ~ kaon2namedobjects(X0) ),
inference(flattening,[],[f2877]) ).
fof(f2884,plain,
! [X0] :
( hasmaker(X0,X0)
| ~ wine(X0)
| ~ kaon2namedobjects(X0) ),
inference(ennf_transformation,[],[f1493]) ).
fof(f2885,plain,
! [X0] :
( hasmaker(X0,X0)
| ~ wine(X0)
| ~ kaon2namedobjects(X0) ),
inference(flattening,[],[f2884]) ).
fof(f2890,plain,
! [X0] :
( hassugar(X0,X0)
| ~ wine(X0)
| ~ kaon2namedobjects(X0) ),
inference(ennf_transformation,[],[f1496]) ).
fof(f2891,plain,
! [X0] :
( hassugar(X0,X0)
| ~ wine(X0)
| ~ kaon2namedobjects(X0) ),
inference(flattening,[],[f2890]) ).
fof(f2894,plain,
! [X0] :
( hassugar(X0,X0)
| ~ whitewine(X0)
| ~ kaon2namedobjects(X0) ),
inference(ennf_transformation,[],[f1498]) ).
fof(f2895,plain,
! [X0] :
( hassugar(X0,X0)
| ~ whitewine(X0)
| ~ kaon2namedobjects(X0) ),
inference(flattening,[],[f2894]) ).
fof(f2912,plain,
! [X0,X1] :
( haswinedescriptor(X0,X1)
| ~ hasflavor(X0,X1) ),
inference(ennf_transformation,[],[f1508]) ).
fof(f2913,plain,
! [X0,X1] :
( haswinedescriptor(X0,X1)
| ~ hassugar(X0,X1) ),
inference(ennf_transformation,[],[f1509]) ).
fof(f2940,plain,
! [X0] :
( locatedin(X0,X0)
| ~ chianti(X0)
| ~ kaon2namedobjects(X0) ),
inference(ennf_transformation,[],[f1523]) ).
fof(f2941,plain,
! [X0] :
( locatedin(X0,X0)
| ~ chianti(X0)
| ~ kaon2namedobjects(X0) ),
inference(flattening,[],[f2940]) ).
fof(f2976,plain,
! [X0,X1] :
( madefromfruit(X0,X1)
| ~ madefromgrape(X0,X1) ),
inference(ennf_transformation,[],[f1541]) ).
fof(f2984,plain,
! [X0] :
( madefromgrape(X0,X0)
| ~ wine(X0)
| ~ kaon2namedobjects(X0) ),
inference(ennf_transformation,[],[f1546]) ).
fof(f2985,plain,
! [X0] :
( madefromgrape(X0,X0)
| ~ wine(X0)
| ~ kaon2namedobjects(X0) ),
inference(flattening,[],[f2984]) ).
fof(f3008,plain,
! [X0] :
( madefromgrape(X0,X0)
| ~ cabernetfranc(X0)
| ~ kaon2namedobjects(X0) ),
inference(ennf_transformation,[],[f1558]) ).
fof(f3009,plain,
! [X0] :
( madefromgrape(X0,X0)
| ~ cabernetfranc(X0)
| ~ kaon2namedobjects(X0) ),
inference(flattening,[],[f3008]) ).
fof(f3020,plain,
! [X0,X1] :
( madeintowine(X1,X0)
| ~ madefromgrape(X0,X1) ),
inference(ennf_transformation,[],[f1564]) ).
fof(f3025,plain,
! [X0,X1] :
( produceswine(X1,X0)
| ~ hasmaker(X0,X1) ),
inference(ennf_transformation,[],[f1567]) ).
fof(f3084,plain,
( ! [X0] : ~ californiawine(X0)
| ! [X1] : ~ americanwine(X1)
| ! [X2] : ~ bordeaux(X2)
| ! [X3] : ~ burgundy(X3)
| ! [X4] : ~ anjou(X4)
| ! [X5] : ~ beaujolais(X5)
| ! [X6] : ~ cabernetfranc(X6)
| ! [X7] : ~ cabernetsauvignon(X7)
| ! [X8] : ~ californiawine(X8)
| ! [X9] : ~ chardonnay(X9)
| ! [X10] : ~ cheninblanc(X10)
| ! [X11] : ~ chianti(X11)
| ! [X12] : ~ cotesdor(X12)
| ! [X13] : ~ dessertwine(X13)
| ! [X14] : ~ dryriesling(X14)
| ! [X15] : ~ dryredwine(X15)
| ! [X16] : ~ drywhitewine(X16)
| ! [X17] : ~ drywine(X17)
| ! [X18] : ~ fullbodiedwine(X18)
| ! [X19] : ~ gamay(X19)
| ! [X20] : ~ germanwine(X20)
| ! [X21] : ~ grape(X21)
| ! [X22] : ~ icewine(X22)
| ! [X23] : ~ italianwine(X23)
| ! [X24] : ~ lateharvest(X24)
| ! [X25] : ~ loire(X25)
| ! [X26] : ~ margaux(X26)
| ! [X27] : ~ medoc(X27)
| ! [X28] : ~ meritage(X28)
| ! [X29] : ~ merlot(X29)
| ! [X30] : ~ meursault(X30)
| ! [X31] : ~ muscadet(X31)
| ! [X32] : ~ pauillac(X32)
| ! [X33] : ~ petitesyrah(X33)
| ! [X34] : ~ pinotblanc(X34)
| ! [X35] : ~ pinotnoir(X35)
| ! [X36] : ~ port(X36)
| ! [X37] : ~ potableliquid(X37)
| ! [X38] : ~ redbordeaux(X38)
| ! [X39] : ~ redburgundy(X39)
| ! [X40] : ~ redtablewine(X40)
| ! [X41] : ~ redwine(X41)
| ! [X42] : ~ region(X42)
| ! [X43] : ~ riesling(X43)
| ! [X44] : ~ rosewine(X44)
| ! [X45] : ~ sancerre(X45)
| ! [X46] : ~ sauternes(X46)
| ! [X47] : ~ sauvignonblanc(X47)
| ! [X48] : ~ semillon(X48)
| ! [X49] : ~ semillonorsauvignonblanc(X49)
| ! [X50] : ~ stemilion(X50)
| ! [X51] : ~ sweetriesling(X51)
| ! [X52] : ~ sweetwine(X52)
| ! [X53] : ~ tablewine(X53)
| ! [X54] : ~ texaswine(X54)
| ! [X55] : ~ vintage(X55)
| ! [X56] : ~ vintageyear(X56)
| ! [X57] : ~ whitebordeaux(X57)
| ! [X58] : ~ whiteburgundy(X58)
| ! [X59] : ~ whiteloire(X59)
| ! [X60] : ~ whitenonsweetwine(X60)
| ! [X61] : ~ whitetablewine(X61)
| ! [X62] : ~ whitewine(X62)
| ! [X63] : ~ wine(X63)
| ! [X64] : ~ winebody(X64)
| ! [X65] : ~ winecolor(X65)
| ! [X66] : ~ winedescriptor(X66)
| ! [X67] : ~ wineflavor(X67)
| ! [X68] : ~ winegrape(X68)
| ! [X69] : ~ winesugar(X69)
| ! [X70] : ~ winery(X70)
| ! [X71] : ~ winetaste(X71)
| ! [X72] : ~ zinfandel(X72)
| ! [X73,X74] : ~ hasbody(X74,X73)
| ! [X75,X76] : ~ hascolor(X76,X75)
| ! [X77,X78] : ~ hasflavor(X78,X77)
| ! [X79,X80] : ~ hasmaker(X80,X79)
| ! [X81,X82] : ~ hassugar(X82,X81)
| ! [X83,X84] : ~ hasvintageyear(X84,X83)
| ! [X85,X86] : ~ haswinedescriptor(X86,X85)
| ! [X87,X88] : ~ locatedin(X88,X87)
| ! [X89,X90] : ~ madefromgrape(X90,X89)
| ! [X91,X92] : ~ madefromfruit(X92,X91)
| ! [X93,X94] : ~ madeintowine(X94,X93)
| ! [X95,X96] : ~ produceswine(X96,X95) ),
inference(ennf_transformation,[],[f1617]) ).
fof(f3085,plain,
hasbody_aux(pulignymontrachetwhiteburgundy,medium),
inference(cnf_transformation,[],[f1]) ).
fof(f3086,plain,
hasbody_aux(formanchardonnay,full),
inference(cnf_transformation,[],[f2]) ).
fof(f3126,plain,
hascolor_aux(selaksicewine,white),
inference(cnf_transformation,[],[f42]) ).
fof(f3127,plain,
hasflavor_aux(pulignymontrachetwhiteburgundy,moderate),
inference(cnf_transformation,[],[f43]) ).
fof(f3128,plain,
hasflavor_aux(formanchardonnay,moderate),
inference(cnf_transformation,[],[f44]) ).
fof(f3138,plain,
hasflavor_aux(bancroftchardonnay,moderate),
inference(cnf_transformation,[],[f54]) ).
fof(f3139,plain,
hasflavor_aux(elysezinfandel,moderate),
inference(cnf_transformation,[],[f55]) ).
fof(f3170,plain,
hasmaker_aux(pulignymontrachetwhiteburgundy,pulignymontrachet),
inference(cnf_transformation,[],[f86]) ).
fof(f3222,plain,
hassugar_aux(pulignymontrachetwhiteburgundy,dry),
inference(cnf_transformation,[],[f138]) ).
fof(f3233,plain,
hassugar_aux(elysezinfandel,dry),
inference(cnf_transformation,[],[f149]) ).
fof(f3262,plain,
locatedin_aux(californiaregion,usregion),
inference(cnf_transformation,[],[f178]) ).
fof(f3265,plain,
locatedin_aux(stgenevievetexaswhite,centraltexasregion),
inference(cnf_transformation,[],[f181]) ).
fof(f3273,plain,
locatedin_aux(bancroftchardonnay,naparegion),
inference(cnf_transformation,[],[f189]) ).
fof(f3275,plain,
locatedin_aux(naparegion,californiaregion),
inference(cnf_transformation,[],[f191]) ).
fof(f3281,plain,
locatedin_aux(centraltexasregion,texasregion),
inference(cnf_transformation,[],[f197]) ).
fof(f3282,plain,
locatedin_aux(schlossrothermeltrochenbierenausleseriesling,germanyregion),
inference(cnf_transformation,[],[f198]) ).
fof(f3315,plain,
locatedin_aux(whitehalllanecabernetfranc,naparegion),
inference(cnf_transformation,[],[f231]) ).
fof(f3330,plain,
ot____nom10_aux(texasregion),
inference(cnf_transformation,[],[f246]) ).
fof(f3332,plain,
ot____nom12_aux(dry),
inference(cnf_transformation,[],[f248]) ).
fof(f3335,plain,
ot____nom15_aux(californiaregion),
inference(cnf_transformation,[],[f251]) ).
fof(f3337,plain,
ot____nom17_aux(germanyregion),
inference(cnf_transformation,[],[f253]) ).
fof(f3364,plain,
ot____nom38_aux(usregion),
inference(cnf_transformation,[],[f280]) ).
fof(f3374,plain,
ot____nom45_aux(full),
inference(cnf_transformation,[],[f290]) ).
fof(f3480,plain,
zinfandel_aux(elysezinfandel),
inference(cnf_transformation,[],[f396]) ).
fof(f3483,plain,
zinfandel_aux(mariettazinfandel),
inference(cnf_transformation,[],[f399]) ).
fof(f3491,plain,
whiteburgundy_aux(pulignymontrachetwhiteburgundy),
inference(cnf_transformation,[],[f407]) ).
fof(f3493,plain,
whitewine_aux(stgenevievetexaswhite),
inference(cnf_transformation,[],[f409]) ).
fof(f3494,plain,
muscadet_aux(sevreetmainemuscadet),
inference(cnf_transformation,[],[f410]) ).
fof(f3495,plain,
meursault_aux(chateaudemeursaultmeursault),
inference(cnf_transformation,[],[f411]) ).
fof(f3496,plain,
meritage_aux(kathrynkennedylateral),
inference(cnf_transformation,[],[f412]) ).
fof(f3497,plain,
margaux_aux(chateaumargaux),
inference(cnf_transformation,[],[f413]) ).
fof(f3498,plain,
icewine_aux(selaksicewine),
inference(cnf_transformation,[],[f414]) ).
fof(f3499,plain,
dryriesling_aux(mountadamriesling),
inference(cnf_transformation,[],[f415]) ).
fof(f3501,plain,
cabernetsauvignon_aux(mariettacabernetsauvignon),
inference(cnf_transformation,[],[f417]) ).
fof(f3505,plain,
cabernetfranc_aux(whitehalllanecabernetfranc),
inference(cnf_transformation,[],[f421]) ).
fof(f3506,plain,
beaujolais_aux(chateaumorgonbeaujolais),
inference(cnf_transformation,[],[f422]) ).
fof(f3507,plain,
anjou_aux(rosedanjou),
inference(cnf_transformation,[],[f423]) ).
fof(f3508,plain,
chardonnay_aux(formanchardonnay),
inference(cnf_transformation,[],[f424]) ).
fof(f3513,plain,
cheninblanc_aux(foxencheninblanc),
inference(cnf_transformation,[],[f429]) ).
fof(f3515,plain,
chianti_aux(chianticlassico),
inference(cnf_transformation,[],[f431]) ).
fof(f3516,plain,
cotesdor_aux(closdevougeotcotesdor),
inference(cnf_transformation,[],[f432]) ).
fof(f3517,plain,
merlot_aux(garyfarrellmerlot),
inference(cnf_transformation,[],[f433]) ).
fof(f3519,plain,
pauillac_aux(chateaulafiterothschildpauillac),
inference(cnf_transformation,[],[f435]) ).
fof(f3520,plain,
petitesyrah_aux(mariettapetitesyrah),
inference(cnf_transformation,[],[f436]) ).
fof(f3522,plain,
pinotnoir_aux(mountadampinotnoir),
inference(cnf_transformation,[],[f438]) ).
fof(f3525,plain,
port_aux(taylorport),
inference(cnf_transformation,[],[f441]) ).
fof(f3564,plain,
sancerre_aux(closdelapoussiesancerre),
inference(cnf_transformation,[],[f480]) ).
fof(f3565,plain,
sauternes_aux(chateaudychemsauterne),
inference(cnf_transformation,[],[f481]) ).
fof(f3566,plain,
sauvignonblanc_aux(corbansprivatebinsauvignonblanc),
inference(cnf_transformation,[],[f482]) ).
fof(f3570,plain,
semillon_aux(congressspringssemillon),
inference(cnf_transformation,[],[f486]) ).
fof(f3572,plain,
stemilion_aux(chateauchevalblancstemilion),
inference(cnf_transformation,[],[f488]) ).
fof(f3573,plain,
sweetriesling_aux(schlossrothermeltrochenbierenausleseriesling),
inference(cnf_transformation,[],[f489]) ).
fof(f3574,plain,
sweetriesling_aux(schlossvolradtrochenbierenausleseriesling),
inference(cnf_transformation,[],[f490]) ).
fof(f3641,plain,
kaon2namedobjects(whitehalllanecabernetfranc),
inference(cnf_transformation,[],[f557]) ).
fof(f3646,plain,
kaon2namedobjects(stgenevievetexaswhite),
inference(cnf_transformation,[],[f562]) ).
fof(f3689,plain,
kaon2namedobjects(chianticlassico),
inference(cnf_transformation,[],[f605]) ).
fof(f3706,plain,
kaon2namedobjects(pulignymontrachetwhiteburgundy),
inference(cnf_transformation,[],[f622]) ).
fof(f3708,plain,
kaon2namedobjects(closdevougeotcotesdor),
inference(cnf_transformation,[],[f624]) ).
fof(f3730,plain,
kaon2namedobjects(sevreetmainemuscadet),
inference(cnf_transformation,[],[f646]) ).
fof(f3736,plain,
vintageyear_aux(year1998),
inference(cnf_transformation,[],[f652]) ).
fof(f3737,plain,
hasvintageyear_aux(saucelitocanyonzinfandel1998,year1998),
inference(cnf_transformation,[],[f653]) ).
fof(f3739,plain,
! [X0,X1] :
( ~ locatedin_aux(X0,X1)
| locatedin(X0,X1) ),
inference(cnf_transformation,[],[f1620]) ).
fof(f3740,plain,
! [X0,X1] :
( ~ hassugar_aux(X0,X1)
| hassugar(X0,X1) ),
inference(cnf_transformation,[],[f1621]) ).
fof(f3741,plain,
! [X0,X1] :
( ~ hasmaker_aux(X0,X1)
| hasmaker(X0,X1) ),
inference(cnf_transformation,[],[f1622]) ).
fof(f3742,plain,
! [X0,X1] :
( ~ hasflavor_aux(X0,X1)
| hasflavor(X0,X1) ),
inference(cnf_transformation,[],[f1623]) ).
fof(f3743,plain,
! [X0,X1] :
( ~ hascolor_aux(X0,X1)
| hascolor(X0,X1) ),
inference(cnf_transformation,[],[f1624]) ).
fof(f3744,plain,
! [X0,X1] :
( ~ hasbody_aux(X0,X1)
| hasbody(X0,X1) ),
inference(cnf_transformation,[],[f1625]) ).
fof(f3745,plain,
! [X0,X1] :
( ~ hasvintageyear_aux(X0,X1)
| hasvintageyear(X0,X1) ),
inference(cnf_transformation,[],[f1626]) ).
fof(f3747,plain,
! [X0] :
( ~ ot____nom10_aux(X0)
| ot____nom10(X0) ),
inference(cnf_transformation,[],[f1628]) ).
fof(f3749,plain,
! [X0] :
( ~ ot____nom12_aux(X0)
| ot____nom12(X0) ),
inference(cnf_transformation,[],[f1630]) ).
fof(f3752,plain,
! [X0] :
( ~ ot____nom15_aux(X0)
| ot____nom15(X0) ),
inference(cnf_transformation,[],[f1633]) ).
fof(f3754,plain,
! [X0] :
( ~ ot____nom17_aux(X0)
| ot____nom17(X0) ),
inference(cnf_transformation,[],[f1635]) ).
fof(f3777,plain,
! [X0] :
( ~ ot____nom38_aux(X0)
| ot____nom38(X0) ),
inference(cnf_transformation,[],[f1658]) ).
fof(f3785,plain,
! [X0] :
( ~ ot____nom45_aux(X0)
| ot____nom45(X0) ),
inference(cnf_transformation,[],[f1666]) ).
fof(f3810,plain,
! [X0] :
( ~ zinfandel_aux(X0)
| zinfandel(X0) ),
inference(cnf_transformation,[],[f1691]) ).
fof(f3815,plain,
! [X0] :
( ~ anjou_aux(X0)
| anjou(X0) ),
inference(cnf_transformation,[],[f1696]) ).
fof(f3816,plain,
! [X0] :
( ~ beaujolais_aux(X0)
| beaujolais(X0) ),
inference(cnf_transformation,[],[f1697]) ).
fof(f3817,plain,
! [X0] :
( ~ cabernetfranc_aux(X0)
| cabernetfranc(X0) ),
inference(cnf_transformation,[],[f1698]) ).
fof(f3818,plain,
! [X0] :
( ~ cabernetsauvignon_aux(X0)
| cabernetsauvignon(X0) ),
inference(cnf_transformation,[],[f1699]) ).
fof(f3819,plain,
! [X0] :
( ~ chardonnay_aux(X0)
| chardonnay(X0) ),
inference(cnf_transformation,[],[f1700]) ).
fof(f3820,plain,
! [X0] :
( ~ cheninblanc_aux(X0)
| cheninblanc(X0) ),
inference(cnf_transformation,[],[f1701]) ).
fof(f3821,plain,
! [X0] :
( ~ chianti_aux(X0)
| chianti(X0) ),
inference(cnf_transformation,[],[f1702]) ).
fof(f3822,plain,
! [X0] :
( ~ cotesdor_aux(X0)
| cotesdor(X0) ),
inference(cnf_transformation,[],[f1703]) ).
fof(f3824,plain,
! [X0] :
( ~ dryriesling_aux(X0)
| dryriesling(X0) ),
inference(cnf_transformation,[],[f1705]) ).
fof(f3825,plain,
! [X0] :
( ~ icewine_aux(X0)
| icewine(X0) ),
inference(cnf_transformation,[],[f1706]) ).
fof(f3826,plain,
! [X0] :
( ~ margaux_aux(X0)
| margaux(X0) ),
inference(cnf_transformation,[],[f1707]) ).
fof(f3827,plain,
! [X0] :
( ~ meritage_aux(X0)
| meritage(X0) ),
inference(cnf_transformation,[],[f1708]) ).
fof(f3828,plain,
! [X0] :
( ~ merlot_aux(X0)
| merlot(X0) ),
inference(cnf_transformation,[],[f1709]) ).
fof(f3829,plain,
! [X0] :
( ~ meursault_aux(X0)
| meursault(X0) ),
inference(cnf_transformation,[],[f1710]) ).
fof(f3830,plain,
! [X0] :
( ~ muscadet_aux(X0)
| muscadet(X0) ),
inference(cnf_transformation,[],[f1711]) ).
fof(f3831,plain,
! [X0] :
( ~ pauillac_aux(X0)
| pauillac(X0) ),
inference(cnf_transformation,[],[f1712]) ).
fof(f3832,plain,
! [X0] :
( ~ petitesyrah_aux(X0)
| petitesyrah(X0) ),
inference(cnf_transformation,[],[f1713]) ).
fof(f3833,plain,
! [X0] :
( ~ pinotnoir_aux(X0)
| pinotnoir(X0) ),
inference(cnf_transformation,[],[f1714]) ).
fof(f3834,plain,
! [X0] :
( ~ port_aux(X0)
| port(X0) ),
inference(cnf_transformation,[],[f1715]) ).
fof(f3838,plain,
! [X0] :
( ~ sancerre_aux(X0)
| sancerre(X0) ),
inference(cnf_transformation,[],[f1719]) ).
fof(f3839,plain,
! [X0] :
( ~ sauternes_aux(X0)
| sauternes(X0) ),
inference(cnf_transformation,[],[f1720]) ).
fof(f3840,plain,
! [X0] :
( ~ sauvignonblanc_aux(X0)
| sauvignonblanc(X0) ),
inference(cnf_transformation,[],[f1721]) ).
fof(f3841,plain,
! [X0] :
( ~ semillon_aux(X0)
| semillon(X0) ),
inference(cnf_transformation,[],[f1722]) ).
fof(f3842,plain,
! [X0] :
( ~ stemilion_aux(X0)
| stemilion(X0) ),
inference(cnf_transformation,[],[f1723]) ).
fof(f3843,plain,
! [X0] :
( ~ sweetriesling_aux(X0)
| sweetriesling(X0) ),
inference(cnf_transformation,[],[f1724]) ).
fof(f3844,plain,
! [X0] :
( ~ vintageyear_aux(X0)
| vintageyear(X0) ),
inference(cnf_transformation,[],[f1725]) ).
fof(f3845,plain,
! [X0] :
( ~ whiteburgundy_aux(X0)
| whiteburgundy(X0) ),
inference(cnf_transformation,[],[f1726]) ).
fof(f3846,plain,
! [X0] :
( ~ whitewine_aux(X0)
| whitewine(X0) ),
inference(cnf_transformation,[],[f1727]) ).
fof(f3854,plain,
! [X0] :
( ~ zinfandel(X0)
| q0(X0) ),
inference(cnf_transformation,[],[f1735]) ).
fof(f3855,plain,
! [X0] :
( ~ medoc(X0)
| q0(X0) ),
inference(cnf_transformation,[],[f1736]) ).
fof(f3877,plain,
! [X0] :
( ~ pinotblanc(X0)
| q12(X0) ),
inference(cnf_transformation,[],[f1764]) ).
fof(f3878,plain,
! [X0] :
( ~ whitewine(X0)
| q12(X0) ),
inference(cnf_transformation,[],[f1765]) ).
fof(f3880,plain,
! [X0] :
( ~ sauternes(X0)
| q12(X0) ),
inference(cnf_transformation,[],[f1767]) ).
fof(f3888,plain,
! [X0] :
( ~ beaujolais(X0)
| q14(X0) ),
inference(cnf_transformation,[],[f1777]) ).
fof(f3890,plain,
! [X0] :
( ~ anjou(X0)
| q15(X0) ),
inference(cnf_transformation,[],[f1780]) ).
fof(f3915,plain,
! [X0] :
( ~ q12(X0)
| q21(X0) ),
inference(cnf_transformation,[],[f1817]) ).
fof(f3916,plain,
! [X0,X1] :
( ~ hascolor(X0,X1)
| q21(X0)
| ~ ot____nom5(X1) ),
inference(cnf_transformation,[],[f1819]) ).
fof(f3925,plain,
! [X0] :
( ~ muscadet(X0)
| q24(X0) ),
inference(cnf_transformation,[],[f1833]) ).
fof(f3928,plain,
! [X0,X1] :
( ~ locatedin(X0,X1)
| q26(X0)
| ~ q27(X1) ),
inference(cnf_transformation,[],[f1838]) ).
fof(f3930,plain,
! [X0] :
( ~ q26(X0)
| q27(X0) ),
inference(cnf_transformation,[],[f1841]) ).
fof(f3931,plain,
! [X0,X1] :
( ~ locatedin(X0,X1)
| q27(X0)
| ~ ot____nom38(X1) ),
inference(cnf_transformation,[],[f1843]) ).
fof(f3973,plain,
! [X0] :
( ~ burgundy(X0)
| q31(X0) ),
inference(cnf_transformation,[],[f1892]) ).
fof(f4013,plain,
! [X0] :
( ~ q0(X0)
| q41(X0) ),
inference(cnf_transformation,[],[f1949]) ).
fof(f4030,plain,
! [X0,X1] :
( ~ hassugar(X0,X1)
| q46(X0)
| ~ ot____nom12(X1) ),
inference(cnf_transformation,[],[f1975]) ).
fof(f4033,plain,
! [X0,X1] :
( ~ locatedin(X0,X1)
| q47(X0)
| ~ q48(X1) ),
inference(cnf_transformation,[],[f1980]) ).
fof(f4035,plain,
! [X0] :
( ~ q47(X0)
| q48(X0) ),
inference(cnf_transformation,[],[f1983]) ).
fof(f4036,plain,
! [X0,X1] :
( ~ locatedin(X0,X1)
| q48(X0)
| ~ ot____nom15(X1) ),
inference(cnf_transformation,[],[f1985]) ).
fof(f4065,plain,
! [X0,X1] :
( ~ locatedin(X0,X1)
| q50(X0)
| ~ ot____nom17(X1) ),
inference(cnf_transformation,[],[f2033]) ).
fof(f4129,plain,
! [X0] :
( ~ lateharvest(X0)
| q70(X0) ),
inference(cnf_transformation,[],[f2131]) ).
fof(f4131,plain,
! [X0] :
( ~ q70(X0)
| q71(X0) ),
inference(cnf_transformation,[],[f2134]) ).
fof(f4138,plain,
! [X0,X1] :
( ~ locatedin(X0,X1)
| q73(X0)
| ~ q74(X1) ),
inference(cnf_transformation,[],[f2145]) ).
fof(f4140,plain,
! [X0] :
( ~ q73(X0)
| q74(X0) ),
inference(cnf_transformation,[],[f2148]) ).
fof(f4141,plain,
! [X0,X1] :
( ~ locatedin(X0,X1)
| q74(X0)
| ~ ot____nom10(X1) ),
inference(cnf_transformation,[],[f2150]) ).
fof(f4148,plain,
! [X0] :
( ~ wine(X0)
| ~ q27(X0)
| americanwine(X0) ),
inference(cnf_transformation,[],[f2163]) ).
fof(f4154,plain,
! [X0] :
( ~ sauternes(X0)
| bordeaux(X0) ),
inference(cnf_transformation,[],[f2174]) ).
fof(f4155,plain,
! [X0] :
( ~ medoc(X0)
| bordeaux(X0) ),
inference(cnf_transformation,[],[f2175]) ).
fof(f4161,plain,
! [X0] :
( ~ whiteburgundy(X0)
| burgundy(X0) ),
inference(cnf_transformation,[],[f2183]) ).
fof(f4162,plain,
! [X0] :
( ~ redburgundy(X0)
| burgundy(X0) ),
inference(cnf_transformation,[],[f2184]) ).
fof(f4170,plain,
! [X0] :
( ~ q48(X0)
| californiawine(X0)
| ~ wine(X0) ),
inference(cnf_transformation,[],[f2199]) ).
fof(f4182,plain,
! [X0] :
( ~ icewine(X0)
| dessertwine(X0) ),
inference(cnf_transformation,[],[f2219]) ).
fof(f4184,plain,
! [X0] :
( ~ drywine(X0)
| dryredwine(X0)
| ~ redwine(X0) ),
inference(cnf_transformation,[],[f2223]) ).
fof(f4188,plain,
! [X0] :
( ~ drywine(X0)
| drywhitewine(X0)
| ~ whitewine(X0) ),
inference(cnf_transformation,[],[f2231]) ).
fof(f4192,plain,
! [X0] :
( ~ q46(X0)
| drywine(X0)
| ~ wine(X0) ),
inference(cnf_transformation,[],[f2237]) ).
fof(f4199,plain,
! [X0,X1] :
( ~ hasbody(X0,X1)
| ~ wine(X0)
| fullbodiedwine(X0)
| ~ ot____nom45(X1) ),
inference(cnf_transformation,[],[f2250]) ).
fof(f4200,plain,
! [X0] :
( ~ q14(X0)
| gamay(X0) ),
inference(cnf_transformation,[],[f2251]) ).
fof(f4203,plain,
! [X0] :
( ~ q50(X0)
| germanwine(X0)
| ~ wine(X0) ),
inference(cnf_transformation,[],[f2257]) ).
fof(f4205,plain,
! [X0] :
( ~ winegrape(X0)
| grape(X0) ),
inference(cnf_transformation,[],[f2260]) ).
fof(f4209,plain,
! [X0] :
( ~ chianti(X0)
| italianwine(X0) ),
inference(cnf_transformation,[],[f2267]) ).
fof(f4212,plain,
! [X0] :
( ~ icewine(X0)
| lateharvest(X0) ),
inference(cnf_transformation,[],[f2272]) ).
fof(f4219,plain,
! [X0] :
( ~ muscadet(X0)
| loire(X0) ),
inference(cnf_transformation,[],[f2280]) ).
fof(f4224,plain,
! [X0] :
( ~ pauillac(X0)
| medoc(X0) ),
inference(cnf_transformation,[],[f2289]) ).
fof(f4225,plain,
! [X0] :
( ~ margaux(X0)
| medoc(X0) ),
inference(cnf_transformation,[],[f2290]) ).
fof(f4241,plain,
! [X0] :
( ~ q24(X0)
| pinotblanc(X0) ),
inference(cnf_transformation,[],[f2320]) ).
fof(f4248,plain,
! [X0] :
( ~ wine(X0)
| potableliquid(X0) ),
inference(cnf_transformation,[],[f2332]) ).
fof(f4250,plain,
! [X0] :
( ~ bordeaux(X0)
| ~ redwine(X0)
| redbordeaux(X0) ),
inference(cnf_transformation,[],[f2336]) ).
fof(f4252,plain,
! [X0] :
( ~ cotesdor(X0)
| redburgundy(X0) ),
inference(cnf_transformation,[],[f2339]) ).
fof(f4255,plain,
! [X0] :
( ~ q41(X0)
| redtablewine(X0)
| ~ tablewine(X0) ),
inference(cnf_transformation,[],[f2345]) ).
fof(f4257,plain,
! [X0] :
( ~ redburgundy(X0)
| redwine(X0) ),
inference(cnf_transformation,[],[f2348]) ).
fof(f4260,plain,
! [X0] :
( ~ port(X0)
| redwine(X0) ),
inference(cnf_transformation,[],[f2351]) ).
fof(f4261,plain,
! [X0] :
( ~ q41(X0)
| redwine(X0)
| ~ wine(X0) ),
inference(cnf_transformation,[],[f2353]) ).
fof(f4266,plain,
! [X0] :
( ~ wine(X0)
| region(X0)
| ~ kaon2namedobjects(X0) ),
inference(cnf_transformation,[],[f2360]) ).
fof(f4269,plain,
! [X0] :
( ~ sweetriesling(X0)
| riesling(X0) ),
inference(cnf_transformation,[],[f2364]) ).
fof(f4272,plain,
! [X0] :
( ~ q15(X0)
| rosewine(X0) ),
inference(cnf_transformation,[],[f2369]) ).
fof(f4284,plain,
! [X0] :
( ~ sauvignonblanc(X0)
| semillonorsauvignonblanc(X0) ),
inference(cnf_transformation,[],[f2391]) ).
fof(f4292,plain,
! [X0] :
( ~ q71(X0)
| sweetwine(X0)
| ~ wine(X0) ),
inference(cnf_transformation,[],[f2407]) ).
fof(f4296,plain,
! [X0] :
( ~ q46(X0)
| tablewine(X0)
| ~ wine(X0) ),
inference(cnf_transformation,[],[f2413]) ).
fof(f4298,plain,
! [X0] :
( ~ q74(X0)
| texaswine(X0)
| ~ wine(X0) ),
inference(cnf_transformation,[],[f2417]) ).
fof(f4302,plain,
! [X0,X1] :
( ~ hasvintageyear(X0,X1)
| vintage(X0) ),
inference(cnf_transformation,[],[f2424]) ).
fof(f4306,plain,
! [X0] :
( ~ bordeaux(X0)
| whitebordeaux(X0)
| ~ whitewine(X0) ),
inference(cnf_transformation,[],[f2431]) ).
fof(f4308,plain,
! [X0] :
( ~ meursault(X0)
| whiteburgundy(X0) ),
inference(cnf_transformation,[],[f2434]) ).
fof(f4311,plain,
! [X0] :
( ~ loire(X0)
| whiteloire(X0)
| ~ whitewine(X0) ),
inference(cnf_transformation,[],[f2440]) ).
fof(f4313,plain,
! [X0] :
( ~ whitewine(X0)
| whitenonsweetwine(X0)
| ~ kaon2namedobjects(X0) ),
inference(cnf_transformation,[],[f2444]) ).
fof(f4317,plain,
! [X0] :
( ~ tablewine(X0)
| ~ q21(X0)
| whitetablewine(X0) ),
inference(cnf_transformation,[],[f2452]) ).
fof(f4320,plain,
! [X0] :
( ~ whiteburgundy(X0)
| whitewine(X0) ),
inference(cnf_transformation,[],[f2456]) ).
fof(f4324,plain,
! [X0] :
( ~ wine(X0)
| ~ q21(X0)
| whitewine(X0) ),
inference(cnf_transformation,[],[f2461]) ).
fof(f4331,plain,
! [X0,X1] :
( ~ haswinedescriptor(X0,X1)
| wine(X0) ),
inference(cnf_transformation,[],[f2469]) ).
fof(f4341,plain,
! [X0] :
( ~ cabernetfranc(X0)
| wine(X0) ),
inference(cnf_transformation,[],[f2479]) ).
fof(f4345,plain,
! [X0] :
( ~ loire(X0)
| wine(X0) ),
inference(cnf_transformation,[],[f2483]) ).
fof(f4359,plain,
! [X0] :
( ~ bordeaux(X0)
| wine(X0) ),
inference(cnf_transformation,[],[f2497]) ).
fof(f4360,plain,
! [X0] :
( ~ riesling(X0)
| wine(X0) ),
inference(cnf_transformation,[],[f2498]) ).
fof(f4363,plain,
! [X0] :
( ~ whitewine(X0)
| wine(X0) ),
inference(cnf_transformation,[],[f2501]) ).
fof(f4370,plain,
! [X0] :
( ~ burgundy(X0)
| wine(X0) ),
inference(cnf_transformation,[],[f2508]) ).
fof(f4381,plain,
! [X0] :
( ~ lateharvest(X0)
| wine(X0) ),
inference(cnf_transformation,[],[f2519]) ).
fof(f4385,plain,
! [X0,X1] :
( ~ hasbody(X0,X1)
| winebody(X1) ),
inference(cnf_transformation,[],[f2524]) ).
fof(f4388,plain,
! [X0,X1] :
( ~ hascolor(X0,X1)
| winecolor(X1) ),
inference(cnf_transformation,[],[f2528]) ).
fof(f4391,plain,
! [X0] :
( ~ winecolor(X0)
| winedescriptor(X0) ),
inference(cnf_transformation,[],[f2532]) ).
fof(f4395,plain,
! [X0,X1] :
( ~ hasflavor(X0,X1)
| wineflavor(X1) ),
inference(cnf_transformation,[],[f2537]) ).
fof(f4398,plain,
! [X0,X1] :
( ~ madefromgrape(X0,X1)
| winegrape(X1) ),
inference(cnf_transformation,[],[f2541]) ).
fof(f4401,plain,
! [X0,X1] :
( ~ hassugar(X0,X1)
| winesugar(X1) ),
inference(cnf_transformation,[],[f2545]) ).
fof(f4403,plain,
! [X0] :
( ~ wineflavor(X0)
| winetaste(X0) ),
inference(cnf_transformation,[],[f2548]) ).
fof(f4408,plain,
! [X0,X1] :
( ~ hasmaker(X0,X1)
| ~ wine(X0)
| winery(X1) ),
inference(cnf_transformation,[],[f2555]) ).
fof(f4418,plain,
! [X0] :
( ~ q31(X0)
| ot____nom12(X0)
| ~ kaon2namedobjects(X0) ),
inference(cnf_transformation,[],[f2575]) ).
fof(f4500,plain,
! [X0] :
( ~ q12(X0)
| ot____nom5(X0)
| ~ kaon2namedobjects(X0) ),
inference(cnf_transformation,[],[f2736]) ).
fof(f4558,plain,
! [X0] :
( hasbody(X0,X0)
| ~ wine(X0)
| ~ kaon2namedobjects(X0) ),
inference(cnf_transformation,[],[f2850]) ).
fof(f4565,plain,
! [X0] :
( hascolor(X0,X0)
| ~ wine(X0)
| ~ kaon2namedobjects(X0) ),
inference(cnf_transformation,[],[f2864]) ).
fof(f4572,plain,
! [X0] :
( hasflavor(X0,X0)
| ~ wine(X0)
| ~ kaon2namedobjects(X0) ),
inference(cnf_transformation,[],[f2878]) ).
fof(f4576,plain,
! [X0] :
( hasmaker(X0,X0)
| ~ wine(X0)
| ~ kaon2namedobjects(X0) ),
inference(cnf_transformation,[],[f2885]) ).
fof(f4579,plain,
! [X0] :
( hassugar(X0,X0)
| ~ wine(X0)
| ~ kaon2namedobjects(X0) ),
inference(cnf_transformation,[],[f2891]) ).
fof(f4581,plain,
! [X0] :
( hassugar(X0,X0)
| ~ whitewine(X0)
| ~ kaon2namedobjects(X0) ),
inference(cnf_transformation,[],[f2895]) ).
fof(f4591,plain,
! [X0,X1] :
( ~ hasflavor(X0,X1)
| haswinedescriptor(X0,X1) ),
inference(cnf_transformation,[],[f2912]) ).
fof(f4592,plain,
! [X0,X1] :
( ~ hassugar(X0,X1)
| haswinedescriptor(X0,X1) ),
inference(cnf_transformation,[],[f2913]) ).
fof(f4606,plain,
! [X0] :
( locatedin(X0,X0)
| ~ chianti(X0)
| ~ kaon2namedobjects(X0) ),
inference(cnf_transformation,[],[f2941]) ).
fof(f4624,plain,
! [X0,X1] :
( ~ madefromgrape(X0,X1)
| madefromfruit(X0,X1) ),
inference(cnf_transformation,[],[f2976]) ).
fof(f4629,plain,
! [X0] :
( madefromgrape(X0,X0)
| ~ wine(X0)
| ~ kaon2namedobjects(X0) ),
inference(cnf_transformation,[],[f2985]) ).
fof(f4641,plain,
! [X0] :
( madefromgrape(X0,X0)
| ~ cabernetfranc(X0)
| ~ kaon2namedobjects(X0) ),
inference(cnf_transformation,[],[f3009]) ).
fof(f4647,plain,
! [X0,X1] :
( ~ madefromgrape(X0,X1)
| madeintowine(X1,X0) ),
inference(cnf_transformation,[],[f3020]) ).
fof(f4650,plain,
! [X0,X1] :
( ~ hasmaker(X0,X1)
| produceswine(X1,X0) ),
inference(cnf_transformation,[],[f3025]) ).
fof(f4698,plain,
! [X2,X21,X28,X39,X46,X49,X65,X72,X83,X90,X56,X6,X9,X16,X27,X69,X76,X87,X94,X34,X53,X60,X13,X20,X64,X75,X31,X38,X41,X48,X59,X82,X1,X8,X19,X26,X45,X52,X68,X79,X86,X89,X63,X96,X5,X12,X23,X30,X33,X67,X74,X93,X40,X51,X58,X0,X11,X71,X78,X18,X37,X44,X55,X62,X81,X4,X88,X15,X22,X25,X32,X43,X66,X85,X92,X50,X3,X10,X29,X36,X70,X73,X80,X91,X47,X54,X57,X7,X14,X77,X84,X17,X24,X35,X42,X61,X95] :
( ~ californiawine(X0)
| ~ americanwine(X1)
| ~ bordeaux(X2)
| ~ burgundy(X3)
| ~ anjou(X4)
| ~ beaujolais(X5)
| ~ cabernetfranc(X6)
| ~ cabernetsauvignon(X7)
| ~ californiawine(X8)
| ~ chardonnay(X9)
| ~ cheninblanc(X10)
| ~ chianti(X11)
| ~ cotesdor(X12)
| ~ dessertwine(X13)
| ~ dryriesling(X14)
| ~ dryredwine(X15)
| ~ drywhitewine(X16)
| ~ drywine(X17)
| ~ fullbodiedwine(X18)
| ~ gamay(X19)
| ~ germanwine(X20)
| ~ grape(X21)
| ~ icewine(X22)
| ~ italianwine(X23)
| ~ lateharvest(X24)
| ~ loire(X25)
| ~ margaux(X26)
| ~ medoc(X27)
| ~ meritage(X28)
| ~ merlot(X29)
| ~ meursault(X30)
| ~ muscadet(X31)
| ~ pauillac(X32)
| ~ petitesyrah(X33)
| ~ pinotblanc(X34)
| ~ pinotnoir(X35)
| ~ port(X36)
| ~ potableliquid(X37)
| ~ redbordeaux(X38)
| ~ redburgundy(X39)
| ~ redtablewine(X40)
| ~ redwine(X41)
| ~ region(X42)
| ~ riesling(X43)
| ~ rosewine(X44)
| ~ sancerre(X45)
| ~ sauternes(X46)
| ~ sauvignonblanc(X47)
| ~ semillon(X48)
| ~ semillonorsauvignonblanc(X49)
| ~ stemilion(X50)
| ~ sweetriesling(X51)
| ~ sweetwine(X52)
| ~ tablewine(X53)
| ~ texaswine(X54)
| ~ vintage(X55)
| ~ vintageyear(X56)
| ~ whitebordeaux(X57)
| ~ whiteburgundy(X58)
| ~ whiteloire(X59)
| ~ whitenonsweetwine(X60)
| ~ whitetablewine(X61)
| ~ whitewine(X62)
| ~ wine(X63)
| ~ winebody(X64)
| ~ winecolor(X65)
| ~ winedescriptor(X66)
| ~ wineflavor(X67)
| ~ winegrape(X68)
| ~ winesugar(X69)
| ~ winery(X70)
| ~ winetaste(X71)
| ~ zinfandel(X72)
| ~ hasbody(X74,X73)
| ~ hascolor(X76,X75)
| ~ hasflavor(X78,X77)
| ~ hasmaker(X80,X79)
| ~ hassugar(X82,X81)
| ~ hasvintageyear(X84,X83)
| ~ haswinedescriptor(X86,X85)
| ~ locatedin(X88,X87)
| ~ madefromgrape(X90,X89)
| ~ madefromfruit(X92,X91)
| ~ madeintowine(X94,X93)
| ~ produceswine(X96,X95) ),
inference(cnf_transformation,[],[f3084]) ).
fof(f4700,definition,
( spl0_1
<=> ! [X96,X95] : ~ produceswine(X96,X95) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f4701,plain,
( ! [X96,X95] : ~ produceswine(X96,X95)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f4700]) ).
fof(f4703,definition,
( spl0_2
<=> ! [X93,X94] : ~ madeintowine(X94,X93) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f4704,plain,
( ! [X94,X93] : ~ madeintowine(X94,X93)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f4703]) ).
fof(f4706,definition,
( spl0_3
<=> ! [X91,X92] : ~ madefromfruit(X92,X91) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f4707,plain,
( ! [X91,X92] : ~ madefromfruit(X92,X91)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f4706]) ).
fof(f4709,definition,
( spl0_4
<=> ! [X89,X90] : ~ madefromgrape(X90,X89) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f4710,plain,
( ! [X90,X89] : ~ madefromgrape(X90,X89)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f4709]) ).
fof(f4712,definition,
( spl0_5
<=> ! [X88,X87] : ~ locatedin(X88,X87) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f4713,plain,
( ! [X88,X87] : ~ locatedin(X88,X87)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f4712]) ).
fof(f4715,definition,
( spl0_6
<=> ! [X86,X85] : ~ haswinedescriptor(X86,X85) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f4716,plain,
( ! [X86,X85] : ~ haswinedescriptor(X86,X85)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f4715]) ).
fof(f4718,definition,
( spl0_7
<=> ! [X84,X83] : ~ hasvintageyear(X84,X83) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f4719,plain,
( ! [X83,X84] : ~ hasvintageyear(X84,X83)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f4718]) ).
fof(f4721,definition,
( spl0_8
<=> ! [X82,X81] : ~ hassugar(X82,X81) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f4722,plain,
( ! [X82,X81] : ~ hassugar(X82,X81)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f4721]) ).
fof(f4724,definition,
( spl0_9
<=> ! [X80,X79] : ~ hasmaker(X80,X79) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f4725,plain,
( ! [X80,X79] : ~ hasmaker(X80,X79)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f4724]) ).
fof(f4727,definition,
( spl0_10
<=> ! [X77,X78] : ~ hasflavor(X78,X77) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f4728,plain,
( ! [X78,X77] : ~ hasflavor(X78,X77)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f4727]) ).
fof(f4730,definition,
( spl0_11
<=> ! [X76,X75] : ~ hascolor(X76,X75) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f4731,plain,
( ! [X76,X75] : ~ hascolor(X76,X75)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f4730]) ).
fof(f4733,definition,
( spl0_12
<=> ! [X73,X74] : ~ hasbody(X74,X73) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f4734,plain,
( ! [X73,X74] : ~ hasbody(X74,X73)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f4733]) ).
fof(f4736,definition,
( spl0_13
<=> ! [X72] : ~ zinfandel(X72) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f4737,plain,
( ! [X72] : ~ zinfandel(X72)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f4736]) ).
fof(f4739,definition,
( spl0_14
<=> ! [X71] : ~ winetaste(X71) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f4740,plain,
( ! [X71] : ~ winetaste(X71)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f4739]) ).
fof(f4742,definition,
( spl0_15
<=> ! [X70] : ~ winery(X70) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f4743,plain,
( ! [X70] : ~ winery(X70)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f4742]) ).
fof(f4745,definition,
( spl0_16
<=> ! [X69] : ~ winesugar(X69) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f4746,plain,
( ! [X69] : ~ winesugar(X69)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f4745]) ).
fof(f4748,definition,
( spl0_17
<=> ! [X68] : ~ winegrape(X68) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f4749,plain,
( ! [X68] : ~ winegrape(X68)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f4748]) ).
fof(f4751,definition,
( spl0_18
<=> ! [X67] : ~ wineflavor(X67) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f4752,plain,
( ! [X67] : ~ wineflavor(X67)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f4751]) ).
fof(f4754,definition,
( spl0_19
<=> ! [X66] : ~ winedescriptor(X66) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f4755,plain,
( ! [X66] : ~ winedescriptor(X66)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f4754]) ).
fof(f4757,definition,
( spl0_20
<=> ! [X65] : ~ winecolor(X65) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f4758,plain,
( ! [X65] : ~ winecolor(X65)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f4757]) ).
fof(f4760,definition,
( spl0_21
<=> ! [X64] : ~ winebody(X64) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f4761,plain,
( ! [X64] : ~ winebody(X64)
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f4760]) ).
fof(f4763,definition,
( spl0_22
<=> ! [X63] : ~ wine(X63) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f4764,plain,
( ! [X63] : ~ wine(X63)
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f4763]) ).
fof(f4766,definition,
( spl0_23
<=> ! [X62] : ~ whitewine(X62) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f4767,plain,
( ! [X62] : ~ whitewine(X62)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f4766]) ).
fof(f4769,definition,
( spl0_24
<=> ! [X61] : ~ whitetablewine(X61) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f4770,plain,
( ! [X61] : ~ whitetablewine(X61)
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f4769]) ).
fof(f4772,definition,
( spl0_25
<=> ! [X60] : ~ whitenonsweetwine(X60) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f4773,plain,
( ! [X60] : ~ whitenonsweetwine(X60)
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f4772]) ).
fof(f4775,definition,
( spl0_26
<=> ! [X59] : ~ whiteloire(X59) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f4776,plain,
( ! [X59] : ~ whiteloire(X59)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f4775]) ).
fof(f4778,definition,
( spl0_27
<=> ! [X58] : ~ whiteburgundy(X58) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f4779,plain,
( ! [X58] : ~ whiteburgundy(X58)
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f4778]) ).
fof(f4781,definition,
( spl0_28
<=> ! [X57] : ~ whitebordeaux(X57) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f4782,plain,
( ! [X57] : ~ whitebordeaux(X57)
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f4781]) ).
fof(f4784,definition,
( spl0_29
<=> ! [X56] : ~ vintageyear(X56) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f4785,plain,
( ! [X56] : ~ vintageyear(X56)
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f4784]) ).
fof(f4787,definition,
( spl0_30
<=> ! [X55] : ~ vintage(X55) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f4788,plain,
( ! [X55] : ~ vintage(X55)
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f4787]) ).
fof(f4790,definition,
( spl0_31
<=> ! [X54] : ~ texaswine(X54) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f4791,plain,
( ! [X54] : ~ texaswine(X54)
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f4790]) ).
fof(f4793,definition,
( spl0_32
<=> ! [X53] : ~ tablewine(X53) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f4794,plain,
( ! [X53] : ~ tablewine(X53)
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f4793]) ).
fof(f4796,definition,
( spl0_33
<=> ! [X52] : ~ sweetwine(X52) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f4797,plain,
( ! [X52] : ~ sweetwine(X52)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f4796]) ).
fof(f4799,definition,
( spl0_34
<=> ! [X51] : ~ sweetriesling(X51) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f4800,plain,
( ! [X51] : ~ sweetriesling(X51)
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f4799]) ).
fof(f4802,definition,
( spl0_35
<=> ! [X50] : ~ stemilion(X50) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f4803,plain,
( ! [X50] : ~ stemilion(X50)
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f4802]) ).
fof(f4805,definition,
( spl0_36
<=> ! [X49] : ~ semillonorsauvignonblanc(X49) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f4806,plain,
( ! [X49] : ~ semillonorsauvignonblanc(X49)
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f4805]) ).
fof(f4808,definition,
( spl0_37
<=> ! [X48] : ~ semillon(X48) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f4809,plain,
( ! [X48] : ~ semillon(X48)
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f4808]) ).
fof(f4811,definition,
( spl0_38
<=> ! [X47] : ~ sauvignonblanc(X47) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f4812,plain,
( ! [X47] : ~ sauvignonblanc(X47)
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f4811]) ).
fof(f4814,definition,
( spl0_39
<=> ! [X46] : ~ sauternes(X46) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f4815,plain,
( ! [X46] : ~ sauternes(X46)
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f4814]) ).
fof(f4817,definition,
( spl0_40
<=> ! [X45] : ~ sancerre(X45) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f4818,plain,
( ! [X45] : ~ sancerre(X45)
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f4817]) ).
fof(f4820,definition,
( spl0_41
<=> ! [X44] : ~ rosewine(X44) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f4821,plain,
( ! [X44] : ~ rosewine(X44)
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f4820]) ).
fof(f4823,definition,
( spl0_42
<=> ! [X43] : ~ riesling(X43) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f4824,plain,
( ! [X43] : ~ riesling(X43)
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f4823]) ).
fof(f4826,definition,
( spl0_43
<=> ! [X42] : ~ region(X42) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f4827,plain,
( ! [X42] : ~ region(X42)
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f4826]) ).
fof(f4829,definition,
( spl0_44
<=> ! [X41] : ~ redwine(X41) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f4830,plain,
( ! [X41] : ~ redwine(X41)
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f4829]) ).
fof(f4832,definition,
( spl0_45
<=> ! [X40] : ~ redtablewine(X40) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f4833,plain,
( ! [X40] : ~ redtablewine(X40)
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f4832]) ).
fof(f4835,definition,
( spl0_46
<=> ! [X39] : ~ redburgundy(X39) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f4836,plain,
( ! [X39] : ~ redburgundy(X39)
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f4835]) ).
fof(f4838,definition,
( spl0_47
<=> ! [X38] : ~ redbordeaux(X38) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f4839,plain,
( ! [X38] : ~ redbordeaux(X38)
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f4838]) ).
fof(f4841,definition,
( spl0_48
<=> ! [X37] : ~ potableliquid(X37) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f4842,plain,
( ! [X37] : ~ potableliquid(X37)
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f4841]) ).
fof(f4844,definition,
( spl0_49
<=> ! [X36] : ~ port(X36) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f4845,plain,
( ! [X36] : ~ port(X36)
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f4844]) ).
fof(f4847,definition,
( spl0_50
<=> ! [X35] : ~ pinotnoir(X35) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f4848,plain,
( ! [X35] : ~ pinotnoir(X35)
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f4847]) ).
fof(f4850,definition,
( spl0_51
<=> ! [X34] : ~ pinotblanc(X34) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f4851,plain,
( ! [X34] : ~ pinotblanc(X34)
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f4850]) ).
fof(f4853,definition,
( spl0_52
<=> ! [X33] : ~ petitesyrah(X33) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f4854,plain,
( ! [X33] : ~ petitesyrah(X33)
| ~ spl0_52 ),
inference(avatar_component_clause,[],[f4853]) ).
fof(f4856,definition,
( spl0_53
<=> ! [X32] : ~ pauillac(X32) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f4857,plain,
( ! [X32] : ~ pauillac(X32)
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f4856]) ).
fof(f4859,definition,
( spl0_54
<=> ! [X31] : ~ muscadet(X31) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f4860,plain,
( ! [X31] : ~ muscadet(X31)
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f4859]) ).
fof(f4862,definition,
( spl0_55
<=> ! [X30] : ~ meursault(X30) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f4863,plain,
( ! [X30] : ~ meursault(X30)
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f4862]) ).
fof(f4865,definition,
( spl0_56
<=> ! [X29] : ~ merlot(X29) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f4866,plain,
( ! [X29] : ~ merlot(X29)
| ~ spl0_56 ),
inference(avatar_component_clause,[],[f4865]) ).
fof(f4868,definition,
( spl0_57
<=> ! [X28] : ~ meritage(X28) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f4869,plain,
( ! [X28] : ~ meritage(X28)
| ~ spl0_57 ),
inference(avatar_component_clause,[],[f4868]) ).
fof(f4871,definition,
( spl0_58
<=> ! [X27] : ~ medoc(X27) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f4872,plain,
( ! [X27] : ~ medoc(X27)
| ~ spl0_58 ),
inference(avatar_component_clause,[],[f4871]) ).
fof(f4874,definition,
( spl0_59
<=> ! [X26] : ~ margaux(X26) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f4875,plain,
( ! [X26] : ~ margaux(X26)
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f4874]) ).
fof(f4877,definition,
( spl0_60
<=> ! [X25] : ~ loire(X25) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f4878,plain,
( ! [X25] : ~ loire(X25)
| ~ spl0_60 ),
inference(avatar_component_clause,[],[f4877]) ).
fof(f4880,definition,
( spl0_61
<=> ! [X24] : ~ lateharvest(X24) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f4881,plain,
( ! [X24] : ~ lateharvest(X24)
| ~ spl0_61 ),
inference(avatar_component_clause,[],[f4880]) ).
fof(f4883,definition,
( spl0_62
<=> ! [X23] : ~ italianwine(X23) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f4884,plain,
( ! [X23] : ~ italianwine(X23)
| ~ spl0_62 ),
inference(avatar_component_clause,[],[f4883]) ).
fof(f4886,definition,
( spl0_63
<=> ! [X22] : ~ icewine(X22) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f4887,plain,
( ! [X22] : ~ icewine(X22)
| ~ spl0_63 ),
inference(avatar_component_clause,[],[f4886]) ).
fof(f4889,definition,
( spl0_64
<=> ! [X21] : ~ grape(X21) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f4890,plain,
( ! [X21] : ~ grape(X21)
| ~ spl0_64 ),
inference(avatar_component_clause,[],[f4889]) ).
fof(f4892,definition,
( spl0_65
<=> ! [X20] : ~ germanwine(X20) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f4893,plain,
( ! [X20] : ~ germanwine(X20)
| ~ spl0_65 ),
inference(avatar_component_clause,[],[f4892]) ).
fof(f4895,definition,
( spl0_66
<=> ! [X19] : ~ gamay(X19) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f4896,plain,
( ! [X19] : ~ gamay(X19)
| ~ spl0_66 ),
inference(avatar_component_clause,[],[f4895]) ).
fof(f4898,definition,
( spl0_67
<=> ! [X18] : ~ fullbodiedwine(X18) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f4899,plain,
( ! [X18] : ~ fullbodiedwine(X18)
| ~ spl0_67 ),
inference(avatar_component_clause,[],[f4898]) ).
fof(f4901,definition,
( spl0_68
<=> ! [X17] : ~ drywine(X17) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f4902,plain,
( ! [X17] : ~ drywine(X17)
| ~ spl0_68 ),
inference(avatar_component_clause,[],[f4901]) ).
fof(f4904,definition,
( spl0_69
<=> ! [X16] : ~ drywhitewine(X16) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f4905,plain,
( ! [X16] : ~ drywhitewine(X16)
| ~ spl0_69 ),
inference(avatar_component_clause,[],[f4904]) ).
fof(f4907,definition,
( spl0_70
<=> ! [X15] : ~ dryredwine(X15) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f4908,plain,
( ! [X15] : ~ dryredwine(X15)
| ~ spl0_70 ),
inference(avatar_component_clause,[],[f4907]) ).
fof(f4910,definition,
( spl0_71
<=> ! [X14] : ~ dryriesling(X14) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f4911,plain,
( ! [X14] : ~ dryriesling(X14)
| ~ spl0_71 ),
inference(avatar_component_clause,[],[f4910]) ).
fof(f4913,definition,
( spl0_72
<=> ! [X13] : ~ dessertwine(X13) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f4914,plain,
( ! [X13] : ~ dessertwine(X13)
| ~ spl0_72 ),
inference(avatar_component_clause,[],[f4913]) ).
fof(f4916,definition,
( spl0_73
<=> ! [X12] : ~ cotesdor(X12) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f4917,plain,
( ! [X12] : ~ cotesdor(X12)
| ~ spl0_73 ),
inference(avatar_component_clause,[],[f4916]) ).
fof(f4919,definition,
( spl0_74
<=> ! [X11] : ~ chianti(X11) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f4920,plain,
( ! [X11] : ~ chianti(X11)
| ~ spl0_74 ),
inference(avatar_component_clause,[],[f4919]) ).
fof(f4922,definition,
( spl0_75
<=> ! [X10] : ~ cheninblanc(X10) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f4923,plain,
( ! [X10] : ~ cheninblanc(X10)
| ~ spl0_75 ),
inference(avatar_component_clause,[],[f4922]) ).
fof(f4925,definition,
( spl0_76
<=> ! [X9] : ~ chardonnay(X9) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f4926,plain,
( ! [X9] : ~ chardonnay(X9)
| ~ spl0_76 ),
inference(avatar_component_clause,[],[f4925]) ).
fof(f4928,definition,
( spl0_77
<=> ! [X8] : ~ californiawine(X8) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f4929,plain,
( ! [X8] : ~ californiawine(X8)
| ~ spl0_77 ),
inference(avatar_component_clause,[],[f4928]) ).
fof(f4931,definition,
( spl0_78
<=> ! [X7] : ~ cabernetsauvignon(X7) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f4932,plain,
( ! [X7] : ~ cabernetsauvignon(X7)
| ~ spl0_78 ),
inference(avatar_component_clause,[],[f4931]) ).
fof(f4934,definition,
( spl0_79
<=> ! [X6] : ~ cabernetfranc(X6) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f4935,plain,
( ! [X6] : ~ cabernetfranc(X6)
| ~ spl0_79 ),
inference(avatar_component_clause,[],[f4934]) ).
fof(f4937,definition,
( spl0_80
<=> ! [X5] : ~ beaujolais(X5) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f4938,plain,
( ! [X5] : ~ beaujolais(X5)
| ~ spl0_80 ),
inference(avatar_component_clause,[],[f4937]) ).
fof(f4940,definition,
( spl0_81
<=> ! [X4] : ~ anjou(X4) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f4941,plain,
( ! [X4] : ~ anjou(X4)
| ~ spl0_81 ),
inference(avatar_component_clause,[],[f4940]) ).
fof(f4943,definition,
( spl0_82
<=> ! [X3] : ~ burgundy(X3) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f4944,plain,
( ! [X3] : ~ burgundy(X3)
| ~ spl0_82 ),
inference(avatar_component_clause,[],[f4943]) ).
fof(f4946,definition,
( spl0_83
<=> ! [X2] : ~ bordeaux(X2) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f4947,plain,
( ! [X2] : ~ bordeaux(X2)
| ~ spl0_83 ),
inference(avatar_component_clause,[],[f4946]) ).
fof(f4949,definition,
( spl0_84
<=> ! [X1] : ~ americanwine(X1) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f4950,plain,
( ! [X1] : ~ americanwine(X1)
| ~ spl0_84 ),
inference(avatar_component_clause,[],[f4949]) ).
fof(f4951,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4
| spl0_5
| spl0_6
| spl0_7
| spl0_8
| spl0_9
| spl0_10
| spl0_11
| spl0_12
| spl0_13
| spl0_14
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_19
| spl0_20
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_25
| spl0_26
| spl0_27
| spl0_28
| spl0_29
| spl0_30
| spl0_31
| spl0_32
| spl0_33
| spl0_34
| spl0_35
| spl0_36
| spl0_37
| spl0_38
| spl0_39
| spl0_40
| spl0_41
| spl0_42
| spl0_43
| spl0_44
| spl0_45
| spl0_46
| spl0_47
| spl0_48
| spl0_49
| spl0_50
| spl0_51
| spl0_52
| spl0_53
| spl0_54
| spl0_55
| spl0_56
| spl0_57
| spl0_58
| spl0_59
| spl0_60
| spl0_61
| spl0_62
| spl0_63
| spl0_64
| spl0_65
| spl0_66
| spl0_67
| spl0_68
| spl0_69
| spl0_70
| spl0_71
| spl0_72
| spl0_73
| spl0_74
| spl0_75
| spl0_76
| spl0_77
| spl0_78
| spl0_79
| spl0_80
| spl0_81
| spl0_82
| spl0_83
| spl0_84
| spl0_77 ),
inference(avatar_split_clause,[],[f4698,f4928,f4949,f4946,f4943,f4940,f4937,f4934,f4931,f4928,f4925,f4922,f4919,f4916,f4913,f4910,f4907,f4904,f4901,f4898,f4895,f4892,f4889,f4886,f4883,f4880,f4877,f4874,f4871,f4868,f4865,f4862,f4859,f4856,f4853,f4850,f4847,f4844,f4841,f4838,f4835,f4832,f4829,f4826,f4823,f4820,f4817,f4814,f4811,f4808,f4805,f4802,f4799,f4796,f4793,f4790,f4787,f4784,f4781,f4778,f4775,f4772,f4769,f4766,f4763,f4760,f4757,f4754,f4751,f4748,f4745,f4742,f4739,f4736,f4733,f4730,f4727,f4724,f4721,f4718,f4715,f4712,f4709,f4706,f4703,f4700]) ).
fof(f5018,plain,
! [X0] :
( ~ wine(X0)
| ~ kaon2namedobjects(X0)
| ~ wine(X0)
| winery(X0) ),
inference(resolution,[],[f4576,f4408]) ).
fof(f5020,plain,
! [X0] :
( ~ wine(X0)
| ~ kaon2namedobjects(X0)
| winery(X0) ),
inference(duplicate_literal_removal,[],[f5018]) ).
fof(f5033,plain,
! [X0] :
( ~ wine(X0)
| ~ kaon2namedobjects(X0)
| winegrape(X0) ),
inference(resolution,[],[f4629,f4398]) ).
fof(f5055,plain,
! [X0] :
( ~ wine(X0)
| ~ kaon2namedobjects(X0)
| winecolor(X0) ),
inference(resolution,[],[f4565,f4388]) ).
fof(f5077,plain,
! [X0] :
( ~ wine(X0)
| ~ kaon2namedobjects(X0)
| wineflavor(X0) ),
inference(resolution,[],[f4572,f4395]) ).
fof(f5100,plain,
! [X0] :
( ~ wine(X0)
| ~ kaon2namedobjects(X0)
| winebody(X0) ),
inference(resolution,[],[f4558,f4385]) ).
fof(f5112,plain,
! [X0] :
( ~ whitewine(X0)
| ~ kaon2namedobjects(X0)
| winesugar(X0) ),
inference(resolution,[],[f4581,f4401]) ).
fof(f5113,plain,
! [X0] :
( haswinedescriptor(X0,X0)
| ~ kaon2namedobjects(X0)
| ~ whitewine(X0) ),
inference(resolution,[],[f4581,f4592]) ).
fof(f5187,plain,
! [X0] :
( madefromfruit(X0,X0)
| ~ kaon2namedobjects(X0)
| ~ cabernetfranc(X0) ),
inference(resolution,[],[f4641,f4624]) ).
fof(f5188,plain,
! [X0] :
( madeintowine(X0,X0)
| ~ kaon2namedobjects(X0)
| ~ cabernetfranc(X0) ),
inference(resolution,[],[f4641,f4647]) ).
fof(f5201,plain,
( ! [X0] :
( ~ cabernetfranc(X0)
| ~ kaon2namedobjects(X0) )
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f5188,f4704]) ).
fof(f5231,plain,
cabernetfranc(whitehalllanecabernetfranc),
inference(resolution,[],[f3505,f3817]) ).
fof(f5232,plain,
wine(whitehalllanecabernetfranc),
inference(resolution,[],[f5231,f4341]) ).
fof(f5236,plain,
dryriesling(mountadamriesling),
inference(resolution,[],[f3499,f3824]) ).
fof(f5244,plain,
meritage(kathrynkennedylateral),
inference(resolution,[],[f3496,f3827]) ).
fof(f5257,plain,
meursault(chateaudemeursaultmeursault),
inference(resolution,[],[f3495,f3829]) ).
fof(f5258,plain,
whitewine(stgenevievetexaswhite),
inference(resolution,[],[f3493,f3846]) ).
fof(f5259,plain,
( ~ kaon2namedobjects(whitehalllanecabernetfranc)
| ~ spl0_2 ),
inference(resolution,[],[f5201,f5231]) ).
fof(f5260,plain,
( $false
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f5259,f3641]) ).
fof(f5261,plain,
~ spl0_2,
inference(avatar_contradiction_clause,[],[f5260]) ).
fof(f5272,plain,
whiteburgundy(chateaudemeursaultmeursault),
inference(resolution,[],[f5257,f4308]) ).
fof(f5277,plain,
( ! [X0] :
( ~ cabernetfranc(X0)
| ~ kaon2namedobjects(X0) )
| ~ spl0_3 ),
inference(resolution,[],[f5187,f4707]) ).
fof(f5278,plain,
( ~ kaon2namedobjects(whitehalllanecabernetfranc)
| ~ spl0_3 ),
inference(resolution,[],[f5277,f5231]) ).
fof(f5279,plain,
( $false
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f5278,f3641]) ).
fof(f5280,plain,
~ spl0_3,
inference(avatar_contradiction_clause,[],[f5279]) ).
fof(f5289,plain,
( ! [X0] :
( ~ cabernetfranc(X0)
| ~ kaon2namedobjects(X0) )
| ~ spl0_4 ),
inference(resolution,[],[f4710,f4641]) ).
fof(f5291,plain,
( ~ kaon2namedobjects(whitehalllanecabernetfranc)
| ~ spl0_4 ),
inference(resolution,[],[f5289,f5231]) ).
fof(f5292,plain,
( $false
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f5291,f3641]) ).
fof(f5293,plain,
~ spl0_4,
inference(avatar_contradiction_clause,[],[f5292]) ).
fof(f5297,plain,
( ! [X0] :
( ~ chianti(X0)
| ~ kaon2namedobjects(X0) )
| ~ spl0_5 ),
inference(resolution,[],[f4713,f4606]) ).
fof(f5325,plain,
icewine(selaksicewine),
inference(resolution,[],[f3498,f3825]) ).
fof(f5326,plain,
dessertwine(selaksicewine),
inference(resolution,[],[f5325,f4182]) ).
fof(f5327,plain,
lateharvest(selaksicewine),
inference(resolution,[],[f5325,f4212]) ).
fof(f5328,plain,
chianti(chianticlassico),
inference(resolution,[],[f3515,f3821]) ).
fof(f5332,plain,
( ~ kaon2namedobjects(chianticlassico)
| ~ spl0_5 ),
inference(resolution,[],[f5328,f5297]) ).
fof(f5333,plain,
italianwine(chianticlassico),
inference(resolution,[],[f5328,f4209]) ).
fof(f5334,plain,
( $false
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f5332,f3689]) ).
fof(f5335,plain,
~ spl0_5,
inference(avatar_contradiction_clause,[],[f5334]) ).
fof(f5345,plain,
( ! [X0] :
( ~ whitewine(X0)
| ~ kaon2namedobjects(X0) )
| ~ spl0_6 ),
inference(resolution,[],[f4716,f5113]) ).
fof(f5346,plain,
muscadet(sevreetmainemuscadet),
inference(resolution,[],[f3494,f3830]) ).
fof(f5347,plain,
loire(sevreetmainemuscadet),
inference(resolution,[],[f5346,f4219]) ).
fof(f5348,plain,
margaux(chateaumargaux),
inference(resolution,[],[f3497,f3826]) ).
fof(f5349,plain,
medoc(chateaumargaux),
inference(resolution,[],[f5348,f4225]) ).
fof(f5350,plain,
pauillac(chateaulafiterothschildpauillac),
inference(resolution,[],[f3519,f3831]) ).
fof(f5351,plain,
medoc(chateaulafiterothschildpauillac),
inference(resolution,[],[f5350,f4224]) ).
fof(f5352,plain,
anjou(rosedanjou),
inference(resolution,[],[f3507,f3815]) ).
fof(f5354,plain,
cotesdor(closdevougeotcotesdor),
inference(resolution,[],[f3516,f3822]) ).
fof(f5355,plain,
redburgundy(closdevougeotcotesdor),
inference(resolution,[],[f5354,f4252]) ).
fof(f5356,plain,
beaujolais(chateaumorgonbeaujolais),
inference(resolution,[],[f3506,f3816]) ).
fof(f5358,plain,
( ~ kaon2namedobjects(stgenevievetexaswhite)
| ~ spl0_6 ),
inference(resolution,[],[f5258,f5345]) ).
fof(f5360,plain,
wine(stgenevievetexaswhite),
inference(resolution,[],[f5258,f4363]) ).
fof(f5364,plain,
( $false
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f5358,f3646]) ).
fof(f5365,plain,
~ spl0_6,
inference(avatar_contradiction_clause,[],[f5364]) ).
fof(f5367,plain,
sancerre(closdelapoussiesancerre),
inference(resolution,[],[f3564,f3838]) ).
fof(f5369,plain,
stemilion(chateauchevalblancstemilion),
inference(resolution,[],[f3572,f3842]) ).
fof(f5371,plain,
port(taylorport),
inference(resolution,[],[f3525,f3834]) ).
fof(f5372,plain,
redwine(taylorport),
inference(resolution,[],[f5371,f4260]) ).
fof(f5373,plain,
sauternes(chateaudychemsauterne),
inference(resolution,[],[f3565,f3839]) ).
fof(f5384,plain,
bordeaux(chateaudychemsauterne),
inference(resolution,[],[f5373,f4154]) ).
fof(f5390,plain,
q12(chateaudychemsauterne),
inference(resolution,[],[f3880,f5373]) ).
fof(f5393,plain,
vintageyear(year1998),
inference(resolution,[],[f3736,f3844]) ).
fof(f5929,plain,
redwine(closdevougeotcotesdor),
inference(resolution,[],[f5355,f4257]) ).
fof(f5930,plain,
burgundy(closdevougeotcotesdor),
inference(resolution,[],[f5355,f4162]) ).
fof(f5932,plain,
q0(chateaumargaux),
inference(resolution,[],[f5349,f3855]) ).
fof(f5933,plain,
bordeaux(chateaumargaux),
inference(resolution,[],[f5349,f4155]) ).
fof(f5934,plain,
q14(chateaumorgonbeaujolais),
inference(resolution,[],[f3888,f5356]) ).
fof(f5966,plain,
q24(sevreetmainemuscadet),
inference(resolution,[],[f3925,f5346]) ).
fof(f6035,plain,
( whiteloire(sevreetmainemuscadet)
| ~ whitewine(sevreetmainemuscadet) ),
inference(resolution,[],[f5347,f4311]) ).
fof(f6036,plain,
wine(sevreetmainemuscadet),
inference(resolution,[],[f5347,f4345]) ).
fof(f6038,definition,
( spl0_145
<=> whitewine(sevreetmainemuscadet) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f6040,plain,
( ~ whitewine(sevreetmainemuscadet)
| spl0_145 ),
inference(avatar_component_clause,[],[f6038]) ).
fof(f6042,definition,
( spl0_146
<=> whiteloire(sevreetmainemuscadet) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f6044,plain,
( whiteloire(sevreetmainemuscadet)
| ~ spl0_146 ),
inference(avatar_component_clause,[],[f6042]) ).
fof(f6045,plain,
( ~ spl0_145
| spl0_146 ),
inference(avatar_split_clause,[],[f6035,f6042,f6038]) ).
fof(f6055,plain,
q15(rosedanjou),
inference(resolution,[],[f3890,f5352]) ).
fof(f6109,plain,
cheninblanc(foxencheninblanc),
inference(resolution,[],[f3513,f3820]) ).
fof(f6244,definition,
( spl0_171
<=> gamay(chateaumorgonbeaujolais) ),
introduced(definition,[new_symbols(definition,[spl0_171])],[avatar_definition]) ).
fof(f6246,plain,
( gamay(chateaumorgonbeaujolais)
| ~ spl0_171 ),
inference(avatar_component_clause,[],[f6244]) ).
fof(f6361,plain,
sweetriesling(schlossvolradtrochenbierenausleseriesling),
inference(resolution,[],[f3574,f3843]) ).
fof(f6473,plain,
sweetriesling(schlossrothermeltrochenbierenausleseriesling),
inference(resolution,[],[f3573,f3843]) ).
fof(f6477,plain,
riesling(schlossrothermeltrochenbierenausleseriesling),
inference(resolution,[],[f6473,f4269]) ).
fof(f6480,plain,
wine(schlossrothermeltrochenbierenausleseriesling),
inference(resolution,[],[f6477,f4360]) ).
fof(f6607,plain,
petitesyrah(mariettapetitesyrah),
inference(resolution,[],[f3520,f3832]) ).
fof(f6843,plain,
merlot(garyfarrellmerlot),
inference(resolution,[],[f3517,f3828]) ).
fof(f7023,plain,
semillon(congressspringssemillon),
inference(resolution,[],[f3570,f3841]) ).
fof(f7253,plain,
whiteburgundy(pulignymontrachetwhiteburgundy),
inference(resolution,[],[f3491,f3845]) ).
fof(f7255,plain,
whitewine(pulignymontrachetwhiteburgundy),
inference(resolution,[],[f7253,f4320]) ).
fof(f7256,plain,
burgundy(pulignymontrachetwhiteburgundy),
inference(resolution,[],[f7253,f4161]) ).
fof(f7258,plain,
wine(pulignymontrachetwhiteburgundy),
inference(resolution,[],[f7256,f4370]) ).
fof(f7287,plain,
q12(pulignymontrachetwhiteburgundy),
inference(resolution,[],[f7255,f3878]) ).
fof(f7290,plain,
( whitenonsweetwine(pulignymontrachetwhiteburgundy)
| ~ kaon2namedobjects(pulignymontrachetwhiteburgundy) ),
inference(resolution,[],[f7255,f4313]) ).
fof(f7291,plain,
whitenonsweetwine(pulignymontrachetwhiteburgundy),
inference(forward_subsumption_resolution,[],[f7290,f3706]) ).
fof(f8164,plain,
cabernetsauvignon(mariettacabernetsauvignon),
inference(resolution,[],[f3501,f3818]) ).
fof(f9979,plain,
q70(selaksicewine),
inference(resolution,[],[f5327,f4129]) ).
fof(f9981,plain,
wine(selaksicewine),
inference(resolution,[],[f5327,f4381]) ).
fof(f10352,plain,
( whitebordeaux(chateaudychemsauterne)
| ~ whitewine(chateaudychemsauterne) ),
inference(resolution,[],[f5384,f4306]) ).
fof(f10353,plain,
wine(chateaudychemsauterne),
inference(resolution,[],[f5384,f4359]) ).
fof(f10365,definition,
( spl0_848
<=> whitewine(chateaudychemsauterne) ),
introduced(definition,[new_symbols(definition,[spl0_848])],[avatar_definition]) ).
fof(f10367,plain,
( ~ whitewine(chateaudychemsauterne)
| spl0_848 ),
inference(avatar_component_clause,[],[f10365]) ).
fof(f10369,definition,
( spl0_849
<=> whitebordeaux(chateaudychemsauterne) ),
introduced(definition,[new_symbols(definition,[spl0_849])],[avatar_definition]) ).
fof(f10371,plain,
( whitebordeaux(chateaudychemsauterne)
| ~ spl0_849 ),
inference(avatar_component_clause,[],[f10369]) ).
fof(f10372,plain,
( ~ spl0_848
| spl0_849 ),
inference(avatar_split_clause,[],[f10352,f10369,f10365]) ).
fof(f10774,plain,
hasflavor(formanchardonnay,moderate),
inference(resolution,[],[f3128,f3742]) ).
fof(f10784,plain,
haswinedescriptor(formanchardonnay,moderate),
inference(resolution,[],[f10774,f4591]) ).
fof(f10787,plain,
hasflavor(pulignymontrachetwhiteburgundy,moderate),
inference(resolution,[],[f3127,f3742]) ).
fof(f10848,definition,
( spl0_887
<=> q21(chateaudychemsauterne) ),
introduced(definition,[new_symbols(definition,[spl0_887])],[avatar_definition]) ).
fof(f10849,plain,
( q21(chateaudychemsauterne)
| ~ spl0_887 ),
inference(avatar_component_clause,[],[f10848]) ).
fof(f10918,plain,
hasflavor(bancroftchardonnay,moderate),
inference(resolution,[],[f3138,f3742]) ).
fof(f10928,plain,
haswinedescriptor(bancroftchardonnay,moderate),
inference(resolution,[],[f10918,f4591]) ).
fof(f10929,plain,
hasflavor(elysezinfandel,moderate),
inference(resolution,[],[f3139,f3742]) ).
fof(f10939,plain,
haswinedescriptor(elysezinfandel,moderate),
inference(resolution,[],[f10929,f4591]) ).
fof(f11402,plain,
locatedin(centraltexasregion,texasregion),
inference(resolution,[],[f3281,f3739]) ).
fof(f11556,plain,
wine(formanchardonnay),
inference(resolution,[],[f10784,f4331]) ).
fof(f11685,plain,
q31(closdevougeotcotesdor),
inference(resolution,[],[f5930,f3973]) ).
fof(f11686,plain,
wine(closdevougeotcotesdor),
inference(resolution,[],[f5930,f4370]) ).
fof(f11738,plain,
wine(elysezinfandel),
inference(resolution,[],[f10939,f4331]) ).
fof(f11782,plain,
wine(bancroftchardonnay),
inference(resolution,[],[f10928,f4331]) ).
fof(f12045,plain,
locatedin(californiaregion,usregion),
inference(resolution,[],[f3262,f3739]) ).
fof(f12239,plain,
locatedin(schlossrothermeltrochenbierenausleseriesling,germanyregion),
inference(resolution,[],[f3282,f3739]) ).
fof(f12463,plain,
locatedin(stgenevievetexaswhite,centraltexasregion),
inference(resolution,[],[f3265,f3739]) ).
fof(f12468,plain,
( q73(stgenevievetexaswhite)
| ~ q74(centraltexasregion) ),
inference(resolution,[],[f12463,f4138]) ).
fof(f12474,definition,
( spl0_991
<=> q74(centraltexasregion) ),
introduced(definition,[new_symbols(definition,[spl0_991])],[avatar_definition]) ).
fof(f12476,plain,
( ~ q74(centraltexasregion)
| spl0_991 ),
inference(avatar_component_clause,[],[f12474]) ).
fof(f12478,definition,
( spl0_992
<=> q73(stgenevievetexaswhite) ),
introduced(definition,[new_symbols(definition,[spl0_992])],[avatar_definition]) ).
fof(f12480,plain,
( q73(stgenevievetexaswhite)
| ~ spl0_992 ),
inference(avatar_component_clause,[],[f12478]) ).
fof(f12481,plain,
( ~ spl0_991
| spl0_992 ),
inference(avatar_split_clause,[],[f12468,f12478,f12474]) ).
fof(f12704,definition,
( spl0_1007
<=> wine(chateaumargaux) ),
introduced(definition,[new_symbols(definition,[spl0_1007])],[avatar_definition]) ).
fof(f12705,plain,
( wine(chateaumargaux)
| ~ spl0_1007 ),
inference(avatar_component_clause,[],[f12704]) ).
fof(f12706,plain,
( ~ wine(chateaumargaux)
| spl0_1007 ),
inference(avatar_component_clause,[],[f12704]) ).
fof(f12839,definition,
( spl0_1022
<=> q27(californiaregion) ),
introduced(definition,[new_symbols(definition,[spl0_1022])],[avatar_definition]) ).
fof(f12840,plain,
( q27(californiaregion)
| ~ spl0_1022 ),
inference(avatar_component_clause,[],[f12839]) ).
fof(f12841,plain,
( ~ q27(californiaregion)
| spl0_1022 ),
inference(avatar_component_clause,[],[f12839]) ).
fof(f13696,plain,
wine(chateaumargaux),
inference(resolution,[],[f5933,f4359]) ).
fof(f13697,plain,
( ~ redwine(chateaumargaux)
| redbordeaux(chateaumargaux) ),
inference(resolution,[],[f5933,f4250]) ).
fof(f13699,definition,
( spl0_1092
<=> redbordeaux(chateaumargaux) ),
introduced(definition,[new_symbols(definition,[spl0_1092])],[avatar_definition]) ).
fof(f13701,plain,
( redbordeaux(chateaumargaux)
| ~ spl0_1092 ),
inference(avatar_component_clause,[],[f13699]) ).
fof(f13703,definition,
( spl0_1093
<=> redwine(chateaumargaux) ),
introduced(definition,[new_symbols(definition,[spl0_1093])],[avatar_definition]) ).
fof(f13705,plain,
( ~ redwine(chateaumargaux)
| spl0_1093 ),
inference(avatar_component_clause,[],[f13703]) ).
fof(f13706,plain,
( spl0_1092
| ~ spl0_1093 ),
inference(avatar_split_clause,[],[f13697,f13703,f13699]) ).
fof(f13707,plain,
( $false
| spl0_1007 ),
inference(forward_subsumption_resolution,[],[f13696,f12706]) ).
fof(f13708,plain,
spl0_1007,
inference(avatar_contradiction_clause,[],[f13707]) ).
fof(f14185,definition,
( spl0_1142
<=> q48(naparegion) ),
introduced(definition,[new_symbols(definition,[spl0_1142])],[avatar_definition]) ).
fof(f14186,plain,
( q48(naparegion)
| ~ spl0_1142 ),
inference(avatar_component_clause,[],[f14185]) ).
fof(f14187,plain,
( ~ q48(naparegion)
| spl0_1142 ),
inference(avatar_component_clause,[],[f14185]) ).
fof(f14194,definition,
( spl0_1144
<=> q27(naparegion) ),
introduced(definition,[new_symbols(definition,[spl0_1144])],[avatar_definition]) ).
fof(f14195,plain,
( q27(naparegion)
| ~ spl0_1144 ),
inference(avatar_component_clause,[],[f14194]) ).
fof(f14196,plain,
( ~ q27(naparegion)
| spl0_1144 ),
inference(avatar_component_clause,[],[f14194]) ).
fof(f14408,plain,
hasmaker(pulignymontrachetwhiteburgundy,pulignymontrachet),
inference(resolution,[],[f3170,f3741]) ).
fof(f14410,plain,
produceswine(pulignymontrachet,pulignymontrachetwhiteburgundy),
inference(resolution,[],[f14408,f4650]) ).
fof(f14412,plain,
chardonnay(formanchardonnay),
inference(resolution,[],[f3508,f3819]) ).
fof(f14417,plain,
locatedin(whitehalllanecabernetfranc,naparegion),
inference(resolution,[],[f3315,f3739]) ).
fof(f14419,plain,
( q47(whitehalllanecabernetfranc)
| ~ q48(naparegion) ),
inference(resolution,[],[f14417,f4033]) ).
fof(f14876,plain,
locatedin(naparegion,californiaregion),
inference(resolution,[],[f3275,f3739]) ).
fof(f14878,plain,
( q26(naparegion)
| ~ q27(californiaregion) ),
inference(resolution,[],[f14876,f3928]) ).
fof(f15065,plain,
( ~ kaon2namedobjects(pulignymontrachetwhiteburgundy)
| winesugar(pulignymontrachetwhiteburgundy) ),
inference(resolution,[],[f5112,f7255]) ).
fof(f15068,plain,
winesugar(pulignymontrachetwhiteburgundy),
inference(forward_subsumption_resolution,[],[f15065,f3706]) ).
fof(f15104,plain,
sauvignonblanc(corbansprivatebinsauvignonblanc),
inference(resolution,[],[f3566,f3840]) ).
fof(f15107,plain,
semillonorsauvignonblanc(corbansprivatebinsauvignonblanc),
inference(resolution,[],[f15104,f4284]) ).
fof(f15423,plain,
locatedin(bancroftchardonnay,naparegion),
inference(resolution,[],[f3273,f3739]) ).
fof(f15425,plain,
( q26(bancroftchardonnay)
| ~ q27(naparegion) ),
inference(resolution,[],[f15423,f3928]) ).
fof(f16255,plain,
( ~ q21(sevreetmainemuscadet)
| whitewine(sevreetmainemuscadet) ),
inference(resolution,[],[f6036,f4324]) ).
fof(f16294,plain,
( ~ q21(sevreetmainemuscadet)
| spl0_145 ),
inference(forward_subsumption_resolution,[],[f16255,f6040]) ).
fof(f16371,definition,
( spl0_1300
<=> pinotblanc(sevreetmainemuscadet) ),
introduced(definition,[new_symbols(definition,[spl0_1300])],[avatar_definition]) ).
fof(f16373,plain,
( pinotblanc(sevreetmainemuscadet)
| ~ spl0_1300 ),
inference(avatar_component_clause,[],[f16371]) ).
fof(f16933,definition,
( spl0_1387
<=> rosewine(rosedanjou) ),
introduced(definition,[new_symbols(definition,[spl0_1387])],[avatar_definition]) ).
fof(f16935,plain,
( rosewine(rosedanjou)
| ~ spl0_1387 ),
inference(avatar_component_clause,[],[f16933]) ).
fof(f17588,definition,
( spl0_1471
<=> ot____nom45(full) ),
introduced(definition,[new_symbols(definition,[spl0_1471])],[avatar_definition]) ).
fof(f17589,plain,
( ot____nom45(full)
| ~ spl0_1471 ),
inference(avatar_component_clause,[],[f17588]) ).
fof(f17590,plain,
( ~ ot____nom45(full)
| spl0_1471 ),
inference(avatar_component_clause,[],[f17588]) ).
fof(f17846,plain,
hasbody(formanchardonnay,full),
inference(resolution,[],[f3086,f3744]) ).
fof(f17847,plain,
( ~ wine(formanchardonnay)
| fullbodiedwine(formanchardonnay)
| ~ ot____nom45(full) ),
inference(resolution,[],[f17846,f4199]) ).
fof(f18146,plain,
hasbody(pulignymontrachetwhiteburgundy,medium),
inference(resolution,[],[f3085,f3744]) ).
fof(f19129,plain,
potableliquid(pulignymontrachetwhiteburgundy),
inference(resolution,[],[f7258,f4248]) ).
fof(f19130,plain,
( region(pulignymontrachetwhiteburgundy)
| ~ kaon2namedobjects(pulignymontrachetwhiteburgundy) ),
inference(resolution,[],[f7258,f4266]) ).
fof(f19133,plain,
( ~ kaon2namedobjects(pulignymontrachetwhiteburgundy)
| winery(pulignymontrachetwhiteburgundy) ),
inference(resolution,[],[f7258,f5020]) ).
fof(f19134,plain,
( ~ kaon2namedobjects(pulignymontrachetwhiteburgundy)
| winegrape(pulignymontrachetwhiteburgundy) ),
inference(resolution,[],[f7258,f5033]) ).
fof(f19142,plain,
( ~ kaon2namedobjects(pulignymontrachetwhiteburgundy)
| winecolor(pulignymontrachetwhiteburgundy) ),
inference(resolution,[],[f7258,f5055]) ).
fof(f19144,plain,
( ~ kaon2namedobjects(pulignymontrachetwhiteburgundy)
| wineflavor(pulignymontrachetwhiteburgundy) ),
inference(resolution,[],[f7258,f5077]) ).
fof(f19149,plain,
( ~ kaon2namedobjects(pulignymontrachetwhiteburgundy)
| winebody(pulignymontrachetwhiteburgundy) ),
inference(resolution,[],[f7258,f5100]) ).
fof(f19154,plain,
winebody(pulignymontrachetwhiteburgundy),
inference(forward_subsumption_resolution,[],[f19149,f3706]) ).
fof(f19159,plain,
wineflavor(pulignymontrachetwhiteburgundy),
inference(forward_subsumption_resolution,[],[f19144,f3706]) ).
fof(f19161,plain,
winecolor(pulignymontrachetwhiteburgundy),
inference(forward_subsumption_resolution,[],[f19142,f3706]) ).
fof(f19168,plain,
winegrape(pulignymontrachetwhiteburgundy),
inference(forward_subsumption_resolution,[],[f19134,f3706]) ).
fof(f19169,plain,
winery(pulignymontrachetwhiteburgundy),
inference(forward_subsumption_resolution,[],[f19133,f3706]) ).
fof(f19171,plain,
region(pulignymontrachetwhiteburgundy),
inference(forward_subsumption_resolution,[],[f19130,f3706]) ).
fof(f19336,plain,
winetaste(pulignymontrachetwhiteburgundy),
inference(resolution,[],[f19159,f4403]) ).
fof(f19340,plain,
winedescriptor(pulignymontrachetwhiteburgundy),
inference(resolution,[],[f19161,f4391]) ).
fof(f19341,plain,
grape(pulignymontrachetwhiteburgundy),
inference(resolution,[],[f19168,f4205]) ).
fof(f20756,plain,
q21(chateaudychemsauterne),
inference(resolution,[],[f5390,f3915]) ).
fof(f20762,plain,
spl0_887,
inference(avatar_split_clause,[],[f20756,f10848]) ).
fof(f20804,plain,
hascolor(selaksicewine,white),
inference(resolution,[],[f3126,f3743]) ).
fof(f21040,plain,
gamay(chateaumorgonbeaujolais),
inference(resolution,[],[f5934,f4200]) ).
fof(f21052,plain,
spl0_171,
inference(avatar_split_clause,[],[f21040,f6244]) ).
fof(f21183,plain,
hassugar(pulignymontrachetwhiteburgundy,dry),
inference(resolution,[],[f3222,f3740]) ).
fof(f21449,plain,
hassugar(elysezinfandel,dry),
inference(resolution,[],[f3233,f3740]) ).
fof(f21533,plain,
hasvintageyear(saucelitocanyonzinfandel1998,year1998),
inference(resolution,[],[f3737,f3745]) ).
fof(f21534,plain,
( $false
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f21533,f4719]) ).
fof(f21535,plain,
~ spl0_7,
inference(avatar_contradiction_clause,[],[f21534]) ).
fof(f21542,plain,
( $false
| ~ spl0_8 ),
inference(resolution,[],[f4722,f21183]) ).
fof(f21621,plain,
~ spl0_8,
inference(avatar_contradiction_clause,[],[f21542]) ).
fof(f21623,plain,
( $false
| ~ spl0_9 ),
inference(resolution,[],[f4725,f14408]) ).
fof(f21726,plain,
~ spl0_9,
inference(avatar_contradiction_clause,[],[f21623]) ).
fof(f21731,plain,
( $false
| ~ spl0_10 ),
inference(resolution,[],[f4728,f10787]) ).
fof(f21816,plain,
~ spl0_10,
inference(avatar_contradiction_clause,[],[f21731]) ).
fof(f21821,plain,
( $false
| ~ spl0_11 ),
inference(resolution,[],[f4731,f20804]) ).
fof(f21822,plain,
~ spl0_11,
inference(avatar_contradiction_clause,[],[f21821]) ).
fof(f21827,plain,
( $false
| ~ spl0_12 ),
inference(resolution,[],[f4734,f18146]) ).
fof(f21908,plain,
~ spl0_12,
inference(avatar_contradiction_clause,[],[f21827]) ).
fof(f21911,plain,
vintage(saucelitocanyonzinfandel1998),
inference(resolution,[],[f21533,f4302]) ).
fof(f21958,plain,
rosewine(rosedanjou),
inference(resolution,[],[f6055,f4272]) ).
fof(f21959,plain,
spl0_1387,
inference(avatar_split_clause,[],[f21958,f16933]) ).
fof(f21977,plain,
pinotnoir(mountadampinotnoir),
inference(resolution,[],[f3522,f3833]) ).
fof(f22063,plain,
pinotblanc(sevreetmainemuscadet),
inference(resolution,[],[f5966,f4241]) ).
fof(f22075,plain,
spl0_1300,
inference(avatar_split_clause,[],[f22063,f16371]) ).
fof(f22078,plain,
( q12(sevreetmainemuscadet)
| ~ spl0_1300 ),
inference(resolution,[],[f16373,f3877]) ).
fof(f22613,plain,
ot____nom12(dry),
inference(resolution,[],[f3749,f3332]) ).
fof(f23417,plain,
( q27(californiaregion)
| ~ ot____nom38(usregion) ),
inference(resolution,[],[f3931,f12045]) ).
fof(f23558,plain,
( ~ ot____nom38(usregion)
| spl0_1022 ),
inference(forward_subsumption_resolution,[],[f23417,f12841]) ).
fof(f23660,definition,
( spl0_2052
<=> q27(bancroftchardonnay) ),
introduced(definition,[new_symbols(definition,[spl0_2052])],[avatar_definition]) ).
fof(f23662,plain,
( q27(bancroftchardonnay)
| ~ spl0_2052 ),
inference(avatar_component_clause,[],[f23660]) ).
fof(f23786,plain,
( q50(schlossrothermeltrochenbierenausleseriesling)
| ~ ot____nom17(germanyregion) ),
inference(resolution,[],[f4065,f12239]) ).
fof(f23986,definition,
( spl0_2089
<=> ot____nom17(germanyregion) ),
introduced(definition,[new_symbols(definition,[spl0_2089])],[avatar_definition]) ).
fof(f23988,plain,
( ~ ot____nom17(germanyregion)
| spl0_2089 ),
inference(avatar_component_clause,[],[f23986]) ).
fof(f24118,definition,
( spl0_2117
<=> q50(schlossrothermeltrochenbierenausleseriesling) ),
introduced(definition,[new_symbols(definition,[spl0_2117])],[avatar_definition]) ).
fof(f24120,plain,
( q50(schlossrothermeltrochenbierenausleseriesling)
| ~ spl0_2117 ),
inference(avatar_component_clause,[],[f24118]) ).
fof(f24121,plain,
( ~ spl0_2089
| spl0_2117 ),
inference(avatar_split_clause,[],[f23786,f24118,f23986]) ).
fof(f29189,plain,
( q48(naparegion)
| ~ ot____nom15(californiaregion) ),
inference(resolution,[],[f4036,f14876]) ).
fof(f29278,definition,
( spl0_2966
<=> ot____nom15(californiaregion) ),
introduced(definition,[new_symbols(definition,[spl0_2966])],[avatar_definition]) ).
fof(f29280,plain,
( ~ ot____nom15(californiaregion)
| spl0_2966 ),
inference(avatar_component_clause,[],[f29278]) ).
fof(f29320,plain,
( ~ ot____nom15(californiaregion)
| spl0_1142 ),
inference(forward_subsumption_resolution,[],[f29189,f14187]) ).
fof(f29397,definition,
( spl0_2989
<=> q48(whitehalllanecabernetfranc) ),
introduced(definition,[new_symbols(definition,[spl0_2989])],[avatar_definition]) ).
fof(f29399,plain,
( q48(whitehalllanecabernetfranc)
| ~ spl0_2989 ),
inference(avatar_component_clause,[],[f29397]) ).
fof(f29561,plain,
( ~ spl0_2966
| spl0_1142 ),
inference(avatar_split_clause,[],[f29320,f14185,f29278]) ).
fof(f29576,plain,
( ~ q21(chateaudychemsauterne)
| whitewine(chateaudychemsauterne) ),
inference(resolution,[],[f10353,f4324]) ).
fof(f29612,plain,
( whitewine(chateaudychemsauterne)
| ~ spl0_887 ),
inference(forward_subsumption_resolution,[],[f29576,f10849]) ).
fof(f29699,plain,
( $false
| spl0_848
| ~ spl0_887 ),
inference(forward_subsumption_resolution,[],[f29612,f10367]) ).
fof(f29700,plain,
( spl0_848
| ~ spl0_887 ),
inference(avatar_contradiction_clause,[],[f29699]) ).
fof(f32937,plain,
ot____nom15(californiaregion),
inference(resolution,[],[f3752,f3335]) ).
fof(f32938,plain,
( $false
| spl0_2966 ),
inference(forward_subsumption_resolution,[],[f32937,f29280]) ).
fof(f32939,plain,
spl0_2966,
inference(avatar_contradiction_clause,[],[f32938]) ).
fof(f32946,plain,
( q47(whitehalllanecabernetfranc)
| ~ spl0_1142 ),
inference(forward_subsumption_resolution,[],[f14419,f14186]) ).
fof(f33202,plain,
( q74(centraltexasregion)
| ~ ot____nom10(texasregion) ),
inference(resolution,[],[f4141,f11402]) ).
fof(f33331,plain,
( ~ ot____nom10(texasregion)
| spl0_991 ),
inference(forward_subsumption_resolution,[],[f33202,f12476]) ).
fof(f33345,definition,
( spl0_3603
<=> q74(stgenevievetexaswhite) ),
introduced(definition,[new_symbols(definition,[spl0_3603])],[avatar_definition]) ).
fof(f33347,plain,
( q74(stgenevievetexaswhite)
| ~ spl0_3603 ),
inference(avatar_component_clause,[],[f33345]) ).
fof(f33648,plain,
( q48(whitehalllanecabernetfranc)
| ~ spl0_1142 ),
inference(resolution,[],[f32946,f4035]) ).
fof(f33650,plain,
( spl0_2989
| ~ spl0_1142 ),
inference(avatar_split_clause,[],[f33648,f14185,f29397]) ).
fof(f33651,plain,
( californiawine(whitehalllanecabernetfranc)
| ~ wine(whitehalllanecabernetfranc)
| ~ spl0_2989 ),
inference(resolution,[],[f29399,f4170]) ).
fof(f33652,plain,
( californiawine(whitehalllanecabernetfranc)
| ~ spl0_2989 ),
inference(forward_subsumption_resolution,[],[f33651,f5232]) ).
fof(f34186,plain,
ot____nom45(full),
inference(resolution,[],[f3785,f3374]) ).
fof(f34187,plain,
( $false
| spl0_1471 ),
inference(forward_subsumption_resolution,[],[f34186,f17590]) ).
fof(f34188,plain,
spl0_1471,
inference(avatar_contradiction_clause,[],[f34187]) ).
fof(f34193,plain,
( fullbodiedwine(formanchardonnay)
| ~ ot____nom45(full) ),
inference(forward_subsumption_resolution,[],[f17847,f11556]) ).
fof(f34203,plain,
( fullbodiedwine(formanchardonnay)
| ~ spl0_1471 ),
inference(forward_subsumption_resolution,[],[f34193,f17589]) ).
fof(f34565,plain,
! [X0] :
( ~ wine(X0)
| ~ ot____nom5(X0)
| q21(X0)
| ~ kaon2namedobjects(X0) ),
inference(resolution,[],[f3916,f4565]) ).
fof(f35195,plain,
q21(pulignymontrachetwhiteburgundy),
inference(resolution,[],[f7287,f3915]) ).
fof(f35377,plain,
! [X0] :
( ~ wine(X0)
| ~ ot____nom12(X0)
| q46(X0)
| ~ kaon2namedobjects(X0) ),
inference(resolution,[],[f4030,f4579]) ).
fof(f35380,plain,
( q46(pulignymontrachetwhiteburgundy)
| ~ ot____nom12(dry) ),
inference(resolution,[],[f4030,f21183]) ).
fof(f35390,plain,
( q46(elysezinfandel)
| ~ ot____nom12(dry) ),
inference(resolution,[],[f4030,f21449]) ).
fof(f35477,plain,
q46(elysezinfandel),
inference(forward_subsumption_resolution,[],[f35390,f22613]) ).
fof(f35487,plain,
q46(pulignymontrachetwhiteburgundy),
inference(forward_subsumption_resolution,[],[f35380,f22613]) ).
fof(f36041,plain,
( drywine(pulignymontrachetwhiteburgundy)
| ~ wine(pulignymontrachetwhiteburgundy) ),
inference(resolution,[],[f35487,f4192]) ).
fof(f36042,plain,
( tablewine(pulignymontrachetwhiteburgundy)
| ~ wine(pulignymontrachetwhiteburgundy) ),
inference(resolution,[],[f35487,f4296]) ).
fof(f36049,plain,
tablewine(pulignymontrachetwhiteburgundy),
inference(forward_subsumption_resolution,[],[f36042,f7258]) ).
fof(f36050,plain,
drywine(pulignymontrachetwhiteburgundy),
inference(forward_subsumption_resolution,[],[f36041,f7258]) ).
fof(f36052,plain,
( ~ q21(pulignymontrachetwhiteburgundy)
| whitetablewine(pulignymontrachetwhiteburgundy) ),
inference(resolution,[],[f36049,f4317]) ).
fof(f36054,plain,
whitetablewine(pulignymontrachetwhiteburgundy),
inference(forward_subsumption_resolution,[],[f36052,f35195]) ).
fof(f36057,plain,
( drywhitewine(pulignymontrachetwhiteburgundy)
| ~ whitewine(pulignymontrachetwhiteburgundy) ),
inference(resolution,[],[f36050,f4188]) ).
fof(f36059,plain,
drywhitewine(pulignymontrachetwhiteburgundy),
inference(forward_subsumption_resolution,[],[f36057,f7255]) ).
fof(f36154,plain,
( tablewine(elysezinfandel)
| ~ wine(elysezinfandel) ),
inference(resolution,[],[f35477,f4296]) ).
fof(f36157,plain,
tablewine(elysezinfandel),
inference(forward_subsumption_resolution,[],[f36154,f11738]) ).
fof(f37030,plain,
ot____nom10(texasregion),
inference(resolution,[],[f3747,f3330]) ).
fof(f37031,plain,
( $false
| spl0_991 ),
inference(forward_subsumption_resolution,[],[f37030,f33331]) ).
fof(f37032,plain,
spl0_991,
inference(avatar_contradiction_clause,[],[f37031]) ).
fof(f37043,plain,
( q74(stgenevievetexaswhite)
| ~ spl0_992 ),
inference(resolution,[],[f12480,f4140]) ).
fof(f37045,plain,
( spl0_3603
| ~ spl0_992 ),
inference(avatar_split_clause,[],[f37043,f12478,f33345]) ).
fof(f37046,plain,
( texaswine(stgenevievetexaswhite)
| ~ wine(stgenevievetexaswhite)
| ~ spl0_3603 ),
inference(resolution,[],[f33347,f4298]) ).
fof(f37047,plain,
( texaswine(stgenevievetexaswhite)
| ~ spl0_3603 ),
inference(forward_subsumption_resolution,[],[f37046,f5360]) ).
fof(f50734,plain,
zinfandel(mariettazinfandel),
inference(resolution,[],[f3483,f3810]) ).
fof(f50735,plain,
( $false
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f50734,f4737]) ).
fof(f50736,plain,
~ spl0_13,
inference(avatar_contradiction_clause,[],[f50735]) ).
fof(f50755,plain,
( $false
| ~ spl0_14 ),
inference(resolution,[],[f4740,f19336]) ).
fof(f50832,plain,
~ spl0_14,
inference(avatar_contradiction_clause,[],[f50755]) ).
fof(f50833,plain,
( $false
| ~ spl0_15 ),
inference(resolution,[],[f4743,f19169]) ).
fof(f50986,plain,
~ spl0_15,
inference(avatar_contradiction_clause,[],[f50833]) ).
fof(f50987,plain,
( $false
| ~ spl0_16 ),
inference(resolution,[],[f4746,f15068]) ).
fof(f51064,plain,
~ spl0_16,
inference(avatar_contradiction_clause,[],[f50987]) ).
fof(f51065,plain,
( $false
| ~ spl0_17 ),
inference(resolution,[],[f4749,f19168]) ).
fof(f51164,plain,
~ spl0_17,
inference(avatar_contradiction_clause,[],[f51065]) ).
fof(f51165,plain,
( $false
| ~ spl0_18 ),
inference(resolution,[],[f4752,f19159]) ).
fof(f51242,plain,
~ spl0_18,
inference(avatar_contradiction_clause,[],[f51165]) ).
fof(f51243,plain,
( $false
| ~ spl0_19 ),
inference(resolution,[],[f4755,f19340]) ).
fof(f51332,plain,
~ spl0_19,
inference(avatar_contradiction_clause,[],[f51243]) ).
fof(f51333,plain,
( $false
| ~ spl0_20 ),
inference(resolution,[],[f4758,f19161]) ).
fof(f51434,plain,
~ spl0_20,
inference(avatar_contradiction_clause,[],[f51333]) ).
fof(f51435,plain,
( $false
| ~ spl0_21 ),
inference(resolution,[],[f4761,f19154]) ).
fof(f51512,plain,
~ spl0_21,
inference(avatar_contradiction_clause,[],[f51435]) ).
fof(f51513,plain,
( $false
| ~ spl0_22 ),
inference(resolution,[],[f4764,f7258]) ).
fof(f51584,plain,
~ spl0_22,
inference(avatar_contradiction_clause,[],[f51513]) ).
fof(f51585,plain,
( $false
| ~ spl0_23 ),
inference(resolution,[],[f4767,f7255]) ).
fof(f51610,plain,
~ spl0_23,
inference(avatar_contradiction_clause,[],[f51585]) ).
fof(f51611,plain,
( $false
| ~ spl0_24 ),
inference(resolution,[],[f4770,f36054]) ).
fof(f51642,plain,
~ spl0_24,
inference(avatar_contradiction_clause,[],[f51611]) ).
fof(f51643,plain,
( $false
| ~ spl0_25 ),
inference(resolution,[],[f4773,f7291]) ).
fof(f51668,plain,
~ spl0_25,
inference(avatar_contradiction_clause,[],[f51643]) ).
fof(f51805,plain,
zinfandel(elysezinfandel),
inference(resolution,[],[f3480,f3810]) ).
fof(f51806,plain,
q0(elysezinfandel),
inference(resolution,[],[f51805,f3854]) ).
fof(f52931,plain,
ot____nom17(germanyregion),
inference(resolution,[],[f3754,f3337]) ).
fof(f52932,plain,
( $false
| spl0_2089 ),
inference(forward_subsumption_resolution,[],[f52931,f23988]) ).
fof(f52933,plain,
spl0_2089,
inference(avatar_contradiction_clause,[],[f52932]) ).
fof(f52936,plain,
( germanwine(schlossrothermeltrochenbierenausleseriesling)
| ~ wine(schlossrothermeltrochenbierenausleseriesling)
| ~ spl0_2117 ),
inference(resolution,[],[f24120,f4203]) ).
fof(f52937,plain,
( germanwine(schlossrothermeltrochenbierenausleseriesling)
| ~ spl0_2117 ),
inference(forward_subsumption_resolution,[],[f52936,f6480]) ).
fof(f54231,plain,
q71(selaksicewine),
inference(resolution,[],[f9979,f4131]) ).
fof(f54235,plain,
( sweetwine(selaksicewine)
| ~ wine(selaksicewine) ),
inference(resolution,[],[f54231,f4292]) ).
fof(f54236,plain,
sweetwine(selaksicewine),
inference(forward_subsumption_resolution,[],[f54235,f9981]) ).
fof(f54265,plain,
ot____nom38(usregion),
inference(resolution,[],[f3777,f3364]) ).
fof(f54268,plain,
( $false
| spl0_1022 ),
inference(forward_subsumption_resolution,[],[f54265,f23558]) ).
fof(f54269,plain,
spl0_1022,
inference(avatar_contradiction_clause,[],[f54268]) ).
fof(f54276,plain,
( q26(naparegion)
| ~ spl0_1022 ),
inference(forward_subsumption_resolution,[],[f14878,f12840]) ).
fof(f54720,plain,
( q27(naparegion)
| ~ spl0_1022 ),
inference(resolution,[],[f54276,f3930]) ).
fof(f54740,plain,
( $false
| ~ spl0_1022
| spl0_1144 ),
inference(forward_subsumption_resolution,[],[f54720,f14196]) ).
fof(f54741,plain,
( ~ spl0_1022
| spl0_1144 ),
inference(avatar_contradiction_clause,[],[f54740]) ).
fof(f54747,plain,
( q26(bancroftchardonnay)
| ~ spl0_1144 ),
inference(forward_subsumption_resolution,[],[f15425,f14195]) ).
fof(f55046,plain,
( q27(bancroftchardonnay)
| ~ spl0_1144 ),
inference(resolution,[],[f54747,f3930]) ).
fof(f55066,plain,
( spl0_2052
| ~ spl0_1144 ),
inference(avatar_split_clause,[],[f55046,f14194,f23660]) ).
fof(f55399,definition,
( spl0_6515
<=> q41(chateaumargaux) ),
introduced(definition,[new_symbols(definition,[spl0_6515])],[avatar_definition]) ).
fof(f55401,plain,
( q41(chateaumargaux)
| ~ spl0_6515 ),
inference(avatar_component_clause,[],[f55399]) ).
fof(f55784,plain,
( ~ ot____nom5(sevreetmainemuscadet)
| q21(sevreetmainemuscadet)
| ~ kaon2namedobjects(sevreetmainemuscadet) ),
inference(resolution,[],[f34565,f6036]) ).
fof(f55785,plain,
( ~ ot____nom5(sevreetmainemuscadet)
| ~ kaon2namedobjects(sevreetmainemuscadet)
| spl0_145 ),
inference(forward_subsumption_resolution,[],[f55784,f16294]) ).
fof(f55790,plain,
( ~ ot____nom5(sevreetmainemuscadet)
| spl0_145 ),
inference(forward_subsumption_resolution,[],[f55785,f3730]) ).
fof(f55825,plain,
q41(elysezinfandel),
inference(resolution,[],[f4013,f51806]) ).
fof(f55847,plain,
q41(chateaumargaux),
inference(resolution,[],[f4013,f5932]) ).
fof(f55848,plain,
spl0_6515,
inference(avatar_split_clause,[],[f55847,f55399]) ).
fof(f55891,plain,
( redtablewine(elysezinfandel)
| ~ tablewine(elysezinfandel) ),
inference(resolution,[],[f55825,f4255]) ).
fof(f55892,plain,
redtablewine(elysezinfandel),
inference(forward_subsumption_resolution,[],[f55891,f36157]) ).
fof(f55938,plain,
( redwine(chateaumargaux)
| ~ wine(chateaumargaux)
| ~ spl0_6515 ),
inference(resolution,[],[f55401,f4261]) ).
fof(f55949,plain,
( ~ wine(chateaumargaux)
| spl0_1093
| ~ spl0_6515 ),
inference(forward_subsumption_resolution,[],[f55938,f13705]) ).
fof(f55950,plain,
( $false
| ~ spl0_1007
| spl0_1093
| ~ spl0_6515 ),
inference(forward_subsumption_resolution,[],[f55949,f12705]) ).
fof(f55951,plain,
( ~ spl0_1007
| spl0_1093
| ~ spl0_6515 ),
inference(avatar_contradiction_clause,[],[f55950]) ).
fof(f56341,plain,
( ~ ot____nom12(closdevougeotcotesdor)
| q46(closdevougeotcotesdor)
| ~ kaon2namedobjects(closdevougeotcotesdor) ),
inference(resolution,[],[f35377,f11686]) ).
fof(f56350,plain,
( ~ ot____nom12(closdevougeotcotesdor)
| q46(closdevougeotcotesdor) ),
inference(forward_subsumption_resolution,[],[f56341,f3708]) ).
fof(f56400,definition,
( spl0_6612
<=> q46(closdevougeotcotesdor) ),
introduced(definition,[new_symbols(definition,[spl0_6612])],[avatar_definition]) ).
fof(f56402,plain,
( q46(closdevougeotcotesdor)
| ~ spl0_6612 ),
inference(avatar_component_clause,[],[f56400]) ).
fof(f56404,definition,
( spl0_6613
<=> ot____nom12(closdevougeotcotesdor) ),
introduced(definition,[new_symbols(definition,[spl0_6613])],[avatar_definition]) ).
fof(f56406,plain,
( ~ ot____nom12(closdevougeotcotesdor)
| spl0_6613 ),
inference(avatar_component_clause,[],[f56404]) ).
fof(f56407,plain,
( spl0_6612
| ~ spl0_6613 ),
inference(avatar_split_clause,[],[f56350,f56404,f56400]) ).
fof(f65305,plain,
( ~ q27(bancroftchardonnay)
| americanwine(bancroftchardonnay) ),
inference(resolution,[],[f11782,f4148]) ).
fof(f65389,plain,
( americanwine(bancroftchardonnay)
| ~ spl0_2052 ),
inference(forward_subsumption_resolution,[],[f65305,f23662]) ).
fof(f67493,plain,
( ot____nom12(closdevougeotcotesdor)
| ~ kaon2namedobjects(closdevougeotcotesdor) ),
inference(resolution,[],[f4418,f11685]) ).
fof(f67498,plain,
( ~ kaon2namedobjects(closdevougeotcotesdor)
| spl0_6613 ),
inference(forward_subsumption_resolution,[],[f67493,f56406]) ).
fof(f67521,plain,
( $false
| spl0_6613 ),
inference(forward_subsumption_resolution,[],[f67498,f3708]) ).
fof(f67522,plain,
spl0_6613,
inference(avatar_contradiction_clause,[],[f67521]) ).
fof(f67581,plain,
( drywine(closdevougeotcotesdor)
| ~ wine(closdevougeotcotesdor)
| ~ spl0_6612 ),
inference(resolution,[],[f56402,f4192]) ).
fof(f67590,plain,
( drywine(closdevougeotcotesdor)
| ~ spl0_6612 ),
inference(forward_subsumption_resolution,[],[f67581,f11686]) ).
fof(f67601,plain,
( dryredwine(closdevougeotcotesdor)
| ~ redwine(closdevougeotcotesdor)
| ~ spl0_6612 ),
inference(resolution,[],[f67590,f4184]) ).
fof(f67602,plain,
( dryredwine(closdevougeotcotesdor)
| ~ spl0_6612 ),
inference(forward_subsumption_resolution,[],[f67601,f5929]) ).
fof(f67739,plain,
( ot____nom5(sevreetmainemuscadet)
| ~ kaon2namedobjects(sevreetmainemuscadet)
| ~ spl0_1300 ),
inference(resolution,[],[f22078,f4500]) ).
fof(f67744,plain,
( ~ kaon2namedobjects(sevreetmainemuscadet)
| spl0_145
| ~ spl0_1300 ),
inference(forward_subsumption_resolution,[],[f67739,f55790]) ).
fof(f67747,plain,
( $false
| spl0_145
| ~ spl0_1300 ),
inference(forward_subsumption_resolution,[],[f67744,f3730]) ).
fof(f67748,plain,
( spl0_145
| ~ spl0_1300 ),
inference(avatar_contradiction_clause,[],[f67747]) ).
fof(f67749,plain,
( $false
| ~ spl0_26
| ~ spl0_146 ),
inference(forward_subsumption_resolution,[],[f6044,f4776]) ).
fof(f67750,plain,
( ~ spl0_26
| ~ spl0_146 ),
inference(avatar_contradiction_clause,[],[f67749]) ).
fof(f67770,plain,
( $false
| ~ spl0_27 ),
inference(resolution,[],[f4779,f5272]) ).
fof(f67775,plain,
~ spl0_27,
inference(avatar_contradiction_clause,[],[f67770]) ).
fof(f67776,plain,
( $false
| ~ spl0_28
| ~ spl0_849 ),
inference(resolution,[],[f4782,f10371]) ).
fof(f67777,plain,
( ~ spl0_28
| ~ spl0_849 ),
inference(avatar_contradiction_clause,[],[f67776]) ).
fof(f67778,plain,
( $false
| ~ spl0_29 ),
inference(resolution,[],[f4785,f5393]) ).
fof(f67781,plain,
~ spl0_29,
inference(avatar_contradiction_clause,[],[f67778]) ).
fof(f67782,plain,
( $false
| ~ spl0_30 ),
inference(resolution,[],[f4788,f21911]) ).
fof(f67783,plain,
~ spl0_30,
inference(avatar_contradiction_clause,[],[f67782]) ).
fof(f67784,plain,
( $false
| ~ spl0_31
| ~ spl0_3603 ),
inference(resolution,[],[f4791,f37047]) ).
fof(f67785,plain,
( ~ spl0_31
| ~ spl0_3603 ),
inference(avatar_contradiction_clause,[],[f67784]) ).
fof(f67786,plain,
( $false
| ~ spl0_32 ),
inference(resolution,[],[f4794,f36049]) ).
fof(f67871,plain,
~ spl0_32,
inference(avatar_contradiction_clause,[],[f67786]) ).
fof(f67872,plain,
( $false
| ~ spl0_33 ),
inference(resolution,[],[f4797,f54236]) ).
fof(f67883,plain,
~ spl0_33,
inference(avatar_contradiction_clause,[],[f67872]) ).
fof(f67884,plain,
( $false
| ~ spl0_34 ),
inference(resolution,[],[f4800,f6361]) ).
fof(f67887,plain,
~ spl0_34,
inference(avatar_contradiction_clause,[],[f67884]) ).
fof(f67888,plain,
( $false
| ~ spl0_35 ),
inference(resolution,[],[f4803,f5369]) ).
fof(f67889,plain,
~ spl0_35,
inference(avatar_contradiction_clause,[],[f67888]) ).
fof(f67890,plain,
( $false
| ~ spl0_36 ),
inference(resolution,[],[f4806,f15107]) ).
fof(f67901,plain,
~ spl0_36,
inference(avatar_contradiction_clause,[],[f67890]) ).
fof(f67902,plain,
( $false
| ~ spl0_37 ),
inference(resolution,[],[f4809,f7023]) ).
fof(f67905,plain,
~ spl0_37,
inference(avatar_contradiction_clause,[],[f67902]) ).
fof(f67906,plain,
( $false
| ~ spl0_38 ),
inference(resolution,[],[f4812,f15104]) ).
fof(f67913,plain,
~ spl0_38,
inference(avatar_contradiction_clause,[],[f67906]) ).
fof(f67914,plain,
( $false
| ~ spl0_39 ),
inference(resolution,[],[f4815,f5373]) ).
fof(f67915,plain,
~ spl0_39,
inference(avatar_contradiction_clause,[],[f67914]) ).
fof(f67916,plain,
( $false
| ~ spl0_40 ),
inference(resolution,[],[f4818,f5367]) ).
fof(f67917,plain,
~ spl0_40,
inference(avatar_contradiction_clause,[],[f67916]) ).
fof(f67918,plain,
( $false
| ~ spl0_41
| ~ spl0_1387 ),
inference(resolution,[],[f4821,f16935]) ).
fof(f67919,plain,
( ~ spl0_41
| ~ spl0_1387 ),
inference(avatar_contradiction_clause,[],[f67918]) ).
fof(f67920,plain,
( $false
| ~ spl0_42 ),
inference(resolution,[],[f4824,f6477]) ).
fof(f67927,plain,
~ spl0_42,
inference(avatar_contradiction_clause,[],[f67920]) ).
fof(f67928,plain,
( $false
| ~ spl0_43 ),
inference(resolution,[],[f4827,f19171]) ).
fof(f68097,plain,
~ spl0_43,
inference(avatar_contradiction_clause,[],[f67928]) ).
fof(f68119,plain,
( $false
| ~ spl0_44 ),
inference(resolution,[],[f4830,f5372]) ).
fof(f68124,plain,
~ spl0_44,
inference(avatar_contradiction_clause,[],[f68119]) ).
fof(f68148,plain,
( $false
| ~ spl0_45 ),
inference(resolution,[],[f4833,f55892]) ).
fof(f68189,plain,
~ spl0_45,
inference(avatar_contradiction_clause,[],[f68148]) ).
fof(f68192,plain,
( $false
| ~ spl0_46 ),
inference(resolution,[],[f4836,f5355]) ).
fof(f68193,plain,
~ spl0_46,
inference(avatar_contradiction_clause,[],[f68192]) ).
fof(f68194,plain,
( $false
| ~ spl0_47
| ~ spl0_1092 ),
inference(resolution,[],[f4839,f13701]) ).
fof(f68199,plain,
( ~ spl0_47
| ~ spl0_1092 ),
inference(avatar_contradiction_clause,[],[f68194]) ).
fof(f68200,plain,
( $false
| ~ spl0_48 ),
inference(resolution,[],[f4842,f19129]) ).
fof(f68305,plain,
~ spl0_48,
inference(avatar_contradiction_clause,[],[f68200]) ).
fof(f68306,plain,
( $false
| ~ spl0_49 ),
inference(resolution,[],[f4845,f5371]) ).
fof(f68307,plain,
~ spl0_49,
inference(avatar_contradiction_clause,[],[f68306]) ).
fof(f68308,plain,
( $false
| ~ spl0_50 ),
inference(resolution,[],[f4848,f21977]) ).
fof(f68315,plain,
~ spl0_50,
inference(avatar_contradiction_clause,[],[f68308]) ).
fof(f68316,plain,
( $false
| ~ spl0_51
| ~ spl0_1300 ),
inference(resolution,[],[f4851,f16373]) ).
fof(f68317,plain,
( ~ spl0_51
| ~ spl0_1300 ),
inference(avatar_contradiction_clause,[],[f68316]) ).
fof(f68318,plain,
( $false
| ~ spl0_52 ),
inference(resolution,[],[f4854,f6607]) ).
fof(f68321,plain,
~ spl0_52,
inference(avatar_contradiction_clause,[],[f68318]) ).
fof(f68322,plain,
( $false
| ~ spl0_53 ),
inference(resolution,[],[f4857,f5350]) ).
fof(f68323,plain,
~ spl0_53,
inference(avatar_contradiction_clause,[],[f68322]) ).
fof(f68324,plain,
( $false
| ~ spl0_54 ),
inference(resolution,[],[f4860,f5346]) ).
fof(f68325,plain,
~ spl0_54,
inference(avatar_contradiction_clause,[],[f68324]) ).
fof(f68326,plain,
( $false
| ~ spl0_55 ),
inference(resolution,[],[f4863,f5257]) ).
fof(f68327,plain,
~ spl0_55,
inference(avatar_contradiction_clause,[],[f68326]) ).
fof(f68328,plain,
( $false
| ~ spl0_56 ),
inference(resolution,[],[f4866,f6843]) ).
fof(f68333,plain,
~ spl0_56,
inference(avatar_contradiction_clause,[],[f68328]) ).
fof(f68334,plain,
( $false
| ~ spl0_57 ),
inference(resolution,[],[f4869,f5244]) ).
fof(f68335,plain,
~ spl0_57,
inference(avatar_contradiction_clause,[],[f68334]) ).
fof(f68336,plain,
( $false
| ~ spl0_58 ),
inference(resolution,[],[f4872,f5351]) ).
fof(f68339,plain,
~ spl0_58,
inference(avatar_contradiction_clause,[],[f68336]) ).
fof(f68340,plain,
( $false
| ~ spl0_59 ),
inference(resolution,[],[f4875,f5348]) ).
fof(f68341,plain,
~ spl0_59,
inference(avatar_contradiction_clause,[],[f68340]) ).
fof(f68342,plain,
( $false
| ~ spl0_60 ),
inference(resolution,[],[f4878,f5347]) ).
fof(f68347,plain,
~ spl0_60,
inference(avatar_contradiction_clause,[],[f68342]) ).
fof(f68348,plain,
( $false
| ~ spl0_61 ),
inference(resolution,[],[f4881,f5327]) ).
fof(f68351,plain,
~ spl0_61,
inference(avatar_contradiction_clause,[],[f68348]) ).
fof(f68352,plain,
( $false
| ~ spl0_62 ),
inference(resolution,[],[f4884,f5333]) ).
fof(f68353,plain,
~ spl0_62,
inference(avatar_contradiction_clause,[],[f68352]) ).
fof(f68354,plain,
( $false
| ~ spl0_63 ),
inference(resolution,[],[f4887,f5325]) ).
fof(f68355,plain,
~ spl0_63,
inference(avatar_contradiction_clause,[],[f68354]) ).
fof(f68356,plain,
( $false
| ~ spl0_64 ),
inference(resolution,[],[f4890,f19341]) ).
fof(f68465,plain,
~ spl0_64,
inference(avatar_contradiction_clause,[],[f68356]) ).
fof(f68467,plain,
( $false
| ~ spl0_65
| ~ spl0_2117 ),
inference(resolution,[],[f4893,f52937]) ).
fof(f68468,plain,
( ~ spl0_65
| ~ spl0_2117 ),
inference(avatar_contradiction_clause,[],[f68467]) ).
fof(f68470,plain,
( $false
| ~ spl0_66
| ~ spl0_171 ),
inference(resolution,[],[f4896,f6246]) ).
fof(f68471,plain,
( ~ spl0_66
| ~ spl0_171 ),
inference(avatar_contradiction_clause,[],[f68470]) ).
fof(f68472,plain,
( $false
| ~ spl0_67
| ~ spl0_1471 ),
inference(resolution,[],[f4899,f34203]) ).
fof(f68503,plain,
( ~ spl0_67
| ~ spl0_1471 ),
inference(avatar_contradiction_clause,[],[f68472]) ).
fof(f68504,plain,
( $false
| ~ spl0_68 ),
inference(resolution,[],[f4902,f36050]) ).
fof(f68589,plain,
~ spl0_68,
inference(avatar_contradiction_clause,[],[f68504]) ).
fof(f68590,plain,
( $false
| ~ spl0_69 ),
inference(resolution,[],[f4905,f36059]) ).
fof(f68623,plain,
~ spl0_69,
inference(avatar_contradiction_clause,[],[f68590]) ).
fof(f68645,plain,
( $false
| ~ spl0_70
| ~ spl0_6612 ),
inference(resolution,[],[f4908,f67602]) ).
fof(f68648,plain,
( ~ spl0_70
| ~ spl0_6612 ),
inference(avatar_contradiction_clause,[],[f68645]) ).
fof(f68670,plain,
( $false
| ~ spl0_71 ),
inference(resolution,[],[f4911,f5236]) ).
fof(f68671,plain,
~ spl0_71,
inference(avatar_contradiction_clause,[],[f68670]) ).
fof(f68672,plain,
( $false
| ~ spl0_72 ),
inference(resolution,[],[f4914,f5326]) ).
fof(f68679,plain,
~ spl0_72,
inference(avatar_contradiction_clause,[],[f68672]) ).
fof(f68680,plain,
( $false
| ~ spl0_73 ),
inference(resolution,[],[f4917,f5354]) ).
fof(f68681,plain,
~ spl0_73,
inference(avatar_contradiction_clause,[],[f68680]) ).
fof(f68682,plain,
( $false
| ~ spl0_74 ),
inference(resolution,[],[f4920,f5328]) ).
fof(f68683,plain,
~ spl0_74,
inference(avatar_contradiction_clause,[],[f68682]) ).
fof(f68684,plain,
( $false
| ~ spl0_75 ),
inference(resolution,[],[f4923,f6109]) ).
fof(f68687,plain,
~ spl0_75,
inference(avatar_contradiction_clause,[],[f68684]) ).
fof(f68689,plain,
( $false
| ~ spl0_76 ),
inference(resolution,[],[f4926,f14412]) ).
fof(f68702,plain,
~ spl0_76,
inference(avatar_contradiction_clause,[],[f68689]) ).
fof(f68722,plain,
( $false
| ~ spl0_77
| ~ spl0_2989 ),
inference(resolution,[],[f4929,f33652]) ).
fof(f68731,plain,
( ~ spl0_77
| ~ spl0_2989 ),
inference(avatar_contradiction_clause,[],[f68722]) ).
fof(f68750,plain,
( $false
| ~ spl0_78 ),
inference(resolution,[],[f4932,f8164]) ).
fof(f68761,plain,
~ spl0_78,
inference(avatar_contradiction_clause,[],[f68750]) ).
fof(f68762,plain,
( $false
| ~ spl0_79 ),
inference(resolution,[],[f4935,f5231]) ).
fof(f68763,plain,
~ spl0_79,
inference(avatar_contradiction_clause,[],[f68762]) ).
fof(f68764,plain,
( $false
| ~ spl0_80 ),
inference(resolution,[],[f4938,f5356]) ).
fof(f68765,plain,
~ spl0_80,
inference(avatar_contradiction_clause,[],[f68764]) ).
fof(f68766,plain,
( $false
| ~ spl0_81 ),
inference(resolution,[],[f4941,f5352]) ).
fof(f68767,plain,
~ spl0_81,
inference(avatar_contradiction_clause,[],[f68766]) ).
fof(f68768,plain,
( $false
| ~ spl0_82 ),
inference(resolution,[],[f4944,f7256]) ).
fof(f68775,plain,
~ spl0_82,
inference(avatar_contradiction_clause,[],[f68768]) ).
fof(f68776,plain,
( $false
| ~ spl0_83 ),
inference(resolution,[],[f4947,f5384]) ).
fof(f68783,plain,
~ spl0_83,
inference(avatar_contradiction_clause,[],[f68776]) ).
fof(f68788,plain,
( $false
| ~ spl0_84
| ~ spl0_2052 ),
inference(resolution,[],[f4950,f65389]) ).
fof(f68827,plain,
( ~ spl0_84
| ~ spl0_2052 ),
inference(avatar_contradiction_clause,[],[f68788]) ).
fof(f68833,plain,
( $false
| ~ spl0_1 ),
inference(resolution,[],[f4701,f14410]) ).
fof(f68936,plain,
~ spl0_1,
inference(avatar_contradiction_clause,[],[f68833]) ).
cnf(s1,plain,
( spl0_77
| spl0_2
| spl0_3
| spl0_4
| spl0_5
| spl0_6
| spl0_7
| spl0_8
| spl0_9
| spl0_10
| spl0_11
| spl0_12
| spl0_13
| spl0_14
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_19
| spl0_20
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_25
| spl0_26
| spl0_27
| spl0_28
| spl0_29
| spl0_30
| spl0_31
| spl0_32
| spl0_33
| spl0_34
| spl0_35
| spl0_36
| spl0_37
| spl0_38
| spl0_39
| spl0_40
| spl0_41
| spl0_42
| spl0_43
| spl0_44
| spl0_45
| spl0_46
| spl0_47
| spl0_48
| spl0_49
| spl0_50
| spl0_51
| spl0_52
| spl0_53
| spl0_54
| spl0_55
| spl0_56
| spl0_57
| spl0_58
| spl0_59
| spl0_60
| spl0_61
| spl0_62
| spl0_63
| spl0_64
| spl0_65
| spl0_66
| spl0_67
| spl0_68
| spl0_69
| spl0_70
| spl0_71
| spl0_72
| spl0_73
| spl0_74
| spl0_75
| spl0_76
| spl0_1
| spl0_77
| spl0_78
| spl0_79
| spl0_80
| spl0_81
| spl0_82
| spl0_83
| spl0_84 ),
inference(sat_conversion,[],[f4951]) ).
cnf(s2,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4
| spl0_5
| spl0_6
| spl0_7
| spl0_8
| spl0_9
| spl0_10
| spl0_11
| spl0_12
| spl0_13
| spl0_14
| spl0_15
| spl0_16
| spl0_17
| spl0_18
| spl0_19
| spl0_20
| spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_25
| spl0_26
| spl0_27
| spl0_28
| spl0_29
| spl0_30
| spl0_31
| spl0_32
| spl0_33
| spl0_34
| spl0_35
| spl0_36
| spl0_37
| spl0_38
| spl0_39
| spl0_40
| spl0_41
| spl0_42
| spl0_43
| spl0_44
| spl0_45
| spl0_46
| spl0_47
| spl0_48
| spl0_49
| spl0_50
| spl0_51
| spl0_52
| spl0_53
| spl0_54
| spl0_55
| spl0_56
| spl0_57
| spl0_58
| spl0_59
| spl0_60
| spl0_61
| spl0_62
| spl0_63
| spl0_64
| spl0_65
| spl0_66
| spl0_67
| spl0_68
| spl0_69
| spl0_70
| spl0_71
| spl0_72
| spl0_73
| spl0_74
| spl0_75
| spl0_76
| spl0_77
| spl0_78
| spl0_79
| spl0_80
| spl0_81
| spl0_82
| spl0_83
| spl0_84 ),
inference(rat,[],[s1]) ).
cnf(s3,plain,
~ spl0_2,
inference(sat_conversion,[],[f5261]) ).
cnf(s4,plain,
~ spl0_3,
inference(sat_conversion,[],[f5280]) ).
cnf(s5,plain,
~ spl0_4,
inference(sat_conversion,[],[f5293]) ).
cnf(s6,plain,
~ spl0_5,
inference(sat_conversion,[],[f5335]) ).
cnf(s7,plain,
~ spl0_6,
inference(sat_conversion,[],[f5365]) ).
cnf(s38,plain,
( ~ spl0_145
| spl0_146 ),
inference(sat_conversion,[],[f6045]) ).
cnf(s437,plain,
( ~ spl0_848
| spl0_849 ),
inference(sat_conversion,[],[f10372]) ).
cnf(s547,plain,
( ~ spl0_991
| spl0_992 ),
inference(sat_conversion,[],[f12481]) ).
cnf(s606,plain,
( spl0_1092
| ~ spl0_1093 ),
inference(sat_conversion,[],[f13706]) ).
cnf(s607,plain,
spl0_1007,
inference(sat_conversion,[],[f13708]) ).
cnf(s1008,plain,
spl0_887,
inference(sat_conversion,[],[f20762]) ).
cnf(s1021,plain,
spl0_171,
inference(sat_conversion,[],[f21052]) ).
cnf(s1056,plain,
~ spl0_7,
inference(sat_conversion,[],[f21535]) ).
cnf(s1096,plain,
~ spl0_8,
inference(sat_conversion,[],[f21621]) ).
cnf(s1148,plain,
~ spl0_9,
inference(sat_conversion,[],[f21726]) ).
cnf(s1191,plain,
~ spl0_10,
inference(sat_conversion,[],[f21816]) ).
cnf(s1192,plain,
~ spl0_11,
inference(sat_conversion,[],[f21822]) ).
cnf(s1233,plain,
~ spl0_12,
inference(sat_conversion,[],[f21908]) ).
cnf(s1235,plain,
spl0_1387,
inference(sat_conversion,[],[f21959]) ).
cnf(s1240,plain,
spl0_1300,
inference(sat_conversion,[],[f22075]) ).
cnf(s1486,plain,
( ~ spl0_2089
| spl0_2117 ),
inference(sat_conversion,[],[f24121]) ).
cnf(s2214,plain,
( spl0_1142
| ~ spl0_2966 ),
inference(sat_conversion,[],[f29561]) ).
cnf(s2229,plain,
( spl0_848
| ~ spl0_887 ),
inference(sat_conversion,[],[f29700]) ).
cnf(s2612,plain,
spl0_2966,
inference(sat_conversion,[],[f32939]) ).
cnf(s2703,plain,
( ~ spl0_1142
| spl0_2989 ),
inference(sat_conversion,[],[f33650]) ).
cnf(s2761,plain,
spl0_1471,
inference(sat_conversion,[],[f34188]) ).
cnf(s2991,plain,
spl0_991,
inference(sat_conversion,[],[f37032]) ).
cnf(s2993,plain,
( ~ spl0_992
| spl0_3603 ),
inference(sat_conversion,[],[f37045]) ).
cnf(s4692,plain,
~ spl0_13,
inference(sat_conversion,[],[f50736]) ).
cnf(s4735,plain,
~ spl0_14,
inference(sat_conversion,[],[f50832]) ).
cnf(s4812,plain,
~ spl0_15,
inference(sat_conversion,[],[f50986]) ).
cnf(s4851,plain,
~ spl0_16,
inference(sat_conversion,[],[f51064]) ).
cnf(s4901,plain,
~ spl0_17,
inference(sat_conversion,[],[f51164]) ).
cnf(s4940,plain,
~ spl0_18,
inference(sat_conversion,[],[f51242]) ).
cnf(s4985,plain,
~ spl0_19,
inference(sat_conversion,[],[f51332]) ).
cnf(s5036,plain,
~ spl0_20,
inference(sat_conversion,[],[f51434]) ).
cnf(s5075,plain,
~ spl0_21,
inference(sat_conversion,[],[f51512]) ).
cnf(s5111,plain,
~ spl0_22,
inference(sat_conversion,[],[f51584]) ).
cnf(s5124,plain,
~ spl0_23,
inference(sat_conversion,[],[f51610]) ).
cnf(s5140,plain,
~ spl0_24,
inference(sat_conversion,[],[f51642]) ).
cnf(s5153,plain,
~ spl0_25,
inference(sat_conversion,[],[f51668]) ).
cnf(s5277,plain,
spl0_2089,
inference(sat_conversion,[],[f52933]) ).
cnf(s5438,plain,
spl0_1022,
inference(sat_conversion,[],[f54269]) ).
cnf(s5471,plain,
( ~ spl0_1022
| spl0_1144 ),
inference(sat_conversion,[],[f54741]) ).
cnf(s5485,plain,
( ~ spl0_1144
| spl0_2052 ),
inference(sat_conversion,[],[f55066]) ).
cnf(s5542,plain,
spl0_6515,
inference(sat_conversion,[],[f55848]) ).
cnf(s5567,plain,
( ~ spl0_1007
| spl0_1093
| ~ spl0_6515 ),
inference(sat_conversion,[],[f55951]) ).
cnf(s5593,plain,
( spl0_6612
| ~ spl0_6613 ),
inference(sat_conversion,[],[f56407]) ).
cnf(s6655,plain,
spl0_6613,
inference(sat_conversion,[],[f67522]) ).
cnf(s6679,plain,
( spl0_145
| ~ spl0_1300 ),
inference(sat_conversion,[],[f67748]) ).
cnf(s6680,plain,
( ~ spl0_26
| ~ spl0_146 ),
inference(sat_conversion,[],[f67750]) ).
cnf(s6687,plain,
~ spl0_27,
inference(sat_conversion,[],[f67775]) ).
cnf(s6688,plain,
( ~ spl0_28
| ~ spl0_849 ),
inference(sat_conversion,[],[f67777]) ).
cnf(s6690,plain,
~ spl0_29,
inference(sat_conversion,[],[f67781]) ).
cnf(s6691,plain,
~ spl0_30,
inference(sat_conversion,[],[f67783]) ).
cnf(s6692,plain,
( ~ spl0_31
| ~ spl0_3603 ),
inference(sat_conversion,[],[f67785]) ).
cnf(s6735,plain,
~ spl0_32,
inference(sat_conversion,[],[f67871]) ).
cnf(s6741,plain,
~ spl0_33,
inference(sat_conversion,[],[f67883]) ).
cnf(s6743,plain,
~ spl0_34,
inference(sat_conversion,[],[f67887]) ).
cnf(s6744,plain,
~ spl0_35,
inference(sat_conversion,[],[f67889]) ).
cnf(s6750,plain,
~ spl0_36,
inference(sat_conversion,[],[f67901]) ).
cnf(s6752,plain,
~ spl0_37,
inference(sat_conversion,[],[f67905]) ).
cnf(s6756,plain,
~ spl0_38,
inference(sat_conversion,[],[f67913]) ).
cnf(s6757,plain,
~ spl0_39,
inference(sat_conversion,[],[f67915]) ).
cnf(s6758,plain,
~ spl0_40,
inference(sat_conversion,[],[f67917]) ).
cnf(s6759,plain,
( ~ spl0_41
| ~ spl0_1387 ),
inference(sat_conversion,[],[f67919]) ).
cnf(s6763,plain,
~ spl0_42,
inference(sat_conversion,[],[f67927]) ).
cnf(s6848,plain,
~ spl0_43,
inference(sat_conversion,[],[f68097]) ).
cnf(s6851,plain,
~ spl0_44,
inference(sat_conversion,[],[f68124]) ).
cnf(s6893,plain,
~ spl0_45,
inference(sat_conversion,[],[f68189]) ).
cnf(s6896,plain,
~ spl0_46,
inference(sat_conversion,[],[f68193]) ).
cnf(s6899,plain,
( ~ spl0_47
| ~ spl0_1092 ),
inference(sat_conversion,[],[f68199]) ).
cnf(s6952,plain,
~ spl0_48,
inference(sat_conversion,[],[f68305]) ).
cnf(s6953,plain,
~ spl0_49,
inference(sat_conversion,[],[f68307]) ).
cnf(s6957,plain,
~ spl0_50,
inference(sat_conversion,[],[f68315]) ).
cnf(s6958,plain,
( ~ spl0_51
| ~ spl0_1300 ),
inference(sat_conversion,[],[f68317]) ).
cnf(s6960,plain,
~ spl0_52,
inference(sat_conversion,[],[f68321]) ).
cnf(s6961,plain,
~ spl0_53,
inference(sat_conversion,[],[f68323]) ).
cnf(s6962,plain,
~ spl0_54,
inference(sat_conversion,[],[f68325]) ).
cnf(s6963,plain,
~ spl0_55,
inference(sat_conversion,[],[f68327]) ).
cnf(s6966,plain,
~ spl0_56,
inference(sat_conversion,[],[f68333]) ).
cnf(s6967,plain,
~ spl0_57,
inference(sat_conversion,[],[f68335]) ).
cnf(s6969,plain,
~ spl0_58,
inference(sat_conversion,[],[f68339]) ).
cnf(s6970,plain,
~ spl0_59,
inference(sat_conversion,[],[f68341]) ).
cnf(s6973,plain,
~ spl0_60,
inference(sat_conversion,[],[f68347]) ).
cnf(s6975,plain,
~ spl0_61,
inference(sat_conversion,[],[f68351]) ).
cnf(s6976,plain,
~ spl0_62,
inference(sat_conversion,[],[f68353]) ).
cnf(s6977,plain,
~ spl0_63,
inference(sat_conversion,[],[f68355]) ).
cnf(s7032,plain,
~ spl0_64,
inference(sat_conversion,[],[f68465]) ).
cnf(s7033,plain,
( ~ spl0_65
| ~ spl0_2117 ),
inference(sat_conversion,[],[f68468]) ).
cnf(s7035,plain,
( ~ spl0_66
| ~ spl0_171 ),
inference(sat_conversion,[],[f68471]) ).
cnf(s7051,plain,
( ~ spl0_67
| ~ spl0_1471 ),
inference(sat_conversion,[],[f68503]) ).
cnf(s7094,plain,
~ spl0_68,
inference(sat_conversion,[],[f68589]) ).
cnf(s7111,plain,
~ spl0_69,
inference(sat_conversion,[],[f68623]) ).
cnf(s7113,plain,
( ~ spl0_70
| ~ spl0_6612 ),
inference(sat_conversion,[],[f68648]) ).
cnf(s7135,plain,
~ spl0_71,
inference(sat_conversion,[],[f68671]) ).
cnf(s7139,plain,
~ spl0_72,
inference(sat_conversion,[],[f68679]) ).
cnf(s7140,plain,
~ spl0_73,
inference(sat_conversion,[],[f68681]) ).
cnf(s7141,plain,
~ spl0_74,
inference(sat_conversion,[],[f68683]) ).
cnf(s7143,plain,
~ spl0_75,
inference(sat_conversion,[],[f68687]) ).
cnf(s7150,plain,
~ spl0_76,
inference(sat_conversion,[],[f68702]) ).
cnf(s7156,plain,
( ~ spl0_77
| ~ spl0_2989 ),
inference(sat_conversion,[],[f68731]) ).
cnf(s7180,plain,
~ spl0_78,
inference(sat_conversion,[],[f68761]) ).
cnf(s7181,plain,
~ spl0_79,
inference(sat_conversion,[],[f68763]) ).
cnf(s7182,plain,
~ spl0_80,
inference(sat_conversion,[],[f68765]) ).
cnf(s7183,plain,
~ spl0_81,
inference(sat_conversion,[],[f68767]) ).
cnf(s7187,plain,
~ spl0_82,
inference(sat_conversion,[],[f68775]) ).
cnf(s7191,plain,
~ spl0_83,
inference(sat_conversion,[],[f68783]) ).
cnf(s7211,plain,
( ~ spl0_84
| ~ spl0_2052 ),
inference(sat_conversion,[],[f68827]) ).
cnf(s7267,plain,
~ spl0_1,
inference(sat_conversion,[],[f68936]) ).
cnf(s7294,plain,
spl0_6612,
inference(rat,[],[s5593,s6655]) ).
cnf(s7295,plain,
~ spl0_70,
inference(rat,[],[s7113,s7294]) ).
cnf(s7319,plain,
spl0_1144,
inference(rat,[],[s5471,s5438]) ).
cnf(s7327,plain,
spl0_2052,
inference(rat,[],[s5485,s7319]) ).
cnf(s7342,plain,
~ spl0_84,
inference(rat,[],[s7211,s7327]) ).
cnf(s7373,plain,
~ spl0_67,
inference(rat,[],[s7051,s2761]) ).
cnf(s7388,plain,
spl0_1142,
inference(rat,[],[s2214,s2612]) ).
cnf(s7390,plain,
spl0_2989,
inference(rat,[],[s2703,s7388]) ).
cnf(s7397,plain,
~ spl0_77,
inference(rat,[],[s7156,s7390]) ).
cnf(s7425,plain,
spl0_2117,
inference(rat,[],[s1486,s5277]) ).
cnf(s7426,plain,
~ spl0_65,
inference(rat,[],[s7033,s7425]) ).
cnf(s7447,plain,
~ spl0_51,
inference(rat,[],[s6958,s1240]) ).
cnf(s7450,plain,
spl0_145,
inference(rat,[],[s6679,s1240]) ).
cnf(s7452,plain,
~ spl0_41,
inference(rat,[],[s6759,s1235]) ).
cnf(s7453,plain,
~ spl0_66,
inference(rat,[],[s7035,s1021]) ).
cnf(s7454,plain,
spl0_848,
inference(rat,[],[s2229,s1008]) ).
cnf(s7480,plain,
spl0_1093,
inference(rat,[],[s5567,s5542,s607]) ).
cnf(s7483,plain,
spl0_1092,
inference(rat,[],[s606,s7480]) ).
cnf(s7484,plain,
~ spl0_47,
inference(rat,[],[s6899,s7483]) ).
cnf(s7507,plain,
spl0_992,
inference(rat,[],[s547,s2991]) ).
cnf(s7508,plain,
spl0_3603,
inference(rat,[],[s2993,s7507]) ).
cnf(s7509,plain,
~ spl0_31,
inference(rat,[],[s6692,s7508]) ).
cnf(s7524,plain,
spl0_849,
inference(rat,[],[s437,s7454]) ).
cnf(s7525,plain,
~ spl0_28,
inference(rat,[],[s6688,s7524]) ).
cnf(s7539,plain,
spl0_146,
inference(rat,[],[s38,s7450]) ).
cnf(s7540,plain,
~ spl0_26,
inference(rat,[],[s6680,s7539]) ).
cnf(s7542,plain,
$false,
inference(rat,[],[s2,s7342,s7191,s7187,s7183,s7182,s7181,s7180,s7397,s7150,s7143,s7141,s7140,s7139,s7135,s7295,s7111,s7094,s7373,s7453,s7426,s7032,s6977,s6976,s6975,s6973,s6970,s6969,s6967,s6966,s6963,s6962,s6961,s6960,s7447,s6957,s6953,s6952,s7484,s6896,s6893,s6851,s6848,s6763,s7452,s6758,s6757,s6756,s6752,s6750,s6744,s6743,s6741,s6735,s7509,s6691,s6690,s7525,s6687,s7540,s5153,s5140,s5124,s5111,s5075,s5036,s4985,s4940,s4901,s4851,s4812,s4735,s4692,s1233,s1192,s1191,s1148,s1096,s1056,s7,s6,s5,s4,s3,s7267]) ).
fof(f68937,plain,
$false,
inference(avatar_sat_refutation,[],[s7542]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRD001+1 : TPTP v9.3.1. Released v6.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.36 % Computer : n008.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8046.5625MB
% 0.12/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Sun Sep 27 22:16:39 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.39 Running first-order theorem proving
% 0.14/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.89/2.44 % (1658456)Detected formulas, will run a generic FOF schedule.
% 10.89/2.44 % (1658462)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1365373081:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.89/2.44 % (1658465)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2283425903:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.89/2.44 % (1658467)dis-21_1_sil=8000:lcm=predicate:random_seed=3553513475:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 10.89/2.44 % (1658461)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1315083820:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.89/2.44 % (1658464)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=539572531:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.89/2.44 % (1658463)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=486965206:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.89/2.44 % (1658466)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1933247937:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.89/2.44 % (1658464)Refutation not found, incomplete strategy
% 10.89/2.44 % (1658464)------------------------------
% 10.89/2.44 % (1658464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/2.44 % (1658464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/2.44 % (1658464)CaDiCaL version: 2.1.3
% 10.89/2.44 % (1658464)Termination reason: Refutation not found, incomplete strategy
% 10.89/2.44 % (1658464)Time elapsed: 0.016 s
% 10.89/2.44 % (1658464)Peak memory usage: 89 MB
% 10.89/2.44 % (1658464)Instructions burned: 32 (million)
% 10.89/2.44 % (1658465)Instruction limit reached!
% 10.89/2.44 % (1658465)------------------------------
% 10.89/2.44 % (1658465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/2.44 % (1658465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/2.44 % (1658465)CaDiCaL version: 2.1.3
% 10.89/2.44 % (1658465)Termination reason: Instruction limit
% 10.89/2.44 % (1658465)Termination phase: Saturation
% 10.89/2.44 % (1658465)Time elapsed: 0.056 s
% 10.89/2.44 % (1658465)Peak memory usage: 89 MB
% 10.89/2.44 % (1658465)Instructions burned: 121 (million)
% 10.89/2.44 % (1658467)Instruction limit reached!
% 10.89/2.44 % (1658467)------------------------------
% 10.89/2.44 % (1658467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/2.44 % (1658467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/2.44 % (1658467)CaDiCaL version: 2.1.3
% 10.89/2.44 % (1658467)Termination reason: Instruction limit
% 10.89/2.44 % (1658467)Termination phase: Saturation
% 10.89/2.44 % (1658467)Time elapsed: 0.066 s
% 10.89/2.44 % (1658467)Peak memory usage: 91 MB
% 10.89/2.44 % (1658467)Instructions burned: 131 (million)
% 10.89/2.44 % (1658466)Instruction limit reached!
% 10.89/2.44 % (1658466)------------------------------
% 10.89/2.44 % (1658466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/2.44 % (1658466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/2.44 % (1658466)CaDiCaL version: 2.1.3
% 10.89/2.44 % (1658466)Termination reason: Instruction limit
% 10.89/2.44 % (1658466)Termination phase: Saturation
% 10.89/2.44 % (1658466)Time elapsed: 0.079 s
% 10.89/2.44 % (1658466)Peak memory usage: 91 MB
% 10.89/2.44 % (1658466)Instructions burned: 140 (million)
% 10.89/2.44 % (1658475)lrs+10_1_sil=8000:sp=occurrence:random_seed=3251127830:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 10.89/2.44 % (1658476)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3615760224:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 10.89/2.44 % (1658476)Refutation not found, incomplete strategy
% 10.89/2.44 % (1658476)------------------------------
% 10.89/2.44 % (1658476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.89/2.44 % (1658476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.89/2.44 % (1658476)CaDiCaL version: 2.1.3
% 10.89/2.44 % (1658476)Termination reason: Refutation not found, incomplete strategy
% 16.32/3.62 % (1658476)Time elapsed: 0.012 s
% 16.32/3.62 % (1658476)Peak memory usage: 90 MB
% 16.32/3.62 % (1658476)Instructions burned: 22 (million)
% 16.32/3.62 % (1658477)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2188652052:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 16.32/3.62 % (1658477)Refutation not found, incomplete strategy
% 16.32/3.62 % (1658477)------------------------------
% 16.32/3.62 % (1658477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.32/3.62 % (1658477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/3.62 % (1658477)CaDiCaL version: 2.1.3
% 16.32/3.62 % (1658477)Termination reason: Refutation not found, incomplete strategy
% 16.32/3.62 % (1658477)Time elapsed: 0.011 s
% 16.32/3.62 % (1658477)Peak memory usage: 90 MB
% 16.32/3.62 % (1658477)Instructions burned: 19 (million)
% 16.32/3.62 % (1658464)------------------------------
% 16.32/3.62 % (1658464)------------------------------
% 16.32/3.62 % (1658475)Instruction limit reached!
% 16.32/3.62 % (1658475)------------------------------
% 16.32/3.62 % (1658475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.32/3.62 % (1658475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/3.62 % (1658475)CaDiCaL version: 2.1.3
% 16.32/3.62 % (1658475)Termination reason: Instruction limit
% 16.32/3.62 % (1658475)Termination phase: Saturation
% 16.32/3.62 % (1658475)Time elapsed: 0.151 s
% 16.32/3.62 % (1658475)Peak memory usage: 96 MB
% 16.32/3.62 % (1658475)Instructions burned: 287 (million)
% 16.32/3.62 [W927 22:16:40.430843859 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 16.32/3.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 16.32/3.62 [W927 22:16:40.430890943 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 16.32/3.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 16.32/3.62 % (1658481)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3580180060:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 16.32/3.62 % (1658476)------------------------------
% 16.32/3.62 % (1658476)------------------------------
% 16.32/3.62 % (1658477)------------------------------
% 16.32/3.62 % (1658477)------------------------------
% 16.32/3.62 % (1658482)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=274569630:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 16.32/3.62 % (1658482)Refutation not found, incomplete strategy
% 16.32/3.62 % (1658482)------------------------------
% 16.32/3.62 % (1658482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.32/3.62 % (1658482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/3.62 % (1658482)CaDiCaL version: 2.1.3
% 16.32/3.62 % (1658482)Termination reason: Refutation not found, incomplete strategy
% 16.32/3.62 % (1658482)Time elapsed: 0.014 s
% 16.32/3.62 % (1658482)Peak memory usage: 89 MB
% 16.32/3.62 % (1658482)Instructions burned: 26 (million)
% 16.32/3.62 % (1658481)Instruction limit reached!
% 16.32/3.62 % (1658481)------------------------------
% 16.32/3.62 % (1658481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.32/3.62 % (1658481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/3.62 % (1658481)CaDiCaL version: 2.1.3
% 16.32/3.62 % (1658481)Termination reason: Instruction limit
% 16.32/3.62 % (1658481)Termination phase: Saturation
% 16.32/3.62 % (1658481)Time elapsed: 0.128 s
% 16.32/3.62 % (1658481)Peak memory usage: 92 MB
% 16.32/3.62 % (1658481)Instructions burned: 249 (million)
% 16.32/3.62 % (1658484)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4115121816:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 16.32/3.62 % (1658485)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3417394615:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 16.32/3.62 % (1658485)Instruction limit reached!
% 16.32/3.62 % (1658485)------------------------------
% 16.32/3.62 % (1658485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.32/3.62 % (1658485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/3.62 % (1658485)CaDiCaL version: 2.1.3
% 16.32/3.62 % (1658485)Termination reason: Instruction limit
% 16.32/3.62 % (1658485)Termination phase: Saturation
% 16.32/3.62 % (1658485)Time elapsed: 0.058 s
% 16.32/3.62 % (1658485)Peak memory usage: 91 MB
% 16.32/3.62 % (1658485)Instructions burned: 115 (million)
% 16.32/3.62 % (1658487)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1616607914:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 16.32/3.62 % (1658482)------------------------------
% 16.32/3.62 % (1658482)------------------------------
% 16.32/3.62 % (1658487)Instruction limit reached!
% 16.32/3.62 % (1658487)------------------------------
% 16.32/3.62 % (1658487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.32/3.62 % (1658487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/3.62 % (1658487)CaDiCaL version: 2.1.3
% 16.32/3.62 % (1658487)Termination reason: Instruction limit
% 16.32/3.62 % (1658487)Termination phase: Saturation
% 16.32/3.62 % (1658487)Time elapsed: 0.067 s
% 16.32/3.62 % (1658487)Peak memory usage: 90 MB
% 16.32/3.62 % (1658487)Instructions burned: 129 (million)
% 16.32/3.62 % (1658490)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1533134160:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 16.32/3.62 % (1658490)Refutation not found, incomplete strategy
% 16.32/3.62 % (1658490)------------------------------
% 16.32/3.62 % (1658490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.32/3.62 % (1658490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/3.62 % (1658490)CaDiCaL version: 2.1.3
% 16.32/3.62 % (1658490)Termination reason: Refutation not found, incomplete strategy
% 16.32/3.62 % (1658490)Time elapsed: 0.010 s
% 16.32/3.62 % (1658490)Peak memory usage: 90 MB
% 16.32/3.62 % (1658490)Instructions burned: 20 (million)
% 16.32/3.62 % (1658492)lrs+10_1_sil=8000:sp=occurrence:random_seed=2685276354:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 16.32/3.62 % (1658493)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4044165130:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 16.32/3.62 % (1658493)Refutation not found, incomplete strategy
% 16.32/3.62 % (1658493)------------------------------
% 16.32/3.62 % (1658493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.32/3.62 % (1658493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/3.62 % (1658493)CaDiCaL version: 2.1.3
% 16.32/3.62 % (1658493)Termination reason: Refutation not found, incomplete strategy
% 16.32/3.62 % (1658493)Time elapsed: 0.008 s
% 16.32/3.62 % (1658493)Peak memory usage: 89 MB
% 16.32/3.62 % (1658493)Instructions burned: 13 (million)
% 16.32/3.62 % (1658490)------------------------------
% 16.32/3.62 % (1658490)------------------------------
% 16.32/3.62 % (1658493)------------------------------
% 16.32/3.62 % (1658493)------------------------------
% 16.32/3.62 % (1658497)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2157239561:i=5202:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/5202Mi)
% 16.32/3.62 % (1658492)Instruction limit reached!
% 16.32/3.62 % (1658492)------------------------------
% 16.32/3.62 % (1658492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.32/3.62 % (1658492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/3.62 % (1658492)CaDiCaL version: 2.1.3
% 16.32/3.62 % (1658492)Termination reason: Instruction limit
% 16.32/3.62 % (1658492)Termination phase: Saturation
% 16.32/3.62 % (1658492)Time elapsed: 0.387 s
% 16.32/3.62 % (1658492)Peak memory usage: 105 MB
% 16.32/3.62 % (1658492)Instructions burned: 908 (million)
% 16.32/3.62 % (1658498)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2889070144:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2985 on theBenchmark for (2985ds/134Mi)
% 16.32/3.62 % (1658498)Refutation not found, incomplete strategy
% 16.32/3.62 % (1658498)------------------------------
% 16.32/3.62 % (1658498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.32/3.62 % (1658498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/3.62 % (1658498)CaDiCaL version: 2.1.3
% 16.32/3.62 % (1658498)Termination reason: Refutation not found, incomplete strategy
% 16.32/3.62 % (1658498)Time elapsed: 0.013 s
% 16.32/3.62 % (1658498)Peak memory usage: 90 MB
% 16.32/3.62 % (1658498)Instructions burned: 22 (million)
% 16.32/3.62 % (1658500)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1102142456:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 16.32/3.62 % (1658500)Refutation not found, incomplete strategy
% 16.32/3.62 % (1658500)------------------------------
% 16.32/3.62 % (1658500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.32/3.62 % (1658500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/3.62 % (1658500)CaDiCaL version: 2.1.3
% 16.32/3.62 % (1658500)Termination reason: Refutation not found, incomplete strategy
% 16.32/3.62 % (1658500)Time elapsed: 0.026 s
% 16.32/3.62 % (1658500)Peak memory usage: 91 MB
% 16.32/3.62 % (1658500)Instructions burned: 51 (million)
% 16.32/3.62 % (1658498)------------------------------
% 16.32/3.62 % (1658498)------------------------------
% 16.32/3.62 % (1658500)------------------------------
% 16.32/3.62 % (1658500)------------------------------
% 16.32/3.62 % (1658503)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=993635677:st=3:i=13193:sd=3:ss=axioms_2981 on theBenchmark for (2981ds/13193Mi)
% 16.32/3.62 % (1658504)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=3379274347:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/125Mi)
% 16.32/3.62 % (1658504)Instruction limit reached!
% 16.32/3.62 % (1658504)------------------------------
% 16.32/3.62 % (1658504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.32/3.62 % (1658504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/3.62 % (1658504)CaDiCaL version: 2.1.3
% 16.32/3.62 % (1658504)Termination reason: Instruction limit
% 16.32/3.62 % (1658504)Termination phase: Saturation
% 16.32/3.62 % (1658504)Time elapsed: 0.061 s
% 16.32/3.62 % (1658504)Peak memory usage: 92 MB
% 16.32/3.62 % (1658504)Instructions burned: 126 (million)
% 16.32/3.62 % (1658484)Instruction limit reached!
% 16.32/3.62 % (1658484)------------------------------
% 16.32/3.62 % (1658484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.32/3.62 % (1658484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/3.62 % (1658484)CaDiCaL version: 2.1.3
% 16.32/3.62 % (1658484)Termination reason: Instruction limit
% 16.32/3.62 % (1658484)Termination phase: Saturation
% 16.32/3.62 % (1658484)Time elapsed: 1.518 s
% 16.32/3.62 % (1658484)Peak memory usage: 149 MB
% 16.32/3.62 % (1658484)Instructions burned: 2351 (million)
% 16.32/3.62 % (1658507)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=643362062:i=134:gtgl=5:slsql=off:gtg=exists_sym_2978 on theBenchmark for (2978ds/134Mi)
% 16.32/3.62 % (1658507)Instruction limit reached!
% 16.32/3.62 % (1658507)------------------------------
% 16.32/3.62 % (1658507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.32/3.62 % (1658507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/3.62 % (1658507)CaDiCaL version: 2.1.3
% 16.32/3.62 % (1658507)Termination reason: Instruction limit
% 16.32/3.62 % (1658507)Termination phase: Saturation
% 16.32/3.62 % (1658507)Time elapsed: 0.068 s
% 16.32/3.62 % (1658507)Peak memory usage: 93 MB
% 16.32/3.62 % (1658507)Instructions burned: 134 (million)
% 16.32/3.62 % (1658508)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3354159424:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/141Mi)
% 16.32/3.62 % (1658461)First to succeed.
% 16.32/3.62 % (1658508)Refutation not found, incomplete strategy
% 16.32/3.62 % (1658508)------------------------------
% 16.32/3.62 % (1658508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.32/3.62 % (1658508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.32/3.62 % (1658508)CaDiCaL version: 2.1.3
% 16.32/3.62 % (1658508)Termination reason: Refutation not found, incomplete strategy
% 16.32/3.62 % (1658508)Time elapsed: 0.017 s
% 16.32/3.62 % (1658508)Peak memory usage: 90 MB
% 16.32/3.62 % (1658508)Instructions burned: 34 (million)
% 16.32/3.62 % (1658461)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1658456"
% 16.32/3.62 % (1658510)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1902676256:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2975 on theBenchmark for (2975ds/431Mi)
% 16.32/3.62 % (1658508)------------------------------
% 16.32/3.62 % (1658508)------------------------------
% 16.32/3.62 % (1658461)Refutation found. Thanks to Tanya!
% 16.32/3.62 % SZS status Theorem for theBenchmark
% 16.32/3.62 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/3.80 % (1658461)------------------------------
% 0.17/3.80 % (1658461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/3.80 % (1658461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/3.80 % (1658461)CaDiCaL version: 2.1.3
% 0.17/3.80 % (1658461)Termination reason: Refutation
% 0.17/3.80 % (1658461)Time elapsed: 2.333 s
% 0.17/3.80 % (1658461)Peak memory usage: 184 MB
% 0.17/3.80 % (1658461)Instructions burned: 6550 (million)
% 0.17/3.80 % (1658461)------------------------------
% 0.17/3.80 % (1658461)------------------------------
% 0.17/3.80 % (1658456)Success in time 2.774 s
% 0.17/3.80 % Vampire exiting
%------------------------------------------------------------------------------