Comment: This TM produces >6.9x10^4931 nonzeros in >2.5x10^9863 steps.
| State | on 0 |
on 1 |
on 2 |
on 3 |
on 4 |
on 5 |
on 0 | on 1 | on 2 | on 3 | on 4 | on 5 | ||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Move | Goto | Move | Goto | Move | Goto | Move | Goto | Move | Goto | Move | Goto | |||||||||||||
| A | 1RB | 1LB | 3RA | 4LA | 2LA | 4LB | 1 | right | B | 1 | left | B | 3 | right | A | 4 | left | A | 2 | left | A | 4 | left | B |
| B | 2LA | 2RB | 3LB | 1LA | 5RA | 1RH | 2 | left | A | 2 | right | B | 3 | left | B | 1 | left | A | 5 | right | A | 1 | right | H |
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 <B(1) 2
3 4 -2 <A(2) 1 2
4 11 -3 <A(1) 12 2
5 13 -1 1 (2)B> 12 2
6 15 1 1 22 (2)B> 2
7 17 -1 1 22 <B(3) 3
8 19 -3 1 <B(3) 33
9 24 -4 <A(1) 1 33
10 26 -2 1 (2)B> 1 33
11 27 -1 1 2 (2)B> 33
12 31 -3 1 2 <A(1) 1 32
13 34 -4 1 <A(1) 12 32
14 35 -5 <B(1) 13 32
15 36 -6 <A(2) 14 32
16 43 -7 <A(1) 15 32
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <A(1) 11+V(2) 32+V(1)
1 2 2 1 (2)B> 11+V(2) 32+V(1)
2 3+V(2) 3+V(2) 1 21+V(2) (2)B> 32+V(1)
3 7+V(2) 1+V(2) 1 21+V(2) <A(1) 1 31+V(1)
4 10+4*V(2) 0 1 <A(1) 12+V(2) 31+V(1)
5 11+4*V(2) -1 <B(1) 13+V(2) 31+V(1)
6 12+4*V(2) -2 <A(2) 14+V(2) 31+V(1)
7 19+4*V(2) -3 <A(1) 15+V(2) 31+V(1)
<< Success! ==> defined new CTR 1 (PA)
16 43 -7 <A(1) 15 32
== Executing PA-CTR 1, V(1)=0, V(2)=4, repcount=1, factor=4/1
23 78 -10 <A(1) 19 3
24 80 -8 1 (2)B> 19 3
25 89 1 1 29 (2)B> 3
26 93 -1 1 29 <A(1) 1
27 120 -10 1 <A(1) 110
28 121 -11 <B(1) 111
29 122 -12 <A(2) 112
30 129 -13 <A(1) 113
31 131 -11 1 (2)B> 113
32 144 2 1 213 (2)B>
33 147 3 1 213 3 (3)A>
34 148 4 1 213 32 (1)B>
35 150 2 1 213 32 <B(1) 2
36 151 1 1 213 3 <A(1) 1 2
37 152 0 1 213 <A(4) 12 2
38 191 -13 1 <A(4) 213 12 2
39 192 -14 <B(1) 4 213 12 2
40 193 -15 <A(2) 1 4 213 12 2
41 200 -16 <A(1) 12 4 213 12 2
42 202 -14 1 (2)B> 12 4 213 12 2
43 204 -12 1 22 (2)B> 4 213 12 2
44 205 -11 1 23 (5)A> 213 12 2
45 206 -10 1 23 5 (3)A> 212 12 2
46 218 2 1 23 5 312 (3)A> 12 2
47 220 0 1 23 5 312 <A(1) 12 2
48 221 -1 1 23 5 311 <A(4) 13 2
49 232 -12 1 23 5 <A(4) 411 13 2
50 233 -13 1 23 <B(4) 412 13 2
51 234 -14 1 22 <B(3) 413 13 2
52 236 -16 1 <B(3) 32 413 13 2
53 241 -17 <A(1) 1 32 413 13 2
54 243 -15 1 (2)B> 1 32 413 13 2
55 244 -14 1 2 (2)B> 32 413 13 2
56 248 -16 1 2 <A(1) 1 3 413 13 2
57 251 -17 1 <A(1) 12 3 413 13 2
58 252 -18 <B(1) 13 3 413 13 2
59 253 -19 <A(2) 14 3 413 13 2
60 260 -20 <A(1) 15 3 413 13 2
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <A(1) 11+V(2) 32+V(1) [*]* [*]* [*]*
1 2 2 1 (2)B> 11+V(2) 32+V(1) [*]* [*]* [*]*
2 3+V(2) 3+V(2) 1 21+V(2) (2)B> 32+V(1) [*]* [*]* [*]*
3 7+V(2) 1+V(2) 1 21+V(2) <A(1) 1 31+V(1) [*]* [*]* [*]*
4 10+4*V(2) 0 1 <A(1) 12+V(2) 31+V(1) [*]* [*]* [*]*
5 11+4*V(2) -1 <B(1) 13+V(2) 31+V(1) [*]* [*]* [*]*
6 12+4*V(2) -2 <A(2) 14+V(2) 31+V(1) [*]* [*]* [*]*
7 19+4*V(2) -3 <A(1) 15+V(2) 31+V(1) [*]* [*]* [*]*
<< Success! ==> defined new CTR 2 (PA)
61 262 -18 1 (2)B> 15 3 413 13 2
62 267 -13 1 25 (2)B> 3 413 13 2
63 271 -15 1 25 <A(1) 1 413 13 2
64 286 -20 1 <A(1) 16 413 13 2
65 287 -21 <B(1) 17 413 13 2
66 288 -22 <A(2) 18 413 13 2
67 295 -23 <A(1) 19 413 13 2
68 297 -21 1 (2)B> 19 413 13 2
69 306 -12 1 29 (2)B> 413 13 2
70 307 -11 1 210 (5)A> 412 13 2
71 309 -13 1 210 <B(4) 2 411 13 2
72 310 -14 1 29 <B(3) 4 2 411 13 2
73 319 -23 1 <B(3) 39 4 2 411 13 2
74 324 -24 <A(1) 1 39 4 2 411 13 2
75 326 -22 1 (2)B> 1 39 4 2 411 13 2
76 327 -21 1 2 (2)B> 39 4 2 411 13 2
77 331 -23 1 2 <A(1) 1 38 4 2 411 13 2
78 334 -24 1 <A(1) 12 38 4 2 411 13 2
79 335 -25 <B(1) 13 38 4 2 411 13 2
80 336 -26 <A(2) 14 38 4 2 411 13 2
81 343 -27 <A(1) 15 38 4 2 411 13 2
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <A(1) 11+V(2) 32+V(1) [*]* [*]* [*]* [*]* [*]*
1 2 2 1 (2)B> 11+V(2) 32+V(1) [*]* [*]* [*]* [*]* [*]*
2 3+V(2) 3+V(2) 1 21+V(2) (2)B> 32+V(1) [*]* [*]* [*]* [*]* [*]*
3 7+V(2) 1+V(2) 1 21+V(2) <A(1) 1 31+V(1) [*]* [*]* [*]* [*]* [*]*
4 10+4*V(2) 0 1 <A(1) 12+V(2) 31+V(1) [*]* [*]* [*]* [*]* [*]*
5 11+4*V(2) -1 <B(1) 13+V(2) 31+V(1) [*]* [*]* [*]* [*]* [*]*
6 12+4*V(2) -2 <A(2) 14+V(2) 31+V(1) [*]* [*]* [*]* [*]* [*]*
7 19+4*V(2) -3 <A(1) 15+V(2) 31+V(1) [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 3 (PA)
81 343 -27 <A(1) 15 38 4 2 411 13 2
== Executing PA-CTR 3, V(1)=6, V(2)=4, repcount=7, factor=4/1
130 924 -48 <A(1) 133 3 4 2 411 13 2
131 926 -46 1 (2)B> 133 3 4 2 411 13 2
132 959 -13 1 233 (2)B> 3 4 2 411 13 2
133 963 -15 1 233 <A(1) 1 4 2 411 13 2
134 1062 -48 1 <A(1) 134 4 2 411 13 2
135 1063 -49 <B(1) 135 4 2 411 13 2
136 1064 -50 <A(2) 136 4 2 411 13 2
137 1071 -51 <A(1) 137 4 2 411 13 2
138 1073 -49 1 (2)B> 137 4 2 411 13 2
139 1110 -12 1 237 (2)B> 4 2 411 13 2
140 1111 -11 1 238 (5)A> 2 411 13 2
141 1112 -10 1 238 5 (3)A> 411 13 2
142 1114 -12 1 238 5 <A(4) 2 410 13 2
143 1115 -13 1 238 <B(4) 4 2 410 13 2
144 1116 -14 1 237 <B(3) 42 2 410 13 2
145 1153 -51 1 <B(3) 337 42 2 410 13 2
146 1158 -52 <A(1) 1 337 42 2 410 13 2
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <A(1) 11+V(2) 3 4 2 42+V(1) [*]* [*]*
1 2 2 1 (2)B> 11+V(2) 3 4 2 42+V(1) [*]* [*]*
2 3+V(2) 3+V(2) 1 21+V(2) (2)B> 3 4 2 42+V(1) [*]* [*]*
3 7+V(2) 1+V(2) 1 21+V(2) <A(1) 1 4 2 42+V(1) [*]* [*]*
4 10+4*V(2) 0 1 <A(1) 12+V(2) 4 2 42+V(1) [*]* [*]*
5 11+4*V(2) -1 <B(1) 13+V(2) 4 2 42+V(1) [*]* [*]*
6 12+4*V(2) -2 <A(2) 14+V(2) 4 2 42+V(1) [*]* [*]*
7 19+4*V(2) -3 <A(1) 15+V(2) 4 2 42+V(1) [*]* [*]*
8 21+4*V(2) -1 1 (2)B> 15+V(2) 4 2 42+V(1) [*]* [*]*
9 26+5*V(2) 4+V(2) 1 25+V(2) (2)B> 4 2 42+V(1) [*]* [*]*
10 27+5*V(2) 5+V(2) 1 26+V(2) (5)A> 2 42+V(1) [*]* [*]*
11 28+5*V(2) 6+V(2) 1 26+V(2) 5 (3)A> 42+V(1) [*]* [*]*
12 30+5*V(2) 4+V(2) 1 26+V(2) 5 <A(4) 2 41+V(1) [*]* [*]*
13 31+5*V(2) 3+V(2) 1 26+V(2) <B(4) 4 2 41+V(1) [*]* [*]*
14 32+5*V(2) 2+V(2) 1 25+V(2) <B(3) 42 2 41+V(1) [*]* [*]*
15 37+6*V(2) -3 1 <B(3) 35+V(2) 42 2 41+V(1) [*]* [*]*
16 42+6*V(2) -4 <A(1) 1 35+V(2) 42 2 41+V(1) [*]* [*]*
<< Success! ==> defined new CTR 4 (PPA)
146 1158 -52 <A(1) 1 337 42 2 410 13 2
== Executing PA-CTR 3, V(1)=35, V(2)=0, repcount=36, factor=4/1
398 11922 -160 <A(1) 1145 3 42 2 410 13 2
399 11924 -158 1 (2)B> 1145 3 42 2 410 13 2
400 12069 -13 1 2145 (2)B> 3 42 2 410 13 2
401 12073 -15 1 2145 <A(1) 1 42 2 410 13 2
402 12508 -160 1 <A(1) 1146 42 2 410 13 2
403 12509 -161 <B(1) 1147 42 2 410 13 2
404 12510 -162 <A(2) 1148 42 2 410 13 2
405 12517 -163 <A(1) 1149 42 2 410 13 2
406 12519 -161 1 (2)B> 1149 42 2 410 13 2
407 12668 -12 1 2149 (2)B> 42 2 410 13 2
408 12669 -11 1 2150 (5)A> 4 2 410 13 2
409 12671 -13 1 2150 <B(4) 22 410 13 2
410 12672 -14 1 2149 <B(3) 4 22 410 13 2
411 12821 -163 1 <B(3) 3149 4 22 410 13 2
412 12826 -164 <A(1) 1 3149 4 22 410 13 2
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <A(1) 11+V(2) 3 42 21+V(1) [*]* [*]* [*]*
1 2 2 1 (2)B> 11+V(2) 3 42 21+V(1) [*]* [*]* [*]*
2 3+V(2) 3+V(2) 1 21+V(2) (2)B> 3 42 21+V(1) [*]* [*]* [*]*
3 7+V(2) 1+V(2) 1 21+V(2) <A(1) 1 42 21+V(1) [*]* [*]* [*]*
4 10+4*V(2) 0 1 <A(1) 12+V(2) 42 21+V(1) [*]* [*]* [*]*
5 11+4*V(2) -1 <B(1) 13+V(2) 42 21+V(1) [*]* [*]* [*]*
6 12+4*V(2) -2 <A(2) 14+V(2) 42 21+V(1) [*]* [*]* [*]*
7 19+4*V(2) -3 <A(1) 15+V(2) 42 21+V(1) [*]* [*]* [*]*
8 21+4*V(2) -1 1 (2)B> 15+V(2) 42 21+V(1) [*]* [*]* [*]*
9 26+5*V(2) 4+V(2) 1 25+V(2) (2)B> 42 21+V(1) [*]* [*]* [*]*
10 27+5*V(2) 5+V(2) 1 26+V(2) (5)A> 4 21+V(1) [*]* [*]* [*]*
11 29+5*V(2) 3+V(2) 1 26+V(2) <B(4) 22+V(1) [*]* [*]* [*]*
12 30+5*V(2) 2+V(2) 1 25+V(2) <B(3) 4 22+V(1) [*]* [*]* [*]*
13 35+6*V(2) -3 1 <B(3) 35+V(2) 4 22+V(1) [*]* [*]* [*]*
14 40+6*V(2) -4 <A(1) 1 35+V(2) 4 22+V(1) [*]* [*]* [*]*
<< Success! ==> defined new CTR 5 (PPA)
412 12826 -164 <A(1) 1 3149 4 22 410 13 2
== Executing PA-CTR 3, V(1)=147, V(2)=0, repcount=148, factor=4/1
1448 189686 -608 <A(1) 1593 3 4 22 410 13 2
1449 189688 -606 1 (2)B> 1593 3 4 22 410 13 2
1450 190281 -13 1 2593 (2)B> 3 4 22 410 13 2
1451 190285 -15 1 2593 <A(1) 1 4 22 410 13 2
1452 192064 -608 1 <A(1) 1594 4 22 410 13 2
1453 192065 -609 <B(1) 1595 4 22 410 13 2
1454 192066 -610 <A(2) 1596 4 22 410 13 2
1455 192073 -611 <A(1) 1597 4 22 410 13 2
1456 192075 -609 1 (2)B> 1597 4 22 410 13 2
1457 192672 -12 1 2597 (2)B> 4 22 410 13 2
1458 192673 -11 1 2598 (5)A> 22 410 13 2
1459 192674 -10 1 2598 5 (3)A> 2 410 13 2
1460 192675 -9 1 2598 5 3 (3)A> 410 13 2
1461 192677 -11 1 2598 5 3 <A(4) 2 49 13 2
1462 192678 -12 1 2598 5 <A(4) 4 2 49 13 2
1463 192679 -13 1 2598 <B(4) 42 2 49 13 2
1464 192680 -14 1 2597 <B(3) 43 2 49 13 2
1465 193277 -611 1 <B(3) 3597 43 2 49 13 2
1466 193282 -612 <A(1) 1 3597 43 2 49 13 2
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 <A(1) 11+V(3) 3 4 22+V(2) 42+V(1) [*]* [*]*
1 2 2 1 (2)B> 11+V(3) 3 4 22+V(2) 42+V(1) [*]* [*]*
2 3+V(3) 3+V(3) 1 21+V(3) (2)B> 3 4 22+V(2) 42+V(1) [*]* [*]*
3 7+V(3) 1+V(3) 1 21+V(3) <A(1) 1 4 22+V(2) 42+V(1) [*]* [*]*
4 10+4*V(3) 0 1 <A(1) 12+V(3) 4 22+V(2) 42+V(1) [*]* [*]*
5 11+4*V(3) -1 <B(1) 13+V(3) 4 22+V(2) 42+V(1) [*]* [*]*
6 12+4*V(3) -2 <A(2) 14+V(3) 4 22+V(2) 42+V(1) [*]* [*]*
7 19+4*V(3) -3 <A(1) 15+V(3) 4 22+V(2) 42+V(1) [*]* [*]*
8 21+4*V(3) -1 1 (2)B> 15+V(3) 4 22+V(2) 42+V(1) [*]* [*]*
9 26+5*V(3) 4+V(3) 1 25+V(3) (2)B> 4 22+V(2) 42+V(1) [*]* [*]*
10 27+5*V(3) 5+V(3) 1 26+V(3) (5)A> 22+V(2) 42+V(1) [*]* [*]*
11 28+5*V(3) 6+V(3) 1 26+V(3) 5 (3)A> 21+V(2) 42+V(1) [*]* [*]*
12 29+V(2)+5*V(3) 7+V(2)+V(3) 1 26+V(3) 5 31+V(2) (3)A> 42+V(1) [*]* [*]*
13 31+V(2)+5*V(3) 5+V(2)+V(3) 1 26+V(3) 5 31+V(2) <A(4) 2 41+V(1) [*]* [*]*
14 32+2*V(2)+5*V(3) 4+V(3) 1 26+V(3) 5 <A(4) 41+V(2) 2 41+V(1) [*]* [*]*
15 33+2*V(2)+5*V(3) 3+V(3) 1 26+V(3) <B(4) 42+V(2) 2 41+V(1) [*]* [*]*
16 34+2*V(2)+5*V(3) 2+V(3) 1 25+V(3) <B(3) 43+V(2) 2 41+V(1) [*]* [*]*
17 39+2*V(2)+6*V(3) -3 1 <B(3) 35+V(3) 43+V(2) 2 41+V(1) [*]* [*]*
18 44+2*V(2)+6*V(3) -4 <A(1) 1 35+V(3) 43+V(2) 2 41+V(1) [*]* [*]*
<< Success! ==> defined new CTR 6 (PPA)
1466 193282 -612 <A(1) 1 3597 43 2 49 13 2
== Executing PA-CTR 3, V(1)=595, V(2)=0, repcount=596, factor=4/1
5638 3041566 -2400 <A(1) 12385 3 43 2 49 13 2
5639 3041568 -2398 1 (2)B> 12385 3 43 2 49 13 2
5640 3043953 -13 1 22385 (2)B> 3 43 2 49 13 2
5641 3043957 -15 1 22385 <A(1) 1 43 2 49 13 2
5642 3051112 -2400 1 <A(1) 12386 43 2 49 13 2
5643 3051113 -2401 <B(1) 12387 43 2 49 13 2
5644 3051114 -2402 <A(2) 12388 43 2 49 13 2
5645 3051121 -2403 <A(1) 12389 43 2 49 13 2
5646 3051123 -2401 1 (2)B> 12389 43 2 49 13 2
5647 3053512 -12 1 22389 (2)B> 43 2 49 13 2
5648 3053513 -11 1 22390 (5)A> 42 2 49 13 2
5649 3053515 -13 1 22390 <B(4) 2 4 2 49 13 2
5650 3053516 -14 1 22389 <B(3) 4 2 4 2 49 13 2
5651 3055905 -2403 1 <B(3) 32389 4 2 4 2 49 13 2
5652 3055910 -2404 <A(1) 1 32389 4 2 4 2 49 13 2
5653 3055912 -2402 1 (2)B> 1 32389 4 2 4 2 49 13 2
5654 3055913 -2401 1 2 (2)B> 32389 4 2 4 2 49 13 2
5655 3055917 -2403 1 2 <A(1) 1 32388 4 2 4 2 49 13 2
5656 3055920 -2404 1 <A(1) 12 32388 4 2 4 2 49 13 2
5657 3055921 -2405 <B(1) 13 32388 4 2 4 2 49 13 2
5658 3055922 -2406 <A(2) 14 32388 4 2 4 2 49 13 2
5659 3055929 -2407 <A(1) 15 32388 4 2 4 2 49 13 2
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <A(1) 11+V(2) 32+V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]*
1 2 2 1 (2)B> 11+V(2) 32+V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]*
2 3+V(2) 3+V(2) 1 21+V(2) (2)B> 32+V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]*
3 7+V(2) 1+V(2) 1 21+V(2) <A(1) 1 31+V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]*
4 10+4*V(2) 0 1 <A(1) 12+V(2) 31+V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]*
5 11+4*V(2) -1 <B(1) 13+V(2) 31+V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]*
6 12+4*V(2) -2 <A(2) 14+V(2) 31+V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]*
7 19+4*V(2) -3 <A(1) 15+V(2) 31+V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 7 (PA)
5659 3055929 -2407 <A(1) 15 32388 4 2 4 2 49 13 2
== Executing PA-CTR 7, V(1)=2386, V(2)=4, repcount=2387, factor=4/1
22368 48702530 -9568 <A(1) 19553 3 4 2 4 2 49 13 2
22369 48702532 -9566 1 (2)B> 19553 3 4 2 4 2 49 13 2
22370 48712085 -13 1 29553 (2)B> 3 4 2 4 2 49 13 2
22371 48712089 -15 1 29553 <A(1) 1 4 2 4 2 49 13 2
22372 48740748 -9568 1 <A(1) 19554 4 2 4 2 49 13 2
22373 48740749 -9569 <B(1) 19555 4 2 4 2 49 13 2
22374 48740750 -9570 <A(2) 19556 4 2 4 2 49 13 2
22375 48740757 -9571 <A(1) 19557 4 2 4 2 49 13 2
22376 48740759 -9569 1 (2)B> 19557 4 2 4 2 49 13 2
22377 48750316 -12 1 29557 (2)B> 4 2 4 2 49 13 2
22378 48750317 -11 1 29558 (5)A> 2 4 2 49 13 2
22379 48750318 -10 1 29558 5 (3)A> 4 2 49 13 2
22380 48750320 -12 1 29558 5 <A(4) 22 49 13 2
22381 48750321 -13 1 29558 <B(4) 4 22 49 13 2
22382 48750322 -14 1 29557 <B(3) 42 22 49 13 2
22383 48759879 -9571 1 <B(3) 39557 42 22 49 13 2
22384 48759884 -9572 <A(1) 1 39557 42 22 49 13 2
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <A(1) 11+V(2) 3 4 2 4 21+V(1) [*]* [*]* [*]*
1 2 2 1 (2)B> 11+V(2) 3 4 2 4 21+V(1) [*]* [*]* [*]*
2 3+V(2) 3+V(2) 1 21+V(2) (2)B> 3 4 2 4 21+V(1) [*]* [*]* [*]*
3 7+V(2) 1+V(2) 1 21+V(2) <A(1) 1 4 2 4 21+V(1) [*]* [*]* [*]*
4 10+4*V(2) 0 1 <A(1) 12+V(2) 4 2 4 21+V(1) [*]* [*]* [*]*
5 11+4*V(2) -1 <B(1) 13+V(2) 4 2 4 21+V(1) [*]* [*]* [*]*
6 12+4*V(2) -2 <A(2) 14+V(2) 4 2 4 21+V(1) [*]* [*]* [*]*
7 19+4*V(2) -3 <A(1) 15+V(2) 4 2 4 21+V(1) [*]* [*]* [*]*
8 21+4*V(2) -1 1 (2)B> 15+V(2) 4 2 4 21+V(1) [*]* [*]* [*]*
9 26+5*V(2) 4+V(2) 1 25+V(2) (2)B> 4 2 4 21+V(1) [*]* [*]* [*]*
10 27+5*V(2) 5+V(2) 1 26+V(2) (5)A> 2 4 21+V(1) [*]* [*]* [*]*
11 28+5*V(2) 6+V(2) 1 26+V(2) 5 (3)A> 4 21+V(1) [*]* [*]* [*]*
12 30+5*V(2) 4+V(2) 1 26+V(2) 5 <A(4) 22+V(1) [*]* [*]* [*]*
13 31+5*V(2) 3+V(2) 1 26+V(2) <B(4) 4 22+V(1) [*]* [*]* [*]*
14 32+5*V(2) 2+V(2) 1 25+V(2) <B(3) 42 22+V(1) [*]* [*]* [*]*
15 37+6*V(2) -3 1 <B(3) 35+V(2) 42 22+V(1) [*]* [*]* [*]*
16 42+6*V(2) -4 <A(1) 1 35+V(2) 42 22+V(1) [*]* [*]* [*]*
<< Success! ==> defined new CTR 8 (PPA)
22384 48759884 -9572 <A(1) 1 39557 42 22 49 13 2
== Executing PA-CTR 3, V(1)=9555, V(2)=0, repcount=9556, factor=4/1
89276 779402088 -38240 <A(1) 138225 3 42 22 49 13 2
== Executing PPA-CTR 5 (once), V(1)=1, V(2)=38224
89290 779631472 -38244 <A(1) 1 338229 4 23 49 13 2
== Executing PA-CTR 3, V(1)=38227, V(2)=0, repcount=38228, factor=4/1
356886 12471091852 -152928 <A(1) 1152913 3 4 23 49 13 2
== Executing PPA-CTR 6 (once), V(1)=7, V(2)=1, V(3)=152912
356904 12472009370 -152932 <A(1) 1 3152917 44 2 48 13 2
== Executing PA-CTR 3, V(1)=152915, V(2)=0, repcount=152916, factor=4/1
1427316 199540115894 -611680 <A(1) 1611665 3 44 2 48 13 2
1427317 199540115896 -611678 1 (2)B> 1611665 3 44 2 48 13 2
1427318 199540727561 -13 1 2611665 (2)B> 3 44 2 48 13 2
1427319 199540727565 -15 1 2611665 <A(1) 1 44 2 48 13 2
1427320 199542562560 -611680 1 <A(1) 1611666 44 2 48 13 2
1427321 199542562561 -611681 <B(1) 1611667 44 2 48 13 2
1427322 199542562562 -611682 <A(2) 1611668 44 2 48 13 2
1427323 199542562569 -611683 <A(1) 1611669 44 2 48 13 2
1427324 199542562571 -611681 1 (2)B> 1611669 44 2 48 13 2
1427325 199543174240 -12 1 2611669 (2)B> 44 2 48 13 2
1427326 199543174241 -11 1 2611670 (5)A> 43 2 48 13 2
1427327 199543174243 -13 1 2611670 <B(4) 2 42 2 48 13 2
1427328 199543174244 -14 1 2611669 <B(3) 4 2 42 2 48 13 2
1427329 199543785913 -611683 1 <B(3) 3611669 4 2 42 2 48 13 2
1427330 199543785918 -611684 <A(1) 1 3611669 4 2 42 2 48 13 2
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <A(1) 11+V(2) 3 43+V(1) [*]* [*]* [*]* [*]*
1 2 2 1 (2)B> 11+V(2) 3 43+V(1) [*]* [*]* [*]* [*]*
2 3+V(2) 3+V(2) 1 21+V(2) (2)B> 3 43+V(1) [*]* [*]* [*]* [*]*
3 7+V(2) 1+V(2) 1 21+V(2) <A(1) 1 43+V(1) [*]* [*]* [*]* [*]*
4 10+4*V(2) 0 1 <A(1) 12+V(2) 43+V(1) [*]* [*]* [*]* [*]*
5 11+4*V(2) -1 <B(1) 13+V(2) 43+V(1) [*]* [*]* [*]* [*]*
6 12+4*V(2) -2 <A(2) 14+V(2) 43+V(1) [*]* [*]* [*]* [*]*
7 19+4*V(2) -3 <A(1) 15+V(2) 43+V(1) [*]* [*]* [*]* [*]*
8 21+4*V(2) -1 1 (2)B> 15+V(2) 43+V(1) [*]* [*]* [*]* [*]*
9 26+5*V(2) 4+V(2) 1 25+V(2) (2)B> 43+V(1) [*]* [*]* [*]* [*]*
10 27+5*V(2) 5+V(2) 1 26+V(2) (5)A> 42+V(1) [*]* [*]* [*]* [*]*
11 29+5*V(2) 3+V(2) 1 26+V(2) <B(4) 2 41+V(1) [*]* [*]* [*]* [*]*
12 30+5*V(2) 2+V(2) 1 25+V(2) <B(3) 4 2 41+V(1) [*]* [*]* [*]* [*]*
13 35+6*V(2) -3 1 <B(3) 35+V(2) 4 2 41+V(1) [*]* [*]* [*]* [*]*
14 40+6*V(2) -4 <A(1) 1 35+V(2) 4 2 41+V(1) [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 9 (PPA)
1427330 199543785918 -611684 <A(1) 1 3611669 4 2 42 2 48 13 2
== Executing PA-CTR 7, V(1)=611667, V(2)=0, repcount=611668, factor=4/1
5709006 3192652452058 -2446688 <A(1) 12446673 3 4 2 42 2 48 13 2
5709007 3192652452060 -2446686 1 (2)B> 12446673 3 4 2 42 2 48 13 2
5709008 3192654898733 -13 1 22446673 (2)B> 3 4 2 42 2 48 13 2
5709009 3192654898737 -15 1 22446673 <A(1) 1 4 2 42 2 48 13 2
5709010 3192662238756 -2446688 1 <A(1) 12446674 4 2 42 2 48 13 2
5709011 3192662238757 -2446689 <B(1) 12446675 4 2 42 2 48 13 2
5709012 3192662238758 -2446690 <A(2) 12446676 4 2 42 2 48 13 2
5709013 3192662238765 -2446691 <A(1) 12446677 4 2 42 2 48 13 2
5709014 3192662238767 -2446689 1 (2)B> 12446677 4 2 42 2 48 13 2
5709015 3192664685444 -12 1 22446677 (2)B> 4 2 42 2 48 13 2
5709016 3192664685445 -11 1 22446678 (5)A> 2 42 2 48 13 2
5709017 3192664685446 -10 1 22446678 5 (3)A> 42 2 48 13 2
5709018 3192664685448 -12 1 22446678 5 <A(4) 2 4 2 48 13 2
5709019 3192664685449 -13 1 22446678 <B(4) 4 2 4 2 48 13 2
5709020 3192664685450 -14 1 22446677 <B(3) 42 2 4 2 48 13 2
5709021 3192667132127 -2446691 1 <B(3) 32446677 42 2 4 2 48 13 2
5709022 3192667132132 -2446692 <A(1) 1 32446677 42 2 4 2 48 13 2
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <A(1) 11+V(2) 3 4 2 42+V(1) [*]* [*]* [*]* [*]*
1 2 2 1 (2)B> 11+V(2) 3 4 2 42+V(1) [*]* [*]* [*]* [*]*
2 3+V(2) 3+V(2) 1 21+V(2) (2)B> 3 4 2 42+V(1) [*]* [*]* [*]* [*]*
3 7+V(2) 1+V(2) 1 21+V(2) <A(1) 1 4 2 42+V(1) [*]* [*]* [*]* [*]*
4 10+4*V(2) 0 1 <A(1) 12+V(2) 4 2 42+V(1) [*]* [*]* [*]* [*]*
5 11+4*V(2) -1 <B(1) 13+V(2) 4 2 42+V(1) [*]* [*]* [*]* [*]*
6 12+4*V(2) -2 <A(2) 14+V(2) 4 2 42+V(1) [*]* [*]* [*]* [*]*
7 19+4*V(2) -3 <A(1) 15+V(2) 4 2 42+V(1) [*]* [*]* [*]* [*]*
8 21+4*V(2) -1 1 (2)B> 15+V(2) 4 2 42+V(1) [*]* [*]* [*]* [*]*
9 26+5*V(2) 4+V(2) 1 25+V(2) (2)B> 4 2 42+V(1) [*]* [*]* [*]* [*]*
10 27+5*V(2) 5+V(2) 1 26+V(2) (5)A> 2 42+V(1) [*]* [*]* [*]* [*]*
11 28+5*V(2) 6+V(2) 1 26+V(2) 5 (3)A> 42+V(1) [*]* [*]* [*]* [*]*
12 30+5*V(2) 4+V(2) 1 26+V(2) 5 <A(4) 2 41+V(1) [*]* [*]* [*]* [*]*
13 31+5*V(2) 3+V(2) 1 26+V(2) <B(4) 4 2 41+V(1) [*]* [*]* [*]* [*]*
14 32+5*V(2) 2+V(2) 1 25+V(2) <B(3) 42 2 41+V(1) [*]* [*]* [*]* [*]*
15 37+6*V(2) -3 1 <B(3) 35+V(2) 42 2 41+V(1) [*]* [*]* [*]* [*]*
16 42+6*V(2) -4 <A(1) 1 35+V(2) 42 2 41+V(1) [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 10 (PPA)
5709022 3192667132132 -2446692 <A(1) 1 32446677 42 2 4 2 48 13 2
== Executing PA-CTR 7, V(1)=2446675, V(2)=0, repcount=2446676, factor=4/1
22835754 51082481637376 -9786720 <A(1) 19786705 3 42 2 4 2 48 13 2
22835755 51082481637378 -9786718 1 (2)B> 19786705 3 42 2 4 2 48 13 2
22835756 51082491424083 -13 1 29786705 (2)B> 3 42 2 4 2 48 13 2
22835757 51082491424087 -15 1 29786705 <A(1) 1 42 2 4 2 48 13 2
22835758 51082520784202 -9786720 1 <A(1) 19786706 42 2 4 2 48 13 2
22835759 51082520784203 -9786721 <B(1) 19786707 42 2 4 2 48 13 2
22835760 51082520784204 -9786722 <A(2) 19786708 42 2 4 2 48 13 2
22835761 51082520784211 -9786723 <A(1) 19786709 42 2 4 2 48 13 2
22835762 51082520784213 -9786721 1 (2)B> 19786709 42 2 4 2 48 13 2
22835763 51082530570922 -12 1 29786709 (2)B> 42 2 4 2 48 13 2
22835764 51082530570923 -11 1 29786710 (5)A> 4 2 4 2 48 13 2
22835765 51082530570925 -13 1 29786710 <B(4) 22 4 2 48 13 2
22835766 51082530570926 -14 1 29786709 <B(3) 4 22 4 2 48 13 2
22835767 51082540357635 -9786723 1 <B(3) 39786709 4 22 4 2 48 13 2
22835768 51082540357640 -9786724 <A(1) 1 39786709 4 22 4 2 48 13 2
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <A(1) 11+V(2) 3 42 21+V(1) [*]* [*]* [*]* [*]* [*]*
1 2 2 1 (2)B> 11+V(2) 3 42 21+V(1) [*]* [*]* [*]* [*]* [*]*
2 3+V(2) 3+V(2) 1 21+V(2) (2)B> 3 42 21+V(1) [*]* [*]* [*]* [*]* [*]*
3 7+V(2) 1+V(2) 1 21+V(2) <A(1) 1 42 21+V(1) [*]* [*]* [*]* [*]* [*]*
4 10+4*V(2) 0 1 <A(1) 12+V(2) 42 21+V(1) [*]* [*]* [*]* [*]* [*]*
5 11+4*V(2) -1 <B(1) 13+V(2) 42 21+V(1) [*]* [*]* [*]* [*]* [*]*
6 12+4*V(2) -2 <A(2) 14+V(2) 42 21+V(1) [*]* [*]* [*]* [*]* [*]*
7 19+4*V(2) -3 <A(1) 15+V(2) 42 21+V(1) [*]* [*]* [*]* [*]* [*]*
8 21+4*V(2) -1 1 (2)B> 15+V(2) 42 21+V(1) [*]* [*]* [*]* [*]* [*]*
9 26+5*V(2) 4+V(2) 1 25+V(2) (2)B> 42 21+V(1) [*]* [*]* [*]* [*]* [*]*
10 27+5*V(2) 5+V(2) 1 26+V(2) (5)A> 4 21+V(1) [*]* [*]* [*]* [*]* [*]*
11 29+5*V(2) 3+V(2) 1 26+V(2) <B(4) 22+V(1) [*]* [*]* [*]* [*]* [*]*
12 30+5*V(2) 2+V(2) 1 25+V(2) <B(3) 4 22+V(1) [*]* [*]* [*]* [*]* [*]*
13 35+6*V(2) -3 1 <B(3) 35+V(2) 4 22+V(1) [*]* [*]* [*]* [*]* [*]*
14 40+6*V(2) -4 <A(1) 1 35+V(2) 4 22+V(1) [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 11 (PPA)
22835768 51082540357640 -9786724 <A(1) 1 39786709 4 22 4 2 48 13 2
== Executing PA-CTR 7, V(1)=9786707, V(2)=0, repcount=9786708, factor=4/1
91342724 817319875829540 -39146848 <A(1) 139146833 3 4 22 4 2 48 13 2
91342725 817319875829542 -39146846 1 (2)B> 139146833 3 4 22 4 2 48 13 2
91342726 817319914976375 -13 1 239146833 (2)B> 3 4 22 4 2 48 13 2
91342727 817319914976379 -15 1 239146833 <A(1) 1 4 22 4 2 48 13 2
91342728 817320032416878 -39146848 1 <A(1) 139146834 4 22 4 2 48 13 2
91342729 817320032416879 -39146849 <B(1) 139146835 4 22 4 2 48 13 2
91342730 817320032416880 -39146850 <A(2) 139146836 4 22 4 2 48 13 2
91342731 817320032416887 -39146851 <A(1) 139146837 4 22 4 2 48 13 2
91342732 817320032416889 -39146849 1 (2)B> 139146837 4 22 4 2 48 13 2
91342733 817320071563726 -12 1 239146837 (2)B> 4 22 4 2 48 13 2
91342734 817320071563727 -11 1 239146838 (5)A> 22 4 2 48 13 2
91342735 817320071563728 -10 1 239146838 5 (3)A> 2 4 2 48 13 2
91342736 817320071563729 -9 1 239146838 5 3 (3)A> 4 2 48 13 2
91342737 817320071563731 -11 1 239146838 5 3 <A(4) 22 48 13 2
91342738 817320071563732 -12 1 239146838 5 <A(4) 4 22 48 13 2
91342739 817320071563733 -13 1 239146838 <B(4) 42 22 48 13 2
91342740 817320071563734 -14 1 239146837 <B(3) 43 22 48 13 2
91342741 817320110710571 -39146851 1 <B(3) 339146837 43 22 48 13 2
91342742 817320110710576 -39146852 <A(1) 1 339146837 43 22 48 13 2
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 <A(1) 11+V(3) 3 4 22+V(2) 4 21+V(1) [*]* [*]* [*]*
1 2 2 1 (2)B> 11+V(3) 3 4 22+V(2) 4 21+V(1) [*]* [*]* [*]*
2 3+V(3) 3+V(3) 1 21+V(3) (2)B> 3 4 22+V(2) 4 21+V(1) [*]* [*]* [*]*
3 7+V(3) 1+V(3) 1 21+V(3) <A(1) 1 4 22+V(2) 4 21+V(1) [*]* [*]* [*]*
4 10+4*V(3) 0 1 <A(1) 12+V(3) 4 22+V(2) 4 21+V(1) [*]* [*]* [*]*
5 11+4*V(3) -1 <B(1) 13+V(3) 4 22+V(2) 4 21+V(1) [*]* [*]* [*]*
6 12+4*V(3) -2 <A(2) 14+V(3) 4 22+V(2) 4 21+V(1) [*]* [*]* [*]*
7 19+4*V(3) -3 <A(1) 15+V(3) 4 22+V(2) 4 21+V(1) [*]* [*]* [*]*
8 21+4*V(3) -1 1 (2)B> 15+V(3) 4 22+V(2) 4 21+V(1) [*]* [*]* [*]*
9 26+5*V(3) 4+V(3) 1 25+V(3) (2)B> 4 22+V(2) 4 21+V(1) [*]* [*]* [*]*
10 27+5*V(3) 5+V(3) 1 26+V(3) (5)A> 22+V(2) 4 21+V(1) [*]* [*]* [*]*
11 28+5*V(3) 6+V(3) 1 26+V(3) 5 (3)A> 21+V(2) 4 21+V(1) [*]* [*]* [*]*
12 29+V(2)+5*V(3) 7+V(2)+V(3) 1 26+V(3) 5 31+V(2) (3)A> 4 21+V(1) [*]* [*]* [*]*
13 31+V(2)+5*V(3) 5+V(2)+V(3) 1 26+V(3) 5 31+V(2) <A(4) 22+V(1) [*]* [*]* [*]*
14 32+2*V(2)+5*V(3) 4+V(3) 1 26+V(3) 5 <A(4) 41+V(2) 22+V(1) [*]* [*]* [*]*
15 33+2*V(2)+5*V(3) 3+V(3) 1 26+V(3) <B(4) 42+V(2) 22+V(1) [*]* [*]* [*]*
16 34+2*V(2)+5*V(3) 2+V(3) 1 25+V(3) <B(3) 43+V(2) 22+V(1) [*]* [*]* [*]*
17 39+2*V(2)+6*V(3) -3 1 <B(3) 35+V(3) 43+V(2) 22+V(1) [*]* [*]* [*]*
18 44+2*V(2)+6*V(3) -4 <A(1) 1 35+V(3) 43+V(2) 22+V(1) [*]* [*]* [*]*
<< Success! ==> defined new CTR 12 (PPA)
91342742 817320110710576 -39146852 <A(1) 1 339146837 43 22 48 13 2
== Executing PA-CTR 3, V(1)=39146835, V(2)=0, repcount=39146836, factor=4/1
365370594 13077118691812940 -156587360 <A(1) 1156587345 3 43 22 48 13 2
== Executing PPA-CTR 9 (once), V(1)=0, V(2)=156587344
365370608 13077119631337044 -156587364 <A(1) 1 3156587349 4 2 4 22 48 13 2
== Executing PA-CTR 7, V(1)=156587347, V(2)=0, repcount=156587348, factor=4/1
1461482044 2092339[4]3182704 -626349408 <A(1) 1626349393 3 4 2 4 22 48 13 2
== Executing PPA-CTR 8 (once), V(1)=1, V(2)=626349392
1461482060 2092339[4]1279098 -626349412 <A(1) 1 3626349397 42 23 48 13 2
== Executing PA-CTR 3, V(1)=626349395, V(2)=0, repcount=626349396, factor=4/1
5845927832 3347742[5]7640982 -2505397600 <A(1) 12505397585 3 42 23 48 13 2
== Executing PPA-CTR 5 (once), V(1)=2, V(2)=2505397584
5845927846 3347742[5]0026526 -2505397604 <A(1) 1 32505397589 4 24 48 13 2
== Executing PA-CTR 3, V(1)=2505397587, V(2)=0, repcount=2505397588, factor=4/1
23383710962 5356387[6]9141946 -10021590368 <A(1) 110021590353 3 4 24 48 13 2
== Executing PPA-CTR 6 (once), V(1)=6, V(2)=2, V(3)=10021590352
23383710980 5356387[6]8684106 -10021590372 <A(1) 1 310021590357 45 2 47 13 2
== Executing PA-CTR 3, V(1)=10021590355, V(2)=0, repcount=10021590356, factor=4/1
93534843472 8570220[7]3831910 -40086361440 <A(1) 140086361425 3 45 2 47 13 2
== Executing PPA-CTR 9 (once), V(1)=2, V(2)=40086361424
93534843486 8570220[7]2000494 -40086361444 <A(1) 1 340086361429 4 2 43 2 47 13 2
== Executing PA-CTR 7, V(1)=40086361427, V(2)=0, repcount=40086361428, factor=4/1
374139373482 1371235[9]1569674 -160345445728 <A(1) 1160345445713 3 4 2 43 2 47 13 2
== Executing PPA-CTR 10 (once), V(1)=1, V(2)=160345445712
374139373498 1371235[9]4243988 -160345445732 <A(1) 1 3160345445717 42 2 42 2 47 13 2
== Executing PA-CTR 7, V(1)=160345445715, V(2)=0, repcount=160345445716, factor=4/1
1496557493510 2193976[10]6168112 -641381782880 <A(1) 1641381782865 3 42 2 42 2 47 13 2
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=641381782864
1496557493524 2193976[10]6865336 -641381782884 <A(1) 1 3641381782869 4 22 42 2 47 13 2
== Executing PA-CTR 7, V(1)=641381782867, V(2)=0, repcount=641381782868, factor=4/1
5986229973600 3510362[11]2920276 -2565527131488 <A(1) 12565527131473 3 4 22 42 2 47 13 2
5986229973601 3510362[11]2920278 -2565527131486 1 (2)B> 12565527131473 3 4 22 42 2 47 13 2
5986229973602 3510362[11]0051751 -13 1 22565527131473 (2)B> 3 4 22 42 2 47 13 2
5986229973603 3510362[11]0051755 -15 1 22565527131473 <A(1) 1 4 22 42 2 47 13 2
5986229973604 3510362[11]1446174 -2565527131488 1 <A(1) 12565527131474 4 22 42 2 47 13 2
5986229973605 3510362[11]1446175 -2565527131489 <B(1) 12565527131475 4 22 42 2 47 13 2
5986229973606 3510362[11]1446176 -2565527131490 <A(2) 12565527131476 4 22 42 2 47 13 2
5986229973607 3510362[11]1446183 -2565527131491 <A(1) 12565527131477 4 22 42 2 47 13 2
5986229973608 3510362[11]1446185 -2565527131489 1 (2)B> 12565527131477 4 22 42 2 47 13 2
5986229973609 3510362[11]8577662 -12 1 22565527131477 (2)B> 4 22 42 2 47 13 2
5986229973610 3510362[11]8577663 -11 1 22565527131478 (5)A> 22 42 2 47 13 2
5986229973611 3510362[11]8577664 -10 1 22565527131478 5 (3)A> 2 42 2 47 13 2
5986229973612 3510362[11]8577665 -9 1 22565527131478 5 3 (3)A> 42 2 47 13 2
5986229973613 3510362[11]8577667 -11 1 22565527131478 5 3 <A(4) 2 4 2 47 13 2
5986229973614 3510362[11]8577668 -12 1 22565527131478 5 <A(4) 4 2 4 2 47 13 2
5986229973615 3510362[11]8577669 -13 1 22565527131478 <B(4) 42 2 4 2 47 13 2
5986229973616 3510362[11]8577670 -14 1 22565527131477 <B(3) 43 2 4 2 47 13 2
5986229973617 3510362[11]5709147 -2565527131491 1 <B(3) 32565527131477 43 2 4 2 47 13 2
5986229973618 3510362[11]5709152 -2565527131492 <A(1) 1 32565527131477 43 2 4 2 47 13 2
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 <A(1) 11+V(3) 3 4 22+V(2) 42+V(1) [*]* [*]* [*]* [*]*
1 2 2 1 (2)B> 11+V(3) 3 4 22+V(2) 42+V(1) [*]* [*]* [*]* [*]*
2 3+V(3) 3+V(3) 1 21+V(3) (2)B> 3 4 22+V(2) 42+V(1) [*]* [*]* [*]* [*]*
3 7+V(3) 1+V(3) 1 21+V(3) <A(1) 1 4 22+V(2) 42+V(1) [*]* [*]* [*]* [*]*
4 10+4*V(3) 0 1 <A(1) 12+V(3) 4 22+V(2) 42+V(1) [*]* [*]* [*]* [*]*
5 11+4*V(3) -1 <B(1) 13+V(3) 4 22+V(2) 42+V(1) [*]* [*]* [*]* [*]*
6 12+4*V(3) -2 <A(2) 14+V(3) 4 22+V(2) 42+V(1) [*]* [*]* [*]* [*]*
7 19+4*V(3) -3 <A(1) 15+V(3) 4 22+V(2) 42+V(1) [*]* [*]* [*]* [*]*
8 21+4*V(3) -1 1 (2)B> 15+V(3) 4 22+V(2) 42+V(1) [*]* [*]* [*]* [*]*
9 26+5*V(3) 4+V(3) 1 25+V(3) (2)B> 4 22+V(2) 42+V(1) [*]* [*]* [*]* [*]*
10 27+5*V(3) 5+V(3) 1 26+V(3) (5)A> 22+V(2) 42+V(1) [*]* [*]* [*]* [*]*
11 28+5*V(3) 6+V(3) 1 26+V(3) 5 (3)A> 21+V(2) 42+V(1) [*]* [*]* [*]* [*]*
12 29+V(2)+5*V(3) 7+V(2)+V(3) 1 26+V(3) 5 31+V(2) (3)A> 42+V(1) [*]* [*]* [*]* [*]*
13 31+V(2)+5*V(3) 5+V(2)+V(3) 1 26+V(3) 5 31+V(2) <A(4) 2 41+V(1) [*]* [*]* [*]* [*]*
14 32+2*V(2)+5*V(3) 4+V(3) 1 26+V(3) 5 <A(4) 41+V(2) 2 41+V(1) [*]* [*]* [*]* [*]*
15 33+2*V(2)+5*V(3) 3+V(3) 1 26+V(3) <B(4) 42+V(2) 2 41+V(1) [*]* [*]* [*]* [*]*
16 34+2*V(2)+5*V(3) 2+V(3) 1 25+V(3) <B(3) 43+V(2) 2 41+V(1) [*]* [*]* [*]* [*]*
17 39+2*V(2)+6*V(3) -3 1 <B(3) 35+V(3) 43+V(2) 2 41+V(1) [*]* [*]* [*]* [*]*
18 44+2*V(2)+6*V(3) -4 <A(1) 1 35+V(3) 43+V(2) 2 41+V(1) [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 13 (PPA)
5986229973618 3510362[11]5709152 -2565527131492 <A(1) 1 32565527131477 43 2 4 2 47 13 2
== Executing PA-CTR 7, V(1)=2565527131475, V(2)=0, repcount=2565527131476, factor=4/1
23944919893950 5616579[12]3663996 -10262108525920 <A(1) 110262108525905 3 43 2 4 2 47 13 2
23944919893951 5616579[12]3663998 -10262108525918 1 (2)B> 110262108525905 3 43 2 4 2 47 13 2
23944919893952 5616579[12]2189903 -13 1 210262108525905 (2)B> 3 43 2 4 2 47 13 2
23944919893953 5616579[12]2189907 -15 1 210262108525905 <A(1) 1 43 2 4 2 47 13 2
23944919893954 5616579[12]7767622 -10262108525920 1 <A(1) 110262108525906 43 2 4 2 47 13 2
23944919893955 5616579[12]7767623 -10262108525921 <B(1) 110262108525907 43 2 4 2 47 13 2
23944919893956 5616579[12]7767624 -10262108525922 <A(2) 110262108525908 43 2 4 2 47 13 2
23944919893957 5616579[12]7767631 -10262108525923 <A(1) 110262108525909 43 2 4 2 47 13 2
23944919893958 5616579[12]7767633 -10262108525921 1 (2)B> 110262108525909 43 2 4 2 47 13 2
23944919893959 5616579[12]6293542 -12 1 210262108525909 (2)B> 43 2 4 2 47 13 2
23944919893960 5616579[12]6293543 -11 1 210262108525910 (5)A> 42 2 4 2 47 13 2
23944919893961 5616579[12]6293545 -13 1 210262108525910 <B(4) 2 4 2 4 2 47 13 2
23944919893962 5616579[12]6293546 -14 1 210262108525909 <B(3) 4 2 4 2 4 2 47 13 2
23944919893963 5616579[12]4819455 -10262108525923 1 <B(3) 310262108525909 4 2 4 2 4 2 47 13 2
23944919893964 5616579[12]4819460 -10262108525924 <A(1) 1 310262108525909 4 2 4 2 4 2 47 13 2
23944919893965 5616579[12]4819462 -10262108525922 1 (2)B> 1 310262108525909 4 2 4 2 4 2 47 13 2
23944919893966 5616579[12]4819463 -10262108525921 1 2 (2)B> 310262108525909 4 2 4 2 4 2 47 13 2
23944919893967 5616579[12]4819467 -10262108525923 1 2 <A(1) 1 310262108525908 4 2 4 2 4 2 47 13 2
23944919893968 5616579[12]4819470 -10262108525924 1 <A(1) 12 310262108525908 4 2 4 2 4 2 47 13 2
23944919893969 5616579[12]4819471 -10262108525925 <B(1) 13 310262108525908 4 2 4 2 4 2 47 13 2
23944919893970 5616579[12]4819472 -10262108525926 <A(2) 14 310262108525908 4 2 4 2 4 2 47 13 2
23944919893971 5616579[12]4819479 -10262108525927 <A(1) 15 310262108525908 4 2 4 2 4 2 47 13 2
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <A(1) 11+V(2) 32+V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]*
1 2 2 1 (2)B> 11+V(2) 32+V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]*
2 3+V(2) 3+V(2) 1 21+V(2) (2)B> 32+V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]*
3 7+V(2) 1+V(2) 1 21+V(2) <A(1) 1 31+V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]*
4 10+4*V(2) 0 1 <A(1) 12+V(2) 31+V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]*
5 11+4*V(2) -1 <B(1) 13+V(2) 31+V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]*
6 12+4*V(2) -2 <A(2) 14+V(2) 31+V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]*
7 19+4*V(2) -3 <A(1) 15+V(2) 31+V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 14 (PA)
23944919893971 5616579[12]4819479 -10262108525927 <A(1) 15 310262108525908 4 2 4 2 4 2 47 13 2
== Executing PA-CTR 14, V(1)=10262108525906, V(2)=4, repcount=10262108525907, factor=4/1
95779679575320 8986527[13]6400160 -41048434103648 <A(1) 141048434103633 3 4 2 4 2 4 2 47 13 2
95779679575321 8986527[13]6400162 -41048434103646 1 (2)B> 141048434103633 3 4 2 4 2 4 2 47 13 2
95779679575322 8986527[13]0503795 -13 1 241048434103633 (2)B> 3 4 2 4 2 4 2 47 13 2
95779679575323 8986527[13]0503799 -15 1 241048434103633 <A(1) 1 4 2 4 2 4 2 47 13 2
95779679575324 8986527[13]2814698 -41048434103648 1 <A(1) 141048434103634 4 2 4 2 4 2 47 13 2
95779679575325 8986527[13]2814699 -41048434103649 <B(1) 141048434103635 4 2 4 2 4 2 47 13 2
95779679575326 8986527[13]2814700 -41048434103650 <A(2) 141048434103636 4 2 4 2 4 2 47 13 2
95779679575327 8986527[13]2814707 -41048434103651 <A(1) 141048434103637 4 2 4 2 4 2 47 13 2
95779679575328 8986527[13]2814709 -41048434103649 1 (2)B> 141048434103637 4 2 4 2 4 2 47 13 2
95779679575329 8986527[13]6918346 -12 1 241048434103637 (2)B> 4 2 4 2 4 2 47 13 2
95779679575330 8986527[13]6918347 -11 1 241048434103638 (5)A> 2 4 2 4 2 47 13 2
95779679575331 8986527[13]6918348 -10 1 241048434103638 5 (3)A> 4 2 4 2 47 13 2
95779679575332 8986527[13]6918350 -12 1 241048434103638 5 <A(4) 22 4 2 47 13 2
95779679575333 8986527[13]6918351 -13 1 241048434103638 <B(4) 4 22 4 2 47 13 2
95779679575334 8986527[13]6918352 -14 1 241048434103637 <B(3) 42 22 4 2 47 13 2
95779679575335 8986527[13]1021989 -41048434103651 1 <B(3) 341048434103637 42 22 4 2 47 13 2
95779679575336 8986527[13]1021994 -41048434103652 <A(1) 1 341048434103637 42 22 4 2 47 13 2
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <A(1) 11+V(2) 3 4 2 4 21+V(1) [*]* [*]* [*]* [*]* [*]*
1 2 2 1 (2)B> 11+V(2) 3 4 2 4 21+V(1) [*]* [*]* [*]* [*]* [*]*
2 3+V(2) 3+V(2) 1 21+V(2) (2)B> 3 4 2 4 21+V(1) [*]* [*]* [*]* [*]* [*]*
3 7+V(2) 1+V(2) 1 21+V(2) <A(1) 1 4 2 4 21+V(1) [*]* [*]* [*]* [*]* [*]*
4 10+4*V(2) 0 1 <A(1) 12+V(2) 4 2 4 21+V(1) [*]* [*]* [*]* [*]* [*]*
5 11+4*V(2) -1 <B(1) 13+V(2) 4 2 4 21+V(1) [*]* [*]* [*]* [*]* [*]*
6 12+4*V(2) -2 <A(2) 14+V(2) 4 2 4 21+V(1) [*]* [*]* [*]* [*]* [*]*
7 19+4*V(2) -3 <A(1) 15+V(2) 4 2 4 21+V(1) [*]* [*]* [*]* [*]* [*]*
8 21+4*V(2) -1 1 (2)B> 15+V(2) 4 2 4 21+V(1) [*]* [*]* [*]* [*]* [*]*
9 26+5*V(2) 4+V(2) 1 25+V(2) (2)B> 4 2 4 21+V(1) [*]* [*]* [*]* [*]* [*]*
10 27+5*V(2) 5+V(2) 1 26+V(2) (5)A> 2 4 21+V(1) [*]* [*]* [*]* [*]* [*]*
11 28+5*V(2) 6+V(2) 1 26+V(2) 5 (3)A> 4 21+V(1) [*]* [*]* [*]* [*]* [*]*
12 30+5*V(2) 4+V(2) 1 26+V(2) 5 <A(4) 22+V(1) [*]* [*]* [*]* [*]* [*]*
13 31+5*V(2) 3+V(2) 1 26+V(2) <B(4) 4 22+V(1) [*]* [*]* [*]* [*]* [*]*
14 32+5*V(2) 2+V(2) 1 25+V(2) <B(3) 42 22+V(1) [*]* [*]* [*]* [*]* [*]*
15 37+6*V(2) -3 1 <B(3) 35+V(2) 42 22+V(1) [*]* [*]* [*]* [*]* [*]*
16 42+6*V(2) -4 <A(1) 1 35+V(2) 42 22+V(1) [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 15 (PPA)
95779679575336 8986527[13]1021994 -41048434103652 <A(1) 1 341048434103637 42 22 4 2 47 13 2
== Executing PA-CTR 7, V(1)=41048434103635, V(2)=0, repcount=41048434103636, factor=4/1
383118718300788 1437844[15]3525958 -164193736414560 <A(1) 1164193736414545 3 42 22 4 2 47 13 2
== Executing PPA-CTR 11 (once), V(1)=1, V(2)=164193736414544
383118718300802 1437844[15]2013262 -164193736414564 <A(1) 1 3164193736414549 4 23 4 2 47 13 2
== Executing PA-CTR 7, V(1)=164193736414547, V(2)=0, repcount=164193736414548, factor=4/1
1532474873202638 2300551[16]0927722 -656774945658208 <A(1) 1656774945658193 3 4 23 4 2 47 13 2
== Executing PPA-CTR 12 (once), V(1)=0, V(2)=1, V(3)=656774945658192
1532474873202656 2300551[16]4876920 -656774945658212 <A(1) 1 3656774945658197 44 22 47 13 2
== Executing PA-CTR 3, V(1)=656774945658195, V(2)=0, repcount=656774945658196, factor=4/1
6129899492810028 3680881[17]2912404 -2627099782632800 <A(1) 12627099782632785 3 44 22 47 13 2
== Executing PPA-CTR 9 (once), V(1)=1, V(2)=2627099782632784
6129899492810042 3680881[17]8709148 -2627099782632804 <A(1) 1 32627099782632789 4 2 42 22 47 13 2
== Executing PA-CTR 7, V(1)=2627099782632787, V(2)=0, repcount=2627099782632788, factor=4/1
24519597971239558 5889410[18]8893368 -105083[4]0531168 <A(1) 110508399130531153 3 4 2 42 22 47 13 2
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=10508399130531152
24519597971239574 5889410[18]2080322 -105083[4]0531172 <A(1) 1 310508399130531157 42 2 4 22 47 13 2
== Executing PA-CTR 7, V(1)=10508399130531155, V(2)=0, repcount=10508399130531156, factor=4/1
98078391884957666 9423057[19]1493726 -420335[4]2124640 <A(1) 142033596522124625 3 42 2 4 22 47 13 2
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=42033596522124624
98078391884957680 9423057[19]4241510 -420335[4]2124644 <A(1) 1 342033596522124629 4 22 4 22 47 13 2
== Executing PA-CTR 7, V(1)=42033596522124627, V(2)=0, repcount=42033596522124628, factor=4/1
3923135[4]9830076 1507689[21]0719490 -168134[5]8498528 <A(1) 11681343[4]8498513 3 4 22 4 22 47 13 2
== Executing PPA-CTR 12 (once), V(1)=1, V(2)=0, V(3)=1681343[4]8498512
3923135[4]9830094 1507689[21]1710606 -168134[5]8498532 <A(1) 1 31681343[4]8498517 43 23 47 13 2
== Executing PA-CTR 3, V(1)=1681343[4]8498515, V(2)=0, repcount=1681343[4]8498516, factor=4/1
1569254[5]9319706 2412302[22]8812330 -672537[5]3994080 <A(1) 16725375[4]3994065 3 43 23 47 13 2
== Executing PPA-CTR 9 (once), V(1)=0, V(2)=6725375[4]3994064
1569254[5]9319720 2412302[22]2776754 -672537[5]3994084 <A(1) 1 36725375[4]3994069 4 2 4 23 47 13 2
== Executing PA-CTR 7, V(1)=6725375[4]3994067, V(2)=0, repcount=6725375[4]3994068, factor=4/1
6277017[5]7278196 3859684[23]0220494 -269015[6]5976288 <A(1) 12690150[5]5976273 3 4 2 4 23 47 13 2
== Executing PPA-CTR 8 (once), V(1)=2, V(2)=2690150[5]5976272
6277017[5]7278212 3859684[23]6078168 -269015[6]5976292 <A(1) 1 32690150[5]5976277 42 24 47 13 2
== Executing PA-CTR 3, V(1)=2690150[5]5976275, V(2)=0, repcount=2690150[5]5976276, factor=4/1
2510806[6]9112144 6175494[24]0442612 -107606[7]3905120 <A(1) 11076060[6]3905105 3 42 24 47 13 2
== Executing PPA-CTR 5 (once), V(1)=3, V(2)=1076060[6]3905104
2510806[6]9112158 6175494[24]3873276 -107606[7]3905124 <A(1) 1 31076060[6]3905109 4 25 47 13 2
== Executing PA-CTR 3, V(1)=1076060[6]3905107, V(2)=0, repcount=1076060[6]3905108, factor=4/1
1004322[7]6447914 9880791[25]4762776 -430424[7]5620448 <A(1) 14304240[6]5620433 3 4 25 47 13 2
== Executing PPA-CTR 6 (once), V(1)=5, V(2)=3, V(3)=4304240[6]5620432
1004322[7]6447932 9880791[25]8485418 -430424[7]5620452 <A(1) 1 34304240[6]5620437 46 2 46 13 2
== Executing PA-CTR 3, V(1)=4304240[6]5620435, V(2)=0, repcount=4304240[6]5620436, factor=4/1
4017290[7]5790984 1580926[27]6950982 -172169[8]2481760 <A(1) 11721696[7]2481745 3 46 2 46 13 2
== Executing PPA-CTR 9 (once), V(1)=3, V(2)=1721696[7]2481744
4017290[7]5790998 1580926[27]1841486 -172169[8]2481764 <A(1) 1 31721696[7]2481749 4 2 44 2 46 13 2
== Executing PA-CTR 7, V(1)=1721696[7]2481747, V(2)=0, repcount=1721696[7]2481748, factor=4/1
1606916[8]3163234 2529482[28]4224746 -688678[8]9927008 <A(1) 16886784[7]9926993 3 4 2 44 2 46 13 2
== Executing PPA-CTR 10 (once), V(1)=2, V(2)=6886784[7]9926992
1606916[8]3163250 2529482[28]3786740 -688678[8]9927012 <A(1) 1 36886784[7]9926997 42 2 43 2 46 13 2
== Executing PA-CTR 7, V(1)=6886784[7]9926995, V(2)=0, repcount=6886784[7]9926996, factor=4/1
6427665[8]2652222 4047172[29]9655824 -275471[9]9708000 <A(1) 12754713[8]9707985 3 42 2 43 2 46 13 2
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=2754713[8]9707984
6427665[8]2652236 4047172[29]7903768 -275471[9]9708004 <A(1) 1 32754713[8]9707989 4 22 43 2 46 13 2
== Executing PA-CTR 7, V(1)=2754713[8]9707987, V(2)=0, repcount=2754713[8]9707988, factor=4/1
2571066[9]0608152 6475475[30]2756788 -110188[10]8831968 <A(1) 11101885[9]8831953 3 4 22 43 2 46 13 2
== Executing PPA-CTR 13 (once), V(1)=1, V(2)=0, V(3)=1101885[9]8831952
2571066[9]0608170 6475475[30]5748544 -110188[10]8831972 <A(1) 1 31101885[9]8831957 43 2 42 2 46 13 2
== Executing PA-CTR 7, V(1)=1101885[9]8831955, V(2)=0, repcount=1101885[9]8831956, factor=4/1
1028426[10]2431862 1036076[32]7187548 -440754[10]5327840 <A(1) 14407542[9]5327825 3 43 2 42 2 46 13 2
1028426[10]2431863 1036076[32]7187550 -440754[10]5327838 1 (2)B> 14407542[9]5327825 3 43 2 42 2 46 13 2
1028426[10]2431864 1036076[32]2515375 -13 1 24407542[9]5327825 (2)B> 3 43 2 42 2 46 13 2
1028426[10]2431865 1036076[32]2515379 -15 1 24407542[9]5327825 <A(1) 1 43 2 42 2 46 13 2
1028426[10]2431866 1036076[32]8498854 -440754[10]5327840 1 <A(1) 14407542[9]5327826 43 2 42 2 46 13 2
1028426[10]2431867 1036076[32]8498855 -440754[10]5327841 <B(1) 14407542[9]5327827 43 2 42 2 46 13 2
1028426[10]2431868 1036076[32]8498856 -440754[10]5327842 <A(2) 14407542[9]5327828 43 2 42 2 46 13 2
1028426[10]2431869 1036076[32]8498863 -440754[10]5327843 <A(1) 14407542[9]5327829 43 2 42 2 46 13 2
1028426[10]2431870 1036076[32]8498865 -440754[10]5327841 1 (2)B> 14407542[9]5327829 43 2 42 2 46 13 2
1028426[10]2431871 1036076[32]3826694 -12 1 24407542[9]5327829 (2)B> 43 2 42 2 46 13 2
1028426[10]2431872 1036076[32]3826695 -11 1 24407542[9]5327830 (5)A> 42 2 42 2 46 13 2
1028426[10]2431873 1036076[32]3826697 -13 1 24407542[9]5327830 <B(4) 2 4 2 42 2 46 13 2
1028426[10]2431874 1036076[32]3826698 -14 1 24407542[9]5327829 <B(3) 4 2 4 2 42 2 46 13 2
1028426[10]2431875 1036076[32]9154527 -440754[10]5327843 1 <B(3) 34407542[9]5327829 4 2 4 2 42 2 46 13 2
Lines: 350
Top steps: 349
Macro steps: 102842647849161162431875
Basic steps: 1036076102853215321064734306590090334289154527
Tape index: -44075420506783355327843
nonzeros: 44075420506783355327848
log10(nonzeros): 22.644
log10(steps ): 45.015
Some long numbers above are shortened: #(omitted digits) shown in "[]".
Input to awk program:
gohalt 1
nbs 6
T 2-state 6-symbol #f (T.J. & S. Ligocki)
: >6.9x10^4931 >2.5x10^9863
5T 1RB 1LB 3RA 4LA 2LA 4LB 2LA 2RB 3LB 1LA 5RA 1RH
L 20
M 350
pref sim
machv Lig26_f just simple
machv Lig26_f-r with repetitions reduced
machv Lig26_f-1 with tape symbol exponents
machv Lig26_f-m as 1-bck-macro machine
machv Lig26_f-a as 1-bck-macro machine with pure additive config-TRs
iam Lig26_f-a
mtype 1 0
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:13:22 CEST 2010
edate Tue Jul 6 22:13:24 CEST 2010
bnspeed 1
short 7
Constructed by: $Id: tmJob.awk,v 1.34 2010/05/06 18:26:17 heiner Exp $
$Id: basics.awk,v 1.1 2010/05/06 17:24:17 heiner Exp $
$Id: htSupp.awk,v 1.14 2010/07/06 19:48:32 heiner Exp $
$Id: mmSim.awk,v 1.34 2005/01/09 22:23:28 heiner Exp $
$Id: bignum.awk,v 1.34 2010/05/06 17:58:14 heiner Exp $
$Id: varLI.awk,v 1.11 2005/01/15 21:01:29 heiner Exp $
bignum signature: LEN={S++:9 U++:9 S+:8 U+:8 S*:4 U*:4} DONT: y i o;
Start: Tue Jul 6 22:13:22 CEST 2010