(set-option :produce-models true)
(set-option :pull-nested-quantifiers true)
(set-option :mbqi true)
(declare-const x (_ BitVec 15))
(declare-const y (_ BitVec 15))
(declare-const xs (_ BitVec 15))
; --- Parsed BLIF network from Z:\Projects\Z3 4Biology\Code\v0.1\models\arabidopsis.cnet--------
(declare-fun T ((_ BitVec 15) (_ BitVec 15) ) bool)
; -------------- Transition Relation: -----------------
(assert (forall ((x (_ BitVec 15)) (y (_ BitVec 15))
  )(= (T x y)
     (and (= (= ((_ extract 0 0) y) (_ bv1 1))
             (or (and (= ((_ extract 9 9) x) (_ bv1 1))
                      (= ((_ extract 13 13) x) (_ bv1 1))
                      (= ((_ extract 14 14) x) (_ bv1 1))
                      (= ((_ extract 0 0) x) (_ bv1 1)))
                 (and (= ((_ extract 4 4) x) (_ bv1 1))
                      (= ((_ extract 13 13) x) (_ bv1 1))
                      (= ((_ extract 14 14) x) (_ bv1 1))
                      (= ((_ extract 0 0) x) (_ bv1 1)))
                 (and (= ((_ extract 6 6) x) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1)))))
          (= (= ((_ extract 1 1) y) (_ bv1 1)) (or (and (= ((_ extract 1 1) x) (_ bv1 1)))))
          (= (= ((_ extract 2 2) y) (_ bv1 1))
             (or (and (not (= ((_ extract 4 4) x) (_ bv1 1)))
                      (not (= ((_ extract 12 12) x) (_ bv1 1))))))
          (= (= ((_ extract 3 3) y) (_ bv1 1))
             (or (and (not (= ((_ extract 5 5) x) (_ bv1 1))))))
          (= (= ((_ extract 4 4) y) (_ bv1 1))
             (or (and (not (= ((_ extract 9 9) x) (_ bv1 1)))
                      (not (= ((_ extract 12 12) x) (_ bv1 1))))
                 (and (= ((_ extract 6 6) x) (_ bv1 1))
                      (not (= ((_ extract 9 9) x) (_ bv1 1))))
                 (and (= ((_ extract 3 3) x) (_ bv1 1))
                      (not (= ((_ extract 9 9) x) (_ bv1 1))))))
          (= (= ((_ extract 5 5) y) (_ bv1 1))
             (or (and (not (= ((_ extract 6 6) x) (_ bv1 1))))))
          (= (= ((_ extract 6 6) y) (_ bv1 1))
             (or (and (not (= ((_ extract 12 12) x) (_ bv1 1))))
                 (and (not (= ((_ extract 5 5) x) (_ bv1 1))))))
          (= (= ((_ extract 7 7) y) (_ bv1 1))
             (or (and (not (= ((_ extract 12 12) x) (_ bv1 1))))))
          (= (= ((_ extract 8 8) y) (_ bv1 1))
             (or (and (= ((_ extract 8 8) x) (_ bv1 1))
                      (not (= ((_ extract 14 14) x) (_ bv1 1))))
                 (and (= ((_ extract 8 8) x) (_ bv1 1))
                      (not (= ((_ extract 9 9) x) (_ bv1 1))))))
          (= (= ((_ extract 9 9) y) (_ bv1 1))
             (or (and (= ((_ extract 6 6) x) (_ bv1 1))
                      (= ((_ extract 9 9) x) (_ bv1 1))
                      (= ((_ extract 14 14) x) (_ bv1 1)))
                 (and (not (= ((_ extract 7 7) x) (_ bv1 1)))
                      (not (= ((_ extract 12 12) x) (_ bv1 1))))
                 (and (= ((_ extract 6 6) x) (_ bv1 1))
                      (not (= ((_ extract 11 11) x) (_ bv1 1))))
                 (and (= ((_ extract 6 6) x) (_ bv1 1))
                      (not (= ((_ extract 10 10) x) (_ bv1 1))))
                 (and (= ((_ extract 6 6) x) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1)))
                 (and (not (= ((_ extract 4 4) x) (_ bv1 1)))
                      (= ((_ extract 6 6) x) (_ bv1 1)))
                 (and (= ((_ extract 6 6) x) (_ bv1 1))
                      (not (= ((_ extract 7 7) x) (_ bv1 1))))))
          (= (= ((_ extract 10 10) y) (_ bv1 1)) (or true))
          (= (= ((_ extract 11 11) y) (_ bv1 1)) (or true))
          (= (= ((_ extract 12 12) y) (_ bv1 1))
             (or (and (not (= ((_ extract 4 4) x) (_ bv1 1)))
                      (= ((_ extract 5 5) x) (_ bv1 1))
                      (not (= ((_ extract 6 6) x) (_ bv1 1))))))
          (= (= ((_ extract 13 13) y) (_ bv1 1))
             (or (and (= ((_ extract 4 4) x) (_ bv1 1))
                      (= ((_ extract 13 13) x) (_ bv1 1))
                      (= ((_ extract 14 14) x) (_ bv1 1))
                      (= ((_ extract 0 0) x) (_ bv1 1)))
                 (and (= ((_ extract 9 9) x) (_ bv1 1))
                      (= ((_ extract 13 13) x) (_ bv1 1))
                      (= ((_ extract 14 14) x) (_ bv1 1))
                      (= ((_ extract 0 0) x) (_ bv1 1)))
                 (and (= ((_ extract 6 6) x) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1)))
                 (and (= ((_ extract 6 6) x) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1)))))
          (= (= ((_ extract 14 14) y) (_ bv1 1))
             (or (and (= ((_ extract 6 6) x) (_ bv1 1)))))))))
; ------------------ END ------------------------------
(get-info :all-statistics)