API tools faq
paste
Guest User

to_smt2() constraints

a guest
Jan 25th, 2017
144
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 62.54 KB | None | 0 0
raw download clone embed print report
  1. ;
  2. (set-info :status unknown)
  3. (declare-fun bmAx<r>-0 (Int) Real)
  4. (declare-fun r<r>-4 (Int) Real)
  5. (declare-fun bmAx<o>-0 (Int) Real)
  6. (declare-fun r<o>-4 (Int) Real)
  7. (declare-fun i<r>-1 () Int)
  8. (declare-fun i<o>-1 () Int)
  9. (declare-fun r_norm<r>-4 () Real)
  10. (declare-fun r_norm<o>-4 () Real)
  11. (declare-fun b<r>-0 (Int) Real)
  12. (declare-fun b<o>-0 (Int) Real)
  13. (declare-fun x<r>-0 (Int) Real)
  14. (declare-fun x<o>-0 (Int) Real)
  15. (declare-fun A<r>-0 (Int Int) Real)
  16. (declare-fun A<o>-0 (Int Int) Real)
  17. (declare-fun iters<r>-0 () Int)
  18. (declare-fun iters<o>-0 () Int)
  19. (declare-fun q<o>-0 (Int) Real)
  20. (declare-fun q<o>-1 (Int) Real)
  21. (declare-fun q<r>-0 (Int) Real)
  22. (declare-fun q<r>-1 (Int) Real)
  23. (declare-fun tmp<o>-16 () Real)
  24. (declare-fun tmp<r>-16 () Real)
  25. (declare-fun q<o>-2 (Int) Real)
  26. (declare-fun q<r>-2 (Int) Real)
  27. (declare-fun tmp<o>-17 () Real)
  28. (declare-fun tmp<r>-17 () Real)
  29. (declare-fun q<o>-3 (Int) Real)
  30. (declare-fun q<r>-3 (Int) Real)
  31. (declare-fun tmp<o>-18 () Real)
  32. (declare-fun tmp<r>-18 () Real)
  33. (declare-fun q<o>-4 (Int) Real)
  34. (declare-fun q<r>-4 (Int) Real)
  35. (declare-fun q<o>-5 (Int) Real)
  36. (declare-fun q<r>-5 (Int) Real)
  37. (declare-fun tmp<o>-19 () Real)
  38. (declare-fun tmp<r>-19 () Real)
  39. (declare-fun q<o>-6 (Int) Real)
  40. (declare-fun q<r>-6 (Int) Real)
  41. (declare-fun tmp<o>-20 () Real)
  42. (declare-fun tmp<r>-20 () Real)
  43. (declare-fun q<o>-7 (Int) Real)
  44. (declare-fun q<r>-7 (Int) Real)
  45. (declare-fun tmp<o>-21 () Real)
  46. (declare-fun tmp<r>-21 () Real)
  47. (declare-fun q<o>-8 (Int) Real)
  48. (declare-fun q<r>-8 (Int) Real)
  49. (declare-fun q<o>-9 (Int) Real)
  50. (declare-fun q<r>-9 (Int) Real)
  51. (declare-fun tmp<o>-22 () Real)
  52. (declare-fun tmp<r>-22 () Real)
  53. (declare-fun q<o>-10 (Int) Real)
  54. (declare-fun q<r>-10 (Int) Real)
  55. (declare-fun tmp<o>-23 () Real)
  56. (declare-fun tmp<r>-23 () Real)
  57. (declare-fun q<o>-11 (Int) Real)
  58. (declare-fun q<r>-11 (Int) Real)
  59. (declare-fun tmp<o>-24 () Real)
  60. (declare-fun tmp<r>-24 () Real)
  61. (declare-fun q<o>-12 (Int) Real)
  62. (declare-fun q<r>-12 (Int) Real)
  63. (declare-fun q<o>-13 (Int) Real)
  64. (declare-fun q<r>-13 (Int) Real)
  65. (declare-fun tmp<o>-25 () Real)
  66. (declare-fun tmp<r>-25 () Real)
  67. (declare-fun q<o>-14 (Int) Real)
  68. (declare-fun q<r>-14 (Int) Real)
  69. (declare-fun tmp<o>-26 () Real)
  70. (declare-fun tmp<r>-26 () Real)
  71. (declare-fun q<o>-15 (Int) Real)
  72. (declare-fun q<r>-15 (Int) Real)
  73. (declare-fun tmp<o>-27 () Real)
  74. (declare-fun tmp<r>-27 () Real)
  75. (declare-fun q<o>-16 (Int) Real)
  76. (declare-fun q<r>-16 (Int) Real)
  77. (declare-fun rtq<o>-1 () Real)
  78. (declare-fun rtq<r>-1 () Real)
  79. (declare-fun tmp<o>-28 () Real)
  80. (declare-fun tmp<r>-28 () Real)
  81. (declare-fun rtq<o>-2 () Real)
  82. (declare-fun rtq<r>-2 () Real)
  83. (declare-fun tmp<o>-29 () Real)
  84. (declare-fun tmp<r>-29 () Real)
  85. (declare-fun rtq<o>-3 () Real)
  86. (declare-fun rtq<r>-3 () Real)
  87. (declare-fun tmp<o>-30 () Real)
  88. (declare-fun tmp<r>-30 () Real)
  89. (declare-fun rtq<o>-4 () Real)
  90. (declare-fun rtq<r>-4 () Real)
  91. (declare-fun alpha<o>-1 () Real)
  92. (declare-fun alpha<r>-1 () Real)
  93. (declare-fun alphar<o>-0 (Int) Real)
  94. (declare-fun alphar<o>-1 (Int) Real)
  95. (declare-fun alphar<r>-0 (Int) Real)
  96. (declare-fun alphar<r>-1 (Int) Real)
  97. (declare-fun alphar<o>-2 (Int) Real)
  98. (declare-fun alphar<r>-2 (Int) Real)
  99. (declare-fun alphar<o>-3 (Int) Real)
  100. (declare-fun alphar<r>-3 (Int) Real)
  101. (declare-fun alphar<o>-4 (Int) Real)
  102. (declare-fun alphar<r>-4 (Int) Real)
  103. (declare-fun x<o>-1 (Int) Real)
  104. (declare-fun x<r>-1 (Int) Real)
  105. (declare-fun x<o>-2 (Int) Real)
  106. (declare-fun x<r>-2 (Int) Real)
  107. (declare-fun x<o>-3 (Int) Real)
  108. (declare-fun x<r>-3 (Int) Real)
  109. (declare-fun x<o>-4 (Int) Real)
  110. (declare-fun x<r>-4 (Int) Real)
  111. (declare-fun alphaq<o>-0 (Int) Real)
  112. (declare-fun alphaq<o>-1 (Int) Real)
  113. (declare-fun alphaq<r>-0 (Int) Real)
  114. (declare-fun alphaq<r>-1 (Int) Real)
  115. (declare-fun alphaq<o>-2 (Int) Real)
  116. (declare-fun alphaq<r>-2 (Int) Real)
  117. (declare-fun alphaq<o>-3 (Int) Real)
  118. (declare-fun alphaq<r>-3 (Int) Real)
  119. (declare-fun alphaq<o>-4 (Int) Real)
  120. (declare-fun alphaq<r>-4 (Int) Real)
  121. (declare-fun r<o>-5 (Int) Real)
  122. (declare-fun r<r>-5 (Int) Real)
  123. (declare-fun r<o>-6 (Int) Real)
  124. (declare-fun r<r>-6 (Int) Real)
  125. (declare-fun r<o>-7 (Int) Real)
  126. (declare-fun r<r>-7 (Int) Real)
  127. (declare-fun r<o>-8 (Int) Real)
  128. (declare-fun r<r>-8 (Int) Real)
  129. (declare-fun r_norm<o>-5 () Real)
  130. (declare-fun r_norm<r>-5 () Real)
  131. (declare-fun tmp<o>-31 () Real)
  132. (declare-fun tmp<r>-31 () Real)
  133. (declare-fun r_norm<o>-6 () Real)
  134. (declare-fun r_norm<r>-6 () Real)
  135. (declare-fun tmp<o>-32 () Real)
  136. (declare-fun tmp<r>-32 () Real)
  137. (declare-fun r_norm<o>-7 () Real)
  138. (declare-fun r_norm<r>-7 () Real)
  139. (declare-fun tmp<o>-33 () Real)
  140. (declare-fun tmp<r>-33 () Real)
  141. (declare-fun r_norm<o>-8 () Real)
  142. (declare-fun r_norm<r>-8 () Real)
  143. (declare-fun i<o>-2 () Int)
  144. (declare-fun i<r>-2 () Int)
  145. (declare-fun Ax<o>-16 (Int) Real)
  146. (declare-fun Ax<o>-17 (Int) Real)
  147. (declare-fun Ax<r>-16 (Int) Real)
  148. (declare-fun Ax<r>-17 (Int) Real)
  149. (declare-fun tmp<o>-34 () Real)
  150. (declare-fun tmp<r>-34 () Real)
  151. (declare-fun Ax<o>-18 (Int) Real)
  152. (declare-fun Ax<r>-18 (Int) Real)
  153. (declare-fun tmp<o>-35 () Real)
  154. (declare-fun tmp<r>-35 () Real)
  155. (declare-fun Ax<o>-19 (Int) Real)
  156. (declare-fun Ax<r>-19 (Int) Real)
  157. (declare-fun tmp<o>-36 () Real)
  158. (declare-fun tmp<r>-36 () Real)
  159. (declare-fun Ax<o>-20 (Int) Real)
  160. (declare-fun Ax<r>-20 (Int) Real)
  161. (declare-fun Ax<o>-21 (Int) Real)
  162. (declare-fun Ax<r>-21 (Int) Real)
  163. (declare-fun tmp<o>-37 () Real)
  164. (declare-fun tmp<r>-37 () Real)
  165. (declare-fun Ax<o>-22 (Int) Real)
  166. (declare-fun Ax<r>-22 (Int) Real)
  167. (declare-fun tmp<o>-38 () Real)
  168. (declare-fun tmp<r>-38 () Real)
  169. (declare-fun Ax<o>-23 (Int) Real)
  170. (declare-fun Ax<r>-23 (Int) Real)
  171. (declare-fun tmp<o>-39 () Real)
  172. (declare-fun tmp<r>-39 () Real)
  173. (declare-fun Ax<o>-24 (Int) Real)
  174. (declare-fun Ax<r>-24 (Int) Real)
  175. (declare-fun Ax<o>-25 (Int) Real)
  176. (declare-fun Ax<r>-25 (Int) Real)
  177. (declare-fun tmp<o>-40 () Real)
  178. (declare-fun tmp<r>-40 () Real)
  179. (declare-fun Ax<o>-26 (Int) Real)
  180. (declare-fun Ax<r>-26 (Int) Real)
  181. (declare-fun tmp<o>-41 () Real)
  182. (declare-fun tmp<r>-41 () Real)
  183. (declare-fun Ax<o>-27 (Int) Real)
  184. (declare-fun Ax<r>-27 (Int) Real)
  185. (declare-fun tmp<o>-42 () Real)
  186. (declare-fun tmp<r>-42 () Real)
  187. (declare-fun Ax<o>-28 (Int) Real)
  188. (declare-fun Ax<r>-28 (Int) Real)
  189. (declare-fun Ax<o>-29 (Int) Real)
  190. (declare-fun Ax<r>-29 (Int) Real)
  191. (declare-fun tmp<o>-43 () Real)
  192. (declare-fun tmp<r>-43 () Real)
  193. (declare-fun Ax<o>-30 (Int) Real)
  194. (declare-fun Ax<r>-30 (Int) Real)
  195. (declare-fun tmp<o>-44 () Real)
  196. (declare-fun tmp<r>-44 () Real)
  197. (declare-fun Ax<o>-31 (Int) Real)
  198. (declare-fun Ax<r>-31 (Int) Real)
  199. (declare-fun tmp<o>-45 () Real)
  200. (declare-fun tmp<r>-45 () Real)
  201. (declare-fun Ax<o>-32 (Int) Real)
  202. (declare-fun Ax<r>-32 (Int) Real)
  203. (declare-fun bmAx<o>-1 (Int) Real)
  204. (declare-fun bmAx<r>-1 (Int) Real)
  205. (declare-fun bmAx<o>-2 (Int) Real)
  206. (declare-fun bmAx<r>-2 (Int) Real)
  207. (declare-fun bmAx<o>-3 (Int) Real)
  208. (declare-fun bmAx<r>-3 (Int) Real)
  209. (declare-fun bmAx<o>-4 (Int) Real)
  210. (declare-fun bmAx<r>-4 (Int) Real)
  211. (assert
  212. (let ((?x238 (bmAx<r>-0 3)))
  213. (let ((?x1034 (r<r>-4 3)))
  214. (let (($x1126 (= ?x1034 ?x238)))
  215. (let ((?x234 (bmAx<r>-0 2)))
  216. (let ((?x1030 (r<r>-4 2)))
  217. (let (($x1124 (= ?x1030 ?x234)))
  218. (let ((?x230 (bmAx<r>-0 1)))
  219. (let ((?x1026 (r<r>-4 1)))
  220. (let (($x1122 (= ?x1026 ?x230)))
  221. (let ((?x227 (bmAx<r>-0 0)))
  222. (let ((?x1023 (r<r>-4 0)))
  223. (let (($x1121 (= ?x1023 ?x227)))
  224. (let (($x1123 (and $x1121 $x1122)))
  225. (let (($x1125 (and $x1123 $x1124)))
  226. (let (($x1127 (and $x1125 $x1126)))
  227. (let ((?x237 (bmAx<o>-0 3)))
  228. (let ((?x1019 (r<o>-4 3)))
  229. (let (($x1119 (= ?x1019 ?x237)))
  230. (let ((?x233 (bmAx<o>-0 2)))
  231. (let ((?x1015 (r<o>-4 2)))
  232. (let (($x1117 (= ?x1015 ?x233)))
  233. (let ((?x229 (bmAx<o>-0 1)))
  234. (let ((?x1011 (r<o>-4 1)))
  235. (let (($x1115 (= ?x1011 ?x229)))
  236. (let ((?x226 (bmAx<o>-0 0)))
  237. (let ((?x1006 (r<o>-4 0)))
  238. (let (($x1114 (= ?x1006 ?x226)))
  239. (let (($x1116 (and $x1114 $x1115)))
  240. (let (($x1118 (and $x1116 $x1117)))
  241. (let (($x1120 (and $x1118 $x1119)))
  242. (let (($x1128 (=> $x1120 $x1127)))
  243. (let (($x1112 (= i<o>-1 i<r>-1)))
  244. (let (($x1110 (= r_norm<o>-4 r_norm<r>-4)))
  245. (let ((?x111 (b<r>-0 3)))
  246. (let ((?x110 (b<o>-0 3)))
  247. (let (($x112 (= ?x110 ?x111)))
  248. (let ((?x107 (b<r>-0 2)))
  249. (let ((?x106 (b<o>-0 2)))
  250. (let (($x108 (= ?x106 ?x107)))
  251. (let ((?x103 (b<r>-0 1)))
  252. (let ((?x102 (b<o>-0 1)))
  253. (let (($x104 (= ?x102 ?x103)))
  254. (let ((?x100 (b<r>-0 0)))
  255. (let ((?x99 (b<o>-0 0)))
  256. (let (($x101 (= ?x99 ?x100)))
  257. (let (($x113 (and (and (and $x101 $x104) $x108) $x112)))
  258. (let ((?x126 (x<r>-0 3)))
  259. (let ((?x125 (x<o>-0 3)))
  260. (let (($x127 (= ?x125 ?x126)))
  261. (let ((?x122 (x<r>-0 2)))
  262. (let ((?x121 (x<o>-0 2)))
  263. (let (($x123 (= ?x121 ?x122)))
  264. (let ((?x118 (x<r>-0 1)))
  265. (let ((?x117 (x<o>-0 1)))
  266. (let (($x119 (= ?x117 ?x118)))
  267. (let ((?x115 (x<r>-0 0)))
  268. (let ((?x114 (x<o>-0 0)))
  269. (let (($x116 (= ?x114 ?x115)))
  270. (let (($x128 (and (and (and $x116 $x119) $x123) $x127)))
  271. (let (($x1105 (= ?x1019 ?x1034)))
  272. (let (($x1106 (and (and (and (= ?x1006 ?x1023) (= ?x1011 ?x1026)) (= ?x1015 ?x1030)) $x1105)))
  273. (let ((?x96 (A<r>-0 3 3)))
  274. (let ((?x95 (A<o>-0 3 3)))
  275. (let (($x97 (= ?x95 ?x96)))
  276. (let ((?x92 (A<r>-0 3 2)))
  277. (let ((?x91 (A<o>-0 3 2)))
  278. (let (($x93 (= ?x91 ?x92)))
  279. (let ((?x88 (A<r>-0 3 1)))
  280. (let ((?x87 (A<o>-0 3 1)))
  281. (let (($x89 (= ?x87 ?x88)))
  282. (let ((?x84 (A<r>-0 3 0)))
  283. (let ((?x83 (A<o>-0 3 0)))
  284. (let (($x85 (= ?x83 ?x84)))
  285. (let ((?x80 (A<r>-0 2 3)))
  286. (let ((?x79 (A<o>-0 2 3)))
  287. (let (($x81 (= ?x79 ?x80)))
  288. (let ((?x76 (A<r>-0 2 2)))
  289. (let ((?x75 (A<o>-0 2 2)))
  290. (let (($x77 (= ?x75 ?x76)))
  291. (let ((?x72 (A<r>-0 2 1)))
  292. (let ((?x71 (A<o>-0 2 1)))
  293. (let (($x73 (= ?x71 ?x72)))
  294. (let ((?x68 (A<r>-0 2 0)))
  295. (let ((?x67 (A<o>-0 2 0)))
  296. (let (($x69 (= ?x67 ?x68)))
  297. (let ((?x64 (A<r>-0 1 3)))
  298. (let ((?x63 (A<o>-0 1 3)))
  299. (let (($x65 (= ?x63 ?x64)))
  300. (let ((?x60 (A<r>-0 1 2)))
  301. (let ((?x59 (A<o>-0 1 2)))
  302. (let (($x61 (= ?x59 ?x60)))
  303. (let ((?x56 (A<r>-0 1 1)))
  304. (let ((?x55 (A<o>-0 1 1)))
  305. (let (($x57 (= ?x55 ?x56)))
  306. (let ((?x52 (A<r>-0 1 0)))
  307. (let ((?x51 (A<o>-0 1 0)))
  308. (let (($x53 (= ?x51 ?x52)))
  309. (let ((?x48 (A<r>-0 0 3)))
  310. (let ((?x47 (A<o>-0 0 3)))
  311. (let (($x49 (= ?x47 ?x48)))
  312. (let ((?x43 (A<r>-0 0 2)))
  313. (let ((?x42 (A<o>-0 0 2)))
  314. (let (($x44 (= ?x42 ?x43)))
  315. (let ((?x38 (A<r>-0 0 1)))
  316. (let ((?x37 (A<o>-0 0 1)))
  317. (let (($x39 (= ?x37 ?x38)))
  318. (let ((?x35 (A<r>-0 0 0)))
  319. (let ((?x34 (A<o>-0 0 0)))
  320. (let (($x36 (= ?x34 ?x35)))
  321. (let (($x62 (and (and (and (and (and (and $x36 $x39) $x44) $x49) $x53) $x57) $x61)))
  322. (let (($x86 (and (and (and (and (and (and $x62 $x65) $x69) $x73) $x77) $x81) $x85)))
  323. (let (($x98 (and (and (and $x86 $x89) $x93) $x97)))
  324. (let (($x1107 (and $x98 $x1106)))
  325. (let (($x1108 (and $x1107 $x128)))
  326. (let (($x1109 (and $x1108 $x113)))
  327. (let (($x1111 (and $x1109 $x1110)))
  328. (let (($x1113 (and $x1111 $x1112)))
  329. (and $x1113 $x1128)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  330. (assert
  331. (let (($x1790 (< i<r>-1 iters<r>-0)))
  332. (let (($x1789 (< i<o>-1 iters<o>-0)))
  333. (and $x1789 $x1790))))
  334. (assert
  335. (let (($x1968 (and (=> (and (distinct 0 0) true) (= (q<o>-1 0) (q<o>-0 0))) (=> (and (distinct 0 1) true) (= (q<o>-1 1) (q<o>-0 1))))))
  336. (let (($x1972 (and $x1968 (=> (and (distinct 0 2) true) (= (q<o>-1 2) (q<o>-0 2))))))
  337. (and $x1972 (=> (and (distinct 0 3) true) (= (q<o>-1 3) (q<o>-0 3)))))))
  338. (assert
  339. (let (($x1983 (and (=> (and (distinct 0 0) true) (= (q<r>-1 0) (q<r>-0 0))) (=> (and (distinct 0 1) true) (= (q<r>-1 1) (q<r>-0 1))))))
  340. (let (($x1987 (and $x1983 (=> (and (distinct 0 2) true) (= (q<r>-1 2) (q<r>-0 2))))))
  341. (and $x1987 (=> (and (distinct 0 3) true) (= (q<r>-1 3) (q<r>-0 3)))))))
  342. (assert
  343. (let ((?x1006 (r<o>-4 0)))
  344. (let ((?x34 (A<o>-0 0 0)))
  345. (let ((?x1961 (* ?x34 ?x1006)))
  346. (let ((?x1960 (q<o>-1 0)))
  347. (= ?x1960 ?x1961))))))
  348. (assert
  349. (and true (= (q<r>-1 0) (* (A<r>-0 0 0) (r<r>-4 0)))))
  350. (assert
  351. (let ((?x1011 (r<o>-4 1)))
  352. (let ((?x37 (A<o>-0 0 1)))
  353. (let ((?x1996 (* ?x37 ?x1011)))
  354. (= tmp<o>-16 ?x1996)))))
  355. (assert
  356. (and true (= tmp<r>-16 (* (A<r>-0 0 1) (r<r>-4 1)))))
  357. (assert
  358. (let (($x2010 (and (=> (and (distinct 0 0) true) (= (q<o>-2 0) (q<o>-1 0))) (=> (and (distinct 0 1) true) (= (q<o>-2 1) (q<o>-1 1))))))
  359. (let (($x2014 (and $x2010 (=> (and (distinct 0 2) true) (= (q<o>-2 2) (q<o>-1 2))))))
  360. (and $x2014 (=> (and (distinct 0 3) true) (= (q<o>-2 3) (q<o>-1 3)))))))
  361. (assert
  362. (let (($x2025 (and (=> (and (distinct 0 0) true) (= (q<r>-2 0) (q<r>-1 0))) (=> (and (distinct 0 1) true) (= (q<r>-2 1) (q<r>-1 1))))))
  363. (let (($x2029 (and $x2025 (=> (and (distinct 0 2) true) (= (q<r>-2 2) (q<r>-1 2))))))
  364. (and $x2029 (=> (and (distinct 0 3) true) (= (q<r>-2 3) (q<r>-1 3)))))))
  365. (assert
  366. (let ((?x2002 (q<o>-2 0)))
  367. (= ?x2002 (+ (q<o>-1 0) tmp<o>-16))))
  368. (assert
  369. (and true (= (q<r>-2 0) (+ (q<r>-1 0) tmp<r>-16))))
  370. (assert
  371. (let ((?x1015 (r<o>-4 2)))
  372. (let ((?x42 (A<o>-0 0 2)))
  373. (let ((?x2038 (* ?x42 ?x1015)))
  374. (= tmp<o>-17 ?x2038)))))
  375. (assert
  376. (and true (= tmp<r>-17 (* (A<r>-0 0 2) (r<r>-4 2)))))
  377. (assert
  378. (let (($x2052 (and (=> (and (distinct 0 0) true) (= (q<o>-3 0) (q<o>-2 0))) (=> (and (distinct 0 1) true) (= (q<o>-3 1) (q<o>-2 1))))))
  379. (let (($x2056 (and $x2052 (=> (and (distinct 0 2) true) (= (q<o>-3 2) (q<o>-2 2))))))
  380. (and $x2056 (=> (and (distinct 0 3) true) (= (q<o>-3 3) (q<o>-2 3)))))))
  381. (assert
  382. (let (($x2067 (and (=> (and (distinct 0 0) true) (= (q<r>-3 0) (q<r>-2 0))) (=> (and (distinct 0 1) true) (= (q<r>-3 1) (q<r>-2 1))))))
  383. (let (($x2071 (and $x2067 (=> (and (distinct 0 2) true) (= (q<r>-3 2) (q<r>-2 2))))))
  384. (and $x2071 (=> (and (distinct 0 3) true) (= (q<r>-3 3) (q<r>-2 3)))))))
  385. (assert
  386. (let ((?x2044 (q<o>-3 0)))
  387. (= ?x2044 (+ (q<o>-2 0) tmp<o>-17))))
  388. (assert
  389. (and true (= (q<r>-3 0) (+ (q<r>-2 0) tmp<r>-17))))
  390. (assert
  391. (let ((?x1019 (r<o>-4 3)))
  392. (let ((?x47 (A<o>-0 0 3)))
  393. (let ((?x2080 (* ?x47 ?x1019)))
  394. (= tmp<o>-18 ?x2080)))))
  395. (assert
  396. (and true (= tmp<r>-18 (* (A<r>-0 0 3) (r<r>-4 3)))))
  397. (assert
  398. (let (($x2094 (and (=> (and (distinct 0 0) true) (= (q<o>-4 0) (q<o>-3 0))) (=> (and (distinct 0 1) true) (= (q<o>-4 1) (q<o>-3 1))))))
  399. (let (($x2098 (and $x2094 (=> (and (distinct 0 2) true) (= (q<o>-4 2) (q<o>-3 2))))))
  400. (and $x2098 (=> (and (distinct 0 3) true) (= (q<o>-4 3) (q<o>-3 3)))))))
  401. (assert
  402. (let (($x2109 (and (=> (and (distinct 0 0) true) (= (q<r>-4 0) (q<r>-3 0))) (=> (and (distinct 0 1) true) (= (q<r>-4 1) (q<r>-3 1))))))
  403. (let (($x2113 (and $x2109 (=> (and (distinct 0 2) true) (= (q<r>-4 2) (q<r>-3 2))))))
  404. (and $x2113 (=> (and (distinct 0 3) true) (= (q<r>-4 3) (q<r>-3 3)))))))
  405. (assert
  406. (let ((?x2086 (q<o>-4 0)))
  407. (= ?x2086 (+ (q<o>-3 0) tmp<o>-18))))
  408. (assert
  409. (and true (= (q<r>-4 0) (+ (q<r>-3 0) tmp<r>-18))))
  410. (assert
  411. (let (($x2129 (and (=> (and (distinct 1 0) true) (= (q<o>-5 0) (q<o>-4 0))) (=> (and (distinct 1 1) true) (= (q<o>-5 1) (q<o>-4 1))))))
  412. (let (($x2133 (and $x2129 (=> (and (distinct 1 2) true) (= (q<o>-5 2) (q<o>-4 2))))))
  413. (and $x2133 (=> (and (distinct 1 3) true) (= (q<o>-5 3) (q<o>-4 3)))))))
  414. (assert
  415. (let (($x2144 (and (=> (and (distinct 1 0) true) (= (q<r>-5 0) (q<r>-4 0))) (=> (and (distinct 1 1) true) (= (q<r>-5 1) (q<r>-4 1))))))
  416. (let (($x2148 (and $x2144 (=> (and (distinct 1 2) true) (= (q<r>-5 2) (q<r>-4 2))))))
  417. (and $x2148 (=> (and (distinct 1 3) true) (= (q<r>-5 3) (q<r>-4 3)))))))
  418. (assert
  419. (let ((?x1006 (r<o>-4 0)))
  420. (let ((?x51 (A<o>-0 1 0)))
  421. (let ((?x2122 (* ?x51 ?x1006)))
  422. (let ((?x2126 (q<o>-5 1)))
  423. (= ?x2126 ?x2122))))))
  424. (assert
  425. (and true (= (q<r>-5 1) (* (A<r>-0 1 0) (r<r>-4 0)))))
  426. (assert
  427. (let ((?x1011 (r<o>-4 1)))
  428. (let ((?x55 (A<o>-0 1 1)))
  429. (let ((?x2157 (* ?x55 ?x1011)))
  430. (= tmp<o>-19 ?x2157)))))
  431. (assert
  432. (and true (= tmp<r>-19 (* (A<r>-0 1 1) (r<r>-4 1)))))
  433. (assert
  434. (let (($x2171 (and (=> (and (distinct 1 0) true) (= (q<o>-6 0) (q<o>-5 0))) (=> (and (distinct 1 1) true) (= (q<o>-6 1) (q<o>-5 1))))))
  435. (let (($x2175 (and $x2171 (=> (and (distinct 1 2) true) (= (q<o>-6 2) (q<o>-5 2))))))
  436. (and $x2175 (=> (and (distinct 1 3) true) (= (q<o>-6 3) (q<o>-5 3)))))))
  437. (assert
  438. (let (($x2186 (and (=> (and (distinct 1 0) true) (= (q<r>-6 0) (q<r>-5 0))) (=> (and (distinct 1 1) true) (= (q<r>-6 1) (q<r>-5 1))))))
  439. (let (($x2190 (and $x2186 (=> (and (distinct 1 2) true) (= (q<r>-6 2) (q<r>-5 2))))))
  440. (and $x2190 (=> (and (distinct 1 3) true) (= (q<r>-6 3) (q<r>-5 3)))))))
  441. (assert
  442. (let ((?x2168 (q<o>-6 1)))
  443. (= ?x2168 (+ (q<o>-5 0) tmp<o>-19))))
  444. (assert
  445. (and true (= (q<r>-6 1) (+ (q<r>-5 0) tmp<r>-19))))
  446. (assert
  447. (let ((?x1015 (r<o>-4 2)))
  448. (let ((?x59 (A<o>-0 1 2)))
  449. (let ((?x2199 (* ?x59 ?x1015)))
  450. (= tmp<o>-20 ?x2199)))))
  451. (assert
  452. (and true (= tmp<r>-20 (* (A<r>-0 1 2) (r<r>-4 2)))))
  453. (assert
  454. (let (($x2213 (and (=> (and (distinct 1 0) true) (= (q<o>-7 0) (q<o>-6 0))) (=> (and (distinct 1 1) true) (= (q<o>-7 1) (q<o>-6 1))))))
  455. (let (($x2217 (and $x2213 (=> (and (distinct 1 2) true) (= (q<o>-7 2) (q<o>-6 2))))))
  456. (and $x2217 (=> (and (distinct 1 3) true) (= (q<o>-7 3) (q<o>-6 3)))))))
  457. (assert
  458. (let (($x2228 (and (=> (and (distinct 1 0) true) (= (q<r>-7 0) (q<r>-6 0))) (=> (and (distinct 1 1) true) (= (q<r>-7 1) (q<r>-6 1))))))
  459. (let (($x2232 (and $x2228 (=> (and (distinct 1 2) true) (= (q<r>-7 2) (q<r>-6 2))))))
  460. (and $x2232 (=> (and (distinct 1 3) true) (= (q<r>-7 3) (q<r>-6 3)))))))
  461. (assert
  462. (let ((?x2210 (q<o>-7 1)))
  463. (= ?x2210 (+ (q<o>-6 0) tmp<o>-20))))
  464. (assert
  465. (and true (= (q<r>-7 1) (+ (q<r>-6 0) tmp<r>-20))))
  466. (assert
  467. (let ((?x1019 (r<o>-4 3)))
  468. (let ((?x63 (A<o>-0 1 3)))
  469. (let ((?x2241 (* ?x63 ?x1019)))
  470. (= tmp<o>-21 ?x2241)))))
  471. (assert
  472. (and true (= tmp<r>-21 (* (A<r>-0 1 3) (r<r>-4 3)))))
  473. (assert
  474. (let (($x2255 (and (=> (and (distinct 1 0) true) (= (q<o>-8 0) (q<o>-7 0))) (=> (and (distinct 1 1) true) (= (q<o>-8 1) (q<o>-7 1))))))
  475. (let (($x2259 (and $x2255 (=> (and (distinct 1 2) true) (= (q<o>-8 2) (q<o>-7 2))))))
  476. (and $x2259 (=> (and (distinct 1 3) true) (= (q<o>-8 3) (q<o>-7 3)))))))
  477. (assert
  478. (let (($x2270 (and (=> (and (distinct 1 0) true) (= (q<r>-8 0) (q<r>-7 0))) (=> (and (distinct 1 1) true) (= (q<r>-8 1) (q<r>-7 1))))))
  479. (let (($x2274 (and $x2270 (=> (and (distinct 1 2) true) (= (q<r>-8 2) (q<r>-7 2))))))
  480. (and $x2274 (=> (and (distinct 1 3) true) (= (q<r>-8 3) (q<r>-7 3)))))))
  481. (assert
  482. (let ((?x2252 (q<o>-8 1)))
  483. (= ?x2252 (+ (q<o>-7 0) tmp<o>-21))))
  484. (assert
  485. (and true (= (q<r>-8 1) (+ (q<r>-7 0) tmp<r>-21))))
  486. (assert
  487. (let (($x2290 (and (=> (and (distinct 2 0) true) (= (q<o>-9 0) (q<o>-8 0))) (=> (and (distinct 2 1) true) (= (q<o>-9 1) (q<o>-8 1))))))
  488. (let (($x2294 (and $x2290 (=> (and (distinct 2 2) true) (= (q<o>-9 2) (q<o>-8 2))))))
  489. (and $x2294 (=> (and (distinct 2 3) true) (= (q<o>-9 3) (q<o>-8 3)))))))
  490. (assert
  491. (let (($x2305 (and (=> (and (distinct 2 0) true) (= (q<r>-9 0) (q<r>-8 0))) (=> (and (distinct 2 1) true) (= (q<r>-9 1) (q<r>-8 1))))))
  492. (let (($x2309 (and $x2305 (=> (and (distinct 2 2) true) (= (q<r>-9 2) (q<r>-8 2))))))
  493. (and $x2309 (=> (and (distinct 2 3) true) (= (q<r>-9 3) (q<r>-8 3)))))))
  494. (assert
  495. (let ((?x1006 (r<o>-4 0)))
  496. (let ((?x67 (A<o>-0 2 0)))
  497. (let ((?x2283 (* ?x67 ?x1006)))
  498. (let ((?x2291 (q<o>-9 2)))
  499. (= ?x2291 ?x2283))))))
  500. (assert
  501. (and true (= (q<r>-9 2) (* (A<r>-0 2 0) (r<r>-4 0)))))
  502. (assert
  503. (let ((?x1011 (r<o>-4 1)))
  504. (let ((?x71 (A<o>-0 2 1)))
  505. (let ((?x2318 (* ?x71 ?x1011)))
  506. (= tmp<o>-22 ?x2318)))))
  507. (assert
  508. (and true (= tmp<r>-22 (* (A<r>-0 2 1) (r<r>-4 1)))))
  509. (assert
  510. (let (($x2332 (and (=> (and (distinct 2 0) true) (= (q<o>-10 0) (q<o>-9 0))) (=> (and (distinct 2 1) true) (= (q<o>-10 1) (q<o>-9 1))))))
  511. (let (($x2336 (and $x2332 (=> (and (distinct 2 2) true) (= (q<o>-10 2) (q<o>-9 2))))))
  512. (and $x2336 (=> (and (distinct 2 3) true) (= (q<o>-10 3) (q<o>-9 3)))))))
  513. (assert
  514. (let (($x2347 (and (=> (and (distinct 2 0) true) (= (q<r>-10 0) (q<r>-9 0))) (=> (and (distinct 2 1) true) (= (q<r>-10 1) (q<r>-9 1))))))
  515. (let (($x2351 (and $x2347 (=> (and (distinct 2 2) true) (= (q<r>-10 2) (q<r>-9 2))))))
  516. (and $x2351 (=> (and (distinct 2 3) true) (= (q<r>-10 3) (q<r>-9 3)))))))
  517. (assert
  518. (let ((?x2333 (q<o>-10 2)))
  519. (= ?x2333 (+ (q<o>-9 0) tmp<o>-22))))
  520. (assert
  521. (and true (= (q<r>-10 2) (+ (q<r>-9 0) tmp<r>-22))))
  522. (assert
  523. (let ((?x1015 (r<o>-4 2)))
  524. (let ((?x75 (A<o>-0 2 2)))
  525. (let ((?x2360 (* ?x75 ?x1015)))
  526. (= tmp<o>-23 ?x2360)))))
  527. (assert
  528. (and true (= tmp<r>-23 (* (A<r>-0 2 2) (r<r>-4 2)))))
  529. (assert
  530. (let (($x2374 (and (=> (and (distinct 2 0) true) (= (q<o>-11 0) (q<o>-10 0))) (=> (and (distinct 2 1) true) (= (q<o>-11 1) (q<o>-10 1))))))
  531. (let (($x2378 (and $x2374 (=> (and (distinct 2 2) true) (= (q<o>-11 2) (q<o>-10 2))))))
  532. (and $x2378 (=> (and (distinct 2 3) true) (= (q<o>-11 3) (q<o>-10 3)))))))
  533. (assert
  534. (let (($x2389 (and (=> (and (distinct 2 0) true) (= (q<r>-11 0) (q<r>-10 0))) (=> (and (distinct 2 1) true) (= (q<r>-11 1) (q<r>-10 1))))))
  535. (let (($x2393 (and $x2389 (=> (and (distinct 2 2) true) (= (q<r>-11 2) (q<r>-10 2))))))
  536. (and $x2393 (=> (and (distinct 2 3) true) (= (q<r>-11 3) (q<r>-10 3)))))))
  537. (assert
  538. (let ((?x2375 (q<o>-11 2)))
  539. (= ?x2375 (+ (q<o>-10 0) tmp<o>-23))))
  540. (assert
  541. (and true (= (q<r>-11 2) (+ (q<r>-10 0) tmp<r>-23))))
  542. (assert
  543. (let ((?x1019 (r<o>-4 3)))
  544. (let ((?x79 (A<o>-0 2 3)))
  545. (let ((?x2402 (* ?x79 ?x1019)))
  546. (= tmp<o>-24 ?x2402)))))
  547. (assert
  548. (and true (= tmp<r>-24 (* (A<r>-0 2 3) (r<r>-4 3)))))
  549. (assert
  550. (let (($x2416 (and (=> (and (distinct 2 0) true) (= (q<o>-12 0) (q<o>-11 0))) (=> (and (distinct 2 1) true) (= (q<o>-12 1) (q<o>-11 1))))))
  551. (let (($x2420 (and $x2416 (=> (and (distinct 2 2) true) (= (q<o>-12 2) (q<o>-11 2))))))
  552. (and $x2420 (=> (and (distinct 2 3) true) (= (q<o>-12 3) (q<o>-11 3)))))))
  553. (assert
  554. (let (($x2431 (and (=> (and (distinct 2 0) true) (= (q<r>-12 0) (q<r>-11 0))) (=> (and (distinct 2 1) true) (= (q<r>-12 1) (q<r>-11 1))))))
  555. (let (($x2435 (and $x2431 (=> (and (distinct 2 2) true) (= (q<r>-12 2) (q<r>-11 2))))))
  556. (and $x2435 (=> (and (distinct 2 3) true) (= (q<r>-12 3) (q<r>-11 3)))))))
  557. (assert
  558. (let ((?x2417 (q<o>-12 2)))
  559. (= ?x2417 (+ (q<o>-11 0) tmp<o>-24))))
  560. (assert
  561. (and true (= (q<r>-12 2) (+ (q<r>-11 0) tmp<r>-24))))
  562. (assert
  563. (let (($x2451 (and (=> (and (distinct 3 0) true) (= (q<o>-13 0) (q<o>-12 0))) (=> (and (distinct 3 1) true) (= (q<o>-13 1) (q<o>-12 1))))))
  564. (let (($x2455 (and $x2451 (=> (and (distinct 3 2) true) (= (q<o>-13 2) (q<o>-12 2))))))
  565. (and $x2455 (=> (and (distinct 3 3) true) (= (q<o>-13 3) (q<o>-12 3)))))))
  566. (assert
  567. (let (($x2466 (and (=> (and (distinct 3 0) true) (= (q<r>-13 0) (q<r>-12 0))) (=> (and (distinct 3 1) true) (= (q<r>-13 1) (q<r>-12 1))))))
  568. (let (($x2470 (and $x2466 (=> (and (distinct 3 2) true) (= (q<r>-13 2) (q<r>-12 2))))))
  569. (and $x2470 (=> (and (distinct 3 3) true) (= (q<r>-13 3) (q<r>-12 3)))))))
  570. (assert
  571. (let ((?x1006 (r<o>-4 0)))
  572. (let ((?x83 (A<o>-0 3 0)))
  573. (let ((?x2444 (* ?x83 ?x1006)))
  574. (let ((?x2456 (q<o>-13 3)))
  575. (= ?x2456 ?x2444))))))
  576. (assert
  577. (and true (= (q<r>-13 3) (* (A<r>-0 3 0) (r<r>-4 0)))))
  578. (assert
  579. (let ((?x1011 (r<o>-4 1)))
  580. (let ((?x87 (A<o>-0 3 1)))
  581. (let ((?x2479 (* ?x87 ?x1011)))
  582. (= tmp<o>-25 ?x2479)))))
  583. (assert
  584. (and true (= tmp<r>-25 (* (A<r>-0 3 1) (r<r>-4 1)))))
  585. (assert
  586. (let (($x2493 (and (=> (and (distinct 3 0) true) (= (q<o>-14 0) (q<o>-13 0))) (=> (and (distinct 3 1) true) (= (q<o>-14 1) (q<o>-13 1))))))
  587. (let (($x2497 (and $x2493 (=> (and (distinct 3 2) true) (= (q<o>-14 2) (q<o>-13 2))))))
  588. (and $x2497 (=> (and (distinct 3 3) true) (= (q<o>-14 3) (q<o>-13 3)))))))
  589. (assert
  590. (let (($x2508 (and (=> (and (distinct 3 0) true) (= (q<r>-14 0) (q<r>-13 0))) (=> (and (distinct 3 1) true) (= (q<r>-14 1) (q<r>-13 1))))))
  591. (let (($x2512 (and $x2508 (=> (and (distinct 3 2) true) (= (q<r>-14 2) (q<r>-13 2))))))
  592. (and $x2512 (=> (and (distinct 3 3) true) (= (q<r>-14 3) (q<r>-13 3)))))))
  593. (assert
  594. (let ((?x2498 (q<o>-14 3)))
  595. (= ?x2498 (+ (q<o>-13 0) tmp<o>-25))))
  596. (assert
  597. (and true (= (q<r>-14 3) (+ (q<r>-13 0) tmp<r>-25))))
  598. (assert
  599. (let ((?x1015 (r<o>-4 2)))
  600. (let ((?x91 (A<o>-0 3 2)))
  601. (let ((?x2521 (* ?x91 ?x1015)))
  602. (= tmp<o>-26 ?x2521)))))
  603. (assert
  604. (and true (= tmp<r>-26 (* (A<r>-0 3 2) (r<r>-4 2)))))
  605. (assert
  606. (let (($x2535 (and (=> (and (distinct 3 0) true) (= (q<o>-15 0) (q<o>-14 0))) (=> (and (distinct 3 1) true) (= (q<o>-15 1) (q<o>-14 1))))))
  607. (let (($x2539 (and $x2535 (=> (and (distinct 3 2) true) (= (q<o>-15 2) (q<o>-14 2))))))
  608. (and $x2539 (=> (and (distinct 3 3) true) (= (q<o>-15 3) (q<o>-14 3)))))))
  609. (assert
  610. (let (($x2550 (and (=> (and (distinct 3 0) true) (= (q<r>-15 0) (q<r>-14 0))) (=> (and (distinct 3 1) true) (= (q<r>-15 1) (q<r>-14 1))))))
  611. (let (($x2554 (and $x2550 (=> (and (distinct 3 2) true) (= (q<r>-15 2) (q<r>-14 2))))))
  612. (and $x2554 (=> (and (distinct 3 3) true) (= (q<r>-15 3) (q<r>-14 3)))))))
  613. (assert
  614. (let ((?x2540 (q<o>-15 3)))
  615. (= ?x2540 (+ (q<o>-14 0) tmp<o>-26))))
  616. (assert
  617. (and true (= (q<r>-15 3) (+ (q<r>-14 0) tmp<r>-26))))
  618. (assert
  619. (let ((?x1019 (r<o>-4 3)))
  620. (let ((?x95 (A<o>-0 3 3)))
  621. (let ((?x2563 (* ?x95 ?x1019)))
  622. (= tmp<o>-27 ?x2563)))))
  623. (assert
  624. (and true (= tmp<r>-27 (* (A<r>-0 3 3) (r<r>-4 3)))))
  625. (assert
  626. (let (($x2577 (and (=> (and (distinct 3 0) true) (= (q<o>-16 0) (q<o>-15 0))) (=> (and (distinct 3 1) true) (= (q<o>-16 1) (q<o>-15 1))))))
  627. (let (($x2581 (and $x2577 (=> (and (distinct 3 2) true) (= (q<o>-16 2) (q<o>-15 2))))))
  628. (and $x2581 (=> (and (distinct 3 3) true) (= (q<o>-16 3) (q<o>-15 3)))))))
  629. (assert
  630. (let (($x2592 (and (=> (and (distinct 3 0) true) (= (q<r>-16 0) (q<r>-15 0))) (=> (and (distinct 3 1) true) (= (q<r>-16 1) (q<r>-15 1))))))
  631. (let (($x2596 (and $x2592 (=> (and (distinct 3 2) true) (= (q<r>-16 2) (q<r>-15 2))))))
  632. (and $x2596 (=> (and (distinct 3 3) true) (= (q<r>-16 3) (q<r>-15 3)))))))
  633. (assert
  634. (let ((?x2582 (q<o>-16 3)))
  635. (= ?x2582 (+ (q<o>-15 0) tmp<o>-27))))
  636. (assert
  637. (and true (= (q<r>-16 3) (+ (q<r>-15 0) tmp<r>-27))))
  638. (assert
  639. (let ((?x2569 (q<o>-16 0)))
  640. (let ((?x1006 (r<o>-4 0)))
  641. (let ((?x2605 (* ?x1006 ?x2569)))
  642. (= rtq<o>-1 ?x2605)))))
  643. (assert
  644. (and true (= rtq<r>-1 (* (r<r>-4 0) (q<r>-16 0)))))
  645. (assert
  646. (let ((?x2574 (q<o>-16 1)))
  647. (let ((?x1011 (r<o>-4 1)))
  648. (let ((?x2612 (* ?x1011 ?x2574)))
  649. (= tmp<o>-28 ?x2612)))))
  650. (assert
  651. (and true (= tmp<r>-28 (* (r<r>-4 1) (q<r>-16 1)))))
  652. (assert
  653. (= rtq<o>-2 (+ rtq<o>-1 tmp<o>-28)))
  654. (assert
  655. (and true (= rtq<r>-2 (+ rtq<r>-1 tmp<r>-28))))
  656. (assert
  657. (let ((?x2578 (q<o>-16 2)))
  658. (let ((?x1015 (r<o>-4 2)))
  659. (let ((?x2626 (* ?x1015 ?x2578)))
  660. (= tmp<o>-29 ?x2626)))))
  661. (assert
  662. (and true (= tmp<r>-29 (* (r<r>-4 2) (q<r>-16 2)))))
  663. (assert
  664. (= rtq<o>-3 (+ rtq<o>-2 tmp<o>-29)))
  665. (assert
  666. (and true (= rtq<r>-3 (+ rtq<r>-2 tmp<r>-29))))
  667. (assert
  668. (let ((?x2582 (q<o>-16 3)))
  669. (let ((?x1019 (r<o>-4 3)))
  670. (let ((?x2640 (* ?x1019 ?x2582)))
  671. (= tmp<o>-30 ?x2640)))))
  672. (assert
  673. (and true (= tmp<r>-30 (* (r<r>-4 3) (q<r>-16 3)))))
  674. (assert
  675. (= rtq<o>-4 (+ rtq<o>-3 tmp<o>-30)))
  676. (assert
  677. (and true (= rtq<r>-4 (+ rtq<r>-3 tmp<r>-30))))
  678. (assert
  679. (let ((?x2654 (/ r_norm<o>-4 rtq<o>-4)))
  680. (= alpha<o>-1 ?x2654)))
  681. (assert
  682. (and true (= alpha<r>-1 (/ r_norm<r>-4 rtq<r>-4))))
  683. (assert
  684. (let (($x2668 (and (=> (and (distinct 0 0) true) (= (alphar<o>-1 0) (alphar<o>-0 0))) (=> (and (distinct 0 1) true) (= (alphar<o>-1 1) (alphar<o>-0 1))))))
  685. (let (($x2672 (and $x2668 (=> (and (distinct 0 2) true) (= (alphar<o>-1 2) (alphar<o>-0 2))))))
  686. (and $x2672 (=> (and (distinct 0 3) true) (= (alphar<o>-1 3) (alphar<o>-0 3)))))))
  687. (assert
  688. (let (($x2683 (and (=> (and (distinct 0 0) true) (= (alphar<r>-1 0) (alphar<r>-0 0))) (=> (and (distinct 0 1) true) (= (alphar<r>-1 1) (alphar<r>-0 1))))))
  689. (let (($x2687 (and $x2683 (=> (and (distinct 0 2) true) (= (alphar<r>-1 2) (alphar<r>-0 2))))))
  690. (and $x2687 (=> (and (distinct 0 3) true) (= (alphar<r>-1 3) (alphar<r>-0 3)))))))
  691. (assert
  692. (let ((?x2660 (alphar<o>-1 0)))
  693. (= ?x2660 (* alpha<o>-1 (r<o>-4 0)))))
  694. (assert
  695. (and true (= (alphar<r>-1 0) (* alpha<r>-1 (r<r>-4 0)))))
  696. (assert
  697. (let (($x2703 (and (=> (and (distinct 1 0) true) (= (alphar<o>-2 0) (alphar<o>-1 0))) (=> (and (distinct 1 1) true) (= (alphar<o>-2 1) (alphar<o>-1 1))))))
  698. (let (($x2707 (and $x2703 (=> (and (distinct 1 2) true) (= (alphar<o>-2 2) (alphar<o>-1 2))))))
  699. (and $x2707 (=> (and (distinct 1 3) true) (= (alphar<o>-2 3) (alphar<o>-1 3)))))))
  700. (assert
  701. (let (($x2718 (and (=> (and (distinct 1 0) true) (= (alphar<r>-2 0) (alphar<r>-1 0))) (=> (and (distinct 1 1) true) (= (alphar<r>-2 1) (alphar<r>-1 1))))))
  702. (let (($x2722 (and $x2718 (=> (and (distinct 1 2) true) (= (alphar<r>-2 2) (alphar<r>-1 2))))))
  703. (and $x2722 (=> (and (distinct 1 3) true) (= (alphar<r>-2 3) (alphar<r>-1 3)))))))
  704. (assert
  705. (let ((?x2700 (alphar<o>-2 1)))
  706. (= ?x2700 (* alpha<o>-1 (r<o>-4 1)))))
  707. (assert
  708. (and true (= (alphar<r>-2 1) (* alpha<r>-1 (r<r>-4 1)))))
  709. (assert
  710. (let (($x2738 (and (=> (and (distinct 2 0) true) (= (alphar<o>-3 0) (alphar<o>-2 0))) (=> (and (distinct 2 1) true) (= (alphar<o>-3 1) (alphar<o>-2 1))))))
  711. (let (($x2742 (and $x2738 (=> (and (distinct 2 2) true) (= (alphar<o>-3 2) (alphar<o>-2 2))))))
  712. (and $x2742 (=> (and (distinct 2 3) true) (= (alphar<o>-3 3) (alphar<o>-2 3)))))))
  713. (assert
  714. (let (($x2753 (and (=> (and (distinct 2 0) true) (= (alphar<r>-3 0) (alphar<r>-2 0))) (=> (and (distinct 2 1) true) (= (alphar<r>-3 1) (alphar<r>-2 1))))))
  715. (let (($x2757 (and $x2753 (=> (and (distinct 2 2) true) (= (alphar<r>-3 2) (alphar<r>-2 2))))))
  716. (and $x2757 (=> (and (distinct 2 3) true) (= (alphar<r>-3 3) (alphar<r>-2 3)))))))
  717. (assert
  718. (let ((?x2739 (alphar<o>-3 2)))
  719. (= ?x2739 (* alpha<o>-1 (r<o>-4 2)))))
  720. (assert
  721. (and true (= (alphar<r>-3 2) (* alpha<r>-1 (r<r>-4 2)))))
  722. (assert
  723. (let (($x2773 (and (=> (and (distinct 3 0) true) (= (alphar<o>-4 0) (alphar<o>-3 0))) (=> (and (distinct 3 1) true) (= (alphar<o>-4 1) (alphar<o>-3 1))))))
  724. (let (($x2777 (and $x2773 (=> (and (distinct 3 2) true) (= (alphar<o>-4 2) (alphar<o>-3 2))))))
  725. (and $x2777 (=> (and (distinct 3 3) true) (= (alphar<o>-4 3) (alphar<o>-3 3)))))))
  726. (assert
  727. (let (($x2788 (and (=> (and (distinct 3 0) true) (= (alphar<r>-4 0) (alphar<r>-3 0))) (=> (and (distinct 3 1) true) (= (alphar<r>-4 1) (alphar<r>-3 1))))))
  728. (let (($x2792 (and $x2788 (=> (and (distinct 3 2) true) (= (alphar<r>-4 2) (alphar<r>-3 2))))))
  729. (and $x2792 (=> (and (distinct 3 3) true) (= (alphar<r>-4 3) (alphar<r>-3 3)))))))
  730. (assert
  731. (let ((?x2778 (alphar<o>-4 3)))
  732. (= ?x2778 (* alpha<o>-1 (r<o>-4 3)))))
  733. (assert
  734. (and true (= (alphar<r>-4 3) (* alpha<r>-1 (r<r>-4 3)))))
  735. (assert
  736. (let (($x2808 (and (=> (and (distinct 0 0) true) (= (x<o>-1 0) (x<o>-0 0))) (=> (and (distinct 0 1) true) (= (x<o>-1 1) (x<o>-0 1))))))
  737. (let (($x2812 (and $x2808 (=> (and (distinct 0 2) true) (= (x<o>-1 2) (x<o>-0 2))))))
  738. (and $x2812 (=> (and (distinct 0 3) true) (= (x<o>-1 3) (x<o>-0 3)))))))
  739. (assert
  740. (let (($x2823 (and (=> (and (distinct 0 0) true) (= (x<r>-1 0) (x<r>-0 0))) (=> (and (distinct 0 1) true) (= (x<r>-1 1) (x<r>-0 1))))))
  741. (let (($x2827 (and $x2823 (=> (and (distinct 0 2) true) (= (x<r>-1 2) (x<r>-0 2))))))
  742. (and $x2827 (=> (and (distinct 0 3) true) (= (x<r>-1 3) (x<r>-0 3)))))))
  743. (assert
  744. (let ((?x2800 (x<o>-1 0)))
  745. (= ?x2800 (+ (x<o>-0 0) (alphar<o>-4 0)))))
  746. (assert
  747. (and true (= (x<r>-1 0) (+ (x<r>-0 0) (alphar<r>-4 0)))))
  748. (assert
  749. (let (($x2843 (and (=> (and (distinct 1 0) true) (= (x<o>-2 0) (x<o>-1 0))) (=> (and (distinct 1 1) true) (= (x<o>-2 1) (x<o>-1 1))))))
  750. (let (($x2847 (and $x2843 (=> (and (distinct 1 2) true) (= (x<o>-2 2) (x<o>-1 2))))))
  751. (and $x2847 (=> (and (distinct 1 3) true) (= (x<o>-2 3) (x<o>-1 3)))))))
  752. (assert
  753. (let (($x2858 (and (=> (and (distinct 1 0) true) (= (x<r>-2 0) (x<r>-1 0))) (=> (and (distinct 1 1) true) (= (x<r>-2 1) (x<r>-1 1))))))
  754. (let (($x2862 (and $x2858 (=> (and (distinct 1 2) true) (= (x<r>-2 2) (x<r>-1 2))))))
  755. (and $x2862 (=> (and (distinct 1 3) true) (= (x<r>-2 3) (x<r>-1 3)))))))
  756. (assert
  757. (let ((?x2840 (x<o>-2 1)))
  758. (= ?x2840 (+ (x<o>-1 1) (alphar<o>-4 1)))))
  759. (assert
  760. (and true (= (x<r>-2 1) (+ (x<r>-1 1) (alphar<r>-4 1)))))
  761. (assert
  762. (let (($x2878 (and (=> (and (distinct 2 0) true) (= (x<o>-3 0) (x<o>-2 0))) (=> (and (distinct 2 1) true) (= (x<o>-3 1) (x<o>-2 1))))))
  763. (let (($x2882 (and $x2878 (=> (and (distinct 2 2) true) (= (x<o>-3 2) (x<o>-2 2))))))
  764. (and $x2882 (=> (and (distinct 2 3) true) (= (x<o>-3 3) (x<o>-2 3)))))))
  765. (assert
  766. (let (($x2893 (and (=> (and (distinct 2 0) true) (= (x<r>-3 0) (x<r>-2 0))) (=> (and (distinct 2 1) true) (= (x<r>-3 1) (x<r>-2 1))))))
  767. (let (($x2897 (and $x2893 (=> (and (distinct 2 2) true) (= (x<r>-3 2) (x<r>-2 2))))))
  768. (and $x2897 (=> (and (distinct 2 3) true) (= (x<r>-3 3) (x<r>-2 3)))))))
  769. (assert
  770. (let ((?x2879 (x<o>-3 2)))
  771. (= ?x2879 (+ (x<o>-2 2) (alphar<o>-4 2)))))
  772. (assert
  773. (and true (= (x<r>-3 2) (+ (x<r>-2 2) (alphar<r>-4 2)))))
  774. (assert
  775. (let (($x2913 (and (=> (and (distinct 3 0) true) (= (x<o>-4 0) (x<o>-3 0))) (=> (and (distinct 3 1) true) (= (x<o>-4 1) (x<o>-3 1))))))
  776. (let (($x2917 (and $x2913 (=> (and (distinct 3 2) true) (= (x<o>-4 2) (x<o>-3 2))))))
  777. (and $x2917 (=> (and (distinct 3 3) true) (= (x<o>-4 3) (x<o>-3 3)))))))
  778. (assert
  779. (let (($x2928 (and (=> (and (distinct 3 0) true) (= (x<r>-4 0) (x<r>-3 0))) (=> (and (distinct 3 1) true) (= (x<r>-4 1) (x<r>-3 1))))))
  780. (let (($x2932 (and $x2928 (=> (and (distinct 3 2) true) (= (x<r>-4 2) (x<r>-3 2))))))
  781. (and $x2932 (=> (and (distinct 3 3) true) (= (x<r>-4 3) (x<r>-3 3)))))))
  782. (assert
  783. (let ((?x2918 (x<o>-4 3)))
  784. (= ?x2918 (+ (x<o>-3 3) (alphar<o>-4 3)))))
  785. (assert
  786. (and true (= (x<r>-4 3) (+ (x<r>-3 3) (alphar<r>-4 3)))))
  787. (assert
  788. (let (($x2948 (and (=> (and (distinct 0 0) true) (= (alphaq<o>-1 0) (alphaq<o>-0 0))) (=> (and (distinct 0 1) true) (= (alphaq<o>-1 1) (alphaq<o>-0 1))))))
  789. (let (($x2952 (and $x2948 (=> (and (distinct 0 2) true) (= (alphaq<o>-1 2) (alphaq<o>-0 2))))))
  790. (and $x2952 (=> (and (distinct 0 3) true) (= (alphaq<o>-1 3) (alphaq<o>-0 3)))))))
  791. (assert
  792. (let (($x2963 (and (=> (and (distinct 0 0) true) (= (alphaq<r>-1 0) (alphaq<r>-0 0))) (=> (and (distinct 0 1) true) (= (alphaq<r>-1 1) (alphaq<r>-0 1))))))
  793. (let (($x2967 (and $x2963 (=> (and (distinct 0 2) true) (= (alphaq<r>-1 2) (alphaq<r>-0 2))))))
  794. (and $x2967 (=> (and (distinct 0 3) true) (= (alphaq<r>-1 3) (alphaq<r>-0 3)))))))
  795. (assert
  796. (let ((?x2940 (alphaq<o>-1 0)))
  797. (= ?x2940 (* alpha<o>-1 (q<o>-16 0)))))
  798. (assert
  799. (and true (= (alphaq<r>-1 0) (* alpha<r>-1 (q<r>-16 0)))))
  800. (assert
  801. (let (($x2983 (and (=> (and (distinct 1 0) true) (= (alphaq<o>-2 0) (alphaq<o>-1 0))) (=> (and (distinct 1 1) true) (= (alphaq<o>-2 1) (alphaq<o>-1 1))))))
  802. (let (($x2987 (and $x2983 (=> (and (distinct 1 2) true) (= (alphaq<o>-2 2) (alphaq<o>-1 2))))))
  803. (and $x2987 (=> (and (distinct 1 3) true) (= (alphaq<o>-2 3) (alphaq<o>-1 3)))))))
  804. (assert
  805. (let (($x2998 (and (=> (and (distinct 1 0) true) (= (alphaq<r>-2 0) (alphaq<r>-1 0))) (=> (and (distinct 1 1) true) (= (alphaq<r>-2 1) (alphaq<r>-1 1))))))
  806. (let (($x3002 (and $x2998 (=> (and (distinct 1 2) true) (= (alphaq<r>-2 2) (alphaq<r>-1 2))))))
  807. (and $x3002 (=> (and (distinct 1 3) true) (= (alphaq<r>-2 3) (alphaq<r>-1 3)))))))
  808. (assert
  809. (let ((?x2980 (alphaq<o>-2 1)))
  810. (= ?x2980 (* alpha<o>-1 (q<o>-16 1)))))
  811. (assert
  812. (and true (= (alphaq<r>-2 1) (* alpha<r>-1 (q<r>-16 1)))))
  813. (assert
  814. (let (($x3018 (and (=> (and (distinct 2 0) true) (= (alphaq<o>-3 0) (alphaq<o>-2 0))) (=> (and (distinct 2 1) true) (= (alphaq<o>-3 1) (alphaq<o>-2 1))))))
  815. (let (($x3022 (and $x3018 (=> (and (distinct 2 2) true) (= (alphaq<o>-3 2) (alphaq<o>-2 2))))))
  816. (and $x3022 (=> (and (distinct 2 3) true) (= (alphaq<o>-3 3) (alphaq<o>-2 3)))))))
  817. (assert
  818. (let (($x3033 (and (=> (and (distinct 2 0) true) (= (alphaq<r>-3 0) (alphaq<r>-2 0))) (=> (and (distinct 2 1) true) (= (alphaq<r>-3 1) (alphaq<r>-2 1))))))
  819. (let (($x3037 (and $x3033 (=> (and (distinct 2 2) true) (= (alphaq<r>-3 2) (alphaq<r>-2 2))))))
  820. (and $x3037 (=> (and (distinct 2 3) true) (= (alphaq<r>-3 3) (alphaq<r>-2 3)))))))
  821. (assert
  822. (let ((?x3019 (alphaq<o>-3 2)))
  823. (= ?x3019 (* alpha<o>-1 (q<o>-16 2)))))
  824. (assert
  825. (and true (= (alphaq<r>-3 2) (* alpha<r>-1 (q<r>-16 2)))))
  826. (assert
  827. (let (($x3053 (and (=> (and (distinct 3 0) true) (= (alphaq<o>-4 0) (alphaq<o>-3 0))) (=> (and (distinct 3 1) true) (= (alphaq<o>-4 1) (alphaq<o>-3 1))))))
  828. (let (($x3057 (and $x3053 (=> (and (distinct 3 2) true) (= (alphaq<o>-4 2) (alphaq<o>-3 2))))))
  829. (and $x3057 (=> (and (distinct 3 3) true) (= (alphaq<o>-4 3) (alphaq<o>-3 3)))))))
  830. (assert
  831. (let (($x3068 (and (=> (and (distinct 3 0) true) (= (alphaq<r>-4 0) (alphaq<r>-3 0))) (=> (and (distinct 3 1) true) (= (alphaq<r>-4 1) (alphaq<r>-3 1))))))
  832. (let (($x3072 (and $x3068 (=> (and (distinct 3 2) true) (= (alphaq<r>-4 2) (alphaq<r>-3 2))))))
  833. (and $x3072 (=> (and (distinct 3 3) true) (= (alphaq<r>-4 3) (alphaq<r>-3 3)))))))
  834. (assert
  835. (let ((?x3058 (alphaq<o>-4 3)))
  836. (= ?x3058 (* alpha<o>-1 (q<o>-16 3)))))
  837. (assert
  838. (and true (= (alphaq<r>-4 3) (* alpha<r>-1 (q<r>-16 3)))))
  839. (assert
  840. (let (($x3088 (and (=> (and (distinct 0 0) true) (= (r<o>-5 0) (r<o>-4 0))) (=> (and (distinct 0 1) true) (= (r<o>-5 1) (r<o>-4 1))))))
  841. (let (($x3092 (and $x3088 (=> (and (distinct 0 2) true) (= (r<o>-5 2) (r<o>-4 2))))))
  842. (and $x3092 (=> (and (distinct 0 3) true) (= (r<o>-5 3) (r<o>-4 3)))))))
  843. (assert
  844. (let (($x3103 (and (=> (and (distinct 0 0) true) (= (r<r>-5 0) (r<r>-4 0))) (=> (and (distinct 0 1) true) (= (r<r>-5 1) (r<r>-4 1))))))
  845. (let (($x3107 (and $x3103 (=> (and (distinct 0 2) true) (= (r<r>-5 2) (r<r>-4 2))))))
  846. (and $x3107 (=> (and (distinct 0 3) true) (= (r<r>-5 3) (r<r>-4 3)))))))
  847. (assert
  848. (let ((?x3080 (r<o>-5 0)))
  849. (= ?x3080 (- (r<o>-4 0) (alphaq<o>-4 0)))))
  850. (assert
  851. (and true (= (r<r>-5 0) (- (r<r>-4 0) (alphaq<r>-4 0)))))
  852. (assert
  853. (let (($x3123 (and (=> (and (distinct 1 0) true) (= (r<o>-6 0) (r<o>-5 0))) (=> (and (distinct 1 1) true) (= (r<o>-6 1) (r<o>-5 1))))))
  854. (let (($x3127 (and $x3123 (=> (and (distinct 1 2) true) (= (r<o>-6 2) (r<o>-5 2))))))
  855. (and $x3127 (=> (and (distinct 1 3) true) (= (r<o>-6 3) (r<o>-5 3)))))))
  856. (assert
  857. (let (($x3138 (and (=> (and (distinct 1 0) true) (= (r<r>-6 0) (r<r>-5 0))) (=> (and (distinct 1 1) true) (= (r<r>-6 1) (r<r>-5 1))))))
  858. (let (($x3142 (and $x3138 (=> (and (distinct 1 2) true) (= (r<r>-6 2) (r<r>-5 2))))))
  859. (and $x3142 (=> (and (distinct 1 3) true) (= (r<r>-6 3) (r<r>-5 3)))))))
  860. (assert
  861. (let ((?x3120 (r<o>-6 1)))
  862. (= ?x3120 (- (r<o>-5 1) (alphaq<o>-4 1)))))
  863. (assert
  864. (and true (= (r<r>-6 1) (- (r<r>-5 1) (alphaq<r>-4 1)))))
  865. (assert
  866. (let (($x3158 (and (=> (and (distinct 2 0) true) (= (r<o>-7 0) (r<o>-6 0))) (=> (and (distinct 2 1) true) (= (r<o>-7 1) (r<o>-6 1))))))
  867. (let (($x3162 (and $x3158 (=> (and (distinct 2 2) true) (= (r<o>-7 2) (r<o>-6 2))))))
  868. (and $x3162 (=> (and (distinct 2 3) true) (= (r<o>-7 3) (r<o>-6 3)))))))
  869. (assert
  870. (let (($x3173 (and (=> (and (distinct 2 0) true) (= (r<r>-7 0) (r<r>-6 0))) (=> (and (distinct 2 1) true) (= (r<r>-7 1) (r<r>-6 1))))))
  871. (let (($x3177 (and $x3173 (=> (and (distinct 2 2) true) (= (r<r>-7 2) (r<r>-6 2))))))
  872. (and $x3177 (=> (and (distinct 2 3) true) (= (r<r>-7 3) (r<r>-6 3)))))))
  873. (assert
  874. (let ((?x3159 (r<o>-7 2)))
  875. (= ?x3159 (- (r<o>-6 2) (alphaq<o>-4 2)))))
  876. (assert
  877. (and true (= (r<r>-7 2) (- (r<r>-6 2) (alphaq<r>-4 2)))))
  878. (assert
  879. (let (($x3193 (and (=> (and (distinct 3 0) true) (= (r<o>-8 0) (r<o>-7 0))) (=> (and (distinct 3 1) true) (= (r<o>-8 1) (r<o>-7 1))))))
  880. (let (($x3197 (and $x3193 (=> (and (distinct 3 2) true) (= (r<o>-8 2) (r<o>-7 2))))))
  881. (and $x3197 (=> (and (distinct 3 3) true) (= (r<o>-8 3) (r<o>-7 3)))))))
  882. (assert
  883. (let (($x3208 (and (=> (and (distinct 3 0) true) (= (r<r>-8 0) (r<r>-7 0))) (=> (and (distinct 3 1) true) (= (r<r>-8 1) (r<r>-7 1))))))
  884. (let (($x3212 (and $x3208 (=> (and (distinct 3 2) true) (= (r<r>-8 2) (r<r>-7 2))))))
  885. (and $x3212 (=> (and (distinct 3 3) true) (= (r<r>-8 3) (r<r>-7 3)))))))
  886. (assert
  887. (let ((?x3198 (r<o>-8 3)))
  888. (= ?x3198 (- (r<o>-7 3) (alphaq<o>-4 3)))))
  889. (assert
  890. (and true (= (r<r>-8 3) (- (r<r>-7 3) (alphaq<r>-4 3)))))
  891. (assert
  892. (let ((?x3185 (r<o>-8 0)))
  893. (let ((?x3221 (* ?x3185 ?x3185)))
  894. (= r_norm<o>-5 ?x3221))))
  895. (assert
  896. (and true (= r_norm<r>-5 (* (r<r>-8 0) (r<r>-8 0)))))
  897. (assert
  898. (let ((?x3190 (r<o>-8 1)))
  899. (let ((?x3228 (* ?x3190 ?x3190)))
  900. (= tmp<o>-31 ?x3228))))
  901. (assert
  902. (and true (= tmp<r>-31 (* (r<r>-8 1) (r<r>-8 1)))))
  903. (assert
  904. (= r_norm<o>-6 (+ r_norm<o>-5 tmp<o>-31)))
  905. (assert
  906. (and true (= r_norm<r>-6 (+ r_norm<r>-5 tmp<r>-31))))
  907. (assert
  908. (let ((?x3194 (r<o>-8 2)))
  909. (let ((?x3242 (* ?x3194 ?x3194)))
  910. (= tmp<o>-32 ?x3242))))
  911. (assert
  912. (and true (= tmp<r>-32 (* (r<r>-8 2) (r<r>-8 2)))))
  913. (assert
  914. (= r_norm<o>-7 (+ r_norm<o>-6 tmp<o>-32)))
  915. (assert
  916. (and true (= r_norm<r>-7 (+ r_norm<r>-6 tmp<r>-32))))
  917. (assert
  918. (let ((?x3198 (r<o>-8 3)))
  919. (let ((?x3256 (* ?x3198 ?x3198)))
  920. (= tmp<o>-33 ?x3256))))
  921. (assert
  922. (and true (= tmp<r>-33 (* (r<r>-8 3) (r<r>-8 3)))))
  923. (assert
  924. (= r_norm<o>-8 (+ r_norm<o>-7 tmp<o>-33)))
  925. (assert
  926. (and true (= r_norm<r>-8 (+ r_norm<r>-7 tmp<r>-33))))
  927. (assert
  928. (= i<o>-2 (+ i<o>-1 1)))
  929. (assert
  930. (and true (= i<r>-2 (+ i<r>-1 1))))
  931. (assert
  932. (let (($x3284 (and (=> (and (distinct 0 0) true) (= (Ax<o>-17 0) (Ax<o>-16 0))) (=> (and (distinct 0 1) true) (= (Ax<o>-17 1) (Ax<o>-16 1))))))
  933. (let (($x3288 (and $x3284 (=> (and (distinct 0 2) true) (= (Ax<o>-17 2) (Ax<o>-16 2))))))
  934. (and $x3288 (=> (and (distinct 0 3) true) (= (Ax<o>-17 3) (Ax<o>-16 3)))))))
  935. (assert
  936. (let (($x3299 (and (=> (and (distinct 0 0) true) (= (Ax<r>-17 0) (Ax<r>-16 0))) (=> (and (distinct 0 1) true) (= (Ax<r>-17 1) (Ax<r>-16 1))))))
  937. (let (($x3303 (and $x3299 (=> (and (distinct 0 2) true) (= (Ax<r>-17 2) (Ax<r>-16 2))))))
  938. (and $x3303 (=> (and (distinct 0 3) true) (= (Ax<r>-17 3) (Ax<r>-16 3)))))))
  939. (assert
  940. (let ((?x2905 (x<o>-4 0)))
  941. (let ((?x34 (A<o>-0 0 0)))
  942. (let ((?x3277 (* ?x34 ?x2905)))
  943. (let ((?x3276 (Ax<o>-17 0)))
  944. (= ?x3276 ?x3277))))))
  945. (assert
  946. (and true (= (Ax<r>-17 0) (* (A<r>-0 0 0) (x<r>-4 0)))))
  947. (assert
  948. (let ((?x2910 (x<o>-4 1)))
  949. (let ((?x37 (A<o>-0 0 1)))
  950. (let ((?x3312 (* ?x37 ?x2910)))
  951. (= tmp<o>-34 ?x3312)))))
  952. (assert
  953. (and true (= tmp<r>-34 (* (A<r>-0 0 1) (x<r>-4 1)))))
  954. (assert
  955. (let (($x3326 (and (=> (and (distinct 0 0) true) (= (Ax<o>-18 0) (Ax<o>-17 0))) (=> (and (distinct 0 1) true) (= (Ax<o>-18 1) (Ax<o>-17 1))))))
  956. (let (($x3330 (and $x3326 (=> (and (distinct 0 2) true) (= (Ax<o>-18 2) (Ax<o>-17 2))))))
  957. (and $x3330 (=> (and (distinct 0 3) true) (= (Ax<o>-18 3) (Ax<o>-17 3)))))))
  958. (assert
  959. (let (($x3341 (and (=> (and (distinct 0 0) true) (= (Ax<r>-18 0) (Ax<r>-17 0))) (=> (and (distinct 0 1) true) (= (Ax<r>-18 1) (Ax<r>-17 1))))))
  960. (let (($x3345 (and $x3341 (=> (and (distinct 0 2) true) (= (Ax<r>-18 2) (Ax<r>-17 2))))))
  961. (and $x3345 (=> (and (distinct 0 3) true) (= (Ax<r>-18 3) (Ax<r>-17 3)))))))
  962. (assert
  963. (let ((?x3318 (Ax<o>-18 0)))
  964. (= ?x3318 (+ (Ax<o>-17 0) tmp<o>-34))))
  965. (assert
  966. (and true (= (Ax<r>-18 0) (+ (Ax<r>-17 0) tmp<r>-34))))
  967. (assert
  968. (let ((?x2914 (x<o>-4 2)))
  969. (let ((?x42 (A<o>-0 0 2)))
  970. (let ((?x3354 (* ?x42 ?x2914)))
  971. (= tmp<o>-35 ?x3354)))))
  972. (assert
  973. (and true (= tmp<r>-35 (* (A<r>-0 0 2) (x<r>-4 2)))))
  974. (assert
  975. (let (($x3368 (and (=> (and (distinct 0 0) true) (= (Ax<o>-19 0) (Ax<o>-18 0))) (=> (and (distinct 0 1) true) (= (Ax<o>-19 1) (Ax<o>-18 1))))))
  976. (let (($x3372 (and $x3368 (=> (and (distinct 0 2) true) (= (Ax<o>-19 2) (Ax<o>-18 2))))))
  977. (and $x3372 (=> (and (distinct 0 3) true) (= (Ax<o>-19 3) (Ax<o>-18 3)))))))
  978. (assert
  979. (let (($x3383 (and (=> (and (distinct 0 0) true) (= (Ax<r>-19 0) (Ax<r>-18 0))) (=> (and (distinct 0 1) true) (= (Ax<r>-19 1) (Ax<r>-18 1))))))
  980. (let (($x3387 (and $x3383 (=> (and (distinct 0 2) true) (= (Ax<r>-19 2) (Ax<r>-18 2))))))
  981. (and $x3387 (=> (and (distinct 0 3) true) (= (Ax<r>-19 3) (Ax<r>-18 3)))))))
  982. (assert
  983. (let ((?x3360 (Ax<o>-19 0)))
  984. (= ?x3360 (+ (Ax<o>-18 0) tmp<o>-35))))
  985. (assert
  986. (and true (= (Ax<r>-19 0) (+ (Ax<r>-18 0) tmp<r>-35))))
  987. (assert
  988. (let ((?x2918 (x<o>-4 3)))
  989. (let ((?x47 (A<o>-0 0 3)))
  990. (let ((?x3396 (* ?x47 ?x2918)))
  991. (= tmp<o>-36 ?x3396)))))
  992. (assert
  993. (and true (= tmp<r>-36 (* (A<r>-0 0 3) (x<r>-4 3)))))
  994. (assert
  995. (let (($x3410 (and (=> (and (distinct 0 0) true) (= (Ax<o>-20 0) (Ax<o>-19 0))) (=> (and (distinct 0 1) true) (= (Ax<o>-20 1) (Ax<o>-19 1))))))
  996. (let (($x3414 (and $x3410 (=> (and (distinct 0 2) true) (= (Ax<o>-20 2) (Ax<o>-19 2))))))
  997. (and $x3414 (=> (and (distinct 0 3) true) (= (Ax<o>-20 3) (Ax<o>-19 3)))))))
  998. (assert
  999. (let (($x3425 (and (=> (and (distinct 0 0) true) (= (Ax<r>-20 0) (Ax<r>-19 0))) (=> (and (distinct 0 1) true) (= (Ax<r>-20 1) (Ax<r>-19 1))))))
  1000. (let (($x3429 (and $x3425 (=> (and (distinct 0 2) true) (= (Ax<r>-20 2) (Ax<r>-19 2))))))
  1001. (and $x3429 (=> (and (distinct 0 3) true) (= (Ax<r>-20 3) (Ax<r>-19 3)))))))
  1002. (assert
  1003. (let ((?x3402 (Ax<o>-20 0)))
  1004. (= ?x3402 (+ (Ax<o>-19 0) tmp<o>-36))))
  1005. (assert
  1006. (and true (= (Ax<r>-20 0) (+ (Ax<r>-19 0) tmp<r>-36))))
  1007. (assert
  1008. (let (($x3445 (and (=> (and (distinct 1 0) true) (= (Ax<o>-21 0) (Ax<o>-20 0))) (=> (and (distinct 1 1) true) (= (Ax<o>-21 1) (Ax<o>-20 1))))))
  1009. (let (($x3449 (and $x3445 (=> (and (distinct 1 2) true) (= (Ax<o>-21 2) (Ax<o>-20 2))))))
  1010. (and $x3449 (=> (and (distinct 1 3) true) (= (Ax<o>-21 3) (Ax<o>-20 3)))))))
  1011. (assert
  1012. (let (($x3460 (and (=> (and (distinct 1 0) true) (= (Ax<r>-21 0) (Ax<r>-20 0))) (=> (and (distinct 1 1) true) (= (Ax<r>-21 1) (Ax<r>-20 1))))))
  1013. (let (($x3464 (and $x3460 (=> (and (distinct 1 2) true) (= (Ax<r>-21 2) (Ax<r>-20 2))))))
  1014. (and $x3464 (=> (and (distinct 1 3) true) (= (Ax<r>-21 3) (Ax<r>-20 3)))))))
  1015. (assert
  1016. (let ((?x2905 (x<o>-4 0)))
  1017. (let ((?x51 (A<o>-0 1 0)))
  1018. (let ((?x3438 (* ?x51 ?x2905)))
  1019. (let ((?x3442 (Ax<o>-21 1)))
  1020. (= ?x3442 ?x3438))))))
  1021. (assert
  1022. (and true (= (Ax<r>-21 1) (* (A<r>-0 1 0) (x<r>-4 0)))))
  1023. (assert
  1024. (let ((?x2910 (x<o>-4 1)))
  1025. (let ((?x55 (A<o>-0 1 1)))
  1026. (let ((?x3473 (* ?x55 ?x2910)))
  1027. (= tmp<o>-37 ?x3473)))))
  1028. (assert
  1029. (and true (= tmp<r>-37 (* (A<r>-0 1 1) (x<r>-4 1)))))
  1030. (assert
  1031. (let (($x3487 (and (=> (and (distinct 1 0) true) (= (Ax<o>-22 0) (Ax<o>-21 0))) (=> (and (distinct 1 1) true) (= (Ax<o>-22 1) (Ax<o>-21 1))))))
  1032. (let (($x3491 (and $x3487 (=> (and (distinct 1 2) true) (= (Ax<o>-22 2) (Ax<o>-21 2))))))
  1033. (and $x3491 (=> (and (distinct 1 3) true) (= (Ax<o>-22 3) (Ax<o>-21 3)))))))
  1034. (assert
  1035. (let (($x3502 (and (=> (and (distinct 1 0) true) (= (Ax<r>-22 0) (Ax<r>-21 0))) (=> (and (distinct 1 1) true) (= (Ax<r>-22 1) (Ax<r>-21 1))))))
  1036. (let (($x3506 (and $x3502 (=> (and (distinct 1 2) true) (= (Ax<r>-22 2) (Ax<r>-21 2))))))
  1037. (and $x3506 (=> (and (distinct 1 3) true) (= (Ax<r>-22 3) (Ax<r>-21 3)))))))
  1038. (assert
  1039. (let ((?x3484 (Ax<o>-22 1)))
  1040. (= ?x3484 (+ (Ax<o>-21 0) tmp<o>-37))))
  1041. (assert
  1042. (and true (= (Ax<r>-22 1) (+ (Ax<r>-21 0) tmp<r>-37))))
  1043. (assert
  1044. (let ((?x2914 (x<o>-4 2)))
  1045. (let ((?x59 (A<o>-0 1 2)))
  1046. (let ((?x3515 (* ?x59 ?x2914)))
  1047. (= tmp<o>-38 ?x3515)))))
  1048. (assert
  1049. (and true (= tmp<r>-38 (* (A<r>-0 1 2) (x<r>-4 2)))))
  1050. (assert
  1051. (let (($x3529 (and (=> (and (distinct 1 0) true) (= (Ax<o>-23 0) (Ax<o>-22 0))) (=> (and (distinct 1 1) true) (= (Ax<o>-23 1) (Ax<o>-22 1))))))
  1052. (let (($x3533 (and $x3529 (=> (and (distinct 1 2) true) (= (Ax<o>-23 2) (Ax<o>-22 2))))))
  1053. (and $x3533 (=> (and (distinct 1 3) true) (= (Ax<o>-23 3) (Ax<o>-22 3)))))))
  1054. (assert
  1055. (let (($x3544 (and (=> (and (distinct 1 0) true) (= (Ax<r>-23 0) (Ax<r>-22 0))) (=> (and (distinct 1 1) true) (= (Ax<r>-23 1) (Ax<r>-22 1))))))
  1056. (let (($x3548 (and $x3544 (=> (and (distinct 1 2) true) (= (Ax<r>-23 2) (Ax<r>-22 2))))))
  1057. (and $x3548 (=> (and (distinct 1 3) true) (= (Ax<r>-23 3) (Ax<r>-22 3)))))))
  1058. (assert
  1059. (let ((?x3526 (Ax<o>-23 1)))
  1060. (= ?x3526 (+ (Ax<o>-22 0) tmp<o>-38))))
  1061. (assert
  1062. (and true (= (Ax<r>-23 1) (+ (Ax<r>-22 0) tmp<r>-38))))
  1063. (assert
  1064. (let ((?x2918 (x<o>-4 3)))
  1065. (let ((?x63 (A<o>-0 1 3)))
  1066. (let ((?x3557 (* ?x63 ?x2918)))
  1067. (= tmp<o>-39 ?x3557)))))
  1068. (assert
  1069. (and true (= tmp<r>-39 (* (A<r>-0 1 3) (x<r>-4 3)))))
  1070. (assert
  1071. (let (($x3571 (and (=> (and (distinct 1 0) true) (= (Ax<o>-24 0) (Ax<o>-23 0))) (=> (and (distinct 1 1) true) (= (Ax<o>-24 1) (Ax<o>-23 1))))))
  1072. (let (($x3575 (and $x3571 (=> (and (distinct 1 2) true) (= (Ax<o>-24 2) (Ax<o>-23 2))))))
  1073. (and $x3575 (=> (and (distinct 1 3) true) (= (Ax<o>-24 3) (Ax<o>-23 3)))))))
  1074. (assert
  1075. (let (($x3586 (and (=> (and (distinct 1 0) true) (= (Ax<r>-24 0) (Ax<r>-23 0))) (=> (and (distinct 1 1) true) (= (Ax<r>-24 1) (Ax<r>-23 1))))))
  1076. (let (($x3590 (and $x3586 (=> (and (distinct 1 2) true) (= (Ax<r>-24 2) (Ax<r>-23 2))))))
  1077. (and $x3590 (=> (and (distinct 1 3) true) (= (Ax<r>-24 3) (Ax<r>-23 3)))))))
  1078. (assert
  1079. (let ((?x3568 (Ax<o>-24 1)))
  1080. (= ?x3568 (+ (Ax<o>-23 0) tmp<o>-39))))
  1081. (assert
  1082. (and true (= (Ax<r>-24 1) (+ (Ax<r>-23 0) tmp<r>-39))))
  1083. (assert
  1084. (let (($x3606 (and (=> (and (distinct 2 0) true) (= (Ax<o>-25 0) (Ax<o>-24 0))) (=> (and (distinct 2 1) true) (= (Ax<o>-25 1) (Ax<o>-24 1))))))
  1085. (let (($x3610 (and $x3606 (=> (and (distinct 2 2) true) (= (Ax<o>-25 2) (Ax<o>-24 2))))))
  1086. (and $x3610 (=> (and (distinct 2 3) true) (= (Ax<o>-25 3) (Ax<o>-24 3)))))))
  1087. (assert
  1088. (let (($x3621 (and (=> (and (distinct 2 0) true) (= (Ax<r>-25 0) (Ax<r>-24 0))) (=> (and (distinct 2 1) true) (= (Ax<r>-25 1) (Ax<r>-24 1))))))
  1089. (let (($x3625 (and $x3621 (=> (and (distinct 2 2) true) (= (Ax<r>-25 2) (Ax<r>-24 2))))))
  1090. (and $x3625 (=> (and (distinct 2 3) true) (= (Ax<r>-25 3) (Ax<r>-24 3)))))))
  1091. (assert
  1092. (let ((?x2905 (x<o>-4 0)))
  1093. (let ((?x67 (A<o>-0 2 0)))
  1094. (let ((?x3599 (* ?x67 ?x2905)))
  1095. (let ((?x3607 (Ax<o>-25 2)))
  1096. (= ?x3607 ?x3599))))))
  1097. (assert
  1098. (and true (= (Ax<r>-25 2) (* (A<r>-0 2 0) (x<r>-4 0)))))
  1099. (assert
  1100. (let ((?x2910 (x<o>-4 1)))
  1101. (let ((?x71 (A<o>-0 2 1)))
  1102. (let ((?x3634 (* ?x71 ?x2910)))
  1103. (= tmp<o>-40 ?x3634)))))
  1104. (assert
  1105. (and true (= tmp<r>-40 (* (A<r>-0 2 1) (x<r>-4 1)))))
  1106. (assert
  1107. (let (($x3648 (and (=> (and (distinct 2 0) true) (= (Ax<o>-26 0) (Ax<o>-25 0))) (=> (and (distinct 2 1) true) (= (Ax<o>-26 1) (Ax<o>-25 1))))))
  1108. (let (($x3652 (and $x3648 (=> (and (distinct 2 2) true) (= (Ax<o>-26 2) (Ax<o>-25 2))))))
  1109. (and $x3652 (=> (and (distinct 2 3) true) (= (Ax<o>-26 3) (Ax<o>-25 3)))))))
  1110. (assert
  1111. (let (($x3663 (and (=> (and (distinct 2 0) true) (= (Ax<r>-26 0) (Ax<r>-25 0))) (=> (and (distinct 2 1) true) (= (Ax<r>-26 1) (Ax<r>-25 1))))))
  1112. (let (($x3667 (and $x3663 (=> (and (distinct 2 2) true) (= (Ax<r>-26 2) (Ax<r>-25 2))))))
  1113. (and $x3667 (=> (and (distinct 2 3) true) (= (Ax<r>-26 3) (Ax<r>-25 3)))))))
  1114. (assert
  1115. (let ((?x3649 (Ax<o>-26 2)))
  1116. (= ?x3649 (+ (Ax<o>-25 0) tmp<o>-40))))
  1117. (assert
  1118. (and true (= (Ax<r>-26 2) (+ (Ax<r>-25 0) tmp<r>-40))))
  1119. (assert
  1120. (let ((?x2914 (x<o>-4 2)))
  1121. (let ((?x75 (A<o>-0 2 2)))
  1122. (let ((?x3676 (* ?x75 ?x2914)))
  1123. (= tmp<o>-41 ?x3676)))))
  1124. (assert
  1125. (and true (= tmp<r>-41 (* (A<r>-0 2 2) (x<r>-4 2)))))
  1126. (assert
  1127. (let (($x3690 (and (=> (and (distinct 2 0) true) (= (Ax<o>-27 0) (Ax<o>-26 0))) (=> (and (distinct 2 1) true) (= (Ax<o>-27 1) (Ax<o>-26 1))))))
  1128. (let (($x3694 (and $x3690 (=> (and (distinct 2 2) true) (= (Ax<o>-27 2) (Ax<o>-26 2))))))
  1129. (and $x3694 (=> (and (distinct 2 3) true) (= (Ax<o>-27 3) (Ax<o>-26 3)))))))
  1130. (assert
  1131. (let (($x3705 (and (=> (and (distinct 2 0) true) (= (Ax<r>-27 0) (Ax<r>-26 0))) (=> (and (distinct 2 1) true) (= (Ax<r>-27 1) (Ax<r>-26 1))))))
  1132. (let (($x3709 (and $x3705 (=> (and (distinct 2 2) true) (= (Ax<r>-27 2) (Ax<r>-26 2))))))
  1133. (and $x3709 (=> (and (distinct 2 3) true) (= (Ax<r>-27 3) (Ax<r>-26 3)))))))
  1134. (assert
  1135. (let ((?x3691 (Ax<o>-27 2)))
  1136. (= ?x3691 (+ (Ax<o>-26 0) tmp<o>-41))))
  1137. (assert
  1138. (and true (= (Ax<r>-27 2) (+ (Ax<r>-26 0) tmp<r>-41))))
  1139. (assert
  1140. (let ((?x2918 (x<o>-4 3)))
  1141. (let ((?x79 (A<o>-0 2 3)))
  1142. (let ((?x3718 (* ?x79 ?x2918)))
  1143. (= tmp<o>-42 ?x3718)))))
  1144. (assert
  1145. (and true (= tmp<r>-42 (* (A<r>-0 2 3) (x<r>-4 3)))))
  1146. (assert
  1147. (let (($x3732 (and (=> (and (distinct 2 0) true) (= (Ax<o>-28 0) (Ax<o>-27 0))) (=> (and (distinct 2 1) true) (= (Ax<o>-28 1) (Ax<o>-27 1))))))
  1148. (let (($x3736 (and $x3732 (=> (and (distinct 2 2) true) (= (Ax<o>-28 2) (Ax<o>-27 2))))))
  1149. (and $x3736 (=> (and (distinct 2 3) true) (= (Ax<o>-28 3) (Ax<o>-27 3)))))))
  1150. (assert
  1151. (let (($x3747 (and (=> (and (distinct 2 0) true) (= (Ax<r>-28 0) (Ax<r>-27 0))) (=> (and (distinct 2 1) true) (= (Ax<r>-28 1) (Ax<r>-27 1))))))
  1152. (let (($x3751 (and $x3747 (=> (and (distinct 2 2) true) (= (Ax<r>-28 2) (Ax<r>-27 2))))))
  1153. (and $x3751 (=> (and (distinct 2 3) true) (= (Ax<r>-28 3) (Ax<r>-27 3)))))))
  1154. (assert
  1155. (let ((?x3733 (Ax<o>-28 2)))
  1156. (= ?x3733 (+ (Ax<o>-27 0) tmp<o>-42))))
  1157. (assert
  1158. (and true (= (Ax<r>-28 2) (+ (Ax<r>-27 0) tmp<r>-42))))
  1159. (assert
  1160. (let (($x3767 (and (=> (and (distinct 3 0) true) (= (Ax<o>-29 0) (Ax<o>-28 0))) (=> (and (distinct 3 1) true) (= (Ax<o>-29 1) (Ax<o>-28 1))))))
  1161. (let (($x3771 (and $x3767 (=> (and (distinct 3 2) true) (= (Ax<o>-29 2) (Ax<o>-28 2))))))
  1162. (and $x3771 (=> (and (distinct 3 3) true) (= (Ax<o>-29 3) (Ax<o>-28 3)))))))
  1163. (assert
  1164. (let (($x3782 (and (=> (and (distinct 3 0) true) (= (Ax<r>-29 0) (Ax<r>-28 0))) (=> (and (distinct 3 1) true) (= (Ax<r>-29 1) (Ax<r>-28 1))))))
  1165. (let (($x3786 (and $x3782 (=> (and (distinct 3 2) true) (= (Ax<r>-29 2) (Ax<r>-28 2))))))
  1166. (and $x3786 (=> (and (distinct 3 3) true) (= (Ax<r>-29 3) (Ax<r>-28 3)))))))
  1167. (assert
  1168. (let ((?x2905 (x<o>-4 0)))
  1169. (let ((?x83 (A<o>-0 3 0)))
  1170. (let ((?x3760 (* ?x83 ?x2905)))
  1171. (let ((?x3772 (Ax<o>-29 3)))
  1172. (= ?x3772 ?x3760))))))
  1173. (assert
  1174. (and true (= (Ax<r>-29 3) (* (A<r>-0 3 0) (x<r>-4 0)))))
  1175. (assert
  1176. (let ((?x2910 (x<o>-4 1)))
  1177. (let ((?x87 (A<o>-0 3 1)))
  1178. (let ((?x3795 (* ?x87 ?x2910)))
  1179. (= tmp<o>-43 ?x3795)))))
  1180. (assert
  1181. (and true (= tmp<r>-43 (* (A<r>-0 3 1) (x<r>-4 1)))))
  1182. (assert
  1183. (let (($x3809 (and (=> (and (distinct 3 0) true) (= (Ax<o>-30 0) (Ax<o>-29 0))) (=> (and (distinct 3 1) true) (= (Ax<o>-30 1) (Ax<o>-29 1))))))
  1184. (let (($x3813 (and $x3809 (=> (and (distinct 3 2) true) (= (Ax<o>-30 2) (Ax<o>-29 2))))))
  1185. (and $x3813 (=> (and (distinct 3 3) true) (= (Ax<o>-30 3) (Ax<o>-29 3)))))))
  1186. (assert
  1187. (let (($x3824 (and (=> (and (distinct 3 0) true) (= (Ax<r>-30 0) (Ax<r>-29 0))) (=> (and (distinct 3 1) true) (= (Ax<r>-30 1) (Ax<r>-29 1))))))
  1188. (let (($x3828 (and $x3824 (=> (and (distinct 3 2) true) (= (Ax<r>-30 2) (Ax<r>-29 2))))))
  1189. (and $x3828 (=> (and (distinct 3 3) true) (= (Ax<r>-30 3) (Ax<r>-29 3)))))))
  1190. (assert
  1191. (let ((?x3814 (Ax<o>-30 3)))
  1192. (= ?x3814 (+ (Ax<o>-29 0) tmp<o>-43))))
  1193. (assert
  1194. (and true (= (Ax<r>-30 3) (+ (Ax<r>-29 0) tmp<r>-43))))
  1195. (assert
  1196. (let ((?x2914 (x<o>-4 2)))
  1197. (let ((?x91 (A<o>-0 3 2)))
  1198. (let ((?x3837 (* ?x91 ?x2914)))
  1199. (= tmp<o>-44 ?x3837)))))
  1200. (assert
  1201. (and true (= tmp<r>-44 (* (A<r>-0 3 2) (x<r>-4 2)))))
  1202. (assert
  1203. (let (($x3851 (and (=> (and (distinct 3 0) true) (= (Ax<o>-31 0) (Ax<o>-30 0))) (=> (and (distinct 3 1) true) (= (Ax<o>-31 1) (Ax<o>-30 1))))))
  1204. (let (($x3855 (and $x3851 (=> (and (distinct 3 2) true) (= (Ax<o>-31 2) (Ax<o>-30 2))))))
  1205. (and $x3855 (=> (and (distinct 3 3) true) (= (Ax<o>-31 3) (Ax<o>-30 3)))))))
  1206. (assert
  1207. (let (($x3866 (and (=> (and (distinct 3 0) true) (= (Ax<r>-31 0) (Ax<r>-30 0))) (=> (and (distinct 3 1) true) (= (Ax<r>-31 1) (Ax<r>-30 1))))))
  1208. (let (($x3870 (and $x3866 (=> (and (distinct 3 2) true) (= (Ax<r>-31 2) (Ax<r>-30 2))))))
  1209. (and $x3870 (=> (and (distinct 3 3) true) (= (Ax<r>-31 3) (Ax<r>-30 3)))))))
  1210. (assert
  1211. (let ((?x3856 (Ax<o>-31 3)))
  1212. (= ?x3856 (+ (Ax<o>-30 0) tmp<o>-44))))
  1213. (assert
  1214. (and true (= (Ax<r>-31 3) (+ (Ax<r>-30 0) tmp<r>-44))))
  1215. (assert
  1216. (let ((?x2918 (x<o>-4 3)))
  1217. (let ((?x95 (A<o>-0 3 3)))
  1218. (let ((?x3879 (* ?x95 ?x2918)))
  1219. (= tmp<o>-45 ?x3879)))))
  1220. (assert
  1221. (and true (= tmp<r>-45 (* (A<r>-0 3 3) (x<r>-4 3)))))
  1222. (assert
  1223. (let (($x3893 (and (=> (and (distinct 3 0) true) (= (Ax<o>-32 0) (Ax<o>-31 0))) (=> (and (distinct 3 1) true) (= (Ax<o>-32 1) (Ax<o>-31 1))))))
  1224. (let (($x3897 (and $x3893 (=> (and (distinct 3 2) true) (= (Ax<o>-32 2) (Ax<o>-31 2))))))
  1225. (and $x3897 (=> (and (distinct 3 3) true) (= (Ax<o>-32 3) (Ax<o>-31 3)))))))
  1226. (assert
  1227. (let (($x3908 (and (=> (and (distinct 3 0) true) (= (Ax<r>-32 0) (Ax<r>-31 0))) (=> (and (distinct 3 1) true) (= (Ax<r>-32 1) (Ax<r>-31 1))))))
  1228. (let (($x3912 (and $x3908 (=> (and (distinct 3 2) true) (= (Ax<r>-32 2) (Ax<r>-31 2))))))
  1229. (and $x3912 (=> (and (distinct 3 3) true) (= (Ax<r>-32 3) (Ax<r>-31 3)))))))
  1230. (assert
  1231. (let ((?x3898 (Ax<o>-32 3)))
  1232. (= ?x3898 (+ (Ax<o>-31 0) tmp<o>-45))))
  1233. (assert
  1234. (and true (= (Ax<r>-32 3) (+ (Ax<r>-31 0) tmp<r>-45))))
  1235. (assert
  1236. (let (($x3928 (and (=> (and (distinct 0 0) true) (= (bmAx<o>-1 0) (bmAx<o>-0 0))) (=> (and (distinct 0 1) true) (= (bmAx<o>-1 1) (bmAx<o>-0 1))))))
  1237. (let (($x3932 (and $x3928 (=> (and (distinct 0 2) true) (= (bmAx<o>-1 2) (bmAx<o>-0 2))))))
  1238. (and $x3932 (=> (and (distinct 0 3) true) (= (bmAx<o>-1 3) (bmAx<o>-0 3)))))))
  1239. (assert
  1240. (let (($x3943 (and (=> (and (distinct 0 0) true) (= (bmAx<r>-1 0) (bmAx<r>-0 0))) (=> (and (distinct 0 1) true) (= (bmAx<r>-1 1) (bmAx<r>-0 1))))))
  1241. (let (($x3947 (and $x3943 (=> (and (distinct 0 2) true) (= (bmAx<r>-1 2) (bmAx<r>-0 2))))))
  1242. (and $x3947 (=> (and (distinct 0 3) true) (= (bmAx<r>-1 3) (bmAx<r>-0 3)))))))
  1243. (assert
  1244. (let ((?x3920 (bmAx<o>-1 0)))
  1245. (= ?x3920 (- (b<o>-0 0) (Ax<o>-32 0)))))
  1246. (assert
  1247. (and true (= (bmAx<r>-1 0) (- (b<r>-0 0) (Ax<r>-32 0)))))
  1248. (assert
  1249. (let (($x3963 (and (=> (and (distinct 1 0) true) (= (bmAx<o>-2 0) (bmAx<o>-1 0))) (=> (and (distinct 1 1) true) (= (bmAx<o>-2 1) (bmAx<o>-1 1))))))
  1250. (let (($x3967 (and $x3963 (=> (and (distinct 1 2) true) (= (bmAx<o>-2 2) (bmAx<o>-1 2))))))
  1251. (and $x3967 (=> (and (distinct 1 3) true) (= (bmAx<o>-2 3) (bmAx<o>-1 3)))))))
  1252. (assert
  1253. (let (($x3978 (and (=> (and (distinct 1 0) true) (= (bmAx<r>-2 0) (bmAx<r>-1 0))) (=> (and (distinct 1 1) true) (= (bmAx<r>-2 1) (bmAx<r>-1 1))))))
  1254. (let (($x3982 (and $x3978 (=> (and (distinct 1 2) true) (= (bmAx<r>-2 2) (bmAx<r>-1 2))))))
  1255. (and $x3982 (=> (and (distinct 1 3) true) (= (bmAx<r>-2 3) (bmAx<r>-1 3)))))))
  1256. (assert
  1257. (let ((?x3960 (bmAx<o>-2 1)))
  1258. (= ?x3960 (- (b<o>-0 1) (Ax<o>-32 1)))))
  1259. (assert
  1260. (and true (= (bmAx<r>-2 1) (- (b<r>-0 1) (Ax<r>-32 1)))))
  1261. (assert
  1262. (let (($x3998 (and (=> (and (distinct 2 0) true) (= (bmAx<o>-3 0) (bmAx<o>-2 0))) (=> (and (distinct 2 1) true) (= (bmAx<o>-3 1) (bmAx<o>-2 1))))))
  1263. (let (($x4002 (and $x3998 (=> (and (distinct 2 2) true) (= (bmAx<o>-3 2) (bmAx<o>-2 2))))))
  1264. (and $x4002 (=> (and (distinct 2 3) true) (= (bmAx<o>-3 3) (bmAx<o>-2 3)))))))
  1265. (assert
  1266. (let (($x4013 (and (=> (and (distinct 2 0) true) (= (bmAx<r>-3 0) (bmAx<r>-2 0))) (=> (and (distinct 2 1) true) (= (bmAx<r>-3 1) (bmAx<r>-2 1))))))
  1267. (let (($x4017 (and $x4013 (=> (and (distinct 2 2) true) (= (bmAx<r>-3 2) (bmAx<r>-2 2))))))
  1268. (and $x4017 (=> (and (distinct 2 3) true) (= (bmAx<r>-3 3) (bmAx<r>-2 3)))))))
  1269. (assert
  1270. (let ((?x3999 (bmAx<o>-3 2)))
  1271. (= ?x3999 (- (b<o>-0 2) (Ax<o>-32 2)))))
  1272. (assert
  1273. (and true (= (bmAx<r>-3 2) (- (b<r>-0 2) (Ax<r>-32 2)))))
  1274. (assert
  1275. (let (($x4033 (and (=> (and (distinct 3 0) true) (= (bmAx<o>-4 0) (bmAx<o>-3 0))) (=> (and (distinct 3 1) true) (= (bmAx<o>-4 1) (bmAx<o>-3 1))))))
  1276. (let (($x4037 (and $x4033 (=> (and (distinct 3 2) true) (= (bmAx<o>-4 2) (bmAx<o>-3 2))))))
  1277. (and $x4037 (=> (and (distinct 3 3) true) (= (bmAx<o>-4 3) (bmAx<o>-3 3)))))))
  1278. (assert
  1279. (let (($x4048 (and (=> (and (distinct 3 0) true) (= (bmAx<r>-4 0) (bmAx<r>-3 0))) (=> (and (distinct 3 1) true) (= (bmAx<r>-4 1) (bmAx<r>-3 1))))))
  1280. (let (($x4052 (and $x4048 (=> (and (distinct 3 2) true) (= (bmAx<r>-4 2) (bmAx<r>-3 2))))))
  1281. (and $x4052 (=> (and (distinct 3 3) true) (= (bmAx<r>-4 3) (bmAx<r>-3 3)))))))
  1282. (assert
  1283. (let ((?x4038 (bmAx<o>-4 3)))
  1284. (= ?x4038 (- (b<o>-0 3) (Ax<o>-32 3)))))
  1285. (assert
  1286. (and true (= (bmAx<r>-4 3) (- (b<r>-0 3) (Ax<r>-32 3)))))
  1287. (assert
  1288. (let ((?x4053 (bmAx<r>-4 3)))
  1289. (let ((?x3213 (r<r>-8 3)))
  1290. (let (($x4093 (= ?x3213 ?x4053)))
  1291. (let ((?x4049 (bmAx<r>-4 2)))
  1292. (let ((?x3209 (r<r>-8 2)))
  1293. (let (($x4091 (= ?x3209 ?x4049)))
  1294. (let ((?x4045 (bmAx<r>-4 1)))
  1295. (let ((?x3205 (r<r>-8 1)))
  1296. (let (($x4089 (= ?x3205 ?x4045)))
  1297. (let ((?x4042 (bmAx<r>-4 0)))
  1298. (let ((?x3202 (r<r>-8 0)))
  1299. (let (($x4088 (= ?x3202 ?x4042)))
  1300. (let (($x4094 (and (and (and $x4088 $x4089) $x4091) $x4093)))
  1301. (let ((?x4038 (bmAx<o>-4 3)))
  1302. (let ((?x3198 (r<o>-8 3)))
  1303. (let (($x4086 (= ?x3198 ?x4038)))
  1304. (let ((?x4034 (bmAx<o>-4 2)))
  1305. (let ((?x3194 (r<o>-8 2)))
  1306. (let (($x4084 (= ?x3194 ?x4034)))
  1307. (let ((?x4030 (bmAx<o>-4 1)))
  1308. (let ((?x3190 (r<o>-8 1)))
  1309. (let (($x4082 (= ?x3190 ?x4030)))
  1310. (let ((?x4025 (bmAx<o>-4 0)))
  1311. (let ((?x3185 (r<o>-8 0)))
  1312. (let (($x4081 (= ?x3185 ?x4025)))
  1313. (let (($x4087 (and (and (and $x4081 $x4082) $x4084) $x4086)))
  1314. (let (($x4079 (= i<o>-2 i<r>-2)))
  1315. (let (($x4077 (= r_norm<o>-8 r_norm<r>-8)))
  1316. (let ((?x111 (b<r>-0 3)))
  1317. (let ((?x110 (b<o>-0 3)))
  1318. (let (($x112 (= ?x110 ?x111)))
  1319. (let ((?x107 (b<r>-0 2)))
  1320. (let ((?x106 (b<o>-0 2)))
  1321. (let (($x108 (= ?x106 ?x107)))
  1322. (let ((?x103 (b<r>-0 1)))
  1323. (let ((?x102 (b<o>-0 1)))
  1324. (let (($x104 (= ?x102 ?x103)))
  1325. (let ((?x100 (b<r>-0 0)))
  1326. (let ((?x99 (b<o>-0 0)))
  1327. (let (($x101 (= ?x99 ?x100)))
  1328. (let (($x113 (and (and (and $x101 $x104) $x108) $x112)))
  1329. (let ((?x2933 (x<r>-4 3)))
  1330. (let ((?x2918 (x<o>-4 3)))
  1331. (let (($x4073 (= ?x2918 ?x2933)))
  1332. (let ((?x2929 (x<r>-4 2)))
  1333. (let ((?x2914 (x<o>-4 2)))
  1334. (let (($x4071 (= ?x2914 ?x2929)))
  1335. (let ((?x2925 (x<r>-4 1)))
  1336. (let ((?x2910 (x<o>-4 1)))
  1337. (let (($x4069 (= ?x2910 ?x2925)))
  1338. (let ((?x2922 (x<r>-4 0)))
  1339. (let ((?x2905 (x<o>-4 0)))
  1340. (let (($x4068 (= ?x2905 ?x2922)))
  1341. (let (($x4065 (= ?x3198 ?x3213)))
  1342. (let ((?x96 (A<r>-0 3 3)))
  1343. (let ((?x95 (A<o>-0 3 3)))
  1344. (let (($x97 (= ?x95 ?x96)))
  1345. (let ((?x92 (A<r>-0 3 2)))
  1346. (let ((?x91 (A<o>-0 3 2)))
  1347. (let (($x93 (= ?x91 ?x92)))
  1348. (let ((?x88 (A<r>-0 3 1)))
  1349. (let ((?x87 (A<o>-0 3 1)))
  1350. (let (($x89 (= ?x87 ?x88)))
  1351. (let ((?x84 (A<r>-0 3 0)))
  1352. (let ((?x83 (A<o>-0 3 0)))
  1353. (let (($x85 (= ?x83 ?x84)))
  1354. (let ((?x80 (A<r>-0 2 3)))
  1355. (let ((?x79 (A<o>-0 2 3)))
  1356. (let (($x81 (= ?x79 ?x80)))
  1357. (let ((?x76 (A<r>-0 2 2)))
  1358. (let ((?x75 (A<o>-0 2 2)))
  1359. (let (($x77 (= ?x75 ?x76)))
  1360. (let ((?x72 (A<r>-0 2 1)))
  1361. (let ((?x71 (A<o>-0 2 1)))
  1362. (let (($x73 (= ?x71 ?x72)))
  1363. (let ((?x68 (A<r>-0 2 0)))
  1364. (let ((?x67 (A<o>-0 2 0)))
  1365. (let (($x69 (= ?x67 ?x68)))
  1366. (let ((?x64 (A<r>-0 1 3)))
  1367. (let ((?x63 (A<o>-0 1 3)))
  1368. (let (($x65 (= ?x63 ?x64)))
  1369. (let ((?x60 (A<r>-0 1 2)))
  1370. (let ((?x59 (A<o>-0 1 2)))
  1371. (let (($x61 (= ?x59 ?x60)))
  1372. (let ((?x56 (A<r>-0 1 1)))
  1373. (let ((?x55 (A<o>-0 1 1)))
  1374. (let (($x57 (= ?x55 ?x56)))
  1375. (let ((?x52 (A<r>-0 1 0)))
  1376. (let ((?x51 (A<o>-0 1 0)))
  1377. (let (($x53 (= ?x51 ?x52)))
  1378. (let ((?x48 (A<r>-0 0 3)))
  1379. (let ((?x47 (A<o>-0 0 3)))
  1380. (let (($x49 (= ?x47 ?x48)))
  1381. (let ((?x43 (A<r>-0 0 2)))
  1382. (let ((?x42 (A<o>-0 0 2)))
  1383. (let (($x44 (= ?x42 ?x43)))
  1384. (let ((?x38 (A<r>-0 0 1)))
  1385. (let ((?x37 (A<o>-0 0 1)))
  1386. (let (($x39 (= ?x37 ?x38)))
  1387. (let ((?x35 (A<r>-0 0 0)))
  1388. (let ((?x34 (A<o>-0 0 0)))
  1389. (let (($x36 (= ?x34 ?x35)))
  1390. (let (($x62 (and (and (and (and (and (and $x36 $x39) $x44) $x49) $x53) $x57) $x61)))
  1391. (let (($x86 (and (and (and (and (and (and $x62 $x65) $x69) $x73) $x77) $x81) $x85)))
  1392. (let (($x98 (and (and (and $x86 $x89) $x93) $x97)))
  1393. (let (($x4067 (and $x98 (and (and (and (= ?x3185 ?x3202) (= ?x3190 ?x3205)) (= ?x3194 ?x3209)) $x4065))))
  1394. (let (($x4078 (and (and (and $x4067 (and (and (and $x4068 $x4069) $x4071) $x4073)) $x113) $x4077)))
  1395. (let (($x4080 (and $x4078 $x4079)))
  1396. (not (and $x4080 (=> $x4087 $x4094))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  1397. (check-sat)
Add Comment
Please, Sign In to add comment
Public Pastes
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!