introduced option for nat-as-int in SMT
authorblanchet
Fri Jul 28 15:36:32 2017 +0100 (22 months ago)
changeset 662985ff9fe3fee66
parent 66297 d425bdf419f5
child 66299 1b4aa3e3e4e6
introduced option for nat-as-int in SMT
NEWS
src/HOL/SMT.thy
src/HOL/SMT_Examples/SMT_Examples.certs
src/HOL/SMT_Examples/SMT_Examples.thy
src/HOL/SMT_Examples/SMT_Tests.thy
src/HOL/Tools/SMT/smt_builtin.ML
src/HOL/Tools/SMT/smt_config.ML
src/HOL/Tools/SMT/smt_normalize.ML
     1.1 --- a/NEWS	Thu Jul 27 15:22:35 2017 +0100
     1.2 +++ b/NEWS	Fri Jul 28 15:36:32 2017 +0100
     1.3 @@ -197,6 +197,9 @@
     1.4  Knaster-Tarski fixed point theorem and Galois Connections.
     1.5  
     1.6  * SMT module:
     1.7 +  - A new option, 'smt_nat_as_int', has been added to translate 'nat' to
     1.8 +    'int' and benefit from the SMT solver's theory reasoning. It is disabled
     1.9 +    by default.
    1.10    - The legacy module 'src/HOL/Library/Old_SMT.thy' has been removed.
    1.11    - Several small issues have been rectified in the 'smt' command.
    1.12  
     2.1 --- a/src/HOL/SMT.thy	Thu Jul 27 15:22:35 2017 +0100
     2.2 +++ b/src/HOL/SMT.thy	Fri Jul 28 15:36:32 2017 +0100
     2.3 @@ -119,6 +119,26 @@
     2.4  lemmas min_def_raw = min_def[abs_def]
     2.5  lemmas max_def_raw = max_def[abs_def]
     2.6  
     2.7 +lemma nat_int': "\<forall>n. nat (int n) = n" by simp
     2.8 +lemma int_nat_nneg: "\<forall>i. i \<ge> 0 \<longrightarrow> int (nat i) = i" by simp
     2.9 +lemma int_nat_neg: "\<forall>i. i < 0 \<longrightarrow> int (nat i) = 0" by simp
    2.10 +
    2.11 +lemmas nat_zero_as_int = transfer_nat_int_numerals(1)
    2.12 +lemmas nat_one_as_int = transfer_nat_int_numerals(2)
    2.13 +lemma nat_numeral_as_int: "numeral = (\<lambda>i. nat (numeral i))" by simp
    2.14 +lemma nat_less_as_int: "op < = (\<lambda>a b. int a < int b)" by simp
    2.15 +lemma nat_leq_as_int: "op \<le> = (\<lambda>a b. int a \<le> int b)" by simp
    2.16 +lemma Suc_as_int: "Suc = (\<lambda>a. nat (int a + 1))" by (rule ext) simp
    2.17 +lemma nat_plus_as_int: "op + = (\<lambda>a b. nat (int a + int b))" by (rule ext)+ simp
    2.18 +lemma nat_minus_as_int: "op - = (\<lambda>a b. nat (int a - int b))" by (rule ext)+ simp
    2.19 +lemma nat_times_as_int: "op * = (\<lambda>a b. nat (int a * int b))" by (simp add: nat_mult_distrib)
    2.20 +lemma nat_div_as_int: "op div = (\<lambda>a b. nat (int a div int b))" by (simp add: nat_div_distrib)
    2.21 +lemma nat_mod_as_int: "op mod = (\<lambda>a b. nat (int a mod int b))" by (simp add: nat_mod_distrib)
    2.22 +
    2.23 +lemma int_Suc: "int (Suc n) = int n + 1" by simp
    2.24 +lemma int_plus: "int (n + m) = int n + int m" by (rule of_nat_add)
    2.25 +lemma int_minus: "int (n - m) = int (nat (int n - int m))" by auto
    2.26 +
    2.27  
    2.28  subsection \<open>Integer division and modulo for Z3\<close>
    2.29  
     3.1 --- a/src/HOL/SMT_Examples/SMT_Examples.certs	Thu Jul 27 15:22:35 2017 +0100
     3.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.certs	Fri Jul 28 15:36:32 2017 +0100
     3.3 @@ -6633,3 +6633,1474 @@
     3.4  (let ((@x895 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x117 $x807 (not $x673))) @x891 (or $x807 (not $x673)))))
     3.5  ((_ th-lemma arith farkas -2 -2 1 -1 1 1) (unit-resolution @x895 @x889 $x807) @x485 @x745 @x488 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x134 $x679)) @x584 $x679) (unit-resolution ((_ th-lemma arith) (or false $x564)) @x26 $x564) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
     3.6  
     3.7 +d982bc989c38d6a72f2d807a1168e928070f463b 100 0
     3.8 +unsat
     3.9 +(
    3.10 +a141
    3.11 +a32
    3.12 +a142
    3.13 +a33
    3.14 +a143
    3.15 +a34
    3.16 +a144
    3.17 +a35
    3.18 +a145
    3.19 +a36
    3.20 +a146
    3.21 +a147
    3.22 +a37
    3.23 +a148
    3.24 +a38
    3.25 +a93
    3.26 +a149
    3.27 +a39
    3.28 +a150
    3.29 +a40
    3.30 +a151
    3.31 +a41
    3.32 +a152
    3.33 +a96
    3.34 +a42
    3.35 +a153
    3.36 +a43
    3.37 +a154
    3.38 +a44
    3.39 +a155
    3.40 +a45
    3.41 +a156
    3.42 +a46
    3.43 +a157
    3.44 +a47
    3.45 +a158
    3.46 +a48
    3.47 +a159
    3.48 +a160
    3.49 +a49
    3.50 +a161
    3.51 +a50
    3.52 +a162
    3.53 +a14
    3.54 +a13
    3.55 +a15
    3.56 +a113
    3.57 +a16
    3.58 +a114
    3.59 +a115
    3.60 +a169
    3.61 +a116
    3.62 +a7
    3.63 +a117
    3.64 +a8
    3.65 +a61
    3.66 +a118
    3.67 +a62
    3.68 +a119
    3.69 +a120
    3.70 +a121
    3.71 +a122
    3.72 +a69
    3.73 +a17
    3.74 +a70
    3.75 +a124
    3.76 +a18
    3.77 +a182
    3.78 +a71
    3.79 +a72
    3.80 +a183
    3.81 +a73
    3.82 +a127
    3.83 +a184
    3.84 +a74
    3.85 +a128
    3.86 +a75
    3.87 +a129
    3.88 +a23
    3.89 +a76
    3.90 +a130
    3.91 +a24
    3.92 +a25
    3.93 +a79
    3.94 +a133
    3.95 +a26
    3.96 +a27
    3.97 +a135
    3.98 +a136
    3.99 +a28
   3.100 +a137
   3.101 +a29
   3.102 +a138
   3.103 +a30
   3.104 +a139
   3.105 +a140
   3.106 +a31
   3.107 +)
   3.108 +356e447dfc184b20563d0467365f8b5f8cef0ab1 97 0
   3.109 +unsat
   3.110 +(
   3.111 +a29
   3.112 +a80
   3.113 +a81
   3.114 +a30
   3.115 +a31
   3.116 +a82
   3.117 +a32
   3.118 +a83
   3.119 +a33
   3.120 +a84
   3.121 +a85
   3.122 +a34
   3.123 +a86
   3.124 +a35
   3.125 +a87
   3.126 +a36
   3.127 +a88
   3.128 +a37
   3.129 +a89
   3.130 +a38
   3.131 +a90
   3.132 +a39
   3.133 +a91
   3.134 +a40
   3.135 +a92
   3.136 +a41
   3.137 +a93
   3.138 +a42
   3.139 +a94
   3.140 +a43
   3.141 +a95
   3.142 +a44
   3.143 +a45
   3.144 +a96
   3.145 +a46
   3.146 +a97
   3.147 +a50
   3.148 +a51
   3.149 +a1
   3.150 +a52
   3.151 +a2
   3.152 +a53
   3.153 +a3
   3.154 +a4
   3.155 +a54
   3.156 +a5
   3.157 +a55
   3.158 +a6
   3.159 +a56
   3.160 +a7
   3.161 +a57
   3.162 +a8
   3.163 +a58
   3.164 +a9
   3.165 +a59
   3.166 +a10
   3.167 +a60
   3.168 +a11
   3.169 +a61
   3.170 +a12
   3.171 +a62
   3.172 +a13
   3.173 +a63
   3.174 +a14
   3.175 +a64
   3.176 +a15
   3.177 +a65
   3.178 +a16
   3.179 +a66
   3.180 +a17
   3.181 +a67
   3.182 +a18
   3.183 +a68
   3.184 +a69
   3.185 +a19
   3.186 +a70
   3.187 +a20
   3.188 +a71
   3.189 +a21
   3.190 +a72
   3.191 +a22
   3.192 +a73
   3.193 +a23
   3.194 +a74
   3.195 +a24
   3.196 +a75
   3.197 +a25
   3.198 +a76
   3.199 +a26
   3.200 +a77
   3.201 +a27
   3.202 +a78
   3.203 +a28
   3.204 +a79
   3.205 +)
   3.206 +52fd45adea6478e9d5ad83eff76800476c97a929 2 0
   3.207 +sat
   3.208 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
   3.209 +986242bd9f42b2ccb6c2f7242f7302e1f4a543ef 2 0
   3.210 +sat
   3.211 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
   3.212 +72ac661c77e89ad0f41fb5c62073e8267bf5a6c1 2 0
   3.213 +sat
   3.214 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
   3.215 +707271ac37bbf9aba707687e1d6d62497810fc5d 2 0
   3.216 +sat
   3.217 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
   3.218 +9882e692cde42bbd5ed7cdcd884340dfaa68b016 2 0
   3.219 +sat
   3.220 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
   3.221 +763f8658cf70daf26cd303b055bde69d09e03192 2 0
   3.222 +sat
   3.223 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
   3.224 +5ace894fbc0cab965d77619b71e294a7498ea670 2 0
   3.225 +sat
   3.226 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
   3.227 +35953e5bdfb3c20982931376ab02561049c3d3ec 2 0
   3.228 +sat
   3.229 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
   3.230 +834942f3e869aeabae6a62cc9136262f9e001d9b 2 0
   3.231 +sat
   3.232 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
   3.233 +1915bb36fd704a827d0d979f7d3273ea47ac12ff 2 0
   3.234 +sat
   3.235 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
   3.236 +112b71a74adbf7dc3d30f9548dd7e6e7e507b5cb 90 0
   3.237 +unsat
   3.238 +(
   3.239 +a28
   3.240 +a78
   3.241 +a29
   3.242 +a79
   3.243 +a30
   3.244 +a80
   3.245 +a31
   3.246 +a32
   3.247 +a33
   3.248 +a83
   3.249 +a84
   3.250 +a34
   3.251 +a85
   3.252 +a35
   3.253 +a86
   3.254 +a36
   3.255 +a87
   3.256 +a37
   3.257 +a88
   3.258 +a38
   3.259 +a89
   3.260 +a39
   3.261 +a90
   3.262 +a40
   3.263 +a91
   3.264 +a41
   3.265 +a92
   3.266 +a42
   3.267 +a93
   3.268 +a43
   3.269 +a44
   3.270 +a45
   3.271 +a46
   3.272 +a47
   3.273 +a48
   3.274 +a49
   3.275 +a1
   3.276 +a50
   3.277 +a2
   3.278 +a51
   3.279 +a52
   3.280 +a3
   3.281 +a53
   3.282 +a4
   3.283 +a54
   3.284 +a5
   3.285 +a55
   3.286 +a6
   3.287 +a56
   3.288 +a57
   3.289 +a7
   3.290 +a58
   3.291 +a8
   3.292 +a59
   3.293 +a9
   3.294 +a60
   3.295 +a61
   3.296 +a10
   3.297 +a62
   3.298 +a11
   3.299 +a63
   3.300 +a12
   3.301 +a64
   3.302 +a13
   3.303 +a65
   3.304 +a14
   3.305 +a66
   3.306 +a15
   3.307 +a67
   3.308 +a68
   3.309 +a17
   3.310 +a18
   3.311 +a69
   3.312 +a70
   3.313 +a20
   3.314 +a71
   3.315 +a21
   3.316 +a72
   3.317 +a22
   3.318 +a23
   3.319 +a24
   3.320 +a25
   3.321 +a75
   3.322 +a26
   3.323 +a76
   3.324 +a27
   3.325 +a77
   3.326 +)
   3.327 +55c4468a22c3129940ee0f507180fb5cb8a244d5 2 0
   3.328 +sat
   3.329 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
   3.330 +834270f8dd620f74a77f5565b14e1f3bada38fbc 13 0
   3.331 +unsat
   3.332 +(
   3.333 +a0
   3.334 +a1
   3.335 +a2
   3.336 +a3
   3.337 +a4
   3.338 +a5
   3.339 +a6
   3.340 +a7
   3.341 +a8
   3.342 +a9
   3.343 +)
   3.344 +f22198ac4ffd581fb59d39b6771250bce4f2b10c 13 0
   3.345 +unsat
   3.346 +(
   3.347 +a0
   3.348 +a1
   3.349 +a2
   3.350 +a3
   3.351 +a4
   3.352 +a5
   3.353 +a6
   3.354 +a7
   3.355 +a8
   3.356 +a9
   3.357 +)
   3.358 +c2cfe7fbd368fc0ecc0401a01b53f57caeef131a 4 0
   3.359 +unsat
   3.360 +(
   3.361 +a0
   3.362 +)
   3.363 +1b75f6cb11115d60847d54399897af90dea90827 4 0
   3.364 +unsat
   3.365 +(
   3.366 +a0
   3.367 +)
   3.368 +4998d5a79895ec5f3cef0120dc86abbbd8e29b48 4 0
   3.369 +unsat
   3.370 +(
   3.371 +a2
   3.372 +)
   3.373 +1437414329c2da0f812cda22f62176795fe4b488 2 0
   3.374 +sat
   3.375 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
   3.376 +6ca70dfdb60448a41d66f81903a82cf3bfc1d3c0 6 0
   3.377 +unsat
   3.378 +(
   3.379 +a11
   3.380 +a4
   3.381 +a5
   3.382 +)
   3.383 +2998de44350b8173b123947e09d691282118e3a6 6 0
   3.384 +unsat
   3.385 +(
   3.386 +a0
   3.387 +a1
   3.388 +a2
   3.389 +)
   3.390 +9e56e42500b1c152c4d6f34a9829575456349872 2 0
   3.391 +sat
   3.392 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
   3.393 +20e7bc67dece8e9eee65bc5c217876381ad19805 7 0
   3.394 +unsat
   3.395 +(
   3.396 +a44
   3.397 +a5
   3.398 +a6
   3.399 +a40
   3.400 +)
   3.401 +47a88885e5196eac2e3922eb19ce30b6d748259f 7 0
   3.402 +unsat
   3.403 +(
   3.404 +a0
   3.405 +a1
   3.406 +a3
   3.407 +a5
   3.408 +)
   3.409 +e06991d1826b36a536b8ecef95433bd1f28774f6 2 0
   3.410 +unknown
   3.411 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
   3.412 +5ecd136d06134f07af067717cf168158b90a4fe5 2 0
   3.413 +unknown
   3.414 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
   3.415 +0b10533518bb68ba1619340435dfd68ab76ab077 6 0
   3.416 +unsat
   3.417 +(
   3.418 +a0
   3.419 +a3
   3.420 +a104
   3.421 +)
   3.422 +2a33649206162ac011eff175206722d181426839 6 0
   3.423 +unsat
   3.424 +(
   3.425 +a0
   3.426 +a1
   3.427 +a2
   3.428 +)
   3.429 +375c41e114323d3d731079fe1d402f74a9d2651f 2 0
   3.430 +sat
   3.431 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
   3.432 +e666d5e185fdae30099fc5a288467b6b29dd2412 7 0
   3.433 +unsat
   3.434 +(
   3.435 +a170
   3.436 +a176
   3.437 +a89
   3.438 +a4
   3.439 +)
   3.440 +38448f458cf85259745f3f72f0ef85742b6132c3 7 0
   3.441 +unsat
   3.442 +(
   3.443 +a0
   3.444 +a1
   3.445 +a2
   3.446 +a3
   3.447 +)
   3.448 +3e59b0c055a1eaf3a70cee6780566e0c51865d4c 2 0
   3.449 +sat
   3.450 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
   3.451 +40fc07c6890b8180980355c66bcf18270b94dbe2 5 0
   3.452 +unsat
   3.453 +(
   3.454 +a0
   3.455 +a2
   3.456 +)
   3.457 +a0984a525fc9fe1f8886060622bc7f06810aa427 2 0
   3.458 +sat
   3.459 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
   3.460 +bdd84922010fb8a29483543e42719deb8169a21d 2 0
   3.461 +sat
   3.462 +(error "line 14 column 10: proof is not available")
   3.463 +5229e4ae9267447d5281e256ba94b22471594333 2 0
   3.464 +sat
   3.465 +(error "line 15 column 10: proof is not available")
   3.466 +9931ad6cacee040172b5200df33d2ff766d9ab3f 2 0
   3.467 +sat
   3.468 +(error "line 14 column 10: proof is not available")
   3.469 +24fee7a6227ca691697261bdf9710f47f3306cf4 2 0
   3.470 +sat
   3.471 +(error "line 13 column 10: proof is not available")
   3.472 +f5ea14decc68f09b91c21ca192729ed973297ac3 2 0
   3.473 +sat
   3.474 +(error "line 10 column 10: proof is not available")
   3.475 +c2358f1bb12beb27e84bf6b9d4edbd4a7ce4c606 2 0
   3.476 +sat
   3.477 +(error "line 20 column 10: proof is not available")
   3.478 +1e10ff820821c9cb846ff93eb2274f54845cd885 7 0
   3.479 +unsat
   3.480 +(
   3.481 +a57
   3.482 +a0
   3.483 +a3
   3.484 +a34
   3.485 +)
   3.486 +037b1f2d8c0f457a04260cddd88499544bfb551f 7 0
   3.487 +unsat
   3.488 +(
   3.489 +a0
   3.490 +a1
   3.491 +a2
   3.492 +a3
   3.493 +)
   3.494 +9f1937e419764d5c93a8821ef6d0e32a40427cf1 2 0
   3.495 +unknown
   3.496 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
   3.497 +7eaf5e7924f7478914e32e3781267cee9333ddd4 2 0
   3.498 +unknown
   3.499 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
   3.500 +1c2b6530334930f2f4f6e0d6b73f1d249b6c5fd8 23 0
   3.501 +unsat
   3.502 +((set-logic AUFLIA)
   3.503 +(proof
   3.504 +(let ((?x28 (of_nat$ a$)))
   3.505 +(let (($x57 (>= ?x28 4)))
   3.506 +(let (($x47 (>= ?x28 3)))
   3.507 +(let (($x61 (or $x47 (not $x57))))
   3.508 +(let (($x64 (not $x61)))
   3.509 +(let ((@x51 (monotonicity (rewrite (= (< ?x28 3) (not $x47))) (= (not (< ?x28 3)) (not (not $x47))))))
   3.510 +(let ((@x55 (trans @x51 (rewrite (= (not (not $x47)) $x47)) (= (not (< ?x28 3)) $x47))))
   3.511 +(let ((@x63 (monotonicity @x55 (rewrite (= (< (* 2 ?x28) 7) (not $x57))) (= (or (not (< ?x28 3)) (< (* 2 ?x28) 7)) $x61))))
   3.512 +(let ((@x66 (monotonicity @x63 (= (not (or (not (< ?x28 3)) (< (* 2 ?x28) 7))) $x64))))
   3.513 +(let (($x36 (not (=> (< ?x28 3) (< (* 2 ?x28) 7)))))
   3.514 +(let (($x34 (< (* 2 ?x28) 7)))
   3.515 +(let (($x30 (< ?x28 3)))
   3.516 +(let (($x38 (not $x30)))
   3.517 +(let (($x39 (or $x38 $x34)))
   3.518 +(let ((@x44 (monotonicity (rewrite (= (=> $x30 $x34) $x39)) (= $x36 (not $x39)))))
   3.519 +(let ((@x71 (not-or-elim (mp (asserted $x36) (trans @x44 @x66 (= $x36 $x64)) $x64) $x57)))
   3.520 +(let (($x45 (not $x47)))
   3.521 +(let ((@x70 (not-or-elim (mp (asserted $x36) (trans @x44 @x66 (= $x36 $x64)) $x64) $x45)))
   3.522 +(unit-resolution ((_ th-lemma arith farkas 1 1) $x61) @x70 @x71 false)))))))))))))))))))))
   3.523 +
   3.524 +995f80f06d5874ea2208846fb3b3217c3a3b9bfd 147 0
   3.525 +unsat
   3.526 +((set-logic AUFLIA)
   3.527 +(proof
   3.528 +(let ((?x29 (of_nat$ y$)))
   3.529 +(let ((?x30 (+ 1 ?x29)))
   3.530 +(let ((?x31 (nat$ ?x30)))
   3.531 +(let ((?x32 (of_nat$ ?x31)))
   3.532 +(let ((?x43 (* (- 1) ?x29)))
   3.533 +(let ((?x44 (+ ?x43 ?x32)))
   3.534 +(let ((?x47 (nat$ ?x44)))
   3.535 +(let ((?x50 (of_nat$ ?x47)))
   3.536 +(let ((?x567 (* (- 1) ?x32)))
   3.537 +(let ((?x255 (+ ?x29 ?x567 ?x50)))
   3.538 +(let (($x513 (>= ?x255 0)))
   3.539 +(let (($x532 (= ?x255 0)))
   3.540 +(let ((?x568 (+ ?x29 ?x567)))
   3.541 +(let (($x248 (<= ?x568 0)))
   3.542 +(let (($x551 (<= ?x568 (- 1))))
   3.543 +(let (($x558 (= ?x568 (- 1))))
   3.544 +(let (($x229 (>= ?x29 (- 1))))
   3.545 +(let (($x387 (>= ?x29 0)))
   3.546 +(let ((?x154 (nat$ ?x29)))
   3.547 +(let ((?x388 (of_nat$ ?x154)))
   3.548 +(let (($x352 (= ?x388 0)))
   3.549 +(let (($x498 (or $x387 $x352)))
   3.550 +(let (($x584 (forall ((?v0 Int) )(! (let ((?x81 (nat$ ?v0)))
   3.551 +(let ((?x82 (of_nat$ ?x81)))
   3.552 +(let (($x110 (= ?x82 0)))
   3.553 +(let (($x95 (>= ?v0 0)))
   3.554 +(or $x95 $x110))))) :pattern ( (nat$ ?v0) ) :qid k!11))
   3.555 +))
   3.556 +(let (($x133 (forall ((?v0 Int) )(! (let ((?x81 (nat$ ?v0)))
   3.557 +(let ((?x82 (of_nat$ ?x81)))
   3.558 +(let (($x110 (= ?x82 0)))
   3.559 +(let (($x95 (>= ?v0 0)))
   3.560 +(or $x95 $x110))))) :qid k!11))
   3.561 +))
   3.562 +(let ((?x81 (nat$ ?0)))
   3.563 +(let ((?x82 (of_nat$ ?x81)))
   3.564 +(let (($x110 (= ?x82 0)))
   3.565 +(let (($x95 (>= ?0 0)))
   3.566 +(let (($x130 (or $x95 $x110)))
   3.567 +(let (($x112 (forall ((?v0 Int) )(! (let ((?x81 (nat$ ?v0)))
   3.568 +(let ((?x82 (of_nat$ ?x81)))
   3.569 +(let (($x110 (= ?x82 0)))
   3.570 +(let (($x109 (< ?v0 0)))
   3.571 +(=> $x109 $x110))))) :qid k!11))
   3.572 +))
   3.573 +(let (($x118 (forall ((?v0 Int) )(! (let ((?x81 (nat$ ?v0)))
   3.574 +(let ((?x82 (of_nat$ ?x81)))
   3.575 +(let (($x110 (= ?x82 0)))
   3.576 +(let (($x109 (< ?v0 0)))
   3.577 +(let (($x114 (not $x109)))
   3.578 +(or $x114 $x110)))))) :qid k!11))
   3.579 +))
   3.580 +(let ((@x125 (monotonicity (rewrite (= (< ?0 0) (not $x95))) (= (not (< ?0 0)) (not (not $x95))))))
   3.581 +(let ((@x129 (trans @x125 (rewrite (= (not (not $x95)) $x95)) (= (not (< ?0 0)) $x95))))
   3.582 +(let ((@x135 (quant-intro (monotonicity @x129 (= (or (not (< ?0 0)) $x110) $x130)) (= $x118 $x133))))
   3.583 +(let ((@x117 (rewrite (= (=> (< ?0 0) $x110) (or (not (< ?0 0)) $x110)))))
   3.584 +(let ((@x138 (mp (asserted $x112) (trans (quant-intro @x117 (= $x112 $x118)) @x135 (= $x112 $x133)) $x133)))
   3.585 +(let ((@x589 (mp (mp~ @x138 (nnf-pos (refl (~ $x130 $x130)) (~ $x133 $x133)) $x133) (quant-intro (refl (= $x130 $x130)) (= $x133 $x584)) $x584)))
   3.586 +(let (($x555 (not $x584)))
   3.587 +(let (($x500 (or $x555 $x387 $x352)))
   3.588 +(let ((@x404 (mp ((_ quant-inst (of_nat$ y$)) (or $x555 $x498)) (rewrite (= (or $x555 $x498) $x500)) $x500)))
   3.589 +(let ((@x487 (unit-resolution (unit-resolution @x404 @x589 $x498) (hypothesis (not $x387)) $x352)))
   3.590 +(let (($x239 (= ?x154 y$)))
   3.591 +(let (($x570 (forall ((?v0 Nat$) )(! (= (nat$ (of_nat$ ?v0)) ?v0) :pattern ( (of_nat$ ?v0) ) :qid k!9))
   3.592 +))
   3.593 +(let (($x77 (forall ((?v0 Nat$) )(! (= (nat$ (of_nat$ ?v0)) ?v0) :qid k!9))
   3.594 +))
   3.595 +(let ((@x575 (trans (rewrite (= $x77 $x570)) (rewrite (= $x570 $x570)) (= $x77 $x570))))
   3.596 +(let ((@x144 (refl (~ (= (nat$ (of_nat$ ?0)) ?0) (= (nat$ (of_nat$ ?0)) ?0)))))
   3.597 +(let ((@x576 (mp (mp~ (asserted $x77) (nnf-pos @x144 (~ $x77 $x77)) $x77) @x575 $x570)))
   3.598 +(let (($x241 (not $x570)))
   3.599 +(let (($x231 (or $x241 $x239)))
   3.600 +(let ((@x242 ((_ quant-inst y$) $x231)))
   3.601 +(let ((@x475 (monotonicity (symm (unit-resolution @x242 @x576 $x239) (= y$ ?x154)) (= ?x29 ?x388))))
   3.602 +(let ((@x480 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= ?x29 0)) $x387)) (hypothesis (not $x387)) (trans @x475 @x487 (= ?x29 0)) false)))
   3.603 +(let ((@x468 (unit-resolution ((_ th-lemma arith farkas 1 1) (or (not $x387) $x229)) (lemma @x480 $x387) $x229)))
   3.604 +(let (($x564 (not $x229)))
   3.605 +(let (($x559 (or $x564 $x558)))
   3.606 +(let (($x578 (forall ((?v0 Int) )(! (let ((?x81 (nat$ ?v0)))
   3.607 +(let ((?x82 (of_nat$ ?x81)))
   3.608 +(let (($x83 (= ?x82 ?v0)))
   3.609 +(let (($x95 (>= ?v0 0)))
   3.610 +(let (($x97 (not $x95)))
   3.611 +(or $x97 $x83)))))) :pattern ( (nat$ ?v0) ) :qid k!10))
   3.612 +))
   3.613 +(let (($x103 (forall ((?v0 Int) )(! (let ((?x81 (nat$ ?v0)))
   3.614 +(let ((?x82 (of_nat$ ?x81)))
   3.615 +(let (($x83 (= ?x82 ?v0)))
   3.616 +(let (($x95 (>= ?v0 0)))
   3.617 +(let (($x97 (not $x95)))
   3.618 +(or $x97 $x83)))))) :qid k!10))
   3.619 +))
   3.620 +(let ((@x580 (refl (= (or (not $x95) (= ?x82 ?0)) (or (not $x95) (= ?x82 ?0))))))
   3.621 +(let ((@x139 (refl (~ (or (not $x95) (= ?x82 ?0)) (or (not $x95) (= ?x82 ?0))))))
   3.622 +(let (($x85 (forall ((?v0 Int) )(! (let ((?x81 (nat$ ?v0)))
   3.623 +(let ((?x82 (of_nat$ ?x81)))
   3.624 +(let (($x83 (= ?x82 ?v0)))
   3.625 +(let (($x80 (<= 0 ?v0)))
   3.626 +(=> $x80 $x83))))) :qid k!10))
   3.627 +))
   3.628 +(let (($x91 (forall ((?v0 Int) )(! (let ((?x81 (nat$ ?v0)))
   3.629 +(let ((?x82 (of_nat$ ?x81)))
   3.630 +(let (($x83 (= ?x82 ?v0)))
   3.631 +(or (not (<= 0 ?v0)) $x83)))) :qid k!10))
   3.632 +))
   3.633 +(let (($x83 (= ?x82 ?0)))
   3.634 +(let (($x97 (not $x95)))
   3.635 +(let (($x100 (or $x97 $x83)))
   3.636 +(let (($x88 (or (not (<= 0 ?0)) $x83)))
   3.637 +(let ((@x99 (monotonicity (rewrite (= (<= 0 ?0) $x95)) (= (not (<= 0 ?0)) $x97))))
   3.638 +(let ((@x93 (quant-intro (rewrite (= (=> (<= 0 ?0) $x83) $x88)) (= $x85 $x91))))
   3.639 +(let ((@x107 (trans @x93 (quant-intro (monotonicity @x99 (= $x88 $x100)) (= $x91 $x103)) (= $x85 $x103))))
   3.640 +(let ((@x148 (mp~ (mp (asserted $x85) @x107 $x103) (nnf-pos @x139 (~ $x103 $x103)) $x103)))
   3.641 +(let ((@x583 (mp @x148 (quant-intro @x580 (= $x103 $x578)) $x578)))
   3.642 +(let (($x202 (not $x578)))
   3.643 +(let (($x544 (or $x202 $x564 $x558)))
   3.644 +(let (($x557 (or (not (>= ?x30 0)) (= ?x32 ?x30))))
   3.645 +(let (($x205 (or $x202 $x557)))
   3.646 +(let ((@x566 (monotonicity (rewrite (= (>= ?x30 0) $x229)) (= (not (>= ?x30 0)) $x564))))
   3.647 +(let ((@x560 (monotonicity @x566 (rewrite (= (= ?x32 ?x30) $x558)) (= $x557 $x559))))
   3.648 +(let ((@x549 (trans (monotonicity @x560 (= $x205 (or $x202 $x559))) (rewrite (= (or $x202 $x559) $x544)) (= $x205 $x544))))
   3.649 +(let ((@x550 (mp ((_ quant-inst (+ 1 ?x29)) $x205) @x549 $x544)))
   3.650 +(let ((@x453 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x558) $x551)) (unit-resolution (unit-resolution @x550 @x583 $x559) @x468 $x558) $x551)))
   3.651 +(let (($x251 (not $x248)))
   3.652 +(let (($x535 (or $x251 $x532)))
   3.653 +(let (($x523 (or $x202 $x251 $x532)))
   3.654 +(let (($x541 (or (not (>= ?x44 0)) (= ?x50 ?x44))))
   3.655 +(let (($x524 (or $x202 $x541)))
   3.656 +(let ((@x531 (monotonicity (rewrite (= (>= ?x44 0) $x248)) (= (not (>= ?x44 0)) $x251))))
   3.657 +(let ((@x522 (monotonicity @x531 (rewrite (= (= ?x50 ?x44) $x532)) (= $x541 $x535))))
   3.658 +(let ((@x369 (trans (monotonicity @x522 (= $x524 (or $x202 $x535))) (rewrite (= (or $x202 $x535) $x523)) (= $x524 $x523))))
   3.659 +(let ((@x511 (mp ((_ quant-inst (+ ?x43 ?x32)) $x524) @x369 $x523)))
   3.660 +(let ((@x459 (unit-resolution (unit-resolution @x511 @x583 $x535) (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x248 (not $x551))) @x453 $x248) $x532)))
   3.661 +(let (($x59 (<= ?x50 0)))
   3.662 +(let ((@x65 (monotonicity (rewrite (= (< 0 ?x50) (not $x59))) (= (not (< 0 ?x50)) (not (not $x59))))))
   3.663 +(let ((@x69 (trans @x65 (rewrite (= (not (not $x59)) $x59)) (= (not (< 0 ?x50)) $x59))))
   3.664 +(let (($x53 (< 0 ?x50)))
   3.665 +(let (($x56 (not $x53)))
   3.666 +(let (($x38 (not (< (* 0 ?x32) (of_nat$ (nat$ (- ?x32 ?x29)))))))
   3.667 +(let ((@x49 (monotonicity (rewrite (= (- ?x32 ?x29) ?x44)) (= (nat$ (- ?x32 ?x29)) ?x47))))
   3.668 +(let ((@x55 (monotonicity (rewrite (= (* 0 ?x32) 0)) (monotonicity @x49 (= (of_nat$ (nat$ (- ?x32 ?x29))) ?x50)) (= (< (* 0 ?x32) (of_nat$ (nat$ (- ?x32 ?x29)))) $x53))))
   3.669 +(let ((@x72 (mp (asserted $x38) (trans (monotonicity @x55 (= $x38 $x56)) @x69 (= $x38 $x59)) $x59)))
   3.670 +((_ th-lemma arith farkas -1 -1 1) @x72 @x453 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x532) $x513)) @x459 $x513) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   3.671 +
   3.672 +49c385b161a0c500f84c45f85272a8ec9574fef4 126 0
   3.673 +unsat
   3.674 +((set-logic AUFLIA)
   3.675 +(proof
   3.676 +(let ((?x29 (of_nat$ x$)))
   3.677 +(let ((?x30 (* 2 ?x29)))
   3.678 +(let ((?x31 (nat$ ?x30)))
   3.679 +(let ((?x212 (of_nat$ ?x31)))
   3.680 +(let ((?x532 (* (- 1) ?x212)))
   3.681 +(let ((?x533 (+ ?x30 ?x532)))
   3.682 +(let (($x513 (<= ?x533 0)))
   3.683 +(let (($x531 (= ?x533 0)))
   3.684 +(let (($x193 (>= ?x29 0)))
   3.685 +(let (($x487 (>= ?x212 1)))
   3.686 +(let (($x485 (= ?x212 1)))
   3.687 +(let ((?x33 (nat$ 1)))
   3.688 +(let ((?x504 (of_nat$ ?x33)))
   3.689 +(let (($x505 (= ?x504 1)))
   3.690 +(let (($x546 (forall ((?v0 Int) )(! (let ((?x49 (nat$ ?v0)))
   3.691 +(let ((?x50 (of_nat$ ?x49)))
   3.692 +(let (($x51 (= ?x50 ?v0)))
   3.693 +(let (($x64 (>= ?v0 0)))
   3.694 +(let (($x65 (not $x64)))
   3.695 +(or $x65 $x51)))))) :pattern ( (nat$ ?v0) ) :qid k!10))
   3.696 +))
   3.697 +(let (($x71 (forall ((?v0 Int) )(! (let ((?x49 (nat$ ?v0)))
   3.698 +(let ((?x50 (of_nat$ ?x49)))
   3.699 +(let (($x51 (= ?x50 ?v0)))
   3.700 +(let (($x64 (>= ?v0 0)))
   3.701 +(let (($x65 (not $x64)))
   3.702 +(or $x65 $x51)))))) :qid k!10))
   3.703 +))
   3.704 +(let ((?x49 (nat$ ?0)))
   3.705 +(let ((?x50 (of_nat$ ?x49)))
   3.706 +(let (($x51 (= ?x50 ?0)))
   3.707 +(let (($x64 (>= ?0 0)))
   3.708 +(let (($x65 (not $x64)))
   3.709 +(let (($x68 (or $x65 $x51)))
   3.710 +(let (($x53 (forall ((?v0 Int) )(! (let ((?x49 (nat$ ?v0)))
   3.711 +(let ((?x50 (of_nat$ ?x49)))
   3.712 +(let (($x51 (= ?x50 ?v0)))
   3.713 +(let (($x48 (<= 0 ?v0)))
   3.714 +(=> $x48 $x51))))) :qid k!10))
   3.715 +))
   3.716 +(let (($x59 (forall ((?v0 Int) )(! (let ((?x49 (nat$ ?v0)))
   3.717 +(let ((?x50 (of_nat$ ?x49)))
   3.718 +(let (($x51 (= ?x50 ?v0)))
   3.719 +(or (not (<= 0 ?v0)) $x51)))) :qid k!10))
   3.720 +))
   3.721 +(let ((@x67 (monotonicity (rewrite (= (<= 0 ?0) $x64)) (= (not (<= 0 ?0)) $x65))))
   3.722 +(let ((@x73 (quant-intro (monotonicity @x67 (= (or (not (<= 0 ?0)) $x51) $x68)) (= $x59 $x71))))
   3.723 +(let ((@x58 (rewrite (= (=> (<= 0 ?0) $x51) (or (not (<= 0 ?0)) $x51)))))
   3.724 +(let ((@x76 (mp (asserted $x53) (trans (quant-intro @x58 (= $x53 $x59)) @x73 (= $x53 $x71)) $x71)))
   3.725 +(let ((@x551 (mp (mp~ @x76 (nnf-pos (refl (~ $x68 $x68)) (~ $x71 $x71)) $x71) (quant-intro (refl (= $x68 $x68)) (= $x71 $x546)) $x546)))
   3.726 +(let (($x526 (not $x546)))
   3.727 +(let (($x489 (or $x526 $x505)))
   3.728 +(let ((@x506 (rewrite (= (>= 1 0) true))))
   3.729 +(let ((@x219 (trans (monotonicity @x506 (= (not (>= 1 0)) (not true))) (rewrite (= (not true) false)) (= (not (>= 1 0)) false))))
   3.730 +(let ((@x223 (monotonicity @x219 (= (or (not (>= 1 0)) $x505) (or false $x505)))))
   3.731 +(let ((@x503 (trans @x223 (rewrite (= (or false $x505) $x505)) (= (or (not (>= 1 0)) $x505) $x505))))
   3.732 +(let ((@x493 (monotonicity @x503 (= (or $x526 (or (not (>= 1 0)) $x505)) $x489))))
   3.733 +(let ((@x496 (trans @x493 (rewrite (= $x489 $x489)) (= (or $x526 (or (not (>= 1 0)) $x505)) $x489))))
   3.734 +(let ((@x497 (mp ((_ quant-inst 1) (or $x526 (or (not (>= 1 0)) $x505))) @x496 $x489)))
   3.735 +(let (($x34 (= ?x31 ?x33)))
   3.736 +(let ((@x42 (mp (asserted (not (not $x34))) (rewrite (= (not (not $x34)) $x34)) $x34)))
   3.737 +(let ((@x356 (trans (monotonicity @x42 (= ?x212 ?x504)) (unit-resolution @x497 @x551 $x505) $x485)))
   3.738 +(let ((@x371 (unit-resolution ((_ th-lemma arith farkas 1 1) (or (not $x487) (not (<= ?x212 0)))) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x485) $x487)) @x356 $x487) (not (<= ?x212 0)))))
   3.739 +(let ((@x374 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= ?x212 0)) (<= ?x212 0))) @x371 (not (= ?x212 0)))))
   3.740 +(let (($x515 (= ?x212 0)))
   3.741 +(let (($x517 (or $x193 $x515)))
   3.742 +(let (($x552 (forall ((?v0 Int) )(! (let ((?x49 (nat$ ?v0)))
   3.743 +(let ((?x50 (of_nat$ ?x49)))
   3.744 +(let (($x78 (= ?x50 0)))
   3.745 +(let (($x64 (>= ?v0 0)))
   3.746 +(or $x64 $x78))))) :pattern ( (nat$ ?v0) ) :qid k!11))
   3.747 +))
   3.748 +(let (($x101 (forall ((?v0 Int) )(! (let ((?x49 (nat$ ?v0)))
   3.749 +(let ((?x50 (of_nat$ ?x49)))
   3.750 +(let (($x78 (= ?x50 0)))
   3.751 +(let (($x64 (>= ?v0 0)))
   3.752 +(or $x64 $x78))))) :qid k!11))
   3.753 +))
   3.754 +(let ((@x556 (quant-intro (refl (= (or $x64 (= ?x50 0)) (or $x64 (= ?x50 0)))) (= $x101 $x552))))
   3.755 +(let ((@x120 (nnf-pos (refl (~ (or $x64 (= ?x50 0)) (or $x64 (= ?x50 0)))) (~ $x101 $x101))))
   3.756 +(let (($x80 (forall ((?v0 Int) )(! (let ((?x49 (nat$ ?v0)))
   3.757 +(let ((?x50 (of_nat$ ?x49)))
   3.758 +(let (($x78 (= ?x50 0)))
   3.759 +(let (($x77 (< ?v0 0)))
   3.760 +(=> $x77 $x78))))) :qid k!11))
   3.761 +))
   3.762 +(let (($x86 (forall ((?v0 Int) )(! (let ((?x49 (nat$ ?v0)))
   3.763 +(let ((?x50 (of_nat$ ?x49)))
   3.764 +(let (($x78 (= ?x50 0)))
   3.765 +(let (($x77 (< ?v0 0)))
   3.766 +(let (($x82 (not $x77)))
   3.767 +(or $x82 $x78)))))) :qid k!11))
   3.768 +))
   3.769 +(let (($x78 (= ?x50 0)))
   3.770 +(let (($x98 (or $x64 $x78)))
   3.771 +(let (($x77 (< ?0 0)))
   3.772 +(let (($x82 (not $x77)))
   3.773 +(let (($x83 (or $x82 $x78)))
   3.774 +(let ((@x97 (trans (monotonicity (rewrite (= $x77 $x65)) (= $x82 (not $x65))) (rewrite (= (not $x65) $x64)) (= $x82 $x64))))
   3.775 +(let ((@x105 (trans (quant-intro (rewrite (= (=> $x77 $x78) $x83)) (= $x80 $x86)) (quant-intro (monotonicity @x97 (= $x83 $x98)) (= $x86 $x101)) (= $x80 $x101))))
   3.776 +(let ((@x557 (mp (mp~ (mp (asserted $x80) @x105 $x101) @x120 $x101) @x556 $x552)))
   3.777 +(let (($x156 (not $x552)))
   3.778 +(let (($x520 (or $x156 $x193 $x515)))
   3.779 +(let ((@x530 (rewrite (= (>= ?x30 0) $x193))))
   3.780 +(let ((@x523 (monotonicity (monotonicity @x530 (= (or (>= ?x30 0) $x515) $x517)) (= (or $x156 (or (>= ?x30 0) $x515)) (or $x156 $x517)))))
   3.781 +(let ((@x215 (trans @x523 (rewrite (= (or $x156 $x517) $x520)) (= (or $x156 (or (>= ?x30 0) $x515)) $x520))))
   3.782 +(let ((@x229 (mp ((_ quant-inst (* 2 ?x29)) (or $x156 (or (>= ?x30 0) $x515))) @x215 $x520)))
   3.783 +(let (($x185 (not $x193)))
   3.784 +(let (($x534 (or $x185 $x531)))
   3.785 +(let (($x188 (or $x526 $x185 $x531)))
   3.786 +(let (($x213 (= ?x212 ?x30)))
   3.787 +(let (($x208 (>= ?x30 0)))
   3.788 +(let (($x209 (not $x208)))
   3.789 +(let (($x214 (or $x209 $x213)))
   3.790 +(let (($x189 (or $x526 $x214)))
   3.791 +(let ((@x536 (monotonicity (monotonicity @x530 (= $x209 $x185)) (rewrite (= $x213 $x531)) (= $x214 $x534))))
   3.792 +(let ((@x175 (trans (monotonicity @x536 (= $x189 (or $x526 $x534))) (rewrite (= (or $x526 $x534) $x188)) (= $x189 $x188))))
   3.793 +(let ((@x176 (mp ((_ quant-inst (* 2 ?x29)) $x189) @x175 $x188)))
   3.794 +(let ((@x470 (unit-resolution (unit-resolution @x176 @x551 $x534) (unit-resolution (unit-resolution @x229 @x557 $x517) @x374 $x193) $x531)))
   3.795 +(let (($x514 (>= ?x533 0)))
   3.796 +(let (($x486 (<= ?x212 1)))
   3.797 +((_ th-lemma arith gcd-test -1/2 -1/2 -1/2 -1/2) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x485) $x487)) @x356 $x487) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x485) $x486)) @x356 $x486) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x531) $x514)) @x470 $x514) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x531) $x513)) @x470 $x513) false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   3.798 +
   3.799 +b2e870cca8f9ff26b649a7a2c6910fff2183e779 6 0
   3.800 +unsat
   3.801 +(
   3.802 +a0
   3.803 +a259
   3.804 +a260
   3.805 +)
   3.806 +0df05630a046f3db612e71e7557cbf94daec55ea 6 0
   3.807 +unsat
   3.808 +(
   3.809 +a0
   3.810 +a2
   3.811 +a3
   3.812 +)
   3.813 +5d99a07ea08069a53b86d7f3330815887331e82a 145 0
   3.814 +unsat
   3.815 +((set-logic AUFLIA)
   3.816 +(proof
   3.817 +(let ((?x29 (of_nat$ y$)))
   3.818 +(let ((?x30 (+ 1 ?x29)))
   3.819 +(let ((?x31 (nat$ ?x30)))
   3.820 +(let ((?x32 (of_nat$ ?x31)))
   3.821 +(let ((?x48 (+ (- 1) ?x32)))
   3.822 +(let ((?x51 (nat$ ?x48)))
   3.823 +(let ((?x585 (of_nat$ ?x51)))
   3.824 +(let ((?x299 (* (- 1) ?x585)))
   3.825 +(let ((?x434 (+ ?x29 ?x299)))
   3.826 +(let (($x436 (>= ?x434 0)))
   3.827 +(let (($x558 (= ?x29 ?x585)))
   3.828 +(let (($x54 (= ?x51 y$)))
   3.829 +(let (($x88 (<= ?x32 0)))
   3.830 +(let (($x98 (not (or (= (not $x88) $x54) (not $x88)))))
   3.831 +(let (($x40 (=> (not (ite (< 0 ?x32) true false)) false)))
   3.832 +(let (($x33 (< 0 ?x32)))
   3.833 +(let (($x34 (ite $x33 true false)))
   3.834 +(let (($x38 (= $x34 (= (nat$ (- ?x32 1)) y$))))
   3.835 +(let (($x42 (or false (or $x38 $x40))))
   3.836 +(let (($x43 (not $x42)))
   3.837 +(let (($x60 (= $x33 $x54)))
   3.838 +(let (($x75 (or $x60 $x33)))
   3.839 +(let ((@x94 (monotonicity (rewrite (= $x33 (not $x88))) (= $x60 (= (not $x88) $x54)))))
   3.840 +(let ((@x97 (monotonicity @x94 (rewrite (= $x33 (not $x88))) (= $x75 (or (= (not $x88) $x54) (not $x88))))))
   3.841 +(let ((@x70 (monotonicity (monotonicity (rewrite (= $x34 $x33)) (= (not $x34) (not $x33))) (= $x40 (=> (not $x33) false)))))
   3.842 +(let ((@x74 (trans @x70 (rewrite (= (=> (not $x33) false) $x33)) (= $x40 $x33))))
   3.843 +(let ((@x53 (monotonicity (rewrite (= (- ?x32 1) ?x48)) (= (nat$ (- ?x32 1)) ?x51))))
   3.844 +(let ((@x59 (monotonicity (rewrite (= $x34 $x33)) (monotonicity @x53 (= (= (nat$ (- ?x32 1)) y$) $x54)) (= $x38 (= $x33 $x54)))))
   3.845 +(let ((@x77 (monotonicity (trans @x59 (rewrite (= (= $x33 $x54) $x60)) (= $x38 $x60)) @x74 (= (or $x38 $x40) $x75))))
   3.846 +(let ((@x84 (trans (monotonicity @x77 (= $x42 (or false $x75))) (rewrite (= (or false $x75) $x75)) (= $x42 $x75))))
   3.847 +(let ((@x102 (trans (monotonicity @x84 (= $x43 (not $x75))) (monotonicity @x97 (= (not $x75) $x98)) (= $x43 $x98))))
   3.848 +(let ((@x106 (not-or-elim (mp (asserted $x43) @x102 $x98) $x88)))
   3.849 +(let ((@x187 (monotonicity (iff-true @x106 (= $x88 true)) (= (= $x88 $x54) (= true $x54)))))
   3.850 +(let ((@x191 (trans @x187 (rewrite (= (= true $x54) $x54)) (= (= $x88 $x54) $x54))))
   3.851 +(let (($x173 (= $x88 $x54)))
   3.852 +(let ((@x105 (not-or-elim (mp (asserted $x43) @x102 $x98) (not (= (not $x88) $x54)))))
   3.853 +(let ((@x192 (mp (mp @x105 (rewrite (= (not (= (not $x88) $x54)) $x173)) $x173) @x191 $x54)))
   3.854 +(let ((@x457 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x558) $x436)) (monotonicity (symm @x192 (= y$ ?x51)) $x558) $x436)))
   3.855 +(let ((?x613 (* (- 1) ?x32)))
   3.856 +(let ((?x614 (+ ?x29 ?x613)))
   3.857 +(let (($x595 (<= ?x614 (- 1))))
   3.858 +(let (($x612 (= ?x614 (- 1))))
   3.859 +(let (($x610 (>= ?x29 (- 1))))
   3.860 +(let (($x557 (>= ?x585 0)))
   3.861 +(let (($x559 (= ?x585 0)))
   3.862 +(let (($x586 (>= ?x32 1)))
   3.863 +(let (($x589 (not $x586)))
   3.864 +(let (($x632 (forall ((?v0 Int) )(! (let ((?x115 (nat$ ?v0)))
   3.865 +(let ((?x116 (of_nat$ ?x115)))
   3.866 +(let (($x144 (= ?x116 0)))
   3.867 +(let (($x129 (>= ?v0 0)))
   3.868 +(or $x129 $x144))))) :pattern ( (nat$ ?v0) ) :qid k!11))
   3.869 +))
   3.870 +(let (($x167 (forall ((?v0 Int) )(! (let ((?x115 (nat$ ?v0)))
   3.871 +(let ((?x116 (of_nat$ ?x115)))
   3.872 +(let (($x144 (= ?x116 0)))
   3.873 +(let (($x129 (>= ?v0 0)))
   3.874 +(or $x129 $x144))))) :qid k!11))
   3.875 +))
   3.876 +(let ((?x115 (nat$ ?0)))
   3.877 +(let ((?x116 (of_nat$ ?x115)))
   3.878 +(let (($x144 (= ?x116 0)))
   3.879 +(let (($x129 (>= ?0 0)))
   3.880 +(let (($x164 (or $x129 $x144)))
   3.881 +(let (($x146 (forall ((?v0 Int) )(! (let ((?x115 (nat$ ?v0)))
   3.882 +(let ((?x116 (of_nat$ ?x115)))
   3.883 +(let (($x144 (= ?x116 0)))
   3.884 +(let (($x143 (< ?v0 0)))
   3.885 +(=> $x143 $x144))))) :qid k!11))
   3.886 +))
   3.887 +(let (($x152 (forall ((?v0 Int) )(! (let ((?x115 (nat$ ?v0)))
   3.888 +(let ((?x116 (of_nat$ ?x115)))
   3.889 +(let (($x144 (= ?x116 0)))
   3.890 +(let (($x143 (< ?v0 0)))
   3.891 +(let (($x148 (not $x143)))
   3.892 +(or $x148 $x144)))))) :qid k!11))
   3.893 +))
   3.894 +(let ((@x159 (monotonicity (rewrite (= (< ?0 0) (not $x129))) (= (not (< ?0 0)) (not (not $x129))))))
   3.895 +(let ((@x163 (trans @x159 (rewrite (= (not (not $x129)) $x129)) (= (not (< ?0 0)) $x129))))
   3.896 +(let ((@x169 (quant-intro (monotonicity @x163 (= (or (not (< ?0 0)) $x144) $x164)) (= $x152 $x167))))
   3.897 +(let ((@x151 (rewrite (= (=> (< ?0 0) $x144) (or (not (< ?0 0)) $x144)))))
   3.898 +(let ((@x172 (mp (asserted $x146) (trans (quant-intro @x151 (= $x146 $x152)) @x169 (= $x146 $x167)) $x167)))
   3.899 +(let ((@x637 (mp (mp~ @x172 (nnf-pos (refl (~ $x164 $x164)) (~ $x167 $x167)) $x167) (quant-intro (refl (= $x164 $x164)) (= $x167 $x632)) $x632)))
   3.900 +(let (($x601 (not $x632)))
   3.901 +(let (($x564 (or $x601 $x586 $x559)))
   3.902 +(let ((@x588 (rewrite (= (>= ?x48 0) $x586))))
   3.903 +(let ((@x394 (monotonicity (monotonicity @x588 (= (or (>= ?x48 0) $x559) (or $x586 $x559))) (= (or $x601 (or (>= ?x48 0) $x559)) (or $x601 (or $x586 $x559))))))
   3.904 +(let ((@x554 (trans @x394 (rewrite (= (or $x601 (or $x586 $x559)) $x564)) (= (or $x601 (or (>= ?x48 0) $x559)) $x564))))
   3.905 +(let ((@x555 (mp ((_ quant-inst (+ (- 1) ?x32)) (or $x601 (or (>= ?x48 0) $x559))) @x554 $x564)))
   3.906 +(let ((@x539 (unit-resolution @x555 @x637 (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x589 (not $x88))) @x106 $x589) $x559)))
   3.907 +(let ((@x545 (unit-resolution ((_ th-lemma arith assign-bounds 1 1) (or $x610 (not $x557) (not $x436))) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x559) $x557)) @x539 $x557) @x457 $x610)))
   3.908 +(let (($x605 (not $x610)))
   3.909 +(let (($x616 (or $x605 $x612)))
   3.910 +(let (($x626 (forall ((?v0 Int) )(! (let ((?x115 (nat$ ?v0)))
   3.911 +(let ((?x116 (of_nat$ ?x115)))
   3.912 +(let (($x117 (= ?x116 ?v0)))
   3.913 +(let (($x129 (>= ?v0 0)))
   3.914 +(let (($x131 (not $x129)))
   3.915 +(or $x131 $x117)))))) :pattern ( (nat$ ?v0) ) :qid k!10))
   3.916 +))
   3.917 +(let (($x137 (forall ((?v0 Int) )(! (let ((?x115 (nat$ ?v0)))
   3.918 +(let ((?x116 (of_nat$ ?x115)))
   3.919 +(let (($x117 (= ?x116 ?v0)))
   3.920 +(let (($x129 (>= ?v0 0)))
   3.921 +(let (($x131 (not $x129)))
   3.922 +(or $x131 $x117)))))) :qid k!10))
   3.923 +))
   3.924 +(let ((@x628 (refl (= (or (not $x129) (= ?x116 ?0)) (or (not $x129) (= ?x116 ?0))))))
   3.925 +(let ((@x185 (refl (~ (or (not $x129) (= ?x116 ?0)) (or (not $x129) (= ?x116 ?0))))))
   3.926 +(let (($x119 (forall ((?v0 Int) )(! (let ((?x115 (nat$ ?v0)))
   3.927 +(let ((?x116 (of_nat$ ?x115)))
   3.928 +(let (($x117 (= ?x116 ?v0)))
   3.929 +(let (($x114 (<= 0 ?v0)))
   3.930 +(=> $x114 $x117))))) :qid k!10))
   3.931 +))
   3.932 +(let (($x125 (forall ((?v0 Int) )(! (let ((?x115 (nat$ ?v0)))
   3.933 +(let ((?x116 (of_nat$ ?x115)))
   3.934 +(let (($x117 (= ?x116 ?v0)))
   3.935 +(or (not (<= 0 ?v0)) $x117)))) :qid k!10))
   3.936 +))
   3.937 +(let (($x117 (= ?x116 ?0)))
   3.938 +(let (($x131 (not $x129)))
   3.939 +(let (($x134 (or $x131 $x117)))
   3.940 +(let (($x122 (or (not (<= 0 ?0)) $x117)))
   3.941 +(let ((@x133 (monotonicity (rewrite (= (<= 0 ?0) $x129)) (= (not (<= 0 ?0)) $x131))))
   3.942 +(let ((@x127 (quant-intro (rewrite (= (=> (<= 0 ?0) $x117) $x122)) (= $x119 $x125))))
   3.943 +(let ((@x141 (trans @x127 (quant-intro (monotonicity @x133 (= $x122 $x134)) (= $x125 $x137)) (= $x119 $x137))))
   3.944 +(let ((@x196 (mp~ (mp (asserted $x119) @x141 $x137) (nnf-pos @x185 (~ $x137 $x137)) $x137)))
   3.945 +(let ((@x631 (mp @x196 (quant-intro @x628 (= $x137 $x626)) $x626)))
   3.946 +(let (($x269 (not $x626)))
   3.947 +(let (($x607 (or $x269 $x605 $x612)))
   3.948 +(let (($x273 (= ?x32 ?x30)))
   3.949 +(let (($x291 (>= ?x30 0)))
   3.950 +(let (($x292 (not $x291)))
   3.951 +(let (($x609 (or $x292 $x273)))
   3.952 +(let (($x271 (or $x269 $x609)))
   3.953 +(let ((@x268 (monotonicity (monotonicity (rewrite (= $x291 $x610)) (= $x292 $x605)) (rewrite (= $x273 $x612)) (= $x609 $x616))))
   3.954 +(let ((@x593 (trans (monotonicity @x268 (= $x271 (or $x269 $x616))) (rewrite (= (or $x269 $x616) $x607)) (= $x271 $x607))))
   3.955 +(let ((@x594 (mp ((_ quant-inst (+ 1 ?x29)) $x271) @x593 $x607)))
   3.956 +(let ((@x538 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x612) $x595)) (unit-resolution (unit-resolution @x594 @x631 $x616) @x545 $x612) $x595)))
   3.957 +((_ th-lemma arith farkas 1 -1 -1 1) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x559) $x557)) @x539 $x557) @x106 @x538 @x457 false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   3.958 +
   3.959 +09cc14017050c484625b3e0c3d671ae32b66851f 5 0
   3.960 +unsat
   3.961 +(
   3.962 +a0
   3.963 +a1
   3.964 +)
   3.965 +7d4feac3284b531c122b21d3a2a25c87f1e3b93b 78 0
   3.966 +unsat
   3.967 +((set-logic AUFLIA)
   3.968 +(proof
   3.969 +(let ((?x37 (* (- 1) x$)))
   3.970 +(let (($x55 (>= x$ 0)))
   3.971 +(let ((?x62 (ite $x55 x$ ?x37)))
   3.972 +(let ((?x554 (* (- 1) ?x62)))
   3.973 +(let ((?x217 (+ ?x37 ?x554)))
   3.974 +(let (($x562 (<= ?x217 0)))
   3.975 +(let (($x249 (= ?x37 ?x62)))
   3.976 +(let (($x56 (not $x55)))
   3.977 +(let (($x163 (= x$ ?x62)))
   3.978 +(let ((@x559 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x163) (<= (+ x$ ?x554) 0))) (unit-resolution (def-axiom (or $x56 $x163)) (hypothesis $x55) $x163) (<= (+ x$ ?x554) 0))))
   3.979 +(let (($x254 (>= ?x62 0)))
   3.980 +(let (($x255 (not $x254)))
   3.981 +(let (($x588 (forall ((?v0 Int) )(! (let ((?x90 (nat$ ?v0)))
   3.982 +(let ((?x91 (of_nat$ ?x90)))
   3.983 +(let (($x92 (= ?x91 ?v0)))
   3.984 +(let (($x104 (>= ?v0 0)))
   3.985 +(let (($x106 (not $x104)))
   3.986 +(or $x106 $x92)))))) :pattern ( (nat$ ?v0) ) :qid k!10))
   3.987 +))
   3.988 +(let (($x112 (forall ((?v0 Int) )(! (let ((?x90 (nat$ ?v0)))
   3.989 +(let ((?x91 (of_nat$ ?x90)))
   3.990 +(let (($x92 (= ?x91 ?v0)))
   3.991 +(let (($x104 (>= ?v0 0)))
   3.992 +(let (($x106 (not $x104)))
   3.993 +(or $x106 $x92)))))) :qid k!10))
   3.994 +))
   3.995 +(let ((?x90 (nat$ ?0)))
   3.996 +(let ((?x91 (of_nat$ ?x90)))
   3.997 +(let (($x92 (= ?x91 ?0)))
   3.998 +(let (($x104 (>= ?0 0)))
   3.999 +(let (($x106 (not $x104)))
  3.1000 +(let (($x109 (or $x106 $x92)))
  3.1001 +(let (($x94 (forall ((?v0 Int) )(! (let ((?x90 (nat$ ?v0)))
  3.1002 +(let ((?x91 (of_nat$ ?x90)))
  3.1003 +(let (($x92 (= ?x91 ?v0)))
  3.1004 +(let (($x89 (<= 0 ?v0)))
  3.1005 +(=> $x89 $x92))))) :qid k!10))
  3.1006 +))
  3.1007 +(let (($x100 (forall ((?v0 Int) )(! (let ((?x90 (nat$ ?v0)))
  3.1008 +(let ((?x91 (of_nat$ ?x90)))
  3.1009 +(let (($x92 (= ?x91 ?v0)))
  3.1010 +(or (not (<= 0 ?v0)) $x92)))) :qid k!10))
  3.1011 +))
  3.1012 +(let ((@x108 (monotonicity (rewrite (= (<= 0 ?0) $x104)) (= (not (<= 0 ?0)) $x106))))
  3.1013 +(let ((@x114 (quant-intro (monotonicity @x108 (= (or (not (<= 0 ?0)) $x92) $x109)) (= $x100 $x112))))
  3.1014 +(let ((@x99 (rewrite (= (=> (<= 0 ?0) $x92) (or (not (<= 0 ?0)) $x92)))))
  3.1015 +(let ((@x117 (mp (asserted $x94) (trans (quant-intro @x99 (= $x94 $x100)) @x114 (= $x94 $x112)) $x112)))
  3.1016 +(let ((@x593 (mp (mp~ @x117 (nnf-pos (refl (~ $x109 $x109)) (~ $x112 $x112)) $x112) (quant-intro (refl (= $x109 $x109)) (= $x112 $x588)) $x588)))
  3.1017 +(let ((?x67 (nat$ ?x62)))
  3.1018 +(let ((?x70 (of_nat$ ?x67)))
  3.1019 +(let (($x73 (= ?x70 ?x62)))
  3.1020 +(let (($x76 (not $x73)))
  3.1021 +(let (($x28 (< x$ 0)))
  3.1022 +(let ((?x30 (ite $x28 (- x$) x$)))
  3.1023 +(let (($x34 (not (= (of_nat$ (nat$ ?x30)) ?x30))))
  3.1024 +(let (($x77 (= (not (= (of_nat$ (nat$ (ite $x28 ?x37 x$))) (ite $x28 ?x37 x$))) $x76)))
  3.1025 +(let ((?x40 (ite $x28 ?x37 x$)))
  3.1026 +(let ((?x43 (nat$ ?x40)))
  3.1027 +(let ((?x46 (of_nat$ ?x43)))
  3.1028 +(let (($x49 (= ?x46 ?x40)))
  3.1029 +(let ((@x66 (trans (monotonicity (rewrite (= $x28 $x56)) (= ?x40 (ite $x56 ?x37 x$))) (rewrite (= (ite $x56 ?x37 x$) ?x62)) (= ?x40 ?x62))))
  3.1030 +(let ((@x75 (monotonicity (monotonicity (monotonicity @x66 (= ?x43 ?x67)) (= ?x46 ?x70)) @x66 (= $x49 $x73))))
  3.1031 +(let ((@x45 (monotonicity (monotonicity (rewrite (= (- x$) ?x37)) (= ?x30 ?x40)) (= (nat$ ?x30) ?x43))))
  3.1032 +(let ((@x51 (monotonicity (monotonicity @x45 (= (of_nat$ (nat$ ?x30)) ?x46)) (monotonicity (rewrite (= (- x$) ?x37)) (= ?x30 ?x40)) (= (= (of_nat$ (nat$ ?x30)) ?x30) $x49))))
  3.1033 +(let ((@x80 (trans (monotonicity @x51 (= $x34 (not $x49))) (monotonicity @x75 $x77) (= $x34 $x76))))
  3.1034 +(let ((@x81 (mp (asserted $x34) @x80 $x76)))
  3.1035 +(let (($x239 (or (not $x588) $x255 $x73)))
  3.1036 +(let ((@x576 (mp ((_ quant-inst (ite $x55 x$ ?x37)) (or (not $x588) (or $x255 $x73))) (rewrite (= (or (not $x588) (or $x255 $x73)) $x239)) $x239)))
  3.1037 +(let ((@x561 ((_ th-lemma arith farkas -1 1 1) (hypothesis $x55) (unit-resolution @x576 @x81 @x593 $x255) @x559 false)))
  3.1038 +(let ((@x198 (lemma @x561 $x56)))
  3.1039 +(let ((@x566 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x249) $x562)) (unit-resolution (def-axiom (or $x55 $x249)) @x198 $x249) $x562)))
  3.1040 +(let (($x578 (<= ?x62 0)))
  3.1041 +(let ((@x257 (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x578 $x254)) (unit-resolution @x576 @x81 @x593 $x255) $x578)))
  3.1042 +((_ th-lemma arith farkas 1 1 1) @x257 @x198 @x566 false)))))))))))))))))))))))))))))))))))))))))))))))))))))))
  3.1043 +
  3.1044 +74a1c0d44cbd0147017229e79a08e8dfcfe4eee2 7 0
  3.1045 +unsat
  3.1046 +(
  3.1047 +a2
  3.1048 +a189
  3.1049 +a138
  3.1050 +a7
  3.1051 +)
  3.1052 +1a98e6860e90be637d16c2d7127e7141065068af 5 0
  3.1053 +unsat
  3.1054 +(
  3.1055 +a0
  3.1056 +a1
  3.1057 +)
  3.1058 +14f8ad1280ad869e9c8ef4e6a613ceb808bfd5ab 7 0
  3.1059 +unsat
  3.1060 +(
  3.1061 +a0
  3.1062 +a1
  3.1063 +a2
  3.1064 +a4
  3.1065 +)
  3.1066 +15ec6864dfa5b932b5e4bed685e55140b1a81105 6 0
  3.1067 +unsat
  3.1068 +(
  3.1069 +a0
  3.1070 +a1
  3.1071 +a3
  3.1072 +)
  3.1073 +ce85402875b83dc2f06a381810d29a2061933b9f 312 0
  3.1074 +unsat
  3.1075 +((set-logic AUFLIA)
  3.1076 +(declare-fun ?v1!0 (Nat$) Nat$)
  3.1077 +(proof
  3.1078 +(let ((?x89 (of_nat$ m$)))
  3.1079 +(let ((?x90 (* 4 ?x89)))
  3.1080 +(let ((?x98 (+ 1 ?x90)))
  3.1081 +(let ((?x101 (nat$ ?x98)))
  3.1082 +(let ((?x295 (of_nat$ ?x101)))
  3.1083 +(let ((?x598 (* (- 1) ?x295)))
  3.1084 +(let ((?x599 (+ ?x90 ?x598)))
  3.1085 +(let (($x574 (>= ?x599 (- 1))))
  3.1086 +(let (($x597 (= ?x599 (- 1))))
  3.1087 +(let (($x610 (>= ?x89 0)))
  3.1088 +(let (($x380 (<= ?x295 1)))
  3.1089 +(let (($x687 (not $x380)))
  3.1090 +(let (($x701 (forall ((?v1 Nat$) )(! (let ((?x89 (of_nat$ m$)))
  3.1091 +(let ((?x90 (* 4 ?x89)))
  3.1092 +(let ((?x98 (+ 1 ?x90)))
  3.1093 +(let ((?x101 (nat$ ?x98)))
  3.1094 +(let (($x382 (= ?v1 ?x101)))
  3.1095 +(let ((?x34 (nat$ 1)))
  3.1096 +(let (($x35 (= ?v1 ?x34)))
  3.1097 +(let (($x381 (dvd$ ?v1 ?x101)))
  3.1098 +(let (($x371 (not $x381)))
  3.1099 +(or $x371 $x35 $x382)))))))))) :pattern ( (dvd$ ?v1 (nat$ (+ 1 (* 4 (of_nat$ m$))))) ) :qid k!10))
  3.1100 +))
  3.1101 +(let (($x702 (not $x701)))
  3.1102 +(let (($x357 (or $x380 $x702)))
  3.1103 +(let (($x487 (not $x357)))
  3.1104 +(let (($x104 (prime_nat$ ?x101)))
  3.1105 +(let (($x110 (not $x104)))
  3.1106 +(let (($x697 (or $x110 $x487)))
  3.1107 +(let ((?x703 (?v1!0 ?x101)))
  3.1108 +(let (($x707 (= ?x703 ?x101)))
  3.1109 +(let ((?x34 (nat$ 1)))
  3.1110 +(let (($x706 (= ?x703 ?x34)))
  3.1111 +(let (($x704 (dvd$ ?x703 ?x101)))
  3.1112 +(let (($x705 (not $x704)))
  3.1113 +(let (($x708 (or $x705 $x706 $x707)))
  3.1114 +(let (($x698 (not $x708)))
  3.1115 +(let (($x360 (or $x104 $x380 $x698)))
  3.1116 +(let (($x700 (not $x360)))
  3.1117 +(let (($x369 (not $x697)))
  3.1118 +(let (($x342 (or $x369 $x700)))
  3.1119 +(let (($x684 (not $x342)))
  3.1120 +(let (($x738 (forall ((?v0 Nat$) )(! (let (($x219 (or (not (dvd$ (?v1!0 ?v0) ?v0)) (= (?v1!0 ?v0) (nat$ 1)) (= (?v1!0 ?v0) ?v0))))
  3.1121 +(let (($x220 (not $x219)))
  3.1122 +(let ((?x30 (of_nat$ ?v0)))
  3.1123 +(let (($x65 (<= ?x30 1)))
  3.1124 +(let (($x28 (prime_nat$ ?v0)))
  3.1125 +(let (($x245 (or $x28 $x65 $x220)))
  3.1126 +(let (($x710 (forall ((?v1 Nat$) )(! (let ((?x34 (nat$ 1)))
  3.1127 +(let (($x35 (= ?v1 ?x34)))
  3.1128 +(or (not (dvd$ ?v1 ?v0)) $x35 (= ?v1 ?v0)))) :pattern ( (dvd$ ?v1 ?v0) ) :qid k!10))
  3.1129 +))
  3.1130 +(let (($x200 (not $x28)))
  3.1131 +(not (or (not (or $x200 (not (or $x65 (not $x710))))) (not $x245))))))))))) :pattern ( (prime_nat$ ?v0) ) :pattern ( (of_nat$ ?v0) ) :qid k!10))
  3.1132 +))
  3.1133 +(let (($x290 (forall ((?v0 Nat$) )(! (let (($x219 (or (not (dvd$ (?v1!0 ?v0) ?v0)) (= (?v1!0 ?v0) (nat$ 1)) (= (?v1!0 ?v0) ?v0))))
  3.1134 +(let (($x220 (not $x219)))
  3.1135 +(let ((?x30 (of_nat$ ?v0)))
  3.1136 +(let (($x65 (<= ?x30 1)))
  3.1137 +(let (($x28 (prime_nat$ ?v0)))
  3.1138 +(let (($x245 (or $x28 $x65 $x220)))
  3.1139 +(let (($x72 (forall ((?v1 Nat$) )(! (let ((?x34 (nat$ 1)))
  3.1140 +(let (($x35 (= ?v1 ?x34)))
  3.1141 +(or (not (dvd$ ?v1 ?v0)) $x35 (= ?v1 ?v0)))) :qid k!10))
  3.1142 +))
  3.1143 +(let (($x221 (not $x72)))
  3.1144 +(let (($x273 (not (or $x65 $x221))))
  3.1145 +(let (($x200 (not $x28)))
  3.1146 +(let (($x276 (or $x200 $x273)))
  3.1147 +(not (or (not $x276) (not $x245)))))))))))))) :qid k!10))
  3.1148 +))
  3.1149 +(let (($x219 (or (not (dvd$ (?v1!0 ?0) ?0)) (= (?v1!0 ?0) ?x34) (= (?v1!0 ?0) ?0))))
  3.1150 +(let (($x220 (not $x219)))
  3.1151 +(let ((?x30 (of_nat$ ?0)))
  3.1152 +(let (($x65 (<= ?x30 1)))
  3.1153 +(let (($x28 (prime_nat$ ?0)))
  3.1154 +(let (($x245 (or $x28 $x65 $x220)))
  3.1155 +(let (($x710 (forall ((?v1 Nat$) )(! (let ((?x34 (nat$ 1)))
  3.1156 +(let (($x35 (= ?v1 ?x34)))
  3.1157 +(or (not (dvd$ ?v1 ?0)) $x35 (= ?v1 ?0)))) :pattern ( (dvd$ ?v1 ?0) ) :qid k!10))
  3.1158 +))
  3.1159 +(let (($x200 (not $x28)))
  3.1160 +(let (($x72 (forall ((?v1 Nat$) )(! (let ((?x34 (nat$ 1)))
  3.1161 +(let (($x35 (= ?v1 ?x34)))
  3.1162 +(or (not (dvd$ ?v1 ?0)) $x35 (= ?v1 ?0)))) :qid k!10))
  3.1163 +))
  3.1164 +(let (($x221 (not $x72)))
  3.1165 +(let (($x273 (not (or $x65 $x221))))
  3.1166 +(let (($x276 (or $x200 $x273)))
  3.1167 +(let (($x285 (not (or (not $x276) (not $x245)))))
  3.1168 +(let (($x734 (= $x285 (not (or (not (or $x200 (not (or $x65 (not $x710))))) (not $x245))))))
  3.1169 +(let (($x731 (= (or (not $x276) (not $x245)) (or (not (or $x200 (not (or $x65 (not $x710))))) (not $x245)))))
  3.1170 +(let (($x35 (= ?0 ?x34)))
  3.1171 +(let (($x69 (or (not (dvd$ ?0 ?1)) $x35 (= ?0 ?1))))
  3.1172 +(let ((@x717 (monotonicity (quant-intro (refl (= $x69 $x69)) (= $x72 $x710)) (= $x221 (not $x710)))))
  3.1173 +(let ((@x723 (monotonicity (monotonicity @x717 (= (or $x65 $x221) (or $x65 (not $x710)))) (= $x273 (not (or $x65 (not $x710)))))))
  3.1174 +(let ((@x729 (monotonicity (monotonicity @x723 (= $x276 (or $x200 (not (or $x65 (not $x710)))))) (= (not $x276) (not (or $x200 (not (or $x65 (not $x710)))))))))
  3.1175 +(let ((@x740 (quant-intro (monotonicity (monotonicity @x729 $x731) $x734) (= $x290 $x738))))
  3.1176 +(let (($x253 (forall ((?v0 Nat$) )(! (let (($x219 (or (not (dvd$ (?v1!0 ?v0) ?v0)) (= (?v1!0 ?v0) (nat$ 1)) (= (?v1!0 ?v0) ?v0))))
  3.1177 +(let (($x220 (not $x219)))
  3.1178 +(let ((?x30 (of_nat$ ?v0)))
  3.1179 +(let (($x65 (<= ?x30 1)))
  3.1180 +(let (($x28 (prime_nat$ ?v0)))
  3.1181 +(let (($x245 (or $x28 $x65 $x220)))
  3.1182 +(let (($x72 (forall ((?v1 Nat$) )(! (let ((?x34 (nat$ 1)))
  3.1183 +(let (($x35 (= ?v1 ?x34)))
  3.1184 +(or (not (dvd$ ?v1 ?v0)) $x35 (= ?v1 ?v0)))) :qid k!10))
  3.1185 +))
  3.1186 +(let (($x66 (not $x65)))
  3.1187 +(let (($x75 (and $x66 $x72)))
  3.1188 +(let (($x200 (not $x28)))
  3.1189 +(let (($x229 (or $x200 $x75)))
  3.1190 +(and $x229 $x245)))))))))))) :qid k!10))
  3.1191 +))
  3.1192 +(let ((@x278 (monotonicity (rewrite (= (and (not $x65) $x72) $x273)) (= (or $x200 (and (not $x65) $x72)) $x276))))
  3.1193 +(let ((@x281 (monotonicity @x278 (= (and (or $x200 (and (not $x65) $x72)) $x245) (and $x276 $x245)))))
  3.1194 +(let ((@x289 (trans @x281 (rewrite (= (and $x276 $x245) $x285)) (= (and (or $x200 (and (not $x65) $x72)) $x245) $x285))))
  3.1195 +(let (($x233 (forall ((?v0 Nat$) )(! (let (($x219 (or (not (dvd$ (?v1!0 ?v0) ?v0)) (= (?v1!0 ?v0) (nat$ 1)) (= (?v1!0 ?v0) ?v0))))
  3.1196 +(let (($x220 (not $x219)))
  3.1197 +(let ((?x30 (of_nat$ ?v0)))
  3.1198 +(let (($x65 (<= ?x30 1)))
  3.1199 +(let (($x66 (not $x65)))
  3.1200 +(let (($x211 (not $x66)))
  3.1201 +(let (($x224 (or $x211 $x220)))
  3.1202 +(let (($x28 (prime_nat$ ?v0)))
  3.1203 +(let (($x228 (or $x28 $x224)))
  3.1204 +(let (($x72 (forall ((?v1 Nat$) )(! (let ((?x34 (nat$ 1)))
  3.1205 +(let (($x35 (= ?v1 ?x34)))
  3.1206 +(or (not (dvd$ ?v1 ?v0)) $x35 (= ?v1 ?v0)))) :qid k!10))
  3.1207 +))
  3.1208 +(let (($x75 (and $x66 $x72)))
  3.1209 +(let (($x200 (not $x28)))
  3.1210 +(let (($x229 (or $x200 $x75)))
  3.1211 +(and $x229 $x228)))))))))))))) :qid k!10))
  3.1212 +))
  3.1213 +(let (($x66 (not $x65)))
  3.1214 +(let (($x75 (and $x66 $x72)))
  3.1215 +(let (($x229 (or $x200 $x75)))
  3.1216 +(let (($x250 (and $x229 $x245)))
  3.1217 +(let (($x211 (not $x66)))
  3.1218 +(let (($x224 (or $x211 $x220)))
  3.1219 +(let (($x228 (or $x28 $x224)))
  3.1220 +(let (($x230 (and $x229 $x228)))
  3.1221 +(let ((@x244 (monotonicity (monotonicity (rewrite (= $x211 $x65)) (= $x224 (or $x65 $x220))) (= $x228 (or $x28 (or $x65 $x220))))))
  3.1222 +(let ((@x249 (trans @x244 (rewrite (= (or $x28 (or $x65 $x220)) $x245)) (= $x228 $x245))))
  3.1223 +(let (($x81 (forall ((?v0 Nat$) )(! (let (($x72 (forall ((?v1 Nat$) )(! (let ((?x34 (nat$ 1)))
  3.1224 +(let (($x35 (= ?v1 ?x34)))
  3.1225 +(or (not (dvd$ ?v1 ?v0)) $x35 (= ?v1 ?v0)))) :qid k!10))
  3.1226 +))
  3.1227 +(let ((?x30 (of_nat$ ?v0)))
  3.1228 +(let (($x65 (<= ?x30 1)))
  3.1229 +(let (($x66 (not $x65)))
  3.1230 +(let (($x75 (and $x66 $x72)))
  3.1231 +(let (($x28 (prime_nat$ ?v0)))
  3.1232 +(= $x28 $x75))))))) :qid k!10))
  3.1233 +))
  3.1234 +(let ((@x227 (nnf-neg (refl (~ $x211 $x211)) (sk (~ $x221 $x220)) (~ (not $x75) $x224))))
  3.1235 +(let ((@x210 (monotonicity (refl (~ $x66 $x66)) (nnf-pos (refl (~ $x69 $x69)) (~ $x72 $x72)) (~ $x75 $x75))))
  3.1236 +(let ((@x232 (nnf-pos (refl (~ $x28 $x28)) (refl (~ $x200 $x200)) @x210 @x227 (~ (= $x28 $x75) $x230))))
  3.1237 +(let (($x42 (forall ((?v0 Nat$) )(! (let (($x39 (forall ((?v1 Nat$) )(! (let (($x33 (dvd$ ?v1 ?v0)))
  3.1238 +(=> $x33 (or (= ?v1 (nat$ 1)) (= ?v1 ?v0)))) :qid k!10))
  3.1239 +))
  3.1240 +(let ((?x30 (of_nat$ ?v0)))
  3.1241 +(let (($x31 (< 1 ?x30)))
  3.1242 +(let (($x28 (prime_nat$ ?v0)))
  3.1243 +(= $x28 (and $x31 $x39)))))) :qid k!10))
  3.1244 +))
  3.1245 +(let (($x62 (forall ((?v0 Nat$) )(! (let (($x48 (forall ((?v1 Nat$) )(! (or (not (dvd$ ?v1 ?v0)) (or (= ?v1 (nat$ 1)) (= ?v1 ?v0))) :qid k!10))
  3.1246 +))
  3.1247 +(let ((?x30 (of_nat$ ?v0)))
  3.1248 +(let (($x31 (< 1 ?x30)))
  3.1249 +(let (($x51 (and $x31 $x48)))
  3.1250 +(let (($x28 (prime_nat$ ?v0)))
  3.1251 +(= $x28 $x51)))))) :qid k!10))
  3.1252 +))
  3.1253 +(let (($x78 (= $x28 $x75)))
  3.1254 +(let (($x48 (forall ((?v1 Nat$) )(! (or (not (dvd$ ?v1 ?0)) (or (= ?v1 (nat$ 1)) (= ?v1 ?0))) :qid k!10))
  3.1255 +))
  3.1256 +(let (($x31 (< 1 ?x30)))
  3.1257 +(let (($x51 (and $x31 $x48)))
  3.1258 +(let (($x57 (= $x28 $x51)))
  3.1259 +(let ((@x71 (rewrite (= (or (not (dvd$ ?0 ?1)) (or $x35 (= ?0 ?1))) $x69))))
  3.1260 +(let ((@x77 (monotonicity (rewrite (= $x31 $x66)) (quant-intro @x71 (= $x48 $x72)) (= $x51 $x75))))
  3.1261 +(let (($x39 (forall ((?v1 Nat$) )(! (let (($x33 (dvd$ ?v1 ?0)))
  3.1262 +(=> $x33 (or (= ?v1 (nat$ 1)) (= ?v1 ?0)))) :qid k!10))
  3.1263 +))
  3.1264 +(let (($x41 (= $x28 (and $x31 $x39))))
  3.1265 +(let (($x45 (or (not (dvd$ ?0 ?1)) (or $x35 (= ?0 ?1)))))
  3.1266 +(let ((@x50 (quant-intro (rewrite (= (=> (dvd$ ?0 ?1) (or $x35 (= ?0 ?1))) $x45)) (= $x39 $x48))))
  3.1267 +(let ((@x56 (monotonicity (monotonicity @x50 (= (and $x31 $x39) $x51)) (= $x41 (= $x28 $x51)))))
  3.1268 +(let ((@x64 (quant-intro (trans @x56 (rewrite (= (= $x28 $x51) $x57)) (= $x41 $x57)) (= $x42 $x62))))
  3.1269 +(let ((@x85 (trans @x64 (quant-intro (monotonicity @x77 (= $x57 $x78)) (= $x62 $x81)) (= $x42 $x81))))
  3.1270 +(let ((@x236 (mp~ (mp (asserted $x42) @x85 $x81) (nnf-pos @x232 (~ $x81 $x233)) $x233)))
  3.1271 +(let ((@x256 (mp @x236 (quant-intro (monotonicity @x249 (= $x230 $x250)) (= $x233 $x253)) $x253)))
  3.1272 +(let ((@x741 (mp (mp @x256 (quant-intro @x289 (= $x253 $x290)) $x290) @x740 $x738)))
  3.1273 +(let (($x348 (or (not $x738) $x684)))
  3.1274 +(let ((@x685 ((_ quant-inst (nat$ ?x98)) $x348)))
  3.1275 +(let ((@x569 (unit-resolution (def-axiom (or $x342 $x697)) (unit-resolution @x685 @x741 $x684) $x697)))
  3.1276 +(let (($x125 (not (or $x110 (>= ?x89 1)))))
  3.1277 +(let (($x94 (<= 1 ?x89)))
  3.1278 +(let (($x95 (=> (prime_nat$ (nat$ (+ ?x90 1))) $x94)))
  3.1279 +(let (($x96 (not $x95)))
  3.1280 +(let ((@x124 (monotonicity (rewrite (= $x94 (>= ?x89 1))) (= (or $x110 $x94) (or $x110 (>= ?x89 1))))))
  3.1281 +(let ((@x103 (monotonicity (rewrite (= (+ ?x90 1) ?x98)) (= (nat$ (+ ?x90 1)) ?x101))))
  3.1282 +(let ((@x109 (monotonicity (monotonicity @x103 (= (prime_nat$ (nat$ (+ ?x90 1))) $x104)) (= $x95 (=> $x104 $x94)))))
  3.1283 +(let ((@x115 (trans @x109 (rewrite (= (=> $x104 $x94) (or $x110 $x94))) (= $x95 (or $x110 $x94)))))
  3.1284 +(let ((@x129 (trans (monotonicity @x115 (= $x96 (not (or $x110 $x94)))) (monotonicity @x124 (= (not (or $x110 $x94)) $x125)) (= $x96 $x125))))
  3.1285 +(let ((@x131 (not-or-elim (mp (asserted $x96) @x129 $x125) $x104)))
  3.1286 +(let ((@x572 (unit-resolution (unit-resolution (def-axiom (or $x369 $x110 $x487)) @x131 (or $x369 $x487)) @x569 $x487)))
  3.1287 +(let ((@x530 (unit-resolution ((_ th-lemma arith farkas 1 1) (or (not (<= ?x295 0)) $x380)) (unit-resolution (def-axiom (or $x357 $x687)) @x572 $x687) (not (<= ?x295 0)))))
  3.1288 +(let ((@x561 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= ?x295 0)) (<= ?x295 0))) @x530 (not (= ?x295 0)))))
  3.1289 +(let (($x575 (= ?x295 0)))
  3.1290 +(let (($x577 (or $x610 $x575)))
  3.1291 +(let (($x756 (forall ((?v0 Int) )(! (let ((?x140 (nat$ ?v0)))
  3.1292 +(let ((?x141 (of_nat$ ?x140)))
  3.1293 +(let (($x169 (= ?x141 0)))
  3.1294 +(let (($x155 (>= ?v0 0)))
  3.1295 +(or $x155 $x169))))) :pattern ( (nat$ ?v0) ) :qid k!14))
  3.1296 +))
  3.1297 +(let (($x192 (forall ((?v0 Int) )(! (let ((?x140 (nat$ ?v0)))
  3.1298 +(let ((?x141 (of_nat$ ?x140)))
  3.1299 +(let (($x169 (= ?x141 0)))
  3.1300 +(let (($x155 (>= ?v0 0)))
  3.1301 +(or $x155 $x169))))) :qid k!14))
  3.1302 +))
  3.1303 +(let ((?x140 (nat$ ?0)))
  3.1304 +(let ((?x141 (of_nat$ ?x140)))
  3.1305 +(let (($x169 (= ?x141 0)))
  3.1306 +(let (($x155 (>= ?0 0)))
  3.1307 +(let (($x189 (or $x155 $x169)))
  3.1308 +(let (($x171 (forall ((?v0 Int) )(! (let ((?x140 (nat$ ?v0)))
  3.1309 +(let ((?x141 (of_nat$ ?x140)))
  3.1310 +(let (($x169 (= ?x141 0)))
  3.1311 +(let (($x168 (< ?v0 0)))
  3.1312 +(=> $x168 $x169))))) :qid k!14))
  3.1313 +))
  3.1314 +(let (($x177 (forall ((?v0 Int) )(! (let ((?x140 (nat$ ?v0)))
  3.1315 +(let ((?x141 (of_nat$ ?x140)))
  3.1316 +(let (($x169 (= ?x141 0)))
  3.1317 +(let (($x168 (< ?v0 0)))
  3.1318 +(let (($x173 (not $x168)))
  3.1319 +(or $x173 $x169)))))) :qid k!14))
  3.1320 +))
  3.1321 +(let ((@x184 (monotonicity (rewrite (= (< ?0 0) (not $x155))) (= (not (< ?0 0)) (not (not $x155))))))
  3.1322 +(let ((@x188 (trans @x184 (rewrite (= (not (not $x155)) $x155)) (= (not (< ?0 0)) $x155))))
  3.1323 +(let ((@x194 (quant-intro (monotonicity @x188 (= (or (not (< ?0 0)) $x169) $x189)) (= $x177 $x192))))
  3.1324 +(let ((@x176 (rewrite (= (=> (< ?0 0) $x169) (or (not (< ?0 0)) $x169)))))
  3.1325 +(let ((@x197 (mp (asserted $x171) (trans (quant-intro @x176 (= $x171 $x177)) @x194 (= $x171 $x192)) $x192)))
  3.1326 +(let ((@x761 (mp (mp~ @x197 (nnf-pos (refl (~ $x189 $x189)) (~ $x192 $x192)) $x192) (quant-intro (refl (= $x189 $x189)) (= $x192 $x756)) $x756)))
  3.1327 +(let (($x580 (not $x756)))
  3.1328 +(let (($x581 (or $x580 $x610 $x575)))
  3.1329 +(let ((@x612 (rewrite (= (>= ?x98 0) $x610))))
  3.1330 +(let ((@x579 (monotonicity @x612 (= (or (>= ?x98 0) $x575) $x577))))
  3.1331 +(let ((@x555 (monotonicity @x579 (= (or $x580 (or (>= ?x98 0) $x575)) (or $x580 $x577)))))
  3.1332 +(let ((@x564 (trans @x555 (rewrite (= (or $x580 $x577) $x581)) (= (or $x580 (or (>= ?x98 0) $x575)) $x581))))
  3.1333 +(let ((@x565 (mp ((_ quant-inst (+ 1 ?x90)) (or $x580 (or (>= ?x98 0) $x575))) @x564 $x581)))
  3.1334 +(let (($x613 (not $x610)))
  3.1335 +(let (($x600 (or $x613 $x597)))
  3.1336 +(let (($x750 (forall ((?v0 Int) )(! (let ((?x140 (nat$ ?v0)))
  3.1337 +(let ((?x141 (of_nat$ ?x140)))
  3.1338 +(let (($x142 (= ?x141 ?v0)))
  3.1339 +(let (($x155 (>= ?v0 0)))
  3.1340 +(let (($x156 (not $x155)))
  3.1341 +(or $x156 $x142)))))) :pattern ( (nat$ ?v0) ) :qid k!13))
  3.1342 +))
  3.1343 +(let (($x162 (forall ((?v0 Int) )(! (let ((?x140 (nat$ ?v0)))
  3.1344 +(let ((?x141 (of_nat$ ?x140)))
  3.1345 +(let (($x142 (= ?x141 ?v0)))
  3.1346 +(let (($x155 (>= ?v0 0)))
  3.1347 +(let (($x156 (not $x155)))
  3.1348 +(or $x156 $x142)))))) :qid k!13))
  3.1349 +))
  3.1350 +(let ((@x752 (refl (= (or (not $x155) (= ?x141 ?0)) (or (not $x155) (= ?x141 ?0))))))
  3.1351 +(let ((@x263 (refl (~ (or (not $x155) (= ?x141 ?0)) (or (not $x155) (= ?x141 ?0))))))
  3.1352 +(let (($x144 (forall ((?v0 Int) )(! (let ((?x140 (nat$ ?v0)))
  3.1353 +(let ((?x141 (of_nat$ ?x140)))
  3.1354 +(let (($x142 (= ?x141 ?v0)))
  3.1355 +(let (($x139 (<= 0 ?v0)))
  3.1356 +(=> $x139 $x142))))) :qid k!13))
  3.1357 +))
  3.1358 +(let (($x150 (forall ((?v0 Int) )(! (let ((?x140 (nat$ ?v0)))
  3.1359 +(let ((?x141 (of_nat$ ?x140)))
  3.1360 +(let (($x142 (= ?x141 ?v0)))
  3.1361 +(or (not (<= 0 ?v0)) $x142)))) :qid k!13))
  3.1362 +))
  3.1363 +(let (($x142 (= ?x141 ?0)))
  3.1364 +(let (($x156 (not $x155)))
  3.1365 +(let (($x159 (or $x156 $x142)))
  3.1366 +(let (($x147 (or (not (<= 0 ?0)) $x142)))
  3.1367 +(let ((@x158 (monotonicity (rewrite (= (<= 0 ?0) $x155)) (= (not (<= 0 ?0)) $x156))))
  3.1368 +(let ((@x152 (quant-intro (rewrite (= (=> (<= 0 ?0) $x142) $x147)) (= $x144 $x150))))
  3.1369 +(let ((@x166 (trans @x152 (quant-intro (monotonicity @x158 (= $x147 $x159)) (= $x150 $x162)) (= $x144 $x162))))
  3.1370 +(let ((@x266 (mp~ (mp (asserted $x144) @x166 $x162) (nnf-pos @x263 (~ $x162 $x162)) $x162)))
  3.1371 +(let ((@x755 (mp @x266 (quant-intro @x752 (= $x162 $x750)) $x750)))
  3.1372 +(let (($x603 (not $x750)))
  3.1373 +(let (($x604 (or $x603 $x613 $x597)))
  3.1374 +(let (($x608 (= ?x295 ?x98)))
  3.1375 +(let (($x618 (>= ?x98 0)))
  3.1376 +(let (($x619 (not $x618)))
  3.1377 +(let (($x609 (or $x619 $x608)))
  3.1378 +(let (($x605 (or $x603 $x609)))
  3.1379 +(let ((@x602 (monotonicity (monotonicity @x612 (= $x619 $x613)) (rewrite (= $x608 $x597)) (= $x609 $x600))))
  3.1380 +(let ((@x590 (trans (monotonicity @x602 (= $x605 (or $x603 $x600))) (rewrite (= (or $x603 $x600) $x604)) (= $x605 $x604))))
  3.1381 +(let ((@x591 (mp ((_ quant-inst (+ 1 ?x90)) $x605) @x590 $x604)))
  3.1382 +(let ((@x532 (unit-resolution (unit-resolution @x591 @x755 $x600) (unit-resolution (unit-resolution @x565 @x761 $x577) @x561 $x610) $x597)))
  3.1383 +(let ((@x133 (not-or-elim (mp (asserted $x96) @x129 $x125) (not (>= ?x89 1)))))
  3.1384 +((_ th-lemma arith farkas -4 1 1) @x133 (unit-resolution (def-axiom (or $x357 $x687)) @x572 $x687) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x597) $x574)) @x532 $x574) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  3.1385 +
  3.1386 +9e3a7cb6b1687db90ac27c1322f4180e0715e89a 7 0
  3.1387 +unsat
  3.1388 +(
  3.1389 +a1
  3.1390 +a169
  3.1391 +a170
  3.1392 +a94
  3.1393 +)
  3.1394 +0f29eff8af0baceae4a69ea0ceff00e3a8c44aaf 7 0
  3.1395 +unsat
  3.1396 +(
  3.1397 +a0
  3.1398 +a1
  3.1399 +a3
  3.1400 +a4
  3.1401 +)
  3.1402 +2f309a4750090c04f284fbecb4a976eedaa46ce9 7 0
  3.1403 +unsat
  3.1404 +(
  3.1405 +a95
  3.1406 +a173
  3.1407 +a5
  3.1408 +a179
  3.1409 +)
  3.1410 +e0764188710d396d7c3d8c7ed12e92df610f3d5d 6 0
  3.1411 +unsat
  3.1412 +(
  3.1413 +a0
  3.1414 +a2
  3.1415 +a3
  3.1416 +)
  3.1417 +ff18566d8fd433a50da07b998b8d9915d4e6d38c 7 0
  3.1418 +unsat
  3.1419 +(
  3.1420 +a0
  3.1421 +a1
  3.1422 +a2
  3.1423 +a3
  3.1424 +)
  3.1425 +85b5e78e459667d6880efd720fc8258c1f632634 5 0
  3.1426 +unsat
  3.1427 +(
  3.1428 +a0
  3.1429 +a2
  3.1430 +)
  3.1431 +d9da06f46916827de91e55898f12e162fc4394a9 5 0
  3.1432 +unsat
  3.1433 +(
  3.1434 +a0
  3.1435 +a2
  3.1436 +)
  3.1437 +0c5b279548a729dbbc42ad3281942c493cea61a9 2 0
  3.1438 +unknown
  3.1439 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
  3.1440 +f38355a9ae0344ba7fe2a48aa18389448f4b9cd2 2 0
  3.1441 +unknown
  3.1442 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
  3.1443 +bbdbbe6715d50b1bf20ff06d778334d19ea80167 5 0
  3.1444 +unsat
  3.1445 +(
  3.1446 +a0
  3.1447 +a1
  3.1448 +)
  3.1449 +933c14ef800372ac93564be5a3ef60dc447e5229 5 0
  3.1450 +unsat
  3.1451 +(
  3.1452 +a2
  3.1453 +a3
  3.1454 +)
  3.1455 +b2b6ec8367faf6099e2eb37a31144e974fe80a4d 5 0
  3.1456 +unsat
  3.1457 +(
  3.1458 +a0
  3.1459 +a1
  3.1460 +)
  3.1461 +7d3ccc6fd748dc986de65f6b96355c1acc61633a 5 0
  3.1462 +unsat
  3.1463 +(
  3.1464 +a0
  3.1465 +a1
  3.1466 +)
  3.1467 +502c6566fddc9f002ef331f2822f70acfc1eb0a6 2 0
  3.1468 +sat
  3.1469 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
  3.1470 +9a7dd691b0176ee4885324369fa4400bb78fa856 2 0
  3.1471 +sat
  3.1472 +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
  3.1473 +5dee863399bac5f53042e3459e153dff890dd2a5 4 0
  3.1474 +unsat
  3.1475 +(
  3.1476 +a0
  3.1477 +)
     4.1 --- a/src/HOL/SMT_Examples/SMT_Examples.thy	Thu Jul 27 15:22:35 2017 +0100
     4.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Fri Jul 28 15:36:32 2017 +0100
     4.3 @@ -378,6 +378,32 @@
     4.4    using assms by (metis mult_le_0_iff)
     4.5  
     4.6  
     4.7 +subsection {* Linear arithmetic for natural numbers *}
     4.8 +
     4.9 +declare [[smt_nat_as_int]]
    4.10 +
    4.11 +lemma "2 * (x::nat) \<noteq> 1" by smt
    4.12 +
    4.13 +lemma "a < 3 \<Longrightarrow> (7::nat) > 2 * a" by smt
    4.14 +
    4.15 +lemma "let x = (1::nat) + y in x - y > 0 * x" by smt
    4.16 +
    4.17 +lemma
    4.18 +  "let x = (1::nat) + y in
    4.19 +   let P = (if x > 0 then True else False) in
    4.20 +   False \<or> P = (x - 1 = y) \<or> (\<not>P \<longrightarrow> False)"
    4.21 +  by smt
    4.22 +
    4.23 +lemma "int (nat \<bar>x::int\<bar>) = \<bar>x\<bar>" by smt
    4.24 +
    4.25 +definition prime_nat :: "nat \<Rightarrow> bool" where
    4.26 +  "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    4.27 +
    4.28 +lemma "prime_nat (4*m + 1) \<Longrightarrow> m \<ge> (1::nat)" by (smt prime_nat_def)
    4.29 +
    4.30 +declare [[smt_nat_as_int = false]]
    4.31 +
    4.32 +
    4.33  section \<open>Pairs\<close>
    4.34  
    4.35  lemma "fst (x, y) = a \<Longrightarrow> x = a"
     5.1 --- a/src/HOL/SMT_Examples/SMT_Tests.thy	Thu Jul 27 15:22:35 2017 +0100
     5.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Fri Jul 28 15:36:32 2017 +0100
     5.3 @@ -222,6 +222,123 @@
     5.4    by smt+
     5.5  
     5.6  
     5.7 +section {* Natural numbers *}
     5.8 +
     5.9 +declare [[smt_nat_as_int]]
    5.10 +
    5.11 +lemma
    5.12 +  "(0::nat) = 0"
    5.13 +  "(1::nat) = 1"
    5.14 +  "(0::nat) < 1"
    5.15 +  "(0::nat) \<le> 1"
    5.16 +  "(123456789::nat) < 2345678901"
    5.17 +  by smt+
    5.18 +
    5.19 +lemma
    5.20 +  "Suc 0 = 1"
    5.21 +  "Suc x = x + 1"
    5.22 +  "x < Suc x"
    5.23 +  "(Suc x = Suc y) = (x = y)"
    5.24 +  "Suc (x + y) < Suc x + Suc y"
    5.25 +  by smt+
    5.26 +
    5.27 +lemma
    5.28 +  "(x::nat) + 0 = x"
    5.29 +  "0 + x = x"
    5.30 +  "x + y = y + x"
    5.31 +  "x + (y + z) = (x + y) + z"
    5.32 +  "(x + y = 0) = (x = 0 \<and> y = 0)"
    5.33 +  by smt+
    5.34 +
    5.35 +lemma
    5.36 +  "(x::nat) - 0 = x"
    5.37 +  "x < y \<longrightarrow> x - y = 0"
    5.38 +  "x - y = 0 \<or> y - x = 0"
    5.39 +  "(x - y) + y = (if x < y then y else x)"
    5.40 +  "x - y - z = x - (y + z)"
    5.41 +  by smt+
    5.42 +
    5.43 +lemma
    5.44 +  "(x::nat) * 0 = 0"
    5.45 +  "0 * x = 0"
    5.46 +  "x * 1 = x"
    5.47 +  "1 * x = x"
    5.48 +  "3 * x = x * 3"
    5.49 +  by smt+
    5.50 +
    5.51 +lemma
    5.52 +  "(0::nat) div 0 = 0"
    5.53 +  "(x::nat) div 0 = 0"
    5.54 +  "(0::nat) div 1 = 0"
    5.55 +  "(1::nat) div 1 = 1"
    5.56 +  "(3::nat) div 1 = 3"
    5.57 +  "(x::nat) div 1 = x"
    5.58 +  "(0::nat) div 3 = 0"
    5.59 +  "(1::nat) div 3 = 0"
    5.60 +  "(3::nat) div 3 = 1"
    5.61 +  "(x::nat) div 3 \<le> x"
    5.62 +  "(x div 3 = x) = (x = 0)"
    5.63 +  using [[z3_extensions]]
    5.64 +  by smt+
    5.65 +
    5.66 +lemma
    5.67 +  "(0::nat) mod 0 = 0"
    5.68 +  "(x::nat) mod 0 = x"
    5.69 +  "(0::nat) mod 1 = 0"
    5.70 +  "(1::nat) mod 1 = 0"
    5.71 +  "(3::nat) mod 1 = 0"
    5.72 +  "(x::nat) mod 1 = 0"
    5.73 +  "(0::nat) mod 3 = 0"
    5.74 +  "(1::nat) mod 3 = 1"
    5.75 +  "(3::nat) mod 3 = 0"
    5.76 +  "x mod 3 < 3"
    5.77 +  "(x mod 3 = x) = (x < 3)"
    5.78 +  using [[z3_extensions]]
    5.79 +  by smt+
    5.80 +
    5.81 +lemma
    5.82 +  "(x::nat) = x div 1 * 1 + x mod 1"
    5.83 +  "x = x div 3 * 3 + x mod 3"
    5.84 +  using [[z3_extensions]]
    5.85 +  by smt+
    5.86 +
    5.87 +lemma
    5.88 +  "min (x::nat) y \<le> x"
    5.89 +  "min x y \<le> y"
    5.90 +  "min x y \<le> x + y"
    5.91 +  "z < x \<and> z < y \<longrightarrow> z < min x y"
    5.92 +  "min x y = min y x"
    5.93 +  "min x 0 = 0"
    5.94 +  by smt+
    5.95 +
    5.96 +lemma
    5.97 +  "max (x::nat) y \<ge> x"
    5.98 +  "max x y \<ge> y"
    5.99 +  "max x y \<ge> (x - y) + (y - x)"
   5.100 +  "z > x \<and> z > y \<longrightarrow> z > max x y"
   5.101 +  "max x y = max y x"
   5.102 +  "max x 0 = x"
   5.103 +  by smt+
   5.104 +
   5.105 +lemma
   5.106 +  "0 \<le> (x::nat)"
   5.107 +  "0 < x \<and> x \<le> 1 \<longrightarrow> x = 1"
   5.108 +  "x \<le> x"
   5.109 +  "x \<le> y \<longrightarrow> 3 * x \<le> 3 * y"
   5.110 +  "x < y \<longrightarrow> 3 * x < 3 * y"
   5.111 +  "x < y \<longrightarrow> x \<le> y"
   5.112 +  "(x < y) = (x + 1 \<le> y)"
   5.113 +  "\<not> (x < x)"
   5.114 +  "x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   5.115 +  "x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   5.116 +  "x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z"
   5.117 +  "x < y \<longrightarrow> y < z \<longrightarrow> x < z"
   5.118 +  "x < y \<and> y < z \<longrightarrow> \<not> (z < x)"
   5.119 +  by smt+
   5.120 +
   5.121 +declare [[smt_nat_as_int = false]]
   5.122 +
   5.123 +
   5.124  section \<open>Integers\<close>
   5.125  
   5.126  lemma
     6.1 --- a/src/HOL/Tools/SMT/smt_builtin.ML	Thu Jul 27 15:22:35 2017 +0100
     6.2 +++ b/src/HOL/Tools/SMT/smt_builtin.ML	Fri Jul 28 15:36:32 2017 +0100
     6.3 @@ -13,7 +13,7 @@
     6.4    val add_builtin_typ: SMT_Util.class ->
     6.5      typ * (typ -> string option) * (typ -> int -> string option) -> Context.generic ->
     6.6      Context.generic
     6.7 -  val add_builtin_typ_ext: typ * (typ -> bool) -> Context.generic ->
     6.8 +  val add_builtin_typ_ext: typ * (Proof.context -> typ -> bool) -> Context.generic ->
     6.9      Context.generic
    6.10    val dest_builtin_typ: Proof.context -> typ -> string option
    6.11    val is_builtin_typ_ext: Proof.context -> typ -> bool
    6.12 @@ -93,7 +93,7 @@
    6.13  structure Builtins = Generic_Data
    6.14  (
    6.15    type T =
    6.16 -    (typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab *
    6.17 +    (Proof.context -> typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab *
    6.18      (term list bfun, bfunr option bfun) btab
    6.19    val empty = ([], Symtab.empty)
    6.20    val extend = I
    6.21 @@ -125,7 +125,7 @@
    6.22  fun is_builtin_typ_ext ctxt T =
    6.23    (case lookup_builtin_typ ctxt T of
    6.24      SOME (_, Int (f, _)) => is_some (f T)
    6.25 -  | SOME (_, Ext f) => f T
    6.26 +  | SOME (_, Ext f) => f ctxt T
    6.27    | NONE => false)
    6.28  
    6.29  
     7.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Thu Jul 27 15:22:35 2017 +0100
     7.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Fri Jul 28 15:36:32 2017 +0100
     7.3 @@ -32,6 +32,7 @@
     7.4    val statistics: bool Config.T
     7.5    val monomorph_limit: int Config.T
     7.6    val monomorph_instances: int Config.T
     7.7 +  val nat_as_int: bool Config.T
     7.8    val infer_triggers: bool Config.T
     7.9    val debug_files: string Config.T
    7.10    val sat_solver: string Config.T
    7.11 @@ -179,6 +180,7 @@
    7.12  val statistics = Attrib.setup_config_bool @{binding smt_statistics} (K false)
    7.13  val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10)
    7.14  val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500)
    7.15 +val nat_as_int = Attrib.setup_config_bool @{binding smt_nat_as_int} (K false)
    7.16  val infer_triggers = Attrib.setup_config_bool @{binding smt_infer_triggers} (K false)
    7.17  val debug_files = Attrib.setup_config_string @{binding smt_debug_files} (K "")
    7.18  val sat_solver = Attrib.setup_config_string @{binding smt_sat_solver} (K "cdclite")
     8.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Thu Jul 27 15:22:35 2017 +0100
     8.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Jul 28 15:36:32 2017 +0100
     8.3 @@ -327,6 +327,85 @@
     8.4  end
     8.5  
     8.6  
     8.7 +(** embedding of standard natural number operations into integer operations **)
     8.8 +
     8.9 +local
    8.10 +  val nat_embedding = @{thms nat_int' int_nat_nneg int_nat_neg}
    8.11 +
    8.12 +  val simple_nat_ops = [
    8.13 +    @{const less (nat)}, @{const less_eq (nat)},
    8.14 +    @{const Suc}, @{const plus (nat)}, @{const minus (nat)}]
    8.15 +
    8.16 +  val mult_nat_ops =
    8.17 +    [@{const times (nat)}, @{const divide (nat)}, @{const modulo (nat)}]
    8.18 +
    8.19 +  val nat_ops = simple_nat_ops @ mult_nat_ops
    8.20 +
    8.21 +  val nat_consts = nat_ops @ [@{const numeral (nat)},
    8.22 +    @{const zero_class.zero (nat)}, @{const one_class.one (nat)}]
    8.23 +
    8.24 +  val nat_int_coercions = [@{const of_nat (int)}, @{const nat}]
    8.25 +
    8.26 +  val builtin_nat_ops = nat_int_coercions @ simple_nat_ops
    8.27 +
    8.28 +  val is_nat_const = member (op aconv) nat_consts
    8.29 +
    8.30 +  fun is_nat_const' @{const of_nat (int)} = true
    8.31 +    | is_nat_const' t = is_nat_const t
    8.32 +
    8.33 +  val expands = map mk_meta_eq @{thms nat_zero_as_int nat_one_as_int nat_numeral_as_int
    8.34 +    nat_less_as_int nat_leq_as_int Suc_as_int nat_plus_as_int nat_minus_as_int nat_times_as_int
    8.35 +    nat_div_as_int nat_mod_as_int}
    8.36 +
    8.37 +  val ints = map mk_meta_eq @{thms of_nat_0 of_nat_1 int_Suc int_plus int_minus of_nat_mult zdiv_int
    8.38 +    zmod_int}
    8.39 +  val int_if = mk_meta_eq @{lemma "int (if P then n else m) = (if P then int n else int m)" by simp}
    8.40 +
    8.41 +  fun mk_number_eq ctxt i lhs =
    8.42 +    let
    8.43 +      val eq = SMT_Util.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
    8.44 +      val ctxt' = put_simpset HOL_ss ctxt addsimps @{thms of_nat_numeral}
    8.45 +      val tac = HEADGOAL (Simplifier.simp_tac ctxt')
    8.46 +    in Goal.norm_result ctxt (Goal.prove_internal ctxt [] eq (K tac)) end
    8.47 +
    8.48 +  fun ite_conv cv1 cv2 =
    8.49 +    Conv.combination_conv (Conv.combination_conv (Conv.arg_conv cv1) cv2) cv2
    8.50 +
    8.51 +  fun int_conv ctxt ct =
    8.52 +    (case Thm.term_of ct of
    8.53 +      @{const of_nat (int)} $ (n as (@{const numeral (nat)} $ _)) =>
    8.54 +        Conv.rewr_conv (mk_number_eq ctxt (snd (HOLogic.dest_number n)) ct)
    8.55 +    | @{const of_nat (int)} $ _ =>
    8.56 +        (Conv.rewrs_conv ints then_conv Conv.sub_conv ints_conv ctxt) else_conv
    8.57 +        (Conv.rewr_conv int_if then_conv
    8.58 +          ite_conv (nat_conv ctxt) (int_conv ctxt)) else_conv
    8.59 +        Conv.sub_conv (Conv.top_sweep_conv nat_conv) ctxt
    8.60 +    | _ => Conv.no_conv) ct
    8.61 +
    8.62 +  and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt
    8.63 +
    8.64 +  and expand_conv ctxt =
    8.65 +    SMT_Util.if_conv (is_nat_const o Term.head_of)
    8.66 +      (expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt) (int_conv ctxt)
    8.67 +
    8.68 +  and nat_conv ctxt = SMT_Util.if_exists_conv is_nat_const' (Conv.top_sweep_conv expand_conv ctxt)
    8.69 +
    8.70 +  val uses_nat_int = Term.exists_subterm (member (op aconv) nat_int_coercions)
    8.71 +in
    8.72 +
    8.73 +val nat_as_int_conv = nat_conv
    8.74 +
    8.75 +fun add_nat_embedding thms =
    8.76 +  if exists (uses_nat_int o Thm.prop_of) thms then (thms, nat_embedding) else (thms, [])
    8.77 +
    8.78 +val setup_nat_as_int =
    8.79 +  SMT_Builtin.add_builtin_typ_ext (@{typ nat},
    8.80 +    fn ctxt => K (Config.get ctxt SMT_Config.nat_as_int)) #>
    8.81 +  fold (SMT_Builtin.add_builtin_fun_ext' o Term.dest_Const) builtin_nat_ops
    8.82 +
    8.83 +end
    8.84 +
    8.85 +
    8.86  (** normalize numerals **)
    8.87  
    8.88  local
    8.89 @@ -359,23 +438,27 @@
    8.90  
    8.91  (** combined unfoldings and rewritings **)
    8.92  
    8.93 -fun unfold_conv ctxt =
    8.94 -  rewrite_case_bool_conv ctxt then_conv
    8.95 -  unfold_abs_min_max_conv ctxt then_conv
    8.96 -  Thm.beta_conversion true
    8.97 -
    8.98 -fun unfold_polymorph ctxt = map (apsnd (Conv.fconv_rule (unfold_conv ctxt)))
    8.99 -fun unfold_monomorph ctxt = map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt)))
   8.100 -
   8.101 -
   8.102 -(* overall normalization *)
   8.103 -
   8.104  fun burrow_ids f ithms =
   8.105    let
   8.106      val (is, thms) = split_list ithms
   8.107      val (thms', extra_thms) = f thms
   8.108    in (is ~~ thms') @ map (pair ~1) extra_thms end
   8.109  
   8.110 +fun unfold_conv ctxt =
   8.111 +  rewrite_case_bool_conv ctxt then_conv
   8.112 +  unfold_abs_min_max_conv ctxt then_conv
   8.113 +  (if Config.get ctxt SMT_Config.nat_as_int then nat_as_int_conv ctxt
   8.114 +   else Conv.all_conv) then_conv
   8.115 +  Thm.beta_conversion true
   8.116 +
   8.117 +fun unfold_polymorph ctxt = map (apsnd (Conv.fconv_rule (unfold_conv ctxt)))
   8.118 +fun unfold_monomorph ctxt =
   8.119 +  map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt)))
   8.120 +  #> Config.get ctxt SMT_Config.nat_as_int ? burrow_ids add_nat_embedding
   8.121 +
   8.122 +
   8.123 +(* overall normalization *)
   8.124 +
   8.125  type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
   8.126  
   8.127  structure Extra_Norms = Generic_Data
   8.128 @@ -439,6 +522,7 @@
   8.129    setup_unfolded_quants #>
   8.130    setup_trigger #>
   8.131    setup_case_bool #>
   8.132 -  setup_abs_min_max))
   8.133 +  setup_abs_min_max #>
   8.134 +  setup_nat_as_int))
   8.135  
   8.136  end;