Comment: This TM produces >8.0x10^986 nonzeros in >3.7x10^1973 steps.
| State | on 0 |
on 1 |
on 2 |
on 0 | on 1 | on 2 | ||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Move | Goto | Move | Goto | Move | Goto | |||||||
| A | 1RB | 1RA | 0LB | 1 | right | B | 1 | right | A | 0 | left | B |
| B | 2LC | 1LB | 1RC | 2 | left | C | 1 | left | B | 1 | right | C |
| C | 0RD | 2LC | 1RA | 0 | right | D | 2 | left | C | 1 | right | A |
| D | 2RA | 1RH | 1RC | 2 | right | A | 1 | right | H | 1 | right | C |
The same TM just simple.
The same TM with repetitions reduced.
The same TM with tape symbol exponents.
The same TM as 1-bck-macro machine.
Simulation is done as 1-bck-macro machine with pure additive config-TRs.
Pushing initial machine.
Pushing macro factor 1.
Pushing BCK machine.
Steps BasSteps BasTpos Tape contents
0 0 0 (0)A>
1 1 1 (1)B>
2 3 -1 <C(2) 2
3 5 1 (1)C> 2
4 6 2 1 (1)A>
5 7 3 12 (1)B>
6 9 1 12 <C(2) 2
7 11 -1 <C(2) 23
8 13 1 (1)C> 23
9 14 2 1 (1)A> 22
10 16 0 1 <B(1) 0 2
11 17 -1 <B(1) 1 0 2
12 18 -2 <C(2) 12 0 2
13 20 0 (1)C> 12 0 2
14 22 -2 <C(2) 2 1 0 2
15 24 0 (1)C> 2 1 0 2
16 25 1 1 (1)A> 1 0 2
17 26 2 12 (1)A> 0 2
18 27 3 13 (1)B> 2
19 28 4 14 (1)C>
20 29 5 15 (0)D>
21 30 6 15 0 (2)A>
22 31 7 15 0 2 (1)B>
23 33 5 15 0 2 <C(2) 2
24 36 4 15 0 <B(1) 0 2
25 37 3 15 <C(2) 1 0 2
26 42 -2 <C(2) 25 1 0 2
27 44 0 (1)C> 25 1 0 2
28 45 1 1 (1)A> 24 1 0 2
29 47 -1 1 <B(1) 0 23 1 0 2
30 48 -2 <B(1) 1 0 23 1 0 2
31 49 -3 <C(2) 12 0 23 1 0 2
32 51 -1 (1)C> 12 0 23 1 0 2
33 53 -3 <C(2) 2 1 0 23 1 0 2
34 55 -1 (1)C> 2 1 0 23 1 0 2
35 56 0 1 (1)A> 1 0 23 1 0 2
36 57 1 12 (1)A> 0 23 1 0 2
37 58 2 13 (1)B> 23 1 0 2
38 59 3 14 (1)C> 22 1 0 2
39 60 4 15 (1)A> 2 1 0 2
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 11+V(1) (1)A> 24+V(2) [*]* [*]* [*]*
1 2 -2 11+V(1) <B(1) 0 23+V(2) [*]* [*]* [*]*
2 3+V(1) -3+-1*V(1) <B(1) 11+V(1) 0 23+V(2) [*]* [*]* [*]*
3 4+V(1) -4+-1*V(1) <C(2) 12+V(1) 0 23+V(2) [*]* [*]* [*]*
4 6+V(1) -2+-1*V(1) (1)C> 12+V(1) 0 23+V(2) [*]* [*]* [*]*
5 8+V(1) -4+-1*V(1) <C(2) 2 11+V(1) 0 23+V(2) [*]* [*]* [*]*
6 10+V(1) -2+-1*V(1) (1)C> 2 11+V(1) 0 23+V(2) [*]* [*]* [*]*
7 11+V(1) -1+-1*V(1) 1 (1)A> 11+V(1) 0 23+V(2) [*]* [*]* [*]*
8 12+2*V(1) 0 12+V(1) (1)A> 0 23+V(2) [*]* [*]* [*]*
9 13+2*V(1) 1 13+V(1) (1)B> 23+V(2) [*]* [*]* [*]*
10 14+2*V(1) 2 14+V(1) (1)C> 22+V(2) [*]* [*]* [*]*
11 15+2*V(1) 3 15+V(1) (1)A> 21+V(2) [*]* [*]* [*]*
<< Success! ==> defined new CTR 1 (PA)
40 62 2 15 <B(1) 0 1 0 2
41 67 -3 <B(1) 15 0 1 0 2
42 68 -4 <C(2) 16 0 1 0 2
43 70 -2 (1)C> 16 0 1 0 2
44 72 -4 <C(2) 2 15 0 1 0 2
45 74 -2 (1)C> 2 15 0 1 0 2
46 75 -1 1 (1)A> 15 0 1 0 2
47 80 4 16 (1)A> 0 1 0 2
48 81 5 17 (1)B> 1 0 2
49 83 3 17 <B(1) 1 0 2
50 90 -4 <B(1) 18 0 2
51 91 -5 <C(2) 19 0 2
52 93 -3 (1)C> 19 0 2
53 95 -5 <C(2) 2 18 0 2
54 97 -3 (1)C> 2 18 0 2
55 98 -2 1 (1)A> 18 0 2
56 106 6 19 (1)A> 0 2
57 107 7 110 (1)B> 2
58 108 8 111 (1)C>
59 109 9 112 (0)D>
60 110 10 112 0 (2)A>
61 111 11 112 0 2 (1)B>
62 113 9 112 0 2 <C(2) 2
63 116 8 112 0 <B(1) 0 2
64 117 7 112 <C(2) 1 0 2
65 129 -5 <C(2) 212 1 0 2
66 131 -3 (1)C> 212 1 0 2
67 132 -2 1 (1)A> 211 1 0 2
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 11+V(1) (1)A> 2 11+V(2) 0 2
1 2 -2 11+V(1) <B(1) 0 11+V(2) 0 2
2 3+V(1) -3+-1*V(1) <B(1) 11+V(1) 0 11+V(2) 0 2
3 4+V(1) -4+-1*V(1) <C(2) 12+V(1) 0 11+V(2) 0 2
4 6+V(1) -2+-1*V(1) (1)C> 12+V(1) 0 11+V(2) 0 2
5 8+V(1) -4+-1*V(1) <C(2) 2 11+V(1) 0 11+V(2) 0 2
6 10+V(1) -2+-1*V(1) (1)C> 2 11+V(1) 0 11+V(2) 0 2
7 11+V(1) -1+-1*V(1) 1 (1)A> 11+V(1) 0 11+V(2) 0 2
8 12+2*V(1) 0 12+V(1) (1)A> 0 11+V(2) 0 2
9 13+2*V(1) 1 13+V(1) (1)B> 11+V(2) 0 2
10 15+2*V(1) -1 13+V(1) <B(1) 11+V(2) 0 2
11 18+3*V(1) -4+-1*V(1) <B(1) 14+V(1)+V(2) 0 2
12 19+3*V(1) -5+-1*V(1) <C(2) 15+V(1)+V(2) 0 2
13 21+3*V(1) -3+-1*V(1) (1)C> 15+V(1)+V(2) 0 2
14 23+3*V(1) -5+-1*V(1) <C(2) 2 14+V(1)+V(2) 0 2
15 25+3*V(1) -3+-1*V(1) (1)C> 2 14+V(1)+V(2) 0 2
16 26+3*V(1) -2+-1*V(1) 1 (1)A> 14+V(1)+V(2) 0 2
17 30+4*V(1)+V(2) 2+V(2) 15+V(1)+V(2) (1)A> 0 2
18 31+4*V(1)+V(2) 3+V(2) 16+V(1)+V(2) (1)B> 2
19 32+4*V(1)+V(2) 4+V(2) 17+V(1)+V(2) (1)C>
20 33+4*V(1)+V(2) 5+V(2) 18+V(1)+V(2) (0)D>
21 34+4*V(1)+V(2) 6+V(2) 18+V(1)+V(2) 0 (2)A>
22 35+4*V(1)+V(2) 7+V(2) 18+V(1)+V(2) 0 2 (1)B>
23 37+4*V(1)+V(2) 5+V(2) 18+V(1)+V(2) 0 2 <C(2) 2
24 40+4*V(1)+V(2) 4+V(2) 18+V(1)+V(2) 0 <B(1) 0 2
25 41+4*V(1)+V(2) 3+V(2) 18+V(1)+V(2) <C(2) 1 0 2
26 49+5*V(1)+2*V(2) -5+-1*V(1) <C(2) 28+V(1)+V(2) 1 0 2
27 51+5*V(1)+2*V(2) -3+-1*V(1) (1)C> 28+V(1)+V(2) 1 0 2
28 52+5*V(1)+2*V(2) -2+-1*V(1) 1 (1)A> 27+V(1)+V(2) 1 0 2
<< Success! ==> defined new CTR 2 (PPA)
67 132 -2 1 (1)A> 211 1 0 2
== Executing PA-CTR 1, V(1)=0, V(2)=7, repcount=3, factor=4/3
100 201 7 113 (1)A> 22 1 0 2
101 203 5 113 <B(1) 0 2 1 0 2
102 216 -8 <B(1) 113 0 2 1 0 2
103 217 -9 <C(2) 114 0 2 1 0 2
104 219 -7 (1)C> 114 0 2 1 0 2
105 221 -9 <C(2) 2 113 0 2 1 0 2
106 223 -7 (1)C> 2 113 0 2 1 0 2
107 224 -6 1 (1)A> 113 0 2 1 0 2
108 237 7 114 (1)A> 0 2 1 0 2
109 238 8 115 (1)B> 2 1 0 2
110 239 9 116 (1)C> 1 0 2
111 241 7 116 <C(2) 2 0 2
112 257 -9 <C(2) 217 0 2
113 259 -7 (1)C> 217 0 2
114 260 -6 1 (1)A> 216 0 2
115 262 -8 1 <B(1) 0 215 0 2
116 263 -9 <B(1) 1 0 215 0 2
117 264 -10 <C(2) 12 0 215 0 2
118 266 -8 (1)C> 12 0 215 0 2
119 268 -10 <C(2) 2 1 0 215 0 2
120 270 -8 (1)C> 2 1 0 215 0 2
121 271 -7 1 (1)A> 1 0 215 0 2
122 272 -6 12 (1)A> 0 215 0 2
123 273 -5 13 (1)B> 215 0 2
124 274 -4 14 (1)C> 214 0 2
125 275 -3 15 (1)A> 213 0 2
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 11+V(1) (1)A> 24+V(2) [*]* [*]*
1 2 -2 11+V(1) <B(1) 0 23+V(2) [*]* [*]*
2 3+V(1) -3+-1*V(1) <B(1) 11+V(1) 0 23+V(2) [*]* [*]*
3 4+V(1) -4+-1*V(1) <C(2) 12+V(1) 0 23+V(2) [*]* [*]*
4 6+V(1) -2+-1*V(1) (1)C> 12+V(1) 0 23+V(2) [*]* [*]*
5 8+V(1) -4+-1*V(1) <C(2) 2 11+V(1) 0 23+V(2) [*]* [*]*
6 10+V(1) -2+-1*V(1) (1)C> 2 11+V(1) 0 23+V(2) [*]* [*]*
7 11+V(1) -1+-1*V(1) 1 (1)A> 11+V(1) 0 23+V(2) [*]* [*]*
8 12+2*V(1) 0 12+V(1) (1)A> 0 23+V(2) [*]* [*]*
9 13+2*V(1) 1 13+V(1) (1)B> 23+V(2) [*]* [*]*
10 14+2*V(1) 2 14+V(1) (1)C> 22+V(2) [*]* [*]*
11 15+2*V(1) 3 15+V(1) (1)A> 21+V(2) [*]* [*]*
<< Success! ==> defined new CTR 3 (PA)
125 275 -3 15 (1)A> 213 0 2
== Executing PA-CTR 3, V(1)=4, V(2)=9, repcount=4, factor=4/3
169 415 9 121 (1)A> 2 0 2
170 417 7 121 <B(1) 02 2
171 438 -14 <B(1) 121 02 2
172 439 -15 <C(2) 122 02 2
173 441 -13 (1)C> 122 02 2
174 443 -15 <C(2) 2 121 02 2
175 445 -13 (1)C> 2 121 02 2
176 446 -12 1 (1)A> 121 02 2
177 467 9 122 (1)A> 02 2
178 468 10 123 (1)B> 0 2
179 470 8 123 <C(2) 22
180 493 -15 <C(2) 225
181 495 -13 (1)C> 225
182 496 -12 1 (1)A> 224
183 498 -14 1 <B(1) 0 223
184 499 -15 <B(1) 1 0 223
185 500 -16 <C(2) 12 0 223
186 502 -14 (1)C> 12 0 223
187 504 -16 <C(2) 2 1 0 223
188 506 -14 (1)C> 2 1 0 223
189 507 -13 1 (1)A> 1 0 223
190 508 -12 12 (1)A> 0 223
191 509 -11 13 (1)B> 223
192 510 -10 14 (1)C> 222
193 511 -9 15 (1)A> 221
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 11+V(1) (1)A> 24+V(2)
1 2 -2 11+V(1) <B(1) 0 23+V(2)
2 3+V(1) -3+-1*V(1) <B(1) 11+V(1) 0 23+V(2)
3 4+V(1) -4+-1*V(1) <C(2) 12+V(1) 0 23+V(2)
4 6+V(1) -2+-1*V(1) (1)C> 12+V(1) 0 23+V(2)
5 8+V(1) -4+-1*V(1) <C(2) 2 11+V(1) 0 23+V(2)
6 10+V(1) -2+-1*V(1) (1)C> 2 11+V(1) 0 23+V(2)
7 11+V(1) -1+-1*V(1) 1 (1)A> 11+V(1) 0 23+V(2)
8 12+2*V(1) 0 12+V(1) (1)A> 0 23+V(2)
9 13+2*V(1) 1 13+V(1) (1)B> 23+V(2)
10 14+2*V(1) 2 14+V(1) (1)C> 22+V(2)
11 15+2*V(1) 3 15+V(1) (1)A> 21+V(2)
<< Success! ==> defined new CTR 4 (PA)
193 511 -9 15 (1)A> 221
== Executing PA-CTR 4, V(1)=4, V(2)=17, repcount=6, factor=4/3
259 769 9 129 (1)A> 23
260 771 7 129 <B(1) 0 22
261 800 -22 <B(1) 129 0 22
262 801 -23 <C(2) 130 0 22
263 803 -21 (1)C> 130 0 22
264 805 -23 <C(2) 2 129 0 22
265 807 -21 (1)C> 2 129 0 22
266 808 -20 1 (1)A> 129 0 22
267 837 9 130 (1)A> 0 22
268 838 10 131 (1)B> 22
269 839 11 132 (1)C> 2
270 840 12 133 (1)A>
271 841 13 134 (1)B>
272 843 11 134 <C(2) 2
273 877 -23 <C(2) 235
274 879 -21 (1)C> 235
275 880 -20 1 (1)A> 234
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 11+V(1) (1)A> 23
1 2 -2 11+V(1) <B(1) 0 22
2 3+V(1) -3+-1*V(1) <B(1) 11+V(1) 0 22
3 4+V(1) -4+-1*V(1) <C(2) 12+V(1) 0 22
4 6+V(1) -2+-1*V(1) (1)C> 12+V(1) 0 22
5 8+V(1) -4+-1*V(1) <C(2) 2 11+V(1) 0 22
6 10+V(1) -2+-1*V(1) (1)C> 2 11+V(1) 0 22
7 11+V(1) -1+-1*V(1) 1 (1)A> 11+V(1) 0 22
8 12+2*V(1) 0 12+V(1) (1)A> 0 22
9 13+2*V(1) 1 13+V(1) (1)B> 22
10 14+2*V(1) 2 14+V(1) (1)C> 2
11 15+2*V(1) 3 15+V(1) (1)A>
12 16+2*V(1) 4 16+V(1) (1)B>
13 18+2*V(1) 2 16+V(1) <C(2) 2
14 24+3*V(1) -4+-1*V(1) <C(2) 27+V(1)
15 26+3*V(1) -2+-1*V(1) (1)C> 27+V(1)
16 27+3*V(1) -1+-1*V(1) 1 (1)A> 26+V(1)
<< Success! ==> defined new CTR 5 (PPA)
275 880 -20 1 (1)A> 234
== Executing PA-CTR 4, V(1)=0, V(2)=30, repcount=11, factor=4/3
396 1485 13 145 (1)A> 2
397 1487 11 145 <B(1)
398 1532 -34 <B(1) 145
399 1533 -35 <C(2) 146
400 1535 -33 (1)C> 146
401 1537 -35 <C(2) 2 145
402 1539 -33 (1)C> 2 145
403 1540 -32 1 (1)A> 145
404 1585 13 146 (1)A>
405 1586 14 147 (1)B>
406 1588 12 147 <C(2) 2
407 1635 -35 <C(2) 248
408 1637 -33 (1)C> 248
409 1638 -32 1 (1)A> 247
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 12+V(1) (1)A> 2
1 2 -2 12+V(1) <B(1)
2 4+V(1) -4+-1*V(1) <B(1) 12+V(1)
3 5+V(1) -5+-1*V(1) <C(2) 13+V(1)
4 7+V(1) -3+-1*V(1) (1)C> 13+V(1)
5 9+V(1) -5+-1*V(1) <C(2) 2 12+V(1)
6 11+V(1) -3+-1*V(1) (1)C> 2 12+V(1)
7 12+V(1) -2+-1*V(1) 1 (1)A> 12+V(1)
8 14+2*V(1) 0 13+V(1) (1)A>
9 15+2*V(1) 1 14+V(1) (1)B>
10 17+2*V(1) -1 14+V(1) <C(2) 2
11 21+3*V(1) -5+-1*V(1) <C(2) 25+V(1)
12 23+3*V(1) -3+-1*V(1) (1)C> 25+V(1)
13 24+3*V(1) -2+-1*V(1) 1 (1)A> 24+V(1)
<< Success! ==> defined new CTR 6 (PPA)
409 1638 -32 1 (1)A> 247
== Executing PA-CTR 4, V(1)=0, V(2)=43, repcount=15, factor=4/3
574 2703 13 161 (1)A> 22
575 2705 11 161 <B(1) 0 2
576 2766 -50 <B(1) 161 0 2
577 2767 -51 <C(2) 162 0 2
578 2769 -49 (1)C> 162 0 2
579 2771 -51 <C(2) 2 161 0 2
580 2773 -49 (1)C> 2 161 0 2
581 2774 -48 1 (1)A> 161 0 2
582 2835 13 162 (1)A> 0 2
583 2836 14 163 (1)B> 2
584 2837 15 164 (1)C>
585 2838 16 165 (0)D>
586 2839 17 165 0 (2)A>
587 2840 18 165 0 2 (1)B>
588 2842 16 165 0 2 <C(2) 2
589 2845 15 165 0 <B(1) 0 2
590 2846 14 165 <C(2) 1 0 2
591 2911 -51 <C(2) 265 1 0 2
592 2913 -49 (1)C> 265 1 0 2
593 2914 -48 1 (1)A> 264 1 0 2
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 11+V(1) (1)A> 22
1 2 -2 11+V(1) <B(1) 0 2
2 3+V(1) -3+-1*V(1) <B(1) 11+V(1) 0 2
3 4+V(1) -4+-1*V(1) <C(2) 12+V(1) 0 2
4 6+V(1) -2+-1*V(1) (1)C> 12+V(1) 0 2
5 8+V(1) -4+-1*V(1) <C(2) 2 11+V(1) 0 2
6 10+V(1) -2+-1*V(1) (1)C> 2 11+V(1) 0 2
7 11+V(1) -1+-1*V(1) 1 (1)A> 11+V(1) 0 2
8 12+2*V(1) 0 12+V(1) (1)A> 0 2
9 13+2*V(1) 1 13+V(1) (1)B> 2
10 14+2*V(1) 2 14+V(1) (1)C>
11 15+2*V(1) 3 15+V(1) (0)D>
12 16+2*V(1) 4 15+V(1) 0 (2)A>
13 17+2*V(1) 5 15+V(1) 0 2 (1)B>
14 19+2*V(1) 3 15+V(1) 0 2 <C(2) 2
15 22+2*V(1) 2 15+V(1) 0 <B(1) 0 2
16 23+2*V(1) 1 15+V(1) <C(2) 1 0 2
17 28+3*V(1) -4+-1*V(1) <C(2) 25+V(1) 1 0 2
18 30+3*V(1) -2+-1*V(1) (1)C> 25+V(1) 1 0 2
19 31+3*V(1) -1+-1*V(1) 1 (1)A> 24+V(1) 1 0 2
<< Success! ==> defined new CTR 7 (PPA)
593 2914 -48 1 (1)A> 264 1 0 2
== Executing PA-CTR 1, V(1)=0, V(2)=60, repcount=21, factor=4/3
824 4909 15 185 (1)A> 2 1 0 2
== Executing PPA-CTR 2 (once), V(1)=84, V(2)=0
852 5381 -71 1 (1)A> 291 1 0 2
== Executing PA-CTR 1, V(1)=0, V(2)=87, repcount=30, factor=4/3
1182 9311 19 1121 (1)A> 2 1 0 2
== Executing PPA-CTR 2 (once), V(1)=120, V(2)=0
1210 9963 -103 1 (1)A> 2127 1 0 2
== Executing PA-CTR 1, V(1)=0, V(2)=123, repcount=42, factor=4/3
1672 17481 23 1169 (1)A> 2 1 0 2
== Executing PPA-CTR 2 (once), V(1)=168, V(2)=0
1700 18373 -147 1 (1)A> 2175 1 0 2
== Executing PA-CTR 1, V(1)=0, V(2)=171, repcount=58, factor=4/3
2338 32467 27 1233 (1)A> 2 1 0 2
== Executing PPA-CTR 2 (once), V(1)=232, V(2)=0
2366 33679 -207 1 (1)A> 2239 1 0 2
== Executing PA-CTR 1, V(1)=0, V(2)=235, repcount=79, factor=4/3
3235 59512 30 1317 (1)A> 22 1 0 2
3236 59514 28 1317 <B(1) 0 2 1 0 2
3237 59831 -289 <B(1) 1317 0 2 1 0 2
3238 59832 -290 <C(2) 1318 0 2 1 0 2
3239 59834 -288 (1)C> 1318 0 2 1 0 2
3240 59836 -290 <C(2) 2 1317 0 2 1 0 2
3241 59838 -288 (1)C> 2 1317 0 2 1 0 2
3242 59839 -287 1 (1)A> 1317 0 2 1 0 2
3243 60156 30 1318 (1)A> 0 2 1 0 2
3244 60157 31 1319 (1)B> 2 1 0 2
3245 60158 32 1320 (1)C> 1 0 2
3246 60160 30 1320 <C(2) 2 0 2
3247 60480 -290 <C(2) 2321 0 2
3248 60482 -288 (1)C> 2321 0 2
3249 60483 -287 1 (1)A> 2320 0 2
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 11+V(1) (1)A> 22 1 [*]* [*]*
1 2 -2 11+V(1) <B(1) 0 2 1 [*]* [*]*
2 3+V(1) -3+-1*V(1) <B(1) 11+V(1) 0 2 1 [*]* [*]*
3 4+V(1) -4+-1*V(1) <C(2) 12+V(1) 0 2 1 [*]* [*]*
4 6+V(1) -2+-1*V(1) (1)C> 12+V(1) 0 2 1 [*]* [*]*
5 8+V(1) -4+-1*V(1) <C(2) 2 11+V(1) 0 2 1 [*]* [*]*
6 10+V(1) -2+-1*V(1) (1)C> 2 11+V(1) 0 2 1 [*]* [*]*
7 11+V(1) -1+-1*V(1) 1 (1)A> 11+V(1) 0 2 1 [*]* [*]*
8 12+2*V(1) 0 12+V(1) (1)A> 0 2 1 [*]* [*]*
9 13+2*V(1) 1 13+V(1) (1)B> 2 1 [*]* [*]*
10 14+2*V(1) 2 14+V(1) (1)C> 1 [*]* [*]*
11 16+2*V(1) 0 14+V(1) <C(2) 2 [*]* [*]*
12 20+3*V(1) -4+-1*V(1) <C(2) 25+V(1) [*]* [*]*
13 22+3*V(1) -2+-1*V(1) (1)C> 25+V(1) [*]* [*]*
14 23+3*V(1) -1+-1*V(1) 1 (1)A> 24+V(1) [*]* [*]*
<< Success! ==> defined new CTR 8 (PPA)
3249 60483 -287 1 (1)A> 2320 0 2
== Executing PA-CTR 3, V(1)=0, V(2)=316, repcount=106, factor=4/3
4415 106593 31 1425 (1)A> 22 0 2
4416 106595 29 1425 <B(1) 0 2 0 2
4417 107020 -396 <B(1) 1425 0 2 0 2
4418 107021 -397 <C(2) 1426 0 2 0 2
4419 107023 -395 (1)C> 1426 0 2 0 2
4420 107025 -397 <C(2) 2 1425 0 2 0 2
4421 107027 -395 (1)C> 2 1425 0 2 0 2
4422 107028 -394 1 (1)A> 1425 0 2 0 2
4423 107453 31 1426 (1)A> 0 2 0 2
4424 107454 32 1427 (1)B> 2 0 2
4425 107455 33 1428 (1)C> 0 2
4426 107456 34 1429 (0)D> 2
4427 107457 35 1429 0 (1)C>
4428 107458 36 1429 0 1 (0)D>
4429 107459 37 1429 0 1 0 (2)A>
4430 107460 38 1429 0 1 0 2 (1)B>
4431 107462 36 1429 0 1 0 2 <C(2) 2
4432 107465 35 1429 0 1 0 <B(1) 0 2
4433 107466 34 1429 0 1 <C(2) 1 0 2
4434 107467 33 1429 0 <C(2) 2 1 0 2
4435 107469 35 1429 0 (1)C> 2 1 0 2
4436 107470 36 1429 0 1 (1)A> 1 0 2
4437 107471 37 1429 0 12 (1)A> 0 2
4438 107472 38 1429 0 13 (1)B> 2
4439 107473 39 1429 0 14 (1)C>
4440 107474 40 1429 0 15 (0)D>
4441 107475 41 1429 0 15 0 (2)A>
4442 107476 42 1429 0 15 0 2 (1)B>
4443 107478 40 1429 0 15 0 2 <C(2) 2
4444 107481 39 1429 0 15 0 <B(1) 0 2
4445 107482 38 1429 0 15 <C(2) 1 0 2
4446 107487 33 1429 0 <C(2) 25 1 0 2
4447 107489 35 1429 0 (1)C> 25 1 0 2
4448 107490 36 1429 0 1 (1)A> 24 1 0 2
4449 107492 34 1429 0 1 <B(1) 0 23 1 0 2
4450 107493 33 1429 0 <B(1) 1 0 23 1 0 2
4451 107494 32 1429 <C(2) 12 0 23 1 0 2
4452 107923 -397 <C(2) 2429 12 0 23 1 0 2
4453 107925 -395 (1)C> 2429 12 0 23 1 0 2
4454 107926 -394 1 (1)A> 2428 12 0 23 1 0 2
4455 107928 -396 1 <B(1) 0 2427 12 0 23 1 0 2
4456 107929 -397 <B(1) 1 0 2427 12 0 23 1 0 2
4457 107930 -398 <C(2) 12 0 2427 12 0 23 1 0 2
4458 107932 -396 (1)C> 12 0 2427 12 0 23 1 0 2
4459 107934 -398 <C(2) 2 1 0 2427 12 0 23 1 0 2
4460 107936 -396 (1)C> 2 1 0 2427 12 0 23 1 0 2
4461 107937 -395 1 (1)A> 1 0 2427 12 0 23 1 0 2
4462 107938 -394 12 (1)A> 0 2427 12 0 23 1 0 2
4463 107939 -393 13 (1)B> 2427 12 0 23 1 0 2
4464 107940 -392 14 (1)C> 2426 12 0 23 1 0 2
4465 107941 -391 15 (1)A> 2425 12 0 23 1 0 2
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 11+V(1) (1)A> 24+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
1 2 -2 11+V(1) <B(1) 0 23+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
2 3+V(1) -3+-1*V(1) <B(1) 11+V(1) 0 23+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
3 4+V(1) -4+-1*V(1) <C(2) 12+V(1) 0 23+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
4 6+V(1) -2+-1*V(1) (1)C> 12+V(1) 0 23+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
5 8+V(1) -4+-1*V(1) <C(2) 2 11+V(1) 0 23+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
6 10+V(1) -2+-1*V(1) (1)C> 2 11+V(1) 0 23+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
7 11+V(1) -1+-1*V(1) 1 (1)A> 11+V(1) 0 23+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
8 12+2*V(1) 0 12+V(1) (1)A> 0 23+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
9 13+2*V(1) 1 13+V(1) (1)B> 23+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
10 14+2*V(1) 2 14+V(1) (1)C> 22+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
11 15+2*V(1) 3 15+V(1) (1)A> 21+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 9 (PA)
4465 107941 -391 15 (1)A> 2425 12 0 23 1 0 2
== Executing PA-CTR 9, V(1)=4, V(2)=421, repcount=141, factor=4/3
6016 190144 32 1569 (1)A> 22 12 0 23 1 0 2
6017 190146 30 1569 <B(1) 0 2 12 0 23 1 0 2
6018 190715 -539 <B(1) 1569 0 2 12 0 23 1 0 2
6019 190716 -540 <C(2) 1570 0 2 12 0 23 1 0 2
6020 190718 -538 (1)C> 1570 0 2 12 0 23 1 0 2
6021 190720 -540 <C(2) 2 1569 0 2 12 0 23 1 0 2
6022 190722 -538 (1)C> 2 1569 0 2 12 0 23 1 0 2
6023 190723 -537 1 (1)A> 1569 0 2 12 0 23 1 0 2
6024 191292 32 1570 (1)A> 0 2 12 0 23 1 0 2
6025 191293 33 1571 (1)B> 2 12 0 23 1 0 2
6026 191294 34 1572 (1)C> 12 0 23 1 0 2
6027 191296 32 1572 <C(2) 2 1 0 23 1 0 2
6028 191868 -540 <C(2) 2573 1 0 23 1 0 2
6029 191870 -538 (1)C> 2573 1 0 23 1 0 2
6030 191871 -537 1 (1)A> 2572 1 0 23 1 0 2
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 11+V(1) (1)A> 22 12+V(2) [*]* [*]* [*]* [*]* [*]*
1 2 -2 11+V(1) <B(1) 0 2 12+V(2) [*]* [*]* [*]* [*]* [*]*
2 3+V(1) -3+-1*V(1) <B(1) 11+V(1) 0 2 12+V(2) [*]* [*]* [*]* [*]* [*]*
3 4+V(1) -4+-1*V(1) <C(2) 12+V(1) 0 2 12+V(2) [*]* [*]* [*]* [*]* [*]*
4 6+V(1) -2+-1*V(1) (1)C> 12+V(1) 0 2 12+V(2) [*]* [*]* [*]* [*]* [*]*
5 8+V(1) -4+-1*V(1) <C(2) 2 11+V(1) 0 2 12+V(2) [*]* [*]* [*]* [*]* [*]*
6 10+V(1) -2+-1*V(1) (1)C> 2 11+V(1) 0 2 12+V(2) [*]* [*]* [*]* [*]* [*]*
7 11+V(1) -1+-1*V(1) 1 (1)A> 11+V(1) 0 2 12+V(2) [*]* [*]* [*]* [*]* [*]*
8 12+2*V(1) 0 12+V(1) (1)A> 0 2 12+V(2) [*]* [*]* [*]* [*]* [*]*
9 13+2*V(1) 1 13+V(1) (1)B> 2 12+V(2) [*]* [*]* [*]* [*]* [*]*
10 14+2*V(1) 2 14+V(1) (1)C> 12+V(2) [*]* [*]* [*]* [*]* [*]*
11 16+2*V(1) 0 14+V(1) <C(2) 2 11+V(2) [*]* [*]* [*]* [*]* [*]*
12 20+3*V(1) -4+-1*V(1) <C(2) 25+V(1) 11+V(2) [*]* [*]* [*]* [*]* [*]*
13 22+3*V(1) -2+-1*V(1) (1)C> 25+V(1) 11+V(2) [*]* [*]* [*]* [*]* [*]*
14 23+3*V(1) -1+-1*V(1) 1 (1)A> 24+V(1) 11+V(2) [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 10 (PPA)
6030 191871 -537 1 (1)A> 2572 1 0 23 1 0 2
== Executing PA-CTR 9, V(1)=0, V(2)=568, repcount=190, factor=4/3
8120 338361 33 1761 (1)A> 22 1 0 23 1 0 2
8121 338363 31 1761 <B(1) 0 2 1 0 23 1 0 2
8122 339124 -730 <B(1) 1761 0 2 1 0 23 1 0 2
8123 339125 -731 <C(2) 1762 0 2 1 0 23 1 0 2
8124 339127 -729 (1)C> 1762 0 2 1 0 23 1 0 2
8125 339129 -731 <C(2) 2 1761 0 2 1 0 23 1 0 2
8126 339131 -729 (1)C> 2 1761 0 2 1 0 23 1 0 2
8127 339132 -728 1 (1)A> 1761 0 2 1 0 23 1 0 2
8128 339893 33 1762 (1)A> 0 2 1 0 23 1 0 2
8129 339894 34 1763 (1)B> 2 1 0 23 1 0 2
8130 339895 35 1764 (1)C> 1 0 23 1 0 2
8131 339897 33 1764 <C(2) 2 0 23 1 0 2
8132 340661 -731 <C(2) 2765 0 23 1 0 2
8133 340663 -729 (1)C> 2765 0 23 1 0 2
8134 340664 -728 1 (1)A> 2764 0 23 1 0 2
8135 340666 -730 1 <B(1) 0 2763 0 23 1 0 2
8136 340667 -731 <B(1) 1 0 2763 0 23 1 0 2
8137 340668 -732 <C(2) 12 0 2763 0 23 1 0 2
8138 340670 -730 (1)C> 12 0 2763 0 23 1 0 2
8139 340672 -732 <C(2) 2 1 0 2763 0 23 1 0 2
8140 340674 -730 (1)C> 2 1 0 2763 0 23 1 0 2
8141 340675 -729 1 (1)A> 1 0 2763 0 23 1 0 2
8142 340676 -728 12 (1)A> 0 2763 0 23 1 0 2
8143 340677 -727 13 (1)B> 2763 0 23 1 0 2
8144 340678 -726 14 (1)C> 2762 0 23 1 0 2
8145 340679 -725 15 (1)A> 2761 0 23 1 0 2
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 11+V(1) (1)A> 24+V(2) [*]* [*]* [*]* [*]* [*]*
1 2 -2 11+V(1) <B(1) 0 23+V(2) [*]* [*]* [*]* [*]* [*]*
2 3+V(1) -3+-1*V(1) <B(1) 11+V(1) 0 23+V(2) [*]* [*]* [*]* [*]* [*]*
3 4+V(1) -4+-1*V(1) <C(2) 12+V(1) 0 23+V(2) [*]* [*]* [*]* [*]* [*]*
4 6+V(1) -2+-1*V(1) (1)C> 12+V(1) 0 23+V(2) [*]* [*]* [*]* [*]* [*]*
5 8+V(1) -4+-1*V(1) <C(2) 2 11+V(1) 0 23+V(2) [*]* [*]* [*]* [*]* [*]*
6 10+V(1) -2+-1*V(1) (1)C> 2 11+V(1) 0 23+V(2) [*]* [*]* [*]* [*]* [*]*
7 11+V(1) -1+-1*V(1) 1 (1)A> 11+V(1) 0 23+V(2) [*]* [*]* [*]* [*]* [*]*
8 12+2*V(1) 0 12+V(1) (1)A> 0 23+V(2) [*]* [*]* [*]* [*]* [*]*
9 13+2*V(1) 1 13+V(1) (1)B> 23+V(2) [*]* [*]* [*]* [*]* [*]*
10 14+2*V(1) 2 14+V(1) (1)C> 22+V(2) [*]* [*]* [*]* [*]* [*]*
11 15+2*V(1) 3 15+V(1) (1)A> 21+V(2) [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 11 (PA)
8145 340679 -725 15 (1)A> 2761 0 23 1 0 2
== Executing PA-CTR 11, V(1)=4, V(2)=757, repcount=253, factor=4/3
10928 601522 34 11017 (1)A> 22 0 23 1 0 2
10929 601524 32 11017 <B(1) 0 2 0 23 1 0 2
10930 602541 -985 <B(1) 11017 0 2 0 23 1 0 2
10931 602542 -986 <C(2) 11018 0 2 0 23 1 0 2
10932 602544 -984 (1)C> 11018 0 2 0 23 1 0 2
10933 602546 -986 <C(2) 2 11017 0 2 0 23 1 0 2
10934 602548 -984 (1)C> 2 11017 0 2 0 23 1 0 2
10935 602549 -983 1 (1)A> 11017 0 2 0 23 1 0 2
10936 603566 34 11018 (1)A> 0 2 0 23 1 0 2
10937 603567 35 11019 (1)B> 2 0 23 1 0 2
10938 603568 36 11020 (1)C> 0 23 1 0 2
10939 603569 37 11021 (0)D> 23 1 0 2
10940 603570 38 11021 0 (1)C> 22 1 0 2
10941 603571 39 11021 0 1 (1)A> 2 1 0 2
10942 603573 37 11021 0 1 <B(1) 0 1 0 2
10943 603574 36 11021 0 <B(1) 1 0 1 0 2
10944 603575 35 11021 <C(2) 12 0 1 0 2
10945 604596 -986 <C(2) 21021 12 0 1 0 2
10946 604598 -984 (1)C> 21021 12 0 1 0 2
10947 604599 -983 1 (1)A> 21020 12 0 1 0 2
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 11+V(1) (1)A> 22 0 23 [*]* [*]* [*]*
1 2 -2 11+V(1) <B(1) 0 2 0 23 [*]* [*]* [*]*
2 3+V(1) -3+-1*V(1) <B(1) 11+V(1) 0 2 0 23 [*]* [*]* [*]*
3 4+V(1) -4+-1*V(1) <C(2) 12+V(1) 0 2 0 23 [*]* [*]* [*]*
4 6+V(1) -2+-1*V(1) (1)C> 12+V(1) 0 2 0 23 [*]* [*]* [*]*
5 8+V(1) -4+-1*V(1) <C(2) 2 11+V(1) 0 2 0 23 [*]* [*]* [*]*
6 10+V(1) -2+-1*V(1) (1)C> 2 11+V(1) 0 2 0 23 [*]* [*]* [*]*
7 11+V(1) -1+-1*V(1) 1 (1)A> 11+V(1) 0 2 0 23 [*]* [*]* [*]*
8 12+2*V(1) 0 12+V(1) (1)A> 0 2 0 23 [*]* [*]* [*]*
9 13+2*V(1) 1 13+V(1) (1)B> 2 0 23 [*]* [*]* [*]*
10 14+2*V(1) 2 14+V(1) (1)C> 0 23 [*]* [*]* [*]*
11 15+2*V(1) 3 15+V(1) (0)D> 23 [*]* [*]* [*]*
12 16+2*V(1) 4 15+V(1) 0 (1)C> 22 [*]* [*]* [*]*
13 17+2*V(1) 5 15+V(1) 0 1 (1)A> 2 [*]* [*]* [*]*
14 19+2*V(1) 3 15+V(1) 0 1 <B(1) 0 [*]* [*]* [*]*
15 20+2*V(1) 2 15+V(1) 0 <B(1) 1 0 [*]* [*]* [*]*
16 21+2*V(1) 1 15+V(1) <C(2) 12 0 [*]* [*]* [*]*
17 26+3*V(1) -4+-1*V(1) <C(2) 25+V(1) 12 0 [*]* [*]* [*]*
18 28+3*V(1) -2+-1*V(1) (1)C> 25+V(1) 12 0 [*]* [*]* [*]*
19 29+3*V(1) -1+-1*V(1) 1 (1)A> 24+V(1) 12 0 [*]* [*]* [*]*
<< Success! ==> defined new CTR 12 (PPA)
10947 604599 -983 1 (1)A> 21020 12 0 1 0 2
== Executing PA-CTR 11, V(1)=0, V(2)=1016, repcount=339, factor=4/3
14676 1068012 34 11357 (1)A> 23 12 0 1 0 2
14677 1068014 32 11357 <B(1) 0 22 12 0 1 0 2
14678 1069371 -1325 <B(1) 11357 0 22 12 0 1 0 2
14679 1069372 -1326 <C(2) 11358 0 22 12 0 1 0 2
14680 1069374 -1324 (1)C> 11358 0 22 12 0 1 0 2
14681 1069376 -1326 <C(2) 2 11357 0 22 12 0 1 0 2
14682 1069378 -1324 (1)C> 2 11357 0 22 12 0 1 0 2
14683 1069379 -1323 1 (1)A> 11357 0 22 12 0 1 0 2
14684 1070736 34 11358 (1)A> 0 22 12 0 1 0 2
14685 1070737 35 11359 (1)B> 22 12 0 1 0 2
14686 1070738 36 11360 (1)C> 2 12 0 1 0 2
14687 1070739 37 11361 (1)A> 12 0 1 0 2
14688 1070741 39 11363 (1)A> 0 1 0 2
14689 1070742 40 11364 (1)B> 1 0 2
14690 1070744 38 11364 <B(1) 1 0 2
14691 1072108 -1326 <B(1) 11365 0 2
14692 1072109 -1327 <C(2) 11366 0 2
14693 1072111 -1325 (1)C> 11366 0 2
14694 1072113 -1327 <C(2) 2 11365 0 2
14695 1072115 -1325 (1)C> 2 11365 0 2
14696 1072116 -1324 1 (1)A> 11365 0 2
14697 1073481 41 11366 (1)A> 0 2
14698 1073482 42 11367 (1)B> 2
14699 1073483 43 11368 (1)C>
14700 1073484 44 11369 (0)D>
14701 1073485 45 11369 0 (2)A>
14702 1073486 46 11369 0 2 (1)B>
14703 1073488 44 11369 0 2 <C(2) 2
14704 1073491 43 11369 0 <B(1) 0 2
14705 1073492 42 11369 <C(2) 1 0 2
14706 1074861 -1327 <C(2) 21369 1 0 2
14707 1074863 -1325 (1)C> 21369 1 0 2
14708 1074864 -1324 1 (1)A> 21368 1 0 2
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 11+V(1) (1)A> 23 11+V(3) 0 11+V(2) 0 2
1 2 -2 11+V(1) <B(1) 0 22 11+V(3) 0 11+V(2) 0 2
2 3+V(1) -3+-1*V(1) <B(1) 11+V(1) 0 22 11+V(3) 0 11+V(2) 0 2
3 4+V(1) -4+-1*V(1) <C(2) 12+V(1) 0 22 11+V(3) 0 11+V(2) 0 2
4 6+V(1) -2+-1*V(1) (1)C> 12+V(1) 0 22 11+V(3) 0 11+V(2) 0 2
5 8+V(1) -4+-1*V(1) <C(2) 2 11+V(1) 0 22 11+V(3) 0 11+V(2) 0 2
6 10+V(1) -2+-1*V(1) (1)C> 2 11+V(1) 0 22 11+V(3) 0 11+V(2) 0 2
7 11+V(1) -1+-1*V(1) 1 (1)A> 11+V(1) 0 22 11+V(3) 0 11+V(2) 0 2
8 12+2*V(1) 0 12+V(1) (1)A> 0 22 11+V(3) 0 11+V(2) 0 2
9 13+2*V(1) 1 13+V(1) (1)B> 22 11+V(3) 0 11+V(2) 0 2
10 14+2*V(1) 2 14+V(1) (1)C> 2 11+V(3) 0 11+V(2) 0 2
11 15+2*V(1) 3 15+V(1) (1)A> 11+V(3) 0 11+V(2) 0 2
12 16+2*V(1)+V(3) 4+V(3) 16+V(1)+V(3) (1)A> 0 11+V(2) 0 2
13 17+2*V(1)+V(3) 5+V(3) 17+V(1)+V(3) (1)B> 11+V(2) 0 2
14 19+2*V(1)+V(3) 3+V(3) 17+V(1)+V(3) <B(1) 11+V(2) 0 2
15 26+3*V(1)+2*V(3) -4+-1*V(1) <B(1) 18+V(1)+V(2)+V(3) 0 2
16 27+3*V(1)+2*V(3) -5+-1*V(1) <C(2) 19+V(1)+V(2)+V(3) 0 2
17 29+3*V(1)+2*V(3) -3+-1*V(1) (1)C> 19+V(1)+V(2)+V(3) 0 2
18 31+3*V(1)+2*V(3) -5+-1*V(1) <C(2) 2 18+V(1)+V(2)+V(3) 0 2
19 33+3*V(1)+2*V(3) -3+-1*V(1) (1)C> 2 18+V(1)+V(2)+V(3) 0 2
20 34+3*V(1)+2*V(3) -2+-1*V(1) 1 (1)A> 18+V(1)+V(2)+V(3) 0 2
21 42+4*V(1)+V(2)+3*V(3) 6+V(2)+V(3) 19+V(1)+V(2)+V(3) (1)A> 0 2
22 43+4*V(1)+V(2)+3*V(3) 7+V(2)+V(3) 110+V(1)+V(2)+V(3) (1)B> 2
23 44+4*V(1)+V(2)+3*V(3) 8+V(2)+V(3) 111+V(1)+V(2)+V(3) (1)C>
24 45+4*V(1)+V(2)+3*V(3) 9+V(2)+V(3) 112+V(1)+V(2)+V(3) (0)D>
25 46+4*V(1)+V(2)+3*V(3) 10+V(2)+V(3) 112+V(1)+V(2)+V(3) 0 (2)A>
26 47+4*V(1)+V(2)+3*V(3) 11+V(2)+V(3) 112+V(1)+V(2)+V(3) 0 2 (1)B>
27 49+4*V(1)+V(2)+3*V(3) 9+V(2)+V(3) 112+V(1)+V(2)+V(3) 0 2 <C(2) 2
28 52+4*V(1)+V(2)+3*V(3) 8+V(2)+V(3) 112+V(1)+V(2)+V(3) 0 <B(1) 0 2
29 53+4*V(1)+V(2)+3*V(3) 7+V(2)+V(3) 112+V(1)+V(2)+V(3) <C(2) 1 0 2
30 65+5*V(1)+2*V(2)+4*V(3) -5+-1*V(1) <C(2) 212+V(1)+V(2)+V(3) 1 0 2
31 67+5*V(1)+2*V(2)+4*V(3) -3+-1*V(1) (1)C> 212+V(1)+V(2)+V(3) 1 0 2
32 68+5*V(1)+2*V(2)+4*V(3) -2+-1*V(1) 1 (1)A> 211+V(1)+V(2)+V(3) 1 0 2
<< Success! ==> defined new CTR 13 (PPA)
14708 1074864 -1324 1 (1)A> 21368 1 0 2
== Executing PA-CTR 1, V(1)=0, V(2)=1364, repcount=455, factor=4/3
19713 1907969 41 11821 (1)A> 23 1 0 2
19714 1907971 39 11821 <B(1) 0 22 1 0 2
19715 1909792 -1782 <B(1) 11821 0 22 1 0 2
19716 1909793 -1783 <C(2) 11822 0 22 1 0 2
19717 1909795 -1781 (1)C> 11822 0 22 1 0 2
19718 1909797 -1783 <C(2) 2 11821 0 22 1 0 2
19719 1909799 -1781 (1)C> 2 11821 0 22 1 0 2
19720 1909800 -1780 1 (1)A> 11821 0 22 1 0 2
19721 1911621 41 11822 (1)A> 0 22 1 0 2
19722 1911622 42 11823 (1)B> 22 1 0 2
19723 1911623 43 11824 (1)C> 2 1 0 2
19724 1911624 44 11825 (1)A> 1 0 2
19725 1911625 45 11826 (1)A> 0 2
19726 1911626 46 11827 (1)B> 2
19727 1911627 47 11828 (1)C>
19728 1911628 48 11829 (0)D>
19729 1911629 49 11829 0 (2)A>
19730 1911630 50 11829 0 2 (1)B>
19731 1911632 48 11829 0 2 <C(2) 2
19732 1911635 47 11829 0 <B(1) 0 2
19733 1911636 46 11829 <C(2) 1 0 2
19734 1913465 -1783 <C(2) 21829 1 0 2
19735 1913467 -1781 (1)C> 21829 1 0 2
19736 1913468 -1780 1 (1)A> 21828 1 0 2
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 11+V(1) (1)A> 23 11+V(2) 0 2
1 2 -2 11+V(1) <B(1) 0 22 11+V(2) 0 2
2 3+V(1) -3+-1*V(1) <B(1) 11+V(1) 0 22 11+V(2) 0 2
3 4+V(1) -4+-1*V(1) <C(2) 12+V(1) 0 22 11+V(2) 0 2
4 6+V(1) -2+-1*V(1) (1)C> 12+V(1) 0 22 11+V(2) 0 2
5 8+V(1) -4+-1*V(1) <C(2) 2 11+V(1) 0 22 11+V(2) 0 2
6 10+V(1) -2+-1*V(1) (1)C> 2 11+V(1) 0 22 11+V(2) 0 2
7 11+V(1) -1+-1*V(1) 1 (1)A> 11+V(1) 0 22 11+V(2) 0 2
8 12+2*V(1) 0 12+V(1) (1)A> 0 22 11+V(2) 0 2
9 13+2*V(1) 1 13+V(1) (1)B> 22 11+V(2) 0 2
10 14+2*V(1) 2 14+V(1) (1)C> 2 11+V(2) 0 2
11 15+2*V(1) 3 15+V(1) (1)A> 11+V(2) 0 2
12 16+2*V(1)+V(2) 4+V(2) 16+V(1)+V(2) (1)A> 0 2
13 17+2*V(1)+V(2) 5+V(2) 17+V(1)+V(2) (1)B> 2
14 18+2*V(1)+V(2) 6+V(2) 18+V(1)+V(2) (1)C>
15 19+2*V(1)+V(2) 7+V(2) 19+V(1)+V(2) (0)D>
16 20+2*V(1)+V(2) 8+V(2) 19+V(1)+V(2) 0 (2)A>
17 21+2*V(1)+V(2) 9+V(2) 19+V(1)+V(2) 0 2 (1)B>
18 23+2*V(1)+V(2) 7+V(2) 19+V(1)+V(2) 0 2 <C(2) 2
19 26+2*V(1)+V(2) 6+V(2) 19+V(1)+V(2) 0 <B(1) 0 2
20 27+2*V(1)+V(2) 5+V(2) 19+V(1)+V(2) <C(2) 1 0 2
21 36+3*V(1)+2*V(2) -4+-1*V(1) <C(2) 29+V(1)+V(2) 1 0 2
22 38+3*V(1)+2*V(2) -2+-1*V(1) (1)C> 29+V(1)+V(2) 1 0 2
23 39+3*V(1)+2*V(2) -1+-1*V(1) 1 (1)A> 28+V(1)+V(2) 1 0 2
<< Success! ==> defined new CTR 14 (PPA)
19736 1913468 -1780 1 (1)A> 21828 1 0 2
== Executing PA-CTR 1, V(1)=0, V(2)=1824, repcount=609, factor=4/3
26435 3403691 47 12437 (1)A> 2 1 0 2
== Executing PPA-CTR 2 (once), V(1)=2436, V(2)=0
26463 3415923 -2391 1 (1)A> 22443 1 0 2
== Executing PA-CTR 1, V(1)=0, V(2)=2439, repcount=814, factor=4/3
35417 6075261 51 13257 (1)A> 2 1 0 2
== Executing PPA-CTR 2 (once), V(1)=3256, V(2)=0
35445 6091593 -3207 1 (1)A> 23263 1 0 2
== Executing PA-CTR 1, V(1)=0, V(2)=3259, repcount=1087, factor=4/3
47402 10829826 54 14349 (1)A> 22 1 0 2
== Executing PPA-CTR 8 (once), V(1)=4348
47416 10842893 -4295 1 (1)A> 24352 0 2
== Executing PA-CTR 3, V(1)=0, V(2)=4348, repcount=1450, factor=4/3
63366 19268843 55 15801 (1)A> 22 0 2
63367 19268845 53 15801 <B(1) 0 2 0 2
63368 19274646 -5748 <B(1) 15801 0 2 0 2
63369 19274647 -5749 <C(2) 15802 0 2 0 2
63370 19274649 -5747 (1)C> 15802 0 2 0 2
63371 19274651 -5749 <C(2) 2 15801 0 2 0 2
63372 19274653 -5747 (1)C> 2 15801 0 2 0 2
63373 19274654 -5746 1 (1)A> 15801 0 2 0 2
63374 19280455 55 15802 (1)A> 0 2 0 2
63375 19280456 56 15803 (1)B> 2 0 2
63376 19280457 57 15804 (1)C> 0 2
63377 19280458 58 15805 (0)D> 2
63378 19280459 59 15805 0 (1)C>
63379 19280460 60 15805 0 1 (0)D>
63380 19280461 61 15805 0 1 0 (2)A>
63381 19280462 62 15805 0 1 0 2 (1)B>
63382 19280464 60 15805 0 1 0 2 <C(2) 2
63383 19280467 59 15805 0 1 0 <B(1) 0 2
63384 19280468 58 15805 0 1 <C(2) 1 0 2
63385 19280469 57 15805 0 <C(2) 2 1 0 2
63386 19280471 59 15805 0 (1)C> 2 1 0 2
63387 19280472 60 15805 0 1 (1)A> 1 0 2
63388 19280473 61 15805 0 12 (1)A> 0 2
63389 19280474 62 15805 0 13 (1)B> 2
63390 19280475 63 15805 0 14 (1)C>
63391 19280476 64 15805 0 15 (0)D>
63392 19280477 65 15805 0 15 0 (2)A>
63393 19280478 66 15805 0 15 0 2 (1)B>
63394 19280480 64 15805 0 15 0 2 <C(2) 2
63395 19280483 63 15805 0 15 0 <B(1) 0 2
63396 19280484 62 15805 0 15 <C(2) 1 0 2
63397 19280489 57 15805 0 <C(2) 25 1 0 2
63398 19280491 59 15805 0 (1)C> 25 1 0 2
63399 19280492 60 15805 0 1 (1)A> 24 1 0 2
63400 19280494 58 15805 0 1 <B(1) 0 23 1 0 2
63401 19280495 57 15805 0 <B(1) 1 0 23 1 0 2
63402 19280496 56 15805 <C(2) 12 0 23 1 0 2
63403 19286301 -5749 <C(2) 25805 12 0 23 1 0 2
63404 19286303 -5747 (1)C> 25805 12 0 23 1 0 2
63405 19286304 -5746 1 (1)A> 25804 12 0 23 1 0 2
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 11+V(1) (1)A> 22 0 2
1 2 -2 11+V(1) <B(1) 0 2 0 2
2 3+V(1) -3+-1*V(1) <B(1) 11+V(1) 0 2 0 2
3 4+V(1) -4+-1*V(1) <C(2) 12+V(1) 0 2 0 2
4 6+V(1) -2+-1*V(1) (1)C> 12+V(1) 0 2 0 2
5 8+V(1) -4+-1*V(1) <C(2) 2 11+V(1) 0 2 0 2
6 10+V(1) -2+-1*V(1) (1)C> 2 11+V(1) 0 2 0 2
7 11+V(1) -1+-1*V(1) 1 (1)A> 11+V(1) 0 2 0 2
8 12+2*V(1) 0 12+V(1) (1)A> 0 2 0 2
9 13+2*V(1) 1 13+V(1) (1)B> 2 0 2
10 14+2*V(1) 2 14+V(1) (1)C> 0 2
11 15+2*V(1) 3 15+V(1) (0)D> 2
12 16+2*V(1) 4 15+V(1) 0 (1)C>
13 17+2*V(1) 5 15+V(1) 0 1 (0)D>
14 18+2*V(1) 6 15+V(1) 0 1 0 (2)A>
15 19+2*V(1) 7 15+V(1) 0 1 0 2 (1)B>
16 21+2*V(1) 5 15+V(1) 0 1 0 2 <C(2) 2
17 24+2*V(1) 4 15+V(1) 0 1 0 <B(1) 0 2
18 25+2*V(1) 3 15+V(1) 0 1 <C(2) 1 0 2
19 26+2*V(1) 2 15+V(1) 0 <C(2) 2 1 0 2
20 28+2*V(1) 4 15+V(1) 0 (1)C> 2 1 0 2
21 29+2*V(1) 5 15+V(1) 0 1 (1)A> 1 0 2
22 30+2*V(1) 6 15+V(1) 0 12 (1)A> 0 2
23 31+2*V(1) 7 15+V(1) 0 13 (1)B> 2
24 32+2*V(1) 8 15+V(1) 0 14 (1)C>
25 33+2*V(1) 9 15+V(1) 0 15 (0)D>
26 34+2*V(1) 10 15+V(1) 0 15 0 (2)A>
27 35+2*V(1) 11 15+V(1) 0 15 0 2 (1)B>
28 37+2*V(1) 9 15+V(1) 0 15 0 2 <C(2) 2
29 40+2*V(1) 8 15+V(1) 0 15 0 <B(1) 0 2
30 41+2*V(1) 7 15+V(1) 0 15 <C(2) 1 0 2
31 46+2*V(1) 2 15+V(1) 0 <C(2) 25 1 0 2
32 48+2*V(1) 4 15+V(1) 0 (1)C> 25 1 0 2
33 49+2*V(1) 5 15+V(1) 0 1 (1)A> 24 1 0 2
34 51+2*V(1) 3 15+V(1) 0 1 <B(1) 0 23 1 0 2
35 52+2*V(1) 2 15+V(1) 0 <B(1) 1 0 23 1 0 2
36 53+2*V(1) 1 15+V(1) <C(2) 12 0 23 1 0 2
37 58+3*V(1) -4+-1*V(1) <C(2) 25+V(1) 12 0 23 1 0 2
38 60+3*V(1) -2+-1*V(1) (1)C> 25+V(1) 12 0 23 1 0 2
39 61+3*V(1) -1+-1*V(1) 1 (1)A> 24+V(1) 12 0 23 1 0 2
<< Success! ==> defined new CTR 15 (PPA)
63405 19286304 -5746 1 (1)A> 25804 12 0 23 1 0 2
== Executing PA-CTR 9, V(1)=0, V(2)=5800, repcount=1934, factor=4/3
84679 34269002 56 17737 (1)A> 22 12 0 23 1 0 2
== Executing PPA-CTR 10 (once), V(1)=7736, V(2)=0
84693 34292233 -7681 1 (1)A> 27740 1 0 23 1 0 2
== Executing PA-CTR 9, V(1)=0, V(2)=7736, repcount=2579, factor=4/3
113062 60925566 56 110317 (1)A> 23 1 0 23 1 0 2
113063 60925568 54 110317 <B(1) 0 22 1 0 23 1 0 2
113064 60935885 -10263 <B(1) 110317 0 22 1 0 23 1 0 2
113065 60935886 -10264 <C(2) 110318 0 22 1 0 23 1 0 2
113066 60935888 -10262 (1)C> 110318 0 22 1 0 23 1 0 2
113067 60935890 -10264 <C(2) 2 110317 0 22 1 0 23 1 0 2
113068 60935892 -10262 (1)C> 2 110317 0 22 1 0 23 1 0 2
113069 60935893 -10261 1 (1)A> 110317 0 22 1 0 23 1 0 2
113070 60946210 56 110318 (1)A> 0 22 1 0 23 1 0 2
113071 60946211 57 110319 (1)B> 22 1 0 23 1 0 2
113072 60946212 58 110320 (1)C> 2 1 0 23 1 0 2
113073 60946213 59 110321 (1)A> 1 0 23 1 0 2
113074 60946214 60 110322 (1)A> 0 23 1 0 2
113075 60946215 61 110323 (1)B> 23 1 0 2
113076 60946216 62 110324 (1)C> 22 1 0 2
113077 60946217 63 110325 (1)A> 2 1 0 2
113078 60946219 61 110325 <B(1) 0 1 0 2
113079 60956544 -10264 <B(1) 110325 0 1 0 2
113080 60956545 -10265 <C(2) 110326 0 1 0 2
113081 60956547 -10263 (1)C> 110326 0 1 0 2
113082 60956549 -10265 <C(2) 2 110325 0 1 0 2
113083 60956551 -10263 (1)C> 2 110325 0 1 0 2
113084 60956552 -10262 1 (1)A> 110325 0 1 0 2
113085 60966877 63 110326 (1)A> 0 1 0 2
113086 60966878 64 110327 (1)B> 1 0 2
113087 60966880 62 110327 <B(1) 1 0 2
113088 60977207 -10265 <B(1) 110328 0 2
113089 60977208 -10266 <C(2) 110329 0 2
113090 60977210 -10264 (1)C> 110329 0 2
113091 60977212 -10266 <C(2) 2 110328 0 2
113092 60977214 -10264 (1)C> 2 110328 0 2
113093 60977215 -10263 1 (1)A> 110328 0 2
113094 60987543 65 110329 (1)A> 0 2
113095 60987544 66 110330 (1)B> 2
113096 60987545 67 110331 (1)C>
113097 60987546 68 110332 (0)D>
113098 60987547 69 110332 0 (2)A>
113099 60987548 70 110332 0 2 (1)B>
113100 60987550 68 110332 0 2 <C(2) 2
113101 60987553 67 110332 0 <B(1) 0 2
113102 60987554 66 110332 <C(2) 1 0 2
113103 60997886 -10266 <C(2) 210332 1 0 2
113104 60997888 -10264 (1)C> 210332 1 0 2
113105 60997889 -10263 1 (1)A> 210331 1 0 2
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 11+V(1) (1)A> 23 11+V(3) 0 23 11+V(2) 0 2
1 2 -2 11+V(1) <B(1) 0 22 11+V(3) 0 23 11+V(2) 0 2
2 3+V(1) -3+-1*V(1) <B(1) 11+V(1) 0 22 11+V(3) 0 23 11+V(2) 0 2
3 4+V(1) -4+-1*V(1) <C(2) 12+V(1) 0 22 11+V(3) 0 23 11+V(2) 0 2
4 6+V(1) -2+-1*V(1) (1)C> 12+V(1) 0 22 11+V(3) 0 23 11+V(2) 0 2
5 8+V(1) -4+-1*V(1) <C(2) 2 11+V(1) 0 22 11+V(3) 0 23 11+V(2) 0 2
6 10+V(1) -2+-1*V(1) (1)C> 2 11+V(1) 0 22 11+V(3) 0 23 11+V(2) 0 2
7 11+V(1) -1+-1*V(1) 1 (1)A> 11+V(1) 0 22 11+V(3) 0 23 11+V(2) 0 2
8 12+2*V(1) 0 12+V(1) (1)A> 0 22 11+V(3) 0 23 11+V(2) 0 2
9 13+2*V(1) 1 13+V(1) (1)B> 22 11+V(3) 0 23 11+V(2) 0 2
10 14+2*V(1) 2 14+V(1) (1)C> 2 11+V(3) 0 23 11+V(2) 0 2
11 15+2*V(1) 3 15+V(1) (1)A> 11+V(3) 0 23 11+V(2) 0 2
12 16+2*V(1)+V(3) 4+V(3) 16+V(1)+V(3) (1)A> 0 23 11+V(2) 0 2
13 17+2*V(1)+V(3) 5+V(3) 17+V(1)+V(3) (1)B> 23 11+V(2) 0 2
14 18+2*V(1)+V(3) 6+V(3) 18+V(1)+V(3) (1)C> 22 11+V(2) 0 2
15 19+2*V(1)+V(3) 7+V(3) 19+V(1)+V(3) (1)A> 2 11+V(2) 0 2
16 21+2*V(1)+V(3) 5+V(3) 19+V(1)+V(3) <B(1) 0 11+V(2) 0 2
17 30+3*V(1)+2*V(3) -4+-1*V(1) <B(1) 19+V(1)+V(3) 0 11+V(2) 0 2
18 31+3*V(1)+2*V(3) -5+-1*V(1) <C(2) 110+V(1)+V(3) 0 11+V(2) 0 2
19 33+3*V(1)+2*V(3) -3+-1*V(1) (1)C> 110+V(1)+V(3) 0 11+V(2) 0 2
20 35+3*V(1)+2*V(3) -5+-1*V(1) <C(2) 2 19+V(1)+V(3) 0 11+V(2) 0 2
21 37+3*V(1)+2*V(3) -3+-1*V(1) (1)C> 2 19+V(1)+V(3) 0 11+V(2) 0 2
22 38+3*V(1)+2*V(3) -2+-1*V(1) 1 (1)A> 19+V(1)+V(3) 0 11+V(2) 0 2
23 47+4*V(1)+3*V(3) 7+V(3) 110+V(1)+V(3) (1)A> 0 11+V(2) 0 2
24 48+4*V(1)+3*V(3) 8+V(3) 111+V(1)+V(3) (1)B> 11+V(2) 0 2
25 50+4*V(1)+3*V(3) 6+V(3) 111+V(1)+V(3) <B(1) 11+V(2) 0 2
26 61+5*V(1)+4*V(3) -5+-1*V(1) <B(1) 112+V(1)+V(2)+V(3) 0 2
27 62+5*V(1)+4*V(3) -6+-1*V(1) <C(2) 113+V(1)+V(2)+V(3) 0 2
28 64+5*V(1)+4*V(3) -4+-1*V(1) (1)C> 113+V(1)+V(2)+V(3) 0 2
29 66+5*V(1)+4*V(3) -6+-1*V(1) <C(2) 2 112+V(1)+V(2)+V(3) 0 2
30 68+5*V(1)+4*V(3) -4+-1*V(1) (1)C> 2 112+V(1)+V(2)+V(3) 0 2
31 69+5*V(1)+4*V(3) -3+-1*V(1) 1 (1)A> 112+V(1)+V(2)+V(3) 0 2
32 81+6*V(1)+V(2)+5*V(3) 9+V(2)+V(3) 113+V(1)+V(2)+V(3) (1)A> 0 2
33 82+6*V(1)+V(2)+5*V(3) 10+V(2)+V(3) 114+V(1)+V(2)+V(3) (1)B> 2
34 83+6*V(1)+V(2)+5*V(3) 11+V(2)+V(3) 115+V(1)+V(2)+V(3) (1)C>
35 84+6*V(1)+V(2)+5*V(3) 12+V(2)+V(3) 116+V(1)+V(2)+V(3) (0)D>
36 85+6*V(1)+V(2)+5*V(3) 13+V(2)+V(3) 116+V(1)+V(2)+V(3) 0 (2)A>
37 86+6*V(1)+V(2)+5*V(3) 14+V(2)+V(3) 116+V(1)+V(2)+V(3) 0 2 (1)B>
38 88+6*V(1)+V(2)+5*V(3) 12+V(2)+V(3) 116+V(1)+V(2)+V(3) 0 2 <C(2) 2
39 91+6*V(1)+V(2)+5*V(3) 11+V(2)+V(3) 116+V(1)+V(2)+V(3) 0 <B(1) 0 2
40 92+6*V(1)+V(2)+5*V(3) 10+V(2)+V(3) 116+V(1)+V(2)+V(3) <C(2) 1 0 2
41 108+7*V(1)+2*V(2)+6*V(3) -6+-1*V(1) <C(2) 216+V(1)+V(2)+V(3) 1 0 2
42 110+7*V(1)+2*V(2)+6*V(3) -4+-1*V(1) (1)C> 216+V(1)+V(2)+V(3) 1 0 2
43 111+7*V(1)+2*V(2)+6*V(3) -3+-1*V(1) 1 (1)A> 215+V(1)+V(2)+V(3) 1 0 2
<< Success! ==> defined new CTR 16 (PPA)
113105 60997889 -10263 1 (1)A> 210331 1 0 2
== Executing PA-CTR 1, V(1)=0, V(2)=10327, repcount=3443, factor=4/3
150978 108452758 66 113773 (1)A> 22 1 0 2
== Executing PPA-CTR 8 (once), V(1)=13772
150992 108494097 -13707 1 (1)A> 213776 0 2
== Executing PA-CTR 3, V(1)=0, V(2)=13772, repcount=4591, factor=4/3
201493 192853722 66 118365 (1)A> 23 0 2
201494 192853724 64 118365 <B(1) 0 22 0 2
201495 192872089 -18301 <B(1) 118365 0 22 0 2
201496 192872090 -18302 <C(2) 118366 0 22 0 2
201497 192872092 -18300 (1)C> 118366 0 22 0 2
201498 192872094 -18302 <C(2) 2 118365 0 22 0 2
201499 192872096 -18300 (1)C> 2 118365 0 22 0 2
201500 192872097 -18299 1 (1)A> 118365 0 22 0 2
201501 192890462 66 118366 (1)A> 0 22 0 2
201502 192890463 67 118367 (1)B> 22 0 2
201503 192890464 68 118368 (1)C> 2 0 2
201504 192890465 69 118369 (1)A> 0 2
201505 192890466 70 118370 (1)B> 2
201506 192890467 71 118371 (1)C>
201507 192890468 72 118372 (0)D>
201508 192890469 73 118372 0 (2)A>
201509 192890470 74 118372 0 2 (1)B>
201510 192890472 72 118372 0 2 <C(2) 2
201511 192890475 71 118372 0 <B(1) 0 2
201512 192890476 70 118372 <C(2) 1 0 2
201513 192908848 -18302 <C(2) 218372 1 0 2
201514 192908850 -18300 (1)C> 218372 1 0 2
201515 192908851 -18299 1 (1)A> 218371 1 0 2
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 11+V(1) (1)A> 23 0 2
1 2 -2 11+V(1) <B(1) 0 22 0 2
2 3+V(1) -3+-1*V(1) <B(1) 11+V(1) 0 22 0 2
3 4+V(1) -4+-1*V(1) <C(2) 12+V(1) 0 22 0 2
4 6+V(1) -2+-1*V(1) (1)C> 12+V(1) 0 22 0 2
5 8+V(1) -4+-1*V(1) <C(2) 2 11+V(1) 0 22 0 2
6 10+V(1) -2+-1*V(1) (1)C> 2 11+V(1) 0 22 0 2
7 11+V(1) -1+-1*V(1) 1 (1)A> 11+V(1) 0 22 0 2
8 12+2*V(1) 0 12+V(1) (1)A> 0 22 0 2
9 13+2*V(1) 1 13+V(1) (1)B> 22 0 2
10 14+2*V(1) 2 14+V(1) (1)C> 2 0 2
11 15+2*V(1) 3 15+V(1) (1)A> 0 2
12 16+2*V(1) 4 16+V(1) (1)B> 2
13 17+2*V(1) 5 17+V(1) (1)C>
14 18+2*V(1) 6 18+V(1) (0)D>
15 19+2*V(1) 7 18+V(1) 0 (2)A>
16 20+2*V(1) 8 18+V(1) 0 2 (1)B>
17 22+2*V(1) 6 18+V(1) 0 2 <C(2) 2
18 25+2*V(1) 5 18+V(1) 0 <B(1) 0 2
19 26+2*V(1) 4 18+V(1) <C(2) 1 0 2
20 34+3*V(1) -4+-1*V(1) <C(2) 28+V(1) 1 0 2
21 36+3*V(1) -2+-1*V(1) (1)C> 28+V(1) 1 0 2
22 37+3*V(1) -1+-1*V(1) 1 (1)A> 27+V(1) 1 0 2
<< Success! ==> defined new CTR 17 (PPA)
201515 192908851 -18299 1 (1)A> 218371 1 0 2
== Executing PA-CTR 1, V(1)=0, V(2)=18367, repcount=6123, factor=4/3
268868 342940720 70 124493 (1)A> 22 1 0 2
== Executing PPA-CTR 8 (once), V(1)=24492
268882 343014219 -24423 1 (1)A> 224496 0 2
== Executing PA-CTR 3, V(1)=0, V(2)=24492, repcount=8165, factor=4/3
358697 609772934 72 132661 (1)A> 2 0 2
358698 609772936 70 132661 <B(1) 02 2
358699 609805597 -32591 <B(1) 132661 02 2
358700 609805598 -32592 <C(2) 132662 02 2
358701 609805600 -32590 (1)C> 132662 02 2
358702 609805602 -32592 <C(2) 2 132661 02 2
358703 609805604 -32590 (1)C> 2 132661 02 2
358704 609805605 -32589 1 (1)A> 132661 02 2
358705 609838266 72 132662 (1)A> 02 2
358706 609838267 73 132663 (1)B> 0 2
358707 609838269 71 132663 <C(2) 22
358708 609870932 -32592 <C(2) 232665
358709 609870934 -32590 (1)C> 232665
358710 609870935 -32589 1 (1)A> 232664
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 11+V(1) (1)A> 2 0 21+V(2)
1 2 -2 11+V(1) <B(1) 02 21+V(2)
2 3+V(1) -3+-1*V(1) <B(1) 11+V(1) 02 21+V(2)
3 4+V(1) -4+-1*V(1) <C(2) 12+V(1) 02 21+V(2)
4 6+V(1) -2+-1*V(1) (1)C> 12+V(1) 02 21+V(2)
5 8+V(1) -4+-1*V(1) <C(2) 2 11+V(1) 02 21+V(2)
6 10+V(1) -2+-1*V(1) (1)C> 2 11+V(1) 02 21+V(2)
7 11+V(1) -1+-1*V(1) 1 (1)A> 11+V(1) 02 21+V(2)
8 12+2*V(1) 0 12+V(1) (1)A> 02 21+V(2)
9 13+2*V(1) 1 13+V(1) (1)B> 0 21+V(2)
10 15+2*V(1) -1 13+V(1) <C(2) 22+V(2)
11 18+3*V(1) -4+-1*V(1) <C(2) 25+V(1)+V(2)
12 20+3*V(1) -2+-1*V(1) (1)C> 25+V(1)+V(2)
13 21+3*V(1) -1+-1*V(1) 1 (1)A> 24+V(1)+V(2)
<< Success! ==> defined new CTR 18 (PPA)
358710 609870935 -32589 1 (1)A> 232664
== Executing PA-CTR 4, V(1)=0, V(2)=32660, repcount=10887, factor=4/3
478467 1084097768 72 143549 (1)A> 23
== Executing PPA-CTR 5 (once), V(1)=43548
478483 1084228439 -43477 1 (1)A> 243554
== Executing PA-CTR 4, V(1)=0, V(2)=43550, repcount=14517, factor=4/3
638170 1927361282 74 158069 (1)A> 23
== Executing PPA-CTR 5 (once), V(1)=58068
638186 1927535513 -57995 1 (1)A> 258074
== Executing PA-CTR 4, V(1)=0, V(2)=58070, repcount=19357, factor=4/3
851113 3426522236 76 177429 (1)A> 23
Lines: 500
Top steps: 499
Macro steps: 851113
Basic steps: 3426522236
Tape index: 76
nonzeros: 77433
log10(nonzeros): 4.889
log10(steps ): 9.535
Input to awk program:
gohalt 1
nbs 3
T 4-state 3-symbol #d (T.J. & S. Ligocki)
: >8.0x10^986 >3.7x10^1973
5T 1RB 1RA 0LB 2LC 1LB 1RC 0RD 2LC 1RA 2RA 1RH 1RC
L 14
M 500
pref sim
machv Lig43_d just simple
machv Lig43_d-r with repetitions reduced
machv Lig43_d-1 with tape symbol exponents
machv Lig43_d-m as 1-bck-macro machine
machv Lig43_d-a as 1-bck-macro machine with pure additive config-TRs
iam Lig43_d-a
mtype 1 0
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:14:06 CEST 2010
edate Tue Jul 6 22:14:09 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:06 CEST 2010