Comment: This TM produces >1.4x10^2355 nonzeros in >3.4x10^4710 steps.
State | on 0 |
on 1 |
on 2 |
on 3 |
on 0 | on 1 | on 2 | on 3 | ||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Move | Goto | Move | Goto | Move | Goto | Move | Goto | |||||||||
A | 1RB | 2LB | 2RA | 1LA | 1 | right | B | 2 | left | B | 2 | right | A | 1 | left | A |
B | 2LA | 1RC | 0LB | 2RA | 2 | left | A | 1 | right | C | 0 | left | B | 2 | right | A |
C | 1RB | 3LC | 1LA | 1RH | 1 | right | B | 3 | left | C | 1 | left | A | 1 | right | H |
The same TM just simple. The same TM with repetitions reduced. The same TM with tape symbol exponents. The same TM as 2-bck-macro machine. Simulation is done as 2-bck-macro machine with pure additive config-TRs. Pushing initial machine. Pushing macro factor 2. Pushing BCK machine. Steps BasSteps BasTpos Tape contents 0 0 0 (00)A> 1 14 2 11 (11)B> 2 19 -1 11 <B(21) 20 3 25 -3 <B(21) 11 20 4 34 0 11 (11)C> 11 20 5 37 -3 11 <C(33) 31 20 6 39 -5 <C(33) 33 31 20 7 50 -2 01 (11)B> 33 31 20 8 60 0 01 11 (11)B> 31 20 9 68 2 01 112 (11)B> 20 10 79 -1 01 112 <B(21) 12 11 91 -5 01 <B(21) 112 12 12 95 -7 <A(22) 113 12 13 102 -4 01 (11)B> 113 12 14 107 -7 01 <C(33) 33 112 12 15 120 -4 11 (12)A> 33 112 12 16 130 -2 112 (12)A> 112 12 17 138 0 113 (11)C> 11 12 18 141 -3 113 <C(33) 31 12 19 147 -9 <C(33) 333 31 12 20 158 -6 01 (11)B> 333 31 12 21 188 0 01 113 (11)B> 31 12 22 196 2 01 114 (11)B> 12 23 205 -1 01 114 <B(21) 11 24 229 -9 01 <B(21) 115 25 233 -11 <A(22) 116 26 240 -8 01 (11)B> 116 27 245 -11 01 <C(33) 33 115 28 258 -8 11 (12)A> 33 115 29 268 -6 112 (12)A> 115 30 276 -4 113 (11)C> 114 31 279 -7 113 <C(33) 31 113 32 285 -13 <C(33) 333 31 113 33 296 -10 01 (11)B> 333 31 113 34 326 -4 01 113 (11)B> 31 113 35 334 -2 01 114 (11)B> 113 36 339 -5 01 114 <C(33) 33 112 37 347 -13 01 <C(33) 335 112 >> Try to prove a PA-CTR with 2 Vars... 0 0 0 01 <C(33) 331+V(2) 114+V(1) 1 13 3 11 (12)A> 331+V(2) 114+V(1) 2 23+10*V(2) 5+2*V(2) 112+V(2) (12)A> 114+V(1) 3 31+10*V(2) 7+2*V(2) 113+V(2) (11)C> 113+V(1) 4 34+10*V(2) 4+2*V(2) 113+V(2) <C(33) 31 112+V(1) 5 40+12*V(2) -2 <C(33) 333+V(2) 31 112+V(1) 6 51+12*V(2) 1 01 (11)B> 333+V(2) 31 112+V(1) 7 81+22*V(2) 7+2*V(2) 01 113+V(2) (11)B> 31 112+V(1) 8 89+22*V(2) 9+2*V(2) 01 114+V(2) (11)B> 112+V(1) 9 94+22*V(2) 6+2*V(2) 01 114+V(2) <C(33) 33 111+V(1) 10 102+24*V(2) -2 01 <C(33) 335+V(2) 111+V(1) << Success! ==> defined new CTR 1 (PA) 38 360 -10 11 (12)A> 335 112 39 410 0 116 (12)A> 112 40 418 2 117 (11)C> 11 41 421 -1 117 <C(33) 31 42 435 -15 <C(33) 337 31 43 446 -12 01 (11)B> 337 31 44 516 2 01 117 (11)B> 31 45 524 4 01 118 (11)B> 46 529 1 01 118 <B(21) 20 47 577 -15 01 <B(21) 118 20 48 581 -17 <A(22) 119 20 49 588 -14 01 (11)B> 119 20 50 593 -17 01 <C(33) 33 118 20 51 606 -14 11 (12)A> 33 118 20 52 616 -12 112 (12)A> 118 20 53 624 -10 113 (11)C> 117 20 54 627 -13 113 <C(33) 31 116 20 55 633 -19 <C(33) 333 31 116 20 56 644 -16 01 (11)B> 333 31 116 20 57 674 -10 01 113 (11)B> 31 116 20 58 682 -8 01 114 (11)B> 116 20 59 687 -11 01 114 <C(33) 33 115 20 60 695 -19 01 <C(33) 335 115 20 >> Try to prove a PA-CTR with 2 Vars... 0 0 0 01 <C(33) 331+V(2) 114+V(1) [*]* 1 13 3 11 (12)A> 331+V(2) 114+V(1) [*]* 2 23+10*V(2) 5+2*V(2) 112+V(2) (12)A> 114+V(1) [*]* 3 31+10*V(2) 7+2*V(2) 113+V(2) (11)C> 113+V(1) [*]* 4 34+10*V(2) 4+2*V(2) 113+V(2) <C(33) 31 112+V(1) [*]* 5 40+12*V(2) -2 <C(33) 333+V(2) 31 112+V(1) [*]* 6 51+12*V(2) 1 01 (11)B> 333+V(2) 31 112+V(1) [*]* 7 81+22*V(2) 7+2*V(2) 01 113+V(2) (11)B> 31 112+V(1) [*]* 8 89+22*V(2) 9+2*V(2) 01 114+V(2) (11)B> 112+V(1) [*]* 9 94+22*V(2) 6+2*V(2) 01 114+V(2) <C(33) 33 111+V(1) [*]* 10 102+24*V(2) -2 01 <C(33) 335+V(2) 111+V(1) [*]* << Success! ==> defined new CTR 2 (PA) 60 695 -19 01 <C(33) 335 115 20 == Executing PA-CTR 2, V(1)=1, V(2)=4, repcount=1, factor=4/3 70 893 -21 01 <C(33) 339 112 20 71 906 -18 11 (12)A> 339 112 20 72 996 0 1110 (12)A> 112 20 73 1004 2 1111 (11)C> 11 20 74 1007 -1 1111 <C(33) 31 20 75 1029 -23 <C(33) 3311 31 20 76 1040 -20 01 (11)B> 3311 31 20 77 1150 2 01 1111 (11)B> 31 20 78 1158 4 01 1112 (11)B> 20 79 1169 1 01 1112 <B(21) 12 80 1241 -23 01 <B(21) 1112 12 81 1245 -25 <A(22) 1113 12 82 1252 -22 01 (11)B> 1113 12 83 1257 -25 01 <C(33) 33 1112 12 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 01 <C(33) 331+V(1) 112 20 1 13 3 11 (12)A> 331+V(1) 112 20 2 23+10*V(1) 5+2*V(1) 112+V(1) (12)A> 112 20 3 31+10*V(1) 7+2*V(1) 113+V(1) (11)C> 11 20 4 34+10*V(1) 4+2*V(1) 113+V(1) <C(33) 31 20 5 40+12*V(1) -2 <C(33) 333+V(1) 31 20 6 51+12*V(1) 1 01 (11)B> 333+V(1) 31 20 7 81+22*V(1) 7+2*V(1) 01 113+V(1) (11)B> 31 20 8 89+22*V(1) 9+2*V(1) 01 114+V(1) (11)B> 20 9 100+22*V(1) 6+2*V(1) 01 114+V(1) <B(21) 12 10 124+28*V(1) -2 01 <B(21) 114+V(1) 12 11 128+28*V(1) -4 <A(22) 115+V(1) 12 12 135+28*V(1) -1 01 (11)B> 115+V(1) 12 13 140+28*V(1) -4 01 <C(33) 33 114+V(1) 12 << Success! ==> defined new CTR 3 (PPA) 83 1257 -25 01 <C(33) 33 1112 12 == Executing PA-CTR 2, V(1)=8, V(2)=0, repcount=3, factor=4/3 113 1851 -31 01 <C(33) 3313 113 12 114 1864 -28 11 (12)A> 3313 113 12 115 1994 -2 1114 (12)A> 113 12 116 2002 0 1115 (11)C> 112 12 117 2005 -3 1115 <C(33) 31 11 12 118 2035 -33 <C(33) 3315 31 11 12 119 2046 -30 01 (11)B> 3315 31 11 12 120 2196 0 01 1115 (11)B> 31 11 12 121 2204 2 01 1116 (11)B> 11 12 122 2209 -1 01 1116 <C(33) 33 12 123 2241 -33 01 <C(33) 3317 12 124 2254 -30 11 (12)A> 3317 12 125 2424 4 1118 (12)A> 12 126 2434 6 1119 (11)B> 127 2439 3 1119 <B(21) 20 128 2553 -35 <B(21) 1119 20 129 2562 -32 11 (11)C> 1119 20 130 2565 -35 11 <C(33) 31 1118 20 131 2567 -37 <C(33) 33 31 1118 20 132 2578 -34 01 (11)B> 33 31 1118 20 133 2588 -32 01 11 (11)B> 31 1118 20 134 2596 -30 01 112 (11)B> 1118 20 135 2601 -33 01 112 <C(33) 33 1117 20 136 2605 -37 01 <C(33) 333 1117 20 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 01 <C(33) 331+V(1) 113 12 1 13 3 11 (12)A> 331+V(1) 113 12 2 23+10*V(1) 5+2*V(1) 112+V(1) (12)A> 113 12 3 31+10*V(1) 7+2*V(1) 113+V(1) (11)C> 112 12 4 34+10*V(1) 4+2*V(1) 113+V(1) <C(33) 31 11 12 5 40+12*V(1) -2 <C(33) 333+V(1) 31 11 12 6 51+12*V(1) 1 01 (11)B> 333+V(1) 31 11 12 7 81+22*V(1) 7+2*V(1) 01 113+V(1) (11)B> 31 11 12 8 89+22*V(1) 9+2*V(1) 01 114+V(1) (11)B> 11 12 9 94+22*V(1) 6+2*V(1) 01 114+V(1) <C(33) 33 12 10 102+24*V(1) -2 01 <C(33) 335+V(1) 12 11 115+24*V(1) 1 11 (12)A> 335+V(1) 12 12 165+34*V(1) 11+2*V(1) 116+V(1) (12)A> 12 13 175+34*V(1) 13+2*V(1) 117+V(1) (11)B> 14 180+34*V(1) 10+2*V(1) 117+V(1) <B(21) 20 15 222+40*V(1) -4 <B(21) 117+V(1) 20 16 231+40*V(1) -1 11 (11)C> 117+V(1) 20 17 234+40*V(1) -4 11 <C(33) 31 116+V(1) 20 18 236+40*V(1) -6 <C(33) 33 31 116+V(1) 20 19 247+40*V(1) -3 01 (11)B> 33 31 116+V(1) 20 20 257+40*V(1) -1 01 11 (11)B> 31 116+V(1) 20 21 265+40*V(1) 1 01 112 (11)B> 116+V(1) 20 22 270+40*V(1) -2 01 112 <C(33) 33 115+V(1) 20 23 274+40*V(1) -6 01 <C(33) 333 115+V(1) 20 << Success! ==> defined new CTR 4 (PPA) 136 2605 -37 01 <C(33) 333 1117 20 == Executing PA-CTR 2, V(1)=13, V(2)=2, repcount=5, factor=4/3 186 4315 -47 01 <C(33) 3323 112 20 == Executing PPA-CTR 3 (once), V(1)=22 199 5071 -51 01 <C(33) 33 1126 12 == Executing PA-CTR 2, V(1)=22, V(2)=0, repcount=8, factor=4/3 279 8575 -67 01 <C(33) 3333 112 12 280 8588 -64 11 (12)A> 3333 112 12 281 8918 2 1134 (12)A> 112 12 282 8926 4 1135 (11)C> 11 12 283 8929 1 1135 <C(33) 31 12 284 8999 -69 <C(33) 3335 31 12 285 9010 -66 01 (11)B> 3335 31 12 286 9360 4 01 1135 (11)B> 31 12 287 9368 6 01 1136 (11)B> 12 288 9377 3 01 1136 <B(21) 11 289 9593 -69 01 <B(21) 1137 290 9597 -71 <A(22) 1138 291 9604 -68 01 (11)B> 1138 292 9609 -71 01 <C(33) 33 1137 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 01 <C(33) 331+V(1) 112 12 1 13 3 11 (12)A> 331+V(1) 112 12 2 23+10*V(1) 5+2*V(1) 112+V(1) (12)A> 112 12 3 31+10*V(1) 7+2*V(1) 113+V(1) (11)C> 11 12 4 34+10*V(1) 4+2*V(1) 113+V(1) <C(33) 31 12 5 40+12*V(1) -2 <C(33) 333+V(1) 31 12 6 51+12*V(1) 1 01 (11)B> 333+V(1) 31 12 7 81+22*V(1) 7+2*V(1) 01 113+V(1) (11)B> 31 12 8 89+22*V(1) 9+2*V(1) 01 114+V(1) (11)B> 12 9 98+22*V(1) 6+2*V(1) 01 114+V(1) <B(21) 11 10 122+28*V(1) -2 01 <B(21) 115+V(1) 11 126+28*V(1) -4 <A(22) 116+V(1) 12 133+28*V(1) -1 01 (11)B> 116+V(1) 13 138+28*V(1) -4 01 <C(33) 33 115+V(1) << Success! ==> defined new CTR 5 (PPA) 292 9609 -71 01 <C(33) 33 1137 == Executing PA-CTR 1, V(1)=33, V(2)=0, repcount=12, factor=4/3 412 17169 -95 01 <C(33) 3349 11 413 17182 -92 11 (12)A> 3349 11 414 17672 6 1150 (12)A> 11 415 17680 8 1151 (11)C> 416 17689 5 1151 <B(21) 12 417 17995 -97 <B(21) 1151 12 418 18004 -94 11 (11)C> 1151 12 419 18007 -97 11 <C(33) 31 1150 12 420 18009 -99 <C(33) 33 31 1150 12 421 18020 -96 01 (11)B> 33 31 1150 12 422 18030 -94 01 11 (11)B> 31 1150 12 423 18038 -92 01 112 (11)B> 1150 12 424 18043 -95 01 112 <C(33) 33 1149 12 425 18047 -99 01 <C(33) 333 1149 12 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 01 <C(33) 334+V(1) 11 1 13 3 11 (12)A> 334+V(1) 11 2 53+10*V(1) 11+2*V(1) 115+V(1) (12)A> 11 3 61+10*V(1) 13+2*V(1) 116+V(1) (11)C> 4 70+10*V(1) 10+2*V(1) 116+V(1) <B(21) 12 5 106+16*V(1) -2 <B(21) 116+V(1) 12 6 115+16*V(1) 1 11 (11)C> 116+V(1) 12 7 118+16*V(1) -2 11 <C(33) 31 115+V(1) 12 8 120+16*V(1) -4 <C(33) 33 31 115+V(1) 12 9 131+16*V(1) -1 01 (11)B> 33 31 115+V(1) 12 10 141+16*V(1) 1 01 11 (11)B> 31 115+V(1) 12 11 149+16*V(1) 3 01 112 (11)B> 115+V(1) 12 12 154+16*V(1) 0 01 112 <C(33) 33 114+V(1) 12 13 158+16*V(1) -4 01 <C(33) 333 114+V(1) 12 << Success! ==> defined new CTR 6 (PPA) 425 18047 -99 01 <C(33) 333 1149 12 == Executing PA-CTR 2, V(1)=45, V(2)=2, repcount=16, factor=4/3 585 31967 -131 01 <C(33) 3367 11 12 586 31980 -128 11 (12)A> 3367 11 12 587 32650 6 1168 (12)A> 11 12 588 32658 8 1169 (11)C> 12 589 32661 5 1169 <C(33) 32 590 32799 -133 <C(33) 3369 32 591 32810 -130 01 (11)B> 3369 32 592 33500 8 01 1169 (11)B> 32 593 33502 10 01 1170 (22)A> 594 33507 7 01 1170 <B(00) 22 595 33517 5 01 1169 <B(21) 12 22 596 33931 -133 01 <B(21) 1169 12 22 597 33935 -135 <A(22) 1170 12 22 598 33942 -132 01 (11)B> 1170 12 22 599 33947 -135 01 <C(33) 33 1169 12 22 600 33960 -132 11 (12)A> 33 1169 12 22 601 33970 -130 112 (12)A> 1169 12 22 602 33978 -128 113 (11)C> 1168 12 22 603 33981 -131 113 <C(33) 31 1167 12 22 604 33987 -137 <C(33) 333 31 1167 12 22 605 33998 -134 01 (11)B> 333 31 1167 12 22 606 34028 -128 01 113 (11)B> 31 1167 12 22 607 34036 -126 01 114 (11)B> 1167 12 22 608 34041 -129 01 114 <C(33) 33 1166 12 22 609 34049 -137 01 <C(33) 335 1166 12 22 >> Try to prove a PA-CTR with 2 Vars... 0 0 0 01 <C(33) 331+V(2) 114+V(1) [*]* [*]* 1 13 3 11 (12)A> 331+V(2) 114+V(1) [*]* [*]* 2 23+10*V(2) 5+2*V(2) 112+V(2) (12)A> 114+V(1) [*]* [*]* 3 31+10*V(2) 7+2*V(2) 113+V(2) (11)C> 113+V(1) [*]* [*]* 4 34+10*V(2) 4+2*V(2) 113+V(2) <C(33) 31 112+V(1) [*]* [*]* 5 40+12*V(2) -2 <C(33) 333+V(2) 31 112+V(1) [*]* [*]* 6 51+12*V(2) 1 01 (11)B> 333+V(2) 31 112+V(1) [*]* [*]* 7 81+22*V(2) 7+2*V(2) 01 113+V(2) (11)B> 31 112+V(1) [*]* [*]* 8 89+22*V(2) 9+2*V(2) 01 114+V(2) (11)B> 112+V(1) [*]* [*]* 9 94+22*V(2) 6+2*V(2) 01 114+V(2) <C(33) 33 111+V(1) [*]* [*]* 10 102+24*V(2) -2 01 <C(33) 335+V(2) 111+V(1) [*]* [*]* << Success! ==> defined new CTR 7 (PA) 609 34049 -137 01 <C(33) 335 1166 12 22 == Executing PA-CTR 7, V(1)=62, V(2)=4, repcount=21, factor=4/3 819 58367 -179 01 <C(33) 3389 113 12 22 820 58380 -176 11 (12)A> 3389 113 12 22 821 59270 2 1190 (12)A> 113 12 22 822 59278 4 1191 (11)C> 112 12 22 823 59281 1 1191 <C(33) 31 11 12 22 824 59463 -181 <C(33) 3391 31 11 12 22 825 59474 -178 01 (11)B> 3391 31 11 12 22 826 60384 4 01 1191 (11)B> 31 11 12 22 827 60392 6 01 1192 (11)B> 11 12 22 828 60397 3 01 1192 <C(33) 33 12 22 829 60581 -181 01 <C(33) 3393 12 22 830 60594 -178 11 (12)A> 3393 12 22 831 61524 8 1194 (12)A> 12 22 832 61534 10 1195 (11)B> 22 833 61540 12 1196 (11)B> 834 61545 9 1196 <B(21) 20 835 62121 -183 <B(21) 1196 20 836 62130 -180 11 (11)C> 1196 20 837 62133 -183 11 <C(33) 31 1195 20 838 62135 -185 <C(33) 33 31 1195 20 839 62146 -182 01 (11)B> 33 31 1195 20 840 62156 -180 01 11 (11)B> 31 1195 20 841 62164 -178 01 112 (11)B> 1195 20 842 62169 -181 01 112 <C(33) 33 1194 20 843 62173 -185 01 <C(33) 333 1194 20 >> Try to prove a PPA-CTR with 2 Vars... 0 0 0 01 <C(33) 331+V(2) 113 12 221+V(1) 1 13 3 11 (12)A> 331+V(2) 113 12 221+V(1) 2 23+10*V(2) 5+2*V(2) 112+V(2) (12)A> 113 12 221+V(1) 3 31+10*V(2) 7+2*V(2) 113+V(2) (11)C> 112 12 221+V(1) 4 34+10*V(2) 4+2*V(2) 113+V(2) <C(33) 31 11 12 221+V(1) 5 40+12*V(2) -2 <C(33) 333+V(2) 31 11 12 221+V(1) 6 51+12*V(2) 1 01 (11)B> 333+V(2) 31 11 12 221+V(1) 7 81+22*V(2) 7+2*V(2) 01 113+V(2) (11)B> 31 11 12 221+V(1) 8 89+22*V(2) 9+2*V(2) 01 114+V(2) (11)B> 11 12 221+V(1) 9 94+22*V(2) 6+2*V(2) 01 114+V(2) <C(33) 33 12 221+V(1) 10 102+24*V(2) -2 01 <C(33) 335+V(2) 12 221+V(1) 11 115+24*V(2) 1 11 (12)A> 335+V(2) 12 221+V(1) 12 165+34*V(2) 11+2*V(2) 116+V(2) (12)A> 12 221+V(1) 13 175+34*V(2) 13+2*V(2) 117+V(2) (11)B> 221+V(1) 14 181+6*V(1)+34*V(2) 15+2*V(1)+2*V(2) 118+V(1)+V(2) (11)B> 15 186+6*V(1)+34*V(2) 12+2*V(1)+2*V(2) 118+V(1)+V(2) <B(21) 20 16 234+12*V(1)+40*V(2) -4 <B(21) 118+V(1)+V(2) 20 17 243+12*V(1)+40*V(2) -1 11 (11)C> 118+V(1)+V(2) 20 18 246+12*V(1)+40*V(2) -4 11 <C(33) 31 117+V(1)+V(2) 20 19 248+12*V(1)+40*V(2) -6 <C(33) 33 31 117+V(1)+V(2) 20 20 259+12*V(1)+40*V(2) -3 01 (11)B> 33 31 117+V(1)+V(2) 20 21 269+12*V(1)+40*V(2) -1 01 11 (11)B> 31 117+V(1)+V(2) 20 22 277+12*V(1)+40*V(2) 1 01 112 (11)B> 117+V(1)+V(2) 20 23 282+12*V(1)+40*V(2) -2 01 112 <C(33) 33 116+V(1)+V(2) 20 24 286+12*V(1)+40*V(2) -6 01 <C(33) 333 116+V(1)+V(2) 20 << Success! ==> defined new CTR 8 (PPA) 843 62173 -185 01 <C(33) 333 1194 20 == Executing PA-CTR 2, V(1)=90, V(2)=2, repcount=31, factor=4/3 1153 111463 -247 01 <C(33) 33127 11 20 1154 111476 -244 11 (12)A> 33127 11 20 1155 112746 10 11128 (12)A> 11 20 1156 112754 12 11129 (11)C> 20 1157 112759 9 11129 <B(21) 10 1158 113533 -249 <B(21) 11129 10 1159 113542 -246 11 (11)C> 11129 10 1160 113545 -249 11 <C(33) 31 11128 10 1161 113547 -251 <C(33) 33 31 11128 10 1162 113558 -248 01 (11)B> 33 31 11128 10 1163 113568 -246 01 11 (11)B> 31 11128 10 1164 113576 -244 01 112 (11)B> 11128 10 1165 113581 -247 01 112 <C(33) 33 11127 10 1166 113585 -251 01 <C(33) 333 11127 10 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 01 <C(33) 334+V(1) 11 20 1 13 3 11 (12)A> 334+V(1) 11 20 2 53+10*V(1) 11+2*V(1) 115+V(1) (12)A> 11 20 3 61+10*V(1) 13+2*V(1) 116+V(1) (11)C> 20 4 66+10*V(1) 10+2*V(1) 116+V(1) <B(21) 10 5 102+16*V(1) -2 <B(21) 116+V(1) 10 6 111+16*V(1) 1 11 (11)C> 116+V(1) 10 7 114+16*V(1) -2 11 <C(33) 31 115+V(1) 10 8 116+16*V(1) -4 <C(33) 33 31 115+V(1) 10 9 127+16*V(1) -1 01 (11)B> 33 31 115+V(1) 10 10 137+16*V(1) 1 01 11 (11)B> 31 115+V(1) 10 11 145+16*V(1) 3 01 112 (11)B> 115+V(1) 10 12 150+16*V(1) 0 01 112 <C(33) 33 114+V(1) 10 13 154+16*V(1) -4 01 <C(33) 333 114+V(1) 10 << Success! ==> defined new CTR 9 (PPA) 1166 113585 -251 01 <C(33) 333 11127 10 == Executing PA-CTR 2, V(1)=123, V(2)=2, repcount=42, factor=4/3 1586 202541 -335 01 <C(33) 33171 11 10 1587 202554 -332 11 (12)A> 33171 11 10 1588 204264 10 11172 (12)A> 11 10 1589 204272 12 11173 (11)C> 10 1590 204275 9 11173 <C(33) 30 1591 204621 -337 <C(33) 33173 30 1592 204632 -334 01 (11)B> 33173 30 1593 206362 12 01 11173 (11)B> 30 1594 206364 14 01 11174 (21)B> 1595 206367 11 01 11174 <B(02) 20 1596 206372 14 01 11174 (11)B> 20 1597 206383 11 01 11174 <B(21) 12 1598 207427 -337 01 <B(21) 11174 12 1599 207431 -339 <A(22) 11175 12 1600 207438 -336 01 (11)B> 11175 12 1601 207443 -339 01 <C(33) 33 11174 12 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 01 <C(33) 331+V(1) 11 10 1 13 3 11 (12)A> 331+V(1) 11 10 2 23+10*V(1) 5+2*V(1) 112+V(1) (12)A> 11 10 3 31+10*V(1) 7+2*V(1) 113+V(1) (11)C> 10 4 34+10*V(1) 4+2*V(1) 113+V(1) <C(33) 30 5 40+12*V(1) -2 <C(33) 333+V(1) 30 6 51+12*V(1) 1 01 (11)B> 333+V(1) 30 7 81+22*V(1) 7+2*V(1) 01 113+V(1) (11)B> 30 8 83+22*V(1) 9+2*V(1) 01 114+V(1) (21)B> 9 86+22*V(1) 6+2*V(1) 01 114+V(1) <B(02) 20 10 91+22*V(1) 9+2*V(1) 01 114+V(1) (11)B> 20 11 102+22*V(1) 6+2*V(1) 01 114+V(1) <B(21) 12 12 126+28*V(1) -2 01 <B(21) 114+V(1) 12 13 130+28*V(1) -4 <A(22) 115+V(1) 12 14 137+28*V(1) -1 01 (11)B> 115+V(1) 12 15 142+28*V(1) -4 01 <C(33) 33 114+V(1) 12 << Success! ==> defined new CTR 10 (PPA) 1601 207443 -339 01 <C(33) 33 11174 12 == Executing PA-CTR 2, V(1)=170, V(2)=0, repcount=57, factor=4/3 2171 366473 -453 01 <C(33) 33229 113 12 == Executing PPA-CTR 4 (once), V(1)=228 2194 375867 -459 01 <C(33) 333 11233 20 == Executing PA-CTR 2, V(1)=229, V(2)=2, repcount=77, factor=4/3 2964 668313 -613 01 <C(33) 33311 112 20 == Executing PPA-CTR 3 (once), V(1)=310 2977 677133 -617 01 <C(33) 33 11314 12 == Executing PA-CTR 2, V(1)=310, V(2)=0, repcount=104, factor=4/3 4017 1201917 -825 01 <C(33) 33417 112 12 == Executing PPA-CTR 5 (once), V(1)=416 4030 1213703 -829 01 <C(33) 33 11421 == Executing PA-CTR 1, V(1)=417, V(2)=0, repcount=140, factor=4/3 5430 2162063 -1109 01 <C(33) 33561 11 == Executing PPA-CTR 6 (once), V(1)=557 5443 2171133 -1113 01 <C(33) 333 11561 12 == Executing PA-CTR 2, V(1)=557, V(2)=2, repcount=186, factor=4/3 7303 3850713 -1485 01 <C(33) 33747 113 12 == Executing PPA-CTR 4 (once), V(1)=746 7326 3880827 -1491 01 <C(33) 333 11751 20 == Executing PA-CTR 2, V(1)=747, V(2)=2, repcount=250, factor=4/3 9826 6906327 -1991 01 <C(33) 331003 11 20 == Executing PPA-CTR 9 (once), V(1)=999 9839 6922465 -1995 01 <C(33) 333 111003 10 == Executing PA-CTR 2, V(1)=999, V(2)=2, repcount=334, factor=4/3 13179 12311221 -2663 01 <C(33) 331339 11 10 == Executing PPA-CTR 10 (once), V(1)=1338 13194 12348827 -2667 01 <C(33) 33 111342 12 == Executing PA-CTR 2, V(1)=1338, V(2)=0, repcount=447, factor=4/3 17664 21963797 -3561 01 <C(33) 331789 11 12 17665 21963810 -3558 11 (12)A> 331789 11 12 17666 21981700 20 111790 (12)A> 11 12 17667 21981708 22 111791 (11)C> 12 17668 21981711 19 111791 <C(33) 32 17669 21985293 -3563 <C(33) 331791 32 17670 21985304 -3560 01 (11)B> 331791 32 17671 22003214 22 01 111791 (11)B> 32 17672 22003216 24 01 111792 (22)A> 17673 22003221 21 01 111792 <B(00) 22 17674 22003231 19 01 111791 <B(21) 12 22 17675 22013977 -3563 01 <B(21) 111791 12 22 17676 22013981 -3565 <A(22) 111792 12 22 17677 22013988 -3562 01 (11)B> 111792 12 22 17678 22013993 -3565 01 <C(33) 33 111791 12 22 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 01 <C(33) 332+V(1) 11 12 1 13 3 11 (12)A> 332+V(1) 11 12 2 33+10*V(1) 7+2*V(1) 113+V(1) (12)A> 11 12 3 41+10*V(1) 9+2*V(1) 114+V(1) (11)C> 12 4 44+10*V(1) 6+2*V(1) 114+V(1) <C(33) 32 5 52+12*V(1) -2 <C(33) 334+V(1) 32 6 63+12*V(1) 1 01 (11)B> 334+V(1) 32 7 103+22*V(1) 9+2*V(1) 01 114+V(1) (11)B> 32 8 105+22*V(1) 11+2*V(1) 01 115+V(1) (22)A> 9 110+22*V(1) 8+2*V(1) 01 115+V(1) <B(00) 22 10 120+22*V(1) 6+2*V(1) 01 114+V(1) <B(21) 12 22 11 144+28*V(1) -2 01 <B(21) 114+V(1) 12 22 12 148+28*V(1) -4 <A(22) 115+V(1) 12 22 13 155+28*V(1) -1 01 (11)B> 115+V(1) 12 22 14 160+28*V(1) -4 01 <C(33) 33 114+V(1) 12 22 << Success! ==> defined new CTR 11 (PPA) 17678 22013993 -3565 01 <C(33) 33 111791 12 22 == Executing PA-CTR 7, V(1)=1787, V(2)=0, repcount=596, factor=4/3 23638 39096545 -4757 01 <C(33) 332385 113 12 22 == Executing PPA-CTR 8 (once), V(1)=0, V(2)=2384 23662 39192191 -4763 01 <C(33) 333 112390 20 == Executing PA-CTR 2, V(1)=2386, V(2)=2, repcount=796, factor=4/3 31622 69686951 -6355 01 <C(33) 333187 112 20 == Executing PPA-CTR 3 (once), V(1)=3186 31635 69776299 -6359 01 <C(33) 33 113190 12 == Executing PA-CTR 2, V(1)=3186, V(2)=0, repcount=1063, factor=4/3 42265 124072213 -8485 01 <C(33) 334253 11 12 == Executing PPA-CTR 11 (once), V(1)=4251 42279 124191401 -8489 01 <C(33) 33 114255 12 22 == Executing PA-CTR 7, V(1)=4251, V(2)=0, repcount=1418, factor=4/3 56459 220782725 -11325 01 <C(33) 335673 11 12 22 56460 220782738 -11322 11 (12)A> 335673 11 12 22 56461 220839468 24 115674 (12)A> 11 12 22 56462 220839476 26 115675 (11)C> 12 22 56463 220839479 23 115675 <C(33) 32 22 56464 220850829 -11327 <C(33) 335675 32 22 56465 220850840 -11324 01 (11)B> 335675 32 22 56466 220907590 26 01 115675 (11)B> 32 22 56467 220907592 28 01 115676 (22)A> 22 56468 220907594 30 01 115676 22 (22)A> 56469 220907599 27 01 115676 22 <B(00) 22 56470 220907601 25 01 115676 <B(00) 00 22 56471 220907611 23 01 115675 <B(21) 12 00 22 56472 220941661 -11327 01 <B(21) 115675 12 00 22 56473 220941665 -11329 <A(22) 115676 12 00 22 56474 220941672 -11326 01 (11)B> 115676 12 00 22 56475 220941677 -11329 01 <C(33) 33 115675 12 00 22 56476 220941690 -11326 11 (12)A> 33 115675 12 00 22 56477 220941700 -11324 112 (12)A> 115675 12 00 22 56478 220941708 -11322 113 (11)C> 115674 12 00 22 56479 220941711 -11325 113 <C(33) 31 115673 12 00 22 56480 220941717 -11331 <C(33) 333 31 115673 12 00 22 56481 220941728 -11328 01 (11)B> 333 31 115673 12 00 22 56482 220941758 -11322 01 113 (11)B> 31 115673 12 00 22 56483 220941766 -11320 01 114 (11)B> 115673 12 00 22 56484 220941771 -11323 01 114 <C(33) 33 115672 12 00 22 56485 220941779 -11331 01 <C(33) 335 115672 12 00 22 >> Try to prove a PA-CTR with 2 Vars... 0 0 0 01 <C(33) 331+V(2) 114+V(1) [*]* [*]* [*]* 1 13 3 11 (12)A> 331+V(2) 114+V(1) [*]* [*]* [*]* 2 23+10*V(2) 5+2*V(2) 112+V(2) (12)A> 114+V(1) [*]* [*]* [*]* 3 31+10*V(2) 7+2*V(2) 113+V(2) (11)C> 113+V(1) [*]* [*]* [*]* 4 34+10*V(2) 4+2*V(2) 113+V(2) <C(33) 31 112+V(1) [*]* [*]* [*]* 5 40+12*V(2) -2 <C(33) 333+V(2) 31 112+V(1) [*]* [*]* [*]* 6 51+12*V(2) 1 01 (11)B> 333+V(2) 31 112+V(1) [*]* [*]* [*]* 7 81+22*V(2) 7+2*V(2) 01 113+V(2) (11)B> 31 112+V(1) [*]* [*]* [*]* 8 89+22*V(2) 9+2*V(2) 01 114+V(2) (11)B> 112+V(1) [*]* [*]* [*]* 9 94+22*V(2) 6+2*V(2) 01 114+V(2) <C(33) 33 111+V(1) [*]* [*]* [*]* 10 102+24*V(2) -2 01 <C(33) 335+V(2) 111+V(1) [*]* [*]* [*]* << Success! ==> defined new CTR 12 (PA) 56485 220941779 -11331 01 <C(33) 335 115672 12 00 22 == Executing PA-CTR 12, V(1)=5668, V(2)=4, repcount=1890, factor=4/3 75385 392686079 -15111 01 <C(33) 337565 112 12 00 22 75386 392686092 -15108 11 (12)A> 337565 112 12 00 22 75387 392761742 22 117566 (12)A> 112 12 00 22 75388 392761750 24 117567 (11)C> 11 12 00 22 75389 392761753 21 117567 <C(33) 31 12 00 22 75390 392776887 -15113 <C(33) 337567 31 12 00 22 75391 392776898 -15110 01 (11)B> 337567 31 12 00 22 75392 392852568 24 01 117567 (11)B> 31 12 00 22 75393 392852576 26 01 117568 (11)B> 12 00 22 75394 392852585 23 01 117568 <B(21) 11 00 22 75395 392897993 -15113 01 <B(21) 117569 00 22 75396 392897997 -15115 <A(22) 117570 00 22 75397 392898004 -15112 01 (11)B> 117570 00 22 75398 392898009 -15115 01 <C(33) 33 117569 00 22 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 01 <C(33) 331+V(1) 112 12 [*]* [*]* 1 13 3 11 (12)A> 331+V(1) 112 12 [*]* [*]* 2 23+10*V(1) 5+2*V(1) 112+V(1) (12)A> 112 12 [*]* [*]* 3 31+10*V(1) 7+2*V(1) 113+V(1) (11)C> 11 12 [*]* [*]* 4 34+10*V(1) 4+2*V(1) 113+V(1) <C(33) 31 12 [*]* [*]* 5 40+12*V(1) -2 <C(33) 333+V(1) 31 12 [*]* [*]* 6 51+12*V(1) 1 01 (11)B> 333+V(1) 31 12 [*]* [*]* 7 81+22*V(1) 7+2*V(1) 01 113+V(1) (11)B> 31 12 [*]* [*]* 8 89+22*V(1) 9+2*V(1) 01 114+V(1) (11)B> 12 [*]* [*]* 9 98+22*V(1) 6+2*V(1) 01 114+V(1) <B(21) 11 [*]* [*]* 10 122+28*V(1) -2 01 <B(21) 115+V(1) [*]* [*]* 11 126+28*V(1) -4 <A(22) 116+V(1) [*]* [*]* 12 133+28*V(1) -1 01 (11)B> 116+V(1) [*]* [*]* 13 138+28*V(1) -4 01 <C(33) 33 115+V(1) [*]* [*]* << Success! ==> defined new CTR 13 (PPA) 75398 392898009 -15115 01 <C(33) 33 117569 00 22 == Executing PA-CTR 7, V(1)=7565, V(2)=0, repcount=2522, factor=4/3 100618 698337429 -20159 01 <C(33) 3310089 113 00 22 100619 698337442 -20156 11 (12)A> 3310089 113 00 22 100620 698438332 22 1110090 (12)A> 113 00 22 100621 698438340 24 1110091 (11)C> 112 00 22 100622 698438343 21 1110091 <C(33) 31 11 00 22 100623 698458525 -20161 <C(33) 3310091 31 11 00 22 100624 698458536 -20158 01 (11)B> 3310091 31 11 00 22 100625 698559446 24 01 1110091 (11)B> 31 11 00 22 100626 698559454 26 01 1110092 (11)B> 11 00 22 100627 698559459 23 01 1110092 <C(33) 33 00 22 100628 698579643 -20161 01 <C(33) 3310093 00 22 100629 698579656 -20158 11 (12)A> 3310093 00 22 100630 698680586 28 1110094 (12)A> 00 22 100631 698680598 30 1110095 (11)B> 22 100632 698680604 32 1110096 (11)B> 100633 698680609 29 1110096 <B(21) 20 100634 698741185 -20163 <B(21) 1110096 20 100635 698741194 -20160 11 (11)C> 1110096 20 100636 698741197 -20163 11 <C(33) 31 1110095 20 100637 698741199 -20165 <C(33) 33 31 1110095 20 100638 698741210 -20162 01 (11)B> 33 31 1110095 20 100639 698741220 -20160 01 11 (11)B> 31 1110095 20 100640 698741228 -20158 01 112 (11)B> 1110095 20 100641 698741233 -20161 01 112 <C(33) 33 1110094 20 100642 698741237 -20165 01 <C(33) 333 1110094 20 >> Try to prove a PPA-CTR with 2 Vars... 0 0 0 01 <C(33) 331+V(2) 113 00 221+V(1) 1 13 3 11 (12)A> 331+V(2) 113 00 221+V(1) 2 23+10*V(2) 5+2*V(2) 112+V(2) (12)A> 113 00 221+V(1) 3 31+10*V(2) 7+2*V(2) 113+V(2) (11)C> 112 00 221+V(1) 4 34+10*V(2) 4+2*V(2) 113+V(2) <C(33) 31 11 00 221+V(1) 5 40+12*V(2) -2 <C(33) 333+V(2) 31 11 00 221+V(1) 6 51+12*V(2) 1 01 (11)B> 333+V(2) 31 11 00 221+V(1) 7 81+22*V(2) 7+2*V(2) 01 113+V(2) (11)B> 31 11 00 221+V(1) 8 89+22*V(2) 9+2*V(2) 01 114+V(2) (11)B> 11 00 221+V(1) 9 94+22*V(2) 6+2*V(2) 01 114+V(2) <C(33) 33 00 221+V(1) 10 102+24*V(2) -2 01 <C(33) 335+V(2) 00 221+V(1) 11 115+24*V(2) 1 11 (12)A> 335+V(2) 00 221+V(1) 12 165+34*V(2) 11+2*V(2) 116+V(2) (12)A> 00 221+V(1) 13 177+34*V(2) 13+2*V(2) 117+V(2) (11)B> 221+V(1) 14 183+6*V(1)+34*V(2) 15+2*V(1)+2*V(2) 118+V(1)+V(2) (11)B> 15 188+6*V(1)+34*V(2) 12+2*V(1)+2*V(2) 118+V(1)+V(2) <B(21) 20 16 236+12*V(1)+40*V(2) -4 <B(21) 118+V(1)+V(2) 20 17 245+12*V(1)+40*V(2) -1 11 (11)C> 118+V(1)+V(2) 20 18 248+12*V(1)+40*V(2) -4 11 <C(33) 31 117+V(1)+V(2) 20 19 250+12*V(1)+40*V(2) -6 <C(33) 33 31 117+V(1)+V(2) 20 20 261+12*V(1)+40*V(2) -3 01 (11)B> 33 31 117+V(1)+V(2) 20 21 271+12*V(1)+40*V(2) -1 01 11 (11)B> 31 117+V(1)+V(2) 20 22 279+12*V(1)+40*V(2) 1 01 112 (11)B> 117+V(1)+V(2) 20 23 284+12*V(1)+40*V(2) -2 01 112 <C(33) 33 116+V(1)+V(2) 20 24 288+12*V(1)+40*V(2) -6 01 <C(33) 333 116+V(1)+V(2) 20 << Success! ==> defined new CTR 14 (PPA) 100642 698741237 -20165 01 <C(33) 333 1110094 20 == Executing PA-CTR 2, V(1)=10090, V(2)=2, repcount=3364, factor=4/3 134282 1242276173 -26893 01 <C(33) 3313459 112 20 == Executing PPA-CTR 3 (once), V(1)=13458 134295 1242653137 -26897 01 <C(33) 33 1113462 12 == Executing PA-CTR 2, V(1)=13458, V(2)=0, repcount=4487, factor=4/3 179165 2209287547 -35871 01 <C(33) 3317949 11 12 == Executing PPA-CTR 11 (once), V(1)=17947 179179 2209790223 -35875 01 <C(33) 33 1117951 12 22 == Executing PA-CTR 7, V(1)=17947, V(2)=0, repcount=5983, factor=4/3 239009 3928335177 -47841 01 <C(33) 3323933 112 12 22 239010 3928335190 -47838 11 (12)A> 3323933 112 12 22 239011 3928574520 28 1123934 (12)A> 112 12 22 239012 3928574528 30 1123935 (11)C> 11 12 22 239013 3928574531 27 1123935 <C(33) 31 12 22 239014 3928622401 -47843 <C(33) 3323935 31 12 22 239015 3928622412 -47840 01 (11)B> 3323935 31 12 22 239016 3928861762 30 01 1123935 (11)B> 31 12 22 239017 3928861770 32 01 1123936 (11)B> 12 22 239018 3928861779 29 01 1123936 <B(21) 11 22 239019 3929005395 -47843 01 <B(21) 1123937 22 239020 3929005399 -47845 <A(22) 1123938 22 239021 3929005406 -47842 01 (11)B> 1123938 22 239022 3929005411 -47845 01 <C(33) 33 1123937 22 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 01 <C(33) 331+V(1) 112 12 [*]* 1 13 3 11 (12)A> 331+V(1) 112 12 [*]* 2 23+10*V(1) 5+2*V(1) 112+V(1) (12)A> 112 12 [*]* 3 31+10*V(1) 7+2*V(1) 113+V(1) (11)C> 11 12 [*]* 4 34+10*V(1) 4+2*V(1) 113+V(1) <C(33) 31 12 [*]* 5 40+12*V(1) -2 <C(33) 333+V(1) 31 12 [*]* 6 51+12*V(1) 1 01 (11)B> 333+V(1) 31 12 [*]* 7 81+22*V(1) 7+2*V(1) 01 113+V(1) (11)B> 31 12 [*]* 8 89+22*V(1) 9+2*V(1) 01 114+V(1) (11)B> 12 [*]* 9 98+22*V(1) 6+2*V(1) 01 114+V(1) <B(21) 11 [*]* 10 122+28*V(1) -2 01 <B(21) 115+V(1) [*]* 11 126+28*V(1) -4 <A(22) 116+V(1) [*]* 12 133+28*V(1) -1 01 (11)B> 116+V(1) [*]* 13 138+28*V(1) -4 01 <C(33) 33 115+V(1) [*]* << Success! ==> defined new CTR 15 (PPA) 239022 3929005411 -47845 01 <C(33) 33 1123937 22 == Executing PA-CTR 2, V(1)=23933, V(2)=0, repcount=7978, factor=4/3 318802 6984563455 -63801 01 <C(33) 3331913 113 22 318803 6984563468 -63798 11 (12)A> 3331913 113 22 318804 6984882598 28 1131914 (12)A> 113 22 318805 6984882606 30 1131915 (11)C> 112 22 318806 6984882609 27 1131915 <C(33) 31 11 22 318807 6984946439 -63803 <C(33) 3331915 31 11 22 318808 6984946450 -63800 01 (11)B> 3331915 31 11 22 318809 6985265600 30 01 1131915 (11)B> 31 11 22 318810 6985265608 32 01 1131916 (11)B> 11 22 318811 6985265613 29 01 1131916 <C(33) 33 22 318812 6985329445 -63803 01 <C(33) 3331917 22 318813 6985329458 -63800 11 (12)A> 3331917 22 318814 6985648628 34 1131918 (12)A> 22 318815 6985648630 36 1131918 12 (22)A> 318816 6985648635 33 1131918 12 <B(00) 22 318817 6985648643 31 1131918 <B(21) 20 22 318818 6985840151 -63805 <B(21) 1131918 20 22 318819 6985840160 -63802 11 (11)C> 1131918 20 22 318820 6985840163 -63805 11 <C(33) 31 1131917 20 22 318821 6985840165 -63807 <C(33) 33 31 1131917 20 22 318822 6985840176 -63804 01 (11)B> 33 31 1131917 20 22 318823 6985840186 -63802 01 11 (11)B> 31 1131917 20 22 318824 6985840194 -63800 01 112 (11)B> 1131917 20 22 318825 6985840199 -63803 01 112 <C(33) 33 1131916 20 22 318826 6985840203 -63807 01 <C(33) 333 1131916 20 22 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 01 <C(33) 331+V(1) 113 22 1 13 3 11 (12)A> 331+V(1) 113 22 2 23+10*V(1) 5+2*V(1) 112+V(1) (12)A> 113 22 3 31+10*V(1) 7+2*V(1) 113+V(1) (11)C> 112 22 4 34+10*V(1) 4+2*V(1) 113+V(1) <C(33) 31 11 22 5 40+12*V(1) -2 <C(33) 333+V(1) 31 11 22 6 51+12*V(1) 1 01 (11)B> 333+V(1) 31 11 22 7 81+22*V(1) 7+2*V(1) 01 113+V(1) (11)B> 31 11 22 8 89+22*V(1) 9+2*V(1) 01 114+V(1) (11)B> 11 22 9 94+22*V(1) 6+2*V(1) 01 114+V(1) <C(33) 33 22 10 102+24*V(1) -2 01 <C(33) 335+V(1) 22 11 115+24*V(1) 1 11 (12)A> 335+V(1) 22 12 165+34*V(1) 11+2*V(1) 116+V(1) (12)A> 22 13 167+34*V(1) 13+2*V(1) 116+V(1) 12 (22)A> 14 172+34*V(1) 10+2*V(1) 116+V(1) 12 <B(00) 22 15 180+34*V(1) 8+2*V(1) 116+V(1) <B(21) 20 22 16 216+40*V(1) -4 <B(21) 116+V(1) 20 22 17 225+40*V(1) -1 11 (11)C> 116+V(1) 20 22 18 228+40*V(1) -4 11 <C(33) 31 115+V(1) 20 22 19 230+40*V(1) -6 <C(33) 33 31 115+V(1) 20 22 20 241+40*V(1) -3 01 (11)B> 33 31 115+V(1) 20 22 21 251+40*V(1) -1 01 11 (11)B> 31 115+V(1) 20 22 22 259+40*V(1) 1 01 112 (11)B> 115+V(1) 20 22 23 264+40*V(1) -2 01 112 <C(33) 33 114+V(1) 20 22 24 268+40*V(1) -6 01 <C(33) 333 114+V(1) 20 22 << Success! ==> defined new CTR 16 (PPA) 318826 6985840203 -63807 01 <C(33) 333 1131916 20 22 == Executing PA-CTR 7, V(1)=31912, V(2)=2, repcount=10638, factor=4/3 425206 12418943391 -85083 01 <C(33) 3342555 112 20 22 425207 12418943404 -85080 11 (12)A> 3342555 112 20 22 425208 12419368954 30 1142556 (12)A> 112 20 22 425209 12419368962 32 1142557 (11)C> 11 20 22 425210 12419368965 29 1142557 <C(33) 31 20 22 425211 12419454079 -85085 <C(33) 3342557 31 20 22 425212 12419454090 -85082 01 (11)B> 3342557 31 20 22 425213 12419879660 32 01 1142557 (11)B> 31 20 22 425214 12419879668 34 01 1142558 (11)B> 20 22 425215 12419879679 31 01 1142558 <B(21) 12 22 425216 12420135027 -85085 01 <B(21) 1142558 12 22 425217 12420135031 -85087 <A(22) 1142559 12 22 425218 12420135038 -85084 01 (11)B> 1142559 12 22 425219 12420135043 -85087 01 <C(33) 33 1142558 12 22 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 01 <C(33) 331+V(1) 112 20 [*]* 1 13 3 11 (12)A> 331+V(1) 112 20 [*]* 2 23+10*V(1) 5+2*V(1) 112+V(1) (12)A> 112 20 [*]* 3 31+10*V(1) 7+2*V(1) 113+V(1) (11)C> 11 20 [*]* 4 34+10*V(1) 4+2*V(1) 113+V(1) <C(33) 31 20 [*]* 5 40+12*V(1) -2 <C(33) 333+V(1) 31 20 [*]* 6 51+12*V(1) 1 01 (11)B> 333+V(1) 31 20 [*]* 7 81+22*V(1) 7+2*V(1) 01 113+V(1) (11)B> 31 20 [*]* 8 89+22*V(1) 9+2*V(1) 01 114+V(1) (11)B> 20 [*]* 9 100+22*V(1) 6+2*V(1) 01 114+V(1) <B(21) 12 [*]* 10 124+28*V(1) -2 01 <B(21) 114+V(1) 12 [*]* 11 128+28*V(1) -4 <A(22) 115+V(1) 12 [*]* 12 135+28*V(1) -1 01 (11)B> 115+V(1) 12 [*]* 13 140+28*V(1) -4 01 <C(33) 33 114+V(1) 12 [*]* << Success! ==> defined new CTR 17 (PPA) 425219 12420135043 -85087 01 <C(33) 33 1142558 12 22 == Executing PA-CTR 7, V(1)=42554, V(2)=0, repcount=14185, factor=4/3 567069 22079183833 -113457 01 <C(33) 3356741 113 12 22 == Executing PPA-CTR 8 (once), V(1)=0, V(2)=56740 567093 22081453719 -113463 01 <C(33) 333 1156746 20 == Executing PA-CTR 2, V(1)=56742, V(2)=2, repcount=18915, factor=4/3 756243 39256689849 -151293 01 <C(33) 3375663 11 20 == Executing PPA-CTR 9 (once), V(1)=75659 756256 39257900547 -151297 01 <C(33) 333 1175663 10 == Executing PA-CTR 2, V(1)=75659, V(2)=2, repcount=25220, factor=4/3 1008456 69790796187 -201737 01 <C(33) 33100883 113 10 1008457 69790796200 -201734 11 (12)A> 33100883 113 10 1008458 69791805030 32 11100884 (12)A> 113 10 1008459 69791805038 34 11100885 (11)C> 112 10 1008460 69791805041 31 11100885 <C(33) 31 11 10 1008461 69792006811 -201739 <C(33) 33100885 31 11 10 1008462 69792006822 -201736 01 (11)B> 33100885 31 11 10 1008463 69793015672 34 01 11100885 (11)B> 31 11 10 1008464 69793015680 36 01 11100886 (11)B> 11 10 1008465 69793015685 33 01 11100886 <C(33) 33 10 1008466 69793217457 -201739 01 <C(33) 33100887 10 1008467 69793217470 -201736 11 (12)A> 33100887 10 1008468 69794226340 38 11100888 (12)A> 10 1008469 69794226355 35 11100888 <B(21) 12 1008470 69794831683 -201741 <B(21) 11100888 12 1008471 69794831692 -201738 11 (11)C> 11100888 12 1008472 69794831695 -201741 11 <C(33) 31 11100887 12 1008473 69794831697 -201743 <C(33) 33 31 11100887 12 1008474 69794831708 -201740 01 (11)B> 33 31 11100887 12 1008475 69794831718 -201738 01 11 (11)B> 31 11100887 12 1008476 69794831726 -201736 01 112 (11)B> 11100887 12 1008477 69794831731 -201739 01 112 <C(33) 33 11100886 12 1008478 69794831735 -201743 01 <C(33) 333 11100886 12 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 01 <C(33) 331+V(1) 113 10 1 13 3 11 (12)A> 331+V(1) 113 10 2 23+10*V(1) 5+2*V(1) 112+V(1) (12)A> 113 10 3 31+10*V(1) 7+2*V(1) 113+V(1) (11)C> 112 10 4 34+10*V(1) 4+2*V(1) 113+V(1) <C(33) 31 11 10 5 40+12*V(1) -2 <C(33) 333+V(1) 31 11 10 6 51+12*V(1) 1 01 (11)B> 333+V(1) 31 11 10 7 81+22*V(1) 7+2*V(1) 01 113+V(1) (11)B> 31 11 10 8 89+22*V(1) 9+2*V(1) 01 114+V(1) (11)B> 11 10 9 94+22*V(1) 6+2*V(1) 01 114+V(1) <C(33) 33 10 10 102+24*V(1) -2 01 <C(33) 335+V(1) 10 11 115+24*V(1) 1 11 (12)A> 335+V(1) 10 12 165+34*V(1) 11+2*V(1) 116+V(1) (12)A> 10 13 180+34*V(1) 8+2*V(1) 116+V(1) <B(21) 12 14 216+40*V(1) -4 <B(21) 116+V(1) 12 15 225+40*V(1) -1 11 (11)C> 116+V(1) 12 16 228+40*V(1) -4 11 <C(33) 31 115+V(1) 12 17 230+40*V(1) -6 <C(33) 33 31 115+V(1) 12 18 241+40*V(1) -3 01 (11)B> 33 31 115+V(1) 12 19 251+40*V(1) -1 01 11 (11)B> 31 115+V(1) 12 20 259+40*V(1) 1 01 112 (11)B> 115+V(1) 12 21 264+40*V(1) -2 01 112 <C(33) 33 114+V(1) 12 22 268+40*V(1) -6 01 <C(33) 333 114+V(1) 12 << Success! ==> defined new CTR 18 (PPA) 1008478 69794831735 -201743 01 <C(33) 333 11100886 12 == Executing PA-CTR 2, V(1)=100882, V(2)=2, repcount=33628, factor=4/3 1344758 124078696223 -268999 01 <C(33) 33134515 112 12 == Executing PPA-CTR 5 (once), V(1)=134514 1344771 124082462753 -269003 01 <C(33) 33 11134519 == Executing PA-CTR 1, V(1)=134515, V(2)=0, repcount=44839, factor=4/3 1793161 220590608267 -358681 01 <C(33) 33179357 112 1793162 220590608280 -358678 11 (12)A> 33179357 112 1793163 220592401850 36 11179358 (12)A> 112 1793164 220592401858 38 11179359 (11)C> 11 1793165 220592401861 35 11179359 <C(33) 31 1793166 220592760579 -358683 <C(33) 33179359 31 1793167 220592760590 -358680 01 (11)B> 33179359 31 1793168 220594554180 38 01 11179359 (11)B> 31 1793169 220594554188 40 01 11179360 (11)B> 1793170 220594554193 37 01 11179360 <B(21) 20 1793171 220595630353 -358683 01 <B(21) 11179360 20 1793172 220595630357 -358685 <A(22) 11179361 20 1793173 220595630364 -358682 01 (11)B> 11179361 20 1793174 220595630369 -358685 01 <C(33) 33 11179360 20 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 01 <C(33) 331+V(1) 112 1 13 3 11 (12)A> 331+V(1) 112 2 23+10*V(1) 5+2*V(1) 112+V(1) (12)A> 112 3 31+10*V(1) 7+2*V(1) 113+V(1) (11)C> 11 4 34+10*V(1) 4+2*V(1) 113+V(1) <C(33) 31 5 40+12*V(1) -2 <C(33) 333+V(1) 31 6 51+12*V(1) 1 01 (11)B> 333+V(1) 31 7 81+22*V(1) 7+2*V(1) 01 113+V(1) (11)B> 31 8 89+22*V(1) 9+2*V(1) 01 114+V(1) (11)B> 9 94+22*V(1) 6+2*V(1) 01 114+V(1) <B(21) 20 10 118+28*V(1) -2 01 <B(21) 114+V(1) 20 11 122+28*V(1) -4 <A(22) 115+V(1) 20 12 129+28*V(1) -1 01 (11)B> 115+V(1) 20 13 134+28*V(1) -4 01 <C(33) 33 114+V(1) 20 << Success! ==> defined new CTR 19 (PPA) 1793174 220595630369 -358685 01 <C(33) 33 11179360 20 == Executing PA-CTR 2, V(1)=179356, V(2)=0, repcount=59786, factor=4/3 2391034 392168417021 -478257 01 <C(33) 33239145 112 20 == Executing PPA-CTR 3 (once), V(1)=239144 2391047 392175113193 -478261 01 <C(33) 33 11239148 12 == Executing PA-CTR 2, V(1)=239144, V(2)=0, repcount=79715, factor=4/3 3188197 697194516603 -637691 01 <C(33) 33318861 113 12 == Executing PPA-CTR 4 (once), V(1)=318860 3188220 697207271277 -637697 01 <C(33) 333 11318865 20 == Executing PA-CTR 2, V(1)=318861, V(2)=2, repcount=106288, factor=4/3 4251100 1239480781965 -850273 01 <C(33) 33425155 11 20 == Executing PPA-CTR 9 (once), V(1)=425151 4251113 1239487584535 -850277 01 <C(33) 333 11425155 10 == Executing PA-CTR 2, V(1)=425151, V(2)=2, repcount=141718, factor=4/3 5668293 2203533632923 -1133713 01 <C(33) 33566875 11 10 == Executing PPA-CTR 10 (once), V(1)=566874 5668308 2203549505537 -1133717 01 <C(33) 33 11566878 12 == Executing PA-CTR 2, V(1)=566874, V(2)=0, repcount=188959, factor=4/3 7557898 3917423886011 -1511635 01 <C(33) 33755837 11 12 == Executing PPA-CTR 11 (once), V(1)=755835 7557912 3917445049551 -1511639 01 <C(33) 33 11755839 12 22 == Executing PA-CTR 7, V(1)=755835, V(2)=0, repcount=251946, factor=4/3 10077372 6964344426603 -2015531 01 <C(33) 331007785 11 12 22 10077373 6964344426616 -2015528 11 (12)A> 331007785 11 12 22 10077374 6964354504466 42 111007786 (12)A> 11 12 22 10077375 6964354504474 44 111007787 (11)C> 12 22 10077376 6964354504477 41 111007787 <C(33) 32 22 10077377 6964356520051 -2015533 <C(33) 331007787 32 22 10077378 6964356520062 -2015530 01 (11)B> 331007787 32 22 10077379 6964366597932 44 01 111007787 (11)B> 32 22 10077380 6964366597934 46 01 111007788 (22)A> 22 10077381 6964366597936 48 01 111007788 22 (22)A> 10077382 6964366597941 45 01 111007788 22 <B(00) 22 10077383 6964366597943 43 01 111007788 <B(00) 00 22 10077384 6964366597953 41 01 111007787 <B(21) 12 00 22 10077385 6964372644675 -2015533 01 <B(21) 111007787 12 00 22 10077386 6964372644679 -2015535 <A(22) 111007788 12 00 22 10077387 6964372644686 -2015532 01 (11)B> 111007788 12 00 22 10077388 6964372644691 -2015535 01 <C(33) 33 111007787 12 00 22 >> Try to prove a PPA-CTR with 2 Vars... 0 0 0 01 <C(33) 332+V(2) 11 12 221+V(1) 1 13 3 11 (12)A> 332+V(2) 11 12 221+V(1) 2 33+10*V(2) 7+2*V(2) 113+V(2) (12)A> 11 12 221+V(1) 3 41+10*V(2) 9+2*V(2) 114+V(2) (11)C> 12 221+V(1) 4 44+10*V(2) 6+2*V(2) 114+V(2) <C(33) 32 221+V(1) 5 52+12*V(2) -2 <C(33) 334+V(2) 32 221+V(1) 6 63+12*V(2) 1 01 (11)B> 334+V(2) 32 221+V(1) 7 103+22*V(2) 9+2*V(2) 01 114+V(2) (11)B> 32 221+V(1) 8 105+22*V(2) 11+2*V(2) 01 115+V(2) (22)A> 221+V(1) 9 107+2*V(1)+22*V(2) 13+2*V(1)+2*V(2) 01 115+V(2) 221+V(1) (22)A> 10 112+2*V(1)+22*V(2) 10+2*V(1)+2*V(2) 01 115+V(2) 221+V(1) <B(00) 22 11 114+4*V(1)+22*V(2) 8+2*V(2) 01 115+V(2) <B(00) 001+V(1) 22 12 124+4*V(1)+22*V(2) 6+2*V(2) 01 114+V(2) <B(21) 12 001+V(1) 22 13 148+4*V(1)+28*V(2) -2 01 <B(21) 114+V(2) 12 001+V(1) 22 14 152+4*V(1)+28*V(2) -4 <A(22) 115+V(2) 12 001+V(1) 22 15 159+4*V(1)+28*V(2) -1 01 (11)B> 115+V(2) 12 001+V(1) 22 16 164+4*V(1)+28*V(2) -4 01 <C(33) 33 114+V(2) 12 001+V(1) 22 << Success! ==> defined new CTR 20 (PPA) 10077388 6964372644691 -2015535 01 <C(33) 33 111007787 12 00 22 == Executing PA-CTR 12, V(1)=1007783, V(2)=0, repcount=335928, factor=4/3 13436668 12381076601635 -2687391 01 <C(33) 331343713 113 12 00 22 13436669 12381076601648 -2687388 11 (12)A> 331343713 113 12 00 22 13436670 12381090038778 38 111343714 (12)A> 113 12 00 22 13436671 12381090038786 40 111343715 (11)C> 112 12 00 22 13436672 12381090038789 37 111343715 <C(33) 31 11 12 00 22 13436673 12381092726219 -2687393 <C(33) 331343715 31 11 12 00 22 13436674 12381092726230 -2687390 01 (11)B> 331343715 31 11 12 00 22 13436675 12381106163380 40 01 111343715 (11)B> 31 11 12 00 22 13436676 12381106163388 42 01 111343716 (11)B> 11 12 00 22 13436677 12381106163393 39 01 111343716 <C(33) 33 12 00 22 13436678 12381108850825 -2687393 01 <C(33) 331343717 12 00 22 13436679 12381108850838 -2687390 11 (12)A> 331343717 12 00 22 13436680 12381122288008 44 111343718 (12)A> 12 00 22 13436681 12381122288018 46 111343719 (11)B> 00 22 13436682 12381122288023 43 111343719 <B(21) 20 22 13436683 12381130350337 -2687395 <B(21) 111343719 20 22 13436684 12381130350346 -2687392 11 (11)C> 111343719 20 22 13436685 12381130350349 -2687395 11 <C(33) 31 111343718 20 22 13436686 12381130350351 -2687397 <C(33) 33 31 111343718 20 22 13436687 12381130350362 -2687394 01 (11)B> 33 31 111343718 20 22 13436688 12381130350372 -2687392 01 11 (11)B> 31 111343718 20 22 13436689 12381130350380 -2687390 01 112 (11)B> 111343718 20 22 13436690 12381130350385 -2687393 01 112 <C(33) 33 111343717 20 22 13436691 12381130350389 -2687397 01 <C(33) 333 111343717 20 22 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 01 <C(33) 331+V(1) 113 12 00 [*]* 1 13 3 11 (12)A> 331+V(1) 113 12 00 [*]* 2 23+10*V(1) 5+2*V(1) 112+V(1) (12)A> 113 12 00 [*]* 3 31+10*V(1) 7+2*V(1) 113+V(1) (11)C> 112 12 00 [*]* 4 34+10*V(1) 4+2*V(1) 113+V(1) <C(33) 31 11 12 00 [*]* 5 40+12*V(1) -2 <C(33) 333+V(1) 31 11 12 00 [*]* 6 51+12*V(1) 1 01 (11)B> 333+V(1) 31 11 12 00 [*]* 7 81+22*V(1) 7+2*V(1) 01 113+V(1) (11)B> 31 11 12 00 [*]* 8 89+22*V(1) 9+2*V(1) 01 114+V(1) (11)B> 11 12 00 [*]* 9 94+22*V(1) 6+2*V(1) 01 114+V(1) <C(33) 33 12 00 [*]* 10 102+24*V(1) -2 01 <C(33) 335+V(1) 12 00 [*]* 11 115+24*V(1) 1 11 (12)A> 335+V(1) 12 00 [*]* 12 165+34*V(1) 11+2*V(1) 116+V(1) (12)A> 12 00 [*]* 13 175+34*V(1) 13+2*V(1) 117+V(1) (11)B> 00 [*]* 14 180+34*V(1) 10+2*V(1) 117+V(1) <B(21) 20 [*]* 15 222+40*V(1) -4 <B(21) 117+V(1) 20 [*]* 16 231+40*V(1) -1 11 (11)C> 117+V(1) 20 [*]* 17 234+40*V(1) -4 11 <C(33) 31 116+V(1) 20 [*]* 18 236+40*V(1) -6 <C(33) 33 31 116+V(1) 20 [*]* 19 247+40*V(1) -3 01 (11)B> 33 31 116+V(1) 20 [*]* 20 257+40*V(1) -1 01 11 (11)B> 31 116+V(1) 20 [*]* 21 265+40*V(1) 1 01 112 (11)B> 116+V(1) 20 [*]* 22 270+40*V(1) -2 01 112 <C(33) 33 115+V(1) 20 [*]* 23 274+40*V(1) -6 01 <C(33) 333 115+V(1) 20 [*]* << Success! ==> defined new CTR 21 (PPA) 13436691 12381130350389 -2687397 01 <C(33) 333 111343717 20 22 == Executing PA-CTR 7, V(1)=1343713, V(2)=2, repcount=447905, factor=4/3 17915741 22010882709899 -3583207 01 <C(33) 331791623 112 20 22 == Executing PPA-CTR 17 (once), V(1)=1791622 17915754 22010932875455 -3583211 01 <C(33) 33 111791626 12 22 == Executing PA-CTR 7, V(1)=1791622, V(2)=0, repcount=597208, factor=4/3 23887834 39130520097359 -4777627 01 <C(33) 332388833 112 12 22 == Executing PPA-CTR 15 (once), V(1)=2388832 23887847 39130586984793 -4777631 01 <C(33) 33 112388837 22 == Executing PA-CTR 2, V(1)=2388833, V(2)=0, repcount=796278, factor=4/3 31850627 69565445341437 -6370187 01 <C(33) 333185113 113 22 == Executing PPA-CTR 16 (once), V(1)=3185112 31850651 69565572746185 -6370193 01 <C(33) 333 113185116 20 22 == Executing PA-CTR 7, V(1)=3185112, V(2)=2, repcount=1061705, factor=4/3 42467701 123672121377295 -8493603 01 <C(33) 334246823 11 20 22 42467702 123672121377308 -8493600 11 (12)A> 334246823 11 20 22 42467703 123672163845538 46 114246824 (12)A> 11 20 22 42467704 123672163845546 48 114246825 (11)C> 20 22 42467705 123672163845551 45 114246825 <B(21) 10 22 42467706 123672189326501 -8493605 <B(21) 114246825 10 22 42467707 123672189326510 -8493602 11 (11)C> 114246825 10 22 42467708 123672189326513 -8493605 11 <C(33) 31 114246824 10 22 42467709 123672189326515 -8493607 <C(33) 33 31 114246824 10 22 42467710 123672189326526 -8493604 01 (11)B> 33 31 114246824 10 22 42467711 123672189326536 -8493602 01 11 (11)B> 31 114246824 10 22 42467712 123672189326544 -8493600 01 112 (11)B> 114246824 10 22 42467713 123672189326549 -8493603 01 112 <C(33) 33 114246823 10 22 42467714 123672189326553 -8493607 01 <C(33) 333 114246823 10 22 >> Try to prove a PPA-CTR with 1 Vars... 0 0 0 01 <C(33) 334+V(1) 11 20 [*]* 1 13 3 11 (12)A> 334+V(1) 11 20 [*]* 2 53+10*V(1) 11+2*V(1) 115+V(1) (12)A> 11 20 [*]* 3 61+10*V(1) 13+2*V(1) 116+V(1) (11)C> 20 [*]* 4 66+10*V(1) 10+2*V(1) 116+V(1) <B(21) 10 [*]* 5 102+16*V(1) -2 <B(21) 116+V(1) 10 [*]* 6 111+16*V(1) 1 11 (11)C> 116+V(1) 10 [*]* 7 114+16*V(1) -2 11 <C(33) 31 115+V(1) 10 [*]* 8 116+16*V(1) -4 <C(33) 33 31 115+V(1) 10 [*]* 9 127+16*V(1) -1 01 (11)B> 33 31 115+V(1) 10 [*]* 10 137+16*V(1) 1 01 11 (11)B> 31 115+V(1) 10 [*]* 11 145+16*V(1) 3 01 112 (11)B> 115+V(1) 10 [*]* 12 150+16*V(1) 0 01 112 <C(33) 33 114+V(1) 10 [*]* 13 154+16*V(1) -4 01 <C(33) 333 114+V(1) 10 [*]* << Success! ==> defined new CTR 22 (PPA) 42467714 123672189326553 -8493607 01 <C(33) 333 114246823 10 22 == Executing PA-CTR 7, V(1)=4246819, V(2)=2, repcount=1415607, factor=4/3 56623784 219861606284019 -11324821 01 <C(33) 335662431 112 10 22 56623785 219861606284032 -11324818 11 (12)A> 335662431 112 10 22 56623786 219861662908342 44 115662432 (12)A> 112 10 22 56623787 219861662908350 46 115662433 (11)C> 11 10 22 56623788 219861662908353 43 115662433 <C(33) 31 10 22 56623789 219861674233219 -11324823 <C(33) 335662433 31 10 22 56623790 219861674233230 -11324820 01 (11)B> 335662433 31 10 22 56623791 219861730857560 46 01 115662433 (11)B> 31 10 22 56623792 219861730857568 48 01 115662434 (11)B> 10 22 56623793 219861730857570 50 01 115662435 (11)B> 22 56623794 219861730857576 52 01 115662436 (11)B> 56623795 219861730857581 49 01 115662436 <B(21) 20 56623796 219861764832197 -11324823 01 <B(21) 115662436 20 56623797 219861764832201 -11324825 <A(22) 115662437 20 56623798 219861764832208 -11324822 01 (11)B> 115662437 20 56623799 219861764832213 -11324825 01 <C(33) 33 115662436 20 >> Try to prove a PPA-CTR with 3 Vars... 0 0 0 01 <C(33) 331+V(3) 112 101+V(2) 221+V(1) 1 13 3 11 (12)A> 331+V(3) 112 101+V(2) 221+V(1) 2 23+10*V(3) 5+2*V(3) 112+V(3) (12)A> 112 101+V(2) 221+V(1) 3 31+10*V(3) 7+2*V(3) 113+V(3) (11)C> 11 101+V(2) 221+V(1) 4 34+10*V(3) 4+2*V(3) 113+V(3) <C(33) 31 101+V(2) 221+V(1) 5 40+12*V(3) -2 <C(33) 333+V(3) 31 101+V(2) 221+V(1) 6 51+12*V(3) 1 01 (11)B> 333+V(3) 31 101+V(2) 221+V(1) 7 81+22*V(3) 7+2*V(3) 01 113+V(3) (11)B> 31 101+V(2) 221+V(1) 8 89+22*V(3) 9+2*V(3) 01 114+V(3) (11)B> 101+V(2) 221+V(1) 9 91+2*V(2)+22*V(3) 11+2*V(2)+2*V(3) 01 115+V(2)+V(3) (11)B> 221+V(1) 10 97+6*V(1)+2*V(2)+22*V(3) 13+2*V(1)+2*V(2)+2*V(3) 01 116+V(1)+V(2)+V(3) (11)B> 11 102+6*V(1)+2*V(2)+22*V(3) 10+2*V(1)+2*V(2)+2*V(3) 01 116+V(1)+V(2)+V(3) <B(21) 20 12 138+12*V(1)+8*V(2)+28*V(3) -2 01 <B(21) 116+V(1)+V(2)+V(3) 20 13 142+12*V(1)+8*V(2)+28*V(3) -4 <A(22) 117+V(1)+V(2)+V(3) 20 14 149+12*V(1)+8*V(2)+28*V(3) -1 01 (11)B> 117+V(1)+V(2)+V(3) 20 15 154+12*V(1)+8*V(2)+28*V(3) -4 01 <C(33) 33 116+V(1)+V(2)+V(3) 20 << Success! ==> defined new CTR 23 (PPA) 56623799 219861764832213 -11324825 01 <C(33) 33 115662436 20 == Executing PA-CTR 2, V(1)=5662432, V(2)=0, repcount=1887478, factor=4/3 75498579 390865380379257 -15099781 01 <C(33) 337549913 112 20 == Executing PPA-CTR 3 (once), V(1)=7549912 75498592 390865591776933 -15099785 01 <C(33) 33 117549916 12 == Executing PA-CTR 2, V(1)=7549912, V(2)=0, repcount=2516638, factor=4/3 100664972 694872135181497 -20133061 01 <C(33) 3310066553 112 12 Lines: 500 Top steps: 499 Macro steps: 100664972 Basic steps: 694872135181497 Tape index: -20133061 nonzeros: 20133115 log10(nonzeros): 7.304 log10(steps ): 14.842
Input to awk program: gohalt 1 nbs 4 T 3-state 4-symbol #g (T.J. & S. Ligocki) : >1.4x10^2355 >3.4x10^4710 5T 1RB 2LB 2RA 1LA 2LA 1RC 0LB 2RA 1RB 3LC 1LA 1RH L 10 M 500 pref sim machv Lig34_g just simple machv Lig34_g-r with repetitions reduced machv Lig34_g-1 with tape symbol exponents machv Lig34_g-m as 2-bck-macro machine machv Lig34_g-a as 2-bck-macro machine with pure additive config-TRs iam Lig34_g-a mtype 2 0 mmtyp 3 r 1 H 1 mac 0 E 2 sympr HM 1 date Tue Jul 6 22:13:52 CEST 2010 edate Tue Jul 6 22:13:54 CEST 2010 bnspeed 1 short 7Start: Tue Jul 6 22:13:52 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;