2-state 6-symbol #d (T.J. & S. Ligocki)

Comment: This TM produces >1.9x10^27 nonzeros in >2.3x10^54 steps.

State on
0
on
1
on
2
on
3
on
4
on
5
on 0 on 1 on 2 on 3 on 4 on 5
Print Move Goto Print Move Goto Print Move Goto Print Move Goto Print Move Goto Print Move Goto
A 1RB 0RB 3LA 5LA 1RH 4LB 1 right B 0 right B 3 left A 5 left A 1 right H 4 left B
B 1LA 2RB 3LA 4LB 3RB 3RA 1 left A 2 right B 3 left A 4 left B 3 right B 3 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-macro machine.
Simulation is done as 1-macro machine with pure additive config-TRs.

Pushing initial machine.
Pushing macro factor 1.

Steps             BasSteps              BasTpos  Tape contents
    0                    0                    0  A>
    1                    1                    1  1 B>
    2                    2                    0  1 <A 1
    3                    3                    1  B> 1
    4                    4                    2  2 B>
    5                    5                    1  2 <A 1
    6                    6                    0  <A 3 1
    7                    7                    1  1 B> 3 1
    8                    8                    0  1 <B 4 1
    9                    9                    1  2 B> 4 1
   10                   10                    2  2 3 B> 1
   11                   11                    3  2 3 2 B>
   12                   12                    2  2 3 2 <A 1
   13                   13                    1  2 3 <A 3 1
   14                   14                    0  2 <A 5 3 1
   15                   15                   -1  <A 3 5 3 1
   16                   16                    0  1 B> 3 5 3 1
   17                   17                   -1  1 <B 4 5 3 1
   18                   18                    0  2 B> 4 5 3 1
   19                   19                    1  2 3 B> 5 3 1
   20                   20                    2  2 32 A> 3 1
   21                   21                    1  2 32 <A 5 1
   22                   23                   -1  2 <A 53 1
   23                   24                   -2  <A 3 53 1
   24                   25                   -1  1 B> 3 53 1
   25                   26                   -2  1 <B 4 53 1
   26                   27                   -1  2 B> 4 53 1
   27                   28                    0  2 3 B> 53 1
   28                   29                    1  2 32 A> 52 1
   29                   30                    0  2 32 <B 4 5 1
   30                   32                   -2  2 <B 43 5 1
   31                   33                   -3  <A 3 43 5 1
   32                   34                   -2  1 B> 3 43 5 1
   33                   35                   -3  1 <B 44 5 1
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  1 <B 41+V(2) 53+V(1) [*]*
    1                    1                    1  2 B> 41+V(2) 53+V(1) [*]*
    2               2+V(2)               2+V(2)  2 31+V(2) B> 53+V(1) [*]*
    3               3+V(2)               3+V(2)  2 32+V(2) A> 52+V(1) [*]*
    4               4+V(2)               2+V(2)  2 32+V(2) <B 4 51+V(1) [*]*
    5             6+2*V(2)                    0  2 <B 43+V(2) 51+V(1) [*]*
    6             7+2*V(2)                   -1  <A 3 43+V(2) 51+V(1) [*]*
    7             8+2*V(2)                    0  1 B> 3 43+V(2) 51+V(1) [*]*
    8             9+2*V(2)                   -1  1 <B 44+V(2) 51+V(1) [*]*
<< Success! ==> defined new CTR 1 (PA)
   34                   36                   -2  2 B> 44 5 1
   35                   40                    2  2 34 B> 5 1
   36                   41                    3  2 35 A> 1
   37                   42                    4  2 35 0 B>
   38                   43                    3  2 35 0 <A 1
   39                   44                    4  2 35 1 B> 1
   40                   45                    5  2 35 1 2 B>
   41                   46                    4  2 35 1 2 <A 1
   42                   47                    3  2 35 1 <A 3 1
   43                   48                    4  2 35 0 B> 3 1
   44                   49                    3  2 35 0 <B 4 1
   45                   50                    2  2 35 <A 1 4 1
   46                   55                   -3  2 <A 55 1 4 1
   47                   56                   -4  <A 3 55 1 4 1
   48                   57                   -3  1 B> 3 55 1 4 1
   49                   58                   -4  1 <B 4 55 1 4 1
   50                   59                   -3  2 B> 4 55 1 4 1
   51                   60                   -2  2 3 B> 55 1 4 1
   52                   61                   -1  2 32 A> 54 1 4 1
   53                   62                   -2  2 32 <B 4 53 1 4 1
   54                   64                   -4  2 <B 43 53 1 4 1
   55                   65                   -5  <A 3 43 53 1 4 1
   56                   66                   -4  1 B> 3 43 53 1 4 1
   57                   67                   -5  1 <B 44 53 1 4 1
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  1 <B 41+V(2) 53+V(1) [*]* [*]* [*]*
    1                    1                    1  2 B> 41+V(2) 53+V(1) [*]* [*]* [*]*
    2               2+V(2)               2+V(2)  2 31+V(2) B> 53+V(1) [*]* [*]* [*]*
    3               3+V(2)               3+V(2)  2 32+V(2) A> 52+V(1) [*]* [*]* [*]*
    4               4+V(2)               2+V(2)  2 32+V(2) <B 4 51+V(1) [*]* [*]* [*]*
    5             6+2*V(2)                    0  2 <B 43+V(2) 51+V(1) [*]* [*]* [*]*
    6             7+2*V(2)                   -1  <A 3 43+V(2) 51+V(1) [*]* [*]* [*]*
    7             8+2*V(2)                    0  1 B> 3 43+V(2) 51+V(1) [*]* [*]* [*]*
    8             9+2*V(2)                   -1  1 <B 44+V(2) 51+V(1) [*]* [*]* [*]*
<< Success! ==> defined new CTR 2 (PA)
   57                   67                   -5  1 <B 44 53 1 4 1
== Executing  PA-CTR  2, V(1)=0, V(2)=3, repcount=1, factor=3/2
   65                   82                   -6  1 <B 47 5 1 4 1
   66                   83                   -5  2 B> 47 5 1 4 1
   67                   90                    2  2 37 B> 5 1 4 1
   68                   91                    3  2 38 A> 1 4 1
   69                   92                    4  2 38 0 B> 4 1
   70                   93                    5  2 38 0 3 B> 1
   71                   94                    6  2 38 0 3 2 B>
   72                   95                    5  2 38 0 3 2 <A 1
   73                   96                    4  2 38 0 3 <A 3 1
   74                   97                    3  2 38 0 <A 5 3 1
   75                   98                    4  2 38 1 B> 5 3 1
   76                   99                    5  2 38 1 3 A> 3 1
   77                  100                    4  2 38 1 3 <A 5 1
   78                  101                    3  2 38 1 <A 52 1
   79                  102                    4  2 38 0 B> 52 1
   80                  103                    5  2 38 0 3 A> 5 1
   81                  104                    4  2 38 0 3 <B 4 1
   82                  105                    3  2 38 0 <B 42 1
   83                  106                    2  2 38 <A 1 42 1
   84                  114                   -6  2 <A 58 1 42 1
   85                  115                   -7  <A 3 58 1 42 1
   86                  116                   -6  1 B> 3 58 1 42 1
   87                  117                   -7  1 <B 4 58 1 42 1
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  1 <B 42+V(1) 5 1 4 1
    1                    1                    1  2 B> 42+V(1) 5 1 4 1
    2               3+V(1)               3+V(1)  2 32+V(1) B> 5 1 4 1
    3               4+V(1)               4+V(1)  2 33+V(1) A> 1 4 1
    4               5+V(1)               5+V(1)  2 33+V(1) 0 B> 4 1
    5               6+V(1)               6+V(1)  2 33+V(1) 0 3 B> 1
    6               7+V(1)               7+V(1)  2 33+V(1) 0 3 2 B>
    7               8+V(1)               6+V(1)  2 33+V(1) 0 3 2 <A 1
    8               9+V(1)               5+V(1)  2 33+V(1) 0 3 <A 3 1
    9              10+V(1)               4+V(1)  2 33+V(1) 0 <A 5 3 1
   10              11+V(1)               5+V(1)  2 33+V(1) 1 B> 5 3 1
   11              12+V(1)               6+V(1)  2 33+V(1) 1 3 A> 3 1
   12              13+V(1)               5+V(1)  2 33+V(1) 1 3 <A 5 1
   13              14+V(1)               4+V(1)  2 33+V(1) 1 <A 52 1
   14              15+V(1)               5+V(1)  2 33+V(1) 0 B> 52 1
   15              16+V(1)               6+V(1)  2 33+V(1) 0 3 A> 5 1
   16              17+V(1)               5+V(1)  2 33+V(1) 0 3 <B 4 1
   17              18+V(1)               4+V(1)  2 33+V(1) 0 <B 42 1
   18              19+V(1)               3+V(1)  2 33+V(1) <A 1 42 1
   19            22+2*V(1)                    0  2 <A 53+V(1) 1 42 1
   20            23+2*V(1)                   -1  <A 3 53+V(1) 1 42 1
   21            24+2*V(1)                    0  1 B> 3 53+V(1) 1 42 1
   22            25+2*V(1)                   -1  1 <B 4 53+V(1) 1 42 1
<< Success! ==> defined new CTR 3 (PPA)
   87                  117                   -7  1 <B 4 58 1 42 1
