Comment: This TM produces >1.1x10^713 nonzeros in >1.5x10^1426 steps.
| State | on 0 |
on 1 |
on 2 |
on 0 | on 1 | on 2 | ||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Move | Goto | Move | Goto | Move | Goto | |||||||
| A | 1RB | 0LC | 1RH | 1 | right | B | 0 | left | C | 1 | right | H |
| B | 2LC | 1RD | 0LB | 2 | left | C | 1 | right | D | 0 | left | B |
| C | 2LA | 1LC | 1LA | 2 | left | A | 1 | left | C | 1 | left | A |
| D | 1RB | 2LD | 2RA | 1 | right | B | 2 | left | D | 2 | right | A |
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(1) 2
3 4 -2 <A(2) 1 2
4 8 0 1 (1)B> 1 2
5 9 1 12 (1)D> 2
6 10 2 13 (2)A>
7 11 3 13 2 (1)B>
8 13 1 13 2 <C(1) 2
9 14 0 13 <A(1) 1 2
10 15 -1 12 <C(0) 12 2
11 16 -2 1 <C(1) 0 12 2
12 17 -3 <C(1) 1 0 12 2
13 18 -4 <A(2) 12 0 12 2
14 22 -2 1 (1)B> 12 0 12 2
15 23 -1 12 (1)D> 1 0 12 2
16 25 -3 12 <D(2) 2 0 12 2
17 27 -5 <D(2) 23 0 12 2
18 31 -3 1 (1)B> 23 0 12 2
19 40 0 14 (1)B> 0 12 2
20 42 -2 14 <C(1) 2 12 2
21 46 -6 <C(1) 14 2 12 2
22 47 -7 <A(2) 15 2 12 2
23 51 -5 1 (1)B> 15 2 12 2
24 52 -4 12 (1)D> 14 2 12 2
25 54 -6 12 <D(2) 2 13 2 12 2
26 56 -8 <D(2) 23 13 2 12 2
27 60 -6 1 (1)B> 23 13 2 12 2
28 69 -3 14 (1)B> 13 2 12 2
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 11+V(1) (1)B> 13+V(2) [*]* [*]* [*]*
1 1 1 12+V(1) (1)D> 12+V(2) [*]* [*]* [*]*
2 3 -1 12+V(1) <D(2) 2 11+V(2) [*]* [*]* [*]*
3 5+V(1) -3+-1*V(1) <D(2) 23+V(1) 11+V(2) [*]* [*]* [*]*
4 9+V(1) -1+-1*V(1) 1 (1)B> 23+V(1) 11+V(2) [*]* [*]* [*]*
5 18+4*V(1) 2 14+V(1) (1)B> 11+V(2) [*]* [*]* [*]*
<< Success! ==> defined new CTR 1 (PA)
28 69 -3 14 (1)B> 13 2 12 2
== Executing PA-CTR 1, V(1)=3, V(2)=0, repcount=1, factor=3/2
33 99 -1 17 (1)B> 1 2 12 2
34 100 0 18 (1)D> 2 12 2
35 101 1 19 (2)A> 12 2
36 103 -1 19 <A(1) 0 1 2
37 104 -2 18 <C(0) 1 0 1 2
38 105 -3 17 <C(1) 0 1 0 1 2
39 112 -10 <C(1) 17 0 1 0 1 2
40 113 -11 <A(2) 18 0 1 0 1 2
41 117 -9 1 (1)B> 18 0 1 0 1 2
42 118 -8 12 (1)D> 17 0 1 0 1 2
43 120 -10 12 <D(2) 2 16 0 1 0 1 2
44 122 -12 <D(2) 23 16 0 1 0 1 2
45 126 -10 1 (1)B> 23 16 0 1 0 1 2
46 135 -7 14 (1)B> 16 0 1 0 1 2
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 11+V(1) (1)B> 13+V(2) [*]* [*]* [*]* [*]* [*]*
1 1 1 12+V(1) (1)D> 12+V(2) [*]* [*]* [*]* [*]* [*]*
2 3 -1 12+V(1) <D(2) 2 11+V(2) [*]* [*]* [*]* [*]* [*]*
3 5+V(1) -3+-1*V(1) <D(2) 23+V(1) 11+V(2) [*]* [*]* [*]* [*]* [*]*
4 9+V(1) -1+-1*V(1) 1 (1)B> 23+V(1) 11+V(2) [*]* [*]* [*]* [*]* [*]*
5 18+4*V(1) 2 14+V(1) (1)B> 11+V(2) [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 2 (PA)
46 135 -7 14 (1)B> 16 0 1 0 1 2
== Executing PA-CTR 2, V(1)=3, V(2)=3, repcount=2, factor=3/2
56 207 -3 110 (1)B> 12 0 1 0 1 2
57 208 -2 111 (1)D> 1 0 1 0 1 2
58 210 -4 111 <D(2) 2 0 1 0 1 2
59 221 -15 <D(2) 212 0 1 0 1 2
60 225 -13 1 (1)B> 212 0 1 0 1 2
61 261 -1 113 (1)B> 0 1 0 1 2
62 263 -3 113 <C(1) 2 1 0 1 2
63 276 -16 <C(1) 113 2 1 0 1 2
64 277 -17 <A(2) 114 2 1 0 1 2
65 281 -15 1 (1)B> 114 2 1 0 1 2
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 11+V(1) (1)B> 12 0 [*]* [*]* [*]* [*]*
1 1 1 12+V(1) (1)D> 1 0 [*]* [*]* [*]* [*]*
2 3 -1 12+V(1) <D(2) 2 0 [*]* [*]* [*]* [*]*
3 5+V(1) -3+-1*V(1) <D(2) 23+V(1) 0 [*]* [*]* [*]* [*]*
4 9+V(1) -1+-1*V(1) 1 (1)B> 23+V(1) 0 [*]* [*]* [*]* [*]*
5 18+4*V(1) 2 14+V(1) (1)B> 0 [*]* [*]* [*]* [*]*
6 20+4*V(1) 0 14+V(1) <C(1) 2 [*]* [*]* [*]* [*]*
7 24+5*V(1) -4+-1*V(1) <C(1) 14+V(1) 2 [*]* [*]* [*]* [*]*
8 25+5*V(1) -5+-1*V(1) <A(2) 15+V(1) 2 [*]* [*]* [*]* [*]*
9 29+5*V(1) -3+-1*V(1) 1 (1)B> 15+V(1) 2 [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 3 (PPA)
65 281 -15 1 (1)B> 114 2 1 0 1 2
== Executing PA-CTR 2, V(1)=0, V(2)=11, repcount=6, factor=3/2
95 569 -3 119 (1)B> 12 2 1 0 1 2
96 570 -2 120 (1)D> 1 2 1 0 1 2
97 572 -4 120 <D(2) 22 1 0 1 2
98 592 -24 <D(2) 222 1 0 1 2
99 596 -22 1 (1)B> 222 1 0 1 2
100 662 0 123 (1)B> 1 0 1 2
101 663 1 124 (1)D> 0 1 2
102 664 2 125 (1)B> 1 2
103 665 3 126 (1)D> 2
104 666 4 127 (2)A>
105 667 5 127 2 (1)B>
106 669 3 127 2 <C(1) 2
107 670 2 127 <A(1) 1 2
108 671 1 126 <C(0) 12 2
109 672 0 125 <C(1) 0 12 2
110 697 -25 <C(1) 125 0 12 2
111 698 -26 <A(2) 126 0 12 2
112 702 -24 1 (1)B> 126 0 12 2
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 11+V(1) (1)B> 12 21+V(2) 1 0 1 2
1 1 1 12+V(1) (1)D> 1 21+V(2) 1 0 1 2
2 3 -1 12+V(1) <D(2) 22+V(2) 1 0 1 2
3 5+V(1) -3+-1*V(1) <D(2) 24+V(1)+V(2) 1 0 1 2
4 9+V(1) -1+-1*V(1) 1 (1)B> 24+V(1)+V(2) 1 0 1 2
5 21+4*V(1)+3*V(2) 3+V(2) 15+V(1)+V(2) (1)B> 1 0 1 2
6 22+4*V(1)+3*V(2) 4+V(2) 16+V(1)+V(2) (1)D> 0 1 2
7 23+4*V(1)+3*V(2) 5+V(2) 17+V(1)+V(2) (1)B> 1 2
8 24+4*V(1)+3*V(2) 6+V(2) 18+V(1)+V(2) (1)D> 2
9 25+4*V(1)+3*V(2) 7+V(2) 19+V(1)+V(2) (2)A>
10 26+4*V(1)+3*V(2) 8+V(2) 19+V(1)+V(2) 2 (1)B>
11 28+4*V(1)+3*V(2) 6+V(2) 19+V(1)+V(2) 2 <C(1) 2
12 29+4*V(1)+3*V(2) 5+V(2) 19+V(1)+V(2) <A(1) 1 2
13 30+4*V(1)+3*V(2) 4+V(2) 18+V(1)+V(2) <C(0) 12 2
14 31+4*V(1)+3*V(2) 3+V(2) 17+V(1)+V(2) <C(1) 0 12 2
15 38+5*V(1)+4*V(2) -4+-1*V(1) <C(1) 17+V(1)+V(2) 0 12 2
16 39+5*V(1)+4*V(2) -5+-1*V(1) <A(2) 18+V(1)+V(2) 0 12 2
17 43+5*V(1)+4*V(2) -3+-1*V(1) 1 (1)B> 18+V(1)+V(2) 0 12 2
<< Success! ==> defined new CTR 4 (PPA)
112 702 -24 1 (1)B> 126 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=23, repcount=12, factor=3/2
172 1710 0 137 (1)B> 12 0 12 2
173 1711 1 138 (1)D> 1 0 12 2
174 1713 -1 138 <D(2) 2 0 12 2
175 1751 -39 <D(2) 239 0 12 2
176 1755 -37 1 (1)B> 239 0 12 2
177 1872 2 140 (1)B> 0 12 2
178 1874 0 140 <C(1) 2 12 2
179 1914 -40 <C(1) 140 2 12 2
180 1915 -41 <A(2) 141 2 12 2
181 1919 -39 1 (1)B> 141 2 12 2
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 11+V(1) (1)B> 12 0 [*]* [*]*
1 1 1 12+V(1) (1)D> 1 0 [*]* [*]*
2 3 -1 12+V(1) <D(2) 2 0 [*]* [*]*
3 5+V(1) -3+-1*V(1) <D(2) 23+V(1) 0 [*]* [*]*
4 9+V(1) -1+-1*V(1) 1 (1)B> 23+V(1) 0 [*]* [*]*
5 18+4*V(1) 2 14+V(1) (1)B> 0 [*]* [*]*
6 20+4*V(1) 0 14+V(1) <C(1) 2 [*]* [*]*
7 24+5*V(1) -4+-1*V(1) <C(1) 14+V(1) 2 [*]* [*]*
8 25+5*V(1) -5+-1*V(1) <A(2) 15+V(1) 2 [*]* [*]*
9 29+5*V(1) -3+-1*V(1) 1 (1)B> 15+V(1) 2 [*]* [*]*
<< Success! ==> defined new CTR 5 (PPA)
181 1919 -39 1 (1)B> 141 2 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=38, repcount=20, factor=3/2
281 4559 1 161 (1)B> 1 2 12 2
282 4560 2 162 (1)D> 2 12 2
283 4561 3 163 (2)A> 12 2
284 4563 1 163 <A(1) 0 1 2
285 4564 0 162 <C(0) 1 0 1 2
286 4565 -1 161 <C(1) 0 1 0 1 2
287 4626 -62 <C(1) 161 0 1 0 1 2
288 4627 -63 <A(2) 162 0 1 0 1 2
289 4631 -61 1 (1)B> 162 0 1 0 1 2
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 12+V(1) (1)B> 1 2 12+V(2) [*]*
1 1 1 13+V(1) (1)D> 2 12+V(2) [*]*
2 2 2 14+V(1) (2)A> 12+V(2) [*]*
3 4 0 14+V(1) <A(1) 0 11+V(2) [*]*
4 5 -1 13+V(1) <C(0) 1 0 11+V(2) [*]*
5 6 -2 12+V(1) <C(1) 0 1 0 11+V(2) [*]*
6 8+V(1) -4+-1*V(1) <C(1) 12+V(1) 0 1 0 11+V(2) [*]*
7 9+V(1) -5+-1*V(1) <A(2) 13+V(1) 0 1 0 11+V(2) [*]*
8 13+V(1) -3+-1*V(1) 1 (1)B> 13+V(1) 0 1 0 11+V(2) [*]*
<< Success! ==> defined new CTR 6 (PPA)
289 4631 -61 1 (1)B> 162 0 1 0 1 2
== Executing PA-CTR 2, V(1)=0, V(2)=59, repcount=30, factor=3/2
439 10391 -1 191 (1)B> 12 0 1 0 1 2
== Executing PPA-CTR 3 (once), V(1)=90
448 10870 -94 1 (1)B> 195 2 1 0 1 2
== Executing PA-CTR 2, V(1)=0, V(2)=92, repcount=47, factor=3/2
683 24688 0 1142 (1)B> 1 2 1 0 1 2
684 24689 1 1143 (1)D> 2 1 0 1 2
685 24690 2 1144 (2)A> 1 0 1 2
686 24692 0 1144 <A(1) 02 1 2
687 24693 -1 1143 <C(0) 1 02 1 2
688 24694 -2 1142 <C(1) 0 1 02 1 2
689 24836 -144 <C(1) 1142 0 1 02 1 2
690 24837 -145 <A(2) 1143 0 1 02 1 2
691 24841 -143 1 (1)B> 1143 0 1 02 1 2
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 12+V(1) (1)B> 1 2 1 01+V(2) [*]* [*]*
1 1 1 13+V(1) (1)D> 2 1 01+V(2) [*]* [*]*
2 2 2 14+V(1) (2)A> 1 01+V(2) [*]* [*]*
3 4 0 14+V(1) <A(1) 02+V(2) [*]* [*]*
4 5 -1 13+V(1) <C(0) 1 02+V(2) [*]* [*]*
5 6 -2 12+V(1) <C(1) 0 1 02+V(2) [*]* [*]*
6 8+V(1) -4+-1*V(1) <C(1) 12+V(1) 0 1 02+V(2) [*]* [*]*
7 9+V(1) -5+-1*V(1) <A(2) 13+V(1) 0 1 02+V(2) [*]* [*]*
8 13+V(1) -3+-1*V(1) 1 (1)B> 13+V(1) 0 1 02+V(2) [*]* [*]*
<< Success! ==> defined new CTR 7 (PPA)
691 24841 -143 1 (1)B> 1143 0 1 02 1 2
== Executing PA-CTR 2, V(1)=0, V(2)=140, repcount=71, factor=3/2
1046 55939 -1 1214 (1)B> 1 0 1 02 1 2
1047 55940 0 1215 (1)D> 0 1 02 1 2
1048 55941 1 1216 (1)B> 1 02 1 2
1049 55942 2 1217 (1)D> 02 1 2
1050 55943 3 1218 (1)B> 0 1 2
1051 55945 1 1218 <C(1) 2 1 2
1052 56163 -217 <C(1) 1218 2 1 2
1053 56164 -218 <A(2) 1219 2 1 2
1054 56168 -216 1 (1)B> 1219 2 1 2
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 11+V(1) (1)B> 1 0 1 02 [*]* [*]*
1 1 1 12+V(1) (1)D> 0 1 02 [*]* [*]*
2 2 2 13+V(1) (1)B> 1 02 [*]* [*]*
3 3 3 14+V(1) (1)D> 02 [*]* [*]*
4 4 4 15+V(1) (1)B> 0 [*]* [*]*
5 6 2 15+V(1) <C(1) 2 [*]* [*]*
6 11+V(1) -3+-1*V(1) <C(1) 15+V(1) 2 [*]* [*]*
7 12+V(1) -4+-1*V(1) <A(2) 16+V(1) 2 [*]* [*]*
8 16+V(1) -2+-1*V(1) 1 (1)B> 16+V(1) 2 [*]* [*]*
<< Success! ==> defined new CTR 8 (PPA)
1054 56168 -216 1 (1)B> 1219 2 1 2
== Executing PA-CTR 1, V(1)=0, V(2)=216, repcount=109, factor=3/2
1599 128762 2 1328 (1)B> 1 2 1 2
1600 128763 3 1329 (1)D> 2 1 2
1601 128764 4 1330 (2)A> 1 2
1602 128766 2 1330 <A(1) 0 2
1603 128767 1 1329 <C(0) 1 0 2
1604 128768 0 1328 <C(1) 0 1 0 2
1605 129096 -328 <C(1) 1328 0 1 0 2
1606 129097 -329 <A(2) 1329 0 1 0 2
1607 129101 -327 1 (1)B> 1329 0 1 0 2
1608 129102 -326 12 (1)D> 1328 0 1 0 2
1609 129104 -328 12 <D(2) 2 1327 0 1 0 2
1610 129106 -330 <D(2) 23 1327 0 1 0 2
1611 129110 -328 1 (1)B> 23 1327 0 1 0 2
1612 129119 -325 14 (1)B> 1327 0 1 0 2
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 11+V(1) (1)B> 13+V(2) [*]* [*]* [*]* [*]*
1 1 1 12+V(1) (1)D> 12+V(2) [*]* [*]* [*]* [*]*
2 3 -1 12+V(1) <D(2) 2 11+V(2) [*]* [*]* [*]* [*]*
3 5+V(1) -3+-1*V(1) <D(2) 23+V(1) 11+V(2) [*]* [*]* [*]* [*]*
4 9+V(1) -1+-1*V(1) 1 (1)B> 23+V(1) 11+V(2) [*]* [*]* [*]* [*]*
5 18+4*V(1) 2 14+V(1) (1)B> 11+V(2) [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 9 (PA)
1612 129119 -325 14 (1)B> 1327 0 1 0 2
== Executing PA-CTR 9, V(1)=3, V(2)=324, repcount=163, factor=3/2
2427 292445 1 1493 (1)B> 1 0 1 0 2
2428 292446 2 1494 (1)D> 0 1 0 2
2429 292447 3 1495 (1)B> 1 0 2
2430 292448 4 1496 (1)D> 0 2
2431 292449 5 1497 (1)B> 2
2432 292452 6 1498 (1)B>
2433 292454 4 1498 <C(1) 2
2434 292952 -494 <C(1) 1498 2
2435 292953 -495 <A(2) 1499 2
2436 292957 -493 1 (1)B> 1499 2
2437 292958 -492 12 (1)D> 1498 2
2438 292960 -494 12 <D(2) 2 1497 2
2439 292962 -496 <D(2) 23 1497 2
2440 292966 -494 1 (1)B> 23 1497 2
2441 292975 -491 14 (1)B> 1497 2
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 11+V(1) (1)B> 13+V(2) [*]*
1 1 1 12+V(1) (1)D> 12+V(2) [*]*
2 3 -1 12+V(1) <D(2) 2 11+V(2) [*]*
3 5+V(1) -3+-1*V(1) <D(2) 23+V(1) 11+V(2) [*]*
4 9+V(1) -1+-1*V(1) 1 (1)B> 23+V(1) 11+V(2) [*]*
5 18+4*V(1) 2 14+V(1) (1)B> 11+V(2) [*]*
<< Success! ==> defined new CTR 10 (PA)
2441 292975 -491 14 (1)B> 1497 2
== Executing PA-CTR 10, V(1)=3, V(2)=494, repcount=248, factor=3/2
3681 667951 5 1748 (1)B> 1 2
3682 667952 6 1749 (1)D> 2
3683 667953 7 1750 (2)A>
3684 667954 8 1750 2 (1)B>
3685 667956 6 1750 2 <C(1) 2
3686 667957 5 1750 <A(1) 1 2
3687 667958 4 1749 <C(0) 12 2
3688 667959 3 1748 <C(1) 0 12 2
3689 668707 -745 <C(1) 1748 0 12 2
3690 668708 -746 <A(2) 1749 0 12 2
3691 668712 -744 1 (1)B> 1749 0 12 2
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 12+V(1) (1)B> 1 2
1 1 1 13+V(1) (1)D> 2
2 2 2 14+V(1) (2)A>
3 3 3 14+V(1) 2 (1)B>
4 5 1 14+V(1) 2 <C(1) 2
5 6 0 14+V(1) <A(1) 1 2
6 7 -1 13+V(1) <C(0) 12 2
7 8 -2 12+V(1) <C(1) 0 12 2
8 10+V(1) -4+-1*V(1) <C(1) 12+V(1) 0 12 2
9 11+V(1) -5+-1*V(1) <A(2) 13+V(1) 0 12 2
10 15+V(1) -3+-1*V(1) 1 (1)B> 13+V(1) 0 12 2
<< Success! ==> defined new CTR 11 (PPA)
3691 668712 -744 1 (1)B> 1749 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=746, repcount=374, factor=3/2
5561 1512456 4 11123 (1)B> 1 0 12 2
5562 1512457 5 11124 (1)D> 0 12 2
5563 1512458 6 11125 (1)B> 12 2
5564 1512459 7 11126 (1)D> 1 2
5565 1512461 5 11126 <D(2) 22
5566 1513587 -1121 <D(2) 21128
5567 1513591 -1119 1 (1)B> 21128
5568 1516975 9 11129 (1)B>
5569 1516977 7 11129 <C(1) 2
5570 1518106 -1122 <C(1) 11129 2
5571 1518107 -1123 <A(2) 11130 2
5572 1518111 -1121 1 (1)B> 11130 2
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 11+V(1) (1)B> 1 0 12 21+V(2)
1 1 1 12+V(1) (1)D> 0 12 21+V(2)
2 2 2 13+V(1) (1)B> 12 21+V(2)
3 3 3 14+V(1) (1)D> 1 21+V(2)
4 5 1 14+V(1) <D(2) 22+V(2)
5 9+V(1) -3+-1*V(1) <D(2) 26+V(1)+V(2)
6 13+V(1) -1+-1*V(1) 1 (1)B> 26+V(1)+V(2)
7 31+4*V(1)+3*V(2) 5+V(2) 17+V(1)+V(2) (1)B>
8 33+4*V(1)+3*V(2) 3+V(2) 17+V(1)+V(2) <C(1) 2
9 40+5*V(1)+4*V(2) -4+-1*V(1) <C(1) 17+V(1)+V(2) 2
10 41+5*V(1)+4*V(2) -5+-1*V(1) <A(2) 18+V(1)+V(2) 2
11 45+5*V(1)+4*V(2) -3+-1*V(1) 1 (1)B> 18+V(1)+V(2) 2
<< Success! ==> defined new CTR 12 (PPA)
5572 1518111 -1121 1 (1)B> 11130 2
== Executing PA-CTR 10, V(1)=0, V(2)=1127, repcount=564, factor=3/2
8392 3433455 7 11693 (1)B> 12 2
8393 3433456 8 11694 (1)D> 1 2
8394 3433458 6 11694 <D(2) 22
8395 3435152 -1688 <D(2) 21696
8396 3435156 -1686 1 (1)B> 21696
8397 3440244 10 11697 (1)B>
8398 3440246 8 11697 <C(1) 2
8399 3441943 -1689 <C(1) 11697 2
8400 3441944 -1690 <A(2) 11698 2
8401 3441948 -1688 1 (1)B> 11698 2
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 11+V(1) (1)B> 12 21+V(2)
1 1 1 12+V(1) (1)D> 1 21+V(2)
2 3 -1 12+V(1) <D(2) 22+V(2)
3 5+V(1) -3+-1*V(1) <D(2) 24+V(1)+V(2)
4 9+V(1) -1+-1*V(1) 1 (1)B> 24+V(1)+V(2)
5 21+4*V(1)+3*V(2) 3+V(2) 15+V(1)+V(2) (1)B>
6 23+4*V(1)+3*V(2) 1+V(2) 15+V(1)+V(2) <C(1) 2
7 28+5*V(1)+4*V(2) -4+-1*V(1) <C(1) 15+V(1)+V(2) 2
8 29+5*V(1)+4*V(2) -5+-1*V(1) <A(2) 16+V(1)+V(2) 2
9 33+5*V(1)+4*V(2) -3+-1*V(1) 1 (1)B> 16+V(1)+V(2) 2
<< Success! ==> defined new CTR 13 (PPA)
8401 3441948 -1688 1 (1)B> 11698 2
== Executing PA-CTR 10, V(1)=0, V(2)=1695, repcount=848, factor=3/2
12641 7766748 8 12545 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=2544, V(2)=0
12650 7779501 -2539 1 (1)B> 12550 2
== Executing PA-CTR 10, V(1)=0, V(2)=2547, repcount=1274, factor=3/2
19020 17533245 9 13823 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=3822, V(2)=0
19029 17552388 -3816 1 (1)B> 13828 2
== Executing PA-CTR 10, V(1)=0, V(2)=3825, repcount=1913, factor=3/2
28594 39532758 10 15740 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=5739, V(2)=0
28603 39561486 -5732 1 (1)B> 15745 2
== Executing PA-CTR 10, V(1)=0, V(2)=5742, repcount=2872, factor=3/2
42963 89086254 12 18617 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=8615
42973 89094884 -8606 1 (1)B> 18618 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=8615, repcount=4308, factor=3/2
64513 200499764 10 112925 (1)B> 12 0 12 2
== Executing PPA-CTR 5 (once), V(1)=12924
64522 200564413 -12917 1 (1)B> 112929 2 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=12926, repcount=6464, factor=3/2
96842 451341757 11 119393 (1)B> 1 2 12 2
== Executing PPA-CTR 6 (once), V(1)=19391, V(2)=0
96850 451361161 -19383 1 (1)B> 119394 0 1 0 1 2
== Executing PA-CTR 2, V(1)=0, V(2)=19391, repcount=9696, factor=3/2
145330 1015552009 9 129089 (1)B> 12 0 1 0 1 2
== Executing PPA-CTR 3 (once), V(1)=29088
145339 1015697478 -29082 1 (1)B> 129093 2 1 0 1 2
== Executing PA-CTR 2, V(1)=0, V(2)=29090, repcount=14546, factor=3/2
218069 2285388726 10 143639 (1)B> 1 2 1 0 1 2
== Executing PPA-CTR 7 (once), V(1)=43637, V(2)=0
218077 2285432376 -43630 1 (1)B> 143640 0 1 02 1 2
== Executing PA-CTR 2, V(1)=0, V(2)=43637, repcount=21819, factor=3/2
327172 5142106770 8 165458 (1)B> 12 0 1 02 1 2
== Executing PPA-CTR 3 (once), V(1)=65457
327181 5142434084 -65452 1 (1)B> 165462 2 1 02 1 2
== Executing PA-CTR 2, V(1)=0, V(2)=65459, repcount=32730, factor=3/2
490831 11570344244 8 198191 (1)B> 12 2 1 02 1 2
490832 11570344245 9 198192 (1)D> 1 2 1 02 1 2
490833 11570344247 7 198192 <D(2) 22 1 02 1 2
490834 11570442439 -98185 <D(2) 298194 1 02 1 2
490835 11570442443 -98183 1 (1)B> 298194 1 02 1 2
490836 11570737025 11 198195 (1)B> 1 02 1 2
490837 11570737026 12 198196 (1)D> 02 1 2
490838 11570737027 13 198197 (1)B> 0 1 2
490839 11570737029 11 198197 <C(1) 2 1 2
490840 11570835226 -98186 <C(1) 198197 2 1 2
490841 11570835227 -98187 <A(2) 198198 2 1 2
490842 11570835231 -98185 1 (1)B> 198198 2 1 2
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 11+V(1) (1)B> 12 21+V(2) 1 02 [*]* [*]*
1 1 1 12+V(1) (1)D> 1 21+V(2) 1 02 [*]* [*]*
2 3 -1 12+V(1) <D(2) 22+V(2) 1 02 [*]* [*]*
3 5+V(1) -3+-1*V(1) <D(2) 24+V(1)+V(2) 1 02 [*]* [*]*
4 9+V(1) -1+-1*V(1) 1 (1)B> 24+V(1)+V(2) 1 02 [*]* [*]*
5 21+4*V(1)+3*V(2) 3+V(2) 15+V(1)+V(2) (1)B> 1 02 [*]* [*]*
6 22+4*V(1)+3*V(2) 4+V(2) 16+V(1)+V(2) (1)D> 02 [*]* [*]*
7 23+4*V(1)+3*V(2) 5+V(2) 17+V(1)+V(2) (1)B> 0 [*]* [*]*
8 25+4*V(1)+3*V(2) 3+V(2) 17+V(1)+V(2) <C(1) 2 [*]* [*]*
9 32+5*V(1)+4*V(2) -4+-1*V(1) <C(1) 17+V(1)+V(2) 2 [*]* [*]*
10 33+5*V(1)+4*V(2) -5+-1*V(1) <A(2) 18+V(1)+V(2) 2 [*]* [*]*
11 37+5*V(1)+4*V(2) -3+-1*V(1) 1 (1)B> 18+V(1)+V(2) 2 [*]* [*]*
<< Success! ==> defined new CTR 14 (PPA)
490842 11570835231 -98185 1 (1)B> 198198 2 1 2
== Executing PA-CTR 1, V(1)=0, V(2)=98195, repcount=49098, factor=3/2
736332 26035106031 11 1147295 (1)B> 12 2 1 2
736333 26035106032 12 1147296 (1)D> 1 2 1 2
736334 26035106034 10 1147296 <D(2) 22 1 2
736335 26035253330 -147286 <D(2) 2147298 1 2
736336 26035253334 -147284 1 (1)B> 2147298 1 2
736337 26035695228 14 1147299 (1)B> 1 2
736338 26035695229 15 1147300 (1)D> 2
736339 26035695230 16 1147301 (2)A>
736340 26035695231 17 1147301 2 (1)B>
736341 26035695233 15 1147301 2 <C(1) 2
736342 26035695234 14 1147301 <A(1) 1 2
736343 26035695235 13 1147300 <C(0) 12 2
736344 26035695236 12 1147299 <C(1) 0 12 2
736345 26035842535 -147287 <C(1) 1147299 0 12 2
736346 26035842536 -147288 <A(2) 1147300 0 12 2
736347 26035842540 -147286 1 (1)B> 1147300 0 12 2
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 11+V(1) (1)B> 12 21+V(2) 1 2
1 1 1 12+V(1) (1)D> 1 21+V(2) 1 2
2 3 -1 12+V(1) <D(2) 22+V(2) 1 2
3 5+V(1) -3+-1*V(1) <D(2) 24+V(1)+V(2) 1 2
4 9+V(1) -1+-1*V(1) 1 (1)B> 24+V(1)+V(2) 1 2
5 21+4*V(1)+3*V(2) 3+V(2) 15+V(1)+V(2) (1)B> 1 2
6 22+4*V(1)+3*V(2) 4+V(2) 16+V(1)+V(2) (1)D> 2
7 23+4*V(1)+3*V(2) 5+V(2) 17+V(1)+V(2) (2)A>
8 24+4*V(1)+3*V(2) 6+V(2) 17+V(1)+V(2) 2 (1)B>
9 26+4*V(1)+3*V(2) 4+V(2) 17+V(1)+V(2) 2 <C(1) 2
10 27+4*V(1)+3*V(2) 3+V(2) 17+V(1)+V(2) <A(1) 1 2
11 28+4*V(1)+3*V(2) 2+V(2) 16+V(1)+V(2) <C(0) 12 2
12 29+4*V(1)+3*V(2) 1+V(2) 15+V(1)+V(2) <C(1) 0 12 2
13 34+5*V(1)+4*V(2) -4+-1*V(1) <C(1) 15+V(1)+V(2) 0 12 2
14 35+5*V(1)+4*V(2) -5+-1*V(1) <A(2) 16+V(1)+V(2) 0 12 2
15 39+5*V(1)+4*V(2) -3+-1*V(1) 1 (1)B> 16+V(1)+V(2) 0 12 2
<< Success! ==> defined new CTR 15 (PPA)
736347 26035842540 -147286 1 (1)B> 1147300 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=147297, repcount=73649, factor=3/2
1104592 58581777534 12 1220948 (1)B> 12 0 12 2
== Executing PPA-CTR 5 (once), V(1)=220947
1104601 58582882298 -220938 1 (1)B> 1220952 2 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=220949, repcount=110475, factor=3/2
1656976 131812561748 12 1331426 (1)B> 12 2 12 2
1656977 131812561749 13 1331427 (1)D> 1 2 12 2
1656978 131812561751 11 1331427 <D(2) 22 12 2
1656979 131812893178 -331416 <D(2) 2331429 12 2
1656980 131812893182 -331414 1 (1)B> 2331429 12 2
1656981 131813887469 15 1331430 (1)B> 12 2
1656982 131813887470 16 1331431 (1)D> 1 2
1656983 131813887472 14 1331431 <D(2) 22
1656984 131814218903 -331417 <D(2) 2331433
1656985 131814218907 -331415 1 (1)B> 2331433
1656986 131815213206 18 1331434 (1)B>
1656987 131815213208 16 1331434 <C(1) 2
1656988 131815544642 -331418 <C(1) 1331434 2
1656989 131815544643 -331419 <A(2) 1331435 2
1656990 131815544647 -331417 1 (1)B> 1331435 2
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 11+V(1) (1)B> 12 21+V(3) 12 21+V(2)
1 1 1 12+V(1) (1)D> 1 21+V(3) 12 21+V(2)
2 3 -1 12+V(1) <D(2) 22+V(3) 12 21+V(2)
3 5+V(1) -3+-1*V(1) <D(2) 24+V(1)+V(3) 12 21+V(2)
4 9+V(1) -1+-1*V(1) 1 (1)B> 24+V(1)+V(3) 12 21+V(2)
5 21+4*V(1)+3*V(3) 3+V(3) 15+V(1)+V(3) (1)B> 12 21+V(2)
6 22+4*V(1)+3*V(3) 4+V(3) 16+V(1)+V(3) (1)D> 1 21+V(2)
7 24+4*V(1)+3*V(3) 2+V(3) 16+V(1)+V(3) <D(2) 22+V(2)
8 30+5*V(1)+4*V(3) -4+-1*V(1) <D(2) 28+V(1)+V(2)+V(3)
9 34+5*V(1)+4*V(3) -2+-1*V(1) 1 (1)B> 28+V(1)+V(2)+V(3)
10 58+8*V(1)+3*V(2)+7*V(3) 6+V(2)+V(3) 19+V(1)+V(2)+V(3) (1)B>
11 60+8*V(1)+3*V(2)+7*V(3) 4+V(2)+V(3) 19+V(1)+V(2)+V(3) <C(1) 2
12 69+9*V(1)+4*V(2)+8*V(3) -5+-1*V(1) <C(1) 19+V(1)+V(2)+V(3) 2
13 70+9*V(1)+4*V(2)+8*V(3) -6+-1*V(1) <A(2) 110+V(1)+V(2)+V(3) 2
14 74+9*V(1)+4*V(2)+8*V(3) -4+-1*V(1) 1 (1)B> 110+V(1)+V(2)+V(3) 2
<< Success! ==> defined new CTR 16 (PPA)
1656990 131815544647 -331417 1 (1)B> 1331435 2
== Executing PA-CTR 10, V(1)=0, V(2)=331432, repcount=165717, factor=3/2
2485575 296590277785 17 1497152 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=497150
2485585 296590774950 -497136 1 (1)B> 1497153 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=497150, repcount=248576, factor=3/2
3728465 667333924518 16 1745729 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=745728, V(2)=0
3728476 667337653203 -745715 1 (1)B> 1745736 2
== Executing PA-CTR 10, V(1)=0, V(2)=745733, repcount=372867, factor=3/2
5592811 1501520925741 19 11118602 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=1118601, V(2)=0
5592820 1501526518779 -1118585 1 (1)B> 11118607 2
== Executing PA-CTR 10, V(1)=0, V(2)=1118604, repcount=559303, factor=3/2
8389335 3378452305269 21 11677910 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=1677908
8389345 3378453983192 -1677890 1 (1)B> 11677911 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=1677908, repcount=838955, factor=3/2
12584120 7601537002802 20 12516866 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=2516865, V(2)=0
12584131 7601549587172 -2516848 1 (1)B> 12516873 2
== Executing PA-CTR 10, V(1)=0, V(2)=2516870, repcount=1258436, factor=3/2
18876311 17103531684980 24 13775309 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=3775307
18876321 17103535460302 -3775286 1 (1)B> 13775310 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=3775307, repcount=1887654, factor=3/2
28314591 38482983854446 22 15662963 (1)B> 12 0 12 2
== Executing PPA-CTR 5 (once), V(1)=5662962
28314600 38483012169285 -5662943 1 (1)B> 15662967 2 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=5662964, repcount=2831483, factor=3/2
42472015 86586822022815 23 18494450 (1)B> 1 2 12 2
== Executing PPA-CTR 6 (once), V(1)=8494448, V(2)=0
42472023 86586830517276 -8494428 1 (1)B> 18494451 0 1 0 1 2
== Executing PA-CTR 2, V(1)=0, V(2)=8494448, repcount=4247225, factor=3/2
63708148 194820402687726 22 112741676 (1)B> 1 0 1 0 1 2
63708149 194820402687727 23 112741677 (1)D> 0 1 0 1 2
63708150 194820402687728 24 112741678 (1)B> 1 0 1 2
63708151 194820402687729 25 112741679 (1)D> 0 1 2
63708152 194820402687730 26 112741680 (1)B> 1 2
63708153 194820402687731 27 112741681 (1)D> 2
63708154 194820402687732 28 112741682 (2)A>
63708155 194820402687733 29 112741682 2 (1)B>
63708156 194820402687735 27 112741682 2 <C(1) 2
63708157 194820402687736 26 112741682 <A(1) 1 2
63708158 194820402687737 25 112741681 <C(0) 12 2
63708159 194820402687738 24 112741680 <C(1) 0 12 2
63708160 194820415429418 -12741656 <C(1) 112741680 0 12 2
63708161 194820415429419 -12741657 <A(2) 112741681 0 12 2
63708162 194820415429423 -12741655 1 (1)B> 112741681 0 12 2
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 11+V(1) (1)B> 1 0 1 0 1 2
1 1 1 12+V(1) (1)D> 0 1 0 1 2
2 2 2 13+V(1) (1)B> 1 0 1 2
3 3 3 14+V(1) (1)D> 0 1 2
4 4 4 15+V(1) (1)B> 1 2
5 5 5 16+V(1) (1)D> 2
6 6 6 17+V(1) (2)A>
7 7 7 17+V(1) 2 (1)B>
8 9 5 17+V(1) 2 <C(1) 2
9 10 4 17+V(1) <A(1) 1 2
10 11 3 16+V(1) <C(0) 12 2
11 12 2 15+V(1) <C(1) 0 12 2
12 17+V(1) -3+-1*V(1) <C(1) 15+V(1) 0 12 2
13 18+V(1) -4+-1*V(1) <A(2) 16+V(1) 0 12 2
14 22+V(1) -2+-1*V(1) 1 (1)B> 16+V(1) 0 12 2
<< Success! ==> defined new CTR 17 (PPA)
63708162 194820415429423 -12741655 1 (1)B> 112741681 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=12741678, repcount=6370840, factor=3/2
95562362 438346105713103 25 119112521 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=19112520, V(2)=0
95562373 438346201275748 -19112498 1 (1)B> 119112528 2
== Executing PA-CTR 10, V(1)=0, V(2)=19112525, repcount=9556263, factor=3/2
143343688 986279291101918 28 128668790 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=28668789, V(2)=0
143343697 986279434445896 -28668764 1 (1)B> 128668795 2
== Executing PA-CTR 10, V(1)=0, V(2)=28668792, repcount=14334397, factor=3/2
215015682 2219129230580314 30 143003192 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=43003190
215015692 2219129273583519 -43003163 1 (1)B> 143003193 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=43003190, repcount=21501596, factor=3/2
322523672 4993041314885967 29 164504789 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=64504788, V(2)=0
322523683 4993041637409952 -64504762 1 (1)B> 164504796 2
== Executing PA-CTR 10, V(1)=0, V(2)=64504793, repcount=32252397, factor=3/2
483785668 11234344697912370 32 196757192 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=96757191, V(2)=0
483785677 11234345181698358 -96757162 1 (1)B> 196757197 2
== Executing PA-CTR 10, V(1)=0, V(2)=96757194, repcount=48378598, factor=3/2
725678667 25277278228915158 34 1145135795 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=145135793
725678677 25277278374050966 -145135762 1 (1)B> 1145135796 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=145135793, repcount=72567897, factor=3/2
1088518162 56873877294881384 32 1217703692 (1)B> 12 0 12 2
== Executing PPA-CTR 5 (once), V(1)=217703691
1088518171 56873878383399868 -217703662 1 (1)B> 1217703696 2 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=217703693, repcount=108851847, factor=3/2
1632777406 1279662[4]1490486 32 1326555542 (1)B> 12 2 12 2
== Executing PPA-CTR 16 (once), V(1)=326555541, V(2)=0, V(3)=0
1632777420 1279662[4]0490429 -326555513 1 (1)B> 1326555551 2
== Executing PA-CTR 10, V(1)=0, V(2)=326555548, repcount=163277775, factor=3/2
2449166295 2879240[4]3527479 37 1489833326 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=489833324
2449166305 2879240[4]3360818 -489833290 1 (1)B> 1489833327 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=489833324, repcount=244916663, factor=3/2
3673749620 6478290[4]2694188 36 1734749990 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=734749989, V(2)=0
3673749631 6478290[4]6444178 -734749956 1 (1)B> 1734749997 2
== Executing PA-CTR 10, V(1)=0, V(2)=734749994, repcount=367374998, factor=3/2
5510624621 1457615[5]7944178 40 11102124995 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=1102124993
5510624631 1457615[5]0069186 -1102124956 1 (1)B> 11102124996 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=1102124993, repcount=551062497, factor=3/2
8265937116 3279634[5]2069204 38 11653187492 (1)B> 12 0 12 2
== Executing PPA-CTR 5 (once), V(1)=1653187491
8265937125 3279634[5]8006688 -1653187456 1 (1)B> 11653187496 2 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=1653187493, repcount=826593747, factor=3/2
12398905860 7379178[5]4131706 38 12479781242 (1)B> 12 2 12 2
== Executing PPA-CTR 16 (once), V(1)=2479781241, V(2)=0, V(3)=0
12398905874 7379178[5]2162949 -2479781207 1 (1)B> 12479781251 2
== Executing PA-CTR 10, V(1)=0, V(2)=2479781248, repcount=1239890625, factor=3/2
18598358999 1660315[6]8194199 43 13719671876 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=3719671874
18598359009 1660315[6]7866088 -3719671834 1 (1)B> 13719671877 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=3719671874, repcount=1859835938, factor=3/2
27897538699 3735708[6]3936408 42 15579507815 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=5579507814, V(2)=0
27897538710 3735708[6]1475523 -5579507775 1 (1)B> 15579507822 2
== Executing PA-CTR 10, V(1)=0, V(2)=5579507819, repcount=2789753910, factor=3/2
41846308260 8405345[6]0251043 45 18369261731 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=8369261730, V(2)=0
41846308269 8405345[6]6559726 -8369261688 1 (1)B> 18369261736 2
== Executing PA-CTR 10, V(1)=0, V(2)=8369261733, repcount=4184630867, factor=3/2
62769462604 1891202[7]7160264 46 112553892602 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=12553892601, V(2)=0
62769462613 1891202[7]6623302 -12553892558 1 (1)B> 112553892607 2
== Executing PA-CTR 10, V(1)=0, V(2)=12553892604, repcount=6276946303, factor=3/2
94154194128 4255205[7]2185792 48 118830838910 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=18830838908
94154194138 4255205[7]3024715 -18830838863 1 (1)B> 118830838911 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=18830838908, repcount=9415419455, factor=3/2
141231291413 9574213[7]3040325 47 128246258366 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=28246258365, V(2)=0
141231291424 9574213[7]4332195 -28246258321 1 (1)B> 128246258373 2
== Executing PA-CTR 10, V(1)=0, V(2)=28246258370, repcount=14123129186, factor=3/2
211846937354 2154198[8]2018003 51 142369387559 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=42369387557
211846937364 2154198[8]1405575 -42369387509 1 (1)B> 142369387560 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=42369387557, repcount=21184693779, factor=3/2
317770406259 4846945[8]5535969 49 163554081338 (1)B> 12 0 12 2
== Executing PPA-CTR 5 (once), V(1)=63554081337
317770406268 4846945[8]5942683 -63554081291 1 (1)B> 163554081342 2 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=63554081339, repcount=31777040670, factor=3/2
476655609618 1090562[9]4724123 49 195331122011 (1)B> 12 2 12 2
== Executing PPA-CTR 16 (once), V(1)=95331122010, V(2)=0, V(3)=0
476655609632 1090562[9]4822287 -95331121965 1 (1)B> 195331122020 2
== Executing PA-CTR 10, V(1)=0, V(2)=95331122017, repcount=47665561009, factor=3/2
714983414677 2453766[9]8142881 53 1142996683028 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=142996683027, V(2)=0
714983414686 2453766[9]1558049 -142996682977 1 (1)B> 1142996683033 2
== Executing PA-CTR 10, V(1)=0, V(2)=142996683030, repcount=71498341516, factor=3/2
1072475122266 5520973[9]6725777 55 1214495024549 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=214495024547
1072475122276 5520973[9]1750339 -214495024495 1 (1)B> 1214495024550 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=214495024547, repcount=107247512274, factor=3/2
1608712683646 1242219[10]5804083 53 1321742536823 (1)B> 12 0 12 2
== Executing PPA-CTR 5 (once), V(1)=321742536822
1608712683655 1242219[10]8488222 -321742536772 1 (1)B> 1321742536827 2 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=321742536824, repcount=160871268413, factor=3/2
2413069025720 2794993[10]2940592 54 1482613805240 (1)B> 1 2 12 2
== Executing PPA-CTR 6 (once), V(1)=482613805238, V(2)=0
2413069025728 2794993[10]6745843 -482613805187 1 (1)B> 1482613805241 0 1 0 1 2
== Executing PA-CTR 2, V(1)=0, V(2)=482613805238, repcount=241306902620, factor=3/2
3619603538828 6288734[10]6763683 53 1723920707861 (1)B> 1 0 1 0 1 2
== Executing PPA-CTR 17 (once), V(1)=723920707860
3619603538842 6288734[10]7471565 -723920707809 1 (1)B> 1723920707866 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=723920707863, repcount=361960353932, factor=3/2
5429405308502 1414965[11]8882493 55 11085881061797 (1)B> 12 0 12 2
== Executing PPA-CTR 5 (once), V(1)=1085881061796
5429405308511 1414965[11]4191502 -1085881061744 1 (1)B> 11085881061801 2 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=1085881061798, repcount=542940530900, factor=3/2
8144107963011 3183671[11]9422302 56 11628821592701 (1)B> 1 2 12 2
== Executing PPA-CTR 6 (once), V(1)=1628821592699, V(2)=0
8144107963019 3183671[11]1015014 -1628821592646 1 (1)B> 11628821592702 0 1 0 1 2
== Executing PA-CTR 2, V(1)=0, V(2)=1628821592699, repcount=814410796350, factor=3/2
12216161944769 7163261[11]0506214 54 12443232389051 (1)B> 12 0 1 0 1 2
== Executing PPA-CTR 3 (once), V(1)=2443232389050
12216161944778 7163261[11]2451493 -2443232388999 1 (1)B> 12443232389055 2 1 0 1 2
== Executing PA-CTR 2, V(1)=0, V(2)=2443232389052, repcount=1221616194527, factor=3/2
18324242917413 1611733[12]5308191 55 13664848583582 (1)B> 1 2 1 0 1 2
== Executing PPA-CTR 7 (once), V(1)=3664848583580, V(2)=0
18324242917421 1611733[12]3891784 -3664848583528 1 (1)B> 13664848583583 0 1 02 1 2
== Executing PA-CTR 2, V(1)=0, V(2)=3664848583580, repcount=1832424291791, factor=3/2
27486364376376 3626401[12]5319362 54 15497272875374 (1)B> 1 0 1 02 1 2
== Executing PPA-CTR 8 (once), V(1)=5497272875373
27486364376384 3626401[12]8194751 -5497272875321 1 (1)B> 15497272875379 2 1 2
== Executing PA-CTR 1, V(1)=0, V(2)=5497272875376, repcount=2748636437689, factor=3/2
41229546564829 8159402[12]3411345 57 18245909313068 (1)B> 1 2 1 2
41229546564830 8159402[12]3411346 58 18245909313069 (1)D> 2 1 2
41229546564831 8159402[12]3411347 59 18245909313070 (2)A> 1 2
41229546564832 8159402[12]3411349 57 18245909313070 <A(1) 0 2
41229546564833 8159402[12]3411350 56 18245909313069 <C(0) 1 0 2
41229546564834 8159402[12]3411351 55 18245909313068 <C(1) 0 1 0 2
41229546564835 8159402[12]2724419 -8245909313013 <C(1) 18245909313068 0 1 0 2
41229546564836 8159402[12]2724420 -8245909313014 <A(2) 18245909313069 0 1 0 2
41229546564837 8159402[12]2724424 -8245909313012 1 (1)B> 18245909313069 0 1 0 2
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 12+V(1) (1)B> 1 2 1 [*]*
1 1 1 13+V(1) (1)D> 2 1 [*]*
2 2 2 14+V(1) (2)A> 1 [*]*
3 4 0 14+V(1) <A(1) 0 [*]*
4 5 -1 13+V(1) <C(0) 1 0 [*]*
5 6 -2 12+V(1) <C(1) 0 1 0 [*]*
6 8+V(1) -4+-1*V(1) <C(1) 12+V(1) 0 1 0 [*]*
7 9+V(1) -5+-1*V(1) <A(2) 13+V(1) 0 1 0 [*]*
8 13+V(1) -3+-1*V(1) 1 (1)B> 13+V(1) 0 1 0 [*]*
<< Success! ==> defined new CTR 18 (PPA)
41229546564837 8159402[12]2724424 -8245909313012 1 (1)B> 18245909313069 0 1 0 2
== Executing PA-CTR 9, V(1)=0, V(2)=8245909313066, repcount=4122954656534, factor=3/2
61844319847507 1835865[13]1961768 56 112368863969603 (1)B> 1 0 1 0 2
61844319847508 1835865[13]1961769 57 112368863969604 (1)D> 0 1 0 2
61844319847509 1835865[13]1961770 58 112368863969605 (1)B> 1 0 2
61844319847510 1835865[13]1961771 59 112368863969606 (1)D> 0 2
61844319847511 1835865[13]1961772 60 112368863969607 (1)B> 2
61844319847512 1835865[13]1961775 61 112368863969608 (1)B>
61844319847513 1835865[13]1961777 59 112368863969608 <C(1) 2
61844319847514 1835865[13]5931385 -12368863969549 <C(1) 112368863969608 2
61844319847515 1835865[13]5931386 -12368863969550 <A(2) 112368863969609 2
61844319847516 1835865[13]5931390 -12368863969548 1 (1)B> 112368863969609 2
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 11+V(1) (1)B> 1 0 1 0 21+V(2)
1 1 1 12+V(1) (1)D> 0 1 0 21+V(2)
2 2 2 13+V(1) (1)B> 1 0 21+V(2)
3 3 3 14+V(1) (1)D> 0 21+V(2)
4 4 4 15+V(1) (1)B> 21+V(2)
5 7+3*V(2) 5+V(2) 16+V(1)+V(2) (1)B>
6 9+3*V(2) 3+V(2) 16+V(1)+V(2) <C(1) 2
7 15+V(1)+4*V(2) -3+-1*V(1) <C(1) 16+V(1)+V(2) 2
8 16+V(1)+4*V(2) -4+-1*V(1) <A(2) 17+V(1)+V(2) 2
9 20+V(1)+4*V(2) -2+-1*V(1) 1 (1)B> 17+V(1)+V(2) 2
<< Success! ==> defined new CTR 19 (PPA)
61844319847516 1835865[13]5931390 -12368863969548 1 (1)B> 112368863969609 2
== Executing PA-CTR 10, V(1)=0, V(2)=12368863969606, repcount=6184431984804, factor=3/2
92766479771536 4130697[13]1259534 60 118553295954413 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=18553295954411
92766479771546 4130697[13]7213960 -18553295954354 1 (1)B> 118553295954414 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=18553295954411, repcount=9276647977206, factor=3/2
139149719657576 9294069[13]6339048 58 127829943931619 (1)B> 12 0 12 2
== Executing PPA-CTR 5 (once), V(1)=27829943931618
139149719657585 9294069[13]5997167 -27829943931563 1 (1)B> 127829943931623 2 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=27829943931620, repcount=13914971965811, factor=3/2
208724579486640 2091165[14]6913225 59 141744915897434 (1)B> 1 2 12 2
== Executing PPA-CTR 6 (once), V(1)=41744915897432, V(2)=0
208724579486648 2091165[14]2810670 -41744915897376 1 (1)B> 141744915897435 0 1 0 1 2
== Executing PA-CTR 2, V(1)=0, V(2)=41744915897432, repcount=20872457948717, factor=3/2
313086869230233 4705122[14]9871808 58 162617373846152 (1)B> 1 0 1 0 1 2
== Executing PPA-CTR 17 (once), V(1)=62617373846151
313086869230247 4705122[14]3717981 -62617373846095 1 (1)B> 162617373846157 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=62617373846154, repcount=31308686923078, factor=3/2
469630303845637 1058652[15]0759421 61 193926060769235 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=93926060769234, V(2)=0
469630303845648 1058652[15]4605636 -93926060769176 1 (1)B> 193926060769242 2
== Executing PA-CTR 10, V(1)=0, V(2)=93926060769239, repcount=46963030384620, factor=3/2
704445455768748 2381968[15]4487476 64 1140889091153861 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=140889091153860, V(2)=0
704445455768757 2381968[15]0256809 -140889091153799 1 (1)B> 1140889091153866 2
== Executing PA-CTR 10, V(1)=0, V(2)=140889091153863, repcount=70444545576932, factor=3/2
1056668183653417 5359428[15]0375737 65 1211333636730797 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=211333636730796, V(2)=0
1056668183653426 5359428[15]4029750 -211333636730734 1 (1)B> 1211333636730802 2
== Executing PA-CTR 10, V(1)=0, V(2)=211333636730799, repcount=105666818365400, factor=3/2
1585002275480426 1205871[16]7374550 66 1317000455096201 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=317000455096200, V(2)=0
1585002275480435 1205871[16]2855583 -317000455096137 1 (1)B> 1317000455096206 2
== Executing PA-CTR 10, V(1)=0, V(2)=317000455096203, repcount=158500227548102, factor=3/2
2377503413220945 2713210[16]6247231 67 1475500682644307 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=475500682644306, V(2)=0
2377503413220954 2713210[16]9468794 -475500682644242 1 (1)B> 1475500682644312 2
== Executing PA-CTR 10, V(1)=0, V(2)=475500682644309, repcount=237750341322155, factor=3/2
3566255119831729 6104724[16]8398804 68 1713251023966466 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=713251023966465, V(2)=0
3566255119831738 6104724[16]8231162 -713251023966400 1 (1)B> 1713251023966471 2
== Executing PA-CTR 10, V(1)=0, V(2)=713251023966468, repcount=356625511983235, factor=3/2
5349382679747913 1373562[17]8421332 70 11069876535949706 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=1069876535949704
5349382679747923 1373562[17]4371051 -1069876535949637 1 (1)B> 11069876535949707 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=1069876535949704, repcount=534938267974853, factor=3/2
8024074019622188 3090516[17]2298941 69 11604814803924560 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=1604814803924559, V(2)=0
8024074019622199 3090516[17]1921781 -1604814803924493 1 (1)B> 11604814803924567 2
== Executing PA-CTR 10, V(1)=0, V(2)=1604814803924564, repcount=802407401962283, factor=3/2
12036111029433614 6953662[17]2901711 73 12407222205886850 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=2407222205886848
12036111029433624 6953662[17]8788574 -2407222205886778 1 (1)B> 12407222205886851 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=2407222205886848, repcount=1203611102943425, factor=3/2
18054166544150749 1564574[18]8493424 72 13610833308830276 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=3610833308830275, V(2)=0
18054166544150760 1564574[18]2644844 -3610833308830206 1 (1)B> 13610833308830283 2
== Executing PA-CTR 10, V(1)=0, V(2)=3610833308830280, repcount=1805416654415141, factor=3/2
27081249816226465 3520291[18]5925822 76 15416249963245424 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=5416249963245422
27081249816226475 3520291[18]9171259 -5416249963245349 1 (1)B> 15416249963245425 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=5416249963245422, repcount=2708124981622712, factor=3/2
40621874724340035 7920656[18]4053467 75 18124374944868137 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=8124374944868136, V(2)=0
40621874724340046 7920656[18]8394192 -8124374944868064 1 (1)B> 18124374944868144 2
== Executing PA-CTR 10, V(1)=0, V(2)=8124374944868141, repcount=4062187472434071, factor=3/2
60932812086510401 1782147[19]7401290 78 112186562417302214 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=12186562417302213, V(2)=0
60932812086510410 1782147[19]3912388 -121865[4]7302138 1 (1)B> 112186562417302219 2
== Executing PA-CTR 10, V(1)=0, V(2)=12186562417302216, repcount=6093281208651109, factor=3/2
91399218129765955 4009832[19]9304982 80 118279843625953328 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=18279843625953326
91399218129765965 4009832[19]5258323 -182798[4]5953249 1 (1)B> 118279843625953329 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=18279843625953326, repcount=9139921812976664, factor=3/2
1370988[4]4649285 9022122[19]2391667 79 127419765438929993 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=27419765438929992, V(2)=0
1370988[4]4649296 9022122[19]7041672 -274197[4]8929916 1 (1)B> 127419765438930000 2
== Executing PA-CTR 10, V(1)=0, V(2)=27419765438929997, repcount=13709882719464999, factor=3/2
2056482[4]1974291 2029977[20]7041666 82 141129648158394998 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=41129648158394997, V(2)=0
2056482[4]1974300 2029977[20]9016684 -411296[4]8394918 1 (1)B> 141129648158395003 2
== Executing PA-CTR 10, V(1)=0, V(2)=41129648158395000, repcount=20564824079197501, factor=3/2
3084723[4]7961805 4567449[20]7256702 84 161694472237592504 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=61694472237592502
3084723[4]7961815 4567449[20]4849219 -616944[4]7592421 1 (1)B> 161694472237592505 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=61694472237592502, repcount=30847236118796252, factor=3/2
4627085[4]1943075 1027676[21]5889267 83 192541708356388757 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=92541708356388756, V(2)=0
4627085[4]1943086 1027676[21]7833092 -925417[4]6388676 1 (1)B> 192541708356388764 2
== Executing PA-CTR 10, V(1)=0, V(2)=92541708356388761, repcount=46270854178194381, factor=3/2
6940628[4]2914991 2312271[21]6004630 86 11388125[4]4583144 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=1388125[4]4583143, V(2)=0
6940628[4]2915000 2312271[21]8920378 -138812[5]4583060 1 (1)B> 11388125[4]4583149 2
== Executing PA-CTR 10, V(1)=0, V(2)=1388125[4]4583146, repcount=69406281267291574, factor=3/2
1041094[5]9372870 5202610[21]4804122 88 12082188[4]1874723 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=2082188[4]1874721
1041094[5]9372880 5202610[21]6678858 -208218[5]1874636 1 (1)B> 12082188[4]1874724 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=2082188[4]1874721, repcount=1041094[4]0937361, factor=3/2
1561641[5]4059685 1170587[22]1793116 86 13123282[4]2812084 (1)B> 12 0 12 2
== Executing PPA-CTR 5 (once), V(1)=3123282[4]2812083
1561641[5]4059694 1170587[22]5853560 -312328[5]2812000 1 (1)B> 13123282[4]2812088 2 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=3123282[4]2812085, repcount=1561641[4]1406043, factor=3/2
2342461[5]1089909 2633821[22]4233170 86 14684923[4]4218130 (1)B> 12 2 12 2
== Executing PPA-CTR 16 (once), V(1)=4684923[4]4218129, V(2)=0, V(3)=0
2342461[5]1089923 2633821[22]2196405 -468492[5]4218047 1 (1)B> 14684923[4]4218139 2
== Executing PA-CTR 10, V(1)=0, V(2)=4684923[4]4218136, repcount=2342461[4]7109069, factor=3/2
3513692[5]6635268 5926098[22]9785799 91 17027385[4]1327208 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=7027385[4]1327206
3513692[5]6635278 5926098[22]1113020 -702738[5]1327118 1 (1)B> 17027385[4]1327209 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=7027385[4]1327206, repcount=3513692[4]5663604, factor=3/2
5270539[5]4953298 1333372[23]0689164 90 11054107[5]6990813 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=1054107[5]6990812, V(2)=0
5270539[5]4953309 1333372[23]5643269 -105410[6]6990725 1 (1)B> 11054107[5]6990820 2
== Executing PA-CTR 10, V(1)=0, V(2)=1054107[5]6990817, repcount=5270539[4]3495409, factor=3/2
7905809[5]2430354 3000087[23]2051863 93 11581161[5]0486228 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=1581161[5]0486227, V(2)=0
7905809[5]2430363 3000087[23]4483031 -158116[6]0486137 1 (1)B> 11581161[5]0486233 2
== Executing PA-CTR 10, V(1)=0, V(2)=1581161[5]0486230, repcount=7905809[4]0243116, factor=3/2
1185871[6]3645943 6750196[23]9737159 95 12371742[5]0729349 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=2371742[5]0729347
1185871[6]3645953 6750196[23]0466521 -237174[6]0729255 1 (1)B> 12371742[5]0729350 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=2371742[5]0729347, repcount=1185871[5]0364674, factor=3/2
1778807[6]5469323 1518794[24]7600265 93 13557614[5]1094023 (1)B> 12 0 12 2
== Executing PPA-CTR 5 (once), V(1)=3557614[5]1094022
1778807[6]5469332 1518794[24]3070404 -355761[6]1093932 1 (1)B> 13557614[5]1094027 2 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=3557614[5]1094024, repcount=1778807[5]0547013, factor=3/2
2668210[6]8204397 3417286[24]8967574 94 15336421[5]1641040 (1)B> 1 2 12 2
== Executing PPA-CTR 6 (once), V(1)=5336421[5]1641038, V(2)=0
2668210[6]8204405 3417286[24]0608625 -533642[6]1640947 1 (1)B> 15336421[5]1641041 0 1 0 1 2
== Executing PA-CTR 2, V(1)=0, V(2)=5336421[5]1641038, repcount=2668210[5]0820520, factor=3/2
4002315[6]2307005 7688895[24]8877265 93 18004631[5]2461561 (1)B> 1 0 1 0 1 2
== Executing PPA-CTR 17 (once), V(1)=8004631[5]2461560
4002315[6]2307019 7688895[24]1338847 -800463[6]2461469 1 (1)B> 18004631[5]2461566 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=8004631[5]2461563, repcount=4002315[5]1230782, factor=3/2
6003473[6]8460929 1730001[25]2097375 95 11200694[6]3692347 (1)B> 12 0 12 2
== Executing PPA-CTR 5 (once), V(1)=1200694[6]3692346
6003473[6]8460938 1730001[25]0559134 -120069[7]3692254 1 (1)B> 11200694[6]3692351 2 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=1200694[6]3692348, repcount=6003473[5]1846175, factor=3/2
9005210[6]7691813 3892503[25]5496984 96 11801042[6]5538526 (1)B> 1 2 12 2
== Executing PPA-CTR 6 (once), V(1)=1801042[6]5538524, V(2)=0
9005210[6]7691821 3892503[25]1035521 -180104[7]5538431 1 (1)B> 11801042[6]5538527 0 1 0 1 2
== Executing PA-CTR 2, V(1)=0, V(2)=1801042[6]5538524, repcount=9005210[5]7769263, factor=3/2
1350781[7]6538136 8758132[25]9645691 95 12701563[6]3307790 (1)B> 1 0 1 0 1 2
== Executing PPA-CTR 17 (once), V(1)=2701563[6]3307789
1350781[7]6538150 8758132[25]2953502 -270156[7]3307696 1 (1)B> 12701563[6]3307795 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=2701563[6]3307792, repcount=1350781[6]6653897, factor=3/2
2026172[7]9807635 1970579[26]4519920 98 14052344[6]9961692 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=4052344[6]9961691, V(2)=0
2026172[7]9807646 1970579[26]4328420 -405234[7]9961596 1 (1)B> 14052344[6]9961699 2
== Executing PA-CTR 10, V(1)=0, V(2)=4052344[6]9961696, repcount=2026172[6]4980849, factor=3/2
3039258[7]4711891 4433804[26]4663414 102 16078517[6]4942548 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=6078517[6]4942546
3039258[7]4711901 4433804[26]9605975 -607851[7]4942447 1 (1)B> 16078517[6]4942549 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=6078517[6]4942546, repcount=3039258[6]2471274, factor=3/2
4558887[7]7068271 9976060[26]0359719 101 19117775[6]7413823 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=9117775[6]7413822, V(2)=0
4558887[7]7068282 9976060[26]7428874 -911777[7]7413724 1 (1)B> 19117775[6]7413830 2
== Executing PA-CTR 10, V(1)=0, V(2)=9117775[6]7413827, repcount=4558887[6]3706914, factor=3/2
6838331[7]5602852 2244613[27]0332218 104 11367666[7]1120743 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=1367666[7]1120742, V(2)=0
6838331[7]5602861 2244613[27]5935961 -136766[8]1120641 1 (1)B> 11367666[7]1120748 2
== Executing PA-CTR 10, V(1)=0, V(2)=1367666[7]1120745, repcount=6838331[6]5560373, factor=3/2
1025749[8]3404726 5050380[27]0055211 105 12051499[7]6681120 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=2051499[7]6681119, V(2)=0
1025749[8]3404735 5050380[27]3460839 -205149[8]6681017 1 (1)B> 12051499[7]6681125 2
== Executing PA-CTR 10, V(1)=0, V(2)=2051499[7]6681122, repcount=1025749[7]3340562, factor=3/2
1538624[8]0107545 1136335[28]0402647 107 13077249[7]0021687 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=3077249[7]0021685
1538624[8]0107555 1136335[28]0424347 -307724[8]0021581 1 (1)B> 13077249[7]0021688 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=3077249[7]0021685, repcount=1538624[7]5010843, factor=3/2
2307937[8]5161770 2556755[28]5978357 105 14615874[7]5032530 (1)B> 12 0 12 2
== Executing PPA-CTR 5 (once), V(1)=4615874[7]5032529
2307937[8]5161779 2556755[28]1141031 -461587[8]5032427 1 (1)B> 14615874[7]5032534 2 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=4615874[7]5032531, repcount=2307937[7]2516266, factor=3/2
3461905[8]7743109 5752699[28]8832759 105 16923811[7]7548799 (1)B> 12 2 12 2
== Executing PPA-CTR 16 (once), V(1)=6923811[7]7548798, V(2)=0, V(3)=0
3461905[8]7743123 5752699[28]6772015 -692381[8]7548697 1 (1)B> 16923811[7]7548808 2
== Executing PA-CTR 10, V(1)=0, V(2)=6923811[7]7548805, repcount=3461905[7]3774403, factor=3/2
5192858[8]6615138 1294357[29]0103305 109 11038571[8]1323210 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=1038571[8]1323209, V(2)=0
5192858[8]6615147 1294357[29]6719383 -103857[9]1323103 1 (1)B> 11038571[8]1323215 2
== Executing PA-CTR 10, V(1)=0, V(2)=1038571[8]1323212, repcount=5192858[7]0661607, factor=3/2
7789287[8]9923182 2912303[29]7593361 111 11557857[8]1984822 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=1557857[8]1984820
7789287[8]9923192 2912303[29]9578196 -155785[9]1984712 1 (1)B> 11557857[8]1984823 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=1557857[8]1984820, repcount=7789287[7]5992411, factor=3/2
1168393[9]9885247 6552683[29]9044654 110 12336786[8]7977234 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=2336786[8]7977233, V(2)=0
1168393[9]9885258 6552683[29]8930864 -233678[9]7977126 1 (1)B> 12336786[8]7977241 2
== Executing PA-CTR 10, V(1)=0, V(2)=2336786[8]7977238, repcount=1168393[8]8988620, factor=3/2
1752589[9]4828358 1474353[30]3820704 114 13505179[8]6965861 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=3505179[8]6965859
1752589[9]4828368 1474353[30]0786578 -350517[9]6965748 1 (1)B> 13505179[8]6965862 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=3505179[8]6965859, repcount=1752589[8]8482930, factor=3/2
2628884[9]7243018 3317296[30]0891138 112 15257769[8]5448791 (1)B> 12 0 12 2
== Executing PPA-CTR 5 (once), V(1)=5257769[8]5448790
2628884[9]7243027 3317296[30]8135117 -525776[9]5448681 1 (1)B> 15257769[8]5448795 2 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=5257769[8]5448792, repcount=2628884[8]7724397, factor=3/2
3943326[9]5865012 7463916[30]4909535 113 17886653[8]3173192 (1)B> 1 2 12 2
== Executing PPA-CTR 6 (once), V(1)=7886653[8]3173190, V(2)=0
3943326[9]5865020 7463916[30]8082738 -788665[9]3173080 1 (1)B> 17886653[8]3173193 0 1 0 1 2
== Executing PA-CTR 2, V(1)=0, V(2)=7886653[8]3173190, repcount=3943326[8]1586596, factor=3/2
5914990[9]3798000 1679381[31]8325186 112 11182998[9]4759789 (1)B> 1 0 1 0 1 2
== Executing PPA-CTR 17 (once), V(1)=1182998[9]4759788
5914990[9]3798014 1679381[31]3084996 -118299[10]4759678 1 (1)B> 11182998[9]4759794 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=1182998[9]4759791, repcount=5914990[8]2379896, factor=3/2
8872485[9]5697494 3778607[31]1468644 114 11774497[9]7139689 (1)B> 12 0 12 2
== Executing PPA-CTR 5 (once), V(1)=1774497[9]7139688
8872485[9]5697503 3778607[31]7167113 -177449[10]7139577 1 (1)B> 11774497[9]7139693 2 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=1774497[9]7139690, repcount=8872485[8]3569846, factor=3/2
1330872[10]3546733 8501867[31]2787561 115 12661745[9]0709539 (1)B> 1 2 12 2
== Executing PPA-CTR 6 (once), V(1)=2661745[9]0709537, V(2)=0
1330872[10]3546741 8501867[31]3497111 -266174[10]0709425 1 (1)B> 12661745[9]0709540 0 1 0 1 2
== Executing PA-CTR 2, V(1)=0, V(2)=2661745[9]0709537, repcount=1330872[9]0354769, factor=3/2
1996309[10]5320586 1912920[32]4014505 113 13992618[9]1064308 (1)B> 12 0 1 0 1 2
== Executing PPA-CTR 3 (once), V(1)=3992618[9]1064307
1996309[10]5320595 1912920[32]9336069 -399261[10]1064197 1 (1)B> 13992618[9]1064312 2 1 0 1 2
== Executing PA-CTR 2, V(1)=0, V(2)=3992618[9]1064309, repcount=1996309[9]0532155, factor=3/2
2994463[10]7981370 4304070[32]9386079 113 15988927[9]1596466 (1)B> 12 2 1 0 1 2
== Executing PPA-CTR 4 (once), V(1)=5988927[9]1596465, V(2)=0
2994463[10]7981387 4304070[32]7368447 -598892[10]1596355 1 (1)B> 15988927[9]1596473 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=5988927[9]1596470, repcount=2994463[9]0798236, factor=3/2
4491695[10]1972567 9684158[32]1217455 117 18983391[9]2394709 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=8983391[9]2394708, V(2)=0
4491695[10]1972578 9684158[32]3191040 -898339[10]2394594 1 (1)B> 18983391[9]2394716 2
== Executing PA-CTR 10, V(1)=0, V(2)=8983391[9]2394713, repcount=4491695[9]1197357, factor=3/2
6737543[10]7959363 2178935[33]0272018 120 11347508[10]3592072 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=1347508[10]3592071, V(2)=0
6737543[10]7959372 2178935[33]8232406 -134750[11]3591954 1 (1)B> 11347508[10]3592077 2
== Executing PA-CTR 10, V(1)=0, V(2)=1347508[10]3592074, repcount=6737543[9]6796038, factor=3/2
1010631[11]1939562 4902605[33]4769526 122 12021263[10]0388115 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=2021263[10]0388113
1010631[11]1939572 4902605[33]5157654 -202126[11]0387994 1 (1)B> 12021263[10]0388116 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=2021263[10]0388113, repcount=1010631[10]0194057, factor=3/2
1515947[11]2909857 1103086[34]6201832 120 13031894[10]0582172 (1)B> 12 0 12 2
== Executing PPA-CTR 5 (once), V(1)=3031894[10]0582171
1515947[11]2909866 1103086[34]9112716 -303189[11]0582054 1 (1)B> 13031894[10]0582176 2 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=3031894[10]0582173, repcount=1515947[10]5291087, factor=3/2
2273920[11]9365301 2481943[34]2455174 120 14547841[10]5873262 (1)B> 12 2 12 2
== Executing PPA-CTR 16 (once), V(1)=4547841[10]5873261, V(2)=0, V(3)=0
2273920[11]9365315 2481943[34]5314597 -454784[11]5873145 1 (1)B> 14547841[10]5873271 2
== Executing PA-CTR 10, V(1)=0, V(2)=4547841[10]5873268, repcount=2273920[10]7936635, factor=3/2
3410881[11]9048490 5584373[34]1293567 125 16821762[10]3809906 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=6821762[10]3809904
3410881[11]9048500 5584373[34]5103486 -682176[11]3809782 1 (1)B> 16821762[10]3809907 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=6821762[10]3809904, repcount=3410881[10]1904953, factor=3/2
5116322[11]8573265 1256484[35]3556176 124 11023264[11]5714860 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=1023264[11]5714859, V(2)=0
5116322[11]8573276 1256484[35]2130516 -102326[12]5714738 1 (1)B> 11023264[11]5714867 2
== Executing PA-CTR 10, V(1)=0, V(2)=1023264[11]5714864, repcount=5116322[10]2857433, factor=3/2
7674483[11]2860441 2827089[35]6516646 128 11534896[11]8572300 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=1534896[11]8572298
7674483[11]2860451 2827089[35]5088959 -153489[12]8572173 1 (1)B> 11534896[11]8572301 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=1534896[11]8572298, repcount=7674483[10]9286150, factor=3/2
1151172[12]9291201 6360950[35]7457759 127 12302344[11]7858451 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=2302344[11]7858450, V(2)=0
1151172[12]9291212 6360950[35]6750054 -230234[12]7858326 1 (1)B> 12302344[11]7858458 2
== Executing PA-CTR 10, V(1)=0, V(2)=2302344[11]7858455, repcount=1151172[11]8929228, factor=3/2
1726758[12]3937352 1431213[36]9956694 130 13453517[11]6787685 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=3453517[11]6787684, V(2)=0
1726758[12]3937361 1431213[36]3895147 -345351[12]6787557 1 (1)B> 13453517[11]6787690 2
== Executing PA-CTR 10, V(1)=0, V(2)=3453517[11]6787687, repcount=1726758[11]3393844, factor=3/2
2590138[12]0906581 3220231[36]7199291 131 15180276[11]0181533 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=5180276[11]0181532, V(2)=0
2590138[12]0906590 3220231[36]8106984 -518027[12]0181404 1 (1)B> 15180276[11]0181538 2
== Executing PA-CTR 10, V(1)=0, V(2)=5180276[11]0181535, repcount=2590138[11]0090768, factor=3/2
3885207[12]1360430 7245520[36]2175144 132 17770414[11]0272305 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=7770414[11]0272304, V(2)=0
3885207[12]1360439 7245520[36]3536697 -777041[12]0272175 1 (1)B> 17770414[11]0272310 2
== Executing PA-CTR 10, V(1)=0, V(2)=7770414[11]0272307, repcount=3885207[11]5136154, factor=3/2
5827810[12]7041209 1630242[37]2640841 133 11165562[12]5408463 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=1165562[12]5408462, V(2)=0
5827810[12]7041218 1630242[37]9683184 -116556[13]5408332 1 (1)B> 11165562[12]5408468 2
== Executing PA-CTR 10, V(1)=0, V(2)=1165562[12]5408465, repcount=5827810[11]2704233, factor=3/2
8741715[12]0562383 3668044[37]8843714 134 11748343[12]8112700 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=1748343[12]8112699, V(2)=0
8741715[12]0562392 3668044[37]9407242 -174834[13]8112568 1 (1)B> 11748343[12]8112705 2
== Executing PA-CTR 10, V(1)=0, V(2)=1748343[12]8112702, repcount=8741715[11]4056352, factor=3/2
1311257[13]0844152 8253100[37]7370890 136 12622514[12]2169057 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=2622514[12]2169055
1311257[13]0844162 8253100[37]9539960 -262251[13]2168922 1 (1)B> 12622514[12]2169058 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=2622514[12]2169055, repcount=1311257[12]6084528, factor=3/2
1966886[13]1266802 1856947[38]8451000 134 13933772[12]8253585 (1)B> 12 0 12 2
== Executing PPA-CTR 5 (once), V(1)=3933772[12]8253584
1966886[13]1266811 1856947[38]9718949 -393377[13]8253453 1 (1)B> 13933772[12]8253589 2 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=3933772[12]8253586, repcount=1966886[12]9126794, factor=3/2
2950329[13]6900781 4178132[38]1551093 135 15900658[12]7380383 (1)B> 1 2 12 2
== Executing PPA-CTR 6 (once), V(1)=5900658[12]7380381, V(2)=0
2950329[13]6900789 4178132[38]8931487 -590065[13]7380249 1 (1)B> 15900658[12]7380384 0 1 0 1 2
== Executing PA-CTR 2, V(1)=0, V(2)=5900658[12]7380381, repcount=2950329[12]3690191, factor=3/2
4425493[13]5351744 9400797[38]0912665 133 18850987[12]1070574 (1)B> 12 0 1 0 1 2
== Executing PPA-CTR 3 (once), V(1)=8850987[12]1070573
4425493[13]5351753 9400797[38]6265559 -885098[13]1070443 1 (1)B> 18850987[12]1070578 2 1 0 1 2
== Executing PA-CTR 2, V(1)=0, V(2)=8850987[12]1070575, repcount=4425493[12]5535288, factor=3/2
6638240[13]3028193 2115179[39]2146679 133 11327648[13]6605865 (1)B> 12 2 1 0 1 2
== Executing PPA-CTR 4 (once), V(1)=1327648[13]6605864, V(2)=0
6638240[13]3028210 2115179[39]5176042 -132764[14]6605734 1 (1)B> 11327648[13]6605872 0 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=1327648[13]6605869, repcount=6638240[12]3302935, factor=3/2
9957360[13]9542885 4759153[39]2496612 136 11991472[13]9908806 (1)B> 12 0 12 2
== Executing PPA-CTR 5 (once), V(1)=1991472[13]9908805
9957360[13]9542894 4759153[39]2040666 -199147[14]9908672 1 (1)B> 11991472[13]9908810 2 12 2
== Executing PA-CTR 1, V(1)=0, V(2)=1991472[13]9908807, repcount=9957360[12]9954404, factor=3/2
1493604[14]9314914 1070809[40]5464810 136 12987208[13]9863213 (1)B> 12 2 12 2
Lines: 500
Top steps: 499
Macro steps: 1493604130025095043699314914
Basic steps: 107080958266945009047565808606843399894171920385464810
Tape index: 136
nonzeros: 298720826005019008739863220
log10(nonzeros): 26.475
log10(steps ): 53.030
Some long numbers above are shortened: #(omitted digits) shown in "[]".
Input to awk program:
gohalt 1
nbs 3
T 4-state 3-symbol #b (T.J. & S. Ligocki)
: >1.1x10^713 >1.5x10^1426
5T 1RB 0LC 1RH 2LC 1RD 0LB 2LA 1LC 1LA 1RB 2LD 2RA
L 16
M 500
pref sim
machv Lig43_b just simple
machv Lig43_b-r with repetitions reduced
machv Lig43_b-1 with tape symbol exponents
machv Lig43_b-m as 1-bck-macro machine
machv Lig43_b-a as 1-bck-macro machine with pure additive config-TRs
iam Lig43_b-a
mtype 1 0
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:14:01 CEST 2010
edate Tue Jul 6 22:14:03 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:01 CEST 2010