src/HOL/SMT_Examples/SMT_Word_Examples.certs2
changeset 56079 175ac95720d4
child 56109 1ba56358eba4
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SMT_Examples/SMT_Word_Examples.certs2	Thu Mar 13 13:18:13 2014 +0100
     1.3 @@ -0,0 +1,434 @@
     1.4 +a438ed86857e9b990f36b8fba1876d2ee3208e44 8 0
     1.5 +unsat
     1.6 +((set-logic <null>)
     1.7 +(proof
     1.8 +(let ((@x17 (monotonicity (rewrite (= (bvneg (_ bv5 4)) (_ bv11 4))) (= (= (_ bv11 4) (bvneg (_ bv5 4))) (= (_ bv11 4) (_ bv11 4))))))
     1.9 +(let ((@x21 (trans @x17 (rewrite (= (= (_ bv11 4) (_ bv11 4)) true)) (= (= (_ bv11 4) (bvneg (_ bv5 4))) true))))
    1.10 +(let ((@x28 (trans (monotonicity @x21 (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) (not true))) (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) false))))
    1.11 +(mp (asserted (not (= (_ bv11 4) (bvneg (_ bv5 4))))) @x28 false))))))
    1.12 +
    1.13 +9b71beed4cadbb1c6e2962eb013e86c8f71abf17 9 0
    1.14 +unsat
    1.15 +((set-logic <null>)
    1.16 +(proof
    1.17 +(let ((@x20 (monotonicity (rewrite (= (bvule (_ bv27 8) (_ bv23 8)) false)) (= (not (bvule (_ bv27 8) (_ bv23 8))) (not false)))))
    1.18 +(let ((@x24 (trans @x20 (rewrite (= (not false) true)) (= (not (bvule (_ bv27 8) (_ bv23 8))) true))))
    1.19 +(let ((@x26 (trans (rewrite (= (bvult (_ bv23 8) (_ bv27 8)) (not (bvule (_ bv27 8) (_ bv23 8))))) @x24 (= (bvult (_ bv23 8) (_ bv27 8)) true))))
    1.20 +(let ((@x33 (trans (monotonicity @x26 (= (not (bvult (_ bv23 8) (_ bv27 8))) (not true))) (rewrite (= (not true) false)) (= (not (bvult (_ bv23 8) (_ bv27 8))) false))))
    1.21 +(mp (asserted (not (bvult (_ bv23 8) (_ bv27 8)))) @x33 false)))))))
    1.22 +
    1.23 +83e5e97d82127f63e5519904051508641143369d 7 0
    1.24 +unsat
    1.25 +((set-logic <null>)
    1.26 +(proof
    1.27 +(let ((@x15 (monotonicity (rewrite (= (= (_ bv11 4) (_ bv11 4)) true)) (= (not (= (_ bv11 4) (_ bv11 4))) (not true)))))
    1.28 +(let ((@x19 (trans @x15 (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (_ bv11 4))) false))))
    1.29 +(mp (asserted (not (= (_ bv11 4) (_ bv11 4)))) @x19 false)))))
    1.30 +
    1.31 +1e5c1dd05129223256f56ebbd2d47effcee4561c 9 0
    1.32 +unsat
    1.33 +((set-logic <null>)
    1.34 +(proof
    1.35 +(let ((@x17 (monotonicity (rewrite (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) (= (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)) (= (_ bv6 5) (_ bv6 5))))))
    1.36 +(let ((@x21 (trans @x17 (rewrite (= (= (_ bv6 5) (_ bv6 5)) true)) (= (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)) true))))
    1.37 +(let ((@x24 (monotonicity @x21 (= (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) (not true)))))
    1.38 +(let ((@x28 (trans @x24 (rewrite (= (not true) false)) (= (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) false))))
    1.39 +(mp (asserted (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)))) @x28 false)))))))
    1.40 +
    1.41 +2999cde57fdda8b4770e92440b939692e4a6aa5f 12 0
    1.42 +unsat
    1.43 +((set-logic <null>)
    1.44 +(proof
    1.45 +(let ((@x25 (monotonicity (rewrite (= (bvmul (_ bv255 8) (_ bv27 8)) (_ bv229 8))) (= (bvadd (_ bv11 8) (bvmul (_ bv255 8) (_ bv27 8))) (bvadd (_ bv11 8) (_ bv229 8))))))
    1.46 +(let ((@x30 (trans @x25 (rewrite (= (bvadd (_ bv11 8) (_ bv229 8)) (_ bv240 8))) (= (bvadd (_ bv11 8) (bvmul (_ bv255 8) (_ bv27 8))) (_ bv240 8)))))
    1.47 +(let ((@x32 (trans (rewrite (= (bvsub (_ bv11 8) (_ bv27 8)) (bvadd (_ bv11 8) (bvmul (_ bv255 8) (_ bv27 8))))) @x30 (= (bvsub (_ bv11 8) (_ bv27 8)) (_ bv240 8)))))
    1.48 +(let ((@x37 (monotonicity @x32 (rewrite (= (bvneg (_ bv16 8)) (_ bv240 8))) (= (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))) (= (_ bv240 8) (_ bv240 8))))))
    1.49 +(let ((@x41 (trans @x37 (rewrite (= (= (_ bv240 8) (_ bv240 8)) true)) (= (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))) true))))
    1.50 +(let ((@x44 (monotonicity @x41 (= (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8)))) (not true)))))
    1.51 +(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8)))) false))))
    1.52 +(mp (asserted (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))))) @x48 false))))))))))
    1.53 +
    1.54 +5276e53d12319b7263028b7b35a0e825901a044d 9 0
    1.55 +unsat
    1.56 +((set-logic <null>)
    1.57 +(proof
    1.58 +(let ((@x17 (monotonicity (rewrite (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) (= (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)) (= (_ bv21 8) (_ bv21 8))))))
    1.59 +(let ((@x21 (trans @x17 (rewrite (= (= (_ bv21 8) (_ bv21 8)) true)) (= (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)) true))))
    1.60 +(let ((@x24 (monotonicity @x21 (= (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) (not true)))))
    1.61 +(let ((@x28 (trans @x24 (rewrite (= (not true) false)) (= (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) false))))
    1.62 +(mp (asserted (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)))) @x28 false)))))))
    1.63 +
    1.64 +234b2b4e895fc2df774f19f02134d0ca4a5a16a1 7 0
    1.65 +unsat
    1.66 +((set-logic <null>)
    1.67 +(proof
    1.68 +(let ((@x15 (monotonicity (rewrite (= (= (_ bv11 5) (_ bv11 5)) true)) (= (not (= (_ bv11 5) (_ bv11 5))) (not true)))))
    1.69 +(let ((@x19 (trans @x15 (rewrite (= (not true) false)) (= (not (= (_ bv11 5) (_ bv11 5))) false))))
    1.70 +(mp (asserted (not (= (_ bv11 5) (_ bv11 5)))) @x19 false)))))
    1.71 +
    1.72 +dc503704730fb3b59f839ff9f108d372052a8660 11 0
    1.73 +unsat
    1.74 +((set-logic <null>)
    1.75 +(proof
    1.76 +(let ((@x21 (monotonicity (rewrite (= (bvneg (_ bv40 7)) (_ bv88 7))) (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvadd (_ bv88 7) (_ bv1 7))))))
    1.77 +(let ((@x26 (trans @x21 (rewrite (= (bvadd (_ bv88 7) (_ bv1 7)) (_ bv89 7))) (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (_ bv89 7)))))
    1.78 +(let ((@x31 (monotonicity @x26 (rewrite (= (bvneg (_ bv39 7)) (_ bv89 7))) (= (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))) (= (_ bv89 7) (_ bv89 7))))))
    1.79 +(let ((@x35 (trans @x31 (rewrite (= (= (_ bv89 7) (_ bv89 7)) true)) (= (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))) true))))
    1.80 +(let ((@x38 (monotonicity @x35 (= (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7)))) (not true)))))
    1.81 +(let ((@x42 (trans @x38 (rewrite (= (not true) false)) (= (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7)))) false))))
    1.82 +(mp (asserted (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))))) @x42 false)))))))))
    1.83 +
    1.84 +a1e71f94523b4cd464028b84ee475aaff660cb0f 16 0
    1.85 +unsat
    1.86 +((set-logic <null>)
    1.87 +(proof
    1.88 +(let ((?x12 (bvsub (bvadd (bvadd |$a| (bvmul (_ bv2 32) |$b|)) |$c|) |$b|)))
    1.89 +(let (($x15 (= ?x12 (bvadd (bvadd |$b| |$c|) |$a|))))
    1.90 +(let (($x16 (not $x15)))
    1.91 +(let ((@x45 (rewrite (= (= (bvadd |$a| |$b| |$c|) (bvadd |$b| |$c| |$a|)) true))))
    1.92 +(let ((?x33 (bvadd |$a| |$b| |$c|)))
    1.93 +(let ((?x20 (bvadd |$a| (bvmul (_ bv2 32) |$b|) |$c|)))
    1.94 +(let ((?x28 (bvadd ?x20 (bvmul (_ bv4294967295 32) |$b|))))
    1.95 +(let ((@x25 (monotonicity (rewrite (= (bvadd (bvadd |$a| (bvmul (_ bv2 32) |$b|)) |$c|) ?x20)) (= ?x12 (bvsub ?x20 |$b|)))))
    1.96 +(let ((@x37 (trans (trans @x25 (rewrite (= (bvsub ?x20 |$b|) ?x28)) (= ?x12 ?x28)) (rewrite (= ?x28 ?x33)) (= ?x12 ?x33))))
    1.97 +(let ((@x43 (monotonicity @x37 (rewrite (= (bvadd (bvadd |$b| |$c|) |$a|) (bvadd |$b| |$c| |$a|))) (= $x15 (= ?x33 (bvadd |$b| |$c| |$a|))))))
    1.98 +(let ((@x50 (monotonicity (trans @x43 @x45 (= $x15 true)) (= $x16 (not true)))))
    1.99 +(mp (asserted $x16) (trans @x50 (rewrite (= (not true) false)) (= $x16 false)) false))))))))))))))
   1.100 +
   1.101 +07ce4ddeaf1a897fd86c82ea0be2917368402c4b 14 0
   1.102 +unsat
   1.103 +((set-logic <null>)
   1.104 +(proof
   1.105 +(let (($x10 (= (bvmul (_ bv4 4) |$x|) (_ bv4 4))))
   1.106 +(let (($x7 (= |$x| (_ bv5 4))))
   1.107 +(let ((@x22 (monotonicity (rewrite (= (=> $x7 $x10) (or (not $x7) $x10))) (= (not (=> $x7 $x10)) (not (or (not $x7) $x10))))))
   1.108 +(let ((@x24 (|not-or-elim| (mp (asserted (not (=> $x7 $x10))) @x22 (not (or (not $x7) $x10))) $x7)))
   1.109 +(let ((@x32 (trans (monotonicity @x24 (= (bvmul (_ bv4 4) |$x|) (bvmul (_ bv4 4) (_ bv5 4)))) (rewrite (= (bvmul (_ bv4 4) (_ bv5 4)) (_ bv4 4))) $x10)))
   1.110 +(let ((@x39 (trans (monotonicity @x32 (= $x10 (= (_ bv4 4) (_ bv4 4)))) (rewrite (= (= (_ bv4 4) (_ bv4 4)) true)) (= $x10 true))))
   1.111 +(let ((@x46 (trans (monotonicity @x39 (= (not $x10) (not true))) (rewrite (= (not true) false)) (= (not $x10) false))))
   1.112 +(let (($x25 (not $x10)))
   1.113 +(let ((@x26 (|not-or-elim| (mp (asserted (not (=> $x7 $x10))) @x22 (not (or (not $x7) $x10))) $x25)))
   1.114 +(mp @x26 @x46 false))))))))))))
   1.115 +
   1.116 +bf082d012c77348e9e5c8d77f54b71808a9a2b45 13 0
   1.117 +unsat
   1.118 +((set-logic <null>)
   1.119 +(proof
   1.120 +(let (($x9 (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))))
   1.121 +(let ((@x28 (monotonicity (rewrite (= (bvnot (_ bv6 32)) (_ bv4294967289 32))) (rewrite (= (bvnot (_ bv5 32)) (_ bv4294967290 32))) (= (bvor (bvnot (_ bv6 32)) (bvnot (_ bv5 32))) (bvor (_ bv4294967289 32) (_ bv4294967290 32))))))
   1.122 +(let ((@x33 (trans @x28 (rewrite (= (bvor (_ bv4294967289 32) (_ bv4294967290 32)) (_ bv4294967291 32))) (= (bvor (bvnot (_ bv6 32)) (bvnot (_ bv5 32))) (_ bv4294967291 32)))))
   1.123 +(let ((@x36 (monotonicity @x33 (= (bvnot (bvor (bvnot (_ bv6 32)) (bvnot (_ bv5 32)))) (bvnot (_ bv4294967291 32))))))
   1.124 +(let ((@x40 (trans @x36 (rewrite (= (bvnot (_ bv4294967291 32)) (_ bv4 32))) (= (bvnot (bvor (bvnot (_ bv6 32)) (bvnot (_ bv5 32)))) (_ bv4 32)))))
   1.125 +(let ((@x19 (rewrite (= (bvand (_ bv6 32) (_ bv5 32)) (bvnot (bvor (bvnot (_ bv6 32)) (bvnot (_ bv5 32))))))))
   1.126 +(let ((@x48 (trans (monotonicity (trans @x19 @x40 $x9) (= $x9 (= (_ bv4 32) (_ bv4 32)))) (rewrite (= (= (_ bv4 32) (_ bv4 32)) true)) (= $x9 true))))
   1.127 +(let ((@x55 (trans (monotonicity @x48 (= (not $x9) (not true))) (rewrite (= (not true) false)) (= (not $x9) false))))
   1.128 +(mp (asserted (not $x9)) @x55 false)))))))))))
   1.129 +
   1.130 +224e3adf486b015b2b86fd13b422d3432d5dd2ea 9 0
   1.131 +unsat
   1.132 +((set-logic <null>)
   1.133 +(proof
   1.134 +(let ((@x17 (monotonicity (rewrite (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) (= (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)) (= (_ bv7 8) (_ bv7 8))))))
   1.135 +(let ((@x21 (trans @x17 (rewrite (= (= (_ bv7 8) (_ bv7 8)) true)) (= (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)) true))))
   1.136 +(let ((@x24 (monotonicity @x21 (= (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) (not true)))))
   1.137 +(let ((@x28 (trans @x24 (rewrite (= (not true) false)) (= (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) false))))
   1.138 +(mp (asserted (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)))) @x28 false)))))))
   1.139 +
   1.140 +6f410cdf4d96b9ee8b7b886db44e51fe495aad40 9 0
   1.141 +unsat
   1.142 +((set-logic <null>)
   1.143 +(proof
   1.144 +(let ((@x17 (monotonicity (rewrite (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) (= (_ bv15 8) (_ bv15 8))))))
   1.145 +(let ((@x21 (trans @x17 (rewrite (= (= (_ bv15 8) (_ bv15 8)) true)) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) true))))
   1.146 +(let ((@x24 (monotonicity @x21 (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (not true)))))
   1.147 +(let ((@x28 (trans @x24 (rewrite (= (not true) false)) (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) false))))
   1.148 +(mp (asserted (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)))) @x28 false)))))))
   1.149 +
   1.150 +75e911429d9da77b77c961a3f11bf4fae39c1289 8 0
   1.151 +unsat
   1.152 +((set-logic <null>)
   1.153 +(proof
   1.154 +(let ((@x16 (monotonicity (rewrite (= (bvnot (_ bv240 16)) (_ bv65295 16))) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) (= (_ bv65295 16) (_ bv65295 16))))))
   1.155 +(let ((@x20 (trans @x16 (rewrite (= (= (_ bv65295 16) (_ bv65295 16)) true)) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) true))))
   1.156 +(let ((@x27 (trans (monotonicity @x20 (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) (not true))) (rewrite (= (not true) false)) (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) false))))
   1.157 +(mp (asserted (not (= (bvnot (_ bv240 16)) (_ bv65295 16)))) @x27 false))))))
   1.158 +
   1.159 +144996e0132e6e5e8657189d4b8fc16447f15f7f 9 0
   1.160 +unsat
   1.161 +((set-logic <null>)
   1.162 +(proof
   1.163 +(let ((@x17 (monotonicity (rewrite (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) (= (_ bv2843 12) (_ bv2843 12))))))
   1.164 +(let ((@x21 (trans @x17 (rewrite (= (= (_ bv2843 12) (_ bv2843 12)) true)) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) true))))
   1.165 +(let ((@x24 (monotonicity @x21 (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (not true)))))
   1.166 +(let ((@x28 (trans @x24 (rewrite (= (not true) false)) (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) false))))
   1.167 +(mp (asserted (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)))) @x28 false)))))))
   1.168 +
   1.169 +dedf960210e12ce3dfe685dabb09a7ae103a6b34 9 0
   1.170 +unsat
   1.171 +((set-logic <null>)
   1.172 +(proof
   1.173 +(let ((@x17 (monotonicity (rewrite (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) (= (_ bv207 10) (_ bv207 10))))))
   1.174 +(let ((@x21 (trans @x17 (rewrite (= (= (_ bv207 10) (_ bv207 10)) true)) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) true))))
   1.175 +(let ((@x24 (monotonicity @x21 (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (not true)))))
   1.176 +(let ((@x28 (trans @x24 (rewrite (= (not true) false)) (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) false))))
   1.177 +(mp (asserted (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)))) @x28 false)))))))
   1.178 +
   1.179 +efa324caae835caf47cbb2d21e18358840d28baa 8 0
   1.180 +unsat
   1.181 +((set-logic <null>)
   1.182 +(proof
   1.183 +(let ((@x36 (monotonicity (rewrite (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) (= (_ bv3 2) (_ bv3 2))))))
   1.184 +(let ((@x40 (trans @x36 (rewrite (= (= (_ bv3 2) (_ bv3 2)) true)) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) true))))
   1.185 +(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))))
   1.186 +(mp (asserted (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)))) @x47 false))))))
   1.187 +
   1.188 +21eb47482df6fb5cf3198774bf96beedaec719a7 9 0
   1.189 +unsat
   1.190 +((set-logic <null>)
   1.191 +(proof
   1.192 +(let (($x8 (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))))
   1.193 +(let ((@x19 (trans (rewrite (= ((_ zero_extend 6) (_ bv10 4)) (concat (_ bv0 6) (_ bv10 4)))) (rewrite (= (concat (_ bv0 6) (_ bv10 4)) (_ bv10 10))) $x8)))
   1.194 +(let ((@x26 (trans (monotonicity @x19 (= $x8 (= (_ bv10 10) (_ bv10 10)))) (rewrite (= (= (_ bv10 10) (_ bv10 10)) true)) (= $x8 true))))
   1.195 +(let ((@x33 (trans (monotonicity @x26 (= (not $x8) (not true))) (rewrite (= (not true) false)) (= (not $x8) false))))
   1.196 +(mp (asserted (not $x8)) @x33 false)))))))
   1.197 +
   1.198 +4b811cc374f3df84ff1252430c602976203f62f2 9 0
   1.199 +unsat
   1.200 +((set-logic <null>)
   1.201 +(proof
   1.202 +(let ((@x16 (monotonicity (rewrite (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) (= (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)) (= (_ bv58 6) (_ bv58 6))))))
   1.203 +(let ((@x20 (trans @x16 (rewrite (= (= (_ bv58 6) (_ bv58 6)) true)) (= (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)) true))))
   1.204 +(let ((@x23 (monotonicity @x20 (= (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) (not true)))))
   1.205 +(let ((@x27 (trans @x23 (rewrite (= (not true) false)) (= (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) false))))
   1.206 +(mp (asserted (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)))) @x27 false)))))))
   1.207 +
   1.208 +80eccdbf8bbcc6ea1d4f3857bd01f3a1ad159ef2 9 0
   1.209 +unsat
   1.210 +((set-logic <null>)
   1.211 +(proof
   1.212 +(let ((@x37 (monotonicity (rewrite (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) (= (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)) (= (_ bv76 8) (_ bv76 8))))))
   1.213 +(let ((@x41 (trans @x37 (rewrite (= (= (_ bv76 8) (_ bv76 8)) true)) (= (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)) true))))
   1.214 +(let ((@x44 (monotonicity @x41 (= (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) (not true)))))
   1.215 +(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) false))))
   1.216 +(mp (asserted (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)))) @x48 false)))))))
   1.217 +
   1.218 +97eb054e915337f30396aae674e0c82d561ec48b 9 0
   1.219 +unsat
   1.220 +((set-logic <null>)
   1.221 +(proof
   1.222 +(let ((@x37 (monotonicity (rewrite (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) (= (_ bv4 8) (_ bv4 8))))))
   1.223 +(let ((@x41 (trans @x37 (rewrite (= (= (_ bv4 8) (_ bv4 8)) true)) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) true))))
   1.224 +(let ((@x44 (monotonicity @x41 (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (not true)))))
   1.225 +(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) false))))
   1.226 +(mp (asserted (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)))) @x48 false)))))))
   1.227 +
   1.228 +a91b3649f65952bf743777b618e6da6b37fcc95f 9 0
   1.229 +unsat
   1.230 +((set-logic <null>)
   1.231 +(proof
   1.232 +(let ((@x37 (monotonicity (rewrite (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) (= (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)) (= (_ bv6 8) (_ bv6 8))))))
   1.233 +(let ((@x41 (trans @x37 (rewrite (= (= (_ bv6 8) (_ bv6 8)) true)) (= (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)) true))))
   1.234 +(let ((@x44 (monotonicity @x41 (= (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) (not true)))))
   1.235 +(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) false))))
   1.236 +(mp (asserted (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)))) @x48 false)))))))
   1.237 +
   1.238 +329e4f3ee0408af9d367ae6246fb53276a50a32f 11 0
   1.239 +unsat
   1.240 +((set-logic <null>)
   1.241 +(proof
   1.242 +(let (($x8 (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))))
   1.243 +(let ((@x45 (monotonicity (rewrite (= ((_ extract 2 0) (_ bv14 4)) (_ bv6 3))) (rewrite (= ((_ extract 3 3) (_ bv14 4)) (_ bv1 1))) (= (concat ((_ extract 2 0) (_ bv14 4)) ((_ extract 3 3) (_ bv14 4))) (concat (_ bv6 3) (_ bv1 1))))))
   1.244 +(let ((@x49 (trans @x45 (rewrite (= (concat (_ bv6 3) (_ bv1 1)) (_ bv13 4))) (= (concat ((_ extract 2 0) (_ bv14 4)) ((_ extract 3 3) (_ bv14 4))) (_ bv13 4)))))
   1.245 +(let ((@x50 (trans (rewrite (= ((_ rotate_left 1) (_ bv14 4)) (concat ((_ extract 2 0) (_ bv14 4)) ((_ extract 3 3) (_ bv14 4))))) @x49 $x8)))
   1.246 +(let ((@x57 (trans (monotonicity @x50 (= $x8 (= (_ bv13 4) (_ bv13 4)))) (rewrite (= (= (_ bv13 4) (_ bv13 4)) true)) (= $x8 true))))
   1.247 +(let ((@x64 (trans (monotonicity @x57 (= (not $x8) (not true))) (rewrite (= (not true) false)) (= (not $x8) false))))
   1.248 +(mp (asserted (not $x8)) @x64 false)))))))))
   1.249 +
   1.250 +591572ec6e8cad807a5a51108eafba79636afecf 11 0
   1.251 +unsat
   1.252 +((set-logic <null>)
   1.253 +(proof
   1.254 +(let (($x8 (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))))
   1.255 +(let ((@x46 (monotonicity (rewrite (= ((_ extract 1 0) (_ bv6 4)) (_ bv2 2))) (rewrite (= ((_ extract 3 2) (_ bv6 4)) (_ bv1 2))) (= (concat ((_ extract 1 0) (_ bv6 4)) ((_ extract 3 2) (_ bv6 4))) (concat (_ bv2 2) (_ bv1 2))))))
   1.256 +(let ((@x50 (trans @x46 (rewrite (= (concat (_ bv2 2) (_ bv1 2)) (_ bv9 4))) (= (concat ((_ extract 1 0) (_ bv6 4)) ((_ extract 3 2) (_ bv6 4))) (_ bv9 4)))))
   1.257 +(let ((@x37 (rewrite (= ((_ rotate_right 2) (_ bv6 4)) (concat ((_ extract 1 0) (_ bv6 4)) ((_ extract 3 2) (_ bv6 4)))))))
   1.258 +(let ((@x58 (trans (monotonicity (trans @x37 @x50 $x8) (= $x8 (= (_ bv9 4) (_ bv9 4)))) (rewrite (= (= (_ bv9 4) (_ bv9 4)) true)) (= $x8 true))))
   1.259 +(let ((@x65 (trans (monotonicity @x58 (= (not $x8) (not true))) (rewrite (= (not true) false)) (= (not $x8) false))))
   1.260 +(mp (asserted (not $x8)) @x65 false)))))))))
   1.261 +
   1.262 +06e703e92f9238355e516e861c984a3eb7d984a8 44 0
   1.263 +unsat
   1.264 +((set-logic <null>)
   1.265 +(proof
   1.266 +(let ((?x9 (bvand |$x| (_ bv255 16))))
   1.267 +(let ((?x7 (bvand |$x| (_ bv65280 16))))
   1.268 +(let ((?x10 (bvor ?x7 ?x9)))
   1.269 +(let (($x11 (= ?x10 |$x|)))
   1.270 +(let (($x12 (not $x11)))
   1.271 +(let ((?x113 (concat ((_ extract 15 8) (concat ((_ extract 15 8) |$x|) (_ bv0 8))) ((_ extract 7 0) (concat (_ bv0 8) ((_ extract 7 0) |$x|))))))
   1.272 +(let ((@x124 (monotonicity (rewrite (= ((_ extract 15 8) (concat ((_ extract 15 8) |$x|) (_ bv0 8))) ((_ extract 15 8) |$x|))) (rewrite (= ((_ extract 7 0) (concat (_ bv0 8) ((_ extract 7 0) |$x|))) ((_ extract 7 0) |$x|))) (= ?x113 (concat ((_ extract 15 8) |$x|) ((_ extract 7 0) |$x|))))))
   1.273 +(let ((@x129 (trans @x124 (rewrite (= (concat ((_ extract 15 8) |$x|) ((_ extract 7 0) |$x|)) ((_ extract 15 0) |$x|))) (= ?x113 ((_ extract 15 0) |$x|)))))
   1.274 +(let (($x114 (= (bvor (concat ((_ extract 15 8) |$x|) (_ bv0 8)) (concat (_ bv0 8) ((_ extract 7 0) |$x|))) ?x113)))
   1.275 +(let (($x109 (= ?x10 (bvor (concat ((_ extract 15 8) |$x|) (_ bv0 8)) (concat (_ bv0 8) ((_ extract 7 0) |$x|))))))
   1.276 +(let ((?x81 ((_ extract 7 0) |$x|)))
   1.277 +(let ((?x101 (concat (_ bv0 8) ?x81)))
   1.278 +(let ((?x16 (bvnot |$x|)))
   1.279 +(let ((?x66 (bvor ?x16 (bvnot (_ bv255 16)))))
   1.280 +(let ((?x67 (bvnot ?x66)))
   1.281 +(let ((@x103 (monotonicity (rewrite (= (bvnot (_ bv255 8)) (_ bv0 8))) (rewrite (= (bvnot (bvnot ?x81)) ?x81)) (= (concat (bvnot (_ bv255 8)) (bvnot (bvnot ?x81))) ?x101))))
   1.282 +(let ((?x47 (bvnot (_ bv255 8))))
   1.283 +(let ((?x94 (concat ?x47 (bvnot (bvnot ?x81)))))
   1.284 +(let ((@x87 (monotonicity (rewrite (= ((_ extract 7 0) ?x16) (bvnot ?x81))) (= (concat (_ bv255 8) ((_ extract 7 0) ?x16)) (concat (_ bv255 8) (bvnot ?x81))))))
   1.285 +(let ((@x74 (monotonicity (rewrite (= (bvnot (_ bv255 16)) (_ bv65280 16))) (= ?x66 (bvor ?x16 (_ bv65280 16))))))
   1.286 +(let ((@x80 (trans @x74 (rewrite (= (bvor ?x16 (_ bv65280 16)) (concat (_ bv255 8) ((_ extract 7 0) ?x16)))) (= ?x66 (concat (_ bv255 8) ((_ extract 7 0) ?x16))))))
   1.287 +(let ((@x92 (monotonicity (trans @x80 @x87 (= ?x66 (concat (_ bv255 8) (bvnot ?x81)))) (= ?x67 (bvnot (concat (_ bv255 8) (bvnot ?x81)))))))
   1.288 +(let ((@x98 (trans @x92 (rewrite (= (bvnot (concat (_ bv255 8) (bvnot ?x81))) ?x94)) (= ?x67 ?x94))))
   1.289 +(let ((@x107 (trans (rewrite (= ?x9 ?x67)) (trans @x98 @x103 (= ?x67 ?x101)) (= ?x9 ?x101))))
   1.290 +(let ((?x34 ((_ extract 15 8) |$x|)))
   1.291 +(let ((?x58 (concat ?x34 (_ bv0 8))))
   1.292 +(let ((?x48 (concat (bvnot (bvnot ?x34)) ?x47)))
   1.293 +(let ((@x60 (monotonicity (rewrite (= (bvnot (bvnot ?x34)) ?x34)) (rewrite (= ?x47 (_ bv0 8))) (= ?x48 ?x58))))
   1.294 +(let ((?x18 (bvor ?x16 (bvnot (_ bv65280 16)))))
   1.295 +(let ((?x19 (bvnot ?x18)))
   1.296 +(let ((@x40 (monotonicity (rewrite (= ((_ extract 15 8) ?x16) (bvnot ?x34))) (= (concat ((_ extract 15 8) ?x16) (_ bv255 8)) (concat (bvnot ?x34) (_ bv255 8))))))
   1.297 +(let ((@x26 (monotonicity (rewrite (= (bvnot (_ bv65280 16)) (_ bv255 16))) (= ?x18 (bvor ?x16 (_ bv255 16))))))
   1.298 +(let ((@x33 (trans @x26 (rewrite (= (bvor ?x16 (_ bv255 16)) (concat ((_ extract 15 8) ?x16) (_ bv255 8)))) (= ?x18 (concat ((_ extract 15 8) ?x16) (_ bv255 8))))))
   1.299 +(let ((@x45 (monotonicity (trans @x33 @x40 (= ?x18 (concat (bvnot ?x34) (_ bv255 8)))) (= ?x19 (bvnot (concat (bvnot ?x34) (_ bv255 8)))))))
   1.300 +(let ((@x52 (trans @x45 (rewrite (= (bvnot (concat (bvnot ?x34) (_ bv255 8))) ?x48)) (= ?x19 ?x48))))
   1.301 +(let ((@x64 (trans (rewrite (= ?x7 ?x19)) (trans @x52 @x60 (= ?x19 ?x58)) (= ?x7 ?x58))))
   1.302 +(let ((@x134 (trans (trans (monotonicity @x64 @x107 $x109) (rewrite $x114) (= ?x10 ?x113)) (trans @x129 (rewrite (= ((_ extract 15 0) |$x|) |$x|)) (= ?x113 |$x|)) $x11)))
   1.303 +(let ((@x141 (trans (monotonicity @x134 (= $x11 (= |$x| |$x|))) (rewrite (= (= |$x| |$x|) true)) (= $x11 true))))
   1.304 +(let ((@x148 (trans (monotonicity @x141 (= $x12 (not true))) (rewrite (= (not true) false)) (= $x12 false))))
   1.305 +(mp (asserted $x12) @x148 false))))))))))))))))))))))))))))))))))))))))))
   1.306 +
   1.307 +9e9d8bb4c49a1669973a1c2e9f8c033d853f6801 97 0
   1.308 +unsat
   1.309 +((set-logic <null>)
   1.310 +(declare-fun k!150 () Bool)
   1.311 +(declare-fun k!140 () Bool)
   1.312 +(declare-fun k!130 () Bool)
   1.313 +(declare-fun k!120 () Bool)
   1.314 +(declare-fun k!110 () Bool)
   1.315 +(declare-fun k!100 () Bool)
   1.316 +(declare-fun k!90 () Bool)
   1.317 +(declare-fun k!80 () Bool)
   1.318 +(declare-fun k!70 () Bool)
   1.319 +(declare-fun k!60 () Bool)
   1.320 +(declare-fun k!50 () Bool)
   1.321 +(declare-fun k!40 () Bool)
   1.322 +(declare-fun k!30 () Bool)
   1.323 +(declare-fun k!20 () Bool)
   1.324 +(declare-fun k!10 () Bool)
   1.325 +(declare-fun k!00 () Bool)
   1.326 +(proof
   1.327 +(let (($x199 (or k!80 k!90 k!100 k!110 k!120 k!130 k!140 k!150)))
   1.328 +(let (($x364 (= (or false false false false false false false false) false)))
   1.329 +(let (($x362 (= $x199 (or false false false false false false false false))))
   1.330 +(let (($x312 (= k!150 false)))
   1.331 +(let ((@x316 (symm (rewrite (= $x312 (not k!150))) (= (not k!150) $x312))))
   1.332 +(let (($x143 (not k!150)))
   1.333 +(let (($x119 (not (or k!90 k!80 (not (or (not k!90) (not k!80)))))))
   1.334 +(let (($x118 (not k!100)))
   1.335 +(let (($x122 (or k!100 (or k!90 k!80 (not (or (not k!90) (not k!80)))) (not (or $x118 $x119)))))
   1.336 +(let (($x123 (not k!110)))
   1.337 +(let (($x128 (not k!120)))
   1.338 +(let (($x131 (not (or $x128 (not (or k!110 $x122 (not (or $x123 (not $x122)))))))))
   1.339 +(let (($x134 (not (or k!120 (or k!110 $x122 (not (or $x123 (not $x122)))) $x131))))
   1.340 +(let (($x133 (not k!130)))
   1.341 +(let (($x137 (or k!130 (or k!120 (or k!110 $x122 (not (or $x123 (not $x122)))) $x131) (not (or $x133 $x134)))))
   1.342 +(let (($x138 (not k!140)))
   1.343 +(let (($x146 (not (or $x143 (not (or k!140 $x137 (not (or $x138 (not $x137)))))))))
   1.344 +(let (($x147 (or k!150 (or k!140 $x137 (not (or $x138 (not $x137)))) $x146)))
   1.345 +(let ((?x107 (mkbv k!00 k!10 k!20 k!30 k!40 k!50 k!60 k!70 k!80 k!90 k!100 k!110 k!120 k!130 k!140 k!150)))
   1.346 +(let ((?x88 (mkbv false false false false false false false false true false false false false false false false)))
   1.347 +(let ((@x109 (rewrite (= |$w| ?x107))))
   1.348 +(let ((@x112 (monotonicity (rewrite (= (_ bv256 16) ?x88)) @x109 (= (bvule (_ bv256 16) |$w|) (bvule ?x88 ?x107)))))
   1.349 +(let ((@x151 (trans @x112 (rewrite (= (bvule ?x88 ?x107) $x147)) (= (bvule (_ bv256 16) |$w|) $x147))))
   1.350 +(let (($x16 (bvule (_ bv256 16) |$w|)))
   1.351 +(let (($x17 (not $x16)))
   1.352 +(let (($x11 (=> (bvult |$w| (_ bv256 16)) (= (bvand |$w| (_ bv255 16)) |$w|))))
   1.353 +(let (($x12 (not $x11)))
   1.354 +(let ((?x39 ((_ extract 7 0) |$w|)))
   1.355 +(let ((?x63 (concat (_ bv0 8) ?x39)))
   1.356 +(let (($x70 (= ?x63 |$w|)))
   1.357 +(let (($x76 (or $x16 $x70)))
   1.358 +(let ((@x65 (monotonicity (rewrite (= (bvnot (_ bv255 8)) (_ bv0 8))) (rewrite (= (bvnot (bvnot ?x39)) ?x39)) (= (concat (bvnot (_ bv255 8)) (bvnot (bvnot ?x39))) ?x63))))
   1.359 +(let ((?x53 (concat (bvnot (_ bv255 8)) (bvnot (bvnot ?x39)))))
   1.360 +(let ((?x20 (bvnot |$w|)))
   1.361 +(let ((?x22 (bvor ?x20 (bvnot (_ bv255 16)))))
   1.362 +(let ((?x23 (bvnot ?x22)))
   1.363 +(let ((@x45 (monotonicity (rewrite (= ((_ extract 7 0) ?x20) (bvnot ?x39))) (= (concat (_ bv255 8) ((_ extract 7 0) ?x20)) (concat (_ bv255 8) (bvnot ?x39))))))
   1.364 +(let ((@x31 (monotonicity (rewrite (= (bvnot (_ bv255 16)) (_ bv65280 16))) (= ?x22 (bvor ?x20 (_ bv65280 16))))))
   1.365 +(let ((@x38 (trans @x31 (rewrite (= (bvor ?x20 (_ bv65280 16)) (concat (_ bv255 8) ((_ extract 7 0) ?x20)))) (= ?x22 (concat (_ bv255 8) ((_ extract 7 0) ?x20))))))
   1.366 +(let ((@x50 (monotonicity (trans @x38 @x45 (= ?x22 (concat (_ bv255 8) (bvnot ?x39)))) (= ?x23 (bvnot (concat (_ bv255 8) (bvnot ?x39)))))))
   1.367 +(let ((@x57 (trans @x50 (rewrite (= (bvnot (concat (_ bv255 8) (bvnot ?x39))) ?x53)) (= ?x23 ?x53))))
   1.368 +(let ((@x69 (trans (rewrite (= (bvand |$w| (_ bv255 16)) ?x23)) (trans @x57 @x65 (= ?x23 ?x63)) (= (bvand |$w| (_ bv255 16)) ?x63))))
   1.369 +(let ((@x75 (monotonicity (rewrite (= (bvult |$w| (_ bv256 16)) $x17)) (monotonicity @x69 (= (= (bvand |$w| (_ bv255 16)) |$w|) $x70)) (= $x11 (=> $x17 $x70)))))
   1.370 +(let ((@x83 (monotonicity (trans @x75 (rewrite (= (=> $x17 $x70) $x76)) (= $x11 $x76)) (= $x12 (not $x76)))))
   1.371 +(let ((@x155 (mp (|not-or-elim| (mp (asserted $x12) @x83 (not $x76)) $x17) (monotonicity @x151 (= $x17 (not $x147))) (not $x147))))
   1.372 +(let (($x318 (= k!140 false)))
   1.373 +(let ((@x157 (|not-or-elim| @x155 (not (or k!140 $x137 (not (or $x138 (not $x137))))))))
   1.374 +(let ((@x323 (mp (|not-or-elim| @x157 $x138) (symm (rewrite (= $x318 $x138)) (= $x138 $x318)) $x318)))
   1.375 +(let (($x324 (= k!130 false)))
   1.376 +(let ((@x329 (mp (|not-or-elim| (|not-or-elim| @x157 (not $x137)) $x133) (symm (rewrite (= $x324 $x133)) (= $x133 $x324)) $x324)))
   1.377 +(let (($x330 (= k!120 false)))
   1.378 +(let ((@x335 (mp (|not-or-elim| (|not-or-elim| (|not-or-elim| @x157 (not $x137)) $x134) $x128) (symm (rewrite (= $x330 $x128)) (= $x128 $x330)) $x330)))
   1.379 +(let (($x336 (= k!110 false)))
   1.380 +(let ((@x163 (|not-or-elim| (|not-or-elim| (|not-or-elim| @x157 (not $x137)) $x134) (not (or k!110 $x122 (not (or $x123 (not $x122))))))))
   1.381 +(let ((@x341 (mp (|not-or-elim| @x163 $x123) (symm (rewrite (= $x336 $x123)) (= $x123 $x336)) $x336)))
   1.382 +(let (($x342 (= k!100 false)))
   1.383 +(let ((@x347 (mp (|not-or-elim| (|not-or-elim| @x163 (not $x122)) $x118) (symm (rewrite (= $x342 $x118)) (= $x118 $x342)) $x342)))
   1.384 +(let (($x348 (= k!90 false)))
   1.385 +(let ((@x352 (symm (rewrite (= $x348 (not k!90))) (= (not k!90) $x348))))
   1.386 +(let (($x113 (not k!90)))
   1.387 +(let ((@x353 (mp (|not-or-elim| (|not-or-elim| (|not-or-elim| @x163 (not $x122)) $x119) $x113) @x352 $x348)))
   1.388 +(let (($x354 (= k!80 false)))
   1.389 +(let ((@x358 (symm (rewrite (= $x354 (not k!80))) (= (not k!80) $x354))))
   1.390 +(let (($x114 (not k!80)))
   1.391 +(let ((@x359 (mp (|not-or-elim| (|not-or-elim| (|not-or-elim| @x163 (not $x122)) $x119) $x114) @x358 $x354)))
   1.392 +(let ((@x363 (monotonicity @x359 @x353 @x347 @x341 @x335 @x329 @x323 (mp (|not-or-elim| @x155 $x143) @x316 $x312) $x362)))
   1.393 +(let (($x200 (not $x199)))
   1.394 +(let (($x205 (not $x200)))
   1.395 +(let ((?x191 (mkbv k!00 k!10 k!20 k!30 k!40 k!50 k!60 k!70 false false false false false false false false)))
   1.396 +(let ((?x183 (mkbv k!00 k!10 k!20 k!30 k!40 k!50 k!60 k!70)))
   1.397 +(let ((?x188 (concat (mkbv false false false false false false false false) ?x183)))
   1.398 +(let ((@x187 (trans (monotonicity @x109 (= ?x39 ((_ extract 7 0) ?x107))) (rewrite (= ((_ extract 7 0) ?x107) ?x183)) (= ?x39 ?x183))))
   1.399 +(let (($x178 (= (_ bv0 8) (mkbv false false false false false false false false))))
   1.400 +(let ((@x195 (trans (monotonicity (rewrite $x178) @x187 (= ?x63 ?x188)) (rewrite (= ?x188 ?x191)) (= ?x63 ?x191))))
   1.401 +(let ((@x204 (trans (monotonicity @x195 @x109 (= $x70 (= ?x191 ?x107))) (rewrite (= (= ?x191 ?x107) $x200)) (= $x70 $x200))))
   1.402 +(let ((@x208 (mp (|not-or-elim| (mp (asserted $x12) @x83 (not $x76)) (not $x70)) (monotonicity @x204 (= (not $x70) $x205)) $x205)))
   1.403 +(mp (mp @x208 (rewrite (= $x205 $x199)) $x199) (trans @x363 (rewrite $x364) (= $x199 false)) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   1.404 +
   1.405 +f611d24907b7d60f35d0adf911b0c146313d6c07 13 0
   1.406 +unsat
   1.407 +((set-logic <null>)
   1.408 +(proof
   1.409 +(let ((?x10 (|$p| true)))
   1.410 +(let (($x11 (= (|$p| (ite (bvule (_ bv0 4) |$a|) true false)) ?x10)))
   1.411 +(let (($x12 (not $x11)))
   1.412 +(let (($x8 (ite (bvule (_ bv0 4) |$a|) true false)))
   1.413 +(let ((@x20 (monotonicity (rewrite (= (bvule (_ bv0 4) |$a|) true)) (= $x8 (ite true true false)))))
   1.414 +(let ((@x24 (trans @x20 (rewrite (= (ite true true false) true)) (= $x8 true))))
   1.415 +(let ((@x32 (trans (monotonicity (monotonicity @x24 $x11) (= $x11 (= ?x10 ?x10))) (rewrite (= (= ?x10 ?x10) true)) (= $x11 true))))
   1.416 +(let ((@x39 (trans (monotonicity @x32 (= $x12 (not true))) (rewrite (= (not true) false)) (= $x12 false))))
   1.417 +(mp (asserted $x12) @x39 false)))))))))))
   1.418 +
   1.419 +eb851e3355032ef6b75793abd314b6b2bc9c3459 18 0
   1.420 +unsat
   1.421 +((set-logic <null>)
   1.422 +(proof
   1.423 +(let (($x600 (forall ((?v0 (_ BitVec 2)) )(!(not (<= (|$bv2int| ?v0) 0)) :pattern ( (|$bv2int| ?v0) )))
   1.424 +))
   1.425 +(let (($x45 (forall ((?v0 (_ BitVec 2)) )(not (<= (|$bv2int| ?v0) 0)))
   1.426 +))
   1.427 +(let ((@x602 (refl (= (not (<= (|$bv2int| ?0) 0)) (not (<= (|$bv2int| ?0) 0))))))
   1.428 +(let ((@x132 (refl (|~| (not (<= (|$bv2int| ?0) 0)) (not (<= (|$bv2int| ?0) 0))))))
   1.429 +(let (($x24 (forall ((?v0 (_ BitVec 2)) )(let ((?x22 (|$bv2int| ?v0)))
   1.430 +(< 0 ?x22)))
   1.431 +))
   1.432 +(let ((@x44 (rewrite (= (< 0 (|$bv2int| ?0)) (not (<= (|$bv2int| ?0) 0))))))
   1.433 +(let ((@x133 (|mp~| (mp (asserted $x24) (|quant-intro| @x44 (= $x24 $x45)) $x45) (|nnf-pos| @x132 (|~| $x45 $x45)) $x45)))
   1.434 +(let ((@x597 (|unit-resolution| ((_ |quant-inst| (_ bv0 2)) (or (not $x600) (not (<= (|$bv2int| (_ bv0 2)) 0)))) (mp @x133 (|quant-intro| @x602 (= $x45 $x600)) $x600) (not (<= (|$bv2int| (_ bv0 2)) 0)))))
   1.435 +(let ((@x589 ((_ |th-lemma| arith triangle-eq) (or (not (= (|$bv2int| (_ bv0 2)) 0)) (<= (|$bv2int| (_ bv0 2)) 0)))))
   1.436 +(|unit-resolution| @x589 (asserted (= (|$bv2int| (_ bv0 2)) 0)) @x597 false))))))))))))
   1.437 +