Comment: This TM produces >1.6x10^809 nonzeros in >7.7x10^1618 steps.
| State | on 0 |
on 1 |
on 2 |
on 0 | on 1 | on 2 | ||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Move | Goto | Move | Goto | Move | Goto | |||||||
| A | 1RB | 2RC | 1RA | 1 | right | B | 2 | right | C | 1 | right | A |
| B | 2LC | 1LA | 1LB | 2 | left | C | 1 | left | A | 1 | left | B |
| C | 2LD | 0LB | 0RC | 2 | left | D | 0 | left | B | 0 | right | C |
| D | 0RD | 1RH | 0RA | 0 | right | D | 1 | right | H | 0 | right | A |
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 5 -3 <D(22) 02
2 8 0 (01)A> 02
3 15 -3 <C(21) 01
4 20 0 (12)C> 01
5 24 2 10 (12)C>
6 28 4 102 (11)B>
7 31 1 102 <A(10) 20
8 37 -1 10 <A(11) 00 20
9 43 -3 <A(11) 01 00 20
10 49 -5 <C(21) 012 00 20
11 54 -2 (12)C> 012 00 20
12 62 2 102 (12)C> 00 20
13 66 4 103 (11)B> 20
14 71 1 103 <B(10) 10
15 73 -1 102 <B(02) 102
16 77 -5 <B(02) 022 102
17 79 -7 <D(22) 023 102
18 82 -4 (01)A> 023 102
19 89 -7 <C(21) 01 022 102
20 94 -4 (12)C> 01 022 102
21 98 -2 10 (12)C> 022 102
22 102 0 102 (11)A> 02 102
23 109 -3 102 <A(11) 01 102
24 121 -7 <A(11) 013 102
25 127 -9 <C(21) 014 102
26 132 -6 (12)C> 014 102
27 148 2 104 (12)C> 102
28 151 -1 104 <A(11) 00 10
29 175 -9 <A(11) 014 00 10
30 181 -11 <C(21) 015 00 10
31 186 -8 (12)C> 015 00 10
32 206 2 105 (12)C> 00 10
33 210 4 106 (11)B> 10
34 215 1 106 <A(11)
35 251 -11 <A(11) 016
36 257 -13 <C(21) 017
37 262 -10 (12)C> 017
38 290 4 107 (12)C>
39 294 6 108 (11)B>
40 297 3 108 <A(10) 20
41 303 1 107 <A(11) 00 20
42 345 -13 <A(11) 017 00 20
43 351 -15 <C(21) 018 00 20
44 356 -12 (12)C> 018 00 20
45 388 4 108 (12)C> 00 20
46 392 6 109 (11)B> 20
47 397 3 109 <B(10) 10
48 399 1 108 <B(02) 102
49 415 -15 <B(02) 028 102
50 417 -17 <D(22) 029 102
51 420 -14 (01)A> 029 102
52 427 -17 <C(21) 01 028 102
53 432 -14 (12)C> 01 028 102
54 436 -12 10 (12)C> 028 102
55 440 -10 102 (11)A> 027 102
56 447 -13 102 <A(11) 01 026 102
57 459 -17 <A(11) 013 026 102
58 465 -19 <C(21) 014 026 102
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <C(21) 011+V(2) 023+V(1) [*]*
1 5 3 (12)C> 011+V(2) 023+V(1) [*]*
2 9+4*V(2) 5+2*V(2) 101+V(2) (12)C> 023+V(1) [*]*
3 13+4*V(2) 7+2*V(2) 102+V(2) (11)A> 022+V(1) [*]*
4 20+4*V(2) 4+2*V(2) 102+V(2) <A(11) 01 021+V(1) [*]*
5 32+10*V(2) 0 <A(11) 013+V(2) 021+V(1) [*]*
6 38+10*V(2) -2 <C(21) 014+V(2) 021+V(1) [*]*
<< Success! ==> defined new CTR 1 (PA)
58 465 -19 <C(21) 014 026 102
== Executing PA-CTR 1, V(1)=3, V(2)=3, repcount=2, factor=3/2
70 631 -23 <C(21) 0110 022 102
71 636 -20 (12)C> 0110 022 102
72 676 0 1010 (12)C> 022 102
73 680 2 1011 (11)A> 02 102
74 687 -1 1011 <A(11) 01 102
75 753 -23 <A(11) 0112 102
76 759 -25 <C(21) 0113 102
77 764 -22 (12)C> 0113 102
78 816 4 1013 (12)C> 102
79 819 1 1013 <A(11) 00 10
80 897 -25 <A(11) 0113 00 10
81 903 -27 <C(21) 0114 00 10
82 908 -24 (12)C> 0114 00 10
83 964 4 1014 (12)C> 00 10
84 968 6 1015 (11)B> 10
85 973 3 1015 <A(11)
86 1063 -27 <A(11) 0115
87 1069 -29 <C(21) 0116
88 1074 -26 (12)C> 0116
89 1138 6 1016 (12)C>
90 1142 8 1017 (11)B>
91 1145 5 1017 <A(10) 20
92 1151 3 1016 <A(11) 00 20
93 1247 -29 <A(11) 0116 00 20
94 1253 -31 <C(21) 0117 00 20
95 1258 -28 (12)C> 0117 00 20
96 1326 6 1017 (12)C> 00 20
97 1330 8 1018 (11)B> 20
98 1335 5 1018 <B(10) 10
99 1337 3 1017 <B(02) 102
100 1371 -31 <B(02) 0217 102
101 1373 -33 <D(22) 0218 102
102 1376 -30 (01)A> 0218 102
103 1383 -33 <C(21) 01 0217 102
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <C(21) 011+V(1) 022 102
1 5 3 (12)C> 011+V(1) 022 102
2 9+4*V(1) 5+2*V(1) 101+V(1) (12)C> 022 102
3 13+4*V(1) 7+2*V(1) 102+V(1) (11)A> 02 102
4 20+4*V(1) 4+2*V(1) 102+V(1) <A(11) 01 102
5 32+10*V(1) 0 <A(11) 013+V(1) 102
6 38+10*V(1) -2 <C(21) 014+V(1) 102
7 43+10*V(1) 1 (12)C> 014+V(1) 102
8 59+14*V(1) 9+2*V(1) 104+V(1) (12)C> 102
9 62+14*V(1) 6+2*V(1) 104+V(1) <A(11) 00 10
10 86+20*V(1) -2 <A(11) 014+V(1) 00 10
11 92+20*V(1) -4 <C(21) 015+V(1) 00 10
12 97+20*V(1) -1 (12)C> 015+V(1) 00 10
13 117+24*V(1) 9+2*V(1) 105+V(1) (12)C> 00 10
14 121+24*V(1) 11+2*V(1) 106+V(1) (11)B> 10
15 126+24*V(1) 8+2*V(1) 106+V(1) <A(11)
16 162+30*V(1) -4 <A(11) 016+V(1)
17 168+30*V(1) -6 <C(21) 017+V(1)
18 173+30*V(1) -3 (12)C> 017+V(1)
19 201+34*V(1) 11+2*V(1) 107+V(1) (12)C>
20 205+34*V(1) 13+2*V(1) 108+V(1) (11)B>
21 208+34*V(1) 10+2*V(1) 108+V(1) <A(10) 20
22 214+34*V(1) 8+2*V(1) 107+V(1) <A(11) 00 20
23 256+40*V(1) -6 <A(11) 017+V(1) 00 20
24 262+40*V(1) -8 <C(21) 018+V(1) 00 20
25 267+40*V(1) -5 (12)C> 018+V(1) 00 20
26 299+44*V(1) 11+2*V(1) 108+V(1) (12)C> 00 20
27 303+44*V(1) 13+2*V(1) 109+V(1) (11)B> 20
28 308+44*V(1) 10+2*V(1) 109+V(1) <B(10) 10
29 310+44*V(1) 8+2*V(1) 108+V(1) <B(02) 102
30 326+46*V(1) -8 <B(02) 028+V(1) 102
31 328+46*V(1) -10 <D(22) 029+V(1) 102
32 331+46*V(1) -7 (01)A> 029+V(1) 102
33 338+46*V(1) -10 <C(21) 01 028+V(1) 102
<< Success! ==> defined new CTR 2 (PPA)
103 1383 -33 <C(21) 01 0217 102
== Executing PA-CTR 1, V(1)=14, V(2)=0, repcount=8, factor=3/2
151 2527 -49 <C(21) 0125 02 102
152 2532 -46 (12)C> 0125 02 102
153 2632 4 1025 (12)C> 02 102
154 2636 6 1026 (11)A> 102
155 2640 8 1026 11 (01)A> 10
156 2644 10 1026 11 01 (01)A>
157 2653 7 1026 11 01 <B(10) 02
158 2659 5 1026 11 <B(10) 10 02
159 2663 3 1026 <B(10) 102 02
160 2665 1 1025 <B(02) 103 02
161 2715 -49 <B(02) 0225 103 02
162 2717 -51 <D(22) 0226 103 02
163 2720 -48 (01)A> 0226 103 02
164 2727 -51 <C(21) 01 0225 103 02
165 2732 -48 (12)C> 01 0225 103 02
166 2736 -46 10 (12)C> 0225 103 02
167 2740 -44 102 (11)A> 0224 103 02
168 2747 -47 102 <A(11) 01 0223 103 02
169 2759 -51 <A(11) 013 0223 103 02
170 2765 -53 <C(21) 014 0223 103 02
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <C(21) 011+V(2) 023+V(1) [*]* [*]*
1 5 3 (12)C> 011+V(2) 023+V(1) [*]* [*]*
2 9+4*V(2) 5+2*V(2) 101+V(2) (12)C> 023+V(1) [*]* [*]*
3 13+4*V(2) 7+2*V(2) 102+V(2) (11)A> 022+V(1) [*]* [*]*
4 20+4*V(2) 4+2*V(2) 102+V(2) <A(11) 01 021+V(1) [*]* [*]*
5 32+10*V(2) 0 <A(11) 013+V(2) 021+V(1) [*]* [*]*
6 38+10*V(2) -2 <C(21) 014+V(2) 021+V(1) [*]* [*]*
<< Success! ==> defined new CTR 3 (PA)
170 2765 -53 <C(21) 014 0223 103 02
== Executing PA-CTR 3, V(1)=20, V(2)=3, repcount=11, factor=3/2
236 5163 -75 <C(21) 0137 02 103 02
237 5168 -72 (12)C> 0137 02 103 02
238 5316 2 1037 (12)C> 02 103 02
239 5320 4 1038 (11)A> 103 02
240 5324 6 1038 11 (01)A> 102 02
241 5332 10 1038 11 012 (01)A> 02
242 5339 7 1038 11 012 <C(21) 01
243 5341 5 1038 11 01 <C(20) 21 01
244 5343 3 1038 11 <C(20) 20 21 01
245 5345 1 1038 <A(10) 202 21 01
246 5351 -1 1037 <A(11) 00 202 21 01
247 5573 -75 <A(11) 0137 00 202 21 01
248 5579 -77 <C(21) 0138 00 202 21 01
249 5584 -74 (12)C> 0138 00 202 21 01
250 5736 2 1038 (12)C> 00 202 21 01
251 5740 4 1039 (11)B> 202 21 01
252 5745 1 1039 <B(10) 10 20 21 01
253 5747 -1 1038 <B(02) 102 20 21 01
254 5823 -77 <B(02) 0238 102 20 21 01
255 5825 -79 <D(22) 0239 102 20 21 01
256 5828 -76 (01)A> 0239 102 20 21 01
257 5835 -79 <C(21) 01 0238 102 20 21 01
258 5840 -76 (12)C> 01 0238 102 20 21 01
259 5844 -74 10 (12)C> 0238 102 20 21 01
260 5848 -72 102 (11)A> 0237 102 20 21 01
261 5855 -75 102 <A(11) 01 0236 102 20 21 01
262 5867 -79 <A(11) 013 0236 102 20 21 01
263 5873 -81 <C(21) 014 0236 102 20 21 01
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <C(21) 011+V(2) 023+V(1) [*]* [*]* [*]* [*]*
1 5 3 (12)C> 011+V(2) 023+V(1) [*]* [*]* [*]* [*]*
2 9+4*V(2) 5+2*V(2) 101+V(2) (12)C> 023+V(1) [*]* [*]* [*]* [*]*
3 13+4*V(2) 7+2*V(2) 102+V(2) (11)A> 022+V(1) [*]* [*]* [*]* [*]*
4 20+4*V(2) 4+2*V(2) 102+V(2) <A(11) 01 021+V(1) [*]* [*]* [*]* [*]*
5 32+10*V(2) 0 <A(11) 013+V(2) 021+V(1) [*]* [*]* [*]* [*]*
6 38+10*V(2) -2 <C(21) 014+V(2) 021+V(1) [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 4 (PA)
263 5873 -81 <C(21) 014 0236 102 20 21 01
== Executing PA-CTR 4, V(1)=33, V(2)=3, repcount=17, factor=3/2
365 11109 -115 <C(21) 0155 022 102 20 21 01
366 11114 -112 (12)C> 0155 022 102 20 21 01
367 11334 -2 1055 (12)C> 022 102 20 21 01
368 11338 0 1056 (11)A> 02 102 20 21 01
369 11345 -3 1056 <A(11) 01 102 20 21 01
370 11681 -115 <A(11) 0157 102 20 21 01
371 11687 -117 <C(21) 0158 102 20 21 01
372 11692 -114 (12)C> 0158 102 20 21 01
373 11924 2 1058 (12)C> 102 20 21 01
374 11927 -1 1058 <A(11) 00 10 20 21 01
375 12275 -117 <A(11) 0158 00 10 20 21 01
376 12281 -119 <C(21) 0159 00 10 20 21 01
377 12286 -116 (12)C> 0159 00 10 20 21 01
378 12522 2 1059 (12)C> 00 10 20 21 01
379 12526 4 1060 (11)B> 10 20 21 01
380 12531 1 1060 <A(11) 00 20 21 01
381 12891 -119 <A(11) 0160 00 20 21 01
382 12897 -121 <C(21) 0161 00 20 21 01
383 12902 -118 (12)C> 0161 00 20 21 01
384 13146 4 1061 (12)C> 00 20 21 01
385 13150 6 1062 (11)B> 20 21 01
386 13155 3 1062 <B(10) 10 21 01
387 13157 1 1061 <B(02) 102 21 01
388 13279 -121 <B(02) 0261 102 21 01
389 13281 -123 <D(22) 0262 102 21 01
390 13284 -120 (01)A> 0262 102 21 01
391 13291 -123 <C(21) 01 0261 102 21 01
392 13296 -120 (12)C> 01 0261 102 21 01
393 13300 -118 10 (12)C> 0261 102 21 01
394 13304 -116 102 (11)A> 0260 102 21 01
395 13311 -119 102 <A(11) 01 0259 102 21 01
396 13323 -123 <A(11) 013 0259 102 21 01
397 13329 -125 <C(21) 014 0259 102 21 01
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <C(21) 011+V(2) 023+V(1) [*]* [*]* [*]*
1 5 3 (12)C> 011+V(2) 023+V(1) [*]* [*]* [*]*
2 9+4*V(2) 5+2*V(2) 101+V(2) (12)C> 023+V(1) [*]* [*]* [*]*
3 13+4*V(2) 7+2*V(2) 102+V(2) (11)A> 022+V(1) [*]* [*]* [*]*
4 20+4*V(2) 4+2*V(2) 102+V(2) <A(11) 01 021+V(1) [*]* [*]* [*]*
5 32+10*V(2) 0 <A(11) 013+V(2) 021+V(1) [*]* [*]* [*]*
6 38+10*V(2) -2 <C(21) 014+V(2) 021+V(1) [*]* [*]* [*]*
<< Success! ==> defined new CTR 5 (PA)
397 13329 -125 <C(21) 014 0259 102 21 01
== Executing PA-CTR 5, V(1)=56, V(2)=3, repcount=29, factor=3/2
571 27481 -183 <C(21) 0191 02 102 21 01
572 27486 -180 (12)C> 0191 02 102 21 01
573 27850 2 1091 (12)C> 02 102 21 01
574 27854 4 1092 (11)A> 102 21 01
575 27858 6 1092 11 (01)A> 10 21 01
576 27862 8 1092 11 01 (01)A> 21 01
577 27864 10 1092 11 012 (12)C> 01
578 27868 12 1092 11 012 10 (12)C>
579 27872 14 1092 11 012 102 (11)B>
580 27875 11 1092 11 012 102 <A(10) 20
581 27881 9 1092 11 012 10 <A(11) 00 20
582 27887 7 1092 11 012 <A(11) 01 00 20
583 27891 5 1092 11 01 <C(21) 012 00 20
584 27893 3 1092 11 <C(20) 21 012 00 20
585 27895 1 1092 <A(10) 20 21 012 00 20
586 27901 -1 1091 <A(11) 00 20 21 012 00 20
587 28447 -183 <A(11) 0191 00 20 21 012 00 20
588 28453 -185 <C(21) 0192 00 20 21 012 00 20
589 28458 -182 (12)C> 0192 00 20 21 012 00 20
590 28826 2 1092 (12)C> 00 20 21 012 00 20
591 28830 4 1093 (11)B> 20 21 012 00 20
592 28835 1 1093 <B(10) 10 21 012 00 20
593 28837 -1 1092 <B(02) 102 21 012 00 20
594 29021 -185 <B(02) 0292 102 21 012 00 20
595 29023 -187 <D(22) 0293 102 21 012 00 20
596 29026 -184 (01)A> 0293 102 21 012 00 20
597 29033 -187 <C(21) 01 0292 102 21 012 00 20
598 29038 -184 (12)C> 01 0292 102 21 012 00 20
599 29042 -182 10 (12)C> 0292 102 21 012 00 20
600 29046 -180 102 (11)A> 0291 102 21 012 00 20
601 29053 -183 102 <A(11) 01 0290 102 21 012 00 20
602 29065 -187 <A(11) 013 0290 102 21 012 00 20
603 29071 -189 <C(21) 014 0290 102 21 012 00 20
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <C(21) 011+V(2) 023+V(1) [*]* [*]* [*]* [*]* [*]*
1 5 3 (12)C> 011+V(2) 023+V(1) [*]* [*]* [*]* [*]* [*]*
2 9+4*V(2) 5+2*V(2) 101+V(2) (12)C> 023+V(1) [*]* [*]* [*]* [*]* [*]*
3 13+4*V(2) 7+2*V(2) 102+V(2) (11)A> 022+V(1) [*]* [*]* [*]* [*]* [*]*
4 20+4*V(2) 4+2*V(2) 102+V(2) <A(11) 01 021+V(1) [*]* [*]* [*]* [*]* [*]*
5 32+10*V(2) 0 <A(11) 013+V(2) 021+V(1) [*]* [*]* [*]* [*]* [*]*
6 38+10*V(2) -2 <C(21) 014+V(2) 021+V(1) [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 6 (PA)
603 29071 -189 <C(21) 014 0290 102 21 012 00 20
== Executing PA-CTR 6, V(1)=87, V(2)=3, repcount=44, factor=3/2
867 60443 -277 <C(21) 01136 022 102 21 012 00 20
868 60448 -274 (12)C> 01136 022 102 21 012 00 20
869 60992 -2 10136 (12)C> 022 102 21 012 00 20
870 60996 0 10137 (11)A> 02 102 21 012 00 20
871 61003 -3 10137 <A(11) 01 102 21 012 00 20
872 61825 -277 <A(11) 01138 102 21 012 00 20
873 61831 -279 <C(21) 01139 102 21 012 00 20
874 61836 -276 (12)C> 01139 102 21 012 00 20
875 62392 2 10139 (12)C> 102 21 012 00 20
876 62395 -1 10139 <A(11) 00 10 21 012 00 20
877 63229 -279 <A(11) 01139 00 10 21 012 00 20
878 63235 -281 <C(21) 01140 00 10 21 012 00 20
879 63240 -278 (12)C> 01140 00 10 21 012 00 20
880 63800 2 10140 (12)C> 00 10 21 012 00 20
881 63804 4 10141 (11)B> 10 21 012 00 20
882 63809 1 10141 <A(11) 00 21 012 00 20
883 64655 -281 <A(11) 01141 00 21 012 00 20
884 64661 -283 <C(21) 01142 00 21 012 00 20
885 64666 -280 (12)C> 01142 00 21 012 00 20
886 65234 4 10142 (12)C> 00 21 012 00 20
887 65238 6 10143 (11)B> 21 012 00 20
888 65243 3 10143 <B(10) 11 012 00 20
889 65245 1 10142 <B(02) 10 11 012 00 20
890 65529 -283 <B(02) 02142 10 11 012 00 20
891 65531 -285 <D(22) 02143 10 11 012 00 20
892 65534 -282 (01)A> 02143 10 11 012 00 20
893 65541 -285 <C(21) 01 02142 10 11 012 00 20
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <C(21) 011+V(1) 022 102 21 [*]* [*]* [*]*
1 5 3 (12)C> 011+V(1) 022 102 21 [*]* [*]* [*]*
2 9+4*V(1) 5+2*V(1) 101+V(1) (12)C> 022 102 21 [*]* [*]* [*]*
3 13+4*V(1) 7+2*V(1) 102+V(1) (11)A> 02 102 21 [*]* [*]* [*]*
4 20+4*V(1) 4+2*V(1) 102+V(1) <A(11) 01 102 21 [*]* [*]* [*]*
5 32+10*V(1) 0 <A(11) 013+V(1) 102 21 [*]* [*]* [*]*
6 38+10*V(1) -2 <C(21) 014+V(1) 102 21 [*]* [*]* [*]*
7 43+10*V(1) 1 (12)C> 014+V(1) 102 21 [*]* [*]* [*]*
8 59+14*V(1) 9+2*V(1) 104+V(1) (12)C> 102 21 [*]* [*]* [*]*
9 62+14*V(1) 6+2*V(1) 104+V(1) <A(11) 00 10 21 [*]* [*]* [*]*
10 86+20*V(1) -2 <A(11) 014+V(1) 00 10 21 [*]* [*]* [*]*
11 92+20*V(1) -4 <C(21) 015+V(1) 00 10 21 [*]* [*]* [*]*
12 97+20*V(1) -1 (12)C> 015+V(1) 00 10 21 [*]* [*]* [*]*
13 117+24*V(1) 9+2*V(1) 105+V(1) (12)C> 00 10 21 [*]* [*]* [*]*
14 121+24*V(1) 11+2*V(1) 106+V(1) (11)B> 10 21 [*]* [*]* [*]*
15 126+24*V(1) 8+2*V(1) 106+V(1) <A(11) 00 21 [*]* [*]* [*]*
16 162+30*V(1) -4 <A(11) 016+V(1) 00 21 [*]* [*]* [*]*
17 168+30*V(1) -6 <C(21) 017+V(1) 00 21 [*]* [*]* [*]*
18 173+30*V(1) -3 (12)C> 017+V(1) 00 21 [*]* [*]* [*]*
19 201+34*V(1) 11+2*V(1) 107+V(1) (12)C> 00 21 [*]* [*]* [*]*
20 205+34*V(1) 13+2*V(1) 108+V(1) (11)B> 21 [*]* [*]* [*]*
21 210+34*V(1) 10+2*V(1) 108+V(1) <B(10) 11 [*]* [*]* [*]*
22 212+34*V(1) 8+2*V(1) 107+V(1) <B(02) 10 11 [*]* [*]* [*]*
23 226+36*V(1) -6 <B(02) 027+V(1) 10 11 [*]* [*]* [*]*
24 228+36*V(1) -8 <D(22) 028+V(1) 10 11 [*]* [*]* [*]*
25 231+36*V(1) -5 (01)A> 028+V(1) 10 11 [*]* [*]* [*]*
26 238+36*V(1) -8 <C(21) 01 027+V(1) 10 11 [*]* [*]* [*]*
<< Success! ==> defined new CTR 7 (PPA)
893 65541 -285 <C(21) 01 02142 10 11 012 00 20
== Executing PA-CTR 6, V(1)=139, V(2)=0, repcount=70, factor=3/2
1313 140651 -425 <C(21) 01211 022 10 11 012 00 20
1314 140656 -422 (12)C> 01211 022 10 11 012 00 20
1315 141500 0 10211 (12)C> 022 10 11 012 00 20
1316 141504 2 10212 (11)A> 02 10 11 012 00 20
1317 141511 -1 10212 <A(11) 01 10 11 012 00 20
1318 142783 -425 <A(11) 01213 10 11 012 00 20
1319 142789 -427 <C(21) 01214 10 11 012 00 20
1320 142794 -424 (12)C> 01214 10 11 012 00 20
1321 143650 4 10214 (12)C> 10 11 012 00 20
1322 143653 1 10214 <A(11) 00 11 012 00 20
1323 144937 -427 <A(11) 01214 00 11 012 00 20
1324 144943 -429 <C(21) 01215 00 11 012 00 20
1325 144948 -426 (12)C> 01215 00 11 012 00 20
1326 145808 4 10215 (12)C> 00 11 012 00 20
1327 145812 6 10216 (11)B> 11 012 00 20
1328 145817 3 10216 <A(11) 013 00 20
1329 147113 -429 <A(11) 01219 00 20
1330 147119 -431 <C(21) 01220 00 20
1331 147124 -428 (12)C> 01220 00 20
1332 148004 12 10220 (12)C> 00 20
1333 148008 14 10221 (11)B> 20
1334 148013 11 10221 <B(10) 10
1335 148015 9 10220 <B(02) 102
1336 148455 -431 <B(02) 02220 102
1337 148457 -433 <D(22) 02221 102
1338 148460 -430 (01)A> 02221 102
1339 148467 -433 <C(21) 01 02220 102
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <C(21) 011+V(2) 022 10 11 011+V(1) 00 20
1 5 3 (12)C> 011+V(2) 022 10 11 011+V(1) 00 20
2 9+4*V(2) 5+2*V(2) 101+V(2) (12)C> 022 10 11 011+V(1) 00 20
3 13+4*V(2) 7+2*V(2) 102+V(2) (11)A> 02 10 11 011+V(1) 00 20
4 20+4*V(2) 4+2*V(2) 102+V(2) <A(11) 01 10 11 011+V(1) 00 20
5 32+10*V(2) 0 <A(11) 013+V(2) 10 11 011+V(1) 00 20
6 38+10*V(2) -2 <C(21) 014+V(2) 10 11 011+V(1) 00 20
7 43+10*V(2) 1 (12)C> 014+V(2) 10 11 011+V(1) 00 20
8 59+14*V(2) 9+2*V(2) 104+V(2) (12)C> 10 11 011+V(1) 00 20
9 62+14*V(2) 6+2*V(2) 104+V(2) <A(11) 00 11 011+V(1) 00 20
10 86+20*V(2) -2 <A(11) 014+V(2) 00 11 011+V(1) 00 20
11 92+20*V(2) -4 <C(21) 015+V(2) 00 11 011+V(1) 00 20
12 97+20*V(2) -1 (12)C> 015+V(2) 00 11 011+V(1) 00 20
13 117+24*V(2) 9+2*V(2) 105+V(2) (12)C> 00 11 011+V(1) 00 20
14 121+24*V(2) 11+2*V(2) 106+V(2) (11)B> 11 011+V(1) 00 20
15 126+24*V(2) 8+2*V(2) 106+V(2) <A(11) 012+V(1) 00 20
16 162+30*V(2) -4 <A(11) 018+V(1)+V(2) 00 20
17 168+30*V(2) -6 <C(21) 019+V(1)+V(2) 00 20
18 173+30*V(2) -3 (12)C> 019+V(1)+V(2) 00 20
19 209+4*V(1)+34*V(2) 15+2*V(1)+2*V(2) 109+V(1)+V(2) (12)C> 00 20
20 213+4*V(1)+34*V(2) 17+2*V(1)+2*V(2) 1010+V(1)+V(2) (11)B> 20
21 218+4*V(1)+34*V(2) 14+2*V(1)+2*V(2) 1010+V(1)+V(2) <B(10) 10
22 220+4*V(1)+34*V(2) 12+2*V(1)+2*V(2) 109+V(1)+V(2) <B(02) 102
23 238+6*V(1)+36*V(2) -6 <B(02) 029+V(1)+V(2) 102
24 240+6*V(1)+36*V(2) -8 <D(22) 0210+V(1)+V(2) 102
25 243+6*V(1)+36*V(2) -5 (01)A> 0210+V(1)+V(2) 102
26 250+6*V(1)+36*V(2) -8 <C(21) 01 029+V(1)+V(2) 102
<< Success! ==> defined new CTR 8 (PPA)
1339 148467 -433 <C(21) 01 02220 102
== Executing PA-CTR 1, V(1)=217, V(2)=0, repcount=109, factor=3/2
1993 329189 -651 <C(21) 01328 022 102
== Executing PPA-CTR 2 (once), V(1)=327
2026 344569 -661 <C(21) 01 02335 102
== Executing PA-CTR 1, V(1)=332, V(2)=0, repcount=167, factor=3/2
3028 766745 -995 <C(21) 01502 02 102
3029 766750 -992 (12)C> 01502 02 102
3030 768758 12 10502 (12)C> 02 102
3031 768762 14 10503 (11)A> 102
3032 768766 16 10503 11 (01)A> 10
3033 768770 18 10503 11 01 (01)A>
3034 768779 15 10503 11 01 <B(10) 02
3035 768785 13 10503 11 <B(10) 10 02
3036 768789 11 10503 <B(10) 102 02
3037 768791 9 10502 <B(02) 103 02
3038 769795 -995 <B(02) 02502 103 02
3039 769797 -997 <D(22) 02503 103 02
3040 769800 -994 (01)A> 02503 103 02
3041 769807 -997 <C(21) 01 02502 103 02
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <C(21) 013+V(2) 02 102+V(1)
1 5 3 (12)C> 013+V(2) 02 102+V(1)
2 17+4*V(2) 9+2*V(2) 103+V(2) (12)C> 02 102+V(1)
3 21+4*V(2) 11+2*V(2) 104+V(2) (11)A> 102+V(1)
4 25+4*V(2) 13+2*V(2) 104+V(2) 11 (01)A> 101+V(1)
5 29+4*V(1)+4*V(2) 15+2*V(1)+2*V(2) 104+V(2) 11 011+V(1) (01)A>
6 38+4*V(1)+4*V(2) 12+2*V(1)+2*V(2) 104+V(2) 11 011+V(1) <B(10) 02
7 44+10*V(1)+4*V(2) 10+2*V(2) 104+V(2) 11 <B(10) 101+V(1) 02
8 48+10*V(1)+4*V(2) 8+2*V(2) 104+V(2) <B(10) 102+V(1) 02
9 50+10*V(1)+4*V(2) 6+2*V(2) 103+V(2) <B(02) 103+V(1) 02
10 56+10*V(1)+6*V(2) 0 <B(02) 023+V(2) 103+V(1) 02
11 58+10*V(1)+6*V(2) -2 <D(22) 024+V(2) 103+V(1) 02
12 61+10*V(1)+6*V(2) 1 (01)A> 024+V(2) 103+V(1) 02
13 68+10*V(1)+6*V(2) -2 <C(21) 01 023+V(2) 103+V(1) 02
<< Success! ==> defined new CTR 9 (PPA)
3041 769807 -997 <C(21) 01 02502 103 02
== Executing PA-CTR 3, V(1)=499, V(2)=0, repcount=250, factor=3/2
4541 1713057 -1497 <C(21) 01751 022 103 02
4542 1713062 -1494 (12)C> 01751 022 103 02
4543 1716066 8 10751 (12)C> 022 103 02
4544 1716070 10 10752 (11)A> 02 103 02
4545 1716077 7 10752 <A(11) 01 103 02
4546 1720589 -1497 <A(11) 01753 103 02
4547 1720595 -1499 <C(21) 01754 103 02
4548 1720600 -1496 (12)C> 01754 103 02
4549 1723616 12 10754 (12)C> 103 02
4550 1723619 9 10754 <A(11) 00 102 02
4551 1728143 -1499 <A(11) 01754 00 102 02
4552 1728149 -1501 <C(21) 01755 00 102 02
4553 1728154 -1498 (12)C> 01755 00 102 02
4554 1731174 12 10755 (12)C> 00 102 02
4555 1731178 14 10756 (11)B> 102 02
4556 1731183 11 10756 <A(11) 00 10 02
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 101+V(1) <A(11) 00 102+V(2) [*]*
1 6+6*V(1) -2+-2*V(1) <A(11) 011+V(1) 00 102+V(2) [*]*
2 12+6*V(1) -4+-2*V(1) <C(21) 012+V(1) 00 102+V(2) [*]*
3 17+6*V(1) -1+-2*V(1) (12)C> 012+V(1) 00 102+V(2) [*]*
4 25+10*V(1) 3 102+V(1) (12)C> 00 102+V(2) [*]*
5 29+10*V(1) 5 103+V(1) (11)B> 102+V(2) [*]*
6 34+10*V(1) 2 103+V(1) <A(11) 00 101+V(2) [*]*
<< Success! ==> defined new CTR 10 (PA)
4557 1735719 -1501 <A(11) 01756 00 10 02
4558 1735725 -1503 <C(21) 01757 00 10 02
4559 1735730 -1500 (12)C> 01757 00 10 02
4560 1738758 14 10757 (12)C> 00 10 02
4561 1738762 16 10758 (11)B> 10 02
4562 1738767 13 10758 <A(11) 00 02
4563 1743315 -1503 <A(11) 01758 00 02
4564 1743321 -1505 <C(21) 01759 00 02
4565 1743326 -1502 (12)C> 01759 00 02
4566 1746362 16 10759 (12)C> 00 02
4567 1746366 18 10760 (11)B> 02
4568 1746369 15 10760 <A(10) 22
4569 1746375 13 10759 <A(11) 00 22
4570 1750929 -1505 <A(11) 01759 00 22
4571 1750935 -1507 <C(21) 01760 00 22
4572 1750940 -1504 (12)C> 01760 00 22
4573 1753980 16 10760 (12)C> 00 22
4574 1753984 18 10761 (11)B> 22
4575 1753989 15 10761 <B(10) 12
4576 1753991 13 10760 <B(02) 10 12
4577 1755511 -1507 <B(02) 02760 10 12
4578 1755513 -1509 <D(22) 02761 10 12
4579 1755516 -1506 (01)A> 02761 10 12
4580 1755523 -1509 <C(21) 01 02760 10 12
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 101+V(1) <A(11) 00 10 02
1 6+6*V(1) -2+-2*V(1) <A(11) 011+V(1) 00 10 02
2 12+6*V(1) -4+-2*V(1) <C(21) 012+V(1) 00 10 02
3 17+6*V(1) -1+-2*V(1) (12)C> 012+V(1) 00 10 02
4 25+10*V(1) 3 102+V(1) (12)C> 00 10 02
5 29+10*V(1) 5 103+V(1) (11)B> 10 02
6 34+10*V(1) 2 103+V(1) <A(11) 00 02
7 52+16*V(1) -4+-2*V(1) <A(11) 013+V(1) 00 02
8 58+16*V(1) -6+-2*V(1) <C(21) 014+V(1) 00 02
9 63+16*V(1) -3+-2*V(1) (12)C> 014+V(1) 00 02
10 79+20*V(1) 5 104+V(1) (12)C> 00 02
11 83+20*V(1) 7 105+V(1) (11)B> 02
12 86+20*V(1) 4 105+V(1) <A(10) 22
13 92+20*V(1) 2 104+V(1) <A(11) 00 22
14 116+26*V(1) -6+-2*V(1) <A(11) 014+V(1) 00 22
15 122+26*V(1) -8+-2*V(1) <C(21) 015+V(1) 00 22
16 127+26*V(1) -5+-2*V(1) (12)C> 015+V(1) 00 22
17 147+30*V(1) 5 105+V(1) (12)C> 00 22
18 151+30*V(1) 7 106+V(1) (11)B> 22
19 156+30*V(1) 4 106+V(1) <B(10) 12
20 158+30*V(1) 2 105+V(1) <B(02) 10 12
21 168+32*V(1) -8+-2*V(1) <B(02) 025+V(1) 10 12
22 170+32*V(1) -10+-2*V(1) <D(22) 026+V(1) 10 12
23 173+32*V(1) -7+-2*V(1) (01)A> 026+V(1) 10 12
24 180+32*V(1) -10+-2*V(1) <C(21) 01 025+V(1) 10 12
<< Success! ==> defined new CTR 11 (PPA)
4580 1755523 -1509 <C(21) 01 02760 10 12
== Executing PA-CTR 3, V(1)=757, V(2)=0, repcount=379, factor=3/2
6854 3918855 -2267 <C(21) 011138 022 10 12
6855 3918860 -2264 (12)C> 011138 022 10 12
6856 3923412 12 101138 (12)C> 022 10 12
6857 3923416 14 101139 (11)A> 02 10 12
6858 3923423 11 101139 <A(11) 01 10 12
6859 3930257 -2267 <A(11) 011140 10 12
6860 3930263 -2269 <C(21) 011141 10 12
6861 3930268 -2266 (12)C> 011141 10 12
6862 3934832 16 101141 (12)C> 10 12
6863 3934835 13 101141 <A(11) 00 12
6864 3941681 -2269 <A(11) 011141 00 12
6865 3941687 -2271 <C(21) 011142 00 12
6866 3941692 -2268 (12)C> 011142 00 12
6867 3946260 16 101142 (12)C> 00 12
6868 3946264 18 101143 (11)B> 12
6869 3946269 15 101143 <A(11) 02
6870 3953127 -2271 <A(11) 011143 02
6871 3953133 -2273 <C(21) 011144 02
6872 3953138 -2270 (12)C> 011144 02
6873 3957714 18 101144 (12)C> 02
6874 3957718 20 101145 (11)A>
6875 3957725 17 101145 <B(10) 02
6876 3957727 15 101144 <B(02) 10 02
6877 3960015 -2273 <B(02) 021144 10 02
6878 3960017 -2275 <D(22) 021145 10 02
6879 3960020 -2272 (01)A> 021145 10 02
6880 3960027 -2275 <C(21) 01 021144 10 02
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <C(21) 011+V(1) 022 10 12
1 5 3 (12)C> 011+V(1) 022 10 12
2 9+4*V(1) 5+2*V(1) 101+V(1) (12)C> 022 10 12
3 13+4*V(1) 7+2*V(1) 102+V(1) (11)A> 02 10 12
4 20+4*V(1) 4+2*V(1) 102+V(1) <A(11) 01 10 12
5 32+10*V(1) 0 <A(11) 013+V(1) 10 12
6 38+10*V(1) -2 <C(21) 014+V(1) 10 12
7 43+10*V(1) 1 (12)C> 014+V(1) 10 12
8 59+14*V(1) 9+2*V(1) 104+V(1) (12)C> 10 12
9 62+14*V(1) 6+2*V(1) 104+V(1) <A(11) 00 12
10 86+20*V(1) -2 <A(11) 014+V(1) 00 12
11 92+20*V(1) -4 <C(21) 015+V(1) 00 12
12 97+20*V(1) -1 (12)C> 015+V(1) 00 12
13 117+24*V(1) 9+2*V(1) 105+V(1) (12)C> 00 12
14 121+24*V(1) 11+2*V(1) 106+V(1) (11)B> 12
15 126+24*V(1) 8+2*V(1) 106+V(1) <A(11) 02
16 162+30*V(1) -4 <A(11) 016+V(1) 02
17 168+30*V(1) -6 <C(21) 017+V(1) 02
18 173+30*V(1) -3 (12)C> 017+V(1) 02
19 201+34*V(1) 11+2*V(1) 107+V(1) (12)C> 02
20 205+34*V(1) 13+2*V(1) 108+V(1) (11)A>
21 212+34*V(1) 10+2*V(1) 108+V(1) <B(10) 02
22 214+34*V(1) 8+2*V(1) 107+V(1) <B(02) 10 02
23 228+36*V(1) -6 <B(02) 027+V(1) 10 02
24 230+36*V(1) -8 <D(22) 028+V(1) 10 02
25 233+36*V(1) -5 (01)A> 028+V(1) 10 02
26 240+36*V(1) -8 <C(21) 01 027+V(1) 10 02
<< Success! ==> defined new CTR 12 (PPA)
6880 3960027 -2275 <C(21) 01 021144 10 02
== Executing PA-CTR 3, V(1)=1141, V(2)=0, repcount=571, factor=3/2
10306 8863775 -3417 <C(21) 011714 022 10 02
10307 8863780 -3414 (12)C> 011714 022 10 02
10308 8870636 14 101714 (12)C> 022 10 02
10309 8870640 16 101715 (11)A> 02 10 02
10310 8870647 13 101715 <A(11) 01 10 02
10311 8880937 -3417 <A(11) 011716 10 02
10312 8880943 -3419 <C(21) 011717 10 02
10313 8880948 -3416 (12)C> 011717 10 02
10314 8887816 18 101717 (12)C> 10 02
10315 8887819 15 101717 <A(11) 00 02
10316 8898121 -3419 <A(11) 011717 00 02
10317 8898127 -3421 <C(21) 011718 00 02
10318 8898132 -3418 (12)C> 011718 00 02
10319 8905004 18 101718 (12)C> 00 02
10320 8905008 20 101719 (11)B> 02
10321 8905011 17 101719 <A(10) 22
10322 8905017 15 101718 <A(11) 00 22
10323 8915325 -3421 <A(11) 011718 00 22
10324 8915331 -3423 <C(21) 011719 00 22
10325 8915336 -3420 (12)C> 011719 00 22
10326 8922212 18 101719 (12)C> 00 22
10327 8922216 20 101720 (11)B> 22
10328 8922221 17 101720 <B(10) 12
10329 8922223 15 101719 <B(02) 10 12
10330 8925661 -3423 <B(02) 021719 10 12
10331 8925663 -3425 <D(22) 021720 10 12
10332 8925666 -3422 (01)A> 021720 10 12
10333 8925673 -3425 <C(21) 01 021719 10 12
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <C(21) 011+V(1) 022 10 02
1 5 3 (12)C> 011+V(1) 022 10 02
2 9+4*V(1) 5+2*V(1) 101+V(1) (12)C> 022 10 02
3 13+4*V(1) 7+2*V(1) 102+V(1) (11)A> 02 10 02
4 20+4*V(1) 4+2*V(1) 102+V(1) <A(11) 01 10 02
5 32+10*V(1) 0 <A(11) 013+V(1) 10 02
6 38+10*V(1) -2 <C(21) 014+V(1) 10 02
7 43+10*V(1) 1 (12)C> 014+V(1) 10 02
8 59+14*V(1) 9+2*V(1) 104+V(1) (12)C> 10 02
9 62+14*V(1) 6+2*V(1) 104+V(1) <A(11) 00 02
10 86+20*V(1) -2 <A(11) 014+V(1) 00 02
11 92+20*V(1) -4 <C(21) 015+V(1) 00 02
12 97+20*V(1) -1 (12)C> 015+V(1) 00 02
13 117+24*V(1) 9+2*V(1) 105+V(1) (12)C> 00 02
14 121+24*V(1) 11+2*V(1) 106+V(1) (11)B> 02
15 124+24*V(1) 8+2*V(1) 106+V(1) <A(10) 22
16 130+24*V(1) 6+2*V(1) 105+V(1) <A(11) 00 22
17 160+30*V(1) -4 <A(11) 015+V(1) 00 22
18 166+30*V(1) -6 <C(21) 016+V(1) 00 22
19 171+30*V(1) -3 (12)C> 016+V(1) 00 22
20 195+34*V(1) 9+2*V(1) 106+V(1) (12)C> 00 22
21 199+34*V(1) 11+2*V(1) 107+V(1) (11)B> 22
22 204+34*V(1) 8+2*V(1) 107+V(1) <B(10) 12
23 206+34*V(1) 6+2*V(1) 106+V(1) <B(02) 10 12
24 218+36*V(1) -6 <B(02) 026+V(1) 10 12
25 220+36*V(1) -8 <D(22) 027+V(1) 10 12
26 223+36*V(1) -5 (01)A> 027+V(1) 10 12
27 230+36*V(1) -8 <C(21) 01 026+V(1) 10 12
<< Success! ==> defined new CTR 13 (PPA)
10333 8925673 -3425 <C(21) 01 021719 10 12
== Executing PA-CTR 3, V(1)=1716, V(2)=0, repcount=859, factor=3/2
15487 20013645 -5143 <C(21) 012578 02 10 12
15488 20013650 -5140 (12)C> 012578 02 10 12
15489 20023962 16 102578 (12)C> 02 10 12
15490 20023966 18 102579 (11)A> 10 12
15491 20023970 20 102579 11 (01)A> 12
15492 20023972 22 102579 11 01 (20)C>
15493 20023976 24 102579 11 01 20 (01)B>
15494 20023979 21 102579 11 01 20 <C(20) 20
15495 20023984 24 102579 11 012 (11)B> 20
15496 20023989 21 102579 11 012 <B(10) 10
15497 20024001 17 102579 11 <B(10) 103
15498 20024005 15 102579 <B(10) 104
15499 20024007 13 102578 <B(02) 105
15500 20029163 -5143 <B(02) 022578 105
15501 20029165 -5145 <D(22) 022579 105
15502 20029168 -5142 (01)A> 022579 105
15503 20029175 -5145 <C(21) 01 022578 105
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <C(21) 013+V(1) 02 10 12
1 5 3 (12)C> 013+V(1) 02 10 12
2 17+4*V(1) 9+2*V(1) 103+V(1) (12)C> 02 10 12
3 21+4*V(1) 11+2*V(1) 104+V(1) (11)A> 10 12
4 25+4*V(1) 13+2*V(1) 104+V(1) 11 (01)A> 12
5 27+4*V(1) 15+2*V(1) 104+V(1) 11 01 (20)C>
6 31+4*V(1) 17+2*V(1) 104+V(1) 11 01 20 (01)B>
7 34+4*V(1) 14+2*V(1) 104+V(1) 11 01 20 <C(20) 20
8 39+4*V(1) 17+2*V(1) 104+V(1) 11 012 (11)B> 20
9 44+4*V(1) 14+2*V(1) 104+V(1) 11 012 <B(10) 10
10 56+4*V(1) 10+2*V(1) 104+V(1) 11 <B(10) 103
11 60+4*V(1) 8+2*V(1) 104+V(1) <B(10) 104
12 62+4*V(1) 6+2*V(1) 103+V(1) <B(02) 105
13 68+6*V(1) 0 <B(02) 023+V(1) 105
14 70+6*V(1) -2 <D(22) 024+V(1) 105
15 73+6*V(1) 1 (01)A> 024+V(1) 105
16 80+6*V(1) -2 <C(21) 01 023+V(1) 105
<< Success! ==> defined new CTR 14 (PPA)
15503 20029175 -5145 <C(21) 01 022578 105
== Executing PA-CTR 1, V(1)=2575, V(2)=0, repcount=1288, factor=3/2
23231 44942959 -7721 <C(21) 013865 022 105
23232 44942964 -7718 (12)C> 013865 022 105
23233 44958424 12 103865 (12)C> 022 105
23234 44958428 14 103866 (11)A> 02 105
23235 44958435 11 103866 <A(11) 01 105
23236 44981631 -7721 <A(11) 013867 105
23237 44981637 -7723 <C(21) 013868 105
23238 44981642 -7720 (12)C> 013868 105
23239 44997114 16 103868 (12)C> 105
23240 44997117 13 103868 <A(11) 00 104
23241 45020325 -7723 <A(11) 013868 00 104
23242 45020331 -7725 <C(21) 013869 00 104
23243 45020336 -7722 (12)C> 013869 00 104
23244 45035812 16 103869 (12)C> 00 104
23245 45035816 18 103870 (11)B> 104
23246 45035821 15 103870 <A(11) 00 103
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 101+V(1) <A(11) 00 102+V(2)
1 6+6*V(1) -2+-2*V(1) <A(11) 011+V(1) 00 102+V(2)
2 12+6*V(1) -4+-2*V(1) <C(21) 012+V(1) 00 102+V(2)
3 17+6*V(1) -1+-2*V(1) (12)C> 012+V(1) 00 102+V(2)
4 25+10*V(1) 3 102+V(1) (12)C> 00 102+V(2)
5 29+10*V(1) 5 103+V(1) (11)B> 102+V(2)
6 34+10*V(1) 2 103+V(1) <A(11) 00 101+V(2)
<< Success! ==> defined new CTR 15 (PA)
23246 45035821 15 103870 <A(11) 00 103
== Executing PA-CTR 15, V(1)=3869, V(2)=1, repcount=2, factor=2/1
23258 45113289 19 103874 <A(11) 00 10
23259 45136533 -7729 <A(11) 013874 00 10
23260 45136539 -7731 <C(21) 013875 00 10
23261 45136544 -7728 (12)C> 013875 00 10
23262 45152044 22 103875 (12)C> 00 10
23263 45152048 24 103876 (11)B> 10
23264 45152053 21 103876 <A(11)
23265 45175309 -7731 <A(11) 013876
23266 45175315 -7733 <C(21) 013877
23267 45175320 -7730 (12)C> 013877
23268 45190828 24 103877 (12)C>
23269 45190832 26 103878 (11)B>
23270 45190835 23 103878 <A(10) 20
23271 45190841 21 103877 <A(11) 00 20
23272 45214103 -7733 <A(11) 013877 00 20
23273 45214109 -7735 <C(21) 013878 00 20
23274 45214114 -7732 (12)C> 013878 00 20
23275 45229626 24 103878 (12)C> 00 20
23276 45229630 26 103879 (11)B> 20
23277 45229635 23 103879 <B(10) 10
23278 45229637 21 103878 <B(02) 102
23279 45237393 -7735 <B(02) 023878 102
23280 45237395 -7737 <D(22) 023879 102
23281 45237398 -7734 (01)A> 023879 102
23282 45237405 -7737 <C(21) 01 023878 102
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 101+V(1) <A(11) 00 10
1 6+6*V(1) -2+-2*V(1) <A(11) 011+V(1) 00 10
2 12+6*V(1) -4+-2*V(1) <C(21) 012+V(1) 00 10
3 17+6*V(1) -1+-2*V(1) (12)C> 012+V(1) 00 10
4 25+10*V(1) 3 102+V(1) (12)C> 00 10
5 29+10*V(1) 5 103+V(1) (11)B> 10
6 34+10*V(1) 2 103+V(1) <A(11)
7 52+16*V(1) -4+-2*V(1) <A(11) 013+V(1)
8 58+16*V(1) -6+-2*V(1) <C(21) 014+V(1)
9 63+16*V(1) -3+-2*V(1) (12)C> 014+V(1)
10 79+20*V(1) 5 104+V(1) (12)C>
11 83+20*V(1) 7 105+V(1) (11)B>
12 86+20*V(1) 4 105+V(1) <A(10) 20
13 92+20*V(1) 2 104+V(1) <A(11) 00 20
14 116+26*V(1) -6+-2*V(1) <A(11) 014+V(1) 00 20
15 122+26*V(1) -8+-2*V(1) <C(21) 015+V(1) 00 20
16 127+26*V(1) -5+-2*V(1) (12)C> 015+V(1) 00 20
17 147+30*V(1) 5 105+V(1) (12)C> 00 20
18 151+30*V(1) 7 106+V(1) (11)B> 20
19 156+30*V(1) 4 106+V(1) <B(10) 10
20 158+30*V(1) 2 105+V(1) <B(02) 102
21 168+32*V(1) -8+-2*V(1) <B(02) 025+V(1) 102
22 170+32*V(1) -10+-2*V(1) <D(22) 026+V(1) 102
23 173+32*V(1) -7+-2*V(1) (01)A> 026+V(1) 102
24 180+32*V(1) -10+-2*V(1) <C(21) 01 025+V(1) 102
<< Success! ==> defined new CTR 16 (PPA)
23282 45237405 -7737 <C(21) 01 023878 102
== Executing PA-CTR 1, V(1)=3875, V(2)=0, repcount=1938, factor=3/2
34910 101619639 -11613 <C(21) 015815 022 102
== Executing PPA-CTR 2 (once), V(1)=5814
34943 101887421 -11623 <C(21) 01 025822 102
== Executing PA-CTR 1, V(1)=5819, V(2)=0, repcount=2910, factor=3/2
52403 228975851 -17443 <C(21) 018731 022 102
== Executing PPA-CTR 2 (once), V(1)=8730
52436 229377769 -17453 <C(21) 01 028738 102
== Executing PA-CTR 1, V(1)=8735, V(2)=0, repcount=4368, factor=3/2
78644 515669593 -26189 <C(21) 0113105 022 102
== Executing PPA-CTR 2 (once), V(1)=13104
78677 516272715 -26199 <C(21) 01 0213112 102
== Executing PA-CTR 1, V(1)=13109, V(2)=0, repcount=6555, factor=3/2
118007 1160943855 -39309 <C(21) 0119666 022 102
== Executing PPA-CTR 2 (once), V(1)=19665
118040 1161848783 -39319 <C(21) 01 0219673 102
== Executing PA-CTR 1, V(1)=19670, V(2)=0, repcount=9836, factor=3/2
177056 2613278451 -58991 <C(21) 0129509 02 102
== Executing PPA-CTR 9 (once), V(1)=0, V(2)=29506
177069 2613455555 -58993 <C(21) 01 0229509 103 02
== Executing PA-CTR 3, V(1)=29506, V(2)=0, repcount=14754, factor=3/2
265593 5879002637 -88501 <C(21) 0144263 02 103 02
265594 5879002642 -88498 (12)C> 0144263 02 103 02
265595 5879179694 28 1044263 (12)C> 02 103 02
265596 5879179698 30 1044264 (11)A> 103 02
265597 5879179702 32 1044264 11 (01)A> 102 02
265598 5879179710 36 1044264 11 012 (01)A> 02
265599 5879179717 33 1044264 11 012 <C(21) 01
265600 5879179719 31 1044264 11 01 <C(20) 21 01
265601 5879179721 29 1044264 11 <C(20) 20 21 01
265602 5879179723 27 1044264 <A(10) 202 21 01
265603 5879179729 25 1044263 <A(11) 00 202 21 01
265604 5879445307 -88501 <A(11) 0144263 00 202 21 01
265605 5879445313 -88503 <C(21) 0144264 00 202 21 01
265606 5879445318 -88500 (12)C> 0144264 00 202 21 01
265607 5879622374 28 1044264 (12)C> 00 202 21 01
265608 5879622378 30 1044265 (11)B> 202 21 01
265609 5879622383 27 1044265 <B(10) 10 20 21 01
265610 5879622385 25 1044264 <B(02) 102 20 21 01
265611 5879710913 -88503 <B(02) 0244264 102 20 21 01
265612 5879710915 -88505 <D(22) 0244265 102 20 21 01
265613 5879710918 -88502 (01)A> 0244265 102 20 21 01
265614 5879710925 -88505 <C(21) 01 0244264 102 20 21 01
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <C(21) 012+V(2) 02 103+V(1) 02
1 5 3 (12)C> 012+V(2) 02 103+V(1) 02
2 13+4*V(2) 7+2*V(2) 102+V(2) (12)C> 02 103+V(1) 02
3 17+4*V(2) 9+2*V(2) 103+V(2) (11)A> 103+V(1) 02
4 21+4*V(2) 11+2*V(2) 103+V(2) 11 (01)A> 102+V(1) 02
5 29+4*V(1)+4*V(2) 15+2*V(1)+2*V(2) 103+V(2) 11 012+V(1) (01)A> 02
6 36+4*V(1)+4*V(2) 12+2*V(1)+2*V(2) 103+V(2) 11 012+V(1) <C(21) 01
7 38+4*V(1)+4*V(2) 10+2*V(1)+2*V(2) 103+V(2) 11 011+V(1) <C(20) 21 01
8 40+6*V(1)+4*V(2) 8+2*V(2) 103+V(2) 11 <C(20) 201+V(1) 21 01
9 42+6*V(1)+4*V(2) 6+2*V(2) 103+V(2) <A(10) 202+V(1) 21 01
10 48+6*V(1)+4*V(2) 4+2*V(2) 102+V(2) <A(11) 00 202+V(1) 21 01
11 60+6*V(1)+10*V(2) 0 <A(11) 012+V(2) 00 202+V(1) 21 01
12 66+6*V(1)+10*V(2) -2 <C(21) 013+V(2) 00 202+V(1) 21 01
13 71+6*V(1)+10*V(2) 1 (12)C> 013+V(2) 00 202+V(1) 21 01
14 83+6*V(1)+14*V(2) 7+2*V(2) 103+V(2) (12)C> 00 202+V(1) 21 01
15 87+6*V(1)+14*V(2) 9+2*V(2) 104+V(2) (11)B> 202+V(1) 21 01
16 92+6*V(1)+14*V(2) 6+2*V(2) 104+V(2) <B(10) 10 201+V(1) 21 01
17 94+6*V(1)+14*V(2) 4+2*V(2) 103+V(2) <B(02) 102 201+V(1) 21 01
18 100+6*V(1)+16*V(2) -2 <B(02) 023+V(2) 102 201+V(1) 21 01
19 102+6*V(1)+16*V(2) -4 <D(22) 024+V(2) 102 201+V(1) 21 01
20 105+6*V(1)+16*V(2) -1 (01)A> 024+V(2) 102 201+V(1) 21 01
21 112+6*V(1)+16*V(2) -4 <C(21) 01 023+V(2) 102 201+V(1) 21 01
<< Success! ==> defined new CTR 17 (PPA)
265614 5879710925 -88505 <C(21) 01 0244264 102 20 21 01
== Executing PA-CTR 4, V(1)=44261, V(2)=0, repcount=22131, factor=3/2
398400 13226937353 -132767 <C(21) 0166394 022 102 20 21 01
398401 13226937358 -132764 (12)C> 0166394 022 102 20 21 01
398402 13227202934 24 1066394 (12)C> 022 102 20 21 01
398403 13227202938 26 1066395 (11)A> 02 102 20 21 01
398404 13227202945 23 1066395 <A(11) 01 102 20 21 01
398405 13227601315 -132767 <A(11) 0166396 102 20 21 01
398406 13227601321 -132769 <C(21) 0166397 102 20 21 01
398407 13227601326 -132766 (12)C> 0166397 102 20 21 01
398408 13227866914 28 1066397 (12)C> 102 20 21 01
398409 13227866917 25 1066397 <A(11) 00 10 20 21 01
398410 13228265299 -132769 <A(11) 0166397 00 10 20 21 01
398411 13228265305 -132771 <C(21) 0166398 00 10 20 21 01
398412 13228265310 -132768 (12)C> 0166398 00 10 20 21 01
398413 13228530902 28 1066398 (12)C> 00 10 20 21 01
398414 13228530906 30 1066399 (11)B> 10 20 21 01
398415 13228530911 27 1066399 <A(11) 00 20 21 01
398416 13228929305 -132771 <A(11) 0166399 00 20 21 01
398417 13228929311 -132773 <C(21) 0166400 00 20 21 01
398418 13228929316 -132770 (12)C> 0166400 00 20 21 01
398419 13229194916 30 1066400 (12)C> 00 20 21 01
398420 13229194920 32 1066401 (11)B> 20 21 01
398421 13229194925 29 1066401 <B(10) 10 21 01
398422 13229194927 27 1066400 <B(02) 102 21 01
398423 13229327727 -132773 <B(02) 0266400 102 21 01
398424 13229327729 -132775 <D(22) 0266401 102 21 01
398425 13229327732 -132772 (01)A> 0266401 102 21 01
398426 13229327739 -132775 <C(21) 01 0266400 102 21 01
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <C(21) 011+V(1) 022 102 20 [*]* [*]*
1 5 3 (12)C> 011+V(1) 022 102 20 [*]* [*]*
2 9+4*V(1) 5+2*V(1) 101+V(1) (12)C> 022 102 20 [*]* [*]*
3 13+4*V(1) 7+2*V(1) 102+V(1) (11)A> 02 102 20 [*]* [*]*
4 20+4*V(1) 4+2*V(1) 102+V(1) <A(11) 01 102 20 [*]* [*]*
5 32+10*V(1) 0 <A(11) 013+V(1) 102 20 [*]* [*]*
6 38+10*V(1) -2 <C(21) 014+V(1) 102 20 [*]* [*]*
7 43+10*V(1) 1 (12)C> 014+V(1) 102 20 [*]* [*]*
8 59+14*V(1) 9+2*V(1) 104+V(1) (12)C> 102 20 [*]* [*]*
9 62+14*V(1) 6+2*V(1) 104+V(1) <A(11) 00 10 20 [*]* [*]*
10 86+20*V(1) -2 <A(11) 014+V(1) 00 10 20 [*]* [*]*
11 92+20*V(1) -4 <C(21) 015+V(1) 00 10 20 [*]* [*]*
12 97+20*V(1) -1 (12)C> 015+V(1) 00 10 20 [*]* [*]*
13 117+24*V(1) 9+2*V(1) 105+V(1) (12)C> 00 10 20 [*]* [*]*
14 121+24*V(1) 11+2*V(1) 106+V(1) (11)B> 10 20 [*]* [*]*
15 126+24*V(1) 8+2*V(1) 106+V(1) <A(11) 00 20 [*]* [*]*
16 162+30*V(1) -4 <A(11) 016+V(1) 00 20 [*]* [*]*
17 168+30*V(1) -6 <C(21) 017+V(1) 00 20 [*]* [*]*
18 173+30*V(1) -3 (12)C> 017+V(1) 00 20 [*]* [*]*
19 201+34*V(1) 11+2*V(1) 107+V(1) (12)C> 00 20 [*]* [*]*
20 205+34*V(1) 13+2*V(1) 108+V(1) (11)B> 20 [*]* [*]*
21 210+34*V(1) 10+2*V(1) 108+V(1) <B(10) 10 [*]* [*]*
22 212+34*V(1) 8+2*V(1) 107+V(1) <B(02) 102 [*]* [*]*
23 226+36*V(1) -6 <B(02) 027+V(1) 102 [*]* [*]*
24 228+36*V(1) -8 <D(22) 028+V(1) 102 [*]* [*]*
25 231+36*V(1) -5 (01)A> 028+V(1) 102 [*]* [*]*
26 238+36*V(1) -8 <C(21) 01 027+V(1) 102 [*]* [*]*
<< Success! ==> defined new CTR 18 (PPA)
398426 13229327739 -132775 <C(21) 01 0266400 102 21 01
== Executing PA-CTR 5, V(1)=66397, V(2)=0, repcount=33199, factor=3/2
597620 29762695331 -199173 <C(21) 0199598 022 102 21 01
597621 29762695336 -199170 (12)C> 0199598 022 102 21 01
597622 29763093728 26 1099598 (12)C> 022 102 21 01
597623 29763093732 28 1099599 (11)A> 02 102 21 01
597624 29763093739 25 1099599 <A(11) 01 102 21 01
597625 29763691333 -199173 <A(11) 0199600 102 21 01
597626 29763691339 -199175 <C(21) 0199601 102 21 01
597627 29763691344 -199172 (12)C> 0199601 102 21 01
597628 29764089748 30 1099601 (12)C> 102 21 01
597629 29764089751 27 1099601 <A(11) 00 10 21 01
597630 29764687357 -199175 <A(11) 0199601 00 10 21 01
Lines: 500
Top steps: 499
Macro steps: 597630
Basic steps: 29764687357
Tape index: -199175
nonzeros: 99607
log10(nonzeros): 4.998
log10(steps ): 10.474
Input to awk program:
gohalt 1
nbs 3
T 4-state 3-symbol #c (T.J. & S. Ligocki)
: >1.6x10^809 >7.7x10^1618
5T 1RB 2RC 1RA 2LC 1LA 1LB 2LD 0LB 0RC 0RD 1RH 0RA
L 12
M 500
pref sim
machv Lig43_c just simple
machv Lig43_c-r with repetitions reduced
machv Lig43_c-1 with tape symbol exponents
machv Lig43_c-m as 2-bck-macro machine
machv Lig43_c-a as 2-bck-macro machine with pure additive config-TRs
iam Lig43_c-a
mtype 2 0
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:14:04 CEST 2010
edate Tue Jul 6 22:14:06 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:04 CEST 2010