Comment: This TM produces >4.6x10^434 nonzeros in >7.6x10^868 steps.
| State | on 0 |
on 1 |
on 2 |
on 3 |
on 0 | on 1 | on 2 | on 3 | ||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Move | Goto | Move | Goto | Move | Goto | Move | Goto | |||||||||
| A | 1RB | 0RB | 3LC | 1RC | 1 | right | B | 0 | right | B | 3 | left | C | 1 | right | C |
| B | 0RC | 1RH | 2RC | 3RC | 0 | right | C | 1 | right | H | 2 | right | C | 3 | right | C |
| C | 1LB | 2LA | 3LA | 2RB | 1 | left | B | 2 | left | A | 3 | left | A | 2 | right | B |
The same TM just simple.
The same TM with repetitions reduced.
The same TM with tape symbol exponents.
The same TM as 2-bck-macro machine.
Simulation is done as 2-bck-macro machine with pure additive config-TRs.
Pushing initial machine.
Pushing macro factor 2.
Pushing BCK machine.
Steps BasSteps BasTpos Tape contents
0 0 0 (00)A>
1 2 2 (10)C>
2 16 4 02 (22)C>
3 21 1 02 <A(33) 20
4 23 -1 <B(13) 33 20
5 28 2 01 (22)B> 33 20
6 30 4 01 22 (32)B> 20
7 42 6 01 22 12 (12)B>
8 48 8 01 22 122 (12)C>
9 53 5 01 22 122 <A(23) 20
10 57 1 01 22 <A(23) 232 20
11 59 -1 01 <A(33) 233 20
12 62 2 (32)B> 233 20
13 64 4 32 (22)B> 232 20
14 68 8 32 222 (22)B> 20
15 75 5 32 222 <C(33) 32
16 79 1 32 <C(33) 332 32
17 84 4 12 (32)B> 332 32
18 88 8 12 322 (32)B> 32
19 92 10 12 323 (12)B>
20 98 12 12 323 12 (12)C>
21 103 9 12 323 12 <A(23) 20
22 105 7 12 323 <A(23) 23 20
23 112 10 12 322 21 (23)C> 23 20
24 116 12 12 322 212 (23)C> 20
25 120 14 12 322 213 (20)C>
26 131 11 12 322 213 <C(32) 32
27 137 5 12 322 <C(32) 324
28 144 8 12 32 12 (12)B> 324
29 160 16 12 32 125 (12)B>
30 166 18 12 32 126 (12)C>
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* 323+V(2) 121+V(1) (12)C>
1 5 -3 [*]* 323+V(2) 121+V(1) <A(23) 20
2 7+2*V(1) -5+-2*V(1) [*]* 323+V(2) <A(23) 231+V(1) 20
3 14+2*V(1) -2+-2*V(1) [*]* 322+V(2) 21 (23)C> 231+V(1) 20
4 18+6*V(1) 0 [*]* 322+V(2) 212+V(1) (23)C> 20
5 22+6*V(1) 2 [*]* 322+V(2) 213+V(1) (20)C>
6 33+6*V(1) -1 [*]* 322+V(2) 213+V(1) <C(32) 32
7 39+8*V(1) -7+-2*V(1) [*]* 322+V(2) <C(32) 324+V(1)
8 46+8*V(1) -4+-2*V(1) [*]* 321+V(2) 12 (12)B> 324+V(1)
9 62+12*V(1) 4 [*]* 321+V(2) 125+V(1) (12)B>
10 68+12*V(1) 6 [*]* 321+V(2) 126+V(1) (12)C>
<< Success! ==> defined new CTR 1 (PA)
31 171 15 12 32 126 <A(23) 20
32 183 3 12 32 <A(23) 236 20
33 190 6 12 21 (23)C> 236 20
34 214 18 12 217 (23)C> 20
35 218 20 12 218 (20)C>
36 229 17 12 218 <C(32) 32
37 245 1 12 <C(32) 329
38 250 4 03 (22)C> 329
39 268 22 03 229 (22)C>
40 273 19 03 229 <A(33) 20
41 291 1 03 <A(33) 339 20
42 294 4 01 (23)C> 339 20
43 312 22 01 239 (23)C> 20
44 316 24 01 239 21 (20)C>
45 327 21 01 239 21 <C(32) 32
46 329 19 01 239 <C(32) 322
47 334 22 01 238 22 (12)B> 322
48 342 26 01 238 22 122 (12)B>
49 348 28 01 238 22 123 (12)C>
50 353 25 01 238 22 123 <A(23) 20
51 359 19 01 238 22 <A(23) 233 20
52 361 17 01 238 <A(33) 234 20
53 364 20 01 237 21 (23)C> 234 20
54 380 28 01 237 215 (23)C> 20
55 384 30 01 237 216 (20)C>
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* 233+V(2) 211+V(1) (20)C>
1 11 -3 [*]* 233+V(2) 211+V(1) <C(32) 32
2 13+2*V(1) -5+-2*V(1) [*]* 233+V(2) <C(32) 322+V(1)
3 18+2*V(1) -2+-2*V(1) [*]* 232+V(2) 22 (12)B> 322+V(1)
4 26+6*V(1) 2 [*]* 232+V(2) 22 122+V(1) (12)B>
5 32+6*V(1) 4 [*]* 232+V(2) 22 123+V(1) (12)C>
6 37+6*V(1) 1 [*]* 232+V(2) 22 123+V(1) <A(23) 20
7 43+8*V(1) -5+-2*V(1) [*]* 232+V(2) 22 <A(23) 233+V(1) 20
8 45+8*V(1) -7+-2*V(1) [*]* 232+V(2) <A(33) 234+V(1) 20
9 48+8*V(1) -4+-2*V(1) [*]* 231+V(2) 21 (23)C> 234+V(1) 20
10 64+12*V(1) 4 [*]* 231+V(2) 215+V(1) (23)C> 20
11 68+12*V(1) 6 [*]* 231+V(2) 216+V(1) (20)C>
<< Success! ==> defined new CTR 2 (PA)
55 384 30 01 237 216 (20)C>
== Executing PA-CTR 2, V(1)=5, V(2)=4, repcount=3, factor=5/2
88 948 48 01 23 2121 (20)C>
89 959 45 01 23 2121 <C(32) 32
90 1001 3 01 23 <C(32) 3222
91 1006 6 01 22 (12)B> 3222
92 1094 50 01 22 1222 (12)B>
93 1100 52 01 22 1223 (12)C>
94 1105 49 01 22 1223 <A(23) 20
95 1151 3 01 22 <A(23) 2323 20
96 1153 1 01 <A(33) 2324 20
97 1156 4 (32)B> 2324 20
98 1158 6 32 (22)B> 2323 20
99 1204 52 32 2223 (22)B> 20
100 1211 49 32 2223 <C(33) 32
101 1257 3 32 <C(33) 3323 32
102 1262 6 12 (32)B> 3323 32
103 1308 52 12 3223 (32)B> 32
104 1312 54 12 3224 (12)B>
105 1318 56 12 3224 12 (12)C>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 23 211+V(1) (20)C>
1 11 -3 01 23 211+V(1) <C(32) 32
2 13+2*V(1) -5+-2*V(1) 01 23 <C(32) 322+V(1)
3 18+2*V(1) -2+-2*V(1) 01 22 (12)B> 322+V(1)
4 26+6*V(1) 2 01 22 122+V(1) (12)B>
5 32+6*V(1) 4 01 22 123+V(1) (12)C>
6 37+6*V(1) 1 01 22 123+V(1) <A(23) 20
7 43+8*V(1) -5+-2*V(1) 01 22 <A(23) 233+V(1) 20
8 45+8*V(1) -7+-2*V(1) 01 <A(33) 234+V(1) 20
9 48+8*V(1) -4+-2*V(1) (32)B> 234+V(1) 20
10 50+8*V(1) -2+-2*V(1) 32 (22)B> 233+V(1) 20
11 56+10*V(1) 4 32 223+V(1) (22)B> 20
12 63+10*V(1) 1 32 223+V(1) <C(33) 32
13 69+12*V(1) -5+-2*V(1) 32 <C(33) 333+V(1) 32
14 74+12*V(1) -2+-2*V(1) 12 (32)B> 333+V(1) 32
15 80+14*V(1) 4 12 323+V(1) (32)B> 32
16 84+14*V(1) 6 12 324+V(1) (12)B>
17 90+14*V(1) 8 12 324+V(1) 12 (12)C>
<< Success! ==> defined new CTR 3 (PPA)
105 1318 56 12 3224 12 (12)C>
== Executing PA-CTR 1, V(1)=0, V(2)=21, repcount=11, factor=5/2
215 5366 122 12 322 1256 (12)C>
216 5371 119 12 322 1256 <A(23) 20
217 5483 7 12 322 <A(23) 2356 20
218 5490 10 12 32 21 (23)C> 2356 20
219 5714 122 12 32 2157 (23)C> 20
220 5718 124 12 32 2158 (20)C>
221 5729 121 12 32 2158 <C(32) 32
222 5845 5 12 32 <C(32) 3259
223 5852 8 122 (12)B> 3259
224 6088 126 1261 (12)B>
225 6094 128 1262 (12)C>
226 6099 125 1262 <A(23) 20
227 6223 1 <A(23) 2362 20
228 6226 4 01 (22)B> 2362 20
229 6350 128 01 2262 (22)B> 20
230 6357 125 01 2262 <C(33) 32
231 6481 1 01 <C(33) 3362 32
232 6486 4 12 (23)C> 3362 32
233 6610 128 12 2362 (23)C> 32
234 6612 130 12 2363 (22)C>
235 6617 127 12 2363 <A(33) 20
236 6620 130 12 2362 21 (23)C> 20
237 6624 132 12 2362 212 (20)C>
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 121+V(2) 322 121+V(1) (12)C>
1 5 -3 121+V(2) 322 121+V(1) <A(23) 20
2 7+2*V(1) -5+-2*V(1) 121+V(2) 322 <A(23) 231+V(1) 20
3 14+2*V(1) -2+-2*V(1) 121+V(2) 32 21 (23)C> 231+V(1) 20
4 18+6*V(1) 0 121+V(2) 32 212+V(1) (23)C> 20
5 22+6*V(1) 2 121+V(2) 32 213+V(1) (20)C>
6 33+6*V(1) -1 121+V(2) 32 213+V(1) <C(32) 32
7 39+8*V(1) -7+-2*V(1) 121+V(2) 32 <C(32) 324+V(1)
8 46+8*V(1) -4+-2*V(1) 122+V(2) (12)B> 324+V(1)
9 62+12*V(1) 4 126+V(1)+V(2) (12)B>
10 68+12*V(1) 6 127+V(1)+V(2) (12)C>
11 73+12*V(1) 3 127+V(1)+V(2) <A(23) 20
12 87+14*V(1)+2*V(2) -11+-2*V(1)+-2*V(2) <A(23) 237+V(1)+V(2) 20
13 90+14*V(1)+2*V(2) -8+-2*V(1)+-2*V(2) 01 (22)B> 237+V(1)+V(2) 20
14 104+16*V(1)+4*V(2) 6 01 227+V(1)+V(2) (22)B> 20
15 111+16*V(1)+4*V(2) 3 01 227+V(1)+V(2) <C(33) 32
16 125+18*V(1)+6*V(2) -11+-2*V(1)+-2*V(2) 01 <C(33) 337+V(1)+V(2) 32
17 130+18*V(1)+6*V(2) -8+-2*V(1)+-2*V(2) 12 (23)C> 337+V(1)+V(2) 32
18 144+20*V(1)+8*V(2) 6 12 237+V(1)+V(2) (23)C> 32
19 146+20*V(1)+8*V(2) 8 12 238+V(1)+V(2) (22)C>
20 151+20*V(1)+8*V(2) 5 12 238+V(1)+V(2) <A(33) 20
21 154+20*V(1)+8*V(2) 8 12 237+V(1)+V(2) 21 (23)C> 20
22 158+20*V(1)+8*V(2) 10 12 237+V(1)+V(2) 212 (20)C>
<< Success! ==> defined new CTR 4 (PPA)
237 6624 132 12 2362 212 (20)C>
== Executing PA-CTR 2, V(1)=1, V(2)=59, repcount=30, factor=5/2
567 35124 312 12 232 21152 (20)C>
568 35135 309 12 232 21152 <C(32) 32
569 35439 5 12 232 <C(32) 32153
570 35444 8 12 23 22 (12)B> 32153
571 36056 314 12 23 22 12153 (12)B>
572 36062 316 12 23 22 12154 (12)C>
573 36067 313 12 23 22 12154 <A(23) 20
574 36375 5 12 23 22 <A(23) 23154 20
575 36377 3 12 23 <A(33) 23155 20
576 36380 6 12 21 (23)C> 23155 20
577 37000 316 12 21156 (23)C> 20
578 37004 318 12 21157 (20)C>
579 37015 315 12 21157 <C(32) 32
580 37329 1 12 <C(32) 32158
581 37334 4 03 (22)C> 32158
582 37650 320 03 22158 (22)C>
583 37655 317 03 22158 <A(33) 20
584 37971 1 03 <A(33) 33158 20
585 37974 4 01 (23)C> 33158 20
586 38290 320 01 23158 (23)C> 20
587 38294 322 01 23158 21 (20)C>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 12 232 211+V(1) (20)C>
1 11 -3 12 232 211+V(1) <C(32) 32
2 13+2*V(1) -5+-2*V(1) 12 232 <C(32) 322+V(1)
3 18+2*V(1) -2+-2*V(1) 12 23 22 (12)B> 322+V(1)
4 26+6*V(1) 2 12 23 22 122+V(1) (12)B>
5 32+6*V(1) 4 12 23 22 123+V(1) (12)C>
6 37+6*V(1) 1 12 23 22 123+V(1) <A(23) 20
7 43+8*V(1) -5+-2*V(1) 12 23 22 <A(23) 233+V(1) 20
8 45+8*V(1) -7+-2*V(1) 12 23 <A(33) 234+V(1) 20
9 48+8*V(1) -4+-2*V(1) 12 21 (23)C> 234+V(1) 20
10 64+12*V(1) 4 12 215+V(1) (23)C> 20
11 68+12*V(1) 6 12 216+V(1) (20)C>
12 79+12*V(1) 3 12 216+V(1) <C(32) 32
13 91+14*V(1) -9+-2*V(1) 12 <C(32) 327+V(1)
14 96+14*V(1) -6+-2*V(1) 03 (22)C> 327+V(1)
15 110+16*V(1) 8 03 227+V(1) (22)C>
16 115+16*V(1) 5 03 227+V(1) <A(33) 20
17 129+18*V(1) -9+-2*V(1) 03 <A(33) 337+V(1) 20
18 132+18*V(1) -6+-2*V(1) 01 (23)C> 337+V(1) 20
19 146+20*V(1) 8 01 237+V(1) (23)C> 20
20 150+20*V(1) 10 01 237+V(1) 21 (20)C>
<< Success! ==> defined new CTR 5 (PPA)
587 38294 322 01 23158 21 (20)C>
== Executing PA-CTR 2, V(1)=0, V(2)=155, repcount=78, factor=5/2
1445 223778 790 01 232 21391 (20)C>
1446 223789 787 01 232 21391 <C(32) 32
1447 224571 5 01 232 <C(32) 32392
1448 224576 8 01 23 22 (12)B> 32392
1449 226144 792 01 23 22 12392 (12)B>
1450 226150 794 01 23 22 12393 (12)C>
1451 226155 791 01 23 22 12393 <A(23) 20
1452 226941 5 01 23 22 <A(23) 23393 20
1453 226943 3 01 23 <A(33) 23394 20
1454 226946 6 01 21 (23)C> 23394 20
1455 228522 794 01 21395 (23)C> 20
1456 228526 796 01 21396 (20)C>
1457 228537 793 01 21396 <C(32) 32
1458 229329 1 01 <C(32) 32397
1459 229334 4 12 (22)C> 32397
1460 230128 798 12 22397 (22)C>
1461 230133 795 12 22397 <A(33) 20
1462 230927 1 12 <A(33) 33397 20
1463 230929 -1 <A(23) 33398 20
1464 230932 2 01 (22)B> 33398 20
1465 230934 4 01 22 (32)B> 33397 20
1466 231728 798 01 22 32397 (32)B> 20
1467 231740 800 01 22 32397 12 (12)B>
1468 231746 802 01 22 32397 122 (12)C>
1469 231751 799 01 22 32397 122 <A(23) 20
1470 231755 795 01 22 32397 <A(23) 232 20
1471 231762 798 01 22 32396 21 (23)C> 232 20
1472 231770 802 01 22 32396 213 (23)C> 20
1473 231774 804 01 22 32396 214 (20)C>
1474 231785 801 01 22 32396 214 <C(32) 32
1475 231793 793 01 22 32396 <C(32) 325
1476 231800 796 01 22 32395 12 (12)B> 325
1477 231820 806 01 22 32395 126 (12)B>
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* 323+V(2) 121+V(1) (12)B>
1 6 2 [*]* [*]* 323+V(2) 122+V(1) (12)C>
2 11 -1 [*]* [*]* 323+V(2) 122+V(1) <A(23) 20
3 15+2*V(1) -5+-2*V(1) [*]* [*]* 323+V(2) <A(23) 232+V(1) 20
4 22+2*V(1) -2+-2*V(1) [*]* [*]* 322+V(2) 21 (23)C> 232+V(1) 20
5 30+6*V(1) 2 [*]* [*]* 322+V(2) 213+V(1) (23)C> 20
6 34+6*V(1) 4 [*]* [*]* 322+V(2) 214+V(1) (20)C>
7 45+6*V(1) 1 [*]* [*]* 322+V(2) 214+V(1) <C(32) 32
8 53+8*V(1) -7+-2*V(1) [*]* [*]* 322+V(2) <C(32) 325+V(1)
9 60+8*V(1) -4+-2*V(1) [*]* [*]* 321+V(2) 12 (12)B> 325+V(1)
10 80+12*V(1) 6 [*]* [*]* 321+V(2) 126+V(1) (12)B>
<< Success! ==> defined new CTR 6 (PA)
1477 231820 806 01 22 32395 126 (12)B>
== Executing PA-CTR 6, V(1)=5, V(2)=392, repcount=197, factor=5/2
3447 1417760 1988 01 22 32 12991 (12)B>
3448 1417766 1990 01 22 32 12992 (12)C>
3449 1417771 1987 01 22 32 12992 <A(23) 20
3450 1419755 3 01 22 32 <A(23) 23992 20
3451 1419762 6 01 22 21 (23)C> 23992 20
3452 1423730 1990 01 22 21993 (23)C> 20
3453 1423734 1992 01 22 21994 (20)C>
3454 1423745 1989 01 22 21994 <C(32) 32
3455 1425733 1 01 22 <C(32) 32995
3456 1425735 -1 01 <C(33) 32996
3457 1425740 2 12 (23)C> 32996
3458 1425742 4 12 23 (22)C> 32995
3459 1427732 1994 12 23 22995 (22)C>
3460 1427737 1991 12 23 22995 <A(33) 20
3461 1429727 1 12 23 <A(33) 33995 20
3462 1429730 4 12 21 (23)C> 33995 20
3463 1431720 1994 12 21 23995 (23)C> 20
3464 1431724 1996 12 21 23995 21 (20)C>
3465 1431735 1993 12 21 23995 21 <C(32) 32
3466 1431737 1991 12 21 23995 <C(32) 322
3467 1431742 1994 12 21 23994 22 (12)B> 322
3468 1431750 1998 12 21 23994 22 122 (12)B>
3469 1431756 2000 12 21 23994 22 123 (12)C>
3470 1431761 1997 12 21 23994 22 123 <A(23) 20
3471 1431767 1991 12 21 23994 22 <A(23) 233 20
3472 1431769 1989 12 21 23994 <A(33) 234 20
3473 1431772 1992 12 21 23993 21 (23)C> 234 20
3474 1431788 2000 12 21 23993 215 (23)C> 20
3475 1431792 2002 12 21 23993 216 (20)C>
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* 233+V(2) 211+V(1) (20)C>
1 11 -3 [*]* [*]* 233+V(2) 211+V(1) <C(32) 32
2 13+2*V(1) -5+-2*V(1) [*]* [*]* 233+V(2) <C(32) 322+V(1)
3 18+2*V(1) -2+-2*V(1) [*]* [*]* 232+V(2) 22 (12)B> 322+V(1)
4 26+6*V(1) 2 [*]* [*]* 232+V(2) 22 122+V(1) (12)B>
5 32+6*V(1) 4 [*]* [*]* 232+V(2) 22 123+V(1) (12)C>
6 37+6*V(1) 1 [*]* [*]* 232+V(2) 22 123+V(1) <A(23) 20
7 43+8*V(1) -5+-2*V(1) [*]* [*]* 232+V(2) 22 <A(23) 233+V(1) 20
8 45+8*V(1) -7+-2*V(1) [*]* [*]* 232+V(2) <A(33) 234+V(1) 20
9 48+8*V(1) -4+-2*V(1) [*]* [*]* 231+V(2) 21 (23)C> 234+V(1) 20
10 64+12*V(1) 4 [*]* [*]* 231+V(2) 215+V(1) (23)C> 20
11 68+12*V(1) 6 [*]* [*]* 231+V(2) 216+V(1) (20)C>
<< Success! ==> defined new CTR 7 (PA)
3475 1431792 2002 12 21 23993 216 (20)C>
== Executing PA-CTR 7, V(1)=5, V(2)=990, repcount=496, factor=5/2
8931 8860880 4978 12 21 23 212486 (20)C>
8932 8860891 4975 12 21 23 212486 <C(32) 32
8933 8865863 3 12 21 23 <C(32) 322487
8934 8865868 6 12 21 22 (12)B> 322487
8935 8875816 4980 12 21 22 122487 (12)B>
8936 8875822 4982 12 21 22 122488 (12)C>
8937 8875827 4979 12 21 22 122488 <A(23) 20
8938 8880803 3 12 21 22 <A(23) 232488 20
8939 8880805 1 12 21 <A(33) 232489 20
8940 8880808 4 12 20 (32)B> 232489 20
8941 8880810 6 12 20 32 (22)B> 232488 20
8942 8885786 4982 12 20 32 222488 (22)B> 20
8943 8885793 4979 12 20 32 222488 <C(33) 32
8944 8890769 3 12 20 32 <C(33) 332488 32
8945 8890774 6 12 20 12 (32)B> 332488 32
8946 8895750 4982 12 20 12 322488 (32)B> 32
8947 8895754 4984 12 20 12 322489 (12)B>
8948 8895760 4986 12 20 12 322489 12 (12)C>
8949 8895765 4983 12 20 12 322489 12 <A(23) 20
8950 8895767 4981 12 20 12 322489 <A(23) 23 20
8951 8895774 4984 12 20 12 322488 21 (23)C> 23 20
8952 8895778 4986 12 20 12 322488 212 (23)C> 20
8953 8895782 4988 12 20 12 322488 213 (20)C>
8954 8895793 4985 12 20 12 322488 213 <C(32) 32
8955 8895799 4979 12 20 12 322488 <C(32) 324
8956 8895806 4982 12 20 12 322487 12 (12)B> 324
8957 8895822 4990 12 20 12 322487 125 (12)B>
8958 8895828 4992 12 20 12 322487 126 (12)C>
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* 323+V(2) 121+V(1) (12)C>
1 5 -3 [*]* [*]* [*]* 323+V(2) 121+V(1) <A(23) 20
2 7+2*V(1) -5+-2*V(1) [*]* [*]* [*]* 323+V(2) <A(23) 231+V(1) 20
3 14+2*V(1) -2+-2*V(1) [*]* [*]* [*]* 322+V(2) 21 (23)C> 231+V(1) 20
4 18+6*V(1) 0 [*]* [*]* [*]* 322+V(2) 212+V(1) (23)C> 20
5 22+6*V(1) 2 [*]* [*]* [*]* 322+V(2) 213+V(1) (20)C>
6 33+6*V(1) -1 [*]* [*]* [*]* 322+V(2) 213+V(1) <C(32) 32
7 39+8*V(1) -7+-2*V(1) [*]* [*]* [*]* 322+V(2) <C(32) 324+V(1)
8 46+8*V(1) -4+-2*V(1) [*]* [*]* [*]* 321+V(2) 12 (12)B> 324+V(1)
9 62+12*V(1) 4 [*]* [*]* [*]* 321+V(2) 125+V(1) (12)B>
10 68+12*V(1) 6 [*]* [*]* [*]* 321+V(2) 126+V(1) (12)C>
<< Success! ==> defined new CTR 8 (PA)
8958 8895828 4992 12 20 12 322487 126 (12)C>
== Executing PA-CTR 8, V(1)=5, V(2)=2484, repcount=1243, factor=5/2
21388 55369112 12450 12 20 12 32 126221 (12)C>
21389 55369117 12447 12 20 12 32 126221 <A(23) 20
21390 55381559 5 12 20 12 32 <A(23) 236221 20
21391 55381566 8 12 20 12 21 (23)C> 236221 20
21392 55406450 12450 12 20 12 216222 (23)C> 20
21393 55406454 12452 12 20 12 216223 (20)C>
21394 55406465 12449 12 20 12 216223 <C(32) 32
21395 55418911 3 12 20 12 <C(32) 326224
21396 55418916 6 12 20 03 (22)C> 326224
21397 55431364 12454 12 20 03 226224 (22)C>
21398 55431369 12451 12 20 03 226224 <A(33) 20
21399 55443817 3 12 20 03 <A(33) 336224 20
21400 55443820 6 12 20 01 (23)C> 336224 20
21401 55456268 12454 12 20 01 236224 (23)C> 20
21402 55456272 12456 12 20 01 236224 21 (20)C>
21403 55456283 12453 12 20 01 236224 21 <C(32) 32
21404 55456285 12451 12 20 01 236224 <C(32) 322
21405 55456290 12454 12 20 01 236223 22 (12)B> 322
21406 55456298 12458 12 20 01 236223 22 122 (12)B>
21407 55456304 12460 12 20 01 236223 22 123 (12)C>
21408 55456309 12457 12 20 01 236223 22 123 <A(23) 20
21409 55456315 12451 12 20 01 236223 22 <A(23) 233 20
21410 55456317 12449 12 20 01 236223 <A(33) 234 20
21411 55456320 12452 12 20 01 236222 21 (23)C> 234 20
21412 55456336 12460 12 20 01 236222 215 (23)C> 20
21413 55456340 12462 12 20 01 236222 216 (20)C>
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* 233+V(2) 211+V(1) (20)C>
1 11 -3 [*]* [*]* [*]* 233+V(2) 211+V(1) <C(32) 32
2 13+2*V(1) -5+-2*V(1) [*]* [*]* [*]* 233+V(2) <C(32) 322+V(1)
3 18+2*V(1) -2+-2*V(1) [*]* [*]* [*]* 232+V(2) 22 (12)B> 322+V(1)
4 26+6*V(1) 2 [*]* [*]* [*]* 232+V(2) 22 122+V(1) (12)B>
5 32+6*V(1) 4 [*]* [*]* [*]* 232+V(2) 22 123+V(1) (12)C>
6 37+6*V(1) 1 [*]* [*]* [*]* 232+V(2) 22 123+V(1) <A(23) 20
7 43+8*V(1) -5+-2*V(1) [*]* [*]* [*]* 232+V(2) 22 <A(23) 233+V(1) 20
8 45+8*V(1) -7+-2*V(1) [*]* [*]* [*]* 232+V(2) <A(33) 234+V(1) 20
9 48+8*V(1) -4+-2*V(1) [*]* [*]* [*]* 231+V(2) 21 (23)C> 234+V(1) 20
10 64+12*V(1) 4 [*]* [*]* [*]* 231+V(2) 215+V(1) (23)C> 20
11 68+12*V(1) 6 [*]* [*]* [*]* 231+V(2) 216+V(1) (20)C>
<< Success! ==> defined new CTR 9 (PA)
21413 55456340 12462 12 20 01 236222 216 (20)C>
== Executing PA-CTR 9, V(1)=5, V(2)=6219, repcount=3110, factor=5/2
55623 345924120 31122 12 20 01 232 2115556 (20)C>
55624 345924131 31119 12 20 01 232 2115556 <C(32) 32
55625 345955243 7 12 20 01 232 <C(32) 3215557
55626 345955248 10 12 20 01 23 22 (12)B> 3215557
55627 346017476 31124 12 20 01 23 22 1215557 (12)B>
55628 346017482 31126 12 20 01 23 22 1215558 (12)C>
55629 346017487 31123 12 20 01 23 22 1215558 <A(23) 20
55630 346048603 7 12 20 01 23 22 <A(23) 2315558 20
55631 346048605 5 12 20 01 23 <A(33) 2315559 20
55632 346048608 8 12 20 01 21 (23)C> 2315559 20
55633 346110844 31126 12 20 01 2115560 (23)C> 20
55634 346110848 31128 12 20 01 2115561 (20)C>
55635 346110859 31125 12 20 01 2115561 <C(32) 32
55636 346141981 3 12 20 01 <C(32) 3215562
55637 346141986 6 12 20 12 (22)C> 3215562
55638 346173110 31130 12 20 12 2215562 (22)C>
55639 346173115 31127 12 20 12 2215562 <A(33) 20
55640 346204239 3 12 20 12 <A(33) 3315562 20
55641 346204241 1 12 20 <A(23) 3315563 20
55642 346204244 4 12 21 (22)B> 3315563 20
55643 346204246 6 12 21 22 (32)B> 3315562 20
55644 346235370 31130 12 21 22 3215562 (32)B> 20
55645 346235382 31132 12 21 22 3215562 12 (12)B>
55646 346235388 31134 12 21 22 3215562 122 (12)C>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 [*]* 20 01 232 211+V(1) (20)C>
1 11 -3 [*]* 20 01 232 211+V(1) <C(32) 32
2 13+2*V(1) -5+-2*V(1) [*]* 20 01 232 <C(32) 322+V(1)
3 18+2*V(1) -2+-2*V(1) [*]* 20 01 23 22 (12)B> 322+V(1)
4 26+6*V(1) 2 [*]* 20 01 23 22 122+V(1) (12)B>
5 32+6*V(1) 4 [*]* 20 01 23 22 123+V(1) (12)C>
6 37+6*V(1) 1 [*]* 20 01 23 22 123+V(1) <A(23) 20
7 43+8*V(1) -5+-2*V(1) [*]* 20 01 23 22 <A(23) 233+V(1) 20
8 45+8*V(1) -7+-2*V(1) [*]* 20 01 23 <A(33) 234+V(1) 20
9 48+8*V(1) -4+-2*V(1) [*]* 20 01 21 (23)C> 234+V(1) 20
10 64+12*V(1) 4 [*]* 20 01 215+V(1) (23)C> 20
11 68+12*V(1) 6 [*]* 20 01 216+V(1) (20)C>
12 79+12*V(1) 3 [*]* 20 01 216+V(1) <C(32) 32
13 91+14*V(1) -9+-2*V(1) [*]* 20 01 <C(32) 327+V(1)
14 96+14*V(1) -6+-2*V(1) [*]* 20 12 (22)C> 327+V(1)
15 110+16*V(1) 8 [*]* 20 12 227+V(1) (22)C>
16 115+16*V(1) 5 [*]* 20 12 227+V(1) <A(33) 20
17 129+18*V(1) -9+-2*V(1) [*]* 20 12 <A(33) 337+V(1) 20
18 131+18*V(1) -11+-2*V(1) [*]* 20 <A(23) 338+V(1) 20
19 134+18*V(1) -8+-2*V(1) [*]* 21 (22)B> 338+V(1) 20
20 136+18*V(1) -6+-2*V(1) [*]* 21 22 (32)B> 337+V(1) 20
21 150+20*V(1) 8 [*]* 21 22 327+V(1) (32)B> 20
22 162+20*V(1) 10 [*]* 21 22 327+V(1) 12 (12)B>
23 168+20*V(1) 12 [*]* 21 22 327+V(1) 122 (12)C>
<< Success! ==> defined new CTR 10 (PPA)
55646 346235388 31134 12 21 22 3215562 122 (12)C>
== Executing PA-CTR 8, V(1)=1, V(2)=15559, repcount=7780, factor=5/2
133446 2162476388 77814 12 21 22 322 1238902 (12)C>
133447 2162476393 77811 12 21 22 322 1238902 <A(23) 20
133448 2162554197 7 12 21 22 322 <A(23) 2338902 20
133449 2162554204 10 12 21 22 32 21 (23)C> 2338902 20
133450 2162709812 77814 12 21 22 32 2138903 (23)C> 20
133451 2162709816 77816 12 21 22 32 2138904 (20)C>
133452 2162709827 77813 12 21 22 32 2138904 <C(32) 32
133453 2162787635 5 12 21 22 32 <C(32) 3238905
133454 2162787642 8 12 21 22 12 (12)B> 3238905
133455 2162943262 77818 12 21 22 1238906 (12)B>
133456 2162943268 77820 12 21 22 1238907 (12)C>
133457 2162943273 77817 12 21 22 1238907 <A(23) 20
133458 2163021087 3 12 21 22 <A(23) 2338907 20
133459 2163021089 1 12 21 <A(33) 2338908 20
133460 2163021092 4 12 20 (32)B> 2338908 20
133461 2163021094 6 12 20 32 (22)B> 2338907 20
133462 2163098908 77820 12 20 32 2238907 (22)B> 20
133463 2163098915 77817 12 20 32 2238907 <C(33) 32
133464 2163176729 3 12 20 32 <C(33) 3338907 32
133465 2163176734 6 12 20 12 (32)B> 3338907 32
133466 2163254548 77820 12 20 12 3238907 (32)B> 32
133467 2163254552 77822 12 20 12 3238908 (12)B>
133468 2163254558 77824 12 20 12 3238908 12 (12)C>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 [*]* 21 22 322 121+V(1) (12)C>
1 5 -3 [*]* 21 22 322 121+V(1) <A(23) 20
2 7+2*V(1) -5+-2*V(1) [*]* 21 22 322 <A(23) 231+V(1) 20
3 14+2*V(1) -2+-2*V(1) [*]* 21 22 32 21 (23)C> 231+V(1) 20
4 18+6*V(1) 0 [*]* 21 22 32 212+V(1) (23)C> 20
5 22+6*V(1) 2 [*]* 21 22 32 213+V(1) (20)C>
6 33+6*V(1) -1 [*]* 21 22 32 213+V(1) <C(32) 32
7 39+8*V(1) -7+-2*V(1) [*]* 21 22 32 <C(32) 324+V(1)
8 46+8*V(1) -4+-2*V(1) [*]* 21 22 12 (12)B> 324+V(1)
9 62+12*V(1) 4 [*]* 21 22 125+V(1) (12)B>
10 68+12*V(1) 6 [*]* 21 22 126+V(1) (12)C>
11 73+12*V(1) 3 [*]* 21 22 126+V(1) <A(23) 20
12 85+14*V(1) -9+-2*V(1) [*]* 21 22 <A(23) 236+V(1) 20
13 87+14*V(1) -11+-2*V(1) [*]* 21 <A(33) 237+V(1) 20
14 90+14*V(1) -8+-2*V(1) [*]* 20 (32)B> 237+V(1) 20
15 92+14*V(1) -6+-2*V(1) [*]* 20 32 (22)B> 236+V(1) 20
16 104+16*V(1) 6 [*]* 20 32 226+V(1) (22)B> 20
17 111+16*V(1) 3 [*]* 20 32 226+V(1) <C(33) 32
18 123+18*V(1) -9+-2*V(1) [*]* 20 32 <C(33) 336+V(1) 32
19 128+18*V(1) -6+-2*V(1) [*]* 20 12 (32)B> 336+V(1) 32
20 140+20*V(1) 6 [*]* 20 12 326+V(1) (32)B> 32
21 144+20*V(1) 8 [*]* 20 12 327+V(1) (12)B>
22 150+20*V(1) 10 [*]* 20 12 327+V(1) 12 (12)C>
<< Success! ==> defined new CTR 11 (PPA)
133468 2163254558 77824 12 20 12 3238908 12 (12)C>
== Executing PA-CTR 8, V(1)=0, V(2)=38905, repcount=19453, factor=5/2
327998 13516570042 194542 12 20 12 322 1297266 (12)C>
327999 13516570047 194539 12 20 12 322 1297266 <A(23) 20
328000 13516764579 7 12 20 12 322 <A(23) 2397266 20
328001 13516764586 10 12 20 12 32 21 (23)C> 2397266 20
328002 13517153650 194542 12 20 12 32 2197267 (23)C> 20
328003 13517153654 194544 12 20 12 32 2197268 (20)C>
328004 13517153665 194541 12 20 12 32 2197268 <C(32) 32
328005 13517348201 5 12 20 12 32 <C(32) 3297269
328006 13517348208 8 12 20 122 (12)B> 3297269
328007 13517737284 194546 12 20 1297271 (12)B>
328008 13517737290 194548 12 20 1297272 (12)C>
328009 13517737295 194545 12 20 1297272 <A(23) 20
328010 13517931839 1 12 20 <A(23) 2397272 20
328011 13517931842 4 12 21 (22)B> 2397272 20
328012 13518126386 194548 12 21 2297272 (22)B> 20
328013 13518126393 194545 12 21 2297272 <C(33) 32
328014 13518320937 1 12 21 <C(33) 3397272 32
328015 13518320939 -1 12 <C(32) 3397273 32
328016 13518320944 2 03 (22)C> 3397273 32
328017 13518320946 4 03 22 (23)C> 3397272 32
328018 13518515490 194548 03 22 2397272 (23)C> 32
328019 13518515492 194550 03 22 2397273 (22)C>
328020 13518515497 194547 03 22 2397273 <A(33) 20
328021 13518515500 194550 03 22 2397272 21 (23)C> 20
328022 13518515504 194552 03 22 2397272 212 (20)C>
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 12 20 121+V(2) 322 121+V(1) (12)C>
1 5 -3 12 20 121+V(2) 322 121+V(1) <A(23) 20
2 7+2*V(1) -5+-2*V(1) 12 20 121+V(2) 322 <A(23) 231+V(1) 20
3 14+2*V(1) -2+-2*V(1) 12 20 121+V(2) 32 21 (23)C> 231+V(1) 20
4 18+6*V(1) 0 12 20 121+V(2) 32 212+V(1) (23)C> 20
5 22+6*V(1) 2 12 20 121+V(2) 32 213+V(1) (20)C>
6 33+6*V(1) -1 12 20 121+V(2) 32 213+V(1) <C(32) 32
7 39+8*V(1) -7+-2*V(1) 12 20 121+V(2) 32 <C(32) 324+V(1)
8 46+8*V(1) -4+-2*V(1) 12 20 122+V(2) (12)B> 324+V(1)
9 62+12*V(1) 4 12 20 126+V(1)+V(2) (12)B>
10 68+12*V(1) 6 12 20 127+V(1)+V(2) (12)C>
11 73+12*V(1) 3 12 20 127+V(1)+V(2) <A(23) 20
12 87+14*V(1)+2*V(2) -11+-2*V(1)+-2*V(2) 12 20 <A(23) 237+V(1)+V(2) 20
13 90+14*V(1)+2*V(2) -8+-2*V(1)+-2*V(2) 12 21 (22)B> 237+V(1)+V(2) 20
14 104+16*V(1)+4*V(2) 6 12 21 227+V(1)+V(2) (22)B> 20
15 111+16*V(1)+4*V(2) 3 12 21 227+V(1)+V(2) <C(33) 32
16 125+18*V(1)+6*V(2) -11+-2*V(1)+-2*V(2) 12 21 <C(33) 337+V(1)+V(2) 32
17 127+18*V(1)+6*V(2) -13+-2*V(1)+-2*V(2) 12 <C(32) 338+V(1)+V(2) 32
18 132+18*V(1)+6*V(2) -10+-2*V(1)+-2*V(2) 03 (22)C> 338+V(1)+V(2) 32
19 134+18*V(1)+6*V(2) -8+-2*V(1)+-2*V(2) 03 22 (23)C> 337+V(1)+V(2) 32
20 148+20*V(1)+8*V(2) 6 03 22 237+V(1)+V(2) (23)C> 32
21 150+20*V(1)+8*V(2) 8 03 22 238+V(1)+V(2) (22)C>
22 155+20*V(1)+8*V(2) 5 03 22 238+V(1)+V(2) <A(33) 20
23 158+20*V(1)+8*V(2) 8 03 22 237+V(1)+V(2) 21 (23)C> 20
24 162+20*V(1)+8*V(2) 10 03 22 237+V(1)+V(2) 212 (20)C>
<< Success! ==> defined new CTR 12 (PPA)
328022 13518515504 194552 03 22 2397272 212 (20)C>
== Executing PA-CTR 7, V(1)=1, V(2)=97269, repcount=48635, factor=5/2
863007 84481844004 486362 03 22 232 21243177 (20)C>
863008 84481844015 486359 03 22 232 21243177 <C(32) 32
863009 84482330369 5 03 22 232 <C(32) 32243178
863010 84482330374 8 03 22 23 22 (12)B> 32243178
863011 84483303086 486364 03 22 23 22 12243178 (12)B>
863012 84483303092 486366 03 22 23 22 12243179 (12)C>
863013 84483303097 486363 03 22 23 22 12243179 <A(23) 20
863014 84483789455 5 03 22 23 22 <A(23) 23243179 20
863015 84483789457 3 03 22 23 <A(33) 23243180 20
863016 84483789460 6 03 22 21 (23)C> 23243180 20
863017 84484762180 486366 03 22 21243181 (23)C> 20
863018 84484762184 486368 03 22 21243182 (20)C>
863019 84484762195 486365 03 22 21243182 <C(32) 32
863020 84485248559 1 03 22 <C(32) 32243183
863021 84485248561 -1 03 <C(33) 32243184
863022 84485248564 2 02 (32)B> 32243184
863023 84485248568 4 02 32 (12)B> 32243183
863024 84486221300 486370 02 32 12243183 (12)B>
863025 84486221306 486372 02 32 12243184 (12)C>
863026 84486221311 486369 02 32 12243184 <A(23) 20
863027 84486707679 1 02 32 <A(23) 23243184 20
863028 84486707686 4 02 21 (23)C> 23243184 20
863029 84487680422 486372 02 21243185 (23)C> 20
863030 84487680426 486374 02 21243186 (20)C>
863031 84487680437 486371 02 21243186 <C(32) 32
863032 84488166809 -1 02 <C(32) 32243187
863033 84488166814 2 13 (22)C> 32243187
863034 84488653188 486376 13 22243187 (22)C>
863035 84488653193 486373 13 22243187 <A(33) 20
863036 84489139567 -1 13 <A(33) 33243187 20
863037 84489139570 2 11 (23)C> 33243187 20
863038 84489625944 486376 11 23243187 (23)C> 20
863039 84489625948 486378 11 23243187 21 (20)C>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 03 22 232 211+V(1) (20)C>
1 11 -3 03 22 232 211+V(1) <C(32) 32
2 13+2*V(1) -5+-2*V(1) 03 22 232 <C(32) 322+V(1)
3 18+2*V(1) -2+-2*V(1) 03 22 23 22 (12)B> 322+V(1)
4 26+6*V(1) 2 03 22 23 22 122+V(1) (12)B>
5 32+6*V(1) 4 03 22 23 22 123+V(1) (12)C>
6 37+6*V(1) 1 03 22 23 22 123+V(1) <A(23) 20
7 43+8*V(1) -5+-2*V(1) 03 22 23 22 <A(23) 233+V(1) 20
8 45+8*V(1) -7+-2*V(1) 03 22 23 <A(33) 234+V(1) 20
9 48+8*V(1) -4+-2*V(1) 03 22 21 (23)C> 234+V(1) 20
10 64+12*V(1) 4 03 22 215+V(1) (23)C> 20
11 68+12*V(1) 6 03 22 216+V(1) (20)C>
12 79+12*V(1) 3 03 22 216+V(1) <C(32) 32
13 91+14*V(1) -9+-2*V(1) 03 22 <C(32) 327+V(1)
14 93+14*V(1) -11+-2*V(1) 03 <C(33) 328+V(1)
15 96+14*V(1) -8+-2*V(1) 02 (32)B> 328+V(1)
16 100+14*V(1) -6+-2*V(1) 02 32 (12)B> 327+V(1)
17 128+18*V(1) 8 02 32 127+V(1) (12)B>
18 134+18*V(1) 10 02 32 128+V(1) (12)C>
19 139+18*V(1) 7 02 32 128+V(1) <A(23) 20
20 155+20*V(1) -9+-2*V(1) 02 32 <A(23) 238+V(1) 20
21 162+20*V(1) -6+-2*V(1) 02 21 (23)C> 238+V(1) 20
22 194+24*V(1) 10 02 219+V(1) (23)C> 20
23 198+24*V(1) 12 02 2110+V(1) (20)C>
24 209+24*V(1) 9 02 2110+V(1) <C(32) 32
25 229+26*V(1) -11+-2*V(1) 02 <C(32) 3211+V(1)
26 234+26*V(1) -8+-2*V(1) 13 (22)C> 3211+V(1)
27 256+28*V(1) 14 13 2211+V(1) (22)C>
28 261+28*V(1) 11 13 2211+V(1) <A(33) 20
29 283+30*V(1) -11+-2*V(1) 13 <A(33) 3311+V(1) 20
30 286+30*V(1) -8+-2*V(1) 11 (23)C> 3311+V(1) 20
31 308+32*V(1) 14 11 2311+V(1) (23)C> 20
32 312+32*V(1) 16 11 2311+V(1) 21 (20)C>
<< Success! ==> defined new CTR 13 (PPA)
863039 84489625948 486378 11 23243187 21 (20)C>
== Executing PA-CTR 2, V(1)=0, V(2)=243184, repcount=121593, factor=5/2
2200562 528039975952 1215936 11 23 21607966 (20)C>
2200563 528039975963 1215933 11 23 21607966 <C(32) 32
2200564 528041191895 1 11 23 <C(32) 32607967
2200565 528041191900 4 11 22 (12)B> 32607967
2200566 528043623768 1215938 11 22 12607967 (12)B>
2200567 528043623774 1215940 11 22 12607968 (12)C>
2200568 528043623779 1215937 11 22 12607968 <A(23) 20
2200569 528044839715 1 11 22 <A(23) 23607968 20
2200570 528044839717 -1 11 <A(33) 23607969 20
2200571 528044839720 2 10 (32)B> 23607969 20
2200572 528044839722 4 10 32 (22)B> 23607968 20
2200573 528046055658 1215940 10 32 22607968 (22)B> 20
2200574 528046055665 1215937 10 32 22607968 <C(33) 32
2200575 528047271601 1 10 32 <C(33) 33607968 32
2200576 528047271606 4 10 12 (32)B> 33607968 32
2200577 528048487542 1215940 10 12 32607968 (32)B> 32
2200578 528048487546 1215942 10 12 32607969 (12)B>
2200579 528048487552 1215944 10 12 32607969 12 (12)C>
2200580 528048487557 1215941 10 12 32607969 12 <A(23) 20
2200581 528048487559 1215939 10 12 32607969 <A(23) 23 20
2200582 528048487566 1215942 10 12 32607968 21 (23)C> 23 20
2200583 528048487570 1215944 10 12 32607968 212 (23)C> 20
2200584 528048487574 1215946 10 12 32607968 213 (20)C>
2200585 528048487585 1215943 10 12 32607968 213 <C(32) 32
2200586 528048487591 1215937 10 12 32607968 <C(32) 324
2200587 528048487598 1215940 10 12 32607967 12 (12)B> 324
2200588 528048487614 1215948 10 12 32607967 125 (12)B>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 11 23 212+V(1) (20)C>
1 11 -3 11 23 212+V(1) <C(32) 32
2 15+2*V(1) -7+-2*V(1) 11 23 <C(32) 323+V(1)
3 20+2*V(1) -4+-2*V(1) 11 22 (12)B> 323+V(1)
4 32+6*V(1) 2 11 22 123+V(1) (12)B>
5 38+6*V(1) 4 11 22 124+V(1) (12)C>
6 43+6*V(1) 1 11 22 124+V(1) <A(23) 20
7 51+8*V(1) -7+-2*V(1) 11 22 <A(23) 234+V(1) 20
8 53+8*V(1) -9+-2*V(1) 11 <A(33) 235+V(1) 20
9 56+8*V(1) -6+-2*V(1) 10 (32)B> 235+V(1) 20
10 58+8*V(1) -4+-2*V(1) 10 32 (22)B> 234+V(1) 20
11 66+10*V(1) 4 10 32 224+V(1) (22)B> 20
12 73+10*V(1) 1 10 32 224+V(1) <C(33) 32
13 81+12*V(1) -7+-2*V(1) 10 32 <C(33) 334+V(1) 32
14 86+12*V(1) -4+-2*V(1) 10 12 (32)B> 334+V(1) 32
15 94+14*V(1) 4 10 12 324+V(1) (32)B> 32
16 98+14*V(1) 6 10 12 325+V(1) (12)B>
17 104+14*V(1) 8 10 12 325+V(1) 12 (12)C>
18 109+14*V(1) 5 10 12 325+V(1) 12 <A(23) 20
19 111+14*V(1) 3 10 12 325+V(1) <A(23) 23 20
20 118+14*V(1) 6 10 12 324+V(1) 21 (23)C> 23 20
21 122+14*V(1) 8 10 12 324+V(1) 212 (23)C> 20
22 126+14*V(1) 10 10 12 324+V(1) 213 (20)C>
23 137+14*V(1) 7 10 12 324+V(1) 213 <C(32) 32
24 143+14*V(1) 1 10 12 324+V(1) <C(32) 324
25 150+14*V(1) 4 10 12 323+V(1) 12 (12)B> 324
26 166+14*V(1) 12 10 12 323+V(1) 125 (12)B>
<< Success! ==> defined new CTR 14 (PPA)
2200588 528048487614 1215948 10 12 32607967 125 (12)B>
== Executing PA-CTR 6, V(1)=4, V(2)=607964, repcount=303983, factor=5/2
5240418 3300248206618 3039846 10 12 32 121519920 (12)B>
5240419 3300248206624 3039848 10 12 32 121519921 (12)C>
5240420 3300248206629 3039845 10 12 32 121519921 <A(23) 20
5240421 3300251246471 3 10 12 32 <A(23) 231519921 20
5240422 3300251246478 6 10 12 21 (23)C> 231519921 20
5240423 3300257326162 3039848 10 12 211519922 (23)C> 20
5240424 3300257326166 3039850 10 12 211519923 (20)C>
5240425 3300257326177 3039847 10 12 211519923 <C(32) 32
5240426 3300260366023 1 10 12 <C(32) 321519924
5240427 3300260366028 4 10 03 (22)C> 321519924
5240428 3300263405876 3039852 10 03 221519924 (22)C>
5240429 3300263405881 3039849 10 03 221519924 <A(33) 20
5240430 3300266445729 1 10 03 <A(33) 331519924 20
5240431 3300266445732 4 10 01 (23)C> 331519924 20
5240432 3300269485580 3039852 10 01 231519924 (23)C> 20
5240433 3300269485584 3039854 10 01 231519924 21 (20)C>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 [*]* 12 32 121+V(1) (12)B>
1 6 2 [*]* 12 32 122+V(1) (12)C>
2 11 -1 [*]* 12 32 122+V(1) <A(23) 20
3 15+2*V(1) -5+-2*V(1) [*]* 12 32 <A(23) 232+V(1) 20
4 22+2*V(1) -2+-2*V(1) [*]* 12 21 (23)C> 232+V(1) 20
5 30+6*V(1) 2 [*]* 12 213+V(1) (23)C> 20
6 34+6*V(1) 4 [*]* 12 214+V(1) (20)C>
7 45+6*V(1) 1 [*]* 12 214+V(1) <C(32) 32
8 53+8*V(1) -7+-2*V(1) [*]* 12 <C(32) 325+V(1)
9 58+8*V(1) -4+-2*V(1) [*]* 03 (22)C> 325+V(1)
10 68+10*V(1) 6 [*]* 03 225+V(1) (22)C>
11 73+10*V(1) 3 [*]* 03 225+V(1) <A(33) 20
12 83+12*V(1) -7+-2*V(1) [*]* 03 <A(33) 335+V(1) 20
13 86+12*V(1) -4+-2*V(1) [*]* 01 (23)C> 335+V(1) 20
14 96+14*V(1) 6 [*]* 01 235+V(1) (23)C> 20
15 100+14*V(1) 8 [*]* 01 235+V(1) 21 (20)C>
<< Success! ==> defined new CTR 15 (PPA)
5240433 3300269485584 3039854 10 01 231519924 21 (20)C>
== Executing PA-CTR 7, V(1)=0, V(2)=1519921, repcount=759961, factor=5/2
13600004 20626520009732 7599620 10 01 232 213799806 (20)C>
13600005 20626520009743 7599617 10 01 232 213799806 <C(32) 32
13600006 20626527609355 5 10 01 232 <C(32) 323799807
13600007 20626527609360 8 10 01 23 22 (12)B> 323799807
13600008 20626542808588 7599622 10 01 23 22 123799807 (12)B>
13600009 20626542808594 7599624 10 01 23 22 123799808 (12)C>
13600010 20626542808599 7599621 10 01 23 22 123799808 <A(23) 20
13600011 20626550408215 5 10 01 23 22 <A(23) 233799808 20
13600012 20626550408217 3 10 01 23 <A(33) 233799809 20
13600013 20626550408220 6 10 01 21 (23)C> 233799809 20
13600014 20626565607456 7599624 10 01 213799810 (23)C> 20
13600015 20626565607460 7599626 10 01 213799811 (20)C>
13600016 20626565607471 7599623 10 01 213799811 <C(32) 32
13600017 20626573207093 1 10 01 <C(32) 323799812
13600018 20626573207098 4 10 12 (22)C> 323799812
13600019 20626580806722 7599628 10 12 223799812 (22)C>
13600020 20626580806727 7599625 10 12 223799812 <A(33) 20
13600021 20626588406351 1 10 12 <A(33) 333799812 20
13600022 20626588406353 -1 10 <A(23) 333799813 20
13600023 20626588406356 2 11 (22)B> 333799813 20
13600024 20626588406358 4 11 22 (32)B> 333799812 20
13600025 20626596005982 7599628 11 22 323799812 (32)B> 20
13600026 20626596005994 7599630 11 22 323799812 12 (12)B>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 10 01 232 211+V(1) (20)C>
1 11 -3 10 01 232 211+V(1) <C(32) 32
2 13+2*V(1) -5+-2*V(1) 10 01 232 <C(32) 322+V(1)
3 18+2*V(1) -2+-2*V(1) 10 01 23 22 (12)B> 322+V(1)
4 26+6*V(1) 2 10 01 23 22 122+V(1) (12)B>
5 32+6*V(1) 4 10 01 23 22 123+V(1) (12)C>
6 37+6*V(1) 1 10 01 23 22 123+V(1) <A(23) 20
7 43+8*V(1) -5+-2*V(1) 10 01 23 22 <A(23) 233+V(1) 20
8 45+8*V(1) -7+-2*V(1) 10 01 23 <A(33) 234+V(1) 20
9 48+8*V(1) -4+-2*V(1) 10 01 21 (23)C> 234+V(1) 20
10 64+12*V(1) 4 10 01 215+V(1) (23)C> 20
11 68+12*V(1) 6 10 01 216+V(1) (20)C>
12 79+12*V(1) 3 10 01 216+V(1) <C(32) 32
13 91+14*V(1) -9+-2*V(1) 10 01 <C(32) 327+V(1)
14 96+14*V(1) -6+-2*V(1) 10 12 (22)C> 327+V(1)
15 110+16*V(1) 8 10 12 227+V(1) (22)C>
16 115+16*V(1) 5 10 12 227+V(1) <A(33) 20
17 129+18*V(1) -9+-2*V(1) 10 12 <A(33) 337+V(1) 20
18 131+18*V(1) -11+-2*V(1) 10 <A(23) 338+V(1) 20
19 134+18*V(1) -8+-2*V(1) 11 (22)B> 338+V(1) 20
20 136+18*V(1) -6+-2*V(1) 11 22 (32)B> 337+V(1) 20
21 150+20*V(1) 8 11 22 327+V(1) (32)B> 20
22 162+20*V(1) 10 11 22 327+V(1) 12 (12)B>
<< Success! ==> defined new CTR 16 (PPA)
13600026 20626596005994 7599630 11 22 323799812 12 (12)B>
== Executing PA-CTR 6, V(1)=0, V(2)=3799809, repcount=1899905, factor=5/2
32599076 128915861271994 18999060 11 22 322 129499526 (12)B>
32599077 128915861272000 18999062 11 22 322 129499527 (12)C>
32599078 128915861272005 18999059 11 22 322 129499527 <A(23) 20
32599079 128915880271059 5 11 22 322 <A(23) 239499527 20
32599080 128915880271066 8 11 22 32 21 (23)C> 239499527 20
32599081 128915918269174 18999062 11 22 32 219499528 (23)C> 20
32599082 128915918269178 18999064 11 22 32 219499529 (20)C>
32599083 128915918269189 18999061 11 22 32 219499529 <C(32) 32
32599084 128915937268247 3 11 22 32 <C(32) 329499530
32599085 128915937268254 6 11 22 12 (12)B> 329499530
32599086 128915975266374 18999066 11 22 129499531 (12)B>
32599087 128915975266380 18999068 11 22 129499532 (12)C>
32599088 128915975266385 18999065 11 22 129499532 <A(23) 20
32599089 128915994265449 1 11 22 <A(23) 239499532 20
32599090 128915994265451 -1 11 <A(33) 239499533 20
32599091 128915994265454 2 10 (32)B> 239499533 20
32599092 128915994265456 4 10 32 (22)B> 239499532 20
32599093 128916013264520 18999068 10 32 229499532 (22)B> 20
32599094 128916013264527 18999065 10 32 229499532 <C(33) 32
32599095 128916032263591 1 10 32 <C(33) 339499532 32
32599096 128916032263596 4 10 12 (32)B> 339499532 32
32599097 128916051262660 18999068 10 12 329499532 (32)B> 32
32599098 128916051262664 18999070 10 12 329499533 (12)B>
32599099 128916051262670 18999072 10 12 329499533 12 (12)C>
32599100 128916051262675 18999069 10 12 329499533 12 <A(23) 20
32599101 128916051262677 18999067 10 12 329499533 <A(23) 23 20
32599102 128916051262684 18999070 10 12 329499532 21 (23)C> 23 20
32599103 128916051262688 18999072 10 12 329499532 212 (23)C> 20
32599104 128916051262692 18999074 10 12 329499532 213 (20)C>
32599105 128916051262703 18999071 10 12 329499532 213 <C(32) 32
32599106 128916051262709 18999065 10 12 329499532 <C(32) 324
32599107 128916051262716 18999068 10 12 329499531 12 (12)B> 324
32599108 128916051262732 18999076 10 12 329499531 125 (12)B>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 11 22 322 121+V(1) (12)B>
1 6 2 11 22 322 122+V(1) (12)C>
2 11 -1 11 22 322 122+V(1) <A(23) 20
3 15+2*V(1) -5+-2*V(1) 11 22 322 <A(23) 232+V(1) 20
4 22+2*V(1) -2+-2*V(1) 11 22 32 21 (23)C> 232+V(1) 20
5 30+6*V(1) 2 11 22 32 213+V(1) (23)C> 20
6 34+6*V(1) 4 11 22 32 214+V(1) (20)C>
7 45+6*V(1) 1 11 22 32 214+V(1) <C(32) 32
8 53+8*V(1) -7+-2*V(1) 11 22 32 <C(32) 325+V(1)
9 60+8*V(1) -4+-2*V(1) 11 22 12 (12)B> 325+V(1)
10 80+12*V(1) 6 11 22 126+V(1) (12)B>
11 86+12*V(1) 8 11 22 127+V(1) (12)C>
12 91+12*V(1) 5 11 22 127+V(1) <A(23) 20
13 105+14*V(1) -9+-2*V(1) 11 22 <A(23) 237+V(1) 20
14 107+14*V(1) -11+-2*V(1) 11 <A(33) 238+V(1) 20
15 110+14*V(1) -8+-2*V(1) 10 (32)B> 238+V(1) 20
16 112+14*V(1) -6+-2*V(1) 10 32 (22)B> 237+V(1) 20
17 126+16*V(1) 8 10 32 227+V(1) (22)B> 20
18 133+16*V(1) 5 10 32 227+V(1) <C(33) 32
19 147+18*V(1) -9+-2*V(1) 10 32 <C(33) 337+V(1) 32
20 152+18*V(1) -6+-2*V(1) 10 12 (32)B> 337+V(1) 32
21 166+20*V(1) 8 10 12 327+V(1) (32)B> 32
22 170+20*V(1) 10 10 12 328+V(1) (12)B>
23 176+20*V(1) 12 10 12 328+V(1) 12 (12)C>
24 181+20*V(1) 9 10 12 328+V(1) 12 <A(23) 20
25 183+20*V(1) 7 10 12 328+V(1) <A(23) 23 20
26 190+20*V(1) 10 10 12 327+V(1) 21 (23)C> 23 20
27 194+20*V(1) 12 10 12 327+V(1) 212 (23)C> 20
28 198+20*V(1) 14 10 12 327+V(1) 213 (20)C>
29 209+20*V(1) 11 10 12 327+V(1) 213 <C(32) 32
30 215+20*V(1) 5 10 12 327+V(1) <C(32) 324
31 222+20*V(1) 8 10 12 326+V(1) 12 (12)B> 324
32 238+20*V(1) 16 10 12 326+V(1) 125 (12)B>
<< Success! ==> defined new CTR 17 (PPA)
32599108 128916051262732 18999076 10 12 329499531 125 (12)B>
== Executing PA-CTR 6, V(1)=4, V(2)=9499528, repcount=4749765, factor=5/2
80096758 805724543396452 47497666 10 12 32 1223748830 (12)B>
== Executing PPA-CTR 15 (once), V(1)=23748829
80096773 805724875880158 47497674 10 01 2323748834 21 (20)C>
== Executing PA-CTR 7, V(1)=0, V(2)=23748831, repcount=11874416, factor=5/2
210715349 5035777987339646 118744170 10 01 232 2159372081 (20)C>
== Executing PPA-CTR 16 (once), V(1)=59372080
210715371 5035779174781408 118744180 11 22 3259372087 12 (12)B>
== Executing PA-CTR 6, V(1)=0, V(2)=59372084, repcount=29686043, factor=5/2
507575801 31473615129019028 296860438 11 22 32 12148430216 (12)B>
507575802 31473615129019034 296860440 11 22 32 12148430217 (12)C>
507575803 31473615129019039 296860437 11 22 32 12148430217 <A(23) 20
507575804 31473615425879473 3 11 22 32 <A(23) 23148430217 20
507575805 31473615425879480 6 11 22 21 (23)C> 23148430217 20
507575806 31473616019600348 296860440 11 22 21148430218 (23)C> 20
507575807 31473616019600352 296860442 11 22 21148430219 (20)C>
507575808 31473616019600363 296860439 11 22 21148430219 <C(32) 32
507575809 31473616316460801 1 11 22 <C(32) 32148430220
507575810 31473616316460803 -1 11 <C(33) 32148430221
507575811 31473616316460808 2 02 (23)C> 32148430221
507575812 31473616316460810 4 02 23 (22)C> 32148430220
507575813 31473616613321250 296860444 02 23 22148430220 (22)C>
507575814 31473616613321255 296860441 02 23 22148430220 <A(33) 20
507575815 31473616910181695 1 02 23 <A(33) 33148430220 20
507575816 31473616910181698 4 02 21 (23)C> 33148430220 20
507575817 31473617207042138 296860444 02 21 23148430220 (23)C> 20
507575818 31473617207042142 296860446 02 21 23148430220 21 (20)C>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 11 22 32 121+V(1) (12)B>
1 6 2 11 22 32 122+V(1) (12)C>
2 11 -1 11 22 32 122+V(1) <A(23) 20
3 15+2*V(1) -5+-2*V(1) 11 22 32 <A(23) 232+V(1) 20
4 22+2*V(1) -2+-2*V(1) 11 22 21 (23)C> 232+V(1) 20
5 30+6*V(1) 2 11 22 213+V(1) (23)C> 20
6 34+6*V(1) 4 11 22 214+V(1) (20)C>
7 45+6*V(1) 1 11 22 214+V(1) <C(32) 32
8 53+8*V(1) -7+-2*V(1) 11 22 <C(32) 325+V(1)
9 55+8*V(1) -9+-2*V(1) 11 <C(33) 326+V(1)
10 60+8*V(1) -6+-2*V(1) 02 (23)C> 326+V(1)
11 62+8*V(1) -4+-2*V(1) 02 23 (22)C> 325+V(1)
12 72+10*V(1) 6 02 23 225+V(1) (22)C>
13 77+10*V(1) 3 02 23 225+V(1) <A(33) 20
14 87+12*V(1) -7+-2*V(1) 02 23 <A(33) 335+V(1) 20
15 90+12*V(1) -4+-2*V(1) 02 21 (23)C> 335+V(1) 20
16 100+14*V(1) 6 02 21 235+V(1) (23)C> 20
17 104+14*V(1) 8 02 21 235+V(1) 21 (20)C>
<< Success! ==> defined new CTR 18 (PPA)
507575818 31473617207042142 296860446 02 21 23148430220 21 (20)C>
== Executing PA-CTR 7, V(1)=0, V(2)=148430217, repcount=74215109, factor=5/2
1323942017 1967100[4]3672714 742151100 02 21 232 21371075546 (20)C>
1323942018 1967100[4]3672725 742151097 02 21 232 21371075546 <C(32) 32
1323942019 1967100[4]5823817 5 02 21 232 <C(32) 32371075547
1323942020 1967100[4]5823822 8 02 21 23 22 (12)B> 32371075547
1323942021 1967100[4]0126010 742151102 02 21 23 22 12371075547 (12)B>
1323942022 1967100[4]0126016 742151104 02 21 23 22 12371075548 (12)C>
1323942023 1967100[4]0126021 742151101 02 21 23 22 12371075548 <A(23) 20
1323942024 1967100[4]2277117 5 02 21 23 22 <A(23) 23371075548 20
1323942025 1967100[4]2277119 3 02 21 23 <A(33) 23371075549 20
1323942026 1967100[4]2277122 6 02 212 (23)C> 23371075549 20
1323942027 1967100[4]6579318 742151104 02 21371075551 (23)C> 20
1323942028 1967100[4]6579322 742151106 02 21371075552 (20)C>
1323942029 1967100[4]6579333 742151103 02 21371075552 <C(32) 32
1323942030 1967100[4]8730437 -1 02 <C(32) 32371075553
1323942031 1967100[4]8730442 2 13 (22)C> 32371075553
1323942032 1967100[4]0881548 742151108 13 22371075553 (22)C>
1323942033 1967100[4]0881553 742151105 13 22371075553 <A(33) 20
1323942034 1967100[4]3032659 -1 13 <A(33) 33371075553 20
1323942035 1967100[4]3032662 2 11 (23)C> 33371075553 20
1323942036 1967100[4]5183768 742151108 11 23371075553 (23)C> 20
1323942037 1967100[4]5183772 742151110 11 23371075553 21 (20)C>
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 02 211+V(2) 232 211+V(1) (20)C>
1 11 -3 02 211+V(2) 232 211+V(1) <C(32) 32
2 13+2*V(1) -5+-2*V(1) 02 211+V(2) 232 <C(32) 322+V(1)
3 18+2*V(1) -2+-2*V(1) 02 211+V(2) 23 22 (12)B> 322+V(1)
4 26+6*V(1) 2 02 211+V(2) 23 22 122+V(1) (12)B>
5 32+6*V(1) 4 02 211+V(2) 23 22 123+V(1) (12)C>
6 37+6*V(1) 1 02 211+V(2) 23 22 123+V(1) <A(23) 20
7 43+8*V(1) -5+-2*V(1) 02 211+V(2) 23 22 <A(23) 233+V(1) 20
8 45+8*V(1) -7+-2*V(1) 02 211+V(2) 23 <A(33) 234+V(1) 20
9 48+8*V(1) -4+-2*V(1) 02 212+V(2) (23)C> 234+V(1) 20
10 64+12*V(1) 4 02 216+V(1)+V(2) (23)C> 20
11 68+12*V(1) 6 02 217+V(1)+V(2) (20)C>
12 79+12*V(1) 3 02 217+V(1)+V(2) <C(32) 32
13 93+14*V(1)+2*V(2) -11+-2*V(1)+-2*V(2) 02 <C(32) 328+V(1)+V(2)
14 98+14*V(1)+2*V(2) -8+-2*V(1)+-2*V(2) 13 (22)C> 328+V(1)+V(2)
15 114+16*V(1)+4*V(2) 8 13 228+V(1)+V(2) (22)C>
16 119+16*V(1)+4*V(2) 5 13 228+V(1)+V(2) <A(33) 20
17 135+18*V(1)+6*V(2) -11+-2*V(1)+-2*V(2) 13 <A(33) 338+V(1)+V(2) 20
18 138+18*V(1)+6*V(2) -8+-2*V(1)+-2*V(2) 11 (23)C> 338+V(1)+V(2) 20
19 154+20*V(1)+8*V(2) 8 11 238+V(1)+V(2) (23)C> 20
20 158+20*V(1)+8*V(2) 10 11 238+V(1)+V(2) 21 (20)C>
<< Success! ==> defined new CTR 19 (PPA)
1323942037 1967100[4]5183772 742151110 11 23371075553 21 (20)C>
== Executing PA-CTR 2, V(1)=0, V(2)=371075550, repcount=185537776, factor=5/2
3364857573 1229438[5]6404540 1855377766 11 23 21927688881 (20)C>
== Executing PPA-CTR 14 (once), V(1)=927688879
3364857599 1229438[5]4049012 1855377778 10 12 32927688882 125 (12)B>
== Executing PA-CTR 6, V(1)=4, V(2)=927688879, repcount=463844440, factor=5/2
8003301999 7683988[5]8212132 4638444418 10 12 322 122319222205 (12)B>
8003302000 7683988[5]8212138 4638444420 10 12 322 122319222206 (12)C>
8003302001 7683988[5]8212143 4638444417 10 12 322 122319222206 <A(23) 20
8003302002 7683988[5]6656555 5 10 12 322 <A(23) 232319222206 20
8003302003 7683988[5]6656562 8 10 12 32 21 (23)C> 232319222206 20
8003302004 7683988[5]3545386 4638444420 10 12 32 212319222207 (23)C> 20
8003302005 7683988[5]3545390 4638444422 10 12 32 212319222208 (20)C>
8003302006 7683988[5]3545401 4638444419 10 12 32 212319222208 <C(32) 32
8003302007 7683988[5]1989817 3 10 12 32 <C(32) 322319222209
8003302008 7683988[5]1989824 6 10 122 (12)B> 322319222209
8003302009 7683988[5]8878660 4638444424 10 122319222211 (12)B>
8003302010 7683988[5]8878666 4638444426 10 122319222212 (12)C>
8003302011 7683988[5]8878671 4638444423 10 122319222212 <A(23) 20
8003302012 7683988[5]7323095 -1 10 <A(23) 232319222212 20
8003302013 7683988[5]7323098 2 11 (22)B> 232319222212 20
8003302014 7683988[5]5767522 4638444426 11 222319222212 (22)B> 20
8003302015 7683988[5]5767529 4638444423 11 222319222212 <C(33) 32
8003302016 7683988[5]4211953 -1 11 <C(33) 332319222212 32
8003302017 7683988[5]4211958 2 02 (23)C> 332319222212 32
8003302018 7683988[5]2656382 4638444426 02 232319222212 (23)C> 32
8003302019 7683988[5]2656384 4638444428 02 232319222213 (22)C>
8003302020 7683988[5]2656389 4638444425 02 232319222213 <A(33) 20
8003302021 7683988[5]2656392 4638444428 02 232319222212 21 (23)C> 20
8003302022 7683988[5]2656396 4638444430 02 232319222212 212 (20)C>
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 10 121+V(2) 322 121+V(1) (12)B>
1 6 2 10 121+V(2) 322 122+V(1) (12)C>
2 11 -1 10 121+V(2) 322 122+V(1) <A(23) 20
3 15+2*V(1) -5+-2*V(1) 10 121+V(2) 322 <A(23) 232+V(1) 20
4 22+2*V(1) -2+-2*V(1) 10 121+V(2) 32 21 (23)C> 232+V(1) 20
5 30+6*V(1) 2 10 121+V(2) 32 213+V(1) (23)C> 20
6 34+6*V(1) 4 10 121+V(2) 32 214+V(1) (20)C>
7 45+6*V(1) 1 10 121+V(2) 32 214+V(1) <C(32) 32
8 53+8*V(1) -7+-2*V(1) 10 121+V(2) 32 <C(32) 325+V(1)
9 60+8*V(1) -4+-2*V(1) 10 122+V(2) (12)B> 325+V(1)
10 80+12*V(1) 6 10 127+V(1)+V(2) (12)B>
11 86+12*V(1) 8 10 128+V(1)+V(2) (12)C>
12 91+12*V(1) 5 10 128+V(1)+V(2) <A(23) 20
13 107+14*V(1)+2*V(2) -11+-2*V(1)+-2*V(2) 10 <A(23) 238+V(1)+V(2) 20
14 110+14*V(1)+2*V(2) -8+-2*V(1)+-2*V(2) 11 (22)B> 238+V(1)+V(2) 20
15 126+16*V(1)+4*V(2) 8 11 228+V(1)+V(2) (22)B> 20
16 133+16*V(1)+4*V(2) 5 11 228+V(1)+V(2) <C(33) 32
17 149+18*V(1)+6*V(2) -11+-2*V(1)+-2*V(2) 11 <C(33) 338+V(1)+V(2) 32
18 154+18*V(1)+6*V(2) -8+-2*V(1)+-2*V(2) 02 (23)C> 338+V(1)+V(2) 32
19 170+20*V(1)+8*V(2) 8 02 238+V(1)+V(2) (23)C> 32
20 172+20*V(1)+8*V(2) 10 02 239+V(1)+V(2) (22)C>
21 177+20*V(1)+8*V(2) 7 02 239+V(1)+V(2) <A(33) 20
22 180+20*V(1)+8*V(2) 10 02 238+V(1)+V(2) 21 (23)C> 20
23 184+20*V(1)+8*V(2) 12 02 238+V(1)+V(2) 212 (20)C>
<< Success! ==> defined new CTR 20 (PPA)
8003302022 7683988[5]2656396 4638444430 02 232319222212 212 (20)C>
== Executing PA-CTR 2, V(1)=1, V(2)=2319222209, repcount=1159611105, factor=5/2
20759024177 4802492[6]2842396 11596111060 02 232 215798055527 (20)C>
20759024178 4802492[6]2842407 11596111057 02 232 215798055527 <C(32) 32
20759024179 4802492[6]8953461 3 02 232 <C(32) 325798055528
20759024180 4802492[6]8953466 6 02 23 22 (12)B> 325798055528
20759024181 4802492[6]1175578 11596111062 02 23 22 125798055528 (12)B>
20759024182 4802492[6]1175584 11596111064 02 23 22 125798055529 (12)C>
20759024183 4802492[6]1175589 11596111061 02 23 22 125798055529 <A(23) 20
20759024184 4802492[6]7286647 3 02 23 22 <A(23) 235798055529 20
20759024185 4802492[6]7286649 1 02 23 <A(33) 235798055530 20
20759024186 4802492[6]7286652 4 02 21 (23)C> 235798055530 20
20759024187 4802492[6]9508772 11596111064 02 215798055531 (23)C> 20
20759024188 4802492[6]9508776 11596111066 02 215798055532 (20)C>
20759024189 4802492[6]9508787 11596111063 02 215798055532 <C(32) 32
20759024190 4802492[6]5619851 -1 02 <C(32) 325798055533
20759024191 4802492[6]5619856 2 13 (22)C> 325798055533
20759024192 4802492[6]1730922 11596111068 13 225798055533 (22)C>
20759024193 4802492[6]1730927 11596111065 13 225798055533 <A(33) 20
20759024194 4802492[6]7841993 -1 13 <A(33) 335798055533 20
20759024195 4802492[6]7841996 2 11 (23)C> 335798055533 20
20759024196 4802492[6]3953062 11596111068 11 235798055533 (23)C> 20
20759024197 4802492[6]3953066 11596111070 11 235798055533 21 (20)C>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 02 232 211+V(1) (20)C>
1 11 -3 02 232 211+V(1) <C(32) 32
2 13+2*V(1) -5+-2*V(1) 02 232 <C(32) 322+V(1)
3 18+2*V(1) -2+-2*V(1) 02 23 22 (12)B> 322+V(1)
4 26+6*V(1) 2 02 23 22 122+V(1) (12)B>
5 32+6*V(1) 4 02 23 22 123+V(1) (12)C>
6 37+6*V(1) 1 02 23 22 123+V(1) <A(23) 20
7 43+8*V(1) -5+-2*V(1) 02 23 22 <A(23) 233+V(1) 20
8 45+8*V(1) -7+-2*V(1) 02 23 <A(33) 234+V(1) 20
9 48+8*V(1) -4+-2*V(1) 02 21 (23)C> 234+V(1) 20
10 64+12*V(1) 4 02 215+V(1) (23)C> 20
11 68+12*V(1) 6 02 216+V(1) (20)C>
12 79+12*V(1) 3 02 216+V(1) <C(32) 32
13 91+14*V(1) -9+-2*V(1) 02 <C(32) 327+V(1)
14 96+14*V(1) -6+-2*V(1) 13 (22)C> 327+V(1)
15 110+16*V(1) 8 13 227+V(1) (22)C>
16 115+16*V(1) 5 13 227+V(1) <A(33) 20
17 129+18*V(1) -9+-2*V(1) 13 <A(33) 337+V(1) 20
18 132+18*V(1) -6+-2*V(1) 11 (23)C> 337+V(1) 20
19 146+20*V(1) 8 11 237+V(1) (23)C> 20
20 150+20*V(1) 10 11 237+V(1) 21 (20)C>
<< Success! ==> defined new CTR 21 (PPA)
20759024197 4802492[6]3953066 11596111070 11 235798055533 21 (20)C>
== Executing PA-CTR 2, V(1)=0, V(2)=5798055530, repcount=2899027766, factor=5/2
52648329623 3001557[7]5530854 28990277666 11 23 2114495138831 (20)C>
== Executing PPA-CTR 14 (once), V(1)=14495138829
52648329649 3001557[7]7474626 28990277678 10 12 3214495138832 125 (12)B>
== Executing PA-CTR 6, V(1)=4, V(2)=14495138829, repcount=7247569415, factor=5/2
125124023799 1875973[8]2544046 72475694168 10 12 322 1236237847080 (12)B>
== Executing PPA-CTR 20 (once), V(1)=36237847079, V(2)=0
125124023822 1875973[8]9485810 72475694180 02 2336237847087 212 (20)C>
== Executing PA-CTR 2, V(1)=1, V(2)=36237847084, repcount=18118923543, factor=5/2
324432182795 1172483[9]5848430 181189235438 02 23 2190594617717 (20)C>
324432182796 1172483[9]5848441 181189235435 02 23 2190594617717 <C(32) 32
324432182797 1172483[9]5083875 1 02 23 <C(32) 3290594617718
324432182798 1172483[9]5083880 4 02 22 (12)B> 3290594617718
324432182799 1172483[9]3554752 181189235440 02 22 1290594617718 (12)B>
324432182800 1172483[9]3554758 181189235442 02 22 1290594617719 (12)C>
324432182801 1172483[9]3554763 181189235439 02 22 1290594617719 <A(23) 20
324432182802 1172483[9]2790201 1 02 22 <A(23) 2390594617719 20
324432182803 1172483[9]2790203 -1 02 <A(33) 2390594617720 20
324432182804 1172483[9]2790205 -3 <B(13) 33 2390594617720 20
324432182805 1172483[9]2790210 0 01 (22)B> 33 2390594617720 20
324432182806 1172483[9]2790212 2 01 22 (32)B> 2390594617720 20
324432182807 1172483[9]2790214 4 01 22 32 (22)B> 2390594617719 20
324432182808 1172483[9]2025652 181189235442 01 22 32 2290594617719 (22)B> 20
324432182809 1172483[9]2025659 181189235439 01 22 32 2290594617719 <C(33) 32
324432182810 1172483[9]1261097 1 01 22 32 <C(33) 3390594617719 32
324432182811 1172483[9]1261102 4 01 22 12 (32)B> 3390594617719 32
324432182812 1172483[9]0496540 181189235442 01 22 12 3290594617719 (32)B> 32
324432182813 1172483[9]0496544 181189235444 01 22 12 3290594617720 (12)B>
324432182814 1172483[9]0496550 181189235446 01 22 12 3290594617720 12 (12)C>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 02 23 211+V(1) (20)C>
1 11 -3 02 23 211+V(1) <C(32) 32
2 13+2*V(1) -5+-2*V(1) 02 23 <C(32) 322+V(1)
3 18+2*V(1) -2+-2*V(1) 02 22 (12)B> 322+V(1)
4 26+6*V(1) 2 02 22 122+V(1) (12)B>
5 32+6*V(1) 4 02 22 123+V(1) (12)C>
6 37+6*V(1) 1 02 22 123+V(1) <A(23) 20
7 43+8*V(1) -5+-2*V(1) 02 22 <A(23) 233+V(1) 20
8 45+8*V(1) -7+-2*V(1) 02 <A(33) 234+V(1) 20
9 47+8*V(1) -9+-2*V(1) <B(13) 33 234+V(1) 20
10 52+8*V(1) -6+-2*V(1) 01 (22)B> 33 234+V(1) 20
11 54+8*V(1) -4+-2*V(1) 01 22 (32)B> 234+V(1) 20
12 56+8*V(1) -2+-2*V(1) 01 22 32 (22)B> 233+V(1) 20
13 62+10*V(1) 4 01 22 32 223+V(1) (22)B> 20
14 69+10*V(1) 1 01 22 32 223+V(1) <C(33) 32
15 75+12*V(1) -5+-2*V(1) 01 22 32 <C(33) 333+V(1) 32
16 80+12*V(1) -2+-2*V(1) 01 22 12 (32)B> 333+V(1) 32
17 86+14*V(1) 4 01 22 12 323+V(1) (32)B> 32
18 90+14*V(1) 6 01 22 12 324+V(1) (12)B>
19 96+14*V(1) 8 01 22 12 324+V(1) 12 (12)C>
<< Success! ==> defined new CTR 22 (PPA)
324432182814 1172483[9]0496550 181189235446 01 22 12 3290594617720 12 (12)C>
== Executing PA-CTR 8, V(1)=0, V(2)=90594617717, repcount=45297308859, factor=5/2
777405271404 7328022[9]4689622 452973088600 01 22 12 322 12226486544296 (12)C>
777405271405 7328022[9]4689627 452973088597 01 22 12 322 12226486544296 <A(23) 20
777405271406 7328022[9]7778219 5 01 22 12 322 <A(23) 23226486544296 20
777405271407 7328022[9]7778226 8 01 22 12 32 21 (23)C> 23226486544296 20
777405271408 7328022[9]3955410 452973088600 01 22 12 32 21226486544297 (23)C> 20
777405271409 7328022[9]3955414 452973088602 01 22 12 32 21226486544298 (20)C>
777405271410 7328022[9]3955425 452973088599 01 22 12 32 21226486544298 <C(32) 32
777405271411 7328022[9]7044021 3 01 22 12 32 <C(32) 32226486544299
777405271412 7328022[9]7044028 6 01 22 122 (12)B> 32226486544299
777405271413 7328022[9]3221224 452973088604 01 22 12226486544301 (12)B>
777405271414 7328022[9]3221230 452973088606 01 22 12226486544302 (12)C>
777405271415 7328022[9]3221235 452973088603 01 22 12226486544302 <A(23) 20
777405271416 7328022[9]6309839 -1 01 22 <A(23) 23226486544302 20
777405271417 7328022[9]6309841 -3 01 <A(33) 23226486544303 20
777405271418 7328022[9]6309844 0 (32)B> 23226486544303 20
777405271419 7328022[9]6309846 2 32 (22)B> 23226486544302 20
777405271420 7328022[9]9398450 452973088606 32 22226486544302 (22)B> 20
777405271421 7328022[9]9398457 452973088603 32 22226486544302 <C(33) 32
777405271422 7328022[9]2487061 -1 32 <C(33) 33226486544302 32
777405271423 7328022[9]2487066 2 12 (32)B> 33226486544302 32
777405271424 7328022[9]5575670 452973088606 12 32226486544302 (32)B> 32
777405271425 7328022[9]5575674 452973088608 12 32226486544303 (12)B>
777405271426 7328022[9]5575680 452973088610 12 32226486544303 12 (12)C>
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 01 22 121+V(2) 322 121+V(1) (12)C>
1 5 -3 01 22 121+V(2) 322 121+V(1) <A(23) 20
2 7+2*V(1) -5+-2*V(1) 01 22 121+V(2) 322 <A(23) 231+V(1) 20
3 14+2*V(1) -2+-2*V(1) 01 22 121+V(2) 32 21 (23)C> 231+V(1) 20
4 18+6*V(1) 0 01 22 121+V(2) 32 212+V(1) (23)C> 20
5 22+6*V(1) 2 01 22 121+V(2) 32 213+V(1) (20)C>
6 33+6*V(1) -1 01 22 121+V(2) 32 213+V(1) <C(32) 32
7 39+8*V(1) -7+-2*V(1) 01 22 121+V(2) 32 <C(32) 324+V(1)
8 46+8*V(1) -4+-2*V(1) 01 22 122+V(2) (12)B> 324+V(1)
9 62+12*V(1) 4 01 22 126+V(1)+V(2) (12)B>
10 68+12*V(1) 6 01 22 127+V(1)+V(2) (12)C>
11 73+12*V(1) 3 01 22 127+V(1)+V(2) <A(23) 20
12 87+14*V(1)+2*V(2) -11+-2*V(1)+-2*V(2) 01 22 <A(23) 237+V(1)+V(2) 20
13 89+14*V(1)+2*V(2) -13+-2*V(1)+-2*V(2) 01 <A(33) 238+V(1)+V(2) 20
14 92+14*V(1)+2*V(2) -10+-2*V(1)+-2*V(2) (32)B> 238+V(1)+V(2) 20
15 94+14*V(1)+2*V(2) -8+-2*V(1)+-2*V(2) 32 (22)B> 237+V(1)+V(2) 20
16 108+16*V(1)+4*V(2) 6 32 227+V(1)+V(2) (22)B> 20
17 115+16*V(1)+4*V(2) 3 32 227+V(1)+V(2) <C(33) 32
18 129+18*V(1)+6*V(2) -11+-2*V(1)+-2*V(2) 32 <C(33) 337+V(1)+V(2) 32
19 134+18*V(1)+6*V(2) -8+-2*V(1)+-2*V(2) 12 (32)B> 337+V(1)+V(2) 32
20 148+20*V(1)+8*V(2) 6 12 327+V(1)+V(2) (32)B> 32
21 152+20*V(1)+8*V(2) 8 12 328+V(1)+V(2) (12)B>
22 158+20*V(1)+8*V(2) 10 12 328+V(1)+V(2) 12 (12)C>
<< Success! ==> defined new CTR 23 (PPA)
777405271426 7328022[9]5575680 452973088610 12 32226486544303 12 (12)C>
== Executing PA-CTR 1, V(1)=0, V(2)=226486544300, repcount=113243272151, factor=5/2
1909837992936 4580013[10]4921448 1132432721516 12 32 12566216360756 (12)C>
1909837992937 4580013[10]4921453 1132432721513 12 32 12566216360756 <A(23) 20
1909837992938 4580013[10]7642965 1 12 32 <A(23) 23566216360756 20
1909837992939 4580013[10]7642972 4 12 21 (23)C> 23566216360756 20
1909837992940 4580013[10]3085996 1132432721516 12 21566216360757 (23)C> 20
1909837992941 4580013[10]3086000 1132432721518 12 21566216360758 (20)C>
1909837992942 4580013[10]3086011 1132432721515 12 21566216360758 <C(32) 32
1909837992943 4580013[10]5807527 -1 12 <C(32) 32566216360759
1909837992944 4580013[10]5807532 2 03 (22)C> 32566216360759
1909837992945 4580013[10]8529050 1132432721520 03 22566216360759 (22)C>
1909837992946 4580013[10]8529055 1132432721517 03 22566216360759 <A(33) 20
1909837992947 4580013[10]1250573 -1 03 <A(33) 33566216360759 20
1909837992948 4580013[10]1250576 2 01 (23)C> 33566216360759 20
1909837992949 4580013[10]3972094 1132432721520 01 23566216360759 (23)C> 20
1909837992950 4580013[10]3972098 1132432721522 01 23566216360759 21 (20)C>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 12 32 121+V(1) (12)C>
1 5 -3 12 32 121+V(1) <A(23) 20
2 7+2*V(1) -5+-2*V(1) 12 32 <A(23) 231+V(1) 20
3 14+2*V(1) -2+-2*V(1) 12 21 (23)C> 231+V(1) 20
4 18+6*V(1) 0 12 212+V(1) (23)C> 20
5 22+6*V(1) 2 12 213+V(1) (20)C>
6 33+6*V(1) -1 12 213+V(1) <C(32) 32
7 39+8*V(1) -7+-2*V(1) 12 <C(32) 324+V(1)
8 44+8*V(1) -4+-2*V(1) 03 (22)C> 324+V(1)
9 52+10*V(1) 4 03 224+V(1) (22)C>
10 57+10*V(1) 1 03 224+V(1) <A(33) 20
11 65+12*V(1) -7+-2*V(1) 03 <A(33) 334+V(1) 20
12 68+12*V(1) -4+-2*V(1) 01 (23)C> 334+V(1) 20
13 76+14*V(1) 4 01 234+V(1) (23)C> 20
14 80+14*V(1) 6 01 234+V(1) 21 (20)C>
<< Success! ==> defined new CTR 24 (PPA)
1909837992950 4580013[10]3972098 1132432721522 01 23566216360759 21 (20)C>
== Executing PA-CTR 2, V(1)=0, V(2)=566216360756, repcount=283108180379, factor=5/2
5024027977119 2862508[11]2335730 2831081803796 01 23 211415540901896 (20)C>
== Executing PPA-CTR 3 (once), V(1)=1415540901895
5024027977136 2862508[11]4962350 2831081803804 12 321415540901899 12 (12)C>
== Executing PA-CTR 1, V(1)=0, V(2)=1415540901896, repcount=707770450949, factor=5/2
12101732486626 1789067[12]2116442 7077704509498 12 32 123538852254746 (12)C>
== Executing PPA-CTR 24 (once), V(1)=3538852254745
12101732486640 1789067[12]3682952 7077704509504 01 233538852254749 21 (20)C>
== Executing PA-CTR 2, V(1)=0, V(2)=3538852254746, repcount=1769426127374, factor=5/2
31565419887754 1118167[13]0599444 17694261273748 01 23 218847130636871 (20)C>
== Executing PPA-CTR 3 (once), V(1)=8847130636870
31565419887771 1118167[13]9515714 17694261273756 12 328847130636874 12 (12)C>
== Executing PA-CTR 1, V(1)=0, V(2)=8847130636871, repcount=4423565318436, factor=5/2
75801073072131 6988546[13]6199162 44235653184372 12 322 1222117826592181 (12)C>
== Executing PPA-CTR 4 (once), V(1)=22117826592180, V(2)=0
75801073072153 6988546[13]8042920 44235653184382 12 2322117826592187 212 (20)C>
== Executing PA-CTR 2, V(1)=1, V(2)=22117826592184, repcount=11058913296093, factor=5/2
197449119329176 4367841[14]4787040 110589132960940 12 23 2155294566480467 (20)C>
197449119329177 4367841[14]4787051 110589132960937 12 23 2155294566480467 <C(32) 32
197449119329178 4367841[14]7747985 3 12 23 <C(32) 3255294566480468
197449119329179 4367841[14]7747990 6 12 22 (12)B> 3255294566480468
197449119329180 4367841[14]3669862 110589132960942 12 22 1255294566480468 (12)B>
197449119329181 4367841[14]3669868 110589132960944 12 22 1255294566480469 (12)C>
197449119329182 4367841[14]3669873 110589132960941 12 22 1255294566480469 <A(23) 20
197449119329183 4367841[14]6630811 3 12 22 <A(23) 2355294566480469 20
197449119329184 4367841[14]6630813 1 12 <A(33) 2355294566480470 20
197449119329185 4367841[14]6630815 -1 <A(23) 33 2355294566480470 20
197449119329186 4367841[14]6630818 2 01 (22)B> 33 2355294566480470 20
197449119329187 4367841[14]6630820 4 01 22 (32)B> 2355294566480470 20
197449119329188 4367841[14]6630822 6 01 22 32 (22)B> 2355294566480469 20
197449119329189 4367841[14]9591760 110589132960944 01 22 32 2255294566480469 (22)B> 20
197449119329190 4367841[14]9591767 110589132960941 01 22 32 2255294566480469 <C(33) 32
197449119329191 4367841[14]2552705 3 01 22 32 <C(33) 3355294566480469 32
197449119329192 4367841[14]2552710 6 01 22 12 (32)B> 3355294566480469 32
197449119329193 4367841[14]5513648 110589132960944 01 22 12 3255294566480469 (32)B> 32
197449119329194 4367841[14]5513652 110589132960946 01 22 12 3255294566480470 (12)B>
197449119329195 4367841[14]5513658 110589132960948 01 22 12 3255294566480470 12 (12)C>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 12 23 211+V(1) (20)C>
1 11 -3 12 23 211+V(1) <C(32) 32
2 13+2*V(1) -5+-2*V(1) 12 23 <C(32) 322+V(1)
3 18+2*V(1) -2+-2*V(1) 12 22 (12)B> 322+V(1)
4 26+6*V(1) 2 12 22 122+V(1) (12)B>
5 32+6*V(1) 4 12 22 123+V(1) (12)C>
6 37+6*V(1) 1 12 22 123+V(1) <A(23) 20
7 43+8*V(1) -5+-2*V(1) 12 22 <A(23) 233+V(1) 20
8 45+8*V(1) -7+-2*V(1) 12 <A(33) 234+V(1) 20
9 47+8*V(1) -9+-2*V(1) <A(23) 33 234+V(1) 20
10 50+8*V(1) -6+-2*V(1) 01 (22)B> 33 234+V(1) 20
11 52+8*V(1) -4+-2*V(1) 01 22 (32)B> 234+V(1) 20
12 54+8*V(1) -2+-2*V(1) 01 22 32 (22)B> 233+V(1) 20
13 60+10*V(1) 4 01 22 32 223+V(1) (22)B> 20
14 67+10*V(1) 1 01 22 32 223+V(1) <C(33) 32
15 73+12*V(1) -5+-2*V(1) 01 22 32 <C(33) 333+V(1) 32
16 78+12*V(1) -2+-2*V(1) 01 22 12 (32)B> 333+V(1) 32
17 84+14*V(1) 4 01 22 12 323+V(1) (32)B> 32
18 88+14*V(1) 6 01 22 12 324+V(1) (12)B>
19 94+14*V(1) 8 01 22 12 324+V(1) 12 (12)C>
<< Success! ==> defined new CTR 25 (PPA)
197449119329195 4367841[14]5513658 110589132960948 01 22 12 3255294566480470 12 (12)C>
== Executing PA-CTR 8, V(1)=0, V(2)=55294566480467, repcount=27647283240234, factor=5/2
473921951731535 2729900[15]9885230 276472832402352 01 22 12 322 12138236416201171 (12)C>
== Executing PPA-CTR 23 (once), V(1)=138236416201170, V(2)=0
473921951731557 2729900[15]3908788 276472832402362 12 32138236416201178 12 (12)C>
== Executing PA-CTR 1, V(1)=0, V(2)=138236416201175, repcount=69118208100588, factor=5/2
1165104032737437 1706188[16]0103452 691182081005890 12 322 12345591040502941 (12)C>
== Executing PPA-CTR 4 (once), V(1)=345591040502940, V(2)=0
1165104032737459 1706188[16]0162410 691182081005900 12 23345591040502947 212 (20)C>
== Executing PA-CTR 2, V(1)=1, V(2)=345591040502944, repcount=172795520251473, factor=5/2
3065854755503662 1066367[17]2827930 1727955202514738 12 23 21863977601257367 (20)C>
== Executing PPA-CTR 25 (once), V(1)=863977601257366
3065854755503681 1066367[17]0431148 1727955202514746 01 22 12 32863977601257370 12 (12)C>
== Executing PA-CTR 8, V(1)=0, V(2)=863977601257367, repcount=431988800628684, factor=5/2
7385742761790521 6664797[17]1476820 4319888006286850 01 22 12 322 122159944003143421 (12)C>
== Executing PPA-CTR 23 (once), V(1)=2159944003143420, V(2)=0
7385742761790543 6664797[17]4345378 4319888006286860 12 322159944003143428 12 (12)C>
== Executing PA-CTR 1, V(1)=0, V(2)=2159944003143425, repcount=1079972001571713, factor=5/2
18185462777507673 4165498[18]6701542 10799720015717138 12 322 125399860007858566 (12)C>
== Executing PPA-CTR 4 (once), V(1)=5399860007858565, V(2)=0
18185462777507695 4165498[18]3873000 10799720015717148 12 235399860007858572 212 (20)C>
== Executing PA-CTR 2, V(1)=1, V(2)=5399860007858569, repcount=2699930003929285, factor=5/2
47884692820729830 2603436[19]8674000 26999300039292858 12 232 2113499650019646427 (20)C>
== Executing PPA-CTR 5 (once), V(1)=13499650019646426
47884692820729850 2603436[19]1602670 26999300039292868 01 2313499650019646433 21 (20)C>
== Executing PA-CTR 2, V(1)=0, V(2)=13499650019646430, repcount=6749825009823216, factor=5/2
1221327[4]8785226 1627147[20]2364558 67498250098232164 01 23 2133749125049116081 (20)C>
== Executing PPA-CTR 3 (once), V(1)=33749125049116080
1221327[4]8785243 1627147[20]9989768 67498250098232172 12 3233749125049116084 12 (12)C>
== Executing PA-CTR 1, V(1)=0, V(2)=33749125049116081, repcount=16874562524558041, factor=5/2
2908783[4]4365653 1016967[21]5925756 1687456[4]5580418 12 322 1284372812622790206 (12)C>
== Executing PPA-CTR 4 (once), V(1)=84372812622790205, V(2)=0
2908783[4]4365675 1016967[21]1730014 1687456[4]5580428 12 2384372812622790212 212 (20)C>
== Executing PA-CTR 2, V(1)=1, V(2)=84372812622790209, repcount=42186406311395105, factor=5/2
7549288[4]9711830 6356045[21]0316014 4218640[4]3951058 12 232 212109320[4]6975527 (20)C>
== Executing PPA-CTR 5 (once), V(1)=2109320[4]6975526
7549288[4]9711850 6356045[21]9826684 4218640[4]3951068 01 232109320[4]6975533 21 (20)C>
== Executing PA-CTR 2, V(1)=0, V(2)=2109320[4]6975530, repcount=1054660[4]8487766, factor=5/2
1915055[5]3077276 3972528[22]2484472 1054660[5]4877664 01 23 215273300[4]2438831 (20)C>
== Executing PPA-CTR 3 (once), V(1)=5273300[4]2438830
1915055[5]3077293 3972528[22]6628182 1054660[5]4877672 12 325273300[4]2438834 12 (12)C>
== Executing PA-CTR 1, V(1)=0, V(2)=5273300[4]2438831, repcount=2636650[4]6219416, factor=5/2
4551705[5]5271453 2482830[23]4397670 2636650[5]2194168 12 322 121318325[5]1097081 (12)C>
== Executing PPA-CTR 4 (once), V(1)=1318325[5]1097080, V(2)=0
4551705[5]5271475 2482830[23]6339428 2636650[5]2194178 12 231318325[5]1097087 212 (20)C>
== Executing PA-CTR 2, V(1)=1, V(2)=1318325[5]1097084, repcount=6591625[4]5548543, factor=5/2
1180249[6]6305448 1551769[24]6452048 6591625[5]5485436 12 23 213295812[5]7742717 (20)C>
== Executing PPA-CTR 25 (once), V(1)=3295812[5]7742716
1180249[6]6305467 1551769[24]4850166 6591625[5]5485444 01 22 12 323295812[5]7742720 12 (12)C>
== Executing PA-CTR 8, V(1)=0, V(2)=3295812[5]7742717, repcount=1647906[5]8871359, factor=5/2
2828155[6]5019057 9698556[24]7168238 1647906[6]8713598 01 22 12 322 128239532[5]4356796 (12)C>
== Executing PPA-CTR 23 (once), V(1)=8239532[5]4356795, V(2)=0
2828155[6]5019079 9698556[24]4304296 1647906[6]8713608 12 328239532[5]4356803 12 (12)C>
== Executing PA-CTR 1, V(1)=0, V(2)=8239532[5]4356800, repcount=4119766[5]7178401, factor=5/2
6947922[6]6803089 6061597[25]4587564 4119766[6]1784014 12 32 122059883[6]5892006 (12)C>
== Executing PPA-CTR 24 (once), V(1)=2059883[6]5892005
6947922[6]6803103 6061597[25]7075714 4119766[6]1784020 01 232059883[6]5892009 21 (20)C>
== Executing PA-CTR 2, V(1)=0, V(2)=2059883[6]5892006, repcount=1029941[6]7946004, factor=5/2
1827727[7]4209147 3788498[26]6064346 1029941[7]9460044 01 23 215149707[6]9730021 (20)C>
== Executing PPA-CTR 3 (once), V(1)=5149707[6]9730020
1827727[7]4209164 3788498[26]2284716 1029941[7]9460052 12 325149707[6]9730024 12 (12)C>
== Executing PA-CTR 1, V(1)=0, V(2)=5149707[6]9730021, repcount=2574853[6]9865011, factor=5/2
4402581[7]2859274 2367811[27]8058764 2574853[7]8650118 12 322 121287426[7]9325056 (12)C>
== Executing PPA-CTR 4 (once), V(1)=1287426[7]9325055, V(2)=0
4402581[7]2859296 2367811[27]4560022 2574853[7]8650128 12 231287426[7]9325062 212 (20)C>
== Executing PA-CTR 2, V(1)=1, V(2)=1287426[7]9325059, repcount=6437134[6]9662530, factor=5/2
1148343[8]9147126 1479882[28]7713522 6437134[7]6625308 12 232 213218567[7]8312652 (20)C>
== Executing PPA-CTR 5 (once), V(1)=3218567[7]8312651
1148343[8]9147146 1479882[28]3966692 6437134[7]6625318 01 233218567[7]8312658 21 (20)C>
== Executing PA-CTR 2, V(1)=0, V(2)=3218567[7]8312655, repcount=1609283[7]4156328, factor=5/2
2918555[8]4866754 9249264[28]5214676 1609283[8]1563286 01 232 218046418[7]0781641 (20)C>
2918555[8]4866755 9249264[28]5214687 1609283[8]1563283 01 232 218046418[7]0781641 <C(32) 32
2918555[8]4866756 9249264[28]6777969 1 01 232 <C(32) 328046418[7]0781642
2918555[8]4866757 9249264[28]6777974 4 01 23 22 (12)B> 328046418[7]0781642
2918555[8]4866758 9249264[28]9904542 1609283[8]1563288 01 23 22 128046418[7]0781642 (12)B>
2918555[8]4866759 9249264[28]9904548 1609283[8]1563290 01 23 22 128046418[7]0781643 (12)C>
2918555[8]4866760 9249264[28]9904553 1609283[8]1563287 01 23 22 128046418[7]0781643 <A(23) 20
2918555[8]4866761 9249264[28]1467839 1 01 23 22 <A(23) 238046418[7]0781643 20
2918555[8]4866762 9249264[28]1467841 -1 01 23 <A(33) 238046418[7]0781644 20
2918555[8]4866763 9249264[28]1467844 2 01 21 (23)C> 238046418[7]0781644 20
2918555[8]4866764 9249264[28]4594420 1609283[8]1563290 01 218046418[7]0781645 (23)C> 20
2918555[8]4866765 9249264[28]4594424 1609283[8]1563292 01 218046418[7]0781646 (20)C>
2918555[8]4866766 9249264[28]4594435 1609283[8]1563289 01 218046418[7]0781646 <C(32) 32
2918555[8]4866767 9249264[28]6157727 -3 01 <C(32) 328046418[7]0781647
2918555[8]4866768 9249264[28]6157732 0 12 (22)C> 328046418[7]0781647
2918555[8]4866769 9249264[28]7721026 1609283[8]1563294 12 228046418[7]0781647 (22)C>
2918555[8]4866770 9249264[28]7721031 1609283[8]1563291 12 228046418[7]0781647 <A(33) 20
2918555[8]4866771 9249264[28]9284325 -3 12 <A(33) 338046418[7]0781647 20
2918555[8]4866772 9249264[28]9284327 -5 <A(23) 338046418[7]0781648 20
2918555[8]4866773 9249264[28]9284330 -2 01 (22)B> 338046418[7]0781648 20
2918555[8]4866774 9249264[28]9284332 0 01 22 (32)B> 338046418[7]0781647 20
2918555[8]4866775 9249264[28]0847626 1609283[8]1563294 01 22 328046418[7]0781647 (32)B> 20
2918555[8]4866776 9249264[28]0847638 1609283[8]1563296 01 22 328046418[7]0781647 12 (12)B>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 232 211+V(1) (20)C>
1 11 -3 01 232 211+V(1) <C(32) 32
2 13+2*V(1) -5+-2*V(1) 01 232 <C(32) 322+V(1)
3 18+2*V(1) -2+-2*V(1) 01 23 22 (12)B> 322+V(1)
4 26+6*V(1) 2 01 23 22 122+V(1) (12)B>
5 32+6*V(1) 4 01 23 22 123+V(1) (12)C>
6 37+6*V(1) 1 01 23 22 123+V(1) <A(23) 20
7 43+8*V(1) -5+-2*V(1) 01 23 22 <A(23) 233+V(1) 20
8 45+8*V(1) -7+-2*V(1) 01 23 <A(33) 234+V(1) 20
9 48+8*V(1) -4+-2*V(1) 01 21 (23)C> 234+V(1) 20
10 64+12*V(1) 4 01 215+V(1) (23)C> 20
11 68+12*V(1) 6 01 216+V(1) (20)C>
12 79+12*V(1) 3 01 216+V(1) <C(32) 32
13 91+14*V(1) -9+-2*V(1) 01 <C(32) 327+V(1)
14 96+14*V(1) -6+-2*V(1) 12 (22)C> 327+V(1)
15 110+16*V(1) 8 12 227+V(1) (22)C>
16 115+16*V(1) 5 12 227+V(1) <A(33) 20
17 129+18*V(1) -9+-2*V(1) 12 <A(33) 337+V(1) 20
18 131+18*V(1) -11+-2*V(1) <A(23) 338+V(1) 20
19 134+18*V(1) -8+-2*V(1) 01 (22)B> 338+V(1) 20
20 136+18*V(1) -6+-2*V(1) 01 22 (32)B> 337+V(1) 20
21 150+20*V(1) 8 01 22 327+V(1) (32)B> 20
22 162+20*V(1) 10 01 22 327+V(1) 12 (12)B>
<< Success! ==> defined new CTR 26 (PPA)
2918555[8]4866776 9249264[28]0847638 1609283[8]1563296 01 22 328046418[7]0781647 12 (12)B>
== Executing PA-CTR 6, V(1)=0, V(2)=8046418[7]0781644, repcount=4023209[7]0390823, factor=5/2
6941764[8]8775006 5780790[29]8908658 4023209[8]3908234 01 22 32 122011604[8]1954116 (12)B>
6941764[8]8775007 5780790[29]8908664 4023209[8]3908236 01 22 32 122011604[8]1954117 (12)C>
6941764[8]8775008 5780790[29]8908669 4023209[8]3908233 01 22 32 122011604[8]1954117 <A(23) 20
6941764[8]8775009 5780790[29]2816903 -1 01 22 32 <A(23) 232011604[8]1954117 20
6941764[8]8775010 5780790[29]2816910 2 01 22 21 (23)C> 232011604[8]1954117 20
6941764[8]8775011 5780790[29]0633378 4023209[8]3908236 01 22 212011604[8]1954118 (23)C> 20
6941764[8]8775012 5780790[29]0633382 4023209[8]3908238 01 22 212011604[8]1954119 (20)C>
6941764[8]8775013 5780790[29]0633393 4023209[8]3908235 01 22 212011604[8]1954119 <C(32) 32
6941764[8]8775014 5780790[29]4541631 -3 01 22 <C(32) 322011604[8]1954120
6941764[8]8775015 5780790[29]4541633 -5 01 <C(33) 322011604[8]1954121
6941764[8]8775016 5780790[29]4541638 -2 12 (23)C> 322011604[8]1954121
6941764[8]8775017 5780790[29]4541640 0 12 23 (22)C> 322011604[8]1954120
6941764[8]8775018 5780790[29]8449880 4023209[8]3908240 12 23 222011604[8]1954120 (22)C>
6941764[8]8775019 5780790[29]8449885 4023209[8]3908237 12 23 222011604[8]1954120 <A(33) 20
6941764[8]8775020 5780790[29]2358125 -3 12 23 <A(33) 332011604[8]1954120 20
6941764[8]8775021 5780790[29]2358128 0 12 21 (23)C> 332011604[8]1954120 20
6941764[8]8775022 5780790[29]6266368 4023209[8]3908240 12 21 232011604[8]1954120 (23)C> 20
6941764[8]8775023 5780790[29]6266372 4023209[8]3908242 12 21 232011604[8]1954120 21 (20)C>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 22 32 121+V(1) (12)B>
1 6 2 01 22 32 122+V(1) (12)C>
2 11 -1 01 22 32 122+V(1) <A(23) 20
3 15+2*V(1) -5+-2*V(1) 01 22 32 <A(23) 232+V(1) 20
4 22+2*V(1) -2+-2*V(1) 01 22 21 (23)C> 232+V(1) 20
5 30+6*V(1) 2 01 22 213+V(1) (23)C> 20
6 34+6*V(1) 4 01 22 214+V(1) (20)C>
7 45+6*V(1) 1 01 22 214+V(1) <C(32) 32
8 53+8*V(1) -7+-2*V(1) 01 22 <C(32) 325+V(1)
9 55+8*V(1) -9+-2*V(1) 01 <C(33) 326+V(1)
10 60+8*V(1) -6+-2*V(1) 12 (23)C> 326+V(1)
11 62+8*V(1) -4+-2*V(1) 12 23 (22)C> 325+V(1)
12 72+10*V(1) 6 12 23 225+V(1) (22)C>
13 77+10*V(1) 3 12 23 225+V(1) <A(33) 20
14 87+12*V(1) -7+-2*V(1) 12 23 <A(33) 335+V(1) 20
15 90+12*V(1) -4+-2*V(1) 12 21 (23)C> 335+V(1) 20
16 100+14*V(1) 6 12 21 235+V(1) (23)C> 20
17 104+14*V(1) 8 12 21 235+V(1) 21 (20)C>
<< Success! ==> defined new CTR 27 (PPA)
6941764[8]8775023 5780790[29]6266372 4023209[8]3908242 12 21 232011604[8]1954120 21 (20)C>
== Executing PA-CTR 7, V(1)=0, V(2)=2011604[8]1954117, repcount=1005802[8]0977059, factor=5/2
1800558[9]9522672 3612993[30]2079044 1005802[9]9770596 12 21 232 215029011[8]4885296 (20)C>
1800558[9]9522673 3612993[30]2079055 1005802[9]9770593 12 21 232 215029011[8]4885296 <C(32) 32
1800558[9]9522674 3612993[30]1849647 1 12 21 232 <C(32) 325029011[8]4885297
1800558[9]9522675 3612993[30]1849652 4 12 21 23 22 (12)B> 325029011[8]4885297
1800558[9]9522676 3612993[30]1390840 1005802[9]9770598 12 21 23 22 125029011[8]4885297 (12)B>
1800558[9]9522677 3612993[30]1390846 1005802[9]9770600 12 21 23 22 125029011[8]4885298 (12)C>
1800558[9]9522678 3612993[30]1390851 1005802[9]9770597 12 21 23 22 125029011[8]4885298 <A(23) 20
1800558[9]9522679 3612993[30]1161447 1 12 21 23 22 <A(23) 235029011[8]4885298 20
1800558[9]9522680 3612993[30]1161449 -1 12 21 23 <A(33) 235029011[8]4885299 20
1800558[9]9522681 3612993[30]1161452 2 12 212 (23)C> 235029011[8]4885299 20
1800558[9]9522682 3612993[30]0702648 1005802[9]9770600 12 215029011[8]4885301 (23)C> 20
1800558[9]9522683 3612993[30]0702652 1005802[9]9770602 12 215029011[8]4885302 (20)C>
1800558[9]9522684 3612993[30]0702663 1005802[9]9770599 12 215029011[8]4885302 <C(32) 32
1800558[9]9522685 3612993[30]0473267 -5 12 <C(32) 325029011[8]4885303
1800558[9]9522686 3612993[30]0473272 -2 03 (22)C> 325029011[8]4885303
1800558[9]9522687 3612993[30]0243878 1005802[9]9770604 03 225029011[8]4885303 (22)C>
1800558[9]9522688 3612993[30]0243883 1005802[9]9770601 03 225029011[8]4885303 <A(33) 20
1800558[9]9522689 3612993[30]0014489 -5 03 <A(33) 335029011[8]4885303 20
1800558[9]9522690 3612993[30]0014492 -2 01 (23)C> 335029011[8]4885303 20
1800558[9]9522691 3612993[30]9785098 1005802[9]9770604 01 235029011[8]4885303 (23)C> 20
1800558[9]9522692 3612993[30]9785102 1005802[9]9770606 01 235029011[8]4885303 21 (20)C>
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 12 211+V(2) 232 211+V(1) (20)C>
1 11 -3 12 211+V(2) 232 211+V(1) <C(32) 32
2 13+2*V(1) -5+-2*V(1) 12 211+V(2) 232 <C(32) 322+V(1)
3 18+2*V(1) -2+-2*V(1) 12 211+V(2) 23 22 (12)B> 322+V(1)
4 26+6*V(1) 2 12 211+V(2) 23 22 122+V(1) (12)B>
5 32+6*V(1) 4 12 211+V(2) 23 22 123+V(1) (12)C>
6 37+6*V(1) 1 12 211+V(2) 23 22 123+V(1) <A(23) 20
7 43+8*V(1) -5+-2*V(1) 12 211+V(2) 23 22 <A(23) 233+V(1) 20
8 45+8*V(1) -7+-2*V(1) 12 211+V(2) 23 <A(33) 234+V(1) 20
9 48+8*V(1) -4+-2*V(1) 12 212+V(2) (23)C> 234+V(1) 20
10 64+12*V(1) 4 12 216+V(1)+V(2) (23)C> 20
11 68+12*V(1) 6 12 217+V(1)+V(2) (20)C>
12 79+12*V(1) 3 12 217+V(1)+V(2) <C(32) 32
13 93+14*V(1)+2*V(2) -11+-2*V(1)+-2*V(2) 12 <C(32) 328+V(1)+V(2)
14 98+14*V(1)+2*V(2) -8+-2*V(1)+-2*V(2) 03 (22)C> 328+V(1)+V(2)
15 114+16*V(1)+4*V(2) 8 03 228+V(1)+V(2) (22)C>
16 119+16*V(1)+4*V(2) 5 03 228+V(1)+V(2) <A(33) 20
17 135+18*V(1)+6*V(2) -11+-2*V(1)+-2*V(2) 03 <A(33) 338+V(1)+V(2) 20
18 138+18*V(1)+6*V(2) -8+-2*V(1)+-2*V(2) 01 (23)C> 338+V(1)+V(2) 20
19 154+20*V(1)+8*V(2) 8 01 238+V(1)+V(2) (23)C> 20
20 158+20*V(1)+8*V(2) 10 01 238+V(1)+V(2) 21 (20)C>
<< Success! ==> defined new CTR 28 (PPA)
1800558[9]9522692 3612993[30]9785102 1005802[9]9770606 01 235029011[8]4885303 21 (20)C>
== Executing PA-CTR 2, V(1)=0, V(2)=5029011[8]4885300, repcount=2514505[8]2442651, factor=5/2
4566515[9]6391853 2258121[31]9839870 2514505[9]4426512 01 23 211257252[9]2213256 (20)C>
== Executing PPA-CTR 3 (once), V(1)=1257252[9]2213255
4566515[9]6391870 2258121[31]0825530 2514505[9]4426520 12 321257252[9]2213259 12 (12)C>
== Executing PA-CTR 1, V(1)=0, V(2)=1257252[9]2213256, repcount=6286264[8]6106629, factor=5/2
1085277[10]7458160 1411325[32]5186662 6286264[9]1066294 12 32 123143132[9]0533146 (12)C>
== Executing PPA-CTR 24 (once), V(1)=3143132[9]0533145
1085277[10]7458174 1411325[32]2650772 6286264[9]1066300 01 233143132[9]0533149 21 (20)C>
== Executing PA-CTR 2, V(1)=0, V(2)=3143132[9]0533146, repcount=1571566[9]5266574, factor=5/2
2814000[10]5390488 8820785[32]3704864 1571566[10]2665744 01 23 217857830[9]6332871 (20)C>
== Executing PPA-CTR 3 (once), V(1)=7857830[9]6332870
2814000[10]5390505 8820785[32]2365134 1571566[10]2665752 12 327857830[9]6332874 12 (12)C>
== Executing PA-CTR 1, V(1)=0, V(2)=7857830[9]6332871, repcount=3928915[9]3166436, factor=5/2
6742915[10]7054865 5512991[33]0952582 3928915[10]1664368 12 322 121964457[10]5832181 (12)C>
== Executing PPA-CTR 4 (once), V(1)=1964457[10]5832180, V(2)=0
6742915[10]7054887 5512991[33]7596340 3928915[10]1664378 12 231964457[10]5832187 212 (20)C>
== Executing PA-CTR 2, V(1)=1, V(2)=1964457[10]5832184, repcount=9822288[9]7916093, factor=5/2
1754743[11]4131910 3445619[34]4940460 9822288[10]9160936 12 23 214911144[10]9580467 (20)C>
== Executing PPA-CTR 25 (once), V(1)=4911144[10]9580466
1754743[11]4131929 3445619[34]9067078 9822288[10]9160944 01 22 12 324911144[10]9580470 12 (12)C>
== Executing PA-CTR 8, V(1)=0, V(2)=4911144[10]9580467, repcount=2455572[10]9790234, factor=5/2
4210315[11]2034269 2153512[35]4338650 2455572[11]7902348 01 22 12 322 121227786[11]8951171 (12)C>
== Executing PPA-CTR 23 (once), V(1)=1227786[11]8951170, V(2)=0
4210315[11]2034291 2153512[35]3362208 2455572[11]7902358 12 321227786[11]8951178 12 (12)C>
== Executing PA-CTR 1, V(1)=0, V(2)=1227786[11]8951175, repcount=6138930[10]4475588, factor=5/2
1034924[12]6790171 1345945[36]1806872 6138930[11]4755886 12 322 123069465[11]2377941 (12)C>
== Executing PPA-CTR 4 (once), V(1)=3069465[11]2377940, V(2)=0
1034924[12]6790193 1345945[36]9365830 6138930[11]4755896 12 233069465[11]2377947 212 (20)C>
== Executing PA-CTR 2, V(1)=1, V(2)=3069465[11]2377944, repcount=1534732[11]1188973, factor=5/2
2723130[12]9868896 8412156[36]2656350 1534732[12]1889734 12 23 217673662[11]5944867 (20)C>
== Executing PPA-CTR 25 (once), V(1)=7673662[11]5944866
2723130[12]9868915 8412156[36]5884568 1534732[12]1889742 01 22 12 327673662[11]5944870 12 (12)C>
== Executing PA-CTR 8, V(1)=0, V(2)=7673662[11]5944867, repcount=3836831[11]7972434, factor=5/2
6559961[12]9593255 5257598[37]5367740 3836831[12]9724346 01 22 12 322 121918415[12]9862171 (12)C>
== Executing PPA-CTR 23 (once), V(1)=1918415[12]9862170, V(2)=0
6559961[12]9593277 5257598[37]2611298 3836831[12]9724356 12 321918415[12]9862178 12 (12)C>
== Executing PA-CTR 1, V(1)=0, V(2)=1918415[12]9862175, repcount=9592078[11]9931088, factor=5/2
1615203[13]8904157 3285998[38]5904962 9592078[12]9310884 12 322 124796039[12]9655441 (12)C>
== Executing PPA-CTR 4 (once), V(1)=4796039[12]9655440, V(2)=0
1615203[13]8904179 3285998[38]9013920 9592078[12]9310894 12 234796039[12]9655447 212 (20)C>
== Executing PA-CTR 2, V(1)=1, V(2)=4796039[12]9655444, repcount=2398019[12]4827723, factor=5/2
4253025[13]2009132 2053749[39]1341940 2398019[13]8277232 12 23 211199009[13]4138617 (20)C>
== Executing PPA-CTR 25 (once), V(1)=1199009[13]4138616
4253025[13]2009151 2053749[39]9282658 2398019[13]8277240 01 22 12 321199009[13]4138620 12 (12)C>
== Executing PA-CTR 8, V(1)=0, V(2)=1199009[13]4138617, repcount=5995048[12]2069309, factor=5/2
1024807[14]2702241 1283593[40]0040830 5995048[13]0693094 01 22 12 322 122997524[13]0346546 (12)C>
== Executing PPA-CTR 23 (once), V(1)=2997524[13]0346545, V(2)=0
1024807[14]2702263 1283593[40]6971888 5995048[13]0693104 12 322997524[13]0346553 12 (12)C>
== Executing PA-CTR 1, V(1)=0, V(2)=2997524[13]0346550, repcount=1498762[13]0173276, factor=5/2
2523569[14]4435023 8022457[40]0721656 1498762[14]1732760 12 32 127493811[13]0866381 (12)C>
== Executing PPA-CTR 24 (once), V(1)=7493811[13]0866380
2523569[14]4435037 8022457[40]2851056 1498762[14]1732766 01 237493811[13]0866384 21 (20)C>
== Executing PA-CTR 2, V(1)=0, V(2)=7493811[13]0866381, repcount=3746905[13]0433191, factor=5/2
6645165[14]9200138 5014036[41]2586744 3746905[14]4331912 01 232 211873452[14]2165956 (20)C>
== Executing PPA-CTR 26 (once), V(1)=1873452[14]2165955
6645165[14]9200160 5014036[41]5906006 3746905[14]4331922 01 22 321873452[14]2165962 12 (12)B>
== Executing PA-CTR 6, V(1)=0, V(2)=1873452[14]2165959, repcount=9367263[13]6082980, factor=5/2
1601242[15]0029960 3133772[42]0467006 9367263[14]0829802 01 22 322 124683631[14]0414901 (12)B>
1601242[15]0029961 3133772[42]0467012 9367263[14]0829804 01 22 322 124683631[14]0414902 (12)C>
1601242[15]0029962 3133772[42]0467017 9367263[14]0829801 01 22 322 124683631[14]0414902 <A(23) 20
1601242[15]0029963 3133772[42]1296821 -3 01 22 322 <A(23) 234683631[14]0414902 20
1601242[15]0029964 3133772[42]1296828 0 01 22 32 21 (23)C> 234683631[14]0414902 20
1601242[15]0029965 3133772[42]2956436 9367263[14]0829804 01 22 32 214683631[14]0414903 (23)C> 20
1601242[15]0029966 3133772[42]2956440 9367263[14]0829806 01 22 32 214683631[14]0414904 (20)C>
1601242[15]0029967 3133772[42]2956451 9367263[14]0829803 01 22 32 214683631[14]0414904 <C(32) 32
1601242[15]0029968 3133772[42]3786259 -5 01 22 32 <C(32) 324683631[14]0414905
1601242[15]0029969 3133772[42]3786266 -2 01 22 12 (12)B> 324683631[14]0414905
1601242[15]0029970 3133772[42]5445886 9367263[14]0829808 01 22 124683631[14]0414906 (12)B>
1601242[15]0029971 3133772[42]5445892 9367263[14]0829810 01 22 124683631[14]0414907 (12)C>
1601242[15]0029972 3133772[42]5445897 9367263[14]0829807 01 22 124683631[14]0414907 <A(23) 20
1601242[15]0029973 3133772[42]6275711 -7 01 22 <A(23) 234683631[14]0414907 20
1601242[15]0029974 3133772[42]6275713 -9 01 <A(33) 234683631[14]0414908 20
1601242[15]0029975 3133772[42]6275716 -6 (32)B> 234683631[14]0414908 20
1601242[15]0029976 3133772[42]6275718 -4 32 (22)B> 234683631[14]0414907 20
1601242[15]0029977 3133772[42]7105532 9367263[14]0829810 32 224683631[14]0414907 (22)B> 20
1601242[15]0029978 3133772[42]7105539 9367263[14]0829807 32 224683631[14]0414907 <C(33) 32
1601242[15]0029979 3133772[42]7935353 -7 32 <C(33) 334683631[14]0414907 32
1601242[15]0029980 3133772[42]7935358 -4 12 (32)B> 334683631[14]0414907 32
1601242[15]0029981 3133772[42]8765172 9367263[14]0829810 12 324683631[14]0414907 (32)B> 32
1601242[15]0029982 3133772[42]8765176 9367263[14]0829812 12 324683631[14]0414908 (12)B>
1601242[15]0029983 3133772[42]8765182 9367263[14]0829814 12 324683631[14]0414908 12 (12)C>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 22 322 121+V(1) (12)B>
1 6 2 01 22 322 122+V(1) (12)C>
2 11 -1 01 22 322 122+V(1) <A(23) 20
3 15+2*V(1) -5+-2*V(1) 01 22 322 <A(23) 232+V(1) 20
4 22+2*V(1) -2+-2*V(1) 01 22 32 21 (23)C> 232+V(1) 20
5 30+6*V(1) 2 01 22 32 213+V(1) (23)C> 20
6 34+6*V(1) 4 01 22 32 214+V(1) (20)C>
7 45+6*V(1) 1 01 22 32 214+V(1) <C(32) 32
8 53+8*V(1) -7+-2*V(1) 01 22 32 <C(32) 325+V(1)
9 60+8*V(1) -4+-2*V(1) 01 22 12 (12)B> 325+V(1)
10 80+12*V(1) 6 01 22 126+V(1) (12)B>
11 86+12*V(1) 8 01 22 127+V(1) (12)C>
12 91+12*V(1) 5 01 22 127+V(1) <A(23) 20
13 105+14*V(1) -9+-2*V(1) 01 22 <A(23) 237+V(1) 20
14 107+14*V(1) -11+-2*V(1) 01 <A(33) 238+V(1) 20
15 110+14*V(1) -8+-2*V(1) (32)B> 238+V(1) 20
16 112+14*V(1) -6+-2*V(1) 32 (22)B> 237+V(1) 20
17 126+16*V(1) 8 32 227+V(1) (22)B> 20
18 133+16*V(1) 5 32 227+V(1) <C(33) 32
19 147+18*V(1) -9+-2*V(1) 32 <C(33) 337+V(1) 32
20 152+18*V(1) -6+-2*V(1) 12 (32)B> 337+V(1) 32
21 166+20*V(1) 8 12 327+V(1) (32)B> 32
22 170+20*V(1) 10 12 328+V(1) (12)B>
23 176+20*V(1) 12 12 328+V(1) 12 (12)C>
<< Success! ==> defined new CTR 29 (PPA)
1601242[15]0029983 3133772[42]8765182 9367263[14]0829814 12 324683631[14]0414908 12 (12)C>
== Executing PA-CTR 1, V(1)=0, V(2)=4683631[14]0414905, repcount=2341815[14]0207453, factor=5/2
3943058[15]2104513 1958607[43]9064666 2341815[15]2074532 12 322 121170907[15]1037266 (12)C>
== Executing PPA-CTR 4 (once), V(1)=1170907[15]1037265, V(2)=0
3943058[15]2104535 1958607[43]9810124 2341815[15]2074542 12 231170907[15]1037272 212 (20)C>
== Executing PA-CTR 2, V(1)=1, V(2)=1170907[15]1037269, repcount=5854539[14]5518635, factor=5/2
1038305[16]2809520 1224129[44]3638624 5854539[15]5186352 12 232 212927269[15]7593177 (20)C>
== Executing PPA-CTR 5 (once), V(1)=2927269[15]7593176
1038305[16]2809540 1224129[44]5502294 5854539[15]5186362 01 232927269[15]7593183 21 (20)C>
== Executing PA-CTR 2, V(1)=0, V(2)=2927269[15]7593180, repcount=1463634[15]3796591, factor=5/2
2648303[16]4572041 7650812[44]6411182 1463634[16]7965908 01 23 217318174[15]8982956 (20)C>
== Executing PPA-CTR 3 (once), V(1)=7318174[15]8982955
2648303[16]4572058 7650812[44]2172642 1463634[16]7965916 12 327318174[15]8982959 12 (12)C>
== Executing PA-CTR 1, V(1)=0, V(2)=7318174[15]8982956, repcount=3659087[15]9491479, factor=5/2
6307391[16]9486848 4781757[45]1072074 3659087[16]4914790 12 32 121829543[16]7457396 (12)C>
== Executing PPA-CTR 24 (once), V(1)=1829543[16]7457395
6307391[16]9486862 4781757[45]5475684 3659087[16]4914796 01 231829543[16]7457399 21 (20)C>
== Executing PA-CTR 2, V(1)=0, V(2)=1829543[16]7457396, repcount=9147718[15]3728699, factor=5/2
1636988[17]0502551 2988598[46]4144276 9147718[16]7286990 01 23 214573859[16]8643496 (20)C>
== Executing PPA-CTR 3 (once), V(1)=4573859[16]8643495
1636988[17]0502568 2988598[46]5153296 9147718[16]7286998 12 324573859[16]8643499 12 (12)C>
== Executing PA-CTR 1, V(1)=0, V(2)=4573859[16]8643496, repcount=2286929[16]9321749, factor=5/2
3923917[17]3720058 1867874[47]1949788 2286929[17]3217492 12 32 121143464[17]6608746 (12)C>
== Executing PPA-CTR 24 (once), V(1)=1143464[17]6608745
3923917[17]3720072 1867874[47]4472298 2286929[17]3217498 01 231143464[17]6608749 21 (20)C>
== Executing PA-CTR 2, V(1)=0, V(2)=1143464[17]6608746, repcount=5717324[16]3304374, factor=5/2
1021297[18]0068186 1167421[48]5994790 5717324[17]3043742 01 23 212858662[17]6521871 (20)C>
== Executing PPA-CTR 3 (once), V(1)=2858662[17]6521870
1021297[18]0068203 1167421[48]7301060 5717324[17]3043750 12 322858662[17]6521874 12 (12)C>
== Executing PA-CTR 1, V(1)=0, V(2)=2858662[17]6521871, repcount=1429331[17]8260936, factor=5/2
2450628[18]2677563 7296382[48]9099508 1429331[18]2609366 12 322 127146655[17]1304681 (12)C>
== Executing PPA-CTR 4 (once), V(1)=7146655[17]1304680, V(2)=0
2450628[18]2677585 7296382[48]5193266 1429331[18]2609376 12 237146655[17]1304687 212 (20)C>
== Executing PA-CTR 2, V(1)=1, V(2)=7146655[17]1304684, repcount=3573327[17]5652343, factor=5/2
6381288[18]4853358 4560239[49]9499886 3573327[18]6523434 12 23 211786663[18]8261717 (20)C>
== Executing PPA-CTR 25 (once), V(1)=1786663[18]8261716
6381288[18]4853377 4560239[49]5164004 3573327[18]6523442 01 22 12 321786663[18]8261720 12 (12)C>
== Executing PA-CTR 8, V(1)=0, V(2)=1786663[18]8261717, repcount=8933319[17]4130859, factor=5/2
1531460[19]6161967 2850149[50]4473076 8933319[18]1308596 01 22 12 322 124466659[18]0654296 (12)C>
== Executing PPA-CTR 23 (once), V(1)=4466659[18]0654295, V(2)=0
1531460[19]6161989 2850149[50]7559134 8933319[18]1308606 12 324466659[18]0654303 12 (12)C>
== Executing PA-CTR 1, V(1)=0, V(2)=4466659[18]0654300, repcount=2233329[18]0327151, factor=5/2
3764790[19]9433499 1781343[51]3294902 2233329[19]3271512 12 32 121116664[19]1635756 (12)C>
== Executing PPA-CTR 24 (once), V(1)=1116664[19]1635755
3764790[19]9433513 1781343[51]6195552 2233329[19]3271518 01 231116664[19]1635759 21 (20)C>
== Executing PA-CTR 2, V(1)=0, V(2)=1116664[19]1635756, repcount=5583324[18]5817879, factor=5/2
9906447[19]3430182 1113339[52]9034184 5583324[19]8178792 01 23 212791662[19]9089396 (20)C>
== Executing PPA-CTR 3 (once), V(1)=2791662[19]9089395
9906447[19]3430199 1113339[52]6285804 5583324[19]8178800 12 322791662[19]9089399 12 (12)C>
== Executing PA-CTR 1, V(1)=0, V(2)=2791662[19]9089396, repcount=1395831[19]4544699, factor=5/2
2386475[20]8877189 6958373[52]9002396 1395831[20]5446994 12 32 126979155[19]2723496 (12)C>
== Executing PPA-CTR 24 (once), V(1)=6979155[19]2723495
2386475[20]8877203 6958373[52]7131406 1395831[20]5447000 01 236979155[19]2723499 21 (20)C>
== Executing PA-CTR 2, V(1)=0, V(2)=6979155[19]2723496, repcount=3489577[19]6361749, factor=5/2
6225011[20]8856442 4348983[53]9047898 3489577[20]3617494 01 23 211744788[20]1808746 (20)C>
== Executing PPA-CTR 3 (once), V(1)=1744788[20]1808745
6225011[20]8856459 4348983[53]4370418 3489577[20]3617502 12 321744788[20]1808749 12 (12)C>
== Executing PA-CTR 1, V(1)=0, V(2)=1744788[20]1808746, repcount=8723944[19]5904374, factor=5/2
1494895[21]7900199 2718114[54]8692910 8723944[20]9043746 12 32 124361972[20]9521871 (12)C>
== Executing PPA-CTR 24 (once), V(1)=4361972[20]9521870
1494895[21]7900213 2718114[54]1999170 8723944[20]9043752 01 234361972[20]9521874 21 (20)C>
== Executing PA-CTR 2, V(1)=0, V(2)=4361972[20]9521871, repcount=2180986[20]4760936, factor=5/2
3893980[21]0270509 1698821[55]0797618 2180986[21]7609368 01 232 211090493[21]3804681 (20)C>
== Executing PPA-CTR 26 (once), V(1)=1090493[21]3804680
3893980[21]0270531 1698821[55]6891380 2180986[21]7609378 01 22 321090493[21]3804687 12 (12)B>
== Executing PA-CTR 6, V(1)=0, V(2)=1090493[21]3804684, repcount=5452465[20]6902343, factor=5/2
9346445[21]9293961 1061763[56]8698000 5452465[21]9023436 01 22 32 122726232[21]4511716 (12)B>
== Executing PPA-CTR 27 (once), V(1)=2726232[21]4511715
9346445[21]9293978 1061763[56]1862114 5452465[21]9023444 12 21 232726232[21]4511720 21 (20)C>
Lines: 800
Top steps: 799
Macro steps: 93464454883949241345875290599293978
Basic steps: 1061763463773339838151580295658244343657301767565363808330615011862114
Tape index: 54524652209485495688631372869023444
nonzeros: 54524652209485495688631372869023447
log10(nonzeros): 34.737
log10(steps ): 69.026
Some long numbers above are shortened: #(omitted digits) shown in "[]".
Input to awk program:
gohalt 1
nbs 4
T 3-state 4-symbol #d (T.J. & S. Ligocki)
: >4.6x10^434 >7.6x10^868
5T 1RB 0RB 3LC 1RC 0RC 1RH 2RC 3RC 1LB 2LA 3LA 2RB
L 2
M 800
pref sim
machv Lig34_d just simple
machv Lig34_d-r with repetitions reduced
machv Lig34_d-1 with tape symbol exponents
machv Lig34_d-m as 2-bck-macro machine
machv Lig34_d-a as 2-bck-macro machine with pure additive config-TRs
iam Lig34_d-a
mtype 2 0
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:13:45 CEST 2010
edate Tue Jul 6 22:13:49 CEST 2010
bnspeed 1
short 7
Constructed by: $Id: tmJob.awk,v 1.34 2010/05/06 18:26:17 heiner Exp $
$Id: basics.awk,v 1.1 2010/05/06 17:24:17 heiner Exp $
$Id: htSupp.awk,v 1.14 2010/07/06 19:48:32 heiner Exp $
$Id: mmSim.awk,v 1.34 2005/01/09 22:23:28 heiner Exp $
$Id: bignum.awk,v 1.34 2010/05/06 17:58:14 heiner Exp $
$Id: varLI.awk,v 1.11 2005/01/15 21:01:29 heiner Exp $
bignum signature: LEN={S++:9 U++:9 S+:8 U+:8 S*:4 U*:4} DONT: y i o;
Start: Tue Jul 6 22:13:45 CEST 2010