(sturm_examples
 (example_1_TCC1 0
  (example_1_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil) nil nil))
 (example_1_TCC2 0
  (example_1_TCC2-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (example_1_TCC3 0
  (example_1_TCC3-1 nil 3622997593 ("" (subtype-tcc) nil nil) nil nil))
 (example_1 0
  (example_1-1 nil 3622997593 ("" (sturm) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (expt_x1 formula-decl nil exponentiation nil)
    (polylist_minus formula-decl nil polylist "Sturm/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (polylist_pow formula-decl nil polylist "Sturm/")
    (polylist_sum formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (polylist_prod formula-decl nil polylist "Sturm/")
    (contains? const-decl "bool" RealInt "reals/")
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__89 skolem-const-decl "Polylist" sturm_examples nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (pprod const-decl "Polylist" polylist "Sturm/")
    (pconst const-decl "Polylist" polylist "Sturm/")
    (polylist const-decl "real" polylist "Sturm/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (psum def-decl "{pql: Polylist |
         FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}"
          polylist "Sturm/")
    (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)
    (ppow def-decl "Polylist" polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (length def-decl "nat" list_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (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))
   shostak))
 (example_2 0
  (example_2-1 nil 3622997593 ("" (sturm) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (polylist_prod formula-decl nil polylist "Sturm/")
    (polylist_pow formula-decl nil polylist "Sturm/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (polylist_sum formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (polylist_monom formula-decl nil polylist "Sturm/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (polylist_minus formula-decl nil polylist "Sturm/")
    (expt_x1 formula-decl nil exponentiation nil)
    (contains? const-decl "bool" RealInt "reals/")
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__92 skolem-const-decl "Polylist" sturm_examples nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (pprod const-decl "Polylist" polylist "Sturm/")
    (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)
    (ppow def-decl "Polylist" polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (length def-decl "nat" list_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (pconst const-decl "Polylist" polylist "Sturm/")
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (psum def-decl "{pql: Polylist |
         FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}"
          polylist "Sturm/")
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil))
   shostak))
 (example_3_TCC1 0
  (example_3_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (example_3_TCC2 0
  (example_3_TCC2-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (example_3_TCC3 0
  (example_3_TCC3-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (example_3_TCC4 0
  (example_3_TCC4-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (example_3_TCC5 0
  (example_3_TCC5-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (example_3_TCC6 0
  (example_3_TCC6-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (example_3_TCC7 0
  (example_3_TCC7-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (example_3_TCC8 0
  (example_3_TCC8-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (example_3_TCC9 0
  (example_3_TCC9-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (example_3_TCC10 0
  (example_3_TCC10-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (example_3_TCC11 0
  (example_3_TCC11-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (example_3_TCC12 0
  (example_3_TCC12-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (example_3_TCC13 0
  (example_3_TCC13-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (example_3_TCC14 0
  (example_3_TCC14-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (^ const-decl "real" exponentiation nil))
   nil))
 (example_3 0
  (example_3-1 nil 3622997593 ("" (sturm) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (contains? const-decl "bool" RealInt "reals/")
    (polylist_pow formula-decl nil polylist "Sturm/")
    (polylist_sum formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (polylist_minus formula-decl nil polylist "Sturm/")
    (polylist_monom formula-decl nil polylist "Sturm/")
    (expt_x1 formula-decl nil exponentiation nil)
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__95 skolem-const-decl "Polylist" sturm_examples nil)
    (real_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)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (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)
    (ppow def-decl "Polylist" polylist "Sturm/")
    (polylist const-decl "real" polylist "Sturm/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (psum def-decl "{pql: Polylist |
         FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}"
          polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (length def-decl "nat" list_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (pconst const-decl "Polylist" polylist "Sturm/"))
   shostak))
 (example_4_TCC1 0
  (example_4_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (example_4 0
  (example_4-1 nil 3622997593 ("" (sturm) nil nil)
   ((minus_real_is_real application-judgement "real" reals nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (contains? const-decl "bool" RealInt "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (polylist_minus formula-decl nil polylist "Sturm/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (polylist_neg formula-decl nil polylist "Sturm/")
    (expt_x1 formula-decl nil exponentiation nil)
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__98 skolem-const-decl "Polylist" sturm_examples nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (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)
    (length def-decl "nat" list_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (pneg const-decl "Polylist" polylist "Sturm/"))
   shostak))
 (example_5 0
  (example_5-1 nil 3622997593 ("" (sturm) nil nil)
   ((real_minus_real_is_real application-judgement "real" reals nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (contains? const-decl "bool" RealInt "reals/")
    (polylist_minus formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (polylist_monom formula-decl nil polylist "Sturm/")
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__101 skolem-const-decl "Polylist" sturm_examples nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (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)
    (length def-decl "nat" list_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (pconst const-decl "Polylist" polylist "Sturm/"))
   shostak))
 (example_6_TCC1 0
  (example_6_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (example_6 0
  (example_6-1 nil 3622997593 ("" (sturm) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (contains? const-decl "bool" RealInt "reals/")
    (expt_x1 formula-decl nil exponentiation nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (polylist_minus formula-decl nil polylist "Sturm/")
    (polylist_sum formula-decl nil polylist "Sturm/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__104 skolem-const-decl "{pql: Polylist |
         FORALL (x):
           polylist(pql)(x) =
            polylist(pconst(1))(x) +
             polylist(pminus(pmonom(1, 2), pmonom(2, 1)))(x)}"
              sturm_examples nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (polylist const-decl "real" polylist "Sturm/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (psum def-decl "{pql: Polylist |
         FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}"
          polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (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)
    (length def-decl "nat" list_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (pconst const-decl "Polylist" polylist "Sturm/"))
   shostak))
 (example_7 0
  (example_7-1 nil 3622997593 ("" (sturm) nil nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (<= const-decl "bool" reals nil)
    (FALSE const-decl "bool" booleans nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (contains? const-decl "bool" RealInt "reals/")
    (expt_x1 formula-decl nil exponentiation nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (polylist_prod formula-decl nil polylist "Sturm/")
    (polylist_minus formula-decl nil polylist "Sturm/")
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__107 skolem-const-decl "Polylist" sturm_examples nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (pprod const-decl "Polylist" polylist "Sturm/")
    (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)
    (length def-decl "nat" list_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (pconst const-decl "Polylist" polylist "Sturm/")
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil))
   shostak))
 (example_8 0
  (example_8-1 nil 3622997593 ("" (sturm) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (polylist_minus formula-decl nil polylist "Sturm/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (expt_x1 formula-decl nil exponentiation nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (contains? const-decl "bool" RealInt "reals/")
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__110 skolem-const-decl "Polylist" sturm_examples nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (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)
    (length def-decl "nat" list_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/"))
   shostak))
 (example_n8 0
  (example_n8-1 nil 3622997593 ("" (sturm -1) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (polylist_minus formula-decl nil polylist "Sturm/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (expt_x1 formula-decl nil exponentiation nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (contains? const-decl "bool" RealInt "reals/")
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__113 skolem-const-decl "Polylist" sturm_examples nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (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)
    (length def-decl "nat" list_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/"))
   shostak))
 (example_80 0
  (example_80-1 nil 3622997593 ("" (sturm) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (polylist_minus formula-decl nil polylist "Sturm/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (expt_x1 formula-decl nil exponentiation nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (contains? const-decl "bool" RealInt "reals/")
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__116 skolem-const-decl "Polylist" sturm_examples nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (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)
    (length def-decl "nat" list_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/"))
   shostak))
 (example_n80 0
  (example_n80-1 nil 3622997593 ("" (sturm -1) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (polylist_minus formula-decl nil polylist "Sturm/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (expt_x1 formula-decl nil exponentiation nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (contains? const-decl "bool" RealInt "reals/")
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__119 skolem-const-decl "Polylist" sturm_examples nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (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)
    (length def-decl "nat" list_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/"))
   shostak))
 (example_9 0
  (example_9-1 nil 3622997593 ("" (sturm) nil nil)
   ((minus_real_is_real application-judgement "real" reals nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (contains? const-decl "bool" RealInt "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (polylist_minus formula-decl nil polylist "Sturm/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (polylist_neg formula-decl nil polylist "Sturm/")
    (expt_x1 formula-decl nil exponentiation nil)
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__122 skolem-const-decl "Polylist" sturm_examples nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (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)
    (length def-decl "nat" list_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (pneg const-decl "Polylist" polylist "Sturm/"))
   shostak))
 (example_n9 0
  (example_n9-1 nil 3622997593 ("" (sturm -1) nil nil)
   ((minus_real_is_real application-judgement "real" reals nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (contains? const-decl "bool" RealInt "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (polylist_minus formula-decl nil polylist "Sturm/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (polylist_neg formula-decl nil polylist "Sturm/")
    (expt_x1 formula-decl nil exponentiation nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__125 skolem-const-decl "Polylist" sturm_examples nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (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)
    (length def-decl "nat" list_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (pneg const-decl "Polylist" polylist "Sturm/"))
   shostak))
 (example_90 0
  (example_90-1 nil 3622997593 ("" (sturm) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (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)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (contains? const-decl "bool" RealInt "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__128 skolem-const-decl "{pl: Polylist |
         length(pl) = 6 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 5)}"
              sturm_examples nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (> const-decl "bool" reals nil)
    (below type-eq-decl nil nat_types nil)
    (nth def-decl "T" list_props nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (rat nonempty-type-eq-decl nil 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (length def-decl "nat" list_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/"))
   shostak))
 (example_n90 0
  (example_n90-1 nil 3622997593 ("" (sturm -1) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (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)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (contains? const-decl "bool" RealInt "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__131 skolem-const-decl "{pl: Polylist |
         length(pl) = 6 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 5)}"
              sturm_examples nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (> const-decl "bool" reals nil)
    (below type-eq-decl nil nat_types nil)
    (nth def-decl "T" list_props nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (rat nonempty-type-eq-decl nil 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (length def-decl "nat" list_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/"))
   shostak))
 (example_10 0
  (example_10-1 nil 3622997593 ("" (sturm -1) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (contains? const-decl "bool" RealInt "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (polylist_monom formula-decl nil polylist "Sturm/")
    (nzreal_exp application-judgement "nzreal" exponentiation nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__134 skolem-const-decl "{pl: Polylist |
         length(pl) = 4 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 3)}"
              sturm_examples nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (> const-decl "bool" reals nil)
    (below type-eq-decl nil nat_types nil)
    (nth def-decl "T" list_props nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (rat nonempty-type-eq-decl nil 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (length def-decl "nat" list_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/"))
   shostak))
 (example_11 0
  (example_11-1 nil 3622997593 ("" (sturm) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (<= const-decl "bool" reals nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (contains? const-decl "bool" RealInt "reals/")
    (expt_x1 formula-decl nil exponentiation nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (polylist_minus formula-decl nil polylist "Sturm/")
    (polylist_sum formula-decl nil polylist "Sturm/")
    (polylist_prod formula-decl nil polylist "Sturm/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (abs_le formula-decl nil abs_lems "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__137 skolem-const-decl "Polylist" sturm_examples nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (pprod const-decl "Polylist" polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (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)
    (length def-decl "nat" list_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (pconst const-decl "Polylist" polylist "Sturm/")
    (psum def-decl "{pql: Polylist |
         FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}"
          polylist "Sturm/"))
   shostak))
 (example_12_TCC1 0
  (example_12_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (example_12_TCC2 0
  (example_12_TCC2-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (example_12 0
  (example_12-1 nil 3622997593 ("" (sturm) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (contains? const-decl "bool" RealInt "reals/")
    (polylist_monom formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (polylist_minus formula-decl nil polylist "Sturm/")
    (polylist_sum formula-decl nil polylist "Sturm/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__140 skolem-const-decl "{pql: Polylist |
         FORALL (x):
           polylist(pql)(x) =
            polylist(pconst(1))(x) +
             polylist(pminus(pmonom(1, 120), pmonom(2, 60)))(x)}"
              sturm_examples nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (polylist const-decl "real" polylist "Sturm/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (psum def-decl "{pql: Polylist |
         FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}"
          polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (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)
    (length def-decl "nat" list_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (pconst const-decl "Polylist" polylist "Sturm/"))
   shostak))
 (legendre_TCC1 0
  (legendre_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (legendre_TCC2 0
  (legendre_TCC2-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (legendre_TCC3 0
  (legendre_TCC3-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (legendre 0
  (legendre-1 nil 3622997593 ("" (sturm) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (abs_lt formula-decl nil abs_lems "reals/")
    (polylist_minus formula-decl nil polylist "Sturm/")
    (polylist_monom formula-decl nil polylist "Sturm/")
    (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
    (polylist_sum formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (contains? const-decl "bool" RealInt "reals/")
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__143 skolem-const-decl "Polylist" sturm_examples nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (polylist const-decl "real" polylist "Sturm/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (psum def-decl "{pql: Polylist |
         FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}"
          polylist "Sturm/")
    (pconst const-decl "Polylist" polylist "Sturm/")
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields 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)
    (length def-decl "nat" list_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil))
   shostak))
 (legendre3_TCC1 0
  (legendre3_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (^ const-decl "real" exponentiation nil))
   nil))
 (legendre3 0
  (legendre3-1 nil 3622997593 ("" (sturm) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (abs_lt formula-decl nil abs_lems "reals/")
    (polylist_pow formula-decl nil polylist "Sturm/")
    (polylist_minus formula-decl nil polylist "Sturm/")
    (polylist_monom formula-decl nil polylist "Sturm/")
    (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
    (polylist_sum formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (contains? const-decl "bool" RealInt "reals/")
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__146 skolem-const-decl "Polylist" sturm_examples nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (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)
    (ppow def-decl "Polylist" polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (polylist const-decl "real" polylist "Sturm/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (psum def-decl "{pql: Polylist |
         FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}"
          polylist "Sturm/")
    (pconst const-decl "Polylist" polylist "Sturm/")
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (length def-decl "nat" list_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil))
   shostak))
 (harrison_sos_TCC1 0
  (harrison_sos_TCC1-1 nil 3624270611 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (harrison_sos_TCC2 0
  (harrison_sos_TCC2-1 nil 3624270611 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (harrison_sos 0
  (harrison_sos-1 nil 3624270612 ("" (sturm) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (contains? const-decl "bool" RealInt "reals/")
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (nat_exp application-judgement "nat" exponentiation nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (polylist_prod formula-decl nil polylist "Sturm/")
    (polylist_pow formula-decl nil polylist "Sturm/")
    (polylist_sum formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (polylist_minus formula-decl nil polylist "Sturm/")
    (polylist_div formula-decl nil polylist "Sturm/")
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__149 skolem-const-decl "Polylist" sturm_examples nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (rational nonempty-type-from-decl nil rationals nil)
    (/= const-decl "boolean" notequal nil)
    (nzrat nonempty-type-eq-decl nil rationals nil)
    (pdiv const-decl "Polylist" polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (polylist const-decl "real" polylist "Sturm/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (psum def-decl "{pql: Polylist |
         FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}"
          polylist "Sturm/")
    (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)
    (ppow def-decl "Polylist" polylist "Sturm/")
    (length def-decl "nat" list_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (pconst const-decl "Polylist" polylist "Sturm/")
    (pprod const-decl "Polylist" polylist "Sturm/"))
   shostak))
 (example_13 0
  (example_13-1 nil 3622997593 ("" (sturm) nil nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (minus_even_is_even application-judgement "even_int" integers nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (<= const-decl "bool" reals nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (expt_x1 formula-decl nil exponentiation nil)
    (rat_plus_rat_is_rat application-judgement "rat" rationals nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
    (polylist_sum formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (polylist_minus formula-decl nil polylist "Sturm/")
    (contains? const-decl "bool" RealInt "reals/")
    (Interval type-eq-decl nil interval "interval_arith/")
    (|##| const-decl "bool" interval "interval_arith/")
    ([\|\|] const-decl "Interval" interval "interval_arith/")
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__152 skolem-const-decl "Polylist" sturm_examples nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (polylist const-decl "real" polylist "Sturm/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (psum def-decl "{pql: Polylist |
         FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}"
          polylist "Sturm/")
    (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)
    (length def-decl "nat" list_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (pconst const-decl "Polylist" polylist "Sturm/")
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil))
   shostak))
 (example_14 0
  (example_14-1 nil 3622997594 ("" (sturm) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (<= const-decl "bool" reals nil)
    (FALSE const-decl "bool" booleans nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (RealInf type-decl nil RealInt "reals/")
    ([\|\|] const-decl "RealInt" RealInt "reals/")
    (inf? adt-recognizer-decl "[RealInf -> boolean]" RealInt "reals/")
    (oo adt-constructor-decl "(inf?)" RealInt "reals/")
    (|##| const-decl "bool" RealInt "reals/")
    (contains? const-decl "bool" RealInt "reals/")
    (minus_real_is_real application-judgement "real" reals nil)
    (polylist_neg formula-decl nil polylist "Sturm/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__155 skolem-const-decl "Polylist" sturm_examples nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (pneg const-decl "Polylist" polylist "Sturm/")
    (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)
    (length def-decl "nat" list_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/"))
   shostak))
 (example_15 0
  (example_15-1 nil 3622997594 ("" (sturm) nil nil)
   ((minus_real_is_real application-judgement "real" reals nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (RealInf type-decl nil RealInt "reals/")
    ([\|\|] const-decl "RealInt" RealInt "reals/")
    (open? adt-recognizer-decl "[RealInf -> boolean]" RealInt "reals/")
    (open adt-constructor-decl "[real -> (open?)]" RealInt "reals/")
    (inf? adt-recognizer-decl "[RealInf -> boolean]" RealInt "reals/")
    (oo adt-constructor-decl "(inf?)" RealInt "reals/")
    (|##| const-decl "bool" RealInt "reals/")
    (contains? const-decl "bool" RealInt "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (polylist_minus formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (polylist_neg formula-decl nil polylist "Sturm/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__158 skolem-const-decl "Polylist" sturm_examples nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (pneg const-decl "Polylist" polylist "Sturm/")
    (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)
    (length def-decl "nat" list_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (pconst const-decl "Polylist" polylist "Sturm/"))
   shostak))
 (example_16 0
  (example_16-1 nil 3622997594 ("" (sturm) nil nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (<= const-decl "bool" reals nil)
    (FALSE const-decl "bool" booleans nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (RealInf type-decl nil RealInt "reals/")
    ([\|\|] const-decl "RealInt" RealInt "reals/")
    (inf? adt-recognizer-decl "[RealInf -> boolean]" RealInt "reals/")
    (Inf type-eq-decl nil RealInt "reals/")
    (ninf? adt-recognizer-decl "[RealInf -> boolean]" RealInt "reals/")
    (nInf type-eq-decl nil RealInt "reals/")
    (- const-decl "nInf" RealInt "reals/")
    (oo adt-constructor-decl "(inf?)" RealInt "reals/")
    (expt_x1 formula-decl nil exponentiation nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (polylist_prod formula-decl nil polylist "Sturm/")
    (polylist_minus formula-decl nil polylist "Sturm/")
    (contains? const-decl "bool" RealInt "reals/")
    (|##| const-decl "bool" RealInt "reals/")
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__161 skolem-const-decl "Polylist" sturm_examples nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (pprod const-decl "Polylist" polylist "Sturm/")
    (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)
    (length def-decl "nat" list_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (pconst const-decl "Polylist" polylist "Sturm/")
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil))
   shostak))
 (example_17_TCC1 0
  (example_17_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (example_17_TCC2 0
  (example_17_TCC2-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (example_17_TCC3 0
  (example_17_TCC3-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (example_17_TCC4 0
  (example_17_TCC4-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (example_17 0
  (example_17-1 nil 3622997594 ("" (sturm) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (FALSE const-decl "bool" booleans nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (contains? const-decl "bool" RealInt "reals/")
    (polylist_prod formula-decl nil polylist "Sturm/")
    (polylist_pow formula-decl nil polylist "Sturm/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (polylist_minus formula-decl nil polylist "Sturm/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (polylist_const formula-decl nil polylist "Sturm/")
    (polylist_monom formula-decl nil polylist "Sturm/")
    (expt_x1 formula-decl nil exponentiation nil)
    (sturm const-decl "bool" poly_strategy "Sturm/")
    (stu__164 skolem-const-decl "Polylist" sturm_examples nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (sturm_def formula-decl nil poly_strategy "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (deg const-decl "{d: below(length(pl)) |
         (d > 0 IFF
           (EXISTS (j: below(length(pl))): j > 0 AND nth(pl, j) /= 0))
          AND
          (d > 0 IMPLIES
            (FORALL (j: below(length(pl))): j > d IMPLIES nth(pl, j) = 0))
           AND (d > 0 IMPLIES nth(pl, d) /= 0)}" polylist "Sturm/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (> const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (pprod const-decl "Polylist" polylist "Sturm/")
    (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)
    (length def-decl "nat" list_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (ppow def-decl "Polylist" polylist "Sturm/")
    (pminus const-decl "Polylist" polylist "Sturm/")
    (pconst const-decl "Polylist" polylist "Sturm/"))
   shostak))
 (mono_example_1_TCC1 0
  (mono_example_1_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil) nil
   nil))
 (mono_example_1 0
  (mono_example_1-1 nil 3622997594 ("" (mono-poly) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (mono_def formula-decl nil compute_sturm "Sturm/")
    (mono const-decl "bool" compute_sturm "Sturm/")
    (lp__171 skolem-const-decl "[nat -> rat]" sturm_examples nil)
    (pl__169 skolem-const-decl "(cons?[numfield])" sturm_examples nil)
    (polylist_sum formula-decl nil polylist "Sturm/")
    (polylist_minus formula-decl nil polylist "Sturm/")
    (polylist_prod formula-decl nil polylist "Sturm/")
    (polylist_pow formula-decl nil polylist "Sturm/")
    (polylist_const formula-decl nil polylist "Sturm/")
    (polylist_monom formula-decl nil polylist "Sturm/")
    (expt_x1 formula-decl nil exponentiation nil)
    (p1__167 skolem-const-decl "Polylist" sturm_examples nil)
    (p2__168 skolem-const-decl "{pql: Polylist |
         FORALL (x):
           polylist(pql)(x) =
            polylist(pconst(1/16))(x) +
             polylist(pminus(pprod(pmonom(1, 1), pmonom(1, 1)),
                             pmonom(1/2, 1)))
                     (x)}" sturm_examples nil)
    (polylist_eval formula-decl nil polylist "Sturm/")
    (xval__170 skolem-const-decl "[# bounded_above: bool,
   bounded_below: bool,
   closed_above: bool,
   closed_below: bool,
   lb: posint,
   ub: posint #]" sturm_examples nil)
    (contains? const-decl "bool" RealInt "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (posnat nonempty-type-eq-decl nil integers nil)
    (relvar__174 skolem-const-decl "RealOrder" sturm_examples nil)
    (rel__173 skolem-const-decl "RealOrder" sturm_examples nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (deg__172 skolem-const-decl "int" sturm_examples nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (< const-decl "bool" reals nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<= const-decl "bool" reals nil)
    (realorder? const-decl "bool" real_orders "reals/")
    (RealOrder type-eq-decl nil real_orders "reals/")
    (int_minus_int_is_int application-judgement "int" integers nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (list2array def-decl "T" array2list "structures/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posint nonempty-type-eq-decl nil integers nil)
    (FALSE const-decl "bool" booleans nil)
    (pprod const-decl "Polylist" polylist "Sturm/")
    (psum def-decl "{pql: Polylist |
         FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}"
          polylist "Sturm/")
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (pconst const-decl "Polylist" polylist "Sturm/")
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (length def-decl "nat" list_props nil)
    (pminus const-decl "Polylist" polylist "Sturm/")
    (ppow def-decl "Polylist" polylist "Sturm/")
    (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)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (every adt-def-decl "boolean" list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (list type-decl nil list_adt nil)
    (number nonempty-type-decl nil numbers nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil))
   shostak))
 (mono_example_2_TCC1 0
  (mono_example_2_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (mono_example_2 0
  (mono_example_2-1 nil 3622997594 ("" (mono-poly) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (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)
    (mono_def formula-decl nil compute_sturm "Sturm/")
    (mono const-decl "bool" compute_sturm "Sturm/")
    (contains? const-decl "bool" RealInt "reals/")
    (xval__180 skolem-const-decl "[# bounded_above: bool,
   bounded_below: bool,
   closed_above: bool,
   closed_below: bool,
   lb: odd_int,
   ub: posint #]" sturm_examples nil)
    (polylist_eval formula-decl nil polylist "Sturm/")
    (p2__178 skolem-const-decl "{pl: Polylist |
         length(pl) = 6 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 5)}"
             sturm_examples nil)
    (p1__177 skolem-const-decl "{pl: Polylist |
         length(pl) = 6 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 5)}"
             sturm_examples nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (pl__179 skolem-const-decl "(cons?)" sturm_examples nil)
    (lp__181 skolem-const-decl "[nat -> rat]" sturm_examples nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (posnat nonempty-type-eq-decl nil integers nil)
    (relvar__184 skolem-const-decl "RealOrder" sturm_examples nil)
    (rel__183 skolem-const-decl "[[real, real] -> boolean]"
              sturm_examples nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (deg__182 skolem-const-decl "int" sturm_examples nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (< const-decl "bool" reals nil)
    (realorder? const-decl "bool" real_orders "reals/")
    (RealOrder type-eq-decl nil real_orders "reals/")
    (int_minus_int_is_int application-judgement "int" integers nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (list2array def-decl "T" array2list "structures/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (odd? const-decl "bool" integers nil)
    (odd_int nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posint nonempty-type-eq-decl nil integers nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (FALSE const-decl "bool" booleans nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (length def-decl "nat" list_props nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (every adt-def-decl "boolean" list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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 "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (list type-decl nil list_adt nil)
    (number nonempty-type-decl nil numbers nil))
   shostak))
 (mono_example_3_TCC1 0
  (mono_example_3_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (mono_example_3_TCC2 0
  (mono_example_3_TCC2-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (mono_example_3 0
  (mono_example_3-1 nil 3622997594 ("" (mono-poly) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (mono_def formula-decl nil compute_sturm "Sturm/")
    (mono const-decl "bool" compute_sturm "Sturm/")
    (lp__191 skolem-const-decl "[nat -> rat]" sturm_examples nil)
    (pl__189 skolem-const-decl "(cons?[numfield])" sturm_examples nil)
    (polylist_sum formula-decl nil polylist "Sturm/")
    (polylist_minus formula-decl nil polylist "Sturm/")
    (polylist_prod formula-decl nil polylist "Sturm/")
    (polylist_div formula-decl nil polylist "Sturm/")
    (polylist_monom formula-decl nil polylist "Sturm/")
    (expt_x1 formula-decl nil exponentiation nil)
    (polylist_const formula-decl nil polylist "Sturm/")
    (p1__187 skolem-const-decl "{pql: Polylist |
         FORALL (x):
           polylist(pql)(x) =
            polylist(pdiv(pmonom(1, 1), 5))(x) +
             polylist(pminus(pmonom(1, 5), pmonom(1, 3)))(x)}"
             sturm_examples nil)
    (p2__188 skolem-const-decl "Polylist" sturm_examples nil)
    (polylist_eval formula-decl nil polylist "Sturm/")
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (xval__190 skolem-const-decl "[# bounded_above: bool,
   bounded_below: bool,
   closed_above: bool,
   closed_below: bool,
   lb: posrat,
   ub: posrat #]" sturm_examples nil)
    (contains? const-decl "bool" RealInt "reals/")
    (RealInt type-eq-decl nil RealInt "reals/")
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (relvar__194 skolem-const-decl "RealOrder" sturm_examples nil)
    (rel__193 skolem-const-decl "RealOrder" sturm_examples nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (deg__192 skolem-const-decl "int" sturm_examples nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (< const-decl "bool" reals nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (realorder? const-decl "bool" real_orders "reals/")
    (RealOrder type-eq-decl nil real_orders "reals/")
    (int_minus_int_is_int application-judgement "int" integers nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (list2array def-decl "T" array2list "structures/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (nonneg_rat nonempty-type-eq-decl nil rationals nil)
    (> const-decl "bool" reals nil)
    (posrat nonempty-type-eq-decl nil rationals nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (pconst const-decl "Polylist" polylist "Sturm/")
    (pprod const-decl "Polylist" polylist "Sturm/")
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (pdiv const-decl "Polylist" polylist "Sturm/")
    (nzrat nonempty-type-eq-decl nil rationals nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (length def-decl "nat" list_props nil)
    (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)
    (pminus const-decl "Polylist" polylist "Sturm/")
    (psum def-decl "{pql: Polylist |
         FORALL (x): polylist(pql)(x) = polylist(pl)(x) + polylist(ql)(x)}"
          polylist "Sturm/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (Polylist type-eq-decl nil polylist "Sturm/")
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (every adt-def-decl "boolean" list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (list type-decl nil list_adt nil)
    (number nonempty-type-decl nil numbers nil))
   shostak))
 (mono_example_4_TCC1 0
  (mono_example_4_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (mono_example_4 0
  (mono_example_4-1 nil 3622997594 ("" (mono-poly) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (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)
    (mono_def formula-decl nil compute_sturm "Sturm/")
    (< const-decl "bool" reals nil)
    (mono const-decl "bool" compute_sturm "Sturm/")
    (contains? const-decl "bool" RealInt "reals/")
    (xval__200 skolem-const-decl "[# bounded_above: bool,
   bounded_below: bool,
   closed_above: bool,
   closed_below: bool,
   lb: odd_int,
   ub: posint #]" sturm_examples nil)
    (polylist_eval formula-decl nil polylist "Sturm/")
    (p2__198 skolem-const-decl "{pl: Polylist |
         length(pl) = 4 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 3)}"
             sturm_examples nil)
    (p1__197 skolem-const-decl "{pl: Polylist |
         length(pl) = 4 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 3)}"
             sturm_examples nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (pl__199 skolem-const-decl "(cons?)" sturm_examples nil)
    (lp__201 skolem-const-decl "[nat -> rat]" sturm_examples nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (posnat nonempty-type-eq-decl nil integers nil)
    (relvar__204 skolem-const-decl "[[real, real] -> boolean]"
                 sturm_examples nil)
    (rel__203 skolem-const-decl "[[real, real] -> boolean]"
              sturm_examples nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (deg__202 skolem-const-decl "int" sturm_examples nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (list2array def-decl "T" array2list "structures/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (odd? const-decl "bool" integers nil)
    (odd_int nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posint nonempty-type-eq-decl nil integers nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (FALSE const-decl "bool" booleans nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (length def-decl "nat" list_props nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (every adt-def-decl "boolean" list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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 "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (list type-decl nil list_adt nil)
    (number nonempty-type-decl nil numbers nil))
   shostak))
 (mono_example_5 0
  (mono_example_5-1 nil 3622997594 ("" (mono-poly) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (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)
    (mono_def formula-decl nil compute_sturm "Sturm/")
    (mono const-decl "bool" compute_sturm "Sturm/")
    (contains? const-decl "bool" RealInt "reals/")
    (lp__211 skolem-const-decl "[nat -> rat]" sturm_examples nil)
    (xval__210 skolem-const-decl "[# bounded_above: bool,
   bounded_below: bool,
   closed_above: bool,
   closed_below: bool,
   lb: odd_int,
   ub: posint #]" sturm_examples nil)
    (polylist_eval formula-decl nil polylist "Sturm/")
    (p2__208 skolem-const-decl "Polylist" sturm_examples nil)
    (p1__207 skolem-const-decl "{pl: Polylist |
         length(pl) = 3 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 2)}"
             sturm_examples nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (polylist_monom formula-decl nil polylist "Sturm/")
    (polylist_sq formula-decl nil polylist "Sturm/")
    (expt_x1 formula-decl nil exponentiation nil)
    (pl__209 skolem-const-decl "(cons?)" sturm_examples nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (posnat nonempty-type-eq-decl nil integers nil)
    (relvar__214 skolem-const-decl "RealOrder" sturm_examples nil)
    (rel__213 skolem-const-decl "RealOrder" sturm_examples nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (deg__212 skolem-const-decl "int" sturm_examples nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (< const-decl "bool" reals nil)
    (realorder? const-decl "bool" real_orders "reals/")
    (RealOrder type-eq-decl nil real_orders "reals/")
    (int_minus_int_is_int application-judgement "int" integers nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (list2array def-decl "T" array2list "structures/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (odd? const-decl "bool" integers nil)
    (odd_int nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posint nonempty-type-eq-decl nil integers nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (FALSE const-decl "bool" booleans nil)
    (psq const-decl "Polylist" polylist "Sturm/")
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (length def-decl "nat" list_props nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (every adt-def-decl "boolean" list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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 "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (list type-decl nil list_adt nil)
    (number nonempty-type-decl nil numbers nil))
   shostak))
 (mono_example_6_TCC1 0
  (mono_example_6_TCC1-1 nil 3622997593 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (mono_example_6 0
  (mono_example_6-1 nil 3622997594 ("" (mono-poly) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (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)
    (mono_def formula-decl nil compute_sturm "Sturm/")
    (< const-decl "bool" reals nil)
    (mono const-decl "bool" compute_sturm "Sturm/")
    (contains? const-decl "bool" RealInt "reals/")
    (lp__221 skolem-const-decl "[nat -> rat]" sturm_examples nil)
    (xval__220 skolem-const-decl "[# bounded_above: bool,
   bounded_below: bool,
   closed_above: bool,
   closed_below: bool,
   lb: odd_int,
   ub: naturalnumber #]" sturm_examples nil)
    (polylist_eval formula-decl nil polylist "Sturm/")
    (p2__218 skolem-const-decl "{pl: Polylist |
         length(pl) = 5 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 4)}"
             sturm_examples nil)
    (p1__217 skolem-const-decl "{pl: Polylist |
         length(pl) = 5 AND (FORALL (x: real): polylist(pl)(x) = 1 * x ^ 4)}"
             sturm_examples nil)
    (x_226 skolem-const-decl "real" sturm_examples nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (polylist_monom formula-decl nil polylist "Sturm/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (pl__219 skolem-const-decl "(cons?)" sturm_examples nil)
    (RealInt type-eq-decl nil RealInt "reals/")
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (relvar__224 skolem-const-decl "RealOrder" sturm_examples nil)
    (rel__223 skolem-const-decl "RealOrder" sturm_examples nil)
    (SturmRel? const-decl "bool" compute_sturm "Sturm/")
    (deg__222 skolem-const-decl "int" sturm_examples nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (realorder? const-decl "bool" real_orders "reals/")
    (RealOrder type-eq-decl nil real_orders "reals/")
    (int_minus_int_is_int application-judgement "int" integers nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (list2array def-decl "T" array2list "structures/")
    (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
    (listn_0 name-judgement "listn[real](0)" polynomial_division
     "Sturm/")
    (listn_0 name-judgement "listn[rat](0)" polylist "Sturm/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (odd? const-decl "bool" integers nil)
    (odd_int nonempty-type-eq-decl nil integers nil)
    (naturalnumber type-eq-decl nil naturalnumbers nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (FALSE const-decl "bool" booleans nil)
    (pmonom def-decl "{pl: Polylist |
         length(pl) = deg + 1 AND
          (FORALL (x: real): polylist(pl)(x) = c * x ^ deg)}" polylist
            "Sturm/")
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (polylist const-decl "real" polylist "Sturm/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (length def-decl "nat" list_props nil)
    (Polylist type-eq-decl nil polylist "Sturm/")
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (every adt-def-decl "boolean" list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (rat nonempty-type-eq-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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 "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (list type-decl nil list_adt nil)
    (number nonempty-type-decl nil numbers nil))
   shostak)))