4-state 3-symbol #b (T.J. & S. Ligocki)

Comment: This TM produces >1.1x10^713 nonzeros in >1.5x10^1426 steps.

State on
0
on
1
on
2
on 0 on 1 on 2
Print Move Goto Print Move Goto Print Move Goto
A 1RB 0LC 1RH 1 right B 0 left C 1 right H
B 2LC 1RD 0LB 2 left C 1 right D 0 left B
C 2LA 1LC 1LA 2 left A 1 left C 1 left A
D 1RB 2LD 2RA 1 right B 2 left D 2 right A
Transition table
The same TM just simple.
The same TM with repetitions reduced.
The same TM with tape symbol exponents.
The same TM as 1-bck-macro machine.
Simulation is done as 1-bck-macro machine with pure additive config-TRs.

Pushing initial machine.
Pushing macro factor 1.
Pushing BCK machine.

Steps             BasSteps              BasTpos  Tape contents
    0                    0                    0  (0)A>
    1                    1                    1  (1)B>
    2                    3                   -1  <C(1) 2
    3                    4                   -2  <A(2) 1 2
    4                    8                    0  1 (1)B> 1 2
    5                    9                    1  12 (1)D> 2
    6                   10                    2  13 (2)A>
    7                   11                    3  13 2 (1)B>
    8                   13                    1  13 2 <C(1) 2
    9                   14                    0  13 <A(1) 1 2
   10                   15                   -1  12 <C(0) 12 2
   11                   16                   -2  1 <C(1) 0 12 2
   12                   17                   -3  <C(1) 1 0 12 2
   13                   18                   -4  <A(2) 12 0 12 2
   14                   22                   -2  1 (1)B> 12 0 12 2
   15                   23                   -1  12 (1)D> 1 0 12 2
   16                   25                   -3  12 <D(2) 2 0 12 2
   17                   27                   -5  <D(2) 23 0 12 2
   18                   31                   -3  1 (1)B> 23 0 12 2
   19                   40                    0  14 (1)B> 0 12 2
   20                   42                   -2  14 <C(1) 2 12 2
   21                   46                   -6  <C(1) 14 2 12 2
   22                   47                   -7  <A(2) 15 2 12 2
   23                   51                   -5  1 (1)B> 15 2 12 2
   24                   52                   -4  12 (1)D> 14 2 12 2
   25                   54                   -6  12 <D(2) 2 13 2 12 2
   26                   56                   -8  <D(2) 23 13 2 12 2
   27                   60                   -6  1 (1)B> 23 13 2 12 2
   28                   69                   -3  14 (1)B> 13 2 12 2
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  11+V(1) (1)B> 13+V(2) [*]* [*]* [*]*
    1                    1                    1  12+V(1) (1)D> 12+V(2) [*]* [*]* [*]*
    2                    3                   -1  12+V(1) <D(2) 2 11+V(2) [*]* [*]* [*]*
    3               5+V(1)           -3+-1*V(1)  <D(2) 23+V(1) 11+V(2) [*]* [*]* [*]*
    4               9+V(1)           -1+-1*V(1)  1 (1)B> 23+V(1) 11+V(2) [*]* [*]* [*]*
    5            18+4*V(1)                    2  14+V(1) (1)B> 11+V(2) [*]* [*]* [*]*
<< Success! ==> defined new CTR 1 (PA)
   28                   69                   -3  14 (1)B> 13 2 12 2
