Comment: This TM produces >8.9x10^4931 nonzeros in >7.9x10^9863 steps.
| State | on 0 |
on 1 |
on 2 |
on 0 | on 1 | on 2 | ||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Move | Goto | Move | Goto | Move | Goto | |||||||
| A | 1RB | 1LD | 1RH | 1 | right | B | 1 | left | D | 1 | right | H |
| B | 1RC | 2LB | 2LD | 1 | right | C | 2 | left | B | 2 | left | D |
| C | 1LC | 2RA | 0RD | 1 | left | C | 2 | right | A | 0 | right | D |
| D | 1RC | 1LA | 0LA | 1 | right | C | 1 | left | A | 0 | 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-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 2 2 (11)C>
2 7 -1 <D(10) 10
3 10 2 01 (21)B> 10
4 13 -1 01 <D(22) 20
5 17 -3 <B(22) 22 20
6 22 0 01 (11)C> 22 20
7 26 2 01 11 (11)C> 20
8 28 4 01 112 (01)C>
9 36 6 01 113 (21)B>
10 43 3 01 113 <A(01) 01
11 45 1 01 112 <A(11) 012
12 49 -3 01 <A(11) 112 012
13 55 -5 <D(10) 113 012
14 58 -2 01 (21)B> 113 012
15 61 -5 01 <D(22) 21 112 012
16 65 -7 <B(22) 22 21 112 012
17 70 -4 01 (11)C> 22 21 112 012
18 74 -2 01 11 (11)C> 21 112 012
19 81 -5 01 11 <B(22) 22 112 012
20 83 -7 01 <B(22) 222 112 012
21 90 -4 11 (10)D> 222 112 012
22 98 0 113 (10)D> 112 012
23 103 -3 113 <B(22) 21 11 012
24 109 -9 <B(22) 223 21 11 012
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <B(22) 221+V(2) 21 112+V(1) [*]*
1 5 3 01 (11)C> 221+V(2) 21 112+V(1) [*]*
2 9+4*V(2) 5+2*V(2) 01 111+V(2) (11)C> 21 112+V(1) [*]*
3 16+4*V(2) 2+2*V(2) 01 111+V(2) <B(22) 22 112+V(1) [*]*
4 18+6*V(2) 0 01 <B(22) 222+V(2) 112+V(1) [*]*
5 25+6*V(2) 3 11 (10)D> 222+V(2) 112+V(1) [*]*
6 33+10*V(2) 7+2*V(2) 113+V(2) (10)D> 112+V(1) [*]*
7 38+10*V(2) 4+2*V(2) 113+V(2) <B(22) 21 111+V(1) [*]*
8 44+12*V(2) -2 <B(22) 223+V(2) 21 111+V(1) [*]*
<< Success! ==> defined new CTR 1 (PA)
25 114 -6 01 (11)C> 223 21 11 012
26 126 0 01 113 (11)C> 21 11 012
27 133 -3 01 113 <B(22) 22 11 012
28 139 -9 01 <B(22) 224 11 012
29 146 -6 11 (10)D> 224 11 012
30 162 2 115 (10)D> 11 012
31 167 -1 115 <B(22) 21 012
32 177 -11 <B(22) 225 21 012
33 182 -8 01 (11)C> 225 21 012
34 202 2 01 115 (11)C> 21 012
35 209 -1 01 115 <B(22) 22 012
36 219 -11 01 <B(22) 226 012
37 226 -8 11 (10)D> 226 012
38 250 4 117 (10)D> 012
39 252 6 117 10 (12)A> 01
40 257 3 117 10 <A(12) 22
41 261 1 117 <B(22) 222
42 275 -13 <B(22) 229
43 280 -10 01 (11)C> 229
44 316 8 01 119 (11)C>
45 321 5 01 119 <D(10) 10
46 323 3 01 118 <D(11) 102
47 339 -13 01 <D(11) 118 102
48 343 -15 <B(22) 119 102
49 348 -12 01 (11)C> 119 102
50 353 -15 01 <A(11) 01 118 102
51 359 -17 <D(10) 11 01 118 102
52 362 -14 01 (21)B> 11 01 118 102
53 365 -17 01 <D(22) 21 01 118 102
54 369 -19 <B(22) 22 21 01 118 102
55 374 -16 01 (11)C> 22 21 01 118 102
56 378 -14 01 11 (11)C> 21 01 118 102
57 385 -17 01 11 <B(22) 22 01 118 102
58 387 -19 01 <B(22) 222 01 118 102
59 394 -16 11 (10)D> 222 01 118 102
60 402 -12 113 (10)D> 01 118 102
61 404 -10 113 10 (12)A> 118 102
62 407 -13 113 10 <D(10) 118 102
63 410 -10 114 (21)B> 118 102
64 413 -13 114 <D(22) 21 117 102
65 415 -15 113 <D(11) 22 21 117 102
66 421 -21 <D(11) 113 22 21 117 102
67 433 -23 <A(12) 22 113 22 21 117 102
68 442 -20 11 (10)D> 22 113 22 21 117 102
69 446 -18 112 (10)D> 113 22 21 117 102
70 451 -21 112 <B(22) 21 112 22 21 117 102
71 455 -25 <B(22) 222 21 112 22 21 117 102
72 460 -22 01 (11)C> 222 21 112 22 21 117 102
73 468 -18 01 112 (11)C> 21 112 22 21 117 102
74 475 -21 01 112 <B(22) 22 112 22 21 117 102
75 479 -25 01 <B(22) 223 112 22 21 117 102
76 486 -22 11 (10)D> 223 112 22 21 117 102
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 11 (10)D> 221+V(2) 112+V(1) [*]* [*]* [*]* [*]*
1 4+4*V(2) 2+2*V(2) 112+V(2) (10)D> 112+V(1) [*]* [*]* [*]* [*]*
2 9+4*V(2) -1+2*V(2) 112+V(2) <B(22) 21 111+V(1) [*]* [*]* [*]* [*]*
3 13+6*V(2) -5 <B(22) 222+V(2) 21 111+V(1) [*]* [*]* [*]* [*]*
4 18+6*V(2) -2 01 (11)C> 222+V(2) 21 111+V(1) [*]* [*]* [*]* [*]*
5 26+10*V(2) 2+2*V(2) 01 112+V(2) (11)C> 21 111+V(1) [*]* [*]* [*]* [*]*
6 33+10*V(2) -1+2*V(2) 01 112+V(2) <B(22) 22 111+V(1) [*]* [*]* [*]* [*]*
7 37+12*V(2) -5 01 <B(22) 223+V(2) 111+V(1) [*]* [*]* [*]* [*]*
8 44+12*V(2) -2 11 (10)D> 223+V(2) 111+V(1) [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 2 (PA)
76 486 -22 11 (10)D> 223 112 22 21 117 102
== Executing PA-CTR 2, V(1)=0, V(2)=2, repcount=1, factor=2/1
84 554 -24 11 (10)D> 225 11 22 21 117 102
85 574 -14 116 (10)D> 11 22 21 117 102
86 579 -17 116 <B(22) 21 22 21 117 102
87 591 -29 <B(22) 226 21 22 21 117 102
88 596 -26 01 (11)C> 226 21 22 21 117 102
89 620 -14 01 116 (11)C> 21 22 21 117 102
90 627 -17 01 116 <B(22) 222 21 117 102
91 639 -29 01 <B(22) 228 21 117 102
92 646 -26 11 (10)D> 228 21 117 102
93 678 -10 119 (10)D> 21 117 102
94 682 -8 1110 (12)A> 117 102
95 685 -11 1110 <D(10) 117 102
96 687 -13 119 <D(11) 10 117 102
97 705 -31 <D(11) 119 10 117 102
98 717 -33 <A(12) 22 119 10 117 102
99 726 -30 11 (10)D> 22 119 10 117 102
100 730 -28 112 (10)D> 119 10 117 102
101 735 -31 112 <B(22) 21 118 10 117 102
102 739 -35 <B(22) 222 21 118 10 117 102
103 744 -32 01 (11)C> 222 21 118 10 117 102
104 752 -28 01 112 (11)C> 21 118 10 117 102
105 759 -31 01 112 <B(22) 22 118 10 117 102
106 763 -35 01 <B(22) 223 118 10 117 102
107 770 -32 11 (10)D> 223 118 10 117 102
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 11 (10)D> 221+V(2) 112+V(1) [*]* [*]* [*]*
1 4+4*V(2) 2+2*V(2) 112+V(2) (10)D> 112+V(1) [*]* [*]* [*]*
2 9+4*V(2) -1+2*V(2) 112+V(2) <B(22) 21 111+V(1) [*]* [*]* [*]*
3 13+6*V(2) -5 <B(22) 222+V(2) 21 111+V(1) [*]* [*]* [*]*
4 18+6*V(2) -2 01 (11)C> 222+V(2) 21 111+V(1) [*]* [*]* [*]*
5 26+10*V(2) 2+2*V(2) 01 112+V(2) (11)C> 21 111+V(1) [*]* [*]* [*]*
6 33+10*V(2) -1+2*V(2) 01 112+V(2) <B(22) 22 111+V(1) [*]* [*]* [*]*
7 37+12*V(2) -5 01 <B(22) 223+V(2) 111+V(1) [*]* [*]* [*]*
8 44+12*V(2) -2 11 (10)D> 223+V(2) 111+V(1) [*]* [*]* [*]*
<< Success! ==> defined new CTR 3 (PA)
107 770 -32 11 (10)D> 223 118 10 117 102
== Executing PA-CTR 3, V(1)=6, V(2)=2, repcount=7, factor=2/1
163 1750 -46 11 (10)D> 2217 11 10 117 102
164 1818 -12 1118 (10)D> 11 10 117 102
165 1823 -15 1118 <B(22) 21 10 117 102
166 1859 -51 <B(22) 2218 21 10 117 102
167 1864 -48 01 (11)C> 2218 21 10 117 102
168 1936 -12 01 1118 (11)C> 21 10 117 102
169 1943 -15 01 1118 <B(22) 22 10 117 102
170 1979 -51 01 <B(22) 2219 10 117 102
171 1986 -48 11 (10)D> 2219 10 117 102
172 2062 -10 1120 (10)D> 10 117 102
173 2067 -13 1120 <B(22) 20 117 102
174 2107 -53 <B(22) 2220 20 117 102
175 2112 -50 01 (11)C> 2220 20 117 102
176 2192 -10 01 1120 (11)C> 20 117 102
177 2194 -8 01 1121 (01)C> 117 102
178 2205 -11 01 1121 <A(12) 22 116 102
179 2207 -13 01 1120 <A(11) 12 22 116 102
180 2247 -53 01 <A(11) 1120 12 22 116 102
181 2253 -55 <D(10) 1121 12 22 116 102
182 2256 -52 01 (21)B> 1121 12 22 116 102
183 2259 -55 01 <D(22) 21 1120 12 22 116 102
184 2263 -57 <B(22) 22 21 1120 12 22 116 102
185 2268 -54 01 (11)C> 22 21 1120 12 22 116 102
186 2272 -52 01 11 (11)C> 21 1120 12 22 116 102
187 2279 -55 01 11 <B(22) 22 1120 12 22 116 102
188 2281 -57 01 <B(22) 222 1120 12 22 116 102
189 2288 -54 11 (10)D> 222 1120 12 22 116 102
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 111+V(1) (10)D> 221+V(3) 11 10 112+V(2) [*]*
1 4+4*V(3) 2+2*V(3) 112+V(1)+V(3) (10)D> 11 10 112+V(2) [*]*
2 9+4*V(3) -1+2*V(3) 112+V(1)+V(3) <B(22) 21 10 112+V(2) [*]*
3 13+2*V(1)+6*V(3) -5+-2*V(1) <B(22) 222+V(1)+V(3) 21 10 112+V(2) [*]*
4 18+2*V(1)+6*V(3) -2+-2*V(1) 01 (11)C> 222+V(1)+V(3) 21 10 112+V(2) [*]*
5 26+6*V(1)+10*V(3) 2+2*V(3) 01 112+V(1)+V(3) (11)C> 21 10 112+V(2) [*]*
6 33+6*V(1)+10*V(3) -1+2*V(3) 01 112+V(1)+V(3) <B(22) 22 10 112+V(2) [*]*
7 37+8*V(1)+12*V(3) -5+-2*V(1) 01 <B(22) 223+V(1)+V(3) 10 112+V(2) [*]*
8 44+8*V(1)+12*V(3) -2+-2*V(1) 11 (10)D> 223+V(1)+V(3) 10 112+V(2) [*]*
9 56+12*V(1)+16*V(3) 4+2*V(3) 114+V(1)+V(3) (10)D> 10 112+V(2) [*]*
10 61+12*V(1)+16*V(3) 1+2*V(3) 114+V(1)+V(3) <B(22) 20 112+V(2) [*]*
11 69+14*V(1)+18*V(3) -7+-2*V(1) <B(22) 224+V(1)+V(3) 20 112+V(2) [*]*
12 74+14*V(1)+18*V(3) -4+-2*V(1) 01 (11)C> 224+V(1)+V(3) 20 112+V(2) [*]*
13 90+18*V(1)+22*V(3) 4+2*V(3) 01 114+V(1)+V(3) (11)C> 20 112+V(2) [*]*
14 92+18*V(1)+22*V(3) 6+2*V(3) 01 115+V(1)+V(3) (01)C> 112+V(2) [*]*
15 103+18*V(1)+22*V(3) 3+2*V(3) 01 115+V(1)+V(3) <A(12) 22 111+V(2) [*]*
16 105+18*V(1)+22*V(3) 1+2*V(3) 01 114+V(1)+V(3) <A(11) 12 22 111+V(2) [*]*
17 113+20*V(1)+24*V(3) -7+-2*V(1) 01 <A(11) 114+V(1)+V(3) 12 22 111+V(2) [*]*
18 119+20*V(1)+24*V(3) -9+-2*V(1) <D(10) 115+V(1)+V(3) 12 22 111+V(2) [*]*
19 122+20*V(1)+24*V(3) -6+-2*V(1) 01 (21)B> 115+V(1)+V(3) 12 22 111+V(2) [*]*
20 125+20*V(1)+24*V(3) -9+-2*V(1) 01 <D(22) 21 114+V(1)+V(3) 12 22 111+V(2) [*]*
21 129+20*V(1)+24*V(3) -11+-2*V(1) <B(22) 22 21 114+V(1)+V(3) 12 22 111+V(2) [*]*
22 134+20*V(1)+24*V(3) -8+-2*V(1) 01 (11)C> 22 21 114+V(1)+V(3) 12 22 111+V(2) [*]*
23 138+20*V(1)+24*V(3) -6+-2*V(1) 01 11 (11)C> 21 114+V(1)+V(3) 12 22 111+V(2) [*]*
24 145+20*V(1)+24*V(3) -9+-2*V(1) 01 11 <B(22) 22 114+V(1)+V(3) 12 22 111+V(2) [*]*
25 147+20*V(1)+24*V(3) -11+-2*V(1) 01 <B(22) 222 114+V(1)+V(3) 12 22 111+V(2) [*]*
26 154+20*V(1)+24*V(3) -8+-2*V(1) 11 (10)D> 222 114+V(1)+V(3) 12 22 111+V(2) [*]*
<< Success! ==> defined new CTR 4 (PPA)
189 2288 -54 11 (10)D> 222 1120 12 22 116 102
== Executing PA-CTR 2, V(1)=18, V(2)=1, repcount=19, factor=2/1
341 7456 -92 11 (10)D> 2240 11 12 22 116 102
342 7616 -12 1141 (10)D> 11 12 22 116 102
343 7621 -15 1141 <B(22) 21 12 22 116 102
344 7703 -97 <B(22) 2241 21 12 22 116 102
345 7708 -94 01 (11)C> 2241 21 12 22 116 102
346 7872 -12 01 1141 (11)C> 21 12 22 116 102
347 7879 -15 01 1141 <B(22) 22 12 22 116 102
348 7961 -97 01 <B(22) 2242 12 22 116 102
349 7968 -94 11 (10)D> 2242 12 22 116 102
350 8136 -10 1143 (10)D> 12 22 116 102
351 8141 -13 1143 <B(22) 222 116 102
352 8227 -99 <B(22) 2245 116 102
353 8232 -96 01 (11)C> 2245 116 102
354 8412 -6 01 1145 (11)C> 116 102
355 8417 -9 01 1145 <A(11) 01 115 102
356 8507 -99 01 <A(11) 1145 01 115 102
357 8513 -101 <D(10) 1146 01 115 102
358 8516 -98 01 (21)B> 1146 01 115 102
359 8519 -101 01 <D(22) 21 1145 01 115 102
360 8523 -103 <B(22) 22 21 1145 01 115 102
361 8528 -100 01 (11)C> 22 21 1145 01 115 102
362 8532 -98 01 11 (11)C> 21 1145 01 115 102
363 8539 -101 01 11 <B(22) 22 1145 01 115 102
364 8541 -103 01 <B(22) 222 1145 01 115 102
365 8548 -100 11 (10)D> 222 1145 01 115 102
>> Try to prove a PPA-CTR with 4 Vars...
0 0 0 111+V(1) (10)D> 221+V(4) 11 12 221+V(3) 112+V(2) [*]*
1 4+4*V(4) 2+2*V(4) 112+V(1)+V(4) (10)D> 11 12 221+V(3) 112+V(2) [*]*
2 9+4*V(4) -1+2*V(4) 112+V(1)+V(4) <B(22) 21 12 221+V(3) 112+V(2) [*]*
3 13+2*V(1)+6*V(4) -5+-2*V(1) <B(22) 222+V(1)+V(4) 21 12 221+V(3) 112+V(2) [*]*
4 18+2*V(1)+6*V(4) -2+-2*V(1) 01 (11)C> 222+V(1)+V(4) 21 12 221+V(3) 112+V(2) [*]*
5 26+6*V(1)+10*V(4) 2+2*V(4) 01 112+V(1)+V(4) (11)C> 21 12 221+V(3) 112+V(2) [*]*
6 33+6*V(1)+10*V(4) -1+2*V(4) 01 112+V(1)+V(4) <B(22) 22 12 221+V(3) 112+V(2) [*]*
7 37+8*V(1)+12*V(4) -5+-2*V(1) 01 <B(22) 223+V(1)+V(4) 12 221+V(3) 112+V(2) [*]*
8 44+8*V(1)+12*V(4) -2+-2*V(1) 11 (10)D> 223+V(1)+V(4) 12 221+V(3) 112+V(2) [*]*
9 56+12*V(1)+16*V(4) 4+2*V(4) 114+V(1)+V(4) (10)D> 12 221+V(3) 112+V(2) [*]*
10 61+12*V(1)+16*V(4) 1+2*V(4) 114+V(1)+V(4) <B(22) 222+V(3) 112+V(2) [*]*
11 69+14*V(1)+18*V(4) -7+-2*V(1) <B(22) 226+V(1)+V(3)+V(4) 112+V(2) [*]*
12 74+14*V(1)+18*V(4) -4+-2*V(1) 01 (11)C> 226+V(1)+V(3)+V(4) 112+V(2) [*]*
13 98+18*V(1)+4*V(3)+22*V(4) 8+2*V(3)+2*V(4) 01 116+V(1)+V(3)+V(4) (11)C> 112+V(2) [*]*
14 103+18*V(1)+4*V(3)+22*V(4) 5+2*V(3)+2*V(4) 01 116+V(1)+V(3)+V(4) <A(11) 01 111+V(2) [*]*
15 115+20*V(1)+6*V(3)+24*V(4) -7+-2*V(1) 01 <A(11) 116+V(1)+V(3)+V(4) 01 111+V(2) [*]*
16 121+20*V(1)+6*V(3)+24*V(4) -9+-2*V(1) <D(10) 117+V(1)+V(3)+V(4) 01 111+V(2) [*]*
17 124+20*V(1)+6*V(3)+24*V(4) -6+-2*V(1) 01 (21)B> 117+V(1)+V(3)+V(4) 01 111+V(2) [*]*
18 127+20*V(1)+6*V(3)+24*V(4) -9+-2*V(1) 01 <D(22) 21 116+V(1)+V(3)+V(4) 01 111+V(2) [*]*
19 131+20*V(1)+6*V(3)+24*V(4) -11+-2*V(1) <B(22) 22 21 116+V(1)+V(3)+V(4) 01 111+V(2) [*]*
20 136+20*V(1)+6*V(3)+24*V(4) -8+-2*V(1) 01 (11)C> 22 21 116+V(1)+V(3)+V(4) 01 111+V(2) [*]*
21 140+20*V(1)+6*V(3)+24*V(4) -6+-2*V(1) 01 11 (11)C> 21 116+V(1)+V(3)+V(4) 01 111+V(2) [*]*
22 147+20*V(1)+6*V(3)+24*V(4) -9+-2*V(1) 01 11 <B(22) 22 116+V(1)+V(3)+V(4) 01 111+V(2) [*]*
23 149+20*V(1)+6*V(3)+24*V(4) -11+-2*V(1) 01 <B(22) 222 116+V(1)+V(3)+V(4) 01 111+V(2) [*]*
24 156+20*V(1)+6*V(3)+24*V(4) -8+-2*V(1) 11 (10)D> 222 116+V(1)+V(3)+V(4) 01 111+V(2) [*]*
<< Success! ==> defined new CTR 5 (PPA)
365 8548 -100 11 (10)D> 222 1145 01 115 102
== Executing PA-CTR 3, V(1)=43, V(2)=1, repcount=44, factor=2/1
717 33716 -188 11 (10)D> 2290 11 01 115 102
718 34076 -8 1191 (10)D> 11 01 115 102
719 34081 -11 1191 <B(22) 21 01 115 102
720 34263 -193 <B(22) 2291 21 01 115 102
721 34268 -190 01 (11)C> 2291 21 01 115 102
722 34632 -8 01 1191 (11)C> 21 01 115 102
723 34639 -11 01 1191 <B(22) 22 01 115 102
724 34821 -193 01 <B(22) 2292 01 115 102
725 34828 -190 11 (10)D> 2292 01 115 102
726 35196 -6 1193 (10)D> 01 115 102
727 35198 -4 1193 10 (12)A> 115 102
728 35201 -7 1193 10 <D(10) 115 102
729 35204 -4 1194 (21)B> 115 102
730 35207 -7 1194 <D(22) 21 114 102
731 35209 -9 1193 <D(11) 22 21 114 102
732 35395 -195 <D(11) 1193 22 21 114 102
733 35407 -197 <A(12) 22 1193 22 21 114 102
734 35416 -194 11 (10)D> 22 1193 22 21 114 102
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 111+V(1) (10)D> 221+V(3) 11 01 112+V(2) [*]*
1 4+4*V(3) 2+2*V(3) 112+V(1)+V(3) (10)D> 11 01 112+V(2) [*]*
2 9+4*V(3) -1+2*V(3) 112+V(1)+V(3) <B(22) 21 01 112+V(2) [*]*
3 13+2*V(1)+6*V(3) -5+-2*V(1) <B(22) 222+V(1)+V(3) 21 01 112+V(2) [*]*
4 18+2*V(1)+6*V(3) -2+-2*V(1) 01 (11)C> 222+V(1)+V(3) 21 01 112+V(2) [*]*
5 26+6*V(1)+10*V(3) 2+2*V(3) 01 112+V(1)+V(3) (11)C> 21 01 112+V(2) [*]*
6 33+6*V(1)+10*V(3) -1+2*V(3) 01 112+V(1)+V(3) <B(22) 22 01 112+V(2) [*]*
7 37+8*V(1)+12*V(3) -5+-2*V(1) 01 <B(22) 223+V(1)+V(3) 01 112+V(2) [*]*
8 44+8*V(1)+12*V(3) -2+-2*V(1) 11 (10)D> 223+V(1)+V(3) 01 112+V(2) [*]*
9 56+12*V(1)+16*V(3) 4+2*V(3) 114+V(1)+V(3) (10)D> 01 112+V(2) [*]*
10 58+12*V(1)+16*V(3) 6+2*V(3) 114+V(1)+V(3) 10 (12)A> 112+V(2) [*]*
11 61+12*V(1)+16*V(3) 3+2*V(3) 114+V(1)+V(3) 10 <D(10) 112+V(2) [*]*
12 64+12*V(1)+16*V(3) 6+2*V(3) 115+V(1)+V(3) (21)B> 112+V(2) [*]*
13 67+12*V(1)+16*V(3) 3+2*V(3) 115+V(1)+V(3) <D(22) 21 111+V(2) [*]*
14 69+12*V(1)+16*V(3) 1+2*V(3) 114+V(1)+V(3) <D(11) 22 21 111+V(2) [*]*
15 77+14*V(1)+18*V(3) -7+-2*V(1) <D(11) 114+V(1)+V(3) 22 21 111+V(2) [*]*
16 89+14*V(1)+18*V(3) -9+-2*V(1) <A(12) 22 114+V(1)+V(3) 22 21 111+V(2) [*]*
17 98+14*V(1)+18*V(3) -6+-2*V(1) 11 (10)D> 22 114+V(1)+V(3) 22 21 111+V(2) [*]*
<< Success! ==> defined new CTR 6 (PPA)
734 35416 -194 11 (10)D> 22 1193 22 21 114 102
== Executing PA-CTR 2, V(1)=91, V(2)=0, repcount=92, factor=2/1
1470 139928 -378 11 (10)D> 22185 11 22 21 114 102
1471 140668 -8 11186 (10)D> 11 22 21 114 102
1472 140673 -11 11186 <B(22) 21 22 21 114 102
1473 141045 -383 <B(22) 22186 21 22 21 114 102
1474 141050 -380 01 (11)C> 22186 21 22 21 114 102
1475 141794 -8 01 11186 (11)C> 21 22 21 114 102
1476 141801 -11 01 11186 <B(22) 222 21 114 102
1477 142173 -383 01 <B(22) 22188 21 114 102
1478 142180 -380 11 (10)D> 22188 21 114 102
1479 142932 -4 11189 (10)D> 21 114 102
1480 142936 -2 11190 (12)A> 114 102
1481 142939 -5 11190 <D(10) 114 102
1482 142941 -7 11189 <D(11) 10 114 102
1483 143319 -385 <D(11) 11189 10 114 102
1484 143331 -387 <A(12) 22 11189 10 114 102
1485 143340 -384 11 (10)D> 22 11189 10 114 102
>> Try to prove a PPA-CTR with 4 Vars...
0 0 0 111+V(1) (10)D> 221+V(4) 11 221+V(3) 21 111+V(2) [*]*
1 4+4*V(4) 2+2*V(4) 112+V(1)+V(4) (10)D> 11 221+V(3) 21 111+V(2) [*]*
2 9+4*V(4) -1+2*V(4) 112+V(1)+V(4) <B(22) 21 221+V(3) 21 111+V(2) [*]*
3 13+2*V(1)+6*V(4) -5+-2*V(1) <B(22) 222+V(1)+V(4) 21 221+V(3) 21 111+V(2) [*]*
4 18+2*V(1)+6*V(4) -2+-2*V(1) 01 (11)C> 222+V(1)+V(4) 21 221+V(3) 21 111+V(2) [*]*
5 26+6*V(1)+10*V(4) 2+2*V(4) 01 112+V(1)+V(4) (11)C> 21 221+V(3) 21 111+V(2) [*]*
6 33+6*V(1)+10*V(4) -1+2*V(4) 01 112+V(1)+V(4) <B(22) 222+V(3) 21 111+V(2) [*]*
7 37+8*V(1)+12*V(4) -5+-2*V(1) 01 <B(22) 224+V(1)+V(3)+V(4) 21 111+V(2) [*]*
8 44+8*V(1)+12*V(4) -2+-2*V(1) 11 (10)D> 224+V(1)+V(3)+V(4) 21 111+V(2) [*]*
9 60+12*V(1)+4*V(3)+16*V(4) 6+2*V(3)+2*V(4) 115+V(1)+V(3)+V(4) (10)D> 21 111+V(2) [*]*
10 64+12*V(1)+4*V(3)+16*V(4) 8+2*V(3)+2*V(4) 116+V(1)+V(3)+V(4) (12)A> 111+V(2) [*]*
11 67+12*V(1)+4*V(3)+16*V(4) 5+2*V(3)+2*V(4) 116+V(1)+V(3)+V(4) <D(10) 111+V(2) [*]*
12 69+12*V(1)+4*V(3)+16*V(4) 3+2*V(3)+2*V(4) 115+V(1)+V(3)+V(4) <D(11) 10 111+V(2) [*]*
13 79+14*V(1)+6*V(3)+18*V(4) -7+-2*V(1) <D(11) 115+V(1)+V(3)+V(4) 10 111+V(2) [*]*
14 91+14*V(1)+6*V(3)+18*V(4) -9+-2*V(1) <A(12) 22 115+V(1)+V(3)+V(4) 10 111+V(2) [*]*
15 100+14*V(1)+6*V(3)+18*V(4) -6+-2*V(1) 11 (10)D> 22 115+V(1)+V(3)+V(4) 10 111+V(2) [*]*
<< Success! ==> defined new CTR 7 (PPA)
1485 143340 -384 11 (10)D> 22 11189 10 114 102
== Executing PA-CTR 3, V(1)=187, V(2)=0, repcount=188, factor=2/1
2989 573484 -760 11 (10)D> 22377 11 10 114 102
== Executing PPA-CTR 4 (once), V(1)=0, V(2)=2, V(3)=376
3015 582662 -768 11 (10)D> 222 11380 12 22 113 102
== Executing PA-CTR 2, V(1)=378, V(2)=1, repcount=379, factor=2/1
6047 2323030 -1526 11 (10)D> 22760 11 12 22 113 102
== Executing PPA-CTR 5 (once), V(1)=0, V(2)=1, V(3)=0, V(4)=759
6071 2341402 -1534 11 (10)D> 222 11765 01 112 102
== Executing PA-CTR 3, V(1)=763, V(2)=1, repcount=764, factor=2/1
12183 9379370 -3062 11 (10)D> 221530 11 01 112 102
== Executing PPA-CTR 6 (once), V(1)=0, V(2)=0, V(3)=1529
12200 9406990 -3068 11 (10)D> 22 111533 22 21 11 102
== Executing PA-CTR 2, V(1)=1531, V(2)=0, repcount=1532, factor=2/1
24456 37620302 -6132 11 (10)D> 223065 11 22 21 11 102
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=0, V(3)=0, V(4)=3064
24471 37675554 -6138 11 (10)D> 22 113069 10 11 102
== Executing PA-CTR 3, V(1)=3067, V(2)=0, repcount=3068, factor=2/1
49015 150725218 -12274 11 (10)D> 226137 11 10 11 102
49016 150749766 0 116138 (10)D> 11 10 11 102
49017 150749771 -3 116138 <B(22) 21 10 11 102
49018 150762047 -12279 <B(22) 226138 21 10 11 102
49019 150762052 -12276 01 (11)C> 226138 21 10 11 102
49020 150786604 0 01 116138 (11)C> 21 10 11 102
49021 150786611 -3 01 116138 <B(22) 22 10 11 102
49022 150798887 -12279 01 <B(22) 226139 10 11 102
49023 150798894 -12276 11 (10)D> 226139 10 11 102
49024 150823450 2 116140 (10)D> 10 11 102
49025 150823455 -1 116140 <B(22) 20 11 102
49026 150835735 -12281 <B(22) 226140 20 11 102
49027 150835740 -12278 01 (11)C> 226140 20 11 102
49028 150860300 2 01 116140 (11)C> 20 11 102
49029 150860302 4 01 116141 (01)C> 11 102
49030 150860313 1 01 116141 <A(12) 22 102
49031 150860315 -1 01 116140 <A(11) 12 22 102
49032 150872595 -12281 01 <A(11) 116140 12 22 102
49033 150872601 -12283 <D(10) 116141 12 22 102
49034 150872604 -12280 01 (21)B> 116141 12 22 102
49035 150872607 -12283 01 <D(22) 21 116140 12 22 102
49036 150872611 -12285 <B(22) 22 21 116140 12 22 102
49037 150872616 -12282 01 (11)C> 22 21 116140 12 22 102
49038 150872620 -12280 01 11 (11)C> 21 116140 12 22 102
49039 150872627 -12283 01 11 <B(22) 22 116140 12 22 102
49040 150872629 -12285 01 <B(22) 222 116140 12 22 102
49041 150872636 -12282 11 (10)D> 222 116140 12 22 102
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 111+V(1) (10)D> 221+V(2) 11 10 11 [*]*
1 4+4*V(2) 2+2*V(2) 112+V(1)+V(2) (10)D> 11 10 11 [*]*
2 9+4*V(2) -1+2*V(2) 112+V(1)+V(2) <B(22) 21 10 11 [*]*
3 13+2*V(1)+6*V(2) -5+-2*V(1) <B(22) 222+V(1)+V(2) 21 10 11 [*]*
4 18+2*V(1)+6*V(2) -2+-2*V(1) 01 (11)C> 222+V(1)+V(2) 21 10 11 [*]*
5 26+6*V(1)+10*V(2) 2+2*V(2) 01 112+V(1)+V(2) (11)C> 21 10 11 [*]*
6 33+6*V(1)+10*V(2) -1+2*V(2) 01 112+V(1)+V(2) <B(22) 22 10 11 [*]*
7 37+8*V(1)+12*V(2) -5+-2*V(1) 01 <B(22) 223+V(1)+V(2) 10 11 [*]*
8 44+8*V(1)+12*V(2) -2+-2*V(1) 11 (10)D> 223+V(1)+V(2) 10 11 [*]*
9 56+12*V(1)+16*V(2) 4+2*V(2) 114+V(1)+V(2) (10)D> 10 11 [*]*
10 61+12*V(1)+16*V(2) 1+2*V(2) 114+V(1)+V(2) <B(22) 20 11 [*]*
11 69+14*V(1)+18*V(2) -7+-2*V(1) <B(22) 224+V(1)+V(2) 20 11 [*]*
12 74+14*V(1)+18*V(2) -4+-2*V(1) 01 (11)C> 224+V(1)+V(2) 20 11 [*]*
13 90+18*V(1)+22*V(2) 4+2*V(2) 01 114+V(1)+V(2) (11)C> 20 11 [*]*
14 92+18*V(1)+22*V(2) 6+2*V(2) 01 115+V(1)+V(2) (01)C> 11 [*]*
15 103+18*V(1)+22*V(2) 3+2*V(2) 01 115+V(1)+V(2) <A(12) 22 [*]*
16 105+18*V(1)+22*V(2) 1+2*V(2) 01 114+V(1)+V(2) <A(11) 12 22 [*]*
17 113+20*V(1)+24*V(2) -7+-2*V(1) 01 <A(11) 114+V(1)+V(2) 12 22 [*]*
18 119+20*V(1)+24*V(2) -9+-2*V(1) <D(10) 115+V(1)+V(2) 12 22 [*]*
19 122+20*V(1)+24*V(2) -6+-2*V(1) 01 (21)B> 115+V(1)+V(2) 12 22 [*]*
20 125+20*V(1)+24*V(2) -9+-2*V(1) 01 <D(22) 21 114+V(1)+V(2) 12 22 [*]*
21 129+20*V(1)+24*V(2) -11+-2*V(1) <B(22) 22 21 114+V(1)+V(2) 12 22 [*]*
22 134+20*V(1)+24*V(2) -8+-2*V(1) 01 (11)C> 22 21 114+V(1)+V(2) 12 22 [*]*
23 138+20*V(1)+24*V(2) -6+-2*V(1) 01 11 (11)C> 21 114+V(1)+V(2) 12 22 [*]*
24 145+20*V(1)+24*V(2) -9+-2*V(1) 01 11 <B(22) 22 114+V(1)+V(2) 12 22 [*]*
25 147+20*V(1)+24*V(2) -11+-2*V(1) 01 <B(22) 222 114+V(1)+V(2) 12 22 [*]*
26 154+20*V(1)+24*V(2) -8+-2*V(1) 11 (10)D> 222 114+V(1)+V(2) 12 22 [*]*
<< Success! ==> defined new CTR 8 (PPA)
49041 150872636 -12282 11 (10)D> 222 116140 12 22 102
== Executing PA-CTR 3, V(1)=6138, V(2)=1, repcount=6139, factor=2/1
98153 603390604 -24560 11 (10)D> 2212280 11 12 22 102
98154 603439724 0 1112281 (10)D> 11 12 22 102
98155 603439729 -3 1112281 <B(22) 21 12 22 102
98156 603464291 -24565 <B(22) 2212281 21 12 22 102
98157 603464296 -24562 01 (11)C> 2212281 21 12 22 102
98158 603513420 0 01 1112281 (11)C> 21 12 22 102
98159 603513427 -3 01 1112281 <B(22) 22 12 22 102
98160 603537989 -24565 01 <B(22) 2212282 12 22 102
98161 603537996 -24562 11 (10)D> 2212282 12 22 102
98162 603587124 2 1112283 (10)D> 12 22 102
98163 603587129 -1 1112283 <B(22) 222 102
98164 603611695 -24567 <B(22) 2212285 102
98165 603611700 -24564 01 (11)C> 2212285 102
98166 603660840 6 01 1112285 (11)C> 102
98167 603660842 8 01 1112286 (21)B> 10
98168 603660845 5 01 1112286 <D(22) 20
98169 603660847 3 01 1112285 <D(11) 22 20
98170 603685417 -24567 01 <D(11) 1112285 22 20
98171 603685421 -24569 <B(22) 1112286 22 20
98172 603685426 -24566 01 (11)C> 1112286 22 20
98173 603685431 -24569 01 <A(11) 01 1112285 22 20
98174 603685437 -24571 <D(10) 11 01 1112285 22 20
98175 603685440 -24568 01 (21)B> 11 01 1112285 22 20
98176 603685443 -24571 01 <D(22) 21 01 1112285 22 20
98177 603685447 -24573 <B(22) 22 21 01 1112285 22 20
98178 603685452 -24570 01 (11)C> 22 21 01 1112285 22 20
98179 603685456 -24568 01 11 (11)C> 21 01 1112285 22 20
98180 603685463 -24571 01 11 <B(22) 22 01 1112285 22 20
98181 603685465 -24573 01 <B(22) 222 01 1112285 22 20
98182 603685472 -24570 11 (10)D> 222 01 1112285 22 20
98183 603685480 -24566 113 (10)D> 01 1112285 22 20
98184 603685482 -24564 113 10 (12)A> 1112285 22 20
98185 603685485 -24567 113 10 <D(10) 1112285 22 20
98186 603685488 -24564 114 (21)B> 1112285 22 20
98187 603685491 -24567 114 <D(22) 21 1112284 22 20
98188 603685493 -24569 113 <D(11) 22 21 1112284 22 20
98189 603685499 -24575 <D(11) 113 22 21 1112284 22 20
98190 603685511 -24577 <A(12) 22 113 22 21 1112284 22 20
98191 603685520 -24574 11 (10)D> 22 113 22 21 1112284 22 20
98192 603685524 -24572 112 (10)D> 113 22 21 1112284 22 20
98193 603685529 -24575 112 <B(22) 21 112 22 21 1112284 22 20
98194 603685533 -24579 <B(22) 222 21 112 22 21 1112284 22 20
98195 603685538 -24576 01 (11)C> 222 21 112 22 21 1112284 22 20
98196 603685546 -24572 01 112 (11)C> 21 112 22 21 1112284 22 20
98197 603685553 -24575 01 112 <B(22) 22 112 22 21 1112284 22 20
98198 603685557 -24579 01 <B(22) 223 112 22 21 1112284 22 20
98199 603685564 -24576 11 (10)D> 223 112 22 21 1112284 22 20
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 11 (10)D> 221+V(2) 112+V(1) [*]* [*]* [*]* [*]* [*]*
1 4+4*V(2) 2+2*V(2) 112+V(2) (10)D> 112+V(1) [*]* [*]* [*]* [*]* [*]*
2 9+4*V(2) -1+2*V(2) 112+V(2) <B(22) 21 111+V(1) [*]* [*]* [*]* [*]* [*]*
3 13+6*V(2) -5 <B(22) 222+V(2) 21 111+V(1) [*]* [*]* [*]* [*]* [*]*
4 18+6*V(2) -2 01 (11)C> 222+V(2) 21 111+V(1) [*]* [*]* [*]* [*]* [*]*
5 26+10*V(2) 2+2*V(2) 01 112+V(2) (11)C> 21 111+V(1) [*]* [*]* [*]* [*]* [*]*
6 33+10*V(2) -1+2*V(2) 01 112+V(2) <B(22) 22 111+V(1) [*]* [*]* [*]* [*]* [*]*
7 37+12*V(2) -5 01 <B(22) 223+V(2) 111+V(1) [*]* [*]* [*]* [*]* [*]*
8 44+12*V(2) -2 11 (10)D> 223+V(2) 111+V(1) [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 9 (PA)
98199 603685564 -24576 11 (10)D> 223 112 22 21 1112284 22 20
== Executing PA-CTR 9, V(1)=0, V(2)=2, repcount=1, factor=2/1
98207 603685632 -24578 11 (10)D> 225 11 22 21 1112284 22 20
98208 603685652 -24568 116 (10)D> 11 22 21 1112284 22 20
98209 603685657 -24571 116 <B(22) 21 22 21 1112284 22 20
98210 603685669 -24583 <B(22) 226 21 22 21 1112284 22 20
98211 603685674 -24580 01 (11)C> 226 21 22 21 1112284 22 20
98212 603685698 -24568 01 116 (11)C> 21 22 21 1112284 22 20
98213 603685705 -24571 01 116 <B(22) 222 21 1112284 22 20
98214 603685717 -24583 01 <B(22) 228 21 1112284 22 20
98215 603685724 -24580 11 (10)D> 228 21 1112284 22 20
98216 603685756 -24564 119 (10)D> 21 1112284 22 20
98217 603685760 -24562 1110 (12)A> 1112284 22 20
98218 603685763 -24565 1110 <D(10) 1112284 22 20
98219 603685765 -24567 119 <D(11) 10 1112284 22 20
98220 603685783 -24585 <D(11) 119 10 1112284 22 20
98221 603685795 -24587 <A(12) 22 119 10 1112284 22 20
98222 603685804 -24584 11 (10)D> 22 119 10 1112284 22 20
>> Try to prove a PPA-CTR with 4 Vars...
0 0 0 111+V(1) (10)D> 221+V(4) 11 221+V(3) 21 111+V(2) [*]* [*]*
1 4+4*V(4) 2+2*V(4) 112+V(1)+V(4) (10)D> 11 221+V(3) 21 111+V(2) [*]* [*]*
2 9+4*V(4) -1+2*V(4) 112+V(1)+V(4) <B(22) 21 221+V(3) 21 111+V(2) [*]* [*]*
3 13+2*V(1)+6*V(4) -5+-2*V(1) <B(22) 222+V(1)+V(4) 21 221+V(3) 21 111+V(2) [*]* [*]*
4 18+2*V(1)+6*V(4) -2+-2*V(1) 01 (11)C> 222+V(1)+V(4) 21 221+V(3) 21 111+V(2) [*]* [*]*
5 26+6*V(1)+10*V(4) 2+2*V(4) 01 112+V(1)+V(4) (11)C> 21 221+V(3) 21 111+V(2) [*]* [*]*
6 33+6*V(1)+10*V(4) -1+2*V(4) 01 112+V(1)+V(4) <B(22) 222+V(3) 21 111+V(2) [*]* [*]*
7 37+8*V(1)+12*V(4) -5+-2*V(1) 01 <B(22) 224+V(1)+V(3)+V(4) 21 111+V(2) [*]* [*]*
8 44+8*V(1)+12*V(4) -2+-2*V(1) 11 (10)D> 224+V(1)+V(3)+V(4) 21 111+V(2) [*]* [*]*
9 60+12*V(1)+4*V(3)+16*V(4) 6+2*V(3)+2*V(4) 115+V(1)+V(3)+V(4) (10)D> 21 111+V(2) [*]* [*]*
10 64+12*V(1)+4*V(3)+16*V(4) 8+2*V(3)+2*V(4) 116+V(1)+V(3)+V(4) (12)A> 111+V(2) [*]* [*]*
11 67+12*V(1)+4*V(3)+16*V(4) 5+2*V(3)+2*V(4) 116+V(1)+V(3)+V(4) <D(10) 111+V(2) [*]* [*]*
12 69+12*V(1)+4*V(3)+16*V(4) 3+2*V(3)+2*V(4) 115+V(1)+V(3)+V(4) <D(11) 10 111+V(2) [*]* [*]*
13 79+14*V(1)+6*V(3)+18*V(4) -7+-2*V(1) <D(11) 115+V(1)+V(3)+V(4) 10 111+V(2) [*]* [*]*
14 91+14*V(1)+6*V(3)+18*V(4) -9+-2*V(1) <A(12) 22 115+V(1)+V(3)+V(4) 10 111+V(2) [*]* [*]*
15 100+14*V(1)+6*V(3)+18*V(4) -6+-2*V(1) 11 (10)D> 22 115+V(1)+V(3)+V(4) 10 111+V(2) [*]* [*]*
<< Success! ==> defined new CTR 10 (PPA)
98222 603685804 -24584 11 (10)D> 22 119 10 1112284 22 20
== Executing PA-CTR 2, V(1)=7, V(2)=0, repcount=8, factor=2/1
98286 603686828 -24600 11 (10)D> 2217 11 10 1112284 22 20
98287 603686896 -24566 1118 (10)D> 11 10 1112284 22 20
98288 603686901 -24569 1118 <B(22) 21 10 1112284 22 20
98289 603686937 -24605 <B(22) 2218 21 10 1112284 22 20
98290 603686942 -24602 01 (11)C> 2218 21 10 1112284 22 20
98291 603687014 -24566 01 1118 (11)C> 21 10 1112284 22 20
98292 603687021 -24569 01 1118 <B(22) 22 10 1112284 22 20
98293 603687057 -24605 01 <B(22) 2219 10 1112284 22 20
98294 603687064 -24602 11 (10)D> 2219 10 1112284 22 20
98295 603687140 -24564 1120 (10)D> 10 1112284 22 20
98296 603687145 -24567 1120 <B(22) 20 1112284 22 20
98297 603687185 -24607 <B(22) 2220 20 1112284 22 20
98298 603687190 -24604 01 (11)C> 2220 20 1112284 22 20
98299 603687270 -24564 01 1120 (11)C> 20 1112284 22 20
98300 603687272 -24562 01 1121 (01)C> 1112284 22 20
98301 603687283 -24565 01 1121 <A(12) 22 1112283 22 20
98302 603687285 -24567 01 1120 <A(11) 12 22 1112283 22 20
98303 603687325 -24607 01 <A(11) 1120 12 22 1112283 22 20
98304 603687331 -24609 <D(10) 1121 12 22 1112283 22 20
98305 603687334 -24606 01 (21)B> 1121 12 22 1112283 22 20
98306 603687337 -24609 01 <D(22) 21 1120 12 22 1112283 22 20
98307 603687341 -24611 <B(22) 22 21 1120 12 22 1112283 22 20
98308 603687346 -24608 01 (11)C> 22 21 1120 12 22 1112283 22 20
98309 603687350 -24606 01 11 (11)C> 21 1120 12 22 1112283 22 20
98310 603687357 -24609 01 11 <B(22) 22 1120 12 22 1112283 22 20
98311 603687359 -24611 01 <B(22) 222 1120 12 22 1112283 22 20
98312 603687366 -24608 11 (10)D> 222 1120 12 22 1112283 22 20
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 111+V(1) (10)D> 221+V(3) 11 10 112+V(2) [*]* [*]*
1 4+4*V(3) 2+2*V(3) 112+V(1)+V(3) (10)D> 11 10 112+V(2) [*]* [*]*
2 9+4*V(3) -1+2*V(3) 112+V(1)+V(3) <B(22) 21 10 112+V(2) [*]* [*]*
3 13+2*V(1)+6*V(3) -5+-2*V(1) <B(22) 222+V(1)+V(3) 21 10 112+V(2) [*]* [*]*
4 18+2*V(1)+6*V(3) -2+-2*V(1) 01 (11)C> 222+V(1)+V(3) 21 10 112+V(2) [*]* [*]*
5 26+6*V(1)+10*V(3) 2+2*V(3) 01 112+V(1)+V(3) (11)C> 21 10 112+V(2) [*]* [*]*
6 33+6*V(1)+10*V(3) -1+2*V(3) 01 112+V(1)+V(3) <B(22) 22 10 112+V(2) [*]* [*]*
7 37+8*V(1)+12*V(3) -5+-2*V(1) 01 <B(22) 223+V(1)+V(3) 10 112+V(2) [*]* [*]*
8 44+8*V(1)+12*V(3) -2+-2*V(1) 11 (10)D> 223+V(1)+V(3) 10 112+V(2) [*]* [*]*
9 56+12*V(1)+16*V(3) 4+2*V(3) 114+V(1)+V(3) (10)D> 10 112+V(2) [*]* [*]*
10 61+12*V(1)+16*V(3) 1+2*V(3) 114+V(1)+V(3) <B(22) 20 112+V(2) [*]* [*]*
11 69+14*V(1)+18*V(3) -7+-2*V(1) <B(22) 224+V(1)+V(3) 20 112+V(2) [*]* [*]*
12 74+14*V(1)+18*V(3) -4+-2*V(1) 01 (11)C> 224+V(1)+V(3) 20 112+V(2) [*]* [*]*
13 90+18*V(1)+22*V(3) 4+2*V(3) 01 114+V(1)+V(3) (11)C> 20 112+V(2) [*]* [*]*
14 92+18*V(1)+22*V(3) 6+2*V(3) 01 115+V(1)+V(3) (01)C> 112+V(2) [*]* [*]*
15 103+18*V(1)+22*V(3) 3+2*V(3) 01 115+V(1)+V(3) <A(12) 22 111+V(2) [*]* [*]*
16 105+18*V(1)+22*V(3) 1+2*V(3) 01 114+V(1)+V(3) <A(11) 12 22 111+V(2) [*]* [*]*
17 113+20*V(1)+24*V(3) -7+-2*V(1) 01 <A(11) 114+V(1)+V(3) 12 22 111+V(2) [*]* [*]*
18 119+20*V(1)+24*V(3) -9+-2*V(1) <D(10) 115+V(1)+V(3) 12 22 111+V(2) [*]* [*]*
19 122+20*V(1)+24*V(3) -6+-2*V(1) 01 (21)B> 115+V(1)+V(3) 12 22 111+V(2) [*]* [*]*
20 125+20*V(1)+24*V(3) -9+-2*V(1) 01 <D(22) 21 114+V(1)+V(3) 12 22 111+V(2) [*]* [*]*
21 129+20*V(1)+24*V(3) -11+-2*V(1) <B(22) 22 21 114+V(1)+V(3) 12 22 111+V(2) [*]* [*]*
22 134+20*V(1)+24*V(3) -8+-2*V(1) 01 (11)C> 22 21 114+V(1)+V(3) 12 22 111+V(2) [*]* [*]*
23 138+20*V(1)+24*V(3) -6+-2*V(1) 01 11 (11)C> 21 114+V(1)+V(3) 12 22 111+V(2) [*]* [*]*
24 145+20*V(1)+24*V(3) -9+-2*V(1) 01 11 <B(22) 22 114+V(1)+V(3) 12 22 111+V(2) [*]* [*]*
25 147+20*V(1)+24*V(3) -11+-2*V(1) 01 <B(22) 222 114+V(1)+V(3) 12 22 111+V(2) [*]* [*]*
26 154+20*V(1)+24*V(3) -8+-2*V(1) 11 (10)D> 222 114+V(1)+V(3) 12 22 111+V(2) [*]* [*]*
<< Success! ==> defined new CTR 11 (PPA)
98312 603687366 -24608 11 (10)D> 222 1120 12 22 1112283 22 20
== Executing PA-CTR 9, V(1)=18, V(2)=1, repcount=19, factor=2/1
98464 603692534 -24646 11 (10)D> 2240 11 12 22 1112283 22 20
98465 603692694 -24566 1141 (10)D> 11 12 22 1112283 22 20
98466 603692699 -24569 1141 <B(22) 21 12 22 1112283 22 20
98467 603692781 -24651 <B(22) 2241 21 12 22 1112283 22 20
98468 603692786 -24648 01 (11)C> 2241 21 12 22 1112283 22 20
98469 603692950 -24566 01 1141 (11)C> 21 12 22 1112283 22 20
98470 603692957 -24569 01 1141 <B(22) 22 12 22 1112283 22 20
98471 603693039 -24651 01 <B(22) 2242 12 22 1112283 22 20
98472 603693046 -24648 11 (10)D> 2242 12 22 1112283 22 20
98473 603693214 -24564 1143 (10)D> 12 22 1112283 22 20
98474 603693219 -24567 1143 <B(22) 222 1112283 22 20
98475 603693305 -24653 <B(22) 2245 1112283 22 20
98476 603693310 -24650 01 (11)C> 2245 1112283 22 20
98477 603693490 -24560 01 1145 (11)C> 1112283 22 20
98478 603693495 -24563 01 1145 <A(11) 01 1112282 22 20
98479 603693585 -24653 01 <A(11) 1145 01 1112282 22 20
98480 603693591 -24655 <D(10) 1146 01 1112282 22 20
98481 603693594 -24652 01 (21)B> 1146 01 1112282 22 20
98482 603693597 -24655 01 <D(22) 21 1145 01 1112282 22 20
98483 603693601 -24657 <B(22) 22 21 1145 01 1112282 22 20
98484 603693606 -24654 01 (11)C> 22 21 1145 01 1112282 22 20
98485 603693610 -24652 01 11 (11)C> 21 1145 01 1112282 22 20
98486 603693617 -24655 01 11 <B(22) 22 1145 01 1112282 22 20
98487 603693619 -24657 01 <B(22) 222 1145 01 1112282 22 20
98488 603693626 -24654 11 (10)D> 222 1145 01 1112282 22 20
>> Try to prove a PPA-CTR with 4 Vars...
0 0 0 111+V(1) (10)D> 221+V(4) 11 12 221+V(3) 112+V(2) [*]* [*]*
1 4+4*V(4) 2+2*V(4) 112+V(1)+V(4) (10)D> 11 12 221+V(3) 112+V(2) [*]* [*]*
2 9+4*V(4) -1+2*V(4) 112+V(1)+V(4) <B(22) 21 12 221+V(3) 112+V(2) [*]* [*]*
3 13+2*V(1)+6*V(4) -5+-2*V(1) <B(22) 222+V(1)+V(4) 21 12 221+V(3) 112+V(2) [*]* [*]*
4 18+2*V(1)+6*V(4) -2+-2*V(1) 01 (11)C> 222+V(1)+V(4) 21 12 221+V(3) 112+V(2) [*]* [*]*
5 26+6*V(1)+10*V(4) 2+2*V(4) 01 112+V(1)+V(4) (11)C> 21 12 221+V(3) 112+V(2) [*]* [*]*
6 33+6*V(1)+10*V(4) -1+2*V(4) 01 112+V(1)+V(4) <B(22) 22 12 221+V(3) 112+V(2) [*]* [*]*
7 37+8*V(1)+12*V(4) -5+-2*V(1) 01 <B(22) 223+V(1)+V(4) 12 221+V(3) 112+V(2) [*]* [*]*
8 44+8*V(1)+12*V(4) -2+-2*V(1) 11 (10)D> 223+V(1)+V(4) 12 221+V(3) 112+V(2) [*]* [*]*
9 56+12*V(1)+16*V(4) 4+2*V(4) 114+V(1)+V(4) (10)D> 12 221+V(3) 112+V(2) [*]* [*]*
10 61+12*V(1)+16*V(4) 1+2*V(4) 114+V(1)+V(4) <B(22) 222+V(3) 112+V(2) [*]* [*]*
11 69+14*V(1)+18*V(4) -7+-2*V(1) <B(22) 226+V(1)+V(3)+V(4) 112+V(2) [*]* [*]*
12 74+14*V(1)+18*V(4) -4+-2*V(1) 01 (11)C> 226+V(1)+V(3)+V(4) 112+V(2) [*]* [*]*
13 98+18*V(1)+4*V(3)+22*V(4) 8+2*V(3)+2*V(4) 01 116+V(1)+V(3)+V(4) (11)C> 112+V(2) [*]* [*]*
14 103+18*V(1)+4*V(3)+22*V(4) 5+2*V(3)+2*V(4) 01 116+V(1)+V(3)+V(4) <A(11) 01 111+V(2) [*]* [*]*
15 115+20*V(1)+6*V(3)+24*V(4) -7+-2*V(1) 01 <A(11) 116+V(1)+V(3)+V(4) 01 111+V(2) [*]* [*]*
16 121+20*V(1)+6*V(3)+24*V(4) -9+-2*V(1) <D(10) 117+V(1)+V(3)+V(4) 01 111+V(2) [*]* [*]*
17 124+20*V(1)+6*V(3)+24*V(4) -6+-2*V(1) 01 (21)B> 117+V(1)+V(3)+V(4) 01 111+V(2) [*]* [*]*
18 127+20*V(1)+6*V(3)+24*V(4) -9+-2*V(1) 01 <D(22) 21 116+V(1)+V(3)+V(4) 01 111+V(2) [*]* [*]*
19 131+20*V(1)+6*V(3)+24*V(4) -11+-2*V(1) <B(22) 22 21 116+V(1)+V(3)+V(4) 01 111+V(2) [*]* [*]*
20 136+20*V(1)+6*V(3)+24*V(4) -8+-2*V(1) 01 (11)C> 22 21 116+V(1)+V(3)+V(4) 01 111+V(2) [*]* [*]*
21 140+20*V(1)+6*V(3)+24*V(4) -6+-2*V(1) 01 11 (11)C> 21 116+V(1)+V(3)+V(4) 01 111+V(2) [*]* [*]*
22 147+20*V(1)+6*V(3)+24*V(4) -9+-2*V(1) 01 11 <B(22) 22 116+V(1)+V(3)+V(4) 01 111+V(2) [*]* [*]*
23 149+20*V(1)+6*V(3)+24*V(4) -11+-2*V(1) 01 <B(22) 222 116+V(1)+V(3)+V(4) 01 111+V(2) [*]* [*]*
24 156+20*V(1)+6*V(3)+24*V(4) -8+-2*V(1) 11 (10)D> 222 116+V(1)+V(3)+V(4) 01 111+V(2) [*]* [*]*
<< Success! ==> defined new CTR 12 (PPA)
98488 603693626 -24654 11 (10)D> 222 1145 01 1112282 22 20
== Executing PA-CTR 2, V(1)=43, V(2)=1, repcount=44, factor=2/1
98840 603718794 -24742 11 (10)D> 2290 11 01 1112282 22 20
98841 603719154 -24562 1191 (10)D> 11 01 1112282 22 20
98842 603719159 -24565 1191 <B(22) 21 01 1112282 22 20
98843 603719341 -24747 <B(22) 2291 21 01 1112282 22 20
98844 603719346 -24744 01 (11)C> 2291 21 01 1112282 22 20
98845 603719710 -24562 01 1191 (11)C> 21 01 1112282 22 20
98846 603719717 -24565 01 1191 <B(22) 22 01 1112282 22 20
98847 603719899 -24747 01 <B(22) 2292 01 1112282 22 20
98848 603719906 -24744 11 (10)D> 2292 01 1112282 22 20
98849 603720274 -24560 1193 (10)D> 01 1112282 22 20
98850 603720276 -24558 1193 10 (12)A> 1112282 22 20
98851 603720279 -24561 1193 10 <D(10) 1112282 22 20
98852 603720282 -24558 1194 (21)B> 1112282 22 20
98853 603720285 -24561 1194 <D(22) 21 1112281 22 20
98854 603720287 -24563 1193 <D(11) 22 21 1112281 22 20
98855 603720473 -24749 <D(11) 1193 22 21 1112281 22 20
98856 603720485 -24751 <A(12) 22 1193 22 21 1112281 22 20
98857 603720494 -24748 11 (10)D> 22 1193 22 21 1112281 22 20
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 111+V(1) (10)D> 221+V(3) 11 01 112+V(2) [*]* [*]*
1 4+4*V(3) 2+2*V(3) 112+V(1)+V(3) (10)D> 11 01 112+V(2) [*]* [*]*
2 9+4*V(3) -1+2*V(3) 112+V(1)+V(3) <B(22) 21 01 112+V(2) [*]* [*]*
3 13+2*V(1)+6*V(3) -5+-2*V(1) <B(22) 222+V(1)+V(3) 21 01 112+V(2) [*]* [*]*
4 18+2*V(1)+6*V(3) -2+-2*V(1) 01 (11)C> 222+V(1)+V(3) 21 01 112+V(2) [*]* [*]*
5 26+6*V(1)+10*V(3) 2+2*V(3) 01 112+V(1)+V(3) (11)C> 21 01 112+V(2) [*]* [*]*
6 33+6*V(1)+10*V(3) -1+2*V(3) 01 112+V(1)+V(3) <B(22) 22 01 112+V(2) [*]* [*]*
7 37+8*V(1)+12*V(3) -5+-2*V(1) 01 <B(22) 223+V(1)+V(3) 01 112+V(2) [*]* [*]*
8 44+8*V(1)+12*V(3) -2+-2*V(1) 11 (10)D> 223+V(1)+V(3) 01 112+V(2) [*]* [*]*
9 56+12*V(1)+16*V(3) 4+2*V(3) 114+V(1)+V(3) (10)D> 01 112+V(2) [*]* [*]*
10 58+12*V(1)+16*V(3) 6+2*V(3) 114+V(1)+V(3) 10 (12)A> 112+V(2) [*]* [*]*
11 61+12*V(1)+16*V(3) 3+2*V(3) 114+V(1)+V(3) 10 <D(10) 112+V(2) [*]* [*]*
12 64+12*V(1)+16*V(3) 6+2*V(3) 115+V(1)+V(3) (21)B> 112+V(2) [*]* [*]*
13 67+12*V(1)+16*V(3) 3+2*V(3) 115+V(1)+V(3) <D(22) 21 111+V(2) [*]* [*]*
14 69+12*V(1)+16*V(3) 1+2*V(3) 114+V(1)+V(3) <D(11) 22 21 111+V(2) [*]* [*]*
15 77+14*V(1)+18*V(3) -7+-2*V(1) <D(11) 114+V(1)+V(3) 22 21 111+V(2) [*]* [*]*
16 89+14*V(1)+18*V(3) -9+-2*V(1) <A(12) 22 114+V(1)+V(3) 22 21 111+V(2) [*]* [*]*
17 98+14*V(1)+18*V(3) -6+-2*V(1) 11 (10)D> 22 114+V(1)+V(3) 22 21 111+V(2) [*]* [*]*
<< Success! ==> defined new CTR 13 (PPA)
98857 603720494 -24748 11 (10)D> 22 1193 22 21 1112281 22 20
== Executing PA-CTR 9, V(1)=91, V(2)=0, repcount=92, factor=2/1
99593 603825006 -24932 11 (10)D> 22185 11 22 21 1112281 22 20
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=12280, V(3)=0, V(4)=184
99608 603828418 -24938 11 (10)D> 22 11189 10 1112281 22 20
== Executing PA-CTR 2, V(1)=187, V(2)=0, repcount=188, factor=2/1
101112 604258562 -25314 11 (10)D> 22377 11 10 1112281 22 20
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=12279, V(3)=376
101138 604267740 -25322 11 (10)D> 222 11380 12 22 1112280 22 20
== Executing PA-CTR 9, V(1)=378, V(2)=1, repcount=379, factor=2/1
104170 606008108 -26080 11 (10)D> 22760 11 12 22 1112280 22 20
== Executing PPA-CTR 12 (once), V(1)=0, V(2)=12278, V(3)=0, V(4)=759
104194 606026480 -26088 11 (10)D> 222 11765 01 1112279 22 20
== Executing PA-CTR 2, V(1)=763, V(2)=1, repcount=764, factor=2/1
110306 613064448 -27616 11 (10)D> 221530 11 01 1112279 22 20
== Executing PPA-CTR 13 (once), V(1)=0, V(2)=12277, V(3)=1529
110323 613092068 -27622 11 (10)D> 22 111533 22 21 1112278 22 20
== Executing PA-CTR 9, V(1)=1531, V(2)=0, repcount=1532, factor=2/1
122579 641305380 -30686 11 (10)D> 223065 11 22 21 1112278 22 20
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=12277, V(3)=0, V(4)=3064
122594 641360632 -30692 11 (10)D> 22 113069 10 1112278 22 20
== Executing PA-CTR 2, V(1)=3067, V(2)=0, repcount=3068, factor=2/1
147138 754410296 -36828 11 (10)D> 226137 11 10 1112278 22 20
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=12276, V(3)=6136
147164 754557714 -36836 11 (10)D> 222 116140 12 22 1112277 22 20
== Executing PA-CTR 9, V(1)=6138, V(2)=1, repcount=6139, factor=2/1
196276 1207075682 -49114 11 (10)D> 2212280 11 12 22 1112277 22 20
== Executing PPA-CTR 12 (once), V(1)=0, V(2)=12275, V(3)=0, V(4)=12279
196300 1207370534 -49122 11 (10)D> 222 1112285 01 1112276 22 20
== Executing PA-CTR 2, V(1)=12283, V(2)=1, repcount=12284, factor=2/1
294572 3018670902 -73690 11 (10)D> 2224570 11 01 1112276 22 20
== Executing PPA-CTR 13 (once), V(1)=0, V(2)=12274, V(3)=24569
294589 3019113242 -73696 11 (10)D> 22 1124573 22 21 1112275 22 20
== Executing PA-CTR 9, V(1)=24571, V(2)=0, repcount=24572, factor=2/1
491165 10265297754 -122840 11 (10)D> 2249145 11 22 21 1112275 22 20
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=12274, V(3)=0, V(4)=49144
491180 10266182446 -122846 11 (10)D> 22 1149149 10 1112275 22 20
== Executing PA-CTR 2, V(1)=49147, V(2)=0, repcount=49148, factor=2/1
884364 39254066030 -221142 11 (10)D> 2298297 11 10 1112275 22 20
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=12273, V(3)=98296
884390 39256425288 -221150 11 (10)D> 222 1198300 12 22 1112274 22 20
== Executing PA-CTR 9, V(1)=98298, V(2)=1, repcount=98299, factor=2/1
1670782 155213071256 -417748 11 (10)D> 22196600 11 12 22 1112274 22 20
== Executing PPA-CTR 12 (once), V(1)=0, V(2)=12272, V(3)=0, V(4)=196599
1670806 155217789788 -417756 11 (10)D> 222 11196605 01 1112273 22 20
== Executing PA-CTR 2, V(1)=196603, V(2)=1, repcount=196604, factor=2/1
3243638 619064034156 -810964 11 (10)D> 22393210 11 01 1112273 22 20
== Executing PPA-CTR 13 (once), V(1)=0, V(2)=12271, V(3)=393209
3243655 619071112016 -810970 11 (10)D> 22 11393213 22 21 1112272 22 20
== Executing PA-CTR 9, V(1)=393211, V(2)=0, repcount=393212, factor=2/1
6389351 2474471818128 -1597394 11 (10)D> 22786425 11 22 21 1112272 22 20
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=12271, V(3)=0, V(4)=786424
6389366 2474485973860 -1597400 11 (10)D> 22 11786429 10 1112272 22 20
== Executing PA-CTR 2, V(1)=786427, V(2)=0, repcount=786428, factor=2/1
12680790 9896139129764 -3170256 11 (10)D> 221572857 11 10 1112272 22 20
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=12270, V(3)=1572856
12680816 9896176878462 -3170264 11 (10)D> 222 111572860 12 22 1112271 22 20
== Executing PA-CTR 9, V(1)=1572858, V(2)=1, repcount=1572859, factor=2/1
25263688 39582871290830 -6315982 11 (10)D> 223145720 11 12 22 1112271 22 20
== Executing PPA-CTR 12 (once), V(1)=0, V(2)=12269, V(3)=0, V(4)=3145719
25263712 39582946788242 -6315990 11 (10)D> 222 113145725 01 1112270 22 20
== Executing PA-CTR 2, V(1)=3145723, V(2)=1, repcount=3145724, factor=2/1
50429504 158330039010210 -12607438 11 (10)D> 226291450 11 01 1112270 22 20
== Executing PPA-CTR 13 (once), V(1)=0, V(2)=12268, V(3)=6291449
50429521 158330152256390 -12607444 11 (10)D> 22 116291453 22 21 1112269 22 20
== Executing PA-CTR 9, V(1)=6291451, V(2)=0, repcount=6291452, factor=2/1
100761137 633318772802502 -25190348 11 (10)D> 2212582905 11 22 21 1112269 22 20
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=12268, V(3)=0, V(4)=12582904
100761152 633318999294874 -25190354 11 (10)D> 22 1112582909 10 1112269 22 20
== Executing PA-CTR 2, V(1)=12582907, V(2)=0, repcount=12582908, factor=2/1
201424416 2533274286785498 -50356170 11 (10)D> 2225165817 11 10 1112269 22 20
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=12267, V(3)=25165816
201424442 2533274890765236 -50356178 11 (10)D> 222 1125165820 12 22 1112268 22 20
== Executing PA-CTR 9, V(1)=25165818, V(2)=1, repcount=25165819, factor=2/1
402750994 10133097349350404 -100687816 11 (10)D> 2250331640 11 12 22 1112268 22 20
== Executing PPA-CTR 12 (once), V(1)=0, V(2)=12266, V(3)=0, V(4)=50331639
402751018 10133098557309896 -100687824 11 (10)D> 222 1150331645 01 1112267 22 20
== Executing PA-CTR 2, V(1)=50331643, V(2)=1, repcount=50331644, factor=2/1
805404170 40532393424815064 -201351112 11 (10)D> 22100663290 11 01 1112267 22 20
== Executing PPA-CTR 13 (once), V(1)=0, V(2)=12265, V(3)=100663289
805404187 40532395236754364 -201351118 11 (10)D> 22 11100663293 22 21 1112266 22 20
== Executing PA-CTR 9, V(1)=100663291, V(2)=0, repcount=100663292, factor=2/1
1610710523 1621295[4]3306876 -402677702 11 (10)D> 22201326585 11 22 21 1112266 22 20
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=12265, V(3)=0, V(4)=201326584
1610710538 1621295[4]7185488 -402677708 11 (10)D> 22 11201326589 10 1112266 22 20
== Executing PA-CTR 2, V(1)=201326587, V(2)=0, repcount=201326588, factor=2/1
3221323242 6485183[4]8297232 -805330884 11 (10)D> 22402653177 11 10 1112266 22 20
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=12264, V(3)=402653176
3221323268 6485183[4]1973610 -805330892 11 (10)D> 222 11402653180 12 22 1112265 22 20
== Executing PA-CTR 9, V(1)=402653178, V(2)=1, repcount=402653179, factor=2/1
6442548700 2594073[5]4385978 -1610637250 11 (10)D> 22805306360 11 12 22 1112265 22 20
== Executing PPA-CTR 12 (once), V(1)=0, V(2)=12263, V(3)=0, V(4)=805306359
6442548724 2594073[5]1738750 -1610637258 11 (10)D> 222 11805306365 01 1112264 22 20
== Executing PA-CTR 2, V(1)=805306363, V(2)=1, repcount=805306364, factor=2/1
12884999636 1037629[6]2024718 -3221249986 11 (10)D> 221610612730 11 01 1112264 22 20
== Executing PPA-CTR 13 (once), V(1)=0, V(2)=12262, V(3)=1610612729
12884999653 1037629[6]3053938 -3221249992 11 (10)D> 22 111610612733 22 21 1112263 22 20
== Executing PA-CTR 9, V(1)=1610612731, V(2)=0, repcount=1610612732, factor=2/1
25769901509 4150517[6]8707250 -6442475456 11 (10)D> 223221225465 11 22 21 1112263 22 20
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=12262, V(3)=0, V(4)=3221225464
25769901524 4150517[6]0765702 -6442475462 11 (10)D> 22 113221225469 10 1112263 22 20
== Executing PA-CTR 2, V(1)=3221225467, V(2)=0, repcount=3221225468, factor=2/1
51539705268 1660206[7]1808966 -12884926398 11 (10)D> 226442450937 11 10 1112263 22 20
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=12261, V(3)=6442450936
51539705294 1660206[7]0631584 -12884926406 11 (10)D> 222 116442450940 12 22 1112262 22 20
== Executing PA-CTR 9, V(1)=6442450938, V(2)=1, repcount=6442450939, factor=2/1
103079312806 6640827[7]2253552 -25769828284 11 (10)D> 2212884901880 11 12 22 1112262 22 20
== Executing PPA-CTR 12 (once), V(1)=0, V(2)=12260, V(3)=0, V(4)=12884901879
103079312830 6640827[7]9898804 -25769828292 11 (10)D> 222 1112884901885 01 1112261 22 20
== Executing PA-CTR 2, V(1)=12884901883, V(2)=1, repcount=12884901884, factor=2/1
206158527902 2656331[8]6575172 -51539632060 11 (10)D> 2225769803770 11 01 1112261 22 20
== Executing PPA-CTR 13 (once), V(1)=0, V(2)=12259, V(3)=25769803769
206158527919 2656331[8]3043112 -51539632066 11 (10)D> 22 1125769803773 22 21 1112260 22 20
== Executing PA-CTR 9, V(1)=25769803771, V(2)=0, repcount=25769803772, factor=2/1
412316958095 1062532[9]1899624 -103079239610 11 (10)D> 2251539607545 11 22 21 1112260 22 20
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=12259, V(3)=0, V(4)=51539607544
412316958110 1062532[9]4835516 -103079239616 11 (10)D> 22 1151539607549 10 1112260 22 20
== Executing PA-CTR 2, V(1)=51539607547, V(2)=0, repcount=51539607548, factor=2/1
824633818494 4250129[9]5144700 -206158454712 11 (10)D> 22103079215097 11 10 1112260 22 20
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=12258, V(3)=103079215096
824633818520 4250129[9]6307158 -206158454720 11 (10)D> 222 11103079215100 12 22 1112259 22 20
== Executing PA-CTR 9, V(1)=103079215098, V(2)=1, repcount=103079215099, factor=2/1
1649267539312 1700051[10]6729126 -412316884918 11 (10)D> 22206158430200 11 12 22 1112259 22 20
== Executing PPA-CTR 12 (once), V(1)=0, V(2)=12257, V(3)=0, V(4)=206158430199
1649267539336 1700051[10]9054058 -412316884926 11 (10)D> 222 11206158430205 01 1112258 22 20
== Executing PA-CTR 2, V(1)=206158430203, V(2)=1, repcount=206158430204, factor=2/1
3298534980968 6800207[10]3762426 -824633745334 11 (10)D> 22412316860410 11 01 1112258 22 20
== Executing PPA-CTR 13 (once), V(1)=0, V(2)=12256, V(3)=412316860409
3298534980985 6800207[10]7249886 -824633745340 11 (10)D> 22 11412316860413 22 21 1112257 22 20
== Executing PA-CTR 9, V(1)=412316860411, V(2)=0, repcount=412316860412, factor=2/1
6597069864281 2720083[11]0499998 -1649267466164 11 (10)D> 22824633720825 11 22 21 1112257 22 20
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=12256, V(3)=0, V(4)=824633720824
6597069864296 2720083[11]7474930 -1649267466170 11 (10)D> 22 11824633720829 10 1112257 22 20
== Executing PA-CTR 2, V(1)=824633720827, V(2)=0, repcount=824633720828, factor=2/1
13194139630920 1088033[12]8608434 -3298534907826 11 (10)D> 221649267441657 11 10 1112257 22 20
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=12255, V(3)=1649267441656
13194139630946 1088033[12]7208332 -3298534907834 11 (10)D> 222 111649267441660 12 22 1112256 22 20
== Executing PA-CTR 9, V(1)=1649267441658, V(2)=1, repcount=1649267441659, factor=2/1
26388279164218 4352132[12]8708700 -6597069791152 11 (10)D> 223298534883320 11 12 22 1112256 22 20
== Executing PPA-CTR 12 (once), V(1)=0, V(2)=12254, V(3)=0, V(4)=3298534883319
26388279164242 4352132[12]5908512 -6597069791160 11 (10)D> 222 113298534883325 01 1112255 22 20
== Executing PA-CTR 2, V(1)=3298534883323, V(2)=1, repcount=3298534883324, factor=2/1
52776558230834 1740853[13]0242480 -13194139557808 11 (10)D> 226597069766650 11 01 1112255 22 20
== Executing PPA-CTR 13 (once), V(1)=0, V(2)=12253, V(3)=6597069766649
52776558230851 1740853[13]6042260 -13194139557814 11 (10)D> 22 116597069766653 22 21 1112254 22 20
== Executing PA-CTR 9, V(1)=6597069766651, V(2)=0, repcount=6597069766652, factor=2/1
105553116364067 6963412[13]4044372 -26388279091118 11 (10)D> 2213194139533305 11 22 21 1112254 22 20
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=12253, V(3)=0, V(4)=13194139533304
105553116364082 6963412[13]5643944 -26388279091124 11 (10)D> 22 1113194139533309 10 1112254 22 20
== Executing PA-CTR 2, V(1)=13194139533307, V(2)=0, repcount=13194139533308, factor=2/1
211106232630546 2785365[14]7784168 -52776558157740 11 (10)D> 2226388279066617 11 10 1112254 22 20
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=12252, V(3)=26388279066616
211106232630572 2785365[14]5383106 -52776558157748 11 (10)D> 222 1126388279066620 12 22 1112253 22 20
== Executing PA-CTR 9, V(1)=26388279066618, V(2)=1, repcount=26388279066619, factor=2/1
422212465163524 1114146[15]5408274 -105553116290986 11 (10)D> 2252776558133240 11 12 22 1112253 22 20
== Executing PPA-CTR 12 (once), V(1)=0, V(2)=12251, V(3)=0, V(4)=52776558133239
422212465163548 1114146[15]0606166 -105553116290994 11 (10)D> 222 1152776558133245 01 1112252 22 20
== Executing PA-CTR 2, V(1)=52776558133243, V(2)=1, repcount=52776558133244, factor=2/1
844424930229500 4456584[15]4031334 -211106232557482 11 (10)D> 22105553116266490 11 01 1112252 22 20
== Executing PPA-CTR 13 (once), V(1)=0, V(2)=12250, V(3)=105553116266489
844424930229517 4456584[15]6828234 -211106232557488 11 (10)D> 22 11105553116266493 22 21 1112251 22 20
== Executing PA-CTR 9, V(1)=105553116266491, V(2)=0, repcount=105553116266492, factor=2/1
1688849860361453 1782633[16]1188746 -422212465090472 11 (10)D> 22211106232532985 11 22 21 1112251 22 20
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=12250, V(3)=0, V(4)=211106232532984
1688849860361468 1782633[16]6782558 -422212465090478 11 (10)D> 22 11211106232532989 10 1112251 22 20
== Executing PA-CTR 2, V(1)=211106232532987, V(2)=0, repcount=211106232532988, factor=2/1
3377699720625372 7130534[16]6335902 -844424930156454 11 (10)D> 22422212465065977 11 10 1112251 22 20
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=12249, V(3)=422212465065976
3377699720625398 7130534[16]7919480 -844424930156462 11 (10)D> 222 11422212465065980 12 22 1112250 22 20
== Executing PA-CTR 9, V(1)=422212465065978, V(2)=1, repcount=422212465065979, factor=2/1
6755399441153230 2852213[17]9563848 -1688849860288420 11 (10)D> 22844424930131960 11 12 22 1112250 22 20
== Executing PPA-CTR 12 (once), V(1)=0, V(2)=12248, V(3)=0, V(4)=844424930131959
6755399441153254 2852213[17]2731020 -1688849860288428 11 (10)D> 222 11844424930131965 01 1112249 22 20
== Executing PA-CTR 2, V(1)=844424930131963, V(2)=1, repcount=844424930131964, factor=2/1
13510798882208966 1140885[18]2504988 -3377699720552356 11 (10)D> 221688849860263930 11 01 1112249 22 20
== Executing PPA-CTR 13 (once), V(1)=0, V(2)=12247, V(3)=1688849860263929
13510798882208983 1140885[18]7255808 -3377699720552362 11 (10)D> 22 111688849860263933 22 21 1112248 22 20
== Executing PA-CTR 9, V(1)=1688849860263931, V(2)=0, repcount=1688849860263932, factor=2/1
27021597764320439 4563542[18]6909120 -6755399441080226 11 (10)D> 223377699720527865 11 22 21 1112248 22 20
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=12247, V(3)=0, V(4)=3377699720527864
27021597764320454 4563542[18]6410772 -6755399441080232 11 (10)D> 22 113377699720527869 10 1112248 22 20
== Executing PA-CTR 2, V(1)=3377699720527867, V(2)=0, repcount=3377699720527868, factor=2/1
54043195528543398 1825416[19]8807636 -135107[4]2135968 11 (10)D> 226755399441055737 11 10 1112248 22 20
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=12246, V(3)=6755399441055736
54043195528543424 1825416[19]4145454 -135107[4]2135976 11 (10)D> 222 116755399441055740 12 22 1112247 22 20
== Executing PA-CTR 9, V(1)=6755399441055738, V(2)=1, repcount=6755399441055739, factor=2/1
1080863[4]6989336 7301667[19]8631422 -270215[4]4247454 11 (10)D> 2213510798882111480 11 12 22 1112247 22 20
== Executing PPA-CTR 12 (once), V(1)=0, V(2)=12245, V(3)=0, V(4)=13510798882111479
1080863[4]6989360 7301667[19]9307074 -270215[4]4247462 11 (10)D> 222 1113510798882111485 01 1112246 22 20
== Executing PA-CTR 2, V(1)=13510798882111483, V(2)=1, repcount=13510798882111484, factor=2/1
2161727[4]3881232 2920666[20]8399442 -540431[4]8470430 11 (10)D> 2227021597764222970 11 01 1112246 22 20
== Executing PPA-CTR 13 (once), V(1)=0, V(2)=12244, V(3)=27021597764222969
2161727[4]3881249 2920666[20]4412982 -540431[4]8470436 11 (10)D> 22 1127021597764222973 22 21 1112245 22 20
== Executing PA-CTR 9, V(1)=27021597764222971, V(2)=0, repcount=27021597764222972, factor=2/1
4323455[4]7665025 1168266[21]9701494 -108086[5]6916380 11 (10)D> 2254043195528445945 11 22 21 1112245 22 20
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=12244, V(3)=0, V(4)=54043195528445944
4323455[4]7665040 1168266[21]1728586 -108086[5]6916386 11 (10)D> 22 1154043195528445949 10 1112245 22 20
== Executing PA-CTR 2, V(1)=54043195528445947, V(2)=0, repcount=54043195528445948, factor=2/1
8646911[4]5232624 4673067[21]3423370 -216172[5]3808282 11 (10)D> 221080863[4]6891897 11 10 1112245 22 20
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=12243, V(3)=1080863[4]6891896
8646911[4]5232650 4673067[21]8829028 -216172[5]3808290 11 (10)D> 222 111080863[4]6891900 12 22 1112244 22 20
== Executing PA-CTR 9, V(1)=1080863[4]6891898, V(2)=1, repcount=1080863[4]6891899, factor=2/1
1729382[5]0367842 1869226[22]3986996 -432345[5]7592088 11 (10)D> 222161727[4]3783800 11 12 22 1112244 22 20
== Executing PPA-CTR 12 (once), V(1)=0, V(2)=12242, V(3)=0, V(4)=2161727[4]3783799
1729382[5]0367866 1869226[22]4798328 -432345[5]7592096 11 (10)D> 222 112161727[4]3783805 01 1112243 22 20
== Executing PA-CTR 2, V(1)=2161727[4]3783803, V(2)=1, repcount=2161727[4]3783804, factor=2/1
3458764[5]0638298 7476907[22]3810696 -864691[5]5159704 11 (10)D> 224323455[4]7567610 11 01 1112243 22 20
== Executing PPA-CTR 13 (once), V(1)=0, V(2)=12241, V(3)=4323455[4]7567609
3458764[5]0638315 7476907[22]0027756 -864691[5]5159710 11 (10)D> 22 114323455[4]7567613 22 21 1112242 22 20
== Executing PA-CTR 9, V(1)=4323455[4]7567611, V(2)=0, repcount=4323455[4]7567612, factor=2/1
6917529[5]1179211 2990762[23]8781868 -172938[6]0294934 11 (10)D> 228646911[4]5135225 11 22 21 1112242 22 20
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=12241, V(3)=0, V(4)=8646911[4]5135224
6917529[5]1179226 2990762[23]1216000 -172938[6]0294940 11 (10)D> 22 118646911[4]5135229 10 1112242 22 20
== Executing PA-CTR 2, V(1)=8646911[4]5135227, V(2)=0, repcount=8646911[4]5135228, factor=2/1
1383505[6]2261050 1196305[24]4887104 -345876[6]0565396 11 (10)D> 221729382[5]0270457 11 10 1112242 22 20
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=12240, V(3)=1729382[5]0270456
1383505[6]2261076 1196305[24]1378202 -345876[6]0565404 11 (10)D> 222 111729382[5]0270460 12 22 1112241 22 20
== Executing PA-CTR 9, V(1)=1729382[5]0270458, V(2)=1, repcount=1729382[5]0270459, factor=2/1
2767011[6]4424748 4785220[24]0126570 -691752[6]1106322 11 (10)D> 223458764[5]0540920 11 12 22 1112241 22 20
== Executing PPA-CTR 12 (once), V(1)=0, V(2)=12239, V(3)=0, V(4)=3458764[5]0540919
2767011[6]4424772 4785220[24]3108782 -691752[6]1106330 11 (10)D> 222 113458764[5]0540925 01 1112240 22 20
== Executing PA-CTR 2, V(1)=3458764[5]0540923, V(2)=1, repcount=3458764[5]0540924, factor=2/1
5534023[6]8752164 1914088[25]2194750 -138350[7]2188178 11 (10)D> 226917529[5]1081850 11 01 1112240 22 20
== Executing PPA-CTR 13 (once), V(1)=0, V(2)=12238, V(3)=6917529[5]1081849
5534023[6]8752181 1914088[25]1668130 -138350[7]2188184 11 (10)D> 22 116917529[5]1081853 22 21 1112239 22 20
== Executing PA-CTR 9, V(1)=6917529[5]1081851, V(2)=0, repcount=6917529[5]1081852, factor=2/1
1106804[7]7406997 7656353[25]1286242 -276701[7]4351888 11 (10)D> 221383505[6]2163705 11 22 21 1112239 22 20
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=12238, V(3)=0, V(4)=1383505[6]2163704
1106804[7]7407012 7656353[25]0233014 -276701[7]4351894 11 (10)D> 22 111383505[6]2163709 10 1112239 22 20
== Executing PA-CTR 2, V(1)=1383505[6]2163707, V(2)=0, repcount=1383505[6]2163708, factor=2/1
2213609[7]4716676 3062541[26]7182838 -553402[7]8679310 11 (10)D> 222767011[6]4327417 11 10 1112239 22 20
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=12237, V(3)=2767011[6]4327416
2213609[7]4716702 3062541[26]1040976 -553402[7]8679318 11 (10)D> 222 112767011[6]4327420 12 22 1112238 22 20
== Executing PA-CTR 9, V(1)=2767011[6]4327418, V(2)=1, repcount=2767011[6]4327419, factor=2/1
4427218[7]9336054 1225016[27]3866144 -110680[8]7334156 11 (10)D> 225534023[6]8654840 11 12 22 1112238 22 20
== Executing PPA-CTR 12 (once), V(1)=0, V(2)=12236, V(3)=0, V(4)=5534023[6]8654839
4427218[7]9336078 1225016[27]1582436 -110680[8]7334164 11 (10)D> 222 115534023[6]8654845 01 1112237 22 20
== Executing PA-CTR 2, V(1)=5534023[6]8654843, V(2)=1, repcount=5534023[6]8654844, factor=2/1
8854437[7]8574830 4900066[27]8367604 -221360[8]4643852 11 (10)D> 221106804[7]7309690 11 01 1112237 22 20
== Executing PPA-CTR 13 (once), V(1)=0, V(2)=12235, V(3)=1106804[7]7309689
8854437[7]8574847 4900066[27]9942104 -221360[8]4643858 11 (10)D> 22 111106804[7]7309693 22 21 1112236 22 20
== Executing PA-CTR 9, V(1)=1106804[7]7309691, V(2)=0, repcount=1106804[7]7309692, factor=2/1
1770887[8]7052383 1960026[28]9470616 -442721[8]9263242 11 (10)D> 222213609[7]4619385 11 22 21 1112236 22 20
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=12235, V(3)=0, V(4)=2213609[7]4619384
1770887[8]7052398 1960026[28]2619628 -442721[8]9263248 11 (10)D> 22 112213609[7]4619389 10 1112236 22 20
== Executing PA-CTR 2, V(1)=2213609[7]4619387, V(2)=0, repcount=2213609[7]4619388, factor=2/1
3541774[8]4007502 7840105[28]6374572 -885443[8]8502024 11 (10)D> 224427218[7]9238777 11 10 1112236 22 20
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=12234, V(3)=4427218[7]9238776
3541774[8]4007528 7840105[28]8105350 -885443[8]8502032 11 (10)D> 222 114427218[7]9238780 12 22 1112235 22 20
== Executing PA-CTR 9, V(1)=4427218[7]9238778, V(2)=1, repcount=4427218[7]9238779, factor=2/1
7083549[8]7917760 3136042[29]3541718 -177088[9]6979590 11 (10)D> 228854437[7]8477560 11 12 22 1112235 22 20
== Executing PPA-CTR 12 (once), V(1)=0, V(2)=12233, V(3)=0, V(4)=8854437[7]8477559
7083549[8]7917784 3136042[29]7003290 -177088[9]6979598 11 (10)D> 222 118854437[7]8477565 01 1112234 22 20
== Executing PA-CTR 2, V(1)=8854437[7]8477563, V(2)=1, repcount=8854437[7]8477564, factor=2/1
1416709[9]5738296 1254416[30]6505258 -354177[9]3934726 11 (10)D> 221770887[8]6955130 11 01 1112234 22 20
== Executing PPA-CTR 13 (once), V(1)=0, V(2)=12232, V(3)=1770887[8]6955129
1416709[9]5738313 1254416[30]1697678 -354177[9]3934732 11 (10)D> 22 111770887[8]6955133 22 21 1112233 22 20
== Executing PA-CTR 9, V(1)=1770887[8]6955131, V(2)=0, repcount=1770887[8]6955132, factor=2/1
2833419[9]1379369 5017667[30]7910990 -708354[9]7844996 11 (10)D> 223541774[8]3910265 11 22 21 1112233 22 20
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=12232, V(3)=0, V(4)=3541774[8]3910264
2833419[9]1379384 5017667[30]8295842 -708354[9]7845002 11 (10)D> 22 113541774[8]3910269 10 1112233 22 20
== Executing PA-CTR 2, V(1)=3541774[8]3910267, V(2)=0, repcount=3541774[8]3910268, factor=2/1
5666839[9]2661528 2007067[31]3406306 -141670[10]5665538 11 (10)D> 227083549[8]7820537 11 10 1112233 22 20
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=12231, V(3)=7083549[8]7820536
5666839[9]2661554 2007067[31]1099324 -141670[10]5665546 11 (10)D> 222 117083549[8]7820540 12 22 1112232 22 20
== Executing PA-CTR 9, V(1)=7083549[8]7820538, V(2)=1, repcount=7083549[8]7820539, factor=2/1
1133367[10]5225866 8028268[31]8209292 -283341[10]1306624 11 (10)D> 221416709[9]5641080 11 12 22 1112232 22 20
== Executing PPA-CTR 12 (once), V(1)=0, V(2)=12230, V(3)=0, V(4)=1416709[9]5641079
1133367[10]5225890 8028268[31]3595344 -283341[10]1306632 11 (10)D> 222 111416709[9]5641085 01 1112231 22 20
== Executing PA-CTR 2, V(1)=1416709[9]5641083, V(2)=1, repcount=1416709[9]5641084, factor=2/1
2266735[10]0354562 3211307[32]6143712 -566683[10]2588800 11 (10)D> 222833419[9]1282170 11 01 1112231 22 20
== Executing PPA-CTR 13 (once), V(1)=0, V(2)=12229, V(3)=2833419[9]1282169
2266735[10]0354579 3211307[32]9222852 -566683[10]2588806 11 (10)D> 22 112833419[9]1282173 22 21 1112230 22 20
== Executing PA-CTR 9, V(1)=2833419[9]1282171, V(2)=0, repcount=2833419[9]1282172, factor=2/1
4533471[10]0611955 1284522[33]0703364 -113336[11]5153150 11 (10)D> 225666839[9]2564345 11 22 21 1112230 22 20
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=12229, V(3)=0, V(4)=5666839[9]2564344
4533471[10]0611970 1284522[33]6861656 -113336[11]5153156 11 (10)D> 22 115666839[9]2564349 10 1112230 22 20
== Executing PA-CTR 2, V(1)=5666839[9]2564347, V(2)=0, repcount=5666839[9]2564348, factor=2/1
9066943[10]1126754 5138091[33]6902040 -226673[11]0281852 11 (10)D> 221133367[10]5128697 11 10 1112230 22 20
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=12228, V(3)=1133367[10]5128696
9066943[10]1126780 5138091[33]9990898 -226673[11]0281860 11 (10)D> 222 111133367[10]5128700 12 22 1112229 22 20
== Executing PA-CTR 9, V(1)=1133367[10]5128698, V(2)=1, repcount=1133367[10]5128699, factor=2/1
1813388[11]2156372 2055236[34]6844866 -453347[11]0539258 11 (10)D> 222266735[10]0257400 11 12 22 1112229 22 20
== Executing PPA-CTR 12 (once), V(1)=0, V(2)=12227, V(3)=0, V(4)=2266735[10]0257399
1813388[11]2156396 2055236[34]3022598 -453347[11]0539266 11 (10)D> 222 112266735[10]0257405 01 1112228 22 20
== Executing PA-CTR 2, V(1)=2266735[10]0257403, V(2)=1, repcount=2266735[10]0257404, factor=2/1
3626777[11]4215628 8220946[34]6178966 -906694[11]1054074 11 (10)D> 224533471[10]0514810 11 01 1112228 22 20
== Executing PPA-CTR 13 (once), V(1)=0, V(2)=12226, V(3)=4533471[10]0514809
3626777[11]4215645 8220946[34]5445626 -906694[11]1054080 11 (10)D> 22 114533471[10]0514813 22 21 1112227 22 20
== Executing PA-CTR 9, V(1)=4533471[10]0514811, V(2)=0, repcount=4533471[10]0514812, factor=2/1
7253554[11]8334141 3288378[35]8663738 -181338[12]2083704 11 (10)D> 229066943[10]1029625 11 22 21 1112227 22 20
Lines: 500
Top steps: 499
Macro steps: 7253554917687775048334141
Basic steps: 3288378683994531565958252792448318933407448663738
Tape index: -1813388729421943762083704
nonzeros: 1813388729421943762083716
log10(nonzeros): 24.258
log10(steps ): 48.517
Some long numbers above are shortened: #(omitted digits) shown in "[]".
Input to awk program:
gohalt 1
nbs 3
T 4-state 3-symbol #g (T.J. & S. Ligocki)
: >8.9x10^4931 >7.9x10^9863
5T 1RB 1LD 1RH 1RC 2LB 2LD 1LC 2RA 0RD 1RC 1LA 0LA
L 12
M 500
pref sim
machv Lig43_g just simple
machv Lig43_g-r with repetitions reduced
machv Lig43_g-1 with tape symbol exponents
machv Lig43_g-m as 2-bck-macro machine
machv Lig43_g-a as 2-bck-macro machine with pure additive config-TRs
iam Lig43_g-a
mtype 2 0
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:14:14 CEST 2010
edate Tue Jul 6 22:14:17 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:14 CEST 2010