# HG changeset patch
# User blanchet
# Date 1406488295 -7200
# Node ID fb71c6f100f814d82a840a12d4480164b8448139
# Parent  987c9ceeaafd40ff14a3215ef53d223fbaacd4a8
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly

diff -r 987c9ceeaafd -r fb71c6f100f8 src/HOL/SMT2.thy
--- a/src/HOL/SMT2.thy	Sun Jul 27 15:44:08 2014 +0200
+++ b/src/HOL/SMT2.thy	Sun Jul 27 21:11:35 2014 +0200
@@ -13,15 +13,15 @@
 
 text {*
 Some SMT solvers support patterns as a quantifier instantiation
-heuristics.  Patterns may either be positive terms (tagged by "pat")
+heuristics. Patterns may either be positive terms (tagged by "pat")
 triggering quantifier instantiations -- when the solver finds a
 term matching a positive pattern, it instantiates the corresponding
 quantifier accordingly -- or negative terms (tagged by "nopat")
-inhibiting quantifier instantiations.  A list of patterns
+inhibiting quantifier instantiations. A list of patterns
 of the same kind is called a multipattern, and all patterns in a
 multipattern are considered conjunctively for quantifier instantiation.
 A list of multipatterns is called a trigger, and their multipatterns
-act disjunctively during quantifier instantiation.  Each multipattern
+act disjunctively during quantifier instantiation. Each multipattern
 should mention at least all quantified variables of the preceding
 quantifier block.
 *}
@@ -46,7 +46,7 @@
 
 text {*
 Application is made explicit for constants occurring with varying
-numbers of arguments.  This is achieved by the introduction of the
+numbers of arguments. This is achieved by the introduction of the
 following constant.
 *}
 
@@ -54,7 +54,7 @@
 
 text {*
 Some solvers support a theory of arrays which can be used to encode
-higher-order functions.  The following set of lemmas specifies the
+higher-order functions. The following set of lemmas specifies the
 properties of such (extensional) arrays.
 *}
 
@@ -66,26 +66,6 @@
 lemma case_bool_if[abs_def]: "case_bool x y P = (if P then x else y)"
   by simp
 
-lemma nat_int': "\<forall>n. nat (int n) = n" by simp
-lemma int_nat_nneg: "\<forall>i. i \<ge> 0 \<longrightarrow> int (nat i) = i" by simp
-lemma int_nat_neg: "\<forall>i. i < 0 \<longrightarrow> int (nat i) = 0" by simp
-
-lemma nat_zero_as_int: "0 = nat 0" by simp
-lemma nat_one_as_int: "1 = nat 1" by simp
-lemma nat_numeral_as_int: "numeral = (\<lambda>i. nat (numeral i))" by simp
-lemma nat_less_as_int: "op < = (\<lambda>a b. int a < int b)" by simp
-lemma nat_leq_as_int: "op \<le> = (\<lambda>a b. int a <= int b)" by simp
-lemma Suc_as_int: "Suc = (\<lambda>a. nat (int a + 1))" by (rule ext) simp
-lemma nat_plus_as_int: "op + = (\<lambda>a b. nat (int a + int b))" by (rule ext)+ simp
-lemma nat_minus_as_int: "op - = (\<lambda>a b. nat (int a - int b))" by (rule ext)+ simp
-lemma nat_times_as_int: "op * = (\<lambda>a b. nat (int a * int b))" by (simp add: nat_mult_distrib)
-lemma nat_div_as_int: "op div = (\<lambda>a b. nat (int a div int b))" by (simp add: nat_div_distrib)
-lemma nat_mod_as_int: "op mod = (\<lambda>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
-
 lemmas Ex1_def_raw = Ex1_def[abs_def]
 lemmas Ball_def_raw = Ball_def[abs_def]
 lemmas Bex_def_raw = Bex_def[abs_def]
@@ -154,15 +134,14 @@
 *}
 
 
-
 subsection {* General configuration options *}
 
 text {*
 The option @{text smt2_solver} can be used to change the target SMT
-solver.  The possible values can be obtained from the @{text smt2_status}
+solver. The possible values can be obtained from the @{text smt2_status}
 command.
 
-Due to licensing restrictions, Z3 is not enabled by default.  Z3 is free
+Due to licensing restrictions, Z3 is not enabled by default. Z3 is free
 for non-commercial applications and can be enabled by setting Isabelle
 system option @{text z3_non_commercial} to @{text yes}.
 *}
@@ -170,15 +149,14 @@
 declare [[smt2_solver = z3]]
 
 text {*
-Since SMT solvers are potentially non-terminating, there is a timeout
-(given in seconds) to restrict their runtime.  A value greater than
-120 (seconds) is in most cases not advisable.
+Since SMT solvers are potentially nonterminating, there is a timeout
+(given in seconds) to restrict their runtime.
 *}
 
 declare [[smt2_timeout = 20]]
 
 text {*
-SMT solvers apply randomized heuristics.  In case a problem is not
+SMT solvers apply randomized heuristics. In case a problem is not
 solvable by an SMT solver, changing the following option might help.
 *}
 
@@ -186,16 +164,16 @@
 
 text {*
 In general, the binding to SMT solvers runs as an oracle, i.e, the SMT
-solvers are fully trusted without additional checks.  The following
+solvers are fully trusted without additional checks. The following
 option can cause the SMT solver to run in proof-producing mode, giving
-a checkable certificate.  This is currently only implemented for Z3.
+a checkable certificate. This is currently only implemented for Z3.
 *}
 
 declare [[smt2_oracle = false]]
 
 text {*
 Each SMT solver provides several commandline options to tweak its
-behaviour.  They can be passed to the solver by setting the following
+behaviour. They can be passed to the solver by setting the following
 options.
 *}
 
@@ -207,14 +185,14 @@
 The SMT method provides an inference mechanism to detect simple triggers
 in quantified formulas, which might increase the number of problems
 solvable by SMT solvers (note: triggers guide quantifier instantiations
-in the SMT solver).  To turn it on, set the following option.
+in the SMT solver). To turn it on, set the following option.
 *}
 
 declare [[smt2_infer_triggers = false]]
 
 text {*
 Enable the following option to use built-in support for div/mod, datatypes,
-and records in Z3.  Currently, this is implemented only in oracle mode.
+and records in Z3. Currently, this is implemented only in oracle mode.
 *}
 
 declare [[z3_new_extensions = false]]
@@ -227,9 +205,9 @@
 all following applications of an SMT solver a cached in that file.
 Any further application of the same SMT solver (using the very same
 configuration) re-uses the cached certificate instead of invoking the
-solver.  An empty string disables caching certificates.
+solver. An empty string disables caching certificates.
 
-The filename should be given as an explicit path.  It is good
+The filename should be given as an explicit path. It is good
 practice to use the name of the current theory (with ending
 @{text ".certs"} instead of @{text ".thy"}) as the certificates file.
 Certificate files should be used at most once in a certain theory context,
@@ -241,7 +219,7 @@
 text {*
 The option @{text smt2_read_only_certificates} controls whether only
 stored certificates are should be used or invocation of an SMT solver
-is allowed.  When set to @{text true}, no SMT solver will ever be
+is allowed. When set to @{text true}, no SMT solver will ever be
 invoked and only the existing certificates found in the configured
 cache are used;  when set to @{text false} and there is no cached
 certificate for some proposition, then the configured SMT solver is
@@ -251,11 +229,10 @@
 declare [[smt2_read_only_certificates = false]]
 
 
-
 subsection {* Tracing *}
 
 text {*
-The SMT method, when applied, traces important information.  To
+The SMT method, when applied, traces important information. To
 make it entirely silent, set the following option to @{text false}.
 *}
 
@@ -273,7 +250,7 @@
 subsection {* Schematic rules for Z3 proof reconstruction *}
 
 text {*
-Several prof rules of Z3 are not very well documented.  There are two
+Several prof rules of Z3 are not very well documented. There are two
 lemma groups which can turn failing Z3 proof reconstruction attempts
 into succeeding ones: the facts in @{text z3_rule} are tried prior to
 any implemented reconstruction procedure for all uncertain Z3 proof
diff -r 987c9ceeaafd -r fb71c6f100f8 src/HOL/SMT_Examples/SMT_Examples.certs2
--- a/src/HOL/SMT_Examples/SMT_Examples.certs2	Sun Jul 27 15:44:08 2014 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs2	Sun Jul 27 21:11:35 2014 +0200
@@ -3600,6 +3600,33 @@
 (let ((@x73 (not-or-elim @x70 $x62)))
 (unit-resolution (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x65 (not $x62))) @x73 $x65) @x74 false))))))))))))))))))
 
+271390ea915947de195c2202e30f90bb84689d60 26 0
+unsat
+((set-logic <null>)
+(proof
+(let ((?x35 (+ y$ 1)))
+(let ((?x36 (* a$ ?x35)))
+(let ((?x34 (* a$ x$)))
+(let ((?x37 (+ ?x34 ?x36)))
+(let ((?x30 (+ x$ 1)))
+(let ((?x32 (+ ?x30 y$)))
+(let ((?x33 (* a$ ?x32)))
+(let (($x38 (= ?x33 ?x37)))
+(let (($x39 (not $x38)))
+(let (($x82 (= (= (+ a$ ?x34 (* a$ y$)) (+ a$ ?x34 (* a$ y$))) true)))
+(let (($x80 (= $x38 (= (+ a$ ?x34 (* a$ y$)) (+ a$ ?x34 (* a$ y$))))))
+(let ((@x76 (rewrite (= (+ ?x34 (+ a$ (* a$ y$))) (+ a$ ?x34 (* a$ y$))))))
+(let ((@x66 (monotonicity (rewrite (= ?x35 (+ 1 y$))) (= ?x36 (* a$ (+ 1 y$))))))
+(let ((@x71 (trans @x66 (rewrite (= (* a$ (+ 1 y$)) (+ a$ (* a$ y$)))) (= ?x36 (+ a$ (* a$ y$))))))
+(let ((@x78 (trans (monotonicity @x71 (= ?x37 (+ ?x34 (+ a$ (* a$ y$))))) @x76 (= ?x37 (+ a$ ?x34 (* a$ y$))))))
+(let ((@x58 (rewrite (= (* a$ (+ 1 x$ y$)) (+ a$ ?x34 (* a$ y$))))))
+(let ((@x46 (monotonicity (rewrite (= ?x30 (+ 1 x$))) (= ?x32 (+ (+ 1 x$) y$)))))
+(let ((@x51 (trans @x46 (rewrite (= (+ (+ 1 x$) y$) (+ 1 x$ y$))) (= ?x32 (+ 1 x$ y$)))))
+(let ((@x60 (trans (monotonicity @x51 (= ?x33 (* a$ (+ 1 x$ y$)))) @x58 (= ?x33 (+ a$ ?x34 (* a$ y$))))))
+(let ((@x88 (monotonicity (trans (monotonicity @x60 @x78 $x80) (rewrite $x82) (= $x38 true)) (= $x39 (not true)))))
+(let ((@x92 (trans @x88 (rewrite (= (not true) false)) (= $x39 false))))
+(mp (asserted $x39) @x92 false))))))))))))))))))))))))
+
 d98ad8f668dead6f610669a52351ea0176a811b0 26 0
 unsat
 ((set-logic <null>)
@@ -3627,33 +3654,6 @@
 (let ((@x73 (and-elim (not-or-elim (mp (asserted $x35) @x69 $x65) $x52) $x49)))
 ((_ th-lemma arith farkas 1 1 1) @x73 @x72 @x74 false))))))))))))))))))))))))
 
-271390ea915947de195c2202e30f90bb84689d60 26 0
-unsat
-((set-logic <null>)
-(proof
-(let ((?x35 (+ y$ 1)))
-(let ((?x36 (* a$ ?x35)))
-(let ((?x34 (* a$ x$)))
-(let ((?x37 (+ ?x34 ?x36)))
-(let ((?x30 (+ x$ 1)))
-(let ((?x32 (+ ?x30 y$)))
-(let ((?x33 (* a$ ?x32)))
-(let (($x38 (= ?x33 ?x37)))
-(let (($x39 (not $x38)))
-(let (($x82 (= (= (+ a$ ?x34 (* a$ y$)) (+ a$ ?x34 (* a$ y$))) true)))
-(let (($x80 (= $x38 (= (+ a$ ?x34 (* a$ y$)) (+ a$ ?x34 (* a$ y$))))))
-(let ((@x76 (rewrite (= (+ ?x34 (+ a$ (* a$ y$))) (+ a$ ?x34 (* a$ y$))))))
-(let ((@x66 (monotonicity (rewrite (= ?x35 (+ 1 y$))) (= ?x36 (* a$ (+ 1 y$))))))
-(let ((@x71 (trans @x66 (rewrite (= (* a$ (+ 1 y$)) (+ a$ (* a$ y$)))) (= ?x36 (+ a$ (* a$ y$))))))
-(let ((@x78 (trans (monotonicity @x71 (= ?x37 (+ ?x34 (+ a$ (* a$ y$))))) @x76 (= ?x37 (+ a$ ?x34 (* a$ y$))))))
-(let ((@x58 (rewrite (= (* a$ (+ 1 x$ y$)) (+ a$ ?x34 (* a$ y$))))))
-(let ((@x46 (monotonicity (rewrite (= ?x30 (+ 1 x$))) (= ?x32 (+ (+ 1 x$) y$)))))
-(let ((@x51 (trans @x46 (rewrite (= (+ (+ 1 x$) y$) (+ 1 x$ y$))) (= ?x32 (+ 1 x$ y$)))))
-(let ((@x60 (trans (monotonicity @x51 (= ?x33 (* a$ (+ 1 x$ y$)))) @x58 (= ?x33 (+ a$ ?x34 (* a$ y$))))))
-(let ((@x88 (monotonicity (trans (monotonicity @x60 @x78 $x80) (rewrite $x82) (= $x38 true)) (= $x39 (not true)))))
-(let ((@x92 (trans @x88 (rewrite (= (not true) false)) (= $x39 false))))
-(mp (asserted $x39) @x92 false))))))))))))))))))))))))
-
 b216c79478e44396acca3654b76845499fc18a04 23 0
 unsat
 ((set-logic <null>)
@@ -3730,842 +3730,6 @@
 (let ((@x152 (trans (monotonicity @x145 (= $x52 (not true))) (rewrite (= (not true) false)) (= $x52 false))))
 (mp (asserted $x52) @x152 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) )))
-))
-(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)))))))
-))
-(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))))))
-))
-(let (($x59 (forall ((?v0 Int) )(let ((?x49 (nat$ ?v0)))
-(let ((?x50 (of_nat$ ?x49)))
-(let (($x51 (= ?x50 ?v0)))
-(or (not (<= 0 ?v0)) $x51)))))
-))
-(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) )))
-))
-(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))))))
-))
-(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))))))
-))
-(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)))))))
-))
-(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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-
-1c2b6530334930f2f4f6e0d6b73f1d249b6c5fd8 22 0
-unsat
-((set-logic AUFLIA)
-(proof
-(let ((?x28 (of_nat$ a$)))
-(let (($x57 (>= ?x28 4)))
-(let (($x64 (not (or (>= ?x28 3) (not $x57)))))
-(let (($x34 (< (* 2 ?x28) 7)))
-(let (($x30 (< ?x28 3)))
-(let (($x38 (not $x30)))
-(let (($x39 (or $x38 $x34)))
-(let ((@x51 (monotonicity (rewrite (= $x30 (not (>= ?x28 3)))) (= $x38 (not (not (>= ?x28 3)))))))
-(let ((@x55 (trans @x51 (rewrite (= (not (not (>= ?x28 3))) (>= ?x28 3))) (= $x38 (>= ?x28 3)))))
-(let ((@x63 (monotonicity @x55 (rewrite (= $x34 (not $x57))) (= $x39 (or (>= ?x28 3) (not $x57))))))
-(let ((@x44 (monotonicity (rewrite (= (=> $x30 $x34) $x39)) (= (not (=> $x30 $x34)) (not $x39)))))
-(let ((@x68 (trans @x44 (monotonicity @x63 (= (not $x39) $x64)) (= (not (=> $x30 $x34)) $x64))))
-(let ((@x71 (not-or-elim (mp (asserted (not (=> $x30 $x34))) @x68 $x64) $x57)))
-(let (($x58 (not $x57)))
-(let (($x47 (>= ?x28 3)))
-(let (($x45 (not $x47)))
-(let ((@x70 (not-or-elim (mp (asserted (not (=> $x30 $x34))) @x68 $x64) $x45)))
-(unit-resolution (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x58 $x47)) @x70 $x58) @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) )))
-))
-(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))))))
-))
-(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))))))
-))
-(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)))))))
-))
-(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) )))
-))
-(let (($x77 (forall ((?v0 Nat$) )(= (nat$ (of_nat$ ?v0)) ?v0))
-))
-(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) )))
-))
-(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)))))))
-))
-(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))))))
-))
-(let (($x91 (forall ((?v0 Int) )(let ((?x81 (nat$ ?v0)))
-(let ((?x82 (of_nat$ ?x81)))
-(let (($x83 (= ?x82 ?v0)))
-(or (not (<= 0 ?v0)) $x83)))))
-))
-(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 (not $x551) $x248)) @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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-
-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) )))
-))
-(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))))))
-))
-(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))))))
-))
-(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)))))))
-))
-(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) )))
-))
-(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)))))))
-))
-(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))))))
-))
-(let (($x125 (forall ((?v0 Int) )(let ((?x115 (nat$ ?v0)))
-(let ((?x116 (of_nat$ ?x115)))
-(let (($x117 (= ?x116 ?v0)))
-(or (not (<= 0 ?v0)) $x117)))))
-))
-(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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-
-8704d70b06a6aa746ec0e023752eaa0b7eb0df18 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) )))
-))
-(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)))))))
-))
-(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))))))
-))
-(let (($x100 (forall ((?v0 Int) )(let ((?x90 (nat$ ?v0)))
-(let ((?x91 (of_nat$ ?x90)))
-(let (($x92 (= ?x91 ?v0)))
-(or (not (<= 0 ?v0)) $x92)))))
-))
-(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)))))))))))))))))))))))))))))))))))))))))))))))))))))))
-
-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$))))) )))
-))
-(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) )))
-))
-(let (($x200 (not $x28)))
-(not (or (not (or $x200 (not (or $x65 (not $x710))))) (not $x245))))))))))) :pattern ( (prime_nat$ ?v0) ) :pattern ( (of_nat$ ?v0) )))
-))
-(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)))))
-))
-(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)))))))))))))))
-))
-(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) )))
-))
-(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)))))
-))
-(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)))))
-))
-(let (($x66 (not $x65)))
-(let (($x75 (and $x66 $x72)))
-(let (($x200 (not $x28)))
-(let (($x229 (or $x200 $x75)))
-(and $x229 $x245)))))))))))))
-))
-(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)))))
-))
-(let (($x75 (and $x66 $x72)))
-(let (($x200 (not $x28)))
-(let (($x229 (or $x200 $x75)))
-(and $x229 $x228)))))))))))))))
-))
-(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)))))
-))
-(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))))))))
-))
-(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)))))
-))
-(let ((?x30 (of_nat$ ?v0)))
-(let (($x31 (< 1 ?x30)))
-(let (($x28 (prime_nat$ ?v0)))
-(= $x28 (and $x31 $x39)))))))
-))
-(let (($x62 (forall ((?v0 Nat$) )(let (($x48 (forall ((?v1 Nat$) )(or (not (dvd$ ?v1 ?v0)) (or (= ?v1 (nat$ 1)) (= ?v1 ?v0))))
-))
-(let ((?x30 (of_nat$ ?v0)))
-(let (($x31 (< 1 ?x30)))
-(let (($x51 (and $x31 $x48)))
-(let (($x28 (prime_nat$ ?v0)))
-(= $x28 $x51)))))))
-))
-(let (($x78 (= $x28 $x75)))
-(let (($x48 (forall ((?v1 Nat$) )(or (not (dvd$ ?v1 ?0)) (or (= ?v1 (nat$ 1)) (= ?v1 ?0))))
-))
-(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)))))
-))
-(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) )))
-))
-(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))))))
-))
-(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))))))
-))
-(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)))))))
-))
-(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) )))
-))
-(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)))))))
-))
-(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))))))
-))
-(let (($x150 (forall ((?v0 Int) )(let ((?x140 (nat$ ?v0)))
-(let ((?x141 (of_nat$ ?x140)))
-(let (($x142 (= ?x141 ?v0)))
-(or (not (<= 0 ?v0)) $x142)))))
-))
-(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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-
 5e90e9139eb4e9a7c2678bca8dda6cda05861f4c 23 0
 unsat
 ((set-logic AUFLIA)
@@ -4780,21 +3944,6 @@
 (let ((@x53 (trans (monotonicity @x46 (= $x33 (not true))) (rewrite (= (not true) false)) (= $x33 false))))
 (mp (asserted $x33) @x53 false)))))))))))
 
-8b09776b03122aeacc9dd9526e1f0e5d41a07f14 14 0
-unsat
-((set-logic AUFLIA)
-(proof
-(let (($x29 (forall ((?v0 A$) )(g$ ?v0))
-))
-(let (($x30 (ite $x29 true false)))
-(let (($x31 (f$ $x30)))
-(let (($x32 (=> $x31 true)))
-(let (($x33 (not $x32)))
-(let ((@x42 (monotonicity (monotonicity (rewrite (= $x30 $x29)) (= $x31 (f$ $x29))) (= $x32 (=> (f$ $x29) true)))))
-(let ((@x46 (trans @x42 (rewrite (= (=> (f$ $x29) true) true)) (= $x32 true))))
-(let ((@x53 (trans (monotonicity @x46 (= $x33 (not true))) (rewrite (= (not true) false)) (= $x33 false))))
-(mp (asserted $x33) @x53 false)))))))))))
-
 b221de9d8dbe279344ac85e2ada07f5722636ce5 46 0
 unsat
 ((set-logic AUFLIA)
@@ -4842,195 +3991,96 @@
 (let ((@x478 (mp ((_ quant-inst 3 42) (or (not $x52) $x171)) (trans (monotonicity @x131 $x137) (rewrite (= $x134 $x134)) $x137) $x134)))
 (unit-resolution (unit-resolution @x478 @x78 $x168) (mp @x77 @x472 (not $x168)) false)))))))))))))))))))))))))))))))))))
 
