(set-logic QF_UFNIA)
(set-option :incremental true)
(set-option :check-models true)
(set-option :finite-model-find true)
(set-option :stats-every-query false)
(set-option :sygus-sym-break-dynamic false)
(set-option :bv-eq-solver true)
(set-option :minisat-elimination false)
(set-option :se-solve-int false)
(set-option :dt-rewrite-error-sel false)
(set-option :bv-lazy-rewrite-extf false)
(set-option :dt-infer-as-lemmas true)
(set-option :print-success true)
(set-option :arrays-model-based true)
(set-option :dio-decomps false)
(set-option :bv-skolemize true)
(set-option :dt-cyclic false)
(set-option :bv-extract-arith true)
(set-option :cbqi-use-inf-real false)
(set-option :cbqi-nested-qe true)
(set-option :arrays-eager-index false)
(set-option :bv-inequality-solver false)
(set-option :strict-parsing true)
(set-option :minisat-dump-dimacs false)
(set-option :bv-div-zero-const false)
(set-option :preprocess-only false)
(set-option :bv-eager-explanations true)
(set-option :conjecture-filter-active-terms true)
(set-option :cbqi-multi-inst false)
(set-option :arrays-eager-lemmas false)
(set-option :nl-ext-split-zero true)
(set-option :conjecture-gen false)
(set-option :nl-ext-purify false)
(set-option :nl-ext-tplanes true)
(set-option :cbqi-all false)
(set-option :arith-rewrite-equalities true)
(set-option :ag-miniscope-quant true)
(set-option :dt-use-testers false)
(set-option :filesystem-access true)
(set-option :miplib-trick false)
(set-option :revert-arith-models-on-unsat true)
(set-option :cbqi-innermost false)
(set-option :use-soi false)
(set-option :elim-ext-arith-quant true)
(set-option :stats false)
(set-option :cbqi-nopt false)
(set-option :cbqi-recurse false)
(set-option :parse-only true)
(set-option :restrict-pivots false)
(set-option :arrays-optimize-linear true)
(set-option :nl-ext-inc-prec false)
(set-option :cbqi-bv-interleave-value false)
(set-option :cbqi-bv-solve-nl false)
(set-option :e-matching true)
(set-option :cbqi-sat false)
(set-option :fewer-preprocessing-holes false)
(set-option :nl-ext-ent-conf false)
(set-option :use-fcsimplex true)
(set-option :bv-alg-extf true)
(set-option :dt-binary-split true)
(set-option :decision-use-weight false)
(set-option :cbqi-repeat-lit false)
(set-option :nl-ext-rbound false)
(set-option :cegqi-si-sol-min-core true)
(set-option :continued-execution false)
(set-option :sygus-sym-break-lazy true)
(set-option :cbqi-use-inf-int false)
(set-option :type-checking true)
(set-option :collect-pivot-stats true)
(set-option :conjecture-gen-uee-intro true)
(set-option :idl-rewrite-equalities false)
(set-option :use-approx true)
(set-option :arrays-reduce-sharing false)
(set-option :nl-ext-tplanes-interleave false)
(set-option :arrays-weak-equiv false)
(set-option :bv-algebraic-solver false)
(set-option :bv-gauss-elim true)
(set-option :soi-qe true)
(set-option :bv-quick-xplain false)
(set-option :cbqi-min-bounds true)
(set-option :help true)
(set-option :fallback-sequential true)
(set-option :cegqi false)
(set-option :repeat-simp false)
(set-option :produce-assertions true)
(set-option :quant-ind false)
(set-option :dump-proofs false)
(set-option :register-quant-body-terms false)
(set-option :sygus-eval-unfold-bool true)
(set-option :lte-partial-inst false)
(set-option :sep-exp true)
(set-option :sets-infer-as-lemmas true)
(set-option :mbqi-one-inst-per-round false)
(set-option :sygus-auto-unfold false)
(set-option :fs-interleave true)
(set-option :fmf-inst-gen-one-quant-per-round false)
(set-option :omit-dont-cares true)
(set-option :sygus-rr-synth-filter-order true)
(set-option :infer-arith-trigger-eq-exp true)
(set-option :sygus-crepair-abort false)
(set-option :sygus-rr-synth-check false)
(set-option :model-u-dt-enum false)
(set-option :quant-cf true)
(set-option :macros-quant true)
(set-option :purify-dt-triggers false)
(set-option :sep-check-neg false)
(set-option :dump-unsat-cores-full true)
(set-option :sygus-eval-opt true)
(set-option :sygus-add-const-grammar false)
(set-option :sep-deq-c true)
(set-option :sets-rel-eager true)
(set-option :relational-triggers false)
(set-option :qcf-eager-check-rd false)
(set-option :infer-arith-trigger-eq true)
(set-option :sep-child-refine false)
(set-option :sygus-rr-verify false)
(set-option :inst-when-tc-first false)
(set-option :proof false)
(set-option :inst-when-strict-interleave false)
(set-option :ho-merge-term-db true)
(set-option :sygus-inv-templ-when-sg false)
(set-option :sygus-rr-synth-filter-cong false)
(set-option :fmf-inst-gen true)
(set-option :qcf-tconstraint false)
(set-option :ite-dtt-split-quant false)
(set-option :produce-models true)
(set-option :produce-unsat-cores true)
(set-option :check-synth-sol true)
(set-option :quant-model-ee true)
(set-option :rr-one-inst-per-round true)
(set-option :miniscope-quant true)
(set-option :abstract-values false)
(set-option :inst-prop true)
(set-option :min-synth-sol true)
(set-option :quant-split false)
(set-option :hard-limit true)
(set-option :sygus-rr-synth true)
(set-option :sygus-qe-preproc true)
(set-option :pre-skolem-quant false)
(set-option :sygus-ext-rew false)
(set-option :partial-triggers true)
(set-option :qcf-eager-test false)
(set-option :strict-triggers false)
(set-option :ho-matching true)
(set-option :sygus-sample-grammar true)
(set-option :purify-triggers true)
(set-option :quant-fun-wd true)
(set-option :qcf-vo-exp true)
(set-option :sygus-verify-subcall false)
(set-option :fmf-bound-lazy true)
(set-option :sygus-pbe-multi-fair false)
(set-option :sygus-rr-verify-abort true)
(set-option :cpu-time true)
(set-option :mbqi-one-quant-per-round false)
(set-option :quant-alpha-equiv false)
(set-option :force-no-limit-cpu-while-dump false)
(set-option :sep-min-refine false)
(set-option :sygus-min-grammar false)
(set-option :qcf-skip-rd false)
(set-option :quant-epr-match false)
(set-option :incremental false)
(set-option :fmf-bound true)
(set-option :var-ineq-elim-quant true)
(set-option :int-wf-ind false)
(set-option :qcf-all-conflict true)
(set-option :sygus-rr-synth-accel true)
(set-option :sets-proxy-lemmas false)
(set-option :quant-epr true)
(set-option :fmf-fresh-dc true)
(set-option :fmf-empty-sorts false)
(set-option :fmf-fun-rlv true)
(set-option :sygus-sample-fp-uniform true)
(set-option :multi-trigger-when-single true)
(set-option :produce-unsat-assumptions true)
(set-option :increment-triggers false)
(set-option :check-unsat-cores true)
(set-option :uf-ss-clique-splits true)
(set-option :uf-ho-ext true)
(set-option :simp-ite-compress false)
(set-option :uf-ss-regions false)
(set-option :strings-print-ascii false)
(set-option :solve-real-as-int true)
(set-option :simp-with-care true)
(set-option :symmetry-breaker-exp false)
(set-option :strings-min-prefix-explain false)
(set-option :strings-eager-len false)
(set-option :strings-eit true)
(set-option :strings-abort-loop true)
(set-option :condense-function-values false)
(set-option :strings-guess-model true)
(set-option :strings-check-entail-len true)
(set-option :strings-len-norm false)
(set-option :strings-infer-sym true)
(set-option :sort-inference false)
(set-option :strings-infer-as-lemmas false)
(set-option :symmetry-breaker true)
(set-option :strings-uf-reduct true)
(set-option :uf-ss-eager-split false)
(set-option :strings-exp false)
(set-option :synth-rr-prep-ext-rew false)
(set-option :strings-inm true)
(set-option :assign-function-values true)
(set-option :synth-rr-prep true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const i3 Int)
(assert v16)
(assert v9)
(assert v17)
(assert (or v14 v17 v13 v11))
(assert v5)
(declare-const v18 Bool)
(assert (and (= (< (abs 22) 56) v11 v0 v1 (or v14 v17 v13 v11) v15 v11 v4) v13 (= (< (abs 22) 56) v11 v0 v1 (or v14 v17 v13 v11) v15 v11 v4) v0 v11 v18 v3))
(declare-const i5 Int)
(assert (= v17 (= v4 v10 (or v14 v17 v13 v11) v3 v3 v11 v3 v9) v2 (< (abs 22) 56) v11 v15 v16 (= v4 v10 (or v14 v17 v13 v11) v3 v3 v11 v3 v9) v2))
(declare-const i6 Int)
(assert (= (= (< (abs 22) 56) v11 v0 v1 (or v14 v17 v13 v11) v15 v11 v4) (>= i5 (- (abs 22))) (= v17 (= v4 v10 (or v14 v17 v13 v11) v3 v3 v11 v3 v9) v2 (< (abs 22) 56) v11 v15 v16 (= v4 v10 (or v14 v17 v13 v11) v3 v3 v11 v3 v9) v2) (= (< (abs 22) 56) v11 v0 v1 (or v14 v17 v13 v11) v15 v11 v4) v12 (>= i5 (- (abs 22))) v7))
(declare-const v19 Bool)
(declare-const i7 Int)
(declare-const v20 Bool)
(declare-sort S0 0)
(assert v11)
(declare-const v21 Bool)
(assert (or v14 v17 v13 v11))
(declare-const v22 Bool)
(assert v11)
(declare-const v23 Bool)
(assert (or v3 (< i7 (mod 22 (abs 22))) (or v14 v17 v13 v11) (= (abs 22) (- (abs 22))) v5))
(declare-const i8 Int)
(declare-const v24 Bool)
(assert (xor (< i7 (mod 22 (abs 22))) (and (= (< (abs 22) 56) v11 v0 v1 (or v14 v17 v13 v11) v15 v11 v4) v13 (= (< (abs 22) 56) v11 v0 v1 (or v14 v17 v13 v11) v15 v11 v4) v0 v11 v18 v3) v3 (= (abs 22) (- (abs 22))) v18 (>= i5 (- (abs 22))) v17))
(assert v21)
(declare-const v25 Bool)
(assert (and (<= (- (* 51 22 98 i3)) (mod 22 (abs 22))) v18 (< (abs 22) 56) (= v4 v10 (or v14 v17 v13 v11) v3 v3 v11 v3 v9) v3 v24 v17 v5 v21 v1 v14))
(assert (xor (= 7 312) (= (abs 22) (- (abs 22))) (and v11 v5 v4 v2 v3 v14 v8 v1) v23 (distinct (abs 22) 51) v15 (= 7 312) v14))
(declare-const v26 Bool)
(declare-const v27 Bool)
(assert (or v3 (< i7 (mod 22 (abs 22))) (or v14 v17 v13 v11) (= (abs 22) (- (abs 22))) v5))
(check-sat)
(exit)