Debug output from python api

(transform N7datalog13mk_coi_filterE...no-op 0s)
(transform N7datalog25mk_interp_tail_simplifierE...16 rules 0.0161756s)
(transform N7datalog27mk_quantifier_instantiationE...no-op 0s)
(transform N7datalog8mk_scaleE...no-op 0s)
(transform N7datalog18mk_karr_invariantsE...no-op 0s)
(transform N7datalog14mk_array_blastE...no-op 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog12mk_bit_blastE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...15 rules 0.00260911s)
(transform N7datalog13mk_coi_filterE...no-op 0s)
(transform N7datalog25mk_interp_tail_simplifierE...15 rules 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0.00205675s)
(transform N7datalog13mk_coi_filterE...no-op 0s)
(transform N7datalog25mk_interp_tail_simplifierE...15 rules 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0.00186199s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0.00200551s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0.001905s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog8mk_sliceE...no-op 0s)
Entering level 1
Entering level 2
Entering level 3
Entering level 4
(define-fun stmt_list ((x!1 Int)
 (x!2 Int)
 (x!3 Int)
 (x!4 Int)
 (x!5 Int)
 (x!6 Int)
 (x!7 Int)
 (x!8 Int)
 (x!9 Int)
 (x!10 Int)
 (x!11 Int)
 (x!12 Int)
 (x!13 Int)
 (x!14 Int)
 (x!15 Int)
 (x!16 Int)
 (x!17 Int)
 (x!18 Int)
 (x!19 Int)
 (x!20 Int)
 (x!21 Int)
 (x!22 Int)
 (x!23 Int)
 (x!24 Int)
 (x!25 Int)
 (x!26 Int)
 (x!27 Int)
 (x!28 Int)
 (x!29 Int)
 (x!30 Int)
 (x!31 Int)
 (x!32 Int)
 (x!33 Int)
 (x!34 Int)
 (x!35 Int)
 (x!36 Int)
 (x!37 Int)
 (x!38 Int)) Bool
  (let ((a!1 (or (<= (+ x!18 (* (- 1) x!37)) (- 1))
                 (<= (+ x!15 (* (- 1) x!34)) 0)))
        (a!2 (or (<= (+ x!15 (* (- 1) x!34)) (- 1))
                 (<= (+ x!38 (* (- 1) x!19)) 0)
                 (<= (+ x!18 (* (- 1) x!37)) (- 1)))))
    (and a!1 (<= (+ x!18 (* (- 1) x!37)) 0) a!2)))
(define-fun stmt ((x!1 Int)
 (x!2 Int)
 (x!3 Int)
 (x!4 Int)
 (x!5 Int)
 (x!6 Int)
 (x!7 Int)
 (x!8 Int)
 (x!9 Int)
 (x!10 Int)
 (x!11 Int)
 (x!12 Int)
 (x!13 Int)
 (x!14 Int)
 (x!15 Int)
 (x!16 Int)
 (x!17 Int)
 (x!18 Int)
 (x!19 Int)
 (x!20 Int)
 (x!21 Int)
 (x!22 Int)
 (x!23 Int)
 (x!24 Int)
 (x!25 Int)
 (x!26 Int)
 (x!27 Int)
 (x!28 Int)
 (x!29 Int)
 (x!30 Int)
 (x!31 Int)
 (x!32 Int)
 (x!33 Int)
 (x!34 Int)
 (x!35 Int)
 (x!36 Int)
 (x!37 Int)
 (x!38 Int)) Bool
  (let ((a!1 (or (<= (+ x!15 (* (- 1) x!34)) (- 1))
                 (<= (+ x!18 (* (- 1) x!37)) (- 1)))))
    (and (<= (+ x!18 (* (- 1) x!37)) 0) a!1)))
