(integral_domain
 (fullset_is_integral_domain 0
  (fullset_is_integral_domain-1 nil 3292787563
   ("" (expand "integral_domain?")
    (("" (lemma "fullset_is_commutative_ring")
      (("" (lemma "no_zero_divisors")
        (("" (replace -2)
          (("" (expand "no_zero_divisors?")
            (("" (skosimp*)
              (("" (inst - "x!1" "y!1") (("" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((fullset_is_commutative_ring formula-decl nil commutative_ring
     nil))
   shostak))
 (IMP_commutative_ring_TCC1 0
  (IMP_commutative_ring_TCC1-1 nil 3292787346
   ("" (lemma "fullset_is_integral_domain")
    (("" (expand "integral_domain?") (("" (flatten) nil nil)) nil))
    nil)
   ((integral_domain? const-decl "bool" integral_domain_def nil)
    (fullset_is_integral_domain formula-decl nil integral_domain nil))
   shostak))
 (integral_domain_TCC1 0
  (integral_domain_TCC1-1 nil 3292787453
   ("" (lemma "fullset_is_integral_domain") (("" (propax) nil nil))
    nil)
   ((fullset_is_integral_domain formula-decl nil integral_domain nil))
   shostak))
 (integral_domain_is 0
  (integral_domain_is-1 nil 3292787653
   ("" (skolem!) (("" (typepred "I!1") (("" (propax) nil nil)) nil))
    nil)
   ((integral_domain nonempty-type-eq-decl nil integral_domain nil)
    (integral_domain? const-decl "bool" integral_domain_def nil)
    (zero formal-const-decl "T" integral_domain nil)
    (* formal-const-decl "[T, T -> T]" integral_domain nil)
    (+ formal-const-decl "[T, T -> T]" integral_domain nil)
    (set type-eq-decl nil sets nil)
    (T formal-nonempty-type-decl nil integral_domain nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (integral_domain_is_ring 0
  (integral_domain_is_ring-1 nil 3292787671
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (expand "integral_domain?") (("" (flatten) nil nil)) nil))
      nil))
    nil)
   ((integral_domain nonempty-type-eq-decl nil integral_domain nil)
    (integral_domain? const-decl "bool" integral_domain_def nil)
    (zero formal-const-decl "T" integral_domain nil)
    (* formal-const-decl "[T, T -> T]" integral_domain nil)
    (+ formal-const-decl "[T, T -> T]" integral_domain nil)
    (set type-eq-decl nil sets nil)
    (T formal-nonempty-type-decl nil integral_domain nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak)))