Comment: This TM produces >1.383x10^7036 nonzeros in >1.025x10^14072 steps. Comment: This is the currently best known 4x3 TM
| State | on 0 |
on 1 |
on 2 |
on 0 | on 1 | on 2 | ||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Move | Goto | Move | Goto | Move | Goto | |||||||
| A | 1RB | 1RH | 2RC | 1 | right | B | 1 | right | H | 2 | right | C |
| B | 2LC | 2RD | 0LC | 2 | left | C | 2 | right | D | 0 | left | C |
| C | 1RA | 2RB | 0LB | 1 | right | A | 2 | right | B | 0 | left | B |
| D | 1LB | 0LD | 2RC | 1 | left | B | 0 | left | D | 2 | right | C |
The same TM just simple.
The same TM with repetitions reduced.
The same TM with tape symbol exponents.
The same TM as 2-bck-macro machine.
Simulation is done as 2-bck-macro machine with pure additive config-TRs.
Pushing initial machine.
Pushing macro factor 2.
Pushing BCK machine.
Steps BasSteps BasTpos Tape contents
0 0 0 (00)A>
1 10 2 12 (11)B>
2 17 -1 12 <C(01)
3 21 -3 <C(01) 01
4 24 0 01 (12)D> 01
5 29 -3 01 <B(02) 11
6 36 0 11 (22)C> 11
7 38 2 11 22 (22)D>
8 41 -1 11 22 <B(00) 10
9 43 -3 11 <B(00) 00 10
10 49 -5 <B(02) 10 00 10
11 54 -2 12 (12)C> 10 00 10
12 61 -5 12 <B(02) 02 00 10
13 65 -7 <B(02) 022 00 10
14 70 -4 12 (12)C> 022 00 10
15 74 0 123 (12)C> 00 10
16 76 2 124 (11)B> 10
17 85 -1 124 <C(01) 21
18 101 -9 <C(01) 014 21
19 104 -6 01 (12)D> 014 21
20 109 -9 01 <B(02) 11 013 21
21 116 -6 11 (22)C> 11 013 21
22 118 -4 11 22 (22)D> 013 21
23 121 -7 11 22 <B(00) 11 012 21
24 123 -9 11 <B(00) 00 11 012 21
25 129 -11 <B(02) 10 00 11 012 21
26 134 -8 12 (12)C> 10 00 11 012 21
27 141 -11 12 <B(02) 02 00 11 012 21
28 145 -13 <B(02) 022 00 11 012 21
29 150 -10 12 (12)C> 022 00 11 012 21
30 154 -6 123 (12)C> 00 11 012 21
31 156 -4 124 (11)B> 11 012 21
32 160 -2 124 11 (21)A> 012 21
33 162 0 124 11 21 (12)D> 01 21
34 167 -3 124 11 21 <B(02) 11 21
35 171 -5 124 11 <B(00) 12 11 21
36 177 -7 124 <B(02) 10 12 11 21
37 193 -15 <B(02) 024 10 12 11 21
38 198 -12 12 (12)C> 024 10 12 11 21
39 206 -4 125 (12)C> 10 12 11 21
40 213 -7 125 <B(02) 02 12 11 21
41 233 -17 <B(02) 026 12 11 21
42 238 -14 12 (12)C> 026 12 11 21
43 250 -2 127 (12)C> 12 11 21
44 257 -5 127 <B(02) 00 11 21
45 285 -19 <B(02) 027 00 11 21
46 290 -16 12 (12)C> 027 00 11 21
47 304 -2 128 (12)C> 00 11 21
48 306 0 129 (11)B> 11 21
49 310 2 129 11 (21)A> 21
50 312 4 129 11 21 (22)B>
51 315 1 129 11 21 <C(00) 20
52 319 -1 129 11 <C(00) 202
53 325 -3 129 <C(01) 203
54 361 -21 <C(01) 019 203
55 364 -18 01 (12)D> 019 203
56 369 -21 01 <B(02) 11 018 203
57 376 -18 11 (22)C> 11 018 203
58 378 -16 11 22 (22)D> 018 203
59 381 -19 11 22 <B(00) 11 017 203
60 383 -21 11 <B(00) 00 11 017 203
61 389 -23 <B(02) 10 00 11 017 203
62 394 -20 12 (12)C> 10 00 11 017 203
63 401 -23 12 <B(02) 02 00 11 017 203
64 405 -25 <B(02) 022 00 11 017 203
65 410 -22 12 (12)C> 022 00 11 017 203
66 414 -18 123 (12)C> 00 11 017 203
67 416 -16 124 (11)B> 11 017 203
68 420 -14 124 11 (21)A> 017 203
69 422 -12 124 11 21 (12)D> 016 203
70 427 -15 124 11 21 <B(02) 11 015 203
71 431 -17 124 11 <B(00) 12 11 015 203
72 437 -19 124 <B(02) 10 12 11 015 203
73 453 -27 <B(02) 024 10 12 11 015 203
74 458 -24 12 (12)C> 024 10 12 11 015 203
75 466 -16 125 (12)C> 10 12 11 015 203
76 473 -19 125 <B(02) 02 12 11 015 203
77 493 -29 <B(02) 026 12 11 015 203
78 498 -26 12 (12)C> 026 12 11 015 203
79 510 -14 127 (12)C> 12 11 015 203
80 517 -17 127 <B(02) 00 11 015 203
81 545 -31 <B(02) 027 00 11 015 203
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <B(02) 021+V(2) 00 11 013+V(1) [*]*
1 5 3 12 (12)C> 021+V(2) 00 11 013+V(1) [*]*
2 7+2*V(2) 5+2*V(2) 122+V(2) (12)C> 00 11 013+V(1) [*]*
3 9+2*V(2) 7+2*V(2) 123+V(2) (11)B> 11 013+V(1) [*]*
4 13+2*V(2) 9+2*V(2) 123+V(2) 11 (21)A> 013+V(1) [*]*
5 15+2*V(2) 11+2*V(2) 123+V(2) 11 21 (12)D> 012+V(1) [*]*
6 20+2*V(2) 8+2*V(2) 123+V(2) 11 21 <B(02) 11 011+V(1) [*]*
7 24+2*V(2) 6+2*V(2) 123+V(2) 11 <B(00) 12 11 011+V(1) [*]*
8 30+2*V(2) 4+2*V(2) 123+V(2) <B(02) 10 12 11 011+V(1) [*]*
9 42+6*V(2) -2 <B(02) 023+V(2) 10 12 11 011+V(1) [*]*
10 47+6*V(2) 1 12 (12)C> 023+V(2) 10 12 11 011+V(1) [*]*
11 53+8*V(2) 7+2*V(2) 124+V(2) (12)C> 10 12 11 011+V(1) [*]*
12 60+8*V(2) 4+2*V(2) 124+V(2) <B(02) 02 12 11 011+V(1) [*]*
13 76+12*V(2) -4 <B(02) 025+V(2) 12 11 011+V(1) [*]*
14 81+12*V(2) -1 12 (12)C> 025+V(2) 12 11 011+V(1) [*]*
15 91+14*V(2) 9+2*V(2) 126+V(2) (12)C> 12 11 011+V(1) [*]*
16 98+14*V(2) 6+2*V(2) 126+V(2) <B(02) 00 11 011+V(1) [*]*
17 122+18*V(2) -6 <B(02) 026+V(2) 00 11 011+V(1) [*]*
<< Success! ==> defined new CTR 1 (PA)
81 545 -31 <B(02) 027 00 11 015 203
== Executing PA-CTR 1, V(1)=2, V(2)=6, repcount=2, factor=5/2
115 1095 -43 <B(02) 0217 00 11 01 203
116 1100 -40 12 (12)C> 0217 00 11 01 203
117 1134 -6 1218 (12)C> 00 11 01 203
118 1136 -4 1219 (11)B> 11 01 203
119 1140 -2 1219 11 (21)A> 01 203
120 1142 0 1219 11 21 (12)D> 203
121 1144 2 1219 11 21 12 (21)A> 202
122 1148 6 1219 11 21 12 212 (21)A>
123 1157 3 1219 11 21 12 212 <B(00) 10
124 1165 -1 1219 11 21 12 <B(00) 103
125 1169 -3 1219 11 21 <B(02) 00 103
126 1173 -5 1219 11 <B(00) 12 00 103
127 1179 -7 1219 <B(02) 10 12 00 103
128 1255 -45 <B(02) 0219 10 12 00 103
129 1260 -42 12 (12)C> 0219 10 12 00 103
130 1298 -4 1220 (12)C> 10 12 00 103
131 1305 -7 1220 <B(02) 02 12 00 103
132 1385 -47 <B(02) 0221 12 00 103
133 1390 -44 12 (12)C> 0221 12 00 103
134 1432 -2 1222 (12)C> 12 00 103
135 1439 -5 1222 <B(02) 002 103
136 1527 -49 <B(02) 0222 002 103
137 1532 -46 12 (12)C> 0222 002 103
138 1576 -2 1223 (12)C> 002 103
139 1578 0 1224 (11)B> 00 103
140 1585 -3 1224 <C(01) 00 103
141 1681 -51 <C(01) 0124 00 103
142 1684 -48 01 (12)D> 0124 00 103
143 1689 -51 01 <B(02) 11 0123 00 103
144 1696 -48 11 (22)C> 11 0123 00 103
145 1698 -46 11 22 (22)D> 0123 00 103
146 1701 -49 11 22 <B(00) 11 0122 00 103
147 1703 -51 11 <B(00) 00 11 0122 00 103
148 1709 -53 <B(02) 10 00 11 0122 00 103
149 1714 -50 12 (12)C> 10 00 11 0122 00 103
150 1721 -53 12 <B(02) 02 00 11 0122 00 103
151 1725 -55 <B(02) 022 00 11 0122 00 103
152 1730 -52 12 (12)C> 022 00 11 0122 00 103
153 1734 -48 123 (12)C> 00 11 0122 00 103
154 1736 -46 124 (11)B> 11 0122 00 103
155 1740 -44 124 11 (21)A> 0122 00 103
156 1742 -42 124 11 21 (12)D> 0121 00 103
157 1747 -45 124 11 21 <B(02) 11 0120 00 103
158 1751 -47 124 11 <B(00) 12 11 0120 00 103
159 1757 -49 124 <B(02) 10 12 11 0120 00 103
160 1773 -57 <B(02) 024 10 12 11 0120 00 103
161 1778 -54 12 (12)C> 024 10 12 11 0120 00 103
162 1786 -46 125 (12)C> 10 12 11 0120 00 103
163 1793 -49 125 <B(02) 02 12 11 0120 00 103
164 1813 -59 <B(02) 026 12 11 0120 00 103
165 1818 -56 12 (12)C> 026 12 11 0120 00 103
166 1830 -44 127 (12)C> 12 11 0120 00 103
167 1837 -47 127 <B(02) 00 11 0120 00 103
168 1865 -61 <B(02) 027 00 11 0120 00 103
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <B(02) 021+V(2) 00 11 013+V(1) [*]* [*]*
1 5 3 12 (12)C> 021+V(2) 00 11 013+V(1) [*]* [*]*
2 7+2*V(2) 5+2*V(2) 122+V(2) (12)C> 00 11 013+V(1) [*]* [*]*
3 9+2*V(2) 7+2*V(2) 123+V(2) (11)B> 11 013+V(1) [*]* [*]*
4 13+2*V(2) 9+2*V(2) 123+V(2) 11 (21)A> 013+V(1) [*]* [*]*
5 15+2*V(2) 11+2*V(2) 123+V(2) 11 21 (12)D> 012+V(1) [*]* [*]*
6 20+2*V(2) 8+2*V(2) 123+V(2) 11 21 <B(02) 11 011+V(1) [*]* [*]*
7 24+2*V(2) 6+2*V(2) 123+V(2) 11 <B(00) 12 11 011+V(1) [*]* [*]*
8 30+2*V(2) 4+2*V(2) 123+V(2) <B(02) 10 12 11 011+V(1) [*]* [*]*
9 42+6*V(2) -2 <B(02) 023+V(2) 10 12 11 011+V(1) [*]* [*]*
10 47+6*V(2) 1 12 (12)C> 023+V(2) 10 12 11 011+V(1) [*]* [*]*
11 53+8*V(2) 7+2*V(2) 124+V(2) (12)C> 10 12 11 011+V(1) [*]* [*]*
12 60+8*V(2) 4+2*V(2) 124+V(2) <B(02) 02 12 11 011+V(1) [*]* [*]*
13 76+12*V(2) -4 <B(02) 025+V(2) 12 11 011+V(1) [*]* [*]*
14 81+12*V(2) -1 12 (12)C> 025+V(2) 12 11 011+V(1) [*]* [*]*
15 91+14*V(2) 9+2*V(2) 126+V(2) (12)C> 12 11 011+V(1) [*]* [*]*
16 98+14*V(2) 6+2*V(2) 126+V(2) <B(02) 00 11 011+V(1) [*]* [*]*
17 122+18*V(2) -6 <B(02) 026+V(2) 00 11 011+V(1) [*]* [*]*
<< Success! ==> defined new CTR 2 (PA)
168 1865 -61 <B(02) 027 00 11 0120 00 103
== Executing PA-CTR 2, V(1)=17, V(2)=6, repcount=9, factor=5/2
321 7175 -115 <B(02) 0252 00 11 012 00 103
322 7180 -112 12 (12)C> 0252 00 11 012 00 103
323 7284 -8 1253 (12)C> 00 11 012 00 103
324 7286 -6 1254 (11)B> 11 012 00 103
325 7290 -4 1254 11 (21)A> 012 00 103
326 7292 -2 1254 11 21 (12)D> 01 00 103
327 7297 -5 1254 11 21 <B(02) 11 00 103
328 7301 -7 1254 11 <B(00) 12 11 00 103
329 7307 -9 1254 <B(02) 10 12 11 00 103
330 7523 -117 <B(02) 0254 10 12 11 00 103
331 7528 -114 12 (12)C> 0254 10 12 11 00 103
332 7636 -6 1255 (12)C> 10 12 11 00 103
333 7643 -9 1255 <B(02) 02 12 11 00 103
334 7863 -119 <B(02) 0256 12 11 00 103
335 7868 -116 12 (12)C> 0256 12 11 00 103
336 7980 -4 1257 (12)C> 12 11 00 103
337 7987 -7 1257 <B(02) 00 11 00 103
338 8215 -121 <B(02) 0257 00 11 00 103
339 8220 -118 12 (12)C> 0257 00 11 00 103
340 8334 -4 1258 (12)C> 00 11 00 103
341 8336 -2 1259 (11)B> 11 00 103
342 8340 0 1259 11 (21)A> 00 103
343 8349 -3 1259 11 <B(00) 104
344 8355 -5 1259 <B(02) 105
345 8591 -123 <B(02) 0259 105
346 8596 -120 12 (12)C> 0259 105
347 8714 -2 1260 (12)C> 105
348 8721 -5 1260 <B(02) 02 104
349 8961 -125 <B(02) 0261 104
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <B(02) 021+V(2) 102+V(1)
1 5 3 12 (12)C> 021+V(2) 102+V(1)
2 7+2*V(2) 5+2*V(2) 122+V(2) (12)C> 102+V(1)
3 14+2*V(2) 2+2*V(2) 122+V(2) <B(02) 02 101+V(1)
4 22+6*V(2) -2 <B(02) 023+V(2) 101+V(1)
<< Success! ==> defined new CTR 3 (PA)
349 8961 -125 <B(02) 0261 104
== Executing PA-CTR 3, V(1)=2, V(2)=60, repcount=3, factor=2/1
361 10143 -131 <B(02) 0267 10
362 10148 -128 12 (12)C> 0267 10
363 10282 6 1268 (12)C> 10
364 10289 3 1268 <B(02) 02
365 10561 -133 <B(02) 0269
366 10566 -130 12 (12)C> 0269
367 10704 8 1270 (12)C>
368 10706 10 1271 (11)B>
369 10713 7 1271 <C(01)
370 10997 -135 <C(01) 0171
371 11000 -132 01 (12)D> 0171
372 11005 -135 01 <B(02) 11 0170
373 11012 -132 11 (22)C> 11 0170
374 11014 -130 11 22 (22)D> 0170
375 11017 -133 11 22 <B(00) 11 0169
376 11019 -135 11 <B(00) 00 11 0169
377 11025 -137 <B(02) 10 00 11 0169
378 11030 -134 12 (12)C> 10 00 11 0169
379 11037 -137 12 <B(02) 02 00 11 0169
380 11041 -139 <B(02) 022 00 11 0169
381 11046 -136 12 (12)C> 022 00 11 0169
382 11050 -132 123 (12)C> 00 11 0169
383 11052 -130 124 (11)B> 11 0169
384 11056 -128 124 11 (21)A> 0169
385 11058 -126 124 11 21 (12)D> 0168
386 11063 -129 124 11 21 <B(02) 11 0167
387 11067 -131 124 11 <B(00) 12 11 0167
388 11073 -133 124 <B(02) 10 12 11 0167
389 11089 -141 <B(02) 024 10 12 11 0167
390 11094 -138 12 (12)C> 024 10 12 11 0167
391 11102 -130 125 (12)C> 10 12 11 0167
392 11109 -133 125 <B(02) 02 12 11 0167
393 11129 -143 <B(02) 026 12 11 0167
394 11134 -140 12 (12)C> 026 12 11 0167
395 11146 -128 127 (12)C> 12 11 0167
396 11153 -131 127 <B(02) 00 11 0167
397 11181 -145 <B(02) 027 00 11 0167
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <B(02) 021+V(2) 00 11 013+V(1)
1 5 3 12 (12)C> 021+V(2) 00 11 013+V(1)
2 7+2*V(2) 5+2*V(2) 122+V(2) (12)C> 00 11 013+V(1)
3 9+2*V(2) 7+2*V(2) 123+V(2) (11)B> 11 013+V(1)
4 13+2*V(2) 9+2*V(2) 123+V(2) 11 (21)A> 013+V(1)
5 15+2*V(2) 11+2*V(2) 123+V(2) 11 21 (12)D> 012+V(1)
6 20+2*V(2) 8+2*V(2) 123+V(2) 11 21 <B(02) 11 011+V(1)
7 24+2*V(2) 6+2*V(2) 123+V(2) 11 <B(00) 12 11 011+V(1)
8 30+2*V(2) 4+2*V(2) 123+V(2) <B(02) 10 12 11 011+V(1)
9 42+6*V(2) -2 <B(02) 023+V(2) 10 12 11 011+V(1)
10 47+6*V(2) 1 12 (12)C> 023+V(2) 10 12 11 011+V(1)
11 53+8*V(2) 7+2*V(2) 124+V(2) (12)C> 10 12 11 011+V(1)
12 60+8*V(2) 4+2*V(2) 124+V(2) <B(02) 02 12 11 011+V(1)
13 76+12*V(2) -4 <B(02) 025+V(2) 12 11 011+V(1)
14 81+12*V(2) -1 12 (12)C> 025+V(2) 12 11 011+V(1)
15 91+14*V(2) 9+2*V(2) 126+V(2) (12)C> 12 11 011+V(1)
16 98+14*V(2) 6+2*V(2) 126+V(2) <B(02) 00 11 011+V(1)
17 122+18*V(2) -6 <B(02) 026+V(2) 00 11 011+V(1)
<< Success! ==> defined new CTR 4 (PA)
397 11181 -145 <B(02) 027 00 11 0167
== Executing PA-CTR 4, V(1)=64, V(2)=6, repcount=33, factor=5/2
958 66291 -343 <B(02) 02172 00 11 01
959 66296 -340 12 (12)C> 02172 00 11 01
960 66640 4 12173 (12)C> 00 11 01
961 66642 6 12174 (11)B> 11 01
962 66646 8 12174 11 (21)A> 01
963 66648 10 12174 11 21 (12)D>
964 66653 7 12174 11 21 <B(02) 10
965 66657 5 12174 11 <B(00) 12 10
966 66663 3 12174 <B(02) 10 12 10
967 67359 -345 <B(02) 02174 10 12 10
968 67364 -342 12 (12)C> 02174 10 12 10
969 67712 6 12175 (12)C> 10 12 10
970 67719 3 12175 <B(02) 02 12 10
971 68419 -347 <B(02) 02176 12 10
972 68424 -344 12 (12)C> 02176 12 10
973 68776 8 12177 (12)C> 12 10
974 68783 5 12177 <B(02) 00 10
975 69491 -349 <B(02) 02177 00 10
976 69496 -346 12 (12)C> 02177 00 10
977 69850 8 12178 (12)C> 00 10
978 69852 10 12179 (11)B> 10
979 69861 7 12179 <C(01) 21
980 70577 -351 <C(01) 01179 21
981 70580 -348 01 (12)D> 01179 21
982 70585 -351 01 <B(02) 11 01178 21
983 70592 -348 11 (22)C> 11 01178 21
984 70594 -346 11 22 (22)D> 01178 21
985 70597 -349 11 22 <B(00) 11 01177 21
986 70599 -351 11 <B(00) 00 11 01177 21
987 70605 -353 <B(02) 10 00 11 01177 21
988 70610 -350 12 (12)C> 10 00 11 01177 21
989 70617 -353 12 <B(02) 02 00 11 01177 21
990 70621 -355 <B(02) 022 00 11 01177 21
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <B(02) 021+V(1) 00 11 01
1 5 3 12 (12)C> 021+V(1) 00 11 01
2 7+2*V(1) 5+2*V(1) 122+V(1) (12)C> 00 11 01
3 9+2*V(1) 7+2*V(1) 123+V(1) (11)B> 11 01
4 13+2*V(1) 9+2*V(1) 123+V(1) 11 (21)A> 01
5 15+2*V(1) 11+2*V(1) 123+V(1) 11 21 (12)D>
6 20+2*V(1) 8+2*V(1) 123+V(1) 11 21 <B(02) 10
7 24+2*V(1) 6+2*V(1) 123+V(1) 11 <B(00) 12 10
8 30+2*V(1) 4+2*V(1) 123+V(1) <B(02) 10 12 10
9 42+6*V(1) -2 <B(02) 023+V(1) 10 12 10
10 47+6*V(1) 1 12 (12)C> 023+V(1) 10 12 10
11 53+8*V(1) 7+2*V(1) 124+V(1) (12)C> 10 12 10
12 60+8*V(1) 4+2*V(1) 124+V(1) <B(02) 02 12 10
13 76+12*V(1) -4 <B(02) 025+V(1) 12 10
14 81+12*V(1) -1 12 (12)C> 025+V(1) 12 10
15 91+14*V(1) 9+2*V(1) 126+V(1) (12)C> 12 10
16 98+14*V(1) 6+2*V(1) 126+V(1) <B(02) 00 10
17 122+18*V(1) -6 <B(02) 026+V(1) 00 10
18 127+18*V(1) -3 12 (12)C> 026+V(1) 00 10
19 139+20*V(1) 9+2*V(1) 127+V(1) (12)C> 00 10
20 141+20*V(1) 11+2*V(1) 128+V(1) (11)B> 10
21 150+20*V(1) 8+2*V(1) 128+V(1) <C(01) 21
22 182+24*V(1) -8 <C(01) 018+V(1) 21
23 185+24*V(1) -5 01 (12)D> 018+V(1) 21
24 190+24*V(1) -8 01 <B(02) 11 017+V(1) 21
25 197+24*V(1) -5 11 (22)C> 11 017+V(1) 21
26 199+24*V(1) -3 11 22 (22)D> 017+V(1) 21
27 202+24*V(1) -6 11 22 <B(00) 11 016+V(1) 21
28 204+24*V(1) -8 11 <B(00) 00 11 016+V(1) 21
29 210+24*V(1) -10 <B(02) 10 00 11 016+V(1) 21
30 215+24*V(1) -7 12 (12)C> 10 00 11 016+V(1) 21
31 222+24*V(1) -10 12 <B(02) 02 00 11 016+V(1) 21
32 226+24*V(1) -12 <B(02) 022 00 11 016+V(1) 21
<< Success! ==> defined new CTR 5 (PPA)
990 70621 -355 <B(02) 022 00 11 01177 21
== Executing PA-CTR 1, V(1)=174, V(2)=1, repcount=88, factor=5/2
2486 427461 -883 <B(02) 02442 00 11 01 21
2487 427466 -880 12 (12)C> 02442 00 11 01 21
2488 428350 4 12443 (12)C> 00 11 01 21
2489 428352 6 12444 (11)B> 11 01 21
2490 428356 8 12444 11 (21)A> 01 21
2491 428358 10 12444 11 21 (12)D> 21
2492 428360 12 12444 11 21 12 (22)B>
2493 428363 9 12444 11 21 12 <C(00) 20
2494 428367 7 12444 11 21 <C(01) 00 20
2495 428371 5 12444 11 <C(00) 21 00 20
2496 428377 3 12444 <C(01) 20 21 00 20
2497 430153 -885 <C(01) 01444 20 21 00 20
2498 430156 -882 01 (12)D> 01444 20 21 00 20
2499 430161 -885 01 <B(02) 11 01443 20 21 00 20
2500 430168 -882 11 (22)C> 11 01443 20 21 00 20
2501 430170 -880 11 22 (22)D> 01443 20 21 00 20
2502 430173 -883 11 22 <B(00) 11 01442 20 21 00 20
2503 430175 -885 11 <B(00) 00 11 01442 20 21 00 20
2504 430181 -887 <B(02) 10 00 11 01442 20 21 00 20
2505 430186 -884 12 (12)C> 10 00 11 01442 20 21 00 20
2506 430193 -887 12 <B(02) 02 00 11 01442 20 21 00 20
2507 430197 -889 <B(02) 022 00 11 01442 20 21 00 20
2508 430202 -886 12 (12)C> 022 00 11 01442 20 21 00 20
2509 430206 -882 123 (12)C> 00 11 01442 20 21 00 20
2510 430208 -880 124 (11)B> 11 01442 20 21 00 20
2511 430212 -878 124 11 (21)A> 01442 20 21 00 20
2512 430214 -876 124 11 21 (12)D> 01441 20 21 00 20
2513 430219 -879 124 11 21 <B(02) 11 01440 20 21 00 20
2514 430223 -881 124 11 <B(00) 12 11 01440 20 21 00 20
2515 430229 -883 124 <B(02) 10 12 11 01440 20 21 00 20
2516 430245 -891 <B(02) 024 10 12 11 01440 20 21 00 20
2517 430250 -888 12 (12)C> 024 10 12 11 01440 20 21 00 20
2518 430258 -880 125 (12)C> 10 12 11 01440 20 21 00 20
2519 430265 -883 125 <B(02) 02 12 11 01440 20 21 00 20
2520 430285 -893 <B(02) 026 12 11 01440 20 21 00 20
2521 430290 -890 12 (12)C> 026 12 11 01440 20 21 00 20
2522 430302 -878 127 (12)C> 12 11 01440 20 21 00 20
2523 430309 -881 127 <B(02) 00 11 01440 20 21 00 20
2524 430337 -895 <B(02) 027 00 11 01440 20 21 00 20
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <B(02) 021+V(2) 00 11 013+V(1) [*]* [*]* [*]* [*]*
1 5 3 12 (12)C> 021+V(2) 00 11 013+V(1) [*]* [*]* [*]* [*]*
2 7+2*V(2) 5+2*V(2) 122+V(2) (12)C> 00 11 013+V(1) [*]* [*]* [*]* [*]*
3 9+2*V(2) 7+2*V(2) 123+V(2) (11)B> 11 013+V(1) [*]* [*]* [*]* [*]*
4 13+2*V(2) 9+2*V(2) 123+V(2) 11 (21)A> 013+V(1) [*]* [*]* [*]* [*]*
5 15+2*V(2) 11+2*V(2) 123+V(2) 11 21 (12)D> 012+V(1) [*]* [*]* [*]* [*]*
6 20+2*V(2) 8+2*V(2) 123+V(2) 11 21 <B(02) 11 011+V(1) [*]* [*]* [*]* [*]*
7 24+2*V(2) 6+2*V(2) 123+V(2) 11 <B(00) 12 11 011+V(1) [*]* [*]* [*]* [*]*
8 30+2*V(2) 4+2*V(2) 123+V(2) <B(02) 10 12 11 011+V(1) [*]* [*]* [*]* [*]*
9 42+6*V(2) -2 <B(02) 023+V(2) 10 12 11 011+V(1) [*]* [*]* [*]* [*]*
10 47+6*V(2) 1 12 (12)C> 023+V(2) 10 12 11 011+V(1) [*]* [*]* [*]* [*]*
11 53+8*V(2) 7+2*V(2) 124+V(2) (12)C> 10 12 11 011+V(1) [*]* [*]* [*]* [*]*
12 60+8*V(2) 4+2*V(2) 124+V(2) <B(02) 02 12 11 011+V(1) [*]* [*]* [*]* [*]*
13 76+12*V(2) -4 <B(02) 025+V(2) 12 11 011+V(1) [*]* [*]* [*]* [*]*
14 81+12*V(2) -1 12 (12)C> 025+V(2) 12 11 011+V(1) [*]* [*]* [*]* [*]*
15 91+14*V(2) 9+2*V(2) 126+V(2) (12)C> 12 11 011+V(1) [*]* [*]* [*]* [*]*
16 98+14*V(2) 6+2*V(2) 126+V(2) <B(02) 00 11 011+V(1) [*]* [*]* [*]* [*]*
17 122+18*V(2) -6 <B(02) 026+V(2) 00 11 011+V(1) [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 6 (PA)
2524 430337 -895 <B(02) 027 00 11 01440 20 21 00 20
== Executing PA-CTR 6, V(1)=437, V(2)=6, repcount=219, factor=5/2
6247 2629097 -2209 <B(02) 021102 00 11 012 20 21 00 20
6248 2629102 -2206 12 (12)C> 021102 00 11 012 20 21 00 20
6249 2631306 -2 121103 (12)C> 00 11 012 20 21 00 20
6250 2631308 0 121104 (11)B> 11 012 20 21 00 20
6251 2631312 2 121104 11 (21)A> 012 20 21 00 20
6252 2631314 4 121104 11 21 (12)D> 01 20 21 00 20
6253 2631319 1 121104 11 21 <B(02) 11 20 21 00 20
6254 2631323 -1 121104 11 <B(00) 12 11 20 21 00 20
6255 2631329 -3 121104 <B(02) 10 12 11 20 21 00 20
6256 2635745 -2211 <B(02) 021104 10 12 11 20 21 00 20
6257 2635750 -2208 12 (12)C> 021104 10 12 11 20 21 00 20
6258 2637958 0 121105 (12)C> 10 12 11 20 21 00 20
6259 2637965 -3 121105 <B(02) 02 12 11 20 21 00 20
6260 2642385 -2213 <B(02) 021106 12 11 20 21 00 20
6261 2642390 -2210 12 (12)C> 021106 12 11 20 21 00 20
6262 2644602 2 121107 (12)C> 12 11 20 21 00 20
6263 2644609 -1 121107 <B(02) 00 11 20 21 00 20
6264 2649037 -2215 <B(02) 021107 00 11 20 21 00 20
6265 2649042 -2212 12 (12)C> 021107 00 11 20 21 00 20
6266 2651256 2 121108 (12)C> 00 11 20 21 00 20
6267 2651258 4 121109 (11)B> 11 20 21 00 20
6268 2651262 6 121109 11 (21)A> 20 21 00 20
6269 2651264 8 121109 11 21 (21)A> 21 00 20
6270 2651266 10 121109 11 212 (22)B> 00 20
6271 2651269 7 121109 11 212 <C(00) 202
6272 2651277 3 121109 11 <C(00) 204
6273 2651283 1 121109 <C(01) 205
6274 2655719 -2217 <C(01) 011109 205
6275 2655722 -2214 01 (12)D> 011109 205
6276 2655727 -2217 01 <B(02) 11 011108 205
6277 2655734 -2214 11 (22)C> 11 011108 205
6278 2655736 -2212 11 22 (22)D> 011108 205
6279 2655739 -2215 11 22 <B(00) 11 011107 205
6280 2655741 -2217 11 <B(00) 00 11 011107 205
6281 2655747 -2219 <B(02) 10 00 11 011107 205
6282 2655752 -2216 12 (12)C> 10 00 11 011107 205
6283 2655759 -2219 12 <B(02) 02 00 11 011107 205
6284 2655763 -2221 <B(02) 022 00 11 011107 205
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 <B(02) 021+V(3) 00 11 012 201+V(2) 21 00 201+V(1)
1 5 3 12 (12)C> 021+V(3) 00 11 012 201+V(2) 21 00 201+V(1)
2 7+2*V(3) 5+2*V(3) 122+V(3) (12)C> 00 11 012 201+V(2) 21 00 201+V(1)
3 9+2*V(3) 7+2*V(3) 123+V(3) (11)B> 11 012 201+V(2) 21 00 201+V(1)
4 13+2*V(3) 9+2*V(3) 123+V(3) 11 (21)A> 012 201+V(2) 21 00 201+V(1)
5 15+2*V(3) 11+2*V(3) 123+V(3) 11 21 (12)D> 01 201+V(2) 21 00 201+V(1)
6 20+2*V(3) 8+2*V(3) 123+V(3) 11 21 <B(02) 11 201+V(2) 21 00 201+V(1)
7 24+2*V(3) 6+2*V(3) 123+V(3) 11 <B(00) 12 11 201+V(2) 21 00 201+V(1)
8 30+2*V(3) 4+2*V(3) 123+V(3) <B(02) 10 12 11 201+V(2) 21 00 201+V(1)
9 42+6*V(3) -2 <B(02) 023+V(3) 10 12 11 201+V(2) 21 00 201+V(1)
10 47+6*V(3) 1 12 (12)C> 023+V(3) 10 12 11 201+V(2) 21 00 201+V(1)
11 53+8*V(3) 7+2*V(3) 124+V(3) (12)C> 10 12 11 201+V(2) 21 00 201+V(1)
12 60+8*V(3) 4+2*V(3) 124+V(3) <B(02) 02 12 11 201+V(2) 21 00 201+V(1)
13 76+12*V(3) -4 <B(02) 025+V(3) 12 11 201+V(2) 21 00 201+V(1)
14 81+12*V(3) -1 12 (12)C> 025+V(3) 12 11 201+V(2) 21 00 201+V(1)
15 91+14*V(3) 9+2*V(3) 126+V(3) (12)C> 12 11 201+V(2) 21 00 201+V(1)
16 98+14*V(3) 6+2*V(3) 126+V(3) <B(02) 00 11 201+V(2) 21 00 201+V(1)
17 122+18*V(3) -6 <B(02) 026+V(3) 00 11 201+V(2) 21 00 201+V(1)
18 127+18*V(3) -3 12 (12)C> 026+V(3) 00 11 201+V(2) 21 00 201+V(1)
19 139+20*V(3) 9+2*V(3) 127+V(3) (12)C> 00 11 201+V(2) 21 00 201+V(1)
20 141+20*V(3) 11+2*V(3) 128+V(3) (11)B> 11 201+V(2) 21 00 201+V(1)
21 145+20*V(3) 13+2*V(3) 128+V(3) 11 (21)A> 201+V(2) 21 00 201+V(1)
22 147+2*V(2)+20*V(3) 15+2*V(2)+2*V(3) 128+V(3) 11 211+V(2) (21)A> 21 00 201+V(1)
23 149+2*V(2)+20*V(3) 17+2*V(2)+2*V(3) 128+V(3) 11 212+V(2) (22)B> 00 201+V(1)
24 152+2*V(2)+20*V(3) 14+2*V(2)+2*V(3) 128+V(3) 11 212+V(2) <C(00) 202+V(1)
25 160+6*V(2)+20*V(3) 10+2*V(3) 128+V(3) 11 <C(00) 204+V(1)+V(2)
26 166+6*V(2)+20*V(3) 8+2*V(3) 128+V(3) <C(01) 205+V(1)+V(2)
27 198+6*V(2)+24*V(3) -8 <C(01) 018+V(3) 205+V(1)+V(2)
28 201+6*V(2)+24*V(3) -5 01 (12)D> 018+V(3) 205+V(1)+V(2)
29 206+6*V(2)+24*V(3) -8 01 <B(02) 11 017+V(3) 205+V(1)+V(2)
30 213+6*V(2)+24*V(3) -5 11 (22)C> 11 017+V(3) 205+V(1)+V(2)
31 215+6*V(2)+24*V(3) -3 11 22 (22)D> 017+V(3) 205+V(1)+V(2)
32 218+6*V(2)+24*V(3) -6 11 22 <B(00) 11 016+V(3) 205+V(1)+V(2)
33 220+6*V(2)+24*V(3) -8 11 <B(00) 00 11 016+V(3) 205+V(1)+V(2)
34 226+6*V(2)+24*V(3) -10 <B(02) 10 00 11 016+V(3) 205+V(1)+V(2)
35 231+6*V(2)+24*V(3) -7 12 (12)C> 10 00 11 016+V(3) 205+V(1)+V(2)
36 238+6*V(2)+24*V(3) -10 12 <B(02) 02 00 11 016+V(3) 205+V(1)+V(2)
37 242+6*V(2)+24*V(3) -12 <B(02) 022 00 11 016+V(3) 205+V(1)+V(2)
<< Success! ==> defined new CTR 7 (PPA)
6284 2655763 -2221 <B(02) 022 00 11 011107 205
== Executing PA-CTR 1, V(1)=1104, V(2)=1, repcount=553, factor=5/2
15685 16469703 -5539 <B(02) 022767 00 11 01 205
15686 16469708 -5536 12 (12)C> 022767 00 11 01 205
15687 16475242 -2 122768 (12)C> 00 11 01 205
15688 16475244 0 122769 (11)B> 11 01 205
15689 16475248 2 122769 11 (21)A> 01 205
15690 16475250 4 122769 11 21 (12)D> 205
15691 16475252 6 122769 11 21 12 (21)A> 204
15692 16475260 14 122769 11 21 12 214 (21)A>
15693 16475269 11 122769 11 21 12 214 <B(00) 10
15694 16475285 3 122769 11 21 12 <B(00) 105
15695 16475289 1 122769 11 21 <B(02) 00 105
15696 16475293 -1 122769 11 <B(00) 12 00 105
15697 16475299 -3 122769 <B(02) 10 12 00 105
15698 16486375 -5541 <B(02) 022769 10 12 00 105
15699 16486380 -5538 12 (12)C> 022769 10 12 00 105
15700 16491918 0 122770 (12)C> 10 12 00 105
15701 16491925 -3 122770 <B(02) 02 12 00 105
15702 16503005 -5543 <B(02) 022771 12 00 105
15703 16503010 -5540 12 (12)C> 022771 12 00 105
15704 16508552 2 122772 (12)C> 12 00 105
15705 16508559 -1 122772 <B(02) 002 105
15706 16519647 -5545 <B(02) 022772 002 105
15707 16519652 -5542 12 (12)C> 022772 002 105
15708 16525196 2 122773 (12)C> 002 105
15709 16525198 4 122774 (11)B> 00 105
15710 16525205 1 122774 <C(01) 00 105
15711 16536301 -5547 <C(01) 012774 00 105
15712 16536304 -5544 01 (12)D> 012774 00 105
15713 16536309 -5547 01 <B(02) 11 012773 00 105
15714 16536316 -5544 11 (22)C> 11 012773 00 105
15715 16536318 -5542 11 22 (22)D> 012773 00 105
15716 16536321 -5545 11 22 <B(00) 11 012772 00 105
15717 16536323 -5547 11 <B(00) 00 11 012772 00 105
15718 16536329 -5549 <B(02) 10 00 11 012772 00 105
15719 16536334 -5546 12 (12)C> 10 00 11 012772 00 105
15720 16536341 -5549 12 <B(02) 02 00 11 012772 00 105
15721 16536345 -5551 <B(02) 022 00 11 012772 00 105
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <B(02) 021+V(2) 00 11 01 202+V(1)
1 5 3 12 (12)C> 021+V(2) 00 11 01 202+V(1)
2 7+2*V(2) 5+2*V(2) 122+V(2) (12)C> 00 11 01 202+V(1)
3 9+2*V(2) 7+2*V(2) 123+V(2) (11)B> 11 01 202+V(1)
4 13+2*V(2) 9+2*V(2) 123+V(2) 11 (21)A> 01 202+V(1)
5 15+2*V(2) 11+2*V(2) 123+V(2) 11 21 (12)D> 202+V(1)
6 17+2*V(2) 13+2*V(2) 123+V(2) 11 21 12 (21)A> 201+V(1)
7 19+2*V(1)+2*V(2) 15+2*V(1)+2*V(2) 123+V(2) 11 21 12 211+V(1) (21)A>
8 28+2*V(1)+2*V(2) 12+2*V(1)+2*V(2) 123+V(2) 11 21 12 211+V(1) <B(00) 10
9 32+6*V(1)+2*V(2) 10+2*V(2) 123+V(2) 11 21 12 <B(00) 102+V(1)
10 36+6*V(1)+2*V(2) 8+2*V(2) 123+V(2) 11 21 <B(02) 00 102+V(1)
11 40+6*V(1)+2*V(2) 6+2*V(2) 123+V(2) 11 <B(00) 12 00 102+V(1)
12 46+6*V(1)+2*V(2) 4+2*V(2) 123+V(2) <B(02) 10 12 00 102+V(1)
13 58+6*V(1)+6*V(2) -2 <B(02) 023+V(2) 10 12 00 102+V(1)
14 63+6*V(1)+6*V(2) 1 12 (12)C> 023+V(2) 10 12 00 102+V(1)
15 69+6*V(1)+8*V(2) 7+2*V(2) 124+V(2) (12)C> 10 12 00 102+V(1)
16 76+6*V(1)+8*V(2) 4+2*V(2) 124+V(2) <B(02) 02 12 00 102+V(1)
17 92+6*V(1)+12*V(2) -4 <B(02) 025+V(2) 12 00 102+V(1)
18 97+6*V(1)+12*V(2) -1 12 (12)C> 025+V(2) 12 00 102+V(1)
19 107+6*V(1)+14*V(2) 9+2*V(2) 126+V(2) (12)C> 12 00 102+V(1)
20 114+6*V(1)+14*V(2) 6+2*V(2) 126+V(2) <B(02) 002 102+V(1)
21 138+6*V(1)+18*V(2) -6 <B(02) 026+V(2) 002 102+V(1)
22 143+6*V(1)+18*V(2) -3 12 (12)C> 026+V(2) 002 102+V(1)
23 155+6*V(1)+20*V(2) 9+2*V(2) 127+V(2) (12)C> 002 102+V(1)
24 157+6*V(1)+20*V(2) 11+2*V(2) 128+V(2) (11)B> 00 102+V(1)
25 164+6*V(1)+20*V(2) 8+2*V(2) 128+V(2) <C(01) 00 102+V(1)
26 196+6*V(1)+24*V(2) -8 <C(01) 018+V(2) 00 102+V(1)
27 199+6*V(1)+24*V(2) -5 01 (12)D> 018+V(2) 00 102+V(1)
28 204+6*V(1)+24*V(2) -8 01 <B(02) 11 017+V(2) 00 102+V(1)
29 211+6*V(1)+24*V(2) -5 11 (22)C> 11 017+V(2) 00 102+V(1)
30 213+6*V(1)+24*V(2) -3 11 22 (22)D> 017+V(2) 00 102+V(1)
31 216+6*V(1)+24*V(2) -6 11 22 <B(00) 11 016+V(2) 00 102+V(1)
32 218+6*V(1)+24*V(2) -8 11 <B(00) 00 11 016+V(2) 00 102+V(1)
33 224+6*V(1)+24*V(2) -10 <B(02) 10 00 11 016+V(2) 00 102+V(1)
34 229+6*V(1)+24*V(2) -7 12 (12)C> 10 00 11 016+V(2) 00 102+V(1)
35 236+6*V(1)+24*V(2) -10 12 <B(02) 02 00 11 016+V(2) 00 102+V(1)
36 240+6*V(1)+24*V(2) -12 <B(02) 022 00 11 016+V(2) 00 102+V(1)
<< Success! ==> defined new CTR 8 (PPA)
15721 16536345 -5551 <B(02) 022 00 11 012772 00 105
== Executing PA-CTR 2, V(1)=2769, V(2)=1, repcount=1385, factor=5/2
39266 102988045 -13861 <B(02) 026927 00 11 012 00 105
39267 102988050 -13858 12 (12)C> 026927 00 11 012 00 105
39268 103001904 -4 126928 (12)C> 00 11 012 00 105
39269 103001906 -2 126929 (11)B> 11 012 00 105
39270 103001910 0 126929 11 (21)A> 012 00 105
39271 103001912 2 126929 11 21 (12)D> 01 00 105
39272 103001917 -1 126929 11 21 <B(02) 11 00 105
39273 103001921 -3 126929 11 <B(00) 12 11 00 105
39274 103001927 -5 126929 <B(02) 10 12 11 00 105
39275 103029643 -13863 <B(02) 026929 10 12 11 00 105
39276 103029648 -13860 12 (12)C> 026929 10 12 11 00 105
39277 103043506 -2 126930 (12)C> 10 12 11 00 105
39278 103043513 -5 126930 <B(02) 02 12 11 00 105
39279 103071233 -13865 <B(02) 026931 12 11 00 105
39280 103071238 -13862 12 (12)C> 026931 12 11 00 105
39281 103085100 0 126932 (12)C> 12 11 00 105
39282 103085107 -3 126932 <B(02) 00 11 00 105
39283 103112835 -13867 <B(02) 026932 00 11 00 105
39284 103112840 -13864 12 (12)C> 026932 00 11 00 105
39285 103126704 0 126933 (12)C> 00 11 00 105
39286 103126706 2 126934 (11)B> 11 00 105
39287 103126710 4 126934 11 (21)A> 00 105
39288 103126719 1 126934 11 <B(00) 106
39289 103126725 -1 126934 <B(02) 107
39290 103154461 -13869 <B(02) 026934 107
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <B(02) 021+V(2) 00 11 012 00 101+V(1)
1 5 3 12 (12)C> 021+V(2) 00 11 012 00 101+V(1)
2 7+2*V(2) 5+2*V(2) 122+V(2) (12)C> 00 11 012 00 101+V(1)
3 9+2*V(2) 7+2*V(2) 123+V(2) (11)B> 11 012 00 101+V(1)
4 13+2*V(2) 9+2*V(2) 123+V(2) 11 (21)A> 012 00 101+V(1)
5 15+2*V(2) 11+2*V(2) 123+V(2) 11 21 (12)D> 01 00 101+V(1)
6 20+2*V(2) 8+2*V(2) 123+V(2) 11 21 <B(02) 11 00 101+V(1)
7 24+2*V(2) 6+2*V(2) 123+V(2) 11 <B(00) 12 11 00 101+V(1)
8 30+2*V(2) 4+2*V(2) 123+V(2) <B(02) 10 12 11 00 101+V(1)
9 42+6*V(2) -2 <B(02) 023+V(2) 10 12 11 00 101+V(1)
10 47+6*V(2) 1 12 (12)C> 023+V(2) 10 12 11 00 101+V(1)
11 53+8*V(2) 7+2*V(2) 124+V(2) (12)C> 10 12 11 00 101+V(1)
12 60+8*V(2) 4+2*V(2) 124+V(2) <B(02) 02 12 11 00 101+V(1)
13 76+12*V(2) -4 <B(02) 025+V(2) 12 11 00 101+V(1)
14 81+12*V(2) -1 12 (12)C> 025+V(2) 12 11 00 101+V(1)
15 91+14*V(2) 9+2*V(2) 126+V(2) (12)C> 12 11 00 101+V(1)
16 98+14*V(2) 6+2*V(2) 126+V(2) <B(02) 00 11 00 101+V(1)
17 122+18*V(2) -6 <B(02) 026+V(2) 00 11 00 101+V(1)
18 127+18*V(2) -3 12 (12)C> 026+V(2) 00 11 00 101+V(1)
19 139+20*V(2) 9+2*V(2) 127+V(2) (12)C> 00 11 00 101+V(1)
20 141+20*V(2) 11+2*V(2) 128+V(2) (11)B> 11 00 101+V(1)
21 145+20*V(2) 13+2*V(2) 128+V(2) 11 (21)A> 00 101+V(1)
22 154+20*V(2) 10+2*V(2) 128+V(2) 11 <B(00) 102+V(1)
23 160+20*V(2) 8+2*V(2) 128+V(2) <B(02) 103+V(1)
24 192+24*V(2) -8 <B(02) 028+V(2) 103+V(1)
<< Success! ==> defined new CTR 9 (PPA)
39290 103154461 -13869 <B(02) 026934 107
== Executing PA-CTR 3, V(1)=5, V(2)=6933, repcount=6, factor=2/1
39314 103404361 -13881 <B(02) 026946 10
39315 103404366 -13878 12 (12)C> 026946 10
39316 103418258 14 126947 (12)C> 10
39317 103418265 11 126947 <B(02) 02
39318 103446053 -13883 <B(02) 026948
39319 103446058 -13880 12 (12)C> 026948
39320 103459954 16 126949 (12)C>
39321 103459956 18 126950 (11)B>
39322 103459963 15 126950 <C(01)
39323 103487763 -13885 <C(01) 016950
39324 103487766 -13882 01 (12)D> 016950
39325 103487771 -13885 01 <B(02) 11 016949
39326 103487778 -13882 11 (22)C> 11 016949
39327 103487780 -13880 11 22 (22)D> 016949
39328 103487783 -13883 11 22 <B(00) 11 016948
39329 103487785 -13885 11 <B(00) 00 11 016948
39330 103487791 -13887 <B(02) 10 00 11 016948
39331 103487796 -13884 12 (12)C> 10 00 11 016948
39332 103487803 -13887 12 <B(02) 02 00 11 016948
39333 103487807 -13889 <B(02) 022 00 11 016948
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <B(02) 021+V(1) 10
1 5 3 12 (12)C> 021+V(1) 10
2 7+2*V(1) 5+2*V(1) 122+V(1) (12)C> 10
3 14+2*V(1) 2+2*V(1) 122+V(1) <B(02) 02
4 22+6*V(1) -2 <B(02) 023+V(1)
5 27+6*V(1) 1 12 (12)C> 023+V(1)
6 33+8*V(1) 7+2*V(1) 124+V(1) (12)C>
7 35+8*V(1) 9+2*V(1) 125+V(1) (11)B>
8 42+8*V(1) 6+2*V(1) 125+V(1) <C(01)
9 62+12*V(1) -4 <C(01) 015+V(1)
10 65+12*V(1) -1 01 (12)D> 015+V(1)
11 70+12*V(1) -4 01 <B(02) 11 014+V(1)
12 77+12*V(1) -1 11 (22)C> 11 014+V(1)
13 79+12*V(1) 1 11 22 (22)D> 014+V(1)
14 82+12*V(1) -2 11 22 <B(00) 11 013+V(1)
15 84+12*V(1) -4 11 <B(00) 00 11 013+V(1)
16 90+12*V(1) -6 <B(02) 10 00 11 013+V(1)
17 95+12*V(1) -3 12 (12)C> 10 00 11 013+V(1)
18 102+12*V(1) -6 12 <B(02) 02 00 11 013+V(1)
19 106+12*V(1) -8 <B(02) 022 00 11 013+V(1)
<< Success! ==> defined new CTR 10 (PPA)
39333 103487807 -13889 <B(02) 022 00 11 016948
== Executing PA-CTR 4, V(1)=6945, V(2)=1, repcount=3473, factor=5/2
98374 646595547 -34727 <B(02) 0217367 00 11 012
98375 646595552 -34724 12 (12)C> 0217367 00 11 012
98376 646630286 10 1217368 (12)C> 00 11 012
98377 646630288 12 1217369 (11)B> 11 012
98378 646630292 14 1217369 11 (21)A> 012
98379 646630294 16 1217369 11 21 (12)D> 01
98380 646630299 13 1217369 11 21 <B(02) 11
98381 646630303 11 1217369 11 <B(00) 12 11
98382 646630309 9 1217369 <B(02) 10 12 11
98383 646699785 -34729 <B(02) 0217369 10 12 11
98384 646699790 -34726 12 (12)C> 0217369 10 12 11
98385 646734528 12 1217370 (12)C> 10 12 11
98386 646734535 9 1217370 <B(02) 02 12 11
98387 646804015 -34731 <B(02) 0217371 12 11
98388 646804020 -34728 12 (12)C> 0217371 12 11
98389 646838762 14 1217372 (12)C> 12 11
98390 646838769 11 1217372 <B(02) 00 11
98391 646908257 -34733 <B(02) 0217372 00 11
98392 646908262 -34730 12 (12)C> 0217372 00 11
98393 646943006 14 1217373 (12)C> 00 11
98394 646943008 16 1217374 (11)B> 11
98395 646943012 18 1217374 11 (21)A>
98396 646943021 15 1217374 11 <B(00) 10
98397 646943027 13 1217374 <B(02) 102
98398 647012523 -34735 <B(02) 0217374 102
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <B(02) 021+V(1) 00 11 012
1 5 3 12 (12)C> 021+V(1) 00 11 012
2 7+2*V(1) 5+2*V(1) 122+V(1) (12)C> 00 11 012
3 9+2*V(1) 7+2*V(1) 123+V(1) (11)B> 11 012
4 13+2*V(1) 9+2*V(1) 123+V(1) 11 (21)A> 012
5 15+2*V(1) 11+2*V(1) 123+V(1) 11 21 (12)D> 01
6 20+2*V(1) 8+2*V(1) 123+V(1) 11 21 <B(02) 11
7 24+2*V(1) 6+2*V(1) 123+V(1) 11 <B(00) 12 11
8 30+2*V(1) 4+2*V(1) 123+V(1) <B(02) 10 12 11
9 42+6*V(1) -2 <B(02) 023+V(1) 10 12 11
10 47+6*V(1) 1 12 (12)C> 023+V(1) 10 12 11
11 53+8*V(1) 7+2*V(1) 124+V(1) (12)C> 10 12 11
12 60+8*V(1) 4+2*V(1) 124+V(1) <B(02) 02 12 11
13 76+12*V(1) -4 <B(02) 025+V(1) 12 11
14 81+12*V(1) -1 12 (12)C> 025+V(1) 12 11
15 91+14*V(1) 9+2*V(1) 126+V(1) (12)C> 12 11
16 98+14*V(1) 6+2*V(1) 126+V(1) <B(02) 00 11
17 122+18*V(1) -6 <B(02) 026+V(1) 00 11
18 127+18*V(1) -3 12 (12)C> 026+V(1) 00 11
19 139+20*V(1) 9+2*V(1) 127+V(1) (12)C> 00 11
20 141+20*V(1) 11+2*V(1) 128+V(1) (11)B> 11
21 145+20*V(1) 13+2*V(1) 128+V(1) 11 (21)A>
22 154+20*V(1) 10+2*V(1) 128+V(1) 11 <B(00) 10
23 160+20*V(1) 8+2*V(1) 128+V(1) <B(02) 102
24 192+24*V(1) -8 <B(02) 028+V(1) 102
<< Success! ==> defined new CTR 11 (PPA)
98398 647012523 -34735 <B(02) 0217374 102
== Executing PA-CTR 3, V(1)=0, V(2)=17373, repcount=1, factor=2/1
98402 647116783 -34737 <B(02) 0217376 10
== Executing PPA-CTR 10 (once), V(1)=17375
98421 647325389 -34745 <B(02) 022 00 11 0117378
== Executing PA-CTR 4, V(1)=17375, V(2)=1, repcount=8688, factor=5/2
246117 4044811229 -86873 <B(02) 0243442 00 11 012
== Executing PPA-CTR 11 (once), V(1)=43441
246141 4045854005 -86881 <B(02) 0243449 102
== Executing PA-CTR 3, V(1)=0, V(2)=43448, repcount=1, factor=2/1
246145 4046114715 -86883 <B(02) 0243451 10
== Executing PPA-CTR 10 (once), V(1)=43450
246164 4046636221 -86891 <B(02) 022 00 11 0143453
== Executing PA-CTR 4, V(1)=43450, V(2)=1, repcount=21726, factor=5/2
615506 25289558611 -217247 <B(02) 02108632 00 11 01
== Executing PPA-CTR 5 (once), V(1)=108631
615538 25292165981 -217259 <B(02) 022 00 11 01108637 21
== Executing PA-CTR 1, V(1)=108634, V(2)=1, repcount=54318, factor=5/2
1538944 158067356771 -543167 <B(02) 02271592 00 11 01 21
1538945 158067356776 -543164 12 (12)C> 02271592 00 11 01 21
1538946 158067899960 20 12271593 (12)C> 00 11 01 21
1538947 158067899962 22 12271594 (11)B> 11 01 21
1538948 158067899966 24 12271594 11 (21)A> 01 21
1538949 158067899968 26 12271594 11 21 (12)D> 21
1538950 158067899970 28 12271594 11 21 12 (22)B>
1538951 158067899973 25 12271594 11 21 12 <C(00) 20
1538952 158067899977 23 12271594 11 21 <C(01) 00 20
1538953 158067899981 21 12271594 11 <C(00) 21 00 20
1538954 158067899987 19 12271594 <C(01) 20 21 00 20
1538955 158068986363 -543169 <C(01) 01271594 20 21 00 20
1538956 158068986366 -543166 01 (12)D> 01271594 20 21 00 20
1538957 158068986371 -543169 01 <B(02) 11 01271593 20 21 00 20
1538958 158068986378 -543166 11 (22)C> 11 01271593 20 21 00 20
1538959 158068986380 -543164 11 22 (22)D> 01271593 20 21 00 20
1538960 158068986383 -543167 11 22 <B(00) 11 01271592 20 21 00 20
1538961 158068986385 -543169 11 <B(00) 00 11 01271592 20 21 00 20
1538962 158068986391 -543171 <B(02) 10 00 11 01271592 20 21 00 20
1538963 158068986396 -543168 12 (12)C> 10 00 11 01271592 20 21 00 20
1538964 158068986403 -543171 12 <B(02) 02 00 11 01271592 20 21 00 20
1538965 158068986407 -543173 <B(02) 022 00 11 01271592 20 21 00 20
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <B(02) 023+V(1) 00 11 01 21
1 5 3 12 (12)C> 023+V(1) 00 11 01 21
2 11+2*V(1) 9+2*V(1) 124+V(1) (12)C> 00 11 01 21
3 13+2*V(1) 11+2*V(1) 125+V(1) (11)B> 11 01 21
4 17+2*V(1) 13+2*V(1) 125+V(1) 11 (21)A> 01 21
5 19+2*V(1) 15+2*V(1) 125+V(1) 11 21 (12)D> 21
6 21+2*V(1) 17+2*V(1) 125+V(1) 11 21 12 (22)B>
7 24+2*V(1) 14+2*V(1) 125+V(1) 11 21 12 <C(00) 20
8 28+2*V(1) 12+2*V(1) 125+V(1) 11 21 <C(01) 00 20
9 32+2*V(1) 10+2*V(1) 125+V(1) 11 <C(00) 21 00 20
10 38+2*V(1) 8+2*V(1) 125+V(1) <C(01) 20 21 00 20
11 58+6*V(1) -2 <C(01) 015+V(1) 20 21 00 20
12 61+6*V(1) 1 01 (12)D> 015+V(1) 20 21 00 20
13 66+6*V(1) -2 01 <B(02) 11 014+V(1) 20 21 00 20
14 73+6*V(1) 1 11 (22)C> 11 014+V(1) 20 21 00 20
15 75+6*V(1) 3 11 22 (22)D> 014+V(1) 20 21 00 20
16 78+6*V(1) 0 11 22 <B(00) 11 013+V(1) 20 21 00 20
17 80+6*V(1) -2 11 <B(00) 00 11 013+V(1) 20 21 00 20
18 86+6*V(1) -4 <B(02) 10 00 11 013+V(1) 20 21 00 20
19 91+6*V(1) -1 12 (12)C> 10 00 11 013+V(1) 20 21 00 20
20 98+6*V(1) -4 12 <B(02) 02 00 11 013+V(1) 20 21 00 20
21 102+6*V(1) -6 <B(02) 022 00 11 013+V(1) 20 21 00 20
<< Success! ==> defined new CTR 12 (PPA)
1538965 158068986407 -543173 <B(02) 022 00 11 01271592 20 21 00 20
== Executing PA-CTR 6, V(1)=271589, V(2)=1, repcount=135795, factor=5/2
3847480 987894578057 -1357943 <B(02) 02678977 00 11 012 20 21 00 20
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=0, V(3)=678976
3847517 987910873723 -1357955 <B(02) 022 00 11 01678982 205
== Executing PA-CTR 1, V(1)=678979, V(2)=1, repcount=339490, factor=5/2
9618847 6174348829773 -3394895 <B(02) 021697452 00 11 012 205
9618848 6174348829778 -3394892 12 (12)C> 021697452 00 11 012 205
9618849 6174352224682 12 121697453 (12)C> 00 11 012 205
9618850 6174352224684 14 121697454 (11)B> 11 012 205
9618851 6174352224688 16 121697454 11 (21)A> 012 205
9618852 6174352224690 18 121697454 11 21 (12)D> 01 205
9618853 6174352224695 15 121697454 11 21 <B(02) 11 205
9618854 6174352224699 13 121697454 11 <B(00) 12 11 205
9618855 6174352224705 11 121697454 <B(02) 10 12 11 205
9618856 6174359014521 -3394897 <B(02) 021697454 10 12 11 205
9618857 6174359014526 -3394894 12 (12)C> 021697454 10 12 11 205
9618858 6174362409434 14 121697455 (12)C> 10 12 11 205
9618859 6174362409441 11 121697455 <B(02) 02 12 11 205
9618860 6174369199261 -3394899 <B(02) 021697456 12 11 205
9618861 6174369199266 -3394896 12 (12)C> 021697456 12 11 205
9618862 6174372594178 16 121697457 (12)C> 12 11 205
9618863 6174372594185 13 121697457 <B(02) 00 11 205
9618864 6174379384013 -3394901 <B(02) 021697457 00 11 205
9618865 6174379384018 -3394898 12 (12)C> 021697457 00 11 205
9618866 6174382778932 16 121697458 (12)C> 00 11 205
9618867 6174382778934 18 121697459 (11)B> 11 205
9618868 6174382778938 20 121697459 11 (21)A> 205
9618869 6174382778948 30 121697459 11 215 (21)A>
9618870 6174382778957 27 121697459 11 215 <B(00) 10
9618871 6174382778977 17 121697459 11 <B(00) 106
9618872 6174382778983 15 121697459 <B(02) 107
9618873 6174389568819 -3394903 <B(02) 021697459 107
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <B(02) 021+V(2) 00 11 012 201+V(1)
1 5 3 12 (12)C> 021+V(2) 00 11 012 201+V(1)
2 7+2*V(2) 5+2*V(2) 122+V(2) (12)C> 00 11 012 201+V(1)
3 9+2*V(2) 7+2*V(2) 123+V(2) (11)B> 11 012 201+V(1)
4 13+2*V(2) 9+2*V(2) 123+V(2) 11 (21)A> 012 201+V(1)
5 15+2*V(2) 11+2*V(2) 123+V(2) 11 21 (12)D> 01 201+V(1)
6 20+2*V(2) 8+2*V(2) 123+V(2) 11 21 <B(02) 11 201+V(1)
7 24+2*V(2) 6+2*V(2) 123+V(2) 11 <B(00) 12 11 201+V(1)
8 30+2*V(2) 4+2*V(2) 123+V(2) <B(02) 10 12 11 201+V(1)
9 42+6*V(2) -2 <B(02) 023+V(2) 10 12 11 201+V(1)
10 47+6*V(2) 1 12 (12)C> 023+V(2) 10 12 11 201+V(1)
11 53+8*V(2) 7+2*V(2) 124+V(2) (12)C> 10 12 11 201+V(1)
12 60+8*V(2) 4+2*V(2) 124+V(2) <B(02) 02 12 11 201+V(1)
13 76+12*V(2) -4 <B(02) 025+V(2) 12 11 201+V(1)
14 81+12*V(2) -1 12 (12)C> 025+V(2) 12 11 201+V(1)
15 91+14*V(2) 9+2*V(2) 126+V(2) (12)C> 12 11 201+V(1)
16 98+14*V(2) 6+2*V(2) 126+V(2) <B(02) 00 11 201+V(1)
17 122+18*V(2) -6 <B(02) 026+V(2) 00 11 201+V(1)
18 127+18*V(2) -3 12 (12)C> 026+V(2) 00 11 201+V(1)
19 139+20*V(2) 9+2*V(2) 127+V(2) (12)C> 00 11 201+V(1)
20 141+20*V(2) 11+2*V(2) 128+V(2) (11)B> 11 201+V(1)
21 145+20*V(2) 13+2*V(2) 128+V(2) 11 (21)A> 201+V(1)
22 147+2*V(1)+20*V(2) 15+2*V(1)+2*V(2) 128+V(2) 11 211+V(1) (21)A>
23 156+2*V(1)+20*V(2) 12+2*V(1)+2*V(2) 128+V(2) 11 211+V(1) <B(00) 10
24 160+6*V(1)+20*V(2) 10+2*V(2) 128+V(2) 11 <B(00) 102+V(1)
25 166+6*V(1)+20*V(2) 8+2*V(2) 128+V(2) <B(02) 103+V(1)
26 198+6*V(1)+24*V(2) -8 <B(02) 028+V(2) 103+V(1)
<< Success! ==> defined new CTR 13 (PPA)
9618873 6174389568819 -3394903 <B(02) 021697459 107
== Executing PA-CTR 3, V(1)=5, V(2)=1697458, repcount=6, factor=2/1
9618897 6174450677619 -3394915 <B(02) 021697471 10
== Executing PPA-CTR 10 (once), V(1)=1697470
9618916 6174471047365 -3394923 <B(02) 022 00 11 011697473
== Executing PA-CTR 4, V(1)=1697470, V(2)=1, repcount=848736, factor=5/2
24047428 38590427573605 -8487339 <B(02) 024243682 00 11 01
== Executing PPA-CTR 5 (once), V(1)=4243681
24047460 38590529422175 -8487351 <B(02) 022 00 11 014243687 21
== Executing PA-CTR 1, V(1)=4243684, V(2)=1, repcount=2121843, factor=5/2
60118791 241190528246465 -21218409 <B(02) 0210609217 00 11 01 21
== Executing PPA-CTR 12 (once), V(1)=10609214
60118812 241190591901851 -21218415 <B(02) 022 00 11 0110609217 20 21 00 20
== Executing PA-CTR 6, V(1)=10609214, V(2)=1, repcount=5304608, factor=5/2
150297148 1507440067354491 -53046063 <B(02) 0226523042 00 11 01 20 21 00 20
150297149 1507440067354496 -53046060 12 (12)C> 0226523042 00 11 01 20 21 00 20
150297150 1507440120400580 24 1226523043 (12)C> 00 11 01 20 21 00 20
150297151 1507440120400582 26 1226523044 (11)B> 11 01 20 21 00 20
150297152 1507440120400586 28 1226523044 11 (21)A> 01 20 21 00 20
150297153 1507440120400588 30 1226523044 11 21 (12)D> 20 21 00 20
150297154 1507440120400590 32 1226523044 11 21 12 (21)A> 21 00 20
150297155 1507440120400592 34 1226523044 11 21 12 21 (22)B> 00 20
150297156 1507440120400595 31 1226523044 11 21 12 21 <C(00) 202
150297157 1507440120400599 29 1226523044 11 21 12 <C(00) 203
150297158 1507440120400603 27 1226523044 11 21 <C(01) 00 203
150297159 1507440120400607 25 1226523044 11 <C(00) 21 00 203
150297160 1507440120400613 23 1226523044 <C(01) 20 21 00 203
150297161 1507440226492789 -53046065 <C(01) 0126523044 20 21 00 203
150297162 1507440226492792 -53046062 01 (12)D> 0126523044 20 21 00 203
150297163 1507440226492797 -53046065 01 <B(02) 11 0126523043 20 21 00 203
Lines: 500
Top steps: 499
Macro steps: 150297163
Basic steps: 1507440226492797
Tape index: -53046065
nonzeros: 26523053
log10(nonzeros): 7.424
log10(steps ): 15.178
Input to awk program:
gohalt 1
nbs 3
T 4-state 3-symbol #i (T.J. & S. Ligocki)
: >1.383x10^7036 >1.025x10^14072
C This is the currently best known 4x3 TM
5T 1RB 1RH 2RC 2LC 2RD 0LC 1RA 2RB 0LB 1LB 0LD 2RC
L 16
M 500
pref sim
machv Lig43_i just simple
machv Lig43_i-r with repetitions reduced
machv Lig43_i-1 with tape symbol exponents
machv Lig43_i-m as 2-bck-macro machine
machv Lig43_i-a as 2-bck-macro machine with pure additive config-TRs
iam Lig43_i-a
mtype 2 0
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:14:19 CEST 2010
edate Tue Jul 6 22:14:21 CEST 2010
bnspeed 1
short 7
Constructed by: $Id: tmJob.awk,v 1.34 2010/05/06 18:26:17 heiner Exp $
$Id: basics.awk,v 1.1 2010/05/06 17:24:17 heiner Exp $
$Id: htSupp.awk,v 1.14 2010/07/06 19:48:32 heiner Exp $
$Id: mmSim.awk,v 1.34 2005/01/09 22:23:28 heiner Exp $
$Id: bignum.awk,v 1.34 2010/05/06 17:58:14 heiner Exp $
$Id: varLI.awk,v 1.11 2005/01/15 21:01:29 heiner Exp $
bignum signature: LEN={S++:9 U++:9 S+:8 U+:8 S*:4 U*:4} DONT: y i o;
Start: Tue Jul 6 22:14:19 CEST 2010