Comment: This TM produces >6.7*10^47 ones in >2.0*10^95 steps.
State | on 0 |
on 1 |
on 0 | on 1 | ||||
---|---|---|---|---|---|---|---|---|
Move | Goto | Move | Goto | |||||
A | B1R | C0L | 1 | right | B | 0 | left | C |
B | A1L | D1R | 1 | left | A | 1 | right | D |
C | B0L | E0L | 0 | left | B | 0 | left | E |
D | A1R | B0R | 1 | right | A | 0 | right | B |
E | F1L | C1L | 1 | left | F | 1 | left | C |
F | D1R | Z1R | 1 | right | D | 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 1-bck-2-macro machine. Simulation is done as 1-bck-2-macro machine with pure additive config-TRs. Pushing initial machine. Pushing macro factor 1. Pushing BCK machine. Pushing macro factor 2. Steps BasSteps BasTpos Tape contents 0 0 0 (0)A> 1 4 -2 <B(0) 01 2 8 0 11 (1)A> 01 3 10 2 112 (1)D> 4 12 4 113 (1)B> 5 14 2 113 <C(0) 10 6 16 0 112 <C(1) 00 10 7 20 -4 <C(1) 012 00 10 8 22 -6 <A(1) 013 00 10 9 24 -4 01 (1)D> 013 00 10 10 28 -6 01 <C(1) 00 012 00 10 11 30 -8 <F(1) 01 00 012 00 10 12 32 -6 01 (0)B> 01 00 012 00 10 13 36 -4 01 11 (0)B> 00 012 00 10 14 40 -2 01 112 (1)A> 012 00 10 15 42 0 01 113 (1)D> 01 00 10 16 46 -2 01 113 <C(1) 002 10 17 52 -8 01 <C(1) 013 002 10 18 54 -10 <F(1) 014 002 10 19 56 -8 01 (0)B> 014 002 10 20 72 0 01 114 (0)B> 002 10 21 76 2 01 115 (1)A> 00 10 22 80 0 01 115 <E(0) 01 10 23 90 -10 01 <E(0) 105 01 10 24 92 -12 <B(0) 106 01 10 25 96 -10 11 (1)A> 106 01 10 26 98 -12 11 <E(0) 00 105 01 10 27 100 -14 <E(0) 10 00 105 01 10 28 106 -12 11 (1)D> 10 00 105 01 10 29 110 -10 112 (1)D> 00 105 01 10 30 112 -8 113 (1)B> 105 01 10 31 114 -6 114 (1)A> 104 01 10 >> Try to prove a PA-CTR with 2 Vars... 0 0 0 111+V(1) (1)A> 103+V(2) [*]* [*]* 1 2 -2 111+V(1) <E(0) 00 102+V(2) [*]* [*]* 2 4+2*V(1) -4+-2*V(1) <E(0) 101+V(1) 00 102+V(2) [*]* [*]* 3 10+2*V(1) -2+-2*V(1) 11 (1)D> 101+V(1) 00 102+V(2) [*]* [*]* 4 14+6*V(1) 0 112+V(1) (1)D> 00 102+V(2) [*]* [*]* 5 16+6*V(1) 2 113+V(1) (1)B> 102+V(2) [*]* [*]* 6 18+6*V(1) 4 114+V(1) (1)A> 101+V(2) [*]* [*]* << Success! ==> defined new CTR 1 (PA) 31 114 -6 114 (1)A> 104 01 10 == Executing PA-CTR 1, V(1)=3, V(2)=1, repcount=1, factor=3/2 37 150 -2 117 (1)A> 102 01 10 38 152 -4 117 <E(0) 00 10 01 10 39 166 -18 <E(0) 107 00 10 01 10 40 172 -16 11 (1)D> 107 00 10 01 10 41 200 -2 118 (1)D> 00 10 01 10 42 202 0 119 (1)B> 10 01 10 43 204 2 1110 (1)A> 01 10 44 206 4 1111 (1)D> 10 45 210 6 1112 (1)D> 46 212 8 1113 (1)B> 47 214 6 1113 <C(0) 10 48 216 4 1112 <C(1) 00 10 49 240 -20 <C(1) 0112 00 10 50 242 -22 <A(1) 0113 00 10 51 244 -20 01 (1)D> 0113 00 10 52 248 -22 01 <C(1) 00 0112 00 10 53 250 -24 <F(1) 01 00 0112 00 10 54 252 -22 01 (0)B> 01 00 0112 00 10 55 256 -20 01 11 (0)B> 00 0112 00 10 56 260 -18 01 112 (1)A> 0112 00 10 57 262 -16 01 113 (1)D> 0111 00 10 58 266 -18 01 113 <C(1) 00 0110 00 10 59 272 -24 01 <C(1) 013 00 0110 00 10 60 274 -26 <F(1) 014 00 0110 00 10 >> Try to prove a PA-CTR with 2 Vars... 0 0 0 <F(1) 011+V(2) 00 013+V(1) [*]* [*]* 1 2 2 01 (0)B> 011+V(2) 00 013+V(1) [*]* [*]* 2 6+4*V(2) 4+2*V(2) 01 111+V(2) (0)B> 00 013+V(1) [*]* [*]* 3 10+4*V(2) 6+2*V(2) 01 112+V(2) (1)A> 013+V(1) [*]* [*]* 4 12+4*V(2) 8+2*V(2) 01 113+V(2) (1)D> 012+V(1) [*]* [*]* 5 16+4*V(2) 6+2*V(2) 01 113+V(2) <C(1) 00 011+V(1) [*]* [*]* 6 22+6*V(2) 0 01 <C(1) 013+V(2) 00 011+V(1) [*]* [*]* 7 24+6*V(2) -2 <F(1) 014+V(2) 00 011+V(1) [*]* [*]* << Success! ==> defined new CTR 2 (PA) 60 274 -26 <F(1) 014 00 0110 00 10 == Executing PA-CTR 2, V(1)=7, V(2)=3, repcount=4, factor=3/2 88 550 -34 <F(1) 0116 00 012 00 10 89 552 -32 01 (0)B> 0116 00 012 00 10 90 616 0 01 1116 (0)B> 00 012 00 10 91 620 2 01 1117 (1)A> 012 00 10 92 622 4 01 1118 (1)D> 01 00 10 93 626 2 01 1118 <C(1) 002 10 94 662 -34 01 <C(1) 0118 002 10 95 664 -36 <F(1) 0119 002 10 96 666 -34 01 (0)B> 0119 002 10 97 742 4 01 1119 (0)B> 002 10 98 746 6 01 1120 (1)A> 00 10 99 750 4 01 1120 <E(0) 01 10 100 790 -36 01 <E(0) 1020 01 10 101 792 -38 <B(0) 1021 01 10 102 796 -36 11 (1)A> 1021 01 10 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 <F(1) 011+V(1) 00 012 00 [*]* 1 2 2 01 (0)B> 011+V(1) 00 012 00 [*]* 2 6+4*V(1) 4+2*V(1) 01 111+V(1) (0)B> 00 012 00 [*]* 3 10+4*V(1) 6+2*V(1) 01 112+V(1) (1)A> 012 00 [*]* 4 12+4*V(1) 8+2*V(1) 01 113+V(1) (1)D> 01 00 [*]* 5 16+4*V(1) 6+2*V(1) 01 113+V(1) <C(1) 002 [*]* 6 22+6*V(1) 0 01 <C(1) 013+V(1) 002 [*]* 7 24+6*V(1) -2 <F(1) 014+V(1) 002 [*]* 8 26+6*V(1) 0 01 (0)B> 014+V(1) 002 [*]* 9 42+10*V(1) 8+2*V(1) 01 114+V(1) (0)B> 002 [*]* 10 46+10*V(1) 10+2*V(1) 01 115+V(1) (1)A> 00 [*]* 11 50+10*V(1) 8+2*V(1) 01 115+V(1) <E(0) 01 [*]* 12 60+12*V(1) -2 01 <E(0) 105+V(1) 01 [*]* 13 62+12*V(1) -4 <B(0) 106+V(1) 01 [*]* 14 66+12*V(1) -2 11 (1)A> 106+V(1) 01 [*]* << Success! ==> defined new CTR 3 (PPA) 102 796 -36 11 (1)A> 1021 01 10 == Executing PA-CTR 1, V(1)=0, V(2)=18, repcount=10, factor=3/2 162 1786 4 1131 (1)A> 10 01 10 163 1788 2 1131 <E(0) 00 01 10 164 1850 -60 <E(0) 1031 00 01 10 165 1856 -58 11 (1)D> 1031 00 01 10 166 1980 4 1132 (1)D> 00 01 10 167 1982 6 1133 (1)B> 01 10 168 1984 4 1133 <C(0) 11 10 169 1986 2 1132 <C(1) 00 11 10 170 2050 -62 <C(1) 0132 00 11 10 171 2052 -64 <A(1) 0133 00 11 10 172 2054 -62 01 (1)D> 0133 00 11 10 173 2058 -64 01 <C(1) 00 0132 00 11 10 174 2060 -66 <F(1) 01 00 0132 00 11 10 175 2062 -64 01 (0)B> 01 00 0132 00 11 10 176 2066 -62 01 11 (0)B> 00 0132 00 11 10 177 2070 -60 01 112 (1)A> 0132 00 11 10 178 2072 -58 01 113 (1)D> 0131 00 11 10 179 2076 -60 01 113 <C(1) 00 0130 00 11 10 180 2082 -66 01 <C(1) 013 00 0130 00 11 10 181 2084 -68 <F(1) 014 00 0130 00 11 10 >> Try to prove a PA-CTR with 2 Vars... 0 0 0 <F(1) 011+V(2) 00 013+V(1) [*]* [*]* [*]* 1 2 2 01 (0)B> 011+V(2) 00 013+V(1) [*]* [*]* [*]* 2 6+4*V(2) 4+2*V(2) 01 111+V(2) (0)B> 00 013+V(1) [*]* [*]* [*]* 3 10+4*V(2) 6+2*V(2) 01 112+V(2) (1)A> 013+V(1) [*]* [*]* [*]* 4 12+4*V(2) 8+2*V(2) 01 113+V(2) (1)D> 012+V(1) [*]* [*]* [*]* 5 16+4*V(2) 6+2*V(2) 01 113+V(2) <C(1) 00 011+V(1) [*]* [*]* [*]* 6 22+6*V(2) 0 01 <C(1) 013+V(2) 00 011+V(1) [*]* [*]* [*]* 7 24+6*V(2) -2 <F(1) 014+V(2) 00 011+V(1) [*]* [*]* [*]* << Success! ==> defined new CTR 4 (PA) 181 2084 -68 <F(1) 014 00 0130 00 11 10 == Executing PA-CTR 4, V(1)=27, V(2)=3, repcount=14, factor=3/2 279 4310 -96 <F(1) 0146 00 012 00 11 10 280 4312 -94 01 (0)B> 0146 00 012 00 11 10 281 4496 -2 01 1146 (0)B> 00 012 00 11 10 282 4500 0 01 1147 (1)A> 012 00 11 10 283 4502 2 01 1148 (1)D> 01 00 11 10 284 4506 0 01 1148 <C(1) 002 11 10 285 4602 -96 01 <C(1) 0148 002 11 10 286 4604 -98 <F(1) 0149 002 11 10 287 4606 -96 01 (0)B> 0149 002 11 10 288 4802 2 01 1149 (0)B> 002 11 10 289 4806 4 01 1150 (1)A> 00 11 10 290 4810 2 01 1150 <E(0) 01 11 10 291 4910 -98 01 <E(0) 1050 01 11 10 292 4912 -100 <B(0) 1051 01 11 10 293 4916 -98 11 (1)A> 1051 01 11 10 294 4918 -100 11 <E(0) 00 1050 01 11 10 295 4920 -102 <E(0) 10 00 1050 01 11 10 296 4926 -100 11 (1)D> 10 00 1050 01 11 10 297 4930 -98 112 (1)D> 00 1050 01 11 10 298 4932 -96 113 (1)B> 1050 01 11 10 299 4934 -94 114 (1)A> 1049 01 11 10 >> Try to prove a PA-CTR with 2 Vars... 0 0 0 111+V(1) (1)A> 103+V(2) [*]* [*]* [*]* 1 2 -2 111+V(1) <E(0) 00 102+V(2) [*]* [*]* [*]* 2 4+2*V(1) -4+-2*V(1) <E(0) 101+V(1) 00 102+V(2) [*]* [*]* [*]* 3 10+2*V(1) -2+-2*V(1) 11 (1)D> 101+V(1) 00 102+V(2) [*]* [*]* [*]* 4 14+6*V(1) 0 112+V(1) (1)D> 00 102+V(2) [*]* [*]* [*]* 5 16+6*V(1) 2 113+V(1) (1)B> 102+V(2) [*]* [*]* [*]* 6 18+6*V(1) 4 114+V(1) (1)A> 101+V(2) [*]* [*]* [*]* << Success! ==> defined new CTR 5 (PA) 299 4934 -94 114 (1)A> 1049 01 11 10 == Executing PA-CTR 5, V(1)=3, V(2)=46, repcount=24, factor=3/2 443 10766 2 1176 (1)A> 10 01 11 10 444 10768 0 1176 <E(0) 00 01 11 10 445 10920 -152 <E(0) 1076 00 01 11 10 446 10926 -150 11 (1)D> 1076 00 01 11 10 447 11230 2 1177 (1)D> 00 01 11 10 448 11232 4 1178 (1)B> 01 11 10 449 11234 2 1178 <C(0) 112 10 450 11236 0 1177 <C(1) 00 112 10 451 11390 -154 <C(1) 0177 00 112 10 452 11392 -156 <A(1) 0178 00 112 10 453 11394 -154 01 (1)D> 0178 00 112 10 454 11398 -156 01 <C(1) 00 0177 00 112 10 455 11400 -158 <F(1) 01 00 0177 00 112 10 >> Try to prove a PPA-CTR with 2 Vars... 0 0 0 112+V(1) (1)A> 10 01 111+V(2) [*]* 1 2 -2 112+V(1) <E(0) 00 01 111+V(2) [*]* 2 6+2*V(1) -6+-2*V(1) <E(0) 102+V(1) 00 01 111+V(2) [*]* 3 12+2*V(1) -4+-2*V(1) 11 (1)D> 102+V(1) 00 01 111+V(2) [*]* 4 20+6*V(1) 0 113+V(1) (1)D> 00 01 111+V(2) [*]* 5 22+6*V(1) 2 114+V(1) (1)B> 01 111+V(2) [*]* 6 24+6*V(1) 0 114+V(1) <C(0) 112+V(2) [*]* 7 26+6*V(1) -2 113+V(1) <C(1) 00 112+V(2) [*]* 8 32+8*V(1) -8+-2*V(1) <C(1) 013+V(1) 00 112+V(2) [*]* 9 34+8*V(1) -10+-2*V(1) <A(1) 014+V(1) 00 112+V(2) [*]* 10 36+8*V(1) -8+-2*V(1) 01 (1)D> 014+V(1) 00 112+V(2) [*]* 11 40+8*V(1) -10+-2*V(1) 01 <C(1) 00 013+V(1) 00 112+V(2) [*]* 12 42+8*V(1) -12+-2*V(1) <F(1) 01 00 013+V(1) 00 112+V(2) [*]* << Success! ==> defined new CTR 6 (PPA) 455 11400 -158 <F(1) 01 00 0177 00 112 10 == Executing PA-CTR 4, V(1)=74, V(2)=0, repcount=38, factor=3/2 721 24966 -234 <F(1) 01115 00 01 00 112 10 722 24968 -232 01 (0)B> 01115 00 01 00 112 10 723 25428 -2 01 11115 (0)B> 00 01 00 112 10 724 25432 0 01 11116 (1)A> 01 00 112 10 725 25434 2 01 11117 (1)D> 00 112 10 726 25436 4 01 11118 (1)B> 112 10 727 25438 6 01 11119 (0)B> 11 10 728 25440 8 01 11119 01 (0)B> 10 729 25442 10 01 11119 012 (1)A> 730 25446 8 01 11119 012 <E(0) 01 731 25448 6 01 11119 01 <B(0) 10 01 732 25450 8 01 11119 01 (1)A> 10 01 733 25452 6 01 11119 01 <E(0) 00 01 734 25454 4 01 11119 <B(0) 10 00 01 735 25456 6 01 11119 (1)A> 10 00 01 736 25458 4 01 11119 <E(0) 002 01 737 25696 -234 01 <E(0) 10119 002 01 738 25698 -236 <B(0) 10120 002 01 739 25702 -234 11 (1)A> 10120 002 01 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 <F(1) 011+V(1) 00 01 00 112 10 1 2 2 01 (0)B> 011+V(1) 00 01 00 112 10 2 6+4*V(1) 4+2*V(1) 01 111+V(1) (0)B> 00 01 00 112 10 3 10+4*V(1) 6+2*V(1) 01 112+V(1) (1)A> 01 00 112 10 4 12+4*V(1) 8+2*V(1) 01 113+V(1) (1)D> 00 112 10 5 14+4*V(1) 10+2*V(1) 01 114+V(1) (1)B> 112 10 6 16+4*V(1) 12+2*V(1) 01 115+V(1) (0)B> 11 10 7 18+4*V(1) 14+2*V(1) 01 115+V(1) 01 (0)B> 10 8 20+4*V(1) 16+2*V(1) 01 115+V(1) 012 (1)A> 9 24+4*V(1) 14+2*V(1) 01 115+V(1) 012 <E(0) 01 10 26+4*V(1) 12+2*V(1) 01 115+V(1) 01 <B(0) 10 01 11 28+4*V(1) 14+2*V(1) 01 115+V(1) 01 (1)A> 10 01 12 30+4*V(1) 12+2*V(1) 01 115+V(1) 01 <E(0) 00 01 13 32+4*V(1) 10+2*V(1) 01 115+V(1) <B(0) 10 00 01 14 34+4*V(1) 12+2*V(1) 01 115+V(1) (1)A> 10 00 01 15 36+4*V(1) 10+2*V(1) 01 115+V(1) <E(0) 002 01 16 46+6*V(1) 0 01 <E(0) 105+V(1) 002 01 17 48+6*V(1) -2 <B(0) 106+V(1) 002 01 18 52+6*V(1) 0 11 (1)A> 106+V(1) 002 01 << Success! ==> defined new CTR 7 (PPA) 739 25702 -234 11 (1)A> 10120 002 01 == Executing PA-CTR 1, V(1)=0, V(2)=117, repcount=59, factor=3/2 1093 57562 2 11178 (1)A> 102 002 01 1094 57564 0 11178 <E(0) 00 10 002 01 1095 57920 -356 <E(0) 10178 00 10 002 01 1096 57926 -354 11 (1)D> 10178 00 10 002 01 1097 58638 2 11179 (1)D> 00 10 002 01 1098 58640 4 11180 (1)B> 10 002 01 1099 58642 6 11181 (1)A> 002 01 1100 58646 4 11181 <E(0) 01 00 01 1101 59008 -358 <E(0) 10181 01 00 01 1102 59014 -356 11 (1)D> 10181 01 00 01 1103 59738 6 11182 (1)D> 01 00 01 1104 59742 4 11182 <C(1) 002 01 1105 60106 -360 <C(1) 01182 002 01 1106 60108 -362 <A(1) 01183 002 01 1107 60110 -360 01 (1)D> 01183 002 01 1108 60114 -362 01 <C(1) 00 01182 002 01 1109 60116 -364 <F(1) 01 00 01182 002 01 >> Try to prove a PPA-CTR with 2 Vars... 0 0 0 111+V(1) (1)A> 102 001+V(2) [*]* 1 2 -2 111+V(1) <E(0) 00 10 001+V(2) [*]* 2 4+2*V(1) -4+-2*V(1) <E(0) 101+V(1) 00 10 001+V(2) [*]* 3 10+2*V(1) -2+-2*V(1) 11 (1)D> 101+V(1) 00 10 001+V(2) [*]* 4 14+6*V(1) 0 112+V(1) (1)D> 00 10 001+V(2) [*]* 5 16+6*V(1) 2 113+V(1) (1)B> 10 001+V(2) [*]* 6 18+6*V(1) 4 114+V(1) (1)A> 001+V(2) [*]* 7 22+6*V(1) 2 114+V(1) <E(0) 01 000+V(2) [*]* 8 30+8*V(1) -6+-2*V(1) <E(0) 104+V(1) 01 000+V(2) [*]* 9 36+8*V(1) -4+-2*V(1) 11 (1)D> 104+V(1) 01 000+V(2) [*]* 10 52+12*V(1) 4 115+V(1) (1)D> 01 000+V(2) [*]* 11 56+12*V(1) 2 115+V(1) <C(1) 001+V(2) [*]* 12 66+14*V(1) -8+-2*V(1) <C(1) 015+V(1) 001+V(2) [*]* 13 68+14*V(1) -10+-2*V(1) <A(1) 016+V(1) 001+V(2) [*]* 14 70+14*V(1) -8+-2*V(1) 01 (1)D> 016+V(1) 001+V(2) [*]* 15 74+14*V(1) -10+-2*V(1) 01 <C(1) 00 015+V(1) 001+V(2) [*]* 16 76+14*V(1) -12+-2*V(1) <F(1) 01 00 015+V(1) 001+V(2) [*]* << Success! ==> defined new CTR 8 (PPA) 1109 60116 -364 <F(1) 01 00 01182 002 01 == Executing PA-CTR 2, V(1)=179, V(2)=0, repcount=90, factor=3/2 1739 134366 -544 <F(1) 01271 00 012 002 01 1740 134368 -542 01 (0)B> 01271 00 012 002 01 1741 135452 0 01 11271 (0)B> 00 012 002 01 1742 135456 2 01 11272 (1)A> 012 002 01 1743 135458 4 01 11273 (1)D> 01 002 01 1744 135462 2 01 11273 <C(1) 003 01 1745 136008 -544 01 <C(1) 01273 003 01 1746 136010 -546 <F(1) 01274 003 01 1747 136012 -544 01 (0)B> 01274 003 01 1748 137108 4 01 11274 (0)B> 003 01 1749 137112 6 01 11275 (1)A> 002 01 1750 137116 4 01 11275 <E(0) 01 00 01 1751 137666 -546 01 <E(0) 10275 01 00 01 1752 137668 -548 <B(0) 10276 01 00 01 1753 137672 -546 11 (1)A> 10276 01 00 01 >> Try to prove a PPA-CTR with 2 Vars... 0 0 0 <F(1) 011+V(2) 00 012 002+V(1) [*]* 1 2 2 01 (0)B> 011+V(2) 00 012 002+V(1) [*]* 2 6+4*V(2) 4+2*V(2) 01 111+V(2) (0)B> 00 012 002+V(1) [*]* 3 10+4*V(2) 6+2*V(2) 01 112+V(2) (1)A> 012 002+V(1) [*]* 4 12+4*V(2) 8+2*V(2) 01 113+V(2) (1)D> 01 002+V(1) [*]* 5 16+4*V(2) 6+2*V(2) 01 113+V(2) <C(1) 003+V(1) [*]* 6 22+6*V(2) 0 01 <C(1) 013+V(2) 003+V(1) [*]* 7 24+6*V(2) -2 <F(1) 014+V(2) 003+V(1) [*]* 8 26+6*V(2) 0 01 (0)B> 014+V(2) 003+V(1) [*]* 9 42+10*V(2) 8+2*V(2) 01 114+V(2) (0)B> 003+V(1) [*]* 10 46+10*V(2) 10+2*V(2) 01 115+V(2) (1)A> 002+V(1) [*]* 11 50+10*V(2) 8+2*V(2) 01 115+V(2) <E(0) 01 001+V(1) [*]* 12 60+12*V(2) -2 01 <E(0) 105+V(2) 01 001+V(1) [*]* 13 62+12*V(2) -4 <B(0) 106+V(2) 01 001+V(1) [*]* 14 66+12*V(2) -2 11 (1)A> 106+V(2) 01 001+V(1) [*]* << Success! ==> defined new CTR 9 (PPA) 1753 137672 -546 11 (1)A> 10276 01 00 01 == Executing PA-CTR 5, V(1)=0, V(2)=273, repcount=137, factor=3/2 2575 307826 2 11412 (1)A> 102 01 00 01 2576 307828 0 11412 <E(0) 00 10 01 00 01 2577 308652 -824 <E(0) 10412 00 10 01 00 01 2578 308658 -822 11 (1)D> 10412 00 10 01 00 01 2579 310306 2 11413 (1)D> 00 10 01 00 01 2580 310308 4 11414 (1)B> 10 01 00 01 2581 310310 6 11415 (1)A> 01 00 01 2582 310312 8 11416 (1)D> 00 01 2583 310314 10 11417 (1)B> 01 2584 310316 8 11417 <C(0) 11 2585 310318 6 11416 <C(1) 00 11 2586 311150 -826 <C(1) 01416 00 11 2587 311152 -828 <A(1) 01417 00 11 2588 311154 -826 01 (1)D> 01417 00 11 2589 311158 -828 01 <C(1) 00 01416 00 11 2590 311160 -830 <F(1) 01 00 01416 00 11 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 111+V(1) (1)A> 102 01 00 01 1 2 -2 111+V(1) <E(0) 00 10 01 00 01 2 4+2*V(1) -4+-2*V(1) <E(0) 101+V(1) 00 10 01 00 01 3 10+2*V(1) -2+-2*V(1) 11 (1)D> 101+V(1) 00 10 01 00 01 4 14+6*V(1) 0 112+V(1) (1)D> 00 10 01 00 01 5 16+6*V(1) 2 113+V(1) (1)B> 10 01 00 01 6 18+6*V(1) 4 114+V(1) (1)A> 01 00 01 7 20+6*V(1) 6 115+V(1) (1)D> 00 01 8 22+6*V(1) 8 116+V(1) (1)B> 01 9 24+6*V(1) 6 116+V(1) <C(0) 11 10 26+6*V(1) 4 115+V(1) <C(1) 00 11 11 36+8*V(1) -6+-2*V(1) <C(1) 015+V(1) 00 11 12 38+8*V(1) -8+-2*V(1) <A(1) 016+V(1) 00 11 13 40+8*V(1) -6+-2*V(1) 01 (1)D> 016+V(1) 00 11 14 44+8*V(1) -8+-2*V(1) 01 <C(1) 00 015+V(1) 00 11 15 46+8*V(1) -10+-2*V(1) <F(1) 01 00 015+V(1) 00 11 << Success! ==> defined new CTR 10 (PPA) 2590 311160 -830 <F(1) 01 00 01416 00 11 == Executing PA-CTR 2, V(1)=413, V(2)=0, repcount=207, factor=3/2 4039 699906 -1244 <F(1) 01622 00 012 00 11 == Executing PPA-CTR 3 (once), V(1)=621 4053 707424 -1246 11 (1)A> 10627 01 11 == Executing PA-CTR 1, V(1)=0, V(2)=624, repcount=313, factor=3/2 5931 1591962 6 11940 (1)A> 10 01 11 5932 1591964 4 11940 <E(0) 00 01 11 5933 1593844 -1876 <E(0) 10940 00 01 11 5934 1593850 -1874 11 (1)D> 10940 00 01 11 5935 1597610 6 11941 (1)D> 00 01 11 5936 1597612 8 11942 (1)B> 01 11 5937 1597614 6 11942 <C(0) 112 5938 1597616 4 11941 <C(1) 00 112 5939 1599498 -1878 <C(1) 01941 00 112 5940 1599500 -1880 <A(1) 01942 00 112 5941 1599502 -1878 01 (1)D> 01942 00 112 5942 1599506 -1880 01 <C(1) 00 01941 00 112 5943 1599508 -1882 <F(1) 01 00 01941 00 112 >> Try to prove a PPA-CTR with 2 Vars... 0 0 0 112+V(1) (1)A> 10 01 111+V(2) 1 2 -2 112+V(1) <E(0) 00 01 111+V(2) 2 6+2*V(1) -6+-2*V(1) <E(0) 102+V(1) 00 01 111+V(2) 3 12+2*V(1) -4+-2*V(1) 11 (1)D> 102+V(1) 00 01 111+V(2) 4 20+6*V(1) 0 113+V(1) (1)D> 00 01 111+V(2) 5 22+6*V(1) 2 114+V(1) (1)B> 01 111+V(2) 6 24+6*V(1) 0 114+V(1) <C(0) 112+V(2) 7 26+6*V(1) -2 113+V(1) <C(1) 00 112+V(2) 8 32+8*V(1) -8+-2*V(1) <C(1) 013+V(1) 00 112+V(2) 9 34+8*V(1) -10+-2*V(1) <A(1) 014+V(1) 00 112+V(2) 10 36+8*V(1) -8+-2*V(1) 01 (1)D> 014+V(1) 00 112+V(2) 11 40+8*V(1) -10+-2*V(1) 01 <C(1) 00 013+V(1) 00 112+V(2) 12 42+8*V(1) -12+-2*V(1) <F(1) 01 00 013+V(1) 00 112+V(2) << Success! ==> defined new CTR 11 (PPA) 5943 1599508 -1882 <F(1) 01 00 01941 00 112 == Executing PA-CTR 2, V(1)=938, V(2)=0, repcount=470, factor=3/2 9233 3594658 -2822 <F(1) 011411 00 01 00 112 9234 3594660 -2820 01 (0)B> 011411 00 01 00 112 9235 3600304 2 01 111411 (0)B> 00 01 00 112 9236 3600308 4 01 111412 (1)A> 01 00 112 9237 3600310 6 01 111413 (1)D> 00 112 9238 3600312 8 01 111414 (1)B> 112 9239 3600314 10 01 111415 (0)B> 11 9240 3600316 12 01 111415 01 (0)B> 9241 3600320 14 01 111415 01 11 (1)A> 9242 3600324 12 01 111415 01 11 <E(0) 01 9243 3600326 10 01 111415 01 <E(0) 10 01 9244 3600328 8 01 111415 <B(0) 102 01 9245 3600330 10 01 111415 (1)A> 102 01 9246 3600332 8 01 111415 <E(0) 00 10 01 9247 3603162 -2822 01 <E(0) 101415 00 10 01 9248 3603164 -2824 <B(0) 101416 00 10 01 9249 3603168 -2822 11 (1)A> 101416 00 10 01 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 <F(1) 011+V(1) 00 01 00 112 1 2 2 01 (0)B> 011+V(1) 00 01 00 112 2 6+4*V(1) 4+2*V(1) 01 111+V(1) (0)B> 00 01 00 112 3 10+4*V(1) 6+2*V(1) 01 112+V(1) (1)A> 01 00 112 4 12+4*V(1) 8+2*V(1) 01 113+V(1) (1)D> 00 112 5 14+4*V(1) 10+2*V(1) 01 114+V(1) (1)B> 112 6 16+4*V(1) 12+2*V(1) 01 115+V(1) (0)B> 11 7 18+4*V(1) 14+2*V(1) 01 115+V(1) 01 (0)B> 8 22+4*V(1) 16+2*V(1) 01 115+V(1) 01 11 (1)A> 9 26+4*V(1) 14+2*V(1) 01 115+V(1) 01 11 <E(0) 01 10 28+4*V(1) 12+2*V(1) 01 115+V(1) 01 <E(0) 10 01 11 30+4*V(1) 10+2*V(1) 01 115+V(1) <B(0) 102 01 12 32+4*V(1) 12+2*V(1) 01 115+V(1) (1)A> 102 01 13 34+4*V(1) 10+2*V(1) 01 115+V(1) <E(0) 00 10 01 14 44+6*V(1) 0 01 <E(0) 105+V(1) 00 10 01 15 46+6*V(1) -2 <B(0) 106+V(1) 00 10 01 16 50+6*V(1) 0 11 (1)A> 106+V(1) 00 10 01 << Success! ==> defined new CTR 12 (PPA) 9249 3603168 -2822 11 (1)A> 101416 00 10 01 == Executing PA-CTR 5, V(1)=0, V(2)=1413, repcount=707, factor=3/2 13491 8108172 6 112122 (1)A> 102 00 10 01 13492 8108174 4 112122 <E(0) 00 10 00 10 01 13493 8112418 -4240 <E(0) 102122 00 10 00 10 01 13494 8112424 -4238 11 (1)D> 102122 00 10 00 10 01 13495 8120912 6 112123 (1)D> 00 10 00 10 01 13496 8120914 8 112124 (1)B> 10 00 10 01 13497 8120916 10 112125 (1)A> 00 10 01 13498 8120920 8 112125 <E(0) 01 10 01 13499 8125170 -4242 <E(0) 102125 01 10 01 13500 8125176 -4240 11 (1)D> 102125 01 10 01 13501 8133676 10 112126 (1)D> 01 10 01 13502 8133680 8 112126 <C(1) 00 10 01 13503 8137932 -4244 <C(1) 012126 00 10 01 13504 8137934 -4246 <A(1) 012127 00 10 01 13505 8137936 -4244 01 (1)D> 012127 00 10 01 13506 8137940 -4246 01 <C(1) 00 012126 00 10 01 13507 8137942 -4248 <F(1) 01 00 012126 00 10 01 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 111+V(1) (1)A> 102 00 [*]* [*]* 1 2 -2 111+V(1) <E(0) 00 10 00 [*]* [*]* 2 4+2*V(1) -4+-2*V(1) <E(0) 101+V(1) 00 10 00 [*]* [*]* 3 10+2*V(1) -2+-2*V(1) 11 (1)D> 101+V(1) 00 10 00 [*]* [*]* 4 14+6*V(1) 0 112+V(1) (1)D> 00 10 00 [*]* [*]* 5 16+6*V(1) 2 113+V(1) (1)B> 10 00 [*]* [*]* 6 18+6*V(1) 4 114+V(1) (1)A> 00 [*]* [*]* 7 22+6*V(1) 2 114+V(1) <E(0) 01 [*]* [*]* 8 30+8*V(1) -6+-2*V(1) <E(0) 104+V(1) 01 [*]* [*]* 9 36+8*V(1) -4+-2*V(1) 11 (1)D> 104+V(1) 01 [*]* [*]* 10 52+12*V(1) 4 115+V(1) (1)D> 01 [*]* [*]* 11 56+12*V(1) 2 115+V(1) <C(1) 00 [*]* [*]* 12 66+14*V(1) -8+-2*V(1) <C(1) 015+V(1) 00 [*]* [*]* 13 68+14*V(1) -10+-2*V(1) <A(1) 016+V(1) 00 [*]* [*]* 14 70+14*V(1) -8+-2*V(1) 01 (1)D> 016+V(1) 00 [*]* [*]* 15 74+14*V(1) -10+-2*V(1) 01 <C(1) 00 015+V(1) 00 [*]* [*]* 16 76+14*V(1) -12+-2*V(1) <F(1) 01 00 015+V(1) 00 [*]* [*]* << Success! ==> defined new CTR 13 (PPA) 13507 8137942 -4248 <F(1) 01 00 012126 00 10 01 == Executing PA-CTR 4, V(1)=2123, V(2)=0, repcount=1062, factor=3/2 20941 18304468 -6372 <F(1) 013187 00 012 00 10 01 20942 18304470 -6370 01 (0)B> 013187 00 012 00 10 01 20943 18317218 4 01 113187 (0)B> 00 012 00 10 01 20944 18317222 6 01 113188 (1)A> 012 00 10 01 20945 18317224 8 01 113189 (1)D> 01 00 10 01 20946 18317228 6 01 113189 <C(1) 002 10 01 20947 18323606 -6372 01 <C(1) 013189 002 10 01 20948 18323608 -6374 <F(1) 013190 002 10 01 20949 18323610 -6372 01 (0)B> 013190 002 10 01 20950 18336370 8 01 113190 (0)B> 002 10 01 20951 18336374 10 01 113191 (1)A> 00 10 01 20952 18336378 8 01 113191 <E(0) 01 10 01 20953 18342760 -6374 01 <E(0) 103191 01 10 01 20954 18342762 -6376 <B(0) 103192 01 10 01 20955 18342766 -6374 11 (1)A> 103192 01 10 01 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 <F(1) 011+V(1) 00 012 00 [*]* [*]* 1 2 2 01 (0)B> 011+V(1) 00 012 00 [*]* [*]* 2 6+4*V(1) 4+2*V(1) 01 111+V(1) (0)B> 00 012 00 [*]* [*]* 3 10+4*V(1) 6+2*V(1) 01 112+V(1) (1)A> 012 00 [*]* [*]* 4 12+4*V(1) 8+2*V(1) 01 113+V(1) (1)D> 01 00 [*]* [*]* 5 16+4*V(1) 6+2*V(1) 01 113+V(1) <C(1) 002 [*]* [*]* 6 22+6*V(1) 0 01 <C(1) 013+V(1) 002 [*]* [*]* 7 24+6*V(1) -2 <F(1) 014+V(1) 002 [*]* [*]* 8 26+6*V(1) 0 01 (0)B> 014+V(1) 002 [*]* [*]* 9 42+10*V(1) 8+2*V(1) 01 114+V(1) (0)B> 002 [*]* [*]* 10 46+10*V(1) 10+2*V(1) 01 115+V(1) (1)A> 00 [*]* [*]* 11 50+10*V(1) 8+2*V(1) 01 115+V(1) <E(0) 01 [*]* [*]* 12 60+12*V(1) -2 01 <E(0) 105+V(1) 01 [*]* [*]* 13 62+12*V(1) -4 <B(0) 106+V(1) 01 [*]* [*]* 14 66+12*V(1) -2 11 (1)A> 106+V(1) 01 [*]* [*]* << Success! ==> defined new CTR 14 (PPA) 20955 18342766 -6374 11 (1)A> 103192 01 10 01 == Executing PA-CTR 5, V(1)=0, V(2)=3189, repcount=1595, factor=3/2 30525 41253346 6 114786 (1)A> 102 01 10 01 30526 41253348 4 114786 <E(0) 00 10 01 10 01 30527 41262920 -9568 <E(0) 104786 00 10 01 10 01 30528 41262926 -9566 11 (1)D> 104786 00 10 01 10 01 30529 41282070 6 114787 (1)D> 00 10 01 10 01 30530 41282072 8 114788 (1)B> 10 01 10 01 30531 41282074 10 114789 (1)A> 01 10 01 30532 41282076 12 114790 (1)D> 10 01 30533 41282080 14 114791 (1)D> 01 30534 41282084 12 114791 <C(1) 30535 41291666 -9570 <C(1) 014791 30536 41291668 -9572 <A(1) 014792 30537 41291670 -9570 01 (1)D> 014792 30538 41291674 -9572 01 <C(1) 00 014791 30539 41291676 -9574 <F(1) 01 00 014791 30540 41291678 -9572 01 (0)B> 01 00 014791 30541 41291682 -9570 01 11 (0)B> 00 014791 30542 41291686 -9568 01 112 (1)A> 014791 30543 41291688 -9566 01 113 (1)D> 014790 30544 41291692 -9568 01 113 <C(1) 00 014789 30545 41291698 -9574 01 <C(1) 013 00 014789 30546 41291700 -9576 <F(1) 014 00 014789 >> Try to prove a PA-CTR with 2 Vars... 0 0 0 <F(1) 011+V(2) 00 013+V(1) 1 2 2 01 (0)B> 011+V(2) 00 013+V(1) 2 6+4*V(2) 4+2*V(2) 01 111+V(2) (0)B> 00 013+V(1) 3 10+4*V(2) 6+2*V(2) 01 112+V(2) (1)A> 013+V(1) 4 12+4*V(2) 8+2*V(2) 01 113+V(2) (1)D> 012+V(1) 5 16+4*V(2) 6+2*V(2) 01 113+V(2) <C(1) 00 011+V(1) 6 22+6*V(2) 0 01 <C(1) 013+V(2) 00 011+V(1) 7 24+6*V(2) -2 <F(1) 014+V(2) 00 011+V(1) << Success! ==> defined new CTR 15 (PA) 30546 41291700 -9576 <F(1) 014 00 014789 == Executing PA-CTR 15, V(1)=4786, V(2)=3, repcount=2394, factor=3/2 47304 92951826 -14364 <F(1) 017186 00 01 47305 92951828 -14362 01 (0)B> 017186 00 01 47306 92980572 10 01 117186 (0)B> 00 01 47307 92980576 12 01 117187 (1)A> 01 47308 92980578 14 01 117188 (1)D> 47309 92980580 16 01 117189 (1)B> 47310 92980582 14 01 117189 <C(0) 10 47311 92980584 12 01 117188 <C(1) 00 10 47312 92994960 -14364 01 <C(1) 017188 00 10 47313 92994962 -14366 <F(1) 017189 00 10 47314 92994964 -14364 01 (0)B> 017189 00 10 47315 93023720 14 01 117189 (0)B> 00 10 47316 93023724 16 01 117190 (1)A> 10 47317 93023726 14 01 117190 <E(0) 47318 93038106 -14366 01 <E(0) 107190 47319 93038108 -14368 <B(0) 107191 47320 93038112 -14366 11 (1)A> 107191 47321 93038114 -14368 11 <E(0) 00 107190 47322 93038116 -14370 <E(0) 10 00 107190 47323 93038122 -14368 11 (1)D> 10 00 107190 47324 93038126 -14366 112 (1)D> 00 107190 47325 93038128 -14364 113 (1)B> 107190 47326 93038130 -14362 114 (1)A> 107189 >> Try to prove a PA-CTR with 2 Vars... 0 0 0 111+V(1) (1)A> 103+V(2) 1 2 -2 111+V(1) <E(0) 00 102+V(2) 2 4+2*V(1) -4+-2*V(1) <E(0) 101+V(1) 00 102+V(2) 3 10+2*V(1) -2+-2*V(1) 11 (1)D> 101+V(1) 00 102+V(2) 4 14+6*V(1) 0 112+V(1) (1)D> 00 102+V(2) 5 16+6*V(1) 2 113+V(1) (1)B> 102+V(2) 6 18+6*V(1) 4 114+V(1) (1)A> 101+V(2) << Success! ==> defined new CTR 16 (PA) 47326 93038130 -14362 114 (1)A> 107189 == Executing PA-CTR 16, V(1)=3, V(2)=7186, repcount=3594, factor=3/2 68890 209386692 14 1110786 (1)A> 10 68891 209386694 12 1110786 <E(0) 68892 209408266 -21560 <E(0) 1010786 68893 209408272 -21558 11 (1)D> 1010786 68894 209451416 14 1110787 (1)D> 68895 209451418 16 1110788 (1)B> 68896 209451420 14 1110788 <C(0) 10 68897 209451422 12 1110787 <C(1) 00 10 68898 209472996 -21562 <C(1) 0110787 00 10 68899 209472998 -21564 <A(1) 0110788 00 10 68900 209473000 -21562 01 (1)D> 0110788 00 10 68901 209473004 -21564 01 <C(1) 00 0110787 00 10 68902 209473006 -21566 <F(1) 01 00 0110787 00 10 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 112+V(1) (1)A> 10 1 2 -2 112+V(1) <E(0) 2 6+2*V(1) -6+-2*V(1) <E(0) 102+V(1) 3 12+2*V(1) -4+-2*V(1) 11 (1)D> 102+V(1) 4 20+6*V(1) 0 113+V(1) (1)D> 5 22+6*V(1) 2 114+V(1) (1)B> 6 24+6*V(1) 0 114+V(1) <C(0) 10 7 26+6*V(1) -2 113+V(1) <C(1) 00 10 8 32+8*V(1) -8+-2*V(1) <C(1) 013+V(1) 00 10 9 34+8*V(1) -10+-2*V(1) <A(1) 014+V(1) 00 10 10 36+8*V(1) -8+-2*V(1) 01 (1)D> 014+V(1) 00 10 11 40+8*V(1) -10+-2*V(1) 01 <C(1) 00 013+V(1) 00 10 12 42+8*V(1) -12+-2*V(1) <F(1) 01 00 013+V(1) 00 10 << Success! ==> defined new CTR 17 (PPA) 68902 209473006 -21566 <F(1) 01 00 0110787 00 10 == Executing PA-CTR 2, V(1)=10784, V(2)=0, repcount=5393, factor=3/2 106653 471313942 -32352 <F(1) 0116180 00 01 00 10 106654 471313944 -32350 01 (0)B> 0116180 00 01 00 10 106655 471378664 10 01 1116180 (0)B> 00 01 00 10 106656 471378668 12 01 1116181 (1)A> 01 00 10 106657 471378670 14 01 1116182 (1)D> 00 10 106658 471378672 16 01 1116183 (1)B> 10 106659 471378674 18 01 1116184 (1)A> 106660 471378678 16 01 1116184 <E(0) 01 106661 471411046 -32352 01 <E(0) 1016184 01 106662 471411048 -32354 <B(0) 1016185 01 106663 471411052 -32352 11 (1)A> 1016185 01 106664 471411054 -32354 11 <E(0) 00 1016184 01 106665 471411056 -32356 <E(0) 10 00 1016184 01 106666 471411062 -32354 11 (1)D> 10 00 1016184 01 106667 471411066 -32352 112 (1)D> 00 1016184 01 106668 471411068 -32350 113 (1)B> 1016184 01 106669 471411070 -32348 114 (1)A> 1016183 01 >> Try to prove a PA-CTR with 2 Vars... 0 0 0 111+V(1) (1)A> 103+V(2) [*]* 1 2 -2 111+V(1) <E(0) 00 102+V(2) [*]* 2 4+2*V(1) -4+-2*V(1) <E(0) 101+V(1) 00 102+V(2) [*]* 3 10+2*V(1) -2+-2*V(1) 11 (1)D> 101+V(1) 00 102+V(2) [*]* 4 14+6*V(1) 0 112+V(1) (1)D> 00 102+V(2) [*]* 5 16+6*V(1) 2 113+V(1) (1)B> 102+V(2) [*]* 6 18+6*V(1) 4 114+V(1) (1)A> 101+V(2) [*]* << Success! ==> defined new CTR 18 (PA) 106669 471411070 -32348 114 (1)A> 1016183 01 == Executing PA-CTR 18, V(1)=3, V(2)=16180, repcount=8091, factor=3/2 155215 1060808056 16 1124277 (1)A> 10 01 155216 1060808058 14 1124277 <E(0) 00 01 155217 1060856612 -48540 <E(0) 1024277 00 01 155218 1060856618 -48538 11 (1)D> 1024277 00 01 155219 1060953726 16 1124278 (1)D> 00 01 155220 1060953728 18 1124279 (1)B> 01 155221 1060953730 16 1124279 <C(0) 11 155222 1060953732 14 1124278 <C(1) 00 11 155223 1061002288 -48542 <C(1) 0124278 00 11 155224 1061002290 -48544 <A(1) 0124279 00 11 155225 1061002292 -48542 01 (1)D> 0124279 00 11 155226 1061002296 -48544 01 <C(1) 00 0124278 00 11 155227 1061002298 -48546 <F(1) 01 00 0124278 00 11 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 112+V(1) (1)A> 10 01 1 2 -2 112+V(1) <E(0) 00 01 2 6+2*V(1) -6+-2*V(1) <E(0) 102+V(1) 00 01 3 12+2*V(1) -4+-2*V(1) 11 (1)D> 102+V(1) 00 01 4 20+6*V(1) 0 113+V(1) (1)D> 00 01 5 22+6*V(1) 2 114+V(1) (1)B> 01 6 24+6*V(1) 0 114+V(1) <C(0) 11 7 26+6*V(1) -2 113+V(1) <C(1) 00 11 8 32+8*V(1) -8+-2*V(1) <C(1) 013+V(1) 00 11 9 34+8*V(1) -10+-2*V(1) <A(1) 014+V(1) 00 11 10 36+8*V(1) -8+-2*V(1) 01 (1)D> 014+V(1) 00 11 11 40+8*V(1) -10+-2*V(1) 01 <C(1) 00 013+V(1) 00 11 12 42+8*V(1) -12+-2*V(1) <F(1) 01 00 013+V(1) 00 11 << Success! ==> defined new CTR 19 (PPA) 155227 1061002298 -48546 <F(1) 01 00 0124278 00 11 == Executing PA-CTR 2, V(1)=24275, V(2)=0, repcount=12138, factor=3/2 240193 2387163764 -72822 <F(1) 0136415 00 012 00 11 == Executing PPA-CTR 3 (once), V(1)=36414 240207 2387600798 -72824 11 (1)A> 1036420 01 11 == Executing PA-CTR 1, V(1)=0, V(2)=36417, repcount=18209, factor=3/2 349461 5371873808 12 1154628 (1)A> 102 01 11 349462 5371873810 10 1154628 <E(0) 00 10 01 11 349463 5371983066 -109246 <E(0) 1054628 00 10 01 11 349464 5371983072 -109244 11 (1)D> 1054628 00 10 01 11 349465 5372201584 12 1154629 (1)D> 00 10 01 11 349466 5372201586 14 1154630 (1)B> 10 01 11 349467 5372201588 16 1154631 (1)A> 01 11 349468 5372201590 18 1154632 (1)D> 11 349469 5372201592 20 1154632 10 (1)D> 349470 5372201594 22 1154632 10 11 (1)B> 349471 5372201596 20 1154632 10 11 <C(0) 10 349472 5372201598 18 1154632 10 <C(1) 00 10 349473 5372201604 16 1154632 <C(1) 002 10 349474 5372310868 -109248 <C(1) 0154632 002 10 349475 5372310870 -109250 <A(1) 0154633 002 10 349476 5372310872 -109248 01 (1)D> 0154633 002 10 349477 5372310876 -109250 01 <C(1) 00 0154632 002 10 349478 5372310878 -109252 <F(1) 01 00 0154632 002 10 >> Try to prove a PPA-CTR with 2 Vars... 0 0 0 111+V(1) (1)A> 102 01 111+V(2) 1 2 -2 111+V(1) <E(0) 00 10 01 111+V(2) 2 4+2*V(1) -4+-2*V(1) <E(0) 101+V(1) 00 10 01 111+V(2) 3 10+2*V(1) -2+-2*V(1) 11 (1)D> 101+V(1) 00 10 01 111+V(2) 4 14+6*V(1) 0 112+V(1) (1)D> 00 10 01 111+V(2) 5 16+6*V(1) 2 113+V(1) (1)B> 10 01 111+V(2) 6 18+6*V(1) 4 114+V(1) (1)A> 01 111+V(2) 7 20+6*V(1) 6 115+V(1) (1)D> 111+V(2) 8 22+6*V(1)+2*V(2) 8+2*V(2) 115+V(1) 101+V(2) (1)D> 9 24+6*V(1)+2*V(2) 10+2*V(2) 115+V(1) 101+V(2) 11 (1)B> 10 26+6*V(1)+2*V(2) 8+2*V(2) 115+V(1) 101+V(2) 11 <C(0) 10 11 28+6*V(1)+2*V(2) 6+2*V(2) 115+V(1) 101+V(2) <C(1) 00 10 12 34+6*V(1)+8*V(2) 4 115+V(1) <C(1) 002+V(2) 10 13 44+8*V(1)+8*V(2) -6+-2*V(1) <C(1) 015+V(1) 002+V(2) 10 14 46+8*V(1)+8*V(2) -8+-2*V(1) <A(1) 016+V(1) 002+V(2) 10 15 48+8*V(1)+8*V(2) -6+-2*V(1) 01 (1)D> 016+V(1) 002+V(2) 10 16 52+8*V(1)+8*V(2) -8+-2*V(1) 01 <C(1) 00 015+V(1) 002+V(2) 10 17 54+8*V(1)+8*V(2) -10+-2*V(1) <F(1) 01 00 015+V(1) 002+V(2) 10 << Success! ==> defined new CTR 20 (PPA) 349478 5372310878 -109252 <F(1) 01 00 0154632 002 10 == Executing PA-CTR 2, V(1)=54629, V(2)=0, repcount=27315, factor=3/2 540683 12087703628 -163882 <F(1) 0181946 00 012 002 10 == Executing PPA-CTR 9 (once), V(1)=0, V(2)=81945 540697 12088687034 -163884 11 (1)A> 1081951 01 00 10 == Executing PA-CTR 5, V(1)=0, V(2)=81948, repcount=40975, factor=3/2 786547 27199611434 16 11122926 (1)A> 10 01 00 10 786548 27199611436 14 11122926 <E(0) 00 01 00 10 786549 27199857288 -245838 <E(0) 10122926 00 01 00 10 786550 27199857294 -245836 11 (1)D> 10122926 00 01 00 10 786551 27200348998 16 11122927 (1)D> 00 01 00 10 786552 27200349000 18 11122928 (1)B> 01 00 10 786553 27200349002 16 11122928 <C(0) 11 00 10 786554 27200349004 14 11122927 <C(1) 00 11 00 10 786555 27200594858 -245840 <C(1) 01122927 00 11 00 10 786556 27200594860 -245842 <A(1) 01122928 00 11 00 10 786557 27200594862 -245840 01 (1)D> 01122928 00 11 00 10 786558 27200594866 -245842 01 <C(1) 00 01122927 00 11 00 10 786559 27200594868 -245844 <F(1) 01 00 01122927 00 11 00 10 786560 27200594870 -245842 01 (0)B> 01 00 01122927 00 11 00 10 786561 27200594874 -245840 01 11 (0)B> 00 01122927 00 11 00 10 786562 27200594878 -245838 01 112 (1)A> 01122927 00 11 00 10 786563 27200594880 -245836 01 113 (1)D> 01122926 00 11 00 10 786564 27200594884 -245838 01 113 <C(1) 00 01122925 00 11 00 10 786565 27200594890 -245844 01 <C(1) 013 00 01122925 00 11 00 10 786566 27200594892 -245846 <F(1) 014 00 01122925 00 11 00 10 >> Try to prove a PA-CTR with 2 Vars... 0 0 0 <F(1) 011+V(2) 00 013+V(1) [*]* [*]* [*]* [*]* 1 2 2 01 (0)B> 011+V(2) 00 013+V(1) [*]* [*]* [*]* [*]* 2 6+4*V(2) 4+2*V(2) 01 111+V(2) (0)B> 00 013+V(1) [*]* [*]* [*]* [*]* 3 10+4*V(2) 6+2*V(2) 01 112+V(2) (1)A> 013+V(1) [*]* [*]* [*]* [*]* 4 12+4*V(2) 8+2*V(2) 01 113+V(2) (1)D> 012+V(1) [*]* [*]* [*]* [*]* 5 16+4*V(2) 6+2*V(2) 01 113+V(2) <C(1) 00 011+V(1) [*]* [*]* [*]* [*]* 6 22+6*V(2) 0 01 <C(1) 013+V(2) 00 011+V(1) [*]* [*]* [*]* [*]* 7 24+6*V(2) -2 <F(1) 014+V(2) 00 011+V(1) [*]* [*]* [*]* [*]* << Success! ==> defined new CTR 21 (PA) 786566 27200594892 -245846 <F(1) 014 00 01122925 00 11 00 10 == Executing PA-CTR 21, V(1)=122922, V(2)=3, repcount=61462, factor=3/2 1216800 61200820134 -368770 <F(1) 01184390 00 01 00 11 00 10 1216801 61200820136 -368768 01 (0)B> 01184390 00 01 00 11 00 10 1216802 61201557696 12 01 11184390 (0)B> 00 01 00 11 00 10 1216803 61201557700 14 01 11184391 (1)A> 01 00 11 00 10 1216804 61201557702 16 01 11184392 (1)D> 00 11 00 10 1216805 61201557704 18 01 11184393 (1)B> 11 00 10 1216806 61201557706 20 01 11184394 (0)B> 00 10 1216807 61201557710 22 01 11184395 (1)A> 10 1216808 61201557712 20 01 11184395 <E(0) 1216809 61201926502 -368770 01 <E(0) 10184395 1216810 61201926504 -368772 <B(0) 10184396 1216811 61201926508 -368770 11 (1)A> 10184396 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 <F(1) 011+V(1) 00 01 00 11 00 10 1 2 2 01 (0)B> 011+V(1) 00 01 00 11 00 10 2 6+4*V(1) 4+2*V(1) 01 111+V(1) (0)B> 00 01 00 11 00 10 3 10+4*V(1) 6+2*V(1) 01 112+V(1) (1)A> 01 00 11 00 10 4 12+4*V(1) 8+2*V(1) 01 113+V(1) (1)D> 00 11 00 10 5 14+4*V(1) 10+2*V(1) 01 114+V(1) (1)B> 11 00 10 6 16+4*V(1) 12+2*V(1) 01 115+V(1) (0)B> 00 10 7 20+4*V(1) 14+2*V(1) 01 116+V(1) (1)A> 10 8 22+4*V(1) 12+2*V(1) 01 116+V(1) <E(0) 9 34+6*V(1) 0 01 <E(0) 106+V(1) 10 36+6*V(1) -2 <B(0) 107+V(1) 11 40+6*V(1) 0 11 (1)A> 107+V(1) << Success! ==> defined new CTR 22 (PPA) 1216811 61201926508 -368770 11 (1)A> 10184396 == Executing PA-CTR 16, V(1)=0, V(2)=184393, repcount=92197, factor=3/2 1769993 137705337562 18 11276592 (1)A> 102 1769994 137705337564 16 11276592 <E(0) 00 10 1769995 137705890748 -553168 <E(0) 10276592 00 10 1769996 137705890754 -553166 11 (1)D> 10276592 00 10 1769997 137706997122 18 11276593 (1)D> 00 10 1769998 137706997124 20 11276594 (1)B> 10 1769999 137706997126 22 11276595 (1)A> 1770000 137706997130 20 11276595 <E(0) 01 1770001 137707550320 -553170 <E(0) 10276595 01 1770002 137707550326 -553168 11 (1)D> 10276595 01 1770003 137708656706 22 11276596 (1)D> 01 1770004 137708656710 20 11276596 <C(1) 1770005 137709209902 -553172 <C(1) 01276596 1770006 137709209904 -553174 <A(1) 01276597 1770007 137709209906 -553172 01 (1)D> 01276597 1770008 137709209910 -553174 01 <C(1) 00 01276596 1770009 137709209912 -553176 <F(1) 01 00 01276596 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 111+V(1) (1)A> 102 1 2 -2 111+V(1) <E(0) 00 10 2 4+2*V(1) -4+-2*V(1) <E(0) 101+V(1) 00 10 3 10+2*V(1) -2+-2*V(1) 11 (1)D> 101+V(1) 00 10 4 14+6*V(1) 0 112+V(1) (1)D> 00 10 5 16+6*V(1) 2 113+V(1) (1)B> 10 6 18+6*V(1) 4 114+V(1) (1)A> 7 22+6*V(1) 2 114+V(1) <E(0) 01 8 30+8*V(1) -6+-2*V(1) <E(0) 104+V(1) 01 9 36+8*V(1) -4+-2*V(1) 11 (1)D> 104+V(1) 01 10 52+12*V(1) 4 115+V(1) (1)D> 01 11 56+12*V(1) 2 115+V(1) <C(1) 12 66+14*V(1) -8+-2*V(1) <C(1) 015+V(1) 13 68+14*V(1) -10+-2*V(1) <A(1) 016+V(1) 14 70+14*V(1) -8+-2*V(1) 01 (1)D> 016+V(1) 15 74+14*V(1) -10+-2*V(1) 01 <C(1) 00 015+V(1) 16 76+14*V(1) -12+-2*V(1) <F(1) 01 00 015+V(1) << Success! ==> defined new CTR 23 (PPA) 1770009 137709209912 -553176 <F(1) 01 00 01276596 == Executing PA-CTR 15, V(1)=276593, V(2)=0, repcount=138297, factor=3/2 2738088 309845826248 -829770 <F(1) 01414892 00 012 2738089 309845826250 -829768 01 (0)B> 01414892 00 012 2738090 309847485818 16 01 11414892 (0)B> 00 012 2738091 309847485822 18 01 11414893 (1)A> 012 2738092 309847485824 20 01 11414894 (1)D> 01 2738093 309847485828 18 01 11414894 <C(1) 2738094 309848315616 -829770 01 <C(1) 01414894 2738095 309848315618 -829772 <F(1) 01414895 2738096 309848315620 -829770 01 (0)B> 01414895 2738097 309849975200 20 01 11414895 (0)B> 2738098 309849975204 22 01 11414896 (1)A> 2738099 309849975208 20 01 11414896 <E(0) 01 2738100 309850805000 -829772 01 <E(0) 10414896 01 2738101 309850805002 -829774 <B(0) 10414897 01 2738102 309850805006 -829772 11 (1)A> 10414897 01 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 <F(1) 011+V(1) 00 012 1 2 2 01 (0)B> 011+V(1) 00 012 2 6+4*V(1) 4+2*V(1) 01 111+V(1) (0)B> 00 012 3 10+4*V(1) 6+2*V(1) 01 112+V(1) (1)A> 012 4 12+4*V(1) 8+2*V(1) 01 113+V(1) (1)D> 01 5 16+4*V(1) 6+2*V(1) 01 113+V(1) <C(1) 6 22+6*V(1) 0 01 <C(1) 013+V(1) 7 24+6*V(1) -2 <F(1) 014+V(1) 8 26+6*V(1) 0 01 (0)B> 014+V(1) 9 42+10*V(1) 8+2*V(1) 01 114+V(1) (0)B> 10 46+10*V(1) 10+2*V(1) 01 115+V(1) (1)A> 11 50+10*V(1) 8+2*V(1) 01 115+V(1) <E(0) 01 12 60+12*V(1) -2 01 <E(0) 105+V(1) 01 13 62+12*V(1) -4 <B(0) 106+V(1) 01 14 66+12*V(1) -2 11 (1)A> 106+V(1) 01 << Success! ==> defined new CTR 24 (PPA) 2738102 309850805006 -829772 11 (1)A> 10414897 01 == Executing PA-CTR 18, V(1)=0, V(2)=414894, repcount=207448, factor=3/2 3982790 697164726374 20 11622345 (1)A> 10 01 == Executing PPA-CTR 19 (once), V(1)=622343 3982802 697169705160 -1244678 <F(1) 01 00 01622346 00 11 == Executing PA-CTR 2, V(1)=622343, V(2)=0, repcount=311172, factor=3/2 6161006 1568626494996 -1867022 <F(1) 01933517 00 012 00 11 == Executing PPA-CTR 3 (once), V(1)=933516 6161020 1568637697254 -1867024 11 (1)A> 10933522 01 11 == Executing PA-CTR 1, V(1)=0, V(2)=933519, repcount=466760, factor=3/2 8961580 3529425976494 16 111400281 (1)A> 102 01 11 == Executing PPA-CTR 20 (once), V(1)=1400280, V(2)=0 8961597 3529437178788 -2800554 <F(1) 01 00 011400285 002 10 == Executing PA-CTR 2, V(1)=1400282, V(2)=0, repcount=700142, factor=3/2 13862591 7941237062394 -4200838 <F(1) 012100427 00 01 002 10 13862592 7941237062396 -4200836 01 (0)B> 012100427 00 01 002 10 13862593 7941245464104 18 01 112100427 (0)B> 00 01 002 10 13862594 7941245464108 20 01 112100428 (1)A> 01 002 10 13862595 7941245464110 22 01 112100429 (1)D> 002 10 13862596 7941245464112 24 01 112100430 (1)B> 00 10 13862597 7941245464114 22 01 112100430 <C(0) 102 13862598 7941245464116 20 01 112100429 <C(1) 00 102 13862599 7941249664974 -4200838 01 <C(1) 012100429 00 102 13862600 7941249664976 -4200840 <F(1) 012100430 00 102 13862601 7941249664978 -4200838 01 (0)B> 012100430 00 102 13862602 7941258066698 22 01 112100430 (0)B> 00 102 13862603 7941258066702 24 01 112100431 (1)A> 102 13862604 7941258066704 22 01 112100431 <E(0) 00 10 13862605 7941262267566 -4200840 01 <E(0) 102100431 00 10 13862606 7941262267568 -4200842 <B(0) 102100432 00 10 13862607 7941262267572 -4200840 11 (1)A> 102100432 00 10 >> Try to prove a PPA-CTR with 2 Vars... 0 0 0 <F(1) 011+V(2) 00 01 002 101+V(1) 1 2 2 01 (0)B> 011+V(2) 00 01 002 101+V(1) 2 6+4*V(2) 4+2*V(2) 01 111+V(2) (0)B> 00 01 002 101+V(1) 3 10+4*V(2) 6+2*V(2) 01 112+V(2) (1)A> 01 002 101+V(1) 4 12+4*V(2) 8+2*V(2) 01 113+V(2) (1)D> 002 101+V(1) 5 14+4*V(2) 10+2*V(2) 01 114+V(2) (1)B> 00 101+V(1) 6 16+4*V(2) 8+2*V(2) 01 114+V(2) <C(0) 102+V(1) 7 18+4*V(2) 6+2*V(2) 01 113+V(2) <C(1) 00 102+V(1) 8 24+6*V(2) 0 01 <C(1) 013+V(2) 00 102+V(1) 9 26+6*V(2) -2 <F(1) 014+V(2) 00 102+V(1) 10 28+6*V(2) 0 01 (0)B> 014+V(2) 00 102+V(1) 11 44+10*V(2) 8+2*V(2) 01 114+V(2) (0)B> 00 102+V(1) 12 48+10*V(2) 10+2*V(2) 01 115+V(2) (1)A> 102+V(1) 13 50+10*V(2) 8+2*V(2) 01 115+V(2) <E(0) 00 101+V(1) 14 60+12*V(2) -2 01 <E(0) 105+V(2) 00 101+V(1) 15 62+12*V(2) -4 <B(0) 106+V(2) 00 101+V(1) 16 66+12*V(2) -2 11 (1)A> 106+V(2) 00 101+V(1) << Success! ==> defined new CTR 25 (PPA) 13862607 7941262267572 -4200840 11 (1)A> 102100432 00 10 == Executing PA-CTR 1, V(1)=0, V(2)=2100429, repcount=1050215, factor=3/2 20163897 17867835635532 20 113150646 (1)A> 102 00 10 == Executing PPA-CTR 8 (once), V(1)=3150645, V(2)=0 20163913 17867879744638 -6301282 <F(1) 01 00 013150650 00 10 == Executing PA-CTR 2, V(1)=3150647, V(2)=0, repcount=1575324, factor=3/2 31191181 40202714719282 -9451930 <F(1) 014725973 00 012 00 10 == Executing PPA-CTR 3 (once), V(1)=4725972 31191195 40202771431012 -9451932 11 (1)A> 104725978 01 10 == Executing PA-CTR 1, V(1)=0, V(2)=4725975, repcount=2362988, factor=3/2 45369123 90456203291200 20 117088965 (1)A> 102 01 10 45369124 90456203291202 18 117088965 <E(0) 00 10 01 10 45369125 90456217469132 -14177912 <E(0) 107088965 00 10 01 10 45369126 90456217469138 -14177910 11 (1)D> 107088965 00 10 01 10 45369127 90456245824998 20 117088966 (1)D> 00 10 01 10 45369128 90456245825000 22 117088967 (1)B> 10 01 10 45369129 90456245825002 24 117088968 (1)A> 01 10 45369130 90456245825004 26 117088969 (1)D> 10 45369131 90456245825008 28 117088970 (1)D> 45369132 90456245825010 30 117088971 (1)B> 45369133 90456245825012 28 117088971 <C(0) 10 45369134 90456245825014 26 117088970 <C(1) 00 10 45369135 90456260002954 -14177914 <C(1) 017088970 00 10 45369136 90456260002956 -14177916 <A(1) 017088971 00 10 45369137 90456260002958 -14177914 01 (1)D> 017088971 00 10 45369138 90456260002962 -14177916 01 <C(1) 00 017088970 00 10 45369139 90456260002964 -14177918 <F(1) 01 00 017088970 00 10 >> Try to prove a PPA-CTR with 2 Vars... 0 0 0 111+V(1) (1)A> 102 01 101+V(2) 1 2 -2 111+V(1) <E(0) 00 10 01 101+V(2) 2 4+2*V(1) -4+-2*V(1) <E(0) 101+V(1) 00 10 01 101+V(2) 3 10+2*V(1) -2+-2*V(1) 11 (1)D> 101+V(1) 00 10 01 101+V(2) 4 14+6*V(1) 0 112+V(1) (1)D> 00 10 01 101+V(2) 5 16+6*V(1) 2 113+V(1) (1)B> 10 01 101+V(2) 6 18+6*V(1) 4 114+V(1) (1)A> 01 101+V(2) 7 20+6*V(1) 6 115+V(1) (1)D> 101+V(2) 8 24+6*V(1)+4*V(2) 8+2*V(2) 116+V(1)+V(2) (1)D> 9 26+6*V(1)+4*V(2) 10+2*V(2) 117+V(1)+V(2) (1)B> 10 28+6*V(1)+4*V(2) 8+2*V(2) 117+V(1)+V(2) <C(0) 10 11 30+6*V(1)+4*V(2) 6+2*V(2) 116+V(1)+V(2) <C(1) 00 10 12 42+8*V(1)+6*V(2) -6+-2*V(1) <C(1) 016+V(1)+V(2) 00 10 13 44+8*V(1)+6*V(2) -8+-2*V(1) <A(1) 017+V(1)+V(2) 00 10 14 46+8*V(1)+6*V(2) -6+-2*V(1) 01 (1)D> 017+V(1)+V(2) 00 10 15 50+8*V(1)+6*V(2) -8+-2*V(1) 01 <C(1) 00 016+V(1)+V(2) 00 10 16 52+8*V(1)+6*V(2) -10+-2*V(1) <F(1) 01 00 016+V(1)+V(2) 00 10 << Success! ==> defined new CTR 26 (PPA) 45369139 90456260002964 -14177918 <F(1) 01 00 017088970 00 10 == Executing PA-CTR 2, V(1)=7088967, V(2)=0, repcount=3544484, factor=3/2 70180527 203526614606528 -21266886 <F(1) 0110633453 00 012 00 10 == Executing PPA-CTR 3 (once), V(1)=10633452 70180541 203526742208018 -21266888 11 (1)A> 1010633458 01 10 == Executing PA-CTR 1, V(1)=0, V(2)=10633455, repcount=5316728, factor=3/2 102080909 457935159692426 24 1115950185 (1)A> 102 01 10 == Executing PPA-CTR 26 (once), V(1)=15950184, V(2)=0 102080925 457935287293950 -31900354 <F(1) 01 00 0115950190 00 10 == Executing PA-CTR 2, V(1)=15950187, V(2)=0, repcount=7975094, factor=3/2 157906583 1030354525699884 -47850542 <F(1) 0123925283 00 012 00 10 == Executing PPA-CTR 3 (once), V(1)=23925282 157906597 1030354812803334 -47850544 11 (1)A> 1023925288 01 10 == Executing PA-CTR 1, V(1)=0, V(2)=23925285, repcount=11962643, factor=3/2 229682455 2318298368376162 28 1135887930 (1)A> 102 01 10 == Executing PPA-CTR 26 (once), V(1)=35887929, V(2)=0 229682471 2318298655479646 -71775840 <F(1) 01 00 0135887935 00 10 == Executing PA-CTR 2, V(1)=35887932, V(2)=0, repcount=17943967, factor=3/2 355290240 5216172489912952 -107663774 <F(1) 0153831902 00 01 00 10 355290241 5216172489912954 -107663772 01 (0)B> 0153831902 00 01 00 10 355290242 5216172705240562 32 01 1153831902 (0)B> 00 01 00 10 355290243 5216172705240566 34 01 1153831903 (1)A> 01 00 10 355290244 5216172705240568 36 01 1153831904 (1)D> 00 10 355290245 5216172705240570 38 01 1153831905 (1)B> 10 355290246 5216172705240572 40 01 1153831906 (1)A> 355290247 5216172705240576 38 01 1153831906 <E(0) 01 355290248 5216172812904388 -107663774 01 <E(0) 1053831906 01 355290249 5216172812904390 -107663776 <B(0) 1053831907 01 355290250 5216172812904394 -107663774 11 (1)A> 1053831907 01 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 <F(1) 011+V(1) 00 01 00 10 1 2 2 01 (0)B> 011+V(1) 00 01 00 10 2 6+4*V(1) 4+2*V(1) 01 111+V(1) (0)B> 00 01 00 10 3 10+4*V(1) 6+2*V(1) 01 112+V(1) (1)A> 01 00 10 4 12+4*V(1) 8+2*V(1) 01 113+V(1) (1)D> 00 10 5 14+4*V(1) 10+2*V(1) 01 114+V(1) (1)B> 10 6 16+4*V(1) 12+2*V(1) 01 115+V(1) (1)A> 7 20+4*V(1) 10+2*V(1) 01 115+V(1) <E(0) 01 8 30+6*V(1) 0 01 <E(0) 105+V(1) 01 9 32+6*V(1) -2 <B(0) 106+V(1) 01 10 36+6*V(1) 0 11 (1)A> 106+V(1) 01 << Success! ==> defined new CTR 27 (PPA) 355290250 5216172812904394 -107663774 11 (1)A> 1053831907 01 == Executing PA-CTR 18, V(1)=0, V(2)=53831904, repcount=26915953, factor=3/2 516785968 11736389788231852 38 1180747860 (1)A> 10 01 == Executing PPA-CTR 19 (once), V(1)=80747858 516785980 11736390434214758 -161495690 <F(1) 01 00 0180747861 00 11 == Executing PA-CTR 2, V(1)=80747858, V(2)=0, repcount=40373930, factor=3/2 799403490 26406879052627808 -242243550 <F(1) 01121121791 00 01 00 11 799403491 26406879052627810 -242243548 01 (0)B> 01121121791 00 01 00 11 799403492 26406879537114974 34 01 11121121791 (0)B> 00 01 00 11 799403493 26406879537114978 36 01 11121121792 (1)A> 01 00 11 799403494 26406879537114980 38 01 11121121793 (1)D> 00 11 799403495 26406879537114982 40 01 11121121794 (1)B> 11 Lines: 501 Top steps: 500 Macro steps: 799403495 Basic steps: 26406879537114982 Tape index: 40 ones: 242243592 log10(ones ): 8.384 log10(steps ): 16.422
Input to awk program: gohalt 1 L 26 5T B1R C0L A1L D1R B0L E0L A1R B0R F1L C1L D1R Z1R : >6.7*10^47 >2.0*10^95 T 6-state TM #l from MaBu-List M 501 pref sim machv mbL6_l just simple machv mbL6_l-r with repetitions reduced machv mbL6_l-1 with tape symbol exponents machv mbL6_l-m as 1-bck-2-macro machine machv mbL6_l-a as 1-bck-2-macro machine with pure additive config-TRs iam mbL6_l-a mtype 1 0 2 mmtyp 3 r 1 H 1 mac 0 E 2 sympr HM 1 date Tue Jul 6 22:11:02 CEST 2010 edate Tue Jul 6 22:11:04 CEST 2010 bnspeed 1Start: Tue Jul 6 22:11:02 CEST 2010
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;