Comment: This TM produces 17485734 ones in 95547257425490 steps.
| State | on 0 |
on 1 |
on 0 | on 1 | ||||
|---|---|---|---|---|---|---|---|---|
| Move | Goto | Move | Goto | |||||
| A | B1R | C0L | 1 | right | B | 0 | left | C |
| B | A1L | A0R | 1 | left | A | 0 | right | A |
| C | D0L | Z1R | 0 | left | D | 1 | right | Z |
| D | E1R | D1L | 1 | right | E | 1 | left | D |
| E | F0L | E0L | 0 | left | F | 0 | left | E |
| F | F1R | B0L | 1 | right | F | 0 | left | 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 3 -1 <C(0) 1
3 4 -2 <D(0) 0 1
4 7 -3 <B(0) 02 1
5 8 -4 <A(1) 03 1
6 10 -2 1 (0)A> 03 1
7 11 -1 1 0 (1)B> 02 1
8 13 -3 1 0 <C(0) 1 0 1
9 14 -4 1 <D(0) 0 1 0 1
10 15 -5 <D(1) 02 1 0 1
11 18 -6 <E(0) 03 1 0 1
12 19 -7 <F(0) 04 1 0 1
13 21 -5 1 (1)F> 04 1 0 1
14 25 -1 15 (1)F> 1 0 1
15 28 0 15 0 (1)B> 0 1
16 30 -2 15 0 <C(0) 12
17 31 -3 15 <D(0) 0 12
18 32 -4 14 <D(1) 02 12
19 36 -8 <D(1) 14 02 12
20 39 -9 <E(0) 0 14 02 12
21 40 -10 <F(0) 02 14 02 12
22 42 -8 1 (1)F> 02 14 02 12
23 44 -6 13 (1)F> 14 02 12
24 47 -5 13 0 (1)B> 13 02 12
25 48 -4 13 0 1 (0)A> 12 02 12
26 50 -6 13 0 1 <D(0) 0 1 02 12
27 51 -7 13 0 <D(1) 02 1 02 12
28 54 -8 13 <E(0) 03 1 02 12
29 57 -11 <E(0) 06 1 02 12
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <E(0) 01+V(2) 14+V(1) [*]* [*]*
1 1 -1 <F(0) 02+V(2) 14+V(1) [*]* [*]*
2 3 1 1 (1)F> 02+V(2) 14+V(1) [*]* [*]*
3 5+V(2) 3+V(2) 13+V(2) (1)F> 14+V(1) [*]* [*]*
4 8+V(2) 4+V(2) 13+V(2) 0 (1)B> 13+V(1) [*]* [*]*
5 9+V(2) 5+V(2) 13+V(2) 0 1 (0)A> 12+V(1) [*]* [*]*
6 11+V(2) 3+V(2) 13+V(2) 0 1 <D(0) 0 11+V(1) [*]* [*]*
7 12+V(2) 2+V(2) 13+V(2) 0 <D(1) 02 11+V(1) [*]* [*]*
8 15+V(2) 1+V(2) 13+V(2) <E(0) 03 11+V(1) [*]* [*]*
9 18+2*V(2) -2 <E(0) 06+V(2) 11+V(1) [*]* [*]*
<< Success! ==> defined new CTR 1 (PA)
30 58 -12 <F(0) 07 1 02 12
31 60 -10 1 (1)F> 07 1 02 12
32 67 -3 18 (1)F> 1 02 12
33 70 -2 18 0 (1)B> 02 12
34 72 -4 18 0 <C(0) 1 0 12
35 73 -5 18 <D(0) 0 1 0 12
36 74 -6 17 <D(1) 02 1 0 12
37 81 -13 <D(1) 17 02 1 0 12
38 84 -14 <E(0) 0 17 02 1 0 12
39 85 -15 <F(0) 02 17 02 1 0 12
40 87 -13 1 (1)F> 02 17 02 1 0 12
41 89 -11 13 (1)F> 17 02 1 0 12
42 92 -10 13 0 (1)B> 16 02 1 0 12
43 93 -9 13 0 1 (0)A> 15 02 1 0 12
44 95 -11 13 0 1 <D(0) 0 14 02 1 0 12
45 96 -12 13 0 <D(1) 02 14 02 1 0 12
46 99 -13 13 <E(0) 03 14 02 1 0 12
47 102 -16 <E(0) 06 14 02 1 0 12
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <E(0) 01+V(2) 14+V(1) [*]* [*]* [*]* [*]*
1 1 -1 <F(0) 02+V(2) 14+V(1) [*]* [*]* [*]* [*]*
2 3 1 1 (1)F> 02+V(2) 14+V(1) [*]* [*]* [*]* [*]*
3 5+V(2) 3+V(2) 13+V(2) (1)F> 14+V(1) [*]* [*]* [*]* [*]*
4 8+V(2) 4+V(2) 13+V(2) 0 (1)B> 13+V(1) [*]* [*]* [*]* [*]*
5 9+V(2) 5+V(2) 13+V(2) 0 1 (0)A> 12+V(1) [*]* [*]* [*]* [*]*
6 11+V(2) 3+V(2) 13+V(2) 0 1 <D(0) 0 11+V(1) [*]* [*]* [*]* [*]*
7 12+V(2) 2+V(2) 13+V(2) 0 <D(1) 02 11+V(1) [*]* [*]* [*]* [*]*
8 15+V(2) 1+V(2) 13+V(2) <E(0) 03 11+V(1) [*]* [*]* [*]* [*]*
9 18+2*V(2) -2 <E(0) 06+V(2) 11+V(1) [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 2 (PA)
47 102 -16 <E(0) 06 14 02 1 0 12
== Executing PA-CTR 2, V(1)=0, V(2)=5, repcount=1, factor=5/3
56 130 -18 <E(0) 011 1 02 1 0 12
57 131 -19 <F(0) 012 1 02 1 0 12
58 133 -17 1 (1)F> 012 1 02 1 0 12
59 145 -5 113 (1)F> 1 02 1 0 12
60 148 -4 113 0 (1)B> 02 1 0 12
61 150 -6 113 0 <C(0) 1 0 1 0 12
62 151 -7 113 <D(0) 0 1 0 1 0 12
63 152 -8 112 <D(1) 02 1 0 1 0 12
64 164 -20 <D(1) 112 02 1 0 1 0 12
65 167 -21 <E(0) 0 112 02 1 0 1 0 12
66 168 -22 <F(0) 02 112 02 1 0 1 0 12
67 170 -20 1 (1)F> 02 112 02 1 0 1 0 12
68 172 -18 13 (1)F> 112 02 1 0 1 0 12
69 175 -17 13 0 (1)B> 111 02 1 0 1 0 12
70 176 -16 13 0 1 (0)A> 110 02 1 0 1 0 12
71 178 -18 13 0 1 <D(0) 0 19 02 1 0 1 0 12
72 179 -19 13 0 <D(1) 02 19 02 1 0 1 0 12
73 182 -20 13 <E(0) 03 19 02 1 0 1 0 12
74 185 -23 <E(0) 06 19 02 1 0 1 0 12
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <E(0) 01+V(2) 14+V(1) [*]* [*]* [*]* [*]* [*]* [*]*
1 1 -1 <F(0) 02+V(2) 14+V(1) [*]* [*]* [*]* [*]* [*]* [*]*
2 3 1 1 (1)F> 02+V(2) 14+V(1) [*]* [*]* [*]* [*]* [*]* [*]*
3 5+V(2) 3+V(2) 13+V(2) (1)F> 14+V(1) [*]* [*]* [*]* [*]* [*]* [*]*
4 8+V(2) 4+V(2) 13+V(2) 0 (1)B> 13+V(1) [*]* [*]* [*]* [*]* [*]* [*]*
5 9+V(2) 5+V(2) 13+V(2) 0 1 (0)A> 12+V(1) [*]* [*]* [*]* [*]* [*]* [*]*
6 11+V(2) 3+V(2) 13+V(2) 0 1 <D(0) 0 11+V(1) [*]* [*]* [*]* [*]* [*]* [*]*
7 12+V(2) 2+V(2) 13+V(2) 0 <D(1) 02 11+V(1) [*]* [*]* [*]* [*]* [*]* [*]*
8 15+V(2) 1+V(2) 13+V(2) <E(0) 03 11+V(1) [*]* [*]* [*]* [*]* [*]* [*]*
9 18+2*V(2) -2 <E(0) 06+V(2) 11+V(1) [*]* [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 3 (PA)
74 185 -23 <E(0) 06 19 02 1 0 1 0 12
== Executing PA-CTR 3, V(1)=5, V(2)=5, repcount=2, factor=5/3
92 251 -27 <E(0) 016 13 02 1 0 1 0 12
93 252 -28 <F(0) 017 13 02 1 0 1 0 12
94 254 -26 1 (1)F> 017 13 02 1 0 1 0 12
95 271 -9 118 (1)F> 13 02 1 0 1 0 12
96 274 -8 118 0 (1)B> 12 02 1 0 1 0 12
97 275 -7 118 0 1 (0)A> 1 02 1 0 1 0 12
98 277 -9 118 0 1 <D(0) 03 1 0 1 0 12
99 278 -10 118 0 <D(1) 04 1 0 1 0 12
100 281 -11 118 <E(0) 05 1 0 1 0 12
101 299 -29 <E(0) 023 1 0 1 0 12
102 300 -30 <F(0) 024 1 0 1 0 12
103 302 -28 1 (1)F> 024 1 0 1 0 12
104 326 -4 125 (1)F> 1 0 1 0 12
105 329 -3 125 0 (1)B> 0 1 0 12
106 331 -5 125 0 <C(0) 12 0 12
107 332 -6 125 <D(0) 0 12 0 12
108 333 -7 124 <D(1) 02 12 0 12
109 357 -31 <D(1) 124 02 12 0 12
110 360 -32 <E(0) 0 124 02 12 0 12
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 <E(0) 01+V(3) 13 01+V(2) 1 0 11+V(1) [*]* [*]*
1 1 -1 <F(0) 02+V(3) 13 01+V(2) 1 0 11+V(1) [*]* [*]*
2 3 1 1 (1)F> 02+V(3) 13 01+V(2) 1 0 11+V(1) [*]* [*]*
3 5+V(3) 3+V(3) 13+V(3) (1)F> 13 01+V(2) 1 0 11+V(1) [*]* [*]*
4 8+V(3) 4+V(3) 13+V(3) 0 (1)B> 12 01+V(2) 1 0 11+V(1) [*]* [*]*
5 9+V(3) 5+V(3) 13+V(3) 0 1 (0)A> 1 01+V(2) 1 0 11+V(1) [*]* [*]*
6 11+V(3) 3+V(3) 13+V(3) 0 1 <D(0) 02+V(2) 1 0 11+V(1) [*]* [*]*
7 12+V(3) 2+V(3) 13+V(3) 0 <D(1) 03+V(2) 1 0 11+V(1) [*]* [*]*
8 15+V(3) 1+V(3) 13+V(3) <E(0) 04+V(2) 1 0 11+V(1) [*]* [*]*
9 18+2*V(3) -2 <E(0) 07+V(2)+V(3) 1 0 11+V(1) [*]* [*]*
10 19+2*V(3) -3 <F(0) 08+V(2)+V(3) 1 0 11+V(1) [*]* [*]*
11 21+2*V(3) -1 1 (1)F> 08+V(2)+V(3) 1 0 11+V(1) [*]* [*]*
12 29+V(2)+3*V(3) 7+V(2)+V(3) 19+V(2)+V(3) (1)F> 1 0 11+V(1) [*]* [*]*
13 32+V(2)+3*V(3) 8+V(2)+V(3) 19+V(2)+V(3) 0 (1)B> 0 11+V(1) [*]* [*]*
14 34+V(2)+3*V(3) 6+V(2)+V(3) 19+V(2)+V(3) 0 <C(0) 12+V(1) [*]* [*]*
15 35+V(2)+3*V(3) 5+V(2)+V(3) 19+V(2)+V(3) <D(0) 0 12+V(1) [*]* [*]*
16 36+V(2)+3*V(3) 4+V(2)+V(3) 18+V(2)+V(3) <D(1) 02 12+V(1) [*]* [*]*
17 44+2*V(2)+4*V(3) -4 <D(1) 18+V(2)+V(3) 02 12+V(1) [*]* [*]*
18 47+2*V(2)+4*V(3) -5 <E(0) 0 18+V(2)+V(3) 02 12+V(1) [*]* [*]*
<< Success! ==> defined new CTR 4 (PPA)
110 360 -32 <E(0) 0 124 02 12 0 12
== Executing PA-CTR 2, V(1)=20, V(2)=0, repcount=7, factor=5/3
173 696 -46 <E(0) 036 13 02 12 0 12
174 697 -47 <F(0) 037 13 02 12 0 12
175 699 -45 1 (1)F> 037 13 02 12 0 12
176 736 -8 138 (1)F> 13 02 12 0 12
177 739 -7 138 0 (1)B> 12 02 12 0 12
178 740 -6 138 0 1 (0)A> 1 02 12 0 12
179 742 -8 138 0 1 <D(0) 03 12 0 12
180 743 -9 138 0 <D(1) 04 12 0 12
181 746 -10 138 <E(0) 05 12 0 12
182 784 -48 <E(0) 043 12 0 12
183 785 -49 <F(0) 044 12 0 12
184 787 -47 1 (1)F> 044 12 0 12
185 831 -3 145 (1)F> 12 0 12
186 834 -2 145 0 (1)B> 1 0 12
187 835 -1 145 0 1 (0)A> 0 12
188 836 0 145 0 1 0 (1)B> 12
189 837 1 145 0 1 0 1 (0)A> 1
190 839 -1 145 0 1 0 1 <D(0)
191 840 -2 145 0 1 0 <D(1)
192 843 -3 145 0 1 <E(0)
193 844 -4 145 0 <E(0)
194 845 -5 145 <F(0)
195 846 -6 144 <B(0)
196 848 -4 143 0 (1)B>
197 850 -6 143 0 <C(0) 1
198 851 -7 143 <D(0) 0 1
199 852 -8 142 <D(1) 02 1
200 894 -50 <D(1) 142 02 1
201 897 -51 <E(0) 0 142 02 1
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <E(0) 01+V(2) 13 01+V(1) 12 0 12
1 1 -1 <F(0) 02+V(2) 13 01+V(1) 12 0 12
2 3 1 1 (1)F> 02+V(2) 13 01+V(1) 12 0 12
3 5+V(2) 3+V(2) 13+V(2) (1)F> 13 01+V(1) 12 0 12
4 8+V(2) 4+V(2) 13+V(2) 0 (1)B> 12 01+V(1) 12 0 12
5 9+V(2) 5+V(2) 13+V(2) 0 1 (0)A> 1 01+V(1) 12 0 12
6 11+V(2) 3+V(2) 13+V(2) 0 1 <D(0) 02+V(1) 12 0 12
7 12+V(2) 2+V(2) 13+V(2) 0 <D(1) 03+V(1) 12 0 12
8 15+V(2) 1+V(2) 13+V(2) <E(0) 04+V(1) 12 0 12
9 18+2*V(2) -2 <E(0) 07+V(1)+V(2) 12 0 12
10 19+2*V(2) -3 <F(0) 08+V(1)+V(2) 12 0 12
11 21+2*V(2) -1 1 (1)F> 08+V(1)+V(2) 12 0 12
12 29+V(1)+3*V(2) 7+V(1)+V(2) 19+V(1)+V(2) (1)F> 12 0 12
13 32+V(1)+3*V(2) 8+V(1)+V(2) 19+V(1)+V(2) 0 (1)B> 1 0 12
14 33+V(1)+3*V(2) 9+V(1)+V(2) 19+V(1)+V(2) 0 1 (0)A> 0 12
15 34+V(1)+3*V(2) 10+V(1)+V(2) 19+V(1)+V(2) 0 1 0 (1)B> 12
16 35+V(1)+3*V(2) 11+V(1)+V(2) 19+V(1)+V(2) 0 1 0 1 (0)A> 1
17 37+V(1)+3*V(2) 9+V(1)+V(2) 19+V(1)+V(2) 0 1 0 1 <D(0)
18 38+V(1)+3*V(2) 8+V(1)+V(2) 19+V(1)+V(2) 0 1 0 <D(1)
19 41+V(1)+3*V(2) 7+V(1)+V(2) 19+V(1)+V(2) 0 1 <E(0)
20 42+V(1)+3*V(2) 6+V(1)+V(2) 19+V(1)+V(2) 0 <E(0)
21 43+V(1)+3*V(2) 5+V(1)+V(2) 19+V(1)+V(2) <F(0)
22 44+V(1)+3*V(2) 4+V(1)+V(2) 18+V(1)+V(2) <B(0)
23 46+V(1)+3*V(2) 6+V(1)+V(2) 17+V(1)+V(2) 0 (1)B>
24 48+V(1)+3*V(2) 4+V(1)+V(2) 17+V(1)+V(2) 0 <C(0) 1
25 49+V(1)+3*V(2) 3+V(1)+V(2) 17+V(1)+V(2) <D(0) 0 1
26 50+V(1)+3*V(2) 2+V(1)+V(2) 16+V(1)+V(2) <D(1) 02 1
27 56+2*V(1)+4*V(2) -4 <D(1) 16+V(1)+V(2) 02 1
28 59+2*V(1)+4*V(2) -5 <E(0) 0 16+V(1)+V(2) 02 1
<< Success! ==> defined new CTR 5 (PPA)
201 897 -51 <E(0) 0 142 02 1
== Executing PA-CTR 1, V(1)=38, V(2)=0, repcount=13, factor=5/3
318 1911 -77 <E(0) 066 13 02 1
319 1912 -78 <F(0) 067 13 02 1
320 1914 -76 1 (1)F> 067 13 02 1
321 1981 -9 168 (1)F> 13 02 1
322 1984 -8 168 0 (1)B> 12 02 1
323 1985 -7 168 0 1 (0)A> 1 02 1
324 1987 -9 168 0 1 <D(0) 03 1
325 1988 -10 168 0 <D(1) 04 1
326 1991 -11 168 <E(0) 05 1
327 2059 -79 <E(0) 073 1
328 2060 -80 <F(0) 074 1
329 2062 -78 1 (1)F> 074 1
330 2136 -4 175 (1)F> 1
331 2139 -3 175 0 (1)B>
332 2141 -5 175 0 <C(0) 1
333 2142 -6 175 <D(0) 0 1
334 2143 -7 174 <D(1) 02 1
335 2217 -81 <D(1) 174 02 1
336 2220 -82 <E(0) 0 174 02 1
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <E(0) 01+V(2) 13 01+V(1) 1
1 1 -1 <F(0) 02+V(2) 13 01+V(1) 1
2 3 1 1 (1)F> 02+V(2) 13 01+V(1) 1
3 5+V(2) 3+V(2) 13+V(2) (1)F> 13 01+V(1) 1
4 8+V(2) 4+V(2) 13+V(2) 0 (1)B> 12 01+V(1) 1
5 9+V(2) 5+V(2) 13+V(2) 0 1 (0)A> 1 01+V(1) 1
6 11+V(2) 3+V(2) 13+V(2) 0 1 <D(0) 02+V(1) 1
7 12+V(2) 2+V(2) 13+V(2) 0 <D(1) 03+V(1) 1
8 15+V(2) 1+V(2) 13+V(2) <E(0) 04+V(1) 1
9 18+2*V(2) -2 <E(0) 07+V(1)+V(2) 1
10 19+2*V(2) -3 <F(0) 08+V(1)+V(2) 1
11 21+2*V(2) -1 1 (1)F> 08+V(1)+V(2) 1
12 29+V(1)+3*V(2) 7+V(1)+V(2) 19+V(1)+V(2) (1)F> 1
13 32+V(1)+3*V(2) 8+V(1)+V(2) 19+V(1)+V(2) 0 (1)B>
14 34+V(1)+3*V(2) 6+V(1)+V(2) 19+V(1)+V(2) 0 <C(0) 1
15 35+V(1)+3*V(2) 5+V(1)+V(2) 19+V(1)+V(2) <D(0) 0 1
16 36+V(1)+3*V(2) 4+V(1)+V(2) 18+V(1)+V(2) <D(1) 02 1
17 44+2*V(1)+4*V(2) -4 <D(1) 18+V(1)+V(2) 02 1
18 47+2*V(1)+4*V(2) -5 <E(0) 0 18+V(1)+V(2) 02 1
<< Success! ==> defined new CTR 6 (PPA)
336 2220 -82 <E(0) 0 174 02 1
== Executing PA-CTR 1, V(1)=70, V(2)=0, repcount=24, factor=5/3
552 5412 -130 <E(0) 0121 12 02 1
553 5413 -131 <F(0) 0122 12 02 1
554 5415 -129 1 (1)F> 0122 12 02 1
555 5537 -7 1123 (1)F> 12 02 1
556 5540 -6 1123 0 (1)B> 1 02 1
557 5541 -5 1123 0 1 (0)A> 02 1
558 5542 -4 1123 0 1 0 (1)B> 0 1
559 5544 -6 1123 0 1 0 <C(0) 12
560 5545 -7 1123 0 1 <D(0) 0 12
561 5546 -8 1123 0 <D(1) 02 12
562 5549 -9 1123 <E(0) 03 12
563 5672 -132 <E(0) 0126 12
564 5673 -133 <F(0) 0127 12
565 5675 -131 1 (1)F> 0127 12
566 5802 -4 1128 (1)F> 12
567 5805 -3 1128 0 (1)B> 1
568 5806 -2 1128 0 1 (0)A>
569 5807 -1 1128 0 1 0 (1)B>
570 5809 -3 1128 0 1 0 <C(0) 1
571 5810 -4 1128 0 1 <D(0) 0 1
572 5811 -5 1128 0 <D(1) 02 1
573 5814 -6 1128 <E(0) 03 1
574 5942 -134 <E(0) 0131 1
575 5943 -135 <F(0) 0132 1
576 5945 -133 1 (1)F> 0132 1
577 6077 -1 1133 (1)F> 1
578 6080 0 1133 0 (1)B>
579 6082 -2 1133 0 <C(0) 1
580 6083 -3 1133 <D(0) 0 1
581 6084 -4 1132 <D(1) 02 1
582 6216 -136 <D(1) 1132 02 1
583 6219 -137 <E(0) 0 1132 02 1
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <E(0) 01+V(1) 12 02 1
1 1 -1 <F(0) 02+V(1) 12 02 1
2 3 1 1 (1)F> 02+V(1) 12 02 1
3 5+V(1) 3+V(1) 13+V(1) (1)F> 12 02 1
4 8+V(1) 4+V(1) 13+V(1) 0 (1)B> 1 02 1
5 9+V(1) 5+V(1) 13+V(1) 0 1 (0)A> 02 1
6 10+V(1) 6+V(1) 13+V(1) 0 1 0 (1)B> 0 1
7 12+V(1) 4+V(1) 13+V(1) 0 1 0 <C(0) 12
8 13+V(1) 3+V(1) 13+V(1) 0 1 <D(0) 0 12
9 14+V(1) 2+V(1) 13+V(1) 0 <D(1) 02 12
10 17+V(1) 1+V(1) 13+V(1) <E(0) 03 12
11 20+2*V(1) -2 <E(0) 06+V(1) 12
12 21+2*V(1) -3 <F(0) 07+V(1) 12
13 23+2*V(1) -1 1 (1)F> 07+V(1) 12
14 30+3*V(1) 6+V(1) 18+V(1) (1)F> 12
15 33+3*V(1) 7+V(1) 18+V(1) 0 (1)B> 1
16 34+3*V(1) 8+V(1) 18+V(1) 0 1 (0)A>
17 35+3*V(1) 9+V(1) 18+V(1) 0 1 0 (1)B>
18 37+3*V(1) 7+V(1) 18+V(1) 0 1 0 <C(0) 1
19 38+3*V(1) 6+V(1) 18+V(1) 0 1 <D(0) 0 1
20 39+3*V(1) 5+V(1) 18+V(1) 0 <D(1) 02 1
21 42+3*V(1) 4+V(1) 18+V(1) <E(0) 03 1
22 50+4*V(1) -4 <E(0) 011+V(1) 1
23 51+4*V(1) -5 <F(0) 012+V(1) 1
24 53+4*V(1) -3 1 (1)F> 012+V(1) 1
25 65+5*V(1) 9+V(1) 113+V(1) (1)F> 1
26 68+5*V(1) 10+V(1) 113+V(1) 0 (1)B>
27 70+5*V(1) 8+V(1) 113+V(1) 0 <C(0) 1
28 71+5*V(1) 7+V(1) 113+V(1) <D(0) 0 1
29 72+5*V(1) 6+V(1) 112+V(1) <D(1) 02 1
30 84+6*V(1) -6 <D(1) 112+V(1) 02 1
31 87+6*V(1) -7 <E(0) 0 112+V(1) 02 1
<< Success! ==> defined new CTR 7 (PPA)
583 6219 -137 <E(0) 0 1132 02 1
== Executing PA-CTR 1, V(1)=128, V(2)=0, repcount=43, factor=5/3
970 16023 -223 <E(0) 0216 13 02 1
== Executing PPA-CTR 6 (once), V(1)=1, V(2)=215
988 16932 -228 <E(0) 0 1224 02 1
== Executing PA-CTR 1, V(1)=220, V(2)=0, repcount=74, factor=5/3
1654 45274 -376 <E(0) 0371 12 02 1
== Executing PPA-CTR 7 (once), V(1)=370
1685 47581 -383 <E(0) 0 1382 02 1
== Executing PA-CTR 1, V(1)=378, V(2)=0, repcount=127, factor=5/3
2828 129877 -637 <E(0) 0636 1 02 1
2829 129878 -638 <F(0) 0637 1 02 1
2830 129880 -636 1 (1)F> 0637 1 02 1
2831 130517 1 1638 (1)F> 1 02 1
2832 130520 2 1638 0 (1)B> 02 1
2833 130522 0 1638 0 <C(0) 1 0 1
2834 130523 -1 1638 <D(0) 0 1 0 1
2835 130524 -2 1637 <D(1) 02 1 0 1
2836 131161 -639 <D(1) 1637 02 1 0 1
2837 131164 -640 <E(0) 0 1637 02 1 0 1
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <E(0) 03+V(2) 1 02+V(1) [*]*
1 1 -1 <F(0) 04+V(2) 1 02+V(1) [*]*
2 3 1 1 (1)F> 04+V(2) 1 02+V(1) [*]*
3 7+V(2) 5+V(2) 15+V(2) (1)F> 1 02+V(1) [*]*
4 10+V(2) 6+V(2) 15+V(2) 0 (1)B> 02+V(1) [*]*
5 12+V(2) 4+V(2) 15+V(2) 0 <C(0) 1 01+V(1) [*]*
6 13+V(2) 3+V(2) 15+V(2) <D(0) 0 1 01+V(1) [*]*
7 14+V(2) 2+V(2) 14+V(2) <D(1) 02 1 01+V(1) [*]*
8 18+2*V(2) -2 <D(1) 14+V(2) 02 1 01+V(1) [*]*
9 21+2*V(2) -3 <E(0) 0 14+V(2) 02 1 01+V(1) [*]*
<< Success! ==> defined new CTR 8 (PPA)
2837 131164 -640 <E(0) 0 1637 02 1 0 1
== Executing PA-CTR 2, V(1)=633, V(2)=0, repcount=212, factor=5/3
4745 358640 -1064 <E(0) 01061 1 02 1 0 1
4746 358641 -1065 <F(0) 01062 1 02 1 0 1
4747 358643 -1063 1 (1)F> 01062 1 02 1 0 1
4748 359705 -1 11063 (1)F> 1 02 1 0 1
4749 359708 0 11063 0 (1)B> 02 1 0 1
4750 359710 -2 11063 0 <C(0) 1 0 1 0 1
4751 359711 -3 11063 <D(0) 0 1 0 1 0 1
4752 359712 -4 11062 <D(1) 02 1 0 1 0 1
4753 360774 -1066 <D(1) 11062 02 1 0 1 0 1
4754 360777 -1067 <E(0) 0 11062 02 1 0 1 0 1
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <E(0) 03+V(2) 1 02+V(1) [*]* [*]* [*]*
1 1 -1 <F(0) 04+V(2) 1 02+V(1) [*]* [*]* [*]*
2 3 1 1 (1)F> 04+V(2) 1 02+V(1) [*]* [*]* [*]*
3 7+V(2) 5+V(2) 15+V(2) (1)F> 1 02+V(1) [*]* [*]* [*]*
4 10+V(2) 6+V(2) 15+V(2) 0 (1)B> 02+V(1) [*]* [*]* [*]*
5 12+V(2) 4+V(2) 15+V(2) 0 <C(0) 1 01+V(1) [*]* [*]* [*]*
6 13+V(2) 3+V(2) 15+V(2) <D(0) 0 1 01+V(1) [*]* [*]* [*]*
7 14+V(2) 2+V(2) 14+V(2) <D(1) 02 1 01+V(1) [*]* [*]* [*]*
8 18+2*V(2) -2 <D(1) 14+V(2) 02 1 01+V(1) [*]* [*]* [*]*
9 21+2*V(2) -3 <E(0) 0 14+V(2) 02 1 01+V(1) [*]* [*]* [*]*
<< Success! ==> defined new CTR 9 (PPA)
4754 360777 -1067 <E(0) 0 11062 02 1 0 1 0 1
== Executing PA-CTR 3, V(1)=1058, V(2)=0, repcount=353, factor=5/3
7931 988411 -1773 <E(0) 01766 13 02 1 0 1 0 1
== Executing PPA-CTR 4 (once), V(1)=0, V(2)=1, V(3)=1765
7949 995520 -1778 <E(0) 0 11774 02 12 0 1
== Executing PA-CTR 2, V(1)=1770, V(2)=0, repcount=591, factor=5/3
13268 2749608 -2960 <E(0) 02956 1 02 12 0 1
== Executing PPA-CTR 9 (once), V(1)=0, V(2)=2953
13277 2755535 -2963 <E(0) 0 12957 02 1 0 12 0 1
== Executing PA-CTR 3, V(1)=2953, V(2)=0, repcount=985, factor=5/3
22142 7619465 -4933 <E(0) 04926 12 02 1 0 12 0 1
22143 7619466 -4934 <F(0) 04927 12 02 1 0 12 0 1
22144 7619468 -4932 1 (1)F> 04927 12 02 1 0 12 0 1
22145 7624395 -5 14928 (1)F> 12 02 1 0 12 0 1
22146 7624398 -4 14928 0 (1)B> 1 02 1 0 12 0 1
22147 7624399 -3 14928 0 1 (0)A> 02 1 0 12 0 1
22148 7624400 -2 14928 0 1 0 (1)B> 0 1 0 12 0 1
22149 7624402 -4 14928 0 1 0 <C(0) 12 0 12 0 1
22150 7624403 -5 14928 0 1 <D(0) 0 12 0 12 0 1
22151 7624404 -6 14928 0 <D(1) 02 12 0 12 0 1
22152 7624407 -7 14928 <E(0) 03 12 0 12 0 1
22153 7629335 -4935 <E(0) 04931 12 0 12 0 1
22154 7629336 -4936 <F(0) 04932 12 0 12 0 1
22155 7629338 -4934 1 (1)F> 04932 12 0 12 0 1
22156 7634270 -2 14933 (1)F> 12 0 12 0 1
22157 7634273 -1 14933 0 (1)B> 1 0 12 0 1
22158 7634274 0 14933 0 1 (0)A> 0 12 0 1
22159 7634275 1 14933 0 1 0 (1)B> 12 0 1
22160 7634276 2 14933 0 1 0 1 (0)A> 1 0 1
22161 7634278 0 14933 0 1 0 1 <D(0) 02 1
22162 7634279 -1 14933 0 1 0 <D(1) 03 1
22163 7634282 -2 14933 0 1 <E(0) 04 1
22164 7634283 -3 14933 0 <E(0) 05 1
22165 7634284 -4 14933 <F(0) 06 1
22166 7634285 -5 14932 <B(0) 07 1
22167 7634287 -3 14931 0 (1)B> 07 1
22168 7634289 -5 14931 0 <C(0) 1 06 1
22169 7634290 -6 14931 <D(0) 0 1 06 1
22170 7634291 -7 14930 <D(1) 02 1 06 1
22171 7639221 -4937 <D(1) 14930 02 1 06 1
22172 7639224 -4938 <E(0) 0 14930 02 1 06 1
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <E(0) 01+V(2) 12 02 1 0 12 01+V(1) [*]*
1 1 -1 <F(0) 02+V(2) 12 02 1 0 12 01+V(1) [*]*
2 3 1 1 (1)F> 02+V(2) 12 02 1 0 12 01+V(1) [*]*
3 5+V(2) 3+V(2) 13+V(2) (1)F> 12 02 1 0 12 01+V(1) [*]*
4 8+V(2) 4+V(2) 13+V(2) 0 (1)B> 1 02 1 0 12 01+V(1) [*]*
5 9+V(2) 5+V(2) 13+V(2) 0 1 (0)A> 02 1 0 12 01+V(1) [*]*
6 10+V(2) 6+V(2) 13+V(2) 0 1 0 (1)B> 0 1 0 12 01+V(1) [*]*
7 12+V(2) 4+V(2) 13+V(2) 0 1 0 <C(0) 12 0 12 01+V(1) [*]*
8 13+V(2) 3+V(2) 13+V(2) 0 1 <D(0) 0 12 0 12 01+V(1) [*]*
9 14+V(2) 2+V(2) 13+V(2) 0 <D(1) 02 12 0 12 01+V(1) [*]*
10 17+V(2) 1+V(2) 13+V(2) <E(0) 03 12 0 12 01+V(1) [*]*
11 20+2*V(2) -2 <E(0) 06+V(2) 12 0 12 01+V(1) [*]*
12 21+2*V(2) -3 <F(0) 07+V(2) 12 0 12 01+V(1) [*]*
13 23+2*V(2) -1 1 (1)F> 07+V(2) 12 0 12 01+V(1) [*]*
14 30+3*V(2) 6+V(2) 18+V(2) (1)F> 12 0 12 01+V(1) [*]*
15 33+3*V(2) 7+V(2) 18+V(2) 0 (1)B> 1 0 12 01+V(1) [*]*
16 34+3*V(2) 8+V(2) 18+V(2) 0 1 (0)A> 0 12 01+V(1) [*]*
17 35+3*V(2) 9+V(2) 18+V(2) 0 1 0 (1)B> 12 01+V(1) [*]*
18 36+3*V(2) 10+V(2) 18+V(2) 0 1 0 1 (0)A> 1 01+V(1) [*]*
19 38+3*V(2) 8+V(2) 18+V(2) 0 1 0 1 <D(0) 02+V(1) [*]*
20 39+3*V(2) 7+V(2) 18+V(2) 0 1 0 <D(1) 03+V(1) [*]*
21 42+3*V(2) 6+V(2) 18+V(2) 0 1 <E(0) 04+V(1) [*]*
22 43+3*V(2) 5+V(2) 18+V(2) 0 <E(0) 05+V(1) [*]*
23 44+3*V(2) 4+V(2) 18+V(2) <F(0) 06+V(1) [*]*
24 45+3*V(2) 3+V(2) 17+V(2) <B(0) 07+V(1) [*]*
25 47+3*V(2) 5+V(2) 16+V(2) 0 (1)B> 07+V(1) [*]*
26 49+3*V(2) 3+V(2) 16+V(2) 0 <C(0) 1 06+V(1) [*]*
27 50+3*V(2) 2+V(2) 16+V(2) <D(0) 0 1 06+V(1) [*]*
28 51+3*V(2) 1+V(2) 15+V(2) <D(1) 02 1 06+V(1) [*]*
29 56+4*V(2) -4 <D(1) 15+V(2) 02 1 06+V(1) [*]*
30 59+4*V(2) -5 <E(0) 0 15+V(2) 02 1 06+V(1) [*]*
<< Success! ==> defined new CTR 10 (PPA)
22172 7639224 -4938 <E(0) 0 14930 02 1 06 1
== Executing PA-CTR 2, V(1)=4926, V(2)=0, repcount=1643, factor=5/3
36959 21157828 -8224 <E(0) 08216 1 02 1 06 1
== Executing PPA-CTR 9 (once), V(1)=0, V(2)=8213
36968 21174275 -8227 <E(0) 0 18217 02 1 0 1 06 1
== Executing PA-CTR 3, V(1)=8213, V(2)=0, repcount=2738, factor=5/3
61610 58693089 -13703 <E(0) 013691 13 02 1 0 1 06 1
== Executing PPA-CTR 4 (once), V(1)=0, V(2)=1, V(3)=13690
61628 58747898 -13708 <E(0) 0 113699 02 12 06 1
== Executing PA-CTR 2, V(1)=13695, V(2)=0, repcount=4566, factor=5/3
102722 163049036 -22840 <E(0) 022831 1 02 12 06 1
== Executing PPA-CTR 9 (once), V(1)=0, V(2)=22828
102731 163094713 -22843 <E(0) 0 122832 02 1 0 12 06 1
== Executing PA-CTR 3, V(1)=22828, V(2)=0, repcount=7610, factor=5/3
171221 452754143 -38063 <E(0) 038051 12 02 1 0 12 06 1
== Executing PPA-CTR 10 (once), V(1)=5, V(2)=38050
171251 452906402 -38068 <E(0) 0 138055 02 1 011 1
== Executing PA-CTR 2, V(1)=38051, V(2)=0, repcount=12684, factor=5/3
285407 1257490574 -63436 <E(0) 063421 13 02 1 011 1
285408 1257490575 -63437 <F(0) 063422 13 02 1 011 1
285409 1257490577 -63435 1 (1)F> 063422 13 02 1 011 1
285410 1257553999 -13 163423 (1)F> 13 02 1 011 1
285411 1257554002 -12 163423 0 (1)B> 12 02 1 011 1
285412 1257554003 -11 163423 0 1 (0)A> 1 02 1 011 1
285413 1257554005 -13 163423 0 1 <D(0) 03 1 011 1
285414 1257554006 -14 163423 0 <D(1) 04 1 011 1
285415 1257554009 -15 163423 <E(0) 05 1 011 1
285416 1257617432 -63438 <E(0) 063428 1 011 1
285417 1257617433 -63439 <F(0) 063429 1 011 1
285418 1257617435 -63437 1 (1)F> 063429 1 011 1
285419 1257680864 -8 163430 (1)F> 1 011 1
285420 1257680867 -7 163430 0 (1)B> 011 1
285421 1257680869 -9 163430 0 <C(0) 1 010 1
285422 1257680870 -10 163430 <D(0) 0 1 010 1
285423 1257680871 -11 163429 <D(1) 02 1 010 1
285424 1257744300 -63440 <D(1) 163429 02 1 010 1
285425 1257744303 -63441 <E(0) 0 163429 02 1 010 1
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 <E(0) 01+V(3) 13 01+V(2) 1 02+V(1) [*]*
1 1 -1 <F(0) 02+V(3) 13 01+V(2) 1 02+V(1) [*]*
2 3 1 1 (1)F> 02+V(3) 13 01+V(2) 1 02+V(1) [*]*
3 5+V(3) 3+V(3) 13+V(3) (1)F> 13 01+V(2) 1 02+V(1) [*]*
4 8+V(3) 4+V(3) 13+V(3) 0 (1)B> 12 01+V(2) 1 02+V(1) [*]*
5 9+V(3) 5+V(3) 13+V(3) 0 1 (0)A> 1 01+V(2) 1 02+V(1) [*]*
6 11+V(3) 3+V(3) 13+V(3) 0 1 <D(0) 02+V(2) 1 02+V(1) [*]*
7 12+V(3) 2+V(3) 13+V(3) 0 <D(1) 03+V(2) 1 02+V(1) [*]*
8 15+V(3) 1+V(3) 13+V(3) <E(0) 04+V(2) 1 02+V(1) [*]*
9 18+2*V(3) -2 <E(0) 07+V(2)+V(3) 1 02+V(1) [*]*
10 19+2*V(3) -3 <F(0) 08+V(2)+V(3) 1 02+V(1) [*]*
11 21+2*V(3) -1 1 (1)F> 08+V(2)+V(3) 1 02+V(1) [*]*
12 29+V(2)+3*V(3) 7+V(2)+V(3) 19+V(2)+V(3) (1)F> 1 02+V(1) [*]*
13 32+V(2)+3*V(3) 8+V(2)+V(3) 19+V(2)+V(3) 0 (1)B> 02+V(1) [*]*
14 34+V(2)+3*V(3) 6+V(2)+V(3) 19+V(2)+V(3) 0 <C(0) 1 01+V(1) [*]*
15 35+V(2)+3*V(3) 5+V(2)+V(3) 19+V(2)+V(3) <D(0) 0 1 01+V(1) [*]*
16 36+V(2)+3*V(3) 4+V(2)+V(3) 18+V(2)+V(3) <D(1) 02 1 01+V(1) [*]*
17 44+2*V(2)+4*V(3) -4 <D(1) 18+V(2)+V(3) 02 1 01+V(1) [*]*
18 47+2*V(2)+4*V(3) -5 <E(0) 0 18+V(2)+V(3) 02 1 01+V(1) [*]*
<< Success! ==> defined new CTR 11 (PPA)
285425 1257744303 -63441 <E(0) 0 163429 02 1 010 1
== Executing PA-CTR 2, V(1)=63425, V(2)=0, repcount=21142, factor=5/3
475703 3492939969 -105725 <E(0) 0105711 13 02 1 010 1
== Executing PPA-CTR 11 (once), V(1)=8, V(2)=1, V(3)=105710
475721 3493362858 -105730 <E(0) 0 1105719 02 1 09 1
== Executing PA-CTR 2, V(1)=105715, V(2)=0, repcount=35239, factor=5/3
792872 9702756570 -176208 <E(0) 0176196 12 02 1 09 1
792873 9702756571 -176209 <F(0) 0176197 12 02 1 09 1
792874 9702756573 -176207 1 (1)F> 0176197 12 02 1 09 1
792875 9702932770 -10 1176198 (1)F> 12 02 1 09 1
792876 9702932773 -9 1176198 0 (1)B> 1 02 1 09 1
792877 9702932774 -8 1176198 0 1 (0)A> 02 1 09 1
792878 9702932775 -7 1176198 0 1 0 (1)B> 0 1 09 1
792879 9702932777 -9 1176198 0 1 0 <C(0) 12 09 1
792880 9702932778 -10 1176198 0 1 <D(0) 0 12 09 1
792881 9702932779 -11 1176198 0 <D(1) 02 12 09 1
792882 9702932782 -12 1176198 <E(0) 03 12 09 1
792883 9703108980 -176210 <E(0) 0176201 12 09 1
792884 9703108981 -176211 <F(0) 0176202 12 09 1
792885 9703108983 -176209 1 (1)F> 0176202 12 09 1
792886 9703285185 -7 1176203 (1)F> 12 09 1
792887 9703285188 -6 1176203 0 (1)B> 1 09 1
792888 9703285189 -5 1176203 0 1 (0)A> 09 1
792889 9703285190 -4 1176203 0 1 0 (1)B> 08 1
792890 9703285192 -6 1176203 0 1 0 <C(0) 1 07 1
792891 9703285193 -7 1176203 0 1 <D(0) 0 1 07 1
792892 9703285194 -8 1176203 0 <D(1) 02 1 07 1
792893 9703285197 -9 1176203 <E(0) 03 1 07 1
792894 9703461400 -176212 <E(0) 0176206 1 07 1
792895 9703461401 -176213 <F(0) 0176207 1 07 1
792896 9703461403 -176211 1 (1)F> 0176207 1 07 1
792897 9703637610 -4 1176208 (1)F> 1 07 1
792898 9703637613 -3 1176208 0 (1)B> 07 1
792899 9703637615 -5 1176208 0 <C(0) 1 06 1
792900 9703637616 -6 1176208 <D(0) 0 1 06 1
792901 9703637617 -7 1176207 <D(1) 02 1 06 1
792902 9703813824 -176214 <D(1) 1176207 02 1 06 1
792903 9703813827 -176215 <E(0) 0 1176207 02 1 06 1
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <E(0) 01+V(2) 12 02 1 04+V(1) [*]*
1 1 -1 <F(0) 02+V(2) 12 02 1 04+V(1) [*]*
2 3 1 1 (1)F> 02+V(2) 12 02 1 04+V(1) [*]*
3 5+V(2) 3+V(2) 13+V(2) (1)F> 12 02 1 04+V(1) [*]*
4 8+V(2) 4+V(2) 13+V(2) 0 (1)B> 1 02 1 04+V(1) [*]*
5 9+V(2) 5+V(2) 13+V(2) 0 1 (0)A> 02 1 04+V(1) [*]*
6 10+V(2) 6+V(2) 13+V(2) 0 1 0 (1)B> 0 1 04+V(1) [*]*
7 12+V(2) 4+V(2) 13+V(2) 0 1 0 <C(0) 12 04+V(1) [*]*
8 13+V(2) 3+V(2) 13+V(2) 0 1 <D(0) 0 12 04+V(1) [*]*
9 14+V(2) 2+V(2) 13+V(2) 0 <D(1) 02 12 04+V(1) [*]*
10 17+V(2) 1+V(2) 13+V(2) <E(0) 03 12 04+V(1) [*]*
11 20+2*V(2) -2 <E(0) 06+V(2) 12 04+V(1) [*]*
12 21+2*V(2) -3 <F(0) 07+V(2) 12 04+V(1) [*]*
13 23+2*V(2) -1 1 (1)F> 07+V(2) 12 04+V(1) [*]*
14 30+3*V(2) 6+V(2) 18+V(2) (1)F> 12 04+V(1) [*]*
15 33+3*V(2) 7+V(2) 18+V(2) 0 (1)B> 1 04+V(1) [*]*
16 34+3*V(2) 8+V(2) 18+V(2) 0 1 (0)A> 04+V(1) [*]*
17 35+3*V(2) 9+V(2) 18+V(2) 0 1 0 (1)B> 03+V(1) [*]*
18 37+3*V(2) 7+V(2) 18+V(2) 0 1 0 <C(0) 1 02+V(1) [*]*
19 38+3*V(2) 6+V(2) 18+V(2) 0 1 <D(0) 0 1 02+V(1) [*]*
20 39+3*V(2) 5+V(2) 18+V(2) 0 <D(1) 02 1 02+V(1) [*]*
21 42+3*V(2) 4+V(2) 18+V(2) <E(0) 03 1 02+V(1) [*]*
22 50+4*V(2) -4 <E(0) 011+V(2) 1 02+V(1) [*]*
23 51+4*V(2) -5 <F(0) 012+V(2) 1 02+V(1) [*]*
24 53+4*V(2) -3 1 (1)F> 012+V(2) 1 02+V(1) [*]*
25 65+5*V(2) 9+V(2) 113+V(2) (1)F> 1 02+V(1) [*]*
26 68+5*V(2) 10+V(2) 113+V(2) 0 (1)B> 02+V(1) [*]*
27 70+5*V(2) 8+V(2) 113+V(2) 0 <C(0) 1 01+V(1) [*]*
28 71+5*V(2) 7+V(2) 113+V(2) <D(0) 0 1 01+V(1) [*]*
29 72+5*V(2) 6+V(2) 112+V(2) <D(1) 02 1 01+V(1) [*]*
30 84+6*V(2) -6 <D(1) 112+V(2) 02 1 01+V(1) [*]*
31 87+6*V(2) -7 <E(0) 0 112+V(2) 02 1 01+V(1) [*]*
<< Success! ==> defined new CTR 12 (PPA)
792903 9703813827 -176215 <E(0) 0 1176207 02 1 06 1
== Executing PA-CTR 2, V(1)=176203, V(2)=0, repcount=58735, factor=5/3
1321518 26953578507 -293685 <E(0) 0293676 12 02 1 06 1
== Executing PPA-CTR 12 (once), V(1)=2, V(2)=293675
1321549 26955340644 -293692 <E(0) 0 1293687 02 1 03 1
== Executing PA-CTR 2, V(1)=293683, V(2)=0, repcount=97895, factor=5/3
2202604 74873768404 -489482 <E(0) 0489476 12 02 1 03 1
2202605 74873768405 -489483 <F(0) 0489477 12 02 1 03 1
2202606 74873768407 -489481 1 (1)F> 0489477 12 02 1 03 1
2202607 74874257884 -4 1489478 (1)F> 12 02 1 03 1
2202608 74874257887 -3 1489478 0 (1)B> 1 02 1 03 1
2202609 74874257888 -2 1489478 0 1 (0)A> 02 1 03 1
2202610 74874257889 -1 1489478 0 1 0 (1)B> 0 1 03 1
2202611 74874257891 -3 1489478 0 1 0 <C(0) 12 03 1
2202612 74874257892 -4 1489478 0 1 <D(0) 0 12 03 1
2202613 74874257893 -5 1489478 0 <D(1) 02 12 03 1
2202614 74874257896 -6 1489478 <E(0) 03 12 03 1
2202615 74874747374 -489484 <E(0) 0489481 12 03 1
2202616 74874747375 -489485 <F(0) 0489482 12 03 1
2202617 74874747377 -489483 1 (1)F> 0489482 12 03 1
2202618 74875236859 -1 1489483 (1)F> 12 03 1
2202619 74875236862 0 1489483 0 (1)B> 1 03 1
2202620 74875236863 1 1489483 0 1 (0)A> 03 1
2202621 74875236864 2 1489483 0 1 0 (1)B> 02 1
2202622 74875236866 0 1489483 0 1 0 <C(0) 1 0 1
2202623 74875236867 -1 1489483 0 1 <D(0) 0 1 0 1
2202624 74875236868 -2 1489483 0 <D(1) 02 1 0 1
2202625 74875236871 -3 1489483 <E(0) 03 1 0 1
2202626 74875726354 -489486 <E(0) 0489486 1 0 1
2202627 74875726355 -489487 <F(0) 0489487 1 0 1
2202628 74875726357 -489485 1 (1)F> 0489487 1 0 1
2202629 74876215844 2 1489488 (1)F> 1 0 1
2202630 74876215847 3 1489488 0 (1)B> 0 1
2202631 74876215849 1 1489488 0 <C(0) 12
2202632 74876215850 0 1489488 <D(0) 0 12
2202633 74876215851 -1 1489487 <D(1) 02 12
2202634 74876705338 -489488 <D(1) 1489487 02 12
2202635 74876705341 -489489 <E(0) 0 1489487 02 12
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <E(0) 01+V(2) 12 02 1 03 11+V(1)
1 1 -1 <F(0) 02+V(2) 12 02 1 03 11+V(1)
2 3 1 1 (1)F> 02+V(2) 12 02 1 03 11+V(1)
3 5+V(2) 3+V(2) 13+V(2) (1)F> 12 02 1 03 11+V(1)
4 8+V(2) 4+V(2) 13+V(2) 0 (1)B> 1 02 1 03 11+V(1)
5 9+V(2) 5+V(2) 13+V(2) 0 1 (0)A> 02 1 03 11+V(1)
6 10+V(2) 6+V(2) 13+V(2) 0 1 0 (1)B> 0 1 03 11+V(1)
7 12+V(2) 4+V(2) 13+V(2) 0 1 0 <C(0) 12 03 11+V(1)
8 13+V(2) 3+V(2) 13+V(2) 0 1 <D(0) 0 12 03 11+V(1)
9 14+V(2) 2+V(2) 13+V(2) 0 <D(1) 02 12 03 11+V(1)
10 17+V(2) 1+V(2) 13+V(2) <E(0) 03 12 03 11+V(1)
11 20+2*V(2) -2 <E(0) 06+V(2) 12 03 11+V(1)
12 21+2*V(2) -3 <F(0) 07+V(2) 12 03 11+V(1)
13 23+2*V(2) -1 1 (1)F> 07+V(2) 12 03 11+V(1)
14 30+3*V(2) 6+V(2) 18+V(2) (1)F> 12 03 11+V(1)
15 33+3*V(2) 7+V(2) 18+V(2) 0 (1)B> 1 03 11+V(1)
16 34+3*V(2) 8+V(2) 18+V(2) 0 1 (0)A> 03 11+V(1)
17 35+3*V(2) 9+V(2) 18+V(2) 0 1 0 (1)B> 02 11+V(1)
18 37+3*V(2) 7+V(2) 18+V(2) 0 1 0 <C(0) 1 0 11+V(1)
19 38+3*V(2) 6+V(2) 18+V(2) 0 1 <D(0) 0 1 0 11+V(1)
20 39+3*V(2) 5+V(2) 18+V(2) 0 <D(1) 02 1 0 11+V(1)
21 42+3*V(2) 4+V(2) 18+V(2) <E(0) 03 1 0 11+V(1)
22 50+4*V(2) -4 <E(0) 011+V(2) 1 0 11+V(1)
23 51+4*V(2) -5 <F(0) 012+V(2) 1 0 11+V(1)
24 53+4*V(2) -3 1 (1)F> 012+V(2) 1 0 11+V(1)
25 65+5*V(2) 9+V(2) 113+V(2) (1)F> 1 0 11+V(1)
26 68+5*V(2) 10+V(2) 113+V(2) 0 (1)B> 0 11+V(1)
27 70+5*V(2) 8+V(2) 113+V(2) 0 <C(0) 12+V(1)
28 71+5*V(2) 7+V(2) 113+V(2) <D(0) 0 12+V(1)
29 72+5*V(2) 6+V(2) 112+V(2) <D(1) 02 12+V(1)
30 84+6*V(2) -6 <D(1) 112+V(2) 02 12+V(1)
31 87+6*V(2) -7 <E(0) 0 112+V(2) 02 12+V(1)
<< Success! ==> defined new CTR 13 (PPA)
2202635 74876705341 -489489 <E(0) 0 1489487 02 12
== Executing PA-CTR 1, V(1)=489483, V(2)=0, repcount=163162, factor=5/3
3671093 207988017667 -815813 <E(0) 0815811 1 02 12
== Executing PPA-CTR 8 (once), V(1)=0, V(2)=815808
3671102 207989649304 -815816 <E(0) 0 1815812 02 1 0 12
== Executing PA-CTR 2, V(1)=815808, V(2)=0, repcount=271937, factor=5/3
6118535 577741844330 -1359690 <E(0) 01359686 1 02 1 0 12
== Executing PPA-CTR 9 (once), V(1)=0, V(2)=1359683
6118544 577744563717 -1359693 <E(0) 0 11359687 02 1 0 1 0 12
== Executing PA-CTR 3, V(1)=1359683, V(2)=0, repcount=453228, factor=5/3
10197596 1604828555601 -2266149 <E(0) 02266141 13 02 1 0 1 0 12
== Executing PPA-CTR 4 (once), V(1)=0, V(2)=1, V(3)=2266140
10197614 1604837620210 -2266154 <E(0) 0 12266149 02 12 0 12
== Executing PA-CTR 2, V(1)=2266145, V(2)=0, repcount=755382, factor=5/3
16996052 4457857269796 -3776918 <E(0) 03776911 13 02 12 0 12
== Executing PPA-CTR 5 (once), V(1)=1, V(2)=3776910
16996080 4457872377497 -3776923 <E(0) 0 13776917 02 1
== Executing PA-CTR 1, V(1)=3776913, V(2)=0, repcount=1258972, factor=5/3
28326828 12382941228053 -6294867 <E(0) 06294861 1 02 1
== Executing PPA-CTR 8 (once), V(1)=0, V(2)=6294858
28326837 12382953817790 -6294870 <E(0) 0 16294862 02 1 0 1
== Executing PA-CTR 2, V(1)=6294858, V(2)=0, repcount=2098287, factor=5/3
47211420 34397022767366 -10491444 <E(0) 010491436 1 02 1 0 1
== Executing PPA-CTR 9 (once), V(1)=0, V(2)=10491433
47211429 34397043750253 -10491447 <E(0) 0 110491437 02 1 0 1 0 1
== Executing PA-CTR 3, V(1)=10491433, V(2)=0, repcount=3497145, factor=5/3
78685734 95547204968263 -17485737 <E(0) 017485726 12 02 1 0 1 0 1
78685735 95547204968264 -17485738 <F(0) 017485727 12 02 1 0 1 0 1
78685736 95547204968266 -17485736 1 (1)F> 017485727 12 02 1 0 1 0 1
78685737 95547222453993 -9 117485728 (1)F> 12 02 1 0 1 0 1
78685738 95547222453996 -8 117485728 0 (1)B> 1 02 1 0 1 0 1
78685739 95547222453997 -7 117485728 0 1 (0)A> 02 1 0 1 0 1
78685740 95547222453998 -6 117485728 0 1 0 (1)B> 0 1 0 1 0 1
78685741 95547222454000 -8 117485728 0 1 0 <C(0) 12 0 1 0 1
78685742 95547222454001 -9 117485728 0 1 <D(0) 0 12 0 1 0 1
78685743 95547222454002 -10 117485728 0 <D(1) 02 12 0 1 0 1
78685744 95547222454005 -11 117485728 <E(0) 03 12 0 1 0 1
78685745 95547239939733 -17485739 <E(0) 017485731 12 0 1 0 1
78685746 95547239939734 -17485740 <F(0) 017485732 12 0 1 0 1
78685747 95547239939736 -17485738 1 (1)F> 017485732 12 0 1 0 1
78685748 95547257425468 -6 117485733 (1)F> 12 0 1 0 1
78685749 95547257425471 -5 117485733 0 (1)B> 1 0 1 0 1
78685750 95547257425472 -4 117485733 0 1 (0)A> 0 1 0 1
78685751 95547257425473 -3 117485733 0 1 0 (1)B> 1 0 1
78685752 95547257425474 -2 117485733 0 1 0 1 (0)A> 0 1
78685753 95547257425475 -1 117485733 0 1 0 1 0 (1)B> 1
78685754 95547257425476 0 117485733 0 1 0 1 0 1 (0)A>
78685755 95547257425477 1 117485733 0 1 0 1 0 1 0 (1)B>
78685756 95547257425479 -1 117485733 0 1 0 1 0 1 0 <C(0) 1
78685757 95547257425480 -2 117485733 0 1 0 1 0 1 <D(0) 0 1
78685758 95547257425481 -3 117485733 0 1 0 1 0 <D(1) 02 1
78685759 95547257425484 -4 117485733 0 1 0 1 <E(0) 03 1
78685760 95547257425485 -5 117485733 0 1 0 <E(0) 04 1
78685761 95547257425486 -6 117485733 0 1 <F(0) 05 1
78685762 95547257425487 -7 117485733 0 <B(0) 06 1
78685763 95547257425488 -8 117485733 <A(1) 07 1
78685764 95547257425489 -9 117485732 <C(0) 1 07 1
78685765 95547257425490 -8 117485731 1 Z> 0 1 07 1 [stop]
Lines: 364
Top steps: 363
Macro steps: 78685765
Basic steps: 95547257425490
Tape index: -8
ones: 17485734
log10(ones ): 7.243
log10(steps ): 13.980
Run state: stop
Input to awk program:
gohalt 1
L 60
5T B1R C0L A1L A0R D0L Z1R E1R D1L F0L E0L F1R B0L : 17485734 95547257425490
T 6-state TM #a from MaBu-List
M 650
pref sim
machv mbL6_a just simple
machv mbL6_a-r with repetitions reduced
machv mbL6_a-1 with tape symbol exponents
machv mbL6_a-m as 1-bck-macro machine
machv mbL6_a-a as 1-bck-macro machine with pure additive config-TRs
iam mbL6_a-a
mtype 1 0
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:10:37 CEST 2010
edate Tue Jul 6 22:10:39 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:10:37 CEST 2010