# HG changeset patch # User blanchet # Date 1501252592 -3600 # Node ID 5ff9fe3fee664f7e506d50b4c3a07866bffffa2a # Parent d425bdf419f5d86687ea3815398d70431cc2676e introduced option for nat-as-int in SMT diff -r d425bdf419f5 -r 5ff9fe3fee66 NEWS --- a/NEWS Thu Jul 27 15:22:35 2017 +0100 +++ b/NEWS Fri Jul 28 15:36:32 2017 +0100 @@ -197,6 +197,9 @@ Knaster-Tarski fixed point theorem and Galois Connections. * SMT module: + - A new option, 'smt_nat_as_int', has been added to translate 'nat' to + 'int' and benefit from the SMT solver's theory reasoning. It is disabled + by default. - The legacy module 'src/HOL/Library/Old_SMT.thy' has been removed. - Several small issues have been rectified in the 'smt' command. diff -r d425bdf419f5 -r 5ff9fe3fee66 src/HOL/SMT.thy --- a/src/HOL/SMT.thy Thu Jul 27 15:22:35 2017 +0100 +++ b/src/HOL/SMT.thy Fri Jul 28 15:36:32 2017 +0100 @@ -119,6 +119,26 @@ lemmas min_def_raw = min_def[abs_def] lemmas max_def_raw = max_def[abs_def] +lemma nat_int': "\n. nat (int n) = n" by simp +lemma int_nat_nneg: "\i. i \ 0 \ int (nat i) = i" by simp +lemma int_nat_neg: "\i. i < 0 \ int (nat i) = 0" by simp + +lemmas nat_zero_as_int = transfer_nat_int_numerals(1) +lemmas nat_one_as_int = transfer_nat_int_numerals(2) +lemma nat_numeral_as_int: "numeral = (\i. nat (numeral i))" by simp +lemma nat_less_as_int: "op < = (\a b. int a < int b)" by simp +lemma nat_leq_as_int: "op \ = (\a b. int a \ int b)" by simp +lemma Suc_as_int: "Suc = (\a. nat (int a + 1))" by (rule ext) simp +lemma nat_plus_as_int: "op + = (\a b. nat (int a + int b))" by (rule ext)+ simp +lemma nat_minus_as_int: "op - = (\a b. nat (int a - int b))" by (rule ext)+ simp +lemma nat_times_as_int: "op * = (\a b. nat (int a * int b))" by (simp add: nat_mult_distrib) +lemma nat_div_as_int: "op div = (\a b. nat (int a div int b))" by (simp add: nat_div_distrib) +lemma nat_mod_as_int: "op mod = (\a b. nat (int a mod int b))" by (simp add: nat_mod_distrib) + +lemma int_Suc: "int (Suc n) = int n + 1" by simp +lemma int_plus: "int (n + m) = int n + int m" by (rule of_nat_add) +lemma int_minus: "int (n - m) = int (nat (int n - int m))" by auto + subsection \Integer division and modulo for Z3\ diff -r d425bdf419f5 -r 5ff9fe3fee66 src/HOL/SMT_Examples/SMT_Examples.certs --- a/src/HOL/SMT_Examples/SMT_Examples.certs Thu Jul 27 15:22:35 2017 +0100 +++ b/src/HOL/SMT_Examples/SMT_Examples.certs Fri Jul 28 15:36:32 2017 +0100 @@ -6633,3 +6633,1474 @@ (let ((@x895 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x117 $x807 (not $x673))) @x891 (or $x807 (not $x673))))) ((_ 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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +d982bc989c38d6a72f2d807a1168e928070f463b 100 0 +unsat +( +a141 +a32 +a142 +a33 +a143 +a34 +a144 +a35 +a145 +a36 +a146 +a147 +a37 +a148 +a38 +a93 +a149 +a39 +a150 +a40 +a151 +a41 +a152 +a96 +a42 +a153 +a43 +a154 +a44 +a155 +a45 +a156 +a46 +a157 +a47 +a158 +a48 +a159 +a160 +a49 +a161 +a50 +a162 +a14 +a13 +a15 +a113 +a16 +a114 +a115 +a169 +a116 +a7 +a117 +a8 +a61 +a118 +a62 +a119 +a120 +a121 +a122 +a69 +a17 +a70 +a124 +a18 +a182 +a71 +a72 +a183 +a73 +a127 +a184 +a74 +a128 +a75 +a129 +a23 +a76 +a130 +a24 +a25 +a79 +a133 +a26 +a27 +a135 +a136 +a28 +a137 +a29 +a138 +a30 +a139 +a140 +a31 +) +356e447dfc184b20563d0467365f8b5f8cef0ab1 97 0 +unsat +( +a29 +a80 +a81 +a30 +a31 +a82 +a32 +a83 +a33 +a84 +a85 +a34 +a86 +a35 +a87 +a36 +a88 +a37 +a89 +a38 +a90 +a39 +a91 +a40 +a92 +a41 +a93 +a42 +a94 +a43 +a95 +a44 +a45 +a96 +a46 +a97 +a50 +a51 +a1 +a52 +a2 +a53 +a3 +a4 +a54 +a5 +a55 +a6 +a56 +a7 +a57 +a8 +a58 +a9 +a59 +a10 +a60 +a11 +a61 +a12 +a62 +a13 +a63 +a14 +a64 +a15 +a65 +a16 +a66 +a17 +a67 +a18 +a68 +a69 +a19 +a70 +a20 +a71 +a21 +a72 +a22 +a73 +a23 +a74 +a24 +a75 +a25 +a76 +a26 +a77 +a27 +a78 +a28 +a79 +) +52fd45adea6478e9d5ad83eff76800476c97a929 2 0 +sat +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +986242bd9f42b2ccb6c2f7242f7302e1f4a543ef 2 0 +sat +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +72ac661c77e89ad0f41fb5c62073e8267bf5a6c1 2 0 +sat +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +707271ac37bbf9aba707687e1d6d62497810fc5d 2 0 +sat +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +9882e692cde42bbd5ed7cdcd884340dfaa68b016 2 0 +sat +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +763f8658cf70daf26cd303b055bde69d09e03192 2 0 +sat +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +5ace894fbc0cab965d77619b71e294a7498ea670 2 0 +sat +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +35953e5bdfb3c20982931376ab02561049c3d3ec 2 0 +sat +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +834942f3e869aeabae6a62cc9136262f9e001d9b 2 0 +sat +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +1915bb36fd704a827d0d979f7d3273ea47ac12ff 2 0 +sat +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +112b71a74adbf7dc3d30f9548dd7e6e7e507b5cb 90 0 +unsat +( +a28 +a78 +a29 +a79 +a30 +a80 +a31 +a32 +a33 +a83 +a84 +a34 +a85 +a35 +a86 +a36 +a87 +a37 +a88 +a38 +a89 +a39 +a90 +a40 +a91 +a41 +a92 +a42 +a93 +a43 +a44 +a45 +a46 +a47 +a48 +a49 +a1 +a50 +a2 +a51 +a52 +a3 +a53 +a4 +a54 +a5 +a55 +a6 +a56 +a57 +a7 +a58 +a8 +a59 +a9 +a60 +a61 +a10 +a62 +a11 +a63 +a12 +a64 +a13 +a65 +a14 +a66 +a15 +a67 +a68 +a17 +a18 +a69 +a70 +a20 +a71 +a21 +a72 +a22 +a23 +a24 +a25 +a75 +a26 +a76 +a27 +a77 +) +55c4468a22c3129940ee0f507180fb5cb8a244d5 2 0 +sat +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +834270f8dd620f74a77f5565b14e1f3bada38fbc 13 0 +unsat +( +a0 +a1 +a2 +a3 +a4 +a5 +a6 +a7 +a8 +a9 +) +f22198ac4ffd581fb59d39b6771250bce4f2b10c 13 0 +unsat +( +a0 +a1 +a2 +a3 +a4 +a5 +a6 +a7 +a8 +a9 +) +c2cfe7fbd368fc0ecc0401a01b53f57caeef131a 4 0 +unsat +( +a0 +) +1b75f6cb11115d60847d54399897af90dea90827 4 0 +unsat +( +a0 +) +4998d5a79895ec5f3cef0120dc86abbbd8e29b48 4 0 +unsat +( +a2 +) +1437414329c2da0f812cda22f62176795fe4b488 2 0 +sat +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +6ca70dfdb60448a41d66f81903a82cf3bfc1d3c0 6 0 +unsat +( +a11 +a4 +a5 +) +2998de44350b8173b123947e09d691282118e3a6 6 0 +unsat +( +a0 +a1 +a2 +) +9e56e42500b1c152c4d6f34a9829575456349872 2 0 +sat +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +20e7bc67dece8e9eee65bc5c217876381ad19805 7 0 +unsat +( +a44 +a5 +a6 +a40 +) +47a88885e5196eac2e3922eb19ce30b6d748259f 7 0 +unsat +( +a0 +a1 +a3 +a5 +) +e06991d1826b36a536b8ecef95433bd1f28774f6 2 0 +unknown +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +5ecd136d06134f07af067717cf168158b90a4fe5 2 0 +unknown +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +0b10533518bb68ba1619340435dfd68ab76ab077 6 0 +unsat +( +a0 +a3 +a104 +) +2a33649206162ac011eff175206722d181426839 6 0 +unsat +( +a0 +a1 +a2 +) +375c41e114323d3d731079fe1d402f74a9d2651f 2 0 +sat +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +e666d5e185fdae30099fc5a288467b6b29dd2412 7 0 +unsat +( +a170 +a176 +a89 +a4 +) +38448f458cf85259745f3f72f0ef85742b6132c3 7 0 +unsat +( +a0 +a1 +a2 +a3 +) +3e59b0c055a1eaf3a70cee6780566e0c51865d4c 2 0 +sat +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +40fc07c6890b8180980355c66bcf18270b94dbe2 5 0 +unsat +( +a0 +a2 +) +a0984a525fc9fe1f8886060622bc7f06810aa427 2 0 +sat +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +bdd84922010fb8a29483543e42719deb8169a21d 2 0 +sat +(error "line 14 column 10: proof is not available") +5229e4ae9267447d5281e256ba94b22471594333 2 0 +sat +(error "line 15 column 10: proof is not available") +9931ad6cacee040172b5200df33d2ff766d9ab3f 2 0 +sat +(error "line 14 column 10: proof is not available") +24fee7a6227ca691697261bdf9710f47f3306cf4 2 0 +sat +(error "line 13 column 10: proof is not available") +f5ea14decc68f09b91c21ca192729ed973297ac3 2 0 +sat +(error "line 10 column 10: proof is not available") +c2358f1bb12beb27e84bf6b9d4edbd4a7ce4c606 2 0 +sat +(error "line 20 column 10: proof is not available") +1e10ff820821c9cb846ff93eb2274f54845cd885 7 0 +unsat +( +a57 +a0 +a3 +a34 +) +037b1f2d8c0f457a04260cddd88499544bfb551f 7 0 +unsat +( +a0 +a1 +a2 +a3 +) +9f1937e419764d5c93a8821ef6d0e32a40427cf1 2 0 +unknown +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +7eaf5e7924f7478914e32e3781267cee9333ddd4 2 0 +unknown +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +1c2b6530334930f2f4f6e0d6b73f1d249b6c5fd8 23 0 +unsat +((set-logic AUFLIA) +(proof +(let ((?x28 (of_nat$ a$))) +(let (($x57 (>= ?x28 4))) +(let (($x47 (>= ?x28 3))) +(let (($x61 (or $x47 (not $x57)))) +(let (($x64 (not $x61))) +(let ((@x51 (monotonicity (rewrite (= (< ?x28 3) (not $x47))) (= (not (< ?x28 3)) (not (not $x47)))))) +(let ((@x55 (trans @x51 (rewrite (= (not (not $x47)) $x47)) (= (not (< ?x28 3)) $x47)))) +(let ((@x63 (monotonicity @x55 (rewrite (= (< (* 2 ?x28) 7) (not $x57))) (= (or (not (< ?x28 3)) (< (* 2 ?x28) 7)) $x61)))) +(let ((@x66 (monotonicity @x63 (= (not (or (not (< ?x28 3)) (< (* 2 ?x28) 7))) $x64)))) +(let (($x36 (not (=> (< ?x28 3) (< (* 2 ?x28) 7))))) +(let (($x34 (< (* 2 ?x28) 7))) +(let (($x30 (< ?x28 3))) +(let (($x38 (not $x30))) +(let (($x39 (or $x38 $x34))) +(let ((@x44 (monotonicity (rewrite (= (=> $x30 $x34) $x39)) (= $x36 (not $x39))))) +(let ((@x71 (not-or-elim (mp (asserted $x36) (trans @x44 @x66 (= $x36 $x64)) $x64) $x57))) +(let (($x45 (not $x47))) +(let ((@x70 (not-or-elim (mp (asserted $x36) (trans @x44 @x66 (= $x36 $x64)) $x64) $x45))) +(unit-resolution ((_ th-lemma arith farkas 1 1) $x61) @x70 @x71 false))))))))))))))))))))) + +995f80f06d5874ea2208846fb3b3217c3a3b9bfd 147 0 +unsat +((set-logic AUFLIA) +(proof +(let ((?x29 (of_nat$ y$))) +(let ((?x30 (+ 1 ?x29))) +(let ((?x31 (nat$ ?x30))) +(let ((?x32 (of_nat$ ?x31))) +(let ((?x43 (* (- 1) ?x29))) +(let ((?x44 (+ ?x43 ?x32))) +(let ((?x47 (nat$ ?x44))) +(let ((?x50 (of_nat$ ?x47))) +(let ((?x567 (* (- 1) ?x32))) +(let ((?x255 (+ ?x29 ?x567 ?x50))) +(let (($x513 (>= ?x255 0))) +(let (($x532 (= ?x255 0))) +(let ((?x568 (+ ?x29 ?x567))) +(let (($x248 (<= ?x568 0))) +(let (($x551 (<= ?x568 (- 1)))) +(let (($x558 (= ?x568 (- 1)))) +(let (($x229 (>= ?x29 (- 1)))) +(let (($x387 (>= ?x29 0))) +(let ((?x154 (nat$ ?x29))) +(let ((?x388 (of_nat$ ?x154))) +(let (($x352 (= ?x388 0))) +(let (($x498 (or $x387 $x352))) +(let (($x584 (forall ((?v0 Int) )(! (let ((?x81 (nat$ ?v0))) +(let ((?x82 (of_nat$ ?x81))) +(let (($x110 (= ?x82 0))) +(let (($x95 (>= ?v0 0))) +(or $x95 $x110))))) :pattern ( (nat$ ?v0) ) :qid k!11)) +)) +(let (($x133 (forall ((?v0 Int) )(! (let ((?x81 (nat$ ?v0))) +(let ((?x82 (of_nat$ ?x81))) +(let (($x110 (= ?x82 0))) +(let (($x95 (>= ?v0 0))) +(or $x95 $x110))))) :qid k!11)) +)) +(let ((?x81 (nat$ ?0))) +(let ((?x82 (of_nat$ ?x81))) +(let (($x110 (= ?x82 0))) +(let (($x95 (>= ?0 0))) +(let (($x130 (or $x95 $x110))) +(let (($x112 (forall ((?v0 Int) )(! (let ((?x81 (nat$ ?v0))) +(let ((?x82 (of_nat$ ?x81))) +(let (($x110 (= ?x82 0))) +(let (($x109 (< ?v0 0))) +(=> $x109 $x110))))) :qid k!11)) +)) +(let (($x118 (forall ((?v0 Int) )(! (let ((?x81 (nat$ ?v0))) +(let ((?x82 (of_nat$ ?x81))) +(let (($x110 (= ?x82 0))) +(let (($x109 (< ?v0 0))) +(let (($x114 (not $x109))) +(or $x114 $x110)))))) :qid k!11)) +)) +(let ((@x125 (monotonicity (rewrite (= (< ?0 0) (not $x95))) (= (not (< ?0 0)) (not (not $x95)))))) +(let ((@x129 (trans @x125 (rewrite (= (not (not $x95)) $x95)) (= (not (< ?0 0)) $x95)))) +(let ((@x135 (quant-intro (monotonicity @x129 (= (or (not (< ?0 0)) $x110) $x130)) (= $x118 $x133)))) +(let ((@x117 (rewrite (= (=> (< ?0 0) $x110) (or (not (< ?0 0)) $x110))))) +(let ((@x138 (mp (asserted $x112) (trans (quant-intro @x117 (= $x112 $x118)) @x135 (= $x112 $x133)) $x133))) +(let ((@x589 (mp (mp~ @x138 (nnf-pos (refl (~ $x130 $x130)) (~ $x133 $x133)) $x133) (quant-intro (refl (= $x130 $x130)) (= $x133 $x584)) $x584))) +(let (($x555 (not $x584))) +(let (($x500 (or $x555 $x387 $x352))) +(let ((@x404 (mp ((_ quant-inst (of_nat$ y$)) (or $x555 $x498)) (rewrite (= (or $x555 $x498) $x500)) $x500))) +(let ((@x487 (unit-resolution (unit-resolution @x404 @x589 $x498) (hypothesis (not $x387)) $x352))) +(let (($x239 (= ?x154 y$))) +(let (($x570 (forall ((?v0 Nat$) )(! (= (nat$ (of_nat$ ?v0)) ?v0) :pattern ( (of_nat$ ?v0) ) :qid k!9)) +)) +(let (($x77 (forall ((?v0 Nat$) )(! (= (nat$ (of_nat$ ?v0)) ?v0) :qid k!9)) +)) +(let ((@x575 (trans (rewrite (= $x77 $x570)) (rewrite (= $x570 $x570)) (= $x77 $x570)))) +(let ((@x144 (refl (~ (= (nat$ (of_nat$ ?0)) ?0) (= (nat$ (of_nat$ ?0)) ?0))))) +(let ((@x576 (mp (mp~ (asserted $x77) (nnf-pos @x144 (~ $x77 $x77)) $x77) @x575 $x570))) +(let (($x241 (not $x570))) +(let (($x231 (or $x241 $x239))) +(let ((@x242 ((_ quant-inst y$) $x231))) +(let ((@x475 (monotonicity (symm (unit-resolution @x242 @x576 $x239) (= y$ ?x154)) (= ?x29 ?x388)))) +(let ((@x480 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= ?x29 0)) $x387)) (hypothesis (not $x387)) (trans @x475 @x487 (= ?x29 0)) false))) +(let ((@x468 (unit-resolution ((_ th-lemma arith farkas 1 1) (or (not $x387) $x229)) (lemma @x480 $x387) $x229))) +(let (($x564 (not $x229))) +(let (($x559 (or $x564 $x558))) +(let (($x578 (forall ((?v0 Int) )(! (let ((?x81 (nat$ ?v0))) +(let ((?x82 (of_nat$ ?x81))) +(let (($x83 (= ?x82 ?v0))) +(let (($x95 (>= ?v0 0))) +(let (($x97 (not $x95))) +(or $x97 $x83)))))) :pattern ( (nat$ ?v0) ) :qid k!10)) +)) +(let (($x103 (forall ((?v0 Int) )(! (let ((?x81 (nat$ ?v0))) +(let ((?x82 (of_nat$ ?x81))) +(let (($x83 (= ?x82 ?v0))) +(let (($x95 (>= ?v0 0))) +(let (($x97 (not $x95))) +(or $x97 $x83)))))) :qid k!10)) +)) +(let ((@x580 (refl (= (or (not $x95) (= ?x82 ?0)) (or (not $x95) (= ?x82 ?0)))))) +(let ((@x139 (refl (~ (or (not $x95) (= ?x82 ?0)) (or (not $x95) (= ?x82 ?0)))))) +(let (($x85 (forall ((?v0 Int) )(! (let ((?x81 (nat$ ?v0))) +(let ((?x82 (of_nat$ ?x81))) +(let (($x83 (= ?x82 ?v0))) +(let (($x80 (<= 0 ?v0))) +(=> $x80 $x83))))) :qid k!10)) +)) +(let (($x91 (forall ((?v0 Int) )(! (let ((?x81 (nat$ ?v0))) +(let ((?x82 (of_nat$ ?x81))) +(let (($x83 (= ?x82 ?v0))) +(or (not (<= 0 ?v0)) $x83)))) :qid k!10)) +)) +(let (($x83 (= ?x82 ?0))) +(let (($x97 (not $x95))) +(let (($x100 (or $x97 $x83))) +(let (($x88 (or (not (<= 0 ?0)) $x83))) +(let ((@x99 (monotonicity (rewrite (= (<= 0 ?0) $x95)) (= (not (<= 0 ?0)) $x97)))) +(let ((@x93 (quant-intro (rewrite (= (=> (<= 0 ?0) $x83) $x88)) (= $x85 $x91)))) +(let ((@x107 (trans @x93 (quant-intro (monotonicity @x99 (= $x88 $x100)) (= $x91 $x103)) (= $x85 $x103)))) +(let ((@x148 (mp~ (mp (asserted $x85) @x107 $x103) (nnf-pos @x139 (~ $x103 $x103)) $x103))) +(let ((@x583 (mp @x148 (quant-intro @x580 (= $x103 $x578)) $x578))) +(let (($x202 (not $x578))) +(let (($x544 (or $x202 $x564 $x558))) +(let (($x557 (or (not (>= ?x30 0)) (= ?x32 ?x30)))) +(let (($x205 (or $x202 $x557))) +(let ((@x566 (monotonicity (rewrite (= (>= ?x30 0) $x229)) (= (not (>= ?x30 0)) $x564)))) +(let ((@x560 (monotonicity @x566 (rewrite (= (= ?x32 ?x30) $x558)) (= $x557 $x559)))) +(let ((@x549 (trans (monotonicity @x560 (= $x205 (or $x202 $x559))) (rewrite (= (or $x202 $x559) $x544)) (= $x205 $x544)))) +(let ((@x550 (mp ((_ quant-inst (+ 1 ?x29)) $x205) @x549 $x544))) +(let ((@x453 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x558) $x551)) (unit-resolution (unit-resolution @x550 @x583 $x559) @x468 $x558) $x551))) +(let (($x251 (not $x248))) +(let (($x535 (or $x251 $x532))) +(let (($x523 (or $x202 $x251 $x532))) +(let (($x541 (or (not (>= ?x44 0)) (= ?x50 ?x44)))) +(let (($x524 (or $x202 $x541))) +(let ((@x531 (monotonicity (rewrite (= (>= ?x44 0) $x248)) (= (not (>= ?x44 0)) $x251)))) +(let ((@x522 (monotonicity @x531 (rewrite (= (= ?x50 ?x44) $x532)) (= $x541 $x535)))) +(let ((@x369 (trans (monotonicity @x522 (= $x524 (or $x202 $x535))) (rewrite (= (or $x202 $x535) $x523)) (= $x524 $x523)))) +(let ((@x511 (mp ((_ quant-inst (+ ?x43 ?x32)) $x524) @x369 $x523))) +(let ((@x459 (unit-resolution (unit-resolution @x511 @x583 $x535) (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x248 (not $x551))) @x453 $x248) $x532))) +(let (($x59 (<= ?x50 0))) +(let ((@x65 (monotonicity (rewrite (= (< 0 ?x50) (not $x59))) (= (not (< 0 ?x50)) (not (not $x59)))))) +(let ((@x69 (trans @x65 (rewrite (= (not (not $x59)) $x59)) (= (not (< 0 ?x50)) $x59)))) +(let (($x53 (< 0 ?x50))) +(let (($x56 (not $x53))) +(let (($x38 (not (< (* 0 ?x32) (of_nat$ (nat$ (- ?x32 ?x29))))))) +(let ((@x49 (monotonicity (rewrite (= (- ?x32 ?x29) ?x44)) (= (nat$ (- ?x32 ?x29)) ?x47)))) +(let ((@x55 (monotonicity (rewrite (= (* 0 ?x32) 0)) (monotonicity @x49 (= (of_nat$ (nat$ (- ?x32 ?x29))) ?x50)) (= (< (* 0 ?x32) (of_nat$ (nat$ (- ?x32 ?x29)))) $x53)))) +(let ((@x72 (mp (asserted $x38) (trans (monotonicity @x55 (= $x38 $x56)) @x69 (= $x38 $x59)) $x59))) +((_ th-lemma arith farkas -1 -1 1) @x72 @x453 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x532) $x513)) @x459 $x513) false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + +49c385b161a0c500f84c45f85272a8ec9574fef4 126 0 +unsat +((set-logic AUFLIA) +(proof +(let ((?x29 (of_nat$ x$))) +(let ((?x30 (* 2 ?x29))) +(let ((?x31 (nat$ ?x30))) +(let ((?x212 (of_nat$ ?x31))) +(let ((?x532 (* (- 1) ?x212))) +(let ((?x533 (+ ?x30 ?x532))) +(let (($x513 (<= ?x533 0))) +(let (($x531 (= ?x533 0))) +(let (($x193 (>= ?x29 0))) +(let (($x487 (>= ?x212 1))) +(let (($x485 (= ?x212 1))) +(let ((?x33 (nat$ 1))) +(let ((?x504 (of_nat$ ?x33))) +(let (($x505 (= ?x504 1))) +(let (($x546 (forall ((?v0 Int) )(! (let ((?x49 (nat$ ?v0))) +(let ((?x50 (of_nat$ ?x49))) +(let (($x51 (= ?x50 ?v0))) +(let (($x64 (>= ?v0 0))) +(let (($x65 (not $x64))) +(or $x65 $x51)))))) :pattern ( (nat$ ?v0) ) :qid k!10)) +)) +(let (($x71 (forall ((?v0 Int) )(! (let ((?x49 (nat$ ?v0))) +(let ((?x50 (of_nat$ ?x49))) +(let (($x51 (= ?x50 ?v0))) +(let (($x64 (>= ?v0 0))) +(let (($x65 (not $x64))) +(or $x65 $x51)))))) :qid k!10)) +)) +(let ((?x49 (nat$ ?0))) +(let ((?x50 (of_nat$ ?x49))) +(let (($x51 (= ?x50 ?0))) +(let (($x64 (>= ?0 0))) +(let (($x65 (not $x64))) +(let (($x68 (or $x65 $x51))) +(let (($x53 (forall ((?v0 Int) )(! (let ((?x49 (nat$ ?v0))) +(let ((?x50 (of_nat$ ?x49))) +(let (($x51 (= ?x50 ?v0))) +(let (($x48 (<= 0 ?v0))) +(=> $x48 $x51))))) :qid k!10)) +)) +(let (($x59 (forall ((?v0 Int) )(! (let ((?x49 (nat$ ?v0))) +(let ((?x50 (of_nat$ ?x49))) +(let (($x51 (= ?x50 ?v0))) +(or (not (<= 0 ?v0)) $x51)))) :qid k!10)) +)) +(let ((@x67 (monotonicity (rewrite (= (<= 0 ?0) $x64)) (= (not (<= 0 ?0)) $x65)))) +(let ((@x73 (quant-intro (monotonicity @x67 (= (or (not (<= 0 ?0)) $x51) $x68)) (= $x59 $x71)))) +(let ((@x58 (rewrite (= (=> (<= 0 ?0) $x51) (or (not (<= 0 ?0)) $x51))))) +(let ((@x76 (mp (asserted $x53) (trans (quant-intro @x58 (= $x53 $x59)) @x73 (= $x53 $x71)) $x71))) +(let ((@x551 (mp (mp~ @x76 (nnf-pos (refl (~ $x68 $x68)) (~ $x71 $x71)) $x71) (quant-intro (refl (= $x68 $x68)) (= $x71 $x546)) $x546))) +(let (($x526 (not $x546))) +(let (($x489 (or $x526 $x505))) +(let ((@x506 (rewrite (= (>= 1 0) true)))) +(let ((@x219 (trans (monotonicity @x506 (= (not (>= 1 0)) (not true))) (rewrite (= (not true) false)) (= (not (>= 1 0)) false)))) +(let ((@x223 (monotonicity @x219 (= (or (not (>= 1 0)) $x505) (or false $x505))))) +(let ((@x503 (trans @x223 (rewrite (= (or false $x505) $x505)) (= (or (not (>= 1 0)) $x505) $x505)))) +(let ((@x493 (monotonicity @x503 (= (or $x526 (or (not (>= 1 0)) $x505)) $x489)))) +(let ((@x496 (trans @x493 (rewrite (= $x489 $x489)) (= (or $x526 (or (not (>= 1 0)) $x505)) $x489)))) +(let ((@x497 (mp ((_ quant-inst 1) (or $x526 (or (not (>= 1 0)) $x505))) @x496 $x489))) +(let (($x34 (= ?x31 ?x33))) +(let ((@x42 (mp (asserted (not (not $x34))) (rewrite (= (not (not $x34)) $x34)) $x34))) +(let ((@x356 (trans (monotonicity @x42 (= ?x212 ?x504)) (unit-resolution @x497 @x551 $x505) $x485))) +(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))))) +(let ((@x374 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= ?x212 0)) (<= ?x212 0))) @x371 (not (= ?x212 0))))) +(let (($x515 (= ?x212 0))) +(let (($x517 (or $x193 $x515))) +(let (($x552 (forall ((?v0 Int) )(! (let ((?x49 (nat$ ?v0))) +(let ((?x50 (of_nat$ ?x49))) +(let (($x78 (= ?x50 0))) +(let (($x64 (>= ?v0 0))) +(or $x64 $x78))))) :pattern ( (nat$ ?v0) ) :qid k!11)) +)) +(let (($x101 (forall ((?v0 Int) )(! (let ((?x49 (nat$ ?v0))) +(let ((?x50 (of_nat$ ?x49))) +(let (($x78 (= ?x50 0))) +(let (($x64 (>= ?v0 0))) +(or $x64 $x78))))) :qid k!11)) +)) +(let ((@x556 (quant-intro (refl (= (or $x64 (= ?x50 0)) (or $x64 (= ?x50 0)))) (= $x101 $x552)))) +(let ((@x120 (nnf-pos (refl (~ (or $x64 (= ?x50 0)) (or $x64 (= ?x50 0)))) (~ $x101 $x101)))) +(let (($x80 (forall ((?v0 Int) )(! (let ((?x49 (nat$ ?v0))) +(let ((?x50 (of_nat$ ?x49))) +(let (($x78 (= ?x50 0))) +(let (($x77 (< ?v0 0))) +(=> $x77 $x78))))) :qid k!11)) +)) +(let (($x86 (forall ((?v0 Int) )(! (let ((?x49 (nat$ ?v0))) +(let ((?x50 (of_nat$ ?x49))) +(let (($x78 (= ?x50 0))) +(let (($x77 (< ?v0 0))) +(let (($x82 (not $x77))) +(or $x82 $x78)))))) :qid k!11)) +)) +(let (($x78 (= ?x50 0))) +(let (($x98 (or $x64 $x78))) +(let (($x77 (< ?0 0))) +(let (($x82 (not $x77))) +(let (($x83 (or $x82 $x78))) +(let ((@x97 (trans (monotonicity (rewrite (= $x77 $x65)) (= $x82 (not $x65))) (rewrite (= (not $x65) $x64)) (= $x82 $x64)))) +(let ((@x105 (trans (quant-intro (rewrite (= (=> $x77 $x78) $x83)) (= $x80 $x86)) (quant-intro (monotonicity @x97 (= $x83 $x98)) (= $x86 $x101)) (= $x80 $x101)))) +(let ((@x557 (mp (mp~ (mp (asserted $x80) @x105 $x101) @x120 $x101) @x556 $x552))) +(let (($x156 (not $x552))) +(let (($x520 (or $x156 $x193 $x515))) +(let ((@x530 (rewrite (= (>= ?x30 0) $x193)))) +(let ((@x523 (monotonicity (monotonicity @x530 (= (or (>= ?x30 0) $x515) $x517)) (= (or $x156 (or (>= ?x30 0) $x515)) (or $x156 $x517))))) +(let ((@x215 (trans @x523 (rewrite (= (or $x156 $x517) $x520)) (= (or $x156 (or (>= ?x30 0) $x515)) $x520)))) +(let ((@x229 (mp ((_ quant-inst (* 2 ?x29)) (or $x156 (or (>= ?x30 0) $x515))) @x215 $x520))) +(let (($x185 (not $x193))) +(let (($x534 (or $x185 $x531))) +(let (($x188 (or $x526 $x185 $x531))) +(let (($x213 (= ?x212 ?x30))) +(let (($x208 (>= ?x30 0))) +(let (($x209 (not $x208))) +(let (($x214 (or $x209 $x213))) +(let (($x189 (or $x526 $x214))) +(let ((@x536 (monotonicity (monotonicity @x530 (= $x209 $x185)) (rewrite (= $x213 $x531)) (= $x214 $x534)))) +(let ((@x175 (trans (monotonicity @x536 (= $x189 (or $x526 $x534))) (rewrite (= (or $x526 $x534) $x188)) (= $x189 $x188)))) +(let ((@x176 (mp ((_ quant-inst (* 2 ?x29)) $x189) @x175 $x188))) +(let ((@x470 (unit-resolution (unit-resolution @x176 @x551 $x534) (unit-resolution (unit-resolution @x229 @x557 $x517) @x374 $x193) $x531))) +(let (($x514 (>= ?x533 0))) +(let (($x486 (<= ?x212 1))) +((_ 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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + +b2e870cca8f9ff26b649a7a2c6910fff2183e779 6 0 +unsat +( +a0 +a259 +a260 +) +0df05630a046f3db612e71e7557cbf94daec55ea 6 0 +unsat +( +a0 +a2 +a3 +) +5d99a07ea08069a53b86d7f3330815887331e82a 145 0 +unsat +((set-logic AUFLIA) +(proof +(let ((?x29 (of_nat$ y$))) +(let ((?x30 (+ 1 ?x29))) +(let ((?x31 (nat$ ?x30))) +(let ((?x32 (of_nat$ ?x31))) +(let ((?x48 (+ (- 1) ?x32))) +(let ((?x51 (nat$ ?x48))) +(let ((?x585 (of_nat$ ?x51))) +(let ((?x299 (* (- 1) ?x585))) +(let ((?x434 (+ ?x29 ?x299))) +(let (($x436 (>= ?x434 0))) +(let (($x558 (= ?x29 ?x585))) +(let (($x54 (= ?x51 y$))) +(let (($x88 (<= ?x32 0))) +(let (($x98 (not (or (= (not $x88) $x54) (not $x88))))) +(let (($x40 (=> (not (ite (< 0 ?x32) true false)) false))) +(let (($x33 (< 0 ?x32))) +(let (($x34 (ite $x33 true false))) +(let (($x38 (= $x34 (= (nat$ (- ?x32 1)) y$)))) +(let (($x42 (or false (or $x38 $x40)))) +(let (($x43 (not $x42))) +(let (($x60 (= $x33 $x54))) +(let (($x75 (or $x60 $x33))) +(let ((@x94 (monotonicity (rewrite (= $x33 (not $x88))) (= $x60 (= (not $x88) $x54))))) +(let ((@x97 (monotonicity @x94 (rewrite (= $x33 (not $x88))) (= $x75 (or (= (not $x88) $x54) (not $x88)))))) +(let ((@x70 (monotonicity (monotonicity (rewrite (= $x34 $x33)) (= (not $x34) (not $x33))) (= $x40 (=> (not $x33) false))))) +(let ((@x74 (trans @x70 (rewrite (= (=> (not $x33) false) $x33)) (= $x40 $x33)))) +(let ((@x53 (monotonicity (rewrite (= (- ?x32 1) ?x48)) (= (nat$ (- ?x32 1)) ?x51)))) +(let ((@x59 (monotonicity (rewrite (= $x34 $x33)) (monotonicity @x53 (= (= (nat$ (- ?x32 1)) y$) $x54)) (= $x38 (= $x33 $x54))))) +(let ((@x77 (monotonicity (trans @x59 (rewrite (= (= $x33 $x54) $x60)) (= $x38 $x60)) @x74 (= (or $x38 $x40) $x75)))) +(let ((@x84 (trans (monotonicity @x77 (= $x42 (or false $x75))) (rewrite (= (or false $x75) $x75)) (= $x42 $x75)))) +(let ((@x102 (trans (monotonicity @x84 (= $x43 (not $x75))) (monotonicity @x97 (= (not $x75) $x98)) (= $x43 $x98)))) +(let ((@x106 (not-or-elim (mp (asserted $x43) @x102 $x98) $x88))) +(let ((@x187 (monotonicity (iff-true @x106 (= $x88 true)) (= (= $x88 $x54) (= true $x54))))) +(let ((@x191 (trans @x187 (rewrite (= (= true $x54) $x54)) (= (= $x88 $x54) $x54)))) +(let (($x173 (= $x88 $x54))) +(let ((@x105 (not-or-elim (mp (asserted $x43) @x102 $x98) (not (= (not $x88) $x54))))) +(let ((@x192 (mp (mp @x105 (rewrite (= (not (= (not $x88) $x54)) $x173)) $x173) @x191 $x54))) +(let ((@x457 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x558) $x436)) (monotonicity (symm @x192 (= y$ ?x51)) $x558) $x436))) +(let ((?x613 (* (- 1) ?x32))) +(let ((?x614 (+ ?x29 ?x613))) +(let (($x595 (<= ?x614 (- 1)))) +(let (($x612 (= ?x614 (- 1)))) +(let (($x610 (>= ?x29 (- 1)))) +(let (($x557 (>= ?x585 0))) +(let (($x559 (= ?x585 0))) +(let (($x586 (>= ?x32 1))) +(let (($x589 (not $x586))) +(let (($x632 (forall ((?v0 Int) )(! (let ((?x115 (nat$ ?v0))) +(let ((?x116 (of_nat$ ?x115))) +(let (($x144 (= ?x116 0))) +(let (($x129 (>= ?v0 0))) +(or $x129 $x144))))) :pattern ( (nat$ ?v0) ) :qid k!11)) +)) +(let (($x167 (forall ((?v0 Int) )(! (let ((?x115 (nat$ ?v0))) +(let ((?x116 (of_nat$ ?x115))) +(let (($x144 (= ?x116 0))) +(let (($x129 (>= ?v0 0))) +(or $x129 $x144))))) :qid k!11)) +)) +(let ((?x115 (nat$ ?0))) +(let ((?x116 (of_nat$ ?x115))) +(let (($x144 (= ?x116 0))) +(let (($x129 (>= ?0 0))) +(let (($x164 (or $x129 $x144))) +(let (($x146 (forall ((?v0 Int) )(! (let ((?x115 (nat$ ?v0))) +(let ((?x116 (of_nat$ ?x115))) +(let (($x144 (= ?x116 0))) +(let (($x143 (< ?v0 0))) +(=> $x143 $x144))))) :qid k!11)) +)) +(let (($x152 (forall ((?v0 Int) )(! (let ((?x115 (nat$ ?v0))) +(let ((?x116 (of_nat$ ?x115))) +(let (($x144 (= ?x116 0))) +(let (($x143 (< ?v0 0))) +(let (($x148 (not $x143))) +(or $x148 $x144)))))) :qid k!11)) +)) +(let ((@x159 (monotonicity (rewrite (= (< ?0 0) (not $x129))) (= (not (< ?0 0)) (not (not $x129)))))) +(let ((@x163 (trans @x159 (rewrite (= (not (not $x129)) $x129)) (= (not (< ?0 0)) $x129)))) +(let ((@x169 (quant-intro (monotonicity @x163 (= (or (not (< ?0 0)) $x144) $x164)) (= $x152 $x167)))) +(let ((@x151 (rewrite (= (=> (< ?0 0) $x144) (or (not (< ?0 0)) $x144))))) +(let ((@x172 (mp (asserted $x146) (trans (quant-intro @x151 (= $x146 $x152)) @x169 (= $x146 $x167)) $x167))) +(let ((@x637 (mp (mp~ @x172 (nnf-pos (refl (~ $x164 $x164)) (~ $x167 $x167)) $x167) (quant-intro (refl (= $x164 $x164)) (= $x167 $x632)) $x632))) +(let (($x601 (not $x632))) +(let (($x564 (or $x601 $x586 $x559))) +(let ((@x588 (rewrite (= (>= ?x48 0) $x586)))) +(let ((@x394 (monotonicity (monotonicity @x588 (= (or (>= ?x48 0) $x559) (or $x586 $x559))) (= (or $x601 (or (>= ?x48 0) $x559)) (or $x601 (or $x586 $x559)))))) +(let ((@x554 (trans @x394 (rewrite (= (or $x601 (or $x586 $x559)) $x564)) (= (or $x601 (or (>= ?x48 0) $x559)) $x564)))) +(let ((@x555 (mp ((_ quant-inst (+ (- 1) ?x32)) (or $x601 (or (>= ?x48 0) $x559))) @x554 $x564))) +(let ((@x539 (unit-resolution @x555 @x637 (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x589 (not $x88))) @x106 $x589) $x559))) +(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))) +(let (($x605 (not $x610))) +(let (($x616 (or $x605 $x612))) +(let (($x626 (forall ((?v0 Int) )(! (let ((?x115 (nat$ ?v0))) +(let ((?x116 (of_nat$ ?x115))) +(let (($x117 (= ?x116 ?v0))) +(let (($x129 (>= ?v0 0))) +(let (($x131 (not $x129))) +(or $x131 $x117)))))) :pattern ( (nat$ ?v0) ) :qid k!10)) +)) +(let (($x137 (forall ((?v0 Int) )(! (let ((?x115 (nat$ ?v0))) +(let ((?x116 (of_nat$ ?x115))) +(let (($x117 (= ?x116 ?v0))) +(let (($x129 (>= ?v0 0))) +(let (($x131 (not $x129))) +(or $x131 $x117)))))) :qid k!10)) +)) +(let ((@x628 (refl (= (or (not $x129) (= ?x116 ?0)) (or (not $x129) (= ?x116 ?0)))))) +(let ((@x185 (refl (~ (or (not $x129) (= ?x116 ?0)) (or (not $x129) (= ?x116 ?0)))))) +(let (($x119 (forall ((?v0 Int) )(! (let ((?x115 (nat$ ?v0))) +(let ((?x116 (of_nat$ ?x115))) +(let (($x117 (= ?x116 ?v0))) +(let (($x114 (<= 0 ?v0))) +(=> $x114 $x117))))) :qid k!10)) +)) +(let (($x125 (forall ((?v0 Int) )(! (let ((?x115 (nat$ ?v0))) +(let ((?x116 (of_nat$ ?x115))) +(let (($x117 (= ?x116 ?v0))) +(or (not (<= 0 ?v0)) $x117)))) :qid k!10)) +)) +(let (($x117 (= ?x116 ?0))) +(let (($x131 (not $x129))) +(let (($x134 (or $x131 $x117))) +(let (($x122 (or (not (<= 0 ?0)) $x117))) +(let ((@x133 (monotonicity (rewrite (= (<= 0 ?0) $x129)) (= (not (<= 0 ?0)) $x131)))) +(let ((@x127 (quant-intro (rewrite (= (=> (<= 0 ?0) $x117) $x122)) (= $x119 $x125)))) +(let ((@x141 (trans @x127 (quant-intro (monotonicity @x133 (= $x122 $x134)) (= $x125 $x137)) (= $x119 $x137)))) +(let ((@x196 (mp~ (mp (asserted $x119) @x141 $x137) (nnf-pos @x185 (~ $x137 $x137)) $x137))) +(let ((@x631 (mp @x196 (quant-intro @x628 (= $x137 $x626)) $x626))) +(let (($x269 (not $x626))) +(let (($x607 (or $x269 $x605 $x612))) +(let (($x273 (= ?x32 ?x30))) +(let (($x291 (>= ?x30 0))) +(let (($x292 (not $x291))) +(let (($x609 (or $x292 $x273))) +(let (($x271 (or $x269 $x609))) +(let ((@x268 (monotonicity (monotonicity (rewrite (= $x291 $x610)) (= $x292 $x605)) (rewrite (= $x273 $x612)) (= $x609 $x616)))) +(let ((@x593 (trans (monotonicity @x268 (= $x271 (or $x269 $x616))) (rewrite (= (or $x269 $x616) $x607)) (= $x271 $x607)))) +(let ((@x594 (mp ((_ quant-inst (+ 1 ?x29)) $x271) @x593 $x607))) +(let ((@x538 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x612) $x595)) (unit-resolution (unit-resolution @x594 @x631 $x616) @x545 $x612) $x595))) +((_ 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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + +09cc14017050c484625b3e0c3d671ae32b66851f 5 0 +unsat +( +a0 +a1 +) +7d4feac3284b531c122b21d3a2a25c87f1e3b93b 78 0 +unsat +((set-logic AUFLIA) +(proof +(let ((?x37 (* (- 1) x$))) +(let (($x55 (>= x$ 0))) +(let ((?x62 (ite $x55 x$ ?x37))) +(let ((?x554 (* (- 1) ?x62))) +(let ((?x217 (+ ?x37 ?x554))) +(let (($x562 (<= ?x217 0))) +(let (($x249 (= ?x37 ?x62))) +(let (($x56 (not $x55))) +(let (($x163 (= x$ ?x62))) +(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)))) +(let (($x254 (>= ?x62 0))) +(let (($x255 (not $x254))) +(let (($x588 (forall ((?v0 Int) )(! (let ((?x90 (nat$ ?v0))) +(let ((?x91 (of_nat$ ?x90))) +(let (($x92 (= ?x91 ?v0))) +(let (($x104 (>= ?v0 0))) +(let (($x106 (not $x104))) +(or $x106 $x92)))))) :pattern ( (nat$ ?v0) ) :qid k!10)) +)) +(let (($x112 (forall ((?v0 Int) )(! (let ((?x90 (nat$ ?v0))) +(let ((?x91 (of_nat$ ?x90))) +(let (($x92 (= ?x91 ?v0))) +(let (($x104 (>= ?v0 0))) +(let (($x106 (not $x104))) +(or $x106 $x92)))))) :qid k!10)) +)) +(let ((?x90 (nat$ ?0))) +(let ((?x91 (of_nat$ ?x90))) +(let (($x92 (= ?x91 ?0))) +(let (($x104 (>= ?0 0))) +(let (($x106 (not $x104))) +(let (($x109 (or $x106 $x92))) +(let (($x94 (forall ((?v0 Int) )(! (let ((?x90 (nat$ ?v0))) +(let ((?x91 (of_nat$ ?x90))) +(let (($x92 (= ?x91 ?v0))) +(let (($x89 (<= 0 ?v0))) +(=> $x89 $x92))))) :qid k!10)) +)) +(let (($x100 (forall ((?v0 Int) )(! (let ((?x90 (nat$ ?v0))) +(let ((?x91 (of_nat$ ?x90))) +(let (($x92 (= ?x91 ?v0))) +(or (not (<= 0 ?v0)) $x92)))) :qid k!10)) +)) +(let ((@x108 (monotonicity (rewrite (= (<= 0 ?0) $x104)) (= (not (<= 0 ?0)) $x106)))) +(let ((@x114 (quant-intro (monotonicity @x108 (= (or (not (<= 0 ?0)) $x92) $x109)) (= $x100 $x112)))) +(let ((@x99 (rewrite (= (=> (<= 0 ?0) $x92) (or (not (<= 0 ?0)) $x92))))) +(let ((@x117 (mp (asserted $x94) (trans (quant-intro @x99 (= $x94 $x100)) @x114 (= $x94 $x112)) $x112))) +(let ((@x593 (mp (mp~ @x117 (nnf-pos (refl (~ $x109 $x109)) (~ $x112 $x112)) $x112) (quant-intro (refl (= $x109 $x109)) (= $x112 $x588)) $x588))) +(let ((?x67 (nat$ ?x62))) +(let ((?x70 (of_nat$ ?x67))) +(let (($x73 (= ?x70 ?x62))) +(let (($x76 (not $x73))) +(let (($x28 (< x$ 0))) +(let ((?x30 (ite $x28 (- x$) x$))) +(let (($x34 (not (= (of_nat$ (nat$ ?x30)) ?x30)))) +(let (($x77 (= (not (= (of_nat$ (nat$ (ite $x28 ?x37 x$))) (ite $x28 ?x37 x$))) $x76))) +(let ((?x40 (ite $x28 ?x37 x$))) +(let ((?x43 (nat$ ?x40))) +(let ((?x46 (of_nat$ ?x43))) +(let (($x49 (= ?x46 ?x40))) +(let ((@x66 (trans (monotonicity (rewrite (= $x28 $x56)) (= ?x40 (ite $x56 ?x37 x$))) (rewrite (= (ite $x56 ?x37 x$) ?x62)) (= ?x40 ?x62)))) +(let ((@x75 (monotonicity (monotonicity (monotonicity @x66 (= ?x43 ?x67)) (= ?x46 ?x70)) @x66 (= $x49 $x73)))) +(let ((@x45 (monotonicity (monotonicity (rewrite (= (- x$) ?x37)) (= ?x30 ?x40)) (= (nat$ ?x30) ?x43)))) +(let ((@x51 (monotonicity (monotonicity @x45 (= (of_nat$ (nat$ ?x30)) ?x46)) (monotonicity (rewrite (= (- x$) ?x37)) (= ?x30 ?x40)) (= (= (of_nat$ (nat$ ?x30)) ?x30) $x49)))) +(let ((@x80 (trans (monotonicity @x51 (= $x34 (not $x49))) (monotonicity @x75 $x77) (= $x34 $x76)))) +(let ((@x81 (mp (asserted $x34) @x80 $x76))) +(let (($x239 (or (not $x588) $x255 $x73))) +(let ((@x576 (mp ((_ quant-inst (ite $x55 x$ ?x37)) (or (not $x588) (or $x255 $x73))) (rewrite (= (or (not $x588) (or $x255 $x73)) $x239)) $x239))) +(let ((@x561 ((_ th-lemma arith farkas -1 1 1) (hypothesis $x55) (unit-resolution @x576 @x81 @x593 $x255) @x559 false))) +(let ((@x198 (lemma @x561 $x56))) +(let ((@x566 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x249) $x562)) (unit-resolution (def-axiom (or $x55 $x249)) @x198 $x249) $x562))) +(let (($x578 (<= ?x62 0))) +(let ((@x257 (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x578 $x254)) (unit-resolution @x576 @x81 @x593 $x255) $x578))) +((_ th-lemma arith farkas 1 1 1) @x257 @x198 @x566 false))))))))))))))))))))))))))))))))))))))))))))))))))))))) + +74a1c0d44cbd0147017229e79a08e8dfcfe4eee2 7 0 +unsat +( +a2 +a189 +a138 +a7 +) +1a98e6860e90be637d16c2d7127e7141065068af 5 0 +unsat +( +a0 +a1 +) +14f8ad1280ad869e9c8ef4e6a613ceb808bfd5ab 7 0 +unsat +( +a0 +a1 +a2 +a4 +) +15ec6864dfa5b932b5e4bed685e55140b1a81105 6 0 +unsat +( +a0 +a1 +a3 +) +ce85402875b83dc2f06a381810d29a2061933b9f 312 0 +unsat +((set-logic AUFLIA) +(declare-fun ?v1!0 (Nat$) Nat$) +(proof +(let ((?x89 (of_nat$ m$))) +(let ((?x90 (* 4 ?x89))) +(let ((?x98 (+ 1 ?x90))) +(let ((?x101 (nat$ ?x98))) +(let ((?x295 (of_nat$ ?x101))) +(let ((?x598 (* (- 1) ?x295))) +(let ((?x599 (+ ?x90 ?x598))) +(let (($x574 (>= ?x599 (- 1)))) +(let (($x597 (= ?x599 (- 1)))) +(let (($x610 (>= ?x89 0))) +(let (($x380 (<= ?x295 1))) +(let (($x687 (not $x380))) +(let (($x701 (forall ((?v1 Nat$) )(! (let ((?x89 (of_nat$ m$))) +(let ((?x90 (* 4 ?x89))) +(let ((?x98 (+ 1 ?x90))) +(let ((?x101 (nat$ ?x98))) +(let (($x382 (= ?v1 ?x101))) +(let ((?x34 (nat$ 1))) +(let (($x35 (= ?v1 ?x34))) +(let (($x381 (dvd$ ?v1 ?x101))) +(let (($x371 (not $x381))) +(or $x371 $x35 $x382)))))))))) :pattern ( (dvd$ ?v1 (nat$ (+ 1 (* 4 (of_nat$ m$))))) ) :qid k!10)) +)) +(let (($x702 (not $x701))) +(let (($x357 (or $x380 $x702))) +(let (($x487 (not $x357))) +(let (($x104 (prime_nat$ ?x101))) +(let (($x110 (not $x104))) +(let (($x697 (or $x110 $x487))) +(let ((?x703 (?v1!0 ?x101))) +(let (($x707 (= ?x703 ?x101))) +(let ((?x34 (nat$ 1))) +(let (($x706 (= ?x703 ?x34))) +(let (($x704 (dvd$ ?x703 ?x101))) +(let (($x705 (not $x704))) +(let (($x708 (or $x705 $x706 $x707))) +(let (($x698 (not $x708))) +(let (($x360 (or $x104 $x380 $x698))) +(let (($x700 (not $x360))) +(let (($x369 (not $x697))) +(let (($x342 (or $x369 $x700))) +(let (($x684 (not $x342))) +(let (($x738 (forall ((?v0 Nat$) )(! (let (($x219 (or (not (dvd$ (?v1!0 ?v0) ?v0)) (= (?v1!0 ?v0) (nat$ 1)) (= (?v1!0 ?v0) ?v0)))) +(let (($x220 (not $x219))) +(let ((?x30 (of_nat$ ?v0))) +(let (($x65 (<= ?x30 1))) +(let (($x28 (prime_nat$ ?v0))) +(let (($x245 (or $x28 $x65 $x220))) +(let (($x710 (forall ((?v1 Nat$) )(! (let ((?x34 (nat$ 1))) +(let (($x35 (= ?v1 ?x34))) +(or (not (dvd$ ?v1 ?v0)) $x35 (= ?v1 ?v0)))) :pattern ( (dvd$ ?v1 ?v0) ) :qid k!10)) +)) +(let (($x200 (not $x28))) +(not (or (not (or $x200 (not (or $x65 (not $x710))))) (not $x245))))))))))) :pattern ( (prime_nat$ ?v0) ) :pattern ( (of_nat$ ?v0) ) :qid k!10)) +)) +(let (($x290 (forall ((?v0 Nat$) )(! (let (($x219 (or (not (dvd$ (?v1!0 ?v0) ?v0)) (= (?v1!0 ?v0) (nat$ 1)) (= (?v1!0 ?v0) ?v0)))) +(let (($x220 (not $x219))) +(let ((?x30 (of_nat$ ?v0))) +(let (($x65 (<= ?x30 1))) +(let (($x28 (prime_nat$ ?v0))) +(let (($x245 (or $x28 $x65 $x220))) +(let (($x72 (forall ((?v1 Nat$) )(! (let ((?x34 (nat$ 1))) +(let (($x35 (= ?v1 ?x34))) +(or (not (dvd$ ?v1 ?v0)) $x35 (= ?v1 ?v0)))) :qid k!10)) +)) +(let (($x221 (not $x72))) +(let (($x273 (not (or $x65 $x221)))) +(let (($x200 (not $x28))) +(let (($x276 (or $x200 $x273))) +(not (or (not $x276) (not $x245)))))))))))))) :qid k!10)) +)) +(let (($x219 (or (not (dvd$ (?v1!0 ?0) ?0)) (= (?v1!0 ?0) ?x34) (= (?v1!0 ?0) ?0)))) +(let (($x220 (not $x219))) +(let ((?x30 (of_nat$ ?0))) +(let (($x65 (<= ?x30 1))) +(let (($x28 (prime_nat$ ?0))) +(let (($x245 (or $x28 $x65 $x220))) +(let (($x710 (forall ((?v1 Nat$) )(! (let ((?x34 (nat$ 1))) +(let (($x35 (= ?v1 ?x34))) +(or (not (dvd$ ?v1 ?0)) $x35 (= ?v1 ?0)))) :pattern ( (dvd$ ?v1 ?0) ) :qid k!10)) +)) +(let (($x200 (not $x28))) +(let (($x72 (forall ((?v1 Nat$) )(! (let ((?x34 (nat$ 1))) +(let (($x35 (= ?v1 ?x34))) +(or (not (dvd$ ?v1 ?0)) $x35 (= ?v1 ?0)))) :qid k!10)) +)) +(let (($x221 (not $x72))) +(let (($x273 (not (or $x65 $x221)))) +(let (($x276 (or $x200 $x273))) +(let (($x285 (not (or (not $x276) (not $x245))))) +(let (($x734 (= $x285 (not (or (not (or $x200 (not (or $x65 (not $x710))))) (not $x245)))))) +(let (($x731 (= (or (not $x276) (not $x245)) (or (not (or $x200 (not (or $x65 (not $x710))))) (not $x245))))) +(let (($x35 (= ?0 ?x34))) +(let (($x69 (or (not (dvd$ ?0 ?1)) $x35 (= ?0 ?1)))) +(let ((@x717 (monotonicity (quant-intro (refl (= $x69 $x69)) (= $x72 $x710)) (= $x221 (not $x710))))) +(let ((@x723 (monotonicity (monotonicity @x717 (= (or $x65 $x221) (or $x65 (not $x710)))) (= $x273 (not (or $x65 (not $x710))))))) +(let ((@x729 (monotonicity (monotonicity @x723 (= $x276 (or $x200 (not (or $x65 (not $x710)))))) (= (not $x276) (not (or $x200 (not (or $x65 (not $x710))))))))) +(let ((@x740 (quant-intro (monotonicity (monotonicity @x729 $x731) $x734) (= $x290 $x738)))) +(let (($x253 (forall ((?v0 Nat$) )(! (let (($x219 (or (not (dvd$ (?v1!0 ?v0) ?v0)) (= (?v1!0 ?v0) (nat$ 1)) (= (?v1!0 ?v0) ?v0)))) +(let (($x220 (not $x219))) +(let ((?x30 (of_nat$ ?v0))) +(let (($x65 (<= ?x30 1))) +(let (($x28 (prime_nat$ ?v0))) +(let (($x245 (or $x28 $x65 $x220))) +(let (($x72 (forall ((?v1 Nat$) )(! (let ((?x34 (nat$ 1))) +(let (($x35 (= ?v1 ?x34))) +(or (not (dvd$ ?v1 ?v0)) $x35 (= ?v1 ?v0)))) :qid k!10)) +)) +(let (($x66 (not $x65))) +(let (($x75 (and $x66 $x72))) +(let (($x200 (not $x28))) +(let (($x229 (or $x200 $x75))) +(and $x229 $x245)))))))))))) :qid k!10)) +)) +(let ((@x278 (monotonicity (rewrite (= (and (not $x65) $x72) $x273)) (= (or $x200 (and (not $x65) $x72)) $x276)))) +(let ((@x281 (monotonicity @x278 (= (and (or $x200 (and (not $x65) $x72)) $x245) (and $x276 $x245))))) +(let ((@x289 (trans @x281 (rewrite (= (and $x276 $x245) $x285)) (= (and (or $x200 (and (not $x65) $x72)) $x245) $x285)))) +(let (($x233 (forall ((?v0 Nat$) )(! (let (($x219 (or (not (dvd$ (?v1!0 ?v0) ?v0)) (= (?v1!0 ?v0) (nat$ 1)) (= (?v1!0 ?v0) ?v0)))) +(let (($x220 (not $x219))) +(let ((?x30 (of_nat$ ?v0))) +(let (($x65 (<= ?x30 1))) +(let (($x66 (not $x65))) +(let (($x211 (not $x66))) +(let (($x224 (or $x211 $x220))) +(let (($x28 (prime_nat$ ?v0))) +(let (($x228 (or $x28 $x224))) +(let (($x72 (forall ((?v1 Nat$) )(! (let ((?x34 (nat$ 1))) +(let (($x35 (= ?v1 ?x34))) +(or (not (dvd$ ?v1 ?v0)) $x35 (= ?v1 ?v0)))) :qid k!10)) +)) +(let (($x75 (and $x66 $x72))) +(let (($x200 (not $x28))) +(let (($x229 (or $x200 $x75))) +(and $x229 $x228)))))))))))))) :qid k!10)) +)) +(let (($x66 (not $x65))) +(let (($x75 (and $x66 $x72))) +(let (($x229 (or $x200 $x75))) +(let (($x250 (and $x229 $x245))) +(let (($x211 (not $x66))) +(let (($x224 (or $x211 $x220))) +(let (($x228 (or $x28 $x224))) +(let (($x230 (and $x229 $x228))) +(let ((@x244 (monotonicity (monotonicity (rewrite (= $x211 $x65)) (= $x224 (or $x65 $x220))) (= $x228 (or $x28 (or $x65 $x220)))))) +(let ((@x249 (trans @x244 (rewrite (= (or $x28 (or $x65 $x220)) $x245)) (= $x228 $x245)))) +(let (($x81 (forall ((?v0 Nat$) )(! (let (($x72 (forall ((?v1 Nat$) )(! (let ((?x34 (nat$ 1))) +(let (($x35 (= ?v1 ?x34))) +(or (not (dvd$ ?v1 ?v0)) $x35 (= ?v1 ?v0)))) :qid k!10)) +)) +(let ((?x30 (of_nat$ ?v0))) +(let (($x65 (<= ?x30 1))) +(let (($x66 (not $x65))) +(let (($x75 (and $x66 $x72))) +(let (($x28 (prime_nat$ ?v0))) +(= $x28 $x75))))))) :qid k!10)) +)) +(let ((@x227 (nnf-neg (refl (~ $x211 $x211)) (sk (~ $x221 $x220)) (~ (not $x75) $x224)))) +(let ((@x210 (monotonicity (refl (~ $x66 $x66)) (nnf-pos (refl (~ $x69 $x69)) (~ $x72 $x72)) (~ $x75 $x75)))) +(let ((@x232 (nnf-pos (refl (~ $x28 $x28)) (refl (~ $x200 $x200)) @x210 @x227 (~ (= $x28 $x75) $x230)))) +(let (($x42 (forall ((?v0 Nat$) )(! (let (($x39 (forall ((?v1 Nat$) )(! (let (($x33 (dvd$ ?v1 ?v0))) +(=> $x33 (or (= ?v1 (nat$ 1)) (= ?v1 ?v0)))) :qid k!10)) +)) +(let ((?x30 (of_nat$ ?v0))) +(let (($x31 (< 1 ?x30))) +(let (($x28 (prime_nat$ ?v0))) +(= $x28 (and $x31 $x39)))))) :qid k!10)) +)) +(let (($x62 (forall ((?v0 Nat$) )(! (let (($x48 (forall ((?v1 Nat$) )(! (or (not (dvd$ ?v1 ?v0)) (or (= ?v1 (nat$ 1)) (= ?v1 ?v0))) :qid k!10)) +)) +(let ((?x30 (of_nat$ ?v0))) +(let (($x31 (< 1 ?x30))) +(let (($x51 (and $x31 $x48))) +(let (($x28 (prime_nat$ ?v0))) +(= $x28 $x51)))))) :qid k!10)) +)) +(let (($x78 (= $x28 $x75))) +(let (($x48 (forall ((?v1 Nat$) )(! (or (not (dvd$ ?v1 ?0)) (or (= ?v1 (nat$ 1)) (= ?v1 ?0))) :qid k!10)) +)) +(let (($x31 (< 1 ?x30))) +(let (($x51 (and $x31 $x48))) +(let (($x57 (= $x28 $x51))) +(let ((@x71 (rewrite (= (or (not (dvd$ ?0 ?1)) (or $x35 (= ?0 ?1))) $x69)))) +(let ((@x77 (monotonicity (rewrite (= $x31 $x66)) (quant-intro @x71 (= $x48 $x72)) (= $x51 $x75)))) +(let (($x39 (forall ((?v1 Nat$) )(! (let (($x33 (dvd$ ?v1 ?0))) +(=> $x33 (or (= ?v1 (nat$ 1)) (= ?v1 ?0)))) :qid k!10)) +)) +(let (($x41 (= $x28 (and $x31 $x39)))) +(let (($x45 (or (not (dvd$ ?0 ?1)) (or $x35 (= ?0 ?1))))) +(let ((@x50 (quant-intro (rewrite (= (=> (dvd$ ?0 ?1) (or $x35 (= ?0 ?1))) $x45)) (= $x39 $x48)))) +(let ((@x56 (monotonicity (monotonicity @x50 (= (and $x31 $x39) $x51)) (= $x41 (= $x28 $x51))))) +(let ((@x64 (quant-intro (trans @x56 (rewrite (= (= $x28 $x51) $x57)) (= $x41 $x57)) (= $x42 $x62)))) +(let ((@x85 (trans @x64 (quant-intro (monotonicity @x77 (= $x57 $x78)) (= $x62 $x81)) (= $x42 $x81)))) +(let ((@x236 (mp~ (mp (asserted $x42) @x85 $x81) (nnf-pos @x232 (~ $x81 $x233)) $x233))) +(let ((@x256 (mp @x236 (quant-intro (monotonicity @x249 (= $x230 $x250)) (= $x233 $x253)) $x253))) +(let ((@x741 (mp (mp @x256 (quant-intro @x289 (= $x253 $x290)) $x290) @x740 $x738))) +(let (($x348 (or (not $x738) $x684))) +(let ((@x685 ((_ quant-inst (nat$ ?x98)) $x348))) +(let ((@x569 (unit-resolution (def-axiom (or $x342 $x697)) (unit-resolution @x685 @x741 $x684) $x697))) +(let (($x125 (not (or $x110 (>= ?x89 1))))) +(let (($x94 (<= 1 ?x89))) +(let (($x95 (=> (prime_nat$ (nat$ (+ ?x90 1))) $x94))) +(let (($x96 (not $x95))) +(let ((@x124 (monotonicity (rewrite (= $x94 (>= ?x89 1))) (= (or $x110 $x94) (or $x110 (>= ?x89 1)))))) +(let ((@x103 (monotonicity (rewrite (= (+ ?x90 1) ?x98)) (= (nat$ (+ ?x90 1)) ?x101)))) +(let ((@x109 (monotonicity (monotonicity @x103 (= (prime_nat$ (nat$ (+ ?x90 1))) $x104)) (= $x95 (=> $x104 $x94))))) +(let ((@x115 (trans @x109 (rewrite (= (=> $x104 $x94) (or $x110 $x94))) (= $x95 (or $x110 $x94))))) +(let ((@x129 (trans (monotonicity @x115 (= $x96 (not (or $x110 $x94)))) (monotonicity @x124 (= (not (or $x110 $x94)) $x125)) (= $x96 $x125)))) +(let ((@x131 (not-or-elim (mp (asserted $x96) @x129 $x125) $x104))) +(let ((@x572 (unit-resolution (unit-resolution (def-axiom (or $x369 $x110 $x487)) @x131 (or $x369 $x487)) @x569 $x487))) +(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))))) +(let ((@x561 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not (= ?x295 0)) (<= ?x295 0))) @x530 (not (= ?x295 0))))) +(let (($x575 (= ?x295 0))) +(let (($x577 (or $x610 $x575))) +(let (($x756 (forall ((?v0 Int) )(! (let ((?x140 (nat$ ?v0))) +(let ((?x141 (of_nat$ ?x140))) +(let (($x169 (= ?x141 0))) +(let (($x155 (>= ?v0 0))) +(or $x155 $x169))))) :pattern ( (nat$ ?v0) ) :qid k!14)) +)) +(let (($x192 (forall ((?v0 Int) )(! (let ((?x140 (nat$ ?v0))) +(let ((?x141 (of_nat$ ?x140))) +(let (($x169 (= ?x141 0))) +(let (($x155 (>= ?v0 0))) +(or $x155 $x169))))) :qid k!14)) +)) +(let ((?x140 (nat$ ?0))) +(let ((?x141 (of_nat$ ?x140))) +(let (($x169 (= ?x141 0))) +(let (($x155 (>= ?0 0))) +(let (($x189 (or $x155 $x169))) +(let (($x171 (forall ((?v0 Int) )(! (let ((?x140 (nat$ ?v0))) +(let ((?x141 (of_nat$ ?x140))) +(let (($x169 (= ?x141 0))) +(let (($x168 (< ?v0 0))) +(=> $x168 $x169))))) :qid k!14)) +)) +(let (($x177 (forall ((?v0 Int) )(! (let ((?x140 (nat$ ?v0))) +(let ((?x141 (of_nat$ ?x140))) +(let (($x169 (= ?x141 0))) +(let (($x168 (< ?v0 0))) +(let (($x173 (not $x168))) +(or $x173 $x169)))))) :qid k!14)) +)) +(let ((@x184 (monotonicity (rewrite (= (< ?0 0) (not $x155))) (= (not (< ?0 0)) (not (not $x155)))))) +(let ((@x188 (trans @x184 (rewrite (= (not (not $x155)) $x155)) (= (not (< ?0 0)) $x155)))) +(let ((@x194 (quant-intro (monotonicity @x188 (= (or (not (< ?0 0)) $x169) $x189)) (= $x177 $x192)))) +(let ((@x176 (rewrite (= (=> (< ?0 0) $x169) (or (not (< ?0 0)) $x169))))) +(let ((@x197 (mp (asserted $x171) (trans (quant-intro @x176 (= $x171 $x177)) @x194 (= $x171 $x192)) $x192))) +(let ((@x761 (mp (mp~ @x197 (nnf-pos (refl (~ $x189 $x189)) (~ $x192 $x192)) $x192) (quant-intro (refl (= $x189 $x189)) (= $x192 $x756)) $x756))) +(let (($x580 (not $x756))) +(let (($x581 (or $x580 $x610 $x575))) +(let ((@x612 (rewrite (= (>= ?x98 0) $x610)))) +(let ((@x579 (monotonicity @x612 (= (or (>= ?x98 0) $x575) $x577)))) +(let ((@x555 (monotonicity @x579 (= (or $x580 (or (>= ?x98 0) $x575)) (or $x580 $x577))))) +(let ((@x564 (trans @x555 (rewrite (= (or $x580 $x577) $x581)) (= (or $x580 (or (>= ?x98 0) $x575)) $x581)))) +(let ((@x565 (mp ((_ quant-inst (+ 1 ?x90)) (or $x580 (or (>= ?x98 0) $x575))) @x564 $x581))) +(let (($x613 (not $x610))) +(let (($x600 (or $x613 $x597))) +(let (($x750 (forall ((?v0 Int) )(! (let ((?x140 (nat$ ?v0))) +(let ((?x141 (of_nat$ ?x140))) +(let (($x142 (= ?x141 ?v0))) +(let (($x155 (>= ?v0 0))) +(let (($x156 (not $x155))) +(or $x156 $x142)))))) :pattern ( (nat$ ?v0) ) :qid k!13)) +)) +(let (($x162 (forall ((?v0 Int) )(! (let ((?x140 (nat$ ?v0))) +(let ((?x141 (of_nat$ ?x140))) +(let (($x142 (= ?x141 ?v0))) +(let (($x155 (>= ?v0 0))) +(let (($x156 (not $x155))) +(or $x156 $x142)))))) :qid k!13)) +)) +(let ((@x752 (refl (= (or (not $x155) (= ?x141 ?0)) (or (not $x155) (= ?x141 ?0)))))) +(let ((@x263 (refl (~ (or (not $x155) (= ?x141 ?0)) (or (not $x155) (= ?x141 ?0)))))) +(let (($x144 (forall ((?v0 Int) )(! (let ((?x140 (nat$ ?v0))) +(let ((?x141 (of_nat$ ?x140))) +(let (($x142 (= ?x141 ?v0))) +(let (($x139 (<= 0 ?v0))) +(=> $x139 $x142))))) :qid k!13)) +)) +(let (($x150 (forall ((?v0 Int) )(! (let ((?x140 (nat$ ?v0))) +(let ((?x141 (of_nat$ ?x140))) +(let (($x142 (= ?x141 ?v0))) +(or (not (<= 0 ?v0)) $x142)))) :qid k!13)) +)) +(let (($x142 (= ?x141 ?0))) +(let (($x156 (not $x155))) +(let (($x159 (or $x156 $x142))) +(let (($x147 (or (not (<= 0 ?0)) $x142))) +(let ((@x158 (monotonicity (rewrite (= (<= 0 ?0) $x155)) (= (not (<= 0 ?0)) $x156)))) +(let ((@x152 (quant-intro (rewrite (= (=> (<= 0 ?0) $x142) $x147)) (= $x144 $x150)))) +(let ((@x166 (trans @x152 (quant-intro (monotonicity @x158 (= $x147 $x159)) (= $x150 $x162)) (= $x144 $x162)))) +(let ((@x266 (mp~ (mp (asserted $x144) @x166 $x162) (nnf-pos @x263 (~ $x162 $x162)) $x162))) +(let ((@x755 (mp @x266 (quant-intro @x752 (= $x162 $x750)) $x750))) +(let (($x603 (not $x750))) +(let (($x604 (or $x603 $x613 $x597))) +(let (($x608 (= ?x295 ?x98))) +(let (($x618 (>= ?x98 0))) +(let (($x619 (not $x618))) +(let (($x609 (or $x619 $x608))) +(let (($x605 (or $x603 $x609))) +(let ((@x602 (monotonicity (monotonicity @x612 (= $x619 $x613)) (rewrite (= $x608 $x597)) (= $x609 $x600)))) +(let ((@x590 (trans (monotonicity @x602 (= $x605 (or $x603 $x600))) (rewrite (= (or $x603 $x600) $x604)) (= $x605 $x604)))) +(let ((@x591 (mp ((_ quant-inst (+ 1 ?x90)) $x605) @x590 $x604))) +(let ((@x532 (unit-resolution (unit-resolution @x591 @x755 $x600) (unit-resolution (unit-resolution @x565 @x761 $x577) @x561 $x610) $x597))) +(let ((@x133 (not-or-elim (mp (asserted $x96) @x129 $x125) (not (>= ?x89 1))))) +((_ 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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + +9e3a7cb6b1687db90ac27c1322f4180e0715e89a 7 0 +unsat +( +a1 +a169 +a170 +a94 +) +0f29eff8af0baceae4a69ea0ceff00e3a8c44aaf 7 0 +unsat +( +a0 +a1 +a3 +a4 +) +2f309a4750090c04f284fbecb4a976eedaa46ce9 7 0 +unsat +( +a95 +a173 +a5 +a179 +) +e0764188710d396d7c3d8c7ed12e92df610f3d5d 6 0 +unsat +( +a0 +a2 +a3 +) +ff18566d8fd433a50da07b998b8d9915d4e6d38c 7 0 +unsat +( +a0 +a1 +a2 +a3 +) +85b5e78e459667d6880efd720fc8258c1f632634 5 0 +unsat +( +a0 +a2 +) +d9da06f46916827de91e55898f12e162fc4394a9 5 0 +unsat +( +a0 +a2 +) +0c5b279548a729dbbc42ad3281942c493cea61a9 2 0 +unknown +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +f38355a9ae0344ba7fe2a48aa18389448f4b9cd2 2 0 +unknown +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +bbdbbe6715d50b1bf20ff06d778334d19ea80167 5 0 +unsat +( +a0 +a1 +) +933c14ef800372ac93564be5a3ef60dc447e5229 5 0 +unsat +( +a2 +a3 +) +b2b6ec8367faf6099e2eb37a31144e974fe80a4d 5 0 +unsat +( +a0 +a1 +) +7d3ccc6fd748dc986de65f6b96355c1acc61633a 5 0 +unsat +( +a0 +a1 +) +502c6566fddc9f002ef331f2822f70acfc1eb0a6 2 0 +sat +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +9a7dd691b0176ee4885324369fa4400bb78fa856 2 0 +sat +(error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +5dee863399bac5f53042e3459e153dff890dd2a5 4 0 +unsat +( +a0 +) diff -r d425bdf419f5 -r 5ff9fe3fee66 src/HOL/SMT_Examples/SMT_Examples.thy --- a/src/HOL/SMT_Examples/SMT_Examples.thy Thu Jul 27 15:22:35 2017 +0100 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy Fri Jul 28 15:36:32 2017 +0100 @@ -378,6 +378,32 @@ using assms by (metis mult_le_0_iff) +subsection {* Linear arithmetic for natural numbers *} + +declare [[smt_nat_as_int]] + +lemma "2 * (x::nat) \ 1" by smt + +lemma "a < 3 \ (7::nat) > 2 * a" by smt + +lemma "let x = (1::nat) + y in x - y > 0 * x" by smt + +lemma + "let x = (1::nat) + y in + let P = (if x > 0 then True else False) in + False \ P = (x - 1 = y) \ (\P \ False)" + by smt + +lemma "int (nat \x::int\) = \x\" by smt + +definition prime_nat :: "nat \ bool" where + "prime_nat p = (1 < p \ (\m. m dvd p --> m = 1 \ m = p))" + +lemma "prime_nat (4*m + 1) \ m \ (1::nat)" by (smt prime_nat_def) + +declare [[smt_nat_as_int = false]] + + section \Pairs\ lemma "fst (x, y) = a \ x = a" diff -r d425bdf419f5 -r 5ff9fe3fee66 src/HOL/SMT_Examples/SMT_Tests.thy --- a/src/HOL/SMT_Examples/SMT_Tests.thy Thu Jul 27 15:22:35 2017 +0100 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy Fri Jul 28 15:36:32 2017 +0100 @@ -222,6 +222,123 @@ by smt+ +section {* Natural numbers *} + +declare [[smt_nat_as_int]] + +lemma + "(0::nat) = 0" + "(1::nat) = 1" + "(0::nat) < 1" + "(0::nat) \ 1" + "(123456789::nat) < 2345678901" + by smt+ + +lemma + "Suc 0 = 1" + "Suc x = x + 1" + "x < Suc x" + "(Suc x = Suc y) = (x = y)" + "Suc (x + y) < Suc x + Suc y" + by smt+ + +lemma + "(x::nat) + 0 = x" + "0 + x = x" + "x + y = y + x" + "x + (y + z) = (x + y) + z" + "(x + y = 0) = (x = 0 \ y = 0)" + by smt+ + +lemma + "(x::nat) - 0 = x" + "x < y \ x - y = 0" + "x - y = 0 \ y - x = 0" + "(x - y) + y = (if x < y then y else x)" + "x - y - z = x - (y + z)" + by smt+ + +lemma + "(x::nat) * 0 = 0" + "0 * x = 0" + "x * 1 = x" + "1 * x = x" + "3 * x = x * 3" + by smt+ + +lemma + "(0::nat) div 0 = 0" + "(x::nat) div 0 = 0" + "(0::nat) div 1 = 0" + "(1::nat) div 1 = 1" + "(3::nat) div 1 = 3" + "(x::nat) div 1 = x" + "(0::nat) div 3 = 0" + "(1::nat) div 3 = 0" + "(3::nat) div 3 = 1" + "(x::nat) div 3 \ x" + "(x div 3 = x) = (x = 0)" + using [[z3_extensions]] + by smt+ + +lemma + "(0::nat) mod 0 = 0" + "(x::nat) mod 0 = x" + "(0::nat) mod 1 = 0" + "(1::nat) mod 1 = 0" + "(3::nat) mod 1 = 0" + "(x::nat) mod 1 = 0" + "(0::nat) mod 3 = 0" + "(1::nat) mod 3 = 1" + "(3::nat) mod 3 = 0" + "x mod 3 < 3" + "(x mod 3 = x) = (x < 3)" + using [[z3_extensions]] + by smt+ + +lemma + "(x::nat) = x div 1 * 1 + x mod 1" + "x = x div 3 * 3 + x mod 3" + using [[z3_extensions]] + by smt+ + +lemma + "min (x::nat) y \ x" + "min x y \ y" + "min x y \ x + y" + "z < x \ z < y \ z < min x y" + "min x y = min y x" + "min x 0 = 0" + by smt+ + +lemma + "max (x::nat) y \ x" + "max x y \ y" + "max x y \ (x - y) + (y - x)" + "z > x \ z > y \ z > max x y" + "max x y = max y x" + "max x 0 = x" + by smt+ + +lemma + "0 \ (x::nat)" + "0 < x \ x \ 1 \ x = 1" + "x \ x" + "x \ y \ 3 * x \ 3 * y" + "x < y \ 3 * x < 3 * y" + "x < y \ x \ y" + "(x < y) = (x + 1 \ y)" + "\ (x < x)" + "x \ y \ y \ z \ x \ z" + "x < y \ y \ z \ x \ z" + "x \ y \ y < z \ x \ z" + "x < y \ y < z \ x < z" + "x < y \ y < z \ \ (z < x)" + by smt+ + +declare [[smt_nat_as_int = false]] + + section \Integers\ lemma diff -r d425bdf419f5 -r 5ff9fe3fee66 src/HOL/Tools/SMT/smt_builtin.ML --- a/src/HOL/Tools/SMT/smt_builtin.ML Thu Jul 27 15:22:35 2017 +0100 +++ b/src/HOL/Tools/SMT/smt_builtin.ML Fri Jul 28 15:36:32 2017 +0100 @@ -13,7 +13,7 @@ val add_builtin_typ: SMT_Util.class -> typ * (typ -> string option) * (typ -> int -> string option) -> Context.generic -> Context.generic - val add_builtin_typ_ext: typ * (typ -> bool) -> Context.generic -> + val add_builtin_typ_ext: typ * (Proof.context -> typ -> bool) -> Context.generic -> Context.generic val dest_builtin_typ: Proof.context -> typ -> string option val is_builtin_typ_ext: Proof.context -> typ -> bool @@ -93,7 +93,7 @@ structure Builtins = Generic_Data ( type T = - (typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab * + (Proof.context -> typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab * (term list bfun, bfunr option bfun) btab val empty = ([], Symtab.empty) val extend = I @@ -125,7 +125,7 @@ fun is_builtin_typ_ext ctxt T = (case lookup_builtin_typ ctxt T of SOME (_, Int (f, _)) => is_some (f T) - | SOME (_, Ext f) => f T + | SOME (_, Ext f) => f ctxt T | NONE => false) diff -r d425bdf419f5 -r 5ff9fe3fee66 src/HOL/Tools/SMT/smt_config.ML --- a/src/HOL/Tools/SMT/smt_config.ML Thu Jul 27 15:22:35 2017 +0100 +++ b/src/HOL/Tools/SMT/smt_config.ML Fri Jul 28 15:36:32 2017 +0100 @@ -32,6 +32,7 @@ val statistics: bool Config.T val monomorph_limit: int Config.T val monomorph_instances: int Config.T + val nat_as_int: bool Config.T val infer_triggers: bool Config.T val debug_files: string Config.T val sat_solver: string Config.T @@ -179,6 +180,7 @@ val statistics = Attrib.setup_config_bool @{binding smt_statistics} (K false) val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10) val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500) +val nat_as_int = Attrib.setup_config_bool @{binding smt_nat_as_int} (K false) val infer_triggers = Attrib.setup_config_bool @{binding smt_infer_triggers} (K false) val debug_files = Attrib.setup_config_string @{binding smt_debug_files} (K "") val sat_solver = Attrib.setup_config_string @{binding smt_sat_solver} (K "cdclite") diff -r d425bdf419f5 -r 5ff9fe3fee66 src/HOL/Tools/SMT/smt_normalize.ML --- a/src/HOL/Tools/SMT/smt_normalize.ML Thu Jul 27 15:22:35 2017 +0100 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Fri Jul 28 15:36:32 2017 +0100 @@ -327,6 +327,85 @@ end +(** embedding of standard natural number operations into integer operations **) + +local + val nat_embedding = @{thms nat_int' int_nat_nneg int_nat_neg} + + val simple_nat_ops = [ + @{const less (nat)}, @{const less_eq (nat)}, + @{const Suc}, @{const plus (nat)}, @{const minus (nat)}] + + val mult_nat_ops = + [@{const times (nat)}, @{const divide (nat)}, @{const modulo (nat)}] + + val nat_ops = simple_nat_ops @ mult_nat_ops + + val nat_consts = nat_ops @ [@{const numeral (nat)}, + @{const zero_class.zero (nat)}, @{const one_class.one (nat)}] + + val nat_int_coercions = [@{const of_nat (int)}, @{const nat}] + + val builtin_nat_ops = nat_int_coercions @ simple_nat_ops + + val is_nat_const = member (op aconv) nat_consts + + fun is_nat_const' @{const of_nat (int)} = true + | is_nat_const' t = is_nat_const t + + val expands = map mk_meta_eq @{thms nat_zero_as_int nat_one_as_int nat_numeral_as_int + nat_less_as_int nat_leq_as_int Suc_as_int nat_plus_as_int nat_minus_as_int nat_times_as_int + nat_div_as_int nat_mod_as_int} + + val ints = map mk_meta_eq @{thms of_nat_0 of_nat_1 int_Suc int_plus int_minus of_nat_mult zdiv_int + zmod_int} + val int_if = mk_meta_eq @{lemma "int (if P then n else m) = (if P then int n else int m)" by simp} + + fun mk_number_eq ctxt i lhs = + let + val eq = SMT_Util.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i) + val ctxt' = put_simpset HOL_ss ctxt addsimps @{thms of_nat_numeral} + val tac = HEADGOAL (Simplifier.simp_tac ctxt') + in Goal.norm_result ctxt (Goal.prove_internal ctxt [] eq (K tac)) end + + fun ite_conv cv1 cv2 = + Conv.combination_conv (Conv.combination_conv (Conv.arg_conv cv1) cv2) cv2 + + fun int_conv ctxt ct = + (case Thm.term_of ct of + @{const of_nat (int)} $ (n as (@{const numeral (nat)} $ _)) => + Conv.rewr_conv (mk_number_eq ctxt (snd (HOLogic.dest_number n)) ct) + | @{const of_nat (int)} $ _ => + (Conv.rewrs_conv ints then_conv Conv.sub_conv ints_conv ctxt) else_conv + (Conv.rewr_conv int_if then_conv + ite_conv (nat_conv ctxt) (int_conv ctxt)) else_conv + Conv.sub_conv (Conv.top_sweep_conv nat_conv) ctxt + | _ => Conv.no_conv) ct + + and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt + + and expand_conv ctxt = + SMT_Util.if_conv (is_nat_const o Term.head_of) + (expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt) (int_conv ctxt) + + and nat_conv ctxt = SMT_Util.if_exists_conv is_nat_const' (Conv.top_sweep_conv expand_conv ctxt) + + val uses_nat_int = Term.exists_subterm (member (op aconv) nat_int_coercions) +in + +val nat_as_int_conv = nat_conv + +fun add_nat_embedding thms = + if exists (uses_nat_int o Thm.prop_of) thms then (thms, nat_embedding) else (thms, []) + +val setup_nat_as_int = + SMT_Builtin.add_builtin_typ_ext (@{typ nat}, + fn ctxt => K (Config.get ctxt SMT_Config.nat_as_int)) #> + fold (SMT_Builtin.add_builtin_fun_ext' o Term.dest_Const) builtin_nat_ops + +end + + (** normalize numerals **) local @@ -359,23 +438,27 @@ (** combined unfoldings and rewritings **) -fun unfold_conv ctxt = - rewrite_case_bool_conv ctxt then_conv - unfold_abs_min_max_conv ctxt then_conv - Thm.beta_conversion true - -fun unfold_polymorph ctxt = map (apsnd (Conv.fconv_rule (unfold_conv ctxt))) -fun unfold_monomorph ctxt = map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt))) - - -(* overall normalization *) - fun burrow_ids f ithms = let val (is, thms) = split_list ithms val (thms', extra_thms) = f thms in (is ~~ thms') @ map (pair ~1) extra_thms end +fun unfold_conv ctxt = + rewrite_case_bool_conv ctxt then_conv + unfold_abs_min_max_conv ctxt then_conv + (if Config.get ctxt SMT_Config.nat_as_int then nat_as_int_conv ctxt + else Conv.all_conv) then_conv + Thm.beta_conversion true + +fun unfold_polymorph ctxt = map (apsnd (Conv.fconv_rule (unfold_conv ctxt))) +fun unfold_monomorph ctxt = + map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt))) + #> Config.get ctxt SMT_Config.nat_as_int ? burrow_ids add_nat_embedding + + +(* overall normalization *) + type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list structure Extra_Norms = Generic_Data @@ -439,6 +522,7 @@ setup_unfolded_quants #> setup_trigger #> setup_case_bool #> - setup_abs_min_max)) + setup_abs_min_max #> + setup_nat_as_int)) end;