Comment: This TM produces 5234513991 ones in 93943325529148987897 steps.
| State | on 0 |
on 1 |
on 0 | on 1 | ||||
|---|---|---|---|---|---|---|---|---|
| Move | Goto | Move | Goto | |||||
| A | B1R | B0L | 1 | right | B | 0 | left | B |
| B | A1L | C1L | 1 | left | A | 1 | left | C |
| C | B1L | D0R | 1 | left | B | 0 | right | D |
| D | Z1R | E1R | 1 | right | Z | 1 | right | E |
| E | F1R | A0R | 1 | right | F | 0 | right | A |
| F | C0R | C1L | 0 | right | C | 1 | left | C |
The same TM just simple.
The same TM with repetitions reduced.
The same TM with tape symbol exponents.
The same TM as 2-bck-bck-macro machine.
Simulation is done as 2-bck-bck-macro machine with pure additive config-TRs.
Pushing initial machine.
Pushing macro factor 2.
Pushing BCK machine.
Pushing BCK machine.
Steps BasSteps BasTpos Tape contents
0 0 0 (00)(00)A>
1 12 2 (01)(01)E>
2 14 4 01 (01)(10)C>
3 19 -1 01 <B(11)(01) 10
4 21 -3 <B(11)(11) 01 10
5 31 -5 <A(10)(10) 11 01 10
6 40 0 (10)(11)F> 11 01 10
7 44 2 10 (10)(10)A> 01 10
8 48 4 102 (10)(01)E> 10
9 50 6 103 (01)(01)B>
10 55 1 103 <A(10)(10) 10
11 64 6 103 (10)(11)F> 10
12 68 8 104 (10)(11)F>
13 75 3 104 <C(11)(10) 11
14 77 1 103 <C(11)(11) 10 11
15 83 -5 <C(11)(11) 113 10 11
16 85 -7 <A(11)(11) 114 10 11
17 106 -2 01 (01)(01)E> 114 10 11
18 113 -7 01 <A(10)(10) 10 113 10 11
19 115 -9 <A(10)(10) 102 113 10 11
20 124 -4 (10)(11)F> 102 113 10 11
21 132 0 102 (10)(11)F> 113 10 11
22 136 2 103 (10)(10)A> 112 10 11
23 141 -3 103 <B(01)(01) 01 11 10 11
24 147 -9 <B(01)(01) 014 11 10 11
25 160 -4 01 (01)(01)E> 014 11 10 11
26 176 4 015 (01)(01)E> 11 10 11
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 011+V(1) (01)(01)E> 114+V(2) [*]* [*]*
1 7 -5 011+V(1) <A(10)(10) 10 113+V(2) [*]* [*]*
2 9+2*V(1) -7+-2*V(1) <A(10)(10) 102+V(1) 113+V(2) [*]* [*]*
3 18+2*V(1) -2+-2*V(1) (10)(11)F> 102+V(1) 113+V(2) [*]* [*]*
4 26+6*V(1) 2 102+V(1) (10)(11)F> 113+V(2) [*]* [*]*
5 30+6*V(1) 4 103+V(1) (10)(10)A> 112+V(2) [*]* [*]*
6 35+6*V(1) -1 103+V(1) <B(01)(01) 01 111+V(2) [*]* [*]*
7 41+8*V(1) -7+-2*V(1) <B(01)(01) 014+V(1) 111+V(2) [*]* [*]*
8 54+8*V(1) -2+-2*V(1) 01 (01)(01)E> 014+V(1) 111+V(2) [*]* [*]*
9 70+12*V(1) 6 015+V(1) (01)(01)E> 111+V(2) [*]* [*]*
<< Success! ==> defined new CTR 1 (PA)
27 183 -1 015 <A(10)(10) 102 11
28 193 -11 <A(10)(10) 107 11
29 202 -6 (10)(11)F> 107 11
30 230 8 107 (10)(11)F> 11
31 234 10 108 (10)(10)A>
32 241 5 108 <B(01)(01) 01
33 257 -11 <B(01)(01) 019
34 270 -6 01 (01)(01)E> 019
35 306 12 0110 (01)(01)E>
36 308 14 0111 (01)(10)C>
37 313 9 0111 <B(11)(01) 10
38 315 7 0110 <B(11)(11) 01 10
39 335 -13 <B(11)(11) 1110 01 10
40 345 -15 <A(10)(10) 1111 01 10
41 354 -10 (10)(11)F> 1111 01 10
42 358 -8 10 (10)(10)A> 1110 01 10
43 363 -13 10 <B(01)(01) 01 119 01 10
44 365 -15 <B(01)(01) 012 119 01 10
45 378 -10 01 (01)(01)E> 012 119 01 10
46 386 -6 013 (01)(01)E> 119 01 10
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 011+V(1) (01)(01)E> 11 101+V(2) 11
1 7 -5 011+V(1) <A(10)(10) 102+V(2) 11
2 9+2*V(1) -7+-2*V(1) <A(10)(10) 103+V(1)+V(2) 11
3 18+2*V(1) -2+-2*V(1) (10)(11)F> 103+V(1)+V(2) 11
4 30+6*V(1)+4*V(2) 4+2*V(2) 103+V(1)+V(2) (10)(11)F> 11
5 34+6*V(1)+4*V(2) 6+2*V(2) 104+V(1)+V(2) (10)(10)A>
6 41+6*V(1)+4*V(2) 1+2*V(2) 104+V(1)+V(2) <B(01)(01) 01
7 49+8*V(1)+6*V(2) -7+-2*V(1) <B(01)(01) 015+V(1)+V(2)
8 62+8*V(1)+6*V(2) -2+-2*V(1) 01 (01)(01)E> 015+V(1)+V(2)
9 82+12*V(1)+10*V(2) 8+2*V(2) 016+V(1)+V(2) (01)(01)E>
10 84+12*V(1)+10*V(2) 10+2*V(2) 017+V(1)+V(2) (01)(10)C>
11 89+12*V(1)+10*V(2) 5+2*V(2) 017+V(1)+V(2) <B(11)(01) 10
12 91+12*V(1)+10*V(2) 3+2*V(2) 016+V(1)+V(2) <B(11)(11) 01 10
13 103+14*V(1)+12*V(2) -9+-2*V(1) <B(11)(11) 116+V(1)+V(2) 01 10
14 113+14*V(1)+12*V(2) -11+-2*V(1) <A(10)(10) 117+V(1)+V(2) 01 10
15 122+14*V(1)+12*V(2) -6+-2*V(1) (10)(11)F> 117+V(1)+V(2) 01 10
16 126+14*V(1)+12*V(2) -4+-2*V(1) 10 (10)(10)A> 116+V(1)+V(2) 01 10
17 131+14*V(1)+12*V(2) -9+-2*V(1) 10 <B(01)(01) 01 115+V(1)+V(2) 01 10
18 133+14*V(1)+12*V(2) -11+-2*V(1) <B(01)(01) 012 115+V(1)+V(2) 01 10
19 146+14*V(1)+12*V(2) -6+-2*V(1) 01 (01)(01)E> 012 115+V(1)+V(2) 01 10
20 154+14*V(1)+12*V(2) -2+-2*V(1) 013 (01)(01)E> 115+V(1)+V(2) 01 10
<< Success! ==> defined new CTR 2 (PPA)
46 386 -6 013 (01)(01)E> 119 01 10
== Executing PA-CTR 1, V(1)=2, V(2)=5, repcount=2, factor=4/3
64 622 6 0111 (01)(01)E> 113 01 10
65 629 1 0111 <A(10)(10) 10 112 01 10
66 651 -21 <A(10)(10) 1012 112 01 10
67 660 -16 (10)(11)F> 1012 112 01 10
68 708 8 1012 (10)(11)F> 112 01 10
69 712 10 1013 (10)(10)A> 11 01 10
70 717 5 1013 <B(01)(01) 012 10
71 743 -21 <B(01)(01) 0115 10
72 756 -16 01 (01)(01)E> 0115 10
73 816 14 0116 (01)(01)E> 10
74 818 16 0117 (01)(01)B>
75 823 11 0117 <A(10)(10) 10
76 857 -23 <A(10)(10) 1018
77 866 -18 (10)(11)F> 1018
78 938 18 1018 (10)(11)F>
79 945 13 1018 <C(11)(10) 11
80 947 11 1017 <C(11)(11) 10 11
81 981 -23 <C(11)(11) 1117 10 11
82 983 -25 <A(11)(11) 1118 10 11
83 1004 -20 01 (01)(01)E> 1118 10 11
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 011+V(1) (01)(01)E> 113 011+V(2) 10
1 7 -5 011+V(1) <A(10)(10) 10 112 011+V(2) 10
2 9+2*V(1) -7+-2*V(1) <A(10)(10) 102+V(1) 112 011+V(2) 10
3 18+2*V(1) -2+-2*V(1) (10)(11)F> 102+V(1) 112 011+V(2) 10
4 26+6*V(1) 2 102+V(1) (10)(11)F> 112 011+V(2) 10
5 30+6*V(1) 4 103+V(1) (10)(10)A> 11 011+V(2) 10
6 35+6*V(1) -1 103+V(1) <B(01)(01) 012+V(2) 10
7 41+8*V(1) -7+-2*V(1) <B(01)(01) 015+V(1)+V(2) 10
8 54+8*V(1) -2+-2*V(1) 01 (01)(01)E> 015+V(1)+V(2) 10
9 74+12*V(1)+4*V(2) 8+2*V(2) 016+V(1)+V(2) (01)(01)E> 10
10 76+12*V(1)+4*V(2) 10+2*V(2) 017+V(1)+V(2) (01)(01)B>
11 81+12*V(1)+4*V(2) 5+2*V(2) 017+V(1)+V(2) <A(10)(10) 10
12 95+14*V(1)+6*V(2) -9+-2*V(1) <A(10)(10) 108+V(1)+V(2)
13 104+14*V(1)+6*V(2) -4+-2*V(1) (10)(11)F> 108+V(1)+V(2)
14 136+18*V(1)+10*V(2) 12+2*V(2) 108+V(1)+V(2) (10)(11)F>
15 143+18*V(1)+10*V(2) 7+2*V(2) 108+V(1)+V(2) <C(11)(10) 11
16 145+18*V(1)+10*V(2) 5+2*V(2) 107+V(1)+V(2) <C(11)(11) 10 11
17 159+20*V(1)+12*V(2) -9+-2*V(1) <C(11)(11) 117+V(1)+V(2) 10 11
18 161+20*V(1)+12*V(2) -11+-2*V(1) <A(11)(11) 118+V(1)+V(2) 10 11
19 182+20*V(1)+12*V(2) -6+-2*V(1) 01 (01)(01)E> 118+V(1)+V(2) 10 11
<< Success! ==> defined new CTR 3 (PPA)
83 1004 -20 01 (01)(01)E> 1118 10 11
== Executing PA-CTR 1, V(1)=0, V(2)=14, repcount=5, factor=4/3
128 1834 10 0121 (01)(01)E> 113 10 11
129 1841 5 0121 <A(10)(10) 10 112 10 11
130 1883 -37 <A(10)(10) 1022 112 10 11
131 1892 -32 (10)(11)F> 1022 112 10 11
132 1980 12 1022 (10)(11)F> 112 10 11
133 1984 14 1023 (10)(10)A> 11 10 11
134 1989 9 1023 <B(01)(01) 01 10 11
135 2035 -37 <B(01)(01) 0124 10 11
136 2048 -32 01 (01)(01)E> 0124 10 11
137 2144 16 0125 (01)(01)E> 10 11
138 2146 18 0126 (01)(01)B> 11
139 2150 20 0127 (00)(10)A>
140 2168 22 0128 (01)(01)E>
141 2170 24 0129 (01)(10)C>
142 2175 19 0129 <B(11)(01) 10
143 2177 17 0128 <B(11)(11) 01 10
144 2233 -39 <B(11)(11) 1128 01 10
145 2243 -41 <A(10)(10) 1129 01 10
146 2252 -36 (10)(11)F> 1129 01 10
147 2256 -34 10 (10)(10)A> 1128 01 10
148 2261 -39 10 <B(01)(01) 01 1127 01 10
149 2263 -41 <B(01)(01) 012 1127 01 10
150 2276 -36 01 (01)(01)E> 012 1127 01 10
151 2284 -32 013 (01)(01)E> 1127 01 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 011+V(1) (01)(01)E> 113 10 11
1 7 -5 011+V(1) <A(10)(10) 10 112 10 11
2 9+2*V(1) -7+-2*V(1) <A(10)(10) 102+V(1) 112 10 11
3 18+2*V(1) -2+-2*V(1) (10)(11)F> 102+V(1) 112 10 11
4 26+6*V(1) 2 102+V(1) (10)(11)F> 112 10 11
5 30+6*V(1) 4 103+V(1) (10)(10)A> 11 10 11
6 35+6*V(1) -1 103+V(1) <B(01)(01) 01 10 11
7 41+8*V(1) -7+-2*V(1) <B(01)(01) 014+V(1) 10 11
8 54+8*V(1) -2+-2*V(1) 01 (01)(01)E> 014+V(1) 10 11
9 70+12*V(1) 6 015+V(1) (01)(01)E> 10 11
10 72+12*V(1) 8 016+V(1) (01)(01)B> 11
11 76+12*V(1) 10 017+V(1) (00)(10)A>
12 94+12*V(1) 12 018+V(1) (01)(01)E>
13 96+12*V(1) 14 019+V(1) (01)(10)C>
14 101+12*V(1) 9 019+V(1) <B(11)(01) 10
15 103+12*V(1) 7 018+V(1) <B(11)(11) 01 10
16 119+14*V(1) -9+-2*V(1) <B(11)(11) 118+V(1) 01 10
17 129+14*V(1) -11+-2*V(1) <A(10)(10) 119+V(1) 01 10
18 138+14*V(1) -6+-2*V(1) (10)(11)F> 119+V(1) 01 10
19 142+14*V(1) -4+-2*V(1) 10 (10)(10)A> 118+V(1) 01 10
20 147+14*V(1) -9+-2*V(1) 10 <B(01)(01) 01 117+V(1) 01 10
21 149+14*V(1) -11+-2*V(1) <B(01)(01) 012 117+V(1) 01 10
22 162+14*V(1) -6+-2*V(1) 01 (01)(01)E> 012 117+V(1) 01 10
23 170+14*V(1) -2+-2*V(1) 013 (01)(01)E> 117+V(1) 01 10
<< Success! ==> defined new CTR 4 (PPA)
151 2284 -32 013 (01)(01)E> 1127 01 10
== Executing PA-CTR 1, V(1)=2, V(2)=23, repcount=8, factor=4/3
223 4380 16 0135 (01)(01)E> 113 01 10
== Executing PPA-CTR 3 (once), V(1)=34, V(2)=0
242 5242 -58 01 (01)(01)E> 1142 10 11
== Executing PA-CTR 1, V(1)=0, V(2)=38, repcount=13, factor=4/3
359 9896 20 0153 (01)(01)E> 113 10 11
== Executing PPA-CTR 4 (once), V(1)=52
382 10794 -86 013 (01)(01)E> 1159 01 10
== Executing PA-CTR 1, V(1)=2, V(2)=55, repcount=19, factor=4/3
553 20788 28 0179 (01)(01)E> 112 01 10
554 20795 23 0179 <A(10)(10) 10 11 01 10
555 20953 -135 <A(10)(10) 1080 11 01 10
556 20962 -130 (10)(11)F> 1080 11 01 10
557 21282 30 1080 (10)(11)F> 11 01 10
558 21286 32 1081 (10)(10)A> 01 10
559 21290 34 1082 (10)(01)E> 10
560 21292 36 1083 (01)(01)B>
561 21297 31 1083 <A(10)(10) 10
562 21306 36 1083 (10)(11)F> 10
563 21310 38 1084 (10)(11)F>
564 21317 33 1084 <C(11)(10) 11
565 21319 31 1083 <C(11)(11) 10 11
566 21485 -135 <C(11)(11) 1183 10 11
567 21487 -137 <A(11)(11) 1184 10 11
568 21508 -132 01 (01)(01)E> 1184 10 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 011+V(1) (01)(01)E> 112 01 10
1 7 -5 011+V(1) <A(10)(10) 10 11 01 10
2 9+2*V(1) -7+-2*V(1) <A(10)(10) 102+V(1) 11 01 10
3 18+2*V(1) -2+-2*V(1) (10)(11)F> 102+V(1) 11 01 10
4 26+6*V(1) 2 102+V(1) (10)(11)F> 11 01 10
5 30+6*V(1) 4 103+V(1) (10)(10)A> 01 10
6 34+6*V(1) 6 104+V(1) (10)(01)E> 10
7 36+6*V(1) 8 105+V(1) (01)(01)B>
8 41+6*V(1) 3 105+V(1) <A(10)(10) 10
9 50+6*V(1) 8 105+V(1) (10)(11)F> 10
10 54+6*V(1) 10 106+V(1) (10)(11)F>
11 61+6*V(1) 5 106+V(1) <C(11)(10) 11
12 63+6*V(1) 3 105+V(1) <C(11)(11) 10 11
13 73+8*V(1) -7+-2*V(1) <C(11)(11) 115+V(1) 10 11
14 75+8*V(1) -9+-2*V(1) <A(11)(11) 116+V(1) 10 11
15 96+8*V(1) -4+-2*V(1) 01 (01)(01)E> 116+V(1) 10 11
<< Success! ==> defined new CTR 5 (PPA)
568 21508 -132 01 (01)(01)E> 1184 10 11
== Executing PA-CTR 1, V(1)=0, V(2)=80, repcount=27, factor=4/3
811 40246 30 01109 (01)(01)E> 113 10 11
== Executing PPA-CTR 4 (once), V(1)=108
834 41928 -188 013 (01)(01)E> 11115 01 10
== Executing PA-CTR 1, V(1)=2, V(2)=111, repcount=38, factor=4/3
1176 79244 40 01155 (01)(01)E> 11 01 10
1177 79251 35 01155 <A(10)(10) 10 01 10
1178 79561 -275 <A(10)(10) 10156 01 10
1179 79570 -270 (10)(11)F> 10156 01 10
1180 80194 42 10156 (10)(11)F> 01 10
1181 80196 44 10157 (11)(00)D> 10
1182 80198 46 10157 11 (00)(11)F>
1183 80205 41 10157 11 <A(11)(10) 11
1184 80207 39 10157 <C(10)(11) 10 11
1185 80209 37 10156 <C(11)(10) 11 10 11
1186 80211 35 10155 <C(11)(11) 10 11 10 11
1187 80521 -275 <C(11)(11) 11155 10 11 10 11
1188 80523 -277 <A(11)(11) 11156 10 11 10 11
1189 80544 -272 01 (01)(01)E> 11156 10 11 10 11
1190 80551 -277 01 <A(10)(10) 10 11155 10 11 10 11
1191 80553 -279 <A(10)(10) 102 11155 10 11 10 11
1192 80562 -274 (10)(11)F> 102 11155 10 11 10 11
1193 80570 -270 102 (10)(11)F> 11155 10 11 10 11
1194 80574 -268 103 (10)(10)A> 11154 10 11 10 11
1195 80579 -273 103 <B(01)(01) 01 11153 10 11 10 11
1196 80585 -279 <B(01)(01) 014 11153 10 11 10 11
1197 80598 -274 01 (01)(01)E> 014 11153 10 11 10 11
1198 80614 -266 015 (01)(01)E> 11153 10 11 10 11
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 011+V(1) (01)(01)E> 114+V(2) [*]* [*]* [*]* [*]*
1 7 -5 011+V(1) <A(10)(10) 10 113+V(2) [*]* [*]* [*]* [*]*
2 9+2*V(1) -7+-2*V(1) <A(10)(10) 102+V(1) 113+V(2) [*]* [*]* [*]* [*]*
3 18+2*V(1) -2+-2*V(1) (10)(11)F> 102+V(1) 113+V(2) [*]* [*]* [*]* [*]*
4 26+6*V(1) 2 102+V(1) (10)(11)F> 113+V(2) [*]* [*]* [*]* [*]*
5 30+6*V(1) 4 103+V(1) (10)(10)A> 112+V(2) [*]* [*]* [*]* [*]*
6 35+6*V(1) -1 103+V(1) <B(01)(01) 01 111+V(2) [*]* [*]* [*]* [*]*
7 41+8*V(1) -7+-2*V(1) <B(01)(01) 014+V(1) 111+V(2) [*]* [*]* [*]* [*]*
8 54+8*V(1) -2+-2*V(1) 01 (01)(01)E> 014+V(1) 111+V(2) [*]* [*]* [*]* [*]*
9 70+12*V(1) 6 015+V(1) (01)(01)E> 111+V(2) [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 6 (PA)
1198 80614 -266 015 (01)(01)E> 11153 10 11 10 11
== Executing PA-CTR 6, V(1)=4, V(2)=149, repcount=50, factor=4/3
1648 145314 34 01205 (01)(01)E> 113 10 11 10 11
1649 145321 29 01205 <A(10)(10) 10 112 10 11 10 11
1650 145731 -381 <A(10)(10) 10206 112 10 11 10 11
1651 145740 -376 (10)(11)F> 10206 112 10 11 10 11
1652 146564 36 10206 (10)(11)F> 112 10 11 10 11
1653 146568 38 10207 (10)(10)A> 11 10 11 10 11
1654 146573 33 10207 <B(01)(01) 01 10 11 10 11
1655 146987 -381 <B(01)(01) 01208 10 11 10 11
1656 147000 -376 01 (01)(01)E> 01208 10 11 10 11
1657 147832 40 01209 (01)(01)E> 10 11 10 11
1658 147834 42 01210 (01)(01)B> 11 10 11
1659 147838 44 01211 (00)(10)A> 10 11
1660 147852 46 01212 (01)(10)C> 11
1661 147854 48 01213 (10)(01)E>
1662 147856 50 01213 10 (01)(10)C>
1663 147861 45 01213 10 <B(11)(01) 10
1664 147863 43 01213 <B(01)(11) 01 10
1665 147865 41 01212 <B(11)(01) 11 01 10
1666 147867 39 01211 <B(11)(11) 01 11 01 10
1667 148289 -383 <B(11)(11) 11211 01 11 01 10
1668 148299 -385 <A(10)(10) 11212 01 11 01 10
1669 148308 -380 (10)(11)F> 11212 01 11 01 10
1670 148312 -378 10 (10)(10)A> 11211 01 11 01 10
1671 148317 -383 10 <B(01)(01) 01 11210 01 11 01 10
1672 148319 -385 <B(01)(01) 012 11210 01 11 01 10
1673 148332 -380 01 (01)(01)E> 012 11210 01 11 01 10
1674 148340 -376 013 (01)(01)E> 11210 01 11 01 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 011+V(1) (01)(01)E> 113 10 11 10 11
1 7 -5 011+V(1) <A(10)(10) 10 112 10 11 10 11
2 9+2*V(1) -7+-2*V(1) <A(10)(10) 102+V(1) 112 10 11 10 11
3 18+2*V(1) -2+-2*V(1) (10)(11)F> 102+V(1) 112 10 11 10 11
4 26+6*V(1) 2 102+V(1) (10)(11)F> 112 10 11 10 11
5 30+6*V(1) 4 103+V(1) (10)(10)A> 11 10 11 10 11
6 35+6*V(1) -1 103+V(1) <B(01)(01) 01 10 11 10 11
7 41+8*V(1) -7+-2*V(1) <B(01)(01) 014+V(1) 10 11 10 11
8 54+8*V(1) -2+-2*V(1) 01 (01)(01)E> 014+V(1) 10 11 10 11
9 70+12*V(1) 6 015+V(1) (01)(01)E> 10 11 10 11
10 72+12*V(1) 8 016+V(1) (01)(01)B> 11 10 11
11 76+12*V(1) 10 017+V(1) (00)(10)A> 10 11
12 90+12*V(1) 12 018+V(1) (01)(10)C> 11
13 92+12*V(1) 14 019+V(1) (10)(01)E>
14 94+12*V(1) 16 019+V(1) 10 (01)(10)C>
15 99+12*V(1) 11 019+V(1) 10 <B(11)(01) 10
16 101+12*V(1) 9 019+V(1) <B(01)(11) 01 10
17 103+12*V(1) 7 018+V(1) <B(11)(01) 11 01 10
18 105+12*V(1) 5 017+V(1) <B(11)(11) 01 11 01 10
19 119+14*V(1) -9+-2*V(1) <B(11)(11) 117+V(1) 01 11 01 10
20 129+14*V(1) -11+-2*V(1) <A(10)(10) 118+V(1) 01 11 01 10
21 138+14*V(1) -6+-2*V(1) (10)(11)F> 118+V(1) 01 11 01 10
22 142+14*V(1) -4+-2*V(1) 10 (10)(10)A> 117+V(1) 01 11 01 10
23 147+14*V(1) -9+-2*V(1) 10 <B(01)(01) 01 116+V(1) 01 11 01 10
24 149+14*V(1) -11+-2*V(1) <B(01)(01) 012 116+V(1) 01 11 01 10
25 162+14*V(1) -6+-2*V(1) 01 (01)(01)E> 012 116+V(1) 01 11 01 10
26 170+14*V(1) -2+-2*V(1) 013 (01)(01)E> 116+V(1) 01 11 01 10
<< Success! ==> defined new CTR 7 (PPA)
1674 148340 -376 013 (01)(01)E> 11210 01 11 01 10
== Executing PA-CTR 6, V(1)=2, V(2)=206, repcount=69, factor=4/3
2295 267434 38 01279 (01)(01)E> 113 01 11 01 10
2296 267441 33 01279 <A(10)(10) 10 112 01 11 01 10
2297 267999 -525 <A(10)(10) 10280 112 01 11 01 10
2298 268008 -520 (10)(11)F> 10280 112 01 11 01 10
2299 269128 40 10280 (10)(11)F> 112 01 11 01 10
2300 269132 42 10281 (10)(10)A> 11 01 11 01 10
2301 269137 37 10281 <B(01)(01) 012 11 01 10
2302 269699 -525 <B(01)(01) 01283 11 01 10
2303 269712 -520 01 (01)(01)E> 01283 11 01 10
2304 270844 46 01284 (01)(01)E> 11 01 10
2305 270851 41 01284 <A(10)(10) 10 01 10
2306 271419 -527 <A(10)(10) 10285 01 10
2307 271428 -522 (10)(11)F> 10285 01 10
2308 272568 48 10285 (10)(11)F> 01 10
2309 272570 50 10286 (11)(00)D> 10
2310 272572 52 10286 11 (00)(11)F>
2311 272579 47 10286 11 <A(11)(10) 11
2312 272581 45 10286 <C(10)(11) 10 11
2313 272583 43 10285 <C(11)(10) 11 10 11
2314 272585 41 10284 <C(11)(11) 10 11 10 11
2315 273153 -527 <C(11)(11) 11284 10 11 10 11
2316 273155 -529 <A(11)(11) 11285 10 11 10 11
2317 273176 -524 01 (01)(01)E> 11285 10 11 10 11
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 011+V(1) (01)(01)E> 113 011+V(2) 11 01 10
1 7 -5 011+V(1) <A(10)(10) 10 112 011+V(2) 11 01 10
2 9+2*V(1) -7+-2*V(1) <A(10)(10) 102+V(1) 112 011+V(2) 11 01 10
3 18+2*V(1) -2+-2*V(1) (10)(11)F> 102+V(1) 112 011+V(2) 11 01 10
4 26+6*V(1) 2 102+V(1) (10)(11)F> 112 011+V(2) 11 01 10
5 30+6*V(1) 4 103+V(1) (10)(10)A> 11 011+V(2) 11 01 10
6 35+6*V(1) -1 103+V(1) <B(01)(01) 012+V(2) 11 01 10
7 41+8*V(1) -7+-2*V(1) <B(01)(01) 015+V(1)+V(2) 11 01 10
8 54+8*V(1) -2+-2*V(1) 01 (01)(01)E> 015+V(1)+V(2) 11 01 10
9 74+12*V(1)+4*V(2) 8+2*V(2) 016+V(1)+V(2) (01)(01)E> 11 01 10
10 81+12*V(1)+4*V(2) 3+2*V(2) 016+V(1)+V(2) <A(10)(10) 10 01 10
11 93+14*V(1)+6*V(2) -9+-2*V(1) <A(10)(10) 107+V(1)+V(2) 01 10
12 102+14*V(1)+6*V(2) -4+-2*V(1) (10)(11)F> 107+V(1)+V(2) 01 10
13 130+18*V(1)+10*V(2) 10+2*V(2) 107+V(1)+V(2) (10)(11)F> 01 10
14 132+18*V(1)+10*V(2) 12+2*V(2) 108+V(1)+V(2) (11)(00)D> 10
15 134+18*V(1)+10*V(2) 14+2*V(2) 108+V(1)+V(2) 11 (00)(11)F>
16 141+18*V(1)+10*V(2) 9+2*V(2) 108+V(1)+V(2) 11 <A(11)(10) 11
17 143+18*V(1)+10*V(2) 7+2*V(2) 108+V(1)+V(2) <C(10)(11) 10 11
18 145+18*V(1)+10*V(2) 5+2*V(2) 107+V(1)+V(2) <C(11)(10) 11 10 11
19 147+18*V(1)+10*V(2) 3+2*V(2) 106+V(1)+V(2) <C(11)(11) 10 11 10 11
20 159+20*V(1)+12*V(2) -9+-2*V(1) <C(11)(11) 116+V(1)+V(2) 10 11 10 11
21 161+20*V(1)+12*V(2) -11+-2*V(1) <A(11)(11) 117+V(1)+V(2) 10 11 10 11
22 182+20*V(1)+12*V(2) -6+-2*V(1) 01 (01)(01)E> 117+V(1)+V(2) 10 11 10 11
<< Success! ==> defined new CTR 8 (PPA)
2317 273176 -524 01 (01)(01)E> 11285 10 11 10 11
== Executing PA-CTR 6, V(1)=0, V(2)=281, repcount=94, factor=4/3
3163 489564 40 01377 (01)(01)E> 113 10 11 10 11
== Executing PPA-CTR 7 (once), V(1)=376
3189 494998 -714 013 (01)(01)E> 11382 01 11 01 10
== Executing PA-CTR 6, V(1)=2, V(2)=378, repcount=127, factor=4/3
4332 890984 48 01511 (01)(01)E> 11 01 11 01 10
4333 890991 43 01511 <A(10)(10) 10 01 11 01 10
4334 892013 -979 <A(10)(10) 10512 01 11 01 10
4335 892022 -974 (10)(11)F> 10512 01 11 01 10
4336 894070 50 10512 (10)(11)F> 01 11 01 10
4337 894072 52 10513 (11)(00)D> 11 01 10
4338 894074 54 10513 11 (00)(10)A> 01 10
4339 894078 56 10513 11 00 (10)(01)E> 10
4340 894080 58 10513 11 00 10 (01)(01)B>
4341 894085 53 10513 11 00 10 <A(10)(10) 10
4342 894094 58 10513 11 00 10 (10)(11)F> 10
4343 894098 60 10513 11 00 102 (10)(11)F>
4344 894105 55 10513 11 00 102 <C(11)(10) 11
4345 894107 53 10513 11 00 10 <C(11)(11) 10 11
4346 894109 51 10513 11 00 <C(11)(11) 11 10 11
4347 894111 49 10513 11 <A(11)(11) 112 10 11
4348 894113 47 10513 <C(10)(11) 113 10 11
4349 894115 45 10512 <C(11)(10) 114 10 11
4350 894117 43 10511 <C(11)(11) 10 114 10 11
4351 895139 -979 <C(11)(11) 11511 10 114 10 11
4352 895141 -981 <A(11)(11) 11512 10 114 10 11
4353 895162 -976 01 (01)(01)E> 11512 10 114 10 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 013+V(1) (01)(01)E> 11 01 11 01 10
1 7 -5 013+V(1) <A(10)(10) 10 01 11 01 10
2 13+2*V(1) -11+-2*V(1) <A(10)(10) 104+V(1) 01 11 01 10
3 22+2*V(1) -6+-2*V(1) (10)(11)F> 104+V(1) 01 11 01 10
4 38+6*V(1) 2 104+V(1) (10)(11)F> 01 11 01 10
5 40+6*V(1) 4 105+V(1) (11)(00)D> 11 01 10
6 42+6*V(1) 6 105+V(1) 11 (00)(10)A> 01 10
7 46+6*V(1) 8 105+V(1) 11 00 (10)(01)E> 10
8 48+6*V(1) 10 105+V(1) 11 00 10 (01)(01)B>
9 53+6*V(1) 5 105+V(1) 11 00 10 <A(10)(10) 10
10 62+6*V(1) 10 105+V(1) 11 00 10 (10)(11)F> 10
11 66+6*V(1) 12 105+V(1) 11 00 102 (10)(11)F>
12 73+6*V(1) 7 105+V(1) 11 00 102 <C(11)(10) 11
13 75+6*V(1) 5 105+V(1) 11 00 10 <C(11)(11) 10 11
14 77+6*V(1) 3 105+V(1) 11 00 <C(11)(11) 11 10 11
15 79+6*V(1) 1 105+V(1) 11 <A(11)(11) 112 10 11
16 81+6*V(1) -1 105+V(1) <C(10)(11) 113 10 11
17 83+6*V(1) -3 104+V(1) <C(11)(10) 114 10 11
18 85+6*V(1) -5 103+V(1) <C(11)(11) 10 114 10 11
19 91+8*V(1) -11+-2*V(1) <C(11)(11) 113+V(1) 10 114 10 11
20 93+8*V(1) -13+-2*V(1) <A(11)(11) 114+V(1) 10 114 10 11
21 114+8*V(1) -8+-2*V(1) 01 (01)(01)E> 114+V(1) 10 114 10 11
<< Success! ==> defined new CTR 9 (PPA)
4353 895162 -976 01 (01)(01)E> 11512 10 114 10 11
== Executing PA-CTR 6, V(1)=0, V(2)=508, repcount=170, factor=4/3
5883 1596582 44 01681 (01)(01)E> 112 10 114 10 11
5884 1596589 39 01681 <A(10)(10) 10 11 10 114 10 11
5885 1597951 -1323 <A(10)(10) 10682 11 10 114 10 11
5886 1597960 -1318 (10)(11)F> 10682 11 10 114 10 11
5887 1600688 46 10682 (10)(11)F> 11 10 114 10 11
5888 1600692 48 10683 (10)(10)A> 10 114 10 11
5889 1600697 43 10683 <B(01)(01) 00 114 10 11
5890 1602063 -1323 <B(01)(01) 01683 00 114 10 11
5891 1602076 -1318 01 (01)(01)E> 01683 00 114 10 11
5892 1604808 48 01684 (01)(01)E> 00 114 10 11
5893 1604810 50 01685 (01)(10)C> 114 10 11
5894 1604812 52 01686 (10)(01)E> 113 10 11
5895 1604826 54 01686 10 (10)(11)F> 112 10 11
5896 1604830 56 01686 102 (10)(10)A> 11 10 11
5897 1604835 51 01686 102 <B(01)(01) 01 10 11
5898 1604839 47 01686 <B(01)(01) 013 10 11
5899 1604841 45 01685 <B(11)(01) 014 10 11
5900 1604843 43 01684 <B(11)(11) 015 10 11
5901 1606211 -1325 <B(11)(11) 11684 015 10 11
5902 1606221 -1327 <A(10)(10) 11685 015 10 11
5903 1606230 -1322 (10)(11)F> 11685 015 10 11
5904 1606234 -1320 10 (10)(10)A> 11684 015 10 11
5905 1606239 -1325 10 <B(01)(01) 01 11683 015 10 11
5906 1606241 -1327 <B(01)(01) 012 11683 015 10 11
5907 1606254 -1322 01 (01)(01)E> 012 11683 015 10 11
5908 1606262 -1318 013 (01)(01)E> 11683 015 10 11
5909 1606269 -1323 013 <A(10)(10) 10 11682 015 10 11
5910 1606275 -1329 <A(10)(10) 104 11682 015 10 11
5911 1606284 -1324 (10)(11)F> 104 11682 015 10 11
5912 1606300 -1316 104 (10)(11)F> 11682 015 10 11
5913 1606304 -1314 105 (10)(10)A> 11681 015 10 11
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 101+V(1) (10)(10)A> 114+V(2) [*]* [*]* [*]*
1 5 -5 101+V(1) <B(01)(01) 01 113+V(2) [*]* [*]* [*]*
2 7+2*V(1) -7+-2*V(1) <B(01)(01) 012+V(1) 113+V(2) [*]* [*]* [*]*
3 20+2*V(1) -2+-2*V(1) 01 (01)(01)E> 012+V(1) 113+V(2) [*]* [*]* [*]*
4 28+6*V(1) 2 013+V(1) (01)(01)E> 113+V(2) [*]* [*]* [*]*
5 35+6*V(1) -3 013+V(1) <A(10)(10) 10 112+V(2) [*]* [*]* [*]*
6 41+8*V(1) -9+-2*V(1) <A(10)(10) 104+V(1) 112+V(2) [*]* [*]* [*]*
7 50+8*V(1) -4+-2*V(1) (10)(11)F> 104+V(1) 112+V(2) [*]* [*]* [*]*
8 66+12*V(1) 4 104+V(1) (10)(11)F> 112+V(2) [*]* [*]* [*]*
9 70+12*V(1) 6 105+V(1) (10)(10)A> 111+V(2) [*]* [*]* [*]*
<< Success! ==> defined new CTR 10 (PA)
5913 1606304 -1314 105 (10)(10)A> 11681 015 10 11
== Executing PA-CTR 10, V(1)=4, V(2)=677, repcount=226, factor=4/3
7947 2853372 42 10909 (10)(10)A> 113 015 10 11
7948 2853377 37 10909 <B(01)(01) 01 112 015 10 11
7949 2855195 -1781 <B(01)(01) 01910 112 015 10 11
7950 2855208 -1776 01 (01)(01)E> 01910 112 015 10 11
7951 2858848 44 01911 (01)(01)E> 112 015 10 11
7952 2858855 39 01911 <A(10)(10) 10 11 015 10 11
7953 2860677 -1783 <A(10)(10) 10912 11 015 10 11
7954 2860686 -1778 (10)(11)F> 10912 11 015 10 11
7955 2864334 46 10912 (10)(11)F> 11 015 10 11
7956 2864338 48 10913 (10)(10)A> 015 10 11
7957 2864342 50 10914 (10)(01)E> 014 10 11
7958 2864346 52 10915 (01)(01)E> 013 10 11
7959 2864358 58 10915 013 (01)(01)E> 10 11
7960 2864360 60 10915 014 (01)(01)B> 11
7961 2864364 62 10915 015 (00)(10)A>
7962 2864382 64 10915 016 (01)(01)E>
7963 2864384 66 10915 017 (01)(10)C>
7964 2864389 61 10915 017 <B(11)(01) 10
7965 2864391 59 10915 016 <B(11)(11) 01 10
7966 2864403 47 10915 <B(11)(11) 116 01 10
7967 2864405 45 10914 <B(01)(11) 117 01 10
7968 2864407 43 10913 <B(01)(01) 118 01 10
7969 2866233 -1783 <B(01)(01) 01913 118 01 10
7970 2866246 -1778 01 (01)(01)E> 01913 118 01 10
7971 2869898 48 01914 (01)(01)E> 118 01 10
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 101+V(1) (10)(10)A> 113 013+V(2) 10 11
1 5 -5 101+V(1) <B(01)(01) 01 112 013+V(2) 10 11
2 7+2*V(1) -7+-2*V(1) <B(01)(01) 012+V(1) 112 013+V(2) 10 11
3 20+2*V(1) -2+-2*V(1) 01 (01)(01)E> 012+V(1) 112 013+V(2) 10 11
4 28+6*V(1) 2 013+V(1) (01)(01)E> 112 013+V(2) 10 11
5 35+6*V(1) -3 013+V(1) <A(10)(10) 10 11 013+V(2) 10 11
6 41+8*V(1) -9+-2*V(1) <A(10)(10) 104+V(1) 11 013+V(2) 10 11
7 50+8*V(1) -4+-2*V(1) (10)(11)F> 104+V(1) 11 013+V(2) 10 11
8 66+12*V(1) 4 104+V(1) (10)(11)F> 11 013+V(2) 10 11
9 70+12*V(1) 6 105+V(1) (10)(10)A> 013+V(2) 10 11
10 74+12*V(1) 8 106+V(1) (10)(01)E> 012+V(2) 10 11
11 78+12*V(1) 10 107+V(1) (01)(01)E> 011+V(2) 10 11
12 82+12*V(1)+4*V(2) 12+2*V(2) 107+V(1) 011+V(2) (01)(01)E> 10 11
13 84+12*V(1)+4*V(2) 14+2*V(2) 107+V(1) 012+V(2) (01)(01)B> 11
14 88+12*V(1)+4*V(2) 16+2*V(2) 107+V(1) 013+V(2) (00)(10)A>
15 106+12*V(1)+4*V(2) 18+2*V(2) 107+V(1) 014+V(2) (01)(01)E>
16 108+12*V(1)+4*V(2) 20+2*V(2) 107+V(1) 015+V(2) (01)(10)C>
17 113+12*V(1)+4*V(2) 15+2*V(2) 107+V(1) 015+V(2) <B(11)(01) 10
18 115+12*V(1)+4*V(2) 13+2*V(2) 107+V(1) 014+V(2) <B(11)(11) 01 10
19 123+12*V(1)+6*V(2) 5 107+V(1) <B(11)(11) 114+V(2) 01 10
20 125+12*V(1)+6*V(2) 3 106+V(1) <B(01)(11) 115+V(2) 01 10
21 127+12*V(1)+6*V(2) 1 105+V(1) <B(01)(01) 116+V(2) 01 10
22 137+14*V(1)+6*V(2) -9+-2*V(1) <B(01)(01) 015+V(1) 116+V(2) 01 10
23 150+14*V(1)+6*V(2) -4+-2*V(1) 01 (01)(01)E> 015+V(1) 116+V(2) 01 10
24 170+18*V(1)+6*V(2) 6 016+V(1) (01)(01)E> 116+V(2) 01 10
<< Success! ==> defined new CTR 11 (PPA)
7971 2869898 48 01914 (01)(01)E> 118 01 10
== Executing PA-CTR 1, V(1)=913, V(2)=4, repcount=2, factor=4/3
7989 2891998 60 01922 (01)(01)E> 112 01 10
== Executing PPA-CTR 5 (once), V(1)=921
8004 2899462 -1786 01 (01)(01)E> 11927 10 11
== Executing PA-CTR 1, V(1)=0, V(2)=923, repcount=308, factor=4/3
10776 5190366 62 011233 (01)(01)E> 113 10 11
== Executing PPA-CTR 4 (once), V(1)=1232
10799 5207784 -2404 013 (01)(01)E> 111239 01 10
== Executing PA-CTR 1, V(1)=2, V(2)=1235, repcount=412, factor=4/3
14507 9310480 68 011651 (01)(01)E> 113 01 10
== Executing PPA-CTR 3 (once), V(1)=1650, V(2)=0
14526 9343662 -3238 01 (01)(01)E> 111658 10 11
== Executing PA-CTR 1, V(1)=0, V(2)=1654, repcount=552, factor=4/3
19494 16681950 74 012209 (01)(01)E> 112 10 11
19495 16681957 69 012209 <A(10)(10) 10 11 10 11
19496 16686375 -4349 <A(10)(10) 102210 11 10 11
19497 16686384 -4344 (10)(11)F> 102210 11 10 11
19498 16695224 76 102210 (10)(11)F> 11 10 11
19499 16695228 78 102211 (10)(10)A> 10 11
19500 16695233 73 102211 <B(01)(01) 00 11
19501 16699655 -4349 <B(01)(01) 012211 00 11
19502 16699668 -4344 01 (01)(01)E> 012211 00 11
19503 16708512 78 012212 (01)(01)E> 00 11
19504 16708514 80 012213 (01)(10)C> 11
19505 16708516 82 012214 (10)(01)E>
19506 16708518 84 012214 10 (01)(10)C>
19507 16708523 79 012214 10 <B(11)(01) 10
19508 16708525 77 012214 <B(01)(11) 01 10
19509 16708527 75 012213 <B(11)(01) 11 01 10
19510 16708529 73 012212 <B(11)(11) 01 11 01 10
19511 16712953 -4351 <B(11)(11) 112212 01 11 01 10
19512 16712963 -4353 <A(10)(10) 112213 01 11 01 10
19513 16712972 -4348 (10)(11)F> 112213 01 11 01 10
19514 16712976 -4346 10 (10)(10)A> 112212 01 11 01 10
19515 16712981 -4351 10 <B(01)(01) 01 112211 01 11 01 10
19516 16712983 -4353 <B(01)(01) 012 112211 01 11 01 10
19517 16712996 -4348 01 (01)(01)E> 012 112211 01 11 01 10
19518 16713004 -4344 013 (01)(01)E> 112211 01 11 01 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 012+V(1) (01)(01)E> 112 10 11
1 7 -5 012+V(1) <A(10)(10) 10 11 10 11
2 11+2*V(1) -9+-2*V(1) <A(10)(10) 103+V(1) 11 10 11
3 20+2*V(1) -4+-2*V(1) (10)(11)F> 103+V(1) 11 10 11
4 32+6*V(1) 2 103+V(1) (10)(11)F> 11 10 11
5 36+6*V(1) 4 104+V(1) (10)(10)A> 10 11
6 41+6*V(1) -1 104+V(1) <B(01)(01) 00 11
7 49+8*V(1) -9+-2*V(1) <B(01)(01) 014+V(1) 00 11
8 62+8*V(1) -4+-2*V(1) 01 (01)(01)E> 014+V(1) 00 11
9 78+12*V(1) 4 015+V(1) (01)(01)E> 00 11
10 80+12*V(1) 6 016+V(1) (01)(10)C> 11
11 82+12*V(1) 8 017+V(1) (10)(01)E>
12 84+12*V(1) 10 017+V(1) 10 (01)(10)C>
13 89+12*V(1) 5 017+V(1) 10 <B(11)(01) 10
14 91+12*V(1) 3 017+V(1) <B(01)(11) 01 10
15 93+12*V(1) 1 016+V(1) <B(11)(01) 11 01 10
16 95+12*V(1) -1 015+V(1) <B(11)(11) 01 11 01 10
17 105+14*V(1) -11+-2*V(1) <B(11)(11) 115+V(1) 01 11 01 10
18 115+14*V(1) -13+-2*V(1) <A(10)(10) 116+V(1) 01 11 01 10
19 124+14*V(1) -8+-2*V(1) (10)(11)F> 116+V(1) 01 11 01 10
20 128+14*V(1) -6+-2*V(1) 10 (10)(10)A> 115+V(1) 01 11 01 10
21 133+14*V(1) -11+-2*V(1) 10 <B(01)(01) 01 114+V(1) 01 11 01 10
22 135+14*V(1) -13+-2*V(1) <B(01)(01) 012 114+V(1) 01 11 01 10
23 148+14*V(1) -8+-2*V(1) 01 (01)(01)E> 012 114+V(1) 01 11 01 10
24 156+14*V(1) -4+-2*V(1) 013 (01)(01)E> 114+V(1) 01 11 01 10
<< Success! ==> defined new CTR 12 (PPA)
19518 16713004 -4344 013 (01)(01)E> 112211 01 11 01 10
== Executing PA-CTR 6, V(1)=2, V(2)=2207, repcount=736, factor=4/3
26142 29765228 72 012947 (01)(01)E> 113 01 11 01 10
== Executing PPA-CTR 8 (once), V(1)=2946, V(2)=0
26164 29824330 -5826 01 (01)(01)E> 112953 10 11 10 11
== Executing PA-CTR 6, V(1)=0, V(2)=2949, repcount=984, factor=4/3
35020 53107738 78 013937 (01)(01)E> 11 10 11 10 11
35021 53107745 73 013937 <A(10)(10) 102 11 10 11
35022 53115619 -7801 <A(10)(10) 103939 11 10 11
35023 53115628 -7796 (10)(11)F> 103939 11 10 11
35024 53131384 82 103939 (10)(11)F> 11 10 11
35025 53131388 84 103940 (10)(10)A> 10 11
35026 53131393 79 103940 <B(01)(01) 00 11
35027 53139273 -7801 <B(01)(01) 013940 00 11
35028 53139286 -7796 01 (01)(01)E> 013940 00 11
35029 53155046 84 013941 (01)(01)E> 00 11
35030 53155048 86 013942 (01)(10)C> 11
35031 53155050 88 013943 (10)(01)E>
35032 53155052 90 013943 10 (01)(10)C>
35033 53155057 85 013943 10 <B(11)(01) 10
35034 53155059 83 013943 <B(01)(11) 01 10
35035 53155061 81 013942 <B(11)(01) 11 01 10
35036 53155063 79 013941 <B(11)(11) 01 11 01 10
35037 53162945 -7803 <B(11)(11) 113941 01 11 01 10
35038 53162955 -7805 <A(10)(10) 113942 01 11 01 10
35039 53162964 -7800 (10)(11)F> 113942 01 11 01 10
35040 53162968 -7798 10 (10)(10)A> 113941 01 11 01 10
35041 53162973 -7803 10 <B(01)(01) 01 113940 01 11 01 10
35042 53162975 -7805 <B(01)(01) 012 113940 01 11 01 10
35043 53162988 -7800 01 (01)(01)E> 012 113940 01 11 01 10
35044 53162996 -7796 013 (01)(01)E> 113940 01 11 01 10
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 011+V(1) (01)(01)E> 11 101+V(2) 11 10 11
1 7 -5 011+V(1) <A(10)(10) 102+V(2) 11 10 11
2 9+2*V(1) -7+-2*V(1) <A(10)(10) 103+V(1)+V(2) 11 10 11
3 18+2*V(1) -2+-2*V(1) (10)(11)F> 103+V(1)+V(2) 11 10 11
4 30+6*V(1)+4*V(2) 4+2*V(2) 103+V(1)+V(2) (10)(11)F> 11 10 11
5 34+6*V(1)+4*V(2) 6+2*V(2) 104+V(1)+V(2) (10)(10)A> 10 11
6 39+6*V(1)+4*V(2) 1+2*V(2) 104+V(1)+V(2) <B(01)(01) 00 11
7 47+8*V(1)+6*V(2) -7+-2*V(1) <B(01)(01) 014+V(1)+V(2) 00 11
8 60+8*V(1)+6*V(2) -2+-2*V(1) 01 (01)(01)E> 014+V(1)+V(2) 00 11
9 76+12*V(1)+10*V(2) 6+2*V(2) 015+V(1)+V(2) (01)(01)E> 00 11
10 78+12*V(1)+10*V(2) 8+2*V(2) 016+V(1)+V(2) (01)(10)C> 11
11 80+12*V(1)+10*V(2) 10+2*V(2) 017+V(1)+V(2) (10)(01)E>
12 82+12*V(1)+10*V(2) 12+2*V(2) 017+V(1)+V(2) 10 (01)(10)C>
13 87+12*V(1)+10*V(2) 7+2*V(2) 017+V(1)+V(2) 10 <B(11)(01) 10
14 89+12*V(1)+10*V(2) 5+2*V(2) 017+V(1)+V(2) <B(01)(11) 01 10
15 91+12*V(1)+10*V(2) 3+2*V(2) 016+V(1)+V(2) <B(11)(01) 11 01 10
16 93+12*V(1)+10*V(2) 1+2*V(2) 015+V(1)+V(2) <B(11)(11) 01 11 01 10
17 103+14*V(1)+12*V(2) -9+-2*V(1) <B(11)(11) 115+V(1)+V(2) 01 11 01 10
18 113+14*V(1)+12*V(2) -11+-2*V(1) <A(10)(10) 116+V(1)+V(2) 01 11 01 10
19 122+14*V(1)+12*V(2) -6+-2*V(1) (10)(11)F> 116+V(1)+V(2) 01 11 01 10
20 126+14*V(1)+12*V(2) -4+-2*V(1) 10 (10)(10)A> 115+V(1)+V(2) 01 11 01 10
21 131+14*V(1)+12*V(2) -9+-2*V(1) 10 <B(01)(01) 01 114+V(1)+V(2) 01 11 01 10
22 133+14*V(1)+12*V(2) -11+-2*V(1) <B(01)(01) 012 114+V(1)+V(2) 01 11 01 10
23 146+14*V(1)+12*V(2) -6+-2*V(1) 01 (01)(01)E> 012 114+V(1)+V(2) 01 11 01 10
24 154+14*V(1)+12*V(2) -2+-2*V(1) 013 (01)(01)E> 114+V(1)+V(2) 01 11 01 10
<< Success! ==> defined new CTR 13 (PPA)
35044 53162996 -7796 013 (01)(01)E> 113940 01 11 01 10
== Executing PA-CTR 6, V(1)=2, V(2)=3936, repcount=1313, factor=4/3
46861 94630162 82 015255 (01)(01)E> 11 01 11 01 10
== Executing PPA-CTR 9 (once), V(1)=5252
46882 94672292 -10430 01 (01)(01)E> 115256 10 114 10 11
== Executing PA-CTR 6, V(1)=0, V(2)=5252, repcount=1751, factor=4/3
62641 168336862 76 017005 (01)(01)E> 113 10 114 10 11
62642 168336869 71 017005 <A(10)(10) 10 112 10 114 10 11
62643 168350879 -13939 <A(10)(10) 107006 112 10 114 10 11
62644 168350888 -13934 (10)(11)F> 107006 112 10 114 10 11
62645 168378912 78 107006 (10)(11)F> 112 10 114 10 11
62646 168378916 80 107007 (10)(10)A> 11 10 114 10 11
62647 168378921 75 107007 <B(01)(01) 01 10 114 10 11
62648 168392935 -13939 <B(01)(01) 017008 10 114 10 11
62649 168392948 -13934 01 (01)(01)E> 017008 10 114 10 11
62650 168420980 82 017009 (01)(01)E> 10 114 10 11
62651 168420982 84 017010 (01)(01)B> 114 10 11
62652 168420986 86 017011 (00)(10)A> 113 10 11
62653 168421002 88 017012 (01)(01)E> 112 10 11
62654 168421009 83 017012 <A(10)(10) 10 11 10 11
62655 168435033 -13941 <A(10)(10) 107013 11 10 11
62656 168435042 -13936 (10)(11)F> 107013 11 10 11
62657 168463094 90 107013 (10)(11)F> 11 10 11
62658 168463098 92 107014 (10)(10)A> 10 11
62659 168463103 87 107014 <B(01)(01) 00 11
62660 168477131 -13941 <B(01)(01) 017014 00 11
62661 168477144 -13936 01 (01)(01)E> 017014 00 11
62662 168505200 92 017015 (01)(01)E> 00 11
62663 168505202 94 017016 (01)(10)C> 11
62664 168505204 96 017017 (10)(01)E>
62665 168505206 98 017017 10 (01)(10)C>
62666 168505211 93 017017 10 <B(11)(01) 10
62667 168505213 91 017017 <B(01)(11) 01 10
62668 168505215 89 017016 <B(11)(01) 11 01 10
62669 168505217 87 017015 <B(11)(11) 01 11 01 10
62670 168519247 -13943 <B(11)(11) 117015 01 11 01 10
62671 168519257 -13945 <A(10)(10) 117016 01 11 01 10
62672 168519266 -13940 (10)(11)F> 117016 01 11 01 10
62673 168519270 -13938 10 (10)(10)A> 117015 01 11 01 10
62674 168519275 -13943 10 <B(01)(01) 01 117014 01 11 01 10
62675 168519277 -13945 <B(01)(01) 012 117014 01 11 01 10
62676 168519290 -13940 01 (01)(01)E> 012 117014 01 11 01 10
62677 168519298 -13936 013 (01)(01)E> 117014 01 11 01 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 011+V(1) (01)(01)E> 113 10 114 10 11
1 7 -5 011+V(1) <A(10)(10) 10 112 10 114 10 11
2 9+2*V(1) -7+-2*V(1) <A(10)(10) 102+V(1) 112 10 114 10 11
3 18+2*V(1) -2+-2*V(1) (10)(11)F> 102+V(1) 112 10 114 10 11
4 26+6*V(1) 2 102+V(1) (10)(11)F> 112 10 114 10 11
5 30+6*V(1) 4 103+V(1) (10)(10)A> 11 10 114 10 11
6 35+6*V(1) -1 103+V(1) <B(01)(01) 01 10 114 10 11
7 41+8*V(1) -7+-2*V(1) <B(01)(01) 014+V(1) 10 114 10 11
8 54+8*V(1) -2+-2*V(1) 01 (01)(01)E> 014+V(1) 10 114 10 11
9 70+12*V(1) 6 015+V(1) (01)(01)E> 10 114 10 11
10 72+12*V(1) 8 016+V(1) (01)(01)B> 114 10 11
11 76+12*V(1) 10 017+V(1) (00)(10)A> 113 10 11
12 92+12*V(1) 12 018+V(1) (01)(01)E> 112 10 11
13 99+12*V(1) 7 018+V(1) <A(10)(10) 10 11 10 11
14 115+14*V(1) -9+-2*V(1) <A(10)(10) 109+V(1) 11 10 11
15 124+14*V(1) -4+-2*V(1) (10)(11)F> 109+V(1) 11 10 11
16 160+18*V(1) 14 109+V(1) (10)(11)F> 11 10 11
17 164+18*V(1) 16 1010+V(1) (10)(10)A> 10 11
18 169+18*V(1) 11 1010+V(1) <B(01)(01) 00 11
19 189+20*V(1) -9+-2*V(1) <B(01)(01) 0110+V(1) 00 11
20 202+20*V(1) -4+-2*V(1) 01 (01)(01)E> 0110+V(1) 00 11
21 242+24*V(1) 16 0111+V(1) (01)(01)E> 00 11
22 244+24*V(1) 18 0112+V(1) (01)(10)C> 11
23 246+24*V(1) 20 0113+V(1) (10)(01)E>
24 248+24*V(1) 22 0113+V(1) 10 (01)(10)C>
25 253+24*V(1) 17 0113+V(1) 10 <B(11)(01) 10
26 255+24*V(1) 15 0113+V(1) <B(01)(11) 01 10
27 257+24*V(1) 13 0112+V(1) <B(11)(01) 11 01 10
28 259+24*V(1) 11 0111+V(1) <B(11)(11) 01 11 01 10
29 281+26*V(1) -11+-2*V(1) <B(11)(11) 1111+V(1) 01 11 01 10
30 291+26*V(1) -13+-2*V(1) <A(10)(10) 1112+V(1) 01 11 01 10
31 300+26*V(1) -8+-2*V(1) (10)(11)F> 1112+V(1) 01 11 01 10
32 304+26*V(1) -6+-2*V(1) 10 (10)(10)A> 1111+V(1) 01 11 01 10
33 309+26*V(1) -11+-2*V(1) 10 <B(01)(01) 01 1110+V(1) 01 11 01 10
34 311+26*V(1) -13+-2*V(1) <B(01)(01) 012 1110+V(1) 01 11 01 10
35 324+26*V(1) -8+-2*V(1) 01 (01)(01)E> 012 1110+V(1) 01 11 01 10
36 332+26*V(1) -4+-2*V(1) 013 (01)(01)E> 1110+V(1) 01 11 01 10
<< Success! ==> defined new CTR 14 (PPA)
62677 168519298 -13936 013 (01)(01)E> 117014 01 11 01 10
== Executing PA-CTR 6, V(1)=2, V(2)=7010, repcount=2337, factor=4/3
83710 299760544 86 019351 (01)(01)E> 113 01 11 01 10
== Executing PPA-CTR 8 (once), V(1)=9350, V(2)=0
83732 299947726 -18620 01 (01)(01)E> 119357 10 11 10 11
== Executing PA-CTR 6, V(1)=0, V(2)=9353, repcount=3118, factor=4/3
111794 533417330 88 0112473 (01)(01)E> 113 10 11 10 11
== Executing PPA-CTR 7 (once), V(1)=12472
111820 533592108 -24858 013 (01)(01)E> 1112478 01 11 01 10
== Executing PA-CTR 6, V(1)=2, V(2)=12474, repcount=4159, factor=4/3
149251 949017982 96 0116639 (01)(01)E> 11 01 11 01 10
== Executing PPA-CTR 9 (once), V(1)=16636
149272 949151184 -33184 01 (01)(01)E> 1116640 10 114 10 11
== Executing PA-CTR 6, V(1)=0, V(2)=16636, repcount=5546, factor=4/3
199186 1687601084 92 0122185 (01)(01)E> 112 10 114 10 11
199187 1687601091 87 0122185 <A(10)(10) 10 11 10 114 10 11
199188 1687645461 -44283 <A(10)(10) 1022186 11 10 114 10 11
199189 1687645470 -44278 (10)(11)F> 1022186 11 10 114 10 11
199190 1687734214 94 1022186 (10)(11)F> 11 10 114 10 11
199191 1687734218 96 1022187 (10)(10)A> 10 114 10 11
199192 1687734223 91 1022187 <B(01)(01) 00 114 10 11
199193 1687778597 -44283 <B(01)(01) 0122187 00 114 10 11
199194 1687778610 -44278 01 (01)(01)E> 0122187 00 114 10 11
199195 1687867358 96 0122188 (01)(01)E> 00 114 10 11
199196 1687867360 98 0122189 (01)(10)C> 114 10 11
199197 1687867362 100 0122190 (10)(01)E> 113 10 11
199198 1687867376 102 0122190 10 (10)(11)F> 112 10 11
199199 1687867380 104 0122190 102 (10)(10)A> 11 10 11
199200 1687867385 99 0122190 102 <B(01)(01) 01 10 11
199201 1687867389 95 0122190 <B(01)(01) 013 10 11
199202 1687867391 93 0122189 <B(11)(01) 014 10 11
199203 1687867393 91 0122188 <B(11)(11) 015 10 11
199204 1687911769 -44285 <B(11)(11) 1122188 015 10 11
199205 1687911779 -44287 <A(10)(10) 1122189 015 10 11
199206 1687911788 -44282 (10)(11)F> 1122189 015 10 11
199207 1687911792 -44280 10 (10)(10)A> 1122188 015 10 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 011+V(1) (01)(01)E> 112 10 114 [*]* [*]*
1 7 -5 011+V(1) <A(10)(10) 10 11 10 114 [*]* [*]*
2 9+2*V(1) -7+-2*V(1) <A(10)(10) 102+V(1) 11 10 114 [*]* [*]*
3 18+2*V(1) -2+-2*V(1) (10)(11)F> 102+V(1) 11 10 114 [*]* [*]*
4 26+6*V(1) 2 102+V(1) (10)(11)F> 11 10 114 [*]* [*]*
5 30+6*V(1) 4 103+V(1) (10)(10)A> 10 114 [*]* [*]*
6 35+6*V(1) -1 103+V(1) <B(01)(01) 00 114 [*]* [*]*
7 41+8*V(1) -7+-2*V(1) <B(01)(01) 013+V(1) 00 114 [*]* [*]*
8 54+8*V(1) -2+-2*V(1) 01 (01)(01)E> 013+V(1) 00 114 [*]* [*]*
9 66+12*V(1) 4 014+V(1) (01)(01)E> 00 114 [*]* [*]*
10 68+12*V(1) 6 015+V(1) (01)(10)C> 114 [*]* [*]*
11 70+12*V(1) 8 016+V(1) (10)(01)E> 113 [*]* [*]*
12 84+12*V(1) 10 016+V(1) 10 (10)(11)F> 112 [*]* [*]*
13 88+12*V(1) 12 016+V(1) 102 (10)(10)A> 11 [*]* [*]*
14 93+12*V(1) 7 016+V(1) 102 <B(01)(01) 01 [*]* [*]*
15 97+12*V(1) 3 016+V(1) <B(01)(01) 013 [*]* [*]*
16 99+12*V(1) 1 015+V(1) <B(11)(01) 014 [*]* [*]*
17 101+12*V(1) -1 014+V(1) <B(11)(11) 015 [*]* [*]*
18 109+14*V(1) -9+-2*V(1) <B(11)(11) 114+V(1) 015 [*]* [*]*
19 119+14*V(1) -11+-2*V(1) <A(10)(10) 115+V(1) 015 [*]* [*]*
20 128+14*V(1) -6+-2*V(1) (10)(11)F> 115+V(1) 015 [*]* [*]*
21 132+14*V(1) -4+-2*V(1) 10 (10)(10)A> 114+V(1) 015 [*]* [*]*
<< Success! ==> defined new CTR 15 (PPA)
199207 1687911792 -44280 10 (10)(10)A> 1122188 015 10 11
== Executing PA-CTR 10, V(1)=0, V(2)=22184, repcount=7395, factor=4/3
265762 3000716562 90 1029581 (10)(10)A> 113 015 10 11
== Executing PPA-CTR 11 (once), V(1)=29580, V(2)=2
265786 3001249184 96 0129586 (01)(01)E> 118 01 10
== Executing PA-CTR 1, V(1)=29585, V(2)=4, repcount=2, factor=4/3
265804 3001959412 108 0129594 (01)(01)E> 112 01 10
== Executing PPA-CTR 5 (once), V(1)=29593
265819 3002196252 -59082 01 (01)(01)E> 1129599 10 11
== Executing PA-CTR 1, V(1)=0, V(2)=29595, repcount=9866, factor=4/3
354613 5338761032 114 0139465 (01)(01)E> 11 10 11
== Executing PPA-CTR 2 (once), V(1)=39464, V(2)=0
354633 5339313682 -78816 013 (01)(01)E> 1139469 01 10
== Executing PA-CTR 1, V(1)=2, V(2)=39465, repcount=13156, factor=4/3
473037 9494162666 120 0152627 (01)(01)E> 11 01 10
473038 9494162673 115 0152627 <A(10)(10) 10 01 10
473039 9494267927 -105139 <A(10)(10) 1052628 01 10
473040 9494267936 -105134 (10)(11)F> 1052628 01 10
473041 9494478448 122 1052628 (10)(11)F> 01 10
473042 9494478450 124 1052629 (11)(00)D> 10
473043 9494478452 126 1052629 11 (00)(11)F>
473044 9494478459 121 1052629 11 <A(11)(10) 11
473045 9494478461 119 1052629 <C(10)(11) 10 11
473046 9494478463 117 1052628 <C(11)(10) 11 10 11
473047 9494478465 115 1052627 <C(11)(11) 10 11 10 11
473048 9494583719 -105139 <C(11)(11) 1152627 10 11 10 11
473049 9494583721 -105141 <A(11)(11) 1152628 10 11 10 11
473050 9494583742 -105136 01 (01)(01)E> 1152628 10 11 10 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 013+V(1) (01)(01)E> 11 01 10
1 7 -5 013+V(1) <A(10)(10) 10 01 10
2 13+2*V(1) -11+-2*V(1) <A(10)(10) 104+V(1) 01 10
3 22+2*V(1) -6+-2*V(1) (10)(11)F> 104+V(1) 01 10
4 38+6*V(1) 2 104+V(1) (10)(11)F> 01 10
5 40+6*V(1) 4 105+V(1) (11)(00)D> 10
6 42+6*V(1) 6 105+V(1) 11 (00)(11)F>
7 49+6*V(1) 1 105+V(1) 11 <A(11)(10) 11
8 51+6*V(1) -1 105+V(1) <C(10)(11) 10 11
9 53+6*V(1) -3 104+V(1) <C(11)(10) 11 10 11
10 55+6*V(1) -5 103+V(1) <C(11)(11) 10 11 10 11
11 61+8*V(1) -11+-2*V(1) <C(11)(11) 113+V(1) 10 11 10 11
12 63+8*V(1) -13+-2*V(1) <A(11)(11) 114+V(1) 10 11 10 11
13 84+8*V(1) -8+-2*V(1) 01 (01)(01)E> 114+V(1) 10 11 10 11
<< Success! ==> defined new CTR 16 (PPA)
473050 9494583742 -105136 01 (01)(01)E> 1152628 10 11 10 11
== Executing PA-CTR 6, V(1)=0, V(2)=52624, repcount=17542, factor=4/3
630928 16880713010 116 0170169 (01)(01)E> 112 10 11 10 11
630929 16880713017 111 0170169 <A(10)(10) 10 11 10 11 10 11
630930 16880853355 -140227 <A(10)(10) 1070170 11 10 11 10 11
630931 16880853364 -140222 (10)(11)F> 1070170 11 10 11 10 11
630932 16881134044 118 1070170 (10)(11)F> 11 10 11 10 11
630933 16881134048 120 1070171 (10)(10)A> 10 11 10 11
630934 16881134053 115 1070171 <B(01)(01) 00 11 10 11
630935 16881274395 -140227 <B(01)(01) 0170171 00 11 10 11
630936 16881274408 -140222 01 (01)(01)E> 0170171 00 11 10 11
630937 16881555092 120 0170172 (01)(01)E> 00 11 10 11
630938 16881555094 122 0170173 (01)(10)C> 11 10 11
630939 16881555096 124 0170174 (10)(01)E> 10 11
630940 16881555098 126 0170174 10 (01)(01)B> 11
630941 16881555102 128 0170174 10 01 (00)(10)A>
630942 16881555120 130 0170174 10 012 (01)(01)E>
630943 16881555122 132 0170174 10 013 (01)(10)C>
630944 16881555127 127 0170174 10 013 <B(11)(01) 10
630945 16881555129 125 0170174 10 012 <B(11)(11) 01 10
630946 16881555133 121 0170174 10 <B(11)(11) 112 01 10
630947 16881555135 119 0170174 <B(01)(11) 113 01 10
630948 16881555137 117 0170173 <B(11)(01) 114 01 10
630949 16881555139 115 0170172 <B(11)(11) 01 114 01 10
630950 16881695483 -140229 <B(11)(11) 1170172 01 114 01 10
630951 16881695493 -140231 <A(10)(10) 1170173 01 114 01 10
630952 16881695502 -140226 (10)(11)F> 1170173 01 114 01 10
630953 16881695506 -140224 10 (10)(10)A> 1170172 01 114 01 10
630954 16881695511 -140229 10 <B(01)(01) 01 1170171 01 114 01 10
630955 16881695513 -140231 <B(01)(01) 012 1170171 01 114 01 10
630956 16881695526 -140226 01 (01)(01)E> 012 1170171 01 114 01 10
630957 16881695534 -140222 013 (01)(01)E> 1170171 01 114 01 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 012+V(1) (01)(01)E> 112 10 11 10 11
1 7 -5 012+V(1) <A(10)(10) 10 11 10 11 10 11
2 11+2*V(1) -9+-2*V(1) <A(10)(10) 103+V(1) 11 10 11 10 11
3 20+2*V(1) -4+-2*V(1) (10)(11)F> 103+V(1) 11 10 11 10 11
4 32+6*V(1) 2 103+V(1) (10)(11)F> 11 10 11 10 11
5 36+6*V(1) 4 104+V(1) (10)(10)A> 10 11 10 11
6 41+6*V(1) -1 104+V(1) <B(01)(01) 00 11 10 11
7 49+8*V(1) -9+-2*V(1) <B(01)(01) 014+V(1) 00 11 10 11
8 62+8*V(1) -4+-2*V(1) 01 (01)(01)E> 014+V(1) 00 11 10 11
9 78+12*V(1) 4 015+V(1) (01)(01)E> 00 11 10 11
10 80+12*V(1) 6 016+V(1) (01)(10)C> 11 10 11
11 82+12*V(1) 8 017+V(1) (10)(01)E> 10 11
12 84+12*V(1) 10 017+V(1) 10 (01)(01)B> 11
13 88+12*V(1) 12 017+V(1) 10 01 (00)(10)A>
14 106+12*V(1) 14 017+V(1) 10 012 (01)(01)E>
15 108+12*V(1) 16 017+V(1) 10 013 (01)(10)C>
16 113+12*V(1) 11 017+V(1) 10 013 <B(11)(01) 10
17 115+12*V(1) 9 017+V(1) 10 012 <B(11)(11) 01 10
18 119+12*V(1) 5 017+V(1) 10 <B(11)(11) 112 01 10
19 121+12*V(1) 3 017+V(1) <B(01)(11) 113 01 10
20 123+12*V(1) 1 016+V(1) <B(11)(01) 114 01 10
21 125+12*V(1) -1 015+V(1) <B(11)(11) 01 114 01 10
22 135+14*V(1) -11+-2*V(1) <B(11)(11) 115+V(1) 01 114 01 10
23 145+14*V(1) -13+-2*V(1) <A(10)(10) 116+V(1) 01 114 01 10
24 154+14*V(1) -8+-2*V(1) (10)(11)F> 116+V(1) 01 114 01 10
25 158+14*V(1) -6+-2*V(1) 10 (10)(10)A> 115+V(1) 01 114 01 10
26 163+14*V(1) -11+-2*V(1) 10 <B(01)(01) 01 114+V(1) 01 114 01 10
27 165+14*V(1) -13+-2*V(1) <B(01)(01) 012 114+V(1) 01 114 01 10
28 178+14*V(1) -8+-2*V(1) 01 (01)(01)E> 012 114+V(1) 01 114 01 10
29 186+14*V(1) -4+-2*V(1) 013 (01)(01)E> 114+V(1) 01 114 01 10
<< Success! ==> defined new CTR 17 (PPA)
630957 16881695534 -140222 013 (01)(01)E> 1170171 01 114 01 10
== Executing PA-CTR 6, V(1)=2, V(2)=70167, repcount=23390, factor=4/3
841467 30013543234 118 0193563 (01)(01)E> 11 01 114 01 10
841468 30013543241 113 0193563 <A(10)(10) 10 01 114 01 10
841469 30013730367 -187013 <A(10)(10) 1093564 01 114 01 10
841470 30013730376 -187008 (10)(11)F> 1093564 01 114 01 10
841471 30014104632 120 1093564 (10)(11)F> 01 114 01 10
841472 30014104634 122 1093565 (11)(00)D> 114 01 10
841473 30014104636 124 1093565 11 (00)(10)A> 113 01 10
841474 30014104652 126 1093565 11 01 (01)(01)E> 112 01 10
841475 30014104659 121 1093565 11 01 <A(10)(10) 10 11 01 10
841476 30014104661 119 1093565 11 <A(10)(10) 102 11 01 10
841477 30014104663 117 1093565 <C(10)(10) 103 11 01 10
841478 30014104665 115 1093564 <C(11)(10) 104 11 01 10
841479 30014104667 113 1093563 <C(11)(11) 105 11 01 10
841480 30014291793 -187013 <C(11)(11) 1193563 105 11 01 10
841481 30014291795 -187015 <A(11)(11) 1193564 105 11 01 10
841482 30014291816 -187010 01 (01)(01)E> 1193564 105 11 01 10
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 013+V(1) (01)(01)E> 11 01 114+V(2) [*]* [*]*
1 7 -5 013+V(1) <A(10)(10) 10 01 114+V(2) [*]* [*]*
2 13+2*V(1) -11+-2*V(1) <A(10)(10) 104+V(1) 01 114+V(2) [*]* [*]*
3 22+2*V(1) -6+-2*V(1) (10)(11)F> 104+V(1) 01 114+V(2) [*]* [*]*
4 38+6*V(1) 2 104+V(1) (10)(11)F> 01 114+V(2) [*]* [*]*
5 40+6*V(1) 4 105+V(1) (11)(00)D> 114+V(2) [*]* [*]*
6 42+6*V(1) 6 105+V(1) 11 (00)(10)A> 113+V(2) [*]* [*]*
7 58+6*V(1) 8 105+V(1) 11 01 (01)(01)E> 112+V(2) [*]* [*]*
8 65+6*V(1) 3 105+V(1) 11 01 <A(10)(10) 10 111+V(2) [*]* [*]*
9 67+6*V(1) 1 105+V(1) 11 <A(10)(10) 102 111+V(2) [*]* [*]*
10 69+6*V(1) -1 105+V(1) <C(10)(10) 103 111+V(2) [*]* [*]*
11 71+6*V(1) -3 104+V(1) <C(11)(10) 104 111+V(2) [*]* [*]*
12 73+6*V(1) -5 103+V(1) <C(11)(11) 105 111+V(2) [*]* [*]*
13 79+8*V(1) -11+-2*V(1) <C(11)(11) 113+V(1) 105 111+V(2) [*]* [*]*
14 81+8*V(1) -13+-2*V(1) <A(11)(11) 114+V(1) 105 111+V(2) [*]* [*]*
15 102+8*V(1) -8+-2*V(1) 01 (01)(01)E> 114+V(1) 105 111+V(2) [*]* [*]*
<< Success! ==> defined new CTR 18 (PPA)
841482 30014291816 -187010 01 (01)(01)E> 1193564 105 11 01 10
== Executing PA-CTR 6, V(1)=0, V(2)=93560, repcount=31187, factor=4/3
1122165 53358821674 112 01124749 (01)(01)E> 113 105 11 01 10
1122166 53358821681 107 01124749 <A(10)(10) 10 112 105 11 01 10
1122167 53359071179 -249391 <A(10)(10) 10124750 112 105 11 01 10
1122168 53359071188 -249386 (10)(11)F> 10124750 112 105 11 01 10
1122169 53359570188 114 10124750 (10)(11)F> 112 105 11 01 10
1122170 53359570192 116 10124751 (10)(10)A> 11 105 11 01 10
1122171 53359570197 111 10124751 <B(01)(01) 01 105 11 01 10
1122172 53359819699 -249391 <B(01)(01) 01124752 105 11 01 10
1122173 53359819712 -249386 01 (01)(01)E> 01124752 105 11 01 10
1122174 53360318720 118 01124753 (01)(01)E> 105 11 01 10
1122175 53360318722 120 01124754 (01)(01)B> 104 11 01 10
1122176 53360318726 122 01124755 (00)(11)F> 103 11 01 10
1122177 53360318730 124 01124755 00 (10)(11)F> 102 11 01 10
1122178 53360318738 128 01124755 00 102 (10)(11)F> 11 01 10
1122179 53360318742 130 01124755 00 103 (10)(10)A> 01 10
1122180 53360318746 132 01124755 00 104 (10)(01)E> 10
1122181 53360318748 134 01124755 00 105 (01)(01)B>
1122182 53360318753 129 01124755 00 105 <A(10)(10) 10
1122183 53360318762 134 01124755 00 105 (10)(11)F> 10
1122184 53360318766 136 01124755 00 106 (10)(11)F>
1122185 53360318773 131 01124755 00 106 <C(11)(10) 11
1122186 53360318775 129 01124755 00 105 <C(11)(11) 10 11
1122187 53360318785 119 01124755 00 <C(11)(11) 115 10 11
1122188 53360318787 117 01124755 <A(11)(11) 116 10 11
1122189 53360318789 115 01124754 <A(10)(11) 117 10 11
1122190 53360318791 113 01124753 <A(10)(10) 118 10 11
1122191 53360568297 -249393 <A(10)(10) 10124753 118 10 11
1122192 53360568306 -249388 (10)(11)F> 10124753 118 10 11
1122193 53361067318 118 10124753 (10)(11)F> 118 10 11
1122194 53361067322 120 10124754 (10)(10)A> 117 10 11
1122195 53361067327 115 10124754 <B(01)(01) 01 116 10 11
1122196 53361316835 -249393 <B(01)(01) 01124755 116 10 11
1122197 53361316848 -249388 01 (01)(01)E> 01124755 116 10 11
1122198 53361815868 122 01124756 (01)(01)E> 116 10 11
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 011+V(1) (01)(01)E> 113 104+V(2) 11 01 10
1 7 -5 011+V(1) <A(10)(10) 10 112 104+V(2) 11 01 10
2 9+2*V(1) -7+-2*V(1) <A(10)(10) 102+V(1) 112 104+V(2) 11 01 10
3 18+2*V(1) -2+-2*V(1) (10)(11)F> 102+V(1) 112 104+V(2) 11 01 10
4 26+6*V(1) 2 102+V(1) (10)(11)F> 112 104+V(2) 11 01 10
5 30+6*V(1) 4 103+V(1) (10)(10)A> 11 104+V(2) 11 01 10
6 35+6*V(1) -1 103+V(1) <B(01)(01) 01 104+V(2) 11 01 10
7 41+8*V(1) -7+-2*V(1) <B(01)(01) 014+V(1) 104+V(2) 11 01 10
8 54+8*V(1) -2+-2*V(1) 01 (01)(01)E> 014+V(1) 104+V(2) 11 01 10
9 70+12*V(1) 6 015+V(1) (01)(01)E> 104+V(2) 11 01 10
10 72+12*V(1) 8 016+V(1) (01)(01)B> 103+V(2) 11 01 10
11 76+12*V(1) 10 017+V(1) (00)(11)F> 102+V(2) 11 01 10
12 80+12*V(1) 12 017+V(1) 00 (10)(11)F> 101+V(2) 11 01 10
13 84+12*V(1)+4*V(2) 14+2*V(2) 017+V(1) 00 101+V(2) (10)(11)F> 11 01 10
14 88+12*V(1)+4*V(2) 16+2*V(2) 017+V(1) 00 102+V(2) (10)(10)A> 01 10
15 92+12*V(1)+4*V(2) 18+2*V(2) 017+V(1) 00 103+V(2) (10)(01)E> 10
16 94+12*V(1)+4*V(2) 20+2*V(2) 017+V(1) 00 104+V(2) (01)(01)B>
17 99+12*V(1)+4*V(2) 15+2*V(2) 017+V(1) 00 104+V(2) <A(10)(10) 10
18 108+12*V(1)+4*V(2) 20+2*V(2) 017+V(1) 00 104+V(2) (10)(11)F> 10
19 112+12*V(1)+4*V(2) 22+2*V(2) 017+V(1) 00 105+V(2) (10)(11)F>
20 119+12*V(1)+4*V(2) 17+2*V(2) 017+V(1) 00 105+V(2) <C(11)(10) 11
21 121+12*V(1)+4*V(2) 15+2*V(2) 017+V(1) 00 104+V(2) <C(11)(11) 10 11
22 129+12*V(1)+6*V(2) 7 017+V(1) 00 <C(11)(11) 114+V(2) 10 11
23 131+12*V(1)+6*V(2) 5 017+V(1) <A(11)(11) 115+V(2) 10 11
24 133+12*V(1)+6*V(2) 3 016+V(1) <A(10)(11) 116+V(2) 10 11
25 135+12*V(1)+6*V(2) 1 015+V(1) <A(10)(10) 117+V(2) 10 11
26 145+14*V(1)+6*V(2) -9+-2*V(1) <A(10)(10) 105+V(1) 117+V(2) 10 11
27 154+14*V(1)+6*V(2) -4+-2*V(1) (10)(11)F> 105+V(1) 117+V(2) 10 11
28 174+18*V(1)+6*V(2) 6 105+V(1) (10)(11)F> 117+V(2) 10 11
29 178+18*V(1)+6*V(2) 8 106+V(1) (10)(10)A> 116+V(2) 10 11
30 183+18*V(1)+6*V(2) 3 106+V(1) <B(01)(01) 01 115+V(2) 10 11
31 195+20*V(1)+6*V(2) -9+-2*V(1) <B(01)(01) 017+V(1) 115+V(2) 10 11
32 208+20*V(1)+6*V(2) -4+-2*V(1) 01 (01)(01)E> 017+V(1) 115+V(2) 10 11
33 236+24*V(1)+6*V(2) 10 018+V(1) (01)(01)E> 115+V(2) 10 11
<< Success! ==> defined new CTR 19 (PPA)
1122198 53361815868 122 01124756 (01)(01)E> 116 10 11
== Executing PA-CTR 1, V(1)=124755, V(2)=2, repcount=1, factor=4/3
1122207 53363312998 128 01124760 (01)(01)E> 113 10 11
== Executing PPA-CTR 4 (once), V(1)=124759
1122230 53365059794 -249392 013 (01)(01)E> 11124766 01 10
== Executing PA-CTR 1, V(1)=2, V(2)=124762, repcount=41588, factor=4/3
1496522 94877452810 136 01166355 (01)(01)E> 112 01 10
== Executing PPA-CTR 5 (once), V(1)=166354
1496537 94878783738 -332576 01 (01)(01)E> 11166360 10 11
== Executing PA-CTR 1, V(1)=0, V(2)=166356, repcount=55453, factor=4/3
1995614 168682179592 142 01221813 (01)(01)E> 11 10 11
== Executing PPA-CTR 2 (once), V(1)=221812, V(2)=0
1995634 168685285114 -443484 013 (01)(01)E> 11221817 01 10
== Executing PA-CTR 1, V(1)=2, V(2)=221813, repcount=73938, factor=4/3
2661076 299894329030 144 01295755 (01)(01)E> 113 01 10
== Executing PPA-CTR 3 (once), V(1)=295754, V(2)=0
2661095 299900244292 -591370 01 (01)(01)E> 11295762 10 11
== Executing PA-CTR 1, V(1)=0, V(2)=295758, repcount=98587, factor=4/3
3548378 533170296950 152 01394349 (01)(01)E> 11 10 11
== Executing PPA-CTR 2 (once), V(1)=394348, V(2)=0
3548398 533175817976 -788546 013 (01)(01)E> 11394353 01 10
== Executing PA-CTR 1, V(1)=2, V(2)=394349, repcount=131450, factor=4/3
4731448 947883479476 154 01525803 (01)(01)E> 113 01 10
== Executing PPA-CTR 3 (once), V(1)=525802, V(2)=0
4731467 947893995698 -1051456 01 (01)(01)E> 11525810 10 11
== Executing PA-CTR 1, V(1)=0, V(2)=525806, repcount=175269, factor=4/3
6308888 1685163394736 158 01701077 (01)(01)E> 113 10 11
== Executing PPA-CTR 4 (once), V(1)=701076
6308911 1685173209970 -1401996 013 (01)(01)E> 11701083 01 10
== Executing PA-CTR 1, V(1)=2, V(2)=701079, repcount=233694, factor=4/3
8412157 2995898823814 168 01934779 (01)(01)E> 11 01 10
== Executing PPA-CTR 16 (once), V(1)=934776
8412170 2995906302106 -1869392 01 (01)(01)E> 11934780 10 11 10 11
== Executing PA-CTR 6, V(1)=0, V(2)=934776, repcount=311593, factor=4/3
11216507 5326085378960 166 011246373 (01)(01)E> 11 10 11 10 11
== Executing PPA-CTR 13 (once), V(1)=1246372, V(2)=0
11216531 5326102828322 -2492580 013 (01)(01)E> 111246376 01 11 01 10
== Executing PA-CTR 6, V(1)=2, V(2)=1246372, repcount=415458, factor=4/3
14955653 9468660304718 168 011661835 (01)(01)E> 112 01 11 01 10
14955654 9468660304725 163 011661835 <A(10)(10) 10 11 01 11 01 10
14955655 9468663628395 -3323507 <A(10)(10) 101661836 11 01 11 01 10
14955656 9468663628404 -3323502 (10)(11)F> 101661836 11 01 11 01 10
14955657 9468670275748 170 101661836 (10)(11)F> 11 01 11 01 10
14955658 9468670275752 172 101661837 (10)(10)A> 01 11 01 10
14955659 9468670275756 174 101661838 (10)(01)E> 11 01 10
14955660 9468670275770 176 101661839 (10)(11)F> 01 10
14955661 9468670275772 178 101661840 (11)(00)D> 10
14955662 9468670275774 180 101661840 11 (00)(11)F>
14955663 9468670275781 175 101661840 11 <A(11)(10) 11
14955664 9468670275783 173 101661840 <C(10)(11) 10 11
14955665 9468670275785 171 101661839 <C(11)(10) 11 10 11
14955666 9468670275787 169 101661838 <C(11)(11) 10 11 10 11
14955667 9468673599463 -3323507 <C(11)(11) 111661838 10 11 10 11
14955668 9468673599465 -3323509 <A(11)(11) 111661839 10 11 10 11
14955669 9468673599486 -3323504 01 (01)(01)E> 111661839 10 11 10 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 011+V(1) (01)(01)E> 112 01 11 01 10
1 7 -5 011+V(1) <A(10)(10) 10 11 01 11 01 10
2 9+2*V(1) -7+-2*V(1) <A(10)(10) 102+V(1) 11 01 11 01 10
3 18+2*V(1) -2+-2*V(1) (10)(11)F> 102+V(1) 11 01 11 01 10
4 26+6*V(1) 2 102+V(1) (10)(11)F> 11 01 11 01 10
5 30+6*V(1) 4 103+V(1) (10)(10)A> 01 11 01 10
6 34+6*V(1) 6 104+V(1) (10)(01)E> 11 01 10
7 48+6*V(1) 8 105+V(1) (10)(11)F> 01 10
8 50+6*V(1) 10 106+V(1) (11)(00)D> 10
9 52+6*V(1) 12 106+V(1) 11 (00)(11)F>
10 59+6*V(1) 7 106+V(1) 11 <A(11)(10) 11
11 61+6*V(1) 5 106+V(1) <C(10)(11) 10 11
12 63+6*V(1) 3 105+V(1) <C(11)(10) 11 10 11
13 65+6*V(1) 1 104+V(1) <C(11)(11) 10 11 10 11
14 73+8*V(1) -7+-2*V(1) <C(11)(11) 114+V(1) 10 11 10 11
15 75+8*V(1) -9+-2*V(1) <A(11)(11) 115+V(1) 10 11 10 11
16 96+8*V(1) -4+-2*V(1) 01 (01)(01)E> 115+V(1) 10 11 10 11
<< Success! ==> defined new CTR 20 (PPA)
14955669 9468673599486 -3323504 01 (01)(01)E> 111661839 10 11 10 11
== Executing PA-CTR 6, V(1)=0, V(2)=1661835, repcount=553946, factor=4/3
19941183 16833247182986 172 012215785 (01)(01)E> 11 10 11 10 11
== Executing PPA-CTR 13 (once), V(1)=2215784, V(2)=0
19941207 16833278204116 -4431398 013 (01)(01)E> 112215788 01 11 01 10
== Executing PA-CTR 6, V(1)=2, V(2)=2215784, repcount=738595, factor=4/3
26588562 29925871682366 172 012954383 (01)(01)E> 113 01 11 01 10
== Executing PPA-CTR 8 (once), V(1)=2954382, V(2)=0
26588584 29925930770188 -5908598 01 (01)(01)E> 112954389 10 11 10 11
== Executing PA-CTR 6, V(1)=0, V(2)=2954385, repcount=984796, factor=4/3
35451748 53201731949588 178 013939185 (01)(01)E> 11 10 11 10 11
== Executing PPA-CTR 13 (once), V(1)=3939184, V(2)=0
35451772 53201787098318 -7878192 013 (01)(01)E> 113939188 01 11 01 10
== Executing PA-CTR 6, V(1)=2, V(2)=3939184, repcount=1313062, factor=4/3
47269330 94581042592914 180 015252251 (01)(01)E> 112 01 11 01 10
== Executing PPA-CTR 20 (once), V(1)=5252250
47269346 94581084611010 -10504324 01 (01)(01)E> 115252255 10 11 10 11
== Executing PA-CTR 6, V(1)=0, V(2)=5252251, repcount=1750751, factor=4/3
63026105 168144262681580 182 017003005 (01)(01)E> 112 10 11 10 11
== Executing PPA-CTR 17 (once), V(1)=7003003
63026134 168144360723808 -14005828 013 (01)(01)E> 117003007 01 114 01 10
== Executing PA-CTR 6, V(1)=2, V(2)=7003003, repcount=2334335, factor=4/3
84035149 298923401540658 182 019337343 (01)(01)E> 112 01 114 01 10
84035150 298923401540665 177 019337343 <A(10)(10) 10 11 01 114 01 10
84035151 298923420215351 -18674509 <A(10)(10) 109337344 11 01 114 01 10
84035152 298923420215360 -18674504 (10)(11)F> 109337344 11 01 114 01 10
84035153 298923457564736 184 109337344 (10)(11)F> 11 01 114 01 10
84035154 298923457564740 186 109337345 (10)(10)A> 01 114 01 10
84035155 298923457564744 188 109337346 (10)(01)E> 114 01 10
84035156 298923457564758 190 109337347 (10)(11)F> 113 01 10
84035157 298923457564762 192 109337348 (10)(10)A> 112 01 10
84035158 298923457564767 187 109337348 <B(01)(01) 01 11 01 10
84035159 298923476239463 -18674509 <B(01)(01) 019337349 11 01 10
84035160 298923476239476 -18674504 01 (01)(01)E> 019337349 11 01 10
84035161 298923513588872 194 019337350 (01)(01)E> 11 01 10
84035162 298923513588879 189 019337350 <A(10)(10) 10 01 10
84035163 298923532263579 -18674511 <A(10)(10) 109337351 01 10
84035164 298923532263588 -18674506 (10)(11)F> 109337351 01 10
84035165 298923569612992 196 109337351 (10)(11)F> 01 10
84035166 298923569612994 198 109337352 (11)(00)D> 10
84035167 298923569612996 200 109337352 11 (00)(11)F>
84035168 298923569613003 195 109337352 11 <A(11)(10) 11
84035169 298923569613005 193 109337352 <C(10)(11) 10 11
84035170 298923569613007 191 109337351 <C(11)(10) 11 10 11
84035171 298923569613009 189 109337350 <C(11)(11) 10 11 10 11
84035172 298923588287709 -18674511 <C(11)(11) 119337350 10 11 10 11
84035173 298923588287711 -18674513 <A(11)(11) 119337351 10 11 10 11
84035174 298923588287732 -18674508 01 (01)(01)E> 119337351 10 11 10 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 011+V(1) (01)(01)E> 112 01 114 01 10
1 7 -5 011+V(1) <A(10)(10) 10 11 01 114 01 10
2 9+2*V(1) -7+-2*V(1) <A(10)(10) 102+V(1) 11 01 114 01 10
3 18+2*V(1) -2+-2*V(1) (10)(11)F> 102+V(1) 11 01 114 01 10
4 26+6*V(1) 2 102+V(1) (10)(11)F> 11 01 114 01 10
5 30+6*V(1) 4 103+V(1) (10)(10)A> 01 114 01 10
6 34+6*V(1) 6 104+V(1) (10)(01)E> 114 01 10
7 48+6*V(1) 8 105+V(1) (10)(11)F> 113 01 10
8 52+6*V(1) 10 106+V(1) (10)(10)A> 112 01 10
9 57+6*V(1) 5 106+V(1) <B(01)(01) 01 11 01 10
10 69+8*V(1) -7+-2*V(1) <B(01)(01) 017+V(1) 11 01 10
11 82+8*V(1) -2+-2*V(1) 01 (01)(01)E> 017+V(1) 11 01 10
12 110+12*V(1) 12 018+V(1) (01)(01)E> 11 01 10
13 117+12*V(1) 7 018+V(1) <A(10)(10) 10 01 10
14 133+14*V(1) -9+-2*V(1) <A(10)(10) 109+V(1) 01 10
15 142+14*V(1) -4+-2*V(1) (10)(11)F> 109+V(1) 01 10
16 178+18*V(1) 14 109+V(1) (10)(11)F> 01 10
17 180+18*V(1) 16 1010+V(1) (11)(00)D> 10
18 182+18*V(1) 18 1010+V(1) 11 (00)(11)F>
19 189+18*V(1) 13 1010+V(1) 11 <A(11)(10) 11
20 191+18*V(1) 11 1010+V(1) <C(10)(11) 10 11
21 193+18*V(1) 9 109+V(1) <C(11)(10) 11 10 11
22 195+18*V(1) 7 108+V(1) <C(11)(11) 10 11 10 11
23 211+20*V(1) -9+-2*V(1) <C(11)(11) 118+V(1) 10 11 10 11
24 213+20*V(1) -11+-2*V(1) <A(11)(11) 119+V(1) 10 11 10 11
25 234+20*V(1) -6+-2*V(1) 01 (01)(01)E> 119+V(1) 10 11 10 11
<< Success! ==> defined new CTR 21 (PPA)
84035174 298923588287732 -18674508 01 (01)(01)E> 119337351 10 11 10 11
== Executing PA-CTR 6, V(1)=0, V(2)=9337347, repcount=3112450, factor=4/3
112047224 531420011520432 192 0112449801 (01)(01)E> 11 10 11 10 11
== Executing PPA-CTR 13 (once), V(1)=12449800, V(2)=0
112047248 531420185817786 -24899410 013 (01)(01)E> 1112449804 01 11 01 10
== Executing PA-CTR 6, V(1)=2, V(2)=12449800, repcount=4149934, factor=4/3
149396654 944747329217710 194 0116599739 (01)(01)E> 112 01 11 01 10
== Executing PPA-CTR 20 (once), V(1)=16599738
149396670 944747462015710 -33199286 01 (01)(01)E> 1116599743 10 11 10 11
== Executing PA-CTR 6, V(1)=0, V(2)=16599739, repcount=5533247, factor=4/3
199195893 1679551453257288 196 0122132989 (01)(01)E> 112 10 11 10 11
== Executing PPA-CTR 17 (once), V(1)=22132987
199195922 1679551763119292 -44265782 013 (01)(01)E> 1122132991 01 114 01 10
== Executing PA-CTR 6, V(1)=2, V(2)=22132987, repcount=7377663, factor=4/3
265594889 2985870151753358 196 0129510655 (01)(01)E> 112 01 114 01 10
== Executing PPA-CTR 21 (once), V(1)=29510654
265594914 2985870741966672 -59021118 01 (01)(01)E> 1129510663 10 11 10 11
== Executing PA-CTR 6, V(1)=0, V(2)=29510659, repcount=9836887, factor=4/3
354126897 5308215494881930 204 0139347549 (01)(01)E> 112 10 11 10 11
== Executing PPA-CTR 17 (once), V(1)=39347547
354126926 5308216045747774 -78694894 013 (01)(01)E> 1139347551 01 114 01 10
== Executing PA-CTR 6, V(1)=2, V(2)=39347547, repcount=13115850, factor=4/3
472169576 9436829473197274 206 0152463403 (01)(01)E> 11 01 114 01 10
== Executing PPA-CTR 18 (once), V(1)=52463400, V(2)=0
472169591 9436829892904576 -104926602 01 (01)(01)E> 1152463404 105 11 01 10
== Executing PA-CTR 6, V(1)=0, V(2)=52463400, repcount=17487801, factor=4/3
629559800 16776587108917846 204 0169951205 (01)(01)E> 11 105 11 01 10
629559801 16776587108917853 199 0169951205 <A(10)(10) 106 11 01 10
629559802 16776587248820263 -139902211 <A(10)(10) 1069951211 11 01 10
629559803 16776587248820272 -139902206 (10)(11)F> 1069951211 11 01 10
629559804 16776587528625116 216 1069951211 (10)(11)F> 11 01 10
629559805 16776587528625120 218 1069951212 (10)(10)A> 01 10
629559806 16776587528625124 220 1069951213 (10)(01)E> 10
629559807 16776587528625126 222 1069951214 (01)(01)B>
629559808 16776587528625131 217 1069951214 <A(10)(10) 10
629559809 16776587528625140 222 1069951214 (10)(11)F> 10
629559810 16776587528625144 224 1069951215 (10)(11)F>
629559811 16776587528625151 219 1069951215 <C(11)(10) 11
629559812 16776587528625153 217 1069951214 <C(11)(11) 10 11
629559813 16776587668527581 -139902211 <C(11)(11) 1169951214 10 11
629559814 16776587668527583 -139902213 <A(11)(11) 1169951215 10 11
629559815 16776587668527604 -139902208 01 (01)(01)E> 1169951215 10 11
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 011+V(1) (01)(01)E> 11 101+V(2) 11 01 10
1 7 -5 011+V(1) <A(10)(10) 102+V(2) 11 01 10
2 9+2*V(1) -7+-2*V(1) <A(10)(10) 103+V(1)+V(2) 11 01 10
3 18+2*V(1) -2+-2*V(1) (10)(11)F> 103+V(1)+V(2) 11 01 10
4 30+6*V(1)+4*V(2) 4+2*V(2) 103+V(1)+V(2) (10)(11)F> 11 01 10
5 34+6*V(1)+4*V(2) 6+2*V(2) 104+V(1)+V(2) (10)(10)A> 01 10
6 38+6*V(1)+4*V(2) 8+2*V(2) 105+V(1)+V(2) (10)(01)E> 10
7 40+6*V(1)+4*V(2) 10+2*V(2) 106+V(1)+V(2) (01)(01)B>
8 45+6*V(1)+4*V(2) 5+2*V(2) 106+V(1)+V(2) <A(10)(10) 10
9 54+6*V(1)+4*V(2) 10+2*V(2) 106+V(1)+V(2) (10)(11)F> 10
10 58+6*V(1)+4*V(2) 12+2*V(2) 107+V(1)+V(2) (10)(11)F>
11 65+6*V(1)+4*V(2) 7+2*V(2) 107+V(1)+V(2) <C(11)(10) 11
12 67+6*V(1)+4*V(2) 5+2*V(2) 106+V(1)+V(2) <C(11)(11) 10 11
13 79+8*V(1)+6*V(2) -7+-2*V(1) <C(11)(11) 116+V(1)+V(2) 10 11
14 81+8*V(1)+6*V(2) -9+-2*V(1) <A(11)(11) 117+V(1)+V(2) 10 11
15 102+8*V(1)+6*V(2) -4+-2*V(1) 01 (01)(01)E> 117+V(1)+V(2) 10 11
<< Success! ==> defined new CTR 22 (PPA)
629559815 16776587668527604 -139902208 01 (01)(01)E> 1169951215 10 11
== Executing PA-CTR 1, V(1)=0, V(2)=69951211, repcount=23317071, factor=4/3
839413454 29825047941569854 218 0193268285 (01)(01)E> 112 10 11
== Executing PPA-CTR 12 (once), V(1)=93268283
839413478 29825049247325972 -186536352 013 (01)(01)E> 1193268287 01 11 01 10
== Executing PA-CTR 6, V(1)=2, V(2)=93268283, repcount=31089428, factor=4/3
1119218330 53022312224398348 216 01124357715 (01)(01)E> 113 01 11 01 10
== Executing PPA-CTR 8 (once), V(1)=124357714, V(2)=0
1119218352 53022314711552810 -248715218 01 (01)(01)E> 11124357721 10 11 10 11
== Executing PA-CTR 6, V(1)=0, V(2)=124357717, repcount=41452573, factor=4/3
1492291509 94261896018059064 220 01165810293 (01)(01)E> 112 10 11 10 11
== Executing PPA-CTR 17 (once), V(1)=165810291
1492291538 94261898339403324 -331620366 013 (01)(01)E> 11165810295 01 114 01 10
== Executing PA-CTR 6, V(1)=2, V(2)=165810291, repcount=55270098, factor=4/3
1989722420 1675767[4]8620680 222 01221080395 (01)(01)E> 11 01 114 01 10
== Executing PPA-CTR 18 (once), V(1)=221080392, V(2)=0
1989722435 1675767[4]7263918 -442160570 01 (01)(01)E> 11221080396 105 11 01 10
== Executing PA-CTR 6, V(1)=0, V(2)=221080392, repcount=73693465, factor=4/3
2652963620 2979141[4]6112708 220 01294773861 (01)(01)E> 11 105 11 01 10
== Executing PPA-CTR 22 (once), V(1)=294773860, V(2)=4
2652963635 2979141[4]4303714 -589547504 01 (01)(01)E> 11294773871 10 11
== Executing PA-CTR 1, V(1)=0, V(2)=294773867, repcount=98257956, factor=4/3
3537285239 5296251[4]9320154 232 01393031825 (01)(01)E> 113 10 11
== Executing PPA-CTR 4 (once), V(1)=393031824
3537285262 5296251[4]1765860 -786063418 013 (01)(01)E> 11393031831 01 10
== Executing PA-CTR 1, V(1)=2, V(2)=393031827, repcount=131010610, factor=4/3
4716380752 9415559[4]4238960 242 01524042443 (01)(01)E> 11 01 10
== Executing PPA-CTR 16 (once), V(1)=524042440
4716380765 9415559[4]6578564 -1048084646 01 (01)(01)E> 11524042444 10 11 10 11
== Executing PA-CTR 6, V(1)=0, V(2)=524042440, repcount=174680814, factor=4/3
6288508091 1673877[5]4758312 238 01698723257 (01)(01)E> 112 10 11 10 11
== Executing PPA-CTR 17 (once), V(1)=698723255
6288508120 1673877[5]6884068 -1397446276 013 (01)(01)E> 11698723259 01 114 01 10
== Executing PA-CTR 6, V(1)=2, V(2)=698723255, repcount=232907752, factor=4/3
8384677888 2975781[5]1070804 236 01931631011 (01)(01)E> 113 01 114 01 10
8384677889 2975781[5]1070811 231 01931631011 <A(10)(10) 10 112 01 114 01 10
8384677890 2975781[5]4332833 -1863261791 <A(10)(10) 10931631012 112 01 114 01 10
8384677891 2975781[5]4332842 -1863261786 (10)(11)F> 10931631012 112 01 114 01 10
8384677892 2975781[5]0856890 238 10931631012 (10)(11)F> 112 01 114 01 10
8384677893 2975781[5]0856894 240 10931631013 (10)(10)A> 11 01 114 01 10
8384677894 2975781[5]0856899 235 10931631013 <B(01)(01) 012 114 01 10
8384677895 2975781[5]4118925 -1863261791 <B(01)(01) 01931631015 114 01 10
8384677896 2975781[5]4118938 -1863261786 01 (01)(01)E> 01931631015 114 01 10
8384677897 2975781[5]0642998 244 01931631016 (01)(01)E> 114 01 10
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 011+V(1) (01)(01)E> 113 011+V(3) 114+V(2) [*]* [*]*
1 7 -5 011+V(1) <A(10)(10) 10 112 011+V(3) 114+V(2) [*]* [*]*
2 9+2*V(1) -7+-2*V(1) <A(10)(10) 102+V(1) 112 011+V(3) 114+V(2) [*]* [*]*
3 18+2*V(1) -2+-2*V(1) (10)(11)F> 102+V(1) 112 011+V(3) 114+V(2) [*]* [*]*
4 26+6*V(1) 2 102+V(1) (10)(11)F> 112 011+V(3) 114+V(2) [*]* [*]*
5 30+6*V(1) 4 103+V(1) (10)(10)A> 11 011+V(3) 114+V(2) [*]* [*]*
6 35+6*V(1) -1 103+V(1) <B(01)(01) 012+V(3) 114+V(2) [*]* [*]*
7 41+8*V(1) -7+-2*V(1) <B(01)(01) 015+V(1)+V(3) 114+V(2) [*]* [*]*
8 54+8*V(1) -2+-2*V(1) 01 (01)(01)E> 015+V(1)+V(3) 114+V(2) [*]* [*]*
9 74+12*V(1)+4*V(3) 8+2*V(3) 016+V(1)+V(3) (01)(01)E> 114+V(2) [*]* [*]*
<< Success! ==> defined new CTR 23 (PPA)
8384677897 2975781[5]0642998 244 01931631016 (01)(01)E> 114 01 10
== Executing PA-CTR 1, V(1)=931631015, V(2)=0, repcount=1, factor=4/3
8384677906 2975781[5]0215248 250 01931631020 (01)(01)E> 11 01 10
== Executing PPA-CTR 16 (once), V(1)=931631017
8384677919 2975781[5]3263468 -1863261792 01 (01)(01)E> 11931631021 10 11 10 11
== Executing PA-CTR 6, V(1)=0, V(2)=931631017, repcount=310543673, factor=4/3
11179570976 5290278[5]6214722 246 011242174693 (01)(01)E> 112 10 11 10 11
== Executing PPA-CTR 17 (once), V(1)=1242174691
11179571005 5290278[5]6660582 -2484349140 013 (01)(01)E> 111242174695 01 114 01 10
== Executing PA-CTR 6, V(1)=2, V(2)=1242174691, repcount=414058231, factor=4/3
14906095084 9404940[5]3121416 246 011656232927 (01)(01)E> 112 01 114 01 10
== Executing PPA-CTR 21 (once), V(1)=1656232926
14906095109 9404940[5]7780170 -3312465612 01 (01)(01)E> 111656232935 10 11 10 11
== Executing PA-CTR 6, V(1)=0, V(2)=1656232931, repcount=552077644, factor=4/3
19874793905 1671989[6]3529458 252 012208310577 (01)(01)E> 113 10 11 10 11
== Executing PPA-CTR 7 (once), V(1)=2208310576
19874793931 1671989[6]9877692 -4416620902 013 (01)(01)E> 112208310582 01 11 01 10
== Executing PA-CTR 6, V(1)=2, V(2)=2208310578, repcount=736103527, factor=4/3
26499725674 2972425[6]1278078 260 012944414111 (01)(01)E> 11 01 11 01 10
== Executing PPA-CTR 9 (once), V(1)=2944414108
26499725695 2972425[6]6591056 -5888827964 01 (01)(01)E> 112944414112 10 114 10 11
== Executing PA-CTR 6, V(1)=0, V(2)=2944414108, repcount=981471370, factor=4/3
35332968025 5284312[6]6519676 256 013925885481 (01)(01)E> 112 10 114 10 11
== Executing PPA-CTR 15 (once), V(1)=3925885480
35332968046 5284312[6]8916528 -7851770708 10 (10)(10)A> 113925885484 015 10 11
== Executing PA-CTR 10, V(1)=0, V(2)=3925885480, repcount=1308628494, factor=4/3
47110624492 9394332[6]4820116 256 105234513977 (10)(10)A> 112 015 10 11
47110624493 9394332[6]4820121 251 105234513977 <B(01)(01) 01 11 015 10 11
47110624494 9394332[6]3848075 -10469027703 <B(01)(01) 015234513978 11 015 10 11
47110624495 9394332[6]3848088 -10469027698 01 (01)(01)E> 015234513978 11 015 10 11
47110624496 9394332[6]1904000 258 015234513979 (01)(01)E> 11 015 10 11
47110624497 9394332[6]1904007 253 015234513979 <A(10)(10) 10 015 10 11
47110624498 9394332[6]0931965 -10469027705 <A(10)(10) 105234513980 015 10 11
47110624499 9394332[6]0931974 -10469027700 (10)(11)F> 105234513980 015 10 11
47110624500 9394332[6]8987894 260 105234513980 (10)(11)F> 015 10 11
47110624501 9394332[6]8987896 262 105234513981 (11)(00)D> 014 10 11
47110624502 9394332[6]8987897 263 105234513981 11001 Z> 1 013 10 11 [stop]
Lines: 639
Top steps: 638
Macro steps: 47110624502
Basic steps: 93943325529148987897
Tape index: 263
ones: 5234513991
log10(ones ): 9.719
log10(steps ): 19.973
Run state: stop
Some long numbers above are shortened: #(omitted digits) shown in "[]".
Input to awk program:
gohalt 1
L 12
5T B1R B0L A1L C1L B1L D0R Z1R E1R F1R A0R C0R C1L : 5234513991 93943325529148987897
T 6-state TM #d from MaBu-List
M 650
pref sim
machv mbL6_d just simple
machv mbL6_d-r with repetitions reduced
machv mbL6_d-1 with tape symbol exponents
machv mbL6_d-m as 2-bck-bck-macro machine
machv mbL6_d-a as 2-bck-bck-macro machine with pure additive config-TRs
iam mbL6_d-a
mtype 2 0 0
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:10:44 CEST 2010
edate Tue Jul 6 22:10:47 CEST 2010
bnspeed 1
short 7
Constructed by: $Id: tmJob.awk,v 1.34 2010/05/06 18:26:17 heiner Exp $
$Id: basics.awk,v 1.1 2010/05/06 17:24:17 heiner Exp $
$Id: htSupp.awk,v 1.14 2010/07/06 19:48:32 heiner Exp $
$Id: mmSim.awk,v 1.34 2005/01/09 22:23:28 heiner Exp $
$Id: bignum.awk,v 1.34 2010/05/06 17:58:14 heiner Exp $
$Id: varLI.awk,v 1.11 2005/01/15 21:01:29 heiner Exp $
bignum signature: LEN={S++:9 U++:9 S+:8 U+:8 S*:4 U*:4} DONT: y i o;
Start: Tue Jul 6 22:10:44 CEST 2010