Comment: This TM produces >4.6x10^1439 ones in >2.5x10^2879 steps. Comment: This was the best known 6x2 TM until May-2010
| State | on 0 |
on 1 |
on 0 | on 1 | ||||
|---|---|---|---|---|---|---|---|---|
| Move | Goto | Move | Goto | |||||
| A | 1RB | 0LE | 1 | right | B | 0 | left | E |
| B | 1LC | 0RA | 1 | left | C | 0 | right | A |
| C | 1LD | 0RC | 1 | left | D | 0 | right | C |
| D | 1LE | 0LF | 1 | left | E | 0 | left | F |
| E | 1LA | 1LC | 1 | left | A | 1 | left | C |
| F | 1LE | 1RH | 1 | left | E | 1 | right | H |
The same TM just simple.
The same TM with repetitions reduced.
The same TM with tape symbol exponents.
The same TM as 2-bck-2-macro machine.
Simulation is done as 2-bck-2-macro machine with pure additive config-TRs.
Pushing initial machine.
Pushing macro factor 2.
Pushing BCK machine.
Pushing macro factor 2.
Steps BasSteps BasTpos Tape contents
0 0 0 (00)A>
1 13 -3 <A(10) 1010
2 16 0 0001 (01)B> 1010
3 20 4 0001 0101 (01)B>
4 31 1 0001 0101 <E(01) 0100
5 35 -3 0001 <E(10) 1101 0100
6 39 -7 <A(11) 1110 1101 0100
7 50 -4 0101 (01)B> 1110 1101 0100
8 55 -7 0101 <A(10) 1010 1101 0100
9 59 -11 <A(10) 10102 1101 0100
10 62 -8 0001 (01)B> 10102 1101 0100
11 70 0 0001 01012 (01)B> 1101 0100
12 75 -3 0001 01012 <A(10) 1001 0100
13 83 -11 0001 <A(10) 10102 1001 0100
14 90 -8 0101 (01)B> 10102 1001 0100
15 98 0 01013 (01)B> 1001 0100
16 104 4 01013 0100 (00)C> 0100
17 107 1 01013 0100 <A(11) 1100
18 115 -3 01013 <A(10) 1010 1100
19 127 -15 <A(10) 10104 1100
20 130 -12 0001 (01)B> 10104 1100
21 146 4 0001 01014 (01)B> 1100
22 151 1 0001 01014 <A(10) 1000
23 167 -15 0001 <A(10) 10104 1000
24 174 -12 0101 (01)B> 10104 1000
25 190 4 01015 (01)B> 1000
26 205 1 01015 <D(11) 0101
27 225 -19 <D(11) 10115 0101
28 233 -23 <A(10) 10116 0101
29 236 -20 0001 (01)B> 10116 0101
30 245 -23 0001 <A(10) 1010 10115 0101
31 252 -20 0101 (01)B> 1010 10115 0101
32 256 -16 01012 (01)B> 10115 0101
33 265 -19 01012 <A(10) 1010 10114 0101
34 273 -27 <A(10) 10103 10114 0101
35 276 -24 0001 (01)B> 10103 10114 0101
36 288 -12 0001 01013 (01)B> 10114 0101
37 297 -15 0001 01013 <A(10) 1010 10113 0101
38 309 -27 0001 <A(10) 10104 10113 0101
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 0001 <A(10) 10101+V(2) 10113+V(1) [*]*
1 7 3 0101 (01)B> 10101+V(2) 10113+V(1) [*]*
2 11+4*V(2) 7+4*V(2) 01012+V(2) (01)B> 10113+V(1) [*]*
3 20+4*V(2) 4+4*V(2) 01012+V(2) <A(10) 1010 10112+V(1) [*]*
4 28+8*V(2) -4 <A(10) 10103+V(2) 10112+V(1) [*]*
5 31+8*V(2) -1 0001 (01)B> 10103+V(2) 10112+V(1) [*]*
6 43+12*V(2) 11+4*V(2) 0001 01013+V(2) (01)B> 10112+V(1) [*]*
7 52+12*V(2) 8+4*V(2) 0001 01013+V(2) <A(10) 1010 10111+V(1) [*]*
8 64+16*V(2) -4 0001 <A(10) 10104+V(2) 10111+V(1) [*]*
<< Success! ==> defined new CTR 1 (PA)
38 309 -27 0001 <A(10) 10104 10113 0101
== Executing PA-CTR 1, V(1)=0, V(2)=3, repcount=1, factor=3/2
46 421 -31 0001 <A(10) 10107 1011 0101
47 428 -28 0101 (01)B> 10107 1011 0101
48 456 0 01018 (01)B> 1011 0101
49 465 -3 01018 <A(10) 1010 0101
50 497 -35 <A(10) 10109 0101
51 500 -32 0001 (01)B> 10109 0101
52 536 4 0001 01019 (01)B> 0101
53 549 1 0001 01019 <A(10) 1011
54 585 -35 0001 <A(10) 10109 1011
55 592 -32 0101 (01)B> 10109 1011
56 628 4 010110 (01)B> 1011
57 637 1 010110 <A(10) 1010
58 677 -39 <A(10) 101011
59 680 -36 0001 (01)B> 101011
60 724 8 0001 010111 (01)B>
61 735 5 0001 010111 <E(01) 0100
62 739 1 0001 010110 <E(10) 1101 0100
63 779 -39 0001 <E(10) 111010 1101 0100
64 783 -43 <A(11) 111011 1101 0100
65 794 -40 0101 (01)B> 111011 1101 0100
66 799 -43 0101 <A(10) 1010 111010 1101 0100
67 803 -47 <A(10) 10102 111010 1101 0100
68 806 -44 0001 (01)B> 10102 111010 1101 0100
69 814 -36 0001 01012 (01)B> 111010 1101 0100
70 819 -39 0001 01012 <A(10) 1010 11109 1101 0100
71 827 -47 0001 <A(10) 10103 11109 1101 0100
72 834 -44 0101 (01)B> 10103 11109 1101 0100
73 846 -32 01014 (01)B> 11109 1101 0100
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 01011+V(1) (01)B> 11103+V(2) [*]* [*]*
1 5 -3 01011+V(1) <A(10) 1010 11102+V(2) [*]* [*]*
2 9+4*V(1) -7+-4*V(1) <A(10) 10102+V(1) 11102+V(2) [*]* [*]*
3 12+4*V(1) -4+-4*V(1) 0001 (01)B> 10102+V(1) 11102+V(2) [*]* [*]*
4 20+8*V(1) 4 0001 01012+V(1) (01)B> 11102+V(2) [*]* [*]*
5 25+8*V(1) 1 0001 01012+V(1) <A(10) 1010 11101+V(2) [*]* [*]*
6 33+12*V(1) -7+-4*V(1) 0001 <A(10) 10103+V(1) 11101+V(2) [*]* [*]*
7 40+12*V(1) -4+-4*V(1) 0101 (01)B> 10103+V(1) 11101+V(2) [*]* [*]*
8 52+16*V(1) 8 01014+V(1) (01)B> 11101+V(2) [*]* [*]*
<< Success! ==> defined new CTR 2 (PA)
73 846 -32 01014 (01)B> 11109 1101 0100
== Executing PA-CTR 2, V(1)=3, V(2)=6, repcount=4, factor=3/2
105 1534 0 010116 (01)B> 1110 1101 0100
106 1539 -3 010116 <A(10) 1010 1101 0100
107 1603 -67 <A(10) 101017 1101 0100
108 1606 -64 0001 (01)B> 101017 1101 0100
109 1674 4 0001 010117 (01)B> 1101 0100
110 1679 1 0001 010117 <A(10) 1001 0100
111 1747 -67 0001 <A(10) 101017 1001 0100
112 1754 -64 0101 (01)B> 101017 1001 0100
113 1822 4 010118 (01)B> 1001 0100
114 1828 8 010118 0100 (00)C> 0100
115 1831 5 010118 0100 <A(11) 1100
116 1839 1 010118 <A(10) 1010 1100
117 1911 -71 <A(10) 101019 1100
118 1914 -68 0001 (01)B> 101019 1100
119 1990 8 0001 010119 (01)B> 1100
120 1995 5 0001 010119 <A(10) 1000
121 2071 -71 0001 <A(10) 101019 1000
122 2078 -68 0101 (01)B> 101019 1000
123 2154 8 010120 (01)B> 1000
124 2169 5 010120 <D(11) 0101
125 2249 -75 <D(11) 101120 0101
126 2257 -79 <A(10) 101121 0101
127 2260 -76 0001 (01)B> 101121 0101
128 2269 -79 0001 <A(10) 1010 101120 0101
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01011+V(1) (01)B> 1110 1101 0100
1 5 -3 01011+V(1) <A(10) 1010 1101 0100
2 9+4*V(1) -7+-4*V(1) <A(10) 10102+V(1) 1101 0100
3 12+4*V(1) -4+-4*V(1) 0001 (01)B> 10102+V(1) 1101 0100
4 20+8*V(1) 4 0001 01012+V(1) (01)B> 1101 0100
5 25+8*V(1) 1 0001 01012+V(1) <A(10) 1001 0100
6 33+12*V(1) -7+-4*V(1) 0001 <A(10) 10102+V(1) 1001 0100
7 40+12*V(1) -4+-4*V(1) 0101 (01)B> 10102+V(1) 1001 0100
8 48+16*V(1) 4 01013+V(1) (01)B> 1001 0100
9 54+16*V(1) 8 01013+V(1) 0100 (00)C> 0100
10 57+16*V(1) 5 01013+V(1) 0100 <A(11) 1100
11 65+16*V(1) 1 01013+V(1) <A(10) 1010 1100
12 77+20*V(1) -11+-4*V(1) <A(10) 10104+V(1) 1100
13 80+20*V(1) -8+-4*V(1) 0001 (01)B> 10104+V(1) 1100
14 96+24*V(1) 8 0001 01014+V(1) (01)B> 1100
15 101+24*V(1) 5 0001 01014+V(1) <A(10) 1000
16 117+28*V(1) -11+-4*V(1) 0001 <A(10) 10104+V(1) 1000
17 124+28*V(1) -8+-4*V(1) 0101 (01)B> 10104+V(1) 1000
18 140+32*V(1) 8 01015+V(1) (01)B> 1000
19 155+32*V(1) 5 01015+V(1) <D(11) 0101
20 175+36*V(1) -15+-4*V(1) <D(11) 10115+V(1) 0101
21 183+36*V(1) -19+-4*V(1) <A(10) 10116+V(1) 0101
22 186+36*V(1) -16+-4*V(1) 0001 (01)B> 10116+V(1) 0101
23 195+36*V(1) -19+-4*V(1) 0001 <A(10) 1010 10115+V(1) 0101
<< Success! ==> defined new CTR 3 (PPA)
128 2269 -79 0001 <A(10) 1010 101120 0101
== Executing PA-CTR 1, V(1)=17, V(2)=0, repcount=9, factor=3/2
200 4573 -115 0001 <A(10) 101028 10112 0101
201 4580 -112 0101 (01)B> 101028 10112 0101
202 4692 0 010129 (01)B> 10112 0101
203 4701 -3 010129 <A(10) 1010 1011 0101
204 4817 -119 <A(10) 101030 1011 0101
205 4820 -116 0001 (01)B> 101030 1011 0101
206 4940 4 0001 010130 (01)B> 1011 0101
207 4949 1 0001 010130 <A(10) 1010 0101
208 5069 -119 0001 <A(10) 101031 0101
209 5076 -116 0101 (01)B> 101031 0101
210 5200 8 010132 (01)B> 0101
211 5213 5 010132 <A(10) 1011
212 5341 -123 <A(10) 101032 1011
213 5344 -120 0001 (01)B> 101032 1011
214 5472 8 0001 010132 (01)B> 1011
215 5481 5 0001 010132 <A(10) 1010
216 5609 -123 0001 <A(10) 101033
217 5616 -120 0101 (01)B> 101033
218 5748 12 010134 (01)B>
219 5759 9 010134 <E(01) 0100
220 5763 5 010133 <E(10) 1101 0100
221 5895 -127 <E(10) 111033 1101 0100
222 5910 -124 1010 (00)C> 111033 1101 0100
223 5928 -120 10102 (10)A> 111032 1101 0100
224 5931 -123 10102 <E(01) 0110 111031 1101 0100
225 5939 -131 <E(01) 01012 0110 111031 1101 0100
226 5944 -128 0010 (10)A> 01012 0110 111031 1101 0100
227 5952 -120 0010 10102 (10)A> 0110 111031 1101 0100
228 5959 -123 0010 10102 <E(01) 0100 111031 1101 0100
229 5967 -131 0010 <E(01) 01012 0100 111031 1101 0100
230 5976 -128 1010 (10)A> 01012 0100 111031 1101 0100
231 5984 -120 10103 (10)A> 0100 111031 1101 0100
232 5990 -116 10104 (00)C> 111031 1101 0100
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 10101+V(1) (00)C> 11103+V(2) [*]* [*]*
1 18 4 10102+V(1) (10)A> 11102+V(2) [*]* [*]*
2 21 1 10102+V(1) <E(01) 0110 11101+V(2) [*]* [*]*
3 29+4*V(1) -7+-4*V(1) <E(01) 01012+V(1) 0110 11101+V(2) [*]* [*]*
4 34+4*V(1) -4+-4*V(1) 0010 (10)A> 01012+V(1) 0110 11101+V(2) [*]* [*]*
5 42+8*V(1) 4 0010 10102+V(1) (10)A> 0110 11101+V(2) [*]* [*]*
6 49+8*V(1) 1 0010 10102+V(1) <E(01) 0100 11101+V(2) [*]* [*]*
7 57+12*V(1) -7+-4*V(1) 0010 <E(01) 01012+V(1) 0100 11101+V(2) [*]* [*]*
8 66+12*V(1) -4+-4*V(1) 1010 (10)A> 01012+V(1) 0100 11101+V(2) [*]* [*]*
9 74+16*V(1) 4 10103+V(1) (10)A> 0100 11101+V(2) [*]* [*]*
10 80+16*V(1) 8 10104+V(1) (00)C> 11101+V(2) [*]* [*]*
<< Success! ==> defined new CTR 4 (PA)
232 5990 -116 10104 (00)C> 111031 1101 0100
== Executing PA-CTR 4, V(1)=3, V(2)=28, repcount=15, factor=3/2
382 12950 4 101049 (00)C> 1110 1101 0100
383 12968 8 101050 (10)A> 1101 0100
384 12971 5 101050 <E(01) 0101 0100
385 13171 -195 <E(01) 010151 0100
386 13176 -192 0010 (10)A> 010151 0100
387 13380 12 0010 101051 (10)A> 0100
388 13386 16 0010 101052 (00)C>
389 13389 13 0010 101052 <A(11) 1000
390 13397 9 0010 101051 <F(01) 1010 1000
391 13601 -195 0010 <F(01) 110151 1010 1000
392 13605 -199 <E(11) 110152 1010 1000
393 13618 -196 1010 (10)A> 110152 1010 1000
394 13621 -199 1010 <E(01) 0101 110151 1010 1000
395 13625 -203 <E(01) 01012 110151 1010 1000
396 13630 -200 0010 (10)A> 01012 110151 1010 1000
397 13638 -192 0010 10102 (10)A> 110151 1010 1000
398 13641 -195 0010 10102 <E(01) 0101 110150 1010 1000
399 13649 -203 0010 <E(01) 01013 110150 1010 1000
400 13658 -200 1010 (10)A> 01013 110150 1010 1000
401 13670 -188 10104 (10)A> 110150 1010 1000
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 10101+V(1) (10)A> 11013+V(2) [*]* [*]*
1 3 -3 10101+V(1) <E(01) 0101 11012+V(2) [*]* [*]*
2 7+4*V(1) -7+-4*V(1) <E(01) 01012+V(1) 11012+V(2) [*]* [*]*
3 12+4*V(1) -4+-4*V(1) 0010 (10)A> 01012+V(1) 11012+V(2) [*]* [*]*
4 20+8*V(1) 4 0010 10102+V(1) (10)A> 11012+V(2) [*]* [*]*
5 23+8*V(1) 1 0010 10102+V(1) <E(01) 0101 11011+V(2) [*]* [*]*
6 31+12*V(1) -7+-4*V(1) 0010 <E(01) 01013+V(1) 11011+V(2) [*]* [*]*
7 40+12*V(1) -4+-4*V(1) 1010 (10)A> 01013+V(1) 11011+V(2) [*]* [*]*
8 52+16*V(1) 8 10104+V(1) (10)A> 11011+V(2) [*]* [*]*
<< Success! ==> defined new CTR 5 (PA)
401 13670 -188 10104 (10)A> 110150 1010 1000
== Executing PA-CTR 5, V(1)=3, V(2)=47, repcount=24, factor=3/2
593 29318 4 101076 (10)A> 11012 1010 1000
594 29321 1 101076 <E(01) 0101 1101 1010 1000
595 29625 -303 <E(01) 010177 1101 1010 1000
596 29630 -300 0010 (10)A> 010177 1101 1010 1000
597 29938 8 0010 101077 (10)A> 1101 1010 1000
598 29941 5 0010 101077 <E(01) 0101 1010 1000
599 30249 -303 0010 <E(01) 010178 1010 1000
600 30258 -300 1010 (10)A> 010178 1010 1000
601 30570 12 101079 (10)A> 1010 1000
602 30573 9 101079 <E(01) 0010 1000
603 30889 -307 <E(01) 010179 0010 1000
604 30894 -304 0010 (10)A> 010179 0010 1000
605 31210 12 0010 101079 (10)A> 0010 1000
606 31225 9 0010 101079 <E(01) 0101 1000
607 31541 -307 0010 <E(01) 010180 1000
608 31550 -304 1010 (10)A> 010180 1000
609 31870 16 101081 (10)A> 1000
610 31873 13 101081 <E(01)
611 32197 -311 <E(01) 010181
612 32202 -308 0010 (10)A> 010181
613 32526 16 0010 101081 (10)A>
614 32539 13 0010 101081 <C(10) 1010
615 32543 9 0010 101080 <C(11) 0110 1010
616 32863 -311 0010 <C(11) 011180 0110 1010
617 32867 -315 <A(11) 011181 0110 1010
618 32878 -312 0101 (01)B> 011181 0110 1010
619 32884 -308 0101 0000 (00)C> 011180 0110 1010
620 32887 -311 0101 0000 <A(11) 1111 011179 0110 1010
621 32898 -308 01012 (01)B> 1111 011179 0110 1010
622 32903 -311 01012 <A(10) 1011 011179 0110 1010
623 32911 -319 <A(10) 10102 1011 011179 0110 1010
624 32914 -316 0001 (01)B> 10102 1011 011179 0110 1010
625 32922 -308 0001 01012 (01)B> 1011 011179 0110 1010
626 32931 -311 0001 01012 <A(10) 1010 011179 0110 1010
627 32939 -319 0001 <A(10) 10103 011179 0110 1010
628 32946 -316 0101 (01)B> 10103 011179 0110 1010
629 32958 -304 01014 (01)B> 011179 0110 1010
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 01011+V(1) (01)B> 01113+V(2) [*]* [*]*
1 6 4 01011+V(1) 0000 (00)C> 01112+V(2) [*]* [*]*
2 9 1 01011+V(1) 0000 <A(11) 1111 01111+V(2) [*]* [*]*
3 20 4 01012+V(1) (01)B> 1111 01111+V(2) [*]* [*]*
4 25 1 01012+V(1) <A(10) 1011 01111+V(2) [*]* [*]*
5 33+4*V(1) -7+-4*V(1) <A(10) 10102+V(1) 1011 01111+V(2) [*]* [*]*
6 36+4*V(1) -4+-4*V(1) 0001 (01)B> 10102+V(1) 1011 01111+V(2) [*]* [*]*
7 44+8*V(1) 4 0001 01012+V(1) (01)B> 1011 01111+V(2) [*]* [*]*
8 53+8*V(1) 1 0001 01012+V(1) <A(10) 1010 01111+V(2) [*]* [*]*
9 61+12*V(1) -7+-4*V(1) 0001 <A(10) 10103+V(1) 01111+V(2) [*]* [*]*
10 68+12*V(1) -4+-4*V(1) 0101 (01)B> 10103+V(1) 01111+V(2) [*]* [*]*
11 80+16*V(1) 8 01014+V(1) (01)B> 01111+V(2) [*]* [*]*
<< Success! ==> defined new CTR 6 (PA)
629 32958 -304 01014 (01)B> 011179 0110 1010
== Executing PA-CTR 6, V(1)=3, V(2)=76, repcount=39, factor=3/2
1058 73518 8 0101121 (01)B> 0111 0110 1010
1059 73524 12 0101121 0000 (00)C> 0110 1010
1060 73527 9 0101121 0000 <A(11) 1110 1010
1061 73538 12 0101122 (01)B> 1110 1010
1062 73543 9 0101122 <A(10) 10102
1063 74031 -479 <A(10) 1010124
1064 74034 -476 0001 (01)B> 1010124
1065 74530 20 0001 0101124 (01)B>
1066 74541 17 0001 0101124 <E(01) 0100
1067 74545 13 0001 0101123 <E(10) 1101 0100
1068 75037 -479 0001 <E(10) 1110123 1101 0100
1069 75041 -483 <A(11) 1110124 1101 0100
1070 75052 -480 0101 (01)B> 1110124 1101 0100
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 01011+V(1) (01)B> 0111 0110 10101+V(2)
1 6 4 01011+V(1) 0000 (00)C> 0110 10101+V(2)
2 9 1 01011+V(1) 0000 <A(11) 1110 10101+V(2)
3 20 4 01012+V(1) (01)B> 1110 10101+V(2)
4 25 1 01012+V(1) <A(10) 10102+V(2)
5 33+4*V(1) -7+-4*V(1) <A(10) 10104+V(1)+V(2)
6 36+4*V(1) -4+-4*V(1) 0001 (01)B> 10104+V(1)+V(2)
7 52+8*V(1)+4*V(2) 12+4*V(2) 0001 01014+V(1)+V(2) (01)B>
8 63+8*V(1)+4*V(2) 9+4*V(2) 0001 01014+V(1)+V(2) <E(01) 0100
9 67+8*V(1)+4*V(2) 5+4*V(2) 0001 01013+V(1)+V(2) <E(10) 1101 0100
10 79+12*V(1)+8*V(2) -7+-4*V(1) 0001 <E(10) 11103+V(1)+V(2) 1101 0100
11 83+12*V(1)+8*V(2) -11+-4*V(1) <A(11) 11104+V(1)+V(2) 1101 0100
12 94+12*V(1)+8*V(2) -8+-4*V(1) 0101 (01)B> 11104+V(1)+V(2) 1101 0100
<< Success! ==> defined new CTR 7 (PPA)
1070 75052 -480 0101 (01)B> 1110124 1101 0100
== Executing PA-CTR 2, V(1)=0, V(2)=121, repcount=61, factor=3/2
1558 166064 8 0101184 (01)B> 11102 1101 0100
1559 166069 5 0101184 <A(10) 1010 1110 1101 0100
1560 166805 -731 <A(10) 1010185 1110 1101 0100
1561 166808 -728 0001 (01)B> 1010185 1110 1101 0100
1562 167548 12 0001 0101185 (01)B> 1110 1101 0100
1563 167553 9 0001 0101185 <A(10) 1010 1101 0100
1564 168293 -731 0001 <A(10) 1010186 1101 0100
1565 168300 -728 0101 (01)B> 1010186 1101 0100
1566 169044 16 0101187 (01)B> 1101 0100
1567 169049 13 0101187 <A(10) 1001 0100
1568 169797 -735 <A(10) 1010187 1001 0100
1569 169800 -732 0001 (01)B> 1010187 1001 0100
1570 170548 16 0001 0101187 (01)B> 1001 0100
1571 170554 20 0001 0101187 0100 (00)C> 0100
1572 170557 17 0001 0101187 0100 <A(11) 1100
1573 170565 13 0001 0101187 <A(10) 1010 1100
1574 171313 -735 0001 <A(10) 1010188 1100
1575 171320 -732 0101 (01)B> 1010188 1100
1576 172072 20 0101189 (01)B> 1100
1577 172077 17 0101189 <A(10) 1000
1578 172833 -739 <A(10) 1010189 1000
1579 172836 -736 0001 (01)B> 1010189 1000
1580 173592 20 0001 0101189 (01)B> 1000
1581 173607 17 0001 0101189 <D(11) 0101
1582 174363 -739 0001 <D(11) 1011189 0101
1583 174371 -743 <E(01) 0011 1011189 0101
1584 174376 -740 0010 (10)A> 0011 1011189 0101
1585 174382 -736 0010 1000 (00)C> 1011189 0101
1586 174391 -739 0010 1000 <E(01) 0111 1011188 0101
1587 174396 -736 0010 1010 (10)A> 0111 1011188 0101
1588 174403 -739 0010 1010 <E(01) 0101 1011188 0101
1589 174407 -743 0010 <E(01) 01012 1011188 0101
1590 174416 -740 1010 (10)A> 01012 1011188 0101
1591 174424 -732 10103 (10)A> 1011188 0101
1592 174427 -735 10103 <E(01) 0011 1011187 0101
1593 174439 -747 <E(01) 01013 0011 1011187 0101
1594 174444 -744 0010 (10)A> 01013 0011 1011187 0101
1595 174456 -732 0010 10103 (10)A> 0011 1011187 0101
1596 174462 -728 0010 10103 1000 (00)C> 1011187 0101
1597 174471 -731 0010 10103 1000 <E(01) 0111 1011186 0101
1598 174476 -728 0010 10104 (10)A> 0111 1011186 0101
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 0010 10101+V(1) (10)A> 0111 10113+V(2) [*]*
1 7 -3 0010 10101+V(1) <E(01) 0101 10113+V(2) [*]*
2 11+4*V(1) -7+-4*V(1) 0010 <E(01) 01012+V(1) 10113+V(2) [*]*
3 20+4*V(1) -4+-4*V(1) 1010 (10)A> 01012+V(1) 10113+V(2) [*]*
4 28+8*V(1) 4 10103+V(1) (10)A> 10113+V(2) [*]*
5 31+8*V(1) 1 10103+V(1) <E(01) 0011 10112+V(2) [*]*
6 43+12*V(1) -11+-4*V(1) <E(01) 01013+V(1) 0011 10112+V(2) [*]*
7 48+12*V(1) -8+-4*V(1) 0010 (10)A> 01013+V(1) 0011 10112+V(2) [*]*
8 60+16*V(1) 4 0010 10103+V(1) (10)A> 0011 10112+V(2) [*]*
9 66+16*V(1) 8 0010 10103+V(1) 1000 (00)C> 10112+V(2) [*]*
10 75+16*V(1) 5 0010 10103+V(1) 1000 <E(01) 0111 10111+V(2) [*]*
11 80+16*V(1) 8 0010 10104+V(1) (10)A> 0111 10111+V(2) [*]*
<< Success! ==> defined new CTR 8 (PA)
1598 174476 -728 0010 10104 (10)A> 0111 1011186 0101
== Executing PA-CTR 8, V(1)=3, V(2)=183, repcount=92, factor=3/2
2610 387180 8 0010 1010280 (10)A> 0111 10112 0101
2611 387187 5 0010 1010280 <E(01) 0101 10112 0101
2612 388307 -1115 0010 <E(01) 0101281 10112 0101
2613 388316 -1112 1010 (10)A> 0101281 10112 0101
2614 389440 12 1010282 (10)A> 10112 0101
2615 389443 9 1010282 <E(01) 0011 1011 0101
2616 390571 -1119 <E(01) 0101282 0011 1011 0101
2617 390576 -1116 0010 (10)A> 0101282 0011 1011 0101
2618 391704 12 0010 1010282 (10)A> 0011 1011 0101
2619 391710 16 0010 1010282 1000 (00)C> 1011 0101
2620 391719 13 0010 1010282 1000 <E(01) 0111 0101
2621 391724 16 0010 1010283 (10)A> 0111 0101
2622 391731 13 0010 1010283 <E(01) 01012
2623 392863 -1119 0010 <E(01) 0101285
2624 392872 -1116 1010 (10)A> 0101285
2625 394012 24 1010286 (10)A>
2626 394025 21 1010286 <C(10) 1010
2627 394029 17 1010285 <C(11) 0110 1010
2628 395169 -1123 <C(11) 0111285 0110 1010
2629 395177 -1127 <E(01) 0111286 0110 1010
2630 395182 -1124 0010 (10)A> 0111286 0110 1010
2631 395189 -1127 0010 <E(01) 0101 0111285 0110 1010
2632 395198 -1124 1010 (10)A> 0101 0111285 0110 1010
2633 395202 -1120 10102 (10)A> 0111285 0110 1010
2634 395209 -1123 10102 <E(01) 0101 0111284 0110 1010
2635 395217 -1131 <E(01) 01013 0111284 0110 1010
2636 395222 -1128 0010 (10)A> 01013 0111284 0110 1010
2637 395234 -1116 0010 10103 (10)A> 0111284 0110 1010
2638 395241 -1119 0010 10103 <E(01) 0101 0111283 0110 1010
2639 395253 -1131 0010 <E(01) 01014 0111283 0110 1010
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 0010 <E(01) 01011+V(2) 01113+V(1) [*]* [*]*
1 9 3 1010 (10)A> 01011+V(2) 01113+V(1) [*]* [*]*
2 13+4*V(2) 7+4*V(2) 10102+V(2) (10)A> 01113+V(1) [*]* [*]*
3 20+4*V(2) 4+4*V(2) 10102+V(2) <E(01) 0101 01112+V(1) [*]* [*]*
4 28+8*V(2) -4 <E(01) 01013+V(2) 01112+V(1) [*]* [*]*
5 33+8*V(2) -1 0010 (10)A> 01013+V(2) 01112+V(1) [*]* [*]*
6 45+12*V(2) 11+4*V(2) 0010 10103+V(2) (10)A> 01112+V(1) [*]* [*]*
7 52+12*V(2) 8+4*V(2) 0010 10103+V(2) <E(01) 0101 01111+V(1) [*]* [*]*
8 64+16*V(2) -4 0010 <E(01) 01014+V(2) 01111+V(1) [*]* [*]*
<< Success! ==> defined new CTR 9 (PA)
2639 395253 -1131 0010 <E(01) 01014 0111283 0110 1010
== Executing PA-CTR 9, V(1)=280, V(2)=3, repcount=141, factor=3/2
3767 884805 -1695 0010 <E(01) 0101427 0111 0110 1010
3768 884814 -1692 1010 (10)A> 0101427 0111 0110 1010
3769 886522 16 1010428 (10)A> 0111 0110 1010
3770 886529 13 1010428 <E(01) 0101 0110 1010
3771 888241 -1699 <E(01) 0101429 0110 1010
3772 888246 -1696 0010 (10)A> 0101429 0110 1010
3773 889962 20 0010 1010429 (10)A> 0110 1010
3774 889969 17 0010 1010429 <E(01) 0100 1010
3775 891685 -1699 0010 <E(01) 0101429 0100 1010
3776 891694 -1696 1010 (10)A> 0101429 0100 1010
3777 893410 20 1010430 (10)A> 0100 1010
3778 893416 24 1010431 (00)C> 1010
3779 893425 21 1010431 <E(01) 0110
3780 895149 -1703 <E(01) 0101431 0110
3781 895154 -1700 0010 (10)A> 0101431 0110
3782 896878 24 0010 1010431 (10)A> 0110
3783 896885 21 0010 1010431 <E(01) 0100
3784 898609 -1703 0010 <E(01) 0101431 0100
3785 898618 -1700 1010 (10)A> 0101431 0100
3786 900342 24 1010432 (10)A> 0100
3787 900348 28 1010433 (00)C>
3788 900351 25 1010433 <A(11) 1000
3789 900359 21 1010432 <F(01) 1010 1000
3790 902087 -1707 <F(01) 1101432 1010 1000
3791 902095 -1711 <A(10) 1001 1101432 1010 1000
3792 902098 -1708 0001 (01)B> 1001 1101432 1010 1000
3793 902104 -1704 0001 0100 (00)C> 1101432 1010 1000
3794 902115 -1707 0001 0100 <A(10) 1011 1101431 1010 1000
3795 902118 -1704 0001 0101 (01)B> 1011 1101431 1010 1000
3796 902127 -1707 0001 0101 <A(10) 1010 1101431 1010 1000
3797 902131 -1711 0001 <A(10) 10102 1101431 1010 1000
3798 902138 -1708 0101 (01)B> 10102 1101431 1010 1000
3799 902146 -1700 01013 (01)B> 1101431 1010 1000
3800 902151 -1703 01013 <A(10) 1001 1101430 1010 1000
3801 902163 -1715 <A(10) 10103 1001 1101430 1010 1000
3802 902166 -1712 0001 (01)B> 10103 1001 1101430 1010 1000
3803 902178 -1700 0001 01013 (01)B> 1001 1101430 1010 1000
3804 902184 -1696 0001 01013 0100 (00)C> 1101430 1010 1000
3805 902195 -1699 0001 01013 0100 <A(10) 1011 1101429 1010 1000
3806 902198 -1696 0001 01014 (01)B> 1011 1101429 1010 1000
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 0001 01011+V(1) (01)B> 1011 11013+V(2) [*]* [*]*
1 9 -3 0001 01011+V(1) <A(10) 1010 11013+V(2) [*]* [*]*
2 13+4*V(1) -7+-4*V(1) 0001 <A(10) 10102+V(1) 11013+V(2) [*]* [*]*
3 20+4*V(1) -4+-4*V(1) 0101 (01)B> 10102+V(1) 11013+V(2) [*]* [*]*
4 28+8*V(1) 4 01013+V(1) (01)B> 11013+V(2) [*]* [*]*
5 33+8*V(1) 1 01013+V(1) <A(10) 1001 11012+V(2) [*]* [*]*
6 45+12*V(1) -11+-4*V(1) <A(10) 10103+V(1) 1001 11012+V(2) [*]* [*]*
7 48+12*V(1) -8+-4*V(1) 0001 (01)B> 10103+V(1) 1001 11012+V(2) [*]* [*]*
8 60+16*V(1) 4 0001 01013+V(1) (01)B> 1001 11012+V(2) [*]* [*]*
9 66+16*V(1) 8 0001 01013+V(1) 0100 (00)C> 11012+V(2) [*]* [*]*
10 77+16*V(1) 5 0001 01013+V(1) 0100 <A(10) 1011 11011+V(2) [*]* [*]*
11 80+16*V(1) 8 0001 01014+V(1) (01)B> 1011 11011+V(2) [*]* [*]*
<< Success! ==> defined new CTR 10 (PA)
3806 902198 -1696 0001 01014 (01)B> 1011 1101429 1010 1000
== Executing PA-CTR 10, V(1)=3, V(2)=426, repcount=214, factor=3/2
6160 2023558 16 0001 0101646 (01)B> 1011 1101 1010 1000
6161 2023567 13 0001 0101646 <A(10) 1010 1101 1010 1000
6162 2026151 -2571 0001 <A(10) 1010647 1101 1010 1000
6163 2026158 -2568 0101 (01)B> 1010647 1101 1010 1000
6164 2028746 20 0101648 (01)B> 1101 1010 1000
6165 2028751 17 0101648 <A(10) 1001 1010 1000
6166 2031343 -2575 <A(10) 1010648 1001 1010 1000
6167 2031346 -2572 0001 (01)B> 1010648 1001 1010 1000
6168 2033938 20 0001 0101648 (01)B> 1001 1010 1000
6169 2033944 24 0001 0101648 0100 (00)C> 1010 1000
6170 2033953 21 0001 0101648 0100 <E(01) 0110 1000
6171 2033958 24 0001 0101648 0110 (10)A> 0110 1000
6172 2033965 21 0001 0101648 0110 <E(01) 0100 1000
6173 2033969 17 0001 0101648 <D(11) 0101 0100 1000
6174 2036561 -2575 0001 <D(11) 1011648 0101 0100 1000
6175 2036569 -2579 <E(01) 0011 1011648 0101 0100 1000
6176 2036574 -2576 0010 (10)A> 0011 1011648 0101 0100 1000
6177 2036580 -2572 0010 1000 (00)C> 1011648 0101 0100 1000
6178 2036589 -2575 0010 1000 <E(01) 0111 1011647 0101 0100 1000
6179 2036594 -2572 0010 1010 (10)A> 0111 1011647 0101 0100 1000
6180 2036601 -2575 0010 1010 <E(01) 0101 1011647 0101 0100 1000
6181 2036605 -2579 0010 <E(01) 01012 1011647 0101 0100 1000
6182 2036614 -2576 1010 (10)A> 01012 1011647 0101 0100 1000
6183 2036622 -2568 10103 (10)A> 1011647 0101 0100 1000
6184 2036625 -2571 10103 <E(01) 0011 1011646 0101 0100 1000
6185 2036637 -2583 <E(01) 01013 0011 1011646 0101 0100 1000
6186 2036642 -2580 0010 (10)A> 01013 0011 1011646 0101 0100 1000
6187 2036654 -2568 0010 10103 (10)A> 0011 1011646 0101 0100 1000
6188 2036660 -2564 0010 10103 1000 (00)C> 1011646 0101 0100 1000
6189 2036669 -2567 0010 10103 1000 <E(01) 0111 1011645 0101 0100 1000
6190 2036674 -2564 0010 10104 (10)A> 0111 1011645 0101 0100 1000
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 0010 10101+V(1) (10)A> 0111 10113+V(2) [*]* [*]* [*]*
1 7 -3 0010 10101+V(1) <E(01) 0101 10113+V(2) [*]* [*]* [*]*
2 11+4*V(1) -7+-4*V(1) 0010 <E(01) 01012+V(1) 10113+V(2) [*]* [*]* [*]*
3 20+4*V(1) -4+-4*V(1) 1010 (10)A> 01012+V(1) 10113+V(2) [*]* [*]* [*]*
4 28+8*V(1) 4 10103+V(1) (10)A> 10113+V(2) [*]* [*]* [*]*
5 31+8*V(1) 1 10103+V(1) <E(01) 0011 10112+V(2) [*]* [*]* [*]*
6 43+12*V(1) -11+-4*V(1) <E(01) 01013+V(1) 0011 10112+V(2) [*]* [*]* [*]*
7 48+12*V(1) -8+-4*V(1) 0010 (10)A> 01013+V(1) 0011 10112+V(2) [*]* [*]* [*]*
8 60+16*V(1) 4 0010 10103+V(1) (10)A> 0011 10112+V(2) [*]* [*]* [*]*
9 66+16*V(1) 8 0010 10103+V(1) 1000 (00)C> 10112+V(2) [*]* [*]* [*]*
10 75+16*V(1) 5 0010 10103+V(1) 1000 <E(01) 0111 10111+V(2) [*]* [*]* [*]*
11 80+16*V(1) 8 0010 10104+V(1) (10)A> 0111 10111+V(2) [*]* [*]* [*]*
<< Success! ==> defined new CTR 11 (PA)
6190 2036674 -2564 0010 10104 (10)A> 0111 1011645 0101 0100 1000
== Executing PA-CTR 11, V(1)=3, V(2)=642, repcount=322, factor=3/2
9732 4558578 12 0010 1010970 (10)A> 0111 1011 0101 0100 1000
9733 4558585 9 0010 1010970 <E(01) 0101 1011 0101 0100 1000
9734 4562465 -3871 0010 <E(01) 0101971 1011 0101 0100 1000
9735 4562474 -3868 1010 (10)A> 0101971 1011 0101 0100 1000
9736 4566358 16 1010972 (10)A> 1011 0101 0100 1000
9737 4566361 13 1010972 <E(01) 0011 0101 0100 1000
9738 4570249 -3875 <E(01) 0101972 0011 0101 0100 1000
9739 4570254 -3872 0010 (10)A> 0101972 0011 0101 0100 1000
9740 4574142 16 0010 1010972 (10)A> 0011 0101 0100 1000
9741 4574148 20 0010 1010972 1000 (00)C> 0101 0100 1000
9742 4574151 17 0010 1010972 1000 <A(11) 1101 0100 1000
9743 4574162 20 0010 1010972 1101 (01)B> 1101 0100 1000
9744 4574167 17 0010 1010972 1101 <A(10) 1001 0100 1000
9745 4574171 13 0010 1010972 <C(10) 1010 1001 0100 1000
9746 4574175 9 0010 1010971 <C(11) 0110 1010 1001 0100 1000
9747 4578059 -3875 0010 <C(11) 0111971 0110 1010 1001 0100 1000
9748 4578063 -3879 <A(11) 0111972 0110 1010 1001 0100 1000
9749 4578074 -3876 0101 (01)B> 0111972 0110 1010 1001 0100 1000
9750 4578080 -3872 0101 0000 (00)C> 0111971 0110 1010 1001 0100 1000
9751 4578083 -3875 0101 0000 <A(11) 1111 0111970 0110 1010 1001 0100 1000
9752 4578094 -3872 01012 (01)B> 1111 0111970 0110 1010 1001 0100 1000
9753 4578099 -3875 01012 <A(10) 1011 0111970 0110 1010 1001 0100 1000
9754 4578107 -3883 <A(10) 10102 1011 0111970 0110 1010 1001 0100 1000
9755 4578110 -3880 0001 (01)B> 10102 1011 0111970 0110 1010 1001 0100 1000
9756 4578118 -3872 0001 01012 (01)B> 1011 0111970 0110 1010 1001 0100 1000
9757 4578127 -3875 0001 01012 <A(10) 1010 0111970 0110 1010 1001 0100 1000
9758 4578135 -3883 0001 <A(10) 10103 0111970 0110 1010 1001 0100 1000
9759 4578142 -3880 0101 (01)B> 10103 0111970 0110 1010 1001 0100 1000
9760 4578154 -3868 01014 (01)B> 0111970 0110 1010 1001 0100 1000
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 01011+V(1) (01)B> 01113+V(2) [*]* [*]* [*]* [*]* [*]*
1 6 4 01011+V(1) 0000 (00)C> 01112+V(2) [*]* [*]* [*]* [*]* [*]*
2 9 1 01011+V(1) 0000 <A(11) 1111 01111+V(2) [*]* [*]* [*]* [*]* [*]*
3 20 4 01012+V(1) (01)B> 1111 01111+V(2) [*]* [*]* [*]* [*]* [*]*
4 25 1 01012+V(1) <A(10) 1011 01111+V(2) [*]* [*]* [*]* [*]* [*]*
5 33+4*V(1) -7+-4*V(1) <A(10) 10102+V(1) 1011 01111+V(2) [*]* [*]* [*]* [*]* [*]*
6 36+4*V(1) -4+-4*V(1) 0001 (01)B> 10102+V(1) 1011 01111+V(2) [*]* [*]* [*]* [*]* [*]*
7 44+8*V(1) 4 0001 01012+V(1) (01)B> 1011 01111+V(2) [*]* [*]* [*]* [*]* [*]*
8 53+8*V(1) 1 0001 01012+V(1) <A(10) 1010 01111+V(2) [*]* [*]* [*]* [*]* [*]*
9 61+12*V(1) -7+-4*V(1) 0001 <A(10) 10103+V(1) 01111+V(2) [*]* [*]* [*]* [*]* [*]*
10 68+12*V(1) -4+-4*V(1) 0101 (01)B> 10103+V(1) 01111+V(2) [*]* [*]* [*]* [*]* [*]*
11 80+16*V(1) 8 01014+V(1) (01)B> 01111+V(2) [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 12 (PA)
9760 4578154 -3868 01014 (01)B> 0111970 0110 1010 1001 0100 1000
== Executing PA-CTR 12, V(1)=3, V(2)=967, repcount=484, factor=3/2
15084 10250634 4 01011456 (01)B> 01112 0110 1010 1001 0100 1000
15085 10250640 8 01011456 0000 (00)C> 0111 0110 1010 1001 0100 1000
15086 10250643 5 01011456 0000 <A(11) 1111 0110 1010 1001 0100 1000
15087 10250654 8 01011457 (01)B> 1111 0110 1010 1001 0100 1000
15088 10250659 5 01011457 <A(10) 1011 0110 1010 1001 0100 1000
15089 10256487 -5823 <A(10) 10101457 1011 0110 1010 1001 0100 1000
15090 10256490 -5820 0001 (01)B> 10101457 1011 0110 1010 1001 0100 1000
15091 10262318 8 0001 01011457 (01)B> 1011 0110 1010 1001 0100 1000
15092 10262327 5 0001 01011457 <A(10) 1010 0110 1010 1001 0100 1000
15093 10268155 -5823 0001 <A(10) 10101458 0110 1010 1001 0100 1000
15094 10268162 -5820 0101 (01)B> 10101458 0110 1010 1001 0100 1000
15095 10273994 12 01011459 (01)B> 0110 1010 1001 0100 1000
15096 10274014 16 01011459 1010 (10)A> 1010 1001 0100 1000
15097 10274017 13 01011459 1010 <E(01) 0010 1001 0100 1000
15098 10274021 9 01011459 <E(01) 0101 0010 1001 0100 1000
15099 10274025 5 01011458 <E(10) 1101 0101 0010 1001 0100 1000
15100 10279857 -5827 <E(10) 11101458 1101 0101 0010 1001 0100 1000
15101 10279872 -5824 1010 (00)C> 11101458 1101 0101 0010 1001 0100 1000
15102 10279890 -5820 10102 (10)A> 11101457 1101 0101 0010 1001 0100 1000
15103 10279893 -5823 10102 <E(01) 0110 11101456 1101 0101 0010 1001 0100 1000
15104 10279901 -5831 <E(01) 01012 0110 11101456 1101 0101 0010 1001 0100 1000
15105 10279906 -5828 0010 (10)A> 01012 0110 11101456 1101 0101 0010 1001 0100 1000
15106 10279914 -5820 0010 10102 (10)A> 0110 11101456 1101 0101 0010 1001 0100 1000
15107 10279921 -5823 0010 10102 <E(01) 0100 11101456 1101 0101 0010 1001 0100 1000
15108 10279929 -5831 0010 <E(01) 01012 0100 11101456 1101 0101 0010 1001 0100 1000
15109 10279938 -5828 1010 (10)A> 01012 0100 11101456 1101 0101 0010 1001 0100 1000
15110 10279946 -5820 10103 (10)A> 0100 11101456 1101 0101 0010 1001 0100 1000
15111 10279952 -5816 10104 (00)C> 11101456 1101 0101 0010 1001 0100 1000
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 10101+V(1) (00)C> 11103+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
1 18 4 10102+V(1) (10)A> 11102+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
2 21 1 10102+V(1) <E(01) 0110 11101+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
3 29+4*V(1) -7+-4*V(1) <E(01) 01012+V(1) 0110 11101+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
4 34+4*V(1) -4+-4*V(1) 0010 (10)A> 01012+V(1) 0110 11101+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
5 42+8*V(1) 4 0010 10102+V(1) (10)A> 0110 11101+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
6 49+8*V(1) 1 0010 10102+V(1) <E(01) 0100 11101+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
7 57+12*V(1) -7+-4*V(1) 0010 <E(01) 01012+V(1) 0100 11101+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
8 66+12*V(1) -4+-4*V(1) 1010 (10)A> 01012+V(1) 0100 11101+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
9 74+16*V(1) 4 10103+V(1) (10)A> 0100 11101+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
10 80+16*V(1) 8 10104+V(1) (00)C> 11101+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 13 (PA)
15111 10279952 -5816 10104 (00)C> 11101456 1101 0101 0010 1001 0100 1000
== Executing PA-CTR 13, V(1)=3, V(2)=1453, repcount=727, factor=3/2
22381 23040256 0 10102185 (00)C> 11102 1101 0101 0010 1001 0100 1000
22382 23040274 4 10102186 (10)A> 1110 1101 0101 0010 1001 0100 1000
22383 23040277 1 10102186 <E(01) 0110 1101 0101 0010 1001 0100 1000
22384 23049021 -8743 <E(01) 01012186 0110 1101 0101 0010 1001 0100 1000
22385 23049026 -8740 0010 (10)A> 01012186 0110 1101 0101 0010 1001 0100 1000
22386 23057770 4 0010 10102186 (10)A> 0110 1101 0101 0010 1001 0100 1000
22387 23057777 1 0010 10102186 <E(01) 0100 1101 0101 0010 1001 0100 1000
22388 23066521 -8743 0010 <E(01) 01012186 0100 1101 0101 0010 1001 0100 1000
22389 23066530 -8740 1010 (10)A> 01012186 0100 1101 0101 0010 1001 0100 1000
22390 23075274 4 10102187 (10)A> 0100 1101 0101 0010 1001 0100 1000
22391 23075280 8 10102188 (00)C> 1101 0101 0010 1001 0100 1000
22392 23075291 5 10102188 <A(10) 1011 0101 0010 1001 0100 1000
22393 23075294 8 10102187 1011 (01)B> 1011 0101 0010 1001 0100 1000
22394 23075303 5 10102187 1011 <A(10) 1010 0101 0010 1001 0100 1000
22395 23075307 1 10102187 <F(01) 10102 0101 0010 1001 0100 1000
22396 23084055 -8747 <F(01) 11012187 10102 0101 0010 1001 0100 1000
22397 23084063 -8751 <A(10) 1001 11012187 10102 0101 0010 1001 0100 1000
22398 23084066 -8748 0001 (01)B> 1001 11012187 10102 0101 0010 1001 0100 1000
22399 23084072 -8744 0001 0100 (00)C> 11012187 10102 0101 0010 1001 0100 1000
22400 23084083 -8747 0001 0100 <A(10) 1011 11012186 10102 0101 0010 1001 0100 1000
22401 23084086 -8744 0001 0101 (01)B> 1011 11012186 10102 0101 0010 1001 0100 1000
22402 23084095 -8747 0001 0101 <A(10) 1010 11012186 10102 0101 0010 1001 0100 1000
22403 23084099 -8751 0001 <A(10) 10102 11012186 10102 0101 0010 1001 0100 1000
22404 23084106 -8748 0101 (01)B> 10102 11012186 10102 0101 0010 1001 0100 1000
22405 23084114 -8740 01013 (01)B> 11012186 10102 0101 0010 1001 0100 1000
22406 23084119 -8743 01013 <A(10) 1001 11012185 10102 0101 0010 1001 0100 1000
22407 23084131 -8755 <A(10) 10103 1001 11012185 10102 0101 0010 1001 0100 1000
22408 23084134 -8752 0001 (01)B> 10103 1001 11012185 10102 0101 0010 1001 0100 1000
22409 23084146 -8740 0001 01013 (01)B> 1001 11012185 10102 0101 0010 1001 0100 1000
22410 23084152 -8736 0001 01013 0100 (00)C> 11012185 10102 0101 0010 1001 0100 1000
22411 23084163 -8739 0001 01013 0100 <A(10) 1011 11012184 10102 0101 0010 1001 0100 1000
22412 23084166 -8736 0001 01014 (01)B> 1011 11012184 10102 0101 0010 1001 0100 1000
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 0001 01011+V(1) (01)B> 1011 11013+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
1 9 -3 0001 01011+V(1) <A(10) 1010 11013+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
2 13+4*V(1) -7+-4*V(1) 0001 <A(10) 10102+V(1) 11013+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
3 20+4*V(1) -4+-4*V(1) 0101 (01)B> 10102+V(1) 11013+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
4 28+8*V(1) 4 01013+V(1) (01)B> 11013+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
5 33+8*V(1) 1 01013+V(1) <A(10) 1001 11012+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
6 45+12*V(1) -11+-4*V(1) <A(10) 10103+V(1) 1001 11012+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
7 48+12*V(1) -8+-4*V(1) 0001 (01)B> 10103+V(1) 1001 11012+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
8 60+16*V(1) 4 0001 01013+V(1) (01)B> 1001 11012+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
9 66+16*V(1) 8 0001 01013+V(1) 0100 (00)C> 11012+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
10 77+16*V(1) 5 0001 01013+V(1) 0100 <A(10) 1011 11011+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
11 80+16*V(1) 8 0001 01014+V(1) (01)B> 1011 11011+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 14 (PA)
22412 23084166 -8736 0001 01014 (01)B> 1011 11012184 10102 0101 0010 1001 0100 1000
== Executing PA-CTR 14, V(1)=3, V(2)=2181, repcount=1091, factor=3/2
34413 51764374 -8 0001 01013277 (01)B> 1011 11012 10102 0101 0010 1001 0100 1000
34414 51764383 -11 0001 01013277 <A(10) 1010 11012 10102 0101 0010 1001 0100 1000
34415 51777491 -13119 0001 <A(10) 10103278 11012 10102 0101 0010 1001 0100 1000
34416 51777498 -13116 0101 (01)B> 10103278 11012 10102 0101 0010 1001 0100 1000
34417 51790610 -4 01013279 (01)B> 11012 10102 0101 0010 1001 0100 1000
34418 51790615 -7 01013279 <A(10) 1001 1101 10102 0101 0010 1001 0100 1000
34419 51803731 -13123 <A(10) 10103279 1001 1101 10102 0101 0010 1001 0100 1000
34420 51803734 -13120 0001 (01)B> 10103279 1001 1101 10102 0101 0010 1001 0100 1000
34421 51816850 -4 0001 01013279 (01)B> 1001 1101 10102 0101 0010 1001 0100 1000
34422 51816856 0 0001 01013279 0100 (00)C> 1101 10102 0101 0010 1001 0100 1000
34423 51816867 -3 0001 01013279 0100 <A(10) 1011 10102 0101 0010 1001 0100 1000
34424 51816870 0 0001 01013280 (01)B> 1011 10102 0101 0010 1001 0100 1000
34425 51816879 -3 0001 01013280 <A(10) 10103 0101 0010 1001 0100 1000
34426 51829999 -13123 0001 <A(10) 10103283 0101 0010 1001 0100 1000
34427 51830006 -13120 0101 (01)B> 10103283 0101 0010 1001 0100 1000
34428 51843138 12 01013284 (01)B> 0101 0010 1001 0100 1000
34429 51843151 9 01013284 <A(10) 1011 0010 1001 0100 1000
34430 51856287 -13127 <A(10) 10103284 1011 0010 1001 0100 1000
34431 51856290 -13124 0001 (01)B> 10103284 1011 0010 1001 0100 1000
34432 51869426 12 0001 01013284 (01)B> 1011 0010 1001 0100 1000
34433 51869435 9 0001 01013284 <A(10) 1010 0010 1001 0100 1000
34434 51882571 -13127 0001 <A(10) 10103285 0010 1001 0100 1000
34435 51882578 -13124 0101 (01)B> 10103285 0010 1001 0100 1000
34436 51895718 16 01013286 (01)B> 0010 1001 0100 1000
34437 51895729 13 01013286 <E(01) 0110 1001 0100 1000
34438 51895733 9 01013285 <E(10) 1101 0110 1001 0100 1000
34439 51908873 -13131 <E(10) 11103285 1101 0110 1001 0100 1000
34440 51908888 -13128 1010 (00)C> 11103285 1101 0110 1001 0100 1000
34441 51908906 -13124 10102 (10)A> 11103284 1101 0110 1001 0100 1000
34442 51908909 -13127 10102 <E(01) 0110 11103283 1101 0110 1001 0100 1000
34443 51908917 -13135 <E(01) 01012 0110 11103283 1101 0110 1001 0100 1000
34444 51908922 -13132 0010 (10)A> 01012 0110 11103283 1101 0110 1001 0100 1000
34445 51908930 -13124 0010 10102 (10)A> 0110 11103283 1101 0110 1001 0100 1000
34446 51908937 -13127 0010 10102 <E(01) 0100 11103283 1101 0110 1001 0100 1000
34447 51908945 -13135 0010 <E(01) 01012 0100 11103283 1101 0110 1001 0100 1000
34448 51908954 -13132 1010 (10)A> 01012 0100 11103283 1101 0110 1001 0100 1000
34449 51908962 -13124 10103 (10)A> 0100 11103283 1101 0110 1001 0100 1000
34450 51908968 -13120 10104 (00)C> 11103283 1101 0110 1001 0100 1000
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 10101+V(1) (00)C> 11103+V(2) [*]* [*]* [*]* [*]* [*]*
1 18 4 10102+V(1) (10)A> 11102+V(2) [*]* [*]* [*]* [*]* [*]*
2 21 1 10102+V(1) <E(01) 0110 11101+V(2) [*]* [*]* [*]* [*]* [*]*
3 29+4*V(1) -7+-4*V(1) <E(01) 01012+V(1) 0110 11101+V(2) [*]* [*]* [*]* [*]* [*]*
4 34+4*V(1) -4+-4*V(1) 0010 (10)A> 01012+V(1) 0110 11101+V(2) [*]* [*]* [*]* [*]* [*]*
5 42+8*V(1) 4 0010 10102+V(1) (10)A> 0110 11101+V(2) [*]* [*]* [*]* [*]* [*]*
6 49+8*V(1) 1 0010 10102+V(1) <E(01) 0100 11101+V(2) [*]* [*]* [*]* [*]* [*]*
7 57+12*V(1) -7+-4*V(1) 0010 <E(01) 01012+V(1) 0100 11101+V(2) [*]* [*]* [*]* [*]* [*]*
8 66+12*V(1) -4+-4*V(1) 1010 (10)A> 01012+V(1) 0100 11101+V(2) [*]* [*]* [*]* [*]* [*]*
9 74+16*V(1) 4 10103+V(1) (10)A> 0100 11101+V(2) [*]* [*]* [*]* [*]* [*]*
10 80+16*V(1) 8 10104+V(1) (00)C> 11101+V(2) [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 15 (PA)
34450 51908968 -13120 10104 (00)C> 11103283 1101 0110 1001 0100 1000
== Executing PA-CTR 15, V(1)=3, V(2)=3280, repcount=1641, factor=3/2
50860 116708776 8 10104927 (00)C> 1110 1101 0110 1001 0100 1000
50861 116708794 12 10104928 (10)A> 1101 0110 1001 0100 1000
50862 116708797 9 10104928 <E(01) 0101 0110 1001 0100 1000
50863 116728509 -19703 <E(01) 01014929 0110 1001 0100 1000
50864 116728514 -19700 0010 (10)A> 01014929 0110 1001 0100 1000
50865 116748230 16 0010 10104929 (10)A> 0110 1001 0100 1000
50866 116748237 13 0010 10104929 <E(01) 0100 1001 0100 1000
50867 116767953 -19703 0010 <E(01) 01014929 0100 1001 0100 1000
50868 116767962 -19700 1010 (10)A> 01014929 0100 1001 0100 1000
50869 116787678 16 10104930 (10)A> 0100 1001 0100 1000
50870 116787684 20 10104931 (00)C> 1001 0100 1000
50871 116787693 17 10104931 <E(01) 0101 0100 1000
50872 116807417 -19707 <E(01) 01014932 0100 1000
50873 116807422 -19704 0010 (10)A> 01014932 0100 1000
50874 116827150 24 0010 10104932 (10)A> 0100 1000
50875 116827156 28 0010 10104933 (00)C> 1000
50876 116827165 25 0010 10104933 <E(01) 0100
50877 116846897 -19707 0010 <E(01) 01014933 0100
50878 116846906 -19704 1010 (10)A> 01014933 0100
50879 116866638 28 10104934 (10)A> 0100
50880 116866644 32 10104935 (00)C>
50881 116866647 29 10104935 <A(11) 1000
50882 116866655 25 10104934 <F(01) 1010 1000
50883 116886391 -19711 <F(01) 11014934 1010 1000
50884 116886399 -19715 <A(10) 1001 11014934 1010 1000
50885 116886402 -19712 0001 (01)B> 1001 11014934 1010 1000
50886 116886408 -19708 0001 0100 (00)C> 11014934 1010 1000
50887 116886419 -19711 0001 0100 <A(10) 1011 11014933 1010 1000
50888 116886422 -19708 0001 0101 (01)B> 1011 11014933 1010 1000
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 10101+V(1) (00)C> 1110 1101 0110 1001 0100 1000
1 18 4 10102+V(1) (10)A> 1101 0110 1001 0100 1000
2 21 1 10102+V(1) <E(01) 0101 0110 1001 0100 1000
3 29+4*V(1) -7+-4*V(1) <E(01) 01013+V(1) 0110 1001 0100 1000
4 34+4*V(1) -4+-4*V(1) 0010 (10)A> 01013+V(1) 0110 1001 0100 1000
5 46+8*V(1) 8 0010 10103+V(1) (10)A> 0110 1001 0100 1000
6 53+8*V(1) 5 0010 10103+V(1) <E(01) 0100 1001 0100 1000
7 65+12*V(1) -7+-4*V(1) 0010 <E(01) 01013+V(1) 0100 1001 0100 1000
8 74+12*V(1) -4+-4*V(1) 1010 (10)A> 01013+V(1) 0100 1001 0100 1000
9 86+16*V(1) 8 10104+V(1) (10)A> 0100 1001 0100 1000
10 92+16*V(1) 12 10105+V(1) (00)C> 1001 0100 1000
11 101+16*V(1) 9 10105+V(1) <E(01) 0101 0100 1000
12 121+20*V(1) -11+-4*V(1) <E(01) 01016+V(1) 0100 1000
13 126+20*V(1) -8+-4*V(1) 0010 (10)A> 01016+V(1) 0100 1000
14 150+24*V(1) 16 0010 10106+V(1) (10)A> 0100 1000
15 156+24*V(1) 20 0010 10107+V(1) (00)C> 1000
16 165+24*V(1) 17 0010 10107+V(1) <E(01) 0100
17 193+28*V(1) -11+-4*V(1) 0010 <E(01) 01017+V(1) 0100
18 202+28*V(1) -8+-4*V(1) 1010 (10)A> 01017+V(1) 0100
19 230+32*V(1) 20 10108+V(1) (10)A> 0100
20 236+32*V(1) 24 10109+V(1) (00)C>
21 239+32*V(1) 21 10109+V(1) <A(11) 1000
22 247+32*V(1) 17 10108+V(1) <F(01) 1010 1000
23 279+36*V(1) -15+-4*V(1) <F(01) 11018+V(1) 1010 1000
24 287+36*V(1) -19+-4*V(1) <A(10) 1001 11018+V(1) 1010 1000
25 290+36*V(1) -16+-4*V(1) 0001 (01)B> 1001 11018+V(1) 1010 1000
26 296+36*V(1) -12+-4*V(1) 0001 0100 (00)C> 11018+V(1) 1010 1000
27 307+36*V(1) -15+-4*V(1) 0001 0100 <A(10) 1011 11017+V(1) 1010 1000
28 310+36*V(1) -12+-4*V(1) 0001 0101 (01)B> 1011 11017+V(1) 1010 1000
<< Success! ==> defined new CTR 16 (PPA)
50888 116886422 -19708 0001 0101 (01)B> 1011 11014933 1010 1000
== Executing PA-CTR 10, V(1)=0, V(2)=4930, repcount=2466, factor=3/2
78014 262972262 20 0001 01017399 (01)B> 1011 1101 1010 1000
78015 262972271 17 0001 01017399 <A(10) 1010 1101 1010 1000
78016 263001867 -29579 0001 <A(10) 10107400 1101 1010 1000
78017 263001874 -29576 0101 (01)B> 10107400 1101 1010 1000
78018 263031474 24 01017401 (01)B> 1101 1010 1000
78019 263031479 21 01017401 <A(10) 1001 1010 1000
78020 263061083 -29583 <A(10) 10107401 1001 1010 1000
78021 263061086 -29580 0001 (01)B> 10107401 1001 1010 1000
Lines: 500
Top steps: 499
Macro steps: 78021
Basic steps: 263061086
Tape index: -29580
ones: 14809
log10(ones ): 4.171
log10(steps ): 8.420
Input to awk program:
gohalt 1
T 6-state 2-symbol #b (T.J. & S. Ligocki)
: >4.6x10^1439 >2.5x10^2879
C This was the best known 6x2 TM until May-2010
5T 1RB 0LE 1LC 0RA 1LD 0RC 1LE 0LF 1LA 1LC 1LE 1RH
L 18
M 500
pref sim
machv Lig62_b just simple
machv Lig62_b-r with repetitions reduced
machv Lig62_b-1 with tape symbol exponents
machv Lig62_b-m as 2-bck-2-macro machine
machv Lig62_b-a as 2-bck-2-macro machine with pure additive config-TRs
iam Lig62_b-a
mtype 2 0 2
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:14:23 CEST 2010
edate Tue Jul 6 22:14:25 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:14:23 CEST 2010