(set-logic QF_UFLRA)
(set-option :produce-abducts true)
(set-option :fs-interleave true)
(set-option :quant-cf true)
(set-option :full-saturate-quant true)
(set-option :uf-ho 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 r0 Real)
(declare-const r2 Real)
(declare-const r3 Real)
(declare-const r4 Real)
(declare-const r5 Real)
(declare-const r7 Real)
(declare-const r8 Real)
(declare-const v12 Bool)
(declare-const r9 Real)
(declare-const r10 Real)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-sort S0 0)
(declare-const v15 Bool)
(declare-const r11 Real)
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const r12 Real)
(declare-const v19 Bool)
(declare-const v20 Bool)
(declare-const v21 Bool)
(push 1)
(declare-sort S1 0)
(declare-const r13 Real)
(push 1)
(declare-const v22 Bool)
(declare-const r14 Real)
(pop 1)
(declare-const v23 Bool)
(pop 1)
(declare-const S0-0 S0)
(declare-const S0-1 S0)
(declare-const v24 Bool)
(declare-const v25 Bool)
(declare-const r15 Real)
(declare-const r16 Real)
(declare-const S0-2 S0)
(declare-const v26 Bool)
(declare-const v27 Bool)
(declare-const r17 Real)
(declare-const v28 Bool)
(declare-const v29 Bool)
(push 1)
(declare-const v30 Bool)
(pop 1)
(declare-const S0-3 S0)
(declare-const r18 Real)
(declare-sort S1 0)
(declare-const v31 Bool)
(declare-const r19 Real)
(push 1)
(declare-const v32 Bool)
(declare-sort S2 0)
(push 1)
(declare-const v33 Bool)
(pop 1)
(declare-const v34 Bool)
(declare-const r20 Real)
(declare-const v35 Bool)
(pop 1)
(push 1)
(declare-const r21 Real)
(declare-const v36 Bool)
(declare-const S1-0 S1)
(declare-const v37 Bool)
(declare-const v38 Bool)
(declare-const r22 Real)
(declare-const r23 Real)
(declare-const v39 Bool)
(declare-const v40 Bool)
(pop 1)
(push 1)
(push 1)
(push 1)
(push 1)
(declare-const v41 Bool)
(declare-const r24 Real)
(declare-const r25 Real)
(declare-const v42 Bool)
(pop 1)
(declare-const r26 Real)
(declare-const v43 Bool)
(declare-const v44 Bool)
(declare-const S0-4 S0)
(declare-const v45 Bool)
(declare-const r27 Real)
(declare-const r28 Real)
(declare-sort S2 0)
(declare-const v46 Bool)
(declare-const r29 Real)
(declare-const v47 Bool)
(declare-const S0-5 S0)
(declare-const v48 Bool)
(declare-const r30 Real)
(declare-const v49 Bool)
(declare-const r31 Real)
(declare-const v50 Bool)
(declare-const v51 Bool)
(declare-const r32 Real)
(push 1)
(declare-const v52 Bool)
(declare-sort S3 0)
(declare-const S2-0 S2)
(declare-const v53 Bool)
(push 1)
(push 1)
(pop 1)
(declare-const v54 Bool)
(declare-const r33 Real)
(pop 1)
(pop 1)
(declare-const v55 Bool)
(declare-const r34 Real)
(declare-const S2-0 S2)
(declare-const r35 Real)
(declare-const v56 Bool)
(declare-const r36 Real)
(pop 1)
(pop 1)
(declare-const v57 Bool)
(declare-const r37 Real)
(declare-const v58 Bool)
(push 1)
(declare-const v59 Bool)
(pop 1)
(push 1)
(declare-const v60 Bool)
(declare-const r38 Real)
(declare-const v61 Bool)
(declare-const r39 Real)
(declare-const v62 Bool)
(declare-const v63 Bool)
(declare-const r40 Real)
(declare-const v64 Bool)
(declare-const r41 Real)
(pop 1)
(declare-const v65 Bool)
(push 1)
(declare-const v66 Bool)
(declare-const v67 Bool)
(declare-sort S2 0)
(declare-const v68 Bool)
(declare-const r42 Real)
(declare-const v69 Bool)
(declare-const v70 Bool)
(push 1)
(push 1)
(declare-const v71 Bool)
(push 1)
(declare-const S2-0 S2)
(declare-const v72 Bool)
(declare-const v73 Bool)
(declare-const v74 Bool)
(declare-sort S3 0)
(declare-sort S4 0)
(pop 1)
(push 1)
(push 1)
(declare-const r43 Real)
(declare-const r44 Real)
(declare-const v75 Bool)
(push 1)
(declare-const v76 Bool)
(push 1)
(declare-const v77 Bool)
(pop 1)
(declare-const v78 Bool)
(declare-const v79 Bool)
(declare-const r45 Real)
(declare-const v80 Bool)
(declare-const v81 Bool)
(declare-const v82 Bool)
(declare-const r46 Real)
(pop 1)
(declare-const v83 Bool)
(push 1)
(declare-const r47 Real)
(declare-const v84 Bool)
(declare-const r48 Real)
(declare-sort S3 0)
(push 1)
(declare-const v85 Bool)
(push 1)
(pop 1)
(declare-const S0-4 S0)
(declare-const r49 Real)
(push 1)
(declare-const S1-0 S1)
(declare-const v86 Bool)
(declare-const v87 Bool)
(push 1)
(declare-const v88 Bool)
(declare-const r50 Real)
(declare-const r51 Real)
(declare-const v89 Bool)
(declare-const v90 Bool)
(declare-const v91 Bool)
(declare-const v92 Bool)
(declare-const v93 Bool)
(declare-const v94 Bool)
(declare-const v95 Bool)
(declare-const S1-1 S1)
(declare-const v96 Bool)
(push 1)
(declare-const v97 Bool)
(pop 1)
(declare-const r52 Real)
(declare-const r53 Real)
(push 1)
(declare-const S2-0 S2)
(declare-const r54 Real)
(assert (or v19))
(assert (or v19))
(assert (or (< 0.0 r11 r3 r4 (- r7))))
(assert (or v87))
(assert (or v87 (= S0-2 S0-1 S0-3)))
(assert (or v24 (<= r2 r4) (<= r2 r4) (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v87))
(assert (or (< 0.0 r11 r3 r4 (- r7)) v87 (< 0.0 r11 r3 r4 (- r7)) (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v87 (<= r2 r4) (= S0-2 S0-1 S0-3) v19 (< 0.0 r11 r3 r4 (- r7))))
(assert (or v65 v87 (< 0.0 r11 r3 r4 (- r7)) (<= r2 r4) v24 (< 0.0 r11 r3 r4 (- r7)) (<= r2 r4)))
(assert (or (< 0.0 r11 r3 r4 (- r7)) v19 (<= r2 r4) v24 (= S0-2 S0-1 S0-3) (< 0.0 r11 r3 r4 (- r7)) (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v65 (= S0-2 S0-1 S0-3) v65))
(assert (or (= S0-2 S0-1 S0-3) (<= r2 r4)))
(assert (or v24))
(assert (or v65 v65 v65))
(assert (or v24))
(assert (or (< 0.0 r11 r3 r4 (- r7)) v19 v65 (<= r2 r4)))
(assert (or (<= r2 r4)))
(assert (or (< 0.0 r11 r3 r4 (- r7)) (<= r5 (- r3) (- r3) 0.1421602) v87 v87 v87 (< 0.0 r11 r3 r4 (- r7))))
(assert (or v65 v24 v19 v87 (= S0-2 S0-1 S0-3)))
(assert (or v24 (<= r5 (- r3) (- r3) 0.1421602) v24 v65 v24 (< 0.0 r11 r3 r4 (- r7)) v24))
(assert (or v19))
(assert (or v65))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (<= r5 (- r3) (- r3) 0.1421602) (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v65 (<= r2 r4)))
(assert (or v87))
(assert (or v65 v19 v19))
(assert (or v24 v24 v87 (= S0-2 S0-1 S0-3) v24 (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v19 (<= r5 (- r3) (- r3) 0.1421602) (<= r5 (- r3) (- r3) 0.1421602) v24))
(assert (or (< 0.0 r11 r3 r4 (- r7))))
(assert (or v19 v19))
(assert (or (< 0.0 r11 r3 r4 (- r7)) v24))
(assert (or (<= r2 r4) (< 0.0 r11 r3 r4 (- r7)) (< 0.0 r11 r3 r4 (- r7)) v65 (< 0.0 r11 r3 r4 (- r7))))
(assert (or v24))
(assert (or v65 (<= r2 r4)))
(assert (or (= S0-2 S0-1 S0-3)))
(assert (or v19 v87 (= S0-2 S0-1 S0-3) v65 v87))
(assert (or (<= r2 r4) v87))
(assert (or (= S0-2 S0-1 S0-3)))
(assert (or (< 0.0 r11 r3 r4 (- r7)) (<= r5 (- r3) (- r3) 0.1421602) (< 0.0 r11 r3 r4 (- r7)) (< 0.0 r11 r3 r4 (- r7)) v87 (= S0-2 S0-1 S0-3) v19))
(assert (or v19))
(assert (or v65 (<= r5 (- r3) (- r3) 0.1421602) (< 0.0 r11 r3 r4 (- r7)) v24 (<= r2 r4) (= S0-2 S0-1 S0-3) (< 0.0 r11 r3 r4 (- r7))))
(assert (or v65 (<= r2 r4) (<= r5 (- r3) (- r3) 0.1421602) v87))
(assert (or (<= r2 r4) (<= r5 (- r3) (- r3) 0.1421602) v24))
(assert (or v65))
(assert (or v87 v87 (<= r5 (- r3) (- r3) 0.1421602) (<= r2 r4) (<= r2 r4)))
(assert (or v65 v87 v24))
(assert (or (= S0-2 S0-1 S0-3)))
(assert (or v24 (< 0.0 r11 r3 r4 (- r7))))
(assert (or (<= r2 r4) (<= r2 r4) (< 0.0 r11 r3 r4 (- r7))))
(assert (or (<= r2 r4) (<= r2 r4) (<= r5 (- r3) (- r3) 0.1421602) (= S0-2 S0-1 S0-3) v87 (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v65 (< 0.0 r11 r3 r4 (- r7)) (<= r5 (- r3) (- r3) 0.1421602) (< 0.0 r11 r3 r4 (- r7)) v19))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (<= r2 r4)))
(assert (or (<= r2 r4) (= S0-2 S0-1 S0-3)))
(assert (or v65 v65 (= S0-2 S0-1 S0-3) (< 0.0 r11 r3 r4 (- r7)) (= S0-2 S0-1 S0-3) v87 v65 (<= r2 r4)))
(assert (or v87 (< 0.0 r11 r3 r4 (- r7)) v87 (<= r5 (- r3) (- r3) 0.1421602) (<= r2 r4) v24 (<= r5 (- r3) (- r3) 0.1421602) v65 v24))
(assert (or (= S0-2 S0-1 S0-3) v65))
(assert (or v65))
(assert (or v87 v65 (< 0.0 r11 r3 r4 (- r7)) v24 v65))
(assert (or (< 0.0 r11 r3 r4 (- r7)) v87))
(assert (or v87))
(assert (or (< 0.0 r11 r3 r4 (- r7))))
(assert (or (<= r2 r4) (< 0.0 r11 r3 r4 (- r7)) (= S0-2 S0-1 S0-3) (< 0.0 r11 r3 r4 (- r7))))
(assert (or (<= r2 r4) (= S0-2 S0-1 S0-3) v87))
(assert (or v24 (< 0.0 r11 r3 r4 (- r7))))
(assert (or v24 (= S0-2 S0-1 S0-3) (<= r2 r4) (< 0.0 r11 r3 r4 (- r7)) (= S0-2 S0-1 S0-3) (<= r2 r4) (<= r2 r4) v87 v24))
(assert (or (< 0.0 r11 r3 r4 (- r7)) v19))
(assert (or (= S0-2 S0-1 S0-3) v19 (<= r2 r4)))
(assert (or v65 (< 0.0 r11 r3 r4 (- r7)) (< 0.0 r11 r3 r4 (- r7)) (= S0-2 S0-1 S0-3) (<= r5 (- r3) (- r3) 0.1421602) v87))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (= S0-2 S0-1 S0-3)))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (<= r5 (- r3) (- r3) 0.1421602) v24 (<= r5 (- r3) (- r3) 0.1421602) (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v24))
(assert (or (= S0-2 S0-1 S0-3) v24 v65 v65))
(assert (or v87 v65 v65 (<= r5 (- r3) (- r3) 0.1421602) (< 0.0 r11 r3 r4 (- r7)) (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v87 v65 (= S0-2 S0-1 S0-3) v19 (<= r5 (- r3) (- r3) 0.1421602) (< 0.0 r11 r3 r4 (- r7)) v65 (< 0.0 r11 r3 r4 (- r7)) (= S0-2 S0-1 S0-3) (<= r5 (- r3) (- r3) 0.1421602) (<= r2 r4) v87))
(assert (or v87))
(assert (or (<= r2 r4) v19))
(assert (or v65))
(assert (or (<= r2 r4) (< 0.0 r11 r3 r4 (- r7))))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (= S0-2 S0-1 S0-3) (<= r5 (- r3) (- r3) 0.1421602) (< 0.0 r11 r3 r4 (- r7)) v87 v87))
(assert (or (< 0.0 r11 r3 r4 (- r7))))
(assert (or (<= r2 r4) v87 v87))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) v19))
(assert (or (< 0.0 r11 r3 r4 (- r7))))
(assert (or v24 v19))
(assert (or (= S0-2 S0-1 S0-3) (<= r2 r4) (< 0.0 r11 r3 r4 (- r7))))
(assert (or v87))
(assert (or v24 v87 v24))
(assert (or v19))
(assert (or v65 (< 0.0 r11 r3 r4 (- r7)) (<= r2 r4) v24))
(assert (or (< 0.0 r11 r3 r4 (- r7))))
(assert (or v87))
(assert (or (<= r2 r4) (<= r2 r4) v24 (= S0-2 S0-1 S0-3) v19 v87))
(assert (or (<= r2 r4) (= S0-2 S0-1 S0-3)))
(assert (or (<= r2 r4) (<= r5 (- r3) (- r3) 0.1421602) v24 v87 v24 v87 v19 v24 v19 (= S0-2 S0-1 S0-3) v19))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (<= r2 r4) v19))
(assert (or (< 0.0 r11 r3 r4 (- r7))))
(assert (or v87 v24 (= S0-2 S0-1 S0-3) v87 (<= r2 r4)))
(assert (or v65 (<= r2 r4)))
(assert (or v87))
(assert (or v87))
(assert (or (< 0.0 r11 r3 r4 (- r7)) (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v65 v24 v87))
(assert (or (= S0-2 S0-1 S0-3) v24 v87 v65))
(assert (or v24 v24 (<= r5 (- r3) (- r3) 0.1421602) (= S0-2 S0-1 S0-3)))
(assert (or v24))
(assert (or (<= r2 r4) (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or (<= r2 r4) (= S0-2 S0-1 S0-3) v87 (< 0.0 r11 r3 r4 (- r7))))
(assert (or v19 v87 (<= r5 (- r3) (- r3) 0.1421602) (< 0.0 r11 r3 r4 (- r7))))
(assert (or (= S0-2 S0-1 S0-3) (< 0.0 r11 r3 r4 (- r7)) (< 0.0 r11 r3 r4 (- r7))))
(assert (or v24))
(assert (or (<= r2 r4) (< 0.0 r11 r3 r4 (- r7))))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (<= r2 r4) v19 v65 v65))
(assert (or v65 v19 v24 (<= r5 (- r3) (- r3) 0.1421602) v24))
(assert (or v19))
(assert (or (< 0.0 r11 r3 r4 (- r7))))
(assert (or v19 v19 v87 (<= r5 (- r3) (- r3) 0.1421602) (< 0.0 r11 r3 r4 (- r7)) v24))
(assert (or (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v87 (< 0.0 r11 r3 r4 (- r7))))
(assert (or v24 v24 (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v19))
(assert (or (= S0-2 S0-1 S0-3) (<= r2 r4)))
(assert (or v19 (<= r5 (- r3) (- r3) 0.1421602) v87 (<= r5 (- r3) (- r3) 0.1421602) (< 0.0 r11 r3 r4 (- r7)) v24 (<= r2 r4) v24 v87 (= S0-2 S0-1 S0-3) v65 (< 0.0 r11 r3 r4 (- r7)) v19 v24 (= S0-2 S0-1 S0-3) (<= r5 (- r3) (- r3) 0.1421602) v24))
(assert (or v65 (= S0-2 S0-1 S0-3)))
(assert (or v87 v87 (<= r2 r4) (= S0-2 S0-1 S0-3) (<= r5 (- r3) (- r3) 0.1421602) (<= r5 (- r3) (- r3) 0.1421602) v65 v24 v65 (< 0.0 r11 r3 r4 (- r7))))
(assert (or (= S0-2 S0-1 S0-3) (<= r2 r4) (= S0-2 S0-1 S0-3) v65 (<= r2 r4) (<= r2 r4)))
(assert (or (<= r2 r4) v87))
(assert (or (<= r2 r4)))
(assert (or (= S0-2 S0-1 S0-3)))
(assert (or (<= r2 r4) v24 (= S0-2 S0-1 S0-3) v24))
(assert (or v19 v87))
(assert (or (= S0-2 S0-1 S0-3)))
(assert (or (<= r2 r4) (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v65))
(assert (or v19))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) v65 v19 v87 v87 (= S0-2 S0-1 S0-3) (< 0.0 r11 r3 r4 (- r7))))
(assert (or (< 0.0 r11 r3 r4 (- r7)) (< 0.0 r11 r3 r4 (- r7))))
(assert (or v19))
(assert (or (< 0.0 r11 r3 r4 (- r7)) v65 (<= r2 r4) (= S0-2 S0-1 S0-3)))
(assert (or v24 (<= r5 (- r3) (- r3) 0.1421602) v65 v19 v19 v24 v19))
(assert (or (<= r2 r4) v87 (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v65 v65 v65 (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v24 (<= r5 (- r3) (- r3) 0.1421602) (= S0-2 S0-1 S0-3) v24))
(assert (or v19 v65))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (<= r2 r4) (< 0.0 r11 r3 r4 (- r7)) v65 v19 (= S0-2 S0-1 S0-3) v65 (<= r2 r4) (< 0.0 r11 r3 r4 (- r7)) (<= r5 (- r3) (- r3) 0.1421602) (<= r5 (- r3) (- r3) 0.1421602) v19 v87))
(assert (or v24 v65 v19 v65 (<= r2 r4)))
(assert (or v65))
(assert (or v87 v24 v87))
(assert (or v19 v19 (= S0-2 S0-1 S0-3)))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) v87 (= S0-2 S0-1 S0-3) (< 0.0 r11 r3 r4 (- r7))))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) v65 (<= r5 (- r3) (- r3) 0.1421602) (= S0-2 S0-1 S0-3) v65 v19 v24))
(assert (or v19))
(assert (or (= S0-2 S0-1 S0-3) (< 0.0 r11 r3 r4 (- r7)) (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or (= S0-2 S0-1 S0-3) (<= r2 r4) v24 v24))
(assert (or (= S0-2 S0-1 S0-3)))
(assert (or v19))
(assert (or v19 (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v24 v65 v65))
(assert (or v87 (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v87 v19 (<= r2 r4) v87))
(assert (or v65))
(assert (or (< 0.0 r11 r3 r4 (- r7))))
(assert (or v19))
(assert (or v24))
(assert (or (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or (= S0-2 S0-1 S0-3) v87 v19 (< 0.0 r11 r3 r4 (- r7)) v65))
(assert (or (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or (< 0.0 r11 r3 r4 (- r7)) v19 (< 0.0 r11 r3 r4 (- r7))))
(assert (or (= S0-2 S0-1 S0-3) v65 v19))
(assert (or (= S0-2 S0-1 S0-3) v87 (<= r2 r4)))
(assert (or (<= r2 r4) v65))
(assert (or v24))
(assert (or v65 (<= r5 (- r3) (- r3) 0.1421602) v24 (<= r2 r4)))
(assert (or v24))
(assert (or (< 0.0 r11 r3 r4 (- r7))))
(assert (or v87 v65 v65 v87 v24))
(assert (or (= S0-2 S0-1 S0-3) (<= r5 (- r3) (- r3) 0.1421602) v87))
(assert (or v24 v87 v24))
(assert (or (= S0-2 S0-1 S0-3) v24 (< 0.0 r11 r3 r4 (- r7)) v65))
(assert (or (< 0.0 r11 r3 r4 (- r7)) (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v87 v65 v24 v19))
(assert (or (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v65))
(assert (or (= S0-2 S0-1 S0-3) (= S0-2 S0-1 S0-3) (= S0-2 S0-1 S0-3) (= S0-2 S0-1 S0-3) (<= r5 (- r3) (- r3) 0.1421602) (= S0-2 S0-1 S0-3) (<= r2 r4)))
(assert (or v87 v65))
(assert (or (< 0.0 r11 r3 r4 (- r7)) v24 v19))
(assert (or v65 v87 v65))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (= S0-2 S0-1 S0-3) v19 v87 v87))
(assert (or (<= r2 r4) (<= r2 r4) (< 0.0 r11 r3 r4 (- r7))))
(assert (or v24 (= S0-2 S0-1 S0-3) (= S0-2 S0-1 S0-3) v87 (<= r2 r4) (< 0.0 r11 r3 r4 (- r7)) v65))
(assert (or v24 v87 v65))
(assert (or (<= r2 r4)))
(assert (or (<= r2 r4)))
(assert (or v65 v19 v65 v19 v24))
(assert (or v65))
(assert (or v19 v87))
(assert (or (= S0-2 S0-1 S0-3) (= S0-2 S0-1 S0-3)))
(assert (or (< 0.0 r11 r3 r4 (- r7)) v19 (< 0.0 r11 r3 r4 (- r7)) v65))
(assert (or (< 0.0 r11 r3 r4 (- r7))))
(assert (or v24 v87))
(assert (or v19))
(assert (or (= S0-2 S0-1 S0-3) (<= r5 (- r3) (- r3) 0.1421602) v19 v24))
(assert (or (= S0-2 S0-1 S0-3) (= S0-2 S0-1 S0-3)))
(assert (or v87 (<= r2 r4)))
(assert (or v24 v19 v24))
(assert (or v19 v24))
(assert (or (< 0.0 r11 r3 r4 (- r7)) (<= r5 (- r3) (- r3) 0.1421602) (<= r5 (- r3) (- r3) 0.1421602) v87))
(assert (or (<= r2 r4) v19 (= S0-2 S0-1 S0-3)))
(assert (or v24))
(assert (or v19))
(assert (or (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or (<= r2 r4) v24 (< 0.0 r11 r3 r4 (- r7)) v19))
(assert (or (< 0.0 r11 r3 r4 (- r7)) v24 (<= r2 r4)))
(assert (or v19 (< 0.0 r11 r3 r4 (- r7)) (<= r2 r4)))
(assert (or (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v87 v24 (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or (= S0-2 S0-1 S0-3) (= S0-2 S0-1 S0-3) v24 v24))
(assert (or v65))
(assert (or (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or (< 0.0 r11 r3 r4 (- r7)) (<= r5 (- r3) (- r3) 0.1421602) (<= r2 r4) (<= r5 (- r3) (- r3) 0.1421602) (< 0.0 r11 r3 r4 (- r7)) v19))
(assert (or v24 v87 v65 (= S0-2 S0-1 S0-3)))
(assert (or (<= r2 r4) v19 (= S0-2 S0-1 S0-3) v19 (< 0.0 r11 r3 r4 (- r7))))
(assert (or v65 v24))
(assert (or v87 (<= r5 (- r3) (- r3) 0.1421602) (<= r2 r4)))
(assert (or v87))
(assert (or v24 v24))
(assert (or (= S0-2 S0-1 S0-3)))
(assert (or (< 0.0 r11 r3 r4 (- r7)) v24 (<= r5 (- r3) (- r3) 0.1421602) v65 v65 (< 0.0 r11 r3 r4 (- r7)) (<= r5 (- r3) (- r3) 0.1421602) (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or (<= r2 r4)))
(assert (or v19))
(assert (or v19 (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v87 (= S0-2 S0-1 S0-3)))
(assert (or (<= r2 r4) v65 (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v65))
(assert (or (<= r2 r4) v24 (= S0-2 S0-1 S0-3) v87 v65 v65))
(assert (or (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or (< 0.0 r11 r3 r4 (- r7)) v24 v24 (= S0-2 S0-1 S0-3)))
(assert (or (= S0-2 S0-1 S0-3)))
(assert (or (= S0-2 S0-1 S0-3) (<= r2 r4) (= S0-2 S0-1 S0-3)))
(assert (or v65 (= S0-2 S0-1 S0-3)))
(assert (or v87 (= S0-2 S0-1 S0-3)))
(assert (or v19 (< 0.0 r11 r3 r4 (- r7)) (<= r5 (- r3) (- r3) 0.1421602) (= S0-2 S0-1 S0-3)))
(assert (or v65 (<= r2 r4)))
(assert (or (<= r2 r4) v19 (< 0.0 r11 r3 r4 (- r7)) v24))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or (= S0-2 S0-1 S0-3) (= S0-2 S0-1 S0-3) v24 (<= r2 r4)))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (< 0.0 r11 r3 r4 (- r7)) (< 0.0 r11 r3 r4 (- r7)) (= S0-2 S0-1 S0-3) (<= r2 r4) v65 v87 (<= r2 r4)))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (= S0-2 S0-1 S0-3) v19 v24 (<= r2 r4) (< 0.0 r11 r3 r4 (- r7)) v19))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (< 0.0 r11 r3 r4 (- r7))))
(assert (or v65 (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or (< 0.0 r11 r3 r4 (- r7))))
(assert (or v65 v24))
(assert (or v87 (< 0.0 r11 r3 r4 (- r7))))
(assert (or v87))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) v65))
(assert (or v65))
(assert (or (<= r2 r4)))
(assert (or v87 v87))
(assert (or v24 (<= r2 r4) (= S0-2 S0-1 S0-3) v24 (= S0-2 S0-1 S0-3) (<= r5 (- r3) (- r3) 0.1421602) (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v19 v24 v87 v24 v65 (<= r5 (- r3) (- r3) 0.1421602) (= S0-2 S0-1 S0-3) (<= r2 r4) (= S0-2 S0-1 S0-3) v24 (= S0-2 S0-1 S0-3)))
(assert (or (= S0-2 S0-1 S0-3) (<= r2 r4) v24))
(assert (or v19))
(assert (or v65))
(assert (or v87 (< 0.0 r11 r3 r4 (- r7)) (<= r2 r4) (< 0.0 r11 r3 r4 (- r7)) v24 v65 (<= r5 (- r3) (- r3) 0.1421602) v65))
(assert (or (<= r2 r4) (<= r2 r4) (= S0-2 S0-1 S0-3)))
(assert (or (= S0-2 S0-1 S0-3) (<= r2 r4) (< 0.0 r11 r3 r4 (- r7))))
(assert (or (< 0.0 r11 r3 r4 (- r7))))
(assert (or v65 v19 (<= r5 (- r3) (- r3) 0.1421602) v19 v87 (<= r5 (- r3) (- r3) 0.1421602) (= S0-2 S0-1 S0-3) (<= r2 r4)))
(assert (or v65))
(assert (or v87 (< 0.0 r11 r3 r4 (- r7)) (<= r5 (- r3) (- r3) 0.1421602) (<= r2 r4)))
(assert (or (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (< 0.0 r11 r3 r4 (- r7)) v87 v87 (<= r2 r4) (< 0.0 r11 r3 r4 (- r7)) v87 v24 (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v24))
(assert (or v19))
(assert (or v24))
(assert (or v19 (<= r2 r4)))
(assert (or (< 0.0 r11 r3 r4 (- r7))))
(assert (or v87 v87 (<= r2 r4) (<= r2 r4)))
(assert (or v87))
(assert (or v24 (= S0-2 S0-1 S0-3) v87 (= S0-2 S0-1 S0-3) (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v87))
(assert (or v87))
(assert (or v24))
(assert (or v65 v65 (< 0.0 r11 r3 r4 (- r7))))
(assert (or (< 0.0 r11 r3 r4 (- r7)) v65 v19))
(assert (or v87 v24))
(assert (or (<= r2 r4)))
(assert (or v24))
(assert (or v65 (<= r2 r4) v65 (< 0.0 r11 r3 r4 (- r7)) (<= r5 (- r3) (- r3) 0.1421602) v19 (< 0.0 r11 r3 r4 (- r7)) v24))
(assert (or (= S0-2 S0-1 S0-3) v87 (<= r2 r4) v19))
(assert (or (<= r2 r4)))
(assert (or v65 (< 0.0 r11 r3 r4 (- r7))))
(assert (or v65 (= S0-2 S0-1 S0-3)))
(assert (or (<= r2 r4) (< 0.0 r11 r3 r4 (- r7)) (= S0-2 S0-1 S0-3) v24))
(assert (or v87))
(assert (or v24 v87 v24))
(assert (or v19))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) v65))
(assert (or (= S0-2 S0-1 S0-3) v24 v19 v87 v87 (< 0.0 r11 r3 r4 (- r7)) v65 (= S0-2 S0-1 S0-3)))
(assert (or v19 v24 v87))
(assert (or v24))
(assert (or v24))
(assert (or v87))
(assert (or (<= r2 r4)))
(assert (or v24))
(assert (or v65))
(assert (or v87 v19 (< 0.0 r11 r3 r4 (- r7)) v19))
(assert (or (<= r2 r4) (< 0.0 r11 r3 r4 (- r7))))
(assert (or v65))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (= S0-2 S0-1 S0-3) v19))
(assert (or v87 (= S0-2 S0-1 S0-3) v19 (< 0.0 r11 r3 r4 (- r7))))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (<= r5 (- r3) (- r3) 0.1421602) (< 0.0 r11 r3 r4 (- r7))))
(assert (or (< 0.0 r11 r3 r4 (- r7))))
(assert (or (<= r2 r4) (< 0.0 r11 r3 r4 (- r7)) v24 v24 v24 v65 v87 (= S0-2 S0-1 S0-3)))
(assert (or v87 v65 v19 v24 v24 v87 (= S0-2 S0-1 S0-3)))
(assert (or v19 v65))
(assert (or v87 (<= r2 r4)))
(assert (or v65 v65 (<= r5 (- r3) (- r3) 0.1421602) v65 v24 v24 (< 0.0 r11 r3 r4 (- r7))))
(assert (or (< 0.0 r11 r3 r4 (- r7)) (<= r2 r4) (= S0-2 S0-1 S0-3) (= S0-2 S0-1 S0-3)))
(assert (or (< 0.0 r11 r3 r4 (- r7)) v65))
(assert (or v87 (< 0.0 r11 r3 r4 (- r7))))
(assert (or v65))
(assert (or (= S0-2 S0-1 S0-3) (<= r5 (- r3) (- r3) 0.1421602) (< 0.0 r11 r3 r4 (- r7)) (<= r2 r4)))
(assert (or v24 v87 v24 (< 0.0 r11 r3 r4 (- r7)) v87 v24 (<= r2 r4) v24))
(assert (or v87))
(assert (or (< 0.0 r11 r3 r4 (- r7)) v19 (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or (<= r2 r4) (< 0.0 r11 r3 r4 (- r7)) (<= r5 (- r3) (- r3) 0.1421602) (= S0-2 S0-1 S0-3) (<= r5 (- r3) (- r3) 0.1421602) (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v87))
(assert (or (= S0-2 S0-1 S0-3) (<= r5 (- r3) (- r3) 0.1421602) (<= r2 r4) v65))
(assert (or v24 v24 v19))
(assert (or v19 v65 v87))
(assert (or (< 0.0 r11 r3 r4 (- r7)) v19 v19 v65 v19 v87 v87 (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v87 (<= r5 (- r3) (- r3) 0.1421602) v65))
(assert (or v24))
(assert (or v65))
(assert (or (< 0.0 r11 r3 r4 (- r7)) v87 v19 (< 0.0 r11 r3 r4 (- r7))))
(assert (or v65))
(assert (or v24 v24 (<= r5 (- r3) (- r3) 0.1421602) v19 v65 (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v87 (= S0-2 S0-1 S0-3) (<= r5 (- r3) (- r3) 0.1421602) v65 v65 v19))
(assert (or v19))
(assert (or (= S0-2 S0-1 S0-3) (<= r5 (- r3) (- r3) 0.1421602) v65))
(assert (or v24 (<= r5 (- r3) (- r3) 0.1421602) (<= r5 (- r3) (- r3) 0.1421602) (<= r5 (- r3) (- r3) 0.1421602) v87))
(assert (or v19))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) v24 v19))
(assert (or (< 0.0 r11 r3 r4 (- r7)) (= S0-2 S0-1 S0-3) v65 v19 (= S0-2 S0-1 S0-3)))
(assert (or v19 (= S0-2 S0-1 S0-3) (= S0-2 S0-1 S0-3) v19 (<= r2 r4)))
(assert (or (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v87))
(assert (or v24 (<= r2 r4) v24 v87))
(assert (or v87 (<= r2 r4) v19 v87 v19 (< 0.0 r11 r3 r4 (- r7)) v19 v87))
(assert (or v87 (<= r2 r4)))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (< 0.0 r11 r3 r4 (- r7)) (<= r5 (- r3) (- r3) 0.1421602) v65))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) v19 (<= r2 r4)))
(assert (or v24))
(assert (or (<= r2 r4) (<= r5 (- r3) (- r3) 0.1421602) v24 (= S0-2 S0-1 S0-3)))
(assert (or v65 v24 v87 v24 (< 0.0 r11 r3 r4 (- r7)) (< 0.0 r11 r3 r4 (- r7))))
(assert (or v87 v87))
(assert (or v19))
(assert (or v87 v87))
(assert (or v65 v87 (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v87))
(assert (or (<= r2 r4) (< 0.0 r11 r3 r4 (- r7)) v24 (< 0.0 r11 r3 r4 (- r7)) v65))
(assert (or v65))
(assert (or v87 (<= r5 (- r3) (- r3) 0.1421602) (<= r2 r4)))
(assert (or (< 0.0 r11 r3 r4 (- r7)) v87 (<= r5 (- r3) (- r3) 0.1421602) v24 (= S0-2 S0-1 S0-3)))
(assert (or (< 0.0 r11 r3 r4 (- r7)) v65))
(assert (or v87))
(assert (or v87 (< 0.0 r11 r3 r4 (- r7))))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (<= r2 r4) v65 v19 (< 0.0 r11 r3 r4 (- r7))))
(assert (or (< 0.0 r11 r3 r4 (- r7))))
(assert (or v87 (< 0.0 r11 r3 r4 (- r7))))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (<= r5 (- r3) (- r3) 0.1421602) v24))
(assert (or v24))
(assert (or (< 0.0 r11 r3 r4 (- r7))))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (= S0-2 S0-1 S0-3) v87))
(assert (or (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v19 (<= r2 r4) v65 (<= r2 r4) (= S0-2 S0-1 S0-3) v19 v24 v24 v87))
(assert (or (<= r2 r4) v19))
(assert (or (<= r2 r4) (< 0.0 r11 r3 r4 (- r7)) (= S0-2 S0-1 S0-3) v65))
(assert (or (<= r2 r4) v19 v24 (<= r2 r4) (= S0-2 S0-1 S0-3)))
(assert (or (<= r5 (- r3) (- r3) 0.1421602) (<= r5 (- r3) (- r3) 0.1421602) v19))
(assert (or (< 0.0 r11 r3 r4 (- r7))))
(assert (or (<= r2 r4) (<= r5 (- r3) (- r3) 0.1421602) (<= r2 r4) v87 v24 (< 0.0 r11 r3 r4 (- r7)) (<= r2 r4) (= S0-2 S0-1 S0-3) (<= r2 r4)))
(assert (or v24 v19 (<= r5 (- r3) (- r3) 0.1421602) (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or v19))
(assert (or v19 v24 (<= r2 r4) v87 (<= r5 (- r3) (- r3) 0.1421602)))
(assert (or (< 0.0 r11 r3 r4 (- r7)) v19 v19))
(assert (or (< 0.0 r11 r3 r4 (- r7)) v24 (<= r5 (- r3) (- r3) 0.1421602) (= S0-2 S0-1 S0-3) (< 0.0 r11 r3 r4 (- r7)) (= S0-2 S0-1 S0-3) v24))
(assert (or v87 v19 v87))
(assert (or v65 v24))
(assert (or v19 v24 (= S0-2 S0-1 S0-3) v24 (< 0.0 r11 r3 r4 (- r7))))
(assert (or v24))
(get-abduct A (xor (<= (- (/ r2 8925.848)) (/ 49.0 49.0)) (xor v6 v15) v67 v19))
(check-sat)
(exit)