drinks.csv

vodka_martini,vodka,dry_vermouth,lemon,olive
mimosa,champagne,orange_juice,orange
martini,gin,dry_vermouth,lemon
margarita,tequila,triple_sec,lime_juice,salt
grasshopper,white_creme_de_cacao,green_creme_de_menthe,cream,mint
ve_n_to,grappa,lemon_juice,honey_syrup,chamomile_syrup,honey_syrup,egg_white,lemon,white_grape
boulevardier,bourbon_whiskey,sweet_red_vermouth,campari,orange,lemon
bee_s_nees,london_dry_gin,honey_syrup,lemon_juice,orange_juice,orange
southside,london_dry_gin,lemon_juice,simple_syrup,mint,egg_white
whiskey_sour,bourbon_whiskey,lemon_juice,simple_syrup,egg_white,cherry,orange
champagne_cocktail,champagne,cognac,angostura_bitters,sugar,grand_marnier,orange,cherry
suffering_bastard,brandy,gin,lime_juice,angostura_bitters,ginger_beer,mint,orange
illegal,mezcal,overproof_white_rum,lime_juice,falernum,simple_syrup,maraschino,egg_white
toronto,canadian_whiskey,fernet_branca,sugar,angostura_bitters,orange
french_75,gin,simple_syrup,lemon_juice,champagne
cuba_libre,cola,white_rum,lime_juice,lime
moscow_mule,vodka,ginger_beer,lime_juice,lime
bellini,prosecco,peach_puree
black_russian,vodka,coffee_liqueur
caipirinha,cachaca,lime,cane_sugar
mojito,white_rum,lime_juice,mint,cane_sugar,lemon,soda_water
dark__n__stormy,dark_rum,ginger_beer,lime
bramble,gin,lemon_juice,simple_syrup,creme_de_mure,lemon,blackberry
french_martini,vodka,raspberry_liqueur,pineapple_juice,lemon
kamikaze,vodka,triple_sec,lime_juice,lime
lemon_drop_martini,vodka,triple_sec,lemon_juice,sugar,lime
vesper,gin,vodka,lillet_blanc,lemon
alexander,cognac,brown_creme_de_cacao,light_cream,nutmeg
americano,campari,sweet_red_vermouth,soda_water,orange,lemon
angel_face,gin,apricot_brandy,calvados
aviation,gin,lemon_juice,maraschino,creme_de_violette,cherry
bacardi_cocktail,white_rum,lime_juice,grenadine
between_the_sheets,white_rum,cognac,triple_sec,lemon_juice
casino,old_tom_gin,maraschino,orange_bitters,lemon_juice,lemon,cherry
clover_club,gin,lemon_juice,raspberry_syrup,egg_white,raspberry
daiquiri,white_rum,lemon_juice,simple_syrup
derby,gin,peach_bitters,mint
dry_martini,gin,dry_vermouth,lemon,olive
gin_fizz,gin,lemon_juice,simple_syrup,soda_water,lemon
john_collins,gin,lemon_juice,simple_syrup,soda_water,angostura_bitters,lemon,cherry
manhattan,rye_whiskey,sweet_red_vermouth,angostura_bitters,cherry
mary_pickford,white_rum,pineapple_juice,grenadine,maraschino
monkey_gland,gin,orange_juice,absinthe,grenadine
negroni,gin,sweet_red_vermouth,campari,orange
old_fashioned,whiskey,angostura_bitters,sugar,water,orange,cherry
paradise,gin,apricot_brandy,orange_juice
planter_s_punch,dark_rum,orange_juice,pineapple_juice,lemon_juice,grenadine,simple_syrup,angostura_bitters,cherry,pineapple
porto_flip,brandy,port,egg_yolk,nutmeg
ramos_fizz,gin,cream,simple_syrup,lime_juice,lemon_juice,egg_white,orange_flower_water,vanilla_extract,soda_water
rusty_nail,scotch_whiskey,drambuie,lemon
sazerac,cognac,absinthe,sugar,peychaud_s_bitters,lemon
screwdriver,vodka,orange_juice,orange
sidecar,cognac,triple_sec,lemon_juice
stinger,cognac,white_creme_de_menthe
tuxedo,old_tom_gin,dry_vermouth,maraschino,absinthe,orange_bitters,cherry,lemon
white_lady,gin,triple_sec,lemon_juice
french_connection,cognac,amaretto
mint_julep,bourbon_whiskey,mint,water,powdered_sugar
white_russian,vodka,coffee_liqueur,cream
bloody_mary,vodka,tomato_juice,lemon_juice,worcestershire_sauce,tabasco,celery_salt,pepper,celery,lemon
kir,dry_white_wine,creme_de_cassis
kir_royal,champagne,creme_de_cassis
long_island_iced_tea,vodka,tequila,white_rum,gin,cointreau,lemon_juice,simple_syrup,cola,lemon
mai-tai,white_rum,dark_rum,curacao,orgeat__almond__syrup,lime_juice,simple_syrup,pineapple,mint,lime
tommy_s_margarita,tequila,lime_juice,agave_nectar
b52,coffee_liqueur,triple_sec,irish_cream_liqueur
barracuda,gold_rum,galliano,pineapple_juice,lime_juice,prosecco
corpse_reviver_N2,gin,cointreau,lillet_blanc,lemon_juice,absinthe,orange
cosmopolitan,vodka,cointreau,lime_juice,cranberry_juice,lemon
dirty_martini,vodka,dry_vermouth,olive_juice,olive
espresso_martini,vodka,coffee_liqueur,simple_syrup,espresso
golden_dream,triple_sec,galliano,orange_juice,cream
hemingway_special,white_rum,grapefruit_juice,maraschino,lime_juice
horse_s_neck,cognac,ginger_ale,angostura_bitters,lemon
irish_coffee,irish_whiskey,coffee,cream,sugar
tom_collins,old_tom_gin,lemon_juice,simple_syrup,soda_water,angostura_bitters,lemon,cherry
pina_colada,white_rum,coconut_cream,pineapple_juice,pineapple,cherry
pisco_sour,pisco,simple_syrup,lemon_juice,egg_white,angostura_bitters
russian_spring_punch,vodka,lemon_juice,creme_de_cassis,simple_syrup,sparkling_wine,lemon,blackberry
sea_breeze,vodka,cranberry_juice,grapefruit_juice,orange,cherry
sex_on_the_beach,vodka,peach_schnapps,orange_juice,cranberry_juice,grapefruit_juice,orange
singapore_sling,gin,cherry_liqueur,cointreau,dom_benedictine,pineapple_juice,lime_juice,grenadine,angostura_bitters,cherry,pineapple
tequila_sunrise,tequila,orange_juice,grenadine,orange
yellow_bird,white_rum,galliano,triple_sec,lime_juice
zombie,dark_rum,gold_rum,demerara_rum,lime_juice,falernum,grapefruit_juice,cinnamon_syrup,grenadine,angostura_bitters,absinthe,mint
brandy_crusta,brandy,lemon_juice,maraschino,curacao,simple_syrup,aromatic_bitters,orange,powdered_sugar
hanky_panky,london_dry_gin,sweet_red_vermouth,fernet_branca,orange
last_word,gin,green_chartreuse,maraschino,lime_juice
martinez,london_dry_gin,sweet_red_vermouth,maraschino,orange_bitters,lemon
vieux_carre,rye_whiskey,cognac,sweet_red_vermouth,dom_benedictine,peychaud_s_bitters,orange,cherry
cachanchara,cuban_aguardiente,lemon_juice,honey,water,lime
fernandito,fernet_branca,cola
old_cuban,rum,sparkling_wine,lime_juice,simple_syrup,angostura_bitters,mint
paloma,tequila,grapefruit_soda,lime_juice,salt,lime
paper_plane,bourbon_whiskey,amaro_nonino,aperol,lemon_juice
penicillin,blended_scotch_whiskey,islay_single_malt_scotch_whiskey,lemon_juice,honey_syrup,ginger,candied_ginger
spicy_fifty,vodka,elderflower_syrup,lemon_juice,honey_syrup,vanilla_extract,red_chili_pepper
tipperary,irish_whiskey,sweet_red_vermouth,green_chartreuse,angostura_bitters,orange
trinidad_sour,angostura_bitters,orgeat__almond__syrup,lemon_juice,rye_whiskey
naked_and_famous,mezcal,yellow_chartreuse,aperol,lime_juice
new_york_sour,rye_whiskey,lemon_juice,egg_white,simple_syrup,red_wine,lemon,cherry
spritz,prosecco,aperol,soda_water,orange
gimlet,lime_juice,simple_syrup,gin
n20th_century,gin,lemon_juice,white_creme_de_cacao,kina_lillet,lemon

drinks.rb

require "csv"
require "set"

data = CSV.read("#{__dir__}/drinks.csv", headers: false)

ingredients = Set.new

data.each do |recipe|
  recipe.delete_if { |x| x == nil || x == "" }
  recipe.each_with_index do |d,i|
    recipe[i] = "#{i == 0 ? "cok_" : "ing_"}#{recipe[i]}"
  end

  puts "(declare-const #{recipe[0]} Int)"
  puts "(declare-const #{recipe[0]}__r Real)"

  recipe[1..-1].each do |ing|
    ingredients << ing
  end
end

ingredients.each do |ing|
  puts "(declare-const #{ing} Int)"
end

puts "(assert (and "
data.each do |recipe|
  puts "  (>= #{recipe[0]} 0) (<= #{recipe[0]} 1)"
  puts "  (>= #{recipe[0]}__r 0) (< #{recipe[0]}__r 1)"
