%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PRD002+1 : TPTP v9.3.1. Released v6.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n006.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:13 PM UTC 2026
% Result : CounterSatisfiable 0.39s 0.51s
% Output : FiniteModel 0.39s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
tff('declare_$i1',type,
'fmb_$i_1': $i ).
tff('declare_$i2',type,
'fmb_$i_2': $i ).
tff('finite_domain_$i',axiom,
! [X: $i] :
( ( X = 'fmb_$i_1' )
| ( X = 'fmb_$i_2' ) ) ).
tff('distinct_domain_$i',axiom,
'fmb_$i_1' != 'fmb_$i_2' ).
tff(declare_pulignymontrachetwhiteburgundy,type,
pulignymontrachetwhiteburgundy: $i ).
tff(pulignymontrachetwhiteburgundy_definition,axiom,
pulignymontrachetwhiteburgundy = 'fmb_$i_1' ).
tff(declare_medium,type,
medium: $i ).
tff(medium_definition,axiom,
medium = 'fmb_$i_1' ).
tff(declare_formanchardonnay,type,
formanchardonnay: $i ).
tff(formanchardonnay_definition,axiom,
formanchardonnay = 'fmb_$i_1' ).
tff(declare_full,type,
full: $i ).
tff(full_definition,axiom,
full = 'fmb_$i_1' ).
tff(declare_foxencheninblanc,type,
foxencheninblanc: $i ).
tff(foxencheninblanc_definition,axiom,
foxencheninblanc = 'fmb_$i_1' ).
tff(declare_chianticlassico,type,
chianticlassico: $i ).
tff(chianticlassico_definition,axiom,
chianticlassico = 'fmb_$i_1' ).
tff(declare_cortonmontrachetwhiteburgundy,type,
cortonmontrachetwhiteburgundy: $i ).
tff(cortonmontrachetwhiteburgundy_definition,axiom,
cortonmontrachetwhiteburgundy = 'fmb_$i_1' ).
tff(declare_corbansprivatebinsauvignonblanc,type,
corbansprivatebinsauvignonblanc: $i ).
tff(corbansprivatebinsauvignonblanc_definition,axiom,
corbansprivatebinsauvignonblanc = 'fmb_$i_1' ).
tff(declare_congressspringssemillon,type,
congressspringssemillon: $i ).
tff(congressspringssemillon_definition,axiom,
congressspringssemillon = 'fmb_$i_1' ).
tff(declare_mariettapetitesyrah,type,
mariettapetitesyrah: $i ).
tff(mariettapetitesyrah_definition,axiom,
mariettapetitesyrah = 'fmb_$i_1' ).
tff(declare_corbanssauvignonblanc,type,
corbanssauvignonblanc: $i ).
tff(corbanssauvignonblanc_definition,axiom,
corbanssauvignonblanc = 'fmb_$i_1' ).
tff(declare_petermccoychardonnay,type,
petermccoychardonnay: $i ).
tff(petermccoychardonnay_definition,axiom,
petermccoychardonnay = 'fmb_$i_1' ).
tff(declare_selaksicewine,type,
selaksicewine: $i ).
tff(selaksicewine_definition,axiom,
selaksicewine = 'fmb_$i_1' ).
tff(declare_bancroftchardonnay,type,
bancroftchardonnay: $i ).
tff(bancroftchardonnay_definition,axiom,
bancroftchardonnay = 'fmb_$i_1' ).
tff(declare_elysezinfandel,type,
elysezinfandel: $i ).
tff(elysezinfandel_definition,axiom,
elysezinfandel = 'fmb_$i_1' ).
tff(declare_mountadampinotnoir,type,
mountadampinotnoir: $i ).
tff(mountadampinotnoir_definition,axiom,
mountadampinotnoir = 'fmb_$i_1' ).
tff(declare_mariettacabernetsauvignon,type,
mariettacabernetsauvignon: $i ).
tff(mariettacabernetsauvignon_definition,axiom,
mariettacabernetsauvignon = 'fmb_$i_1' ).
tff(declare_schlossrothermeltrochenbierenausleseriesling,type,
schlossrothermeltrochenbierenausleseriesling: $i ).
tff(schlossrothermeltrochenbierenausleseriesling_definition,axiom,
schlossrothermeltrochenbierenausleseriesling = 'fmb_$i_1' ).
tff(declare_garyfarrellmerlot,type,
garyfarrellmerlot: $i ).
tff(garyfarrellmerlot_definition,axiom,
garyfarrellmerlot = 'fmb_$i_1' ).
tff(declare_cotturizinfandel,type,
cotturizinfandel: $i ).
tff(cotturizinfandel_definition,axiom,
cotturizinfandel = 'fmb_$i_1' ).
tff(declare_mariettaoldvinesred,type,
mariettaoldvinesred: $i ).
tff(mariettaoldvinesred_definition,axiom,
mariettaoldvinesred = 'fmb_$i_1' ).
tff(declare_longridgemerlot,type,
longridgemerlot: $i ).
tff(longridgemerlot_definition,axiom,
longridgemerlot = 'fmb_$i_1' ).
tff(declare_light,type,
light: $i ).
tff(light_definition,axiom,
light = 'fmb_$i_1' ).
tff(declare_kalincellarssemillon,type,
kalincellarssemillon: $i ).
tff(kalincellarssemillon_definition,axiom,
kalincellarssemillon = 'fmb_$i_1' ).
tff(declare_pagemillwinerycabernetsauvignon,type,
pagemillwinerycabernetsauvignon: $i ).
tff(pagemillwinerycabernetsauvignon_definition,axiom,
pagemillwinerycabernetsauvignon = 'fmb_$i_1' ).
tff(declare_seanthackreysiriuspetitesyrah,type,
seanthackreysiriuspetitesyrah: $i ).
tff(seanthackreysiriuspetitesyrah_definition,axiom,
seanthackreysiriuspetitesyrah = 'fmb_$i_1' ).
tff(declare_saucelitocanyonzinfandel1998,type,
saucelitocanyonzinfandel1998: $i ).
tff(saucelitocanyonzinfandel1998_definition,axiom,
saucelitocanyonzinfandel1998 = 'fmb_$i_1' ).
tff(declare_whitehalllaneprimavera,type,
whitehalllaneprimavera: $i ).
tff(whitehalllaneprimavera_definition,axiom,
whitehalllaneprimavera = 'fmb_$i_1' ).
tff(declare_santacruzmountainvineyardcabernetsauvignon,type,
santacruzmountainvineyardcabernetsauvignon: $i ).
tff(santacruzmountainvineyardcabernetsauvignon_definition,axiom,
santacruzmountainvineyardcabernetsauvignon = 'fmb_$i_1' ).
tff(declare_lanetannerpinotnoir,type,
lanetannerpinotnoir: $i ).
tff(lanetannerpinotnoir_definition,axiom,
lanetannerpinotnoir = 'fmb_$i_1' ).
tff(declare_corbansdrywhiteriesling,type,
corbansdrywhiteriesling: $i ).
tff(corbansdrywhiteriesling_definition,axiom,
corbansdrywhiteriesling = 'fmb_$i_1' ).
tff(declare_mountadamchardonnay,type,
mountadamchardonnay: $i ).
tff(mountadamchardonnay_definition,axiom,
mountadamchardonnay = 'fmb_$i_1' ).
tff(declare_mountadamriesling,type,
mountadamriesling: $i ).
tff(mountadamriesling_definition,axiom,
mountadamriesling = 'fmb_$i_1' ).
tff(declare_mariettazinfandel,type,
mariettazinfandel: $i ).
tff(mariettazinfandel_definition,axiom,
mariettazinfandel = 'fmb_$i_1' ).
tff(declare_kathrynkennedylateral,type,
kathrynkennedylateral: $i ).
tff(kathrynkennedylateral_definition,axiom,
kathrynkennedylateral = 'fmb_$i_1' ).
tff(declare_mountedenvineyardestatepinotnoir,type,
mountedenvineyardestatepinotnoir: $i ).
tff(mountedenvineyardestatepinotnoir_definition,axiom,
mountedenvineyardestatepinotnoir = 'fmb_$i_1' ).
tff(declare_whitehalllanecabernetfranc,type,
whitehalllanecabernetfranc: $i ).
tff(whitehalllanecabernetfranc_definition,axiom,
whitehalllanecabernetfranc = 'fmb_$i_1' ).
tff(declare_ventanacheninblanc,type,
ventanacheninblanc: $i ).
tff(ventanacheninblanc_definition,axiom,
ventanacheninblanc = 'fmb_$i_1' ).
tff(declare_saucelitocanyonzinfandel,type,
saucelitocanyonzinfandel: $i ).
tff(saucelitocanyonzinfandel_definition,axiom,
saucelitocanyonzinfandel = 'fmb_$i_1' ).
tff(declare_formancabernetsauvignon,type,
formancabernetsauvignon: $i ).
tff(formancabernetsauvignon_definition,axiom,
formancabernetsauvignon = 'fmb_$i_1' ).
tff(declare_schlossvolradtrochenbierenausleseriesling,type,
schlossvolradtrochenbierenausleseriesling: $i ).
tff(schlossvolradtrochenbierenausleseriesling_definition,axiom,
schlossvolradtrochenbierenausleseriesling = 'fmb_$i_1' ).
tff(declare_mountedenvineyardednavalleychardonnay,type,
mountedenvineyardednavalleychardonnay: $i ).
tff(mountedenvineyardednavalleychardonnay_definition,axiom,
mountedenvineyardednavalleychardonnay = 'fmb_$i_1' ).
tff(declare_stonleighsauvignonblanc,type,
stonleighsauvignonblanc: $i ).
tff(stonleighsauvignonblanc_definition,axiom,
stonleighsauvignonblanc = 'fmb_$i_1' ).
tff(declare_selakssauvignonblanc,type,
selakssauvignonblanc: $i ).
tff(selakssauvignonblanc_definition,axiom,
selakssauvignonblanc = 'fmb_$i_1' ).
tff(declare_white,type,
white: $i ).
tff(white_definition,axiom,
white = 'fmb_$i_1' ).
tff(declare_moderate,type,
moderate: $i ).
tff(moderate_definition,axiom,
moderate = 'fmb_$i_1' ).
tff(declare_stgenevievetexaswhite,type,
stgenevievetexaswhite: $i ).
tff(stgenevievetexaswhite_definition,axiom,
stgenevievetexaswhite = 'fmb_$i_1' ).
tff(declare_strong,type,
strong: $i ).
tff(strong_definition,axiom,
strong = 'fmb_$i_1' ).
tff(declare_chateaudychemsauterne,type,
chateaudychemsauterne: $i ).
tff(chateaudychemsauterne_definition,axiom,
chateaudychemsauterne = 'fmb_$i_1' ).
tff(declare_chateaudemeursaultmeursault,type,
chateaudemeursaultmeursault: $i ).
tff(chateaudemeursaultmeursault_definition,axiom,
chateaudemeursaultmeursault = 'fmb_$i_1' ).
tff(declare_delicate,type,
delicate: $i ).
tff(delicate_definition,axiom,
delicate = 'fmb_$i_1' ).
tff(declare_pulignymontrachet,type,
pulignymontrachet: $i ).
tff(pulignymontrachet_definition,axiom,
pulignymontrachet = 'fmb_$i_1' ).
tff(declare_chateaulafiterothschildpauillac,type,
chateaulafiterothschildpauillac: $i ).
tff(chateaulafiterothschildpauillac_definition,axiom,
chateaulafiterothschildpauillac = 'fmb_$i_1' ).
tff(declare_chateaulafiterothschild,type,
chateaulafiterothschild: $i ).
tff(chateaulafiterothschild_definition,axiom,
chateaulafiterothschild = 'fmb_$i_1' ).
tff(declare_forman,type,
forman: $i ).
tff(forman_definition,axiom,
forman = 'fmb_$i_1' ).
tff(declare_stgenevieve,type,
stgenevieve: $i ).
tff(stgenevieve_definition,axiom,
stgenevieve = 'fmb_$i_1' ).
tff(declare_foxen,type,
foxen: $i ).
tff(foxen_definition,axiom,
foxen = 'fmb_$i_1' ).
tff(declare_mcguinnesso,type,
mcguinnesso: $i ).
tff(mcguinnesso_definition,axiom,
mcguinnesso = 'fmb_$i_1' ).
tff(declare_cortonmontrachet,type,
cortonmontrachet: $i ).
tff(cortonmontrachet_definition,axiom,
cortonmontrachet = 'fmb_$i_1' ).
tff(declare_corbans,type,
corbans: $i ).
tff(corbans_definition,axiom,
corbans = 'fmb_$i_1' ).
tff(declare_congresssprings,type,
congresssprings: $i ).
tff(congresssprings_definition,axiom,
congresssprings = 'fmb_$i_1' ).
tff(declare_marietta,type,
marietta: $i ).
tff(marietta_definition,axiom,
marietta = 'fmb_$i_1' ).
tff(declare_petermccoy,type,
petermccoy: $i ).
tff(petermccoy_definition,axiom,
petermccoy = 'fmb_$i_1' ).
tff(declare_selaks,type,
selaks: $i ).
tff(selaks_definition,axiom,
selaks = 'fmb_$i_1' ).
tff(declare_bancroft,type,
bancroft: $i ).
tff(bancroft_definition,axiom,
bancroft = 'fmb_$i_1' ).
tff(declare_chateauchevalblancstemilion,type,
chateauchevalblancstemilion: $i ).
tff(chateauchevalblancstemilion_definition,axiom,
chateauchevalblancstemilion = 'fmb_$i_1' ).
tff(declare_chateauchevalblanc,type,
chateauchevalblanc: $i ).
tff(chateauchevalblanc_definition,axiom,
chateauchevalblanc = 'fmb_$i_1' ).
tff(declare_chateaumorgonbeaujolais,type,
chateaumorgonbeaujolais: $i ).
tff(chateaumorgonbeaujolais_definition,axiom,
chateaumorgonbeaujolais = 'fmb_$i_1' ).
tff(declare_chateaumorgon,type,
chateaumorgon: $i ).
tff(chateaumorgon_definition,axiom,
chateaumorgon = 'fmb_$i_1' ).
tff(declare_elyse,type,
elyse: $i ).
tff(elyse_definition,axiom,
elyse = 'fmb_$i_1' ).
tff(declare_mountadam,type,
mountadam: $i ).
tff(mountadam_definition,axiom,
mountadam = 'fmb_$i_1' ).
tff(declare_taylorport,type,
taylorport: $i ).
tff(taylorport_definition,axiom,
taylorport = 'fmb_$i_1' ).
tff(declare_taylor,type,
taylor: $i ).
tff(taylor_definition,axiom,
taylor = 'fmb_$i_1' ).
tff(declare_chateaudychem,type,
chateaudychem: $i ).
tff(chateaudychem_definition,axiom,
chateaudychem = 'fmb_$i_1' ).
tff(declare_schlossrothermel,type,
schlossrothermel: $i ).
tff(schlossrothermel_definition,axiom,
schlossrothermel = 'fmb_$i_1' ).
tff(declare_garyfarrell,type,
garyfarrell: $i ).
tff(garyfarrell_definition,axiom,
garyfarrell = 'fmb_$i_1' ).
tff(declare_closdevougeotcotesdor,type,
closdevougeotcotesdor: $i ).
tff(closdevougeotcotesdor_definition,axiom,
closdevougeotcotesdor = 'fmb_$i_1' ).
tff(declare_closdevougeot,type,
closdevougeot: $i ).
tff(closdevougeot_definition,axiom,
closdevougeot = 'fmb_$i_1' ).
tff(declare_cotturi,type,
cotturi: $i ).
tff(cotturi_definition,axiom,
cotturi = 'fmb_$i_1' ).
tff(declare_closdelapoussiesancerre,type,
closdelapoussiesancerre: $i ).
tff(closdelapoussiesancerre_definition,axiom,
closdelapoussiesancerre = 'fmb_$i_1' ).
tff(declare_closdelapoussie,type,
closdelapoussie: $i ).
tff(closdelapoussie_definition,axiom,
closdelapoussie = 'fmb_$i_1' ).
tff(declare_longridge,type,
longridge: $i ).
tff(longridge_definition,axiom,
longridge = 'fmb_$i_1' ).
tff(declare_kalincellars,type,
kalincellars: $i ).
tff(kalincellars_definition,axiom,
kalincellars = 'fmb_$i_1' ).
tff(declare_pagemillwinery,type,
pagemillwinery: $i ).
tff(pagemillwinery_definition,axiom,
pagemillwinery = 'fmb_$i_1' ).
tff(declare_seanthackrey,type,
seanthackrey: $i ).
tff(seanthackrey_definition,axiom,
seanthackrey = 'fmb_$i_1' ).
tff(declare_saucelitocanyon,type,
saucelitocanyon: $i ).
tff(saucelitocanyon_definition,axiom,
saucelitocanyon = 'fmb_$i_1' ).
tff(declare_chateaudemeursault,type,
chateaudemeursault: $i ).
tff(chateaudemeursault_definition,axiom,
chateaudemeursault = 'fmb_$i_1' ).
tff(declare_santacruzmountainvineyard,type,
santacruzmountainvineyard: $i ).
tff(santacruzmountainvineyard_definition,axiom,
santacruzmountainvineyard = 'fmb_$i_1' ).
tff(declare_lanetanner,type,
lanetanner: $i ).
tff(lanetanner_definition,axiom,
lanetanner = 'fmb_$i_1' ).
tff(declare_rosedanjou,type,
rosedanjou: $i ).
tff(rosedanjou_definition,axiom,
rosedanjou = 'fmb_$i_1' ).
tff(declare_danjou,type,
danjou: $i ).
tff(danjou_definition,axiom,
danjou = 'fmb_$i_1' ).
tff(declare_chateaumargaux,type,
chateaumargaux: $i ).
tff(chateaumargaux_definition,axiom,
chateaumargaux = 'fmb_$i_1' ).
tff(declare_chateaumargauxwinery,type,
chateaumargauxwinery: $i ).
tff(chateaumargauxwinery_definition,axiom,
chateaumargauxwinery = 'fmb_$i_1' ).
tff(declare_kathrynkennedy,type,
kathrynkennedy: $i ).
tff(kathrynkennedy_definition,axiom,
kathrynkennedy = 'fmb_$i_1' ).
tff(declare_mountedenvineyard,type,
mountedenvineyard: $i ).
tff(mountedenvineyard_definition,axiom,
mountedenvineyard = 'fmb_$i_1' ).
tff(declare_whitehalllane,type,
whitehalllane: $i ).
tff(whitehalllane_definition,axiom,
whitehalllane = 'fmb_$i_1' ).
tff(declare_ventana,type,
ventana: $i ).
tff(ventana_definition,axiom,
ventana = 'fmb_$i_1' ).
tff(declare_schlossvolrad,type,
schlossvolrad: $i ).
tff(schlossvolrad_definition,axiom,
schlossvolrad = 'fmb_$i_1' ).
tff(declare_stonleigh,type,
stonleigh: $i ).
tff(stonleigh_definition,axiom,
stonleigh = 'fmb_$i_1' ).
tff(declare_sevreetmainemuscadet,type,
sevreetmainemuscadet: $i ).
tff(sevreetmainemuscadet_definition,axiom,
sevreetmainemuscadet = 'fmb_$i_1' ).
tff(declare_sevreetmaine,type,
sevreetmaine: $i ).
tff(sevreetmaine_definition,axiom,
sevreetmaine = 'fmb_$i_1' ).
tff(declare_dry,type,
dry: $i ).
tff(dry_definition,axiom,
dry = 'fmb_$i_1' ).
tff(declare_sweet,type,
sweet: $i ).
tff(sweet_definition,axiom,
sweet = 'fmb_$i_1' ).
tff(declare_offdry,type,
offdry: $i ).
tff(offdry_definition,axiom,
offdry = 'fmb_$i_1' ).
tff(declare_californiaregion,type,
californiaregion: $i ).
tff(californiaregion_definition,axiom,
californiaregion = 'fmb_$i_1' ).
tff(declare_usregion,type,
usregion: $i ).
tff(usregion_definition,axiom,
usregion = 'fmb_$i_1' ).
tff(declare_sancerreregion,type,
sancerreregion: $i ).
tff(sancerreregion_definition,axiom,
sancerreregion = 'fmb_$i_2' ).
tff(declare_loireregion,type,
loireregion: $i ).
tff(loireregion_definition,axiom,
loireregion = 'fmb_$i_2' ).
tff(declare_naparegion,type,
naparegion: $i ).
tff(naparegion_definition,axiom,
naparegion = 'fmb_$i_1' ).
tff(declare_centraltexasregion,type,
centraltexasregion: $i ).
tff(centraltexasregion_definition,axiom,
centraltexasregion = 'fmb_$i_1' ).
tff(declare_santabarbararegion,type,
santabarbararegion: $i ).
tff(santabarbararegion_definition,axiom,
santabarbararegion = 'fmb_$i_1' ).
tff(declare_frenchregion,type,
frenchregion: $i ).
tff(frenchregion_definition,axiom,
frenchregion = 'fmb_$i_2' ).
tff(declare_newzealandregion,type,
newzealandregion: $i ).
tff(newzealandregion_definition,axiom,
newzealandregion = 'fmb_$i_1' ).
tff(declare_sonomaregion,type,
sonomaregion: $i ).
tff(sonomaregion_definition,axiom,
sonomaregion = 'fmb_$i_1' ).
tff(declare_southaustraliaregion,type,
southaustraliaregion: $i ).
tff(southaustraliaregion_definition,axiom,
southaustraliaregion = 'fmb_$i_1' ).
tff(declare_chiantiregion,type,
chiantiregion: $i ).
tff(chiantiregion_definition,axiom,
chiantiregion = 'fmb_$i_2' ).
tff(declare_italianregion,type,
italianregion: $i ).
tff(italianregion_definition,axiom,
italianregion = 'fmb_$i_2' ).
tff(declare_sauterneregion,type,
sauterneregion: $i ).
tff(sauterneregion_definition,axiom,
sauterneregion = 'fmb_$i_2' ).
tff(declare_bordeauxregion,type,
bordeauxregion: $i ).
tff(bordeauxregion_definition,axiom,
bordeauxregion = 'fmb_$i_2' ).
tff(declare_pauillacregion,type,
pauillacregion: $i ).
tff(pauillacregion_definition,axiom,
pauillacregion = 'fmb_$i_2' ).
tff(declare_medocregion,type,
medocregion: $i ).
tff(medocregion_definition,axiom,
medocregion = 'fmb_$i_2' ).
tff(declare_texasregion,type,
texasregion: $i ).
tff(texasregion_definition,axiom,
texasregion = 'fmb_$i_1' ).
tff(declare_germanyregion,type,
germanyregion: $i ).
tff(germanyregion_definition,axiom,
germanyregion = 'fmb_$i_1' ).
tff(declare_anjouregion,type,
anjouregion: $i ).
tff(anjouregion_definition,axiom,
anjouregion = 'fmb_$i_2' ).
tff(declare_centralcoastregion,type,
centralcoastregion: $i ).
tff(centralcoastregion_definition,axiom,
centralcoastregion = 'fmb_$i_1' ).
tff(declare_arroyogranderegion,type,
arroyogranderegion: $i ).
tff(arroyogranderegion_definition,axiom,
arroyogranderegion = 'fmb_$i_1' ).
tff(declare_australianregion,type,
australianregion: $i ).
tff(australianregion_definition,axiom,
australianregion = 'fmb_$i_1' ).
tff(declare_santacruzmountainsregion,type,
santacruzmountainsregion: $i ).
tff(santacruzmountainsregion_definition,axiom,
santacruzmountainsregion = 'fmb_$i_1' ).
tff(declare_mendocinoregion,type,
mendocinoregion: $i ).
tff(mendocinoregion_definition,axiom,
mendocinoregion = 'fmb_$i_2' ).
tff(declare_margauxregion,type,
margauxregion: $i ).
tff(margauxregion_definition,axiom,
margauxregion = 'fmb_$i_2' ).
tff(declare_muscadetregion,type,
muscadetregion: $i ).
tff(muscadetregion_definition,axiom,
muscadetregion = 'fmb_$i_2' ).
tff(declare_alsaceregion,type,
alsaceregion: $i ).
tff(alsaceregion_definition,axiom,
alsaceregion = 'fmb_$i_2' ).
tff(declare_stemilionregion,type,
stemilionregion: $i ).
tff(stemilionregion_definition,axiom,
stemilionregion = 'fmb_$i_2' ).
tff(declare_bourgogneregion,type,
bourgogneregion: $i ).
tff(bourgogneregion_definition,axiom,
bourgogneregion = 'fmb_$i_2' ).
tff(declare_toursregion,type,
toursregion: $i ).
tff(toursregion_definition,axiom,
toursregion = 'fmb_$i_2' ).
tff(declare_cotesdorregion,type,
cotesdorregion: $i ).
tff(cotesdorregion_definition,axiom,
cotesdorregion = 'fmb_$i_2' ).
tff(declare_ednavalleyregion,type,
ednavalleyregion: $i ).
tff(ednavalleyregion_definition,axiom,
ednavalleyregion = 'fmb_$i_1' ).
tff(declare_beaujolaisregion,type,
beaujolaisregion: $i ).
tff(beaujolaisregion_definition,axiom,
beaujolaisregion = 'fmb_$i_2' ).
tff(declare_meursaultregion,type,
meursaultregion: $i ).
tff(meursaultregion_definition,axiom,
meursaultregion = 'fmb_$i_2' ).
tff(declare_semillongrape,type,
semillongrape: $i ).
tff(semillongrape_definition,axiom,
semillongrape = 'fmb_$i_1' ).
tff(declare_sauvignonblancgrape,type,
sauvignonblancgrape: $i ).
tff(sauvignonblancgrape_definition,axiom,
sauvignonblancgrape = 'fmb_$i_1' ).
tff(declare_zinfandelgrape,type,
zinfandelgrape: $i ).
tff(zinfandelgrape_definition,axiom,
zinfandelgrape = 'fmb_$i_2' ).
tff(declare_pinotblancgrape,type,
pinotblancgrape: $i ).
tff(pinotblancgrape_definition,axiom,
pinotblancgrape = 'fmb_$i_2' ).
tff(declare_chardonnaygrape,type,
chardonnaygrape: $i ).
tff(chardonnaygrape_definition,axiom,
chardonnaygrape = 'fmb_$i_2' ).
tff(declare_petitesyrahgrape,type,
petitesyrahgrape: $i ).
tff(petitesyrahgrape_definition,axiom,
petitesyrahgrape = 'fmb_$i_2' ).
tff(declare_red,type,
red: $i ).
tff(red_definition,axiom,
red = 'fmb_$i_2' ).
tff(declare_cabernetsauvignongrape,type,
cabernetsauvignongrape: $i ).
tff(cabernetsauvignongrape_definition,axiom,
cabernetsauvignongrape = 'fmb_$i_2' ).
tff(declare_cabernetfrancgrape,type,
cabernetfrancgrape: $i ).
tff(cabernetfrancgrape_definition,axiom,
cabernetfrancgrape = 'fmb_$i_2' ).
tff(declare_rose,type,
rose: $i ).
tff(rose_definition,axiom,
rose = 'fmb_$i_2' ).
tff(declare_gamaygrape,type,
gamaygrape: $i ).
tff(gamaygrape_definition,axiom,
gamaygrape = 'fmb_$i_2' ).
tff(declare_cheninblancgrape,type,
cheninblancgrape: $i ).
tff(cheninblancgrape_definition,axiom,
cheninblancgrape = 'fmb_$i_2' ).
tff(declare_rieslinggrape,type,
rieslinggrape: $i ).
tff(rieslinggrape_definition,axiom,
rieslinggrape = 'fmb_$i_2' ).
tff(declare_pinotnoirgrape,type,
pinotnoirgrape: $i ).
tff(pinotnoirgrape_definition,axiom,
pinotnoirgrape = 'fmb_$i_2' ).
tff(declare_merlotgrape,type,
merlotgrape: $i ).
tff(merlotgrape_definition,axiom,
merlotgrape = 'fmb_$i_2' ).
tff(declare_portugalregion,type,
portugalregion: $i ).
tff(portugalregion_definition,axiom,
portugalregion = 'fmb_$i_2' ).
tff(declare_sangiovesegrape,type,
sangiovesegrape: $i ).
tff(sangiovesegrape_definition,axiom,
sangiovesegrape = 'fmb_$i_2' ).
tff(declare_petiteverdotgrape,type,
petiteverdotgrape: $i ).
tff(petiteverdotgrape_definition,axiom,
petiteverdotgrape = 'fmb_$i_2' ).
tff(declare_malbecgrape,type,
malbecgrape: $i ).
tff(malbecgrape_definition,axiom,
malbecgrape = 'fmb_$i_2' ).
tff(declare_beringer,type,
beringer: $i ).
tff(beringer_definition,axiom,
beringer = 'fmb_$i_2' ).
tff(declare_handley,type,
handley: $i ).
tff(handley_definition,axiom,
handley = 'fmb_$i_2' ).
tff(declare_year1998,type,
year1998: $i ).
tff(year1998_definition,axiom,
year1998 = 'fmb_$i_1' ).
tff(declare_hasbody_aux,type,
hasbody_aux: ( $i * $i ) > $o ).
tff(predicate_hasbody_aux,axiom,
( hasbody_aux('fmb_$i_1','fmb_$i_1')
& ~ hasbody_aux('fmb_$i_1','fmb_$i_2')
& ~ hasbody_aux('fmb_$i_2','fmb_$i_1')
& ~ hasbody_aux('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_hascolor_aux,type,
hascolor_aux: ( $i * $i ) > $o ).
tff(predicate_hascolor_aux,axiom,
( hascolor_aux('fmb_$i_1','fmb_$i_1')
& ~ hascolor_aux('fmb_$i_1','fmb_$i_2')
& ~ hascolor_aux('fmb_$i_2','fmb_$i_1')
& ~ hascolor_aux('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_hasflavor_aux,type,
hasflavor_aux: ( $i * $i ) > $o ).
tff(predicate_hasflavor_aux,axiom,
( hasflavor_aux('fmb_$i_1','fmb_$i_1')
& ~ hasflavor_aux('fmb_$i_1','fmb_$i_2')
& ~ hasflavor_aux('fmb_$i_2','fmb_$i_1')
& ~ hasflavor_aux('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_hasmaker_aux,type,
hasmaker_aux: ( $i * $i ) > $o ).
tff(predicate_hasmaker_aux,axiom,
( hasmaker_aux('fmb_$i_1','fmb_$i_1')
& ~ hasmaker_aux('fmb_$i_1','fmb_$i_2')
& hasmaker_aux('fmb_$i_2','fmb_$i_1')
& ~ hasmaker_aux('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_hassugar_aux,type,
hassugar_aux: ( $i * $i ) > $o ).
tff(predicate_hassugar_aux,axiom,
( hassugar_aux('fmb_$i_1','fmb_$i_1')
& ~ hassugar_aux('fmb_$i_1','fmb_$i_2')
& ~ hassugar_aux('fmb_$i_2','fmb_$i_1')
& ~ hassugar_aux('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_locatedin_aux,type,
locatedin_aux: ( $i * $i ) > $o ).
tff(predicate_locatedin_aux,axiom,
( locatedin_aux('fmb_$i_1','fmb_$i_1')
& ~ locatedin_aux('fmb_$i_1','fmb_$i_2')
& locatedin_aux('fmb_$i_2','fmb_$i_1')
& locatedin_aux('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_madefromgrape_aux,type,
madefromgrape_aux: ( $i * $i ) > $o ).
tff(predicate_madefromgrape_aux,axiom,
( madefromgrape_aux('fmb_$i_1','fmb_$i_1')
& ~ madefromgrape_aux('fmb_$i_1','fmb_$i_2')
& ~ madefromgrape_aux('fmb_$i_2','fmb_$i_1')
& ~ madefromgrape_aux('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_ot____nom1_aux,type,
ot____nom1_aux: $i > $o ).
tff(predicate_ot____nom1_aux,axiom,
( ot____nom1_aux('fmb_$i_1')
& ot____nom1_aux('fmb_$i_2') ) ).
tff(declare_ot____nom10_aux,type,
ot____nom10_aux: $i > $o ).
tff(predicate_ot____nom10_aux,axiom,
( ot____nom10_aux('fmb_$i_1')
& ~ ot____nom10_aux('fmb_$i_2') ) ).
tff(declare_ot____nom11_aux,type,
ot____nom11_aux: $i > $o ).
tff(predicate_ot____nom11_aux,axiom,
( ot____nom11_aux('fmb_$i_1')
& ~ ot____nom11_aux('fmb_$i_2') ) ).
tff(declare_ot____nom12_aux,type,
ot____nom12_aux: $i > $o ).
tff(predicate_ot____nom12_aux,axiom,
( ot____nom12_aux('fmb_$i_1')
& ot____nom12_aux('fmb_$i_2') ) ).
tff(declare_ot____nom13_aux,type,
ot____nom13_aux: $i > $o ).
tff(predicate_ot____nom13_aux,axiom,
( ~ ot____nom13_aux('fmb_$i_1')
& ot____nom13_aux('fmb_$i_2') ) ).
tff(declare_ot____nom14_aux,type,
ot____nom14_aux: $i > $o ).
tff(predicate_ot____nom14_aux,axiom,
( ot____nom14_aux('fmb_$i_1')
& ot____nom14_aux('fmb_$i_2') ) ).
tff(declare_ot____nom15_aux,type,
ot____nom15_aux: $i > $o ).
tff(predicate_ot____nom15_aux,axiom,
( ot____nom15_aux('fmb_$i_1')
& ot____nom15_aux('fmb_$i_2') ) ).
tff(declare_ot____nom16_aux,type,
ot____nom16_aux: $i > $o ).
tff(predicate_ot____nom16_aux,axiom,
( ~ ot____nom16_aux('fmb_$i_1')
& ot____nom16_aux('fmb_$i_2') ) ).
tff(declare_ot____nom17_aux,type,
ot____nom17_aux: $i > $o ).
tff(predicate_ot____nom17_aux,axiom,
( ot____nom17_aux('fmb_$i_1')
& ot____nom17_aux('fmb_$i_2') ) ).
tff(declare_ot____nom18_aux,type,
ot____nom18_aux: $i > $o ).
tff(predicate_ot____nom18_aux,axiom,
( ot____nom18_aux('fmb_$i_1')
& ot____nom18_aux('fmb_$i_2') ) ).
tff(declare_ot____nom19_aux,type,
ot____nom19_aux: $i > $o ).
tff(predicate_ot____nom19_aux,axiom,
( ~ ot____nom19_aux('fmb_$i_1')
& ot____nom19_aux('fmb_$i_2') ) ).
tff(declare_ot____nom2_aux,type,
ot____nom2_aux: $i > $o ).
tff(predicate_ot____nom2_aux,axiom,
( ot____nom2_aux('fmb_$i_1')
& ot____nom2_aux('fmb_$i_2') ) ).
tff(declare_ot____nom20_aux,type,
ot____nom20_aux: $i > $o ).
tff(predicate_ot____nom20_aux,axiom,
( ~ ot____nom20_aux('fmb_$i_1')
& ot____nom20_aux('fmb_$i_2') ) ).
tff(declare_ot____nom21_aux,type,
ot____nom21_aux: $i > $o ).
tff(predicate_ot____nom21_aux,axiom,
( ot____nom21_aux('fmb_$i_1')
& ot____nom21_aux('fmb_$i_2') ) ).
tff(declare_ot____nom22_aux,type,
ot____nom22_aux: $i > $o ).
tff(predicate_ot____nom22_aux,axiom,
( ot____nom22_aux('fmb_$i_1')
& ot____nom22_aux('fmb_$i_2') ) ).
tff(declare_ot____nom23_aux,type,
ot____nom23_aux: $i > $o ).
tff(predicate_ot____nom23_aux,axiom,
( ~ ot____nom23_aux('fmb_$i_1')
& ot____nom23_aux('fmb_$i_2') ) ).
tff(declare_ot____nom24_aux,type,
ot____nom24_aux: $i > $o ).
tff(predicate_ot____nom24_aux,axiom,
( ~ ot____nom24_aux('fmb_$i_1')
& ot____nom24_aux('fmb_$i_2') ) ).
tff(declare_ot____nom25_aux,type,
ot____nom25_aux: $i > $o ).
tff(predicate_ot____nom25_aux,axiom,
( ~ ot____nom25_aux('fmb_$i_1')
& ot____nom25_aux('fmb_$i_2') ) ).
tff(declare_ot____nom26_aux,type,
ot____nom26_aux: $i > $o ).
tff(predicate_ot____nom26_aux,axiom,
( ~ ot____nom26_aux('fmb_$i_1')
& ot____nom26_aux('fmb_$i_2') ) ).
tff(declare_ot____nom27_aux,type,
ot____nom27_aux: $i > $o ).
tff(predicate_ot____nom27_aux,axiom,
( ot____nom27_aux('fmb_$i_1')
& ot____nom27_aux('fmb_$i_2') ) ).
tff(declare_ot____nom28_aux,type,
ot____nom28_aux: $i > $o ).
tff(predicate_ot____nom28_aux,axiom,
( ~ ot____nom28_aux('fmb_$i_1')
& ot____nom28_aux('fmb_$i_2') ) ).
tff(declare_ot____nom29_aux,type,
ot____nom29_aux: $i > $o ).
tff(predicate_ot____nom29_aux,axiom,
( ot____nom29_aux('fmb_$i_1')
& ot____nom29_aux('fmb_$i_2') ) ).
tff(declare_ot____nom3_aux,type,
ot____nom3_aux: $i > $o ).
tff(predicate_ot____nom3_aux,axiom,
( ot____nom3_aux('fmb_$i_1')
& ot____nom3_aux('fmb_$i_2') ) ).
tff(declare_ot____nom30_aux,type,
ot____nom30_aux: $i > $o ).
tff(predicate_ot____nom30_aux,axiom,
( ~ ot____nom30_aux('fmb_$i_1')
& ot____nom30_aux('fmb_$i_2') ) ).
tff(declare_ot____nom31_aux,type,
ot____nom31_aux: $i > $o ).
tff(predicate_ot____nom31_aux,axiom,
( ot____nom31_aux('fmb_$i_1')
& ot____nom31_aux('fmb_$i_2') ) ).
tff(declare_ot____nom32_aux,type,
ot____nom32_aux: $i > $o ).
tff(predicate_ot____nom32_aux,axiom,
( ot____nom32_aux('fmb_$i_1')
& ot____nom32_aux('fmb_$i_2') ) ).
tff(declare_ot____nom33_aux,type,
ot____nom33_aux: $i > $o ).
tff(predicate_ot____nom33_aux,axiom,
( ot____nom33_aux('fmb_$i_1')
& ot____nom33_aux('fmb_$i_2') ) ).
tff(declare_ot____nom34_aux,type,
ot____nom34_aux: $i > $o ).
tff(predicate_ot____nom34_aux,axiom,
( ~ ot____nom34_aux('fmb_$i_1')
& ot____nom34_aux('fmb_$i_2') ) ).
tff(declare_ot____nom35_aux,type,
ot____nom35_aux: $i > $o ).
tff(predicate_ot____nom35_aux,axiom,
( ot____nom35_aux('fmb_$i_1')
& ot____nom35_aux('fmb_$i_2') ) ).
tff(declare_ot____nom36_aux,type,
ot____nom36_aux: $i > $o ).
tff(predicate_ot____nom36_aux,axiom,
( ~ ot____nom36_aux('fmb_$i_1')
& ot____nom36_aux('fmb_$i_2') ) ).
tff(declare_ot____nom37_aux,type,
ot____nom37_aux: $i > $o ).
tff(predicate_ot____nom37_aux,axiom,
( ot____nom37_aux('fmb_$i_1')
& ot____nom37_aux('fmb_$i_2') ) ).
tff(declare_ot____nom38_aux,type,
ot____nom38_aux: $i > $o ).
tff(predicate_ot____nom38_aux,axiom,
( ot____nom38_aux('fmb_$i_1')
& ~ ot____nom38_aux('fmb_$i_2') ) ).
tff(declare_ot____nom39_aux,type,
ot____nom39_aux: $i > $o ).
tff(predicate_ot____nom39_aux,axiom,
( ot____nom39_aux('fmb_$i_1')
& ot____nom39_aux('fmb_$i_2') ) ).
tff(declare_ot____nom4_aux,type,
ot____nom4_aux: $i > $o ).
tff(predicate_ot____nom4_aux,axiom,
( ~ ot____nom4_aux('fmb_$i_1')
& ot____nom4_aux('fmb_$i_2') ) ).
tff(declare_ot____nom40_aux,type,
ot____nom40_aux: $i > $o ).
tff(predicate_ot____nom40_aux,axiom,
( ot____nom40_aux('fmb_$i_1')
& ot____nom40_aux('fmb_$i_2') ) ).
tff(declare_ot____nom41_aux,type,
ot____nom41_aux: $i > $o ).
tff(predicate_ot____nom41_aux,axiom,
( ~ ot____nom41_aux('fmb_$i_1')
& ot____nom41_aux('fmb_$i_2') ) ).
tff(declare_ot____nom42_aux,type,
ot____nom42_aux: $i > $o ).
tff(predicate_ot____nom42_aux,axiom,
( ~ ot____nom42_aux('fmb_$i_1')
& ot____nom42_aux('fmb_$i_2') ) ).
tff(declare_ot____nom43_aux,type,
ot____nom43_aux: $i > $o ).
tff(predicate_ot____nom43_aux,axiom,
( ot____nom43_aux('fmb_$i_1')
& ot____nom43_aux('fmb_$i_2') ) ).
tff(declare_ot____nom44_aux,type,
ot____nom44_aux: $i > $o ).
tff(predicate_ot____nom44_aux,axiom,
( ~ ot____nom44_aux('fmb_$i_1')
& ot____nom44_aux('fmb_$i_2') ) ).
tff(declare_ot____nom45_aux,type,
ot____nom45_aux: $i > $o ).
tff(predicate_ot____nom45_aux,axiom,
( ot____nom45_aux('fmb_$i_1')
& ~ ot____nom45_aux('fmb_$i_2') ) ).
tff(declare_ot____nom46_aux,type,
ot____nom46_aux: $i > $o ).
tff(predicate_ot____nom46_aux,axiom,
( ot____nom46_aux('fmb_$i_1')
& ot____nom46_aux('fmb_$i_2') ) ).
tff(declare_ot____nom47_aux,type,
ot____nom47_aux: $i > $o ).
tff(predicate_ot____nom47_aux,axiom,
( ot____nom47_aux('fmb_$i_1')
& ot____nom47_aux('fmb_$i_2') ) ).
tff(declare_ot____nom48_aux,type,
ot____nom48_aux: $i > $o ).
tff(predicate_ot____nom48_aux,axiom,
( ot____nom48_aux('fmb_$i_1')
& ot____nom48_aux('fmb_$i_2') ) ).
tff(declare_ot____nom49_aux,type,
ot____nom49_aux: $i > $o ).
tff(predicate_ot____nom49_aux,axiom,
( ot____nom49_aux('fmb_$i_1')
& ~ ot____nom49_aux('fmb_$i_2') ) ).
tff(declare_ot____nom5_aux,type,
ot____nom5_aux: $i > $o ).
tff(predicate_ot____nom5_aux,axiom,
( ot____nom5_aux('fmb_$i_1')
& ~ ot____nom5_aux('fmb_$i_2') ) ).
tff(declare_ot____nom50_aux,type,
ot____nom50_aux: $i > $o ).
tff(predicate_ot____nom50_aux,axiom,
( ot____nom50_aux('fmb_$i_1')
& ~ ot____nom50_aux('fmb_$i_2') ) ).
tff(declare_ot____nom51_aux,type,
ot____nom51_aux: $i > $o ).
tff(predicate_ot____nom51_aux,axiom,
( ot____nom51_aux('fmb_$i_1')
& ot____nom51_aux('fmb_$i_2') ) ).
tff(declare_ot____nom52_aux,type,
ot____nom52_aux: $i > $o ).
tff(predicate_ot____nom52_aux,axiom,
( ot____nom52_aux('fmb_$i_1')
& ot____nom52_aux('fmb_$i_2') ) ).
tff(declare_ot____nom53_aux,type,
ot____nom53_aux: $i > $o ).
tff(predicate_ot____nom53_aux,axiom,
( ot____nom53_aux('fmb_$i_1')
& ~ ot____nom53_aux('fmb_$i_2') ) ).
tff(declare_ot____nom54_aux,type,
ot____nom54_aux: $i > $o ).
tff(predicate_ot____nom54_aux,axiom,
( ot____nom54_aux('fmb_$i_1')
& ot____nom54_aux('fmb_$i_2') ) ).
tff(declare_ot____nom55_aux,type,
ot____nom55_aux: $i > $o ).
tff(predicate_ot____nom55_aux,axiom,
( ot____nom55_aux('fmb_$i_1')
& ot____nom55_aux('fmb_$i_2') ) ).
tff(declare_ot____nom56_aux,type,
ot____nom56_aux: $i > $o ).
tff(predicate_ot____nom56_aux,axiom,
( ot____nom56_aux('fmb_$i_1')
& ~ ot____nom56_aux('fmb_$i_2') ) ).
tff(declare_ot____nom57_aux,type,
ot____nom57_aux: $i > $o ).
tff(predicate_ot____nom57_aux,axiom,
( ot____nom57_aux('fmb_$i_1')
& ot____nom57_aux('fmb_$i_2') ) ).
tff(declare_ot____nom58_aux,type,
ot____nom58_aux: $i > $o ).
tff(predicate_ot____nom58_aux,axiom,
( ot____nom58_aux('fmb_$i_1')
& ~ ot____nom58_aux('fmb_$i_2') ) ).
tff(declare_ot____nom59_aux,type,
ot____nom59_aux: $i > $o ).
tff(predicate_ot____nom59_aux,axiom,
( ot____nom59_aux('fmb_$i_1')
& ot____nom59_aux('fmb_$i_2') ) ).
tff(declare_ot____nom6_aux,type,
ot____nom6_aux: $i > $o ).
tff(predicate_ot____nom6_aux,axiom,
( ot____nom6_aux('fmb_$i_1')
& ot____nom6_aux('fmb_$i_2') ) ).
tff(declare_ot____nom60_aux,type,
ot____nom60_aux: $i > $o ).
tff(predicate_ot____nom60_aux,axiom,
( ot____nom60_aux('fmb_$i_1')
& ot____nom60_aux('fmb_$i_2') ) ).
tff(declare_ot____nom61_aux,type,
ot____nom61_aux: $i > $o ).
tff(predicate_ot____nom61_aux,axiom,
( ot____nom61_aux('fmb_$i_1')
& ot____nom61_aux('fmb_$i_2') ) ).
tff(declare_ot____nom62_aux,type,
ot____nom62_aux: $i > $o ).
tff(predicate_ot____nom62_aux,axiom,
( ot____nom62_aux('fmb_$i_1')
& ot____nom62_aux('fmb_$i_2') ) ).
tff(declare_ot____nom63_aux,type,
ot____nom63_aux: $i > $o ).
tff(predicate_ot____nom63_aux,axiom,
( ot____nom63_aux('fmb_$i_1')
& ot____nom63_aux('fmb_$i_2') ) ).
tff(declare_ot____nom64_aux,type,
ot____nom64_aux: $i > $o ).
tff(predicate_ot____nom64_aux,axiom,
( ot____nom64_aux('fmb_$i_1')
& ot____nom64_aux('fmb_$i_2') ) ).
tff(declare_ot____nom7_aux,type,
ot____nom7_aux: $i > $o ).
tff(predicate_ot____nom7_aux,axiom,
( ot____nom7_aux('fmb_$i_1')
& ~ ot____nom7_aux('fmb_$i_2') ) ).
tff(declare_ot____nom8_aux,type,
ot____nom8_aux: $i > $o ).
tff(predicate_ot____nom8_aux,axiom,
( ot____nom8_aux('fmb_$i_1')
& ot____nom8_aux('fmb_$i_2') ) ).
tff(declare_ot____nom9_aux,type,
ot____nom9_aux: $i > $o ).
tff(predicate_ot____nom9_aux,axiom,
( ot____nom9_aux('fmb_$i_1')
& ot____nom9_aux('fmb_$i_2') ) ).
tff(declare_wineflavor_aux,type,
wineflavor_aux: $i > $o ).
tff(predicate_wineflavor_aux,axiom,
( wineflavor_aux('fmb_$i_1')
& ~ wineflavor_aux('fmb_$i_2') ) ).
tff(declare_winegrape_aux,type,
winegrape_aux: $i > $o ).
tff(predicate_winegrape_aux,axiom,
( winegrape_aux('fmb_$i_1')
& winegrape_aux('fmb_$i_2') ) ).
tff(declare_winesugar_aux,type,
winesugar_aux: $i > $o ).
tff(predicate_winesugar_aux,axiom,
( winesugar_aux('fmb_$i_1')
& ~ winesugar_aux('fmb_$i_2') ) ).
tff(declare_winery_aux,type,
winery_aux: $i > $o ).
tff(predicate_winery_aux,axiom,
( winery_aux('fmb_$i_1')
& winery_aux('fmb_$i_2') ) ).
tff(declare_zinfandel_aux,type,
zinfandel_aux: $i > $o ).
tff(predicate_zinfandel_aux,axiom,
( zinfandel_aux('fmb_$i_1')
& ~ zinfandel_aux('fmb_$i_2') ) ).
tff(declare_winebody_aux,type,
winebody_aux: $i > $o ).
tff(predicate_winebody_aux,axiom,
( winebody_aux('fmb_$i_1')
& winebody_aux('fmb_$i_2') ) ).
tff(declare_winecolor_aux,type,
winecolor_aux: $i > $o ).
tff(predicate_winecolor_aux,axiom,
( winecolor_aux('fmb_$i_1')
& winecolor_aux('fmb_$i_2') ) ).
tff(declare_whiteburgundy_aux,type,
whiteburgundy_aux: $i > $o ).
tff(predicate_whiteburgundy_aux,axiom,
( whiteburgundy_aux('fmb_$i_1')
& ~ whiteburgundy_aux('fmb_$i_2') ) ).
tff(declare_whitewine_aux,type,
whitewine_aux: $i > $o ).
tff(predicate_whitewine_aux,axiom,
( whitewine_aux('fmb_$i_1')
& ~ whitewine_aux('fmb_$i_2') ) ).
tff(declare_muscadet_aux,type,
muscadet_aux: $i > $o ).
tff(predicate_muscadet_aux,axiom,
( muscadet_aux('fmb_$i_1')
& ~ muscadet_aux('fmb_$i_2') ) ).
tff(declare_meursault_aux,type,
meursault_aux: $i > $o ).
tff(predicate_meursault_aux,axiom,
( meursault_aux('fmb_$i_1')
& ~ meursault_aux('fmb_$i_2') ) ).
tff(declare_meritage_aux,type,
meritage_aux: $i > $o ).
tff(predicate_meritage_aux,axiom,
( meritage_aux('fmb_$i_1')
& ~ meritage_aux('fmb_$i_2') ) ).
tff(declare_margaux_aux,type,
margaux_aux: $i > $o ).
tff(predicate_margaux_aux,axiom,
( margaux_aux('fmb_$i_1')
& ~ margaux_aux('fmb_$i_2') ) ).
tff(declare_icewine_aux,type,
icewine_aux: $i > $o ).
tff(predicate_icewine_aux,axiom,
( icewine_aux('fmb_$i_1')
& ~ icewine_aux('fmb_$i_2') ) ).
tff(declare_dryriesling_aux,type,
dryriesling_aux: $i > $o ).
tff(predicate_dryriesling_aux,axiom,
( dryriesling_aux('fmb_$i_1')
& ~ dryriesling_aux('fmb_$i_2') ) ).
tff(declare_dessertwine_aux,type,
dessertwine_aux: $i > $o ).
tff(predicate_dessertwine_aux,axiom,
( dessertwine_aux('fmb_$i_1')
& ~ dessertwine_aux('fmb_$i_2') ) ).
tff(declare_cabernetsauvignon_aux,type,
cabernetsauvignon_aux: $i > $o ).
tff(predicate_cabernetsauvignon_aux,axiom,
( cabernetsauvignon_aux('fmb_$i_1')
& ~ cabernetsauvignon_aux('fmb_$i_2') ) ).
tff(declare_cabernetfranc_aux,type,
cabernetfranc_aux: $i > $o ).
tff(predicate_cabernetfranc_aux,axiom,
( cabernetfranc_aux('fmb_$i_1')
& ~ cabernetfranc_aux('fmb_$i_2') ) ).
tff(declare_beaujolais_aux,type,
beaujolais_aux: $i > $o ).
tff(predicate_beaujolais_aux,axiom,
( beaujolais_aux('fmb_$i_1')
& ~ beaujolais_aux('fmb_$i_2') ) ).
tff(declare_anjou_aux,type,
anjou_aux: $i > $o ).
tff(predicate_anjou_aux,axiom,
( anjou_aux('fmb_$i_1')
& ~ anjou_aux('fmb_$i_2') ) ).
tff(declare_chardonnay_aux,type,
chardonnay_aux: $i > $o ).
tff(predicate_chardonnay_aux,axiom,
( chardonnay_aux('fmb_$i_1')
& ~ chardonnay_aux('fmb_$i_2') ) ).
tff(declare_cheninblanc_aux,type,
cheninblanc_aux: $i > $o ).
tff(predicate_cheninblanc_aux,axiom,
( cheninblanc_aux('fmb_$i_1')
& ~ cheninblanc_aux('fmb_$i_2') ) ).
tff(declare_chianti_aux,type,
chianti_aux: $i > $o ).
tff(predicate_chianti_aux,axiom,
( chianti_aux('fmb_$i_1')
& ~ chianti_aux('fmb_$i_2') ) ).
tff(declare_cotesdor_aux,type,
cotesdor_aux: $i > $o ).
tff(predicate_cotesdor_aux,axiom,
( cotesdor_aux('fmb_$i_1')
& ~ cotesdor_aux('fmb_$i_2') ) ).
tff(declare_merlot_aux,type,
merlot_aux: $i > $o ).
tff(predicate_merlot_aux,axiom,
( merlot_aux('fmb_$i_1')
& ~ merlot_aux('fmb_$i_2') ) ).
tff(declare_pauillac_aux,type,
pauillac_aux: $i > $o ).
tff(predicate_pauillac_aux,axiom,
( pauillac_aux('fmb_$i_1')
& ~ pauillac_aux('fmb_$i_2') ) ).
tff(declare_petitesyrah_aux,type,
petitesyrah_aux: $i > $o ).
tff(predicate_petitesyrah_aux,axiom,
( petitesyrah_aux('fmb_$i_1')
& ~ petitesyrah_aux('fmb_$i_2') ) ).
tff(declare_pinotnoir_aux,type,
pinotnoir_aux: $i > $o ).
tff(predicate_pinotnoir_aux,axiom,
( pinotnoir_aux('fmb_$i_1')
& ~ pinotnoir_aux('fmb_$i_2') ) ).
tff(declare_port_aux,type,
port_aux: $i > $o ).
tff(predicate_port_aux,axiom,
( port_aux('fmb_$i_1')
& ~ port_aux('fmb_$i_2') ) ).
tff(declare_redtablewine_aux,type,
redtablewine_aux: $i > $o ).
tff(predicate_redtablewine_aux,axiom,
( redtablewine_aux('fmb_$i_1')
& ~ redtablewine_aux('fmb_$i_2') ) ).
tff(declare_region_aux,type,
region_aux: $i > $o ).
tff(predicate_region_aux,axiom,
( region_aux('fmb_$i_1')
& region_aux('fmb_$i_2') ) ).
tff(declare_riesling_aux,type,
riesling_aux: $i > $o ).
tff(predicate_riesling_aux,axiom,
( riesling_aux('fmb_$i_1')
& ~ riesling_aux('fmb_$i_2') ) ).
tff(declare_sancerre_aux,type,
sancerre_aux: $i > $o ).
tff(predicate_sancerre_aux,axiom,
( sancerre_aux('fmb_$i_1')
& ~ sancerre_aux('fmb_$i_2') ) ).
tff(declare_sauternes_aux,type,
sauternes_aux: $i > $o ).
tff(predicate_sauternes_aux,axiom,
( sauternes_aux('fmb_$i_1')
& ~ sauternes_aux('fmb_$i_2') ) ).
tff(declare_sauvignonblanc_aux,type,
sauvignonblanc_aux: $i > $o ).
tff(predicate_sauvignonblanc_aux,axiom,
( sauvignonblanc_aux('fmb_$i_1')
& ~ sauvignonblanc_aux('fmb_$i_2') ) ).
tff(declare_semillon_aux,type,
semillon_aux: $i > $o ).
tff(predicate_semillon_aux,axiom,
( semillon_aux('fmb_$i_1')
& ~ semillon_aux('fmb_$i_2') ) ).
tff(declare_stemilion_aux,type,
stemilion_aux: $i > $o ).
tff(predicate_stemilion_aux,axiom,
( stemilion_aux('fmb_$i_1')
& ~ stemilion_aux('fmb_$i_2') ) ).
tff(declare_sweetriesling_aux,type,
sweetriesling_aux: $i > $o ).
tff(predicate_sweetriesling_aux,axiom,
( sweetriesling_aux('fmb_$i_1')
& ~ sweetriesling_aux('fmb_$i_2') ) ).
tff(declare_kaon2namedobjects,type,
kaon2namedobjects: $i > $o ).
tff(predicate_kaon2namedobjects,axiom,
( kaon2namedobjects('fmb_$i_1')
& kaon2namedobjects('fmb_$i_2') ) ).
tff(declare_vintageyear_aux,type,
vintageyear_aux: $i > $o ).
tff(predicate_vintageyear_aux,axiom,
( vintageyear_aux('fmb_$i_1')
& ~ vintageyear_aux('fmb_$i_2') ) ).
tff(declare_hasvintageyear_aux,type,
hasvintageyear_aux: ( $i * $i ) > $o ).
tff(predicate_hasvintageyear_aux,axiom,
( hasvintageyear_aux('fmb_$i_1','fmb_$i_1')
& ~ hasvintageyear_aux('fmb_$i_1','fmb_$i_2')
& ~ hasvintageyear_aux('fmb_$i_2','fmb_$i_1')
& ~ hasvintageyear_aux('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_madefromgrape,type,
madefromgrape: ( $i * $i ) > $o ).
tff(predicate_madefromgrape,axiom,
( madefromgrape('fmb_$i_1','fmb_$i_1')
& ~ madefromgrape('fmb_$i_1','fmb_$i_2')
& ~ madefromgrape('fmb_$i_2','fmb_$i_1')
& ~ madefromgrape('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_locatedin,type,
locatedin: ( $i * $i ) > $o ).
tff(predicate_locatedin,axiom,
( locatedin('fmb_$i_1','fmb_$i_1')
& ~ locatedin('fmb_$i_1','fmb_$i_2')
& locatedin('fmb_$i_2','fmb_$i_1')
& locatedin('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_hassugar,type,
hassugar: ( $i * $i ) > $o ).
tff(predicate_hassugar,axiom,
( hassugar('fmb_$i_1','fmb_$i_1')
& ~ hassugar('fmb_$i_1','fmb_$i_2')
& ~ hassugar('fmb_$i_2','fmb_$i_1')
& ~ hassugar('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_hasmaker,type,
hasmaker: ( $i * $i ) > $o ).
tff(predicate_hasmaker,axiom,
( hasmaker('fmb_$i_1','fmb_$i_1')
& ~ hasmaker('fmb_$i_1','fmb_$i_2')
& hasmaker('fmb_$i_2','fmb_$i_1')
& ~ hasmaker('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_hasflavor,type,
hasflavor: ( $i * $i ) > $o ).
tff(predicate_hasflavor,axiom,
( hasflavor('fmb_$i_1','fmb_$i_1')
& ~ hasflavor('fmb_$i_1','fmb_$i_2')
& ~ hasflavor('fmb_$i_2','fmb_$i_1')
& ~ hasflavor('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_hascolor,type,
hascolor: ( $i * $i ) > $o ).
tff(predicate_hascolor,axiom,
( hascolor('fmb_$i_1','fmb_$i_1')
& ~ hascolor('fmb_$i_1','fmb_$i_2')
& ~ hascolor('fmb_$i_2','fmb_$i_1')
& ~ hascolor('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_hasbody,type,
hasbody: ( $i * $i ) > $o ).
tff(predicate_hasbody,axiom,
( hasbody('fmb_$i_1','fmb_$i_1')
& ~ hasbody('fmb_$i_1','fmb_$i_2')
& ~ hasbody('fmb_$i_2','fmb_$i_1')
& ~ hasbody('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_adjacentregion_aux,type,
adjacentregion_aux: ( $i * $i ) > $o ).
tff(predicate_adjacentregion_aux,axiom,
( ~ adjacentregion_aux('fmb_$i_1','fmb_$i_1')
& ~ adjacentregion_aux('fmb_$i_1','fmb_$i_2')
& ~ adjacentregion_aux('fmb_$i_2','fmb_$i_1')
& ~ adjacentregion_aux('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_adjacentregion,type,
adjacentregion: ( $i * $i ) > $o ).
tff(predicate_adjacentregion,axiom,
( adjacentregion('fmb_$i_1','fmb_$i_1')
& adjacentregion('fmb_$i_1','fmb_$i_2')
& adjacentregion('fmb_$i_2','fmb_$i_1')
& adjacentregion('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_hasvintageyear,type,
hasvintageyear: ( $i * $i ) > $o ).
tff(predicate_hasvintageyear,axiom,
( hasvintageyear('fmb_$i_1','fmb_$i_1')
& ~ hasvintageyear('fmb_$i_1','fmb_$i_2')
& ~ hasvintageyear('fmb_$i_2','fmb_$i_1')
& ~ hasvintageyear('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_ot____nom1,type,
ot____nom1: $i > $o ).
tff(predicate_ot____nom1,axiom,
( ot____nom1('fmb_$i_1')
& ot____nom1('fmb_$i_2') ) ).
tff(declare_ot____nom10,type,
ot____nom10: $i > $o ).
tff(predicate_ot____nom10,axiom,
( ot____nom10('fmb_$i_1')
& ot____nom10('fmb_$i_2') ) ).
tff(declare_ot____nom11,type,
ot____nom11: $i > $o ).
tff(predicate_ot____nom11,axiom,
( ot____nom11('fmb_$i_1')
& ~ ot____nom11('fmb_$i_2') ) ).
tff(declare_ot____nom12,type,
ot____nom12: $i > $o ).
tff(predicate_ot____nom12,axiom,
( ot____nom12('fmb_$i_1')
& ot____nom12('fmb_$i_2') ) ).
tff(declare_ot____nom13,type,
ot____nom13: $i > $o ).
tff(predicate_ot____nom13,axiom,
( ~ ot____nom13('fmb_$i_1')
& ot____nom13('fmb_$i_2') ) ).
tff(declare_ot____nom14,type,
ot____nom14: $i > $o ).
tff(predicate_ot____nom14,axiom,
( ot____nom14('fmb_$i_1')
& ot____nom14('fmb_$i_2') ) ).
tff(declare_ot____nom15,type,
ot____nom15: $i > $o ).
tff(predicate_ot____nom15,axiom,
( ot____nom15('fmb_$i_1')
& ot____nom15('fmb_$i_2') ) ).
tff(declare_ot____nom16,type,
ot____nom16: $i > $o ).
tff(predicate_ot____nom16,axiom,
( ot____nom16('fmb_$i_1')
& ot____nom16('fmb_$i_2') ) ).
tff(declare_ot____nom17,type,
ot____nom17: $i > $o ).
tff(predicate_ot____nom17,axiom,
( ot____nom17('fmb_$i_1')
& ot____nom17('fmb_$i_2') ) ).
tff(declare_ot____nom18,type,
ot____nom18: $i > $o ).
tff(predicate_ot____nom18,axiom,
( ot____nom18('fmb_$i_1')
& ot____nom18('fmb_$i_2') ) ).
tff(declare_ot____nom19,type,
ot____nom19: $i > $o ).
tff(predicate_ot____nom19,axiom,
( ot____nom19('fmb_$i_1')
& ot____nom19('fmb_$i_2') ) ).
tff(declare_ot____nom2,type,
ot____nom2: $i > $o ).
tff(predicate_ot____nom2,axiom,
( ot____nom2('fmb_$i_1')
& ot____nom2('fmb_$i_2') ) ).
tff(declare_ot____nom20,type,
ot____nom20: $i > $o ).
tff(predicate_ot____nom20,axiom,
( ot____nom20('fmb_$i_1')
& ot____nom20('fmb_$i_2') ) ).
tff(declare_ot____nom21,type,
ot____nom21: $i > $o ).
tff(predicate_ot____nom21,axiom,
( ot____nom21('fmb_$i_1')
& ot____nom21('fmb_$i_2') ) ).
tff(declare_ot____nom22,type,
ot____nom22: $i > $o ).
tff(predicate_ot____nom22,axiom,
( ot____nom22('fmb_$i_1')
& ot____nom22('fmb_$i_2') ) ).
tff(declare_ot____nom23,type,
ot____nom23: $i > $o ).
tff(predicate_ot____nom23,axiom,
( ot____nom23('fmb_$i_1')
& ot____nom23('fmb_$i_2') ) ).
tff(declare_ot____nom24,type,
ot____nom24: $i > $o ).
tff(predicate_ot____nom24,axiom,
( ot____nom24('fmb_$i_1')
& ot____nom24('fmb_$i_2') ) ).
tff(declare_ot____nom25,type,
ot____nom25: $i > $o ).
tff(predicate_ot____nom25,axiom,
( ot____nom25('fmb_$i_1')
& ot____nom25('fmb_$i_2') ) ).
tff(declare_ot____nom26,type,
ot____nom26: $i > $o ).
tff(predicate_ot____nom26,axiom,
( ot____nom26('fmb_$i_1')
& ot____nom26('fmb_$i_2') ) ).
tff(declare_ot____nom27,type,
ot____nom27: $i > $o ).
tff(predicate_ot____nom27,axiom,
( ot____nom27('fmb_$i_1')
& ot____nom27('fmb_$i_2') ) ).
tff(declare_ot____nom28,type,
ot____nom28: $i > $o ).
tff(predicate_ot____nom28,axiom,
( ot____nom28('fmb_$i_1')
& ot____nom28('fmb_$i_2') ) ).
tff(declare_ot____nom29,type,
ot____nom29: $i > $o ).
tff(predicate_ot____nom29,axiom,
( ot____nom29('fmb_$i_1')
& ot____nom29('fmb_$i_2') ) ).
tff(declare_ot____nom3,type,
ot____nom3: $i > $o ).
tff(predicate_ot____nom3,axiom,
( ot____nom3('fmb_$i_1')
& ot____nom3('fmb_$i_2') ) ).
tff(declare_ot____nom30,type,
ot____nom30: $i > $o ).
tff(predicate_ot____nom30,axiom,
( ot____nom30('fmb_$i_1')
& ot____nom30('fmb_$i_2') ) ).
tff(declare_ot____nom31,type,
ot____nom31: $i > $o ).
tff(predicate_ot____nom31,axiom,
( ot____nom31('fmb_$i_1')
& ot____nom31('fmb_$i_2') ) ).
tff(declare_ot____nom32,type,
ot____nom32: $i > $o ).
tff(predicate_ot____nom32,axiom,
( ot____nom32('fmb_$i_1')
& ot____nom32('fmb_$i_2') ) ).
tff(declare_ot____nom33,type,
ot____nom33: $i > $o ).
tff(predicate_ot____nom33,axiom,
( ot____nom33('fmb_$i_1')
& ot____nom33('fmb_$i_2') ) ).
tff(declare_ot____nom34,type,
ot____nom34: $i > $o ).
tff(predicate_ot____nom34,axiom,
( ot____nom34('fmb_$i_1')
& ot____nom34('fmb_$i_2') ) ).
tff(declare_ot____nom35,type,
ot____nom35: $i > $o ).
tff(predicate_ot____nom35,axiom,
( ot____nom35('fmb_$i_1')
& ot____nom35('fmb_$i_2') ) ).
tff(declare_ot____nom36,type,
ot____nom36: $i > $o ).
tff(predicate_ot____nom36,axiom,
( ot____nom36('fmb_$i_1')
& ot____nom36('fmb_$i_2') ) ).
tff(declare_ot____nom37,type,
ot____nom37: $i > $o ).
tff(predicate_ot____nom37,axiom,
( ot____nom37('fmb_$i_1')
& ot____nom37('fmb_$i_2') ) ).
tff(declare_ot____nom38,type,
ot____nom38: $i > $o ).
tff(predicate_ot____nom38,axiom,
( ot____nom38('fmb_$i_1')
& ot____nom38('fmb_$i_2') ) ).
tff(declare_ot____nom39,type,
ot____nom39: $i > $o ).
tff(predicate_ot____nom39,axiom,
( ot____nom39('fmb_$i_1')
& ot____nom39('fmb_$i_2') ) ).
tff(declare_ot____nom4,type,
ot____nom4: $i > $o ).
tff(predicate_ot____nom4,axiom,
( ~ ot____nom4('fmb_$i_1')
& ot____nom4('fmb_$i_2') ) ).
tff(declare_ot____nom40,type,
ot____nom40: $i > $o ).
tff(predicate_ot____nom40,axiom,
( ot____nom40('fmb_$i_1')
& ot____nom40('fmb_$i_2') ) ).
tff(declare_ot____nom41,type,
ot____nom41: $i > $o ).
tff(predicate_ot____nom41,axiom,
( ~ ot____nom41('fmb_$i_1')
& ot____nom41('fmb_$i_2') ) ).
tff(declare_ot____nom42,type,
ot____nom42: $i > $o ).
tff(predicate_ot____nom42,axiom,
( ot____nom42('fmb_$i_1')
& ot____nom42('fmb_$i_2') ) ).
tff(declare_ot____nom43,type,
ot____nom43: $i > $o ).
tff(predicate_ot____nom43,axiom,
( ot____nom43('fmb_$i_1')
& ot____nom43('fmb_$i_2') ) ).
tff(declare_ot____nom44,type,
ot____nom44: $i > $o ).
tff(predicate_ot____nom44,axiom,
( ot____nom44('fmb_$i_1')
& ot____nom44('fmb_$i_2') ) ).
tff(declare_ot____nom45,type,
ot____nom45: $i > $o ).
tff(predicate_ot____nom45,axiom,
( ot____nom45('fmb_$i_1')
& ~ ot____nom45('fmb_$i_2') ) ).
tff(declare_ot____nom46,type,
ot____nom46: $i > $o ).
tff(predicate_ot____nom46,axiom,
( ot____nom46('fmb_$i_1')
& ot____nom46('fmb_$i_2') ) ).
tff(declare_ot____nom47,type,
ot____nom47: $i > $o ).
tff(predicate_ot____nom47,axiom,
( ot____nom47('fmb_$i_1')
& ot____nom47('fmb_$i_2') ) ).
tff(declare_ot____nom48,type,
ot____nom48: $i > $o ).
tff(predicate_ot____nom48,axiom,
( ot____nom48('fmb_$i_1')
& ot____nom48('fmb_$i_2') ) ).
tff(declare_ot____nom49,type,
ot____nom49: $i > $o ).
tff(predicate_ot____nom49,axiom,
( ot____nom49('fmb_$i_1')
& ot____nom49('fmb_$i_2') ) ).
tff(declare_ot____nom5,type,
ot____nom5: $i > $o ).
tff(predicate_ot____nom5,axiom,
( ot____nom5('fmb_$i_1')
& ot____nom5('fmb_$i_2') ) ).
tff(declare_ot____nom50,type,
ot____nom50: $i > $o ).
tff(predicate_ot____nom50,axiom,
( ot____nom50('fmb_$i_1')
& ot____nom50('fmb_$i_2') ) ).
tff(declare_ot____nom51,type,
ot____nom51: $i > $o ).
tff(predicate_ot____nom51,axiom,
( ot____nom51('fmb_$i_1')
& ot____nom51('fmb_$i_2') ) ).
tff(declare_ot____nom52,type,
ot____nom52: $i > $o ).
tff(predicate_ot____nom52,axiom,
( ot____nom52('fmb_$i_1')
& ot____nom52('fmb_$i_2') ) ).
tff(declare_ot____nom53,type,
ot____nom53: $i > $o ).
tff(predicate_ot____nom53,axiom,
( ot____nom53('fmb_$i_1')
& ot____nom53('fmb_$i_2') ) ).
tff(declare_ot____nom54,type,
ot____nom54: $i > $o ).
tff(predicate_ot____nom54,axiom,
( ot____nom54('fmb_$i_1')
& ot____nom54('fmb_$i_2') ) ).
tff(declare_ot____nom55,type,
ot____nom55: $i > $o ).
tff(predicate_ot____nom55,axiom,
( ot____nom55('fmb_$i_1')
& ot____nom55('fmb_$i_2') ) ).
tff(declare_ot____nom56,type,
ot____nom56: $i > $o ).
tff(predicate_ot____nom56,axiom,
( ot____nom56('fmb_$i_1')
& ~ ot____nom56('fmb_$i_2') ) ).
tff(declare_ot____nom57,type,
ot____nom57: $i > $o ).
tff(predicate_ot____nom57,axiom,
( ot____nom57('fmb_$i_1')
& ot____nom57('fmb_$i_2') ) ).
tff(declare_ot____nom58,type,
ot____nom58: $i > $o ).
tff(predicate_ot____nom58,axiom,
( ot____nom58('fmb_$i_1')
& ~ ot____nom58('fmb_$i_2') ) ).
tff(declare_ot____nom59,type,
ot____nom59: $i > $o ).
tff(predicate_ot____nom59,axiom,
( ot____nom59('fmb_$i_1')
& ot____nom59('fmb_$i_2') ) ).
tff(declare_ot____nom6,type,
ot____nom6: $i > $o ).
tff(predicate_ot____nom6,axiom,
( ot____nom6('fmb_$i_1')
& ot____nom6('fmb_$i_2') ) ).
tff(declare_ot____nom60,type,
ot____nom60: $i > $o ).
tff(predicate_ot____nom60,axiom,
( ot____nom60('fmb_$i_1')
& ot____nom60('fmb_$i_2') ) ).
tff(declare_ot____nom61,type,
ot____nom61: $i > $o ).
tff(predicate_ot____nom61,axiom,
( ot____nom61('fmb_$i_1')
& ot____nom61('fmb_$i_2') ) ).
tff(declare_ot____nom62,type,
ot____nom62: $i > $o ).
tff(predicate_ot____nom62,axiom,
( ot____nom62('fmb_$i_1')
& ot____nom62('fmb_$i_2') ) ).
tff(declare_ot____nom63,type,
ot____nom63: $i > $o ).
tff(predicate_ot____nom63,axiom,
( ot____nom63('fmb_$i_1')
& ot____nom63('fmb_$i_2') ) ).
tff(declare_ot____nom64,type,
ot____nom64: $i > $o ).
tff(predicate_ot____nom64,axiom,
( ot____nom64('fmb_$i_1')
& ot____nom64('fmb_$i_2') ) ).
tff(declare_ot____nom7,type,
ot____nom7: $i > $o ).
tff(predicate_ot____nom7,axiom,
( ot____nom7('fmb_$i_1')
& ~ ot____nom7('fmb_$i_2') ) ).
tff(declare_ot____nom8,type,
ot____nom8: $i > $o ).
tff(predicate_ot____nom8,axiom,
( ot____nom8('fmb_$i_1')
& ot____nom8('fmb_$i_2') ) ).
tff(declare_ot____nom9,type,
ot____nom9: $i > $o ).
tff(predicate_ot____nom9,axiom,
( ot____nom9('fmb_$i_1')
& ot____nom9('fmb_$i_2') ) ).
tff(declare_zinfandel,type,
zinfandel: $i > $o ).
tff(predicate_zinfandel,axiom,
( zinfandel('fmb_$i_1')
& ~ zinfandel('fmb_$i_2') ) ).
tff(declare_winery,type,
winery: $i > $o ).
tff(predicate_winery,axiom,
( winery('fmb_$i_1')
& winery('fmb_$i_2') ) ).
tff(declare_winegrape,type,
winegrape: $i > $o ).
tff(predicate_winegrape,axiom,
( winegrape('fmb_$i_1')
& winegrape('fmb_$i_2') ) ).
tff(declare_winesugar,type,
winesugar: $i > $o ).
tff(predicate_winesugar,axiom,
( winesugar('fmb_$i_1')
& winesugar('fmb_$i_2') ) ).
tff(declare_wineflavor,type,
wineflavor: $i > $o ).
tff(predicate_wineflavor,axiom,
( wineflavor('fmb_$i_1')
& wineflavor('fmb_$i_2') ) ).
tff(declare_anjou,type,
anjou: $i > $o ).
tff(predicate_anjou,axiom,
( anjou('fmb_$i_1')
& ~ anjou('fmb_$i_2') ) ).
tff(declare_beaujolais,type,
beaujolais: $i > $o ).
tff(predicate_beaujolais,axiom,
( beaujolais('fmb_$i_1')
& ~ beaujolais('fmb_$i_2') ) ).
tff(declare_cabernetfranc,type,
cabernetfranc: $i > $o ).
tff(predicate_cabernetfranc,axiom,
( cabernetfranc('fmb_$i_1')
& ~ cabernetfranc('fmb_$i_2') ) ).
tff(declare_cabernetsauvignon,type,
cabernetsauvignon: $i > $o ).
tff(predicate_cabernetsauvignon,axiom,
( cabernetsauvignon('fmb_$i_1')
& ~ cabernetsauvignon('fmb_$i_2') ) ).
tff(declare_chardonnay,type,
chardonnay: $i > $o ).
tff(predicate_chardonnay,axiom,
( chardonnay('fmb_$i_1')
& ~ chardonnay('fmb_$i_2') ) ).
tff(declare_cheninblanc,type,
cheninblanc: $i > $o ).
tff(predicate_cheninblanc,axiom,
( cheninblanc('fmb_$i_1')
& ~ cheninblanc('fmb_$i_2') ) ).
tff(declare_chianti,type,
chianti: $i > $o ).
tff(predicate_chianti,axiom,
( chianti('fmb_$i_1')
& ~ chianti('fmb_$i_2') ) ).
tff(declare_cotesdor,type,
cotesdor: $i > $o ).
tff(predicate_cotesdor,axiom,
( cotesdor('fmb_$i_1')
& ~ cotesdor('fmb_$i_2') ) ).
tff(declare_dessertwine,type,
dessertwine: $i > $o ).
tff(predicate_dessertwine,axiom,
( dessertwine('fmb_$i_1')
& ~ dessertwine('fmb_$i_2') ) ).
tff(declare_dryriesling,type,
dryriesling: $i > $o ).
tff(predicate_dryriesling,axiom,
( dryriesling('fmb_$i_1')
& ~ dryriesling('fmb_$i_2') ) ).
tff(declare_icewine,type,
icewine: $i > $o ).
tff(predicate_icewine,axiom,
( icewine('fmb_$i_1')
& ~ icewine('fmb_$i_2') ) ).
tff(declare_margaux,type,
margaux: $i > $o ).
tff(predicate_margaux,axiom,
( margaux('fmb_$i_1')
& ~ margaux('fmb_$i_2') ) ).
tff(declare_meritage,type,
meritage: $i > $o ).
tff(predicate_meritage,axiom,
( meritage('fmb_$i_1')
& ~ meritage('fmb_$i_2') ) ).
tff(declare_merlot,type,
merlot: $i > $o ).
tff(predicate_merlot,axiom,
( merlot('fmb_$i_1')
& ~ merlot('fmb_$i_2') ) ).
tff(declare_meursault,type,
meursault: $i > $o ).
tff(predicate_meursault,axiom,
( meursault('fmb_$i_1')
& ~ meursault('fmb_$i_2') ) ).
tff(declare_muscadet,type,
muscadet: $i > $o ).
tff(predicate_muscadet,axiom,
( muscadet('fmb_$i_1')
& ~ muscadet('fmb_$i_2') ) ).
tff(declare_pauillac,type,
pauillac: $i > $o ).
tff(predicate_pauillac,axiom,
( pauillac('fmb_$i_1')
& ~ pauillac('fmb_$i_2') ) ).
tff(declare_petitesyrah,type,
petitesyrah: $i > $o ).
tff(predicate_petitesyrah,axiom,
( petitesyrah('fmb_$i_1')
& ~ petitesyrah('fmb_$i_2') ) ).
tff(declare_pinotnoir,type,
pinotnoir: $i > $o ).
tff(predicate_pinotnoir,axiom,
( pinotnoir('fmb_$i_1')
& ~ pinotnoir('fmb_$i_2') ) ).
tff(declare_port,type,
port: $i > $o ).
tff(predicate_port,axiom,
( port('fmb_$i_1')
& ~ port('fmb_$i_2') ) ).
tff(declare_redtablewine,type,
redtablewine: $i > $o ).
tff(predicate_redtablewine,axiom,
( redtablewine('fmb_$i_1')
& ~ redtablewine('fmb_$i_2') ) ).
tff(declare_region,type,
region: $i > $o ).
tff(predicate_region,axiom,
( region('fmb_$i_1')
& region('fmb_$i_2') ) ).
tff(declare_riesling,type,
riesling: $i > $o ).
tff(predicate_riesling,axiom,
( riesling('fmb_$i_1')
& ~ riesling('fmb_$i_2') ) ).
tff(declare_sancerre,type,
sancerre: $i > $o ).
tff(predicate_sancerre,axiom,
( sancerre('fmb_$i_1')
& ~ sancerre('fmb_$i_2') ) ).
tff(declare_sauternes,type,
sauternes: $i > $o ).
tff(predicate_sauternes,axiom,
( sauternes('fmb_$i_1')
& ~ sauternes('fmb_$i_2') ) ).
tff(declare_sauvignonblanc,type,
sauvignonblanc: $i > $o ).
tff(predicate_sauvignonblanc,axiom,
( sauvignonblanc('fmb_$i_1')
& ~ sauvignonblanc('fmb_$i_2') ) ).
tff(declare_semillon,type,
semillon: $i > $o ).
tff(predicate_semillon,axiom,
( semillon('fmb_$i_1')
& ~ semillon('fmb_$i_2') ) ).
tff(declare_stemilion,type,
stemilion: $i > $o ).
tff(predicate_stemilion,axiom,
( stemilion('fmb_$i_1')
& ~ stemilion('fmb_$i_2') ) ).
tff(declare_sweetriesling,type,
sweetriesling: $i > $o ).
tff(predicate_sweetriesling,axiom,
( sweetriesling('fmb_$i_1')
& ~ sweetriesling('fmb_$i_2') ) ).
tff(declare_vintageyear,type,
vintageyear: $i > $o ).
tff(predicate_vintageyear,axiom,
( vintageyear('fmb_$i_1')
& ~ vintageyear('fmb_$i_2') ) ).
tff(declare_whiteburgundy,type,
whiteburgundy: $i > $o ).
tff(predicate_whiteburgundy,axiom,
( whiteburgundy('fmb_$i_1')
& ~ whiteburgundy('fmb_$i_2') ) ).
tff(declare_whitewine,type,
whitewine: $i > $o ).
tff(predicate_whitewine,axiom,
( whitewine('fmb_$i_1')
& ~ whitewine('fmb_$i_2') ) ).
tff(declare_winebody,type,
winebody: $i > $o ).
tff(predicate_winebody,axiom,
( winebody('fmb_$i_1')
& winebody('fmb_$i_2') ) ).
tff(declare_winecolor,type,
winecolor: $i > $o ).
tff(predicate_winecolor,axiom,
( winecolor('fmb_$i_1')
& winecolor('fmb_$i_2') ) ).
tff(declare_q0,type,
q0: $i > $o ).
tff(predicate_q0,axiom,
( q0('fmb_$i_1')
& ~ q0('fmb_$i_2') ) ).
tff(declare_medoc,type,
medoc: $i > $o ).
tff(predicate_medoc,axiom,
( medoc('fmb_$i_1')
& ~ medoc('fmb_$i_2') ) ).
tff(declare_redwine,type,
redwine: $i > $o ).
tff(predicate_redwine,axiom,
( redwine('fmb_$i_1')
& ~ redwine('fmb_$i_2') ) ).
tff(declare_kaon2equal,type,
kaon2equal: ( $i * $i ) > $o ).
tff(predicate_kaon2equal,axiom,
( kaon2equal('fmb_$i_1','fmb_$i_1')
& ~ kaon2equal('fmb_$i_1','fmb_$i_2')
& ~ kaon2equal('fmb_$i_2','fmb_$i_1')
& kaon2equal('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_bordeaux,type,
bordeaux: $i > $o ).
tff(predicate_bordeaux,axiom,
( bordeaux('fmb_$i_1')
& ~ bordeaux('fmb_$i_2') ) ).
tff(declare_q1,type,
q1: $i > $o ).
tff(predicate_q1,axiom,
( q1('fmb_$i_1')
& q1('fmb_$i_2') ) ).
tff(declare_q2,type,
q2: $i > $o ).
tff(predicate_q2,axiom,
( q2('fmb_$i_1')
& q2('fmb_$i_2') ) ).
tff(declare_q9,type,
q9: $i > $o ).
tff(predicate_q9,axiom,
( ~ q9('fmb_$i_1')
& q9('fmb_$i_2') ) ).
tff(declare_q10,type,
q10: $i > $o ).
tff(predicate_q10,axiom,
( ~ q10('fmb_$i_1')
& q10('fmb_$i_2') ) ).
tff(declare_q11,type,
q11: $i > $o ).
tff(predicate_q11,axiom,
( q11('fmb_$i_1')
& ~ q11('fmb_$i_2') ) ).
tff(declare_q12,type,
q12: $i > $o ).
tff(predicate_q12,axiom,
( q12('fmb_$i_1')
& ~ q12('fmb_$i_2') ) ).
tff(declare_whitetablewine,type,
whitetablewine: $i > $o ).
tff(predicate_whitetablewine,axiom,
( whitetablewine('fmb_$i_1')
& ~ whitetablewine('fmb_$i_2') ) ).
tff(declare_pinotblanc,type,
pinotblanc: $i > $o ).
tff(predicate_pinotblanc,axiom,
( pinotblanc('fmb_$i_1')
& ~ pinotblanc('fmb_$i_2') ) ).
tff(declare_semillonorsauvignonblanc,type,
semillonorsauvignonblanc: $i > $o ).
tff(predicate_semillonorsauvignonblanc,axiom,
( semillonorsauvignonblanc('fmb_$i_1')
& ~ semillonorsauvignonblanc('fmb_$i_2') ) ).
tff(declare_q13,type,
q13: $i > $o ).
tff(predicate_q13,axiom,
( q13('fmb_$i_1')
& ~ q13('fmb_$i_2') ) ).
tff(declare_gamay,type,
gamay: $i > $o ).
tff(predicate_gamay,axiom,
( gamay('fmb_$i_1')
& ~ gamay('fmb_$i_2') ) ).
tff(declare_q14,type,
q14: $i > $o ).
tff(predicate_q14,axiom,
( q14('fmb_$i_1')
& ~ q14('fmb_$i_2') ) ).
tff(declare_q15,type,
q15: $i > $o ).
tff(predicate_q15,axiom,
( q15('fmb_$i_1')
& ~ q15('fmb_$i_2') ) ).
tff(declare_rosewine,type,
rosewine: $i > $o ).
tff(predicate_rosewine,axiom,
( rosewine('fmb_$i_1')
& ~ rosewine('fmb_$i_2') ) ).
tff(declare_q16,type,
q16: $i > $o ).
tff(predicate_q16,axiom,
( q16('fmb_$i_1')
& q16('fmb_$i_2') ) ).
tff(declare_q17,type,
q17: $i > $o ).
tff(predicate_q17,axiom,
( q17('fmb_$i_1')
& q17('fmb_$i_2') ) ).
tff(declare_q18,type,
q18: $i > $o ).
tff(predicate_q18,axiom,
( q18('fmb_$i_1')
& q18('fmb_$i_2') ) ).
tff(declare_q19,type,
q19: $i > $o ).
tff(predicate_q19,axiom,
( q19('fmb_$i_1')
& q19('fmb_$i_2') ) ).
tff(declare_q20,type,
q20: $i > $o ).
tff(predicate_q20,axiom,
( q20('fmb_$i_1')
& ~ q20('fmb_$i_2') ) ).
tff(declare_q21,type,
q21: $i > $o ).
tff(predicate_q21,axiom,
( q21('fmb_$i_1')
& ~ q21('fmb_$i_2') ) ).
tff(declare_q22,type,
q22: $i > $o ).
tff(predicate_q22,axiom,
( q22('fmb_$i_1')
& q22('fmb_$i_2') ) ).
tff(declare_q23,type,
q23: $i > $o ).
tff(predicate_q23,axiom,
( q23('fmb_$i_1')
& q23('fmb_$i_2') ) ).
tff(declare_q24,type,
q24: $i > $o ).
tff(predicate_q24,axiom,
( q24('fmb_$i_1')
& ~ q24('fmb_$i_2') ) ).
tff(declare_americanwine,type,
americanwine: $i > $o ).
tff(predicate_americanwine,axiom,
( americanwine('fmb_$i_1')
& ~ americanwine('fmb_$i_2') ) ).
tff(declare_q26,type,
q26: $i > $o ).
tff(predicate_q26,axiom,
( q26('fmb_$i_1')
& q26('fmb_$i_2') ) ).
tff(declare_q27,type,
q27: $i > $o ).
tff(predicate_q27,axiom,
( q27('fmb_$i_1')
& q27('fmb_$i_2') ) ).
tff(declare_burgundy,type,
burgundy: $i > $o ).
tff(predicate_burgundy,axiom,
( burgundy('fmb_$i_1')
& ~ burgundy('fmb_$i_2') ) ).
tff(declare_q29,type,
q29: $i > $o ).
tff(predicate_q29,axiom,
( q29('fmb_$i_1')
& q29('fmb_$i_2') ) ).
tff(declare_q30,type,
q30: $i > $o ).
tff(predicate_q30,axiom,
( q30('fmb_$i_1')
& q30('fmb_$i_2') ) ).
tff(declare_q3,type,
q3: $i > $o ).
tff(predicate_q3,axiom,
( q3('fmb_$i_1')
& ~ q3('fmb_$i_2') ) ).
tff(declare_tours,type,
tours: $i > $o ).
tff(predicate_tours,axiom,
( ~ tours('fmb_$i_1')
& ~ tours('fmb_$i_2') ) ).
tff(declare_redburgundy,type,
redburgundy: $i > $o ).
tff(predicate_redburgundy,axiom,
( redburgundy('fmb_$i_1')
& ~ redburgundy('fmb_$i_2') ) ).
tff(declare_wine,type,
wine: $i > $o ).
tff(predicate_wine,axiom,
( wine('fmb_$i_1')
& ~ wine('fmb_$i_2') ) ).
tff(declare_q31,type,
q31: $i > $o ).
tff(predicate_q31,axiom,
( q31('fmb_$i_1')
& ~ q31('fmb_$i_2') ) ).
tff(declare_tablewine,type,
tablewine: $i > $o ).
tff(predicate_tablewine,axiom,
( tablewine('fmb_$i_1')
& ~ tablewine('fmb_$i_2') ) ).
tff(declare_drywine,type,
drywine: $i > $o ).
tff(predicate_drywine,axiom,
( drywine('fmb_$i_1')
& ~ drywine('fmb_$i_2') ) ).
tff(declare_q32,type,
q32: $i > $o ).
tff(predicate_q32,axiom,
( q32('fmb_$i_1')
& ~ q32('fmb_$i_2') ) ).
tff(declare_q33,type,
q33: $i > $o ).
tff(predicate_q33,axiom,
( q33('fmb_$i_1')
& q33('fmb_$i_2') ) ).
tff(declare_q34,type,
q34: $i > $o ).
tff(predicate_q34,axiom,
( q34('fmb_$i_1')
& q34('fmb_$i_2') ) ).
tff(declare_q35,type,
q35: $i > $o ).
tff(predicate_q35,axiom,
( q35('fmb_$i_1')
& ~ q35('fmb_$i_2') ) ).
tff(declare_fullbodiedwine,type,
fullbodiedwine: $i > $o ).
tff(predicate_fullbodiedwine,axiom,
( fullbodiedwine('fmb_$i_1')
& ~ fullbodiedwine('fmb_$i_2') ) ).
tff(declare_whitenonsweetwine,type,
whitenonsweetwine: $i > $o ).
tff(predicate_whitenonsweetwine,axiom,
( whitenonsweetwine('fmb_$i_1')
& ~ whitenonsweetwine('fmb_$i_2') ) ).
tff(declare_q36,type,
q36: $i > $o ).
tff(predicate_q36,axiom,
( q36('fmb_$i_1')
& q36('fmb_$i_2') ) ).
tff(declare_earlyharvest,type,
earlyharvest: $i > $o ).
tff(predicate_earlyharvest,axiom,
( earlyharvest('fmb_$i_1')
& ~ earlyharvest('fmb_$i_2') ) ).
tff(declare_q37,type,
q37: $i > $o ).
tff(predicate_q37,axiom,
( q37('fmb_$i_1')
& q37('fmb_$i_2') ) ).
tff(declare_q38,type,
q38: $i > $o ).
tff(predicate_q38,axiom,
( q38('fmb_$i_1')
& q38('fmb_$i_2') ) ).
tff(declare_q39,type,
q39: $i > $o ).
tff(predicate_q39,axiom,
( q39('fmb_$i_1')
& q39('fmb_$i_2') ) ).
tff(declare_q40,type,
q40: $i > $o ).
tff(predicate_q40,axiom,
( q40('fmb_$i_1')
& q40('fmb_$i_2') ) ).
tff(declare_q4,type,
q4: $i > $o ).
tff(predicate_q4,axiom,
( q4('fmb_$i_1')
& ~ q4('fmb_$i_2') ) ).
tff(declare_q41,type,
q41: $i > $o ).
tff(predicate_q41,axiom,
( q41('fmb_$i_1')
& q41('fmb_$i_2') ) ).
tff(declare_q42,type,
q42: $i > $o ).
tff(predicate_q42,axiom,
( q42('fmb_$i_1')
& q42('fmb_$i_2') ) ).
tff(declare_q43,type,
q43: $i > $o ).
tff(predicate_q43,axiom,
( q43('fmb_$i_1')
& q43('fmb_$i_2') ) ).
tff(declare_q44,type,
q44: $i > $o ).
tff(predicate_q44,axiom,
( q44('fmb_$i_1')
& ~ q44('fmb_$i_2') ) ).
tff(declare_q45,type,
q45: $i > $o ).
tff(predicate_q45,axiom,
( q45('fmb_$i_1')
& ~ q45('fmb_$i_2') ) ).
tff(declare_q46,type,
q46: $i > $o ).
tff(predicate_q46,axiom,
( q46('fmb_$i_1')
& q46('fmb_$i_2') ) ).
tff(declare_californiawine,type,
californiawine: $i > $o ).
tff(predicate_californiawine,axiom,
( californiawine('fmb_$i_1')
& ~ californiawine('fmb_$i_2') ) ).
tff(declare_q47,type,
q47: $i > $o ).
tff(predicate_q47,axiom,
( q47('fmb_$i_1')
& q47('fmb_$i_2') ) ).
tff(declare_q48,type,
q48: $i > $o ).
tff(predicate_q48,axiom,
( q48('fmb_$i_1')
& q48('fmb_$i_2') ) ).
tff(declare_germanwine,type,
germanwine: $i > $o ).
tff(predicate_germanwine,axiom,
( germanwine('fmb_$i_1')
& ~ germanwine('fmb_$i_2') ) ).
tff(declare_q49,type,
q49: $i > $o ).
tff(predicate_q49,axiom,
( q49('fmb_$i_1')
& q49('fmb_$i_2') ) ).
tff(declare_q50,type,
q50: $i > $o ).
tff(predicate_q50,axiom,
( q50('fmb_$i_1')
& q50('fmb_$i_2') ) ).
tff(declare_q5,type,
q5: $i > $o ).
tff(predicate_q5,axiom,
( q5('fmb_$i_1')
& ~ q5('fmb_$i_2') ) ).
tff(declare_q6,type,
q6: $i > $o ).
tff(predicate_q6,axiom,
( q6('fmb_$i_1')
& ~ q6('fmb_$i_2') ) ).
tff(declare_q72,type,
q72: $i > $o ).
tff(predicate_q72,axiom,
( q72('fmb_$i_1')
& ~ q72('fmb_$i_2') ) ).
tff(declare_q69,type,
q69: $i > $o ).
tff(predicate_q69,axiom,
( q69('fmb_$i_1')
& ~ q69('fmb_$i_2') ) ).
tff(declare_q63,type,
q63: $i > $o ).
tff(predicate_q63,axiom,
( q63('fmb_$i_1')
& ~ q63('fmb_$i_2') ) ).
tff(declare_frenchwine,type,
frenchwine: $i > $o ).
tff(predicate_frenchwine,axiom,
( ~ frenchwine('fmb_$i_1')
& ~ frenchwine('fmb_$i_2') ) ).
tff(declare_q51,type,
q51: $i > $o ).
tff(predicate_q51,axiom,
( ~ q51('fmb_$i_1')
& q51('fmb_$i_2') ) ).
tff(declare_q52,type,
q52: $i > $o ).
tff(predicate_q52,axiom,
( ~ q52('fmb_$i_1')
& q52('fmb_$i_2') ) ).
tff(declare_q55,type,
q55: $i > $o ).
tff(predicate_q55,axiom,
( q55('fmb_$i_1')
& q55('fmb_$i_2') ) ).
tff(declare_q56,type,
q56: $i > $o ).
tff(predicate_q56,axiom,
( q56('fmb_$i_1')
& q56('fmb_$i_2') ) ).
tff(declare_loire,type,
loire: $i > $o ).
tff(predicate_loire,axiom,
( loire('fmb_$i_1')
& ~ loire('fmb_$i_2') ) ).
tff(declare_q57,type,
q57: $i > $o ).
tff(predicate_q57,axiom,
( q57('fmb_$i_1')
& q57('fmb_$i_2') ) ).
tff(declare_q58,type,
q58: $i > $o ).
tff(predicate_q58,axiom,
( q58('fmb_$i_1')
& q58('fmb_$i_2') ) ).
tff(declare_alsatianwine,type,
alsatianwine: $i > $o ).
tff(predicate_alsatianwine,axiom,
( ~ alsatianwine('fmb_$i_1')
& ~ alsatianwine('fmb_$i_2') ) ).
tff(declare_q59,type,
q59: $i > $o ).
tff(predicate_q59,axiom,
( ~ q59('fmb_$i_1')
& q59('fmb_$i_2') ) ).
tff(declare_q60,type,
q60: $i > $o ).
tff(predicate_q60,axiom,
( ~ q60('fmb_$i_1')
& q60('fmb_$i_2') ) ).
tff(declare_italianwine,type,
italianwine: $i > $o ).
tff(predicate_italianwine,axiom,
( italianwine('fmb_$i_1')
& ~ italianwine('fmb_$i_2') ) ).
tff(declare_q61,type,
q61: $i > $o ).
tff(predicate_q61,axiom,
( q61('fmb_$i_1')
& q61('fmb_$i_2') ) ).
tff(declare_q62,type,
q62: $i > $o ).
tff(predicate_q62,axiom,
( q62('fmb_$i_1')
& q62('fmb_$i_2') ) ).
tff(declare_q64,type,
q64: $i > $o ).
tff(predicate_q64,axiom,
( q64('fmb_$i_1')
& q64('fmb_$i_2') ) ).
tff(declare_q65,type,
q65: $i > $o ).
tff(predicate_q65,axiom,
( q65('fmb_$i_1')
& q65('fmb_$i_2') ) ).
tff(declare_q66,type,
q66: $i > $o ).
tff(predicate_q66,axiom,
( q66('fmb_$i_1')
& q66('fmb_$i_2') ) ).
tff(declare_q67,type,
q67: $i > $o ).
tff(predicate_q67,axiom,
( q67('fmb_$i_1')
& q67('fmb_$i_2') ) ).
tff(declare_whitebordeaux,type,
whitebordeaux: $i > $o ).
tff(predicate_whitebordeaux,axiom,
( whitebordeaux('fmb_$i_1')
& ~ whitebordeaux('fmb_$i_2') ) ).
tff(declare_q68,type,
q68: $i > $o ).
tff(predicate_q68,axiom,
( q68('fmb_$i_1')
& ~ q68('fmb_$i_2') ) ).
tff(declare_q7,type,
q7: $i > $o ).
tff(predicate_q7,axiom,
( q7('fmb_$i_1')
& ~ q7('fmb_$i_2') ) ).
tff(declare_q70,type,
q70: $i > $o ).
tff(predicate_q70,axiom,
( q70('fmb_$i_1')
& ~ q70('fmb_$i_2') ) ).
tff(declare_sweetwine,type,
sweetwine: $i > $o ).
tff(predicate_sweetwine,axiom,
( sweetwine('fmb_$i_1')
& ~ sweetwine('fmb_$i_2') ) ).
tff(declare_lateharvest,type,
lateharvest: $i > $o ).
tff(predicate_lateharvest,axiom,
( lateharvest('fmb_$i_1')
& ~ lateharvest('fmb_$i_2') ) ).
tff(declare_q71,type,
q71: $i > $o ).
tff(predicate_q71,axiom,
( q71('fmb_$i_1')
& q71('fmb_$i_2') ) ).
tff(declare_texaswine,type,
texaswine: $i > $o ).
tff(predicate_texaswine,axiom,
( texaswine('fmb_$i_1')
& ~ texaswine('fmb_$i_2') ) ).
tff(declare_q73,type,
q73: $i > $o ).
tff(predicate_q73,axiom,
( q73('fmb_$i_1')
& q73('fmb_$i_2') ) ).
tff(declare_q74,type,
q74: $i > $o ).
tff(predicate_q74,axiom,
( q74('fmb_$i_1')
& q74('fmb_$i_2') ) ).
tff(declare_redbordeaux,type,
redbordeaux: $i > $o ).
tff(predicate_redbordeaux,axiom,
( redbordeaux('fmb_$i_1')
& ~ redbordeaux('fmb_$i_2') ) ).
tff(declare_dryredwine,type,
dryredwine: $i > $o ).
tff(predicate_dryredwine,axiom,
( dryredwine('fmb_$i_1')
& ~ dryredwine('fmb_$i_2') ) ).
tff(declare_drywhitewine,type,
drywhitewine: $i > $o ).
tff(predicate_drywhitewine,axiom,
( drywhitewine('fmb_$i_1')
& ~ drywhitewine('fmb_$i_2') ) ).
tff(declare_grape,type,
grape: $i > $o ).
tff(predicate_grape,axiom,
( grape('fmb_$i_1')
& grape('fmb_$i_2') ) ).
tff(declare_whiteloire,type,
whiteloire: $i > $o ).
tff(predicate_whiteloire,axiom,
( whiteloire('fmb_$i_1')
& ~ whiteloire('fmb_$i_2') ) ).
tff(declare_potableliquid,type,
potableliquid: $i > $o ).
tff(predicate_potableliquid,axiom,
( potableliquid('fmb_$i_1')
& potableliquid('fmb_$i_2') ) ).
tff(declare_vintage,type,
vintage: $i > $o ).
tff(predicate_vintage,axiom,
( vintage('fmb_$i_1')
& ~ vintage('fmb_$i_2') ) ).
tff(declare_haswinedescriptor,type,
haswinedescriptor: ( $i * $i ) > $o ).
tff(predicate_haswinedescriptor,axiom,
( haswinedescriptor('fmb_$i_1','fmb_$i_1')
& haswinedescriptor('fmb_$i_1','fmb_$i_2')
& ~ haswinedescriptor('fmb_$i_2','fmb_$i_1')
& ~ haswinedescriptor('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_winedescriptor,type,
winedescriptor: $i > $o ).
tff(predicate_winedescriptor,axiom,
( winedescriptor('fmb_$i_1')
& winedescriptor('fmb_$i_2') ) ).
tff(declare_winetaste,type,
winetaste: $i > $o ).
tff(predicate_winetaste,axiom,
( winetaste('fmb_$i_1')
& winetaste('fmb_$i_2') ) ).
tff(declare_produceswine,type,
produceswine: ( $i * $i ) > $o ).
tff(predicate_produceswine,axiom,
( produceswine('fmb_$i_1','fmb_$i_1')
& produceswine('fmb_$i_1','fmb_$i_2')
& ~ produceswine('fmb_$i_2','fmb_$i_1')
& ~ produceswine('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_madefromfruit,type,
madefromfruit: ( $i * $i ) > $o ).
tff(predicate_madefromfruit,axiom,
( madefromfruit('fmb_$i_1','fmb_$i_1')
& madefromfruit('fmb_$i_1','fmb_$i_2')
& madefromfruit('fmb_$i_2','fmb_$i_1')
& madefromfruit('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_madeintowine,type,
madeintowine: ( $i * $i ) > $o ).
tff(predicate_madeintowine,axiom,
( madeintowine('fmb_$i_1','fmb_$i_1')
& ~ madeintowine('fmb_$i_1','fmb_$i_2')
& ~ madeintowine('fmb_$i_2','fmb_$i_1')
& ~ madeintowine('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_kaon2hu,type,
kaon2hu: $i > $o ).
tff(predicate_kaon2hu,axiom,
( kaon2hu('fmb_$i_1')
& kaon2hu('fmb_$i_2') ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRD002+1 : TPTP v9.3.1. Released v6.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.36 % Computer : n006.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 22:15:40 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.14/0.40 Running first-order model finding
% 0.14/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.39/0.51 % (3378929)Will run a generic schedule for satisfiability detection.
% 0.39/0.51 % (3378938)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2961482891:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.39/0.51 % (3378935)% WARNING: option uhcvi not known.
% 0.39/0.51 % (3378934)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2716510802_2999 on theBenchmark for (2999ds/0Mi)
% 0.39/0.51 % (3378936)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=461426908:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.39/0.51 % (3378937)dis+10_1_sil=32000:sp=arity:random_seed=2808959061:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.39/0.51 % (3378939)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=744993741:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.39/0.51 % (3378940)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3039447229:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.39/0.51 % (3378935)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2796779500:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.39/0.51 % (3378938)Instruction limit reached!
% 0.39/0.51 % (3378938)------------------------------
% 0.39/0.51 % (3378938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.39/0.51 % (3378938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.39/0.51 % (3378938)CaDiCaL version: 2.1.3
% 0.39/0.51 % (3378938)Termination reason: Instruction limit
% 0.39/0.51 % (3378938)Termination phase: Saturation
% 0.39/0.51 % (3378938)Time elapsed: 0.034 s
% 0.39/0.51 % (3378938)Peak memory usage: 15 MB
% 0.39/0.51 % (3378938)Instructions burned: 120 (million)
% 0.39/0.51 % Detected minimum model sizes of [1]
% 0.39/0.51 % Detected maximum model sizes of [161]
% 0.39/0.51 % TRYING [1]
% 0.39/0.51 % TRYING [2]
% 0.39/0.51 % Finite Model Found!
% 0.39/0.51 % SZS status CounterSatisfiable for theBenchmark
% 0.39/0.51 % (3378934) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3378929-3378934"...
% 0.39/0.51 % (3378934)...printing done.
% 0.39/0.51 % SZS output start FiniteModel for theBenchmark
% See solution above
% 0.39/0.53 % (3378934)------------------------------
% 0.39/0.53 % (3378934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.39/0.53 % (3378934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.39/0.53 % (3378934)CaDiCaL version: 2.1.3
% 0.39/0.53 % (3378934)Termination reason: Satisfiable
% 0.39/0.53 % (3378934)Time elapsed: 0.042 s
% 0.39/0.53 % (3378934)Peak memory usage: 15 MB
% 0.39/0.53 % (3378934)Instructions burned: 89 (million)
% 0.39/0.53 % (3378929)Success in time 0.106 s
% 0.39/0.53 % Vampire exiting
%------------------------------------------------------------------------------