Comment: This TM produces 11974457230330 ones in 83425527831799543594604927 steps.
| State | on 0 |
on 1 |
on 0 | on 1 | ||||
|---|---|---|---|---|---|---|---|---|
| Move | Goto | Move | Goto | |||||
| A | B1R | C1L | 1 | right | B | 1 | left | C |
| B | A0L | D0L | 0 | left | A | 0 | left | D |
| C | A1L | Z1R | 1 | left | A | 1 | right | Z |
| D | B1L | E1R | 1 | left | B | 1 | right | E |
| E | D0R | F0R | 0 | right | D | 0 | right | F |
| F | F0R | D0L | 0 | right | F | 0 | left | D |
The same TM just simple.
The same TM with repetitions reduced.
The same TM with tape symbol exponents.
The same TM as 1-bck-2-macro machine.
Simulation is done as 1-bck-2-macro machine with pure additive config-TRs.
Pushing initial machine.
Pushing macro factor 1.
Pushing BCK machine.
Pushing macro factor 2.
Steps BasSteps BasTpos Tape contents
0 0 0 (0)A>
1 4 -2 <A(1) 10
2 8 0 01 (0)D> 10
3 10 2 012 (0)D>
4 12 0 012 <A(0) 10
5 14 -2 01 <A(1) 102
6 16 -4 <A(1) 11 102
7 20 -2 01 (0)D> 11 102
8 22 0 012 (0)F> 102
9 24 -2 012 <B(1) 00 10
10 28 -6 <B(1) 012 00 10
11 32 -8 <C(1) 013 00 10
12 38 -6 10 (1)E> 013 00 10
13 44 0 104 (1)E> 00 10
14 48 -2 104 <C(1) 01 10
15 56 -10 <C(1) 114 01 10
16 62 -8 10 (1)E> 114 01 10
17 66 -10 10 <D(0) 10 113 01 10
18 68 -12 <D(0) 102 113 01 10
19 70 -14 <A(0) 103 113 01 10
20 74 -16 <A(1) 104 113 01 10
21 78 -14 01 (0)D> 104 113 01 10
22 86 -6 015 (0)D> 113 01 10
23 88 -4 016 (0)F> 112 01 10
24 90 -6 016 <B(1) 01 11 01 10
25 102 -18 <B(1) 017 11 01 10
26 106 -20 <C(1) 018 11 01 10
27 112 -18 10 (1)E> 018 11 01 10
28 128 -2 109 (1)E> 11 01 10
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 101+V(1) (1)E> 114+V(2) [*]* [*]*
1 4 -2 101+V(1) <D(0) 10 113+V(2) [*]* [*]*
2 6+2*V(1) -4+-2*V(1) <D(0) 102+V(1) 113+V(2) [*]* [*]*
3 8+2*V(1) -6+-2*V(1) <A(0) 103+V(1) 113+V(2) [*]* [*]*
4 12+2*V(1) -8+-2*V(1) <A(1) 104+V(1) 113+V(2) [*]* [*]*
5 16+2*V(1) -6+-2*V(1) 01 (0)D> 104+V(1) 113+V(2) [*]* [*]*
6 24+4*V(1) 2 015+V(1) (0)D> 113+V(2) [*]* [*]*
7 26+4*V(1) 4 016+V(1) (0)F> 112+V(2) [*]* [*]*
8 28+4*V(1) 2 016+V(1) <B(1) 01 111+V(2) [*]* [*]*
9 40+6*V(1) -10+-2*V(1) <B(1) 017+V(1) 111+V(2) [*]* [*]*
10 44+6*V(1) -12+-2*V(1) <C(1) 018+V(1) 111+V(2) [*]* [*]*
11 50+6*V(1) -10+-2*V(1) 10 (1)E> 018+V(1) 111+V(2) [*]* [*]*
12 66+8*V(1) 6 109+V(1) (1)E> 111+V(2) [*]* [*]*
<< Success! ==> defined new CTR 1 (PA)
29 132 -4 109 <D(0) 10 01 10
30 150 -22 <D(0) 1010 01 10
31 152 -24 <A(0) 1011 01 10
32 156 -26 <A(1) 1012 01 10
33 160 -24 01 (0)D> 1012 01 10
34 184 0 0113 (0)D> 01 10
35 186 -2 0113 <A(0) 11 10
36 188 -4 0112 <A(1) 10 11 10
37 212 -28 <A(1) 1112 10 11 10
38 216 -26 01 (0)D> 1112 10 11 10
39 218 -24 012 (0)F> 1111 10 11 10
40 220 -26 012 <B(1) 01 1110 10 11 10
41 224 -30 <B(1) 013 1110 10 11 10
42 228 -32 <C(1) 014 1110 10 11 10
43 234 -30 10 (1)E> 014 1110 10 11 10
44 242 -22 105 (1)E> 1110 10 11 10
45 246 -24 105 <D(0) 10 119 10 11 10
46 256 -34 <D(0) 106 119 10 11 10
47 258 -36 <A(0) 107 119 10 11 10
48 262 -38 <A(1) 108 119 10 11 10
49 266 -36 01 (0)D> 108 119 10 11 10
50 282 -20 019 (0)D> 119 10 11 10
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 011+V(1) (0)D> 114+V(2) [*]* [*]* [*]*
1 2 2 012+V(1) (0)F> 113+V(2) [*]* [*]* [*]*
2 4 0 012+V(1) <B(1) 01 112+V(2) [*]* [*]* [*]*
3 8+2*V(1) -4+-2*V(1) <B(1) 013+V(1) 112+V(2) [*]* [*]* [*]*
4 12+2*V(1) -6+-2*V(1) <C(1) 014+V(1) 112+V(2) [*]* [*]* [*]*
5 18+2*V(1) -4+-2*V(1) 10 (1)E> 014+V(1) 112+V(2) [*]* [*]* [*]*
6 26+4*V(1) 4 105+V(1) (1)E> 112+V(2) [*]* [*]* [*]*
7 30+4*V(1) 2 105+V(1) <D(0) 10 111+V(2) [*]* [*]* [*]*
8 40+6*V(1) -8+-2*V(1) <D(0) 106+V(1) 111+V(2) [*]* [*]* [*]*
9 42+6*V(1) -10+-2*V(1) <A(0) 107+V(1) 111+V(2) [*]* [*]* [*]*
10 46+6*V(1) -12+-2*V(1) <A(1) 108+V(1) 111+V(2) [*]* [*]* [*]*
11 50+6*V(1) -10+-2*V(1) 01 (0)D> 108+V(1) 111+V(2) [*]* [*]* [*]*
12 66+8*V(1) 6 019+V(1) (0)D> 111+V(2) [*]* [*]* [*]*
<< Success! ==> defined new CTR 2 (PA)
50 282 -20 019 (0)D> 119 10 11 10
== Executing PA-CTR 2, V(1)=8, V(2)=5, repcount=2, factor=8/3
74 606 -8 0125 (0)D> 113 10 11 10
75 608 -6 0126 (0)F> 112 10 11 10
76 610 -8 0126 <B(1) 01 11 10 11 10
77 662 -60 <B(1) 0127 11 10 11 10
78 666 -62 <C(1) 0128 11 10 11 10
79 672 -60 10 (1)E> 0128 11 10 11 10
80 728 -4 1029 (1)E> 11 10 11 10
81 732 -6 1029 <D(0) 102 11 10
82 790 -64 <D(0) 1031 11 10
83 792 -66 <A(0) 1032 11 10
84 796 -68 <A(1) 1033 11 10
85 800 -66 01 (0)D> 1033 11 10
86 866 0 0134 (0)D> 11 10
87 868 2 0135 (0)F> 10
88 870 0 0135 <B(1)
89 940 -70 <B(1) 0135
90 944 -72 <C(1) 0136
91 950 -70 10 (1)E> 0136
92 1022 2 1037 (1)E>
93 1026 0 1037 <C(1) 01
94 1100 -74 <C(1) 1137 01
95 1106 -72 10 (1)E> 1137 01
96 1110 -74 10 <D(0) 10 1136 01
97 1112 -76 <D(0) 102 1136 01
98 1114 -78 <A(0) 103 1136 01
99 1118 -80 <A(1) 104 1136 01
100 1122 -78 01 (0)D> 104 1136 01
101 1130 -70 015 (0)D> 1136 01
102 1132 -68 016 (0)F> 1135 01
103 1134 -70 016 <B(1) 01 1134 01
104 1146 -82 <B(1) 017 1134 01
105 1150 -84 <C(1) 018 1134 01
106 1156 -82 10 (1)E> 018 1134 01
107 1172 -66 109 (1)E> 1134 01
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 101+V(1) (1)E> 114+V(2) [*]*
1 4 -2 101+V(1) <D(0) 10 113+V(2) [*]*
2 6+2*V(1) -4+-2*V(1) <D(0) 102+V(1) 113+V(2) [*]*
3 8+2*V(1) -6+-2*V(1) <A(0) 103+V(1) 113+V(2) [*]*
4 12+2*V(1) -8+-2*V(1) <A(1) 104+V(1) 113+V(2) [*]*
5 16+2*V(1) -6+-2*V(1) 01 (0)D> 104+V(1) 113+V(2) [*]*
6 24+4*V(1) 2 015+V(1) (0)D> 113+V(2) [*]*
7 26+4*V(1) 4 016+V(1) (0)F> 112+V(2) [*]*
8 28+4*V(1) 2 016+V(1) <B(1) 01 111+V(2) [*]*
9 40+6*V(1) -10+-2*V(1) <B(1) 017+V(1) 111+V(2) [*]*
10 44+6*V(1) -12+-2*V(1) <C(1) 018+V(1) 111+V(2) [*]*
11 50+6*V(1) -10+-2*V(1) 10 (1)E> 018+V(1) 111+V(2) [*]*
12 66+8*V(1) 6 109+V(1) (1)E> 111+V(2) [*]*
<< Success! ==> defined new CTR 3 (PA)
107 1172 -66 109 (1)E> 1134 01
== Executing PA-CTR 3, V(1)=8, V(2)=30, repcount=11, factor=8/3
239 6122 0 1097 (1)E> 11 01
240 6126 -2 1097 <D(0) 10 01
241 6320 -196 <D(0) 1098 01
242 6322 -198 <A(0) 1099 01
243 6326 -200 <A(1) 10100 01
244 6330 -198 01 (0)D> 10100 01
245 6530 2 01101 (0)D> 01
246 6532 0 01101 <A(0) 11
247 6534 -2 01100 <A(1) 10 11
248 6734 -202 <A(1) 11100 10 11
249 6738 -200 01 (0)D> 11100 10 11
250 6740 -198 012 (0)F> 1199 10 11
251 6742 -200 012 <B(1) 01 1198 10 11
252 6746 -204 <B(1) 013 1198 10 11
253 6750 -206 <C(1) 014 1198 10 11
254 6756 -204 10 (1)E> 014 1198 10 11
255 6764 -196 105 (1)E> 1198 10 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 103+V(1) (1)E> 11 01
1 4 -2 103+V(1) <D(0) 10 01
2 10+2*V(1) -8+-2*V(1) <D(0) 104+V(1) 01
3 12+2*V(1) -10+-2*V(1) <A(0) 105+V(1) 01
4 16+2*V(1) -12+-2*V(1) <A(1) 106+V(1) 01
5 20+2*V(1) -10+-2*V(1) 01 (0)D> 106+V(1) 01
6 32+4*V(1) 2 017+V(1) (0)D> 01
7 34+4*V(1) 0 017+V(1) <A(0) 11
8 36+4*V(1) -2 016+V(1) <A(1) 10 11
9 48+6*V(1) -14+-2*V(1) <A(1) 116+V(1) 10 11
10 52+6*V(1) -12+-2*V(1) 01 (0)D> 116+V(1) 10 11
11 54+6*V(1) -10+-2*V(1) 012 (0)F> 115+V(1) 10 11
12 56+6*V(1) -12+-2*V(1) 012 <B(1) 01 114+V(1) 10 11
13 60+6*V(1) -16+-2*V(1) <B(1) 013 114+V(1) 10 11
14 64+6*V(1) -18+-2*V(1) <C(1) 014 114+V(1) 10 11
15 70+6*V(1) -16+-2*V(1) 10 (1)E> 014 114+V(1) 10 11
16 78+6*V(1) -8+-2*V(1) 105 (1)E> 114+V(1) 10 11
<< Success! ==> defined new CTR 4 (PPA)
255 6764 -196 105 (1)E> 1198 10 11
== Executing PA-CTR 1, V(1)=4, V(2)=94, repcount=32, factor=8/3
639 41644 -4 10261 (1)E> 112 10 11
640 41648 -6 10261 <D(0) 10 11 10 11
641 42170 -528 <D(0) 10262 11 10 11
642 42172 -530 <A(0) 10263 11 10 11
643 42176 -532 <A(1) 10264 11 10 11
644 42180 -530 01 (0)D> 10264 11 10 11
645 42708 -2 01265 (0)D> 11 10 11
646 42710 0 01266 (0)F> 10 11
647 42712 -2 01266 <B(1) 00 11
648 43244 -534 <B(1) 01266 00 11
649 43248 -536 <C(1) 01267 00 11
650 43254 -534 10 (1)E> 01267 00 11
651 43788 0 10268 (1)E> 00 11
652 43792 -2 10268 <C(1) 01 11
653 44328 -538 <C(1) 11268 01 11
654 44334 -536 10 (1)E> 11268 01 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 101+V(1) (1)E> 112 10 [*]*
1 4 -2 101+V(1) <D(0) 10 11 10 [*]*
2 6+2*V(1) -4+-2*V(1) <D(0) 102+V(1) 11 10 [*]*
3 8+2*V(1) -6+-2*V(1) <A(0) 103+V(1) 11 10 [*]*
4 12+2*V(1) -8+-2*V(1) <A(1) 104+V(1) 11 10 [*]*
5 16+2*V(1) -6+-2*V(1) 01 (0)D> 104+V(1) 11 10 [*]*
6 24+4*V(1) 2 015+V(1) (0)D> 11 10 [*]*
7 26+4*V(1) 4 016+V(1) (0)F> 10 [*]*
8 28+4*V(1) 2 016+V(1) <B(1) 00 [*]*
9 40+6*V(1) -10+-2*V(1) <B(1) 016+V(1) 00 [*]*
10 44+6*V(1) -12+-2*V(1) <C(1) 017+V(1) 00 [*]*
11 50+6*V(1) -10+-2*V(1) 10 (1)E> 017+V(1) 00 [*]*
12 64+8*V(1) 4 108+V(1) (1)E> 00 [*]*
13 68+8*V(1) 2 108+V(1) <C(1) 01 [*]*
14 84+10*V(1) -14+-2*V(1) <C(1) 118+V(1) 01 [*]*
15 90+10*V(1) -12+-2*V(1) 10 (1)E> 118+V(1) 01 [*]*
<< Success! ==> defined new CTR 5 (PPA)
654 44334 -536 10 (1)E> 11268 01 11
== Executing PA-CTR 1, V(1)=0, V(2)=264, repcount=89, factor=8/3
1722 300832 -2 10713 (1)E> 11 01 11
1723 300836 -4 10713 <D(0) 10 01 11
1724 302262 -1430 <D(0) 10714 01 11
1725 302264 -1432 <A(0) 10715 01 11
1726 302268 -1434 <A(1) 10716 01 11
1727 302272 -1432 01 (0)D> 10716 01 11
1728 303704 0 01717 (0)D> 01 11
1729 303706 -2 01717 <A(0) 112
1730 303708 -4 01716 <A(1) 10 112
1731 305140 -1436 <A(1) 11716 10 112
1732 305144 -1434 01 (0)D> 11716 10 112
1733 305146 -1432 012 (0)F> 11715 10 112
1734 305148 -1434 012 <B(1) 01 11714 10 112
1735 305152 -1438 <B(1) 013 11714 10 112
1736 305156 -1440 <C(1) 014 11714 10 112
1737 305162 -1438 10 (1)E> 014 11714 10 112
1738 305170 -1430 105 (1)E> 11714 10 112
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 103+V(1) (1)E> 11 01 111+V(2)
1 4 -2 103+V(1) <D(0) 10 01 111+V(2)
2 10+2*V(1) -8+-2*V(1) <D(0) 104+V(1) 01 111+V(2)
3 12+2*V(1) -10+-2*V(1) <A(0) 105+V(1) 01 111+V(2)
4 16+2*V(1) -12+-2*V(1) <A(1) 106+V(1) 01 111+V(2)
5 20+2*V(1) -10+-2*V(1) 01 (0)D> 106+V(1) 01 111+V(2)
6 32+4*V(1) 2 017+V(1) (0)D> 01 111+V(2)
7 34+4*V(1) 0 017+V(1) <A(0) 112+V(2)
8 36+4*V(1) -2 016+V(1) <A(1) 10 112+V(2)
9 48+6*V(1) -14+-2*V(1) <A(1) 116+V(1) 10 112+V(2)
10 52+6*V(1) -12+-2*V(1) 01 (0)D> 116+V(1) 10 112+V(2)
11 54+6*V(1) -10+-2*V(1) 012 (0)F> 115+V(1) 10 112+V(2)
12 56+6*V(1) -12+-2*V(1) 012 <B(1) 01 114+V(1) 10 112+V(2)
13 60+6*V(1) -16+-2*V(1) <B(1) 013 114+V(1) 10 112+V(2)
14 64+6*V(1) -18+-2*V(1) <C(1) 014 114+V(1) 10 112+V(2)
15 70+6*V(1) -16+-2*V(1) 10 (1)E> 014 114+V(1) 10 112+V(2)
16 78+6*V(1) -8+-2*V(1) 105 (1)E> 114+V(1) 10 112+V(2)
<< Success! ==> defined new CTR 6 (PPA)
1738 305170 -1430 105 (1)E> 11714 10 112
== Executing PA-CTR 1, V(1)=4, V(2)=710, repcount=237, factor=8/3
4582 2118220 -8 101901 (1)E> 113 10 112
4583 2118224 -10 101901 <D(0) 10 112 10 112
4584 2122026 -3812 <D(0) 101902 112 10 112
4585 2122028 -3814 <A(0) 101903 112 10 112
4586 2122032 -3816 <A(1) 101904 112 10 112
4587 2122036 -3814 01 (0)D> 101904 112 10 112
4588 2125844 -6 011905 (0)D> 112 10 112
4589 2125846 -4 011906 (0)F> 11 10 112
4590 2125848 -6 011906 <B(1) 01 10 112
4591 2129660 -3818 <B(1) 011907 10 112
4592 2129664 -3820 <C(1) 011908 10 112
4593 2129670 -3818 10 (1)E> 011908 10 112
4594 2133486 -2 101909 (1)E> 10 112
4595 2133488 0 101910 (0)F> 112
4596 2133490 -2 101910 <B(1) 01 11
4597 2133492 -4 101909 <C(1) 012 11
4598 2137310 -3822 <C(1) 111909 012 11
4599 2137316 -3820 10 (1)E> 111909 012 11
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 101+V(1) (1)E> 113 10 112+V(2)
1 4 -2 101+V(1) <D(0) 10 112 10 112+V(2)
2 6+2*V(1) -4+-2*V(1) <D(0) 102+V(1) 112 10 112+V(2)
3 8+2*V(1) -6+-2*V(1) <A(0) 103+V(1) 112 10 112+V(2)
4 12+2*V(1) -8+-2*V(1) <A(1) 104+V(1) 112 10 112+V(2)
5 16+2*V(1) -6+-2*V(1) 01 (0)D> 104+V(1) 112 10 112+V(2)
6 24+4*V(1) 2 015+V(1) (0)D> 112 10 112+V(2)
7 26+4*V(1) 4 016+V(1) (0)F> 11 10 112+V(2)
8 28+4*V(1) 2 016+V(1) <B(1) 01 10 112+V(2)
9 40+6*V(1) -10+-2*V(1) <B(1) 017+V(1) 10 112+V(2)
10 44+6*V(1) -12+-2*V(1) <C(1) 018+V(1) 10 112+V(2)
11 50+6*V(1) -10+-2*V(1) 10 (1)E> 018+V(1) 10 112+V(2)
12 66+8*V(1) 6 109+V(1) (1)E> 10 112+V(2)
13 68+8*V(1) 8 1010+V(1) (0)F> 112+V(2)
14 70+8*V(1) 6 1010+V(1) <B(1) 01 111+V(2)
15 72+8*V(1) 4 109+V(1) <C(1) 012 111+V(2)
16 90+10*V(1) -14+-2*V(1) <C(1) 119+V(1) 012 111+V(2)
17 96+10*V(1) -12+-2*V(1) 10 (1)E> 119+V(1) 012 111+V(2)
<< Success! ==> defined new CTR 7 (PPA)
4599 2137316 -3820 10 (1)E> 111909 012 11
== Executing PA-CTR 1, V(1)=0, V(2)=1905, repcount=636, factor=8/3
12231 15102812 -4 105089 (1)E> 11 012 11
12232 15102816 -6 105089 <D(0) 10 012 11
12233 15112994 -10184 <D(0) 105090 012 11
12234 15112996 -10186 <A(0) 105091 012 11
12235 15113000 -10188 <A(1) 105092 012 11
12236 15113004 -10186 01 (0)D> 105092 012 11
12237 15123188 -2 015093 (0)D> 012 11
12238 15123190 -4 015093 <A(0) 11 01 11
12239 15123192 -6 015092 <A(1) 10 11 01 11
12240 15133376 -10190 <A(1) 115092 10 11 01 11
12241 15133380 -10188 01 (0)D> 115092 10 11 01 11
12242 15133382 -10186 012 (0)F> 115091 10 11 01 11
12243 15133384 -10188 012 <B(1) 01 115090 10 11 01 11
12244 15133388 -10192 <B(1) 013 115090 10 11 01 11
12245 15133392 -10194 <C(1) 014 115090 10 11 01 11
12246 15133398 -10192 10 (1)E> 014 115090 10 11 01 11
12247 15133406 -10184 105 (1)E> 115090 10 11 01 11
12248 15133410 -10186 105 <D(0) 10 115089 10 11 01 11
12249 15133420 -10196 <D(0) 106 115089 10 11 01 11
12250 15133422 -10198 <A(0) 107 115089 10 11 01 11
12251 15133426 -10200 <A(1) 108 115089 10 11 01 11
12252 15133430 -10198 01 (0)D> 108 115089 10 11 01 11
12253 15133446 -10182 019 (0)D> 115089 10 11 01 11
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 011+V(1) (0)D> 114+V(2) [*]* [*]* [*]* [*]*
1 2 2 012+V(1) (0)F> 113+V(2) [*]* [*]* [*]* [*]*
2 4 0 012+V(1) <B(1) 01 112+V(2) [*]* [*]* [*]* [*]*
3 8+2*V(1) -4+-2*V(1) <B(1) 013+V(1) 112+V(2) [*]* [*]* [*]* [*]*
4 12+2*V(1) -6+-2*V(1) <C(1) 014+V(1) 112+V(2) [*]* [*]* [*]* [*]*
5 18+2*V(1) -4+-2*V(1) 10 (1)E> 014+V(1) 112+V(2) [*]* [*]* [*]* [*]*
6 26+4*V(1) 4 105+V(1) (1)E> 112+V(2) [*]* [*]* [*]* [*]*
7 30+4*V(1) 2 105+V(1) <D(0) 10 111+V(2) [*]* [*]* [*]* [*]*
8 40+6*V(1) -8+-2*V(1) <D(0) 106+V(1) 111+V(2) [*]* [*]* [*]* [*]*
9 42+6*V(1) -10+-2*V(1) <A(0) 107+V(1) 111+V(2) [*]* [*]* [*]* [*]*
10 46+6*V(1) -12+-2*V(1) <A(1) 108+V(1) 111+V(2) [*]* [*]* [*]* [*]*
11 50+6*V(1) -10+-2*V(1) 01 (0)D> 108+V(1) 111+V(2) [*]* [*]* [*]* [*]*
12 66+8*V(1) 6 019+V(1) (0)D> 111+V(2) [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 8 (PA)
12253 15133446 -10182 019 (0)D> 115089 10 11 01 11
== Executing PA-CTR 8, V(1)=8, V(2)=5085, repcount=1696, factor=8/3
32605 107344966 -6 0113577 (0)D> 11 10 11 01 11
32606 107344968 -4 0113578 (0)F> 10 11 01 11
32607 107344970 -6 0113578 <B(1) 00 11 01 11
32608 107372126 -27162 <B(1) 0113578 00 11 01 11
32609 107372130 -27164 <C(1) 0113579 00 11 01 11
32610 107372136 -27162 10 (1)E> 0113579 00 11 01 11
32611 107399294 -4 1013580 (1)E> 00 11 01 11
32612 107399298 -6 1013580 <C(1) 01 11 01 11
32613 107426458 -27166 <C(1) 1113580 01 11 01 11
32614 107426464 -27164 10 (1)E> 1113580 01 11 01 11
32615 107426468 -27166 10 <D(0) 10 1113579 01 11 01 11
32616 107426470 -27168 <D(0) 102 1113579 01 11 01 11
32617 107426472 -27170 <A(0) 103 1113579 01 11 01 11
32618 107426476 -27172 <A(1) 104 1113579 01 11 01 11
32619 107426480 -27170 01 (0)D> 104 1113579 01 11 01 11
32620 107426488 -27162 015 (0)D> 1113579 01 11 01 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 012+V(1) (0)D> 11 10 [*]* [*]* [*]*
1 2 2 013+V(1) (0)F> 10 [*]* [*]* [*]*
2 4 0 013+V(1) <B(1) 00 [*]* [*]* [*]*
3 10+2*V(1) -6+-2*V(1) <B(1) 013+V(1) 00 [*]* [*]* [*]*
4 14+2*V(1) -8+-2*V(1) <C(1) 014+V(1) 00 [*]* [*]* [*]*
5 20+2*V(1) -6+-2*V(1) 10 (1)E> 014+V(1) 00 [*]* [*]* [*]*
6 28+4*V(1) 2 105+V(1) (1)E> 00 [*]* [*]* [*]*
7 32+4*V(1) 0 105+V(1) <C(1) 01 [*]* [*]* [*]*
8 42+6*V(1) -10+-2*V(1) <C(1) 115+V(1) 01 [*]* [*]* [*]*
9 48+6*V(1) -8+-2*V(1) 10 (1)E> 115+V(1) 01 [*]* [*]* [*]*
10 52+6*V(1) -10+-2*V(1) 10 <D(0) 10 114+V(1) 01 [*]* [*]* [*]*
11 54+6*V(1) -12+-2*V(1) <D(0) 102 114+V(1) 01 [*]* [*]* [*]*
12 56+6*V(1) -14+-2*V(1) <A(0) 103 114+V(1) 01 [*]* [*]* [*]*
13 60+6*V(1) -16+-2*V(1) <A(1) 104 114+V(1) 01 [*]* [*]* [*]*
14 64+6*V(1) -14+-2*V(1) 01 (0)D> 104 114+V(1) 01 [*]* [*]* [*]*
15 72+6*V(1) -6+-2*V(1) 015 (0)D> 114+V(1) 01 [*]* [*]* [*]*
<< Success! ==> defined new CTR 9 (PPA)
32620 107426488 -27162 015 (0)D> 1113579 01 11 01 11
== Executing PA-CTR 8, V(1)=4, V(2)=13575, repcount=4526, factor=8/3
86932 763234836 -6 0136213 (0)D> 11 01 11 01 11
86933 763234838 -4 0136214 (0)F> 01 11 01 11
86934 763234842 -6 0136214 <A(0) 10 11 01 11
86935 763234844 -8 0136213 <A(1) 102 11 01 11
86936 763307270 -72434 <A(1) 1136213 102 11 01 11
86937 763307274 -72432 01 (0)D> 1136213 102 11 01 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 014+V(1) (0)D> 11 01 [*]* [*]* [*]*
1 2 2 015+V(1) (0)F> 01 [*]* [*]* [*]*
2 6 0 015+V(1) <A(0) 10 [*]* [*]* [*]*
3 8 -2 014+V(1) <A(1) 102 [*]* [*]* [*]*
4 16+2*V(1) -10+-2*V(1) <A(1) 114+V(1) 102 [*]* [*]* [*]*
5 20+2*V(1) -8+-2*V(1) 01 (0)D> 114+V(1) 102 [*]* [*]* [*]*
<< Success! ==> defined new CTR 10 (PPA)
86937 763307274 -72432 01 (0)D> 1136213 102 11 01 11
== Executing PA-CTR 8, V(1)=0, V(2)=36209, repcount=12070, factor=8/3
231777 5425634454 -12 0196561 (0)D> 113 102 11 01 11
231778 5425634456 -10 0196562 (0)F> 112 102 11 01 11
231779 5425634458 -12 0196562 <B(1) 01 11 102 11 01 11
231780 5425827582 -193136 <B(1) 0196563 11 102 11 01 11
231781 5425827586 -193138 <C(1) 0196564 11 102 11 01 11
231782 5425827592 -193136 10 (1)E> 0196564 11 102 11 01 11
231783 5426020720 -8 1096565 (1)E> 11 102 11 01 11
231784 5426020724 -10 1096565 <D(0) 103 11 01 11
231785 5426213854 -193140 <D(0) 1096568 11 01 11
231786 5426213856 -193142 <A(0) 1096569 11 01 11
231787 5426213860 -193144 <A(1) 1096570 11 01 11
231788 5426213864 -193142 01 (0)D> 1096570 11 01 11
231789 5426407004 -2 0196571 (0)D> 11 01 11
231790 5426407006 0 0196572 (0)F> 01 11
231791 5426407010 -2 0196572 <A(0) 10 11
231792 5426407012 -4 0196571 <A(1) 102 11
231793 5426600154 -193146 <A(1) 1196571 102 11
231794 5426600158 -193144 01 (0)D> 1196571 102 11
231795 5426600160 -193142 012 (0)F> 1196570 102 11
231796 5426600162 -193144 012 <B(1) 01 1196569 102 11
231797 5426600166 -193148 <B(1) 013 1196569 102 11
231798 5426600170 -193150 <C(1) 014 1196569 102 11
231799 5426600176 -193148 10 (1)E> 014 1196569 102 11
231800 5426600184 -193140 105 (1)E> 1196569 102 11
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 011+V(1) (0)D> 113 101+V(2) 11 01 [*]*
1 2 2 012+V(1) (0)F> 112 101+V(2) 11 01 [*]*
2 4 0 012+V(1) <B(1) 01 11 101+V(2) 11 01 [*]*
3 8+2*V(1) -4+-2*V(1) <B(1) 013+V(1) 11 101+V(2) 11 01 [*]*
4 12+2*V(1) -6+-2*V(1) <C(1) 014+V(1) 11 101+V(2) 11 01 [*]*
5 18+2*V(1) -4+-2*V(1) 10 (1)E> 014+V(1) 11 101+V(2) 11 01 [*]*
6 26+4*V(1) 4 105+V(1) (1)E> 11 101+V(2) 11 01 [*]*
7 30+4*V(1) 2 105+V(1) <D(0) 102+V(2) 11 01 [*]*
8 40+6*V(1) -8+-2*V(1) <D(0) 107+V(1)+V(2) 11 01 [*]*
9 42+6*V(1) -10+-2*V(1) <A(0) 108+V(1)+V(2) 11 01 [*]*
10 46+6*V(1) -12+-2*V(1) <A(1) 109+V(1)+V(2) 11 01 [*]*
11 50+6*V(1) -10+-2*V(1) 01 (0)D> 109+V(1)+V(2) 11 01 [*]*
12 68+8*V(1)+2*V(2) 8+2*V(2) 0110+V(1)+V(2) (0)D> 11 01 [*]*
13 70+8*V(1)+2*V(2) 10+2*V(2) 0111+V(1)+V(2) (0)F> 01 [*]*
14 74+8*V(1)+2*V(2) 8+2*V(2) 0111+V(1)+V(2) <A(0) 10 [*]*
15 76+8*V(1)+2*V(2) 6+2*V(2) 0110+V(1)+V(2) <A(1) 102 [*]*
16 96+10*V(1)+4*V(2) -14+-2*V(1) <A(1) 1110+V(1)+V(2) 102 [*]*
17 100+10*V(1)+4*V(2) -12+-2*V(1) 01 (0)D> 1110+V(1)+V(2) 102 [*]*
18 102+10*V(1)+4*V(2) -10+-2*V(1) 012 (0)F> 119+V(1)+V(2) 102 [*]*
19 104+10*V(1)+4*V(2) -12+-2*V(1) 012 <B(1) 01 118+V(1)+V(2) 102 [*]*
20 108+10*V(1)+4*V(2) -16+-2*V(1) <B(1) 013 118+V(1)+V(2) 102 [*]*
21 112+10*V(1)+4*V(2) -18+-2*V(1) <C(1) 014 118+V(1)+V(2) 102 [*]*
22 118+10*V(1)+4*V(2) -16+-2*V(1) 10 (1)E> 014 118+V(1)+V(2) 102 [*]*
23 126+10*V(1)+4*V(2) -8+-2*V(1) 105 (1)E> 118+V(1)+V(2) 102 [*]*
<< Success! ==> defined new CTR 11 (PPA)
231800 5426600184 -193140 105 (1)E> 1196569 102 11
== Executing PA-CTR 1, V(1)=4, V(2)=96565, repcount=32189, factor=8/3
618068 38584939730 -6 10257517 (1)E> 112 102 11
618069 38584939734 -8 10257517 <D(0) 10 11 102 11
618070 38585454768 -515042 <D(0) 10257518 11 102 11
618071 38585454770 -515044 <A(0) 10257519 11 102 11
618072 38585454774 -515046 <A(1) 10257520 11 102 11
618073 38585454778 -515044 01 (0)D> 10257520 11 102 11
618074 38585969818 -4 01257521 (0)D> 11 102 11
618075 38585969820 -2 01257522 (0)F> 102 11
618076 38585969822 -4 01257522 <B(1) 00 10 11
618077 38586484866 -515048 <B(1) 01257522 00 10 11
618078 38586484870 -515050 <C(1) 01257523 00 10 11
618079 38586484876 -515048 10 (1)E> 01257523 00 10 11
618080 38586999922 -2 10257524 (1)E> 00 10 11
618081 38586999926 -4 10257524 <C(1) 01 10 11
618082 38587514974 -515052 <C(1) 11257524 01 10 11
618083 38587514980 -515050 10 (1)E> 11257524 01 10 11
618084 38587514984 -515052 10 <D(0) 10 11257523 01 10 11
618085 38587514986 -515054 <D(0) 102 11257523 01 10 11
618086 38587514988 -515056 <A(0) 103 11257523 01 10 11
618087 38587514992 -515058 <A(1) 104 11257523 01 10 11
618088 38587514996 -515056 01 (0)D> 104 11257523 01 10 11
618089 38587515004 -515048 015 (0)D> 11257523 01 10 11
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 101+V(1) (1)E> 112 102+V(2) [*]*
1 4 -2 101+V(1) <D(0) 10 11 102+V(2) [*]*
2 6+2*V(1) -4+-2*V(1) <D(0) 102+V(1) 11 102+V(2) [*]*
3 8+2*V(1) -6+-2*V(1) <A(0) 103+V(1) 11 102+V(2) [*]*
4 12+2*V(1) -8+-2*V(1) <A(1) 104+V(1) 11 102+V(2) [*]*
5 16+2*V(1) -6+-2*V(1) 01 (0)D> 104+V(1) 11 102+V(2) [*]*
6 24+4*V(1) 2 015+V(1) (0)D> 11 102+V(2) [*]*
7 26+4*V(1) 4 016+V(1) (0)F> 102+V(2) [*]*
8 28+4*V(1) 2 016+V(1) <B(1) 00 101+V(2) [*]*
9 40+6*V(1) -10+-2*V(1) <B(1) 016+V(1) 00 101+V(2) [*]*
10 44+6*V(1) -12+-2*V(1) <C(1) 017+V(1) 00 101+V(2) [*]*
11 50+6*V(1) -10+-2*V(1) 10 (1)E> 017+V(1) 00 101+V(2) [*]*
12 64+8*V(1) 4 108+V(1) (1)E> 00 101+V(2) [*]*
13 68+8*V(1) 2 108+V(1) <C(1) 01 101+V(2) [*]*
14 84+10*V(1) -14+-2*V(1) <C(1) 118+V(1) 01 101+V(2) [*]*
15 90+10*V(1) -12+-2*V(1) 10 (1)E> 118+V(1) 01 101+V(2) [*]*
16 94+10*V(1) -14+-2*V(1) 10 <D(0) 10 117+V(1) 01 101+V(2) [*]*
17 96+10*V(1) -16+-2*V(1) <D(0) 102 117+V(1) 01 101+V(2) [*]*
18 98+10*V(1) -18+-2*V(1) <A(0) 103 117+V(1) 01 101+V(2) [*]*
19 102+10*V(1) -20+-2*V(1) <A(1) 104 117+V(1) 01 101+V(2) [*]*
20 106+10*V(1) -18+-2*V(1) 01 (0)D> 104 117+V(1) 01 101+V(2) [*]*
21 114+10*V(1) -10+-2*V(1) 015 (0)D> 117+V(1) 01 101+V(2) [*]*
<< Success! ==> defined new CTR 12 (PPA)
618089 38587515004 -515048 015 (0)D> 11257523 01 10 11
== Executing PA-CTR 2, V(1)=4, V(2)=257519, repcount=85840, factor=8/3
1648169 274385359644 -8 01686725 (0)D> 113 01 10 11
1648170 274385359646 -6 01686726 (0)F> 112 01 10 11
1648171 274385359648 -8 01686726 <B(1) 01 11 01 10 11
1648172 274386733100 -1373460 <B(1) 01686727 11 01 10 11
1648173 274386733104 -1373462 <C(1) 01686728 11 01 10 11
1648174 274386733110 -1373460 10 (1)E> 01686728 11 01 10 11
1648175 274388106566 -4 10686729 (1)E> 11 01 10 11
1648176 274388106570 -6 10686729 <D(0) 10 01 10 11
1648177 274389480028 -1373464 <D(0) 10686730 01 10 11
1648178 274389480030 -1373466 <A(0) 10686731 01 10 11
1648179 274389480034 -1373468 <A(1) 10686732 01 10 11
1648180 274389480038 -1373466 01 (0)D> 10686732 01 10 11
1648181 274390853502 -2 01686733 (0)D> 01 10 11
1648182 274390853504 -4 01686733 <A(0) 11 10 11
1648183 274390853506 -6 01686732 <A(1) 10 11 10 11
1648184 274392226970 -1373470 <A(1) 11686732 10 11 10 11
1648185 274392226974 -1373468 01 (0)D> 11686732 10 11 10 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 011+V(1) (0)D> 113 01 [*]* [*]*
1 2 2 012+V(1) (0)F> 112 01 [*]* [*]*
2 4 0 012+V(1) <B(1) 01 11 01 [*]* [*]*
3 8+2*V(1) -4+-2*V(1) <B(1) 013+V(1) 11 01 [*]* [*]*
4 12+2*V(1) -6+-2*V(1) <C(1) 014+V(1) 11 01 [*]* [*]*
5 18+2*V(1) -4+-2*V(1) 10 (1)E> 014+V(1) 11 01 [*]* [*]*
6 26+4*V(1) 4 105+V(1) (1)E> 11 01 [*]* [*]*
7 30+4*V(1) 2 105+V(1) <D(0) 10 01 [*]* [*]*
8 40+6*V(1) -8+-2*V(1) <D(0) 106+V(1) 01 [*]* [*]*
9 42+6*V(1) -10+-2*V(1) <A(0) 107+V(1) 01 [*]* [*]*
10 46+6*V(1) -12+-2*V(1) <A(1) 108+V(1) 01 [*]* [*]*
11 50+6*V(1) -10+-2*V(1) 01 (0)D> 108+V(1) 01 [*]* [*]*
12 66+8*V(1) 6 019+V(1) (0)D> 01 [*]* [*]*
13 68+8*V(1) 4 019+V(1) <A(0) 11 [*]* [*]*
14 70+8*V(1) 2 018+V(1) <A(1) 10 11 [*]* [*]*
15 86+10*V(1) -14+-2*V(1) <A(1) 118+V(1) 10 11 [*]* [*]*
16 90+10*V(1) -12+-2*V(1) 01 (0)D> 118+V(1) 10 11 [*]* [*]*
<< Success! ==> defined new CTR 13 (PPA)
1648185 274392226974 -1373468 01 (0)D> 11686732 10 11 10 11
== Executing PA-CTR 8, V(1)=0, V(2)=686728, repcount=228910, factor=8/3
4395105 1951193229114 -8 011831281 (0)D> 112 10 11 10 11
4395106 1951193229116 -6 011831282 (0)F> 11 10 11 10 11
4395107 1951193229118 -8 011831282 <B(1) 01 10 11 10 11
4395108 1951196891682 -3662572 <B(1) 011831283 10 11 10 11
4395109 1951196891686 -3662574 <C(1) 011831284 10 11 10 11
4395110 1951196891692 -3662572 10 (1)E> 011831284 10 11 10 11
4395111 1951200554260 -4 101831285 (1)E> 10 11 10 11
4395112 1951200554262 -2 101831286 (0)F> 11 10 11
4395113 1951200554264 -4 101831286 <B(1) 01 10 11
4395114 1951200554266 -6 101831285 <C(1) 012 10 11
4395115 1951204216836 -3662576 <C(1) 111831285 012 10 11
4395116 1951204216842 -3662574 10 (1)E> 111831285 012 10 11
4395117 1951204216846 -3662576 10 <D(0) 10 111831284 012 10 11
4395118 1951204216848 -3662578 <D(0) 102 111831284 012 10 11
4395119 1951204216850 -3662580 <A(0) 103 111831284 012 10 11
4395120 1951204216854 -3662582 <A(1) 104 111831284 012 10 11
4395121 1951204216858 -3662580 01 (0)D> 104 111831284 012 10 11
4395122 1951204216866 -3662572 015 (0)D> 111831284 012 10 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 011+V(1) (0)D> 112 10 11 [*]* [*]*
1 2 2 012+V(1) (0)F> 11 10 11 [*]* [*]*
2 4 0 012+V(1) <B(1) 01 10 11 [*]* [*]*
3 8+2*V(1) -4+-2*V(1) <B(1) 013+V(1) 10 11 [*]* [*]*
4 12+2*V(1) -6+-2*V(1) <C(1) 014+V(1) 10 11 [*]* [*]*
5 18+2*V(1) -4+-2*V(1) 10 (1)E> 014+V(1) 10 11 [*]* [*]*
6 26+4*V(1) 4 105+V(1) (1)E> 10 11 [*]* [*]*
7 28+4*V(1) 6 106+V(1) (0)F> 11 [*]* [*]*
8 30+4*V(1) 4 106+V(1) <B(1) 01 [*]* [*]*
9 32+4*V(1) 2 105+V(1) <C(1) 012 [*]* [*]*
10 42+6*V(1) -8+-2*V(1) <C(1) 115+V(1) 012 [*]* [*]*
11 48+6*V(1) -6+-2*V(1) 10 (1)E> 115+V(1) 012 [*]* [*]*
12 52+6*V(1) -8+-2*V(1) 10 <D(0) 10 114+V(1) 012 [*]* [*]*
13 54+6*V(1) -10+-2*V(1) <D(0) 102 114+V(1) 012 [*]* [*]*
14 56+6*V(1) -12+-2*V(1) <A(0) 103 114+V(1) 012 [*]* [*]*
15 60+6*V(1) -14+-2*V(1) <A(1) 104 114+V(1) 012 [*]* [*]*
16 64+6*V(1) -12+-2*V(1) 01 (0)D> 104 114+V(1) 012 [*]* [*]*
17 72+6*V(1) -4+-2*V(1) 015 (0)D> 114+V(1) 012 [*]* [*]*
<< Success! ==> defined new CTR 14 (PPA)
4395122 1951204216866 -3662572 015 (0)D> 111831284 012 10 11
== Executing PA-CTR 2, V(1)=4, V(2)=1831280, repcount=610427, factor=8/3
11720246 13875120419576 -10 014883421 (0)D> 113 012 10 11
11720247 13875120419578 -8 014883422 (0)F> 112 012 10 11
11720248 13875120419580 -10 014883422 <B(1) 01 11 012 10 11
11720249 13875130186424 -9766854 <B(1) 014883423 11 012 10 11
11720250 13875130186428 -9766856 <C(1) 014883424 11 012 10 11
11720251 13875130186434 -9766854 10 (1)E> 014883424 11 012 10 11
11720252 13875139953282 -6 104883425 (1)E> 11 012 10 11
11720253 13875139953286 -8 104883425 <D(0) 10 012 10 11
11720254 13875149720136 -9766858 <D(0) 104883426 012 10 11
11720255 13875149720138 -9766860 <A(0) 104883427 012 10 11
11720256 13875149720142 -9766862 <A(1) 104883428 012 10 11
11720257 13875149720146 -9766860 01 (0)D> 104883428 012 10 11
11720258 13875159487002 -4 014883429 (0)D> 012 10 11
11720259 13875159487004 -6 014883429 <A(0) 11 01 10 11
11720260 13875159487006 -8 014883428 <A(1) 10 11 01 10 11
11720261 13875169253862 -9766864 <A(1) 114883428 10 11 01 10 11
11720262 13875169253866 -9766862 01 (0)D> 114883428 10 11 01 10 11
11720263 13875169253868 -9766860 012 (0)F> 114883427 10 11 01 10 11
11720264 13875169253870 -9766862 012 <B(1) 01 114883426 10 11 01 10 11
11720265 13875169253874 -9766866 <B(1) 013 114883426 10 11 01 10 11
11720266 13875169253878 -9766868 <C(1) 014 114883426 10 11 01 10 11
11720267 13875169253884 -9766866 10 (1)E> 014 114883426 10 11 01 10 11
11720268 13875169253892 -9766858 105 (1)E> 114883426 10 11 01 10 11
11720269 13875169253896 -9766860 105 <D(0) 10 114883425 10 11 01 10 11
11720270 13875169253906 -9766870 <D(0) 106 114883425 10 11 01 10 11
11720271 13875169253908 -9766872 <A(0) 107 114883425 10 11 01 10 11
11720272 13875169253912 -9766874 <A(1) 108 114883425 10 11 01 10 11
11720273 13875169253916 -9766872 01 (0)D> 108 114883425 10 11 01 10 11
11720274 13875169253932 -9766856 019 (0)D> 114883425 10 11 01 10 11
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 011+V(1) (0)D> 114+V(2) [*]* [*]* [*]* [*]* [*]*
1 2 2 012+V(1) (0)F> 113+V(2) [*]* [*]* [*]* [*]* [*]*
2 4 0 012+V(1) <B(1) 01 112+V(2) [*]* [*]* [*]* [*]* [*]*
3 8+2*V(1) -4+-2*V(1) <B(1) 013+V(1) 112+V(2) [*]* [*]* [*]* [*]* [*]*
4 12+2*V(1) -6+-2*V(1) <C(1) 014+V(1) 112+V(2) [*]* [*]* [*]* [*]* [*]*
5 18+2*V(1) -4+-2*V(1) 10 (1)E> 014+V(1) 112+V(2) [*]* [*]* [*]* [*]* [*]*
6 26+4*V(1) 4 105+V(1) (1)E> 112+V(2) [*]* [*]* [*]* [*]* [*]*
7 30+4*V(1) 2 105+V(1) <D(0) 10 111+V(2) [*]* [*]* [*]* [*]* [*]*
8 40+6*V(1) -8+-2*V(1) <D(0) 106+V(1) 111+V(2) [*]* [*]* [*]* [*]* [*]*
9 42+6*V(1) -10+-2*V(1) <A(0) 107+V(1) 111+V(2) [*]* [*]* [*]* [*]* [*]*
10 46+6*V(1) -12+-2*V(1) <A(1) 108+V(1) 111+V(2) [*]* [*]* [*]* [*]* [*]*
11 50+6*V(1) -10+-2*V(1) 01 (0)D> 108+V(1) 111+V(2) [*]* [*]* [*]* [*]* [*]*
12 66+8*V(1) 6 019+V(1) (0)D> 111+V(2) [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 15 (PA)
11720274 13875169253932 -9766856 019 (0)D> 114883425 10 11 01 10 11
== Executing PA-CTR 15, V(1)=8, V(2)=4883421, repcount=1627808, factor=8/3
31253970 98667613094764 -8 0113022473 (0)D> 11 10 11 01 10 11
31253971 98667613094766 -6 0113022474 (0)F> 10 11 01 10 11
31253972 98667613094768 -8 0113022474 <B(1) 00 11 01 10 11
31253973 98667639139716 -26044956 <B(1) 0113022474 00 11 01 10 11
31253974 98667639139720 -26044958 <C(1) 0113022475 00 11 01 10 11
31253975 98667639139726 -26044956 10 (1)E> 0113022475 00 11 01 10 11
31253976 98667665184676 -6 1013022476 (1)E> 00 11 01 10 11
31253977 98667665184680 -8 1013022476 <C(1) 01 11 01 10 11
31253978 98667691229632 -26044960 <C(1) 1113022476 01 11 01 10 11
31253979 98667691229638 -26044958 10 (1)E> 1113022476 01 11 01 10 11
31253980 98667691229642 -26044960 10 <D(0) 10 1113022475 01 11 01 10 11
31253981 98667691229644 -26044962 <D(0) 102 1113022475 01 11 01 10 11
31253982 98667691229646 -26044964 <A(0) 103 1113022475 01 11 01 10 11
31253983 98667691229650 -26044966 <A(1) 104 1113022475 01 11 01 10 11
31253984 98667691229654 -26044964 01 (0)D> 104 1113022475 01 11 01 10 11
31253985 98667691229662 -26044956 015 (0)D> 1113022475 01 11 01 10 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 012+V(1) (0)D> 11 10 [*]* [*]* [*]* [*]*
1 2 2 013+V(1) (0)F> 10 [*]* [*]* [*]* [*]*
2 4 0 013+V(1) <B(1) 00 [*]* [*]* [*]* [*]*
3 10+2*V(1) -6+-2*V(1) <B(1) 013+V(1) 00 [*]* [*]* [*]* [*]*
4 14+2*V(1) -8+-2*V(1) <C(1) 014+V(1) 00 [*]* [*]* [*]* [*]*
5 20+2*V(1) -6+-2*V(1) 10 (1)E> 014+V(1) 00 [*]* [*]* [*]* [*]*
6 28+4*V(1) 2 105+V(1) (1)E> 00 [*]* [*]* [*]* [*]*
7 32+4*V(1) 0 105+V(1) <C(1) 01 [*]* [*]* [*]* [*]*
8 42+6*V(1) -10+-2*V(1) <C(1) 115+V(1) 01 [*]* [*]* [*]* [*]*
9 48+6*V(1) -8+-2*V(1) 10 (1)E> 115+V(1) 01 [*]* [*]* [*]* [*]*
10 52+6*V(1) -10+-2*V(1) 10 <D(0) 10 114+V(1) 01 [*]* [*]* [*]* [*]*
11 54+6*V(1) -12+-2*V(1) <D(0) 102 114+V(1) 01 [*]* [*]* [*]* [*]*
12 56+6*V(1) -14+-2*V(1) <A(0) 103 114+V(1) 01 [*]* [*]* [*]* [*]*
13 60+6*V(1) -16+-2*V(1) <A(1) 104 114+V(1) 01 [*]* [*]* [*]* [*]*
14 64+6*V(1) -14+-2*V(1) 01 (0)D> 104 114+V(1) 01 [*]* [*]* [*]* [*]*
15 72+6*V(1) -6+-2*V(1) 015 (0)D> 114+V(1) 01 [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 16 (PPA)
31253985 98667691229662 -26044956 015 (0)D> 1113022475 01 11 01 10 11
== Executing PA-CTR 15, V(1)=4, V(2)=13022471, repcount=4340824, factor=8/3
83343873 701636073691278 -12 0134726597 (0)D> 113 01 11 01 10 11
83343874 701636073691280 -10 0134726598 (0)F> 112 01 11 01 10 11
83343875 701636073691282 -12 0134726598 <B(1) 01 11 01 11 01 10 11
83343876 701636143144478 -69453208 <B(1) 0134726599 11 01 11 01 10 11
83343877 701636143144482 -69453210 <C(1) 0134726600 11 01 11 01 10 11
83343878 701636143144488 -69453208 10 (1)E> 0134726600 11 01 11 01 10 11
83343879 701636212597688 -8 1034726601 (1)E> 11 01 11 01 10 11
83343880 701636212597692 -10 1034726601 <D(0) 10 01 11 01 10 11
83343881 701636282050894 -69453212 <D(0) 1034726602 01 11 01 10 11
83343882 701636282050896 -69453214 <A(0) 1034726603 01 11 01 10 11
83343883 701636282050900 -69453216 <A(1) 1034726604 01 11 01 10 11
83343884 701636282050904 -69453214 01 (0)D> 1034726604 01 11 01 10 11
83343885 701636351504112 -6 0134726605 (0)D> 01 11 01 10 11
83343886 701636351504114 -8 0134726605 <A(0) 112 01 10 11
83343887 701636351504116 -10 0134726604 <A(1) 10 112 01 10 11
83343888 701636420957324 -69453218 <A(1) 1134726604 10 112 01 10 11
83343889 701636420957328 -69453216 01 (0)D> 1134726604 10 112 01 10 11
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 011+V(1) (0)D> 113 01 111+V(2) [*]* [*]* [*]*
1 2 2 012+V(1) (0)F> 112 01 111+V(2) [*]* [*]* [*]*
2 4 0 012+V(1) <B(1) 01 11 01 111+V(2) [*]* [*]* [*]*
3 8+2*V(1) -4+-2*V(1) <B(1) 013+V(1) 11 01 111+V(2) [*]* [*]* [*]*
4 12+2*V(1) -6+-2*V(1) <C(1) 014+V(1) 11 01 111+V(2) [*]* [*]* [*]*
5 18+2*V(1) -4+-2*V(1) 10 (1)E> 014+V(1) 11 01 111+V(2) [*]* [*]* [*]*
6 26+4*V(1) 4 105+V(1) (1)E> 11 01 111+V(2) [*]* [*]* [*]*
7 30+4*V(1) 2 105+V(1) <D(0) 10 01 111+V(2) [*]* [*]* [*]*
8 40+6*V(1) -8+-2*V(1) <D(0) 106+V(1) 01 111+V(2) [*]* [*]* [*]*
9 42+6*V(1) -10+-2*V(1) <A(0) 107+V(1) 01 111+V(2) [*]* [*]* [*]*
10 46+6*V(1) -12+-2*V(1) <A(1) 108+V(1) 01 111+V(2) [*]* [*]* [*]*
11 50+6*V(1) -10+-2*V(1) 01 (0)D> 108+V(1) 01 111+V(2) [*]* [*]* [*]*
12 66+8*V(1) 6 019+V(1) (0)D> 01 111+V(2) [*]* [*]* [*]*
13 68+8*V(1) 4 019+V(1) <A(0) 112+V(2) [*]* [*]* [*]*
14 70+8*V(1) 2 018+V(1) <A(1) 10 112+V(2) [*]* [*]* [*]*
15 86+10*V(1) -14+-2*V(1) <A(1) 118+V(1) 10 112+V(2) [*]* [*]* [*]*
16 90+10*V(1) -12+-2*V(1) 01 (0)D> 118+V(1) 10 112+V(2) [*]* [*]* [*]*
<< Success! ==> defined new CTR 17 (PPA)
83343889 701636420957328 -69453216 01 (0)D> 1134726604 10 112 01 10 11
== Executing PA-CTR 15, V(1)=0, V(2)=34726600, repcount=11575534, factor=8/3
222250297 4989412410850476 -12 0192604273 (0)D> 112 10 112 01 10 11
222250298 4989412410850478 -10 0192604274 (0)F> 11 10 112 01 10 11
222250299 4989412410850480 -12 0192604274 <B(1) 01 10 112 01 10 11
222250300 4989412596059028 -185208560 <B(1) 0192604275 10 112 01 10 11
222250301 4989412596059032 -185208562 <C(1) 0192604276 10 112 01 10 11
222250302 4989412596059038 -185208560 10 (1)E> 0192604276 10 112 01 10 11
222250303 4989412781267590 -8 1092604277 (1)E> 10 112 01 10 11
222250304 4989412781267592 -6 1092604278 (0)F> 112 01 10 11
222250305 4989412781267594 -8 1092604278 <B(1) 01 11 01 10 11
222250306 4989412781267596 -10 1092604277 <C(1) 012 11 01 10 11
222250307 4989412966476150 -185208564 <C(1) 1192604277 012 11 01 10 11
222250308 4989412966476156 -185208562 10 (1)E> 1192604277 012 11 01 10 11
222250309 4989412966476160 -185208564 10 <D(0) 10 1192604276 012 11 01 10 11
222250310 4989412966476162 -185208566 <D(0) 102 1192604276 012 11 01 10 11
222250311 4989412966476164 -185208568 <A(0) 103 1192604276 012 11 01 10 11
222250312 4989412966476168 -185208570 <A(1) 104 1192604276 012 11 01 10 11
222250313 4989412966476172 -185208568 01 (0)D> 104 1192604276 012 11 01 10 11
222250314 4989412966476180 -185208560 015 (0)D> 1192604276 012 11 01 10 11
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 011+V(1) (0)D> 112 10 112+V(2) [*]* [*]* [*]*
1 2 2 012+V(1) (0)F> 11 10 112+V(2) [*]* [*]* [*]*
2 4 0 012+V(1) <B(1) 01 10 112+V(2) [*]* [*]* [*]*
3 8+2*V(1) -4+-2*V(1) <B(1) 013+V(1) 10 112+V(2) [*]* [*]* [*]*
4 12+2*V(1) -6+-2*V(1) <C(1) 014+V(1) 10 112+V(2) [*]* [*]* [*]*
5 18+2*V(1) -4+-2*V(1) 10 (1)E> 014+V(1) 10 112+V(2) [*]* [*]* [*]*
6 26+4*V(1) 4 105+V(1) (1)E> 10 112+V(2) [*]* [*]* [*]*
7 28+4*V(1) 6 106+V(1) (0)F> 112+V(2) [*]* [*]* [*]*
8 30+4*V(1) 4 106+V(1) <B(1) 01 111+V(2) [*]* [*]* [*]*
9 32+4*V(1) 2 105+V(1) <C(1) 012 111+V(2) [*]* [*]* [*]*
10 42+6*V(1) -8+-2*V(1) <C(1) 115+V(1) 012 111+V(2) [*]* [*]* [*]*
11 48+6*V(1) -6+-2*V(1) 10 (1)E> 115+V(1) 012 111+V(2) [*]* [*]* [*]*
12 52+6*V(1) -8+-2*V(1) 10 <D(0) 10 114+V(1) 012 111+V(2) [*]* [*]* [*]*
13 54+6*V(1) -10+-2*V(1) <D(0) 102 114+V(1) 012 111+V(2) [*]* [*]* [*]*
14 56+6*V(1) -12+-2*V(1) <A(0) 103 114+V(1) 012 111+V(2) [*]* [*]* [*]*
15 60+6*V(1) -14+-2*V(1) <A(1) 104 114+V(1) 012 111+V(2) [*]* [*]* [*]*
16 64+6*V(1) -12+-2*V(1) 01 (0)D> 104 114+V(1) 012 111+V(2) [*]* [*]* [*]*
17 72+6*V(1) -4+-2*V(1) 015 (0)D> 114+V(1) 012 111+V(2) [*]* [*]* [*]*
<< Success! ==> defined new CTR 18 (PPA)
222250314 4989412966476180 -185208560 015 (0)D> 1192604276 012 11 01 10 11
== Executing PA-CTR 15, V(1)=4, V(2)=92604272, repcount=30868091, factor=8/3
592667406 35480264347267178 -14 01246944733 (0)D> 113 012 11 01 10 11
592667407 35480264347267180 -12 01246944734 (0)F> 112 012 11 01 10 11
592667408 35480264347267182 -14 01246944734 <B(1) 01 11 012 11 01 10 11
592667409 35480264841156650 -493889482 <B(1) 01246944735 11 012 11 01 10 11
592667410 35480264841156654 -493889484 <C(1) 01246944736 11 012 11 01 10 11
592667411 35480264841156660 -493889482 10 (1)E> 01246944736 11 012 11 01 10 11
592667412 35480265335046132 -10 10246944737 (1)E> 11 012 11 01 10 11
592667413 35480265335046136 -12 10246944737 <D(0) 10 012 11 01 10 11
592667414 35480265828935610 -493889486 <D(0) 10246944738 012 11 01 10 11
592667415 35480265828935612 -493889488 <A(0) 10246944739 012 11 01 10 11
592667416 35480265828935616 -493889490 <A(1) 10246944740 012 11 01 10 11
592667417 35480265828935620 -493889488 01 (0)D> 10246944740 012 11 01 10 11
592667418 35480266322825100 -8 01246944741 (0)D> 012 11 01 10 11
592667419 35480266322825102 -10 01246944741 <A(0) 11 01 11 01 10 11
592667420 35480266322825104 -12 01246944740 <A(1) 10 11 01 11 01 10 11
592667421 35480266816714584 -493889492 <A(1) 11246944740 10 11 01 11 01 10 11
592667422 35480266816714588 -493889490 01 (0)D> 11246944740 10 11 01 11 01 10 11
592667423 35480266816714590 -493889488 012 (0)F> 11246944739 10 11 01 11 01 10 11
592667424 35480266816714592 -493889490 012 <B(1) 01 11246944738 10 11 01 11 01 10 11
592667425 35480266816714596 -493889494 <B(1) 013 11246944738 10 11 01 11 01 10 11
592667426 35480266816714600 -493889496 <C(1) 014 11246944738 10 11 01 11 01 10 11
592667427 35480266816714606 -493889494 10 (1)E> 014 11246944738 10 11 01 11 01 10 11
592667428 35480266816714614 -493889486 105 (1)E> 11246944738 10 11 01 11 01 10 11
592667429 35480266816714618 -493889488 105 <D(0) 10 11246944737 10 11 01 11 01 10 11
592667430 35480266816714628 -493889498 <D(0) 106 11246944737 10 11 01 11 01 10 11
592667431 35480266816714630 -493889500 <A(0) 107 11246944737 10 11 01 11 01 10 11
592667432 35480266816714634 -493889502 <A(1) 108 11246944737 10 11 01 11 01 10 11
592667433 35480266816714638 -493889500 01 (0)D> 108 11246944737 10 11 01 11 01 10 11
592667434 35480266816714654 -493889484 019 (0)D> 11246944737 10 11 01 11 01 10 11
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 011+V(1) (0)D> 114+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]*
1 2 2 012+V(1) (0)F> 113+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]*
2 4 0 012+V(1) <B(1) 01 112+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]*
3 8+2*V(1) -4+-2*V(1) <B(1) 013+V(1) 112+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]*
4 12+2*V(1) -6+-2*V(1) <C(1) 014+V(1) 112+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]*
5 18+2*V(1) -4+-2*V(1) 10 (1)E> 014+V(1) 112+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]*
6 26+4*V(1) 4 105+V(1) (1)E> 112+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]*
7 30+4*V(1) 2 105+V(1) <D(0) 10 111+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]*
8 40+6*V(1) -8+-2*V(1) <D(0) 106+V(1) 111+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]*
9 42+6*V(1) -10+-2*V(1) <A(0) 107+V(1) 111+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]*
10 46+6*V(1) -12+-2*V(1) <A(1) 108+V(1) 111+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]*
11 50+6*V(1) -10+-2*V(1) 01 (0)D> 108+V(1) 111+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]*
12 66+8*V(1) 6 019+V(1) (0)D> 111+V(2) [*]* [*]* [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 19 (PA)
592667434 35480266816714654 -493889484 019 (0)D> 11246944737 10 11 01 11 01 10 11
== Executing PA-CTR 19, V(1)=8, V(2)=246944733, repcount=82314912, factor=8/3
1580446378 252304106485743838 -12 01658519305 (0)D> 11 10 11 01 11 01 10 11
1580446379 252304106485743840 -10 01658519306 (0)F> 10 11 01 11 01 10 11
1580446380 252304106485743842 -12 01658519306 <B(1) 00 11 01 11 01 10 11
1580446381 252304107802782454 -1317038624 <B(1) 01658519306 00 11 01 11 01 10 11
1580446382 252304107802782458 -1317038626 <C(1) 01658519307 00 11 01 11 01 10 11
1580446383 252304107802782464 -1317038624 10 (1)E> 01658519307 00 11 01 11 01 10 11
1580446384 252304109119821078 -10 10658519308 (1)E> 00 11 01 11 01 10 11
1580446385 252304109119821082 -12 10658519308 <C(1) 01 11 01 11 01 10 11
1580446386 252304110436859698 -1317038628 <C(1) 11658519308 01 11 01 11 01 10 11
1580446387 252304110436859704 -1317038626 10 (1)E> 11658519308 01 11 01 11 01 10 11
1580446388 252304110436859708 -1317038628 10 <D(0) 10 11658519307 01 11 01 11 01 10 11
1580446389 252304110436859710 -1317038630 <D(0) 102 11658519307 01 11 01 11 01 10 11
1580446390 252304110436859712 -1317038632 <A(0) 103 11658519307 01 11 01 11 01 10 11
1580446391 252304110436859716 -1317038634 <A(1) 104 11658519307 01 11 01 11 01 10 11
1580446392 252304110436859720 -1317038632 01 (0)D> 104 11658519307 01 11 01 11 01 10 11
1580446393 252304110436859728 -1317038624 015 (0)D> 11658519307 01 11 01 11 01 10 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 012+V(1) (0)D> 11 10 [*]* [*]* [*]* [*]* [*]* [*]*
1 2 2 013+V(1) (0)F> 10 [*]* [*]* [*]* [*]* [*]* [*]*
2 4 0 013+V(1) <B(1) 00 [*]* [*]* [*]* [*]* [*]* [*]*
3 10+2*V(1) -6+-2*V(1) <B(1) 013+V(1) 00 [*]* [*]* [*]* [*]* [*]* [*]*
4 14+2*V(1) -8+-2*V(1) <C(1) 014+V(1) 00 [*]* [*]* [*]* [*]* [*]* [*]*
5 20+2*V(1) -6+-2*V(1) 10 (1)E> 014+V(1) 00 [*]* [*]* [*]* [*]* [*]* [*]*
6 28+4*V(1) 2 105+V(1) (1)E> 00 [*]* [*]* [*]* [*]* [*]* [*]*
7 32+4*V(1) 0 105+V(1) <C(1) 01 [*]* [*]* [*]* [*]* [*]* [*]*
8 42+6*V(1) -10+-2*V(1) <C(1) 115+V(1) 01 [*]* [*]* [*]* [*]* [*]* [*]*
9 48+6*V(1) -8+-2*V(1) 10 (1)E> 115+V(1) 01 [*]* [*]* [*]* [*]* [*]* [*]*
10 52+6*V(1) -10+-2*V(1) 10 <D(0) 10 114+V(1) 01 [*]* [*]* [*]* [*]* [*]* [*]*
11 54+6*V(1) -12+-2*V(1) <D(0) 102 114+V(1) 01 [*]* [*]* [*]* [*]* [*]* [*]*
12 56+6*V(1) -14+-2*V(1) <A(0) 103 114+V(1) 01 [*]* [*]* [*]* [*]* [*]* [*]*
13 60+6*V(1) -16+-2*V(1) <A(1) 104 114+V(1) 01 [*]* [*]* [*]* [*]* [*]* [*]*
14 64+6*V(1) -14+-2*V(1) 01 (0)D> 104 114+V(1) 01 [*]* [*]* [*]* [*]* [*]* [*]*
15 72+6*V(1) -6+-2*V(1) 015 (0)D> 114+V(1) 01 [*]* [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 20 (PPA)
1580446393 252304110436859728 -1317038624 015 (0)D> 11658519307 01 11 01 11 01 10 11
== Executing PA-CTR 19, V(1)=4, V(2)=658519303, repcount=219506435, factor=8/3
4214523613 1794162525129379638 -14 011756051485 (0)D> 112 01 11 01 11 01 10 11
4214523614 1794162525129379640 -12 011756051486 (0)F> 11 01 11 01 11 01 10 11
4214523615 1794162525129379642 -14 011756051486 <B(1) 012 11 01 11 01 10 11
4214523616 1794162528641482614 -3512102986 <B(1) 011756051488 11 01 11 01 10 11
4214523617 1794162528641482618 -3512102988 <C(1) 011756051489 11 01 11 01 10 11
4214523618 1794162528641482624 -3512102986 10 (1)E> 011756051489 11 01 11 01 10 11
4214523619 1794162532153585602 -8 101756051490 (1)E> 11 01 11 01 10 11
4214523620 1794162532153585606 -10 101756051490 <D(0) 10 01 11 01 10 11
4214523621 1794162535665688586 -3512102990 <D(0) 101756051491 01 11 01 10 11
4214523622 1794162535665688588 -3512102992 <A(0) 101756051492 01 11 01 10 11
4214523623 1794162535665688592 -3512102994 <A(1) 101756051493 01 11 01 10 11
4214523624 1794162535665688596 -3512102992 01 (0)D> 101756051493 01 11 01 10 11
4214523625 1794162539177791582 -6 011756051494 (0)D> 01 11 01 10 11
4214523626 1794162539177791584 -8 011756051494 <A(0) 112 01 10 11
4214523627 1794162539177791586 -10 011756051493 <A(1) 10 112 01 10 11
4214523628 1794162542689894572 -3512102996 <A(1) 111756051493 10 112 01 10 11
4214523629 1794162542689894576 -3512102994 01 (0)D> 111756051493 10 112 01 10 11
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 011+V(1) (0)D> 112 011+V(3) 11 01 111+V(2) [*]* [*]* [*]*
1 2 2 012+V(1) (0)F> 11 011+V(3) 11 01 111+V(2) [*]* [*]* [*]*
2 4 0 012+V(1) <B(1) 012+V(3) 11 01 111+V(2) [*]* [*]* [*]*
3 8+2*V(1) -4+-2*V(1) <B(1) 014+V(1)+V(3) 11 01 111+V(2) [*]* [*]* [*]*
4 12+2*V(1) -6+-2*V(1) <C(1) 015+V(1)+V(3) 11 01 111+V(2) [*]* [*]* [*]*
5 18+2*V(1) -4+-2*V(1) 10 (1)E> 015+V(1)+V(3) 11 01 111+V(2) [*]* [*]* [*]*
6 28+4*V(1)+2*V(3) 6+2*V(3) 106+V(1)+V(3) (1)E> 11 01 111+V(2) [*]* [*]* [*]*
7 32+4*V(1)+2*V(3) 4+2*V(3) 106+V(1)+V(3) <D(0) 10 01 111+V(2) [*]* [*]* [*]*
8 44+6*V(1)+4*V(3) -8+-2*V(1) <D(0) 107+V(1)+V(3) 01 111+V(2) [*]* [*]* [*]*
9 46+6*V(1)+4*V(3) -10+-2*V(1) <A(0) 108+V(1)+V(3) 01 111+V(2) [*]* [*]* [*]*
10 50+6*V(1)+4*V(3) -12+-2*V(1) <A(1) 109+V(1)+V(3) 01 111+V(2) [*]* [*]* [*]*
11 54+6*V(1)+4*V(3) -10+-2*V(1) 01 (0)D> 109+V(1)+V(3) 01 111+V(2) [*]* [*]* [*]*
12 72+8*V(1)+6*V(3) 8+2*V(3) 0110+V(1)+V(3) (0)D> 01 111+V(2) [*]* [*]* [*]*
13 74+8*V(1)+6*V(3) 6+2*V(3) 0110+V(1)+V(3) <A(0) 112+V(2) [*]* [*]* [*]*
14 76+8*V(1)+6*V(3) 4+2*V(3) 019+V(1)+V(3) <A(1) 10 112+V(2) [*]* [*]* [*]*
15 94+10*V(1)+8*V(3) -14+-2*V(1) <A(1) 119+V(1)+V(3) 10 112+V(2) [*]* [*]* [*]*
16 98+10*V(1)+8*V(3) -12+-2*V(1) 01 (0)D> 119+V(1)+V(3) 10 112+V(2) [*]* [*]* [*]*
<< Success! ==> defined new CTR 21 (PPA)
4214523629 1794162542689894576 -3512102994 01 (0)D> 111756051493 10 112 01 10 11
== Executing PA-CTR 15, V(1)=0, V(2)=1756051489, repcount=585350497, factor=8/3
11238729593 12758489101412515762 -12 014682803977 (0)D> 112 10 112 01 10 11
== Executing PPA-CTR 18 (once), V(1)=4682803976, V(2)=0
11238729610 12758489129509339690 -9365607968 015 (0)D> 114682803980 012 11 01 10 11
== Executing PA-CTR 15, V(1)=4, V(2)=4682803976, repcount=1560934659, factor=8/3
29969945518 90727033541889308176 -14 0112487477277 (0)D> 113 012 11 01 10 11
29969945519 90727033541889308178 -12 0112487477278 (0)F> 112 012 11 01 10 11
29969945520 90727033541889308180 -14 0112487477278 <B(1) 01 11 012 11 01 10 11
29969945521 90727033566864262736 -24974954570 <B(1) 0112487477279 11 012 11 01 10 11
29969945522 90727033566864262740 -24974954572 <C(1) 0112487477280 11 012 11 01 10 11
29969945523 90727033566864262746 -24974954570 10 (1)E> 0112487477280 11 012 11 01 10 11
29969945524 90727033591839217306 -10 1012487477281 (1)E> 11 012 11 01 10 11
29969945525 90727033591839217310 -12 1012487477281 <D(0) 10 012 11 01 10 11
29969945526 90727033616814171872 -24974954574 <D(0) 1012487477282 012 11 01 10 11
29969945527 90727033616814171874 -24974954576 <A(0) 1012487477283 012 11 01 10 11
29969945528 90727033616814171878 -24974954578 <A(1) 1012487477284 012 11 01 10 11
29969945529 90727033616814171882 -24974954576 01 (0)D> 1012487477284 012 11 01 10 11
29969945530 90727033641789126450 -8 0112487477285 (0)D> 012 11 01 10 11
29969945531 90727033641789126452 -10 0112487477285 <A(0) 11 01 11 01 10 11
29969945532 90727033641789126454 -12 0112487477284 <A(1) 10 11 01 11 01 10 11
29969945533 90727033666764081022 -24974954580 <A(1) 1112487477284 10 11 01 11 01 10 11
29969945534 90727033666764081026 -24974954578 01 (0)D> 1112487477284 10 11 01 11 01 10 11
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 011+V(1) (0)D> 113 012+V(2) [*]* [*]* [*]* [*]*
1 2 2 012+V(1) (0)F> 112 012+V(2) [*]* [*]* [*]* [*]*
2 4 0 012+V(1) <B(1) 01 11 012+V(2) [*]* [*]* [*]* [*]*
3 8+2*V(1) -4+-2*V(1) <B(1) 013+V(1) 11 012+V(2) [*]* [*]* [*]* [*]*
4 12+2*V(1) -6+-2*V(1) <C(1) 014+V(1) 11 012+V(2) [*]* [*]* [*]* [*]*
5 18+2*V(1) -4+-2*V(1) 10 (1)E> 014+V(1) 11 012+V(2) [*]* [*]* [*]* [*]*
6 26+4*V(1) 4 105+V(1) (1)E> 11 012+V(2) [*]* [*]* [*]* [*]*
7 30+4*V(1) 2 105+V(1) <D(0) 10 012+V(2) [*]* [*]* [*]* [*]*
8 40+6*V(1) -8+-2*V(1) <D(0) 106+V(1) 012+V(2) [*]* [*]* [*]* [*]*
9 42+6*V(1) -10+-2*V(1) <A(0) 107+V(1) 012+V(2) [*]* [*]* [*]* [*]*
10 46+6*V(1) -12+-2*V(1) <A(1) 108+V(1) 012+V(2) [*]* [*]* [*]* [*]*
11 50+6*V(1) -10+-2*V(1) 01 (0)D> 108+V(1) 012+V(2) [*]* [*]* [*]* [*]*
12 66+8*V(1) 6 019+V(1) (0)D> 012+V(2) [*]* [*]* [*]* [*]*
13 68+8*V(1) 4 019+V(1) <A(0) 11 011+V(2) [*]* [*]* [*]* [*]*
14 70+8*V(1) 2 018+V(1) <A(1) 10 11 011+V(2) [*]* [*]* [*]* [*]*
15 86+10*V(1) -14+-2*V(1) <A(1) 118+V(1) 10 11 011+V(2) [*]* [*]* [*]* [*]*
16 90+10*V(1) -12+-2*V(1) 01 (0)D> 118+V(1) 10 11 011+V(2) [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 22 (PPA)
29969945534 90727033666764081026 -24974954578 01 (0)D> 1112487477284 10 11 01 11 01 10 11
== Executing PA-CTR 19, V(1)=0, V(2)=12487477280, repcount=4162492427, factor=8/3
79919854658 645170016362924034072 -16 0133299939417 (0)D> 113 10 11 01 11 01 10 11
79919854659 645170016362924034074 -14 0133299939418 (0)F> 112 10 11 01 11 01 10 11
79919854660 645170016362924034076 -16 0133299939418 <B(1) 01 11 10 11 01 11 01 10 11
79919854661 645170016429523912912 -66599878852 <B(1) 0133299939419 11 10 11 01 11 01 10 11
79919854662 645170016429523912916 -66599878854 <C(1) 0133299939420 11 10 11 01 11 01 10 11
79919854663 645170016429523912922 -66599878852 10 (1)E> 0133299939420 11 10 11 01 11 01 10 11
79919854664 645170016496123791762 -12 1033299939421 (1)E> 11 10 11 01 11 01 10 11
79919854665 645170016496123791766 -14 1033299939421 <D(0) 102 11 01 11 01 10 11
79919854666 645170016562723670608 -66599878856 <D(0) 1033299939423 11 01 11 01 10 11
79919854667 645170016562723670610 -66599878858 <A(0) 1033299939424 11 01 11 01 10 11
79919854668 645170016562723670614 -66599878860 <A(1) 1033299939425 11 01 11 01 10 11
79919854669 645170016562723670618 -66599878858 01 (0)D> 1033299939425 11 01 11 01 10 11
79919854670 645170016629323549468 -8 0133299939426 (0)D> 11 01 11 01 10 11
79919854671 645170016629323549470 -6 0133299939427 (0)F> 01 11 01 10 11
79919854672 645170016629323549474 -8 0133299939427 <A(0) 10 11 01 10 11
79919854673 645170016629323549476 -10 0133299939426 <A(1) 102 11 01 10 11
79919854674 645170016695923428328 -66599878862 <A(1) 1133299939426 102 11 01 10 11
79919854675 645170016695923428332 -66599878860 01 (0)D> 1133299939426 102 11 01 10 11
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 011+V(1) (0)D> 113 101+V(2) 11 01 [*]* [*]* [*]* [*]*
1 2 2 012+V(1) (0)F> 112 101+V(2) 11 01 [*]* [*]* [*]* [*]*
2 4 0 012+V(1) <B(1) 01 11 101+V(2) 11 01 [*]* [*]* [*]* [*]*
3 8+2*V(1) -4+-2*V(1) <B(1) 013+V(1) 11 101+V(2) 11 01 [*]* [*]* [*]* [*]*
4 12+2*V(1) -6+-2*V(1) <C(1) 014+V(1) 11 101+V(2) 11 01 [*]* [*]* [*]* [*]*
5 18+2*V(1) -4+-2*V(1) 10 (1)E> 014+V(1) 11 101+V(2) 11 01 [*]* [*]* [*]* [*]*
6 26+4*V(1) 4 105+V(1) (1)E> 11 101+V(2) 11 01 [*]* [*]* [*]* [*]*
7 30+4*V(1) 2 105+V(1) <D(0) 102+V(2) 11 01 [*]* [*]* [*]* [*]*
8 40+6*V(1) -8+-2*V(1) <D(0) 107+V(1)+V(2) 11 01 [*]* [*]* [*]* [*]*
9 42+6*V(1) -10+-2*V(1) <A(0) 108+V(1)+V(2) 11 01 [*]* [*]* [*]* [*]*
10 46+6*V(1) -12+-2*V(1) <A(1) 109+V(1)+V(2) 11 01 [*]* [*]* [*]* [*]*
11 50+6*V(1) -10+-2*V(1) 01 (0)D> 109+V(1)+V(2) 11 01 [*]* [*]* [*]* [*]*
12 68+8*V(1)+2*V(2) 8+2*V(2) 0110+V(1)+V(2) (0)D> 11 01 [*]* [*]* [*]* [*]*
13 70+8*V(1)+2*V(2) 10+2*V(2) 0111+V(1)+V(2) (0)F> 01 [*]* [*]* [*]* [*]*
14 74+8*V(1)+2*V(2) 8+2*V(2) 0111+V(1)+V(2) <A(0) 10 [*]* [*]* [*]* [*]*
15 76+8*V(1)+2*V(2) 6+2*V(2) 0110+V(1)+V(2) <A(1) 102 [*]* [*]* [*]* [*]*
16 96+10*V(1)+4*V(2) -14+-2*V(1) <A(1) 1110+V(1)+V(2) 102 [*]* [*]* [*]* [*]*
17 100+10*V(1)+4*V(2) -12+-2*V(1) 01 (0)D> 1110+V(1)+V(2) 102 [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 23 (PPA)
79919854675 645170016695923428332 -66599878860 01 (0)D> 1133299939426 102 11 01 10 11
== Executing PA-CTR 15, V(1)=0, V(2)=33299939422, repcount=11099979808, factor=8/3
213119612371 4587875672689569681452 -12 0188799838465 (0)D> 112 102 11 01 10 11
213119612372 4587875672689569681454 -10 0188799838466 (0)F> 11 102 11 01 10 11
213119612373 4587875672689569681456 -12 0188799838466 <B(1) 01 102 11 01 10 11
213119612374 4587875672867169358388 -177599676944 <B(1) 0188799838467 102 11 01 10 11
213119612375 4587875672867169358392 -177599676946 <C(1) 0188799838468 102 11 01 10 11
213119612376 4587875672867169358398 -177599676944 10 (1)E> 0188799838468 102 11 01 10 11
213119612377 4587875673044769035334 -8 1088799838469 (1)E> 102 11 01 10 11
213119612378 4587875673044769035336 -6 1088799838470 (0)F> 10 11 01 10 11
213119612379 4587875673044769035338 -8 1088799838470 <B(1) 00 11 01 10 11
213119612380 4587875673044769035340 -10 1088799838469 <C(1) 01 00 11 01 10 11
213119612381 4587875673222368712278 -177599676948 <C(1) 1188799838469 01 00 11 01 10 11
213119612382 4587875673222368712284 -177599676946 10 (1)E> 1188799838469 01 00 11 01 10 11
213119612383 4587875673222368712288 -177599676948 10 <D(0) 10 1188799838468 01 00 11 01 10 11
213119612384 4587875673222368712290 -177599676950 <D(0) 102 1188799838468 01 00 11 01 10 11
213119612385 4587875673222368712292 -177599676952 <A(0) 103 1188799838468 01 00 11 01 10 11
213119612386 4587875673222368712296 -177599676954 <A(1) 104 1188799838468 01 00 11 01 10 11
213119612387 4587875673222368712300 -177599676952 01 (0)D> 104 1188799838468 01 00 11 01 10 11
213119612388 4587875673222368712308 -177599676944 015 (0)D> 1188799838468 01 00 11 01 10 11
213119612389 4587875673222368712310 -177599676942 016 (0)F> 1188799838467 01 00 11 01 10 11
213119612390 4587875673222368712312 -177599676944 016 <B(1) 01 1188799838466 01 00 11 01 10 11
213119612391 4587875673222368712324 -177599676956 <B(1) 017 1188799838466 01 00 11 01 10 11
213119612392 4587875673222368712328 -177599676958 <C(1) 018 1188799838466 01 00 11 01 10 11
213119612393 4587875673222368712334 -177599676956 10 (1)E> 018 1188799838466 01 00 11 01 10 11
213119612394 4587875673222368712350 -177599676940 109 (1)E> 1188799838466 01 00 11 01 10 11
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 101+V(1) (1)E> 114+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
1 4 -2 101+V(1) <D(0) 10 113+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
2 6+2*V(1) -4+-2*V(1) <D(0) 102+V(1) 113+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
3 8+2*V(1) -6+-2*V(1) <A(0) 103+V(1) 113+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
4 12+2*V(1) -8+-2*V(1) <A(1) 104+V(1) 113+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
5 16+2*V(1) -6+-2*V(1) 01 (0)D> 104+V(1) 113+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
6 24+4*V(1) 2 015+V(1) (0)D> 113+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
7 26+4*V(1) 4 016+V(1) (0)F> 112+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
8 28+4*V(1) 2 016+V(1) <B(1) 01 111+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
9 40+6*V(1) -10+-2*V(1) <B(1) 017+V(1) 111+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
10 44+6*V(1) -12+-2*V(1) <C(1) 018+V(1) 111+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
11 50+6*V(1) -10+-2*V(1) 10 (1)E> 018+V(1) 111+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
12 66+8*V(1) 6 109+V(1) (1)E> 111+V(2) [*]* [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 24 (PA)
213119612394 4587875673222368712350 -177599676940 109 (1)E> 1188799838466 01 00 11 01 10 11
== Executing PA-CTR 24, V(1)=8, V(2)=88799838462, repcount=29599946155, factor=8/3
568318966254 32624893672247940524340 -10 10236799569249 (1)E> 11 01 00 11 01 10 11
568318966255 32624893672247940524344 -12 10236799569249 <D(0) 10 01 00 11 01 10 11
568318966256 32624893672721539662842 -473599138510 <D(0) 10236799569250 01 00 11 01 10 11
568318966257 32624893672721539662844 -473599138512 <A(0) 10236799569251 01 00 11 01 10 11
568318966258 32624893672721539662848 -473599138514 <A(1) 10236799569252 01 00 11 01 10 11
568318966259 32624893672721539662852 -473599138512 01 (0)D> 10236799569252 01 00 11 01 10 11
568318966260 32624893673195138801356 -8 01236799569253 (0)D> 01 00 11 01 10 11
568318966261 32624893673195138801358 -10 01236799569253 <A(0) 11 00 11 01 10 11
568318966262 32624893673195138801360 -12 01236799569252 <A(1) 10 11 00 11 01 10 11
568318966263 32624893673668737939864 -473599138516 <A(1) 11236799569252 10 11 00 11 01 10 11
568318966264 32624893673668737939868 -473599138514 01 (0)D> 11236799569252 10 11 00 11 01 10 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 101+V(1) (1)E> 11 01 [*]* [*]* [*]* [*]* [*]*
1 4 -2 101+V(1) <D(0) 10 01 [*]* [*]* [*]* [*]* [*]*
2 6+2*V(1) -4+-2*V(1) <D(0) 102+V(1) 01 [*]* [*]* [*]* [*]* [*]*
3 8+2*V(1) -6+-2*V(1) <A(0) 103+V(1) 01 [*]* [*]* [*]* [*]* [*]*
4 12+2*V(1) -8+-2*V(1) <A(1) 104+V(1) 01 [*]* [*]* [*]* [*]* [*]*
5 16+2*V(1) -6+-2*V(1) 01 (0)D> 104+V(1) 01 [*]* [*]* [*]* [*]* [*]*
6 24+4*V(1) 2 015+V(1) (0)D> 01 [*]* [*]* [*]* [*]* [*]*
7 26+4*V(1) 0 015+V(1) <A(0) 11 [*]* [*]* [*]* [*]* [*]*
8 28+4*V(1) -2 014+V(1) <A(1) 10 11 [*]* [*]* [*]* [*]* [*]*
9 36+6*V(1) -10+-2*V(1) <A(1) 114+V(1) 10 11 [*]* [*]* [*]* [*]* [*]*
10 40+6*V(1) -8+-2*V(1) 01 (0)D> 114+V(1) 10 11 [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 25 (PPA)
568318966264 32624893673668737939868 -473599138514 01 (0)D> 11236799569252 10 11 00 11 01 10 11
== Executing PA-CTR 19, V(1)=0, V(2)=236799569248, repcount=78933189750, factor=8/3
1515517243264 231999243887856628391368 -14 01631465518001 (0)D> 112 10 11 00 11 01 10 11
1515517243265 231999243887856628391370 -12 01631465518002 (0)F> 11 10 11 00 11 01 10 11
1515517243266 231999243887856628391372 -14 01631465518002 <B(1) 01 10 11 00 11 01 10 11
1515517243267 231999243889119559427376 -1262931036018 <B(1) 01631465518003 10 11 00 11 01 10 11
1515517243268 231999243889119559427380 -1262931036020 <C(1) 01631465518004 10 11 00 11 01 10 11
1515517243269 231999243889119559427386 -1262931036018 10 (1)E> 01631465518004 10 11 00 11 01 10 11
1515517243270 231999243890382490463394 -10 10631465518005 (1)E> 10 11 00 11 01 10 11
1515517243271 231999243890382490463396 -8 10631465518006 (0)F> 11 00 11 01 10 11
1515517243272 231999243890382490463398 -10 10631465518006 <B(1) 01 00 11 01 10 11
1515517243273 231999243890382490463400 -12 10631465518005 <C(1) 012 00 11 01 10 11
1515517243274 231999243891645421499410 -1262931036022 <C(1) 11631465518005 012 00 11 01 10 11
1515517243275 231999243891645421499416 -1262931036020 10 (1)E> 11631465518005 012 00 11 01 10 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 011+V(1) (0)D> 112 10 11 [*]* [*]* [*]* [*]* [*]*
1 2 2 012+V(1) (0)F> 11 10 11 [*]* [*]* [*]* [*]* [*]*
2 4 0 012+V(1) <B(1) 01 10 11 [*]* [*]* [*]* [*]* [*]*
3 8+2*V(1) -4+-2*V(1) <B(1) 013+V(1) 10 11 [*]* [*]* [*]* [*]* [*]*
4 12+2*V(1) -6+-2*V(1) <C(1) 014+V(1) 10 11 [*]* [*]* [*]* [*]* [*]*
5 18+2*V(1) -4+-2*V(1) 10 (1)E> 014+V(1) 10 11 [*]* [*]* [*]* [*]* [*]*
6 26+4*V(1) 4 105+V(1) (1)E> 10 11 [*]* [*]* [*]* [*]* [*]*
7 28+4*V(1) 6 106+V(1) (0)F> 11 [*]* [*]* [*]* [*]* [*]*
8 30+4*V(1) 4 106+V(1) <B(1) 01 [*]* [*]* [*]* [*]* [*]*
9 32+4*V(1) 2 105+V(1) <C(1) 012 [*]* [*]* [*]* [*]* [*]*
10 42+6*V(1) -8+-2*V(1) <C(1) 115+V(1) 012 [*]* [*]* [*]* [*]* [*]*
11 48+6*V(1) -6+-2*V(1) 10 (1)E> 115+V(1) 012 [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 26 (PPA)
1515517243275 231999243891645421499416 -1262931036020 10 (1)E> 11631465518005 012 00 11 01 10 11
== Executing PA-CTR 24, V(1)=0, V(2)=631465518001, repcount=210488506001, factor=8/3
4041379315287 1649772400971858447087482 -14 101683908048009 (1)E> 112 012 00 11 01 10 11
4041379315288 1649772400971858447087486 -16 101683908048009 <D(0) 10 11 012 00 11 01 10 11
4041379315289 1649772400975226263183504 -3367816096034 <D(0) 101683908048010 11 012 00 11 01 10 11
4041379315290 1649772400975226263183506 -3367816096036 <A(0) 101683908048011 11 012 00 11 01 10 11
4041379315291 1649772400975226263183510 -3367816096038 <A(1) 101683908048012 11 012 00 11 01 10 11
4041379315292 1649772400975226263183514 -3367816096036 01 (0)D> 101683908048012 11 012 00 11 01 10 11
4041379315293 1649772400978594079279538 -12 011683908048013 (0)D> 11 012 00 11 01 10 11
4041379315294 1649772400978594079279540 -10 011683908048014 (0)F> 012 00 11 01 10 11
4041379315295 1649772400978594079279544 -12 011683908048014 <A(0) 10 01 00 11 01 10 11
4041379315296 1649772400978594079279546 -14 011683908048013 <A(1) 102 01 00 11 01 10 11
4041379315297 1649772400981961895375572 -3367816096040 <A(1) 111683908048013 102 01 00 11 01 10 11
4041379315298 1649772400981961895375576 -3367816096038 01 (0)D> 111683908048013 102 01 00 11 01 10 11
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 101+V(1) (1)E> 112 012+V(2) [*]* [*]* [*]* [*]* [*]*
1 4 -2 101+V(1) <D(0) 10 11 012+V(2) [*]* [*]* [*]* [*]* [*]*
2 6+2*V(1) -4+-2*V(1) <D(0) 102+V(1) 11 012+V(2) [*]* [*]* [*]* [*]* [*]*
3 8+2*V(1) -6+-2*V(1) <A(0) 103+V(1) 11 012+V(2) [*]* [*]* [*]* [*]* [*]*
4 12+2*V(1) -8+-2*V(1) <A(1) 104+V(1) 11 012+V(2) [*]* [*]* [*]* [*]* [*]*
5 16+2*V(1) -6+-2*V(1) 01 (0)D> 104+V(1) 11 012+V(2) [*]* [*]* [*]* [*]* [*]*
6 24+4*V(1) 2 015+V(1) (0)D> 11 012+V(2) [*]* [*]* [*]* [*]* [*]*
7 26+4*V(1) 4 016+V(1) (0)F> 012+V(2) [*]* [*]* [*]* [*]* [*]*
8 30+4*V(1) 2 016+V(1) <A(0) 10 011+V(2) [*]* [*]* [*]* [*]* [*]*
9 32+4*V(1) 0 015+V(1) <A(1) 102 011+V(2) [*]* [*]* [*]* [*]* [*]*
10 42+6*V(1) -10+-2*V(1) <A(1) 115+V(1) 102 011+V(2) [*]* [*]* [*]* [*]* [*]*
11 46+6*V(1) -8+-2*V(1) 01 (0)D> 115+V(1) 102 011+V(2) [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 27 (PPA)
4041379315298 1649772400981961895375576 -3367816096038 01 (0)D> 111683908048013 102 01 00 11 01 10 11
== Executing PA-CTR 19, V(1)=0, V(2)=1683908048009, repcount=561302682670, factor=8/3
10777011507338 11731714851322285173111156 -18 014490421461361 (0)D> 113 102 01 00 11 01 10 11
10777011507339 11731714851322285173111158 -16 014490421461362 (0)F> 112 102 01 00 11 01 10 11
10777011507340 11731714851322285173111160 -18 014490421461362 <B(1) 01 11 102 01 00 11 01 10 11
10777011507341 11731714851331266016033884 -8980842922742 <B(1) 014490421461363 11 102 01 00 11 01 10 11
10777011507342 11731714851331266016033888 -8980842922744 <C(1) 014490421461364 11 102 01 00 11 01 10 11
10777011507343 11731714851331266016033894 -8980842922742 10 (1)E> 014490421461364 11 102 01 00 11 01 10 11
10777011507344 11731714851340246858956622 -14 104490421461365 (1)E> 11 102 01 00 11 01 10 11
10777011507345 11731714851340246858956626 -16 104490421461365 <D(0) 103 01 00 11 01 10 11
10777011507346 11731714851349227701879356 -8980842922746 <D(0) 104490421461368 01 00 11 01 10 11
10777011507347 11731714851349227701879358 -8980842922748 <A(0) 104490421461369 01 00 11 01 10 11
10777011507348 11731714851349227701879362 -8980842922750 <A(1) 104490421461370 01 00 11 01 10 11
10777011507349 11731714851349227701879366 -8980842922748 01 (0)D> 104490421461370 01 00 11 01 10 11
10777011507350 11731714851358208544802106 -8 014490421461371 (0)D> 01 00 11 01 10 11
10777011507351 11731714851358208544802108 -10 014490421461371 <A(0) 11 00 11 01 10 11
10777011507352 11731714851358208544802110 -12 014490421461370 <A(1) 10 11 00 11 01 10 11
10777011507353 11731714851367189387724850 -8980842922752 <A(1) 114490421461370 10 11 00 11 01 10 11
10777011507354 11731714851367189387724854 -8980842922750 01 (0)D> 114490421461370 10 11 00 11 01 10 11
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 011+V(1) (0)D> 113 101+V(2) 01 [*]* [*]* [*]* [*]* [*]*
1 2 2 012+V(1) (0)F> 112 101+V(2) 01 [*]* [*]* [*]* [*]* [*]*
2 4 0 012+V(1) <B(1) 01 11 101+V(2) 01 [*]* [*]* [*]* [*]* [*]*
3 8+2*V(1) -4+-2*V(1) <B(1) 013+V(1) 11 101+V(2) 01 [*]* [*]* [*]* [*]* [*]*
4 12+2*V(1) -6+-2*V(1) <C(1) 014+V(1) 11 101+V(2) 01 [*]* [*]* [*]* [*]* [*]*
5 18+2*V(1) -4+-2*V(1) 10 (1)E> 014+V(1) 11 101+V(2) 01 [*]* [*]* [*]* [*]* [*]*
6 26+4*V(1) 4 105+V(1) (1)E> 11 101+V(2) 01 [*]* [*]* [*]* [*]* [*]*
7 30+4*V(1) 2 105+V(1) <D(0) 102+V(2) 01 [*]* [*]* [*]* [*]* [*]*
8 40+6*V(1) -8+-2*V(1) <D(0) 107+V(1)+V(2) 01 [*]* [*]* [*]* [*]* [*]*
9 42+6*V(1) -10+-2*V(1) <A(0) 108+V(1)+V(2) 01 [*]* [*]* [*]* [*]* [*]*
10 46+6*V(1) -12+-2*V(1) <A(1) 109+V(1)+V(2) 01 [*]* [*]* [*]* [*]* [*]*
11 50+6*V(1) -10+-2*V(1) 01 (0)D> 109+V(1)+V(2) 01 [*]* [*]* [*]* [*]* [*]*
12 68+8*V(1)+2*V(2) 8+2*V(2) 0110+V(1)+V(2) (0)D> 01 [*]* [*]* [*]* [*]* [*]*
13 70+8*V(1)+2*V(2) 6+2*V(2) 0110+V(1)+V(2) <A(0) 11 [*]* [*]* [*]* [*]* [*]*
14 72+8*V(1)+2*V(2) 4+2*V(2) 019+V(1)+V(2) <A(1) 10 11 [*]* [*]* [*]* [*]* [*]*
15 90+10*V(1)+4*V(2) -14+-2*V(1) <A(1) 119+V(1)+V(2) 10 11 [*]* [*]* [*]* [*]* [*]*
16 94+10*V(1)+4*V(2) -12+-2*V(1) 01 (0)D> 119+V(1)+V(2) 10 11 [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 28 (PPA)
10777011507354 11731714851367189387724854 -8980842922750 01 (0)D> 114490421461370 10 11 00 11 01 10 11
== Executing PA-CTR 19, V(1)=0, V(2)=4490421461366, repcount=1496807153789, factor=8/3
28738697352822 83425527831703747936762352 -16 0111974457230313 (0)D> 113 10 11 00 11 01 10 11
28738697352823 83425527831703747936762354 -14 0111974457230314 (0)F> 112 10 11 00 11 01 10 11
28738697352824 83425527831703747936762356 -16 0111974457230314 <B(1) 01 11 10 11 00 11 01 10 11
28738697352825 83425527831727696851222984 -23948914460644 <B(1) 0111974457230315 11 10 11 00 11 01 10 11
28738697352826 83425527831727696851222988 -23948914460646 <C(1) 0111974457230316 11 10 11 00 11 01 10 11
28738697352827 83425527831727696851222994 -23948914460644 10 (1)E> 0111974457230316 11 10 11 00 11 01 10 11
28738697352828 83425527831751645765683626 -12 1011974457230317 (1)E> 11 10 11 00 11 01 10 11
28738697352829 83425527831751645765683630 -14 1011974457230317 <D(0) 102 11 00 11 01 10 11
28738697352830 83425527831775594680144264 -23948914460648 <D(0) 1011974457230319 11 00 11 01 10 11
28738697352831 83425527831775594680144266 -23948914460650 <A(0) 1011974457230320 11 00 11 01 10 11
28738697352832 83425527831775594680144270 -23948914460652 <A(1) 1011974457230321 11 00 11 01 10 11
28738697352833 83425527831775594680144274 -23948914460650 01 (0)D> 1011974457230321 11 00 11 01 10 11
28738697352834 83425527831799543594604916 -8 0111974457230322 (0)D> 11 00 11 01 10 11
28738697352835 83425527831799543594604918 -6 0111974457230323 (0)F> 00 11 01 10 11
28738697352836 83425527831799543594604920 -4 0111974457230323 00 (0)F> 11 01 10 11
28738697352837 83425527831799543594604922 -6 0111974457230323 00 <B(1) 012 10 11
28738697352838 83425527831799543594604926 -8 0111974457230323 <C(1) 013 10 11
28738697352839 83425527831799543594604927 -7 0111974457230322 01 Z> 1 013 10 11 [stop]
Lines: 552
Top steps: 551
Macro steps: 28738697352839
Basic steps: 83425527831799543594604927
Tape index: -7
ones: 11974457230330
log10(ones ): 13.078
log10(steps ): 25.921
Run state: stop
Input to awk program:
gohalt 1
L 38
5T B1R C1L A0L D0L A1L Z1R B1L E1R D0R F0R F0R D0L : 11974457230330 83425527831799543594604927
T 6-state TM #g from MaBu-List
M 600
pref sim
machv mbL6_g just simple
machv mbL6_g-r with repetitions reduced
machv mbL6_g-1 with tape symbol exponents
machv mbL6_g-m as 1-bck-2-macro machine
machv mbL6_g-a as 1-bck-2-macro machine with pure additive config-TRs
iam mbL6_g-a
mtype 1 0 2
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:10:51 CEST 2010
edate Tue Jul 6 22:10:54 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:10:51 CEST 2010