-c94d83d8571ae767bf6025c563cdac64250f7638 189 0
+8b09776b03122aeacc9dd9526e1f0e5d41a07f14 14 0
+unsat
+((set-logic AUFLIA)
+(proof
+(let (($x29 (forall ((?v0 A$) )(g$ ?v0))
+))
+(let (($x30 (ite $x29 true false)))
+(let (($x31 (f$ $x30)))
+(let (($x32 (=> $x31 true)))
+(let (($x33 (not $x32)))
+(let ((@x42 (monotonicity (monotonicity (rewrite (= $x30 $x29)) (= $x31 (f$ $x29))) (= $x32 (=> (f$ $x29) true)))))
+(let ((@x46 (trans @x42 (rewrite (= (=> (f$ $x29) true) true)) (= $x32 true))))
+(let ((@x53 (trans (monotonicity @x46 (= $x33 (not true))) (rewrite (= (not true) false)) (= $x33 false))))
+(mp (asserted $x33) @x53 false)))))))))))
+
+5d3ccbcf168a634cad3952ad8f6d2798329d6a77 75 0
 unsat
 ((set-logic AUFLIA)
 (proof
-(let ((?x74 (nat$ 2)))
-(let ((?x75 (cons$ ?x74 nil$)))
-(let ((?x69 (nat$ 1)))
-(let ((?x76 (cons$ ?x69 ?x75)))
-(let ((?x70 (cons$ ?x69 nil$)))
-(let ((?x68 (nat$ 0)))
-(let ((?x71 (cons$ ?x68 ?x70)))
-(let ((?x72 (map$ uu$ ?x71)))
-(let (($x77 (= ?x72 ?x76)))
-(let ((?x264 (map$ uu$ ?x70)))
-(let ((?x427 (map$ uu$ nil$)))
-(let ((?x426 (fun_app$ uu$ ?x69)))
-(let ((?x428 (cons$ ?x426 ?x427)))
-(let (($x429 (= ?x264 ?x428)))
-(let (($x598 (forall ((?v0 Nat_nat_fun$) (?v1 Nat$) (?v2 Nat_list$) )(!(let ((?x64 (cons$ (fun_app$ ?v0 ?v1) (map$ ?v0 ?v2))))
-(let ((?x61 (map$ ?v0 (cons$ ?v1 ?v2))))
-(= ?x61 ?x64))) :pattern ( (map$ ?v0 (cons$ ?v1 ?v2)) ) :pattern ( (cons$ (fun_app$ ?v0 ?v1) (map$ ?v0 ?v2)) )))
+(let ((?x78 (cons$ 2 nil$)))
+(let ((?x79 (cons$ 1 ?x78)))
+(let ((?x74 (cons$ 1 nil$)))
+(let ((?x75 (cons$ 0 ?x74)))
+(let ((?x76 (map$ uu$ ?x75)))
+(let (($x80 (= ?x76 ?x79)))
+(let ((?x185 (map$ uu$ ?x74)))
+(let ((?x189 (map$ uu$ nil$)))
+(let ((?x188 (fun_app$ uu$ 1)))
+(let ((?x160 (cons$ ?x188 ?x189)))
+(let (($x290 (= ?x185 ?x160)))
+(let (($x521 (forall ((?v0 Int_int_fun$) (?v1 Int) (?v2 Int_list$) )(!(= (map$ ?v0 (cons$ ?v1 ?v2)) (cons$ (fun_app$ ?v0 ?v1) (map$ ?v0 ?v2))) :pattern ( (map$ ?v0 (cons$ ?v1 ?v2)) ) :pattern ( (cons$ (fun_app$ ?v0 ?v1) (map$ ?v0 ?v2)) )))
 ))
-(let (($x66 (forall ((?v0 Nat_nat_fun$) (?v1 Nat$) (?v2 Nat_list$) )(let ((?x64 (cons$ (fun_app$ ?v0 ?v1) (map$ ?v0 ?v2))))
-(let ((?x61 (map$ ?v0 (cons$ ?v1 ?v2))))
-(= ?x61 ?x64))))
-))
-(let ((?x64 (cons$ (fun_app$ ?2 ?1) (map$ ?2 ?0))))
-(let ((?x61 (map$ ?2 (cons$ ?1 ?0))))
-(let (($x65 (= ?x61 ?x64)))
-(let ((@x158 (mp~ (asserted $x66) (nnf-pos (refl (~ $x65 $x65)) (~ $x66 $x66)) $x66)))
-(let ((@x603 (mp @x158 (quant-intro (refl (= $x65 $x65)) (= $x66 $x598)) $x598)))
-(let (($x582 (not $x598)))
-(let (($x524 (or $x582 $x429)))
-(let ((@x511 ((_ quant-inst uu$ (nat$ 1) nil$) $x524)))
-(let (($x515 (= ?x427 nil$)))
-(let (($x590 (forall ((?v0 Nat_nat_fun$) )(!(= (map$ ?v0 nil$) nil$) :pattern ( (map$ ?v0 nil$) )))
-))
-(let (($x55 (forall ((?v0 Nat_nat_fun$) )(= (map$ ?v0 nil$) nil$))
+(let (($x72 (forall ((?v0 Int_int_fun$) (?v1 Int) (?v2 Int_list$) )(= (map$ ?v0 (cons$ ?v1 ?v2)) (cons$ (fun_app$ ?v0 ?v1) (map$ ?v0 ?v2))))
 ))
-(let ((@x592 (refl (= (= (map$ ?0 nil$) nil$) (= (map$ ?0 nil$) nil$)))))
-(let ((@x152 (refl (~ (= (map$ ?0 nil$) nil$) (= (map$ ?0 nil$) nil$)))))
-(let ((@x595 (mp (mp~ (asserted $x55) (nnf-pos @x152 (~ $x55 $x55)) $x55) (quant-intro @x592 (= $x55 $x590)) $x590)))
-(let (($x506 (or (not $x590) $x515)))
-(let ((@x507 ((_ quant-inst uu$) $x506)))
-(let ((?x281 (of_nat$ ?x69)))
-(let ((?x516 (+ 1 ?x281)))
-(let ((?x517 (nat$ ?x516)))
-(let (($x508 (= ?x426 ?x517)))
-(let (($x47 (forall ((?v0 Nat$) )(!(let ((?x29 (fun_app$ uu$ ?v0)))
-(= ?x29 (nat$ (+ 1 (of_nat$ ?v0))))) :pattern ( (fun_app$ uu$ ?v0) )))
-))
-(let ((?x29 (fun_app$ uu$ ?0)))
-(let (($x44 (= ?x29 (nat$ (+ 1 (of_nat$ ?0))))))
-(let (($x36 (forall ((?v0 Nat$) )(!(let ((?x29 (fun_app$ uu$ ?v0)))
-(= ?x29 (nat$ (+ (of_nat$ ?v0) 1)))) :pattern ( (fun_app$ uu$ ?v0) )))
+(let (($x71 (= (map$ ?2 (cons$ ?1 ?0)) (cons$ (fun_app$ ?2 ?1) (map$ ?2 ?0)))))
+(let ((@x97 (mp~ (asserted $x72) (nnf-pos (refl (~ $x71 $x71)) (~ $x72 $x72)) $x72)))
+(let ((@x526 (mp @x97 (quant-intro (refl (= $x71 $x71)) (= $x72 $x521)) $x521)))
+(let (($x173 (or (not $x521) $x290)))
+(let ((@x506 ((_ quant-inst uu$ 1 nil$) $x173)))
+(let (($x492 (= ?x189 nil$)))
+(let (($x513 (forall ((?v0 Int_int_fun$) )(!(= (map$ ?v0 nil$) nil$) :pattern ( (map$ ?v0 nil$) )))
 ))
-(let ((@x43 (monotonicity (rewrite (= (+ (of_nat$ ?0) 1) (+ 1 (of_nat$ ?0)))) (= (nat$ (+ (of_nat$ ?0) 1)) (nat$ (+ 1 (of_nat$ ?0)))))))
-(let ((@x46 (monotonicity @x43 (= (= ?x29 (nat$ (+ (of_nat$ ?0) 1))) $x44))))
-(let ((@x156 (mp~ (mp (asserted $x36) (quant-intro @x46 (= $x36 $x47)) $x47) (nnf-pos (refl (~ $x44 $x44)) (~ $x47 $x47)) $x47)))
-(let (($x494 (or (not $x47) $x508)))
-(let ((@x495 ((_ quant-inst (nat$ 1)) $x494)))
-(let ((?x445 (of_nat$ ?x517)))
-(let ((?x376 (nat$ ?x445)))
-(let (($x377 (= ?x376 ?x517)))
-(let (($x605 (forall ((?v0 Nat$) )(!(= (nat$ (of_nat$ ?v0)) ?v0) :pattern ( (of_nat$ ?v0) )))
-))
-(let (($x82 (forall ((?v0 Nat$) )(= (nat$ (of_nat$ ?v0)) ?v0))
+(let (($x61 (forall ((?v0 Int_int_fun$) )(= (map$ ?v0 nil$) nil$))
 ))
-(let ((@x610 (trans (rewrite (= $x82 $x605)) (rewrite (= $x605 $x605)) (= $x82 $x605))))
-(let ((@x162 (refl (~ (= (nat$ (of_nat$ ?0)) ?0) (= (nat$ (of_nat$ ?0)) ?0)))))
-(let ((@x611 (mp (mp~ (asserted $x82) (nnf-pos @x162 (~ $x82 $x82)) $x82) @x610 $x605)))
-(let (($x384 (or (not $x605) $x377)))
-(let ((@x385 ((_ quant-inst (nat$ ?x516)) $x384)))
-(let ((?x437 (* (- 1) ?x445)))
-(let ((?x410 (+ ?x281 ?x437)))
-(let (($x431 (<= ?x410 (- 1))))
-(let (($x378 (= ?x410 (- 1))))
-(let (($x448 (>= ?x281 (- 1))))
-(let (($x442 (>= ?x281 1)))
-(let (($x282 (= ?x281 1)))
-(let (($x613 (forall ((?v0 Int) )(!(let (($x88 (= (of_nat$ (nat$ ?v0)) ?v0)))
-(let (($x101 (>= ?v0 0)))
-(let (($x102 (not $x101)))
-(or $x102 $x88)))) :pattern ( (nat$ ?v0) )))
-))
-(let (($x108 (forall ((?v0 Int) )(let (($x88 (= (of_nat$ (nat$ ?v0)) ?v0)))
-(let (($x101 (>= ?v0 0)))
-(let (($x102 (not $x101)))
-(or $x102 $x88)))))
+(let ((@x515 (refl (= (= (map$ ?0 nil$) nil$) (= (map$ ?0 nil$) nil$)))))
+(let ((@x83 (refl (~ (= (map$ ?0 nil$) nil$) (= (map$ ?0 nil$) nil$)))))
+(let ((@x518 (mp (mp~ (asserted $x61) (nnf-pos @x83 (~ $x61 $x61)) $x61) (quant-intro @x515 (= $x61 $x513)) $x513)))
+(let (($x495 (or (not $x513) $x492)))
+(let ((@x496 ((_ quant-inst uu$) $x495)))
+(let (($x136 (= ?x188 2)))
+(let (($x51 (forall ((?v0 Int) )(!(= (+ ?v0 (* (- 1) (fun_app$ uu$ ?v0))) (- 1)) :pattern ( (fun_app$ uu$ ?v0) )))
 ))
-(let (($x88 (= (of_nat$ (nat$ ?0)) ?0)))
-(let (($x101 (>= ?0 0)))
-(let (($x102 (not $x101)))
-(let (($x105 (or $x102 $x88)))
-(let (($x90 (forall ((?v0 Int) )(let (($x88 (= (of_nat$ (nat$ ?v0)) ?v0)))
-(let (($x85 (<= 0 ?v0)))
-(=> $x85 $x88))))
+(let (($x47 (= (+ ?0 (* (- 1) (fun_app$ uu$ ?0))) (- 1))))
+(let (($x34 (forall ((?v0 Int) )(!(let ((?x29 (fun_app$ uu$ ?v0)))
+(= ?x29 (+ ?v0 1))) :pattern ( (fun_app$ uu$ ?v0) )))
 ))
-(let (($x96 (forall ((?v0 Int) )(let (($x88 (= (of_nat$ (nat$ ?v0)) ?v0)))
-(or (not (<= 0 ?v0)) $x88)))
+(let (($x42 (forall ((?v0 Int) )(!(let ((?x29 (fun_app$ uu$ ?v0)))
+(= ?x29 (+ 1 ?v0))) :pattern ( (fun_app$ uu$ ?v0) )))
 ))
-(let ((@x104 (monotonicity (rewrite (= (<= 0 ?0) $x101)) (= (not (<= 0 ?0)) $x102))))
-(let ((@x110 (quant-intro (monotonicity @x104 (= (or (not (<= 0 ?0)) $x88) $x105)) (= $x96 $x108))))
-(let ((@x95 (rewrite (= (=> (<= 0 ?0) $x88) (or (not (<= 0 ?0)) $x88)))))
-(let ((@x113 (mp (asserted $x90) (trans (quant-intro @x95 (= $x90 $x96)) @x110 (= $x90 $x108)) $x108)))
-(let ((@x618 (mp (mp~ @x113 (nnf-pos (refl (~ $x105 $x105)) (~ $x108 $x108)) $x108) (quant-intro (refl (= $x105 $x105)) (= $x108 $x613)) $x613)))
-(let (($x227 (not $x613)))
-(let (($x271 (or $x227 $x282)))
-(let ((@x578 (rewrite (= (not true) false))))
-(let ((@x181 (rewrite (= (>= 1 0) true))))
-(let ((@x289 (trans (monotonicity @x181 (= (not (>= 1 0)) (not true))) @x578 (= (not (>= 1 0)) false))))
-(let ((@x560 (monotonicity @x289 (= (or (not (>= 1 0)) $x282) (or false $x282)))))
-(let ((@x270 (trans @x560 (rewrite (= (or false $x282) $x282)) (= (or (not (>= 1 0)) $x282) $x282))))
-(let ((@x552 (monotonicity @x270 (= (or $x227 (or (not (>= 1 0)) $x282)) $x271))))
-(let ((@x555 (trans @x552 (rewrite (= $x271 $x271)) (= (or $x227 (or (not (>= 1 0)) $x282)) $x271))))
-(let ((@x541 (mp ((_ quant-inst 1) (or $x227 (or (not (>= 1 0)) $x282))) @x555 $x271)))
-(let ((@x351 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x282) $x442)) (unit-resolution @x541 @x618 $x282) $x442)))
-(let (($x451 (not $x448)))
-(let (($x409 (or $x227 $x451 $x378)))
-(let (($x446 (= ?x445 ?x516)))
-(let (($x443 (>= ?x516 0)))
-(let (($x444 (not $x443)))
-(let (($x447 (or $x444 $x446)))
-(let (($x411 (or $x227 $x447)))
-(let ((@x441 (monotonicity (monotonicity (rewrite (= $x443 $x448)) (= $x444 $x451)) (rewrite (= $x446 $x378)) (= $x447 (or $x451 $x378)))))
-(let ((@x420 (trans (monotonicity @x441 (= $x411 (or $x227 (or $x451 $x378)))) (rewrite (= (or $x227 (or $x451 $x378)) $x409)) (= $x411 $x409))))
-(let ((@x430 (mp ((_ quant-inst (+ 1 ?x281)) $x411) @x420 $x409)))
-(let ((@x343 (unit-resolution @x430 @x618 (unit-resolution ((_ th-lemma arith farkas 1 1) (or (not $x442) $x448)) @x351 $x448) $x378)))
-(let (($x432 (>= ?x410 (- 1))))
-(let (($x331 (<= ?x281 1)))
-(let ((@x335 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x282) $x331)) (unit-resolution @x541 @x618 $x282) $x331)))
-(let ((@x341 ((_ th-lemma arith eq-propagate -1 -1 1 1) @x351 @x335 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x378) $x432)) @x343 $x432) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x378) $x431)) @x343 $x431) (= ?x445 2))))
-(let ((@x327 (trans (monotonicity (symm @x341 (= 2 ?x445)) (= ?x74 ?x376)) (unit-resolution @x385 @x611 $x377) (= ?x74 ?x517))))
-(let ((@x329 (trans @x327 (symm (unit-resolution @x495 @x156 $x508) (= ?x517 ?x426)) (= ?x74 ?x426))))
-(let ((@x312 (monotonicity @x329 (symm (unit-resolution @x507 @x595 $x515) (= nil$ ?x427)) (= ?x75 ?x428))))
-(let ((@x316 (trans @x312 (symm (unit-resolution @x511 @x603 $x429) (= ?x428 ?x264)) (= ?x75 ?x264))))
-(let ((?x577 (of_nat$ ?x68)))
-(let ((?x522 (+ 1 ?x577)))
-(let ((?x523 (nat$ ?x522)))
-(let ((?x263 (fun_app$ uu$ ?x68)))
-(let (($x512 (= ?x263 ?x523)))
-(let (($x513 (or (not $x47) $x512)))
-(let ((@x514 ((_ quant-inst (nat$ 0)) $x513)))
-(let ((?x496 (of_nat$ ?x523)))
-(let ((?x373 (nat$ ?x496)))
-(let (($x375 (= ?x373 ?x523)))
-(let (($x380 (or (not $x605) $x375)))
-(let ((@x381 ((_ quant-inst (nat$ ?x522)) $x380)))
-(let ((?x490 (* (- 1) ?x577)))
-(let ((?x491 (+ ?x496 ?x490)))
-(let (($x465 (<= ?x491 1)))
-(let (($x492 (= ?x491 1)))
-(let (($x499 (>= ?x577 (- 1))))
-(let (($x502 (>= ?x577 0)))
-(let (($x249 (= ?x577 0)))
-(let (($x228 (or $x227 $x249)))
-(let ((@x584 (rewrite (= (>= 0 0) true))))
-(let ((@x241 (trans (monotonicity @x584 (= (not (>= 0 0)) (not true))) @x578 (= (not (>= 0 0)) false))))
-(let ((@x580 (monotonicity @x241 (= (or (not (>= 0 0)) $x249) (or false $x249)))))
-(let ((@x226 (trans @x580 (rewrite (= (or false $x249) $x249)) (= (or (not (>= 0 0)) $x249) $x249))))
-(let ((@x568 (monotonicity @x226 (= (or $x227 (or (not (>= 0 0)) $x249)) $x228))))
-(let ((@x571 (trans @x568 (rewrite (= $x228 $x228)) (= (or $x227 (or (not (>= 0 0)) $x249)) $x228))))
-(let ((@x208 (mp ((_ quant-inst 0) (or $x227 (or (not (>= 0 0)) $x249))) @x571 $x228)))
-(let ((@x323 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x249) $x502)) (unit-resolution @x208 @x618 $x249) $x502)))
-(let (($x487 (not $x499)))
-(let (($x477 (or $x227 $x487 $x492)))
-(let (($x497 (= ?x496 ?x522)))
-(let (($x509 (>= ?x522 0)))
-(let (($x510 (not $x509)))
-(let (($x498 (or $x510 $x497)))
-(let (($x478 (or $x227 $x498)))
-(let ((@x476 (monotonicity (monotonicity (rewrite (= $x509 $x499)) (= $x510 $x487)) (rewrite (= $x497 $x492)) (= $x498 (or $x487 $x492)))))
-(let ((@x486 (trans (monotonicity @x476 (= $x478 (or $x227 (or $x487 $x492)))) (rewrite (= (or $x227 (or $x487 $x492)) $x477)) (= $x478 $x477))))
-(let ((@x464 (mp ((_ quant-inst (+ 1 ?x577)) $x478) @x486 $x477)))
-(let ((@x304 (unit-resolution @x464 @x618 (unit-resolution ((_ th-lemma arith farkas 1 1) (or (not $x502) $x499)) @x323 $x499) $x492)))
-(let (($x466 (>= ?x491 1)))
-(let (($x504 (<= ?x577 0)))
-(let ((@x298 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x249) $x504)) (unit-resolution @x208 @x618 $x249) $x504)))
-(let ((@x300 ((_ th-lemma arith eq-propagate -1 -1 -1 -1) @x323 @x298 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x492) $x466)) @x304 $x466) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x492) $x465)) @x304 $x465) (= ?x496 1))))
-(let ((@x294 (trans (monotonicity (symm @x300 (= 1 ?x496)) (= ?x69 ?x373)) (unit-resolution @x381 @x611 $x375) (= ?x69 ?x523))))
-(let ((@x273 (trans @x294 (symm (unit-resolution @x514 @x156 $x512) (= ?x523 ?x263)) (= ?x69 ?x263))))
-(let ((@x279 (symm (monotonicity @x273 @x316 (= ?x76 (cons$ ?x263 ?x264))) (= (cons$ ?x263 ?x264) ?x76))))
-(let ((?x265 (cons$ ?x263 ?x264)))
-(let (($x266 (= ?x72 ?x265)))
-(let (($x237 (or $x582 $x266)))
-(let ((@x367 ((_ quant-inst uu$ (nat$ 0) (cons$ ?x69 nil$)) $x237)))
-(let (($x78 (not $x77)))
-(let ((@x79 (asserted $x78)))
-(unit-resolution @x79 (trans (unit-resolution @x367 @x603 $x266) @x279 $x77) false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(let ((@x53 (quant-intro (rewrite (= (= (fun_app$ uu$ ?0) (+ 1 ?0)) $x47)) (= $x42 $x51))))
+(let ((?x29 (fun_app$ uu$ ?0)))
+(let (($x39 (= ?x29 (+ 1 ?0))))
+(let ((@x41 (monotonicity (rewrite (= (+ ?0 1) (+ 1 ?0))) (= (= ?x29 (+ ?0 1)) $x39))))
+(let ((@x56 (mp (asserted $x34) (trans (quant-intro @x41 (= $x34 $x42)) @x53 (= $x34 $x51)) $x51)))
+(let ((@x85 (mp~ @x56 (nnf-pos (refl (~ $x47 $x47)) (~ $x51 $x51)) $x51)))
+(let (($x145 (not $x51)))
+(let (($x499 (or $x145 $x136)))
+(let ((@x498 (rewrite (= (= (+ 1 (* (- 1) ?x188)) (- 1)) $x136))))
+(let ((@x204 (monotonicity @x498 (= (or $x145 (= (+ 1 (* (- 1) ?x188)) (- 1))) $x499))))
+(let ((@x207 (trans @x204 (rewrite (= $x499 $x499)) (= (or $x145 (= (+ 1 (* (- 1) ?x188)) (- 1))) $x499))))
+(let ((@x104 (mp ((_ quant-inst 1) (or $x145 (= (+ 1 (* (- 1) ?x188)) (- 1)))) @x207 $x499)))
+(let ((@x191 (monotonicity (symm (unit-resolution @x104 @x85 $x136) (= 2 ?x188)) (symm (unit-resolution @x496 @x518 $x492) (= nil$ ?x189)) (= ?x78 ?x160))))
+(let ((@x473 (trans @x191 (symm (unit-resolution @x506 @x526 $x290) (= ?x160 ?x185)) (= ?x78 ?x185))))
+(let ((?x182 (fun_app$ uu$ 0)))
+(let (($x163 (= ?x182 1)))
+(let (($x487 (or $x145 $x163)))
+(let ((@x501 (monotonicity (rewrite (= (+ 0 (* (- 1) ?x182)) (* (- 1) ?x182))) (= (= (+ 0 (* (- 1) ?x182)) (- 1)) (= (* (- 1) ?x182) (- 1))))))
+(let ((@x503 (trans @x501 (rewrite (= (= (* (- 1) ?x182) (- 1)) $x163)) (= (= (+ 0 (* (- 1) ?x182)) (- 1)) $x163))))
+(let ((@x151 (monotonicity @x503 (= (or $x145 (= (+ 0 (* (- 1) ?x182)) (- 1))) $x487))))
+(let ((@x490 (trans @x151 (rewrite (= $x487 $x487)) (= (or $x145 (= (+ 0 (* (- 1) ?x182)) (- 1))) $x487))))
+(let ((@x491 (mp ((_ quant-inst 0) (or $x145 (= (+ 0 (* (- 1) ?x182)) (- 1)))) @x490 $x487)))
+(let ((@x478 (monotonicity (symm (unit-resolution @x491 @x85 $x163) (= 1 ?x182)) @x473 (= ?x79 (cons$ ?x182 ?x185)))))
+(let ((?x186 (cons$ ?x182 ?x185)))
+(let (($x187 (= ?x76 ?x186)))
+(let (($x504 (or (not $x521) $x187)))
+(let ((@x505 ((_ quant-inst uu$ 0 (cons$ 1 nil$)) $x504)))
+(let ((@x466 (trans (unit-resolution @x505 @x526 $x187) (symm @x478 (= ?x186 ?x79)) $x80)))
+(let (($x81 (not $x80)))
+(let ((@x82 (asserted $x81)))
+(unit-resolution @x82 @x466 false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 
 40c61a0200976d6203302a7343af5b7ad1e6ce36 11 0
 unsat
@@ -5044,533 +4094,452 @@
 (let ((@x42 (trans (monotonicity (rewrite (= $x31 true)) (= $x32 (not true))) (rewrite (= (not true) false)) (= $x32 false))))
 (mp (asserted $x32) @x42 false))))))))
 
-825fdd8f086b9606c3db6feacf7565b92faf5ae2 190 0
+f17a5e4d5f1a5a93fbc847f858c7c845c29d8349 109 0
 unsat
 ((set-logic AUFLIA)
 (proof
-(let ((?x87 (nat$ 6)))
-(let ((?x80 (nat$ 4)))
-(let ((?x81 (dec_10$ ?x80)))
-(let ((?x82 (of_nat$ ?x81)))
-(let ((?x83 (* 4 ?x82)))
-(let ((?x84 (nat$ ?x83)))
-(let ((?x85 (dec_10$ ?x84)))
-(let (($x88 (= ?x85 ?x87)))
-(let ((?x461 (dec_10$ ?x87)))
-(let (($x421 (= ?x461 ?x87)))
-(let ((?x487 (of_nat$ ?x87)))
-(let ((?x464 (+ (- 10) ?x487)))
-(let ((?x447 (nat$ ?x464)))
-(let ((?x389 (dec_10$ ?x447)))
-(let (($x448 (= ?x461 ?x389)))
-(let (($x460 (>= ?x487 10)))
-(let (($x449 (ite $x460 $x448 $x421)))
-(let (($x602 (forall ((?v0 Nat$) )(!(let ((?x29 (of_nat$ ?v0)))
-(let (($x60 (>= ?x29 10)))
-(ite $x60 (= (dec_10$ ?v0) (dec_10$ (nat$ (+ (- 10) ?x29)))) (= (dec_10$ ?v0) ?v0)))) :pattern ( (of_nat$ ?v0) ) :pattern ( (dec_10$ ?v0) )))
+(let ((?x75 (dec_10$ 4)))
+(let ((?x76 (* 4 ?x75)))
+(let ((?x77 (dec_10$ ?x76)))
+(let (($x79 (= ?x77 6)))
+(let (($x150 (<= ?x75 4)))
+(let (($x174 (= ?x75 4)))
+(let (($x513 (forall ((?v0 Int) )(!(let (($x55 (>= ?v0 10)))
+(ite $x55 (= (dec_10$ ?v0) (dec_10$ (+ (- 10) ?v0))) (= (dec_10$ ?v0) ?v0))) :pattern ( (dec_10$ ?v0) )))
 ))
-(let (($x180 (forall ((?v0 Nat$) )(let ((?x29 (of_nat$ ?v0)))
-(let (($x60 (>= ?x29 10)))
-(ite $x60 (= (dec_10$ ?v0) (dec_10$ (nat$ (+ (- 10) ?x29)))) (= (dec_10$ ?v0) ?v0)))))
+(let (($x92 (forall ((?v0 Int) )(let (($x55 (>= ?v0 10)))
+(ite $x55 (= (dec_10$ ?v0) (dec_10$ (+ (- 10) ?v0))) (= (dec_10$ ?v0) ?v0))))
 ))
-(let ((?x29 (of_nat$ ?0)))
-(let (($x60 (>= ?x29 10)))
-(let (($x177 (ite $x60 (= (dec_10$ ?0) (dec_10$ (nat$ (+ (- 10) ?x29)))) (= (dec_10$ ?0) ?0))))
-(let (($x73 (forall ((?v0 Nat$) )(let ((?x46 (dec_10$ (nat$ (+ (- 10) (of_nat$ ?v0))))))
-(let ((?x29 (of_nat$ ?v0)))
-(let (($x60 (>= ?x29 10)))
-(let ((?x65 (ite $x60 ?x46 ?v0)))
-(let ((?x28 (dec_10$ ?v0)))
-(= ?x28 ?x65)))))))
-))
-(let ((?x46 (dec_10$ (nat$ (+ (- 10) ?x29)))))
-(let ((?x65 (ite $x60 ?x46 ?0)))
-(let ((?x28 (dec_10$ ?0)))
-(let (($x70 (= ?x28 ?x65)))
-(let (($x37 (forall ((?v0 Nat$) )(let ((?x29 (of_nat$ ?v0)))
-(let (($x31 (< ?x29 10)))
+(let (($x55 (>= ?0 10)))
+(let (($x87 (ite $x55 (= (dec_10$ ?0) (dec_10$ (+ (- 10) ?0))) (= (dec_10$ ?0) ?0))))
+(let (($x68 (forall ((?v0 Int) )(let ((?x38 (+ (- 10) ?v0)))
+(let ((?x41 (dec_10$ ?x38)))
+(let (($x55 (>= ?v0 10)))
+(let ((?x60 (ite $x55 ?x41 ?v0)))
 (let ((?x28 (dec_10$ ?v0)))
-(= ?x28 (ite $x31 ?v0 (dec_10$ (nat$ (- ?x29 10)))))))))
-))
-(let (($x55 (forall ((?v0 Nat$) )(let ((?x46 (dec_10$ (nat$ (+ (- 10) (of_nat$ ?v0))))))
-(let ((?x29 (of_nat$ ?v0)))
-(let (($x31 (< ?x29 10)))
-(let ((?x49 (ite $x31 ?v0 ?x46)))
-(let ((?x28 (dec_10$ ?v0)))
-(= ?x28 ?x49)))))))
+(= ?x28 ?x60)))))))
 ))
-(let ((@x64 (monotonicity (rewrite (= (< ?x29 10) (not $x60))) (= (ite (< ?x29 10) ?0 ?x46) (ite (not $x60) ?0 ?x46)))))
-(let ((@x69 (trans @x64 (rewrite (= (ite (not $x60) ?0 ?x46) ?x65)) (= (ite (< ?x29 10) ?0 ?x46) ?x65))))
-(let ((@x72 (monotonicity @x69 (= (= ?x28 (ite (< ?x29 10) ?0 ?x46)) $x70))))
-(let (($x31 (< ?x29 10)))
-(let ((?x49 (ite $x31 ?0 ?x46)))
-(let (($x52 (= ?x28 ?x49)))
-(let ((@x45 (monotonicity (rewrite (= (- ?x29 10) (+ (- 10) ?x29))) (= (nat$ (- ?x29 10)) (nat$ (+ (- 10) ?x29))))))
-(let ((@x51 (monotonicity (monotonicity @x45 (= (dec_10$ (nat$ (- ?x29 10))) ?x46)) (= (ite $x31 ?0 (dec_10$ (nat$ (- ?x29 10)))) ?x49))))
-(let ((@x54 (monotonicity @x51 (= (= ?x28 (ite $x31 ?0 (dec_10$ (nat$ (- ?x29 10))))) $x52))))
-(let ((@x77 (trans (quant-intro @x54 (= $x37 $x55)) (quant-intro @x72 (= $x55 $x73)) (= $x37 $x73))))
-(let ((@x161 (mp~ (mp (asserted $x37) @x77 $x73) (nnf-pos (refl (~ $x70 $x70)) (~ $x73 $x73)) $x73)))
-(let ((@x183 (mp @x161 (quant-intro (rewrite (= $x70 $x177)) (= $x73 $x180)) $x180)))
-(let ((@x607 (mp @x183 (quant-intro (refl (= $x177 $x177)) (= $x180 $x602)) $x602)))
-(let (($x256 (not $x602)))
-(let (($x452 (or $x256 $x449)))
-(let ((@x420 ((_ quant-inst (nat$ 6)) $x452)))
-(let (($x385 (not $x460)))
-(let (($x450 (<= ?x487 6)))
-(let (($x488 (= ?x487 6)))
-(let (($x616 (forall ((?v0 Int) )(!(let ((?x97 (nat$ ?v0)))
-(let ((?x98 (of_nat$ ?x97)))
-(let (($x99 (= ?x98 ?v0)))
-(let (($x112 (>= ?v0 0)))
-(let (($x113 (not $x112)))
-(or $x113 $x99)))))) :pattern ( (nat$ ?v0) )))
+(let ((?x38 (+ (- 10) ?0)))
+(let ((?x41 (dec_10$ ?x38)))
+(let ((?x60 (ite $x55 ?x41 ?0)))
+(let ((?x28 (dec_10$ ?0)))
+(let (($x65 (= ?x28 ?x60)))
+(let (($x35 (forall ((?v0 Int) )(let ((?x28 (dec_10$ ?v0)))
+(= ?x28 (ite (< ?v0 10) ?v0 (dec_10$ (- ?v0 10))))))
 ))
-(let (($x119 (forall ((?v0 Int) )(let ((?x97 (nat$ ?v0)))
-(let ((?x98 (of_nat$ ?x97)))
-(let (($x99 (= ?x98 ?v0)))
-(let (($x112 (>= ?v0 0)))
-(let (($x113 (not $x112)))
-(or $x113 $x99)))))))
+(let (($x50 (forall ((?v0 Int) )(let ((?x38 (+ (- 10) ?v0)))
+(let ((?x41 (dec_10$ ?x38)))
+(let (($x30 (< ?v0 10)))
+(let ((?x44 (ite $x30 ?v0 ?x41)))
+(let ((?x28 (dec_10$ ?v0)))
+(= ?x28 ?x44)))))))
 ))
-(let ((?x97 (nat$ ?0)))
-(let ((?x98 (of_nat$ ?x97)))
-(let (($x99 (= ?x98 ?0)))
-(let (($x112 (>= ?0 0)))
-(let (($x113 (not $x112)))
-(let (($x116 (or $x113 $x99)))
-(let (($x101 (forall ((?v0 Int) )(let ((?x97 (nat$ ?v0)))
-(let ((?x98 (of_nat$ ?x97)))
-(let (($x99 (= ?x98 ?v0)))
-(let (($x96 (<= 0 ?v0)))
-(=> $x96 $x99))))))
-))
-(let (($x107 (forall ((?v0 Int) )(let ((?x97 (nat$ ?v0)))
-(let ((?x98 (of_nat$ ?x97)))
-(let (($x99 (= ?x98 ?v0)))
-(or (not (<= 0 ?v0)) $x99)))))
-))
-(let ((@x115 (monotonicity (rewrite (= (<= 0 ?0) $x112)) (= (not (<= 0 ?0)) $x113))))
-(let ((@x121 (quant-intro (monotonicity @x115 (= (or (not (<= 0 ?0)) $x99) $x116)) (= $x107 $x119))))
-(let ((@x106 (rewrite (= (=> (<= 0 ?0) $x99) (or (not (<= 0 ?0)) $x99)))))
-(let ((@x124 (mp (asserted $x101) (trans (quant-intro @x106 (= $x101 $x107)) @x121 (= $x101 $x119)) $x119)))
-(let ((@x621 (mp (mp~ @x124 (nnf-pos (refl (~ $x116 $x116)) (~ $x119 $x119)) $x119) (quant-intro (refl (= $x116 $x116)) (= $x119 $x616)) $x616)))
-(let (($x544 (not $x616)))
-(let (($x480 (or $x544 $x488)))
-(let ((@x491 (rewrite (= (>= 6 0) true))))
-(let ((@x495 (trans (monotonicity @x491 (= (not (>= 6 0)) (not true))) (rewrite (= (not true) false)) (= (not (>= 6 0)) false))))
-(let ((@x475 (monotonicity @x495 (= (or (not (>= 6 0)) $x488) (or false $x488)))))
-(let ((@x479 (trans @x475 (rewrite (= (or false $x488) $x488)) (= (or (not (>= 6 0)) $x488) $x488))))
-(let ((@x465 (monotonicity @x479 (= (or $x544 (or (not (>= 6 0)) $x488)) $x480))))
-(let ((@x468 (trans @x465 (rewrite (= $x480 $x480)) (= (or $x544 (or (not (>= 6 0)) $x488)) $x480))))
-(let ((@x469 (mp ((_ quant-inst 6) (or $x544 (or (not (>= 6 0)) $x488))) @x468 $x480)))
-(let ((@x415 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x488) $x450)) (unit-resolution @x469 @x621 $x488) $x450)))
-(let ((@x386 (unit-resolution (def-axiom (or (not $x449) $x460 $x421)) (unit-resolution ((_ th-lemma arith farkas 1 1) (or (not $x450) $x385)) @x415 $x385) (unit-resolution @x420 @x607 $x449) $x421)))
-(let ((?x251 (of_nat$ ?x80)))
-(let ((?x454 (* (- 1) ?x251)))
-(let ((?x455 (+ ?x82 ?x454)))
-(let (($x456 (<= ?x455 0)))
-(let (($x453 (= ?x82 ?x251)))
-(let (($x238 (= ?x81 ?x80)))
-(let ((?x233 (+ (- 10) ?x251)))
-(let ((?x575 (nat$ ?x233)))
-(let ((?x236 (dec_10$ ?x575)))
-(let (($x237 (= ?x81 ?x236)))
-(let (($x252 (>= ?x251 10)))
-(let (($x239 (ite $x252 $x237 $x238)))
-(let (($x578 (or $x256 $x239)))
-(let ((@x579 ((_ quant-inst (nat$ 4)) $x578)))
-(let (($x581 (not $x252)))
-(let (($x380 (<= ?x251 4)))
-(let (($x563 (= ?x251 4)))
-(let (($x545 (or $x544 $x563)))
-(let ((@x566 (rewrite (= (>= 4 0) true))))
-(let ((@x558 (trans (monotonicity @x566 (= (not (>= 4 0)) (not true))) (rewrite (= (not true) false)) (= (not (>= 4 0)) false))))
-(let ((@x398 (monotonicity @x558 (= (or (not (>= 4 0)) $x563) (or false $x563)))))
-(let ((@x543 (trans @x398 (rewrite (= (or false $x563) $x563)) (= (or (not (>= 4 0)) $x563) $x563))))
-(let ((@x549 (monotonicity @x543 (= (or $x544 (or (not (>= 4 0)) $x563)) $x545))))
-(let ((@x377 (trans @x549 (rewrite (= $x545 $x545)) (= (or $x544 (or (not (>= 4 0)) $x563)) $x545))))
-(let ((@x379 (mp ((_ quant-inst 4) (or $x544 (or (not (>= 4 0)) $x563))) @x377 $x545)))
-(let ((@x393 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x563) $x380)) (unit-resolution @x379 @x621 $x563) $x380)))
-(let ((@x367 (unit-resolution (def-axiom (or (not $x239) $x252 $x238)) (unit-resolution ((_ th-lemma arith farkas 1 1) (or (not $x380) $x581)) @x393 $x581) (unit-resolution @x579 @x607 $x239) $x238)))
-(let ((@x215 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x453) $x456)) (monotonicity @x367 $x453) $x456)))
-(let (($x457 (>= ?x455 0)))
-(let ((@x376 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x453) $x457)) (monotonicity @x367 $x453) $x457)))
-(let (($x536 (>= ?x251 4)))
-(let ((@x362 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x563) $x536)) (unit-resolution @x379 @x621 $x563) $x536)))
-(let ((?x576 (of_nat$ ?x84)))
-(let ((?x439 (* (- 1) ?x576)))
-(let ((?x440 (+ ?x83 ?x439)))
-(let (($x517 (<= ?x440 0)))
-(let (($x438 (= ?x440 0)))
-(let (($x532 (>= ?x82 0)))
-(let ((@x354 (unit-resolution ((_ th-lemma arith assign-bounds 1 1) (or $x532 (not $x536) (not $x457))) @x362 @x376 $x532)))
-(let (($x434 (not $x532)))
-(let (($x533 (or $x434 $x438)))
-(let (($x522 (or $x544 $x434 $x438)))
-(let (($x530 (= ?x576 ?x83)))
-(let (($x529 (>= ?x83 0)))
-(let (($x433 (not $x529)))
-(let (($x531 (or $x433 $x530)))
-(let (($x523 (or $x544 $x531)))
-(let ((@x535 (monotonicity (monotonicity (rewrite (= $x529 $x532)) (= $x433 $x434)) (rewrite (= $x530 $x438)) (= $x531 $x533))))
-(let ((@x528 (trans (monotonicity @x535 (= $x523 (or $x544 $x533))) (rewrite (= (or $x544 $x533) $x522)) (= $x523 $x522))))
-(let ((@x516 (mp ((_ quant-inst (* 4 ?x82)) $x523) @x528 $x522)))
-(let ((@x351 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x438) $x517)) (unit-resolution (unit-resolution @x516 @x621 $x533) @x354 $x438) $x517)))
-(let (($x518 (>= ?x440 0)))
-(let ((@x345 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x438) $x518)) (unit-resolution (unit-resolution @x516 @x621 $x533) @x354 $x438) $x518)))
-(let ((@x349 (monotonicity ((_ th-lemma arith eq-propagate 1 1 -4 -4 -4 -4) @x345 @x351 @x362 @x393 @x376 @x215 (= (+ (- 10) ?x576) 6)) (= (nat$ (+ (- 10) ?x576)) ?x87))))
-(let ((?x574 (+ (- 10) ?x576)))
-(let ((?x278 (nat$ ?x574)))
-(let ((?x292 (dec_10$ ?x278)))
-(let (($x293 (= ?x85 ?x292)))
-(let (($x294 (= ?x85 ?x84)))
-(let (($x577 (>= ?x576 10)))
-(let (($x295 (ite $x577 $x293 $x294)))
-(let (($x568 (or $x256 $x295)))
-(let ((@x299 ((_ quant-inst (nat$ ?x83)) $x568)))
-(let ((@x336 (unit-resolution ((_ th-lemma arith assign-bounds 1 4 4) (or $x577 (not $x517) (not $x536) (not $x457))) @x362 @x351 @x376 $x577)))
-(let ((@x337 (unit-resolution (def-axiom (or (not $x295) (not $x577) $x293)) @x336 (unit-resolution @x299 @x607 $x295) $x293)))
-(let ((@x323 (trans (trans @x337 (monotonicity @x349 (= ?x292 ?x461)) (= ?x85 ?x461)) @x386 $x88)))
-(let (($x89 (not $x88)))
-(let ((@x90 (asserted $x89)))
-(unit-resolution @x90 @x323 false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(let ((@x59 (monotonicity (rewrite (= (< ?0 10) (not $x55))) (= (ite (< ?0 10) ?0 ?x41) (ite (not $x55) ?0 ?x41)))))
+(let ((@x64 (trans @x59 (rewrite (= (ite (not $x55) ?0 ?x41) ?x60)) (= (ite (< ?0 10) ?0 ?x41) ?x60))))
+(let ((@x67 (monotonicity @x64 (= (= ?x28 (ite (< ?0 10) ?0 ?x41)) $x65))))
+(let (($x30 (< ?0 10)))
+(let ((?x44 (ite $x30 ?0 ?x41)))
+(let (($x47 (= ?x28 ?x44)))
+(let ((@x43 (monotonicity (rewrite (= (- ?0 10) ?x38)) (= (dec_10$ (- ?0 10)) ?x41))))
+(let ((@x49 (monotonicity (monotonicity @x43 (= (ite $x30 ?0 (dec_10$ (- ?0 10))) ?x44)) (= (= ?x28 (ite $x30 ?0 (dec_10$ (- ?0 10)))) $x47))))
+(let ((@x72 (trans (quant-intro @x49 (= $x35 $x50)) (quant-intro @x67 (= $x50 $x68)) (= $x35 $x68))))
+(let ((@x86 (mp~ (mp (asserted $x35) @x72 $x68) (nnf-pos (refl (~ $x65 $x65)) (~ $x68 $x68)) $x68)))
+(let ((@x95 (mp @x86 (quant-intro (rewrite (= $x65 $x87)) (= $x68 $x92)) $x92)))
+(let ((@x518 (mp @x95 (quant-intro (refl (= $x87 $x87)) (= $x92 $x513)) $x513)))
+(let (($x501 (not $x513)))
+(let (($x163 (or $x501 $x174)))
+(let ((?x97 (+ (- 10) 4)))
+(let ((?x183 (dec_10$ ?x97)))
+(let (($x184 (= ?x75 ?x183)))
+(let (($x96 (>= 4 10)))
+(let (($x185 (ite $x96 $x184 $x174)))
+(let ((@x172 (monotonicity (monotonicity (rewrite (= ?x97 (- 6))) (= ?x183 (dec_10$ (- 6)))) (= $x184 (= ?x75 (dec_10$ (- 6)))))))
+(let ((@x507 (monotonicity (rewrite (= $x96 false)) @x172 (= $x185 (ite false (= ?x75 (dec_10$ (- 6))) $x174)))))
+(let ((@x511 (trans @x507 (rewrite (= (ite false (= ?x75 (dec_10$ (- 6))) $x174) $x174)) (= $x185 $x174))))
+(let ((@x148 (trans (monotonicity @x511 (= (or $x501 $x185) $x163)) (rewrite (= $x163 $x163)) (= (or $x501 $x185) $x163))))
+(let ((@x149 (mp ((_ quant-inst 4) (or $x501 $x185)) @x148 $x163)))
+(let ((@x438 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x174) $x150)) (unit-resolution @x149 @x518 $x174) $x150)))
+(let (($x151 (>= ?x75 4)))
+(let ((@x428 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x174) $x151)) (unit-resolution @x149 @x518 $x174) $x151)))
+(let ((?x489 (+ (- 10) ?x76)))
+(let ((?x490 (dec_10$ ?x489)))
+(let ((?x448 (* (- 1) ?x490)))
+(let ((?x449 (+ ?x76 ?x448)))
+(let (($x444 (<= ?x449 10)))
+(let (($x292 (= ?x449 10)))
+(let ((?x455 (+ (- 20) ?x76)))
+(let ((?x458 (dec_10$ ?x455)))
+(let (($x461 (= ?x490 ?x458)))
+(let (($x310 (>= ?x75 5)))
+(let (($x450 (ite $x310 $x461 $x292)))
+(let (($x453 (or $x501 $x450)))
+(let (($x470 (= ?x490 ?x489)))
+(let ((?x467 (+ (- 10) ?x489)))
+(let ((?x468 (dec_10$ ?x467)))
+(let (($x469 (= ?x490 ?x468)))
+(let (($x466 (>= ?x489 10)))
+(let (($x471 (ite $x466 $x469 $x470)))
+(let ((@x463 (monotonicity (monotonicity (rewrite (= ?x467 ?x455)) (= ?x468 ?x458)) (= $x469 $x461))))
+(let ((@x452 (monotonicity (rewrite (= $x466 $x310)) @x463 (rewrite (= $x470 $x292)) (= $x471 $x450))))
+(let ((@x442 (trans (monotonicity @x452 (= (or $x501 $x471) $x453)) (rewrite (= $x453 $x453)) (= (or $x501 $x471) $x453))))
+(let ((@x443 (mp ((_ quant-inst (+ (- 10) ?x76)) (or $x501 $x471)) @x442 $x453)))
+(let (($x346 (not $x310)))
+(let ((@x418 (unit-resolution (def-axiom (or (not $x450) $x310 $x292)) (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x346 (not $x150))) @x438 $x346) (or (not $x450) $x292))))
+(let ((@x422 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x292) $x444)) (unit-resolution @x418 (unit-resolution @x443 @x518 $x450) $x292) $x444)))
+(let (($x336 (>= ?x449 10)))
+(let ((@x410 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x292) $x336)) (unit-resolution @x418 (unit-resolution @x443 @x518 $x450) $x292) $x336)))
+(let (($x491 (= ?x77 ?x490)))
+(let ((?x499 (* (- 1) ?x77)))
+(let ((?x485 (+ ?x76 ?x499)))
+(let (($x497 (= ?x485 0)))
+(let (($x131 (>= ?x75 3)))
+(let (($x486 (ite $x131 $x491 $x497)))
+(let (($x205 (or $x501 $x486)))
+(let ((@x204 (monotonicity (rewrite (= (>= ?x76 10) $x131)) (rewrite (= (= ?x77 ?x76) $x497)) (= (ite (>= ?x76 10) $x491 (= ?x77 ?x76)) $x486))))
+(let ((@x479 (monotonicity @x204 (= (or $x501 (ite (>= ?x76 10) $x491 (= ?x77 ?x76))) $x205))))
+(let ((@x212 (trans @x479 (rewrite (= $x205 $x205)) (= (or $x501 (ite (>= ?x76 10) $x491 (= ?x77 ?x76))) $x205))))
+(let ((@x481 (mp ((_ quant-inst (* 4 ?x75)) (or $x501 (ite (>= ?x76 10) $x491 (= ?x77 ?x76)))) @x212 $x205)))
+(let ((@x397 (unit-resolution (def-axiom (or (not $x486) (not $x131) $x491)) (unit-resolution ((_ th-lemma arith farkas 1 1) (or (not $x151) $x131)) @x428 $x131) (unit-resolution @x481 @x518 $x486) $x491)))
+(let (($x80 (not $x79)))
+(let ((@x81 (asserted $x80)))
+(unit-resolution @x81 (trans @x397 ((_ th-lemma arith eq-propagate 1 1 -4 -4) @x410 @x422 @x428 @x438 (= ?x490 6)) $x79) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 
-f8d23ebbeac7f77a32b969922f558052d0057659 336 0
+fa62bf7228a50eb8c663092f87f9af7c25feaffe 336 0
 unsat
 ((set-logic <null>)
 (proof
-(let ((?x102 (mod$ l$ 2)))
-(let ((?x99 (map$ uu$ xs$)))
-(let ((?x100 (eval_dioph$ ks$ ?x99)))
-(let ((?x101 (mod$ ?x100 2)))
-(let (($x103 (= ?x101 ?x102)))
-(let ((?x96 (eval_dioph$ ks$ xs$)))
-(let (($x98 (= ?x96 l$)))
-(let ((?x113 (* (- 1) ?x100)))
-(let ((?x114 (+ l$ ?x113)))
-(let ((?x117 (div$ ?x114 2)))
-(let ((?x104 (map$ uua$ xs$)))
-(let ((?x105 (eval_dioph$ ks$ ?x104)))
-(let (($x120 (= ?x105 ?x117)))
-(let (($x364 (not $x120)))
-(let (($x363 (not $x103)))
-(let (($x365 (or $x363 $x364)))
-(let ((?x849 (div ?x96 2)))
-(let ((?x1076 (* (- 1) ?x849)))
-(let ((?x804 (mod ?x96 2)))
-(let ((?x831 (* (- 1) ?x804)))
-(let ((?x621 (mod l$ 2)))
-(let ((?x648 (* (- 1) ?x621)))
-(let (($x1078 (>= (+ l$ ?x102 ?x648 (* (- 1) (div l$ 2)) ?x831 ?x1076) 1)))
-(let ((?x475 (* (- 1) l$)))
-(let ((?x798 (+ ?x96 ?x475)))
-(let (($x800 (>= ?x798 0)))
-(let (($x874 (not $x800)))
-(let (($x799 (<= ?x798 0)))
-(let ((?x791 (+ ?x105 (* (- 1) ?x117))))
-(let (($x792 (<= ?x791 0)))
-(let (($x366 (not $x365)))
-(let ((@x583 (hypothesis $x366)))
-(let ((@x577 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x364 $x792)) (unit-resolution (def-axiom (or $x365 $x120)) @x583 $x120) $x792)))
-(let ((?x542 (+ l$ ?x113 (* (- 2) (div ?x114 2)) (* (- 1) (mod (+ l$ ?x100) 2)))))
-(let (($x548 (>= ?x542 0)))
-(let (($x539 (= ?x542 0)))
+(let ((?x99 (mod$ l$ 2)))
+(let ((?x96 (map$ uu$ xs$)))
+(let ((?x97 (eval_dioph$ ks$ ?x96)))
+(let ((?x98 (mod$ ?x97 2)))
+(let (($x100 (= ?x98 ?x99)))
+(let ((?x93 (eval_dioph$ ks$ xs$)))
+(let (($x95 (= ?x93 l$)))
+(let ((?x110 (* (- 1) ?x97)))
+(let ((?x111 (+ l$ ?x110)))
+(let ((?x114 (div$ ?x111 2)))
+(let ((?x101 (map$ uua$ xs$)))
+(let ((?x102 (eval_dioph$ ks$ ?x101)))
+(let (($x117 (= ?x102 ?x114)))
+(let (($x282 (not $x117)))
+(let (($x281 (not $x100)))
+(let (($x283 (or $x281 $x282)))
+(let ((?x744 (div ?x93 2)))
+(let ((?x970 (* (- 1) ?x744)))
+(let ((?x699 (mod ?x93 2)))
+(let ((?x726 (* (- 1) ?x699)))
+(let ((?x516 (mod l$ 2)))
+(let ((?x543 (* (- 1) ?x516)))
+(let (($x972 (>= (+ l$ ?x99 ?x543 (* (- 1) (div l$ 2)) ?x726 ?x970) 1)))
+(let ((?x369 (* (- 1) l$)))
+(let ((?x693 (+ ?x93 ?x369)))
+(let (($x695 (>= ?x693 0)))
+(let (($x857 (not $x695)))
+(let (($x694 (<= ?x693 0)))
+(let ((?x686 (+ ?x102 (* (- 1) ?x114))))
+(let (($x687 (<= ?x686 0)))
+(let (($x284 (not $x283)))
+(let ((@x837 (hypothesis $x284)))
+(let ((@x591 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x282 $x687)) (unit-resolution (def-axiom (or $x283 $x117)) @x837 $x117) $x687)))
+(let ((?x437 (+ l$ ?x110 (* (- 2) (div ?x111 2)) (* (- 1) (mod (+ l$ ?x97) 2)))))
+(let (($x443 (>= ?x437 0)))
+(let (($x434 (= ?x437 0)))
 (let ((@x26 (true-axiom true)))
-(let ((@x898 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x539) $x548)) (unit-resolution ((_ th-lemma arith) (or false $x539)) @x26 $x539) $x548)))
-(let ((?x606 (* (- 2) ?x105)))
-(let ((?x607 (+ ?x96 ?x113 ?x606)))
-(let (($x614 (<= ?x607 0)))
-(let (($x608 (= ?x607 0)))
-(let (($x386 (forall ((?v0 Int_list$) (?v1 Nat_list$) )(!(let ((?x48 (eval_dioph$ ?v0 ?v1)))
-(let ((?x86 (+ ?x48 (* (- 1) (eval_dioph$ ?v0 (map$ uu$ ?v1))) (* (- 2) (eval_dioph$ ?v0 (map$ uua$ ?v1))))))
-(= ?x86 0))) :pattern ( (eval_dioph$ ?v0 (map$ uu$ ?v1)) ) :pattern ( (eval_dioph$ ?v0 (map$ uua$ ?v1)) )))
+(let ((@x793 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x434) $x443)) (unit-resolution ((_ th-lemma arith) (or false $x434)) @x26 $x434) $x443)))
+(let ((?x501 (* (- 2) ?x102)))
+(let ((?x502 (+ ?x93 ?x110 ?x501)))
+(let (($x509 (<= ?x502 0)))
+(let (($x503 (= ?x502 0)))
+(let (($x304 (forall ((?v0 Int_list$) (?v1 Int_list$) )(!(let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?v0 (map$ uu$ ?v1))) (* (- 2) (eval_dioph$ ?v0 (map$ uua$ ?v1))))))
+(= ?x83 0))) :pattern ( (eval_dioph$ ?v0 (map$ uu$ ?v1)) ) :pattern ( (eval_dioph$ ?v0 (map$ uua$ ?v1)) )))
 ))
-(let (($x88 (forall ((?v0 Int_list$) (?v1 Nat_list$) )(let ((?x48 (eval_dioph$ ?v0 ?v1)))
-(let ((?x86 (+ ?x48 (* (- 1) (eval_dioph$ ?v0 (map$ uu$ ?v1))) (* (- 2) (eval_dioph$ ?v0 (map$ uua$ ?v1))))))
-(= ?x86 0))))
+(let (($x85 (forall ((?v0 Int_list$) (?v1 Int_list$) )(let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?v0 (map$ uu$ ?v1))) (* (- 2) (eval_dioph$ ?v0 (map$ uua$ ?v1))))))
+(= ?x83 0))))
 ))
-(let ((?x48 (eval_dioph$ ?1 ?0)))
-(let ((?x86 (+ ?x48 (* (- 1) (eval_dioph$ ?1 (map$ uu$ ?0))) (* (- 2) (eval_dioph$ ?1 (map$ uua$ ?0))))))
-(let (($x82 (= ?x86 0)))
-(let (($x61 (forall ((?v0 Int_list$) (?v1 Nat_list$) )(let ((?x48 (eval_dioph$ ?v0 ?v1)))
-(let ((?x51 (eval_dioph$ ?v0 (map$ uu$ ?v1))))
-(let ((?x59 (+ (* (eval_dioph$ ?v0 (map$ uua$ ?v1)) 2) ?x51)))
-(= ?x59 ?x48)))))
+(let ((?x45 (eval_dioph$ ?1 ?0)))
+(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?1 (map$ uu$ ?0))) (* (- 2) (eval_dioph$ ?1 (map$ uua$ ?0))))))
+(let (($x79 (= ?x83 0)))
+(let (($x58 (forall ((?v0 Int_list$) (?v1 Int_list$) )(let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x48 (eval_dioph$ ?v0 (map$ uu$ ?v1))))
+(let ((?x56 (+ (* (eval_dioph$ ?v0 (map$ uua$ ?v1)) 2) ?x48)))
+(= ?x56 ?x45)))))
 ))
-(let (($x77 (forall ((?v0 Int_list$) (?v1 Nat_list$) )(let ((?x48 (eval_dioph$ ?v0 ?v1)))
-(let ((?x57 (eval_dioph$ ?v0 (map$ uua$ ?v1))))
-(let ((?x63 (* 2 ?x57)))
-(let ((?x51 (eval_dioph$ ?v0 (map$ uu$ ?v1))))
-(let ((?x69 (+ ?x51 ?x63)))
-(= ?x69 ?x48)))))))
+(let (($x74 (forall ((?v0 Int_list$) (?v1 Int_list$) )(let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x54 (eval_dioph$ ?v0 (map$ uua$ ?v1))))
+(let ((?x60 (* 2 ?x54)))
+(let ((?x48 (eval_dioph$ ?v0 (map$ uu$ ?v1))))
+(let ((?x66 (+ ?x48 ?x60)))
+(= ?x66 ?x45)))))))
 ))
-(let ((?x57 (eval_dioph$ ?1 (map$ uua$ ?0))))
-(let ((?x63 (* 2 ?x57)))
-(let ((?x51 (eval_dioph$ ?1 (map$ uu$ ?0))))
-(let ((?x69 (+ ?x51 ?x63)))
-(let (($x74 (= ?x69 ?x48)))
-(let ((@x68 (monotonicity (rewrite (= (* ?x57 2) ?x63)) (= (+ (* ?x57 2) ?x51) (+ ?x63 ?x51)))))
-(let ((@x73 (trans @x68 (rewrite (= (+ ?x63 ?x51) ?x69)) (= (+ (* ?x57 2) ?x51) ?x69))))
-(let ((@x79 (quant-intro (monotonicity @x73 (= (= (+ (* ?x57 2) ?x51) ?x48) $x74)) (= $x61 $x77))))
-(let ((@x92 (trans @x79 (quant-intro (rewrite (= $x74 $x82)) (= $x77 $x88)) (= $x61 $x88))))
-(let ((@x337 (mp~ (mp (asserted $x61) @x92 $x88) (nnf-pos (refl (~ $x82 $x82)) (~ $x88 $x88)) $x88)))
-(let ((@x391 (mp @x337 (quant-intro (refl (= $x82 $x82)) (= $x88 $x386)) $x386)))
-(let (($x612 (or (not $x386) $x608)))
-(let ((@x613 ((_ quant-inst ks$ xs$) $x612)))
-(let ((@x905 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x608) $x614)) (unit-resolution @x613 @x391 $x608) $x614)))
-(let ((?x502 (+ ?x117 (* (- 1) (div ?x114 2)))))
-(let (($x519 (<= ?x502 0)))
-(let (($x503 (= ?x502 0)))
-(let (($x413 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x212 (div ?v0 ?v1)))
-(let ((?x224 (* (- 1) ?v1)))
-(let ((?x221 (* (- 1) ?v0)))
-(let ((?x227 (div ?x221 ?x224)))
-(let (($x242 (<= ?v1 0)))
-(let ((?x249 (ite $x242 ?x227 ?x212)))
-(let (($x210 (= ?v1 0)))
-(let ((?x209 (div$ ?v0 ?v1)))
-(= ?x209 (ite $x210 0 ?x249)))))))))) :pattern ( (div$ ?v0 ?v1) )))
+(let ((?x54 (eval_dioph$ ?1 (map$ uua$ ?0))))
+(let ((?x60 (* 2 ?x54)))
+(let ((?x48 (eval_dioph$ ?1 (map$ uu$ ?0))))
+(let ((?x66 (+ ?x48 ?x60)))
+(let (($x71 (= ?x66 ?x45)))
+(let ((@x65 (monotonicity (rewrite (= (* ?x54 2) ?x60)) (= (+ (* ?x54 2) ?x48) (+ ?x60 ?x48)))))
+(let ((@x70 (trans @x65 (rewrite (= (+ ?x60 ?x48) ?x66)) (= (+ (* ?x54 2) ?x48) ?x66))))
+(let ((@x76 (quant-intro (monotonicity @x70 (= (= (+ (* ?x54 2) ?x48) ?x45) $x71)) (= $x58 $x74))))
+(let ((@x89 (trans @x76 (quant-intro (rewrite (= $x71 $x79)) (= $x74 $x85)) (= $x58 $x85))))
+(let ((@x270 (mp~ (mp (asserted $x58) @x89 $x85) (nnf-pos (refl (~ $x79 $x79)) (~ $x85 $x85)) $x85)))
+(let ((@x309 (mp @x270 (quant-intro (refl (= $x79 $x79)) (= $x85 $x304)) $x304)))
+(let (($x507 (or (not $x304) $x503)))
+(let ((@x508 ((_ quant-inst ks$ xs$) $x507)))
+(let ((@x800 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x503) $x509)) (unit-resolution @x508 @x309 $x503) $x509)))
+(let ((?x396 (+ ?x114 (* (- 1) (div ?x111 2)))))
+(let (($x413 (<= ?x396 0)))
+(let (($x397 (= ?x396 0)))
+(let (($x311 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x145 (div ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x160 (div ?x154 ?x157)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x182 (ite $x175 ?x160 ?x145)))
+(let (($x143 (= ?v1 0)))
+(let ((?x141 (div$ ?v0 ?v1)))
+(= ?x141 (ite $x143 0 ?x182)))))))))) :pattern ( (div$ ?v0 ?v1) )))
 ))
-(let (($x260 (forall ((?v0 Int) (?v1 Int) )(let ((?x212 (div ?v0 ?v1)))
-(let ((?x224 (* (- 1) ?v1)))
-(let ((?x221 (* (- 1) ?v0)))
-(let ((?x227 (div ?x221 ?x224)))
-(let (($x242 (<= ?v1 0)))
-(let ((?x249 (ite $x242 ?x227 ?x212)))
-(let (($x210 (= ?v1 0)))
-(let ((?x209 (div$ ?v0 ?v1)))
-(= ?x209 (ite $x210 0 ?x249)))))))))))
+(let (($x193 (forall ((?v0 Int) (?v1 Int) )(let ((?x145 (div ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x160 (div ?x154 ?x157)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x182 (ite $x175 ?x160 ?x145)))
+(let (($x143 (= ?v1 0)))
+(let ((?x141 (div$ ?v0 ?v1)))
+(= ?x141 (ite $x143 0 ?x182)))))))))))
 ))
-(let ((?x212 (div ?1 ?0)))
-(let ((?x224 (* (- 1) ?0)))
-(let ((?x221 (* (- 1) ?1)))
-(let ((?x227 (div ?x221 ?x224)))
-(let (($x242 (<= ?0 0)))
-(let ((?x249 (ite $x242 ?x227 ?x212)))
-(let (($x210 (= ?0 0)))
-(let ((?x209 (div$ ?1 ?0)))
-(let (($x257 (= ?x209 (ite $x210 0 ?x249))))
-(let (($x219 (forall ((?v0 Int) (?v1 Int) )(let (($x210 (= ?v1 0)))
-(let ((?x217 (ite $x210 0 (ite (< 0 ?v1) (div ?v0 ?v1) (div (- ?v0) (- ?v1))))))
-(let ((?x209 (div$ ?v0 ?v1)))
-(= ?x209 ?x217)))))
+(let ((?x145 (div ?1 ?0)))
+(let ((?x157 (* (- 1) ?0)))
+(let ((?x154 (* (- 1) ?1)))
+(let ((?x160 (div ?x154 ?x157)))
+(let (($x175 (<= ?0 0)))
+(let ((?x182 (ite $x175 ?x160 ?x145)))
+(let (($x143 (= ?0 0)))
+(let ((?x141 (div$ ?1 ?0)))
+(let (($x190 (= ?x141 (ite $x143 0 ?x182))))
+(let (($x152 (forall ((?v0 Int) (?v1 Int) )(let (($x143 (= ?v1 0)))
+(let ((?x150 (ite $x143 0 (ite (< 0 ?v1) (div ?v0 ?v1) (div (- ?v0) (- ?v1))))))
+(let ((?x141 (div$ ?v0 ?v1)))
+(= ?x141 ?x150)))))
 ))
-(let (($x239 (forall ((?v0 Int) (?v1 Int) )(let ((?x224 (* (- 1) ?v1)))
-(let ((?x221 (* (- 1) ?v0)))
-(let ((?x227 (div ?x221 ?x224)))
-(let ((?x212 (div ?v0 ?v1)))
-(let (($x211 (< 0 ?v1)))
-(let ((?x230 (ite $x211 ?x212 ?x227)))
-(let (($x210 (= ?v1 0)))
-(let ((?x233 (ite $x210 0 ?x230)))
-(let ((?x209 (div$ ?v0 ?v1)))
-(= ?x209 ?x233)))))))))))
+(let (($x172 (forall ((?v0 Int) (?v1 Int) )(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x160 (div ?x154 ?x157)))
+(let ((?x145 (div ?v0 ?v1)))
+(let (($x144 (< 0 ?v1)))
+(let ((?x163 (ite $x144 ?x145 ?x160)))
+(let (($x143 (= ?v1 0)))
+(let ((?x166 (ite $x143 0 ?x163)))
+(let ((?x141 (div$ ?v0 ?v1)))
+(= ?x141 ?x166)))))))))))
 ))
-(let (($x211 (< 0 ?0)))
-(let ((?x230 (ite $x211 ?x212 ?x227)))
-(let ((?x233 (ite $x210 0 ?x230)))
-(let ((@x248 (monotonicity (rewrite (= $x211 (not $x242))) (= ?x230 (ite (not $x242) ?x212 ?x227)))))
-(let ((@x253 (trans @x248 (rewrite (= (ite (not $x242) ?x212 ?x227) ?x249)) (= ?x230 ?x249))))
-(let ((@x259 (monotonicity (monotonicity @x253 (= ?x233 (ite $x210 0 ?x249))) (= (= ?x209 ?x233) $x257))))
-(let (($x236 (= ?x209 ?x233)))
-(let (($x237 (= (= ?x209 (ite $x210 0 (ite $x211 ?x212 (div (- ?1) (- ?0))))) $x236)))
-(let ((@x229 (monotonicity (rewrite (= (- ?1) ?x221)) (rewrite (= (- ?0) ?x224)) (= (div (- ?1) (- ?0)) ?x227))))
-(let ((@x235 (monotonicity (monotonicity @x229 (= (ite $x211 ?x212 (div (- ?1) (- ?0))) ?x230)) (= (ite $x210 0 (ite $x211 ?x212 (div (- ?1) (- ?0)))) ?x233))))
-(let ((@x264 (trans (quant-intro (monotonicity @x235 $x237) (= $x219 $x239)) (quant-intro @x259 (= $x239 $x260)) (= $x219 $x260))))
-(let ((@x357 (mp~ (mp (asserted $x219) @x264 $x260) (nnf-pos (refl (~ $x257 $x257)) (~ $x260 $x260)) $x260)))
-(let ((@x418 (mp @x357 (quant-intro (refl (= $x257 $x257)) (= $x260 $x413)) $x413)))
-(let (($x509 (or (not $x413) $x503)))
-(let ((?x467 (div ?x114 2)))
-(let (($x463 (<= 2 0)))
-(let ((?x468 (ite $x463 (div (* (- 1) ?x114) (* (- 1) 2)) ?x467)))
-(let (($x462 (= 2 0)))
-(let ((?x469 (ite $x462 0 ?x468)))
-(let (($x470 (= ?x117 ?x469)))
-(let ((@x480 (rewrite (= (* (- 1) 2) (- 2)))))
-(let ((@x483 (monotonicity (rewrite (= (* (- 1) ?x114) (+ ?x475 ?x100))) @x480 (= (div (* (- 1) ?x114) (* (- 1) 2)) (div (+ ?x475 ?x100) (- 2))))))
-(let ((@x474 (rewrite (= $x463 false))))
-(let ((@x486 (monotonicity @x474 @x483 (= ?x468 (ite false (div (+ ?x475 ?x100) (- 2)) ?x467)))))
-(let ((@x490 (trans @x486 (rewrite (= (ite false (div (+ ?x475 ?x100) (- 2)) ?x467) ?x467)) (= ?x468 ?x467))))
-(let ((@x472 (rewrite (= $x462 false))))
-(let ((@x497 (trans (monotonicity @x472 @x490 (= ?x469 (ite false 0 ?x467))) (rewrite (= (ite false 0 ?x467) ?x467)) (= ?x469 ?x467))))
-(let ((@x507 (trans (monotonicity @x497 (= $x470 (= ?x117 ?x467))) (rewrite (= (= ?x117 ?x467) $x503)) (= $x470 $x503))))
-(let ((@x516 (trans (monotonicity @x507 (= (or (not $x413) $x470) $x509)) (rewrite (= $x509 $x509)) (= (or (not $x413) $x470) $x509))))
-(let ((@x907 (unit-resolution (mp ((_ quant-inst (+ l$ ?x113) 2) (or (not $x413) $x470)) @x516 $x509) @x418 $x503)))
-(let ((?x530 (mod (+ l$ ?x100) 2)))
-(let (($x570 (>= ?x530 0)))
-(let ((@x915 ((_ th-lemma arith farkas 1 -2 -2 -1 1 1) (unit-resolution ((_ th-lemma arith) (or false $x570)) @x26 $x570) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x503) $x519)) @x907 $x519) (hypothesis $x792) @x905 (hypothesis (not $x799)) @x898 false)))
-(let (($x137 (not $x98)))
-(let (($x372 (= $x98 $x365)))
-(let ((@x371 (monotonicity (rewrite (= (and $x103 $x120) $x366)) (= (= $x137 (and $x103 $x120)) (= $x137 $x366)))))
-(let ((@x376 (trans @x371 (rewrite (= (= $x137 $x366) $x372)) (= (= $x137 (and $x103 $x120)) $x372))))
-(let (($x123 (and $x103 $x120)))
-(let (($x138 (= $x137 $x123)))
-(let (($x110 (= $x98 (and $x103 (= ?x105 (div$ (- l$ ?x100) 2))))))
-(let (($x111 (not $x110)))
-(let ((@x119 (monotonicity (rewrite (= (- l$ ?x100) ?x114)) (= (div$ (- l$ ?x100) 2) ?x117))))
-(let ((@x125 (monotonicity (monotonicity @x119 (= (= ?x105 (div$ (- l$ ?x100) 2)) $x120)) (= (and $x103 (= ?x105 (div$ (- l$ ?x100) 2))) $x123))))
-(let ((@x133 (trans (monotonicity @x125 (= $x110 (= $x98 $x123))) (rewrite (= (= $x98 $x123) (= $x98 $x123))) (= $x110 (= $x98 $x123)))))
-(let ((@x142 (trans (monotonicity @x133 (= $x111 (not (= $x98 $x123)))) (rewrite (= (not (= $x98 $x123)) $x138)) (= $x111 $x138))))
-(let ((@x377 (mp (mp (asserted $x111) @x142 $x138) @x376 $x372)))
-(let ((@x449 (unit-resolution (def-axiom (or $x137 $x365 (not $x372))) @x377 (or $x137 $x365))))
-(let ((@x603 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x98 (not $x799) $x874)) (unit-resolution @x449 @x583 $x137) (or (not $x799) $x874))))
-(let ((@x604 (unit-resolution @x603 (unit-resolution (lemma @x915 (or $x799 (not $x792))) @x577 $x799) $x874)))
-(let ((?x649 (+ ?x102 ?x648)))
-(let (($x666 (>= ?x649 0)))
-(let (($x650 (= ?x649 0)))
-(let (($x420 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x267 (mod ?v0 ?v1)))
-(let ((?x224 (* (- 1) ?v1)))
-(let ((?x221 (* (- 1) ?v0)))
-(let ((?x275 (mod ?x221 ?x224)))
-(let ((?x281 (* (- 1) ?x275)))
-(let (($x242 (<= ?v1 0)))
-(let ((?x301 (ite $x242 ?x281 ?x267)))
-(let (($x210 (= ?v1 0)))
-(let ((?x306 (ite $x210 ?v0 ?x301)))
-(let ((?x266 (mod$ ?v0 ?v1)))
-(= ?x266 ?x306))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
+(let (($x144 (< 0 ?0)))
+(let ((?x163 (ite $x144 ?x145 ?x160)))
+(let ((?x166 (ite $x143 0 ?x163)))
+(let ((@x181 (monotonicity (rewrite (= $x144 (not $x175))) (= ?x163 (ite (not $x175) ?x145 ?x160)))))
+(let ((@x186 (trans @x181 (rewrite (= (ite (not $x175) ?x145 ?x160) ?x182)) (= ?x163 ?x182))))
+(let ((@x192 (monotonicity (monotonicity @x186 (= ?x166 (ite $x143 0 ?x182))) (= (= ?x141 ?x166) $x190))))
+(let (($x169 (= ?x141 ?x166)))
+(let (($x170 (= (= ?x141 (ite $x143 0 (ite $x144 ?x145 (div (- ?1) (- ?0))))) $x169)))
+(let ((@x162 (monotonicity (rewrite (= (- ?1) ?x154)) (rewrite (= (- ?0) ?x157)) (= (div (- ?1) (- ?0)) ?x160))))
+(let ((@x168 (monotonicity (monotonicity @x162 (= (ite $x144 ?x145 (div (- ?1) (- ?0))) ?x163)) (= (ite $x143 0 (ite $x144 ?x145 (div (- ?1) (- ?0)))) ?x166))))
+(let ((@x197 (trans (quant-intro (monotonicity @x168 $x170) (= $x152 $x172)) (quant-intro @x192 (= $x172 $x193)) (= $x152 $x193))))
+(let ((@x275 (mp~ (mp (asserted $x152) @x197 $x193) (nnf-pos (refl (~ $x190 $x190)) (~ $x193 $x193)) $x193)))
+(let ((@x316 (mp @x275 (quant-intro (refl (= $x190 $x190)) (= $x193 $x311)) $x311)))
+(let (($x403 (or (not $x311) $x397)))
+(let ((?x361 (div ?x111 2)))
+(let (($x357 (<= 2 0)))
+(let ((?x362 (ite $x357 (div (* (- 1) ?x111) (* (- 1) 2)) ?x361)))
+(let (($x356 (= 2 0)))
+(let ((?x363 (ite $x356 0 ?x362)))
+(let (($x364 (= ?x114 ?x363)))
+(let ((@x374 (rewrite (= (* (- 1) 2) (- 2)))))
+(let ((@x377 (monotonicity (rewrite (= (* (- 1) ?x111) (+ ?x369 ?x97))) @x374 (= (div (* (- 1) ?x111) (* (- 1) 2)) (div (+ ?x369 ?x97) (- 2))))))
+(let ((@x368 (rewrite (= $x357 false))))
+(let ((@x380 (monotonicity @x368 @x377 (= ?x362 (ite false (div (+ ?x369 ?x97) (- 2)) ?x361)))))
+(let ((@x384 (trans @x380 (rewrite (= (ite false (div (+ ?x369 ?x97) (- 2)) ?x361) ?x361)) (= ?x362 ?x361))))
+(let ((@x366 (rewrite (= $x356 false))))
+(let ((@x391 (trans (monotonicity @x366 @x384 (= ?x363 (ite false 0 ?x361))) (rewrite (= (ite false 0 ?x361) ?x361)) (= ?x363 ?x361))))
+(let ((@x401 (trans (monotonicity @x391 (= $x364 (= ?x114 ?x361))) (rewrite (= (= ?x114 ?x361) $x397)) (= $x364 $x397))))
+(let ((@x410 (trans (monotonicity @x401 (= (or (not $x311) $x364) $x403)) (rewrite (= $x403 $x403)) (= (or (not $x311) $x364) $x403))))
+(let ((@x802 (unit-resolution (mp ((_ quant-inst (+ l$ ?x110) 2) (or (not $x311) $x364)) @x410 $x403) @x316 $x397)))
+(let ((?x425 (mod (+ l$ ?x97) 2)))
+(let (($x465 (>= ?x425 0)))
+(let ((@x810 ((_ th-lemma arith farkas 1 -2 -2 -1 1 1) (unit-resolution ((_ th-lemma arith) (or false $x465)) @x26 $x465) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x397) $x413)) @x802 $x413) (hypothesis $x687) @x800 (hypothesis (not $x694)) @x793 false)))
+(let (($x134 (not $x95)))
+(let (($x290 (= $x95 $x283)))
+(let ((@x289 (monotonicity (rewrite (= (and $x100 $x117) $x284)) (= (= $x134 (and $x100 $x117)) (= $x134 $x284)))))
+(let ((@x294 (trans @x289 (rewrite (= (= $x134 $x284) $x290)) (= (= $x134 (and $x100 $x117)) $x290))))
+(let (($x120 (and $x100 $x117)))
+(let (($x135 (= $x134 $x120)))
+(let (($x107 (= $x95 (and $x100 (= ?x102 (div$ (- l$ ?x97) 2))))))
+(let (($x108 (not $x107)))
+(let ((@x116 (monotonicity (rewrite (= (- l$ ?x97) ?x111)) (= (div$ (- l$ ?x97) 2) ?x114))))
+(let ((@x122 (monotonicity (monotonicity @x116 (= (= ?x102 (div$ (- l$ ?x97) 2)) $x117)) (= (and $x100 (= ?x102 (div$ (- l$ ?x97) 2))) $x120))))
+(let ((@x130 (trans (monotonicity @x122 (= $x107 (= $x95 $x120))) (rewrite (= (= $x95 $x120) (= $x95 $x120))) (= $x107 (= $x95 $x120)))))
+(let ((@x139 (trans (monotonicity @x130 (= $x108 (not (= $x95 $x120)))) (rewrite (= (not (= $x95 $x120)) $x135)) (= $x108 $x135))))
+(let ((@x295 (mp (mp (asserted $x108) @x139 $x135) @x294 $x290)))
+(let ((@x344 (unit-resolution (def-axiom (or $x134 $x283 (not $x290))) @x295 (or $x134 $x283))))
+(let ((@x870 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x95 (not $x694) $x857)) (unit-resolution @x344 @x837 $x134) (or (not $x694) $x857))))
+(let ((@x897 (unit-resolution @x870 (unit-resolution (lemma @x810 (or $x694 (not $x687))) @x591 $x694) $x857)))
+(let ((?x544 (+ ?x99 ?x543)))
+(let (($x561 (>= ?x544 0)))
+(let (($x545 (= ?x544 0)))
+(let (($x318 (forall ((?v0 Int) (?v1 Int) )(!(let ((?x200 (mod ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x234 (ite $x175 ?x214 ?x200)))
+(let (($x143 (= ?v1 0)))
+(let ((?x239 (ite $x143 ?v0 ?x234)))
+(let ((?x199 (mod$ ?v0 ?v1)))
+(= ?x199 ?x239))))))))))) :pattern ( (mod$ ?v0 ?v1) )))
 ))
-(let (($x312 (forall ((?v0 Int) (?v1 Int) )(let ((?x267 (mod ?v0 ?v1)))
-(let ((?x224 (* (- 1) ?v1)))
-(let ((?x221 (* (- 1) ?v0)))
-(let ((?x275 (mod ?x221 ?x224)))
-(let ((?x281 (* (- 1) ?x275)))
-(let (($x242 (<= ?v1 0)))
-(let ((?x301 (ite $x242 ?x281 ?x267)))
-(let (($x210 (= ?v1 0)))
-(let ((?x306 (ite $x210 ?v0 ?x301)))
-(let ((?x266 (mod$ ?v0 ?v1)))
-(= ?x266 ?x306))))))))))))
+(let (($x245 (forall ((?v0 Int) (?v1 Int) )(let ((?x200 (mod ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x234 (ite $x175 ?x214 ?x200)))
+(let (($x143 (= ?v1 0)))
+(let ((?x239 (ite $x143 ?v0 ?x234)))
+(let ((?x199 (mod$ ?v0 ?v1)))
+(= ?x199 ?x239))))))))))))
 ))
-(let ((?x267 (mod ?1 ?0)))
-(let ((?x275 (mod ?x221 ?x224)))
-(let ((?x281 (* (- 1) ?x275)))
-(let ((?x301 (ite $x242 ?x281 ?x267)))
-(let ((?x306 (ite $x210 ?1 ?x301)))
-(let ((?x266 (mod$ ?1 ?0)))
-(let (($x309 (= ?x266 ?x306)))
-(let (($x273 (forall ((?v0 Int) (?v1 Int) )(let (($x210 (= ?v1 0)))
-(let ((?x271 (ite $x210 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
-(let ((?x266 (mod$ ?v0 ?v1)))
-(= ?x266 ?x271)))))
+(let ((?x200 (mod ?1 ?0)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let ((?x234 (ite $x175 ?x214 ?x200)))
+(let ((?x239 (ite $x143 ?1 ?x234)))
+(let ((?x199 (mod$ ?1 ?0)))
+(let (($x242 (= ?x199 ?x239)))
+(let (($x206 (forall ((?v0 Int) (?v1 Int) )(let (($x143 (= ?v1 0)))
+(let ((?x204 (ite $x143 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
+(let ((?x199 (mod$ ?v0 ?v1)))
+(= ?x199 ?x204)))))
 ))
-(let (($x295 (forall ((?v0 Int) (?v1 Int) )(let ((?x224 (* (- 1) ?v1)))
-(let ((?x221 (* (- 1) ?v0)))
-(let ((?x275 (mod ?x221 ?x224)))
-(let ((?x281 (* (- 1) ?x275)))
-(let ((?x267 (mod ?v0 ?v1)))
-(let (($x211 (< 0 ?v1)))
-(let ((?x286 (ite $x211 ?x267 ?x281)))
-(let (($x210 (= ?v1 0)))
-(let ((?x289 (ite $x210 ?v0 ?x286)))
-(let ((?x266 (mod$ ?v0 ?v1)))
-(= ?x266 ?x289))))))))))))
+(let (($x228 (forall ((?v0 Int) (?v1 Int) )(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let ((?x200 (mod ?v0 ?v1)))
+(let (($x144 (< 0 ?v1)))
+(let ((?x219 (ite $x144 ?x200 ?x214)))
+(let (($x143 (= ?v1 0)))
+(let ((?x222 (ite $x143 ?v0 ?x219)))
+(let ((?x199 (mod$ ?v0 ?v1)))
+(= ?x199 ?x222))))))))))))
 ))
-(let ((@x300 (monotonicity (rewrite (= $x211 (not $x242))) (= (ite $x211 ?x267 ?x281) (ite (not $x242) ?x267 ?x281)))))
-(let ((@x305 (trans @x300 (rewrite (= (ite (not $x242) ?x267 ?x281) ?x301)) (= (ite $x211 ?x267 ?x281) ?x301))))
-(let ((@x311 (monotonicity (monotonicity @x305 (= (ite $x210 ?1 (ite $x211 ?x267 ?x281)) ?x306)) (= (= ?x266 (ite $x210 ?1 (ite $x211 ?x267 ?x281))) $x309))))
-(let ((?x286 (ite $x211 ?x267 ?x281)))
-(let ((?x289 (ite $x210 ?1 ?x286)))
-(let (($x292 (= ?x266 ?x289)))
-(let (($x293 (= (= ?x266 (ite $x210 ?1 (ite $x211 ?x267 (- (mod (- ?1) (- ?0)))))) $x292)))
-(let ((@x277 (monotonicity (rewrite (= (- ?1) ?x221)) (rewrite (= (- ?0) ?x224)) (= (mod (- ?1) (- ?0)) ?x275))))
-(let ((@x285 (trans (monotonicity @x277 (= (- (mod (- ?1) (- ?0))) (- ?x275))) (rewrite (= (- ?x275) ?x281)) (= (- (mod (- ?1) (- ?0))) ?x281))))
-(let ((@x288 (monotonicity @x285 (= (ite $x211 ?x267 (- (mod (- ?1) (- ?0)))) ?x286))))
-(let ((@x291 (monotonicity @x288 (= (ite $x210 ?1 (ite $x211 ?x267 (- (mod (- ?1) (- ?0))))) ?x289))))
-(let ((@x316 (trans (quant-intro (monotonicity @x291 $x293) (= $x273 $x295)) (quant-intro @x311 (= $x295 $x312)) (= $x273 $x312))))
-(let ((@x362 (mp~ (mp (asserted $x273) @x316 $x312) (nnf-pos (refl (~ $x309 $x309)) (~ $x312 $x312)) $x312)))
-(let ((@x425 (mp @x362 (quant-intro (refl (= $x309 $x309)) (= $x312 $x420)) $x420)))
-(let (($x655 (not $x420)))
-(let (($x656 (or $x655 $x650)))
-(let ((?x465 (* (- 1) 2)))
-(let ((?x616 (mod ?x475 ?x465)))
-(let ((?x617 (* (- 1) ?x616)))
-(let ((?x622 (ite $x463 ?x617 ?x621)))
-(let ((?x623 (ite $x462 l$ ?x622)))
-(let (($x624 (= ?x102 ?x623)))
-(let ((@x630 (monotonicity (monotonicity @x480 (= ?x616 (mod ?x475 (- 2)))) (= ?x617 (* (- 1) (mod ?x475 (- 2)))))))
-(let ((@x633 (monotonicity @x474 @x630 (= ?x622 (ite false (* (- 1) (mod ?x475 (- 2))) ?x621)))))
-(let ((@x637 (trans @x633 (rewrite (= (ite false (* (- 1) (mod ?x475 (- 2))) ?x621) ?x621)) (= ?x622 ?x621))))
-(let ((@x644 (trans (monotonicity @x472 @x637 (= ?x623 (ite false l$ ?x621))) (rewrite (= (ite false l$ ?x621) ?x621)) (= ?x623 ?x621))))
-(let ((@x654 (trans (monotonicity @x644 (= $x624 (= ?x102 ?x621))) (rewrite (= (= ?x102 ?x621) $x650)) (= $x624 $x650))))
-(let ((@x663 (trans (monotonicity @x654 (= (or $x655 $x624) $x656)) (rewrite (= $x656 $x656)) (= (or $x655 $x624) $x656))))
-(let ((@x664 (mp ((_ quant-inst l$ 2) (or $x655 $x624)) @x663 $x656)))
-(let ((@x921 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x650) $x666)) (unit-resolution @x664 @x425 $x650) $x666)))
-(let ((?x862 (* (- 2) ?x849)))
-(let ((?x863 (+ ?x96 ?x831 ?x862)))
-(let (($x869 (>= ?x863 0)))
-(let (($x861 (= ?x863 0)))
-(let ((@x924 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x861) $x869)) (unit-resolution ((_ th-lemma arith) (or false $x861)) @x26 $x861) $x869)))
-(let ((?x667 (div l$ 2)))
-(let ((?x680 (* (- 2) ?x667)))
-(let ((?x681 (+ l$ ?x648 ?x680)))
-(let (($x687 (>= ?x681 0)))
-(let (($x679 (= ?x681 0)))
-(let ((@x934 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x679) $x687)) (unit-resolution ((_ th-lemma arith) (or false $x679)) @x26 $x679) $x687)))
-(let ((?x609 (mod$ ?x96 2)))
-(let ((?x832 (+ ?x609 ?x831)))
-(let (($x833 (= ?x832 0)))
-(let (($x838 (or $x655 $x833)))
-(let ((?x801 (* (- 1) ?x96)))
-(let ((?x802 (mod ?x801 ?x465)))
-(let ((?x803 (* (- 1) ?x802)))
-(let ((?x805 (ite $x463 ?x803 ?x804)))
-(let ((?x806 (ite $x462 ?x96 ?x805)))
-(let (($x807 (= ?x609 ?x806)))
-(let ((@x813 (monotonicity (monotonicity @x480 (= ?x802 (mod ?x801 (- 2)))) (= ?x803 (* (- 1) (mod ?x801 (- 2)))))))
-(let ((@x816 (monotonicity @x474 @x813 (= ?x805 (ite false (* (- 1) (mod ?x801 (- 2))) ?x804)))))
-(let ((@x820 (trans @x816 (rewrite (= (ite false (* (- 1) (mod ?x801 (- 2))) ?x804) ?x804)) (= ?x805 ?x804))))
-(let ((@x827 (trans (monotonicity @x472 @x820 (= ?x806 (ite false ?x96 ?x804))) (rewrite (= (ite false ?x96 ?x804) ?x804)) (= ?x806 ?x804))))
-(let ((@x837 (trans (monotonicity @x827 (= $x807 (= ?x609 ?x804))) (rewrite (= (= ?x609 ?x804) $x833)) (= $x807 $x833))))
-(let ((@x845 (trans (monotonicity @x837 (= (or $x655 $x807) $x838)) (rewrite (= $x838 $x838)) (= (or $x655 $x807) $x838))))
-(let ((@x775 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x833) (>= ?x832 0))) (unit-resolution (mp ((_ quant-inst (eval_dioph$ ks$ xs$) 2) (or $x655 $x807)) @x845 $x838) @x425 $x833) (>= ?x832 0))))
-(let ((?x888 (* (- 1) ?x609)))
-(let ((?x889 (+ ?x102 ?x888)))
-(let (($x891 (>= ?x889 0)))
-(let (($x887 (= ?x102 ?x609)))
-(let (($x881 (= ?x101 ?x609)))
-(let (($x610 (= ?x609 ?x101)))
-(let (($x379 (forall ((?v0 Int_list$) (?v1 Nat_list$) )(!(= (mod$ (eval_dioph$ ?v0 ?v1) 2) (mod$ (eval_dioph$ ?v0 (map$ uu$ ?v1)) 2)) :pattern ( (eval_dioph$ ?v0 (map$ uu$ ?v1)) )))
+(let ((@x233 (monotonicity (rewrite (= $x144 (not $x175))) (= (ite $x144 ?x200 ?x214) (ite (not $x175) ?x200 ?x214)))))
+(let ((@x238 (trans @x233 (rewrite (= (ite (not $x175) ?x200 ?x214) ?x234)) (= (ite $x144 ?x200 ?x214) ?x234))))
+(let ((@x244 (monotonicity (monotonicity @x238 (= (ite $x143 ?1 (ite $x144 ?x200 ?x214)) ?x239)) (= (= ?x199 (ite $x143 ?1 (ite $x144 ?x200 ?x214))) $x242))))
+(let ((?x219 (ite $x144 ?x200 ?x214)))
+(let ((?x222 (ite $x143 ?1 ?x219)))
+(let (($x225 (= ?x199 ?x222)))
+(let (($x226 (= (= ?x199 (ite $x143 ?1 (ite $x144 ?x200 (- (mod (- ?1) (- ?0)))))) $x225)))
+(let ((@x210 (monotonicity (rewrite (= (- ?1) ?x154)) (rewrite (= (- ?0) ?x157)) (= (mod (- ?1) (- ?0)) ?x208))))
+(let ((@x218 (trans (monotonicity @x210 (= (- (mod (- ?1) (- ?0))) (- ?x208))) (rewrite (= (- ?x208) ?x214)) (= (- (mod (- ?1) (- ?0))) ?x214))))
+(let ((@x221 (monotonicity @x218 (= (ite $x144 ?x200 (- (mod (- ?1) (- ?0)))) ?x219))))
+(let ((@x224 (monotonicity @x221 (= (ite $x143 ?1 (ite $x144 ?x200 (- (mod (- ?1) (- ?0))))) ?x222))))
+(let ((@x249 (trans (quant-intro (monotonicity @x224 $x226) (= $x206 $x228)) (quant-intro @x244 (= $x228 $x245)) (= $x206 $x245))))
+(let ((@x280 (mp~ (mp (asserted $x206) @x249 $x245) (nnf-pos (refl (~ $x242 $x242)) (~ $x245 $x245)) $x245)))
+(let ((@x323 (mp @x280 (quant-intro (refl (= $x242 $x242)) (= $x245 $x318)) $x318)))
+(let (($x550 (not $x318)))
+(let (($x551 (or $x550 $x545)))
+(let ((?x359 (* (- 1) 2)))
+(let ((?x511 (mod ?x369 ?x359)))
+(let ((?x512 (* (- 1) ?x511)))
+(let ((?x517 (ite $x357 ?x512 ?x516)))
+(let ((?x518 (ite $x356 l$ ?x517)))
+(let (($x519 (= ?x99 ?x518)))
+(let ((@x525 (monotonicity (monotonicity @x374 (= ?x511 (mod ?x369 (- 2)))) (= ?x512 (* (- 1) (mod ?x369 (- 2)))))))
+(let ((@x528 (monotonicity @x368 @x525 (= ?x517 (ite false (* (- 1) (mod ?x369 (- 2))) ?x516)))))
+(let ((@x532 (trans @x528 (rewrite (= (ite false (* (- 1) (mod ?x369 (- 2))) ?x516) ?x516)) (= ?x517 ?x516))))
+(let ((@x539 (trans (monotonicity @x366 @x532 (= ?x518 (ite false l$ ?x516))) (rewrite (= (ite false l$ ?x516) ?x516)) (= ?x518 ?x516))))
+(let ((@x549 (trans (monotonicity @x539 (= $x519 (= ?x99 ?x516))) (rewrite (= (= ?x99 ?x516) $x545)) (= $x519 $x545))))
+(let ((@x558 (trans (monotonicity @x549 (= (or $x550 $x519) $x551)) (rewrite (= $x551 $x551)) (= (or $x550 $x519) $x551))))
+(let ((@x559 (mp ((_ quant-inst l$ 2) (or $x550 $x519)) @x558 $x551)))
+(let ((@x900 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x545) $x561)) (unit-resolution @x559 @x323 $x545) $x561)))
+(let ((?x757 (* (- 2) ?x744)))
+(let ((?x758 (+ ?x93 ?x726 ?x757)))
+(let (($x764 (>= ?x758 0)))
+(let (($x756 (= ?x758 0)))
+(let ((@x903 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x756) $x764)) (unit-resolution ((_ th-lemma arith) (or false $x756)) @x26 $x756) $x764)))
+(let ((?x562 (div l$ 2)))
+(let ((?x575 (* (- 2) ?x562)))
+(let ((?x576 (+ l$ ?x543 ?x575)))
+(let (($x582 (>= ?x576 0)))
+(let (($x574 (= ?x576 0)))
+(let ((@x906 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x574) $x582)) (unit-resolution ((_ th-lemma arith) (or false $x574)) @x26 $x574) $x582)))
+(let ((?x504 (mod$ ?x93 2)))
+(let ((?x727 (+ ?x504 ?x726)))
+(let (($x728 (= ?x727 0)))
+(let (($x733 (or $x550 $x728)))
+(let ((?x696 (* (- 1) ?x93)))
+(let ((?x697 (mod ?x696 ?x359)))
+(let ((?x698 (* (- 1) ?x697)))
+(let ((?x700 (ite $x357 ?x698 ?x699)))
+(let ((?x701 (ite $x356 ?x93 ?x700)))
+(let (($x702 (= ?x504 ?x701)))
+(let ((@x708 (monotonicity (monotonicity @x374 (= ?x697 (mod ?x696 (- 2)))) (= ?x698 (* (- 1) (mod ?x696 (- 2)))))))
+(let ((@x711 (monotonicity @x368 @x708 (= ?x700 (ite false (* (- 1) (mod ?x696 (- 2))) ?x699)))))
+(let ((@x715 (trans @x711 (rewrite (= (ite false (* (- 1) (mod ?x696 (- 2))) ?x699) ?x699)) (= ?x700 ?x699))))
+(let ((@x722 (trans (monotonicity @x366 @x715 (= ?x701 (ite false ?x93 ?x699))) (rewrite (= (ite false ?x93 ?x699) ?x699)) (= ?x701 ?x699))))
+(let ((@x732 (trans (monotonicity @x722 (= $x702 (= ?x504 ?x699))) (rewrite (= (= ?x504 ?x699) $x728)) (= $x702 $x728))))
+(let ((@x740 (trans (monotonicity @x732 (= (or $x550 $x702) $x733)) (rewrite (= $x733 $x733)) (= (or $x550 $x702) $x733))))
+(let ((@x455 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x728) (>= ?x727 0))) (unit-resolution (mp ((_ quant-inst (eval_dioph$ ks$ xs$) 2) (or $x550 $x702)) @x740 $x733) @x323 $x728) (>= ?x727 0))))
+(let ((?x783 (* (- 1) ?x504)))
+(let ((?x784 (+ ?x99 ?x783)))
+(let (($x786 (>= ?x784 0)))
+(let (($x782 (= ?x99 ?x504)))
+(let (($x663 (= ?x98 ?x504)))
+(let (($x505 (= ?x504 ?x98)))
+(let (($x297 (forall ((?v0 Int_list$) (?v1 Int_list$) )(!(= (mod$ (eval_dioph$ ?v0 ?v1) 2) (mod$ (eval_dioph$ ?v0 (map$ uu$ ?v1)) 2)) :pattern ( (eval_dioph$ ?v0 (map$ uu$ ?v1)) )))
 ))
-(let (($x54 (forall ((?v0 Int_list$) (?v1 Nat_list$) )(= (mod$ (eval_dioph$ ?v0 ?v1) 2) (mod$ (eval_dioph$ ?v0 (map$ uu$ ?v1)) 2)))
+(let (($x51 (forall ((?v0 Int_list$) (?v1 Int_list$) )(= (mod$ (eval_dioph$ ?v0 ?v1) 2) (mod$ (eval_dioph$ ?v0 (map$ uu$ ?v1)) 2)))
 ))
-(let (($x53 (= (mod$ ?x48 2) (mod$ ?x51 2))))
-(let ((@x332 (mp~ (asserted $x54) (nnf-pos (refl (~ $x53 $x53)) (~ $x54 $x54)) $x54)))
-(let ((@x384 (mp @x332 (quant-intro (refl (= $x53 $x53)) (= $x54 $x379)) $x379)))
-(let (($x619 (or (not $x379) $x610)))
-(let ((@x620 ((_ quant-inst ks$ xs$) $x619)))
-(let ((@x965 (symm (unit-resolution (def-axiom (or $x365 $x103)) @x583 $x103) (= ?x102 ?x101))))
-(let ((@x962 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x887) $x891)) (trans @x965 (symm (unit-resolution @x620 @x384 $x610) $x881) $x887) $x891)))
-(let (($x890 (<= ?x889 0)))
-(let ((@x1023 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x887) $x890)) (trans @x965 (symm (unit-resolution @x620 @x384 $x610) $x881) $x887) $x890)))
-(let (($x793 (>= ?x791 0)))
-(let ((@x522 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x364 $x793)) (unit-resolution (def-axiom (or $x365 $x120)) @x583 $x120) $x793)))
-(let ((@x1085 (unit-resolution ((_ th-lemma arith) (or false (not (>= ?x530 2)))) @x26 (not (>= ?x530 2)))))
-(let (($x665 (<= ?x649 0)))
-(let ((@x767 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x650) $x665)) (unit-resolution @x664 @x425 $x650) $x665)))
-(let (($x868 (<= ?x863 0)))
-(let ((@x858 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x861) $x868)) (unit-resolution ((_ th-lemma arith) (or false $x861)) @x26 $x861) $x868)))
-(let (($x686 (<= ?x681 0)))
-(let ((@x1092 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x679) $x686)) (unit-resolution ((_ th-lemma arith) (or false $x679)) @x26 $x679) $x686)))
-(let ((@x1095 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x833) (<= ?x832 0))) (unit-resolution (mp ((_ quant-inst (eval_dioph$ ks$ xs$) 2) (or $x655 $x807)) @x845 $x838) @x425 $x833) (<= ?x832 0))))
-(let (($x615 (>= ?x607 0)))
-(let ((@x1100 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x608) $x615)) (unit-resolution @x613 @x391 $x608) $x615)))
-(let ((@x1104 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x503) (>= ?x502 0))) @x907 (>= ?x502 0))))
-(let ((@x1107 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x539) (<= ?x542 0))) (unit-resolution ((_ th-lemma arith) (or false $x539)) @x26 $x539) (<= ?x542 0))))
-(let ((@x1108 ((_ th-lemma arith farkas 1 -2 -2 -1 -2 1 1 1 1 1 1) @x1107 @x1104 (hypothesis $x793) @x1100 (hypothesis $x1078) (hypothesis $x890) @x1095 @x1092 @x858 @x767 @x1085 false)))
-(let ((@x576 (unit-resolution (lemma @x1108 (or (not $x1078) (not $x793) (not $x890))) @x522 @x1023 (not $x1078))))
-(let ((@x966 (unit-resolution @x576 ((_ th-lemma arith) @x962 @x775 @x934 @x924 @x921 @x604 $x1078) false)))
-(let ((@x967 (lemma @x966 $x365)))
-(let ((@x445 (unit-resolution (def-axiom (or $x98 $x366 (not $x372))) @x377 (or $x98 $x366))))
-(let ((@x586 (unit-resolution @x445 @x967 $x98)))
-(let ((@x1067 (trans (symm (unit-resolution @x620 @x384 $x610) $x881) (monotonicity @x586 (= ?x609 ?x102)) $x103)))
-(let (($x916 (not $x792)))
-(let ((@x950 ((_ th-lemma arith assign-bounds 1 -1/2 -1/2 1/2 -1/2) (or $x793 (not $x519) (not $x570) (not $x548) (not $x614) $x874))))
-(let ((@x951 (unit-resolution @x950 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x503) $x519)) @x907 $x519) (unit-resolution ((_ th-lemma arith triangle-eq) (or $x137 $x800)) @x586 $x800) @x898 (unit-resolution ((_ th-lemma arith) (or false $x570)) @x26 $x570) @x905 $x793)))
-(let ((@x1040 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x120 $x916 (not $x793))) (hypothesis $x364) (or $x916 (not $x793)))))
-(let ((@x1060 ((_ th-lemma arith farkas -2 -2 1 -1 1 1) (unit-resolution @x1040 @x951 $x916) @x1104 @x1107 @x1100 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x137 $x799)) @x586 $x799) @x1085 false)))
-(let ((@x569 (unit-resolution (unit-resolution (def-axiom (or $x366 $x363 $x364)) @x967 $x365) (lemma @x1060 $x120) $x363)))
-(unit-resolution @x569 @x1067 false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(let (($x50 (= (mod$ ?x45 2) (mod$ ?x48 2))))
+(let ((@x265 (mp~ (asserted $x51) (nnf-pos (refl (~ $x50 $x50)) (~ $x51 $x51)) $x51)))
+(let ((@x302 (mp @x265 (quant-intro (refl (= $x50 $x50)) (= $x51 $x297)) $x297)))
+(let (($x514 (or (not $x297) $x505)))
+(let ((@x515 ((_ quant-inst ks$ xs$) $x514)))
+(let ((@x658 (symm (unit-resolution (def-axiom (or $x283 $x100)) @x837 $x100) (= ?x99 ?x98))))
+(let ((@x911 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x782) $x786)) (trans @x658 (symm (unit-resolution @x515 @x302 $x505) $x663) $x782) $x786)))
+(let (($x785 (<= ?x784 0)))
+(let ((@x814 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x782) $x785)) (trans @x658 (symm (unit-resolution @x515 @x302 $x505) $x663) $x782) $x785)))
+(let (($x688 (>= ?x686 0)))
+(let ((@x824 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x282 $x688)) (unit-resolution (def-axiom (or $x283 $x117)) @x837 $x117) $x688)))
+(let ((@x979 (unit-resolution ((_ th-lemma arith) (or false (not (>= ?x425 2)))) @x26 (not (>= ?x425 2)))))
+(let (($x560 (<= ?x544 0)))
+(let ((@x427 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x545) $x560)) (unit-resolution @x559 @x323 $x545) $x560)))
+(let (($x763 (<= ?x758 0)))
+(let ((@x569 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x756) $x763)) (unit-resolution ((_ th-lemma arith) (or false $x756)) @x26 $x756) $x763)))
+(let (($x581 (<= ?x576 0)))
+(let ((@x986 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x574) $x581)) (unit-resolution ((_ th-lemma arith) (or false $x574)) @x26 $x574) $x581)))
+(let ((@x989 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x728) (<= ?x727 0))) (unit-resolution (mp ((_ quant-inst (eval_dioph$ ks$ xs$) 2) (or $x550 $x702)) @x740 $x733) @x323 $x728) (<= ?x727 0))))
+(let (($x510 (>= ?x502 0)))
+(let ((@x994 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x503) $x510)) (unit-resolution @x508 @x309 $x503) $x510)))
+(let ((@x998 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x397) (>= ?x396 0))) @x802 (>= ?x396 0))))
+(let ((@x1001 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x434) (<= ?x437 0))) (unit-resolution ((_ th-lemma arith) (or false $x434)) @x26 $x434) (<= ?x437 0))))
+(let ((@x1002 ((_ th-lemma arith farkas 1 -2 -2 -1 -2 1 1 1 1 1 1) @x1001 @x998 (hypothesis $x688) @x994 (hypothesis $x972) (hypothesis $x785) @x989 @x986 @x569 @x427 @x979 false)))
+(let ((@x821 (unit-resolution (lemma @x1002 (or (not $x972) (not $x688) (not $x785))) @x824 @x814 (not $x972))))
+(let ((@x769 (unit-resolution @x821 ((_ th-lemma arith) @x911 @x455 @x906 @x903 @x900 @x897 $x972) false)))
+(let ((@x770 (lemma @x769 $x283)))
+(let ((@x340 (unit-resolution (def-axiom (or $x95 $x284 (not $x290))) @x295 (or $x95 $x284))))
+(let ((@x753 (unit-resolution @x340 @x770 $x95)))
+(let ((@x867 (trans (symm (unit-resolution @x515 @x302 $x505) $x663) (monotonicity @x753 (= ?x504 ?x99)) $x100)))
+(let (($x811 (not $x687)))
+(let ((@x845 ((_ th-lemma arith assign-bounds 1 -1/2 -1/2 1/2 -1/2) (or $x688 (not $x413) (not $x465) (not $x443) (not $x509) $x857))))
+(let ((@x892 (unit-resolution @x845 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x397) $x413)) @x802 $x413) (unit-resolution ((_ th-lemma arith triangle-eq) (or $x134 $x695)) @x753 $x695) @x793 (unit-resolution ((_ th-lemma arith) (or false $x465)) @x26 $x465) @x800 $x688)))
+(let ((@x935 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x117 $x811 (not $x688))) (hypothesis $x282) (or $x811 (not $x688)))))
+(let ((@x955 ((_ th-lemma arith farkas -2 -2 1 -1 1 1) (unit-resolution @x935 @x892 $x811) @x998 @x1001 @x994 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x134 $x694)) @x753 $x694) @x979 false)))
+(let ((@x939 (unit-resolution (unit-resolution (def-axiom (or $x284 $x281 $x282)) @x770 $x283) (lemma @x955 $x117) $x281)))
+(unit-resolution @x939 @x867 false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 
 d277a40ca34ecc409672601e981711fef2d0064f 64 0
 unsat
@@ -5663,30 +4632,30 @@
 (let ((@x258 ((_ quant-inst 1) $x257)))
 (unit-resolution @x258 @x620 @x145 false))))))))))))))))))
 
-4e5cf2f6b4df716b03e440b50af106a8af8b2799 170 0
+b4b100f728c8f0d6f96483e4de44e248cc4be1aa 101 0
 unsat
 ((set-logic AUFLIA)
 (proof
-(let ((?x209 (some$a true)))
-(let ((?x210 (g$b ?x209)))
-(let ((?x206 (some$ 3)))
-(let ((?x208 (g$ ?x206)))
-(let (($x211 (= ?x208 ?x210)))
-(let ((?x434 (cons$a true nil$a)))
-(let ((?x435 (g$c ?x434)))
-(let (($x406 (= ?x210 ?x435)))
-(let (($x768 (forall ((?v0 Bool) )(!(= (g$b (some$a ?v0)) (g$c (cons$a ?v0 nil$a))) :pattern ( (some$a ?v0) ) :pattern ( (cons$a ?v0 nil$a) )))
+(let ((?x124 (some$a true)))
+(let ((?x125 (g$b ?x124)))
+(let ((?x122 (some$ 3)))
+(let ((?x123 (g$ ?x122)))
+(let (($x126 (= ?x123 ?x125)))
+(let ((?x269 (cons$a true nil$a)))
+(let ((?x270 (g$c ?x269)))
+(let (($x587 (= ?x125 ?x270)))
+(let (($x604 (forall ((?v0 Bool) )(!(= (g$b (some$a ?v0)) (g$c (cons$a ?v0 nil$a))) :pattern ( (some$a ?v0) ) :pattern ( (cons$a ?v0 nil$a) )))
 ))
 (let (($x43 (forall ((?v0 Bool) )(= (g$b (some$a ?v0)) (g$c (cons$a ?v0 nil$a))))
 ))
 (let (($x42 (= (g$b (some$a ?0)) (g$c (cons$a ?0 nil$a)))))
-(let ((@x280 (mp~ (asserted $x43) (nnf-pos (refl (~ $x42 $x42)) (~ $x43 $x43)) $x43)))
-(let ((@x773 (mp @x280 (quant-intro (refl (= $x42 $x42)) (= $x43 $x768)) $x768)))
-(let (($x419 (or (not $x768) $x406)))
-(let ((@x752 ((_ quant-inst true) $x419)))
-(let ((?x720 (size$ ?x434)))
-(let (($x444 (= ?x435 ?x720)))
-(let (($x776 (forall ((?v0 Bool_list$) )(!(let ((?x61 (size$ ?v0)))
+(let ((@x160 (mp~ (asserted $x43) (nnf-pos (refl (~ $x42 $x42)) (~ $x43 $x43)) $x43)))
+(let ((@x609 (mp @x160 (quant-intro (refl (= $x42 $x42)) (= $x43 $x604)) $x604)))
+(let (($x254 (or (not $x604) $x587)))
+(let ((@x255 ((_ quant-inst true) $x254)))
+(let ((?x227 (size$ ?x269)))
+(let (($x569 (= ?x270 ?x227)))
+(let (($x612 (forall ((?v0 Bool_list$) )(!(let ((?x61 (size$ ?v0)))
 (let ((?x60 (g$c ?v0)))
 (= ?x60 ?x61))) :pattern ( (g$c ?v0) ) :pattern ( (size$ ?v0) )))
 ))
@@ -5694,115 +4663,46 @@
 (let ((?x60 (g$c ?v0)))
 (= ?x60 ?x61))))
 ))
-(let ((@x780 (quant-intro (refl (= (= (g$c ?0) (size$ ?0)) (= (g$c ?0) (size$ ?0)))) (= $x63 $x776))))
-(let ((@x306 (nnf-pos (refl (~ (= (g$c ?0) (size$ ?0)) (= (g$c ?0) (size$ ?0)))) (~ $x63 $x63))))
-(let ((@x781 (mp (mp~ (asserted $x63) @x306 $x63) @x780 $x776)))
-(let (($x711 (or (not $x776) $x444)))
-(let ((@x712 ((_ quant-inst (cons$a true nil$a)) $x711)))
-(let ((?x149 (size$ nil$a)))
-(let ((?x724 (of_nat$ ?x149)))
-(let ((?x710 (+ 1 ?x724)))
-(let ((?x713 (nat$ ?x710)))
-(let (($x714 (= ?x720 ?x713)))
-(let (($x819 (forall ((?v0 Bool) (?v1 Bool_list$) )(!(= (size$ (cons$a ?v0 ?v1)) (nat$ (+ 1 (of_nat$ (size$ ?v1))))) :pattern ( (cons$a ?v0 ?v1) )))
-))
-(let (($x177 (forall ((?v0 Bool) (?v1 Bool_list$) )(= (size$ (cons$a ?v0 ?v1)) (nat$ (+ 1 (of_nat$ (size$ ?v1))))))
-))
-(let (($x174 (= (size$ (cons$a ?1 ?0)) (nat$ (+ 1 (of_nat$ (size$ ?0)))))))
-(let (($x161 (forall ((?v0 Bool) (?v1 Bool_list$) )(= (size$ (cons$a ?v0 ?v1)) (nat$ (+ (of_nat$ (size$ ?v1)) (+ 0 1)))))
+(let ((@x616 (quant-intro (refl (= (= (g$c ?0) (size$ ?0)) (= (g$c ?0) (size$ ?0)))) (= $x63 $x612))))
+(let ((@x142 (nnf-pos (refl (~ (= (g$c ?0) (size$ ?0)) (= (g$c ?0) (size$ ?0)))) (~ $x63 $x63))))
+(let ((@x617 (mp (mp~ (asserted $x63) @x142 $x63) @x616 $x612)))
+(let (($x571 (or (not $x612) $x569)))
+(let ((@x572 ((_ quant-inst (cons$a true nil$a)) $x571)))
+(let ((?x89 (suc$ zero$)))
+(let ((?x105 (size$ nil$a)))
+(let ((?x233 (plus$ ?x105 ?x89)))
+(let (($x570 (= ?x227 ?x233)))
+(let (($x657 (forall ((?v0 Bool) (?v1 Bool_list$) )(!(= (size$ (cons$a ?v0 ?v1)) (plus$ (size$ ?v1) (suc$ zero$))) :pattern ( (cons$a ?v0 ?v1) )))
 ))
-(let (($x160 (= (size$ (cons$a ?1 ?0)) (nat$ (+ (of_nat$ (size$ ?0)) (+ 0 1))))))
-(let (($x172 (= (nat$ (+ (of_nat$ (size$ ?0)) (+ 0 1))) (nat$ (+ 1 (of_nat$ (size$ ?0)))))))
-(let ((?x61 (size$ ?0)))
-(let ((?x157 (of_nat$ ?x61)))
-(let ((?x166 (+ 1 ?x157)))
-(let ((?x92 (+ 0 1)))
-(let ((?x158 (+ ?x157 ?x92)))
-(let ((@x170 (trans (monotonicity (rewrite (= ?x92 1)) (= ?x158 (+ ?x157 1))) (rewrite (= (+ ?x157 1) ?x166)) (= ?x158 ?x166))))
-(let ((@x179 (quant-intro (monotonicity (monotonicity @x170 $x172) (= $x160 $x174)) (= $x161 $x177))))
-(let ((@x323 (mp~ (mp (asserted $x161) @x179 $x177) (nnf-pos (refl (~ $x174 $x174)) (~ $x177 $x177)) $x177)))
-(let ((@x824 (mp @x323 (quant-intro (refl (= $x174 $x174)) (= $x177 $x819)) $x819)))
-(let (($x718 (or (not $x819) $x714)))
-(let ((@x556 ((_ quant-inst true nil$a) $x718)))
-(let ((?x153 (size$a nil$)))
-(let ((?x730 (of_nat$ ?x153)))
-(let (($x716 (<= ?x730 0)))
-(let (($x715 (= ?x730 0)))
-(let ((?x73 (nat$ 0)))
-(let ((?x748 (of_nat$ ?x73)))
-(let (($x412 (= ?x748 0)))
-(let (($x841 (forall ((?v0 Int) )(!(let (($x223 (= (of_nat$ (nat$ ?v0)) ?v0)))
-(let (($x236 (>= ?v0 0)))
-(let (($x237 (not $x236)))
-(or $x237 $x223)))) :pattern ( (nat$ ?v0) )))
-))
-(let (($x243 (forall ((?v0 Int) )(let (($x223 (= (of_nat$ (nat$ ?v0)) ?v0)))
-(let (($x236 (>= ?v0 0)))
-(let (($x237 (not $x236)))
-(or $x237 $x223)))))
-))
-(let (($x223 (= (of_nat$ (nat$ ?0)) ?0)))
-(let (($x236 (>= ?0 0)))
-(let (($x237 (not $x236)))
-(let (($x240 (or $x237 $x223)))
-(let (($x225 (forall ((?v0 Int) )(let (($x223 (= (of_nat$ (nat$ ?v0)) ?v0)))
-(let (($x220 (<= 0 ?v0)))
-(=> $x220 $x223))))
+(let (($x114 (forall ((?v0 Bool) (?v1 Bool_list$) )(= (size$ (cons$a ?v0 ?v1)) (plus$ (size$ ?v1) (suc$ zero$))))
 ))
-(let (($x231 (forall ((?v0 Int) )(let (($x223 (= (of_nat$ (nat$ ?v0)) ?v0)))
-(or (not (<= 0 ?v0)) $x223)))
+(let (($x113 (= (size$ (cons$a ?1 ?0)) (plus$ (size$ ?0) ?x89))))
+(let ((@x173 (mp~ (asserted $x114) (nnf-pos (refl (~ $x113 $x113)) (~ $x114 $x114)) $x114)))
+(let ((@x662 (mp @x173 (quant-intro (refl (= $x113 $x113)) (= $x114 $x657)) $x657)))
+(let (($x576 (or (not $x657) $x570)))
+(let ((@x213 ((_ quant-inst true nil$a) $x576)))
+(let ((?x108 (size$a nil$)))
+(let (($x109 (= ?x108 zero$)))
+(let ((@x110 (asserted $x109)))
+(let (($x106 (= ?x105 zero$)))
+(let ((@x107 (asserted $x106)))
+(let ((@x287 (monotonicity (trans @x107 (symm @x110 (= zero$ ?x108)) (= ?x105 ?x108)) (= ?x233 (plus$ ?x108 ?x89)))))
+(let ((?x246 (plus$ ?x108 ?x89)))
+(let ((?x256 (cons$ 3 nil$)))
+(let ((?x588 (size$a ?x256)))
+(let (($x584 (= ?x588 ?x246)))
+(let (($x664 (forall ((?v0 Int) (?v1 Int_list$) )(!(= (size$a (cons$ ?v0 ?v1)) (plus$ (size$a ?v1) (suc$ zero$))) :pattern ( (cons$ ?v0 ?v1) )))
 ))
-(let ((@x239 (monotonicity (rewrite (= (<= 0 ?0) $x236)) (= (not (<= 0 ?0)) $x237))))
-(let ((@x245 (quant-intro (monotonicity @x239 (= (or (not (<= 0 ?0)) $x223) $x240)) (= $x231 $x243))))
-(let ((@x230 (rewrite (= (=> (<= 0 ?0) $x223) (or (not (<= 0 ?0)) $x223)))))
-(let ((@x248 (mp (asserted $x225) (trans (quant-intro @x230 (= $x225 $x231)) @x245 (= $x225 $x243)) $x243)))
-(let ((@x846 (mp (mp~ @x248 (nnf-pos (refl (~ $x240 $x240)) (~ $x243 $x243)) $x243) (quant-intro (refl (= $x240 $x240)) (= $x243 $x841)) $x841)))
-(let (($x381 (not $x841)))
-(let (($x382 (or $x381 $x412)))
-(let ((@x733 (rewrite (= (>= 0 0) true))))
-(let ((@x736 (trans (monotonicity @x733 (= (not (>= 0 0)) (not true))) (rewrite (= (not true) false)) (= (not (>= 0 0)) false))))
-(let ((@x739 (monotonicity @x736 (= (or (not (>= 0 0)) $x412) (or false $x412)))))
-(let ((@x742 (trans @x739 (rewrite (= (or false $x412) $x412)) (= (or (not (>= 0 0)) $x412) $x412))))
-(let ((@x731 (monotonicity @x742 (= (or $x381 (or (not (>= 0 0)) $x412)) $x382))))
-(let ((@x450 (trans @x731 (rewrite (= $x382 $x382)) (= (or $x381 (or (not (>= 0 0)) $x412)) $x382))))
-(let ((@x451 (mp ((_ quant-inst 0) (or $x381 (or (not (>= 0 0)) $x412))) @x450 $x382)))
-(let ((@x621 (trans (monotonicity (asserted (= ?x153 ?x73)) (= ?x730 ?x748)) (unit-resolution @x451 @x846 $x412) $x715)))
-(let (($x557 (>= ?x730 0)))
-(let ((@x610 ((_ th-lemma arith eq-propagate -1 -1) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x715) $x557)) @x621 $x557) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x715) $x716)) @x621 $x716) (= (+ 1 ?x730) 1))))
-(let (($x700 (<= ?x724 0)))
-(let (($x558 (= ?x724 0)))
-(let ((@x583 (trans (monotonicity (asserted (= ?x149 ?x73)) (= ?x724 ?x748)) (unit-resolution @x451 @x846 $x412) $x558)))
-(let (($x701 (>= ?x724 0)))
-(let ((@x559 ((_ th-lemma arith eq-propagate -1 -1) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x558) $x701)) @x583 $x701) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x558) $x700)) @x583 $x700) (= ?x710 1))))
-(let ((@x563 (trans @x559 (symm @x610 (= 1 (+ 1 ?x730))) (= ?x710 (+ 1 ?x730)))))
-(let ((@x539 (symm (monotonicity @x563 (= ?x713 (nat$ (+ 1 ?x730)))) (= (nat$ (+ 1 ?x730)) ?x713))))
-(let ((?x437 (+ 1 ?x730)))
-(let ((?x440 (nat$ ?x437)))
-(let ((?x431 (cons$ 3 nil$)))
-(let ((?x728 (size$a ?x431)))
-(let (($x719 (= ?x728 ?x440)))
-(let (($x826 (forall ((?v0 Int) (?v1 Int_list$) )(!(= (size$a (cons$ ?v0 ?v1)) (nat$ (+ 1 (of_nat$ (size$a ?v1))))) :pattern ( (cons$ ?v0 ?v1) )))
+(let (($x119 (forall ((?v0 Int) (?v1 Int_list$) )(= (size$a (cons$ ?v0 ?v1)) (plus$ (size$a ?v1) (suc$ zero$))))
 ))
-(let (($x202 (forall ((?v0 Int) (?v1 Int_list$) )(= (size$a (cons$ ?v0 ?v1)) (nat$ (+ 1 (of_nat$ (size$a ?v1))))))
-))
-(let (($x199 (= (size$a (cons$ ?1 ?0)) (nat$ (+ 1 (of_nat$ (size$a ?0)))))))
-(let (($x186 (forall ((?v0 Int) (?v1 Int_list$) )(= (size$a (cons$ ?v0 ?v1)) (nat$ (+ (of_nat$ (size$a ?v1)) (+ 0 1)))))
-))
-(let (($x185 (= (size$a (cons$ ?1 ?0)) (nat$ (+ (of_nat$ (size$a ?0)) ?x92)))))
-(let (($x197 (= (nat$ (+ (of_nat$ (size$a ?0)) ?x92)) (nat$ (+ 1 (of_nat$ (size$a ?0)))))))
-(let ((?x67 (size$a ?0)))
-(let ((?x181 (of_nat$ ?x67)))
-(let ((?x191 (+ 1 ?x181)))
-(let ((?x183 (+ ?x181 ?x92)))
-(let ((@x195 (trans (monotonicity (rewrite (= ?x92 1)) (= ?x183 (+ ?x181 1))) (rewrite (= (+ ?x181 1) ?x191)) (= ?x183 ?x191))))
-(let ((@x204 (quant-intro (monotonicity (monotonicity @x195 $x197) (= $x185 $x199)) (= $x186 $x202))))
-(let ((@x328 (mp~ (mp (asserted $x186) @x204 $x202) (nnf-pos (refl (~ $x199 $x199)) (~ $x202 $x202)) $x202)))
-(let ((@x831 (mp @x328 (quant-intro (refl (= $x199 $x199)) (= $x202 $x826)) $x826)))
-(let (($x722 (or (not $x826) $x719)))
-(let ((@x723 ((_ quant-inst 3 nil$) $x722)))
-(let ((?x432 (g$a ?x431)))
-(let (($x729 (= ?x432 ?x728)))
-(let (($x784 (forall ((?v0 Int_list$) )(!(let ((?x67 (size$a ?v0)))
+(let (($x118 (= (size$a (cons$ ?1 ?0)) (plus$ (size$a ?0) ?x89))))
+(let ((@x178 (mp~ (asserted $x119) (nnf-pos (refl (~ $x118 $x118)) (~ $x119 $x119)) $x119)))
+(let ((@x669 (mp @x178 (quant-intro (refl (= $x118 $x118)) (= $x119 $x664)) $x664)))
+(let (($x231 (or (not $x664) $x584)))
+(let ((@x232 ((_ quant-inst 3 nil$) $x231)))
+(let ((?x267 (g$a ?x256)))
+(let (($x592 (= ?x267 ?x588)))
+(let (($x620 (forall ((?v0 Int_list$) )(!(let ((?x67 (size$a ?v0)))
 (let ((?x66 (g$a ?v0)))
 (= ?x66 ?x67))) :pattern ( (g$a ?v0) ) :pattern ( (size$a ?v0) )))
 ))
@@ -5810,27 +4710,27 @@
 (let ((?x66 (g$a ?v0)))
 (= ?x66 ?x67))))
 ))
-(let ((@x788 (quant-intro (refl (= (= (g$a ?0) ?x67) (= (g$a ?0) ?x67))) (= $x69 $x784))))
-(let ((@x295 (nnf-pos (refl (~ (= (g$a ?0) ?x67) (= (g$a ?0) ?x67))) (~ $x69 $x69))))
-(let ((@x789 (mp (mp~ (asserted $x69) @x295 $x69) @x788 $x784)))
-(let (($x438 (or (not $x784) $x729)))
-(let ((@x439 ((_ quant-inst (cons$ 3 nil$)) $x438)))
-(let (($x433 (= ?x208 ?x432)))
-(let (($x760 (forall ((?v0 Int) )(!(= (g$ (some$ ?v0)) (g$a (cons$ ?v0 nil$))) :pattern ( (some$ ?v0) ) :pattern ( (cons$ ?v0 nil$) )))
+(let ((@x622 (refl (= (= (g$a ?0) (size$a ?0)) (= (g$a ?0) (size$a ?0))))))
+(let ((@x129 (nnf-pos (refl (~ (= (g$a ?0) (size$a ?0)) (= (g$a ?0) (size$a ?0)))) (~ $x69 $x69))))
+(let ((@x625 (mp (mp~ (asserted $x69) @x129 $x69) (quant-intro @x622 (= $x69 $x620)) $x620)))
+(let (($x248 (or (not $x620) $x592)))
+(let ((@x585 ((_ quant-inst (cons$ 3 nil$)) $x248)))
+(let (($x268 (= ?x123 ?x267)))
+(let (($x596 (forall ((?v0 Int) )(!(= (g$ (some$ ?v0)) (g$a (cons$ ?v0 nil$))) :pattern ( (some$ ?v0) ) :pattern ( (cons$ ?v0 nil$) )))
 ))
 (let (($x34 (forall ((?v0 Int) )(= (g$ (some$ ?v0)) (g$a (cons$ ?v0 nil$))))
 ))
 (let (($x33 (= (g$ (some$ ?0)) (g$a (cons$ ?0 nil$)))))
-(let ((@x297 (mp~ (asserted $x34) (nnf-pos (refl (~ $x33 $x33)) (~ $x34 $x34)) $x34)))
-(let ((@x765 (mp @x297 (quant-intro (refl (= $x33 $x33)) (= $x34 $x760)) $x760)))
-(let (($x750 (or (not $x760) $x433)))
-(let ((@x751 ((_ quant-inst 3) $x750)))
-(let ((@x550 (trans (unit-resolution @x751 @x765 $x433) (unit-resolution @x439 @x789 $x729) (= ?x208 ?x728))))
-(let ((@x554 (trans (trans @x550 (unit-resolution @x723 @x831 $x719) (= ?x208 ?x440)) @x539 (= ?x208 ?x713))))
-(let ((@x525 (trans @x554 (symm (unit-resolution @x556 @x824 $x714) (= ?x713 ?x720)) (= ?x208 ?x720))))
-(let ((@x527 (trans @x525 (symm (unit-resolution @x712 @x781 $x444) (= ?x720 ?x435)) (= ?x208 ?x435))))
-(let ((@x528 (trans @x527 (symm (unit-resolution @x752 @x773 $x406) (= ?x435 ?x210)) $x211)))
-(let (($x212 (not $x211)))
-(let ((@x213 (asserted $x212)))
-(unit-resolution @x213 @x528 false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(let ((@x157 (mp~ (asserted $x34) (nnf-pos (refl (~ $x33 $x33)) (~ $x34 $x34)) $x34)))
+(let ((@x601 (mp @x157 (quant-intro (refl (= $x33 $x33)) (= $x34 $x596)) $x596)))
+(let (($x250 (or (not $x596) $x268)))
+(let ((@x586 ((_ quant-inst 3) $x250)))
+(let ((@x275 (trans (unit-resolution @x586 @x601 $x268) (unit-resolution @x585 @x625 $x592) (= ?x123 ?x588))))
+(let ((@x280 (trans (trans @x275 (unit-resolution @x232 @x669 $x584) (= ?x123 ?x246)) (symm @x287 (= ?x246 ?x233)) (= ?x123 ?x233))))
+(let ((@x558 (trans @x280 (symm (unit-resolution @x213 @x662 $x570) (= ?x233 ?x227)) (= ?x123 ?x227))))
+(let ((@x560 (trans @x558 (symm (unit-resolution @x572 @x617 $x569) (= ?x227 ?x270)) (= ?x123 ?x270))))
+(let ((@x546 (trans @x560 (symm (unit-resolution @x255 @x609 $x587) (= ?x270 ?x125)) $x126)))
+(let (($x127 (not $x126)))
+(let ((@x128 (asserted $x127)))
+(unit-resolution @x128 @x546 false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 
diff -r 987c9ceeaafd -r fb71c6f100f8 src/HOL/SMT_Examples/SMT_Examples.thy
--- a/src/HOL/SMT_Examples/SMT_Examples.thy	Sun Jul 27 15:44:08 2014 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Sun Jul 27 21:11:35 2014 +0200
@@ -393,27 +393,6 @@
   by smt (* smt2 FIXME: "th-lemma" tactic fails *)
 
 
-subsection {* Linear arithmetic for natural numbers *}
-
-lemma "2 * (x::nat) ~= 1" by smt2
-
-lemma "a < 3 \<Longrightarrow> (7::nat) > 2 * a" by smt2
-
-lemma "let x = (1::nat) + y in x - y > 0 * x" by smt2
-
-lemma
-  "let x = (1::nat) + y in
-   let P = (if x > 0 then True else False) in
-   False \<or> P = (x - 1 = y) \<or> (\<not>P \<longrightarrow> False)"
-  by smt2
-
-lemma "int (nat \<bar>x::int\<bar>) = \<bar>x\<bar>" by smt2
-
-definition prime_nat :: "nat \<Rightarrow> bool" where
-  "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
-lemma "prime_nat (4*m + 1) \<Longrightarrow> m \<ge> (1::nat)" by (smt2 prime_nat_def)
-
-
 section {* Pairs *}
 
 lemma "fst (x, y) = a \<Longrightarrow> x = a"
@@ -444,30 +423,28 @@
 
 lemma True using let_rsp by smt2
 lemma "le = op \<le> \<Longrightarrow> le (3::int) 42" by smt2
-lemma "map (\<lambda>i::nat. i + 1) [0, 1] = [1, 2]" by (smt2 list.map)
+lemma "map (\<lambda>i::int. i + 1) [0, 1] = [1, 2]" by (smt2 list.map)
 lemma "(ALL x. P x) \<or> ~ All P" by smt2
 
-fun dec_10 :: "nat \<Rightarrow> nat" where
+fun dec_10 :: "int \<Rightarrow> int" where
   "dec_10 n = (if n < 10 then n else dec_10 (n - 10))"
 
 lemma "dec_10 (4 * dec_10 4) = 6" by (smt2 dec_10.simps)
 
 axiomatization
-  eval_dioph :: "int list \<Rightarrow> nat list \<Rightarrow> int"
+  eval_dioph :: "int list \<Rightarrow> int list \<Rightarrow> int"
 where
-  eval_dioph_mod:
-  "eval_dioph ks xs mod int n = eval_dioph ks (map (\<lambda>x. x mod n) xs) mod int n"
+  eval_dioph_mod: "eval_dioph ks xs mod n = eval_dioph ks (map (\<lambda>x. x mod n) xs) mod n"
 and
   eval_dioph_div_mult:
-  "eval_dioph ks (map (\<lambda>x. x div n) xs) * int n +
+  "eval_dioph ks (map (\<lambda>x. x div n) xs) * n +
    eval_dioph ks (map (\<lambda>x. x mod n) xs) = eval_dioph ks xs"
 
 lemma
   "(eval_dioph ks xs = l) =
    (eval_dioph ks (map (\<lambda>x. x mod 2) xs) mod 2 = l mod 2 \<and>
-    eval_dioph ks (map (\<lambda>x. x div 2) xs) =
-      (l - eval_dioph ks (map (\<lambda>x. x mod 2) xs)) div 2)"
-  using [[smt2_oracle=true]] (*FIXME*)
+    eval_dioph ks (map (\<lambda>x. x div 2) xs) = (l - eval_dioph ks (map (\<lambda>x. x mod 2) xs)) div 2)"
+  using [[smt2_oracle = true]] (*FIXME*)
   using [[z3_new_extensions]]
   by (smt2 eval_dioph_mod[where n=2] eval_dioph_div_mult[where n=2])
 
diff -r 987c9ceeaafd -r fb71c6f100f8 src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Sun Jul 27 15:44:08 2014 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Sun Jul 27 21:11:35 2014 +0200
@@ -223,119 +223,6 @@
   by smt2+
 
 
-section {* Natural numbers *}
-
-lemma
-  "(0::nat) = 0"
-  "(1::nat) = 1"
-  "(0::nat) < 1"
-  "(0::nat) \<le> 1"
-  "(123456789::nat) < 2345678901"
-  by smt2+
-
-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 smt2+
-
-lemma
-  "(x::nat) + 0 = x"
-  "0 + x = x"
-  "x + y = y + x"
-  "x + (y + z) = (x + y) + z"
-  "(x + y = 0) = (x = 0 \<and> y = 0)"
-  by smt2+
-
-lemma
-  "(x::nat) - 0 = x"
-  "x < y \<longrightarrow> x - y = 0"
-  "x - y = 0 \<or> y - x = 0"
-  "(x - y) + y = (if x < y then y else x)"
-  "x - y - z = x - (y + z)"
-  by smt2+
-
-lemma
-  "(x::nat) * 0 = 0"
-  "0 * x = 0"
-  "x * 1 = x"
-  "1 * x = x"
-  "3 * x = x * 3"
-  by smt2+
-
-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 \<le> x"
-  "(x div 3 = x) = (x = 0)"
-  using [[z3_new_extensions]]
-  by smt2+
-
-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_new_extensions]]
-  by smt2+
-
-lemma
-  "(x::nat) = x div 1 * 1 + x mod 1"
-  "x = x div 3 * 3 + x mod 3"
-  using [[z3_new_extensions]]
-  by smt2+
-
-lemma
-  "min (x::nat) y \<le> x"
-  "min x y \<le> y"
-  "min x y \<le> x + y"
-  "z < x \<and> z < y \<longrightarrow> z < min x y"
-  "min x y = min y x"
-  "min x 0 = 0"
-  by smt2+
-
-lemma
-  "max (x::nat) y \<ge> x"
-  "max x y \<ge> y"
-  "max x y \<ge> (x - y) + (y - x)"
-  "z > x \<and> z > y \<longrightarrow> z > max x y"
-  "max x y = max y x"
-  "max x 0 = x"
-  by smt2+
-
-lemma
-  "0 \<le> (x::nat)"
-  "0 < x \<and> x \<le> 1 \<longrightarrow> x = 1"
-  "x \<le> x"
-  "x \<le> y \<longrightarrow> 3 * x \<le> 3 * y"
-  "x < y \<longrightarrow> 3 * x < 3 * y"
-  "x < y \<longrightarrow> x \<le> y"
-  "(x < y) = (x + 1 \<le> y)"
-  "\<not> (x < x)"
-  "x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
-  "x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
-  "x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z"
-  "x < y \<longrightarrow> y < z \<longrightarrow> x < z"
-  "x < y \<and> y < z \<longrightarrow> \<not> (z < x)"
-  by smt2+
-
-
 section {* Integers *}
 
 lemma
diff -r 987c9ceeaafd -r fb71c6f100f8 src/HOL/SMT_Examples/SMT_Word_Examples.certs2
--- a/src/HOL/SMT_Examples/SMT_Word_Examples.certs2	Sun Jul 27 15:44:08 2014 +0200
+++ b/src/HOL/SMT_Examples/SMT_Word_Examples.certs2	Sun Jul 27 21:11:35 2014 +0200
@@ -43,6 +43,14 @@
 (let ((@x49 (trans @x45 (rewrite (= (not true) false)) (= (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) false))))
 (mp (asserted (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)))) @x49 false)))))))
 
+6dd848d7b26e0521039e21a5e2bafebc1fee8c9b 7 0
+unsat
+((set-logic <null>)
+(proof
+(let ((@x35 (monotonicity (rewrite (= (= (_ bv11 5) (_ bv11 5)) true)) (= (not (= (_ bv11 5) (_ bv11 5))) (not true)))))
+(let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 5) (_ bv11 5))) false))))
+(mp (asserted (not (= (_ bv11 5) (_ bv11 5)))) @x39 false)))))
+
 45bf9e0a746f7dde46f8242e5851928c2671c7f2 9 0
 unsat
 ((set-logic <null>)
@@ -53,14 +61,6 @@
 (let ((@x54 (trans @x50 (rewrite (= (not true) false)) (= (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8)))) false))))
 (mp (asserted (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))))) @x54 false)))))))
 
-6dd848d7b26e0521039e21a5e2bafebc1fee8c9b 7 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x35 (monotonicity (rewrite (= (= (_ bv11 5) (_ bv11 5)) true)) (= (not (= (_ bv11 5) (_ bv11 5))) (not true)))))
-(let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 5) (_ bv11 5))) false))))
-(mp (asserted (not (= (_ bv11 5) (_ bv11 5)))) @x39 false)))))
-
 00a7ff287d9c23d984163ea8e0cac8ac61008afd 11 0
 unsat
 ((set-logic <null>)
@@ -142,15 +142,6 @@
 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) false))))
 (mp (asserted (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)))) @x48 false)))))))
 
-3838eb33edcd292c3a0ecbf1662b54af3940189f 8 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x36 (monotonicity (rewrite (= (bvnot (_ bv240 16)) (_ bv65295 16))) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) (= (_ bv65295 16) (_ bv65295 16))))))
-(let ((@x40 (trans @x36 (rewrite (= (= (_ bv65295 16) (_ bv65295 16)) true)) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) true))))
-(let ((@x47 (trans (monotonicity @x40 (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) (not true))) (rewrite (= (not true) false)) (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) false))))
-(mp (asserted (not (= (bvnot (_ bv240 16)) (_ bv65295 16)))) @x47 false))))))
-
 14431ccb33137348161eb6ca6cfb2e57942c3f9d 9 0
 unsat
 ((set-logic <null>)
@@ -161,6 +152,24 @@
 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) false))))
 (mp (asserted (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)))) @x48 false)))))))
 
+3838eb33edcd292c3a0ecbf1662b54af3940189f 8 0
+unsat
+((set-logic <null>)
+(proof
+(let ((@x36 (monotonicity (rewrite (= (bvnot (_ bv240 16)) (_ bv65295 16))) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) (= (_ bv65295 16) (_ bv65295 16))))))
+(let ((@x40 (trans @x36 (rewrite (= (= (_ bv65295 16) (_ bv65295 16)) true)) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) true))))
+(let ((@x47 (trans (monotonicity @x40 (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) (not true))) (rewrite (= (not true) false)) (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) false))))
+(mp (asserted (not (= (bvnot (_ bv240 16)) (_ bv65295 16)))) @x47 false))))))
+
+8d29c9b5ef712a3d9d2db87383c9c25c0b553e01 8 0
+unsat
+((set-logic <null>)
+(proof
+(let ((@x36 (monotonicity (rewrite (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) (= (_ bv3 2) (_ bv3 2))))))
+(let ((@x40 (trans @x36 (rewrite (= (= (_ bv3 2) (_ bv3 2)) true)) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) true))))
+(let ((@x47 (trans (monotonicity @x40 (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (not true))) (rewrite (= (not true) false)) (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) false))))
+(mp (asserted (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)))) @x47 false))))))
+
 880bee16a8f6469b14122277b92e87533ef6a071 9 0
 unsat
 ((set-logic <null>)
@@ -171,15 +180,6 @@
 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) false))))
 (mp (asserted (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)))) @x48 false)))))))
 
-6b4cf44be412b1ba63dbf9b301260e877097b1be 8 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x36 (monotonicity (rewrite (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) (= (_ bv3 2) (_ bv3 2))))))
-(let ((@x40 (trans @x36 (rewrite (= (= (_ bv3 2) (_ bv3 2)) true)) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) true))))
-(let ((@x47 (trans (monotonicity @x40 (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (not true))) (rewrite (= (not true) false)) (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) false))))
-(mp (asserted (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)))) @x47 false))))))
-
 446b3cb9d63aa1f488dc092ed3fb111d2ad50b4e 9 0
 unsat
 ((set-logic <null>)
@@ -200,7 +200,7 @@
 (let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) false))))
 (mp (asserted (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)))) @x47 false)))))))
 
-7a821bfbd2032abe40931e46e7875c58d78cac74 9 0
+8e075e24ee51b2c8d282203ef406cf993a4d32e8 9 0
 unsat
 ((set-logic <null>)
 (proof
@@ -210,7 +210,7 @@
 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) false))))
 (mp (asserted (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)))) @x48 false)))))))
 
-3a90f9cf3517f16b198f07da78a10c267f6ca981 9 0
+e11f6641dec327aa96166093ca6eb62aa10965c0 9 0
 unsat
 ((set-logic <null>)
 (proof
@@ -220,7 +220,7 @@
 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) false))))
 (mp (asserted (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)))) @x48 false)))))))
 
-512889429971c22172b835746742cd1214354685 9 0
+f1f29c69ebfcb6af36e96ba5a738d9b0d7b31835 9 0
 unsat
 ((set-logic <null>)
 (proof
@@ -230,7 +230,7 @@
 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) false))))
 (mp (asserted (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)))) @x48 false)))))))
 
-85eb639dc934d6e3f29fcc025e09dac5e8ec35be 9 0
+d5599ccc28266367053026b485d411472eb0665c 9 0
 unsat
 ((set-logic <null>)
 (proof
@@ -240,16 +240,6 @@
 (let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) false))))
 (mp (asserted (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)))) @x47 false)))))))
 
-072b118d30c575706ced09a142498447b46fa41f 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x36 (monotonicity (rewrite (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) (= (_ bv13 4) (_ bv13 4))))))
-(let ((@x40 (trans @x36 (rewrite (= (= (_ bv13 4) (_ bv13 4)) true)) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) true))))
-(let ((@x43 (monotonicity @x40 (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (not true)))))
-(let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) false))))
-(mp (asserted (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)))) @x47 false)))))))
-
 5c4e275bed2d91897e820ccd6744b0a775a6e26e 17 0
 unsat
 ((set-logic <null>)
@@ -268,6 +258,46 @@
 (let ((@x55 (unit-resolution ((_ th-lemma bv) $x53) @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 $x52)))
 (unit-resolution @x55 @x63 false)))))))))))))))
 
+33a52e620069e1ecebbc00aa6b0099170558c111 9 0
+unsat
+((set-logic <null>)
+(proof
+(let ((@x36 (monotonicity (rewrite (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) (= (_ bv13 4) (_ bv13 4))))))
+(let ((@x40 (trans @x36 (rewrite (= (= (_ bv13 4) (_ bv13 4)) true)) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) true))))
+(let ((@x43 (monotonicity @x40 (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (not true)))))
+(let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) false))))
+(mp (asserted (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)))) @x47 false)))))))
+
+115ab22c9945d493b971e69a38d9e608c5b40a71 29 0
+unsat
+((set-logic <null>)
+(proof
+(let ((?x28 (bv2int$ (_ bv0 2))))
+(let (($x183 (<= ?x28 0)))
+(let (($x184 (not $x183)))
+(let (($x175 (forall ((?v0 (_ BitVec 2)) )(!(let ((?x47 (bv2int$ ?v0)))
+(let (($x53 (<= ?x47 0)))
+(not $x53))) :pattern ( (bv2int$ ?v0) )))
+))
+(let (($x57 (forall ((?v0 (_ BitVec 2)) )(let ((?x47 (bv2int$ ?v0)))
+(let (($x53 (<= ?x47 0)))
+(not $x53))))
+))
+(let ((@x177 (refl (= (not (<= (bv2int$ ?0) 0)) (not (<= (bv2int$ ?0) 0))))))
+(let ((@x112 (refl (~ (not (<= (bv2int$ ?0) 0)) (not (<= (bv2int$ ?0) 0))))))
+(let (($x49 (forall ((?v0 (_ BitVec 2)) )(let ((?x47 (bv2int$ ?v0)))
+(< 0 ?x47)))
+))
+(let ((@x56 (rewrite (= (< 0 (bv2int$ ?0)) (not (<= (bv2int$ ?0) 0))))))
+(let ((@x115 (mp~ (mp (asserted $x49) (quant-intro @x56 (= $x49 $x57)) $x57) (nnf-pos @x112 (~ $x57 $x57)) $x57)))
+(let ((@x180 (mp @x115 (quant-intro @x177 (= $x57 $x175)) $x175)))
+(let (($x187 (not $x175)))
+(let (($x188 (or $x187 $x184)))
+(let ((@x189 ((_ quant-inst (_ bv0 2)) $x188)))
+(let (($x29 (= ?x28 0)))
+(let ((@x30 (asserted $x29)))
+(unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x29) $x183)) @x30 (unit-resolution @x189 @x180 $x184) false)))))))))))))))))))
+
 1d4a0e2a4449a8adbcf5a134bf7f2b0ee940d954 51 0
 unsat
 ((set-logic <null>)
@@ -320,36 +350,6 @@
 (let ((@x314 (unit-resolution ((_ th-lemma bv) $x312) @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 (unit-resolution (def-axiom (or $x95 (not $x74))) @x303 (not $x74)) (unit-resolution (def-axiom (or $x95 (not $x75))) @x303 (not $x75)) (unit-resolution (def-axiom (or $x95 (not $x76))) @x303 (not $x76)) (unit-resolution (def-axiom (or $x95 (not $x77))) @x303 (not $x77)) (unit-resolution (def-axiom (or $x95 (not $x78))) @x303 (not $x78)) (unit-resolution (def-axiom (or $x95 (not $x79))) @x303 (not $x79)) (unit-resolution (def-axiom (or $x95 (not $x80))) @x303 (not $x80)) (unit-resolution (def-axiom (or $x95 $x264)) @x303 $x264) $x300)))
 (unit-resolution @x314 @x322 false)))))))))))))))))))))))))))))))))))))))))))))))))
 
-115ab22c9945d493b971e69a38d9e608c5b40a71 29 0
-unsat
-((set-logic <null>)
-(proof
-(let ((?x28 (bv2int$ (_ bv0 2))))
-(let (($x183 (<= ?x28 0)))
-(let (($x184 (not $x183)))
-(let (($x175 (forall ((?v0 (_ BitVec 2)) )(!(let ((?x47 (bv2int$ ?v0)))
-(let (($x53 (<= ?x47 0)))
-(not $x53))) :pattern ( (bv2int$ ?v0) )))
-))
-(let (($x57 (forall ((?v0 (_ BitVec 2)) )(let ((?x47 (bv2int$ ?v0)))
-(let (($x53 (<= ?x47 0)))
-(not $x53))))
-))
-(let ((@x177 (refl (= (not (<= (bv2int$ ?0) 0)) (not (<= (bv2int$ ?0) 0))))))
-(let ((@x112 (refl (~ (not (<= (bv2int$ ?0) 0)) (not (<= (bv2int$ ?0) 0))))))
-(let (($x49 (forall ((?v0 (_ BitVec 2)) )(let ((?x47 (bv2int$ ?v0)))
-(< 0 ?x47)))
-))
-(let ((@x56 (rewrite (= (< 0 (bv2int$ ?0)) (not (<= (bv2int$ ?0) 0))))))
-(let ((@x115 (mp~ (mp (asserted $x49) (quant-intro @x56 (= $x49 $x57)) $x57) (nnf-pos @x112 (~ $x57 $x57)) $x57)))
-(let ((@x180 (mp @x115 (quant-intro @x177 (= $x57 $x175)) $x175)))
-(let (($x187 (not $x175)))
-(let (($x188 (or $x187 $x184)))
-(let ((@x189 ((_ quant-inst (_ bv0 2)) $x188)))
-(let (($x29 (= ?x28 0)))
-(let ((@x30 (asserted $x29)))
-(unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x29) $x183)) @x30 (unit-resolution @x189 @x180 $x184) false)))))))))))))))))))
-
 d14e7b8f0d1858316e700b4eb09e7d03e57cf9c3 16 0
 unsat
 ((set-logic <null>)
diff -r 987c9ceeaafd -r fb71c6f100f8 src/HOL/Tools/SMT2/smt2_normalize.ML
--- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Sun Jul 27 15:44:08 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Sun Jul 27 21:11:35 2014 +0200
@@ -324,84 +324,6 @@
 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 div (nat)}, @{const mod (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 int_0 int_1 int_Suc int_plus int_minus int_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 = SMT2_Util.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
-      val ctxt' = put_simpset HOL_ss ctxt addsimps @{thms Int.int_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 =
-    SMT2_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 = SMT2_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 =
-  SMT2_Builtin.add_builtin_typ_ext (@{typ nat}, K true) #>
-  fold (SMT2_Builtin.add_builtin_fun_ext' o Term.dest_Const) builtin_nat_ops
-
-end
-
-
 (** normalize numerals **)
 
 local
@@ -414,14 +336,12 @@
         true
     | is_irregular_number (Const (@{const_name uminus}, _) $ Const (@{const_name Groups.zero}, _)) =
         true
-    | is_irregular_number _ =
-        false;
+    | is_irregular_number _ = false
 
-  fun is_strange_number ctxt t = is_irregular_number t andalso SMT2_Builtin.is_builtin_num ctxt t;
+  fun is_strange_number ctxt t = is_irregular_number t andalso SMT2_Builtin.is_builtin_num ctxt t
 
   val proper_num_ss =
-    simpset_of (put_simpset HOL_ss @{context}
-      addsimps @{thms Num.numeral_One minus_zero})
+    simpset_of (put_simpset HOL_ss @{context} addsimps @{thms Num.numeral_One minus_zero})
 
   fun norm_num_conv ctxt =
     SMT2_Util.if_conv (is_strange_number ctxt) (Simplifier.rewrite (put_simpset proper_num_ss ctxt))
@@ -439,10 +359,13 @@
 fun unfold_conv ctxt =
   rewrite_case_bool_conv ctxt then_conv
   unfold_abs_min_max_conv ctxt then_conv
-  nat_as_int_conv ctxt then_conv
   Thm.beta_conversion true
 
-fun unfold1 ctxt = map (apsnd (Conv.fconv_rule (unfold_conv ctxt)))
+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
@@ -450,14 +373,6 @@
     val (thms', extra_thms) = f thms
   in (is ~~ thms') @ map (pair ~1) extra_thms end
 
-fun unfold2 ctxt ithms =
-  ithms
-  |> map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt)))
-  |> 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
@@ -511,9 +426,9 @@
   wthms
   |> map_index I
   |> gen_normalize ctxt
-  |> unfold1 ctxt
+  |> unfold_polymorph ctxt
   |> monomorph ctxt
-  |> unfold2 ctxt
+  |> unfold_monomorph ctxt
   |> apply_extra_norms ctxt
 
 val _ = Theory.setup (Context.theory_map (
@@ -521,7 +436,6 @@
   setup_unfolded_quants #>
   setup_trigger #>
   setup_case_bool #>
-  setup_abs_min_max #>
-  setup_nat_as_int))
+  setup_abs_min_max))
 
 end;
diff -r 987c9ceeaafd -r fb71c6f100f8 src/HOL/Word/Tools/smt2_word.ML
--- a/src/HOL/Word/Tools/smt2_word.ML	Sun Jul 27 15:44:08 2014 +0200
+++ b/src/HOL/Word/Tools/smt2_word.ML	Sun Jul 27 21:11:35 2014 +0200
@@ -12,7 +12,7 @@
 
 (* SMT-LIB logic *)
 
-(* "QF_AUFBV" is too restricted for Isabelle's problems, which contain aritmetic and quantifiers.
+(* "QF_AUFBV" is too restrictive for Isabelle's problems, which contain aritmetic and quantifiers.
    Better set the logic to "" and make at least Z3 happy. *)
 fun smtlib_logic ts =
   if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "" else NONE
@@ -38,9 +38,7 @@
   fun if_fixed pred m n T ts =
     let val (Us, U) = Term.strip_type T
     in
-      if pred (U, Us) then
-        SOME (n, length Us, ts, Term.list_comb o pair (Const (m, T)))
-      else NONE
+      if pred (U, Us) then SOME (n, length Us, ts, Term.list_comb o pair (Const (m, T))) else NONE
     end
 
   fun if_fixed_all m = if_fixed (forall (can dest_wordT) o (op ::)) m
@@ -50,12 +48,7 @@
     let val (m, _) = Term.dest_Const t
     in SMT2_Builtin.add_builtin_fun smtlib2C (Term.dest_Const t, K (f m n)) end
 
-  fun hd2 xs = hd (tl xs)
-
-  fun mk_nat i = @{const nat} $ HOLogic.mk_number @{typ nat} i
-
-  fun dest_nat (@{const nat} $ n) = snd (HOLogic.dest_number n)
-    | dest_nat t = raise TERM ("not a natural number", [t])
+  val mk_nat = HOLogic.mk_number @{typ nat}
 
   fun mk_shift c [t, u] = Const c $ t $ mk_nat (snd (HOLogic.dest_number u))
     | mk_shift c ts = raise TERM ("bad arguments", Const c :: ts)
@@ -63,7 +56,7 @@
   fun shift m n T ts =
     let val U = Term.domain_type T
     in
-      (case (can dest_wordT U, try (dest_nat o hd2) ts) of
+      (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd o tl) ts) of
         (true, SOME i) =>
           SOME (n, 2, [hd ts, HOLogic.mk_number U i], mk_shift (m, T))
       | _ => NONE)   (* FIXME: also support non-numerical shifts *)
@@ -74,7 +67,7 @@
   fun extract m n T ts =
     let val U = Term.range_type (Term.range_type T)
     in
-      (case (try (dest_nat o hd) ts, try dest_wordT U) of
+      (case (try (snd o HOLogic.dest_number o hd) ts, try dest_wordT U) of
         (SOME lb, SOME i) =>
           SOME (index2 n (i + lb - 1) lb, 1, tl ts, mk_extract (m, T) lb)
       | _ => NONE)
@@ -97,7 +90,7 @@
   fun rotate m n T ts =
     let val U = Term.domain_type (Term.range_type T)
     in
-      (case (can dest_wordT U, try (dest_nat o hd) ts) of
+      (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd) ts) of
         (true, SOME i) => SOME (index1 n i, 1, tl ts, mk_rotate (m, T) i)
       | _ => NONE)
     end
diff -r 987c9ceeaafd -r fb71c6f100f8 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sun Jul 27 15:44:08 2014 +0200
+++ b/src/HOL/Word/Word.thy	Sun Jul 27 21:11:35 2014 +0200
@@ -4760,4 +4760,3 @@
 hide_const (open) Word
 
 end
-