API tools faq
paste
Guest User

operator<<() constraints

a guest
Jan 25th, 2017
141
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 44.09 KB | None | 0 0
raw download clone embed print report
  1. (declare-fun bmAx<r>-0 (Int) Real)
  2. (declare-fun r<r>-4 (Int) Real)
  3. (declare-fun bmAx<o>-0 (Int) Real)
  4. (declare-fun r<o>-4 (Int) Real)
  5. (declare-fun i<r>-1 () Int)
  6. (declare-fun i<o>-1 () Int)
  7. (declare-fun r_norm<r>-4 () Real)
  8. (declare-fun r_norm<o>-4 () Real)
  9. (declare-fun b<r>-0 (Int) Real)
  10. (declare-fun b<o>-0 (Int) Real)
  11. (declare-fun x<r>-0 (Int) Real)
  12. (declare-fun x<o>-0 (Int) Real)
  13. (declare-fun A<r>-0 (Int Int) Real)
  14. (declare-fun A<o>-0 (Int Int) Real)
  15. (declare-fun iters<r>-0 () Int)
  16. (declare-fun iters<o>-0 () Int)
  17. (declare-fun q<o>-0 (Int) Real)
  18. (declare-fun q<o>-1 (Int) Real)
  19. (declare-fun q<r>-0 (Int) Real)
  20. (declare-fun q<r>-1 (Int) Real)
  21. (declare-fun tmp<o>-16 () Real)
  22. (declare-fun tmp<r>-16 () Real)
  23. (declare-fun q<o>-2 (Int) Real)
  24. (declare-fun q<r>-2 (Int) Real)
  25. (declare-fun tmp<o>-17 () Real)
  26. (declare-fun tmp<r>-17 () Real)
  27. (declare-fun q<o>-3 (Int) Real)
  28. (declare-fun q<r>-3 (Int) Real)
  29. (declare-fun tmp<o>-18 () Real)
  30. (declare-fun tmp<r>-18 () Real)
  31. (declare-fun q<o>-4 (Int) Real)
  32. (declare-fun q<r>-4 (Int) Real)
  33. (declare-fun q<o>-5 (Int) Real)
  34. (declare-fun q<r>-5 (Int) Real)
  35. (declare-fun tmp<o>-19 () Real)
  36. (declare-fun tmp<r>-19 () Real)
  37. (declare-fun q<o>-6 (Int) Real)
  38. (declare-fun q<r>-6 (Int) Real)
  39. (declare-fun tmp<o>-20 () Real)
  40. (declare-fun tmp<r>-20 () Real)
  41. (declare-fun q<o>-7 (Int) Real)
  42. (declare-fun q<r>-7 (Int) Real)
  43. (declare-fun tmp<o>-21 () Real)
  44. (declare-fun tmp<r>-21 () Real)
  45. (declare-fun q<o>-8 (Int) Real)
  46. (declare-fun q<r>-8 (Int) Real)
  47. (declare-fun q<o>-9 (Int) Real)
  48. (declare-fun q<r>-9 (Int) Real)
  49. (declare-fun tmp<o>-22 () Real)
  50. (declare-fun tmp<r>-22 () Real)
  51. (declare-fun q<o>-10 (Int) Real)
  52. (declare-fun q<r>-10 (Int) Real)
  53. (declare-fun tmp<o>-23 () Real)
  54. (declare-fun tmp<r>-23 () Real)
  55. (declare-fun q<o>-11 (Int) Real)
  56. (declare-fun q<r>-11 (Int) Real)
  57. (declare-fun tmp<o>-24 () Real)
  58. (declare-fun tmp<r>-24 () Real)
  59. (declare-fun q<o>-12 (Int) Real)
  60. (declare-fun q<r>-12 (Int) Real)
  61. (declare-fun q<o>-13 (Int) Real)
  62. (declare-fun q<r>-13 (Int) Real)
  63. (declare-fun tmp<o>-25 () Real)
  64. (declare-fun tmp<r>-25 () Real)
  65. (declare-fun q<o>-14 (Int) Real)
  66. (declare-fun q<r>-14 (Int) Real)
  67. (declare-fun tmp<o>-26 () Real)
  68. (declare-fun tmp<r>-26 () Real)
  69. (declare-fun q<o>-15 (Int) Real)
  70. (declare-fun q<r>-15 (Int) Real)
  71. (declare-fun tmp<o>-27 () Real)
  72. (declare-fun tmp<r>-27 () Real)
  73. (declare-fun q<o>-16 (Int) Real)
  74. (declare-fun q<r>-16 (Int) Real)
  75. (declare-fun rtq<o>-1 () Real)
  76. (declare-fun rtq<r>-1 () Real)
  77. (declare-fun tmp<o>-28 () Real)
  78. (declare-fun tmp<r>-28 () Real)
  79. (declare-fun rtq<o>-2 () Real)
  80. (declare-fun rtq<r>-2 () Real)
  81. (declare-fun tmp<o>-29 () Real)
  82. (declare-fun tmp<r>-29 () Real)
  83. (declare-fun rtq<o>-3 () Real)
  84. (declare-fun rtq<r>-3 () Real)
  85. (declare-fun tmp<o>-30 () Real)
  86. (declare-fun tmp<r>-30 () Real)
  87. (declare-fun rtq<o>-4 () Real)
  88. (declare-fun rtq<r>-4 () Real)
  89. (declare-fun alpha<o>-1 () Real)
  90. (declare-fun alpha<r>-1 () Real)
  91. (declare-fun alphar<o>-0 (Int) Real)
  92. (declare-fun alphar<o>-1 (Int) Real)
  93. (declare-fun alphar<r>-0 (Int) Real)
  94. (declare-fun alphar<r>-1 (Int) Real)
  95. (declare-fun alphar<o>-2 (Int) Real)
  96. (declare-fun alphar<r>-2 (Int) Real)
  97. (declare-fun alphar<o>-3 (Int) Real)
  98. (declare-fun alphar<r>-3 (Int) Real)
  99. (declare-fun alphar<o>-4 (Int) Real)
  100. (declare-fun alphar<r>-4 (Int) Real)
  101. (declare-fun x<o>-1 (Int) Real)
  102. (declare-fun x<r>-1 (Int) Real)
  103. (declare-fun x<o>-2 (Int) Real)
  104. (declare-fun x<r>-2 (Int) Real)
  105. (declare-fun x<o>-3 (Int) Real)
  106. (declare-fun x<r>-3 (Int) Real)
  107. (declare-fun x<o>-4 (Int) Real)
  108. (declare-fun x<r>-4 (Int) Real)
  109. (declare-fun alphaq<o>-0 (Int) Real)
  110. (declare-fun alphaq<o>-1 (Int) Real)
  111. (declare-fun alphaq<r>-0 (Int) Real)
  112. (declare-fun alphaq<r>-1 (Int) Real)
  113. (declare-fun alphaq<o>-2 (Int) Real)
  114. (declare-fun alphaq<r>-2 (Int) Real)
  115. (declare-fun alphaq<o>-3 (Int) Real)
  116. (declare-fun alphaq<r>-3 (Int) Real)
  117. (declare-fun alphaq<o>-4 (Int) Real)
  118. (declare-fun alphaq<r>-4 (Int) Real)
  119. (declare-fun r<o>-5 (Int) Real)
  120. (declare-fun r<r>-5 (Int) Real)
  121. (declare-fun r<o>-6 (Int) Real)
  122. (declare-fun r<r>-6 (Int) Real)
  123. (declare-fun r<o>-7 (Int) Real)
  124. (declare-fun r<r>-7 (Int) Real)
  125. (declare-fun r<o>-8 (Int) Real)
  126. (declare-fun r<r>-8 (Int) Real)
  127. (declare-fun r_norm<o>-5 () Real)
  128. (declare-fun r_norm<r>-5 () Real)
  129. (declare-fun tmp<o>-31 () Real)
  130. (declare-fun tmp<r>-31 () Real)
  131. (declare-fun r_norm<o>-6 () Real)
  132. (declare-fun r_norm<r>-6 () Real)
  133. (declare-fun tmp<o>-32 () Real)
  134. (declare-fun tmp<r>-32 () Real)
  135. (declare-fun r_norm<o>-7 () Real)
  136. (declare-fun r_norm<r>-7 () Real)
  137. (declare-fun tmp<o>-33 () Real)
  138. (declare-fun tmp<r>-33 () Real)
  139. (declare-fun r_norm<o>-8 () Real)
  140. (declare-fun r_norm<r>-8 () Real)
  141. (declare-fun i<o>-2 () Int)
  142. (declare-fun i<r>-2 () Int)
  143. (declare-fun Ax<o>-16 (Int) Real)
  144. (declare-fun Ax<o>-17 (Int) Real)
  145. (declare-fun Ax<r>-16 (Int) Real)
  146. (declare-fun Ax<r>-17 (Int) Real)
  147. (declare-fun tmp<o>-34 () Real)
  148. (declare-fun tmp<r>-34 () Real)
  149. (declare-fun Ax<o>-18 (Int) Real)
  150. (declare-fun Ax<r>-18 (Int) Real)
  151. (declare-fun tmp<o>-35 () Real)
  152. (declare-fun tmp<r>-35 () Real)
  153. (declare-fun Ax<o>-19 (Int) Real)
  154. (declare-fun Ax<r>-19 (Int) Real)
  155. (declare-fun tmp<o>-36 () Real)
  156. (declare-fun tmp<r>-36 () Real)
  157. (declare-fun Ax<o>-20 (Int) Real)
  158. (declare-fun Ax<r>-20 (Int) Real)
  159. (declare-fun Ax<o>-21 (Int) Real)
  160. (declare-fun Ax<r>-21 (Int) Real)
  161. (declare-fun tmp<o>-37 () Real)
  162. (declare-fun tmp<r>-37 () Real)
  163. (declare-fun Ax<o>-22 (Int) Real)
  164. (declare-fun Ax<r>-22 (Int) Real)
  165. (declare-fun tmp<o>-38 () Real)
  166. (declare-fun tmp<r>-38 () Real)
  167. (declare-fun Ax<o>-23 (Int) Real)
  168. (declare-fun Ax<r>-23 (Int) Real)
  169. (declare-fun tmp<o>-39 () Real)
  170. (declare-fun tmp<r>-39 () Real)
  171. (declare-fun Ax<o>-24 (Int) Real)
  172. (declare-fun Ax<r>-24 (Int) Real)
  173. (declare-fun Ax<o>-25 (Int) Real)
  174. (declare-fun Ax<r>-25 (Int) Real)
  175. (declare-fun tmp<o>-40 () Real)
  176. (declare-fun tmp<r>-40 () Real)
  177. (declare-fun Ax<o>-26 (Int) Real)
  178. (declare-fun Ax<r>-26 (Int) Real)
  179. (declare-fun tmp<o>-41 () Real)
  180. (declare-fun tmp<r>-41 () Real)
  181. (declare-fun Ax<o>-27 (Int) Real)
  182. (declare-fun Ax<r>-27 (Int) Real)
  183. (declare-fun tmp<o>-42 () Real)
  184. (declare-fun tmp<r>-42 () Real)
  185. (declare-fun Ax<o>-28 (Int) Real)
  186. (declare-fun Ax<r>-28 (Int) Real)
  187. (declare-fun Ax<o>-29 (Int) Real)
  188. (declare-fun Ax<r>-29 (Int) Real)
  189. (declare-fun tmp<o>-43 () Real)
  190. (declare-fun tmp<r>-43 () Real)
  191. (declare-fun Ax<o>-30 (Int) Real)
  192. (declare-fun Ax<r>-30 (Int) Real)
  193. (declare-fun tmp<o>-44 () Real)
  194. (declare-fun tmp<r>-44 () Real)
  195. (declare-fun Ax<o>-31 (Int) Real)
  196. (declare-fun Ax<r>-31 (Int) Real)
  197. (declare-fun tmp<o>-45 () Real)
  198. (declare-fun tmp<r>-45 () Real)
  199. (declare-fun Ax<o>-32 (Int) Real)
  200. (declare-fun Ax<r>-32 (Int) Real)
  201. (declare-fun bmAx<o>-1 (Int) Real)
  202. (declare-fun bmAx<r>-1 (Int) Real)
  203. (declare-fun bmAx<o>-2 (Int) Real)
  204. (declare-fun bmAx<r>-2 (Int) Real)
  205. (declare-fun bmAx<o>-3 (Int) Real)
  206. (declare-fun bmAx<r>-3 (Int) Real)
  207. (declare-fun bmAx<o>-4 (Int) Real)
  208. (declare-fun bmAx<r>-4 (Int) Real)
  209. (assert (let ((a!1 (=> (and (= (r<o>-4 0) (bmAx<o>-0 0))
  210. (= (r<o>-4 1) (bmAx<o>-0 1))
  211. (= (r<o>-4 2) (bmAx<o>-0 2))
  212. (= (r<o>-4 3) (bmAx<o>-0 3)))
  213. (and (= (r<r>-4 0) (bmAx<r>-0 0))
  214. (= (r<r>-4 1) (bmAx<r>-0 1))
  215. (= (r<r>-4 2) (bmAx<r>-0 2))
  216. (= (r<r>-4 3) (bmAx<r>-0 3))))))
  217. (and (= (A<o>-0 0 0) (A<r>-0 0 0))
  218. (= (A<o>-0 0 1) (A<r>-0 0 1))
  219. (= (A<o>-0 0 2) (A<r>-0 0 2))
  220. (= (A<o>-0 0 3) (A<r>-0 0 3))
  221. (= (A<o>-0 1 0) (A<r>-0 1 0))
  222. (= (A<o>-0 1 1) (A<r>-0 1 1))
  223. (= (A<o>-0 1 2) (A<r>-0 1 2))
  224. (= (A<o>-0 1 3) (A<r>-0 1 3))
  225. (= (A<o>-0 2 0) (A<r>-0 2 0))
  226. (= (A<o>-0 2 1) (A<r>-0 2 1))
  227. (= (A<o>-0 2 2) (A<r>-0 2 2))
  228. (= (A<o>-0 2 3) (A<r>-0 2 3))
  229. (= (A<o>-0 3 0) (A<r>-0 3 0))
  230. (= (A<o>-0 3 1) (A<r>-0 3 1))
  231. (= (A<o>-0 3 2) (A<r>-0 3 2))
  232. (= (A<o>-0 3 3) (A<r>-0 3 3))
  233. (= (r<o>-4 0) (r<r>-4 0))
  234. (= (r<o>-4 1) (r<r>-4 1))
  235. (= (r<o>-4 2) (r<r>-4 2))
  236. (= (r<o>-4 3) (r<r>-4 3))
  237. (= (x<o>-0 0) (x<r>-0 0))
  238. (= (x<o>-0 1) (x<r>-0 1))
  239. (= (x<o>-0 2) (x<r>-0 2))
  240. (= (x<o>-0 3) (x<r>-0 3))
  241. (= (b<o>-0 0) (b<r>-0 0))
  242. (= (b<o>-0 1) (b<r>-0 1))
  243. (= (b<o>-0 2) (b<r>-0 2))
  244. (= (b<o>-0 3) (b<r>-0 3))
  245. (= r_norm<o>-4 r_norm<r>-4)
  246. (= i<o>-1 i<r>-1)
  247. a!1)))
  248. (assert (and (< i<o>-1 iters<o>-0) (< i<r>-1 iters<r>-0)))
  249. (assert (and (=> (distinct 0 0) (= (q<o>-1 0) (q<o>-0 0)))
  250. (=> (distinct 0 1) (= (q<o>-1 1) (q<o>-0 1)))
  251. (=> (distinct 0 2) (= (q<o>-1 2) (q<o>-0 2)))
  252. (=> (distinct 0 3) (= (q<o>-1 3) (q<o>-0 3)))))
  253. (assert (and (=> (distinct 0 0) (= (q<r>-1 0) (q<r>-0 0)))
  254. (=> (distinct 0 1) (= (q<r>-1 1) (q<r>-0 1)))
  255. (=> (distinct 0 2) (= (q<r>-1 2) (q<r>-0 2)))
  256. (=> (distinct 0 3) (= (q<r>-1 3) (q<r>-0 3)))))
  257. (assert (= (q<o>-1 0) (* (A<o>-0 0 0) (r<o>-4 0))))
  258. (assert (and true (= (q<r>-1 0) (* (A<r>-0 0 0) (r<r>-4 0)))))
  259. (assert (= tmp<o>-16 (* (A<o>-0 0 1) (r<o>-4 1))))
  260. (assert (and true (= tmp<r>-16 (* (A<r>-0 0 1) (r<r>-4 1)))))
  261. (assert (and (=> (distinct 0 0) (= (q<o>-2 0) (q<o>-1 0)))
  262. (=> (distinct 0 1) (= (q<o>-2 1) (q<o>-1 1)))
  263. (=> (distinct 0 2) (= (q<o>-2 2) (q<o>-1 2)))
  264. (=> (distinct 0 3) (= (q<o>-2 3) (q<o>-1 3)))))
  265. (assert (and (=> (distinct 0 0) (= (q<r>-2 0) (q<r>-1 0)))
  266. (=> (distinct 0 1) (= (q<r>-2 1) (q<r>-1 1)))
  267. (=> (distinct 0 2) (= (q<r>-2 2) (q<r>-1 2)))
  268. (=> (distinct 0 3) (= (q<r>-2 3) (q<r>-1 3)))))
  269. (assert (= (q<o>-2 0) (+ (q<o>-1 0) tmp<o>-16)))
  270. (assert (and true (= (q<r>-2 0) (+ (q<r>-1 0) tmp<r>-16))))
  271. (assert (= tmp<o>-17 (* (A<o>-0 0 2) (r<o>-4 2))))
  272. (assert (and true (= tmp<r>-17 (* (A<r>-0 0 2) (r<r>-4 2)))))
  273. (assert (and (=> (distinct 0 0) (= (q<o>-3 0) (q<o>-2 0)))
  274. (=> (distinct 0 1) (= (q<o>-3 1) (q<o>-2 1)))
  275. (=> (distinct 0 2) (= (q<o>-3 2) (q<o>-2 2)))
  276. (=> (distinct 0 3) (= (q<o>-3 3) (q<o>-2 3)))))
  277. (assert (and (=> (distinct 0 0) (= (q<r>-3 0) (q<r>-2 0)))
  278. (=> (distinct 0 1) (= (q<r>-3 1) (q<r>-2 1)))
  279. (=> (distinct 0 2) (= (q<r>-3 2) (q<r>-2 2)))
  280. (=> (distinct 0 3) (= (q<r>-3 3) (q<r>-2 3)))))
  281. (assert (= (q<o>-3 0) (+ (q<o>-2 0) tmp<o>-17)))
  282. (assert (and true (= (q<r>-3 0) (+ (q<r>-2 0) tmp<r>-17))))
  283. (assert (= tmp<o>-18 (* (A<o>-0 0 3) (r<o>-4 3))))
  284. (assert (and true (= tmp<r>-18 (* (A<r>-0 0 3) (r<r>-4 3)))))
  285. (assert (and (=> (distinct 0 0) (= (q<o>-4 0) (q<o>-3 0)))
  286. (=> (distinct 0 1) (= (q<o>-4 1) (q<o>-3 1)))
  287. (=> (distinct 0 2) (= (q<o>-4 2) (q<o>-3 2)))
  288. (=> (distinct 0 3) (= (q<o>-4 3) (q<o>-3 3)))))
  289. (assert (and (=> (distinct 0 0) (= (q<r>-4 0) (q<r>-3 0)))
  290. (=> (distinct 0 1) (= (q<r>-4 1) (q<r>-3 1)))
  291. (=> (distinct 0 2) (= (q<r>-4 2) (q<r>-3 2)))
  292. (=> (distinct 0 3) (= (q<r>-4 3) (q<r>-3 3)))))
  293. (assert (= (q<o>-4 0) (+ (q<o>-3 0) tmp<o>-18)))
  294. (assert (and true (= (q<r>-4 0) (+ (q<r>-3 0) tmp<r>-18))))
  295. (assert (and (=> (distinct 1 0) (= (q<o>-5 0) (q<o>-4 0)))
  296. (=> (distinct 1 1) (= (q<o>-5 1) (q<o>-4 1)))
  297. (=> (distinct 1 2) (= (q<o>-5 2) (q<o>-4 2)))
  298. (=> (distinct 1 3) (= (q<o>-5 3) (q<o>-4 3)))))
  299. (assert (and (=> (distinct 1 0) (= (q<r>-5 0) (q<r>-4 0)))
  300. (=> (distinct 1 1) (= (q<r>-5 1) (q<r>-4 1)))
  301. (=> (distinct 1 2) (= (q<r>-5 2) (q<r>-4 2)))
  302. (=> (distinct 1 3) (= (q<r>-5 3) (q<r>-4 3)))))
  303. (assert (= (q<o>-5 1) (* (A<o>-0 1 0) (r<o>-4 0))))
  304. (assert (and true (= (q<r>-5 1) (* (A<r>-0 1 0) (r<r>-4 0)))))
  305. (assert (= tmp<o>-19 (* (A<o>-0 1 1) (r<o>-4 1))))
  306. (assert (and true (= tmp<r>-19 (* (A<r>-0 1 1) (r<r>-4 1)))))
  307. (assert (and (=> (distinct 1 0) (= (q<o>-6 0) (q<o>-5 0)))
  308. (=> (distinct 1 1) (= (q<o>-6 1) (q<o>-5 1)))
  309. (=> (distinct 1 2) (= (q<o>-6 2) (q<o>-5 2)))
  310. (=> (distinct 1 3) (= (q<o>-6 3) (q<o>-5 3)))))
  311. (assert (and (=> (distinct 1 0) (= (q<r>-6 0) (q<r>-5 0)))
  312. (=> (distinct 1 1) (= (q<r>-6 1) (q<r>-5 1)))
  313. (=> (distinct 1 2) (= (q<r>-6 2) (q<r>-5 2)))
  314. (=> (distinct 1 3) (= (q<r>-6 3) (q<r>-5 3)))))
  315. (assert (= (q<o>-6 1) (+ (q<o>-5 0) tmp<o>-19)))
  316. (assert (and true (= (q<r>-6 1) (+ (q<r>-5 0) tmp<r>-19))))
  317. (assert (= tmp<o>-20 (* (A<o>-0 1 2) (r<o>-4 2))))
  318. (assert (and true (= tmp<r>-20 (* (A<r>-0 1 2) (r<r>-4 2)))))
  319. (assert (and (=> (distinct 1 0) (= (q<o>-7 0) (q<o>-6 0)))
  320. (=> (distinct 1 1) (= (q<o>-7 1) (q<o>-6 1)))
  321. (=> (distinct 1 2) (= (q<o>-7 2) (q<o>-6 2)))
  322. (=> (distinct 1 3) (= (q<o>-7 3) (q<o>-6 3)))))
  323. (assert (and (=> (distinct 1 0) (= (q<r>-7 0) (q<r>-6 0)))
  324. (=> (distinct 1 1) (= (q<r>-7 1) (q<r>-6 1)))
  325. (=> (distinct 1 2) (= (q<r>-7 2) (q<r>-6 2)))
  326. (=> (distinct 1 3) (= (q<r>-7 3) (q<r>-6 3)))))
  327. (assert (= (q<o>-7 1) (+ (q<o>-6 0) tmp<o>-20)))
  328. (assert (and true (= (q<r>-7 1) (+ (q<r>-6 0) tmp<r>-20))))
  329. (assert (= tmp<o>-21 (* (A<o>-0 1 3) (r<o>-4 3))))
  330. (assert (and true (= tmp<r>-21 (* (A<r>-0 1 3) (r<r>-4 3)))))
  331. (assert (and (=> (distinct 1 0) (= (q<o>-8 0) (q<o>-7 0)))
  332. (=> (distinct 1 1) (= (q<o>-8 1) (q<o>-7 1)))
  333. (=> (distinct 1 2) (= (q<o>-8 2) (q<o>-7 2)))
  334. (=> (distinct 1 3) (= (q<o>-8 3) (q<o>-7 3)))))
  335. (assert (and (=> (distinct 1 0) (= (q<r>-8 0) (q<r>-7 0)))
  336. (=> (distinct 1 1) (= (q<r>-8 1) (q<r>-7 1)))
  337. (=> (distinct 1 2) (= (q<r>-8 2) (q<r>-7 2)))
  338. (=> (distinct 1 3) (= (q<r>-8 3) (q<r>-7 3)))))
  339. (assert (= (q<o>-8 1) (+ (q<o>-7 0) tmp<o>-21)))
  340. (assert (and true (= (q<r>-8 1) (+ (q<r>-7 0) tmp<r>-21))))
  341. (assert (and (=> (distinct 2 0) (= (q<o>-9 0) (q<o>-8 0)))
  342. (=> (distinct 2 1) (= (q<o>-9 1) (q<o>-8 1)))
  343. (=> (distinct 2 2) (= (q<o>-9 2) (q<o>-8 2)))
  344. (=> (distinct 2 3) (= (q<o>-9 3) (q<o>-8 3)))))
  345. (assert (and (=> (distinct 2 0) (= (q<r>-9 0) (q<r>-8 0)))
  346. (=> (distinct 2 1) (= (q<r>-9 1) (q<r>-8 1)))
  347. (=> (distinct 2 2) (= (q<r>-9 2) (q<r>-8 2)))
  348. (=> (distinct 2 3) (= (q<r>-9 3) (q<r>-8 3)))))
  349. (assert (= (q<o>-9 2) (* (A<o>-0 2 0) (r<o>-4 0))))
  350. (assert (and true (= (q<r>-9 2) (* (A<r>-0 2 0) (r<r>-4 0)))))
  351. (assert (= tmp<o>-22 (* (A<o>-0 2 1) (r<o>-4 1))))
  352. (assert (and true (= tmp<r>-22 (* (A<r>-0 2 1) (r<r>-4 1)))))
  353. (assert (and (=> (distinct 2 0) (= (q<o>-10 0) (q<o>-9 0)))
  354. (=> (distinct 2 1) (= (q<o>-10 1) (q<o>-9 1)))
  355. (=> (distinct 2 2) (= (q<o>-10 2) (q<o>-9 2)))
  356. (=> (distinct 2 3) (= (q<o>-10 3) (q<o>-9 3)))))
  357. (assert (and (=> (distinct 2 0) (= (q<r>-10 0) (q<r>-9 0)))
  358. (=> (distinct 2 1) (= (q<r>-10 1) (q<r>-9 1)))
  359. (=> (distinct 2 2) (= (q<r>-10 2) (q<r>-9 2)))
  360. (=> (distinct 2 3) (= (q<r>-10 3) (q<r>-9 3)))))
  361. (assert (= (q<o>-10 2) (+ (q<o>-9 0) tmp<o>-22)))
  362. (assert (and true (= (q<r>-10 2) (+ (q<r>-9 0) tmp<r>-22))))
  363. (assert (= tmp<o>-23 (* (A<o>-0 2 2) (r<o>-4 2))))
  364. (assert (and true (= tmp<r>-23 (* (A<r>-0 2 2) (r<r>-4 2)))))
  365. (assert (and (=> (distinct 2 0) (= (q<o>-11 0) (q<o>-10 0)))
  366. (=> (distinct 2 1) (= (q<o>-11 1) (q<o>-10 1)))
  367. (=> (distinct 2 2) (= (q<o>-11 2) (q<o>-10 2)))
  368. (=> (distinct 2 3) (= (q<o>-11 3) (q<o>-10 3)))))
  369. (assert (and (=> (distinct 2 0) (= (q<r>-11 0) (q<r>-10 0)))
  370. (=> (distinct 2 1) (= (q<r>-11 1) (q<r>-10 1)))
  371. (=> (distinct 2 2) (= (q<r>-11 2) (q<r>-10 2)))
  372. (=> (distinct 2 3) (= (q<r>-11 3) (q<r>-10 3)))))
  373. (assert (= (q<o>-11 2) (+ (q<o>-10 0) tmp<o>-23)))
  374. (assert (and true (= (q<r>-11 2) (+ (q<r>-10 0) tmp<r>-23))))
  375. (assert (= tmp<o>-24 (* (A<o>-0 2 3) (r<o>-4 3))))
  376. (assert (and true (= tmp<r>-24 (* (A<r>-0 2 3) (r<r>-4 3)))))
  377. (assert (and (=> (distinct 2 0) (= (q<o>-12 0) (q<o>-11 0)))
  378. (=> (distinct 2 1) (= (q<o>-12 1) (q<o>-11 1)))
  379. (=> (distinct 2 2) (= (q<o>-12 2) (q<o>-11 2)))
  380. (=> (distinct 2 3) (= (q<o>-12 3) (q<o>-11 3)))))
  381. (assert (and (=> (distinct 2 0) (= (q<r>-12 0) (q<r>-11 0)))
  382. (=> (distinct 2 1) (= (q<r>-12 1) (q<r>-11 1)))
  383. (=> (distinct 2 2) (= (q<r>-12 2) (q<r>-11 2)))
  384. (=> (distinct 2 3) (= (q<r>-12 3) (q<r>-11 3)))))
  385. (assert (= (q<o>-12 2) (+ (q<o>-11 0) tmp<o>-24)))
  386. (assert (and true (= (q<r>-12 2) (+ (q<r>-11 0) tmp<r>-24))))
  387. (assert (and (=> (distinct 3 0) (= (q<o>-13 0) (q<o>-12 0)))
  388. (=> (distinct 3 1) (= (q<o>-13 1) (q<o>-12 1)))
  389. (=> (distinct 3 2) (= (q<o>-13 2) (q<o>-12 2)))
  390. (=> (distinct 3 3) (= (q<o>-13 3) (q<o>-12 3)))))
  391. (assert (and (=> (distinct 3 0) (= (q<r>-13 0) (q<r>-12 0)))
  392. (=> (distinct 3 1) (= (q<r>-13 1) (q<r>-12 1)))
  393. (=> (distinct 3 2) (= (q<r>-13 2) (q<r>-12 2)))
  394. (=> (distinct 3 3) (= (q<r>-13 3) (q<r>-12 3)))))
  395. (assert (= (q<o>-13 3) (* (A<o>-0 3 0) (r<o>-4 0))))
  396. (assert (and true (= (q<r>-13 3) (* (A<r>-0 3 0) (r<r>-4 0)))))
  397. (assert (= tmp<o>-25 (* (A<o>-0 3 1) (r<o>-4 1))))
  398. (assert (and true (= tmp<r>-25 (* (A<r>-0 3 1) (r<r>-4 1)))))
  399. (assert (and (=> (distinct 3 0) (= (q<o>-14 0) (q<o>-13 0)))
  400. (=> (distinct 3 1) (= (q<o>-14 1) (q<o>-13 1)))
  401. (=> (distinct 3 2) (= (q<o>-14 2) (q<o>-13 2)))
  402. (=> (distinct 3 3) (= (q<o>-14 3) (q<o>-13 3)))))
  403. (assert (and (=> (distinct 3 0) (= (q<r>-14 0) (q<r>-13 0)))
  404. (=> (distinct 3 1) (= (q<r>-14 1) (q<r>-13 1)))
  405. (=> (distinct 3 2) (= (q<r>-14 2) (q<r>-13 2)))
  406. (=> (distinct 3 3) (= (q<r>-14 3) (q<r>-13 3)))))
  407. (assert (= (q<o>-14 3) (+ (q<o>-13 0) tmp<o>-25)))
  408. (assert (and true (= (q<r>-14 3) (+ (q<r>-13 0) tmp<r>-25))))
  409. (assert (= tmp<o>-26 (* (A<o>-0 3 2) (r<o>-4 2))))
  410. (assert (and true (= tmp<r>-26 (* (A<r>-0 3 2) (r<r>-4 2)))))
  411. (assert (and (=> (distinct 3 0) (= (q<o>-15 0) (q<o>-14 0)))
  412. (=> (distinct 3 1) (= (q<o>-15 1) (q<o>-14 1)))
  413. (=> (distinct 3 2) (= (q<o>-15 2) (q<o>-14 2)))
  414. (=> (distinct 3 3) (= (q<o>-15 3) (q<o>-14 3)))))
  415. (assert (and (=> (distinct 3 0) (= (q<r>-15 0) (q<r>-14 0)))
  416. (=> (distinct 3 1) (= (q<r>-15 1) (q<r>-14 1)))
  417. (=> (distinct 3 2) (= (q<r>-15 2) (q<r>-14 2)))
  418. (=> (distinct 3 3) (= (q<r>-15 3) (q<r>-14 3)))))
  419. (assert (= (q<o>-15 3) (+ (q<o>-14 0) tmp<o>-26)))
  420. (assert (and true (= (q<r>-15 3) (+ (q<r>-14 0) tmp<r>-26))))
  421. (assert (= tmp<o>-27 (* (A<o>-0 3 3) (r<o>-4 3))))
  422. (assert (and true (= tmp<r>-27 (* (A<r>-0 3 3) (r<r>-4 3)))))
  423. (assert (and (=> (distinct 3 0) (= (q<o>-16 0) (q<o>-15 0)))
  424. (=> (distinct 3 1) (= (q<o>-16 1) (q<o>-15 1)))
  425. (=> (distinct 3 2) (= (q<o>-16 2) (q<o>-15 2)))
  426. (=> (distinct 3 3) (= (q<o>-16 3) (q<o>-15 3)))))
  427. (assert (and (=> (distinct 3 0) (= (q<r>-16 0) (q<r>-15 0)))
  428. (=> (distinct 3 1) (= (q<r>-16 1) (q<r>-15 1)))
  429. (=> (distinct 3 2) (= (q<r>-16 2) (q<r>-15 2)))
  430. (=> (distinct 3 3) (= (q<r>-16 3) (q<r>-15 3)))))
  431. (assert (= (q<o>-16 3) (+ (q<o>-15 0) tmp<o>-27)))
  432. (assert (and true (= (q<r>-16 3) (+ (q<r>-15 0) tmp<r>-27))))
  433. (assert (= rtq<o>-1 (* (r<o>-4 0) (q<o>-16 0))))
  434. (assert (and true (= rtq<r>-1 (* (r<r>-4 0) (q<r>-16 0)))))
  435. (assert (= tmp<o>-28 (* (r<o>-4 1) (q<o>-16 1))))
  436. (assert (and true (= tmp<r>-28 (* (r<r>-4 1) (q<r>-16 1)))))
  437. (assert (= rtq<o>-2 (+ rtq<o>-1 tmp<o>-28)))
  438. (assert (and true (= rtq<r>-2 (+ rtq<r>-1 tmp<r>-28))))
  439. (assert (= tmp<o>-29 (* (r<o>-4 2) (q<o>-16 2))))
  440. (assert (and true (= tmp<r>-29 (* (r<r>-4 2) (q<r>-16 2)))))
  441. (assert (= rtq<o>-3 (+ rtq<o>-2 tmp<o>-29)))
  442. (assert (and true (= rtq<r>-3 (+ rtq<r>-2 tmp<r>-29))))
  443. (assert (= tmp<o>-30 (* (r<o>-4 3) (q<o>-16 3))))
  444. (assert (and true (= tmp<r>-30 (* (r<r>-4 3) (q<r>-16 3)))))
  445. (assert (= rtq<o>-4 (+ rtq<o>-3 tmp<o>-30)))
  446. (assert (and true (= rtq<r>-4 (+ rtq<r>-3 tmp<r>-30))))
  447. (assert (= alpha<o>-1 (/ r_norm<o>-4 rtq<o>-4)))
  448. (assert (and true (= alpha<r>-1 (/ r_norm<r>-4 rtq<r>-4))))
  449. (assert (and (=> (distinct 0 0) (= (alphar<o>-1 0) (alphar<o>-0 0)))
  450. (=> (distinct 0 1) (= (alphar<o>-1 1) (alphar<o>-0 1)))
  451. (=> (distinct 0 2) (= (alphar<o>-1 2) (alphar<o>-0 2)))
  452. (=> (distinct 0 3) (= (alphar<o>-1 3) (alphar<o>-0 3)))))
  453. (assert (and (=> (distinct 0 0) (= (alphar<r>-1 0) (alphar<r>-0 0)))
  454. (=> (distinct 0 1) (= (alphar<r>-1 1) (alphar<r>-0 1)))
  455. (=> (distinct 0 2) (= (alphar<r>-1 2) (alphar<r>-0 2)))
  456. (=> (distinct 0 3) (= (alphar<r>-1 3) (alphar<r>-0 3)))))
  457. (assert (= (alphar<o>-1 0) (* alpha<o>-1 (r<o>-4 0))))
  458. (assert (and true (= (alphar<r>-1 0) (* alpha<r>-1 (r<r>-4 0)))))
  459. (assert (and (=> (distinct 1 0) (= (alphar<o>-2 0) (alphar<o>-1 0)))
  460. (=> (distinct 1 1) (= (alphar<o>-2 1) (alphar<o>-1 1)))
  461. (=> (distinct 1 2) (= (alphar<o>-2 2) (alphar<o>-1 2)))
  462. (=> (distinct 1 3) (= (alphar<o>-2 3) (alphar<o>-1 3)))))
  463. (assert (and (=> (distinct 1 0) (= (alphar<r>-2 0) (alphar<r>-1 0)))
  464. (=> (distinct 1 1) (= (alphar<r>-2 1) (alphar<r>-1 1)))
  465. (=> (distinct 1 2) (= (alphar<r>-2 2) (alphar<r>-1 2)))
  466. (=> (distinct 1 3) (= (alphar<r>-2 3) (alphar<r>-1 3)))))
  467. (assert (= (alphar<o>-2 1) (* alpha<o>-1 (r<o>-4 1))))
  468. (assert (and true (= (alphar<r>-2 1) (* alpha<r>-1 (r<r>-4 1)))))
  469. (assert (and (=> (distinct 2 0) (= (alphar<o>-3 0) (alphar<o>-2 0)))
  470. (=> (distinct 2 1) (= (alphar<o>-3 1) (alphar<o>-2 1)))
  471. (=> (distinct 2 2) (= (alphar<o>-3 2) (alphar<o>-2 2)))
  472. (=> (distinct 2 3) (= (alphar<o>-3 3) (alphar<o>-2 3)))))
  473. (assert (and (=> (distinct 2 0) (= (alphar<r>-3 0) (alphar<r>-2 0)))
  474. (=> (distinct 2 1) (= (alphar<r>-3 1) (alphar<r>-2 1)))
  475. (=> (distinct 2 2) (= (alphar<r>-3 2) (alphar<r>-2 2)))
  476. (=> (distinct 2 3) (= (alphar<r>-3 3) (alphar<r>-2 3)))))
  477. (assert (= (alphar<o>-3 2) (* alpha<o>-1 (r<o>-4 2))))
  478. (assert (and true (= (alphar<r>-3 2) (* alpha<r>-1 (r<r>-4 2)))))
  479. (assert (and (=> (distinct 3 0) (= (alphar<o>-4 0) (alphar<o>-3 0)))
  480. (=> (distinct 3 1) (= (alphar<o>-4 1) (alphar<o>-3 1)))
  481. (=> (distinct 3 2) (= (alphar<o>-4 2) (alphar<o>-3 2)))
  482. (=> (distinct 3 3) (= (alphar<o>-4 3) (alphar<o>-3 3)))))
  483. (assert (and (=> (distinct 3 0) (= (alphar<r>-4 0) (alphar<r>-3 0)))
  484. (=> (distinct 3 1) (= (alphar<r>-4 1) (alphar<r>-3 1)))
  485. (=> (distinct 3 2) (= (alphar<r>-4 2) (alphar<r>-3 2)))
  486. (=> (distinct 3 3) (= (alphar<r>-4 3) (alphar<r>-3 3)))))
  487. (assert (= (alphar<o>-4 3) (* alpha<o>-1 (r<o>-4 3))))
  488. (assert (and true (= (alphar<r>-4 3) (* alpha<r>-1 (r<r>-4 3)))))
  489. (assert (and (=> (distinct 0 0) (= (x<o>-1 0) (x<o>-0 0)))
  490. (=> (distinct 0 1) (= (x<o>-1 1) (x<o>-0 1)))
  491. (=> (distinct 0 2) (= (x<o>-1 2) (x<o>-0 2)))
  492. (=> (distinct 0 3) (= (x<o>-1 3) (x<o>-0 3)))))
  493. (assert (and (=> (distinct 0 0) (= (x<r>-1 0) (x<r>-0 0)))
  494. (=> (distinct 0 1) (= (x<r>-1 1) (x<r>-0 1)))
  495. (=> (distinct 0 2) (= (x<r>-1 2) (x<r>-0 2)))
  496. (=> (distinct 0 3) (= (x<r>-1 3) (x<r>-0 3)))))
  497. (assert (= (x<o>-1 0) (+ (x<o>-0 0) (alphar<o>-4 0))))
  498. (assert (and true (= (x<r>-1 0) (+ (x<r>-0 0) (alphar<r>-4 0)))))
  499. (assert (and (=> (distinct 1 0) (= (x<o>-2 0) (x<o>-1 0)))
  500. (=> (distinct 1 1) (= (x<o>-2 1) (x<o>-1 1)))
  501. (=> (distinct 1 2) (= (x<o>-2 2) (x<o>-1 2)))
  502. (=> (distinct 1 3) (= (x<o>-2 3) (x<o>-1 3)))))
  503. (assert (and (=> (distinct 1 0) (= (x<r>-2 0) (x<r>-1 0)))
  504. (=> (distinct 1 1) (= (x<r>-2 1) (x<r>-1 1)))
  505. (=> (distinct 1 2) (= (x<r>-2 2) (x<r>-1 2)))
  506. (=> (distinct 1 3) (= (x<r>-2 3) (x<r>-1 3)))))
  507. (assert (= (x<o>-2 1) (+ (x<o>-1 1) (alphar<o>-4 1))))
  508. (assert (and true (= (x<r>-2 1) (+ (x<r>-1 1) (alphar<r>-4 1)))))
  509. (assert (and (=> (distinct 2 0) (= (x<o>-3 0) (x<o>-2 0)))
  510. (=> (distinct 2 1) (= (x<o>-3 1) (x<o>-2 1)))
  511. (=> (distinct 2 2) (= (x<o>-3 2) (x<o>-2 2)))
  512. (=> (distinct 2 3) (= (x<o>-3 3) (x<o>-2 3)))))
  513. (assert (and (=> (distinct 2 0) (= (x<r>-3 0) (x<r>-2 0)))
  514. (=> (distinct 2 1) (= (x<r>-3 1) (x<r>-2 1)))
  515. (=> (distinct 2 2) (= (x<r>-3 2) (x<r>-2 2)))
  516. (=> (distinct 2 3) (= (x<r>-3 3) (x<r>-2 3)))))
  517. (assert (= (x<o>-3 2) (+ (x<o>-2 2) (alphar<o>-4 2))))
  518. (assert (and true (= (x<r>-3 2) (+ (x<r>-2 2) (alphar<r>-4 2)))))
  519. (assert (and (=> (distinct 3 0) (= (x<o>-4 0) (x<o>-3 0)))
  520. (=> (distinct 3 1) (= (x<o>-4 1) (x<o>-3 1)))
  521. (=> (distinct 3 2) (= (x<o>-4 2) (x<o>-3 2)))
  522. (=> (distinct 3 3) (= (x<o>-4 3) (x<o>-3 3)))))
  523. (assert (and (=> (distinct 3 0) (= (x<r>-4 0) (x<r>-3 0)))
  524. (=> (distinct 3 1) (= (x<r>-4 1) (x<r>-3 1)))
  525. (=> (distinct 3 2) (= (x<r>-4 2) (x<r>-3 2)))
  526. (=> (distinct 3 3) (= (x<r>-4 3) (x<r>-3 3)))))
  527. (assert (= (x<o>-4 3) (+ (x<o>-3 3) (alphar<o>-4 3))))
  528. (assert (and true (= (x<r>-4 3) (+ (x<r>-3 3) (alphar<r>-4 3)))))
  529. (assert (and (=> (distinct 0 0) (= (alphaq<o>-1 0) (alphaq<o>-0 0)))
  530. (=> (distinct 0 1) (= (alphaq<o>-1 1) (alphaq<o>-0 1)))
  531. (=> (distinct 0 2) (= (alphaq<o>-1 2) (alphaq<o>-0 2)))
  532. (=> (distinct 0 3) (= (alphaq<o>-1 3) (alphaq<o>-0 3)))))
  533. (assert (and (=> (distinct 0 0) (= (alphaq<r>-1 0) (alphaq<r>-0 0)))
  534. (=> (distinct 0 1) (= (alphaq<r>-1 1) (alphaq<r>-0 1)))
  535. (=> (distinct 0 2) (= (alphaq<r>-1 2) (alphaq<r>-0 2)))
  536. (=> (distinct 0 3) (= (alphaq<r>-1 3) (alphaq<r>-0 3)))))
  537. (assert (= (alphaq<o>-1 0) (* alpha<o>-1 (q<o>-16 0))))
  538. (assert (and true (= (alphaq<r>-1 0) (* alpha<r>-1 (q<r>-16 0)))))
  539. (assert (and (=> (distinct 1 0) (= (alphaq<o>-2 0) (alphaq<o>-1 0)))
  540. (=> (distinct 1 1) (= (alphaq<o>-2 1) (alphaq<o>-1 1)))
  541. (=> (distinct 1 2) (= (alphaq<o>-2 2) (alphaq<o>-1 2)))
  542. (=> (distinct 1 3) (= (alphaq<o>-2 3) (alphaq<o>-1 3)))))
  543. (assert (and (=> (distinct 1 0) (= (alphaq<r>-2 0) (alphaq<r>-1 0)))
  544. (=> (distinct 1 1) (= (alphaq<r>-2 1) (alphaq<r>-1 1)))
  545. (=> (distinct 1 2) (= (alphaq<r>-2 2) (alphaq<r>-1 2)))
  546. (=> (distinct 1 3) (= (alphaq<r>-2 3) (alphaq<r>-1 3)))))
  547. (assert (= (alphaq<o>-2 1) (* alpha<o>-1 (q<o>-16 1))))
  548. (assert (and true (= (alphaq<r>-2 1) (* alpha<r>-1 (q<r>-16 1)))))
  549. (assert (and (=> (distinct 2 0) (= (alphaq<o>-3 0) (alphaq<o>-2 0)))
  550. (=> (distinct 2 1) (= (alphaq<o>-3 1) (alphaq<o>-2 1)))
  551. (=> (distinct 2 2) (= (alphaq<o>-3 2) (alphaq<o>-2 2)))
  552. (=> (distinct 2 3) (= (alphaq<o>-3 3) (alphaq<o>-2 3)))))
  553. (assert (and (=> (distinct 2 0) (= (alphaq<r>-3 0) (alphaq<r>-2 0)))
  554. (=> (distinct 2 1) (= (alphaq<r>-3 1) (alphaq<r>-2 1)))
  555. (=> (distinct 2 2) (= (alphaq<r>-3 2) (alphaq<r>-2 2)))
  556. (=> (distinct 2 3) (= (alphaq<r>-3 3) (alphaq<r>-2 3)))))
  557. (assert (= (alphaq<o>-3 2) (* alpha<o>-1 (q<o>-16 2))))
  558. (assert (and true (= (alphaq<r>-3 2) (* alpha<r>-1 (q<r>-16 2)))))
  559. (assert (and (=> (distinct 3 0) (= (alphaq<o>-4 0) (alphaq<o>-3 0)))
  560. (=> (distinct 3 1) (= (alphaq<o>-4 1) (alphaq<o>-3 1)))
  561. (=> (distinct 3 2) (= (alphaq<o>-4 2) (alphaq<o>-3 2)))
  562. (=> (distinct 3 3) (= (alphaq<o>-4 3) (alphaq<o>-3 3)))))
  563. (assert (and (=> (distinct 3 0) (= (alphaq<r>-4 0) (alphaq<r>-3 0)))
  564. (=> (distinct 3 1) (= (alphaq<r>-4 1) (alphaq<r>-3 1)))
  565. (=> (distinct 3 2) (= (alphaq<r>-4 2) (alphaq<r>-3 2)))
  566. (=> (distinct 3 3) (= (alphaq<r>-4 3) (alphaq<r>-3 3)))))
  567. (assert (= (alphaq<o>-4 3) (* alpha<o>-1 (q<o>-16 3))))
  568. (assert (and true (= (alphaq<r>-4 3) (* alpha<r>-1 (q<r>-16 3)))))
  569. (assert (and (=> (distinct 0 0) (= (r<o>-5 0) (r<o>-4 0)))
  570. (=> (distinct 0 1) (= (r<o>-5 1) (r<o>-4 1)))
  571. (=> (distinct 0 2) (= (r<o>-5 2) (r<o>-4 2)))
  572. (=> (distinct 0 3) (= (r<o>-5 3) (r<o>-4 3)))))
  573. (assert (and (=> (distinct 0 0) (= (r<r>-5 0) (r<r>-4 0)))
  574. (=> (distinct 0 1) (= (r<r>-5 1) (r<r>-4 1)))
  575. (=> (distinct 0 2) (= (r<r>-5 2) (r<r>-4 2)))
  576. (=> (distinct 0 3) (= (r<r>-5 3) (r<r>-4 3)))))
  577. (assert (= (r<o>-5 0) (- (r<o>-4 0) (alphaq<o>-4 0))))
  578. (assert (and true (= (r<r>-5 0) (- (r<r>-4 0) (alphaq<r>-4 0)))))
  579. (assert (and (=> (distinct 1 0) (= (r<o>-6 0) (r<o>-5 0)))
  580. (=> (distinct 1 1) (= (r<o>-6 1) (r<o>-5 1)))
  581. (=> (distinct 1 2) (= (r<o>-6 2) (r<o>-5 2)))
  582. (=> (distinct 1 3) (= (r<o>-6 3) (r<o>-5 3)))))
  583. (assert (and (=> (distinct 1 0) (= (r<r>-6 0) (r<r>-5 0)))
  584. (=> (distinct 1 1) (= (r<r>-6 1) (r<r>-5 1)))
  585. (=> (distinct 1 2) (= (r<r>-6 2) (r<r>-5 2)))
  586. (=> (distinct 1 3) (= (r<r>-6 3) (r<r>-5 3)))))
  587. (assert (= (r<o>-6 1) (- (r<o>-5 1) (alphaq<o>-4 1))))
  588. (assert (and true (= (r<r>-6 1) (- (r<r>-5 1) (alphaq<r>-4 1)))))
  589. (assert (and (=> (distinct 2 0) (= (r<o>-7 0) (r<o>-6 0)))
  590. (=> (distinct 2 1) (= (r<o>-7 1) (r<o>-6 1)))
  591. (=> (distinct 2 2) (= (r<o>-7 2) (r<o>-6 2)))
  592. (=> (distinct 2 3) (= (r<o>-7 3) (r<o>-6 3)))))
  593. (assert (and (=> (distinct 2 0) (= (r<r>-7 0) (r<r>-6 0)))
  594. (=> (distinct 2 1) (= (r<r>-7 1) (r<r>-6 1)))
  595. (=> (distinct 2 2) (= (r<r>-7 2) (r<r>-6 2)))
  596. (=> (distinct 2 3) (= (r<r>-7 3) (r<r>-6 3)))))
  597. (assert (= (r<o>-7 2) (- (r<o>-6 2) (alphaq<o>-4 2))))
  598. (assert (and true (= (r<r>-7 2) (- (r<r>-6 2) (alphaq<r>-4 2)))))
  599. (assert (and (=> (distinct 3 0) (= (r<o>-8 0) (r<o>-7 0)))
  600. (=> (distinct 3 1) (= (r<o>-8 1) (r<o>-7 1)))
  601. (=> (distinct 3 2) (= (r<o>-8 2) (r<o>-7 2)))
  602. (=> (distinct 3 3) (= (r<o>-8 3) (r<o>-7 3)))))
  603. (assert (and (=> (distinct 3 0) (= (r<r>-8 0) (r<r>-7 0)))
  604. (=> (distinct 3 1) (= (r<r>-8 1) (r<r>-7 1)))
  605. (=> (distinct 3 2) (= (r<r>-8 2) (r<r>-7 2)))
  606. (=> (distinct 3 3) (= (r<r>-8 3) (r<r>-7 3)))))
  607. (assert (= (r<o>-8 3) (- (r<o>-7 3) (alphaq<o>-4 3))))
  608. (assert (and true (= (r<r>-8 3) (- (r<r>-7 3) (alphaq<r>-4 3)))))
  609. (assert (= r_norm<o>-5 (* (r<o>-8 0) (r<o>-8 0))))
  610. (assert (and true (= r_norm<r>-5 (* (r<r>-8 0) (r<r>-8 0)))))
  611. (assert (= tmp<o>-31 (* (r<o>-8 1) (r<o>-8 1))))
  612. (assert (and true (= tmp<r>-31 (* (r<r>-8 1) (r<r>-8 1)))))
  613. (assert (= r_norm<o>-6 (+ r_norm<o>-5 tmp<o>-31)))
  614. (assert (and true (= r_norm<r>-6 (+ r_norm<r>-5 tmp<r>-31))))
  615. (assert (= tmp<o>-32 (* (r<o>-8 2) (r<o>-8 2))))
  616. (assert (and true (= tmp<r>-32 (* (r<r>-8 2) (r<r>-8 2)))))
  617. (assert (= r_norm<o>-7 (+ r_norm<o>-6 tmp<o>-32)))
  618. (assert (and true (= r_norm<r>-7 (+ r_norm<r>-6 tmp<r>-32))))
  619. (assert (= tmp<o>-33 (* (r<o>-8 3) (r<o>-8 3))))
  620. (assert (and true (= tmp<r>-33 (* (r<r>-8 3) (r<r>-8 3)))))
  621. (assert (= r_norm<o>-8 (+ r_norm<o>-7 tmp<o>-33)))
  622. (assert (and true (= r_norm<r>-8 (+ r_norm<r>-7 tmp<r>-33))))
  623. (assert (= i<o>-2 (+ i<o>-1 1)))
  624. (assert (and true (= i<r>-2 (+ i<r>-1 1))))
  625. (assert (and (=> (distinct 0 0) (= (Ax<o>-17 0) (Ax<o>-16 0)))
  626. (=> (distinct 0 1) (= (Ax<o>-17 1) (Ax<o>-16 1)))
  627. (=> (distinct 0 2) (= (Ax<o>-17 2) (Ax<o>-16 2)))
  628. (=> (distinct 0 3) (= (Ax<o>-17 3) (Ax<o>-16 3)))))
  629. (assert (and (=> (distinct 0 0) (= (Ax<r>-17 0) (Ax<r>-16 0)))
  630. (=> (distinct 0 1) (= (Ax<r>-17 1) (Ax<r>-16 1)))
  631. (=> (distinct 0 2) (= (Ax<r>-17 2) (Ax<r>-16 2)))
  632. (=> (distinct 0 3) (= (Ax<r>-17 3) (Ax<r>-16 3)))))
  633. (assert (= (Ax<o>-17 0) (* (A<o>-0 0 0) (x<o>-4 0))))
  634. (assert (and true (= (Ax<r>-17 0) (* (A<r>-0 0 0) (x<r>-4 0)))))
  635. (assert (= tmp<o>-34 (* (A<o>-0 0 1) (x<o>-4 1))))
  636. (assert (and true (= tmp<r>-34 (* (A<r>-0 0 1) (x<r>-4 1)))))
  637. (assert (and (=> (distinct 0 0) (= (Ax<o>-18 0) (Ax<o>-17 0)))
  638. (=> (distinct 0 1) (= (Ax<o>-18 1) (Ax<o>-17 1)))
  639. (=> (distinct 0 2) (= (Ax<o>-18 2) (Ax<o>-17 2)))
  640. (=> (distinct 0 3) (= (Ax<o>-18 3) (Ax<o>-17 3)))))
  641. (assert (and (=> (distinct 0 0) (= (Ax<r>-18 0) (Ax<r>-17 0)))
  642. (=> (distinct 0 1) (= (Ax<r>-18 1) (Ax<r>-17 1)))
  643. (=> (distinct 0 2) (= (Ax<r>-18 2) (Ax<r>-17 2)))
  644. (=> (distinct 0 3) (= (Ax<r>-18 3) (Ax<r>-17 3)))))
  645. (assert (= (Ax<o>-18 0) (+ (Ax<o>-17 0) tmp<o>-34)))
  646. (assert (and true (= (Ax<r>-18 0) (+ (Ax<r>-17 0) tmp<r>-34))))
  647. (assert (= tmp<o>-35 (* (A<o>-0 0 2) (x<o>-4 2))))
  648. (assert (and true (= tmp<r>-35 (* (A<r>-0 0 2) (x<r>-4 2)))))
  649. (assert (and (=> (distinct 0 0) (= (Ax<o>-19 0) (Ax<o>-18 0)))
  650. (=> (distinct 0 1) (= (Ax<o>-19 1) (Ax<o>-18 1)))
  651. (=> (distinct 0 2) (= (Ax<o>-19 2) (Ax<o>-18 2)))
  652. (=> (distinct 0 3) (= (Ax<o>-19 3) (Ax<o>-18 3)))))
  653. (assert (and (=> (distinct 0 0) (= (Ax<r>-19 0) (Ax<r>-18 0)))
  654. (=> (distinct 0 1) (= (Ax<r>-19 1) (Ax<r>-18 1)))
  655. (=> (distinct 0 2) (= (Ax<r>-19 2) (Ax<r>-18 2)))
  656. (=> (distinct 0 3) (= (Ax<r>-19 3) (Ax<r>-18 3)))))
  657. (assert (= (Ax<o>-19 0) (+ (Ax<o>-18 0) tmp<o>-35)))
  658. (assert (and true (= (Ax<r>-19 0) (+ (Ax<r>-18 0) tmp<r>-35))))
  659. (assert (= tmp<o>-36 (* (A<o>-0 0 3) (x<o>-4 3))))
  660. (assert (and true (= tmp<r>-36 (* (A<r>-0 0 3) (x<r>-4 3)))))
  661. (assert (and (=> (distinct 0 0) (= (Ax<o>-20 0) (Ax<o>-19 0)))
  662. (=> (distinct 0 1) (= (Ax<o>-20 1) (Ax<o>-19 1)))
  663. (=> (distinct 0 2) (= (Ax<o>-20 2) (Ax<o>-19 2)))
  664. (=> (distinct 0 3) (= (Ax<o>-20 3) (Ax<o>-19 3)))))
  665. (assert (and (=> (distinct 0 0) (= (Ax<r>-20 0) (Ax<r>-19 0)))
  666. (=> (distinct 0 1) (= (Ax<r>-20 1) (Ax<r>-19 1)))
  667. (=> (distinct 0 2) (= (Ax<r>-20 2) (Ax<r>-19 2)))
  668. (=> (distinct 0 3) (= (Ax<r>-20 3) (Ax<r>-19 3)))))
  669. (assert (= (Ax<o>-20 0) (+ (Ax<o>-19 0) tmp<o>-36)))
  670. (assert (and true (= (Ax<r>-20 0) (+ (Ax<r>-19 0) tmp<r>-36))))
  671. (assert (and (=> (distinct 1 0) (= (Ax<o>-21 0) (Ax<o>-20 0)))
  672. (=> (distinct 1 1) (= (Ax<o>-21 1) (Ax<o>-20 1)))
  673. (=> (distinct 1 2) (= (Ax<o>-21 2) (Ax<o>-20 2)))
  674. (=> (distinct 1 3) (= (Ax<o>-21 3) (Ax<o>-20 3)))))
  675. (assert (and (=> (distinct 1 0) (= (Ax<r>-21 0) (Ax<r>-20 0)))
  676. (=> (distinct 1 1) (= (Ax<r>-21 1) (Ax<r>-20 1)))
  677. (=> (distinct 1 2) (= (Ax<r>-21 2) (Ax<r>-20 2)))
  678. (=> (distinct 1 3) (= (Ax<r>-21 3) (Ax<r>-20 3)))))
  679. (assert (= (Ax<o>-21 1) (* (A<o>-0 1 0) (x<o>-4 0))))
  680. (assert (and true (= (Ax<r>-21 1) (* (A<r>-0 1 0) (x<r>-4 0)))))
  681. (assert (= tmp<o>-37 (* (A<o>-0 1 1) (x<o>-4 1))))
  682. (assert (and true (= tmp<r>-37 (* (A<r>-0 1 1) (x<r>-4 1)))))
  683. (assert (and (=> (distinct 1 0) (= (Ax<o>-22 0) (Ax<o>-21 0)))
  684. (=> (distinct 1 1) (= (Ax<o>-22 1) (Ax<o>-21 1)))
  685. (=> (distinct 1 2) (= (Ax<o>-22 2) (Ax<o>-21 2)))
  686. (=> (distinct 1 3) (= (Ax<o>-22 3) (Ax<o>-21 3)))))
  687. (assert (and (=> (distinct 1 0) (= (Ax<r>-22 0) (Ax<r>-21 0)))
  688. (=> (distinct 1 1) (= (Ax<r>-22 1) (Ax<r>-21 1)))
  689. (=> (distinct 1 2) (= (Ax<r>-22 2) (Ax<r>-21 2)))
  690. (=> (distinct 1 3) (= (Ax<r>-22 3) (Ax<r>-21 3)))))
  691. (assert (= (Ax<o>-22 1) (+ (Ax<o>-21 0) tmp<o>-37)))
  692. (assert (and true (= (Ax<r>-22 1) (+ (Ax<r>-21 0) tmp<r>-37))))
  693. (assert (= tmp<o>-38 (* (A<o>-0 1 2) (x<o>-4 2))))
  694. (assert (and true (= tmp<r>-38 (* (A<r>-0 1 2) (x<r>-4 2)))))
  695. (assert (and (=> (distinct 1 0) (= (Ax<o>-23 0) (Ax<o>-22 0)))
  696. (=> (distinct 1 1) (= (Ax<o>-23 1) (Ax<o>-22 1)))
  697. (=> (distinct 1 2) (= (Ax<o>-23 2) (Ax<o>-22 2)))
  698. (=> (distinct 1 3) (= (Ax<o>-23 3) (Ax<o>-22 3)))))
  699. (assert (and (=> (distinct 1 0) (= (Ax<r>-23 0) (Ax<r>-22 0)))
  700. (=> (distinct 1 1) (= (Ax<r>-23 1) (Ax<r>-22 1)))
  701. (=> (distinct 1 2) (= (Ax<r>-23 2) (Ax<r>-22 2)))
  702. (=> (distinct 1 3) (= (Ax<r>-23 3) (Ax<r>-22 3)))))
  703. (assert (= (Ax<o>-23 1) (+ (Ax<o>-22 0) tmp<o>-38)))
  704. (assert (and true (= (Ax<r>-23 1) (+ (Ax<r>-22 0) tmp<r>-38))))
  705. (assert (= tmp<o>-39 (* (A<o>-0 1 3) (x<o>-4 3))))
  706. (assert (and true (= tmp<r>-39 (* (A<r>-0 1 3) (x<r>-4 3)))))
  707. (assert (and (=> (distinct 1 0) (= (Ax<o>-24 0) (Ax<o>-23 0)))
  708. (=> (distinct 1 1) (= (Ax<o>-24 1) (Ax<o>-23 1)))
  709. (=> (distinct 1 2) (= (Ax<o>-24 2) (Ax<o>-23 2)))
  710. (=> (distinct 1 3) (= (Ax<o>-24 3) (Ax<o>-23 3)))))
  711. (assert (and (=> (distinct 1 0) (= (Ax<r>-24 0) (Ax<r>-23 0)))
  712. (=> (distinct 1 1) (= (Ax<r>-24 1) (Ax<r>-23 1)))
  713. (=> (distinct 1 2) (= (Ax<r>-24 2) (Ax<r>-23 2)))
  714. (=> (distinct 1 3) (= (Ax<r>-24 3) (Ax<r>-23 3)))))
  715. (assert (= (Ax<o>-24 1) (+ (Ax<o>-23 0) tmp<o>-39)))
  716. (assert (and true (= (Ax<r>-24 1) (+ (Ax<r>-23 0) tmp<r>-39))))
  717. (assert (and (=> (distinct 2 0) (= (Ax<o>-25 0) (Ax<o>-24 0)))
  718. (=> (distinct 2 1) (= (Ax<o>-25 1) (Ax<o>-24 1)))
  719. (=> (distinct 2 2) (= (Ax<o>-25 2) (Ax<o>-24 2)))
  720. (=> (distinct 2 3) (= (Ax<o>-25 3) (Ax<o>-24 3)))))
  721. (assert (and (=> (distinct 2 0) (= (Ax<r>-25 0) (Ax<r>-24 0)))
  722. (=> (distinct 2 1) (= (Ax<r>-25 1) (Ax<r>-24 1)))
  723. (=> (distinct 2 2) (= (Ax<r>-25 2) (Ax<r>-24 2)))
  724. (=> (distinct 2 3) (= (Ax<r>-25 3) (Ax<r>-24 3)))))
  725. (assert (= (Ax<o>-25 2) (* (A<o>-0 2 0) (x<o>-4 0))))
  726. (assert (and true (= (Ax<r>-25 2) (* (A<r>-0 2 0) (x<r>-4 0)))))
  727. (assert (= tmp<o>-40 (* (A<o>-0 2 1) (x<o>-4 1))))
  728. (assert (and true (= tmp<r>-40 (* (A<r>-0 2 1) (x<r>-4 1)))))
  729. (assert (and (=> (distinct 2 0) (= (Ax<o>-26 0) (Ax<o>-25 0)))
  730. (=> (distinct 2 1) (= (Ax<o>-26 1) (Ax<o>-25 1)))
  731. (=> (distinct 2 2) (= (Ax<o>-26 2) (Ax<o>-25 2)))
  732. (=> (distinct 2 3) (= (Ax<o>-26 3) (Ax<o>-25 3)))))
  733. (assert (and (=> (distinct 2 0) (= (Ax<r>-26 0) (Ax<r>-25 0)))
  734. (=> (distinct 2 1) (= (Ax<r>-26 1) (Ax<r>-25 1)))
  735. (=> (distinct 2 2) (= (Ax<r>-26 2) (Ax<r>-25 2)))
  736. (=> (distinct 2 3) (= (Ax<r>-26 3) (Ax<r>-25 3)))))
  737. (assert (= (Ax<o>-26 2) (+ (Ax<o>-25 0) tmp<o>-40)))
  738. (assert (and true (= (Ax<r>-26 2) (+ (Ax<r>-25 0) tmp<r>-40))))
  739. (assert (= tmp<o>-41 (* (A<o>-0 2 2) (x<o>-4 2))))
  740. (assert (and true (= tmp<r>-41 (* (A<r>-0 2 2) (x<r>-4 2)))))
  741. (assert (and (=> (distinct 2 0) (= (Ax<o>-27 0) (Ax<o>-26 0)))
  742. (=> (distinct 2 1) (= (Ax<o>-27 1) (Ax<o>-26 1)))
  743. (=> (distinct 2 2) (= (Ax<o>-27 2) (Ax<o>-26 2)))
  744. (=> (distinct 2 3) (= (Ax<o>-27 3) (Ax<o>-26 3)))))
  745. (assert (and (=> (distinct 2 0) (= (Ax<r>-27 0) (Ax<r>-26 0)))
  746. (=> (distinct 2 1) (= (Ax<r>-27 1) (Ax<r>-26 1)))
  747. (=> (distinct 2 2) (= (Ax<r>-27 2) (Ax<r>-26 2)))
  748. (=> (distinct 2 3) (= (Ax<r>-27 3) (Ax<r>-26 3)))))
  749. (assert (= (Ax<o>-27 2) (+ (Ax<o>-26 0) tmp<o>-41)))
  750. (assert (and true (= (Ax<r>-27 2) (+ (Ax<r>-26 0) tmp<r>-41))))
  751. (assert (= tmp<o>-42 (* (A<o>-0 2 3) (x<o>-4 3))))
  752. (assert (and true (= tmp<r>-42 (* (A<r>-0 2 3) (x<r>-4 3)))))
  753. (assert (and (=> (distinct 2 0) (= (Ax<o>-28 0) (Ax<o>-27 0)))
  754. (=> (distinct 2 1) (= (Ax<o>-28 1) (Ax<o>-27 1)))
  755. (=> (distinct 2 2) (= (Ax<o>-28 2) (Ax<o>-27 2)))
  756. (=> (distinct 2 3) (= (Ax<o>-28 3) (Ax<o>-27 3)))))
  757. (assert (and (=> (distinct 2 0) (= (Ax<r>-28 0) (Ax<r>-27 0)))
  758. (=> (distinct 2 1) (= (Ax<r>-28 1) (Ax<r>-27 1)))
  759. (=> (distinct 2 2) (= (Ax<r>-28 2) (Ax<r>-27 2)))
  760. (=> (distinct 2 3) (= (Ax<r>-28 3) (Ax<r>-27 3)))))
  761. (assert (= (Ax<o>-28 2) (+ (Ax<o>-27 0) tmp<o>-42)))
  762. (assert (and true (= (Ax<r>-28 2) (+ (Ax<r>-27 0) tmp<r>-42))))
  763. (assert (and (=> (distinct 3 0) (= (Ax<o>-29 0) (Ax<o>-28 0)))
  764. (=> (distinct 3 1) (= (Ax<o>-29 1) (Ax<o>-28 1)))
  765. (=> (distinct 3 2) (= (Ax<o>-29 2) (Ax<o>-28 2)))
  766. (=> (distinct 3 3) (= (Ax<o>-29 3) (Ax<o>-28 3)))))
  767. (assert (and (=> (distinct 3 0) (= (Ax<r>-29 0) (Ax<r>-28 0)))
  768. (=> (distinct 3 1) (= (Ax<r>-29 1) (Ax<r>-28 1)))
  769. (=> (distinct 3 2) (= (Ax<r>-29 2) (Ax<r>-28 2)))
  770. (=> (distinct 3 3) (= (Ax<r>-29 3) (Ax<r>-28 3)))))
  771. (assert (= (Ax<o>-29 3) (* (A<o>-0 3 0) (x<o>-4 0))))
  772. (assert (and true (= (Ax<r>-29 3) (* (A<r>-0 3 0) (x<r>-4 0)))))
  773. (assert (= tmp<o>-43 (* (A<o>-0 3 1) (x<o>-4 1))))
  774. (assert (and true (= tmp<r>-43 (* (A<r>-0 3 1) (x<r>-4 1)))))
  775. (assert (and (=> (distinct 3 0) (= (Ax<o>-30 0) (Ax<o>-29 0)))
  776. (=> (distinct 3 1) (= (Ax<o>-30 1) (Ax<o>-29 1)))
  777. (=> (distinct 3 2) (= (Ax<o>-30 2) (Ax<o>-29 2)))
  778. (=> (distinct 3 3) (= (Ax<o>-30 3) (Ax<o>-29 3)))))
  779. (assert (and (=> (distinct 3 0) (= (Ax<r>-30 0) (Ax<r>-29 0)))
  780. (=> (distinct 3 1) (= (Ax<r>-30 1) (Ax<r>-29 1)))
  781. (=> (distinct 3 2) (= (Ax<r>-30 2) (Ax<r>-29 2)))
  782. (=> (distinct 3 3) (= (Ax<r>-30 3) (Ax<r>-29 3)))))
  783. (assert (= (Ax<o>-30 3) (+ (Ax<o>-29 0) tmp<o>-43)))
  784. (assert (and true (= (Ax<r>-30 3) (+ (Ax<r>-29 0) tmp<r>-43))))
  785. (assert (= tmp<o>-44 (* (A<o>-0 3 2) (x<o>-4 2))))
  786. (assert (and true (= tmp<r>-44 (* (A<r>-0 3 2) (x<r>-4 2)))))
  787. (assert (and (=> (distinct 3 0) (= (Ax<o>-31 0) (Ax<o>-30 0)))
  788. (=> (distinct 3 1) (= (Ax<o>-31 1) (Ax<o>-30 1)))
  789. (=> (distinct 3 2) (= (Ax<o>-31 2) (Ax<o>-30 2)))
  790. (=> (distinct 3 3) (= (Ax<o>-31 3) (Ax<o>-30 3)))))
  791. (assert (and (=> (distinct 3 0) (= (Ax<r>-31 0) (Ax<r>-30 0)))
  792. (=> (distinct 3 1) (= (Ax<r>-31 1) (Ax<r>-30 1)))
  793. (=> (distinct 3 2) (= (Ax<r>-31 2) (Ax<r>-30 2)))
  794. (=> (distinct 3 3) (= (Ax<r>-31 3) (Ax<r>-30 3)))))
  795. (assert (= (Ax<o>-31 3) (+ (Ax<o>-30 0) tmp<o>-44)))
  796. (assert (and true (= (Ax<r>-31 3) (+ (Ax<r>-30 0) tmp<r>-44))))
  797. (assert (= tmp<o>-45 (* (A<o>-0 3 3) (x<o>-4 3))))
  798. (assert (and true (= tmp<r>-45 (* (A<r>-0 3 3) (x<r>-4 3)))))
  799. (assert (and (=> (distinct 3 0) (= (Ax<o>-32 0) (Ax<o>-31 0)))
  800. (=> (distinct 3 1) (= (Ax<o>-32 1) (Ax<o>-31 1)))
  801. (=> (distinct 3 2) (= (Ax<o>-32 2) (Ax<o>-31 2)))
  802. (=> (distinct 3 3) (= (Ax<o>-32 3) (Ax<o>-31 3)))))
  803. (assert (and (=> (distinct 3 0) (= (Ax<r>-32 0) (Ax<r>-31 0)))
  804. (=> (distinct 3 1) (= (Ax<r>-32 1) (Ax<r>-31 1)))
  805. (=> (distinct 3 2) (= (Ax<r>-32 2) (Ax<r>-31 2)))
  806. (=> (distinct 3 3) (= (Ax<r>-32 3) (Ax<r>-31 3)))))
  807. (assert (= (Ax<o>-32 3) (+ (Ax<o>-31 0) tmp<o>-45)))
  808. (assert (and true (= (Ax<r>-32 3) (+ (Ax<r>-31 0) tmp<r>-45))))
  809. (assert (and (=> (distinct 0 0) (= (bmAx<o>-1 0) (bmAx<o>-0 0)))
  810. (=> (distinct 0 1) (= (bmAx<o>-1 1) (bmAx<o>-0 1)))
  811. (=> (distinct 0 2) (= (bmAx<o>-1 2) (bmAx<o>-0 2)))
  812. (=> (distinct 0 3) (= (bmAx<o>-1 3) (bmAx<o>-0 3)))))
  813. (assert (and (=> (distinct 0 0) (= (bmAx<r>-1 0) (bmAx<r>-0 0)))
  814. (=> (distinct 0 1) (= (bmAx<r>-1 1) (bmAx<r>-0 1)))
  815. (=> (distinct 0 2) (= (bmAx<r>-1 2) (bmAx<r>-0 2)))
  816. (=> (distinct 0 3) (= (bmAx<r>-1 3) (bmAx<r>-0 3)))))
  817. (assert (= (bmAx<o>-1 0) (- (b<o>-0 0) (Ax<o>-32 0))))
  818. (assert (and true (= (bmAx<r>-1 0) (- (b<r>-0 0) (Ax<r>-32 0)))))
  819. (assert (and (=> (distinct 1 0) (= (bmAx<o>-2 0) (bmAx<o>-1 0)))
  820. (=> (distinct 1 1) (= (bmAx<o>-2 1) (bmAx<o>-1 1)))
  821. (=> (distinct 1 2) (= (bmAx<o>-2 2) (bmAx<o>-1 2)))
  822. (=> (distinct 1 3) (= (bmAx<o>-2 3) (bmAx<o>-1 3)))))
  823. (assert (and (=> (distinct 1 0) (= (bmAx<r>-2 0) (bmAx<r>-1 0)))
  824. (=> (distinct 1 1) (= (bmAx<r>-2 1) (bmAx<r>-1 1)))
  825. (=> (distinct 1 2) (= (bmAx<r>-2 2) (bmAx<r>-1 2)))
  826. (=> (distinct 1 3) (= (bmAx<r>-2 3) (bmAx<r>-1 3)))))
  827. (assert (= (bmAx<o>-2 1) (- (b<o>-0 1) (Ax<o>-32 1))))
  828. (assert (and true (= (bmAx<r>-2 1) (- (b<r>-0 1) (Ax<r>-32 1)))))
  829. (assert (and (=> (distinct 2 0) (= (bmAx<o>-3 0) (bmAx<o>-2 0)))
  830. (=> (distinct 2 1) (= (bmAx<o>-3 1) (bmAx<o>-2 1)))
  831. (=> (distinct 2 2) (= (bmAx<o>-3 2) (bmAx<o>-2 2)))
  832. (=> (distinct 2 3) (= (bmAx<o>-3 3) (bmAx<o>-2 3)))))
  833. (assert (and (=> (distinct 2 0) (= (bmAx<r>-3 0) (bmAx<r>-2 0)))
  834. (=> (distinct 2 1) (= (bmAx<r>-3 1) (bmAx<r>-2 1)))
  835. (=> (distinct 2 2) (= (bmAx<r>-3 2) (bmAx<r>-2 2)))
  836. (=> (distinct 2 3) (= (bmAx<r>-3 3) (bmAx<r>-2 3)))))
  837. (assert (= (bmAx<o>-3 2) (- (b<o>-0 2) (Ax<o>-32 2))))
  838. (assert (and true (= (bmAx<r>-3 2) (- (b<r>-0 2) (Ax<r>-32 2)))))
  839. (assert (and (=> (distinct 3 0) (= (bmAx<o>-4 0) (bmAx<o>-3 0)))
  840. (=> (distinct 3 1) (= (bmAx<o>-4 1) (bmAx<o>-3 1)))
  841. (=> (distinct 3 2) (= (bmAx<o>-4 2) (bmAx<o>-3 2)))
  842. (=> (distinct 3 3) (= (bmAx<o>-4 3) (bmAx<o>-3 3)))))
  843. (assert (and (=> (distinct 3 0) (= (bmAx<r>-4 0) (bmAx<r>-3 0)))
  844. (=> (distinct 3 1) (= (bmAx<r>-4 1) (bmAx<r>-3 1)))
  845. (=> (distinct 3 2) (= (bmAx<r>-4 2) (bmAx<r>-3 2)))
  846. (=> (distinct 3 3) (= (bmAx<r>-4 3) (bmAx<r>-3 3)))))
  847. (assert (= (bmAx<o>-4 3) (- (b<o>-0 3) (Ax<o>-32 3))))
  848. (assert (and true (= (bmAx<r>-4 3) (- (b<r>-0 3) (Ax<r>-32 3)))))
  849. (assert (let ((a!1 (=> (and (= (r<o>-8 0) (bmAx<o>-4 0))
  850. (= (r<o>-8 1) (bmAx<o>-4 1))
  851. (= (r<o>-8 2) (bmAx<o>-4 2))
  852. (= (r<o>-8 3) (bmAx<o>-4 3)))
  853. (and (= (r<r>-8 0) (bmAx<r>-4 0))
  854. (= (r<r>-8 1) (bmAx<r>-4 1))
  855. (= (r<r>-8 2) (bmAx<r>-4 2))
  856. (= (r<r>-8 3) (bmAx<r>-4 3))))))
  857. (not (and (= (A<o>-0 0 0) (A<r>-0 0 0))
  858. (= (A<o>-0 0 1) (A<r>-0 0 1))
  859. (= (A<o>-0 0 2) (A<r>-0 0 2))
  860. (= (A<o>-0 0 3) (A<r>-0 0 3))
  861. (= (A<o>-0 1 0) (A<r>-0 1 0))
  862. (= (A<o>-0 1 1) (A<r>-0 1 1))
  863. (= (A<o>-0 1 2) (A<r>-0 1 2))
  864. (= (A<o>-0 1 3) (A<r>-0 1 3))
  865. (= (A<o>-0 2 0) (A<r>-0 2 0))
  866. (= (A<o>-0 2 1) (A<r>-0 2 1))
  867. (= (A<o>-0 2 2) (A<r>-0 2 2))
  868. (= (A<o>-0 2 3) (A<r>-0 2 3))
  869. (= (A<o>-0 3 0) (A<r>-0 3 0))
  870. (= (A<o>-0 3 1) (A<r>-0 3 1))
  871. (= (A<o>-0 3 2) (A<r>-0 3 2))
  872. (= (A<o>-0 3 3) (A<r>-0 3 3))
  873. (= (r<o>-8 0) (r<r>-8 0))
  874. (= (r<o>-8 1) (r<r>-8 1))
  875. (= (r<o>-8 2) (r<r>-8 2))
  876. (= (r<o>-8 3) (r<r>-8 3))
  877. (= (x<o>-4 0) (x<r>-4 0))
  878. (= (x<o>-4 1) (x<r>-4 1))
  879. (= (x<o>-4 2) (x<r>-4 2))
  880. (= (x<o>-4 3) (x<r>-4 3))
  881. (= (b<o>-0 0) (b<r>-0 0))
  882. (= (b<o>-0 1) (b<r>-0 1))
  883. (= (b<o>-0 2) (b<r>-0 2))
  884. (= (b<o>-0 3) (b<r>-0 3))
  885. (= r_norm<o>-8 r_norm<r>-8)
  886. (= i<o>-2 i<r>-2)
  887. a!1))))
  888.  
  889.  
  890. (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!