Comment: This TM produces >1.9x10^27 nonzeros in >2.3x10^54 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 | 0RB | 3LA | 5LA | 1RH | 4LB | 1 | right | B | 0 | right | B | 3 | left | A | 5 | left | A | 1 | right | H | 4 | left | B |
| B | 1LA | 2RB | 3LA | 4LB | 3RB | 3RA | 1 | left | A | 2 | right | B | 3 | left | A | 4 | left | B | 3 | right | B | 3 | right | A |
The same TM just simple.
The same TM with repetitions reduced.
The same TM with tape symbol exponents.
The same TM as 1-macro machine.
Simulation is done as 1-macro machine with pure additive config-TRs.
Pushing initial machine.
Pushing macro factor 1.
Steps BasSteps BasTpos Tape contents
0 0 0 A>
1 1 1 1 B>
2 2 0 1 <A 1
3 3 1 B> 1
4 4 2 2 B>
5 5 1 2 <A 1
6 6 0 <A 3 1
7 7 1 1 B> 3 1
8 8 0 1 <B 4 1
9 9 1 2 B> 4 1
10 10 2 2 3 B> 1
11 11 3 2 3 2 B>
12 12 2 2 3 2 <A 1
13 13 1 2 3 <A 3 1
14 14 0 2 <A 5 3 1
15 15 -1 <A 3 5 3 1
16 16 0 1 B> 3 5 3 1
17 17 -1 1 <B 4 5 3 1
18 18 0 2 B> 4 5 3 1
19 19 1 2 3 B> 5 3 1
20 20 2 2 32 A> 3 1
21 21 1 2 32 <A 5 1
22 23 -1 2 <A 53 1
23 24 -2 <A 3 53 1
24 25 -1 1 B> 3 53 1
25 26 -2 1 <B 4 53 1
26 27 -1 2 B> 4 53 1
27 28 0 2 3 B> 53 1
28 29 1 2 32 A> 52 1
29 30 0 2 32 <B 4 5 1
30 32 -2 2 <B 43 5 1
31 33 -3 <A 3 43 5 1
32 34 -2 1 B> 3 43 5 1
33 35 -3 1 <B 44 5 1
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 1 <B 41+V(2) 53+V(1) [*]*
1 1 1 2 B> 41+V(2) 53+V(1) [*]*
2 2+V(2) 2+V(2) 2 31+V(2) B> 53+V(1) [*]*
3 3+V(2) 3+V(2) 2 32+V(2) A> 52+V(1) [*]*
4 4+V(2) 2+V(2) 2 32+V(2) <B 4 51+V(1) [*]*
5 6+2*V(2) 0 2 <B 43+V(2) 51+V(1) [*]*
6 7+2*V(2) -1 <A 3 43+V(2) 51+V(1) [*]*
7 8+2*V(2) 0 1 B> 3 43+V(2) 51+V(1) [*]*
8 9+2*V(2) -1 1 <B 44+V(2) 51+V(1) [*]*
<< Success! ==> defined new CTR 1 (PA)
34 36 -2 2 B> 44 5 1
35 40 2 2 34 B> 5 1
36 41 3 2 35 A> 1
37 42 4 2 35 0 B>
38 43 3 2 35 0 <A 1
39 44 4 2 35 1 B> 1
40 45 5 2 35 1 2 B>
41 46 4 2 35 1 2 <A 1
42 47 3 2 35 1 <A 3 1
43 48 4 2 35 0 B> 3 1
44 49 3 2 35 0 <B 4 1
45 50 2 2 35 <A 1 4 1
46 55 -3 2 <A 55 1 4 1
47 56 -4 <A 3 55 1 4 1
48 57 -3 1 B> 3 55 1 4 1
49 58 -4 1 <B 4 55 1 4 1
50 59 -3 2 B> 4 55 1 4 1
51 60 -2 2 3 B> 55 1 4 1
52 61 -1 2 32 A> 54 1 4 1
53 62 -2 2 32 <B 4 53 1 4 1
54 64 -4 2 <B 43 53 1 4 1
55 65 -5 <A 3 43 53 1 4 1
56 66 -4 1 B> 3 43 53 1 4 1
57 67 -5 1 <B 44 53 1 4 1
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 1 <B 41+V(2) 53+V(1) [*]* [*]* [*]*
1 1 1 2 B> 41+V(2) 53+V(1) [*]* [*]* [*]*
2 2+V(2) 2+V(2) 2 31+V(2) B> 53+V(1) [*]* [*]* [*]*
3 3+V(2) 3+V(2) 2 32+V(2) A> 52+V(1) [*]* [*]* [*]*
4 4+V(2) 2+V(2) 2 32+V(2) <B 4 51+V(1) [*]* [*]* [*]*
5 6+2*V(2) 0 2 <B 43+V(2) 51+V(1) [*]* [*]* [*]*
6 7+2*V(2) -1 <A 3 43+V(2) 51+V(1) [*]* [*]* [*]*
7 8+2*V(2) 0 1 B> 3 43+V(2) 51+V(1) [*]* [*]* [*]*
8 9+2*V(2) -1 1 <B 44+V(2) 51+V(1) [*]* [*]* [*]*
<< Success! ==> defined new CTR 2 (PA)
57 67 -5 1 <B 44 53 1 4 1
== Executing PA-CTR 2, V(1)=0, V(2)=3, repcount=1, factor=3/2
65 82 -6 1 <B 47 5 1 4 1
66 83 -5 2 B> 47 5 1 4 1
67 90 2 2 37 B> 5 1 4 1
68 91 3 2 38 A> 1 4 1
69 92 4 2 38 0 B> 4 1
70 93 5 2 38 0 3 B> 1
71 94 6 2 38 0 3 2 B>
72 95 5 2 38 0 3 2 <A 1
73 96 4 2 38 0 3 <A 3 1
74 97 3 2 38 0 <A 5 3 1
75 98 4 2 38 1 B> 5 3 1
76 99 5 2 38 1 3 A> 3 1
77 100 4 2 38 1 3 <A 5 1
78 101 3 2 38 1 <A 52 1
79 102 4 2 38 0 B> 52 1
80 103 5 2 38 0 3 A> 5 1
81 104 4 2 38 0 3 <B 4 1
82 105 3 2 38 0 <B 42 1
83 106 2 2 38 <A 1 42 1
84 114 -6 2 <A 58 1 42 1
85 115 -7 <A 3 58 1 42 1
86 116 -6 1 B> 3 58 1 42 1
87 117 -7 1 <B 4 58 1 42 1
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 1 <B 42+V(1) 5 1 4 1
1 1 1 2 B> 42+V(1) 5 1 4 1
2 3+V(1) 3+V(1) 2 32+V(1) B> 5 1 4 1
3 4+V(1) 4+V(1) 2 33+V(1) A> 1 4 1
4 5+V(1) 5+V(1) 2 33+V(1) 0 B> 4 1
5 6+V(1) 6+V(1) 2 33+V(1) 0 3 B> 1
6 7+V(1) 7+V(1) 2 33+V(1) 0 3 2 B>
7 8+V(1) 6+V(1) 2 33+V(1) 0 3 2 <A 1
8 9+V(1) 5+V(1) 2 33+V(1) 0 3 <A 3 1
9 10+V(1) 4+V(1) 2 33+V(1) 0 <A 5 3 1
10 11+V(1) 5+V(1) 2 33+V(1) 1 B> 5 3 1
11 12+V(1) 6+V(1) 2 33+V(1) 1 3 A> 3 1
12 13+V(1) 5+V(1) 2 33+V(1) 1 3 <A 5 1
13 14+V(1) 4+V(1) 2 33+V(1) 1 <A 52 1
14 15+V(1) 5+V(1) 2 33+V(1) 0 B> 52 1
15 16+V(1) 6+V(1) 2 33+V(1) 0 3 A> 5 1
16 17+V(1) 5+V(1) 2 33+V(1) 0 3 <B 4 1
17 18+V(1) 4+V(1) 2 33+V(1) 0 <B 42 1
18 19+V(1) 3+V(1) 2 33+V(1) <A 1 42 1
19 22+2*V(1) 0 2 <A 53+V(1) 1 42 1
20 23+2*V(1) -1 <A 3 53+V(1) 1 42 1
21 24+2*V(1) 0 1 B> 3 53+V(1) 1 42 1
22 25+2*V(1) -1 1 <B 4 53+V(1) 1 42 1
<< Success! ==> defined new CTR 3 (PPA)
87 117 -7 1 <B 4 58 1 42 1
== Executing PA-CTR 2, V(1)=5, V(2)=0, repcount=3, factor=3/2
111 162 -10 1 <B 410 52 1 42 1
112 163 -9 2 B> 410 52 1 42 1
113 173 1 2 310 B> 52 1 42 1
114 174 2 2 311 A> 5 1 42 1
115 175 1 2 311 <B 4 1 42 1
116 186 -10 2 <B 412 1 42 1
117 187 -11 <A 3 412 1 42 1
118 188 -10 1 B> 3 412 1 42 1
119 189 -11 1 <B 413 1 42 1
120 190 -10 2 B> 413 1 42 1
121 203 3 2 313 B> 1 42 1
122 204 4 2 313 2 B> 42 1
123 206 6 2 313 2 32 B> 1
124 207 7 2 313 2 32 2 B>
125 208 6 2 313 2 32 2 <A 1
126 209 5 2 313 2 32 <A 3 1
127 211 3 2 313 2 <A 52 3 1
128 212 2 2 313 <A 3 52 3 1
129 225 -11 2 <A 513 3 52 3 1
130 226 -12 <A 3 513 3 52 3 1
131 227 -11 1 B> 3 513 3 52 3 1
132 228 -12 1 <B 4 513 3 52 3 1
133 229 -11 2 B> 4 513 3 52 3 1
134 230 -10 2 3 B> 513 3 52 3 1
135 231 -9 2 32 A> 512 3 52 3 1
136 232 -10 2 32 <B 4 511 3 52 3 1
137 234 -12 2 <B 43 511 3 52 3 1
138 235 -13 <A 3 43 511 3 52 3 1
139 236 -12 1 B> 3 43 511 3 52 3 1
140 237 -13 1 <B 44 511 3 52 3 1
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 1 <B 41+V(2) 53+V(1) [*]* [*]* [*]* [*]*
1 1 1 2 B> 41+V(2) 53+V(1) [*]* [*]* [*]* [*]*
2 2+V(2) 2+V(2) 2 31+V(2) B> 53+V(1) [*]* [*]* [*]* [*]*
3 3+V(2) 3+V(2) 2 32+V(2) A> 52+V(1) [*]* [*]* [*]* [*]*
4 4+V(2) 2+V(2) 2 32+V(2) <B 4 51+V(1) [*]* [*]* [*]* [*]*
5 6+2*V(2) 0 2 <B 43+V(2) 51+V(1) [*]* [*]* [*]* [*]*
6 7+2*V(2) -1 <A 3 43+V(2) 51+V(1) [*]* [*]* [*]* [*]*
7 8+2*V(2) 0 1 B> 3 43+V(2) 51+V(1) [*]* [*]* [*]* [*]*
8 9+2*V(2) -1 1 <B 44+V(2) 51+V(1) [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 4 (PA)
140 237 -13 1 <B 44 511 3 52 3 1
== Executing PA-CTR 4, V(1)=8, V(2)=3, repcount=5, factor=3/2
180 372 -18 1 <B 419 5 3 52 3 1
181 373 -17 2 B> 419 5 3 52 3 1
182 392 2 2 319 B> 5 3 52 3 1
183 393 3 2 320 A> 3 52 3 1
184 394 2 2 320 <A 53 3 1
185 414 -18 2 <A 523 3 1
186 415 -19 <A 3 523 3 1
187 416 -18 1 B> 3 523 3 1
188 417 -19 1 <B 4 523 3 1
189 418 -18 2 B> 4 523 3 1
190 419 -17 2 3 B> 523 3 1
191 420 -16 2 32 A> 522 3 1
192 421 -17 2 32 <B 4 521 3 1
193 423 -19 2 <B 43 521 3 1
194 424 -20 <A 3 43 521 3 1
195 425 -19 1 B> 3 43 521 3 1
196 426 -20 1 <B 44 521 3 1
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 1 <B 41+V(2) 53+V(1) [*]* [*]*
1 1 1 2 B> 41+V(2) 53+V(1) [*]* [*]*
2 2+V(2) 2+V(2) 2 31+V(2) B> 53+V(1) [*]* [*]*
3 3+V(2) 3+V(2) 2 32+V(2) A> 52+V(1) [*]* [*]*
4 4+V(2) 2+V(2) 2 32+V(2) <B 4 51+V(1) [*]* [*]*
5 6+2*V(2) 0 2 <B 43+V(2) 51+V(1) [*]* [*]*
6 7+2*V(2) -1 <A 3 43+V(2) 51+V(1) [*]* [*]*
7 8+2*V(2) 0 1 B> 3 43+V(2) 51+V(1) [*]* [*]*
8 9+2*V(2) -1 1 <B 44+V(2) 51+V(1) [*]* [*]*
<< Success! ==> defined new CTR 5 (PA)
196 426 -20 1 <B 44 521 3 1
== Executing PA-CTR 5, V(1)=18, V(2)=3, repcount=10, factor=3/2
276 846 -30 1 <B 434 5 3 1
277 847 -29 2 B> 434 5 3 1
278 881 5 2 334 B> 5 3 1
279 882 6 2 335 A> 3 1
280 883 5 2 335 <A 5 1
281 918 -30 2 <A 536 1
282 919 -31 <A 3 536 1
283 920 -30 1 B> 3 536 1
284 921 -31 1 <B 4 536 1
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 1 <B 41+V(1) 5 3 [*]*
1 1 1 2 B> 41+V(1) 5 3 [*]*
2 2+V(1) 2+V(1) 2 31+V(1) B> 5 3 [*]*
3 3+V(1) 3+V(1) 2 32+V(1) A> 3 [*]*
4 4+V(1) 2+V(1) 2 32+V(1) <A 5 [*]*
5 6+2*V(1) 0 2 <A 53+V(1) [*]*
6 7+2*V(1) -1 <A 3 53+V(1) [*]*
7 8+2*V(1) 0 1 B> 3 53+V(1) [*]*
8 9+2*V(1) -1 1 <B 4 53+V(1) [*]*
<< Success! ==> defined new CTR 6 (PPA)
284 921 -31 1 <B 4 536 1
== Executing PA-CTR 1, V(1)=33, V(2)=0, repcount=17, factor=3/2
420 1890 -48 1 <B 452 52 1
421 1891 -47 2 B> 452 52 1
422 1943 5 2 352 B> 52 1
423 1944 6 2 353 A> 5 1
424 1945 5 2 353 <B 4 1
425 1998 -48 2 <B 454 1
426 1999 -49 <A 3 454 1
427 2000 -48 1 B> 3 454 1
428 2001 -49 1 <B 455 1
429 2002 -48 2 B> 455 1
430 2057 7 2 355 B> 1
431 2058 8 2 355 2 B>
432 2059 7 2 355 2 <A 1
433 2060 6 2 355 <A 3 1
434 2115 -49 2 <A 555 3 1
435 2116 -50 <A 3 555 3 1
436 2117 -49 1 B> 3 555 3 1
437 2118 -50 1 <B 4 555 3 1
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 1 <B 41+V(2) 52 11+V(1)
1 1 1 2 B> 41+V(2) 52 11+V(1)
2 2+V(2) 2+V(2) 2 31+V(2) B> 52 11+V(1)
3 3+V(2) 3+V(2) 2 32+V(2) A> 5 11+V(1)
4 4+V(2) 2+V(2) 2 32+V(2) <B 4 11+V(1)
5 6+2*V(2) 0 2 <B 43+V(2) 11+V(1)
6 7+2*V(2) -1 <A 3 43+V(2) 11+V(1)
7 8+2*V(2) 0 1 B> 3 43+V(2) 11+V(1)
8 9+2*V(2) -1 1 <B 44+V(2) 11+V(1)
9 10+2*V(2) 0 2 B> 44+V(2) 11+V(1)
10 14+3*V(2) 4+V(2) 2 34+V(2) B> 11+V(1)
11 15+V(1)+3*V(2) 5+V(1)+V(2) 2 34+V(2) 21+V(1) B>
12 16+V(1)+3*V(2) 4+V(1)+V(2) 2 34+V(2) 21+V(1) <A 1
13 17+2*V(1)+3*V(2) 3+V(2) 2 34+V(2) <A 31+V(1) 1
14 21+2*V(1)+4*V(2) -1 2 <A 54+V(2) 31+V(1) 1
15 22+2*V(1)+4*V(2) -2 <A 3 54+V(2) 31+V(1) 1
16 23+2*V(1)+4*V(2) -1 1 B> 3 54+V(2) 31+V(1) 1
17 24+2*V(1)+4*V(2) -2 1 <B 4 54+V(2) 31+V(1) 1
<< Success! ==> defined new CTR 7 (PPA)
437 2118 -50 1 <B 4 555 3 1
== Executing PA-CTR 5, V(1)=52, V(2)=0, repcount=27, factor=3/2
653 4467 -77 1 <B 482 5 3 1
== Executing PPA-CTR 6 (once), V(1)=81
661 4638 -78 1 <B 4 584 1
== Executing PA-CTR 1, V(1)=81, V(2)=0, repcount=41, factor=3/2
989 9927 -119 1 <B 4124 52 1
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=123
1006 10443 -121 1 <B 4 5127 3 1
== Executing PA-CTR 5, V(1)=124, V(2)=0, repcount=63, factor=3/2
1510 22728 -184 1 <B 4190 5 3 1
== Executing PPA-CTR 6 (once), V(1)=189
1518 23115 -185 1 <B 4 5192 1
== Executing PA-CTR 1, V(1)=189, V(2)=0, repcount=95, factor=3/2
2278 50760 -280 1 <B 4286 52 1
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=285
2295 51924 -282 1 <B 4 5289 3 1
== Executing PA-CTR 5, V(1)=286, V(2)=0, repcount=144, factor=3/2
3447 114996 -426 1 <B 4433 5 3 1
== Executing PPA-CTR 6 (once), V(1)=432
3455 115869 -427 1 <B 4 5435 1
== Executing PA-CTR 1, V(1)=432, V(2)=0, repcount=217, factor=3/2
5191 258438 -644 1 <B 4652 5 1
5192 258439 -643 2 B> 4652 5 1
5193 259091 9 2 3652 B> 5 1
5194 259092 10 2 3653 A> 1
5195 259093 11 2 3653 0 B>
5196 259094 10 2 3653 0 <A 1
5197 259095 11 2 3653 1 B> 1
5198 259096 12 2 3653 1 2 B>
5199 259097 11 2 3653 1 2 <A 1
5200 259098 10 2 3653 1 <A 3 1
5201 259099 11 2 3653 0 B> 3 1
5202 259100 10 2 3653 0 <B 4 1
5203 259101 9 2 3653 <A 1 4 1
5204 259754 -644 2 <A 5653 1 4 1
5205 259755 -645 <A 3 5653 1 4 1
5206 259756 -644 1 B> 3 5653 1 4 1
5207 259757 -645 1 <B 4 5653 1 4 1
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 1 <B 42+V(1) 5 1
1 1 1 2 B> 42+V(1) 5 1
2 3+V(1) 3+V(1) 2 32+V(1) B> 5 1
3 4+V(1) 4+V(1) 2 33+V(1) A> 1
4 5+V(1) 5+V(1) 2 33+V(1) 0 B>
5 6+V(1) 4+V(1) 2 33+V(1) 0 <A 1
6 7+V(1) 5+V(1) 2 33+V(1) 1 B> 1
7 8+V(1) 6+V(1) 2 33+V(1) 1 2 B>
8 9+V(1) 5+V(1) 2 33+V(1) 1 2 <A 1
9 10+V(1) 4+V(1) 2 33+V(1) 1 <A 3 1
10 11+V(1) 5+V(1) 2 33+V(1) 0 B> 3 1
11 12+V(1) 4+V(1) 2 33+V(1) 0 <B 4 1
12 13+V(1) 3+V(1) 2 33+V(1) <A 1 4 1
13 16+2*V(1) 0 2 <A 53+V(1) 1 4 1
14 17+2*V(1) -1 <A 3 53+V(1) 1 4 1
15 18+2*V(1) 0 1 B> 3 53+V(1) 1 4 1
16 19+2*V(1) -1 1 <B 4 53+V(1) 1 4 1
<< Success! ==> defined new CTR 8 (PPA)
5207 259757 -645 1 <B 4 5653 1 4 1
== Executing PA-CTR 2, V(1)=650, V(2)=0, repcount=326, factor=3/2
7815 580541 -971 1 <B 4979 5 1 4 1
== Executing PPA-CTR 3 (once), V(1)=977
7837 582520 -972 1 <B 4 5980 1 42 1
== Executing PA-CTR 2, V(1)=977, V(2)=0, repcount=489, factor=3/2
11749 1302817 -1461 1 <B 41468 52 1 42 1
11750 1302818 -1460 2 B> 41468 52 1 42 1
11751 1304286 8 2 31468 B> 52 1 42 1
11752 1304287 9 2 31469 A> 5 1 42 1
11753 1304288 8 2 31469 <B 4 1 42 1
11754 1305757 -1461 2 <B 41470 1 42 1
11755 1305758 -1462 <A 3 41470 1 42 1
11756 1305759 -1461 1 B> 3 41470 1 42 1
11757 1305760 -1462 1 <B 41471 1 42 1
11758 1305761 -1461 2 B> 41471 1 42 1
11759 1307232 10 2 31471 B> 1 42 1
11760 1307233 11 2 31471 2 B> 42 1
11761 1307235 13 2 31471 2 32 B> 1
11762 1307236 14 2 31471 2 32 2 B>
11763 1307237 13 2 31471 2 32 2 <A 1
11764 1307238 12 2 31471 2 32 <A 3 1
11765 1307240 10 2 31471 2 <A 52 3 1
11766 1307241 9 2 31471 <A 3 52 3 1
11767 1308712 -1462 2 <A 51471 3 52 3 1
11768 1308713 -1463 <A 3 51471 3 52 3 1
11769 1308714 -1462 1 B> 3 51471 3 52 3 1
11770 1308715 -1463 1 <B 4 51471 3 52 3 1
>> Try to prove a PPA-CTR with 4 Vars...
0 0 0 1 <B 41+V(4) 52 11+V(3) 41+V(2) 11+V(1)
1 1 1 2 B> 41+V(4) 52 11+V(3) 41+V(2) 11+V(1)
2 2+V(4) 2+V(4) 2 31+V(4) B> 52 11+V(3) 41+V(2) 11+V(1)
3 3+V(4) 3+V(4) 2 32+V(4) A> 5 11+V(3) 41+V(2) 11+V(1)
4 4+V(4) 2+V(4) 2 32+V(4) <B 4 11+V(3) 41+V(2) 11+V(1)
5 6+2*V(4) 0 2 <B 43+V(4) 11+V(3) 41+V(2) 11+V(1)
6 7+2*V(4) -1 <A 3 43+V(4) 11+V(3) 41+V(2) 11+V(1)
7 8+2*V(4) 0 1 B> 3 43+V(4) 11+V(3) 41+V(2) 11+V(1)
8 9+2*V(4) -1 1 <B 44+V(4) 11+V(3) 41+V(2) 11+V(1)
9 10+2*V(4) 0 2 B> 44+V(4) 11+V(3) 41+V(2) 11+V(1)
10 14+3*V(4) 4+V(4) 2 34+V(4) B> 11+V(3) 41+V(2) 11+V(1)
11 15+V(3)+3*V(4) 5+V(3)+V(4) 2 34+V(4) 21+V(3) B> 41+V(2) 11+V(1)
12 16+V(2)+V(3)+3*V(4) 6+V(2)+V(3)+V(4) 2 34+V(4) 21+V(3) 31+V(2) B> 11+V(1)
13 17+V(1)+V(2)+V(3)+3*V(4) 7+V(1)+V(2)+V(3)+V(4) 2 34+V(4) 21+V(3) 31+V(2) 21+V(1) B>
14 18+V(1)+V(2)+V(3)+3*V(4) 6+V(1)+V(2)+V(3)+V(4) 2 34+V(4) 21+V(3) 31+V(2) 21+V(1) <A 1
15 19+2*V(1)+V(2)+V(3)+3*V(4) 5+V(2)+V(3)+V(4) 2 34+V(4) 21+V(3) 31+V(2) <A 31+V(1) 1
16 20+2*V(1)+2*V(2)+V(3)+3*V(4) 4+V(3)+V(4) 2 34+V(4) 21+V(3) <A 51+V(2) 31+V(1) 1
17 21+2*V(1)+2*V(2)+2*V(3)+3*V(4) 3+V(4) 2 34+V(4) <A 31+V(3) 51+V(2) 31+V(1) 1
18 25+2*V(1)+2*V(2)+2*V(3)+4*V(4) -1 2 <A 54+V(4) 31+V(3) 51+V(2) 31+V(1) 1
19 26+2*V(1)+2*V(2)+2*V(3)+4*V(4) -2 <A 3 54+V(4) 31+V(3) 51+V(2) 31+V(1) 1
20 27+2*V(1)+2*V(2)+2*V(3)+4*V(4) -1 1 B> 3 54+V(4) 31+V(3) 51+V(2) 31+V(1) 1
21 28+2*V(1)+2*V(2)+2*V(3)+4*V(4) -2 1 <B 4 54+V(4) 31+V(3) 51+V(2) 31+V(1) 1
<< Success! ==> defined new CTR 9 (PPA)
11770 1308715 -1463 1 <B 4 51471 3 52 3 1
== Executing PA-CTR 4, V(1)=1468, V(2)=0, repcount=735, factor=3/2
17650 2933800 -2198 1 <B 42206 5 3 52 3 1
17651 2933801 -2197 2 B> 42206 5 3 52 3 1
17652 2936007 9 2 32206 B> 5 3 52 3 1
17653 2936008 10 2 32207 A> 3 52 3 1
17654 2936009 9 2 32207 <A 53 3 1
17655 2938216 -2198 2 <A 52210 3 1
17656 2938217 -2199 <A 3 52210 3 1
17657 2938218 -2198 1 B> 3 52210 3 1
17658 2938219 -2199 1 <B 4 52210 3 1
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 1 <B 41+V(2) 5 3 51+V(1) [*]* [*]*
1 1 1 2 B> 41+V(2) 5 3 51+V(1) [*]* [*]*
2 2+V(2) 2+V(2) 2 31+V(2) B> 5 3 51+V(1) [*]* [*]*
3 3+V(2) 3+V(2) 2 32+V(2) A> 3 51+V(1) [*]* [*]*
4 4+V(2) 2+V(2) 2 32+V(2) <A 52+V(1) [*]* [*]*
5 6+2*V(2) 0 2 <A 54+V(1)+V(2) [*]* [*]*
6 7+2*V(2) -1 <A 3 54+V(1)+V(2) [*]* [*]*
7 8+2*V(2) 0 1 B> 3 54+V(1)+V(2) [*]* [*]*
8 9+2*V(2) -1 1 <B 4 54+V(1)+V(2) [*]* [*]*
<< Success! ==> defined new CTR 10 (PPA)
17658 2938219 -2199 1 <B 4 52210 3 1
== Executing PA-CTR 5, V(1)=2207, V(2)=0, repcount=1104, factor=3/2
26490 6601291 -3303 1 <B 43313 52 3 1
26491 6601292 -3302 2 B> 43313 52 3 1
26492 6604605 11 2 33313 B> 52 3 1
26493 6604606 12 2 33314 A> 5 3 1
26494 6604607 11 2 33314 <B 4 3 1
26495 6607921 -3303 2 <B 43315 3 1
26496 6607922 -3304 <A 3 43315 3 1
26497 6607923 -3303 1 B> 3 43315 3 1
26498 6607924 -3304 1 <B 43316 3 1
26499 6607925 -3303 2 B> 43316 3 1
26500 6611241 13 2 33316 B> 3 1
26501 6611242 12 2 33316 <B 4 1
26502 6614558 -3304 2 <B 43317 1
26503 6614559 -3305 <A 3 43317 1
26504 6614560 -3304 1 B> 3 43317 1
26505 6614561 -3305 1 <B 43318 1
26506 6614562 -3304 2 B> 43318 1
26507 6617880 14 2 33318 B> 1
26508 6617881 15 2 33318 2 B>
26509 6617882 14 2 33318 2 <A 1
26510 6617883 13 2 33318 <A 3 1
26511 6621201 -3305 2 <A 53318 3 1
26512 6621202 -3306 <A 3 53318 3 1
26513 6621203 -3305 1 B> 3 53318 3 1
26514 6621204 -3306 1 <B 4 53318 3 1
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 1 <B 41+V(2) 52 3 11+V(1)
1 1 1 2 B> 41+V(2) 52 3 11+V(1)
2 2+V(2) 2+V(2) 2 31+V(2) B> 52 3 11+V(1)
3 3+V(2) 3+V(2) 2 32+V(2) A> 5 3 11+V(1)
4 4+V(2) 2+V(2) 2 32+V(2) <B 4 3 11+V(1)
5 6+2*V(2) 0 2 <B 43+V(2) 3 11+V(1)
6 7+2*V(2) -1 <A 3 43+V(2) 3 11+V(1)
7 8+2*V(2) 0 1 B> 3 43+V(2) 3 11+V(1)
8 9+2*V(2) -1 1 <B 44+V(2) 3 11+V(1)
9 10+2*V(2) 0 2 B> 44+V(2) 3 11+V(1)
10 14+3*V(2) 4+V(2) 2 34+V(2) B> 3 11+V(1)
11 15+3*V(2) 3+V(2) 2 34+V(2) <B 4 11+V(1)
12 19+4*V(2) -1 2 <B 45+V(2) 11+V(1)
13 20+4*V(2) -2 <A 3 45+V(2) 11+V(1)
14 21+4*V(2) -1 1 B> 3 45+V(2) 11+V(1)
15 22+4*V(2) -2 1 <B 46+V(2) 11+V(1)
16 23+4*V(2) -1 2 B> 46+V(2) 11+V(1)
17 29+5*V(2) 5+V(2) 2 36+V(2) B> 11+V(1)
18 30+V(1)+5*V(2) 6+V(1)+V(2) 2 36+V(2) 21+V(1) B>
19 31+V(1)+5*V(2) 5+V(1)+V(2) 2 36+V(2) 21+V(1) <A 1
20 32+2*V(1)+5*V(2) 4+V(2) 2 36+V(2) <A 31+V(1) 1
21 38+2*V(1)+6*V(2) -2 2 <A 56+V(2) 31+V(1) 1
22 39+2*V(1)+6*V(2) -3 <A 3 56+V(2) 31+V(1) 1
23 40+2*V(1)+6*V(2) -2 1 B> 3 56+V(2) 31+V(1) 1
24 41+2*V(1)+6*V(2) -3 1 <B 4 56+V(2) 31+V(1) 1
<< Success! ==> defined new CTR 11 (PPA)
26514 6621204 -3306 1 <B 4 53318 3 1
== Executing PA-CTR 5, V(1)=3315, V(2)=0, repcount=1658, factor=3/2
39778 14878044 -4964 1 <B 44975 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=4974
39802 14907929 -4967 1 <B 4 54980 3 1
== Executing PA-CTR 5, V(1)=4977, V(2)=0, repcount=2489, factor=3/2
59714 33508226 -7456 1 <B 47468 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=7467
59738 33553069 -7459 1 <B 4 57473 3 1
== Executing PA-CTR 5, V(1)=7470, V(2)=0, repcount=3736, factor=3/2
89626 75448573 -11195 1 <B 411209 5 3 1
== Executing PPA-CTR 6 (once), V(1)=11208
89634 75470998 -11196 1 <B 4 511211 1
== Executing PA-CTR 1, V(1)=11208, V(2)=0, repcount=5605, factor=3/2
134474 169752703 -16801 1 <B 416816 5 1
== Executing PPA-CTR 8 (once), V(1)=16814
134490 169786350 -16802 1 <B 4 516817 1 4 1
== Executing PA-CTR 2, V(1)=16814, V(2)=0, repcount=8408, factor=3/2
201754 381920190 -25210 1 <B 425225 5 1 4 1
== Executing PPA-CTR 3 (once), V(1)=25223
201776 381970661 -25211 1 <B 4 525226 1 42 1
== Executing PA-CTR 2, V(1)=25223, V(2)=0, repcount=12612, factor=3/2
302672 859233965 -37823 1 <B 437837 52 1 42 1
== Executing PPA-CTR 9 (once), V(1)=0, V(2)=1, V(3)=0, V(4)=37836
302693 859385339 -37825 1 <B 4 537840 3 52 3 1
== Executing PA-CTR 4, V(1)=37837, V(2)=0, repcount=18919, factor=3/2
454045 1933284536 -56744 1 <B 456758 52 3 52 3 1
454046 1933284537 -56743 2 B> 456758 52 3 52 3 1
454047 1933341295 15 2 356758 B> 52 3 52 3 1
454048 1933341296 16 2 356759 A> 5 3 52 3 1
454049 1933341297 15 2 356759 <B 4 3 52 3 1
454050 1933398056 -56744 2 <B 456760 3 52 3 1
454051 1933398057 -56745 <A 3 456760 3 52 3 1
454052 1933398058 -56744 1 B> 3 456760 3 52 3 1
454053 1933398059 -56745 1 <B 456761 3 52 3 1
454054 1933398060 -56744 2 B> 456761 3 52 3 1
454055 1933454821 17 2 356761 B> 3 52 3 1
454056 1933454822 16 2 356761 <B 4 52 3 1
454057 1933511583 -56745 2 <B 456762 52 3 1
454058 1933511584 -56746 <A 3 456762 52 3 1
454059 1933511585 -56745 1 B> 3 456762 52 3 1
454060 1933511586 -56746 1 <B 456763 52 3 1
454061 1933511587 -56745 2 B> 456763 52 3 1
454062 1933568350 18 2 356763 B> 52 3 1
454063 1933568351 19 2 356764 A> 5 3 1
454064 1933568352 18 2 356764 <B 4 3 1
454065 1933625116 -56746 2 <B 456765 3 1
454066 1933625117 -56747 <A 3 456765 3 1
454067 1933625118 -56746 1 B> 3 456765 3 1
454068 1933625119 -56747 1 <B 456766 3 1
454069 1933625120 -56746 2 B> 456766 3 1
454070 1933681886 20 2 356766 B> 3 1
454071 1933681887 19 2 356766 <B 4 1
454072 1933738653 -56747 2 <B 456767 1
454073 1933738654 -56748 <A 3 456767 1
454074 1933738655 -56747 1 B> 3 456767 1
454075 1933738656 -56748 1 <B 456768 1
454076 1933738657 -56747 2 B> 456768 1
454077 1933795425 21 2 356768 B> 1
454078 1933795426 22 2 356768 2 B>
454079 1933795427 21 2 356768 2 <A 1
454080 1933795428 20 2 356768 <A 3 1
454081 1933852196 -56748 2 <A 556768 3 1
454082 1933852197 -56749 <A 3 556768 3 1
454083 1933852198 -56748 1 B> 3 556768 3 1
454084 1933852199 -56749 1 <B 4 556768 3 1
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 1 <B 41+V(2) 52 3 52 3 11+V(1)
1 1 1 2 B> 41+V(2) 52 3 52 3 11+V(1)
2 2+V(2) 2+V(2) 2 31+V(2) B> 52 3 52 3 11+V(1)
3 3+V(2) 3+V(2) 2 32+V(2) A> 5 3 52 3 11+V(1)
4 4+V(2) 2+V(2) 2 32+V(2) <B 4 3 52 3 11+V(1)
5 6+2*V(2) 0 2 <B 43+V(2) 3 52 3 11+V(1)
6 7+2*V(2) -1 <A 3 43+V(2) 3 52 3 11+V(1)
7 8+2*V(2) 0 1 B> 3 43+V(2) 3 52 3 11+V(1)
8 9+2*V(2) -1 1 <B 44+V(2) 3 52 3 11+V(1)
9 10+2*V(2) 0 2 B> 44+V(2) 3 52 3 11+V(1)
10 14+3*V(2) 4+V(2) 2 34+V(2) B> 3 52 3 11+V(1)
11 15+3*V(2) 3+V(2) 2 34+V(2) <B 4 52 3 11+V(1)
12 19+4*V(2) -1 2 <B 45+V(2) 52 3 11+V(1)
13 20+4*V(2) -2 <A 3 45+V(2) 52 3 11+V(1)
14 21+4*V(2) -1 1 B> 3 45+V(2) 52 3 11+V(1)
15 22+4*V(2) -2 1 <B 46+V(2) 52 3 11+V(1)
16 23+4*V(2) -1 2 B> 46+V(2) 52 3 11+V(1)
17 29+5*V(2) 5+V(2) 2 36+V(2) B> 52 3 11+V(1)
18 30+5*V(2) 6+V(2) 2 37+V(2) A> 5 3 11+V(1)
19 31+5*V(2) 5+V(2) 2 37+V(2) <B 4 3 11+V(1)
20 38+6*V(2) -2 2 <B 48+V(2) 3 11+V(1)
21 39+6*V(2) -3 <A 3 48+V(2) 3 11+V(1)
22 40+6*V(2) -2 1 B> 3 48+V(2) 3 11+V(1)
23 41+6*V(2) -3 1 <B 49+V(2) 3 11+V(1)
24 42+6*V(2) -2 2 B> 49+V(2) 3 11+V(1)
25 51+7*V(2) 7+V(2) 2 39+V(2) B> 3 11+V(1)
26 52+7*V(2) 6+V(2) 2 39+V(2) <B 4 11+V(1)
27 61+8*V(2) -3 2 <B 410+V(2) 11+V(1)
28 62+8*V(2) -4 <A 3 410+V(2) 11+V(1)
29 63+8*V(2) -3 1 B> 3 410+V(2) 11+V(1)
30 64+8*V(2) -4 1 <B 411+V(2) 11+V(1)
31 65+8*V(2) -3 2 B> 411+V(2) 11+V(1)
32 76+9*V(2) 8+V(2) 2 311+V(2) B> 11+V(1)
33 77+V(1)+9*V(2) 9+V(1)+V(2) 2 311+V(2) 21+V(1) B>
34 78+V(1)+9*V(2) 8+V(1)+V(2) 2 311+V(2) 21+V(1) <A 1
35 79+2*V(1)+9*V(2) 7+V(2) 2 311+V(2) <A 31+V(1) 1
36 90+2*V(1)+10*V(2) -4 2 <A 511+V(2) 31+V(1) 1
37 91+2*V(1)+10*V(2) -5 <A 3 511+V(2) 31+V(1) 1
38 92+2*V(1)+10*V(2) -4 1 B> 3 511+V(2) 31+V(1) 1
39 93+2*V(1)+10*V(2) -5 1 <B 4 511+V(2) 31+V(1) 1
<< Success! ==> defined new CTR 12 (PPA)
454084 1933852199 -56749 1 <B 4 556768 3 1
== Executing PA-CTR 5, V(1)=56765, V(2)=0, repcount=28383, factor=3/2
681148 4350806564 -85132 1 <B 485150 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=85149
681172 4351317499 -85135 1 <B 4 585155 3 1
== Executing PA-CTR 5, V(1)=85152, V(2)=0, repcount=42577, factor=3/2
1021788 9789975748 -127712 1 <B 4127732 5 3 1
== Executing PPA-CTR 6 (once), V(1)=127731
1021796 9790231219 -127713 1 <B 4 5127734 1
== Executing PA-CTR 1, V(1)=127731, V(2)=0, repcount=63866, factor=3/2
1532724 22027212283 -191579 1 <B 4191599 52 1
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=191598
1532741 22027978699 -191581 1 <B 4 5191602 3 1
== Executing PA-CTR 5, V(1)=191599, V(2)=0, repcount=95800, factor=3/2
2299141 49561473499 -287381 1 <B 4287401 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=287400
2299165 49563197940 -287384 1 <B 4 5287406 3 1
== Executing PA-CTR 5, V(1)=287403, V(2)=0, repcount=143702, factor=3/2
3448781 111514854564 -431086 1 <B 4431107 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=431106
3448805 111517441241 -431089 1 <B 4 5431112 3 1
== Executing PA-CTR 5, V(1)=431109, V(2)=0, repcount=215555, factor=3/2
5173245 250910608646 -646644 1 <B 4646666 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=646665
5173269 250914488677 -646647 1 <B 4 5646671 3 1
== Executing PA-CTR 5, V(1)=646668, V(2)=0, repcount=323335, factor=3/2
7759949 564552995362 -969982 1 <B 4970006 5 3 1
== Executing PPA-CTR 6 (once), V(1)=970005
7759957 564554935381 -969983 1 <B 4 5970008 1
== Executing PA-CTR 1, V(1)=970005, V(2)=0, repcount=485003, factor=3/2
11639981 1270241575426 -1454986 1 <B 41455010 52 1
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=1455009
11639998 1270247395486 -1454988 1 <B 4 51455013 3 1
== Executing PA-CTR 5, V(1)=1455010, V(2)=0, repcount=727506, factor=3/2
17460046 2858046700630 -2182494 1 <B 42182519 5 3 1
== Executing PPA-CTR 6 (once), V(1)=2182518
17460054 2858051065675 -2182495 1 <B 4 52182521 1
== Executing PA-CTR 1, V(1)=2182518, V(2)=0, repcount=1091260, factor=3/2
26190134 6430602776035 -3273755 1 <B 43273781 5 1
== Executing PPA-CTR 8 (once), V(1)=3273779
26190150 6430609323612 -3273756 1 <B 4 53273782 1 4 1
== Executing PA-CTR 2, V(1)=3273779, V(2)=0, repcount=1636890, factor=3/2
39285270 14468845761252 -4910646 1 <B 44910671 52 1 4 1
== Executing PPA-CTR 9 (once), V(1)=0, V(2)=0, V(3)=0, V(4)=4910670
39285291 14468865403960 -4910648 1 <B 4 54910674 3 5 3 1
== Executing PA-CTR 4, V(1)=4910671, V(2)=0, repcount=2455336, factor=3/2
58927979 32554904754664 -7365984 1 <B 47366009 52 3 5 3 1
58927980 32554904754665 -7365983 2 B> 47366009 52 3 5 3 1
58927981 32554912120674 26 2 37366009 B> 52 3 5 3 1
58927982 32554912120675 27 2 37366010 A> 5 3 5 3 1
58927983 32554912120676 26 2 37366010 <B 4 3 5 3 1
58927984 32554919486686 -7365984 2 <B 47366011 3 5 3 1
58927985 32554919486687 -7365985 <A 3 47366011 3 5 3 1
58927986 32554919486688 -7365984 1 B> 3 47366011 3 5 3 1
58927987 32554919486689 -7365985 1 <B 47366012 3 5 3 1
58927988 32554919486690 -7365984 2 B> 47366012 3 5 3 1
58927989 32554926852702 28 2 37366012 B> 3 5 3 1
58927990 32554926852703 27 2 37366012 <B 4 5 3 1
58927991 32554934218715 -7365985 2 <B 47366013 5 3 1
58927992 32554934218716 -7365986 <A 3 47366013 5 3 1
58927993 32554934218717 -7365985 1 B> 3 47366013 5 3 1
58927994 32554934218718 -7365986 1 <B 47366014 5 3 1
58927995 32554934218719 -7365985 2 B> 47366014 5 3 1
58927996 32554941584733 29 2 37366014 B> 5 3 1
58927997 32554941584734 30 2 37366015 A> 3 1
58927998 32554941584735 29 2 37366015 <A 5 1
58927999 32554948950750 -7365986 2 <A 57366016 1
58928000 32554948950751 -7365987 <A 3 57366016 1
58928001 32554948950752 -7365986 1 B> 3 57366016 1
58928002 32554948950753 -7365987 1 <B 4 57366016 1
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 1 <B 41+V(1) 52 3 5 3 [*]*
1 1 1 2 B> 41+V(1) 52 3 5 3 [*]*
2 2+V(1) 2+V(1) 2 31+V(1) B> 52 3 5 3 [*]*
3 3+V(1) 3+V(1) 2 32+V(1) A> 5 3 5 3 [*]*
4 4+V(1) 2+V(1) 2 32+V(1) <B 4 3 5 3 [*]*
5 6+2*V(1) 0 2 <B 43+V(1) 3 5 3 [*]*
6 7+2*V(1) -1 <A 3 43+V(1) 3 5 3 [*]*
7 8+2*V(1) 0 1 B> 3 43+V(1) 3 5 3 [*]*
8 9+2*V(1) -1 1 <B 44+V(1) 3 5 3 [*]*
9 10+2*V(1) 0 2 B> 44+V(1) 3 5 3 [*]*
10 14+3*V(1) 4+V(1) 2 34+V(1) B> 3 5 3 [*]*
11 15+3*V(1) 3+V(1) 2 34+V(1) <B 4 5 3 [*]*
12 19+4*V(1) -1 2 <B 45+V(1) 5 3 [*]*
13 20+4*V(1) -2 <A 3 45+V(1) 5 3 [*]*
14 21+4*V(1) -1 1 B> 3 45+V(1) 5 3 [*]*
15 22+4*V(1) -2 1 <B 46+V(1) 5 3 [*]*
16 23+4*V(1) -1 2 B> 46+V(1) 5 3 [*]*
17 29+5*V(1) 5+V(1) 2 36+V(1) B> 5 3 [*]*
18 30+5*V(1) 6+V(1) 2 37+V(1) A> 3 [*]*
19 31+5*V(1) 5+V(1) 2 37+V(1) <A 5 [*]*
20 38+6*V(1) -2 2 <A 58+V(1) [*]*
21 39+6*V(1) -3 <A 3 58+V(1) [*]*
22 40+6*V(1) -2 1 B> 3 58+V(1) [*]*
23 41+6*V(1) -3 1 <B 4 58+V(1) [*]*
<< Success! ==> defined new CTR 13 (PPA)
58928002 32554948950753 -7365987 1 <B 4 57366016 1
== Executing PA-CTR 1, V(1)=7366013, V(2)=0, repcount=3683007, factor=3/2
88392058 73248592734942 -11048994 1 <B 411049022 52 1
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=11049021
88392075 73248636931050 -11048996 1 <B 4 511049025 3 1
== Executing PA-CTR 5, V(1)=11049022, V(2)=0, repcount=5524512, factor=3/2
132588171 164809368592554 -16573508 1 <B 416573537 5 3 1
== Executing PPA-CTR 6 (once), V(1)=16573536
132588179 164809401739635 -16573509 1 <B 4 516573539 1
== Executing PA-CTR 1, V(1)=16573536, V(2)=0, repcount=8286769, factor=3/2
198882331 370821072838332 -24860278 1 <B 424860308 5 1
== Executing PPA-CTR 8 (once), V(1)=24860306
198882347 370821122558963 -24860279 1 <B 4 524860309 1 4 1
== Executing PA-CTR 2, V(1)=24860306, V(2)=0, repcount=12430154, factor=3/2
298323579 834347382531035 -37290433 1 <B 437290463 5 1 4 1
== Executing PPA-CTR 3 (once), V(1)=37290461
298323601 834347457111982 -37290434 1 <B 4 537290464 1 42 1
== Executing PA-CTR 2, V(1)=37290461, V(2)=0, repcount=18645231, factor=3/2
447485449 1877281486113451 -55935665 1 <B 455935694 52 1 42 1
== Executing PPA-CTR 9 (once), V(1)=0, V(2)=1, V(3)=0, V(4)=55935693
447485470 1877281709856253 -55935667 1 <B 4 555935697 3 52 3 1
== Executing PA-CTR 4, V(1)=55935694, V(2)=0, repcount=27967848, factor=3/2
671228254 4223883442916653 -83903515 1 <B 483903545 5 3 52 3 1
== Executing PPA-CTR 10 (once), V(1)=1, V(2)=83903544
671228262 4223883610723750 -83903516 1 <B 4 583903549 3 1
== Executing PA-CTR 5, V(1)=83903546, V(2)=0, repcount=41951774, factor=3/2
1006842454 9503737887675622 -125855290 1 <B 4125855323 5 3 1
== Executing PPA-CTR 6 (once), V(1)=125855322
1006842462 9503738139386275 -125855291 1 <B 4 5125855325 1
== Executing PA-CTR 1, V(1)=125855322, V(2)=0, repcount=62927662, factor=3/2
1510263758 21383410451310979 -188782953 1 <B 4188782987 5 1
== Executing PPA-CTR 8 (once), V(1)=188782985
1510263774 21383410828876968 -188782954 1 <B 4 5188782988 1 4 1
== Executing PA-CTR 2, V(1)=188782985, V(2)=0, repcount=94391493, factor=3/2
2265395718 48112673247533073 -283174447 1 <B 4283174480 52 1 4 1
== Executing PPA-CTR 9 (once), V(1)=0, V(2)=0, V(3)=0, V(4)=283174479
2265395739 48112674380231017 -283174449 1 <B 4 5283174483 3 5 3 1
== Executing PA-CTR 4, V(1)=283174480, V(2)=0, repcount=141587241, factor=3/2
3398093667 1082535[4]1730706 -424761690 1 <B 4424761724 5 3 5 3 1
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=424761723
3398093675 1082535[4]1254161 -424761691 1 <B 4 5424761727 3 1
== Executing PA-CTR 5, V(1)=424761724, V(2)=0, repcount=212380863, factor=3/2
5097140579 2435704[4]1413646 -637142554 1 <B 4637142590 5 3 1
== Executing PPA-CTR 6 (once), V(1)=637142589
5097140587 2435704[4]5698833 -637142555 1 <B 4 5637142592 1
== Executing PA-CTR 1, V(1)=637142589, V(2)=0, repcount=318571295, factor=3/2
7645710947 5480334[4]1057678 -955713850 1 <B 4955713886 52 1
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=955713885
7645710964 5480334[4]3913242 -955713852 1 <B 4 5955713889 3 1
== Executing PA-CTR 5, V(1)=955713886, V(2)=0, repcount=477856944, factor=3/2
11468566516 1233075[5]8112314 -1433570796 1 <B 41433570833 5 3 1
== Executing PPA-CTR 6 (once), V(1)=1433570832
11468566524 1233075[5]5253987 -1433570797 1 <B 4 51433570835 1
== Executing PA-CTR 1, V(1)=1433570832, V(2)=0, repcount=716785417, factor=3/2
17202849860 2774419[5]7558156 -2150356214 1 <B 42150356252 5 1
== Executing PPA-CTR 8 (once), V(1)=2150356250
17202849876 2774419[5]8270675 -2150356215 1 <B 4 52150356253 1 4 1
== Executing PA-CTR 2, V(1)=2150356250, V(2)=0, repcount=1075178126, factor=3/2
25804274884 6242443[5]5955059 -3225534341 1 <B 43225534379 5 1 4 1
== Executing PPA-CTR 3 (once), V(1)=3225534377
25804274906 6242443[5]7023838 -3225534342 1 <B 4 53225534380 1 42 1
== Executing PA-CTR 2, V(1)=3225534377, V(2)=0, repcount=1612767189, factor=3/2
38706412418 1404549[6]8512135 -4838301531 1 <B 44838301568 52 1 42 1
== Executing PPA-CTR 9 (once), V(1)=0, V(2)=1, V(3)=0, V(4)=4838301567
38706412439 1404549[6]1718433 -4838301533 1 <B 4 54838301571 3 52 3 1
== Executing PA-CTR 4, V(1)=4838301568, V(2)=0, repcount=2419150785, factor=3/2
58059618719 3160236[6]4971818 -7257452318 1 <B 47257452356 5 3 52 3 1
== Executing PPA-CTR 10 (once), V(1)=1, V(2)=7257452355
58059618727 3160236[6]9876537 -7257452319 1 <B 4 57257452360 3 1
== Executing PA-CTR 5, V(1)=7257452357, V(2)=0, repcount=3628726179, factor=3/2
87089428159 7110532[6]2053734 -10886178498 1 <B 410886178538 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=10886178537
87089428183 7110533[6]9124997 -10886178501 1 <B 4 510886178543 3 1
== Executing PA-CTR 5, V(1)=10886178540, V(2)=0, repcount=5443089271, factor=3/2
130634142351 1599869[7]3594946 -16329267772 1 <B 416329267814 5 3 1
== Executing PPA-CTR 6 (once), V(1)=16329267813
130634142359 1599869[7]2130581 -16329267773 1 <B 4 516329267816 1
== Executing PA-CTR 1, V(1)=16329267813, V(2)=0, repcount=8164633907, factor=3/2
195951213615 3599707[7]2187970 -24493901680 1 <B 424493901722 52 1
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=24493901721
195951213632 3599707[7]7794878 -24493901682 1 <B 4 524493901725 3 1
== Executing PA-CTR 5, V(1)=24493901722, V(2)=0, repcount=12246950862, factor=3/2
293926820528 8099341[7]7129182 -36740852544 1 <B 436740852587 5 3 1
== Executing PPA-CTR 6 (once), V(1)=36740852586
293926820536 8099341[7]8834363 -36740852545 1 <B 4 536740852589 1
== Executing PA-CTR 1, V(1)=36740852586, V(2)=0, repcount=18370426294, factor=3/2
440890230888 1822351[8]1115435 -55111278839 1 <B 455111278883 5 1
== Executing PPA-CTR 8 (once), V(1)=55111278881
440890230904 1822351[8]3673216 -55111278840 1 <B 4 555111278884 1 4 1
== Executing PA-CTR 2, V(1)=55111278881, V(2)=0, repcount=27555639441, factor=3/2
661335346432 4100291[8]1887305 -82666918281 1 <B 482666918324 52 1 4 1
== Executing PPA-CTR 9 (once), V(1)=0, V(2)=0, V(3)=0, V(4)=82666918323
661335346453 4100291[8]9560625 -82666918283 1 <B 4 582666918327 3 5 3 1
== Executing PA-CTR 4, V(1)=82666918324, V(2)=0, repcount=41333459163, factor=3/2
992003019757 9225656[8]6297310 -124000377446 1 <B 4124000377490 5 3 5 3 1
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=124000377489
992003019765 9225656[8]7052297 -124000377447 1 <B 4 5124000377493 3 1
== Executing PA-CTR 5, V(1)=124000377490, V(2)=0, repcount=62000188746, factor=3/2
1488004529733 2075772[9]3342321 -186000566193 1 <B 4186000566239 5 3 1
== Executing PPA-CTR 6 (once), V(1)=186000566238
1488004529741 2075772[9]4474806 -186000566194 1 <B 4 5186000566241 1
== Executing PA-CTR 1, V(1)=186000566238, V(2)=0, repcount=93000283120, factor=3/2
2232006794701 4670488[9]6976726 -279000849314 1 <B 4279000849361 5 1
== Executing PPA-CTR 8 (once), V(1)=279000849359
2232006794717 4670488[9]8675463 -279000849315 1 <B 4 5279000849362 1 4 1
== Executing PA-CTR 2, V(1)=279000849359, V(2)=0, repcount=139500424680, factor=3/2
3348010192157 1050859[10]0530743 -418501273995 1 <B 4418501274041 52 1 4 1
== Executing PPA-CTR 9 (once), V(1)=0, V(2)=0, V(3)=0, V(4)=418501274040
3348010192178 1050859[10]5626931 -418501273997 1 <B 4 5418501274044 3 5 3 1
== Executing PA-CTR 4, V(1)=418501274041, V(2)=0, repcount=209250637021, factor=3/2
5022015288346 2364434[10]6712380 -627751911018 1 <B 4627751911064 52 3 5 3 1
== Executing PPA-CTR 13 (once), V(1)=627751911063
5022015288369 2364434[10]8178799 -627751911021 1 <B 4 5627751911071 1
== Executing PA-CTR 1, V(1)=627751911068, V(2)=0, repcount=313875955535, factor=3/2
7533022932649 5319978[10]5320684 -941627866556 1 <B 4941627866606 5 1
== Executing PPA-CTR 8 (once), V(1)=941627866604
7533022932665 5319978[10]1053911 -941627866557 1 <B 4 5941627866607 1 4 1
== Executing PA-CTR 2, V(1)=941627866604, V(2)=0, repcount=470813933303, factor=3/2
11299534399089 1196995[11]2123156 -1412441799860 1 <B 41412441799910 5 1 4 1
== Executing PPA-CTR 3 (once), V(1)=1412441799908
11299534399111 1196995[11]5722997 -1412441799861 1 <B 4 51412441799911 1 42 1
== Executing PA-CTR 2, V(1)=1412441799908, V(2)=0, repcount=706220899955, factor=3/2
16949301598751 2693238[11]8128802 -2118662699816 1 <B 42118662699866 5 1 42 1
16949301598752 2693238[11]8128803 -2118662699815 2 B> 42118662699866 5 1 42 1
16949301598753 2693238[11]0828669 51 2 32118662699866 B> 5 1 42 1
16949301598754 2693238[11]0828670 52 2 32118662699867 A> 1 42 1
16949301598755 2693238[11]0828671 53 2 32118662699867 0 B> 42 1
16949301598756 2693238[11]0828673 55 2 32118662699867 0 32 B> 1
16949301598757 2693238[11]0828674 56 2 32118662699867 0 32 2 B>
16949301598758 2693238[11]0828675 55 2 32118662699867 0 32 2 <A 1
16949301598759 2693238[11]0828676 54 2 32118662699867 0 32 <A 3 1
16949301598760 2693238[11]0828678 52 2 32118662699867 0 <A 52 3 1
16949301598761 2693238[11]0828679 53 2 32118662699867 1 B> 52 3 1
16949301598762 2693238[11]0828680 54 2 32118662699867 1 3 A> 5 3 1
16949301598763 2693238[11]0828681 53 2 32118662699867 1 3 <B 4 3 1
16949301598764 2693238[11]0828682 52 2 32118662699867 1 <B 42 3 1
16949301598765 2693238[11]0828683 53 2 32118662699867 2 B> 42 3 1
16949301598766 2693238[11]0828685 55 2 32118662699867 2 32 B> 3 1
16949301598767 2693238[11]0828686 54 2 32118662699867 2 32 <B 4 1
16949301598768 2693238[11]0828688 52 2 32118662699867 2 <B 43 1
16949301598769 2693238[11]0828689 51 2 32118662699867 <A 3 43 1
16949301598770 2693238[11]3528556 -2118662699816 2 <A 52118662699867 3 43 1
16949301598771 2693238[11]3528557 -2118662699817 <A 3 52118662699867 3 43 1
16949301598772 2693238[11]3528558 -2118662699816 1 B> 3 52118662699867 3 43 1
16949301598773 2693238[11]3528559 -2118662699817 1 <B 4 52118662699867 3 43 1
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 1 <B 42+V(1) 5 1 42 1
1 1 1 2 B> 42+V(1) 5 1 42 1
2 3+V(1) 3+V(1) 2 32+V(1) B> 5 1 42 1
3 4+V(1) 4+V(1) 2 33+V(1) A> 1 42 1
4 5+V(1) 5+V(1) 2 33+V(1) 0 B> 42 1
5 7+V(1) 7+V(1) 2 33+V(1) 0 32 B> 1
6 8+V(1) 8+V(1) 2 33+V(1) 0 32 2 B>
7 9+V(1) 7+V(1) 2 33+V(1) 0 32 2 <A 1
8 10+V(1) 6+V(1) 2 33+V(1) 0 32 <A 3 1
9 12+V(1) 4+V(1) 2 33+V(1) 0 <A 52 3 1
10 13+V(1) 5+V(1) 2 33+V(1) 1 B> 52 3 1
11 14+V(1) 6+V(1) 2 33+V(1) 1 3 A> 5 3 1
12 15+V(1) 5+V(1) 2 33+V(1) 1 3 <B 4 3 1
13 16+V(1) 4+V(1) 2 33+V(1) 1 <B 42 3 1
14 17+V(1) 5+V(1) 2 33+V(1) 2 B> 42 3 1
15 19+V(1) 7+V(1) 2 33+V(1) 2 32 B> 3 1
16 20+V(1) 6+V(1) 2 33+V(1) 2 32 <B 4 1
17 22+V(1) 4+V(1) 2 33+V(1) 2 <B 43 1
18 23+V(1) 3+V(1) 2 33+V(1) <A 3 43 1
19 26+2*V(1) 0 2 <A 53+V(1) 3 43 1
20 27+2*V(1) -1 <A 3 53+V(1) 3 43 1
21 28+2*V(1) 0 1 B> 3 53+V(1) 3 43 1
22 29+2*V(1) -1 1 <B 4 53+V(1) 3 43 1
<< Success! ==> defined new CTR 14 (PPA)
16949301598773 2693238[11]3528559 -2118662699817 1 <B 4 52118662699867 3 43 1
== Executing PA-CTR 2, V(1)=2118662699864, V(2)=0, repcount=1059331349933, factor=3/2
25423952398237 6059787[11]8941624 -3177994049750 1 <B 43177994049800 5 3 43 1
25423952398238 6059787[11]8941625 -3177994049749 2 B> 43177994049800 5 3 43 1
25423952398239 6059787[11]2991425 51 2 33177994049800 B> 5 3 43 1
25423952398240 6059787[11]2991426 52 2 33177994049801 A> 3 43 1
25423952398241 6059787[11]2991427 51 2 33177994049801 <A 5 43 1
25423952398242 6059787[11]7041228 -3177994049750 2 <A 53177994049802 43 1
25423952398243 6059787[11]7041229 -3177994049751 <A 3 53177994049802 43 1
25423952398244 6059787[11]7041230 -3177994049750 1 B> 3 53177994049802 43 1
25423952398245 6059787[11]7041231 -3177994049751 1 <B 4 53177994049802 43 1
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 1 <B 41+V(1) 5 3 [*]* [*]*
1 1 1 2 B> 41+V(1) 5 3 [*]* [*]*
2 2+V(1) 2+V(1) 2 31+V(1) B> 5 3 [*]* [*]*
3 3+V(1) 3+V(1) 2 32+V(1) A> 3 [*]* [*]*
4 4+V(1) 2+V(1) 2 32+V(1) <A 5 [*]* [*]*
5 6+2*V(1) 0 2 <A 53+V(1) [*]* [*]*
6 7+2*V(1) -1 <A 3 53+V(1) [*]* [*]*
7 8+2*V(1) 0 1 B> 3 53+V(1) [*]* [*]*
8 9+2*V(1) -1 1 <B 4 53+V(1) [*]* [*]*
<< Success! ==> defined new CTR 15 (PPA)
25423952398245 6059787[11]7041231 -3177994049751 1 <B 4 53177994049802 43 1
== Executing PA-CTR 5, V(1)=3177994049799, V(2)=0, repcount=1588997024900, factor=3/2
38135928597445 1363452[12]9220631 -4766991074651 1 <B 44766991074701 52 43 1
38135928597446 1363452[12]9220632 -4766991074650 2 B> 44766991074701 52 43 1
38135928597447 1363452[12]0295333 51 2 34766991074701 B> 52 43 1
38135928597448 1363452[12]0295334 52 2 34766991074702 A> 5 43 1
38135928597449 1363452[12]0295335 51 2 34766991074702 <B 44 1
38135928597450 1363452[12]1370037 -4766991074651 2 <B 44766991074706 1
38135928597451 1363452[12]1370038 -4766991074652 <A 3 44766991074706 1
38135928597452 1363452[12]1370039 -4766991074651 1 B> 3 44766991074706 1
38135928597453 1363452[12]1370040 -4766991074652 1 <B 44766991074707 1
38135928597454 1363452[12]1370041 -4766991074651 2 B> 44766991074707 1
38135928597455 1363452[12]2444748 56 2 34766991074707 B> 1
38135928597456 1363452[12]2444749 57 2 34766991074707 2 B>
38135928597457 1363452[12]2444750 56 2 34766991074707 2 <A 1
38135928597458 1363452[12]2444751 55 2 34766991074707 <A 3 1
38135928597459 1363452[12]3519458 -4766991074652 2 <A 54766991074707 3 1
38135928597460 1363452[12]3519459 -4766991074653 <A 3 54766991074707 3 1
38135928597461 1363452[12]3519460 -4766991074652 1 B> 3 54766991074707 3 1
38135928597462 1363452[12]3519461 -4766991074653 1 <B 4 54766991074707 3 1
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 1 <B 41+V(3) 52 41+V(2) 11+V(1)
1 1 1 2 B> 41+V(3) 52 41+V(2) 11+V(1)
2 2+V(3) 2+V(3) 2 31+V(3) B> 52 41+V(2) 11+V(1)
3 3+V(3) 3+V(3) 2 32+V(3) A> 5 41+V(2) 11+V(1)
4 4+V(3) 2+V(3) 2 32+V(3) <B 42+V(2) 11+V(1)
5 6+2*V(3) 0 2 <B 44+V(2)+V(3) 11+V(1)
6 7+2*V(3) -1 <A 3 44+V(2)+V(3) 11+V(1)
7 8+2*V(3) 0 1 B> 3 44+V(2)+V(3) 11+V(1)
8 9+2*V(3) -1 1 <B 45+V(2)+V(3) 11+V(1)
9 10+2*V(3) 0 2 B> 45+V(2)+V(3) 11+V(1)
10 15+V(2)+3*V(3) 5+V(2)+V(3) 2 35+V(2)+V(3) B> 11+V(1)
11 16+V(1)+V(2)+3*V(3) 6+V(1)+V(2)+V(3) 2 35+V(2)+V(3) 21+V(1) B>
12 17+V(1)+V(2)+3*V(3) 5+V(1)+V(2)+V(3) 2 35+V(2)+V(3) 21+V(1) <A 1
13 18+2*V(1)+V(2)+3*V(3) 4+V(2)+V(3) 2 35+V(2)+V(3) <A 31+V(1) 1
14 23+2*V(1)+2*V(2)+4*V(3) -1 2 <A 55+V(2)+V(3) 31+V(1) 1
15 24+2*V(1)+2*V(2)+4*V(3) -2 <A 3 55+V(2)+V(3) 31+V(1) 1
16 25+2*V(1)+2*V(2)+4*V(3) -1 1 B> 3 55+V(2)+V(3) 31+V(1) 1
17 26+2*V(1)+2*V(2)+4*V(3) -2 1 <B 4 55+V(2)+V(3) 31+V(1) 1
<< Success! ==> defined new CTR 16 (PPA)
38135928597462 1363452[12]3519461 -4766991074653 1 <B 4 54766991074707 3 1
== Executing PA-CTR 5, V(1)=4766991074704, V(2)=0, repcount=2383495537353, factor=3/2
57203892896286 3067767[12]1483406 -7150486612006 1 <B 47150486612060 5 3 1
== Executing PPA-CTR 6 (once), V(1)=7150486612059
57203892896294 3067767[12]4707533 -7150486612007 1 <B 4 57150486612062 1
== Executing PA-CTR 1, V(1)=7150486612059, V(2)=0, repcount=3575243306030, factor=3/2
85805839344534 6902476[12]7626413 -10725729918037 1 <B 410725729918091 52 1
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=10725729918090
85805839344551 6902476[12]7298797 -10725729918039 1 <B 4 510725729918094 3 1
== Executing PA-CTR 5, V(1)=10725729918091, V(2)=0, repcount=5362864959046, factor=3/2
128708759016919 1553057[13]8743421 -16088594877085 1 <B 416088594877139 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=16088594877138
128708759016943 1553057[13]8006290 -16088594877088 1 <B 4 516088594877144 3 1
== Executing PA-CTR 5, V(1)=16088594877141, V(2)=0, repcount=8044297438571, factor=3/2
193063138525511 3494378[13]8203839 -24132892315659 1 <B 424132892315714 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=24132892315713
193063138525535 3494378[13]2098158 -24132892315662 1 <B 4 524132892315719 3 1
== Executing PA-CTR 5, V(1)=24132892315716, V(2)=0, repcount=12066446157859, factor=3/2
289594707788407 7862352[13]1436955 -36199338473521 1 <B 436199338473578 5 3 1
== Executing PPA-CTR 6 (once), V(1)=36199338473577
289594707788415 7862352[13]8384118 -36199338473522 1 <B 4 536199338473580 1
== Executing PA-CTR 1, V(1)=36199338473577, V(2)=0, repcount=18099669236789, factor=3/2
434392061682727 1769029[14]6896415 -54299007710311 1 <B 454299007710368 52 1
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=54299007710367
434392061682744 1769029[14]7737907 -54299007710313 1 <B 4 554299007710371 3 1
== Executing PA-CTR 5, V(1)=54299007710368, V(2)=0, repcount=27149503855185, factor=3/2
651588092524224 3980316[14]5021692 -81448511565498 1 <B 481448511565556 5 3 1
== Executing PPA-CTR 6 (once), V(1)=81448511565555
651588092524232 3980316[14]8152811 -81448511565499 1 <B 4 581448511565558 1
== Executing PA-CTR 1, V(1)=81448511565555, V(2)=0, repcount=40724255782778, factor=3/2
977382138786456 8955711[14]7041331 -122172767348277 1 <B 4122172767348335 52 1
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=122172767348334
977382138786473 8955711[14]6434691 -122172767348279 1 <B 4 5122172767348338 3 1
== Executing PA-CTR 5, V(1)=122172767348335, V(2)=0, repcount=61086383674168, factor=3/2
1466073208179817 2015034[15]9956371 -183259151022447 1 <B 4183259151022505 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=183259151022504
1466073208179841 2015034[15]6091436 -183259151022450 1 <B 4 5183259151022510 3 1
== Executing PA-CTR 5, V(1)=183259151022507, V(2)=0, repcount=91629575511254, factor=3/2
2199109812269873 4533828[15]1116508 -274888726533704 1 <B 4274888726533763 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=274888726533762
2199109812269897 4533828[15]0319121 -274888726533707 1 <B 4 5274888726533768 3 1
== Executing PA-CTR 5, V(1)=274888726533765, V(2)=0, repcount=137444363266883, factor=3/2
3298664718404961 1020111[16]3527486 -412333089800590 1 <B 4412333089800650 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=412333089800649
3298664718404985 1020111[16]2331421 -412333089800593 1 <B 4 5412333089800655 3 1
== Executing PA-CTR 5, V(1)=412333089800652, V(2)=0, repcount=206166544900327, factor=3/2
4947997077607601 2295250[16]5854170 -618499634700920 1 <B 4618499634700982 5 3 1
== Executing PPA-CTR 6 (once), V(1)=618499634700981
4947997077607609 2295250[16]5256141 -618499634700921 1 <B 4 5618499634700984 1
== Executing PA-CTR 1, V(1)=618499634700981, V(2)=0, repcount=309249817350491, factor=3/2
7421995616411537 5164314[16]3182330 -927749452051412 1 <B 4927749452051474 52 1
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=927749452051473
7421995616411554 5164314[16]1388246 -927749452051414 1 <B 4 5927749452051477 3 1
== Executing PA-CTR 5, V(1)=927749452051474, V(2)=0, repcount=463874726025738, factor=3/2
11132993424617458 1161970[17]2876606 -1391624178077152 1 <B 41391624178077215 5 3 1
== Executing PPA-CTR 6 (once), V(1)=1391624178077214
11132993424617466 1161970[17]9031043 -1391624178077153 1 <B 4 51391624178077217 1
== Executing PA-CTR 1, V(1)=1391624178077214, V(2)=0, repcount=695812089038608, factor=3/2
16699490136926330 2614434[17]6995683 -2087436267115761 1 <B 42087436267115825 5 1
== Executing PPA-CTR 8 (once), V(1)=2087436267115823
16699490136926346 2614434[17]1227348 -2087436267115762 1 <B 4 52087436267115826 1 4 1
== Executing PA-CTR 2, V(1)=2087436267115823, V(2)=0, repcount=1043718133557912, factor=3/2
25049235205389642 5882476[17]5974052 -3131154400673674 1 <B 43131154400673737 52 1 4 1
== Executing PPA-CTR 9 (once), V(1)=0, V(2)=0, V(3)=0, V(4)=3131154400673736
25049235205389663 5882476[17]8669024 -3131154400673676 1 <B 4 53131154400673740 3 5 3 1
== Executing PA-CTR 4, V(1)=3131154400673737, V(2)=0, repcount=1565577200336869, factor=3/2
37573852808084615 1323557[18]2859721 -4696731601010545 1 <B 44696731601010608 52 3 5 3 1
== Executing PPA-CTR 13 (once), V(1)=4696731601010607
37573852808084638 1323557[18]8923404 -4696731601010548 1 <B 4 54696731601010615 1
== Executing PA-CTR 1, V(1)=4696731601010612, V(2)=0, repcount=2348365800505307, factor=3/2
56360779212127094 2978003[18]7447993 -7045097401515855 1 <B 47045097401515922 5 1
== Executing PPA-CTR 8 (once), V(1)=7045097401515920
56360779212127110 2978003[18]0479852 -7045097401515856 1 <B 4 57045097401515923 1 4 1
== Executing PA-CTR 2, V(1)=7045097401515920, V(2)=0, repcount=3522548700757961, factor=3/2
84541168818190798 6700508[18]9660181 -105676[4]2273817 1 <B 410567646102273884 5 1 4 1
== Executing PPA-CTR 3 (once), V(1)=10567646102273882
84541168818190820 6700508[18]4207970 -105676[4]2273818 1 <B 4 510567646102273885 1 42 1
== Executing PA-CTR 2, V(1)=10567646102273882, V(2)=0, repcount=5283823051136942, factor=3/2
1268117[4]7286356 1507614[19]2363714 -158514[4]3410760 1 <B 415851469153410827 5 1 42 1
== Executing PPA-CTR 14 (once), V(1)=15851469153410825
1268117[4]7286378 1507614[19]9185393 -158514[4]3410761 1 <B 4 515851469153410828 3 43 1
== Executing PA-CTR 2, V(1)=15851469153410825, V(2)=0, repcount=7925734576705413, factor=3/2
1902176[4]0929682 3392132[19]9919578 -237772[4]0116174 1 <B 423777203730116240 52 3 43 1
1902176[4]0929683 3392132[19]9919579 -237772[4]0116173 2 B> 423777203730116240 52 3 43 1
1902176[4]0929684 3392132[19]0035819 67 2 323777203730116240 B> 52 3 43 1
1902176[4]0929685 3392132[19]0035820 68 2 323777203730116241 A> 5 3 43 1
1902176[4]0929686 3392132[19]0035821 67 2 323777203730116241 <B 4 3 43 1
1902176[4]0929687 3392132[19]0152062 -237772[4]0116174 2 <B 423777203730116242 3 43 1
1902176[4]0929688 3392132[19]0152063 -237772[4]0116175 <A 3 423777203730116242 3 43 1
1902176[4]0929689 3392132[19]0152064 -237772[4]0116174 1 B> 3 423777203730116242 3 43 1
1902176[4]0929690 3392132[19]0152065 -237772[4]0116175 1 <B 423777203730116243 3 43 1
1902176[4]0929691 3392132[19]0152066 -237772[4]0116174 2 B> 423777203730116243 3 43 1
1902176[4]0929692 3392132[19]0268309 69 2 323777203730116243 B> 3 43 1
1902176[4]0929693 3392132[19]0268310 68 2 323777203730116243 <B 44 1
1902176[4]0929694 3392132[19]0384553 -237772[4]0116175 2 <B 423777203730116247 1
1902176[4]0929695 3392132[19]0384554 -237772[4]0116176 <A 3 423777203730116247 1
1902176[4]0929696 3392132[19]0384555 -237772[4]0116175 1 B> 3 423777203730116247 1
1902176[4]0929697 3392132[19]0384556 -237772[4]0116176 1 <B 423777203730116248 1
1902176[4]0929698 3392132[19]0384557 -237772[4]0116175 2 B> 423777203730116248 1
1902176[4]0929699 3392132[19]0500805 73 2 323777203730116248 B> 1
1902176[4]0929700 3392132[19]0500806 74 2 323777203730116248 2 B>
1902176[4]0929701 3392132[19]0500807 73 2 323777203730116248 2 <A 1
1902176[4]0929702 3392132[19]0500808 72 2 323777203730116248 <A 3 1
1902176[4]0929703 3392132[19]0617056 -237772[4]0116176 2 <A 523777203730116248 3 1
1902176[4]0929704 3392132[19]0617057 -237772[4]0116177 <A 3 523777203730116248 3 1
1902176[4]0929705 3392132[19]0617058 -237772[4]0116176 1 B> 3 523777203730116248 3 1
1902176[4]0929706 3392132[19]0617059 -237772[4]0116177 1 <B 4 523777203730116248 3 1
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 1 <B 41+V(3) 52 3 41+V(2) 11+V(1)
1 1 1 2 B> 41+V(3) 52 3 41+V(2) 11+V(1)
2 2+V(3) 2+V(3) 2 31+V(3) B> 52 3 41+V(2) 11+V(1)
3 3+V(3) 3+V(3) 2 32+V(3) A> 5 3 41+V(2) 11+V(1)
4 4+V(3) 2+V(3) 2 32+V(3) <B 4 3 41+V(2) 11+V(1)
5 6+2*V(3) 0 2 <B 43+V(3) 3 41+V(2) 11+V(1)
6 7+2*V(3) -1 <A 3 43+V(3) 3 41+V(2) 11+V(1)
7 8+2*V(3) 0 1 B> 3 43+V(3) 3 41+V(2) 11+V(1)
8 9+2*V(3) -1 1 <B 44+V(3) 3 41+V(2) 11+V(1)
9 10+2*V(3) 0 2 B> 44+V(3) 3 41+V(2) 11+V(1)
10 14+3*V(3) 4+V(3) 2 34+V(3) B> 3 41+V(2) 11+V(1)
11 15+3*V(3) 3+V(3) 2 34+V(3) <B 42+V(2) 11+V(1)
12 19+4*V(3) -1 2 <B 46+V(2)+V(3) 11+V(1)
13 20+4*V(3) -2 <A 3 46+V(2)+V(3) 11+V(1)
14 21+4*V(3) -1 1 B> 3 46+V(2)+V(3) 11+V(1)
15 22+4*V(3) -2 1 <B 47+V(2)+V(3) 11+V(1)
16 23+4*V(3) -1 2 B> 47+V(2)+V(3) 11+V(1)
17 30+V(2)+5*V(3) 6+V(2)+V(3) 2 37+V(2)+V(3) B> 11+V(1)
18 31+V(1)+V(2)+5*V(3) 7+V(1)+V(2)+V(3) 2 37+V(2)+V(3) 21+V(1) B>
19 32+V(1)+V(2)+5*V(3) 6+V(1)+V(2)+V(3) 2 37+V(2)+V(3) 21+V(1) <A 1
20 33+2*V(1)+V(2)+5*V(3) 5+V(2)+V(3) 2 37+V(2)+V(3) <A 31+V(1) 1
21 40+2*V(1)+2*V(2)+6*V(3) -2 2 <A 57+V(2)+V(3) 31+V(1) 1
22 41+2*V(1)+2*V(2)+6*V(3) -3 <A 3 57+V(2)+V(3) 31+V(1) 1
23 42+2*V(1)+2*V(2)+6*V(3) -2 1 B> 3 57+V(2)+V(3) 31+V(1) 1
24 43+2*V(1)+2*V(2)+6*V(3) -3 1 <B 4 57+V(2)+V(3) 31+V(1) 1
<< Success! ==> defined new CTR 17 (PPA)
1902176[4]0929706 3392132[19]0617059 -237772[4]0116177 1 <B 4 523777203730116248 3 1
== Executing PA-CTR 5, V(1)=23777203730116245, V(2)=0, repcount=11888601865058123, factor=3/2
2853264[4]1394690 7632298[19]5815184 -356658[4]5174300 1 <B 435665805595174370 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=35665805595174369
2853264[4]1394714 7632298[19]6861439 -356658[4]5174303 1 <B 4 535665805595174375 3 1
== Executing PA-CTR 5, V(1)=35665805595174372, V(2)=0, repcount=17832902797587187, factor=3/2
4279896[4]2092210 1717267[20]2103468 -534987[4]2761490 1 <B 453498708392761562 5 3 1
== Executing PPA-CTR 6 (once), V(1)=53498708392761561
4279896[4]2092218 1717267[20]7626599 -534987[4]2761491 1 <B 4 553498708392761564 1
== Executing PA-CTR 1, V(1)=53498708392761561, V(2)=0, repcount=26749354196380781, factor=3/2
6419845[4]3138466 3863850[20]4421168 -802480[4]9142272 1 <B 480248062589142344 52 1
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=80248062589142343
6419845[4]3138483 3863850[20]0990564 -802480[4]9142274 1 <B 4 580248062589142347 3 1
== Executing PA-CTR 5, V(1)=80248062589142344, V(2)=0, repcount=40124031294571173, factor=3/2
9629767[4]9707867 8693664[20]6205389 -120372[5]3713447 1 <B 41203720[4]3713520 5 3 1
== Executing PPA-CTR 6 (once), V(1)=1203720[4]3713519
9629767[4]9707875 8693664[20]3632436 -120372[5]3713448 1 <B 4 51203720[4]3713522 1
== Executing PA-CTR 1, V(1)=1203720[4]3713519, V(2)=0, repcount=60186046941856760, factor=3/2
1444465[5]4561955 1956074[21]7865796 -180558[5]5570208 1 <B 41805581[4]5570281 52 1
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=1805581[4]5570280
1444465[5]4561972 1956074[21]0146940 -180558[5]5570210 1 <B 4 51805581[4]5570284 3 1
== Executing PA-CTR 5, V(1)=1805581[4]5570281, V(2)=0, repcount=90279070412785141, factor=3/2
2166697[5]6843100 4401167[21]8027429 -270837[5]8355351 1 <B 42708372[4]8355424 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=2708372[4]8355423
2166697[5]6843124 4401167[21]8160008 -270837[5]8355354 1 <B 4 52708372[4]8355429 3 1
== Executing PA-CTR 5, V(1)=2708372[4]8355426, V(2)=0, repcount=1354186[4]9177714, factor=3/2
3250046[5]0264836 9902627[21]6023680 -406255[5]7533068 1 <B 44062558[4]7533143 5 3 1
== Executing PPA-CTR 6 (once), V(1)=4062558[4]7533142
3250046[5]0264844 9902627[21]1089973 -406255[5]7533069 1 <B 4 54062558[4]7533145 1
== Executing PA-CTR 1, V(1)=4062558[4]7533142, V(2)=0, repcount=2031279[4]8766572, factor=3/2
4875069[5]0397420 2228091[22]7582957 -609383[5]6299641 1 <B 46093837[4]6299717 5 1
== Executing PPA-CTR 8 (once), V(1)=6093837[4]6299715
4875069[5]0397436 2228091[22]0182406 -609383[5]6299642 1 <B 4 56093837[4]6299718 1 4 1
== Executing PA-CTR 2, V(1)=6093837[4]6299715, V(2)=0, repcount=3046918[4]3149858, factor=3/2
7312604[5]5596300 5013205[22]5342046 -914075[5]9449500 1 <B 49140755[4]9449575 52 1 4 1
== Executing PPA-CTR 9 (once), V(1)=0, V(2)=0, V(3)=0, V(4)=9140755[4]9449574
7312604[5]5596321 5013205[22]3140370 -914075[5]9449502 1 <B 4 59140755[4]9449578 3 5 3 1
== Executing PA-CTR 4, V(1)=9140755[4]9449575, V(2)=0, repcount=4570377[4]4724788, factor=3/2
1096890[6]3394625 1127971[23]6423930 -137111[6]4174290 1 <B 41371113[5]4174365 52 3 5 3 1
== Executing PPA-CTR 13 (once), V(1)=1371113[5]4174364
1096890[6]3394648 1127971[23]1470155 -137111[6]4174293 1 <B 4 51371113[5]4174372 1
== Executing PA-CTR 1, V(1)=1371113[5]4174369, V(2)=0, repcount=6855566[4]7087185, factor=3/2
1645336[6]0092128 2537935[23]7665940 -205667[6]1261478 1 <B 42056670[5]1261556 52 1
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=2056670[5]1261555
1645336[6]0092145 2537935[23]2712184 -205667[6]1261480 1 <B 4 52056670[5]1261559 3 1
== Executing PA-CTR 5, V(1)=2056670[5]1261556, V(2)=0, repcount=1028335[5]0630779, factor=3/2
2468004[6]5138377 5710353[23]2937381 -308500[6]1892259 1 <B 43085005[5]1892338 5 3 1
== Executing PPA-CTR 6 (once), V(1)=3085005[5]1892337
2468004[6]5138385 5710353[23]6722064 -308500[6]1892260 1 <B 4 53085005[5]1892340 1
== Executing PA-CTR 1, V(1)=3085005[5]1892337, V(2)=0, repcount=1542502[5]0946169, factor=3/2
3702006[6]2707737 1284829[24]9728761 -462750[6]2838429 1 <B 44627507[5]2838508 52 1
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=4627507[5]2838507
3702006[6]2707754 1284829[24]1082813 -462750[6]2838431 1 <B 4 54627507[5]2838511 3 1
== Executing PA-CTR 5, V(1)=4627507[5]2838508, V(2)=0, repcount=2313753[5]6419255, factor=3/2
5553009[6]4061794 2890866[24]3863418 -694126[6]9257686 1 <B 46941261[5]9257766 5 3 1
== Executing PPA-CTR 6 (once), V(1)=6941261[5]9257765
5553009[6]4061802 2890866[24]2378957 -694126[6]9257687 1 <B 4 56941261[5]9257768 1
== Executing PA-CTR 1, V(1)=6941261[5]9257765, V(2)=0, repcount=3470630[5]9628883, factor=3/2
8329513[6]1092866 6504450[24]3635322 -104118[7]8886570 1 <B 41041189[6]8886650 52 1
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=1041189[6]8886649
8329513[6]1092883 6504450[24]9181942 -104118[7]8886572 1 <B 4 51041189[6]8886653 3 1
== Executing PA-CTR 5, V(1)=1041189[6]8886650, V(2)=0, repcount=5205946[5]9443326, factor=3/2
1249427[7]6639491 1463501[25]3668726 -156178[7]8329898 1 <B 41561783[6]8329979 5 3 1
== Executing PPA-CTR 6 (once), V(1)=1561783[6]8329978
1249427[7]6639499 1463501[25]0328691 -156178[7]8329899 1 <B 4 51561783[6]8329981 1
== Executing PA-CTR 1, V(1)=1561783[6]8329978, V(2)=0, repcount=7808919[5]9164990, factor=3/2
1874140[7]9959419 3292877[25]0418931 -234267[7]7494889 1 <B 42342675[6]7494971 5 1
== Executing PPA-CTR 8 (once), V(1)=2342675[6]7494969
1874140[7]9959435 3292877[25]5408888 -234267[7]7494890 1 <B 4 52342675[6]7494972 1 4 1
== Executing PA-CTR 2, V(1)=2342675[6]7494969, V(2)=0, repcount=1171337[6]8747485, factor=3/2
2811210[7]9939315 7408975[25]9369473 -351401[7]6242375 1 <B 43514013[6]6242456 52 1 4 1
== Executing PPA-CTR 9 (once), V(1)=0, V(2)=0, V(3)=0, V(4)=3514013[6]6242455
2811210[7]9939336 7408975[25]4339321 -351401[7]6242377 1 <B 4 53514013[6]6242459 3 5 3 1
== Executing PA-CTR 4, V(1)=3514013[6]6242456, V(2)=0, repcount=1757006[6]3121229, factor=3/2
4216816[7]4909168 1667019[26]4478018 -527102[7]9363606 1 <B 45271020[6]9363688 5 3 5 3 1
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=5271020[6]9363687
4216816[7]4909176 1667019[26]3205401 -527102[7]9363607 1 <B 4 55271020[6]9363691 3 1
== Executing PA-CTR 5, V(1)=5271020[6]9363688, V(2)=0, repcount=2635510[6]4681845, factor=3/2
6325224[7]2363936 3750793[26]9108546 -790653[7]4045452 1 <B 47906530[6]4045536 5 3 1
== Executing PPA-CTR 6 (once), V(1)=7906530[6]4045535
6325224[7]2363944 3750793[26]7199625 -790653[7]4045453 1 <B 4 57906530[6]4045538 1
== Executing PA-CTR 1, V(1)=7906530[6]4045535, V(2)=0, repcount=3953265[6]2022768, factor=3/2
9487836[7]8546088 8439285[26]0481705 -118597[8]6068221 1 <B 41185979[7]6068305 52 1
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=1185979[7]6068304
9487836[7]8546105 8439285[26]4754945 -118597[8]6068223 1 <B 4 51185979[7]6068308 3 1
== Executing PA-CTR 5, V(1)=1185979[7]6068305, V(2)=0, repcount=5929898[6]3034153, factor=3/2
1423175[8]2819329 1898839[27]6242090 -177896[8]9102376 1 <B 41778969[7]9102460 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=1778969[7]9102459
1423175[8]2819353 1898839[27]0856885 -177896[8]9102379 1 <B 4 51778969[7]9102465 3 1
== Executing PA-CTR 5, V(1)=1778969[7]9102462, V(2)=0, repcount=8894847[6]9551232, factor=3/2
2134763[8]9229209 4272388[27]6317749 -266845[8]8653611 1 <B 42668454[7]8653697 5 3 1
== Executing PPA-CTR 6 (once), V(1)=2668454[7]8653696
2134763[8]9229217 4272388[27]3625150 -266845[8]8653612 1 <B 4 52668454[7]8653699 1
== Executing PA-CTR 1, V(1)=2668454[7]8653696, V(2)=0, repcount=1334227[7]9326849, factor=3/2
3202144[8]3844009 9612873[27]6392647 -400268[8]7980461 1 <B 44002681[7]7980548 5 1
== Executing PPA-CTR 8 (once), V(1)=4002681[7]7980546
3202144[8]3844025 9612873[27]2353758 -400268[8]7980462 1 <B 4 54002681[7]7980549 1 4 1
== Executing PA-CTR 2, V(1)=4002681[7]7980546, V(2)=0, repcount=2001340[7]8990274, factor=3/2
4803217[8]5766217 2162896[28]6080630 -600402[8]6970736 1 <B 46004021[7]6970823 5 1 4 1
== Executing PPA-CTR 3 (once), V(1)=6004021[7]6970821
4803217[8]5766239 2162896[28]0022297 -600402[8]6970737 1 <B 4 56004021[7]6970824 1 42 1
== Executing PA-CTR 2, V(1)=6004021[7]6970821, V(2)=0, repcount=3002010[7]8485411, factor=3/2
7204826[8]3649527 4866517[28]0451526 -900603[8]5456148 1 <B 49006032[7]5456234 52 1 42 1
== Executing PPA-CTR 9 (once), V(1)=0, V(2)=1, V(3)=0, V(4)=9006032[7]5456233
7204826[8]3649548 4866517[28]2276488 -900603[8]5456150 1 <B 4 59006032[7]5456237 3 52 3 1
== Executing PA-CTR 4, V(1)=9006032[7]5456234, V(2)=0, repcount=4503016[7]2728118, factor=3/2
1080723[9]5474492 1094966[29]2110968 -135090[9]8184268 1 <B 41350904[8]8184355 5 3 52 3 1
== Executing PPA-CTR 10 (once), V(1)=1, V(2)=1350904[8]8184354
1080723[9]5474500 1094966[29]8479685 -135090[9]8184269 1 <B 4 51350904[8]8184359 3 1
== Executing PA-CTR 5, V(1)=1350904[8]8184356, V(2)=0, repcount=6754524[7]9092179, factor=3/2
1621085[9]8211932 2463674[29]9936882 -202635[9]7276448 1 <B 42026357[8]7276538 5 3 1
== Executing PPA-CTR 6 (once), V(1)=2026357[8]7276537
1621085[9]8211940 2463674[29]4489965 -202635[9]7276449 1 <B 4 52026357[8]7276540 1
== Executing PA-CTR 1, V(1)=2026357[8]7276537, V(2)=0, repcount=1013178[8]8638269, factor=3/2
2431628[9]7318092 5543267[29]0268662 -303953[9]5914718 1 <B 43039536[8]5914808 52 1
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=3039536[8]5914807
2431628[9]7318109 5543267[29]3927914 -303953[9]5914720 1 <B 4 53039536[8]5914811 3 1
== Executing PA-CTR 5, V(1)=3039536[8]5914808, V(2)=0, repcount=1519768[8]7957405, factor=3/2
3647443[9]0977349 1247235[30]4674419 -455930[9]3872125 1 <B 44559304[8]3872216 5 3 1
== Executing PPA-CTR 6 (once), V(1)=4559304[8]3872215
3647443[9]0977357 1247235[30]2418858 -455930[9]3872126 1 <B 4 54559304[8]3872218 1
== Executing PA-CTR 1, V(1)=4559304[8]3872215, V(2)=0, repcount=2279652[8]6936108, factor=3/2
5471164[9]6466221 2806279[30]6598498 -683895[9]0808234 1 <B 46838956[8]0808325 52 1
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=6838956[8]0808324
5471164[9]6466238 2806279[30]9831818 -683895[9]0808236 1 <B 4 56838956[8]0808328 3 1
== Executing PA-CTR 5, V(1)=6838956[8]0808325, V(2)=0, repcount=3419478[8]5404163, factor=3/2
8206747[9]9699542 6314128[30]5448503 -102584[10]6212399 1 <B 41025843[9]6212490 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=1025843[9]6212489
8206747[9]9699566 6314128[30]2723478 -102584[10]6212402 1 <B 4 51025843[9]6212495 3 1
== Executing PA-CTR 5, V(1)=1025843[9]6212492, V(2)=0, repcount=5129217[8]8106247, factor=3/2
1231012[10]4549542 1420678[31]2635987 -153876[10]4318649 1 <B 41538765[9]4318742 5 3 1
== Executing PPA-CTR 6 (once), V(1)=1538765[9]4318741
1231012[10]4549550 1420678[31]1273478 -153876[10]4318650 1 <B 4 51538765[9]4318744 1
== Executing PA-CTR 1, V(1)=1538765[9]4318741, V(2)=0, repcount=7693825[8]2159371, factor=3/2
1846518[10]1824518 3196527[31]3576627 -230814[10]6478021 1 <B 42308147[9]6478114 52 1
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=2308147[9]6478113
1846518[10]1824535 3196527[31]9489103 -230814[10]6478023 1 <B 4 52308147[9]6478117 3 1
== Executing PA-CTR 5, V(1)=2308147[9]6478114, V(2)=0, repcount=1154073[9]8239058, factor=3/2
2769777[10]7736999 7192186[31]9105543 -346222[10]4717081 1 <B 43462221[9]4717175 5 3 1
== Executing PPA-CTR 6 (once), V(1)=3462221[9]4717174
2769777[10]7737007 7192186[31]8539900 -346222[10]4717082 1 <B 4 53462221[9]4717177 1
== Executing PA-CTR 1, V(1)=3462221[9]4717174, V(2)=0, repcount=1731110[9]7358588, factor=3/2
4154665[10]6605711 1618241[32]4752660 -519333[10]2075670 1 <B 45193332[9]2075765 5 1
== Executing PPA-CTR 8 (once), V(1)=5193332[9]2075763
4154665[10]6605727 1618241[32]8904205 -519333[10]2075671 1 <B 4 55193332[9]2075766 1 4 1
== Executing PA-CTR 2, V(1)=5193332[9]2075763, V(2)=0, repcount=2596666[9]6037882, factor=3/2
6231998[10]4908783 3641044[32]2269269 -778999[10]8113553 1 <B 47789998[9]8113647 52 1 4 1
== Executing PPA-CTR 9 (once), V(1)=0, V(2)=0, V(3)=0, V(4)=7789998[9]8113646
6231998[10]4908804 3641044[32]4723881 -778999[10]8113555 1 <B 4 57789998[9]8113650 3 5 3 1
== Executing PA-CTR 4, V(1)=7789998[9]8113647, V(2)=0, repcount=3894999[9]4056824, factor=3/2
9347997[10]7363396 8192349[32]1965753 -116849[11]2170379 1 <B 41168499[10]2170473 52 3 5 3 1
== Executing PPA-CTR 13 (once), V(1)=1168499[10]2170472
9347997[10]7363419 8192349[32]4988626 -116849[11]2170382 1 <B 4 51168499[10]2170480 1
== Executing PA-CTR 1, V(1)=1168499[10]2170477, V(2)=0, repcount=5842498[9]1085239, factor=3/2
1402199[11]6045331 1843278[33]2561423 -175274[11]3255621 1 <B 41752749[10]3255718 52 1
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=1752749[10]3255717
1402199[11]6045348 1843278[33]5584315 -175274[11]3255623 1 <B 4 51752749[10]3255721 3 1
== Executing PA-CTR 5, V(1)=1752749[10]3255718, V(2)=0, repcount=8763748[9]6627860, factor=3/2
2103299[11]9068228 4147377[33]9890275 -262912[11]9883483 1 <B 42629124[10]9883581 5 3 1
== Executing PPA-CTR 6 (once), V(1)=2629124[10]9883580
2103299[11]9068236 4147377[33]9657444 -262912[11]9883484 1 <B 4 52629124[10]9883583 1
== Executing PA-CTR 1, V(1)=2629124[10]9883580, V(2)=0, repcount=1314562[10]4941791, factor=3/2
3154949[11]8602564 9331598[33]4171233 -394368[11]4825275 1 <B 43943686[10]4825374 5 1
== Executing PPA-CTR 8 (once), V(1)=3943686[10]4825372
3154949[11]8602580 9331598[33]3821996 -394368[11]4825276 1 <B 4 53943686[10]4825375 1 4 1
== Executing PA-CTR 2, V(1)=3943686[10]4825372, V(2)=0, repcount=1971843[10]7412687, factor=3/2
4732423[11]7904076 2099609[34]3978025 -591552[11]2237963 1 <B 45915529[10]2238062 5 1 4 1
== Executing PPA-CTR 3 (once), V(1)=5915529[10]2238060
4732423[11]7904098 2099609[34]8454170 -591552[11]2237964 1 <B 4 55915529[10]2238063 1 42 1
== Executing PA-CTR 2, V(1)=5915529[10]2238060, V(2)=0, repcount=2957764[10]1119031, factor=3/2
7098635[11]6856346 4724121[34]6305239 -887329[11]3356995 1 <B 48873294[10]3357094 5 1 42 1
== Executing PPA-CTR 14 (once), V(1)=8873294[10]3357092
7098635[11]6856368 4724121[34]3019452 -887329[11]3356996 1 <B 4 58873294[10]3357095 3 43 1
== Executing PA-CTR 2, V(1)=8873294[10]3357092, V(2)=0, repcount=4436647[10]1678547, factor=3/2
1064795[12]0284744 1062927[35]3184361 -133099[12]5035543 1 <B 41330994[11]5035642 5 3 43 1
== Executing PPA-CTR 15 (once), V(1)=1330994[11]5035641
1064795[12]0284752 1062927[35]3255652 -133099[12]5035544 1 <B 4 51330994[11]5035644 43 1
== Executing PA-CTR 5, V(1)=1330994[11]5035641, V(2)=0, repcount=6654971[10]7517821, factor=3/2
1597193[12]0427320 2391586[35]6126701 -199649[12]2553365 1 <B 41996491[11]2553464 52 43 1
== Executing PPA-CTR 16 (once), V(1)=0, V(2)=2, V(3)=1996491[11]2553463
1597193[12]0427337 2391586[35]6340583 -199649[12]2553367 1 <B 4 51996491[11]2553470 3 1
== Executing PA-CTR 5, V(1)=1996491[11]2553467, V(2)=0, repcount=9982456[10]6276734, factor=3/2
2395789[12]0641209 5381069[35]3121255 -299473[12]8830101 1 <B 42994737[11]8830203 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=2994737[11]8830202
2395789[12]0641233 5381069[35]6102508 -299473[12]8830104 1 <B 4 52994737[11]8830208 3 1
== Executing PA-CTR 5, V(1)=2994737[11]8830205, V(2)=0, repcount=1497368[11]4415103, factor=3/2
3593684[12]5962057 1210740[36]6094953 -449210[12]3245207 1 <B 44492105[11]3245310 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=4492105[11]3245309
3593684[12]5962081 1210740[36]5566848 -449210[12]3245210 1 <B 4 54492105[11]3245315 3 1
== Executing PA-CTR 5, V(1)=4492105[11]3245312, V(2)=0, repcount=2246052[11]6622657, factor=3/2
5390526[12]8943337 2724166[36]2521737 -673815[12]9867867 1 <B 46738158[11]9867972 5 3 1
== Executing PPA-CTR 6 (once), V(1)=6738158[11]9867971
5390526[12]8943345 2724166[36]2257688 -673815[12]9867868 1 <B 4 56738158[11]9867974 1
== Executing PA-CTR 1, V(1)=6738158[11]9867971, V(2)=0, repcount=3369079[11]4933986, factor=3/2
8085790[12]8415233 6129375[36]5406192 -101072[13]4801854 1 <B 41010723[12]4801959 52 1
== Executing PPA-CTR 7 (once), V(1)=0, V(2)=1010723[12]4801958
8085790[12]8415250 6129375[36]4614048 -101072[13]4801856 1 <B 4 51010723[12]4801962 3 1
== Executing PA-CTR 5, V(1)=1010723[12]4801959, V(2)=0, repcount=5053618[11]2400980, factor=3/2
1212868[13]7623090 1379109[37]3901128 -151608[13]7202836 1 <B 41516085[12]7202941 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=1516085[12]7202940
1212868[13]7623114 1379109[37]7118809 -151608[13]7202839 1 <B 4 51516085[12]7202946 3 1
== Executing PA-CTR 5, V(1)=1516085[12]7202943, V(2)=0, repcount=7580428[11]8601472, factor=3/2
1819302[13]6434890 3102996[37]0427993 -227412[13]5804311 1 <B 42274128[12]5804417 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=2274128[12]5804416
1819302[13]6434914 3102996[37]5254530 -227412[13]5804314 1 <B 4 52274128[12]5804422 3 1
== Executing PA-CTR 5, V(1)=2274128[12]5804419, V(2)=0, repcount=1137064[12]7902210, factor=3/2
2728954[13]9652594 6981741[37]1320090 -341119[13]3706524 1 <B 43411192[12]3706631 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=3411192[12]3706630
2728954[13]9652618 6981741[37]3559911 -341119[13]3706527 1 <B 4 53411192[12]3706636 3 1
== Executing PA-CTR 5, V(1)=3411192[12]3706633, V(2)=0, repcount=1705596[12]1853317, factor=3/2
4093431[13]4479154 1570891[38]6387280 -511678[13]5559844 1 <B 45116789[12]5559952 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=5116789[12]5559951
4093431[13]4479178 1570891[38]9747027 -511678[13]5559847 1 <B 4 55116789[12]5559957 3 1
== Executing PA-CTR 5, V(1)=5116789[12]5559954, V(2)=0, repcount=2558394[12]2779978, factor=3/2
6140146[13]6719002 3534506[38]9468347 -767518[13]8339825 1 <B 47675183[12]8339935 5 3 1
== Executing PPA-CTR 6 (once), V(1)=7675183[12]8339934
6140146[13]6719010 3534506[38]6148224 -767518[13]8339826 1 <B 4 57675183[12]8339937 1
== Executing PA-CTR 1, V(1)=7675183[12]8339934, V(2)=0, repcount=3837591[12]9169968, factor=3/2
9210220[13]0078754 7952639[38]0531104 -115127[14]7509794 1 <B 41151277[13]7509905 5 1
== Executing PPA-CTR 8 (once), V(1)=1151277[13]7509903
9210220[13]0078770 7952639[38]5550929 -115127[14]7509795 1 <B 4 51151277[13]7509906 1 4 1
== Executing PA-CTR 2, V(1)=1151277[13]7509903, V(2)=0, repcount=5756387[12]8754952, factor=3/2
1381533[14]0118386 1789343[39]1647553 -172691[14]6264747 1 <B 41726916[13]6264857 52 1 4 1
== Executing PPA-CTR 9 (once), V(1)=0, V(2)=0, V(3)=0, V(4)=1726916[13]6264856
1381533[14]0118407 1789343[39]6707005 -172691[14]6264749 1 <B 4 51726916[13]6264860 3 5 3 1
== Executing PA-CTR 4, V(1)=1726916[13]6264857, V(2)=0, repcount=8634581[12]8132429, factor=3/2
2072299[14]5177839 4026023[39]9821702 -259037[14]4397178 1 <B 42590374[13]4397288 52 3 5 3 1
== Executing PPA-CTR 13 (once), V(1)=2590374[13]4397287
2072299[14]5177862 4026023[39]6205465 -259037[14]4397181 1 <B 4 52590374[13]4397295 1
== Executing PA-CTR 1, V(1)=2590374[13]4397292, V(2)=0, repcount=1295187[13]2198647, factor=3/2
3108449[14]2767038 9058553[39]5289174 -388556[14]6595828 1 <B 43885561[13]6595942 5 1
== Executing PPA-CTR 8 (once), V(1)=3885561[13]6595940
3108449[14]2767054 9058553[39]8481073 -388556[14]6595829 1 <B 4 53885561[13]6595943 1 4 1
== Executing PA-CTR 2, V(1)=3885561[13]6595940, V(2)=0, repcount=1942780[13]3297971, factor=3/2
4662673[14]9150822 2038174[40]6419422 -582834[14]9893800 1 <B 45828342[13]9893914 5 1 4 1
== Executing PPA-CTR 3 (once), V(1)=5828342[13]9893912
4662673[14]9150844 2038174[40]6207271 -582834[14]9893801 1 <B 4 55828342[13]9893915 1 42 1
== Executing PA-CTR 2, V(1)=5828342[13]9893912, V(2)=0, repcount=2914171[13]9946957, factor=3/2
6994010[14]8726500 4585892[40]6568560 -874251[14]9840758 1 <B 48742513[13]9840872 5 1 42 1
== Executing PPA-CTR 14 (once), V(1)=8742513[13]9840870
6994010[14]8726522 4585892[40]6250329 -874251[14]9840759 1 <B 4 58742513[13]9840873 3 43 1
== Executing PA-CTR 2, V(1)=8742513[13]9840870, V(2)=0, repcount=4371256[13]9920436, factor=3/2
1049101[15]8090010 1031825[41]7063233 -131137[15]9761195 1 <B 41311377[14]9761309 5 3 43 1
== Executing PPA-CTR 15 (once), V(1)=1311377[14]9761308
1049101[15]8090018 1031825[41]6585858 -131137[15]9761196 1 <B 4 51311377[14]9761311 43 1
== Executing PA-CTR 5, V(1)=1311377[14]9761308, V(2)=0, repcount=6556885[13]4880655, factor=3/2
1573652[15]7135258 2321608[41]5556863 -196706[15]4641851 1 <B 41967065[14]4641966 5 43 1
1573652[15]7135259 2321608[41]5556864 -196706[15]4641850 2 B> 41967065[14]4641966 5 43 1
1573652[15]7135260 2321608[41]0198830 116 2 31967065[14]4641966 B> 5 43 1
1573652[15]7135261 2321608[41]0198831 117 2 31967065[14]4641967 A> 43 1
1573652[15]7135262 2321608[41]0198832 118 2 31967065[14]4641967 1 H> 42 1
1573652[15]7135262 2321608[41]0198832 118 2 31967065[14]4641967 1 H> 42 1 [stop]
Lines: 641
Top steps: 639
Macro steps: 15736524687484606059477135262
Basic steps: 2321608211623241985057171728803384730914423909950198832
Tape index: 118
nonzeros: 1967065585935575757434641972
log10(nonzeros): 27.294
log10(steps ): 54.366
Run state: stop
Some long numbers above are shortened: #(omitted digits) shown in "[]".
Input to awk program:
gohalt 1
nbs 6
T 2-state 6-symbol #d (T.J. & S. Ligocki)
: >1.9x10^27 >2.3x10^54
5T 1RB 0RB 3LA 5LA 1RH 4LB 1LA 2RB 3LA 4LB 3RB 3RA
L 22
M 650
pref sim
machv Lig26_d just simple
machv Lig26_d-r with repetitions reduced
machv Lig26_d-1 with tape symbol exponents
machv Lig26_d-m as 1-macro machine
machv Lig26_d-a as 1-macro machine with pure additive config-TRs
iam Lig26_d-a
mtype 1
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:13:16 CEST 2010
edate Tue Jul 6 22:13:19 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:16 CEST 2010