Comment: This TM produces 374,676,383 nonzeros in 119,112,334,170,342,540 steps. Comment: This is the currently best known 3x3 TM
| State | on 0 |
on 1 |
on 2 |
on 0 | on 1 | on 2 | ||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Move | Goto | Move | Goto | Move | Goto | |||||||
| A | 1RB | 2LA | 1LC | 1 | right | B | 2 | left | A | 1 | left | C |
| B | 0LA | 2RB | 1LB | 0 | left | A | 2 | right | B | 1 | left | B |
| C | 1RH | 1RA | 1RC | 1 | right | H | 1 | right | A | 1 | right | C |
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 12 2 01 (11)B>
2 15 -1 01 <A(22)
3 23 -3 <B(11) 12
4 27 -5 <A(20) 11 12
5 36 -2 01 (11)B> 11 12
6 38 0 01 11 (22)B> 12
7 43 -3 01 11 <B(11) 11
8 46 0 01 12 (22)B> 11
9 48 2 01 12 22 (22)B>
10 57 -1 01 12 22 <A(22) 20
11 65 -3 01 12 <A(22) 22 20
12 69 -5 01 <A(22) 222 20
13 77 -7 <B(11) 12 222 20
14 81 -9 <A(20) 11 12 222 20
15 90 -6 01 (11)B> 11 12 222 20
16 92 -4 01 11 (22)B> 12 222 20
17 97 -7 01 11 <B(11) 11 222 20
18 100 -4 01 12 (22)B> 11 222 20
19 102 -2 01 12 22 (22)B> 222 20
20 105 -5 01 12 22 <B(11) 12 22 20
21 107 -7 01 12 <B(11) 11 12 22 20
22 112 -4 01 22 (22)B> 11 12 22 20
23 114 -2 01 222 (22)B> 12 22 20
24 119 -5 01 222 <B(11) 11 22 20
25 123 -9 01 <B(11) 113 22 20
26 126 -6 02 (22)B> 113 22 20
27 132 0 02 223 (22)B> 22 20
28 135 -3 02 223 <B(11) 12 20
29 141 -9 02 <B(11) 113 12 20
30 143 -11 <A(01) 114 12 20
31 156 -8 11 (12)B> 114 12 20
32 158 -6 11 12 (22)B> 113 12 20
33 164 0 11 12 223 (22)B> 12 20
34 169 -3 11 12 223 <B(11) 11 20
35 175 -9 11 12 <B(11) 114 20
36 180 -6 11 22 (22)B> 114 20
37 188 2 11 225 (22)B> 20
38 191 -1 11 225 <B(11) 10
39 201 -11 11 <B(11) 115 10
40 204 -8 12 (22)B> 115 10
41 214 2 12 225 (22)B> 10
42 220 4 12 225 21 (11)B>
43 223 1 12 225 21 <A(22)
44 225 -1 12 225 <C(12) 22
45 265 -11 12 <C(12) 226
46 273 -13 <A(22) 227
47 281 -15 <A(01) 11 227
48 294 -12 11 (12)B> 11 227
49 296 -10 11 12 (22)B> 227
50 299 -13 11 12 <B(11) 12 226
51 304 -10 11 22 (22)B> 12 226
52 309 -13 11 22 <B(11) 11 226
53 311 -15 11 <B(11) 112 226
54 314 -12 12 (22)B> 112 226
55 318 -8 12 222 (22)B> 226
56 321 -11 12 222 <B(11) 12 225
57 325 -15 12 <B(11) 112 12 225
58 330 -12 22 (22)B> 112 12 225
59 334 -8 223 (22)B> 12 225
60 339 -11 223 <B(11) 11 225
61 345 -17 <B(11) 114 225
62 349 -19 <A(20) 115 225
63 358 -16 01 (11)B> 115 225
64 360 -14 01 11 (22)B> 114 225
65 368 -6 01 11 224 (22)B> 225
66 371 -9 01 11 224 <B(11) 12 224
67 379 -17 01 11 <B(11) 114 12 224
68 382 -14 01 12 (22)B> 114 12 224
69 390 -6 01 12 224 (22)B> 12 224
70 395 -9 01 12 224 <B(11) 11 224
71 403 -17 01 12 <B(11) 115 224
72 408 -14 01 22 (22)B> 115 224
73 418 -4 01 226 (22)B> 224
74 421 -7 01 226 <B(11) 12 223
75 433 -19 01 <B(11) 116 12 223
76 436 -16 02 (22)B> 116 12 223
77 448 -4 02 226 (22)B> 12 223
78 453 -7 02 226 <B(11) 11 223
79 465 -19 02 <B(11) 117 223
80 467 -21 <A(01) 118 223
81 480 -18 11 (12)B> 118 223
82 482 -16 11 12 (22)B> 117 223
83 496 -2 11 12 227 (22)B> 223
84 499 -5 11 12 227 <B(11) 12 222
85 513 -19 11 12 <B(11) 117 12 222
86 518 -16 11 22 (22)B> 117 12 222
87 532 -2 11 228 (22)B> 12 222
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 11 221+V(1) (22)B> 12 225+V(2)
1 5 -3 11 221+V(1) <B(11) 11 225+V(2)
2 7+2*V(1) -5+-2*V(1) 11 <B(11) 112+V(1) 225+V(2)
3 10+2*V(1) -2+-2*V(1) 12 (22)B> 112+V(1) 225+V(2)
4 14+4*V(1) 2 12 222+V(1) (22)B> 225+V(2)
5 17+4*V(1) -1 12 222+V(1) <B(11) 12 224+V(2)
6 21+6*V(1) -5+-2*V(1) 12 <B(11) 112+V(1) 12 224+V(2)
7 26+6*V(1) -2+-2*V(1) 22 (22)B> 112+V(1) 12 224+V(2)
8 30+8*V(1) 2 223+V(1) (22)B> 12 224+V(2)
9 35+8*V(1) -1 223+V(1) <B(11) 11 224+V(2)
10 41+10*V(1) -7+-2*V(1) <B(11) 114+V(1) 224+V(2)
11 45+10*V(1) -9+-2*V(1) <A(20) 115+V(1) 224+V(2)
12 54+10*V(1) -6+-2*V(1) 01 (11)B> 115+V(1) 224+V(2)
13 56+10*V(1) -4+-2*V(1) 01 11 (22)B> 114+V(1) 224+V(2)
14 64+12*V(1) 4 01 11 224+V(1) (22)B> 224+V(2)
15 67+12*V(1) 1 01 11 224+V(1) <B(11) 12 223+V(2)
16 75+14*V(1) -7+-2*V(1) 01 11 <B(11) 114+V(1) 12 223+V(2)
17 78+14*V(1) -4+-2*V(1) 01 12 (22)B> 114+V(1) 12 223+V(2)
18 86+16*V(1) 4 01 12 224+V(1) (22)B> 12 223+V(2)
19 91+16*V(1) 1 01 12 224+V(1) <B(11) 11 223+V(2)
20 99+18*V(1) -7+-2*V(1) 01 12 <B(11) 115+V(1) 223+V(2)
21 104+18*V(1) -4+-2*V(1) 01 22 (22)B> 115+V(1) 223+V(2)
22 114+20*V(1) 6 01 226+V(1) (22)B> 223+V(2)
23 117+20*V(1) 3 01 226+V(1) <B(11) 12 222+V(2)
24 129+22*V(1) -9+-2*V(1) 01 <B(11) 116+V(1) 12 222+V(2)
25 132+22*V(1) -6+-2*V(1) 02 (22)B> 116+V(1) 12 222+V(2)
26 144+24*V(1) 6 02 226+V(1) (22)B> 12 222+V(2)
27 149+24*V(1) 3 02 226+V(1) <B(11) 11 222+V(2)
28 161+26*V(1) -9+-2*V(1) 02 <B(11) 117+V(1) 222+V(2)
29 163+26*V(1) -11+-2*V(1) <A(01) 118+V(1) 222+V(2)
30 176+26*V(1) -8+-2*V(1) 11 (12)B> 118+V(1) 222+V(2)
31 178+26*V(1) -6+-2*V(1) 11 12 (22)B> 117+V(1) 222+V(2)
32 192+28*V(1) 8 11 12 227+V(1) (22)B> 222+V(2)
33 195+28*V(1) 5 11 12 227+V(1) <B(11) 12 221+V(2)
34 209+30*V(1) -9+-2*V(1) 11 12 <B(11) 117+V(1) 12 221+V(2)
35 214+30*V(1) -6+-2*V(1) 11 22 (22)B> 117+V(1) 12 221+V(2)
36 228+32*V(1) 8 11 228+V(1) (22)B> 12 221+V(2)
<< Success! ==> defined new CTR 1 (PA)
88 537 -5 11 228 <B(11) 11 222
89 553 -21 11 <B(11) 119 222
90 556 -18 12 (22)B> 119 222
91 574 0 12 229 (22)B> 222
92 577 -3 12 229 <B(11) 12 22
93 595 -21 12 <B(11) 119 12 22
94 600 -18 22 (22)B> 119 12 22
95 618 0 2210 (22)B> 12 22
96 623 -3 2210 <B(11) 11 22
97 643 -23 <B(11) 1111 22
98 647 -25 <A(20) 1112 22
99 656 -22 01 (11)B> 1112 22
100 658 -20 01 11 (22)B> 1111 22
101 680 2 01 11 2211 (22)B> 22
102 683 -1 01 11 2211 <B(11) 12
103 705 -23 01 11 <B(11) 1111 12
104 708 -20 01 12 (22)B> 1111 12
105 730 2 01 12 2211 (22)B> 12
106 735 -1 01 12 2211 <B(11) 11
107 757 -23 01 12 <B(11) 1112
108 762 -20 01 22 (22)B> 1112
109 786 4 01 2213 (22)B>
110 795 1 01 2213 <A(22) 20
111 899 -25 01 <A(22) 2213 20
112 907 -27 <B(11) 12 2213 20
113 911 -29 <A(20) 11 12 2213 20
114 920 -26 01 (11)B> 11 12 2213 20
115 922 -24 01 11 (22)B> 12 2213 20
116 927 -27 01 11 <B(11) 11 2213 20
117 930 -24 01 12 (22)B> 11 2213 20
118 932 -22 01 12 22 (22)B> 2213 20
119 935 -25 01 12 22 <B(11) 12 2212 20
120 937 -27 01 12 <B(11) 11 12 2212 20
121 942 -24 01 22 (22)B> 11 12 2212 20
122 944 -22 01 222 (22)B> 12 2212 20
123 949 -25 01 222 <B(11) 11 2212 20
124 953 -29 01 <B(11) 113 2212 20
125 956 -26 02 (22)B> 113 2212 20
126 962 -20 02 223 (22)B> 2212 20
127 965 -23 02 223 <B(11) 12 2211 20
128 971 -29 02 <B(11) 113 12 2211 20
129 973 -31 <A(01) 114 12 2211 20
130 986 -28 11 (12)B> 114 12 2211 20
131 988 -26 11 12 (22)B> 113 12 2211 20
132 994 -20 11 12 223 (22)B> 12 2211 20
133 999 -23 11 12 223 <B(11) 11 2211 20
134 1005 -29 11 12 <B(11) 114 2211 20
135 1010 -26 11 22 (22)B> 114 2211 20
136 1018 -18 11 225 (22)B> 2211 20
137 1021 -21 11 225 <B(11) 12 2210 20
138 1031 -31 11 <B(11) 115 12 2210 20
139 1034 -28 12 (22)B> 115 12 2210 20
140 1044 -18 12 225 (22)B> 12 2210 20
141 1049 -21 12 225 <B(11) 11 2210 20
142 1059 -31 12 <B(11) 116 2210 20
143 1064 -28 22 (22)B> 116 2210 20
144 1076 -16 227 (22)B> 2210 20
145 1079 -19 227 <B(11) 12 229 20
146 1093 -33 <B(11) 117 12 229 20
147 1097 -35 <A(20) 118 12 229 20
148 1106 -32 01 (11)B> 118 12 229 20
149 1108 -30 01 11 (22)B> 117 12 229 20
150 1122 -16 01 11 227 (22)B> 12 229 20
151 1127 -19 01 11 227 <B(11) 11 229 20
152 1141 -33 01 11 <B(11) 118 229 20
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 01 11 <B(11) 111+V(2) 225+V(1) [*]*
1 3 3 01 12 (22)B> 111+V(2) 225+V(1) [*]*
2 5+2*V(2) 5+2*V(2) 01 12 221+V(2) (22)B> 225+V(1) [*]*
3 8+2*V(2) 2+2*V(2) 01 12 221+V(2) <B(11) 12 224+V(1) [*]*
4 10+4*V(2) 0 01 12 <B(11) 111+V(2) 12 224+V(1) [*]*
5 15+4*V(2) 3 01 22 (22)B> 111+V(2) 12 224+V(1) [*]*
6 17+6*V(2) 5+2*V(2) 01 222+V(2) (22)B> 12 224+V(1) [*]*
7 22+6*V(2) 2+2*V(2) 01 222+V(2) <B(11) 11 224+V(1) [*]*
8 26+8*V(2) -2 01 <B(11) 113+V(2) 224+V(1) [*]*
9 29+8*V(2) 1 02 (22)B> 113+V(2) 224+V(1) [*]*
10 35+10*V(2) 7+2*V(2) 02 223+V(2) (22)B> 224+V(1) [*]*
11 38+10*V(2) 4+2*V(2) 02 223+V(2) <B(11) 12 223+V(1) [*]*
12 44+12*V(2) -2 02 <B(11) 113+V(2) 12 223+V(1) [*]*
13 46+12*V(2) -4 <A(01) 114+V(2) 12 223+V(1) [*]*
14 59+12*V(2) -1 11 (12)B> 114+V(2) 12 223+V(1) [*]*
15 61+12*V(2) 1 11 12 (22)B> 113+V(2) 12 223+V(1) [*]*
16 67+14*V(2) 7+2*V(2) 11 12 223+V(2) (22)B> 12 223+V(1) [*]*
17 72+14*V(2) 4+2*V(2) 11 12 223+V(2) <B(11) 11 223+V(1) [*]*
18 78+16*V(2) -2 11 12 <B(11) 114+V(2) 223+V(1) [*]*
19 83+16*V(2) 1 11 22 (22)B> 114+V(2) 223+V(1) [*]*
20 91+18*V(2) 9+2*V(2) 11 225+V(2) (22)B> 223+V(1) [*]*
21 94+18*V(2) 6+2*V(2) 11 225+V(2) <B(11) 12 222+V(1) [*]*
22 104+20*V(2) -4 11 <B(11) 115+V(2) 12 222+V(1) [*]*
23 107+20*V(2) -1 12 (22)B> 115+V(2) 12 222+V(1) [*]*
24 117+22*V(2) 9+2*V(2) 12 225+V(2) (22)B> 12 222+V(1) [*]*
25 122+22*V(2) 6+2*V(2) 12 225+V(2) <B(11) 11 222+V(1) [*]*
26 132+24*V(2) -4 12 <B(11) 116+V(2) 222+V(1) [*]*
27 137+24*V(2) -1 22 (22)B> 116+V(2) 222+V(1) [*]*
28 149+26*V(2) 11+2*V(2) 227+V(2) (22)B> 222+V(1) [*]*
29 152+26*V(2) 8+2*V(2) 227+V(2) <B(11) 12 221+V(1) [*]*
30 166+28*V(2) -6 <B(11) 117+V(2) 12 221+V(1) [*]*
31 170+28*V(2) -8 <A(20) 118+V(2) 12 221+V(1) [*]*
32 179+28*V(2) -5 01 (11)B> 118+V(2) 12 221+V(1) [*]*
33 181+28*V(2) -3 01 11 (22)B> 117+V(2) 12 221+V(1) [*]*
34 195+30*V(2) 11+2*V(2) 01 11 227+V(2) (22)B> 12 221+V(1) [*]*
35 200+30*V(2) 8+2*V(2) 01 11 227+V(2) <B(11) 11 221+V(1) [*]*
36 214+32*V(2) -6 01 11 <B(11) 118+V(2) 221+V(1) [*]*
<< Success! ==> defined new CTR 2 (PA)
152 1141 -33 01 11 <B(11) 118 229 20
== Executing PA-CTR 2, V(1)=4, V(2)=7, repcount=2, factor=7/4
224 2241 -45 01 11 <B(11) 1122 22 20
225 2244 -42 01 12 (22)B> 1122 22 20
226 2288 2 01 12 2222 (22)B> 22 20
227 2291 -1 01 12 2222 <B(11) 12 20
228 2335 -45 01 12 <B(11) 1122 12 20
229 2340 -42 01 22 (22)B> 1122 12 20
230 2384 2 01 2223 (22)B> 12 20
231 2389 -1 01 2223 <B(11) 11 20
232 2435 -47 01 <B(11) 1124 20
233 2438 -44 02 (22)B> 1124 20
234 2486 4 02 2224 (22)B> 20
235 2489 1 02 2224 <B(11) 10
236 2537 -47 02 <B(11) 1124 10
237 2539 -49 <A(01) 1125 10
238 2552 -46 11 (12)B> 1125 10
239 2554 -44 11 12 (22)B> 1124 10
240 2602 4 11 12 2224 (22)B> 10
241 2608 6 11 12 2224 21 (11)B>
242 2611 3 11 12 2224 21 <A(22)
243 2613 1 11 12 2224 <C(12) 22
244 2805 -47 11 12 <C(12) 2225
245 2813 -49 11 <A(22) 2226
246 2815 -51 <A(22) 2227
247 2823 -53 <A(01) 11 2227
248 2836 -50 11 (12)B> 11 2227
249 2838 -48 11 12 (22)B> 2227
250 2841 -51 11 12 <B(11) 12 2226
251 2846 -48 11 22 (22)B> 12 2226
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 11 <B(11) 111+V(1) 22 20
1 3 3 01 12 (22)B> 111+V(1) 22 20
2 5+2*V(1) 5+2*V(1) 01 12 221+V(1) (22)B> 22 20
3 8+2*V(1) 2+2*V(1) 01 12 221+V(1) <B(11) 12 20
4 10+4*V(1) 0 01 12 <B(11) 111+V(1) 12 20
5 15+4*V(1) 3 01 22 (22)B> 111+V(1) 12 20
6 17+6*V(1) 5+2*V(1) 01 222+V(1) (22)B> 12 20
7 22+6*V(1) 2+2*V(1) 01 222+V(1) <B(11) 11 20
8 26+8*V(1) -2 01 <B(11) 113+V(1) 20
9 29+8*V(1) 1 02 (22)B> 113+V(1) 20
10 35+10*V(1) 7+2*V(1) 02 223+V(1) (22)B> 20
11 38+10*V(1) 4+2*V(1) 02 223+V(1) <B(11) 10
12 44+12*V(1) -2 02 <B(11) 113+V(1) 10
13 46+12*V(1) -4 <A(01) 114+V(1) 10
14 59+12*V(1) -1 11 (12)B> 114+V(1) 10
15 61+12*V(1) 1 11 12 (22)B> 113+V(1) 10
16 67+14*V(1) 7+2*V(1) 11 12 223+V(1) (22)B> 10
17 73+14*V(1) 9+2*V(1) 11 12 223+V(1) 21 (11)B>
18 76+14*V(1) 6+2*V(1) 11 12 223+V(1) 21 <A(22)
19 78+14*V(1) 4+2*V(1) 11 12 223+V(1) <C(12) 22
20 102+22*V(1) -2 11 12 <C(12) 224+V(1)
21 110+22*V(1) -4 11 <A(22) 225+V(1)
22 112+22*V(1) -6 <A(22) 226+V(1)
23 120+22*V(1) -8 <A(01) 11 226+V(1)
24 133+22*V(1) -5 11 (12)B> 11 226+V(1)
25 135+22*V(1) -3 11 12 (22)B> 226+V(1)
26 138+22*V(1) -6 11 12 <B(11) 12 225+V(1)
27 143+22*V(1) -3 11 22 (22)B> 12 225+V(1)
<< Success! ==> defined new CTR 3 (PPA)
251 2846 -48 11 22 (22)B> 12 2226
== Executing PA-CTR 1, V(1)=0, V(2)=21, repcount=6, factor=7/4
467 7574 0 11 2243 (22)B> 12 222
468 7579 -3 11 2243 <B(11) 11 222
469 7665 -89 11 <B(11) 1144 222
470 7668 -86 12 (22)B> 1144 222
471 7756 2 12 2244 (22)B> 222
472 7759 -1 12 2244 <B(11) 12 22
473 7847 -89 12 <B(11) 1144 12 22
474 7852 -86 22 (22)B> 1144 12 22
475 7940 2 2245 (22)B> 12 22
476 7945 -1 2245 <B(11) 11 22
477 8035 -91 <B(11) 1146 22
478 8039 -93 <A(20) 1147 22
479 8048 -90 01 (11)B> 1147 22
480 8050 -88 01 11 (22)B> 1146 22
481 8142 4 01 11 2246 (22)B> 22
482 8145 1 01 11 2246 <B(11) 12
483 8237 -91 01 11 <B(11) 1146 12
484 8240 -88 01 12 (22)B> 1146 12
485 8332 4 01 12 2246 (22)B> 12
486 8337 1 01 12 2246 <B(11) 11
487 8429 -91 01 12 <B(11) 1147
488 8434 -88 01 22 (22)B> 1147
489 8528 6 01 2248 (22)B>
490 8537 3 01 2248 <A(22) 20
491 8921 -93 01 <A(22) 2248 20
492 8929 -95 <B(11) 12 2248 20
493 8933 -97 <A(20) 11 12 2248 20
494 8942 -94 01 (11)B> 11 12 2248 20
495 8944 -92 01 11 (22)B> 12 2248 20
496 8949 -95 01 11 <B(11) 11 2248 20
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 11 221+V(1) (22)B> 12 222
1 5 -3 11 221+V(1) <B(11) 11 222
2 7+2*V(1) -5+-2*V(1) 11 <B(11) 112+V(1) 222
3 10+2*V(1) -2+-2*V(1) 12 (22)B> 112+V(1) 222
4 14+4*V(1) 2 12 222+V(1) (22)B> 222
5 17+4*V(1) -1 12 222+V(1) <B(11) 12 22
6 21+6*V(1) -5+-2*V(1) 12 <B(11) 112+V(1) 12 22
7 26+6*V(1) -2+-2*V(1) 22 (22)B> 112+V(1) 12 22
8 30+8*V(1) 2 223+V(1) (22)B> 12 22
9 35+8*V(1) -1 223+V(1) <B(11) 11 22
10 41+10*V(1) -7+-2*V(1) <B(11) 114+V(1) 22
11 45+10*V(1) -9+-2*V(1) <A(20) 115+V(1) 22
12 54+10*V(1) -6+-2*V(1) 01 (11)B> 115+V(1) 22
13 56+10*V(1) -4+-2*V(1) 01 11 (22)B> 114+V(1) 22
14 64+12*V(1) 4 01 11 224+V(1) (22)B> 22
15 67+12*V(1) 1 01 11 224+V(1) <B(11) 12
16 75+14*V(1) -7+-2*V(1) 01 11 <B(11) 114+V(1) 12
17 78+14*V(1) -4+-2*V(1) 01 12 (22)B> 114+V(1) 12
18 86+16*V(1) 4 01 12 224+V(1) (22)B> 12
19 91+16*V(1) 1 01 12 224+V(1) <B(11) 11
20 99+18*V(1) -7+-2*V(1) 01 12 <B(11) 115+V(1)
21 104+18*V(1) -4+-2*V(1) 01 22 (22)B> 115+V(1)
22 114+20*V(1) 6 01 226+V(1) (22)B>
23 123+20*V(1) 3 01 226+V(1) <A(22) 20
24 171+28*V(1) -9+-2*V(1) 01 <A(22) 226+V(1) 20
25 179+28*V(1) -11+-2*V(1) <B(11) 12 226+V(1) 20
26 183+28*V(1) -13+-2*V(1) <A(20) 11 12 226+V(1) 20
27 192+28*V(1) -10+-2*V(1) 01 (11)B> 11 12 226+V(1) 20
28 194+28*V(1) -8+-2*V(1) 01 11 (22)B> 12 226+V(1) 20
29 199+28*V(1) -11+-2*V(1) 01 11 <B(11) 11 226+V(1) 20
<< Success! ==> defined new CTR 4 (PPA)
496 8949 -95 01 11 <B(11) 11 2248 20
== Executing PA-CTR 2, V(1)=43, V(2)=0, repcount=11, factor=7/4
892 23623 -161 01 11 <B(11) 1178 224 20
893 23626 -158 01 12 (22)B> 1178 224 20
894 23782 -2 01 12 2278 (22)B> 224 20
895 23785 -5 01 12 2278 <B(11) 12 223 20
896 23941 -161 01 12 <B(11) 1178 12 223 20
897 23946 -158 01 22 (22)B> 1178 12 223 20
898 24102 -2 01 2279 (22)B> 12 223 20
899 24107 -5 01 2279 <B(11) 11 223 20
900 24265 -163 01 <B(11) 1180 223 20
901 24268 -160 02 (22)B> 1180 223 20
902 24428 0 02 2280 (22)B> 223 20
903 24431 -3 02 2280 <B(11) 12 222 20
904 24591 -163 02 <B(11) 1180 12 222 20
905 24593 -165 <A(01) 1181 12 222 20
906 24606 -162 11 (12)B> 1181 12 222 20
907 24608 -160 11 12 (22)B> 1180 12 222 20
908 24768 0 11 12 2280 (22)B> 12 222 20
909 24773 -3 11 12 2280 <B(11) 11 222 20
910 24933 -163 11 12 <B(11) 1181 222 20
911 24938 -160 11 22 (22)B> 1181 222 20
912 25100 2 11 2282 (22)B> 222 20
913 25103 -1 11 2282 <B(11) 12 22 20
914 25267 -165 11 <B(11) 1182 12 22 20
915 25270 -162 12 (22)B> 1182 12 22 20
916 25434 2 12 2282 (22)B> 12 22 20
917 25439 -1 12 2282 <B(11) 11 22 20
918 25603 -165 12 <B(11) 1183 22 20
919 25608 -162 22 (22)B> 1183 22 20
920 25774 4 2284 (22)B> 22 20
921 25777 1 2284 <B(11) 12 20
922 25945 -167 <B(11) 1184 12 20
923 25949 -169 <A(20) 1185 12 20
924 25958 -166 01 (11)B> 1185 12 20
925 25960 -164 01 11 (22)B> 1184 12 20
926 26128 4 01 11 2284 (22)B> 12 20
927 26133 1 01 11 2284 <B(11) 11 20
928 26301 -167 01 11 <B(11) 1185 20
929 26304 -164 01 12 (22)B> 1185 20
930 26474 6 01 12 2285 (22)B> 20
931 26477 3 01 12 2285 <B(11) 10
932 26647 -167 01 12 <B(11) 1185 10
933 26652 -164 01 22 (22)B> 1185 10
934 26822 6 01 2286 (22)B> 10
935 26828 8 01 2286 21 (11)B>
936 26831 5 01 2286 21 <A(22)
937 26833 3 01 2286 <C(12) 22
938 27521 -169 01 <C(12) 2287
939 27531 -171 <B(11) 12 2287
940 27535 -173 <A(20) 11 12 2287
941 27544 -170 01 (11)B> 11 12 2287
942 27546 -168 01 11 (22)B> 12 2287
943 27551 -171 01 11 <B(11) 11 2287
944 27554 -168 01 12 (22)B> 11 2287
945 27556 -166 01 12 22 (22)B> 2287
946 27559 -169 01 12 22 <B(11) 12 2286
947 27561 -171 01 12 <B(11) 11 12 2286
948 27566 -168 01 22 (22)B> 11 12 2286
949 27568 -166 01 222 (22)B> 12 2286
950 27573 -169 01 222 <B(11) 11 2286
951 27577 -173 01 <B(11) 113 2286
952 27580 -170 02 (22)B> 113 2286
953 27586 -164 02 223 (22)B> 2286
954 27589 -167 02 223 <B(11) 12 2285
955 27595 -173 02 <B(11) 113 12 2285
956 27597 -175 <A(01) 114 12 2285
957 27610 -172 11 (12)B> 114 12 2285
958 27612 -170 11 12 (22)B> 113 12 2285
959 27618 -164 11 12 223 (22)B> 12 2285
960 27623 -167 11 12 223 <B(11) 11 2285
961 27629 -173 11 12 <B(11) 114 2285
962 27634 -170 11 22 (22)B> 114 2285
963 27642 -162 11 225 (22)B> 2285
964 27645 -165 11 225 <B(11) 12 2284
965 27655 -175 11 <B(11) 115 12 2284
966 27658 -172 12 (22)B> 115 12 2284
967 27668 -162 12 225 (22)B> 12 2284
968 27673 -165 12 225 <B(11) 11 2284
969 27683 -175 12 <B(11) 116 2284
970 27688 -172 22 (22)B> 116 2284
971 27700 -160 227 (22)B> 2284
972 27703 -163 227 <B(11) 12 2283
973 27717 -177 <B(11) 117 12 2283
974 27721 -179 <A(20) 118 12 2283
975 27730 -176 01 (11)B> 118 12 2283
976 27732 -174 01 11 (22)B> 117 12 2283
977 27746 -160 01 11 227 (22)B> 12 2283
978 27751 -163 01 11 227 <B(11) 11 2283
979 27765 -177 01 11 <B(11) 118 2283
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 01 11 <B(11) 111+V(2) 225+V(1)
1 3 3 01 12 (22)B> 111+V(2) 225+V(1)
2 5+2*V(2) 5+2*V(2) 01 12 221+V(2) (22)B> 225+V(1)
3 8+2*V(2) 2+2*V(2) 01 12 221+V(2) <B(11) 12 224+V(1)
4 10+4*V(2) 0 01 12 <B(11) 111+V(2) 12 224+V(1)
5 15+4*V(2) 3 01 22 (22)B> 111+V(2) 12 224+V(1)
6 17+6*V(2) 5+2*V(2) 01 222+V(2) (22)B> 12 224+V(1)
7 22+6*V(2) 2+2*V(2) 01 222+V(2) <B(11) 11 224+V(1)
8 26+8*V(2) -2 01 <B(11) 113+V(2) 224+V(1)
9 29+8*V(2) 1 02 (22)B> 113+V(2) 224+V(1)
10 35+10*V(2) 7+2*V(2) 02 223+V(2) (22)B> 224+V(1)
11 38+10*V(2) 4+2*V(2) 02 223+V(2) <B(11) 12 223+V(1)
12 44+12*V(2) -2 02 <B(11) 113+V(2) 12 223+V(1)
13 46+12*V(2) -4 <A(01) 114+V(2) 12 223+V(1)
14 59+12*V(2) -1 11 (12)B> 114+V(2) 12 223+V(1)
15 61+12*V(2) 1 11 12 (22)B> 113+V(2) 12 223+V(1)
16 67+14*V(2) 7+2*V(2) 11 12 223+V(2) (22)B> 12 223+V(1)
17 72+14*V(2) 4+2*V(2) 11 12 223+V(2) <B(11) 11 223+V(1)
18 78+16*V(2) -2 11 12 <B(11) 114+V(2) 223+V(1)
19 83+16*V(2) 1 11 22 (22)B> 114+V(2) 223+V(1)
20 91+18*V(2) 9+2*V(2) 11 225+V(2) (22)B> 223+V(1)
21 94+18*V(2) 6+2*V(2) 11 225+V(2) <B(11) 12 222+V(1)
22 104+20*V(2) -4 11 <B(11) 115+V(2) 12 222+V(1)
23 107+20*V(2) -1 12 (22)B> 115+V(2) 12 222+V(1)
24 117+22*V(2) 9+2*V(2) 12 225+V(2) (22)B> 12 222+V(1)
25 122+22*V(2) 6+2*V(2) 12 225+V(2) <B(11) 11 222+V(1)
26 132+24*V(2) -4 12 <B(11) 116+V(2) 222+V(1)
27 137+24*V(2) -1 22 (22)B> 116+V(2) 222+V(1)
28 149+26*V(2) 11+2*V(2) 227+V(2) (22)B> 222+V(1)
29 152+26*V(2) 8+2*V(2) 227+V(2) <B(11) 12 221+V(1)
30 166+28*V(2) -6 <B(11) 117+V(2) 12 221+V(1)
31 170+28*V(2) -8 <A(20) 118+V(2) 12 221+V(1)
32 179+28*V(2) -5 01 (11)B> 118+V(2) 12 221+V(1)
33 181+28*V(2) -3 01 11 (22)B> 117+V(2) 12 221+V(1)
34 195+30*V(2) 11+2*V(2) 01 11 227+V(2) (22)B> 12 221+V(1)
35 200+30*V(2) 8+2*V(2) 01 11 227+V(2) <B(11) 11 221+V(1)
36 214+32*V(2) -6 01 11 <B(11) 118+V(2) 221+V(1)
<< Success! ==> defined new CTR 5 (PA)
979 27765 -177 01 11 <B(11) 118 2283
== Executing PA-CTR 5, V(1)=78, V(2)=7, repcount=20, factor=7/4
1699 79085 -297 01 11 <B(11) 11148 223
1700 79088 -294 01 12 (22)B> 11148 223
1701 79384 2 01 12 22148 (22)B> 223
1702 79387 -1 01 12 22148 <B(11) 12 222
1703 79683 -297 01 12 <B(11) 11148 12 222
1704 79688 -294 01 22 (22)B> 11148 12 222
1705 79984 2 01 22149 (22)B> 12 222
1706 79989 -1 01 22149 <B(11) 11 222
1707 80287 -299 01 <B(11) 11150 222
1708 80290 -296 02 (22)B> 11150 222
1709 80590 4 02 22150 (22)B> 222
1710 80593 1 02 22150 <B(11) 12 22
1711 80893 -299 02 <B(11) 11150 12 22
1712 80895 -301 <A(01) 11151 12 22
1713 80908 -298 11 (12)B> 11151 12 22
1714 80910 -296 11 12 (22)B> 11150 12 22
1715 81210 4 11 12 22150 (22)B> 12 22
1716 81215 1 11 12 22150 <B(11) 11 22
1717 81515 -299 11 12 <B(11) 11151 22
1718 81520 -296 11 22 (22)B> 11151 22
1719 81822 6 11 22152 (22)B> 22
1720 81825 3 11 22152 <B(11) 12
1721 82129 -301 11 <B(11) 11152 12
1722 82132 -298 12 (22)B> 11152 12
1723 82436 6 12 22152 (22)B> 12
1724 82441 3 12 22152 <B(11) 11
1725 82745 -301 12 <B(11) 11153
1726 82750 -298 22 (22)B> 11153
1727 83056 8 22154 (22)B>
1728 83065 5 22154 <A(22) 20
1729 84297 -303 <A(22) 22154 20
1730 84305 -305 <A(01) 11 22154 20
1731 84318 -302 11 (12)B> 11 22154 20
1732 84320 -300 11 12 (22)B> 22154 20
1733 84323 -303 11 12 <B(11) 12 22153 20
1734 84328 -300 11 22 (22)B> 12 22153 20
1735 84333 -303 11 22 <B(11) 11 22153 20
1736 84335 -305 11 <B(11) 112 22153 20
1737 84338 -302 12 (22)B> 112 22153 20
1738 84342 -298 12 222 (22)B> 22153 20
1739 84345 -301 12 222 <B(11) 12 22152 20
1740 84349 -305 12 <B(11) 112 12 22152 20
1741 84354 -302 22 (22)B> 112 12 22152 20
1742 84358 -298 223 (22)B> 12 22152 20
1743 84363 -301 223 <B(11) 11 22152 20
1744 84369 -307 <B(11) 114 22152 20
1745 84373 -309 <A(20) 115 22152 20
1746 84382 -306 01 (11)B> 115 22152 20
1747 84384 -304 01 11 (22)B> 114 22152 20
1748 84392 -296 01 11 224 (22)B> 22152 20
1749 84395 -299 01 11 224 <B(11) 12 22151 20
1750 84403 -307 01 11 <B(11) 114 12 22151 20
1751 84406 -304 01 12 (22)B> 114 12 22151 20
1752 84414 -296 01 12 224 (22)B> 12 22151 20
1753 84419 -299 01 12 224 <B(11) 11 22151 20
1754 84427 -307 01 12 <B(11) 115 22151 20
1755 84432 -304 01 22 (22)B> 115 22151 20
1756 84442 -294 01 226 (22)B> 22151 20
1757 84445 -297 01 226 <B(11) 12 22150 20
1758 84457 -309 01 <B(11) 116 12 22150 20
1759 84460 -306 02 (22)B> 116 12 22150 20
1760 84472 -294 02 226 (22)B> 12 22150 20
1761 84477 -297 02 226 <B(11) 11 22150 20
1762 84489 -309 02 <B(11) 117 22150 20
1763 84491 -311 <A(01) 118 22150 20
1764 84504 -308 11 (12)B> 118 22150 20
1765 84506 -306 11 12 (22)B> 117 22150 20
1766 84520 -292 11 12 227 (22)B> 22150 20
1767 84523 -295 11 12 227 <B(11) 12 22149 20
1768 84537 -309 11 12 <B(11) 117 12 22149 20
1769 84542 -306 11 22 (22)B> 117 12 22149 20
1770 84556 -292 11 228 (22)B> 12 22149 20
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 11 221+V(1) (22)B> 12 225+V(2) [*]*
1 5 -3 11 221+V(1) <B(11) 11 225+V(2) [*]*
2 7+2*V(1) -5+-2*V(1) 11 <B(11) 112+V(1) 225+V(2) [*]*
3 10+2*V(1) -2+-2*V(1) 12 (22)B> 112+V(1) 225+V(2) [*]*
4 14+4*V(1) 2 12 222+V(1) (22)B> 225+V(2) [*]*
5 17+4*V(1) -1 12 222+V(1) <B(11) 12 224+V(2) [*]*
6 21+6*V(1) -5+-2*V(1) 12 <B(11) 112+V(1) 12 224+V(2) [*]*
7 26+6*V(1) -2+-2*V(1) 22 (22)B> 112+V(1) 12 224+V(2) [*]*
8 30+8*V(1) 2 223+V(1) (22)B> 12 224+V(2) [*]*
9 35+8*V(1) -1 223+V(1) <B(11) 11 224+V(2) [*]*
10 41+10*V(1) -7+-2*V(1) <B(11) 114+V(1) 224+V(2) [*]*
11 45+10*V(1) -9+-2*V(1) <A(20) 115+V(1) 224+V(2) [*]*
12 54+10*V(1) -6+-2*V(1) 01 (11)B> 115+V(1) 224+V(2) [*]*
13 56+10*V(1) -4+-2*V(1) 01 11 (22)B> 114+V(1) 224+V(2) [*]*
14 64+12*V(1) 4 01 11 224+V(1) (22)B> 224+V(2) [*]*
15 67+12*V(1) 1 01 11 224+V(1) <B(11) 12 223+V(2) [*]*
16 75+14*V(1) -7+-2*V(1) 01 11 <B(11) 114+V(1) 12 223+V(2) [*]*
17 78+14*V(1) -4+-2*V(1) 01 12 (22)B> 114+V(1) 12 223+V(2) [*]*
18 86+16*V(1) 4 01 12 224+V(1) (22)B> 12 223+V(2) [*]*
19 91+16*V(1) 1 01 12 224+V(1) <B(11) 11 223+V(2) [*]*
20 99+18*V(1) -7+-2*V(1) 01 12 <B(11) 115+V(1) 223+V(2) [*]*
21 104+18*V(1) -4+-2*V(1) 01 22 (22)B> 115+V(1) 223+V(2) [*]*
22 114+20*V(1) 6 01 226+V(1) (22)B> 223+V(2) [*]*
23 117+20*V(1) 3 01 226+V(1) <B(11) 12 222+V(2) [*]*
24 129+22*V(1) -9+-2*V(1) 01 <B(11) 116+V(1) 12 222+V(2) [*]*
25 132+22*V(1) -6+-2*V(1) 02 (22)B> 116+V(1) 12 222+V(2) [*]*
26 144+24*V(1) 6 02 226+V(1) (22)B> 12 222+V(2) [*]*
27 149+24*V(1) 3 02 226+V(1) <B(11) 11 222+V(2) [*]*
28 161+26*V(1) -9+-2*V(1) 02 <B(11) 117+V(1) 222+V(2) [*]*
29 163+26*V(1) -11+-2*V(1) <A(01) 118+V(1) 222+V(2) [*]*
30 176+26*V(1) -8+-2*V(1) 11 (12)B> 118+V(1) 222+V(2) [*]*
31 178+26*V(1) -6+-2*V(1) 11 12 (22)B> 117+V(1) 222+V(2) [*]*
32 192+28*V(1) 8 11 12 227+V(1) (22)B> 222+V(2) [*]*
33 195+28*V(1) 5 11 12 227+V(1) <B(11) 12 221+V(2) [*]*
34 209+30*V(1) -9+-2*V(1) 11 12 <B(11) 117+V(1) 12 221+V(2) [*]*
35 214+30*V(1) -6+-2*V(1) 11 22 (22)B> 117+V(1) 12 221+V(2) [*]*
36 228+32*V(1) 8 11 228+V(1) (22)B> 12 221+V(2) [*]*
<< Success! ==> defined new CTR 6 (PA)
1770 84556 -292 11 228 (22)B> 12 22149 20
== Executing PA-CTR 6, V(1)=7, V(2)=144, repcount=37, factor=7/4
3102 250464 4 11 22267 (22)B> 12 22 20
3103 250469 1 11 22267 <B(11) 11 22 20
3104 251003 -533 11 <B(11) 11268 22 20
3105 251006 -530 12 (22)B> 11268 22 20
3106 251542 6 12 22268 (22)B> 22 20
3107 251545 3 12 22268 <B(11) 12 20
3108 252081 -533 12 <B(11) 11268 12 20
3109 252086 -530 22 (22)B> 11268 12 20
3110 252622 6 22269 (22)B> 12 20
3111 252627 3 22269 <B(11) 11 20
3112 253165 -535 <B(11) 11270 20
3113 253169 -537 <A(20) 11271 20
3114 253178 -534 01 (11)B> 11271 20
3115 253180 -532 01 11 (22)B> 11270 20
3116 253720 8 01 11 22270 (22)B> 20
3117 253723 5 01 11 22270 <B(11) 10
3118 254263 -535 01 11 <B(11) 11270 10
3119 254266 -532 01 12 (22)B> 11270 10
3120 254806 8 01 12 22270 (22)B> 10
3121 254812 10 01 12 22270 21 (11)B>
3122 254815 7 01 12 22270 21 <A(22)
3123 254817 5 01 12 22270 <C(12) 22
3124 256977 -535 01 12 <C(12) 22271
3125 256985 -537 01 <A(22) 22272
3126 256993 -539 <B(11) 12 22272
3127 256997 -541 <A(20) 11 12 22272
3128 257006 -538 01 (11)B> 11 12 22272
3129 257008 -536 01 11 (22)B> 12 22272
3130 257013 -539 01 11 <B(11) 11 22272
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 11 221+V(1) (22)B> 12 22 20
1 5 -3 11 221+V(1) <B(11) 11 22 20
2 7+2*V(1) -5+-2*V(1) 11 <B(11) 112+V(1) 22 20
3 10+2*V(1) -2+-2*V(1) 12 (22)B> 112+V(1) 22 20
4 14+4*V(1) 2 12 222+V(1) (22)B> 22 20
5 17+4*V(1) -1 12 222+V(1) <B(11) 12 20
6 21+6*V(1) -5+-2*V(1) 12 <B(11) 112+V(1) 12 20
7 26+6*V(1) -2+-2*V(1) 22 (22)B> 112+V(1) 12 20
8 30+8*V(1) 2 223+V(1) (22)B> 12 20
9 35+8*V(1) -1 223+V(1) <B(11) 11 20
10 41+10*V(1) -7+-2*V(1) <B(11) 114+V(1) 20
11 45+10*V(1) -9+-2*V(1) <A(20) 115+V(1) 20
12 54+10*V(1) -6+-2*V(1) 01 (11)B> 115+V(1) 20
13 56+10*V(1) -4+-2*V(1) 01 11 (22)B> 114+V(1) 20
14 64+12*V(1) 4 01 11 224+V(1) (22)B> 20
15 67+12*V(1) 1 01 11 224+V(1) <B(11) 10
16 75+14*V(1) -7+-2*V(1) 01 11 <B(11) 114+V(1) 10
17 78+14*V(1) -4+-2*V(1) 01 12 (22)B> 114+V(1) 10
18 86+16*V(1) 4 01 12 224+V(1) (22)B> 10
19 92+16*V(1) 6 01 12 224+V(1) 21 (11)B>
20 95+16*V(1) 3 01 12 224+V(1) 21 <A(22)
21 97+16*V(1) 1 01 12 224+V(1) <C(12) 22
22 129+24*V(1) -7+-2*V(1) 01 12 <C(12) 225+V(1)
23 137+24*V(1) -9+-2*V(1) 01 <A(22) 226+V(1)
24 145+24*V(1) -11+-2*V(1) <B(11) 12 226+V(1)
25 149+24*V(1) -13+-2*V(1) <A(20) 11 12 226+V(1)
26 158+24*V(1) -10+-2*V(1) 01 (11)B> 11 12 226+V(1)
27 160+24*V(1) -8+-2*V(1) 01 11 (22)B> 12 226+V(1)
28 165+24*V(1) -11+-2*V(1) 01 11 <B(11) 11 226+V(1)
<< Success! ==> defined new CTR 7 (PPA)
3130 257013 -539 01 11 <B(11) 11 22272
== Executing PA-CTR 5, V(1)=267, V(2)=0, repcount=67, factor=7/4
5542 766615 -941 01 11 <B(11) 11470 224
5543 766618 -938 01 12 (22)B> 11470 224
5544 767558 2 01 12 22470 (22)B> 224
5545 767561 -1 01 12 22470 <B(11) 12 223
5546 768501 -941 01 12 <B(11) 11470 12 223
5547 768506 -938 01 22 (22)B> 11470 12 223
5548 769446 2 01 22471 (22)B> 12 223
5549 769451 -1 01 22471 <B(11) 11 223
5550 770393 -943 01 <B(11) 11472 223
5551 770396 -940 02 (22)B> 11472 223
5552 771340 4 02 22472 (22)B> 223
5553 771343 1 02 22472 <B(11) 12 222
5554 772287 -943 02 <B(11) 11472 12 222
5555 772289 -945 <A(01) 11473 12 222
5556 772302 -942 11 (12)B> 11473 12 222
5557 772304 -940 11 12 (22)B> 11472 12 222
5558 773248 4 11 12 22472 (22)B> 12 222
5559 773253 1 11 12 22472 <B(11) 11 222
5560 774197 -943 11 12 <B(11) 11473 222
5561 774202 -940 11 22 (22)B> 11473 222
5562 775148 6 11 22474 (22)B> 222
5563 775151 3 11 22474 <B(11) 12 22
5564 776099 -945 11 <B(11) 11474 12 22
5565 776102 -942 12 (22)B> 11474 12 22
5566 777050 6 12 22474 (22)B> 12 22
5567 777055 3 12 22474 <B(11) 11 22
5568 778003 -945 12 <B(11) 11475 22
5569 778008 -942 22 (22)B> 11475 22
5570 778958 8 22476 (22)B> 22
5571 778961 5 22476 <B(11) 12
5572 779913 -947 <B(11) 11476 12
5573 779917 -949 <A(20) 11477 12
5574 779926 -946 01 (11)B> 11477 12
5575 779928 -944 01 11 (22)B> 11476 12
5576 780880 8 01 11 22476 (22)B> 12
5577 780885 5 01 11 22476 <B(11) 11
5578 781837 -947 01 11 <B(11) 11477
5579 781840 -944 01 12 (22)B> 11477
5580 782794 10 01 12 22477 (22)B>
5581 782803 7 01 12 22477 <A(22) 20
5582 786619 -947 01 12 <A(22) 22477 20
5583 786623 -949 01 <A(22) 22478 20
5584 786631 -951 <B(11) 12 22478 20
5585 786635 -953 <A(20) 11 12 22478 20
5586 786644 -950 01 (11)B> 11 12 22478 20
5587 786646 -948 01 11 (22)B> 12 22478 20
5588 786651 -951 01 11 <B(11) 11 22478 20
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 11 <B(11) 111+V(1) 224
1 3 3 01 12 (22)B> 111+V(1) 224
2 5+2*V(1) 5+2*V(1) 01 12 221+V(1) (22)B> 224
3 8+2*V(1) 2+2*V(1) 01 12 221+V(1) <B(11) 12 223
4 10+4*V(1) 0 01 12 <B(11) 111+V(1) 12 223
5 15+4*V(1) 3 01 22 (22)B> 111+V(1) 12 223
6 17+6*V(1) 5+2*V(1) 01 222+V(1) (22)B> 12 223
7 22+6*V(1) 2+2*V(1) 01 222+V(1) <B(11) 11 223
8 26+8*V(1) -2 01 <B(11) 113+V(1) 223
9 29+8*V(1) 1 02 (22)B> 113+V(1) 223
10 35+10*V(1) 7+2*V(1) 02 223+V(1) (22)B> 223
11 38+10*V(1) 4+2*V(1) 02 223+V(1) <B(11) 12 222
12 44+12*V(1) -2 02 <B(11) 113+V(1) 12 222
13 46+12*V(1) -4 <A(01) 114+V(1) 12 222
14 59+12*V(1) -1 11 (12)B> 114+V(1) 12 222
15 61+12*V(1) 1 11 12 (22)B> 113+V(1) 12 222
16 67+14*V(1) 7+2*V(1) 11 12 223+V(1) (22)B> 12 222
17 72+14*V(1) 4+2*V(1) 11 12 223+V(1) <B(11) 11 222
18 78+16*V(1) -2 11 12 <B(11) 114+V(1) 222
19 83+16*V(1) 1 11 22 (22)B> 114+V(1) 222
20 91+18*V(1) 9+2*V(1) 11 225+V(1) (22)B> 222
21 94+18*V(1) 6+2*V(1) 11 225+V(1) <B(11) 12 22
22 104+20*V(1) -4 11 <B(11) 115+V(1) 12 22
23 107+20*V(1) -1 12 (22)B> 115+V(1) 12 22
24 117+22*V(1) 9+2*V(1) 12 225+V(1) (22)B> 12 22
25 122+22*V(1) 6+2*V(1) 12 225+V(1) <B(11) 11 22
26 132+24*V(1) -4 12 <B(11) 116+V(1) 22
27 137+24*V(1) -1 22 (22)B> 116+V(1) 22
28 149+26*V(1) 11+2*V(1) 227+V(1) (22)B> 22
29 152+26*V(1) 8+2*V(1) 227+V(1) <B(11) 12
30 166+28*V(1) -6 <B(11) 117+V(1) 12
31 170+28*V(1) -8 <A(20) 118+V(1) 12
32 179+28*V(1) -5 01 (11)B> 118+V(1) 12
33 181+28*V(1) -3 01 11 (22)B> 117+V(1) 12
34 195+30*V(1) 11+2*V(1) 01 11 227+V(1) (22)B> 12
35 200+30*V(1) 8+2*V(1) 01 11 227+V(1) <B(11) 11
36 214+32*V(1) -6 01 11 <B(11) 118+V(1)
37 217+32*V(1) -3 01 12 (22)B> 118+V(1)
38 233+34*V(1) 13+2*V(1) 01 12 228+V(1) (22)B>
39 242+34*V(1) 10+2*V(1) 01 12 228+V(1) <A(22) 20
40 306+42*V(1) -6 01 12 <A(22) 228+V(1) 20
41 310+42*V(1) -8 01 <A(22) 229+V(1) 20
42 318+42*V(1) -10 <B(11) 12 229+V(1) 20
43 322+42*V(1) -12 <A(20) 11 12 229+V(1) 20
44 331+42*V(1) -9 01 (11)B> 11 12 229+V(1) 20
45 333+42*V(1) -7 01 11 (22)B> 12 229+V(1) 20
46 338+42*V(1) -10 01 11 <B(11) 11 229+V(1) 20
<< Success! ==> defined new CTR 8 (PPA)
5588 786651 -951 01 11 <B(11) 11 22478 20
== Executing PA-CTR 2, V(1)=473, V(2)=0, repcount=119, factor=7/4
9872 2384821 -1665 01 11 <B(11) 11834 222 20
9873 2384824 -1662 01 12 (22)B> 11834 222 20
9874 2386492 6 01 12 22834 (22)B> 222 20
9875 2386495 3 01 12 22834 <B(11) 12 22 20
9876 2388163 -1665 01 12 <B(11) 11834 12 22 20
9877 2388168 -1662 01 22 (22)B> 11834 12 22 20
9878 2389836 6 01 22835 (22)B> 12 22 20
9879 2389841 3 01 22835 <B(11) 11 22 20
9880 2391511 -1667 01 <B(11) 11836 22 20
9881 2391514 -1664 02 (22)B> 11836 22 20
9882 2393186 8 02 22836 (22)B> 22 20
9883 2393189 5 02 22836 <B(11) 12 20
9884 2394861 -1667 02 <B(11) 11836 12 20
9885 2394863 -1669 <A(01) 11837 12 20
9886 2394876 -1666 11 (12)B> 11837 12 20
9887 2394878 -1664 11 12 (22)B> 11836 12 20
9888 2396550 8 11 12 22836 (22)B> 12 20
9889 2396555 5 11 12 22836 <B(11) 11 20
9890 2398227 -1667 11 12 <B(11) 11837 20
9891 2398232 -1664 11 22 (22)B> 11837 20
9892 2399906 10 11 22838 (22)B> 20
9893 2399909 7 11 22838 <B(11) 10
9894 2401585 -1669 11 <B(11) 11838 10
9895 2401588 -1666 12 (22)B> 11838 10
9896 2403264 10 12 22838 (22)B> 10
9897 2403270 12 12 22838 21 (11)B>
9898 2403273 9 12 22838 21 <A(22)
9899 2403275 7 12 22838 <C(12) 22
9900 2409979 -1669 12 <C(12) 22839
9901 2409987 -1671 <A(22) 22840
9902 2409995 -1673 <A(01) 11 22840
9903 2410008 -1670 11 (12)B> 11 22840
9904 2410010 -1668 11 12 (22)B> 22840
9905 2410013 -1671 11 12 <B(11) 12 22839
9906 2410018 -1668 11 22 (22)B> 12 22839
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 11 <B(11) 111+V(1) 222 20
1 3 3 01 12 (22)B> 111+V(1) 222 20
2 5+2*V(1) 5+2*V(1) 01 12 221+V(1) (22)B> 222 20
3 8+2*V(1) 2+2*V(1) 01 12 221+V(1) <B(11) 12 22 20
4 10+4*V(1) 0 01 12 <B(11) 111+V(1) 12 22 20
5 15+4*V(1) 3 01 22 (22)B> 111+V(1) 12 22 20
6 17+6*V(1) 5+2*V(1) 01 222+V(1) (22)B> 12 22 20
7 22+6*V(1) 2+2*V(1) 01 222+V(1) <B(11) 11 22 20
8 26+8*V(1) -2 01 <B(11) 113+V(1) 22 20
9 29+8*V(1) 1 02 (22)B> 113+V(1) 22 20
10 35+10*V(1) 7+2*V(1) 02 223+V(1) (22)B> 22 20
11 38+10*V(1) 4+2*V(1) 02 223+V(1) <B(11) 12 20
12 44+12*V(1) -2 02 <B(11) 113+V(1) 12 20
13 46+12*V(1) -4 <A(01) 114+V(1) 12 20
14 59+12*V(1) -1 11 (12)B> 114+V(1) 12 20
15 61+12*V(1) 1 11 12 (22)B> 113+V(1) 12 20
16 67+14*V(1) 7+2*V(1) 11 12 223+V(1) (22)B> 12 20
17 72+14*V(1) 4+2*V(1) 11 12 223+V(1) <B(11) 11 20
18 78+16*V(1) -2 11 12 <B(11) 114+V(1) 20
19 83+16*V(1) 1 11 22 (22)B> 114+V(1) 20
20 91+18*V(1) 9+2*V(1) 11 225+V(1) (22)B> 20
21 94+18*V(1) 6+2*V(1) 11 225+V(1) <B(11) 10
22 104+20*V(1) -4 11 <B(11) 115+V(1) 10
23 107+20*V(1) -1 12 (22)B> 115+V(1) 10
24 117+22*V(1) 9+2*V(1) 12 225+V(1) (22)B> 10
25 123+22*V(1) 11+2*V(1) 12 225+V(1) 21 (11)B>
26 126+22*V(1) 8+2*V(1) 12 225+V(1) 21 <A(22)
27 128+22*V(1) 6+2*V(1) 12 225+V(1) <C(12) 22
28 168+30*V(1) -4 12 <C(12) 226+V(1)
29 176+30*V(1) -6 <A(22) 227+V(1)
30 184+30*V(1) -8 <A(01) 11 227+V(1)
31 197+30*V(1) -5 11 (12)B> 11 227+V(1)
32 199+30*V(1) -3 11 12 (22)B> 227+V(1)
33 202+30*V(1) -6 11 12 <B(11) 12 226+V(1)
34 207+30*V(1) -3 11 22 (22)B> 12 226+V(1)
<< Success! ==> defined new CTR 9 (PPA)
9906 2410018 -1668 11 22 (22)B> 12 22839
== Executing PA-CTR 1, V(1)=0, V(2)=834, repcount=209, factor=7/4
17430 7326534 4 11 221464 (22)B> 12 223
17431 7326539 1 11 221464 <B(11) 11 223
17432 7329467 -2927 11 <B(11) 111465 223
17433 7329470 -2924 12 (22)B> 111465 223
17434 7332400 6 12 221465 (22)B> 223
17435 7332403 3 12 221465 <B(11) 12 222
17436 7335333 -2927 12 <B(11) 111465 12 222
17437 7335338 -2924 22 (22)B> 111465 12 222
17438 7338268 6 221466 (22)B> 12 222
17439 7338273 3 221466 <B(11) 11 222
17440 7341205 -2929 <B(11) 111467 222
17441 7341209 -2931 <A(20) 111468 222
17442 7341218 -2928 01 (11)B> 111468 222
17443 7341220 -2926 01 11 (22)B> 111467 222
17444 7344154 8 01 11 221467 (22)B> 222
17445 7344157 5 01 11 221467 <B(11) 12 22
17446 7347091 -2929 01 11 <B(11) 111467 12 22
17447 7347094 -2926 01 12 (22)B> 111467 12 22
17448 7350028 8 01 12 221467 (22)B> 12 22
17449 7350033 5 01 12 221467 <B(11) 11 22
17450 7352967 -2929 01 12 <B(11) 111468 22
17451 7352972 -2926 01 22 (22)B> 111468 22
17452 7355908 10 01 221469 (22)B> 22
17453 7355911 7 01 221469 <B(11) 12
17454 7358849 -2931 01 <B(11) 111469 12
17455 7358852 -2928 02 (22)B> 111469 12
17456 7361790 10 02 221469 (22)B> 12
17457 7361795 7 02 221469 <B(11) 11
17458 7364733 -2931 02 <B(11) 111470
17459 7364735 -2933 <A(01) 111471
17460 7364748 -2930 11 (12)B> 111471
17461 7364750 -2928 11 12 (22)B> 111470
17462 7367690 12 11 12 221470 (22)B>
17463 7367699 9 11 12 221470 <A(22) 20
17464 7379459 -2931 11 12 <A(22) 221470 20
17465 7379463 -2933 11 <A(22) 221471 20
17466 7379465 -2935 <A(22) 221472 20
17467 7379473 -2937 <A(01) 11 221472 20
17468 7379486 -2934 11 (12)B> 11 221472 20
17469 7379488 -2932 11 12 (22)B> 221472 20
17470 7379491 -2935 11 12 <B(11) 12 221471 20
17471 7379496 -2932 11 22 (22)B> 12 221471 20
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 11 221+V(1) (22)B> 12 223
1 5 -3 11 221+V(1) <B(11) 11 223
2 7+2*V(1) -5+-2*V(1) 11 <B(11) 112+V(1) 223
3 10+2*V(1) -2+-2*V(1) 12 (22)B> 112+V(1) 223
4 14+4*V(1) 2 12 222+V(1) (22)B> 223
5 17+4*V(1) -1 12 222+V(1) <B(11) 12 222
6 21+6*V(1) -5+-2*V(1) 12 <B(11) 112+V(1) 12 222
7 26+6*V(1) -2+-2*V(1) 22 (22)B> 112+V(1) 12 222
8 30+8*V(1) 2 223+V(1) (22)B> 12 222
9 35+8*V(1) -1 223+V(1) <B(11) 11 222
10 41+10*V(1) -7+-2*V(1) <B(11) 114+V(1) 222
11 45+10*V(1) -9+-2*V(1) <A(20) 115+V(1) 222
12 54+10*V(1) -6+-2*V(1) 01 (11)B> 115+V(1) 222
13 56+10*V(1) -4+-2*V(1) 01 11 (22)B> 114+V(1) 222
14 64+12*V(1) 4 01 11 224+V(1) (22)B> 222
15 67+12*V(1) 1 01 11 224+V(1) <B(11) 12 22
16 75+14*V(1) -7+-2*V(1) 01 11 <B(11) 114+V(1) 12 22
17 78+14*V(1) -4+-2*V(1) 01 12 (22)B> 114+V(1) 12 22
18 86+16*V(1) 4 01 12 224+V(1) (22)B> 12 22
19 91+16*V(1) 1 01 12 224+V(1) <B(11) 11 22
20 99+18*V(1) -7+-2*V(1) 01 12 <B(11) 115+V(1) 22
21 104+18*V(1) -4+-2*V(1) 01 22 (22)B> 115+V(1) 22
22 114+20*V(1) 6 01 226+V(1) (22)B> 22
23 117+20*V(1) 3 01 226+V(1) <B(11) 12
24 129+22*V(1) -9+-2*V(1) 01 <B(11) 116+V(1) 12
25 132+22*V(1) -6+-2*V(1) 02 (22)B> 116+V(1) 12
26 144+24*V(1) 6 02 226+V(1) (22)B> 12
27 149+24*V(1) 3 02 226+V(1) <B(11) 11
28 161+26*V(1) -9+-2*V(1) 02 <B(11) 117+V(1)
29 163+26*V(1) -11+-2*V(1) <A(01) 118+V(1)
30 176+26*V(1) -8+-2*V(1) 11 (12)B> 118+V(1)
31 178+26*V(1) -6+-2*V(1) 11 12 (22)B> 117+V(1)
32 192+28*V(1) 8 11 12 227+V(1) (22)B>
33 201+28*V(1) 5 11 12 227+V(1) <A(22) 20
34 257+36*V(1) -9+-2*V(1) 11 12 <A(22) 227+V(1) 20
35 261+36*V(1) -11+-2*V(1) 11 <A(22) 228+V(1) 20
36 263+36*V(1) -13+-2*V(1) <A(22) 229+V(1) 20
37 271+36*V(1) -15+-2*V(1) <A(01) 11 229+V(1) 20
38 284+36*V(1) -12+-2*V(1) 11 (12)B> 11 229+V(1) 20
39 286+36*V(1) -10+-2*V(1) 11 12 (22)B> 229+V(1) 20
40 289+36*V(1) -13+-2*V(1) 11 12 <B(11) 12 228+V(1) 20
41 294+36*V(1) -10+-2*V(1) 11 22 (22)B> 12 228+V(1) 20
<< Success! ==> defined new CTR 10 (PPA)
17471 7379496 -2932 11 22 (22)B> 12 221471 20
== Executing PA-CTR 6, V(1)=0, V(2)=1466, repcount=367, factor=7/4
30683 22507236 4 11 222570 (22)B> 12 223 20
30684 22507241 1 11 222570 <B(11) 11 223 20
30685 22512381 -5139 11 <B(11) 112571 223 20
30686 22512384 -5136 12 (22)B> 112571 223 20
30687 22517526 6 12 222571 (22)B> 223 20
30688 22517529 3 12 222571 <B(11) 12 222 20
30689 22522671 -5139 12 <B(11) 112571 12 222 20
30690 22522676 -5136 22 (22)B> 112571 12 222 20
30691 22527818 6 222572 (22)B> 12 222 20
30692 22527823 3 222572 <B(11) 11 222 20
30693 22532967 -5141 <B(11) 112573 222 20
30694 22532971 -5143 <A(20) 112574 222 20
30695 22532980 -5140 01 (11)B> 112574 222 20
30696 22532982 -5138 01 11 (22)B> 112573 222 20
30697 22538128 8 01 11 222573 (22)B> 222 20
30698 22538131 5 01 11 222573 <B(11) 12 22 20
30699 22543277 -5141 01 11 <B(11) 112573 12 22 20
30700 22543280 -5138 01 12 (22)B> 112573 12 22 20
30701 22548426 8 01 12 222573 (22)B> 12 22 20
30702 22548431 5 01 12 222573 <B(11) 11 22 20
30703 22553577 -5141 01 12 <B(11) 112574 22 20
30704 22553582 -5138 01 22 (22)B> 112574 22 20
30705 22558730 10 01 222575 (22)B> 22 20
30706 22558733 7 01 222575 <B(11) 12 20
30707 22563883 -5143 01 <B(11) 112575 12 20
30708 22563886 -5140 02 (22)B> 112575 12 20
30709 22569036 10 02 222575 (22)B> 12 20
30710 22569041 7 02 222575 <B(11) 11 20
30711 22574191 -5143 02 <B(11) 112576 20
30712 22574193 -5145 <A(01) 112577 20
30713 22574206 -5142 11 (12)B> 112577 20
30714 22574208 -5140 11 12 (22)B> 112576 20
30715 22579360 12 11 12 222576 (22)B> 20
30716 22579363 9 11 12 222576 <B(11) 10
30717 22584515 -5143 11 12 <B(11) 112576 10
30718 22584520 -5140 11 22 (22)B> 112576 10
30719 22589672 12 11 222577 (22)B> 10
30720 22589678 14 11 222577 21 (11)B>
30721 22589681 11 11 222577 21 <A(22)
30722 22589683 9 11 222577 <C(12) 22
30723 22610299 -5145 11 <C(12) 222578
30724 22610303 -5147 <A(22) 222579
30725 22610311 -5149 <A(01) 11 222579
30726 22610324 -5146 11 (12)B> 11 222579
30727 22610326 -5144 11 12 (22)B> 222579
30728 22610329 -5147 11 12 <B(11) 12 222578
30729 22610334 -5144 11 22 (22)B> 12 222578
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 11 221+V(1) (22)B> 12 223 20
1 5 -3 11 221+V(1) <B(11) 11 223 20
2 7+2*V(1) -5+-2*V(1) 11 <B(11) 112+V(1) 223 20
3 10+2*V(1) -2+-2*V(1) 12 (22)B> 112+V(1) 223 20
4 14+4*V(1) 2 12 222+V(1) (22)B> 223 20
5 17+4*V(1) -1 12 222+V(1) <B(11) 12 222 20
6 21+6*V(1) -5+-2*V(1) 12 <B(11) 112+V(1) 12 222 20
7 26+6*V(1) -2+-2*V(1) 22 (22)B> 112+V(1) 12 222 20
8 30+8*V(1) 2 223+V(1) (22)B> 12 222 20
9 35+8*V(1) -1 223+V(1) <B(11) 11 222 20
10 41+10*V(1) -7+-2*V(1) <B(11) 114+V(1) 222 20
11 45+10*V(1) -9+-2*V(1) <A(20) 115+V(1) 222 20
12 54+10*V(1) -6+-2*V(1) 01 (11)B> 115+V(1) 222 20
13 56+10*V(1) -4+-2*V(1) 01 11 (22)B> 114+V(1) 222 20
14 64+12*V(1) 4 01 11 224+V(1) (22)B> 222 20
15 67+12*V(1) 1 01 11 224+V(1) <B(11) 12 22 20
16 75+14*V(1) -7+-2*V(1) 01 11 <B(11) 114+V(1) 12 22 20
17 78+14*V(1) -4+-2*V(1) 01 12 (22)B> 114+V(1) 12 22 20
18 86+16*V(1) 4 01 12 224+V(1) (22)B> 12 22 20
19 91+16*V(1) 1 01 12 224+V(1) <B(11) 11 22 20
20 99+18*V(1) -7+-2*V(1) 01 12 <B(11) 115+V(1) 22 20
21 104+18*V(1) -4+-2*V(1) 01 22 (22)B> 115+V(1) 22 20
22 114+20*V(1) 6 01 226+V(1) (22)B> 22 20
23 117+20*V(1) 3 01 226+V(1) <B(11) 12 20
24 129+22*V(1) -9+-2*V(1) 01 <B(11) 116+V(1) 12 20
25 132+22*V(1) -6+-2*V(1) 02 (22)B> 116+V(1) 12 20
26 144+24*V(1) 6 02 226+V(1) (22)B> 12 20
27 149+24*V(1) 3 02 226+V(1) <B(11) 11 20
28 161+26*V(1) -9+-2*V(1) 02 <B(11) 117+V(1) 20
29 163+26*V(1) -11+-2*V(1) <A(01) 118+V(1) 20
30 176+26*V(1) -8+-2*V(1) 11 (12)B> 118+V(1) 20
31 178+26*V(1) -6+-2*V(1) 11 12 (22)B> 117+V(1) 20
32 192+28*V(1) 8 11 12 227+V(1) (22)B> 20
33 195+28*V(1) 5 11 12 227+V(1) <B(11) 10
34 209+30*V(1) -9+-2*V(1) 11 12 <B(11) 117+V(1) 10
35 214+30*V(1) -6+-2*V(1) 11 22 (22)B> 117+V(1) 10
36 228+32*V(1) 8 11 228+V(1) (22)B> 10
37 234+32*V(1) 10 11 228+V(1) 21 (11)B>
38 237+32*V(1) 7 11 228+V(1) 21 <A(22)
39 239+32*V(1) 5 11 228+V(1) <C(12) 22
40 303+40*V(1) -11+-2*V(1) 11 <C(12) 229+V(1)
41 307+40*V(1) -13+-2*V(1) <A(22) 2210+V(1)
42 315+40*V(1) -15+-2*V(1) <A(01) 11 2210+V(1)
43 328+40*V(1) -12+-2*V(1) 11 (12)B> 11 2210+V(1)
44 330+40*V(1) -10+-2*V(1) 11 12 (22)B> 2210+V(1)
45 333+40*V(1) -13+-2*V(1) 11 12 <B(11) 12 229+V(1)
46 338+40*V(1) -10+-2*V(1) 11 22 (22)B> 12 229+V(1)
<< Success! ==> defined new CTR 11 (PPA)
30729 22610334 -5144 11 22 (22)B> 12 222578
== Executing PA-CTR 1, V(1)=0, V(2)=2573, repcount=644, factor=7/4
53913 69135470 8 11 224509 (22)B> 12 222
== Executing PPA-CTR 4 (once), V(1)=4508
53942 69261893 -9019 01 11 <B(11) 11 224514 20
== Executing PA-CTR 2, V(1)=4509, V(2)=0, repcount=1128, factor=7/4
94550 211883957 -15787 01 11 <B(11) 117897 222 20
== Executing PPA-CTR 9 (once), V(1)=7896
94584 212121044 -15790 11 22 (22)B> 12 227902
== Executing PA-CTR 1, V(1)=0, V(2)=7897, repcount=1975, factor=7/4
165684 649220144 10 11 2213826 (22)B> 12 222
== Executing PPA-CTR 4 (once), V(1)=13825
165713 649607443 -27651 01 11 <B(11) 11 2213831 20
== Executing PA-CTR 2, V(1)=13826, V(2)=0, repcount=3457, factor=7/4
290165 1988455145 -48393 01 11 <B(11) 1124200 223 20
290166 1988455148 -48390 01 12 (22)B> 1124200 223 20
290167 1988503548 10 01 12 2224200 (22)B> 223 20
290168 1988503551 7 01 12 2224200 <B(11) 12 222 20
290169 1988551951 -48393 01 12 <B(11) 1124200 12 222 20
290170 1988551956 -48390 01 22 (22)B> 1124200 12 222 20
290171 1988600356 10 01 2224201 (22)B> 12 222 20
290172 1988600361 7 01 2224201 <B(11) 11 222 20
290173 1988648763 -48395 01 <B(11) 1124202 222 20
290174 1988648766 -48392 02 (22)B> 1124202 222 20
290175 1988697170 12 02 2224202 (22)B> 222 20
290176 1988697173 9 02 2224202 <B(11) 12 22 20
290177 1988745577 -48395 02 <B(11) 1124202 12 22 20
290178 1988745579 -48397 <A(01) 1124203 12 22 20
290179 1988745592 -48394 11 (12)B> 1124203 12 22 20
290180 1988745594 -48392 11 12 (22)B> 1124202 12 22 20
290181 1988793998 12 11 12 2224202 (22)B> 12 22 20
290182 1988794003 9 11 12 2224202 <B(11) 11 22 20
290183 1988842407 -48395 11 12 <B(11) 1124203 22 20
290184 1988842412 -48392 11 22 (22)B> 1124203 22 20
290185 1988890818 14 11 2224204 (22)B> 22 20
290186 1988890821 11 11 2224204 <B(11) 12 20
290187 1988939229 -48397 11 <B(11) 1124204 12 20
290188 1988939232 -48394 12 (22)B> 1124204 12 20
290189 1988987640 14 12 2224204 (22)B> 12 20
290190 1988987645 11 12 2224204 <B(11) 11 20
290191 1989036053 -48397 12 <B(11) 1124205 20
290192 1989036058 -48394 22 (22)B> 1124205 20
290193 1989084468 16 2224206 (22)B> 20
290194 1989084471 13 2224206 <B(11) 10
290195 1989132883 -48399 <B(11) 1124206 10
290196 1989132887 -48401 <A(20) 1124207 10
290197 1989132896 -48398 01 (11)B> 1124207 10
290198 1989132898 -48396 01 11 (22)B> 1124206 10
290199 1989181310 16 01 11 2224206 (22)B> 10
290200 1989181316 18 01 11 2224206 21 (11)B>
290201 1989181319 15 01 11 2224206 21 <A(22)
290202 1989181321 13 01 11 2224206 <C(12) 22
290203 1989374969 -48399 01 11 <C(12) 2224207
290204 1989374973 -48401 01 <A(22) 2224208
290205 1989374981 -48403 <B(11) 12 2224208
290206 1989374985 -48405 <A(20) 11 12 2224208
290207 1989374994 -48402 01 (11)B> 11 12 2224208
290208 1989374996 -48400 01 11 (22)B> 12 2224208
290209 1989375001 -48403 01 11 <B(11) 11 2224208
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 11 <B(11) 111+V(1) 223 20
1 3 3 01 12 (22)B> 111+V(1) 223 20
2 5+2*V(1) 5+2*V(1) 01 12 221+V(1) (22)B> 223 20
3 8+2*V(1) 2+2*V(1) 01 12 221+V(1) <B(11) 12 222 20
4 10+4*V(1) 0 01 12 <B(11) 111+V(1) 12 222 20
5 15+4*V(1) 3 01 22 (22)B> 111+V(1) 12 222 20
6 17+6*V(1) 5+2*V(1) 01 222+V(1) (22)B> 12 222 20
7 22+6*V(1) 2+2*V(1) 01 222+V(1) <B(11) 11 222 20
8 26+8*V(1) -2 01 <B(11) 113+V(1) 222 20
9 29+8*V(1) 1 02 (22)B> 113+V(1) 222 20
10 35+10*V(1) 7+2*V(1) 02 223+V(1) (22)B> 222 20
11 38+10*V(1) 4+2*V(1) 02 223+V(1) <B(11) 12 22 20
12 44+12*V(1) -2 02 <B(11) 113+V(1) 12 22 20
13 46+12*V(1) -4 <A(01) 114+V(1) 12 22 20
14 59+12*V(1) -1 11 (12)B> 114+V(1) 12 22 20
15 61+12*V(1) 1 11 12 (22)B> 113+V(1) 12 22 20
16 67+14*V(1) 7+2*V(1) 11 12 223+V(1) (22)B> 12 22 20
17 72+14*V(1) 4+2*V(1) 11 12 223+V(1) <B(11) 11 22 20
18 78+16*V(1) -2 11 12 <B(11) 114+V(1) 22 20
19 83+16*V(1) 1 11 22 (22)B> 114+V(1) 22 20
20 91+18*V(1) 9+2*V(1) 11 225+V(1) (22)B> 22 20
21 94+18*V(1) 6+2*V(1) 11 225+V(1) <B(11) 12 20
22 104+20*V(1) -4 11 <B(11) 115+V(1) 12 20
23 107+20*V(1) -1 12 (22)B> 115+V(1) 12 20
24 117+22*V(1) 9+2*V(1) 12 225+V(1) (22)B> 12 20
25 122+22*V(1) 6+2*V(1) 12 225+V(1) <B(11) 11 20
26 132+24*V(1) -4 12 <B(11) 116+V(1) 20
27 137+24*V(1) -1 22 (22)B> 116+V(1) 20
28 149+26*V(1) 11+2*V(1) 227+V(1) (22)B> 20
29 152+26*V(1) 8+2*V(1) 227+V(1) <B(11) 10
30 166+28*V(1) -6 <B(11) 117+V(1) 10
31 170+28*V(1) -8 <A(20) 118+V(1) 10
32 179+28*V(1) -5 01 (11)B> 118+V(1) 10
33 181+28*V(1) -3 01 11 (22)B> 117+V(1) 10
34 195+30*V(1) 11+2*V(1) 01 11 227+V(1) (22)B> 10
35 201+30*V(1) 13+2*V(1) 01 11 227+V(1) 21 (11)B>
36 204+30*V(1) 10+2*V(1) 01 11 227+V(1) 21 <A(22)
37 206+30*V(1) 8+2*V(1) 01 11 227+V(1) <C(12) 22
38 262+38*V(1) -6 01 11 <C(12) 228+V(1)
39 266+38*V(1) -8 01 <A(22) 229+V(1)
40 274+38*V(1) -10 <B(11) 12 229+V(1)
41 278+38*V(1) -12 <A(20) 11 12 229+V(1)
42 287+38*V(1) -9 01 (11)B> 11 12 229+V(1)
43 289+38*V(1) -7 01 11 (22)B> 12 229+V(1)
44 294+38*V(1) -10 01 11 <B(11) 11 229+V(1)
<< Success! ==> defined new CTR 12 (PPA)
290209 1989375001 -48403 01 11 <B(11) 11 2224208
== Executing PA-CTR 5, V(1)=24203, V(2)=0, repcount=6051, factor=7/4
508045 6090827515 -84709 01 11 <B(11) 1142358 224
== Executing PPA-CTR 8 (once), V(1)=42357
508091 6092606847 -84719 01 11 <B(11) 11 2242366 20
== Executing PA-CTR 2, V(1)=42361, V(2)=0, repcount=10591, factor=7/4
889367 18656646601 -148265 01 11 <B(11) 1174138 222 20
== Executing PPA-CTR 9 (once), V(1)=74137
889401 18658870918 -148268 11 22 (22)B> 12 2274143
== Executing PA-CTR 1, V(1)=0, V(2)=74138, repcount=18535, factor=7/4
1556661 57138198178 12 11 22129746 (22)B> 12 223
== Executing PPA-CTR 10 (once), V(1)=129745
1556702 57142869292 -259488 11 22 (22)B> 12 22129753 20
== Executing PA-CTR 6, V(1)=0, V(2)=129748, repcount=32438, factor=7/4
2724470 174995702628 16 11 22227067 (22)B> 12 22 20
== Executing PPA-CTR 7 (once), V(1)=227066
2724498 175001152377 -454127 01 11 <B(11) 11 22227072
== Executing PA-CTR 5, V(1)=227067, V(2)=0, repcount=56767, factor=7/4
4768110 535926078979 -794729 01 11 <B(11) 11397370 224
== Executing PPA-CTR 8 (once), V(1)=397369
4768156 535942768815 -794739 01 11 <B(11) 11 22397378 20
== Executing PA-CTR 2, V(1)=397373, V(2)=0, repcount=99344, factor=7/4
8344540 1641306699535 -1390803 01 11 <B(11) 11695409 222 20
== Executing PPA-CTR 9 (once), V(1)=695408
8344574 1641327561982 -1390806 11 22 (22)B> 12 22695414
== Executing PA-CTR 1, V(1)=0, V(2)=695409, repcount=173853, factor=7/4
14603282 5026532677138 18 11 221216972 (22)B> 12 222
== Executing PPA-CTR 4 (once), V(1)=1216971
14603311 5026566752525 -2433935 01 11 <B(11) 11 221216977 20
== Executing PA-CTR 2, V(1)=1216972, V(2)=0, repcount=304244, factor=7/4
25556095 15393811877445 -4259399 01 11 <B(11) 112129709 22 20
== Executing PPA-CTR 3 (once), V(1)=2129708
25556122 15393858731164 -4259402 11 22 (22)B> 12 222129713
== Executing PA-CTR 1, V(1)=0, V(2)=2129708, repcount=532428, factor=7/4
44723530 47143632913420 22 11 223726997 (22)B> 12 22
44723531 47143632913425 19 11 223726997 <B(11) 11 22
44723532 47143640367419 -7453975 11 <B(11) 113726998 22
44723533 47143640367422 -7453972 12 (22)B> 113726998 22
44723534 47143647821418 24 12 223726998 (22)B> 22
44723535 47143647821421 21 12 223726998 <B(11) 12
44723536 47143655275417 -7453975 12 <B(11) 113726998 12
44723537 47143655275422 -7453972 22 (22)B> 113726998 12
44723538 47143662729418 24 223726999 (22)B> 12
44723539 47143662729423 21 223726999 <B(11) 11
44723540 47143670183421 -7453977 <B(11) 113727000
44723541 47143670183425 -7453979 <A(20) 113727001
44723542 47143670183434 -7453976 01 (11)B> 113727001
44723543 47143670183436 -7453974 01 11 (22)B> 113727000
44723544 47143677637436 26 01 11 223727000 (22)B>
44723545 47143677637445 23 01 11 223727000 <A(22) 20
44723546 47143707453445 -7453977 01 11 <A(22) 223727000 20
44723547 47143707453447 -7453979 01 <A(22) 223727001 20
44723548 47143707453455 -7453981 <B(11) 12 223727001 20
44723549 47143707453459 -7453983 <A(20) 11 12 223727001 20
44723550 47143707453468 -7453980 01 (11)B> 11 12 223727001 20
44723551 47143707453470 -7453978 01 11 (22)B> 12 223727001 20
44723552 47143707453475 -7453981 01 11 <B(11) 11 223727001 20
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 11 221+V(1) (22)B> 12 22
1 5 -3 11 221+V(1) <B(11) 11 22
2 7+2*V(1) -5+-2*V(1) 11 <B(11) 112+V(1) 22
3 10+2*V(1) -2+-2*V(1) 12 (22)B> 112+V(1) 22
4 14+4*V(1) 2 12 222+V(1) (22)B> 22
5 17+4*V(1) -1 12 222+V(1) <B(11) 12
6 21+6*V(1) -5+-2*V(1) 12 <B(11) 112+V(1) 12
7 26+6*V(1) -2+-2*V(1) 22 (22)B> 112+V(1) 12
8 30+8*V(1) 2 223+V(1) (22)B> 12
9 35+8*V(1) -1 223+V(1) <B(11) 11
10 41+10*V(1) -7+-2*V(1) <B(11) 114+V(1)
11 45+10*V(1) -9+-2*V(1) <A(20) 115+V(1)
12 54+10*V(1) -6+-2*V(1) 01 (11)B> 115+V(1)
13 56+10*V(1) -4+-2*V(1) 01 11 (22)B> 114+V(1)
14 64+12*V(1) 4 01 11 224+V(1) (22)B>
15 73+12*V(1) 1 01 11 224+V(1) <A(22) 20
16 105+20*V(1) -7+-2*V(1) 01 11 <A(22) 224+V(1) 20
17 107+20*V(1) -9+-2*V(1) 01 <A(22) 225+V(1) 20
18 115+20*V(1) -11+-2*V(1) <B(11) 12 225+V(1) 20
19 119+20*V(1) -13+-2*V(1) <A(20) 11 12 225+V(1) 20
20 128+20*V(1) -10+-2*V(1) 01 (11)B> 11 12 225+V(1) 20
21 130+20*V(1) -8+-2*V(1) 01 11 (22)B> 12 225+V(1) 20
22 135+20*V(1) -11+-2*V(1) 01 11 <B(11) 11 225+V(1) 20
<< Success! ==> defined new CTR 13 (PPA)
44723552 47143707453475 -7453981 01 11 <B(11) 11 223727001 20
== Executing PA-CTR 2, V(1)=3726996, V(2)=0, repcount=931750, factor=7/4
78266552 144377505491975 -13044481 01 11 <B(11) 116522251 22 20
== Executing PPA-CTR 3 (once), V(1)=6522250
78266579 144377648981618 -13044484 11 22 (22)B> 12 226522255
== Executing PA-CTR 1, V(1)=0, V(2)=6522250, repcount=1630563, factor=7/4
136966847 442156236187454 20 11 2211413942 (22)B> 12 223
== Executing PPA-CTR 10 (once), V(1)=11413941
136966888 442156647089624 -22827872 11 22 (22)B> 12 2211413949 20
== Executing PA-CTR 6, V(1)=0, V(2)=11413944, repcount=2853487, factor=7/4
239692420 1354104440721044 24 11 2219974410 (22)B> 12 22 20
== Executing PPA-CTR 7 (once), V(1)=19974409
239692448 1354104920107025 -39948805 01 11 <B(11) 11 2219974415
== Executing PA-CTR 5, V(1)=19974410, V(2)=0, repcount=4993603, factor=7/4
419462156 4146945372674739 -69910423 01 11 <B(11) 1134955222 223
419462157 4146945372674742 -69910420 01 12 (22)B> 1134955222 223
419462158 4146945442585186 24 01 12 2234955222 (22)B> 223
419462159 4146945442585189 21 01 12 2234955222 <B(11) 12 222
419462160 4146945512495633 -69910423 01 12 <B(11) 1134955222 12 222
419462161 4146945512495638 -69910420 01 22 (22)B> 1134955222 12 222
419462162 4146945582406082 24 01 2234955223 (22)B> 12 222
419462163 4146945582406087 21 01 2234955223 <B(11) 11 222
419462164 4146945652316533 -69910425 01 <B(11) 1134955224 222
419462165 4146945652316536 -69910422 02 (22)B> 1134955224 222
419462166 4146945722226984 26 02 2234955224 (22)B> 222
419462167 4146945722226987 23 02 2234955224 <B(11) 12 22
419462168 4146945792137435 -69910425 02 <B(11) 1134955224 12 22
419462169 4146945792137437 -69910427 <A(01) 1134955225 12 22
419462170 4146945792137450 -69910424 11 (12)B> 1134955225 12 22
419462171 4146945792137452 -69910422 11 12 (22)B> 1134955224 12 22
419462172 4146945862047900 26 11 12 2234955224 (22)B> 12 22
419462173 4146945862047905 23 11 12 2234955224 <B(11) 11 22
419462174 4146945931958353 -69910425 11 12 <B(11) 1134955225 22
419462175 4146945931958358 -69910422 11 22 (22)B> 1134955225 22
419462176 4146946001868808 28 11 2234955226 (22)B> 22
419462177 4146946001868811 25 11 2234955226 <B(11) 12
419462178 4146946071779263 -69910427 11 <B(11) 1134955226 12
419462179 4146946071779266 -69910424 12 (22)B> 1134955226 12
419462180 4146946141689718 28 12 2234955226 (22)B> 12
419462181 4146946141689723 25 12 2234955226 <B(11) 11
419462182 4146946211600175 -69910427 12 <B(11) 1134955227
419462183 4146946211600180 -69910424 22 (22)B> 1134955227
419462184 4146946281510634 30 2234955228 (22)B>
419462185 4146946281510643 27 2234955228 <A(22) 20
419462186 4146946561152467 -69910429 <A(22) 2234955228 20
419462187 4146946561152475 -69910431 <A(01) 11 2234955228 20
419462188 4146946561152488 -69910428 11 (12)B> 11 2234955228 20
419462189 4146946561152490 -69910426 11 12 (22)B> 2234955228 20
419462190 4146946561152493 -69910429 11 12 <B(11) 12 2234955227 20
419462191 4146946561152498 -69910426 11 22 (22)B> 12 2234955227 20
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 11 <B(11) 111+V(1) 223
1 3 3 01 12 (22)B> 111+V(1) 223
2 5+2*V(1) 5+2*V(1) 01 12 221+V(1) (22)B> 223
3 8+2*V(1) 2+2*V(1) 01 12 221+V(1) <B(11) 12 222
4 10+4*V(1) 0 01 12 <B(11) 111+V(1) 12 222
5 15+4*V(1) 3 01 22 (22)B> 111+V(1) 12 222
6 17+6*V(1) 5+2*V(1) 01 222+V(1) (22)B> 12 222
7 22+6*V(1) 2+2*V(1) 01 222+V(1) <B(11) 11 222
8 26+8*V(1) -2 01 <B(11) 113+V(1) 222
9 29+8*V(1) 1 02 (22)B> 113+V(1) 222
10 35+10*V(1) 7+2*V(1) 02 223+V(1) (22)B> 222
11 38+10*V(1) 4+2*V(1) 02 223+V(1) <B(11) 12 22
12 44+12*V(1) -2 02 <B(11) 113+V(1) 12 22
13 46+12*V(1) -4 <A(01) 114+V(1) 12 22
14 59+12*V(1) -1 11 (12)B> 114+V(1) 12 22
15 61+12*V(1) 1 11 12 (22)B> 113+V(1) 12 22
16 67+14*V(1) 7+2*V(1) 11 12 223+V(1) (22)B> 12 22
17 72+14*V(1) 4+2*V(1) 11 12 223+V(1) <B(11) 11 22
18 78+16*V(1) -2 11 12 <B(11) 114+V(1) 22
19 83+16*V(1) 1 11 22 (22)B> 114+V(1) 22
20 91+18*V(1) 9+2*V(1) 11 225+V(1) (22)B> 22
21 94+18*V(1) 6+2*V(1) 11 225+V(1) <B(11) 12
22 104+20*V(1) -4 11 <B(11) 115+V(1) 12
23 107+20*V(1) -1 12 (22)B> 115+V(1) 12
24 117+22*V(1) 9+2*V(1) 12 225+V(1) (22)B> 12
25 122+22*V(1) 6+2*V(1) 12 225+V(1) <B(11) 11
26 132+24*V(1) -4 12 <B(11) 116+V(1)
27 137+24*V(1) -1 22 (22)B> 116+V(1)
28 149+26*V(1) 11+2*V(1) 227+V(1) (22)B>
29 158+26*V(1) 8+2*V(1) 227+V(1) <A(22) 20
30 214+34*V(1) -6 <A(22) 227+V(1) 20
31 222+34*V(1) -8 <A(01) 11 227+V(1) 20
32 235+34*V(1) -5 11 (12)B> 11 227+V(1) 20
33 237+34*V(1) -3 11 12 (22)B> 227+V(1) 20
34 240+34*V(1) -6 11 12 <B(11) 12 226+V(1) 20
35 245+34*V(1) -3 11 22 (22)B> 12 226+V(1) 20
<< Success! ==> defined new CTR 14 (PPA)
419462191 4146946561152498 -69910426 11 22 (22)B> 12 2234955227 20
== Executing PA-CTR 6, V(1)=0, V(2)=34955222, repcount=8738806, factor=7/4
734059207 12700021369085226 22 11 2261171643 (22)B> 12 223 20
== Executing PPA-CTR 11 (once), V(1)=61171642
734059253 12700023815951244 -122343272 11 22 (22)B> 12 2261171651
== Executing PA-CTR 1, V(1)=0, V(2)=61171646, repcount=15292912, factor=7/4
1284604085 38893819223180364 24 11 22107050385 (22)B> 12 223
== Executing PPA-CTR 10 (once), V(1)=107050384
1284604126 38893823076994482 -214100754 11 22 (22)B> 12 22107050392 20
== Executing PA-CTR 6, V(1)=0, V(2)=107050387, repcount=26762597, factor=7/4
2248057618 119112325178109542 22 11 22187338180 (22)B> 12 224 20
2248057619 119112325178109547 19 11 22187338180 <B(11) 11 224 20
2248057620 119112325552785907 -374676341 11 <B(11) 11187338181 224 20
2248057621 119112325552785910 -374676338 12 (22)B> 11187338181 224 20
2248057622 119112325927462272 24 12 22187338181 (22)B> 224 20
2248057623 119112325927462275 21 12 22187338181 <B(11) 12 223 20
2248057624 119112326302138637 -374676341 12 <B(11) 11187338181 12 223 20
2248057625 119112326302138642 -374676338 22 (22)B> 11187338181 12 223 20
2248057626 119112326676815004 24 22187338182 (22)B> 12 223 20
2248057627 119112326676815009 21 22187338182 <B(11) 11 223 20
2248057628 119112327051491373 -374676343 <B(11) 11187338183 223 20
2248057629 119112327051491377 -374676345 <A(20) 11187338184 223 20
2248057630 119112327051491386 -374676342 01 (11)B> 11187338184 223 20
2248057631 119112327051491388 -374676340 01 11 (22)B> 11187338183 223 20
2248057632 119112327426167754 26 01 11 22187338183 (22)B> 223 20
2248057633 119112327426167757 23 01 11 22187338183 <B(11) 12 222 20
2248057634 119112327800844123 -374676343 01 11 <B(11) 11187338183 12 222 20
2248057635 119112327800844126 -374676340 01 12 (22)B> 11187338183 12 222 20
2248057636 119112328175520492 26 01 12 22187338183 (22)B> 12 222 20
2248057637 119112328175520497 23 01 12 22187338183 <B(11) 11 222 20
2248057638 119112328550196863 -374676343 01 12 <B(11) 11187338184 222 20
2248057639 119112328550196868 -374676340 01 22 (22)B> 11187338184 222 20
2248057640 119112328924873236 28 01 22187338185 (22)B> 222 20
2248057641 119112328924873239 25 01 22187338185 <B(11) 12 22 20
2248057642 119112329299549609 -374676345 01 <B(11) 11187338185 12 22 20
2248057643 119112329299549612 -374676342 02 (22)B> 11187338185 12 22 20
2248057644 119112329674225982 28 02 22187338185 (22)B> 12 22 20
2248057645 119112329674225987 25 02 22187338185 <B(11) 11 22 20
2248057646 119112330048902357 -374676345 02 <B(11) 11187338186 22 20
2248057647 119112330048902359 -374676347 <A(01) 11187338187 22 20
2248057648 119112330048902372 -374676344 11 (12)B> 11187338187 22 20
2248057649 119112330048902374 -374676342 11 12 (22)B> 11187338186 22 20
2248057650 119112330423578746 30 11 12 22187338186 (22)B> 22 20
2248057651 119112330423578749 27 11 12 22187338186 <B(11) 12 20
2248057652 119112330798255121 -374676345 11 12 <B(11) 11187338186 12 20
2248057653 119112330798255126 -374676342 11 22 (22)B> 11187338186 12 20
2248057654 119112331172931498 30 11 22187338187 (22)B> 12 20
2248057655 119112331172931503 27 11 22187338187 <B(11) 11 20
2248057656 119112331547607877 -374676347 11 <B(11) 11187338188 20
2248057657 119112331547607880 -374676344 12 (22)B> 11187338188 20
2248057658 119112331922284256 32 12 22187338188 (22)B> 20
2248057659 119112331922284259 29 12 22187338188 <B(11) 10
2248057660 119112332296960635 -374676347 12 <B(11) 11187338188 10
2248057661 119112332296960640 -374676344 22 (22)B> 11187338188 10
2248057662 119112332671637016 32 22187338189 (22)B> 10
2248057663 119112332671637022 34 22187338189 21 (11)B>
2248057664 119112332671637025 31 22187338189 21 <A(22)
2248057665 119112332671637027 29 22187338189 <C(12) 22
2248057666 119112334170342539 -374676349 <C(12) 22187338190
2248057667 119112334170342540 -374676348 01 H> 12 22187338190 [stop]
Lines: 757
Top steps: 756
Macro steps: 2248057667
Basic steps: 119112334170342540
Tape index: -374676348
nonzeros: 374676383
log10(nonzeros): 8.574
log10(steps ): 17.076
Run state: stop
Input to awk program:
gohalt 1
nbs 3
T 3-state 3-symbol #b (T.J. & S. Ligocki)
: 374,676,383 119,112,334,170,342,540
C This is the currently best known 3x3 TM
5T 1RB 2LA 1LC 0LA 2RB 1LB 1RH 1RA 1RC
L 26
M 800
pref sim
machv Lig33_b just simple
machv Lig33_b-r with repetitions reduced
machv Lig33_b-1 with tape symbol exponents
machv Lig33_b-m as 2-bck-macro machine
machv Lig33_b-a as 2-bck-macro machine with pure additive config-TRs
iam Lig33_b-a
mtype 2 0
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:13:28 CEST 2010
edate Tue Jul 6 22:13:30 CEST 2010
bnspeed 1
Constructed by: $Id: tmJob.awk,v 1.34 2010/05/06 18:26:17 heiner Exp $
$Id: basics.awk,v 1.1 2010/05/06 17:24:17 heiner Exp $
$Id: htSupp.awk,v 1.14 2010/07/06 19:48:32 heiner Exp $
$Id: mmSim.awk,v 1.34 2005/01/09 22:23:28 heiner Exp $
$Id: bignum.awk,v 1.34 2010/05/06 17:58:14 heiner Exp $
$Id: varLI.awk,v 1.11 2005/01/15 21:01:29 heiner Exp $
bignum signature: LEN={S++:9 U++:9 S+:8 U+:8 S*:4 U*:4} DONT: y i o;
Start: Tue Jul 6 22:13:28 CEST 2010