(th_C
 (L1 0
  (L1-1 nil 3666632956
   ("" (flatten 1)
    (("" (lemma "Range")
      (("" (inst -1 "B")
        (("" (split -1)
          (("1" (propax) nil nil) ("2" (propax) nil nil)
           ("3" (lemma "clue1")
            (("3" (lemma "Range")
              (("3" (inst -1 "G")
                (("3" (split -1)
                  (("1" (assert) nil nil) ("2" (assert) nil nil)
                   ("3" (assert) nil nil) ("4" (assert) nil nil)
                   ("5" (assert) nil nil) ("6" (assert) nil nil)
                   ("7" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil)
           ("4" (lemma "Range")
            (("4" (lemma "clue1")
              (("4" (inst -2 "G") (("4" (assert) nil nil)) nil)) nil))
            nil)
           ("5" (lemma "clue1")
            (("5" (lemma "Range")
              (("5" (inst -1 "G") (("5" (assert) nil nil)) nil)) nil))
            nil)
           ("6" (lemma "Range")
            (("6" (lemma "clue1")
              (("6" (inst -2 "G") (("6" (assert) nil nil)) nil)) nil))
            nil)
           ("7" (lemma "Range")
            (("7" (lemma "clue1")
              (("7" (inst -2 "G") (("7" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Range formula-decl nil th_C nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (G? adt-recognizer-decl "[people -> boolean]" th_C nil)
    (G adt-constructor-decl "(G?)" th_C nil)
    (clue1 formula-decl nil th_C nil)
    (B adt-constructor-decl "(B?)" th_C nil)
    (B? adt-recognizer-decl "[people -> boolean]" th_C nil)
    (boolean nonempty-type-decl nil booleans nil)
    (people type-decl nil th_C nil))
   shostak))
 (L2 0
  (L2-1 nil 3666633277
   ("" (lemma "clue2")
    (("" (lemma "Range")
      (("" (inst -1 "A")
        (("" (lemma "L1") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((Range formula-decl nil th_C nil) (L1 formula-decl nil th_C nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (A adt-constructor-decl "(A?)" th_C nil)
    (A? adt-recognizer-decl "[people -> boolean]" th_C nil)
    (boolean nonempty-type-decl nil booleans nil)
    (people type-decl nil th_C nil) (clue2 formula-decl nil th_C nil))
   shostak))
 (L3 0
  (L3-1 nil 3666633369
   ("" (lemma "clue2")
    (("" (lemma "L2")
      (("" (lemma "Range")
        (("" (inst -1 "A") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((L2 formula-decl nil th_C nil) (people type-decl nil th_C nil)
    (boolean nonempty-type-decl nil booleans nil)
    (A? adt-recognizer-decl "[people -> boolean]" th_C nil)
    (A adt-constructor-decl "(A?)" th_C nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Range formula-decl nil th_C nil)
    (clue2 formula-decl nil th_C nil))
   shostak))
 (L4 0
  (L4-1 nil 3666633417
   ("" (lemma "clue1") (("" (lemma "L2") (("" (assert) nil nil)) nil))
    nil)
   ((L2 formula-decl nil th_C nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (clue1 formula-decl nil th_C nil))
   shostak))
 (L5 0
  (L5-1 nil 3666633441
   ("" (lemma "clue4") (("" (lemma "L4") (("" (assert) nil nil)) nil))
    nil)
   ((L4 formula-decl nil th_C nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (clue4 formula-decl nil th_C nil))
   shostak))
 (L6 0
  (L6-1 nil 3666633467
   ("" (lemma "Range")
    (("" (lemma "Unique")
      (("" (inst -2 "D")
        (("" (assert)
          (("" (split -2)
            (("1" (lemma "L3")
              (("1" (inst -3 "A" "D") (("1" (assert) nil nil)) nil))
              nil)
             ("2" (lemma "L2")
              (("2" (inst -3 "B" "D") (("2" (assert) nil nil)) nil))
              nil)
             ("3" (assert) nil nil) ("4" (assert) nil nil)
             ("5" (lemma "L5")
              (("5" (inst -3 "D" "E") (("5" (assert) nil nil)) nil))
              nil)
             ("6" (lemma "clue3")
              (("6" (lemma "L5") (("6" (assert) nil nil)) nil)) nil)
             ("7" (lemma "clue3")
              (("7" (lemma "L5") (("7" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Unique formula-decl nil th_C nil)
    (clue3 formula-decl nil th_C nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (L5 formula-decl nil th_C nil)
    (E? adt-recognizer-decl "[people -> boolean]" th_C nil)
    (E adt-constructor-decl "(E?)" th_C nil)
    (L2 formula-decl nil th_C nil)
    (B? adt-recognizer-decl "[people -> boolean]" th_C nil)
    (B adt-constructor-decl "(B?)" th_C nil)
    (L3 formula-decl nil th_C nil)
    (A? adt-recognizer-decl "[people -> boolean]" th_C nil)
    (A adt-constructor-decl "(A?)" th_C nil)
    (D adt-constructor-decl "(D?)" th_C nil)
    (D? adt-recognizer-decl "[people -> boolean]" th_C nil)
    (boolean nonempty-type-decl nil booleans nil)
    (people type-decl nil th_C nil) (Range formula-decl nil th_C nil))
   shostak))
 (L7 0
  (L7-1 nil 3666633596
   ("" (lemma "clue5")
    (("" (lemma "L6")
      (("" (lemma "Range")
        (("" (lemma "Unique")
          (("" (inst -2 "C")
            (("" (split -2)
              (("1" (lemma "L3")
                (("1" (inst -3 "A" "C") (("1" (assert) nil nil)) nil))
                nil)
               ("2" (lemma "L2")
                (("2" (inst -3 "B" "C") (("2" (assert) nil nil)) nil))
                nil)
               ("3" (assert) nil nil) ("4" (assert) nil nil)
               ("5" (assert) nil nil) ("6" (assert) nil nil)
               ("7" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((L6 formula-decl nil th_C nil) (Unique formula-decl nil th_C nil)
    (A adt-constructor-decl "(A?)" th_C nil)
    (A? adt-recognizer-decl "[people -> boolean]" th_C nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (L3 formula-decl nil th_C nil)
    (B adt-constructor-decl "(B?)" th_C nil)
    (B? adt-recognizer-decl "[people -> boolean]" th_C nil)
    (L2 formula-decl nil th_C nil)
    (C adt-constructor-decl "(C?)" th_C nil)
    (C? adt-recognizer-decl "[people -> boolean]" th_C nil)
    (boolean nonempty-type-decl nil booleans nil)
    (people type-decl nil th_C nil) (Range formula-decl nil th_C nil)
    (clue5 formula-decl nil th_C nil))
   shostak))
 (L8 0
  (L8-1 nil 3666634180
   ("" (lemma "Unique")
    (("" (lemma "Range")
      (("" (inst -1 "F")
        (("" (split -1)
          (("1" (lemma "L3")
            (("1" (inst -3 "A" "F") (("1" (assert) nil nil)) nil)) nil)
           ("2" (lemma "L2")
            (("2" (inst -3 "B" "F") (("2" (assert) nil nil)) nil)) nil)
           ("3" (lemma "L7")
            (("3" (inst -3 "C" "F")
              (("3" (assert)
                (("3" (flatten -1)
                  (("3" (lemma "Unique")
                    (("3" (inst -1 "C" "F") (("3" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("4" (lemma "L7")
            (("4" (flatten -1)
              (("4" (inst -4 "D" "F") (("4" (assert) nil nil)) nil))
              nil))
            nil)
           ("5" (lemma "L5")
            (("5" (inst -3 "E" "F") (("5" (assert) nil nil)) nil)) nil)
           ("6" (propax) nil nil)
           ("7" (lemma "L4")
            (("7" (inst -3 "F" "G") (("7" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Range formula-decl nil th_C nil)
    (A adt-constructor-decl "(A?)" th_C nil)
    (A? adt-recognizer-decl "[people -> boolean]" th_C nil)
    (L3 formula-decl nil th_C nil)
    (B adt-constructor-decl "(B?)" th_C nil)
    (B? adt-recognizer-decl "[people -> boolean]" th_C nil)
    (L2 formula-decl nil th_C nil)
    (C adt-constructor-decl "(C?)" th_C nil)
    (C? adt-recognizer-decl "[people -> boolean]" th_C nil)
    (L7 formula-decl nil th_C nil)
    (D? adt-recognizer-decl "[people -> boolean]" th_C nil)
    (D adt-constructor-decl "(D?)" th_C nil)
    (E adt-constructor-decl "(E?)" th_C nil)
    (E? adt-recognizer-decl "[people -> boolean]" th_C nil)
    (L5 formula-decl nil th_C nil)
    (G adt-constructor-decl "(G?)" th_C nil)
    (G? adt-recognizer-decl "[people -> boolean]" th_C nil)
    (L4 formula-decl nil th_C nil)
    (F adt-constructor-decl "(F?)" th_C nil)
    (F? adt-recognizer-decl "[people -> boolean]" th_C nil)
    (boolean nonempty-type-decl nil booleans nil)
    (people type-decl nil th_C nil) (Unique formula-decl nil th_C nil))
   shostak)))