== Executing  PA-CTR  1, V(1)=3, V(2)=0, repcount=1, factor=3/2
   33                   99                   -1  17 (1)B> 1 2 12 2
   34                  100                    0  18 (1)D> 2 12 2
   35                  101                    1  19 (2)A> 12 2
   36                  103                   -1  19 <A(1) 0 1 2
   37                  104                   -2  18 <C(0) 1 0 1 2
   38                  105                   -3  17 <C(1) 0 1 0 1 2
   39                  112                  -10  <C(1) 17 0 1 0 1 2
   40                  113                  -11  <A(2) 18 0 1 0 1 2
   41                  117                   -9  1 (1)B> 18 0 1 0 1 2
   42                  118                   -8  12 (1)D> 17 0 1 0 1 2
   43                  120                  -10  12 <D(2) 2 16 0 1 0 1 2
   44                  122                  -12  <D(2) 23 16 0 1 0 1 2
   45                  126                  -10  1 (1)B> 23 16 0 1 0 1 2
   46                  135                   -7  14 (1)B> 16 0 1 0 1 2
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  11+V(1) (1)B> 13+V(2) [*]* [*]* [*]* [*]* [*]*
    1                    1                    1  12+V(1) (1)D> 12+V(2) [*]* [*]* [*]* [*]* [*]*
    2                    3                   -1  12+V(1) <D(2) 2 11+V(2) [*]* [*]* [*]* [*]* [*]*
    3               5+V(1)           -3+-1*V(1)  <D(2) 23+V(1) 11+V(2) [*]* [*]* [*]* [*]* [*]*
    4               9+V(1)           -1+-1*V(1)  1 (1)B> 23+V(1) 11+V(2) [*]* [*]* [*]* [*]* [*]*
    5            18+4*V(1)                    2  14+V(1) (1)B> 11+V(2) [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 2 (PA)
   46                  135                   -7  14 (1)B> 16 0 1 0 1 2
== Executing  PA-CTR  2, V(1)=3, V(2)=3, repcount=2, factor=3/2
   56                  207                   -3  110 (1)B> 12 0 1 0 1 2
   57                  208                   -2  111 (1)D> 1 0 1 0 1 2
   58                  210                   -4  111 <D(2) 2 0 1 0 1 2
   59                  221                  -15  <D(2) 212 0 1 0 1 2
   60                  225                  -13  1 (1)B> 212 0 1 0 1 2
   61                  261                   -1  113 (1)B> 0 1 0 1 2
   62                  263                   -3  113 <C(1) 2 1 0 1 2
   63                  276                  -16  <C(1) 113 2 1 0 1 2
   64                  277                  -17  <A(2) 114 2 1 0 1 2
   65                  281                  -15  1 (1)B> 114 2 1 0 1 2
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  11+V(1) (1)B> 12 0 [*]* [*]* [*]* [*]*
    1                    1                    1  12+V(1) (1)D> 1 0 [*]* [*]* [*]* [*]*
    2                    3                   -1  12+V(1) <D(2) 2 0 [*]* [*]* [*]* [*]*
    3               5+V(1)           -3+-1*V(1)  <D(2) 23+V(1) 0 [*]* [*]* [*]* [*]*
    4               9+V(1)           -1+-1*V(1)  1 (1)B> 23+V(1) 0 [*]* [*]* [*]* [*]*
    5            18+4*V(1)                    2  14+V(1) (1)B> 0 [*]* [*]* [*]* [*]*
    6            20+4*V(1)                    0  14+V(1) <C(1) 2 [*]* [*]* [*]* [*]*
    7            24+5*V(1)           -4+-1*V(1)  <C(1) 14+V(1) 2 [*]* [*]* [*]* [*]*
    8            25+5*V(1)           -5+-1*V(1)  <A(2) 15+V(1) 2 [*]* [*]* [*]* [*]*
    9            29+5*V(1)           -3+-1*V(1)  1 (1)B> 15+V(1) 2 [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 3 (PPA)
   65                  281                  -15  1 (1)B> 114 2 1 0 1 2
== Executing  PA-CTR  2, V(1)=0, V(2)=11, repcount=6, factor=3/2
   95                  569                   -3  119 (1)B> 12 2 1 0 1 2
   96                  570                   -2  120 (1)D> 1 2 1 0 1 2
   97                  572                   -4  120 <D(2) 22 1 0 1 2
   98                  592                  -24  <D(2) 222 1 0 1 2
   99                  596                  -22  1 (1)B> 222 1 0 1 2
  100                  662                    0  123 (1)B> 1 0 1 2
  101                  663                    1  124 (1)D> 0 1 2
  102                  664                    2  125 (1)B> 1 2
  103                  665                    3  126 (1)D> 2
  104                  666                    4  127 (2)A>
  105                  667                    5  127 2 (1)B>
  106                  669                    3  127 2 <C(1) 2
  107                  670                    2  127 <A(1) 1 2
  108                  671                    1  126 <C(0) 12 2
  109                  672                    0  125 <C(1) 0 12 2
  110                  697                  -25  <C(1) 125 0 12 2
  111                  698                  -26  <A(2) 126 0 12 2
  112                  702                  -24  1 (1)B> 126 0 12 2
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  11+V(1) (1)B> 12 21+V(2) 1 0 1 2
    1                    1                    1  12+V(1) (1)D> 1 21+V(2) 1 0 1 2
    2                    3                   -1  12+V(1) <D(2) 22+V(2) 1 0 1 2
    3               5+V(1)           -3+-1*V(1)  <D(2) 24+V(1)+V(2) 1 0 1 2
    4               9+V(1)           -1+-1*V(1)  1 (1)B> 24+V(1)+V(2) 1 0 1 2
    5     21+4*V(1)+3*V(2)               3+V(2)  15+V(1)+V(2) (1)B> 1 0 1 2
    6     22+4*V(1)+3*V(2)               4+V(2)  16+V(1)+V(2) (1)D> 0 1 2
    7     23+4*V(1)+3*V(2)               5+V(2)  17+V(1)+V(2) (1)B> 1 2
    8     24+4*V(1)+3*V(2)               6+V(2)  18+V(1)+V(2) (1)D> 2
    9     25+4*V(1)+3*V(2)               7+V(2)  19+V(1)+V(2) (2)A>
   10     26+4*V(1)+3*V(2)               8+V(2)  19+V(1)+V(2) 2 (1)B>
   11     28+4*V(1)+3*V(2)               6+V(2)  19+V(1)+V(2) 2 <C(1) 2
   12     29+4*V(1)+3*V(2)               5+V(2)  19+V(1)+V(2) <A(1) 1 2
   13     30+4*V(1)+3*V(2)               4+V(2)  18+V(1)+V(2) <C(0) 12 2
   14     31+4*V(1)+3*V(2)               3+V(2)  17+V(1)+V(2) <C(1) 0 12 2
   15     38+5*V(1)+4*V(2)           -4+-1*V(1)  <C(1) 17+V(1)+V(2) 0 12 2
   16     39+5*V(1)+4*V(2)           -5+-1*V(1)  <A(2) 18+V(1)+V(2) 0 12 2
   17     43+5*V(1)+4*V(2)           -3+-1*V(1)  1 (1)B> 18+V(1)+V(2) 0 12 2
<< Success! ==> defined new CTR 4 (PPA)
  112                  702                  -24  1 (1)B> 126 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=23, repcount=12, factor=3/2
  172                 1710                    0  137 (1)B> 12 0 12 2
  173                 1711                    1  138 (1)D> 1 0 12 2
  174                 1713                   -1  138 <D(2) 2 0 12 2
  175                 1751                  -39  <D(2) 239 0 12 2
  176                 1755                  -37  1 (1)B> 239 0 12 2
  177                 1872                    2  140 (1)B> 0 12 2
  178                 1874                    0  140 <C(1) 2 12 2
  179                 1914                  -40  <C(1) 140 2 12 2
  180                 1915                  -41  <A(2) 141 2 12 2
  181                 1919                  -39  1 (1)B> 141 2 12 2
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  11+V(1) (1)B> 12 0 [*]* [*]*
    1                    1                    1  12+V(1) (1)D> 1 0 [*]* [*]*
    2                    3                   -1  12+V(1) <D(2) 2 0 [*]* [*]*
    3               5+V(1)           -3+-1*V(1)  <D(2) 23+V(1) 0 [*]* [*]*
    4               9+V(1)           -1+-1*V(1)  1 (1)B> 23+V(1) 0 [*]* [*]*
    5            18+4*V(1)                    2  14+V(1) (1)B> 0 [*]* [*]*
    6            20+4*V(1)                    0  14+V(1) <C(1) 2 [*]* [*]*
    7            24+5*V(1)           -4+-1*V(1)  <C(1) 14+V(1) 2 [*]* [*]*
    8            25+5*V(1)           -5+-1*V(1)  <A(2) 15+V(1) 2 [*]* [*]*
    9            29+5*V(1)           -3+-1*V(1)  1 (1)B> 15+V(1) 2 [*]* [*]*
<< Success! ==> defined new CTR 5 (PPA)
  181                 1919                  -39  1 (1)B> 141 2 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=38, repcount=20, factor=3/2
  281                 4559                    1  161 (1)B> 1 2 12 2
  282                 4560                    2  162 (1)D> 2 12 2
  283                 4561                    3  163 (2)A> 12 2
  284                 4563                    1  163 <A(1) 0 1 2
  285                 4564                    0  162 <C(0) 1 0 1 2
  286                 4565                   -1  161 <C(1) 0 1 0 1 2
  287                 4626                  -62  <C(1) 161 0 1 0 1 2
  288                 4627                  -63  <A(2) 162 0 1 0 1 2
  289                 4631                  -61  1 (1)B> 162 0 1 0 1 2
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  12+V(1) (1)B> 1 2 12+V(2) [*]*
    1                    1                    1  13+V(1) (1)D> 2 12+V(2) [*]*
    2                    2                    2  14+V(1) (2)A> 12+V(2) [*]*
    3                    4                    0  14+V(1) <A(1) 0 11+V(2) [*]*
    4                    5                   -1  13+V(1) <C(0) 1 0 11+V(2) [*]*
    5                    6                   -2  12+V(1) <C(1) 0 1 0 11+V(2) [*]*
    6               8+V(1)           -4+-1*V(1)  <C(1) 12+V(1) 0 1 0 11+V(2) [*]*
    7               9+V(1)           -5+-1*V(1)  <A(2) 13+V(1) 0 1 0 11+V(2) [*]*
    8              13+V(1)           -3+-1*V(1)  1 (1)B> 13+V(1) 0 1 0 11+V(2) [*]*
<< Success! ==> defined new CTR 6 (PPA)
  289                 4631                  -61  1 (1)B> 162 0 1 0 1 2
== Executing  PA-CTR  2, V(1)=0, V(2)=59, repcount=30, factor=3/2
  439                10391                   -1  191 (1)B> 12 0 1 0 1 2
== Executing PPA-CTR  3 (once), V(1)=90
  448                10870                  -94  1 (1)B> 195 2 1 0 1 2
== Executing  PA-CTR  2, V(1)=0, V(2)=92, repcount=47, factor=3/2
  683                24688                    0  1142 (1)B> 1 2 1 0 1 2
  684                24689                    1  1143 (1)D> 2 1 0 1 2
  685                24690                    2  1144 (2)A> 1 0 1 2
  686                24692                    0  1144 <A(1) 02 1 2
  687                24693                   -1  1143 <C(0) 1 02 1 2
  688                24694                   -2  1142 <C(1) 0 1 02 1 2
  689                24836                 -144  <C(1) 1142 0 1 02 1 2
  690                24837                 -145  <A(2) 1143 0 1 02 1 2
  691                24841                 -143  1 (1)B> 1143 0 1 02 1 2
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  12+V(1) (1)B> 1 2 1 01+V(2) [*]* [*]*
    1                    1                    1  13+V(1) (1)D> 2 1 01+V(2) [*]* [*]*
    2                    2                    2  14+V(1) (2)A> 1 01+V(2) [*]* [*]*
    3                    4                    0  14+V(1) <A(1) 02+V(2) [*]* [*]*
    4                    5                   -1  13+V(1) <C(0) 1 02+V(2) [*]* [*]*
    5                    6                   -2  12+V(1) <C(1) 0 1 02+V(2) [*]* [*]*
    6               8+V(1)           -4+-1*V(1)  <C(1) 12+V(1) 0 1 02+V(2) [*]* [*]*
    7               9+V(1)           -5+-1*V(1)  <A(2) 13+V(1) 0 1 02+V(2) [*]* [*]*
    8              13+V(1)           -3+-1*V(1)  1 (1)B> 13+V(1) 0 1 02+V(2) [*]* [*]*
<< Success! ==> defined new CTR 7 (PPA)
  691                24841                 -143  1 (1)B> 1143 0 1 02 1 2
== Executing  PA-CTR  2, V(1)=0, V(2)=140, repcount=71, factor=3/2
 1046                55939                   -1  1214 (1)B> 1 0 1 02 1 2
 1047                55940                    0  1215 (1)D> 0 1 02 1 2
 1048                55941                    1  1216 (1)B> 1 02 1 2
 1049                55942                    2  1217 (1)D> 02 1 2
 1050                55943                    3  1218 (1)B> 0 1 2
 1051                55945                    1  1218 <C(1) 2 1 2
 1052                56163                 -217  <C(1) 1218 2 1 2
 1053                56164                 -218  <A(2) 1219 2 1 2
 1054                56168                 -216  1 (1)B> 1219 2 1 2
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  11+V(1) (1)B> 1 0 1 02 [*]* [*]*
    1                    1                    1  12+V(1) (1)D> 0 1 02 [*]* [*]*
    2                    2                    2  13+V(1) (1)B> 1 02 [*]* [*]*
    3                    3                    3  14+V(1) (1)D> 02 [*]* [*]*
    4                    4                    4  15+V(1) (1)B> 0 [*]* [*]*
    5                    6                    2  15+V(1) <C(1) 2 [*]* [*]*
    6              11+V(1)           -3+-1*V(1)  <C(1) 15+V(1) 2 [*]* [*]*
    7              12+V(1)           -4+-1*V(1)  <A(2) 16+V(1) 2 [*]* [*]*
    8              16+V(1)           -2+-1*V(1)  1 (1)B> 16+V(1) 2 [*]* [*]*
<< Success! ==> defined new CTR 8 (PPA)
 1054                56168                 -216  1 (1)B> 1219 2 1 2
== Executing  PA-CTR  1, V(1)=0, V(2)=216, repcount=109, factor=3/2
 1599               128762                    2  1328 (1)B> 1 2 1 2
 1600               128763                    3  1329 (1)D> 2 1 2
 1601               128764                    4  1330 (2)A> 1 2
 1602               128766                    2  1330 <A(1) 0 2
 1603               128767                    1  1329 <C(0) 1 0 2
 1604               128768                    0  1328 <C(1) 0 1 0 2
 1605               129096                 -328  <C(1) 1328 0 1 0 2
 1606               129097                 -329  <A(2) 1329 0 1 0 2
 1607               129101                 -327  1 (1)B> 1329 0 1 0 2
 1608               129102                 -326  12 (1)D> 1328 0 1 0 2
 1609               129104                 -328  12 <D(2) 2 1327 0 1 0 2
 1610               129106                 -330  <D(2) 23 1327 0 1 0 2
 1611               129110                 -328  1 (1)B> 23 1327 0 1 0 2
 1612               129119                 -325  14 (1)B> 1327 0 1 0 2
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  11+V(1) (1)B> 13+V(2) [*]* [*]* [*]* [*]*
    1                    1                    1  12+V(1) (1)D> 12+V(2) [*]* [*]* [*]* [*]*
    2                    3                   -1  12+V(1) <D(2) 2 11+V(2) [*]* [*]* [*]* [*]*
    3               5+V(1)           -3+-1*V(1)  <D(2) 23+V(1) 11+V(2) [*]* [*]* [*]* [*]*
    4               9+V(1)           -1+-1*V(1)  1 (1)B> 23+V(1) 11+V(2) [*]* [*]* [*]* [*]*
    5            18+4*V(1)                    2  14+V(1) (1)B> 11+V(2) [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 9 (PA)
 1612               129119                 -325  14 (1)B> 1327 0 1 0 2
== Executing  PA-CTR  9, V(1)=3, V(2)=324, repcount=163, factor=3/2
 2427               292445                    1  1493 (1)B> 1 0 1 0 2
 2428               292446                    2  1494 (1)D> 0 1 0 2
 2429               292447                    3  1495 (1)B> 1 0 2
 2430               292448                    4  1496 (1)D> 0 2
 2431               292449                    5  1497 (1)B> 2
 2432               292452                    6  1498 (1)B>
 2433               292454                    4  1498 <C(1) 2
 2434               292952                 -494  <C(1) 1498 2
 2435               292953                 -495  <A(2) 1499 2
 2436               292957                 -493  1 (1)B> 1499 2
 2437               292958                 -492  12 (1)D> 1498 2
 2438               292960                 -494  12 <D(2) 2 1497 2
 2439               292962                 -496  <D(2) 23 1497 2
 2440               292966                 -494  1 (1)B> 23 1497 2
 2441               292975                 -491  14 (1)B> 1497 2
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  11+V(1) (1)B> 13+V(2) [*]*
    1                    1                    1  12+V(1) (1)D> 12+V(2) [*]*
    2                    3                   -1  12+V(1) <D(2) 2 11+V(2) [*]*
    3               5+V(1)           -3+-1*V(1)  <D(2) 23+V(1) 11+V(2) [*]*
    4               9+V(1)           -1+-1*V(1)  1 (1)B> 23+V(1) 11+V(2) [*]*
    5            18+4*V(1)                    2  14+V(1) (1)B> 11+V(2) [*]*
<< Success! ==> defined new CTR 10 (PA)
 2441               292975                 -491  14 (1)B> 1497 2
== Executing  PA-CTR 10, V(1)=3, V(2)=494, repcount=248, factor=3/2
 3681               667951                    5  1748 (1)B> 1 2
 3682               667952                    6  1749 (1)D> 2
 3683               667953                    7  1750 (2)A>
 3684               667954                    8  1750 2 (1)B>
 3685               667956                    6  1750 2 <C(1) 2
 3686               667957                    5  1750 <A(1) 1 2
 3687               667958                    4  1749 <C(0) 12 2
 3688               667959                    3  1748 <C(1) 0 12 2
 3689               668707                 -745  <C(1) 1748 0 12 2
 3690               668708                 -746  <A(2) 1749 0 12 2
 3691               668712                 -744  1 (1)B> 1749 0 12 2
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  12+V(1) (1)B> 1 2
    1                    1                    1  13+V(1) (1)D> 2
    2                    2                    2  14+V(1) (2)A>
    3                    3                    3  14+V(1) 2 (1)B>
    4                    5                    1  14+V(1) 2 <C(1) 2
    5                    6                    0  14+V(1) <A(1) 1 2
    6                    7                   -1  13+V(1) <C(0) 12 2
    7                    8                   -2  12+V(1) <C(1) 0 12 2
    8              10+V(1)           -4+-1*V(1)  <C(1) 12+V(1) 0 12 2
    9              11+V(1)           -5+-1*V(1)  <A(2) 13+V(1) 0 12 2
   10              15+V(1)           -3+-1*V(1)  1 (1)B> 13+V(1) 0 12 2
<< Success! ==> defined new CTR 11 (PPA)
 3691               668712                 -744  1 (1)B> 1749 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=746, repcount=374, factor=3/2
 5561              1512456                    4  11123 (1)B> 1 0 12 2
 5562              1512457                    5  11124 (1)D> 0 12 2
 5563              1512458                    6  11125 (1)B> 12 2
 5564              1512459                    7  11126 (1)D> 1 2
 5565              1512461                    5  11126 <D(2) 22
 5566              1513587                -1121  <D(2) 21128
 5567              1513591                -1119  1 (1)B> 21128
 5568              1516975                    9  11129 (1)B>
 5569              1516977                    7  11129 <C(1) 2
 5570              1518106                -1122  <C(1) 11129 2
 5571              1518107                -1123  <A(2) 11130 2
 5572              1518111                -1121  1 (1)B> 11130 2
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  11+V(1) (1)B> 1 0 12 21+V(2)
    1                    1                    1  12+V(1) (1)D> 0 12 21+V(2)
    2                    2                    2  13+V(1) (1)B> 12 21+V(2)
    3                    3                    3  14+V(1) (1)D> 1 21+V(2)
    4                    5                    1  14+V(1) <D(2) 22+V(2)
    5               9+V(1)           -3+-1*V(1)  <D(2) 26+V(1)+V(2)
    6              13+V(1)           -1+-1*V(1)  1 (1)B> 26+V(1)+V(2)
    7     31+4*V(1)+3*V(2)               5+V(2)  17+V(1)+V(2) (1)B>
    8     33+4*V(1)+3*V(2)               3+V(2)  17+V(1)+V(2) <C(1) 2
    9     40+5*V(1)+4*V(2)           -4+-1*V(1)  <C(1) 17+V(1)+V(2) 2
   10     41+5*V(1)+4*V(2)           -5+-1*V(1)  <A(2) 18+V(1)+V(2) 2
   11     45+5*V(1)+4*V(2)           -3+-1*V(1)  1 (1)B> 18+V(1)+V(2) 2
<< Success! ==> defined new CTR 12 (PPA)
 5572              1518111                -1121  1 (1)B> 11130 2
== Executing  PA-CTR 10, V(1)=0, V(2)=1127, repcount=564, factor=3/2
 8392              3433455                    7  11693 (1)B> 12 2
 8393              3433456                    8  11694 (1)D> 1 2
 8394              3433458                    6  11694 <D(2) 22
 8395              3435152                -1688  <D(2) 21696
 8396              3435156                -1686  1 (1)B> 21696
 8397              3440244                   10  11697 (1)B>
 8398              3440246                    8  11697 <C(1) 2
 8399              3441943                -1689  <C(1) 11697 2
 8400              3441944                -1690  <A(2) 11698 2
 8401              3441948                -1688  1 (1)B> 11698 2
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  11+V(1) (1)B> 12 21+V(2)
    1                    1                    1  12+V(1) (1)D> 1 21+V(2)
    2                    3                   -1  12+V(1) <D(2) 22+V(2)
    3               5+V(1)           -3+-1*V(1)  <D(2) 24+V(1)+V(2)
    4               9+V(1)           -1+-1*V(1)  1 (1)B> 24+V(1)+V(2)
    5     21+4*V(1)+3*V(2)               3+V(2)  15+V(1)+V(2) (1)B>
    6     23+4*V(1)+3*V(2)               1+V(2)  15+V(1)+V(2) <C(1) 2
    7     28+5*V(1)+4*V(2)           -4+-1*V(1)  <C(1) 15+V(1)+V(2) 2
    8     29+5*V(1)+4*V(2)           -5+-1*V(1)  <A(2) 16+V(1)+V(2) 2
    9     33+5*V(1)+4*V(2)           -3+-1*V(1)  1 (1)B> 16+V(1)+V(2) 2
<< Success! ==> defined new CTR 13 (PPA)
 8401              3441948                -1688  1 (1)B> 11698 2
== Executing  PA-CTR 10, V(1)=0, V(2)=1695, repcount=848, factor=3/2
12641              7766748                    8  12545 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=2544, V(2)=0
12650              7779501                -2539  1 (1)B> 12550 2
== Executing  PA-CTR 10, V(1)=0, V(2)=2547, repcount=1274, factor=3/2
19020             17533245                    9  13823 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=3822, V(2)=0
19029             17552388                -3816  1 (1)B> 13828 2
== Executing  PA-CTR 10, V(1)=0, V(2)=3825, repcount=1913, factor=3/2
28594             39532758                   10  15740 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=5739, V(2)=0
28603             39561486                -5732  1 (1)B> 15745 2
== Executing  PA-CTR 10, V(1)=0, V(2)=5742, repcount=2872, factor=3/2
42963             89086254                   12  18617 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=8615
42973             89094884                -8606  1 (1)B> 18618 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=8615, repcount=4308, factor=3/2
64513            200499764                   10  112925 (1)B> 12 0 12 2
== Executing PPA-CTR  5 (once), V(1)=12924
64522            200564413               -12917  1 (1)B> 112929 2 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=12926, repcount=6464, factor=3/2
96842            451341757                   11  119393 (1)B> 1 2 12 2
== Executing PPA-CTR  6 (once), V(1)=19391, V(2)=0
96850            451361161               -19383  1 (1)B> 119394 0 1 0 1 2
== Executing  PA-CTR  2, V(1)=0, V(2)=19391, repcount=9696, factor=3/2
145330           1015552009                    9  129089 (1)B> 12 0 1 0 1 2
== Executing PPA-CTR  3 (once), V(1)=29088
145339           1015697478               -29082  1 (1)B> 129093 2 1 0 1 2
== Executing  PA-CTR  2, V(1)=0, V(2)=29090, repcount=14546, factor=3/2
218069           2285388726                   10  143639 (1)B> 1 2 1 0 1 2
== Executing PPA-CTR  7 (once), V(1)=43637, V(2)=0
218077           2285432376               -43630  1 (1)B> 143640 0 1 02 1 2
== Executing  PA-CTR  2, V(1)=0, V(2)=43637, repcount=21819, factor=3/2
327172           5142106770                    8  165458 (1)B> 12 0 1 02 1 2
== Executing PPA-CTR  3 (once), V(1)=65457
327181           5142434084               -65452  1 (1)B> 165462 2 1 02 1 2
== Executing  PA-CTR  2, V(1)=0, V(2)=65459, repcount=32730, factor=3/2
490831          11570344244                    8  198191 (1)B> 12 2 1 02 1 2
490832          11570344245                    9  198192 (1)D> 1 2 1 02 1 2
490833          11570344247                    7  198192 <D(2) 22 1 02 1 2
490834          11570442439               -98185  <D(2) 298194 1 02 1 2
490835          11570442443               -98183  1 (1)B> 298194 1 02 1 2
490836          11570737025                   11  198195 (1)B> 1 02 1 2
490837          11570737026                   12  198196 (1)D> 02 1 2
490838          11570737027                   13  198197 (1)B> 0 1 2
490839          11570737029                   11  198197 <C(1) 2 1 2
490840          11570835226               -98186  <C(1) 198197 2 1 2
490841          11570835227               -98187  <A(2) 198198 2 1 2
490842          11570835231               -98185  1 (1)B> 198198 2 1 2
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  11+V(1) (1)B> 12 21+V(2) 1 02 [*]* [*]*
    1                    1                    1  12+V(1) (1)D> 1 21+V(2) 1 02 [*]* [*]*
    2                    3                   -1  12+V(1) <D(2) 22+V(2) 1 02 [*]* [*]*
    3               5+V(1)           -3+-1*V(1)  <D(2) 24+V(1)+V(2) 1 02 [*]* [*]*
    4               9+V(1)           -1+-1*V(1)  1 (1)B> 24+V(1)+V(2) 1 02 [*]* [*]*
    5     21+4*V(1)+3*V(2)               3+V(2)  15+V(1)+V(2) (1)B> 1 02 [*]* [*]*
    6     22+4*V(1)+3*V(2)               4+V(2)  16+V(1)+V(2) (1)D> 02 [*]* [*]*
    7     23+4*V(1)+3*V(2)               5+V(2)  17+V(1)+V(2) (1)B> 0 [*]* [*]*
    8     25+4*V(1)+3*V(2)               3+V(2)  17+V(1)+V(2) <C(1) 2 [*]* [*]*
    9     32+5*V(1)+4*V(2)           -4+-1*V(1)  <C(1) 17+V(1)+V(2) 2 [*]* [*]*
   10     33+5*V(1)+4*V(2)           -5+-1*V(1)  <A(2) 18+V(1)+V(2) 2 [*]* [*]*
   11     37+5*V(1)+4*V(2)           -3+-1*V(1)  1 (1)B> 18+V(1)+V(2) 2 [*]* [*]*
<< Success! ==> defined new CTR 14 (PPA)
490842          11570835231               -98185  1 (1)B> 198198 2 1 2
== Executing  PA-CTR  1, V(1)=0, V(2)=98195, repcount=49098, factor=3/2
736332          26035106031                   11  1147295 (1)B> 12 2 1 2
736333          26035106032                   12  1147296 (1)D> 1 2 1 2
736334          26035106034                   10  1147296 <D(2) 22 1 2
736335          26035253330              -147286  <D(2) 2147298 1 2
736336          26035253334              -147284  1 (1)B> 2147298 1 2
736337          26035695228                   14  1147299 (1)B> 1 2
736338          26035695229                   15  1147300 (1)D> 2
736339          26035695230                   16  1147301 (2)A>
736340          26035695231                   17  1147301 2 (1)B>
736341          26035695233                   15  1147301 2 <C(1) 2
736342          26035695234                   14  1147301 <A(1) 1 2
736343          26035695235                   13  1147300 <C(0) 12 2
736344          26035695236                   12  1147299 <C(1) 0 12 2
736345          26035842535              -147287  <C(1) 1147299 0 12 2
736346          26035842536              -147288  <A(2) 1147300 0 12 2
736347          26035842540              -147286  1 (1)B> 1147300 0 12 2
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  11+V(1) (1)B> 12 21+V(2) 1 2
    1                    1                    1  12+V(1) (1)D> 1 21+V(2) 1 2
    2                    3                   -1  12+V(1) <D(2) 22+V(2) 1 2
    3               5+V(1)           -3+-1*V(1)  <D(2) 24+V(1)+V(2) 1 2
    4               9+V(1)           -1+-1*V(1)  1 (1)B> 24+V(1)+V(2) 1 2
    5     21+4*V(1)+3*V(2)               3+V(2)  15+V(1)+V(2) (1)B> 1 2
    6     22+4*V(1)+3*V(2)               4+V(2)  16+V(1)+V(2) (1)D> 2
    7     23+4*V(1)+3*V(2)               5+V(2)  17+V(1)+V(2) (2)A>
    8     24+4*V(1)+3*V(2)               6+V(2)  17+V(1)+V(2) 2 (1)B>
    9     26+4*V(1)+3*V(2)               4+V(2)  17+V(1)+V(2) 2 <C(1) 2
   10     27+4*V(1)+3*V(2)               3+V(2)  17+V(1)+V(2) <A(1) 1 2
   11     28+4*V(1)+3*V(2)               2+V(2)  16+V(1)+V(2) <C(0) 12 2
   12     29+4*V(1)+3*V(2)               1+V(2)  15+V(1)+V(2) <C(1) 0 12 2
   13     34+5*V(1)+4*V(2)           -4+-1*V(1)  <C(1) 15+V(1)+V(2) 0 12 2
   14     35+5*V(1)+4*V(2)           -5+-1*V(1)  <A(2) 16+V(1)+V(2) 0 12 2
   15     39+5*V(1)+4*V(2)           -3+-1*V(1)  1 (1)B> 16+V(1)+V(2) 0 12 2
<< Success! ==> defined new CTR 15 (PPA)
736347          26035842540              -147286  1 (1)B> 1147300 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=147297, repcount=73649, factor=3/2
1104592          58581777534                   12  1220948 (1)B> 12 0 12 2
== Executing PPA-CTR  5 (once), V(1)=220947
1104601          58582882298              -220938  1 (1)B> 1220952 2 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=220949, repcount=110475, factor=3/2
1656976         131812561748                   12  1331426 (1)B> 12 2 12 2
1656977         131812561749                   13  1331427 (1)D> 1 2 12 2
1656978         131812561751                   11  1331427 <D(2) 22 12 2
1656979         131812893178              -331416  <D(2) 2331429 12 2
1656980         131812893182              -331414  1 (1)B> 2331429 12 2
1656981         131813887469                   15  1331430 (1)B> 12 2
1656982         131813887470                   16  1331431 (1)D> 1 2
1656983         131813887472                   14  1331431 <D(2) 22
1656984         131814218903              -331417  <D(2) 2331433
1656985         131814218907              -331415  1 (1)B> 2331433
1656986         131815213206                   18  1331434 (1)B>
1656987         131815213208                   16  1331434 <C(1) 2
1656988         131815544642              -331418  <C(1) 1331434 2
1656989         131815544643              -331419  <A(2) 1331435 2
1656990         131815544647              -331417  1 (1)B> 1331435 2
>> Try to prove a PPA-CTR with 3 Vars...
    0                    0                    0  11+V(1) (1)B> 12 21+V(3) 12 21+V(2)
    1                    1                    1  12+V(1) (1)D> 1 21+V(3) 12 21+V(2)
    2                    3                   -1  12+V(1) <D(2) 22+V(3) 12 21+V(2)
    3               5+V(1)           -3+-1*V(1)  <D(2) 24+V(1)+V(3) 12 21+V(2)
    4               9+V(1)           -1+-1*V(1)  1 (1)B> 24+V(1)+V(3) 12 21+V(2)
    5     21+4*V(1)+3*V(3)               3+V(3)  15+V(1)+V(3) (1)B> 12 21+V(2)
    6     22+4*V(1)+3*V(3)               4+V(3)  16+V(1)+V(3) (1)D> 1 21+V(2)
    7     24+4*V(1)+3*V(3)               2+V(3)  16+V(1)+V(3) <D(2) 22+V(2)
    8     30+5*V(1)+4*V(3)           -4+-1*V(1)  <D(2) 28+V(1)+V(2)+V(3)
    9     34+5*V(1)+4*V(3)           -2+-1*V(1)  1 (1)B> 28+V(1)+V(2)+V(3)
   10 58+8*V(1)+3*V(2)+7*V(3)          6+V(2)+V(3)  19+V(1)+V(2)+V(3) (1)B>
   11 60+8*V(1)+3*V(2)+7*V(3)          4+V(2)+V(3)  19+V(1)+V(2)+V(3) <C(1) 2
   12 69+9*V(1)+4*V(2)+8*V(3)           -5+-1*V(1)  <C(1) 19+V(1)+V(2)+V(3) 2
   13 70+9*V(1)+4*V(2)+8*V(3)           -6+-1*V(1)  <A(2) 110+V(1)+V(2)+V(3) 2
   14 74+9*V(1)+4*V(2)+8*V(3)           -4+-1*V(1)  1 (1)B> 110+V(1)+V(2)+V(3) 2
<< Success! ==> defined new CTR 16 (PPA)
1656990         131815544647              -331417  1 (1)B> 1331435 2
== Executing  PA-CTR 10, V(1)=0, V(2)=331432, repcount=165717, factor=3/2
2485575         296590277785                   17  1497152 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=497150
2485585         296590774950              -497136  1 (1)B> 1497153 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=497150, repcount=248576, factor=3/2
3728465         667333924518                   16  1745729 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=745728, V(2)=0
3728476         667337653203              -745715  1 (1)B> 1745736 2
== Executing  PA-CTR 10, V(1)=0, V(2)=745733, repcount=372867, factor=3/2
5592811        1501520925741                   19  11118602 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=1118601, V(2)=0
5592820        1501526518779             -1118585  1 (1)B> 11118607 2
== Executing  PA-CTR 10, V(1)=0, V(2)=1118604, repcount=559303, factor=3/2
8389335        3378452305269                   21  11677910 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=1677908
8389345        3378453983192             -1677890  1 (1)B> 11677911 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=1677908, repcount=838955, factor=3/2
12584120        7601537002802                   20  12516866 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=2516865, V(2)=0
12584131        7601549587172             -2516848  1 (1)B> 12516873 2
== Executing  PA-CTR 10, V(1)=0, V(2)=2516870, repcount=1258436, factor=3/2
18876311       17103531684980                   24  13775309 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=3775307
18876321       17103535460302             -3775286  1 (1)B> 13775310 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=3775307, repcount=1887654, factor=3/2
28314591       38482983854446                   22  15662963 (1)B> 12 0 12 2
== Executing PPA-CTR  5 (once), V(1)=5662962
28314600       38483012169285             -5662943  1 (1)B> 15662967 2 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=5662964, repcount=2831483, factor=3/2
42472015       86586822022815                   23  18494450 (1)B> 1 2 12 2
== Executing PPA-CTR  6 (once), V(1)=8494448, V(2)=0
42472023       86586830517276             -8494428  1 (1)B> 18494451 0 1 0 1 2
== Executing  PA-CTR  2, V(1)=0, V(2)=8494448, repcount=4247225, factor=3/2
63708148      194820402687726                   22  112741676 (1)B> 1 0 1 0 1 2
63708149      194820402687727                   23  112741677 (1)D> 0 1 0 1 2
63708150      194820402687728                   24  112741678 (1)B> 1 0 1 2
63708151      194820402687729                   25  112741679 (1)D> 0 1 2
63708152      194820402687730                   26  112741680 (1)B> 1 2
63708153      194820402687731                   27  112741681 (1)D> 2
63708154      194820402687732                   28  112741682 (2)A>
63708155      194820402687733                   29  112741682 2 (1)B>
63708156      194820402687735                   27  112741682 2 <C(1) 2
63708157      194820402687736                   26  112741682 <A(1) 1 2
63708158      194820402687737                   25  112741681 <C(0) 12 2
63708159      194820402687738                   24  112741680 <C(1) 0 12 2
63708160      194820415429418            -12741656  <C(1) 112741680 0 12 2
63708161      194820415429419            -12741657  <A(2) 112741681 0 12 2
63708162      194820415429423            -12741655  1 (1)B> 112741681 0 12 2
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  11+V(1) (1)B> 1 0 1 0 1 2
    1                    1                    1  12+V(1) (1)D> 0 1 0 1 2
    2                    2                    2  13+V(1) (1)B> 1 0 1 2
    3                    3                    3  14+V(1) (1)D> 0 1 2
    4                    4                    4  15+V(1) (1)B> 1 2
    5                    5                    5  16+V(1) (1)D> 2
    6                    6                    6  17+V(1) (2)A>
    7                    7                    7  17+V(1) 2 (1)B>
    8                    9                    5  17+V(1) 2 <C(1) 2
    9                   10                    4  17+V(1) <A(1) 1 2
   10                   11                    3  16+V(1) <C(0) 12 2
   11                   12                    2  15+V(1) <C(1) 0 12 2
   12              17+V(1)           -3+-1*V(1)  <C(1) 15+V(1) 0 12 2
   13              18+V(1)           -4+-1*V(1)  <A(2) 16+V(1) 0 12 2
   14              22+V(1)           -2+-1*V(1)  1 (1)B> 16+V(1) 0 12 2
<< Success! ==> defined new CTR 17 (PPA)
63708162      194820415429423            -12741655  1 (1)B> 112741681 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=12741678, repcount=6370840, factor=3/2
95562362      438346105713103                   25  119112521 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=19112520, V(2)=0
95562373      438346201275748            -19112498  1 (1)B> 119112528 2
== Executing  PA-CTR 10, V(1)=0, V(2)=19112525, repcount=9556263, factor=3/2
143343688      986279291101918                   28  128668790 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=28668789, V(2)=0
143343697      986279434445896            -28668764  1 (1)B> 128668795 2
== Executing  PA-CTR 10, V(1)=0, V(2)=28668792, repcount=14334397, factor=3/2
215015682     2219129230580314                   30  143003192 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=43003190
215015692     2219129273583519            -43003163  1 (1)B> 143003193 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=43003190, repcount=21501596, factor=3/2
322523672     4993041314885967                   29  164504789 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=64504788, V(2)=0
322523683     4993041637409952            -64504762  1 (1)B> 164504796 2
== Executing  PA-CTR 10, V(1)=0, V(2)=64504793, repcount=32252397, factor=3/2
483785668    11234344697912370                   32  196757192 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=96757191, V(2)=0
483785677    11234345181698358            -96757162  1 (1)B> 196757197 2
== Executing  PA-CTR 10, V(1)=0, V(2)=96757194, repcount=48378598, factor=3/2
725678667    25277278228915158                   34  1145135795 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=145135793
725678677    25277278374050966           -145135762  1 (1)B> 1145135796 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=145135793, repcount=72567897, factor=3/2
1088518162    56873877294881384                   32  1217703692 (1)B> 12 0 12 2
== Executing PPA-CTR  5 (once), V(1)=217703691
1088518171    56873878383399868           -217703662  1 (1)B> 1217703696 2 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=217703693, repcount=108851847, factor=3/2
1632777406    1279662[4]1490486                   32  1326555542 (1)B> 12 2 12 2
== Executing PPA-CTR 16 (once), V(1)=326555541, V(2)=0, V(3)=0
1632777420    1279662[4]0490429           -326555513  1 (1)B> 1326555551 2
== Executing  PA-CTR 10, V(1)=0, V(2)=326555548, repcount=163277775, factor=3/2
2449166295    2879240[4]3527479                   37  1489833326 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=489833324
2449166305    2879240[4]3360818           -489833290  1 (1)B> 1489833327 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=489833324, repcount=244916663, factor=3/2
3673749620    6478290[4]2694188                   36  1734749990 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=734749989, V(2)=0
3673749631    6478290[4]6444178           -734749956  1 (1)B> 1734749997 2
== Executing  PA-CTR 10, V(1)=0, V(2)=734749994, repcount=367374998, factor=3/2
5510624621    1457615[5]7944178                   40  11102124995 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=1102124993
5510624631    1457615[5]0069186          -1102124956  1 (1)B> 11102124996 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=1102124993, repcount=551062497, factor=3/2
8265937116    3279634[5]2069204                   38  11653187492 (1)B> 12 0 12 2
== Executing PPA-CTR  5 (once), V(1)=1653187491
8265937125    3279634[5]8006688          -1653187456  1 (1)B> 11653187496 2 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=1653187493, repcount=826593747, factor=3/2
12398905860    7379178[5]4131706                   38  12479781242 (1)B> 12 2 12 2
== Executing PPA-CTR 16 (once), V(1)=2479781241, V(2)=0, V(3)=0
12398905874    7379178[5]2162949          -2479781207  1 (1)B> 12479781251 2
== Executing  PA-CTR 10, V(1)=0, V(2)=2479781248, repcount=1239890625, factor=3/2
18598358999    1660315[6]8194199                   43  13719671876 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=3719671874
18598359009    1660315[6]7866088          -3719671834  1 (1)B> 13719671877 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=3719671874, repcount=1859835938, factor=3/2
27897538699    3735708[6]3936408                   42  15579507815 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=5579507814, V(2)=0
27897538710    3735708[6]1475523          -5579507775  1 (1)B> 15579507822 2
== Executing  PA-CTR 10, V(1)=0, V(2)=5579507819, repcount=2789753910, factor=3/2
41846308260    8405345[6]0251043                   45  18369261731 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=8369261730, V(2)=0
41846308269    8405345[6]6559726          -8369261688  1 (1)B> 18369261736 2
== Executing  PA-CTR 10, V(1)=0, V(2)=8369261733, repcount=4184630867, factor=3/2
62769462604    1891202[7]7160264                   46  112553892602 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=12553892601, V(2)=0
62769462613    1891202[7]6623302         -12553892558  1 (1)B> 112553892607 2
== Executing  PA-CTR 10, V(1)=0, V(2)=12553892604, repcount=6276946303, factor=3/2
94154194128    4255205[7]2185792                   48  118830838910 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=18830838908
94154194138    4255205[7]3024715         -18830838863  1 (1)B> 118830838911 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=18830838908, repcount=9415419455, factor=3/2
141231291413    9574213[7]3040325                   47  128246258366 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=28246258365, V(2)=0
141231291424    9574213[7]4332195         -28246258321  1 (1)B> 128246258373 2
== Executing  PA-CTR 10, V(1)=0, V(2)=28246258370, repcount=14123129186, factor=3/2
211846937354    2154198[8]2018003                   51  142369387559 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=42369387557
211846937364    2154198[8]1405575         -42369387509  1 (1)B> 142369387560 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=42369387557, repcount=21184693779, factor=3/2
317770406259    4846945[8]5535969                   49  163554081338 (1)B> 12 0 12 2
== Executing PPA-CTR  5 (once), V(1)=63554081337
317770406268    4846945[8]5942683         -63554081291  1 (1)B> 163554081342 2 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=63554081339, repcount=31777040670, factor=3/2
476655609618    1090562[9]4724123                   49  195331122011 (1)B> 12 2 12 2
== Executing PPA-CTR 16 (once), V(1)=95331122010, V(2)=0, V(3)=0
476655609632    1090562[9]4822287         -95331121965  1 (1)B> 195331122020 2
== Executing  PA-CTR 10, V(1)=0, V(2)=95331122017, repcount=47665561009, factor=3/2
714983414677    2453766[9]8142881                   53  1142996683028 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=142996683027, V(2)=0
714983414686    2453766[9]1558049        -142996682977  1 (1)B> 1142996683033 2
== Executing  PA-CTR 10, V(1)=0, V(2)=142996683030, repcount=71498341516, factor=3/2
1072475122266    5520973[9]6725777                   55  1214495024549 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=214495024547
1072475122276    5520973[9]1750339        -214495024495  1 (1)B> 1214495024550 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=214495024547, repcount=107247512274, factor=3/2
1608712683646   1242219[10]5804083                   53  1321742536823 (1)B> 12 0 12 2
== Executing PPA-CTR  5 (once), V(1)=321742536822
1608712683655   1242219[10]8488222        -321742536772  1 (1)B> 1321742536827 2 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=321742536824, repcount=160871268413, factor=3/2
2413069025720   2794993[10]2940592                   54  1482613805240 (1)B> 1 2 12 2
== Executing PPA-CTR  6 (once), V(1)=482613805238, V(2)=0
2413069025728   2794993[10]6745843        -482613805187  1 (1)B> 1482613805241 0 1 0 1 2
== Executing  PA-CTR  2, V(1)=0, V(2)=482613805238, repcount=241306902620, factor=3/2
3619603538828   6288734[10]6763683                   53  1723920707861 (1)B> 1 0 1 0 1 2
== Executing PPA-CTR 17 (once), V(1)=723920707860
3619603538842   6288734[10]7471565        -723920707809  1 (1)B> 1723920707866 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=723920707863, repcount=361960353932, factor=3/2
5429405308502   1414965[11]8882493                   55  11085881061797 (1)B> 12 0 12 2
== Executing PPA-CTR  5 (once), V(1)=1085881061796
5429405308511   1414965[11]4191502       -1085881061744  1 (1)B> 11085881061801 2 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=1085881061798, repcount=542940530900, factor=3/2
8144107963011   3183671[11]9422302                   56  11628821592701 (1)B> 1 2 12 2
== Executing PPA-CTR  6 (once), V(1)=1628821592699, V(2)=0
8144107963019   3183671[11]1015014       -1628821592646  1 (1)B> 11628821592702 0 1 0 1 2
== Executing  PA-CTR  2, V(1)=0, V(2)=1628821592699, repcount=814410796350, factor=3/2
12216161944769   7163261[11]0506214                   54  12443232389051 (1)B> 12 0 1 0 1 2
== Executing PPA-CTR  3 (once), V(1)=2443232389050
12216161944778   7163261[11]2451493       -2443232388999  1 (1)B> 12443232389055 2 1 0 1 2
== Executing  PA-CTR  2, V(1)=0, V(2)=2443232389052, repcount=1221616194527, factor=3/2
18324242917413   1611733[12]5308191                   55  13664848583582 (1)B> 1 2 1 0 1 2
== Executing PPA-CTR  7 (once), V(1)=3664848583580, V(2)=0
18324242917421   1611733[12]3891784       -3664848583528  1 (1)B> 13664848583583 0 1 02 1 2
== Executing  PA-CTR  2, V(1)=0, V(2)=3664848583580, repcount=1832424291791, factor=3/2
27486364376376   3626401[12]5319362                   54  15497272875374 (1)B> 1 0 1 02 1 2
== Executing PPA-CTR  8 (once), V(1)=5497272875373
27486364376384   3626401[12]8194751       -5497272875321  1 (1)B> 15497272875379 2 1 2
== Executing  PA-CTR  1, V(1)=0, V(2)=5497272875376, repcount=2748636437689, factor=3/2
41229546564829   8159402[12]3411345                   57  18245909313068 (1)B> 1 2 1 2
41229546564830   8159402[12]3411346                   58  18245909313069 (1)D> 2 1 2
41229546564831   8159402[12]3411347                   59  18245909313070 (2)A> 1 2
41229546564832   8159402[12]3411349                   57  18245909313070 <A(1) 0 2
41229546564833   8159402[12]3411350                   56  18245909313069 <C(0) 1 0 2
41229546564834   8159402[12]3411351                   55  18245909313068 <C(1) 0 1 0 2
41229546564835   8159402[12]2724419       -8245909313013  <C(1) 18245909313068 0 1 0 2
41229546564836   8159402[12]2724420       -8245909313014  <A(2) 18245909313069 0 1 0 2
41229546564837   8159402[12]2724424       -8245909313012  1 (1)B> 18245909313069 0 1 0 2
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  12+V(1) (1)B> 1 2 1 [*]*
    1                    1                    1  13+V(1) (1)D> 2 1 [*]*
    2                    2                    2  14+V(1) (2)A> 1 [*]*
    3                    4                    0  14+V(1) <A(1) 0 [*]*
    4                    5                   -1  13+V(1) <C(0) 1 0 [*]*
    5                    6                   -2  12+V(1) <C(1) 0 1 0 [*]*
    6               8+V(1)           -4+-1*V(1)  <C(1) 12+V(1) 0 1 0 [*]*
    7               9+V(1)           -5+-1*V(1)  <A(2) 13+V(1) 0 1 0 [*]*
    8              13+V(1)           -3+-1*V(1)  1 (1)B> 13+V(1) 0 1 0 [*]*
<< Success! ==> defined new CTR 18 (PPA)
41229546564837   8159402[12]2724424       -8245909313012  1 (1)B> 18245909313069 0 1 0 2
== Executing  PA-CTR  9, V(1)=0, V(2)=8245909313066, repcount=4122954656534, factor=3/2
61844319847507   1835865[13]1961768                   56  112368863969603 (1)B> 1 0 1 0 2
61844319847508   1835865[13]1961769                   57  112368863969604 (1)D> 0 1 0 2
61844319847509   1835865[13]1961770                   58  112368863969605 (1)B> 1 0 2
61844319847510   1835865[13]1961771                   59  112368863969606 (1)D> 0 2
61844319847511   1835865[13]1961772                   60  112368863969607 (1)B> 2
61844319847512   1835865[13]1961775                   61  112368863969608 (1)B>
61844319847513   1835865[13]1961777                   59  112368863969608 <C(1) 2
61844319847514   1835865[13]5931385      -12368863969549  <C(1) 112368863969608 2
61844319847515   1835865[13]5931386      -12368863969550  <A(2) 112368863969609 2
61844319847516   1835865[13]5931390      -12368863969548  1 (1)B> 112368863969609 2
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  11+V(1) (1)B> 1 0 1 0 21+V(2)
    1                    1                    1  12+V(1) (1)D> 0 1 0 21+V(2)
    2                    2                    2  13+V(1) (1)B> 1 0 21+V(2)
    3                    3                    3  14+V(1) (1)D> 0 21+V(2)
    4                    4                    4  15+V(1) (1)B> 21+V(2)
    5             7+3*V(2)               5+V(2)  16+V(1)+V(2) (1)B>
    6             9+3*V(2)               3+V(2)  16+V(1)+V(2) <C(1) 2
    7       15+V(1)+4*V(2)           -3+-1*V(1)  <C(1) 16+V(1)+V(2) 2
    8       16+V(1)+4*V(2)           -4+-1*V(1)  <A(2) 17+V(1)+V(2) 2
    9       20+V(1)+4*V(2)           -2+-1*V(1)  1 (1)B> 17+V(1)+V(2) 2
<< Success! ==> defined new CTR 19 (PPA)
61844319847516   1835865[13]5931390      -12368863969548  1 (1)B> 112368863969609 2
== Executing  PA-CTR 10, V(1)=0, V(2)=12368863969606, repcount=6184431984804, factor=3/2
92766479771536   4130697[13]1259534                   60  118553295954413 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=18553295954411
92766479771546   4130697[13]7213960      -18553295954354  1 (1)B> 118553295954414 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=18553295954411, repcount=9276647977206, factor=3/2
139149719657576   9294069[13]6339048                   58  127829943931619 (1)B> 12 0 12 2
== Executing PPA-CTR  5 (once), V(1)=27829943931618
139149719657585   9294069[13]5997167      -27829943931563  1 (1)B> 127829943931623 2 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=27829943931620, repcount=13914971965811, factor=3/2
208724579486640   2091165[14]6913225                   59  141744915897434 (1)B> 1 2 12 2
== Executing PPA-CTR  6 (once), V(1)=41744915897432, V(2)=0
208724579486648   2091165[14]2810670      -41744915897376  1 (1)B> 141744915897435 0 1 0 1 2
== Executing  PA-CTR  2, V(1)=0, V(2)=41744915897432, repcount=20872457948717, factor=3/2
313086869230233   4705122[14]9871808                   58  162617373846152 (1)B> 1 0 1 0 1 2
== Executing PPA-CTR 17 (once), V(1)=62617373846151
313086869230247   4705122[14]3717981      -62617373846095  1 (1)B> 162617373846157 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=62617373846154, repcount=31308686923078, factor=3/2
469630303845637   1058652[15]0759421                   61  193926060769235 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=93926060769234, V(2)=0
469630303845648   1058652[15]4605636      -93926060769176  1 (1)B> 193926060769242 2
== Executing  PA-CTR 10, V(1)=0, V(2)=93926060769239, repcount=46963030384620, factor=3/2
704445455768748   2381968[15]4487476                   64  1140889091153861 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=140889091153860, V(2)=0
704445455768757   2381968[15]0256809     -140889091153799  1 (1)B> 1140889091153866 2
== Executing  PA-CTR 10, V(1)=0, V(2)=140889091153863, repcount=70444545576932, factor=3/2
1056668183653417   5359428[15]0375737                   65  1211333636730797 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=211333636730796, V(2)=0
1056668183653426   5359428[15]4029750     -211333636730734  1 (1)B> 1211333636730802 2
== Executing  PA-CTR 10, V(1)=0, V(2)=211333636730799, repcount=105666818365400, factor=3/2
1585002275480426   1205871[16]7374550                   66  1317000455096201 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=317000455096200, V(2)=0
1585002275480435   1205871[16]2855583     -317000455096137  1 (1)B> 1317000455096206 2
== Executing  PA-CTR 10, V(1)=0, V(2)=317000455096203, repcount=158500227548102, factor=3/2
2377503413220945   2713210[16]6247231                   67  1475500682644307 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=475500682644306, V(2)=0
2377503413220954   2713210[16]9468794     -475500682644242  1 (1)B> 1475500682644312 2
== Executing  PA-CTR 10, V(1)=0, V(2)=475500682644309, repcount=237750341322155, factor=3/2
3566255119831729   6104724[16]8398804                   68  1713251023966466 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=713251023966465, V(2)=0
3566255119831738   6104724[16]8231162     -713251023966400  1 (1)B> 1713251023966471 2
== Executing  PA-CTR 10, V(1)=0, V(2)=713251023966468, repcount=356625511983235, factor=3/2
5349382679747913   1373562[17]8421332                   70  11069876535949706 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=1069876535949704
5349382679747923   1373562[17]4371051    -1069876535949637  1 (1)B> 11069876535949707 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=1069876535949704, repcount=534938267974853, factor=3/2
8024074019622188   3090516[17]2298941                   69  11604814803924560 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=1604814803924559, V(2)=0
8024074019622199   3090516[17]1921781    -1604814803924493  1 (1)B> 11604814803924567 2
== Executing  PA-CTR 10, V(1)=0, V(2)=1604814803924564, repcount=802407401962283, factor=3/2
12036111029433614   6953662[17]2901711                   73  12407222205886850 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=2407222205886848
12036111029433624   6953662[17]8788574    -2407222205886778  1 (1)B> 12407222205886851 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=2407222205886848, repcount=1203611102943425, factor=3/2
18054166544150749   1564574[18]8493424                   72  13610833308830276 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=3610833308830275, V(2)=0
18054166544150760   1564574[18]2644844    -3610833308830206  1 (1)B> 13610833308830283 2
== Executing  PA-CTR 10, V(1)=0, V(2)=3610833308830280, repcount=1805416654415141, factor=3/2
27081249816226465   3520291[18]5925822                   76  15416249963245424 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=5416249963245422
27081249816226475   3520291[18]9171259    -5416249963245349  1 (1)B> 15416249963245425 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=5416249963245422, repcount=2708124981622712, factor=3/2
40621874724340035   7920656[18]4053467                   75  18124374944868137 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=8124374944868136, V(2)=0
40621874724340046   7920656[18]8394192    -8124374944868064  1 (1)B> 18124374944868144 2
== Executing  PA-CTR 10, V(1)=0, V(2)=8124374944868141, repcount=4062187472434071, factor=3/2
60932812086510401   1782147[19]7401290                   78  112186562417302214 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=12186562417302213, V(2)=0
60932812086510410   1782147[19]3912388    -121865[4]7302138  1 (1)B> 112186562417302219 2
== Executing  PA-CTR 10, V(1)=0, V(2)=12186562417302216, repcount=6093281208651109, factor=3/2
91399218129765955   4009832[19]9304982                   80  118279843625953328 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=18279843625953326
91399218129765965   4009832[19]5258323    -182798[4]5953249  1 (1)B> 118279843625953329 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=18279843625953326, repcount=9139921812976664, factor=3/2
1370988[4]4649285   9022122[19]2391667                   79  127419765438929993 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=27419765438929992, V(2)=0
1370988[4]4649296   9022122[19]7041672    -274197[4]8929916  1 (1)B> 127419765438930000 2
== Executing  PA-CTR 10, V(1)=0, V(2)=27419765438929997, repcount=13709882719464999, factor=3/2
2056482[4]1974291   2029977[20]7041666                   82  141129648158394998 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=41129648158394997, V(2)=0
2056482[4]1974300   2029977[20]9016684    -411296[4]8394918  1 (1)B> 141129648158395003 2
== Executing  PA-CTR 10, V(1)=0, V(2)=41129648158395000, repcount=20564824079197501, factor=3/2
3084723[4]7961805   4567449[20]7256702                   84  161694472237592504 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=61694472237592502
3084723[4]7961815   4567449[20]4849219    -616944[4]7592421  1 (1)B> 161694472237592505 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=61694472237592502, repcount=30847236118796252, factor=3/2
4627085[4]1943075   1027676[21]5889267                   83  192541708356388757 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=92541708356388756, V(2)=0
4627085[4]1943086   1027676[21]7833092    -925417[4]6388676  1 (1)B> 192541708356388764 2
== Executing  PA-CTR 10, V(1)=0, V(2)=92541708356388761, repcount=46270854178194381, factor=3/2
6940628[4]2914991   2312271[21]6004630                   86  11388125[4]4583144 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=1388125[4]4583143, V(2)=0
6940628[4]2915000   2312271[21]8920378    -138812[5]4583060  1 (1)B> 11388125[4]4583149 2
== Executing  PA-CTR 10, V(1)=0, V(2)=1388125[4]4583146, repcount=69406281267291574, factor=3/2
1041094[5]9372870   5202610[21]4804122                   88  12082188[4]1874723 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=2082188[4]1874721
1041094[5]9372880   5202610[21]6678858    -208218[5]1874636  1 (1)B> 12082188[4]1874724 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=2082188[4]1874721, repcount=1041094[4]0937361, factor=3/2
1561641[5]4059685   1170587[22]1793116                   86  13123282[4]2812084 (1)B> 12 0 12 2
== Executing PPA-CTR  5 (once), V(1)=3123282[4]2812083
1561641[5]4059694   1170587[22]5853560    -312328[5]2812000  1 (1)B> 13123282[4]2812088 2 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=3123282[4]2812085, repcount=1561641[4]1406043, factor=3/2
2342461[5]1089909   2633821[22]4233170                   86  14684923[4]4218130 (1)B> 12 2 12 2
== Executing PPA-CTR 16 (once), V(1)=4684923[4]4218129, V(2)=0, V(3)=0
2342461[5]1089923   2633821[22]2196405    -468492[5]4218047  1 (1)B> 14684923[4]4218139 2
== Executing  PA-CTR 10, V(1)=0, V(2)=4684923[4]4218136, repcount=2342461[4]7109069, factor=3/2
3513692[5]6635268   5926098[22]9785799                   91  17027385[4]1327208 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=7027385[4]1327206
3513692[5]6635278   5926098[22]1113020    -702738[5]1327118  1 (1)B> 17027385[4]1327209 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=7027385[4]1327206, repcount=3513692[4]5663604, factor=3/2
5270539[5]4953298   1333372[23]0689164                   90  11054107[5]6990813 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=1054107[5]6990812, V(2)=0
5270539[5]4953309   1333372[23]5643269    -105410[6]6990725  1 (1)B> 11054107[5]6990820 2
== Executing  PA-CTR 10, V(1)=0, V(2)=1054107[5]6990817, repcount=5270539[4]3495409, factor=3/2
7905809[5]2430354   3000087[23]2051863                   93  11581161[5]0486228 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=1581161[5]0486227, V(2)=0
7905809[5]2430363   3000087[23]4483031    -158116[6]0486137  1 (1)B> 11581161[5]0486233 2
== Executing  PA-CTR 10, V(1)=0, V(2)=1581161[5]0486230, repcount=7905809[4]0243116, factor=3/2
1185871[6]3645943   6750196[23]9737159                   95  12371742[5]0729349 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=2371742[5]0729347
1185871[6]3645953   6750196[23]0466521    -237174[6]0729255  1 (1)B> 12371742[5]0729350 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=2371742[5]0729347, repcount=1185871[5]0364674, factor=3/2
1778807[6]5469323   1518794[24]7600265                   93  13557614[5]1094023 (1)B> 12 0 12 2
== Executing PPA-CTR  5 (once), V(1)=3557614[5]1094022
1778807[6]5469332   1518794[24]3070404    -355761[6]1093932  1 (1)B> 13557614[5]1094027 2 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=3557614[5]1094024, repcount=1778807[5]0547013, factor=3/2
2668210[6]8204397   3417286[24]8967574                   94  15336421[5]1641040 (1)B> 1 2 12 2
== Executing PPA-CTR  6 (once), V(1)=5336421[5]1641038, V(2)=0
2668210[6]8204405   3417286[24]0608625    -533642[6]1640947  1 (1)B> 15336421[5]1641041 0 1 0 1 2
== Executing  PA-CTR  2, V(1)=0, V(2)=5336421[5]1641038, repcount=2668210[5]0820520, factor=3/2
4002315[6]2307005   7688895[24]8877265                   93  18004631[5]2461561 (1)B> 1 0 1 0 1 2
== Executing PPA-CTR 17 (once), V(1)=8004631[5]2461560
4002315[6]2307019   7688895[24]1338847    -800463[6]2461469  1 (1)B> 18004631[5]2461566 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=8004631[5]2461563, repcount=4002315[5]1230782, factor=3/2
6003473[6]8460929   1730001[25]2097375                   95  11200694[6]3692347 (1)B> 12 0 12 2
== Executing PPA-CTR  5 (once), V(1)=1200694[6]3692346
6003473[6]8460938   1730001[25]0559134    -120069[7]3692254  1 (1)B> 11200694[6]3692351 2 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=1200694[6]3692348, repcount=6003473[5]1846175, factor=3/2
9005210[6]7691813   3892503[25]5496984                   96  11801042[6]5538526 (1)B> 1 2 12 2
== Executing PPA-CTR  6 (once), V(1)=1801042[6]5538524, V(2)=0
9005210[6]7691821   3892503[25]1035521    -180104[7]5538431  1 (1)B> 11801042[6]5538527 0 1 0 1 2
== Executing  PA-CTR  2, V(1)=0, V(2)=1801042[6]5538524, repcount=9005210[5]7769263, factor=3/2
1350781[7]6538136   8758132[25]9645691                   95  12701563[6]3307790 (1)B> 1 0 1 0 1 2
== Executing PPA-CTR 17 (once), V(1)=2701563[6]3307789
1350781[7]6538150   8758132[25]2953502    -270156[7]3307696  1 (1)B> 12701563[6]3307795 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=2701563[6]3307792, repcount=1350781[6]6653897, factor=3/2
2026172[7]9807635   1970579[26]4519920                   98  14052344[6]9961692 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=4052344[6]9961691, V(2)=0
2026172[7]9807646   1970579[26]4328420    -405234[7]9961596  1 (1)B> 14052344[6]9961699 2
== Executing  PA-CTR 10, V(1)=0, V(2)=4052344[6]9961696, repcount=2026172[6]4980849, factor=3/2
3039258[7]4711891   4433804[26]4663414                  102  16078517[6]4942548 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=6078517[6]4942546
3039258[7]4711901   4433804[26]9605975    -607851[7]4942447  1 (1)B> 16078517[6]4942549 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=6078517[6]4942546, repcount=3039258[6]2471274, factor=3/2
4558887[7]7068271   9976060[26]0359719                  101  19117775[6]7413823 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=9117775[6]7413822, V(2)=0
4558887[7]7068282   9976060[26]7428874    -911777[7]7413724  1 (1)B> 19117775[6]7413830 2
== Executing  PA-CTR 10, V(1)=0, V(2)=9117775[6]7413827, repcount=4558887[6]3706914, factor=3/2
6838331[7]5602852   2244613[27]0332218                  104  11367666[7]1120743 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=1367666[7]1120742, V(2)=0
6838331[7]5602861   2244613[27]5935961    -136766[8]1120641  1 (1)B> 11367666[7]1120748 2
== Executing  PA-CTR 10, V(1)=0, V(2)=1367666[7]1120745, repcount=6838331[6]5560373, factor=3/2
1025749[8]3404726   5050380[27]0055211                  105  12051499[7]6681120 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=2051499[7]6681119, V(2)=0
1025749[8]3404735   5050380[27]3460839    -205149[8]6681017  1 (1)B> 12051499[7]6681125 2
== Executing  PA-CTR 10, V(1)=0, V(2)=2051499[7]6681122, repcount=1025749[7]3340562, factor=3/2
1538624[8]0107545   1136335[28]0402647                  107  13077249[7]0021687 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=3077249[7]0021685
1538624[8]0107555   1136335[28]0424347    -307724[8]0021581  1 (1)B> 13077249[7]0021688 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=3077249[7]0021685, repcount=1538624[7]5010843, factor=3/2
2307937[8]5161770   2556755[28]5978357                  105  14615874[7]5032530 (1)B> 12 0 12 2
== Executing PPA-CTR  5 (once), V(1)=4615874[7]5032529
2307937[8]5161779   2556755[28]1141031    -461587[8]5032427  1 (1)B> 14615874[7]5032534 2 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=4615874[7]5032531, repcount=2307937[7]2516266, factor=3/2
3461905[8]7743109   5752699[28]8832759                  105  16923811[7]7548799 (1)B> 12 2 12 2
== Executing PPA-CTR 16 (once), V(1)=6923811[7]7548798, V(2)=0, V(3)=0
3461905[8]7743123   5752699[28]6772015    -692381[8]7548697  1 (1)B> 16923811[7]7548808 2
== Executing  PA-CTR 10, V(1)=0, V(2)=6923811[7]7548805, repcount=3461905[7]3774403, factor=3/2
5192858[8]6615138   1294357[29]0103305                  109  11038571[8]1323210 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=1038571[8]1323209, V(2)=0
5192858[8]6615147   1294357[29]6719383    -103857[9]1323103  1 (1)B> 11038571[8]1323215 2
== Executing  PA-CTR 10, V(1)=0, V(2)=1038571[8]1323212, repcount=5192858[7]0661607, factor=3/2
7789287[8]9923182   2912303[29]7593361                  111  11557857[8]1984822 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=1557857[8]1984820
7789287[8]9923192   2912303[29]9578196    -155785[9]1984712  1 (1)B> 11557857[8]1984823 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=1557857[8]1984820, repcount=7789287[7]5992411, factor=3/2
1168393[9]9885247   6552683[29]9044654                  110  12336786[8]7977234 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=2336786[8]7977233, V(2)=0
1168393[9]9885258   6552683[29]8930864    -233678[9]7977126  1 (1)B> 12336786[8]7977241 2
== Executing  PA-CTR 10, V(1)=0, V(2)=2336786[8]7977238, repcount=1168393[8]8988620, factor=3/2
1752589[9]4828358   1474353[30]3820704                  114  13505179[8]6965861 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=3505179[8]6965859
1752589[9]4828368   1474353[30]0786578    -350517[9]6965748  1 (1)B> 13505179[8]6965862 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=3505179[8]6965859, repcount=1752589[8]8482930, factor=3/2
2628884[9]7243018   3317296[30]0891138                  112  15257769[8]5448791 (1)B> 12 0 12 2
== Executing PPA-CTR  5 (once), V(1)=5257769[8]5448790
2628884[9]7243027   3317296[30]8135117    -525776[9]5448681  1 (1)B> 15257769[8]5448795 2 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=5257769[8]5448792, repcount=2628884[8]7724397, factor=3/2
3943326[9]5865012   7463916[30]4909535                  113  17886653[8]3173192 (1)B> 1 2 12 2
== Executing PPA-CTR  6 (once), V(1)=7886653[8]3173190, V(2)=0
3943326[9]5865020   7463916[30]8082738    -788665[9]3173080  1 (1)B> 17886653[8]3173193 0 1 0 1 2
== Executing  PA-CTR  2, V(1)=0, V(2)=7886653[8]3173190, repcount=3943326[8]1586596, factor=3/2
5914990[9]3798000   1679381[31]8325186                  112  11182998[9]4759789 (1)B> 1 0 1 0 1 2
== Executing PPA-CTR 17 (once), V(1)=1182998[9]4759788
5914990[9]3798014   1679381[31]3084996   -118299[10]4759678  1 (1)B> 11182998[9]4759794 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=1182998[9]4759791, repcount=5914990[8]2379896, factor=3/2
8872485[9]5697494   3778607[31]1468644                  114  11774497[9]7139689 (1)B> 12 0 12 2
== Executing PPA-CTR  5 (once), V(1)=1774497[9]7139688
8872485[9]5697503   3778607[31]7167113   -177449[10]7139577  1 (1)B> 11774497[9]7139693 2 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=1774497[9]7139690, repcount=8872485[8]3569846, factor=3/2
1330872[10]3546733   8501867[31]2787561                  115  12661745[9]0709539 (1)B> 1 2 12 2
== Executing PPA-CTR  6 (once), V(1)=2661745[9]0709537, V(2)=0
1330872[10]3546741   8501867[31]3497111   -266174[10]0709425  1 (1)B> 12661745[9]0709540 0 1 0 1 2
== Executing  PA-CTR  2, V(1)=0, V(2)=2661745[9]0709537, repcount=1330872[9]0354769, factor=3/2
1996309[10]5320586   1912920[32]4014505                  113  13992618[9]1064308 (1)B> 12 0 1 0 1 2
== Executing PPA-CTR  3 (once), V(1)=3992618[9]1064307
1996309[10]5320595   1912920[32]9336069   -399261[10]1064197  1 (1)B> 13992618[9]1064312 2 1 0 1 2
== Executing  PA-CTR  2, V(1)=0, V(2)=3992618[9]1064309, repcount=1996309[9]0532155, factor=3/2
2994463[10]7981370   4304070[32]9386079                  113  15988927[9]1596466 (1)B> 12 2 1 0 1 2
== Executing PPA-CTR  4 (once), V(1)=5988927[9]1596465, V(2)=0
2994463[10]7981387   4304070[32]7368447   -598892[10]1596355  1 (1)B> 15988927[9]1596473 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=5988927[9]1596470, repcount=2994463[9]0798236, factor=3/2
4491695[10]1972567   9684158[32]1217455                  117  18983391[9]2394709 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=8983391[9]2394708, V(2)=0
4491695[10]1972578   9684158[32]3191040   -898339[10]2394594  1 (1)B> 18983391[9]2394716 2
== Executing  PA-CTR 10, V(1)=0, V(2)=8983391[9]2394713, repcount=4491695[9]1197357, factor=3/2
6737543[10]7959363   2178935[33]0272018                  120  11347508[10]3592072 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=1347508[10]3592071, V(2)=0
6737543[10]7959372   2178935[33]8232406   -134750[11]3591954  1 (1)B> 11347508[10]3592077 2
== Executing  PA-CTR 10, V(1)=0, V(2)=1347508[10]3592074, repcount=6737543[9]6796038, factor=3/2
1010631[11]1939562   4902605[33]4769526                  122  12021263[10]0388115 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=2021263[10]0388113
1010631[11]1939572   4902605[33]5157654   -202126[11]0387994  1 (1)B> 12021263[10]0388116 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=2021263[10]0388113, repcount=1010631[10]0194057, factor=3/2
1515947[11]2909857   1103086[34]6201832                  120  13031894[10]0582172 (1)B> 12 0 12 2
== Executing PPA-CTR  5 (once), V(1)=3031894[10]0582171
1515947[11]2909866   1103086[34]9112716   -303189[11]0582054  1 (1)B> 13031894[10]0582176 2 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=3031894[10]0582173, repcount=1515947[10]5291087, factor=3/2
2273920[11]9365301   2481943[34]2455174                  120  14547841[10]5873262 (1)B> 12 2 12 2
== Executing PPA-CTR 16 (once), V(1)=4547841[10]5873261, V(2)=0, V(3)=0
2273920[11]9365315   2481943[34]5314597   -454784[11]5873145  1 (1)B> 14547841[10]5873271 2
== Executing  PA-CTR 10, V(1)=0, V(2)=4547841[10]5873268, repcount=2273920[10]7936635, factor=3/2
3410881[11]9048490   5584373[34]1293567                  125  16821762[10]3809906 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=6821762[10]3809904
3410881[11]9048500   5584373[34]5103486   -682176[11]3809782  1 (1)B> 16821762[10]3809907 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=6821762[10]3809904, repcount=3410881[10]1904953, factor=3/2
5116322[11]8573265   1256484[35]3556176                  124  11023264[11]5714860 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=1023264[11]5714859, V(2)=0
5116322[11]8573276   1256484[35]2130516   -102326[12]5714738  1 (1)B> 11023264[11]5714867 2
== Executing  PA-CTR 10, V(1)=0, V(2)=1023264[11]5714864, repcount=5116322[10]2857433, factor=3/2
7674483[11]2860441   2827089[35]6516646                  128  11534896[11]8572300 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=1534896[11]8572298
7674483[11]2860451   2827089[35]5088959   -153489[12]8572173  1 (1)B> 11534896[11]8572301 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=1534896[11]8572298, repcount=7674483[10]9286150, factor=3/2
1151172[12]9291201   6360950[35]7457759                  127  12302344[11]7858451 (1)B> 1 0 12 2
== Executing PPA-CTR 12 (once), V(1)=2302344[11]7858450, V(2)=0
1151172[12]9291212   6360950[35]6750054   -230234[12]7858326  1 (1)B> 12302344[11]7858458 2
== Executing  PA-CTR 10, V(1)=0, V(2)=2302344[11]7858455, repcount=1151172[11]8929228, factor=3/2
1726758[12]3937352   1431213[36]9956694                  130  13453517[11]6787685 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=3453517[11]6787684, V(2)=0
1726758[12]3937361   1431213[36]3895147   -345351[12]6787557  1 (1)B> 13453517[11]6787690 2
== Executing  PA-CTR 10, V(1)=0, V(2)=3453517[11]6787687, repcount=1726758[11]3393844, factor=3/2
2590138[12]0906581   3220231[36]7199291                  131  15180276[11]0181533 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=5180276[11]0181532, V(2)=0
2590138[12]0906590   3220231[36]8106984   -518027[12]0181404  1 (1)B> 15180276[11]0181538 2
== Executing  PA-CTR 10, V(1)=0, V(2)=5180276[11]0181535, repcount=2590138[11]0090768, factor=3/2
3885207[12]1360430   7245520[36]2175144                  132  17770414[11]0272305 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=7770414[11]0272304, V(2)=0
3885207[12]1360439   7245520[36]3536697   -777041[12]0272175  1 (1)B> 17770414[11]0272310 2
== Executing  PA-CTR 10, V(1)=0, V(2)=7770414[11]0272307, repcount=3885207[11]5136154, factor=3/2
5827810[12]7041209   1630242[37]2640841                  133  11165562[12]5408463 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=1165562[12]5408462, V(2)=0
5827810[12]7041218   1630242[37]9683184   -116556[13]5408332  1 (1)B> 11165562[12]5408468 2
== Executing  PA-CTR 10, V(1)=0, V(2)=1165562[12]5408465, repcount=5827810[11]2704233, factor=3/2
8741715[12]0562383   3668044[37]8843714                  134  11748343[12]8112700 (1)B> 12 2
== Executing PPA-CTR 13 (once), V(1)=1748343[12]8112699, V(2)=0
8741715[12]0562392   3668044[37]9407242   -174834[13]8112568  1 (1)B> 11748343[12]8112705 2
== Executing  PA-CTR 10, V(1)=0, V(2)=1748343[12]8112702, repcount=8741715[11]4056352, factor=3/2
1311257[13]0844152   8253100[37]7370890                  136  12622514[12]2169057 (1)B> 1 2
== Executing PPA-CTR 11 (once), V(1)=2622514[12]2169055
1311257[13]0844162   8253100[37]9539960   -262251[13]2168922  1 (1)B> 12622514[12]2169058 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=2622514[12]2169055, repcount=1311257[12]6084528, factor=3/2
1966886[13]1266802   1856947[38]8451000                  134  13933772[12]8253585 (1)B> 12 0 12 2
== Executing PPA-CTR  5 (once), V(1)=3933772[12]8253584
1966886[13]1266811   1856947[38]9718949   -393377[13]8253453  1 (1)B> 13933772[12]8253589 2 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=3933772[12]8253586, repcount=1966886[12]9126794, factor=3/2
2950329[13]6900781   4178132[38]1551093                  135  15900658[12]7380383 (1)B> 1 2 12 2
== Executing PPA-CTR  6 (once), V(1)=5900658[12]7380381, V(2)=0
2950329[13]6900789   4178132[38]8931487   -590065[13]7380249  1 (1)B> 15900658[12]7380384 0 1 0 1 2
== Executing  PA-CTR  2, V(1)=0, V(2)=5900658[12]7380381, repcount=2950329[12]3690191, factor=3/2
4425493[13]5351744   9400797[38]0912665                  133  18850987[12]1070574 (1)B> 12 0 1 0 1 2
== Executing PPA-CTR  3 (once), V(1)=8850987[12]1070573
4425493[13]5351753   9400797[38]6265559   -885098[13]1070443  1 (1)B> 18850987[12]1070578 2 1 0 1 2
== Executing  PA-CTR  2, V(1)=0, V(2)=8850987[12]1070575, repcount=4425493[12]5535288, factor=3/2
6638240[13]3028193   2115179[39]2146679                  133  11327648[13]6605865 (1)B> 12 2 1 0 1 2
== Executing PPA-CTR  4 (once), V(1)=1327648[13]6605864, V(2)=0
6638240[13]3028210   2115179[39]5176042   -132764[14]6605734  1 (1)B> 11327648[13]6605872 0 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=1327648[13]6605869, repcount=6638240[12]3302935, factor=3/2
9957360[13]9542885   4759153[39]2496612                  136  11991472[13]9908806 (1)B> 12 0 12 2
== Executing PPA-CTR  5 (once), V(1)=1991472[13]9908805
9957360[13]9542894   4759153[39]2040666   -199147[14]9908672  1 (1)B> 11991472[13]9908810 2 12 2
== Executing  PA-CTR  1, V(1)=0, V(2)=1991472[13]9908807, repcount=9957360[12]9954404, factor=3/2
1493604[14]9314914   1070809[40]5464810                  136  12987208[13]9863213 (1)B> 12 2 12 2

Lines:       500
Top steps:   499
Macro steps: 1493604130025095043699314914
Basic steps: 107080958266945009047565808606843399894171920385464810
Tape index:  136
nonzeros:    298720826005019008739863220
log10(nonzeros):   26.475
log10(steps   ):   53.030

Some long numbers above are shortened: #(omitted digits) shown in "[]".

The same TM just simple.
The same TM with repetitions reduced.
The same TM with tape symbol exponents.
The same TM as 1-bck-macro machine.

To the BB simulations page of Heiner Marxen.
To the busy beaver page of Heiner Marxen.
To the home page of Heiner Marxen.
Input to awk program:
    gohalt 1
    nbs 3
    T 4-state 3-symbol #b (T.J. & S. Ligocki)
    : >1.1x10^713 >1.5x10^1426
    5T  1RB 0LC 1RH  2LC 1RD 0LB  2LA 1LC 1LA  1RB 2LD 2RA
    L 16
    M	500
    pref	sim
    machv Lig43_b  	just simple
    machv Lig43_b-r	with repetitions reduced
    machv Lig43_b-1	with tape symbol exponents
    machv Lig43_b-m	as 1-bck-macro machine
    machv Lig43_b-a	as 1-bck-macro machine with pure additive config-TRs
    iam	Lig43_b-a
    mtype	1 0
    mmtyp	3
    r	1
    H	1
    mac	0
    E	2
    sympr	
    HM	1
    date	Tue Jul  6 22:14:01 CEST 2010
    edate	Tue Jul  6 22:14:03 CEST 2010
    bnspeed	1
    short	7

Constructed by: $Id: tmJob.awk,v 1.34 2010/05/06 18:26:17 heiner Exp $ $Id: basics.awk,v 1.1 2010/05/06 17:24:17 heiner Exp $ $Id: htSupp.awk,v 1.14 2010/07/06 19:48:32 heiner Exp $ $Id: mmSim.awk,v 1.34 2005/01/09 22:23:28 heiner Exp $ $Id: bignum.awk,v 1.34 2010/05/06 17:58:14 heiner Exp $ $Id: varLI.awk,v 1.11 2005/01/15 21:01:29 heiner Exp $ bignum signature: LEN={S++:9 U++:9 S+:8 U+:8 S*:4 U*:4} DONT: y i o;
Start: Tue Jul 6 22:14:01 CEST 2010
Ready: Tue Jul 6 22:14:03 CEST 2010