%------------------------------------------------------------------------------
% File : iProver-SAT---3.9.4
% Problem : PRD002+1 : TPTP v9.3.1. Released v6.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p SAT
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:31:18 PM UTC 2026
% Result : CounterSatisfiable 2.36s 6.97s
% Output : Model 8.51s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
%------ Positive definition of hasbody_aux
fof(lit_def,axiom,
! [X0,X1] :
( hasbody_aux(X0,X1)
<=> ( X1 = iProver_Domain_i_1
& X0 = iProver_Domain_i_1 ) ) ).
%------ Positive definition of hascolor_aux
fof(lit_def_001,axiom,
! [X0,X1] :
( hascolor_aux(X0,X1)
<=> ( X1 = iProver_Domain_i_1
& X0 = iProver_Domain_i_1 ) ) ).
%------ Positive definition of hasflavor_aux
fof(lit_def_002,axiom,
! [X0,X1] :
( hasflavor_aux(X0,X1)
<=> ( X1 = iProver_Domain_i_1
& X0 = iProver_Domain_i_1 ) ) ).
%------ Positive definition of hasmaker_aux
fof(lit_def_003,axiom,
! [X0,X1] :
( hasmaker_aux(X0,X1)
<=> ( X1 = iProver_Domain_i_1
& X0 = iProver_Domain_i_1 ) ) ).
%------ Positive definition of hassugar_aux
fof(lit_def_004,axiom,
! [X0,X1] :
( hassugar_aux(X0,X1)
<=> ( X1 = iProver_Domain_i_1
& X0 = iProver_Domain_i_1 ) ) ).
%------ Positive definition of locatedin_aux
fof(lit_def_005,axiom,
! [X0,X1] :
( locatedin_aux(X0,X1)
<=> ( ( X0 != iProver_Domain_i_1
& X1 = iProver_Domain_i_1 )
| ( X1 = iProver_Domain_i_1
& X0 = iProver_Domain_i_1 )
| ( X1 != iProver_Domain_i_1
& X0 != iProver_Domain_i_1 ) ) ) ).
%------ Positive definition of madefromgrape_aux
fof(lit_def_006,axiom,
! [X0,X1] :
( madefromgrape_aux(X0,X1)
<=> ( X1 = iProver_Domain_i_1
& X0 = iProver_Domain_i_1 ) ) ).
%------ Positive definition of ot____nom1_aux
fof(lit_def_007,axiom,
! [X0] :
( ot____nom1_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom10_aux
fof(lit_def_008,axiom,
! [X0] :
( ot____nom10_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom11_aux
fof(lit_def_009,axiom,
! [X0] :
( ot____nom11_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom12_aux
fof(lit_def_010,axiom,
! [X0] :
( ot____nom12_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom13_aux
fof(lit_def_011,axiom,
! [X0] :
( ot____nom13_aux(X0)
<=> ( X0 = iProver_Domain_i_1
| X0 != iProver_Domain_i_1 ) ) ).
%------ Positive definition of ot____nom14_aux
fof(lit_def_012,axiom,
! [X0] :
( ot____nom14_aux(X0)
<=> ( X0 = iProver_Domain_i_1
| X0 != iProver_Domain_i_1 ) ) ).
%------ Positive definition of ot____nom15_aux
fof(lit_def_013,axiom,
! [X0] :
( ot____nom15_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom16_aux
fof(lit_def_014,axiom,
! [X0] :
( ot____nom16_aux(X0)
<=> ( X0 = iProver_Domain_i_1
| X0 != iProver_Domain_i_1 ) ) ).
%------ Positive definition of ot____nom17_aux
fof(lit_def_015,axiom,
! [X0] :
( ot____nom17_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom18_aux
fof(lit_def_016,axiom,
! [X0] :
( ot____nom18_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom19_aux
fof(lit_def_017,axiom,
! [X0] :
( ot____nom19_aux(X0)
<=> ( X0 = iProver_Domain_i_1
| X0 != iProver_Domain_i_1 ) ) ).
%------ Positive definition of ot____nom2_aux
fof(lit_def_018,axiom,
! [X0] :
( ot____nom2_aux(X0)
<=> ( X0 = iProver_Domain_i_1
| X0 != iProver_Domain_i_1 ) ) ).
%------ Positive definition of ot____nom20_aux
fof(lit_def_019,axiom,
! [X0] :
( ot____nom20_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom21_aux
fof(lit_def_020,axiom,
! [X0] :
( ot____nom21_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom22_aux
fof(lit_def_021,axiom,
! [X0] :
( ot____nom22_aux(X0)
<=> ( X0 = iProver_Domain_i_1
| X0 != iProver_Domain_i_1 ) ) ).
%------ Positive definition of ot____nom23_aux
fof(lit_def_022,axiom,
! [X0] :
( ot____nom23_aux(X0)
<=> ( X0 = iProver_Domain_i_1
| X0 != iProver_Domain_i_1 ) ) ).
%------ Positive definition of ot____nom24_aux
fof(lit_def_023,axiom,
! [X0] :
( ot____nom24_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom25_aux
fof(lit_def_024,axiom,
! [X0] :
( ot____nom25_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom26_aux
fof(lit_def_025,axiom,
! [X0] :
( ot____nom26_aux(X0)
<=> ( X0 = iProver_Domain_i_1
| X0 != iProver_Domain_i_1 ) ) ).
%------ Positive definition of ot____nom27_aux
fof(lit_def_026,axiom,
! [X0] :
( ot____nom27_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom28_aux
fof(lit_def_027,axiom,
! [X0] :
( ot____nom28_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom29_aux
fof(lit_def_028,axiom,
! [X0] :
( ot____nom29_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom3_aux
fof(lit_def_029,axiom,
! [X0] :
( ot____nom3_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom30_aux
fof(lit_def_030,axiom,
! [X0] :
( ot____nom30_aux(X0)
<=> ( X0 = iProver_Domain_i_1
| X0 != iProver_Domain_i_1 ) ) ).
%------ Positive definition of ot____nom31_aux
fof(lit_def_031,axiom,
! [X0] :
( ot____nom31_aux(X0)
<=> ( X0 = iProver_Domain_i_1
| X0 != iProver_Domain_i_1 ) ) ).
%------ Positive definition of ot____nom32_aux
fof(lit_def_032,axiom,
! [X0] :
( ot____nom32_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom33_aux
fof(lit_def_033,axiom,
! [X0] :
( ot____nom33_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom34_aux
fof(lit_def_034,axiom,
! [X0] :
( ot____nom34_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom35_aux
fof(lit_def_035,axiom,
! [X0] :
( ot____nom35_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom36_aux
fof(lit_def_036,axiom,
! [X0] :
( ot____nom36_aux(X0)
<=> ( X0 = iProver_Domain_i_1
| X0 != iProver_Domain_i_1 ) ) ).
%------ Positive definition of ot____nom37_aux
fof(lit_def_037,axiom,
! [X0] :
( ot____nom37_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom38_aux
fof(lit_def_038,axiom,
! [X0] :
( ot____nom38_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom39_aux
fof(lit_def_039,axiom,
! [X0] :
( ot____nom39_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom4_aux
fof(lit_def_040,axiom,
! [X0] :
( ot____nom4_aux(X0)
<=> X0 != iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom40_aux
fof(lit_def_041,axiom,
! [X0] :
( ot____nom40_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom41_aux
fof(lit_def_042,axiom,
! [X0] :
( ot____nom41_aux(X0)
<=> X0 != iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom42_aux
fof(lit_def_043,axiom,
! [X0] :
( ot____nom42_aux(X0)
<=> ( X0 = iProver_Domain_i_1
| X0 != iProver_Domain_i_1 ) ) ).
%------ Positive definition of ot____nom43_aux
fof(lit_def_044,axiom,
! [X0] :
( ot____nom43_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom44_aux
fof(lit_def_045,axiom,
! [X0] :
( ot____nom44_aux(X0)
<=> ( X0 = iProver_Domain_i_1
| X0 != iProver_Domain_i_1 ) ) ).
%------ Positive definition of ot____nom45_aux
fof(lit_def_046,axiom,
! [X0] :
( ot____nom45_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom46_aux
fof(lit_def_047,axiom,
! [X0] :
( ot____nom46_aux(X0)
<=> ( X0 = iProver_Domain_i_1
| X0 != iProver_Domain_i_1 ) ) ).
%------ Positive definition of ot____nom47_aux
fof(lit_def_048,axiom,
! [X0] :
( ot____nom47_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom48_aux
fof(lit_def_049,axiom,
! [X0] :
( ot____nom48_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom49_aux
fof(lit_def_050,axiom,
! [X0] :
( ot____nom49_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom5_aux
fof(lit_def_051,axiom,
! [X0] :
( ot____nom5_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom50_aux
fof(lit_def_052,axiom,
! [X0] :
( ot____nom50_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom51_aux
fof(lit_def_053,axiom,
! [X0] :
( ot____nom51_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom52_aux
fof(lit_def_054,axiom,
! [X0] :
( ot____nom52_aux(X0)
<=> ( X0 = iProver_Domain_i_1
| X0 != iProver_Domain_i_1 ) ) ).
%------ Positive definition of ot____nom53_aux
fof(lit_def_055,axiom,
! [X0] :
( ot____nom53_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom54_aux
fof(lit_def_056,axiom,
! [X0] :
( ot____nom54_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom55_aux
fof(lit_def_057,axiom,
! [X0] :
( ot____nom55_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom56_aux
fof(lit_def_058,axiom,
! [X0] :
( ot____nom56_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom57_aux
fof(lit_def_059,axiom,
! [X0] :
( ot____nom57_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom58_aux
fof(lit_def_060,axiom,
! [X0] :
( ot____nom58_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom59_aux
fof(lit_def_061,axiom,
! [X0] :
( ot____nom59_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom6_aux
fof(lit_def_062,axiom,
! [X0] :
( ot____nom6_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom60_aux
fof(lit_def_063,axiom,
! [X0] :
( ot____nom60_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom61_aux
fof(lit_def_064,axiom,
! [X0] :
( ot____nom61_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom62_aux
fof(lit_def_065,axiom,
! [X0] :
( ot____nom62_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom63_aux
fof(lit_def_066,axiom,
! [X0] :
( ot____nom63_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom64_aux
fof(lit_def_067,axiom,
! [X0] :
( ot____nom64_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom7_aux
fof(lit_def_068,axiom,
! [X0] :
( ot____nom7_aux(X0)
<=> $true ) ).
%------ Positive definition of ot____nom8_aux
fof(lit_def_069,axiom,
! [X0] :
( ot____nom8_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom9_aux
fof(lit_def_070,axiom,
! [X0] :
( ot____nom9_aux(X0)
<=> $true ) ).
%------ Positive definition of wineflavor_aux
fof(lit_def_071,axiom,
! [X0] :
( wineflavor_aux(X0)
<=> $true ) ).
%------ Positive definition of winegrape_aux
fof(lit_def_072,axiom,
! [X0] :
( winegrape_aux(X0)
<=> $true ) ).
%------ Positive definition of winesugar_aux
fof(lit_def_073,axiom,
! [X0] :
( winesugar_aux(X0)
<=> $true ) ).
%------ Positive definition of winery_aux
fof(lit_def_074,axiom,
! [X0] :
( winery_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of zinfandel_aux
fof(lit_def_075,axiom,
! [X0] :
( zinfandel_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of winebody_aux
fof(lit_def_076,axiom,
! [X0] :
( winebody_aux(X0)
<=> $true ) ).
%------ Positive definition of winecolor_aux
fof(lit_def_077,axiom,
! [X0] :
( winecolor_aux(X0)
<=> $true ) ).
%------ Positive definition of whiteburgundy_aux
fof(lit_def_078,axiom,
! [X0] :
( whiteburgundy_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of whitewine_aux
fof(lit_def_079,axiom,
! [X0] :
( whitewine_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of muscadet_aux
fof(lit_def_080,axiom,
! [X0] :
( muscadet_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of meursault_aux
fof(lit_def_081,axiom,
! [X0] :
( meursault_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of meritage_aux
fof(lit_def_082,axiom,
! [X0] :
( meritage_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of margaux_aux
fof(lit_def_083,axiom,
! [X0] :
( margaux_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of icewine_aux
fof(lit_def_084,axiom,
! [X0] :
( icewine_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of dryriesling_aux
fof(lit_def_085,axiom,
! [X0] :
( dryriesling_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of dessertwine_aux
fof(lit_def_086,axiom,
! [X0] :
( dessertwine_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of cabernetsauvignon_aux
fof(lit_def_087,axiom,
! [X0] :
( cabernetsauvignon_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of cabernetfranc_aux
fof(lit_def_088,axiom,
! [X0] :
( cabernetfranc_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of beaujolais_aux
fof(lit_def_089,axiom,
! [X0] :
( beaujolais_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of anjou_aux
fof(lit_def_090,axiom,
! [X0] :
( anjou_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of chardonnay_aux
fof(lit_def_091,axiom,
! [X0] :
( chardonnay_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of cheninblanc_aux
fof(lit_def_092,axiom,
! [X0] :
( cheninblanc_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of chianti_aux
fof(lit_def_093,axiom,
! [X0] :
( chianti_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of cotesdor_aux
fof(lit_def_094,axiom,
! [X0] :
( cotesdor_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of merlot_aux
fof(lit_def_095,axiom,
! [X0] :
( merlot_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of pauillac_aux
fof(lit_def_096,axiom,
! [X0] :
( pauillac_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of petitesyrah_aux
fof(lit_def_097,axiom,
! [X0] :
( petitesyrah_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of pinotnoir_aux
fof(lit_def_098,axiom,
! [X0] :
( pinotnoir_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of port_aux
fof(lit_def_099,axiom,
! [X0] :
( port_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of redtablewine_aux
fof(lit_def_100,axiom,
! [X0] :
( redtablewine_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of region_aux
fof(lit_def_101,axiom,
! [X0] :
( region_aux(X0)
<=> $true ) ).
%------ Positive definition of riesling_aux
fof(lit_def_102,axiom,
! [X0] :
( riesling_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of sancerre_aux
fof(lit_def_103,axiom,
! [X0] :
( sancerre_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of sauternes_aux
fof(lit_def_104,axiom,
! [X0] :
( sauternes_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of sauvignonblanc_aux
fof(lit_def_105,axiom,
! [X0] :
( sauvignonblanc_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of semillon_aux
fof(lit_def_106,axiom,
! [X0] :
( semillon_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of stemilion_aux
fof(lit_def_107,axiom,
! [X0] :
( stemilion_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of sweetriesling_aux
fof(lit_def_108,axiom,
! [X0] :
( sweetriesling_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of kaon2namedobjects
fof(lit_def_109,axiom,
! [X0] :
( kaon2namedobjects(X0)
<=> $true ) ).
%------ Positive definition of vintageyear_aux
fof(lit_def_110,axiom,
! [X0] :
( vintageyear_aux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of hasvintageyear_aux
fof(lit_def_111,axiom,
! [X0,X1] :
( hasvintageyear_aux(X0,X1)
<=> ( X1 = iProver_Domain_i_1
& X0 = iProver_Domain_i_1 ) ) ).
%------ Positive definition of madefromgrape
fof(lit_def_112,axiom,
! [X0,X1] :
( madefromgrape(X0,X1)
<=> ( X1 = iProver_Domain_i_1
& X0 = iProver_Domain_i_1 ) ) ).
%------ Positive definition of locatedin
fof(lit_def_113,axiom,
! [X0,X1] :
( locatedin(X0,X1)
<=> ( ( X0 != iProver_Domain_i_1
& X1 = X0 )
| ( X1 = iProver_Domain_i_1
& X0 = iProver_Domain_i_1 )
| X0 != iProver_Domain_i_1 ) ) ).
%------ Positive definition of hassugar
fof(lit_def_114,axiom,
! [X0,X1] :
( hassugar(X0,X1)
<=> ( X1 = iProver_Domain_i_1
& X0 = iProver_Domain_i_1 ) ) ).
%------ Positive definition of hasmaker
fof(lit_def_115,axiom,
! [X0,X1] :
( hasmaker(X0,X1)
<=> ( ( X0 != iProver_Domain_i_1
& X1 = X0 )
| ( X1 = iProver_Domain_i_1
& X0 = iProver_Domain_i_1 )
| ( X1 != iProver_Domain_i_1
& X0 != iProver_Domain_i_1 ) ) ) ).
%------ Positive definition of hasflavor
fof(lit_def_116,axiom,
! [X0,X1] :
( hasflavor(X0,X1)
<=> ( X1 = iProver_Domain_i_1
& X0 = iProver_Domain_i_1 ) ) ).
%------ Positive definition of hascolor
fof(lit_def_117,axiom,
! [X0,X1] :
( hascolor(X0,X1)
<=> ( X1 = iProver_Domain_i_1
& X0 = iProver_Domain_i_1 ) ) ).
%------ Positive definition of hasbody
fof(lit_def_118,axiom,
! [X0,X1] :
( hasbody(X0,X1)
<=> ( X1 = iProver_Domain_i_1
& X0 = iProver_Domain_i_1 ) ) ).
%------ Positive definition of adjacentregion
fof(lit_def_119,axiom,
! [X0,X1] :
( adjacentregion(X0,X1)
<=> $false ) ).
%------ Positive definition of adjacentregion_aux
fof(lit_def_120,axiom,
! [X0,X1] :
( adjacentregion_aux(X0,X1)
<=> $false ) ).
%------ Positive definition of hasvintageyear
fof(lit_def_121,axiom,
! [X0,X1] :
( hasvintageyear(X0,X1)
<=> ( ( X0 != iProver_Domain_i_1
& X1 = X0 )
| ( X1 = iProver_Domain_i_1
& X0 = iProver_Domain_i_1 )
| ( X1 != iProver_Domain_i_1
& X0 != iProver_Domain_i_1 ) ) ) ).
%------ Positive definition of ot____nom1
fof(lit_def_122,axiom,
! [X0] :
( ot____nom1(X0)
<=> $true ) ).
%------ Positive definition of ot____nom10
fof(lit_def_123,axiom,
! [X0] :
( ot____nom10(X0)
<=> $true ) ).
%------ Positive definition of ot____nom11
fof(lit_def_124,axiom,
! [X0] :
( ot____nom11(X0)
<=> $true ) ).
%------ Positive definition of ot____nom12
fof(lit_def_125,axiom,
! [X0] :
( ot____nom12(X0)
<=> $true ) ).
%------ Positive definition of ot____nom13
fof(lit_def_126,axiom,
! [X0] :
( ot____nom13(X0)
<=> $true ) ).
%------ Positive definition of ot____nom14
fof(lit_def_127,axiom,
! [X0] :
( ot____nom14(X0)
<=> $true ) ).
%------ Positive definition of ot____nom15
fof(lit_def_128,axiom,
! [X0] :
( ot____nom15(X0)
<=> $true ) ).
%------ Positive definition of ot____nom16
fof(lit_def_129,axiom,
! [X0] :
( ot____nom16(X0)
<=> $true ) ).
%------ Positive definition of ot____nom17
fof(lit_def_130,axiom,
! [X0] :
( ot____nom17(X0)
<=> $true ) ).
%------ Positive definition of ot____nom18
fof(lit_def_131,axiom,
! [X0] :
( ot____nom18(X0)
<=> $true ) ).
%------ Positive definition of ot____nom19
fof(lit_def_132,axiom,
! [X0] :
( ot____nom19(X0)
<=> $true ) ).
%------ Positive definition of ot____nom2
fof(lit_def_133,axiom,
! [X0] :
( ot____nom2(X0)
<=> $true ) ).
%------ Positive definition of ot____nom20
fof(lit_def_134,axiom,
! [X0] :
( ot____nom20(X0)
<=> $true ) ).
%------ Positive definition of ot____nom21
fof(lit_def_135,axiom,
! [X0] :
( ot____nom21(X0)
<=> $true ) ).
%------ Positive definition of ot____nom22
fof(lit_def_136,axiom,
! [X0] :
( ot____nom22(X0)
<=> $true ) ).
%------ Positive definition of ot____nom23
fof(lit_def_137,axiom,
! [X0] :
( ot____nom23(X0)
<=> $true ) ).
%------ Positive definition of ot____nom24
fof(lit_def_138,axiom,
! [X0] :
( ot____nom24(X0)
<=> $true ) ).
%------ Positive definition of ot____nom25
fof(lit_def_139,axiom,
! [X0] :
( ot____nom25(X0)
<=> $true ) ).
%------ Positive definition of ot____nom26
fof(lit_def_140,axiom,
! [X0] :
( ot____nom26(X0)
<=> $true ) ).
%------ Positive definition of ot____nom27
fof(lit_def_141,axiom,
! [X0] :
( ot____nom27(X0)
<=> $true ) ).
%------ Positive definition of ot____nom28
fof(lit_def_142,axiom,
! [X0] :
( ot____nom28(X0)
<=> $true ) ).
%------ Positive definition of ot____nom29
fof(lit_def_143,axiom,
! [X0] :
( ot____nom29(X0)
<=> $true ) ).
%------ Positive definition of ot____nom3
fof(lit_def_144,axiom,
! [X0] :
( ot____nom3(X0)
<=> $true ) ).
%------ Positive definition of ot____nom30
fof(lit_def_145,axiom,
! [X0] :
( ot____nom30(X0)
<=> $true ) ).
%------ Positive definition of ot____nom31
fof(lit_def_146,axiom,
! [X0] :
( ot____nom31(X0)
<=> $true ) ).
%------ Positive definition of ot____nom32
fof(lit_def_147,axiom,
! [X0] :
( ot____nom32(X0)
<=> $true ) ).
%------ Positive definition of ot____nom33
fof(lit_def_148,axiom,
! [X0] :
( ot____nom33(X0)
<=> $true ) ).
%------ Positive definition of ot____nom34
fof(lit_def_149,axiom,
! [X0] :
( ot____nom34(X0)
<=> $true ) ).
%------ Positive definition of ot____nom35
fof(lit_def_150,axiom,
! [X0] :
( ot____nom35(X0)
<=> $true ) ).
%------ Positive definition of ot____nom36
fof(lit_def_151,axiom,
! [X0] :
( ot____nom36(X0)
<=> $true ) ).
%------ Positive definition of ot____nom37
fof(lit_def_152,axiom,
! [X0] :
( ot____nom37(X0)
<=> $true ) ).
%------ Positive definition of ot____nom38
fof(lit_def_153,axiom,
! [X0] :
( ot____nom38(X0)
<=> $true ) ).
%------ Positive definition of ot____nom39
fof(lit_def_154,axiom,
! [X0] :
( ot____nom39(X0)
<=> $true ) ).
%------ Positive definition of ot____nom4
fof(lit_def_155,axiom,
! [X0] :
( ot____nom4(X0)
<=> X0 != iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom40
fof(lit_def_156,axiom,
! [X0] :
( ot____nom40(X0)
<=> $true ) ).
%------ Positive definition of ot____nom41
fof(lit_def_157,axiom,
! [X0] :
( ot____nom41(X0)
<=> X0 != iProver_Domain_i_1 ) ).
%------ Positive definition of ot____nom42
fof(lit_def_158,axiom,
! [X0] :
( ot____nom42(X0)
<=> $true ) ).
%------ Positive definition of ot____nom43
fof(lit_def_159,axiom,
! [X0] :
( ot____nom43(X0)
<=> $true ) ).
%------ Positive definition of ot____nom44
fof(lit_def_160,axiom,
! [X0] :
( ot____nom44(X0)
<=> $true ) ).
%------ Positive definition of ot____nom45
fof(lit_def_161,axiom,
! [X0] :
( ot____nom45(X0)
<=> $true ) ).
%------ Positive definition of ot____nom46
fof(lit_def_162,axiom,
! [X0] :
( ot____nom46(X0)
<=> $true ) ).
%------ Positive definition of ot____nom47
fof(lit_def_163,axiom,
! [X0] :
( ot____nom47(X0)
<=> $true ) ).
%------ Positive definition of ot____nom48
fof(lit_def_164,axiom,
! [X0] :
( ot____nom48(X0)
<=> $true ) ).
%------ Positive definition of ot____nom49
fof(lit_def_165,axiom,
! [X0] :
( ot____nom49(X0)
<=> $true ) ).
%------ Positive definition of ot____nom5
fof(lit_def_166,axiom,
! [X0] :
( ot____nom5(X0)
<=> $true ) ).
%------ Positive definition of ot____nom50
fof(lit_def_167,axiom,
! [X0] :
( ot____nom50(X0)
<=> $true ) ).
%------ Positive definition of ot____nom51
fof(lit_def_168,axiom,
! [X0] :
( ot____nom51(X0)
<=> $true ) ).
%------ Positive definition of ot____nom52
fof(lit_def_169,axiom,
! [X0] :
( ot____nom52(X0)
<=> $true ) ).
%------ Positive definition of ot____nom53
fof(lit_def_170,axiom,
! [X0] :
( ot____nom53(X0)
<=> $true ) ).
%------ Positive definition of ot____nom54
fof(lit_def_171,axiom,
! [X0] :
( ot____nom54(X0)
<=> $true ) ).
%------ Positive definition of ot____nom55
fof(lit_def_172,axiom,
! [X0] :
( ot____nom55(X0)
<=> $true ) ).
%------ Positive definition of ot____nom56
fof(lit_def_173,axiom,
! [X0] :
( ot____nom56(X0)
<=> $true ) ).
%------ Positive definition of ot____nom57
fof(lit_def_174,axiom,
! [X0] :
( ot____nom57(X0)
<=> $true ) ).
%------ Positive definition of ot____nom58
fof(lit_def_175,axiom,
! [X0] :
( ot____nom58(X0)
<=> $true ) ).
%------ Positive definition of ot____nom59
fof(lit_def_176,axiom,
! [X0] :
( ot____nom59(X0)
<=> $true ) ).
%------ Positive definition of ot____nom6
fof(lit_def_177,axiom,
! [X0] :
( ot____nom6(X0)
<=> $true ) ).
%------ Positive definition of ot____nom60
fof(lit_def_178,axiom,
! [X0] :
( ot____nom60(X0)
<=> $true ) ).
%------ Positive definition of ot____nom61
fof(lit_def_179,axiom,
! [X0] :
( ot____nom61(X0)
<=> $true ) ).
%------ Positive definition of ot____nom62
fof(lit_def_180,axiom,
! [X0] :
( ot____nom62(X0)
<=> $true ) ).
%------ Positive definition of ot____nom63
fof(lit_def_181,axiom,
! [X0] :
( ot____nom63(X0)
<=> $true ) ).
%------ Positive definition of ot____nom64
fof(lit_def_182,axiom,
! [X0] :
( ot____nom64(X0)
<=> $true ) ).
%------ Positive definition of ot____nom7
fof(lit_def_183,axiom,
! [X0] :
( ot____nom7(X0)
<=> $true ) ).
%------ Positive definition of ot____nom8
fof(lit_def_184,axiom,
! [X0] :
( ot____nom8(X0)
<=> $true ) ).
%------ Positive definition of ot____nom9
fof(lit_def_185,axiom,
! [X0] :
( ot____nom9(X0)
<=> $true ) ).
%------ Positive definition of zinfandel
fof(lit_def_186,axiom,
! [X0] :
( zinfandel(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of winery
fof(lit_def_187,axiom,
! [X0] :
( winery(X0)
<=> $true ) ).
%------ Positive definition of winegrape
fof(lit_def_188,axiom,
! [X0] :
( winegrape(X0)
<=> $true ) ).
%------ Positive definition of winesugar
fof(lit_def_189,axiom,
! [X0] :
( winesugar(X0)
<=> $true ) ).
%------ Positive definition of wineflavor
fof(lit_def_190,axiom,
! [X0] :
( wineflavor(X0)
<=> $true ) ).
%------ Positive definition of anjou
fof(lit_def_191,axiom,
! [X0] :
( anjou(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of beaujolais
fof(lit_def_192,axiom,
! [X0] :
( beaujolais(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of cabernetfranc
fof(lit_def_193,axiom,
! [X0] :
( cabernetfranc(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of cabernetsauvignon
fof(lit_def_194,axiom,
! [X0] :
( cabernetsauvignon(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of chardonnay
fof(lit_def_195,axiom,
! [X0] :
( chardonnay(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of cheninblanc
fof(lit_def_196,axiom,
! [X0] :
( cheninblanc(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of chianti
fof(lit_def_197,axiom,
! [X0] :
( chianti(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of cotesdor
fof(lit_def_198,axiom,
! [X0] :
( cotesdor(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of dessertwine
fof(lit_def_199,axiom,
! [X0] :
( dessertwine(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of dryriesling
fof(lit_def_200,axiom,
! [X0] :
( dryriesling(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of icewine
fof(lit_def_201,axiom,
! [X0] :
( icewine(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of margaux
fof(lit_def_202,axiom,
! [X0] :
( margaux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of meritage
fof(lit_def_203,axiom,
! [X0] :
( meritage(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of merlot
fof(lit_def_204,axiom,
! [X0] :
( merlot(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of meursault
fof(lit_def_205,axiom,
! [X0] :
( meursault(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of muscadet
fof(lit_def_206,axiom,
! [X0] :
( muscadet(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of pauillac
fof(lit_def_207,axiom,
! [X0] :
( pauillac(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of petitesyrah
fof(lit_def_208,axiom,
! [X0] :
( petitesyrah(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of pinotnoir
fof(lit_def_209,axiom,
! [X0] :
( pinotnoir(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of port
fof(lit_def_210,axiom,
! [X0] :
( port(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of redtablewine
fof(lit_def_211,axiom,
! [X0] :
( redtablewine(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of region
fof(lit_def_212,axiom,
! [X0] :
( region(X0)
<=> $true ) ).
%------ Positive definition of riesling
fof(lit_def_213,axiom,
! [X0] :
( riesling(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of sancerre
fof(lit_def_214,axiom,
! [X0] :
( sancerre(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of sauternes
fof(lit_def_215,axiom,
! [X0] :
( sauternes(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of sauvignonblanc
fof(lit_def_216,axiom,
! [X0] :
( sauvignonblanc(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of semillon
fof(lit_def_217,axiom,
! [X0] :
( semillon(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of stemilion
fof(lit_def_218,axiom,
! [X0] :
( stemilion(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of sweetriesling
fof(lit_def_219,axiom,
! [X0] :
( sweetriesling(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of vintageyear
fof(lit_def_220,axiom,
! [X0] :
( vintageyear(X0)
<=> $true ) ).
%------ Positive definition of whiteburgundy
fof(lit_def_221,axiom,
! [X0] :
( whiteburgundy(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of whitewine
fof(lit_def_222,axiom,
! [X0] :
( whitewine(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of winebody
fof(lit_def_223,axiom,
! [X0] :
( winebody(X0)
<=> $true ) ).
%------ Positive definition of winecolor
fof(lit_def_224,axiom,
! [X0] :
( winecolor(X0)
<=> $true ) ).
%------ Positive definition of q0
fof(lit_def_225,axiom,
! [X0] :
( q0(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of medoc
fof(lit_def_226,axiom,
! [X0] :
( medoc(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of redwine
fof(lit_def_227,axiom,
! [X0] :
( redwine(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of kaon2equal
fof(lit_def_228,axiom,
! [X0,X1] :
( kaon2equal(X0,X1)
<=> ( X1 = X0
| ( X1 = iProver_Domain_i_1
& X0 = iProver_Domain_i_1 )
| ( X1 != iProver_Domain_i_1
& X0 != iProver_Domain_i_1 ) ) ) ).
%------ Positive definition of q1
fof(lit_def_229,axiom,
! [X0] :
( q1(X0)
<=> $true ) ).
%------ Positive definition of bordeaux
fof(lit_def_230,axiom,
! [X0] :
( bordeaux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q2
fof(lit_def_231,axiom,
! [X0] :
( q2(X0)
<=> $true ) ).
%------ Positive definition of q10
fof(lit_def_232,axiom,
! [X0] :
( q10(X0)
<=> X0 != iProver_Domain_i_1 ) ).
%------ Positive definition of q9
fof(lit_def_233,axiom,
! [X0] :
( q9(X0)
<=> X0 != iProver_Domain_i_1 ) ).
%------ Positive definition of q11
fof(lit_def_234,axiom,
! [X0] :
( q11(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q12
fof(lit_def_235,axiom,
! [X0] :
( q12(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of whitetablewine
fof(lit_def_236,axiom,
! [X0] :
( whitetablewine(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of pinotblanc
fof(lit_def_237,axiom,
! [X0] :
( pinotblanc(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of semillonorsauvignonblanc
fof(lit_def_238,axiom,
! [X0] :
( semillonorsauvignonblanc(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q13
fof(lit_def_239,axiom,
! [X0] :
( q13(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q14
fof(lit_def_240,axiom,
! [X0] :
( q14(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of gamay
fof(lit_def_241,axiom,
! [X0] :
( gamay(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q15
fof(lit_def_242,axiom,
! [X0] :
( q15(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of rosewine
fof(lit_def_243,axiom,
! [X0] :
( rosewine(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q16
fof(lit_def_244,axiom,
! [X0] :
( q16(X0)
<=> $true ) ).
%------ Positive definition of q17
fof(lit_def_245,axiom,
! [X0] :
( q17(X0)
<=> $true ) ).
%------ Positive definition of q18
fof(lit_def_246,axiom,
! [X0] :
( q18(X0)
<=> $true ) ).
%------ Positive definition of q19
fof(lit_def_247,axiom,
! [X0] :
( q19(X0)
<=> $true ) ).
%------ Positive definition of q20
fof(lit_def_248,axiom,
! [X0] :
( q20(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q21
fof(lit_def_249,axiom,
! [X0] :
( q21(X0)
<=> $true ) ).
%------ Positive definition of q22
fof(lit_def_250,axiom,
! [X0] :
( q22(X0)
<=> $true ) ).
%------ Positive definition of q23
fof(lit_def_251,axiom,
! [X0] :
( q23(X0)
<=> $true ) ).
%------ Positive definition of q24
fof(lit_def_252,axiom,
! [X0] :
( q24(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q26
fof(lit_def_253,axiom,
! [X0] :
( q26(X0)
<=> $true ) ).
%------ Positive definition of americanwine
fof(lit_def_254,axiom,
! [X0] :
( americanwine(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q27
fof(lit_def_255,axiom,
! [X0] :
( q27(X0)
<=> $true ) ).
%------ Positive definition of q29
fof(lit_def_256,axiom,
! [X0] :
( q29(X0)
<=> $true ) ).
%------ Positive definition of burgundy
fof(lit_def_257,axiom,
! [X0] :
( burgundy(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q30
fof(lit_def_258,axiom,
! [X0] :
( q30(X0)
<=> $true ) ).
%------ Positive definition of q3
fof(lit_def_259,axiom,
! [X0] :
( q3(X0)
<=> $true ) ).
%------ Positive definition of tours
fof(lit_def_260,axiom,
! [X0] :
( tours(X0)
<=> $false ) ).
%------ Positive definition of redburgundy
fof(lit_def_261,axiom,
! [X0] :
( redburgundy(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of wine
fof(lit_def_262,axiom,
! [X0] :
( wine(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q31
fof(lit_def_263,axiom,
! [X0] :
( q31(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of tablewine
fof(lit_def_264,axiom,
! [X0] :
( tablewine(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of drywine
fof(lit_def_265,axiom,
! [X0] :
( drywine(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q32
fof(lit_def_266,axiom,
! [X0] :
( q32(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q33
fof(lit_def_267,axiom,
! [X0] :
( q33(X0)
<=> $true ) ).
%------ Positive definition of q34
fof(lit_def_268,axiom,
! [X0] :
( q34(X0)
<=> $true ) ).
%------ Positive definition of q35
fof(lit_def_269,axiom,
! [X0] :
( q35(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of fullbodiedwine
fof(lit_def_270,axiom,
! [X0] :
( fullbodiedwine(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q36
fof(lit_def_271,axiom,
! [X0] :
( q36(X0)
<=> $true ) ).
%------ Positive definition of whitenonsweetwine
fof(lit_def_272,axiom,
! [X0] :
( whitenonsweetwine(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of earlyharvest
fof(lit_def_273,axiom,
! [X0] :
( earlyharvest(X0)
<=> $false ) ).
%------ Positive definition of q37
fof(lit_def_274,axiom,
! [X0] :
( q37(X0)
<=> $true ) ).
%------ Positive definition of q38
fof(lit_def_275,axiom,
! [X0] :
( q38(X0)
<=> $true ) ).
%------ Positive definition of q39
fof(lit_def_276,axiom,
! [X0] :
( q39(X0)
<=> $true ) ).
%------ Positive definition of q40
fof(lit_def_277,axiom,
! [X0] :
( q40(X0)
<=> $true ) ).
%------ Positive definition of q4
fof(lit_def_278,axiom,
! [X0] :
( q4(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q41
fof(lit_def_279,axiom,
! [X0] :
( q41(X0)
<=> $true ) ).
%------ Positive definition of q42
fof(lit_def_280,axiom,
! [X0] :
( q42(X0)
<=> $true ) ).
%------ Positive definition of q43
fof(lit_def_281,axiom,
! [X0] :
( q43(X0)
<=> $true ) ).
%------ Positive definition of q44
fof(lit_def_282,axiom,
! [X0] :
( q44(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q45
fof(lit_def_283,axiom,
! [X0] :
( q45(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q46
fof(lit_def_284,axiom,
! [X0] :
( q46(X0)
<=> $true ) ).
%------ Positive definition of q47
fof(lit_def_285,axiom,
! [X0] :
( q47(X0)
<=> $true ) ).
%------ Positive definition of californiawine
fof(lit_def_286,axiom,
! [X0] :
( californiawine(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q48
fof(lit_def_287,axiom,
! [X0] :
( q48(X0)
<=> $true ) ).
%------ Positive definition of q49
fof(lit_def_288,axiom,
! [X0] :
( q49(X0)
<=> $true ) ).
%------ Positive definition of germanwine
fof(lit_def_289,axiom,
! [X0] :
( germanwine(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q50
fof(lit_def_290,axiom,
! [X0] :
( q50(X0)
<=> $true ) ).
%------ Positive definition of q5
fof(lit_def_291,axiom,
! [X0] :
( q5(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q6
fof(lit_def_292,axiom,
! [X0] :
( q6(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q72
fof(lit_def_293,axiom,
! [X0] :
( q72(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q69
fof(lit_def_294,axiom,
! [X0] :
( q69(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q63
fof(lit_def_295,axiom,
! [X0] :
( q63(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q51
fof(lit_def_296,axiom,
! [X0] :
( q51(X0)
<=> X0 != iProver_Domain_i_1 ) ).
%------ Positive definition of frenchwine
fof(lit_def_297,axiom,
! [X0] :
( frenchwine(X0)
<=> $false ) ).
%------ Positive definition of q52
fof(lit_def_298,axiom,
! [X0] :
( q52(X0)
<=> X0 != iProver_Domain_i_1 ) ).
%------ Positive definition of q55
fof(lit_def_299,axiom,
! [X0] :
( q55(X0)
<=> $true ) ).
%------ Positive definition of q56
fof(lit_def_300,axiom,
! [X0] :
( q56(X0)
<=> $true ) ).
%------ Positive definition of q57
fof(lit_def_301,axiom,
! [X0] :
( q57(X0)
<=> $true ) ).
%------ Positive definition of loire
fof(lit_def_302,axiom,
! [X0] :
( loire(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q58
fof(lit_def_303,axiom,
! [X0] :
( q58(X0)
<=> $true ) ).
%------ Positive definition of q59
fof(lit_def_304,axiom,
! [X0] :
( q59(X0)
<=> $true ) ).
%------ Positive definition of alsatianwine
fof(lit_def_305,axiom,
! [X0] :
( alsatianwine(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q60
fof(lit_def_306,axiom,
! [X0] :
( q60(X0)
<=> $true ) ).
%------ Positive definition of q61
fof(lit_def_307,axiom,
! [X0] :
( q61(X0)
<=> $true ) ).
%------ Positive definition of italianwine
fof(lit_def_308,axiom,
! [X0] :
( italianwine(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q62
fof(lit_def_309,axiom,
! [X0] :
( q62(X0)
<=> $true ) ).
%------ Positive definition of q64
fof(lit_def_310,axiom,
! [X0] :
( q64(X0)
<=> $true ) ).
%------ Positive definition of q65
fof(lit_def_311,axiom,
! [X0] :
( q65(X0)
<=> $true ) ).
%------ Positive definition of q66
fof(lit_def_312,axiom,
! [X0] :
( q66(X0)
<=> $true ) ).
%------ Positive definition of q67
fof(lit_def_313,axiom,
! [X0] :
( q67(X0)
<=> $true ) ).
%------ Positive definition of q68
fof(lit_def_314,axiom,
! [X0] :
( q68(X0)
<=> $true ) ).
%------ Positive definition of whitebordeaux
fof(lit_def_315,axiom,
! [X0] :
( whitebordeaux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q7
fof(lit_def_316,axiom,
! [X0] :
( q7(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q70
fof(lit_def_317,axiom,
! [X0] :
( q70(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of sweetwine
fof(lit_def_318,axiom,
! [X0] :
( sweetwine(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of lateharvest
fof(lit_def_319,axiom,
! [X0] :
( lateharvest(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q71
fof(lit_def_320,axiom,
! [X0] :
( q71(X0)
<=> $true ) ).
%------ Positive definition of q73
fof(lit_def_321,axiom,
! [X0] :
( q73(X0)
<=> ( X0 = iProver_Domain_i_1
| X0 != iProver_Domain_i_1 ) ) ).
%------ Positive definition of texaswine
fof(lit_def_322,axiom,
! [X0] :
( texaswine(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of q74
fof(lit_def_323,axiom,
! [X0] :
( q74(X0)
<=> ( X0 = iProver_Domain_i_1
| X0 != iProver_Domain_i_1 ) ) ).
%------ Positive definition of redbordeaux
fof(lit_def_324,axiom,
! [X0] :
( redbordeaux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of dryredwine
fof(lit_def_325,axiom,
! [X0] :
( dryredwine(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of drywhitewine
fof(lit_def_326,axiom,
! [X0] :
( drywhitewine(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of grape
fof(lit_def_327,axiom,
! [X0] :
( grape(X0)
<=> $true ) ).
%------ Positive definition of whiteloire
fof(lit_def_328,axiom,
! [X0] :
( whiteloire(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of potableliquid
fof(lit_def_329,axiom,
! [X0] :
( potableliquid(X0)
<=> $true ) ).
%------ Positive definition of vintage
fof(lit_def_330,axiom,
! [X0] :
( vintage(X0)
<=> $true ) ).
%------ Positive definition of haswinedescriptor
fof(lit_def_331,axiom,
! [X0,X1] :
( haswinedescriptor(X0,X1)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of winedescriptor
fof(lit_def_332,axiom,
! [X0] :
( winedescriptor(X0)
<=> $true ) ).
%------ Positive definition of winetaste
fof(lit_def_333,axiom,
! [X0] :
( winetaste(X0)
<=> $true ) ).
%------ Positive definition of produceswine
fof(lit_def_334,axiom,
! [X0,X1] :
( produceswine(X0,X1)
<=> ( ( X1 = iProver_Domain_i_1
& X0 = iProver_Domain_i_1 )
| ( X1 != iProver_Domain_i_1
& X0 != iProver_Domain_i_1 ) ) ) ).
%------ Positive definition of madefromfruit
fof(lit_def_335,axiom,
! [X0,X1] :
( madefromfruit(X0,X1)
<=> $true ) ).
%------ Positive definition of madeintowine
fof(lit_def_336,axiom,
! [X0,X1] :
( madeintowine(X0,X1)
<=> ( X1 = iProver_Domain_i_1
& X0 = iProver_Domain_i_1 ) ) ).
%------ Positive definition of kaon2hu
fof(lit_def_337,axiom,
! [X0] :
( kaon2hu(X0)
<=> $true ) ).
%------ Positive definition of iProver_Flat_pulignymontrachetwhiteburgundy
fof(lit_def_338,axiom,
! [X0] :
( iProver_Flat_pulignymontrachetwhiteburgundy(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_medium
fof(lit_def_339,axiom,
! [X0] :
( iProver_Flat_medium(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_formanchardonnay
fof(lit_def_340,axiom,
! [X0] :
( iProver_Flat_formanchardonnay(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_full
fof(lit_def_341,axiom,
! [X0] :
( iProver_Flat_full(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_foxencheninblanc
fof(lit_def_342,axiom,
! [X0] :
( iProver_Flat_foxencheninblanc(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_chianticlassico
fof(lit_def_343,axiom,
! [X0] :
( iProver_Flat_chianticlassico(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_cortonmontrachetwhiteburgundy
fof(lit_def_344,axiom,
! [X0] :
( iProver_Flat_cortonmontrachetwhiteburgundy(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_corbansprivatebinsauvignonblanc
fof(lit_def_345,axiom,
! [X0] :
( iProver_Flat_corbansprivatebinsauvignonblanc(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_congressspringssemillon
fof(lit_def_346,axiom,
! [X0] :
( iProver_Flat_congressspringssemillon(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_mariettapetitesyrah
fof(lit_def_347,axiom,
! [X0] :
( iProver_Flat_mariettapetitesyrah(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_corbanssauvignonblanc
fof(lit_def_348,axiom,
! [X0] :
( iProver_Flat_corbanssauvignonblanc(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_petermccoychardonnay
fof(lit_def_349,axiom,
! [X0] :
( iProver_Flat_petermccoychardonnay(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_selaksicewine
fof(lit_def_350,axiom,
! [X0] :
( iProver_Flat_selaksicewine(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_bancroftchardonnay
fof(lit_def_351,axiom,
! [X0] :
( iProver_Flat_bancroftchardonnay(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_elysezinfandel
fof(lit_def_352,axiom,
! [X0] :
( iProver_Flat_elysezinfandel(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_mountadampinotnoir
fof(lit_def_353,axiom,
! [X0] :
( iProver_Flat_mountadampinotnoir(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_mariettacabernetsauvignon
fof(lit_def_354,axiom,
! [X0] :
( iProver_Flat_mariettacabernetsauvignon(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_schlossrothermeltrochenbierenausleseriesling
fof(lit_def_355,axiom,
! [X0] :
( iProver_Flat_schlossrothermeltrochenbierenausleseriesling(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_garyfarrellmerlot
fof(lit_def_356,axiom,
! [X0] :
( iProver_Flat_garyfarrellmerlot(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_cotturizinfandel
fof(lit_def_357,axiom,
! [X0] :
( iProver_Flat_cotturizinfandel(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_mariettaoldvinesred
fof(lit_def_358,axiom,
! [X0] :
( iProver_Flat_mariettaoldvinesred(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_longridgemerlot
fof(lit_def_359,axiom,
! [X0] :
( iProver_Flat_longridgemerlot(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_light
fof(lit_def_360,axiom,
! [X0] :
( iProver_Flat_light(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_kalincellarssemillon
fof(lit_def_361,axiom,
! [X0] :
( iProver_Flat_kalincellarssemillon(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_pagemillwinerycabernetsauvignon
fof(lit_def_362,axiom,
! [X0] :
( iProver_Flat_pagemillwinerycabernetsauvignon(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_seanthackreysiriuspetitesyrah
fof(lit_def_363,axiom,
! [X0] :
( iProver_Flat_seanthackreysiriuspetitesyrah(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_saucelitocanyonzinfandel1998
fof(lit_def_364,axiom,
! [X0] :
( iProver_Flat_saucelitocanyonzinfandel1998(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_whitehalllaneprimavera
fof(lit_def_365,axiom,
! [X0] :
( iProver_Flat_whitehalllaneprimavera(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_santacruzmountainvineyardcabernetsauvignon
fof(lit_def_366,axiom,
! [X0] :
( iProver_Flat_santacruzmountainvineyardcabernetsauvignon(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_lanetannerpinotnoir
fof(lit_def_367,axiom,
! [X0] :
( iProver_Flat_lanetannerpinotnoir(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_corbansdrywhiteriesling
fof(lit_def_368,axiom,
! [X0] :
( iProver_Flat_corbansdrywhiteriesling(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_mountadamchardonnay
fof(lit_def_369,axiom,
! [X0] :
( iProver_Flat_mountadamchardonnay(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_mountadamriesling
fof(lit_def_370,axiom,
! [X0] :
( iProver_Flat_mountadamriesling(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_mariettazinfandel
fof(lit_def_371,axiom,
! [X0] :
( iProver_Flat_mariettazinfandel(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_kathrynkennedylateral
fof(lit_def_372,axiom,
! [X0] :
( iProver_Flat_kathrynkennedylateral(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_mountedenvineyardestatepinotnoir
fof(lit_def_373,axiom,
! [X0] :
( iProver_Flat_mountedenvineyardestatepinotnoir(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_whitehalllanecabernetfranc
fof(lit_def_374,axiom,
! [X0] :
( iProver_Flat_whitehalllanecabernetfranc(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_ventanacheninblanc
fof(lit_def_375,axiom,
! [X0] :
( iProver_Flat_ventanacheninblanc(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_saucelitocanyonzinfandel
fof(lit_def_376,axiom,
! [X0] :
( iProver_Flat_saucelitocanyonzinfandel(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_formancabernetsauvignon
fof(lit_def_377,axiom,
! [X0] :
( iProver_Flat_formancabernetsauvignon(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_schlossvolradtrochenbierenausleseriesling
fof(lit_def_378,axiom,
! [X0] :
( iProver_Flat_schlossvolradtrochenbierenausleseriesling(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_mountedenvineyardednavalleychardonnay
fof(lit_def_379,axiom,
! [X0] :
( iProver_Flat_mountedenvineyardednavalleychardonnay(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_stonleighsauvignonblanc
fof(lit_def_380,axiom,
! [X0] :
( iProver_Flat_stonleighsauvignonblanc(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_selakssauvignonblanc
fof(lit_def_381,axiom,
! [X0] :
( iProver_Flat_selakssauvignonblanc(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_white
fof(lit_def_382,axiom,
! [X0] :
( iProver_Flat_white(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_moderate
fof(lit_def_383,axiom,
! [X0] :
( iProver_Flat_moderate(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_stgenevievetexaswhite
fof(lit_def_384,axiom,
! [X0] :
( iProver_Flat_stgenevievetexaswhite(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_strong
fof(lit_def_385,axiom,
! [X0] :
( iProver_Flat_strong(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_chateaudychemsauterne
fof(lit_def_386,axiom,
! [X0] :
( iProver_Flat_chateaudychemsauterne(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_chateaudemeursaultmeursault
fof(lit_def_387,axiom,
! [X0] :
( iProver_Flat_chateaudemeursaultmeursault(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_delicate
fof(lit_def_388,axiom,
! [X0] :
( iProver_Flat_delicate(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_pulignymontrachet
fof(lit_def_389,axiom,
! [X0] :
( iProver_Flat_pulignymontrachet(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_chateaulafiterothschildpauillac
fof(lit_def_390,axiom,
! [X0] :
( iProver_Flat_chateaulafiterothschildpauillac(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_chateaulafiterothschild
fof(lit_def_391,axiom,
! [X0] :
( iProver_Flat_chateaulafiterothschild(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_forman
fof(lit_def_392,axiom,
! [X0] :
( iProver_Flat_forman(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_stgenevieve
fof(lit_def_393,axiom,
! [X0] :
( iProver_Flat_stgenevieve(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_foxen
fof(lit_def_394,axiom,
! [X0] :
( iProver_Flat_foxen(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_mcguinnesso
fof(lit_def_395,axiom,
! [X0] :
( iProver_Flat_mcguinnesso(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_cortonmontrachet
fof(lit_def_396,axiom,
! [X0] :
( iProver_Flat_cortonmontrachet(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_corbans
fof(lit_def_397,axiom,
! [X0] :
( iProver_Flat_corbans(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_congresssprings
fof(lit_def_398,axiom,
! [X0] :
( iProver_Flat_congresssprings(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_marietta
fof(lit_def_399,axiom,
! [X0] :
( iProver_Flat_marietta(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_petermccoy
fof(lit_def_400,axiom,
! [X0] :
( iProver_Flat_petermccoy(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_selaks
fof(lit_def_401,axiom,
! [X0] :
( iProver_Flat_selaks(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_bancroft
fof(lit_def_402,axiom,
! [X0] :
( iProver_Flat_bancroft(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_chateauchevalblancstemilion
fof(lit_def_403,axiom,
! [X0] :
( iProver_Flat_chateauchevalblancstemilion(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_chateauchevalblanc
fof(lit_def_404,axiom,
! [X0] :
( iProver_Flat_chateauchevalblanc(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_chateaumorgonbeaujolais
fof(lit_def_405,axiom,
! [X0] :
( iProver_Flat_chateaumorgonbeaujolais(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_chateaumorgon
fof(lit_def_406,axiom,
! [X0] :
( iProver_Flat_chateaumorgon(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_elyse
fof(lit_def_407,axiom,
! [X0] :
( iProver_Flat_elyse(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_mountadam
fof(lit_def_408,axiom,
! [X0] :
( iProver_Flat_mountadam(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_taylorport
fof(lit_def_409,axiom,
! [X0] :
( iProver_Flat_taylorport(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_taylor
fof(lit_def_410,axiom,
! [X0] :
( iProver_Flat_taylor(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_chateaudychem
fof(lit_def_411,axiom,
! [X0] :
( iProver_Flat_chateaudychem(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_schlossrothermel
fof(lit_def_412,axiom,
! [X0] :
( iProver_Flat_schlossrothermel(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_garyfarrell
fof(lit_def_413,axiom,
! [X0] :
( iProver_Flat_garyfarrell(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_closdevougeotcotesdor
fof(lit_def_414,axiom,
! [X0] :
( iProver_Flat_closdevougeotcotesdor(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_closdevougeot
fof(lit_def_415,axiom,
! [X0] :
( iProver_Flat_closdevougeot(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_cotturi
fof(lit_def_416,axiom,
! [X0] :
( iProver_Flat_cotturi(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_closdelapoussiesancerre
fof(lit_def_417,axiom,
! [X0] :
( iProver_Flat_closdelapoussiesancerre(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_closdelapoussie
fof(lit_def_418,axiom,
! [X0] :
( iProver_Flat_closdelapoussie(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_longridge
fof(lit_def_419,axiom,
! [X0] :
( iProver_Flat_longridge(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_kalincellars
fof(lit_def_420,axiom,
! [X0] :
( iProver_Flat_kalincellars(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_pagemillwinery
fof(lit_def_421,axiom,
! [X0] :
( iProver_Flat_pagemillwinery(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_seanthackrey
fof(lit_def_422,axiom,
! [X0] :
( iProver_Flat_seanthackrey(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_saucelitocanyon
fof(lit_def_423,axiom,
! [X0] :
( iProver_Flat_saucelitocanyon(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_chateaudemeursault
fof(lit_def_424,axiom,
! [X0] :
( iProver_Flat_chateaudemeursault(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_santacruzmountainvineyard
fof(lit_def_425,axiom,
! [X0] :
( iProver_Flat_santacruzmountainvineyard(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_lanetanner
fof(lit_def_426,axiom,
! [X0] :
( iProver_Flat_lanetanner(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_rosedanjou
fof(lit_def_427,axiom,
! [X0] :
( iProver_Flat_rosedanjou(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_danjou
fof(lit_def_428,axiom,
! [X0] :
( iProver_Flat_danjou(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_chateaumargaux
fof(lit_def_429,axiom,
! [X0] :
( iProver_Flat_chateaumargaux(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_chateaumargauxwinery
fof(lit_def_430,axiom,
! [X0] :
( iProver_Flat_chateaumargauxwinery(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_kathrynkennedy
fof(lit_def_431,axiom,
! [X0] :
( iProver_Flat_kathrynkennedy(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_mountedenvineyard
fof(lit_def_432,axiom,
! [X0] :
( iProver_Flat_mountedenvineyard(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_whitehalllane
fof(lit_def_433,axiom,
! [X0] :
( iProver_Flat_whitehalllane(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_ventana
fof(lit_def_434,axiom,
! [X0] :
( iProver_Flat_ventana(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_schlossvolrad
fof(lit_def_435,axiom,
! [X0] :
( iProver_Flat_schlossvolrad(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_stonleigh
fof(lit_def_436,axiom,
! [X0] :
( iProver_Flat_stonleigh(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_sevreetmainemuscadet
fof(lit_def_437,axiom,
! [X0] :
( iProver_Flat_sevreetmainemuscadet(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_sevreetmaine
fof(lit_def_438,axiom,
! [X0] :
( iProver_Flat_sevreetmaine(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_dry
fof(lit_def_439,axiom,
! [X0] :
( iProver_Flat_dry(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_sweet
fof(lit_def_440,axiom,
! [X0] :
( iProver_Flat_sweet(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_offdry
fof(lit_def_441,axiom,
! [X0] :
( iProver_Flat_offdry(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_californiaregion
fof(lit_def_442,axiom,
! [X0] :
( iProver_Flat_californiaregion(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_usregion
fof(lit_def_443,axiom,
! [X0] :
( iProver_Flat_usregion(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_sancerreregion
fof(lit_def_444,axiom,
! [X0] :
( iProver_Flat_sancerreregion(X0)
<=> X0 = iProver_Domain_i_2 ) ).
%------ Positive definition of iProver_Flat_loireregion
fof(lit_def_445,axiom,
! [X0] :
( iProver_Flat_loireregion(X0)
<=> X0 = iProver_Domain_i_2 ) ).
%------ Positive definition of iProver_Flat_naparegion
fof(lit_def_446,axiom,
! [X0] :
( iProver_Flat_naparegion(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_centraltexasregion
fof(lit_def_447,axiom,
! [X0] :
( iProver_Flat_centraltexasregion(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_santabarbararegion
fof(lit_def_448,axiom,
! [X0] :
( iProver_Flat_santabarbararegion(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_frenchregion
fof(lit_def_449,axiom,
! [X0] :
( iProver_Flat_frenchregion(X0)
<=> X0 = iProver_Domain_i_2 ) ).
%------ Positive definition of iProver_Flat_newzealandregion
fof(lit_def_450,axiom,
! [X0] :
( iProver_Flat_newzealandregion(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_sonomaregion
fof(lit_def_451,axiom,
! [X0] :
( iProver_Flat_sonomaregion(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_southaustraliaregion
fof(lit_def_452,axiom,
! [X0] :
( iProver_Flat_southaustraliaregion(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_chiantiregion
fof(lit_def_453,axiom,
! [X0] :
( iProver_Flat_chiantiregion(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_italianregion
fof(lit_def_454,axiom,
! [X0] :
( iProver_Flat_italianregion(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_sauterneregion
fof(lit_def_455,axiom,
! [X0] :
( iProver_Flat_sauterneregion(X0)
<=> X0 = iProver_Domain_i_2 ) ).
%------ Positive definition of iProver_Flat_bordeauxregion
fof(lit_def_456,axiom,
! [X0] :
( iProver_Flat_bordeauxregion(X0)
<=> X0 = iProver_Domain_i_2 ) ).
%------ Positive definition of iProver_Flat_pauillacregion
fof(lit_def_457,axiom,
! [X0] :
( iProver_Flat_pauillacregion(X0)
<=> X0 = iProver_Domain_i_2 ) ).
%------ Positive definition of iProver_Flat_medocregion
fof(lit_def_458,axiom,
! [X0] :
( iProver_Flat_medocregion(X0)
<=> X0 = iProver_Domain_i_2 ) ).
%------ Positive definition of iProver_Flat_texasregion
fof(lit_def_459,axiom,
! [X0] :
( iProver_Flat_texasregion(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_germanyregion
fof(lit_def_460,axiom,
! [X0] :
( iProver_Flat_germanyregion(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_anjouregion
fof(lit_def_461,axiom,
! [X0] :
( iProver_Flat_anjouregion(X0)
<=> X0 = iProver_Domain_i_2 ) ).
%------ Positive definition of iProver_Flat_centralcoastregion
fof(lit_def_462,axiom,
! [X0] :
( iProver_Flat_centralcoastregion(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_arroyogranderegion
fof(lit_def_463,axiom,
! [X0] :
( iProver_Flat_arroyogranderegion(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_australianregion
fof(lit_def_464,axiom,
! [X0] :
( iProver_Flat_australianregion(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_santacruzmountainsregion
fof(lit_def_465,axiom,
! [X0] :
( iProver_Flat_santacruzmountainsregion(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_mendocinoregion
fof(lit_def_466,axiom,
! [X0] :
( iProver_Flat_mendocinoregion(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_margauxregion
fof(lit_def_467,axiom,
! [X0] :
( iProver_Flat_margauxregion(X0)
<=> X0 = iProver_Domain_i_2 ) ).
%------ Positive definition of iProver_Flat_muscadetregion
fof(lit_def_468,axiom,
! [X0] :
( iProver_Flat_muscadetregion(X0)
<=> X0 = iProver_Domain_i_2 ) ).
%------ Positive definition of iProver_Flat_alsaceregion
fof(lit_def_469,axiom,
! [X0] :
( iProver_Flat_alsaceregion(X0)
<=> X0 = iProver_Domain_i_2 ) ).
%------ Positive definition of iProver_Flat_stemilionregion
fof(lit_def_470,axiom,
! [X0] :
( iProver_Flat_stemilionregion(X0)
<=> X0 = iProver_Domain_i_2 ) ).
%------ Positive definition of iProver_Flat_bourgogneregion
fof(lit_def_471,axiom,
! [X0] :
( iProver_Flat_bourgogneregion(X0)
<=> X0 = iProver_Domain_i_2 ) ).
%------ Positive definition of iProver_Flat_toursregion
fof(lit_def_472,axiom,
! [X0] :
( iProver_Flat_toursregion(X0)
<=> X0 = iProver_Domain_i_2 ) ).
%------ Positive definition of iProver_Flat_cotesdorregion
fof(lit_def_473,axiom,
! [X0] :
( iProver_Flat_cotesdorregion(X0)
<=> X0 = iProver_Domain_i_2 ) ).
%------ Positive definition of iProver_Flat_ednavalleyregion
fof(lit_def_474,axiom,
! [X0] :
( iProver_Flat_ednavalleyregion(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_beaujolaisregion
fof(lit_def_475,axiom,
! [X0] :
( iProver_Flat_beaujolaisregion(X0)
<=> X0 = iProver_Domain_i_2 ) ).
%------ Positive definition of iProver_Flat_meursaultregion
fof(lit_def_476,axiom,
! [X0] :
( iProver_Flat_meursaultregion(X0)
<=> X0 = iProver_Domain_i_2 ) ).
%------ Positive definition of iProver_Flat_semillongrape
fof(lit_def_477,axiom,
! [X0] :
( iProver_Flat_semillongrape(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_sauvignonblancgrape
fof(lit_def_478,axiom,
! [X0] :
( iProver_Flat_sauvignonblancgrape(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_zinfandelgrape
fof(lit_def_479,axiom,
! [X0] :
( iProver_Flat_zinfandelgrape(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_pinotblancgrape
fof(lit_def_480,axiom,
! [X0] :
( iProver_Flat_pinotblancgrape(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_chardonnaygrape
fof(lit_def_481,axiom,
! [X0] :
( iProver_Flat_chardonnaygrape(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_petitesyrahgrape
fof(lit_def_482,axiom,
! [X0] :
( iProver_Flat_petitesyrahgrape(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_red
fof(lit_def_483,axiom,
! [X0] :
( iProver_Flat_red(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_cabernetsauvignongrape
fof(lit_def_484,axiom,
! [X0] :
( iProver_Flat_cabernetsauvignongrape(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_cabernetfrancgrape
fof(lit_def_485,axiom,
! [X0] :
( iProver_Flat_cabernetfrancgrape(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_rose
fof(lit_def_486,axiom,
! [X0] :
( iProver_Flat_rose(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_gamaygrape
fof(lit_def_487,axiom,
! [X0] :
( iProver_Flat_gamaygrape(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_cheninblancgrape
fof(lit_def_488,axiom,
! [X0] :
( iProver_Flat_cheninblancgrape(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_rieslinggrape
fof(lit_def_489,axiom,
! [X0] :
( iProver_Flat_rieslinggrape(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_pinotnoirgrape
fof(lit_def_490,axiom,
! [X0] :
( iProver_Flat_pinotnoirgrape(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_merlotgrape
fof(lit_def_491,axiom,
! [X0] :
( iProver_Flat_merlotgrape(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_portugalregion
fof(lit_def_492,axiom,
! [X0] :
( iProver_Flat_portugalregion(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_sangiovesegrape
fof(lit_def_493,axiom,
! [X0] :
( iProver_Flat_sangiovesegrape(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_petiteverdotgrape
fof(lit_def_494,axiom,
! [X0] :
( iProver_Flat_petiteverdotgrape(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_malbecgrape
fof(lit_def_495,axiom,
! [X0] :
( iProver_Flat_malbecgrape(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_beringer
fof(lit_def_496,axiom,
! [X0] :
( iProver_Flat_beringer(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_handley
fof(lit_def_497,axiom,
! [X0] :
( iProver_Flat_handley(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------ Positive definition of iProver_Flat_year1998
fof(lit_def_498,axiom,
! [X0] :
( iProver_Flat_year1998(X0)
<=> X0 = iProver_Domain_i_1 ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRD002+1 : TPTP v9.3.1. Released v6.2.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p SAT
% 0.12/5.55 % Computer : n018.cluster.edu
% 0.12/5.55 % Model : x86_64 x86_64
% 0.12/5.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.55 % Memory : 8046.5625MB
% 0.12/5.55 % OS : Linux 6.8.0-71-generic
% 0.12/5.55 % CPULimit : 300
% 0.12/5.55 % WCLimit : 300
% 0.12/5.55 % DateTime : Thu Sep 24 06:25:10 UTC 2026
% 0.12/5.55 % CPUTime :
% 0.12/5.55 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p SAT
% 0.12/5.58 Running model finding
% 0.12/5.58 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fnt_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/5.59
% 0.12/5.59 % ======== iProver multi-core TPTP/SMT =========
% 0.12/5.59
% 0.12/5.59 % Detected problem language: tptp
% 0.15/5.61 % Proving...
% 2.36/6.97 % SZS status Started for theBenchmark.p
% 2.36/6.97 % SZS status CounterSatisfiable for theBenchmark.p
% 2.36/6.97
% 2.36/6.97 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.36/6.97
% 2.36/6.97 ------ iProver source info
% 2.36/6.97
% 2.36/6.97 git: date: 2026-07-19 20:42:38 +0200
% 2.36/6.97 git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.36/6.97 git: non_committed_changes: false
% 2.36/6.97
% 2.36/6.97 ------ Parsing...
% 2.36/6.97 ------ Clausification by vclausify_rel & Parsing by iProver...
% 2.36/6.97 ------ Proving...
% 2.36/6.97 ------ Problem Properties
% 2.36/6.97
% 2.36/6.97
% 2.36/6.97 clauses 1615
% 2.36/6.97 conjectures 1
% 2.36/6.97 EPR 1615
% 2.36/6.97 Horn 1615
% 2.36/6.97 unary 654
% 2.36/6.97 binary 456
% 2.36/6.97 lits 3122
% 2.36/6.97 lits eq 0
% 2.36/6.97 fd_pure 0
% 2.36/6.97 fd_pseudo 0
% 2.36/6.97 fd_cond 0
% 2.36/6.97 fd_pseudo_cond 0
% 2.36/6.97 AC symbols 0
% 2.36/6.97
% 2.36/6.97 ------ Input Options Time Limit: Unbounded
% 2.36/6.97
% 2.36/6.97
% 2.36/6.97 ------ Finite Models:
% 2.36/6.97
% 2.36/6.97 ------ lit_activity_flag true
% 2.36/6.97
% 2.36/6.97
% 2.36/6.97 ------ Trying domains of size >= : 1
% 2.36/6.97
% 2.36/6.97 ------ Trying domains of size >= : 2
% 2.36/6.97 ------
% 2.36/6.97 Current options:
% 2.36/6.97 ------
% 2.36/6.97
% 2.36/6.97 ------ Input Options
% 2.36/6.97
% 2.36/6.97 --out_options all
% 2.36/6.97 --tptp_safe_out true
% 2.36/6.97 --problem_path ""
% 2.36/6.97 --include_path ""
% 2.36/6.97 --clausifier res/vclausify_rel
% 2.36/6.97 --clausifier_options --mode clausify -t 101.66 -updr off
% 2.36/6.97 --stdin false
% 2.36/6.97 --proof_out true
% 2.36/6.97 --proof_dot_file ""
% 2.36/6.97 --proof_reduce_dot []
% 2.36/6.97 --suppress_sat_res false
% 2.36/6.97 --suppress_unsat_res true
% 2.36/6.97 --stats_out none
% 2.36/6.97 --stats_mem false
% 2.36/6.97 --theory_stats_out false
% 2.36/6.97
% 2.36/6.97 ------ General Options
% 2.36/6.97
% 2.36/6.97 --fof false
% 2.36/6.97 --time_out_real 304.97
% 2.36/6.97 --time_out_virtual -1.
% 2.36/6.97 --rnd_seed 13
% 2.36/6.97 --symbol_type_check false
% 2.36/6.97 --clausify_out false
% 2.36/6.97 --sig_cnt_out false
% 2.36/6.97 --trig_cnt_out false
% 2.36/6.97 --trig_cnt_out_tolerance 1.
% 2.36/6.97 --trig_cnt_out_sk_spl false
% 2.36/6.97 --abstr_cl_out false
% 2.36/6.97
% 2.36/6.97 ------ Interactive Mode
% 2.36/6.97
% 2.36/6.97 --interactive_mode false
% 2.36/6.97 --external_ip_address ""
% 2.36/6.97 --external_port 0
% 2.36/6.97
% 2.36/6.97 ------ Global Options
% 2.36/6.97
% 2.36/6.97 --schedule none
% 2.36/6.97 --add_important_lit false
% 2.36/6.97 --prop_solver_per_cl 500
% 2.36/6.97 --subs_bck_mult 8
% 2.36/6.97 --min_unsat_core false
% 2.36/6.97 --soft_assumptions false
% 2.36/6.97 --soft_lemma_size 3
% 2.36/6.97 --prop_impl_unit_size 0
% 2.36/6.97 --prop_impl_unit []
% 2.36/6.97 --share_sel_clauses true
% 2.36/6.97 --reset_solvers false
% 2.36/6.97 --bc_imp_inh [conj_cone]
% 2.36/6.97 --conj_cone_tolerance 3.
% 2.36/6.97 --extra_neg_conj none
% 2.36/6.97 --large_theory_mode true
% 2.36/6.97 --prolific_symb_bound 200
% 2.36/6.97 --lt_threshold 2000
% 2.36/6.97 --clause_weak_htbl true
% 2.36/6.97 --gc_record_bc_elim false
% 2.36/6.97
% 2.36/6.97 ------ Preprocessing Options
% 2.36/6.97
% 2.36/6.97 --preprocessing_flag false
% 2.36/6.97 --time_out_prep_mult 0.1
% 2.36/6.97 --splitting_mode input
% 2.36/6.97 --splitting_grd true
% 2.36/6.97 --splitting_cvd false
% 2.36/6.97 --splitting_cvd_svl false
% 2.36/6.97 --splitting_nvd 32
% 2.36/6.97 --sub_typing false
% 2.36/6.97 --prep_eq_flat_conj false
% 2.36/6.97 --prep_ineq_split false
% 2.36/6.97 --prep_eq_flat_all_gr false
% 2.36/6.97 --prep_gs_sim true
% 2.36/6.97 --prep_unflatten true
% 2.36/6.97 --prep_res_sim true
% 2.36/6.97 --prep_sup_sim_all true
% 2.36/6.97 --prep_sup_sim_sup false
% 2.36/6.97 --prep_upred true
% 2.36/6.97 --prep_well_definedness true
% 2.36/6.97 --prep_sem_filter exhaustive
% 2.36/6.97 --prep_sem_filter_out false
% 2.36/6.97 --pred_elim true
% 2.36/6.97 --res_sim_input true
% 2.36/6.97 --eq_ax_congr_red true
% 2.36/6.97 --pure_diseq_elim true
% 2.36/6.97 --brand_transform false
% 2.36/6.97 --non_eq_to_eq false
% 2.36/6.97 --prep_eq_proxy false
% 2.36/6.97 --prep_def_merge true
% 2.36/6.97 --prep_def_merge_prop_impl false
% 2.36/6.97 --prep_def_merge_mbd true
% 2.36/6.97 --prep_def_merge_tr_red false
% 2.36/6.97 --prep_def_merge_tr_cl false
% 2.36/6.97 --smt_preprocessing false
% 2.36/6.97 --smt_ac_axioms fast
% 2.36/6.97 --preprocessed_out false
% 2.36/6.97 --preprocessed_stats false
% 2.36/6.97
% 2.36/6.97 ------ Abstraction refinement Options
% 2.36/6.97
% 2.36/6.97 --abstr_ref []
% 2.36/6.97 --abstr_ref_prep false
% 2.36/6.97 --abstr_ref_until_sat false
% 2.36/6.97 --abstr_ref_sig_restrict funpre
% 2.36/6.97 --abstr_ref_af_restrict_to_split_sk false
% 2.36/6.97 --abstr_ref_under []
% 2.36/6.97
% 2.36/6.97 ------ SAT Options
% 2.36/6.97
% 2.36/6.97 --sat_mode true
% 2.36/6.97 --sat_fm_restart_options ""
% 2.36/6.97 --sat_gr_def false
% 2.36/6.97 --sat_epr_types false
% 2.36/6.97 --sat_non_cyclic_types false
% 2.36/6.97 --sat_finite_models true
% 2.36/6.97 --sat_fm_lemmas false
% 2.36/6.97 --sat_fm_prep false
% 2.36/6.97 --sat_fm_uc_incr false
% 2.36/6.97 --sat_out_model pos
% 2.36/6.97 --sat_out_clauses false
% 2.36/6.97
% 2.36/6.97 ------ QBF Options
% 2.36/6.97
% 2.36/6.97 --qbf_mode false
% 2.36/6.97 --qbf_elim_univ false
% 2.36/6.97 --qbf_dom_inst none
% 2.36/6.97 --qbf_dom_pre_inst false
% 2.36/6.97 --qbf_sk_in false
% 2.36/6.97 --qbf_pred_elim true
% 2.36/6.97 --qbf_split 512
% 2.36/6.97
% 2.36/6.97 ------ BMC1 Options
% 2.36/6.97
% 2.36/6.97 --bmc1_incremental false
% 2.36/6.97 --bmc1_axioms reachable_all
% 2.36/6.97 --bmc1_min_bound 0
% 2.36/6.97 --bmc1_max_bound -1
% 2.36/6.97 --bmc1_max_bound_default -1
% 2.36/6.97 --bmc1_symbol_reachability true
% 2.36/6.97 --bmc1_property_lemmas false
% 2.36/6.97 --bmc1_k_induction false
% 2.36/6.97 --bmc1_non_equiv_states false
% 2.36/6.97 --bmc1_deadlock false
% 2.36/6.97 --bmc1_ucm false
% 2.36/6.97 --bmc1_add_unsat_core none
% 2.36/6.97 --bmc1_unsat_core_children false
% 2.36/6.97 --bmc1_unsat_core_extrapolate_axioms false
% 2.36/6.97 --bmc1_out_stat full
% 2.36/6.97 --bmc1_ground_init false
% 2.36/6.97 --bmc1_pre_inst_next_state false
% 2.36/6.97 --bmc1_pre_inst_state false
% 2.36/6.97 --bmc1_pre_inst_reach_state false
% 2.36/6.97 --bmc1_out_unsat_core false
% 2.36/6.97 --bmc1_aig_witness_out false
% 2.36/6.97 --bmc1_verbose false
% 2.36/6.97 --bmc1_dump_clauses_tptp false
% 2.36/6.97 --bmc1_dump_unsat_core_tptp false
% 2.36/6.97 --bmc1_dump_file -
% 2.36/6.97 --bmc1_ucm_expand_uc_limit 128
% 2.36/6.97 --bmc1_ucm_n_expand_iterations 6
% 2.36/6.97 --bmc1_ucm_extend_mode 1
% 2.36/6.97 --bmc1_ucm_init_mode 2
% 2.36/6.97 --bmc1_ucm_cone_mode none
% 2.36/6.97 --bmc1_ucm_reduced_relation_type 0
% 2.36/6.97 --bmc1_ucm_relax_model 4
% 2.36/6.97 --bmc1_ucm_full_tr_after_sat true
% 2.36/6.97 --bmc1_ucm_expand_neg_assumptions false
% 2.36/6.97 --bmc1_ucm_layered_model none
% 2.36/6.97 --bmc1_ucm_max_lemma_size 10
% 2.36/6.97
% 2.36/6.97 ------ AIG Options
% 2.36/6.97
% 2.36/6.97 --aig_mode false
% 2.36/6.97
% 2.36/6.97 ------ Instantiation Options
% 2.36/6.97
% 2.36/6.97 --instantiation_flag true
% 2.36/6.97 --inst_sos_flag false
% 2.36/6.97 --inst_sos_phase true
% 2.36/6.97 --inst_sos_sth_lit_sel [+prop;+non_prol_conj_symb;-eq;+ground;-num_var;-num_symb]
% 2.36/6.97 --inst_lit_sel [+prop;+sign;+ground;-num_var;-num_symb]
% 2.36/6.97 --inst_lit_sel_side num_symb
% 2.36/6.97 --inst_solver_per_active 1400
% 2.36/6.97 --inst_solver_calls_frac 1.
% 2.36/6.97 --inst_to_smt_solver true
% 2.36/6.97 --inst_passive_queue_type priority_queues
% 2.36/6.97 --inst_passive_queues [[-conj_dist;+conj_symb;-num_var];[+age;-num_symb]]
% 2.36/6.97 --inst_passive_queues_freq [25;2]
% 2.36/6.97 --inst_dismatching true
% 2.36/6.97 --inst_eager_unprocessed_to_passive true
% 2.36/6.97 --inst_unprocessed_bound 1000
% 2.36/6.97 --inst_prop_sim_given true
% 2.36/6.97 --inst_prop_sim_new false
% 2.36/6.97 --inst_subs_new false
% 2.36/6.97 --inst_eq_res_simp false
% 2.36/6.97 --inst_subs_given false
% 2.36/6.97 --inst_orphan_elimination true
% 2.36/6.97 --inst_learning_loop_flag true
% 2.36/6.97 --inst_learning_start 3000
% 2.36/6.97 --inst_learning_factor 2
% 2.36/6.97 --inst_start_prop_sim_after_learn 3
% 2.36/6.97 --inst_sel_renew solver
% 2.36/6.97 --inst_lit_activity_flag true
% 2.36/6.97 --inst_restr_to_given false
% 2.36/6.97 --inst_activity_threshold 500
% 2.36/6.97
% 2.36/6.97 ------ Resolution Options
% 2.36/6.97
% 2.36/6.97 --resolution_flag false
% 2.36/6.97 --res_lit_sel adaptive
% 2.36/6.97 --res_lit_sel_side none
% 2.36/6.97 --res_ordering kbo
% 2.36/6.97 --res_to_prop_solver active
% 2.36/6.97 --res_prop_simpl_new false
% 2.36/6.97 --res_prop_simpl_given true
% 2.36/6.97 --res_to_smt_solver true
% 2.36/6.97 --res_passive_queue_type priority_queues
% 2.36/6.97 --res_passive_queues [[-conj_dist;+conj_symb;-num_symb];[+age;-num_symb]]
% 2.36/6.97 --res_passive_queues_freq [15;5]
% 2.36/6.97 --res_forward_subs full
% 2.36/6.97 --res_backward_subs full
% 2.36/6.97 --res_forward_subs_resolution true
% 2.36/6.97 --res_backward_subs_resolution true
% 2.36/6.97 --res_orphan_elimination true
% 2.36/6.97 --res_time_limit 300.
% 2.36/6.97
% 2.36/6.97 ------ Superposition Options
% 2.36/6.97
% 2.36/6.97 --superposition_flag false
% 2.36/6.97 --sup_passive_queue_type priority_queues
% 2.36/6.97 --sup_passive_queues [[-conj_dist;-num_symb];[+score;+min_def_symb;-max_atom_input_occur;+conj_non_prolific_symb];[+age;-num_symb];[+score;-num_symb]]
% 2.36/6.97 --sup_passive_queues_freq [8;1;4;4]
% 2.36/6.97 --twee_lhs_weight 4
% 2.36/6.97 --sup_set_join false
% 2.36/6.97 --sup_set_join_goals true
% 2.36/6.97 --sup_set_join_limit 1000
% 2.36/6.97 --demod_completeness_check fast
% 2.36/6.97 --demod_use_ground true
% 2.36/6.97 --sup_unprocessed_bound 0
% 2.36/6.97 --sup_to_prop_solver passive
% 2.36/6.97 --sup_prop_simpl_new true
% 2.36/6.97 --sup_prop_simpl_given true
% 2.36/6.97 --sup_fun_splitting false
% 2.36/6.97 --sup_iter_deepening 2
% 2.36/6.97 --sup_restarts_mult 12
% 2.36/6.97 --sup_score sim_d_gen
% 2.36/6.97 --sup_share_score_frac 0.2
% 2.36/6.97 --sup_share_max_num_cl 500
% 2.36/6.97 --sup_ordering kbo
% 2.36/6.97 --sup_symb_ordering invfreq
% 2.36/6.97 --sup_term_weight default
% 2.36/6.97
% 2.36/6.97 ------ Superposition Simplification Setup
% 2.36/6.97
% 2.36/6.97 --sup_indices_passive [LightNormIndex;FwDemodIndex]
% 2.36/6.97 --sup_full_triv [SMTSimplify;PropSubs]
% 2.36/6.97 --sup_full_fw [ACNormalisation;FwLightNorm;FwDemod;FwUnitSubsAndRes;FwSubsumption;FwSubsumptionRes;FwGroundJoinability]
% 2.36/6.97 --sup_full_bw [BwDemod;BwUnitSubsAndRes;BwSubsumption;BwSubsumptionRes]
% 2.36/6.97 --sup_immed_triv []
% 2.36/6.97 --sup_immed_fw_main [ACNormalisation;FwLightNorm;FwUnitSubsAndRes]
% 2.36/6.97 --sup_immed_fw_immed [ACNormalisation;FwUnitSubsAndRes]
% 2.36/6.97 --sup_immed_bw_main [BwUnitSubsAndRes;BwDemod]
% 2.36/6.97 --sup_immed_bw_immed [BwUnitSubsAndRes;BwSubsumption;BwSubsumptionRes]
% 2.36/6.97 --sup_input_triv [Unflattening;SMTSimplify]
% 2.36/6.97 --sup_input_fw [FwACDemod;ACNormalisation;FwLightNorm;FwDemod;FwUnitSubsAndRes;FwSubsumption;FwSubsumptionRes;FwGroundJoinability]
% 2.36/6.97 --sup_input_bw [BwACDemod;BwDemod;BwUnitSubsAndRes;BwSubsumption;BwSubsumptionRes]
% 2.36/6.97 --sup_full_fixpoint true
% 2.36/6.97 --sup_main_fixpoint true
% 2.36/6.97 --sup_immed_fixpoint false
% 2.36/6.97 --sup_input_fixpoint true
% 2.36/6.97 --sup_cache_sim none
% 2.36/6.97 --sup_smt_interval 500
% 2.36/6.97 --sup_bw_gjoin_interval 0
% 2.36/6.97
% 2.36/6.97 ------ Combination Options
% 2.36/6.97
% 2.36/6.97 --comb_mode clause_based
% 2.36/6.97 --comb_inst_mult 5
% 2.36/6.97 --comb_res_mult 1
% 2.36/6.97 --comb_sup_mult 8
% 2.36/6.97 --comb_sup_deep_mult 2
% 2.36/6.97
% 2.36/6.97 ------ Debug Options
% 2.36/6.97
% 2.36/6.97 --dbg_backtrace false
% 2.36/6.97 --dbg_dump_prop_clauses false
% 2.36/6.97 --dbg_dump_prop_clauses_file -
% 2.36/6.97 --dbg_out_stat false
% 2.36/6.97 --dbg_just_parse false
% 2.36/6.97
% 2.36/6.97
% 2.36/6.97
% 2.36/6.97
% 2.36/6.97 ------ Proving...
% 2.36/6.97
% 2.36/6.97
% 2.36/6.97 % SZS status CounterSatisfiable for theBenchmark.p
% 2.36/6.97
% 2.36/6.97 ------ Building Model...Done
% 2.36/6.97
% 2.36/6.97 %------ The model is defined over ground terms (initial term algebra).
% 2.36/6.97 %------ Predicates are defined as (\forall x_1,..,x_n ((~)P(x_1,..,x_n) <=> (\phi(x_1,..,x_n))))
% 2.36/6.97 %------ where \phi is a formula over the term algebra.
% 2.36/6.97 %------ If we have equality in the problem then it is also defined as a predicate above,
% 2.36/6.97 %------ with "=" on the right-hand-side of the definition interpreted over the term algebra term_algebra_type
% 2.36/6.97 %------ See help for --sat_out_model for different model outputs.
% 2.36/6.97 %------ equality_sorted(X0,X1,X2) can be used in the place of usual "="
% 2.36/6.97 %------ where the first argument stands for the sort ($i in the unsorted case)
% 2.36/6.97 % SZS output start Model for theBenchmark.p
% See solution above
% 8.51/7.02
%------------------------------------------------------------------------------