6-state TM #a from MaBu-List

Comment: This TM produces 17485734 ones in 95547257425490 steps.

State on
0
on
1
on 0 on 1
Print Move Goto Print Move Goto
A B1R C0L 1 right B 0 left C
B A1L A0R 1 left A 0 right A
C D0L Z1R 0 left D 1 right Z
D E1R D1L 1 right E 1 left D
E F0L E0L 0 left F 0 left E
F F1R B0L 1 right F 0 left B
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(0) 1
    3                    4                   -2  <D(0) 0 1
    4                    7                   -3  <B(0) 02 1
    5                    8                   -4  <A(1) 03 1
    6                   10                   -2  1 (0)A> 03 1
    7                   11                   -1  1 0 (1)B> 02 1
    8                   13                   -3  1 0 <C(0) 1 0 1
    9                   14                   -4  1 <D(0) 0 1 0 1
   10                   15                   -5  <D(1) 02 1 0 1
   11                   18                   -6  <E(0) 03 1 0 1
   12                   19                   -7  <F(0) 04 1 0 1
   13                   21                   -5  1 (1)F> 04 1 0 1
   14                   25                   -1  15 (1)F> 1 0 1
   15                   28                    0  15 0 (1)B> 0 1
   16                   30                   -2  15 0 <C(0) 12
   17                   31                   -3  15 <D(0) 0 12
   18                   32                   -4  14 <D(1) 02 12
   19                   36                   -8  <D(1) 14 02 12
   20                   39                   -9  <E(0) 0 14 02 12
   21                   40                  -10  <F(0) 02 14 02 12
   22                   42                   -8  1 (1)F> 02 14 02 12
   23                   44                   -6  13 (1)F> 14 02 12
   24                   47                   -5  13 0 (1)B> 13 02 12
   25                   48                   -4  13 0 1 (0)A> 12 02 12
   26                   50                   -6  13 0 1 <D(0) 0 1 02 12
   27                   51                   -7  13 0 <D(1) 02 1 02 12
   28                   54                   -8  13 <E(0) 03 1 02 12
   29                   57                  -11  <E(0) 06 1 02 12
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  <E(0) 01+V(2) 14+V(1) [*]* [*]*
    1                    1                   -1  <F(0) 02+V(2) 14+V(1) [*]* [*]*
    2                    3                    1  1 (1)F> 02+V(2) 14+V(1) [*]* [*]*
    3               5+V(2)               3+V(2)  13+V(2) (1)F> 14+V(1) [*]* [*]*
    4               8+V(2)               4+V(2)  13+V(2) 0 (1)B> 13+V(1) [*]* [*]*
    5               9+V(2)               5+V(2)  13+V(2) 0 1 (0)A> 12+V(1) [*]* [*]*
    6              11+V(2)               3+V(2)  13+V(2) 0 1 <D(0) 0 11+V(1) [*]* [*]*
    7              12+V(2)               2+V(2)  13+V(2) 0 <D(1) 02 11+V(1) [*]* [*]*
    8              15+V(2)               1+V(2)  13+V(2) <E(0) 03 11+V(1) [*]* [*]*
    9            18+2*V(2)                   -2  <E(0) 06+V(2) 11+V(1) [*]* [*]*
