TM: 0 B1R 0 D0L 0 C1R 0 F0R 0 C1L 0 A1L 0 E0L 0 G1L 0 A1L 0 B0R 0 C0R 0 E0R
tape / proofs; generated by unibb prover; 2010-Jul-24 05:55:24
0. A>
1. 1 B>
2. {1}2 C>
3. {1}2 <C 1
4. 1 <A {1}2
5. <D 0 {1}2
6. <E {0}2 {1}2
7. <A 1 {0}2 {1}2
8. 1 B> 1 {0}2 {1}2
9. 10 F> {0}2 {1}2
10. 1 {0}2 C> 0 {1}2
11. 1 {0}2 <C {1}3
12. 10 <C {1}4
13. 1 <C {1}5
14. <A {1}6
15. 1 B> {1}6
16. 10 F> {1}5
17. 1 {0}2 E> {1}4
18. 1 {0}3 B> {1}3
19. 1 {0}4 F> {1}2
20. 1 {0}5 E> 1
21. 1 {0}6 B>
22. 1 {0}6 1 C>
23. 1 {0}6 1 <C 1
24. 1 {0}6 <A {1}2
25. 1 {0}5 1 B> {1}2
26. 1 {0}5 10 F> 1
27. 1 {0}5 1 {0}2 E>
28. 1 {0}5 1 {0}2 <A 1
29. 1 {0}5 101 B> 1
30. 1 {0}5 {10}2 F>
31. 1 {0}5 {10}2 0 C>
32. 1 {0}5 {10}2 0 <C 1
33. 1 {0}5 {10}2 <C {1}2
34. 1 {0}5 101 <C {1}3
35. 1 {0}5 10 <A {1}4
36. 1 {0}5 {1}2 B> {1}4
37. 1 {0}5 {1}2 0 F> {1}3
38. 1 {0}5 {1}2 {0}2 E> {1}2
39. 1 {0}5 {1}2 {0}3 B> 1
40. 1 {0}5 {1}2 {0}4 F>
41. 1 {0}5 {1}2 {0}5 C>
42. 1 {0}5 {1}2 {0}5 <C 1
43. 1 {0}5 {1}2 {0}4 <C {1}2
44. 1 {0}5 {1}2 {0}3 <C {1}3 proof 1 added proof used
USING
proof 1:
0. 1
F {
0}
5:F {
1}
2:F {
0}
3:T|a - 1 <C {
1}
3:T|b + 1
max_repeat = 2
46. 1 {0}5 {1}2 <C {1}6
47. 1 {0}5 1 <A {1}7
48. 1 {0}5 <D 0 {1}7
49. 1 {0}4 <E {0}2 {1}7
50. 1 {0}3 <A 1 {0}2 {1}7
51. 1 {0}2 1 B> 1 {0}2 {1}7
52. 1 {0}2 10 F> {0}2 {1}7
53. {1 {0}2}2 C> 0 {1}7
54. {1 {0}2}2 <C {1}8
55. 1 {0}2 10 <C {1}9
56. 1 {0}2 1 <C {1}10
57. 1 {0}2 <A {1}11
58. 101 B> {1}11
59. {10}2 F> {1}10
60. {10}2 0 E> {1}9
61. {10}2 {0}2 B> {1}8
62. {10}2 {0}3 F> {1}7
63. {10}2 {0}4 E> {1}6
64. {10}2 {0}5 B> {1}5 proof 2 added proof used
USING
proof 2:
2. {
10}
2:F {
0}
5:T|a + 3 B> {
1}
5:T|b - 3
max_repeat = 1
66. {10}2 {0}9 F> 1
67. {10}2 {0}10 E>
68. {10}2 {0}10 <A 1
69. {10}2 {0}9 1 B> 1
70. {10}2 {0}9 10 F>
71. {10}2 {0}9 1 {0}2 C>
72. {10}2 {0}9 1 {0}2 <C 1
73. {10}2 {0}9 10 <C {1}2
74. {10}2 {0}9 1 <C {1}3
75. {10}2 {0}9 <A {1}4
76. {10}2 {0}8 1 B> {1}4
77. {10}2 {0}8 10 F> {1}3
78. {10}2 {0}8 1 {0}2 E> {1}2
79. {10}2 {0}8 1 {0}3 B> 1
80. {10}2 {0}8 1 {0}4 F>
81. {10}2 {0}8 1 {0}5 C>
82. {10}2 {0}8 1 {0}5 <C 1
83. {10}2 {0}8 1 {0}4 <C {1}2 proof used
USING
proof 1:
0. 1
F {
0}
5:F {
1}
2:F {
0}
3:T|a - 1 <C {
1}
3:T|b + 1
max_repeat = 3
85. {10}2 {0}8 1 <C {1}6
86. {10}2 {0}8 <A {1}7
87. {10}2 {0}7 1 B> {1}7
88. {10}2 {0}7 10 F> {1}6
89. {10}2 {0}7 1 {0}2 E> {1}5
90. {10}2 {0}7 1 {0}3 B> {1}4 proof used
USING
proof 2:
2. {
10}
2:F {
0}
5:T|a + 3 B> {
1}
5:T|b - 3
max_repeat = 1
92. {10}2 {0}7 1 {0}7 F> proof 3 added proof used
USING
proof 3:
11. {
10}
2:F {
0}
7:T|b - 1 1
T {
0}
7:T|a + 3 F>
max_repeat = 6
XMOD
a + -1 / 3
7 + -1 / 3
OK
94. {10}2 {0}1 1 {0}26 C>
95. {10}2 {0}1 1 {0}26 <C 1
96. {10}2 {0}1 1 {0}25 <C {1}2 proof used
USING
proof 1:
0. 1
F {
0}
5:F {
1}
2:F {
0}
3:T|a - 1 <C {
1}
3:T|b + 1
max_repeat = 24
98. {10}2 {0}1 1 <C {1}27
99. {10}2 {0}1 <A {1}28
100. {10}2 1 B> {1}28
101. {10}3 F> {1}27
102. {10}3 0 E> {1}26
103. {10}3 {0}2 B> {1}25 proof used
USING
proof 2:
2. {
10}
2:F {
0}
5:T|a + 3 B> {
1}
5:T|b - 3
max_repeat = 8
105. {10}3 {0}27 F>
106. {10}3 {0}28 C>
107. {10}3 {0}28 <C 1
108. {10}3 {0}27 <C {1}2 proof used
USING
proof 1:
0. 1
F {
0}
5:F {
1}
2:F {
0}
3:T|a - 1 <C {
1}
3:T|b + 1
max_repeat = 26
110. {10}3 <C {1}29
111. {10}2 1 <C {1}30
112. {10}2 <A {1}31
113. 10 {1}2 B> {1}31
114. 10 {1}2 0 F> {1}30
115. 10 {1}2 {0}2 E> {1}29
116. 10 {1}2 {0}3 B> {1}28 proof used
USING
proof 2:
2. {
10}
2:F {
0}
5:T|a + 3 B> {
1}
5:T|b - 3
max_repeat = 9
118. 10 {1}2 {0}31 F>
119. 10 {1}2 {0}32 C>
120. 10 {1}2 {0}32 <C 1
121. 10 {1}2 {0}31 <C {1}2 proof used
USING
proof 1:
0. 1
F {
0}
5:F {
1}
2:F {
0}
3:T|a - 1 <C {
1}
3:T|b + 1
max_repeat = 30
123. 10 {1}2 <C {1}33
124. 101 <A {1}34
125. 10 <D 0 {1}34
126. 1 <E {0}2 {1}34
127. 0 B> {0}2 {1}34
128. 01 C> 0 {1}34
129. 01 <C {1}35
130. 0 <A {1}36
131. 1 B> {1}36
132. 10 F> {1}35
133. 1 {0}2 E> {1}34
134. 1 {0}3 B> {1}33 proof used
USING
proof 2:
2. {
10}
2:F {
0}
5:T|a + 3 B> {
1}
5:T|b - 3
max_repeat = 10
136. 1 {0}34 F> {1}2
137. 1 {0}35 E> 1
138. 1 {0}36 B>
139. 1 {0}36 1 C>
140. 1 {0}36 1 <C 1
141. 1 {0}36 <A {1}2
142. 1 {0}35 1 B> {1}2
143. 1 {0}35 10 F> 1
144. 1 {0}35 1 {0}2 E>
145. 1 {0}35 1 {0}2 <A 1
146. 1 {0}35 101 B> 1
147. 1 {0}35 {10}2 F>
148. 1 {0}35 {10}2 0 C>
149. 1 {0}35 {10}2 0 <C 1
150. 1 {0}35 {10}2 <C {1}2
151. 1 {0}35 101 <C {1}3
152. 1 {0}35 10 <A {1}4
153. 1 {0}35 {1}2 B> {1}4
154. 1 {0}35 {1}2 0 F> {1}3
155. 1 {0}35 {1}2 {0}2 E> {1}2
156. 1 {0}35 {1}2 {0}3 B> 1
157. 1 {0}35 {1}2 {0}4 F>
158. 1 {0}35 {1}2 {0}5 C>
159. 1 {0}35 {1}2 {0}5 <C 1
160. 1 {0}35 {1}2 {0}4 <C {1}2 proof used
USING
proof 1:
0. 1
F {
0}
5:F {
1}
2:F {
0}
3:T|a - 1 <C {
1}
3:T|b + 1
max_repeat = 3
162. 1 {0}35 {1}2 <C {1}6
163. 1 {0}35 1 <A {1}7
164. 1 {0}35 <D 0 {1}7
165. 1 {0}34 <E {0}2 {1}7
166. 1 {0}33 <A 1 {0}2 {1}7
167. 1 {0}32 1 B> 1 {0}2 {1}7
168. 1 {0}32 10 F> {0}2 {1}7
169. 1 {0}32 1 {0}2 C> 0 {1}7
170. 1 {0}32 1 {0}2 <C {1}8 proof used
USING
proof 1:
0. 1
F {
0}
5:F {
1}
2:F {
0}
3:T|a - 1 <C {
1}
3:T|b + 1
max_repeat = 1
172. 1 {0}32 1 <C {1}10
173. 1 {0}32 <A {1}11
174. 1 {0}31 1 B> {1}11
175. 1 {0}31 10 F> {1}10
176. 1 {0}31 1 {0}2 E> {1}9
177. 1 {0}31 1 {0}3 B> {1}8 proof used
USING
proof 2:
2. {
10}
2:F {
0}
5:T|a + 3 B> {
1}
5:T|b - 3
max_repeat = 2
179. 1 {0}31 1 {0}10 F> 1
180. 1 {0}31 1 {0}11 E>
181. 1 {0}31 1 {0}11 <A 1
182. 1 {0}31 1 {0}10 1 B> 1
183. 1 {0}31 1 {0}10 10 F>
184. 1 {0}31 1 {0}10 1 {0}2 C>
185. 1 {0}31 1 {0}10 1 {0}2 <C 1
186. 1 {0}31 1 {0}10 10 <C {1}2
187. 1 {0}31 1 {0}10 1 <C {1}3
188. 1 {0}31 1 {0}10 <A {1}4
189. 1 {0}31 1 {0}9 1 B> {1}4
190. 1 {0}31 1 {0}9 10 F> {1}3
191. 1 {0}31 1 {0}9 1 {0}2 E> {1}2
192. 1 {0}31 1 {0}9 1 {0}3 B> 1
193. 1 {0}31 1 {0}9 1 {0}4 F> proof used
USING
proof 3:
11. {
10}
2:F {
0}
7:T|b - 1 1
T {
0}
7:T|a + 3 F>
max_repeat = 8
XMOD
a + -1 / 3
4 + -1 / 3
OK
195. 1 {0}31 1 {0}1 1 {0}29 C>
196. 1 {0}31 1 {0}1 1 {0}29 <C 1
197. 1 {0}31 1 {0}1 1 {0}28 <C {1}2 proof used
USING
proof 1:
0. 1
F {
0}
5:F {
1}
2:F {
0}
3:T|a - 1 <C {
1}
3:T|b + 1
max_repeat = 27
199. 1 {0}31 1 {0}1 1 <C {1}30
200. 1 {0}31 1 {0}1 <A {1}31
201. 1 {0}31 {1}2 B> {1}31
202. 1 {0}31 {1}2 0 F> {1}30
203. 1 {0}31 {1}2 {0}2 E> {1}29
204. 1 {0}31 {1}2 {0}3 B> {1}28 proof used
USING
proof 2:
2. {
10}
2:F {
0}
5:T|a + 3 B> {
1}
5:T|b - 3
max_repeat = 9
206. 1 {0}31 {1}2 {0}31 F> proof 4 added proof used
USING
proof 4:
48. 1
F {
0}
31:T|b - 4 {
1}
2:T {
0}
31:T|a + 4 * 3 + 7 F>
max_repeat = 1
XMOD
a + 2 / 3
31 + 2 / 3
OK
XMOD
a + 4 * 3 + 3 / 3
31 + 4 * 3 + 3 / 3
OK
XVAR:
a + 4 * 3 + 7
31 + 4 * 3 + 7 = 112
XVAR:
b - 4
31 - 4 = 27
USING
proof 4:
48. 1
F {
0}
31:T|b - 4 {
1}
2:T {
0}
31:T|a + 4 * 3 + 7 F>
max_repeat = 1
XMOD
a + 2 / 3
112 + 2 / 3
OK
XMOD
a + 4 * 3 + 3 / 3
112 + 4 * 3 + 3 / 3
OK
XVAR:
a + 4 * 3 + 7
112 + 4 * 3 + 7 = 355
XVAR:
b - 4
27 - 4 = 23
USING
proof 4:
48. 1
F {
0}
31:T|b - 4 {
1}
2:T {
0}
31:T|a + 4 * 3 + 7 F>
max_repeat = 1
XMOD
a + 2 / 3
355 + 2 / 3
OK
XMOD
a + 4 * 3 + 3 / 3
355 + 4 * 3 + 3 / 3
OK
XVAR:
a + 4 * 3 + 7
355 + 4 * 3 + 7 = 1084
XVAR:
b - 4
23 - 4 = 19
USING
proof 4:
48. 1
F {
0}
31:T|b - 4 {
1}
2:T {
0}
31:T|a + 4 * 3 + 7 F>
max_repeat = 1
XMOD
a + 2 / 3
1084 + 2 / 3
OK
XMOD
a + 4 * 3 + 3 / 3
1084 + 4 * 3 + 3 / 3
OK
XVAR:
a + 4 * 3 + 7
1084 + 4 * 3 + 7 = 3271
XVAR:
b - 4
19 - 4 = 15
USING
proof 4:
48. 1
F {
0}
31:T|b - 4 {
1}
2:T {
0}
31:T|a + 4 * 3 + 7 F>
max_repeat = 1
XMOD
a + 2 / 3
3271 + 2 / 3
OK
XMOD
a + 4 * 3 + 3 / 3
3271 + 4 * 3 + 3 / 3
OK
XVAR:
a + 4 * 3 + 7
3271 + 4 * 3 + 7 = 9832
XVAR:
b - 4
15 - 4 = 11
USING
proof 4:
48. 1
F {
0}
31:T|b - 4 {
1}
2:T {
0}
31:T|a + 4 * 3 + 7 F>
max_repeat = 1
XMOD
a + 2 / 3
9832 + 2 / 3
OK
XMOD
a + 4 * 3 + 3 / 3
9832 + 4 * 3 + 3 / 3
OK
XVAR:
a + 4 * 3 + 7
9832 + 4 * 3 + 7 = 29515
XVAR:
b - 4
11 - 4 = 7
USING
proof 4:
48. 1
F {
0}
31:T|b - 4 {
1}
2:T {
0}
31:T|a + 4 * 3 + 7 F>
max_repeat = 1
XMOD
a + 2 / 3
29515 + 2 / 3
OK
XMOD
a + 4 * 3 + 3 / 3
29515 + 4 * 3 + 3 / 3
OK
XVAR:
a + 4 * 3 + 7
29515 + 4 * 3 + 7 = 88564
XVAR:
b - 4
7 - 4 = 3
214. 1 {0}3 {1}2 {0}88565 C>
215. 1 {0}3 {1}2 {0}88565 <C 1
216. 1 {0}3 {1}2 {0}88564 <C {1}2 proof used
USING
proof 1:
0. 1
F {
0}
5:F {
1}
2:F {
0}
3:T|a - 1 <C {
1}
3:T|b + 1
max_repeat = 88563
218. 1 {0}3 {1}2 <C {1}88566
219. 1 {0}3 1 <A {1}88567
220. 1 {0}3 <D 0 {1}88567
221. 1 {0}2 <E {0}2 {1}88567
222. 10 <A 1 {0}2 {1}88567
223. {1}2 B> 1 {0}2 {1}88567
224. {1}2 0 F> {0}2 {1}88567
225. {1}2 {0}2 C> 0 {1}88567
226. {1}2 {0}2 <C {1}88568 proof used
USING
proof 1:
0. 1
F {
0}
5:F {
1}
2:F {
0}
3:T|a - 1 <C {
1}
3:T|b + 1
max_repeat = 1
228. {1}2 <C {1}88570
229. 1 <A {1}88571
230. <D 0 {1}88571
231. <E {0}2 {1}88571
232. <A 1 {0}2 {1}88571
233. 1 B> 1 {0}2 {1}88571
234. 10 F> {0}2 {1}88571
235. 1 {0}2 C> 0 {1}88571
236. 1 {0}2 <C {1}88572 proof used
USING
proof 1:
0. 1
F {
0}
5:F {
1}
2:F {
0}
3:T|a - 1 <C {
1}
3:T|b + 1
max_repeat = 1
238. 1 <C {1}88574
239. <A {1}88575
240. 1 B> {1}88575
241. 10 F> {1}88574
242. 1 {0}2 E> {1}88573
243. 1 {0}3 B> {1}88572 proof used
USING
proof 2:
2. {
10}
2:F {
0}
5:T|a + 3 B> {
1}
5:T|b - 3
max_repeat = 29523
245. 1 {0}88573 F> {1}2
246. 1 {0}88574 E> 1
247. 1 {0}88575 B>
248. 1 {0}88575 1 C>
249. 1 {0}88575 1 <C 1
250. 1 {0}88575 <A {1}2
251. 1 {0}88574 1 B> {1}2
252. 1 {0}88574 10 F> 1
253. 1 {0}88574 1 {0}2 E>
254. 1 {0}88574 1 {0}2 <A 1
255. 1 {0}88574 101 B> 1
256. 1 {0}88574 {10}2 F>
257. 1 {0}88574 {10}2 0 C>
258. 1 {0}88574 {10}2 0 <C 1
259. 1 {0}88574 {10}2 <C {1}2
260. 1 {0}88574 101 <C {1}3
261. 1 {0}88574 10 <A {1}4
262. 1 {0}88574 {1}2 B> {1}4
263. 1 {0}88574 {1}2 0 F> {1}3
264. 1 {0}88574 {1}2 {0}2 E> {1}2
265. 1 {0}88574 {1}2 {0}3 B> 1
266. 1 {0}88574 {1}2 {0}4 F> proof used
USING
proof 4:
48. 1
F {
0}
31:T|b - 4 {
1}
2:T {
0}
31:T|a + 4 * 3 + 7 F>
max_repeat = 1
XMOD
a + 2 / 3
4 + 2 / 3
OK
XMOD
a + 4 * 3 + 3 / 3
4 + 4 * 3 + 3 / 3
OK
XVAR:
a + 4 * 3 + 7
4 + 4 * 3 + 7 = 31
XVAR:
b - 4
88574 - 4 = 88570
USING
proof 4:
48. 1
F {
0}
31:T|b - 4 {
1}
2:T {
0}
31:T|a + 4 * 3 + 7 F>
max_repeat = 1
XMOD
a + 2 / 3
31 + 2 / 3
OK
XMOD
a + 4 * 3 + 3 / 3
31 + 4 * 3 + 3 / 3
OK
XVAR:
a + 4 * 3 + 7
31 + 4 * 3 + 7 = 112
XVAR:
b - 4
88570 - 4 = 88566
. . .
22407. 1 {0}10 {1}2 {0}0.1180414448044852868290706e10566 F> proof used
USING
proof 4:
48. 1
F {
0}
31:T|b - 4 {
1}
2:T {
0}
31:T|a + 4 * 3 + 7 F>
max_repeat = 1
XMOD
a + 2 / 3
0.1180414448044852868290706e10566 + 2 / 3
OK
XMOD
a + 4 * 3 + 3 / 3
0.1180414448044852868290706e10566 + 4 * 3 + 3 / 3
OK
XVAR:
a + 4 * 3 + 7
0.1180414448044852868290706e10566 + 4 * 3 + 7 = 0.3541243344134558604872117e10566
XVAR:
b - 4
10 - 4 = 6
USING
proof 4:
48. 1
F {
0}
31:T|b - 4 {
1}
2:T {
0}
31:T|a + 4 * 3 + 7 F>
max_repeat = 1
XMOD
a + 2 / 3
0.3541243344134558604872117e10566 + 2 / 3
OK
XMOD
a + 4 * 3 + 3 / 3
0.3541243344134558604872117e10566 + 4 * 3 + 3 / 3
OK
XVAR:
a + 4 * 3 + 7
0.3541243344134558604872117e10566 + 4 * 3 + 7 = 0.1062373003240367581461635e10567
XVAR:
b - 4
6 - 4 = 2
22410. 1 {0}2 {1}2 {0}0.1062373003240367581461635e10567 C>
22411. 1 {0}2 {1}2 {0}0.1062373003240367581461635e10567 <C 1
22412. 1 {0}2 {1}2 {0}0.1062373003240367581461635e10567 <C {1}2 proof used
USING
proof 1:
0. 1
F {
0}
5:F {
1}
2:F {
0}
3:T|a - 1 <C {
1}
3:T|b + 1
max_repeat = 0.1062373003240367581461635e10567
22414. 1 {0}2 {1}2 <C {1}0.1062373003240367581461635e10567
22415. 1 {0}2 1 <A {1}0.1062373003240367581461635e10567
22416. 1 {0}2 <D 0 {1}0.1062373003240367581461635e10567
22417. 10 <E {0}2 {1}0.1062373003240367581461635e10567
22418. 1 <A 1 {0}2 {1}0.1062373003240367581461635e10567
22419. <D 01 {0}2 {1}0.1062373003240367581461635e10567
22420. <E {0}2 1 {0}2 {1}0.1062373003240367581461635e10567
22421. <A {1 {0}2}2 {1}0.1062373003240367581461635e10567
22422. 1 B> {1 {0}2}2 {1}0.1062373003240367581461635e10567
22423. 10 F> {0}2 1 {0}2 {1}0.1062373003240367581461635e10567
22424. 1 {0}2 C> 01 {0}2 {1}0.1062373003240367581461635e10567
22425. 1 {0}2 <C {1}2 {0}2 {1}0.1062373003240367581461635e10567
22426. 10 <C {1}3 {0}2 {1}0.1062373003240367581461635e10567
22427. 1 <C {1}4 {0}2 {1}0.1062373003240367581461635e10567
22428. <A {1}5 {0}2 {1}0.1062373003240367581461635e10567
22429. 1 B> {1}5 {0}2 {1}0.1062373003240367581461635e10567
22430. 10 F> {1}4 {0}2 {1}0.1062373003240367581461635e10567
22431. 1 {0}2 E> {1}3 {0}2 {1}0.1062373003240367581461635e10567
22432. 1 {0}3 B> {1}2 {0}2 {1}0.1062373003240367581461635e10567
22433. 1 {0}4 F> 1 {0}2 {1}0.1062373003240367581461635e10567
22434. 1 {0}5 E> {0}2 {1}0.1062373003240367581461635e10567
22435. 1 {0}5 <A 10 {1}0.1062373003240367581461635e10567
22436. 1 {0}4 1 B> 10 {1}0.1062373003240367581461635e10567
22437. 1 {0}4 10 F> 0 {1}0.1062373003240367581461635e10567
22438. 1 {0}4 1 {0}2 C> {1}0.1062373003240367581461635e10567
22439. 1 {0}4 1 {0}2 <A {1}0.1062373003240367581461635e10567
22440. 1 {0}4 101 B> {1}0.1062373003240367581461635e10567
22441. 1 {0}4 {10}2 F> {1}0.1062373003240367581461635e10567
22442. 1 {0}4 {10}2 0 E> {1}0.1062373003240367581461635e10567
22443. 1 {0}4 {10}2 {0}2 B> {1}0.1062373003240367581461635e10567 proof used
USING
proof 2:
2. {
10}
2:F {
0}
5:T|a + 3 B> {
1}
5:T|b - 3
max_repeat = 0.3541243344134558604872117e10566
22445. 1 {0}4 {10}2 {0}0.1062373003240367581461635e10567 F>
22446. 1 {0}4 {10}2 {0}0.1062373003240367581461635e10567 C>
22447. 1 {0}4 {10}2 {0}0.1062373003240367581461635e10567 <C 1
22448. 1 {0}4 {10}2 {0}0.1062373003240367581461635e10567 <C {1}2 proof used
USING
proof 1:
0. 1
F {
0}
5:F {
1}
2:F {
0}
3:T|a - 1 <C {
1}
3:T|b + 1
max_repeat = 0.1062373003240367581461635e10567
22450. 1 {0}4 {10}2 <C {1}0.1062373003240367581461635e10567
22451. 1 {0}4 101 <C {1}0.1062373003240367581461635e10567
22452. 1 {0}4 10 <A {1}0.1062373003240367581461635e10567
22453. 1 {0}4 {1}2 B> {1}0.1062373003240367581461635e10567
22454. 1 {0}4 {1}2 0 F> {1}0.1062373003240367581461635e10567
22455. 1 {0}4 {1}2 {0}2 E> {1}0.1062373003240367581461635e10567
22456. 1 {0}4 {1}2 {0}3 B> {1}0.1062373003240367581461635e10567 proof used
USING
proof 2:
2. {
10}
2:F {
0}
5:T|a + 3 B> {
1}
5:T|b - 3
max_repeat = 0.3541243344134558604872117e10566
22458. 1 {0}4 {1}2 {0}0.1062373003240367581461635e10567 F>
22459. 1 {0}4 {1}2 {0}0.1062373003240367581461635e10567 C>
22460. 1 {0}4 {1}2 {0}0.1062373003240367581461635e10567 <C 1
22461. 1 {0}4 {1}2 {0}0.1062373003240367581461635e10567 <C {1}2 proof used
USING
proof 1:
0. 1
F {
0}
5:F {
1}
2:F {
0}
3:T|a - 1 <C {
1}
3:T|b + 1
max_repeat = 0.1062373003240367581461635e10567
22463. 1 {0}4 {1}2 <C {1}0.1062373003240367581461635e10567
22464. 1 {0}4 1 <A {1}0.1062373003240367581461635e10567
22465. 1 {0}4 <D 0 {1}0.1062373003240367581461635e10567
22466. 1 {0}3 <E {0}2 {1}0.1062373003240367581461635e10567
22467. 1 {0}2 <A 1 {0}2 {1}0.1062373003240367581461635e10567
22468. 101 B> 1 {0}2 {1}0.1062373003240367581461635e10567
22469. {10}2 F> {0}2 {1}0.1062373003240367581461635e10567
22470. {10}2 0 C> 0 {1}0.1062373003240367581461635e10567
22471. {10}2 0 <C {1}0.1062373003240367581461635e10567
22472. {10}2 <C {1}0.1062373003240367581461635e10567
22473. 101 <C {1}0.1062373003240367581461635e10567
22474. 10 <A {1}0.1062373003240367581461635e10567
22475. {1}2 B> {1}0.1062373003240367581461635e10567
22476. {1}2 0 F> {1}0.1062373003240367581461635e10567
22477. {1}2 {0}2 E> {1}0.1062373003240367581461635e10567
22478. {1}2 {0}3 B> {1}0.1062373003240367581461635e10567 proof used
USING
proof 2:
2. {
10}
2:F {
0}
5:T|a + 3 B> {
1}
5:T|b - 3
max_repeat = 0.3541243344134558604872117e10566
22480. {1}2 {0}0.1062373003240367581461635e10567 F> 1
22481. {1}2 {0}0.1062373003240367581461635e10567 E>
22482. {1}2 {0}0.1062373003240367581461635e10567 <A 1
22483. {1}2 {0}0.1062373003240367581461635e10567 1 B> 1
22484. {1}2 {0}0.1062373003240367581461635e10567 10 F>
22485. {1}2 {0}0.1062373003240367581461635e10567 1 {0}2 C>
22486. {1}2 {0}0.1062373003240367581461635e10567 1 {0}2 <C 1
22487. {1}2 {0}0.1062373003240367581461635e10567 10 <C {1}2
22488. {1}2 {0}0.1062373003240367581461635e10567 1 <C {1}3
22489. {1}2 {0}0.1062373003240367581461635e10567 <A {1}4
22490. {1}2 {0}0.1062373003240367581461635e10567 1 B> {1}4
22491. {1}2 {0}0.1062373003240367581461635e10567 10 F> {1}3
22492. {1}2 {0}0.1062373003240367581461635e10567 1 {0}2 E> {1}2
22493. {1}2 {0}0.1062373003240367581461635e10567 1 {0}3 B> 1
22494. {1}2 {0}0.1062373003240367581461635e10567 1 {0}4 F> proof used
USING
proof 3:
11. {
10}
2:F {
0}
7:T|b - 1 1
T {
0}
7:T|a + 3 F>
max_repeat = 0.1062373003240367581461635e10567
XMOD
a + -1 / 3
4 + -1 / 3
OK
22496. {1}2 {0}1 1 {0}0.3187119009721102744384905e10567 C>
22497. {1}2 {0}1 1 {0}0.3187119009721102744384905e10567 <C 1
22498. {1}2 {0}1 1 {0}0.3187119009721102744384905e10567 <C {1}2 proof used
USING
proof 1:
0. 1
F {
0}
5:F {
1}
2:F {
0}
3:T|a - 1 <C {
1}
3:T|b + 1
max_repeat = 0.3187119009721102744384905e10567
22500. {1}2 {0}1 1 <C {1}0.3187119009721102744384905e10567
22501. {1}2 {0}1 <A {1}0.3187119009721102744384905e10567
22502. {1}3 B> {1}0.3187119009721102744384905e10567
22503. {1}3 0 F> {1}0.3187119009721102744384905e10567
22504. {1}3 {0}2 E> {1}0.3187119009721102744384905e10567
22505. {1}3 {0}3 B> {1}0.3187119009721102744384905e10567 proof used
USING
proof 2:
2. {
10}
2:F {
0}
5:T|a + 3 B> {
1}
5:T|b - 3
max_repeat = 0.1062373003240367581461635e10567
22507. {1}3 {0}0.3187119009721102744384905e10567 F>
22508. {1}3 {0}0.3187119009721102744384905e10567 C>
22509. {1}3 {0}0.3187119009721102744384905e10567 <C 1
22510. {1}3 {0}0.3187119009721102744384905e10567 <C {1}2 proof used
USING
proof 1:
0. 1
F {
0}
5:F {
1}
2:F {
0}
3:T|a - 1 <C {
1}
3:T|b + 1
max_repeat = 0.3187119009721102744384905e10567
22512. {1}3 <C {1}0.3187119009721102744384905e10567
22513. {1}2 <A {1}0.3187119009721102744384905e10567
22514. 1 <D 0 {1}0.3187119009721102744384905e10567
22515. <G 10 {1}0.3187119009721102744384905e10567
halt state...