(smt.restarting :propagations 31 :decisions 22 :conflicts 0 :restart 100 :restart-outer 100 :agility 0)
(smt.restarting :propagations 81 :decisions 57 :conflicts 2 :restart 100 :restart-outer 100 :agility 0)
(smt.restarting :propagations 260 :decisions 138 :conflicts 8 :restart 100 :restart-outer 100 :agility 0)
(smt.restarting :propagations 412 :decisions 219 :conflicts 9 :restart 100 :restart-outer 100 :agility 0)
(smt.restarting :propagations 491 :decisions 262 :conflicts 9 :restart 100 :restart-outer 100 :agility 0)
(smt.restarting :propagations 568 :decisions 305 :conflicts 9 :restart 100 :restart-outer 100 :agility 0)
(smt.restarting :propagations 814 :decisions 413 :conflicts 11 :restart 100 :restart-outer 100 :agility 0)
(smt.restarting :propagations 914 :decisions 463 :conflicts 11 :restart 100 :restart-outer 100 :agility 0)
(smt.restarting :propagations 1082 :decisions 537 :conflicts 12 :restart 100 :restart-outer 100 :agility 0)
(smt.restarting :propagations 1359 :decisions 639 :conflicts 13 :restart 100 :restart-outer 100 :agility 0.00126209)
(smt.restarting :propagations 1731 :decisions 785 :conflicts 15 :restart 100 :restart-outer 100 :agility 0.00129777)
(smt.restarting :propagations 2208 :decisions 911 :conflicts 17 :restart 100 :restart-outer 100 :agility 0.00217946)
(smt.restarting :propagations 2468 :decisions 978 :conflicts 17 :restart 100 :restart-outer 100 :agility 0.00211928)
(smt.restarting :propagations 2732 :decisions 1046 :conflicts 17 :restart 100 :restart-outer 100 :agility 0.00205294)
(smt.restarting :propagations 2994 :decisions 1114 :conflicts 17 :restart 100 :restart-outer 100 :agility 0.0019865)
(smt.restarting :propagations 3486 :decisions 1251 :conflicts 18 :restart 100 :restart-outer 100 :agility 0.00187831)
(smt.restarting :propagations 3798 :decisions 1330 :conflicts 18 :restart 100 :restart-outer 100 :agility 0.00181243)
(smt.restarting :propagations 4116 :decisions 1411 :conflicts 18 :restart 100 :restart-outer 100 :agility 0.00261333)
(smt.restarting :propagations 4439 :decisions 1498 :conflicts 18 :restart 100 :restart-outer 100 :agility 0.00319198)
(smt.restarting :propagations 4812 :decisions 1590 :conflicts 18 :restart 100 :restart-outer 100 :agility 0.00374528)
(smt.restarting :propagations 5515 :decisions 1793 :conflicts 19 :restart 100 :restart-outer 100 :agility 0.00349556)
(smt.restarting :propagations 6364 :decisions 2050 :conflicts 21 :restart 100 :restart-outer 100 :agility 0.00412243)
(smt.restarting :propagations 6885 :decisions 2173 :conflicts 21 :restart 100 :restart-outer 100 :agility 0.00462593)
(smt.restarting :propagations 7455 :decisions 2304 :conflicts 21 :restart 100 :restart-outer 100 :agility 0.00435173)
(smt.restarting :propagations 8026 :decisions 2435 :conflicts 21 :restart 100 :restart-outer 100 :agility 0.00407826)
(smt.restarting :propagations 8615 :decisions 2573 :conflicts 21 :restart 100 :restart-outer 100 :agility 0.00382045)
(smt.restarting :propagations 9208 :decisions 2714 :conflicts 21 :restart 100 :restart-outer 100 :agility 0.00356999)
(smt.restarting :propagations 9804 :decisions 2859 :conflicts 21 :restart 100 :restart-outer 100 :agility 0.00333296)
(smt.restarting :propagations 10404 :decisions 3008 :conflicts 21 :restart 100 :restart-outer 100 :agility 0.00310855)
(smt.restarting :propagations 11008 :decisions 3157 :conflicts 21 :restart 100 :restart-outer 100 :agility 0.00289664)
(smt.restarting :propagations 12260 :decisions 3467 :conflicts 22 :restart 100 :restart-outer 100 :agility 0.00251267)
(smt.restarting :propagations 14209 :decisions 3841 :conflicts 25 :restart 100 :restart-outer 100 :agility 0.00295833)
(smt.restarting :propagations 14990 :decisions 4002 :conflicts 25 :restart 100 :restart-outer 100 :agility 0.00272705)
(smt.restarting :propagations 15887 :decisions 4189 :conflicts 25 :restart 100 :restart-outer 100 :agility 0.00259262)
(smt.restarting :propagations 17060 :decisions 4498 :conflicts 26 :restart 100 :restart-outer 100 :agility 0.00623333)
(smt.restarting :propagations 18219 :decisions 4793 :conflicts 27 :restart 100 :restart-outer 100 :agility 0.00543687)
(smt.restarting :propagations 19123 :decisions 4954 :conflicts 27 :restart 100 :restart-outer 100 :agility 0.00492586)
(smt.restarting :propagations 20027 :decisions 5111 :conflicts 27 :restart 100 :restart-outer 100 :agility 0.0058864)
(smt.restarting :propagations 20947 :decisions 5268 :conflicts 27 :restart 100 :restart-outer 100 :agility 0.00531503)
(smt.restarting :propagations 22830 :decisions 5595 :conflicts 28 :restart 100 :restart-outer 100 :agility 0.00432204)
(smt.restarting :propagations 23788 :decisions 5764 :conflicts 28 :restart 100 :restart-outer 100 :agility 0.00388034)
(smt.restarting :propagations 24763 :decisions 5933 :conflicts 28 :restart 100 :restart-outer 100 :agility 0.00348204)
(smt.restarting :propagations 25757 :decisions 6102 :conflicts 28 :restart 100 :restart-outer 100 :agility 0.00311993)
(smt.restarting :propagations 26770 :decisions 6274 :conflicts 28 :restart 100 :restart-outer 100 :agility 0.0027899)
(smt.restarting :propagations 27806 :decisions 6448 :conflicts 28 :restart 100 :restart-outer 100 :agility 0.00249005)
(smt.restarting :propagations 28864 :decisions 6628 :conflicts 28 :restart 100 :restart-outer 100 :agility 0.00221687)
(smt.restarting :propagations 29929 :decisions 6810 :conflicts 28 :restart 100 :restart-outer 100 :agility 0.00197031)
(smt.restarting :propagations 31018 :decisions 6992 :conflicts 28 :restart 100 :restart-outer 100 :agility 0.00174819)
(smt.restarting :propagations 32128 :decisions 7185 :conflicts 28 :restart 100 :restart-outer 100 :agility 0.00154787)
(smt.restarting :propagations 33265 :decisions 7380 :conflicts 28 :restart 100 :restart-outer 100 :agility 0.00136611)
(smt.restarting :propagations 35207 :decisions 7766 :conflicts 29 :restart 100 :restart-outer 100 :agility 0.00109042)
(smt.restarting :propagations 36379 :decisions 7961 :conflicts 29 :restart 100 :restart-outer 100 :agility 0.000958346)
(smt.restarting :propagations 38713 :decisions 8352 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.00112596)
(smt.restarting :propagations 39892 :decisions 8553 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.000988988)
(smt.restarting :propagations 41071 :decisions 8759 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.000867552)
(smt.restarting :propagations 42257 :decisions 8960 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.00148593)
(smt.restarting :propagations 43486 :decisions 9164 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.001301)
(smt.restarting :propagations 44704 :decisions 9368 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.0011359)
(smt.restarting :propagations 45920 :decisions 9574 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.000991258)
(smt.restarting :propagations 47145 :decisions 9781 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.000864688)
(smt.restarting :propagations 48364 :decisions 9989 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.000753977)
(smt.restarting :propagations 49583 :decisions 10198 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.000657375)
(smt.restarting :propagations 50835 :decisions 10415 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.000573093)
(smt.restarting :propagations 52094 :decisions 10632 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.000498419)
(smt.restarting :propagations 53353 :decisions 10852 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.000433475)
(smt.restarting :propagations 54645 :decisions 11076 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.000376202)
(smt.restarting :propagations 55985 :decisions 11321 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.000325486)
(smt.restarting :propagations 57341 :decisions 11578 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.000279894)
(smt.restarting :propagations 58701 :decisions 11843 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.00023992)
(smt.restarting :propagations 60065 :decisions 12114 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.000205202)
(smt.restarting :propagations 61429 :decisions 12384 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.000175333)
(smt.restarting :propagations 62801 :decisions 12658 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.000149797)
(smt.restarting :propagations 64237 :decisions 12940 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.000127852)
(smt.restarting :propagations 65634 :decisions 13224 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.000108828)
(smt.restarting :propagations 67030 :decisions 13508 :conflicts 30 :restart 100 :restart-outer 100 :agility 9.256e-05)
(smt.restarting :propagations 68438 :decisions 13793 :conflicts 30 :restart 100 :restart-outer 100 :agility 7.87162e-05)
(smt.restarting :propagations 69853 :decisions 14081 :conflicts 30 :restart 100 :restart-outer 100 :agility 6.68693e-05)
(smt.restarting :propagations 71286 :decisions 14378 :conflicts 30 :restart 100 :restart-outer 100 :agility 5.67487e-05)
(smt.restarting :propagations 72723 :decisions 14678 :conflicts 30 :restart 100 :restart-outer 100 :agility 4.80539e-05)
(smt.restarting :propagations 74159 :decisions 14979 :conflicts 30 :restart 100 :restart-outer 100 :agility 4.06507e-05)
(smt.restarting :propagations 75614 :decisions 15284 :conflicts 30 :restart 100 :restart-outer 100 :agility 3.43811e-05)
(smt.restarting :propagations 77077 :decisions 15593 :conflicts 30 :restart 100 :restart-outer 100 :agility 2.90349e-05)
(smt.restarting :propagations 78553 :decisions 15905 :conflicts 30 :restart 100 :restart-outer 100 :agility 2.44857e-05)
(smt.restarting :propagations 80202 :decisions 16246 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.000525888)
(smt.restarting :propagations 81755 :decisions 16566 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.00437024)
(smt.restarting :propagations 83275 :decisions 16891 :conflicts 30 :restart 100 :restart-outer 100 :agility 0.00366529)
(smt.restarting :propagations 85733 :decisions 17256 :conflicts 31 :restart 100 :restart-outer 100 :agility 0.00313586)
(smt.restarting :propagations 87281 :decisions 17582 :conflicts 31 :restart 100 :restart-outer 100 :agility 0.00262556)
(smt.restarting :propagations 88871 :decisions 17916 :conflicts 31 :restart 100 :restart-outer 100 :agility 0.00219238)
(smt.restarting :propagations 90468 :decisions 18249 :conflicts 31 :restart 100 :restart-outer 100 :agility 0.00182408)
(smt.restarting :propagations 93331 :decisions 18687 :conflicts 32 :restart 100 :restart-outer 100 :agility 0.0021115)
(smt.restarting :propagations 94976 :decisions 19019 :conflicts 32 :restart 100 :restart-outer 100 :agility 0.00174716)
(smt.restarting :propagations 96633 :decisions 19354 :conflicts 32 :restart 100 :restart-outer 100 :agility 0.00144452)
(smt.restarting :propagations 98301 :decisions 19688 :conflicts 32 :restart 100 :restart-outer 100 :agility 0.00128871)
(smt.restarting :propagations 99989 :decisions 20027 :conflicts 32 :restart 100 :restart-outer 100 :agility 0.00188941)
(smt.restarting :propagations 101676 :decisions 20365 :conflicts 32 :restart 100 :restart-outer 100 :agility 0.00155792)
(smt.restarting :propagations 103380 :decisions 20703 :conflicts 32 :restart 100 :restart-outer 100 :agility 0.00128344)
(smt.restarting :propagations 105104 :decisions 21041 :conflicts 32 :restart 100 :restart-outer 100 :agility 0.00105573)
(smt.restarting :propagations 106852 :decisions 21384 :conflicts 32 :restart 100 :restart-outer 100 :agility 0.000867036)
(smt.restarting :propagations 108628 :decisions 21733 :conflicts 32 :restart 100 :restart-outer 100 :agility 0.000710217)
(smt.restarting :propagations 110407 :decisions 22087 :conflicts 32 :restart 100 :restart-outer 100 :agility 0.000579845)
(smt.restarting :propagations 112184 :decisions 22442 :conflicts 32 :restart 100 :restart-outer 100 :agility 0.000472648)
(smt.restarting :propagations 113970 :decisions 22799 :conflicts 32 :restart 100 :restart-outer 100 :agility 0.00038523)
(smt.restarting :propagations 115774 :decisions 23163 :conflicts 32 :restart 100 :restart-outer 100 :agility 0.000313572)
(smt.restarting :propagations 117594 :decisions 23530 :conflicts 32 :restart 100 :restart-outer 100 :agility 0.000254708)
(smt.restarting :propagations 119434 :decisions 23901 :conflicts 32 :restart 100 :restart-outer 100 :agility 0.000206502)
(smt.restarting :propagations 121278 :decisions 24273 :conflicts 32 :restart 100 :restart-outer 100 :agility 0.000167118)
(smt.restarting :propagations 123127 :decisions 24645 :conflicts 32 :restart 100 :restart-outer 100 :agility 0.00013515)
(smt.restarting :propagations 125002 :decisions 25028 :conflicts 32 :restart 100 :restart-outer 100 :agility 0.000109221)
(smt.restarting :propagations 126874 :decisions 25410 :conflicts 32 :restart 100 :restart-outer 100 :agility 8.79762e-05)
(smt.restarting :propagations 128743 :decisions 25792 :conflicts 32 :restart 100 :restart-outer 100 :agility 7.08493e-05)
(smt.restarting :propagations 130624 :decisions 26178 :conflicts 32 :restart 100 :restart-outer 100 :agility 5.70509e-05)
(smt.restarting :propagations 132525 :decisions 26572 :conflicts 32 :restart 100 :restart-outer 100 :agility 4.58894e-05)
(smt.restarting :propagations 135363 :decisions 26983 :conflicts 33 :restart 100 :restart-outer 100 :agility 0.000527394)
(smt.restarting :propagations 137307 :decisions 27369 :conflicts 33 :restart 100 :restart-outer 100 :agility 0.00106502)
(smt.restarting :propagations 139263 :decisions 27758 :conflicts 33 :restart 100 :restart-outer 100 :agility 0.00140173)
(smt.restarting :propagations 141214 :decisions 28147 :conflicts 33 :restart 100 :restart-outer 100 :agility 0.00112097)
(smt.restarting :propagations 143166 :decisions 28540 :conflicts 33 :restart 100 :restart-outer 100 :agility 0.000896002)
(smt.restarting :propagations 146993 :decisions 29329 :conflicts 34 :restart 100 :restart-outer 100 :agility 0.000576469)
(smt.restarting :propagations 148978 :decisions 29725 :conflicts 34 :restart 100 :restart-outer 100 :agility 0.000459027)
(smt.restarting :propagations 150973 :decisions 30123 :conflicts 34 :restart 100 :restart-outer 100 :agility 0.000365256)
(smt.restarting :propagations 152971 :decisions 30521 :conflicts 34 :restart 100 :restart-outer 100 :agility 0.000290408)
(smt.restarting :propagations 154974 :decisions 30920 :conflicts 34 :restart 100 :restart-outer 100 :agility 0.000230828)
(smt.restarting :propagations 156979 :decisions 31319 :conflicts 34 :restart 100 :restart-outer 100 :agility 0.000183399)
(smt.restarting :propagations 158986 :decisions 31718 :conflicts 34 :restart 100 :restart-outer 100 :agility 0.000145671)
(smt.restarting :propagations 161004 :decisions 32123 :conflicts 34 :restart 100 :restart-outer 100 :agility 0.00011567)
(smt.restarting :propagations 163043 :decisions 32528 :conflicts 34 :restart 100 :restart-outer 100 :agility 9.17373e-05)
(smt.restarting :propagations 165077 :decisions 32936 :conflicts 34 :restart 100 :restart-outer 100 :agility 7.27128e-05)
(smt.restarting :propagations 167118 :decisions 33341 :conflicts 34 :restart 100 :restart-outer 100 :agility 0.000770285)
(smt.restarting :propagations 172128 :decisions 33978 :conflicts 36 :restart 100 :restart-outer 100 :agility 0.00140428)
(smt.restarting :propagations 174250 :decisions 34374 :conflicts 36 :restart 100 :restart-outer 100 :agility 0.00158238)
(smt.restarting :propagations 176417 :decisions 34768 :conflicts 36 :restart 100 :restart-outer 100 :agility 0.00262938)
(smt.restarting :propagations 181548 :decisions 35597 :conflicts 38 :restart 100 :restart-outer 100 :agility 0.00251758)
(smt.restarting :propagations 185861 :decisions 36354 :conflicts 39 :restart 100 :restart-outer 100 :agility 0.00171866)
(smt.restarting :propagations 188146 :decisions 36735 :conflicts 39 :restart 100 :restart-outer 100 :agility 0.00133915)
(smt.restarting :propagations 190438 :decisions 37119 :conflicts 39 :restart 100 :restart-outer 100 :agility 0.00103969)
(smt.restarting :propagations 192752 :decisions 37506 :conflicts 39 :restart 100 :restart-outer 100 :agility 0.000806304)
(smt.restarting :propagations 196380 :decisions 37908 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.000787312)
(smt.restarting :propagations 198699 :decisions 38291 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.000609911)
(smt.restarting :propagations 201069 :decisions 38677 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.00056317)
(smt.restarting :propagations 203404 :decisions 39065 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.001518)
(smt.restarting :propagations 205721 :decisions 39452 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.00117407)
(smt.restarting :propagations 9586854 :decisions 619570 :conflicts 13403 :restart 100 :restart-outer 110 :agility 0.00126051)
(smt.restarting :propagations 208048 :decisions 39842 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.00090798)
(smt.restarting :propagations 210381 :decisions 40236 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.000701562)
(smt.restarting :propagations 212728 :decisions 40630 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.000541312)
(smt.restarting :propagations 215071 :decisions 41024 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.000417416)
(smt.restarting :propagations 217422 :decisions 41423 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.000321813)
(smt.restarting :propagations 219789 :decisions 41829 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.000247784)
(smt.restarting :propagations 222151 :decisions 42235 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.00019046)
(smt.restarting :propagations 224537 :decisions 42639 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.000709089)
(smt.restarting :propagations 226926 :decisions 43042 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.000544445)
(smt.restarting :propagations 229323 :decisions 43448 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.000417612)
(smt.restarting :propagations 231721 :decisions 43854 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.000319974)
(smt.restarting :propagations 234134 :decisions 44263 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.000245115)
(smt.restarting :propagations 236545 :decisions 44675 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.000187619)
(smt.restarting :propagations 238993 :decisions 45087 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.000531022)
(smt.restarting :propagations 241445 :decisions 45503 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.000405325)
(smt.restarting :propagations 243942 :decisions 45931 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.000308918)
(smt.restarting :propagations 246438 :decisions 46356 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.0024278)
(smt.restarting :propagations 12921921 :decisions 801135 :conflicts 16222 :restart 100 :restart-outer 110 :agility 0.000682457)
(smt.restarting :propagations 248950 :decisions 46785 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.00184204)
(smt.restarting :propagations 13143530 :decisions 818434 :conflicts 16445 :restart 100 :restart-outer 110 :agility 0.000682033)
(smt.restarting :propagations 251472 :decisions 47217 :conflicts 40 :restart 100 :restart-outer 100 :agility 0.00139384)
(smt.restarting :propagations 255891 :decisions 47786 :conflicts 41 :restart 100 :restart-outer 100 :agility 0.00133136)
(smt.restarting :propagations 258435 :decisions 48218 :conflicts 41 :restart 100 :restart-outer 100 :agility 0.00100541)
(smt.restarting :propagations 261071 :decisions 48654 :conflicts 41 :restart 100 :restart-outer 100 :agility 0.000757885)
(smt.restarting :propagations 263969 :decisions 49096 :conflicts 41 :restart 100 :restart-outer 100 :agility 0.000570331)
(smt.restarting :propagations 266540 :decisions 49539 :conflicts 41 :restart 100 :restart-outer 100 :agility 0.000428205)
(smt.restarting :propagations 269509 :decisions 50030 :conflicts 41 :restart 100 :restart-outer 100 :agility 0.000321497)
(smt.restarting :propagations 272217 :decisions 50521 :conflicts 41 :restart 100 :restart-outer 100 :agility 0.000238215)
(smt.restarting :propagations 274895 :decisions 51016 :conflicts 41 :restart 100 :restart-outer 100 :agility 0.000176471)
(smt.restarting :propagations 277809 :decisions 51520 :conflicts 41 :restart 100 :restart-outer 100 :agility 0.000130548)
(smt.restarting :propagations 280913 :decisions 52024 :conflicts 41 :restart 100 :restart-outer 100 :agility 9.55671e-05)
(smt.restarting :propagations 296452 :decisions 54817 :conflicts 49 :restart 100 :restart-outer 100 :agility 0.00180494)
(smt.restarting :propagations 300048 :decisions 55357 :conflicts 49 :restart 100 :restart-outer 100 :agility 0.00127266)
(smt.restarting :propagations 307304 :decisions 56471 :conflicts 50 :restart 100 :restart-outer 100 :agility 0.00115244)
(smt.restarting :propagations 310795 :decisions 57037 :conflicts 50 :restart 100 :restart-outer 100 :agility 0.000787777)
(smt.restarting :propagations 314814 :decisions 57617 :conflicts 50 :restart 100 :restart-outer 100 :agility 0.000536623)
(smt.restarting :propagations 318816 :decisions 58200 :conflicts 50 :restart 100 :restart-outer 100 :agility 0.00035823)
(smt.restarting :propagations 322970 :decisions 58809 :conflicts 50 :restart 100 :restart-outer 100 :agility 0.000238855)
(smt.restarting :propagations 327065 :decisions 59417 :conflicts 50 :restart 100 :restart-outer 100 :agility 0.00148059)
(smt.restarting :propagations 331189 :decisions 60042 :conflicts 50 :restart 100 :restart-outer 100 :agility 0.000976112)
(smt.restarting :propagations 335052 :decisions 60667 :conflicts 50 :restart 100 :restart-outer 100 :agility 0.000637565)
(smt.restarting :propagations 345715 :decisions 62668 :conflicts 52 :restart 100 :restart-outer 100 :agility 0.000850284)
(smt.restarting :propagations 354889 :decisions 64065 :conflicts 53 :restart 100 :restart-outer 100 :agility 0.00180543)
(smt.restarting :propagations 359063 :decisions 64754 :conflicts 53 :restart 100 :restart-outer 100 :agility 0.00215161)
(smt.restarting :propagations 382149 :decisions 67524 :conflicts 60 :restart 100 :restart-outer 100 :agility 0.000186)
(smt.restarting :propagations 395622 :decisions 69305 :conflicts 62 :restart 100 :restart-outer 100 :agility 4.6413e-05)
(smt.restarting :propagations 400311 :decisions 70073 :conflicts 62 :restart 100 :restart-outer 100 :agility 2.78394e-05)
(smt.restarting :propagations 405298 :decisions 70844 :conflicts 62 :restart 100 :restart-outer 100 :agility 1.66303e-05)
(smt.restarting :propagations 409943 :decisions 71615 :conflicts 62 :restart 100 :restart-outer 100 :agility 9.92446e-06)
(smt.restarting :propagations 415193 :decisions 72446 :conflicts 62 :restart 100 :restart-outer 100 :agility 5.92261e-06)
(smt.restarting :propagations 434230 :decisions 75781 :conflicts 67 :restart 100 :restart-outer 100 :agility 0.000441718)
(smt.restarting :propagations 439158 :decisions 76611 :conflicts 67 :restart 100 :restart-outer 100 :agility 0.000256529)
(smt.restarting :propagations 444274 :decisions 77504 :conflicts 67 :restart 100 :restart-outer 100 :agility 0.000148327)
(smt.restarting :propagations 449729 :decisions 78405 :conflicts 67 :restart 100 :restart-outer 100 :agility 0.000505313)
(smt.restarting :propagations 455359 :decisions 79332 :conflicts 67 :restart 100 :restart-outer 100 :agility 0.000285759)

program still doesn't terminate.