(sq
 (sq_TCC1 0 (sq_TCC1-1 nil 3255279994 ("" (ground) nil nil) nil nil))
 (sq_nz_pos 0
  (sq_nz_pos-1 nil 3255279994 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (/= const-decl "boolean" notequal 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)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sq const-decl "nonneg_real" sq nil))
   nil))
 (sq_rew 0
  (sq_rew-1 nil 3255279994 ("" (grind) nil nil)
   ((sq const-decl "nonneg_real" sq nil)) nil))
 (sq_expt2_TCC1 0
  (sq_expt2_TCC1-1 nil 3549709855 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (sq_expt2 0
  (sq_expt2-1 nil 3549709856 ("" (grind) nil nil)
   ((sq const-decl "nonneg_real" sq nil)
    (expt def-decl "real" exponentiation nil)
    (^ const-decl "real" exponentiation nil))
   shostak))
 (sq_neg 0
  (sq_neg-1 nil 3255279994 ("" (grind) nil nil)
   ((sq const-decl "nonneg_real" sq nil)
    (minus_real_is_real application-judgement "real" reals nil))
   nil))
 (sq_pos 0
  (sq_pos-1 nil 3255279994
   ("" (skosimp*) (("" (expand "sq") (("" (assert) nil nil)) nil)) nil)
   ((sq const-decl "nonneg_real" sq nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
 (sq_plus_pos 0
  (sq_plus_pos-1 nil 3255279994
   ("" (skolem 1 ("a" "b"))
    (("" (case "sq(a)>=0" "sq(b) >= 0")
      (("1" (ground) nil nil) ("2" (rewrite "sq_pos") nil nil)
       ("3" (rewrite "sq_pos") nil nil))
      nil))
    nil)
   ((sq const-decl "nonneg_real" sq nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq_pos formula-decl nil sq nil))
   nil))
 (sq_times 0
  (sq_times-1 nil 3255279994 ("" (grind) nil nil)
   ((sq const-decl "nonneg_real" sq nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
 (sq_plus 0
  (sq_plus-1 nil 3255279994 ("" (grind) nil nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sq const-decl "nonneg_real" sq nil))
   nil))
 (sq_minus 0
  (sq_minus-1 nil 3255279994 ("" (grind) 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)
    (sq const-decl "nonneg_real" sq nil))
   nil))
 (sq_neg_minus 0
  (sq_neg_minus-1 nil 3255279994 ("" (grind) nil nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sq const-decl "nonneg_real" sq nil))
   nil))
 (sq_abs 0
  (sq_abs-1 nil 3255280284 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (sq const-decl "nonneg_real" sq nil))
   shostak))
 (sq_abs_neg 0
  (sq_abs_neg-1 nil 3255280291 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (sq const-decl "nonneg_real" sq nil))
   shostak))
 (sq_0 0
  (sq_0-1 nil 3255279994 ("" (grind) nil nil)
   ((sq const-decl "nonneg_real" sq nil)) nil))
 (sq_1 0
  (sq_1-1 nil 3255279994 ("" (grind) nil nil)
   ((sq const-decl "nonneg_real" sq nil)
    (sq_nz_pos application-judgement "posreal" sq nil))
   nil))
 (sq_eq_0 0
  (sq_eq_0-1 nil 3255279994
   ("" (skosimp*)
    (("" (expand "sq")
      (("" (lemma "zero_times3")
        (("" (inst?) (("" (ground) nil nil)) nil)) nil))
      nil))
    nil)
   ((sq const-decl "nonneg_real" sq nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil 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)
    (zero_times3 formula-decl nil real_props nil))
   nil))
 (sq_gt_0 0
  (sq_gt_0-1 nil 3255279994
   ("" (skosimp*)
    (("" (expand "sq")
      (("" (lemma "pos_times_gt")
        (("" (inst?) (("" (ground) nil nil)) nil)) nil))
      nil))
    nil)
   ((sq const-decl "nonneg_real" sq nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil 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)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (pos_times_gt formula-decl nil real_props nil))
   nil))
 (sq_div_TCC1 0
  (sq_div_TCC1-1 nil 3255279994
   ("" (skolem 1 "d")
    (("" (ground) (("" (rewrite "sq_eq_0") nil nil)) nil)) 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (sq_eq_0 formula-decl nil sq nil))
   nil))
 (sq_div 0
  (sq_div-1 nil 3255279994 ("" (grind) nil nil)
   ((/= const-decl "boolean" notequal nil)
    (sq const-decl "nonneg_real" sq nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil))
   nil))
 (sq_plus_eq_0 0
  (sq_plus_eq_0-1 nil 3255279994
   ("" (skolem 1 ("a" "b"))
    (("" (ground)
      (("1" (lemma "sq_pos")
        (("1" (inst -1 "b")
          (("1" (case "sq(a)>0")
            (("1" (ground) nil nil)
             ("2" (delete -)
              (("2" (expand "sq")
                (("2" (rewrite "pos_times_gt") (("2" (ground) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (lemma "sq_pos")
        (("2" (inst -1 "a")
          (("2" (case "sq(b)>0")
            (("1" (ground) nil nil)
             ("2" (delete -)
              (("2" (expand "sq")
                (("2" (rewrite "pos_times_gt") (("2" (ground) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("3" (grind) nil nil))
      nil))
    nil)
   ((nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil 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)
    (pos_times_gt formula-decl nil real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (> const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (sq_pos formula-decl nil sq nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
 (sq_ge 0
  (sq_ge-1 nil 3255279994
   ("" (skosimp*)
    (("" (ground)
      (("1" (case "nna!1 < nnb!1")
        (("1" (case "sq(nna!1) < sq(nnb!1)")
          (("1" (ground) nil nil)
           ("2" (hide -2 2)
            (("2" (lemma "lt_times_lt_pos1")
              (("2" (inst -1 "nna!1" "nna!1" "nnb!1" "nnb!1")
                (("1" (ground)
                  (("1" (expand "sq") (("1" (propax) nil nil)) nil))
                  nil)
                 ("2" (ground)
                  (("2" (case "nna!1=0")
                    (("1" (ground)
                      (("1" (replace -1 :hide? t)
                        (("1" (expand "sq")
                          (("1" (ground)
                            (("1" (rewrite "pos_times_lt") nil nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (ground) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (ground) nil nil))
        nil)
       ("2" (lemma "ge_times_ge_pos")
        (("2" (inst?)
          (("2" (inst -1 "nnb!1" "nna!1")
            (("2" (ground)
              (("2" (expand "sq") (("2" (propax) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq const-decl "nonneg_real" sq nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_times_lt_pos1 formula-decl nil real_props nil)
    (pos_times_lt formula-decl nil real_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nna!1 skolem-const-decl "nonneg_real" sq nil)
    (> const-decl "bool" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (ge_times_ge_pos formula-decl nil real_props nil))
   nil))
 (sq_le 0
  (sq_le-1 nil 3255279994
   ("" (lemma "sq_ge")
    (("" (skolem 1 ("nna" "nnb"))
      (("" (inst -1 "nnb" "nna") (("" (ground) nil nil)) nil)) nil))
    nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (sq_ge formula-decl nil sq nil))
   nil))
 (sq_gt 0
  (sq_gt-1 nil 3255279994
   ("" (skosimp*)
    (("" (ground)
      (("1" (case "nna!1 <= nnb!1")
        (("1" (case "sq(nna!1) <= sq(nnb!1)")
          (("1" (ground) nil nil)
           ("2" (hide -2 2)
            (("2" (lemma "le_times_le_pos")
              (("2" (inst -1 "nna!1" "nna!1" "nnb!1" "nnb!1")
                (("2" (ground)
                  (("2" (expand "sq") (("2" (propax) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (ground) nil nil))
        nil)
       ("2" (lemma "gt_times_gt_pos1")
        (("2" (inst?)
          (("2" (inst -1 "nnb!1" "nna!1")
            (("1" (assert)
              (("1" (hide -2)
                (("1" (expand "sq") (("1" (propax) nil nil)) nil))
                nil))
              nil)
             ("2" (case-replace "nnb!1 = 0")
              (("1" (hide -1 1)
                (("1" (expand "sq" 1 2)
                  (("1" (lemma "sq_pos")
                    (("1" (inst?)
                      (("1" (assert)
                        (("1" (lemma "sq_eq_0")
                          (("1" (inst?) (("1" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sq const-decl "nonneg_real" sq nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_times_le_pos formula-decl nil real_props nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sq_eq_0 formula-decl nil sq nil) (sq_pos formula-decl nil sq nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nnb!1 skolem-const-decl "nonneg_real" sq nil)
    (gt_times_gt_pos1 formula-decl nil real_props nil))
   nil))
 (sq_lt 0
  (sq_lt-1 nil 3255279994
   ("" (skolem 1 ("nna" "nnb"))
    (("" (lemma "sq_gt")
      (("" (inst -1 "nnb" "nna") (("" (ground) nil nil)) nil)) nil))
    nil)
   ((sq_gt formula-decl nil sq nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   nil))
 (sq_eq 0
  (sq_eq-1 nil 3255279994
   ("" (skosimp*)
    (("" (case-replace "nna!1 = 0")
      (("1" (lemma "sq_eq_0")
        (("1" (inst -1 "nnb!1")
          (("1" (expand "sq") (("1" (ground) nil nil)) nil)) nil))
        nil)
       ("2" (case-replace "nnb!1 = 0")
        (("1" (lemma "sq_eq_0")
          (("1" (inst?)
            (("1" (expand "sq") (("1" (propax) nil nil)) nil)) nil))
          nil)
         ("2" (ground)
          (("2" (lemma "both_sides_expt2_aux")
            (("2" (inst -1 "2" "nna!1" "nnb!1")
              (("2" (expand "expt")
                (("2" (expand "expt")
                  (("2" (expand "expt")
                    (("2" (expand "sq") (("2" (propax) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((number nonempty-type-decl nil numbers 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (sq_eq_0 formula-decl nil sq nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (expt def-decl "real" exponentiation nil)
    (nnreal_expt application-judgement "nnreal" exponentiation nil)
    (both_sides_expt2_aux formula-decl nil exponentiation nil))
   nil))
 (sq_neg_pos_le 0
  (sq_neg_pos_le-1 nil 3255279994
   ("" (skolem 1 ("a" "c"))
    (("" (case "a >= 0")
      (("1" (lemma "sq_le")
        (("1" (inst -1 "a" "c") (("1" (ground) nil nil)) nil)) nil)
       ("2" (lemma "sq_le")
        (("2" (inst -1 "-a" "c")
          (("1" (case-replace "sq(-a) = sq(a)")
            (("1" (hide -1) (("1" (ground) nil nil)) nil)
             ("2" (hide -1 3)
              (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
            nil)
           ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (a skolem-const-decl "real" sq nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq_le formula-decl nil sq nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sq const-decl "nonneg_real" sq nil))
   nil))
 (neg_pos_sq_le 0
  (neg_pos_sq_le-1 nil 3255279994
   ("" (skolem 1 ("a" "b"))
    (("" (ground)
      (("" (case "a > 0")
        (("1" (lemma "sq_le")
          (("1" (inst -1 "a" "b")
            (("1" (ground) nil nil) ("2" (ground) nil nil)) nil))
          nil)
         ("2" (case "-a <= b")
          (("1" (lemma "sq_le")
            (("1" (inst -1 "-a" "b")
              (("1" (ground) (("1" (rewrite "sq_neg") nil nil)) nil)
               ("2" (ground) nil nil))
              nil))
            nil)
           ("2" (ground) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (<= const-decl "bool" reals nil) (sq_neg formula-decl nil sq nil)
    (sq_le formula-decl nil sq nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (a skolem-const-decl "real" sq nil)
    (>= const-decl "bool" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (> const-decl "bool" reals nil))
   nil))
 (sq_neg_pos_lt 0
  (sq_neg_pos_lt-1 nil 3255279994
   ("" (skolem 1 ("a" "c"))
    (("" (case "a >= 0")
      (("1" (lemma "sq_lt")
        (("1" (inst -1 "a" "c") (("1" (ground) nil nil)) nil)) nil)
       ("2" (lemma "sq_lt")
        (("2" (inst -1 "-a" "c")
          (("1" (case-replace "sq(-a) = sq(a)")
            (("1" (ground) nil nil)
             ("2" (hide -1 3)
              (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
            nil)
           ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (a skolem-const-decl "real" sq nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sq_lt formula-decl nil sq nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sq const-decl "nonneg_real" sq nil))
   nil))
 (neg_pos_sq_lt 0
  (neg_pos_sq_lt-1 nil 3255279994
   ("" (skolem 1 ("a" "b"))
    (("" (ground)
      (("" (case "a > 0")
        (("1" (lemma "sq_lt")
          (("1" (inst -1 "a" "b")
            (("1" (ground) nil nil) ("2" (ground) nil nil)) nil))
          nil)
         ("2" (case "-a < b")
          (("1" (lemma "sq_lt")
            (("1" (inst -1 "-a" "b")
              (("1" (ground) (("1" (rewrite "sq_neg") nil nil)) nil)
               ("2" (ground) nil nil))
              nil))
            nil)
           ("2" (ground) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil) (sq_neg formula-decl nil sq nil)
    (sq_lt formula-decl nil sq nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (a skolem-const-decl "real" sq nil)
    (>= const-decl "bool" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (> const-decl "bool" reals nil))
   nil))
 (sq_le_abs 0
  (sq_le_abs-1 nil 3255279994
   ("" (skosimp*)
    (("" (case-replace "b!1 >= 0")
      (("1" (lemma "sq_neg_pos_le")
        (("1" (inst?)
          (("1" (expand "abs")
            (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
          nil))
        nil)
       ("2" (lemma "sq_neg_pos_le")
        (("2" (inst -1 "a!1" "-b!1")
          (("1" (case-replace "sq(-b!1) = sq(b!1)")
            (("1" (hide -1)
              (("1" (expand "abs")
                (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
              nil)
             ("2" (hide -1 3)
              (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
            nil)
           ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (b!1 skolem-const-decl "real" sq nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (sq_neg_pos_le formula-decl nil sq nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sq const-decl "nonneg_real" sq nil))
   nil))
 (sq_lt_abs 0
  (sq_lt_abs-1 nil 3255279994
   ("" (skosimp*)
    (("" (case-replace "b!1 >= 0")
      (("1" (lemma "sq_neg_pos_lt")
        (("1" (inst?)
          (("1" (expand "abs")
            (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
          nil))
        nil)
       ("2" (lemma "sq_neg_pos_lt")
        (("2" (inst -1 "a!1" "-b!1")
          (("1" (case-replace "sq(-b!1) = sq(b!1)")
            (("1" (hide -1)
              (("1" (expand "abs")
                (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
              nil)
             ("2" (hide -1 3)
              (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
            nil)
           ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (b!1 skolem-const-decl "real" sq nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (sq_neg_pos_lt formula-decl nil sq nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sq const-decl "nonneg_real" sq nil))
   nil))
 (sq_ge_abs 0
  (sq_ge_abs-1 nil 3256039469
   ("" (skosimp*)
    (("" (lemma "sq_le_abs")
      (("" (inst -1 "b!1" "a!1") (("" (ground) nil nil)) nil)) nil))
    nil)
   ((sq_le_abs formula-decl nil sq nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   nil))
 (sq_gt_abs 0
  (sq_gt_abs-1 nil 3256039548
   ("" (skosimp*)
    (("" (lemma "sq_lt_abs")
      (("" (inst -1 "b!1" "a!1")
        (("" (assert) (("" (ground) nil nil)) nil)) nil))
      nil))
    nil)
   ((sq_lt_abs formula-decl nil sq nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   shostak))
 (sq_eq_abs 0
  (sq_eq_abs-1 nil 3255279994
   ("" (skosimp*)
    (("" (case "a!1 >= 0")
      (("1" (case "b!1 >= 0")
        (("1" (rewrite "sq_eq") (("1" (grind) nil nil)) nil)
         ("2" (case-replace "sq(b!1) = sq(-b!1)")
          (("1" (hide -1)
            (("1" (rewrite "sq_eq") (("1" (grind) nil nil)) nil)) nil)
           ("2" (hide 3)
            (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
          nil))
        nil)
       ("2" (case "b!1 >= 0")
        (("1" (case-replace "sq(a!1) = sq(-a!1)")
          (("1" (hide -1)
            (("1" (rewrite "sq_eq") (("1" (grind) nil nil)) nil)) nil)
           ("2" (hide 3)
            (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
          nil)
         ("2" (case-replace "sq(a!1) = sq(-a!1)")
          (("1" (case-replace "sq(b!1) = sq(-b!1)")
            (("1" (hide -1 -2)
              (("1" (rewrite "sq_eq") (("1" (grind) nil nil)) nil))
              nil)
             ("2" (hide -1 4)
              (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
            nil)
           ("2" (hide 4)
            (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sq const-decl "nonneg_real" sq nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq_eq formula-decl nil sq nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (sq_eq_rew 0
  (sq_eq_rew-1 nil 3409051947
   ("" (skosimp*) (("" (assert) nil nil)) nil) nil shostak))
 (triangle_rectangle 0
  (triangle_rectangle-1 nil 3255279994
   ("" (skolem 1 ("a" "b" "c"))
    (("" (flatten)
      (("" (case "sq(a)>=0" "sq(b)>=0" "sq(c)>=0")
        (("1" (case "sq(a) <= sq(c)")
          (("1" (case "sq(b) <= sq(c)")
            (("1" (lemma "sq_neg_pos_le")
              (("1" (inst-cp -1 "a" "c")
                (("1" (inst -1 "b" "c") (("1" (ground) nil nil)) nil))
                nil))
              nil)
             ("2" (hide 2 -1) (("2" (ground) nil nil)) nil))
            nil)
           ("2" (hide 2 -1) (("2" (ground) nil nil)) nil))
          nil)
         ("2" (rewrite "sq_pos") nil nil)
         ("3" (rewrite "sq_pos") nil nil)
         ("4" (rewrite "sq_pos") nil nil))
        nil))
      nil))
    nil)
   ((sq_pos formula-decl nil sq nil) (<= const-decl "bool" reals nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq_neg_pos_le formula-decl nil sq nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil))
   nil))
 (triangle_ineq_lt 0
  (triangle_ineq_lt-1 nil 3255279994
   ("" (skosimp*)
    (("" (lemma "sq_lt_abs")
      (("" (inst?)
        (("" (assert)
          (("" (lemma "sq_lt_abs")
            (("" (inst -1 "b!1" "d!1") (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sq_lt_abs formula-decl nil sq nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   nil))
 (triangle_ineq_le 0
  (triangle_ineq_le-1 nil 3255279994
   ("" (skosimp*)
    (("" (lemma "sq_le_abs")
      (("" (inst?)
        (("" (assert)
          (("" (lemma "sq_le_abs")
            (("" (inst -1 "b!1" "d!1") (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sq_le_abs formula-decl nil sq nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   nil)))