(equality_example
 (IbEx 0
  (IbEx-1 nil 3308569247 nil
   ("" (skolem!)
    (("" (expand* "f" "g")
      (("" (expand "a") (("" (propax) nil nil)) nil)) nil))
    nil)
   unfinished nil nil nil nil nil)))
(E11
 (formulas 0
  (formulas-3 "" 3308656709 3308656709
   ("" (flatten)
    (("" (inst-cp - "b")
      (("" (inst -1 "a") (("" (bddsimp) nil nil)) nil)) nil))
    nil)
   proved nil 849007 2910 t shostak)
  (formulas-2 "Split first, inst later." 3308655850 3308655850
   ("" (flatten)
    (("" (split)
      (("1" (inst -1 "a") nil nil) ("2" (inst -1 "b") nil nil)) nil))
    nil)
   proved
   ((A nonempty-type-decl nil E11 nil) (b const-decl "A" E11 nil)
    (a const-decl "A" E11 nil))
   261011 2910 t shostak)
  (formulas-1 nil 3308655185 3308655519
   ("" (flatten)
    (("" (inst -1 "a")
      (("" (split)
        (("1" (propax) nil nil)
         ("2" (reveal -1) (("2" (inst -1 "b") nil nil)) nil))
        nil))
      nil))
    nil)
   proved
   ((a const-decl "A" E11 nil) (A nonempty-type-decl nil E11 nil)
    (b const-decl "A" E11 nil))
   333666 4590 t shostak))
 (E11_example 0
  (E11_example-1 nil 3308569295 nil
   ("" (flatten)
    (("" (skolem!)
      (("" (skolem!)
        (("" (inst -1 "x!1" "x!2")
          (("" (flatten)
            (("" (inst 1 "x!1")
              (("" (split)
                (("1" (replace -1 *)
                  (("1" (split)
                    (("1" (propax) nil nil) ("2" (propax) nil nil))
                    nil))
                  nil)
                 ("2" (propax) nil nil) ("3" (propax) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   unfinished nil nil nil nil nil)))
(q2a)
(predicate (I1 0
            (I1-1 nil 3308569295 nil
             ("" (flatten)
              (("" (skolem!)
                (("" (inst -1 "x!1")
                  (("" (inst?) (("" (bddsimp) nil nil)) nil)) nil))
                nil))
              nil)
             unfinished nil nil nil nil nil)))
(equality
 (Ia 0
  (Ia-1 nil 3308569295 nil
   ("" (skolem!)
    (("" (expand "f") (("" (expand* "g" "a") nil nil)) nil)) nil)
   unfinished nil nil nil nil nil)))
(counter)
(counter_model
 (NOTHmmm 0
  (NOTHmmm-1 nil 3308569296 nil
   ("" (split)
    (("1" (inst -1 "a1") (("1" (expand* "H" "F") nil nil)) nil)
     ("2" (inst 1 "a1")
      (("2" (split)
        (("1" (expand "E") (("1" (propax) nil nil)) nil)
         ("2" (skolem!) (("2" (expand* "F" "G") nil nil)) nil))
        nil))
      nil)
     ("3" (skolem!) (("3" (expand* "E" "G" "H") nil nil)) nil))
    nil)
   unfinished nil nil nil nil nil)))
(counter_model2
 (NOTHmmm 0
  (NOTHmmm-1 nil 3308569960 nil
   ("" (auto-rewrite-defs :always? t)
    (("" (bddsimp)
      (("1" (assert)
        (("1" (inst -1 "a2")
          (("1" (bddsimp)
            (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
          nil))
        nil)
       ("2" (assert) (("2" (assert) nil nil)) nil)
       ("3" (assert) nil nil))
      nil))
    nil)
   unfinished nil nil nil nil nil))
 (Stupid 0
  (Stupid-1 nil 3308569960 nil
   ("" (inst 1 "2+5/10") (("" (assert) nil nil)) nil) unfinished nil
   nil nil nil nil)))
(example04
 (T1 0
  (T1-1 nil 3308569961 3308570116
   ("" (skolem!) (("" (expand "f") (("" (propax) nil nil)) nil)) nil)
   unchecked ((f const-decl "nat" example04 nil)) 155372 1160 t
   shostak))
 (P1 0
  (P1-1 nil 3308570500 3308570773
   ("" (skolem!) (("" (assert) (("" (postpone) nil nil)) nil)) nil)
   unfinished nil 273299 1680 t shostak))
 (NotP1 0
  (NotP1-1 nil 3308570391 3308570486
   ("" (inst -1 "0") (("" (assert) nil nil)) nil) unchecked
   ((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)
    (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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   94776 1290 t shostak)))