Comment: This TM produces 2,537,699,363,594,175,843,063 ones in >5.3*10^42 steps.
| State | on 0 |
on 1 |
on 0 | on 1 | ||||
|---|---|---|---|---|---|---|---|---|
| Move | Goto | Move | Goto | |||||
| A | B1R | C0R | 1 | right | B | 0 | right | C |
| B | A0L | D0R | 0 | left | A | 0 | right | D |
| C | D1R | H1R | 1 | right | D | 1 | right | H |
| D | E1L | D0L | 1 | left | E | 0 | left | D |
| E | F1R | B1L | 1 | right | F | 1 | left | B |
| F | A1R | E1R | 1 | right | A | 1 | right | E |
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 4 2 (01)D>
2 7 -1 <A(01) 10
3 18 2 11 (11)A> 10
4 20 4 112 (01)D>
5 23 1 112 <A(01) 10
6 29 -1 11 <B(11) 00 10
7 33 -3 <B(11) 01 00 10
8 41 -5 <E(10) 012 00 10
9 44 -2 01 (11)F> 012 00 10
10 46 0 01 11 (10)C> 01 00 10
11 51 -3 01 11 <B(11) 002 10
12 55 -5 01 <B(11) 01 002 10
13 62 -2 11 (11)E> 01 002 10
14 64 0 112 (11)E> 002 10
15 66 2 113 (11)A> 00 10
16 70 4 114 (01)D> 10
17 73 1 114 <E(10)
18 89 -7 <E(10) 104
19 92 -4 01 (11)F> 104
20 100 4 01 114 (11)F>
21 102 6 01 115 (11)B>
22 113 3 01 115 <E(10) 01
23 133 -7 01 <E(10) 105 01
24 135 -9 <A(01) 106 01
25 146 -6 11 (11)A> 106 01
26 148 -4 112 (01)D> 105 01
27 151 -7 112 <E(10) 00 104 01
28 159 -11 <E(10) 102 00 104 01
29 162 -8 01 (11)F> 102 00 104 01
30 166 -4 01 112 (11)F> 00 104 01
31 168 -2 01 113 (11)B> 104 01
32 172 0 01 114 (11)E> 103 01
33 177 -3 01 114 <B(11) 00 102 01
34 193 -11 01 <B(11) 014 00 102 01
35 200 -8 11 (11)E> 014 00 102 01
36 208 0 115 (11)E> 00 102 01
37 210 2 116 (11)A> 102 01
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 111+V(1) (11)A> 105+V(2) [*]*
1 2 2 112+V(1) (01)D> 104+V(2) [*]*
2 5 -1 112+V(1) <E(10) 00 103+V(2) [*]*
3 13+4*V(1) -5+-2*V(1) <E(10) 102+V(1) 00 103+V(2) [*]*
4 16+4*V(1) -2+-2*V(1) 01 (11)F> 102+V(1) 00 103+V(2) [*]*
5 20+6*V(1) 2 01 112+V(1) (11)F> 00 103+V(2) [*]*
6 22+6*V(1) 4 01 113+V(1) (11)B> 103+V(2) [*]*
7 26+6*V(1) 6 01 114+V(1) (11)E> 102+V(2) [*]*
8 31+6*V(1) 3 01 114+V(1) <B(11) 00 101+V(2) [*]*
9 47+10*V(1) -5+-2*V(1) 01 <B(11) 014+V(1) 00 101+V(2) [*]*
10 54+10*V(1) -2+-2*V(1) 11 (11)E> 014+V(1) 00 101+V(2) [*]*
11 62+12*V(1) 6 115+V(1) (11)E> 00 101+V(2) [*]*
12 64+12*V(1) 8 116+V(1) (11)A> 101+V(2) [*]*
<< Success! ==> defined new CTR 1 (PA)
38 212 4 117 (01)D> 10 01
39 215 1 117 <E(10) 00 01
40 243 -13 <E(10) 107 00 01
41 246 -10 01 (11)F> 107 00 01
42 260 4 01 117 (11)F> 00 01
43 262 6 01 118 (11)B> 01
44 269 3 01 118 <B(11)
45 301 -13 01 <B(11) 018
46 308 -10 11 (11)E> 018
47 324 6 119 (11)E>
48 326 8 1110 (11)A>
49 330 10 1111 (01)D>
50 333 7 1111 <A(01) 10
51 339 5 1110 <B(11) 00 10
52 379 -15 <B(11) 0110 00 10
53 387 -17 <E(10) 0111 00 10
54 390 -14 01 (11)F> 0111 00 10
55 392 -12 01 11 (10)C> 0110 00 10
56 397 -15 01 11 <B(11) 00 019 00 10
57 401 -17 01 <B(11) 01 00 019 00 10
58 408 -14 11 (11)E> 01 00 019 00 10
59 410 -12 112 (11)E> 00 019 00 10
60 412 -10 113 (11)A> 019 00 10
61 414 -8 114 (10)D> 018 00 10
62 425 -11 114 <E(10) 10 017 00 10
63 441 -19 <E(10) 105 017 00 10
64 444 -16 01 (11)F> 105 017 00 10
65 454 -6 01 115 (11)F> 017 00 10
66 456 -4 01 116 (10)C> 016 00 10
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 01 111+V(1) (10)C> 015+V(2) [*]* [*]*
1 5 -3 01 111+V(1) <B(11) 00 014+V(2) [*]* [*]*
2 9+4*V(1) -5+-2*V(1) 01 <B(11) 011+V(1) 00 014+V(2) [*]* [*]*
3 16+4*V(1) -2+-2*V(1) 11 (11)E> 011+V(1) 00 014+V(2) [*]* [*]*
4 18+6*V(1) 0 112+V(1) (11)E> 00 014+V(2) [*]* [*]*
5 20+6*V(1) 2 113+V(1) (11)A> 014+V(2) [*]* [*]*
6 22+6*V(1) 4 114+V(1) (10)D> 013+V(2) [*]* [*]*
7 33+6*V(1) 1 114+V(1) <E(10) 10 012+V(2) [*]* [*]*
8 49+10*V(1) -7+-2*V(1) <E(10) 105+V(1) 012+V(2) [*]* [*]*
9 52+10*V(1) -4+-2*V(1) 01 (11)F> 105+V(1) 012+V(2) [*]* [*]*
10 62+12*V(1) 6 01 115+V(1) (11)F> 012+V(2) [*]* [*]*
11 64+12*V(1) 8 01 116+V(1) (10)C> 011+V(2) [*]* [*]*
<< Success! ==> defined new CTR 2 (PA)
66 456 -4 01 116 (10)C> 016 00 10
== Executing PA-CTR 2, V(1)=5, V(2)=1, repcount=1, factor=5/4
77 580 4 01 1111 (10)C> 012 00 10
78 585 1 01 1111 <B(11) 00 01 00 10
79 629 -21 01 <B(11) 0111 00 01 00 10
80 636 -18 11 (11)E> 0111 00 01 00 10
81 658 4 1112 (11)E> 00 01 00 10
82 660 6 1113 (11)A> 01 00 10
83 662 8 1114 (10)D> 00 10
84 666 10 1115 (11)F> 10
85 668 12 1116 (11)F>
86 670 14 1117 (11)B>
87 681 11 1117 <E(10) 01
88 749 -23 <E(10) 1017 01
89 752 -20 01 (11)F> 1017 01
90 786 14 01 1117 (11)F> 01
91 788 16 01 1118 (10)C>
92 797 13 01 1118 <E(10) 01
93 869 -23 01 <E(10) 1018 01
94 871 -25 <A(01) 1019 01
95 882 -22 11 (11)A> 1019 01
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 01 111+V(1) (10)C> 012 00 101+V(2)
1 5 -3 01 111+V(1) <B(11) 00 01 00 101+V(2)
2 9+4*V(1) -5+-2*V(1) 01 <B(11) 011+V(1) 00 01 00 101+V(2)
3 16+4*V(1) -2+-2*V(1) 11 (11)E> 011+V(1) 00 01 00 101+V(2)
4 18+6*V(1) 0 112+V(1) (11)E> 00 01 00 101+V(2)
5 20+6*V(1) 2 113+V(1) (11)A> 01 00 101+V(2)
6 22+6*V(1) 4 114+V(1) (10)D> 00 101+V(2)
7 26+6*V(1) 6 115+V(1) (11)F> 101+V(2)
8 28+6*V(1)+2*V(2) 8+2*V(2) 116+V(1)+V(2) (11)F>
9 30+6*V(1)+2*V(2) 10+2*V(2) 117+V(1)+V(2) (11)B>
10 41+6*V(1)+2*V(2) 7+2*V(2) 117+V(1)+V(2) <E(10) 01
11 69+10*V(1)+6*V(2) -7+-2*V(1) <E(10) 107+V(1)+V(2) 01
12 72+10*V(1)+6*V(2) -4+-2*V(1) 01 (11)F> 107+V(1)+V(2) 01
13 86+12*V(1)+8*V(2) 10+2*V(2) 01 117+V(1)+V(2) (11)F> 01
14 88+12*V(1)+8*V(2) 12+2*V(2) 01 118+V(1)+V(2) (10)C>
15 97+12*V(1)+8*V(2) 9+2*V(2) 01 118+V(1)+V(2) <E(10) 01
16 129+16*V(1)+12*V(2) -7+-2*V(1) 01 <E(10) 108+V(1)+V(2) 01
17 131+16*V(1)+12*V(2) -9+-2*V(1) <A(01) 109+V(1)+V(2) 01
18 142+16*V(1)+12*V(2) -6+-2*V(1) 11 (11)A> 109+V(1)+V(2) 01
<< Success! ==> defined new CTR 3 (PPA)
95 882 -22 11 (11)A> 1019 01
== Executing PA-CTR 1, V(1)=0, V(2)=14, repcount=4, factor=5/4
143 1498 10 1121 (11)A> 103 01
144 1500 12 1122 (01)D> 102 01
145 1503 9 1122 <E(10) 00 10 01
146 1591 -35 <E(10) 1022 00 10 01
147 1594 -32 01 (11)F> 1022 00 10 01
148 1638 12 01 1122 (11)F> 00 10 01
149 1640 14 01 1123 (11)B> 10 01
150 1644 16 01 1124 (11)E> 01
151 1646 18 01 1125 (11)E>
152 1648 20 01 1126 (11)A>
153 1652 22 01 1127 (01)D>
154 1655 19 01 1127 <A(01) 10
155 1661 17 01 1126 <B(11) 00 10
156 1765 -35 01 <B(11) 0126 00 10
157 1772 -32 11 (11)E> 0126 00 10
158 1824 20 1127 (11)E> 00 10
159 1826 22 1128 (11)A> 10
160 1828 24 1129 (01)D>
161 1831 21 1129 <A(01) 10
162 1837 19 1128 <B(11) 00 10
163 1949 -37 <B(11) 0128 00 10
164 1957 -39 <E(10) 0129 00 10
165 1960 -36 01 (11)F> 0129 00 10
166 1962 -34 01 11 (10)C> 0128 00 10
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 111+V(1) (11)A> 103 011+V(2)
1 2 2 112+V(1) (01)D> 102 011+V(2)
2 5 -1 112+V(1) <E(10) 00 10 011+V(2)
3 13+4*V(1) -5+-2*V(1) <E(10) 102+V(1) 00 10 011+V(2)
4 16+4*V(1) -2+-2*V(1) 01 (11)F> 102+V(1) 00 10 011+V(2)
5 20+6*V(1) 2 01 112+V(1) (11)F> 00 10 011+V(2)
6 22+6*V(1) 4 01 113+V(1) (11)B> 10 011+V(2)
7 26+6*V(1) 6 01 114+V(1) (11)E> 011+V(2)
8 28+6*V(1)+2*V(2) 8+2*V(2) 01 115+V(1)+V(2) (11)E>
9 30+6*V(1)+2*V(2) 10+2*V(2) 01 116+V(1)+V(2) (11)A>
10 34+6*V(1)+2*V(2) 12+2*V(2) 01 117+V(1)+V(2) (01)D>
11 37+6*V(1)+2*V(2) 9+2*V(2) 01 117+V(1)+V(2) <A(01) 10
12 43+6*V(1)+2*V(2) 7+2*V(2) 01 116+V(1)+V(2) <B(11) 00 10
13 67+10*V(1)+6*V(2) -5+-2*V(1) 01 <B(11) 016+V(1)+V(2) 00 10
14 74+10*V(1)+6*V(2) -2+-2*V(1) 11 (11)E> 016+V(1)+V(2) 00 10
15 86+12*V(1)+8*V(2) 10+2*V(2) 117+V(1)+V(2) (11)E> 00 10
16 88+12*V(1)+8*V(2) 12+2*V(2) 118+V(1)+V(2) (11)A> 10
17 90+12*V(1)+8*V(2) 14+2*V(2) 119+V(1)+V(2) (01)D>
18 93+12*V(1)+8*V(2) 11+2*V(2) 119+V(1)+V(2) <A(01) 10
19 99+12*V(1)+8*V(2) 9+2*V(2) 118+V(1)+V(2) <B(11) 00 10
20 131+16*V(1)+12*V(2) -7+-2*V(1) <B(11) 018+V(1)+V(2) 00 10
21 139+16*V(1)+12*V(2) -9+-2*V(1) <E(10) 019+V(1)+V(2) 00 10
22 142+16*V(1)+12*V(2) -6+-2*V(1) 01 (11)F> 019+V(1)+V(2) 00 10
23 144+16*V(1)+12*V(2) -4+-2*V(1) 01 11 (10)C> 018+V(1)+V(2) 00 10
<< Success! ==> defined new CTR 4 (PPA)
166 1962 -34 01 11 (10)C> 0128 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=23, repcount=6, factor=5/4
232 3246 14 01 1131 (10)C> 014 00 10
233 3251 11 01 1131 <B(11) 00 013 00 10
234 3375 -51 01 <B(11) 0131 00 013 00 10
235 3382 -48 11 (11)E> 0131 00 013 00 10
236 3444 14 1132 (11)E> 00 013 00 10
237 3446 16 1133 (11)A> 013 00 10
238 3448 18 1134 (10)D> 012 00 10
239 3459 15 1134 <E(10) 10 01 00 10
240 3595 -53 <E(10) 1035 01 00 10
241 3598 -50 01 (11)F> 1035 01 00 10
242 3668 20 01 1135 (11)F> 01 00 10
243 3670 22 01 1136 (10)C> 00 10
244 3679 19 01 1136 <E(10) 01 10
245 3823 -53 01 <E(10) 1036 01 10
246 3825 -55 <A(01) 1037 01 10
247 3836 -52 11 (11)A> 1037 01 10
248 3838 -50 112 (01)D> 1036 01 10
249 3841 -53 112 <E(10) 00 1035 01 10
250 3849 -57 <E(10) 102 00 1035 01 10
251 3852 -54 01 (11)F> 102 00 1035 01 10
252 3856 -50 01 112 (11)F> 00 1035 01 10
253 3858 -48 01 113 (11)B> 1035 01 10
254 3862 -46 01 114 (11)E> 1034 01 10
255 3867 -49 01 114 <B(11) 00 1033 01 10
256 3883 -57 01 <B(11) 014 00 1033 01 10
257 3890 -54 11 (11)E> 014 00 1033 01 10
258 3898 -46 115 (11)E> 00 1033 01 10
259 3900 -44 116 (11)A> 1033 01 10
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 111+V(1) (11)A> 105+V(2) [*]* [*]*
1 2 2 112+V(1) (01)D> 104+V(2) [*]* [*]*
2 5 -1 112+V(1) <E(10) 00 103+V(2) [*]* [*]*
3 13+4*V(1) -5+-2*V(1) <E(10) 102+V(1) 00 103+V(2) [*]* [*]*
4 16+4*V(1) -2+-2*V(1) 01 (11)F> 102+V(1) 00 103+V(2) [*]* [*]*
5 20+6*V(1) 2 01 112+V(1) (11)F> 00 103+V(2) [*]* [*]*
6 22+6*V(1) 4 01 113+V(1) (11)B> 103+V(2) [*]* [*]*
7 26+6*V(1) 6 01 114+V(1) (11)E> 102+V(2) [*]* [*]*
8 31+6*V(1) 3 01 114+V(1) <B(11) 00 101+V(2) [*]* [*]*
9 47+10*V(1) -5+-2*V(1) 01 <B(11) 014+V(1) 00 101+V(2) [*]* [*]*
10 54+10*V(1) -2+-2*V(1) 11 (11)E> 014+V(1) 00 101+V(2) [*]* [*]*
11 62+12*V(1) 6 115+V(1) (11)E> 00 101+V(2) [*]* [*]*
12 64+12*V(1) 8 116+V(1) (11)A> 101+V(2) [*]* [*]*
<< Success! ==> defined new CTR 5 (PA)
259 3900 -44 116 (11)A> 1033 01 10
== Executing PA-CTR 5, V(1)=5, V(2)=28, repcount=8, factor=5/4
355 6572 20 1146 (11)A> 10 01 10
356 6574 22 1147 (01)D> 01 10
357 6577 19 1147 <A(01) 11 10
358 6583 17 1146 <B(11) 00 11 10
359 6767 -75 <B(11) 0146 00 11 10
360 6775 -77 <E(10) 0147 00 11 10
361 6778 -74 01 (11)F> 0147 00 11 10
362 6780 -72 01 11 (10)C> 0146 00 11 10
363 6785 -75 01 11 <B(11) 00 0145 00 11 10
364 6789 -77 01 <B(11) 01 00 0145 00 11 10
365 6796 -74 11 (11)E> 01 00 0145 00 11 10
366 6798 -72 112 (11)E> 00 0145 00 11 10
367 6800 -70 113 (11)A> 0145 00 11 10
368 6802 -68 114 (10)D> 0144 00 11 10
369 6813 -71 114 <E(10) 10 0143 00 11 10
370 6829 -79 <E(10) 105 0143 00 11 10
371 6832 -76 01 (11)F> 105 0143 00 11 10
372 6842 -66 01 115 (11)F> 0143 00 11 10
373 6844 -64 01 116 (10)C> 0142 00 11 10
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 01 111+V(1) (10)C> 015+V(2) [*]* [*]* [*]*
1 5 -3 01 111+V(1) <B(11) 00 014+V(2) [*]* [*]* [*]*
2 9+4*V(1) -5+-2*V(1) 01 <B(11) 011+V(1) 00 014+V(2) [*]* [*]* [*]*
3 16+4*V(1) -2+-2*V(1) 11 (11)E> 011+V(1) 00 014+V(2) [*]* [*]* [*]*
4 18+6*V(1) 0 112+V(1) (11)E> 00 014+V(2) [*]* [*]* [*]*
5 20+6*V(1) 2 113+V(1) (11)A> 014+V(2) [*]* [*]* [*]*
6 22+6*V(1) 4 114+V(1) (10)D> 013+V(2) [*]* [*]* [*]*
7 33+6*V(1) 1 114+V(1) <E(10) 10 012+V(2) [*]* [*]* [*]*
8 49+10*V(1) -7+-2*V(1) <E(10) 105+V(1) 012+V(2) [*]* [*]* [*]*
9 52+10*V(1) -4+-2*V(1) 01 (11)F> 105+V(1) 012+V(2) [*]* [*]* [*]*
10 62+12*V(1) 6 01 115+V(1) (11)F> 012+V(2) [*]* [*]* [*]*
11 64+12*V(1) 8 01 116+V(1) (10)C> 011+V(2) [*]* [*]* [*]*
<< Success! ==> defined new CTR 6 (PA)
373 6844 -64 01 116 (10)C> 0142 00 11 10
== Executing PA-CTR 6, V(1)=5, V(2)=37, repcount=10, factor=5/4
483 10784 16 01 1156 (10)C> 012 00 11 10
484 10789 13 01 1156 <B(11) 00 01 00 11 10
485 11013 -99 01 <B(11) 0156 00 01 00 11 10
486 11020 -96 11 (11)E> 0156 00 01 00 11 10
487 11132 16 1157 (11)E> 00 01 00 11 10
488 11134 18 1158 (11)A> 01 00 11 10
489 11136 20 1159 (10)D> 00 11 10
490 11140 22 1160 (11)F> 11 10
491 11149 19 1160 <E(10) 102
492 11389 -101 <E(10) 1062
493 11392 -98 01 (11)F> 1062
494 11516 26 01 1162 (11)F>
495 11518 28 01 1163 (11)B>
496 11529 25 01 1163 <E(10) 01
497 11781 -101 01 <E(10) 1063 01
498 11783 -103 <A(01) 1064 01
499 11794 -100 11 (11)A> 1064 01
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 01 111+V(1) (10)C> 012 00 11 101+V(2)
1 5 -3 01 111+V(1) <B(11) 00 01 00 11 101+V(2)
2 9+4*V(1) -5+-2*V(1) 01 <B(11) 011+V(1) 00 01 00 11 101+V(2)
3 16+4*V(1) -2+-2*V(1) 11 (11)E> 011+V(1) 00 01 00 11 101+V(2)
4 18+6*V(1) 0 112+V(1) (11)E> 00 01 00 11 101+V(2)
5 20+6*V(1) 2 113+V(1) (11)A> 01 00 11 101+V(2)
6 22+6*V(1) 4 114+V(1) (10)D> 00 11 101+V(2)
7 26+6*V(1) 6 115+V(1) (11)F> 11 101+V(2)
8 35+6*V(1) 3 115+V(1) <E(10) 102+V(2)
9 55+10*V(1) -7+-2*V(1) <E(10) 107+V(1)+V(2)
10 58+10*V(1) -4+-2*V(1) 01 (11)F> 107+V(1)+V(2)
11 72+12*V(1)+2*V(2) 10+2*V(2) 01 117+V(1)+V(2) (11)F>
12 74+12*V(1)+2*V(2) 12+2*V(2) 01 118+V(1)+V(2) (11)B>
13 85+12*V(1)+2*V(2) 9+2*V(2) 01 118+V(1)+V(2) <E(10) 01
14 117+16*V(1)+6*V(2) -7+-2*V(1) 01 <E(10) 108+V(1)+V(2) 01
15 119+16*V(1)+6*V(2) -9+-2*V(1) <A(01) 109+V(1)+V(2) 01
16 130+16*V(1)+6*V(2) -6+-2*V(1) 11 (11)A> 109+V(1)+V(2) 01
<< Success! ==> defined new CTR 7 (PPA)
499 11794 -100 11 (11)A> 1064 01
== Executing PA-CTR 1, V(1)=0, V(2)=59, repcount=15, factor=5/4
679 19054 20 1176 (11)A> 104 01
680 19056 22 1177 (01)D> 103 01
681 19059 19 1177 <E(10) 00 102 01
682 19367 -135 <E(10) 1077 00 102 01
683 19370 -132 01 (11)F> 1077 00 102 01
684 19524 22 01 1177 (11)F> 00 102 01
685 19526 24 01 1178 (11)B> 102 01
686 19530 26 01 1179 (11)E> 10 01
687 19535 23 01 1179 <B(11) 00 01
688 19851 -135 01 <B(11) 0179 00 01
689 19858 -132 11 (11)E> 0179 00 01
690 20016 26 1180 (11)E> 00 01
691 20018 28 1181 (11)A> 01
692 20020 30 1182 (10)D>
693 20024 32 1183 (11)F>
694 20026 34 1184 (11)B>
695 20037 31 1184 <E(10) 01
696 20373 -137 <E(10) 1084 01
697 20376 -134 01 (11)F> 1084 01
698 20544 34 01 1184 (11)F> 01
699 20546 36 01 1185 (10)C>
700 20555 33 01 1185 <E(10) 01
701 20895 -137 01 <E(10) 1085 01
702 20897 -139 <A(01) 1086 01
703 20908 -136 11 (11)A> 1086 01
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 111+V(1) (11)A> 104 01
1 2 2 112+V(1) (01)D> 103 01
2 5 -1 112+V(1) <E(10) 00 102 01
3 13+4*V(1) -5+-2*V(1) <E(10) 102+V(1) 00 102 01
4 16+4*V(1) -2+-2*V(1) 01 (11)F> 102+V(1) 00 102 01
5 20+6*V(1) 2 01 112+V(1) (11)F> 00 102 01
6 22+6*V(1) 4 01 113+V(1) (11)B> 102 01
7 26+6*V(1) 6 01 114+V(1) (11)E> 10 01
8 31+6*V(1) 3 01 114+V(1) <B(11) 00 01
9 47+10*V(1) -5+-2*V(1) 01 <B(11) 014+V(1) 00 01
10 54+10*V(1) -2+-2*V(1) 11 (11)E> 014+V(1) 00 01
11 62+12*V(1) 6 115+V(1) (11)E> 00 01
12 64+12*V(1) 8 116+V(1) (11)A> 01
13 66+12*V(1) 10 117+V(1) (10)D>
14 70+12*V(1) 12 118+V(1) (11)F>
15 72+12*V(1) 14 119+V(1) (11)B>
16 83+12*V(1) 11 119+V(1) <E(10) 01
17 119+16*V(1) -7+-2*V(1) <E(10) 109+V(1) 01
18 122+16*V(1) -4+-2*V(1) 01 (11)F> 109+V(1) 01
19 140+18*V(1) 14 01 119+V(1) (11)F> 01
20 142+18*V(1) 16 01 1110+V(1) (10)C>
21 151+18*V(1) 13 01 1110+V(1) <E(10) 01
22 191+22*V(1) -7+-2*V(1) 01 <E(10) 1010+V(1) 01
23 193+22*V(1) -9+-2*V(1) <A(01) 1011+V(1) 01
24 204+22*V(1) -6+-2*V(1) 11 (11)A> 1011+V(1) 01
<< Success! ==> defined new CTR 8 (PPA)
703 20908 -136 11 (11)A> 1086 01
== Executing PA-CTR 1, V(1)=0, V(2)=81, repcount=21, factor=5/4
955 34852 32 11106 (11)A> 102 01
956 34854 34 11107 (01)D> 10 01
957 34857 31 11107 <E(10) 00 01
958 35285 -183 <E(10) 10107 00 01
959 35288 -180 01 (11)F> 10107 00 01
960 35502 34 01 11107 (11)F> 00 01
961 35504 36 01 11108 (11)B> 01
962 35511 33 01 11108 <B(11)
963 35943 -183 01 <B(11) 01108
964 35950 -180 11 (11)E> 01108
965 36166 36 11109 (11)E>
966 36168 38 11110 (11)A>
967 36172 40 11111 (01)D>
968 36175 37 11111 <A(01) 10
969 36181 35 11110 <B(11) 00 10
970 36621 -185 <B(11) 01110 00 10
971 36629 -187 <E(10) 01111 00 10
972 36632 -184 01 (11)F> 01111 00 10
973 36634 -182 01 11 (10)C> 01110 00 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 111+V(1) (11)A> 102 01
1 2 2 112+V(1) (01)D> 10 01
2 5 -1 112+V(1) <E(10) 00 01
3 13+4*V(1) -5+-2*V(1) <E(10) 102+V(1) 00 01
4 16+4*V(1) -2+-2*V(1) 01 (11)F> 102+V(1) 00 01
5 20+6*V(1) 2 01 112+V(1) (11)F> 00 01
6 22+6*V(1) 4 01 113+V(1) (11)B> 01
7 29+6*V(1) 1 01 113+V(1) <B(11)
8 41+10*V(1) -5+-2*V(1) 01 <B(11) 013+V(1)
9 48+10*V(1) -2+-2*V(1) 11 (11)E> 013+V(1)
10 54+12*V(1) 4 114+V(1) (11)E>
11 56+12*V(1) 6 115+V(1) (11)A>
12 60+12*V(1) 8 116+V(1) (01)D>
13 63+12*V(1) 5 116+V(1) <A(01) 10
14 69+12*V(1) 3 115+V(1) <B(11) 00 10
15 89+16*V(1) -7+-2*V(1) <B(11) 015+V(1) 00 10
16 97+16*V(1) -9+-2*V(1) <E(10) 016+V(1) 00 10
17 100+16*V(1) -6+-2*V(1) 01 (11)F> 016+V(1) 00 10
18 102+16*V(1) -4+-2*V(1) 01 11 (10)C> 015+V(1) 00 10
<< Success! ==> defined new CTR 9 (PPA)
973 36634 -182 01 11 (10)C> 01110 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=105, repcount=27, factor=5/4
1270 59422 34 01 11136 (10)C> 012 00 10
== Executing PPA-CTR 3 (once), V(1)=135, V(2)=0
1288 61724 -242 11 (11)A> 10144 01
== Executing PA-CTR 1, V(1)=0, V(2)=139, repcount=35, factor=5/4
1708 99664 38 11176 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=175
1732 103718 -318 11 (11)A> 10186 01
== Executing PA-CTR 1, V(1)=0, V(2)=181, repcount=46, factor=5/4
2284 168762 50 11231 (11)A> 102 01
== Executing PPA-CTR 9 (once), V(1)=230
2302 172544 -414 01 11 (10)C> 01235 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=230, repcount=58, factor=5/4
2940 275436 50 01 11291 (10)C> 013 00 10
2941 275441 47 01 11291 <B(11) 00 012 00 10
2942 276605 -535 01 <B(11) 01291 00 012 00 10
2943 276612 -532 11 (11)E> 01291 00 012 00 10
2944 277194 50 11292 (11)E> 00 012 00 10
2945 277196 52 11293 (11)A> 012 00 10
2946 277198 54 11294 (10)D> 01 00 10
2947 277209 51 11294 <E(10) 10 00 10
2948 278385 -537 <E(10) 10295 00 10
2949 278388 -534 01 (11)F> 10295 00 10
2950 278978 56 01 11295 (11)F> 00 10
2951 278980 58 01 11296 (11)B> 10
2952 278984 60 01 11297 (11)E>
2953 278986 62 01 11298 (11)A>
2954 278990 64 01 11299 (01)D>
2955 278993 61 01 11299 <A(01) 10
2956 278999 59 01 11298 <B(11) 00 10
2957 280191 -537 01 <B(11) 01298 00 10
2958 280198 -534 11 (11)E> 01298 00 10
2959 280794 62 11299 (11)E> 00 10
2960 280796 64 11300 (11)A> 10
2961 280798 66 11301 (01)D>
2962 280801 63 11301 <A(01) 10
2963 280807 61 11300 <B(11) 00 10
2964 282007 -539 <B(11) 01300 00 10
2965 282015 -541 <E(10) 01301 00 10
2966 282018 -538 01 (11)F> 01301 00 10
2967 282020 -536 01 11 (10)C> 01300 00 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 111+V(1) (10)C> 013 00 10
1 5 -3 01 111+V(1) <B(11) 00 012 00 10
2 9+4*V(1) -5+-2*V(1) 01 <B(11) 011+V(1) 00 012 00 10
3 16+4*V(1) -2+-2*V(1) 11 (11)E> 011+V(1) 00 012 00 10
4 18+6*V(1) 0 112+V(1) (11)E> 00 012 00 10
5 20+6*V(1) 2 113+V(1) (11)A> 012 00 10
6 22+6*V(1) 4 114+V(1) (10)D> 01 00 10
7 33+6*V(1) 1 114+V(1) <E(10) 10 00 10
8 49+10*V(1) -7+-2*V(1) <E(10) 105+V(1) 00 10
9 52+10*V(1) -4+-2*V(1) 01 (11)F> 105+V(1) 00 10
10 62+12*V(1) 6 01 115+V(1) (11)F> 00 10
11 64+12*V(1) 8 01 116+V(1) (11)B> 10
12 68+12*V(1) 10 01 117+V(1) (11)E>
13 70+12*V(1) 12 01 118+V(1) (11)A>
14 74+12*V(1) 14 01 119+V(1) (01)D>
15 77+12*V(1) 11 01 119+V(1) <A(01) 10
16 83+12*V(1) 9 01 118+V(1) <B(11) 00 10
17 115+16*V(1) -7+-2*V(1) 01 <B(11) 018+V(1) 00 10
18 122+16*V(1) -4+-2*V(1) 11 (11)E> 018+V(1) 00 10
19 138+18*V(1) 12 119+V(1) (11)E> 00 10
20 140+18*V(1) 14 1110+V(1) (11)A> 10
21 142+18*V(1) 16 1111+V(1) (01)D>
22 145+18*V(1) 13 1111+V(1) <A(01) 10
23 151+18*V(1) 11 1110+V(1) <B(11) 00 10
24 191+22*V(1) -9+-2*V(1) <B(11) 0110+V(1) 00 10
25 199+22*V(1) -11+-2*V(1) <E(10) 0111+V(1) 00 10
26 202+22*V(1) -8+-2*V(1) 01 (11)F> 0111+V(1) 00 10
27 204+22*V(1) -6+-2*V(1) 01 11 (10)C> 0110+V(1) 00 10
<< Success! ==> defined new CTR 10 (PPA)
2967 282020 -536 01 11 (10)C> 01300 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=295, repcount=74, factor=5/4
3781 448816 56 01 11371 (10)C> 014 00 10
3782 448821 53 01 11371 <B(11) 00 013 00 10
3783 450305 -689 01 <B(11) 01371 00 013 00 10
3784 450312 -686 11 (11)E> 01371 00 013 00 10
3785 451054 56 11372 (11)E> 00 013 00 10
3786 451056 58 11373 (11)A> 013 00 10
3787 451058 60 11374 (10)D> 012 00 10
3788 451069 57 11374 <E(10) 10 01 00 10
3789 452565 -691 <E(10) 10375 01 00 10
3790 452568 -688 01 (11)F> 10375 01 00 10
3791 453318 62 01 11375 (11)F> 01 00 10
3792 453320 64 01 11376 (10)C> 00 10
3793 453329 61 01 11376 <E(10) 01 10
3794 454833 -691 01 <E(10) 10376 01 10
3795 454835 -693 <A(01) 10377 01 10
3796 454846 -690 11 (11)A> 10377 01 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 111+V(1) (10)C> 014 00 [*]*
1 5 -3 01 111+V(1) <B(11) 00 013 00 [*]*
2 9+4*V(1) -5+-2*V(1) 01 <B(11) 011+V(1) 00 013 00 [*]*
3 16+4*V(1) -2+-2*V(1) 11 (11)E> 011+V(1) 00 013 00 [*]*
4 18+6*V(1) 0 112+V(1) (11)E> 00 013 00 [*]*
5 20+6*V(1) 2 113+V(1) (11)A> 013 00 [*]*
6 22+6*V(1) 4 114+V(1) (10)D> 012 00 [*]*
7 33+6*V(1) 1 114+V(1) <E(10) 10 01 00 [*]*
8 49+10*V(1) -7+-2*V(1) <E(10) 105+V(1) 01 00 [*]*
9 52+10*V(1) -4+-2*V(1) 01 (11)F> 105+V(1) 01 00 [*]*
10 62+12*V(1) 6 01 115+V(1) (11)F> 01 00 [*]*
11 64+12*V(1) 8 01 116+V(1) (10)C> 00 [*]*
12 73+12*V(1) 5 01 116+V(1) <E(10) 01 [*]*
13 97+16*V(1) -7+-2*V(1) 01 <E(10) 106+V(1) 01 [*]*
14 99+16*V(1) -9+-2*V(1) <A(01) 107+V(1) 01 [*]*
15 110+16*V(1) -6+-2*V(1) 11 (11)A> 107+V(1) 01 [*]*
<< Success! ==> defined new CTR 11 (PPA)
3796 454846 -690 11 (11)A> 10377 01 10
== Executing PA-CTR 5, V(1)=0, V(2)=372, repcount=94, factor=5/4
4924 723122 62 11471 (11)A> 10 01 10
4925 723124 64 11472 (01)D> 01 10
4926 723127 61 11472 <A(01) 11 10
4927 723133 59 11471 <B(11) 00 11 10
4928 725017 -883 <B(11) 01471 00 11 10
4929 725025 -885 <E(10) 01472 00 11 10
4930 725028 -882 01 (11)F> 01472 00 11 10
4931 725030 -880 01 11 (10)C> 01471 00 11 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 115+V(1) (11)A> 10 01 [*]*
1 2 2 116+V(1) (01)D> 01 [*]*
2 5 -1 116+V(1) <A(01) 11 [*]*
3 11 -3 115+V(1) <B(11) 00 11 [*]*
4 31+4*V(1) -13+-2*V(1) <B(11) 015+V(1) 00 11 [*]*
5 39+4*V(1) -15+-2*V(1) <E(10) 016+V(1) 00 11 [*]*
6 42+4*V(1) -12+-2*V(1) 01 (11)F> 016+V(1) 00 11 [*]*
7 44+4*V(1) -10+-2*V(1) 01 11 (10)C> 015+V(1) 00 11 [*]*
<< Success! ==> defined new CTR 12 (PPA)
4931 725030 -880 01 11 (10)C> 01471 00 11 10
== Executing PA-CTR 6, V(1)=0, V(2)=466, repcount=117, factor=5/4
6218 1139678 56 01 11586 (10)C> 013 00 11 10
6219 1139683 53 01 11586 <B(11) 00 012 00 11 10
6220 1142027 -1119 01 <B(11) 01586 00 012 00 11 10
6221 1142034 -1116 11 (11)E> 01586 00 012 00 11 10
6222 1143206 56 11587 (11)E> 00 012 00 11 10
6223 1143208 58 11588 (11)A> 012 00 11 10
6224 1143210 60 11589 (10)D> 01 00 11 10
6225 1143221 57 11589 <E(10) 10 00 11 10
6226 1145577 -1121 <E(10) 10590 00 11 10
6227 1145580 -1118 01 (11)F> 10590 00 11 10
6228 1146760 62 01 11590 (11)F> 00 11 10
6229 1146762 64 01 11591 (11)B> 11 10
6230 1146769 61 01 11591 <E(10) 102
6231 1149133 -1121 01 <E(10) 10593
6232 1149135 -1123 <A(01) 10594
6233 1149146 -1120 11 (11)A> 10594
6234 1149148 -1118 112 (01)D> 10593
6235 1149151 -1121 112 <E(10) 00 10592
6236 1149159 -1125 <E(10) 102 00 10592
6237 1149162 -1122 01 (11)F> 102 00 10592
6238 1149166 -1118 01 112 (11)F> 00 10592
6239 1149168 -1116 01 113 (11)B> 10592
6240 1149172 -1114 01 114 (11)E> 10591
6241 1149177 -1117 01 114 <B(11) 00 10590
6242 1149193 -1125 01 <B(11) 014 00 10590
6243 1149200 -1122 11 (11)E> 014 00 10590
6244 1149208 -1114 115 (11)E> 00 10590
6245 1149210 -1112 116 (11)A> 10590
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 111+V(1) (11)A> 105+V(2)
1 2 2 112+V(1) (01)D> 104+V(2)
2 5 -1 112+V(1) <E(10) 00 103+V(2)
3 13+4*V(1) -5+-2*V(1) <E(10) 102+V(1) 00 103+V(2)
4 16+4*V(1) -2+-2*V(1) 01 (11)F> 102+V(1) 00 103+V(2)
5 20+6*V(1) 2 01 112+V(1) (11)F> 00 103+V(2)
6 22+6*V(1) 4 01 113+V(1) (11)B> 103+V(2)
7 26+6*V(1) 6 01 114+V(1) (11)E> 102+V(2)
8 31+6*V(1) 3 01 114+V(1) <B(11) 00 101+V(2)
9 47+10*V(1) -5+-2*V(1) 01 <B(11) 014+V(1) 00 101+V(2)
10 54+10*V(1) -2+-2*V(1) 11 (11)E> 014+V(1) 00 101+V(2)
11 62+12*V(1) 6 115+V(1) (11)E> 00 101+V(2)
12 64+12*V(1) 8 116+V(1) (11)A> 101+V(2)
<< Success! ==> defined new CTR 13 (PA)
6245 1149210 -1112 116 (11)A> 10590
== Executing PA-CTR 13, V(1)=5, V(2)=585, repcount=147, factor=5/4
8009 1811298 64 11741 (11)A> 102
8010 1811300 66 11742 (01)D> 10
8011 1811303 63 11742 <E(10)
8012 1814271 -1421 <E(10) 10742
8013 1814274 -1418 01 (11)F> 10742
8014 1815758 66 01 11742 (11)F>
8015 1815760 68 01 11743 (11)B>
8016 1815771 65 01 11743 <E(10) 01
8017 1818743 -1421 01 <E(10) 10743 01
8018 1818745 -1423 <A(01) 10744 01
8019 1818756 -1420 11 (11)A> 10744 01
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 112+V(1) (11)A> 102
1 2 2 113+V(1) (01)D> 10
2 5 -1 113+V(1) <E(10)
3 17+4*V(1) -7+-2*V(1) <E(10) 103+V(1)
4 20+4*V(1) -4+-2*V(1) 01 (11)F> 103+V(1)
5 26+6*V(1) 2 01 113+V(1) (11)F>
6 28+6*V(1) 4 01 114+V(1) (11)B>
7 39+6*V(1) 1 01 114+V(1) <E(10) 01
8 55+10*V(1) -7+-2*V(1) 01 <E(10) 104+V(1) 01
9 57+10*V(1) -9+-2*V(1) <A(01) 105+V(1) 01
10 68+10*V(1) -6+-2*V(1) 11 (11)A> 105+V(1) 01
<< Success! ==> defined new CTR 14 (PPA)
8019 1818756 -1420 11 (11)A> 10744 01
== Executing PA-CTR 1, V(1)=0, V(2)=739, repcount=185, factor=5/4
10239 2851796 60 11926 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=925
10263 2872350 -1796 11 (11)A> 10936 01
== Executing PA-CTR 1, V(1)=0, V(2)=931, repcount=233, factor=5/4
13059 4508942 68 111166 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=1165
13083 4534776 -2268 11 (11)A> 101176 01
== Executing PA-CTR 1, V(1)=0, V(2)=1171, repcount=293, factor=5/4
16599 7120208 76 111466 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=1465
16623 7152642 -2860 11 (11)A> 101476 01
== Executing PA-CTR 1, V(1)=0, V(2)=1471, repcount=368, factor=5/4
21039 11227874 84 111841 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=1840
21063 11268558 -3602 11 (11)A> 101851 01
== Executing PA-CTR 1, V(1)=0, V(2)=1846, repcount=462, factor=5/4
26607 17687586 94 112311 (11)A> 103 01
== Executing PPA-CTR 4 (once), V(1)=2310, V(2)=0
26630 17724690 -4530 01 11 (10)C> 012318 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=2313, repcount=579, factor=5/4
32999 27801606 102 01 112896 (10)C> 012 00 10
== Executing PPA-CTR 3 (once), V(1)=2895, V(2)=0
33017 27848068 -5694 11 (11)A> 102904 01
== Executing PA-CTR 1, V(1)=0, V(2)=2899, repcount=725, factor=5/4
41717 43641468 106 113626 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=3625
41741 43721422 -7150 11 (11)A> 103636 01
== Executing PA-CTR 1, V(1)=0, V(2)=3631, repcount=908, factor=5/4
52637 68486214 114 114541 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=4540
52661 68586298 -8972 11 (11)A> 104551 01
== Executing PA-CTR 1, V(1)=0, V(2)=4546, repcount=1137, factor=5/4
66305 107408026 124 115686 (11)A> 103 01
== Executing PPA-CTR 4 (once), V(1)=5685, V(2)=0
66328 107499130 -11250 01 11 (10)C> 015693 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=5688, repcount=1423, factor=5/4
81981 168295382 134 01 117116 (10)C> 01 00 10
81982 168295387 131 01 117116 <B(11) 002 10
81983 168323851 -14101 01 <B(11) 017116 002 10
81984 168323858 -14098 11 (11)E> 017116 002 10
81985 168338090 134 117117 (11)E> 002 10
81986 168338092 136 117118 (11)A> 00 10
81987 168338096 138 117119 (01)D> 10
81988 168338099 135 117119 <E(10)
81989 168366575 -14103 <E(10) 107119
81990 168366578 -14100 01 (11)F> 107119
81991 168380816 138 01 117119 (11)F>
81992 168380818 140 01 117120 (11)B>
81993 168380829 137 01 117120 <E(10) 01
81994 168409309 -14103 01 <E(10) 107120 01
81995 168409311 -14105 <A(01) 107121 01
81996 168409322 -14102 11 (11)A> 107121 01
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 111+V(1) (10)C> 01 00 10
1 5 -3 01 111+V(1) <B(11) 002 10
2 9+4*V(1) -5+-2*V(1) 01 <B(11) 011+V(1) 002 10
3 16+4*V(1) -2+-2*V(1) 11 (11)E> 011+V(1) 002 10
4 18+6*V(1) 0 112+V(1) (11)E> 002 10
5 20+6*V(1) 2 113+V(1) (11)A> 00 10
6 24+6*V(1) 4 114+V(1) (01)D> 10
7 27+6*V(1) 1 114+V(1) <E(10)
8 43+10*V(1) -7+-2*V(1) <E(10) 104+V(1)
9 46+10*V(1) -4+-2*V(1) 01 (11)F> 104+V(1)
10 54+12*V(1) 4 01 114+V(1) (11)F>
11 56+12*V(1) 6 01 115+V(1) (11)B>
12 67+12*V(1) 3 01 115+V(1) <E(10) 01
13 87+16*V(1) -7+-2*V(1) 01 <E(10) 105+V(1) 01
14 89+16*V(1) -9+-2*V(1) <A(01) 106+V(1) 01
15 100+16*V(1) -6+-2*V(1) 11 (11)A> 106+V(1) 01
<< Success! ==> defined new CTR 15 (PPA)
81996 168409322 -14102 11 (11)A> 107121 01
== Executing PA-CTR 1, V(1)=0, V(2)=7116, repcount=1780, factor=5/4
103356 263521842 138 118901 (11)A> 10 01
103357 263521844 140 118902 (01)D> 01
103358 263521847 137 118902 <A(01) 11
103359 263521853 135 118901 <B(11) 00 11
103360 263557457 -17667 <B(11) 018901 00 11
103361 263557465 -17669 <E(10) 018902 00 11
103362 263557468 -17666 01 (11)F> 018902 00 11
103363 263557470 -17664 01 11 (10)C> 018901 00 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 115+V(1) (11)A> 10 01
1 2 2 116+V(1) (01)D> 01
2 5 -1 116+V(1) <A(01) 11
3 11 -3 115+V(1) <B(11) 00 11
4 31+4*V(1) -13+-2*V(1) <B(11) 015+V(1) 00 11
5 39+4*V(1) -15+-2*V(1) <E(10) 016+V(1) 00 11
6 42+4*V(1) -12+-2*V(1) 01 (11)F> 016+V(1) 00 11
7 44+4*V(1) -10+-2*V(1) 01 11 (10)C> 015+V(1) 00 11
<< Success! ==> defined new CTR 16 (PPA)
103363 263557470 -17664 01 11 (10)C> 018901 00 11
== Executing PA-CTR 2, V(1)=0, V(2)=8896, repcount=2225, factor=5/4
127838 412151870 136 01 1111126 (10)C> 01 00 11
127839 412151875 133 01 1111126 <B(11) 002 11
127840 412196379 -22119 01 <B(11) 0111126 002 11
127841 412196386 -22116 11 (11)E> 0111126 002 11
127842 412218638 136 1111127 (11)E> 002 11
127843 412218640 138 1111128 (11)A> 00 11
127844 412218644 140 1111129 (01)D> 11
127845 412218647 137 1111129 <E(10) 01
127846 412263163 -22121 <E(10) 1011129 01
127847 412263166 -22118 01 (11)F> 1011129 01
127848 412285424 140 01 1111129 (11)F> 01
127849 412285426 142 01 1111130 (10)C>
127850 412285435 139 01 1111130 <E(10) 01
127851 412329955 -22121 01 <E(10) 1011130 01
127852 412329957 -22123 <A(01) 1011131 01
127853 412329968 -22120 11 (11)A> 1011131 01
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 111+V(1) (10)C> 01 00 11
1 5 -3 01 111+V(1) <B(11) 002 11
2 9+4*V(1) -5+-2*V(1) 01 <B(11) 011+V(1) 002 11
3 16+4*V(1) -2+-2*V(1) 11 (11)E> 011+V(1) 002 11
4 18+6*V(1) 0 112+V(1) (11)E> 002 11
5 20+6*V(1) 2 113+V(1) (11)A> 00 11
6 24+6*V(1) 4 114+V(1) (01)D> 11
7 27+6*V(1) 1 114+V(1) <E(10) 01
8 43+10*V(1) -7+-2*V(1) <E(10) 104+V(1) 01
9 46+10*V(1) -4+-2*V(1) 01 (11)F> 104+V(1) 01
10 54+12*V(1) 4 01 114+V(1) (11)F> 01
11 56+12*V(1) 6 01 115+V(1) (10)C>
12 65+12*V(1) 3 01 115+V(1) <E(10) 01
13 85+16*V(1) -7+-2*V(1) 01 <E(10) 105+V(1) 01
14 87+16*V(1) -9+-2*V(1) <A(01) 106+V(1) 01
15 98+16*V(1) -6+-2*V(1) 11 (11)A> 106+V(1) 01
<< Success! ==> defined new CTR 17 (PPA)
127853 412329968 -22120 11 (11)A> 1011131 01
== Executing PA-CTR 1, V(1)=0, V(2)=11126, repcount=2782, factor=5/4
161237 644610276 136 1113911 (11)A> 103 01
== Executing PPA-CTR 4 (once), V(1)=13910, V(2)=0
161260 644832980 -27688 01 11 (10)C> 0113918 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=13913, repcount=3479, factor=5/4
199529 1008054496 144 01 1117396 (10)C> 012 00 10
== Executing PPA-CTR 3 (once), V(1)=17395, V(2)=0
199547 1008332958 -34652 11 (11)A> 1017404 01
== Executing PA-CTR 1, V(1)=0, V(2)=17399, repcount=4350, factor=5/4
251747 1576155858 148 1121751 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=21750
251771 1576634562 -43358 11 (11)A> 1021761 01
== Executing PA-CTR 1, V(1)=0, V(2)=21756, repcount=5440, factor=5/4
317051 2464627522 162 1127201 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=27196
317058 2464736350 -54240 01 11 (10)C> 0127201 00 11
== Executing PA-CTR 2, V(1)=0, V(2)=27196, repcount=6800, factor=5/4
391858 3852167550 160 01 1134001 (10)C> 01 00 11
== Executing PPA-CTR 17 (once), V(1)=34000
391873 3852711648 -67846 11 (11)A> 1034006 01
== Executing PA-CTR 1, V(1)=0, V(2)=34001, repcount=8501, factor=5/4
493885 6021010712 162 1142506 (11)A> 102 01
== Executing PPA-CTR 9 (once), V(1)=42505
493903 6021690894 -84852 01 11 (10)C> 0142510 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=42505, repcount=10627, factor=5/4
610800 9410046082 164 01 1153136 (10)C> 012 00 10
== Executing PPA-CTR 3 (once), V(1)=53135, V(2)=0
610818 9410896384 -106112 11 (11)A> 1053144 01
== Executing PA-CTR 1, V(1)=0, V(2)=53139, repcount=13285, factor=5/4
770238 14706084824 168 1166426 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=66425
770262 14707546378 -132688 11 (11)A> 1066436 01
== Executing PA-CTR 1, V(1)=0, V(2)=66431, repcount=16608, factor=5/4
969558 22982880970 176 1183041 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=83040
969582 22984708054 -165910 11 (11)A> 1083051 01
== Executing PA-CTR 1, V(1)=0, V(2)=83046, repcount=20762, factor=5/4
1218726 35917233282 186 11103811 (11)A> 103 01
== Executing PPA-CTR 4 (once), V(1)=103810, V(2)=0
1218749 35918894386 -207438 01 11 (10)C> 01103818 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=103813, repcount=25954, factor=5/4
1504243 56128080302 194 01 11129771 (10)C> 012 00 10
== Executing PPA-CTR 3 (once), V(1)=129770, V(2)=0
1504261 56130156764 -259352 11 (11)A> 10129779 01
== Executing PA-CTR 1, V(1)=0, V(2)=129774, repcount=32444, factor=5/4
1893589 87709653940 200 11162221 (11)A> 103 01
== Executing PPA-CTR 4 (once), V(1)=162220, V(2)=0
1893612 87712249604 -324244 01 11 (10)C> 01162228 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=162223, repcount=40556, factor=5/4
2339728 137057302588 204 01 11202781 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=202780
2339743 137060547178 -405362 11 (11)A> 10202787 01 10
== Executing PA-CTR 5, V(1)=0, V(2)=202782, repcount=50696, factor=5/4
2948095 214164803322 206 11253481 (11)A> 103 01 10
2948096 214164803324 208 11253482 (01)D> 102 01 10
2948097 214164803327 205 11253482 <E(10) 00 10 01 10
2948098 214165817255 -506759 <E(10) 10253482 00 10 01 10
2948099 214165817258 -506756 01 (11)F> 10253482 00 10 01 10
2948100 214166324222 208 01 11253482 (11)F> 00 10 01 10
2948101 214166324224 210 01 11253483 (11)B> 10 01 10
2948102 214166324228 212 01 11253484 (11)E> 01 10
2948103 214166324230 214 01 11253485 (11)E> 10
2948104 214166324235 211 01 11253485 <B(11)
2948105 214167338175 -506759 01 <B(11) 01253485
2948106 214167338182 -506756 11 (11)E> 01253485
2948107 214167845152 214 11253486 (11)E>
2948108 214167845154 216 11253487 (11)A>
2948109 214167845158 218 11253488 (01)D>
2948110 214167845161 215 11253488 <A(01) 10
2948111 214167845167 213 11253487 <B(11) 00 10
2948112 214168859115 -506761 <B(11) 01253487 00 10
2948113 214168859123 -506763 <E(10) 01253488 00 10
2948114 214168859126 -506760 01 (11)F> 01253488 00 10
2948115 214168859128 -506758 01 11 (10)C> 01253487 00 10
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 111+V(1) (11)A> 103 011+V(2) 10
1 2 2 112+V(1) (01)D> 102 011+V(2) 10
2 5 -1 112+V(1) <E(10) 00 10 011+V(2) 10
3 13+4*V(1) -5+-2*V(1) <E(10) 102+V(1) 00 10 011+V(2) 10
4 16+4*V(1) -2+-2*V(1) 01 (11)F> 102+V(1) 00 10 011+V(2) 10
5 20+6*V(1) 2 01 112+V(1) (11)F> 00 10 011+V(2) 10
6 22+6*V(1) 4 01 113+V(1) (11)B> 10 011+V(2) 10
7 26+6*V(1) 6 01 114+V(1) (11)E> 011+V(2) 10
8 28+6*V(1)+2*V(2) 8+2*V(2) 01 115+V(1)+V(2) (11)E> 10
9 33+6*V(1)+2*V(2) 5+2*V(2) 01 115+V(1)+V(2) <B(11)
10 53+10*V(1)+6*V(2) -5+-2*V(1) 01 <B(11) 015+V(1)+V(2)
11 60+10*V(1)+6*V(2) -2+-2*V(1) 11 (11)E> 015+V(1)+V(2)
12 70+12*V(1)+8*V(2) 8+2*V(2) 116+V(1)+V(2) (11)E>
13 72+12*V(1)+8*V(2) 10+2*V(2) 117+V(1)+V(2) (11)A>
14 76+12*V(1)+8*V(2) 12+2*V(2) 118+V(1)+V(2) (01)D>
15 79+12*V(1)+8*V(2) 9+2*V(2) 118+V(1)+V(2) <A(01) 10
16 85+12*V(1)+8*V(2) 7+2*V(2) 117+V(1)+V(2) <B(11) 00 10
17 113+16*V(1)+12*V(2) -7+-2*V(1) <B(11) 017+V(1)+V(2) 00 10
18 121+16*V(1)+12*V(2) -9+-2*V(1) <E(10) 018+V(1)+V(2) 00 10
19 124+16*V(1)+12*V(2) -6+-2*V(1) 01 (11)F> 018+V(1)+V(2) 00 10
20 126+16*V(1)+12*V(2) -4+-2*V(1) 01 11 (10)C> 017+V(1)+V(2) 00 10
<< Success! ==> defined new CTR 18 (PPA)
2948115 214168859128 -506758 01 11 (10)C> 01253487 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=253482, repcount=63371, factor=5/4
3645196 334647522972 210 01 11316856 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=316855
3645223 334654493986 -633506 01 11 (10)C> 01316865 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=316860, repcount=79216, factor=5/4
4516599 522912427010 222 01 11396081 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=396080
4516614 522918764390 -791944 11 (11)A> 10396086 01
== Executing PA-CTR 1, V(1)=0, V(2)=396081, repcount=99021, factor=5/4
5704866 817076884334 224 11495106 (11)A> 102 01
== Executing PPA-CTR 9 (once), V(1)=495105
5704884 817084806116 -989990 01 11 (10)C> 01495110 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=495105, repcount=123777, factor=5/4
7066431 1276711386404 226 01 11618886 (10)C> 012 00 10
== Executing PPA-CTR 3 (once), V(1)=618885, V(2)=0
7066449 1276721288706 -1237550 11 (11)A> 10618894 01
== Executing PA-CTR 1, V(1)=0, V(2)=618889, repcount=154723, factor=5/4
8923125 1994902751158 234 11773616 (11)A> 102 01
== Executing PPA-CTR 9 (once), V(1)=773615
8923143 1994915129100 -1547000 01 11 (10)C> 01773620 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=773615, repcount=193404, factor=5/4
11050587 3117074921316 232 01 11967021 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=967020
11050602 3117090393746 -1933814 11 (11)A> 10967027 01 10
== Executing PA-CTR 5, V(1)=0, V(2)=967022, repcount=241756, factor=5/4
13951674 4870477519530 234 111208781 (11)A> 103 01 10
== Executing PPA-CTR 18 (once), V(1)=1208780, V(2)=0
13951694 4870496860136 -2417330 01 11 (10)C> 011208787 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=1208782, repcount=302196, factor=5/4
17275850 7610179807280 238 01 111510981 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=1510980
17275877 7610213049044 -3021728 01 11 (10)C> 011510990 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=1510985, repcount=377747, factor=5/4
21431094 11891009772712 248 01 111888736 (10)C> 012 00 10
== Executing PPA-CTR 3 (once), V(1)=1888735, V(2)=0
21431112 11891039992614 -3777228 11 (11)A> 101888744 01
== Executing PA-CTR 1, V(1)=0, V(2)=1888739, repcount=472185, factor=5/4
27097332 18579816273654 252 112360926 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=2360925
27097356 18579868214208 -4721604 11 (11)A> 102360936 01
== Executing PA-CTR 1, V(1)=0, V(2)=2360931, repcount=590233, factor=5/4
34180152 29031138110800 260 112951166 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=2951165
34180176 29031203036634 -5902076 11 (11)A> 102951176 01
== Executing PA-CTR 1, V(1)=0, V(2)=2951171, repcount=737793, factor=5/4
43033692 45361383447066 268 113688966 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=3688965
43033716 45361464604500 -7377668 11 (11)A> 103688976 01
== Executing PA-CTR 1, V(1)=0, V(2)=3688971, repcount=922243, factor=5/4
54100632 70877460492232 276 114611216 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=4611215
54100656 70877561939166 -9222160 11 (11)A> 104611226 01
== Executing PA-CTR 1, V(1)=0, V(2)=4611221, repcount=1152806, factor=5/4
67934328 110746451343650 288 115764031 (11)A> 102 01
== Executing PPA-CTR 9 (once), V(1)=5764030
67934346 110746543568232 -11527776 01 11 (10)C> 015764035 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=5764030, repcount=1441008, factor=5/4
83785434 173041714244424 288 01 117205041 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=7205040
83785461 173041872755508 -14409798 01 11 (10)C> 017205050 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=7205045, repcount=1801262, factor=5/4
103599343 270378277777736 298 01 119006311 (10)C> 012 00 10
== Executing PPA-CTR 3 (once), V(1)=9006310, V(2)=0
103599361 270378421878838 -18012328 11 (11)A> 109006319 01
== Executing PA-CTR 1, V(1)=0, V(2)=9006314, repcount=2251579, factor=5/4
130618309 422466738229754 304 1111257896 (11)A> 103 01
== Executing PPA-CTR 4 (once), V(1)=11257895, V(2)=0
130618332 422466918356218 -22515490 01 11 (10)C> 0111257903 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=11257898, repcount=2814475, factor=5/4
161577557 660105099817118 310 01 1114072376 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=14072375
161577584 660105409409572 -28144446 01 11 (10)C> 0114072385 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=14072380, repcount=3518096, factor=5/4
200276640 1031415512981316 322 01 1117590481 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=17590480
200276655 1031415794429096 -35180644 11 (11)A> 1017590486 01
== Executing PA-CTR 1, V(1)=0, V(2)=17590481, repcount=4397621, factor=5/4
253048107 1611588057737440 324 1121988106 (11)A> 102 01
== Executing PPA-CTR 9 (once), V(1)=21988105
253048125 1611588409547222 -43975890 01 11 (10)C> 0121988110 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=21988105, repcount=5497027, factor=5/4
313515422 2518107771608010 326 01 1127485136 (10)C> 012 00 10
== Executing PPA-CTR 3 (once), V(1)=27485135, V(2)=0
313515440 2518108211370312 -54969950 11 (11)A> 1027485144 01
== Executing PA-CTR 1, V(1)=0, V(2)=27485139, repcount=6871285, factor=5/4
395970860 3934545171530752 330 1134356426 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=34356425
395970884 3934545927372306 -68712526 11 (11)A> 1034356436 01
== Executing PA-CTR 1, V(1)=0, V(2)=34356431, repcount=8589108, factor=5/4
499040180 6147729506471898 338 1142945541 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=42945540
499040204 6147730451273982 -85890748 11 (11)A> 1042945551 01
== Executing PA-CTR 1, V(1)=0, V(2)=42945546, repcount=10736387, factor=5/4
627876848 9605830990724210 348 1153681936 (11)A> 103 01
== Executing PPA-CTR 4 (once), V(1)=53681935, V(2)=0
627876871 9605831849635314 -107363526 01 11 (10)C> 0153681943 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=53681938, repcount=13420485, factor=5/4
775502206 15009114834988554 354 01 1167102426 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=67102425
775502233 15009116311242108 -134204502 01 11 (10)C> 0167102435 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=67102430, repcount=16775608, factor=5/4
960033921 23451747594702700 362 01 1183878041 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=83878040
960033948 23451749440019784 -167755724 01 11 (10)C> 0183878050 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=83878045, repcount=20969512, factor=5/4
1190698580 36643363158527512 372 01 11104847561 (10)C> 012 00 10
== Executing PPA-CTR 3 (once), V(1)=104847560, V(2)=0
1190698598 36643364836088614 -209694754 11 (11)A> 10104847569 01
== Executing PA-CTR 1, V(1)=0, V(2)=104847564, repcount=26211892, factor=5/4
1505241302 57255264193882862 382 11131059461 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=131059456
1505241309 57255264718120730 -262118540 01 11 (10)C> 01131059461 00 11
== Executing PA-CTR 2, V(1)=0, V(2)=131059456, repcount=32764865, factor=5/4
1865654824 89461357186172890 380 01 11163824326 (10)C> 01 00 11
== Executing PPA-CTR 17 (once), V(1)=163824325
1865654839 89461359807362188 -327648276 11 (11)A> 10163824331 01
== Executing PA-CTR 1, V(1)=0, V(2)=163824326, repcount=40956082, factor=5/4
2357127823 1397833[4]3590696 380 11204780411 (11)A> 103 01
== Executing PPA-CTR 4 (once), V(1)=204780410, V(2)=0
2357127846 1397833[4]0077400 -409560444 01 11 (10)C> 01204780418 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=204780413, repcount=51195104, factor=5/4
2920273990 2184115[4]7835416 388 01 11255975521 (10)C> 012 00 10
== Executing PPA-CTR 3 (once), V(1)=255975520, V(2)=0
2920274008 2184115[4]3443878 -511950658 11 (11)A> 10255975529 01
== Executing PA-CTR 1, V(1)=0, V(2)=255975524, repcount=63993882, factor=5/4
3688200592 3412680[4]2133586 398 11319969411 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=319969406
3688200599 3412680[4]2011254 -639938424 01 11 (10)C> 01319969411 00 11
== Executing PA-CTR 2, V(1)=0, V(2)=319969406, repcount=79992352, factor=5/4
4568116471 5332313[4]6508342 392 01 11399961761 (10)C> 013 00 11
4568116472 5332313[4]6508347 389 01 11399961761 <B(11) 00 012 00 11
4568116473 5332313[4]6355391 -799923133 01 <B(11) 01399961761 00 012 00 11
4568116474 5332313[4]6355398 -799923130 11 (11)E> 01399961761 00 012 00 11
4568116475 5332313[4]6278920 392 11399961762 (11)E> 00 012 00 11
4568116476 5332313[4]6278922 394 11399961763 (11)A> 012 00 11
4568116477 5332313[4]6278924 396 11399961764 (10)D> 01 00 11
4568116478 5332313[4]6278935 393 11399961764 <E(10) 10 00 11
4568116479 5332313[4]6125991 -799923135 <E(10) 10399961765 00 11
4568116480 5332313[4]6125994 -799923132 01 (11)F> 10399961765 00 11
4568116481 5332313[4]6049524 398 01 11399961765 (11)F> 00 11
4568116482 5332313[4]6049526 400 01 11399961766 (11)B> 11
4568116483 5332313[4]6049533 397 01 11399961766 <E(10) 10
4568116484 5332313[4]5896597 -799923135 01 <E(10) 10399961767
4568116485 5332313[4]5896599 -799923137 <A(01) 10399961768
4568116486 5332313[4]5896610 -799923134 11 (11)A> 10399961768
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 111+V(1) (10)C> 013 00 11
1 5 -3 01 111+V(1) <B(11) 00 012 00 11
2 9+4*V(1) -5+-2*V(1) 01 <B(11) 011+V(1) 00 012 00 11
3 16+4*V(1) -2+-2*V(1) 11 (11)E> 011+V(1) 00 012 00 11
4 18+6*V(1) 0 112+V(1) (11)E> 00 012 00 11
5 20+6*V(1) 2 113+V(1) (11)A> 012 00 11
6 22+6*V(1) 4 114+V(1) (10)D> 01 00 11
7 33+6*V(1) 1 114+V(1) <E(10) 10 00 11
8 49+10*V(1) -7+-2*V(1) <E(10) 105+V(1) 00 11
9 52+10*V(1) -4+-2*V(1) 01 (11)F> 105+V(1) 00 11
10 62+12*V(1) 6 01 115+V(1) (11)F> 00 11
11 64+12*V(1) 8 01 116+V(1) (11)B> 11
12 71+12*V(1) 5 01 116+V(1) <E(10) 10
13 95+16*V(1) -7+-2*V(1) 01 <E(10) 107+V(1)
14 97+16*V(1) -9+-2*V(1) <A(01) 108+V(1)
15 108+16*V(1) -6+-2*V(1) 11 (11)A> 108+V(1)
<< Success! ==> defined new CTR 19 (PPA)
4568116486 5332313[4]5896610 -799923134 11 (11)A> 10399961768
== Executing PA-CTR 13, V(1)=0, V(2)=399961763, repcount=99990441, factor=5/4
5768001778 8331740[4]6806034 394 11499952206 (11)A> 104
5768001779 8331740[4]6806036 396 11499952207 (01)D> 103
5768001780 8331740[4]6806039 393 11499952207 <E(10) 00 102
5768001781 8331740[4]6614867 -999904021 <E(10) 10499952207 00 102
5768001782 8331740[4]6614870 -999904018 01 (11)F> 10499952207 00 102
5768001783 8331740[4]6519284 396 01 11499952207 (11)F> 00 102
5768001784 8331740[4]6519286 398 01 11499952208 (11)B> 102
5768001785 8331740[4]6519290 400 01 11499952209 (11)E> 10
5768001786 8331740[4]6519295 397 01 11499952209 <B(11)
5768001787 8331740[4]6328131 -999904021 01 <B(11) 01499952209
5768001788 8331740[4]6328138 -999904018 11 (11)E> 01499952209
5768001789 8331740[4]6232556 400 11499952210 (11)E>
5768001790 8331740[4]6232558 402 11499952211 (11)A>
5768001791 8331740[4]6232562 404 11499952212 (01)D>
5768001792 8331740[4]6232565 401 11499952212 <A(01) 10
5768001793 8331740[4]6232571 399 11499952211 <B(11) 00 10
5768001794 8331740[4]6041415 -999904023 <B(11) 01499952211 00 10
5768001795 8331740[4]6041423 -999904025 <E(10) 01499952212 00 10
5768001796 8331740[4]6041426 -999904022 01 (11)F> 01499952212 00 10
5768001797 8331740[4]6041428 -999904020 01 11 (10)C> 01499952211 00 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 111+V(1) (11)A> 104
1 2 2 112+V(1) (01)D> 103
2 5 -1 112+V(1) <E(10) 00 102
3 13+4*V(1) -5+-2*V(1) <E(10) 102+V(1) 00 102
4 16+4*V(1) -2+-2*V(1) 01 (11)F> 102+V(1) 00 102
5 20+6*V(1) 2 01 112+V(1) (11)F> 00 102
6 22+6*V(1) 4 01 113+V(1) (11)B> 102
7 26+6*V(1) 6 01 114+V(1) (11)E> 10
8 31+6*V(1) 3 01 114+V(1) <B(11)
9 47+10*V(1) -5+-2*V(1) 01 <B(11) 014+V(1)
10 54+10*V(1) -2+-2*V(1) 11 (11)E> 014+V(1)
11 62+12*V(1) 6 115+V(1) (11)E>
12 64+12*V(1) 8 116+V(1) (11)A>
13 68+12*V(1) 10 117+V(1) (01)D>
14 71+12*V(1) 7 117+V(1) <A(01) 10
15 77+12*V(1) 5 116+V(1) <B(11) 00 10
16 101+16*V(1) -7+-2*V(1) <B(11) 016+V(1) 00 10
17 109+16*V(1) -9+-2*V(1) <E(10) 017+V(1) 00 10
18 112+16*V(1) -6+-2*V(1) 01 (11)F> 017+V(1) 00 10
19 114+16*V(1) -4+-2*V(1) 01 11 (10)C> 016+V(1) 00 10
<< Success! ==> defined new CTR 20 (PPA)
5768001797 8331740[4]6041428 -999904020 01 11 (10)C> 01499952211 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=499952206, repcount=124988052, factor=5/4
7142870369 1301834[5]8276316 396 01 11624940261 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=624940260
7142870396 1301834[5]6962240 -1249880130 01 11 (10)C> 01624940270 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=624940265, repcount=156235067, factor=5/4
8861456133 2034116[5]3789188 406 01 11781175336 (10)C> 012 00 10
== Executing PPA-CTR 3 (once), V(1)=781175335, V(2)=0
8861456151 2034116[5]2594690 -1562350270 11 (11)A> 10781175344 01
== Executing PA-CTR 1, V(1)=0, V(2)=781175339, repcount=195293835, factor=5/4
11204982171 3178306[5]2801830 410 11976469176 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=976469175
11204982195 3178306[5]5123884 -1952937946 11 (11)A> 10976469186 01
== Executing PA-CTR 1, V(1)=0, V(2)=976469181, repcount=244117296, factor=5/4
14134389747 4966104[5]5660428 422 111220586481 (11)A> 102 01
== Executing PPA-CTR 9 (once), V(1)=1220586480
14134389765 4966104[5]5044210 -2441172542 01 11 (10)C> 011220586485 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=1220586480, repcount=305146621, factor=5/4
17491002596 7759538[5]1558554 426 01 111525733106 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=1525733105
17491002611 7759538[5]3288334 -3051465790 11 (11)A> 101525733111 01
== Executing PA-CTR 1, V(1)=0, V(2)=1525733106, repcount=381433277, factor=5/4
22068201935 1212427[6]0781622 426 111907166386 (11)A> 103 01
== Executing PPA-CTR 4 (once), V(1)=1907166385, V(2)=0
22068201958 1212427[6]5443926 -3814332348 01 11 (10)C> 011907166393 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=1907166388, repcount=476791598, factor=5/4
27312909536 1894418[6]8166378 436 01 112383957991 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=2383957990
27312909551 1894418[6]1494318 -4767915550 11 (11)A> 102383957996 01
== Executing PA-CTR 1, V(1)=0, V(2)=2383957991, repcount=595989498, factor=5/4
34464783527 2960029[6]3897370 434 112979947491 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=2979947490
34464783551 2960029[6]2742354 -5959894552 11 (11)A> 102979947501 01
== Executing PA-CTR 1, V(1)=0, V(2)=2979947496, repcount=744986875, factor=5/4
43404626051 4625045[6]0264854 448 113724934376 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=3724934371
43404626058 4625045[6]0002382 -7449868304 01 11 (10)C> 013724934376 00 11
== Executing PA-CTR 2, V(1)=0, V(2)=3724934371, repcount=931233593, factor=5/4
53648195581 7226633[6]2634014 440 01 114656167966 (10)C> 014 00 11
== Executing PPA-CTR 11 (once), V(1)=4656167965
53648195596 7226633[6]1321564 -9312335496 11 (11)A> 104656167972 01 11
== Executing PA-CTR 5, V(1)=0, V(2)=4656167967, repcount=1164041992, factor=5/4
67616699500 1129161[7]8591212 440 115820209961 (11)A> 104 01 11
67616699501 1129161[7]8591214 442 115820209962 (01)D> 103 01 11
67616699502 1129161[7]8591217 439 115820209962 <E(10) 00 102 01 11
67616699503 1129161[7]9431065 -11640419485 <E(10) 105820209962 00 102 01 11
67616699504 1129161[7]9431068 -11640419482 01 (11)F> 105820209962 00 102 01 11
67616699505 1129161[7]9850992 442 01 115820209962 (11)F> 00 102 01 11
67616699506 1129161[7]9850994 444 01 115820209963 (11)B> 102 01 11
67616699507 1129161[7]9850998 446 01 115820209964 (11)E> 10 01 11
67616699508 1129161[7]9851003 443 01 115820209964 <B(11) 00 01 11
67616699509 1129161[7]0690859 -11640419485 01 <B(11) 015820209964 00 01 11
67616699510 1129161[7]0690866 -11640419482 11 (11)E> 015820209964 00 01 11
67616699511 1129161[7]1110794 446 115820209965 (11)E> 00 01 11
67616699512 1129161[7]1110796 448 115820209966 (11)A> 01 11
67616699513 1129161[7]1110798 450 115820209967 (10)D> 11
67616699514 1129161[7]1110801 447 115820209967 <B(11) 01
67616699515 1129161[7]1950669 -11640419487 <B(11) 015820209968
67616699516 1129161[7]1950677 -11640419489 <E(10) 015820209969
67616699517 1129161[7]1950680 -11640419486 01 (11)F> 015820209969
67616699518 1129161[7]1950682 -11640419484 01 11 (10)C> 015820209968
67616699519 1129161[7]1950687 -11640419487 01 11 <B(11) 00 015820209967
67616699520 1129161[7]1950691 -11640419489 01 <B(11) 01 00 015820209967
67616699521 1129161[7]1950698 -11640419486 11 (11)E> 01 00 015820209967
67616699522 1129161[7]1950700 -11640419484 112 (11)E> 00 015820209967
67616699523 1129161[7]1950702 -11640419482 113 (11)A> 015820209967
67616699524 1129161[7]1950704 -11640419480 114 (10)D> 015820209966
67616699525 1129161[7]1950715 -11640419483 114 <E(10) 10 015820209965
67616699526 1129161[7]1950731 -11640419491 <E(10) 105 015820209965
67616699527 1129161[7]1950734 -11640419488 01 (11)F> 105 015820209965
67616699528 1129161[7]1950744 -11640419478 01 115 (11)F> 015820209965
67616699529 1129161[7]1950746 -11640419476 01 116 (10)C> 015820209964
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 01 111+V(1) (10)C> 015+V(2)
1 5 -3 01 111+V(1) <B(11) 00 014+V(2)
2 9+4*V(1) -5+-2*V(1) 01 <B(11) 011+V(1) 00 014+V(2)
3 16+4*V(1) -2+-2*V(1) 11 (11)E> 011+V(1) 00 014+V(2)
4 18+6*V(1) 0 112+V(1) (11)E> 00 014+V(2)
5 20+6*V(1) 2 113+V(1) (11)A> 014+V(2)
6 22+6*V(1) 4 114+V(1) (10)D> 013+V(2)
7 33+6*V(1) 1 114+V(1) <E(10) 10 012+V(2)
8 49+10*V(1) -7+-2*V(1) <E(10) 105+V(1) 012+V(2)
9 52+10*V(1) -4+-2*V(1) 01 (11)F> 105+V(1) 012+V(2)
10 62+12*V(1) 6 01 115+V(1) (11)F> 012+V(2)
11 64+12*V(1) 8 01 116+V(1) (10)C> 011+V(2)
<< Success! ==> defined new CTR 21 (PA)
67616699529 1129161[7]1950746 -11640419476 01 116 (10)C> 015820209964
== Executing PA-CTR 21, V(1)=5, V(2)=5820209959, repcount=1455052490, factor=5/4
83622276919 1764314[7]2887806 444 01 117275262456 (10)C> 014
83622276920 1764314[7]2887811 441 01 117275262456 <B(11) 00 013
83622276921 1764314[7]3937635 -14550524471 01 <B(11) 017275262456 00 013
83622276922 1764314[7]3937642 -14550524468 11 (11)E> 017275262456 00 013
83622276923 1764314[7]4462554 444 117275262457 (11)E> 00 013
83622276924 1764314[7]4462556 446 117275262458 (11)A> 013
83622276925 1764314[7]4462558 448 117275262459 (10)D> 012
83622276926 1764314[7]4462569 445 117275262459 <E(10) 10 01
83622276927 1764314[7]5512405 -14550524473 <E(10) 107275262460 01
83622276928 1764314[7]5512408 -14550524470 01 (11)F> 107275262460 01
83622276929 1764314[7]6037328 450 01 117275262460 (11)F> 01
83622276930 1764314[7]6037330 452 01 117275262461 (10)C>
83622276931 1764314[7]6037339 449 01 117275262461 <E(10) 01
83622276932 1764314[7]7087183 -14550524473 01 <E(10) 107275262461 01
83622276933 1764314[7]7087185 -14550524475 <A(01) 107275262462 01
83622276934 1764314[7]7087196 -14550524472 11 (11)A> 107275262462 01
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 111+V(1) (10)C> 014
1 5 -3 01 111+V(1) <B(11) 00 013
2 9+4*V(1) -5+-2*V(1) 01 <B(11) 011+V(1) 00 013
3 16+4*V(1) -2+-2*V(1) 11 (11)E> 011+V(1) 00 013
4 18+6*V(1) 0 112+V(1) (11)E> 00 013
5 20+6*V(1) 2 113+V(1) (11)A> 013
6 22+6*V(1) 4 114+V(1) (10)D> 012
7 33+6*V(1) 1 114+V(1) <E(10) 10 01
8 49+10*V(1) -7+-2*V(1) <E(10) 105+V(1) 01
9 52+10*V(1) -4+-2*V(1) 01 (11)F> 105+V(1) 01
10 62+12*V(1) 6 01 115+V(1) (11)F> 01
11 64+12*V(1) 8 01 116+V(1) (10)C>
12 73+12*V(1) 5 01 116+V(1) <E(10) 01
13 97+16*V(1) -7+-2*V(1) 01 <E(10) 106+V(1) 01
14 99+16*V(1) -9+-2*V(1) <A(01) 107+V(1) 01
15 110+16*V(1) -6+-2*V(1) 11 (11)A> 107+V(1) 01
<< Success! ==> defined new CTR 22 (PPA)
83622276934 1764314[7]7087196 -14550524472 11 (11)A> 107275262462 01
== Executing PA-CTR 1, V(1)=0, V(2)=7275262457, repcount=1818815615, factor=5/4
105448064314 2756741[7]1664856 448 119094078076 (11)A> 102 01
== Executing PPA-CTR 9 (once), V(1)=9094078075
105448064332 2756741[7]6914158 -18188155706 01 11 (10)C> 019094078080 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=9094078075, repcount=2273519519, factor=5/4
130456779041 4307409[7]6318634 446 01 1111367597596 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=11367597595
130456779056 4307409[7]7880264 -22735194750 11 (11)A> 1011367597602 01 10
== Executing PA-CTR 5, V(1)=0, V(2)=11367597597, repcount=2841899400, factor=5/4
164559571856 6730326[7]3259864 450 1114209497001 (11)A> 102 01 10
164559571857 6730326[7]3259866 452 1114209497002 (01)D> 10 01 10
164559571858 6730326[7]3259869 449 1114209497002 <E(10) 00 01 10
164559571859 6730326[7]1247877 -28418993555 <E(10) 1014209497002 00 01 10
164559571860 6730326[7]1247880 -28418993552 01 (11)F> 1014209497002 00 01 10
164559571861 6730326[7]0241884 452 01 1114209497002 (11)F> 00 01 10
164559571862 6730326[7]0241886 454 01 1114209497003 (11)B> 01 10
164559571863 6730326[7]0241893 451 01 1114209497003 <B(11) 00 10
164559571864 6730326[7]8229905 -28418993555 01 <B(11) 0114209497003 00 10
164559571865 6730326[7]8229912 -28418993552 11 (11)E> 0114209497003 00 10
164559571866 6730326[7]7223918 454 1114209497004 (11)E> 00 10
164559571867 6730326[7]7223920 456 1114209497005 (11)A> 10
164559571868 6730326[7]7223922 458 1114209497006 (01)D>
164559571869 6730326[7]7223925 455 1114209497006 <A(01) 10
164559571870 6730326[7]7223931 453 1114209497005 <B(11) 00 10
164559571871 6730326[7]5211951 -28418993557 <B(11) 0114209497005 00 10
164559571872 6730326[7]5211959 -28418993559 <E(10) 0114209497006 00 10
164559571873 6730326[7]5211962 -28418993556 01 (11)F> 0114209497006 00 10
164559571874 6730326[7]5211964 -28418993554 01 11 (10)C> 0114209497005 00 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 111+V(1) (11)A> 102 01 10
1 2 2 112+V(1) (01)D> 10 01 10
2 5 -1 112+V(1) <E(10) 00 01 10
3 13+4*V(1) -5+-2*V(1) <E(10) 102+V(1) 00 01 10
4 16+4*V(1) -2+-2*V(1) 01 (11)F> 102+V(1) 00 01 10
5 20+6*V(1) 2 01 112+V(1) (11)F> 00 01 10
6 22+6*V(1) 4 01 113+V(1) (11)B> 01 10
7 29+6*V(1) 1 01 113+V(1) <B(11) 00 10
8 41+10*V(1) -5+-2*V(1) 01 <B(11) 013+V(1) 00 10
9 48+10*V(1) -2+-2*V(1) 11 (11)E> 013+V(1) 00 10
10 54+12*V(1) 4 114+V(1) (11)E> 00 10
11 56+12*V(1) 6 115+V(1) (11)A> 10
12 58+12*V(1) 8 116+V(1) (01)D>
13 61+12*V(1) 5 116+V(1) <A(01) 10
14 67+12*V(1) 3 115+V(1) <B(11) 00 10
15 87+16*V(1) -7+-2*V(1) <B(11) 015+V(1) 00 10
16 95+16*V(1) -9+-2*V(1) <E(10) 016+V(1) 00 10
17 98+16*V(1) -6+-2*V(1) 01 (11)F> 016+V(1) 00 10
18 100+16*V(1) -4+-2*V(1) 01 11 (10)C> 015+V(1) 00 10
<< Success! ==> defined new CTR 23 (PPA)
164559571874 6730326[7]5211964 -28418993554 01 11 (10)C> 0114209497005 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=14209497000, repcount=3552374251, factor=5/4
203635688635 1051613[8]0266528 454 01 1117761871256 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=17761871255
203635688650 1051613[8]0206708 -35523742062 11 (11)A> 1017761871261 01
== Executing PA-CTR 1, V(1)=0, V(2)=17761871256, repcount=4440467815, factor=5/4
256921302430 1643146[8]2339168 458 1122202339076 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=22202339071
256921302437 1643146[8]1695496 -44404677694 01 11 (10)C> 0122202339076 00 11
== Executing PA-CTR 2, V(1)=0, V(2)=22202339071, repcount=5550584768, factor=5/4
317977734885 2567415[8]9992328 450 01 1127752923841 (10)C> 014 00 11
== Executing PPA-CTR 11 (once), V(1)=27752923840
317977734900 2567415[8]6773878 -55505847236 11 (11)A> 1027752923847 01 11
== Executing PA-CTR 5, V(1)=0, V(2)=27752923842, repcount=6938230961, factor=5/4
401236506432 4011587[8]6132182 452 1134691154806 (11)A> 103 01 11
401236506433 4011587[8]6132184 454 1134691154807 (01)D> 102 01 11
401236506434 4011587[8]6132187 451 1134691154807 <E(10) 00 10 01 11
401236506435 4011587[8]0751415 -69382309163 <E(10) 1034691154807 00 10 01 11
401236506436 4011587[8]0751418 -69382309160 01 (11)F> 1034691154807 00 10 01 11
401236506437 4011587[8]3061032 454 01 1134691154807 (11)F> 00 10 01 11
401236506438 4011587[8]3061034 456 01 1134691154808 (11)B> 10 01 11
401236506439 4011587[8]3061038 458 01 1134691154809 (11)E> 01 11
401236506440 4011587[8]3061040 460 01 1134691154810 (11)E> 11
401236506441 4011587[8]3061045 457 01 1134691154810 <B(11) 01
401236506442 4011587[8]7680285 -69382309163 01 <B(11) 0134691154811
401236506443 4011587[8]7680292 -69382309160 11 (11)E> 0134691154811
401236506444 4011587[8]9989914 462 1134691154812 (11)E>
401236506445 4011587[8]9989916 464 1134691154813 (11)A>
401236506446 4011587[8]9989920 466 1134691154814 (01)D>
401236506447 4011587[8]9989923 463 1134691154814 <A(01) 10
401236506448 4011587[8]9989929 461 1134691154813 <B(11) 00 10
401236506449 4011587[8]4609181 -69382309165 <B(11) 0134691154813 00 10
401236506450 4011587[8]4609189 -69382309167 <E(10) 0134691154814 00 10
401236506451 4011587[8]4609192 -69382309164 01 (11)F> 0134691154814 00 10
401236506452 4011587[8]4609194 -69382309162 01 11 (10)C> 0134691154813 00 10
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 111+V(1) (11)A> 103 011+V(2) 11
1 2 2 112+V(1) (01)D> 102 011+V(2) 11
2 5 -1 112+V(1) <E(10) 00 10 011+V(2) 11
3 13+4*V(1) -5+-2*V(1) <E(10) 102+V(1) 00 10 011+V(2) 11
4 16+4*V(1) -2+-2*V(1) 01 (11)F> 102+V(1) 00 10 011+V(2) 11
5 20+6*V(1) 2 01 112+V(1) (11)F> 00 10 011+V(2) 11
6 22+6*V(1) 4 01 113+V(1) (11)B> 10 011+V(2) 11
7 26+6*V(1) 6 01 114+V(1) (11)E> 011+V(2) 11
8 28+6*V(1)+2*V(2) 8+2*V(2) 01 115+V(1)+V(2) (11)E> 11
9 33+6*V(1)+2*V(2) 5+2*V(2) 01 115+V(1)+V(2) <B(11) 01
10 53+10*V(1)+6*V(2) -5+-2*V(1) 01 <B(11) 016+V(1)+V(2)
11 60+10*V(1)+6*V(2) -2+-2*V(1) 11 (11)E> 016+V(1)+V(2)
12 72+12*V(1)+8*V(2) 10+2*V(2) 117+V(1)+V(2) (11)E>
13 74+12*V(1)+8*V(2) 12+2*V(2) 118+V(1)+V(2) (11)A>
14 78+12*V(1)+8*V(2) 14+2*V(2) 119+V(1)+V(2) (01)D>
15 81+12*V(1)+8*V(2) 11+2*V(2) 119+V(1)+V(2) <A(01) 10
16 87+12*V(1)+8*V(2) 9+2*V(2) 118+V(1)+V(2) <B(11) 00 10
17 119+16*V(1)+12*V(2) -7+-2*V(1) <B(11) 018+V(1)+V(2) 00 10
18 127+16*V(1)+12*V(2) -9+-2*V(1) <E(10) 019+V(1)+V(2) 00 10
19 130+16*V(1)+12*V(2) -6+-2*V(1) 01 (11)F> 019+V(1)+V(2) 00 10
20 132+16*V(1)+12*V(2) -4+-2*V(1) 01 11 (10)C> 018+V(1)+V(2) 00 10
<< Success! ==> defined new CTR 24 (PPA)
401236506452 4011587[8]4609194 -69382309162 01 11 (10)C> 0134691154813 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=34691154808, repcount=8672788703, factor=5/4
496637182185 6268105[8]2091366 462 01 1143363943516 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=43363943515
496637182200 6268105[8]5187706 -86727886574 11 (11)A> 1043363943521 01
== Executing PA-CTR 1, V(1)=0, V(2)=43363943516, repcount=10840985880, factor=5/4
626729012760 9793914[8]9939626 466 1154204929401 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=54204929396
626729012767 9793914[8]9657254 -108409858336 01 11 (10)C> 0154204929401 00 11
== Executing PA-CTR 2, V(1)=0, V(2)=54204929396, repcount=13551232350, factor=5/4
775792568617 1530299[9]7232154 464 01 1167756161751 (10)C> 01 00 11
== Executing PPA-CTR 17 (once), V(1)=67756161750
775792568632 1530299[9]5820252 -135512323042 11 (11)A> 1067756161756 01
== Executing PA-CTR 1, V(1)=0, V(2)=67756161751, repcount=16939040438, factor=5/4
979061053888 2391092[9]0150464 462 1184695202191 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=84695202190
979061053912 2391092[9]4598848 -169390403924 11 (11)A> 1084695202201 01
== Executing PA-CTR 1, V(1)=0, V(2)=84695202196, repcount=21173800550, factor=5/4
1233146660512 3736081[9]2892548 476 11105869002751 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=105869002746
1233146660519 3736081[9]8903576 -211738005026 01 11 (10)C> 01105869002751 00 11
== Executing PA-CTR 2, V(1)=0, V(2)=105869002746, repcount=26467250687, factor=5/4
1524286418076 5837627[9]4586004 470 01 11132336253436 (10)C> 013 00 11
== Executing PPA-CTR 19 (once), V(1)=132336253435
1524286418091 5837627[9]4641072 -264672506406 11 (11)A> 10132336253443
== Executing PA-CTR 13, V(1)=0, V(2)=132336253438, repcount=33084063360, factor=5/4
1921295178411 9121293[9]7483312 474 11165420316801 (11)A> 103
1921295178412 9121293[9]7483314 476 11165420316802 (01)D> 102
1921295178413 9121293[9]7483317 473 11165420316802 <E(10) 00 10
1921295178414 9121293[9]8750525 -330840633131 <E(10) 10165420316802 00 10
1921295178415 9121293[9]8750528 -330840633128 01 (11)F> 10165420316802 00 10
1921295178416 9121293[9]9384132 476 01 11165420316802 (11)F> 00 10
1921295178417 9121293[9]9384134 478 01 11165420316803 (11)B> 10
1921295178418 9121293[9]9384138 480 01 11165420316804 (11)E>
1921295178419 9121293[9]9384140 482 01 11165420316805 (11)A>
1921295178420 9121293[9]9384144 484 01 11165420316806 (01)D>
1921295178421 9121293[9]9384147 481 01 11165420316806 <A(01) 10
1921295178422 9121293[9]9384153 479 01 11165420316805 <B(11) 00 10
1921295178423 9121293[9]0651373 -330840633131 01 <B(11) 01165420316805 00 10
1921295178424 9121293[9]0651380 -330840633128 11 (11)E> 01165420316805 00 10
1921295178425 9121293[9]1284990 482 11165420316806 (11)E> 00 10
1921295178426 9121293[9]1284992 484 11165420316807 (11)A> 10
1921295178427 9121293[9]1284994 486 11165420316808 (01)D>
1921295178428 9121293[9]1284997 483 11165420316808 <A(01) 10
1921295178429 9121293[9]1285003 481 11165420316807 <B(11) 00 10
1921295178430 9121293[9]2552231 -330840633133 <B(11) 01165420316807 00 10
1921295178431 9121293[9]2552239 -330840633135 <E(10) 01165420316808 00 10
1921295178432 9121293[9]2552242 -330840633132 01 (11)F> 01165420316808 00 10
1921295178433 9121293[9]2552244 -330840633130 01 11 (10)C> 01165420316807 00 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 111+V(1) (11)A> 103
1 2 2 112+V(1) (01)D> 102
2 5 -1 112+V(1) <E(10) 00 10
3 13+4*V(1) -5+-2*V(1) <E(10) 102+V(1) 00 10
4 16+4*V(1) -2+-2*V(1) 01 (11)F> 102+V(1) 00 10
5 20+6*V(1) 2 01 112+V(1) (11)F> 00 10
6 22+6*V(1) 4 01 113+V(1) (11)B> 10
7 26+6*V(1) 6 01 114+V(1) (11)E>
8 28+6*V(1) 8 01 115+V(1) (11)A>
9 32+6*V(1) 10 01 116+V(1) (01)D>
10 35+6*V(1) 7 01 116+V(1) <A(01) 10
11 41+6*V(1) 5 01 115+V(1) <B(11) 00 10
12 61+10*V(1) -5+-2*V(1) 01 <B(11) 015+V(1) 00 10
13 68+10*V(1) -2+-2*V(1) 11 (11)E> 015+V(1) 00 10
14 78+12*V(1) 8 116+V(1) (11)E> 00 10
15 80+12*V(1) 10 117+V(1) (11)A> 10
16 82+12*V(1) 12 118+V(1) (01)D>
17 85+12*V(1) 9 118+V(1) <A(01) 10
18 91+12*V(1) 7 117+V(1) <B(11) 00 10
19 119+16*V(1) -7+-2*V(1) <B(11) 017+V(1) 00 10
20 127+16*V(1) -9+-2*V(1) <E(10) 018+V(1) 00 10
21 130+16*V(1) -6+-2*V(1) 01 (11)F> 018+V(1) 00 10
22 132+16*V(1) -4+-2*V(1) 01 11 (10)C> 017+V(1) 00 10
<< Success! ==> defined new CTR 25 (PPA)
1921295178433 9121293[9]2552244 -330840633130 01 11 (10)C> 01165420316807 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=165420316802, repcount=41355079201, factor=5/4
2376201049644 1425202[10]9197108 478 01 11206775396006 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=206775396005
2376201049671 1425202[10]7909422 -413550791538 01 11 (10)C> 01206775396015 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=206775396010, repcount=51693849003, factor=5/4
2944833388704 2226878[10]1595794 486 01 11258469245016 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=258469245015
2944833388731 2226878[10]4986328 -516938489550 01 11 (10)C> 01258469245025 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=258469245020, repcount=64617311256, factor=5/4
3655623812547 3479497[10]2495112 498 01 11323086556281 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=323086556280
3655623812562 3479497[10]7395692 -646173112068 11 (11)A> 10323086556286 01
== Executing PA-CTR 1, V(1)=0, V(2)=323086556281, repcount=80771639071, factor=5/4
4624883481414 5436714[10]5415336 500 11403858195356 (11)A> 102 01
== Executing PPA-CTR 9 (once), V(1)=403858195355
4624883481432 5436714[10]6541118 -807716390214 01 11 (10)C> 01403858195360 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=403858195355, repcount=100964548839, factor=5/4
5735493518661 8494866[10]8639274 498 01 11504822744196 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=504822744195
5735493518676 8494866[10]2546504 -1009645487898 11 (11)A> 10504822744202 01 10
== Executing PA-CTR 5, V(1)=0, V(2)=504822744197, repcount=126205686050, factor=5/4
7249961751276 1327322[11]3947204 502 11631028430251 (11)A> 102 01 10
== Executing PPA-CTR 23 (once), V(1)=631028430250
7249961751294 1327322[11]8831304 -1262056860002 01 11 (10)C> 01631028430255 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=631028430250, repcount=157757107563, factor=5/4
8985289934487 2073942[11]4457516 502 01 11788785537816 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=788785537815
8985289934514 2073942[11]6289650 -1577571075134 01 11 (10)C> 01788785537825 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=788785537820, repcount=197196384456, factor=5/4
11154450163530 3240534[11]5839234 514 01 11985981922281 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=985981922280
11154450163545 3240534[11]6595814 -1971963844052 11 (11)A> 10985981922286 01
== Executing PA-CTR 1, V(1)=0, V(2)=985981922281, repcount=246495480571, factor=5/4
14112395930397 5063335[11]7516458 516 111232477402856 (11)A> 102 01
== Executing PPA-CTR 9 (once), V(1)=1232477402855
14112395930415 5063335[11]5962240 -2464954805198 01 11 (10)C> 011232477402860 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=1232477402855, repcount=308119350714, factor=5/4
17501708788269 7911461[11]3180396 514 01 111540596753571 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=1540596753570
17501708788284 7911461[11]1237626 -3081193506632 11 (11)A> 101540596753577 01 10
== Executing PA-CTR 5, V(1)=0, V(2)=1540596753572, repcount=385149188394, factor=5/4
22123499049012 1236165[12]2620102 520 111925745941971 (11)A> 10 01 10
== Executing PPA-CTR 12 (once), V(1)=1925745941966
22123499049019 1236165[12]6388010 -3851491883422 01 11 (10)C> 011925745941971 00 11 10
== Executing PA-CTR 6, V(1)=0, V(2)=1925745941966, repcount=481436485492, factor=5/4
27419300389431 1931509[12]1356658 514 01 112407182427461 (10)C> 013 00 11 10
27419300389432 1931509[12]1356663 511 01 112407182427461 <B(11) 00 012 00 11 10
27419300389433 1931509[12]1066507 -4814364854411 01 <B(11) 012407182427461 00 012 00 11 10
27419300389434 1931509[12]1066514 -4814364854408 11 (11)E> 012407182427461 00 012 00 11 10
27419300389435 1931509[12]5921436 514 112407182427462 (11)E> 00 012 00 11 10
27419300389436 1931509[12]5921438 516 112407182427463 (11)A> 012 00 11 10
27419300389437 1931509[12]5921440 518 112407182427464 (10)D> 01 00 11 10
27419300389438 1931509[12]5921451 515 112407182427464 <E(10) 10 00 11 10
27419300389439 1931509[12]5631307 -4814364854413 <E(10) 102407182427465 00 11 10
27419300389440 1931509[12]5631310 -4814364854410 01 (11)F> 102407182427465 00 11 10
27419300389441 1931509[12]0486240 520 01 112407182427465 (11)F> 00 11 10
27419300389442 1931509[12]0486242 522 01 112407182427466 (11)B> 11 10
27419300389443 1931509[12]0486249 519 01 112407182427466 <E(10) 102
27419300389444 1931509[12]0196113 -4814364854413 01 <E(10) 102407182427468
27419300389445 1931509[12]0196115 -4814364854415 <A(01) 102407182427469
27419300389446 1931509[12]0196126 -4814364854412 11 (11)A> 102407182427469
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 01 111+V(1) (10)C> 013 00 11 101+V(2)
1 5 -3 01 111+V(1) <B(11) 00 012 00 11 101+V(2)
2 9+4*V(1) -5+-2*V(1) 01 <B(11) 011+V(1) 00 012 00 11 101+V(2)
3 16+4*V(1) -2+-2*V(1) 11 (11)E> 011+V(1) 00 012 00 11 101+V(2)
4 18+6*V(1) 0 112+V(1) (11)E> 00 012 00 11 101+V(2)
5 20+6*V(1) 2 113+V(1) (11)A> 012 00 11 101+V(2)
6 22+6*V(1) 4 114+V(1) (10)D> 01 00 11 101+V(2)
7 33+6*V(1) 1 114+V(1) <E(10) 10 00 11 101+V(2)
8 49+10*V(1) -7+-2*V(1) <E(10) 105+V(1) 00 11 101+V(2)
9 52+10*V(1) -4+-2*V(1) 01 (11)F> 105+V(1) 00 11 101+V(2)
10 62+12*V(1) 6 01 115+V(1) (11)F> 00 11 101+V(2)
11 64+12*V(1) 8 01 116+V(1) (11)B> 11 101+V(2)
12 71+12*V(1) 5 01 116+V(1) <E(10) 102+V(2)
13 95+16*V(1) -7+-2*V(1) 01 <E(10) 108+V(1)+V(2)
14 97+16*V(1) -9+-2*V(1) <A(01) 109+V(1)+V(2)
15 108+16*V(1) -6+-2*V(1) 11 (11)A> 109+V(1)+V(2)
<< Success! ==> defined new CTR 26 (PPA)
27419300389446 1931509[12]0196126 -4814364854412 11 (11)A> 102407182427469
== Executing PA-CTR 13, V(1)=0, V(2)=2407182427464, repcount=601795606867, factor=5/4
34640847671850 3017982[12]7500274 524 113008978034336 (11)A> 10
34640847671851 3017982[12]7500276 526 113008978034337 (01)D>
34640847671852 3017982[12]7500279 523 113008978034337 <A(01) 10
34640847671853 3017982[12]7500285 521 113008978034336 <B(11) 00 10
34640847671854 3017982[12]9637629 -6017956068151 <B(11) 013008978034336 00 10
34640847671855 3017982[12]9637637 -6017956068153 <E(10) 013008978034337 00 10
34640847671856 3017982[12]9637640 -6017956068150 01 (11)F> 013008978034337 00 10
34640847671857 3017982[12]9637642 -6017956068148 01 11 (10)C> 013008978034336 00 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 115+V(1) (11)A> 10
1 2 2 116+V(1) (01)D>
2 5 -1 116+V(1) <A(01) 10
3 11 -3 115+V(1) <B(11) 00 10
4 31+4*V(1) -13+-2*V(1) <B(11) 015+V(1) 00 10
5 39+4*V(1) -15+-2*V(1) <E(10) 016+V(1) 00 10
6 42+4*V(1) -12+-2*V(1) 01 (11)F> 016+V(1) 00 10
7 44+4*V(1) -10+-2*V(1) 01 11 (10)C> 015+V(1) 00 10
<< Success! ==> defined new CTR 27 (PPA)
34640847671857 3017982[12]9637642 -6017956068148 01 11 (10)C> 013008978034336 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=3008978034331, repcount=752244508583, factor=5/4
42915537266270 4715598[12]2966134 516 01 113761222542916 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=3761222542915
42915537266285 4715598[12]3652884 -7522445085320 11 (11)A> 103761222542922 01 10
== Executing PA-CTR 5, V(1)=0, V(2)=3761222542917, repcount=940305635730, factor=5/4
54199204895045 7368122[12]4254704 520 114701528178651 (11)A> 102 01 10
== Executing PPA-CTR 23 (once), V(1)=4701528178650
54199204895063 7368122[12]5113204 -9403056356784 01 11 (10)C> 014701528178655 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=4701528178650, repcount=1175382044663, factor=5/4
67128407386356 1151269[13]8138816 520 01 115876910223316 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=5876910223315
67128407386383 1151269[13]3051950 -11753820446116 01 11 (10)C> 015876910223325 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=5876910223320, repcount=1469227555831, factor=5/4
83289910500524 1798858[13]2967034 532 01 117346137779156 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=7346137779155
83289910500539 1798858[13]7433614 -14692275557784 11 (11)A> 107346137779161 01
== Executing PA-CTR 1, V(1)=0, V(2)=7346137779156, repcount=1836534444790, factor=5/4
105328323838019 2810715[13]2879474 536 119182672223951 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=9182672223946
105328323838026 2810715[13]1775302 -18365344447366 01 11 (10)C> 019182672223951 00 11
== Executing PA-CTR 2, V(1)=0, V(2)=9182672223946, repcount=2295668055987, factor=5/4
130580672453883 4391743[13]2003930 530 01 1111478340279936 (10)C> 013 00 11
== Executing PPA-CTR 19 (once), V(1)=11478340279935
130580672453898 4391743[13]6482998 -22956680559346 11 (11)A> 1011478340279943
== Executing PA-CTR 13, V(1)=0, V(2)=11478340279938, repcount=2869585069985, factor=5/4
165015693293718 6862098[13]5869238 534 1114347925349926 (11)A> 103
== Executing PPA-CTR 25 (once), V(1)=14347925349925
165015693293740 6862098[13]1468170 -28695850699320 01 11 (10)C> 0114347925349932 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=14347925349927, repcount=3586981337482, factor=5/4
204472488006042 1072202[14]9952278 536 01 1117934906687411 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=17934906687410
204472488006057 1072202[14]6950948 -35869813374290 11 (11)A> 1017934906687417 01 10
== Executing PA-CTR 5, V(1)=0, V(2)=17934906687412, repcount=4483726671854, factor=5/4
258277208068305 1675317[14]7713464 542 1122418633359271 (11)A> 10 01 10
== Executing PPA-CTR 12 (once), V(1)=22418633359266
258277208068312 1675317[14]1150572 -44837266718000 01 11 (10)C> 0122418633359271 00 11 10
== Executing PA-CTR 6, V(1)=0, V(2)=22418633359266, repcount=5604658339817, factor=5/4
319928449806299 2617682[14]2509020 536 01 1128023291699086 (10)C> 013 00 11 10
== Executing PPA-CTR 26 (once), V(1)=28023291699085, V(2)=0
319928449806314 2617682[14]9694488 -56046583397640 11 (11)A> 1028023291699094
== Executing PA-CTR 13, V(1)=0, V(2)=28023291699089, repcount=7005822924773, factor=5/4
403998324903590 4090129[14]2182640 544 1135029114623866 (11)A> 102
== Executing PPA-CTR 14 (once), V(1)=35029114623864
403998324903600 4090129[14]8421348 -70058229247190 11 (11)A> 1035029114623869 01
== Executing PA-CTR 1, V(1)=0, V(2)=35029114623864, repcount=8757278655967, factor=5/4
509085668775204 6390827[14]3876896 546 1143786393279836 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=43786393279831
509085668775211 6390827[14]6996264 -87572786559126 01 11 (10)C> 0143786393279836 00 11
== Executing PA-CTR 2, V(1)=0, V(2)=43786393279831, repcount=10946598319958, factor=5/4
629498250294749 9985667[14]3527756 538 01 1154732991599791 (10)C> 014 00 11
== Executing PPA-CTR 11 (once), V(1)=54732991599790
629498250294764 9985667[14]9124506 -109465983199048 11 (11)A> 1054732991599797 01 11
== Executing PA-CTR 5, V(1)=0, V(2)=54732991599792, repcount=13683247899949, factor=5/4
793697225094152 1560260[15]3800802 544 1168416239499746 (11)A> 10 01 11
== Executing PPA-CTR 12 (once), V(1)=68416239499741
793697225094159 1560260[15]1799810 -136832478998948 01 11 (10)C> 0168416239499746 00 11 11
== Executing PA-CTR 6, V(1)=0, V(2)=68416239499741, repcount=17104059874936, factor=5/4
981841883718455 2437907[15]7670514 540 01 1185520299374681 (10)C> 012 00 11 11
981841883718456 2437907[15]7670519 537 01 1185520299374681 <B(11) 00 01 00 11 11
981841883718457 2437907[15]5169243 -171040598748825 01 <B(11) 0185520299374681 00 01 00 11 11
981841883718458 2437907[15]5169250 -171040598748822 11 (11)E> 0185520299374681 00 01 00 11 11
981841883718459 2437907[15]3918612 540 1185520299374682 (11)E> 00 01 00 11 11
981841883718460 2437907[15]3918614 542 1185520299374683 (11)A> 01 00 11 11
981841883718461 2437907[15]3918616 544 1185520299374684 (10)D> 00 11 11
981841883718462 2437907[15]3918620 546 1185520299374685 (11)F> 11 11
981841883718463 2437907[15]3918629 543 1185520299374685 <E(10) 10 11
981841883718464 2437907[15]1417369 -171040598748827 <E(10) 1085520299374686 11
981841883718465 2437907[15]1417372 -171040598748824 01 (11)F> 1085520299374686 11
981841883718466 2437907[15]0166744 548 01 1185520299374686 (11)F> 11
981841883718467 2437907[15]0166753 545 01 1185520299374686 <E(10) 10
981841883718468 2437907[15]7665497 -171040598748827 01 <E(10) 1085520299374687
981841883718469 2437907[15]7665499 -171040598748829 <A(01) 1085520299374688
981841883718470 2437907[15]7665510 -171040598748826 11 (11)A> 1085520299374688
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 111+V(1) (10)C> 012 00 11 11
1 5 -3 01 111+V(1) <B(11) 00 01 00 11 11
2 9+4*V(1) -5+-2*V(1) 01 <B(11) 011+V(1) 00 01 00 11 11
3 16+4*V(1) -2+-2*V(1) 11 (11)E> 011+V(1) 00 01 00 11 11
4 18+6*V(1) 0 112+V(1) (11)E> 00 01 00 11 11
5 20+6*V(1) 2 113+V(1) (11)A> 01 00 11 11
6 22+6*V(1) 4 114+V(1) (10)D> 00 11 11
7 26+6*V(1) 6 115+V(1) (11)F> 11 11
8 35+6*V(1) 3 115+V(1) <E(10) 10 11
9 55+10*V(1) -7+-2*V(1) <E(10) 106+V(1) 11
10 58+10*V(1) -4+-2*V(1) 01 (11)F> 106+V(1) 11
11 70+12*V(1) 8 01 116+V(1) (11)F> 11
12 79+12*V(1) 5 01 116+V(1) <E(10) 10
13 103+16*V(1) -7+-2*V(1) 01 <E(10) 107+V(1)
14 105+16*V(1) -9+-2*V(1) <A(01) 108+V(1)
15 116+16*V(1) -6+-2*V(1) 11 (11)A> 108+V(1)
<< Success! ==> defined new CTR 28 (PPA)
981841883718470 2437907[15]7665510 -171040598748826 11 (11)A> 1085520299374688
== Executing PA-CTR 13, V(1)=0, V(2)=85520299374683, repcount=21380074843671, factor=5/4
1238402781842522 3809230[15]5037554 542 11106900374218356 (11)A> 104
== Executing PPA-CTR 20 (once), V(1)=106900374218355
1238402781842541 3809230[15]2531348 -213800748436172 01 11 (10)C> 01106900374218361 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=106900374218356, repcount=26725093554590, factor=5/4
1532378810943031 5951921[15]5430408 548 01 11133625467772951 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=133625467772950
1532378810943046 5951921[15]9797708 -267250935545358 11 (11)A> 10133625467772956 01
== Executing PA-CTR 1, V(1)=0, V(2)=133625467772951, repcount=33406366943238, factor=5/4
1933255214261902 9299877[15]3607120 546 11167031834716191 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=167031834716190
1933255214261926 9299877[15]7363504 -334063669431840 11 (11)A> 10167031834716201 01
== Executing PA-CTR 1, V(1)=0, V(2)=167031834716196, repcount=41757958679050, factor=5/4
2434350718410526 1453105[16]9526204 560 11208789793395251 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=208789793395246
2434350718410533 1453105[16]3107232 -417579586789942 01 11 (10)C> 01208789793395251 00 11
== Executing PA-CTR 2, V(1)=0, V(2)=208789793395246, repcount=52197448348812, factor=5/4
3008522650247465 2270478[16]1307160 554 01 11260987241744061 (10)C> 013 00 11
== Executing PPA-CTR 19 (once), V(1)=260987241744060
3008522650247480 2270478[16]9212228 -521974483487572 11 (11)A> 10260987241744068
== Executing PA-CTR 13, V(1)=0, V(2)=260987241744063, repcount=65246810436016, factor=5/4
3791484375479672 3547621[16]2604452 556 11326234052180081 (11)A> 104
== Executing PPA-CTR 20 (once), V(1)=326234052180080
3791484375479691 3547621[16]7485846 -652468104359608 01 11 (10)C> 01326234052180086 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=326234052180081, repcount=81558513045021, factor=5/4
4688628018974922 5543159[16]7729790 560 01 11407792565225106 (10)C> 012 00 10
== Executing PPA-CTR 3 (once), V(1)=407792565225105, V(2)=0
4688628018974940 5543159[16]1331612 -815585130449656 11 (11)A> 10407792565225114 01
== Executing PA-CTR 1, V(1)=0, V(2)=407792565225109, repcount=101948141306278, factor=5/4
5912005714650276 8661186[16]2143584 568 11509740706531391 (11)A> 102 01
== Executing PPA-CTR 9 (once), V(1)=509740706531390
5912005714650294 8661186[16]6645926 -1019481413062216 01 11 (10)C> 01509740706531395 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=509740706531390, repcount=127435176632848, factor=5/4
7313792657611622 1353310[17]9895878 568 01 11637175883164241 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=637175883164240
7313792657611649 1353310[17]9509362 -1274351766327918 01 11 (10)C> 01637175883164250 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=637175883164245, repcount=159293970791062, factor=5/4
9066026336313331 2114547[17]9040790 578 01 11796469853955311 (10)C> 012 00 10
== Executing PPA-CTR 3 (once), V(1)=796469853955310, V(2)=0
9066026336313349 2114547[17]2325892 -1592939707910048 11 (11)A> 10796469853955319 01
== Executing PA-CTR 1, V(1)=0, V(2)=796469853955314, repcount=199117463488829, factor=5/4
11455435898179297 3303980[17]4683308 584 11995587317444146 (11)A> 103 01
== Executing PPA-CTR 4 (once), V(1)=995587317444145, V(2)=0
11455435898179320 3303980[17]3789772 -1991174634887710 01 11 (10)C> 01995587317444153 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=995587317444148, repcount=248896829361038, factor=5/4
14193301021150738 5162469[17]5188384 594 01 111244484146805191 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=1244484146805190
14193301021150753 5162469[17]4071524 -2488968293609792 11 (11)A> 101244484146805196 01
== Executing PA-CTR 1, V(1)=0, V(2)=1244484146805191, repcount=311121036701298, factor=5/4
17926753461566329 8066358[17]8459776 592 111555605183506491 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=1555605183506490
17926753461566353 8066358[17]5602760 -3111210367012394 11 (11)A> 101555605183506501 01
== Executing PA-CTR 1, V(1)=0, V(2)=1555605183506496, repcount=388901295876625, factor=5/4
22593569012085853 1260368[18]7126760 606 111944506479383126 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=1944506479383121
22593569012085860 1260368[18]4659288 -3889012958765646 01 11 (10)C> 011944506479383126 00 11
== Executing PA-CTR 2, V(1)=0, V(2)=1944506479383121, repcount=486126619845781, factor=5/4
27940961830389451 1969325[18]4414672 602 01 112430633099228906 (10)C> 012 00 11
27940961830389452 1969325[18]4414677 599 01 112430633099228906 <B(11) 00 01 00 11
27940961830389453 1969325[18]1330301 -4861266198457213 01 <B(11) 012430633099228906 00 01 00 11
27940961830389454 1969325[18]1330308 -4861266198457210 11 (11)E> 012430633099228906 00 01 00 11
27940961830389455 1969325[18]9788120 602 112430633099228907 (11)E> 00 01 00 11
27940961830389456 1969325[18]9788122 604 112430633099228908 (11)A> 01 00 11
27940961830389457 1969325[18]9788124 606 112430633099228909 (10)D> 00 11
27940961830389458 1969325[18]9788128 608 112430633099228910 (11)F> 11
27940961830389459 1969325[18]9788137 605 112430633099228910 <E(10) 10
27940961830389460 1969325[18]6703777 -4861266198457215 <E(10) 102430633099228911
27940961830389461 1969325[18]6703780 -4861266198457212 01 (11)F> 102430633099228911
27940961830389462 1969325[18]5161602 610 01 112430633099228911 (11)F>
27940961830389463 1969325[18]5161604 612 01 112430633099228912 (11)B>
27940961830389464 1969325[18]5161615 609 01 112430633099228912 <E(10) 01
27940961830389465 1969325[18]2077263 -4861266198457215 01 <E(10) 102430633099228912 01
27940961830389466 1969325[18]2077265 -4861266198457217 <A(01) 102430633099228913 01
27940961830389467 1969325[18]2077276 -4861266198457214 11 (11)A> 102430633099228913 01
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 111+V(1) (10)C> 012 00 11
1 5 -3 01 111+V(1) <B(11) 00 01 00 11
2 9+4*V(1) -5+-2*V(1) 01 <B(11) 011+V(1) 00 01 00 11
3 16+4*V(1) -2+-2*V(1) 11 (11)E> 011+V(1) 00 01 00 11
4 18+6*V(1) 0 112+V(1) (11)E> 00 01 00 11
5 20+6*V(1) 2 113+V(1) (11)A> 01 00 11
6 22+6*V(1) 4 114+V(1) (10)D> 00 11
7 26+6*V(1) 6 115+V(1) (11)F> 11
8 35+6*V(1) 3 115+V(1) <E(10) 10
9 55+10*V(1) -7+-2*V(1) <E(10) 106+V(1)
10 58+10*V(1) -4+-2*V(1) 01 (11)F> 106+V(1)
11 70+12*V(1) 8 01 116+V(1) (11)F>
12 72+12*V(1) 10 01 117+V(1) (11)B>
13 83+12*V(1) 7 01 117+V(1) <E(10) 01
14 111+16*V(1) -7+-2*V(1) 01 <E(10) 107+V(1) 01
15 113+16*V(1) -9+-2*V(1) <A(01) 108+V(1) 01
16 124+16*V(1) -6+-2*V(1) 11 (11)A> 108+V(1) 01
<< Success! ==> defined new CTR 29 (PPA)
27940961830389467 1969325[18]2077276 -4861266198457214 11 (11)A> 102430633099228913 01
== Executing PA-CTR 1, V(1)=0, V(2)=2430633099228908, repcount=607658274807228, factor=5/4
35232861128076203 3077071[18]6842548 610 113038291374036141 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=3038291374036136
35232861128076210 3077071[18]2987136 -6076582748071672 01 11 (10)C> 013038291374036141 00 11
== Executing PA-CTR 2, V(1)=0, V(2)=3038291374036136, repcount=759572843509035, factor=5/4
43588162406675595 4807924[18]1231076 608 01 113797864217545176 (10)C> 01 00 11
== Executing PPA-CTR 17 (once), V(1)=3797864217545175
43588162406675610 4807924[18]1953974 -7595728435089748 11 (11)A> 103797864217545181 01
== Executing PA-CTR 1, V(1)=0, V(2)=3797864217545176, repcount=949466054386295, factor=5/4
54981755059311150 7512381[18]5898754 612 114747330271931476 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=4747330271931471
54981755059311157 7512381[18]3624682 -9494660543862340 01 11 (10)C> 014747330271931476 00 11
== Executing PA-CTR 2, V(1)=0, V(2)=4747330271931471, repcount=1186832567982868, factor=5/4
68036913307122705 1173809[19]0204914 604 01 115934162839914341 (10)C> 014 00 11
== Executing PPA-CTR 11 (once), V(1)=5934162839914340
68036913307122720 1173809[19]8834464 -118683[4]9828082 11 (11)A> 105934162839914347 01 11
== Executing PA-CTR 5, V(1)=0, V(2)=5934162839914342, repcount=1483540709978586, factor=5/4
85839401826865752 1834077[19]4888268 606 117417703549892931 (11)A> 103 01 11
== Executing PPA-CTR 24 (once), V(1)=7417703549892930, V(2)=0
85839401826865772 1834077[19]3175280 -148354[4]9785258 01 11 (10)C> 017417703549892938 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=7417703549892933, repcount=1854425887473234, factor=5/4
1062380[4]9071346 2865746[19]9827916 614 01 119272129437366171 (10)C> 012 00 10
== Executing PPA-CTR 3 (once), V(1)=9272129437366170, V(2)=0
1062380[4]9071364 2865746[19]7686778 -185442[4]4731732 11 (11)A> 109272129437366179 01
== Executing PA-CTR 1, V(1)=0, V(2)=9272129437366174, repcount=2318032359341544, factor=5/4
1340544[4]1169892 4477728[19]4417354 620 1111590161796707721 (11)A> 103 01
== Executing PPA-CTR 4 (once), V(1)=11590161796707720, V(2)=0
1340544[4]1169915 4477728[19]1741018 -231803[4]3414824 01 11 (10)C> 0111590161796707728 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=11590161796707723, repcount=2897540449176931, factor=5/4
1659274[4]2116156 6996450[19]1119502 624 01 1114487702245884656 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=14487702245884655
1659274[4]2116171 6996450[19]5274092 -289754[4]1768692 11 (11)A> 1014487702245884662 01 10
== Executing PA-CTR 5, V(1)=0, V(2)=14487702245884657, repcount=3621925561471165, factor=5/4
2093905[4]9770151 1093195[20]9010452 628 1118109627807355826 (11)A> 102 01 10
== Executing PPA-CTR 23 (once), V(1)=18109627807355825
2093905[4]9770169 1093195[20]6703752 -362192[4]4711026 01 11 (10)C> 0118109627807355830 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=18109627807355825, repcount=4527406951838957, factor=5/4
2591920[4]9998696 1708117[20]4663760 630 01 1122637034759194786 (10)C> 012 00 10
== Executing PPA-CTR 3 (once), V(1)=22637034759194785, V(2)=0
2591920[4]9998714 1708117[20]1780462 -452740[4]8388946 11 (11)A> 1022637034759194794 01
== Executing PA-CTR 1, V(1)=0, V(2)=22637034759194789, repcount=5659258689798698, factor=5/4
3271031[4]7583090 2668934[20]9792314 638 1128296293448993491 (11)A> 102 01
== Executing PPA-CTR 9 (once), V(1)=28296293448993490
3271031[4]7583108 2668934[20]3688256 -565925[4]7986346 01 11 (10)C> 0128296293448993495 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=28296293448993490, repcount=7074073362248373, factor=5/4
4049179[4]2315211 4170209[20]4546808 638 01 1135370366811241866 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=35370366811241865
4049179[4]2315238 4170209[20]1868042 -707407[4]2483098 01 11 (10)C> 0135370366811241875 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=35370366811241870, repcount=8842591702810468, factor=5/4
5021864[4]3230386 6515952[20]8794674 646 01 1144212958514052341 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=44212958514052340
5021864[4]3230413 6515952[20]7946358 -884259[4]8104040 01 11 (10)C> 0144212958514052350 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=44212958514052345, repcount=11053239628513087, factor=5/4
6237720[4]6874370 1018117[21]5478386 656 01 1155266198142565436 (10)C> 012 00 10
== Executing PPA-CTR 3 (once), V(1)=55266198142565435, V(2)=0
6237720[4]6874388 1018117[21]6525488 -110532[5]5130220 11 (11)A> 1055266198142565444 01
== Executing PA-CTR 1, V(1)=0, V(2)=55266198142565439, repcount=13816549535641360, factor=5/4
7895706[4]4570708 1590808[21]7819728 660 1169082747678206801 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=69082747678206800
7895706[4]4570732 1590808[21]8369532 -138165[5]6412946 11 (11)A> 1069082747678206811 01
== Executing PA-CTR 1, V(1)=0, V(2)=69082747678206806, repcount=17270686919551702, factor=5/4
9968188[4]9191156 2485638[21]6031520 670 1186353434597758511 (11)A> 103 01
== Executing PPA-CTR 4 (once), V(1)=86353434597758510, V(2)=0
9968188[4]9191179 2485638[21]0167824 -172706[5]5516354 01 11 (10)C> 0186353434597758518 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=86353434597758513, repcount=21588358649439629, factor=5/4
1234290[5]3027098 3883810[21]0844440 678 01 111079417[4]7198146 (10)C> 012 00 10
== Executing PPA-CTR 3 (once), V(1)=1079417[4]7198145, V(2)=0
1234290[5]3027116 3883810[21]6014902 -215883[5]4395618 11 (11)A> 101079417[4]7198154 01
== Executing PA-CTR 1, V(1)=0, V(2)=1079417[4]7198149, repcount=26985448311799538, factor=5/4
1558116[5]4621572 6068453[21]7602514 686 111349272[4]8997691 (11)A> 102 01
== Executing PPA-CTR 9 (once), V(1)=1349272[4]8997690
1558116[5]4621590 6068453[21]1565656 -269854[5]7994698 01 11 (10)C> 011349272[4]8997695 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=1349272[4]8997690, repcount=33731810389749423, factor=5/4
1929166[5]1865243 9481958[21]8033908 686 01 111686590[4]8747116 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=1686590[4]8747115
1929166[5]1865270 9481958[21]0470642 -337318[5]7493550 01 11 (10)C> 011686590[4]8747125 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=1686590[4]8747120, repcount=42164762987186781, factor=5/4
2392978[5]0919861 1481556[22]9080026 698 01 112108238[4]5933906 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=2108238[4]5933905
2392978[5]0919876 1481556[22]4022606 -421647[5]1867118 11 (11)A> 102108238[4]5933911 01
== Executing PA-CTR 1, V(1)=0, V(2)=2108238[4]5933906, repcount=52705953733983477, factor=5/4
3025449[5]8721600 2314931[22]9746694 698 112635297[4]9917386 (11)A> 103 01
== Executing PPA-CTR 4 (once), V(1)=2635297[4]9917385, V(2)=0
3025449[5]8721623 2314931[22]8424998 -527059[5]9834076 01 11 (10)C> 012635297[4]9917393 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=2635297[4]9917388, repcount=65882442167479348, factor=5/4
3750156[5]0994451 3617080[22]7875950 708 01 113294122[4]7396741 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=3294122[4]7396740
3750156[5]0994466 3617080[22]6223890 -658824[5]4792778 11 (11)A> 103294122[4]7396746 01
== Executing PA-CTR 1, V(1)=0, V(2)=3294122[4]7396741, repcount=82353052709349186, factor=5/4
4738393[5]3184698 5651687[22]9974094 710 114117652[4]6745931 (11)A> 102 01
== Executing PPA-CTR 9 (once), V(1)=4117652[4]6745930
4738393[5]3184716 5651687[22]7909076 -823530[5]3491154 01 11 (10)C> 014117652[4]6745935 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=4117652[4]6745930, repcount=1029413[4]6686483, factor=5/4
5870747[5]6736029 8830762[22]2528168 710 01 115147065[4]3432416 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=5147065[4]3432415
5870747[5]6736056 8830762[22]8041502 -102941[6]6864126 01 11 (10)C> 015147065[4]3432425 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=5147065[4]3432420, repcount=1286766[4]8358106, factor=5/4
7286191[5]8675222 1379806[23]9434186 722 01 116433832[4]1790531 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=6433832[4]1790530
7286191[5]8675237 1379806[23]8082766 -128676[6]3580344 11 (11)A> 106433832[4]1790536 01
== Executing PA-CTR 1, V(1)=0, V(2)=6433832[4]1790531, repcount=1608458[4]2947633, factor=5/4
9216340[5]4046833 2155947[23]7382958 720 118042290[4]4738166 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=8042290[4]4738165
9216340[5]4046857 2155947[23]1622792 -160845[6]9475616 11 (11)A> 108042290[4]4738176 01
== Executing PA-CTR 1, V(1)=0, V(2)=8042290[4]4738171, repcount=2010572[4]1184543, factor=5/4
1162902[6]8261373 3368668[23]5462724 728 111005286[5]5922716 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=1005286[5]5922715
1162902[6]8261397 3368668[23]5762658 -201057[6]1844708 11 (11)A> 101005286[5]5922726 01
== Executing PA-CTR 1, V(1)=0, V(2)=1005286[5]5922721, repcount=2513215[4]8980681, factor=5/4
1464488[6]6029569 5263544[23]7818642 740 111256607[5]4903406 (11)A> 102 01
== Executing PPA-CTR 9 (once), V(1)=1256607[5]4903405
1464488[6]6029587 5263544[23]6273224 -251321[6]9806074 01 11 (10)C> 011256607[5]4903410 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=1256607[5]4903405, repcount=3141519[4]6225852, factor=5/4
1810055[6]4513959 8224288[23]1729312 742 01 111570759[5]1129261 (10)C> 012 00 10
== Executing PPA-CTR 3 (once), V(1)=1570759[5]1129260, V(2)=0
1810055[6]4513977 8224288[23]9797614 -314151[6]2257784 11 (11)A> 101570759[5]1129269 01
== Executing PA-CTR 1, V(1)=0, V(2)=1570759[5]1129264, repcount=3926899[4]2782317, factor=5/4
2281283[6]7901781 1285045[24]1051062 752 111963449[5]3911586 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=1963449[5]3911581
2281283[6]7901788 1285045[24]6697430 -392689[6]7822420 01 11 (10)C> 011963449[5]3911586 00 11
== Executing PA-CTR 2, V(1)=0, V(2)=1963449[5]3911581, repcount=4908624[4]0977896, factor=5/4
2821232[6]8658644 2007882[24]7550374 748 01 112454312[5]4889481 (10)C> 012 00 11
== Executing PPA-CTR 29 (once), V(1)=2454312[5]4889480
2821232[6]8658660 2007882[24]5782178 -490862[6]9778218 11 (11)A> 102454312[5]4889488 01
== Executing PA-CTR 1, V(1)=0, V(2)=2454312[5]4889483, repcount=6135780[4]3722371, factor=5/4
3557526[6]3327112 3137316[24]8192022 750 113067890[5]8611856 (11)A> 104 01
== Executing PPA-CTR 8 (once), V(1)=3067890[5]8611855
3557526[6]3327136 3137316[24]7653036 -613578[6]7222966 11 (11)A> 103067890[5]8611866 01
== Executing PA-CTR 1, V(1)=0, V(2)=3067890[5]8611861, repcount=7669725[4]7152966, factor=5/4
4477893[6]9162728 4902057[24]8768560 762 113834862[5]5764831 (11)A> 102 01
== Executing PPA-CTR 9 (once), V(1)=3834862[5]5764830
4477893[6]9162746 4902057[24]1005942 -766972[6]1528902 01 11 (10)C> 013834862[5]5764835 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=3834862[5]5764830, repcount=9587157[4]8941208, factor=5/4
5532480[6]7516034 7659465[24]9984934 762 01 114793578[5]4706041 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=4793578[5]4706040
5532480[6]7516061 7659465[24]3518018 -958715[6]9411324 01 11 (10)C> 014793578[5]4706050 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=4793578[5]4706045, repcount=1198394[5]3676512, factor=5/4
6850714[6]7957693 1196791[25]3103746 772 01 115991973[5]8382561 (10)C> 012 00 10
== Executing PPA-CTR 3 (once), V(1)=5991973[5]8382560, V(2)=0
6850714[6]7957711 1196791[25]7224848 -119839[7]6764354 11 (11)A> 105991973[5]8382569 01
== Executing PA-CTR 1, V(1)=0, V(2)=5991973[5]8382564, repcount=1497993[5]9595642, factor=5/4
8648306[6]3105415 1869986[25]5241596 782 117489966[5]7978211 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=7489966[5]7978206
8648306[6]3105422 1869986[25]7154464 -149799[7]5955640 01 11 (10)C> 017489966[5]7978211 00 11
== Executing PA-CTR 2, V(1)=0, V(2)=7489966[5]7978206, repcount=1872491[5]9494552, factor=5/4
1070804[7]7545494 2921854[25]0390352 776 01 119362458[5]7472761 (10)C> 013 00 11
== Executing PPA-CTR 19 (once), V(1)=9362458[5]7472760
1070804[7]7545509 2921854[25]9954620 -187249[7]4944750 11 (11)A> 109362458[5]7472768
== Executing PA-CTR 13, V(1)=0, V(2)=9362458[5]7472763, repcount=2340614[5]1868191, factor=5/4
1351678[7]9963801 4565397[25]1847544 778 111170307[6]9340956 (11)A> 104
== Executing PPA-CTR 20 (once), V(1)=1170307[6]9340955
1351678[7]9963820 4565397[25]1302938 -234061[7]8681136 01 11 (10)C> 011170307[6]9340961 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=1170307[6]9340956, repcount=2925768[5]4835240, factor=5/4
1673512[7]3151460 7133432[25]1429098 784 01 111462884[6]4176201 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=1462884[6]4176200
1673512[7]3151475 7133432[25]8248398 -292576[7]8351622 11 (11)A> 101462884[6]4176206 01
== Executing PA-CTR 1, V(1)=0, V(2)=1462884[6]4176201, repcount=3657210[5]3544051, factor=5/4
2112378[7]5680087 1114598[26]3464162 786 111828605[6]7720256 (11)A> 102 01
== Executing PPA-CTR 9 (once), V(1)=1828605[6]7720255
2112378[7]5680105 1114598[26]6988344 -365721[7]5439728 01 11 (10)C> 011828605[6]7720260 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=1828605[6]7720255, repcount=4571512[5]4430064, factor=5/4
2615244[7]4410809 1741560[26]8933400 784 01 112285756[6]2150321 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=2285756[6]2150320
2615244[7]4410824 1741560[26]3338630 -457151[7]4299862 11 (11)A> 102285756[6]2150327 01 10
== Executing PA-CTR 5, V(1)=0, V(2)=2285756[6]2150322, repcount=5714390[5]0537581, factor=5/4
3300971[7]0861796 2721188[26]1563214 786 112857195[6]2687906 (11)A> 103 01 10
== Executing PPA-CTR 18 (once), V(1)=2857195[6]2687905, V(2)=0
3300971[7]0861816 2721188[26]4569820 -571439[7]5375028 01 11 (10)C> 012857195[6]2687912 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=2857195[6]2687907, repcount=7142988[5]3171977, factor=5/4
4086700[7]5753563 4251857[26]5072908 788 01 113571494[6]5859886 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=3571494[6]5859885
4086700[7]5753578 4251857[26]8831178 -714298[7]1718988 11 (11)A> 103571494[6]5859892 01 10
== Executing PA-CTR 5, V(1)=0, V(2)=3571494[6]5859887, repcount=8928735[5]8964972, factor=5/4
5158148[7]3333242 6643527[26]2463746 788 114464367[6]4824861 (11)A> 104 01 10
5158148[7]3333243 6643527[26]2463748 790 114464367[6]4824862 (01)D> 103 01 10
5158148[7]3333244 6643527[26]2463751 787 114464367[6]4824862 <E(10) 00 102 01 10
5158148[7]3333245 6643527[26]1763199 -892873[7]9648937 <E(10) 104464367[6]4824862 00 102 01 10
5158148[7]3333246 6643527[26]1763202 -892873[7]9648934 01 (11)F> 104464367[6]4824862 00 102 01 10
5158148[7]3333247 6643527[26]1412926 790 01 114464367[6]4824862 (11)F> 00 102 01 10
5158148[7]3333248 6643527[26]1412928 792 01 114464367[6]4824863 (11)B> 102 01 10
5158148[7]3333249 6643527[26]1412932 794 01 114464367[6]4824864 (11)E> 10 01 10
5158148[7]3333250 6643527[26]1412937 791 01 114464367[6]4824864 <B(11) 00 01 10
5158148[7]3333251 6643527[26]0712393 -892873[7]9648937 01 <B(11) 014464367[6]4824864 00 01 10
5158148[7]3333252 6643527[26]0712400 -892873[7]9648934 11 (11)E> 014464367[6]4824864 00 01 10
5158148[7]3333253 6643527[26]0362128 794 114464367[6]4824865 (11)E> 00 01 10
5158148[7]3333254 6643527[26]0362130 796 114464367[6]4824866 (11)A> 01 10
5158148[7]3333255 6643527[26]0362132 798 114464367[6]4824867 (10)D> 10
5158148[7]3333256 6643527[26]0362135 795 114464367[6]4824867 <B(11)
5158148[7]3333257 6643527[26]9661603 -892873[7]9648939 <B(11) 014464367[6]4824867
5158148[7]3333258 6643527[26]9661611 -892873[7]9648941 <E(10) 014464367[6]4824868
5158148[7]3333259 6643527[26]9661614 -892873[7]9648938 01 (11)F> 014464367[6]4824868
5158148[7]3333260 6643527[26]9661616 -892873[7]9648936 01 11 (10)C> 014464367[6]4824867
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 111+V(1) (11)A> 104 01 10
1 2 2 112+V(1) (01)D> 103 01 10
2 5 -1 112+V(1) <E(10) 00 102 01 10
3 13+4*V(1) -5+-2*V(1) <E(10) 102+V(1) 00 102 01 10
4 16+4*V(1) -2+-2*V(1) 01 (11)F> 102+V(1) 00 102 01 10
5 20+6*V(1) 2 01 112+V(1) (11)F> 00 102 01 10
6 22+6*V(1) 4 01 113+V(1) (11)B> 102 01 10
7 26+6*V(1) 6 01 114+V(1) (11)E> 10 01 10
8 31+6*V(1) 3 01 114+V(1) <B(11) 00 01 10
9 47+10*V(1) -5+-2*V(1) 01 <B(11) 014+V(1) 00 01 10
10 54+10*V(1) -2+-2*V(1) 11 (11)E> 014+V(1) 00 01 10
11 62+12*V(1) 6 115+V(1) (11)E> 00 01 10
12 64+12*V(1) 8 116+V(1) (11)A> 01 10
13 66+12*V(1) 10 117+V(1) (10)D> 10
14 69+12*V(1) 7 117+V(1) <B(11)
15 97+16*V(1) -7+-2*V(1) <B(11) 017+V(1)
16 105+16*V(1) -9+-2*V(1) <E(10) 018+V(1)
17 108+16*V(1) -6+-2*V(1) 01 (11)F> 018+V(1)
18 110+16*V(1) -4+-2*V(1) 01 11 (10)C> 017+V(1)
<< Success! ==> defined new CTR 30 (PPA)
5158148[7]3333260 6643527[26]9661616 -892873[7]9648936 01 11 (10)C> 014464367[6]4824867
== Executing PA-CTR 21, V(1)=0, V(2)=4464367[6]4824862, repcount=1116091[6]6206216, factor=5/4
6385849[7]1601636 1038051[27]1832640 792 01 115580459[6]1031081 (10)C> 013
6385849[7]1601637 1038051[27]1832645 789 01 115580459[6]1031081 <B(11) 00 012
6385849[7]1601638 1038051[27]5956969 -111609[8]2061373 01 <B(11) 015580459[6]1031081 00 012
6385849[7]1601639 1038051[27]5956976 -111609[8]2061370 11 (11)E> 015580459[6]1031081 00 012
6385849[7]1601640 1038051[27]8019138 792 115580459[6]1031082 (11)E> 00 012
6385849[7]1601641 1038051[27]8019140 794 115580459[6]1031083 (11)A> 012
6385849[7]1601642 1038051[27]8019142 796 115580459[6]1031084 (10)D> 01
6385849[7]1601643 1038051[27]8019153 793 115580459[6]1031084 <E(10) 10
6385849[7]1601644 1038051[27]2143489 -111609[8]2061375 <E(10) 105580459[6]1031085
6385849[7]1601645 1038051[27]2143492 -111609[8]2061372 01 (11)F> 105580459[6]1031085
6385849[7]1601646 1038051[27]4205662 798 01 115580459[6]1031085 (11)F>
6385849[7]1601647 1038051[27]4205664 800 01 115580459[6]1031086 (11)B>
6385849[7]1601648 1038051[27]4205675 797 01 115580459[6]1031086 <E(10) 01
6385849[7]1601649 1038051[27]8330019 -111609[8]2061375 01 <E(10) 105580459[6]1031086 01
6385849[7]1601650 1038051[27]8330021 -111609[8]2061377 <A(01) 105580459[6]1031087 01
6385849[7]1601651 1038051[27]8330032 -111609[8]2061374 11 (11)A> 105580459[6]1031087 01
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 111+V(1) (10)C> 013
1 5 -3 01 111+V(1) <B(11) 00 012
2 9+4*V(1) -5+-2*V(1) 01 <B(11) 011+V(1) 00 012
3 16+4*V(1) -2+-2*V(1) 11 (11)E> 011+V(1) 00 012
4 18+6*V(1) 0 112+V(1) (11)E> 00 012
5 20+6*V(1) 2 113+V(1) (11)A> 012
6 22+6*V(1) 4 114+V(1) (10)D> 01
7 33+6*V(1) 1 114+V(1) <E(10) 10
8 49+10*V(1) -7+-2*V(1) <E(10) 105+V(1)
9 52+10*V(1) -4+-2*V(1) 01 (11)F> 105+V(1)
10 62+12*V(1) 6 01 115+V(1) (11)F>
11 64+12*V(1) 8 01 116+V(1) (11)B>
12 75+12*V(1) 5 01 116+V(1) <E(10) 01
13 99+16*V(1) -7+-2*V(1) 01 <E(10) 106+V(1) 01
14 101+16*V(1) -9+-2*V(1) <A(01) 107+V(1) 01
15 112+16*V(1) -6+-2*V(1) 11 (11)A> 107+V(1) 01
<< Success! ==> defined new CTR 31 (PPA)
6385849[7]1601651 1038051[27]8330032 -111609[8]2061374 11 (11)A> 105580459[6]1031087 01
== Executing PA-CTR 1, V(1)=0, V(2)=5580459[6]1031082, repcount=1395114[6]7757771, factor=5/4
8059987[7]4694903 1621954[27]8747476 794 116975574[6]8788856 (11)A> 103 01
== Executing PPA-CTR 4 (once), V(1)=6975574[6]8788855, V(2)=0
8059987[7]4694926 1621954[27]9369300 -139511[8]7576920 01 11 (10)C> 016975574[6]8788863 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=6975574[6]8788858, repcount=1743893[6]7197215, factor=5/4
9978270[7]3864291 2534304[27]6761360 800 01 118719468[6]5986076 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=8719468[6]5986075
9978270[7]3864318 2534304[27]8455214 -174389[8]1971356 01 11 (10)C> 018719468[6]5986085 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=8719468[6]5986080, repcount=2179867[6]3996521, factor=5/4
1237612[8]7826049 3959850[27]7440158 812 01 111089933[7]9982606 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=1089933[7]9982605
1237612[8]7826064 3959850[27]7161938 -217986[8]9964404 11 (11)A> 101089933[7]9982611 01
== Executing PA-CTR 1, V(1)=0, V(2)=1089933[7]9982606, repcount=2724833[6]2495652, factor=5/4
1564592[8]7773888 6187266[27]9167226 812 111362416[7]2478261 (11)A> 103 01
== Executing PPA-CTR 4 (once), V(1)=1362416[7]2478260, V(2)=0
1564592[8]7773911 6187266[27]8819530 -272483[8]4955712 01 11 (10)C> 011362416[7]2478268 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=1362416[7]2478263, repcount=3406042[6]5619566, factor=5/4
1939257[8]9589137 9667604[27]0735454 816 01 111703021[7]8097831 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=1703021[7]8097830
1939257[8]9589152 9667604[27]0300844 -340604[8]6194850 11 (11)A> 101703021[7]8097837 01 10
== Executing PA-CTR 5, V(1)=0, V(2)=1703021[7]8097832, repcount=4257553[6]2024459, factor=5/4
2450163[8]3882660 1510563[28]6412880 822 112128776[7]0122296 (11)A> 10 01 10
== Executing PPA-CTR 12 (once), V(1)=2128776[7]0122291
2450163[8]3882667 1510563[28]6902088 -425755[8]0243770 01 11 (10)C> 012128776[7]0122296 00 11 10
== Executing PA-CTR 6, V(1)=0, V(2)=2128776[7]0122291, repcount=5321941[6]2530573, factor=5/4
3035577[8]1718970 2360254[28]4191440 814 01 112660970[7]2652866 (10)C> 014 00 11 10
3035577[8]1718971 2360254[28]4191445 811 01 112660970[7]2652866 <B(11) 00 013 00 11 10
3035577[8]1718972 2360254[28]4802909 -532194[8]5304921 01 <B(11) 012660970[7]2652866 00 013 00 11 10
3035577[8]1718973 2360254[28]4802916 -532194[8]5304918 11 (11)E> 012660970[7]2652866 00 013 00 11 10
3035577[8]1718974 2360254[28]0108648 814 112660970[7]2652867 (11)E> 00 013 00 11 10
3035577[8]1718975 2360254[28]0108650 816 112660970[7]2652868 (11)A> 013 00 11 10
3035577[8]1718976 2360254[28]0108652 818 112660970[7]2652869 (10)D> 012 00 11 10
3035577[8]1718977 2360254[28]0108663 815 112660970[7]2652869 <E(10) 10 01 00 11 10
3035577[8]1718978 2360254[28]0720139 -532194[8]5304923 <E(10) 102660970[7]2652870 01 00 11 10
3035577[8]1718979 2360254[28]0720142 -532194[8]5304920 01 (11)F> 102660970[7]2652870 01 00 11 10
3035577[8]1718980 2360254[28]6025882 820 01 112660970[7]2652870 (11)F> 01 00 11 10
3035577[8]1718981 2360254[28]6025884 822 01 112660970[7]2652871 (10)C> 00 11 10
3035577[8]1718982 2360254[28]6025893 819 01 112660970[7]2652871 <E(10) 01 11 10
3035577[8]1718983 2360254[28]6637377 -532194[8]5304923 01 <E(10) 102660970[7]2652871 01 11 10
3035577[8]1718984 2360254[28]6637379 -532194[8]5304925 <A(01) 102660970[7]2652872 01 11 10
3035577[8]1718985 2360254[28]6637390 -532194[8]5304922 11 (11)A> 102660970[7]2652872 01 11 10
3035577[8]1718986 2360254[28]6637392 -532194[8]5304920 112 (01)D> 102660970[7]2652871 01 11 10
3035577[8]1718987 2360254[28]6637395 -532194[8]5304923 112 <E(10) 00 102660970[7]2652870 01 11 10
3035577[8]1718988 2360254[28]6637403 -532194[8]5304927 <E(10) 102 00 102660970[7]2652870 01 11 10
3035577[8]1718989 2360254[28]6637406 -532194[8]5304924 01 (11)F> 102 00 102660970[7]2652870 01 11 10
3035577[8]1718990 2360254[28]6637410 -532194[8]5304920 01 112 (11)F> 00 102660970[7]2652870 01 11 10
3035577[8]1718991 2360254[28]6637412 -532194[8]5304918 01 113 (11)B> 102660970[7]2652870 01 11 10
3035577[8]1718992 2360254[28]6637416 -532194[8]5304916 01 114 (11)E> 102660970[7]2652869 01 11 10
3035577[8]1718993 2360254[28]6637421 -532194[8]5304919 01 114 <B(11) 00 102660970[7]2652868 01 11 10
3035577[8]1718994 2360254[28]6637437 -532194[8]5304927 01 <B(11) 014 00 102660970[7]2652868 01 11 10
3035577[8]1718995 2360254[28]6637444 -532194[8]5304924 11 (11)E> 014 00 102660970[7]2652868 01 11 10
3035577[8]1718996 2360254[28]6637452 -532194[8]5304916 115 (11)E> 00 102660970[7]2652868 01 11 10
3035577[8]1718997 2360254[28]6637454 -532194[8]5304914 116 (11)A> 102660970[7]2652868 01 11 10
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 111+V(1) (11)A> 105+V(2) [*]* [*]* [*]*
1 2 2 112+V(1) (01)D> 104+V(2) [*]* [*]* [*]*
2 5 -1 112+V(1) <E(10) 00 103+V(2) [*]* [*]* [*]*
3 13+4*V(1) -5+-2*V(1) <E(10) 102+V(1) 00 103+V(2) [*]* [*]* [*]*
4 16+4*V(1) -2+-2*V(1) 01 (11)F> 102+V(1) 00 103+V(2) [*]* [*]* [*]*
5 20+6*V(1) 2 01 112+V(1) (11)F> 00 103+V(2) [*]* [*]* [*]*
6 22+6*V(1) 4 01 113+V(1) (11)B> 103+V(2) [*]* [*]* [*]*
7 26+6*V(1) 6 01 114+V(1) (11)E> 102+V(2) [*]* [*]* [*]*
8 31+6*V(1) 3 01 114+V(1) <B(11) 00 101+V(2) [*]* [*]* [*]*
9 47+10*V(1) -5+-2*V(1) 01 <B(11) 014+V(1) 00 101+V(2) [*]* [*]* [*]*
10 54+10*V(1) -2+-2*V(1) 11 (11)E> 014+V(1) 00 101+V(2) [*]* [*]* [*]*
11 62+12*V(1) 6 115+V(1) (11)E> 00 101+V(2) [*]* [*]* [*]*
12 64+12*V(1) 8 116+V(1) (11)A> 101+V(2) [*]* [*]* [*]*
<< Success! ==> defined new CTR 32 (PA)
3035577[8]1718997 2360254[28]6637454 -532194[8]5304914 116 (11)A> 102660970[7]2652868 01 11 10
== Executing PA-CTR 32, V(1)=5, V(2)=2660970[7]2652863, repcount=6652426[6]3163216, factor=5/4
3833868[8]9677589 3687898[28]7859438 814 113326213[7]5816086 (11)A> 104 01 11 10
3833868[8]9677590 3687898[28]7859440 816 113326213[7]5816087 (01)D> 103 01 11 10
3833868[8]9677591 3687898[28]7859443 813 113326213[7]5816087 <E(10) 00 102 01 11 10
3833868[8]9677592 3687898[28]1123791 -665242[8]1631361 <E(10) 103326213[7]5816087 00 102 01 11 10
3833868[8]9677593 3687898[28]1123794 -665242[8]1631358 01 (11)F> 103326213[7]5816087 00 102 01 11 10
3833868[8]9677594 3687898[28]2755968 816 01 113326213[7]5816087 (11)F> 00 102 01 11 10
3833868[8]9677595 3687898[28]2755970 818 01 113326213[7]5816088 (11)B> 102 01 11 10
3833868[8]9677596 3687898[28]2755974 820 01 113326213[7]5816089 (11)E> 10 01 11 10
3833868[8]9677597 3687898[28]2755979 817 01 113326213[7]5816089 <B(11) 00 01 11 10
3833868[8]9677598 3687898[28]6020335 -665242[8]1631361 01 <B(11) 013326213[7]5816089 00 01 11 10
3833868[8]9677599 3687898[28]6020342 -665242[8]1631358 11 (11)E> 013326213[7]5816089 00 01 11 10
3833868[8]9677600 3687898[28]7652520 820 113326213[7]5816090 (11)E> 00 01 11 10
3833868[8]9677601 3687898[28]7652522 822 113326213[7]5816091 (11)A> 01 11 10
3833868[8]9677602 3687898[28]7652524 824 113326213[7]5816092 (10)D> 11 10
3833868[8]9677603 3687898[28]7652527 821 113326213[7]5816092 <B(11) 01 10
3833868[8]9677604 3687898[28]0916895 -665242[8]1631363 <B(11) 013326213[7]5816093 10
3833868[8]9677605 3687898[28]0916903 -665242[8]1631365 <E(10) 013326213[7]5816094 10
3833868[8]9677606 3687898[28]0916906 -665242[8]1631362 01 (11)F> 013326213[7]5816094 10
3833868[8]9677607 3687898[28]0916908 -665242[8]1631360 01 11 (10)C> 013326213[7]5816093 10
3833868[8]9677608 3687898[28]0916913 -665242[8]1631363 01 11 <B(11) 00 013326213[7]5816092 10
3833868[8]9677609 3687898[28]0916917 -665242[8]1631365 01 <B(11) 01 00 013326213[7]5816092 10
3833868[8]9677610 3687898[28]0916924 -665242[8]1631362 11 (11)E> 01 00 013326213[7]5816092 10
3833868[8]9677611 3687898[28]0916926 -665242[8]1631360 112 (11)E> 00 013326213[7]5816092 10
3833868[8]9677612 3687898[28]0916928 -665242[8]1631358 113 (11)A> 013326213[7]5816092 10
3833868[8]9677613 3687898[28]0916930 -665242[8]1631356 114 (10)D> 013326213[7]5816091 10
3833868[8]9677614 3687898[28]0916941 -665242[8]1631359 114 <E(10) 10 013326213[7]5816090 10
3833868[8]9677615 3687898[28]0916957 -665242[8]1631367 <E(10) 105 013326213[7]5816090 10
3833868[8]9677616 3687898[28]0916960 -665242[8]1631364 01 (11)F> 105 013326213[7]5816090 10
3833868[8]9677617 3687898[28]0916970 -665242[8]1631354 01 115 (11)F> 013326213[7]5816090 10
3833868[8]9677618 3687898[28]0916972 -665242[8]1631352 01 116 (10)C> 013326213[7]5816089 10
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 01 111+V(1) (10)C> 015+V(2) [*]*
1 5 -3 01 111+V(1) <B(11) 00 014+V(2) [*]*
2 9+4*V(1) -5+-2*V(1) 01 <B(11) 011+V(1) 00 014+V(2) [*]*
3 16+4*V(1) -2+-2*V(1) 11 (11)E> 011+V(1) 00 014+V(2) [*]*
4 18+6*V(1) 0 112+V(1) (11)E> 00 014+V(2) [*]*
5 20+6*V(1) 2 113+V(1) (11)A> 014+V(2) [*]*
6 22+6*V(1) 4 114+V(1) (10)D> 013+V(2) [*]*
7 33+6*V(1) 1 114+V(1) <E(10) 10 012+V(2) [*]*
8 49+10*V(1) -7+-2*V(1) <E(10) 105+V(1) 012+V(2) [*]*
9 52+10*V(1) -4+-2*V(1) 01 (11)F> 105+V(1) 012+V(2) [*]*
10 62+12*V(1) 6 01 115+V(1) (11)F> 012+V(2) [*]*
11 64+12*V(1) 8 01 116+V(1) (10)C> 011+V(2) [*]*
<< Success! ==> defined new CTR 33 (PA)
3833868[8]9677618 3687898[28]0916972 -665242[8]1631352 01 116 (10)C> 013326213[7]5816089 10
== Executing PA-CTR 33, V(1)=5, V(2)=3326213[7]5816084, repcount=8315533[6]3954022, factor=5/4
4748576[8]3171860 5762341[28]1889560 824 01 114157766[7]9770116 (10)C> 01 10
4748576[8]3171861 5762341[28]1889565 821 01 114157766[7]9770116 <B(11) 00 10
4748576[8]3171862 5762341[28]0970029 -831553[8]9539411 01 <B(11) 014157766[7]9770116 00 10
4748576[8]3171863 5762341[28]0970036 -831553[8]9539408 11 (11)E> 014157766[7]9770116 00 10
4748576[8]3171864 5762341[28]0510268 824 114157766[7]9770117 (11)E> 00 10
4748576[8]3171865 5762341[28]0510270 826 114157766[7]9770118 (11)A> 10
4748576[8]3171866 5762341[28]0510272 828 114157766[7]9770119 (01)D>
4748576[8]3171867 5762341[28]0510275 825 114157766[7]9770119 <A(01) 10
4748576[8]3171868 5762341[28]0510281 823 114157766[7]9770118 <B(11) 00 10
4748576[8]3171869 5762341[28]9590753 -831553[8]9539413 <B(11) 014157766[7]9770118 00 10
4748576[8]3171870 5762341[28]9590761 -831553[8]9539415 <E(10) 014157766[7]9770119 00 10
4748576[8]3171871 5762341[28]9590764 -831553[8]9539412 01 (11)F> 014157766[7]9770119 00 10
4748576[8]3171872 5762341[28]9590766 -831553[8]9539410 01 11 (10)C> 014157766[7]9770118 00 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 113+V(1) (10)C> 01 10
1 5 -3 01 113+V(1) <B(11) 00 10
2 17+4*V(1) -9+-2*V(1) 01 <B(11) 013+V(1) 00 10
3 24+4*V(1) -6+-2*V(1) 11 (11)E> 013+V(1) 00 10
4 30+6*V(1) 0 114+V(1) (11)E> 00 10
5 32+6*V(1) 2 115+V(1) (11)A> 10
6 34+6*V(1) 4 116+V(1) (01)D>
7 37+6*V(1) 1 116+V(1) <A(01) 10
8 43+6*V(1) -1 115+V(1) <B(11) 00 10
9 63+10*V(1) -11+-2*V(1) <B(11) 015+V(1) 00 10
10 71+10*V(1) -13+-2*V(1) <E(10) 016+V(1) 00 10
11 74+10*V(1) -10+-2*V(1) 01 (11)F> 016+V(1) 00 10
12 76+10*V(1) -8+-2*V(1) 01 11 (10)C> 015+V(1) 00 10
<< Success! ==> defined new CTR 34 (PPA)
4748576[8]3171872 5762341[28]9590766 -831553[8]9539410 01 11 (10)C> 014157766[7]9770118 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=4157766[7]9770113, repcount=1039441[7]7442529, factor=5/4
5891962[8]5039691 9003658[28]0111982 822 01 115197208[7]7212646 (10)C> 012 00 10
== Executing PPA-CTR 3 (once), V(1)=5197208[7]7212645, V(2)=0
5891962[8]5039709 9003658[28]5514444 -103944[9]4424474 11 (11)A> 105197208[7]7212654 01
== Executing PA-CTR 1, V(1)=0, V(2)=5197208[7]7212649, repcount=1299302[7]1803163, factor=5/4
7451125[8]6677665 1406821[29]0959056 830 116496510[7]9015816 (11)A> 102 01
== Executing PPA-CTR 9 (once), V(1)=6496510[7]9015815
7451125[8]6677683 1406821[29]5212198 -129930[9]8030804 01 11 (10)C> 016496510[7]9015820 00 10
== Executing PA-CTR 2, V(1)=0, V(2)=6496510[7]9015815, repcount=1624127[7]7253954, factor=5/4
9237665[8]6471177 2198158[29]0870114 828 01 118120637[7]6269771 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=8120637[7]6269770
9237665[8]6471192 2198158[29]1186544 -162412[9]2538718 11 (11)A> 108120637[7]6269777 01 10
== Executing PA-CTR 5, V(1)=0, V(2)=8120637[7]6269772, repcount=2030159[7]4067444, factor=5/4
1167385[9]5280520 3434622[29]0273720 834 111015079[8]0337221 (11)A> 10 01 10
== Executing PPA-CTR 12 (once), V(1)=1015079[8]0337216
1167385[9]5280527 3434622[29]1622628 -203015[9]0673608 01 11 (10)C> 011015079[8]0337221 00 11 10
== Executing PA-CTR 6, V(1)=0, V(2)=1015079[8]0337216, repcount=2537699[7]7584305, factor=5/4
1446532[9]8707882 5366598[29]9479748 832 01 111268849[8]7921526 (10)C> 01 00 11 10
1446532[9]8707883 5366598[29]9479753 829 01 111268849[8]7921526 <B(11) 002 11 10
1446532[9]8707884 5366598[29]1165857 -253769[9]5842223 01 <B(11) 011268849[8]7921526 002 11 10
1446532[9]8707885 5366598[29]1165864 -253769[9]5842220 11 (11)E> 011268849[8]7921526 002 11 10
1446532[9]8707886 5366598[29]7008916 832 111268849[8]7921527 (11)E> 002 11 10
1446532[9]8707887 5366598[29]7008918 834 111268849[8]7921528 (11)A> 00 11 10
1446532[9]8707888 5366598[29]7008922 836 111268849[8]7921529 (01)D> 11 10
1446532[9]8707889 5366598[29]7008925 833 111268849[8]7921529 <E(10) 01 10
1446532[9]8707890 5366598[29]8695041 -253769[9]5842225 <E(10) 101268849[8]7921529 01 10
1446532[9]8707891 5366598[29]8695044 -253769[9]5842222 01 (11)F> 101268849[8]7921529 01 10
1446532[9]8707892 5366598[29]4538102 836 01 111268849[8]7921529 (11)F> 01 10
1446532[9]8707893 5366598[29]4538104 838 01 111268849[8]7921530 (10)C> 10
1446532[9]8707894 5366598[29]4538105 839 01 111268849[8]7921530 101 H> 0 [stop]
Lines: 1031
Top steps: 1030
Macro steps: 14465326327716818707894
Basic steps: 5366598383321904238506234609927865294538105
Tape index: 839
ones: 2537699363594175843063
log10(ones ): 21.404
log10(steps ): 42.730
Run state: stop
Some long numbers above are shortened: #(omitted digits) shown in "[]".
Input to awk program:
gohalt 1
5T B1R C0R A0L D0R D1R H1R E1L D0L F1R B1L A1R E1R : 2,537,699,363,594,175,843,063 >5.3*10^42
T 6-state TM #3 from MaBu-List
M 1050
pref sim
machv mbL6_3 just simple
machv mbL6_3-r with repetitions reduced
machv mbL6_3-1 with tape symbol exponents
machv mbL6_3-m as 2-bck-macro machine
machv mbL6_3-a as 2-bck-macro machine with pure additive config-TRs
iam mbL6_3-a
mtype 2 0
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:10:32 CEST 2010
edate Tue Jul 6 22:10:36 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:32 CEST 2010