Comment: This TM produces 620,906,587 nonzeros in 91,791,666,497,368,316 steps.
| State | on 0 |
on 1 |
on 2 |
on 3 |
on 4 |
on 0 | on 1 | on 2 | on 3 | on 4 | ||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Move | Goto | Move | Goto | Move | Goto | Move | Goto | Move | Goto | |||||||||||
| A | 1RB | 1RH | 4LA | 4LB | 2RA | 1 | right | B | 1 | right | H | 4 | left | A | 4 | left | B | 2 | right | A |
| B | 2LB | 2RB | 3RB | 2RA | 0RB | 2 | left | B | 2 | right | B | 3 | right | B | 2 | right | A | 0 | right | B |
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 4 2 2 (3)B>
3 8 0 2 <A(4) 4
4 9 -1 <A(4) 42
5 11 1 1 (0)B> 42
6 13 3 1 02 (0)B>
7 15 1 1 02 <B(2) 2
8 17 -1 1 <B(2) 23
9 19 1 2 (3)B> 23
10 22 4 2 33 (3)B>
11 26 2 2 33 <A(4) 4
12 27 1 2 32 <B(4) 42
13 29 3 2 3 2 (2)A> 42
14 31 5 2 3 23 (2)A>
15 32 6 2 3 24 (1)B>
16 35 7 2 3 25 (3)B>
17 39 5 2 3 25 <A(4) 4
18 44 0 2 3 <A(4) 46
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* 33+V(1) <A(4) 41+V(2)
1 1 -1 [*]* 32+V(1) <B(4) 42+V(2)
2 3 1 [*]* 31+V(1) 2 (2)A> 42+V(2)
3 5+V(2) 3+V(2) [*]* 31+V(1) 23+V(2) (2)A>
4 6+V(2) 4+V(2) [*]* 31+V(1) 24+V(2) (1)B>
5 9+V(2) 5+V(2) [*]* 31+V(1) 25+V(2) (3)B>
6 13+V(2) 3+V(2) [*]* 31+V(1) 25+V(2) <A(4) 4
7 18+2*V(2) -2 [*]* 31+V(1) <A(4) 46+V(2)
<< Success! ==> defined new CTR 1 (PA)
19 45 -1 2 <B(4) 47
20 47 1 3 (0)B> 47
21 54 8 3 07 (0)B>
22 56 6 3 07 <B(2) 2
23 63 -1 3 <B(2) 28
24 66 -2 <A(4) 4 28
25 68 0 1 (0)B> 4 28
26 69 1 1 0 (0)B> 28
27 70 2 1 02 (3)B> 27
28 77 9 1 02 37 (3)B>
29 81 7 1 02 37 <A(4) 4
30 82 6 1 02 36 <B(4) 42
31 84 8 1 02 35 2 (2)A> 42
32 86 10 1 02 35 23 (2)A>
33 87 11 1 02 35 24 (1)B>
34 90 12 1 02 35 25 (3)B>
35 94 10 1 02 35 25 <A(4) 4
36 99 5 1 02 35 <A(4) 46
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* 33+V(1) <A(4) 41+V(2)
1 1 -1 [*]* [*]* 32+V(1) <B(4) 42+V(2)
2 3 1 [*]* [*]* 31+V(1) 2 (2)A> 42+V(2)
3 5+V(2) 3+V(2) [*]* [*]* 31+V(1) 23+V(2) (2)A>
4 6+V(2) 4+V(2) [*]* [*]* 31+V(1) 24+V(2) (1)B>
5 9+V(2) 5+V(2) [*]* [*]* 31+V(1) 25+V(2) (3)B>
6 13+V(2) 3+V(2) [*]* [*]* 31+V(1) 25+V(2) <A(4) 4
7 18+2*V(2) -2 [*]* [*]* 31+V(1) <A(4) 46+V(2)
<< Success! ==> defined new CTR 2 (PA)
36 99 5 1 02 35 <A(4) 46
== Executing PA-CTR 2, V(1)=2, V(2)=5, repcount=2, factor=5/2
50 165 1 1 02 3 <A(4) 416
51 166 0 1 02 <B(4) 417
52 167 -1 1 0 <B(2) 418
53 168 -2 1 <B(2) 2 418
54 170 0 2 (3)B> 2 418
55 171 1 2 3 (3)B> 418
56 172 2 2 32 (0)B> 417
57 189 19 2 32 017 (0)B>
58 191 17 2 32 017 <B(2) 2
59 208 0 2 32 <B(2) 218
60 211 -1 2 3 <A(4) 4 218
61 212 -2 2 <B(4) 42 218
62 214 0 3 (0)B> 42 218
63 216 2 3 02 (0)B> 218
64 217 3 3 03 (3)B> 217
65 234 20 3 03 317 (3)B>
66 238 18 3 03 317 <A(4) 4
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 1 02 3 <A(4) 42+V(1)
1 1 -1 1 02 <B(4) 43+V(1)
2 2 -2 1 0 <B(2) 44+V(1)
3 3 -3 1 <B(2) 2 44+V(1)
4 5 -1 2 (3)B> 2 44+V(1)
5 6 0 2 3 (3)B> 44+V(1)
6 7 1 2 32 (0)B> 43+V(1)
7 10+V(1) 4+V(1) 2 32 03+V(1) (0)B>
8 12+V(1) 2+V(1) 2 32 03+V(1) <B(2) 2
9 15+2*V(1) -1 2 32 <B(2) 24+V(1)
10 18+2*V(1) -2 2 3 <A(4) 4 24+V(1)
11 19+2*V(1) -3 2 <B(4) 42 24+V(1)
12 21+2*V(1) -1 3 (0)B> 42 24+V(1)
13 23+2*V(1) 1 3 02 (0)B> 24+V(1)
14 24+2*V(1) 2 3 03 (3)B> 23+V(1)
15 27+3*V(1) 5+V(1) 3 03 33+V(1) (3)B>
16 31+3*V(1) 3+V(1) 3 03 33+V(1) <A(4) 4
<< Success! ==> defined new CTR 3 (PPA)
66 238 18 3 03 317 <A(4) 4
== Executing PA-CTR 2, V(1)=14, V(2)=0, repcount=8, factor=5/2
122 662 2 3 03 3 <A(4) 441
123 663 1 3 03 <B(4) 442
124 664 0 3 02 <B(2) 443
125 666 -2 3 <B(2) 22 443
126 669 -3 <A(4) 4 22 443
127 671 -1 1 (0)B> 4 22 443
128 672 0 1 0 (0)B> 22 443
129 673 1 1 02 (3)B> 2 443
130 674 2 1 02 3 (3)B> 443
131 675 3 1 02 32 (0)B> 442
132 717 45 1 02 32 042 (0)B>
133 719 43 1 02 32 042 <B(2) 2
134 761 1 1 02 32 <B(2) 243
135 764 0 1 02 3 <A(4) 4 243
136 765 -1 1 02 <B(4) 42 243
137 766 -2 1 0 <B(2) 43 243
138 767 -3 1 <B(2) 2 43 243
139 769 -1 2 (3)B> 2 43 243
140 770 0 2 3 (3)B> 43 243
141 771 1 2 32 (0)B> 42 243
142 773 3 2 32 02 (0)B> 243
143 774 4 2 32 03 (3)B> 242
144 816 46 2 32 03 342 (3)B>
145 820 44 2 32 03 342 <A(4) 4
146 821 43 2 32 03 341 <B(4) 42
147 823 45 2 32 03 340 2 (2)A> 42
148 825 47 2 32 03 340 23 (2)A>
149 826 48 2 32 03 340 24 (1)B>
150 829 49 2 32 03 340 25 (3)B>
151 833 47 2 32 03 340 25 <A(4) 4
152 838 42 2 32 03 340 <A(4) 46
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* 33+V(1) <A(4) 41+V(2)
1 1 -1 [*]* [*]* [*]* 32+V(1) <B(4) 42+V(2)
2 3 1 [*]* [*]* [*]* 31+V(1) 2 (2)A> 42+V(2)
3 5+V(2) 3+V(2) [*]* [*]* [*]* 31+V(1) 23+V(2) (2)A>
4 6+V(2) 4+V(2) [*]* [*]* [*]* 31+V(1) 24+V(2) (1)B>
5 9+V(2) 5+V(2) [*]* [*]* [*]* 31+V(1) 25+V(2) (3)B>
6 13+V(2) 3+V(2) [*]* [*]* [*]* 31+V(1) 25+V(2) <A(4) 4
7 18+2*V(2) -2 [*]* [*]* [*]* 31+V(1) <A(4) 46+V(2)
<< Success! ==> defined new CTR 4 (PA)
152 838 42 2 32 03 340 <A(4) 46
== Executing PA-CTR 4, V(1)=37, V(2)=5, repcount=19, factor=5/2
285 3080 4 2 32 03 32 <A(4) 4101
286 3081 3 2 32 03 3 <B(4) 4102
287 3083 5 2 32 03 2 (2)A> 4102
288 3185 107 2 32 03 2103 (2)A>
289 3186 108 2 32 03 2104 (1)B>
290 3189 109 2 32 03 2105 (3)B>
291 3193 107 2 32 03 2105 <A(4) 4
292 3298 2 2 32 03 <A(4) 4106
293 3300 4 2 32 02 1 (0)B> 4106
294 3406 110 2 32 02 1 0106 (0)B>
295 3408 108 2 32 02 1 0106 <B(2) 2
296 3514 2 2 32 02 1 <B(2) 2107
297 3516 4 2 32 02 2 (3)B> 2107
298 3623 111 2 32 02 2 3107 (3)B>
299 3627 109 2 32 02 2 3107 <A(4) 4
300 3628 108 2 32 02 2 3106 <B(4) 42
301 3630 110 2 32 02 2 3105 2 (2)A> 42
302 3632 112 2 32 02 2 3105 23 (2)A>
303 3633 113 2 32 02 2 3105 24 (1)B>
304 3636 114 2 32 02 2 3105 25 (3)B>
305 3640 112 2 32 02 2 3105 25 <A(4) 4
306 3645 107 2 32 02 2 3105 <A(4) 46
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* [*]* 33+V(1) <A(4) 41+V(2)
1 1 -1 [*]* [*]* [*]* [*]* 32+V(1) <B(4) 42+V(2)
2 3 1 [*]* [*]* [*]* [*]* 31+V(1) 2 (2)A> 42+V(2)
3 5+V(2) 3+V(2) [*]* [*]* [*]* [*]* 31+V(1) 23+V(2) (2)A>
4 6+V(2) 4+V(2) [*]* [*]* [*]* [*]* 31+V(1) 24+V(2) (1)B>
5 9+V(2) 5+V(2) [*]* [*]* [*]* [*]* 31+V(1) 25+V(2) (3)B>
6 13+V(2) 3+V(2) [*]* [*]* [*]* [*]* 31+V(1) 25+V(2) <A(4) 4
7 18+2*V(2) -2 [*]* [*]* [*]* [*]* 31+V(1) <A(4) 46+V(2)
<< Success! ==> defined new CTR 5 (PA)
306 3645 107 2 32 02 2 3105 <A(4) 46
== Executing PA-CTR 5, V(1)=102, V(2)=5, repcount=52, factor=5/2
670 18361 3 2 32 02 2 3 <A(4) 4266
671 18362 2 2 32 02 2 <B(4) 4267
672 18364 4 2 32 02 3 (0)B> 4267
673 18631 271 2 32 02 3 0267 (0)B>
674 18633 269 2 32 02 3 0267 <B(2) 2
675 18900 2 2 32 02 3 <B(2) 2268
676 18903 1 2 32 02 <A(4) 4 2268
677 18905 3 2 32 0 1 (0)B> 4 2268
678 18906 4 2 32 0 1 0 (0)B> 2268
679 18907 5 2 32 0 1 02 (3)B> 2267
680 19174 272 2 32 0 1 02 3267 (3)B>
681 19178 270 2 32 0 1 02 3267 <A(4) 4
682 19179 269 2 32 0 1 02 3266 <B(4) 42
683 19181 271 2 32 0 1 02 3265 2 (2)A> 42
684 19183 273 2 32 0 1 02 3265 23 (2)A>
685 19184 274 2 32 0 1 02 3265 24 (1)B>
686 19187 275 2 32 0 1 02 3265 25 (3)B>
687 19191 273 2 32 0 1 02 3265 25 <A(4) 4
688 19196 268 2 32 0 1 02 3265 <A(4) 46
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* [*]* [*]* 33+V(1) <A(4) 41+V(2)
1 1 -1 [*]* [*]* [*]* [*]* [*]* 32+V(1) <B(4) 42+V(2)
2 3 1 [*]* [*]* [*]* [*]* [*]* 31+V(1) 2 (2)A> 42+V(2)
3 5+V(2) 3+V(2) [*]* [*]* [*]* [*]* [*]* 31+V(1) 23+V(2) (2)A>
4 6+V(2) 4+V(2) [*]* [*]* [*]* [*]* [*]* 31+V(1) 24+V(2) (1)B>
5 9+V(2) 5+V(2) [*]* [*]* [*]* [*]* [*]* 31+V(1) 25+V(2) (3)B>
6 13+V(2) 3+V(2) [*]* [*]* [*]* [*]* [*]* 31+V(1) 25+V(2) <A(4) 4
7 18+2*V(2) -2 [*]* [*]* [*]* [*]* [*]* 31+V(1) <A(4) 46+V(2)
<< Success! ==> defined new CTR 6 (PA)
688 19196 268 2 32 0 1 02 3265 <A(4) 46
== Executing PA-CTR 6, V(1)=262, V(2)=5, repcount=132, factor=5/2
1612 109352 4 2 32 0 1 02 3 <A(4) 4666
1613 109353 3 2 32 0 1 02 <B(4) 4667
1614 109354 2 2 32 0 1 0 <B(2) 4668
1615 109355 1 2 32 0 1 <B(2) 2 4668
1616 109357 3 2 32 0 2 (3)B> 2 4668
1617 109358 4 2 32 0 2 3 (3)B> 4668
1618 109359 5 2 32 0 2 32 (0)B> 4667
1619 110026 672 2 32 0 2 32 0667 (0)B>
1620 110028 670 2 32 0 2 32 0667 <B(2) 2
1621 110695 3 2 32 0 2 32 <B(2) 2668
1622 110698 2 2 32 0 2 3 <A(4) 4 2668
1623 110699 1 2 32 0 2 <B(4) 42 2668
1624 110701 3 2 32 0 3 (0)B> 42 2668
1625 110703 5 2 32 0 3 02 (0)B> 2668
1626 110704 6 2 32 0 3 03 (3)B> 2667
1627 111371 673 2 32 0 3 03 3667 (3)B>
1628 111375 671 2 32 0 3 03 3667 <A(4) 4
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 [*]* [*]* [*]* 1 02 3 <A(4) 42+V(1)
1 1 -1 [*]* [*]* [*]* 1 02 <B(4) 43+V(1)
2 2 -2 [*]* [*]* [*]* 1 0 <B(2) 44+V(1)
3 3 -3 [*]* [*]* [*]* 1 <B(2) 2 44+V(1)
4 5 -1 [*]* [*]* [*]* 2 (3)B> 2 44+V(1)
5 6 0 [*]* [*]* [*]* 2 3 (3)B> 44+V(1)
6 7 1 [*]* [*]* [*]* 2 32 (0)B> 43+V(1)
7 10+V(1) 4+V(1) [*]* [*]* [*]* 2 32 03+V(1) (0)B>
8 12+V(1) 2+V(1) [*]* [*]* [*]* 2 32 03+V(1) <B(2) 2
9 15+2*V(1) -1 [*]* [*]* [*]* 2 32 <B(2) 24+V(1)
10 18+2*V(1) -2 [*]* [*]* [*]* 2 3 <A(4) 4 24+V(1)
11 19+2*V(1) -3 [*]* [*]* [*]* 2 <B(4) 42 24+V(1)
12 21+2*V(1) -1 [*]* [*]* [*]* 3 (0)B> 42 24+V(1)
13 23+2*V(1) 1 [*]* [*]* [*]* 3 02 (0)B> 24+V(1)
14 24+2*V(1) 2 [*]* [*]* [*]* 3 03 (3)B> 23+V(1)
15 27+3*V(1) 5+V(1) [*]* [*]* [*]* 3 03 33+V(1) (3)B>
16 31+3*V(1) 3+V(1) [*]* [*]* [*]* 3 03 33+V(1) <A(4) 4
<< Success! ==> defined new CTR 7 (PPA)
1628 111375 671 2 32 0 3 03 3667 <A(4) 4
== Executing PA-CTR 6, V(1)=664, V(2)=0, repcount=333, factor=5/2
3959 670149 5 2 32 0 3 03 3 <A(4) 41666
3960 670150 4 2 32 0 3 03 <B(4) 41667
3961 670151 3 2 32 0 3 02 <B(2) 41668
3962 670153 1 2 32 0 3 <B(2) 22 41668
3963 670156 0 2 32 0 <A(4) 4 22 41668
3964 670158 2 2 32 1 (0)B> 4 22 41668
3965 670159 3 2 32 1 0 (0)B> 22 41668
3966 670160 4 2 32 1 02 (3)B> 2 41668
3967 670161 5 2 32 1 02 3 (3)B> 41668
3968 670162 6 2 32 1 02 32 (0)B> 41667
3969 671829 1673 2 32 1 02 32 01667 (0)B>
3970 671831 1671 2 32 1 02 32 01667 <B(2) 2
3971 673498 4 2 32 1 02 32 <B(2) 21668
3972 673501 3 2 32 1 02 3 <A(4) 4 21668
3973 673502 2 2 32 1 02 <B(4) 42 21668
3974 673503 1 2 32 1 0 <B(2) 43 21668
3975 673504 0 2 32 1 <B(2) 2 43 21668
3976 673506 2 2 32 2 (3)B> 2 43 21668
3977 673507 3 2 32 2 3 (3)B> 43 21668
3978 673508 4 2 32 2 32 (0)B> 42 21668
3979 673510 6 2 32 2 32 02 (0)B> 21668
3980 673511 7 2 32 2 32 03 (3)B> 21667
3981 675178 1674 2 32 2 32 03 31667 (3)B>
3982 675182 1672 2 32 2 32 03 31667 <A(4) 4
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 [*]* [*]* 0 3 03 3 <A(4) 42+V(1)
1 1 -1 [*]* [*]* 0 3 03 <B(4) 43+V(1)
2 2 -2 [*]* [*]* 0 3 02 <B(2) 44+V(1)
3 4 -4 [*]* [*]* 0 3 <B(2) 22 44+V(1)
4 7 -5 [*]* [*]* 0 <A(4) 4 22 44+V(1)
5 9 -3 [*]* [*]* 1 (0)B> 4 22 44+V(1)
6 10 -2 [*]* [*]* 1 0 (0)B> 22 44+V(1)
7 11 -1 [*]* [*]* 1 02 (3)B> 2 44+V(1)
8 12 0 [*]* [*]* 1 02 3 (3)B> 44+V(1)
9 13 1 [*]* [*]* 1 02 32 (0)B> 43+V(1)
10 16+V(1) 4+V(1) [*]* [*]* 1 02 32 03+V(1) (0)B>
11 18+V(1) 2+V(1) [*]* [*]* 1 02 32 03+V(1) <B(2) 2
12 21+2*V(1) -1 [*]* [*]* 1 02 32 <B(2) 24+V(1)
13 24+2*V(1) -2 [*]* [*]* 1 02 3 <A(4) 4 24+V(1)
14 25+2*V(1) -3 [*]* [*]* 1 02 <B(4) 42 24+V(1)
15 26+2*V(1) -4 [*]* [*]* 1 0 <B(2) 43 24+V(1)
16 27+2*V(1) -5 [*]* [*]* 1 <B(2) 2 43 24+V(1)
17 29+2*V(1) -3 [*]* [*]* 2 (3)B> 2 43 24+V(1)
18 30+2*V(1) -2 [*]* [*]* 2 3 (3)B> 43 24+V(1)
19 31+2*V(1) -1 [*]* [*]* 2 32 (0)B> 42 24+V(1)
20 33+2*V(1) 1 [*]* [*]* 2 32 02 (0)B> 24+V(1)
21 34+2*V(1) 2 [*]* [*]* 2 32 03 (3)B> 23+V(1)
22 37+3*V(1) 5+V(1) [*]* [*]* 2 32 03 33+V(1) (3)B>
23 41+3*V(1) 3+V(1) [*]* [*]* 2 32 03 33+V(1) <A(4) 4
<< Success! ==> defined new CTR 8 (PPA)
3982 675182 1672 2 32 2 32 03 31667 <A(4) 4
== Executing PA-CTR 6, V(1)=1664, V(2)=0, repcount=833, factor=5/2
9813 4155456 6 2 32 2 32 03 3 <A(4) 44166
9814 4155457 5 2 32 2 32 03 <B(4) 44167
9815 4155458 4 2 32 2 32 02 <B(2) 44168
9816 4155460 2 2 32 2 32 <B(2) 22 44168
9817 4155463 1 2 32 2 3 <A(4) 4 22 44168
9818 4155464 0 2 32 2 <B(4) 42 22 44168
9819 4155466 2 2 33 (0)B> 42 22 44168
9820 4155468 4 2 33 02 (0)B> 22 44168
9821 4155469 5 2 33 03 (3)B> 2 44168
9822 4155470 6 2 33 03 3 (3)B> 44168
9823 4155471 7 2 33 03 32 (0)B> 44167
9824 4159638 4174 2 33 03 32 04167 (0)B>
9825 4159640 4172 2 33 03 32 04167 <B(2) 2
9826 4163807 5 2 33 03 32 <B(2) 24168
9827 4163810 4 2 33 03 3 <A(4) 4 24168
9828 4163811 3 2 33 03 <B(4) 42 24168
9829 4163812 2 2 33 02 <B(2) 43 24168
9830 4163814 0 2 33 <B(2) 22 43 24168
9831 4163817 -1 2 32 <A(4) 4 22 43 24168
9832 4163818 -2 2 3 <B(4) 42 22 43 24168
9833 4163820 0 22 (2)A> 42 22 43 24168
9834 4163822 2 24 (2)A> 22 43 24168
9835 4163824 0 24 <A(4) 4 2 43 24168
9836 4163828 -4 <A(4) 45 2 43 24168
9837 4163830 -2 1 (0)B> 45 2 43 24168
9838 4163835 3 1 05 (0)B> 2 43 24168
9839 4163836 4 1 06 (3)B> 43 24168
9840 4163837 5 1 06 3 (0)B> 42 24168
9841 4163839 7 1 06 3 02 (0)B> 24168
9842 4163840 8 1 06 3 03 (3)B> 24167
9843 4168007 4175 1 06 3 03 34167 (3)B>
9844 4168011 4173 1 06 3 03 34167 <A(4) 4
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 21+V(1) 32 2 32 03 3 <A(4) 42+V(2)
1 1 -1 21+V(1) 32 2 32 03 <B(4) 43+V(2)
2 2 -2 21+V(1) 32 2 32 02 <B(2) 44+V(2)
3 4 -4 21+V(1) 32 2 32 <B(2) 22 44+V(2)
4 7 -5 21+V(1) 32 2 3 <A(4) 4 22 44+V(2)
5 8 -6 21+V(1) 32 2 <B(4) 42 22 44+V(2)
6 10 -4 21+V(1) 33 (0)B> 42 22 44+V(2)
7 12 -2 21+V(1) 33 02 (0)B> 22 44+V(2)
8 13 -1 21+V(1) 33 03 (3)B> 2 44+V(2)
9 14 0 21+V(1) 33 03 3 (3)B> 44+V(2)
10 15 1 21+V(1) 33 03 32 (0)B> 43+V(2)
11 18+V(2) 4+V(2) 21+V(1) 33 03 32 03+V(2) (0)B>
12 20+V(2) 2+V(2) 21+V(1) 33 03 32 03+V(2) <B(2) 2
13 23+2*V(2) -1 21+V(1) 33 03 32 <B(2) 24+V(2)
14 26+2*V(2) -2 21+V(1) 33 03 3 <A(4) 4 24+V(2)
15 27+2*V(2) -3 21+V(1) 33 03 <B(4) 42 24+V(2)
16 28+2*V(2) -4 21+V(1) 33 02 <B(2) 43 24+V(2)
17 30+2*V(2) -6 21+V(1) 33 <B(2) 22 43 24+V(2)
18 33+2*V(2) -7 21+V(1) 32 <A(4) 4 22 43 24+V(2)
19 34+2*V(2) -8 21+V(1) 3 <B(4) 42 22 43 24+V(2)
20 36+2*V(2) -6 22+V(1) (2)A> 42 22 43 24+V(2)
21 38+2*V(2) -4 24+V(1) (2)A> 22 43 24+V(2)
22 40+2*V(2) -6 24+V(1) <A(4) 4 2 43 24+V(2)
23 44+V(1)+2*V(2) -10+-1*V(1) <A(4) 45+V(1) 2 43 24+V(2)
24 46+V(1)+2*V(2) -8+-1*V(1) 1 (0)B> 45+V(1) 2 43 24+V(2)
25 51+2*V(1)+2*V(2) -3 1 05+V(1) (0)B> 2 43 24+V(2)
26 52+2*V(1)+2*V(2) -2 1 06+V(1) (3)B> 43 24+V(2)
27 53+2*V(1)+2*V(2) -1 1 06+V(1) 3 (0)B> 42 24+V(2)
28 55+2*V(1)+2*V(2) 1 1 06+V(1) 3 02 (0)B> 24+V(2)
29 56+2*V(1)+2*V(2) 2 1 06+V(1) 3 03 (3)B> 23+V(2)
30 59+2*V(1)+3*V(2) 5+V(2) 1 06+V(1) 3 03 33+V(2) (3)B>
31 63+2*V(1)+3*V(2) 3+V(2) 1 06+V(1) 3 03 33+V(2) <A(4) 4
<< Success! ==> defined new CTR 9 (PPA)
9844 4168011 4173 1 06 3 03 34167 <A(4) 4
== Executing PA-CTR 5, V(1)=4164, V(2)=0, repcount=2083, factor=5/2
24425 25889535 7 1 06 3 03 3 <A(4) 410416
24426 25889536 6 1 06 3 03 <B(4) 410417
24427 25889537 5 1 06 3 02 <B(2) 410418
24428 25889539 3 1 06 3 <B(2) 22 410418
24429 25889542 2 1 06 <A(4) 4 22 410418
24430 25889544 4 1 05 1 (0)B> 4 22 410418
24431 25889545 5 1 05 1 0 (0)B> 22 410418
24432 25889546 6 1 05 1 02 (3)B> 2 410418
24433 25889547 7 1 05 1 02 3 (3)B> 410418
24434 25889548 8 1 05 1 02 32 (0)B> 410417
24435 25899965 10425 1 05 1 02 32 010417 (0)B>
24436 25899967 10423 1 05 1 02 32 010417 <B(2) 2
24437 25910384 6 1 05 1 02 32 <B(2) 210418
24438 25910387 5 1 05 1 02 3 <A(4) 4 210418
24439 25910388 4 1 05 1 02 <B(4) 42 210418
24440 25910389 3 1 05 1 0 <B(2) 43 210418
24441 25910390 2 1 05 1 <B(2) 2 43 210418
24442 25910392 4 1 05 2 (3)B> 2 43 210418
24443 25910393 5 1 05 2 3 (3)B> 43 210418
24444 25910394 6 1 05 2 32 (0)B> 42 210418
24445 25910396 8 1 05 2 32 02 (0)B> 210418
24446 25910397 9 1 05 2 32 03 (3)B> 210417
24447 25920814 10426 1 05 2 32 03 310417 (3)B>
24448 25920818 10424 1 05 2 32 03 310417 <A(4) 4
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 [*]* 02+V(1) 3 03 3 <A(4) 42+V(2)
1 1 -1 [*]* 02+V(1) 3 03 <B(4) 43+V(2)
2 2 -2 [*]* 02+V(1) 3 02 <B(2) 44+V(2)
3 4 -4 [*]* 02+V(1) 3 <B(2) 22 44+V(2)
4 7 -5 [*]* 02+V(1) <A(4) 4 22 44+V(2)
5 9 -3 [*]* 01+V(1) 1 (0)B> 4 22 44+V(2)
6 10 -2 [*]* 01+V(1) 1 0 (0)B> 22 44+V(2)
7 11 -1 [*]* 01+V(1) 1 02 (3)B> 2 44+V(2)
8 12 0 [*]* 01+V(1) 1 02 3 (3)B> 44+V(2)
9 13 1 [*]* 01+V(1) 1 02 32 (0)B> 43+V(2)
10 16+V(2) 4+V(2) [*]* 01+V(1) 1 02 32 03+V(2) (0)B>
11 18+V(2) 2+V(2) [*]* 01+V(1) 1 02 32 03+V(2) <B(2) 2
12 21+2*V(2) -1 [*]* 01+V(1) 1 02 32 <B(2) 24+V(2)
13 24+2*V(2) -2 [*]* 01+V(1) 1 02 3 <A(4) 4 24+V(2)
14 25+2*V(2) -3 [*]* 01+V(1) 1 02 <B(4) 42 24+V(2)
15 26+2*V(2) -4 [*]* 01+V(1) 1 0 <B(2) 43 24+V(2)
16 27+2*V(2) -5 [*]* 01+V(1) 1 <B(2) 2 43 24+V(2)
17 29+2*V(2) -3 [*]* 01+V(1) 2 (3)B> 2 43 24+V(2)
18 30+2*V(2) -2 [*]* 01+V(1) 2 3 (3)B> 43 24+V(2)
19 31+2*V(2) -1 [*]* 01+V(1) 2 32 (0)B> 42 24+V(2)
20 33+2*V(2) 1 [*]* 01+V(1) 2 32 02 (0)B> 24+V(2)
21 34+2*V(2) 2 [*]* 01+V(1) 2 32 03 (3)B> 23+V(2)
22 37+3*V(2) 5+V(2) [*]* 01+V(1) 2 32 03 33+V(2) (3)B>
23 41+3*V(2) 3+V(2) [*]* 01+V(1) 2 32 03 33+V(2) <A(4) 4
<< Success! ==> defined new CTR 10 (PPA)
24448 25920818 10424 1 05 2 32 03 310417 <A(4) 4
== Executing PA-CTR 6, V(1)=10414, V(2)=0, repcount=5208, factor=5/2
60904 161604842 8 1 05 2 32 03 3 <A(4) 426041
60905 161604843 7 1 05 2 32 03 <B(4) 426042
60906 161604844 6 1 05 2 32 02 <B(2) 426043
60907 161604846 4 1 05 2 32 <B(2) 22 426043
60908 161604849 3 1 05 2 3 <A(4) 4 22 426043
60909 161604850 2 1 05 2 <B(4) 42 22 426043
60910 161604852 4 1 05 3 (0)B> 42 22 426043
60911 161604854 6 1 05 3 02 (0)B> 22 426043
60912 161604855 7 1 05 3 03 (3)B> 2 426043
60913 161604856 8 1 05 3 03 3 (3)B> 426043
60914 161604857 9 1 05 3 03 32 (0)B> 426042
60915 161630899 26051 1 05 3 03 32 026042 (0)B>
60916 161630901 26049 1 05 3 03 32 026042 <B(2) 2
60917 161656943 7 1 05 3 03 32 <B(2) 226043
60918 161656946 6 1 05 3 03 3 <A(4) 4 226043
60919 161656947 5 1 05 3 03 <B(4) 42 226043
60920 161656948 4 1 05 3 02 <B(2) 43 226043
60921 161656950 2 1 05 3 <B(2) 22 43 226043
60922 161656953 1 1 05 <A(4) 4 22 43 226043
60923 161656955 3 1 04 1 (0)B> 4 22 43 226043
60924 161656956 4 1 04 1 0 (0)B> 22 43 226043
60925 161656957 5 1 04 1 02 (3)B> 2 43 226043
60926 161656958 6 1 04 1 02 3 (3)B> 43 226043
60927 161656959 7 1 04 1 02 32 (0)B> 42 226043
60928 161656961 9 1 04 1 02 32 02 (0)B> 226043
60929 161656962 10 1 04 1 02 32 03 (3)B> 226042
60930 161683004 26052 1 04 1 02 32 03 326042 (3)B>
60931 161683008 26050 1 04 1 02 32 03 326042 <A(4) 4
60932 161683009 26049 1 04 1 02 32 03 326041 <B(4) 42
60933 161683011 26051 1 04 1 02 32 03 326040 2 (2)A> 42
60934 161683013 26053 1 04 1 02 32 03 326040 23 (2)A>
60935 161683014 26054 1 04 1 02 32 03 326040 24 (1)B>
60936 161683017 26055 1 04 1 02 32 03 326040 25 (3)B>
60937 161683021 26053 1 04 1 02 32 03 326040 25 <A(4) 4
60938 161683026 26048 1 04 1 02 32 03 326040 <A(4) 46
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* [*]* [*]* [*]* 33+V(1) <A(4) 41+V(2)
1 1 -1 [*]* [*]* [*]* [*]* [*]* [*]* 32+V(1) <B(4) 42+V(2)
2 3 1 [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 2 (2)A> 42+V(2)
3 5+V(2) 3+V(2) [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 23+V(2) (2)A>
4 6+V(2) 4+V(2) [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 24+V(2) (1)B>
5 9+V(2) 5+V(2) [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 25+V(2) (3)B>
6 13+V(2) 3+V(2) [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 25+V(2) <A(4) 4
7 18+2*V(2) -2 [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) <A(4) 46+V(2)
<< Success! ==> defined new CTR 11 (PA)
60938 161683026 26048 1 04 1 02 32 03 326040 <A(4) 46
== Executing PA-CTR 11, V(1)=26037, V(2)=5, repcount=13019, factor=5/2
152071 1009454268 10 1 04 1 02 32 03 32 <A(4) 465101
152072 1009454269 9 1 04 1 02 32 03 3 <B(4) 465102
152073 1009454271 11 1 04 1 02 32 03 2 (2)A> 465102
152074 1009519373 65113 1 04 1 02 32 03 265103 (2)A>
152075 1009519374 65114 1 04 1 02 32 03 265104 (1)B>
152076 1009519377 65115 1 04 1 02 32 03 265105 (3)B>
152077 1009519381 65113 1 04 1 02 32 03 265105 <A(4) 4
152078 1009584486 8 1 04 1 02 32 03 <A(4) 465106
152079 1009584488 10 1 04 1 02 32 02 1 (0)B> 465106
152080 1009649594 65116 1 04 1 02 32 02 1 065106 (0)B>
152081 1009649596 65114 1 04 1 02 32 02 1 065106 <B(2) 2
152082 1009714702 8 1 04 1 02 32 02 1 <B(2) 265107
152083 1009714704 10 1 04 1 02 32 02 2 (3)B> 265107
152084 1009779811 65117 1 04 1 02 32 02 2 365107 (3)B>
152085 1009779815 65115 1 04 1 02 32 02 2 365107 <A(4) 4
152086 1009779816 65114 1 04 1 02 32 02 2 365106 <B(4) 42
152087 1009779818 65116 1 04 1 02 32 02 2 365105 2 (2)A> 42
152088 1009779820 65118 1 04 1 02 32 02 2 365105 23 (2)A>
152089 1009779821 65119 1 04 1 02 32 02 2 365105 24 (1)B>
152090 1009779824 65120 1 04 1 02 32 02 2 365105 25 (3)B>
152091 1009779828 65118 1 04 1 02 32 02 2 365105 25 <A(4) 4
152092 1009779833 65113 1 04 1 02 32 02 2 365105 <A(4) 46
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 33+V(1) <A(4) 41+V(2)
1 1 -1 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 32+V(1) <B(4) 42+V(2)
2 3 1 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 2 (2)A> 42+V(2)
3 5+V(2) 3+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 23+V(2) (2)A>
4 6+V(2) 4+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 24+V(2) (1)B>
5 9+V(2) 5+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 25+V(2) (3)B>
6 13+V(2) 3+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 25+V(2) <A(4) 4
7 18+2*V(2) -2 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) <A(4) 46+V(2)
<< Success! ==> defined new CTR 12 (PA)
152092 1009779833 65113 1 04 1 02 32 02 2 365105 <A(4) 46
== Executing PA-CTR 12, V(1)=65102, V(2)=5, repcount=32552, factor=5/2
379956 6308692049 9 1 04 1 02 32 02 2 3 <A(4) 4162766
379957 6308692050 8 1 04 1 02 32 02 2 <B(4) 4162767
379958 6308692052 10 1 04 1 02 32 02 3 (0)B> 4162767
379959 6308854819 162777 1 04 1 02 32 02 3 0162767 (0)B>
379960 6308854821 162775 1 04 1 02 32 02 3 0162767 <B(2) 2
379961 6309017588 8 1 04 1 02 32 02 3 <B(2) 2162768
379962 6309017591 7 1 04 1 02 32 02 <A(4) 4 2162768
379963 6309017593 9 1 04 1 02 32 0 1 (0)B> 4 2162768
379964 6309017594 10 1 04 1 02 32 0 1 0 (0)B> 2162768
379965 6309017595 11 1 04 1 02 32 0 1 02 (3)B> 2162767
379966 6309180362 162778 1 04 1 02 32 0 1 02 3162767 (3)B>
379967 6309180366 162776 1 04 1 02 32 0 1 02 3162767 <A(4) 4
379968 6309180367 162775 1 04 1 02 32 0 1 02 3162766 <B(4) 42
379969 6309180369 162777 1 04 1 02 32 0 1 02 3162765 2 (2)A> 42
379970 6309180371 162779 1 04 1 02 32 0 1 02 3162765 23 (2)A>
379971 6309180372 162780 1 04 1 02 32 0 1 02 3162765 24 (1)B>
379972 6309180375 162781 1 04 1 02 32 0 1 02 3162765 25 (3)B>
379973 6309180379 162779 1 04 1 02 32 0 1 02 3162765 25 <A(4) 4
379974 6309180384 162774 1 04 1 02 32 0 1 02 3162765 <A(4) 46
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 33+V(1) <A(4) 41+V(2)
1 1 -1 [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 32+V(1) <B(4) 42+V(2)
2 3 1 [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 2 (2)A> 42+V(2)
3 5+V(2) 3+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 23+V(2) (2)A>
4 6+V(2) 4+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 24+V(2) (1)B>
5 9+V(2) 5+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 25+V(2) (3)B>
6 13+V(2) 3+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 25+V(2) <A(4) 4
7 18+2*V(2) -2 [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) <A(4) 46+V(2)
<< Success! ==> defined new CTR 13 (PA)
379974 6309180384 162774 1 04 1 02 32 0 1 02 3162765 <A(4) 46
== Executing PA-CTR 13, V(1)=162762, V(2)=5, repcount=81382, factor=5/2
949648 39426201790 10 1 04 1 02 32 0 1 02 3 <A(4) 4406916
949649 39426201791 9 1 04 1 02 32 0 1 02 <B(4) 4406917
949650 39426201792 8 1 04 1 02 32 0 1 0 <B(2) 4406918
949651 39426201793 7 1 04 1 02 32 0 1 <B(2) 2 4406918
949652 39426201795 9 1 04 1 02 32 0 2 (3)B> 2 4406918
949653 39426201796 10 1 04 1 02 32 0 2 3 (3)B> 4406918
949654 39426201797 11 1 04 1 02 32 0 2 32 (0)B> 4406917
949655 39426608714 406928 1 04 1 02 32 0 2 32 0406917 (0)B>
949656 39426608716 406926 1 04 1 02 32 0 2 32 0406917 <B(2) 2
949657 39427015633 9 1 04 1 02 32 0 2 32 <B(2) 2406918
949658 39427015636 8 1 04 1 02 32 0 2 3 <A(4) 4 2406918
949659 39427015637 7 1 04 1 02 32 0 2 <B(4) 42 2406918
949660 39427015639 9 1 04 1 02 32 0 3 (0)B> 42 2406918
949661 39427015641 11 1 04 1 02 32 0 3 02 (0)B> 2406918
949662 39427015642 12 1 04 1 02 32 0 3 03 (3)B> 2406917
949663 39427422559 406929 1 04 1 02 32 0 3 03 3406917 (3)B>
949664 39427422563 406927 1 04 1 02 32 0 3 03 3406917 <A(4) 4
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 [*]* [*]* [*]* [*]* [*]* [*]* 1 02 3 <A(4) 42+V(1)
1 1 -1 [*]* [*]* [*]* [*]* [*]* [*]* 1 02 <B(4) 43+V(1)
2 2 -2 [*]* [*]* [*]* [*]* [*]* [*]* 1 0 <B(2) 44+V(1)
3 3 -3 [*]* [*]* [*]* [*]* [*]* [*]* 1 <B(2) 2 44+V(1)
4 5 -1 [*]* [*]* [*]* [*]* [*]* [*]* 2 (3)B> 2 44+V(1)
5 6 0 [*]* [*]* [*]* [*]* [*]* [*]* 2 3 (3)B> 44+V(1)
6 7 1 [*]* [*]* [*]* [*]* [*]* [*]* 2 32 (0)B> 43+V(1)
7 10+V(1) 4+V(1) [*]* [*]* [*]* [*]* [*]* [*]* 2 32 03+V(1) (0)B>
8 12+V(1) 2+V(1) [*]* [*]* [*]* [*]* [*]* [*]* 2 32 03+V(1) <B(2) 2
9 15+2*V(1) -1 [*]* [*]* [*]* [*]* [*]* [*]* 2 32 <B(2) 24+V(1)
10 18+2*V(1) -2 [*]* [*]* [*]* [*]* [*]* [*]* 2 3 <A(4) 4 24+V(1)
11 19+2*V(1) -3 [*]* [*]* [*]* [*]* [*]* [*]* 2 <B(4) 42 24+V(1)
12 21+2*V(1) -1 [*]* [*]* [*]* [*]* [*]* [*]* 3 (0)B> 42 24+V(1)
13 23+2*V(1) 1 [*]* [*]* [*]* [*]* [*]* [*]* 3 02 (0)B> 24+V(1)
14 24+2*V(1) 2 [*]* [*]* [*]* [*]* [*]* [*]* 3 03 (3)B> 23+V(1)
15 27+3*V(1) 5+V(1) [*]* [*]* [*]* [*]* [*]* [*]* 3 03 33+V(1) (3)B>
16 31+3*V(1) 3+V(1) [*]* [*]* [*]* [*]* [*]* [*]* 3 03 33+V(1) <A(4) 4
<< Success! ==> defined new CTR 14 (PPA)
949664 39427422563 406927 1 04 1 02 32 0 3 03 3406917 <A(4) 4
== Executing PA-CTR 13, V(1)=406914, V(2)=0, repcount=203458, factor=5/2
2373870 246405856337 11 1 04 1 02 32 0 3 03 3 <A(4) 41017291
2373871 246405856338 10 1 04 1 02 32 0 3 03 <B(4) 41017292
2373872 246405856339 9 1 04 1 02 32 0 3 02 <B(2) 41017293
2373873 246405856341 7 1 04 1 02 32 0 3 <B(2) 22 41017293
2373874 246405856344 6 1 04 1 02 32 0 <A(4) 4 22 41017293
2373875 246405856346 8 1 04 1 02 32 1 (0)B> 4 22 41017293
2373876 246405856347 9 1 04 1 02 32 1 0 (0)B> 22 41017293
2373877 246405856348 10 1 04 1 02 32 1 02 (3)B> 2 41017293
2373878 246405856349 11 1 04 1 02 32 1 02 3 (3)B> 41017293
2373879 246405856350 12 1 04 1 02 32 1 02 32 (0)B> 41017292
2373880 246406873642 1017304 1 04 1 02 32 1 02 32 01017292 (0)B>
2373881 246406873644 1017302 1 04 1 02 32 1 02 32 01017292 <B(2) 2
2373882 246407890936 10 1 04 1 02 32 1 02 32 <B(2) 21017293
2373883 246407890939 9 1 04 1 02 32 1 02 3 <A(4) 4 21017293
2373884 246407890940 8 1 04 1 02 32 1 02 <B(4) 42 21017293
2373885 246407890941 7 1 04 1 02 32 1 0 <B(2) 43 21017293
2373886 246407890942 6 1 04 1 02 32 1 <B(2) 2 43 21017293
2373887 246407890944 8 1 04 1 02 32 2 (3)B> 2 43 21017293
2373888 246407890945 9 1 04 1 02 32 2 3 (3)B> 43 21017293
2373889 246407890946 10 1 04 1 02 32 2 32 (0)B> 42 21017293
2373890 246407890948 12 1 04 1 02 32 2 32 02 (0)B> 21017293
2373891 246407890949 13 1 04 1 02 32 2 32 03 (3)B> 21017292
2373892 246408908241 1017305 1 04 1 02 32 2 32 03 31017292 (3)B>
2373893 246408908245 1017303 1 04 1 02 32 2 32 03 31017292 <A(4) 4
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 [*]* [*]* [*]* [*]* [*]* 0 3 03 3 <A(4) 42+V(1)
1 1 -1 [*]* [*]* [*]* [*]* [*]* 0 3 03 <B(4) 43+V(1)
2 2 -2 [*]* [*]* [*]* [*]* [*]* 0 3 02 <B(2) 44+V(1)
3 4 -4 [*]* [*]* [*]* [*]* [*]* 0 3 <B(2) 22 44+V(1)
4 7 -5 [*]* [*]* [*]* [*]* [*]* 0 <A(4) 4 22 44+V(1)
5 9 -3 [*]* [*]* [*]* [*]* [*]* 1 (0)B> 4 22 44+V(1)
6 10 -2 [*]* [*]* [*]* [*]* [*]* 1 0 (0)B> 22 44+V(1)
7 11 -1 [*]* [*]* [*]* [*]* [*]* 1 02 (3)B> 2 44+V(1)
8 12 0 [*]* [*]* [*]* [*]* [*]* 1 02 3 (3)B> 44+V(1)
9 13 1 [*]* [*]* [*]* [*]* [*]* 1 02 32 (0)B> 43+V(1)
10 16+V(1) 4+V(1) [*]* [*]* [*]* [*]* [*]* 1 02 32 03+V(1) (0)B>
11 18+V(1) 2+V(1) [*]* [*]* [*]* [*]* [*]* 1 02 32 03+V(1) <B(2) 2
12 21+2*V(1) -1 [*]* [*]* [*]* [*]* [*]* 1 02 32 <B(2) 24+V(1)
13 24+2*V(1) -2 [*]* [*]* [*]* [*]* [*]* 1 02 3 <A(4) 4 24+V(1)
14 25+2*V(1) -3 [*]* [*]* [*]* [*]* [*]* 1 02 <B(4) 42 24+V(1)
15 26+2*V(1) -4 [*]* [*]* [*]* [*]* [*]* 1 0 <B(2) 43 24+V(1)
16 27+2*V(1) -5 [*]* [*]* [*]* [*]* [*]* 1 <B(2) 2 43 24+V(1)
17 29+2*V(1) -3 [*]* [*]* [*]* [*]* [*]* 2 (3)B> 2 43 24+V(1)
18 30+2*V(1) -2 [*]* [*]* [*]* [*]* [*]* 2 3 (3)B> 43 24+V(1)
19 31+2*V(1) -1 [*]* [*]* [*]* [*]* [*]* 2 32 (0)B> 42 24+V(1)
20 33+2*V(1) 1 [*]* [*]* [*]* [*]* [*]* 2 32 02 (0)B> 24+V(1)
21 34+2*V(1) 2 [*]* [*]* [*]* [*]* [*]* 2 32 03 (3)B> 23+V(1)
22 37+3*V(1) 5+V(1) [*]* [*]* [*]* [*]* [*]* 2 32 03 33+V(1) (3)B>
23 41+3*V(1) 3+V(1) [*]* [*]* [*]* [*]* [*]* 2 32 03 33+V(1) <A(4) 4
<< Success! ==> defined new CTR 15 (PPA)
2373893 246408908245 1017303 1 04 1 02 32 2 32 03 31017292 <A(4) 4
== Executing PA-CTR 13, V(1)=1017289, V(2)=0, repcount=508645, factor=5/2
5934408 1540014200755 13 1 04 1 02 32 2 32 03 32 <A(4) 42543226
5934409 1540014200756 12 1 04 1 02 32 2 32 03 3 <B(4) 42543227
5934410 1540014200758 14 1 04 1 02 32 2 32 03 2 (2)A> 42543227
5934411 1540016743985 2543241 1 04 1 02 32 2 32 03 22543228 (2)A>
5934412 1540016743986 2543242 1 04 1 02 32 2 32 03 22543229 (1)B>
5934413 1540016743989 2543243 1 04 1 02 32 2 32 03 22543230 (3)B>
5934414 1540016743993 2543241 1 04 1 02 32 2 32 03 22543230 <A(4) 4
5934415 1540019287223 11 1 04 1 02 32 2 32 03 <A(4) 42543231
5934416 1540019287225 13 1 04 1 02 32 2 32 02 1 (0)B> 42543231
5934417 1540021830456 2543244 1 04 1 02 32 2 32 02 1 02543231 (0)B>
5934418 1540021830458 2543242 1 04 1 02 32 2 32 02 1 02543231 <B(2) 2
5934419 1540024373689 11 1 04 1 02 32 2 32 02 1 <B(2) 22543232
5934420 1540024373691 13 1 04 1 02 32 2 32 02 2 (3)B> 22543232
5934421 1540026916923 2543245 1 04 1 02 32 2 32 02 2 32543232 (3)B>
5934422 1540026916927 2543243 1 04 1 02 32 2 32 02 2 32543232 <A(4) 4
5934423 1540026916928 2543242 1 04 1 02 32 2 32 02 2 32543231 <B(4) 42
5934424 1540026916930 2543244 1 04 1 02 32 2 32 02 2 32543230 2 (2)A> 42
5934425 1540026916932 2543246 1 04 1 02 32 2 32 02 2 32543230 23 (2)A>
5934426 1540026916933 2543247 1 04 1 02 32 2 32 02 2 32543230 24 (1)B>
5934427 1540026916936 2543248 1 04 1 02 32 2 32 02 2 32543230 25 (3)B>
5934428 1540026916940 2543246 1 04 1 02 32 2 32 02 2 32543230 25 <A(4) 4
5934429 1540026916945 2543241 1 04 1 02 32 2 32 02 2 32543230 <A(4) 46
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 33+V(1) <A(4) 41+V(2)
1 1 -1 [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 32+V(1) <B(4) 42+V(2)
2 3 1 [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 2 (2)A> 42+V(2)
3 5+V(2) 3+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 23+V(2) (2)A>
4 6+V(2) 4+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 24+V(2) (1)B>
5 9+V(2) 5+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 25+V(2) (3)B>
6 13+V(2) 3+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 25+V(2) <A(4) 4
7 18+2*V(2) -2 [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) <A(4) 46+V(2)
<< Success! ==> defined new CTR 16 (PA)
5934429 1540026916945 2543241 1 04 1 02 32 2 32 02 2 32543230 <A(4) 46
== Executing PA-CTR 16, V(1)=2543227, V(2)=5, repcount=1271614, factor=5/2
14835727 9625066989047 13 1 04 1 02 32 2 32 02 2 32 <A(4) 46358076
14835728 9625066989048 12 1 04 1 02 32 2 32 02 2 3 <B(4) 46358077
14835729 9625066989050 14 1 04 1 02 32 2 32 02 22 (2)A> 46358077
14835730 9625073347127 6358091 1 04 1 02 32 2 32 02 26358079 (2)A>
14835731 9625073347128 6358092 1 04 1 02 32 2 32 02 26358080 (1)B>
14835732 9625073347131 6358093 1 04 1 02 32 2 32 02 26358081 (3)B>
14835733 9625073347135 6358091 1 04 1 02 32 2 32 02 26358081 <A(4) 4
14835734 9625079705216 10 1 04 1 02 32 2 32 02 <A(4) 46358082
14835735 9625079705218 12 1 04 1 02 32 2 32 0 1 (0)B> 46358082
14835736 9625086063300 6358094 1 04 1 02 32 2 32 0 1 06358082 (0)B>
14835737 9625086063302 6358092 1 04 1 02 32 2 32 0 1 06358082 <B(2) 2
14835738 9625092421384 10 1 04 1 02 32 2 32 0 1 <B(2) 26358083
14835739 9625092421386 12 1 04 1 02 32 2 32 0 2 (3)B> 26358083
14835740 9625098779469 6358095 1 04 1 02 32 2 32 0 2 36358083 (3)B>
14835741 9625098779473 6358093 1 04 1 02 32 2 32 0 2 36358083 <A(4) 4
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 02+V(2) 21+V(1) 32 <A(4) 41+V(3)
1 1 -1 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 02+V(2) 21+V(1) 3 <B(4) 42+V(3)
2 3 1 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 02+V(2) 22+V(1) (2)A> 42+V(3)
3 5+V(3) 3+V(3) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 02+V(2) 24+V(1)+V(3) (2)A>
4 6+V(3) 4+V(3) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 02+V(2) 25+V(1)+V(3) (1)B>
5 9+V(3) 5+V(3) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 02+V(2) 26+V(1)+V(3) (3)B>
6 13+V(3) 3+V(3) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 02+V(2) 26+V(1)+V(3) <A(4) 4
7 19+V(1)+2*V(3) -3+-1*V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 02+V(2) <A(4) 47+V(1)+V(3)
8 21+V(1)+2*V(3) -1+-1*V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 01+V(2) 1 (0)B> 47+V(1)+V(3)
9 28+2*V(1)+3*V(3) 6+V(3) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 01+V(2) 1 07+V(1)+V(3) (0)B>
10 30+2*V(1)+3*V(3) 4+V(3) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 01+V(2) 1 07+V(1)+V(3) <B(2) 2
11 37+3*V(1)+4*V(3) -3+-1*V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 01+V(2) 1 <B(2) 28+V(1)+V(3)
12 39+3*V(1)+4*V(3) -1+-1*V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 01+V(2) 2 (3)B> 28+V(1)+V(3)
13 47+4*V(1)+5*V(3) 7+V(3) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 01+V(2) 2 38+V(1)+V(3) (3)B>
14 51+4*V(1)+5*V(3) 5+V(3) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 01+V(2) 2 38+V(1)+V(3) <A(4) 4
<< Success! ==> defined new CTR 17 (PPA)
14835741 9625098779473 6358093 1 04 1 02 32 2 32 0 2 36358083 <A(4) 4
== Executing PA-CTR 16, V(1)=6358080, V(2)=0, repcount=3179041, factor=5/2
37089028 60156648505411 11 1 04 1 02 32 2 32 0 2 3 <A(4) 415895206
37089029 60156648505412 10 1 04 1 02 32 2 32 0 2 <B(4) 415895207
37089030 60156648505414 12 1 04 1 02 32 2 32 0 3 (0)B> 415895207
37089031 60156664400621 15895219 1 04 1 02 32 2 32 0 3 015895207 (0)B>
37089032 60156664400623 15895217 1 04 1 02 32 2 32 0 3 015895207 <B(2) 2
37089033 60156680295830 10 1 04 1 02 32 2 32 0 3 <B(2) 215895208
37089034 60156680295833 9 1 04 1 02 32 2 32 0 <A(4) 4 215895208
37089035 60156680295835 11 1 04 1 02 32 2 32 1 (0)B> 4 215895208
37089036 60156680295836 12 1 04 1 02 32 2 32 1 0 (0)B> 215895208
37089037 60156680295837 13 1 04 1 02 32 2 32 1 02 (3)B> 215895207
37089038 60156696191044 15895220 1 04 1 02 32 2 32 1 02 315895207 (3)B>
37089039 60156696191048 15895218 1 04 1 02 32 2 32 1 02 315895207 <A(4) 4
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 0 2 3 <A(4) 42+V(1)
1 1 -1 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 0 2 <B(4) 43+V(1)
2 3 1 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 0 3 (0)B> 43+V(1)
3 6+V(1) 4+V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 0 3 03+V(1) (0)B>
4 8+V(1) 2+V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 0 3 03+V(1) <B(2) 2
5 11+2*V(1) -1 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 0 3 <B(2) 24+V(1)
6 14+2*V(1) -2 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 0 <A(4) 4 24+V(1)
7 16+2*V(1) 0 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 1 (0)B> 4 24+V(1)
8 17+2*V(1) 1 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 1 0 (0)B> 24+V(1)
9 18+2*V(1) 2 [*]* [*]* [*]* [*]* [*]* [*]* [*]* 1 02 (3)B> 23+V(1)
10 21+3*V(1) 5+V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 1 02 33+V(1) (3)B>
11 25+3*V(1) 3+V(1) [*]* [*]* [*]* [*]* [*]* [*]* [*]* 1 02 33+V(1) <A(4) 4
<< Success! ==> defined new CTR 18 (PPA)
37089039 60156696191048 15895218 1 04 1 02 32 2 32 1 02 315895207 <A(4) 4
== Executing PA-CTR 16, V(1)=15895204, V(2)=0, repcount=7947603, factor=5/2
92722260 375978766737932 12 1 04 1 02 32 2 32 1 02 3 <A(4) 439738016
92722261 375978766737933 11 1 04 1 02 32 2 32 1 02 <B(4) 439738017
92722262 375978766737934 10 1 04 1 02 32 2 32 1 0 <B(2) 439738018
92722263 375978766737935 9 1 04 1 02 32 2 32 1 <B(2) 2 439738018
92722264 375978766737937 11 1 04 1 02 32 2 32 2 (3)B> 2 439738018
92722265 375978766737938 12 1 04 1 02 32 2 32 2 3 (3)B> 439738018
92722266 375978766737939 13 1 04 1 02 32 2 32 2 32 (0)B> 439738017
92722267 375978806475956 39738030 1 04 1 02 32 2 32 2 32 039738017 (0)B>
92722268 375978806475958 39738028 1 04 1 02 32 2 32 2 32 039738017 <B(2) 2
92722269 375978846213975 11 1 04 1 02 32 2 32 2 32 <B(2) 239738018
92722270 375978846213978 10 1 04 1 02 32 2 32 2 3 <A(4) 4 239738018
92722271 375978846213979 9 1 04 1 02 32 2 32 2 <B(4) 42 239738018
92722272 375978846213981 11 1 04 1 02 32 2 33 (0)B> 42 239738018
92722273 375978846213983 13 1 04 1 02 32 2 33 02 (0)B> 239738018
92722274 375978846213984 14 1 04 1 02 32 2 33 03 (3)B> 239738017
92722275 375978885952001 39738031 1 04 1 02 32 2 33 03 339738017 (3)B>
92722276 375978885952005 39738029 1 04 1 02 32 2 33 03 339738017 <A(4) 4
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 1 02 3 <A(4) 42+V(2)
1 1 -1 [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 1 02 <B(4) 43+V(2)
2 2 -2 [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 1 0 <B(2) 44+V(2)
3 3 -3 [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 1 <B(2) 2 44+V(2)
4 5 -1 [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 2 (3)B> 2 44+V(2)
5 6 0 [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 2 3 (3)B> 44+V(2)
6 7 1 [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 2 32 (0)B> 43+V(2)
7 10+V(2) 4+V(2) [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 2 32 03+V(2) (0)B>
8 12+V(2) 2+V(2) [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 2 32 03+V(2) <B(2) 2
9 15+2*V(2) -1 [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 2 32 <B(2) 24+V(2)
10 18+2*V(2) -2 [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 2 3 <A(4) 4 24+V(2)
11 19+2*V(2) -3 [*]* [*]* [*]* [*]* [*]* [*]* 31+V(1) 2 <B(4) 42 24+V(2)
12 21+2*V(2) -1 [*]* [*]* [*]* [*]* [*]* [*]* 32+V(1) (0)B> 42 24+V(2)
13 23+2*V(2) 1 [*]* [*]* [*]* [*]* [*]* [*]* 32+V(1) 02 (0)B> 24+V(2)
14 24+2*V(2) 2 [*]* [*]* [*]* [*]* [*]* [*]* 32+V(1) 03 (3)B> 23+V(2)
15 27+3*V(2) 5+V(2) [*]* [*]* [*]* [*]* [*]* [*]* 32+V(1) 03 33+V(2) (3)B>
16 31+3*V(2) 3+V(2) [*]* [*]* [*]* [*]* [*]* [*]* 32+V(1) 03 33+V(2) <A(4) 4
<< Success! ==> defined new CTR 19 (PPA)
92722276 375978885952005 39738029 1 04 1 02 32 2 33 03 339738017 <A(4) 4
== Executing PA-CTR 13, V(1)=39738014, V(2)=0, repcount=19869008, factor=5/2
231805332 2349866538769429 13 1 04 1 02 32 2 33 03 3 <A(4) 499345041
231805333 2349866538769430 12 1 04 1 02 32 2 33 03 <B(4) 499345042
231805334 2349866538769431 11 1 04 1 02 32 2 33 02 <B(2) 499345043
231805335 2349866538769433 9 1 04 1 02 32 2 33 <B(2) 22 499345043
231805336 2349866538769436 8 1 04 1 02 32 2 32 <A(4) 4 22 499345043
231805337 2349866538769437 7 1 04 1 02 32 2 3 <B(4) 42 22 499345043
231805338 2349866538769439 9 1 04 1 02 32 22 (2)A> 42 22 499345043
231805339 2349866538769441 11 1 04 1 02 32 24 (2)A> 22 499345043
231805340 2349866538769443 9 1 04 1 02 32 24 <A(4) 4 2 499345043
231805341 2349866538769447 5 1 04 1 02 32 <A(4) 45 2 499345043
231805342 2349866538769448 4 1 04 1 02 3 <B(4) 46 2 499345043
231805343 2349866538769450 6 1 04 1 02 2 (2)A> 46 2 499345043
231805344 2349866538769456 12 1 04 1 02 27 (2)A> 2 499345043
231805345 2349866538769458 10 1 04 1 02 27 <A(4) 499345044
231805346 2349866538769465 3 1 04 1 02 <A(4) 499345051
231805347 2349866538769467 5 1 04 1 0 1 (0)B> 499345051
231805348 2349866638114518 99345056 1 04 1 0 1 099345051 (0)B>
231805349 2349866638114520 99345054 1 04 1 0 1 099345051 <B(2) 2
231805350 2349866737459571 3 1 04 1 0 1 <B(2) 299345052
231805351 2349866737459573 5 1 04 1 0 2 (3)B> 299345052
231805352 2349866836804625 99345057 1 04 1 0 2 399345052 (3)B>
231805353 2349866836804629 99345055 1 04 1 0 2 399345052 <A(4) 4
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 [*]* [*]* [*]* 02+V(2) 32 21+V(1) 33 03 3 <A(4) 41+V(3)
1 1 -1 [*]* [*]* [*]* 02+V(2) 32 21+V(1) 33 03 <B(4) 42+V(3)
2 2 -2 [*]* [*]* [*]* 02+V(2) 32 21+V(1) 33 02 <B(2) 43+V(3)
3 4 -4 [*]* [*]* [*]* 02+V(2) 32 21+V(1) 33 <B(2) 22 43+V(3)
4 7 -5 [*]* [*]* [*]* 02+V(2) 32 21+V(1) 32 <A(4) 4 22 43+V(3)
5 8 -6 [*]* [*]* [*]* 02+V(2) 32 21+V(1) 3 <B(4) 42 22 43+V(3)
6 10 -4 [*]* [*]* [*]* 02+V(2) 32 22+V(1) (2)A> 42 22 43+V(3)
7 12 -2 [*]* [*]* [*]* 02+V(2) 32 24+V(1) (2)A> 22 43+V(3)
8 14 -4 [*]* [*]* [*]* 02+V(2) 32 24+V(1) <A(4) 4 2 43+V(3)
9 18+V(1) -8+-1*V(1) [*]* [*]* [*]* 02+V(2) 32 <A(4) 45+V(1) 2 43+V(3)
10 19+V(1) -9+-1*V(1) [*]* [*]* [*]* 02+V(2) 3 <B(4) 46+V(1) 2 43+V(3)
11 21+V(1) -7+-1*V(1) [*]* [*]* [*]* 02+V(2) 2 (2)A> 46+V(1) 2 43+V(3)
12 27+2*V(1) -1 [*]* [*]* [*]* 02+V(2) 27+V(1) (2)A> 2 43+V(3)
13 29+2*V(1) -3 [*]* [*]* [*]* 02+V(2) 27+V(1) <A(4) 44+V(3)
14 36+3*V(1) -10+-1*V(1) [*]* [*]* [*]* 02+V(2) <A(4) 411+V(1)+V(3)
15 38+3*V(1) -8+-1*V(1) [*]* [*]* [*]* 01+V(2) 1 (0)B> 411+V(1)+V(3)
16 49+4*V(1)+V(3) 3+V(3) [*]* [*]* [*]* 01+V(2) 1 011+V(1)+V(3) (0)B>
17 51+4*V(1)+V(3) 1+V(3) [*]* [*]* [*]* 01+V(2) 1 011+V(1)+V(3) <B(2) 2
18 62+5*V(1)+2*V(3) -10+-1*V(1) [*]* [*]* [*]* 01+V(2) 1 <B(2) 212+V(1)+V(3)
19 64+5*V(1)+2*V(3) -8+-1*V(1) [*]* [*]* [*]* 01+V(2) 2 (3)B> 212+V(1)+V(3)
20 76+6*V(1)+3*V(3) 4+V(3) [*]* [*]* [*]* 01+V(2) 2 312+V(1)+V(3) (3)B>
21 80+6*V(1)+3*V(3) 2+V(3) [*]* [*]* [*]* 01+V(2) 2 312+V(1)+V(3) <A(4) 4
<< Success! ==> defined new CTR 20 (PPA)
231805353 2349866836804629 99345055 1 04 1 0 2 399345052 <A(4) 4
== Executing PA-CTR 6, V(1)=99345049, V(2)=0, repcount=49672525, factor=5/2
579513028 14686666181925579 5 1 04 1 0 2 32 <A(4) 4248362626
579513029 14686666181925580 4 1 04 1 0 2 3 <B(4) 4248362627
579513030 14686666181925582 6 1 04 1 0 22 (2)A> 4248362627
579513031 14686666430288209 248362633 1 04 1 0 2248362629 (2)A>
579513032 14686666430288210 248362634 1 04 1 0 2248362630 (1)B>
579513033 14686666430288213 248362635 1 04 1 0 2248362631 (3)B>
579513034 14686666430288217 248362633 1 04 1 0 2248362631 <A(4) 4
579513035 14686666678650848 2 1 04 1 0 <A(4) 4248362632
579513036 14686666678650850 4 1 04 12 (0)B> 4248362632
579513037 14686666927013482 248362636 1 04 12 0248362632 (0)B>
579513038 14686666927013484 248362634 1 04 12 0248362632 <B(2) 2
579513039 14686667175376116 2 1 04 12 <B(2) 2248362633
579513040 14686667175376118 4 1 04 1 2 (3)B> 2248362633
579513041 14686667423738751 248362637 1 04 1 2 3248362633 (3)B>
579513042 14686667423738755 248362635 1 04 1 2 3248362633 <A(4) 4
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 [*]* [*]* 11+V(2) 0 21+V(1) 32 <A(4) 41+V(3)
1 1 -1 [*]* [*]* 11+V(2) 0 21+V(1) 3 <B(4) 42+V(3)
2 3 1 [*]* [*]* 11+V(2) 0 22+V(1) (2)A> 42+V(3)
3 5+V(3) 3+V(3) [*]* [*]* 11+V(2) 0 24+V(1)+V(3) (2)A>
4 6+V(3) 4+V(3) [*]* [*]* 11+V(2) 0 25+V(1)+V(3) (1)B>
5 9+V(3) 5+V(3) [*]* [*]* 11+V(2) 0 26+V(1)+V(3) (3)B>
6 13+V(3) 3+V(3) [*]* [*]* 11+V(2) 0 26+V(1)+V(3) <A(4) 4
7 19+V(1)+2*V(3) -3+-1*V(1) [*]* [*]* 11+V(2) 0 <A(4) 47+V(1)+V(3)
8 21+V(1)+2*V(3) -1+-1*V(1) [*]* [*]* 12+V(2) (0)B> 47+V(1)+V(3)
9 28+2*V(1)+3*V(3) 6+V(3) [*]* [*]* 12+V(2) 07+V(1)+V(3) (0)B>
10 30+2*V(1)+3*V(3) 4+V(3) [*]* [*]* 12+V(2) 07+V(1)+V(3) <B(2) 2
11 37+3*V(1)+4*V(3) -3+-1*V(1) [*]* [*]* 12+V(2) <B(2) 28+V(1)+V(3)
12 39+3*V(1)+4*V(3) -1+-1*V(1) [*]* [*]* 11+V(2) 2 (3)B> 28+V(1)+V(3)
13 47+4*V(1)+5*V(3) 7+V(3) [*]* [*]* 11+V(2) 2 38+V(1)+V(3) (3)B>
14 51+4*V(1)+5*V(3) 5+V(3) [*]* [*]* 11+V(2) 2 38+V(1)+V(3) <A(4) 4
<< Success! ==> defined new CTR 21 (PPA)
579513042 14686667423738755 248362635 1 04 1 2 3248362633 <A(4) 4
== Executing PA-CTR 5, V(1)=248362630, V(2)=0, repcount=124181316, factor=5/2
1448782254 91791665255555143 3 1 04 1 2 3 <A(4) 4620906581
1448782255 91791665255555144 2 1 04 1 2 <B(4) 4620906582
1448782256 91791665255555146 4 1 04 1 3 (0)B> 4620906582
1448782257 91791665876461728 620906586 1 04 1 3 0620906582 (0)B>
1448782258 91791665876461730 620906584 1 04 1 3 0620906582 <B(2) 2
1448782259 91791666497368312 2 1 04 1 3 <B(2) 2620906583
1448782260 91791666497368315 1 1 04 1 <A(4) 4 2620906583
1448782261 91791666497368316 2 1 04 1 H> 4 4 2620906583 [stop]
Lines: 451
Top steps: 450
Macro steps: 1448782261
Basic steps: 91791666497368316
Tape index: 2
nonzeros: 620906587
log10(nonzeros): 8.793
log10(steps ): 16.963
Run state: stop
Input to awk program:
gohalt 1
nbs 5
T 2-state 5-symbol #g from T.J. & S. Ligocki
5T 1RB 1RH 4LA 4LB 2RA 2LB 2RB 3RB 2RA 0RB
: 620,906,587 91,791,666,497,368,316
L 3
M 600
pref sim
machv Lig25_g just simple
machv Lig25_g-r with repetitions reduced
machv Lig25_g-1 with tape symbol exponents
machv Lig25_g-m as 1-bck-macro machine
machv Lig25_g-a as 1-bck-macro machine with pure additive config-TRs
iam Lig25_g-a
mtype 1 0
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:12:46 CEST 2010
edate Tue Jul 6 22:12:49 CEST 2010
bnspeed 1
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:12:46 CEST 2010