Comment: This TM produces >8.6x10^821 nonzeros in >4.9x10^1643 steps.
| State | on 0 |
on 1 |
on 2 |
on 3 |
on 4 |
on 5 |
on 0 | on 1 | on 2 | on 3 | on 4 | on 5 | ||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Move | Goto | Move | Goto | Move | Goto | Move | Goto | Move | Goto | Move | Goto | |||||||||||||
| A | 1RB | 2LB | 4RB | 1LA | 1RB | 1RH | 1 | right | B | 2 | left | B | 4 | right | B | 1 | left | A | 1 | right | B | 1 | right | H |
| B | 1LA | 3RA | 5RA | 4LB | 0RA | 4LA | 1 | left | A | 3 | right | A | 5 | right | A | 4 | left | B | 0 | right | A | 4 | left | A |
The same TM just simple.
The same TM with repetitions reduced.
The same TM with tape symbol exponents.
The same TM as 2-macro machine.
Simulation is done as 2-macro machine with pure additive config-TRs.
Pushing initial machine.
Pushing macro factor 2.
Steps BasSteps BasTpos Tape contents
0 0 0 A>
1 3 -1 <B 21
2 6 0 13 A> 21
3 8 2 13 43 A>
4 11 1 13 43 <B 21
5 14 2 13 01 B> 21
6 17 1 13 01 <A 42
7 19 -1 13 <A 12 42
8 21 -3 <B 21 12 42
9 24 -2 13 A> 21 12 42
10 26 0 13 43 A> 12 42
11 27 -1 13 43 <B 22 42
12 30 0 13 01 B> 22 42
13 32 2 13 01 54 B> 42
14 34 4 13 01 54 04 B>
15 35 3 13 01 54 04 <A 10
16 36 4 13 01 54 01 B> 10
17 38 6 13 01 54 01 31 B>
18 39 5 13 01 54 01 31 <A 10
19 41 3 13 01 54 01 <B 42 10
20 42 4 13 01 54 03 A> 42 10
21 44 6 13 01 54 03 15 A> 10
22 45 5 13 01 54 03 15 <B 20
23 47 3 13 01 54 03 <B 24 20
24 49 1 13 01 54 <A 14 24 20
25 50 2 13 01 51 B> 14 24 20
26 52 4 13 01 51 31 B> 24 20
27 54 6 13 01 51 31 51 B> 20
28 56 8 13 01 51 31 512 B>
29 57 7 13 01 51 31 512 <A 10
30 61 3 13 01 51 31 <A 422 10
31 63 1 13 01 51 <B 423 10
32 64 2 13 01 53 A> 423 10
33 70 8 13 01 53 153 A> 10
34 71 7 13 01 53 153 <B 20
35 77 1 13 01 53 <B 243 20
36 79 -1 13 01 <A 44 243 20
37 81 -3 13 <A 12 44 243 20
38 83 -5 <B 21 12 44 243 20
39 86 -4 13 A> 21 12 44 243 20
40 88 -2 13 43 A> 12 44 243 20
41 89 -3 13 43 <B 22 44 243 20
42 92 -2 13 01 B> 22 44 243 20
43 94 0 13 01 54 B> 44 243 20
44 96 2 13 01 54 01 B> 243 20
45 102 8 13 01 54 01 513 B> 20
46 104 10 13 01 54 01 514 B>
47 105 9 13 01 54 01 514 <A 10
48 113 1 13 01 54 01 <A 424 10
49 115 -1 13 01 54 <A 12 424 10
50 116 0 13 01 51 B> 12 424 10
51 118 2 13 01 51 34 B> 424 10
52 126 10 13 01 51 34 044 B> 10
53 128 12 13 01 51 34 044 31 B>
54 129 11 13 01 51 34 044 31 <A 10
55 131 9 13 01 51 34 044 <B 42 10
56 132 10 13 01 51 34 043 00 A> 42 10
57 134 12 13 01 51 34 043 00 15 A> 10
58 135 11 13 01 51 34 043 00 15 <B 20
59 137 9 13 01 51 34 043 00 <B 24 20
60 140 10 13 01 51 34 043 13 A> 24 20
61 142 12 13 01 51 34 043 13 40 A> 20
62 146 14 13 01 51 34 043 13 40 13 A>
63 149 13 13 01 51 34 043 13 40 13 <B 21
64 152 14 13 01 51 34 043 13 40 31 B> 21
65 155 13 13 01 51 34 043 13 40 31 <A 42
66 157 11 13 01 51 34 043 13 40 <B 422
67 160 12 13 01 51 34 043 132 A> 422
68 164 16 13 01 51 34 043 132 152 A>
69 167 15 13 01 51 34 043 132 152 <B 21
70 171 11 13 01 51 34 043 132 <B 242 21
71 174 12 13 01 51 34 043 13 31 B> 242 21
72 178 16 13 01 51 34 043 13 31 512 B> 21
73 181 15 13 01 51 34 043 13 31 512 <A 42
74 185 11 13 01 51 34 043 13 31 <A 423
75 187 9 13 01 51 34 043 13 <B 424
76 190 10 13 01 51 34 043 31 B> 424
77 198 18 13 01 51 34 043 31 044 B>
78 199 17 13 01 51 34 043 31 044 <A 10
79 200 18 13 01 51 34 043 31 043 01 B> 10
80 202 20 13 01 51 34 043 31 043 01 31 B>
81 203 19 13 01 51 34 043 31 043 01 31 <A 10
82 205 17 13 01 51 34 043 31 043 01 <B 42 10
83 206 18 13 01 51 34 043 31 043 03 A> 42 10
84 208 20 13 01 51 34 043 31 043 03 15 A> 10
85 209 19 13 01 51 34 043 31 043 03 15 <B 20
86 211 17 13 01 51 34 043 31 043 03 <B 24 20
87 213 15 13 01 51 34 043 31 043 <A 14 24 20
88 214 16 13 01 51 34 043 31 042 01 B> 14 24 20
89 216 18 13 01 51 34 043 31 042 01 31 B> 24 20
90 218 20 13 01 51 34 043 31 042 01 31 51 B> 20
91 220 22 13 01 51 34 043 31 042 01 31 512 B>
92 221 21 13 01 51 34 043 31 042 01 31 512 <A 10
93 225 17 13 01 51 34 043 31 042 01 31 <A 422 10
94 227 15 13 01 51 34 043 31 042 01 <B 423 10
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* [*]* [*]* [*]* 042+V(1) 01 <B 421+V(2) 10
1 1 1 [*]* [*]* [*]* [*]* [*]* [*]* 042+V(1) 03 A> 421+V(2) 10
2 3+2*V(2) 3+2*V(2) [*]* [*]* [*]* [*]* [*]* [*]* 042+V(1) 03 151+V(2) A> 10
3 4+2*V(2) 2+2*V(2) [*]* [*]* [*]* [*]* [*]* [*]* 042+V(1) 03 151+V(2) <B 20
4 6+4*V(2) 0 [*]* [*]* [*]* [*]* [*]* [*]* 042+V(1) 03 <B 241+V(2) 20
5 8+4*V(2) -2 [*]* [*]* [*]* [*]* [*]* [*]* 042+V(1) <A 14 241+V(2) 20
6 9+4*V(2) -1 [*]* [*]* [*]* [*]* [*]* [*]* 041+V(1) 01 B> 14 241+V(2) 20
7 11+4*V(2) 1 [*]* [*]* [*]* [*]* [*]* [*]* 041+V(1) 01 31 B> 241+V(2) 20
8 13+6*V(2) 3+2*V(2) [*]* [*]* [*]* [*]* [*]* [*]* 041+V(1) 01 31 511+V(2) B> 20
9 15+6*V(2) 5+2*V(2) [*]* [*]* [*]* [*]* [*]* [*]* 041+V(1) 01 31 512+V(2) B>
10 16+6*V(2) 4+2*V(2) [*]* [*]* [*]* [*]* [*]* [*]* 041+V(1) 01 31 512+V(2) <A 10
11 20+8*V(2) 0 [*]* [*]* [*]* [*]* [*]* [*]* 041+V(1) 01 31 <A 422+V(2) 10
12 22+8*V(2) -2 [*]* [*]* [*]* [*]* [*]* [*]* 041+V(1) 01 <B 423+V(2) 10
<< Success! ==> defined new CTR 1 (PA)
94 227 15 13 01 51 34 043 31 042 01 <B 423 10
== Executing PA-CTR 1, V(1)=0, V(2)=2, repcount=1, factor=2/1
106 265 13 13 01 51 34 043 31 04 01 <B 425 10
107 266 14 13 01 51 34 043 31 04 03 A> 425 10
108 276 24 13 01 51 34 043 31 04 03 155 A> 10
109 277 23 13 01 51 34 043 31 04 03 155 <B 20
110 287 13 13 01 51 34 043 31 04 03 <B 245 20
111 289 11 13 01 51 34 043 31 04 <A 14 245 20
112 290 12 13 01 51 34 043 31 01 B> 14 245 20
113 292 14 13 01 51 34 043 31 01 31 B> 245 20
114 302 24 13 01 51 34 043 31 01 31 515 B> 20
115 304 26 13 01 51 34 043 31 01 31 516 B>
116 305 25 13 01 51 34 043 31 01 31 516 <A 10
117 317 13 13 01 51 34 043 31 01 31 <A 426 10
118 319 11 13 01 51 34 043 31 01 <B 427 10
119 320 12 13 01 51 34 043 31 03 A> 427 10
120 334 26 13 01 51 34 043 31 03 157 A> 10
121 335 25 13 01 51 34 043 31 03 157 <B 20
122 349 11 13 01 51 34 043 31 03 <B 247 20
123 351 9 13 01 51 34 043 31 <A 14 247 20
124 353 7 13 01 51 34 043 <B 42 14 247 20
125 354 8 13 01 51 34 042 00 A> 42 14 247 20
126 356 10 13 01 51 34 042 00 15 A> 14 247 20
127 357 9 13 01 51 34 042 00 15 <B 248 20
128 359 7 13 01 51 34 042 00 <B 249 20
129 362 8 13 01 51 34 042 13 A> 249 20
130 380 26 13 01 51 34 042 13 409 A> 20
131 384 28 13 01 51 34 042 13 409 13 A>
132 387 27 13 01 51 34 042 13 409 13 <B 21
133 390 28 13 01 51 34 042 13 409 31 B> 21
134 393 27 13 01 51 34 042 13 409 31 <A 42
135 395 25 13 01 51 34 042 13 409 <B 422
136 398 26 13 01 51 34 042 13 408 13 A> 422
137 402 30 13 01 51 34 042 13 408 13 152 A>
138 405 29 13 01 51 34 042 13 408 13 152 <B 21
139 409 25 13 01 51 34 042 13 408 13 <B 242 21
140 412 26 13 01 51 34 042 13 408 31 B> 242 21
141 416 30 13 01 51 34 042 13 408 31 512 B> 21
142 419 29 13 01 51 34 042 13 408 31 512 <A 42
143 423 25 13 01 51 34 042 13 408 31 <A 423
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* [*]* [*]* [*]* 402+V(1) 31 <A 421+V(2)
1 2 -2 [*]* [*]* [*]* [*]* [*]* [*]* 402+V(1) <B 422+V(2)
2 5 -1 [*]* [*]* [*]* [*]* [*]* [*]* 401+V(1) 13 A> 422+V(2)
3 9+2*V(2) 3+2*V(2) [*]* [*]* [*]* [*]* [*]* [*]* 401+V(1) 13 152+V(2) A>
4 12+2*V(2) 2+2*V(2) [*]* [*]* [*]* [*]* [*]* [*]* 401+V(1) 13 152+V(2) <B 21
5 16+4*V(2) -2 [*]* [*]* [*]* [*]* [*]* [*]* 401+V(1) 13 <B 242+V(2) 21
6 19+4*V(2) -1 [*]* [*]* [*]* [*]* [*]* [*]* 401+V(1) 31 B> 242+V(2) 21
7 23+6*V(2) 3+2*V(2) [*]* [*]* [*]* [*]* [*]* [*]* 401+V(1) 31 512+V(2) B> 21
8 26+6*V(2) 2+2*V(2) [*]* [*]* [*]* [*]* [*]* [*]* 401+V(1) 31 512+V(2) <A 42
9 30+8*V(2) -2 [*]* [*]* [*]* [*]* [*]* [*]* 401+V(1) 31 <A 423+V(2)
<< Success! ==> defined new CTR 2 (PA)
143 423 25 13 01 51 34 042 13 408 31 <A 423
== Executing PA-CTR 2, V(1)=6, V(2)=2, repcount=7, factor=2/1
206 1081 11 13 01 51 34 042 13 40 31 <A 4217
207 1083 9 13 01 51 34 042 13 40 <B 4218
208 1086 10 13 01 51 34 042 132 A> 4218
209 1122 46 13 01 51 34 042 132 1518 A>
210 1125 45 13 01 51 34 042 132 1518 <B 21
211 1161 9 13 01 51 34 042 132 <B 2418 21
212 1164 10 13 01 51 34 042 13 31 B> 2418 21
213 1200 46 13 01 51 34 042 13 31 5118 B> 21
214 1203 45 13 01 51 34 042 13 31 5118 <A 42
215 1239 9 13 01 51 34 042 13 31 <A 4219
216 1241 7 13 01 51 34 042 13 <B 4220
217 1244 8 13 01 51 34 042 31 B> 4220
218 1284 48 13 01 51 34 042 31 0420 B>
219 1285 47 13 01 51 34 042 31 0420 <A 10
220 1286 48 13 01 51 34 042 31 0419 01 B> 10
221 1288 50 13 01 51 34 042 31 0419 01 31 B>
222 1289 49 13 01 51 34 042 31 0419 01 31 <A 10
223 1291 47 13 01 51 34 042 31 0419 01 <B 42 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 [*]* [*]* [*]* [*]* [*]* 13 40 31 <A 421+V(1)
1 2 -2 [*]* [*]* [*]* [*]* [*]* 13 40 <B 422+V(1)
2 5 -1 [*]* [*]* [*]* [*]* [*]* 132 A> 422+V(1)
3 9+2*V(1) 3+2*V(1) [*]* [*]* [*]* [*]* [*]* 132 152+V(1) A>
4 12+2*V(1) 2+2*V(1) [*]* [*]* [*]* [*]* [*]* 132 152+V(1) <B 21
5 16+4*V(1) -2 [*]* [*]* [*]* [*]* [*]* 132 <B 242+V(1) 21
6 19+4*V(1) -1 [*]* [*]* [*]* [*]* [*]* 13 31 B> 242+V(1) 21
7 23+6*V(1) 3+2*V(1) [*]* [*]* [*]* [*]* [*]* 13 31 512+V(1) B> 21
8 26+6*V(1) 2+2*V(1) [*]* [*]* [*]* [*]* [*]* 13 31 512+V(1) <A 42
9 30+8*V(1) -2 [*]* [*]* [*]* [*]* [*]* 13 31 <A 423+V(1)
10 32+8*V(1) -4 [*]* [*]* [*]* [*]* [*]* 13 <B 424+V(1)
11 35+8*V(1) -3 [*]* [*]* [*]* [*]* [*]* 31 B> 424+V(1)
12 43+10*V(1) 5+2*V(1) [*]* [*]* [*]* [*]* [*]* 31 044+V(1) B>
13 44+10*V(1) 4+2*V(1) [*]* [*]* [*]* [*]* [*]* 31 044+V(1) <A 10
14 45+10*V(1) 5+2*V(1) [*]* [*]* [*]* [*]* [*]* 31 043+V(1) 01 B> 10
15 47+10*V(1) 7+2*V(1) [*]* [*]* [*]* [*]* [*]* 31 043+V(1) 01 31 B>
16 48+10*V(1) 6+2*V(1) [*]* [*]* [*]* [*]* [*]* 31 043+V(1) 01 31 <A 10
17 50+10*V(1) 4+2*V(1) [*]* [*]* [*]* [*]* [*]* 31 043+V(1) 01 <B 42 10
<< Success! ==> defined new CTR 3 (PPA)
223 1291 47 13 01 51 34 042 31 0419 01 <B 42 10
== Executing PA-CTR 1, V(1)=17, V(2)=0, repcount=18, factor=2/1
439 4135 11 13 01 51 34 042 31 04 01 <B 4237 10
440 4136 12 13 01 51 34 042 31 04 03 A> 4237 10
441 4210 86 13 01 51 34 042 31 04 03 1537 A> 10
442 4211 85 13 01 51 34 042 31 04 03 1537 <B 20
443 4285 11 13 01 51 34 042 31 04 03 <B 2437 20
444 4287 9 13 01 51 34 042 31 04 <A 14 2437 20
445 4288 10 13 01 51 34 042 31 01 B> 14 2437 20
446 4290 12 13 01 51 34 042 31 01 31 B> 2437 20
447 4364 86 13 01 51 34 042 31 01 31 5137 B> 20
448 4366 88 13 01 51 34 042 31 01 31 5138 B>
449 4367 87 13 01 51 34 042 31 01 31 5138 <A 10
450 4443 11 13 01 51 34 042 31 01 31 <A 4238 10
451 4445 9 13 01 51 34 042 31 01 <B 4239 10
452 4446 10 13 01 51 34 042 31 03 A> 4239 10
453 4524 88 13 01 51 34 042 31 03 1539 A> 10
454 4525 87 13 01 51 34 042 31 03 1539 <B 20
455 4603 9 13 01 51 34 042 31 03 <B 2439 20
456 4605 7 13 01 51 34 042 31 <A 14 2439 20
457 4607 5 13 01 51 34 042 <B 42 14 2439 20
458 4608 6 13 01 51 34 04 00 A> 42 14 2439 20
459 4610 8 13 01 51 34 04 00 15 A> 14 2439 20
460 4611 7 13 01 51 34 04 00 15 <B 2440 20
461 4613 5 13 01 51 34 04 00 <B 2441 20
462 4616 6 13 01 51 34 04 13 A> 2441 20
463 4698 88 13 01 51 34 04 13 4041 A> 20
464 4702 90 13 01 51 34 04 13 4041 13 A>
465 4705 89 13 01 51 34 04 13 4041 13 <B 21
466 4708 90 13 01 51 34 04 13 4041 31 B> 21
467 4711 89 13 01 51 34 04 13 4041 31 <A 42
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* [*]* 042+V(1) 31 04 01 <B 421+V(2) 10
1 1 1 [*]* [*]* [*]* [*]* 042+V(1) 31 04 03 A> 421+V(2) 10
2 3+2*V(2) 3+2*V(2) [*]* [*]* [*]* [*]* 042+V(1) 31 04 03 151+V(2) A> 10
3 4+2*V(2) 2+2*V(2) [*]* [*]* [*]* [*]* 042+V(1) 31 04 03 151+V(2) <B 20
4 6+4*V(2) 0 [*]* [*]* [*]* [*]* 042+V(1) 31 04 03 <B 241+V(2) 20
5 8+4*V(2) -2 [*]* [*]* [*]* [*]* 042+V(1) 31 04 <A 14 241+V(2) 20
6 9+4*V(2) -1 [*]* [*]* [*]* [*]* 042+V(1) 31 01 B> 14 241+V(2) 20
7 11+4*V(2) 1 [*]* [*]* [*]* [*]* 042+V(1) 31 01 31 B> 241+V(2) 20
8 13+6*V(2) 3+2*V(2) [*]* [*]* [*]* [*]* 042+V(1) 31 01 31 511+V(2) B> 20
9 15+6*V(2) 5+2*V(2) [*]* [*]* [*]* [*]* 042+V(1) 31 01 31 512+V(2) B>
10 16+6*V(2) 4+2*V(2) [*]* [*]* [*]* [*]* 042+V(1) 31 01 31 512+V(2) <A 10
11 20+8*V(2) 0 [*]* [*]* [*]* [*]* 042+V(1) 31 01 31 <A 422+V(2) 10
12 22+8*V(2) -2 [*]* [*]* [*]* [*]* 042+V(1) 31 01 <B 423+V(2) 10
13 23+8*V(2) -1 [*]* [*]* [*]* [*]* 042+V(1) 31 03 A> 423+V(2) 10
14 29+10*V(2) 5+2*V(2) [*]* [*]* [*]* [*]* 042+V(1) 31 03 153+V(2) A> 10
15 30+10*V(2) 4+2*V(2) [*]* [*]* [*]* [*]* 042+V(1) 31 03 153+V(2) <B 20
16 36+12*V(2) -2 [*]* [*]* [*]* [*]* 042+V(1) 31 03 <B 243+V(2) 20
17 38+12*V(2) -4 [*]* [*]* [*]* [*]* 042+V(1) 31 <A 14 243+V(2) 20
18 40+12*V(2) -6 [*]* [*]* [*]* [*]* 042+V(1) <B 42 14 243+V(2) 20
19 41+12*V(2) -5 [*]* [*]* [*]* [*]* 041+V(1) 00 A> 42 14 243+V(2) 20
20 43+12*V(2) -3 [*]* [*]* [*]* [*]* 041+V(1) 00 15 A> 14 243+V(2) 20
21 44+12*V(2) -4 [*]* [*]* [*]* [*]* 041+V(1) 00 15 <B 244+V(2) 20
22 46+12*V(2) -6 [*]* [*]* [*]* [*]* 041+V(1) 00 <B 245+V(2) 20
23 49+12*V(2) -5 [*]* [*]* [*]* [*]* 041+V(1) 13 A> 245+V(2) 20
24 59+14*V(2) 5+2*V(2) [*]* [*]* [*]* [*]* 041+V(1) 13 405+V(2) A> 20
25 63+14*V(2) 7+2*V(2) [*]* [*]* [*]* [*]* 041+V(1) 13 405+V(2) 13 A>
26 66+14*V(2) 6+2*V(2) [*]* [*]* [*]* [*]* 041+V(1) 13 405+V(2) 13 <B 21
27 69+14*V(2) 7+2*V(2) [*]* [*]* [*]* [*]* 041+V(1) 13 405+V(2) 31 B> 21
28 72+14*V(2) 6+2*V(2) [*]* [*]* [*]* [*]* 041+V(1) 13 405+V(2) 31 <A 42
<< Success! ==> defined new CTR 4 (PPA)
467 4711 89 13 01 51 34 04 13 4041 31 <A 42
== Executing PA-CTR 2, V(1)=39, V(2)=0, repcount=40, factor=2/1
827 18391 9 13 01 51 34 04 13 40 31 <A 4281
== Executing PPA-CTR 3 (once), V(1)=80
844 19241 173 13 01 51 34 04 31 0483 01 <B 42 10
== Executing PA-CTR 1, V(1)=81, V(2)=0, repcount=82, factor=2/1
1828 74181 9 13 01 51 34 04 31 04 01 <B 42165 10
1829 74182 10 13 01 51 34 04 31 04 03 A> 42165 10
1830 74512 340 13 01 51 34 04 31 04 03 15165 A> 10
1831 74513 339 13 01 51 34 04 31 04 03 15165 <B 20
1832 74843 9 13 01 51 34 04 31 04 03 <B 24165 20
1833 74845 7 13 01 51 34 04 31 04 <A 14 24165 20
1834 74846 8 13 01 51 34 04 31 01 B> 14 24165 20
1835 74848 10 13 01 51 34 04 31 01 31 B> 24165 20
1836 75178 340 13 01 51 34 04 31 01 31 51165 B> 20
1837 75180 342 13 01 51 34 04 31 01 31 51166 B>
1838 75181 341 13 01 51 34 04 31 01 31 51166 <A 10
1839 75513 9 13 01 51 34 04 31 01 31 <A 42166 10
1840 75515 7 13 01 51 34 04 31 01 <B 42167 10
1841 75516 8 13 01 51 34 04 31 03 A> 42167 10
1842 75850 342 13 01 51 34 04 31 03 15167 A> 10
1843 75851 341 13 01 51 34 04 31 03 15167 <B 20
1844 76185 7 13 01 51 34 04 31 03 <B 24167 20
1845 76187 5 13 01 51 34 04 31 <A 14 24167 20
1846 76189 3 13 01 51 34 04 <B 42 14 24167 20
1847 76190 4 13 01 51 34 00 A> 42 14 24167 20
1848 76192 6 13 01 51 34 00 15 A> 14 24167 20
1849 76193 5 13 01 51 34 00 15 <B 24168 20
1850 76195 3 13 01 51 34 00 <B 24169 20
1851 76198 4 13 01 51 34 13 A> 24169 20
1852 76536 342 13 01 51 34 13 40169 A> 20
1853 76540 344 13 01 51 34 13 40169 13 A>
1854 76543 343 13 01 51 34 13 40169 13 <B 21
1855 76546 344 13 01 51 34 13 40169 31 B> 21
1856 76549 343 13 01 51 34 13 40169 31 <A 42
1857 76551 341 13 01 51 34 13 40169 <B 422
1858 76554 342 13 01 51 34 13 40168 13 A> 422
1859 76558 346 13 01 51 34 13 40168 13 152 A>
1860 76561 345 13 01 51 34 13 40168 13 152 <B 21
1861 76565 341 13 01 51 34 13 40168 13 <B 242 21
1862 76568 342 13 01 51 34 13 40168 31 B> 242 21
1863 76572 346 13 01 51 34 13 40168 31 512 B> 21
1864 76575 345 13 01 51 34 13 40168 31 512 <A 42
1865 76579 341 13 01 51 34 13 40168 31 <A 423
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* [*]* [*]* 402+V(1) 31 <A 421+V(2)
1 2 -2 [*]* [*]* [*]* [*]* [*]* 402+V(1) <B 422+V(2)
2 5 -1 [*]* [*]* [*]* [*]* [*]* 401+V(1) 13 A> 422+V(2)
3 9+2*V(2) 3+2*V(2) [*]* [*]* [*]* [*]* [*]* 401+V(1) 13 152+V(2) A>
4 12+2*V(2) 2+2*V(2) [*]* [*]* [*]* [*]* [*]* 401+V(1) 13 152+V(2) <B 21
5 16+4*V(2) -2 [*]* [*]* [*]* [*]* [*]* 401+V(1) 13 <B 242+V(2) 21
6 19+4*V(2) -1 [*]* [*]* [*]* [*]* [*]* 401+V(1) 31 B> 242+V(2) 21
7 23+6*V(2) 3+2*V(2) [*]* [*]* [*]* [*]* [*]* 401+V(1) 31 512+V(2) B> 21
8 26+6*V(2) 2+2*V(2) [*]* [*]* [*]* [*]* [*]* 401+V(1) 31 512+V(2) <A 42
9 30+8*V(2) -2 [*]* [*]* [*]* [*]* [*]* 401+V(1) 31 <A 423+V(2)
<< Success! ==> defined new CTR 5 (PA)
1865 76579 341 13 01 51 34 13 40168 31 <A 423
== Executing PA-CTR 5, V(1)=166, V(2)=2, repcount=167, factor=2/1
3368 306037 7 13 01 51 34 13 40 31 <A 42337
3369 306039 5 13 01 51 34 13 40 <B 42338
3370 306042 6 13 01 51 34 132 A> 42338
3371 306718 682 13 01 51 34 132 15338 A>
3372 306721 681 13 01 51 34 132 15338 <B 21
3373 307397 5 13 01 51 34 132 <B 24338 21
3374 307400 6 13 01 51 34 13 31 B> 24338 21
3375 308076 682 13 01 51 34 13 31 51338 B> 21
3376 308079 681 13 01 51 34 13 31 51338 <A 42
3377 308755 5 13 01 51 34 13 31 <A 42339
3378 308757 3 13 01 51 34 13 <B 42340
3379 308760 4 13 01 51 34 31 B> 42340
3380 309440 684 13 01 51 34 31 04340 B>
3381 309441 683 13 01 51 34 31 04340 <A 10
3382 309442 684 13 01 51 34 31 04339 01 B> 10
3383 309444 686 13 01 51 34 31 04339 01 31 B>
3384 309445 685 13 01 51 34 31 04339 01 31 <A 10
3385 309447 683 13 01 51 34 31 04339 01 <B 42 10
3386 309448 684 13 01 51 34 31 04339 03 A> 42 10
3387 309450 686 13 01 51 34 31 04339 03 15 A> 10
3388 309451 685 13 01 51 34 31 04339 03 15 <B 20
3389 309453 683 13 01 51 34 31 04339 03 <B 24 20
3390 309455 681 13 01 51 34 31 04339 <A 14 24 20
3391 309456 682 13 01 51 34 31 04338 01 B> 14 24 20
3392 309458 684 13 01 51 34 31 04338 01 31 B> 24 20
3393 309460 686 13 01 51 34 31 04338 01 31 51 B> 20
3394 309462 688 13 01 51 34 31 04338 01 31 512 B>
3395 309463 687 13 01 51 34 31 04338 01 31 512 <A 10
3396 309467 683 13 01 51 34 31 04338 01 31 <A 422 10
3397 309469 681 13 01 51 34 31 04338 01 <B 423 10
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* [*]* [*]* 042+V(1) 01 <B 421+V(2) 10
1 1 1 [*]* [*]* [*]* [*]* [*]* 042+V(1) 03 A> 421+V(2) 10
2 3+2*V(2) 3+2*V(2) [*]* [*]* [*]* [*]* [*]* 042+V(1) 03 151+V(2) A> 10
3 4+2*V(2) 2+2*V(2) [*]* [*]* [*]* [*]* [*]* 042+V(1) 03 151+V(2) <B 20
4 6+4*V(2) 0 [*]* [*]* [*]* [*]* [*]* 042+V(1) 03 <B 241+V(2) 20
5 8+4*V(2) -2 [*]* [*]* [*]* [*]* [*]* 042+V(1) <A 14 241+V(2) 20
6 9+4*V(2) -1 [*]* [*]* [*]* [*]* [*]* 041+V(1) 01 B> 14 241+V(2) 20
7 11+4*V(2) 1 [*]* [*]* [*]* [*]* [*]* 041+V(1) 01 31 B> 241+V(2) 20
8 13+6*V(2) 3+2*V(2) [*]* [*]* [*]* [*]* [*]* 041+V(1) 01 31 511+V(2) B> 20
9 15+6*V(2) 5+2*V(2) [*]* [*]* [*]* [*]* [*]* 041+V(1) 01 31 512+V(2) B>
10 16+6*V(2) 4+2*V(2) [*]* [*]* [*]* [*]* [*]* 041+V(1) 01 31 512+V(2) <A 10
11 20+8*V(2) 0 [*]* [*]* [*]* [*]* [*]* 041+V(1) 01 31 <A 422+V(2) 10
12 22+8*V(2) -2 [*]* [*]* [*]* [*]* [*]* 041+V(1) 01 <B 423+V(2) 10
<< Success! ==> defined new CTR 6 (PA)
3397 309469 681 13 01 51 34 31 04338 01 <B 423 10
== Executing PA-CTR 6, V(1)=336, V(2)=2, repcount=337, factor=2/1
7441 1228131 7 13 01 51 34 31 04 01 <B 42677 10
7442 1228132 8 13 01 51 34 31 04 03 A> 42677 10
7443 1229486 1362 13 01 51 34 31 04 03 15677 A> 10
7444 1229487 1361 13 01 51 34 31 04 03 15677 <B 20
7445 1230841 7 13 01 51 34 31 04 03 <B 24677 20
7446 1230843 5 13 01 51 34 31 04 <A 14 24677 20
7447 1230844 6 13 01 51 34 31 01 B> 14 24677 20
7448 1230846 8 13 01 51 34 31 01 31 B> 24677 20
7449 1232200 1362 13 01 51 34 31 01 31 51677 B> 20
7450 1232202 1364 13 01 51 34 31 01 31 51678 B>
7451 1232203 1363 13 01 51 34 31 01 31 51678 <A 10
7452 1233559 7 13 01 51 34 31 01 31 <A 42678 10
7453 1233561 5 13 01 51 34 31 01 <B 42679 10
7454 1233562 6 13 01 51 34 31 03 A> 42679 10
7455 1234920 1364 13 01 51 34 31 03 15679 A> 10
7456 1234921 1363 13 01 51 34 31 03 15679 <B 20
7457 1236279 5 13 01 51 34 31 03 <B 24679 20
7458 1236281 3 13 01 51 34 31 <A 14 24679 20
7459 1236283 1 13 01 51 34 <B 42 14 24679 20
7460 1236284 2 13 01 51 30 A> 42 14 24679 20
7461 1236286 4 13 01 51 30 15 A> 14 24679 20
7462 1236287 3 13 01 51 30 15 <B 24680 20
7463 1236289 1 13 01 51 30 <B 24681 20
7464 1236291 -1 13 01 51 <A 11 24681 20
7465 1236293 -3 13 01 <A 42 11 24681 20
7466 1236295 -5 13 <A 12 42 11 24681 20
7467 1236297 -7 <B 21 12 42 11 24681 20
7468 1236300 -6 13 A> 21 12 42 11 24681 20
7469 1236302 -4 13 43 A> 12 42 11 24681 20
7470 1236303 -5 13 43 <B 22 42 11 24681 20
7471 1236306 -4 13 01 B> 22 42 11 24681 20
7472 1236308 -2 13 01 54 B> 42 11 24681 20
7473 1236310 0 13 01 54 04 B> 11 24681 20
7474 1236313 -1 13 01 54 04 <B 42 24681 20
7475 1236314 0 13 01 54 00 A> 42 24681 20
7476 1236316 2 13 01 54 00 15 A> 24681 20
7477 1237678 1364 13 01 54 00 15 40681 A> 20
7478 1237682 1366 13 01 54 00 15 40681 13 A>
7479 1237685 1365 13 01 54 00 15 40681 13 <B 21
7480 1237688 1366 13 01 54 00 15 40681 31 B> 21
7481 1237691 1365 13 01 54 00 15 40681 31 <A 42
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 13 01 51 34 31 04 01 <B 421+V(1) 10
1 1 1 13 01 51 34 31 04 03 A> 421+V(1) 10
2 3+2*V(1) 3+2*V(1) 13 01 51 34 31 04 03 151+V(1) A> 10
3 4+2*V(1) 2+2*V(1) 13 01 51 34 31 04 03 151+V(1) <B 20
4 6+4*V(1) 0 13 01 51 34 31 04 03 <B 241+V(1) 20
5 8+4*V(1) -2 13 01 51 34 31 04 <A 14 241+V(1) 20
6 9+4*V(1) -1 13 01 51 34 31 01 B> 14 241+V(1) 20
7 11+4*V(1) 1 13 01 51 34 31 01 31 B> 241+V(1) 20
8 13+6*V(1) 3+2*V(1) 13 01 51 34 31 01 31 511+V(1) B> 20
9 15+6*V(1) 5+2*V(1) 13 01 51 34 31 01 31 512+V(1) B>
10 16+6*V(1) 4+2*V(1) 13 01 51 34 31 01 31 512+V(1) <A 10
11 20+8*V(1) 0 13 01 51 34 31 01 31 <A 422+V(1) 10
12 22+8*V(1) -2 13 01 51 34 31 01 <B 423+V(1) 10
13 23+8*V(1) -1 13 01 51 34 31 03 A> 423+V(1) 10
14 29+10*V(1) 5+2*V(1) 13 01 51 34 31 03 153+V(1) A> 10
15 30+10*V(1) 4+2*V(1) 13 01 51 34 31 03 153+V(1) <B 20
16 36+12*V(1) -2 13 01 51 34 31 03 <B 243+V(1) 20
17 38+12*V(1) -4 13 01 51 34 31 <A 14 243+V(1) 20
18 40+12*V(1) -6 13 01 51 34 <B 42 14 243+V(1) 20
19 41+12*V(1) -5 13 01 51 30 A> 42 14 243+V(1) 20
20 43+12*V(1) -3 13 01 51 30 15 A> 14 243+V(1) 20
21 44+12*V(1) -4 13 01 51 30 15 <B 244+V(1) 20
22 46+12*V(1) -6 13 01 51 30 <B 245+V(1) 20
23 48+12*V(1) -8 13 01 51 <A 11 245+V(1) 20
24 50+12*V(1) -10 13 01 <A 42 11 245+V(1) 20
25 52+12*V(1) -12 13 <A 12 42 11 245+V(1) 20
26 54+12*V(1) -14 <B 21 12 42 11 245+V(1) 20
27 57+12*V(1) -13 13 A> 21 12 42 11 245+V(1) 20
28 59+12*V(1) -11 13 43 A> 12 42 11 245+V(1) 20
29 60+12*V(1) -12 13 43 <B 22 42 11 245+V(1) 20
30 63+12*V(1) -11 13 01 B> 22 42 11 245+V(1) 20
31 65+12*V(1) -9 13 01 54 B> 42 11 245+V(1) 20
32 67+12*V(1) -7 13 01 54 04 B> 11 245+V(1) 20
33 70+12*V(1) -8 13 01 54 04 <B 42 245+V(1) 20
34 71+12*V(1) -7 13 01 54 00 A> 42 245+V(1) 20
35 73+12*V(1) -5 13 01 54 00 15 A> 245+V(1) 20
36 83+14*V(1) 5+2*V(1) 13 01 54 00 15 405+V(1) A> 20
37 87+14*V(1) 7+2*V(1) 13 01 54 00 15 405+V(1) 13 A>
38 90+14*V(1) 6+2*V(1) 13 01 54 00 15 405+V(1) 13 <B 21
39 93+14*V(1) 7+2*V(1) 13 01 54 00 15 405+V(1) 31 B> 21
40 96+14*V(1) 6+2*V(1) 13 01 54 00 15 405+V(1) 31 <A 42
<< Success! ==> defined new CTR 7 (PPA)
7481 1237691 1365 13 01 54 00 15 40681 31 <A 42
== Executing PA-CTR 5, V(1)=679, V(2)=0, repcount=680, factor=2/1
13601 4951851 5 13 01 54 00 15 40 31 <A 421361
13602 4951853 3 13 01 54 00 15 40 <B 421362
13603 4951856 4 13 01 54 00 15 13 A> 421362
13604 4954580 2728 13 01 54 00 15 13 151362 A>
13605 4954583 2727 13 01 54 00 15 13 151362 <B 21
13606 4957307 3 13 01 54 00 15 13 <B 241362 21
13607 4957310 4 13 01 54 00 15 31 B> 241362 21
13608 4960034 2728 13 01 54 00 15 31 511362 B> 21
13609 4960037 2727 13 01 54 00 15 31 511362 <A 42
13610 4962761 3 13 01 54 00 15 31 <A 421363
13611 4962763 1 13 01 54 00 15 <B 421364
13612 4962765 -1 13 01 54 00 <B 24 421364
13613 4962768 0 13 01 54 13 A> 24 421364
13614 4962770 2 13 01 54 13 40 A> 421364
13615 4965498 2730 13 01 54 13 40 151364 A>
13616 4965501 2729 13 01 54 13 40 151364 <B 21
13617 4968229 1 13 01 54 13 40 <B 241364 21
13618 4968232 2 13 01 54 132 A> 241364 21
13619 4970960 2730 13 01 54 132 401364 A> 21
13620 4970962 2732 13 01 54 132 401364 43 A>
13621 4970965 2731 13 01 54 132 401364 43 <B 21
13622 4970968 2732 13 01 54 132 401364 01 B> 21
13623 4970971 2731 13 01 54 132 401364 01 <A 42
13624 4970973 2729 13 01 54 132 401364 <A 12 42
13625 4970974 2730 13 01 54 132 401363 41 B> 12 42
13626 4970976 2732 13 01 54 132 401363 41 34 B> 42
13627 4970978 2734 13 01 54 132 401363 41 34 04 B>
13628 4970979 2733 13 01 54 132 401363 41 34 04 <A 10
13629 4970980 2734 13 01 54 132 401363 41 34 01 B> 10
13630 4970982 2736 13 01 54 132 401363 41 34 01 31 B>
13631 4970983 2735 13 01 54 132 401363 41 34 01 31 <A 10
13632 4970985 2733 13 01 54 132 401363 41 34 01 <B 42 10
13633 4970986 2734 13 01 54 132 401363 41 34 03 A> 42 10
13634 4970988 2736 13 01 54 132 401363 41 34 03 15 A> 10
13635 4970989 2735 13 01 54 132 401363 41 34 03 15 <B 20
13636 4970991 2733 13 01 54 132 401363 41 34 03 <B 24 20
13637 4970993 2731 13 01 54 132 401363 41 34 <A 14 24 20
13638 4970994 2732 13 01 54 132 401363 41 31 B> 14 24 20
13639 4970996 2734 13 01 54 132 401363 41 312 B> 24 20
13640 4970998 2736 13 01 54 132 401363 41 312 51 B> 20
13641 4971000 2738 13 01 54 132 401363 41 312 512 B>
13642 4971001 2737 13 01 54 132 401363 41 312 512 <A 10
13643 4971005 2733 13 01 54 132 401363 41 312 <A 422 10
13644 4971007 2731 13 01 54 132 401363 41 31 <B 423 10
13645 4971008 2732 13 01 54 132 401363 41 33 A> 423 10
13646 4971014 2738 13 01 54 132 401363 41 33 153 A> 10
13647 4971015 2737 13 01 54 132 401363 41 33 153 <B 20
13648 4971021 2731 13 01 54 132 401363 41 33 <B 243 20
13649 4971023 2729 13 01 54 132 401363 41 <B 44 243 20
13650 4971024 2730 13 01 54 132 401363 43 A> 44 243 20
13651 4971026 2732 13 01 54 132 401363 43 10 A> 243 20
13652 4971032 2738 13 01 54 132 401363 43 10 403 A> 20
13653 4971036 2740 13 01 54 132 401363 43 10 403 13 A>
13654 4971039 2739 13 01 54 132 401363 43 10 403 13 <B 21
13655 4971042 2740 13 01 54 132 401363 43 10 403 31 B> 21
13656 4971045 2739 13 01 54 132 401363 43 10 403 31 <A 42
13657 4971047 2737 13 01 54 132 401363 43 10 403 <B 422
13658 4971050 2738 13 01 54 132 401363 43 10 402 13 A> 422
13659 4971054 2742 13 01 54 132 401363 43 10 402 13 152 A>
13660 4971057 2741 13 01 54 132 401363 43 10 402 13 152 <B 21
13661 4971061 2737 13 01 54 132 401363 43 10 402 13 <B 242 21
13662 4971064 2738 13 01 54 132 401363 43 10 402 31 B> 242 21
13663 4971068 2742 13 01 54 132 401363 43 10 402 31 512 B> 21
13664 4971071 2741 13 01 54 132 401363 43 10 402 31 512 <A 42
13665 4971075 2737 13 01 54 132 401363 43 10 402 31 <A 423
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 402+V(1) 31 <A 421+V(2)
1 2 -2 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 402+V(1) <B 422+V(2)
2 5 -1 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 401+V(1) 13 A> 422+V(2)
3 9+2*V(2) 3+2*V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 401+V(1) 13 152+V(2) A>
4 12+2*V(2) 2+2*V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 401+V(1) 13 152+V(2) <B 21
5 16+4*V(2) -2 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 401+V(1) 13 <B 242+V(2) 21
6 19+4*V(2) -1 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 401+V(1) 31 B> 242+V(2) 21
7 23+6*V(2) 3+2*V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 401+V(1) 31 512+V(2) B> 21
8 26+6*V(2) 2+2*V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 401+V(1) 31 512+V(2) <A 42
9 30+8*V(2) -2 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 401+V(1) 31 <A 423+V(2)
<< Success! ==> defined new CTR 8 (PA)
13665 4971075 2737 13 01 54 132 401363 43 10 402 31 <A 423
== Executing PA-CTR 8, V(1)=0, V(2)=2, repcount=1, factor=2/1
13674 4971121 2735 13 01 54 132 401363 43 10 40 31 <A 425
13675 4971123 2733 13 01 54 132 401363 43 10 40 <B 426
13676 4971126 2734 13 01 54 132 401363 43 10 13 A> 426
13677 4971138 2746 13 01 54 132 401363 43 10 13 156 A>
13678 4971141 2745 13 01 54 132 401363 43 10 13 156 <B 21
13679 4971153 2733 13 01 54 132 401363 43 10 13 <B 246 21
13680 4971156 2734 13 01 54 132 401363 43 10 31 B> 246 21
13681 4971168 2746 13 01 54 132 401363 43 10 31 516 B> 21
13682 4971171 2745 13 01 54 132 401363 43 10 31 516 <A 42
13683 4971183 2733 13 01 54 132 401363 43 10 31 <A 427
13684 4971185 2731 13 01 54 132 401363 43 10 <B 428
13685 4971187 2729 13 01 54 132 401363 43 <B 21 428
13686 4971190 2730 13 01 54 132 401363 01 B> 21 428
13687 4971193 2729 13 01 54 132 401363 01 <A 429
13688 4971195 2727 13 01 54 132 401363 <A 12 429
13689 4971196 2728 13 01 54 132 401362 41 B> 12 429
13690 4971198 2730 13 01 54 132 401362 41 34 B> 429
13691 4971216 2748 13 01 54 132 401362 41 34 049 B>
13692 4971217 2747 13 01 54 132 401362 41 34 049 <A 10
13693 4971218 2748 13 01 54 132 401362 41 34 048 01 B> 10
13694 4971220 2750 13 01 54 132 401362 41 34 048 01 31 B>
13695 4971221 2749 13 01 54 132 401362 41 34 048 01 31 <A 10
13696 4971223 2747 13 01 54 132 401362 41 34 048 01 <B 42 10
13697 4971224 2748 13 01 54 132 401362 41 34 048 03 A> 42 10
13698 4971226 2750 13 01 54 132 401362 41 34 048 03 15 A> 10
13699 4971227 2749 13 01 54 132 401362 41 34 048 03 15 <B 20
13700 4971229 2747 13 01 54 132 401362 41 34 048 03 <B 24 20
13701 4971231 2745 13 01 54 132 401362 41 34 048 <A 14 24 20
13702 4971232 2746 13 01 54 132 401362 41 34 047 01 B> 14 24 20
13703 4971234 2748 13 01 54 132 401362 41 34 047 01 31 B> 24 20
13704 4971236 2750 13 01 54 132 401362 41 34 047 01 31 51 B> 20
13705 4971238 2752 13 01 54 132 401362 41 34 047 01 31 512 B>
13706 4971239 2751 13 01 54 132 401362 41 34 047 01 31 512 <A 10
13707 4971243 2747 13 01 54 132 401362 41 34 047 01 31 <A 422 10
13708 4971245 2745 13 01 54 132 401362 41 34 047 01 <B 423 10
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 042+V(1) 01 <B 421+V(2) 10
1 1 1 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 042+V(1) 03 A> 421+V(2) 10
2 3+2*V(2) 3+2*V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 042+V(1) 03 151+V(2) A> 10
3 4+2*V(2) 2+2*V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 042+V(1) 03 151+V(2) <B 20
4 6+4*V(2) 0 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 042+V(1) 03 <B 241+V(2) 20
5 8+4*V(2) -2 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 042+V(1) <A 14 241+V(2) 20
6 9+4*V(2) -1 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 041+V(1) 01 B> 14 241+V(2) 20
7 11+4*V(2) 1 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 041+V(1) 01 31 B> 241+V(2) 20
8 13+6*V(2) 3+2*V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 041+V(1) 01 31 511+V(2) B> 20
9 15+6*V(2) 5+2*V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 041+V(1) 01 31 512+V(2) B>
10 16+6*V(2) 4+2*V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 041+V(1) 01 31 512+V(2) <A 10
11 20+8*V(2) 0 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 041+V(1) 01 31 <A 422+V(2) 10
12 22+8*V(2) -2 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 041+V(1) 01 <B 423+V(2) 10
<< Success! ==> defined new CTR 9 (PA)
13708 4971245 2745 13 01 54 132 401362 41 34 047 01 <B 423 10
== Executing PA-CTR 9, V(1)=5, V(2)=2, repcount=6, factor=2/1
13780 4971713 2733 13 01 54 132 401362 41 34 04 01 <B 4215 10
13781 4971714 2734 13 01 54 132 401362 41 34 04 03 A> 4215 10
13782 4971744 2764 13 01 54 132 401362 41 34 04 03 1515 A> 10
13783 4971745 2763 13 01 54 132 401362 41 34 04 03 1515 <B 20
13784 4971775 2733 13 01 54 132 401362 41 34 04 03 <B 2415 20
13785 4971777 2731 13 01 54 132 401362 41 34 04 <A 14 2415 20
13786 4971778 2732 13 01 54 132 401362 41 34 01 B> 14 2415 20
13787 4971780 2734 13 01 54 132 401362 41 34 01 31 B> 2415 20
13788 4971810 2764 13 01 54 132 401362 41 34 01 31 5115 B> 20
13789 4971812 2766 13 01 54 132 401362 41 34 01 31 5116 B>
13790 4971813 2765 13 01 54 132 401362 41 34 01 31 5116 <A 10
13791 4971845 2733 13 01 54 132 401362 41 34 01 31 <A 4216 10
13792 4971847 2731 13 01 54 132 401362 41 34 01 <B 4217 10
13793 4971848 2732 13 01 54 132 401362 41 34 03 A> 4217 10
13794 4971882 2766 13 01 54 132 401362 41 34 03 1517 A> 10
13795 4971883 2765 13 01 54 132 401362 41 34 03 1517 <B 20
13796 4971917 2731 13 01 54 132 401362 41 34 03 <B 2417 20
13797 4971919 2729 13 01 54 132 401362 41 34 <A 14 2417 20
13798 4971920 2730 13 01 54 132 401362 41 31 B> 14 2417 20
13799 4971922 2732 13 01 54 132 401362 41 312 B> 2417 20
13800 4971956 2766 13 01 54 132 401362 41 312 5117 B> 20
13801 4971958 2768 13 01 54 132 401362 41 312 5118 B>
13802 4971959 2767 13 01 54 132 401362 41 312 5118 <A 10
13803 4971995 2731 13 01 54 132 401362 41 312 <A 4218 10
13804 4971997 2729 13 01 54 132 401362 41 31 <B 4219 10
13805 4971998 2730 13 01 54 132 401362 41 33 A> 4219 10
13806 4972036 2768 13 01 54 132 401362 41 33 1519 A> 10
13807 4972037 2767 13 01 54 132 401362 41 33 1519 <B 20
13808 4972075 2729 13 01 54 132 401362 41 33 <B 2419 20
13809 4972077 2727 13 01 54 132 401362 41 <B 44 2419 20
13810 4972078 2728 13 01 54 132 401362 43 A> 44 2419 20
13811 4972080 2730 13 01 54 132 401362 43 10 A> 2419 20
13812 4972118 2768 13 01 54 132 401362 43 10 4019 A> 20
13813 4972122 2770 13 01 54 132 401362 43 10 4019 13 A>
13814 4972125 2769 13 01 54 132 401362 43 10 4019 13 <B 21
13815 4972128 2770 13 01 54 132 401362 43 10 4019 31 B> 21
13816 4972131 2769 13 01 54 132 401362 43 10 4019 31 <A 42
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 [*]* [*]* [*]* [*]* [*]* 41 34 04 01 <B 421+V(1) 10
1 1 1 [*]* [*]* [*]* [*]* [*]* 41 34 04 03 A> 421+V(1) 10
2 3+2*V(1) 3+2*V(1) [*]* [*]* [*]* [*]* [*]* 41 34 04 03 151+V(1) A> 10
3 4+2*V(1) 2+2*V(1) [*]* [*]* [*]* [*]* [*]* 41 34 04 03 151+V(1) <B 20
4 6+4*V(1) 0 [*]* [*]* [*]* [*]* [*]* 41 34 04 03 <B 241+V(1) 20
5 8+4*V(1) -2 [*]* [*]* [*]* [*]* [*]* 41 34 04 <A 14 241+V(1) 20
6 9+4*V(1) -1 [*]* [*]* [*]* [*]* [*]* 41 34 01 B> 14 241+V(1) 20
7 11+4*V(1) 1 [*]* [*]* [*]* [*]* [*]* 41 34 01 31 B> 241+V(1) 20
8 13+6*V(1) 3+2*V(1) [*]* [*]* [*]* [*]* [*]* 41 34 01 31 511+V(1) B> 20
9 15+6*V(1) 5+2*V(1) [*]* [*]* [*]* [*]* [*]* 41 34 01 31 512+V(1) B>
10 16+6*V(1) 4+2*V(1) [*]* [*]* [*]* [*]* [*]* 41 34 01 31 512+V(1) <A 10
11 20+8*V(1) 0 [*]* [*]* [*]* [*]* [*]* 41 34 01 31 <A 422+V(1) 10
12 22+8*V(1) -2 [*]* [*]* [*]* [*]* [*]* 41 34 01 <B 423+V(1) 10
13 23+8*V(1) -1 [*]* [*]* [*]* [*]* [*]* 41 34 03 A> 423+V(1) 10
14 29+10*V(1) 5+2*V(1) [*]* [*]* [*]* [*]* [*]* 41 34 03 153+V(1) A> 10
15 30+10*V(1) 4+2*V(1) [*]* [*]* [*]* [*]* [*]* 41 34 03 153+V(1) <B 20
16 36+12*V(1) -2 [*]* [*]* [*]* [*]* [*]* 41 34 03 <B 243+V(1) 20
17 38+12*V(1) -4 [*]* [*]* [*]* [*]* [*]* 41 34 <A 14 243+V(1) 20
18 39+12*V(1) -3 [*]* [*]* [*]* [*]* [*]* 41 31 B> 14 243+V(1) 20
19 41+12*V(1) -1 [*]* [*]* [*]* [*]* [*]* 41 312 B> 243+V(1) 20
20 47+14*V(1) 5+2*V(1) [*]* [*]* [*]* [*]* [*]* 41 312 513+V(1) B> 20
21 49+14*V(1) 7+2*V(1) [*]* [*]* [*]* [*]* [*]* 41 312 514+V(1) B>
22 50+14*V(1) 6+2*V(1) [*]* [*]* [*]* [*]* [*]* 41 312 514+V(1) <A 10
23 58+16*V(1) -2 [*]* [*]* [*]* [*]* [*]* 41 312 <A 424+V(1) 10
24 60+16*V(1) -4 [*]* [*]* [*]* [*]* [*]* 41 31 <B 425+V(1) 10
25 61+16*V(1) -3 [*]* [*]* [*]* [*]* [*]* 41 33 A> 425+V(1) 10
26 71+18*V(1) 7+2*V(1) [*]* [*]* [*]* [*]* [*]* 41 33 155+V(1) A> 10
27 72+18*V(1) 6+2*V(1) [*]* [*]* [*]* [*]* [*]* 41 33 155+V(1) <B 20
28 82+20*V(1) -4 [*]* [*]* [*]* [*]* [*]* 41 33 <B 245+V(1) 20
29 84+20*V(1) -6 [*]* [*]* [*]* [*]* [*]* 41 <B 44 245+V(1) 20
30 85+20*V(1) -5 [*]* [*]* [*]* [*]* [*]* 43 A> 44 245+V(1) 20
31 87+20*V(1) -3 [*]* [*]* [*]* [*]* [*]* 43 10 A> 245+V(1) 20
32 97+22*V(1) 7+2*V(1) [*]* [*]* [*]* [*]* [*]* 43 10 405+V(1) A> 20
33 101+22*V(1) 9+2*V(1) [*]* [*]* [*]* [*]* [*]* 43 10 405+V(1) 13 A>
34 104+22*V(1) 8+2*V(1) [*]* [*]* [*]* [*]* [*]* 43 10 405+V(1) 13 <B 21
35 107+22*V(1) 9+2*V(1) [*]* [*]* [*]* [*]* [*]* 43 10 405+V(1) 31 B> 21
36 110+22*V(1) 8+2*V(1) [*]* [*]* [*]* [*]* [*]* 43 10 405+V(1) 31 <A 42
<< Success! ==> defined new CTR 10 (PPA)
13816 4972131 2769 13 01 54 132 401362 43 10 4019 31 <A 42
== Executing PA-CTR 8, V(1)=17, V(2)=0, repcount=18, factor=2/1
13978 4975119 2733 13 01 54 132 401362 43 10 40 31 <A 4237
13979 4975121 2731 13 01 54 132 401362 43 10 40 <B 4238
13980 4975124 2732 13 01 54 132 401362 43 10 13 A> 4238
13981 4975200 2808 13 01 54 132 401362 43 10 13 1538 A>
13982 4975203 2807 13 01 54 132 401362 43 10 13 1538 <B 21
13983 4975279 2731 13 01 54 132 401362 43 10 13 <B 2438 21
13984 4975282 2732 13 01 54 132 401362 43 10 31 B> 2438 21
13985 4975358 2808 13 01 54 132 401362 43 10 31 5138 B> 21
13986 4975361 2807 13 01 54 132 401362 43 10 31 5138 <A 42
13987 4975437 2731 13 01 54 132 401362 43 10 31 <A 4239
13988 4975439 2729 13 01 54 132 401362 43 10 <B 4240
13989 4975441 2727 13 01 54 132 401362 43 <B 21 4240
13990 4975444 2728 13 01 54 132 401362 01 B> 21 4240
13991 4975447 2727 13 01 54 132 401362 01 <A 4241
13992 4975449 2725 13 01 54 132 401362 <A 12 4241
13993 4975450 2726 13 01 54 132 401361 41 B> 12 4241
13994 4975452 2728 13 01 54 132 401361 41 34 B> 4241
13995 4975534 2810 13 01 54 132 401361 41 34 0441 B>
13996 4975535 2809 13 01 54 132 401361 41 34 0441 <A 10
13997 4975536 2810 13 01 54 132 401361 41 34 0440 01 B> 10
13998 4975538 2812 13 01 54 132 401361 41 34 0440 01 31 B>
13999 4975539 2811 13 01 54 132 401361 41 34 0440 01 31 <A 10
14000 4975541 2809 13 01 54 132 401361 41 34 0440 01 <B 42 10
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* [*]* 402+V(1) 43 10 40 31 <A 421+V(2)
1 2 -2 [*]* [*]* [*]* [*]* 402+V(1) 43 10 40 <B 422+V(2)
2 5 -1 [*]* [*]* [*]* [*]* 402+V(1) 43 10 13 A> 422+V(2)
3 9+2*V(2) 3+2*V(2) [*]* [*]* [*]* [*]* 402+V(1) 43 10 13 152+V(2) A>
4 12+2*V(2) 2+2*V(2) [*]* [*]* [*]* [*]* 402+V(1) 43 10 13 152+V(2) <B 21
5 16+4*V(2) -2 [*]* [*]* [*]* [*]* 402+V(1) 43 10 13 <B 242+V(2) 21
6 19+4*V(2) -1 [*]* [*]* [*]* [*]* 402+V(1) 43 10 31 B> 242+V(2) 21
7 23+6*V(2) 3+2*V(2) [*]* [*]* [*]* [*]* 402+V(1) 43 10 31 512+V(2) B> 21
8 26+6*V(2) 2+2*V(2) [*]* [*]* [*]* [*]* 402+V(1) 43 10 31 512+V(2) <A 42
9 30+8*V(2) -2 [*]* [*]* [*]* [*]* 402+V(1) 43 10 31 <A 423+V(2)
10 32+8*V(2) -4 [*]* [*]* [*]* [*]* 402+V(1) 43 10 <B 424+V(2)
11 34+8*V(2) -6 [*]* [*]* [*]* [*]* 402+V(1) 43 <B 21 424+V(2)
12 37+8*V(2) -5 [*]* [*]* [*]* [*]* 402+V(1) 01 B> 21 424+V(2)
13 40+8*V(2) -6 [*]* [*]* [*]* [*]* 402+V(1) 01 <A 425+V(2)
14 42+8*V(2) -8 [*]* [*]* [*]* [*]* 402+V(1) <A 12 425+V(2)
15 43+8*V(2) -7 [*]* [*]* [*]* [*]* 401+V(1) 41 B> 12 425+V(2)
16 45+8*V(2) -5 [*]* [*]* [*]* [*]* 401+V(1) 41 34 B> 425+V(2)
17 55+10*V(2) 5+2*V(2) [*]* [*]* [*]* [*]* 401+V(1) 41 34 045+V(2) B>
18 56+10*V(2) 4+2*V(2) [*]* [*]* [*]* [*]* 401+V(1) 41 34 045+V(2) <A 10
19 57+10*V(2) 5+2*V(2) [*]* [*]* [*]* [*]* 401+V(1) 41 34 044+V(2) 01 B> 10
20 59+10*V(2) 7+2*V(2) [*]* [*]* [*]* [*]* 401+V(1) 41 34 044+V(2) 01 31 B>
21 60+10*V(2) 6+2*V(2) [*]* [*]* [*]* [*]* 401+V(1) 41 34 044+V(2) 01 31 <A 10
22 62+10*V(2) 4+2*V(2) [*]* [*]* [*]* [*]* 401+V(1) 41 34 044+V(2) 01 <B 42 10
<< Success! ==> defined new CTR 11 (PPA)
14000 4975541 2809 13 01 54 132 401361 41 34 0440 01 <B 42 10
== Executing PA-CTR 9, V(1)=38, V(2)=0, repcount=39, factor=2/1
14468 4988255 2731 13 01 54 132 401361 41 34 04 01 <B 4279 10
== Executing PPA-CTR 10 (once), V(1)=78
14504 4990081 2895 13 01 54 132 401361 43 10 4083 31 <A 42
== Executing PA-CTR 8, V(1)=81, V(2)=0, repcount=82, factor=2/1
15242 5045677 2731 13 01 54 132 401361 43 10 40 31 <A 42165
== Executing PPA-CTR 11 (once), V(1)=1359, V(2)=164
15264 5047379 3063 13 01 54 132 401360 41 34 04168 01 <B 42 10
== Executing PA-CTR 9, V(1)=166, V(2)=0, repcount=167, factor=2/1
17268 5272829 2729 13 01 54 132 401360 41 34 04 01 <B 42335 10
== Executing PPA-CTR 10 (once), V(1)=334
17304 5280287 3405 13 01 54 132 401360 43 10 40339 31 <A 42
== Executing PA-CTR 8, V(1)=337, V(2)=0, repcount=338, factor=2/1
20346 6201675 2729 13 01 54 132 401360 43 10 40 31 <A 42677
== Executing PPA-CTR 11 (once), V(1)=1358, V(2)=676
20368 6208497 4085 13 01 54 132 401359 41 34 04680 01 <B 42 10
== Executing PA-CTR 9, V(1)=678, V(2)=0, repcount=679, factor=2/1
28516 9906331 2727 13 01 54 132 401359 41 34 04 01 <B 421359 10
== Executing PPA-CTR 10 (once), V(1)=1358
28552 9936317 5451 13 01 54 132 401359 43 10 401363 31 <A 42
== Executing PA-CTR 8, V(1)=1361, V(2)=0, repcount=1362, factor=2/1
40810 24806633 2727 13 01 54 132 401359 43 10 40 31 <A 422725
== Executing PPA-CTR 11 (once), V(1)=1357, V(2)=2724
40832 24833935 8179 13 01 54 132 401358 41 34 042728 01 <B 42 10
== Executing PA-CTR 9, V(1)=2726, V(2)=0, repcount=2727, factor=2/1
73556 84364345 2725 13 01 54 132 401358 41 34 04 01 <B 425455 10
== Executing PPA-CTR 10 (once), V(1)=5454
73592 84484443 13641 13 01 54 132 401358 43 10 405459 31 <A 42
== Executing PA-CTR 8, V(1)=5457, V(2)=0, repcount=5458, factor=2/1
122714 322922631 2725 13 01 54 132 401358 43 10 40 31 <A 4210917
== Executing PPA-CTR 11 (once), V(1)=1356, V(2)=10916
122736 323031853 24561 13 01 54 132 401357 41 34 0410920 01 <B 42 10
== Executing PA-CTR 9, V(1)=10918, V(2)=0, repcount=10919, factor=2/1
253764 1276981207 2723 13 01 54 132 401357 41 34 04 01 <B 4221839 10
== Executing PPA-CTR 10 (once), V(1)=21838
253800 1277461753 46407 13 01 54 132 401357 43 10 4021843 31 <A 42
== Executing PA-CTR 8, V(1)=21841, V(2)=0, repcount=21842, factor=2/1
450378 5094525989 2723 13 01 54 132 401357 43 10 40 31 <A 4243685
== Executing PPA-CTR 11 (once), V(1)=1355, V(2)=43684
450400 5094962891 90095 13 01 54 132 401356 41 34 0443688 01 <B 42 10
== Executing PA-CTR 9, V(1)=43686, V(2)=0, repcount=43687, factor=2/1
974644 20364006261 2721 13 01 54 132 401356 41 34 04 01 <B 4287375 10
== Executing PPA-CTR 10 (once), V(1)=87374
974680 20365928599 177477 13 01 54 132 401356 43 10 4087379 31 <A 42
== Executing PA-CTR 8, V(1)=87377, V(2)=0, repcount=87378, factor=2/1
1761082 81447169987 2721 13 01 54 132 401356 43 10 40 31 <A 42174757
== Executing PPA-CTR 11 (once), V(1)=1354, V(2)=174756
1761104 81448917609 352237 13 01 54 132 401355 41 34 04174760 01 <B 42 10
== Executing PA-CTR 9, V(1)=174758, V(2)=0, repcount=174759, factor=2/1
3858212 325777028883 2719 13 01 54 132 401355 41 34 04 01 <B 42349519 10
== Executing PPA-CTR 10 (once), V(1)=349518
3858248 325784718389 701763 13 01 54 132 401355 43 10 40349523 31 <A 42
== Executing PA-CTR 8, V(1)=349521, V(2)=0, repcount=349522, factor=2/1
7003946 1303117435745 2719 13 01 54 132 401355 43 10 40 31 <A 42699045
== Executing PPA-CTR 11 (once), V(1)=1353, V(2)=699044
7003968 1303124426247 1400811 13 01 54 132 401354 41 34 04699048 01 <B 42 10
== Executing PA-CTR 9, V(1)=699046, V(2)=0, repcount=699047, factor=2/1
15392532 5212467878577 2717 13 01 54 132 401354 41 34 04 01 <B 421398095 10
== Executing PPA-CTR 10 (once), V(1)=1398094
15392568 5212498636755 2798913 13 01 54 132 401354 43 10 401398099 31 <A 42
== Executing PA-CTR 8, V(1)=1398097, V(2)=0, repcount=1398098, factor=2/1
27975450 20849953535743 2717 13 01 54 132 401354 43 10 40 31 <A 422796197
== Executing PPA-CTR 11 (once), V(1)=1352, V(2)=2796196
27975472 20849981497765 5595113 13 01 54 132 401353 41 34 042796200 01 <B 42 10
== Executing PA-CTR 9, V(1)=2796198, V(2)=0, repcount=2796199, factor=2/1
61529860 83399851425359 2715 13 01 54 132 401353 41 34 04 01 <B 425592399 10
== Executing PPA-CTR 10 (once), V(1)=5592398
61529896 83399974458225 11187519 13 01 54 132 401353 43 10 405592403 31 <A 42
== Executing PA-CTR 8, V(1)=5592401, V(2)=0, repcount=5592402, factor=2/1
111861514 333599778527901 2715 13 01 54 132 401353 43 10 40 31 <A 4211184805
== Executing PPA-CTR 11 (once), V(1)=1351, V(2)=11184804
111861536 333599890376003 22372327 13 01 54 132 401352 41 34 0411184808 01 <B 42 10
== Executing PA-CTR 9, V(1)=11184806, V(2)=0, repcount=11184807, factor=2/1
246079220 1334399307981293 2713 13 01 54 132 401352 41 34 04 01 <B 4222369615 10
== Executing PPA-CTR 10 (once), V(1)=22369614
246079256 1334399800112911 44741949 13 01 54 132 401352 43 10 4022369619 31 <A 42
== Executing PA-CTR 8, V(1)=22369617, V(2)=0, repcount=22369618, factor=2/1
447405818 5337598767971899 2713 13 01 54 132 401352 43 10 40 31 <A 4244739237
== Executing PPA-CTR 11 (once), V(1)=1350, V(2)=44739236
447405840 5337599215364321 89481189 13 01 54 132 401351 41 34 0444739240 01 <B 42 10
== Executing PA-CTR 9, V(1)=44739238, V(2)=0, repcount=44739239, factor=2/1
984276708 21350395892106635 2711 13 01 54 132 401351 41 34 04 01 <B 4289478479 10
== Executing PPA-CTR 10 (once), V(1)=89478478
984276744 21350397860633261 178959675 13 01 54 132 401351 43 10 4089478483 31 <A 42
== Executing PA-CTR 8, V(1)=89478481, V(2)=0, repcount=89478482, factor=2/1
1789583082 85401589757354457 2711 13 01 54 132 401351 43 10 40 31 <A 42178956965
== Executing PPA-CTR 11 (once), V(1)=1349, V(2)=178956964
1789583104 85401591546924159 357916643 13 01 54 132 401350 41 34 04178956968 01 <B 42 10
== Executing PA-CTR 9, V(1)=178956966, V(2)=0, repcount=178956967, factor=2/1
3937066708 3416063[4]5034409 2709 13 01 54 132 401350 41 34 04 01 <B 42357913935 10
== Executing PPA-CTR 10 (once), V(1)=357913934
3937066744 3416063[4]9141067 715830585 13 01 54 132 401350 43 10 40357913939 31 <A 42
== Executing PA-CTR 8, V(1)=357913937, V(2)=0, repcount=357913938, factor=2/1
7158292186 1366425[5]0590455 2709 13 01 54 132 401350 43 10 40 31 <A 42715827877
== Executing PPA-CTR 11 (once), V(1)=1348, V(2)=715827876
7158292208 1366425[5]8869277 1431658465 13 01 54 132 401349 41 34 04715827880 01 <B 42 10
== Executing PA-CTR 9, V(1)=715827878, V(2)=0, repcount=715827879, factor=2/1
15748226756 5465701[5]9568711 2707 13 01 54 132 401349 41 34 04 01 <B 421431655759 10
Lines: 500
Top steps: 499
Macro steps: 15748226756
Basic steps: 5465701910229568711
Tape index: 2707
nonzeros: 2863312883
log10(nonzeros): 9.457
log10(steps ): 18.738
Some long numbers above are shortened: #(omitted digits) shown in "[]".
Input to awk program:
gohalt 1
nbs 6
T 2-state 6-symbol #e (T.J. & S. Ligocki)
: >8.6x10^821 >4.9x10^1643
5T 1RB 2LB 4RB 1LA 1RB 1RH 1LA 3RA 5RA 4LB 0RA 4LA
L 6
M 500
pref sim
machv Lig26_e just simple
machv Lig26_e-r with repetitions reduced
machv Lig26_e-1 with tape symbol exponents
machv Lig26_e-m as 2-macro machine
machv Lig26_e-a as 2-macro machine with pure additive config-TRs
iam Lig26_e-a
mtype 2
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:13:19 CEST 2010
edate Tue Jul 6 22:13: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:13:19 CEST 2010