(interval_examples4Q
 (zero_to_one_quarter 0
  (zero_to_one_quarter-1 nil 3600857764
   (""
    (then (skeep)
     (numerical (! 1 1) :precision 4 :maxdepth 20 :verbose? t))
    nil nil)
   ((IntervalExpr type-decl nil IntervalExpr_adt "interval_arith/")
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (const? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (RealExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]"
     IntervalExpr_adt "interval_arith/")
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (X const-decl "RealExpr" interval_expr "interval_arith/")
    (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]"
     IntervalExpr_adt "interval_arith/")
    (r2E const-decl "RealExpr" interval_expr "interval_arith/")
    (numerical_soundness formula-decl nil numerical_bandb
     "interval_arith/")
    (sound? const-decl "bool" numerical_bandb "interval_arith/")
    (listn_0 name-judgement "listn[real](0)" simple_bandb
     "interval_arith/")
    (Env type-eq-decl nil box "interval_arith/")
    (vars_in_box? const-decl "bool" box "interval_arith/")
    (list2array def-decl "T" array2list "structures/")
    (x skolem-const-decl "real" interval_examples4Q nil)
    (nml_81 skolem-const-decl "(mult?)" interval_examples4Q nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (|##| const-decl "bool" interval "interval_arith/")
    (lb_interval formula-decl nil interval "interval_arith/")
    (ub_interval formula-decl nil interval "interval_arith/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (eval def-decl "real" interval_expr "interval_arith/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (vars_in_box formula-decl nil box "interval_arith/")
    (length_singleton formula-decl nil more_list_props "structures/")
    (vars_in_box_rec def-decl
     "{b: bool | b = (FORALL (k: subrange(i, n - 1)): vs(k) ## nth(box, k - i))}"
     box "interval_arith/")
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (Interval type-eq-decl nil interval "interval_arith/")
    (list type-decl nil list_adt nil)
    (Box type-eq-decl nil box "interval_arith/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (ProperBox type-eq-decl nil box "interval_arith/")
    (IntervalMinMax type-eq-decl nil numerical_bandb "interval_arith/")
    (ProperBox? const-decl "bool" box "interval_arith/")
    (DirVar type-eq-decl nil branch_and_bound "structures/")
    (stack type-eq-decl nil stack "structures/")
    (length def-decl "nat" list_props nil)
    (DirVarStack type-eq-decl nil branch_and_bound "structures/")
    (DirVarSelector type-eq-decl nil branch_and_bound "structures/")
    (Output type-eq-decl nil branch_and_bound "structures/")
    (numerical const-decl "Output" numerical_bandb "interval_arith/")
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (altdir_maxvar const-decl "DirVar" numerical_bandb
                   "interval_arith/")
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    ([\|\|] const-decl "Interval" interval "interval_arith/")
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (FALSE const-decl "bool" booleans nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil))
   shostak))
 (Heart_TCC1 0
  (Heart_TCC1-1 nil 3600857764 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (Heart_TCC2 0
  (Heart_TCC2-1 nil 3600857764 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (hdp_mm_TCC1 0
  (hdp_mm_TCC1-1 nil 3600857764 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (hdp_mm_TCC2 0
  (hdp_mm_TCC2-1 nil 3600857764 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (hdp_mm_TCC3 0
  (hdp_mm_TCC3-1 nil 3600857764 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (hdp_mm_TCC4 0
  (hdp_mm_TCC4-1 nil 3600857764 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (hdp_mm_TCC5 0
  (hdp_mm_TCC5-1 nil 3600857764 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (hdp_mm_TCC6 0
  (hdp_mm_TCC6-1 nil 3600857764 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (hdp_mm 0
  (hdp_mm-1 nil 3600857764
   ("" (then (skeep) (numerical (! 1 1) :verbose? t)) nil nil)
   ((IntervalExpr type-decl nil IntervalExpr_adt "interval_arith/")
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (const? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (RealExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]"
     IntervalExpr_adt "interval_arith/")
    (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]"
     IntervalExpr_adt "interval_arith/")
    (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]"
     IntervalExpr_adt "interval_arith/")
    (NEG adt-constructor-decl "[RealExpr -> (neg?)]" IntervalExpr_adt
     "interval_arith/")
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (X const-decl "RealExpr" interval_expr "interval_arith/")
    (POW adt-constructor-decl "[[RealExpr, nat] -> (pow?)]"
     IntervalExpr_adt "interval_arith/")
    (r2E const-decl "RealExpr" interval_expr "interval_arith/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (numerical_soundness formula-decl nil numerical_bandb
     "interval_arith/")
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (sound? const-decl "bool" numerical_bandb "interval_arith/")
    (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
    (vars_in_box_rec def-decl
     "{b: bool | b = (FORALL (k: subrange(i, n - 1)): vs(k) ## nth(box, k - i))}"
     box "interval_arith/")
    (vars_in_box formula-decl nil box "interval_arith/")
    (^ const-decl "real" exponentiation nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (eval def-decl "real" interval_expr "interval_arith/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ub_interval formula-decl nil interval "interval_arith/")
    (lb_interval formula-decl nil interval "interval_arith/")
    (|##| const-decl "bool" interval "interval_arith/")
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (nml_82 skolem-const-decl "(sub?)" interval_examples4Q nil)
    (x4 skolem-const-decl "real" interval_examples4Q nil)
    (x7 skolem-const-decl "real" interval_examples4Q nil)
    (x3 skolem-const-decl "real" interval_examples4Q nil)
    (x1 skolem-const-decl "real" interval_examples4Q nil)
    (x5 skolem-const-decl "real" interval_examples4Q nil)
    (x6 skolem-const-decl "real" interval_examples4Q nil)
    (x2 skolem-const-decl "real" interval_examples4Q nil)
    (x0 skolem-const-decl "real" interval_examples4Q nil)
    (list2array def-decl "T" array2list "structures/")
    (vars_in_box? const-decl "bool" box "interval_arith/")
    (Env type-eq-decl nil box "interval_arith/")
    (listn_0 name-judgement "listn[real](0)" simple_bandb
     "interval_arith/")
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (Interval type-eq-decl nil interval "interval_arith/")
    (list type-decl nil list_adt nil)
    (Box type-eq-decl nil box "interval_arith/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (ProperBox type-eq-decl nil box "interval_arith/")
    (IntervalMinMax type-eq-decl nil numerical_bandb "interval_arith/")
    (ProperBox? const-decl "bool" box "interval_arith/")
    (DirVar type-eq-decl nil branch_and_bound "structures/")
    (stack type-eq-decl nil stack "structures/")
    (length def-decl "nat" list_props nil)
    (DirVarStack type-eq-decl nil branch_and_bound "structures/")
    (DirVarSelector type-eq-decl nil branch_and_bound "structures/")
    (Output type-eq-decl nil branch_and_bound "structures/")
    (numerical const-decl "Output" numerical_bandb "interval_arith/")
    (altdir_maxvar const-decl "DirVar" numerical_bandb
                   "interval_arith/")
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    ([\|\|] const-decl "Interval" interval "interval_arith/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (FALSE const-decl "bool" booleans nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil))
   shostak))
 (hdp_minmax 0
  (hdp_minmax-1 nil 3600857764 ("" (then (skeep) (interval)) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (FALSE const-decl "bool" booleans nil)
    (Some adt-constructor-decl "[T -> (some?)]" Maybe "structures/")
    (null adt-constructor-decl "(null?)" list_adt nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    ([\|\|] const-decl "Interval" interval "interval_arith/")
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (alt_max const-decl "DirVar" interval_bandb "interval_arith/")
    (interval const-decl "Output" interval_bandb "interval_arith/")
    (Output type-eq-decl nil branch_and_bound "structures/")
    (DirVarSelector type-eq-decl nil branch_and_bound "structures/")
    (DirVarStack type-eq-decl nil branch_and_bound "structures/")
    (length def-decl "nat" list_props nil)
    (stack type-eq-decl nil stack "structures/")
    (DirVar type-eq-decl nil branch_and_bound "structures/")
    (ProperBox type-eq-decl nil box "interval_arith/")
    (ProperBox? const-decl "bool" box "interval_arith/")
    (Box type-eq-decl nil box "interval_arith/")
    (IntervalOutput type-eq-decl nil interval_bandb "interval_arith/")
    (val adt-accessor-decl "[(some?) -> T]" Maybe "structures/")
    (some? adt-recognizer-decl "[Maybe -> boolean]" Maybe
     "structures/")
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (BoolExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bite? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (brel? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bor? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (band? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (every adt-def-decl "boolean" list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (list type-decl nil list_adt nil)
    (Maybe type-decl nil Maybe "structures/")
    (listn_0 name-judgement "listn[real](0)" simple_bandb
     "interval_arith/")
    (Env type-eq-decl nil box "interval_arith/")
    (vars_in_box? const-decl "bool" box "interval_arith/")
    (list2array def-decl "T" array2list "structures/")
    (x0 skolem-const-decl "real" interval_examples4Q nil)
    (x2 skolem-const-decl "real" interval_examples4Q nil)
    (x6 skolem-const-decl "real" interval_examples4Q nil)
    (x5 skolem-const-decl "real" interval_examples4Q nil)
    (x1 skolem-const-decl "real" interval_examples4Q nil)
    (x3 skolem-const-decl "real" interval_examples4Q nil)
    (x7 skolem-const-decl "real" interval_examples4Q nil)
    (x4 skolem-const-decl "real" interval_examples4Q nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (beval def-decl "bool" interval_bexpr "interval_arith/")
    (eval def-decl "real" interval_expr "interval_arith/")
    (|##| const-decl "bool" interval "interval_arith/")
    (iar_83 skolem-const-decl "(bincludes?)" interval_examples4Q nil)
    (vars_in_box formula-decl nil box "interval_arith/")
    (vars_in_box_rec def-decl
     "{b: bool | b = (FORALL (k: subrange(i, n - 1)): vs(k) ## nth(box, k - i))}"
     box "interval_arith/")
    (lb_interval formula-decl nil interval "interval_arith/")
    (ub_interval formula-decl nil interval "interval_arith/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (sound? const-decl "bool" interval_bandb "interval_arith/")
    (minus_even_is_even application-judgement "even_int" integers nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (interval_soundness formula-decl nil interval_bandb
     "interval_arith/")
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (r2E const-decl "RealExpr" interval_expr "interval_arith/")
    (POW adt-constructor-decl "[[RealExpr, nat] -> (pow?)]"
     IntervalExpr_adt "interval_arith/")
    (X const-decl "RealExpr" interval_expr "interval_arith/")
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (NEG adt-constructor-decl "[RealExpr -> (neg?)]" IntervalExpr_adt
     "interval_arith/")
    (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]"
     IntervalExpr_adt "interval_arith/")
    (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]"
     IntervalExpr_adt "interval_arith/")
    (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]"
     IntervalExpr_adt "interval_arith/")
    (BINCLUDES adt-constructor-decl
     "[[RealExpr, Interval] -> (bincludes?)]" IntervalExpr_adt
     "interval_arith/")
    (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (Interval type-eq-decl nil interval "interval_arith/")
    (RealExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (const? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IntervalExpr type-decl nil IntervalExpr_adt "interval_arith/")
    (>= const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (/= const-decl "boolean" notequal nil)
    (number nonempty-type-decl nil numbers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (common_point_TCC1 0
  (common_point_TCC1-1 nil 3600857764 ("" (subtype-tcc) nil nil)
   (([\|\|] const-decl "Interval" interval "interval_arith/")
    (|##| const-decl "bool" interval "interval_arith/")
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil))
   nil))
 (common_point 0
  (common_point-1 nil 3600857764 ("" (interval :verbose? t) nil nil)
   ((minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (Maybe type-decl nil Maybe "structures/")
    (list type-decl nil list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (some? adt-recognizer-decl "[Maybe -> boolean]" Maybe
     "structures/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (val adt-accessor-decl "[(some?) -> T]" Maybe "structures/")
    (IntervalOutput type-eq-decl nil interval_bandb "interval_arith/")
    (Box type-eq-decl nil box "interval_arith/")
    (ProperBox? const-decl "bool" box "interval_arith/")
    (ProperBox type-eq-decl nil box "interval_arith/")
    (DirVar type-eq-decl nil branch_and_bound "structures/")
    (stack type-eq-decl nil stack "structures/")
    (length def-decl "nat" list_props nil)
    (DirVarStack type-eq-decl nil branch_and_bound "structures/")
    (DirVarSelector type-eq-decl nil branch_and_bound "structures/")
    (Output type-eq-decl nil branch_and_bound "structures/")
    (interval const-decl "Output" interval_bandb "interval_arith/")
    (alt_max const-decl "DirVar" interval_bandb "interval_arith/")
    (FALSE const-decl "bool" booleans nil)
    (BNOT adt-constructor-decl "[BoolExpr -> (bnot?)]" IntervalExpr_adt
     "interval_arith/")
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (Some adt-constructor-decl "[T -> (some?)]" Maybe "structures/")
    (sound? const-decl "bool" interval_bandb "interval_arith/")
    (interval_soundness formula-decl nil interval_bandb
     "interval_arith/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]"
     IntervalExpr_adt "interval_arith/")
    (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]"
     IntervalExpr_adt "interval_arith/")
    (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]"
     IntervalExpr_adt "interval_arith/")
    (< const-decl "bool" reals nil)
    (BLETIN adt-constructor-decl
     "[[IntervalExpr, BoolExpr] -> (bletin?)]" IntervalExpr_adt
     "interval_arith/")
    (BINCLUDES adt-constructor-decl
     "[[RealExpr, Interval] -> (bincludes?)]" IntervalExpr_adt
     "interval_arith/")
    (r2E const-decl "RealExpr" interval_expr "interval_arith/")
    (ABS adt-constructor-decl "[RealExpr -> (abs?)]" IntervalExpr_adt
     "interval_arith/")
    (BREL adt-constructor-decl
     "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt
     "interval_arith/")
    (RealOrder type-eq-decl nil real_orders "reals/")
    (realorder? const-decl "bool" real_orders "reals/")
    (BAND adt-constructor-decl "[[BoolExpr, BoolExpr] -> (band?)]"
     IntervalExpr_adt "interval_arith/")
    (BoolExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bite? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (brel? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bor? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (band? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (IntervalExpr type-decl nil IntervalExpr_adt "interval_arith/")
    (const? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (RealExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (POW adt-constructor-decl "[[RealExpr, nat] -> (pow?)]"
     IntervalExpr_adt "interval_arith/")
    (X const-decl "RealExpr" interval_expr "interval_arith/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (Interval type-eq-decl nil interval "interval_arith/")
    (|##| const-decl "bool" interval "interval_arith/")
    ([\|\|] const-decl "Interval" interval "interval_arith/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (^ const-decl "real" exponentiation nil))
   shostak))
 (simple_ite 0
  (simple_ite-1 nil 3600857764 ("" (interval) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (listn_0 name-judgement "listn[real](0)" simple_bandb
     "interval_arith/")
    (Maybe type-decl nil Maybe "structures/")
    (list type-decl nil list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (some? adt-recognizer-decl "[Maybe -> boolean]" Maybe
     "structures/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (val adt-accessor-decl "[(some?) -> T]" Maybe "structures/")
    (IntervalOutput type-eq-decl nil interval_bandb "interval_arith/")
    (Box type-eq-decl nil box "interval_arith/")
    (ProperBox? const-decl "bool" box "interval_arith/")
    (ProperBox type-eq-decl nil box "interval_arith/")
    (DirVar type-eq-decl nil branch_and_bound "structures/")
    (stack type-eq-decl nil stack "structures/")
    (length def-decl "nat" list_props nil)
    (DirVarStack type-eq-decl nil branch_and_bound "structures/")
    (DirVarSelector type-eq-decl nil branch_and_bound "structures/")
    (Output type-eq-decl nil branch_and_bound "structures/")
    (interval const-decl "Output" interval_bandb "interval_arith/")
    (alt_max const-decl "DirVar" interval_bandb "interval_arith/")
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    ([\|\|] const-decl "Interval" interval "interval_arith/")
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (Some adt-constructor-decl "[T -> (some?)]" Maybe "structures/")
    (FALSE const-decl "bool" booleans nil)
    (vars_in_box_rec def-decl
     "{b: bool | b = (FORALL (k: subrange(i, n - 1)): vs(k) ## nth(box, k - i))}"
     box "interval_arith/")
    (length_singleton formula-decl nil more_list_props "structures/")
    (vars_in_box formula-decl nil box "interval_arith/")
    (iar_87 skolem-const-decl "(bimplies?)" interval_examples4Q nil)
    (eval def-decl "real" interval_expr "interval_arith/")
    (beval def-decl "bool" interval_bexpr "interval_arith/")
    (x_88 skolem-const-decl "{x: real | x ## [|0, 10|]}"
     interval_examples4Q nil)
    (|##| const-decl "bool" interval "interval_arith/")
    (list2array def-decl "T" array2list "structures/")
    (vars_in_box? const-decl "bool" box "interval_arith/")
    (Env type-eq-decl nil box "interval_arith/")
    (Eps const-decl "posreal" interval_examples4Q nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sound? const-decl "bool" interval_bandb "interval_arith/")
    (interval_soundness formula-decl nil interval_bandb
     "interval_arith/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]"
     IntervalExpr_adt "interval_arith/")
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]"
     IntervalExpr_adt "interval_arith/")
    (SQ adt-constructor-decl "[RealExpr -> (sq?)]" IntervalExpr_adt
     "interval_arith/")
    (r2E const-decl "RealExpr" interval_expr "interval_arith/")
    (<= const-decl "bool" reals nil)
    (BREL adt-constructor-decl
     "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt
     "interval_arith/")
    (RealOrder type-eq-decl nil real_orders "reals/")
    (realorder? const-decl "bool" real_orders "reals/")
    (BITE adt-constructor-decl
     "[[BoolExpr, BoolExpr, BoolExpr] -> (bite?)]" IntervalExpr_adt
     "interval_arith/")
    (X const-decl "RealExpr" interval_expr "interval_arith/")
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (BINCLUDES adt-constructor-decl
     "[[RealExpr, Interval] -> (bincludes?)]" IntervalExpr_adt
     "interval_arith/")
    (Interval type-eq-decl nil interval "interval_arith/")
    (real nonempty-type-from-decl nil reals nil)
    (RealExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (const? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (BIMPLIES adt-constructor-decl
     "[[BoolExpr, BoolExpr] -> (bimplies?)]" IntervalExpr_adt
     "interval_arith/")
    (BoolExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bite? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (brel? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bor? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (band? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (IntervalExpr type-decl nil IntervalExpr_adt "interval_arith/"))
   shostak)))