%------------------------------------------------------------------------------ % File : Nitpick---2016 % Problem : PRD002+1 : TPTP v6.4.0. Released v6.2.0. % Transfm : none % Format : tptp:raw % Command : isabelle tptp_nitpick %d %s % Computer : n107.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32218.75MB % OS : Linux 3.10.0-327.36.3.el7.x86_64 % CPULimit : 300s % DateTime : Wed Jan 18 11:39:26 EST 2017 % Result : CounterSatisfiable 36.48s % Output : FiniteModel 36.48s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : PRD002+1 : TPTP v6.4.0. Released v6.2.0. % 0.00/0.04 % Command : isabelle tptp_nitpick %d %s % 0.02/0.23 % Computer : n107.star.cs.uiowa.edu % 0.02/0.23 % Model : x86_64 x86_64 % 0.02/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.02/0.23 % Memory : 32218.75MB % 0.02/0.23 % OS : Linux 3.10.0-327.36.3.el7.x86_64 % 0.02/0.23 % CPULimit : 300 % 0.02/0.23 % DateTime : Sat Jan 14 22:18:18 CST 2017 % 0.02/0.24 % CPUTime : % 36.48/24.29 Nitpicking formula... % 36.48/24.29 Timestamp: 22:18:28 % 36.48/24.29 Using SAT solver "Lingeling_JNI" The following solvers are configured: % 36.48/24.29 "Lingeling_JNI", "CryptoMiniSat_JNI", "MiniSat_JNI", "SAT4J", "SAT4J_Light" % 36.48/24.29 Batch 1 of 20: Trying 5 scopes: % 36.48/24.29 card TPTP_Interpret.ind = 1 % 36.48/24.29 card TPTP_Interpret.ind = 2 % 36.48/24.29 card TPTP_Interpret.ind = 3 % 36.48/24.29 card TPTP_Interpret.ind = 4 % 36.48/24.29 card TPTP_Interpret.ind = 5 % 36.48/24.29 % SZS status CounterSatisfiable % SZS output start FiniteModel % 36.48/24.29 Nitpick found a counterexample for card TPTP_Interpret.ind = 2: % 36.48/24.29 % 36.48/24.29 Constants: % 36.48/24.29 bnd_adjacentregion = % 36.48/24.29 (\<lambda>x. _) % 36.48/24.29 (i1 := (\<lambda>x. _)(i1 := False, i2 := False), % 36.48/24.29 i2 := (\<lambda>x. _)(i1 := False, i2 := False)) % 36.48/24.29 bnd_adjacentregion_aux = % 36.48/24.29 (\<lambda>x. _) % 36.48/24.29 (i1 := (\<lambda>x. _)(i1 := False, i2 := False), % 36.48/24.29 i2 := (\<lambda>x. _)(i1 := False, i2 := False)) % 36.48/24.29 bnd_alsaceregion = i1 % 36.48/24.29 bnd_alsatianwine = (\<lambda>x. _)(i1 := False, i2 := False) % 36.48/24.29 bnd_americanwine = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_anjou = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_anjou_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_anjouregion = i1 % 36.48/24.29 bnd_arroyogranderegion = i2 % 36.48/24.29 bnd_australianregion = i2 % 36.48/24.29 bnd_bancroft = i2 % 36.48/24.29 bnd_bancroftchardonnay = i2 % 36.48/24.29 bnd_beaujolais = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_beaujolais_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_beaujolaisregion = i1 % 36.48/24.29 bnd_beringer = i2 % 36.48/24.29 bnd_bordeaux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_bordeauxregion = i1 % 36.48/24.29 bnd_bourgogneregion = i1 % 36.48/24.29 bnd_burgundy = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_cabernetfranc = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_cabernetfranc_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_cabernetfrancgrape = i2 % 36.48/24.29 bnd_cabernetsauvignon = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_cabernetsauvignon_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_cabernetsauvignongrape = i2 % 36.48/24.29 bnd_californiaregion = i2 % 36.48/24.29 bnd_californiawine = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_centralcoastregion = i2 % 36.48/24.29 bnd_centraltexasregion = i2 % 36.48/24.29 bnd_chardonnay = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_chardonnay_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_chardonnaygrape = i2 % 36.48/24.29 bnd_chateauchevalblanc = i2 % 36.48/24.29 bnd_chateauchevalblancstemilion = i2 % 36.48/24.29 bnd_chateaudemeursault = i2 % 36.48/24.29 bnd_chateaudemeursaultmeursault = i2 % 36.48/24.29 bnd_chateaudychem = i2 % 36.48/24.29 bnd_chateaudychemsauterne = i2 % 36.48/24.29 bnd_chateaulafiterothschild = i2 % 36.48/24.29 bnd_chateaulafiterothschildpauillac = i2 % 36.48/24.29 bnd_chateaumargaux = i2 % 36.48/24.29 bnd_chateaumargauxwinery = i2 % 36.48/24.29 bnd_chateaumorgon = i2 % 36.48/24.29 bnd_chateaumorgonbeaujolais = i2 % 36.48/24.29 bnd_cheninblanc = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_cheninblanc_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_cheninblancgrape = i2 % 36.48/24.29 bnd_chianti = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_chianti_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_chianticlassico = i2 % 36.48/24.29 bnd_chiantiregion = i1 % 36.48/24.29 bnd_closdelapoussie = i2 % 36.48/24.29 bnd_closdelapoussiesancerre = i2 % 36.48/24.29 bnd_closdevougeot = i2 % 36.48/24.29 bnd_closdevougeotcotesdor = i2 % 36.48/24.29 bnd_congresssprings = i2 % 36.48/24.29 bnd_congressspringssemillon = i2 % 36.48/24.29 bnd_corbans = i2 % 36.48/24.29 bnd_corbansdrywhiteriesling = i2 % 36.48/24.29 bnd_corbansprivatebinsauvignonblanc = i2 % 36.48/24.29 bnd_corbanssauvignonblanc = i2 % 36.48/24.29 bnd_cortonmontrachet = i2 % 36.48/24.29 bnd_cortonmontrachetwhiteburgundy = i2 % 36.48/24.29 bnd_cotesdor = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_cotesdor_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_cotesdorregion = i1 % 36.48/24.29 bnd_cotturi = i2 % 36.48/24.29 bnd_cotturizinfandel = i2 % 36.48/24.29 bnd_danjou = i2 % 36.48/24.29 bnd_delicate = i2 % 36.48/24.29 bnd_dessertwine = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_dessertwine_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_dry = i2 % 36.48/24.29 bnd_dryredwine = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_dryriesling = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_dryriesling_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_drywhitewine = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_drywine = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_earlyharvest = (\<lambda>x. _)(i1 := False, i2 := False) % 36.48/24.29 bnd_ednavalleyregion = i2 % 36.48/24.29 bnd_elyse = i2 % 36.48/24.29 bnd_elysezinfandel = i2 % 36.48/24.29 bnd_forman = i2 % 36.48/24.29 bnd_formancabernetsauvignon = i2 % 36.48/24.29 bnd_formanchardonnay = i2 % 36.48/24.29 bnd_foxen = i2 % 36.48/24.29 bnd_foxencheninblanc = i2 % 36.48/24.29 bnd_frenchregion = i1 % 36.48/24.29 bnd_frenchwine = (\<lambda>x. _)(i1 := False, i2 := False) % 36.48/24.29 bnd_full = i2 % 36.48/24.29 bnd_fullbodiedwine = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_gamay = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_gamaygrape = i2 % 36.48/24.29 bnd_garyfarrell = i2 % 36.48/24.29 bnd_garyfarrellmerlot = i2 % 36.48/24.29 bnd_germanwine = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_germanyregion = i2 % 36.48/24.29 bnd_grape = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_handley = i2 % 36.48/24.29 bnd_hasbody = % 36.48/24.29 (\<lambda>x. _) % 36.48/24.29 (i1 := (\<lambda>x. _)(i1 := False, i2 := False), % 36.48/24.29 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 36.48/24.29 bnd_hasbody_aux = % 36.48/24.29 (\<lambda>x. _) % 36.48/24.29 (i1 := (\<lambda>x. _)(i1 := False, i2 := False), % 36.48/24.29 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 36.48/24.29 bnd_hascolor = % 36.48/24.29 (\<lambda>x. _) % 36.48/24.29 (i1 := (\<lambda>x. _)(i1 := False, i2 := False), % 36.48/24.29 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 36.48/24.29 bnd_hascolor_aux = % 36.48/24.29 (\<lambda>x. _) % 36.48/24.29 (i1 := (\<lambda>x. _)(i1 := False, i2 := False), % 36.48/24.29 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 36.48/24.29 bnd_hasflavor = % 36.48/24.29 (\<lambda>x. _) % 36.48/24.29 (i1 := (\<lambda>x. _)(i1 := False, i2 := False), % 36.48/24.29 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 36.48/24.29 bnd_hasflavor_aux = % 36.48/24.29 (\<lambda>x. _) % 36.48/24.29 (i1 := (\<lambda>x. _)(i1 := False, i2 := False), % 36.48/24.29 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 36.48/24.29 bnd_hasmaker = % 36.48/24.29 (\<lambda>x. _) % 36.48/24.29 (i1 := (\<lambda>x. _)(i1 := False, i2 := False), % 36.48/24.29 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 36.48/24.29 bnd_hasmaker_aux = % 36.48/24.29 (\<lambda>x. _) % 36.48/24.29 (i1 := (\<lambda>x. _)(i1 := False, i2 := False), % 36.48/24.29 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 36.48/24.29 bnd_hassugar = % 36.48/24.29 (\<lambda>x. _) % 36.48/24.29 (i1 := (\<lambda>x. _)(i1 := False, i2 := False), % 36.48/24.29 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 36.48/24.29 bnd_hassugar_aux = % 36.48/24.29 (\<lambda>x. _) % 36.48/24.29 (i1 := (\<lambda>x. _)(i1 := False, i2 := False), % 36.48/24.29 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 36.48/24.29 bnd_hasvintageyear = % 36.48/24.29 (\<lambda>x. _) % 36.48/24.29 (i1 := (\<lambda>x. _)(i1 := False, i2 := False), % 36.48/24.29 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 36.48/24.29 bnd_hasvintageyear_aux = % 36.48/24.29 (\<lambda>x. _) % 36.48/24.29 (i1 := (\<lambda>x. _)(i1 := False, i2 := False), % 36.48/24.29 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 36.48/24.29 bnd_haswinedescriptor = % 36.48/24.29 (\<lambda>x. _) % 36.48/24.29 (i1 := (\<lambda>x. _)(i1 := False, i2 := False), % 36.48/24.29 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 36.48/24.29 bnd_icewine = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_icewine_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_italianregion = i1 % 36.48/24.29 bnd_italianwine = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_kalincellars = i2 % 36.48/24.29 bnd_kalincellarssemillon = i2 % 36.48/24.29 bnd_kaon2equal = % 36.48/24.29 (\<lambda>x. _) % 36.48/24.29 (i1 := (\<lambda>x. _)(i1 := True, i2 := False), % 36.48/24.29 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 36.48/24.29 bnd_kaon2hu = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_kaon2namedobjects = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_kathrynkennedy = i2 % 36.48/24.29 bnd_kathrynkennedylateral = i2 % 36.48/24.29 bnd_lanetanner = i2 % 36.48/24.29 bnd_lanetannerpinotnoir = i2 % 36.48/24.29 bnd_lateharvest = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_light = i2 % 36.48/24.29 bnd_locatedin = % 36.48/24.29 (\<lambda>x. _) % 36.48/24.29 (i1 := (\<lambda>x. _)(i1 := True, i2 := False), % 36.48/24.29 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 36.48/24.29 bnd_locatedin_aux = % 36.48/24.29 (\<lambda>x. _) % 36.48/24.29 (i1 := (\<lambda>x. _)(i1 := True, i2 := False), % 36.48/24.29 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 36.48/24.29 bnd_loire = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_loireregion = i1 % 36.48/24.29 bnd_longridge = i2 % 36.48/24.29 bnd_longridgemerlot = i2 % 36.48/24.29 bnd_madefromfruit = % 36.48/24.29 (\<lambda>x. _) % 36.48/24.29 (i1 := (\<lambda>x. _)(i1 := False, i2 := False), % 36.48/24.29 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 36.48/24.29 bnd_madefromgrape = % 36.48/24.29 (\<lambda>x. _) % 36.48/24.29 (i1 := (\<lambda>x. _)(i1 := False, i2 := False), % 36.48/24.29 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 36.48/24.29 bnd_madefromgrape_aux = % 36.48/24.29 (\<lambda>x. _) % 36.48/24.29 (i1 := (\<lambda>x. _)(i1 := False, i2 := False), % 36.48/24.29 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 36.48/24.29 bnd_madeintowine = % 36.48/24.29 (\<lambda>x. _) % 36.48/24.29 (i1 := (\<lambda>x. _)(i1 := False, i2 := False), % 36.48/24.29 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 36.48/24.29 bnd_malbecgrape = i2 % 36.48/24.29 bnd_margaux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_margaux_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_margauxregion = i1 % 36.48/24.29 bnd_marietta = i2 % 36.48/24.29 bnd_mariettacabernetsauvignon = i2 % 36.48/24.29 bnd_mariettaoldvinesred = i2 % 36.48/24.29 bnd_mariettapetitesyrah = i2 % 36.48/24.29 bnd_mariettazinfandel = i2 % 36.48/24.29 bnd_mcguinnesso = i2 % 36.48/24.29 bnd_medium = i2 % 36.48/24.29 bnd_medoc = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_medocregion = i1 % 36.48/24.29 bnd_mendocinoregion = i2 % 36.48/24.29 bnd_meritage = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_meritage_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_merlot = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_merlot_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_merlotgrape = i2 % 36.48/24.29 bnd_meursault = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_meursault_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_meursaultregion = i1 % 36.48/24.29 bnd_moderate = i2 % 36.48/24.29 bnd_mountadam = i2 % 36.48/24.29 bnd_mountadamchardonnay = i2 % 36.48/24.29 bnd_mountadampinotnoir = i2 % 36.48/24.29 bnd_mountadamriesling = i2 % 36.48/24.29 bnd_mountedenvineyard = i2 % 36.48/24.29 bnd_mountedenvineyardednavalleychardonnay = i2 % 36.48/24.29 bnd_mountedenvineyardestatepinotnoir = i2 % 36.48/24.29 bnd_muscadet = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_muscadet_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_muscadetregion = i1 % 36.48/24.29 bnd_naparegion = i2 % 36.48/24.29 bnd_newzealandregion = i2 % 36.48/24.29 bnd_offdry = i2 % 36.48/24.29 bnd_ot____nom1 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom10 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom10_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom11 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom11_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom12 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom12_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom13 = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_ot____nom13_aux = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_ot____nom14 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_ot____nom14_aux = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_ot____nom15 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom15_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom16 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_ot____nom16_aux = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_ot____nom17 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom17_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom18 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom18_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom19 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_ot____nom19_aux = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_ot____nom1_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom2 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_ot____nom20 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom20_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom21 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom21_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom22 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_ot____nom22_aux = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_ot____nom23 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_ot____nom23_aux = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_ot____nom24 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom24_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom25 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom25_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom26 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_ot____nom26_aux = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_ot____nom27 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom27_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom28 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom28_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom29 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom29_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom2_aux = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_ot____nom3 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom30 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_ot____nom30_aux = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_ot____nom31 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_ot____nom31_aux = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_ot____nom32 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom32_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom33 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom33_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom34 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom34_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom35 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom35_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom36 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_ot____nom36_aux = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_ot____nom37 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom37_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom38 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom38_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom39 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom39_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom3_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom4 = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_ot____nom40 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom40_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom41 = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_ot____nom41_aux = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_ot____nom42 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_ot____nom42_aux = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_ot____nom43 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom43_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom44 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_ot____nom44_aux = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_ot____nom45 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom45_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom46 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_ot____nom46_aux = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_ot____nom47 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_ot____nom47_aux = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_ot____nom48 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom48_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom49 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom49_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom4_aux = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_ot____nom5 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom50 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom50_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom51 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom51_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom52 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_ot____nom52_aux = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_ot____nom53 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom53_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom54 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom54_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom55 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom55_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom56 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom56_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom57 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom57_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom58 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom58_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom59 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom59_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom5_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom6 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom60 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom60_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom61 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_ot____nom61_aux = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_ot____nom62 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom62_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom63 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom63_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom64 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom64_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom6_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom7 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom7_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom8 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom8_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom9 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_ot____nom9_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_pagemillwinery = i2 % 36.48/24.29 bnd_pagemillwinerycabernetsauvignon = i2 % 36.48/24.29 bnd_pauillac = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_pauillac_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_pauillacregion = i1 % 36.48/24.29 bnd_petermccoy = i2 % 36.48/24.29 bnd_petermccoychardonnay = i2 % 36.48/24.29 bnd_petitesyrah = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_petitesyrah_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_petitesyrahgrape = i2 % 36.48/24.29 bnd_petiteverdotgrape = i2 % 36.48/24.29 bnd_pinotblanc = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_pinotblancgrape = i2 % 36.48/24.29 bnd_pinotnoir = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_pinotnoir_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_pinotnoirgrape = i2 % 36.48/24.29 bnd_port = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_port_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_portugalregion = i2 % 36.48/24.29 bnd_potableliquid = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_produceswine = % 36.48/24.29 (\<lambda>x. _) % 36.48/24.29 (i1 := (\<lambda>x. _)(i1 := False, i2 := False), % 36.48/24.29 i2 := (\<lambda>x. _)(i1 := False, i2 := True)) % 36.48/24.29 bnd_pulignymontrachet = i2 % 36.48/24.29 bnd_pulignymontrachetwhiteburgundy = i2 % 36.48/24.29 bnd_q0 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q1 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q10 = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_q11 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q12 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q13 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q14 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q15 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q16 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q17 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q18 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q19 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q2 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q20 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q21 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q22 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q23 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q24 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q26 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q27 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q29 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q3 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q30 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q31 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q32 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q33 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q34 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q35 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q36 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q37 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q38 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q39 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q4 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q40 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q41 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q42 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q43 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q44 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q45 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q46 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q47 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q48 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q49 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q5 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q50 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q51 = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_q52 = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_q55 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q56 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q57 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q58 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q59 = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_q6 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q60 = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_q61 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q62 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q63 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q64 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q65 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q66 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q67 = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_q68 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q69 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q7 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q70 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q71 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q72 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q73 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q74 = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_q9 = (\<lambda>x. _)(i1 := True, i2 := False) % 36.48/24.29 bnd_red = i2 % 36.48/24.29 bnd_redbordeaux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_redburgundy = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_redtablewine = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_redtablewine_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_redwine = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_region = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_region_aux = (\<lambda>x. _)(i1 := True, i2 := True) % 36.48/24.29 bnd_riesling = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_riesling_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_rieslinggrape = i2 % 36.48/24.29 bnd_rose = i2 % 36.48/24.29 bnd_rosedanjou = i2 % 36.48/24.29 bnd_rosewine = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_sancerre = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_sancerre_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_sancerreregion = i1 % 36.48/24.29 bnd_sangiovesegrape = i2 % 36.48/24.29 bnd_santabarbararegion = i2 % 36.48/24.29 bnd_santacruzmountainsregion = i2 % 36.48/24.29 bnd_santacruzmountainvineyard = i2 % 36.48/24.29 bnd_santacruzmountainvineyardcabernetsauvignon = i2 % 36.48/24.29 bnd_saucelitocanyon = i2 % 36.48/24.29 bnd_saucelitocanyonzinfandel = i2 % 36.48/24.29 bnd_saucelitocanyonzinfandel1998 = i2 % 36.48/24.29 bnd_sauterneregion = i1 % 36.48/24.29 bnd_sauternes = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_sauternes_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_sauvignonblanc = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_sauvignonblanc_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_sauvignonblancgrape = i2 % 36.48/24.29 bnd_schlossrothermel = i2 % 36.48/24.29 bnd_schlossrothermeltrochenbierenausleseriesling = i2 % 36.48/24.29 bnd_schlossvolrad = i2 % 36.48/24.29 bnd_schlossvolradtrochenbierenausleseriesling = i2 % 36.48/24.29 bnd_seanthackrey = i2 % 36.48/24.29 bnd_seanthackreysiriuspetitesyrah = i2 % 36.48/24.29 bnd_selaks = i2 % 36.48/24.29 bnd_selaksicewine = i2 % 36.48/24.29 bnd_selakssauvignonblanc = i2 % 36.48/24.29 bnd_semillon = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_semillon_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_semillongrape = i2 % 36.48/24.29 bnd_semillonorsauvignonblanc = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_sevreetmaine = i2 % 36.48/24.29 bnd_sevreetmainemuscadet = i2 % 36.48/24.29 bnd_sonomaregion = i2 % 36.48/24.29 bnd_southaustraliaregion = i2 % 36.48/24.29 bnd_stemilion = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_stemilion_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_stemilionregion = i1 % 36.48/24.29 bnd_stgenevieve = i2 % 36.48/24.29 bnd_stgenevievetexaswhite = i2 % 36.48/24.29 bnd_stonleigh = i2 % 36.48/24.29 bnd_stonleighsauvignonblanc = i2 % 36.48/24.29 bnd_strong = i2 % 36.48/24.29 bnd_sweet = i2 % 36.48/24.29 bnd_sweetriesling = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_sweetriesling_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_sweetwine = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_tablewine = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_taylor = i2 % 36.48/24.29 bnd_taylorport = i2 % 36.48/24.29 bnd_texasregion = i2 % 36.48/24.29 bnd_texaswine = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_tours = (\<lambda>x. _)(i1 := False, i2 := False) % 36.48/24.29 bnd_toursregion = i1 % 36.48/24.29 bnd_usregion = i2 % 36.48/24.29 bnd_ventana = i2 % 36.48/24.29 bnd_ventanacheninblanc = i2 % 36.48/24.29 bnd_vintage = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_vintageyear = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_vintageyear_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_white = i2 % 36.48/24.29 bnd_whitebordeaux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_whiteburgundy = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_whiteburgundy_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_whitehalllane = i2 % 36.48/24.29 bnd_whitehalllanecabernetfranc = i2 % 36.48/24.29 bnd_whitehalllaneprimavera = i2 % 36.48/24.29 bnd_whiteloire = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_whitenonsweetwine = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_whitetablewine = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_whitewine = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_whitewine_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_wine = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_winebody = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_winebody_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_winecolor = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_winecolor_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_winedescriptor = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_wineflavor = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_wineflavor_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_winegrape = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_winegrape_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_winery = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_winery_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_winesugar = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_winesugar_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_winetaste = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_year1998 = i2 % 36.48/24.29 bnd_zinfandel = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_zinfandel_aux = (\<lambda>x. _)(i1 := False, i2 := True) % 36.48/24.29 bnd_zinfandelgrape = i2 % 36.48/24.29 % SZS output end FiniteModel % 36.48/24.29 Total time: 12.5 s %------------------------------------------------------------------------------