Comment: This TM produces >1.9*10^19 ones in >7.0*10^37 steps.
| State | on 0 |
on 1 |
on 0 | on 1 | ||||
|---|---|---|---|---|---|---|---|---|
| Move | Goto | Move | Goto | |||||
| A | B1R | C0L | 1 | right | B | 0 | left | C |
| B | A1L | D1R | 1 | left | A | 1 | right | D |
| C | B0L | E0L | 0 | left | B | 0 | left | E |
| D | A1R | B0R | 1 | right | A | 0 | right | B |
| E | F1L | C1L | 1 | left | F | 1 | left | C |
| F | A0L | Z1R | 0 | left | A | 1 | right | Z |
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 5 -3 <A(10) 01
2 8 0 01 (11)A> 01
3 10 2 01 11 (11)D>
4 12 4 01 112 (11)B>
5 15 1 01 112 <E(00) 10
6 17 -1 01 11 <E(01) 00 10
7 19 -3 01 <E(01) 01 00 10
8 21 -5 <B(01) 012 00 10
9 29 -7 <E(01) 00 012 00 10
10 31 -9 <A(01) 01 00 012 00 10
11 35 -11 <B(00) 11 01 00 012 00 10
12 40 -8 11 (11)B> 11 01 00 012 00 10
13 42 -6 112 (10)B> 01 00 012 00 10
14 46 -4 113 (10)B> 00 012 00 10
15 50 -2 114 (11)A> 012 00 10
16 52 0 115 (11)D> 01 00 10
17 57 -3 115 <E(01) 002 10
18 67 -13 <E(01) 015 002 10
19 69 -15 <A(01) 016 002 10
20 73 -17 <B(00) 11 016 002 10
21 78 -14 11 (11)B> 11 016 002 10
22 80 -12 112 (10)B> 016 002 10
23 104 0 118 (10)B> 002 10
24 108 2 119 (11)A> 00 10
25 113 -1 119 <C(10) 01 10
26 131 -19 <C(10) 109 01 10
27 133 -21 <A(10) 1010 01 10
28 136 -18 01 (11)A> 1010 01 10
29 139 -21 01 <C(10) 00 109 01 10
30 141 -23 <F(10) 10 00 109 01 10
31 145 -25 <C(01) 102 00 109 01 10
32 147 -27 <A(10) 01 102 00 109 01 10
33 150 -24 01 (11)A> 01 102 00 109 01 10
34 152 -22 01 11 (11)D> 102 00 109 01 10
35 160 -18 01 113 (11)D> 00 109 01 10
36 162 -16 01 114 (11)B> 109 01 10
37 164 -14 01 115 (11)A> 108 01 10
38 167 -17 01 115 <C(10) 00 107 01 10
39 177 -27 01 <C(10) 105 00 107 01 10
40 179 -29 <F(10) 106 00 107 01 10
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <F(10) 101+V(2) 00 103+V(1) [*]* [*]*
1 4 -2 <C(01) 102+V(2) 00 103+V(1) [*]* [*]*
2 6 -4 <A(10) 01 102+V(2) 00 103+V(1) [*]* [*]*
3 9 -1 01 (11)A> 01 102+V(2) 00 103+V(1) [*]* [*]*
4 11 1 01 11 (11)D> 102+V(2) 00 103+V(1) [*]* [*]*
5 19+4*V(2) 5+2*V(2) 01 113+V(2) (11)D> 00 103+V(1) [*]* [*]*
6 21+4*V(2) 7+2*V(2) 01 114+V(2) (11)B> 103+V(1) [*]* [*]*
7 23+4*V(2) 9+2*V(2) 01 115+V(2) (11)A> 102+V(1) [*]* [*]*
8 26+4*V(2) 6+2*V(2) 01 115+V(2) <C(10) 00 101+V(1) [*]* [*]*
9 36+6*V(2) -4 01 <C(10) 105+V(2) 00 101+V(1) [*]* [*]*
10 38+6*V(2) -6 <F(10) 106+V(2) 00 101+V(1) [*]* [*]*
<< Success! ==> defined new CTR 1 (PA)
40 179 -29 <F(10) 106 00 107 01 10
== Executing PA-CTR 1, V(1)=4, V(2)=5, repcount=3, factor=5/2
70 473 -47 <F(10) 1021 00 10 01 10
71 477 -49 <C(01) 1022 00 10 01 10
72 479 -51 <A(10) 01 1022 00 10 01 10
73 482 -48 01 (11)A> 01 1022 00 10 01 10
74 484 -46 01 11 (11)D> 1022 00 10 01 10
75 572 -2 01 1123 (11)D> 00 10 01 10
76 574 0 01 1124 (11)B> 10 01 10
77 576 2 01 1125 (11)A> 01 10
78 578 4 01 1126 (11)D> 10
79 582 6 01 1127 (11)D>
80 584 8 01 1128 (11)B>
81 587 5 01 1128 <E(00) 10
82 589 3 01 1127 <E(01) 00 10
83 643 -51 01 <E(01) 0127 00 10
84 645 -53 <B(01) 0128 00 10
85 653 -55 <E(01) 00 0128 00 10
86 655 -57 <A(01) 01 00 0128 00 10
87 659 -59 <B(00) 11 01 00 0128 00 10
88 664 -56 11 (11)B> 11 01 00 0128 00 10
89 666 -54 112 (10)B> 01 00 0128 00 10
90 670 -52 113 (10)B> 00 0128 00 10
91 674 -50 114 (11)A> 0128 00 10
92 676 -48 115 (11)D> 0127 00 10
93 681 -51 115 <E(01) 00 0126 00 10
94 691 -61 <E(01) 015 00 0126 00 10
95 693 -63 <A(01) 016 00 0126 00 10
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <A(01) 011+V(2) 00 013+V(1) [*]* [*]*
1 4 -2 <B(00) 11 011+V(2) 00 013+V(1) [*]* [*]*
2 9 1 11 (11)B> 11 011+V(2) 00 013+V(1) [*]* [*]*
3 11 3 112 (10)B> 011+V(2) 00 013+V(1) [*]* [*]*
4 15+4*V(2) 5+2*V(2) 113+V(2) (10)B> 00 013+V(1) [*]* [*]*
5 19+4*V(2) 7+2*V(2) 114+V(2) (11)A> 013+V(1) [*]* [*]*
6 21+4*V(2) 9+2*V(2) 115+V(2) (11)D> 012+V(1) [*]* [*]*
7 26+4*V(2) 6+2*V(2) 115+V(2) <E(01) 00 011+V(1) [*]* [*]*
8 36+6*V(2) -4 <E(01) 015+V(2) 00 011+V(1) [*]* [*]*
9 38+6*V(2) -6 <A(01) 016+V(2) 00 011+V(1) [*]* [*]*
<< Success! ==> defined new CTR 2 (PA)
95 693 -63 <A(01) 016 00 0126 00 10
== Executing PA-CTR 2, V(1)=23, V(2)=5, repcount=12, factor=5/2
203 3489 -135 <A(01) 0166 00 012 00 10
204 3493 -137 <B(00) 11 0166 00 012 00 10
205 3498 -134 11 (11)B> 11 0166 00 012 00 10
206 3500 -132 112 (10)B> 0166 00 012 00 10
207 3764 0 1168 (10)B> 00 012 00 10
208 3768 2 1169 (11)A> 012 00 10
209 3770 4 1170 (11)D> 01 00 10
210 3775 1 1170 <E(01) 002 10
211 3915 -139 <E(01) 0170 002 10
212 3917 -141 <A(01) 0171 002 10
213 3921 -143 <B(00) 11 0171 002 10
214 3926 -140 11 (11)B> 11 0171 002 10
215 3928 -138 112 (10)B> 0171 002 10
216 4212 4 1173 (10)B> 002 10
217 4216 6 1174 (11)A> 00 10
218 4221 3 1174 <C(10) 01 10
219 4369 -145 <C(10) 1074 01 10
220 4371 -147 <A(10) 1075 01 10
221 4374 -144 01 (11)A> 1075 01 10
222 4377 -147 01 <C(10) 00 1074 01 10
223 4379 -149 <F(10) 10 00 1074 01 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <A(01) 011+V(1) 00 012 00 [*]*
1 4 -2 <B(00) 11 011+V(1) 00 012 00 [*]*
2 9 1 11 (11)B> 11 011+V(1) 00 012 00 [*]*
3 11 3 112 (10)B> 011+V(1) 00 012 00 [*]*
4 15+4*V(1) 5+2*V(1) 113+V(1) (10)B> 00 012 00 [*]*
5 19+4*V(1) 7+2*V(1) 114+V(1) (11)A> 012 00 [*]*
6 21+4*V(1) 9+2*V(1) 115+V(1) (11)D> 01 00 [*]*
7 26+4*V(1) 6+2*V(1) 115+V(1) <E(01) 002 [*]*
8 36+6*V(1) -4 <E(01) 015+V(1) 002 [*]*
9 38+6*V(1) -6 <A(01) 016+V(1) 002 [*]*
10 42+6*V(1) -8 <B(00) 11 016+V(1) 002 [*]*
11 47+6*V(1) -5 11 (11)B> 11 016+V(1) 002 [*]*
12 49+6*V(1) -3 112 (10)B> 016+V(1) 002 [*]*
13 73+10*V(1) 9+2*V(1) 118+V(1) (10)B> 002 [*]*
14 77+10*V(1) 11+2*V(1) 119+V(1) (11)A> 00 [*]*
15 82+10*V(1) 8+2*V(1) 119+V(1) <C(10) 01 [*]*
16 100+12*V(1) -10 <C(10) 109+V(1) 01 [*]*
17 102+12*V(1) -12 <A(10) 1010+V(1) 01 [*]*
18 105+12*V(1) -9 01 (11)A> 1010+V(1) 01 [*]*
19 108+12*V(1) -12 01 <C(10) 00 109+V(1) 01 [*]*
20 110+12*V(1) -14 <F(10) 10 00 109+V(1) 01 [*]*
<< Success! ==> defined new CTR 3 (PPA)
223 4379 -149 <F(10) 10 00 1074 01 10
== Executing PA-CTR 1, V(1)=71, V(2)=0, repcount=36, factor=5/2
583 24647 -365 <F(10) 10181 00 102 01 10
584 24651 -367 <C(01) 10182 00 102 01 10
585 24653 -369 <A(10) 01 10182 00 102 01 10
586 24656 -366 01 (11)A> 01 10182 00 102 01 10
587 24658 -364 01 11 (11)D> 10182 00 102 01 10
588 25386 0 01 11183 (11)D> 00 102 01 10
589 25388 2 01 11184 (11)B> 102 01 10
590 25390 4 01 11185 (11)A> 10 01 10
591 25393 1 01 11185 <C(10) 00 01 10
592 25763 -369 01 <C(10) 10185 00 01 10
593 25765 -371 <F(10) 10186 00 01 10
594 25769 -373 <C(01) 10187 00 01 10
595 25771 -375 <A(10) 01 10187 00 01 10
596 25774 -372 01 (11)A> 01 10187 00 01 10
597 25776 -370 01 11 (11)D> 10187 00 01 10
598 26524 4 01 11188 (11)D> 00 01 10
599 26526 6 01 11189 (11)B> 01 10
600 26529 3 01 11189 <E(00) 11 10
601 26531 1 01 11188 <E(01) 00 11 10
602 26907 -375 01 <E(01) 01188 00 11 10
603 26909 -377 <B(01) 01189 00 11 10
604 26917 -379 <E(01) 00 01189 00 11 10
605 26919 -381 <A(01) 01 00 01189 00 11 10
606 26923 -383 <B(00) 11 01 00 01189 00 11 10
607 26928 -380 11 (11)B> 11 01 00 01189 00 11 10
608 26930 -378 112 (10)B> 01 00 01189 00 11 10
609 26934 -376 113 (10)B> 00 01189 00 11 10
610 26938 -374 114 (11)A> 01189 00 11 10
611 26940 -372 115 (11)D> 01188 00 11 10
612 26945 -375 115 <E(01) 00 01187 00 11 10
613 26955 -385 <E(01) 015 00 01187 00 11 10
614 26957 -387 <A(01) 016 00 01187 00 11 10
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <A(01) 011+V(2) 00 013+V(1) [*]* [*]* [*]*
1 4 -2 <B(00) 11 011+V(2) 00 013+V(1) [*]* [*]* [*]*
2 9 1 11 (11)B> 11 011+V(2) 00 013+V(1) [*]* [*]* [*]*
3 11 3 112 (10)B> 011+V(2) 00 013+V(1) [*]* [*]* [*]*
4 15+4*V(2) 5+2*V(2) 113+V(2) (10)B> 00 013+V(1) [*]* [*]* [*]*
5 19+4*V(2) 7+2*V(2) 114+V(2) (11)A> 013+V(1) [*]* [*]* [*]*
6 21+4*V(2) 9+2*V(2) 115+V(2) (11)D> 012+V(1) [*]* [*]* [*]*
7 26+4*V(2) 6+2*V(2) 115+V(2) <E(01) 00 011+V(1) [*]* [*]* [*]*
8 36+6*V(2) -4 <E(01) 015+V(2) 00 011+V(1) [*]* [*]* [*]*
9 38+6*V(2) -6 <A(01) 016+V(2) 00 011+V(1) [*]* [*]* [*]*
<< Success! ==> defined new CTR 4 (PA)
614 26957 -387 <A(01) 016 00 01187 00 11 10
== Executing PA-CTR 4, V(1)=184, V(2)=5, repcount=93, factor=5/2
1451 161621 -945 <A(01) 01471 00 01 00 11 10
1452 161625 -947 <B(00) 11 01471 00 01 00 11 10
1453 161630 -944 11 (11)B> 11 01471 00 01 00 11 10
1454 161632 -942 112 (10)B> 01471 00 01 00 11 10
1455 163516 0 11473 (10)B> 00 01 00 11 10
1456 163520 2 11474 (11)A> 01 00 11 10
1457 163522 4 11475 (11)D> 00 11 10
1458 163524 6 11476 (11)B> 11 10
1459 163526 8 11477 (10)B> 10
1460 163528 10 11477 10 (11)A>
1461 163533 7 11477 10 <C(10) 01
1462 163539 5 11477 <C(10) 00 01
1463 164493 -949 <C(10) 10477 00 01
1464 164495 -951 <A(10) 10478 00 01
1465 164498 -948 01 (11)A> 10478 00 01
1466 164501 -951 01 <C(10) 00 10477 00 01
1467 164503 -953 <F(10) 10 00 10477 00 01
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <A(01) 011+V(1) 00 01 00 11 10
1 4 -2 <B(00) 11 011+V(1) 00 01 00 11 10
2 9 1 11 (11)B> 11 011+V(1) 00 01 00 11 10
3 11 3 112 (10)B> 011+V(1) 00 01 00 11 10
4 15+4*V(1) 5+2*V(1) 113+V(1) (10)B> 00 01 00 11 10
5 19+4*V(1) 7+2*V(1) 114+V(1) (11)A> 01 00 11 10
6 21+4*V(1) 9+2*V(1) 115+V(1) (11)D> 00 11 10
7 23+4*V(1) 11+2*V(1) 116+V(1) (11)B> 11 10
8 25+4*V(1) 13+2*V(1) 117+V(1) (10)B> 10
9 27+4*V(1) 15+2*V(1) 117+V(1) 10 (11)A>
10 32+4*V(1) 12+2*V(1) 117+V(1) 10 <C(10) 01
11 38+4*V(1) 10+2*V(1) 117+V(1) <C(10) 00 01
12 52+6*V(1) -4 <C(10) 107+V(1) 00 01
13 54+6*V(1) -6 <A(10) 108+V(1) 00 01
14 57+6*V(1) -3 01 (11)A> 108+V(1) 00 01
15 60+6*V(1) -6 01 <C(10) 00 107+V(1) 00 01
16 62+6*V(1) -8 <F(10) 10 00 107+V(1) 00 01
<< Success! ==> defined new CTR 5 (PPA)
1467 164503 -953 <F(10) 10 00 10477 00 01
== Executing PA-CTR 1, V(1)=474, V(2)=0, repcount=238, factor=5/2
3847 1019637 -2381 <F(10) 101191 00 10 00 01
3848 1019641 -2383 <C(01) 101192 00 10 00 01
3849 1019643 -2385 <A(10) 01 101192 00 10 00 01
3850 1019646 -2382 01 (11)A> 01 101192 00 10 00 01
3851 1019648 -2380 01 11 (11)D> 101192 00 10 00 01
3852 1024416 4 01 111193 (11)D> 00 10 00 01
3853 1024418 6 01 111194 (11)B> 10 00 01
3854 1024420 8 01 111195 (11)A> 00 01
3855 1024425 5 01 111195 <C(10) 012
3856 1026815 -2385 01 <C(10) 101195 012
3857 1026817 -2387 <F(10) 101196 012
3858 1026821 -2389 <C(01) 101197 012
3859 1026823 -2391 <A(10) 01 101197 012
3860 1026826 -2388 01 (11)A> 01 101197 012
3861 1026828 -2386 01 11 (11)D> 101197 012
3862 1031616 8 01 111198 (11)D> 012
3863 1031621 5 01 111198 <E(01) 00 01
3864 1034017 -2391 01 <E(01) 011198 00 01
3865 1034019 -2393 <B(01) 011199 00 01
3866 1034027 -2395 <E(01) 00 011199 00 01
3867 1034029 -2397 <A(01) 01 00 011199 00 01
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <F(10) 101+V(2) 00 10 00 011+V(1)
1 4 -2 <C(01) 102+V(2) 00 10 00 011+V(1)
2 6 -4 <A(10) 01 102+V(2) 00 10 00 011+V(1)
3 9 -1 01 (11)A> 01 102+V(2) 00 10 00 011+V(1)
4 11 1 01 11 (11)D> 102+V(2) 00 10 00 011+V(1)
5 19+4*V(2) 5+2*V(2) 01 113+V(2) (11)D> 00 10 00 011+V(1)
6 21+4*V(2) 7+2*V(2) 01 114+V(2) (11)B> 10 00 011+V(1)
7 23+4*V(2) 9+2*V(2) 01 115+V(2) (11)A> 00 011+V(1)
8 28+4*V(2) 6+2*V(2) 01 115+V(2) <C(10) 012+V(1)
9 38+6*V(2) -4 01 <C(10) 105+V(2) 012+V(1)
10 40+6*V(2) -6 <F(10) 106+V(2) 012+V(1)
11 44+6*V(2) -8 <C(01) 107+V(2) 012+V(1)
12 46+6*V(2) -10 <A(10) 01 107+V(2) 012+V(1)
13 49+6*V(2) -7 01 (11)A> 01 107+V(2) 012+V(1)
14 51+6*V(2) -5 01 11 (11)D> 107+V(2) 012+V(1)
15 79+10*V(2) 9+2*V(2) 01 118+V(2) (11)D> 012+V(1)
16 84+10*V(2) 6+2*V(2) 01 118+V(2) <E(01) 00 011+V(1)
17 100+12*V(2) -10 01 <E(01) 018+V(2) 00 011+V(1)
18 102+12*V(2) -12 <B(01) 019+V(2) 00 011+V(1)
19 110+12*V(2) -14 <E(01) 00 019+V(2) 00 011+V(1)
20 112+12*V(2) -16 <A(01) 01 00 019+V(2) 00 011+V(1)
<< Success! ==> defined new CTR 6 (PPA)
3867 1034029 -2397 <A(01) 01 00 011199 00 01
== Executing PA-CTR 2, V(1)=1196, V(2)=0, repcount=599, factor=5/2
9258 6429821 -5991 <A(01) 012996 00 01 00 01
9259 6429825 -5993 <B(00) 11 012996 00 01 00 01
9260 6429830 -5990 11 (11)B> 11 012996 00 01 00 01
9261 6429832 -5988 112 (10)B> 012996 00 01 00 01
9262 6441816 4 112998 (10)B> 00 01 00 01
9263 6441820 6 112999 (11)A> 01 00 01
9264 6441822 8 113000 (11)D> 00 01
9265 6441824 10 113001 (11)B> 01
9266 6441827 7 113001 <E(00) 11
9267 6441829 5 113000 <E(01) 00 11
9268 6447829 -5995 <E(01) 013000 00 11
9269 6447831 -5997 <A(01) 013001 00 11
9270 6447835 -5999 <B(00) 11 013001 00 11
9271 6447840 -5996 11 (11)B> 11 013001 00 11
9272 6447842 -5994 112 (10)B> 013001 00 11
9273 6459846 8 113003 (10)B> 00 11
9274 6459850 10 113004 (11)A> 11
9275 6459853 7 113004 <C(10) 01
9276 6465861 -6001 <C(10) 103004 01
9277 6465863 -6003 <A(10) 103005 01
9278 6465866 -6000 01 (11)A> 103005 01
9279 6465869 -6003 01 <C(10) 00 103004 01
9280 6465871 -6005 <F(10) 10 00 103004 01
9281 6465875 -6007 <C(01) 102 00 103004 01
9282 6465877 -6009 <A(10) 01 102 00 103004 01
9283 6465880 -6006 01 (11)A> 01 102 00 103004 01
9284 6465882 -6004 01 11 (11)D> 102 00 103004 01
9285 6465890 -6000 01 113 (11)D> 00 103004 01
9286 6465892 -5998 01 114 (11)B> 103004 01
9287 6465894 -5996 01 115 (11)A> 103003 01
9288 6465897 -5999 01 115 <C(10) 00 103002 01
9289 6465907 -6009 01 <C(10) 105 00 103002 01
9290 6465909 -6011 <F(10) 106 00 103002 01
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <F(10) 101+V(2) 00 103+V(1) [*]*
1 4 -2 <C(01) 102+V(2) 00 103+V(1) [*]*
2 6 -4 <A(10) 01 102+V(2) 00 103+V(1) [*]*
3 9 -1 01 (11)A> 01 102+V(2) 00 103+V(1) [*]*
4 11 1 01 11 (11)D> 102+V(2) 00 103+V(1) [*]*
5 19+4*V(2) 5+2*V(2) 01 113+V(2) (11)D> 00 103+V(1) [*]*
6 21+4*V(2) 7+2*V(2) 01 114+V(2) (11)B> 103+V(1) [*]*
7 23+4*V(2) 9+2*V(2) 01 115+V(2) (11)A> 102+V(1) [*]*
8 26+4*V(2) 6+2*V(2) 01 115+V(2) <C(10) 00 101+V(1) [*]*
9 36+6*V(2) -4 01 <C(10) 105+V(2) 00 101+V(1) [*]*
10 38+6*V(2) -6 <F(10) 106+V(2) 00 101+V(1) [*]*
<< Success! ==> defined new CTR 7 (PA)
9290 6465909 -6011 <F(10) 106 00 103002 01
== Executing PA-CTR 7, V(1)=2999, V(2)=5, repcount=1500, factor=5/2
24290 40295409 -15011 <F(10) 107506 00 102 01
24291 40295413 -15013 <C(01) 107507 00 102 01
24292 40295415 -15015 <A(10) 01 107507 00 102 01
24293 40295418 -15012 01 (11)A> 01 107507 00 102 01
24294 40295420 -15010 01 11 (11)D> 107507 00 102 01
24295 40325448 4 01 117508 (11)D> 00 102 01
24296 40325450 6 01 117509 (11)B> 102 01
24297 40325452 8 01 117510 (11)A> 10 01
24298 40325455 5 01 117510 <C(10) 00 01
24299 40340475 -15015 01 <C(10) 107510 00 01
24300 40340477 -15017 <F(10) 107511 00 01
24301 40340481 -15019 <C(01) 107512 00 01
24302 40340483 -15021 <A(10) 01 107512 00 01
24303 40340486 -15018 01 (11)A> 01 107512 00 01
24304 40340488 -15016 01 11 (11)D> 107512 00 01
24305 40370536 8 01 117513 (11)D> 00 01
24306 40370538 10 01 117514 (11)B> 01
24307 40370541 7 01 117514 <E(00) 11
24308 40370543 5 01 117513 <E(01) 00 11
24309 40385569 -15021 01 <E(01) 017513 00 11
24310 40385571 -15023 <B(01) 017514 00 11
24311 40385579 -15025 <E(01) 00 017514 00 11
24312 40385581 -15027 <A(01) 01 00 017514 00 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <F(10) 101+V(1) 00 102 01
1 4 -2 <C(01) 102+V(1) 00 102 01
2 6 -4 <A(10) 01 102+V(1) 00 102 01
3 9 -1 01 (11)A> 01 102+V(1) 00 102 01
4 11 1 01 11 (11)D> 102+V(1) 00 102 01
5 19+4*V(1) 5+2*V(1) 01 113+V(1) (11)D> 00 102 01
6 21+4*V(1) 7+2*V(1) 01 114+V(1) (11)B> 102 01
7 23+4*V(1) 9+2*V(1) 01 115+V(1) (11)A> 10 01
8 26+4*V(1) 6+2*V(1) 01 115+V(1) <C(10) 00 01
9 36+6*V(1) -4 01 <C(10) 105+V(1) 00 01
10 38+6*V(1) -6 <F(10) 106+V(1) 00 01
11 42+6*V(1) -8 <C(01) 107+V(1) 00 01
12 44+6*V(1) -10 <A(10) 01 107+V(1) 00 01
13 47+6*V(1) -7 01 (11)A> 01 107+V(1) 00 01
14 49+6*V(1) -5 01 11 (11)D> 107+V(1) 00 01
15 77+10*V(1) 9+2*V(1) 01 118+V(1) (11)D> 00 01
16 79+10*V(1) 11+2*V(1) 01 119+V(1) (11)B> 01
17 82+10*V(1) 8+2*V(1) 01 119+V(1) <E(00) 11
18 84+10*V(1) 6+2*V(1) 01 118+V(1) <E(01) 00 11
19 100+12*V(1) -10 01 <E(01) 018+V(1) 00 11
20 102+12*V(1) -12 <B(01) 019+V(1) 00 11
21 110+12*V(1) -14 <E(01) 00 019+V(1) 00 11
22 112+12*V(1) -16 <A(01) 01 00 019+V(1) 00 11
<< Success! ==> defined new CTR 8 (PPA)
24312 40385581 -15027 <A(01) 01 00 017514 00 11
== Executing PA-CTR 2, V(1)=7511, V(2)=0, repcount=3756, factor=5/2
58116 252085009 -37563 <A(01) 0118781 00 012 00 11
== Executing PPA-CTR 3 (once), V(1)=18780
58136 252310479 -37577 <F(10) 10 00 1018789 01 11
== Executing PA-CTR 1, V(1)=18786, V(2)=0, repcount=9394, factor=5/2
152076 1576235081 -93941 <F(10) 1046971 00 10 01 11
152077 1576235085 -93943 <C(01) 1046972 00 10 01 11
152078 1576235087 -93945 <A(10) 01 1046972 00 10 01 11
152079 1576235090 -93942 01 (11)A> 01 1046972 00 10 01 11
152080 1576235092 -93940 01 11 (11)D> 1046972 00 10 01 11
152081 1576422980 4 01 1146973 (11)D> 00 10 01 11
152082 1576422982 6 01 1146974 (11)B> 10 01 11
152083 1576422984 8 01 1146975 (11)A> 01 11
152084 1576422986 10 01 1146976 (11)D> 11
152085 1576422988 12 01 1146977 (01)D>
152086 1576422990 14 01 1146977 01 (11)B>
152087 1576422993 11 01 1146977 01 <E(00) 10
152088 1576422995 9 01 1146977 <B(01) 00 10
152089 1576423001 7 01 1146976 <E(01) 002 10
152090 1576516953 -93945 01 <E(01) 0146976 002 10
152091 1576516955 -93947 <B(01) 0146977 002 10
152092 1576516963 -93949 <E(01) 00 0146977 002 10
152093 1576516965 -93951 <A(01) 01 00 0146977 002 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <F(10) 101+V(1) 00 10 01 11
1 4 -2 <C(01) 102+V(1) 00 10 01 11
2 6 -4 <A(10) 01 102+V(1) 00 10 01 11
3 9 -1 01 (11)A> 01 102+V(1) 00 10 01 11
4 11 1 01 11 (11)D> 102+V(1) 00 10 01 11
5 19+4*V(1) 5+2*V(1) 01 113+V(1) (11)D> 00 10 01 11
6 21+4*V(1) 7+2*V(1) 01 114+V(1) (11)B> 10 01 11
7 23+4*V(1) 9+2*V(1) 01 115+V(1) (11)A> 01 11
8 25+4*V(1) 11+2*V(1) 01 116+V(1) (11)D> 11
9 27+4*V(1) 13+2*V(1) 01 117+V(1) (01)D>
10 29+4*V(1) 15+2*V(1) 01 117+V(1) 01 (11)B>
11 32+4*V(1) 12+2*V(1) 01 117+V(1) 01 <E(00) 10
12 34+4*V(1) 10+2*V(1) 01 117+V(1) <B(01) 00 10
13 40+4*V(1) 8+2*V(1) 01 116+V(1) <E(01) 002 10
14 52+6*V(1) -4 01 <E(01) 016+V(1) 002 10
15 54+6*V(1) -6 <B(01) 017+V(1) 002 10
16 62+6*V(1) -8 <E(01) 00 017+V(1) 002 10
17 64+6*V(1) -10 <A(01) 01 00 017+V(1) 002 10
<< Success! ==> defined new CTR 9 (PPA)
152093 1576516965 -93951 <A(01) 01 00 0146977 002 10
== Executing PA-CTR 2, V(1)=46974, V(2)=0, repcount=23488, factor=5/2
363485 9852349349 -234879 <A(01) 01117441 00 01 002 10
363486 9852349353 -234881 <B(00) 11 01117441 00 01 002 10
363487 9852349358 -234878 11 (11)B> 11 01117441 00 01 002 10
363488 9852349360 -234876 112 (10)B> 01117441 00 01 002 10
363489 9852819124 6 11117443 (10)B> 00 01 002 10
363490 9852819128 8 11117444 (11)A> 01 002 10
363491 9852819130 10 11117445 (11)D> 002 10
363492 9852819132 12 11117446 (11)B> 00 10
363493 9852819135 9 11117446 <E(00) 102
363494 9852819137 7 11117445 <E(01) 00 102
363495 9853054027 -234883 <E(01) 01117445 00 102
363496 9853054029 -234885 <A(01) 01117446 00 102
363497 9853054033 -234887 <B(00) 11 01117446 00 102
363498 9853054038 -234884 11 (11)B> 11 01117446 00 102
363499 9853054040 -234882 112 (10)B> 01117446 00 102
363500 9853523824 10 11117448 (10)B> 00 102
363501 9853523828 12 11117449 (11)A> 102
363502 9853523831 9 11117449 <C(10) 00 10
363503 9853758729 -234889 <C(10) 10117449 00 10
363504 9853758731 -234891 <A(10) 10117450 00 10
363505 9853758734 -234888 01 (11)A> 10117450 00 10
363506 9853758737 -234891 01 <C(10) 00 10117449 00 10
363507 9853758739 -234893 <F(10) 10 00 10117449 00 10
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <A(01) 011+V(2) 00 01 002 101+V(1)
1 4 -2 <B(00) 11 011+V(2) 00 01 002 101+V(1)
2 9 1 11 (11)B> 11 011+V(2) 00 01 002 101+V(1)
3 11 3 112 (10)B> 011+V(2) 00 01 002 101+V(1)
4 15+4*V(2) 5+2*V(2) 113+V(2) (10)B> 00 01 002 101+V(1)
5 19+4*V(2) 7+2*V(2) 114+V(2) (11)A> 01 002 101+V(1)
6 21+4*V(2) 9+2*V(2) 115+V(2) (11)D> 002 101+V(1)
7 23+4*V(2) 11+2*V(2) 116+V(2) (11)B> 00 101+V(1)
8 26+4*V(2) 8+2*V(2) 116+V(2) <E(00) 102+V(1)
9 28+4*V(2) 6+2*V(2) 115+V(2) <E(01) 00 102+V(1)
10 38+6*V(2) -4 <E(01) 015+V(2) 00 102+V(1)
11 40+6*V(2) -6 <A(01) 016+V(2) 00 102+V(1)
12 44+6*V(2) -8 <B(00) 11 016+V(2) 00 102+V(1)
13 49+6*V(2) -5 11 (11)B> 11 016+V(2) 00 102+V(1)
14 51+6*V(2) -3 112 (10)B> 016+V(2) 00 102+V(1)
15 75+10*V(2) 9+2*V(2) 118+V(2) (10)B> 00 102+V(1)
16 79+10*V(2) 11+2*V(2) 119+V(2) (11)A> 102+V(1)
17 82+10*V(2) 8+2*V(2) 119+V(2) <C(10) 00 101+V(1)
18 100+12*V(2) -10 <C(10) 109+V(2) 00 101+V(1)
19 102+12*V(2) -12 <A(10) 1010+V(2) 00 101+V(1)
20 105+12*V(2) -9 01 (11)A> 1010+V(2) 00 101+V(1)
21 108+12*V(2) -12 01 <C(10) 00 109+V(2) 00 101+V(1)
22 110+12*V(2) -14 <F(10) 10 00 109+V(2) 00 101+V(1)
<< Success! ==> defined new CTR 10 (PPA)
363507 9853758739 -234893 <F(10) 10 00 10117449 00 10
== Executing PA-CTR 1, V(1)=117446, V(2)=0, repcount=58724, factor=5/2
950747 61582732031 -587237 <F(10) 10293621 00 10 00 10
950748 61582732035 -587239 <C(01) 10293622 00 10 00 10
950749 61582732037 -587241 <A(10) 01 10293622 00 10 00 10
950750 61582732040 -587238 01 (11)A> 01 10293622 00 10 00 10
950751 61582732042 -587236 01 11 (11)D> 10293622 00 10 00 10
950752 61583906530 8 01 11293623 (11)D> 00 10 00 10
950753 61583906532 10 01 11293624 (11)B> 10 00 10
950754 61583906534 12 01 11293625 (11)A> 00 10
950755 61583906539 9 01 11293625 <C(10) 01 10
950756 61584493789 -587241 01 <C(10) 10293625 01 10
950757 61584493791 -587243 <F(10) 10293626 01 10
950758 61584493795 -587245 <C(01) 10293627 01 10
950759 61584493797 -587247 <A(10) 01 10293627 01 10
950760 61584493800 -587244 01 (11)A> 01 10293627 01 10
950761 61584493802 -587242 01 11 (11)D> 10293627 01 10
950762 61585668310 12 01 11293628 (11)D> 01 10
950763 61585668315 9 01 11293628 <E(01) 00 10
950764 61586255571 -587247 01 <E(01) 01293628 00 10
950765 61586255573 -587249 <B(01) 01293629 00 10
950766 61586255581 -587251 <E(01) 00 01293629 00 10
950767 61586255583 -587253 <A(01) 01 00 01293629 00 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <F(10) 101+V(1) 00 10 00 [*]*
1 4 -2 <C(01) 102+V(1) 00 10 00 [*]*
2 6 -4 <A(10) 01 102+V(1) 00 10 00 [*]*
3 9 -1 01 (11)A> 01 102+V(1) 00 10 00 [*]*
4 11 1 01 11 (11)D> 102+V(1) 00 10 00 [*]*
5 19+4*V(1) 5+2*V(1) 01 113+V(1) (11)D> 00 10 00 [*]*
6 21+4*V(1) 7+2*V(1) 01 114+V(1) (11)B> 10 00 [*]*
7 23+4*V(1) 9+2*V(1) 01 115+V(1) (11)A> 00 [*]*
8 28+4*V(1) 6+2*V(1) 01 115+V(1) <C(10) 01 [*]*
9 38+6*V(1) -4 01 <C(10) 105+V(1) 01 [*]*
10 40+6*V(1) -6 <F(10) 106+V(1) 01 [*]*
11 44+6*V(1) -8 <C(01) 107+V(1) 01 [*]*
12 46+6*V(1) -10 <A(10) 01 107+V(1) 01 [*]*
13 49+6*V(1) -7 01 (11)A> 01 107+V(1) 01 [*]*
14 51+6*V(1) -5 01 11 (11)D> 107+V(1) 01 [*]*
15 79+10*V(1) 9+2*V(1) 01 118+V(1) (11)D> 01 [*]*
16 84+10*V(1) 6+2*V(1) 01 118+V(1) <E(01) 00 [*]*
17 100+12*V(1) -10 01 <E(01) 018+V(1) 00 [*]*
18 102+12*V(1) -12 <B(01) 019+V(1) 00 [*]*
19 110+12*V(1) -14 <E(01) 00 019+V(1) 00 [*]*
20 112+12*V(1) -16 <A(01) 01 00 019+V(1) 00 [*]*
<< Success! ==> defined new CTR 11 (PPA)
950767 61586255583 -587253 <A(01) 01 00 01293629 00 10
== Executing PA-CTR 2, V(1)=293626, V(2)=0, repcount=146814, factor=5/2
2272093 384904891245 -1468137 <A(01) 01734071 00 01 00 10
2272094 384904891249 -1468139 <B(00) 11 01734071 00 01 00 10
2272095 384904891254 -1468136 11 (11)B> 11 01734071 00 01 00 10
2272096 384904891256 -1468134 112 (10)B> 01734071 00 01 00 10
2272097 384907827540 8 11734073 (10)B> 00 01 00 10
2272098 384907827544 10 11734074 (11)A> 01 00 10
2272099 384907827546 12 11734075 (11)D> 00 10
2272100 384907827548 14 11734076 (11)B> 10
2272101 384907827550 16 11734077 (11)A>
2272102 384907827555 13 11734077 <C(10) 01
2272103 384909295709 -1468141 <C(10) 10734077 01
2272104 384909295711 -1468143 <A(10) 10734078 01
2272105 384909295714 -1468140 01 (11)A> 10734078 01
2272106 384909295717 -1468143 01 <C(10) 00 10734077 01
2272107 384909295719 -1468145 <F(10) 10 00 10734077 01
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <A(01) 011+V(1) 00 01 00 10
1 4 -2 <B(00) 11 011+V(1) 00 01 00 10
2 9 1 11 (11)B> 11 011+V(1) 00 01 00 10
3 11 3 112 (10)B> 011+V(1) 00 01 00 10
4 15+4*V(1) 5+2*V(1) 113+V(1) (10)B> 00 01 00 10
5 19+4*V(1) 7+2*V(1) 114+V(1) (11)A> 01 00 10
6 21+4*V(1) 9+2*V(1) 115+V(1) (11)D> 00 10
7 23+4*V(1) 11+2*V(1) 116+V(1) (11)B> 10
8 25+4*V(1) 13+2*V(1) 117+V(1) (11)A>
9 30+4*V(1) 10+2*V(1) 117+V(1) <C(10) 01
10 44+6*V(1) -4 <C(10) 107+V(1) 01
11 46+6*V(1) -6 <A(10) 108+V(1) 01
12 49+6*V(1) -3 01 (11)A> 108+V(1) 01
13 52+6*V(1) -6 01 <C(10) 00 107+V(1) 01
14 54+6*V(1) -8 <F(10) 10 00 107+V(1) 01
<< Success! ==> defined new CTR 12 (PPA)
2272107 384909295719 -1468145 <F(10) 10 00 10734077 01
== Executing PA-CTR 7, V(1)=734074, V(2)=0, repcount=367038, factor=5/2
5942487 2405671139253 -3670373 <F(10) 101835191 00 10 01
5942488 2405671139257 -3670375 <C(01) 101835192 00 10 01
5942489 2405671139259 -3670377 <A(10) 01 101835192 00 10 01
5942490 2405671139262 -3670374 01 (11)A> 01 101835192 00 10 01
5942491 2405671139264 -3670372 01 11 (11)D> 101835192 00 10 01
5942492 2405678480032 12 01 111835193 (11)D> 00 10 01
5942493 2405678480034 14 01 111835194 (11)B> 10 01
5942494 2405678480036 16 01 111835195 (11)A> 01
5942495 2405678480038 18 01 111835196 (11)D>
5942496 2405678480040 20 01 111835197 (11)B>
5942497 2405678480043 17 01 111835197 <E(00) 10
5942498 2405678480045 15 01 111835196 <E(01) 00 10
5942499 2405682150437 -3670377 01 <E(01) 011835196 00 10
5942500 2405682150439 -3670379 <B(01) 011835197 00 10
5942501 2405682150447 -3670381 <E(01) 00 011835197 00 10
5942502 2405682150449 -3670383 <A(01) 01 00 011835197 00 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <F(10) 101+V(1) 00 10 01
1 4 -2 <C(01) 102+V(1) 00 10 01
2 6 -4 <A(10) 01 102+V(1) 00 10 01
3 9 -1 01 (11)A> 01 102+V(1) 00 10 01
4 11 1 01 11 (11)D> 102+V(1) 00 10 01
5 19+4*V(1) 5+2*V(1) 01 113+V(1) (11)D> 00 10 01
6 21+4*V(1) 7+2*V(1) 01 114+V(1) (11)B> 10 01
7 23+4*V(1) 9+2*V(1) 01 115+V(1) (11)A> 01
8 25+4*V(1) 11+2*V(1) 01 116+V(1) (11)D>
9 27+4*V(1) 13+2*V(1) 01 117+V(1) (11)B>
10 30+4*V(1) 10+2*V(1) 01 117+V(1) <E(00) 10
11 32+4*V(1) 8+2*V(1) 01 116+V(1) <E(01) 00 10
12 44+6*V(1) -4 01 <E(01) 016+V(1) 00 10
13 46+6*V(1) -6 <B(01) 017+V(1) 00 10
14 54+6*V(1) -8 <E(01) 00 017+V(1) 00 10
15 56+6*V(1) -10 <A(01) 01 00 017+V(1) 00 10
<< Success! ==> defined new CTR 13 (PPA)
5942502 2405682150449 -3670383 <A(01) 01 00 011835197 00 10
== Executing PA-CTR 2, V(1)=1835194, V(2)=0, repcount=917598, factor=5/2
14200884 15035494599263 -9175971 <A(01) 014587991 00 01 00 10
== Executing PPA-CTR 12 (once), V(1)=4587990
14200898 15035522127257 -9175979 <F(10) 10 00 104587997 01
== Executing PA-CTR 7, V(1)=4587994, V(2)=0, repcount=2293998, factor=5/2
37140878 93971977249271 -22939967 <F(10) 1011469991 00 10 01
== Executing PPA-CTR 13 (once), V(1)=11469990
37140893 93972046069267 -22939977 <A(01) 01 00 0111469997 00 10
== Executing PA-CTR 2, V(1)=11469994, V(2)=0, repcount=5734998, factor=5/2
88755875 587325208874281 -57349965 <A(01) 0128674991 00 01 00 10
== Executing PPA-CTR 12 (once), V(1)=28674990
88755889 587325380924275 -57349973 <F(10) 10 00 1028674997 01
== Executing PA-CTR 7, V(1)=28674994, V(2)=0, repcount=14337498, factor=5/2
232130869 3670783444186789 -143374961 <F(10) 1071687491 00 10 01
== Executing PPA-CTR 13 (once), V(1)=71687490
232130884 3670783874311785 -143374971 <A(01) 01 00 0171687497 00 10
== Executing PA-CTR 2, V(1)=71687494, V(2)=0, repcount=35843748, factor=5/2
554724616 22942398759030549 -358437459 <A(01) 01179218741 00 01 00 10
== Executing PPA-CTR 12 (once), V(1)=179218740
554724630 22942399834343043 -358437467 <F(10) 10 00 10179218747 01
== Executing PA-CTR 7, V(1)=179218744, V(2)=0, repcount=89609373, factor=5/2
1450818360 1433899[4]7155557 -896093705 <F(10) 10448046866 00 10 01
== Executing PPA-CTR 13 (once), V(1)=448046865
1450818375 1433900[4]5436803 -896093715 <A(01) 01 00 01448046872 00 10
== Executing PA-CTR 2, V(1)=448046869, V(2)=0, repcount=224023435, factor=5/2
3467029290 8961874[4]5964183 -2240234325 <A(01) 011120117176 00 012 00 10
== Executing PPA-CTR 3 (once), V(1)=1120117175
3467029310 8961875[4]7370393 -2240234339 <F(10) 10 00 101120117184 01 10
== Executing PA-CTR 1, V(1)=1120117181, V(2)=0, repcount=560058591, factor=5/2
9067615220 5601171[5]2297201 -5600585885 <F(10) 102800292956 00 102 01 10
9067615221 5601171[5]2297205 -5600585887 <C(01) 102800292957 00 102 01 10
9067615222 5601171[5]2297207 -5600585889 <A(10) 01 102800292957 00 102 01 10
9067615223 5601171[5]2297210 -5600585886 01 (11)A> 01 102800292957 00 102 01 10
9067615224 5601171[5]2297212 -5600585884 01 11 (11)D> 102800292957 00 102 01 10
9067615225 5601171[5]3469040 30 01 112800292958 (11)D> 00 102 01 10
9067615226 5601171[5]3469042 32 01 112800292959 (11)B> 102 01 10
9067615227 5601171[5]3469044 34 01 112800292960 (11)A> 10 01 10
9067615228 5601171[5]3469047 31 01 112800292960 <C(10) 00 01 10
9067615229 5601171[5]4054967 -5600585889 01 <C(10) 102800292960 00 01 10
9067615230 5601171[5]4054969 -5600585891 <F(10) 102800292961 00 01 10
9067615231 5601171[5]4054973 -5600585893 <C(01) 102800292962 00 01 10
9067615232 5601171[5]4054975 -5600585895 <A(10) 01 102800292962 00 01 10
9067615233 5601171[5]4054978 -5600585892 01 (11)A> 01 102800292962 00 01 10
9067615234 5601171[5]4054980 -5600585890 01 11 (11)D> 102800292962 00 01 10
9067615235 5601171[5]5226828 34 01 112800292963 (11)D> 00 01 10
9067615236 5601171[5]5226830 36 01 112800292964 (11)B> 01 10
9067615237 5601171[5]5226833 33 01 112800292964 <E(00) 11 10
9067615238 5601171[5]5226835 31 01 112800292963 <E(01) 00 11 10
9067615239 5601171[5]5812761 -5600585895 01 <E(01) 012800292963 00 11 10
9067615240 5601171[5]5812763 -5600585897 <B(01) 012800292964 00 11 10
9067615241 5601171[5]5812771 -5600585899 <E(01) 00 012800292964 00 11 10
9067615242 5601171[5]5812773 -5600585901 <A(01) 01 00 012800292964 00 11 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <F(10) 101+V(1) 00 102 01 [*]*
1 4 -2 <C(01) 102+V(1) 00 102 01 [*]*
2 6 -4 <A(10) 01 102+V(1) 00 102 01 [*]*
3 9 -1 01 (11)A> 01 102+V(1) 00 102 01 [*]*
4 11 1 01 11 (11)D> 102+V(1) 00 102 01 [*]*
5 19+4*V(1) 5+2*V(1) 01 113+V(1) (11)D> 00 102 01 [*]*
6 21+4*V(1) 7+2*V(1) 01 114+V(1) (11)B> 102 01 [*]*
7 23+4*V(1) 9+2*V(1) 01 115+V(1) (11)A> 10 01 [*]*
8 26+4*V(1) 6+2*V(1) 01 115+V(1) <C(10) 00 01 [*]*
9 36+6*V(1) -4 01 <C(10) 105+V(1) 00 01 [*]*
10 38+6*V(1) -6 <F(10) 106+V(1) 00 01 [*]*
11 42+6*V(1) -8 <C(01) 107+V(1) 00 01 [*]*
12 44+6*V(1) -10 <A(10) 01 107+V(1) 00 01 [*]*
13 47+6*V(1) -7 01 (11)A> 01 107+V(1) 00 01 [*]*
14 49+6*V(1) -5 01 11 (11)D> 107+V(1) 00 01 [*]*
15 77+10*V(1) 9+2*V(1) 01 118+V(1) (11)D> 00 01 [*]*
16 79+10*V(1) 11+2*V(1) 01 119+V(1) (11)B> 01 [*]*
17 82+10*V(1) 8+2*V(1) 01 119+V(1) <E(00) 11 [*]*
18 84+10*V(1) 6+2*V(1) 01 118+V(1) <E(01) 00 11 [*]*
19 100+12*V(1) -10 01 <E(01) 018+V(1) 00 11 [*]*
20 102+12*V(1) -12 <B(01) 019+V(1) 00 11 [*]*
21 110+12*V(1) -14 <E(01) 00 019+V(1) 00 11 [*]*
22 112+12*V(1) -16 <A(01) 01 00 019+V(1) 00 11 [*]*
<< Success! ==> defined new CTR 14 (PPA)
9067615242 5601171[5]5812773 -5600585901 <A(01) 01 00 012800292964 00 11 10
== Executing PA-CTR 4, V(1)=2800292961, V(2)=0, repcount=1400146481, factor=5/2
21668933571 3500732[6]9432251 -14001464787 <A(01) 017000732406 00 012 00 11 10
21668933572 3500732[6]9432255 -14001464789 <B(00) 11 017000732406 00 012 00 11 10
21668933573 3500732[6]9432260 -14001464786 11 (11)B> 11 017000732406 00 012 00 11 10
21668933574 3500732[6]9432262 -14001464784 112 (10)B> 017000732406 00 012 00 11 10
21668933575 3500732[6]2361886 28 117000732408 (10)B> 00 012 00 11 10
21668933576 3500732[6]2361890 30 117000732409 (11)A> 012 00 11 10
21668933577 3500732[6]2361892 32 117000732410 (11)D> 01 00 11 10
21668933578 3500732[6]2361897 29 117000732410 <E(01) 002 11 10
21668933579 3500732[6]3826717 -14001464791 <E(01) 017000732410 002 11 10
21668933580 3500732[6]3826719 -14001464793 <A(01) 017000732411 002 11 10
21668933581 3500732[6]3826723 -14001464795 <B(00) 11 017000732411 002 11 10
21668933582 3500732[6]3826728 -14001464792 11 (11)B> 11 017000732411 002 11 10
21668933583 3500732[6]3826730 -14001464790 112 (10)B> 017000732411 002 11 10
21668933584 3500732[6]6756374 32 117000732413 (10)B> 002 11 10
21668933585 3500732[6]6756378 34 117000732414 (11)A> 00 11 10
21668933586 3500732[6]6756383 31 117000732414 <C(10) 01 11 10
21668933587 3500732[6]8221211 -14001464797 <C(10) 107000732414 01 11 10
21668933588 3500732[6]8221213 -14001464799 <A(10) 107000732415 01 11 10
21668933589 3500732[6]8221216 -14001464796 01 (11)A> 107000732415 01 11 10
21668933590 3500732[6]8221219 -14001464799 01 <C(10) 00 107000732414 01 11 10
21668933591 3500732[6]8221221 -14001464801 <F(10) 10 00 107000732414 01 11 10
21668933592 3500732[6]8221225 -14001464803 <C(01) 102 00 107000732414 01 11 10
21668933593 3500732[6]8221227 -14001464805 <A(10) 01 102 00 107000732414 01 11 10
21668933594 3500732[6]8221230 -14001464802 01 (11)A> 01 102 00 107000732414 01 11 10
21668933595 3500732[6]8221232 -14001464800 01 11 (11)D> 102 00 107000732414 01 11 10
21668933596 3500732[6]8221240 -14001464796 01 113 (11)D> 00 107000732414 01 11 10
21668933597 3500732[6]8221242 -14001464794 01 114 (11)B> 107000732414 01 11 10
21668933598 3500732[6]8221244 -14001464792 01 115 (11)A> 107000732413 01 11 10
21668933599 3500732[6]8221247 -14001464795 01 115 <C(10) 00 107000732412 01 11 10
21668933600 3500732[6]8221257 -14001464805 01 <C(10) 105 00 107000732412 01 11 10
21668933601 3500732[6]8221259 -14001464807 <F(10) 106 00 107000732412 01 11 10
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <F(10) 101+V(2) 00 103+V(1) [*]* [*]* [*]*
1 4 -2 <C(01) 102+V(2) 00 103+V(1) [*]* [*]* [*]*
2 6 -4 <A(10) 01 102+V(2) 00 103+V(1) [*]* [*]* [*]*
3 9 -1 01 (11)A> 01 102+V(2) 00 103+V(1) [*]* [*]* [*]*
4 11 1 01 11 (11)D> 102+V(2) 00 103+V(1) [*]* [*]* [*]*
5 19+4*V(2) 5+2*V(2) 01 113+V(2) (11)D> 00 103+V(1) [*]* [*]* [*]*
6 21+4*V(2) 7+2*V(2) 01 114+V(2) (11)B> 103+V(1) [*]* [*]* [*]*
7 23+4*V(2) 9+2*V(2) 01 115+V(2) (11)A> 102+V(1) [*]* [*]* [*]*
8 26+4*V(2) 6+2*V(2) 01 115+V(2) <C(10) 00 101+V(1) [*]* [*]* [*]*
9 36+6*V(2) -4 01 <C(10) 105+V(2) 00 101+V(1) [*]* [*]* [*]*
10 38+6*V(2) -6 <F(10) 106+V(2) 00 101+V(1) [*]* [*]* [*]*
<< Success! ==> defined new CTR 15 (PA)
21668933601 3500732[6]8221259 -14001464807 <F(10) 106 00 107000732412 01 11 10
== Executing PA-CTR 15, V(1)=7000732409, V(2)=5, repcount=3500366205, factor=5/2
56672595651 2187957[7]9160499 -35003662037 <F(10) 1017501831031 00 102 01 11 10
56672595652 2187957[7]9160503 -35003662039 <C(01) 1017501831032 00 102 01 11 10
56672595653 2187957[7]9160505 -35003662041 <A(10) 01 1017501831032 00 102 01 11 10
56672595654 2187957[7]9160508 -35003662038 01 (11)A> 01 1017501831032 00 102 01 11 10
56672595655 2187957[7]9160510 -35003662036 01 11 (11)D> 1017501831032 00 102 01 11 10
56672595656 2187957[7]6484638 28 01 1117501831033 (11)D> 00 102 01 11 10
56672595657 2187957[7]6484640 30 01 1117501831034 (11)B> 102 01 11 10
56672595658 2187957[7]6484642 32 01 1117501831035 (11)A> 10 01 11 10
56672595659 2187957[7]6484645 29 01 1117501831035 <C(10) 00 01 11 10
56672595660 2187957[7]0146715 -35003662041 01 <C(10) 1017501831035 00 01 11 10
56672595661 2187957[7]0146717 -35003662043 <F(10) 1017501831036 00 01 11 10
56672595662 2187957[7]0146721 -35003662045 <C(01) 1017501831037 00 01 11 10
56672595663 2187957[7]0146723 -35003662047 <A(10) 01 1017501831037 00 01 11 10
56672595664 2187957[7]0146726 -35003662044 01 (11)A> 01 1017501831037 00 01 11 10
56672595665 2187957[7]0146728 -35003662042 01 11 (11)D> 1017501831037 00 01 11 10
56672595666 2187957[7]7470876 32 01 1117501831038 (11)D> 00 01 11 10
56672595667 2187957[7]7470878 34 01 1117501831039 (11)B> 01 11 10
56672595668 2187957[7]7470881 31 01 1117501831039 <E(00) 112 10
56672595669 2187957[7]7470883 29 01 1117501831038 <E(01) 00 112 10
56672595670 2187957[7]1132959 -35003662047 01 <E(01) 0117501831038 00 112 10
56672595671 2187957[7]1132961 -35003662049 <B(01) 0117501831039 00 112 10
56672595672 2187957[7]1132969 -35003662051 <E(01) 00 0117501831039 00 112 10
56672595673 2187957[7]1132971 -35003662053 <A(01) 01 00 0117501831039 00 112 10
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <F(10) 101+V(2) 00 102 01 111+V(1) [*]*
1 4 -2 <C(01) 102+V(2) 00 102 01 111+V(1) [*]*
2 6 -4 <A(10) 01 102+V(2) 00 102 01 111+V(1) [*]*
3 9 -1 01 (11)A> 01 102+V(2) 00 102 01 111+V(1) [*]*
4 11 1 01 11 (11)D> 102+V(2) 00 102 01 111+V(1) [*]*
5 19+4*V(2) 5+2*V(2) 01 113+V(2) (11)D> 00 102 01 111+V(1) [*]*
6 21+4*V(2) 7+2*V(2) 01 114+V(2) (11)B> 102 01 111+V(1) [*]*
7 23+4*V(2) 9+2*V(2) 01 115+V(2) (11)A> 10 01 111+V(1) [*]*
8 26+4*V(2) 6+2*V(2) 01 115+V(2) <C(10) 00 01 111+V(1) [*]*
9 36+6*V(2) -4 01 <C(10) 105+V(2) 00 01 111+V(1) [*]*
10 38+6*V(2) -6 <F(10) 106+V(2) 00 01 111+V(1) [*]*
11 42+6*V(2) -8 <C(01) 107+V(2) 00 01 111+V(1) [*]*
12 44+6*V(2) -10 <A(10) 01 107+V(2) 00 01 111+V(1) [*]*
13 47+6*V(2) -7 01 (11)A> 01 107+V(2) 00 01 111+V(1) [*]*
14 49+6*V(2) -5 01 11 (11)D> 107+V(2) 00 01 111+V(1) [*]*
15 77+10*V(2) 9+2*V(2) 01 118+V(2) (11)D> 00 01 111+V(1) [*]*
16 79+10*V(2) 11+2*V(2) 01 119+V(2) (11)B> 01 111+V(1) [*]*
17 82+10*V(2) 8+2*V(2) 01 119+V(2) <E(00) 112+V(1) [*]*
18 84+10*V(2) 6+2*V(2) 01 118+V(2) <E(01) 00 112+V(1) [*]*
19 100+12*V(2) -10 01 <E(01) 018+V(2) 00 112+V(1) [*]*
20 102+12*V(2) -12 <B(01) 019+V(2) 00 112+V(1) [*]*
21 110+12*V(2) -14 <E(01) 00 019+V(2) 00 112+V(1) [*]*
22 112+12*V(2) -16 <A(01) 01 00 019+V(2) 00 112+V(1) [*]*
<< Success! ==> defined new CTR 16 (PPA)
56672595673 2187957[7]1132971 -35003662053 <A(01) 01 00 0117501831039 00 112 10
== Executing PA-CTR 4, V(1)=17501831036, V(2)=0, repcount=8750915519, factor=5/2
135430835344 1367473[8]7780323 -87509155167 <A(01) 0143754577596 00 01 00 112 10
135430835345 1367473[8]7780327 -87509155169 <B(00) 11 0143754577596 00 01 00 112 10
135430835346 1367473[8]7780332 -87509155166 11 (11)B> 11 0143754577596 00 01 00 112 10
135430835347 1367473[8]7780334 -87509155164 112 (10)B> 0143754577596 00 01 00 112 10
135430835348 1367473[8]6090718 28 1143754577598 (10)B> 00 01 00 112 10
135430835349 1367473[8]6090722 30 1143754577599 (11)A> 01 00 112 10
135430835350 1367473[8]6090724 32 1143754577600 (11)D> 00 112 10
135430835351 1367473[8]6090726 34 1143754577601 (11)B> 112 10
135430835352 1367473[8]6090728 36 1143754577602 (10)B> 11 10
135430835353 1367473[8]6090730 38 1143754577602 10 (10)B> 10
135430835354 1367473[8]6090732 40 1143754577602 102 (11)A>
135430835355 1367473[8]6090737 37 1143754577602 102 <C(10) 01
135430835356 1367473[8]6090749 33 1143754577602 <C(10) 002 01
135430835357 1367473[8]5245953 -87509155171 <C(10) 1043754577602 002 01
135430835358 1367473[8]5245955 -87509155173 <A(10) 1043754577603 002 01
135430835359 1367473[8]5245958 -87509155170 01 (11)A> 1043754577603 002 01
135430835360 1367473[8]5245961 -87509155173 01 <C(10) 00 1043754577602 002 01
135430835361 1367473[8]5245963 -87509155175 <F(10) 10 00 1043754577602 002 01
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <A(01) 011+V(2) 00 01 00 112+V(1) 10
1 4 -2 <B(00) 11 011+V(2) 00 01 00 112+V(1) 10
2 9 1 11 (11)B> 11 011+V(2) 00 01 00 112+V(1) 10
3 11 3 112 (10)B> 011+V(2) 00 01 00 112+V(1) 10
4 15+4*V(2) 5+2*V(2) 113+V(2) (10)B> 00 01 00 112+V(1) 10
5 19+4*V(2) 7+2*V(2) 114+V(2) (11)A> 01 00 112+V(1) 10
6 21+4*V(2) 9+2*V(2) 115+V(2) (11)D> 00 112+V(1) 10
7 23+4*V(2) 11+2*V(2) 116+V(2) (11)B> 112+V(1) 10
8 25+4*V(2) 13+2*V(2) 117+V(2) (10)B> 111+V(1) 10
9 27+2*V(1)+4*V(2) 15+2*V(1)+2*V(2) 117+V(2) 101+V(1) (10)B> 10
10 29+2*V(1)+4*V(2) 17+2*V(1)+2*V(2) 117+V(2) 102+V(1) (11)A>
11 34+2*V(1)+4*V(2) 14+2*V(1)+2*V(2) 117+V(2) 102+V(1) <C(10) 01
12 46+8*V(1)+4*V(2) 10+2*V(2) 117+V(2) <C(10) 002+V(1) 01
13 60+8*V(1)+6*V(2) -4 <C(10) 107+V(2) 002+V(1) 01
14 62+8*V(1)+6*V(2) -6 <A(10) 108+V(2) 002+V(1) 01
15 65+8*V(1)+6*V(2) -3 01 (11)A> 108+V(2) 002+V(1) 01
16 68+8*V(1)+6*V(2) -6 01 <C(10) 00 107+V(2) 002+V(1) 01
17 70+8*V(1)+6*V(2) -8 <F(10) 10 00 107+V(2) 002+V(1) 01
<< Success! ==> defined new CTR 17 (PPA)
135430835361 1367473[8]5245963 -87509155175 <F(10) 10 00 1043754577602 002 01
== Executing PA-CTR 1, V(1)=43754577599, V(2)=0, repcount=21877288800, factor=5/2
354203723361 8546710[8]4488363 -218772887975 <F(10) 10109386444001 00 102 002 01
354203723362 8546710[8]4488367 -218772887977 <C(01) 10109386444002 00 102 002 01
354203723363 8546710[8]4488369 -218772887979 <A(10) 01 10109386444002 00 102 002 01
354203723364 8546710[8]4488372 -218772887976 01 (11)A> 01 10109386444002 00 102 002 01
354203723365 8546710[8]4488374 -218772887974 01 11 (11)D> 10109386444002 00 102 002 01
354203723366 8546710[8]0264382 30 01 11109386444003 (11)D> 00 102 002 01
354203723367 8546710[8]0264384 32 01 11109386444004 (11)B> 102 002 01
354203723368 8546710[8]0264386 34 01 11109386444005 (11)A> 10 002 01
354203723369 8546710[8]0264389 31 01 11109386444005 <C(10) 003 01
354203723370 8546710[8]3152399 -218772887979 01 <C(10) 10109386444005 003 01
354203723371 8546710[8]3152401 -218772887981 <F(10) 10109386444006 003 01
354203723372 8546710[8]3152405 -218772887983 <C(01) 10109386444007 003 01
354203723373 8546710[8]3152407 -218772887985 <A(10) 01 10109386444007 003 01
354203723374 8546710[8]3152410 -218772887982 01 (11)A> 01 10109386444007 003 01
354203723375 8546710[8]3152412 -218772887980 01 11 (11)D> 10109386444007 003 01
354203723376 8546710[8]8928440 34 01 11109386444008 (11)D> 003 01
354203723377 8546710[8]8928442 36 01 11109386444009 (11)B> 002 01
354203723378 8546710[8]8928445 33 01 11109386444009 <E(00) 10 00 01
354203723379 8546710[8]8928447 31 01 11109386444008 <E(01) 00 10 00 01
354203723380 8546710[8]1816463 -218772887985 01 <E(01) 01109386444008 00 10 00 01
354203723381 8546710[8]1816465 -218772887987 <B(01) 01109386444009 00 10 00 01
354203723382 8546710[8]1816473 -218772887989 <E(01) 00 01109386444009 00 10 00 01
354203723383 8546710[8]1816475 -218772887991 <A(01) 01 00 01109386444009 00 10 00 01
354203723384 8546710[8]1816479 -218772887993 <B(00) 11 01 00 01109386444009 00 10 00 01
354203723385 8546710[8]1816484 -218772887990 11 (11)B> 11 01 00 01109386444009 00 10 00 01
354203723386 8546710[8]1816486 -218772887988 112 (10)B> 01 00 01109386444009 00 10 00 01
354203723387 8546710[8]1816490 -218772887986 113 (10)B> 00 01109386444009 00 10 00 01
354203723388 8546710[8]1816494 -218772887984 114 (11)A> 01109386444009 00 10 00 01
354203723389 8546710[8]1816496 -218772887982 115 (11)D> 01109386444008 00 10 00 01
354203723390 8546710[8]1816501 -218772887985 115 <E(01) 00 01109386444007 00 10 00 01
354203723391 8546710[8]1816511 -218772887995 <E(01) 015 00 01109386444007 00 10 00 01
354203723392 8546710[8]1816513 -218772887997 <A(01) 016 00 01109386444007 00 10 00 01
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <A(01) 011+V(2) 00 013+V(1) [*]* [*]* [*]* [*]*
1 4 -2 <B(00) 11 011+V(2) 00 013+V(1) [*]* [*]* [*]* [*]*
2 9 1 11 (11)B> 11 011+V(2) 00 013+V(1) [*]* [*]* [*]* [*]*
3 11 3 112 (10)B> 011+V(2) 00 013+V(1) [*]* [*]* [*]* [*]*
4 15+4*V(2) 5+2*V(2) 113+V(2) (10)B> 00 013+V(1) [*]* [*]* [*]* [*]*
5 19+4*V(2) 7+2*V(2) 114+V(2) (11)A> 013+V(1) [*]* [*]* [*]* [*]*
6 21+4*V(2) 9+2*V(2) 115+V(2) (11)D> 012+V(1) [*]* [*]* [*]* [*]*
7 26+4*V(2) 6+2*V(2) 115+V(2) <E(01) 00 011+V(1) [*]* [*]* [*]* [*]*
8 36+6*V(2) -4 <E(01) 015+V(2) 00 011+V(1) [*]* [*]* [*]* [*]*
9 38+6*V(2) -6 <A(01) 016+V(2) 00 011+V(1) [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 18 (PA)
354203723392 8546710[8]1816513 -218772887997 <A(01) 016 00 01109386444007 00 10 00 01
== Executing PA-CTR 18, V(1)=109386444004, V(2)=5, repcount=54693222003, factor=5/2
846442721419 5341693[9]2562807 -546932220015 <A(01) 01273466110021 00 01 00 10 00 01
846442721420 5341693[9]2562811 -546932220017 <B(00) 11 01273466110021 00 01 00 10 00 01
846442721421 5341693[9]2562816 -546932220014 11 (11)B> 11 01273466110021 00 01 00 10 00 01
846442721422 5341693[9]2562818 -546932220012 112 (10)B> 01273466110021 00 01 00 10 00 01
846442721423 5341693[9]7002902 30 11273466110023 (10)B> 00 01 00 10 00 01
846442721424 5341693[9]7002906 32 11273466110024 (11)A> 01 00 10 00 01
846442721425 5341693[9]7002908 34 11273466110025 (11)D> 00 10 00 01
846442721426 5341693[9]7002910 36 11273466110026 (11)B> 10 00 01
846442721427 5341693[9]7002912 38 11273466110027 (11)A> 00 01
846442721428 5341693[9]7002917 35 11273466110027 <C(10) 012
846442721429 5341693[9]9222971 -546932220019 <C(10) 10273466110027 012
846442721430 5341693[9]9222973 -546932220021 <A(10) 10273466110028 012
846442721431 5341693[9]9222976 -546932220018 01 (11)A> 10273466110028 012
846442721432 5341693[9]9222979 -546932220021 01 <C(10) 00 10273466110027 012
846442721433 5341693[9]9222981 -546932220023 <F(10) 10 00 10273466110027 012
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <A(01) 011+V(2) 00 01 00 10 00 011+V(1)
1 4 -2 <B(00) 11 011+V(2) 00 01 00 10 00 011+V(1)
2 9 1 11 (11)B> 11 011+V(2) 00 01 00 10 00 011+V(1)
3 11 3 112 (10)B> 011+V(2) 00 01 00 10 00 011+V(1)
4 15+4*V(2) 5+2*V(2) 113+V(2) (10)B> 00 01 00 10 00 011+V(1)
5 19+4*V(2) 7+2*V(2) 114+V(2) (11)A> 01 00 10 00 011+V(1)
6 21+4*V(2) 9+2*V(2) 115+V(2) (11)D> 00 10 00 011+V(1)
7 23+4*V(2) 11+2*V(2) 116+V(2) (11)B> 10 00 011+V(1)
8 25+4*V(2) 13+2*V(2) 117+V(2) (11)A> 00 011+V(1)
9 30+4*V(2) 10+2*V(2) 117+V(2) <C(10) 012+V(1)
10 44+6*V(2) -4 <C(10) 107+V(2) 012+V(1)
11 46+6*V(2) -6 <A(10) 108+V(2) 012+V(1)
12 49+6*V(2) -3 01 (11)A> 108+V(2) 012+V(1)
13 52+6*V(2) -6 01 <C(10) 00 107+V(2) 012+V(1)
14 54+6*V(2) -8 <F(10) 10 00 107+V(2) 012+V(1)
<< Success! ==> defined new CTR 19 (PPA)
846442721433 5341693[9]9222981 -546932220023 <F(10) 10 00 10273466110027 012
== Executing PA-CTR 7, V(1)=273466110024, V(2)=0, repcount=136733055013, factor=5/2
2213773271563 3338558[10]5940815 -1367330550101 <F(10) 10683665275066 00 10 012
2213773271564 3338558[10]5940819 -1367330550103 <C(01) 10683665275067 00 10 012
2213773271565 3338558[10]5940821 -1367330550105 <A(10) 01 10683665275067 00 10 012
2213773271566 3338558[10]5940824 -1367330550102 01 (11)A> 01 10683665275067 00 10 012
2213773271567 3338558[10]5940826 -1367330550100 01 11 (11)D> 10683665275067 00 10 012
2213773271568 3338558[10]7041094 34 01 11683665275068 (11)D> 00 10 012
2213773271569 3338558[10]7041096 36 01 11683665275069 (11)B> 10 012
2213773271570 3338558[10]7041098 38 01 11683665275070 (11)A> 012
2213773271571 3338558[10]7041100 40 01 11683665275071 (11)D> 01
2213773271572 3338558[10]7041105 37 01 11683665275071 <E(01)
2213773271573 3338558[10]7591247 -1367330550105 01 <E(01) 01683665275071
2213773271574 3338558[10]7591249 -1367330550107 <B(01) 01683665275072
2213773271575 3338558[10]7591257 -1367330550109 <E(01) 00 01683665275072
2213773271576 3338558[10]7591259 -1367330550111 <A(01) 01 00 01683665275072
2213773271577 3338558[10]7591263 -1367330550113 <B(00) 11 01 00 01683665275072
2213773271578 3338558[10]7591268 -1367330550110 11 (11)B> 11 01 00 01683665275072
2213773271579 3338558[10]7591270 -1367330550108 112 (10)B> 01 00 01683665275072
2213773271580 3338558[10]7591274 -1367330550106 113 (10)B> 00 01683665275072
2213773271581 3338558[10]7591278 -1367330550104 114 (11)A> 01683665275072
2213773271582 3338558[10]7591280 -1367330550102 115 (11)D> 01683665275071
2213773271583 3338558[10]7591285 -1367330550105 115 <E(01) 00 01683665275070
2213773271584 3338558[10]7591295 -1367330550115 <E(01) 015 00 01683665275070
2213773271585 3338558[10]7591297 -1367330550117 <A(01) 016 00 01683665275070
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <A(01) 011+V(2) 00 013+V(1)
1 4 -2 <B(00) 11 011+V(2) 00 013+V(1)
2 9 1 11 (11)B> 11 011+V(2) 00 013+V(1)
3 11 3 112 (10)B> 011+V(2) 00 013+V(1)
4 15+4*V(2) 5+2*V(2) 113+V(2) (10)B> 00 013+V(1)
5 19+4*V(2) 7+2*V(2) 114+V(2) (11)A> 013+V(1)
6 21+4*V(2) 9+2*V(2) 115+V(2) (11)D> 012+V(1)
7 26+4*V(2) 6+2*V(2) 115+V(2) <E(01) 00 011+V(1)
8 36+6*V(2) -4 <E(01) 015+V(2) 00 011+V(1)
9 38+6*V(2) -6 <A(01) 016+V(2) 00 011+V(1)
<< Success! ==> defined new CTR 20 (PA)
2213773271585 3338558[10]7591297 -1367330550117 <A(01) 016 00 01683665275070
== Executing PA-CTR 20, V(1)=683665275067, V(2)=5, repcount=341832637534, factor=5/2
5290267009391 2086599[11]1397939 -3418326375321 <A(01) 011709163187676 00 012
5290267009392 2086599[11]1397943 -3418326375323 <B(00) 11 011709163187676 00 012
5290267009393 2086599[11]1397948 -3418326375320 11 (11)B> 11 011709163187676 00 012
5290267009394 2086599[11]1397950 -3418326375318 112 (10)B> 011709163187676 00 012
5290267009395 2086599[11]4148654 34 111709163187678 (10)B> 00 012
5290267009396 2086599[11]4148658 36 111709163187679 (11)A> 012
5290267009397 2086599[11]4148660 38 111709163187680 (11)D> 01
5290267009398 2086599[11]4148665 35 111709163187680 <E(01)
5290267009399 2086599[11]0524025 -3418326375325 <E(01) 011709163187680
5290267009400 2086599[11]0524027 -3418326375327 <A(01) 011709163187681
5290267009401 2086599[11]0524031 -3418326375329 <B(00) 11 011709163187681
5290267009402 2086599[11]0524036 -3418326375326 11 (11)B> 11 011709163187681
5290267009403 2086599[11]0524038 -3418326375324 112 (10)B> 011709163187681
5290267009404 2086599[11]3274762 38 111709163187683 (10)B>
5290267009405 2086599[11]3274766 40 111709163187684 (11)A>
5290267009406 2086599[11]3274771 37 111709163187684 <C(10) 01
5290267009407 2086599[11]9650139 -3418326375331 <C(10) 101709163187684 01
5290267009408 2086599[11]9650141 -3418326375333 <A(10) 101709163187685 01
5290267009409 2086599[11]9650144 -3418326375330 01 (11)A> 101709163187685 01
5290267009410 2086599[11]9650147 -3418326375333 01 <C(10) 00 101709163187684 01
5290267009411 2086599[11]9650149 -3418326375335 <F(10) 10 00 101709163187684 01
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <A(01) 011+V(1) 00 012
1 4 -2 <B(00) 11 011+V(1) 00 012
2 9 1 11 (11)B> 11 011+V(1) 00 012
3 11 3 112 (10)B> 011+V(1) 00 012
4 15+4*V(1) 5+2*V(1) 113+V(1) (10)B> 00 012
5 19+4*V(1) 7+2*V(1) 114+V(1) (11)A> 012
6 21+4*V(1) 9+2*V(1) 115+V(1) (11)D> 01
7 26+4*V(1) 6+2*V(1) 115+V(1) <E(01)
8 36+6*V(1) -4 <E(01) 015+V(1)
9 38+6*V(1) -6 <A(01) 016+V(1)
10 42+6*V(1) -8 <B(00) 11 016+V(1)
11 47+6*V(1) -5 11 (11)B> 11 016+V(1)
12 49+6*V(1) -3 112 (10)B> 016+V(1)
13 73+10*V(1) 9+2*V(1) 118+V(1) (10)B>
14 77+10*V(1) 11+2*V(1) 119+V(1) (11)A>
15 82+10*V(1) 8+2*V(1) 119+V(1) <C(10) 01
16 100+12*V(1) -10 <C(10) 109+V(1) 01
17 102+12*V(1) -12 <A(10) 1010+V(1) 01
18 105+12*V(1) -9 01 (11)A> 1010+V(1) 01
19 108+12*V(1) -12 01 <C(10) 00 109+V(1) 01
20 110+12*V(1) -14 <F(10) 10 00 109+V(1) 01
<< Success! ==> defined new CTR 21 (PPA)
5290267009411 2086599[11]9650149 -3418326375335 <F(10) 10 00 101709163187684 01
== Executing PA-CTR 7, V(1)=1709163187681, V(2)=0, repcount=854581593841, factor=5/2
13836082947821 1304124[12]3307707 -8545815938381 <F(10) 104272907969206 00 102 01
== Executing PPA-CTR 8 (once), V(1)=4272907969205
13836082947843 1304124[12]8938279 -8545815938397 <A(01) 01 00 014272907969214 00 11
== Executing PA-CTR 2, V(1)=4272907969211, V(2)=0, repcount=2136453984606, factor=5/2
33064168809297 8150777[12]5212757 -21364539846033 <A(01) 0110682269923031 00 012 00 11
== Executing PPA-CTR 3 (once), V(1)=10682269923030
33064168809317 8150777[12]4289227 -21364539846047 <F(10) 10 00 1010682269923039 01 11
== Executing PA-CTR 1, V(1)=10682269923036, V(2)=0, repcount=5341134961519, factor=5/2
86475518424507 5094236[13]0214579 -53411349615161 <F(10) 1026705674807596 00 10 01 11
== Executing PPA-CTR 9 (once), V(1)=26705674807595
86475518424524 5094236[13]9060213 -53411349615171 <A(01) 01 00 0126705674807602 002 10
== Executing PA-CTR 2, V(1)=26705674807599, V(2)=0, repcount=13352837403800, factor=5/2
206651055058724 3183897[14]5947613 -133528374037971 <A(01) 0166764187019001 00 012 002 10
206651055058725 3183897[14]5947617 -133528374037973 <B(00) 11 0166764187019001 00 012 002 10
206651055058726 3183897[14]5947622 -133528374037970 11 (11)B> 11 0166764187019001 00 012 002 10
206651055058727 3183897[14]5947624 -133528374037968 112 (10)B> 0166764187019001 00 012 002 10
206651055058728 3183897[14]4023628 34 1166764187019003 (10)B> 00 012 002 10
206651055058729 3183897[14]4023632 36 1166764187019004 (11)A> 012 002 10
206651055058730 3183897[14]4023634 38 1166764187019005 (11)D> 01 002 10
206651055058731 3183897[14]4023639 35 1166764187019005 <E(01) 003 10
206651055058732 3183897[14]8061649 -133528374037975 <E(01) 0166764187019005 003 10
206651055058733 3183897[14]8061651 -133528374037977 <A(01) 0166764187019006 003 10
206651055058734 3183897[14]8061655 -133528374037979 <B(00) 11 0166764187019006 003 10
206651055058735 3183897[14]8061660 -133528374037976 11 (11)B> 11 0166764187019006 003 10
206651055058736 3183897[14]8061662 -133528374037974 112 (10)B> 0166764187019006 003 10
206651055058737 3183897[14]6137686 38 1166764187019008 (10)B> 003 10
206651055058738 3183897[14]6137690 40 1166764187019009 (11)A> 002 10
206651055058739 3183897[14]6137695 37 1166764187019009 <C(10) 01 00 10
206651055058740 3183897[14]0175713 -133528374037981 <C(10) 1066764187019009 01 00 10
206651055058741 3183897[14]0175715 -133528374037983 <A(10) 1066764187019010 01 00 10
206651055058742 3183897[14]0175718 -133528374037980 01 (11)A> 1066764187019010 01 00 10
206651055058743 3183897[14]0175721 -133528374037983 01 <C(10) 00 1066764187019009 01 00 10
206651055058744 3183897[14]0175723 -133528374037985 <F(10) 10 00 1066764187019009 01 00 10
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <A(01) 011+V(2) 00 012 002+V(1) [*]*
1 4 -2 <B(00) 11 011+V(2) 00 012 002+V(1) [*]*
2 9 1 11 (11)B> 11 011+V(2) 00 012 002+V(1) [*]*
3 11 3 112 (10)B> 011+V(2) 00 012 002+V(1) [*]*
4 15+4*V(2) 5+2*V(2) 113+V(2) (10)B> 00 012 002+V(1) [*]*
5 19+4*V(2) 7+2*V(2) 114+V(2) (11)A> 012 002+V(1) [*]*
6 21+4*V(2) 9+2*V(2) 115+V(2) (11)D> 01 002+V(1) [*]*
7 26+4*V(2) 6+2*V(2) 115+V(2) <E(01) 003+V(1) [*]*
8 36+6*V(2) -4 <E(01) 015+V(2) 003+V(1) [*]*
9 38+6*V(2) -6 <A(01) 016+V(2) 003+V(1) [*]*
10 42+6*V(2) -8 <B(00) 11 016+V(2) 003+V(1) [*]*
11 47+6*V(2) -5 11 (11)B> 11 016+V(2) 003+V(1) [*]*
12 49+6*V(2) -3 112 (10)B> 016+V(2) 003+V(1) [*]*
13 73+10*V(2) 9+2*V(2) 118+V(2) (10)B> 003+V(1) [*]*
14 77+10*V(2) 11+2*V(2) 119+V(2) (11)A> 002+V(1) [*]*
15 82+10*V(2) 8+2*V(2) 119+V(2) <C(10) 01 001+V(1) [*]*
16 100+12*V(2) -10 <C(10) 109+V(2) 01 001+V(1) [*]*
17 102+12*V(2) -12 <A(10) 1010+V(2) 01 001+V(1) [*]*
18 105+12*V(2) -9 01 (11)A> 1010+V(2) 01 001+V(1) [*]*
19 108+12*V(2) -12 01 <C(10) 00 109+V(2) 01 001+V(1) [*]*
20 110+12*V(2) -14 <F(10) 10 00 109+V(2) 01 001+V(1) [*]*
<< Success! ==> defined new CTR 22 (PPA)
206651055058744 3183897[14]0175723 -133528374037985 <F(10) 10 00 1066764187019009 01 00 10
== Executing PA-CTR 15, V(1)=66764187019006, V(2)=0, repcount=33382093509504, factor=5/2
540471990153784 1989936[15]5784555 -333820935095009 <F(10) 10166910467547521 00 10 01 00 10
540471990153785 1989936[15]5784559 -333820935095011 <C(01) 10166910467547522 00 10 01 00 10
540471990153786 1989936[15]5784561 -333820935095013 <A(10) 01 10166910467547522 00 10 01 00 10
540471990153787 1989936[15]5784564 -333820935095010 01 (11)A> 01 10166910467547522 00 10 01 00 10
540471990153788 1989936[15]5784566 -333820935095008 01 11 (11)D> 10166910467547522 00 10 01 00 10
540471990153789 1989936[15]5974654 36 01 11166910467547523 (11)D> 00 10 01 00 10
540471990153790 1989936[15]5974656 38 01 11166910467547524 (11)B> 10 01 00 10
540471990153791 1989936[15]5974658 40 01 11166910467547525 (11)A> 01 00 10
540471990153792 1989936[15]5974660 42 01 11166910467547526 (11)D> 00 10
540471990153793 1989936[15]5974662 44 01 11166910467547527 (11)B> 10
540471990153794 1989936[15]5974664 46 01 11166910467547528 (11)A>
540471990153795 1989936[15]5974669 43 01 11166910467547528 <C(10) 01
540471990153796 1989936[15]1069725 -333820935095013 01 <C(10) 10166910467547528 01
540471990153797 1989936[15]1069727 -333820935095015 <F(10) 10166910467547529 01
540471990153798 1989936[15]1069731 -333820935095017 <C(01) 10166910467547530 01
540471990153799 1989936[15]1069733 -333820935095019 <A(10) 01 10166910467547530 01
540471990153800 1989936[15]1069736 -333820935095016 01 (11)A> 01 10166910467547530 01
540471990153801 1989936[15]1069738 -333820935095014 01 11 (11)D> 10166910467547530 01
540471990153802 1989936[15]1259858 46 01 11166910467547531 (11)D> 01
540471990153803 1989936[15]1259863 43 01 11166910467547531 <E(01)
540471990153804 1989936[15]6354925 -333820935095019 01 <E(01) 01166910467547531
540471990153805 1989936[15]6354927 -333820935095021 <B(01) 01166910467547532
540471990153806 1989936[15]6354935 -333820935095023 <E(01) 00 01166910467547532
540471990153807 1989936[15]6354937 -333820935095025 <A(01) 01 00 01166910467547532
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <F(10) 101+V(1) 00 10 01 00 10
1 4 -2 <C(01) 102+V(1) 00 10 01 00 10
2 6 -4 <A(10) 01 102+V(1) 00 10 01 00 10
3 9 -1 01 (11)A> 01 102+V(1) 00 10 01 00 10
4 11 1 01 11 (11)D> 102+V(1) 00 10 01 00 10
5 19+4*V(1) 5+2*V(1) 01 113+V(1) (11)D> 00 10 01 00 10
6 21+4*V(1) 7+2*V(1) 01 114+V(1) (11)B> 10 01 00 10
7 23+4*V(1) 9+2*V(1) 01 115+V(1) (11)A> 01 00 10
8 25+4*V(1) 11+2*V(1) 01 116+V(1) (11)D> 00 10
9 27+4*V(1) 13+2*V(1) 01 117+V(1) (11)B> 10
10 29+4*V(1) 15+2*V(1) 01 118+V(1) (11)A>
11 34+4*V(1) 12+2*V(1) 01 118+V(1) <C(10) 01
12 50+6*V(1) -4 01 <C(10) 108+V(1) 01
13 52+6*V(1) -6 <F(10) 109+V(1) 01
14 56+6*V(1) -8 <C(01) 1010+V(1) 01
15 58+6*V(1) -10 <A(10) 01 1010+V(1) 01
16 61+6*V(1) -7 01 (11)A> 01 1010+V(1) 01
17 63+6*V(1) -5 01 11 (11)D> 1010+V(1) 01
18 103+10*V(1) 15+2*V(1) 01 1111+V(1) (11)D> 01
19 108+10*V(1) 12+2*V(1) 01 1111+V(1) <E(01)
20 130+12*V(1) -10 01 <E(01) 0111+V(1)
21 132+12*V(1) -12 <B(01) 0112+V(1)
22 140+12*V(1) -14 <E(01) 00 0112+V(1)
23 142+12*V(1) -16 <A(01) 01 00 0112+V(1)
<< Success! ==> defined new CTR 23 (PPA)
540471990153807 1989936[15]6354937 -333820935095025 <A(01) 01 00 01166910467547532
== Executing PA-CTR 20, V(1)=166910467547529, V(2)=0, repcount=83455233773765, factor=5/2
1291569094117692 1243710[16]7279907 -834552337737615 <A(01) 01417276168868826 00 012
== Executing PPA-CTR 21 (once), V(1)=417276168868825
1291569094117712 1243710[16]3705917 -834552337737629 <F(10) 10 00 10417276168868834 01
== Executing PA-CTR 7, V(1)=417276168868831, V(2)=0, repcount=208638084434416, factor=5/2
3377949938461872 7773187[16]4613325 -2086380844344125 <F(10) 101043190422172081 00 102 01
== Executing PPA-CTR 8 (once), V(1)=1043190422172080
3377949938461894 7773187[16]0678397 -2086380844344141 <A(01) 01 00 011043190422172089 00 11
== Executing PA-CTR 2, V(1)=1043190422172086, V(2)=0, repcount=521595211086044, factor=5/2
8072306838236290 4858242[17]9206449 -5215952110860405 <A(01) 012607976055430221 00 01 00 11
8072306838236291 4858242[17]9206453 -5215952110860407 <B(00) 11 012607976055430221 00 01 00 11
8072306838236292 4858242[17]9206458 -5215952110860404 11 (11)B> 11 012607976055430221 00 01 00 11
8072306838236293 4858242[17]9206460 -5215952110860402 112 (10)B> 012607976055430221 00 01 00 11
8072306838236294 4858242[17]0927344 40 112607976055430223 (10)B> 00 01 00 11
8072306838236295 4858242[17]0927348 42 112607976055430224 (11)A> 01 00 11
8072306838236296 4858242[17]0927350 44 112607976055430225 (11)D> 00 11
8072306838236297 4858242[17]0927352 46 112607976055430226 (11)B> 11
8072306838236298 4858242[17]0927354 48 112607976055430227 (10)B>
8072306838236299 4858242[17]0927358 50 112607976055430228 (11)A>
8072306838236300 4858242[17]0927363 47 112607976055430228 <C(10) 01
8072306838236301 4858242[17]1787819 -5215952110860409 <C(10) 102607976055430228 01
8072306838236302 4858242[17]1787821 -5215952110860411 <A(10) 102607976055430229 01
8072306838236303 4858242[17]1787824 -5215952110860408 01 (11)A> 102607976055430229 01
8072306838236304 4858242[17]1787827 -5215952110860411 01 <C(10) 00 102607976055430228 01
8072306838236305 4858242[17]1787829 -5215952110860413 <F(10) 10 00 102607976055430228 01
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <A(01) 011+V(1) 00 01 00 11
1 4 -2 <B(00) 11 011+V(1) 00 01 00 11
2 9 1 11 (11)B> 11 011+V(1) 00 01 00 11
3 11 3 112 (10)B> 011+V(1) 00 01 00 11
4 15+4*V(1) 5+2*V(1) 113+V(1) (10)B> 00 01 00 11
5 19+4*V(1) 7+2*V(1) 114+V(1) (11)A> 01 00 11
6 21+4*V(1) 9+2*V(1) 115+V(1) (11)D> 00 11
7 23+4*V(1) 11+2*V(1) 116+V(1) (11)B> 11
8 25+4*V(1) 13+2*V(1) 117+V(1) (10)B>
9 29+4*V(1) 15+2*V(1) 118+V(1) (11)A>
10 34+4*V(1) 12+2*V(1) 118+V(1) <C(10) 01
11 50+6*V(1) -4 <C(10) 108+V(1) 01
12 52+6*V(1) -6 <A(10) 109+V(1) 01
13 55+6*V(1) -3 01 (11)A> 109+V(1) 01
14 58+6*V(1) -6 01 <C(10) 00 108+V(1) 01
15 60+6*V(1) -8 <F(10) 10 00 108+V(1) 01
<< Success! ==> defined new CTR 24 (PPA)
8072306838236305 4858242[17]1787829 -5215952110860413 <F(10) 10 00 102607976055430228 01
== Executing PA-CTR 7, V(1)=2607976055430225, V(2)=0, repcount=1303988027715113, factor=5/2
21112187115387435 3036401[18]8276963 -130398[4]7151091 <F(10) 106519940138575566 00 102 01
== Executing PPA-CTR 8 (once), V(1)=6519940138575565
21112187115387457 3036401[18]1183855 -130398[4]7151107 <A(01) 01 00 016519940138575574 00 11
== Executing PA-CTR 2, V(1)=6519940138575571, V(2)=0, repcount=3259970069287786, factor=5/2
50451917738977531 1897750[19]6529873 -325997[4]2877823 <A(01) 0116299850346438931 00 012 00 11
== Executing PPA-CTR 3 (once), V(1)=16299850346438930
50451917738977551 1897750[19]3797143 -325997[4]2877837 <F(10) 10 00 1016299850346438939 01 11
== Executing PA-CTR 1, V(1)=16299850346438936, V(2)=0, repcount=8149925173219469, factor=5/2
1319511[4]1172241 1186094[20]7474345 -814992[4]2194651 <F(10) 1040749625866097346 00 10 01 11
== Executing PPA-CTR 9 (once), V(1)=40749625866097345
1319511[4]1172258 1186094[20]4058479 -814992[4]2194661 <A(01) 01 00 0140749625866097352 002 10
== Executing PA-CTR 2, V(1)=40749625866097349, V(2)=0, repcount=20374812933048675, factor=5/2
3153244[4]8610333 7413089[20]3012379 -203748[5]0486711 <A(01) 011018740[4]5243376 00 012 002 10
== Executing PPA-CTR 22 (once), V(1)=0, V(2)=1018740[4]5243375
3153244[4]8610353 7413089[20]5932989 -203748[5]0486725 <F(10) 10 00 101018740[4]5243384 01 00 10
== Executing PA-CTR 15, V(1)=1018740[4]5243381, V(2)=0, repcount=50937032332621691, factor=5/2
8246948[4]4827263 4633180[21]1724097 -509370[5]6216871 <F(10) 102546851[4]3108456 00 102 01 00 10
8246948[4]4827264 4633180[21]1724101 -509370[5]6216873 <C(01) 102546851[4]3108457 00 102 01 00 10
8246948[4]4827265 4633180[21]1724103 -509370[5]6216875 <A(10) 01 102546851[4]3108457 00 102 01 00 10
8246948[4]4827266 4633180[21]1724106 -509370[5]6216872 01 (11)A> 01 102546851[4]3108457 00 102 01 00 10
8246948[4]4827267 4633180[21]1724108 -509370[5]6216870 01 11 (11)D> 102546851[4]3108457 00 102 01 00 10
8246948[4]4827268 4633180[21]4157936 44 01 112546851[4]3108458 (11)D> 00 102 01 00 10
8246948[4]4827269 4633180[21]4157938 46 01 112546851[4]3108459 (11)B> 102 01 00 10
8246948[4]4827270 4633180[21]4157940 48 01 112546851[4]3108460 (11)A> 10 01 00 10
8246948[4]4827271 4633180[21]4157943 45 01 112546851[4]3108460 <C(10) 00 01 00 10
8246948[4]4827272 4633180[21]0374863 -509370[5]6216875 01 <C(10) 102546851[4]3108460 00 01 00 10
8246948[4]4827273 4633180[21]0374865 -509370[5]6216877 <F(10) 102546851[4]3108461 00 01 00 10
8246948[4]4827274 4633180[21]0374869 -509370[5]6216879 <C(01) 102546851[4]3108462 00 01 00 10
8246948[4]4827275 4633180[21]0374871 -509370[5]6216881 <A(10) 01 102546851[4]3108462 00 01 00 10
8246948[4]4827276 4633180[21]0374874 -509370[5]6216878 01 (11)A> 01 102546851[4]3108462 00 01 00 10
8246948[4]4827277 4633180[21]0374876 -509370[5]6216876 01 11 (11)D> 102546851[4]3108462 00 01 00 10
8246948[4]4827278 4633180[21]2808724 48 01 112546851[4]3108463 (11)D> 00 01 00 10
8246948[4]4827279 4633180[21]2808726 50 01 112546851[4]3108464 (11)B> 01 00 10
8246948[4]4827280 4633180[21]2808729 47 01 112546851[4]3108464 <E(00) 11 00 10
8246948[4]4827281 4633180[21]2808731 45 01 112546851[4]3108463 <E(01) 00 11 00 10
8246948[4]4827282 4633180[21]9025657 -509370[5]6216881 01 <E(01) 012546851[4]3108463 00 11 00 10
8246948[4]4827283 4633180[21]9025659 -509370[5]6216883 <B(01) 012546851[4]3108464 00 11 00 10
8246948[4]4827284 4633180[21]9025667 -509370[5]6216885 <E(01) 00 012546851[4]3108464 00 11 00 10
8246948[4]4827285 4633180[21]9025669 -509370[5]6216887 <A(01) 01 00 012546851[4]3108464 00 11 00 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <F(10) 101+V(1) 00 102 01 [*]* [*]*
1 4 -2 <C(01) 102+V(1) 00 102 01 [*]* [*]*
2 6 -4 <A(10) 01 102+V(1) 00 102 01 [*]* [*]*
3 9 -1 01 (11)A> 01 102+V(1) 00 102 01 [*]* [*]*
4 11 1 01 11 (11)D> 102+V(1) 00 102 01 [*]* [*]*
5 19+4*V(1) 5+2*V(1) 01 113+V(1) (11)D> 00 102 01 [*]* [*]*
6 21+4*V(1) 7+2*V(1) 01 114+V(1) (11)B> 102 01 [*]* [*]*
7 23+4*V(1) 9+2*V(1) 01 115+V(1) (11)A> 10 01 [*]* [*]*
8 26+4*V(1) 6+2*V(1) 01 115+V(1) <C(10) 00 01 [*]* [*]*
9 36+6*V(1) -4 01 <C(10) 105+V(1) 00 01 [*]* [*]*
10 38+6*V(1) -6 <F(10) 106+V(1) 00 01 [*]* [*]*
11 42+6*V(1) -8 <C(01) 107+V(1) 00 01 [*]* [*]*
12 44+6*V(1) -10 <A(10) 01 107+V(1) 00 01 [*]* [*]*
13 47+6*V(1) -7 01 (11)A> 01 107+V(1) 00 01 [*]* [*]*
14 49+6*V(1) -5 01 11 (11)D> 107+V(1) 00 01 [*]* [*]*
15 77+10*V(1) 9+2*V(1) 01 118+V(1) (11)D> 00 01 [*]* [*]*
16 79+10*V(1) 11+2*V(1) 01 119+V(1) (11)B> 01 [*]* [*]*
17 82+10*V(1) 8+2*V(1) 01 119+V(1) <E(00) 11 [*]* [*]*
18 84+10*V(1) 6+2*V(1) 01 118+V(1) <E(01) 00 11 [*]* [*]*
19 100+12*V(1) -10 01 <E(01) 018+V(1) 00 11 [*]* [*]*
20 102+12*V(1) -12 <B(01) 019+V(1) 00 11 [*]* [*]*
21 110+12*V(1) -14 <E(01) 00 019+V(1) 00 11 [*]* [*]*
22 112+12*V(1) -16 <A(01) 01 00 019+V(1) 00 11 [*]* [*]*
<< Success! ==> defined new CTR 25 (PPA)
8246948[4]4827285 4633180[21]9025669 -509370[5]6216887 <A(01) 01 00 012546851[4]3108464 00 11 00 10
== Executing PA-CTR 18, V(1)=2546851[4]3108461, V(2)=0, repcount=1273425[4]1554231, factor=5/2
1970778[5]8815364 2895738[22]4793397 -127342[6]5542273 <A(01) 016367129[4]7771156 00 012 00 11 00 10
1970778[5]8815365 2895738[22]4793401 -127342[6]5542275 <B(00) 11 016367129[4]7771156 00 012 00 11 00 10
1970778[5]8815366 2895738[22]4793406 -127342[6]5542272 11 (11)B> 11 016367129[4]7771156 00 012 00 11 00 10
1970778[5]8815367 2895738[22]4793408 -127342[6]5542270 112 (10)B> 016367129[4]7771156 00 012 00 11 00 10
1970778[5]8815368 2895738[22]5878032 42 116367129[4]7771158 (10)B> 00 012 00 11 00 10
1970778[5]8815369 2895738[22]5878036 44 116367129[4]7771159 (11)A> 012 00 11 00 10
1970778[5]8815370 2895738[22]5878038 46 116367129[4]7771160 (11)D> 01 00 11 00 10
1970778[5]8815371 2895738[22]5878043 43 116367129[4]7771160 <E(01) 002 11 00 10
1970778[5]8815372 2895738[22]1420363 -127342[6]5542277 <E(01) 016367129[4]7771160 002 11 00 10
1970778[5]8815373 2895738[22]1420365 -127342[6]5542279 <A(01) 016367129[4]7771161 002 11 00 10
1970778[5]8815374 2895738[22]1420369 -127342[6]5542281 <B(00) 11 016367129[4]7771161 002 11 00 10
1970778[5]8815375 2895738[22]1420374 -127342[6]5542278 11 (11)B> 11 016367129[4]7771161 002 11 00 10
1970778[5]8815376 2895738[22]1420376 -127342[6]5542276 112 (10)B> 016367129[4]7771161 002 11 00 10
1970778[5]8815377 2895738[22]2505020 46 116367129[4]7771163 (10)B> 002 11 00 10
1970778[5]8815378 2895738[22]2505024 48 116367129[4]7771164 (11)A> 00 11 00 10
1970778[5]8815379 2895738[22]2505029 45 116367129[4]7771164 <C(10) 01 11 00 10
1970778[5]8815380 2895738[22]8047357 -127342[6]5542283 <C(10) 106367129[4]7771164 01 11 00 10
1970778[5]8815381 2895738[22]8047359 -127342[6]5542285 <A(10) 106367129[4]7771165 01 11 00 10
1970778[5]8815382 2895738[22]8047362 -127342[6]5542282 01 (11)A> 106367129[4]7771165 01 11 00 10
1970778[5]8815383 2895738[22]8047365 -127342[6]5542285 01 <C(10) 00 106367129[4]7771164 01 11 00 10
1970778[5]8815384 2895738[22]8047367 -127342[6]5542287 <F(10) 10 00 106367129[4]7771164 01 11 00 10
1970778[5]8815385 2895738[22]8047371 -127342[6]5542289 <C(01) 102 00 106367129[4]7771164 01 11 00 10
1970778[5]8815386 2895738[22]8047373 -127342[6]5542291 <A(10) 01 102 00 106367129[4]7771164 01 11 00 10
1970778[5]8815387 2895738[22]8047376 -127342[6]5542288 01 (11)A> 01 102 00 106367129[4]7771164 01 11 00 10
1970778[5]8815388 2895738[22]8047378 -127342[6]5542286 01 11 (11)D> 102 00 106367129[4]7771164 01 11 00 10
1970778[5]8815389 2895738[22]8047386 -127342[6]5542282 01 113 (11)D> 00 106367129[4]7771164 01 11 00 10
1970778[5]8815390 2895738[22]8047388 -127342[6]5542280 01 114 (11)B> 106367129[4]7771164 01 11 00 10
1970778[5]8815391 2895738[22]8047390 -127342[6]5542278 01 115 (11)A> 106367129[4]7771163 01 11 00 10
1970778[5]8815392 2895738[22]8047393 -127342[6]5542281 01 115 <C(10) 00 106367129[4]7771162 01 11 00 10
1970778[5]8815393 2895738[22]8047403 -127342[6]5542291 01 <C(10) 105 00 106367129[4]7771162 01 11 00 10
1970778[5]8815394 2895738[22]8047405 -127342[6]5542293 <F(10) 106 00 106367129[4]7771162 01 11 00 10
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 <F(10) 101+V(2) 00 103+V(1) [*]* [*]* [*]* [*]*
1 4 -2 <C(01) 102+V(2) 00 103+V(1) [*]* [*]* [*]* [*]*
2 6 -4 <A(10) 01 102+V(2) 00 103+V(1) [*]* [*]* [*]* [*]*
3 9 -1 01 (11)A> 01 102+V(2) 00 103+V(1) [*]* [*]* [*]* [*]*
4 11 1 01 11 (11)D> 102+V(2) 00 103+V(1) [*]* [*]* [*]* [*]*
5 19+4*V(2) 5+2*V(2) 01 113+V(2) (11)D> 00 103+V(1) [*]* [*]* [*]* [*]*
6 21+4*V(2) 7+2*V(2) 01 114+V(2) (11)B> 103+V(1) [*]* [*]* [*]* [*]*
7 23+4*V(2) 9+2*V(2) 01 115+V(2) (11)A> 102+V(1) [*]* [*]* [*]* [*]*
8 26+4*V(2) 6+2*V(2) 01 115+V(2) <C(10) 00 101+V(1) [*]* [*]* [*]* [*]*
9 36+6*V(2) -4 01 <C(10) 105+V(2) 00 101+V(1) [*]* [*]* [*]* [*]*
10 38+6*V(2) -6 <F(10) 106+V(2) 00 101+V(1) [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 26 (PA)
1970778[5]8815394 2895738[22]8047405 -127342[6]5542293 <F(10) 106 00 106367129[4]7771162 01 11 00 10
== Executing PA-CTR 26, V(1)=6367129[4]7771159, V(2)=5, repcount=3183564[4]8885580, factor=5/2
5154342[5]7671194 1809836[23]8029145 -318356[6]8855773 <F(10) 101591782[5]4427906 00 102 01 11 00 10
5154342[5]7671195 1809836[23]8029149 -318356[6]8855775 <C(01) 101591782[5]4427907 00 102 01 11 00 10
5154342[5]7671196 1809836[23]8029151 -318356[6]8855777 <A(10) 01 101591782[5]4427907 00 102 01 11 00 10
5154342[5]7671197 1809836[23]8029154 -318356[6]8855774 01 (11)A> 01 101591782[5]4427907 00 102 01 11 00 10
5154342[5]7671198 1809836[23]8029156 -318356[6]8855772 01 11 (11)D> 101591782[5]4427907 00 102 01 11 00 10
5154342[5]7671199 1809836[23]5740784 42 01 111591782[5]4427908 (11)D> 00 102 01 11 00 10
5154342[5]7671200 1809836[23]5740786 44 01 111591782[5]4427909 (11)B> 102 01 11 00 10
5154342[5]7671201 1809836[23]5740788 46 01 111591782[5]4427910 (11)A> 10 01 11 00 10
5154342[5]7671202 1809836[23]5740791 43 01 111591782[5]4427910 <C(10) 00 01 11 00 10
5154342[5]7671203 1809836[23]4596611 -318356[6]8855777 01 <C(10) 101591782[5]4427910 00 01 11 00 10
5154342[5]7671204 1809836[23]4596613 -318356[6]8855779 <F(10) 101591782[5]4427911 00 01 11 00 10
5154342[5]7671205 1809836[23]4596617 -318356[6]8855781 <C(01) 101591782[5]4427912 00 01 11 00 10
5154342[5]7671206 1809836[23]4596619 -318356[6]8855783 <A(10) 01 101591782[5]4427912 00 01 11 00 10
5154342[5]7671207 1809836[23]4596622 -318356[6]8855780 01 (11)A> 01 101591782[5]4427912 00 01 11 00 10
5154342[5]7671208 1809836[23]4596624 -318356[6]8855778 01 11 (11)D> 101591782[5]4427912 00 01 11 00 10
5154342[5]7671209 1809836[23]2308272 46 01 111591782[5]4427913 (11)D> 00 01 11 00 10
5154342[5]7671210 1809836[23]2308274 48 01 111591782[5]4427914 (11)B> 01 11 00 10
5154342[5]7671211 1809836[23]2308277 45 01 111591782[5]4427914 <E(00) 112 00 10
5154342[5]7671212 1809836[23]2308279 43 01 111591782[5]4427913 <E(01) 00 112 00 10
5154342[5]7671213 1809836[23]1164105 -318356[6]8855783 01 <E(01) 011591782[5]4427913 00 112 00 10
5154342[5]7671214 1809836[23]1164107 -318356[6]8855785 <B(01) 011591782[5]4427914 00 112 00 10
5154342[5]7671215 1809836[23]1164115 -318356[6]8855787 <E(01) 00 011591782[5]4427914 00 112 00 10
5154342[5]7671216 1809836[23]1164117 -318356[6]8855789 <A(01) 01 00 011591782[5]4427914 00 112 00 10
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 <F(10) 101+V(2) 00 102 01 111+V(1) [*]* [*]*
1 4 -2 <C(01) 102+V(2) 00 102 01 111+V(1) [*]* [*]*
2 6 -4 <A(10) 01 102+V(2) 00 102 01 111+V(1) [*]* [*]*
3 9 -1 01 (11)A> 01 102+V(2) 00 102 01 111+V(1) [*]* [*]*
4 11 1 01 11 (11)D> 102+V(2) 00 102 01 111+V(1) [*]* [*]*
5 19+4*V(2) 5+2*V(2) 01 113+V(2) (11)D> 00 102 01 111+V(1) [*]* [*]*
6 21+4*V(2) 7+2*V(2) 01 114+V(2) (11)B> 102 01 111+V(1) [*]* [*]*
7 23+4*V(2) 9+2*V(2) 01 115+V(2) (11)A> 10 01 111+V(1) [*]* [*]*
8 26+4*V(2) 6+2*V(2) 01 115+V(2) <C(10) 00 01 111+V(1) [*]* [*]*
9 36+6*V(2) -4 01 <C(10) 105+V(2) 00 01 111+V(1) [*]* [*]*
10 38+6*V(2) -6 <F(10) 106+V(2) 00 01 111+V(1) [*]* [*]*
11 42+6*V(2) -8 <C(01) 107+V(2) 00 01 111+V(1) [*]* [*]*
12 44+6*V(2) -10 <A(10) 01 107+V(2) 00 01 111+V(1) [*]* [*]*
13 47+6*V(2) -7 01 (11)A> 01 107+V(2) 00 01 111+V(1) [*]* [*]*
14 49+6*V(2) -5 01 11 (11)D> 107+V(2) 00 01 111+V(1) [*]* [*]*
15 77+10*V(2) 9+2*V(2) 01 118+V(2) (11)D> 00 01 111+V(1) [*]* [*]*
16 79+10*V(2) 11+2*V(2) 01 119+V(2) (11)B> 01 111+V(1) [*]* [*]*
17 82+10*V(2) 8+2*V(2) 01 119+V(2) <E(00) 112+V(1) [*]* [*]*
18 84+10*V(2) 6+2*V(2) 01 118+V(2) <E(01) 00 112+V(1) [*]* [*]*
19 100+12*V(2) -10 01 <E(01) 018+V(2) 00 112+V(1) [*]* [*]*
20 102+12*V(2) -12 <B(01) 019+V(2) 00 112+V(1) [*]* [*]*
21 110+12*V(2) -14 <E(01) 00 019+V(2) 00 112+V(1) [*]* [*]*
22 112+12*V(2) -16 <A(01) 01 00 019+V(2) 00 112+V(1) [*]* [*]*
<< Success! ==> defined new CTR 27 (PPA)
5154342[5]7671216 1809836[23]1164117 -318356[6]8855789 <A(01) 01 00 011591782[5]4427914 00 112 00 10
== Executing PA-CTR 18, V(1)=1591782[5]4427911, V(2)=0, repcount=7958911[4]7213956, factor=5/2
1231736[6]2596820 1131147[24]4634145 -795891[6]2139525 <A(01) 013979455[5]6069781 00 012 00 112 00 10
1231736[6]2596821 1131147[24]4634149 -795891[6]2139527 <B(00) 11 013979455[5]6069781 00 012 00 112 00 10
1231736[6]2596822 1131147[24]4634154 -795891[6]2139524 11 (11)B> 11 013979455[5]6069781 00 012 00 112 00 10
1231736[6]2596823 1131147[24]4634156 -795891[6]2139522 112 (10)B> 013979455[5]6069781 00 012 00 112 00 10
1231736[6]2596824 1131147[24]8913280 40 113979455[5]6069783 (10)B> 00 012 00 112 00 10
1231736[6]2596825 1131147[24]8913284 42 113979455[5]6069784 (11)A> 012 00 112 00 10
1231736[6]2596826 1131147[24]8913286 44 113979455[5]6069785 (11)D> 01 00 112 00 10
1231736[6]2596827 1131147[24]8913291 41 113979455[5]6069785 <E(01) 002 112 00 10
1231736[6]2596828 1131147[24]1052861 -795891[6]2139529 <E(01) 013979455[5]6069785 002 112 00 10
1231736[6]2596829 1131147[24]1052863 -795891[6]2139531 <A(01) 013979455[5]6069786 002 112 00 10
1231736[6]2596830 1131147[24]1052867 -795891[6]2139533 <B(00) 11 013979455[5]6069786 002 112 00 10
1231736[6]2596831 1131147[24]1052872 -795891[6]2139530 11 (11)B> 11 013979455[5]6069786 002 112 00 10
1231736[6]2596832 1131147[24]1052874 -795891[6]2139528 112 (10)B> 013979455[5]6069786 002 112 00 10
1231736[6]2596833 1131147[24]5332018 44 113979455[5]6069788 (10)B> 002 112 00 10
1231736[6]2596834 1131147[24]5332022 46 113979455[5]6069789 (11)A> 00 112 00 10
1231736[6]2596835 1131147[24]5332027 43 113979455[5]6069789 <C(10) 01 112 00 10
1231736[6]2596836 1131147[24]7471605 -795891[6]2139535 <C(10) 103979455[5]6069789 01 112 00 10
1231736[6]2596837 1131147[24]7471607 -795891[6]2139537 <A(10) 103979455[5]6069790 01 112 00 10
1231736[6]2596838 1131147[24]7471610 -795891[6]2139534 01 (11)A> 103979455[5]6069790 01 112 00 10
1231736[6]2596839 1131147[24]7471613 -795891[6]2139537 01 <C(10) 00 103979455[5]6069789 01 112 00 10
1231736[6]2596840 1131147[24]7471615 -795891[6]2139539 <F(10) 10 00 103979455[5]6069789 01 112 00 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 <A(01) 011+V(1) 00 012 00 [*]* [*]* [*]*
1 4 -2 <B(00) 11 011+V(1) 00 012 00 [*]* [*]* [*]*
2 9 1 11 (11)B> 11 011+V(1) 00 012 00 [*]* [*]* [*]*
3 11 3 112 (10)B> 011+V(1) 00 012 00 [*]* [*]* [*]*
4 15+4*V(1) 5+2*V(1) 113+V(1) (10)B> 00 012 00 [*]* [*]* [*]*
5 19+4*V(1) 7+2*V(1) 114+V(1) (11)A> 012 00 [*]* [*]* [*]*
6 21+4*V(1) 9+2*V(1) 115+V(1) (11)D> 01 00 [*]* [*]* [*]*
7 26+4*V(1) 6+2*V(1) 115+V(1) <E(01) 002 [*]* [*]* [*]*
8 36+6*V(1) -4 <E(01) 015+V(1) 002 [*]* [*]* [*]*
9 38+6*V(1) -6 <A(01) 016+V(1) 002 [*]* [*]* [*]*
10 42+6*V(1) -8 <B(00) 11 016+V(1) 002 [*]* [*]* [*]*
11 47+6*V(1) -5 11 (11)B> 11 016+V(1) 002 [*]* [*]* [*]*
12 49+6*V(1) -3 112 (10)B> 016+V(1) 002 [*]* [*]* [*]*
13 73+10*V(1) 9+2*V(1) 118+V(1) (10)B> 002 [*]* [*]* [*]*
14 77+10*V(1) 11+2*V(1) 119+V(1) (11)A> 00 [*]* [*]* [*]*
15 82+10*V(1) 8+2*V(1) 119+V(1) <C(10) 01 [*]* [*]* [*]*
16 100+12*V(1) -10 <C(10) 109+V(1) 01 [*]* [*]* [*]*
17 102+12*V(1) -12 <A(10) 1010+V(1) 01 [*]* [*]* [*]*
18 105+12*V(1) -9 01 (11)A> 1010+V(1) 01 [*]* [*]* [*]*
19 108+12*V(1) -12 01 <C(10) 00 109+V(1) 01 [*]* [*]* [*]*
20 110+12*V(1) -14 <F(10) 10 00 109+V(1) 01 [*]* [*]* [*]*
<< Success! ==> defined new CTR 28 (PPA)
1231736[6]2596840 1131147[24]7471615 -795891[6]2139539 <F(10) 10 00 103979455[5]6069789 01 112 00 10
== Executing PA-CTR 26, V(1)=3979455[5]6069786, V(2)=0, repcount=1989727[5]3034894, factor=5/2
3221464[6]2945780 7069672[24]1142717 -198972[7]0348903 <F(10) 109948639[5]5174471 00 10 01 112 00 10
3221464[6]2945781 7069672[24]1142721 -198972[7]0348905 <C(01) 109948639[5]5174472 00 10 01 112 00 10
3221464[6]2945782 7069672[24]1142723 -198972[7]0348907 <A(10) 01 109948639[5]5174472 00 10 01 112 00 10
3221464[6]2945783 7069672[24]1142726 -198972[7]0348904 01 (11)A> 01 109948639[5]5174472 00 10 01 112 00 10
3221464[6]2945784 7069672[24]1142728 -198972[7]0348902 01 11 (11)D> 109948639[5]5174472 00 10 01 112 00 10
3221464[6]2945785 7069672[24]1840616 42 01 119948639[5]5174473 (11)D> 00 10 01 112 00 10
3221464[6]2945786 7069672[24]1840618 44 01 119948639[5]5174474 (11)B> 10 01 112 00 10
3221464[6]2945787 7069672[24]1840620 46 01 119948639[5]5174475 (11)A> 01 112 00 10
3221464[6]2945788 7069672[24]1840622 48 01 119948639[5]5174476 (11)D> 112 00 10
3221464[6]2945789 7069672[24]1840624 50 01 119948639[5]5174477 (01)D> 11 00 10
3221464[6]2945790 7069672[24]1840626 52 01 119948639[5]5174477 01 (01)D> 00 10
3221464[6]2945791 7069672[24]1840628 54 01 119948639[5]5174477 012 (11)B> 10
3221464[6]2945792 7069672[24]1840630 56 01 119948639[5]5174477 012 11 (11)A>
3221464[6]2945793 7069672[24]1840635 53 01 119948639[5]5174477 012 11 <C(10) 01
3221464[6]2945794 7069672[24]1840637 51 01 119948639[5]5174477 012 <C(10) 10 01
3221464[6]2945795 7069672[24]1840639 49 01 119948639[5]5174477 01 <F(10) 102 01
3221464[6]2945796 7069672[24]1840640 50 01 119948639[5]5174477 01 Z> 10 102 01 [stop]
Lines: 703
Top steps: 702
Macro steps: 32214640984172945796
Basic steps: 70696728920379305834526949238681840640
Tape index: 50
ones: 19897278254930348960
log10(ones ): 19.299
log10(steps ): 37.849
Run state: stop
Some long numbers above are shortened: #(omitted digits) shown in "[]".
Input to awk program:
gohalt 1
L 40
5T B1R C0L A1L D1R B0L E0L A1R B0R F1L C1L A0L Z1R : >1.9*10^19 >7.0*10^37
T 6-state TM #j from MaBu-List
M 750
pref sim
machv mbL6_j just simple
machv mbL6_j-r with repetitions reduced
machv mbL6_j-1 with tape symbol exponents
machv mbL6_j-m as 2-bck-macro machine
machv mbL6_j-a as 2-bck-macro machine with pure additive config-TRs
iam mbL6_j-a
mtype 2 0
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:10:59 CEST 2010
edate Tue Jul 6 22:11:01 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:10:59 CEST 2010