end
puts "))"

puts "(assert (and "
ingredients.each do |ing|
  puts "  (>= #{ing} 0) (<= #{ing} 1)"
end
puts "))"


data.each do |recipe|
  print "(assert (= (+ "
  print recipe[1..-1].join(" ")
  print " ) (* "
  print (recipe.size - 1)
  print "  (+ #{recipe[0]} #{recipe[0]}__r)"
  puts ")))"
end


puts "(assert (= 5 (+ "
puts ingredients.to_a.join(" ")
puts ")))"

puts "(maximize (+ "
print "  "
data.each do |recipe|
  print recipe[0]
  print " "
end
puts "))"

puts "(check-sat)"
puts "(get-model)"

drinks.z3

(declare-const cok_vodka_martini Int)
(declare-const cok_vodka_martini__r Real)
(declare-const cok_mimosa Int)
(declare-const cok_mimosa__r Real)
(declare-const cok_martini Int)
(declare-const cok_martini__r Real)
(declare-const cok_margarita Int)
(declare-const cok_margarita__r Real)
(declare-const cok_grasshopper Int)
(declare-const cok_grasshopper__r Real)
(declare-const cok_ve_n_to Int)
(declare-const cok_ve_n_to__r Real)
(declare-const cok_boulevardier Int)
(declare-const cok_boulevardier__r Real)
(declare-const cok_bee_s_nees Int)
(declare-const cok_bee_s_nees__r Real)
(declare-const cok_southside Int)
(declare-const cok_southside__r Real)
(declare-const cok_whiskey_sour Int)
(declare-const cok_whiskey_sour__r Real)
(declare-const cok_champagne_cocktail Int)
(declare-const cok_champagne_cocktail__r Real)
(declare-const cok_suffering_bastard Int)
(declare-const cok_suffering_bastard__r Real)
(declare-const cok_illegal Int)
(declare-const cok_illegal__r Real)
(declare-const cok_toronto Int)
(declare-const cok_toronto__r Real)
(declare-const cok_french_75 Int)
(declare-const cok_french_75__r Real)
(declare-const cok_cuba_libre Int)
(declare-const cok_cuba_libre__r Real)
(declare-const cok_moscow_mule Int)
(declare-const cok_moscow_mule__r Real)
(declare-const cok_bellini Int)
(declare-const cok_bellini__r Real)
(declare-const cok_black_russian Int)
(declare-const cok_black_russian__r Real)
(declare-const cok_caipirinha Int)
(declare-const cok_caipirinha__r Real)
(declare-const cok_mojito Int)
(declare-const cok_mojito__r Real)
(declare-const cok_dark__n__stormy Int)
(declare-const cok_dark__n__stormy__r Real)
(declare-const cok_bramble Int)
(declare-const cok_bramble__r Real)
(declare-const cok_french_martini Int)
(declare-const cok_french_martini__r Real)
(declare-const cok_kamikaze Int)
(declare-const cok_kamikaze__r Real)
(declare-const cok_lemon_drop_martini Int)
(declare-const cok_lemon_drop_martini__r Real)
(declare-const cok_vesper Int)
(declare-const cok_vesper__r Real)
(declare-const cok_alexander Int)
(declare-const cok_alexander__r Real)
(declare-const cok_americano Int)
(declare-const cok_americano__r Real)
(declare-const cok_angel_face Int)
(declare-const cok_angel_face__r Real)
(declare-const cok_aviation Int)
(declare-const cok_aviation__r Real)
(declare-const cok_bacardi_cocktail Int)
(declare-const cok_bacardi_cocktail__r Real)
(declare-const cok_between_the_sheets Int)
(declare-const cok_between_the_sheets__r Real)
(declare-const cok_casino Int)
(declare-const cok_casino__r Real)
(declare-const cok_clover_club Int)
(declare-const cok_clover_club__r Real)
(declare-const cok_daiquiri Int)
(declare-const cok_daiquiri__r Real)
(declare-const cok_derby Int)
(declare-const cok_derby__r Real)
(declare-const cok_dry_martini Int)
(declare-const cok_dry_martini__r Real)
(declare-const cok_gin_fizz Int)
(declare-const cok_gin_fizz__r Real)
(declare-const cok_john_collins Int)
(declare-const cok_john_collins__r Real)
(declare-const cok_manhattan Int)
(declare-const cok_manhattan__r Real)
(declare-const cok_mary_pickford Int)
(declare-const cok_mary_pickford__r Real)
(declare-const cok_monkey_gland Int)
(declare-const cok_monkey_gland__r Real)
(declare-const cok_negroni Int)
(declare-const cok_negroni__r Real)
(declare-const cok_old_fashioned Int)
(declare-const cok_old_fashioned__r Real)
(declare-const cok_paradise Int)
(declare-const cok_paradise__r Real)
(declare-const cok_planter_s_punch Int)
(declare-const cok_planter_s_punch__r Real)
(declare-const cok_porto_flip Int)
(declare-const cok_porto_flip__r Real)
(declare-const cok_ramos_fizz Int)
(declare-const cok_ramos_fizz__r Real)
(declare-const cok_rusty_nail Int)
(declare-const cok_rusty_nail__r Real)
(declare-const cok_sazerac Int)
(declare-const cok_sazerac__r Real)
(declare-const cok_screwdriver Int)
(declare-const cok_screwdriver__r Real)
(declare-const cok_sidecar Int)
(declare-const cok_sidecar__r Real)
(declare-const cok_stinger Int)
(declare-const cok_stinger__r Real)
(declare-const cok_tuxedo Int)
(declare-const cok_tuxedo__r Real)
(declare-const cok_white_lady Int)
(declare-const cok_white_lady__r Real)
(declare-const cok_french_connection Int)
(declare-const cok_french_connection__r Real)
(declare-const cok_mint_julep Int)
(declare-const cok_mint_julep__r Real)
(declare-const cok_white_russian Int)
(declare-const cok_white_russian__r Real)
(declare-const cok_bloody_mary Int)
(declare-const cok_bloody_mary__r Real)
(declare-const cok_kir Int)
(declare-const cok_kir__r Real)
(declare-const cok_kir_royal Int)
(declare-const cok_kir_royal__r Real)
(declare-const cok_long_island_iced_tea Int)
(declare-const cok_long_island_iced_tea__r Real)
(declare-const cok_mai-tai Int)
(declare-const cok_mai-tai__r Real)
(declare-const cok_tommy_s_margarita Int)
(declare-const cok_tommy_s_margarita__r Real)
(declare-const cok_b52 Int)
(declare-const cok_b52__r Real)
(declare-const cok_barracuda Int)
(declare-const cok_barracuda__r Real)
(declare-const cok_corpse_reviver_N2 Int)
(declare-const cok_corpse_reviver_N2__r Real)
(declare-const cok_cosmopolitan Int)
(declare-const cok_cosmopolitan__r Real)
(declare-const cok_dirty_martini Int)
(declare-const cok_dirty_martini__r Real)
(declare-const cok_espresso_martini Int)
(declare-const cok_espresso_martini__r Real)
(declare-const cok_golden_dream Int)
(declare-const cok_golden_dream__r Real)
(declare-const cok_hemingway_special Int)
(declare-const cok_hemingway_special__r Real)
(declare-const cok_horse_s_neck Int)
(declare-const cok_horse_s_neck__r Real)
(declare-const cok_irish_coffee Int)
(declare-const cok_irish_coffee__r Real)
(declare-const cok_tom_collins Int)
(declare-const cok_tom_collins__r Real)
(declare-const cok_pina_colada Int)
(declare-const cok_pina_colada__r Real)
(declare-const cok_pisco_sour Int)
(declare-const cok_pisco_sour__r Real)
(declare-const cok_russian_spring_punch Int)
(declare-const cok_russian_spring_punch__r Real)
(declare-const cok_sea_breeze Int)
(declare-const cok_sea_breeze__r Real)
(declare-const cok_sex_on_the_beach Int)
(declare-const cok_sex_on_the_beach__r Real)
(declare-const cok_singapore_sling Int)
(declare-const cok_singapore_sling__r Real)
(declare-const cok_tequila_sunrise Int)
(declare-const cok_tequila_sunrise__r Real)
(declare-const cok_yellow_bird Int)
(declare-const cok_yellow_bird__r Real)
(declare-const cok_zombie Int)
(declare-const cok_zombie__r Real)
(declare-const cok_brandy_crusta Int)
(declare-const cok_brandy_crusta__r Real)
(declare-const cok_hanky_panky Int)
(declare-const cok_hanky_panky__r Real)
(declare-const cok_last_word Int)
(declare-const cok_last_word__r Real)
(declare-const cok_martinez Int)
(declare-const cok_martinez__r Real)
(declare-const cok_vieux_carre Int)
(declare-const cok_vieux_carre__r Real)
(declare-const cok_cachanchara Int)
(declare-const cok_cachanchara__r Real)
(declare-const cok_fernandito Int)
(declare-const cok_fernandito__r Real)
(declare-const cok_old_cuban Int)
(declare-const cok_old_cuban__r Real)
(declare-const cok_paloma Int)
(declare-const cok_paloma__r Real)
(declare-const cok_paper_plane Int)
(declare-const cok_paper_plane__r Real)
(declare-const cok_penicillin Int)
(declare-const cok_penicillin__r Real)
(declare-const cok_spicy_fifty Int)
(declare-const cok_spicy_fifty__r Real)
(declare-const cok_tipperary Int)
(declare-const cok_tipperary__r Real)
(declare-const cok_trinidad_sour Int)
(declare-const cok_trinidad_sour__r Real)
(declare-const cok_naked_and_famous Int)
(declare-const cok_naked_and_famous__r Real)
(declare-const cok_new_york_sour Int)
(declare-const cok_new_york_sour__r Real)
(declare-const cok_spritz Int)
(declare-const cok_spritz__r Real)
(declare-const cok_gimlet Int)
(declare-const cok_gimlet__r Real)
(declare-const cok_n20th_century Int)
(declare-const cok_n20th_century__r Real)
(declare-const ing_vodka Int)
(declare-const ing_dry_vermouth Int)
(declare-const ing_lemon Int)
(declare-const ing_olive Int)
(declare-const ing_champagne Int)
(declare-const ing_orange_juice Int)
(declare-const ing_orange Int)
(declare-const ing_gin Int)
(declare-const ing_tequila Int)
(declare-const ing_triple_sec Int)
(declare-const ing_lime_juice Int)
(declare-const ing_salt Int)
(declare-const ing_white_creme_de_cacao Int)
(declare-const ing_green_creme_de_menthe Int)
(declare-const ing_cream Int)
(declare-const ing_mint Int)
(declare-const ing_grappa Int)
(declare-const ing_lemon_juice Int)
(declare-const ing_honey_syrup Int)
(declare-const ing_chamomile_syrup Int)
(declare-const ing_egg_white Int)
(declare-const ing_white_grape Int)
(declare-const ing_bourbon_whiskey Int)
(declare-const ing_sweet_red_vermouth Int)
(declare-const ing_campari Int)
(declare-const ing_london_dry_gin Int)
(declare-const ing_simple_syrup Int)
(declare-const ing_cherry Int)
(declare-const ing_cognac Int)
(declare-const ing_angostura_bitters Int)
(declare-const ing_sugar Int)
(declare-const ing_grand_marnier Int)
(declare-const ing_brandy Int)
(declare-const ing_ginger_beer Int)
(declare-const ing_mezcal Int)
(declare-const ing_overproof_white_rum Int)
(declare-const ing_falernum Int)
(declare-const ing_maraschino Int)
(declare-const ing_canadian_whiskey Int)
(declare-const ing_fernet_branca Int)
(declare-const ing_cola Int)
(declare-const ing_white_rum Int)
(declare-const ing_lime Int)
(declare-const ing_prosecco Int)
(declare-const ing_peach_puree Int)
(declare-const ing_coffee_liqueur Int)
(declare-const ing_cachaca Int)
(declare-const ing_cane_sugar Int)
(declare-const ing_soda_water Int)
(declare-const ing_dark_rum Int)
(declare-const ing_creme_de_mure Int)
(declare-const ing_blackberry Int)
(declare-const ing_raspberry_liqueur Int)
(declare-const ing_pineapple_juice Int)
(declare-const ing_lillet_blanc Int)
(declare-const ing_brown_creme_de_cacao Int)
(declare-const ing_light_cream Int)
(declare-const ing_nutmeg Int)
(declare-const ing_apricot_brandy Int)
(declare-const ing_calvados Int)
(declare-const ing_creme_de_violette Int)
(declare-const ing_grenadine Int)
(declare-const ing_old_tom_gin Int)
(declare-const ing_orange_bitters Int)
(declare-const ing_raspberry_syrup Int)
(declare-const ing_raspberry Int)
(declare-const ing_peach_bitters Int)
(declare-const ing_rye_whiskey Int)
(declare-const ing_absinthe Int)
(declare-const ing_whiskey Int)
(declare-const ing_water Int)
(declare-const ing_pineapple Int)
(declare-const ing_port Int)
(declare-const ing_egg_yolk Int)
(declare-const ing_orange_flower_water Int)
(declare-const ing_vanilla_extract Int)
(declare-const ing_scotch_whiskey Int)
(declare-const ing_drambuie Int)
(declare-const ing_peychaud_s_bitters Int)
(declare-const ing_white_creme_de_menthe Int)
(declare-const ing_amaretto Int)
(declare-const ing_powdered_sugar Int)
(declare-const ing_tomato_juice Int)
(declare-const ing_worcestershire_sauce Int)
(declare-const ing_tabasco Int)
(declare-const ing_celery_salt Int)
(declare-const ing_pepper Int)
(declare-const ing_celery Int)
(declare-const ing_dry_white_wine Int)
(declare-const ing_creme_de_cassis Int)
(declare-const ing_cointreau Int)
(declare-const ing_curacao Int)
(declare-const ing_orgeat__almond__syrup Int)
(declare-const ing_agave_nectar Int)
(declare-const ing_irish_cream_liqueur Int)
(declare-const ing_gold_rum Int)
(declare-const ing_galliano Int)
(declare-const ing_cranberry_juice Int)
(declare-const ing_olive_juice Int)
(declare-const ing_espresso Int)
(declare-const ing_grapefruit_juice Int)
(declare-const ing_ginger_ale Int)
(declare-const ing_irish_whiskey Int)
(declare-const ing_coffee Int)
(declare-const ing_coconut_cream Int)
(declare-const ing_pisco Int)
(declare-const ing_sparkling_wine Int)
(declare-const ing_peach_schnapps Int)
(declare-const ing_cherry_liqueur Int)
(declare-const ing_dom_benedictine Int)
(declare-const ing_demerara_rum Int)
(declare-const ing_cinnamon_syrup Int)
(declare-const ing_aromatic_bitters Int)
(declare-const ing_green_chartreuse Int)
(declare-const ing_cuban_aguardiente Int)
(declare-const ing_honey Int)
(declare-const ing_rum Int)
(declare-const ing_grapefruit_soda Int)
(declare-const ing_amaro_nonino Int)
(declare-const ing_aperol Int)
(declare-const ing_blended_scotch_whiskey Int)
(declare-const ing_islay_single_malt_scotch_whiskey Int)
(declare-const ing_ginger Int)
(declare-const ing_candied_ginger Int)
(declare-const ing_elderflower_syrup Int)
(declare-const ing_red_chili_pepper Int)
(declare-const ing_yellow_chartreuse Int)
(declare-const ing_red_wine Int)
(declare-const ing_kina_lillet Int)
(assert (and
  (>= cok_vodka_martini 0) (<= cok_vodka_martini 1)
  (>= cok_vodka_martini__r 0) (< cok_vodka_martini__r 1)
  (>= cok_mimosa 0) (<= cok_mimosa 1)
  (>= cok_mimosa__r 0) (< cok_mimosa__r 1)
  (>= cok_martini 0) (<= cok_martini 1)
  (>= cok_martini__r 0) (< cok_martini__r 1)
  (>= cok_margarita 0) (<= cok_margarita 1)
  (>= cok_margarita__r 0) (< cok_margarita__r 1)
  (>= cok_grasshopper 0) (<= cok_grasshopper 1)
  (>= cok_grasshopper__r 0) (< cok_grasshopper__r 1)
  (>= cok_ve_n_to 0) (<= cok_ve_n_to 1)
  (>= cok_ve_n_to__r 0) (< cok_ve_n_to__r 1)
  (>= cok_boulevardier 0) (<= cok_boulevardier 1)
  (>= cok_boulevardier__r 0) (< cok_boulevardier__r 1)
  (>= cok_bee_s_nees 0) (<= cok_bee_s_nees 1)
  (>= cok_bee_s_nees__r 0) (< cok_bee_s_nees__r 1)
  (>= cok_southside 0) (<= cok_southside 1)
  (>= cok_southside__r 0) (< cok_southside__r 1)
  (>= cok_whiskey_sour 0) (<= cok_whiskey_sour 1)
  (>= cok_whiskey_sour__r 0) (< cok_whiskey_sour__r 1)
  (>= cok_champagne_cocktail 0) (<= cok_champagne_cocktail 1)
  (>= cok_champagne_cocktail__r 0) (< cok_champagne_cocktail__r 1)
  (>= cok_suffering_bastard 0) (<= cok_suffering_bastard 1)
  (>= cok_suffering_bastard__r 0) (< cok_suffering_bastard__r 1)
  (>= cok_illegal 0) (<= cok_illegal 1)
  (>= cok_illegal__r 0) (< cok_illegal__r 1)
  (>= cok_toronto 0) (<= cok_toronto 1)
  (>= cok_toronto__r 0) (< cok_toronto__r 1)
  (>= cok_french_75 0) (<= cok_french_75 1)
  (>= cok_french_75__r 0) (< cok_french_75__r 1)
  (>= cok_cuba_libre 0) (<= cok_cuba_libre 1)
  (>= cok_cuba_libre__r 0) (< cok_cuba_libre__r 1)
  (>= cok_moscow_mule 0) (<= cok_moscow_mule 1)
  (>= cok_moscow_mule__r 0) (< cok_moscow_mule__r 1)
  (>= cok_bellini 0) (<= cok_bellini 1)
  (>= cok_bellini__r 0) (< cok_bellini__r 1)
  (>= cok_black_russian 0) (<= cok_black_russian 1)
  (>= cok_black_russian__r 0) (< cok_black_russian__r 1)
  (>= cok_caipirinha 0) (<= cok_caipirinha 1)
  (>= cok_caipirinha__r 0) (< cok_caipirinha__r 1)
  (>= cok_mojito 0) (<= cok_mojito 1)
  (>= cok_mojito__r 0) (< cok_mojito__r 1)
  (>= cok_dark__n__stormy 0) (<= cok_dark__n__stormy 1)
  (>= cok_dark__n__stormy__r 0) (< cok_dark__n__stormy__r 1)
  (>= cok_bramble 0) (<= cok_bramble 1)
  (>= cok_bramble__r 0) (< cok_bramble__r 1)
  (>= cok_french_martini 0) (<= cok_french_martini 1)
  (>= cok_french_martini__r 0) (< cok_french_martini__r 1)
  (>= cok_kamikaze 0) (<= cok_kamikaze 1)
  (>= cok_kamikaze__r 0) (< cok_kamikaze__r 1)
  (>= cok_lemon_drop_martini 0) (<= cok_lemon_drop_martini 1)
  (>= cok_lemon_drop_martini__r 0) (< cok_lemon_drop_martini__r 1)
  (>= cok_vesper 0) (<= cok_vesper 1)
  (>= cok_vesper__r 0) (< cok_vesper__r 1)
  (>= cok_alexander 0) (<= cok_alexander 1)
  (>= cok_alexander__r 0) (< cok_alexander__r 1)
  (>= cok_americano 0) (<= cok_americano 1)
  (>= cok_americano__r 0) (< cok_americano__r 1)
  (>= cok_angel_face 0) (<= cok_angel_face 1)
  (>= cok_angel_face__r 0) (< cok_angel_face__r 1)
  (>= cok_aviation 0) (<= cok_aviation 1)
  (>= cok_aviation__r 0) (< cok_aviation__r 1)
  (>= cok_bacardi_cocktail 0) (<= cok_bacardi_cocktail 1)
  (>= cok_bacardi_cocktail__r 0) (< cok_bacardi_cocktail__r 1)
  (>= cok_between_the_sheets 0) (<= cok_between_the_sheets 1)
  (>= cok_between_the_sheets__r 0) (< cok_between_the_sheets__r 1)
  (>= cok_casino 0) (<= cok_casino 1)
  (>= cok_casino__r 0) (< cok_casino__r 1)
  (>= cok_clover_club 0) (<= cok_clover_club 1)
  (>= cok_clover_club__r 0) (< cok_clover_club__r 1)
  (>= cok_daiquiri 0) (<= cok_daiquiri 1)
  (>= cok_daiquiri__r 0) (< cok_daiquiri__r 1)
  (>= cok_derby 0) (<= cok_derby 1)
  (>= cok_derby__r 0) (< cok_derby__r 1)
  (>= cok_dry_martini 0) (<= cok_dry_martini 1)
  (>= cok_dry_martini__r 0) (< cok_dry_martini__r 1)
  (>= cok_gin_fizz 0) (<= cok_gin_fizz 1)
  (>= cok_gin_fizz__r 0) (< cok_gin_fizz__r 1)
  (>= cok_john_collins 0) (<= cok_john_collins 1)
  (>= cok_john_collins__r 0) (< cok_john_collins__r 1)
  (>= cok_manhattan 0) (<= cok_manhattan 1)
  (>= cok_manhattan__r 0) (< cok_manhattan__r 1)
  (>= cok_mary_pickford 0) (<= cok_mary_pickford 1)
  (>= cok_mary_pickford__r 0) (< cok_mary_pickford__r 1)
  (>= cok_monkey_gland 0) (<= cok_monkey_gland 1)
  (>= cok_monkey_gland__r 0) (< cok_monkey_gland__r 1)
  (>= cok_negroni 0) (<= cok_negroni 1)
  (>= cok_negroni__r 0) (< cok_negroni__r 1)
  (>= cok_old_fashioned 0) (<= cok_old_fashioned 1)
  (>= cok_old_fashioned__r 0) (< cok_old_fashioned__r 1)
  (>= cok_paradise 0) (<= cok_paradise 1)
  (>= cok_paradise__r 0) (< cok_paradise__r 1)
  (>= cok_planter_s_punch 0) (<= cok_planter_s_punch 1)
  (>= cok_planter_s_punch__r 0) (< cok_planter_s_punch__r 1)
  (>= cok_porto_flip 0) (<= cok_porto_flip 1)
  (>= cok_porto_flip__r 0) (< cok_porto_flip__r 1)
  (>= cok_ramos_fizz 0) (<= cok_ramos_fizz 1)
  (>= cok_ramos_fizz__r 0) (< cok_ramos_fizz__r 1)
  (>= cok_rusty_nail 0) (<= cok_rusty_nail 1)
  (>= cok_rusty_nail__r 0) (< cok_rusty_nail__r 1)
  (>= cok_sazerac 0) (<= cok_sazerac 1)
  (>= cok_sazerac__r 0) (< cok_sazerac__r 1)
  (>= cok_screwdriver 0) (<= cok_screwdriver 1)
  (>= cok_screwdriver__r 0) (< cok_screwdriver__r 1)
  (>= cok_sidecar 0) (<= cok_sidecar 1)
  (>= cok_sidecar__r 0) (< cok_sidecar__r 1)
  (>= cok_stinger 0) (<= cok_stinger 1)
  (>= cok_stinger__r 0) (< cok_stinger__r 1)
  (>= cok_tuxedo 0) (<= cok_tuxedo 1)
  (>= cok_tuxedo__r 0) (< cok_tuxedo__r 1)
  (>= cok_white_lady 0) (<= cok_white_lady 1)
  (>= cok_white_lady__r 0) (< cok_white_lady__r 1)
  (>= cok_french_connection 0) (<= cok_french_connection 1)
  (>= cok_french_connection__r 0) (< cok_french_connection__r 1)
  (>= cok_mint_julep 0) (<= cok_mint_julep 1)
  (>= cok_mint_julep__r 0) (< cok_mint_julep__r 1)
  (>= cok_white_russian 0) (<= cok_white_russian 1)
  (>= cok_white_russian__r 0) (< cok_white_russian__r 1)
  (>= cok_bloody_mary 0) (<= cok_bloody_mary 1)
  (>= cok_bloody_mary__r 0) (< cok_bloody_mary__r 1)
  (>= cok_kir 0) (<= cok_kir 1)
  (>= cok_kir__r 0) (< cok_kir__r 1)
  (>= cok_kir_royal 0) (<= cok_kir_royal 1)
  (>= cok_kir_royal__r 0) (< cok_kir_royal__r 1)
  (>= cok_long_island_iced_tea 0) (<= cok_long_island_iced_tea 1)
  (>= cok_long_island_iced_tea__r 0) (< cok_long_island_iced_tea__r 1)
  (>= cok_mai-tai 0) (<= cok_mai-tai 1)
  (>= cok_mai-tai__r 0) (< cok_mai-tai__r 1)
  (>= cok_tommy_s_margarita 0) (<= cok_tommy_s_margarita 1)
  (>= cok_tommy_s_margarita__r 0) (< cok_tommy_s_margarita__r 1)
  (>= cok_b52 0) (<= cok_b52 1)
  (>= cok_b52__r 0) (< cok_b52__r 1)
  (>= cok_barracuda 0) (<= cok_barracuda 1)
  (>= cok_barracuda__r 0) (< cok_barracuda__r 1)
  (>= cok_corpse_reviver_N2 0) (<= cok_corpse_reviver_N2 1)
  (>= cok_corpse_reviver_N2__r 0) (< cok_corpse_reviver_N2__r 1)
  (>= cok_cosmopolitan 0) (<= cok_cosmopolitan 1)
  (>= cok_cosmopolitan__r 0) (< cok_cosmopolitan__r 1)
  (>= cok_dirty_martini 0) (<= cok_dirty_martini 1)
  (>= cok_dirty_martini__r 0) (< cok_dirty_martini__r 1)
  (>= cok_espresso_martini 0) (<= cok_espresso_martini 1)
  (>= cok_espresso_martini__r 0) (< cok_espresso_martini__r 1)
  (>= cok_golden_dream 0) (<= cok_golden_dream 1)
  (>= cok_golden_dream__r 0) (< cok_golden_dream__r 1)
  (>= cok_hemingway_special 0) (<= cok_hemingway_special 1)
  (>= cok_hemingway_special__r 0) (< cok_hemingway_special__r 1)
  (>= cok_horse_s_neck 0) (<= cok_horse_s_neck 1)
  (>= cok_horse_s_neck__r 0) (< cok_horse_s_neck__r 1)
  (>= cok_irish_coffee 0) (<= cok_irish_coffee 1)
  (>= cok_irish_coffee__r 0) (< cok_irish_coffee__r 1)
  (>= cok_tom_collins 0) (<= cok_tom_collins 1)
  (>= cok_tom_collins__r 0) (< cok_tom_collins__r 1)
  (>= cok_pina_colada 0) (<= cok_pina_colada 1)
  (>= cok_pina_colada__r 0) (< cok_pina_colada__r 1)
  (>= cok_pisco_sour 0) (<= cok_pisco_sour 1)
  (>= cok_pisco_sour__r 0) (< cok_pisco_sour__r 1)
  (>= cok_russian_spring_punch 0) (<= cok_russian_spring_punch 1)
  (>= cok_russian_spring_punch__r 0) (< cok_russian_spring_punch__r 1)
  (>= cok_sea_breeze 0) (<= cok_sea_breeze 1)
  (>= cok_sea_breeze__r 0) (< cok_sea_breeze__r 1)
  (>= cok_sex_on_the_beach 0) (<= cok_sex_on_the_beach 1)
  (>= cok_sex_on_the_beach__r 0) (< cok_sex_on_the_beach__r 1)
  (>= cok_singapore_sling 0) (<= cok_singapore_sling 1)
  (>= cok_singapore_sling__r 0) (< cok_singapore_sling__r 1)
  (>= cok_tequila_sunrise 0) (<= cok_tequila_sunrise 1)
  (>= cok_tequila_sunrise__r 0) (< cok_tequila_sunrise__r 1)
  (>= cok_yellow_bird 0) (<= cok_yellow_bird 1)
  (>= cok_yellow_bird__r 0) (< cok_yellow_bird__r 1)
  (>= cok_zombie 0) (<= cok_zombie 1)
  (>= cok_zombie__r 0) (< cok_zombie__r 1)
  (>= cok_brandy_crusta 0) (<= cok_brandy_crusta 1)
  (>= cok_brandy_crusta__r 0) (< cok_brandy_crusta__r 1)
  (>= cok_hanky_panky 0) (<= cok_hanky_panky 1)
  (>= cok_hanky_panky__r 0) (< cok_hanky_panky__r 1)
  (>= cok_last_word 0) (<= cok_last_word 1)
  (>= cok_last_word__r 0) (< cok_last_word__r 1)
  (>= cok_martinez 0) (<= cok_martinez 1)
  (>= cok_martinez__r 0) (< cok_martinez__r 1)
  (>= cok_vieux_carre 0) (<= cok_vieux_carre 1)
  (>= cok_vieux_carre__r 0) (< cok_vieux_carre__r 1)
  (>= cok_cachanchara 0) (<= cok_cachanchara 1)
  (>= cok_cachanchara__r 0) (< cok_cachanchara__r 1)
  (>= cok_fernandito 0) (<= cok_fernandito 1)
  (>= cok_fernandito__r 0) (< cok_fernandito__r 1)
  (>= cok_old_cuban 0) (<= cok_old_cuban 1)
  (>= cok_old_cuban__r 0) (< cok_old_cuban__r 1)
  (>= cok_paloma 0) (<= cok_paloma 1)
  (>= cok_paloma__r 0) (< cok_paloma__r 1)
  (>= cok_paper_plane 0) (<= cok_paper_plane 1)
  (>= cok_paper_plane__r 0) (< cok_paper_plane__r 1)
  (>= cok_penicillin 0) (<= cok_penicillin 1)
  (>= cok_penicillin__r 0) (< cok_penicillin__r 1)
  (>= cok_spicy_fifty 0) (<= cok_spicy_fifty 1)
  (>= cok_spicy_fifty__r 0) (< cok_spicy_fifty__r 1)
  (>= cok_tipperary 0) (<= cok_tipperary 1)
  (>= cok_tipperary__r 0) (< cok_tipperary__r 1)
  (>= cok_trinidad_sour 0) (<= cok_trinidad_sour 1)
  (>= cok_trinidad_sour__r 0) (< cok_trinidad_sour__r 1)
  (>= cok_naked_and_famous 0) (<= cok_naked_and_famous 1)
  (>= cok_naked_and_famous__r 0) (< cok_naked_and_famous__r 1)
  (>= cok_new_york_sour 0) (<= cok_new_york_sour 1)
  (>= cok_new_york_sour__r 0) (< cok_new_york_sour__r 1)
  (>= cok_spritz 0) (<= cok_spritz 1)
  (>= cok_spritz__r 0) (< cok_spritz__r 1)
  (>= cok_gimlet 0) (<= cok_gimlet 1)
  (>= cok_gimlet__r 0) (< cok_gimlet__r 1)
  (>= cok_n20th_century 0) (<= cok_n20th_century 1)
  (>= cok_n20th_century__r 0) (< cok_n20th_century__r 1)
))
(assert (and
  (>= ing_vodka 0) (<= ing_vodka 1)
  (>= ing_dry_vermouth 0) (<= ing_dry_vermouth 1)
  (>= ing_lemon 0) (<= ing_lemon 1)
  (>= ing_olive 0) (<= ing_olive 1)
  (>= ing_champagne 0) (<= ing_champagne 1)
  (>= ing_orange_juice 0) (<= ing_orange_juice 1)
  (>= ing_orange 0) (<= ing_orange 1)
  (>= ing_gin 0) (<= ing_gin 1)
  (>= ing_tequila 0) (<= ing_tequila 1)
  (>= ing_triple_sec 0) (<= ing_triple_sec 1)
  (>= ing_lime_juice 0) (<= ing_lime_juice 1)
  (>= ing_salt 0) (<= ing_salt 1)
  (>= ing_white_creme_de_cacao 0) (<= ing_white_creme_de_cacao 1)
  (>= ing_green_creme_de_menthe 0) (<= ing_green_creme_de_menthe 1)
  (>= ing_cream 0) (<= ing_cream 1)
  (>= ing_mint 0) (<= ing_mint 1)
  (>= ing_grappa 0) (<= ing_grappa 1)
  (>= ing_lemon_juice 0) (<= ing_lemon_juice 1)
  (>= ing_honey_syrup 0) (<= ing_honey_syrup 1)
  (>= ing_chamomile_syrup 0) (<= ing_chamomile_syrup 1)
  (>= ing_egg_white 0) (<= ing_egg_white 1)
  (>= ing_white_grape 0) (<= ing_white_grape 1)
  (>= ing_bourbon_whiskey 0) (<= ing_bourbon_whiskey 1)
  (>= ing_sweet_red_vermouth 0) (<= ing_sweet_red_vermouth 1)
  (>= ing_campari 0) (<= ing_campari 1)
  (>= ing_london_dry_gin 0) (<= ing_london_dry_gin 1)
  (>= ing_simple_syrup 0) (<= ing_simple_syrup 1)
  (>= ing_cherry 0) (<= ing_cherry 1)
  (>= ing_cognac 0) (<= ing_cognac 1)
  (>= ing_angostura_bitters 0) (<= ing_angostura_bitters 1)
  (>= ing_sugar 0) (<= ing_sugar 1)
  (>= ing_grand_marnier 0) (<= ing_grand_marnier 1)
  (>= ing_brandy 0) (<= ing_brandy 1)
  (>= ing_ginger_beer 0) (<= ing_ginger_beer 1)
  (>= ing_mezcal 0) (<= ing_mezcal 1)
  (>= ing_overproof_white_rum 0) (<= ing_overproof_white_rum 1)
  (>= ing_falernum 0) (<= ing_falernum 1)
  (>= ing_maraschino 0) (<= ing_maraschino 1)
  (>= ing_canadian_whiskey 0) (<= ing_canadian_whiskey 1)
  (>= ing_fernet_branca 0) (<= ing_fernet_branca 1)
  (>= ing_cola 0) (<= ing_cola 1)
  (>= ing_white_rum 0) (<= ing_white_rum 1)
  (>= ing_lime 0) (<= ing_lime 1)
  (>= ing_prosecco 0) (<= ing_prosecco 1)
  (>= ing_peach_puree 0) (<= ing_peach_puree 1)
  (>= ing_coffee_liqueur 0) (<= ing_coffee_liqueur 1)
  (>= ing_cachaca 0) (<= ing_cachaca 1)
  (>= ing_cane_sugar 0) (<= ing_cane_sugar 1)
  (>= ing_soda_water 0) (<= ing_soda_water 1)
  (>= ing_dark_rum 0) (<= ing_dark_rum 1)
  (>= ing_creme_de_mure 0) (<= ing_creme_de_mure 1)
  (>= ing_blackberry 0) (<= ing_blackberry 1)
  (>= ing_raspberry_liqueur 0) (<= ing_raspberry_liqueur 1)
  (>= ing_pineapple_juice 0) (<= ing_pineapple_juice 1)
  (>= ing_lillet_blanc 0) (<= ing_lillet_blanc 1)
  (>= ing_brown_creme_de_cacao 0) (<= ing_brown_creme_de_cacao 1)
  (>= ing_light_cream 0) (<= ing_light_cream 1)
  (>= ing_nutmeg 0) (<= ing_nutmeg 1)
  (>= ing_apricot_brandy 0) (<= ing_apricot_brandy 1)
  (>= ing_calvados 0) (<= ing_calvados 1)
  (>= ing_creme_de_violette 0) (<= ing_creme_de_violette 1)
  (>= ing_grenadine 0) (<= ing_grenadine 1)
  (>= ing_old_tom_gin 0) (<= ing_old_tom_gin 1)
  (>= ing_orange_bitters 0) (<= ing_orange_bitters 1)
  (>= ing_raspberry_syrup 0) (<= ing_raspberry_syrup 1)
  (>= ing_raspberry 0) (<= ing_raspberry 1)
  (>= ing_peach_bitters 0) (<= ing_peach_bitters 1)
  (>= ing_rye_whiskey 0) (<= ing_rye_whiskey 1)
  (>= ing_absinthe 0) (<= ing_absinthe 1)
  (>= ing_whiskey 0) (<= ing_whiskey 1)
  (>= ing_water 0) (<= ing_water 1)
  (>= ing_pineapple 0) (<= ing_pineapple 1)
  (>= ing_port 0) (<= ing_port 1)
  (>= ing_egg_yolk 0) (<= ing_egg_yolk 1)
  (>= ing_orange_flower_water 0) (<= ing_orange_flower_water 1)
  (>= ing_vanilla_extract 0) (<= ing_vanilla_extract 1)
  (>= ing_scotch_whiskey 0) (<= ing_scotch_whiskey 1)
  (>= ing_drambuie 0) (<= ing_drambuie 1)
  (>= ing_peychaud_s_bitters 0) (<= ing_peychaud_s_bitters 1)
  (>= ing_white_creme_de_menthe 0) (<= ing_white_creme_de_menthe 1)
  (>= ing_amaretto 0) (<= ing_amaretto 1)
  (>= ing_powdered_sugar 0) (<= ing_powdered_sugar 1)
  (>= ing_tomato_juice 0) (<= ing_tomato_juice 1)
  (>= ing_worcestershire_sauce 0) (<= ing_worcestershire_sauce 1)
  (>= ing_tabasco 0) (<= ing_tabasco 1)
  (>= ing_celery_salt 0) (<= ing_celery_salt 1)
  (>= ing_pepper 0) (<= ing_pepper 1)
  (>= ing_celery 0) (<= ing_celery 1)
  (>= ing_dry_white_wine 0) (<= ing_dry_white_wine 1)
  (>= ing_creme_de_cassis 0) (<= ing_creme_de_cassis 1)
  (>= ing_cointreau 0) (<= ing_cointreau 1)
  (>= ing_curacao 0) (<= ing_curacao 1)
  (>= ing_orgeat__almond__syrup 0) (<= ing_orgeat__almond__syrup 1)
  (>= ing_agave_nectar 0) (<= ing_agave_nectar 1)
  (>= ing_irish_cream_liqueur 0) (<= ing_irish_cream_liqueur 1)
  (>= ing_gold_rum 0) (<= ing_gold_rum 1)
  (>= ing_galliano 0) (<= ing_galliano 1)
  (>= ing_cranberry_juice 0) (<= ing_cranberry_juice 1)
  (>= ing_olive_juice 0) (<= ing_olive_juice 1)
  (>= ing_espresso 0) (<= ing_espresso 1)
  (>= ing_grapefruit_juice 0) (<= ing_grapefruit_juice 1)
  (>= ing_ginger_ale 0) (<= ing_ginger_ale 1)
  (>= ing_irish_whiskey 0) (<= ing_irish_whiskey 1)
  (>= ing_coffee 0) (<= ing_coffee 1)
  (>= ing_coconut_cream 0) (<= ing_coconut_cream 1)
  (>= ing_pisco 0) (<= ing_pisco 1)
  (>= ing_sparkling_wine 0) (<= ing_sparkling_wine 1)
  (>= ing_peach_schnapps 0) (<= ing_peach_schnapps 1)
  (>= ing_cherry_liqueur 0) (<= ing_cherry_liqueur 1)
  (>= ing_dom_benedictine 0) (<= ing_dom_benedictine 1)
  (>= ing_demerara_rum 0) (<= ing_demerara_rum 1)
  (>= ing_cinnamon_syrup 0) (<= ing_cinnamon_syrup 1)
  (>= ing_aromatic_bitters 0) (<= ing_aromatic_bitters 1)
  (>= ing_green_chartreuse 0) (<= ing_green_chartreuse 1)
  (>= ing_cuban_aguardiente 0) (<= ing_cuban_aguardiente 1)
  (>= ing_honey 0) (<= ing_honey 1)
  (>= ing_rum 0) (<= ing_rum 1)
  (>= ing_grapefruit_soda 0) (<= ing_grapefruit_soda 1)
  (>= ing_amaro_nonino 0) (<= ing_amaro_nonino 1)
  (>= ing_aperol 0) (<= ing_aperol 1)
  (>= ing_blended_scotch_whiskey 0) (<= ing_blended_scotch_whiskey 1)
  (>= ing_islay_single_malt_scotch_whiskey 0) (<= ing_islay_single_malt_scotch_whiskey 1)
  (>= ing_ginger 0) (<= ing_ginger 1)
  (>= ing_candied_ginger 0) (<= ing_candied_ginger 1)
  (>= ing_elderflower_syrup 0) (<= ing_elderflower_syrup 1)
  (>= ing_red_chili_pepper 0) (<= ing_red_chili_pepper 1)
  (>= ing_yellow_chartreuse 0) (<= ing_yellow_chartreuse 1)
  (>= ing_red_wine 0) (<= ing_red_wine 1)
  (>= ing_kina_lillet 0) (<= ing_kina_lillet 1)
))
(assert (= (+ ing_vodka ing_dry_vermouth ing_lemon ing_olive ) (* 4  (+ cok_vodka_martini cok_vodka_martini__r))))
(assert (= (+ ing_champagne ing_orange_juice ing_orange ) (* 3  (+ cok_mimosa cok_mimosa__r))))
(assert (= (+ ing_gin ing_dry_vermouth ing_lemon ) (* 3  (+ cok_martini cok_martini__r))))
(assert (= (+ ing_tequila ing_triple_sec ing_lime_juice ing_salt ) (* 4  (+ cok_margarita cok_margarita__r))))
(assert (= (+ ing_white_creme_de_cacao ing_green_creme_de_menthe ing_cream ing_mint ) (* 4  (+ cok_grasshopper cok_grasshopper__r))))
(assert (= (+ ing_grappa ing_lemon_juice ing_honey_syrup ing_chamomile_syrup ing_honey_syrup ing_egg_white ing_lemon ing_white_grape ) (* 8  (+ cok_ve_n_to cok_ve_n_to__r))))
(assert (= (+ ing_bourbon_whiskey ing_sweet_red_vermouth ing_campari ing_orange ing_lemon ) (* 5  (+ cok_boulevardier cok_boulevardier__r))))
(assert (= (+ ing_london_dry_gin ing_honey_syrup ing_lemon_juice ing_orange_juice ing_orange ) (* 5  (+ cok_bee_s_nees cok_bee_s_nees__r))))
(assert (= (+ ing_london_dry_gin ing_lemon_juice ing_simple_syrup ing_mint ing_egg_white ) (* 5  (+ cok_southside cok_southside__r))))
(assert (= (+ ing_bourbon_whiskey ing_lemon_juice ing_simple_syrup ing_egg_white ing_cherry ing_orange ) (* 6  (+ cok_whiskey_sour cok_whiskey_sour__r))))
(assert (= (+ ing_champagne ing_cognac ing_angostura_bitters ing_sugar ing_grand_marnier ing_orange ing_cherry ) (* 7  (+ cok_champagne_cocktail cok_champagne_cocktail__r))))
(assert (= (+ ing_brandy ing_gin ing_lime_juice ing_angostura_bitters ing_ginger_beer ing_mint ing_orange ) (* 7  (+ cok_suffering_bastard cok_suffering_bastard__r))))
(assert (= (+ ing_mezcal ing_overproof_white_rum ing_lime_juice ing_falernum ing_simple_syrup ing_maraschino ing_egg_white ) (* 7  (+ cok_illegal cok_illegal__r))))
(assert (= (+ ing_canadian_whiskey ing_fernet_branca ing_sugar ing_angostura_bitters ing_orange ) (* 5  (+ cok_toronto cok_toronto__r))))
(assert (= (+ ing_gin ing_simple_syrup ing_lemon_juice ing_champagne ) (* 4  (+ cok_french_75 cok_french_75__r))))
(assert (= (+ ing_cola ing_white_rum ing_lime_juice ing_lime ) (* 4  (+ cok_cuba_libre cok_cuba_libre__r))))
(assert (= (+ ing_vodka ing_ginger_beer ing_lime_juice ing_lime ) (* 4  (+ cok_moscow_mule cok_moscow_mule__r))))
(assert (= (+ ing_prosecco ing_peach_puree ) (* 2  (+ cok_bellini cok_bellini__r))))
(assert (= (+ ing_vodka ing_coffee_liqueur ) (* 2  (+ cok_black_russian cok_black_russian__r))))
(assert (= (+ ing_cachaca ing_lime ing_cane_sugar ) (* 3  (+ cok_caipirinha cok_caipirinha__r))))
(assert (= (+ ing_white_rum ing_lime_juice ing_mint ing_cane_sugar ing_lemon ing_soda_water ) (* 6  (+ cok_mojito cok_mojito__r))))
(assert (= (+ ing_dark_rum ing_ginger_beer ing_lime ) (* 3  (+ cok_dark__n__stormy cok_dark__n__stormy__r))))
(assert (= (+ ing_gin ing_lemon_juice ing_simple_syrup ing_creme_de_mure ing_lemon ing_blackberry ) (* 6  (+ cok_bramble cok_bramble__r))))
(assert (= (+ ing_vodka ing_raspberry_liqueur ing_pineapple_juice ing_lemon ) (* 4  (+ cok_french_martini cok_french_martini__r))))
(assert (= (+ ing_vodka ing_triple_sec ing_lime_juice ing_lime ) (* 4  (+ cok_kamikaze cok_kamikaze__r))))
(assert (= (+ ing_vodka ing_triple_sec ing_lemon_juice ing_sugar ing_lime ) (* 5  (+ cok_lemon_drop_martini cok_lemon_drop_martini__r))))
(assert (= (+ ing_gin ing_vodka ing_lillet_blanc ing_lemon ) (* 4  (+ cok_vesper cok_vesper__r))))
(assert (= (+ ing_cognac ing_brown_creme_de_cacao ing_light_cream ing_nutmeg ) (* 4  (+ cok_alexander cok_alexander__r))))
(assert (= (+ ing_campari ing_sweet_red_vermouth ing_soda_water ing_orange ing_lemon ) (* 5  (+ cok_americano cok_americano__r))))
(assert (= (+ ing_gin ing_apricot_brandy ing_calvados ) (* 3  (+ cok_angel_face cok_angel_face__r))))
(assert (= (+ ing_gin ing_lemon_juice ing_maraschino ing_creme_de_violette ing_cherry ) (* 5  (+ cok_aviation cok_aviation__r))))
(assert (= (+ ing_white_rum ing_lime_juice ing_grenadine ) (* 3  (+ cok_bacardi_cocktail cok_bacardi_cocktail__r))))
(assert (= (+ ing_white_rum ing_cognac ing_triple_sec ing_lemon_juice ) (* 4  (+ cok_between_the_sheets cok_between_the_sheets__r))))
(assert (= (+ ing_old_tom_gin ing_maraschino ing_orange_bitters ing_lemon_juice ing_lemon ing_cherry ) (* 6  (+ cok_casino cok_casino__r))))
(assert (= (+ ing_gin ing_lemon_juice ing_raspberry_syrup ing_egg_white ing_raspberry ) (* 5  (+ cok_clover_club cok_clover_club__r))))
(assert (= (+ ing_white_rum ing_lemon_juice ing_simple_syrup ) (* 3  (+ cok_daiquiri cok_daiquiri__r))))
(assert (= (+ ing_gin ing_peach_bitters ing_mint ) (* 3  (+ cok_derby cok_derby__r))))
(assert (= (+ ing_gin ing_dry_vermouth ing_lemon ing_olive ) (* 4  (+ cok_dry_martini cok_dry_martini__r))))
(assert (= (+ ing_gin ing_lemon_juice ing_simple_syrup ing_soda_water ing_lemon ) (* 5  (+ cok_gin_fizz cok_gin_fizz__r))))
(assert (= (+ ing_gin ing_lemon_juice ing_simple_syrup ing_soda_water ing_angostura_bitters ing_lemon ing_cherry ) (* 7  (+ cok_john_collins cok_john_collins__r))))
(assert (= (+ ing_rye_whiskey ing_sweet_red_vermouth ing_angostura_bitters ing_cherry ) (* 4  (+ cok_manhattan cok_manhattan__r))))
(assert (= (+ ing_white_rum ing_pineapple_juice ing_grenadine ing_maraschino ) (* 4  (+ cok_mary_pickford cok_mary_pickford__r))))
(assert (= (+ ing_gin ing_orange_juice ing_absinthe ing_grenadine ) (* 4  (+ cok_monkey_gland cok_monkey_gland__r))))
(assert (= (+ ing_gin ing_sweet_red_vermouth ing_campari ing_orange ) (* 4  (+ cok_negroni cok_negroni__r))))
(assert (= (+ ing_whiskey ing_angostura_bitters ing_sugar ing_water ing_orange ing_cherry ) (* 6  (+ cok_old_fashioned cok_old_fashioned__r))))
(assert (= (+ ing_gin ing_apricot_brandy ing_orange_juice ) (* 3  (+ cok_paradise cok_paradise__r))))
(assert (= (+ ing_dark_rum ing_orange_juice ing_pineapple_juice ing_lemon_juice ing_grenadine ing_simple_syrup ing_angostura_bitters ing_cherry ing_pineapple ) (* 9  (+ cok_planter_s_punch cok_planter_s_punch__r))))
(assert (= (+ ing_brandy ing_port ing_egg_yolk ing_nutmeg ) (* 4  (+ cok_porto_flip cok_porto_flip__r))))
(assert (= (+ ing_gin ing_cream ing_simple_syrup ing_lime_juice ing_lemon_juice ing_egg_white ing_orange_flower_water ing_vanilla_extract ing_soda_water ) (* 9  (+ cok_ramos_fizz cok_ramos_fizz__r))))
(assert (= (+ ing_scotch_whiskey ing_drambuie ing_lemon ) (* 3  (+ cok_rusty_nail cok_rusty_nail__r))))
(assert (= (+ ing_cognac ing_absinthe ing_sugar ing_peychaud_s_bitters ing_lemon ) (* 5  (+ cok_sazerac cok_sazerac__r))))
(assert (= (+ ing_vodka ing_orange_juice ing_orange ) (* 3  (+ cok_screwdriver cok_screwdriver__r))))
(assert (= (+ ing_cognac ing_triple_sec ing_lemon_juice ) (* 3  (+ cok_sidecar cok_sidecar__r))))
(assert (= (+ ing_cognac ing_white_creme_de_menthe ) (* 2  (+ cok_stinger cok_stinger__r))))
(assert (= (+ ing_old_tom_gin ing_dry_vermouth ing_maraschino ing_absinthe ing_orange_bitters ing_cherry ing_lemon ) (* 7  (+ cok_tuxedo cok_tuxedo__r))))
(assert (= (+ ing_gin ing_triple_sec ing_lemon_juice ) (* 3  (+ cok_white_lady cok_white_lady__r))))
(assert (= (+ ing_cognac ing_amaretto ) (* 2  (+ cok_french_connection cok_french_connection__r))))
(assert (= (+ ing_bourbon_whiskey ing_mint ing_water ing_powdered_sugar ) (* 4  (+ cok_mint_julep cok_mint_julep__r))))
(assert (= (+ ing_vodka ing_coffee_liqueur ing_cream ) (* 3  (+ cok_white_russian cok_white_russian__r))))
(assert (= (+ ing_vodka ing_tomato_juice ing_lemon_juice ing_worcestershire_sauce ing_tabasco ing_celery_salt ing_pepper ing_celery ing_lemon ) (* 9  (+ cok_bloody_mary cok_bloody_mary__r))))
(assert (= (+ ing_dry_white_wine ing_creme_de_cassis ) (* 2  (+ cok_kir cok_kir__r))))
(assert (= (+ ing_champagne ing_creme_de_cassis ) (* 2  (+ cok_kir_royal cok_kir_royal__r))))
(assert (= (+ ing_vodka ing_tequila ing_white_rum ing_gin ing_cointreau ing_lemon_juice ing_simple_syrup ing_cola ing_lemon ) (* 9  (+ cok_long_island_iced_tea cok_long_island_iced_tea__r))))
(assert (= (+ ing_white_rum ing_dark_rum ing_curacao ing_orgeat__almond__syrup ing_lime_juice ing_simple_syrup ing_pineapple ing_mint ing_lime ) (* 9  (+ cok_mai-tai cok_mai-tai__r))))
(assert (= (+ ing_tequila ing_lime_juice ing_agave_nectar ) (* 3  (+ cok_tommy_s_margarita cok_tommy_s_margarita__r))))
(assert (= (+ ing_coffee_liqueur ing_triple_sec ing_irish_cream_liqueur ) (* 3  (+ cok_b52 cok_b52__r))))
(assert (= (+ ing_gold_rum ing_galliano ing_pineapple_juice ing_lime_juice ing_prosecco ) (* 5  (+ cok_barracuda cok_barracuda__r))))
(assert (= (+ ing_gin ing_cointreau ing_lillet_blanc ing_lemon_juice ing_absinthe ing_orange ) (* 6  (+ cok_corpse_reviver_N2 cok_corpse_reviver_N2__r))))
(assert (= (+ ing_vodka ing_cointreau ing_lime_juice ing_cranberry_juice ing_lemon ) (* 5  (+ cok_cosmopolitan cok_cosmopolitan__r))))
(assert (= (+ ing_vodka ing_dry_vermouth ing_olive_juice ing_olive ) (* 4  (+ cok_dirty_martini cok_dirty_martini__r))))
(assert (= (+ ing_vodka ing_coffee_liqueur ing_simple_syrup ing_espresso ) (* 4  (+ cok_espresso_martini cok_espresso_martini__r))))
(assert (= (+ ing_triple_sec ing_galliano ing_orange_juice ing_cream ) (* 4  (+ cok_golden_dream cok_golden_dream__r))))
(assert (= (+ ing_white_rum ing_grapefruit_juice ing_maraschino ing_lime_juice ) (* 4  (+ cok_hemingway_special cok_hemingway_special__r))))
(assert (= (+ ing_cognac ing_ginger_ale ing_angostura_bitters ing_lemon ) (* 4  (+ cok_horse_s_neck cok_horse_s_neck__r))))
(assert (= (+ ing_irish_whiskey ing_coffee ing_cream ing_sugar ) (* 4  (+ cok_irish_coffee cok_irish_coffee__r))))
(assert (= (+ ing_old_tom_gin ing_lemon_juice ing_simple_syrup ing_soda_water ing_angostura_bitters ing_lemon ing_cherry ) (* 7  (+ cok_tom_collins cok_tom_collins__r))))
(assert (= (+ ing_white_rum ing_coconut_cream ing_pineapple_juice ing_pineapple ing_cherry ) (* 5  (+ cok_pina_colada cok_pina_colada__r))))
(assert (= (+ ing_pisco ing_simple_syrup ing_lemon_juice ing_egg_white ing_angostura_bitters ) (* 5  (+ cok_pisco_sour cok_pisco_sour__r))))
(assert (= (+ ing_vodka ing_lemon_juice ing_creme_de_cassis ing_simple_syrup ing_sparkling_wine ing_lemon ing_blackberry ) (* 7  (+ cok_russian_spring_punch cok_russian_spring_punch__r))))
(assert (= (+ ing_vodka ing_cranberry_juice ing_grapefruit_juice ing_orange ing_cherry ) (* 5  (+ cok_sea_breeze cok_sea_breeze__r))))
(assert (= (+ ing_vodka ing_peach_schnapps ing_orange_juice ing_cranberry_juice ing_grapefruit_juice ing_orange ) (* 6  (+ cok_sex_on_the_beach cok_sex_on_the_beach__r))))
(assert (= (+ ing_gin ing_cherry_liqueur ing_cointreau ing_dom_benedictine ing_pineapple_juice ing_lime_juice ing_grenadine ing_angostura_bitters ing_cherry ing_pineapple ) (* 10  (+ cok_singapore_sling cok_singapore_sling__r))))
(assert (= (+ ing_tequila ing_orange_juice ing_grenadine ing_orange ) (* 4  (+ cok_tequila_sunrise cok_tequila_sunrise__r))))
(assert (= (+ ing_white_rum ing_galliano ing_triple_sec ing_lime_juice ) (* 4  (+ cok_yellow_bird cok_yellow_bird__r))))
(assert (= (+ ing_dark_rum ing_gold_rum ing_demerara_rum ing_lime_juice ing_falernum ing_grapefruit_juice ing_cinnamon_syrup ing_grenadine ing_angostura_bitters ing_absinthe ing_mint ) (* 11  (+ cok_zombie cok_zombie__r))))
(assert (= (+ ing_brandy ing_lemon_juice ing_maraschino ing_curacao ing_simple_syrup ing_aromatic_bitters ing_orange ing_powdered_sugar ) (* 8  (+ cok_brandy_crusta cok_brandy_crusta__r))))
(assert (= (+ ing_london_dry_gin ing_sweet_red_vermouth ing_fernet_branca ing_orange ) (* 4  (+ cok_hanky_panky cok_hanky_panky__r))))
(assert (= (+ ing_gin ing_green_chartreuse ing_maraschino ing_lime_juice ) (* 4  (+ cok_last_word cok_last_word__r))))
(assert (= (+ ing_london_dry_gin ing_sweet_red_vermouth ing_maraschino ing_orange_bitters ing_lemon ) (* 5  (+ cok_martinez cok_martinez__r))))
(assert (= (+ ing_rye_whiskey ing_cognac ing_sweet_red_vermouth ing_dom_benedictine ing_peychaud_s_bitters ing_orange ing_cherry ) (* 7  (+ cok_vieux_carre cok_vieux_carre__r))))
(assert (= (+ ing_cuban_aguardiente ing_lemon_juice ing_honey ing_water ing_lime ) (* 5  (+ cok_cachanchara cok_cachanchara__r))))
(assert (= (+ ing_fernet_branca ing_cola ) (* 2  (+ cok_fernandito cok_fernandito__r))))
(assert (= (+ ing_rum ing_sparkling_wine ing_lime_juice ing_simple_syrup ing_angostura_bitters ing_mint ) (* 6  (+ cok_old_cuban cok_old_cuban__r))))
(assert (= (+ ing_tequila ing_grapefruit_soda ing_lime_juice ing_salt ing_lime ) (* 5  (+ cok_paloma cok_paloma__r))))
(assert (= (+ ing_bourbon_whiskey ing_amaro_nonino ing_aperol ing_lemon_juice ) (* 4  (+ cok_paper_plane cok_paper_plane__r))))
(assert (= (+ ing_blended_scotch_whiskey ing_islay_single_malt_scotch_whiskey ing_lemon_juice ing_honey_syrup ing_ginger ing_candied_ginger ) (* 6  (+ cok_penicillin cok_penicillin__r))))
(assert (= (+ ing_vodka ing_elderflower_syrup ing_lemon_juice ing_honey_syrup ing_vanilla_extract ing_red_chili_pepper ) (* 6  (+ cok_spicy_fifty cok_spicy_fifty__r))))
(assert (= (+ ing_irish_whiskey ing_sweet_red_vermouth ing_green_chartreuse ing_angostura_bitters ing_orange ) (* 5  (+ cok_tipperary cok_tipperary__r))))
(assert (= (+ ing_angostura_bitters ing_orgeat__almond__syrup ing_lemon_juice ing_rye_whiskey ) (* 4  (+ cok_trinidad_sour cok_trinidad_sour__r))))
(assert (= (+ ing_mezcal ing_yellow_chartreuse ing_aperol ing_lime_juice ) (* 4  (+ cok_naked_and_famous cok_naked_and_famous__r))))
(assert (= (+ ing_rye_whiskey ing_lemon_juice ing_egg_white ing_simple_syrup ing_red_wine ing_lemon ing_cherry ) (* 7  (+ cok_new_york_sour cok_new_york_sour__r))))
(assert (= (+ ing_prosecco ing_aperol ing_soda_water ing_orange ) (* 4  (+ cok_spritz cok_spritz__r))))
(assert (= (+ ing_lime_juice ing_simple_syrup ing_gin ) (* 3  (+ cok_gimlet cok_gimlet__r))))
(assert (= (+ ing_gin ing_lemon_juice ing_white_creme_de_cacao ing_kina_lillet ing_lemon ) (* 5  (+ cok_n20th_century cok_n20th_century__r))))
(assert (= 5 (+
ing_vodka ing_dry_vermouth ing_lemon ing_olive ing_champagne ing_orange_juice ing_orange ing_gin ing_tequila ing_triple_sec ing_lime_juice ing_salt ing_white_creme_de_cacao ing_green_creme_de_menthe ing_cream ing_mint ing_grappa ing_lemon_juice ing_honey_syrup ing_chamomile_syrup ing_egg_white ing_white_grape ing_bourbon_whiskey ing_sweet_red_vermouth ing_campari ing_london_dry_gin ing_simple_syrup ing_cherry ing_cognac ing_angostura_bitters ing_sugar ing_grand_marnier ing_brandy ing_ginger_beer ing_mezcal ing_overproof_white_rum ing_falernum ing_maraschino ing_canadian_whiskey ing_fernet_branca ing_cola ing_white_rum ing_lime ing_prosecco ing_peach_puree ing_coffee_liqueur ing_cachaca ing_cane_sugar ing_soda_water ing_dark_rum ing_creme_de_mure ing_blackberry ing_raspberry_liqueur ing_pineapple_juice ing_lillet_blanc ing_brown_creme_de_cacao ing_light_cream ing_nutmeg ing_apricot_brandy ing_calvados ing_creme_de_violette ing_grenadine ing_old_tom_gin ing_orange_bitters ing_raspberry_syrup ing_raspberry ing_peach_bitters ing_rye_whiskey ing_absinthe ing_whiskey ing_water ing_pineapple ing_port ing_egg_yolk ing_orange_flower_water ing_vanilla_extract ing_scotch_whiskey ing_drambuie ing_peychaud_s_bitters ing_white_creme_de_menthe ing_amaretto ing_powdered_sugar ing_tomato_juice ing_worcestershire_sauce ing_tabasco ing_celery_salt ing_pepper ing_celery ing_dry_white_wine ing_creme_de_cassis ing_cointreau ing_curacao ing_orgeat__almond__syrup ing_agave_nectar ing_irish_cream_liqueur ing_gold_rum ing_galliano ing_cranberry_juice ing_olive_juice ing_espresso ing_grapefruit_juice ing_ginger_ale ing_irish_whiskey ing_coffee ing_coconut_cream ing_pisco ing_sparkling_wine ing_peach_schnapps ing_cherry_liqueur ing_dom_benedictine ing_demerara_rum ing_cinnamon_syrup ing_aromatic_bitters ing_green_chartreuse ing_cuban_aguardiente ing_honey ing_rum ing_grapefruit_soda ing_amaro_nonino ing_aperol ing_blended_scotch_whiskey ing_islay_single_malt_scotch_whiskey ing_ginger ing_candied_ginger ing_elderflower_syrup ing_red_chili_pepper ing_yellow_chartreuse ing_red_wine ing_kina_lillet
)))
(maximize (+
  cok_vodka_martini cok_mimosa cok_martini cok_margarita cok_grasshopper cok_ve_n_to cok_boulevardier cok_bee_s_nees cok_southside cok_whiskey_sour cok_champagne_cocktail cok_suffering_bastard cok_illegal cok_toronto cok_french_75 cok_cuba_libre cok_moscow_mule cok_bellini cok_black_russian cok_caipirinha cok_mojito cok_dark__n__stormy cok_bramble cok_french_martini cok_kamikaze cok_lemon_drop_martini cok_vesper cok_alexander cok_americano cok_angel_face cok_aviation cok_bacardi_cocktail cok_between_the_sheets cok_casino cok_clover_club cok_daiquiri cok_derby cok_dry_martini cok_gin_fizz cok_john_collins cok_manhattan cok_mary_pickford cok_monkey_gland cok_negroni cok_old_fashioned cok_paradise cok_planter_s_punch cok_porto_flip cok_ramos_fizz cok_rusty_nail cok_sazerac cok_screwdriver cok_sidecar cok_stinger cok_tuxedo cok_white_lady cok_french_connection cok_mint_julep cok_white_russian cok_bloody_mary cok_kir cok_kir_royal cok_long_island_iced_tea cok_mai-tai cok_tommy_s_margarita cok_b52 cok_barracuda cok_corpse_reviver_N2 cok_cosmopolitan cok_dirty_martini cok_espresso_martini cok_golden_dream cok_hemingway_special cok_horse_s_neck cok_irish_coffee cok_tom_collins cok_pina_colada cok_pisco_sour cok_russian_spring_punch cok_sea_breeze cok_sex_on_the_beach cok_singapore_sling cok_tequila_sunrise cok_yellow_bird cok_zombie cok_brandy_crusta cok_hanky_panky cok_last_word cok_martinez cok_vieux_carre cok_cachanchara cok_fernandito cok_old_cuban cok_paloma cok_paper_plane cok_penicillin cok_spicy_fifty cok_tipperary cok_trinidad_sour cok_naked_and_famous cok_new_york_sour cok_spritz cok_gimlet cok_n20th_century ))
(check-sat)
(get-model)