== Executing  PA-CTR  2, V(1)=5, V(2)=0, repcount=3, factor=3/2
  111                  162                  -10  1 <B 410 52 1 42 1
  112                  163                   -9  2 B> 410 52 1 42 1
  113                  173                    1  2 310 B> 52 1 42 1
  114                  174                    2  2 311 A> 5 1 42 1
  115                  175                    1  2 311 <B 4 1 42 1
  116                  186                  -10  2 <B 412 1 42 1
  117                  187                  -11  <A 3 412 1 42 1
  118                  188                  -10  1 B> 3 412 1 42 1
  119                  189                  -11  1 <B 413 1 42 1
  120                  190                  -10  2 B> 413 1 42 1
  121                  203                    3  2 313 B> 1 42 1
  122                  204                    4  2 313 2 B> 42 1
  123                  206                    6  2 313 2 32 B> 1
  124                  207                    7  2 313 2 32 2 B>
  125                  208                    6  2 313 2 32 2 <A 1
  126                  209                    5  2 313 2 32 <A 3 1
  127                  211                    3  2 313 2 <A 52 3 1
  128                  212                    2  2 313 <A 3 52 3 1
  129                  225                  -11  2 <A 513 3 52 3 1
  130                  226                  -12  <A 3 513 3 52 3 1
  131                  227                  -11  1 B> 3 513 3 52 3 1
  132                  228                  -12  1 <B 4 513 3 52 3 1
  133                  229                  -11  2 B> 4 513 3 52 3 1
  134                  230                  -10  2 3 B> 513 3 52 3 1
  135                  231                   -9  2 32 A> 512 3 52 3 1
  136                  232                  -10  2 32 <B 4 511 3 52 3 1
  137                  234                  -12  2 <B 43 511 3 52 3 1
  138                  235                  -13  <A 3 43 511 3 52 3 1
  139                  236                  -12  1 B> 3 43 511 3 52 3 1
  140                  237                  -13  1 <B 44 511 3 52 3 1
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  1 <B 41+V(2) 53+V(1) [*]* [*]* [*]* [*]*
    1                    1                    1  2 B> 41+V(2) 53+V(1) [*]* [*]* [*]* [*]*
    2               2+V(2)               2+V(2)  2 31+V(2) B> 53+V(1) [*]* [*]* [*]* [*]*
    3               3+V(2)               3+V(2)  2 32+V(2) A> 52+V(1) [*]* [*]* [*]* [*]*
    4               4+V(2)               2+V(2)  2 32+V(2) <B 4 51+V(1) [*]* [*]* [*]* [*]*
    5             6+2*V(2)                    0  2 <B 43+V(2) 51+V(1) [*]* [*]* [*]* [*]*
    6             7+2*V(2)                   -1  <A 3 43+V(2) 51+V(1) [*]* [*]* [*]* [*]*
    7             8+2*V(2)                    0  1 B> 3 43+V(2) 51+V(1) [*]* [*]* [*]* [*]*
    8             9+2*V(2)                   -1  1 <B 44+V(2) 51+V(1) [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 4 (PA)
  140                  237                  -13  1 <B 44 511 3 52 3 1
== Executing  PA-CTR  4, V(1)=8, V(2)=3, repcount=5, factor=3/2
  180                  372                  -18  1 <B 419 5 3 52 3 1
  181                  373                  -17  2 B> 419 5 3 52 3 1
  182                  392                    2  2 319 B> 5 3 52 3 1
  183                  393                    3  2 320 A> 3 52 3 1
  184                  394                    2  2 320 <A 53 3 1
  185                  414                  -18  2 <A 523 3 1
  186                  415                  -19  <A 3 523 3 1
  187                  416                  -18  1 B> 3 523 3 1
  188                  417                  -19  1 <B 4 523 3 1
  189                  418                  -18  2 B> 4 523 3 1
  190                  419                  -17  2 3 B> 523 3 1
  191                  420                  -16  2 32 A> 522 3 1
  192                  421                  -17  2 32 <B 4 521 3 1
  193                  423                  -19  2 <B 43 521 3 1
  194                  424                  -20  <A 3 43 521 3 1
  195                  425                  -19  1 B> 3 43 521 3 1
  196                  426                  -20  1 <B 44 521 3 1
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  1 <B 41+V(2) 53+V(1) [*]* [*]*
    1                    1                    1  2 B> 41+V(2) 53+V(1) [*]* [*]*
    2               2+V(2)               2+V(2)  2 31+V(2) B> 53+V(1) [*]* [*]*
    3               3+V(2)               3+V(2)  2 32+V(2) A> 52+V(1) [*]* [*]*
    4               4+V(2)               2+V(2)  2 32+V(2) <B 4 51+V(1) [*]* [*]*
    5             6+2*V(2)                    0  2 <B 43+V(2) 51+V(1) [*]* [*]*
    6             7+2*V(2)                   -1  <A 3 43+V(2) 51+V(1) [*]* [*]*
    7             8+2*V(2)                    0  1 B> 3 43+V(2) 51+V(1) [*]* [*]*
    8             9+2*V(2)                   -1  1 <B 44+V(2) 51+V(1) [*]* [*]*
<< Success! ==> defined new CTR 5 (PA)
  196                  426                  -20  1 <B 44 521 3 1
== Executing  PA-CTR  5, V(1)=18, V(2)=3, repcount=10, factor=3/2
  276                  846                  -30  1 <B 434 5 3 1
  277                  847                  -29  2 B> 434 5 3 1
  278                  881                    5  2 334 B> 5 3 1
  279                  882                    6  2 335 A> 3 1
  280                  883                    5  2 335 <A 5 1
  281                  918                  -30  2 <A 536 1
  282                  919                  -31  <A 3 536 1
  283                  920                  -30  1 B> 3 536 1
  284                  921                  -31  1 <B 4 536 1
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  1 <B 41+V(1) 5 3 [*]*
    1                    1                    1  2 B> 41+V(1) 5 3 [*]*
    2               2+V(1)               2+V(1)  2 31+V(1) B> 5 3 [*]*
    3               3+V(1)               3+V(1)  2 32+V(1) A> 3 [*]*
    4               4+V(1)               2+V(1)  2 32+V(1) <A 5 [*]*
    5             6+2*V(1)                    0  2 <A 53+V(1) [*]*
    6             7+2*V(1)                   -1  <A 3 53+V(1) [*]*
    7             8+2*V(1)                    0  1 B> 3 53+V(1) [*]*
    8             9+2*V(1)                   -1  1 <B 4 53+V(1) [*]*
<< Success! ==> defined new CTR 6 (PPA)
  284                  921                  -31  1 <B 4 536 1
== Executing  PA-CTR  1, V(1)=33, V(2)=0, repcount=17, factor=3/2
  420                 1890                  -48  1 <B 452 52 1
  421                 1891                  -47  2 B> 452 52 1
  422                 1943                    5  2 352 B> 52 1
  423                 1944                    6  2 353 A> 5 1
  424                 1945                    5  2 353 <B 4 1
  425                 1998                  -48  2 <B 454 1
  426                 1999                  -49  <A 3 454 1
  427                 2000                  -48  1 B> 3 454 1
  428                 2001                  -49  1 <B 455 1
  429                 2002                  -48  2 B> 455 1
  430                 2057                    7  2 355 B> 1
  431                 2058                    8  2 355 2 B>
  432                 2059                    7  2 355 2 <A 1
  433                 2060                    6  2 355 <A 3 1
  434                 2115                  -49  2 <A 555 3 1
  435                 2116                  -50  <A 3 555 3 1
  436                 2117                  -49  1 B> 3 555 3 1
  437                 2118                  -50  1 <B 4 555 3 1
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  1 <B 41+V(2) 52 11+V(1)
    1                    1                    1  2 B> 41+V(2) 52 11+V(1)
    2               2+V(2)               2+V(2)  2 31+V(2) B> 52 11+V(1)
    3               3+V(2)               3+V(2)  2 32+V(2) A> 5 11+V(1)
    4               4+V(2)               2+V(2)  2 32+V(2) <B 4 11+V(1)
    5             6+2*V(2)                    0  2 <B 43+V(2) 11+V(1)
    6             7+2*V(2)                   -1  <A 3 43+V(2) 11+V(1)
    7             8+2*V(2)                    0  1 B> 3 43+V(2) 11+V(1)
    8             9+2*V(2)                   -1  1 <B 44+V(2) 11+V(1)
    9            10+2*V(2)                    0  2 B> 44+V(2) 11+V(1)
   10            14+3*V(2)               4+V(2)  2 34+V(2) B> 11+V(1)
   11       15+V(1)+3*V(2)          5+V(1)+V(2)  2 34+V(2) 21+V(1) B>
   12       16+V(1)+3*V(2)          4+V(1)+V(2)  2 34+V(2) 21+V(1) <A 1
   13     17+2*V(1)+3*V(2)               3+V(2)  2 34+V(2) <A 31+V(1) 1
   14     21+2*V(1)+4*V(2)                   -1  2 <A 54+V(2) 31+V(1) 1
   15     22+2*V(1)+4*V(2)                   -2  <A 3 54+V(2) 31+V(1) 1
   16     23+2*V(1)+4*V(2)                   -1  1 B> 3 54+V(2) 31+V(1) 1
   17     24+2*V(1)+4*V(2)                   -2  1 <B 4 54+V(2) 31+V(1) 1
<< Success! ==> defined new CTR 7 (PPA)
  437                 2118                  -50  1 <B 4 555 3 1
== Executing  PA-CTR  5, V(1)=52, V(2)=0, repcount=27, factor=3/2
  653                 4467                  -77  1 <B 482 5 3 1
== Executing PPA-CTR  6 (once), V(1)=81
  661                 4638                  -78  1 <B 4 584 1
== Executing  PA-CTR  1, V(1)=81, V(2)=0, repcount=41, factor=3/2
  989                 9927                 -119  1 <B 4124 52 1
== Executing PPA-CTR  7 (once), V(1)=0, V(2)=123
 1006                10443                 -121  1 <B 4 5127 3 1
== Executing  PA-CTR  5, V(1)=124, V(2)=0, repcount=63, factor=3/2
 1510                22728                 -184  1 <B 4190 5 3 1
== Executing PPA-CTR  6 (once), V(1)=189
 1518                23115                 -185  1 <B 4 5192 1
== Executing  PA-CTR  1, V(1)=189, V(2)=0, repcount=95, factor=3/2
 2278                50760                 -280  1 <B 4286 52 1
== Executing PPA-CTR  7 (once), V(1)=0, V(2)=285
 2295                51924                 -282  1 <B 4 5289 3 1
== Executing  PA-CTR  5, V(1)=286, V(2)=0, repcount=144, factor=3/2
 3447               114996                 -426  1 <B 4433 5 3 1
== Executing PPA-CTR  6 (once), V(1)=432
 3455               115869                 -427  1 <B 4 5435 1
== Executing  PA-CTR  1, V(1)=432, V(2)=0, repcount=217, factor=3/2
 5191               258438                 -644  1 <B 4652 5 1
 5192               258439                 -643  2 B> 4652 5 1
 5193               259091                    9  2 3652 B> 5 1
 5194               259092                   10  2 3653 A> 1
 5195               259093                   11  2 3653 0 B>
 5196               259094                   10  2 3653 0 <A 1
 5197               259095                   11  2 3653 1 B> 1
 5198               259096                   12  2 3653 1 2 B>
 5199               259097                   11  2 3653 1 2 <A 1
 5200               259098                   10  2 3653 1 <A 3 1
 5201               259099                   11  2 3653 0 B> 3 1
 5202               259100                   10  2 3653 0 <B 4 1
 5203               259101                    9  2 3653 <A 1 4 1
 5204               259754                 -644  2 <A 5653 1 4 1
 5205               259755                 -645  <A 3 5653 1 4 1
 5206               259756                 -644  1 B> 3 5653 1 4 1
 5207               259757                 -645  1 <B 4 5653 1 4 1
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  1 <B 42+V(1) 5 1
    1                    1                    1  2 B> 42+V(1) 5 1
    2               3+V(1)               3+V(1)  2 32+V(1) B> 5 1
    3               4+V(1)               4+V(1)  2 33+V(1) A> 1
    4               5+V(1)               5+V(1)  2 33+V(1) 0 B>
    5               6+V(1)               4+V(1)  2 33+V(1) 0 <A 1
    6               7+V(1)               5+V(1)  2 33+V(1) 1 B> 1
    7               8+V(1)               6+V(1)  2 33+V(1) 1 2 B>
    8               9+V(1)               5+V(1)  2 33+V(1) 1 2 <A 1
    9              10+V(1)               4+V(1)  2 33+V(1) 1 <A 3 1
   10              11+V(1)               5+V(1)  2 33+V(1) 0 B> 3 1
   11              12+V(1)               4+V(1)  2 33+V(1) 0 <B 4 1
   12              13+V(1)               3+V(1)  2 33+V(1) <A 1 4 1
   13            16+2*V(1)                    0  2 <A 53+V(1) 1 4 1
   14            17+2*V(1)                   -1  <A 3 53+V(1) 1 4 1
   15            18+2*V(1)                    0  1 B> 3 53+V(1) 1 4 1
   16            19+2*V(1)                   -1  1 <B 4 53+V(1) 1 4 1
<< Success! ==> defined new CTR 8 (PPA)
 5207               259757                 -645  1 <B 4 5653 1 4 1
== Executing  PA-CTR  2, V(1)=650, V(2)=0, repcount=326, factor=3/2
 7815               580541                 -971  1 <B 4979 5 1 4 1
== Executing PPA-CTR  3 (once), V(1)=977
 7837               582520                 -972  1 <B 4 5980 1 42 1
== Executing  PA-CTR  2, V(1)=977, V(2)=0, repcount=489, factor=3/2
11749              1302817                -1461  1 <B 41468 52 1 42 1
11750              1302818                -1460  2 B> 41468 52 1 42 1
11751              1304286                    8  2 31468 B> 52 1 42 1
11752              1304287                    9  2 31469 A> 5 1 42 1
11753              1304288                    8  2 31469 <B 4 1 42 1
11754              1305757                -1461  2 <B 41470 1 42 1
11755              1305758                -1462  <A 3 41470 1 42 1
11756              1305759                -1461  1 B> 3 41470 1 42 1
11757              1305760                -1462  1 <B 41471 1 42 1
11758              1305761                -1461  2 B> 41471 1 42 1
11759              1307232                   10  2 31471 B> 1 42 1
11760              1307233                   11  2 31471 2 B> 42 1
11761              1307235                   13  2 31471 2 32 B> 1
11762              1307236                   14  2 31471 2 32 2 B>
11763              1307237                   13  2 31471 2 32 2 <A 1
11764              1307238                   12  2 31471 2 32 <A 3 1
11765              1307240                   10  2 31471 2 <A 52 3 1
11766              1307241                    9  2 31471 <A 3 52 3 1
11767              1308712                -1462  2 <A 51471 3 52 3 1
11768              1308713                -1463  <A 3 51471 3 52 3 1
11769              1308714                -1462  1 B> 3 51471 3 52 3 1
11770              1308715                -1463  1 <B 4 51471 3 52 3 1
>> Try to prove a PPA-CTR with 4 Vars...
    0                    0                    0  1 <B 41+V(4) 52 11+V(3) 41+V(2) 11+V(1)
    1                    1                    1  2 B> 41+V(4) 52 11+V(3) 41+V(2) 11+V(1)
    2               2+V(4)               2+V(4)  2 31+V(4) B> 52 11+V(3) 41+V(2) 11+V(1)
    3               3+V(4)               3+V(4)  2 32+V(4) A> 5 11+V(3) 41+V(2) 11+V(1)
    4               4+V(4)               2+V(4)  2 32+V(4) <B 4 11+V(3) 41+V(2) 11+V(1)
    5             6+2*V(4)                    0  2 <B 43+V(4) 11+V(3) 41+V(2) 11+V(1)
    6             7+2*V(4)                   -1  <A 3 43+V(4) 11+V(3) 41+V(2) 11+V(1)
    7             8+2*V(4)                    0  1 B> 3 43+V(4) 11+V(3) 41+V(2) 11+V(1)
    8             9+2*V(4)                   -1  1 <B 44+V(4) 11+V(3) 41+V(2) 11+V(1)
    9            10+2*V(4)                    0  2 B> 44+V(4) 11+V(3) 41+V(2) 11+V(1)
   10            14+3*V(4)               4+V(4)  2 34+V(4) B> 11+V(3) 41+V(2) 11+V(1)
   11       15+V(3)+3*V(4)          5+V(3)+V(4)  2 34+V(4) 21+V(3) B> 41+V(2) 11+V(1)
   12  16+V(2)+V(3)+3*V(4)     6+V(2)+V(3)+V(4)  2 34+V(4) 21+V(3) 31+V(2) B> 11+V(1)
   13 17+V(1)+V(2)+V(3)+3*V(4) 7+V(1)+V(2)+V(3)+V(4)  2 34+V(4) 21+V(3) 31+V(2) 21+V(1) B>
   14 18+V(1)+V(2)+V(3)+3*V(4) 6+V(1)+V(2)+V(3)+V(4)  2 34+V(4) 21+V(3) 31+V(2) 21+V(1) <A 1
   15 19+2*V(1)+V(2)+V(3)+3*V(4)     5+V(2)+V(3)+V(4)  2 34+V(4) 21+V(3) 31+V(2) <A 31+V(1) 1
   16 20+2*V(1)+2*V(2)+V(3)+3*V(4)          4+V(3)+V(4)  2 34+V(4) 21+V(3) <A 51+V(2) 31+V(1) 1
   17 21+2*V(1)+2*V(2)+2*V(3)+3*V(4)               3+V(4)  2 34+V(4) <A 31+V(3) 51+V(2) 31+V(1) 1
   18 25+2*V(1)+2*V(2)+2*V(3)+4*V(4)                   -1  2 <A 54+V(4) 31+V(3) 51+V(2) 31+V(1) 1
   19 26+2*V(1)+2*V(2)+2*V(3)+4*V(4)                   -2  <A 3 54+V(4) 31+V(3) 51+V(2) 31+V(1) 1
   20 27+2*V(1)+2*V(2)+2*V(3)+4*V(4)                   -1  1 B> 3 54+V(4) 31+V(3) 51+V(2) 31+V(1) 1
   21 28+2*V(1)+2*V(2)+2*V(3)+4*V(4)                   -2  1 <B 4 54+V(4) 31+V(3) 51+V(2) 31+V(1) 1
<< Success! ==> defined new CTR 9 (PPA)
11770              1308715                -1463  1 <B 4 51471 3 52 3 1
== Executing  PA-CTR  4, V(1)=1468, V(2)=0, repcount=735, factor=3/2
17650              2933800                -2198  1 <B 42206 5 3 52 3 1
17651              2933801                -2197  2 B> 42206 5 3 52 3 1
17652              2936007                    9  2 32206 B> 5 3 52 3 1
17653              2936008                   10  2 32207 A> 3 52 3 1
17654              2936009                    9  2 32207 <A 53 3 1
17655              2938216                -2198  2 <A 52210 3 1
17656              2938217                -2199  <A 3 52210 3 1
17657              2938218                -2198  1 B> 3 52210 3 1
17658              2938219                -2199  1 <B 4 52210 3 1
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  1 <B 41+V(2) 5 3 51+V(1) [*]* [*]*
    1                    1                    1  2 B> 41+V(2) 5 3 51+V(1) [*]* [*]*
    2               2+V(2)               2+V(2)  2 31+V(2) B> 5 3 51+V(1) [*]* [*]*
    3               3+V(2)               3+V(2)  2 32+V(2) A> 3 51+V(1) [*]* [*]*
    4               4+V(2)               2+V(2)  2 32+V(2) <A 52+V(1) [*]* [*]*
    5             6+2*V(2)                    0  2 <A 54+V(1)+V(2) [*]* [*]*
    6             7+2*V(2)                   -1  <A 3 54+V(1)+V(2) [*]* [*]*
    7             8+2*V(2)                    0  1 B> 3 54+V(1)+V(2) [*]* [*]*
    8             9+2*V(2)                   -1  1 <B 4 54+V(1)+V(2) [*]* [*]*
<< Success! ==> defined new CTR 10 (PPA)
17658              2938219                -2199  1 <B 4 52210 3 1
== Executing  PA-CTR  5, V(1)=2207, V(2)=0, repcount=1104, factor=3/2
26490              6601291                -3303  1 <B 43313 52 3 1
26491              6601292                -3302  2 B> 43313 52 3 1
26492              6604605                   11  2 33313 B> 52 3 1
26493              6604606                   12  2 33314 A> 5 3 1
26494              6604607                   11  2 33314 <B 4 3 1
26495              6607921                -3303  2 <B 43315 3 1
26496              6607922                -3304  <A 3 43315 3 1
26497              6607923                -3303  1 B> 3 43315 3 1
26498              6607924                -3304  1 <B 43316 3 1
26499              6607925                -3303  2 B> 43316 3 1
26500              6611241                   13  2 33316 B> 3 1
26501              6611242                   12  2 33316 <B 4 1
26502              6614558                -3304  2 <B 43317 1
26503              6614559                -3305  <A 3 43317 1
26504              6614560                -3304  1 B> 3 43317 1
26505              6614561                -3305  1 <B 43318 1
26506              6614562                -3304  2 B> 43318 1
26507              6617880                   14  2 33318 B> 1
26508              6617881                   15  2 33318 2 B>
26509              6617882                   14  2 33318 2 <A 1
26510              6617883                   13  2 33318 <A 3 1
26511              6621201                -3305  2 <A 53318 3 1
26512              6621202                -3306  <A 3 53318 3 1
26513              6621203                -3305  1 B> 3 53318 3 1
26514              6621204                -3306  1 <B 4 53318 3 1
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  1 <B 41+V(2) 52 3 11+V(1)
    1                    1                    1  2 B> 41+V(2) 52 3 11+V(1)
    2               2+V(2)               2+V(2)  2 31+V(2) B> 52 3 11+V(1)
    3               3+V(2)               3+V(2)  2 32+V(2) A> 5 3 11+V(1)
    4               4+V(2)               2+V(2)  2 32+V(2) <B 4 3 11+V(1)
    5             6+2*V(2)                    0  2 <B 43+V(2) 3 11+V(1)
    6             7+2*V(2)                   -1  <A 3 43+V(2) 3 11+V(1)
    7             8+2*V(2)                    0  1 B> 3 43+V(2) 3 11+V(1)
    8             9+2*V(2)                   -1  1 <B 44+V(2) 3 11+V(1)
    9            10+2*V(2)                    0  2 B> 44+V(2) 3 11+V(1)
   10            14+3*V(2)               4+V(2)  2 34+V(2) B> 3 11+V(1)
   11            15+3*V(2)               3+V(2)  2 34+V(2) <B 4 11+V(1)
   12            19+4*V(2)                   -1  2 <B 45+V(2) 11+V(1)
   13            20+4*V(2)                   -2  <A 3 45+V(2) 11+V(1)
   14            21+4*V(2)                   -1  1 B> 3 45+V(2) 11+V(1)
   15            22+4*V(2)                   -2  1 <B 46+V(2) 11+V(1)
   16            23+4*V(2)                   -1  2 B> 46+V(2) 11+V(1)
   17            29+5*V(2)               5+V(2)  2 36+V(2) B> 11+V(1)
   18       30+V(1)+5*V(2)          6+V(1)+V(2)  2 36+V(2) 21+V(1) B>
   19       31+V(1)+5*V(2)          5+V(1)+V(2)  2 36+V(2) 21+V(1) <A 1
   20     32+2*V(1)+5*V(2)               4+V(2)  2 36+V(2) <A 31+V(1) 1
   21     38+2*V(1)+6*V(2)                   -2  2 <A 56+V(2) 31+V(1) 1
   22     39+2*V(1)+6*V(2)                   -3  <A 3 56+V(2) 31+V(1) 1
   23     40+2*V(1)+6*V(2)                   -2  1 B> 3 56+V(2) 31+V(1) 1
   24     41+2*V(1)+6*V(2)                   -3  1 <B 4 56+V(2) 31+V(1) 1
<< Success! ==> defined new CTR 11 (PPA)
26514              6621204                -3306  1 <B 4 53318 3 1
== Executing  PA-CTR  5, V(1)=3315, V(2)=0, repcount=1658, factor=3/2
39778             14878044                -4964  1 <B 44975 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=4974
39802             14907929                -4967  1 <B 4 54980 3 1
== Executing  PA-CTR  5, V(1)=4977, V(2)=0, repcount=2489, factor=3/2
59714             33508226                -7456  1 <B 47468 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=7467
59738             33553069                -7459  1 <B 4 57473 3 1
== Executing  PA-CTR  5, V(1)=7470, V(2)=0, repcount=3736, factor=3/2
89626             75448573               -11195  1 <B 411209 5 3 1
== Executing PPA-CTR  6 (once), V(1)=11208
89634             75470998               -11196  1 <B 4 511211 1
== Executing  PA-CTR  1, V(1)=11208, V(2)=0, repcount=5605, factor=3/2
134474            169752703               -16801  1 <B 416816 5 1
== Executing PPA-CTR  8 (once), V(1)=16814
134490            169786350               -16802  1 <B 4 516817 1 4 1
== Executing  PA-CTR  2, V(1)=16814, V(2)=0, repcount=8408, factor=3/2
201754            381920190               -25210  1 <B 425225 5 1 4 1
== Executing PPA-CTR  3 (once), V(1)=25223
201776            381970661               -25211  1 <B 4 525226 1 42 1
== Executing  PA-CTR  2, V(1)=25223, V(2)=0, repcount=12612, factor=3/2
302672            859233965               -37823  1 <B 437837 52 1 42 1
== Executing PPA-CTR  9 (once), V(1)=0, V(2)=1, V(3)=0, V(4)=37836
302693            859385339               -37825  1 <B 4 537840 3 52 3 1
== Executing  PA-CTR  4, V(1)=37837, V(2)=0, repcount=18919, factor=3/2
454045           1933284536               -56744  1 <B 456758 52 3 52 3 1
454046           1933284537               -56743  2 B> 456758 52 3 52 3 1
454047           1933341295                   15  2 356758 B> 52 3 52 3 1
454048           1933341296                   16  2 356759 A> 5 3 52 3 1
454049           1933341297                   15  2 356759 <B 4 3 52 3 1
454050           1933398056               -56744  2 <B 456760 3 52 3 1
454051           1933398057               -56745  <A 3 456760 3 52 3 1
454052           1933398058               -56744  1 B> 3 456760 3 52 3 1
454053           1933398059               -56745  1 <B 456761 3 52 3 1
454054           1933398060               -56744  2 B> 456761 3 52 3 1
454055           1933454821                   17  2 356761 B> 3 52 3 1
454056           1933454822                   16  2 356761 <B 4 52 3 1
454057           1933511583               -56745  2 <B 456762 52 3 1
454058           1933511584               -56746  <A 3 456762 52 3 1
454059           1933511585               -56745  1 B> 3 456762 52 3 1
454060           1933511586               -56746  1 <B 456763 52 3 1
454061           1933511587               -56745  2 B> 456763 52 3 1
454062           1933568350                   18  2 356763 B> 52 3 1
454063           1933568351                   19  2 356764 A> 5 3 1
454064           1933568352                   18  2 356764 <B 4 3 1
454065           1933625116               -56746  2 <B 456765 3 1
454066           1933625117               -56747  <A 3 456765 3 1
454067           1933625118               -56746  1 B> 3 456765 3 1
454068           1933625119               -56747  1 <B 456766 3 1
454069           1933625120               -56746  2 B> 456766 3 1
454070           1933681886                   20  2 356766 B> 3 1
454071           1933681887                   19  2 356766 <B 4 1
454072           1933738653               -56747  2 <B 456767 1
454073           1933738654               -56748  <A 3 456767 1
454074           1933738655               -56747  1 B> 3 456767 1
454075           1933738656               -56748  1 <B 456768 1
454076           1933738657               -56747  2 B> 456768 1
454077           1933795425                   21  2 356768 B> 1
454078           1933795426                   22  2 356768 2 B>
454079           1933795427                   21  2 356768 2 <A 1
454080           1933795428                   20  2 356768 <A 3 1
454081           1933852196               -56748  2 <A 556768 3 1
454082           1933852197               -56749  <A 3 556768 3 1
454083           1933852198               -56748  1 B> 3 556768 3 1
454084           1933852199               -56749  1 <B 4 556768 3 1
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  1 <B 41+V(2) 52 3 52 3 11+V(1)
    1                    1                    1  2 B> 41+V(2) 52 3 52 3 11+V(1)
    2               2+V(2)               2+V(2)  2 31+V(2) B> 52 3 52 3 11+V(1)
    3               3+V(2)               3+V(2)  2 32+V(2) A> 5 3 52 3 11+V(1)
    4               4+V(2)               2+V(2)  2 32+V(2) <B 4 3 52 3 11+V(1)
    5             6+2*V(2)                    0  2 <B 43+V(2) 3 52 3 11+V(1)
    6             7+2*V(2)                   -1  <A 3 43+V(2) 3 52 3 11+V(1)
    7             8+2*V(2)                    0  1 B> 3 43+V(2) 3 52 3 11+V(1)
    8             9+2*V(2)                   -1  1 <B 44+V(2) 3 52 3 11+V(1)
    9            10+2*V(2)                    0  2 B> 44+V(2) 3 52 3 11+V(1)
   10            14+3*V(2)               4+V(2)  2 34+V(2) B> 3 52 3 11+V(1)
   11            15+3*V(2)               3+V(2)  2 34+V(2) <B 4 52 3 11+V(1)
   12            19+4*V(2)                   -1  2 <B 45+V(2) 52 3 11+V(1)
   13            20+4*V(2)                   -2  <A 3 45+V(2) 52 3 11+V(1)
   14            21+4*V(2)                   -1  1 B> 3 45+V(2) 52 3 11+V(1)
   15            22+4*V(2)                   -2  1 <B 46+V(2) 52 3 11+V(1)
   16            23+4*V(2)                   -1  2 B> 46+V(2) 52 3 11+V(1)
   17            29+5*V(2)               5+V(2)  2 36+V(2) B> 52 3 11+V(1)
   18            30+5*V(2)               6+V(2)  2 37+V(2) A> 5 3 11+V(1)
   19            31+5*V(2)               5+V(2)  2 37+V(2) <B 4 3 11+V(1)
   20            38+6*V(2)                   -2  2 <B 48+V(2) 3 11+V(1)
   21            39+6*V(2)                   -3  <A 3 48+V(2) 3 11+V(1)
   22            40+6*V(2)                   -2  1 B> 3 48+V(2) 3 11+V(1)
   23            41+6*V(2)                   -3  1 <B 49+V(2) 3 11+V(1)
   24            42+6*V(2)                   -2  2 B> 49+V(2) 3 11+V(1)
   25            51+7*V(2)               7+V(2)  2 39+V(2) B> 3 11+V(1)
   26            52+7*V(2)               6+V(2)  2 39+V(2) <B 4 11+V(1)
   27            61+8*V(2)                   -3  2 <B 410+V(2) 11+V(1)
   28            62+8*V(2)                   -4  <A 3 410+V(2) 11+V(1)
   29            63+8*V(2)                   -3  1 B> 3 410+V(2) 11+V(1)
   30            64+8*V(2)                   -4  1 <B 411+V(2) 11+V(1)
   31            65+8*V(2)                   -3  2 B> 411+V(2) 11+V(1)
   32            76+9*V(2)               8+V(2)  2 311+V(2) B> 11+V(1)
   33       77+V(1)+9*V(2)          9+V(1)+V(2)  2 311+V(2) 21+V(1) B>
   34       78+V(1)+9*V(2)          8+V(1)+V(2)  2 311+V(2) 21+V(1) <A 1
   35     79+2*V(1)+9*V(2)               7+V(2)  2 311+V(2) <A 31+V(1) 1
   36    90+2*V(1)+10*V(2)                   -4  2 <A 511+V(2) 31+V(1) 1
   37    91+2*V(1)+10*V(2)                   -5  <A 3 511+V(2) 31+V(1) 1
   38    92+2*V(1)+10*V(2)                   -4  1 B> 3 511+V(2) 31+V(1) 1
   39    93+2*V(1)+10*V(2)                   -5  1 <B 4 511+V(2) 31+V(1) 1
<< Success! ==> defined new CTR 12 (PPA)
454084           1933852199               -56749  1 <B 4 556768 3 1
== Executing  PA-CTR  5, V(1)=56765, V(2)=0, repcount=28383, factor=3/2
681148           4350806564               -85132  1 <B 485150 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=85149
681172           4351317499               -85135  1 <B 4 585155 3 1
== Executing  PA-CTR  5, V(1)=85152, V(2)=0, repcount=42577, factor=3/2
1021788           9789975748              -127712  1 <B 4127732 5 3 1
== Executing PPA-CTR  6 (once), V(1)=127731
1021796           9790231219              -127713  1 <B 4 5127734 1
== Executing  PA-CTR  1, V(1)=127731, V(2)=0, repcount=63866, factor=3/2
1532724          22027212283              -191579  1 <B 4191599 52 1
== Executing PPA-CTR  7 (once), V(1)=0, V(2)=191598
1532741          22027978699              -191581  1 <B 4 5191602 3 1
== Executing  PA-CTR  5, V(1)=191599, V(2)=0, repcount=95800, factor=3/2
2299141          49561473499              -287381  1 <B 4287401 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=287400
2299165          49563197940              -287384  1 <B 4 5287406 3 1
== Executing  PA-CTR  5, V(1)=287403, V(2)=0, repcount=143702, factor=3/2
3448781         111514854564              -431086  1 <B 4431107 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=431106
3448805         111517441241              -431089  1 <B 4 5431112 3 1
== Executing  PA-CTR  5, V(1)=431109, V(2)=0, repcount=215555, factor=3/2
5173245         250910608646              -646644  1 <B 4646666 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=646665
5173269         250914488677              -646647  1 <B 4 5646671 3 1
== Executing  PA-CTR  5, V(1)=646668, V(2)=0, repcount=323335, factor=3/2
7759949         564552995362              -969982  1 <B 4970006 5 3 1
== Executing PPA-CTR  6 (once), V(1)=970005
7759957         564554935381              -969983  1 <B 4 5970008 1
== Executing  PA-CTR  1, V(1)=970005, V(2)=0, repcount=485003, factor=3/2
11639981        1270241575426             -1454986  1 <B 41455010 52 1
== Executing PPA-CTR  7 (once), V(1)=0, V(2)=1455009
11639998        1270247395486             -1454988  1 <B 4 51455013 3 1
== Executing  PA-CTR  5, V(1)=1455010, V(2)=0, repcount=727506, factor=3/2
17460046        2858046700630             -2182494  1 <B 42182519 5 3 1
== Executing PPA-CTR  6 (once), V(1)=2182518
17460054        2858051065675             -2182495  1 <B 4 52182521 1
== Executing  PA-CTR  1, V(1)=2182518, V(2)=0, repcount=1091260, factor=3/2
26190134        6430602776035             -3273755  1 <B 43273781 5 1
== Executing PPA-CTR  8 (once), V(1)=3273779
26190150        6430609323612             -3273756  1 <B 4 53273782 1 4 1
== Executing  PA-CTR  2, V(1)=3273779, V(2)=0, repcount=1636890, factor=3/2
39285270       14468845761252             -4910646  1 <B 44910671 52 1 4 1
== Executing PPA-CTR  9 (once), V(1)=0, V(2)=0, V(3)=0, V(4)=4910670
39285291       14468865403960             -4910648  1 <B 4 54910674 3 5 3 1
== Executing  PA-CTR  4, V(1)=4910671, V(2)=0, repcount=2455336, factor=3/2
58927979       32554904754664             -7365984  1 <B 47366009 52 3 5 3 1
58927980       32554904754665             -7365983  2 B> 47366009 52 3 5 3 1
58927981       32554912120674                   26  2 37366009 B> 52 3 5 3 1
58927982       32554912120675                   27  2 37366010 A> 5 3 5 3 1
58927983       32554912120676                   26  2 37366010 <B 4 3 5 3 1
58927984       32554919486686             -7365984  2 <B 47366011 3 5 3 1
58927985       32554919486687             -7365985  <A 3 47366011 3 5 3 1
58927986       32554919486688             -7365984  1 B> 3 47366011 3 5 3 1
58927987       32554919486689             -7365985  1 <B 47366012 3 5 3 1
58927988       32554919486690             -7365984  2 B> 47366012 3 5 3 1
58927989       32554926852702                   28  2 37366012 B> 3 5 3 1
58927990       32554926852703                   27  2 37366012 <B 4 5 3 1
58927991       32554934218715             -7365985  2 <B 47366013 5 3 1
58927992       32554934218716             -7365986  <A 3 47366013 5 3 1
58927993       32554934218717             -7365985  1 B> 3 47366013 5 3 1
58927994       32554934218718             -7365986  1 <B 47366014 5 3 1
58927995       32554934218719             -7365985  2 B> 47366014 5 3 1
58927996       32554941584733                   29  2 37366014 B> 5 3 1
58927997       32554941584734                   30  2 37366015 A> 3 1
58927998       32554941584735                   29  2 37366015 <A 5 1
58927999       32554948950750             -7365986  2 <A 57366016 1
58928000       32554948950751             -7365987  <A 3 57366016 1
58928001       32554948950752             -7365986  1 B> 3 57366016 1
58928002       32554948950753             -7365987  1 <B 4 57366016 1
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  1 <B 41+V(1) 52 3 5 3 [*]*
    1                    1                    1  2 B> 41+V(1) 52 3 5 3 [*]*
    2               2+V(1)               2+V(1)  2 31+V(1) B> 52 3 5 3 [*]*
    3               3+V(1)               3+V(1)  2 32+V(1) A> 5 3 5 3 [*]*
    4               4+V(1)               2+V(1)  2 32+V(1) <B 4 3 5 3 [*]*
    5             6+2*V(1)                    0  2 <B 43+V(1) 3 5 3 [*]*
    6             7+2*V(1)                   -1  <A 3 43+V(1) 3 5 3 [*]*
    7             8+2*V(1)                    0  1 B> 3 43+V(1) 3 5 3 [*]*
    8             9+2*V(1)                   -1  1 <B 44+V(1) 3 5 3 [*]*
    9            10+2*V(1)                    0  2 B> 44+V(1) 3 5 3 [*]*
   10            14+3*V(1)               4+V(1)  2 34+V(1) B> 3 5 3 [*]*
   11            15+3*V(1)               3+V(1)  2 34+V(1) <B 4 5 3 [*]*
   12            19+4*V(1)                   -1  2 <B 45+V(1) 5 3 [*]*
   13            20+4*V(1)                   -2  <A 3 45+V(1) 5 3 [*]*
   14            21+4*V(1)                   -1  1 B> 3 45+V(1) 5 3 [*]*
   15            22+4*V(1)                   -2  1 <B 46+V(1) 5 3 [*]*
   16            23+4*V(1)                   -1  2 B> 46+V(1) 5 3 [*]*
   17            29+5*V(1)               5+V(1)  2 36+V(1) B> 5 3 [*]*
   18            30+5*V(1)               6+V(1)  2 37+V(1) A> 3 [*]*
   19            31+5*V(1)               5+V(1)  2 37+V(1) <A 5 [*]*
   20            38+6*V(1)                   -2  2 <A 58+V(1) [*]*
   21            39+6*V(1)                   -3  <A 3 58+V(1) [*]*
   22            40+6*V(1)                   -2  1 B> 3 58+V(1) [*]*
   23            41+6*V(1)                   -3  1 <B 4 58+V(1) [*]*
<< Success! ==> defined new CTR 13 (PPA)
58928002       32554948950753             -7365987  1 <B 4 57366016 1
== Executing  PA-CTR  1, V(1)=7366013, V(2)=0, repcount=3683007, factor=3/2
88392058       73248592734942            -11048994  1 <B 411049022 52 1
== Executing PPA-CTR  7 (once), V(1)=0, V(2)=11049021
88392075       73248636931050            -11048996  1 <B 4 511049025 3 1
== Executing  PA-CTR  5, V(1)=11049022, V(2)=0, repcount=5524512, factor=3/2
132588171      164809368592554            -16573508  1 <B 416573537 5 3 1
== Executing PPA-CTR  6 (once), V(1)=16573536
132588179      164809401739635            -16573509  1 <B 4 516573539 1
== Executing  PA-CTR  1, V(1)=16573536, V(2)=0, repcount=8286769, factor=3/2
198882331      370821072838332            -24860278  1 <B 424860308 5 1
== Executing PPA-CTR  8 (once), V(1)=24860306
198882347      370821122558963            -24860279  1 <B 4 524860309 1 4 1
== Executing  PA-CTR  2, V(1)=24860306, V(2)=0, repcount=12430154, factor=3/2
298323579      834347382531035            -37290433  1 <B 437290463 5 1 4 1
== Executing PPA-CTR  3 (once), V(1)=37290461
298323601      834347457111982            -37290434  1 <B 4 537290464 1 42 1
== Executing  PA-CTR  2, V(1)=37290461, V(2)=0, repcount=18645231, factor=3/2
447485449     1877281486113451            -55935665  1 <B 455935694 52 1 42 1
== Executing PPA-CTR  9 (once), V(1)=0, V(2)=1, V(3)=0, V(4)=55935693
447485470     1877281709856253            -55935667  1 <B 4 555935697 3 52 3 1
== Executing  PA-CTR  4, V(1)=55935694, V(2)=0, repcount=27967848, factor=3/2
671228254     4223883442916653            -83903515  1 <B 483903545 5 3 52 3 1
== Executing PPA-CTR 10 (once), V(1)=1, V(2)=83903544
671228262     4223883610723750            -83903516  1 <B 4 583903549 3 1
== Executing  PA-CTR  5, V(1)=83903546, V(2)=0, repcount=41951774, factor=3/2
1006842454     9503737887675622           -125855290  1 <B 4125855323 5 3 1
== Executing PPA-CTR  6 (once), V(1)=125855322
1006842462     9503738139386275           -125855291  1 <B 4 5125855325 1
== Executing  PA-CTR  1, V(1)=125855322, V(2)=0, repcount=62927662, factor=3/2
1510263758    21383410451310979           -188782953  1 <B 4188782987 5 1
== Executing PPA-CTR  8 (once), V(1)=188782985
1510263774    21383410828876968           -188782954  1 <B 4 5188782988 1 4 1
== Executing  PA-CTR  2, V(1)=188782985, V(2)=0, repcount=94391493, factor=3/2
2265395718    48112673247533073           -283174447  1 <B 4283174480 52 1 4 1
== Executing PPA-CTR  9 (once), V(1)=0, V(2)=0, V(3)=0, V(4)=283174479
2265395739    48112674380231017           -283174449  1 <B 4 5283174483 3 5 3 1
== Executing  PA-CTR  4, V(1)=283174480, V(2)=0, repcount=141587241, factor=3/2
3398093667    1082535[4]1730706           -424761690  1 <B 4424761724 5 3 5 3 1
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=424761723
3398093675    1082535[4]1254161           -424761691  1 <B 4 5424761727 3 1
== Executing  PA-CTR  5, V(1)=424761724, V(2)=0, repcount=212380863, factor=3/2
5097140579    2435704[4]1413646           -637142554  1 <B 4637142590 5 3 1
== Executing PPA-CTR  6 (once), V(1)=637142589
5097140587    2435704[4]5698833           -637142555  1 <B 4 5637142592 1
== Executing  PA-CTR  1, V(1)=637142589, V(2)=0, repcount=318571295, factor=3/2
7645710947    5480334[4]1057678           -955713850  1 <B 4955713886 52 1
== Executing PPA-CTR  7 (once), V(1)=0, V(2)=955713885
7645710964    5480334[4]3913242           -955713852  1 <B 4 5955713889 3 1
== Executing  PA-CTR  5, V(1)=955713886, V(2)=0, repcount=477856944, factor=3/2
11468566516    1233075[5]8112314          -1433570796  1 <B 41433570833 5 3 1
== Executing PPA-CTR  6 (once), V(1)=1433570832
11468566524    1233075[5]5253987          -1433570797  1 <B 4 51433570835 1
== Executing  PA-CTR  1, V(1)=1433570832, V(2)=0, repcount=716785417, factor=3/2
17202849860    2774419[5]7558156          -2150356214  1 <B 42150356252 5 1
== Executing PPA-CTR  8 (once), V(1)=2150356250
17202849876    2774419[5]8270675          -2150356215  1 <B 4 52150356253 1 4 1
== Executing  PA-CTR  2, V(1)=2150356250, V(2)=0, repcount=1075178126, factor=3/2
25804274884    6242443[5]5955059          -3225534341  1 <B 43225534379 5 1 4 1
== Executing PPA-CTR  3 (once), V(1)=3225534377
25804274906    6242443[5]7023838          -3225534342  1 <B 4 53225534380 1 42 1
== Executing  PA-CTR  2, V(1)=3225534377, V(2)=0, repcount=1612767189, factor=3/2
38706412418    1404549[6]8512135          -4838301531  1 <B 44838301568 52 1 42 1
== Executing PPA-CTR  9 (once), V(1)=0, V(2)=1, V(3)=0, V(4)=4838301567
38706412439    1404549[6]1718433          -4838301533  1 <B 4 54838301571 3 52 3 1
== Executing  PA-CTR  4, V(1)=4838301568, V(2)=0, repcount=2419150785, factor=3/2
58059618719    3160236[6]4971818          -7257452318  1 <B 47257452356 5 3 52 3 1
== Executing PPA-CTR 10 (once), V(1)=1, V(2)=7257452355
58059618727    3160236[6]9876537          -7257452319  1 <B 4 57257452360 3 1
== Executing  PA-CTR  5, V(1)=7257452357, V(2)=0, repcount=3628726179, factor=3/2
87089428159    7110532[6]2053734         -10886178498  1 <B 410886178538 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=10886178537
87089428183    7110533[6]9124997         -10886178501  1 <B 4 510886178543 3 1
== Executing  PA-CTR  5, V(1)=10886178540, V(2)=0, repcount=5443089271, factor=3/2
130634142351    1599869[7]3594946         -16329267772  1 <B 416329267814 5 3 1
== Executing PPA-CTR  6 (once), V(1)=16329267813
130634142359    1599869[7]2130581         -16329267773  1 <B 4 516329267816 1
== Executing  PA-CTR  1, V(1)=16329267813, V(2)=0, repcount=8164633907, factor=3/2
195951213615    3599707[7]2187970         -24493901680  1 <B 424493901722 52 1
== Executing PPA-CTR  7 (once), V(1)=0, V(2)=24493901721
195951213632    3599707[7]7794878         -24493901682  1 <B 4 524493901725 3 1
== Executing  PA-CTR  5, V(1)=24493901722, V(2)=0, repcount=12246950862, factor=3/2
293926820528    8099341[7]7129182         -36740852544  1 <B 436740852587 5 3 1
== Executing PPA-CTR  6 (once), V(1)=36740852586
293926820536    8099341[7]8834363         -36740852545  1 <B 4 536740852589 1
== Executing  PA-CTR  1, V(1)=36740852586, V(2)=0, repcount=18370426294, factor=3/2
440890230888    1822351[8]1115435         -55111278839  1 <B 455111278883 5 1
== Executing PPA-CTR  8 (once), V(1)=55111278881
440890230904    1822351[8]3673216         -55111278840  1 <B 4 555111278884 1 4 1
== Executing  PA-CTR  2, V(1)=55111278881, V(2)=0, repcount=27555639441, factor=3/2
661335346432    4100291[8]1887305         -82666918281  1 <B 482666918324 52 1 4 1
== Executing PPA-CTR  9 (once), V(1)=0, V(2)=0, V(3)=0, V(4)=82666918323
661335346453    4100291[8]9560625         -82666918283  1 <B 4 582666918327 3 5 3 1
== Executing  PA-CTR  4, V(1)=82666918324, V(2)=0, repcount=41333459163, factor=3/2
992003019757    9225656[8]6297310        -124000377446  1 <B 4124000377490 5 3 5 3 1
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=124000377489
992003019765    9225656[8]7052297        -124000377447  1 <B 4 5124000377493 3 1
== Executing  PA-CTR  5, V(1)=124000377490, V(2)=0, repcount=62000188746, factor=3/2
1488004529733    2075772[9]3342321        -186000566193  1 <B 4186000566239 5 3 1
== Executing PPA-CTR  6 (once), V(1)=186000566238
1488004529741    2075772[9]4474806        -186000566194  1 <B 4 5186000566241 1
== Executing  PA-CTR  1, V(1)=186000566238, V(2)=0, repcount=93000283120, factor=3/2
2232006794701    4670488[9]6976726        -279000849314  1 <B 4279000849361 5 1
== Executing PPA-CTR  8 (once), V(1)=279000849359
2232006794717    4670488[9]8675463        -279000849315  1 <B 4 5279000849362 1 4 1
== Executing  PA-CTR  2, V(1)=279000849359, V(2)=0, repcount=139500424680, factor=3/2
3348010192157   1050859[10]0530743        -418501273995  1 <B 4418501274041 52 1 4 1
== Executing PPA-CTR  9 (once), V(1)=0, V(2)=0, V(3)=0, V(4)=418501274040
3348010192178   1050859[10]5626931        -418501273997  1 <B 4 5418501274044 3 5 3 1
== Executing  PA-CTR  4, V(1)=418501274041, V(2)=0, repcount=209250637021, factor=3/2
5022015288346   2364434[10]6712380        -627751911018  1 <B 4627751911064 52 3 5 3 1
== Executing PPA-CTR 13 (once), V(1)=627751911063
5022015288369   2364434[10]8178799        -627751911021  1 <B 4 5627751911071 1
== Executing  PA-CTR  1, V(1)=627751911068, V(2)=0, repcount=313875955535, factor=3/2
7533022932649   5319978[10]5320684        -941627866556  1 <B 4941627866606 5 1
== Executing PPA-CTR  8 (once), V(1)=941627866604
7533022932665   5319978[10]1053911        -941627866557  1 <B 4 5941627866607 1 4 1
== Executing  PA-CTR  2, V(1)=941627866604, V(2)=0, repcount=470813933303, factor=3/2
11299534399089   1196995[11]2123156       -1412441799860  1 <B 41412441799910 5 1 4 1
== Executing PPA-CTR  3 (once), V(1)=1412441799908
11299534399111   1196995[11]5722997       -1412441799861  1 <B 4 51412441799911 1 42 1
== Executing  PA-CTR  2, V(1)=1412441799908, V(2)=0, repcount=706220899955, factor=3/2
16949301598751   2693238[11]8128802       -2118662699816  1 <B 42118662699866 5 1 42 1
16949301598752   2693238[11]8128803       -2118662699815  2 B> 42118662699866 5 1 42 1
16949301598753   2693238[11]0828669                   51  2 32118662699866 B> 5 1 42 1
16949301598754   2693238[11]0828670                   52  2 32118662699867 A> 1 42 1
16949301598755   2693238[11]0828671                   53  2 32118662699867 0 B> 42 1
16949301598756   2693238[11]0828673                   55  2 32118662699867 0 32 B> 1
16949301598757   2693238[11]0828674                   56  2 32118662699867 0 32 2 B>
16949301598758   2693238[11]0828675                   55  2 32118662699867 0 32 2 <A 1
16949301598759   2693238[11]0828676                   54  2 32118662699867 0 32 <A 3 1
16949301598760   2693238[11]0828678                   52  2 32118662699867 0 <A 52 3 1
16949301598761   2693238[11]0828679                   53  2 32118662699867 1 B> 52 3 1
16949301598762   2693238[11]0828680                   54  2 32118662699867 1 3 A> 5 3 1
16949301598763   2693238[11]0828681                   53  2 32118662699867 1 3 <B 4 3 1
16949301598764   2693238[11]0828682                   52  2 32118662699867 1 <B 42 3 1
16949301598765   2693238[11]0828683                   53  2 32118662699867 2 B> 42 3 1
16949301598766   2693238[11]0828685                   55  2 32118662699867 2 32 B> 3 1
16949301598767   2693238[11]0828686                   54  2 32118662699867 2 32 <B 4 1
16949301598768   2693238[11]0828688                   52  2 32118662699867 2 <B 43 1
16949301598769   2693238[11]0828689                   51  2 32118662699867 <A 3 43 1
16949301598770   2693238[11]3528556       -2118662699816  2 <A 52118662699867 3 43 1
16949301598771   2693238[11]3528557       -2118662699817  <A 3 52118662699867 3 43 1
16949301598772   2693238[11]3528558       -2118662699816  1 B> 3 52118662699867 3 43 1
16949301598773   2693238[11]3528559       -2118662699817  1 <B 4 52118662699867 3 43 1
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  1 <B 42+V(1) 5 1 42 1
    1                    1                    1  2 B> 42+V(1) 5 1 42 1
    2               3+V(1)               3+V(1)  2 32+V(1) B> 5 1 42 1
    3               4+V(1)               4+V(1)  2 33+V(1) A> 1 42 1
    4               5+V(1)               5+V(1)  2 33+V(1) 0 B> 42 1
    5               7+V(1)               7+V(1)  2 33+V(1) 0 32 B> 1
    6               8+V(1)               8+V(1)  2 33+V(1) 0 32 2 B>
    7               9+V(1)               7+V(1)  2 33+V(1) 0 32 2 <A 1
    8              10+V(1)               6+V(1)  2 33+V(1) 0 32 <A 3 1
    9              12+V(1)               4+V(1)  2 33+V(1) 0 <A 52 3 1
   10              13+V(1)               5+V(1)  2 33+V(1) 1 B> 52 3 1
   11              14+V(1)               6+V(1)  2 33+V(1) 1 3 A> 5 3 1
   12              15+V(1)               5+V(1)  2 33+V(1) 1 3 <B 4 3 1
   13              16+V(1)               4+V(1)  2 33+V(1) 1 <B 42 3 1
   14              17+V(1)               5+V(1)  2 33+V(1) 2 B> 42 3 1
   15              19+V(1)               7+V(1)  2 33+V(1) 2 32 B> 3 1
   16              20+V(1)               6+V(1)  2 33+V(1) 2 32 <B 4 1
   17              22+V(1)               4+V(1)  2 33+V(1) 2 <B 43 1
   18              23+V(1)               3+V(1)  2 33+V(1) <A 3 43 1
   19            26+2*V(1)                    0  2 <A 53+V(1) 3 43 1
   20            27+2*V(1)                   -1  <A 3 53+V(1) 3 43 1
   21            28+2*V(1)                    0  1 B> 3 53+V(1) 3 43 1
   22            29+2*V(1)                   -1  1 <B 4 53+V(1) 3 43 1
<< Success! ==> defined new CTR 14 (PPA)
16949301598773   2693238[11]3528559       -2118662699817  1 <B 4 52118662699867 3 43 1
== Executing  PA-CTR  2, V(1)=2118662699864, V(2)=0, repcount=1059331349933, factor=3/2
25423952398237   6059787[11]8941624       -3177994049750  1 <B 43177994049800 5 3 43 1
25423952398238   6059787[11]8941625       -3177994049749  2 B> 43177994049800 5 3 43 1
25423952398239   6059787[11]2991425                   51  2 33177994049800 B> 5 3 43 1
25423952398240   6059787[11]2991426                   52  2 33177994049801 A> 3 43 1
25423952398241   6059787[11]2991427                   51  2 33177994049801 <A 5 43 1
25423952398242   6059787[11]7041228       -3177994049750  2 <A 53177994049802 43 1
25423952398243   6059787[11]7041229       -3177994049751  <A 3 53177994049802 43 1
25423952398244   6059787[11]7041230       -3177994049750  1 B> 3 53177994049802 43 1
25423952398245   6059787[11]7041231       -3177994049751  1 <B 4 53177994049802 43 1
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  1 <B 41+V(1) 5 3 [*]* [*]*
    1                    1                    1  2 B> 41+V(1) 5 3 [*]* [*]*
    2               2+V(1)               2+V(1)  2 31+V(1) B> 5 3 [*]* [*]*
    3               3+V(1)               3+V(1)  2 32+V(1) A> 3 [*]* [*]*
    4               4+V(1)               2+V(1)  2 32+V(1) <A 5 [*]* [*]*
    5             6+2*V(1)                    0  2 <A 53+V(1) [*]* [*]*
    6             7+2*V(1)                   -1  <A 3 53+V(1) [*]* [*]*
    7             8+2*V(1)                    0  1 B> 3 53+V(1) [*]* [*]*
    8             9+2*V(1)                   -1  1 <B 4 53+V(1) [*]* [*]*
<< Success! ==> defined new CTR 15 (PPA)
25423952398245   6059787[11]7041231       -3177994049751  1 <B 4 53177994049802 43 1
== Executing  PA-CTR  5, V(1)=3177994049799, V(2)=0, repcount=1588997024900, factor=3/2
38135928597445   1363452[12]9220631       -4766991074651  1 <B 44766991074701 52 43 1
38135928597446   1363452[12]9220632       -4766991074650  2 B> 44766991074701 52 43 1
38135928597447   1363452[12]0295333                   51  2 34766991074701 B> 52 43 1
38135928597448   1363452[12]0295334                   52  2 34766991074702 A> 5 43 1
38135928597449   1363452[12]0295335                   51  2 34766991074702 <B 44 1
38135928597450   1363452[12]1370037       -4766991074651  2 <B 44766991074706 1
38135928597451   1363452[12]1370038       -4766991074652  <A 3 44766991074706 1
38135928597452   1363452[12]1370039       -4766991074651  1 B> 3 44766991074706 1
38135928597453   1363452[12]1370040       -4766991074652  1 <B 44766991074707 1
38135928597454   1363452[12]1370041       -4766991074651  2 B> 44766991074707 1
38135928597455   1363452[12]2444748                   56  2 34766991074707 B> 1
38135928597456   1363452[12]2444749                   57  2 34766991074707 2 B>
38135928597457   1363452[12]2444750                   56  2 34766991074707 2 <A 1
38135928597458   1363452[12]2444751                   55  2 34766991074707 <A 3 1
38135928597459   1363452[12]3519458       -4766991074652  2 <A 54766991074707 3 1
38135928597460   1363452[12]3519459       -4766991074653  <A 3 54766991074707 3 1
38135928597461   1363452[12]3519460       -4766991074652  1 B> 3 54766991074707 3 1
38135928597462   1363452[12]3519461       -4766991074653  1 <B 4 54766991074707 3 1
>> Try to prove a PPA-CTR with 3 Vars...
    0                    0                    0  1 <B 41+V(3) 52 41+V(2) 11+V(1)
    1                    1                    1  2 B> 41+V(3) 52 41+V(2) 11+V(1)
    2               2+V(3)               2+V(3)  2 31+V(3) B> 52 41+V(2) 11+V(1)
    3               3+V(3)               3+V(3)  2 32+V(3) A> 5 41+V(2) 11+V(1)
    4               4+V(3)               2+V(3)  2 32+V(3) <B 42+V(2) 11+V(1)
    5             6+2*V(3)                    0  2 <B 44+V(2)+V(3) 11+V(1)
    6             7+2*V(3)                   -1  <A 3 44+V(2)+V(3) 11+V(1)
    7             8+2*V(3)                    0  1 B> 3 44+V(2)+V(3) 11+V(1)
    8             9+2*V(3)                   -1  1 <B 45+V(2)+V(3) 11+V(1)
    9            10+2*V(3)                    0  2 B> 45+V(2)+V(3) 11+V(1)
   10       15+V(2)+3*V(3)          5+V(2)+V(3)  2 35+V(2)+V(3) B> 11+V(1)
   11  16+V(1)+V(2)+3*V(3)     6+V(1)+V(2)+V(3)  2 35+V(2)+V(3) 21+V(1) B>
   12  17+V(1)+V(2)+3*V(3)     5+V(1)+V(2)+V(3)  2 35+V(2)+V(3) 21+V(1) <A 1
   13 18+2*V(1)+V(2)+3*V(3)          4+V(2)+V(3)  2 35+V(2)+V(3) <A 31+V(1) 1
   14 23+2*V(1)+2*V(2)+4*V(3)                   -1  2 <A 55+V(2)+V(3) 31+V(1) 1
   15 24+2*V(1)+2*V(2)+4*V(3)                   -2  <A 3 55+V(2)+V(3) 31+V(1) 1
   16 25+2*V(1)+2*V(2)+4*V(3)                   -1  1 B> 3 55+V(2)+V(3) 31+V(1) 1
   17 26+2*V(1)+2*V(2)+4*V(3)                   -2  1 <B 4 55+V(2)+V(3) 31+V(1) 1
<< Success! ==> defined new CTR 16 (PPA)
38135928597462   1363452[12]3519461       -4766991074653  1 <B 4 54766991074707 3 1
== Executing  PA-CTR  5, V(1)=4766991074704, V(2)=0, repcount=2383495537353, factor=3/2
57203892896286   3067767[12]1483406       -7150486612006  1 <B 47150486612060 5 3 1
== Executing PPA-CTR  6 (once), V(1)=7150486612059
57203892896294   3067767[12]4707533       -7150486612007  1 <B 4 57150486612062 1
== Executing  PA-CTR  1, V(1)=7150486612059, V(2)=0, repcount=3575243306030, factor=3/2
85805839344534   6902476[12]7626413      -10725729918037  1 <B 410725729918091 52 1
== Executing PPA-CTR  7 (once), V(1)=0, V(2)=10725729918090
85805839344551   6902476[12]7298797      -10725729918039  1 <B 4 510725729918094 3 1
== Executing  PA-CTR  5, V(1)=10725729918091, V(2)=0, repcount=5362864959046, factor=3/2
128708759016919   1553057[13]8743421      -16088594877085  1 <B 416088594877139 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=16088594877138
128708759016943   1553057[13]8006290      -16088594877088  1 <B 4 516088594877144 3 1
== Executing  PA-CTR  5, V(1)=16088594877141, V(2)=0, repcount=8044297438571, factor=3/2
193063138525511   3494378[13]8203839      -24132892315659  1 <B 424132892315714 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=24132892315713
193063138525535   3494378[13]2098158      -24132892315662  1 <B 4 524132892315719 3 1
== Executing  PA-CTR  5, V(1)=24132892315716, V(2)=0, repcount=12066446157859, factor=3/2
289594707788407   7862352[13]1436955      -36199338473521  1 <B 436199338473578 5 3 1
== Executing PPA-CTR  6 (once), V(1)=36199338473577
289594707788415   7862352[13]8384118      -36199338473522  1 <B 4 536199338473580 1
== Executing  PA-CTR  1, V(1)=36199338473577, V(2)=0, repcount=18099669236789, factor=3/2
434392061682727   1769029[14]6896415      -54299007710311  1 <B 454299007710368 52 1
== Executing PPA-CTR  7 (once), V(1)=0, V(2)=54299007710367
434392061682744   1769029[14]7737907      -54299007710313  1 <B 4 554299007710371 3 1
== Executing  PA-CTR  5, V(1)=54299007710368, V(2)=0, repcount=27149503855185, factor=3/2
651588092524224   3980316[14]5021692      -81448511565498  1 <B 481448511565556 5 3 1
== Executing PPA-CTR  6 (once), V(1)=81448511565555
651588092524232   3980316[14]8152811      -81448511565499  1 <B 4 581448511565558 1
== Executing  PA-CTR  1, V(1)=81448511565555, V(2)=0, repcount=40724255782778, factor=3/2
977382138786456   8955711[14]7041331     -122172767348277  1 <B 4122172767348335 52 1
== Executing PPA-CTR  7 (once), V(1)=0, V(2)=122172767348334
977382138786473   8955711[14]6434691     -122172767348279  1 <B 4 5122172767348338 3 1
== Executing  PA-CTR  5, V(1)=122172767348335, V(2)=0, repcount=61086383674168, factor=3/2
1466073208179817   2015034[15]9956371     -183259151022447  1 <B 4183259151022505 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=183259151022504
1466073208179841   2015034[15]6091436     -183259151022450  1 <B 4 5183259151022510 3 1
== Executing  PA-CTR  5, V(1)=183259151022507, V(2)=0, repcount=91629575511254, factor=3/2
2199109812269873   4533828[15]1116508     -274888726533704  1 <B 4274888726533763 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=274888726533762
2199109812269897   4533828[15]0319121     -274888726533707  1 <B 4 5274888726533768 3 1
== Executing  PA-CTR  5, V(1)=274888726533765, V(2)=0, repcount=137444363266883, factor=3/2
3298664718404961   1020111[16]3527486     -412333089800590  1 <B 4412333089800650 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=412333089800649
3298664718404985   1020111[16]2331421     -412333089800593  1 <B 4 5412333089800655 3 1
== Executing  PA-CTR  5, V(1)=412333089800652, V(2)=0, repcount=206166544900327, factor=3/2
4947997077607601   2295250[16]5854170     -618499634700920  1 <B 4618499634700982 5 3 1
== Executing PPA-CTR  6 (once), V(1)=618499634700981
4947997077607609   2295250[16]5256141     -618499634700921  1 <B 4 5618499634700984 1
== Executing  PA-CTR  1, V(1)=618499634700981, V(2)=0, repcount=309249817350491, factor=3/2
7421995616411537   5164314[16]3182330     -927749452051412  1 <B 4927749452051474 52 1
== Executing PPA-CTR  7 (once), V(1)=0, V(2)=927749452051473
7421995616411554   5164314[16]1388246     -927749452051414  1 <B 4 5927749452051477 3 1
== Executing  PA-CTR  5, V(1)=927749452051474, V(2)=0, repcount=463874726025738, factor=3/2
11132993424617458   1161970[17]2876606    -1391624178077152  1 <B 41391624178077215 5 3 1
== Executing PPA-CTR  6 (once), V(1)=1391624178077214
11132993424617466   1161970[17]9031043    -1391624178077153  1 <B 4 51391624178077217 1
== Executing  PA-CTR  1, V(1)=1391624178077214, V(2)=0, repcount=695812089038608, factor=3/2
16699490136926330   2614434[17]6995683    -2087436267115761  1 <B 42087436267115825 5 1
== Executing PPA-CTR  8 (once), V(1)=2087436267115823
16699490136926346   2614434[17]1227348    -2087436267115762  1 <B 4 52087436267115826 1 4 1
== Executing  PA-CTR  2, V(1)=2087436267115823, V(2)=0, repcount=1043718133557912, factor=3/2
25049235205389642   5882476[17]5974052    -3131154400673674  1 <B 43131154400673737 52 1 4 1
== Executing PPA-CTR  9 (once), V(1)=0, V(2)=0, V(3)=0, V(4)=3131154400673736
25049235205389663   5882476[17]8669024    -3131154400673676  1 <B 4 53131154400673740 3 5 3 1
== Executing  PA-CTR  4, V(1)=3131154400673737, V(2)=0, repcount=1565577200336869, factor=3/2
37573852808084615   1323557[18]2859721    -4696731601010545  1 <B 44696731601010608 52 3 5 3 1
== Executing PPA-CTR 13 (once), V(1)=4696731601010607
37573852808084638   1323557[18]8923404    -4696731601010548  1 <B 4 54696731601010615 1
== Executing  PA-CTR  1, V(1)=4696731601010612, V(2)=0, repcount=2348365800505307, factor=3/2
56360779212127094   2978003[18]7447993    -7045097401515855  1 <B 47045097401515922 5 1
== Executing PPA-CTR  8 (once), V(1)=7045097401515920
56360779212127110   2978003[18]0479852    -7045097401515856  1 <B 4 57045097401515923 1 4 1
== Executing  PA-CTR  2, V(1)=7045097401515920, V(2)=0, repcount=3522548700757961, factor=3/2
84541168818190798   6700508[18]9660181    -105676[4]2273817  1 <B 410567646102273884 5 1 4 1
== Executing PPA-CTR  3 (once), V(1)=10567646102273882
84541168818190820   6700508[18]4207970    -105676[4]2273818  1 <B 4 510567646102273885 1 42 1
== Executing  PA-CTR  2, V(1)=10567646102273882, V(2)=0, repcount=5283823051136942, factor=3/2
1268117[4]7286356   1507614[19]2363714    -158514[4]3410760  1 <B 415851469153410827 5 1 42 1
== Executing PPA-CTR 14 (once), V(1)=15851469153410825
1268117[4]7286378   1507614[19]9185393    -158514[4]3410761  1 <B 4 515851469153410828 3 43 1
== Executing  PA-CTR  2, V(1)=15851469153410825, V(2)=0, repcount=7925734576705413, factor=3/2
1902176[4]0929682   3392132[19]9919578    -237772[4]0116174  1 <B 423777203730116240 52 3 43 1
1902176[4]0929683   3392132[19]9919579    -237772[4]0116173  2 B> 423777203730116240 52 3 43 1
1902176[4]0929684   3392132[19]0035819                   67  2 323777203730116240 B> 52 3 43 1
1902176[4]0929685   3392132[19]0035820                   68  2 323777203730116241 A> 5 3 43 1
1902176[4]0929686   3392132[19]0035821                   67  2 323777203730116241 <B 4 3 43 1
1902176[4]0929687   3392132[19]0152062    -237772[4]0116174  2 <B 423777203730116242 3 43 1
1902176[4]0929688   3392132[19]0152063    -237772[4]0116175  <A 3 423777203730116242 3 43 1
1902176[4]0929689   3392132[19]0152064    -237772[4]0116174  1 B> 3 423777203730116242 3 43 1
1902176[4]0929690   3392132[19]0152065    -237772[4]0116175  1 <B 423777203730116243 3 43 1
1902176[4]0929691   3392132[19]0152066    -237772[4]0116174  2 B> 423777203730116243 3 43 1
1902176[4]0929692   3392132[19]0268309                   69  2 323777203730116243 B> 3 43 1
1902176[4]0929693   3392132[19]0268310                   68  2 323777203730116243 <B 44 1
1902176[4]0929694   3392132[19]0384553    -237772[4]0116175  2 <B 423777203730116247 1
1902176[4]0929695   3392132[19]0384554    -237772[4]0116176  <A 3 423777203730116247 1
1902176[4]0929696   3392132[19]0384555    -237772[4]0116175  1 B> 3 423777203730116247 1
1902176[4]0929697   3392132[19]0384556    -237772[4]0116176  1 <B 423777203730116248 1
1902176[4]0929698   3392132[19]0384557    -237772[4]0116175  2 B> 423777203730116248 1
1902176[4]0929699   3392132[19]0500805                   73  2 323777203730116248 B> 1
1902176[4]0929700   3392132[19]0500806                   74  2 323777203730116248 2 B>
1902176[4]0929701   3392132[19]0500807                   73  2 323777203730116248 2 <A 1
1902176[4]0929702   3392132[19]0500808                   72  2 323777203730116248 <A 3 1
1902176[4]0929703   3392132[19]0617056    -237772[4]0116176  2 <A 523777203730116248 3 1
1902176[4]0929704   3392132[19]0617057    -237772[4]0116177  <A 3 523777203730116248 3 1
1902176[4]0929705   3392132[19]0617058    -237772[4]0116176  1 B> 3 523777203730116248 3 1
1902176[4]0929706   3392132[19]0617059    -237772[4]0116177  1 <B 4 523777203730116248 3 1
>> Try to prove a PPA-CTR with 3 Vars...
    0                    0                    0  1 <B 41+V(3) 52 3 41+V(2) 11+V(1)
    1                    1                    1  2 B> 41+V(3) 52 3 41+V(2) 11+V(1)
    2               2+V(3)               2+V(3)  2 31+V(3) B> 52 3 41+V(2) 11+V(1)
    3               3+V(3)               3+V(3)  2 32+V(3) A> 5 3 41+V(2) 11+V(1)
    4               4+V(3)               2+V(3)  2 32+V(3) <B 4 3 41+V(2) 11+V(1)
    5             6+2*V(3)                    0  2 <B 43+V(3) 3 41+V(2) 11+V(1)
    6             7+2*V(3)                   -1  <A 3 43+V(3) 3 41+V(2) 11+V(1)
    7             8+2*V(3)                    0  1 B> 3 43+V(3) 3 41+V(2) 11+V(1)
    8             9+2*V(3)                   -1  1 <B 44+V(3) 3 41+V(2) 11+V(1)
    9            10+2*V(3)                    0  2 B> 44+V(3) 3 41+V(2) 11+V(1)
   10            14+3*V(3)               4+V(3)  2 34+V(3) B> 3 41+V(2) 11+V(1)
   11            15+3*V(3)               3+V(3)  2 34+V(3) <B 42+V(2) 11+V(1)
   12            19+4*V(3)                   -1  2 <B 46+V(2)+V(3) 11+V(1)
   13            20+4*V(3)                   -2  <A 3 46+V(2)+V(3) 11+V(1)
   14            21+4*V(3)                   -1  1 B> 3 46+V(2)+V(3) 11+V(1)
   15            22+4*V(3)                   -2  1 <B 47+V(2)+V(3) 11+V(1)
   16            23+4*V(3)                   -1  2 B> 47+V(2)+V(3) 11+V(1)
   17       30+V(2)+5*V(3)          6+V(2)+V(3)  2 37+V(2)+V(3) B> 11+V(1)
   18  31+V(1)+V(2)+5*V(3)     7+V(1)+V(2)+V(3)  2 37+V(2)+V(3) 21+V(1) B>
   19  32+V(1)+V(2)+5*V(3)     6+V(1)+V(2)+V(3)  2 37+V(2)+V(3) 21+V(1) <A 1
   20 33+2*V(1)+V(2)+5*V(3)          5+V(2)+V(3)  2 37+V(2)+V(3) <A 31+V(1) 1
   21 40+2*V(1)+2*V(2)+6*V(3)                   -2  2 <A 57+V(2)+V(3) 31+V(1) 1
   22 41+2*V(1)+2*V(2)+6*V(3)                   -3  <A 3 57+V(2)+V(3) 31+V(1) 1
   23 42+2*V(1)+2*V(2)+6*V(3)                   -2  1 B> 3 57+V(2)+V(3) 31+V(1) 1
   24 43+2*V(1)+2*V(2)+6*V(3)                   -3  1 <B 4 57+V(2)+V(3) 31+V(1) 1
<< Success! ==> defined new CTR 17 (PPA)
1902176[4]0929706   3392132[19]0617059    -237772[4]0116177  1 <B 4 523777203730116248 3 1
== Executing  PA-CTR  5, V(1)=23777203730116245, V(2)=0, repcount=11888601865058123, factor=3/2
2853264[4]1394690   7632298[19]5815184    -356658[4]5174300  1 <B 435665805595174370 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=35665805595174369
2853264[4]1394714   7632298[19]6861439    -356658[4]5174303  1 <B 4 535665805595174375 3 1
== Executing  PA-CTR  5, V(1)=35665805595174372, V(2)=0, repcount=17832902797587187, factor=3/2
4279896[4]2092210   1717267[20]2103468    -534987[4]2761490  1 <B 453498708392761562 5 3 1
== Executing PPA-CTR  6 (once), V(1)=53498708392761561
4279896[4]2092218   1717267[20]7626599    -534987[4]2761491  1 <B 4 553498708392761564 1
== Executing  PA-CTR  1, V(1)=53498708392761561, V(2)=0, repcount=26749354196380781, factor=3/2
6419845[4]3138466   3863850[20]4421168    -802480[4]9142272  1 <B 480248062589142344 52 1
== Executing PPA-CTR  7 (once), V(1)=0, V(2)=80248062589142343
6419845[4]3138483   3863850[20]0990564    -802480[4]9142274  1 <B 4 580248062589142347 3 1
== Executing  PA-CTR  5, V(1)=80248062589142344, V(2)=0, repcount=40124031294571173, factor=3/2
9629767[4]9707867   8693664[20]6205389    -120372[5]3713447  1 <B 41203720[4]3713520 5 3 1
== Executing PPA-CTR  6 (once), V(1)=1203720[4]3713519
9629767[4]9707875   8693664[20]3632436    -120372[5]3713448  1 <B 4 51203720[4]3713522 1
== Executing  PA-CTR  1, V(1)=1203720[4]3713519, V(2)=0, repcount=60186046941856760, factor=3/2
1444465[5]4561955   1956074[21]7865796    -180558[5]5570208  1 <B 41805581[4]5570281 52 1
== Executing PPA-CTR  7 (once), V(1)=0, V(2)=1805581[4]5570280
1444465[5]4561972   1956074[21]0146940    -180558[5]5570210  1 <B 4 51805581[4]5570284 3 1
== Executing  PA-CTR  5, V(1)=1805581[4]5570281, V(2)=0, repcount=90279070412785141, factor=3/2
2166697[5]6843100   4401167[21]8027429    -270837[5]8355351  1 <B 42708372[4]8355424 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=2708372[4]8355423
2166697[5]6843124   4401167[21]8160008    -270837[5]8355354  1 <B 4 52708372[4]8355429 3 1
== Executing  PA-CTR  5, V(1)=2708372[4]8355426, V(2)=0, repcount=1354186[4]9177714, factor=3/2
3250046[5]0264836   9902627[21]6023680    -406255[5]7533068  1 <B 44062558[4]7533143 5 3 1
== Executing PPA-CTR  6 (once), V(1)=4062558[4]7533142
3250046[5]0264844   9902627[21]1089973    -406255[5]7533069  1 <B 4 54062558[4]7533145 1
== Executing  PA-CTR  1, V(1)=4062558[4]7533142, V(2)=0, repcount=2031279[4]8766572, factor=3/2
4875069[5]0397420   2228091[22]7582957    -609383[5]6299641  1 <B 46093837[4]6299717 5 1
== Executing PPA-CTR  8 (once), V(1)=6093837[4]6299715
4875069[5]0397436   2228091[22]0182406    -609383[5]6299642  1 <B 4 56093837[4]6299718 1 4 1
== Executing  PA-CTR  2, V(1)=6093837[4]6299715, V(2)=0, repcount=3046918[4]3149858, factor=3/2
7312604[5]5596300   5013205[22]5342046    -914075[5]9449500  1 <B 49140755[4]9449575 52 1 4 1
== Executing PPA-CTR  9 (once), V(1)=0, V(2)=0, V(3)=0, V(4)=9140755[4]9449574
7312604[5]5596321   5013205[22]3140370    -914075[5]9449502  1 <B 4 59140755[4]9449578 3 5 3 1
== Executing  PA-CTR  4, V(1)=9140755[4]9449575, V(2)=0, repcount=4570377[4]4724788, factor=3/2
1096890[6]3394625   1127971[23]6423930    -137111[6]4174290  1 <B 41371113[5]4174365 52 3 5 3 1
== Executing PPA-CTR 13 (once), V(1)=1371113[5]4174364
1096890[6]3394648   1127971[23]1470155    -137111[6]4174293  1 <B 4 51371113[5]4174372 1
== Executing  PA-CTR  1, V(1)=1371113[5]4174369, V(2)=0, repcount=6855566[4]7087185, factor=3/2
1645336[6]0092128   2537935[23]7665940    -205667[6]1261478  1 <B 42056670[5]1261556 52 1
== Executing PPA-CTR  7 (once), V(1)=0, V(2)=2056670[5]1261555
1645336[6]0092145   2537935[23]2712184    -205667[6]1261480  1 <B 4 52056670[5]1261559 3 1
== Executing  PA-CTR  5, V(1)=2056670[5]1261556, V(2)=0, repcount=1028335[5]0630779, factor=3/2
2468004[6]5138377   5710353[23]2937381    -308500[6]1892259  1 <B 43085005[5]1892338 5 3 1
== Executing PPA-CTR  6 (once), V(1)=3085005[5]1892337
2468004[6]5138385   5710353[23]6722064    -308500[6]1892260  1 <B 4 53085005[5]1892340 1
== Executing  PA-CTR  1, V(1)=3085005[5]1892337, V(2)=0, repcount=1542502[5]0946169, factor=3/2
3702006[6]2707737   1284829[24]9728761    -462750[6]2838429  1 <B 44627507[5]2838508 52 1
== Executing PPA-CTR  7 (once), V(1)=0, V(2)=4627507[5]2838507
3702006[6]2707754   1284829[24]1082813    -462750[6]2838431  1 <B 4 54627507[5]2838511 3 1
== Executing  PA-CTR  5, V(1)=4627507[5]2838508, V(2)=0, repcount=2313753[5]6419255, factor=3/2
5553009[6]4061794   2890866[24]3863418    -694126[6]9257686  1 <B 46941261[5]9257766 5 3 1
== Executing PPA-CTR  6 (once), V(1)=6941261[5]9257765
5553009[6]4061802   2890866[24]2378957    -694126[6]9257687  1 <B 4 56941261[5]9257768 1
== Executing  PA-CTR  1, V(1)=6941261[5]9257765, V(2)=0, repcount=3470630[5]9628883, factor=3/2
8329513[6]1092866   6504450[24]3635322    -104118[7]8886570  1 <B 41041189[6]8886650 52 1
== Executing PPA-CTR  7 (once), V(1)=0, V(2)=1041189[6]8886649
8329513[6]1092883   6504450[24]9181942    -104118[7]8886572  1 <B 4 51041189[6]8886653 3 1
== Executing  PA-CTR  5, V(1)=1041189[6]8886650, V(2)=0, repcount=5205946[5]9443326, factor=3/2
1249427[7]6639491   1463501[25]3668726    -156178[7]8329898  1 <B 41561783[6]8329979 5 3 1
== Executing PPA-CTR  6 (once), V(1)=1561783[6]8329978
1249427[7]6639499   1463501[25]0328691    -156178[7]8329899  1 <B 4 51561783[6]8329981 1
== Executing  PA-CTR  1, V(1)=1561783[6]8329978, V(2)=0, repcount=7808919[5]9164990, factor=3/2
1874140[7]9959419   3292877[25]0418931    -234267[7]7494889  1 <B 42342675[6]7494971 5 1
== Executing PPA-CTR  8 (once), V(1)=2342675[6]7494969
1874140[7]9959435   3292877[25]5408888    -234267[7]7494890  1 <B 4 52342675[6]7494972 1 4 1
== Executing  PA-CTR  2, V(1)=2342675[6]7494969, V(2)=0, repcount=1171337[6]8747485, factor=3/2
2811210[7]9939315   7408975[25]9369473    -351401[7]6242375  1 <B 43514013[6]6242456 52 1 4 1
== Executing PPA-CTR  9 (once), V(1)=0, V(2)=0, V(3)=0, V(4)=3514013[6]6242455
2811210[7]9939336   7408975[25]4339321    -351401[7]6242377  1 <B 4 53514013[6]6242459 3 5 3 1
== Executing  PA-CTR  4, V(1)=3514013[6]6242456, V(2)=0, repcount=1757006[6]3121229, factor=3/2
4216816[7]4909168   1667019[26]4478018    -527102[7]9363606  1 <B 45271020[6]9363688 5 3 5 3 1
== Executing PPA-CTR 10 (once), V(1)=0, V(2)=5271020[6]9363687
4216816[7]4909176   1667019[26]3205401    -527102[7]9363607  1 <B 4 55271020[6]9363691 3 1
== Executing  PA-CTR  5, V(1)=5271020[6]9363688, V(2)=0, repcount=2635510[6]4681845, factor=3/2
6325224[7]2363936   3750793[26]9108546    -790653[7]4045452  1 <B 47906530[6]4045536 5 3 1
== Executing PPA-CTR  6 (once), V(1)=7906530[6]4045535
6325224[7]2363944   3750793[26]7199625    -790653[7]4045453  1 <B 4 57906530[6]4045538 1
== Executing  PA-CTR  1, V(1)=7906530[6]4045535, V(2)=0, repcount=3953265[6]2022768, factor=3/2
9487836[7]8546088   8439285[26]0481705    -118597[8]6068221  1 <B 41185979[7]6068305 52 1
== Executing PPA-CTR  7 (once), V(1)=0, V(2)=1185979[7]6068304
9487836[7]8546105   8439285[26]4754945    -118597[8]6068223  1 <B 4 51185979[7]6068308 3 1
== Executing  PA-CTR  5, V(1)=1185979[7]6068305, V(2)=0, repcount=5929898[6]3034153, factor=3/2
1423175[8]2819329   1898839[27]6242090    -177896[8]9102376  1 <B 41778969[7]9102460 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=1778969[7]9102459
1423175[8]2819353   1898839[27]0856885    -177896[8]9102379  1 <B 4 51778969[7]9102465 3 1
== Executing  PA-CTR  5, V(1)=1778969[7]9102462, V(2)=0, repcount=8894847[6]9551232, factor=3/2
2134763[8]9229209   4272388[27]6317749    -266845[8]8653611  1 <B 42668454[7]8653697 5 3 1
== Executing PPA-CTR  6 (once), V(1)=2668454[7]8653696
2134763[8]9229217   4272388[27]3625150    -266845[8]8653612  1 <B 4 52668454[7]8653699 1
== Executing  PA-CTR  1, V(1)=2668454[7]8653696, V(2)=0, repcount=1334227[7]9326849, factor=3/2
3202144[8]3844009   9612873[27]6392647    -400268[8]7980461  1 <B 44002681[7]7980548 5 1
== Executing PPA-CTR  8 (once), V(1)=4002681[7]7980546
3202144[8]3844025   9612873[27]2353758    -400268[8]7980462  1 <B 4 54002681[7]7980549 1 4 1
== Executing  PA-CTR  2, V(1)=4002681[7]7980546, V(2)=0, repcount=2001340[7]8990274, factor=3/2
4803217[8]5766217   2162896[28]6080630    -600402[8]6970736  1 <B 46004021[7]6970823 5 1 4 1
== Executing PPA-CTR  3 (once), V(1)=6004021[7]6970821
4803217[8]5766239   2162896[28]0022297    -600402[8]6970737  1 <B 4 56004021[7]6970824 1 42 1
== Executing  PA-CTR  2, V(1)=6004021[7]6970821, V(2)=0, repcount=3002010[7]8485411, factor=3/2
7204826[8]3649527   4866517[28]0451526    -900603[8]5456148  1 <B 49006032[7]5456234 52 1 42 1
== Executing PPA-CTR  9 (once), V(1)=0, V(2)=1, V(3)=0, V(4)=9006032[7]5456233
7204826[8]3649548   4866517[28]2276488    -900603[8]5456150  1 <B 4 59006032[7]5456237 3 52 3 1
== Executing  PA-CTR  4, V(1)=9006032[7]5456234, V(2)=0, repcount=4503016[7]2728118, factor=3/2
1080723[9]5474492   1094966[29]2110968    -135090[9]8184268  1 <B 41350904[8]8184355 5 3 52 3 1
== Executing PPA-CTR 10 (once), V(1)=1, V(2)=1350904[8]8184354
1080723[9]5474500   1094966[29]8479685    -135090[9]8184269  1 <B 4 51350904[8]8184359 3 1
== Executing  PA-CTR  5, V(1)=1350904[8]8184356, V(2)=0, repcount=6754524[7]9092179, factor=3/2
1621085[9]8211932   2463674[29]9936882    -202635[9]7276448  1 <B 42026357[8]7276538 5 3 1
== Executing PPA-CTR  6 (once), V(1)=2026357[8]7276537
1621085[9]8211940   2463674[29]4489965    -202635[9]7276449  1 <B 4 52026357[8]7276540 1
== Executing  PA-CTR  1, V(1)=2026357[8]7276537, V(2)=0, repcount=1013178[8]8638269, factor=3/2
2431628[9]7318092   5543267[29]0268662    -303953[9]5914718  1 <B 43039536[8]5914808 52 1
== Executing PPA-CTR  7 (once), V(1)=0, V(2)=3039536[8]5914807
2431628[9]7318109   5543267[29]3927914    -303953[9]5914720  1 <B 4 53039536[8]5914811 3 1
== Executing  PA-CTR  5, V(1)=3039536[8]5914808, V(2)=0, repcount=1519768[8]7957405, factor=3/2
3647443[9]0977349   1247235[30]4674419    -455930[9]3872125  1 <B 44559304[8]3872216 5 3 1
== Executing PPA-CTR  6 (once), V(1)=4559304[8]3872215
3647443[9]0977357   1247235[30]2418858    -455930[9]3872126  1 <B 4 54559304[8]3872218 1
== Executing  PA-CTR  1, V(1)=4559304[8]3872215, V(2)=0, repcount=2279652[8]6936108, factor=3/2
5471164[9]6466221   2806279[30]6598498    -683895[9]0808234  1 <B 46838956[8]0808325 52 1
== Executing PPA-CTR  7 (once), V(1)=0, V(2)=6838956[8]0808324
5471164[9]6466238   2806279[30]9831818    -683895[9]0808236  1 <B 4 56838956[8]0808328 3 1
== Executing  PA-CTR  5, V(1)=6838956[8]0808325, V(2)=0, repcount=3419478[8]5404163, factor=3/2
8206747[9]9699542   6314128[30]5448503   -102584[10]6212399  1 <B 41025843[9]6212490 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=1025843[9]6212489
8206747[9]9699566   6314128[30]2723478   -102584[10]6212402  1 <B 4 51025843[9]6212495 3 1
== Executing  PA-CTR  5, V(1)=1025843[9]6212492, V(2)=0, repcount=5129217[8]8106247, factor=3/2
1231012[10]4549542   1420678[31]2635987   -153876[10]4318649  1 <B 41538765[9]4318742 5 3 1
== Executing PPA-CTR  6 (once), V(1)=1538765[9]4318741
1231012[10]4549550   1420678[31]1273478   -153876[10]4318650  1 <B 4 51538765[9]4318744 1
== Executing  PA-CTR  1, V(1)=1538765[9]4318741, V(2)=0, repcount=7693825[8]2159371, factor=3/2
1846518[10]1824518   3196527[31]3576627   -230814[10]6478021  1 <B 42308147[9]6478114 52 1
== Executing PPA-CTR  7 (once), V(1)=0, V(2)=2308147[9]6478113
1846518[10]1824535   3196527[31]9489103   -230814[10]6478023  1 <B 4 52308147[9]6478117 3 1
== Executing  PA-CTR  5, V(1)=2308147[9]6478114, V(2)=0, repcount=1154073[9]8239058, factor=3/2
2769777[10]7736999   7192186[31]9105543   -346222[10]4717081  1 <B 43462221[9]4717175 5 3 1
== Executing PPA-CTR  6 (once), V(1)=3462221[9]4717174
2769777[10]7737007   7192186[31]8539900   -346222[10]4717082  1 <B 4 53462221[9]4717177 1
== Executing  PA-CTR  1, V(1)=3462221[9]4717174, V(2)=0, repcount=1731110[9]7358588, factor=3/2
4154665[10]6605711   1618241[32]4752660   -519333[10]2075670  1 <B 45193332[9]2075765 5 1
== Executing PPA-CTR  8 (once), V(1)=5193332[9]2075763
4154665[10]6605727   1618241[32]8904205   -519333[10]2075671  1 <B 4 55193332[9]2075766 1 4 1
== Executing  PA-CTR  2, V(1)=5193332[9]2075763, V(2)=0, repcount=2596666[9]6037882, factor=3/2
6231998[10]4908783   3641044[32]2269269   -778999[10]8113553  1 <B 47789998[9]8113647 52 1 4 1
== Executing PPA-CTR  9 (once), V(1)=0, V(2)=0, V(3)=0, V(4)=7789998[9]8113646
6231998[10]4908804   3641044[32]4723881   -778999[10]8113555  1 <B 4 57789998[9]8113650 3 5 3 1
== Executing  PA-CTR  4, V(1)=7789998[9]8113647, V(2)=0, repcount=3894999[9]4056824, factor=3/2
9347997[10]7363396   8192349[32]1965753   -116849[11]2170379  1 <B 41168499[10]2170473 52 3 5 3 1
== Executing PPA-CTR 13 (once), V(1)=1168499[10]2170472
9347997[10]7363419   8192349[32]4988626   -116849[11]2170382  1 <B 4 51168499[10]2170480 1
== Executing  PA-CTR  1, V(1)=1168499[10]2170477, V(2)=0, repcount=5842498[9]1085239, factor=3/2
1402199[11]6045331   1843278[33]2561423   -175274[11]3255621  1 <B 41752749[10]3255718 52 1
== Executing PPA-CTR  7 (once), V(1)=0, V(2)=1752749[10]3255717
1402199[11]6045348   1843278[33]5584315   -175274[11]3255623  1 <B 4 51752749[10]3255721 3 1
== Executing  PA-CTR  5, V(1)=1752749[10]3255718, V(2)=0, repcount=8763748[9]6627860, factor=3/2
2103299[11]9068228   4147377[33]9890275   -262912[11]9883483  1 <B 42629124[10]9883581 5 3 1
== Executing PPA-CTR  6 (once), V(1)=2629124[10]9883580
2103299[11]9068236   4147377[33]9657444   -262912[11]9883484  1 <B 4 52629124[10]9883583 1
== Executing  PA-CTR  1, V(1)=2629124[10]9883580, V(2)=0, repcount=1314562[10]4941791, factor=3/2
3154949[11]8602564   9331598[33]4171233   -394368[11]4825275  1 <B 43943686[10]4825374 5 1
== Executing PPA-CTR  8 (once), V(1)=3943686[10]4825372
3154949[11]8602580   9331598[33]3821996   -394368[11]4825276  1 <B 4 53943686[10]4825375 1 4 1
== Executing  PA-CTR  2, V(1)=3943686[10]4825372, V(2)=0, repcount=1971843[10]7412687, factor=3/2
4732423[11]7904076   2099609[34]3978025   -591552[11]2237963  1 <B 45915529[10]2238062 5 1 4 1
== Executing PPA-CTR  3 (once), V(1)=5915529[10]2238060
4732423[11]7904098   2099609[34]8454170   -591552[11]2237964  1 <B 4 55915529[10]2238063 1 42 1
== Executing  PA-CTR  2, V(1)=5915529[10]2238060, V(2)=0, repcount=2957764[10]1119031, factor=3/2
7098635[11]6856346   4724121[34]6305239   -887329[11]3356995  1 <B 48873294[10]3357094 5 1 42 1
== Executing PPA-CTR 14 (once), V(1)=8873294[10]3357092
7098635[11]6856368   4724121[34]3019452   -887329[11]3356996  1 <B 4 58873294[10]3357095 3 43 1
== Executing  PA-CTR  2, V(1)=8873294[10]3357092, V(2)=0, repcount=4436647[10]1678547, factor=3/2
1064795[12]0284744   1062927[35]3184361   -133099[12]5035543  1 <B 41330994[11]5035642 5 3 43 1
== Executing PPA-CTR 15 (once), V(1)=1330994[11]5035641
1064795[12]0284752   1062927[35]3255652   -133099[12]5035544  1 <B 4 51330994[11]5035644 43 1
== Executing  PA-CTR  5, V(1)=1330994[11]5035641, V(2)=0, repcount=6654971[10]7517821, factor=3/2
1597193[12]0427320   2391586[35]6126701   -199649[12]2553365  1 <B 41996491[11]2553464 52 43 1
== Executing PPA-CTR 16 (once), V(1)=0, V(2)=2, V(3)=1996491[11]2553463
1597193[12]0427337   2391586[35]6340583   -199649[12]2553367  1 <B 4 51996491[11]2553470 3 1
== Executing  PA-CTR  5, V(1)=1996491[11]2553467, V(2)=0, repcount=9982456[10]6276734, factor=3/2
2395789[12]0641209   5381069[35]3121255   -299473[12]8830101  1 <B 42994737[11]8830203 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=2994737[11]8830202
2395789[12]0641233   5381069[35]6102508   -299473[12]8830104  1 <B 4 52994737[11]8830208 3 1
== Executing  PA-CTR  5, V(1)=2994737[11]8830205, V(2)=0, repcount=1497368[11]4415103, factor=3/2
3593684[12]5962057   1210740[36]6094953   -449210[12]3245207  1 <B 44492105[11]3245310 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=4492105[11]3245309
3593684[12]5962081   1210740[36]5566848   -449210[12]3245210  1 <B 4 54492105[11]3245315 3 1
== Executing  PA-CTR  5, V(1)=4492105[11]3245312, V(2)=0, repcount=2246052[11]6622657, factor=3/2
5390526[12]8943337   2724166[36]2521737   -673815[12]9867867  1 <B 46738158[11]9867972 5 3 1
== Executing PPA-CTR  6 (once), V(1)=6738158[11]9867971
5390526[12]8943345   2724166[36]2257688   -673815[12]9867868  1 <B 4 56738158[11]9867974 1
== Executing  PA-CTR  1, V(1)=6738158[11]9867971, V(2)=0, repcount=3369079[11]4933986, factor=3/2
8085790[12]8415233   6129375[36]5406192   -101072[13]4801854  1 <B 41010723[12]4801959 52 1
== Executing PPA-CTR  7 (once), V(1)=0, V(2)=1010723[12]4801958
8085790[12]8415250   6129375[36]4614048   -101072[13]4801856  1 <B 4 51010723[12]4801962 3 1
== Executing  PA-CTR  5, V(1)=1010723[12]4801959, V(2)=0, repcount=5053618[11]2400980, factor=3/2
1212868[13]7623090   1379109[37]3901128   -151608[13]7202836  1 <B 41516085[12]7202941 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=1516085[12]7202940
1212868[13]7623114   1379109[37]7118809   -151608[13]7202839  1 <B 4 51516085[12]7202946 3 1
== Executing  PA-CTR  5, V(1)=1516085[12]7202943, V(2)=0, repcount=7580428[11]8601472, factor=3/2
1819302[13]6434890   3102996[37]0427993   -227412[13]5804311  1 <B 42274128[12]5804417 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=2274128[12]5804416
1819302[13]6434914   3102996[37]5254530   -227412[13]5804314  1 <B 4 52274128[12]5804422 3 1
== Executing  PA-CTR  5, V(1)=2274128[12]5804419, V(2)=0, repcount=1137064[12]7902210, factor=3/2
2728954[13]9652594   6981741[37]1320090   -341119[13]3706524  1 <B 43411192[12]3706631 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=3411192[12]3706630
2728954[13]9652618   6981741[37]3559911   -341119[13]3706527  1 <B 4 53411192[12]3706636 3 1
== Executing  PA-CTR  5, V(1)=3411192[12]3706633, V(2)=0, repcount=1705596[12]1853317, factor=3/2
4093431[13]4479154   1570891[38]6387280   -511678[13]5559844  1 <B 45116789[12]5559952 52 3 1
== Executing PPA-CTR 11 (once), V(1)=0, V(2)=5116789[12]5559951
4093431[13]4479178   1570891[38]9747027   -511678[13]5559847  1 <B 4 55116789[12]5559957 3 1
== Executing  PA-CTR  5, V(1)=5116789[12]5559954, V(2)=0, repcount=2558394[12]2779978, factor=3/2
6140146[13]6719002   3534506[38]9468347   -767518[13]8339825  1 <B 47675183[12]8339935 5 3 1
== Executing PPA-CTR  6 (once), V(1)=7675183[12]8339934
6140146[13]6719010   3534506[38]6148224   -767518[13]8339826  1 <B 4 57675183[12]8339937 1
== Executing  PA-CTR  1, V(1)=7675183[12]8339934, V(2)=0, repcount=3837591[12]9169968, factor=3/2
9210220[13]0078754   7952639[38]0531104   -115127[14]7509794  1 <B 41151277[13]7509905 5 1
== Executing PPA-CTR  8 (once), V(1)=1151277[13]7509903
9210220[13]0078770   7952639[38]5550929   -115127[14]7509795  1 <B 4 51151277[13]7509906 1 4 1
== Executing  PA-CTR  2, V(1)=1151277[13]7509903, V(2)=0, repcount=5756387[12]8754952, factor=3/2
1381533[14]0118386   1789343[39]1647553   -172691[14]6264747  1 <B 41726916[13]6264857 52 1 4 1
== Executing PPA-CTR  9 (once), V(1)=0, V(2)=0, V(3)=0, V(4)=1726916[13]6264856
1381533[14]0118407   1789343[39]6707005   -172691[14]6264749  1 <B 4 51726916[13]6264860 3 5 3 1
== Executing  PA-CTR  4, V(1)=1726916[13]6264857, V(2)=0, repcount=8634581[12]8132429, factor=3/2
2072299[14]5177839   4026023[39]9821702   -259037[14]4397178  1 <B 42590374[13]4397288 52 3 5 3 1
== Executing PPA-CTR 13 (once), V(1)=2590374[13]4397287
2072299[14]5177862   4026023[39]6205465   -259037[14]4397181  1 <B 4 52590374[13]4397295 1
== Executing  PA-CTR  1, V(1)=2590374[13]4397292, V(2)=0, repcount=1295187[13]2198647, factor=3/2
3108449[14]2767038   9058553[39]5289174   -388556[14]6595828  1 <B 43885561[13]6595942 5 1
== Executing PPA-CTR  8 (once), V(1)=3885561[13]6595940
3108449[14]2767054   9058553[39]8481073   -388556[14]6595829  1 <B 4 53885561[13]6595943 1 4 1
== Executing  PA-CTR  2, V(1)=3885561[13]6595940, V(2)=0, repcount=1942780[13]3297971, factor=3/2
4662673[14]9150822   2038174[40]6419422   -582834[14]9893800  1 <B 45828342[13]9893914 5 1 4 1
== Executing PPA-CTR  3 (once), V(1)=5828342[13]9893912
4662673[14]9150844   2038174[40]6207271   -582834[14]9893801  1 <B 4 55828342[13]9893915 1 42 1
== Executing  PA-CTR  2, V(1)=5828342[13]9893912, V(2)=0, repcount=2914171[13]9946957, factor=3/2
6994010[14]8726500   4585892[40]6568560   -874251[14]9840758  1 <B 48742513[13]9840872 5 1 42 1
== Executing PPA-CTR 14 (once), V(1)=8742513[13]9840870
6994010[14]8726522   4585892[40]6250329   -874251[14]9840759  1 <B 4 58742513[13]9840873 3 43 1
== Executing  PA-CTR  2, V(1)=8742513[13]9840870, V(2)=0, repcount=4371256[13]9920436, factor=3/2
1049101[15]8090010   1031825[41]7063233   -131137[15]9761195  1 <B 41311377[14]9761309 5 3 43 1
== Executing PPA-CTR 15 (once), V(1)=1311377[14]9761308
1049101[15]8090018   1031825[41]6585858   -131137[15]9761196  1 <B 4 51311377[14]9761311 43 1
== Executing  PA-CTR  5, V(1)=1311377[14]9761308, V(2)=0, repcount=6556885[13]4880655, factor=3/2
1573652[15]7135258   2321608[41]5556863   -196706[15]4641851  1 <B 41967065[14]4641966 5 43 1
1573652[15]7135259   2321608[41]5556864   -196706[15]4641850  2 B> 41967065[14]4641966 5 43 1
1573652[15]7135260   2321608[41]0198830                  116  2 31967065[14]4641966 B> 5 43 1
1573652[15]7135261   2321608[41]0198831                  117  2 31967065[14]4641967 A> 43 1
1573652[15]7135262   2321608[41]0198832                  118  2 31967065[14]4641967 1 H> 42 1
1573652[15]7135262   2321608[41]0198832                  118  2 31967065[14]4641967 1 H> 42 1   [stop]

Lines:       641
Top steps:   639
Macro steps: 15736524687484606059477135262
Basic steps: 2321608211623241985057171728803384730914423909950198832
Tape index:  118
nonzeros:    1967065585935575757434641972
log10(nonzeros):   27.294
log10(steps   ):   54.366
Run state:   stop

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-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 6
    T 2-state 6-symbol #d (T.J. & S. Ligocki)
    : >1.9x10^27 >2.3x10^54
    5T  1RB 0RB 3LA 5LA 1RH 4LB  1LA 2RB 3LA 4LB 3RB 3RA
    L 22
    M	650
    pref	sim
    machv Lig26_d  	just simple
    machv Lig26_d-r	with repetitions reduced
    machv Lig26_d-1	with tape symbol exponents
    machv Lig26_d-m	as 1-macro machine
    machv Lig26_d-a	as 1-macro machine with pure additive config-TRs
    iam	Lig26_d-a
    mtype	1
    mmtyp	3
    r	1
    H	1
    mac	0
    E	2
    sympr	
    HM	1
    date	Tue Jul  6 22:13:16 CEST 2010
    edate	Tue Jul  6 22:13:19 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:13:16 CEST 2010
Ready: Tue Jul 6 22:13:19 CEST 2010