<< Success! ==> defined new CTR 1 (PA)
   30                   58                  -12  <F(0) 07 1 02 12
   31                   60                  -10  1 (1)F> 07 1 02 12
   32                   67                   -3  18 (1)F> 1 02 12
   33                   70                   -2  18 0 (1)B> 02 12
   34                   72                   -4  18 0 <C(0) 1 0 12
   35                   73                   -5  18 <D(0) 0 1 0 12
   36                   74                   -6  17 <D(1) 02 1 0 12
   37                   81                  -13  <D(1) 17 02 1 0 12
   38                   84                  -14  <E(0) 0 17 02 1 0 12
   39                   85                  -15  <F(0) 02 17 02 1 0 12
   40                   87                  -13  1 (1)F> 02 17 02 1 0 12
   41                   89                  -11  13 (1)F> 17 02 1 0 12
   42                   92                  -10  13 0 (1)B> 16 02 1 0 12
   43                   93                   -9  13 0 1 (0)A> 15 02 1 0 12
   44                   95                  -11  13 0 1 <D(0) 0 14 02 1 0 12
   45                   96                  -12  13 0 <D(1) 02 14 02 1 0 12
   46                   99                  -13  13 <E(0) 03 14 02 1 0 12
   47                  102                  -16  <E(0) 06 14 02 1 0 12
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  <E(0) 01+V(2) 14+V(1) [*]* [*]* [*]* [*]*
    1                    1                   -1  <F(0) 02+V(2) 14+V(1) [*]* [*]* [*]* [*]*
    2                    3                    1  1 (1)F> 02+V(2) 14+V(1) [*]* [*]* [*]* [*]*
    3               5+V(2)               3+V(2)  13+V(2) (1)F> 14+V(1) [*]* [*]* [*]* [*]*
    4               8+V(2)               4+V(2)  13+V(2) 0 (1)B> 13+V(1) [*]* [*]* [*]* [*]*
    5               9+V(2)               5+V(2)  13+V(2) 0 1 (0)A> 12+V(1) [*]* [*]* [*]* [*]*
    6              11+V(2)               3+V(2)  13+V(2) 0 1 <D(0) 0 11+V(1) [*]* [*]* [*]* [*]*
    7              12+V(2)               2+V(2)  13+V(2) 0 <D(1) 02 11+V(1) [*]* [*]* [*]* [*]*
    8              15+V(2)               1+V(2)  13+V(2) <E(0) 03 11+V(1) [*]* [*]* [*]* [*]*
    9            18+2*V(2)                   -2  <E(0) 06+V(2) 11+V(1) [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 2 (PA)
   47                  102                  -16  <E(0) 06 14 02 1 0 12
== Executing  PA-CTR  2, V(1)=0, V(2)=5, repcount=1, factor=5/3
   56                  130                  -18  <E(0) 011 1 02 1 0 12
   57                  131                  -19  <F(0) 012 1 02 1 0 12
   58                  133                  -17  1 (1)F> 012 1 02 1 0 12
   59                  145                   -5  113 (1)F> 1 02 1 0 12
   60                  148                   -4  113 0 (1)B> 02 1 0 12
   61                  150                   -6  113 0 <C(0) 1 0 1 0 12
   62                  151                   -7  113 <D(0) 0 1 0 1 0 12
   63                  152                   -8  112 <D(1) 02 1 0 1 0 12
   64                  164                  -20  <D(1) 112 02 1 0 1 0 12
   65                  167                  -21  <E(0) 0 112 02 1 0 1 0 12
   66                  168                  -22  <F(0) 02 112 02 1 0 1 0 12
   67                  170                  -20  1 (1)F> 02 112 02 1 0 1 0 12
   68                  172                  -18  13 (1)F> 112 02 1 0 1 0 12
   69                  175                  -17  13 0 (1)B> 111 02 1 0 1 0 12
   70                  176                  -16  13 0 1 (0)A> 110 02 1 0 1 0 12
   71                  178                  -18  13 0 1 <D(0) 0 19 02 1 0 1 0 12
   72                  179                  -19  13 0 <D(1) 02 19 02 1 0 1 0 12
   73                  182                  -20  13 <E(0) 03 19 02 1 0 1 0 12
   74                  185                  -23  <E(0) 06 19 02 1 0 1 0 12
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  <E(0) 01+V(2) 14+V(1) [*]* [*]* [*]* [*]* [*]* [*]*
    1                    1                   -1  <F(0) 02+V(2) 14+V(1) [*]* [*]* [*]* [*]* [*]* [*]*
    2                    3                    1  1 (1)F> 02+V(2) 14+V(1) [*]* [*]* [*]* [*]* [*]* [*]*
    3               5+V(2)               3+V(2)  13+V(2) (1)F> 14+V(1) [*]* [*]* [*]* [*]* [*]* [*]*
    4               8+V(2)               4+V(2)  13+V(2) 0 (1)B> 13+V(1) [*]* [*]* [*]* [*]* [*]* [*]*
    5               9+V(2)               5+V(2)  13+V(2) 0 1 (0)A> 12+V(1) [*]* [*]* [*]* [*]* [*]* [*]*
    6              11+V(2)               3+V(2)  13+V(2) 0 1 <D(0) 0 11+V(1) [*]* [*]* [*]* [*]* [*]* [*]*
    7              12+V(2)               2+V(2)  13+V(2) 0 <D(1) 02 11+V(1) [*]* [*]* [*]* [*]* [*]* [*]*
    8              15+V(2)               1+V(2)  13+V(2) <E(0) 03 11+V(1) [*]* [*]* [*]* [*]* [*]* [*]*
    9            18+2*V(2)                   -2  <E(0) 06+V(2) 11+V(1) [*]* [*]* [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 3 (PA)
   74                  185                  -23  <E(0) 06 19 02 1 0 1 0 12
== Executing  PA-CTR  3, V(1)=5, V(2)=5, repcount=2, factor=5/3
   92                  251                  -27  <E(0) 016 13 02 1 0 1 0 12
   93                  252                  -28  <F(0) 017 13 02 1 0 1 0 12
   94                  254                  -26  1 (1)F> 017 13 02 1 0 1 0 12
   95                  271                   -9  118 (1)F> 13 02 1 0 1 0 12
   96                  274                   -8  118 0 (1)B> 12 02 1 0 1 0 12
   97                  275                   -7  118 0 1 (0)A> 1 02 1 0 1 0 12
   98                  277                   -9  118 0 1 <D(0) 03 1 0 1 0 12
   99                  278                  -10  118 0 <D(1) 04 1 0 1 0 12
  100                  281                  -11  118 <E(0) 05 1 0 1 0 12
  101                  299                  -29  <E(0) 023 1 0 1 0 12
  102                  300                  -30  <F(0) 024 1 0 1 0 12
  103                  302                  -28  1 (1)F> 024 1 0 1 0 12
  104                  326                   -4  125 (1)F> 1 0 1 0 12
  105                  329                   -3  125 0 (1)B> 0 1 0 12
  106                  331                   -5  125 0 <C(0) 12 0 12
  107                  332                   -6  125 <D(0) 0 12 0 12
  108                  333                   -7  124 <D(1) 02 12 0 12
  109                  357                  -31  <D(1) 124 02 12 0 12
  110                  360                  -32  <E(0) 0 124 02 12 0 12
>> Try to prove a PPA-CTR with 3 Vars...
    0                    0                    0  <E(0) 01+V(3) 13 01+V(2) 1 0 11+V(1) [*]* [*]*
    1                    1                   -1  <F(0) 02+V(3) 13 01+V(2) 1 0 11+V(1) [*]* [*]*
    2                    3                    1  1 (1)F> 02+V(3) 13 01+V(2) 1 0 11+V(1) [*]* [*]*
    3               5+V(3)               3+V(3)  13+V(3) (1)F> 13 01+V(2) 1 0 11+V(1) [*]* [*]*
    4               8+V(3)               4+V(3)  13+V(3) 0 (1)B> 12 01+V(2) 1 0 11+V(1) [*]* [*]*
    5               9+V(3)               5+V(3)  13+V(3) 0 1 (0)A> 1 01+V(2) 1 0 11+V(1) [*]* [*]*
    6              11+V(3)               3+V(3)  13+V(3) 0 1 <D(0) 02+V(2) 1 0 11+V(1) [*]* [*]*
    7              12+V(3)               2+V(3)  13+V(3) 0 <D(1) 03+V(2) 1 0 11+V(1) [*]* [*]*
    8              15+V(3)               1+V(3)  13+V(3) <E(0) 04+V(2) 1 0 11+V(1) [*]* [*]*
    9            18+2*V(3)                   -2  <E(0) 07+V(2)+V(3) 1 0 11+V(1) [*]* [*]*
   10            19+2*V(3)                   -3  <F(0) 08+V(2)+V(3) 1 0 11+V(1) [*]* [*]*
   11            21+2*V(3)                   -1  1 (1)F> 08+V(2)+V(3) 1 0 11+V(1) [*]* [*]*
   12       29+V(2)+3*V(3)          7+V(2)+V(3)  19+V(2)+V(3) (1)F> 1 0 11+V(1) [*]* [*]*
   13       32+V(2)+3*V(3)          8+V(2)+V(3)  19+V(2)+V(3) 0 (1)B> 0 11+V(1) [*]* [*]*
   14       34+V(2)+3*V(3)          6+V(2)+V(3)  19+V(2)+V(3) 0 <C(0) 12+V(1) [*]* [*]*
   15       35+V(2)+3*V(3)          5+V(2)+V(3)  19+V(2)+V(3) <D(0) 0 12+V(1) [*]* [*]*
   16       36+V(2)+3*V(3)          4+V(2)+V(3)  18+V(2)+V(3) <D(1) 02 12+V(1) [*]* [*]*
   17     44+2*V(2)+4*V(3)                   -4  <D(1) 18+V(2)+V(3) 02 12+V(1) [*]* [*]*
   18     47+2*V(2)+4*V(3)                   -5  <E(0) 0 18+V(2)+V(3) 02 12+V(1) [*]* [*]*
<< Success! ==> defined new CTR 4 (PPA)
  110                  360                  -32  <E(0) 0 124 02 12 0 12
== Executing  PA-CTR  2, V(1)=20, V(2)=0, repcount=7, factor=5/3
  173                  696                  -46  <E(0) 036 13 02 12 0 12
  174                  697                  -47  <F(0) 037 13 02 12 0 12
  175                  699                  -45  1 (1)F> 037 13 02 12 0 12
  176                  736                   -8  138 (1)F> 13 02 12 0 12
  177                  739                   -7  138 0 (1)B> 12 02 12 0 12
  178                  740                   -6  138 0 1 (0)A> 1 02 12 0 12
  179                  742                   -8  138 0 1 <D(0) 03 12 0 12
  180                  743                   -9  138 0 <D(1) 04 12 0 12
  181                  746                  -10  138 <E(0) 05 12 0 12
  182                  784                  -48  <E(0) 043 12 0 12
  183                  785                  -49  <F(0) 044 12 0 12
  184                  787                  -47  1 (1)F> 044 12 0 12
  185                  831                   -3  145 (1)F> 12 0 12
  186                  834                   -2  145 0 (1)B> 1 0 12
  187                  835                   -1  145 0 1 (0)A> 0 12
  188                  836                    0  145 0 1 0 (1)B> 12
  189                  837                    1  145 0 1 0 1 (0)A> 1
  190                  839                   -1  145 0 1 0 1 <D(0)
  191                  840                   -2  145 0 1 0 <D(1)
  192                  843                   -3  145 0 1 <E(0)
  193                  844                   -4  145 0 <E(0)
  194                  845                   -5  145 <F(0)
  195                  846                   -6  144 <B(0)
  196                  848                   -4  143 0 (1)B>
  197                  850                   -6  143 0 <C(0) 1
  198                  851                   -7  143 <D(0) 0 1
  199                  852                   -8  142 <D(1) 02 1
  200                  894                  -50  <D(1) 142 02 1
  201                  897                  -51  <E(0) 0 142 02 1
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  <E(0) 01+V(2) 13 01+V(1) 12 0 12
    1                    1                   -1  <F(0) 02+V(2) 13 01+V(1) 12 0 12
    2                    3                    1  1 (1)F> 02+V(2) 13 01+V(1) 12 0 12
    3               5+V(2)               3+V(2)  13+V(2) (1)F> 13 01+V(1) 12 0 12
    4               8+V(2)               4+V(2)  13+V(2) 0 (1)B> 12 01+V(1) 12 0 12
    5               9+V(2)               5+V(2)  13+V(2) 0 1 (0)A> 1 01+V(1) 12 0 12
    6              11+V(2)               3+V(2)  13+V(2) 0 1 <D(0) 02+V(1) 12 0 12
    7              12+V(2)               2+V(2)  13+V(2) 0 <D(1) 03+V(1) 12 0 12
    8              15+V(2)               1+V(2)  13+V(2) <E(0) 04+V(1) 12 0 12
    9            18+2*V(2)                   -2  <E(0) 07+V(1)+V(2) 12 0 12
   10            19+2*V(2)                   -3  <F(0) 08+V(1)+V(2) 12 0 12
   11            21+2*V(2)                   -1  1 (1)F> 08+V(1)+V(2) 12 0 12
   12       29+V(1)+3*V(2)          7+V(1)+V(2)  19+V(1)+V(2) (1)F> 12 0 12
   13       32+V(1)+3*V(2)          8+V(1)+V(2)  19+V(1)+V(2) 0 (1)B> 1 0 12
   14       33+V(1)+3*V(2)          9+V(1)+V(2)  19+V(1)+V(2) 0 1 (0)A> 0 12
   15       34+V(1)+3*V(2)         10+V(1)+V(2)  19+V(1)+V(2) 0 1 0 (1)B> 12
   16       35+V(1)+3*V(2)         11+V(1)+V(2)  19+V(1)+V(2) 0 1 0 1 (0)A> 1
   17       37+V(1)+3*V(2)          9+V(1)+V(2)  19+V(1)+V(2) 0 1 0 1 <D(0)
   18       38+V(1)+3*V(2)          8+V(1)+V(2)  19+V(1)+V(2) 0 1 0 <D(1)
   19       41+V(1)+3*V(2)          7+V(1)+V(2)  19+V(1)+V(2) 0 1 <E(0)
   20       42+V(1)+3*V(2)          6+V(1)+V(2)  19+V(1)+V(2) 0 <E(0)
   21       43+V(1)+3*V(2)          5+V(1)+V(2)  19+V(1)+V(2) <F(0)
   22       44+V(1)+3*V(2)          4+V(1)+V(2)  18+V(1)+V(2) <B(0)
   23       46+V(1)+3*V(2)          6+V(1)+V(2)  17+V(1)+V(2) 0 (1)B>
   24       48+V(1)+3*V(2)          4+V(1)+V(2)  17+V(1)+V(2) 0 <C(0) 1
   25       49+V(1)+3*V(2)          3+V(1)+V(2)  17+V(1)+V(2) <D(0) 0 1
   26       50+V(1)+3*V(2)          2+V(1)+V(2)  16+V(1)+V(2) <D(1) 02 1
   27     56+2*V(1)+4*V(2)                   -4  <D(1) 16+V(1)+V(2) 02 1
   28     59+2*V(1)+4*V(2)                   -5  <E(0) 0 16+V(1)+V(2) 02 1
<< Success! ==> defined new CTR 5 (PPA)
  201                  897                  -51  <E(0) 0 142 02 1
== Executing  PA-CTR  1, V(1)=38, V(2)=0, repcount=13, factor=5/3
  318                 1911                  -77  <E(0) 066 13 02 1
  319                 1912                  -78  <F(0) 067 13 02 1
  320                 1914                  -76  1 (1)F> 067 13 02 1
  321                 1981                   -9  168 (1)F> 13 02 1
  322                 1984                   -8  168 0 (1)B> 12 02 1
  323                 1985                   -7  168 0 1 (0)A> 1 02 1
  324                 1987                   -9  168 0 1 <D(0) 03 1
  325                 1988                  -10  168 0 <D(1) 04 1
  326                 1991                  -11  168 <E(0) 05 1
  327                 2059                  -79  <E(0) 073 1
  328                 2060                  -80  <F(0) 074 1
  329                 2062                  -78  1 (1)F> 074 1
  330                 2136                   -4  175 (1)F> 1
  331                 2139                   -3  175 0 (1)B>
  332                 2141                   -5  175 0 <C(0) 1
  333                 2142                   -6  175 <D(0) 0 1
  334                 2143                   -7  174 <D(1) 02 1
  335                 2217                  -81  <D(1) 174 02 1
  336                 2220                  -82  <E(0) 0 174 02 1
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  <E(0) 01+V(2) 13 01+V(1) 1
    1                    1                   -1  <F(0) 02+V(2) 13 01+V(1) 1
    2                    3                    1  1 (1)F> 02+V(2) 13 01+V(1) 1
    3               5+V(2)               3+V(2)  13+V(2) (1)F> 13 01+V(1) 1
    4               8+V(2)               4+V(2)  13+V(2) 0 (1)B> 12 01+V(1) 1
    5               9+V(2)               5+V(2)  13+V(2) 0 1 (0)A> 1 01+V(1) 1
    6              11+V(2)               3+V(2)  13+V(2) 0 1 <D(0) 02+V(1) 1
    7              12+V(2)               2+V(2)  13+V(2) 0 <D(1) 03+V(1) 1
    8              15+V(2)               1+V(2)  13+V(2) <E(0) 04+V(1) 1
    9            18+2*V(2)                   -2  <E(0) 07+V(1)+V(2) 1
   10            19+2*V(2)                   -3  <F(0) 08+V(1)+V(2) 1
   11            21+2*V(2)                   -1  1 (1)F> 08+V(1)+V(2) 1
   12       29+V(1)+3*V(2)          7+V(1)+V(2)  19+V(1)+V(2) (1)F> 1
   13       32+V(1)+3*V(2)          8+V(1)+V(2)  19+V(1)+V(2) 0 (1)B>
   14       34+V(1)+3*V(2)          6+V(1)+V(2)  19+V(1)+V(2) 0 <C(0) 1
   15       35+V(1)+3*V(2)          5+V(1)+V(2)  19+V(1)+V(2) <D(0) 0 1
   16       36+V(1)+3*V(2)          4+V(1)+V(2)  18+V(1)+V(2) <D(1) 02 1
   17     44+2*V(1)+4*V(2)                   -4  <D(1) 18+V(1)+V(2) 02 1
   18     47+2*V(1)+4*V(2)                   -5  <E(0) 0 18+V(1)+V(2) 02 1
<< Success! ==> defined new CTR 6 (PPA)
  336                 2220                  -82  <E(0) 0 174 02 1
== Executing  PA-CTR  1, V(1)=70, V(2)=0, repcount=24, factor=5/3
  552                 5412                 -130  <E(0) 0121 12 02 1
  553                 5413                 -131  <F(0) 0122 12 02 1
  554                 5415                 -129  1 (1)F> 0122 12 02 1
  555                 5537                   -7  1123 (1)F> 12 02 1
  556                 5540                   -6  1123 0 (1)B> 1 02 1
  557                 5541                   -5  1123 0 1 (0)A> 02 1
  558                 5542                   -4  1123 0 1 0 (1)B> 0 1
  559                 5544                   -6  1123 0 1 0 <C(0) 12
  560                 5545                   -7  1123 0 1 <D(0) 0 12
  561                 5546                   -8  1123 0 <D(1) 02 12
  562                 5549                   -9  1123 <E(0) 03 12
  563                 5672                 -132  <E(0) 0126 12
  564                 5673                 -133  <F(0) 0127 12
  565                 5675                 -131  1 (1)F> 0127 12
  566                 5802                   -4  1128 (1)F> 12
  567                 5805                   -3  1128 0 (1)B> 1
  568                 5806                   -2  1128 0 1 (0)A>
  569                 5807                   -1  1128 0 1 0 (1)B>
  570                 5809                   -3  1128 0 1 0 <C(0) 1
  571                 5810                   -4  1128 0 1 <D(0) 0 1
  572                 5811                   -5  1128 0 <D(1) 02 1
  573                 5814                   -6  1128 <E(0) 03 1
  574                 5942                 -134  <E(0) 0131 1
  575                 5943                 -135  <F(0) 0132 1
  576                 5945                 -133  1 (1)F> 0132 1
  577                 6077                   -1  1133 (1)F> 1
  578                 6080                    0  1133 0 (1)B>
  579                 6082                   -2  1133 0 <C(0) 1
  580                 6083                   -3  1133 <D(0) 0 1
  581                 6084                   -4  1132 <D(1) 02 1
  582                 6216                 -136  <D(1) 1132 02 1
  583                 6219                 -137  <E(0) 0 1132 02 1
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  <E(0) 01+V(1) 12 02 1
    1                    1                   -1  <F(0) 02+V(1) 12 02 1
    2                    3                    1  1 (1)F> 02+V(1) 12 02 1
    3               5+V(1)               3+V(1)  13+V(1) (1)F> 12 02 1
    4               8+V(1)               4+V(1)  13+V(1) 0 (1)B> 1 02 1
    5               9+V(1)               5+V(1)  13+V(1) 0 1 (0)A> 02 1
    6              10+V(1)               6+V(1)  13+V(1) 0 1 0 (1)B> 0 1
    7              12+V(1)               4+V(1)  13+V(1) 0 1 0 <C(0) 12
    8              13+V(1)               3+V(1)  13+V(1) 0 1 <D(0) 0 12
    9              14+V(1)               2+V(1)  13+V(1) 0 <D(1) 02 12
   10              17+V(1)               1+V(1)  13+V(1) <E(0) 03 12
   11            20+2*V(1)                   -2  <E(0) 06+V(1) 12
   12            21+2*V(1)                   -3  <F(0) 07+V(1) 12
   13            23+2*V(1)                   -1  1 (1)F> 07+V(1) 12
   14            30+3*V(1)               6+V(1)  18+V(1) (1)F> 12
   15            33+3*V(1)               7+V(1)  18+V(1) 0 (1)B> 1
   16            34+3*V(1)               8+V(1)  18+V(1) 0 1 (0)A>
   17            35+3*V(1)               9+V(1)  18+V(1) 0 1 0 (1)B>
   18            37+3*V(1)               7+V(1)  18+V(1) 0 1 0 <C(0) 1
   19            38+3*V(1)               6+V(1)  18+V(1) 0 1 <D(0) 0 1
   20            39+3*V(1)               5+V(1)  18+V(1) 0 <D(1) 02 1
   21            42+3*V(1)               4+V(1)  18+V(1) <E(0) 03 1
   22            50+4*V(1)                   -4  <E(0) 011+V(1) 1
   23            51+4*V(1)                   -5  <F(0) 012+V(1) 1
   24            53+4*V(1)                   -3  1 (1)F> 012+V(1) 1
   25            65+5*V(1)               9+V(1)  113+V(1) (1)F> 1
   26            68+5*V(1)              10+V(1)  113+V(1) 0 (1)B>
   27            70+5*V(1)               8+V(1)  113+V(1) 0 <C(0) 1
   28            71+5*V(1)               7+V(1)  113+V(1) <D(0) 0 1
   29            72+5*V(1)               6+V(1)  112+V(1) <D(1) 02 1
   30            84+6*V(1)                   -6  <D(1) 112+V(1) 02 1
   31            87+6*V(1)                   -7  <E(0) 0 112+V(1) 02 1
<< Success! ==> defined new CTR 7 (PPA)
  583                 6219                 -137  <E(0) 0 1132 02 1
== Executing  PA-CTR  1, V(1)=128, V(2)=0, repcount=43, factor=5/3
  970                16023                 -223  <E(0) 0216 13 02 1
== Executing PPA-CTR  6 (once), V(1)=1, V(2)=215
  988                16932                 -228  <E(0) 0 1224 02 1
== Executing  PA-CTR  1, V(1)=220, V(2)=0, repcount=74, factor=5/3
 1654                45274                 -376  <E(0) 0371 12 02 1
== Executing PPA-CTR  7 (once), V(1)=370
 1685                47581                 -383  <E(0) 0 1382 02 1
== Executing  PA-CTR  1, V(1)=378, V(2)=0, repcount=127, factor=5/3
 2828               129877                 -637  <E(0) 0636 1 02 1
 2829               129878                 -638  <F(0) 0637 1 02 1
 2830               129880                 -636  1 (1)F> 0637 1 02 1
 2831               130517                    1  1638 (1)F> 1 02 1
 2832               130520                    2  1638 0 (1)B> 02 1
 2833               130522                    0  1638 0 <C(0) 1 0 1
 2834               130523                   -1  1638 <D(0) 0 1 0 1
 2835               130524                   -2  1637 <D(1) 02 1 0 1
 2836               131161                 -639  <D(1) 1637 02 1 0 1
 2837               131164                 -640  <E(0) 0 1637 02 1 0 1
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  <E(0) 03+V(2) 1 02+V(1) [*]*
    1                    1                   -1  <F(0) 04+V(2) 1 02+V(1) [*]*
    2                    3                    1  1 (1)F> 04+V(2) 1 02+V(1) [*]*
    3               7+V(2)               5+V(2)  15+V(2) (1)F> 1 02+V(1) [*]*
    4              10+V(2)               6+V(2)  15+V(2) 0 (1)B> 02+V(1) [*]*
    5              12+V(2)               4+V(2)  15+V(2) 0 <C(0) 1 01+V(1) [*]*
    6              13+V(2)               3+V(2)  15+V(2) <D(0) 0 1 01+V(1) [*]*
    7              14+V(2)               2+V(2)  14+V(2) <D(1) 02 1 01+V(1) [*]*
    8            18+2*V(2)                   -2  <D(1) 14+V(2) 02 1 01+V(1) [*]*
    9            21+2*V(2)                   -3  <E(0) 0 14+V(2) 02 1 01+V(1) [*]*
<< Success! ==> defined new CTR 8 (PPA)
 2837               131164                 -640  <E(0) 0 1637 02 1 0 1
== Executing  PA-CTR  2, V(1)=633, V(2)=0, repcount=212, factor=5/3
 4745               358640                -1064  <E(0) 01061 1 02 1 0 1
 4746               358641                -1065  <F(0) 01062 1 02 1 0 1
 4747               358643                -1063  1 (1)F> 01062 1 02 1 0 1
 4748               359705                   -1  11063 (1)F> 1 02 1 0 1
 4749               359708                    0  11063 0 (1)B> 02 1 0 1
 4750               359710                   -2  11063 0 <C(0) 1 0 1 0 1
 4751               359711                   -3  11063 <D(0) 0 1 0 1 0 1
 4752               359712                   -4  11062 <D(1) 02 1 0 1 0 1
 4753               360774                -1066  <D(1) 11062 02 1 0 1 0 1
 4754               360777                -1067  <E(0) 0 11062 02 1 0 1 0 1
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  <E(0) 03+V(2) 1 02+V(1) [*]* [*]* [*]*
    1                    1                   -1  <F(0) 04+V(2) 1 02+V(1) [*]* [*]* [*]*
    2                    3                    1  1 (1)F> 04+V(2) 1 02+V(1) [*]* [*]* [*]*
    3               7+V(2)               5+V(2)  15+V(2) (1)F> 1 02+V(1) [*]* [*]* [*]*
    4              10+V(2)               6+V(2)  15+V(2) 0 (1)B> 02+V(1) [*]* [*]* [*]*
    5              12+V(2)               4+V(2)  15+V(2) 0 <C(0) 1 01+V(1) [*]* [*]* [*]*
    6              13+V(2)               3+V(2)  15+V(2) <D(0) 0 1 01+V(1) [*]* [*]* [*]*
    7              14+V(2)               2+V(2)  14+V(2) <D(1) 02 1 01+V(1) [*]* [*]* [*]*
    8            18+2*V(2)                   -2  <D(1) 14+V(2) 02 1 01+V(1) [*]* [*]* [*]*
    9            21+2*V(2)                   -3  <E(0) 0 14+V(2) 02 1 01+V(1) [*]* [*]* [*]*
<< Success! ==> defined new CTR 9 (PPA)
 4754               360777                -1067  <E(0) 0 11062 02 1 0 1 0 1
== Executing  PA-CTR  3, V(1)=1058, V(2)=0, repcount=353, factor=5/3
 7931               988411                -1773  <E(0) 01766 13 02 1 0 1 0 1
== Executing PPA-CTR  4 (once), V(1)=0, V(2)=1, V(3)=1765
 7949               995520                -1778  <E(0) 0 11774 02 12 0 1
== Executing  PA-CTR  2, V(1)=1770, V(2)=0, repcount=591, factor=5/3
13268              2749608                -2960  <E(0) 02956 1 02 12 0 1
== Executing PPA-CTR  9 (once), V(1)=0, V(2)=2953
13277              2755535                -2963  <E(0) 0 12957 02 1 0 12 0 1
== Executing  PA-CTR  3, V(1)=2953, V(2)=0, repcount=985, factor=5/3
22142              7619465                -4933  <E(0) 04926 12 02 1 0 12 0 1
22143              7619466                -4934  <F(0) 04927 12 02 1 0 12 0 1
22144              7619468                -4932  1 (1)F> 04927 12 02 1 0 12 0 1
22145              7624395                   -5  14928 (1)F> 12 02 1 0 12 0 1
22146              7624398                   -4  14928 0 (1)B> 1 02 1 0 12 0 1
22147              7624399                   -3  14928 0 1 (0)A> 02 1 0 12 0 1
22148              7624400                   -2  14928 0 1 0 (1)B> 0 1 0 12 0 1
22149              7624402                   -4  14928 0 1 0 <C(0) 12 0 12 0 1
22150              7624403                   -5  14928 0 1 <D(0) 0 12 0 12 0 1
22151              7624404                   -6  14928 0 <D(1) 02 12 0 12 0 1
22152              7624407                   -7  14928 <E(0) 03 12 0 12 0 1
22153              7629335                -4935  <E(0) 04931 12 0 12 0 1
22154              7629336                -4936  <F(0) 04932 12 0 12 0 1
22155              7629338                -4934  1 (1)F> 04932 12 0 12 0 1
22156              7634270                   -2  14933 (1)F> 12 0 12 0 1
22157              7634273                   -1  14933 0 (1)B> 1 0 12 0 1
22158              7634274                    0  14933 0 1 (0)A> 0 12 0 1
22159              7634275                    1  14933 0 1 0 (1)B> 12 0 1
22160              7634276                    2  14933 0 1 0 1 (0)A> 1 0 1
22161              7634278                    0  14933 0 1 0 1 <D(0) 02 1
22162              7634279                   -1  14933 0 1 0 <D(1) 03 1
22163              7634282                   -2  14933 0 1 <E(0) 04 1
22164              7634283                   -3  14933 0 <E(0) 05 1
22165              7634284                   -4  14933 <F(0) 06 1
22166              7634285                   -5  14932 <B(0) 07 1
22167              7634287                   -3  14931 0 (1)B> 07 1
22168              7634289                   -5  14931 0 <C(0) 1 06 1
22169              7634290                   -6  14931 <D(0) 0 1 06 1
22170              7634291                   -7  14930 <D(1) 02 1 06 1
22171              7639221                -4937  <D(1) 14930 02 1 06 1
22172              7639224                -4938  <E(0) 0 14930 02 1 06 1
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  <E(0) 01+V(2) 12 02 1 0 12 01+V(1) [*]*
    1                    1                   -1  <F(0) 02+V(2) 12 02 1 0 12 01+V(1) [*]*
    2                    3                    1  1 (1)F> 02+V(2) 12 02 1 0 12 01+V(1) [*]*
    3               5+V(2)               3+V(2)  13+V(2) (1)F> 12 02 1 0 12 01+V(1) [*]*
    4               8+V(2)               4+V(2)  13+V(2) 0 (1)B> 1 02 1 0 12 01+V(1) [*]*
    5               9+V(2)               5+V(2)  13+V(2) 0 1 (0)A> 02 1 0 12 01+V(1) [*]*
    6              10+V(2)               6+V(2)  13+V(2) 0 1 0 (1)B> 0 1 0 12 01+V(1) [*]*
    7              12+V(2)               4+V(2)  13+V(2) 0 1 0 <C(0) 12 0 12 01+V(1) [*]*
    8              13+V(2)               3+V(2)  13+V(2) 0 1 <D(0) 0 12 0 12 01+V(1) [*]*
    9              14+V(2)               2+V(2)  13+V(2) 0 <D(1) 02 12 0 12 01+V(1) [*]*
   10              17+V(2)               1+V(2)  13+V(2) <E(0) 03 12 0 12 01+V(1) [*]*
   11            20+2*V(2)                   -2  <E(0) 06+V(2) 12 0 12 01+V(1) [*]*
   12            21+2*V(2)                   -3  <F(0) 07+V(2) 12 0 12 01+V(1) [*]*
   13            23+2*V(2)                   -1  1 (1)F> 07+V(2) 12 0 12 01+V(1) [*]*
   14            30+3*V(2)               6+V(2)  18+V(2) (1)F> 12 0 12 01+V(1) [*]*
   15            33+3*V(2)               7+V(2)  18+V(2) 0 (1)B> 1 0 12 01+V(1) [*]*
   16            34+3*V(2)               8+V(2)  18+V(2) 0 1 (0)A> 0 12 01+V(1) [*]*
   17            35+3*V(2)               9+V(2)  18+V(2) 0 1 0 (1)B> 12 01+V(1) [*]*
   18            36+3*V(2)              10+V(2)  18+V(2) 0 1 0 1 (0)A> 1 01+V(1) [*]*
   19            38+3*V(2)               8+V(2)  18+V(2) 0 1 0 1 <D(0) 02+V(1) [*]*
   20            39+3*V(2)               7+V(2)  18+V(2) 0 1 0 <D(1) 03+V(1) [*]*
   21            42+3*V(2)               6+V(2)  18+V(2) 0 1 <E(0) 04+V(1) [*]*
   22            43+3*V(2)               5+V(2)  18+V(2) 0 <E(0) 05+V(1) [*]*
   23            44+3*V(2)               4+V(2)  18+V(2) <F(0) 06+V(1) [*]*
   24            45+3*V(2)               3+V(2)  17+V(2) <B(0) 07+V(1) [*]*
   25            47+3*V(2)               5+V(2)  16+V(2) 0 (1)B> 07+V(1) [*]*
   26            49+3*V(2)               3+V(2)  16+V(2) 0 <C(0) 1 06+V(1) [*]*
   27            50+3*V(2)               2+V(2)  16+V(2) <D(0) 0 1 06+V(1) [*]*
   28            51+3*V(2)               1+V(2)  15+V(2) <D(1) 02 1 06+V(1) [*]*
   29            56+4*V(2)                   -4  <D(1) 15+V(2) 02 1 06+V(1) [*]*
   30            59+4*V(2)                   -5  <E(0) 0 15+V(2) 02 1 06+V(1) [*]*
<< Success! ==> defined new CTR 10 (PPA)
22172              7639224                -4938  <E(0) 0 14930 02 1 06 1
== Executing  PA-CTR  2, V(1)=4926, V(2)=0, repcount=1643, factor=5/3
36959             21157828                -8224  <E(0) 08216 1 02 1 06 1
== Executing PPA-CTR  9 (once), V(1)=0, V(2)=8213
36968             21174275                -8227  <E(0) 0 18217 02 1 0 1 06 1
== Executing  PA-CTR  3, V(1)=8213, V(2)=0, repcount=2738, factor=5/3
61610             58693089               -13703  <E(0) 013691 13 02 1 0 1 06 1
== Executing PPA-CTR  4 (once), V(1)=0, V(2)=1, V(3)=13690
61628             58747898               -13708  <E(0) 0 113699 02 12 06 1
== Executing  PA-CTR  2, V(1)=13695, V(2)=0, repcount=4566, factor=5/3
102722            163049036               -22840  <E(0) 022831 1 02 12 06 1
== Executing PPA-CTR  9 (once), V(1)=0, V(2)=22828
102731            163094713               -22843  <E(0) 0 122832 02 1 0 12 06 1
== Executing  PA-CTR  3, V(1)=22828, V(2)=0, repcount=7610, factor=5/3
171221            452754143               -38063  <E(0) 038051 12 02 1 0 12 06 1
== Executing PPA-CTR 10 (once), V(1)=5, V(2)=38050
171251            452906402               -38068  <E(0) 0 138055 02 1 011 1
== Executing  PA-CTR  2, V(1)=38051, V(2)=0, repcount=12684, factor=5/3
285407           1257490574               -63436  <E(0) 063421 13 02 1 011 1
285408           1257490575               -63437  <F(0) 063422 13 02 1 011 1
285409           1257490577               -63435  1 (1)F> 063422 13 02 1 011 1
285410           1257553999                  -13  163423 (1)F> 13 02 1 011 1
285411           1257554002                  -12  163423 0 (1)B> 12 02 1 011 1
285412           1257554003                  -11  163423 0 1 (0)A> 1 02 1 011 1
285413           1257554005                  -13  163423 0 1 <D(0) 03 1 011 1
285414           1257554006                  -14  163423 0 <D(1) 04 1 011 1
285415           1257554009                  -15  163423 <E(0) 05 1 011 1
285416           1257617432               -63438  <E(0) 063428 1 011 1
285417           1257617433               -63439  <F(0) 063429 1 011 1
285418           1257617435               -63437  1 (1)F> 063429 1 011 1
285419           1257680864                   -8  163430 (1)F> 1 011 1
285420           1257680867                   -7  163430 0 (1)B> 011 1
285421           1257680869                   -9  163430 0 <C(0) 1 010 1
285422           1257680870                  -10  163430 <D(0) 0 1 010 1
285423           1257680871                  -11  163429 <D(1) 02 1 010 1
285424           1257744300               -63440  <D(1) 163429 02 1 010 1
285425           1257744303               -63441  <E(0) 0 163429 02 1 010 1
>> Try to prove a PPA-CTR with 3 Vars...
    0                    0                    0  <E(0) 01+V(3) 13 01+V(2) 1 02+V(1) [*]*
    1                    1                   -1  <F(0) 02+V(3) 13 01+V(2) 1 02+V(1) [*]*
    2                    3                    1  1 (1)F> 02+V(3) 13 01+V(2) 1 02+V(1) [*]*
    3               5+V(3)               3+V(3)  13+V(3) (1)F> 13 01+V(2) 1 02+V(1) [*]*
    4               8+V(3)               4+V(3)  13+V(3) 0 (1)B> 12 01+V(2) 1 02+V(1) [*]*
    5               9+V(3)               5+V(3)  13+V(3) 0 1 (0)A> 1 01+V(2) 1 02+V(1) [*]*
    6              11+V(3)               3+V(3)  13+V(3) 0 1 <D(0) 02+V(2) 1 02+V(1) [*]*
    7              12+V(3)               2+V(3)  13+V(3) 0 <D(1) 03+V(2) 1 02+V(1) [*]*
    8              15+V(3)               1+V(3)  13+V(3) <E(0) 04+V(2) 1 02+V(1) [*]*
    9            18+2*V(3)                   -2  <E(0) 07+V(2)+V(3) 1 02+V(1) [*]*
   10            19+2*V(3)                   -3  <F(0) 08+V(2)+V(3) 1 02+V(1) [*]*
   11            21+2*V(3)                   -1  1 (1)F> 08+V(2)+V(3) 1 02+V(1) [*]*
   12       29+V(2)+3*V(3)          7+V(2)+V(3)  19+V(2)+V(3) (1)F> 1 02+V(1) [*]*
   13       32+V(2)+3*V(3)          8+V(2)+V(3)  19+V(2)+V(3) 0 (1)B> 02+V(1) [*]*
   14       34+V(2)+3*V(3)          6+V(2)+V(3)  19+V(2)+V(3) 0 <C(0) 1 01+V(1) [*]*
   15       35+V(2)+3*V(3)          5+V(2)+V(3)  19+V(2)+V(3) <D(0) 0 1 01+V(1) [*]*
   16       36+V(2)+3*V(3)          4+V(2)+V(3)  18+V(2)+V(3) <D(1) 02 1 01+V(1) [*]*
   17     44+2*V(2)+4*V(3)                   -4  <D(1) 18+V(2)+V(3) 02 1 01+V(1) [*]*
   18     47+2*V(2)+4*V(3)                   -5  <E(0) 0 18+V(2)+V(3) 02 1 01+V(1) [*]*
<< Success! ==> defined new CTR 11 (PPA)
285425           1257744303               -63441  <E(0) 0 163429 02 1 010 1
== Executing  PA-CTR  2, V(1)=63425, V(2)=0, repcount=21142, factor=5/3
475703           3492939969              -105725  <E(0) 0105711 13 02 1 010 1
== Executing PPA-CTR 11 (once), V(1)=8, V(2)=1, V(3)=105710
475721           3493362858              -105730  <E(0) 0 1105719 02 1 09 1
== Executing  PA-CTR  2, V(1)=105715, V(2)=0, repcount=35239, factor=5/3
792872           9702756570              -176208  <E(0) 0176196 12 02 1 09 1
792873           9702756571              -176209  <F(0) 0176197 12 02 1 09 1
792874           9702756573              -176207  1 (1)F> 0176197 12 02 1 09 1
792875           9702932770                  -10  1176198 (1)F> 12 02 1 09 1
792876           9702932773                   -9  1176198 0 (1)B> 1 02 1 09 1
792877           9702932774                   -8  1176198 0 1 (0)A> 02 1 09 1
792878           9702932775                   -7  1176198 0 1 0 (1)B> 0 1 09 1
792879           9702932777                   -9  1176198 0 1 0 <C(0) 12 09 1
792880           9702932778                  -10  1176198 0 1 <D(0) 0 12 09 1
792881           9702932779                  -11  1176198 0 <D(1) 02 12 09 1
792882           9702932782                  -12  1176198 <E(0) 03 12 09 1
792883           9703108980              -176210  <E(0) 0176201 12 09 1
792884           9703108981              -176211  <F(0) 0176202 12 09 1
792885           9703108983              -176209  1 (1)F> 0176202 12 09 1
792886           9703285185                   -7  1176203 (1)F> 12 09 1
792887           9703285188                   -6  1176203 0 (1)B> 1 09 1
792888           9703285189                   -5  1176203 0 1 (0)A> 09 1
792889           9703285190                   -4  1176203 0 1 0 (1)B> 08 1
792890           9703285192                   -6  1176203 0 1 0 <C(0) 1 07 1
792891           9703285193                   -7  1176203 0 1 <D(0) 0 1 07 1
792892           9703285194                   -8  1176203 0 <D(1) 02 1 07 1
792893           9703285197                   -9  1176203 <E(0) 03 1 07 1
792894           9703461400              -176212  <E(0) 0176206 1 07 1
792895           9703461401              -176213  <F(0) 0176207 1 07 1
792896           9703461403              -176211  1 (1)F> 0176207 1 07 1
792897           9703637610                   -4  1176208 (1)F> 1 07 1
792898           9703637613                   -3  1176208 0 (1)B> 07 1
792899           9703637615                   -5  1176208 0 <C(0) 1 06 1
792900           9703637616                   -6  1176208 <D(0) 0 1 06 1
792901           9703637617                   -7  1176207 <D(1) 02 1 06 1
792902           9703813824              -176214  <D(1) 1176207 02 1 06 1
792903           9703813827              -176215  <E(0) 0 1176207 02 1 06 1
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  <E(0) 01+V(2) 12 02 1 04+V(1) [*]*
    1                    1                   -1  <F(0) 02+V(2) 12 02 1 04+V(1) [*]*
    2                    3                    1  1 (1)F> 02+V(2) 12 02 1 04+V(1) [*]*
    3               5+V(2)               3+V(2)  13+V(2) (1)F> 12 02 1 04+V(1) [*]*
    4               8+V(2)               4+V(2)  13+V(2) 0 (1)B> 1 02 1 04+V(1) [*]*
    5               9+V(2)               5+V(2)  13+V(2) 0 1 (0)A> 02 1 04+V(1) [*]*
    6              10+V(2)               6+V(2)  13+V(2) 0 1 0 (1)B> 0 1 04+V(1) [*]*
    7              12+V(2)               4+V(2)  13+V(2) 0 1 0 <C(0) 12 04+V(1) [*]*
    8              13+V(2)               3+V(2)  13+V(2) 0 1 <D(0) 0 12 04+V(1) [*]*
    9              14+V(2)               2+V(2)  13+V(2) 0 <D(1) 02 12 04+V(1) [*]*
   10              17+V(2)               1+V(2)  13+V(2) <E(0) 03 12 04+V(1) [*]*
   11            20+2*V(2)                   -2  <E(0) 06+V(2) 12 04+V(1) [*]*
   12            21+2*V(2)                   -3  <F(0) 07+V(2) 12 04+V(1) [*]*
   13            23+2*V(2)                   -1  1 (1)F> 07+V(2) 12 04+V(1) [*]*
   14            30+3*V(2)               6+V(2)  18+V(2) (1)F> 12 04+V(1) [*]*
   15            33+3*V(2)               7+V(2)  18+V(2) 0 (1)B> 1 04+V(1) [*]*
   16            34+3*V(2)               8+V(2)  18+V(2) 0 1 (0)A> 04+V(1) [*]*
   17            35+3*V(2)               9+V(2)  18+V(2) 0 1 0 (1)B> 03+V(1) [*]*
   18            37+3*V(2)               7+V(2)  18+V(2) 0 1 0 <C(0) 1 02+V(1) [*]*
   19            38+3*V(2)               6+V(2)  18+V(2) 0 1 <D(0) 0 1 02+V(1) [*]*
   20            39+3*V(2)               5+V(2)  18+V(2) 0 <D(1) 02 1 02+V(1) [*]*
   21            42+3*V(2)               4+V(2)  18+V(2) <E(0) 03 1 02+V(1) [*]*
   22            50+4*V(2)                   -4  <E(0) 011+V(2) 1 02+V(1) [*]*
   23            51+4*V(2)                   -5  <F(0) 012+V(2) 1 02+V(1) [*]*
   24            53+4*V(2)                   -3  1 (1)F> 012+V(2) 1 02+V(1) [*]*
   25            65+5*V(2)               9+V(2)  113+V(2) (1)F> 1 02+V(1) [*]*
   26            68+5*V(2)              10+V(2)  113+V(2) 0 (1)B> 02+V(1) [*]*
   27            70+5*V(2)               8+V(2)  113+V(2) 0 <C(0) 1 01+V(1) [*]*
   28            71+5*V(2)               7+V(2)  113+V(2) <D(0) 0 1 01+V(1) [*]*
   29            72+5*V(2)               6+V(2)  112+V(2) <D(1) 02 1 01+V(1) [*]*
   30            84+6*V(2)                   -6  <D(1) 112+V(2) 02 1 01+V(1) [*]*
   31            87+6*V(2)                   -7  <E(0) 0 112+V(2) 02 1 01+V(1) [*]*
<< Success! ==> defined new CTR 12 (PPA)
792903           9703813827              -176215  <E(0) 0 1176207 02 1 06 1
== Executing  PA-CTR  2, V(1)=176203, V(2)=0, repcount=58735, factor=5/3
1321518          26953578507              -293685  <E(0) 0293676 12 02 1 06 1
== Executing PPA-CTR 12 (once), V(1)=2, V(2)=293675
1321549          26955340644              -293692  <E(0) 0 1293687 02 1 03 1
== Executing  PA-CTR  2, V(1)=293683, V(2)=0, repcount=97895, factor=5/3
2202604          74873768404              -489482  <E(0) 0489476 12 02 1 03 1
2202605          74873768405              -489483  <F(0) 0489477 12 02 1 03 1
2202606          74873768407              -489481  1 (1)F> 0489477 12 02 1 03 1
2202607          74874257884                   -4  1489478 (1)F> 12 02 1 03 1
2202608          74874257887                   -3  1489478 0 (1)B> 1 02 1 03 1
2202609          74874257888                   -2  1489478 0 1 (0)A> 02 1 03 1
2202610          74874257889                   -1  1489478 0 1 0 (1)B> 0 1 03 1
2202611          74874257891                   -3  1489478 0 1 0 <C(0) 12 03 1
2202612          74874257892                   -4  1489478 0 1 <D(0) 0 12 03 1
2202613          74874257893                   -5  1489478 0 <D(1) 02 12 03 1
2202614          74874257896                   -6  1489478 <E(0) 03 12 03 1
2202615          74874747374              -489484  <E(0) 0489481 12 03 1
2202616          74874747375              -489485  <F(0) 0489482 12 03 1
2202617          74874747377              -489483  1 (1)F> 0489482 12 03 1
2202618          74875236859                   -1  1489483 (1)F> 12 03 1
2202619          74875236862                    0  1489483 0 (1)B> 1 03 1
2202620          74875236863                    1  1489483 0 1 (0)A> 03 1
2202621          74875236864                    2  1489483 0 1 0 (1)B> 02 1
2202622          74875236866                    0  1489483 0 1 0 <C(0) 1 0 1
2202623          74875236867                   -1  1489483 0 1 <D(0) 0 1 0 1
2202624          74875236868                   -2  1489483 0 <D(1) 02 1 0 1
2202625          74875236871                   -3  1489483 <E(0) 03 1 0 1
2202626          74875726354              -489486  <E(0) 0489486 1 0 1
2202627          74875726355              -489487  <F(0) 0489487 1 0 1
2202628          74875726357              -489485  1 (1)F> 0489487 1 0 1
2202629          74876215844                    2  1489488 (1)F> 1 0 1
2202630          74876215847                    3  1489488 0 (1)B> 0 1
2202631          74876215849                    1  1489488 0 <C(0) 12
2202632          74876215850                    0  1489488 <D(0) 0 12
2202633          74876215851                   -1  1489487 <D(1) 02 12
2202634          74876705338              -489488  <D(1) 1489487 02 12
2202635          74876705341              -489489  <E(0) 0 1489487 02 12
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  <E(0) 01+V(2) 12 02 1 03 11+V(1)
    1                    1                   -1  <F(0) 02+V(2) 12 02 1 03 11+V(1)
    2                    3                    1  1 (1)F> 02+V(2) 12 02 1 03 11+V(1)
    3               5+V(2)               3+V(2)  13+V(2) (1)F> 12 02 1 03 11+V(1)
    4               8+V(2)               4+V(2)  13+V(2) 0 (1)B> 1 02 1 03 11+V(1)
    5               9+V(2)               5+V(2)  13+V(2) 0 1 (0)A> 02 1 03 11+V(1)
    6              10+V(2)               6+V(2)  13+V(2) 0 1 0 (1)B> 0 1 03 11+V(1)
    7              12+V(2)               4+V(2)  13+V(2) 0 1 0 <C(0) 12 03 11+V(1)
    8              13+V(2)               3+V(2)  13+V(2) 0 1 <D(0) 0 12 03 11+V(1)
    9              14+V(2)               2+V(2)  13+V(2) 0 <D(1) 02 12 03 11+V(1)
   10              17+V(2)               1+V(2)  13+V(2) <E(0) 03 12 03 11+V(1)
   11            20+2*V(2)                   -2  <E(0) 06+V(2) 12 03 11+V(1)
   12            21+2*V(2)                   -3  <F(0) 07+V(2) 12 03 11+V(1)
   13            23+2*V(2)                   -1  1 (1)F> 07+V(2) 12 03 11+V(1)
   14            30+3*V(2)               6+V(2)  18+V(2) (1)F> 12 03 11+V(1)
   15            33+3*V(2)               7+V(2)  18+V(2) 0 (1)B> 1 03 11+V(1)
   16            34+3*V(2)               8+V(2)  18+V(2) 0 1 (0)A> 03 11+V(1)
   17            35+3*V(2)               9+V(2)  18+V(2) 0 1 0 (1)B> 02 11+V(1)
   18            37+3*V(2)               7+V(2)  18+V(2) 0 1 0 <C(0) 1 0 11+V(1)
   19            38+3*V(2)               6+V(2)  18+V(2) 0 1 <D(0) 0 1 0 11+V(1)
   20            39+3*V(2)               5+V(2)  18+V(2) 0 <D(1) 02 1 0 11+V(1)
   21            42+3*V(2)               4+V(2)  18+V(2) <E(0) 03 1 0 11+V(1)
   22            50+4*V(2)                   -4  <E(0) 011+V(2) 1 0 11+V(1)
   23            51+4*V(2)                   -5  <F(0) 012+V(2) 1 0 11+V(1)
   24            53+4*V(2)                   -3  1 (1)F> 012+V(2) 1 0 11+V(1)
   25            65+5*V(2)               9+V(2)  113+V(2) (1)F> 1 0 11+V(1)
   26            68+5*V(2)              10+V(2)  113+V(2) 0 (1)B> 0 11+V(1)
   27            70+5*V(2)               8+V(2)  113+V(2) 0 <C(0) 12+V(1)
   28            71+5*V(2)               7+V(2)  113+V(2) <D(0) 0 12+V(1)
   29            72+5*V(2)               6+V(2)  112+V(2) <D(1) 02 12+V(1)
   30            84+6*V(2)                   -6  <D(1) 112+V(2) 02 12+V(1)
   31            87+6*V(2)                   -7  <E(0) 0 112+V(2) 02 12+V(1)
<< Success! ==> defined new CTR 13 (PPA)
2202635          74876705341              -489489  <E(0) 0 1489487 02 12
== Executing  PA-CTR  1, V(1)=489483, V(2)=0, repcount=163162, factor=5/3
3671093         207988017667              -815813  <E(0) 0815811 1 02 12
== Executing PPA-CTR  8 (once), V(1)=0, V(2)=815808
3671102         207989649304              -815816  <E(0) 0 1815812 02 1 0 12
== Executing  PA-CTR  2, V(1)=815808, V(2)=0, repcount=271937, factor=5/3
6118535         577741844330             -1359690  <E(0) 01359686 1 02 1 0 12
== Executing PPA-CTR  9 (once), V(1)=0, V(2)=1359683
6118544         577744563717             -1359693  <E(0) 0 11359687 02 1 0 1 0 12
== Executing  PA-CTR  3, V(1)=1359683, V(2)=0, repcount=453228, factor=5/3
10197596        1604828555601             -2266149  <E(0) 02266141 13 02 1 0 1 0 12
== Executing PPA-CTR  4 (once), V(1)=0, V(2)=1, V(3)=2266140
10197614        1604837620210             -2266154  <E(0) 0 12266149 02 12 0 12
== Executing  PA-CTR  2, V(1)=2266145, V(2)=0, repcount=755382, factor=5/3
16996052        4457857269796             -3776918  <E(0) 03776911 13 02 12 0 12
== Executing PPA-CTR  5 (once), V(1)=1, V(2)=3776910
16996080        4457872377497             -3776923  <E(0) 0 13776917 02 1
== Executing  PA-CTR  1, V(1)=3776913, V(2)=0, repcount=1258972, factor=5/3
28326828       12382941228053             -6294867  <E(0) 06294861 1 02 1
== Executing PPA-CTR  8 (once), V(1)=0, V(2)=6294858
28326837       12382953817790             -6294870  <E(0) 0 16294862 02 1 0 1
== Executing  PA-CTR  2, V(1)=6294858, V(2)=0, repcount=2098287, factor=5/3
47211420       34397022767366            -10491444  <E(0) 010491436 1 02 1 0 1
== Executing PPA-CTR  9 (once), V(1)=0, V(2)=10491433
47211429       34397043750253            -10491447  <E(0) 0 110491437 02 1 0 1 0 1
== Executing  PA-CTR  3, V(1)=10491433, V(2)=0, repcount=3497145, factor=5/3
78685734       95547204968263            -17485737  <E(0) 017485726 12 02 1 0 1 0 1
78685735       95547204968264            -17485738  <F(0) 017485727 12 02 1 0 1 0 1
78685736       95547204968266            -17485736  1 (1)F> 017485727 12 02 1 0 1 0 1
78685737       95547222453993                   -9  117485728 (1)F> 12 02 1 0 1 0 1
78685738       95547222453996                   -8  117485728 0 (1)B> 1 02 1 0 1 0 1
78685739       95547222453997                   -7  117485728 0 1 (0)A> 02 1 0 1 0 1
78685740       95547222453998                   -6  117485728 0 1 0 (1)B> 0 1 0 1 0 1
78685741       95547222454000                   -8  117485728 0 1 0 <C(0) 12 0 1 0 1
78685742       95547222454001                   -9  117485728 0 1 <D(0) 0 12 0 1 0 1
78685743       95547222454002                  -10  117485728 0 <D(1) 02 12 0 1 0 1
78685744       95547222454005                  -11  117485728 <E(0) 03 12 0 1 0 1
78685745       95547239939733            -17485739  <E(0) 017485731 12 0 1 0 1
78685746       95547239939734            -17485740  <F(0) 017485732 12 0 1 0 1
78685747       95547239939736            -17485738  1 (1)F> 017485732 12 0 1 0 1
78685748       95547257425468                   -6  117485733 (1)F> 12 0 1 0 1
78685749       95547257425471                   -5  117485733 0 (1)B> 1 0 1 0 1
78685750       95547257425472                   -4  117485733 0 1 (0)A> 0 1 0 1
78685751       95547257425473                   -3  117485733 0 1 0 (1)B> 1 0 1
78685752       95547257425474                   -2  117485733 0 1 0 1 (0)A> 0 1
78685753       95547257425475                   -1  117485733 0 1 0 1 0 (1)B> 1
78685754       95547257425476                    0  117485733 0 1 0 1 0 1 (0)A>
78685755       95547257425477                    1  117485733 0 1 0 1 0 1 0 (1)B>
78685756       95547257425479                   -1  117485733 0 1 0 1 0 1 0 <C(0) 1
78685757       95547257425480                   -2  117485733 0 1 0 1 0 1 <D(0) 0 1
78685758       95547257425481                   -3  117485733 0 1 0 1 0 <D(1) 02 1
78685759       95547257425484                   -4  117485733 0 1 0 1 <E(0) 03 1
78685760       95547257425485                   -5  117485733 0 1 0 <E(0) 04 1
78685761       95547257425486                   -6  117485733 0 1 <F(0) 05 1
78685762       95547257425487                   -7  117485733 0 <B(0) 06 1
78685763       95547257425488                   -8  117485733 <A(1) 07 1
78685764       95547257425489                   -9  117485732 <C(0) 1 07 1
78685765       95547257425490                   -8  117485731 1 Z> 0 1 07 1   [stop]

Lines:       364
Top steps:   363
Macro steps: 78685765
Basic steps: 95547257425490
Tape index:  -8
ones:        17485734
log10(ones    ):    7.243
log10(steps   ):   13.980
Run state:   stop

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
    L 60
    5T B1R C0L A1L A0R D0L Z1R E1R D1L F0L E0L F1R B0L : 17485734 95547257425490
    T 6-state TM #a from MaBu-List
    M	650
    pref	sim
    machv mbL6_a  	just simple
    machv mbL6_a-r	with repetitions reduced
    machv mbL6_a-1	with tape symbol exponents
    machv mbL6_a-m	as 1-bck-macro machine
    machv mbL6_a-a	as 1-bck-macro machine with pure additive config-TRs
    iam	mbL6_a-a
    mtype	1 0
    mmtyp	3
    r	1
    H	1
    mac	0
    E	2
    sympr	
    HM	1
    date	Tue Jul  6 22:10:37 CEST 2010
    edate	Tue Jul  6 22:10:39 CEST 2010
    bnspeed	1

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