(th_B
 (B_0 0
  (B_0-1 nil 3666686678 ("" (flatten) (("" (inst -1 "a") nil nil)) nil)
   ((U nonempty-type-decl nil th_B nil) (a const-decl "U" th_B nil))
   shostak))
 (B_1 0
  (B_1-1 nil 3666686733
   ("" (flatten) (("" (inst -1 "a") (("" (assert) nil nil)) nil)) nil)
   ((U nonempty-type-decl nil th_B nil) (a const-decl "U" th_B nil))
   shostak))
 (B_2 0
  (B_2-1 nil 3666686753
   ("" (flatten) (("" (inst 1 "a") (("" (inst -1 "a") nil nil)) nil))
    nil)
   ((U nonempty-type-decl nil th_B nil) (a const-decl "U" th_B nil))
   shostak))
 (B_3 0
  (B_3-1 nil 3666686845
   ("" (flatten) (("" (skolem 1 "B") (("" (inst 2 "B") nil nil)) nil))
    nil)
   ((U nonempty-type-decl nil th_B nil)) shostak))
 (B_4 0
  (B_4-1 nil 3666686921
   ("" (split)
    (("1" (flatten)
      (("1" (skolem 1 "A") (("1" (inst 2 "A") nil nil)) nil)) nil)
     ("2" (flatten)
      (("2" (skolem -1 "A") (("2" (inst -1 "A") nil nil)) nil)) nil))
    nil)
   ((U nonempty-type-decl nil th_B nil)) shostak))
 (B_5 0
  (B_5-1 nil 3666687393
   ("" (split)
    (("1" (flatten)
      (("1" (skolem 2 "A") (("1" (inst 1 "A") nil nil)) nil)) nil)
     ("2" (flatten)
      (("2" (skolem -2 "A") (("2" (inst -1 "A") nil nil)) nil)) nil))
    nil)
   ((U nonempty-type-decl nil th_B nil)) shostak))
 (B_6 0
  (B_6-1 nil 3666687440
   ("" (split)
    (("1" (flatten)
      (("1" (skolem 1 "A")
        (("1" (split)
          (("1" (inst -1 "A") nil nil) ("2" (inst -2 "A") nil nil))
          nil))
        nil))
      nil)
     ("2" (flatten)
      (("2" (split)
        (("1" (skolem 1 "A")
          (("1" (inst -1 "A") (("1" (flatten -1) nil nil)) nil)) nil)
         ("2" (skolem 1 "A")
          (("2" (inst -1 "A") (("2" (flatten -1) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((U nonempty-type-decl nil th_B nil)) shostak))
 (B_7 0
  (B_7-1 nil 3666687512
   ("" (split)
    (("1" (flatten)
      (("1" (split -1)
        (("1" (skolem -1 "A")
          (("1" (inst 1 "A") (("1" (flatten 1) nil nil)) nil)) nil)
         ("2" (skolem -1 "A")
          (("2" (inst 1 "A") (("2" (flatten 1) nil nil)) nil)) nil))
        nil))
      nil)
     ("2" (flatten)
      (("2" (skolem -1 "A")
        (("2" (split -1)
          (("1" (inst 1 "A") nil nil) ("2" (inst 2 "A") nil nil)) nil))
        nil))
      nil))
    nil)
   ((U nonempty-type-decl nil th_B nil)) shostak)))