Comment: This TM produces 458,357 nonzeros in 233,431,192,481 steps.
| State | on 0 |
on 1 |
on 2 |
on 3 |
on 4 |
on 0 | on 1 | on 2 | on 3 | on 4 | ||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Move | Goto | Move | Goto | Move | Goto | Move | Goto | Move | Goto | |||||||||||
| A | B1R | B3R | B3R | A1L | B3L | 1 | right | B | 3 | right | B | 3 | right | B | 1 | left | A | 3 | left | B |
| B | A2L | A3R | B4L | A2R | Z1R | 2 | left | A | 3 | right | A | 4 | left | B | 2 | right | A | 1 | right | Z |
The same TM just simple.
The same TM with repetitions reduced.
The same TM with tape symbol exponents.
The same TM as bck-2-macro machine.
Simulation is done as bck-2-macro machine with pure additive config-TRs.
Pushing initial machine.
Pushing BCK machine.
Pushing macro factor 2.
Steps BasSteps BasTpos Tape contents
0 0 0 (0)A>
1 8 -2 <A(2) 43
2 16 0 03 (3)A> 43
3 24 -2 03 <A(1) 11
4 28 0 13 (3)B> 11
5 30 2 13 33 (3)B>
6 32 0 13 33 <A(1) 20
7 34 -2 13 <A(1) 11 20
8 38 0 33 (3)B> 11 20
9 40 2 332 (3)B> 20
10 44 0 332 <B(4) 30
11 56 -4 <B(4) 332 30
12 70 -2 33 (3)A> 332 30
13 72 -4 33 <A(1) 13 33 30
14 74 -6 <A(1) 11 13 33 30
15 76 -4 01 (3)A> 11 13 33 30
16 78 -2 01 33 (3)A> 13 33 30
17 80 0 01 332 (2)A> 33 30
18 86 -2 01 332 <A(1) 11 30
19 90 -6 01 <A(1) 113 30
20 92 -4 03 (3)A> 113 30
21 98 2 03 333 (3)A> 30
22 100 0 03 333 <A(1) 10
23 106 -6 03 <A(1) 113 10
24 110 -4 13 (3)B> 113 10
25 116 2 13 333 (3)B> 10
26 118 4 13 334 (1)B>
27 124 2 13 334 <B(4) 30
28 148 -6 13 <B(4) 334 30
29 160 -8 <A(1) 11 334 30
30 162 -6 01 (3)A> 11 334 30
31 164 -4 01 33 (3)A> 334 30
32 166 -6 01 33 <A(1) 13 333 30
33 168 -8 01 <A(1) 11 13 333 30
34 170 -6 03 (3)A> 11 13 333 30
35 172 -4 03 33 (3)A> 13 333 30
36 174 -2 03 332 (2)A> 333 30
37 180 -4 03 332 <A(1) 11 332 30
38 184 -8 03 <A(1) 113 332 30
39 188 -6 13 (3)B> 113 332 30
40 194 0 13 333 (3)B> 332 30
41 198 2 13 334 (3)A> 33 30
42 200 0 13 334 <A(1) 13 30
43 208 -8 13 <A(1) 114 13 30
44 212 -6 33 (3)B> 114 13 30
45 220 2 335 (3)B> 13 30
46 224 0 335 <A(1) 11 30
47 234 -10 <A(1) 116 30
48 236 -8 01 (3)A> 116 30
49 248 4 01 336 (3)A> 30
50 250 2 01 336 <A(1) 10
51 262 -10 01 <A(1) 116 10
52 264 -8 03 (3)A> 116 10
53 276 4 03 336 (3)A> 10
54 280 2 03 336 <A(1) 12
55 292 -10 03 <A(1) 116 12
56 296 -8 13 (3)B> 116 12
57 308 4 13 336 (3)B> 12
58 310 6 13 337 (3)B>
59 312 4 13 337 <A(1) 20
60 326 -10 13 <A(1) 117 20
61 330 -8 33 (3)B> 117 20
62 344 6 338 (3)B> 20
63 348 4 338 <B(4) 30
64 396 -12 <B(4) 338 30
65 410 -10 33 (3)A> 338 30
66 412 -12 33 <A(1) 13 337 30
67 414 -14 <A(1) 11 13 337 30
68 416 -12 01 (3)A> 11 13 337 30
69 418 -10 01 33 (3)A> 13 337 30
70 420 -8 01 332 (2)A> 337 30
71 426 -10 01 332 <A(1) 11 336 30
72 430 -14 01 <A(1) 113 336 30
73 432 -12 03 (3)A> 113 336 30
74 438 -6 03 333 (3)A> 336 30
75 440 -8 03 333 <A(1) 13 335 30
76 446 -14 03 <A(1) 113 13 335 30
77 450 -12 13 (3)B> 113 13 335 30
78 456 -6 13 333 (3)B> 13 335 30
79 460 -8 13 333 <A(1) 11 335 30
80 466 -14 13 <A(1) 114 335 30
81 470 -12 33 (3)B> 114 335 30
82 478 -4 335 (3)B> 335 30
83 482 -2 336 (3)A> 334 30
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 331+V(1) (3)A> 335+V(2) [*]*
1 2 -2 331+V(1) <A(1) 13 334+V(2) [*]*
2 4+2*V(1) -4+-2*V(1) <A(1) 111+V(1) 13 334+V(2) [*]*
3 6+2*V(1) -2+-2*V(1) 01 (3)A> 111+V(1) 13 334+V(2) [*]*
4 8+4*V(1) 0 01 331+V(1) (3)A> 13 334+V(2) [*]*
5 10+4*V(1) 2 01 332+V(1) (2)A> 334+V(2) [*]*
6 16+4*V(1) 0 01 332+V(1) <A(1) 11 333+V(2) [*]*
7 20+6*V(1) -4+-2*V(1) 01 <A(1) 113+V(1) 333+V(2) [*]*
8 22+6*V(1) -2+-2*V(1) 03 (3)A> 113+V(1) 333+V(2) [*]*
9 28+8*V(1) 4 03 333+V(1) (3)A> 333+V(2) [*]*
10 30+8*V(1) 2 03 333+V(1) <A(1) 13 332+V(2) [*]*
11 36+10*V(1) -4+-2*V(1) 03 <A(1) 113+V(1) 13 332+V(2) [*]*
12 40+10*V(1) -2+-2*V(1) 13 (3)B> 113+V(1) 13 332+V(2) [*]*
13 46+12*V(1) 4 13 333+V(1) (3)B> 13 332+V(2) [*]*
14 50+12*V(1) 2 13 333+V(1) <A(1) 11 332+V(2) [*]*
15 56+14*V(1) -4+-2*V(1) 13 <A(1) 114+V(1) 332+V(2) [*]*
16 60+14*V(1) -2+-2*V(1) 33 (3)B> 114+V(1) 332+V(2) [*]*
17 68+16*V(1) 6 335+V(1) (3)B> 332+V(2) [*]*
18 72+16*V(1) 8 336+V(1) (3)A> 331+V(2) [*]*
<< Success! ==> defined new CTR 1 (PA)
84 484 -4 336 <A(1) 13 333 30
85 496 -16 <A(1) 116 13 333 30
86 498 -14 01 (3)A> 116 13 333 30
87 510 -2 01 336 (3)A> 13 333 30
88 512 0 01 337 (2)A> 333 30
89 518 -2 01 337 <A(1) 11 332 30
90 532 -16 01 <A(1) 118 332 30
91 534 -14 03 (3)A> 118 332 30
92 550 2 03 338 (3)A> 332 30
93 552 0 03 338 <A(1) 13 33 30
94 568 -16 03 <A(1) 118 13 33 30
95 572 -14 13 (3)B> 118 13 33 30
96 588 2 13 338 (3)B> 13 33 30
97 592 0 13 338 <A(1) 11 33 30
98 608 -16 13 <A(1) 119 33 30
99 612 -14 33 (3)B> 119 33 30
100 630 4 3310 (3)B> 33 30
101 634 6 3311 (3)A> 30
102 636 4 3311 <A(1) 10
103 658 -18 <A(1) 1111 10
104 660 -16 01 (3)A> 1111 10
105 682 6 01 3311 (3)A> 10
106 686 4 01 3311 <A(1) 12
107 708 -18 01 <A(1) 1111 12
108 710 -16 03 (3)A> 1111 12
109 732 6 03 3311 (3)A> 12
110 740 4 03 3311 <B(4) 33
111 806 -18 03 <B(4) 3312
112 810 -20 <A(2) 43 3312
113 818 -18 03 (3)A> 43 3312
114 826 -20 03 <A(1) 11 3312
115 830 -18 13 (3)B> 11 3312
116 832 -16 13 33 (3)B> 3312
117 836 -14 13 332 (3)A> 3311
118 838 -16 13 332 <A(1) 13 3310
119 842 -20 13 <A(1) 112 13 3310
120 846 -18 33 (3)B> 112 13 3310
121 850 -14 333 (3)B> 13 3310
122 854 -16 333 <A(1) 11 3310
123 860 -22 <A(1) 114 3310
124 862 -20 01 (3)A> 114 3310
125 870 -12 01 334 (3)A> 3310
126 872 -14 01 334 <A(1) 13 339
127 880 -22 01 <A(1) 114 13 339
128 882 -20 03 (3)A> 114 13 339
129 890 -12 03 334 (3)A> 13 339
130 892 -10 03 335 (2)A> 339
131 898 -12 03 335 <A(1) 11 338
132 908 -22 03 <A(1) 116 338
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 03 <A(1) 111+V(2) 335+V(1)
1 4 2 13 (3)B> 111+V(2) 335+V(1)
2 6+2*V(2) 4+2*V(2) 13 331+V(2) (3)B> 335+V(1)
3 10+2*V(2) 6+2*V(2) 13 332+V(2) (3)A> 334+V(1)
4 12+2*V(2) 4+2*V(2) 13 332+V(2) <A(1) 13 333+V(1)
5 16+4*V(2) 0 13 <A(1) 112+V(2) 13 333+V(1)
6 20+4*V(2) 2 33 (3)B> 112+V(2) 13 333+V(1)
7 24+6*V(2) 6+2*V(2) 333+V(2) (3)B> 13 333+V(1)
8 28+6*V(2) 4+2*V(2) 333+V(2) <A(1) 11 333+V(1)
9 34+8*V(2) -2 <A(1) 114+V(2) 333+V(1)
10 36+8*V(2) 0 01 (3)A> 114+V(2) 333+V(1)
11 44+10*V(2) 8+2*V(2) 01 334+V(2) (3)A> 333+V(1)
12 46+10*V(2) 6+2*V(2) 01 334+V(2) <A(1) 13 332+V(1)
13 54+12*V(2) -2 01 <A(1) 114+V(2) 13 332+V(1)
14 56+12*V(2) 0 03 (3)A> 114+V(2) 13 332+V(1)
15 64+14*V(2) 8+2*V(2) 03 334+V(2) (3)A> 13 332+V(1)
16 66+14*V(2) 10+2*V(2) 03 335+V(2) (2)A> 332+V(1)
17 72+14*V(2) 8+2*V(2) 03 335+V(2) <A(1) 11 331+V(1)
18 82+16*V(2) -2 03 <A(1) 116+V(2) 331+V(1)
<< Success! ==> defined new CTR 2 (PA)
132 908 -22 03 <A(1) 116 338
== Executing PA-CTR 2, V(1)=3, V(2)=5, repcount=1, factor=5/4
150 1070 -24 03 <A(1) 1111 334
151 1074 -22 13 (3)B> 1111 334
152 1096 0 13 3311 (3)B> 334
153 1100 2 13 3312 (3)A> 333
154 1102 0 13 3312 <A(1) 13 332
155 1126 -24 13 <A(1) 1112 13 332
156 1130 -22 33 (3)B> 1112 13 332
157 1154 2 3313 (3)B> 13 332
158 1158 0 3313 <A(1) 11 332
159 1184 -26 <A(1) 1114 332
160 1186 -24 01 (3)A> 1114 332
161 1214 4 01 3314 (3)A> 332
162 1216 2 01 3314 <A(1) 13 33
163 1244 -26 01 <A(1) 1114 13 33
164 1246 -24 03 (3)A> 1114 13 33
165 1274 4 03 3314 (3)A> 13 33
166 1276 6 03 3315 (2)A> 33
167 1282 4 03 3315 <A(1) 11
168 1312 -26 03 <A(1) 1116
169 1316 -24 13 (3)B> 1116
170 1348 8 13 3316 (3)B>
171 1350 6 13 3316 <A(1) 20
172 1382 -26 13 <A(1) 1116 20
173 1386 -24 33 (3)B> 1116 20
174 1418 8 3317 (3)B> 20
175 1422 6 3317 <B(4) 30
176 1524 -28 <B(4) 3317 30
177 1538 -26 33 (3)A> 3317 30
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 03 <A(1) 111+V(1) 334
1 4 2 13 (3)B> 111+V(1) 334
2 6+2*V(1) 4+2*V(1) 13 331+V(1) (3)B> 334
3 10+2*V(1) 6+2*V(1) 13 332+V(1) (3)A> 333
4 12+2*V(1) 4+2*V(1) 13 332+V(1) <A(1) 13 332
5 16+4*V(1) 0 13 <A(1) 112+V(1) 13 332
6 20+4*V(1) 2 33 (3)B> 112+V(1) 13 332
7 24+6*V(1) 6+2*V(1) 333+V(1) (3)B> 13 332
8 28+6*V(1) 4+2*V(1) 333+V(1) <A(1) 11 332
9 34+8*V(1) -2 <A(1) 114+V(1) 332
10 36+8*V(1) 0 01 (3)A> 114+V(1) 332
11 44+10*V(1) 8+2*V(1) 01 334+V(1) (3)A> 332
12 46+10*V(1) 6+2*V(1) 01 334+V(1) <A(1) 13 33
13 54+12*V(1) -2 01 <A(1) 114+V(1) 13 33
14 56+12*V(1) 0 03 (3)A> 114+V(1) 13 33
15 64+14*V(1) 8+2*V(1) 03 334+V(1) (3)A> 13 33
16 66+14*V(1) 10+2*V(1) 03 335+V(1) (2)A> 33
17 72+14*V(1) 8+2*V(1) 03 335+V(1) <A(1) 11
18 82+16*V(1) -2 03 <A(1) 116+V(1)
19 86+16*V(1) 0 13 (3)B> 116+V(1)
20 98+18*V(1) 12+2*V(1) 13 336+V(1) (3)B>
21 100+18*V(1) 10+2*V(1) 13 336+V(1) <A(1) 20
22 112+20*V(1) -2 13 <A(1) 116+V(1) 20
23 116+20*V(1) 0 33 (3)B> 116+V(1) 20
24 128+22*V(1) 12+2*V(1) 337+V(1) (3)B> 20
25 132+22*V(1) 10+2*V(1) 337+V(1) <B(4) 30
26 174+28*V(1) -4 <B(4) 337+V(1) 30
27 188+28*V(1) -2 33 (3)A> 337+V(1) 30
<< Success! ==> defined new CTR 3 (PPA)
177 1538 -26 33 (3)A> 3317 30
== Executing PA-CTR 1, V(1)=0, V(2)=12, repcount=4, factor=5/4
249 2306 6 3321 (3)A> 33 30
250 2308 4 3321 <A(1) 13 30
251 2350 -38 <A(1) 1121 13 30
252 2352 -36 01 (3)A> 1121 13 30
253 2394 6 01 3321 (3)A> 13 30
254 2396 8 01 3322 (2)A> 30
255 2400 10 01 3323 (1)B>
256 2406 8 01 3323 <B(4) 30
257 2544 -38 01 <B(4) 3323 30
258 2550 -36 03 (3)A> 3323 30
259 2552 -38 03 <A(1) 13 3322 30
260 2556 -36 13 (3)B> 13 3322 30
261 2560 -38 13 <A(1) 11 3322 30
262 2564 -36 33 (3)B> 11 3322 30
263 2566 -34 332 (3)B> 3322 30
264 2570 -32 333 (3)A> 3321 30
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 335+V(1) (3)A> 33 30
1 2 -2 335+V(1) <A(1) 13 30
2 12+2*V(1) -12+-2*V(1) <A(1) 115+V(1) 13 30
3 14+2*V(1) -10+-2*V(1) 01 (3)A> 115+V(1) 13 30
4 24+4*V(1) 0 01 335+V(1) (3)A> 13 30
5 26+4*V(1) 2 01 336+V(1) (2)A> 30
6 30+4*V(1) 4 01 337+V(1) (1)B>
7 36+4*V(1) 2 01 337+V(1) <B(4) 30
8 78+10*V(1) -12+-2*V(1) 01 <B(4) 337+V(1) 30
9 84+10*V(1) -10+-2*V(1) 03 (3)A> 337+V(1) 30
10 86+10*V(1) -12+-2*V(1) 03 <A(1) 13 336+V(1) 30
11 90+10*V(1) -10+-2*V(1) 13 (3)B> 13 336+V(1) 30
12 94+10*V(1) -12+-2*V(1) 13 <A(1) 11 336+V(1) 30
13 98+10*V(1) -10+-2*V(1) 33 (3)B> 11 336+V(1) 30
14 100+10*V(1) -8+-2*V(1) 332 (3)B> 336+V(1) 30
15 104+10*V(1) -6+-2*V(1) 333 (3)A> 335+V(1) 30
<< Success! ==> defined new CTR 4 (PPA)
264 2570 -32 333 (3)A> 3321 30
== Executing PA-CTR 1, V(1)=2, V(2)=16, repcount=5, factor=5/4
354 3890 8 3328 (3)A> 33 30
== Executing PPA-CTR 4 (once), V(1)=23
369 4224 -44 333 (3)A> 3328 30
== Executing PA-CTR 1, V(1)=2, V(2)=23, repcount=6, factor=5/4
477 6048 4 3333 (3)A> 334 30
478 6050 2 3333 <A(1) 13 333 30
479 6116 -64 <A(1) 1133 13 333 30
480 6118 -62 01 (3)A> 1133 13 333 30
481 6184 4 01 3333 (3)A> 13 333 30
482 6186 6 01 3334 (2)A> 333 30
483 6192 4 01 3334 <A(1) 11 332 30
484 6260 -64 01 <A(1) 1135 332 30
485 6262 -62 03 (3)A> 1135 332 30
486 6332 8 03 3335 (3)A> 332 30
487 6334 6 03 3335 <A(1) 13 33 30
488 6404 -64 03 <A(1) 1135 13 33 30
489 6408 -62 13 (3)B> 1135 13 33 30
490 6478 8 13 3335 (3)B> 13 33 30
491 6482 6 13 3335 <A(1) 11 33 30
492 6552 -64 13 <A(1) 1136 33 30
493 6556 -62 33 (3)B> 1136 33 30
494 6628 10 3337 (3)B> 33 30
495 6632 12 3338 (3)A> 30
496 6634 10 3338 <A(1) 10
497 6710 -66 <A(1) 1138 10
498 6712 -64 01 (3)A> 1138 10
499 6788 12 01 3338 (3)A> 10
500 6792 10 01 3338 <A(1) 12
501 6868 -66 01 <A(1) 1138 12
502 6870 -64 03 (3)A> 1138 12
503 6946 12 03 3338 (3)A> 12
504 6954 10 03 3338 <B(4) 33
505 7182 -66 03 <B(4) 3339
506 7186 -68 <A(2) 43 3339
507 7194 -66 03 (3)A> 43 3339
508 7202 -68 03 <A(1) 11 3339
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 331+V(1) (3)A> 334 30
1 2 -2 331+V(1) <A(1) 13 333 30
2 4+2*V(1) -4+-2*V(1) <A(1) 111+V(1) 13 333 30
3 6+2*V(1) -2+-2*V(1) 01 (3)A> 111+V(1) 13 333 30
4 8+4*V(1) 0 01 331+V(1) (3)A> 13 333 30
5 10+4*V(1) 2 01 332+V(1) (2)A> 333 30
6 16+4*V(1) 0 01 332+V(1) <A(1) 11 332 30
7 20+6*V(1) -4+-2*V(1) 01 <A(1) 113+V(1) 332 30
8 22+6*V(1) -2+-2*V(1) 03 (3)A> 113+V(1) 332 30
9 28+8*V(1) 4 03 333+V(1) (3)A> 332 30
10 30+8*V(1) 2 03 333+V(1) <A(1) 13 33 30
11 36+10*V(1) -4+-2*V(1) 03 <A(1) 113+V(1) 13 33 30
12 40+10*V(1) -2+-2*V(1) 13 (3)B> 113+V(1) 13 33 30
13 46+12*V(1) 4 13 333+V(1) (3)B> 13 33 30
14 50+12*V(1) 2 13 333+V(1) <A(1) 11 33 30
15 56+14*V(1) -4+-2*V(1) 13 <A(1) 114+V(1) 33 30
16 60+14*V(1) -2+-2*V(1) 33 (3)B> 114+V(1) 33 30
17 68+16*V(1) 6 335+V(1) (3)B> 33 30
18 72+16*V(1) 8 336+V(1) (3)A> 30
19 74+16*V(1) 6 336+V(1) <A(1) 10
20 86+18*V(1) -6+-2*V(1) <A(1) 116+V(1) 10
21 88+18*V(1) -4+-2*V(1) 01 (3)A> 116+V(1) 10
22 100+20*V(1) 8 01 336+V(1) (3)A> 10
23 104+20*V(1) 6 01 336+V(1) <A(1) 12
24 116+22*V(1) -6+-2*V(1) 01 <A(1) 116+V(1) 12
25 118+22*V(1) -4+-2*V(1) 03 (3)A> 116+V(1) 12
26 130+24*V(1) 8 03 336+V(1) (3)A> 12
27 138+24*V(1) 6 03 336+V(1) <B(4) 33
28 174+30*V(1) -6+-2*V(1) 03 <B(4) 337+V(1)
29 178+30*V(1) -8+-2*V(1) <A(2) 43 337+V(1)
30 186+30*V(1) -6+-2*V(1) 03 (3)A> 43 337+V(1)
31 194+30*V(1) -8+-2*V(1) 03 <A(1) 11 337+V(1)
<< Success! ==> defined new CTR 5 (PPA)
508 7202 -68 03 <A(1) 11 3339
== Executing PA-CTR 2, V(1)=34, V(2)=0, repcount=9, factor=5/4
670 10820 -86 03 <A(1) 1146 333
671 10824 -84 13 (3)B> 1146 333
672 10916 8 13 3346 (3)B> 333
673 10920 10 13 3347 (3)A> 332
674 10922 8 13 3347 <A(1) 13 33
675 11016 -86 13 <A(1) 1147 13 33
676 11020 -84 33 (3)B> 1147 13 33
677 11114 10 3348 (3)B> 13 33
678 11118 8 3348 <A(1) 11 33
679 11214 -88 <A(1) 1149 33
680 11216 -86 01 (3)A> 1149 33
681 11314 12 01 3349 (3)A> 33
682 11316 10 01 3349 <A(1) 13
683 11414 -88 01 <A(1) 1149 13
684 11416 -86 03 (3)A> 1149 13
685 11514 12 03 3349 (3)A> 13
686 11516 14 03 3350 (2)A>
687 11524 12 03 3350 <B(4) 43
688 11824 -88 03 <B(4) 3350 43
689 11828 -90 <A(2) 43 3350 43
690 11836 -88 03 (3)A> 43 3350 43
691 11844 -90 03 <A(1) 11 3350 43
692 11848 -88 13 (3)B> 11 3350 43
693 11850 -86 13 33 (3)B> 3350 43
694 11854 -84 13 332 (3)A> 3349 43
695 11856 -86 13 332 <A(1) 13 3348 43
696 11860 -90 13 <A(1) 112 13 3348 43
697 11864 -88 33 (3)B> 112 13 3348 43
698 11868 -84 333 (3)B> 13 3348 43
699 11872 -86 333 <A(1) 11 3348 43
700 11878 -92 <A(1) 114 3348 43
701 11880 -90 01 (3)A> 114 3348 43
702 11888 -82 01 334 (3)A> 3348 43
703 11890 -84 01 334 <A(1) 13 3347 43
704 11898 -92 01 <A(1) 114 13 3347 43
705 11900 -90 03 (3)A> 114 13 3347 43
706 11908 -82 03 334 (3)A> 13 3347 43
707 11910 -80 03 335 (2)A> 3347 43
708 11916 -82 03 335 <A(1) 11 3346 43
709 11926 -92 03 <A(1) 116 3346 43
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 03 <A(1) 111+V(2) 335+V(1) [*]*
1 4 2 13 (3)B> 111+V(2) 335+V(1) [*]*
2 6+2*V(2) 4+2*V(2) 13 331+V(2) (3)B> 335+V(1) [*]*
3 10+2*V(2) 6+2*V(2) 13 332+V(2) (3)A> 334+V(1) [*]*
4 12+2*V(2) 4+2*V(2) 13 332+V(2) <A(1) 13 333+V(1) [*]*
5 16+4*V(2) 0 13 <A(1) 112+V(2) 13 333+V(1) [*]*
6 20+4*V(2) 2 33 (3)B> 112+V(2) 13 333+V(1) [*]*
7 24+6*V(2) 6+2*V(2) 333+V(2) (3)B> 13 333+V(1) [*]*
8 28+6*V(2) 4+2*V(2) 333+V(2) <A(1) 11 333+V(1) [*]*
9 34+8*V(2) -2 <A(1) 114+V(2) 333+V(1) [*]*
10 36+8*V(2) 0 01 (3)A> 114+V(2) 333+V(1) [*]*
11 44+10*V(2) 8+2*V(2) 01 334+V(2) (3)A> 333+V(1) [*]*
12 46+10*V(2) 6+2*V(2) 01 334+V(2) <A(1) 13 332+V(1) [*]*
13 54+12*V(2) -2 01 <A(1) 114+V(2) 13 332+V(1) [*]*
14 56+12*V(2) 0 03 (3)A> 114+V(2) 13 332+V(1) [*]*
15 64+14*V(2) 8+2*V(2) 03 334+V(2) (3)A> 13 332+V(1) [*]*
16 66+14*V(2) 10+2*V(2) 03 335+V(2) (2)A> 332+V(1) [*]*
17 72+14*V(2) 8+2*V(2) 03 335+V(2) <A(1) 11 331+V(1) [*]*
18 82+16*V(2) -2 03 <A(1) 116+V(2) 331+V(1) [*]*
<< Success! ==> defined new CTR 6 (PA)
709 11926 -92 03 <A(1) 116 3346 43
== Executing PA-CTR 6, V(1)=41, V(2)=5, repcount=11, factor=5/4
907 18108 -114 03 <A(1) 1161 332 43
908 18112 -112 13 (3)B> 1161 332 43
909 18234 10 13 3361 (3)B> 332 43
910 18238 12 13 3362 (3)A> 33 43
911 18240 10 13 3362 <A(1) 13 43
912 18364 -114 13 <A(1) 1162 13 43
913 18368 -112 33 (3)B> 1162 13 43
914 18492 12 3363 (3)B> 13 43
915 18496 10 3363 <A(1) 11 43
916 18622 -116 <A(1) 1164 43
917 18624 -114 01 (3)A> 1164 43
918 18752 14 01 3364 (3)A> 43
919 18760 12 01 3364 <A(1) 11
920 18888 -116 01 <A(1) 1165
921 18890 -114 03 (3)A> 1165
922 19020 16 03 3365 (3)A>
923 19030 14 03 3365 <B(4) 33
924 19420 -116 03 <B(4) 3366
925 19424 -118 <A(2) 43 3366
926 19432 -116 03 (3)A> 43 3366
927 19440 -118 03 <A(1) 11 3366
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 03 <A(1) 111+V(1) 332 43
1 4 2 13 (3)B> 111+V(1) 332 43
2 6+2*V(1) 4+2*V(1) 13 331+V(1) (3)B> 332 43
3 10+2*V(1) 6+2*V(1) 13 332+V(1) (3)A> 33 43
4 12+2*V(1) 4+2*V(1) 13 332+V(1) <A(1) 13 43
5 16+4*V(1) 0 13 <A(1) 112+V(1) 13 43
6 20+4*V(1) 2 33 (3)B> 112+V(1) 13 43
7 24+6*V(1) 6+2*V(1) 333+V(1) (3)B> 13 43
8 28+6*V(1) 4+2*V(1) 333+V(1) <A(1) 11 43
9 34+8*V(1) -2 <A(1) 114+V(1) 43
10 36+8*V(1) 0 01 (3)A> 114+V(1) 43
11 44+10*V(1) 8+2*V(1) 01 334+V(1) (3)A> 43
12 52+10*V(1) 6+2*V(1) 01 334+V(1) <A(1) 11
13 60+12*V(1) -2 01 <A(1) 115+V(1)
14 62+12*V(1) 0 03 (3)A> 115+V(1)
15 72+14*V(1) 10+2*V(1) 03 335+V(1) (3)A>
16 82+14*V(1) 8+2*V(1) 03 335+V(1) <B(4) 33
17 112+20*V(1) -2 03 <B(4) 336+V(1)
18 116+20*V(1) -4 <A(2) 43 336+V(1)
19 124+20*V(1) -2 03 (3)A> 43 336+V(1)
20 132+20*V(1) -4 03 <A(1) 11 336+V(1)
<< Success! ==> defined new CTR 7 (PPA)
927 19440 -118 03 <A(1) 11 3366
== Executing PA-CTR 2, V(1)=61, V(2)=0, repcount=16, factor=5/4
1215 30352 -150 03 <A(1) 1181 332
1216 30356 -148 13 (3)B> 1181 332
1217 30518 14 13 3381 (3)B> 332
1218 30522 16 13 3382 (3)A> 33
1219 30524 14 13 3382 <A(1) 13
1220 30688 -150 13 <A(1) 1182 13
1221 30692 -148 33 (3)B> 1182 13
1222 30856 16 3383 (3)B> 13
1223 30860 14 3383 <A(1) 11
1224 31026 -152 <A(1) 1184
1225 31028 -150 01 (3)A> 1184
1226 31196 18 01 3384 (3)A>
1227 31206 16 01 3384 <B(4) 33
1228 31710 -152 01 <B(4) 3385
1229 31716 -150 03 (3)A> 3385
1230 31718 -152 03 <A(1) 13 3384
1231 31722 -150 13 (3)B> 13 3384
1232 31726 -152 13 <A(1) 11 3384
1233 31730 -150 33 (3)B> 11 3384
1234 31732 -148 332 (3)B> 3384
1235 31736 -146 333 (3)A> 3383
1236 31738 -148 333 <A(1) 13 3382
1237 31744 -154 <A(1) 113 13 3382
1238 31746 -152 01 (3)A> 113 13 3382
1239 31752 -146 01 333 (3)A> 13 3382
1240 31754 -144 01 334 (2)A> 3382
1241 31760 -146 01 334 <A(1) 11 3381
1242 31768 -154 01 <A(1) 115 3381
1243 31770 -152 03 (3)A> 115 3381
1244 31780 -142 03 335 (3)A> 3381
1245 31782 -144 03 335 <A(1) 13 3380
1246 31792 -154 03 <A(1) 115 13 3380
1247 31796 -152 13 (3)B> 115 13 3380
1248 31806 -142 13 335 (3)B> 13 3380
1249 31810 -144 13 335 <A(1) 11 3380
1250 31820 -154 13 <A(1) 116 3380
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 13 <A(1) 111+V(2) 335+V(1)
1 4 2 33 (3)B> 111+V(2) 335+V(1)
2 6+2*V(2) 4+2*V(2) 332+V(2) (3)B> 335+V(1)
3 10+2*V(2) 6+2*V(2) 333+V(2) (3)A> 334+V(1)
4 12+2*V(2) 4+2*V(2) 333+V(2) <A(1) 13 333+V(1)
5 18+4*V(2) -2 <A(1) 113+V(2) 13 333+V(1)
6 20+4*V(2) 0 01 (3)A> 113+V(2) 13 333+V(1)
7 26+6*V(2) 6+2*V(2) 01 333+V(2) (3)A> 13 333+V(1)
8 28+6*V(2) 8+2*V(2) 01 334+V(2) (2)A> 333+V(1)
9 34+6*V(2) 6+2*V(2) 01 334+V(2) <A(1) 11 332+V(1)
10 42+8*V(2) -2 01 <A(1) 115+V(2) 332+V(1)
11 44+8*V(2) 0 03 (3)A> 115+V(2) 332+V(1)
12 54+10*V(2) 10+2*V(2) 03 335+V(2) (3)A> 332+V(1)
13 56+10*V(2) 8+2*V(2) 03 335+V(2) <A(1) 13 331+V(1)
14 66+12*V(2) -2 03 <A(1) 115+V(2) 13 331+V(1)
15 70+12*V(2) 0 13 (3)B> 115+V(2) 13 331+V(1)
16 80+14*V(2) 10+2*V(2) 13 335+V(2) (3)B> 13 331+V(1)
17 84+14*V(2) 8+2*V(2) 13 335+V(2) <A(1) 11 331+V(1)
18 94+16*V(2) -2 13 <A(1) 116+V(2) 331+V(1)
<< Success! ==> defined new CTR 8 (PA)
1250 31820 -154 13 <A(1) 116 3380
== Executing PA-CTR 8, V(1)=75, V(2)=5, repcount=19, factor=5/4
1592 48806 -192 13 <A(1) 11101 334
1593 48810 -190 33 (3)B> 11101 334
1594 49012 12 33102 (3)B> 334
1595 49016 14 33103 (3)A> 333
1596 49018 12 33103 <A(1) 13 332
1597 49224 -194 <A(1) 11103 13 332
1598 49226 -192 01 (3)A> 11103 13 332
1599 49432 14 01 33103 (3)A> 13 332
1600 49434 16 01 33104 (2)A> 332
1601 49440 14 01 33104 <A(1) 11 33
1602 49648 -194 01 <A(1) 11105 33
1603 49650 -192 03 (3)A> 11105 33
1604 49860 18 03 33105 (3)A> 33
1605 49862 16 03 33105 <A(1) 13
1606 50072 -194 03 <A(1) 11105 13
1607 50076 -192 13 (3)B> 11105 13
1608 50286 18 13 33105 (3)B> 13
1609 50290 16 13 33105 <A(1) 11
1610 50500 -194 13 <A(1) 11106
1611 50504 -192 33 (3)B> 11106
1612 50716 20 33107 (3)B>
1613 50718 18 33107 <A(1) 20
1614 50932 -196 <A(1) 11107 20
1615 50934 -194 01 (3)A> 11107 20
1616 51148 20 01 33107 (3)A> 20
1617 51152 18 01 33107 <A(1) 12
1618 51366 -196 01 <A(1) 11107 12
1619 51368 -194 03 (3)A> 11107 12
1620 51582 20 03 33107 (3)A> 12
1621 51590 18 03 33107 <B(4) 33
1622 52232 -196 03 <B(4) 33108
1623 52236 -198 <A(2) 43 33108
1624 52244 -196 03 (3)A> 43 33108
1625 52252 -198 03 <A(1) 11 33108
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 13 <A(1) 111+V(1) 334
1 4 2 33 (3)B> 111+V(1) 334
2 6+2*V(1) 4+2*V(1) 332+V(1) (3)B> 334
3 10+2*V(1) 6+2*V(1) 333+V(1) (3)A> 333
4 12+2*V(1) 4+2*V(1) 333+V(1) <A(1) 13 332
5 18+4*V(1) -2 <A(1) 113+V(1) 13 332
6 20+4*V(1) 0 01 (3)A> 113+V(1) 13 332
7 26+6*V(1) 6+2*V(1) 01 333+V(1) (3)A> 13 332
8 28+6*V(1) 8+2*V(1) 01 334+V(1) (2)A> 332
9 34+6*V(1) 6+2*V(1) 01 334+V(1) <A(1) 11 33
10 42+8*V(1) -2 01 <A(1) 115+V(1) 33
11 44+8*V(1) 0 03 (3)A> 115+V(1) 33
12 54+10*V(1) 10+2*V(1) 03 335+V(1) (3)A> 33
13 56+10*V(1) 8+2*V(1) 03 335+V(1) <A(1) 13
14 66+12*V(1) -2 03 <A(1) 115+V(1) 13
15 70+12*V(1) 0 13 (3)B> 115+V(1) 13
16 80+14*V(1) 10+2*V(1) 13 335+V(1) (3)B> 13
17 84+14*V(1) 8+2*V(1) 13 335+V(1) <A(1) 11
18 94+16*V(1) -2 13 <A(1) 116+V(1)
19 98+16*V(1) 0 33 (3)B> 116+V(1)
20 110+18*V(1) 12+2*V(1) 337+V(1) (3)B>
21 112+18*V(1) 10+2*V(1) 337+V(1) <A(1) 20
22 126+20*V(1) -4 <A(1) 117+V(1) 20
23 128+20*V(1) -2 01 (3)A> 117+V(1) 20
24 142+22*V(1) 12+2*V(1) 01 337+V(1) (3)A> 20
25 146+22*V(1) 10+2*V(1) 01 337+V(1) <A(1) 12
26 160+24*V(1) -4 01 <A(1) 117+V(1) 12
27 162+24*V(1) -2 03 (3)A> 117+V(1) 12
28 176+26*V(1) 12+2*V(1) 03 337+V(1) (3)A> 12
29 184+26*V(1) 10+2*V(1) 03 337+V(1) <B(4) 33
30 226+32*V(1) -4 03 <B(4) 338+V(1)
31 230+32*V(1) -6 <A(2) 43 338+V(1)
32 238+32*V(1) -4 03 (3)A> 43 338+V(1)
33 246+32*V(1) -6 03 <A(1) 11 338+V(1)
<< Success! ==> defined new CTR 9 (PPA)
1625 52252 -198 03 <A(1) 11 33108
== Executing PA-CTR 2, V(1)=103, V(2)=0, repcount=26, factor=5/4
2093 80384 -250 03 <A(1) 11131 334
== Executing PPA-CTR 3 (once), V(1)=130
2120 84212 -252 33 (3)A> 33137 30
== Executing PA-CTR 1, V(1)=0, V(2)=132, repcount=34, factor=5/4
2732 131540 20 33171 (3)A> 33 30
== Executing PPA-CTR 4 (once), V(1)=166
2747 133304 -318 333 (3)A> 33171 30
== Executing PA-CTR 1, V(1)=2, V(2)=166, repcount=42, factor=5/4
3503 206552 18 33213 (3)A> 333 30
3504 206554 16 33213 <A(1) 13 332 30
3505 206980 -410 <A(1) 11213 13 332 30
3506 206982 -408 01 (3)A> 11213 13 332 30
3507 207408 18 01 33213 (3)A> 13 332 30
3508 207410 20 01 33214 (2)A> 332 30
3509 207416 18 01 33214 <A(1) 11 33 30
3510 207844 -410 01 <A(1) 11215 33 30
3511 207846 -408 03 (3)A> 11215 33 30
3512 208276 22 03 33215 (3)A> 33 30
3513 208278 20 03 33215 <A(1) 13 30
3514 208708 -410 03 <A(1) 11215 13 30
3515 208712 -408 13 (3)B> 11215 13 30
3516 209142 22 13 33215 (3)B> 13 30
3517 209146 20 13 33215 <A(1) 11 30
3518 209576 -410 13 <A(1) 11216 30
3519 209580 -408 33 (3)B> 11216 30
3520 210012 24 33217 (3)B> 30
3521 210014 26 33217 32 (1)B>
3522 210020 24 33217 32 <B(4) 30
3523 210024 22 33217 <B(4) 34 30
3524 211326 -412 <B(4) 33217 34 30
3525 211340 -410 33 (3)A> 33217 34 30
3526 211342 -412 33 <A(1) 13 33216 34 30
3527 211344 -414 <A(1) 11 13 33216 34 30
3528 211346 -412 01 (3)A> 11 13 33216 34 30
3529 211348 -410 01 33 (3)A> 13 33216 34 30
3530 211350 -408 01 332 (2)A> 33216 34 30
3531 211356 -410 01 332 <A(1) 11 33215 34 30
3532 211360 -414 01 <A(1) 113 33215 34 30
3533 211362 -412 03 (3)A> 113 33215 34 30
3534 211368 -406 03 333 (3)A> 33215 34 30
3535 211370 -408 03 333 <A(1) 13 33214 34 30
3536 211376 -414 03 <A(1) 113 13 33214 34 30
3537 211380 -412 13 (3)B> 113 13 33214 34 30
3538 211386 -406 13 333 (3)B> 13 33214 34 30
3539 211390 -408 13 333 <A(1) 11 33214 34 30
3540 211396 -414 13 <A(1) 114 33214 34 30
3541 211400 -412 33 (3)B> 114 33214 34 30
3542 211408 -404 335 (3)B> 33214 34 30
3543 211412 -402 336 (3)A> 33213 34 30
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 331+V(1) (3)A> 335+V(2) [*]* [*]*
1 2 -2 331+V(1) <A(1) 13 334+V(2) [*]* [*]*
2 4+2*V(1) -4+-2*V(1) <A(1) 111+V(1) 13 334+V(2) [*]* [*]*
3 6+2*V(1) -2+-2*V(1) 01 (3)A> 111+V(1) 13 334+V(2) [*]* [*]*
4 8+4*V(1) 0 01 331+V(1) (3)A> 13 334+V(2) [*]* [*]*
5 10+4*V(1) 2 01 332+V(1) (2)A> 334+V(2) [*]* [*]*
6 16+4*V(1) 0 01 332+V(1) <A(1) 11 333+V(2) [*]* [*]*
7 20+6*V(1) -4+-2*V(1) 01 <A(1) 113+V(1) 333+V(2) [*]* [*]*
8 22+6*V(1) -2+-2*V(1) 03 (3)A> 113+V(1) 333+V(2) [*]* [*]*
9 28+8*V(1) 4 03 333+V(1) (3)A> 333+V(2) [*]* [*]*
10 30+8*V(1) 2 03 333+V(1) <A(1) 13 332+V(2) [*]* [*]*
11 36+10*V(1) -4+-2*V(1) 03 <A(1) 113+V(1) 13 332+V(2) [*]* [*]*
12 40+10*V(1) -2+-2*V(1) 13 (3)B> 113+V(1) 13 332+V(2) [*]* [*]*
13 46+12*V(1) 4 13 333+V(1) (3)B> 13 332+V(2) [*]* [*]*
14 50+12*V(1) 2 13 333+V(1) <A(1) 11 332+V(2) [*]* [*]*
15 56+14*V(1) -4+-2*V(1) 13 <A(1) 114+V(1) 332+V(2) [*]* [*]*
16 60+14*V(1) -2+-2*V(1) 33 (3)B> 114+V(1) 332+V(2) [*]* [*]*
17 68+16*V(1) 6 335+V(1) (3)B> 332+V(2) [*]* [*]*
18 72+16*V(1) 8 336+V(1) (3)A> 331+V(2) [*]* [*]*
<< Success! ==> defined new CTR 10 (PA)
3543 211412 -402 336 (3)A> 33213 34 30
== Executing PA-CTR 10, V(1)=5, V(2)=208, repcount=53, factor=5/4
4497 329708 22 33271 (3)A> 33 34 30
4498 329710 20 33271 <A(1) 13 34 30
4499 330252 -522 <A(1) 11271 13 34 30
4500 330254 -520 01 (3)A> 11271 13 34 30
4501 330796 22 01 33271 (3)A> 13 34 30
4502 330798 24 01 33272 (2)A> 34 30
4503 330806 26 01 33273 (3)A> 30
4504 330808 24 01 33273 <A(1) 10
4505 331354 -522 01 <A(1) 11273 10
4506 331356 -520 03 (3)A> 11273 10
4507 331902 26 03 33273 (3)A> 10
4508 331906 24 03 33273 <A(1) 12
4509 332452 -522 03 <A(1) 11273 12
4510 332456 -520 13 (3)B> 11273 12
4511 333002 26 13 33273 (3)B> 12
4512 333004 28 13 33274 (3)B>
4513 333006 26 13 33274 <A(1) 20
4514 333554 -522 13 <A(1) 11274 20
4515 333558 -520 33 (3)B> 11274 20
4516 334106 28 33275 (3)B> 20
4517 334110 26 33275 <B(4) 30
4518 335760 -524 <B(4) 33275 30
4519 335774 -522 33 (3)A> 33275 30
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 331+V(1) (3)A> 33 34 30
1 2 -2 331+V(1) <A(1) 13 34 30
2 4+2*V(1) -4+-2*V(1) <A(1) 111+V(1) 13 34 30
3 6+2*V(1) -2+-2*V(1) 01 (3)A> 111+V(1) 13 34 30
4 8+4*V(1) 0 01 331+V(1) (3)A> 13 34 30
5 10+4*V(1) 2 01 332+V(1) (2)A> 34 30
6 18+4*V(1) 4 01 333+V(1) (3)A> 30
7 20+4*V(1) 2 01 333+V(1) <A(1) 10
8 26+6*V(1) -4+-2*V(1) 01 <A(1) 113+V(1) 10
9 28+6*V(1) -2+-2*V(1) 03 (3)A> 113+V(1) 10
10 34+8*V(1) 4 03 333+V(1) (3)A> 10
11 38+8*V(1) 2 03 333+V(1) <A(1) 12
12 44+10*V(1) -4+-2*V(1) 03 <A(1) 113+V(1) 12
13 48+10*V(1) -2+-2*V(1) 13 (3)B> 113+V(1) 12
14 54+12*V(1) 4 13 333+V(1) (3)B> 12
15 56+12*V(1) 6 13 334+V(1) (3)B>
16 58+12*V(1) 4 13 334+V(1) <A(1) 20
17 66+14*V(1) -4+-2*V(1) 13 <A(1) 114+V(1) 20
18 70+14*V(1) -2+-2*V(1) 33 (3)B> 114+V(1) 20
19 78+16*V(1) 6 335+V(1) (3)B> 20
20 82+16*V(1) 4 335+V(1) <B(4) 30
21 112+22*V(1) -6+-2*V(1) <B(4) 335+V(1) 30
22 126+22*V(1) -4+-2*V(1) 33 (3)A> 335+V(1) 30
<< Success! ==> defined new CTR 11 (PPA)
4519 335774 -522 33 (3)A> 33275 30
== Executing PA-CTR 1, V(1)=0, V(2)=270, repcount=68, factor=5/4
5743 522910 22 33341 (3)A> 333 30
5744 522912 20 33341 <A(1) 13 332 30
5745 523594 -662 <A(1) 11341 13 332 30
5746 523596 -660 01 (3)A> 11341 13 332 30
5747 524278 22 01 33341 (3)A> 13 332 30
5748 524280 24 01 33342 (2)A> 332 30
5749 524286 22 01 33342 <A(1) 11 33 30
5750 524970 -662 01 <A(1) 11343 33 30
5751 524972 -660 03 (3)A> 11343 33 30
5752 525658 26 03 33343 (3)A> 33 30
5753 525660 24 03 33343 <A(1) 13 30
5754 526346 -662 03 <A(1) 11343 13 30
5755 526350 -660 13 (3)B> 11343 13 30
5756 527036 26 13 33343 (3)B> 13 30
5757 527040 24 13 33343 <A(1) 11 30
5758 527726 -662 13 <A(1) 11344 30
5759 527730 -660 33 (3)B> 11344 30
5760 528418 28 33345 (3)B> 30
5761 528420 30 33345 32 (1)B>
5762 528426 28 33345 32 <B(4) 30
5763 528430 26 33345 <B(4) 34 30
5764 530500 -664 <B(4) 33345 34 30
5765 530514 -662 33 (3)A> 33345 34 30
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 331+V(1) (3)A> 333 30
1 2 -2 331+V(1) <A(1) 13 332 30
2 4+2*V(1) -4+-2*V(1) <A(1) 111+V(1) 13 332 30
3 6+2*V(1) -2+-2*V(1) 01 (3)A> 111+V(1) 13 332 30
4 8+4*V(1) 0 01 331+V(1) (3)A> 13 332 30
5 10+4*V(1) 2 01 332+V(1) (2)A> 332 30
6 16+4*V(1) 0 01 332+V(1) <A(1) 11 33 30
7 20+6*V(1) -4+-2*V(1) 01 <A(1) 113+V(1) 33 30
8 22+6*V(1) -2+-2*V(1) 03 (3)A> 113+V(1) 33 30
9 28+8*V(1) 4 03 333+V(1) (3)A> 33 30
10 30+8*V(1) 2 03 333+V(1) <A(1) 13 30
11 36+10*V(1) -4+-2*V(1) 03 <A(1) 113+V(1) 13 30
12 40+10*V(1) -2+-2*V(1) 13 (3)B> 113+V(1) 13 30
13 46+12*V(1) 4 13 333+V(1) (3)B> 13 30
14 50+12*V(1) 2 13 333+V(1) <A(1) 11 30
15 56+14*V(1) -4+-2*V(1) 13 <A(1) 114+V(1) 30
16 60+14*V(1) -2+-2*V(1) 33 (3)B> 114+V(1) 30
17 68+16*V(1) 6 335+V(1) (3)B> 30
18 70+16*V(1) 8 335+V(1) 32 (1)B>
19 76+16*V(1) 6 335+V(1) 32 <B(4) 30
20 80+16*V(1) 4 335+V(1) <B(4) 34 30
21 110+22*V(1) -6+-2*V(1) <B(4) 335+V(1) 34 30
22 124+22*V(1) -4+-2*V(1) 33 (3)A> 335+V(1) 34 30
<< Success! ==> defined new CTR 12 (PPA)
5765 530514 -662 33 (3)A> 33345 34 30
== Executing PA-CTR 10, V(1)=0, V(2)=340, repcount=86, factor=5/4
7313 829106 26 33431 (3)A> 33 34 30
== Executing PPA-CTR 11 (once), V(1)=430
7335 838692 -838 33 (3)A> 33435 30
== Executing PA-CTR 1, V(1)=0, V(2)=430, repcount=108, factor=5/4
9279 1308708 26 33541 (3)A> 333 30
== Executing PPA-CTR 12 (once), V(1)=540
9301 1320712 -1058 33 (3)A> 33545 34 30
== Executing PA-CTR 10, V(1)=0, V(2)=540, repcount=136, factor=5/4
11749 2064904 30 33681 (3)A> 33 34 30
== Executing PPA-CTR 11 (once), V(1)=680
11771 2079990 -1334 33 (3)A> 33685 30
== Executing PA-CTR 1, V(1)=0, V(2)=680, repcount=171, factor=5/4
14849 3255102 34 33856 (3)A> 33 30
== Executing PPA-CTR 4 (once), V(1)=851
14864 3263716 -1674 333 (3)A> 33856 30
== Executing PA-CTR 1, V(1)=2, V(2)=851, repcount=213, factor=5/4
18698 5092108 30 331068 (3)A> 334 30
== Executing PPA-CTR 5 (once), V(1)=1067
18729 5124312 -2112 03 <A(1) 11 331074
== Executing PA-CTR 2, V(1)=1069, V(2)=0, repcount=268, factor=5/4
23553 8008528 -2648 03 <A(1) 111341 332
23554 8008532 -2646 13 (3)B> 111341 332
23555 8011214 36 13 331341 (3)B> 332
23556 8011218 38 13 331342 (3)A> 33
23557 8011220 36 13 331342 <A(1) 13
23558 8013904 -2648 13 <A(1) 111342 13
23559 8013908 -2646 33 (3)B> 111342 13
23560 8016592 38 331343 (3)B> 13
23561 8016596 36 331343 <A(1) 11
23562 8019282 -2650 <A(1) 111344
23563 8019284 -2648 01 (3)A> 111344
23564 8021972 40 01 331344 (3)A>
23565 8021982 38 01 331344 <B(4) 33
23566 8030046 -2650 01 <B(4) 331345
23567 8030052 -2648 03 (3)A> 331345
23568 8030054 -2650 03 <A(1) 13 331344
23569 8030058 -2648 13 (3)B> 13 331344
23570 8030062 -2650 13 <A(1) 11 331344
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 03 <A(1) 112+V(1) 332
1 4 2 13 (3)B> 112+V(1) 332
2 8+2*V(1) 6+2*V(1) 13 332+V(1) (3)B> 332
3 12+2*V(1) 8+2*V(1) 13 333+V(1) (3)A> 33
4 14+2*V(1) 6+2*V(1) 13 333+V(1) <A(1) 13
5 20+4*V(1) 0 13 <A(1) 113+V(1) 13
6 24+4*V(1) 2 33 (3)B> 113+V(1) 13
7 30+6*V(1) 8+2*V(1) 334+V(1) (3)B> 13
8 34+6*V(1) 6+2*V(1) 334+V(1) <A(1) 11
9 42+8*V(1) -2 <A(1) 115+V(1)
10 44+8*V(1) 0 01 (3)A> 115+V(1)
11 54+10*V(1) 10+2*V(1) 01 335+V(1) (3)A>
12 64+10*V(1) 8+2*V(1) 01 335+V(1) <B(4) 33
13 94+16*V(1) -2 01 <B(4) 336+V(1)
14 100+16*V(1) 0 03 (3)A> 336+V(1)
15 102+16*V(1) -2 03 <A(1) 13 335+V(1)
16 106+16*V(1) 0 13 (3)B> 13 335+V(1)
17 110+16*V(1) -2 13 <A(1) 11 335+V(1)
<< Success! ==> defined new CTR 13 (PPA)
23570 8030062 -2650 13 <A(1) 11 331344
== Executing PA-CTR 8, V(1)=1339, V(2)=0, repcount=335, factor=5/4
29600 12537152 -3320 13 <A(1) 111676 334
== Executing PPA-CTR 9 (once), V(1)=1675
29633 12590998 -3326 03 <A(1) 11 331683
== Executing PA-CTR 2, V(1)=1678, V(2)=0, repcount=420, factor=5/4
37193 19664638 -4166 03 <A(1) 112101 333
37194 19664642 -4164 13 (3)B> 112101 333
37195 19668844 38 13 332101 (3)B> 333
37196 19668848 40 13 332102 (3)A> 332
37197 19668850 38 13 332102 <A(1) 13 33
37198 19673054 -4166 13 <A(1) 112102 13 33
37199 19673058 -4164 33 (3)B> 112102 13 33
37200 19677262 40 332103 (3)B> 13 33
37201 19677266 38 332103 <A(1) 11 33
37202 19681472 -4168 <A(1) 112104 33
37203 19681474 -4166 01 (3)A> 112104 33
37204 19685682 42 01 332104 (3)A> 33
37205 19685684 40 01 332104 <A(1) 13
37206 19689892 -4168 01 <A(1) 112104 13
37207 19689894 -4166 03 (3)A> 112104 13
37208 19694102 42 03 332104 (3)A> 13
37209 19694104 44 03 332105 (2)A>
37210 19694112 42 03 332105 <B(4) 43
37211 19706742 -4168 03 <B(4) 332105 43
37212 19706746 -4170 <A(2) 43 332105 43
37213 19706754 -4168 03 (3)A> 43 332105 43
37214 19706762 -4170 03 <A(1) 11 332105 43
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 03 <A(1) 111+V(1) 333
1 4 2 13 (3)B> 111+V(1) 333
2 6+2*V(1) 4+2*V(1) 13 331+V(1) (3)B> 333
3 10+2*V(1) 6+2*V(1) 13 332+V(1) (3)A> 332
4 12+2*V(1) 4+2*V(1) 13 332+V(1) <A(1) 13 33
5 16+4*V(1) 0 13 <A(1) 112+V(1) 13 33
6 20+4*V(1) 2 33 (3)B> 112+V(1) 13 33
7 24+6*V(1) 6+2*V(1) 333+V(1) (3)B> 13 33
8 28+6*V(1) 4+2*V(1) 333+V(1) <A(1) 11 33
9 34+8*V(1) -2 <A(1) 114+V(1) 33
10 36+8*V(1) 0 01 (3)A> 114+V(1) 33
11 44+10*V(1) 8+2*V(1) 01 334+V(1) (3)A> 33
12 46+10*V(1) 6+2*V(1) 01 334+V(1) <A(1) 13
13 54+12*V(1) -2 01 <A(1) 114+V(1) 13
14 56+12*V(1) 0 03 (3)A> 114+V(1) 13
15 64+14*V(1) 8+2*V(1) 03 334+V(1) (3)A> 13
16 66+14*V(1) 10+2*V(1) 03 335+V(1) (2)A>
17 74+14*V(1) 8+2*V(1) 03 335+V(1) <B(4) 43
18 104+20*V(1) -2 03 <B(4) 335+V(1) 43
19 108+20*V(1) -4 <A(2) 43 335+V(1) 43
20 116+20*V(1) -2 03 (3)A> 43 335+V(1) 43
21 124+20*V(1) -4 03 <A(1) 11 335+V(1) 43
<< Success! ==> defined new CTR 14 (PPA)
37214 19706762 -4170 03 <A(1) 11 332105 43
== Executing PA-CTR 6, V(1)=2100, V(2)=0, repcount=526, factor=5/4
46682 30795894 -5222 03 <A(1) 112631 33 43
46683 30795898 -5220 13 (3)B> 112631 33 43
46684 30801160 42 13 332631 (3)B> 33 43
46685 30801164 44 13 332632 (3)A> 43
46686 30801172 42 13 332632 <A(1) 11
46687 30806436 -5222 13 <A(1) 112633
46688 30806440 -5220 33 (3)B> 112633
46689 30811706 46 332634 (3)B>
46690 30811708 44 332634 <A(1) 20
46691 30816976 -5224 <A(1) 112634 20
46692 30816978 -5222 01 (3)A> 112634 20
46693 30822246 46 01 332634 (3)A> 20
46694 30822250 44 01 332634 <A(1) 12
46695 30827518 -5224 01 <A(1) 112634 12
46696 30827520 -5222 03 (3)A> 112634 12
46697 30832788 46 03 332634 (3)A> 12
46698 30832796 44 03 332634 <B(4) 33
46699 30848600 -5224 03 <B(4) 332635
46700 30848604 -5226 <A(2) 43 332635
46701 30848612 -5224 03 (3)A> 43 332635
46702 30848620 -5226 03 <A(1) 11 332635
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 03 <A(1) 111+V(1) 33 43
1 4 2 13 (3)B> 111+V(1) 33 43
2 6+2*V(1) 4+2*V(1) 13 331+V(1) (3)B> 33 43
3 10+2*V(1) 6+2*V(1) 13 332+V(1) (3)A> 43
4 18+2*V(1) 4+2*V(1) 13 332+V(1) <A(1) 11
5 22+4*V(1) 0 13 <A(1) 113+V(1)
6 26+4*V(1) 2 33 (3)B> 113+V(1)
7 32+6*V(1) 8+2*V(1) 334+V(1) (3)B>
8 34+6*V(1) 6+2*V(1) 334+V(1) <A(1) 20
9 42+8*V(1) -2 <A(1) 114+V(1) 20
10 44+8*V(1) 0 01 (3)A> 114+V(1) 20
11 52+10*V(1) 8+2*V(1) 01 334+V(1) (3)A> 20
12 56+10*V(1) 6+2*V(1) 01 334+V(1) <A(1) 12
13 64+12*V(1) -2 01 <A(1) 114+V(1) 12
14 66+12*V(1) 0 03 (3)A> 114+V(1) 12
15 74+14*V(1) 8+2*V(1) 03 334+V(1) (3)A> 12
16 82+14*V(1) 6+2*V(1) 03 334+V(1) <B(4) 33
17 106+20*V(1) -2 03 <B(4) 335+V(1)
18 110+20*V(1) -4 <A(2) 43 335+V(1)
19 118+20*V(1) -2 03 (3)A> 43 335+V(1)
20 126+20*V(1) -4 03 <A(1) 11 335+V(1)
<< Success! ==> defined new CTR 15 (PPA)
46702 30848620 -5226 03 <A(1) 11 332635
== Executing PA-CTR 2, V(1)=2630, V(2)=0, repcount=658, factor=5/4
58546 48194816 -6542 03 <A(1) 113291 333
== Executing PPA-CTR 14 (once), V(1)=3290
58567 48260740 -6546 03 <A(1) 11 333295 43
== Executing PA-CTR 6, V(1)=3290, V(2)=0, repcount=823, factor=5/4
73381 75388466 -8192 03 <A(1) 114116 333 43
73382 75388470 -8190 13 (3)B> 114116 333 43
73383 75396702 42 13 334116 (3)B> 333 43
73384 75396706 44 13 334117 (3)A> 332 43
73385 75396708 42 13 334117 <A(1) 13 33 43
73386 75404942 -8192 13 <A(1) 114117 13 33 43
73387 75404946 -8190 33 (3)B> 114117 13 33 43
73388 75413180 44 334118 (3)B> 13 33 43
73389 75413184 42 334118 <A(1) 11 33 43
73390 75421420 -8194 <A(1) 114119 33 43
73391 75421422 -8192 01 (3)A> 114119 33 43
73392 75429660 46 01 334119 (3)A> 33 43
73393 75429662 44 01 334119 <A(1) 13 43
73394 75437900 -8194 01 <A(1) 114119 13 43
73395 75437902 -8192 03 (3)A> 114119 13 43
73396 75446140 46 03 334119 (3)A> 13 43
73397 75446142 48 03 334120 (2)A> 43
73398 75446144 46 03 334120 <B(4) 33
73399 75470864 -8194 03 <B(4) 334121
73400 75470868 -8196 <A(2) 43 334121
73401 75470876 -8194 03 (3)A> 43 334121
73402 75470884 -8196 03 <A(1) 11 334121
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 03 <A(1) 111+V(1) 333 43
1 4 2 13 (3)B> 111+V(1) 333 43
2 6+2*V(1) 4+2*V(1) 13 331+V(1) (3)B> 333 43
3 10+2*V(1) 6+2*V(1) 13 332+V(1) (3)A> 332 43
4 12+2*V(1) 4+2*V(1) 13 332+V(1) <A(1) 13 33 43
5 16+4*V(1) 0 13 <A(1) 112+V(1) 13 33 43
6 20+4*V(1) 2 33 (3)B> 112+V(1) 13 33 43
7 24+6*V(1) 6+2*V(1) 333+V(1) (3)B> 13 33 43
8 28+6*V(1) 4+2*V(1) 333+V(1) <A(1) 11 33 43
9 34+8*V(1) -2 <A(1) 114+V(1) 33 43
10 36+8*V(1) 0 01 (3)A> 114+V(1) 33 43
11 44+10*V(1) 8+2*V(1) 01 334+V(1) (3)A> 33 43
12 46+10*V(1) 6+2*V(1) 01 334+V(1) <A(1) 13 43
13 54+12*V(1) -2 01 <A(1) 114+V(1) 13 43
14 56+12*V(1) 0 03 (3)A> 114+V(1) 13 43
15 64+14*V(1) 8+2*V(1) 03 334+V(1) (3)A> 13 43
16 66+14*V(1) 10+2*V(1) 03 335+V(1) (2)A> 43
17 68+14*V(1) 8+2*V(1) 03 335+V(1) <B(4) 33
18 98+20*V(1) -2 03 <B(4) 336+V(1)
19 102+20*V(1) -4 <A(2) 43 336+V(1)
20 110+20*V(1) -2 03 (3)A> 43 336+V(1)
21 118+20*V(1) -4 03 <A(1) 11 336+V(1)
<< Success! ==> defined new CTR 16 (PPA)
73402 75470884 -8196 03 <A(1) 11 334121
== Executing PA-CTR 2, V(1)=4116, V(2)=0, repcount=1030, factor=5/4
91942 117950144 -10256 03 <A(1) 115151 33
91943 117950148 -10254 13 (3)B> 115151 33
91944 117960450 48 13 335151 (3)B> 33
91945 117960454 50 13 335152 (3)A>
91946 117960464 48 13 335152 <B(4) 33
91947 117991376 -10256 13 <B(4) 335153
91948 117991388 -10258 <A(1) 11 335153
91949 117991390 -10256 01 (3)A> 11 335153
91950 117991392 -10254 01 33 (3)A> 335153
91951 117991394 -10256 01 33 <A(1) 13 335152
91952 117991396 -10258 01 <A(1) 11 13 335152
91953 117991398 -10256 03 (3)A> 11 13 335152
91954 117991400 -10254 03 33 (3)A> 13 335152
91955 117991402 -10252 03 332 (2)A> 335152
91956 117991408 -10254 03 332 <A(1) 11 335151
91957 117991412 -10258 03 <A(1) 113 335151
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 03 <A(1) 115+V(1) 33
1 4 2 13 (3)B> 115+V(1) 33
2 14+2*V(1) 12+2*V(1) 13 335+V(1) (3)B> 33
3 18+2*V(1) 14+2*V(1) 13 336+V(1) (3)A>
4 28+2*V(1) 12+2*V(1) 13 336+V(1) <B(4) 33
5 64+8*V(1) 0 13 <B(4) 337+V(1)
6 76+8*V(1) -2 <A(1) 11 337+V(1)
7 78+8*V(1) 0 01 (3)A> 11 337+V(1)
8 80+8*V(1) 2 01 33 (3)A> 337+V(1)
9 82+8*V(1) 0 01 33 <A(1) 13 336+V(1)
10 84+8*V(1) -2 01 <A(1) 11 13 336+V(1)
11 86+8*V(1) 0 03 (3)A> 11 13 336+V(1)
12 88+8*V(1) 2 03 33 (3)A> 13 336+V(1)
13 90+8*V(1) 4 03 332 (2)A> 336+V(1)
14 96+8*V(1) 2 03 332 <A(1) 11 335+V(1)
15 100+8*V(1) -2 03 <A(1) 113 335+V(1)
<< Success! ==> defined new CTR 17 (PPA)
91957 117991412 -10258 03 <A(1) 113 335151
== Executing PA-CTR 2, V(1)=5146, V(2)=2, repcount=1287, factor=5/4
115123 184341410 -12832 03 <A(1) 116438 333
== Executing PPA-CTR 14 (once), V(1)=6437
115144 184470274 -12836 03 <A(1) 11 336442 43
== Executing PA-CTR 6, V(1)=6437, V(2)=0, repcount=1610, factor=5/4
144124 288221894 -16056 03 <A(1) 118051 332 43
== Executing PPA-CTR 7 (once), V(1)=8050
144144 288383026 -16060 03 <A(1) 11 338056
== Executing PA-CTR 2, V(1)=8051, V(2)=0, repcount=2013, factor=5/4
180378 450554332 -20086 03 <A(1) 1110066 334
== Executing PPA-CTR 3 (once), V(1)=10065
180405 450836340 -20088 33 (3)A> 3310072 30
== Executing PA-CTR 1, V(1)=0, V(2)=10067, repcount=2517, factor=5/4
225711 704328444 48 3312586 (3)A> 334 30
== Executing PPA-CTR 5 (once), V(1)=12585
225742 704706188 -25130 03 <A(1) 11 3312592
== Executing PA-CTR 2, V(1)=12587, V(2)=0, repcount=3147, factor=5/4
282388 1100982722 -31424 03 <A(1) 1115736 334
== Executing PPA-CTR 3 (once), V(1)=15735
282415 1101423490 -31426 33 (3)A> 3315742 30
== Executing PA-CTR 1, V(1)=0, V(2)=15737, repcount=3935, factor=5/4
353245 1720918410 54 3319676 (3)A> 332 30
353246 1720918412 52 3319676 <A(1) 13 33 30
353247 1720957764 -39300 <A(1) 1119676 13 33 30
353248 1720957766 -39298 01 (3)A> 1119676 13 33 30
353249 1720997118 54 01 3319676 (3)A> 13 33 30
353250 1720997120 56 01 3319677 (2)A> 33 30
353251 1720997126 54 01 3319677 <A(1) 11 30
353252 1721036480 -39300 01 <A(1) 1119678 30
353253 1721036482 -39298 03 (3)A> 1119678 30
353254 1721075838 58 03 3319678 (3)A> 30
353255 1721075840 56 03 3319678 <A(1) 10
353256 1721115196 -39300 03 <A(1) 1119678 10
353257 1721115200 -39298 13 (3)B> 1119678 10
353258 1721154556 58 13 3319678 (3)B> 10
353259 1721154558 60 13 3319679 (1)B>
353260 1721154564 58 13 3319679 <B(4) 30
353261 1721272638 -39300 13 <B(4) 3319679 30
353262 1721272650 -39302 <A(1) 11 3319679 30
353263 1721272652 -39300 01 (3)A> 11 3319679 30
353264 1721272654 -39298 01 33 (3)A> 3319679 30
353265 1721272656 -39300 01 33 <A(1) 13 3319678 30
353266 1721272658 -39302 01 <A(1) 11 13 3319678 30
353267 1721272660 -39300 03 (3)A> 11 13 3319678 30
353268 1721272662 -39298 03 33 (3)A> 13 3319678 30
353269 1721272664 -39296 03 332 (2)A> 3319678 30
353270 1721272670 -39298 03 332 <A(1) 11 3319677 30
353271 1721272674 -39302 03 <A(1) 113 3319677 30
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 334+V(1) (3)A> 332 30
1 2 -2 334+V(1) <A(1) 13 33 30
2 10+2*V(1) -10+-2*V(1) <A(1) 114+V(1) 13 33 30
3 12+2*V(1) -8+-2*V(1) 01 (3)A> 114+V(1) 13 33 30
4 20+4*V(1) 0 01 334+V(1) (3)A> 13 33 30
5 22+4*V(1) 2 01 335+V(1) (2)A> 33 30
6 28+4*V(1) 0 01 335+V(1) <A(1) 11 30
7 38+6*V(1) -10+-2*V(1) 01 <A(1) 116+V(1) 30
8 40+6*V(1) -8+-2*V(1) 03 (3)A> 116+V(1) 30
9 52+8*V(1) 4 03 336+V(1) (3)A> 30
10 54+8*V(1) 2 03 336+V(1) <A(1) 10
11 66+10*V(1) -10+-2*V(1) 03 <A(1) 116+V(1) 10
12 70+10*V(1) -8+-2*V(1) 13 (3)B> 116+V(1) 10
13 82+12*V(1) 4 13 336+V(1) (3)B> 10
14 84+12*V(1) 6 13 337+V(1) (1)B>
15 90+12*V(1) 4 13 337+V(1) <B(4) 30
16 132+18*V(1) -10+-2*V(1) 13 <B(4) 337+V(1) 30
17 144+18*V(1) -12+-2*V(1) <A(1) 11 337+V(1) 30
18 146+18*V(1) -10+-2*V(1) 01 (3)A> 11 337+V(1) 30
19 148+18*V(1) -8+-2*V(1) 01 33 (3)A> 337+V(1) 30
20 150+18*V(1) -10+-2*V(1) 01 33 <A(1) 13 336+V(1) 30
21 152+18*V(1) -12+-2*V(1) 01 <A(1) 11 13 336+V(1) 30
22 154+18*V(1) -10+-2*V(1) 03 (3)A> 11 13 336+V(1) 30
23 156+18*V(1) -8+-2*V(1) 03 33 (3)A> 13 336+V(1) 30
24 158+18*V(1) -6+-2*V(1) 03 332 (2)A> 336+V(1) 30
25 164+18*V(1) -8+-2*V(1) 03 332 <A(1) 11 335+V(1) 30
26 168+18*V(1) -12+-2*V(1) 03 <A(1) 113 335+V(1) 30
<< Success! ==> defined new CTR 18 (PPA)
353271 1721272674 -39302 03 <A(1) 113 3319677 30
== Executing PA-CTR 6, V(1)=19672, V(2)=2, repcount=4919, factor=5/4
441813 2689499120 -49140 03 <A(1) 1124598 33 30
441814 2689499124 -49138 13 (3)B> 1124598 33 30
441815 2689548320 58 13 3324598 (3)B> 33 30
441816 2689548324 60 13 3324599 (3)A> 30
441817 2689548326 58 13 3324599 <A(1) 10
441818 2689597524 -49140 13 <A(1) 1124599 10
441819 2689597528 -49138 33 (3)B> 1124599 10
441820 2689646726 60 3324600 (3)B> 10
441821 2689646728 62 3324601 (1)B>
441822 2689646734 60 3324601 <B(4) 30
441823 2689794340 -49142 <B(4) 3324601 30
441824 2689794354 -49140 33 (3)A> 3324601 30
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 03 <A(1) 112+V(1) 33 30
1 4 2 13 (3)B> 112+V(1) 33 30
2 8+2*V(1) 6+2*V(1) 13 332+V(1) (3)B> 33 30
3 12+2*V(1) 8+2*V(1) 13 333+V(1) (3)A> 30
4 14+2*V(1) 6+2*V(1) 13 333+V(1) <A(1) 10
5 20+4*V(1) 0 13 <A(1) 113+V(1) 10
6 24+4*V(1) 2 33 (3)B> 113+V(1) 10
7 30+6*V(1) 8+2*V(1) 334+V(1) (3)B> 10
8 32+6*V(1) 10+2*V(1) 335+V(1) (1)B>
9 38+6*V(1) 8+2*V(1) 335+V(1) <B(4) 30
10 68+12*V(1) -2 <B(4) 335+V(1) 30
11 82+12*V(1) 0 33 (3)A> 335+V(1) 30
<< Success! ==> defined new CTR 19 (PPA)
441824 2689794354 -49140 33 (3)A> 3324601 30
== Executing PA-CTR 1, V(1)=0, V(2)=24596, repcount=6150, factor=5/4
552524 4202891154 60 3330751 (3)A> 33 30
== Executing PPA-CTR 4 (once), V(1)=30746
552539 4203198718 -61438 333 (3)A> 3330751 30
== Executing PA-CTR 1, V(1)=2, V(2)=30746, repcount=7687, factor=5/4
690905 6567289446 58 3338438 (3)A> 333 30
== Executing PPA-CTR 12 (once), V(1)=38437
690927 6568135184 -76820 33 (3)A> 3338442 34 30
== Executing PA-CTR 10, V(1)=0, V(2)=38437, repcount=9610, factor=5/4
863907 10262526704 60 3348051 (3)A> 332 34 30
863908 10262526706 58 3348051 <A(1) 13 33 34 30
863909 10262622808 -96044 <A(1) 1148051 13 33 34 30
863910 10262622810 -96042 01 (3)A> 1148051 13 33 34 30
863911 10262718912 60 01 3348051 (3)A> 13 33 34 30
863912 10262718914 62 01 3348052 (2)A> 33 34 30
863913 10262718920 60 01 3348052 <A(1) 11 34 30
863914 10262815024 -96044 01 <A(1) 1148053 34 30
863915 10262815026 -96042 03 (3)A> 1148053 34 30
863916 10262911132 64 03 3348053 (3)A> 34 30
863917 10262911134 62 03 3348053 <A(1) 14 30
863918 10263007240 -96044 03 <A(1) 1148053 14 30
863919 10263007244 -96042 13 (3)B> 1148053 14 30
863920 10263103350 64 13 3348053 (3)B> 14 30
863921 10263103356 66 13 3348054 (3)A> 30
863922 10263103358 64 13 3348054 <A(1) 10
863923 10263199466 -96044 13 <A(1) 1148054 10
863924 10263199470 -96042 33 (3)B> 1148054 10
863925 10263295578 66 3348055 (3)B> 10
863926 10263295580 68 3348056 (1)B>
863927 10263295586 66 3348056 <B(4) 30
863928 10263583922 -96046 <B(4) 3348056 30
863929 10263583936 -96044 33 (3)A> 3348056 30
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 331+V(1) (3)A> 332 34 30
1 2 -2 331+V(1) <A(1) 13 33 34 30
2 4+2*V(1) -4+-2*V(1) <A(1) 111+V(1) 13 33 34 30
3 6+2*V(1) -2+-2*V(1) 01 (3)A> 111+V(1) 13 33 34 30
4 8+4*V(1) 0 01 331+V(1) (3)A> 13 33 34 30
5 10+4*V(1) 2 01 332+V(1) (2)A> 33 34 30
6 16+4*V(1) 0 01 332+V(1) <A(1) 11 34 30
7 20+6*V(1) -4+-2*V(1) 01 <A(1) 113+V(1) 34 30
8 22+6*V(1) -2+-2*V(1) 03 (3)A> 113+V(1) 34 30
9 28+8*V(1) 4 03 333+V(1) (3)A> 34 30
10 30+8*V(1) 2 03 333+V(1) <A(1) 14 30
11 36+10*V(1) -4+-2*V(1) 03 <A(1) 113+V(1) 14 30
12 40+10*V(1) -2+-2*V(1) 13 (3)B> 113+V(1) 14 30
13 46+12*V(1) 4 13 333+V(1) (3)B> 14 30
14 52+12*V(1) 6 13 334+V(1) (3)A> 30
15 54+12*V(1) 4 13 334+V(1) <A(1) 10
16 62+14*V(1) -4+-2*V(1) 13 <A(1) 114+V(1) 10
17 66+14*V(1) -2+-2*V(1) 33 (3)B> 114+V(1) 10
18 74+16*V(1) 6 335+V(1) (3)B> 10
19 76+16*V(1) 8 336+V(1) (1)B>
20 82+16*V(1) 6 336+V(1) <B(4) 30
21 118+22*V(1) -6+-2*V(1) <B(4) 336+V(1) 30
22 132+22*V(1) -4+-2*V(1) 33 (3)A> 336+V(1) 30
<< Success! ==> defined new CTR 20 (PPA)
863929 10263583936 -96044 33 (3)A> 3348056 30
== Executing PA-CTR 1, V(1)=0, V(2)=48051, repcount=12013, factor=5/4
1080163 16036455112 60 3360066 (3)A> 334 30
== Executing PPA-CTR 5 (once), V(1)=60065
1080194 16038257256 -120078 03 <A(1) 11 3360072
== Executing PA-CTR 2, V(1)=60067, V(2)=0, repcount=15017, factor=5/4
1350500 25059299530 -150112 03 <A(1) 1175086 334
== Executing PPA-CTR 3 (once), V(1)=75085
1350527 25061402098 -150114 33 (3)A> 3375092 30
== Executing PA-CTR 1, V(1)=0, V(2)=75087, repcount=18772, factor=5/4
1688423 39157522162 62 3393861 (3)A> 334 30
== Executing PPA-CTR 5 (once), V(1)=93860
1688454 39160338156 -187666 03 <A(1) 11 3393867
== Executing PA-CTR 2, V(1)=93862, V(2)=0, repcount=23466, factor=5/4
2110842 61187449968 -234598 03 <A(1) 11117331 333
== Executing PPA-CTR 14 (once), V(1)=117330
2110863 61189796692 -234602 03 <A(1) 11 33117335 43
== Executing PA-CTR 6, V(1)=117330, V(2)=0, repcount=29333, factor=5/4
2638857 95608024238 -293268 03 <A(1) 11146666 333 43
== Executing PPA-CTR 16 (once), V(1)=146665
2638878 95610957656 -293272 03 <A(1) 11 33146671
== Executing PA-CTR 2, V(1)=146666, V(2)=0, repcount=36667, factor=5/4
3298884 149391253230 -366606 03 <A(1) 11183336 333
== Executing PPA-CTR 14 (once), V(1)=183335
3298905 149394920054 -366610 03 <A(1) 11 33183340 43
== Executing PA-CTR 6, V(1)=183335, V(2)=0, repcount=45834, factor=5/4
4123917 233427067322 -458278 03 <A(1) 11229171 334 43
4123918 233427067326 -458276 13 (3)B> 11229171 334 43
4123919 233427525668 66 13 33229171 (3)B> 334 43
4123920 233427525672 68 13 33229172 (3)A> 333 43
4123921 233427525674 66 13 33229172 <A(1) 13 332 43
4123922 233427984018 -458278 13 <A(1) 11229172 13 332 43
4123923 233427984022 -458276 33 (3)B> 11229172 13 332 43
4123924 233428442366 68 33229173 (3)B> 13 332 43
4123925 233428442370 66 33229173 <A(1) 11 332 43
4123926 233428900716 -458280 <A(1) 11229174 332 43
4123927 233428900718 -458278 01 (3)A> 11229174 332 43
4123928 233429359066 70 01 33229174 (3)A> 332 43
4123929 233429359068 68 01 33229174 <A(1) 13 33 43
4123930 233429817416 -458280 01 <A(1) 11229174 13 33 43
4123931 233429817418 -458278 03 (3)A> 11229174 13 33 43
4123932 233430275766 70 03 33229174 (3)A> 13 33 43
4123933 233430275768 72 03 33229175 (2)A> 33 43
4123934 233430275774 70 03 33229175 <A(1) 11 43
4123935 233430734124 -458280 03 <A(1) 11229176 43
4123936 233430734128 -458278 13 (3)B> 11229176 43
4123937 233431192480 74 13 33229176 (3)B> 43
4123938 233431192481 75 13 33229176 31 Z> 3 [stop]
Lines: 656
Top steps: 655
Macro steps: 4123938
Basic steps: 233431192481
Tape index: 75
nonzeros: 458357
log10(nonzeros): 5.661
log10(steps ): 11.368
Run state: stop
Input to awk program:
gohalt 1
nbs 5
T 2-state 5-symbol TM #d (G. Lafitte & C. Papazian)
5T B1R B3R B3R A1L B3L A2L A3R B4L A2R Z1R
: 458,357 233,431,192,481
L 10
M 700
pref sim
machv Laf25_d just simple
machv Laf25_d-r with repetitions reduced
machv Laf25_d-1 with tape symbol exponents
machv Laf25_d-m as bck-2-macro machine
machv Laf25_d-a as bck-2-macro machine with pure additive config-TRs
iam Laf25_d-a
mtype 0 2
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:11:57 CEST 2010
edate Tue Jul 6 22:12:00 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:11:57 CEST 2010