Comment: This TM produces >9.3x10^30 nonzeros in >5.2x10^61 steps.
| State | on 0 |
on 1 |
on 2 |
on 3 |
on 4 |
on 0 | on 1 | on 2 | on 3 | on 4 | ||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Move | Goto | Move | Goto | Move | Goto | Move | Goto | Move | Goto | |||||||||||
| A | 1RB | 2LA | 4RA | 1LB | 2LA | 1 | right | B | 2 | left | A | 4 | right | A | 1 | left | B | 2 | left | A |
| B | 0LA | 2RB | 3RB | 2RA | 1RH | 0 | left | A | 2 | right | B | 3 | right | B | 2 | right | A | 1 | right | H |
The same TM just simple.
The same TM with repetitions reduced.
The same TM with tape symbol exponents.
The same TM as 1-bck-macro machine.
Simulation is done as 1-bck-macro machine with pure additive config-TRs.
Pushing initial machine.
Pushing macro factor 1.
Pushing BCK machine.
Steps BasSteps BasTpos Tape contents
0 0 0 (0)A>
1 1 1 (1)B>
2 3 -1 <A(2)
3 5 1 1 (3)B>
4 7 -1 1 <B(1)
5 9 1 2 (2)B>
6 12 2 2 4 (1)B>
7 14 0 2 4 <A(2)
8 15 -1 2 <A(2) 2
9 17 1 4 (4)A> 2
10 18 2 42 (4)A>
11 19 3 43 (1)B>
12 21 1 43 <A(2)
13 24 -2 <A(2) 23
14 26 0 1 (3)B> 23
15 29 3 1 33 (3)B>
16 31 1 1 33 <B(1)
17 35 3 1 32 4 (4)A>
18 36 4 1 32 42 (1)B>
19 38 2 1 32 42 <A(2)
20 40 0 1 32 <A(2) 22
21 41 -1 1 3 <B(1) 23
22 45 1 1 4 (4)A> 23
23 48 4 1 44 (4)A>
24 49 5 1 45 (1)B>
25 51 3 1 45 <A(2)
26 56 -2 1 <A(2) 25
27 57 -3 <A(2) 26
28 59 -1 1 (3)B> 26
29 65 5 1 36 (3)B>
30 67 3 1 36 <B(1)
31 71 5 1 35 4 (4)A>
32 72 6 1 35 42 (1)B>
33 74 4 1 35 42 <A(2)
34 76 2 1 35 <A(2) 22
35 77 1 1 34 <B(1) 23
36 81 3 1 33 4 (4)A> 23
37 84 6 1 33 44 (4)A>
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* 33+V(2) 41+V(1) (4)A>
1 1 1 [*]* 33+V(2) 42+V(1) (1)B>
2 3 -1 [*]* 33+V(2) 42+V(1) <A(2)
3 5+V(1) -3+-1*V(1) [*]* 33+V(2) <A(2) 22+V(1)
4 6+V(1) -4+-1*V(1) [*]* 32+V(2) <B(1) 23+V(1)
5 10+V(1) -2+-1*V(1) [*]* 31+V(2) 4 (4)A> 23+V(1)
6 13+2*V(1) 1 [*]* 31+V(2) 44+V(1) (4)A>
<< Success! ==> defined new CTR 1 (PA)
37 84 6 1 33 44 (4)A>
== Executing PA-CTR 1, V(1)=3, V(2)=0, repcount=1, factor=3/2
43 103 7 1 3 47 (4)A>
44 104 8 1 3 48 (1)B>
45 106 6 1 3 48 <A(2)
46 114 -2 1 3 <A(2) 28
47 115 -3 1 <B(1) 29
48 117 -1 2 (2)B> 29
49 118 0 22 (3)B> 28
50 126 8 22 38 (3)B>
51 128 6 22 38 <B(1)
52 132 8 22 37 4 (4)A>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 1 3 43+V(1) (4)A>
1 1 1 1 3 44+V(1) (1)B>
2 3 -1 1 3 44+V(1) <A(2)
3 7+V(1) -5+-1*V(1) 1 3 <A(2) 24+V(1)
4 8+V(1) -6+-1*V(1) 1 <B(1) 25+V(1)
5 10+V(1) -4+-1*V(1) 2 (2)B> 25+V(1)
6 11+V(1) -3+-1*V(1) 22 (3)B> 24+V(1)
7 15+2*V(1) 1 22 34+V(1) (3)B>
8 17+2*V(1) -1 22 34+V(1) <B(1)
9 21+2*V(1) 1 22 33+V(1) 4 (4)A>
<< Success! ==> defined new CTR 2 (PPA)
52 132 8 22 37 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=4, repcount=3, factor=3/2
70 189 11 22 3 410 (4)A>
71 190 12 22 3 411 (1)B>
72 192 10 22 3 411 <A(2)
73 203 -1 22 3 <A(2) 211
74 204 -2 22 <B(1) 212
75 206 0 2 3 (2)B> 212
76 207 1 2 3 2 (3)B> 211
77 218 12 2 3 2 311 (3)B>
78 220 10 2 3 2 311 <B(1)
79 224 12 2 3 2 310 4 (4)A>
80 225 13 2 3 2 310 42 (1)B>
81 227 11 2 3 2 310 42 <A(2)
82 229 9 2 3 2 310 <A(2) 22
83 230 8 2 3 2 39 <B(1) 23
84 234 10 2 3 2 38 4 (4)A> 23
85 237 13 2 3 2 38 44 (4)A>
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* 33+V(2) 41+V(1) (4)A>
1 1 1 [*]* [*]* [*]* 33+V(2) 42+V(1) (1)B>
2 3 -1 [*]* [*]* [*]* 33+V(2) 42+V(1) <A(2)
3 5+V(1) -3+-1*V(1) [*]* [*]* [*]* 33+V(2) <A(2) 22+V(1)
4 6+V(1) -4+-1*V(1) [*]* [*]* [*]* 32+V(2) <B(1) 23+V(1)
5 10+V(1) -2+-1*V(1) [*]* [*]* [*]* 31+V(2) 4 (4)A> 23+V(1)
6 13+2*V(1) 1 [*]* [*]* [*]* 31+V(2) 44+V(1) (4)A>
<< Success! ==> defined new CTR 3 (PA)
85 237 13 2 3 2 38 44 (4)A>
== Executing PA-CTR 3, V(1)=3, V(2)=5, repcount=3, factor=3/2
103 312 16 2 3 2 32 413 (4)A>
104 313 17 2 3 2 32 414 (1)B>
105 315 15 2 3 2 32 414 <A(2)
106 329 1 2 3 2 32 <A(2) 214
107 330 0 2 3 2 3 <B(1) 215
108 334 2 2 3 2 4 (4)A> 215
109 349 17 2 3 2 416 (4)A>
110 350 18 2 3 2 417 (1)B>
111 352 16 2 3 2 417 <A(2)
112 369 -1 2 3 2 <A(2) 217
113 371 1 2 3 4 (4)A> 217
114 388 18 2 3 418 (4)A>
115 389 19 2 3 419 (1)B>
116 391 17 2 3 419 <A(2)
117 410 -2 2 3 <A(2) 219
118 411 -3 2 <B(1) 220
119 413 -1 3 (2)B> 220
120 414 0 3 2 (3)B> 219
121 433 19 3 2 319 (3)B>
122 435 17 3 2 319 <B(1)
123 439 19 3 2 318 4 (4)A>
124 440 20 3 2 318 42 (1)B>
125 442 18 3 2 318 42 <A(2)
126 444 16 3 2 318 <A(2) 22
127 445 15 3 2 317 <B(1) 23
128 449 17 3 2 316 4 (4)A> 23
129 452 20 3 2 316 44 (4)A>
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* 33+V(2) 41+V(1) (4)A>
1 1 1 [*]* [*]* 33+V(2) 42+V(1) (1)B>
2 3 -1 [*]* [*]* 33+V(2) 42+V(1) <A(2)
3 5+V(1) -3+-1*V(1) [*]* [*]* 33+V(2) <A(2) 22+V(1)
4 6+V(1) -4+-1*V(1) [*]* [*]* 32+V(2) <B(1) 23+V(1)
5 10+V(1) -2+-1*V(1) [*]* [*]* 31+V(2) 4 (4)A> 23+V(1)
6 13+2*V(1) 1 [*]* [*]* 31+V(2) 44+V(1) (4)A>
<< Success! ==> defined new CTR 4 (PA)
129 452 20 3 2 316 44 (4)A>
== Executing PA-CTR 4, V(1)=3, V(2)=13, repcount=7, factor=3/2
171 711 27 3 2 32 425 (4)A>
172 712 28 3 2 32 426 (1)B>
173 714 26 3 2 32 426 <A(2)
174 740 0 3 2 32 <A(2) 226
175 741 -1 3 2 3 <B(1) 227
176 745 1 3 2 4 (4)A> 227
177 772 28 3 2 428 (4)A>
178 773 29 3 2 429 (1)B>
179 775 27 3 2 429 <A(2)
180 804 -2 3 2 <A(2) 229
181 806 0 3 4 (4)A> 229
182 835 29 3 430 (4)A>
183 836 30 3 431 (1)B>
184 838 28 3 431 <A(2)
185 869 -3 3 <A(2) 231
186 870 -4 <B(1) 232
187 871 -5 <A(0) 1 232
188 874 -6 <A(2) 0 1 232
189 876 -4 1 (3)B> 0 1 232
190 878 -6 1 <B(1) 0 1 232
191 880 -4 2 (2)B> 0 1 232
192 883 -3 2 4 (1)B> 1 232
193 884 -2 2 4 1 (2)B> 232
194 885 -1 2 4 1 2 (3)B> 231
195 916 30 2 4 1 2 331 (3)B>
196 918 28 2 4 1 2 331 <B(1)
197 922 30 2 4 1 2 330 4 (4)A>
198 923 31 2 4 1 2 330 42 (1)B>
199 925 29 2 4 1 2 330 42 <A(2)
200 927 27 2 4 1 2 330 <A(2) 22
201 928 26 2 4 1 2 329 <B(1) 23
202 932 28 2 4 1 2 328 4 (4)A> 23
203 935 31 2 4 1 2 328 44 (4)A>
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* [*]* 33+V(2) 41+V(1) (4)A>
1 1 1 [*]* [*]* [*]* [*]* 33+V(2) 42+V(1) (1)B>
2 3 -1 [*]* [*]* [*]* [*]* 33+V(2) 42+V(1) <A(2)
3 5+V(1) -3+-1*V(1) [*]* [*]* [*]* [*]* 33+V(2) <A(2) 22+V(1)
4 6+V(1) -4+-1*V(1) [*]* [*]* [*]* [*]* 32+V(2) <B(1) 23+V(1)
5 10+V(1) -2+-1*V(1) [*]* [*]* [*]* [*]* 31+V(2) 4 (4)A> 23+V(1)
6 13+2*V(1) 1 [*]* [*]* [*]* [*]* 31+V(2) 44+V(1) (4)A>
<< Success! ==> defined new CTR 5 (PA)
203 935 31 2 4 1 2 328 44 (4)A>
== Executing PA-CTR 5, V(1)=3, V(2)=25, repcount=13, factor=3/2
281 1650 44 2 4 1 2 32 443 (4)A>
282 1651 45 2 4 1 2 32 444 (1)B>
283 1653 43 2 4 1 2 32 444 <A(2)
284 1697 -1 2 4 1 2 32 <A(2) 244
285 1698 -2 2 4 1 2 3 <B(1) 245
286 1702 0 2 4 1 2 4 (4)A> 245
287 1747 45 2 4 1 2 446 (4)A>
288 1748 46 2 4 1 2 447 (1)B>
289 1750 44 2 4 1 2 447 <A(2)
290 1797 -3 2 4 1 2 <A(2) 247
291 1799 -1 2 4 1 4 (4)A> 247
292 1846 46 2 4 1 448 (4)A>
293 1847 47 2 4 1 449 (1)B>
294 1849 45 2 4 1 449 <A(2)
295 1898 -4 2 4 1 <A(2) 249
296 1899 -5 2 4 <A(2) 250
297 1900 -6 2 <A(2) 251
298 1902 -4 4 (4)A> 251
299 1953 47 452 (4)A>
300 1954 48 453 (1)B>
301 1956 46 453 <A(2)
302 2009 -7 <A(2) 253
303 2011 -5 1 (3)B> 253
304 2064 48 1 353 (3)B>
305 2066 46 1 353 <B(1)
306 2070 48 1 352 4 (4)A>
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 2 41+V(3) 11+V(2) 2 32 41+V(1) (4)A>
1 1 1 2 41+V(3) 11+V(2) 2 32 42+V(1) (1)B>
2 3 -1 2 41+V(3) 11+V(2) 2 32 42+V(1) <A(2)
3 5+V(1) -3+-1*V(1) 2 41+V(3) 11+V(2) 2 32 <A(2) 22+V(1)
4 6+V(1) -4+-1*V(1) 2 41+V(3) 11+V(2) 2 3 <B(1) 23+V(1)
5 10+V(1) -2+-1*V(1) 2 41+V(3) 11+V(2) 2 4 (4)A> 23+V(1)
6 13+2*V(1) 1 2 41+V(3) 11+V(2) 2 44+V(1) (4)A>
7 14+2*V(1) 2 2 41+V(3) 11+V(2) 2 45+V(1) (1)B>
8 16+2*V(1) 0 2 41+V(3) 11+V(2) 2 45+V(1) <A(2)
9 21+3*V(1) -5+-1*V(1) 2 41+V(3) 11+V(2) 2 <A(2) 25+V(1)
10 23+3*V(1) -3+-1*V(1) 2 41+V(3) 11+V(2) 4 (4)A> 25+V(1)
11 28+4*V(1) 2 2 41+V(3) 11+V(2) 46+V(1) (4)A>
12 29+4*V(1) 3 2 41+V(3) 11+V(2) 47+V(1) (1)B>
13 31+4*V(1) 1 2 41+V(3) 11+V(2) 47+V(1) <A(2)
14 38+5*V(1) -6+-1*V(1) 2 41+V(3) 11+V(2) <A(2) 27+V(1)
15 39+5*V(1)+V(2) -7+-1*V(1)+-1*V(2) 2 41+V(3) <A(2) 28+V(1)+V(2)
16 40+5*V(1)+V(2)+V(3) -8+-1*V(1)+-1*V(2)+-1*V(3) 2 <A(2) 29+V(1)+V(2)+V(3)
17 42+5*V(1)+V(2)+V(3) -6+-1*V(1)+-1*V(2)+-1*V(3) 4 (4)A> 29+V(1)+V(2)+V(3)
18 51+6*V(1)+2*V(2)+2*V(3) 3 410+V(1)+V(2)+V(3) (4)A>
19 52+6*V(1)+2*V(2)+2*V(3) 4 411+V(1)+V(2)+V(3) (1)B>
20 54+6*V(1)+2*V(2)+2*V(3) 2 411+V(1)+V(2)+V(3) <A(2)
21 65+7*V(1)+3*V(2)+3*V(3) -9+-1*V(1)+-1*V(2)+-1*V(3) <A(2) 211+V(1)+V(2)+V(3)
22 67+7*V(1)+3*V(2)+3*V(3) -7+-1*V(1)+-1*V(2)+-1*V(3) 1 (3)B> 211+V(1)+V(2)+V(3)
23 78+8*V(1)+4*V(2)+4*V(3) 4 1 311+V(1)+V(2)+V(3) (3)B>
24 80+8*V(1)+4*V(2)+4*V(3) 2 1 311+V(1)+V(2)+V(3) <B(1)
25 84+8*V(1)+4*V(2)+4*V(3) 4 1 310+V(1)+V(2)+V(3) 4 (4)A>
<< Success! ==> defined new CTR 6 (PPA)
306 2070 48 1 352 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=49, repcount=25, factor=3/2
456 4195 73 1 32 476 (4)A>
457 4196 74 1 32 477 (1)B>
458 4198 72 1 32 477 <A(2)
459 4275 -5 1 32 <A(2) 277
460 4276 -6 1 3 <B(1) 278
461 4280 -4 1 4 (4)A> 278
462 4358 74 1 479 (4)A>
463 4359 75 1 480 (1)B>
464 4361 73 1 480 <A(2)
465 4441 -7 1 <A(2) 280
466 4442 -8 <A(2) 281
467 4444 -6 1 (3)B> 281
468 4525 75 1 381 (3)B>
469 4527 73 1 381 <B(1)
470 4531 75 1 380 4 (4)A>
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 11+V(2) 32 41+V(1) (4)A>
1 1 1 11+V(2) 32 42+V(1) (1)B>
2 3 -1 11+V(2) 32 42+V(1) <A(2)
3 5+V(1) -3+-1*V(1) 11+V(2) 32 <A(2) 22+V(1)
4 6+V(1) -4+-1*V(1) 11+V(2) 3 <B(1) 23+V(1)
5 10+V(1) -2+-1*V(1) 11+V(2) 4 (4)A> 23+V(1)
6 13+2*V(1) 1 11+V(2) 44+V(1) (4)A>
7 14+2*V(1) 2 11+V(2) 45+V(1) (1)B>
8 16+2*V(1) 0 11+V(2) 45+V(1) <A(2)
9 21+3*V(1) -5+-1*V(1) 11+V(2) <A(2) 25+V(1)
10 22+3*V(1)+V(2) -6+-1*V(1)+-1*V(2) <A(2) 26+V(1)+V(2)
11 24+3*V(1)+V(2) -4+-1*V(1)+-1*V(2) 1 (3)B> 26+V(1)+V(2)
12 30+4*V(1)+2*V(2) 2 1 36+V(1)+V(2) (3)B>
13 32+4*V(1)+2*V(2) 0 1 36+V(1)+V(2) <B(1)
14 36+4*V(1)+2*V(2) 2 1 35+V(1)+V(2) 4 (4)A>
<< Success! ==> defined new CTR 7 (PPA)
470 4531 75 1 380 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=77, repcount=39, factor=3/2
704 9484 114 1 32 4118 (4)A>
== Executing PPA-CTR 7 (once), V(1)=117, V(2)=0
718 9988 116 1 3122 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=119, repcount=60, factor=3/2
1078 21388 176 1 32 4181 (4)A>
== Executing PPA-CTR 7 (once), V(1)=180, V(2)=0
1092 22144 178 1 3185 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=182, repcount=92, factor=3/2
1644 48456 270 1 3 4277 (4)A>
== Executing PPA-CTR 2 (once), V(1)=274
1653 49025 271 22 3277 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=274, repcount=138, factor=3/2
2481 107537 409 22 3 4415 (4)A>
2482 107538 410 22 3 4416 (1)B>
2483 107540 408 22 3 4416 <A(2)
2484 107956 -8 22 3 <A(2) 2416
2485 107957 -9 22 <B(1) 2417
2486 107959 -7 2 3 (2)B> 2417
2487 107960 -6 2 3 2 (3)B> 2416
2488 108376 410 2 3 2 3416 (3)B>
2489 108378 408 2 3 2 3416 <B(1)
2490 108382 410 2 3 2 3415 4 (4)A>
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 22+V(2) 3 43+V(1) (4)A>
1 1 1 22+V(2) 3 44+V(1) (1)B>
2 3 -1 22+V(2) 3 44+V(1) <A(2)
3 7+V(1) -5+-1*V(1) 22+V(2) 3 <A(2) 24+V(1)
4 8+V(1) -6+-1*V(1) 22+V(2) <B(1) 25+V(1)
5 10+V(1) -4+-1*V(1) 21+V(2) 3 (2)B> 25+V(1)
6 11+V(1) -3+-1*V(1) 21+V(2) 3 2 (3)B> 24+V(1)
7 15+2*V(1) 1 21+V(2) 3 2 34+V(1) (3)B>
8 17+2*V(1) -1 21+V(2) 3 2 34+V(1) <B(1)
9 21+2*V(1) 1 21+V(2) 3 2 33+V(1) 4 (4)A>
<< Success! ==> defined new CTR 8 (PPA)
2490 108382 410 2 3 2 3415 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=412, repcount=207, factor=3/2
3732 238999 617 2 3 2 3 4622 (4)A>
3733 239000 618 2 3 2 3 4623 (1)B>
3734 239002 616 2 3 2 3 4623 <A(2)
3735 239625 -7 2 3 2 3 <A(2) 2623
3736 239626 -8 2 3 2 <B(1) 2624
3737 239628 -6 2 32 (2)B> 2624
3738 239629 -5 2 32 2 (3)B> 2623
3739 240252 618 2 32 2 3623 (3)B>
3740 240254 616 2 32 2 3623 <B(1)
3741 240258 618 2 32 2 3622 4 (4)A>
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 [*]* 31+V(2) 2 3 43+V(1) (4)A>
1 1 1 [*]* 31+V(2) 2 3 44+V(1) (1)B>
2 3 -1 [*]* 31+V(2) 2 3 44+V(1) <A(2)
3 7+V(1) -5+-1*V(1) [*]* 31+V(2) 2 3 <A(2) 24+V(1)
4 8+V(1) -6+-1*V(1) [*]* 31+V(2) 2 <B(1) 25+V(1)
5 10+V(1) -4+-1*V(1) [*]* 32+V(2) (2)B> 25+V(1)
6 11+V(1) -3+-1*V(1) [*]* 32+V(2) 2 (3)B> 24+V(1)
7 15+2*V(1) 1 [*]* 32+V(2) 2 34+V(1) (3)B>
8 17+2*V(1) -1 [*]* 32+V(2) 2 34+V(1) <B(1)
9 21+2*V(1) 1 [*]* 32+V(2) 2 33+V(1) 4 (4)A>
<< Success! ==> defined new CTR 9 (PPA)
3741 240258 618 2 32 2 3622 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=619, repcount=310, factor=3/2
5601 531658 928 2 32 2 32 4931 (4)A>
5602 531659 929 2 32 2 32 4932 (1)B>
5603 531661 927 2 32 2 32 4932 <A(2)
5604 532593 -5 2 32 2 32 <A(2) 2932
5605 532594 -6 2 32 2 3 <B(1) 2933
5606 532598 -4 2 32 2 4 (4)A> 2933
5607 533531 929 2 32 2 4934 (4)A>
5608 533532 930 2 32 2 4935 (1)B>
5609 533534 928 2 32 2 4935 <A(2)
5610 534469 -7 2 32 2 <A(2) 2935
5611 534471 -5 2 32 4 (4)A> 2935
5612 535406 930 2 32 4936 (4)A>
5613 535407 931 2 32 4937 (1)B>
5614 535409 929 2 32 4937 <A(2)
5615 536346 -8 2 32 <A(2) 2937
5616 536347 -9 2 3 <B(1) 2938
5617 536351 -7 2 4 (4)A> 2938
5618 537289 931 2 4939 (4)A>
5619 537290 932 2 4940 (1)B>
5620 537292 930 2 4940 <A(2)
5621 538232 -10 2 <A(2) 2940
5622 538234 -8 4 (4)A> 2940
5623 539174 932 4941 (4)A>
5624 539175 933 4942 (1)B>
5625 539177 931 4942 <A(2)
5626 540119 -11 <A(2) 2942
5627 540121 -9 1 (3)B> 2942
5628 541063 933 1 3942 (3)B>
5629 541065 931 1 3942 <B(1)
5630 541069 933 1 3941 4 (4)A>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 2 32 2 32 41+V(1) (4)A>
1 1 1 2 32 2 32 42+V(1) (1)B>
2 3 -1 2 32 2 32 42+V(1) <A(2)
3 5+V(1) -3+-1*V(1) 2 32 2 32 <A(2) 22+V(1)
4 6+V(1) -4+-1*V(1) 2 32 2 3 <B(1) 23+V(1)
5 10+V(1) -2+-1*V(1) 2 32 2 4 (4)A> 23+V(1)
6 13+2*V(1) 1 2 32 2 44+V(1) (4)A>
7 14+2*V(1) 2 2 32 2 45+V(1) (1)B>
8 16+2*V(1) 0 2 32 2 45+V(1) <A(2)
9 21+3*V(1) -5+-1*V(1) 2 32 2 <A(2) 25+V(1)
10 23+3*V(1) -3+-1*V(1) 2 32 4 (4)A> 25+V(1)
11 28+4*V(1) 2 2 32 46+V(1) (4)A>
12 29+4*V(1) 3 2 32 47+V(1) (1)B>
13 31+4*V(1) 1 2 32 47+V(1) <A(2)
14 38+5*V(1) -6+-1*V(1) 2 32 <A(2) 27+V(1)
15 39+5*V(1) -7+-1*V(1) 2 3 <B(1) 28+V(1)
16 43+5*V(1) -5+-1*V(1) 2 4 (4)A> 28+V(1)
17 51+6*V(1) 3 2 49+V(1) (4)A>
18 52+6*V(1) 4 2 410+V(1) (1)B>
19 54+6*V(1) 2 2 410+V(1) <A(2)
20 64+7*V(1) -8+-1*V(1) 2 <A(2) 210+V(1)
21 66+7*V(1) -6+-1*V(1) 4 (4)A> 210+V(1)
22 76+8*V(1) 4 411+V(1) (4)A>
23 77+8*V(1) 5 412+V(1) (1)B>
24 79+8*V(1) 3 412+V(1) <A(2)
25 91+9*V(1) -9+-1*V(1) <A(2) 212+V(1)
26 93+9*V(1) -7+-1*V(1) 1 (3)B> 212+V(1)
27 105+10*V(1) 5 1 312+V(1) (3)B>
28 107+10*V(1) 3 1 312+V(1) <B(1)
29 111+10*V(1) 5 1 311+V(1) 4 (4)A>
<< Success! ==> defined new CTR 10 (PPA)
5630 541069 933 1 3941 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=938, repcount=470, factor=3/2
8450 1208469 1403 1 3 41411 (4)A>
== Executing PPA-CTR 2 (once), V(1)=1408
8459 1211306 1404 22 31411 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=1408, repcount=705, factor=3/2
12689 2709431 2109 22 3 42116 (4)A>
== Executing PPA-CTR 8 (once), V(1)=2113, V(2)=0
12698 2713678 2110 2 3 2 32116 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=2113, repcount=1057, factor=3/2
19040 6075995 3167 2 3 2 32 43172 (4)A>
19041 6075996 3168 2 3 2 32 43173 (1)B>
19042 6075998 3166 2 3 2 32 43173 <A(2)
19043 6079171 -7 2 3 2 32 <A(2) 23173
19044 6079172 -8 2 3 2 3 <B(1) 23174
19045 6079176 -6 2 3 2 4 (4)A> 23174
19046 6082350 3168 2 3 2 43175 (4)A>
19047 6082351 3169 2 3 2 43176 (1)B>
19048 6082353 3167 2 3 2 43176 <A(2)
19049 6085529 -9 2 3 2 <A(2) 23176
19050 6085531 -7 2 3 4 (4)A> 23176
19051 6088707 3169 2 3 43177 (4)A>
19052 6088708 3170 2 3 43178 (1)B>
19053 6088710 3168 2 3 43178 <A(2)
19054 6091888 -10 2 3 <A(2) 23178
19055 6091889 -11 2 <B(1) 23179
19056 6091891 -9 3 (2)B> 23179
19057 6091892 -8 3 2 (3)B> 23178
19058 6095070 3170 3 2 33178 (3)B>
19059 6095072 3168 3 2 33178 <B(1)
19060 6095076 3170 3 2 33177 4 (4)A>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 2 3 2 32 41+V(1) (4)A>
1 1 1 2 3 2 32 42+V(1) (1)B>
2 3 -1 2 3 2 32 42+V(1) <A(2)
3 5+V(1) -3+-1*V(1) 2 3 2 32 <A(2) 22+V(1)
4 6+V(1) -4+-1*V(1) 2 3 2 3 <B(1) 23+V(1)
5 10+V(1) -2+-1*V(1) 2 3 2 4 (4)A> 23+V(1)
6 13+2*V(1) 1 2 3 2 44+V(1) (4)A>
7 14+2*V(1) 2 2 3 2 45+V(1) (1)B>
8 16+2*V(1) 0 2 3 2 45+V(1) <A(2)
9 21+3*V(1) -5+-1*V(1) 2 3 2 <A(2) 25+V(1)
10 23+3*V(1) -3+-1*V(1) 2 3 4 (4)A> 25+V(1)
11 28+4*V(1) 2 2 3 46+V(1) (4)A>
12 29+4*V(1) 3 2 3 47+V(1) (1)B>
13 31+4*V(1) 1 2 3 47+V(1) <A(2)
14 38+5*V(1) -6+-1*V(1) 2 3 <A(2) 27+V(1)
15 39+5*V(1) -7+-1*V(1) 2 <B(1) 28+V(1)
16 41+5*V(1) -5+-1*V(1) 3 (2)B> 28+V(1)
17 42+5*V(1) -4+-1*V(1) 3 2 (3)B> 27+V(1)
18 49+6*V(1) 3 3 2 37+V(1) (3)B>
19 51+6*V(1) 1 3 2 37+V(1) <B(1)
20 55+6*V(1) 3 3 2 36+V(1) 4 (4)A>
<< Success! ==> defined new CTR 11 (PPA)
19060 6095076 3170 3 2 33177 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=3174, repcount=1588, factor=3/2
28588 13676188 4758 3 2 3 44765 (4)A>
28589 13676189 4759 3 2 3 44766 (1)B>
28590 13676191 4757 3 2 3 44766 <A(2)
28591 13680957 -9 3 2 3 <A(2) 24766
28592 13680958 -10 3 2 <B(1) 24767
28593 13680960 -8 32 (2)B> 24767
28594 13680961 -7 32 2 (3)B> 24766
28595 13685727 4759 32 2 34766 (3)B>
28596 13685729 4757 32 2 34766 <B(1)
28597 13685733 4759 32 2 34765 4 (4)A>
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 31+V(2) 2 3 43+V(1) (4)A>
1 1 1 31+V(2) 2 3 44+V(1) (1)B>
2 3 -1 31+V(2) 2 3 44+V(1) <A(2)
3 7+V(1) -5+-1*V(1) 31+V(2) 2 3 <A(2) 24+V(1)
4 8+V(1) -6+-1*V(1) 31+V(2) 2 <B(1) 25+V(1)
5 10+V(1) -4+-1*V(1) 32+V(2) (2)B> 25+V(1)
6 11+V(1) -3+-1*V(1) 32+V(2) 2 (3)B> 24+V(1)
7 15+2*V(1) 1 32+V(2) 2 34+V(1) (3)B>
8 17+2*V(1) -1 32+V(2) 2 34+V(1) <B(1)
9 21+2*V(1) 1 32+V(2) 2 33+V(1) 4 (4)A>
<< Success! ==> defined new CTR 12 (PPA)
28597 13685733 4759 32 2 34765 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=4762, repcount=2382, factor=3/2
42889 30731325 7141 32 2 3 47147 (4)A>
== Executing PPA-CTR 12 (once), V(1)=7144, V(2)=1
42898 30745634 7142 33 2 37147 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=7144, repcount=3573, factor=3/2
64336 69080351 10715 33 2 3 410720 (4)A>
== Executing PPA-CTR 12 (once), V(1)=10717, V(2)=2
64345 69101806 10716 34 2 310720 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=10717, repcount=5359, factor=3/2
96499 155312039 16075 34 2 32 416078 (4)A>
96500 155312040 16076 34 2 32 416079 (1)B>
96501 155312042 16074 34 2 32 416079 <A(2)
96502 155328121 -5 34 2 32 <A(2) 216079
96503 155328122 -6 34 2 3 <B(1) 216080
96504 155328126 -4 34 2 4 (4)A> 216080
96505 155344206 16076 34 2 416081 (4)A>
96506 155344207 16077 34 2 416082 (1)B>
96507 155344209 16075 34 2 416082 <A(2)
96508 155360291 -7 34 2 <A(2) 216082
96509 155360293 -5 34 4 (4)A> 216082
96510 155376375 16077 34 416083 (4)A>
96511 155376376 16078 34 416084 (1)B>
96512 155376378 16076 34 416084 <A(2)
96513 155392462 -8 34 <A(2) 216084
96514 155392463 -9 33 <B(1) 216085
96515 155392467 -7 32 4 (4)A> 216085
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 33+V(1) 4 (4)A> 21+V(2)
1 1+V(2) 1+V(2) 33+V(1) 42+V(2) (4)A>
2 2+V(2) 2+V(2) 33+V(1) 43+V(2) (1)B>
3 4+V(2) 0+V(2) 33+V(1) 43+V(2) <A(2)
4 7+2*V(2) -3 33+V(1) <A(2) 23+V(2)
5 8+2*V(2) -4 32+V(1) <B(1) 24+V(2)
6 12+2*V(2) -2 31+V(1) 4 (4)A> 24+V(2)
<< Success! ==> defined new CTR 13 (PA)
96516 155408552 16078 32 416086 (4)A>
96517 155408553 16079 32 416087 (1)B>
96518 155408555 16077 32 416087 <A(2)
96519 155424642 -10 32 <A(2) 216087
96520 155424643 -11 3 <B(1) 216088
96521 155424647 -9 4 (4)A> 216088
96522 155440735 16079 416089 (4)A>
96523 155440736 16080 416090 (1)B>
96524 155440738 16078 416090 <A(2)
96525 155456828 -12 <A(2) 216090
96526 155456830 -10 1 (3)B> 216090
96527 155472920 16080 1 316090 (3)B>
96528 155472922 16078 1 316090 <B(1)
96529 155472926 16080 1 316089 4 (4)A>
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 32 41+V(1) (4)A> 21+V(2)
1 1+V(2) 1+V(2) 32 42+V(1)+V(2) (4)A>
2 2+V(2) 2+V(2) 32 43+V(1)+V(2) (1)B>
3 4+V(2) 0+V(2) 32 43+V(1)+V(2) <A(2)
4 7+V(1)+2*V(2) -3+-1*V(1) 32 <A(2) 23+V(1)+V(2)
5 8+V(1)+2*V(2) -4+-1*V(1) 3 <B(1) 24+V(1)+V(2)
6 12+V(1)+2*V(2) -2+-1*V(1) 4 (4)A> 24+V(1)+V(2)
7 16+2*V(1)+3*V(2) 2+V(2) 45+V(1)+V(2) (4)A>
8 17+2*V(1)+3*V(2) 3+V(2) 46+V(1)+V(2) (1)B>
9 19+2*V(1)+3*V(2) 1+V(2) 46+V(1)+V(2) <A(2)
10 25+3*V(1)+4*V(2) -5+-1*V(1) <A(2) 26+V(1)+V(2)
11 27+3*V(1)+4*V(2) -3+-1*V(1) 1 (3)B> 26+V(1)+V(2)
12 33+4*V(1)+5*V(2) 3+V(2) 1 36+V(1)+V(2) (3)B>
13 35+4*V(1)+5*V(2) 1+V(2) 1 36+V(1)+V(2) <B(1)
14 39+4*V(1)+5*V(2) 3+V(2) 1 35+V(1)+V(2) 4 (4)A>
<< Success! ==> defined new CTR 14 (PPA)
96529 155472926 16080 1 316089 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=16086, repcount=8044, factor=3/2
144793 349671174 24124 1 3 424133 (4)A>
== Executing PPA-CTR 2 (once), V(1)=24130
144802 349719455 24125 22 324133 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=24130, repcount=12066, factor=3/2
217198 786605183 36191 22 3 436199 (4)A>
== Executing PPA-CTR 8 (once), V(1)=36196, V(2)=0
217207 786677596 36192 2 3 2 336199 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=36196, repcount=18099, factor=3/2
325801 1769579989 54291 2 3 2 3 454298 (4)A>
== Executing PPA-CTR 9 (once), V(1)=54295, V(2)=0
325810 1769688600 54292 2 32 2 354298 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=54295, repcount=27148, factor=3/2
488698 3981001792 81440 2 32 2 32 481445 (4)A>
== Executing PPA-CTR 10 (once), V(1)=81444
488727 3981816343 81445 1 381455 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=81452, repcount=40727, factor=3/2
733089 8958289200 122172 1 3 4122182 (4)A>
== Executing PPA-CTR 2 (once), V(1)=122179
733098 8958533579 122173 22 3122182 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=122179, repcount=61090, factor=3/2
1099638 20155108779 183263 22 32 4183271 (4)A>
1099639 20155108780 183264 22 32 4183272 (1)B>
1099640 20155108782 183262 22 32 4183272 <A(2)
1099641 20155292054 -10 22 32 <A(2) 2183272
1099642 20155292055 -11 22 3 <B(1) 2183273
1099643 20155292059 -9 22 4 (4)A> 2183273
1099644 20155475332 183264 22 4183274 (4)A>
1099645 20155475333 183265 22 4183275 (1)B>
1099646 20155475335 183263 22 4183275 <A(2)
1099647 20155658610 -12 22 <A(2) 2183275
1099648 20155658612 -10 2 4 (4)A> 2183275
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 22+V(1) 4 (4)A> 21+V(2)
1 1+V(2) 1+V(2) 22+V(1) 42+V(2) (4)A>
2 2+V(2) 2+V(2) 22+V(1) 43+V(2) (1)B>
3 4+V(2) 0+V(2) 22+V(1) 43+V(2) <A(2)
4 7+2*V(2) -3 22+V(1) <A(2) 23+V(2)
5 9+2*V(2) -1 21+V(1) 4 (4)A> 23+V(2)
<< Success! ==> defined new CTR 15 (PA)
1099649 20155841887 183265 2 4183276 (4)A>
1099650 20155841888 183266 2 4183277 (1)B>
1099651 20155841890 183264 2 4183277 <A(2)
1099652 20156025167 -13 2 <A(2) 2183277
1099653 20156025169 -11 4 (4)A> 2183277
1099654 20156208446 183266 4183278 (4)A>
1099655 20156208447 183267 4183279 (1)B>
1099656 20156208449 183265 4183279 <A(2)
1099657 20156391728 -14 <A(2) 2183279
1099658 20156391730 -12 1 (3)B> 2183279
1099659 20156575009 183267 1 3183279 (3)B>
1099660 20156575011 183265 1 3183279 <B(1)
1099661 20156575015 183267 1 3183278 4 (4)A>
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 2 41+V(1) (4)A> 21+V(2)
1 1+V(2) 1+V(2) 2 42+V(1)+V(2) (4)A>
2 2+V(2) 2+V(2) 2 43+V(1)+V(2) (1)B>
3 4+V(2) 0+V(2) 2 43+V(1)+V(2) <A(2)
4 7+V(1)+2*V(2) -3+-1*V(1) 2 <A(2) 23+V(1)+V(2)
5 9+V(1)+2*V(2) -1+-1*V(1) 4 (4)A> 23+V(1)+V(2)
6 12+2*V(1)+3*V(2) 2+V(2) 44+V(1)+V(2) (4)A>
7 13+2*V(1)+3*V(2) 3+V(2) 45+V(1)+V(2) (1)B>
8 15+2*V(1)+3*V(2) 1+V(2) 45+V(1)+V(2) <A(2)
9 20+3*V(1)+4*V(2) -4+-1*V(1) <A(2) 25+V(1)+V(2)
10 22+3*V(1)+4*V(2) -2+-1*V(1) 1 (3)B> 25+V(1)+V(2)
11 27+4*V(1)+5*V(2) 3+V(2) 1 35+V(1)+V(2) (3)B>
12 29+4*V(1)+5*V(2) 1+V(2) 1 35+V(1)+V(2) <B(1)
13 33+4*V(1)+5*V(2) 3+V(2) 1 34+V(1)+V(2) 4 (4)A>
<< Success! ==> defined new CTR 16 (PPA)
1099661 20156575015 183267 1 3183278 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=183275, repcount=91638, factor=3/2
1649489 45350060527 274905 1 32 4274915 (4)A>
== Executing PPA-CTR 7 (once), V(1)=274914, V(2)=0
1649503 45351160219 274907 1 3274919 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=274916, repcount=137459, factor=3/2
2474257 102037464852 412366 1 3 4412378 (4)A>
== Executing PPA-CTR 2 (once), V(1)=412375
2474266 102038289623 412367 22 3412378 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=412375, repcount=206188, factor=3/2
3711394 229580825535 618555 22 32 4618565 (4)A>
3711395 229580825536 618556 22 32 4618566 (1)B>
3711396 229580825538 618554 22 32 4618566 <A(2)
3711397 229581444104 -12 22 32 <A(2) 2618566
3711398 229581444105 -13 22 3 <B(1) 2618567
3711399 229581444109 -11 22 4 (4)A> 2618567
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 22+V(2) 32 41+V(1) (4)A>
1 1 1 22+V(2) 32 42+V(1) (1)B>
2 3 -1 22+V(2) 32 42+V(1) <A(2)
3 5+V(1) -3+-1*V(1) 22+V(2) 32 <A(2) 22+V(1)
4 6+V(1) -4+-1*V(1) 22+V(2) 3 <B(1) 23+V(1)
5 10+V(1) -2+-1*V(1) 22+V(2) 4 (4)A> 23+V(1)
<< Success! ==> defined new CTR 17 (PPA)
3711399 229581444109 -11 22 4 (4)A> 2618567
== Executing PA-CTR 15, V(1)=0, V(2)=618566, repcount=1, factor=2/1
3711404 229582681250 -12 2 4 (4)A> 2618569
== Executing PPA-CTR 16 (once), V(1)=0, V(2)=618568
3711417 229585774123 618559 1 3618572 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=618569, repcount=309285, factor=3/2
5567127 516560500648 927844 1 32 4927856 (4)A>
== Executing PPA-CTR 7 (once), V(1)=927855, V(2)=0
5567141 516564212104 927846 1 3927860 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=927857, repcount=463929, factor=3/2
8350715 1162259202517 1391775 1 32 41391788 (4)A>
== Executing PPA-CTR 7 (once), V(1)=1391787, V(2)=0
8350729 1162264769701 1391777 1 31391792 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=1391789, repcount=695895, factor=3/2
12526099 2615081281726 2087672 1 32 42087686 (4)A>
== Executing PPA-CTR 7 (once), V(1)=2087685, V(2)=0
12526113 2615089632502 2087674 1 32087690 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=2087687, repcount=1043844, factor=3/2
18789177 5883930959950 3131518 1 32 43131533 (4)A>
== Executing PPA-CTR 7 (once), V(1)=3131532, V(2)=0
18789191 5883943486114 3131520 1 33131537 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=3131534, repcount=1565768, factor=3/2
28183799 13238847433266 4697288 1 3 44697305 (4)A>
== Executing PPA-CTR 2 (once), V(1)=4697302
28183808 13238856827891 4697289 22 34697305 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=4697302, repcount=2348652, factor=3/2
42275720 29787378965723 7045941 22 3 47045957 (4)A>
== Executing PPA-CTR 8 (once), V(1)=7045954, V(2)=0
42275729 29787393057652 7045942 2 3 2 37045957 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=7045954, repcount=3522978, factor=3/2
63413597 67021550252884 10568920 2 3 2 3 410568935 (4)A>
== Executing PPA-CTR 9 (once), V(1)=10568932, V(2)=0
63413606 67021571390769 10568921 2 32 2 310568935 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=10568932, repcount=5284467, factor=3/2
95120408 150798398657706 15853388 2 32 2 3 415853402 (4)A>
== Executing PPA-CTR 9 (once), V(1)=15853399, V(2)=1
95120417 150798430364525 15853389 2 33 2 315853402 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=15853399, repcount=7926700, factor=3/2
142680617 339296228301525 23780089 2 33 2 32 423780101 (4)A>
142680618 339296228301526 23780090 2 33 2 32 423780102 (1)B>
142680619 339296228301528 23780088 2 33 2 32 423780102 <A(2)
142680620 339296252081630 -14 2 33 2 32 <A(2) 223780102
142680621 339296252081631 -15 2 33 2 3 <B(1) 223780103
142680622 339296252081635 -13 2 33 2 4 (4)A> 223780103
142680623 339296275861738 23780090 2 33 2 423780104 (4)A>
142680624 339296275861739 23780091 2 33 2 423780105 (1)B>
142680625 339296275861741 23780089 2 33 2 423780105 <A(2)
142680626 339296299641846 -16 2 33 2 <A(2) 223780105
142680627 339296299641848 -14 2 33 4 (4)A> 223780105
142680628 339296323421953 23780091 2 33 423780106 (4)A>
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 [*]* 33+V(2) 2 32 41+V(1) (4)A>
1 1 1 [*]* 33+V(2) 2 32 42+V(1) (1)B>
2 3 -1 [*]* 33+V(2) 2 32 42+V(1) <A(2)
3 5+V(1) -3+-1*V(1) [*]* 33+V(2) 2 32 <A(2) 22+V(1)
4 6+V(1) -4+-1*V(1) [*]* 33+V(2) 2 3 <B(1) 23+V(1)
5 10+V(1) -2+-1*V(1) [*]* 33+V(2) 2 4 (4)A> 23+V(1)
6 13+2*V(1) 1 [*]* 33+V(2) 2 44+V(1) (4)A>
7 14+2*V(1) 2 [*]* 33+V(2) 2 45+V(1) (1)B>
8 16+2*V(1) 0 [*]* 33+V(2) 2 45+V(1) <A(2)
9 21+3*V(1) -5+-1*V(1) [*]* 33+V(2) 2 <A(2) 25+V(1)
10 23+3*V(1) -3+-1*V(1) [*]* 33+V(2) 4 (4)A> 25+V(1)
11 28+4*V(1) 2 [*]* 33+V(2) 46+V(1) (4)A>
<< Success! ==> defined new CTR 18 (PPA)
142680628 339296323421953 23780091 2 33 423780106 (4)A>
== Executing PA-CTR 1, V(1)=23780105, V(2)=0, repcount=1, factor=3/2
142680634 339296370982176 23780092 2 3 423780109 (4)A>
142680635 339296370982177 23780093 2 3 423780110 (1)B>
142680636 339296370982179 23780091 2 3 423780110 <A(2)
142680637 339296394762289 -19 2 3 <A(2) 223780110
142680638 339296394762290 -20 2 <B(1) 223780111
142680639 339296394762292 -18 3 (2)B> 223780111
142680640 339296394762293 -17 3 2 (3)B> 223780110
142680641 339296418542403 23780093 3 2 323780110 (3)B>
142680642 339296418542405 23780091 3 2 323780110 <B(1)
142680643 339296418542409 23780093 3 2 323780109 4 (4)A>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 2 3 43+V(1) (4)A>
1 1 1 2 3 44+V(1) (1)B>
2 3 -1 2 3 44+V(1) <A(2)
3 7+V(1) -5+-1*V(1) 2 3 <A(2) 24+V(1)
4 8+V(1) -6+-1*V(1) 2 <B(1) 25+V(1)
5 10+V(1) -4+-1*V(1) 3 (2)B> 25+V(1)
6 11+V(1) -3+-1*V(1) 3 2 (3)B> 24+V(1)
7 15+2*V(1) 1 3 2 34+V(1) (3)B>
8 17+2*V(1) -1 3 2 34+V(1) <B(1)
9 21+2*V(1) 1 3 2 33+V(1) 4 (4)A>
<< Success! ==> defined new CTR 19 (PPA)
142680643 339296418542409 23780093 3 2 323780109 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=23780106, repcount=11890054, factor=3/2
214020967 763416689811697 35670147 3 2 3 435670163 (4)A>
== Executing PPA-CTR 12 (once), V(1)=35670160, V(2)=0
214020976 763416761152038 35670148 32 2 335670163 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=35670160, repcount=17835081, factor=3/2
321031462 1717687282332531 53505229 32 2 3 453505244 (4)A>
== Executing PPA-CTR 12 (once), V(1)=53505241, V(2)=1
321031471 1717687389343034 53505230 33 2 353505244 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=53505241, repcount=26752621, factor=3/2
481547197 3864795847978167 80257851 33 2 32 480257864 (4)A>
481547198 3864795847978168 80257852 33 2 32 480257865 (1)B>
481547199 3864795847978170 80257850 33 2 32 480257865 <A(2)
481547200 3864795928236035 -15 33 2 32 <A(2) 280257865
481547201 3864795928236036 -16 33 2 3 <B(1) 280257866
481547202 3864795928236040 -14 33 2 4 (4)A> 280257866
481547203 3864796008493906 80257852 33 2 480257867 (4)A>
481547204 3864796008493907 80257853 33 2 480257868 (1)B>
481547205 3864796008493909 80257851 33 2 480257868 <A(2)
481547206 3864796088751777 -17 33 2 <A(2) 280257868
481547207 3864796088751779 -15 33 4 (4)A> 280257868
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 33+V(2) 2 32 41+V(1) (4)A>
1 1 1 33+V(2) 2 32 42+V(1) (1)B>
2 3 -1 33+V(2) 2 32 42+V(1) <A(2)
3 5+V(1) -3+-1*V(1) 33+V(2) 2 32 <A(2) 22+V(1)
4 6+V(1) -4+-1*V(1) 33+V(2) 2 3 <B(1) 23+V(1)
5 10+V(1) -2+-1*V(1) 33+V(2) 2 4 (4)A> 23+V(1)
6 13+2*V(1) 1 33+V(2) 2 44+V(1) (4)A>
7 14+2*V(1) 2 33+V(2) 2 45+V(1) (1)B>
8 16+2*V(1) 0 33+V(2) 2 45+V(1) <A(2)
9 21+3*V(1) -5+-1*V(1) 33+V(2) 2 <A(2) 25+V(1)
10 23+3*V(1) -3+-1*V(1) 33+V(2) 4 (4)A> 25+V(1)
<< Success! ==> defined new CTR 20 (PPA)
481547207 3864796088751779 -15 33 4 (4)A> 280257868
== Executing PA-CTR 13, V(1)=0, V(2)=80257867, repcount=1, factor=3/2
481547213 3864796249267525 -17 3 4 (4)A> 280257871
481547214 3864796329525396 80257854 3 480257872 (4)A>
481547215 3864796329525397 80257855 3 480257873 (1)B>
481547216 3864796329525399 80257853 3 480257873 <A(2)
481547217 3864796409783272 -20 3 <A(2) 280257873
481547218 3864796409783273 -21 <B(1) 280257874
481547219 3864796409783274 -22 <A(0) 1 280257874
481547220 3864796409783277 -23 <A(2) 0 1 280257874
481547221 3864796409783279 -21 1 (3)B> 0 1 280257874
481547222 3864796409783281 -23 1 <B(1) 0 1 280257874
481547223 3864796409783283 -21 2 (2)B> 0 1 280257874
481547224 3864796409783286 -20 2 4 (1)B> 1 280257874
481547225 3864796409783287 -19 2 4 1 (2)B> 280257874
481547226 3864796409783288 -18 2 4 1 2 (3)B> 280257873
481547227 3864796490041161 80257855 2 4 1 2 380257873 (3)B>
481547228 3864796490041163 80257853 2 4 1 2 380257873 <B(1)
481547229 3864796490041167 80257855 2 4 1 2 380257872 4 (4)A>
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 3 41+V(1) (4)A> 22+V(2)
1 2+V(2) 2+V(2) 3 43+V(1)+V(2) (4)A>
2 3+V(2) 3+V(2) 3 44+V(1)+V(2) (1)B>
3 5+V(2) 1+V(2) 3 44+V(1)+V(2) <A(2)
4 9+V(1)+2*V(2) -3+-1*V(1) 3 <A(2) 24+V(1)+V(2)
5 10+V(1)+2*V(2) -4+-1*V(1) <B(1) 25+V(1)+V(2)
6 11+V(1)+2*V(2) -5+-1*V(1) <A(0) 1 25+V(1)+V(2)
7 14+V(1)+2*V(2) -6+-1*V(1) <A(2) 0 1 25+V(1)+V(2)
8 16+V(1)+2*V(2) -4+-1*V(1) 1 (3)B> 0 1 25+V(1)+V(2)
9 18+V(1)+2*V(2) -6+-1*V(1) 1 <B(1) 0 1 25+V(1)+V(2)
10 20+V(1)+2*V(2) -4+-1*V(1) 2 (2)B> 0 1 25+V(1)+V(2)
11 23+V(1)+2*V(2) -3+-1*V(1) 2 4 (1)B> 1 25+V(1)+V(2)
12 24+V(1)+2*V(2) -2+-1*V(1) 2 4 1 (2)B> 25+V(1)+V(2)
13 25+V(1)+2*V(2) -1+-1*V(1) 2 4 1 2 (3)B> 24+V(1)+V(2)
14 29+2*V(1)+3*V(2) 3+V(2) 2 4 1 2 34+V(1)+V(2) (3)B>
15 31+2*V(1)+3*V(2) 1+V(2) 2 4 1 2 34+V(1)+V(2) <B(1)
16 35+2*V(1)+3*V(2) 3+V(2) 2 4 1 2 33+V(1)+V(2) 4 (4)A>
<< Success! ==> defined new CTR 21 (PPA)
481547229 3864796490041167 80257855 2 4 1 2 380257872 4 (4)A>
== Executing PA-CTR 5, V(1)=0, V(2)=80257869, repcount=40128935, factor=3/2
722320839 8695791164033192 120386790 2 4 1 2 32 4120386806 (4)A>
== Executing PPA-CTR 6 (once), V(1)=120386805, V(2)=0, V(3)=0
722320864 8695792127127716 120386794 1 3120386815 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=120386812, repcount=60193407, factor=3/2
1083481306 19565531467864733 180580201 1 3 4180580222 (4)A>
== Executing PPA-CTR 2 (once), V(1)=180580219
1083481315 19565531829025192 180580202 22 3180580222 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=180580219, repcount=90290110, factor=3/2
1625221975 44022444623362592 270870312 22 32 4270870331 (4)A>
== Executing PPA-CTR 17 (once), V(1)=270870330, V(2)=0
1625221980 44022444894232932 -20 22 4 (4)A> 2270870333
== Executing PA-CTR 15, V(1)=0, V(2)=270870332, repcount=1, factor=2/1
1625221985 44022445435973605 -21 2 4 (4)A> 2270870335
== Executing PPA-CTR 16 (once), V(1)=0, V(2)=270870334
1625221998 44022446790325308 270870316 1 3270870338 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=270870335, repcount=135435168, factor=3/2
2437833006 99050502338241660 406305484 1 32 4406305505 (4)A>
== Executing PPA-CTR 7 (once), V(1)=406305504, V(2)=0
2437833020 99050503963463712 406305486 1 3406305509 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=406305506, repcount=203152754, factor=3/2
3656749544 2228636[4]8344800 609458240 1 3 4609458263 (4)A>
== Executing PPA-CTR 2 (once), V(1)=609458260
3656749553 2228636[4]7261341 609458241 22 3609458263 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=609458260, repcount=304729131, factor=3/2
5485124339 5014431[4]4598134 914187372 22 3 4914187394 (4)A>
== Executing PPA-CTR 8 (once), V(1)=914187391, V(2)=0
5485124348 5014431[4]2972937 914187373 2 3 2 3914187394 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=914187391, repcount=457093696, factor=3/2
8227686524 1128247[5]2731145 1371281069 2 3 2 32 41371281089 (4)A>
== Executing PPA-CTR 11 (once), V(1)=1371281088
8227686544 1128247[5]0417728 1371281072 3 2 31371281094 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=1371281091, repcount=685640546, factor=3/2
12341529820 2538556[5]4357536 2056921618 3 2 32 42056921639 (4)A>
12341529821 2538556[5]4357537 2056921619 3 2 32 42056921640 (1)B>
12341529822 2538556[5]4357539 2056921617 3 2 32 42056921640 <A(2)
12341529823 2538556[5]1279179 -23 3 2 32 <A(2) 22056921640
12341529824 2538556[5]1279180 -24 3 2 3 <B(1) 22056921641
12341529825 2538556[5]1279184 -22 3 2 4 (4)A> 22056921641
12341529826 2538556[5]8200825 2056921619 3 2 42056921642 (4)A>
12341529827 2538556[5]8200826 2056921620 3 2 42056921643 (1)B>
12341529828 2538556[5]8200828 2056921618 3 2 42056921643 <A(2)
12341529829 2538556[5]5122471 -25 3 2 <A(2) 22056921643
12341529830 2538556[5]5122473 -23 3 4 (4)A> 22056921643
12341529831 2538556[5]2044116 2056921620 3 42056921644 (4)A>
12341529832 2538556[5]2044117 2056921621 3 42056921645 (1)B>
12341529833 2538556[5]2044119 2056921619 3 42056921645 <A(2)
12341529834 2538556[5]8965764 -26 3 <A(2) 22056921645
12341529835 2538556[5]8965765 -27 <B(1) 22056921646
12341529836 2538556[5]8965766 -28 <A(0) 1 22056921646
12341529837 2538556[5]8965769 -29 <A(2) 0 1 22056921646
12341529838 2538556[5]8965771 -27 1 (3)B> 0 1 22056921646
12341529839 2538556[5]8965773 -29 1 <B(1) 0 1 22056921646
12341529840 2538556[5]8965775 -27 2 (2)B> 0 1 22056921646
12341529841 2538556[5]8965778 -26 2 4 (1)B> 1 22056921646
12341529842 2538556[5]8965779 -25 2 4 1 (2)B> 22056921646
12341529843 2538556[5]8965780 -24 2 4 1 2 (3)B> 22056921645
12341529844 2538556[5]5887425 2056921621 2 4 1 2 32056921645 (3)B>
12341529845 2538556[5]5887427 2056921619 2 4 1 2 32056921645 <B(1)
12341529846 2538556[5]5887431 2056921621 2 4 1 2 32056921644 4 (4)A>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 3 2 32 41+V(1) (4)A>
1 1 1 3 2 32 42+V(1) (1)B>
2 3 -1 3 2 32 42+V(1) <A(2)
3 5+V(1) -3+-1*V(1) 3 2 32 <A(2) 22+V(1)
4 6+V(1) -4+-1*V(1) 3 2 3 <B(1) 23+V(1)
5 10+V(1) -2+-1*V(1) 3 2 4 (4)A> 23+V(1)
6 13+2*V(1) 1 3 2 44+V(1) (4)A>
7 14+2*V(1) 2 3 2 45+V(1) (1)B>
8 16+2*V(1) 0 3 2 45+V(1) <A(2)
9 21+3*V(1) -5+-1*V(1) 3 2 <A(2) 25+V(1)
10 23+3*V(1) -3+-1*V(1) 3 4 (4)A> 25+V(1)
11 28+4*V(1) 2 3 46+V(1) (4)A>
12 29+4*V(1) 3 3 47+V(1) (1)B>
13 31+4*V(1) 1 3 47+V(1) <A(2)
14 38+5*V(1) -6+-1*V(1) 3 <A(2) 27+V(1)
15 39+5*V(1) -7+-1*V(1) <B(1) 28+V(1)
16 40+5*V(1) -8+-1*V(1) <A(0) 1 28+V(1)
17 43+5*V(1) -9+-1*V(1) <A(2) 0 1 28+V(1)
18 45+5*V(1) -7+-1*V(1) 1 (3)B> 0 1 28+V(1)
19 47+5*V(1) -9+-1*V(1) 1 <B(1) 0 1 28+V(1)
20 49+5*V(1) -7+-1*V(1) 2 (2)B> 0 1 28+V(1)
21 52+5*V(1) -6+-1*V(1) 2 4 (1)B> 1 28+V(1)
22 53+5*V(1) -5+-1*V(1) 2 4 1 (2)B> 28+V(1)
23 54+5*V(1) -4+-1*V(1) 2 4 1 2 (3)B> 27+V(1)
24 61+6*V(1) 3 2 4 1 2 37+V(1) (3)B>
25 63+6*V(1) 1 2 4 1 2 37+V(1) <B(1)
26 67+6*V(1) 3 2 4 1 2 36+V(1) 4 (4)A>
<< Success! ==> defined new CTR 22 (PPA)
12341529846 2538556[5]5887431 2056921621 2 4 1 2 32056921644 4 (4)A>
== Executing PA-CTR 5, V(1)=0, V(2)=2056921641, repcount=1028460821, factor=3/2
18512294772 5711751[5]6477764 3085382442 2 4 1 2 32 43085382464 (4)A>
== Executing PPA-CTR 6 (once), V(1)=3085382463, V(2)=0, V(3)=0
18512294797 5711751[5]9537552 3085382446 1 33085382473 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=3085382470, repcount=1542691236, factor=3/2
27768442213 1285143[6]0073000 4628073682 1 3 44628073709 (4)A>
== Executing PPA-CTR 2 (once), V(1)=4628073706
27768442222 1285143[6]6220433 4628073683 22 34628073709 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=4628073706, repcount=2314036854, factor=3/2
41652663346 2891573[6]7240921 6942110537 22 3 46942110563 (4)A>
== Executing PPA-CTR 8 (once), V(1)=6942110560, V(2)=0
41652663355 2891573[6]1462062 6942110538 2 3 2 36942110563 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=6942110560, repcount=3471055281, factor=3/2
62478995041 6506041[6]5981755 10413165819 2 3 2 3 410413165844 (4)A>
== Executing PPA-CTR 9 (once), V(1)=10413165841, V(2)=0
62478995050 6506041[6]2313458 10413165820 2 32 2 310413165844 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=10413165841, repcount=5206582921, factor=3/2
93718492576 1463859[7]4819391 15619748741 2 32 2 32 415619748764 (4)A>
== Executing PPA-CTR 10 (once), V(1)=15619748763
93718492605 1463859[7]2307132 15619748746 1 315619748774 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=15619748771, repcount=7809874386, factor=3/2
140577738921 3293683[7]7681980 23429623132 1 32 423429623159 (4)A>
== Executing PPA-CTR 7 (once), V(1)=23429623158, V(2)=0
140577738935 3293683[7]6174648 23429623134 1 323429623163 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=23429623160, repcount=11714811581, factor=3/2
210866608421 7410787[7]9449141 35144434715 1 3 435144434744 (4)A>
== Executing PPA-CTR 2 (once), V(1)=35144434741
210866608430 7410787[7]8318644 35144434716 22 335144434744 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=35144434741, repcount=17572217371, factor=3/2
316299912656 1667427[8]2947277 52716652087 22 32 452716652114 (4)A>
== Executing PPA-CTR 17 (once), V(1)=52716652113, V(2)=0
316299912661 1667427[8]9599400 -28 22 4 (4)A> 252716652116
== Executing PA-CTR 15, V(1)=0, V(2)=52716652115, repcount=1, factor=2/1
316299912666 1667427[8]2903639 -29 2 4 (4)A> 252716652118
== Executing PPA-CTR 16 (once), V(1)=0, V(2)=52716652117
316299912679 1667427[8]6164257 52716652091 1 352716652121 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=52716652118, repcount=26358326060, factor=3/2
474449869039 3751711[8]4795657 79074978151 1 3 479074978181 (4)A>
== Executing PPA-CTR 2 (once), V(1)=79074978178
474449869048 3751711[8]4752034 79074978152 22 379074978181 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=79074978178, repcount=39537489090, factor=3/2
711674803588 8441350[8]6727234 118612467242 22 3 4118612467271 (4)A>
== Executing PPA-CTR 8 (once), V(1)=118612467268, V(2)=0
711674803597 8441350[8]1661791 118612467243 2 3 2 3118612467271 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=118612467268, repcount=59306233635, factor=3/2
1067512205407 1899303[9]9937816 177918700878 2 3 2 3 4177918700906 (4)A>
== Executing PPA-CTR 9 (once), V(1)=177918700903, V(2)=0
1067512205416 1899303[9]7339643 177918700879 2 32 2 3177918700906 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=177918700903, repcount=88959350452, factor=3/2
1601268308128 4273433[9]8657075 266878051331 2 32 2 32 4266878051357 (4)A>
== Executing PPA-CTR 10 (once), V(1)=266878051356
1601268308157 4273433[9]9170746 266878051336 1 3266878051367 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=266878051364, repcount=133439025683, factor=3/2
2401902462255 9615225[9]0277043 400317077019 1 3 4400317077050 (4)A>
== Executing PPA-CTR 2 (once), V(1)=400317077047
2401902462264 9615225[9]4431158 400317077020 22 3400317077050 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=400317077047, repcount=200158538524, factor=3/2
3602853693408 2163425[10]6112126 600475615544 22 32 4600475615573 (4)A>
== Executing PPA-CTR 17 (once), V(1)=600475615572, V(2)=0
3602853693413 2163425[10]1727708 -30 22 4 (4)A> 2600475615575
== Executing PA-CTR 15, V(1)=0, V(2)=600475615574, repcount=1, factor=2/1
3602853693418 2163425[10]2958865 -31 2 4 (4)A> 2600475615577
== Executing PPA-CTR 16 (once), V(1)=0, V(2)=600475615576
3602853693431 2163425[10]1036778 600475615548 1 3600475615580 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=600475615577, repcount=300237807789, factor=3/2
5404280540165 4867708[10]6320231 900713423337 1 32 4900713423368 (4)A>
== Executing PPA-CTR 7 (once), V(1)=900713423367, V(2)=0
5404280540179 4867708[10]0013735 900713423339 1 3900713423372 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=900713423369, repcount=450356711685, factor=3/2
8106420810289 1095234[11]3748260 1351070135024 1 32 41351070135056 (4)A>
== Executing PPA-CTR 7 (once), V(1)=1351070135055, V(2)=0
8106420810303 1095234[11]4288516 1351070135026 1 31351070135060 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=1351070135057, repcount=675535067529, factor=3/2
12159631215477 2464277[11]5461329 2026605202555 1 32 42026605202588 (4)A>
== Executing PPA-CTR 7 (once), V(1)=2026605202587, V(2)=0
12159631215491 2464277[11]6271713 2026605202557 1 32026605202592 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=2026605202589, repcount=1013302601295, factor=3/2
18239446823261 5544623[11]9315738 3039907803852 1 32 43039907803886 (4)A>
== Executing PPA-CTR 7 (once), V(1)=3039907803885, V(2)=0
18239446823275 5544623[11]0531314 3039907803854 1 33039907803890 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=3039907803887, repcount=1519953901944, factor=3/2
27359170234939 1247540[12]0488162 4559861705798 1 32 44559861705833 (4)A>
== Executing PPA-CTR 7 (once), V(1)=4559861705832, V(2)=0
27359170234953 1247540[12]7311526 4559861705800 1 34559861705837 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=4559861705834, repcount=2279930852918, factor=3/2
41038755352461 2806965[12]3184878 6839792558718 1 3 46839792558755 (4)A>
== Executing PPA-CTR 2 (once), V(1)=6839792558752
41038755352470 2806965[12]8302403 6839792558719 22 36839792558755 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=6839792558752, repcount=3419896279377, factor=3/2
61558133028732 6315672[12]7620560 10259688838096 22 3 410259688838132 (4)A>
== Executing PPA-CTR 8 (once), V(1)=10259688838129, V(2)=0
61558133028741 6315672[12]5296839 10259688838097 2 3 2 310259688838132 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=10259688838129, repcount=5129844419065, factor=3/2
92337199543131 1421026[13]5910164 15389533257162 2 3 2 32 415389533257196 (4)A>
== Executing PPA-CTR 11 (once), V(1)=15389533257195
92337199543151 1421026[13]5453389 15389533257165 3 2 315389533257201 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=15389533257198, repcount=7694766628600, factor=3/2
138505799314751 3197309[13]5619389 23084299885765 3 2 3 423084299885801 (4)A>
== Executing PPA-CTR 12 (once), V(1)=23084299885798, V(2)=0
138505799314760 3197309[13]5391006 23084299885766 32 2 323084299885801 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=23084299885798, repcount=11542149942900, factor=3/2
207758698972160 7193946[13]6050006 34626449828666 32 2 3 434626449828701 (4)A>
== Executing PPA-CTR 12 (once), V(1)=34626449828698, V(2)=1
207758698972169 7193946[13]5707423 34626449828667 33 2 334626449828701 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=34626449828698, repcount=17313224914350, factor=3/2
311638048458269 1618637[14]2618423 51939674743017 33 2 3 451939674743051 (4)A>
== Executing PPA-CTR 12 (once), V(1)=51939674743048, V(2)=2
311638048458278 1618637[14]2104540 51939674743018 34 2 351939674743051 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=51939674743048, repcount=25969837371525, factor=3/2
467457072687428 3641935[14]8296665 77909512114543 34 2 3 477909512114576 (4)A>
== Executing PPA-CTR 12 (once), V(1)=77909512114573, V(2)=3
467457072687437 3641935[14]2525832 77909512114544 35 2 377909512114576 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=77909512114573, repcount=38954756057287, factor=3/2
701185609031159 8194354[14]0499809 116864268171831 35 2 32 4116864268171862 (4)A>
== Executing PPA-CTR 20 (once), V(1)=116864268171861, V(2)=2
701185609031169 8194354[14]5015415 -33 35 4 (4)A> 2116864268171866
== Executing PA-CTR 13, V(1)=2, V(2)=116864268171865, repcount=2, factor=3/2
701185609031181 8194354[14]7702905 -37 3 4 (4)A> 2116864268171872
== Executing PPA-CTR 21 (once), V(1)=0, V(2)=116864268171870
701185609031197 8194354[14]2218550 116864268171836 2 4 1 2 3116864268171873 4 (4)A>
== Executing PA-CTR 5, V(1)=0, V(2)=116864268171870, repcount=58432134085936, factor=3/2
1051778413546813 1843729[15]2066198 175296402257772 2 4 1 2 3 4175296402257809 (4)A>
1051778413546814 1843729[15]2066199 175296402257773 2 4 1 2 3 4175296402257810 (1)B>
1051778413546815 1843729[15]2066201 175296402257771 2 4 1 2 3 4175296402257810 <A(2)
1051778413546816 1843729[15]4324011 -39 2 4 1 2 3 <A(2) 2175296402257810
1051778413546817 1843729[15]4324012 -40 2 4 1 2 <B(1) 2175296402257811
1051778413546818 1843729[15]4324014 -38 2 4 1 3 (2)B> 2175296402257811
1051778413546819 1843729[15]4324015 -37 2 4 1 3 2 (3)B> 2175296402257810
1051778413546820 1843729[15]6581825 175296402257773 2 4 1 3 2 3175296402257810 (3)B>
1051778413546821 1843729[15]6581827 175296402257771 2 4 1 3 2 3175296402257810 <B(1)
1051778413546822 1843729[15]6581831 175296402257773 2 4 1 3 2 3175296402257809 4 (4)A>
1051778413546823 1843729[15]6581832 175296402257774 2 4 1 3 2 3175296402257809 42 (1)B>
1051778413546824 1843729[15]6581834 175296402257772 2 4 1 3 2 3175296402257809 42 <A(2)
1051778413546825 1843729[15]6581836 175296402257770 2 4 1 3 2 3175296402257809 <A(2) 22
1051778413546826 1843729[15]6581837 175296402257769 2 4 1 3 2 3175296402257808 <B(1) 23
1051778413546827 1843729[15]6581841 175296402257771 2 4 1 3 2 3175296402257807 4 (4)A> 23
1051778413546828 1843729[15]6581844 175296402257774 2 4 1 3 2 3175296402257807 44 (4)A>
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* [*]* [*]* 33+V(2) 41+V(1) (4)A>
1 1 1 [*]* [*]* [*]* [*]* [*]* 33+V(2) 42+V(1) (1)B>
2 3 -1 [*]* [*]* [*]* [*]* [*]* 33+V(2) 42+V(1) <A(2)
3 5+V(1) -3+-1*V(1) [*]* [*]* [*]* [*]* [*]* 33+V(2) <A(2) 22+V(1)
4 6+V(1) -4+-1*V(1) [*]* [*]* [*]* [*]* [*]* 32+V(2) <B(1) 23+V(1)
5 10+V(1) -2+-1*V(1) [*]* [*]* [*]* [*]* [*]* 31+V(2) 4 (4)A> 23+V(1)
6 13+2*V(1) 1 [*]* [*]* [*]* [*]* [*]* 31+V(2) 44+V(1) (4)A>
<< Success! ==> defined new CTR 23 (PA)
1051778413546828 1843729[15]6581844 175296402257774 2 4 1 3 2 3175296402257807 44 (4)A>
== Executing PA-CTR 23, V(1)=3, V(2)=175296402257804, repcount=87648201128903, factor=3/2
1577667620320246 4148391[15]0594519 262944603386677 2 4 1 3 2 3 4262944603386713 (4)A>
1577667620320247 4148391[15]0594520 262944603386678 2 4 1 3 2 3 4262944603386714 (1)B>
1577667620320248 4148391[15]0594522 262944603386676 2 4 1 3 2 3 4262944603386714 <A(2)
1577667620320249 4148391[15]3981236 -38 2 4 1 3 2 3 <A(2) 2262944603386714
1577667620320250 4148391[15]3981237 -39 2 4 1 3 2 <B(1) 2262944603386715
1577667620320251 4148391[15]3981239 -37 2 4 1 32 (2)B> 2262944603386715
1577667620320252 4148391[15]3981240 -36 2 4 1 32 2 (3)B> 2262944603386714
1577667620320253 4148391[15]7367954 262944603386678 2 4 1 32 2 3262944603386714 (3)B>
1577667620320254 4148391[15]7367956 262944603386676 2 4 1 32 2 3262944603386714 <B(1)
1577667620320255 4148391[15]7367960 262944603386678 2 4 1 32 2 3262944603386713 4 (4)A>
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* 31+V(2) 2 3 43+V(1) (4)A>
1 1 1 [*]* [*]* [*]* 31+V(2) 2 3 44+V(1) (1)B>
2 3 -1 [*]* [*]* [*]* 31+V(2) 2 3 44+V(1) <A(2)
3 7+V(1) -5+-1*V(1) [*]* [*]* [*]* 31+V(2) 2 3 <A(2) 24+V(1)
4 8+V(1) -6+-1*V(1) [*]* [*]* [*]* 31+V(2) 2 <B(1) 25+V(1)
5 10+V(1) -4+-1*V(1) [*]* [*]* [*]* 32+V(2) (2)B> 25+V(1)
6 11+V(1) -3+-1*V(1) [*]* [*]* [*]* 32+V(2) 2 (3)B> 24+V(1)
7 15+2*V(1) 1 [*]* [*]* [*]* 32+V(2) 2 34+V(1) (3)B>
8 17+2*V(1) -1 [*]* [*]* [*]* 32+V(2) 2 34+V(1) <B(1)
9 21+2*V(1) 1 [*]* [*]* [*]* 32+V(2) 2 33+V(1) 4 (4)A>
<< Success! ==> defined new CTR 24 (PPA)
1577667620320255 4148391[15]7367960 262944603386678 2 4 1 32 2 3262944603386713 4 (4)A>
== Executing PA-CTR 23, V(1)=0, V(2)=262944603386710, repcount=131472301693356, factor=3/2
2366501430480391 9333881[15]7929728 394416905080034 2 4 1 32 2 3 4394416905080069 (4)A>
== Executing PPA-CTR 24 (once), V(1)=394416905080066, V(2)=1
2366501430480400 9333881[15]8089881 394416905080035 2 4 1 33 2 3394416905080069 4 (4)A>
== Executing PA-CTR 23, V(1)=0, V(2)=394416905080066, repcount=197208452540034, factor=3/2
3549752145720604 2100123[16]1653689 591625357620069 2 4 1 33 2 3 4591625357620103 (4)A>
== Executing PPA-CTR 24 (once), V(1)=591625357620100, V(2)=2
3549752145720613 2100123[16]6893910 591625357620070 2 4 1 34 2 3591625357620103 4 (4)A>
== Executing PA-CTR 23, V(1)=0, V(2)=591625357620100, repcount=295812678810051, factor=3/2
5324628218580919 4725277[16]0862223 887438036430121 2 4 1 34 2 3 4887438036430154 (4)A>
== Executing PPA-CTR 24 (once), V(1)=887438036430151, V(2)=3
5324628218580928 4725277[16]3722546 887438036430122 2 4 1 35 2 3887438036430154 4 (4)A>
== Executing PA-CTR 23, V(1)=0, V(2)=887438036430151, repcount=443719018215076, factor=3/2
7986942327871384 1063187[17]6930634 1331157054645198 2 4 1 35 2 32 41331157054645229 (4)A>
7986942327871385 1063187[17]6930635 1331157054645199 2 4 1 35 2 32 41331157054645230 (1)B>
7986942327871386 1063187[17]6930637 1331157054645197 2 4 1 35 2 32 41331157054645230 <A(2)
7986942327871387 1063187[17]1575867 -33 2 4 1 35 2 32 <A(2) 21331157054645230
7986942327871388 1063187[17]1575868 -34 2 4 1 35 2 3 <B(1) 21331157054645231
7986942327871389 1063187[17]1575872 -32 2 4 1 35 2 4 (4)A> 21331157054645231
7986942327871390 1063187[17]6221103 1331157054645199 2 4 1 35 2 41331157054645232 (4)A>
7986942327871391 1063187[17]6221104 1331157054645200 2 4 1 35 2 41331157054645233 (1)B>
7986942327871392 1063187[17]6221106 1331157054645198 2 4 1 35 2 41331157054645233 <A(2)
7986942327871393 1063187[17]0866339 -35 2 4 1 35 2 <A(2) 21331157054645233
7986942327871394 1063187[17]0866341 -33 2 4 1 35 4 (4)A> 21331157054645233
7986942327871395 1063187[17]5511574 1331157054645200 2 4 1 35 41331157054645234 (4)A>
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* 33+V(2) 2 32 41+V(1) (4)A>
1 1 1 [*]* [*]* [*]* 33+V(2) 2 32 42+V(1) (1)B>
2 3 -1 [*]* [*]* [*]* 33+V(2) 2 32 42+V(1) <A(2)
3 5+V(1) -3+-1*V(1) [*]* [*]* [*]* 33+V(2) 2 32 <A(2) 22+V(1)
4 6+V(1) -4+-1*V(1) [*]* [*]* [*]* 33+V(2) 2 3 <B(1) 23+V(1)
5 10+V(1) -2+-1*V(1) [*]* [*]* [*]* 33+V(2) 2 4 (4)A> 23+V(1)
6 13+2*V(1) 1 [*]* [*]* [*]* 33+V(2) 2 44+V(1) (4)A>
7 14+2*V(1) 2 [*]* [*]* [*]* 33+V(2) 2 45+V(1) (1)B>
8 16+2*V(1) 0 [*]* [*]* [*]* 33+V(2) 2 45+V(1) <A(2)
9 21+3*V(1) -5+-1*V(1) [*]* [*]* [*]* 33+V(2) 2 <A(2) 25+V(1)
10 23+3*V(1) -3+-1*V(1) [*]* [*]* [*]* 33+V(2) 4 (4)A> 25+V(1)
11 28+4*V(1) 2 [*]* [*]* [*]* 33+V(2) 46+V(1) (4)A>
<< Success! ==> defined new CTR 25 (PPA)
7986942327871395 1063187[17]5511574 1331157054645200 2 4 1 35 41331157054645234 (4)A>
== Executing PA-CTR 3, V(1)=1331157054645233, V(2)=2, repcount=2, factor=3/2
7986942327871407 1063187[17]4092538 1331157054645202 2 4 1 3 41331157054645240 (4)A>
7986942327871408 1063187[17]4092539 1331157054645203 2 4 1 3 41331157054645241 (1)B>
7986942327871409 1063187[17]4092541 1331157054645201 2 4 1 3 41331157054645241 <A(2)
7986942327871410 1063187[17]8737782 -40 2 4 1 3 <A(2) 21331157054645241
7986942327871411 1063187[17]8737783 -41 2 4 1 <B(1) 21331157054645242
7986942327871412 1063187[17]8737785 -39 2 4 2 (2)B> 21331157054645242
7986942327871413 1063187[17]8737786 -38 2 4 22 (3)B> 21331157054645241
7986942327871414 1063187[17]3383027 1331157054645203 2 4 22 31331157054645241 (3)B>
7986942327871415 1063187[17]3383029 1331157054645201 2 4 22 31331157054645241 <B(1)
7986942327871416 1063187[17]3383033 1331157054645203 2 4 22 31331157054645240 4 (4)A>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 [*]* [*]* 1 3 43+V(1) (4)A>
1 1 1 [*]* [*]* 1 3 44+V(1) (1)B>
2 3 -1 [*]* [*]* 1 3 44+V(1) <A(2)
3 7+V(1) -5+-1*V(1) [*]* [*]* 1 3 <A(2) 24+V(1)
4 8+V(1) -6+-1*V(1) [*]* [*]* 1 <B(1) 25+V(1)
5 10+V(1) -4+-1*V(1) [*]* [*]* 2 (2)B> 25+V(1)
6 11+V(1) -3+-1*V(1) [*]* [*]* 22 (3)B> 24+V(1)
7 15+2*V(1) 1 [*]* [*]* 22 34+V(1) (3)B>
8 17+2*V(1) -1 [*]* [*]* 22 34+V(1) <B(1)
9 21+2*V(1) 1 [*]* [*]* 22 33+V(1) 4 (4)A>
<< Success! ==> defined new CTR 26 (PPA)
7986942327871416 1063187[17]3383033 1331157054645203 2 4 22 31331157054645240 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=1331157054645237, repcount=665578527322619, factor=3/2
11980413491807130 2392171[17]3666706 1996735581967822 2 4 22 32 41996735581967858 (4)A>
11980413491807131 2392171[17]3666707 1996735581967823 2 4 22 32 41996735581967859 (1)B>
11980413491807132 2392171[17]3666709 1996735581967821 2 4 22 32 41996735581967859 <A(2)
11980413491807133 2392171[17]5634568 -38 2 4 22 32 <A(2) 21996735581967859
11980413491807134 2392171[17]5634569 -39 2 4 22 3 <B(1) 21996735581967860
11980413491807135 2392171[17]5634573 -37 2 4 22 4 (4)A> 21996735581967860
11980413491807136 2392171[17]7602433 1996735581967823 2 4 22 41996735581967861 (4)A>
11980413491807137 2392171[17]7602434 1996735581967824 2 4 22 41996735581967862 (1)B>
11980413491807138 2392171[17]7602436 1996735581967822 2 4 22 41996735581967862 <A(2)
11980413491807139 2392171[17]9570298 -40 2 4 22 <A(2) 21996735581967862
11980413491807140 2392171[17]9570300 -38 2 4 2 4 (4)A> 21996735581967862
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* 22+V(1) 4 (4)A> 21+V(2)
1 1+V(2) 1+V(2) [*]* [*]* 22+V(1) 42+V(2) (4)A>
2 2+V(2) 2+V(2) [*]* [*]* 22+V(1) 43+V(2) (1)B>
3 4+V(2) 0+V(2) [*]* [*]* 22+V(1) 43+V(2) <A(2)
4 7+2*V(2) -3 [*]* [*]* 22+V(1) <A(2) 23+V(2)
5 9+2*V(2) -1 [*]* [*]* 21+V(1) 4 (4)A> 23+V(2)
<< Success! ==> defined new CTR 27 (PA)
11980413491807141 2392171[17]1538162 1996735581967824 2 4 2 41996735581967863 (4)A>
11980413491807142 2392171[17]1538163 1996735581967825 2 4 2 41996735581967864 (1)B>
11980413491807143 2392171[17]1538165 1996735581967823 2 4 2 41996735581967864 <A(2)
11980413491807144 2392171[17]3506029 -41 2 4 2 <A(2) 21996735581967864
11980413491807145 2392171[17]3506031 -39 2 42 (4)A> 21996735581967864
11980413491807146 2392171[17]5473895 1996735581967825 2 41996735581967866 (4)A>
11980413491807147 2392171[17]5473896 1996735581967826 2 41996735581967867 (1)B>
11980413491807148 2392171[17]5473898 1996735581967824 2 41996735581967867 <A(2)
11980413491807149 2392171[17]7441765 -43 2 <A(2) 21996735581967867
11980413491807150 2392171[17]7441767 -41 4 (4)A> 21996735581967867
11980413491807151 2392171[17]9409634 1996735581967826 41996735581967868 (4)A>
11980413491807152 2392171[17]9409635 1996735581967827 41996735581967869 (1)B>
11980413491807153 2392171[17]9409637 1996735581967825 41996735581967869 <A(2)
11980413491807154 2392171[17]1377506 -44 <A(2) 21996735581967869
11980413491807155 2392171[17]1377508 -42 1 (3)B> 21996735581967869
11980413491807156 2392171[17]3345377 1996735581967827 1 31996735581967869 (3)B>
11980413491807157 2392171[17]3345379 1996735581967825 1 31996735581967869 <B(1)
11980413491807158 2392171[17]3345383 1996735581967827 1 31996735581967868 4 (4)A>
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 2 41+V(2) 2 41+V(1) (4)A> 21+V(3)
1 1+V(3) 1+V(3) 2 41+V(2) 2 42+V(1)+V(3) (4)A>
2 2+V(3) 2+V(3) 2 41+V(2) 2 43+V(1)+V(3) (1)B>
3 4+V(3) 0+V(3) 2 41+V(2) 2 43+V(1)+V(3) <A(2)
4 7+V(1)+2*V(3) -3+-1*V(1) 2 41+V(2) 2 <A(2) 23+V(1)+V(3)
5 9+V(1)+2*V(3) -1+-1*V(1) 2 42+V(2) (4)A> 23+V(1)+V(3)
6 12+2*V(1)+3*V(3) 2+V(3) 2 45+V(1)+V(2)+V(3) (4)A>
7 13+2*V(1)+3*V(3) 3+V(3) 2 46+V(1)+V(2)+V(3) (1)B>
8 15+2*V(1)+3*V(3) 1+V(3) 2 46+V(1)+V(2)+V(3) <A(2)
9 21+3*V(1)+V(2)+4*V(3) -5+-1*V(1)+-1*V(2) 2 <A(2) 26+V(1)+V(2)+V(3)
10 23+3*V(1)+V(2)+4*V(3) -3+-1*V(1)+-1*V(2) 4 (4)A> 26+V(1)+V(2)+V(3)
11 29+4*V(1)+2*V(2)+5*V(3) 3+V(3) 47+V(1)+V(2)+V(3) (4)A>
12 30+4*V(1)+2*V(2)+5*V(3) 4+V(3) 48+V(1)+V(2)+V(3) (1)B>
13 32+4*V(1)+2*V(2)+5*V(3) 2+V(3) 48+V(1)+V(2)+V(3) <A(2)
14 40+5*V(1)+3*V(2)+6*V(3) -6+-1*V(1)+-1*V(2) <A(2) 28+V(1)+V(2)+V(3)
15 42+5*V(1)+3*V(2)+6*V(3) -4+-1*V(1)+-1*V(2) 1 (3)B> 28+V(1)+V(2)+V(3)
16 50+6*V(1)+4*V(2)+7*V(3) 4+V(3) 1 38+V(1)+V(2)+V(3) (3)B>
17 52+6*V(1)+4*V(2)+7*V(3) 2+V(3) 1 38+V(1)+V(2)+V(3) <B(1)
18 56+6*V(1)+4*V(2)+7*V(3) 4+V(3) 1 37+V(1)+V(2)+V(3) 4 (4)A>
<< Success! ==> defined new CTR 28 (PPA)
11980413491807158 2392171[17]3345383 1996735581967827 1 31996735581967868 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=1996735581967865, repcount=998367790983933, factor=3/2
17970620237710756 5382386[17]5630180 2995103372951760 1 32 42995103372951800 (4)A>
== Executing PPA-CTR 7 (once), V(1)=2995103372951799, V(2)=0
17970620237710770 5382386[17]7437412 2995103372951762 1 32995103372951804 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=2995103372951801, repcount=1497551686475901, factor=3/2
26955930356566176 1211036[18]3481825 4492655059427663 1 32 44492655059427704 (4)A>
== Executing PPA-CTR 7 (once), V(1)=4492655059427703, V(2)=0
26955930356566190 1211036[18]1192673 4492655059427665 1 34492655059427708 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=4492655059427705, repcount=2246327529713853, factor=3/2
40433895534849308 2724833[18]8648030 6738982589141518 1 32 46738982589141560 (4)A>
== Executing PPA-CTR 7 (once), V(1)=6738982589141559, V(2)=0
40433895534849322 2724833[18]5214302 6738982589141520 1 36738982589141564 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=6738982589141561, repcount=3369491294570781, factor=3/2
60650843302274008 6130874[18]7771995 10108473883712301 1 32 410108473883712344 (4)A>
== Executing PPA-CTR 7 (once), V(1)=10108473883712343, V(2)=0
60650843302274022 6130874[18]2621403 10108473883712303 1 310108473883712348 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=10108473883712345, repcount=5054236941856173, factor=3/2
90976264953411060 1379446[19]5800920 15162710825568476 1 32 415162710825568520 (4)A>
== Executing PPA-CTR 7 (once), V(1)=15162710825568519, V(2)=0
90976264953411074 1379446[19]8075032 15162710825568478 1 315162710825568524 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=15162710825568521, repcount=7581355412784261, factor=3/2
1364643[4]0116640 3103755[19]3866005 22744066238352739 1 32 422744066238352784 (4)A>
== Executing PPA-CTR 7 (once), V(1)=22744066238352783, V(2)=0
1364643[4]0116654 3103755[19]7277173 22744066238352741 1 322744066238352788 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=22744066238352785, repcount=11372033119176393, factor=3/2
2046965[4]5175012 6983449[19]4512450 34116099357529134 1 32 434116099357529180 (4)A>
== Executing PPA-CTR 7 (once), V(1)=34116099357529179, V(2)=0
2046965[4]5175026 6983449[19]4629202 34116099357529136 1 334116099357529184 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=34116099357529181, repcount=17058049678764591, factor=3/2
3070448[4]7762572 1571276[20]8466955 51174149036293727 1 32 451174149036293774 (4)A>
== Executing PPA-CTR 7 (once), V(1)=51174149036293773, V(2)=0
3070448[4]7762586 1571276[20]3642083 51174149036293729 1 351174149036293778 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=51174149036293775, repcount=25587074518146888, factor=3/2
4605673[4]6643914 3535371[20]7364595 76761223554440617 1 32 476761223554440665 (4)A>
== Executing PPA-CTR 7 (once), V(1)=76761223554440664, V(2)=0
4605673[4]6643928 3535371[20]5127287 76761223554440619 1 376761223554440669 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=76761223554440666, repcount=38380611777220334, factor=3/2
6908510[4]9965932 7954585[20]6545295 1151418[4]1660953 1 3 41151418[4]1661003 (4)A>
== Executing PPA-CTR 2 (once), V(1)=1151418[4]1661000
6908510[4]9965941 7954585[20]9867316 1151418[4]1660954 22 31151418[4]1661003 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=1151418[4]1661000, repcount=57570917665830501, factor=3/2
1036276[5]4948947 1789781[21]3905329 1727127[4]7491455 22 3 41727127[4]7491504 (4)A>
== Executing PPA-CTR 8 (once), V(1)=1727127[4]7491501, V(2)=0
1036276[5]4948956 1789781[21]8888352 1727127[4]7491456 2 3 2 31727127[4]7491504 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=1727127[4]7491501, repcount=86356376498745751, factor=3/2
1554414[5]7423462 4027008[21]8007865 2590691[4]6237207 2 3 2 32 42590691[4]6237254 (4)A>
== Executing PPA-CTR 11 (once), V(1)=2590691[4]6237253
1554414[5]7423482 4027008[21]5431438 2590691[4]6237210 3 2 32590691[4]6237259 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=2590691[4]6237256, repcount=1295345[4]8118629, factor=3/2
2331622[5]6135256 9060769[21]7136651 3886036[4]4355839 3 2 3 43886036[4]4355888 (4)A>
== Executing PPA-CTR 12 (once), V(1)=3886036[4]4355885, V(2)=0
2331622[5]6135265 9060769[21]5848442 3886036[4]4355840 32 2 33886036[4]4355888 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=3886036[4]4355885, repcount=1943018[4]2177943, factor=3/2
3497433[5]9202923 2038673[22]4761619 5829055[4]6533783 32 2 32 45829055[4]6533830 (4)A>
3497433[5]9202924 2038673[22]4761620 5829055[4]6533784 32 2 32 45829055[4]6533831 (1)B>
3497433[5]9202925 2038673[22]4761622 5829055[4]6533782 32 2 32 45829055[4]6533831 <A(2)
3497433[5]9202926 2038673[22]1295453 -49 32 2 32 <A(2) 25829055[4]6533831
3497433[5]9202927 2038673[22]1295454 -50 32 2 3 <B(1) 25829055[4]6533832
3497433[5]9202928 2038673[22]1295458 -48 32 2 4 (4)A> 25829055[4]6533832
3497433[5]9202929 2038673[22]7829290 5829055[4]6533784 32 2 45829055[4]6533833 (4)A>
3497433[5]9202930 2038673[22]7829291 5829055[4]6533785 32 2 45829055[4]6533834 (1)B>
3497433[5]9202931 2038673[22]7829293 5829055[4]6533783 32 2 45829055[4]6533834 <A(2)
3497433[5]9202932 2038673[22]4363127 -51 32 2 <A(2) 25829055[4]6533834
3497433[5]9202933 2038673[22]4363129 -49 32 4 (4)A> 25829055[4]6533834
3497433[5]9202934 2038673[22]0896963 5829055[4]6533785 32 45829055[4]6533835 (4)A>
3497433[5]9202935 2038673[22]0896964 5829055[4]6533786 32 45829055[4]6533836 (1)B>
3497433[5]9202936 2038673[22]0896966 5829055[4]6533784 32 45829055[4]6533836 <A(2)
3497433[5]9202937 2038673[22]7430802 -52 32 <A(2) 25829055[4]6533836
3497433[5]9202938 2038673[22]7430803 -53 3 <B(1) 25829055[4]6533837
3497433[5]9202939 2038673[22]7430807 -51 4 (4)A> 25829055[4]6533837
3497433[5]9202940 2038673[22]3964644 5829055[4]6533786 45829055[4]6533838 (4)A>
3497433[5]9202941 2038673[22]3964645 5829055[4]6533787 45829055[4]6533839 (1)B>
3497433[5]9202942 2038673[22]3964647 5829055[4]6533785 45829055[4]6533839 <A(2)
3497433[5]9202943 2038673[22]0498486 -54 <A(2) 25829055[4]6533839
3497433[5]9202944 2038673[22]0498488 -52 1 (3)B> 25829055[4]6533839
3497433[5]9202945 2038673[22]7032327 5829055[4]6533787 1 35829055[4]6533839 (3)B>
3497433[5]9202946 2038673[22]7032329 5829055[4]6533785 1 35829055[4]6533839 <B(1)
3497433[5]9202947 2038673[22]7032333 5829055[4]6533787 1 35829055[4]6533838 4 (4)A>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 32 2 32 41+V(1) (4)A>
1 1 1 32 2 32 42+V(1) (1)B>
2 3 -1 32 2 32 42+V(1) <A(2)
3 5+V(1) -3+-1*V(1) 32 2 32 <A(2) 22+V(1)
4 6+V(1) -4+-1*V(1) 32 2 3 <B(1) 23+V(1)
5 10+V(1) -2+-1*V(1) 32 2 4 (4)A> 23+V(1)
6 13+2*V(1) 1 32 2 44+V(1) (4)A>
7 14+2*V(1) 2 32 2 45+V(1) (1)B>
8 16+2*V(1) 0 32 2 45+V(1) <A(2)
9 21+3*V(1) -5+-1*V(1) 32 2 <A(2) 25+V(1)
10 23+3*V(1) -3+-1*V(1) 32 4 (4)A> 25+V(1)
11 28+4*V(1) 2 32 46+V(1) (4)A>
12 29+4*V(1) 3 32 47+V(1) (1)B>
13 31+4*V(1) 1 32 47+V(1) <A(2)
14 38+5*V(1) -6+-1*V(1) 32 <A(2) 27+V(1)
15 39+5*V(1) -7+-1*V(1) 3 <B(1) 28+V(1)
16 43+5*V(1) -5+-1*V(1) 4 (4)A> 28+V(1)
17 51+6*V(1) 3 49+V(1) (4)A>
18 52+6*V(1) 4 410+V(1) (1)B>
19 54+6*V(1) 2 410+V(1) <A(2)
20 64+7*V(1) -8+-1*V(1) <A(2) 210+V(1)
21 66+7*V(1) -6+-1*V(1) 1 (3)B> 210+V(1)
22 76+8*V(1) 4 1 310+V(1) (3)B>
23 78+8*V(1) 2 1 310+V(1) <B(1)
24 82+8*V(1) 4 1 39+V(1) 4 (4)A>
<< Success! ==> defined new CTR 29 (PPA)
3497433[5]9202947 2038673[22]7032333 5829055[4]6533787 1 35829055[4]6533838 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=5829055[4]6533835, repcount=2914527[4]3266918, factor=3/2
5246149[5]8804455 4587014[22]9357685 8743583[4]9800705 1 32 48743583[4]9800755 (4)A>
== Executing PPA-CTR 7 (once), V(1)=8743583[4]9800754, V(2)=0
5246149[5]8804469 4587014[22]8560737 8743583[4]9800707 1 38743583[4]9800759 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=8743583[4]9800756, repcount=4371791[4]4900379, factor=3/2
7869224[5]8206743 1032078[23]0595450 1311537[5]4701086 1 3 41311537[5]4701138 (4)A>
== Executing PPA-CTR 2 (once), V(1)=1311537[5]4701135
7869224[5]8206752 1032078[23]9997741 1311537[5]4701087 22 31311537[5]4701138 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=1311537[5]4701135, repcount=6557687[4]7350568, factor=3/2
1180383[6]2310160 2322176[23]3271293 1967306[5]2051655 22 32 41967306[5]2051705 (4)A>
== Executing PPA-CTR 17 (once), V(1)=1967306[5]2051704, V(2)=0
1180383[6]2310165 2322176[23]5323007 -51 22 4 (4)A> 21967306[5]2051707
== Executing PA-CTR 15, V(1)=0, V(2)=1967306[5]2051706, repcount=1, factor=2/1
1180383[6]2310170 2322176[23]9426428 -52 2 4 (4)A> 21967306[5]2051709
== Executing PPA-CTR 16 (once), V(1)=0, V(2)=1967306[5]2051708
1180383[6]2310183 2322176[23]9685001 1967306[5]2051659 1 31967306[5]2051712 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=1967306[5]2051709, repcount=9836531[4]6025855, factor=3/2
1770575[6]8465313 5224896[23]5386626 2950959[5]8077514 1 32 42950959[5]8077566 (4)A>
== Executing PPA-CTR 7 (once), V(1)=2950959[5]8077565, V(2)=0
1770575[6]8465327 5224896[23]7696922 2950959[5]8077516 1 32950959[5]8077570 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=2950959[5]8077567, repcount=1475479[5]4038784, factor=3/2
2655863[6]2698031 1175601[24]6680730 4426438[5]2116300 1 32 44426438[5]2116353 (4)A>
== Executing PPA-CTR 7 (once), V(1)=4426438[5]2116352, V(2)=0
2655863[6]2698045 1175601[24]5146174 4426438[5]2116302 1 34426438[5]2116357 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=4426438[5]2116354, repcount=2213219[5]6058178, factor=3/2
3983795[6]9047113 2645103[24]7767006 6639658[5]8174480 1 3 46639658[5]8174535 (4)A>
== Executing PPA-CTR 2 (once), V(1)=6639658[5]8174532
3983795[6]9047122 2645103[24]4116091 6639658[5]8174481 22 36639658[5]8174535 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=6639658[5]8174532, repcount=3319829[5]4087267, factor=3/2
5975692[6]3570724 5951483[24]9576628 9959487[5]2261748 22 3 49959487[5]2261802 (4)A>
== Executing PPA-CTR 8 (once), V(1)=9959487[5]2261799, V(2)=0
5975692[6]3570733 5951483[24]4100247 9959487[5]2261749 2 3 2 39959487[5]2261802 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=9959487[5]2261799, repcount=4979743[5]6130900, factor=3/2
8963538[6]0356133 1339083[25]9839247 1493923[6]8392649 2 3 2 32 41493923[6]8392701 (4)A>
== Executing PPA-CTR 11 (once), V(1)=1493923[6]8392700
8963538[6]0356153 1339083[25]0195502 1493923[6]8392652 3 2 31493923[6]8392706 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=1493923[6]8392703, repcount=7469615[5]4196352, factor=3/2
1344530[7]5534265 3012938[25]2482734 2240884[6]2589004 3 2 32 42240884[6]2589057 (4)A>
== Executing PPA-CTR 22 (once), V(1)=2240884[6]2589056
1344530[7]5534291 3012938[25]8017137 2240884[6]2589007 2 4 1 2 32240884[6]2589062 4 (4)A>
== Executing PA-CTR 5, V(1)=0, V(2)=2240884[6]2589059, repcount=1120442[6]6294530, factor=3/2
2016796[7]3301471 6779111[25]4725137 3361327[6]8883537 2 4 1 2 32 43361327[6]8883591 (4)A>
== Executing PPA-CTR 6 (once), V(1)=3361327[6]8883590, V(2)=0, V(3)=0
2016796[7]3301496 6779111[25]5793941 3361327[6]8883541 1 33361327[6]8883600 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=3361327[6]8883597, repcount=1680663[6]4441799, factor=3/2
3025194[7]9952290 1525300[26]5281134 5041990[6]3325340 1 32 45041990[6]3325398 (4)A>
== Executing PPA-CTR 7 (once), V(1)=5041990[6]3325397, V(2)=0
3025194[7]9952304 1525300[26]8582758 5041990[6]3325342 1 35041990[6]3325402 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=5041990[6]3325399, repcount=2520995[6]6662700, factor=3/2
4537791[7]9928504 3431925[26]9079758 7562985[6]9988042 1 32 47562985[6]9988101 (4)A>
== Executing PPA-CTR 7 (once), V(1)=7562985[6]9988100, V(2)=0
4537791[7]9928518 3431925[26]9032194 7562985[6]9988044 1 37562985[6]9988105 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=7562985[6]9988102, repcount=3781492[6]9994052, factor=3/2
6806687[7]9892830 7721832[26]5108826 1134447[7]9982096 1 3 41134447[7]9982157 (4)A>
== Executing PPA-CTR 2 (once), V(1)=1134447[7]9982154
6806687[7]9892839 7721832[26]5073155 1134447[7]9982097 22 31134447[7]9982157 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=1134447[7]9982154, repcount=5672239[6]4991078, factor=3/2
1021003[8]9839307 1737412[27]3790187 1701671[7]4973175 22 3 41701671[7]4973235 (4)A>
== Executing PPA-CTR 8 (once), V(1)=1701671[7]4973232, V(2)=0
1021003[8]9839316 1737412[27]3736672 1701671[7]4973176 2 3 2 31701671[7]4973235 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=1701671[7]4973232, repcount=8508359[6]7486617, factor=3/2
1531504[8]4759018 3909177[27]0916909 2552507[7]2459793 2 3 2 3 42552507[7]2459852 (4)A>
== Executing PPA-CTR 9 (once), V(1)=2552507[7]2459849, V(2)=0
1531504[8]4759027 3909177[27]5836628 2552507[7]2459794 2 32 2 32552507[7]2459852 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=2552507[7]2459849, repcount=1276253[7]6229925, factor=3/2
2297256[8]2138577 8795649[27]4652753 3828761[7]8689719 2 32 2 32 43828761[7]8689776 (4)A>
== Executing PPA-CTR 10 (once), V(1)=3828761[7]8689775
2297256[8]2138606 8795649[27]1550614 3828761[7]8689724 1 33828761[7]8689786 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=3828761[7]8689783, repcount=1914380[7]4344892, factor=3/2
3445885[8]8207958 1979021[28]4474526 5743142[7]3034616 1 32 45743142[7]3034677 (4)A>
== Executing PPA-CTR 7 (once), V(1)=5743142[7]3034676, V(2)=0
3445885[8]8207972 1979021[28]6613266 5743142[7]3034618 1 35743142[7]3034681 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=5743142[7]3034678, repcount=2871571[7]6517340, factor=3/2
5168828[8]7312012 4452797[28]3813466 8614713[7]9551958 1 3 48614713[7]9552021 (4)A>
== Executing PPA-CTR 2 (once), V(1)=8614713[7]9552018
5168828[8]7312021 4452797[28]2917523 8614713[7]9551959 22 38614713[7]9552021 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=8614713[7]9552018, repcount=4307356[7]9776010, factor=3/2
7753242[8]5968081 1001879[29]5237923 1292207[8]9327969 22 3 41292207[8]9328031 (4)A>
== Executing PPA-CTR 8 (once), V(1)=1292207[8]9328028, V(2)=0
7753242[8]5968090 1001879[29]3894000 1292207[8]9327970 2 3 2 31292207[8]9328031 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=1292207[8]9328028, repcount=6461035[7]9664015, factor=3/2
1162986[9]3952180 2254228[29]8294825 1938310[8]8991985 2 3 2 3 41938310[8]8992046 (4)A>
== Executing PPA-CTR 9 (once), V(1)=1938310[8]8992043, V(2)=0
1162986[9]3952189 2254228[29]6278932 1938310[8]8991986 2 32 2 31938310[8]8992046 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=1938310[8]8992043, repcount=9691552[7]4496022, factor=3/2
1744479[9]0928321 5072014[29]2712604 2907465[8]3488008 2 32 2 32 42907465[8]3488067 (4)A>
== Executing PPA-CTR 10 (once), V(1)=2907465[8]3488066
1744479[9]0928350 5072014[29]7593375 2907465[8]3488013 1 32907465[8]3488077 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=2907465[8]3488074, repcount=1453732[8]1744038, factor=3/2
2616719[9]1392578 1141203[30]0670087 4361198[8]5232051 1 3 44361198[8]5232115 (4)A>
== Executing PPA-CTR 2 (once), V(1)=4361198[8]5232112
2616719[9]1392587 1141203[30]1134332 4361198[8]5232052 22 34361198[8]5232115 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=4361198[8]5232112, repcount=2180599[8]2616057, factor=3/2
3925078[9]7088929 2567707[30]9976649 6541798[8]7848109 22 3 46541798[8]7848172 (4)A>
== Executing PPA-CTR 8 (once), V(1)=6541798[8]7848169, V(2)=0
3925078[9]7088938 2567707[30]5673008 6541798[8]7848110 2 3 2 36541798[8]7848172 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=6541798[8]7848169, repcount=3270899[8]8924085, factor=3/2
5887618[9]0633448 5777341[30]4175533 9812697[8]6772195 2 3 2 32 49812697[8]6772256 (4)A>
== Executing PPA-CTR 11 (once), V(1)=9812697[8]6772255
5887618[9]0633468 5777341[30]4809118 9812697[8]6772198 3 2 39812697[8]6772261 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=9812697[8]6772258, repcount=4906348[8]3386130, factor=3/2
8831427[9]0950248 1299901[31]7801118 1471904[9]0158328 3 2 3 41471904[9]0158391 (4)A>
== Executing PPA-CTR 12 (once), V(1)=1471904[9]0158388, V(2)=0
8831427[9]0950257 1299901[31]8117915 1471904[9]0158329 32 2 31471904[9]0158391 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=1471904[9]0158388, repcount=7359522[8]5079195, factor=3/2
1324714[10]1425427 2924779[31]4453940 2207856[9]5237524 32 2 3 42207856[9]5237586 (4)A>
== Executing PPA-CTR 12 (once), V(1)=2207856[9]5237583, V(2)=1
1324714[10]1425436 2924779[31]4929127 2207856[9]5237525 33 2 32207856[9]5237586 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=2207856[9]5237583, repcount=1103928[9]7618792, factor=3/2
1987071[10]7138188 6580753[31]5734839 3311785[9]2856317 33 2 32 43311785[9]2856377 (4)A>
== Executing PPA-CTR 20 (once), V(1)=3311785[9]2856376, V(2)=0
1987071[10]7138198 6580753[31]4303990 -62 33 4 (4)A> 23311785[9]2856381
== Executing PA-CTR 13, V(1)=0, V(2)=3311785[9]2856380, repcount=1, factor=3/2
1987071[10]7138204 6580753[31]0016762 -64 3 4 (4)A> 23311785[9]2856384
== Executing PPA-CTR 21 (once), V(1)=0, V(2)=3311785[9]2856382
1987071[10]7138220 6580753[31]8585943 3311785[9]2856321 2 4 1 2 33311785[9]2856385 4 (4)A>
== Executing PA-CTR 5, V(1)=0, V(2)=3311785[9]2856382, repcount=1655892[9]6428192, factor=3/2
2980606[10]5707372 1480669[32]0034455 4967677[9]9284513 2 4 1 2 3 44967677[9]9284577 (4)A>
2980606[10]5707373 1480669[32]0034456 4967677[9]9284514 2 4 1 2 3 44967677[9]9284578 (1)B>
2980606[10]5707374 1480669[32]0034458 4967677[9]9284512 2 4 1 2 3 44967677[9]9284578 <A(2)
2980606[10]5707375 1480669[32]9319036 -66 2 4 1 2 3 <A(2) 24967677[9]9284578
2980606[10]5707376 1480669[32]9319037 -67 2 4 1 2 <B(1) 24967677[9]9284579
2980606[10]5707377 1480669[32]9319039 -65 2 4 1 3 (2)B> 24967677[9]9284579
2980606[10]5707378 1480669[32]9319040 -64 2 4 1 3 2 (3)B> 24967677[9]9284578
2980606[10]5707379 1480669[32]8603618 4967677[9]9284514 2 4 1 3 2 34967677[9]9284578 (3)B>
2980606[10]5707380 1480669[32]8603620 4967677[9]9284512 2 4 1 3 2 34967677[9]9284578 <B(1)
2980606[10]5707381 1480669[32]8603624 4967677[9]9284514 2 4 1 3 2 34967677[9]9284577 4 (4)A>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 [*]* [*]* [*]* 2 3 43+V(1) (4)A>
1 1 1 [*]* [*]* [*]* 2 3 44+V(1) (1)B>
2 3 -1 [*]* [*]* [*]* 2 3 44+V(1) <A(2)
3 7+V(1) -5+-1*V(1) [*]* [*]* [*]* 2 3 <A(2) 24+V(1)
4 8+V(1) -6+-1*V(1) [*]* [*]* [*]* 2 <B(1) 25+V(1)
5 10+V(1) -4+-1*V(1) [*]* [*]* [*]* 3 (2)B> 25+V(1)
6 11+V(1) -3+-1*V(1) [*]* [*]* [*]* 3 2 (3)B> 24+V(1)
7 15+2*V(1) 1 [*]* [*]* [*]* 3 2 34+V(1) (3)B>
8 17+2*V(1) -1 [*]* [*]* [*]* 3 2 34+V(1) <B(1)
9 21+2*V(1) 1 [*]* [*]* [*]* 3 2 33+V(1) 4 (4)A>
<< Success! ==> defined new CTR 30 (PPA)
2980606[10]5707381 1480669[32]8603624 4967677[9]9284514 2 4 1 3 2 34967677[9]9284577 4 (4)A>
== Executing PA-CTR 23, V(1)=0, V(2)=4967677[9]9284574, repcount=2483838[9]4642288, factor=3/2
4470910[10]3561109 3331506[32]8651336 7451516[9]3926802 2 4 1 3 2 3 47451516[9]3926865 (4)A>
== Executing PPA-CTR 24 (once), V(1)=7451516[9]3926862, V(2)=0
4470910[10]3561118 3331506[32]6505081 7451516[9]3926803 2 4 1 32 2 37451516[9]3926865 4 (4)A>
== Executing PA-CTR 23, V(1)=0, V(2)=7451516[9]3926862, repcount=3725758[9]1963432, factor=3/2
6706365[10]5341710 7495889[32]1795273 1117727[10]5890235 2 4 1 32 2 3 41117727[10]5890297 (4)A>
== Executing PPA-CTR 24 (once), V(1)=1117727[10]5890294, V(2)=1
6706365[10]5341719 7495889[32]3575882 1117727[10]5890236 2 4 1 33 2 31117727[10]5890297 4 (4)A>
== Executing PA-CTR 23, V(1)=0, V(2)=1117727[10]5890294, repcount=5588637[9]7945148, factor=3/2
1005954[11]3012607 1686575[33]3253074 1676591[10]3835384 2 4 1 33 2 3 41676591[10]3835445 (4)A>
== Executing PPA-CTR 24 (once), V(1)=1676591[10]3835442, V(2)=2
1005954[11]3012616 1686575[33]0923979 1676591[10]3835385 2 4 1 34 2 31676591[10]3835445 4 (4)A>
== Executing PA-CTR 23, V(1)=0, V(2)=1676591[10]3835442, repcount=8382956[9]6917722, factor=3/2
1508932[11]4518948 3794793[33]3109051 2514886[10]0753107 2 4 1 34 2 3 42514886[10]0753167 (4)A>
== Executing PPA-CTR 24 (once), V(1)=2514886[10]0753164, V(2)=3
1508932[11]4518957 3794793[33]4615400 2514886[10]0753108 2 4 1 35 2 32514886[10]0753167 4 (4)A>
== Executing PA-CTR 23, V(1)=0, V(2)=2514886[10]0753164, repcount=1257443[10]0376583, factor=3/2
2263398[11]6778455 8538286[33]2648897 3772330[10]1129691 2 4 1 35 2 3 43772330[10]1129750 (4)A>
== Executing PPA-CTR 24 (once), V(1)=3772330[10]1129747, V(2)=4
2263398[11]6778464 8538286[33]4908412 3772330[10]1129692 2 4 1 36 2 33772330[10]1129750 4 (4)A>
== Executing PA-CTR 23, V(1)=0, V(2)=3772330[10]1129747, repcount=1886165[10]0564874, factor=3/2
3395097[11]0167708 1921114[34]8464780 5658495[10]1694566 2 4 1 36 2 32 45658495[10]1694623 (4)A>
== Executing PPA-CTR 25 (once), V(1)=5658495[10]1694622, V(2)=3
3395097[11]0167719 1921114[34]5243296 5658495[10]1694568 2 4 1 36 45658495[10]1694628 (4)A>
== Executing PA-CTR 3, V(1)=5658495[10]1694627, V(2)=3, repcount=2, factor=3/2
3395097[11]0167731 1921114[34]2021836 5658495[10]1694570 2 4 1 32 45658495[10]1694634 (4)A>
3395097[11]0167732 1921114[34]2021837 5658495[10]1694571 2 4 1 32 45658495[10]1694635 (1)B>
3395097[11]0167733 1921114[34]2021839 5658495[10]1694569 2 4 1 32 45658495[10]1694635 <A(2)
3395097[11]0167734 1921114[34]3716474 -66 2 4 1 32 <A(2) 25658495[10]1694635
3395097[11]0167735 1921114[34]3716475 -67 2 4 1 3 <B(1) 25658495[10]1694636
3395097[11]0167736 1921114[34]3716479 -65 2 4 1 4 (4)A> 25658495[10]1694636
3395097[11]0167737 1921114[34]5411115 5658495[10]1694571 2 4 1 45658495[10]1694637 (4)A>
3395097[11]0167738 1921114[34]5411116 5658495[10]1694572 2 4 1 45658495[10]1694638 (1)B>
3395097[11]0167739 1921114[34]5411118 5658495[10]1694570 2 4 1 45658495[10]1694638 <A(2)
3395097[11]0167740 1921114[34]7105756 -68 2 4 1 <A(2) 25658495[10]1694638
3395097[11]0167741 1921114[34]7105757 -69 2 4 <A(2) 25658495[10]1694639
3395097[11]0167742 1921114[34]7105758 -70 2 <A(2) 25658495[10]1694640
3395097[11]0167743 1921114[34]7105760 -68 4 (4)A> 25658495[10]1694640
3395097[11]0167744 1921114[34]8800400 5658495[10]1694572 45658495[10]1694641 (4)A>
3395097[11]0167745 1921114[34]8800401 5658495[10]1694573 45658495[10]1694642 (1)B>
3395097[11]0167746 1921114[34]8800403 5658495[10]1694571 45658495[10]1694642 <A(2)
3395097[11]0167747 1921114[34]0495045 -71 <A(2) 25658495[10]1694642
3395097[11]0167748 1921114[34]0495047 -69 1 (3)B> 25658495[10]1694642
3395097[11]0167749 1921114[34]2189689 5658495[10]1694573 1 35658495[10]1694642 (3)B>
3395097[11]0167750 1921114[34]2189691 5658495[10]1694571 1 35658495[10]1694642 <B(1)
3395097[11]0167751 1921114[34]2189695 5658495[10]1694573 1 35658495[10]1694641 4 (4)A>
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 2 41+V(3) 11+V(2) 32 41+V(1) (4)A>
1 1 1 2 41+V(3) 11+V(2) 32 42+V(1) (1)B>
2 3 -1 2 41+V(3) 11+V(2) 32 42+V(1) <A(2)
3 5+V(1) -3+-1*V(1) 2 41+V(3) 11+V(2) 32 <A(2) 22+V(1)
4 6+V(1) -4+-1*V(1) 2 41+V(3) 11+V(2) 3 <B(1) 23+V(1)
5 10+V(1) -2+-1*V(1) 2 41+V(3) 11+V(2) 4 (4)A> 23+V(1)
6 13+2*V(1) 1 2 41+V(3) 11+V(2) 44+V(1) (4)A>
7 14+2*V(1) 2 2 41+V(3) 11+V(2) 45+V(1) (1)B>
8 16+2*V(1) 0 2 41+V(3) 11+V(2) 45+V(1) <A(2)
9 21+3*V(1) -5+-1*V(1) 2 41+V(3) 11+V(2) <A(2) 25+V(1)
10 22+3*V(1)+V(2) -6+-1*V(1)+-1*V(2) 2 41+V(3) <A(2) 26+V(1)+V(2)
11 23+3*V(1)+V(2)+V(3) -7+-1*V(1)+-1*V(2)+-1*V(3) 2 <A(2) 27+V(1)+V(2)+V(3)
12 25+3*V(1)+V(2)+V(3) -5+-1*V(1)+-1*V(2)+-1*V(3) 4 (4)A> 27+V(1)+V(2)+V(3)
13 32+4*V(1)+2*V(2)+2*V(3) 2 48+V(1)+V(2)+V(3) (4)A>
14 33+4*V(1)+2*V(2)+2*V(3) 3 49+V(1)+V(2)+V(3) (1)B>
15 35+4*V(1)+2*V(2)+2*V(3) 1 49+V(1)+V(2)+V(3) <A(2)
16 44+5*V(1)+3*V(2)+3*V(3) -8+-1*V(1)+-1*V(2)+-1*V(3) <A(2) 29+V(1)+V(2)+V(3)
17 46+5*V(1)+3*V(2)+3*V(3) -6+-1*V(1)+-1*V(2)+-1*V(3) 1 (3)B> 29+V(1)+V(2)+V(3)
18 55+6*V(1)+4*V(2)+4*V(3) 3 1 39+V(1)+V(2)+V(3) (3)B>
19 57+6*V(1)+4*V(2)+4*V(3) 1 1 39+V(1)+V(2)+V(3) <B(1)
20 61+6*V(1)+4*V(2)+4*V(3) 3 1 38+V(1)+V(2)+V(3) 4 (4)A>
<< Success! ==> defined new CTR 31 (PPA)
3395097[11]0167751 1921114[34]2189695 5658495[10]1694573 1 35658495[10]1694641 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=5658495[10]1694638, repcount=2829247[10]5847320, factor=3/2
5092646[11]5251671 4322507[34]4210095 8487743[10]7541893 1 3 48487743[10]7541961 (4)A>
== Executing PPA-CTR 2 (once), V(1)=8487743[10]7541958
5092646[11]5251680 4322507[34]9294032 8487743[10]7541894 22 38487743[10]7541961 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=8487743[10]7541958, repcount=4243871[10]3770980, factor=3/2
7638969[11]7877560 9725641[34]7485032 1273161[11]1312874 22 3 41273161[11]1312941 (4)A>
== Executing PPA-CTR 8 (once), V(1)=1273161[11]1312938, V(2)=0
7638969[11]7877569 9725641[34]0110929 1273161[11]1312875 2 3 2 31273161[11]1312941 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=1273161[11]1312938, repcount=6365807[10]0656470, factor=3/2
1145845[12]1816389 2188269[35]5258329 1909742[11]1969345 2 3 2 3 41909742[11]1969411 (4)A>
== Executing PPA-CTR 9 (once), V(1)=1909742[11]1969408, V(2)=0
1145845[12]1816398 2188269[35]9197166 1909742[11]1969346 2 32 2 31909742[11]1969411 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=1909742[11]1969408, repcount=9548711[10]0984705, factor=3/2
1718768[12]7724628 4923606[35]0855291 2864613[11]2954051 2 32 2 3 42864613[11]2954116 (4)A>
== Executing PPA-CTR 9 (once), V(1)=2864613[11]2954113, V(2)=1
1718768[12]7724637 4923606[35]6763538 2864613[11]2954052 2 33 2 32864613[11]2954116 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=2864613[11]2954113, repcount=1432306[11]6477057, factor=3/2
2578152[12]6586979 1107811[36]3677855 4296920[11]9431109 2 33 2 32 44296920[11]9431172 (4)A>
== Executing PPA-CTR 18 (once), V(1)=4296920[11]9431171, V(2)=0
2578152[12]6586990 1107811[36]1402567 4296920[11]9431111 2 33 44296920[11]9431177 (4)A>
== Executing PA-CTR 1, V(1)=4296920[11]9431176, V(2)=0, repcount=1, factor=3/2
2578152[12]6586996 1107811[36]0264932 4296920[11]9431112 2 3 44296920[11]9431180 (4)A>
== Executing PPA-CTR 19 (once), V(1)=4296920[11]9431177
2578152[12]6587005 1107811[36]9127307 4296920[11]9431113 3 2 34296920[11]9431180 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=4296920[11]9431177, repcount=2148460[11]9715589, factor=3/2
3867228[12]4880539 2492575[36]5133960 6445380[11]9146702 3 2 32 46445380[11]9146768 (4)A>
== Executing PPA-CTR 22 (once), V(1)=6445380[11]9146767
3867228[12]4880565 2492575[36]0014629 6445380[11]9146705 2 4 1 2 36445380[11]9146773 4 (4)A>
== Executing PA-CTR 5, V(1)=0, V(2)=6445380[11]9146770, repcount=3222690[11]9573386, factor=3/2
5800842[12]2320881 5608295[36]4263477 9668070[11]8720091 2 4 1 2 3 49668070[11]8720159 (4)A>
== Executing PPA-CTR 30 (once), V(1)=9668070[11]8720156
5800842[12]2320890 5608295[36]1703810 9668070[11]8720092 2 4 1 3 2 39668070[11]8720159 4 (4)A>
== Executing PA-CTR 23, V(1)=0, V(2)=9668070[11]8720156, repcount=4834035[11]4360079, factor=3/2
8701263[12]8481364 1261866[37]1963323 1450210[12]3080171 2 4 1 3 2 3 41450210[12]3080238 (4)A>
== Executing PPA-CTR 24 (once), V(1)=1450210[12]3080235, V(2)=0
8701263[12]8481373 1261866[37]8123814 1450210[12]3080172 2 4 1 32 2 31450210[12]3080238 4 (4)A>
== Executing PA-CTR 23, V(1)=0, V(2)=1450210[12]3080235, repcount=7251052[11]6540118, factor=3/2
1305189[13]7722081 2839199[37]3886766 2175315[12]9620290 2 4 1 32 2 32 42175315[12]9620355 (4)A>
1305189[13]7722082 2839199[37]3886767 2175315[12]9620291 2 4 1 32 2 32 42175315[12]9620356 (1)B>
1305189[13]7722083 2839199[37]3886769 2175315[12]9620289 2 4 1 32 2 32 42175315[12]9620356 <A(2)
1305189[13]7722084 2839199[37]3507125 -67 2 4 1 32 2 32 <A(2) 22175315[12]9620356
1305189[13]7722085 2839199[37]3507126 -68 2 4 1 32 2 3 <B(1) 22175315[12]9620357
1305189[13]7722086 2839199[37]3507130 -66 2 4 1 32 2 4 (4)A> 22175315[12]9620357
1305189[13]7722087 2839199[37]3127487 2175315[12]9620291 2 4 1 32 2 42175315[12]9620358 (4)A>
1305189[13]7722088 2839199[37]3127488 2175315[12]9620292 2 4 1 32 2 42175315[12]9620359 (1)B>
1305189[13]7722089 2839199[37]3127490 2175315[12]9620290 2 4 1 32 2 42175315[12]9620359 <A(2)
1305189[13]7722090 2839199[37]2747849 -69 2 4 1 32 2 <A(2) 22175315[12]9620359
1305189[13]7722091 2839199[37]2747851 -67 2 4 1 32 4 (4)A> 22175315[12]9620359
1305189[13]7722092 2839199[37]2368210 2175315[12]9620292 2 4 1 32 42175315[12]9620360 (4)A>
1305189[13]7722093 2839199[37]2368211 2175315[12]9620293 2 4 1 32 42175315[12]9620361 (1)B>
1305189[13]7722094 2839199[37]2368213 2175315[12]9620291 2 4 1 32 42175315[12]9620361 <A(2)
1305189[13]7722095 2839199[37]1988574 -70 2 4 1 32 <A(2) 22175315[12]9620361
1305189[13]7722096 2839199[37]1988575 -71 2 4 1 3 <B(1) 22175315[12]9620362
1305189[13]7722097 2839199[37]1988579 -69 2 4 1 4 (4)A> 22175315[12]9620362
1305189[13]7722098 2839199[37]1608941 2175315[12]9620293 2 4 1 42175315[12]9620363 (4)A>
1305189[13]7722099 2839199[37]1608942 2175315[12]9620294 2 4 1 42175315[12]9620364 (1)B>
1305189[13]7722100 2839199[37]1608944 2175315[12]9620292 2 4 1 42175315[12]9620364 <A(2)
1305189[13]7722101 2839199[37]1229308 -72 2 4 1 <A(2) 22175315[12]9620364
1305189[13]7722102 2839199[37]1229309 -73 2 4 <A(2) 22175315[12]9620365
1305189[13]7722103 2839199[37]1229310 -74 2 <A(2) 22175315[12]9620366
1305189[13]7722104 2839199[37]1229312 -72 4 (4)A> 22175315[12]9620366
1305189[13]7722105 2839199[37]0849678 2175315[12]9620294 42175315[12]9620367 (4)A>
1305189[13]7722106 2839199[37]0849679 2175315[12]9620295 42175315[12]9620368 (1)B>
1305189[13]7722107 2839199[37]0849681 2175315[12]9620293 42175315[12]9620368 <A(2)
1305189[13]7722108 2839199[37]0470049 -75 <A(2) 22175315[12]9620368
1305189[13]7722109 2839199[37]0470051 -73 1 (3)B> 22175315[12]9620368
1305189[13]7722110 2839199[37]0090419 2175315[12]9620295 1 32175315[12]9620368 (3)B>
1305189[13]7722111 2839199[37]0090421 2175315[12]9620293 1 32175315[12]9620368 <B(1)
1305189[13]7722112 2839199[37]0090425 2175315[12]9620295 1 32175315[12]9620367 4 (4)A>
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 2 41+V(3) 11+V(2) 32 2 32 41+V(1) (4)A>
1 1 1 2 41+V(3) 11+V(2) 32 2 32 42+V(1) (1)B>
2 3 -1 2 41+V(3) 11+V(2) 32 2 32 42+V(1) <A(2)
3 5+V(1) -3+-1*V(1) 2 41+V(3) 11+V(2) 32 2 32 <A(2) 22+V(1)
4 6+V(1) -4+-1*V(1) 2 41+V(3) 11+V(2) 32 2 3 <B(1) 23+V(1)
5 10+V(1) -2+-1*V(1) 2 41+V(3) 11+V(2) 32 2 4 (4)A> 23+V(1)
6 13+2*V(1) 1 2 41+V(3) 11+V(2) 32 2 44+V(1) (4)A>
7 14+2*V(1) 2 2 41+V(3) 11+V(2) 32 2 45+V(1) (1)B>
8 16+2*V(1) 0 2 41+V(3) 11+V(2) 32 2 45+V(1) <A(2)
9 21+3*V(1) -5+-1*V(1) 2 41+V(3) 11+V(2) 32 2 <A(2) 25+V(1)
10 23+3*V(1) -3+-1*V(1) 2 41+V(3) 11+V(2) 32 4 (4)A> 25+V(1)
11 28+4*V(1) 2 2 41+V(3) 11+V(2) 32 46+V(1) (4)A>
12 29+4*V(1) 3 2 41+V(3) 11+V(2) 32 47+V(1) (1)B>
13 31+4*V(1) 1 2 41+V(3) 11+V(2) 32 47+V(1) <A(2)
14 38+5*V(1) -6+-1*V(1) 2 41+V(3) 11+V(2) 32 <A(2) 27+V(1)
15 39+5*V(1) -7+-1*V(1) 2 41+V(3) 11+V(2) 3 <B(1) 28+V(1)
16 43+5*V(1) -5+-1*V(1) 2 41+V(3) 11+V(2) 4 (4)A> 28+V(1)
17 51+6*V(1) 3 2 41+V(3) 11+V(2) 49+V(1) (4)A>
18 52+6*V(1) 4 2 41+V(3) 11+V(2) 410+V(1) (1)B>
19 54+6*V(1) 2 2 41+V(3) 11+V(2) 410+V(1) <A(2)
20 64+7*V(1) -8+-1*V(1) 2 41+V(3) 11+V(2) <A(2) 210+V(1)
21 65+7*V(1)+V(2) -9+-1*V(1)+-1*V(2) 2 41+V(3) <A(2) 211+V(1)+V(2)
22 66+7*V(1)+V(2)+V(3) -10+-1*V(1)+-1*V(2)+-1*V(3) 2 <A(2) 212+V(1)+V(2)+V(3)
23 68+7*V(1)+V(2)+V(3) -8+-1*V(1)+-1*V(2)+-1*V(3) 4 (4)A> 212+V(1)+V(2)+V(3)
24 80+8*V(1)+2*V(2)+2*V(3) 4 413+V(1)+V(2)+V(3) (4)A>
25 81+8*V(1)+2*V(2)+2*V(3) 5 414+V(1)+V(2)+V(3) (1)B>
26 83+8*V(1)+2*V(2)+2*V(3) 3 414+V(1)+V(2)+V(3) <A(2)
27 97+9*V(1)+3*V(2)+3*V(3) -11+-1*V(1)+-1*V(2)+-1*V(3) <A(2) 214+V(1)+V(2)+V(3)
28 99+9*V(1)+3*V(2)+3*V(3) -9+-1*V(1)+-1*V(2)+-1*V(3) 1 (3)B> 214+V(1)+V(2)+V(3)
29 113+10*V(1)+4*V(2)+4*V(3) 5 1 314+V(1)+V(2)+V(3) (3)B>
30 115+10*V(1)+4*V(2)+4*V(3) 3 1 314+V(1)+V(2)+V(3) <B(1)
31 119+10*V(1)+4*V(2)+4*V(3) 5 1 313+V(1)+V(2)+V(3) 4 (4)A>
<< Success! ==> defined new CTR 32 (PPA)
1305189[13]7722112 2839199[37]0090425 2175315[12]9620295 1 32175315[12]9620367 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=2175315[12]9620364, repcount=1087657[12]4810183, factor=3/2
1957784[13]6583210 6388198[37]9672722 3262973[12]4430478 1 3 43262973[12]4430550 (4)A>
== Executing PPA-CTR 2 (once), V(1)=3262973[12]4430547
1957784[13]6583219 6388198[37]8533837 3262973[12]4430479 22 33262973[12]4430550 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=3262973[12]4430547, repcount=1631486[12]7215274, factor=3/2
2936676[13]9874863 1437344[38]7371805 4894460[12]1645753 22 32 44894460[12]1645823 (4)A>
== Executing PPA-CTR 17 (once), V(1)=4894460[12]1645822, V(2)=0
2936676[13]9874868 1437344[38]9017637 -71 22 4 (4)A> 24894460[12]1645825
== Executing PA-CTR 15, V(1)=0, V(2)=4894460[12]1645824, repcount=1, factor=2/1
2936676[13]9874873 1437344[38]2309294 -72 2 4 (4)A> 24894460[12]1645827
== Executing PPA-CTR 16 (once), V(1)=0, V(2)=4894460[12]1645826
2936676[13]9874886 1437344[38]0538457 4894460[12]1645757 1 34894460[12]1645830 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=4894460[12]1645827, repcount=2447230[12]5822914, factor=3/2
4405014[13]4812370 3234025[38]1121785 7341690[12]7468671 1 32 47341690[12]7468743 (4)A>
== Executing PPA-CTR 7 (once), V(1)=7341690[12]7468742, V(2)=0
4405014[13]4812384 3234025[38]0996789 7341690[12]7468673 1 37341690[12]7468747 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=7341690[12]7468744, repcount=3670845[12]8734373, factor=3/2
6607521[13]7218622 7276557[38]3449906 1101253[13]6203046 1 3 41101253[13]6203120 (4)A>
== Executing PPA-CTR 2 (once), V(1)=1101253[13]6203117
6607521[13]7218631 7276557[38]5856161 1101253[13]6203047 22 31101253[13]6203120 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=1101253[13]6203117, repcount=5506268[12]3101559, factor=3/2
9911282[13]5827985 1637225[39]1563194 1651880[13]9304606 22 32 41651880[13]9304678 (4)A>
== Executing PPA-CTR 17 (once), V(1)=1651880[13]9304677, V(2)=0
9911282[13]5827990 1637225[39]0867881 -73 22 4 (4)A> 21651880[13]9304680
== Executing PA-CTR 15, V(1)=0, V(2)=1651880[13]9304679, repcount=1, factor=2/1
9911282[13]5827995 1637225[39]9477248 -74 2 4 (4)A> 21651880[13]9304682
== Executing PPA-CTR 16 (once), V(1)=0, V(2)=1651880[13]9304681
9911282[13]5828008 1637225[39]6000686 1651880[13]9304610 1 31651880[13]9304685 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=1651880[13]9304682, repcount=8259402[12]9652342, factor=3/2
1486692[14]3742060 3683757[39]0778998 2477820[13]8956952 1 3 42477820[13]8957027 (4)A>
== Executing PPA-CTR 2 (once), V(1)=2477820[13]8957024
1486692[14]3742069 3683757[39]8693067 2477820[13]8956953 22 32477820[13]8957027 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=2477820[13]8957024, repcount=1238910[13]9478513, factor=3/2
2230038[14]0613147 8288453[39]9551704 3716731[13]8435466 22 3 43716731[13]8435540 (4)A>
== Executing PPA-CTR 8 (once), V(1)=3716731[13]8435537, V(2)=0
2230038[14]0613156 8288453[39]6422799 3716731[13]8435467 2 3 2 33716731[13]8435540 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=3716731[13]8435537, repcount=1858365[13]9217769, factor=3/2
3345057[14]5919770 1864902[40]4612572 5575096[13]7653236 2 3 2 32 45575096[13]7653308 (4)A>
== Executing PPA-CTR 11 (once), V(1)=5575096[13]7653307
3345057[14]5919790 1864902[40]0532469 5575096[13]7653239 3 2 35575096[13]7653313 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=5575096[13]7653310, repcount=2787548[13]3826656, factor=3/2
5017586[14]8879726 4196029[40]7226037 8362644[13]1479895 3 2 3 48362644[13]1479969 (4)A>
== Executing PPA-CTR 12 (once), V(1)=8362644[13]1479966, V(2)=0
5017586[14]8879735 4196029[40]0185990 8362644[13]1479896 32 2 38362644[13]1479969 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=8362644[13]1479966, repcount=4181322[13]0739984, factor=3/2
7526380[14]3319639 9441066[40]6546598 1254396[14]2219880 32 2 3 41254396[14]2219953 (4)A>
== Executing PPA-CTR 12 (once), V(1)=1254396[14]2219950, V(2)=1
7526380[14]3319648 9441066[40]0986519 1254396[14]2219881 33 2 31254396[14]2219953 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=1254396[14]2219950, repcount=6271983[13]1109976, factor=3/2
1128957[15]9979504 2124240[41]2248007 1881595[14]3329857 33 2 3 41881595[14]3329929 (4)A>
== Executing PPA-CTR 12 (once), V(1)=1881595[14]3329926, V(2)=2
1128957[15]9979513 2124240[41]8907880 1881595[14]3329858 34 2 31881595[14]3329929 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=1881595[14]3329926, repcount=9407975[13]1664964, factor=3/2
1693435[15]9969297 4779540[41]0921408 2822392[14]4994822 34 2 3 42822392[14]4994893 (4)A>
== Executing PPA-CTR 12 (once), V(1)=2822392[14]4994890, V(2)=3
1693435[15]9969306 4779540[41]0911209 2822392[14]4994823 35 2 32822392[14]4994893 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=2822392[14]4994890, repcount=1411196[14]7497446, factor=3/2
2540153[15]4953982 1075396[42]5454417 4233588[14]2492269 35 2 3 44233588[14]2492339 (4)A>
== Executing PPA-CTR 12 (once), V(1)=4233588[14]2492336, V(2)=4
2540153[15]4953991 1075396[42]0439110 4233588[14]2492270 36 2 34233588[14]2492339 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=4233588[14]2492336, repcount=2116794[14]1246169, factor=3/2
3810230[15]2431005 2419642[42]4430483 6350383[14]3738439 36 2 3 46350383[14]3738508 (4)A>
== Executing PPA-CTR 12 (once), V(1)=6350383[14]3738505, V(2)=5
3810230[15]2431014 2419642[42]1907514 6350383[14]3738440 37 2 36350383[14]3738508 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=6350383[14]3738505, repcount=3175191[14]1869253, factor=3/2
5715345[15]3646532 5444194[42]0934071 9525575[14]5607693 37 2 32 49525575[14]5607760 (4)A>
== Executing PPA-CTR 20 (once), V(1)=9525575[14]5607759, V(2)=4
5715345[15]3646542 5444194[42]7757371 -69 37 4 (4)A> 29525575[14]5607764
== Executing PA-CTR 13, V(1)=4, V(2)=9525575[14]5607763, repcount=3, factor=3/2
5715345[15]3646560 5444194[42]1404003 -75 3 4 (4)A> 29525575[14]5607773
== Executing PPA-CTR 21 (once), V(1)=0, V(2)=9525575[14]5607771
5715345[15]3646576 5444194[42]8227351 9525575[14]5607699 2 4 1 2 39525575[14]5607774 4 (4)A>
== Executing PA-CTR 5, V(1)=0, V(2)=9525575[14]5607771, repcount=4762787[14]7803886, factor=3/2
8573017[15]0469892 1224943[43]6369199 1428836[15]3411585 2 4 1 2 32 41428836[15]3411659 (4)A>
== Executing PPA-CTR 6 (once), V(1)=1428836[15]3411658, V(2)=0, V(3)=0
8573017[15]0469917 1224943[43]3662547 1428836[15]3411589 1 31428836[15]3411668 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=1428836[15]3411665, repcount=7144181[14]1705833, factor=3/2
1285952[16]0704915 2756123[43]9392544 2143254[15]5117422 1 32 42143254[15]5117500 (4)A>
== Executing PPA-CTR 7 (once), V(1)=2143254[15]5117499, V(2)=0
1285952[16]0704929 2756123[43]9862576 2143254[15]5117424 1 32143254[15]5117504 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=2143254[15]5117501, repcount=1071627[15]7558751, factor=3/2
1928928[16]6057435 6201278[43]5490089 3214881[15]2676175 1 32 43214881[15]2676254 (4)A>
== Executing PPA-CTR 7 (once), V(1)=3214881[15]2676253, V(2)=0
1928928[16]6057449 6201278[43]6195137 3214881[15]2676177 1 33214881[15]2676258 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=3214881[15]2676255, repcount=1607440[15]1338128, factor=3/2
2893393[16]4086217 1395287[44]9209569 4822322[15]4014305 1 32 44822322[15]4014385 (4)A>
== Executing PPA-CTR 7 (once), V(1)=4822322[15]4014384, V(2)=0
2893393[16]4086231 1395287[44]5267141 4822322[15]4014307 1 34822322[15]4014389 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=4822322[15]4014386, repcount=2411161[15]2007194, factor=3/2
4340090[16]6129395 3139397[44]8599989 7233483[15]6021501 1 3 47233483[15]6021583 (4)A>
== Executing PPA-CTR 2 (once), V(1)=7233483[15]6021580
4340090[16]6129404 3139397[44]0643170 7233483[15]6021502 22 37233483[15]6021583 4 (4)A>
== Executing PA-CTR 1, V(1)=0, V(2)=7233483[15]6021580, repcount=3616741[15]3010791, factor=3/2
6510135[16]4194150 7063643[44]8088123 1085022[16]9032293 22 3 41085022[16]9032374 (4)A>
== Executing PPA-CTR 8 (once), V(1)=1085022[16]9032371, V(2)=0
6510135[16]4194159 7063643[44]6152886 1085022[16]9032294 2 3 2 31085022[16]9032374 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=1085022[16]9032371, repcount=5425112[15]4516186, factor=3/2
9765202[16]1291275 1589319[45]9274534 1627533[16]3548480 2 3 2 32 41627533[16]3548559 (4)A>
== Executing PPA-CTR 11 (once), V(1)=1627533[16]3548558
9765202[16]1291295 1589319[45]0565937 1627533[16]3548483 3 2 31627533[16]3548564 4 (4)A>
== Executing PA-CTR 4, V(1)=0, V(2)=1627533[16]3548561, repcount=8137669[15]6774281, factor=3/2
1464780[17]1936981 3575969[45]7509630 2441300[16]0322764 3 2 32 42441300[16]0322844 (4)A>
== Executing PPA-CTR 22 (once), V(1)=2441300[16]0322843
1464780[17]1937007 3575969[45]9446755 2441300[16]0322767 2 4 1 2 32441300[16]0322849 4 (4)A>
== Executing PA-CTR 5, V(1)=0, V(2)=2441300[16]0322846, repcount=1220650[16]0161424, factor=3/2
2197170[17]2905551 8045931[45]4184323 3661951[16]0484191 2 4 1 2 3 43661951[16]0484273 (4)A>
== Executing PPA-CTR 30 (once), V(1)=3661951[16]0484270
2197170[17]2905560 8045931[45]5152884 3661951[16]0484192 2 4 1 3 2 33661951[16]0484273 4 (4)A>
== Executing PA-CTR 23, V(1)=0, V(2)=3661951[16]0484270, repcount=1830975[16]5242136, factor=3/2
3295755[17]4358376 1810334[46]7101732 5492926[16]5726328 2 4 1 3 2 3 45492926[16]5726409 (4)A>
== Executing PPA-CTR 24 (once), V(1)=5492926[16]5726406, V(2)=0
3295755[17]4358385 1810334[46]8554565 5492926[16]5726329 2 4 1 32 2 35492926[16]5726409 4 (4)A>
== Executing PA-CTR 23, V(1)=0, V(2)=5492926[16]5726406, repcount=2746463[16]7863204, factor=3/2
4943633[17]1537609 4073252[46]8623453 8239389[16]3589533 2 4 1 32 2 3 48239389[16]3589613 (4)A>
== Executing PPA-CTR 24 (once), V(1)=8239389[16]3589610, V(2)=1
4943633[17]1537618 4073252[46]5802694 8239389[16]3589534 2 4 1 33 2 38239389[16]3589613 4 (4)A>
== Executing PA-CTR 23, V(1)=0, V(2)=8239389[16]3589610, repcount=4119694[16]6794806, factor=3/2
7415450[17]2306454 9164818[46]9483662 1235908[17]0384340 2 4 1 33 2 3 41235908[17]0384419 (4)A>
== Executing PPA-CTR 24 (once), V(1)=1235908[17]0384416, V(2)=2
7415450[17]2306463 9164818[46]0252515 1235908[17]0384341 2 4 1 34 2 31235908[17]0384419 4 (4)A>
== Executing PA-CTR 23, V(1)=0, V(2)=1235908[17]0384416, repcount=6179542[16]0192209, factor=3/2
1112317[18]3459717 2062084[47]5073648 1853862[17]0576550 2 4 1 34 2 3 41853862[17]0576628 (4)A>
== Executing PPA-CTR 24 (once), V(1)=1853862[17]0576625, V(2)=3
1112317[18]3459726 2062084[47]6226919 1853862[17]0576551 2 4 1 35 2 31853862[17]0576628 4 (4)A>
== Executing PA-CTR 23, V(1)=0, V(2)=1853862[17]0576625, repcount=9269313[16]0288313, factor=3/2
1668476[18]5189604 4639689[47]2267956 2780794[17]0864864 2 4 1 35 2 32 42780794[17]0864940 (4)A>
== Executing PPA-CTR 25 (once), V(1)=2780794[17]0864939, V(2)=2
1668476[18]5189615 4639689[47]5727740 2780794[17]0864866 2 4 1 35 42780794[17]0864945 (4)A>
== Executing PA-CTR 3, V(1)=2780794[17]0864944, V(2)=2, repcount=2, factor=3/2
1668476[18]5189627 4639689[47]9187548 2780794[17]0864868 2 4 1 3 42780794[17]0864951 (4)A>
== Executing PPA-CTR 26 (once), V(1)=2780794[17]0864948
1668476[18]5189636 4639689[47]0917465 2780794[17]0864869 2 4 22 32780794[17]0864951 4 (4)A>
== Executing PA-CTR 3, V(1)=0, V(2)=2780794[17]0864948, repcount=1390397[17]5432475, factor=3/2
2502714[18]7784486 1043930[48]9119090 4171191[17]6297344 2 4 22 3 44171191[17]6297426 (4)A>
2502714[18]7784487 1043930[48]9119091 4171191[17]6297345 2 4 22 3 44171191[17]6297427 (1)B>
2502714[18]7784488 1043930[48]9119093 4171191[17]6297343 2 4 22 3 44171191[17]6297427 <A(2)
2502714[18]7784489 1043930[48]5416520 -84 2 4 22 3 <A(2) 24171191[17]6297427
2502714[18]7784490 1043930[48]5416521 -85 2 4 22 <B(1) 24171191[17]6297428
2502714[18]7784491 1043930[48]5416523 -83 2 4 2 3 (2)B> 24171191[17]6297428
2502714[18]7784492 1043930[48]5416524 -82 2 4 2 3 2 (3)B> 24171191[17]6297427
2502714[18]7784493 1043930[48]1713951 4171191[17]6297345 2 4 2 3 2 34171191[17]6297427 (3)B>
2502714[18]7784494 1043930[48]1713953 4171191[17]6297343 2 4 2 3 2 34171191[17]6297427 <B(1)
2502714[18]7784495 1043930[48]1713957 4171191[17]6297345 2 4 2 3 2 34171191[17]6297426 4 (4)A>
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 [*]* [*]* 22+V(2) 3 43+V(1) (4)A>
1 1 1 [*]* [*]* 22+V(2) 3 44+V(1) (1)B>
2 3 -1 [*]* [*]* 22+V(2) 3 44+V(1) <A(2)
3 7+V(1) -5+-1*V(1) [*]* [*]* 22+V(2) 3 <A(2) 24+V(1)
4 8+V(1) -6+-1*V(1) [*]* [*]* 22+V(2) <B(1) 25+V(1)
5 10+V(1) -4+-1*V(1) [*]* [*]* 21+V(2) 3 (2)B> 25+V(1)
6 11+V(1) -3+-1*V(1) [*]* [*]* 21+V(2) 3 2 (3)B> 24+V(1)
7 15+2*V(1) 1 [*]* [*]* 21+V(2) 3 2 34+V(1) (3)B>
8 17+2*V(1) -1 [*]* [*]* 21+V(2) 3 2 34+V(1) <B(1)
9 21+2*V(1) 1 [*]* [*]* 21+V(2) 3 2 33+V(1) 4 (4)A>
<< Success! ==> defined new CTR 33 (PPA)
2502714[18]7784495 1043930[48]1713957 4171191[17]6297345 2 4 2 3 2 34171191[17]6297426 4 (4)A>
== Executing PA-CTR 23, V(1)=0, V(2)=4171191[17]6297423, repcount=2085595[17]8148712, factor=3/2
3754072[18]6676767 2348842[48]4977909 6256786[17]4446057 2 4 2 3 2 32 46256786[17]4446137 (4)A>
3754072[18]6676768 2348842[48]4977910 6256786[17]4446058 2 4 2 3 2 32 46256786[17]4446138 (1)B>
3754072[18]6676769 2348842[48]4977912 6256786[17]4446056 2 4 2 3 2 32 46256786[17]4446138 <A(2)
3754072[18]6676770 2348842[48]9424050 -82 2 4 2 3 2 32 <A(2) 26256786[17]4446138
3754072[18]6676771 2348842[48]9424051 -83 2 4 2 3 2 3 <B(1) 26256786[17]4446139
3754072[18]6676772 2348842[48]9424055 -81 2 4 2 3 2 4 (4)A> 26256786[17]4446139
3754072[18]6676773 2348842[48]3870194 6256786[17]4446058 2 4 2 3 2 46256786[17]4446140 (4)A>
3754072[18]6676774 2348842[48]3870195 6256786[17]4446059 2 4 2 3 2 46256786[17]4446141 (1)B>
3754072[18]6676775 2348842[48]3870197 6256786[17]4446057 2 4 2 3 2 46256786[17]4446141 <A(2)
3754072[18]6676776 2348842[48]8316338 -84 2 4 2 3 2 <A(2) 26256786[17]4446141
3754072[18]6676777 2348842[48]8316340 -82 2 4 2 3 4 (4)A> 26256786[17]4446141
3754072[18]6676778 2348842[48]2762481 6256786[17]4446059 2 4 2 3 46256786[17]4446142 (4)A>
3754072[18]6676779 2348842[48]2762482 6256786[17]4446060 2 4 2 3 46256786[17]4446143 (1)B>
3754072[18]6676780 2348842[48]2762484 6256786[17]4446058 2 4 2 3 46256786[17]4446143 <A(2)
3754072[18]6676781 2348842[48]7208627 -85 2 4 2 3 <A(2) 26256786[17]4446143
3754072[18]6676782 2348842[48]7208628 -86 2 4 2 <B(1) 26256786[17]4446144
3754072[18]6676783 2348842[48]7208630 -84 2 4 3 (2)B> 26256786[17]4446144
3754072[18]6676784 2348842[48]7208631 -83 2 4 3 2 (3)B> 26256786[17]4446143
3754072[18]6676785 2348842[48]1654774 6256786[17]4446060 2 4 3 2 36256786[17]4446143 (3)B>
3754072[18]6676786 2348842[48]1654776 6256786[17]4446058 2 4 3 2 36256786[17]4446143 <B(1)
3754072[18]6676787 2348842[48]1654780 6256786[17]4446060 2 4 3 2 36256786[17]4446142 4 (4)A>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 [*]* [*]* 2 3 2 32 41+V(1) (4)A>
1 1 1 [*]* [*]* 2 3 2 32 42+V(1) (1)B>
2 3 -1 [*]* [*]* 2 3 2 32 42+V(1) <A(2)
3 5+V(1) -3+-1*V(1) [*]* [*]* 2 3 2 32 <A(2) 22+V(1)
4 6+V(1) -4+-1*V(1) [*]* [*]* 2 3 2 3 <B(1) 23+V(1)
5 10+V(1) -2+-1*V(1) [*]* [*]* 2 3 2 4 (4)A> 23+V(1)
6 13+2*V(1) 1 [*]* [*]* 2 3 2 44+V(1) (4)A>
7 14+2*V(1) 2 [*]* [*]* 2 3 2 45+V(1) (1)B>
8 16+2*V(1) 0 [*]* [*]* 2 3 2 45+V(1) <A(2)
9 21+3*V(1) -5+-1*V(1) [*]* [*]* 2 3 2 <A(2) 25+V(1)
10 23+3*V(1) -3+-1*V(1) [*]* [*]* 2 3 4 (4)A> 25+V(1)
11 28+4*V(1) 2 [*]* [*]* 2 3 46+V(1) (4)A>
12 29+4*V(1) 3 [*]* [*]* 2 3 47+V(1) (1)B>
13 31+4*V(1) 1 [*]* [*]* 2 3 47+V(1) <A(2)
14 38+5*V(1) -6+-1*V(1) [*]* [*]* 2 3 <A(2) 27+V(1)
15 39+5*V(1) -7+-1*V(1) [*]* [*]* 2 <B(1) 28+V(1)
16 41+5*V(1) -5+-1*V(1) [*]* [*]* 3 (2)B> 28+V(1)
17 42+5*V(1) -4+-1*V(1) [*]* [*]* 3 2 (3)B> 27+V(1)
18 49+6*V(1) 3 [*]* [*]* 3 2 37+V(1) (3)B>
19 51+6*V(1) 1 [*]* [*]* 3 2 37+V(1) <B(1)
20 55+6*V(1) 3 [*]* [*]* 3 2 36+V(1) 4 (4)A>
<< Success! ==> defined new CTR 34 (PPA)
3754072[18]6676787 2348842[48]1654780 6256786[17]4446060 2 4 3 2 36256786[17]4446142 4 (4)A>
== Executing PA-CTR 5, V(1)=0, V(2)=6256786[17]4446139, repcount=3128393[17]2223070, factor=3/2
5631108[18]0015207 5284896[48]4560180 9385180[17]6669130 2 4 3 2 32 49385180[17]6669211 (4)A>
5631108[18]0015208 5284896[48]4560181 9385180[17]6669131 2 4 3 2 32 49385180[17]6669212 (1)B>
5631108[18]0015209 5284896[48]4560183 9385180[17]6669129 2 4 3 2 32 49385180[17]6669212 <A(2)
5631108[18]0015210 5284896[48]1229395 -83 2 4 3 2 32 <A(2) 29385180[17]6669212
5631108[18]0015211 5284896[48]1229396 -84 2 4 3 2 3 <B(1) 29385180[17]6669213
5631108[18]0015212 5284896[48]1229400 -82 2 4 3 2 4 (4)A> 29385180[17]6669213
5631108[18]0015213 5284896[48]7898613 9385180[17]6669131 2 4 3 2 49385180[17]6669214 (4)A>
5631108[18]0015214 5284896[48]7898614 9385180[17]6669132 2 4 3 2 49385180[17]6669215 (1)B>
5631108[18]0015215 5284896[48]7898616 9385180[17]6669130 2 4 3 2 49385180[17]6669215 <A(2)
5631108[18]0015216 5284896[48]4567831 -85 2 4 3 2 <A(2) 29385180[17]6669215
5631108[18]0015217 5284896[48]4567833 -83 2 4 3 4 (4)A> 29385180[17]6669215
5631108[18]0015218 5284896[48]1237048 9385180[17]6669132 2 4 3 49385180[17]6669216 (4)A>
5631108[18]0015219 5284896[48]1237049 9385180[17]6669133 2 4 3 49385180[17]6669217 (1)B>
5631108[18]0015220 5284896[48]1237051 9385180[17]6669131 2 4 3 49385180[17]6669217 <A(2)
5631108[18]0015221 5284896[48]7906268 -86 2 4 3 <A(2) 29385180[17]6669217
5631108[18]0015222 5284896[48]7906269 -87 2 4 <B(1) 29385180[17]6669218
5631108[18]0015223 5284896[48]7906270 -86 2 1 H> 1 29385180[17]6669218 [stop]
Lines: 909
Top steps: 908
Macro steps: 56311080864886654111667020015223
Basic steps: 52848963802863398154295757589434621786736282921545024067906270
Tape index: -86
nonzeros: 9385180144147775685277836669221
log10(nonzeros): 30.972
log10(steps ): 61.723
Run state: stop
Some long numbers above are shortened: #(omitted digits) shown in "[]".
Input to awk program:
gohalt 1
nbs 5
T 2-state 5-symbol #k from T.J. & S. Ligocki
5T 1RB 2LA 4RA 1LB 2LA 0LA 2RB 3RB 2RA 1RH
: >9.3x10^30 >5.2x10^61
L 4
M 950
pref sim
machv Lig25_k just simple
machv Lig25_k-r with repetitions reduced
machv Lig25_k-1 with tape symbol exponents
machv Lig25_k-m as 1-bck-macro machine
machv Lig25_k-a as 1-bck-macro machine with pure additive config-TRs
iam Lig25_k-a
mtype 1 0
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:12:52 CEST 2010
edate Tue Jul 6 22:12:56 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:12:52 CEST 2010