2-state 5-symbol #k from T.J. & S. Ligocki

Comment: This TM produces >9.3x10^30 nonzeros in >5.2x10^61 steps.

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

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

Steps             BasSteps              BasTpos  Tape contents
    0                    0                    0  (0)A>
    1                    1                    1  (1)B>
    2                    3                   -1  <A(2)
    3                    5                    1  1 (3)B>
    4                    7                   -1  1 <B(1)
    5                    9                    1  2 (2)B>
    6                   12                    2  2 4 (1)B>
    7                   14                    0  2 4 <A(2)
    8                   15                   -1  2 <A(2) 2
    9                   17                    1  4 (4)A> 2
   10                   18                    2  42 (4)A>
   11                   19                    3  43 (1)B>
   12                   21                    1  43 <A(2)
   13                   24                   -2  <A(2) 23
   14                   26                    0  1 (3)B> 23
   15                   29                    3  1 33 (3)B>
   16                   31                    1  1 33 <B(1)
   17                   35                    3  1 32 4 (4)A>
   18                   36                    4  1 32 42 (1)B>
   19                   38                    2  1 32 42 <A(2)
   20                   40                    0  1 32 <A(2) 22
   21                   41                   -1  1 3 <B(1) 23
   22                   45                    1  1 4 (4)A> 23
   23                   48                    4  1 44 (4)A>
   24                   49                    5  1 45 (1)B>
   25                   51                    3  1 45 <A(2)
   26                   56                   -2  1 <A(2) 25
   27                   57                   -3  <A(2) 26
   28                   59                   -1  1 (3)B> 26
   29                   65                    5  1 36 (3)B>
   30                   67                    3  1 36 <B(1)
   31                   71                    5  1 35 4 (4)A>
   32                   72                    6  1 35 42 (1)B>
   33                   74                    4  1 35 42 <A(2)
   34                   76                    2  1 35 <A(2) 22
   35                   77                    1  1 34 <B(1) 23
   36                   81                    3  1 33 4 (4)A> 23
   37                   84                    6  1 33 44 (4)A>
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  [*]* 33+V(2) 41+V(1) (4)A>
    1                    1                    1  [*]* 33+V(2) 42+V(1) (1)B>
    2                    3                   -1  [*]* 33+V(2) 42+V(1) <A(2)
    3               5+V(1)           -3+-1*V(1)  [*]* 33+V(2) <A(2) 22+V(1)
    4               6+V(1)           -4+-1*V(1)  [*]* 32+V(2) <B(1) 23+V(1)
    5              10+V(1)           -2+-1*V(1)  [*]* 31+V(2) 4 (4)A> 23+V(1)
    6            13+2*V(1)                    1  [*]* 31+V(2) 44+V(1) (4)A>
<< Success! ==> defined new CTR 1 (PA)
   37                   84                    6  1 33 44 (4)A>
== Executing  PA-CTR  1, V(1)=3, V(2)=0, repcount=1, factor=3/2
   43                  103                    7  1 3 47 (4)A>
   44                  104                    8  1 3 48 (1)B>
   45                  106                    6  1 3 48 <A(2)
   46                  114                   -2  1 3 <A(2) 28
   47                  115                   -3  1 <B(1) 29
   48                  117                   -1  2 (2)B> 29
   49                  118                    0  22 (3)B> 28
   50                  126                    8  22 38 (3)B>
   51                  128                    6  22 38 <B(1)
   52                  132                    8  22 37 4 (4)A>
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  1 3 43+V(1) (4)A>
    1                    1                    1  1 3 44+V(1) (1)B>
    2                    3                   -1  1 3 44+V(1) <A(2)
    3               7+V(1)           -5+-1*V(1)  1 3 <A(2) 24+V(1)
    4               8+V(1)           -6+-1*V(1)  1 <B(1) 25+V(1)
    5              10+V(1)           -4+-1*V(1)  2 (2)B> 25+V(1)
    6              11+V(1)           -3+-1*V(1)  22 (3)B> 24+V(1)
    7            15+2*V(1)                    1  22 34+V(1) (3)B>
    8            17+2*V(1)                   -1  22 34+V(1) <B(1)
    9            21+2*V(1)                    1  22 33+V(1) 4 (4)A>
<< Success! ==> defined new CTR 2 (PPA)
   52                  132                    8  22 37 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=4, repcount=3, factor=3/2
   70                  189                   11  22 3 410 (4)A>
   71                  190                   12  22 3 411 (1)B>
   72                  192                   10  22 3 411 <A(2)
   73                  203                   -1  22 3 <A(2) 211
   74                  204                   -2  22 <B(1) 212
   75                  206                    0  2 3 (2)B> 212
   76                  207                    1  2 3 2 (3)B> 211
   77                  218                   12  2 3 2 311 (3)B>
   78                  220                   10  2 3 2 311 <B(1)
   79                  224                   12  2 3 2 310 4 (4)A>
   80                  225                   13  2 3 2 310 42 (1)B>
   81                  227                   11  2 3 2 310 42 <A(2)
   82                  229                    9  2 3 2 310 <A(2) 22
   83                  230                    8  2 3 2 39 <B(1) 23
   84                  234                   10  2 3 2 38 4 (4)A> 23
   85                  237                   13  2 3 2 38 44 (4)A>
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  [*]* [*]* [*]* 33+V(2) 41+V(1) (4)A>
    1                    1                    1  [*]* [*]* [*]* 33+V(2) 42+V(1) (1)B>
    2                    3                   -1  [*]* [*]* [*]* 33+V(2) 42+V(1) <A(2)
    3               5+V(1)           -3+-1*V(1)  [*]* [*]* [*]* 33+V(2) <A(2) 22+V(1)
    4               6+V(1)           -4+-1*V(1)  [*]* [*]* [*]* 32+V(2) <B(1) 23+V(1)
    5              10+V(1)           -2+-1*V(1)  [*]* [*]* [*]* 31+V(2) 4 (4)A> 23+V(1)
    6            13+2*V(1)                    1  [*]* [*]* [*]* 31+V(2) 44+V(1) (4)A>
<< Success! ==> defined new CTR 3 (PA)
   85                  237                   13  2 3 2 38 44 (4)A>
== Executing  PA-CTR  3, V(1)=3, V(2)=5, repcount=3, factor=3/2
  103                  312                   16  2 3 2 32 413 (4)A>
  104                  313                   17  2 3 2 32 414 (1)B>
  105                  315                   15  2 3 2 32 414 <A(2)
  106                  329                    1  2 3 2 32 <A(2) 214
  107                  330                    0  2 3 2 3 <B(1) 215
  108                  334                    2  2 3 2 4 (4)A> 215
  109                  349                   17  2 3 2 416 (4)A>
  110                  350                   18  2 3 2 417 (1)B>
  111                  352                   16  2 3 2 417 <A(2)
  112                  369                   -1  2 3 2 <A(2) 217
  113                  371                    1  2 3 4 (4)A> 217
  114                  388                   18  2 3 418 (4)A>
  115                  389                   19  2 3 419 (1)B>
  116                  391                   17  2 3 419 <A(2)
  117                  410                   -2  2 3 <A(2) 219
  118                  411                   -3  2 <B(1) 220
  119                  413                   -1  3 (2)B> 220
  120                  414                    0  3 2 (3)B> 219
  121                  433                   19  3 2 319 (3)B>
  122                  435                   17  3 2 319 <B(1)
  123                  439                   19  3 2 318 4 (4)A>
  124                  440                   20  3 2 318 42 (1)B>
  125                  442                   18  3 2 318 42 <A(2)
  126                  444                   16  3 2 318 <A(2) 22
  127                  445                   15  3 2 317 <B(1) 23
  128                  449                   17  3 2 316 4 (4)A> 23
  129                  452                   20  3 2 316 44 (4)A>
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  [*]* [*]* 33+V(2) 41+V(1) (4)A>
    1                    1                    1  [*]* [*]* 33+V(2) 42+V(1) (1)B>
    2                    3                   -1  [*]* [*]* 33+V(2) 42+V(1) <A(2)
    3               5+V(1)           -3+-1*V(1)  [*]* [*]* 33+V(2) <A(2) 22+V(1)
    4               6+V(1)           -4+-1*V(1)  [*]* [*]* 32+V(2) <B(1) 23+V(1)
    5              10+V(1)           -2+-1*V(1)  [*]* [*]* 31+V(2) 4 (4)A> 23+V(1)
    6            13+2*V(1)                    1  [*]* [*]* 31+V(2) 44+V(1) (4)A>
<< Success! ==> defined new CTR 4 (PA)
  129                  452                   20  3 2 316 44 (4)A>
== Executing  PA-CTR  4, V(1)=3, V(2)=13, repcount=7, factor=3/2
  171                  711                   27  3 2 32 425 (4)A>
  172                  712                   28  3 2 32 426 (1)B>
  173                  714                   26  3 2 32 426 <A(2)
  174                  740                    0  3 2 32 <A(2) 226
  175                  741                   -1  3 2 3 <B(1) 227
  176                  745                    1  3 2 4 (4)A> 227
  177                  772                   28  3 2 428 (4)A>
  178                  773                   29  3 2 429 (1)B>
  179                  775                   27  3 2 429 <A(2)
  180                  804                   -2  3 2 <A(2) 229
  181                  806                    0  3 4 (4)A> 229
  182                  835                   29  3 430 (4)A>
  183                  836                   30  3 431 (1)B>
  184                  838                   28  3 431 <A(2)
  185                  869                   -3  3 <A(2) 231
  186                  870                   -4  <B(1) 232
  187                  871                   -5  <A(0) 1 232
  188                  874                   -6  <A(2) 0 1 232
  189                  876                   -4  1 (3)B> 0 1 232
  190                  878                   -6  1 <B(1) 0 1 232
  191                  880                   -4  2 (2)B> 0 1 232
  192                  883                   -3  2 4 (1)B> 1 232
  193                  884                   -2  2 4 1 (2)B> 232
  194                  885                   -1  2 4 1 2 (3)B> 231
  195                  916                   30  2 4 1 2 331 (3)B>
  196                  918                   28  2 4 1 2 331 <B(1)
  197                  922                   30  2 4 1 2 330 4 (4)A>
  198                  923                   31  2 4 1 2 330 42 (1)B>
  199                  925                   29  2 4 1 2 330 42 <A(2)
  200                  927                   27  2 4 1 2 330 <A(2) 22
  201                  928                   26  2 4 1 2 329 <B(1) 23
  202                  932                   28  2 4 1 2 328 4 (4)A> 23
  203                  935                   31  2 4 1 2 328 44 (4)A>
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  [*]* [*]* [*]* [*]* 33+V(2) 41+V(1) (4)A>
    1                    1                    1  [*]* [*]* [*]* [*]* 33+V(2) 42+V(1) (1)B>
    2                    3                   -1  [*]* [*]* [*]* [*]* 33+V(2) 42+V(1) <A(2)
    3               5+V(1)           -3+-1*V(1)  [*]* [*]* [*]* [*]* 33+V(2) <A(2) 22+V(1)
    4               6+V(1)           -4+-1*V(1)  [*]* [*]* [*]* [*]* 32+V(2) <B(1) 23+V(1)
    5              10+V(1)           -2+-1*V(1)  [*]* [*]* [*]* [*]* 31+V(2) 4 (4)A> 23+V(1)
    6            13+2*V(1)                    1  [*]* [*]* [*]* [*]* 31+V(2) 44+V(1) (4)A>
<< Success! ==> defined new CTR 5 (PA)
  203                  935                   31  2 4 1 2 328 44 (4)A>
== Executing  PA-CTR  5, V(1)=3, V(2)=25, repcount=13, factor=3/2
  281                 1650                   44  2 4 1 2 32 443 (4)A>
  282                 1651                   45  2 4 1 2 32 444 (1)B>
  283                 1653                   43  2 4 1 2 32 444 <A(2)
  284                 1697                   -1  2 4 1 2 32 <A(2) 244
  285                 1698                   -2  2 4 1 2 3 <B(1) 245
  286                 1702                    0  2 4 1 2 4 (4)A> 245
  287                 1747                   45  2 4 1 2 446 (4)A>
  288                 1748                   46  2 4 1 2 447 (1)B>
  289                 1750                   44  2 4 1 2 447 <A(2)
  290                 1797                   -3  2 4 1 2 <A(2) 247
  291                 1799                   -1  2 4 1 4 (4)A> 247
  292                 1846                   46  2 4 1 448 (4)A>
  293                 1847                   47  2 4 1 449 (1)B>
  294                 1849                   45  2 4 1 449 <A(2)
  295                 1898                   -4  2 4 1 <A(2) 249
  296                 1899                   -5  2 4 <A(2) 250
  297                 1900                   -6  2 <A(2) 251
  298                 1902                   -4  4 (4)A> 251
  299                 1953                   47  452 (4)A>
  300                 1954                   48  453 (1)B>
  301                 1956                   46  453 <A(2)
  302                 2009                   -7  <A(2) 253
  303                 2011                   -5  1 (3)B> 253
  304                 2064                   48  1 353 (3)B>
  305                 2066                   46  1 353 <B(1)
  306                 2070                   48  1 352 4 (4)A>
>> Try to prove a PPA-CTR with 3 Vars...
    0                    0                    0  2 41+V(3) 11+V(2) 2 32 41+V(1) (4)A>
    1                    1                    1  2 41+V(3) 11+V(2) 2 32 42+V(1) (1)B>
    2                    3                   -1  2 41+V(3) 11+V(2) 2 32 42+V(1) <A(2)
    3               5+V(1)           -3+-1*V(1)  2 41+V(3) 11+V(2) 2 32 <A(2) 22+V(1)
    4               6+V(1)           -4+-1*V(1)  2 41+V(3) 11+V(2) 2 3 <B(1) 23+V(1)
    5              10+V(1)           -2+-1*V(1)  2 41+V(3) 11+V(2) 2 4 (4)A> 23+V(1)
    6            13+2*V(1)                    1  2 41+V(3) 11+V(2) 2 44+V(1) (4)A>
    7            14+2*V(1)                    2  2 41+V(3) 11+V(2) 2 45+V(1) (1)B>
    8            16+2*V(1)                    0  2 41+V(3) 11+V(2) 2 45+V(1) <A(2)
    9            21+3*V(1)           -5+-1*V(1)  2 41+V(3) 11+V(2) 2 <A(2) 25+V(1)
   10            23+3*V(1)           -3+-1*V(1)  2 41+V(3) 11+V(2) 4 (4)A> 25+V(1)
   11            28+4*V(1)                    2  2 41+V(3) 11+V(2) 46+V(1) (4)A>
   12            29+4*V(1)                    3  2 41+V(3) 11+V(2) 47+V(1) (1)B>
   13            31+4*V(1)                    1  2 41+V(3) 11+V(2) 47+V(1) <A(2)
   14            38+5*V(1)           -6+-1*V(1)  2 41+V(3) 11+V(2) <A(2) 27+V(1)
   15       39+5*V(1)+V(2)   -7+-1*V(1)+-1*V(2)  2 41+V(3) <A(2) 28+V(1)+V(2)
   16  40+5*V(1)+V(2)+V(3) -8+-1*V(1)+-1*V(2)+-1*V(3)  2 <A(2) 29+V(1)+V(2)+V(3)
   17  42+5*V(1)+V(2)+V(3) -6+-1*V(1)+-1*V(2)+-1*V(3)  4 (4)A> 29+V(1)+V(2)+V(3)
   18 51+6*V(1)+2*V(2)+2*V(3)                    3  410+V(1)+V(2)+V(3) (4)A>
   19 52+6*V(1)+2*V(2)+2*V(3)                    4  411+V(1)+V(2)+V(3) (1)B>
   20 54+6*V(1)+2*V(2)+2*V(3)                    2  411+V(1)+V(2)+V(3) <A(2)
   21 65+7*V(1)+3*V(2)+3*V(3) -9+-1*V(1)+-1*V(2)+-1*V(3)  <A(2) 211+V(1)+V(2)+V(3)
   22 67+7*V(1)+3*V(2)+3*V(3) -7+-1*V(1)+-1*V(2)+-1*V(3)  1 (3)B> 211+V(1)+V(2)+V(3)
   23 78+8*V(1)+4*V(2)+4*V(3)                    4  1 311+V(1)+V(2)+V(3) (3)B>
   24 80+8*V(1)+4*V(2)+4*V(3)                    2  1 311+V(1)+V(2)+V(3) <B(1)
   25 84+8*V(1)+4*V(2)+4*V(3)                    4  1 310+V(1)+V(2)+V(3) 4 (4)A>
<< Success! ==> defined new CTR 6 (PPA)
  306                 2070                   48  1 352 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=49, repcount=25, factor=3/2
  456                 4195                   73  1 32 476 (4)A>
  457                 4196                   74  1 32 477 (1)B>
  458                 4198                   72  1 32 477 <A(2)
  459                 4275                   -5  1 32 <A(2) 277
  460                 4276                   -6  1 3 <B(1) 278
  461                 4280                   -4  1 4 (4)A> 278
  462                 4358                   74  1 479 (4)A>
  463                 4359                   75  1 480 (1)B>
  464                 4361                   73  1 480 <A(2)
  465                 4441                   -7  1 <A(2) 280
  466                 4442                   -8  <A(2) 281
  467                 4444                   -6  1 (3)B> 281
  468                 4525                   75  1 381 (3)B>
  469                 4527                   73  1 381 <B(1)
  470                 4531                   75  1 380 4 (4)A>
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  11+V(2) 32 41+V(1) (4)A>
    1                    1                    1  11+V(2) 32 42+V(1) (1)B>
    2                    3                   -1  11+V(2) 32 42+V(1) <A(2)
    3               5+V(1)           -3+-1*V(1)  11+V(2) 32 <A(2) 22+V(1)
    4               6+V(1)           -4+-1*V(1)  11+V(2) 3 <B(1) 23+V(1)
    5              10+V(1)           -2+-1*V(1)  11+V(2) 4 (4)A> 23+V(1)
    6            13+2*V(1)                    1  11+V(2) 44+V(1) (4)A>
    7            14+2*V(1)                    2  11+V(2) 45+V(1) (1)B>
    8            16+2*V(1)                    0  11+V(2) 45+V(1) <A(2)
    9            21+3*V(1)           -5+-1*V(1)  11+V(2) <A(2) 25+V(1)
   10       22+3*V(1)+V(2)   -6+-1*V(1)+-1*V(2)  <A(2) 26+V(1)+V(2)
   11       24+3*V(1)+V(2)   -4+-1*V(1)+-1*V(2)  1 (3)B> 26+V(1)+V(2)
   12     30+4*V(1)+2*V(2)                    2  1 36+V(1)+V(2) (3)B>
   13     32+4*V(1)+2*V(2)                    0  1 36+V(1)+V(2) <B(1)
   14     36+4*V(1)+2*V(2)                    2  1 35+V(1)+V(2) 4 (4)A>
<< Success! ==> defined new CTR 7 (PPA)
  470                 4531                   75  1 380 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=77, repcount=39, factor=3/2
  704                 9484                  114  1 32 4118 (4)A>
== Executing PPA-CTR  7 (once), V(1)=117, V(2)=0
  718                 9988                  116  1 3122 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=119, repcount=60, factor=3/2
 1078                21388                  176  1 32 4181 (4)A>
== Executing PPA-CTR  7 (once), V(1)=180, V(2)=0
 1092                22144                  178  1 3185 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=182, repcount=92, factor=3/2
 1644                48456                  270  1 3 4277 (4)A>
== Executing PPA-CTR  2 (once), V(1)=274
 1653                49025                  271  22 3277 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=274, repcount=138, factor=3/2
 2481               107537                  409  22 3 4415 (4)A>
 2482               107538                  410  22 3 4416 (1)B>
 2483               107540                  408  22 3 4416 <A(2)
 2484               107956                   -8  22 3 <A(2) 2416
 2485               107957                   -9  22 <B(1) 2417
 2486               107959                   -7  2 3 (2)B> 2417
 2487               107960                   -6  2 3 2 (3)B> 2416
 2488               108376                  410  2 3 2 3416 (3)B>
 2489               108378                  408  2 3 2 3416 <B(1)
 2490               108382                  410  2 3 2 3415 4 (4)A>
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  22+V(2) 3 43+V(1) (4)A>
    1                    1                    1  22+V(2) 3 44+V(1) (1)B>
    2                    3                   -1  22+V(2) 3 44+V(1) <A(2)
    3               7+V(1)           -5+-1*V(1)  22+V(2) 3 <A(2) 24+V(1)
    4               8+V(1)           -6+-1*V(1)  22+V(2) <B(1) 25+V(1)
    5              10+V(1)           -4+-1*V(1)  21+V(2) 3 (2)B> 25+V(1)
    6              11+V(1)           -3+-1*V(1)  21+V(2) 3 2 (3)B> 24+V(1)
    7            15+2*V(1)                    1  21+V(2) 3 2 34+V(1) (3)B>
    8            17+2*V(1)                   -1  21+V(2) 3 2 34+V(1) <B(1)
    9            21+2*V(1)                    1  21+V(2) 3 2 33+V(1) 4 (4)A>
<< Success! ==> defined new CTR 8 (PPA)
 2490               108382                  410  2 3 2 3415 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=412, repcount=207, factor=3/2
 3732               238999                  617  2 3 2 3 4622 (4)A>
 3733               239000                  618  2 3 2 3 4623 (1)B>
 3734               239002                  616  2 3 2 3 4623 <A(2)
 3735               239625                   -7  2 3 2 3 <A(2) 2623
 3736               239626                   -8  2 3 2 <B(1) 2624
 3737               239628                   -6  2 32 (2)B> 2624
 3738               239629                   -5  2 32 2 (3)B> 2623
 3739               240252                  618  2 32 2 3623 (3)B>
 3740               240254                  616  2 32 2 3623 <B(1)
 3741               240258                  618  2 32 2 3622 4 (4)A>
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  [*]* 31+V(2) 2 3 43+V(1) (4)A>
    1                    1                    1  [*]* 31+V(2) 2 3 44+V(1) (1)B>
    2                    3                   -1  [*]* 31+V(2) 2 3 44+V(1) <A(2)
    3               7+V(1)           -5+-1*V(1)  [*]* 31+V(2) 2 3 <A(2) 24+V(1)
    4               8+V(1)           -6+-1*V(1)  [*]* 31+V(2) 2 <B(1) 25+V(1)
    5              10+V(1)           -4+-1*V(1)  [*]* 32+V(2) (2)B> 25+V(1)
    6              11+V(1)           -3+-1*V(1)  [*]* 32+V(2) 2 (3)B> 24+V(1)
    7            15+2*V(1)                    1  [*]* 32+V(2) 2 34+V(1) (3)B>
    8            17+2*V(1)                   -1  [*]* 32+V(2) 2 34+V(1) <B(1)
    9            21+2*V(1)                    1  [*]* 32+V(2) 2 33+V(1) 4 (4)A>
<< Success! ==> defined new CTR 9 (PPA)
 3741               240258                  618  2 32 2 3622 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=619, repcount=310, factor=3/2
 5601               531658                  928  2 32 2 32 4931 (4)A>
 5602               531659                  929  2 32 2 32 4932 (1)B>
 5603               531661                  927  2 32 2 32 4932 <A(2)
 5604               532593                   -5  2 32 2 32 <A(2) 2932
 5605               532594                   -6  2 32 2 3 <B(1) 2933
 5606               532598                   -4  2 32 2 4 (4)A> 2933
 5607               533531                  929  2 32 2 4934 (4)A>
 5608               533532                  930  2 32 2 4935 (1)B>
 5609               533534                  928  2 32 2 4935 <A(2)
 5610               534469                   -7  2 32 2 <A(2) 2935
 5611               534471                   -5  2 32 4 (4)A> 2935
 5612               535406                  930  2 32 4936 (4)A>
 5613               535407                  931  2 32 4937 (1)B>
 5614               535409                  929  2 32 4937 <A(2)
 5615               536346                   -8  2 32 <A(2) 2937
 5616               536347                   -9  2 3 <B(1) 2938
 5617               536351                   -7  2 4 (4)A> 2938
 5618               537289                  931  2 4939 (4)A>
 5619               537290                  932  2 4940 (1)B>
 5620               537292                  930  2 4940 <A(2)
 5621               538232                  -10  2 <A(2) 2940
 5622               538234                   -8  4 (4)A> 2940
 5623               539174                  932  4941 (4)A>
 5624               539175                  933  4942 (1)B>
 5625               539177                  931  4942 <A(2)
 5626               540119                  -11  <A(2) 2942
 5627               540121                   -9  1 (3)B> 2942
 5628               541063                  933  1 3942 (3)B>
 5629               541065                  931  1 3942 <B(1)
 5630               541069                  933  1 3941 4 (4)A>
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  2 32 2 32 41+V(1) (4)A>
    1                    1                    1  2 32 2 32 42+V(1) (1)B>
    2                    3                   -1  2 32 2 32 42+V(1) <A(2)
    3               5+V(1)           -3+-1*V(1)  2 32 2 32 <A(2) 22+V(1)
    4               6+V(1)           -4+-1*V(1)  2 32 2 3 <B(1) 23+V(1)
    5              10+V(1)           -2+-1*V(1)  2 32 2 4 (4)A> 23+V(1)
    6            13+2*V(1)                    1  2 32 2 44+V(1) (4)A>
    7            14+2*V(1)                    2  2 32 2 45+V(1) (1)B>
    8            16+2*V(1)                    0  2 32 2 45+V(1) <A(2)
    9            21+3*V(1)           -5+-1*V(1)  2 32 2 <A(2) 25+V(1)
   10            23+3*V(1)           -3+-1*V(1)  2 32 4 (4)A> 25+V(1)
   11            28+4*V(1)                    2  2 32 46+V(1) (4)A>
   12            29+4*V(1)                    3  2 32 47+V(1) (1)B>
   13            31+4*V(1)                    1  2 32 47+V(1) <A(2)
   14            38+5*V(1)           -6+-1*V(1)  2 32 <A(2) 27+V(1)
   15            39+5*V(1)           -7+-1*V(1)  2 3 <B(1) 28+V(1)
   16            43+5*V(1)           -5+-1*V(1)  2 4 (4)A> 28+V(1)
   17            51+6*V(1)                    3  2 49+V(1) (4)A>
   18            52+6*V(1)                    4  2 410+V(1) (1)B>
   19            54+6*V(1)                    2  2 410+V(1) <A(2)
   20            64+7*V(1)           -8+-1*V(1)  2 <A(2) 210+V(1)
   21            66+7*V(1)           -6+-1*V(1)  4 (4)A> 210+V(1)
   22            76+8*V(1)                    4  411+V(1) (4)A>
   23            77+8*V(1)                    5  412+V(1) (1)B>
   24            79+8*V(1)                    3  412+V(1) <A(2)
   25            91+9*V(1)           -9+-1*V(1)  <A(2) 212+V(1)
   26            93+9*V(1)           -7+-1*V(1)  1 (3)B> 212+V(1)
   27          105+10*V(1)                    5  1 312+V(1) (3)B>
   28          107+10*V(1)                    3  1 312+V(1) <B(1)
   29          111+10*V(1)                    5  1 311+V(1) 4 (4)A>
<< Success! ==> defined new CTR 10 (PPA)
 5630               541069                  933  1 3941 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=938, repcount=470, factor=3/2
 8450              1208469                 1403  1 3 41411 (4)A>
== Executing PPA-CTR  2 (once), V(1)=1408
 8459              1211306                 1404  22 31411 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=1408, repcount=705, factor=3/2
12689              2709431                 2109  22 3 42116 (4)A>
== Executing PPA-CTR  8 (once), V(1)=2113, V(2)=0
12698              2713678                 2110  2 3 2 32116 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=2113, repcount=1057, factor=3/2
19040              6075995                 3167  2 3 2 32 43172 (4)A>
19041              6075996                 3168  2 3 2 32 43173 (1)B>
19042              6075998                 3166  2 3 2 32 43173 <A(2)
19043              6079171                   -7  2 3 2 32 <A(2) 23173
19044              6079172                   -8  2 3 2 3 <B(1) 23174
19045              6079176                   -6  2 3 2 4 (4)A> 23174
19046              6082350                 3168  2 3 2 43175 (4)A>
19047              6082351                 3169  2 3 2 43176 (1)B>
19048              6082353                 3167  2 3 2 43176 <A(2)
19049              6085529                   -9  2 3 2 <A(2) 23176
19050              6085531                   -7  2 3 4 (4)A> 23176
19051              6088707                 3169  2 3 43177 (4)A>
19052              6088708                 3170  2 3 43178 (1)B>
19053              6088710                 3168  2 3 43178 <A(2)
19054              6091888                  -10  2 3 <A(2) 23178
19055              6091889                  -11  2 <B(1) 23179
19056              6091891                   -9  3 (2)B> 23179
19057              6091892                   -8  3 2 (3)B> 23178
19058              6095070                 3170  3 2 33178 (3)B>
19059              6095072                 3168  3 2 33178 <B(1)
19060              6095076                 3170  3 2 33177 4 (4)A>
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  2 3 2 32 41+V(1) (4)A>
    1                    1                    1  2 3 2 32 42+V(1) (1)B>
    2                    3                   -1  2 3 2 32 42+V(1) <A(2)
    3               5+V(1)           -3+-1*V(1)  2 3 2 32 <A(2) 22+V(1)
    4               6+V(1)           -4+-1*V(1)  2 3 2 3 <B(1) 23+V(1)
    5              10+V(1)           -2+-1*V(1)  2 3 2 4 (4)A> 23+V(1)
    6            13+2*V(1)                    1  2 3 2 44+V(1) (4)A>
    7            14+2*V(1)                    2  2 3 2 45+V(1) (1)B>
    8            16+2*V(1)                    0  2 3 2 45+V(1) <A(2)
    9            21+3*V(1)           -5+-1*V(1)  2 3 2 <A(2) 25+V(1)
   10            23+3*V(1)           -3+-1*V(1)  2 3 4 (4)A> 25+V(1)
   11            28+4*V(1)                    2  2 3 46+V(1) (4)A>
   12            29+4*V(1)                    3  2 3 47+V(1) (1)B>
   13            31+4*V(1)                    1  2 3 47+V(1) <A(2)
   14            38+5*V(1)           -6+-1*V(1)  2 3 <A(2) 27+V(1)
   15            39+5*V(1)           -7+-1*V(1)  2 <B(1) 28+V(1)
   16            41+5*V(1)           -5+-1*V(1)  3 (2)B> 28+V(1)
   17            42+5*V(1)           -4+-1*V(1)  3 2 (3)B> 27+V(1)
   18            49+6*V(1)                    3  3 2 37+V(1) (3)B>
   19            51+6*V(1)                    1  3 2 37+V(1) <B(1)
   20            55+6*V(1)                    3  3 2 36+V(1) 4 (4)A>
<< Success! ==> defined new CTR 11 (PPA)
19060              6095076                 3170  3 2 33177 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=3174, repcount=1588, factor=3/2
28588             13676188                 4758  3 2 3 44765 (4)A>
28589             13676189                 4759  3 2 3 44766 (1)B>
28590             13676191                 4757  3 2 3 44766 <A(2)
28591             13680957                   -9  3 2 3 <A(2) 24766
28592             13680958                  -10  3 2 <B(1) 24767
28593             13680960                   -8  32 (2)B> 24767
28594             13680961                   -7  32 2 (3)B> 24766
28595             13685727                 4759  32 2 34766 (3)B>
28596             13685729                 4757  32 2 34766 <B(1)
28597             13685733                 4759  32 2 34765 4 (4)A>
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  31+V(2) 2 3 43+V(1) (4)A>
    1                    1                    1  31+V(2) 2 3 44+V(1) (1)B>
    2                    3                   -1  31+V(2) 2 3 44+V(1) <A(2)
    3               7+V(1)           -5+-1*V(1)  31+V(2) 2 3 <A(2) 24+V(1)
    4               8+V(1)           -6+-1*V(1)  31+V(2) 2 <B(1) 25+V(1)
    5              10+V(1)           -4+-1*V(1)  32+V(2) (2)B> 25+V(1)
    6              11+V(1)           -3+-1*V(1)  32+V(2) 2 (3)B> 24+V(1)
    7            15+2*V(1)                    1  32+V(2) 2 34+V(1) (3)B>
    8            17+2*V(1)                   -1  32+V(2) 2 34+V(1) <B(1)
    9            21+2*V(1)                    1  32+V(2) 2 33+V(1) 4 (4)A>
<< Success! ==> defined new CTR 12 (PPA)
28597             13685733                 4759  32 2 34765 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=4762, repcount=2382, factor=3/2
42889             30731325                 7141  32 2 3 47147 (4)A>
== Executing PPA-CTR 12 (once), V(1)=7144, V(2)=1
42898             30745634                 7142  33 2 37147 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=7144, repcount=3573, factor=3/2
64336             69080351                10715  33 2 3 410720 (4)A>
== Executing PPA-CTR 12 (once), V(1)=10717, V(2)=2
64345             69101806                10716  34 2 310720 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=10717, repcount=5359, factor=3/2
96499            155312039                16075  34 2 32 416078 (4)A>
96500            155312040                16076  34 2 32 416079 (1)B>
96501            155312042                16074  34 2 32 416079 <A(2)
96502            155328121                   -5  34 2 32 <A(2) 216079
96503            155328122                   -6  34 2 3 <B(1) 216080
96504            155328126                   -4  34 2 4 (4)A> 216080
96505            155344206                16076  34 2 416081 (4)A>
96506            155344207                16077  34 2 416082 (1)B>
96507            155344209                16075  34 2 416082 <A(2)
96508            155360291                   -7  34 2 <A(2) 216082
96509            155360293                   -5  34 4 (4)A> 216082
96510            155376375                16077  34 416083 (4)A>
96511            155376376                16078  34 416084 (1)B>
96512            155376378                16076  34 416084 <A(2)
96513            155392462                   -8  34 <A(2) 216084
96514            155392463                   -9  33 <B(1) 216085
96515            155392467                   -7  32 4 (4)A> 216085
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  33+V(1) 4 (4)A> 21+V(2)
    1               1+V(2)               1+V(2)  33+V(1) 42+V(2) (4)A>
    2               2+V(2)               2+V(2)  33+V(1) 43+V(2) (1)B>
    3               4+V(2)               0+V(2)  33+V(1) 43+V(2) <A(2)
    4             7+2*V(2)                   -3  33+V(1) <A(2) 23+V(2)
    5             8+2*V(2)                   -4  32+V(1) <B(1) 24+V(2)
    6            12+2*V(2)                   -2  31+V(1) 4 (4)A> 24+V(2)
<< Success! ==> defined new CTR 13 (PA)
96516            155408552                16078  32 416086 (4)A>
96517            155408553                16079  32 416087 (1)B>
96518            155408555                16077  32 416087 <A(2)
96519            155424642                  -10  32 <A(2) 216087
96520            155424643                  -11  3 <B(1) 216088
96521            155424647                   -9  4 (4)A> 216088
96522            155440735                16079  416089 (4)A>
96523            155440736                16080  416090 (1)B>
96524            155440738                16078  416090 <A(2)
96525            155456828                  -12  <A(2) 216090
96526            155456830                  -10  1 (3)B> 216090
96527            155472920                16080  1 316090 (3)B>
96528            155472922                16078  1 316090 <B(1)
96529            155472926                16080  1 316089 4 (4)A>
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  32 41+V(1) (4)A> 21+V(2)
    1               1+V(2)               1+V(2)  32 42+V(1)+V(2) (4)A>
    2               2+V(2)               2+V(2)  32 43+V(1)+V(2) (1)B>
    3               4+V(2)               0+V(2)  32 43+V(1)+V(2) <A(2)
    4        7+V(1)+2*V(2)           -3+-1*V(1)  32 <A(2) 23+V(1)+V(2)
    5        8+V(1)+2*V(2)           -4+-1*V(1)  3 <B(1) 24+V(1)+V(2)
    6       12+V(1)+2*V(2)           -2+-1*V(1)  4 (4)A> 24+V(1)+V(2)
    7     16+2*V(1)+3*V(2)               2+V(2)  45+V(1)+V(2) (4)A>
    8     17+2*V(1)+3*V(2)               3+V(2)  46+V(1)+V(2) (1)B>
    9     19+2*V(1)+3*V(2)               1+V(2)  46+V(1)+V(2) <A(2)
   10     25+3*V(1)+4*V(2)           -5+-1*V(1)  <A(2) 26+V(1)+V(2)
   11     27+3*V(1)+4*V(2)           -3+-1*V(1)  1 (3)B> 26+V(1)+V(2)
   12     33+4*V(1)+5*V(2)               3+V(2)  1 36+V(1)+V(2) (3)B>
   13     35+4*V(1)+5*V(2)               1+V(2)  1 36+V(1)+V(2) <B(1)
   14     39+4*V(1)+5*V(2)               3+V(2)  1 35+V(1)+V(2) 4 (4)A>
<< Success! ==> defined new CTR 14 (PPA)
96529            155472926                16080  1 316089 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=16086, repcount=8044, factor=3/2
144793            349671174                24124  1 3 424133 (4)A>
== Executing PPA-CTR  2 (once), V(1)=24130
144802            349719455                24125  22 324133 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=24130, repcount=12066, factor=3/2
217198            786605183                36191  22 3 436199 (4)A>
== Executing PPA-CTR  8 (once), V(1)=36196, V(2)=0
217207            786677596                36192  2 3 2 336199 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=36196, repcount=18099, factor=3/2
325801           1769579989                54291  2 3 2 3 454298 (4)A>
== Executing PPA-CTR  9 (once), V(1)=54295, V(2)=0
325810           1769688600                54292  2 32 2 354298 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=54295, repcount=27148, factor=3/2
488698           3981001792                81440  2 32 2 32 481445 (4)A>
== Executing PPA-CTR 10 (once), V(1)=81444
488727           3981816343                81445  1 381455 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=81452, repcount=40727, factor=3/2
733089           8958289200               122172  1 3 4122182 (4)A>
== Executing PPA-CTR  2 (once), V(1)=122179
733098           8958533579               122173  22 3122182 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=122179, repcount=61090, factor=3/2
1099638          20155108779               183263  22 32 4183271 (4)A>
1099639          20155108780               183264  22 32 4183272 (1)B>
1099640          20155108782               183262  22 32 4183272 <A(2)
1099641          20155292054                  -10  22 32 <A(2) 2183272
1099642          20155292055                  -11  22 3 <B(1) 2183273
1099643          20155292059                   -9  22 4 (4)A> 2183273
1099644          20155475332               183264  22 4183274 (4)A>
1099645          20155475333               183265  22 4183275 (1)B>
1099646          20155475335               183263  22 4183275 <A(2)
1099647          20155658610                  -12  22 <A(2) 2183275
1099648          20155658612                  -10  2 4 (4)A> 2183275
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  22+V(1) 4 (4)A> 21+V(2)
    1               1+V(2)               1+V(2)  22+V(1) 42+V(2) (4)A>
    2               2+V(2)               2+V(2)  22+V(1) 43+V(2) (1)B>
    3               4+V(2)               0+V(2)  22+V(1) 43+V(2) <A(2)
    4             7+2*V(2)                   -3  22+V(1) <A(2) 23+V(2)
    5             9+2*V(2)                   -1  21+V(1) 4 (4)A> 23+V(2)
<< Success! ==> defined new CTR 15 (PA)
1099649          20155841887               183265  2 4183276 (4)A>
1099650          20155841888               183266  2 4183277 (1)B>
1099651          20155841890               183264  2 4183277 <A(2)
1099652          20156025167                  -13  2 <A(2) 2183277
1099653          20156025169                  -11  4 (4)A> 2183277
1099654          20156208446               183266  4183278 (4)A>
1099655          20156208447               183267  4183279 (1)B>
1099656          20156208449               183265  4183279 <A(2)
1099657          20156391728                  -14  <A(2) 2183279
1099658          20156391730                  -12  1 (3)B> 2183279
1099659          20156575009               183267  1 3183279 (3)B>
1099660          20156575011               183265  1 3183279 <B(1)
1099661          20156575015               183267  1 3183278 4 (4)A>
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  2 41+V(1) (4)A> 21+V(2)
    1               1+V(2)               1+V(2)  2 42+V(1)+V(2) (4)A>
    2               2+V(2)               2+V(2)  2 43+V(1)+V(2) (1)B>
    3               4+V(2)               0+V(2)  2 43+V(1)+V(2) <A(2)
    4        7+V(1)+2*V(2)           -3+-1*V(1)  2 <A(2) 23+V(1)+V(2)
    5        9+V(1)+2*V(2)           -1+-1*V(1)  4 (4)A> 23+V(1)+V(2)
    6     12+2*V(1)+3*V(2)               2+V(2)  44+V(1)+V(2) (4)A>
    7     13+2*V(1)+3*V(2)               3+V(2)  45+V(1)+V(2) (1)B>
    8     15+2*V(1)+3*V(2)               1+V(2)  45+V(1)+V(2) <A(2)
    9     20+3*V(1)+4*V(2)           -4+-1*V(1)  <A(2) 25+V(1)+V(2)
   10     22+3*V(1)+4*V(2)           -2+-1*V(1)  1 (3)B> 25+V(1)+V(2)
   11     27+4*V(1)+5*V(2)               3+V(2)  1 35+V(1)+V(2) (3)B>
   12     29+4*V(1)+5*V(2)               1+V(2)  1 35+V(1)+V(2) <B(1)
   13     33+4*V(1)+5*V(2)               3+V(2)  1 34+V(1)+V(2) 4 (4)A>
<< Success! ==> defined new CTR 16 (PPA)
1099661          20156575015               183267  1 3183278 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=183275, repcount=91638, factor=3/2
1649489          45350060527               274905  1 32 4274915 (4)A>
== Executing PPA-CTR  7 (once), V(1)=274914, V(2)=0
1649503          45351160219               274907  1 3274919 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=274916, repcount=137459, factor=3/2
2474257         102037464852               412366  1 3 4412378 (4)A>
== Executing PPA-CTR  2 (once), V(1)=412375
2474266         102038289623               412367  22 3412378 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=412375, repcount=206188, factor=3/2
3711394         229580825535               618555  22 32 4618565 (4)A>
3711395         229580825536               618556  22 32 4618566 (1)B>
3711396         229580825538               618554  22 32 4618566 <A(2)
3711397         229581444104                  -12  22 32 <A(2) 2618566
3711398         229581444105                  -13  22 3 <B(1) 2618567
3711399         229581444109                  -11  22 4 (4)A> 2618567
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  22+V(2) 32 41+V(1) (4)A>
    1                    1                    1  22+V(2) 32 42+V(1) (1)B>
    2                    3                   -1  22+V(2) 32 42+V(1) <A(2)
    3               5+V(1)           -3+-1*V(1)  22+V(2) 32 <A(2) 22+V(1)
    4               6+V(1)           -4+-1*V(1)  22+V(2) 3 <B(1) 23+V(1)
    5              10+V(1)           -2+-1*V(1)  22+V(2) 4 (4)A> 23+V(1)
<< Success! ==> defined new CTR 17 (PPA)
3711399         229581444109                  -11  22 4 (4)A> 2618567
== Executing  PA-CTR 15, V(1)=0, V(2)=618566, repcount=1, factor=2/1
3711404         229582681250                  -12  2 4 (4)A> 2618569
== Executing PPA-CTR 16 (once), V(1)=0, V(2)=618568
3711417         229585774123               618559  1 3618572 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=618569, repcount=309285, factor=3/2
5567127         516560500648               927844  1 32 4927856 (4)A>
== Executing PPA-CTR  7 (once), V(1)=927855, V(2)=0
5567141         516564212104               927846  1 3927860 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=927857, repcount=463929, factor=3/2
8350715        1162259202517              1391775  1 32 41391788 (4)A>
== Executing PPA-CTR  7 (once), V(1)=1391787, V(2)=0
8350729        1162264769701              1391777  1 31391792 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=1391789, repcount=695895, factor=3/2
12526099        2615081281726              2087672  1 32 42087686 (4)A>
== Executing PPA-CTR  7 (once), V(1)=2087685, V(2)=0
12526113        2615089632502              2087674  1 32087690 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=2087687, repcount=1043844, factor=3/2
18789177        5883930959950              3131518  1 32 43131533 (4)A>
== Executing PPA-CTR  7 (once), V(1)=3131532, V(2)=0
18789191        5883943486114              3131520  1 33131537 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=3131534, repcount=1565768, factor=3/2
28183799       13238847433266              4697288  1 3 44697305 (4)A>
== Executing PPA-CTR  2 (once), V(1)=4697302
28183808       13238856827891              4697289  22 34697305 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=4697302, repcount=2348652, factor=3/2
42275720       29787378965723              7045941  22 3 47045957 (4)A>
== Executing PPA-CTR  8 (once), V(1)=7045954, V(2)=0
42275729       29787393057652              7045942  2 3 2 37045957 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=7045954, repcount=3522978, factor=3/2
63413597       67021550252884             10568920  2 3 2 3 410568935 (4)A>
== Executing PPA-CTR  9 (once), V(1)=10568932, V(2)=0
63413606       67021571390769             10568921  2 32 2 310568935 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=10568932, repcount=5284467, factor=3/2
95120408      150798398657706             15853388  2 32 2 3 415853402 (4)A>
== Executing PPA-CTR  9 (once), V(1)=15853399, V(2)=1
95120417      150798430364525             15853389  2 33 2 315853402 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=15853399, repcount=7926700, factor=3/2
142680617      339296228301525             23780089  2 33 2 32 423780101 (4)A>
142680618      339296228301526             23780090  2 33 2 32 423780102 (1)B>
142680619      339296228301528             23780088  2 33 2 32 423780102 <A(2)
142680620      339296252081630                  -14  2 33 2 32 <A(2) 223780102
142680621      339296252081631                  -15  2 33 2 3 <B(1) 223780103
142680622      339296252081635                  -13  2 33 2 4 (4)A> 223780103
142680623      339296275861738             23780090  2 33 2 423780104 (4)A>
142680624      339296275861739             23780091  2 33 2 423780105 (1)B>
142680625      339296275861741             23780089  2 33 2 423780105 <A(2)
142680626      339296299641846                  -16  2 33 2 <A(2) 223780105
142680627      339296299641848                  -14  2 33 4 (4)A> 223780105
142680628      339296323421953             23780091  2 33 423780106 (4)A>
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  [*]* 33+V(2) 2 32 41+V(1) (4)A>
    1                    1                    1  [*]* 33+V(2) 2 32 42+V(1) (1)B>
    2                    3                   -1  [*]* 33+V(2) 2 32 42+V(1) <A(2)
    3               5+V(1)           -3+-1*V(1)  [*]* 33+V(2) 2 32 <A(2) 22+V(1)
    4               6+V(1)           -4+-1*V(1)  [*]* 33+V(2) 2 3 <B(1) 23+V(1)
    5              10+V(1)           -2+-1*V(1)  [*]* 33+V(2) 2 4 (4)A> 23+V(1)
    6            13+2*V(1)                    1  [*]* 33+V(2) 2 44+V(1) (4)A>
    7            14+2*V(1)                    2  [*]* 33+V(2) 2 45+V(1) (1)B>
    8            16+2*V(1)                    0  [*]* 33+V(2) 2 45+V(1) <A(2)
    9            21+3*V(1)           -5+-1*V(1)  [*]* 33+V(2) 2 <A(2) 25+V(1)
   10            23+3*V(1)           -3+-1*V(1)  [*]* 33+V(2) 4 (4)A> 25+V(1)
   11            28+4*V(1)                    2  [*]* 33+V(2) 46+V(1) (4)A>
<< Success! ==> defined new CTR 18 (PPA)
142680628      339296323421953             23780091  2 33 423780106 (4)A>
== Executing  PA-CTR  1, V(1)=23780105, V(2)=0, repcount=1, factor=3/2
142680634      339296370982176             23780092  2 3 423780109 (4)A>
142680635      339296370982177             23780093  2 3 423780110 (1)B>
142680636      339296370982179             23780091  2 3 423780110 <A(2)
142680637      339296394762289                  -19  2 3 <A(2) 223780110
142680638      339296394762290                  -20  2 <B(1) 223780111
142680639      339296394762292                  -18  3 (2)B> 223780111
142680640      339296394762293                  -17  3 2 (3)B> 223780110
142680641      339296418542403             23780093  3 2 323780110 (3)B>
142680642      339296418542405             23780091  3 2 323780110 <B(1)
142680643      339296418542409             23780093  3 2 323780109 4 (4)A>
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  2 3 43+V(1) (4)A>
    1                    1                    1  2 3 44+V(1) (1)B>
    2                    3                   -1  2 3 44+V(1) <A(2)
    3               7+V(1)           -5+-1*V(1)  2 3 <A(2) 24+V(1)
    4               8+V(1)           -6+-1*V(1)  2 <B(1) 25+V(1)
    5              10+V(1)           -4+-1*V(1)  3 (2)B> 25+V(1)
    6              11+V(1)           -3+-1*V(1)  3 2 (3)B> 24+V(1)
    7            15+2*V(1)                    1  3 2 34+V(1) (3)B>
    8            17+2*V(1)                   -1  3 2 34+V(1) <B(1)
    9            21+2*V(1)                    1  3 2 33+V(1) 4 (4)A>
<< Success! ==> defined new CTR 19 (PPA)
142680643      339296418542409             23780093  3 2 323780109 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=23780106, repcount=11890054, factor=3/2
214020967      763416689811697             35670147  3 2 3 435670163 (4)A>
== Executing PPA-CTR 12 (once), V(1)=35670160, V(2)=0
214020976      763416761152038             35670148  32 2 335670163 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=35670160, repcount=17835081, factor=3/2
321031462     1717687282332531             53505229  32 2 3 453505244 (4)A>
== Executing PPA-CTR 12 (once), V(1)=53505241, V(2)=1
321031471     1717687389343034             53505230  33 2 353505244 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=53505241, repcount=26752621, factor=3/2
481547197     3864795847978167             80257851  33 2 32 480257864 (4)A>
481547198     3864795847978168             80257852  33 2 32 480257865 (1)B>
481547199     3864795847978170             80257850  33 2 32 480257865 <A(2)
481547200     3864795928236035                  -15  33 2 32 <A(2) 280257865
481547201     3864795928236036                  -16  33 2 3 <B(1) 280257866
481547202     3864795928236040                  -14  33 2 4 (4)A> 280257866
481547203     3864796008493906             80257852  33 2 480257867 (4)A>
481547204     3864796008493907             80257853  33 2 480257868 (1)B>
481547205     3864796008493909             80257851  33 2 480257868 <A(2)
481547206     3864796088751777                  -17  33 2 <A(2) 280257868
481547207     3864796088751779                  -15  33 4 (4)A> 280257868
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  33+V(2) 2 32 41+V(1) (4)A>
    1                    1                    1  33+V(2) 2 32 42+V(1) (1)B>
    2                    3                   -1  33+V(2) 2 32 42+V(1) <A(2)
    3               5+V(1)           -3+-1*V(1)  33+V(2) 2 32 <A(2) 22+V(1)
    4               6+V(1)           -4+-1*V(1)  33+V(2) 2 3 <B(1) 23+V(1)
    5              10+V(1)           -2+-1*V(1)  33+V(2) 2 4 (4)A> 23+V(1)
    6            13+2*V(1)                    1  33+V(2) 2 44+V(1) (4)A>
    7            14+2*V(1)                    2  33+V(2) 2 45+V(1) (1)B>
    8            16+2*V(1)                    0  33+V(2) 2 45+V(1) <A(2)
    9            21+3*V(1)           -5+-1*V(1)  33+V(2) 2 <A(2) 25+V(1)
   10            23+3*V(1)           -3+-1*V(1)  33+V(2) 4 (4)A> 25+V(1)
<< Success! ==> defined new CTR 20 (PPA)
481547207     3864796088751779                  -15  33 4 (4)A> 280257868
== Executing  PA-CTR 13, V(1)=0, V(2)=80257867, repcount=1, factor=3/2
481547213     3864796249267525                  -17  3 4 (4)A> 280257871
481547214     3864796329525396             80257854  3 480257872 (4)A>
481547215     3864796329525397             80257855  3 480257873 (1)B>
481547216     3864796329525399             80257853  3 480257873 <A(2)
481547217     3864796409783272                  -20  3 <A(2) 280257873
481547218     3864796409783273                  -21  <B(1) 280257874
481547219     3864796409783274                  -22  <A(0) 1 280257874
481547220     3864796409783277                  -23  <A(2) 0 1 280257874
481547221     3864796409783279                  -21  1 (3)B> 0 1 280257874
481547222     3864796409783281                  -23  1 <B(1) 0 1 280257874
481547223     3864796409783283                  -21  2 (2)B> 0 1 280257874
481547224     3864796409783286                  -20  2 4 (1)B> 1 280257874
481547225     3864796409783287                  -19  2 4 1 (2)B> 280257874
481547226     3864796409783288                  -18  2 4 1 2 (3)B> 280257873
481547227     3864796490041161             80257855  2 4 1 2 380257873 (3)B>
481547228     3864796490041163             80257853  2 4 1 2 380257873 <B(1)
481547229     3864796490041167             80257855  2 4 1 2 380257872 4 (4)A>
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  3 41+V(1) (4)A> 22+V(2)
    1               2+V(2)               2+V(2)  3 43+V(1)+V(2) (4)A>
    2               3+V(2)               3+V(2)  3 44+V(1)+V(2) (1)B>
    3               5+V(2)               1+V(2)  3 44+V(1)+V(2) <A(2)
    4        9+V(1)+2*V(2)           -3+-1*V(1)  3 <A(2) 24+V(1)+V(2)
    5       10+V(1)+2*V(2)           -4+-1*V(1)  <B(1) 25+V(1)+V(2)
    6       11+V(1)+2*V(2)           -5+-1*V(1)  <A(0) 1 25+V(1)+V(2)
    7       14+V(1)+2*V(2)           -6+-1*V(1)  <A(2) 0 1 25+V(1)+V(2)
    8       16+V(1)+2*V(2)           -4+-1*V(1)  1 (3)B> 0 1 25+V(1)+V(2)
    9       18+V(1)+2*V(2)           -6+-1*V(1)  1 <B(1) 0 1 25+V(1)+V(2)
   10       20+V(1)+2*V(2)           -4+-1*V(1)  2 (2)B> 0 1 25+V(1)+V(2)
   11       23+V(1)+2*V(2)           -3+-1*V(1)  2 4 (1)B> 1 25+V(1)+V(2)
   12       24+V(1)+2*V(2)           -2+-1*V(1)  2 4 1 (2)B> 25+V(1)+V(2)
   13       25+V(1)+2*V(2)           -1+-1*V(1)  2 4 1 2 (3)B> 24+V(1)+V(2)
   14     29+2*V(1)+3*V(2)               3+V(2)  2 4 1 2 34+V(1)+V(2) (3)B>
   15     31+2*V(1)+3*V(2)               1+V(2)  2 4 1 2 34+V(1)+V(2) <B(1)
   16     35+2*V(1)+3*V(2)               3+V(2)  2 4 1 2 33+V(1)+V(2) 4 (4)A>
<< Success! ==> defined new CTR 21 (PPA)
481547229     3864796490041167             80257855  2 4 1 2 380257872 4 (4)A>
== Executing  PA-CTR  5, V(1)=0, V(2)=80257869, repcount=40128935, factor=3/2
722320839     8695791164033192            120386790  2 4 1 2 32 4120386806 (4)A>
== Executing PPA-CTR  6 (once), V(1)=120386805, V(2)=0, V(3)=0
722320864     8695792127127716            120386794  1 3120386815 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=120386812, repcount=60193407, factor=3/2
1083481306    19565531467864733            180580201  1 3 4180580222 (4)A>
== Executing PPA-CTR  2 (once), V(1)=180580219
1083481315    19565531829025192            180580202  22 3180580222 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=180580219, repcount=90290110, factor=3/2
1625221975    44022444623362592            270870312  22 32 4270870331 (4)A>
== Executing PPA-CTR 17 (once), V(1)=270870330, V(2)=0
1625221980    44022444894232932                  -20  22 4 (4)A> 2270870333
== Executing  PA-CTR 15, V(1)=0, V(2)=270870332, repcount=1, factor=2/1
1625221985    44022445435973605                  -21  2 4 (4)A> 2270870335
== Executing PPA-CTR 16 (once), V(1)=0, V(2)=270870334
1625221998    44022446790325308            270870316  1 3270870338 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=270870335, repcount=135435168, factor=3/2
2437833006    99050502338241660            406305484  1 32 4406305505 (4)A>
== Executing PPA-CTR  7 (once), V(1)=406305504, V(2)=0
2437833020    99050503963463712            406305486  1 3406305509 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=406305506, repcount=203152754, factor=3/2
3656749544    2228636[4]8344800            609458240  1 3 4609458263 (4)A>
== Executing PPA-CTR  2 (once), V(1)=609458260
3656749553    2228636[4]7261341            609458241  22 3609458263 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=609458260, repcount=304729131, factor=3/2
5485124339    5014431[4]4598134            914187372  22 3 4914187394 (4)A>
== Executing PPA-CTR  8 (once), V(1)=914187391, V(2)=0
5485124348    5014431[4]2972937            914187373  2 3 2 3914187394 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=914187391, repcount=457093696, factor=3/2
8227686524    1128247[5]2731145           1371281069  2 3 2 32 41371281089 (4)A>
== Executing PPA-CTR 11 (once), V(1)=1371281088
8227686544    1128247[5]0417728           1371281072  3 2 31371281094 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=1371281091, repcount=685640546, factor=3/2
12341529820    2538556[5]4357536           2056921618  3 2 32 42056921639 (4)A>
12341529821    2538556[5]4357537           2056921619  3 2 32 42056921640 (1)B>
12341529822    2538556[5]4357539           2056921617  3 2 32 42056921640 <A(2)
12341529823    2538556[5]1279179                  -23  3 2 32 <A(2) 22056921640
12341529824    2538556[5]1279180                  -24  3 2 3 <B(1) 22056921641
12341529825    2538556[5]1279184                  -22  3 2 4 (4)A> 22056921641
12341529826    2538556[5]8200825           2056921619  3 2 42056921642 (4)A>
12341529827    2538556[5]8200826           2056921620  3 2 42056921643 (1)B>
12341529828    2538556[5]8200828           2056921618  3 2 42056921643 <A(2)
12341529829    2538556[5]5122471                  -25  3 2 <A(2) 22056921643
12341529830    2538556[5]5122473                  -23  3 4 (4)A> 22056921643
12341529831    2538556[5]2044116           2056921620  3 42056921644 (4)A>
12341529832    2538556[5]2044117           2056921621  3 42056921645 (1)B>
12341529833    2538556[5]2044119           2056921619  3 42056921645 <A(2)
12341529834    2538556[5]8965764                  -26  3 <A(2) 22056921645
12341529835    2538556[5]8965765                  -27  <B(1) 22056921646
12341529836    2538556[5]8965766                  -28  <A(0) 1 22056921646
12341529837    2538556[5]8965769                  -29  <A(2) 0 1 22056921646
12341529838    2538556[5]8965771                  -27  1 (3)B> 0 1 22056921646
12341529839    2538556[5]8965773                  -29  1 <B(1) 0 1 22056921646
12341529840    2538556[5]8965775                  -27  2 (2)B> 0 1 22056921646
12341529841    2538556[5]8965778                  -26  2 4 (1)B> 1 22056921646
12341529842    2538556[5]8965779                  -25  2 4 1 (2)B> 22056921646
12341529843    2538556[5]8965780                  -24  2 4 1 2 (3)B> 22056921645
12341529844    2538556[5]5887425           2056921621  2 4 1 2 32056921645 (3)B>
12341529845    2538556[5]5887427           2056921619  2 4 1 2 32056921645 <B(1)
12341529846    2538556[5]5887431           2056921621  2 4 1 2 32056921644 4 (4)A>
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  3 2 32 41+V(1) (4)A>
    1                    1                    1  3 2 32 42+V(1) (1)B>
    2                    3                   -1  3 2 32 42+V(1) <A(2)
    3               5+V(1)           -3+-1*V(1)  3 2 32 <A(2) 22+V(1)
    4               6+V(1)           -4+-1*V(1)  3 2 3 <B(1) 23+V(1)
    5              10+V(1)           -2+-1*V(1)  3 2 4 (4)A> 23+V(1)
    6            13+2*V(1)                    1  3 2 44+V(1) (4)A>
    7            14+2*V(1)                    2  3 2 45+V(1) (1)B>
    8            16+2*V(1)                    0  3 2 45+V(1) <A(2)
    9            21+3*V(1)           -5+-1*V(1)  3 2 <A(2) 25+V(1)
   10            23+3*V(1)           -3+-1*V(1)  3 4 (4)A> 25+V(1)
   11            28+4*V(1)                    2  3 46+V(1) (4)A>
   12            29+4*V(1)                    3  3 47+V(1) (1)B>
   13            31+4*V(1)                    1  3 47+V(1) <A(2)
   14            38+5*V(1)           -6+-1*V(1)  3 <A(2) 27+V(1)
   15            39+5*V(1)           -7+-1*V(1)  <B(1) 28+V(1)
   16            40+5*V(1)           -8+-1*V(1)  <A(0) 1 28+V(1)
   17            43+5*V(1)           -9+-1*V(1)  <A(2) 0 1 28+V(1)
   18            45+5*V(1)           -7+-1*V(1)  1 (3)B> 0 1 28+V(1)
   19            47+5*V(1)           -9+-1*V(1)  1 <B(1) 0 1 28+V(1)
   20            49+5*V(1)           -7+-1*V(1)  2 (2)B> 0 1 28+V(1)
   21            52+5*V(1)           -6+-1*V(1)  2 4 (1)B> 1 28+V(1)
   22            53+5*V(1)           -5+-1*V(1)  2 4 1 (2)B> 28+V(1)
   23            54+5*V(1)           -4+-1*V(1)  2 4 1 2 (3)B> 27+V(1)
   24            61+6*V(1)                    3  2 4 1 2 37+V(1) (3)B>
   25            63+6*V(1)                    1  2 4 1 2 37+V(1) <B(1)
   26            67+6*V(1)                    3  2 4 1 2 36+V(1) 4 (4)A>
<< Success! ==> defined new CTR 22 (PPA)
12341529846    2538556[5]5887431           2056921621  2 4 1 2 32056921644 4 (4)A>
== Executing  PA-CTR  5, V(1)=0, V(2)=2056921641, repcount=1028460821, factor=3/2
18512294772    5711751[5]6477764           3085382442  2 4 1 2 32 43085382464 (4)A>
== Executing PPA-CTR  6 (once), V(1)=3085382463, V(2)=0, V(3)=0
18512294797    5711751[5]9537552           3085382446  1 33085382473 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=3085382470, repcount=1542691236, factor=3/2
27768442213    1285143[6]0073000           4628073682  1 3 44628073709 (4)A>
== Executing PPA-CTR  2 (once), V(1)=4628073706
27768442222    1285143[6]6220433           4628073683  22 34628073709 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=4628073706, repcount=2314036854, factor=3/2
41652663346    2891573[6]7240921           6942110537  22 3 46942110563 (4)A>
== Executing PPA-CTR  8 (once), V(1)=6942110560, V(2)=0
41652663355    2891573[6]1462062           6942110538  2 3 2 36942110563 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=6942110560, repcount=3471055281, factor=3/2
62478995041    6506041[6]5981755          10413165819  2 3 2 3 410413165844 (4)A>
== Executing PPA-CTR  9 (once), V(1)=10413165841, V(2)=0
62478995050    6506041[6]2313458          10413165820  2 32 2 310413165844 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=10413165841, repcount=5206582921, factor=3/2
93718492576    1463859[7]4819391          15619748741  2 32 2 32 415619748764 (4)A>
== Executing PPA-CTR 10 (once), V(1)=15619748763
93718492605    1463859[7]2307132          15619748746  1 315619748774 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=15619748771, repcount=7809874386, factor=3/2
140577738921    3293683[7]7681980          23429623132  1 32 423429623159 (4)A>
== Executing PPA-CTR  7 (once), V(1)=23429623158, V(2)=0
140577738935    3293683[7]6174648          23429623134  1 323429623163 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=23429623160, repcount=11714811581, factor=3/2
210866608421    7410787[7]9449141          35144434715  1 3 435144434744 (4)A>
== Executing PPA-CTR  2 (once), V(1)=35144434741
210866608430    7410787[7]8318644          35144434716  22 335144434744 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=35144434741, repcount=17572217371, factor=3/2
316299912656    1667427[8]2947277          52716652087  22 32 452716652114 (4)A>
== Executing PPA-CTR 17 (once), V(1)=52716652113, V(2)=0
316299912661    1667427[8]9599400                  -28  22 4 (4)A> 252716652116
== Executing  PA-CTR 15, V(1)=0, V(2)=52716652115, repcount=1, factor=2/1
316299912666    1667427[8]2903639                  -29  2 4 (4)A> 252716652118
== Executing PPA-CTR 16 (once), V(1)=0, V(2)=52716652117
316299912679    1667427[8]6164257          52716652091  1 352716652121 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=52716652118, repcount=26358326060, factor=3/2
474449869039    3751711[8]4795657          79074978151  1 3 479074978181 (4)A>
== Executing PPA-CTR  2 (once), V(1)=79074978178
474449869048    3751711[8]4752034          79074978152  22 379074978181 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=79074978178, repcount=39537489090, factor=3/2
711674803588    8441350[8]6727234         118612467242  22 3 4118612467271 (4)A>
== Executing PPA-CTR  8 (once), V(1)=118612467268, V(2)=0
711674803597    8441350[8]1661791         118612467243  2 3 2 3118612467271 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=118612467268, repcount=59306233635, factor=3/2
1067512205407    1899303[9]9937816         177918700878  2 3 2 3 4177918700906 (4)A>
== Executing PPA-CTR  9 (once), V(1)=177918700903, V(2)=0
1067512205416    1899303[9]7339643         177918700879  2 32 2 3177918700906 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=177918700903, repcount=88959350452, factor=3/2
1601268308128    4273433[9]8657075         266878051331  2 32 2 32 4266878051357 (4)A>
== Executing PPA-CTR 10 (once), V(1)=266878051356
1601268308157    4273433[9]9170746         266878051336  1 3266878051367 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=266878051364, repcount=133439025683, factor=3/2
2401902462255    9615225[9]0277043         400317077019  1 3 4400317077050 (4)A>
== Executing PPA-CTR  2 (once), V(1)=400317077047
2401902462264    9615225[9]4431158         400317077020  22 3400317077050 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=400317077047, repcount=200158538524, factor=3/2
3602853693408   2163425[10]6112126         600475615544  22 32 4600475615573 (4)A>
== Executing PPA-CTR 17 (once), V(1)=600475615572, V(2)=0
3602853693413   2163425[10]1727708                  -30  22 4 (4)A> 2600475615575
== Executing  PA-CTR 15, V(1)=0, V(2)=600475615574, repcount=1, factor=2/1
3602853693418   2163425[10]2958865                  -31  2 4 (4)A> 2600475615577
== Executing PPA-CTR 16 (once), V(1)=0, V(2)=600475615576
3602853693431   2163425[10]1036778         600475615548  1 3600475615580 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=600475615577, repcount=300237807789, factor=3/2
5404280540165   4867708[10]6320231         900713423337  1 32 4900713423368 (4)A>
== Executing PPA-CTR  7 (once), V(1)=900713423367, V(2)=0
5404280540179   4867708[10]0013735         900713423339  1 3900713423372 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=900713423369, repcount=450356711685, factor=3/2
8106420810289   1095234[11]3748260        1351070135024  1 32 41351070135056 (4)A>
== Executing PPA-CTR  7 (once), V(1)=1351070135055, V(2)=0
8106420810303   1095234[11]4288516        1351070135026  1 31351070135060 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=1351070135057, repcount=675535067529, factor=3/2
12159631215477   2464277[11]5461329        2026605202555  1 32 42026605202588 (4)A>
== Executing PPA-CTR  7 (once), V(1)=2026605202587, V(2)=0
12159631215491   2464277[11]6271713        2026605202557  1 32026605202592 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=2026605202589, repcount=1013302601295, factor=3/2
18239446823261   5544623[11]9315738        3039907803852  1 32 43039907803886 (4)A>
== Executing PPA-CTR  7 (once), V(1)=3039907803885, V(2)=0
18239446823275   5544623[11]0531314        3039907803854  1 33039907803890 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=3039907803887, repcount=1519953901944, factor=3/2
27359170234939   1247540[12]0488162        4559861705798  1 32 44559861705833 (4)A>
== Executing PPA-CTR  7 (once), V(1)=4559861705832, V(2)=0
27359170234953   1247540[12]7311526        4559861705800  1 34559861705837 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=4559861705834, repcount=2279930852918, factor=3/2
41038755352461   2806965[12]3184878        6839792558718  1 3 46839792558755 (4)A>
== Executing PPA-CTR  2 (once), V(1)=6839792558752
41038755352470   2806965[12]8302403        6839792558719  22 36839792558755 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=6839792558752, repcount=3419896279377, factor=3/2
61558133028732   6315672[12]7620560       10259688838096  22 3 410259688838132 (4)A>
== Executing PPA-CTR  8 (once), V(1)=10259688838129, V(2)=0
61558133028741   6315672[12]5296839       10259688838097  2 3 2 310259688838132 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=10259688838129, repcount=5129844419065, factor=3/2
92337199543131   1421026[13]5910164       15389533257162  2 3 2 32 415389533257196 (4)A>
== Executing PPA-CTR 11 (once), V(1)=15389533257195
92337199543151   1421026[13]5453389       15389533257165  3 2 315389533257201 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=15389533257198, repcount=7694766628600, factor=3/2
138505799314751   3197309[13]5619389       23084299885765  3 2 3 423084299885801 (4)A>
== Executing PPA-CTR 12 (once), V(1)=23084299885798, V(2)=0
138505799314760   3197309[13]5391006       23084299885766  32 2 323084299885801 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=23084299885798, repcount=11542149942900, factor=3/2
207758698972160   7193946[13]6050006       34626449828666  32 2 3 434626449828701 (4)A>
== Executing PPA-CTR 12 (once), V(1)=34626449828698, V(2)=1
207758698972169   7193946[13]5707423       34626449828667  33 2 334626449828701 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=34626449828698, repcount=17313224914350, factor=3/2
311638048458269   1618637[14]2618423       51939674743017  33 2 3 451939674743051 (4)A>
== Executing PPA-CTR 12 (once), V(1)=51939674743048, V(2)=2
311638048458278   1618637[14]2104540       51939674743018  34 2 351939674743051 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=51939674743048, repcount=25969837371525, factor=3/2
467457072687428   3641935[14]8296665       77909512114543  34 2 3 477909512114576 (4)A>
== Executing PPA-CTR 12 (once), V(1)=77909512114573, V(2)=3
467457072687437   3641935[14]2525832       77909512114544  35 2 377909512114576 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=77909512114573, repcount=38954756057287, factor=3/2
701185609031159   8194354[14]0499809      116864268171831  35 2 32 4116864268171862 (4)A>
== Executing PPA-CTR 20 (once), V(1)=116864268171861, V(2)=2
701185609031169   8194354[14]5015415                  -33  35 4 (4)A> 2116864268171866
== Executing  PA-CTR 13, V(1)=2, V(2)=116864268171865, repcount=2, factor=3/2
701185609031181   8194354[14]7702905                  -37  3 4 (4)A> 2116864268171872
== Executing PPA-CTR 21 (once), V(1)=0, V(2)=116864268171870
701185609031197   8194354[14]2218550      116864268171836  2 4 1 2 3116864268171873 4 (4)A>
== Executing  PA-CTR  5, V(1)=0, V(2)=116864268171870, repcount=58432134085936, factor=3/2
1051778413546813   1843729[15]2066198      175296402257772  2 4 1 2 3 4175296402257809 (4)A>
1051778413546814   1843729[15]2066199      175296402257773  2 4 1 2 3 4175296402257810 (1)B>
1051778413546815   1843729[15]2066201      175296402257771  2 4 1 2 3 4175296402257810 <A(2)
1051778413546816   1843729[15]4324011                  -39  2 4 1 2 3 <A(2) 2175296402257810
1051778413546817   1843729[15]4324012                  -40  2 4 1 2 <B(1) 2175296402257811
1051778413546818   1843729[15]4324014                  -38  2 4 1 3 (2)B> 2175296402257811
1051778413546819   1843729[15]4324015                  -37  2 4 1 3 2 (3)B> 2175296402257810
1051778413546820   1843729[15]6581825      175296402257773  2 4 1 3 2 3175296402257810 (3)B>
1051778413546821   1843729[15]6581827      175296402257771  2 4 1 3 2 3175296402257810 <B(1)
1051778413546822   1843729[15]6581831      175296402257773  2 4 1 3 2 3175296402257809 4 (4)A>
1051778413546823   1843729[15]6581832      175296402257774  2 4 1 3 2 3175296402257809 42 (1)B>
1051778413546824   1843729[15]6581834      175296402257772  2 4 1 3 2 3175296402257809 42 <A(2)
1051778413546825   1843729[15]6581836      175296402257770  2 4 1 3 2 3175296402257809 <A(2) 22
1051778413546826   1843729[15]6581837      175296402257769  2 4 1 3 2 3175296402257808 <B(1) 23
1051778413546827   1843729[15]6581841      175296402257771  2 4 1 3 2 3175296402257807 4 (4)A> 23
1051778413546828   1843729[15]6581844      175296402257774  2 4 1 3 2 3175296402257807 44 (4)A>
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  [*]* [*]* [*]* [*]* [*]* 33+V(2) 41+V(1) (4)A>
    1                    1                    1  [*]* [*]* [*]* [*]* [*]* 33+V(2) 42+V(1) (1)B>
    2                    3                   -1  [*]* [*]* [*]* [*]* [*]* 33+V(2) 42+V(1) <A(2)
    3               5+V(1)           -3+-1*V(1)  [*]* [*]* [*]* [*]* [*]* 33+V(2) <A(2) 22+V(1)
    4               6+V(1)           -4+-1*V(1)  [*]* [*]* [*]* [*]* [*]* 32+V(2) <B(1) 23+V(1)
    5              10+V(1)           -2+-1*V(1)  [*]* [*]* [*]* [*]* [*]* 31+V(2) 4 (4)A> 23+V(1)
    6            13+2*V(1)                    1  [*]* [*]* [*]* [*]* [*]* 31+V(2) 44+V(1) (4)A>
<< Success! ==> defined new CTR 23 (PA)
1051778413546828   1843729[15]6581844      175296402257774  2 4 1 3 2 3175296402257807 44 (4)A>
== Executing  PA-CTR 23, V(1)=3, V(2)=175296402257804, repcount=87648201128903, factor=3/2
1577667620320246   4148391[15]0594519      262944603386677  2 4 1 3 2 3 4262944603386713 (4)A>
1577667620320247   4148391[15]0594520      262944603386678  2 4 1 3 2 3 4262944603386714 (1)B>
1577667620320248   4148391[15]0594522      262944603386676  2 4 1 3 2 3 4262944603386714 <A(2)
1577667620320249   4148391[15]3981236                  -38  2 4 1 3 2 3 <A(2) 2262944603386714
1577667620320250   4148391[15]3981237                  -39  2 4 1 3 2 <B(1) 2262944603386715
1577667620320251   4148391[15]3981239                  -37  2 4 1 32 (2)B> 2262944603386715
1577667620320252   4148391[15]3981240                  -36  2 4 1 32 2 (3)B> 2262944603386714
1577667620320253   4148391[15]7367954      262944603386678  2 4 1 32 2 3262944603386714 (3)B>
1577667620320254   4148391[15]7367956      262944603386676  2 4 1 32 2 3262944603386714 <B(1)
1577667620320255   4148391[15]7367960      262944603386678  2 4 1 32 2 3262944603386713 4 (4)A>
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  [*]* [*]* [*]* 31+V(2) 2 3 43+V(1) (4)A>
    1                    1                    1  [*]* [*]* [*]* 31+V(2) 2 3 44+V(1) (1)B>
    2                    3                   -1  [*]* [*]* [*]* 31+V(2) 2 3 44+V(1) <A(2)
    3               7+V(1)           -5+-1*V(1)  [*]* [*]* [*]* 31+V(2) 2 3 <A(2) 24+V(1)
    4               8+V(1)           -6+-1*V(1)  [*]* [*]* [*]* 31+V(2) 2 <B(1) 25+V(1)
    5              10+V(1)           -4+-1*V(1)  [*]* [*]* [*]* 32+V(2) (2)B> 25+V(1)
    6              11+V(1)           -3+-1*V(1)  [*]* [*]* [*]* 32+V(2) 2 (3)B> 24+V(1)
    7            15+2*V(1)                    1  [*]* [*]* [*]* 32+V(2) 2 34+V(1) (3)B>
    8            17+2*V(1)                   -1  [*]* [*]* [*]* 32+V(2) 2 34+V(1) <B(1)
    9            21+2*V(1)                    1  [*]* [*]* [*]* 32+V(2) 2 33+V(1) 4 (4)A>
<< Success! ==> defined new CTR 24 (PPA)
1577667620320255   4148391[15]7367960      262944603386678  2 4 1 32 2 3262944603386713 4 (4)A>
== Executing  PA-CTR 23, V(1)=0, V(2)=262944603386710, repcount=131472301693356, factor=3/2
2366501430480391   9333881[15]7929728      394416905080034  2 4 1 32 2 3 4394416905080069 (4)A>
== Executing PPA-CTR 24 (once), V(1)=394416905080066, V(2)=1
2366501430480400   9333881[15]8089881      394416905080035  2 4 1 33 2 3394416905080069 4 (4)A>
== Executing  PA-CTR 23, V(1)=0, V(2)=394416905080066, repcount=197208452540034, factor=3/2
3549752145720604   2100123[16]1653689      591625357620069  2 4 1 33 2 3 4591625357620103 (4)A>
== Executing PPA-CTR 24 (once), V(1)=591625357620100, V(2)=2
3549752145720613   2100123[16]6893910      591625357620070  2 4 1 34 2 3591625357620103 4 (4)A>
== Executing  PA-CTR 23, V(1)=0, V(2)=591625357620100, repcount=295812678810051, factor=3/2
5324628218580919   4725277[16]0862223      887438036430121  2 4 1 34 2 3 4887438036430154 (4)A>
== Executing PPA-CTR 24 (once), V(1)=887438036430151, V(2)=3
5324628218580928   4725277[16]3722546      887438036430122  2 4 1 35 2 3887438036430154 4 (4)A>
== Executing  PA-CTR 23, V(1)=0, V(2)=887438036430151, repcount=443719018215076, factor=3/2
7986942327871384   1063187[17]6930634     1331157054645198  2 4 1 35 2 32 41331157054645229 (4)A>
7986942327871385   1063187[17]6930635     1331157054645199  2 4 1 35 2 32 41331157054645230 (1)B>
7986942327871386   1063187[17]6930637     1331157054645197  2 4 1 35 2 32 41331157054645230 <A(2)
7986942327871387   1063187[17]1575867                  -33  2 4 1 35 2 32 <A(2) 21331157054645230
7986942327871388   1063187[17]1575868                  -34  2 4 1 35 2 3 <B(1) 21331157054645231
7986942327871389   1063187[17]1575872                  -32  2 4 1 35 2 4 (4)A> 21331157054645231
7986942327871390   1063187[17]6221103     1331157054645199  2 4 1 35 2 41331157054645232 (4)A>
7986942327871391   1063187[17]6221104     1331157054645200  2 4 1 35 2 41331157054645233 (1)B>
7986942327871392   1063187[17]6221106     1331157054645198  2 4 1 35 2 41331157054645233 <A(2)
7986942327871393   1063187[17]0866339                  -35  2 4 1 35 2 <A(2) 21331157054645233
7986942327871394   1063187[17]0866341                  -33  2 4 1 35 4 (4)A> 21331157054645233
7986942327871395   1063187[17]5511574     1331157054645200  2 4 1 35 41331157054645234 (4)A>
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  [*]* [*]* [*]* 33+V(2) 2 32 41+V(1) (4)A>
    1                    1                    1  [*]* [*]* [*]* 33+V(2) 2 32 42+V(1) (1)B>
    2                    3                   -1  [*]* [*]* [*]* 33+V(2) 2 32 42+V(1) <A(2)
    3               5+V(1)           -3+-1*V(1)  [*]* [*]* [*]* 33+V(2) 2 32 <A(2) 22+V(1)
    4               6+V(1)           -4+-1*V(1)  [*]* [*]* [*]* 33+V(2) 2 3 <B(1) 23+V(1)
    5              10+V(1)           -2+-1*V(1)  [*]* [*]* [*]* 33+V(2) 2 4 (4)A> 23+V(1)
    6            13+2*V(1)                    1  [*]* [*]* [*]* 33+V(2) 2 44+V(1) (4)A>
    7            14+2*V(1)                    2  [*]* [*]* [*]* 33+V(2) 2 45+V(1) (1)B>
    8            16+2*V(1)                    0  [*]* [*]* [*]* 33+V(2) 2 45+V(1) <A(2)
    9            21+3*V(1)           -5+-1*V(1)  [*]* [*]* [*]* 33+V(2) 2 <A(2) 25+V(1)
   10            23+3*V(1)           -3+-1*V(1)  [*]* [*]* [*]* 33+V(2) 4 (4)A> 25+V(1)
   11            28+4*V(1)                    2  [*]* [*]* [*]* 33+V(2) 46+V(1) (4)A>
<< Success! ==> defined new CTR 25 (PPA)
7986942327871395   1063187[17]5511574     1331157054645200  2 4 1 35 41331157054645234 (4)A>
== Executing  PA-CTR  3, V(1)=1331157054645233, V(2)=2, repcount=2, factor=3/2
7986942327871407   1063187[17]4092538     1331157054645202  2 4 1 3 41331157054645240 (4)A>
7986942327871408   1063187[17]4092539     1331157054645203  2 4 1 3 41331157054645241 (1)B>
7986942327871409   1063187[17]4092541     1331157054645201  2 4 1 3 41331157054645241 <A(2)
7986942327871410   1063187[17]8737782                  -40  2 4 1 3 <A(2) 21331157054645241
7986942327871411   1063187[17]8737783                  -41  2 4 1 <B(1) 21331157054645242
7986942327871412   1063187[17]8737785                  -39  2 4 2 (2)B> 21331157054645242
7986942327871413   1063187[17]8737786                  -38  2 4 22 (3)B> 21331157054645241
7986942327871414   1063187[17]3383027     1331157054645203  2 4 22 31331157054645241 (3)B>
7986942327871415   1063187[17]3383029     1331157054645201  2 4 22 31331157054645241 <B(1)
7986942327871416   1063187[17]3383033     1331157054645203  2 4 22 31331157054645240 4 (4)A>
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  [*]* [*]* 1 3 43+V(1) (4)A>
    1                    1                    1  [*]* [*]* 1 3 44+V(1) (1)B>
    2                    3                   -1  [*]* [*]* 1 3 44+V(1) <A(2)
    3               7+V(1)           -5+-1*V(1)  [*]* [*]* 1 3 <A(2) 24+V(1)
    4               8+V(1)           -6+-1*V(1)  [*]* [*]* 1 <B(1) 25+V(1)
    5              10+V(1)           -4+-1*V(1)  [*]* [*]* 2 (2)B> 25+V(1)
    6              11+V(1)           -3+-1*V(1)  [*]* [*]* 22 (3)B> 24+V(1)
    7            15+2*V(1)                    1  [*]* [*]* 22 34+V(1) (3)B>
    8            17+2*V(1)                   -1  [*]* [*]* 22 34+V(1) <B(1)
    9            21+2*V(1)                    1  [*]* [*]* 22 33+V(1) 4 (4)A>
<< Success! ==> defined new CTR 26 (PPA)
7986942327871416   1063187[17]3383033     1331157054645203  2 4 22 31331157054645240 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=1331157054645237, repcount=665578527322619, factor=3/2
11980413491807130   2392171[17]3666706     1996735581967822  2 4 22 32 41996735581967858 (4)A>
11980413491807131   2392171[17]3666707     1996735581967823  2 4 22 32 41996735581967859 (1)B>
11980413491807132   2392171[17]3666709     1996735581967821  2 4 22 32 41996735581967859 <A(2)
11980413491807133   2392171[17]5634568                  -38  2 4 22 32 <A(2) 21996735581967859
11980413491807134   2392171[17]5634569                  -39  2 4 22 3 <B(1) 21996735581967860
11980413491807135   2392171[17]5634573                  -37  2 4 22 4 (4)A> 21996735581967860
11980413491807136   2392171[17]7602433     1996735581967823  2 4 22 41996735581967861 (4)A>
11980413491807137   2392171[17]7602434     1996735581967824  2 4 22 41996735581967862 (1)B>
11980413491807138   2392171[17]7602436     1996735581967822  2 4 22 41996735581967862 <A(2)
11980413491807139   2392171[17]9570298                  -40  2 4 22 <A(2) 21996735581967862
11980413491807140   2392171[17]9570300                  -38  2 4 2 4 (4)A> 21996735581967862
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  [*]* [*]* 22+V(1) 4 (4)A> 21+V(2)
    1               1+V(2)               1+V(2)  [*]* [*]* 22+V(1) 42+V(2) (4)A>
    2               2+V(2)               2+V(2)  [*]* [*]* 22+V(1) 43+V(2) (1)B>
    3               4+V(2)               0+V(2)  [*]* [*]* 22+V(1) 43+V(2) <A(2)
    4             7+2*V(2)                   -3  [*]* [*]* 22+V(1) <A(2) 23+V(2)
    5             9+2*V(2)                   -1  [*]* [*]* 21+V(1) 4 (4)A> 23+V(2)
<< Success! ==> defined new CTR 27 (PA)
11980413491807141   2392171[17]1538162     1996735581967824  2 4 2 41996735581967863 (4)A>
11980413491807142   2392171[17]1538163     1996735581967825  2 4 2 41996735581967864 (1)B>
11980413491807143   2392171[17]1538165     1996735581967823  2 4 2 41996735581967864 <A(2)
11980413491807144   2392171[17]3506029                  -41  2 4 2 <A(2) 21996735581967864
11980413491807145   2392171[17]3506031                  -39  2 42 (4)A> 21996735581967864
11980413491807146   2392171[17]5473895     1996735581967825  2 41996735581967866 (4)A>
11980413491807147   2392171[17]5473896     1996735581967826  2 41996735581967867 (1)B>
11980413491807148   2392171[17]5473898     1996735581967824  2 41996735581967867 <A(2)
11980413491807149   2392171[17]7441765                  -43  2 <A(2) 21996735581967867
11980413491807150   2392171[17]7441767                  -41  4 (4)A> 21996735581967867
11980413491807151   2392171[17]9409634     1996735581967826  41996735581967868 (4)A>
11980413491807152   2392171[17]9409635     1996735581967827  41996735581967869 (1)B>
11980413491807153   2392171[17]9409637     1996735581967825  41996735581967869 <A(2)
11980413491807154   2392171[17]1377506                  -44  <A(2) 21996735581967869
11980413491807155   2392171[17]1377508                  -42  1 (3)B> 21996735581967869
11980413491807156   2392171[17]3345377     1996735581967827  1 31996735581967869 (3)B>
11980413491807157   2392171[17]3345379     1996735581967825  1 31996735581967869 <B(1)
11980413491807158   2392171[17]3345383     1996735581967827  1 31996735581967868 4 (4)A>
>> Try to prove a PPA-CTR with 3 Vars...
    0                    0                    0  2 41+V(2) 2 41+V(1) (4)A> 21+V(3)
    1               1+V(3)               1+V(3)  2 41+V(2) 2 42+V(1)+V(3) (4)A>
    2               2+V(3)               2+V(3)  2 41+V(2) 2 43+V(1)+V(3) (1)B>
    3               4+V(3)               0+V(3)  2 41+V(2) 2 43+V(1)+V(3) <A(2)
    4        7+V(1)+2*V(3)           -3+-1*V(1)  2 41+V(2) 2 <A(2) 23+V(1)+V(3)
    5        9+V(1)+2*V(3)           -1+-1*V(1)  2 42+V(2) (4)A> 23+V(1)+V(3)
    6     12+2*V(1)+3*V(3)               2+V(3)  2 45+V(1)+V(2)+V(3) (4)A>
    7     13+2*V(1)+3*V(3)               3+V(3)  2 46+V(1)+V(2)+V(3) (1)B>
    8     15+2*V(1)+3*V(3)               1+V(3)  2 46+V(1)+V(2)+V(3) <A(2)
    9 21+3*V(1)+V(2)+4*V(3)   -5+-1*V(1)+-1*V(2)  2 <A(2) 26+V(1)+V(2)+V(3)
   10 23+3*V(1)+V(2)+4*V(3)   -3+-1*V(1)+-1*V(2)  4 (4)A> 26+V(1)+V(2)+V(3)
   11 29+4*V(1)+2*V(2)+5*V(3)               3+V(3)  47+V(1)+V(2)+V(3) (4)A>
   12 30+4*V(1)+2*V(2)+5*V(3)               4+V(3)  48+V(1)+V(2)+V(3) (1)B>
   13 32+4*V(1)+2*V(2)+5*V(3)               2+V(3)  48+V(1)+V(2)+V(3) <A(2)
   14 40+5*V(1)+3*V(2)+6*V(3)   -6+-1*V(1)+-1*V(2)  <A(2) 28+V(1)+V(2)+V(3)
   15 42+5*V(1)+3*V(2)+6*V(3)   -4+-1*V(1)+-1*V(2)  1 (3)B> 28+V(1)+V(2)+V(3)
   16 50+6*V(1)+4*V(2)+7*V(3)               4+V(3)  1 38+V(1)+V(2)+V(3) (3)B>
   17 52+6*V(1)+4*V(2)+7*V(3)               2+V(3)  1 38+V(1)+V(2)+V(3) <B(1)
   18 56+6*V(1)+4*V(2)+7*V(3)               4+V(3)  1 37+V(1)+V(2)+V(3) 4 (4)A>
<< Success! ==> defined new CTR 28 (PPA)
11980413491807158   2392171[17]3345383     1996735581967827  1 31996735581967868 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=1996735581967865, repcount=998367790983933, factor=3/2
17970620237710756   5382386[17]5630180     2995103372951760  1 32 42995103372951800 (4)A>
== Executing PPA-CTR  7 (once), V(1)=2995103372951799, V(2)=0
17970620237710770   5382386[17]7437412     2995103372951762  1 32995103372951804 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=2995103372951801, repcount=1497551686475901, factor=3/2
26955930356566176   1211036[18]3481825     4492655059427663  1 32 44492655059427704 (4)A>
== Executing PPA-CTR  7 (once), V(1)=4492655059427703, V(2)=0
26955930356566190   1211036[18]1192673     4492655059427665  1 34492655059427708 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=4492655059427705, repcount=2246327529713853, factor=3/2
40433895534849308   2724833[18]8648030     6738982589141518  1 32 46738982589141560 (4)A>
== Executing PPA-CTR  7 (once), V(1)=6738982589141559, V(2)=0
40433895534849322   2724833[18]5214302     6738982589141520  1 36738982589141564 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=6738982589141561, repcount=3369491294570781, factor=3/2
60650843302274008   6130874[18]7771995    10108473883712301  1 32 410108473883712344 (4)A>
== Executing PPA-CTR  7 (once), V(1)=10108473883712343, V(2)=0
60650843302274022   6130874[18]2621403    10108473883712303  1 310108473883712348 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=10108473883712345, repcount=5054236941856173, factor=3/2
90976264953411060   1379446[19]5800920    15162710825568476  1 32 415162710825568520 (4)A>
== Executing PPA-CTR  7 (once), V(1)=15162710825568519, V(2)=0
90976264953411074   1379446[19]8075032    15162710825568478  1 315162710825568524 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=15162710825568521, repcount=7581355412784261, factor=3/2
1364643[4]0116640   3103755[19]3866005    22744066238352739  1 32 422744066238352784 (4)A>
== Executing PPA-CTR  7 (once), V(1)=22744066238352783, V(2)=0
1364643[4]0116654   3103755[19]7277173    22744066238352741  1 322744066238352788 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=22744066238352785, repcount=11372033119176393, factor=3/2
2046965[4]5175012   6983449[19]4512450    34116099357529134  1 32 434116099357529180 (4)A>
== Executing PPA-CTR  7 (once), V(1)=34116099357529179, V(2)=0
2046965[4]5175026   6983449[19]4629202    34116099357529136  1 334116099357529184 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=34116099357529181, repcount=17058049678764591, factor=3/2
3070448[4]7762572   1571276[20]8466955    51174149036293727  1 32 451174149036293774 (4)A>
== Executing PPA-CTR  7 (once), V(1)=51174149036293773, V(2)=0
3070448[4]7762586   1571276[20]3642083    51174149036293729  1 351174149036293778 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=51174149036293775, repcount=25587074518146888, factor=3/2
4605673[4]6643914   3535371[20]7364595    76761223554440617  1 32 476761223554440665 (4)A>
== Executing PPA-CTR  7 (once), V(1)=76761223554440664, V(2)=0
4605673[4]6643928   3535371[20]5127287    76761223554440619  1 376761223554440669 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=76761223554440666, repcount=38380611777220334, factor=3/2
6908510[4]9965932   7954585[20]6545295    1151418[4]1660953  1 3 41151418[4]1661003 (4)A>
== Executing PPA-CTR  2 (once), V(1)=1151418[4]1661000
6908510[4]9965941   7954585[20]9867316    1151418[4]1660954  22 31151418[4]1661003 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=1151418[4]1661000, repcount=57570917665830501, factor=3/2
1036276[5]4948947   1789781[21]3905329    1727127[4]7491455  22 3 41727127[4]7491504 (4)A>
== Executing PPA-CTR  8 (once), V(1)=1727127[4]7491501, V(2)=0
1036276[5]4948956   1789781[21]8888352    1727127[4]7491456  2 3 2 31727127[4]7491504 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=1727127[4]7491501, repcount=86356376498745751, factor=3/2
1554414[5]7423462   4027008[21]8007865    2590691[4]6237207  2 3 2 32 42590691[4]6237254 (4)A>
== Executing PPA-CTR 11 (once), V(1)=2590691[4]6237253
1554414[5]7423482   4027008[21]5431438    2590691[4]6237210  3 2 32590691[4]6237259 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=2590691[4]6237256, repcount=1295345[4]8118629, factor=3/2
2331622[5]6135256   9060769[21]7136651    3886036[4]4355839  3 2 3 43886036[4]4355888 (4)A>
== Executing PPA-CTR 12 (once), V(1)=3886036[4]4355885, V(2)=0
2331622[5]6135265   9060769[21]5848442    3886036[4]4355840  32 2 33886036[4]4355888 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=3886036[4]4355885, repcount=1943018[4]2177943, factor=3/2
3497433[5]9202923   2038673[22]4761619    5829055[4]6533783  32 2 32 45829055[4]6533830 (4)A>
3497433[5]9202924   2038673[22]4761620    5829055[4]6533784  32 2 32 45829055[4]6533831 (1)B>
3497433[5]9202925   2038673[22]4761622    5829055[4]6533782  32 2 32 45829055[4]6533831 <A(2)
3497433[5]9202926   2038673[22]1295453                  -49  32 2 32 <A(2) 25829055[4]6533831
3497433[5]9202927   2038673[22]1295454                  -50  32 2 3 <B(1) 25829055[4]6533832
3497433[5]9202928   2038673[22]1295458                  -48  32 2 4 (4)A> 25829055[4]6533832
3497433[5]9202929   2038673[22]7829290    5829055[4]6533784  32 2 45829055[4]6533833 (4)A>
3497433[5]9202930   2038673[22]7829291    5829055[4]6533785  32 2 45829055[4]6533834 (1)B>
3497433[5]9202931   2038673[22]7829293    5829055[4]6533783  32 2 45829055[4]6533834 <A(2)
3497433[5]9202932   2038673[22]4363127                  -51  32 2 <A(2) 25829055[4]6533834
3497433[5]9202933   2038673[22]4363129                  -49  32 4 (4)A> 25829055[4]6533834
3497433[5]9202934   2038673[22]0896963    5829055[4]6533785  32 45829055[4]6533835 (4)A>
3497433[5]9202935   2038673[22]0896964    5829055[4]6533786  32 45829055[4]6533836 (1)B>
3497433[5]9202936   2038673[22]0896966    5829055[4]6533784  32 45829055[4]6533836 <A(2)
3497433[5]9202937   2038673[22]7430802                  -52  32 <A(2) 25829055[4]6533836
3497433[5]9202938   2038673[22]7430803                  -53  3 <B(1) 25829055[4]6533837
3497433[5]9202939   2038673[22]7430807                  -51  4 (4)A> 25829055[4]6533837
3497433[5]9202940   2038673[22]3964644    5829055[4]6533786  45829055[4]6533838 (4)A>
3497433[5]9202941   2038673[22]3964645    5829055[4]6533787  45829055[4]6533839 (1)B>
3497433[5]9202942   2038673[22]3964647    5829055[4]6533785  45829055[4]6533839 <A(2)
3497433[5]9202943   2038673[22]0498486                  -54  <A(2) 25829055[4]6533839
3497433[5]9202944   2038673[22]0498488                  -52  1 (3)B> 25829055[4]6533839
3497433[5]9202945   2038673[22]7032327    5829055[4]6533787  1 35829055[4]6533839 (3)B>
3497433[5]9202946   2038673[22]7032329    5829055[4]6533785  1 35829055[4]6533839 <B(1)
3497433[5]9202947   2038673[22]7032333    5829055[4]6533787  1 35829055[4]6533838 4 (4)A>
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  32 2 32 41+V(1) (4)A>
    1                    1                    1  32 2 32 42+V(1) (1)B>
    2                    3                   -1  32 2 32 42+V(1) <A(2)
    3               5+V(1)           -3+-1*V(1)  32 2 32 <A(2) 22+V(1)
    4               6+V(1)           -4+-1*V(1)  32 2 3 <B(1) 23+V(1)
    5              10+V(1)           -2+-1*V(1)  32 2 4 (4)A> 23+V(1)
    6            13+2*V(1)                    1  32 2 44+V(1) (4)A>
    7            14+2*V(1)                    2  32 2 45+V(1) (1)B>
    8            16+2*V(1)                    0  32 2 45+V(1) <A(2)
    9            21+3*V(1)           -5+-1*V(1)  32 2 <A(2) 25+V(1)
   10            23+3*V(1)           -3+-1*V(1)  32 4 (4)A> 25+V(1)
   11            28+4*V(1)                    2  32 46+V(1) (4)A>
   12            29+4*V(1)                    3  32 47+V(1) (1)B>
   13            31+4*V(1)                    1  32 47+V(1) <A(2)
   14            38+5*V(1)           -6+-1*V(1)  32 <A(2) 27+V(1)
   15            39+5*V(1)           -7+-1*V(1)  3 <B(1) 28+V(1)
   16            43+5*V(1)           -5+-1*V(1)  4 (4)A> 28+V(1)
   17            51+6*V(1)                    3  49+V(1) (4)A>
   18            52+6*V(1)                    4  410+V(1) (1)B>
   19            54+6*V(1)                    2  410+V(1) <A(2)
   20            64+7*V(1)           -8+-1*V(1)  <A(2) 210+V(1)
   21            66+7*V(1)           -6+-1*V(1)  1 (3)B> 210+V(1)
   22            76+8*V(1)                    4  1 310+V(1) (3)B>
   23            78+8*V(1)                    2  1 310+V(1) <B(1)
   24            82+8*V(1)                    4  1 39+V(1) 4 (4)A>
<< Success! ==> defined new CTR 29 (PPA)
3497433[5]9202947   2038673[22]7032333    5829055[4]6533787  1 35829055[4]6533838 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=5829055[4]6533835, repcount=2914527[4]3266918, factor=3/2
5246149[5]8804455   4587014[22]9357685    8743583[4]9800705  1 32 48743583[4]9800755 (4)A>
== Executing PPA-CTR  7 (once), V(1)=8743583[4]9800754, V(2)=0
5246149[5]8804469   4587014[22]8560737    8743583[4]9800707  1 38743583[4]9800759 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=8743583[4]9800756, repcount=4371791[4]4900379, factor=3/2
7869224[5]8206743   1032078[23]0595450    1311537[5]4701086  1 3 41311537[5]4701138 (4)A>
== Executing PPA-CTR  2 (once), V(1)=1311537[5]4701135
7869224[5]8206752   1032078[23]9997741    1311537[5]4701087  22 31311537[5]4701138 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=1311537[5]4701135, repcount=6557687[4]7350568, factor=3/2
1180383[6]2310160   2322176[23]3271293    1967306[5]2051655  22 32 41967306[5]2051705 (4)A>
== Executing PPA-CTR 17 (once), V(1)=1967306[5]2051704, V(2)=0
1180383[6]2310165   2322176[23]5323007                  -51  22 4 (4)A> 21967306[5]2051707
== Executing  PA-CTR 15, V(1)=0, V(2)=1967306[5]2051706, repcount=1, factor=2/1
1180383[6]2310170   2322176[23]9426428                  -52  2 4 (4)A> 21967306[5]2051709
== Executing PPA-CTR 16 (once), V(1)=0, V(2)=1967306[5]2051708
1180383[6]2310183   2322176[23]9685001    1967306[5]2051659  1 31967306[5]2051712 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=1967306[5]2051709, repcount=9836531[4]6025855, factor=3/2
1770575[6]8465313   5224896[23]5386626    2950959[5]8077514  1 32 42950959[5]8077566 (4)A>
== Executing PPA-CTR  7 (once), V(1)=2950959[5]8077565, V(2)=0
1770575[6]8465327   5224896[23]7696922    2950959[5]8077516  1 32950959[5]8077570 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=2950959[5]8077567, repcount=1475479[5]4038784, factor=3/2
2655863[6]2698031   1175601[24]6680730    4426438[5]2116300  1 32 44426438[5]2116353 (4)A>
== Executing PPA-CTR  7 (once), V(1)=4426438[5]2116352, V(2)=0
2655863[6]2698045   1175601[24]5146174    4426438[5]2116302  1 34426438[5]2116357 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=4426438[5]2116354, repcount=2213219[5]6058178, factor=3/2
3983795[6]9047113   2645103[24]7767006    6639658[5]8174480  1 3 46639658[5]8174535 (4)A>
== Executing PPA-CTR  2 (once), V(1)=6639658[5]8174532
3983795[6]9047122   2645103[24]4116091    6639658[5]8174481  22 36639658[5]8174535 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=6639658[5]8174532, repcount=3319829[5]4087267, factor=3/2
5975692[6]3570724   5951483[24]9576628    9959487[5]2261748  22 3 49959487[5]2261802 (4)A>
== Executing PPA-CTR  8 (once), V(1)=9959487[5]2261799, V(2)=0
5975692[6]3570733   5951483[24]4100247    9959487[5]2261749  2 3 2 39959487[5]2261802 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=9959487[5]2261799, repcount=4979743[5]6130900, factor=3/2
8963538[6]0356133   1339083[25]9839247    1493923[6]8392649  2 3 2 32 41493923[6]8392701 (4)A>
== Executing PPA-CTR 11 (once), V(1)=1493923[6]8392700
8963538[6]0356153   1339083[25]0195502    1493923[6]8392652  3 2 31493923[6]8392706 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=1493923[6]8392703, repcount=7469615[5]4196352, factor=3/2
1344530[7]5534265   3012938[25]2482734    2240884[6]2589004  3 2 32 42240884[6]2589057 (4)A>
== Executing PPA-CTR 22 (once), V(1)=2240884[6]2589056
1344530[7]5534291   3012938[25]8017137    2240884[6]2589007  2 4 1 2 32240884[6]2589062 4 (4)A>
== Executing  PA-CTR  5, V(1)=0, V(2)=2240884[6]2589059, repcount=1120442[6]6294530, factor=3/2
2016796[7]3301471   6779111[25]4725137    3361327[6]8883537  2 4 1 2 32 43361327[6]8883591 (4)A>
== Executing PPA-CTR  6 (once), V(1)=3361327[6]8883590, V(2)=0, V(3)=0
2016796[7]3301496   6779111[25]5793941    3361327[6]8883541  1 33361327[6]8883600 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=3361327[6]8883597, repcount=1680663[6]4441799, factor=3/2
3025194[7]9952290   1525300[26]5281134    5041990[6]3325340  1 32 45041990[6]3325398 (4)A>
== Executing PPA-CTR  7 (once), V(1)=5041990[6]3325397, V(2)=0
3025194[7]9952304   1525300[26]8582758    5041990[6]3325342  1 35041990[6]3325402 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=5041990[6]3325399, repcount=2520995[6]6662700, factor=3/2
4537791[7]9928504   3431925[26]9079758    7562985[6]9988042  1 32 47562985[6]9988101 (4)A>
== Executing PPA-CTR  7 (once), V(1)=7562985[6]9988100, V(2)=0
4537791[7]9928518   3431925[26]9032194    7562985[6]9988044  1 37562985[6]9988105 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=7562985[6]9988102, repcount=3781492[6]9994052, factor=3/2
6806687[7]9892830   7721832[26]5108826    1134447[7]9982096  1 3 41134447[7]9982157 (4)A>
== Executing PPA-CTR  2 (once), V(1)=1134447[7]9982154
6806687[7]9892839   7721832[26]5073155    1134447[7]9982097  22 31134447[7]9982157 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=1134447[7]9982154, repcount=5672239[6]4991078, factor=3/2
1021003[8]9839307   1737412[27]3790187    1701671[7]4973175  22 3 41701671[7]4973235 (4)A>
== Executing PPA-CTR  8 (once), V(1)=1701671[7]4973232, V(2)=0
1021003[8]9839316   1737412[27]3736672    1701671[7]4973176  2 3 2 31701671[7]4973235 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=1701671[7]4973232, repcount=8508359[6]7486617, factor=3/2
1531504[8]4759018   3909177[27]0916909    2552507[7]2459793  2 3 2 3 42552507[7]2459852 (4)A>
== Executing PPA-CTR  9 (once), V(1)=2552507[7]2459849, V(2)=0
1531504[8]4759027   3909177[27]5836628    2552507[7]2459794  2 32 2 32552507[7]2459852 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=2552507[7]2459849, repcount=1276253[7]6229925, factor=3/2
2297256[8]2138577   8795649[27]4652753    3828761[7]8689719  2 32 2 32 43828761[7]8689776 (4)A>
== Executing PPA-CTR 10 (once), V(1)=3828761[7]8689775
2297256[8]2138606   8795649[27]1550614    3828761[7]8689724  1 33828761[7]8689786 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=3828761[7]8689783, repcount=1914380[7]4344892, factor=3/2
3445885[8]8207958   1979021[28]4474526    5743142[7]3034616  1 32 45743142[7]3034677 (4)A>
== Executing PPA-CTR  7 (once), V(1)=5743142[7]3034676, V(2)=0
3445885[8]8207972   1979021[28]6613266    5743142[7]3034618  1 35743142[7]3034681 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=5743142[7]3034678, repcount=2871571[7]6517340, factor=3/2
5168828[8]7312012   4452797[28]3813466    8614713[7]9551958  1 3 48614713[7]9552021 (4)A>
== Executing PPA-CTR  2 (once), V(1)=8614713[7]9552018
5168828[8]7312021   4452797[28]2917523    8614713[7]9551959  22 38614713[7]9552021 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=8614713[7]9552018, repcount=4307356[7]9776010, factor=3/2
7753242[8]5968081   1001879[29]5237923    1292207[8]9327969  22 3 41292207[8]9328031 (4)A>
== Executing PPA-CTR  8 (once), V(1)=1292207[8]9328028, V(2)=0
7753242[8]5968090   1001879[29]3894000    1292207[8]9327970  2 3 2 31292207[8]9328031 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=1292207[8]9328028, repcount=6461035[7]9664015, factor=3/2
1162986[9]3952180   2254228[29]8294825    1938310[8]8991985  2 3 2 3 41938310[8]8992046 (4)A>
== Executing PPA-CTR  9 (once), V(1)=1938310[8]8992043, V(2)=0
1162986[9]3952189   2254228[29]6278932    1938310[8]8991986  2 32 2 31938310[8]8992046 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=1938310[8]8992043, repcount=9691552[7]4496022, factor=3/2
1744479[9]0928321   5072014[29]2712604    2907465[8]3488008  2 32 2 32 42907465[8]3488067 (4)A>
== Executing PPA-CTR 10 (once), V(1)=2907465[8]3488066
1744479[9]0928350   5072014[29]7593375    2907465[8]3488013  1 32907465[8]3488077 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=2907465[8]3488074, repcount=1453732[8]1744038, factor=3/2
2616719[9]1392578   1141203[30]0670087    4361198[8]5232051  1 3 44361198[8]5232115 (4)A>
== Executing PPA-CTR  2 (once), V(1)=4361198[8]5232112
2616719[9]1392587   1141203[30]1134332    4361198[8]5232052  22 34361198[8]5232115 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=4361198[8]5232112, repcount=2180599[8]2616057, factor=3/2
3925078[9]7088929   2567707[30]9976649    6541798[8]7848109  22 3 46541798[8]7848172 (4)A>
== Executing PPA-CTR  8 (once), V(1)=6541798[8]7848169, V(2)=0
3925078[9]7088938   2567707[30]5673008    6541798[8]7848110  2 3 2 36541798[8]7848172 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=6541798[8]7848169, repcount=3270899[8]8924085, factor=3/2
5887618[9]0633448   5777341[30]4175533    9812697[8]6772195  2 3 2 32 49812697[8]6772256 (4)A>
== Executing PPA-CTR 11 (once), V(1)=9812697[8]6772255
5887618[9]0633468   5777341[30]4809118    9812697[8]6772198  3 2 39812697[8]6772261 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=9812697[8]6772258, repcount=4906348[8]3386130, factor=3/2
8831427[9]0950248   1299901[31]7801118    1471904[9]0158328  3 2 3 41471904[9]0158391 (4)A>
== Executing PPA-CTR 12 (once), V(1)=1471904[9]0158388, V(2)=0
8831427[9]0950257   1299901[31]8117915    1471904[9]0158329  32 2 31471904[9]0158391 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=1471904[9]0158388, repcount=7359522[8]5079195, factor=3/2
1324714[10]1425427   2924779[31]4453940    2207856[9]5237524  32 2 3 42207856[9]5237586 (4)A>
== Executing PPA-CTR 12 (once), V(1)=2207856[9]5237583, V(2)=1
1324714[10]1425436   2924779[31]4929127    2207856[9]5237525  33 2 32207856[9]5237586 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=2207856[9]5237583, repcount=1103928[9]7618792, factor=3/2
1987071[10]7138188   6580753[31]5734839    3311785[9]2856317  33 2 32 43311785[9]2856377 (4)A>
== Executing PPA-CTR 20 (once), V(1)=3311785[9]2856376, V(2)=0
1987071[10]7138198   6580753[31]4303990                  -62  33 4 (4)A> 23311785[9]2856381
== Executing  PA-CTR 13, V(1)=0, V(2)=3311785[9]2856380, repcount=1, factor=3/2
1987071[10]7138204   6580753[31]0016762                  -64  3 4 (4)A> 23311785[9]2856384
== Executing PPA-CTR 21 (once), V(1)=0, V(2)=3311785[9]2856382
1987071[10]7138220   6580753[31]8585943    3311785[9]2856321  2 4 1 2 33311785[9]2856385 4 (4)A>
== Executing  PA-CTR  5, V(1)=0, V(2)=3311785[9]2856382, repcount=1655892[9]6428192, factor=3/2
2980606[10]5707372   1480669[32]0034455    4967677[9]9284513  2 4 1 2 3 44967677[9]9284577 (4)A>
2980606[10]5707373   1480669[32]0034456    4967677[9]9284514  2 4 1 2 3 44967677[9]9284578 (1)B>
2980606[10]5707374   1480669[32]0034458    4967677[9]9284512  2 4 1 2 3 44967677[9]9284578 <A(2)
2980606[10]5707375   1480669[32]9319036                  -66  2 4 1 2 3 <A(2) 24967677[9]9284578
2980606[10]5707376   1480669[32]9319037                  -67  2 4 1 2 <B(1) 24967677[9]9284579
2980606[10]5707377   1480669[32]9319039                  -65  2 4 1 3 (2)B> 24967677[9]9284579
2980606[10]5707378   1480669[32]9319040                  -64  2 4 1 3 2 (3)B> 24967677[9]9284578
2980606[10]5707379   1480669[32]8603618    4967677[9]9284514  2 4 1 3 2 34967677[9]9284578 (3)B>
2980606[10]5707380   1480669[32]8603620    4967677[9]9284512  2 4 1 3 2 34967677[9]9284578 <B(1)
2980606[10]5707381   1480669[32]8603624    4967677[9]9284514  2 4 1 3 2 34967677[9]9284577 4 (4)A>
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  [*]* [*]* [*]* 2 3 43+V(1) (4)A>
    1                    1                    1  [*]* [*]* [*]* 2 3 44+V(1) (1)B>
    2                    3                   -1  [*]* [*]* [*]* 2 3 44+V(1) <A(2)
    3               7+V(1)           -5+-1*V(1)  [*]* [*]* [*]* 2 3 <A(2) 24+V(1)
    4               8+V(1)           -6+-1*V(1)  [*]* [*]* [*]* 2 <B(1) 25+V(1)
    5              10+V(1)           -4+-1*V(1)  [*]* [*]* [*]* 3 (2)B> 25+V(1)
    6              11+V(1)           -3+-1*V(1)  [*]* [*]* [*]* 3 2 (3)B> 24+V(1)
    7            15+2*V(1)                    1  [*]* [*]* [*]* 3 2 34+V(1) (3)B>
    8            17+2*V(1)                   -1  [*]* [*]* [*]* 3 2 34+V(1) <B(1)
    9            21+2*V(1)                    1  [*]* [*]* [*]* 3 2 33+V(1) 4 (4)A>
<< Success! ==> defined new CTR 30 (PPA)
2980606[10]5707381   1480669[32]8603624    4967677[9]9284514  2 4 1 3 2 34967677[9]9284577 4 (4)A>
== Executing  PA-CTR 23, V(1)=0, V(2)=4967677[9]9284574, repcount=2483838[9]4642288, factor=3/2
4470910[10]3561109   3331506[32]8651336    7451516[9]3926802  2 4 1 3 2 3 47451516[9]3926865 (4)A>
== Executing PPA-CTR 24 (once), V(1)=7451516[9]3926862, V(2)=0
4470910[10]3561118   3331506[32]6505081    7451516[9]3926803  2 4 1 32 2 37451516[9]3926865 4 (4)A>
== Executing  PA-CTR 23, V(1)=0, V(2)=7451516[9]3926862, repcount=3725758[9]1963432, factor=3/2
6706365[10]5341710   7495889[32]1795273   1117727[10]5890235  2 4 1 32 2 3 41117727[10]5890297 (4)A>
== Executing PPA-CTR 24 (once), V(1)=1117727[10]5890294, V(2)=1
6706365[10]5341719   7495889[32]3575882   1117727[10]5890236  2 4 1 33 2 31117727[10]5890297 4 (4)A>
== Executing  PA-CTR 23, V(1)=0, V(2)=1117727[10]5890294, repcount=5588637[9]7945148, factor=3/2
1005954[11]3012607   1686575[33]3253074   1676591[10]3835384  2 4 1 33 2 3 41676591[10]3835445 (4)A>
== Executing PPA-CTR 24 (once), V(1)=1676591[10]3835442, V(2)=2
1005954[11]3012616   1686575[33]0923979   1676591[10]3835385  2 4 1 34 2 31676591[10]3835445 4 (4)A>
== Executing  PA-CTR 23, V(1)=0, V(2)=1676591[10]3835442, repcount=8382956[9]6917722, factor=3/2
1508932[11]4518948   3794793[33]3109051   2514886[10]0753107  2 4 1 34 2 3 42514886[10]0753167 (4)A>
== Executing PPA-CTR 24 (once), V(1)=2514886[10]0753164, V(2)=3
1508932[11]4518957   3794793[33]4615400   2514886[10]0753108  2 4 1 35 2 32514886[10]0753167 4 (4)A>
== Executing  PA-CTR 23, V(1)=0, V(2)=2514886[10]0753164, repcount=1257443[10]0376583, factor=3/2
2263398[11]6778455   8538286[33]2648897   3772330[10]1129691  2 4 1 35 2 3 43772330[10]1129750 (4)A>
== Executing PPA-CTR 24 (once), V(1)=3772330[10]1129747, V(2)=4
2263398[11]6778464   8538286[33]4908412   3772330[10]1129692  2 4 1 36 2 33772330[10]1129750 4 (4)A>
== Executing  PA-CTR 23, V(1)=0, V(2)=3772330[10]1129747, repcount=1886165[10]0564874, factor=3/2
3395097[11]0167708   1921114[34]8464780   5658495[10]1694566  2 4 1 36 2 32 45658495[10]1694623 (4)A>
== Executing PPA-CTR 25 (once), V(1)=5658495[10]1694622, V(2)=3
3395097[11]0167719   1921114[34]5243296   5658495[10]1694568  2 4 1 36 45658495[10]1694628 (4)A>
== Executing  PA-CTR  3, V(1)=5658495[10]1694627, V(2)=3, repcount=2, factor=3/2
3395097[11]0167731   1921114[34]2021836   5658495[10]1694570  2 4 1 32 45658495[10]1694634 (4)A>
3395097[11]0167732   1921114[34]2021837   5658495[10]1694571  2 4 1 32 45658495[10]1694635 (1)B>
3395097[11]0167733   1921114[34]2021839   5658495[10]1694569  2 4 1 32 45658495[10]1694635 <A(2)
3395097[11]0167734   1921114[34]3716474                  -66  2 4 1 32 <A(2) 25658495[10]1694635
3395097[11]0167735   1921114[34]3716475                  -67  2 4 1 3 <B(1) 25658495[10]1694636
3395097[11]0167736   1921114[34]3716479                  -65  2 4 1 4 (4)A> 25658495[10]1694636
3395097[11]0167737   1921114[34]5411115   5658495[10]1694571  2 4 1 45658495[10]1694637 (4)A>
3395097[11]0167738   1921114[34]5411116   5658495[10]1694572  2 4 1 45658495[10]1694638 (1)B>
3395097[11]0167739   1921114[34]5411118   5658495[10]1694570  2 4 1 45658495[10]1694638 <A(2)
3395097[11]0167740   1921114[34]7105756                  -68  2 4 1 <A(2) 25658495[10]1694638
3395097[11]0167741   1921114[34]7105757                  -69  2 4 <A(2) 25658495[10]1694639
3395097[11]0167742   1921114[34]7105758                  -70  2 <A(2) 25658495[10]1694640
3395097[11]0167743   1921114[34]7105760                  -68  4 (4)A> 25658495[10]1694640
3395097[11]0167744   1921114[34]8800400   5658495[10]1694572  45658495[10]1694641 (4)A>
3395097[11]0167745   1921114[34]8800401   5658495[10]1694573  45658495[10]1694642 (1)B>
3395097[11]0167746   1921114[34]8800403   5658495[10]1694571  45658495[10]1694642 <A(2)
3395097[11]0167747   1921114[34]0495045                  -71  <A(2) 25658495[10]1694642
3395097[11]0167748   1921114[34]0495047                  -69  1 (3)B> 25658495[10]1694642
3395097[11]0167749   1921114[34]2189689   5658495[10]1694573  1 35658495[10]1694642 (3)B>
3395097[11]0167750   1921114[34]2189691   5658495[10]1694571  1 35658495[10]1694642 <B(1)
3395097[11]0167751   1921114[34]2189695   5658495[10]1694573  1 35658495[10]1694641 4 (4)A>
>> Try to prove a PPA-CTR with 3 Vars...
    0                    0                    0  2 41+V(3) 11+V(2) 32 41+V(1) (4)A>
    1                    1                    1  2 41+V(3) 11+V(2) 32 42+V(1) (1)B>
    2                    3                   -1  2 41+V(3) 11+V(2) 32 42+V(1) <A(2)
    3               5+V(1)           -3+-1*V(1)  2 41+V(3) 11+V(2) 32 <A(2) 22+V(1)
    4               6+V(1)           -4+-1*V(1)  2 41+V(3) 11+V(2) 3 <B(1) 23+V(1)
    5              10+V(1)           -2+-1*V(1)  2 41+V(3) 11+V(2) 4 (4)A> 23+V(1)
    6            13+2*V(1)                    1  2 41+V(3) 11+V(2) 44+V(1) (4)A>
    7            14+2*V(1)                    2  2 41+V(3) 11+V(2) 45+V(1) (1)B>
    8            16+2*V(1)                    0  2 41+V(3) 11+V(2) 45+V(1) <A(2)
    9            21+3*V(1)           -5+-1*V(1)  2 41+V(3) 11+V(2) <A(2) 25+V(1)
   10       22+3*V(1)+V(2)   -6+-1*V(1)+-1*V(2)  2 41+V(3) <A(2) 26+V(1)+V(2)
   11  23+3*V(1)+V(2)+V(3) -7+-1*V(1)+-1*V(2)+-1*V(3)  2 <A(2) 27+V(1)+V(2)+V(3)
   12  25+3*V(1)+V(2)+V(3) -5+-1*V(1)+-1*V(2)+-1*V(3)  4 (4)A> 27+V(1)+V(2)+V(3)
   13 32+4*V(1)+2*V(2)+2*V(3)                    2  48+V(1)+V(2)+V(3) (4)A>
   14 33+4*V(1)+2*V(2)+2*V(3)                    3  49+V(1)+V(2)+V(3) (1)B>
   15 35+4*V(1)+2*V(2)+2*V(3)                    1  49+V(1)+V(2)+V(3) <A(2)
   16 44+5*V(1)+3*V(2)+3*V(3) -8+-1*V(1)+-1*V(2)+-1*V(3)  <A(2) 29+V(1)+V(2)+V(3)
   17 46+5*V(1)+3*V(2)+3*V(3) -6+-1*V(1)+-1*V(2)+-1*V(3)  1 (3)B> 29+V(1)+V(2)+V(3)
   18 55+6*V(1)+4*V(2)+4*V(3)                    3  1 39+V(1)+V(2)+V(3) (3)B>
   19 57+6*V(1)+4*V(2)+4*V(3)                    1  1 39+V(1)+V(2)+V(3) <B(1)
   20 61+6*V(1)+4*V(2)+4*V(3)                    3  1 38+V(1)+V(2)+V(3) 4 (4)A>
<< Success! ==> defined new CTR 31 (PPA)
3395097[11]0167751   1921114[34]2189695   5658495[10]1694573  1 35658495[10]1694641 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=5658495[10]1694638, repcount=2829247[10]5847320, factor=3/2
5092646[11]5251671   4322507[34]4210095   8487743[10]7541893  1 3 48487743[10]7541961 (4)A>
== Executing PPA-CTR  2 (once), V(1)=8487743[10]7541958
5092646[11]5251680   4322507[34]9294032   8487743[10]7541894  22 38487743[10]7541961 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=8487743[10]7541958, repcount=4243871[10]3770980, factor=3/2
7638969[11]7877560   9725641[34]7485032   1273161[11]1312874  22 3 41273161[11]1312941 (4)A>
== Executing PPA-CTR  8 (once), V(1)=1273161[11]1312938, V(2)=0
7638969[11]7877569   9725641[34]0110929   1273161[11]1312875  2 3 2 31273161[11]1312941 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=1273161[11]1312938, repcount=6365807[10]0656470, factor=3/2
1145845[12]1816389   2188269[35]5258329   1909742[11]1969345  2 3 2 3 41909742[11]1969411 (4)A>
== Executing PPA-CTR  9 (once), V(1)=1909742[11]1969408, V(2)=0
1145845[12]1816398   2188269[35]9197166   1909742[11]1969346  2 32 2 31909742[11]1969411 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=1909742[11]1969408, repcount=9548711[10]0984705, factor=3/2
1718768[12]7724628   4923606[35]0855291   2864613[11]2954051  2 32 2 3 42864613[11]2954116 (4)A>
== Executing PPA-CTR  9 (once), V(1)=2864613[11]2954113, V(2)=1
1718768[12]7724637   4923606[35]6763538   2864613[11]2954052  2 33 2 32864613[11]2954116 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=2864613[11]2954113, repcount=1432306[11]6477057, factor=3/2
2578152[12]6586979   1107811[36]3677855   4296920[11]9431109  2 33 2 32 44296920[11]9431172 (4)A>
== Executing PPA-CTR 18 (once), V(1)=4296920[11]9431171, V(2)=0
2578152[12]6586990   1107811[36]1402567   4296920[11]9431111  2 33 44296920[11]9431177 (4)A>
== Executing  PA-CTR  1, V(1)=4296920[11]9431176, V(2)=0, repcount=1, factor=3/2
2578152[12]6586996   1107811[36]0264932   4296920[11]9431112  2 3 44296920[11]9431180 (4)A>
== Executing PPA-CTR 19 (once), V(1)=4296920[11]9431177
2578152[12]6587005   1107811[36]9127307   4296920[11]9431113  3 2 34296920[11]9431180 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=4296920[11]9431177, repcount=2148460[11]9715589, factor=3/2
3867228[12]4880539   2492575[36]5133960   6445380[11]9146702  3 2 32 46445380[11]9146768 (4)A>
== Executing PPA-CTR 22 (once), V(1)=6445380[11]9146767
3867228[12]4880565   2492575[36]0014629   6445380[11]9146705  2 4 1 2 36445380[11]9146773 4 (4)A>
== Executing  PA-CTR  5, V(1)=0, V(2)=6445380[11]9146770, repcount=3222690[11]9573386, factor=3/2
5800842[12]2320881   5608295[36]4263477   9668070[11]8720091  2 4 1 2 3 49668070[11]8720159 (4)A>
== Executing PPA-CTR 30 (once), V(1)=9668070[11]8720156
5800842[12]2320890   5608295[36]1703810   9668070[11]8720092  2 4 1 3 2 39668070[11]8720159 4 (4)A>
== Executing  PA-CTR 23, V(1)=0, V(2)=9668070[11]8720156, repcount=4834035[11]4360079, factor=3/2
8701263[12]8481364   1261866[37]1963323   1450210[12]3080171  2 4 1 3 2 3 41450210[12]3080238 (4)A>
== Executing PPA-CTR 24 (once), V(1)=1450210[12]3080235, V(2)=0
8701263[12]8481373   1261866[37]8123814   1450210[12]3080172  2 4 1 32 2 31450210[12]3080238 4 (4)A>
== Executing  PA-CTR 23, V(1)=0, V(2)=1450210[12]3080235, repcount=7251052[11]6540118, factor=3/2
1305189[13]7722081   2839199[37]3886766   2175315[12]9620290  2 4 1 32 2 32 42175315[12]9620355 (4)A>
1305189[13]7722082   2839199[37]3886767   2175315[12]9620291  2 4 1 32 2 32 42175315[12]9620356 (1)B>
1305189[13]7722083   2839199[37]3886769   2175315[12]9620289  2 4 1 32 2 32 42175315[12]9620356 <A(2)
1305189[13]7722084   2839199[37]3507125                  -67  2 4 1 32 2 32 <A(2) 22175315[12]9620356
1305189[13]7722085   2839199[37]3507126                  -68  2 4 1 32 2 3 <B(1) 22175315[12]9620357
1305189[13]7722086   2839199[37]3507130                  -66  2 4 1 32 2 4 (4)A> 22175315[12]9620357
1305189[13]7722087   2839199[37]3127487   2175315[12]9620291  2 4 1 32 2 42175315[12]9620358 (4)A>
1305189[13]7722088   2839199[37]3127488   2175315[12]9620292  2 4 1 32 2 42175315[12]9620359 (1)B>
1305189[13]7722089   2839199[37]3127490   2175315[12]9620290  2 4 1 32 2 42175315[12]9620359 <A(2)
1305189[13]7722090   2839199[37]2747849                  -69  2 4 1 32 2 <A(2) 22175315[12]9620359
1305189[13]7722091   2839199[37]2747851                  -67  2 4 1 32 4 (4)A> 22175315[12]9620359
1305189[13]7722092   2839199[37]2368210   2175315[12]9620292  2 4 1 32 42175315[12]9620360 (4)A>
1305189[13]7722093   2839199[37]2368211   2175315[12]9620293  2 4 1 32 42175315[12]9620361 (1)B>
1305189[13]7722094   2839199[37]2368213   2175315[12]9620291  2 4 1 32 42175315[12]9620361 <A(2)
1305189[13]7722095   2839199[37]1988574                  -70  2 4 1 32 <A(2) 22175315[12]9620361
1305189[13]7722096   2839199[37]1988575                  -71  2 4 1 3 <B(1) 22175315[12]9620362
1305189[13]7722097   2839199[37]1988579                  -69  2 4 1 4 (4)A> 22175315[12]9620362
1305189[13]7722098   2839199[37]1608941   2175315[12]9620293  2 4 1 42175315[12]9620363 (4)A>
1305189[13]7722099   2839199[37]1608942   2175315[12]9620294  2 4 1 42175315[12]9620364 (1)B>
1305189[13]7722100   2839199[37]1608944   2175315[12]9620292  2 4 1 42175315[12]9620364 <A(2)
1305189[13]7722101   2839199[37]1229308                  -72  2 4 1 <A(2) 22175315[12]9620364
1305189[13]7722102   2839199[37]1229309                  -73  2 4 <A(2) 22175315[12]9620365
1305189[13]7722103   2839199[37]1229310                  -74  2 <A(2) 22175315[12]9620366
1305189[13]7722104   2839199[37]1229312                  -72  4 (4)A> 22175315[12]9620366
1305189[13]7722105   2839199[37]0849678   2175315[12]9620294  42175315[12]9620367 (4)A>
1305189[13]7722106   2839199[37]0849679   2175315[12]9620295  42175315[12]9620368 (1)B>
1305189[13]7722107   2839199[37]0849681   2175315[12]9620293  42175315[12]9620368 <A(2)
1305189[13]7722108   2839199[37]0470049                  -75  <A(2) 22175315[12]9620368
1305189[13]7722109   2839199[37]0470051                  -73  1 (3)B> 22175315[12]9620368
1305189[13]7722110   2839199[37]0090419   2175315[12]9620295  1 32175315[12]9620368 (3)B>
1305189[13]7722111   2839199[37]0090421   2175315[12]9620293  1 32175315[12]9620368 <B(1)
1305189[13]7722112   2839199[37]0090425   2175315[12]9620295  1 32175315[12]9620367 4 (4)A>
>> Try to prove a PPA-CTR with 3 Vars...
    0                    0                    0  2 41+V(3) 11+V(2) 32 2 32 41+V(1) (4)A>
    1                    1                    1  2 41+V(3) 11+V(2) 32 2 32 42+V(1) (1)B>
    2                    3                   -1  2 41+V(3) 11+V(2) 32 2 32 42+V(1) <A(2)
    3               5+V(1)           -3+-1*V(1)  2 41+V(3) 11+V(2) 32 2 32 <A(2) 22+V(1)
    4               6+V(1)           -4+-1*V(1)  2 41+V(3) 11+V(2) 32 2 3 <B(1) 23+V(1)
    5              10+V(1)           -2+-1*V(1)  2 41+V(3) 11+V(2) 32 2 4 (4)A> 23+V(1)
    6            13+2*V(1)                    1  2 41+V(3) 11+V(2) 32 2 44+V(1) (4)A>
    7            14+2*V(1)                    2  2 41+V(3) 11+V(2) 32 2 45+V(1) (1)B>
    8            16+2*V(1)                    0  2 41+V(3) 11+V(2) 32 2 45+V(1) <A(2)
    9            21+3*V(1)           -5+-1*V(1)  2 41+V(3) 11+V(2) 32 2 <A(2) 25+V(1)
   10            23+3*V(1)           -3+-1*V(1)  2 41+V(3) 11+V(2) 32 4 (4)A> 25+V(1)
   11            28+4*V(1)                    2  2 41+V(3) 11+V(2) 32 46+V(1) (4)A>
   12            29+4*V(1)                    3  2 41+V(3) 11+V(2) 32 47+V(1) (1)B>
   13            31+4*V(1)                    1  2 41+V(3) 11+V(2) 32 47+V(1) <A(2)
   14            38+5*V(1)           -6+-1*V(1)  2 41+V(3) 11+V(2) 32 <A(2) 27+V(1)
   15            39+5*V(1)           -7+-1*V(1)  2 41+V(3) 11+V(2) 3 <B(1) 28+V(1)
   16            43+5*V(1)           -5+-1*V(1)  2 41+V(3) 11+V(2) 4 (4)A> 28+V(1)
   17            51+6*V(1)                    3  2 41+V(3) 11+V(2) 49+V(1) (4)A>
   18            52+6*V(1)                    4  2 41+V(3) 11+V(2) 410+V(1) (1)B>
   19            54+6*V(1)                    2  2 41+V(3) 11+V(2) 410+V(1) <A(2)
   20            64+7*V(1)           -8+-1*V(1)  2 41+V(3) 11+V(2) <A(2) 210+V(1)
   21       65+7*V(1)+V(2)   -9+-1*V(1)+-1*V(2)  2 41+V(3) <A(2) 211+V(1)+V(2)
   22  66+7*V(1)+V(2)+V(3) -10+-1*V(1)+-1*V(2)+-1*V(3)  2 <A(2) 212+V(1)+V(2)+V(3)
   23  68+7*V(1)+V(2)+V(3) -8+-1*V(1)+-1*V(2)+-1*V(3)  4 (4)A> 212+V(1)+V(2)+V(3)
   24 80+8*V(1)+2*V(2)+2*V(3)                    4  413+V(1)+V(2)+V(3) (4)A>
   25 81+8*V(1)+2*V(2)+2*V(3)                    5  414+V(1)+V(2)+V(3) (1)B>
   26 83+8*V(1)+2*V(2)+2*V(3)                    3  414+V(1)+V(2)+V(3) <A(2)
   27 97+9*V(1)+3*V(2)+3*V(3) -11+-1*V(1)+-1*V(2)+-1*V(3)  <A(2) 214+V(1)+V(2)+V(3)
   28 99+9*V(1)+3*V(2)+3*V(3) -9+-1*V(1)+-1*V(2)+-1*V(3)  1 (3)B> 214+V(1)+V(2)+V(3)
   29 113+10*V(1)+4*V(2)+4*V(3)                    5  1 314+V(1)+V(2)+V(3) (3)B>
   30 115+10*V(1)+4*V(2)+4*V(3)                    3  1 314+V(1)+V(2)+V(3) <B(1)
   31 119+10*V(1)+4*V(2)+4*V(3)                    5  1 313+V(1)+V(2)+V(3) 4 (4)A>
<< Success! ==> defined new CTR 32 (PPA)
1305189[13]7722112   2839199[37]0090425   2175315[12]9620295  1 32175315[12]9620367 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=2175315[12]9620364, repcount=1087657[12]4810183, factor=3/2
1957784[13]6583210   6388198[37]9672722   3262973[12]4430478  1 3 43262973[12]4430550 (4)A>
== Executing PPA-CTR  2 (once), V(1)=3262973[12]4430547
1957784[13]6583219   6388198[37]8533837   3262973[12]4430479  22 33262973[12]4430550 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=3262973[12]4430547, repcount=1631486[12]7215274, factor=3/2
2936676[13]9874863   1437344[38]7371805   4894460[12]1645753  22 32 44894460[12]1645823 (4)A>
== Executing PPA-CTR 17 (once), V(1)=4894460[12]1645822, V(2)=0
2936676[13]9874868   1437344[38]9017637                  -71  22 4 (4)A> 24894460[12]1645825
== Executing  PA-CTR 15, V(1)=0, V(2)=4894460[12]1645824, repcount=1, factor=2/1
2936676[13]9874873   1437344[38]2309294                  -72  2 4 (4)A> 24894460[12]1645827
== Executing PPA-CTR 16 (once), V(1)=0, V(2)=4894460[12]1645826
2936676[13]9874886   1437344[38]0538457   4894460[12]1645757  1 34894460[12]1645830 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=4894460[12]1645827, repcount=2447230[12]5822914, factor=3/2
4405014[13]4812370   3234025[38]1121785   7341690[12]7468671  1 32 47341690[12]7468743 (4)A>
== Executing PPA-CTR  7 (once), V(1)=7341690[12]7468742, V(2)=0
4405014[13]4812384   3234025[38]0996789   7341690[12]7468673  1 37341690[12]7468747 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=7341690[12]7468744, repcount=3670845[12]8734373, factor=3/2
6607521[13]7218622   7276557[38]3449906   1101253[13]6203046  1 3 41101253[13]6203120 (4)A>
== Executing PPA-CTR  2 (once), V(1)=1101253[13]6203117
6607521[13]7218631   7276557[38]5856161   1101253[13]6203047  22 31101253[13]6203120 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=1101253[13]6203117, repcount=5506268[12]3101559, factor=3/2
9911282[13]5827985   1637225[39]1563194   1651880[13]9304606  22 32 41651880[13]9304678 (4)A>
== Executing PPA-CTR 17 (once), V(1)=1651880[13]9304677, V(2)=0
9911282[13]5827990   1637225[39]0867881                  -73  22 4 (4)A> 21651880[13]9304680
== Executing  PA-CTR 15, V(1)=0, V(2)=1651880[13]9304679, repcount=1, factor=2/1
9911282[13]5827995   1637225[39]9477248                  -74  2 4 (4)A> 21651880[13]9304682
== Executing PPA-CTR 16 (once), V(1)=0, V(2)=1651880[13]9304681
9911282[13]5828008   1637225[39]6000686   1651880[13]9304610  1 31651880[13]9304685 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=1651880[13]9304682, repcount=8259402[12]9652342, factor=3/2
1486692[14]3742060   3683757[39]0778998   2477820[13]8956952  1 3 42477820[13]8957027 (4)A>
== Executing PPA-CTR  2 (once), V(1)=2477820[13]8957024
1486692[14]3742069   3683757[39]8693067   2477820[13]8956953  22 32477820[13]8957027 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=2477820[13]8957024, repcount=1238910[13]9478513, factor=3/2
2230038[14]0613147   8288453[39]9551704   3716731[13]8435466  22 3 43716731[13]8435540 (4)A>
== Executing PPA-CTR  8 (once), V(1)=3716731[13]8435537, V(2)=0
2230038[14]0613156   8288453[39]6422799   3716731[13]8435467  2 3 2 33716731[13]8435540 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=3716731[13]8435537, repcount=1858365[13]9217769, factor=3/2
3345057[14]5919770   1864902[40]4612572   5575096[13]7653236  2 3 2 32 45575096[13]7653308 (4)A>
== Executing PPA-CTR 11 (once), V(1)=5575096[13]7653307
3345057[14]5919790   1864902[40]0532469   5575096[13]7653239  3 2 35575096[13]7653313 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=5575096[13]7653310, repcount=2787548[13]3826656, factor=3/2
5017586[14]8879726   4196029[40]7226037   8362644[13]1479895  3 2 3 48362644[13]1479969 (4)A>
== Executing PPA-CTR 12 (once), V(1)=8362644[13]1479966, V(2)=0
5017586[14]8879735   4196029[40]0185990   8362644[13]1479896  32 2 38362644[13]1479969 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=8362644[13]1479966, repcount=4181322[13]0739984, factor=3/2
7526380[14]3319639   9441066[40]6546598   1254396[14]2219880  32 2 3 41254396[14]2219953 (4)A>
== Executing PPA-CTR 12 (once), V(1)=1254396[14]2219950, V(2)=1
7526380[14]3319648   9441066[40]0986519   1254396[14]2219881  33 2 31254396[14]2219953 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=1254396[14]2219950, repcount=6271983[13]1109976, factor=3/2
1128957[15]9979504   2124240[41]2248007   1881595[14]3329857  33 2 3 41881595[14]3329929 (4)A>
== Executing PPA-CTR 12 (once), V(1)=1881595[14]3329926, V(2)=2
1128957[15]9979513   2124240[41]8907880   1881595[14]3329858  34 2 31881595[14]3329929 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=1881595[14]3329926, repcount=9407975[13]1664964, factor=3/2
1693435[15]9969297   4779540[41]0921408   2822392[14]4994822  34 2 3 42822392[14]4994893 (4)A>
== Executing PPA-CTR 12 (once), V(1)=2822392[14]4994890, V(2)=3
1693435[15]9969306   4779540[41]0911209   2822392[14]4994823  35 2 32822392[14]4994893 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=2822392[14]4994890, repcount=1411196[14]7497446, factor=3/2
2540153[15]4953982   1075396[42]5454417   4233588[14]2492269  35 2 3 44233588[14]2492339 (4)A>
== Executing PPA-CTR 12 (once), V(1)=4233588[14]2492336, V(2)=4
2540153[15]4953991   1075396[42]0439110   4233588[14]2492270  36 2 34233588[14]2492339 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=4233588[14]2492336, repcount=2116794[14]1246169, factor=3/2
3810230[15]2431005   2419642[42]4430483   6350383[14]3738439  36 2 3 46350383[14]3738508 (4)A>
== Executing PPA-CTR 12 (once), V(1)=6350383[14]3738505, V(2)=5
3810230[15]2431014   2419642[42]1907514   6350383[14]3738440  37 2 36350383[14]3738508 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=6350383[14]3738505, repcount=3175191[14]1869253, factor=3/2
5715345[15]3646532   5444194[42]0934071   9525575[14]5607693  37 2 32 49525575[14]5607760 (4)A>
== Executing PPA-CTR 20 (once), V(1)=9525575[14]5607759, V(2)=4
5715345[15]3646542   5444194[42]7757371                  -69  37 4 (4)A> 29525575[14]5607764
== Executing  PA-CTR 13, V(1)=4, V(2)=9525575[14]5607763, repcount=3, factor=3/2
5715345[15]3646560   5444194[42]1404003                  -75  3 4 (4)A> 29525575[14]5607773
== Executing PPA-CTR 21 (once), V(1)=0, V(2)=9525575[14]5607771
5715345[15]3646576   5444194[42]8227351   9525575[14]5607699  2 4 1 2 39525575[14]5607774 4 (4)A>
== Executing  PA-CTR  5, V(1)=0, V(2)=9525575[14]5607771, repcount=4762787[14]7803886, factor=3/2
8573017[15]0469892   1224943[43]6369199   1428836[15]3411585  2 4 1 2 32 41428836[15]3411659 (4)A>
== Executing PPA-CTR  6 (once), V(1)=1428836[15]3411658, V(2)=0, V(3)=0
8573017[15]0469917   1224943[43]3662547   1428836[15]3411589  1 31428836[15]3411668 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=1428836[15]3411665, repcount=7144181[14]1705833, factor=3/2
1285952[16]0704915   2756123[43]9392544   2143254[15]5117422  1 32 42143254[15]5117500 (4)A>
== Executing PPA-CTR  7 (once), V(1)=2143254[15]5117499, V(2)=0
1285952[16]0704929   2756123[43]9862576   2143254[15]5117424  1 32143254[15]5117504 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=2143254[15]5117501, repcount=1071627[15]7558751, factor=3/2
1928928[16]6057435   6201278[43]5490089   3214881[15]2676175  1 32 43214881[15]2676254 (4)A>
== Executing PPA-CTR  7 (once), V(1)=3214881[15]2676253, V(2)=0
1928928[16]6057449   6201278[43]6195137   3214881[15]2676177  1 33214881[15]2676258 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=3214881[15]2676255, repcount=1607440[15]1338128, factor=3/2
2893393[16]4086217   1395287[44]9209569   4822322[15]4014305  1 32 44822322[15]4014385 (4)A>
== Executing PPA-CTR  7 (once), V(1)=4822322[15]4014384, V(2)=0
2893393[16]4086231   1395287[44]5267141   4822322[15]4014307  1 34822322[15]4014389 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=4822322[15]4014386, repcount=2411161[15]2007194, factor=3/2
4340090[16]6129395   3139397[44]8599989   7233483[15]6021501  1 3 47233483[15]6021583 (4)A>
== Executing PPA-CTR  2 (once), V(1)=7233483[15]6021580
4340090[16]6129404   3139397[44]0643170   7233483[15]6021502  22 37233483[15]6021583 4 (4)A>
== Executing  PA-CTR  1, V(1)=0, V(2)=7233483[15]6021580, repcount=3616741[15]3010791, factor=3/2
6510135[16]4194150   7063643[44]8088123   1085022[16]9032293  22 3 41085022[16]9032374 (4)A>
== Executing PPA-CTR  8 (once), V(1)=1085022[16]9032371, V(2)=0
6510135[16]4194159   7063643[44]6152886   1085022[16]9032294  2 3 2 31085022[16]9032374 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=1085022[16]9032371, repcount=5425112[15]4516186, factor=3/2
9765202[16]1291275   1589319[45]9274534   1627533[16]3548480  2 3 2 32 41627533[16]3548559 (4)A>
== Executing PPA-CTR 11 (once), V(1)=1627533[16]3548558
9765202[16]1291295   1589319[45]0565937   1627533[16]3548483  3 2 31627533[16]3548564 4 (4)A>
== Executing  PA-CTR  4, V(1)=0, V(2)=1627533[16]3548561, repcount=8137669[15]6774281, factor=3/2
1464780[17]1936981   3575969[45]7509630   2441300[16]0322764  3 2 32 42441300[16]0322844 (4)A>
== Executing PPA-CTR 22 (once), V(1)=2441300[16]0322843
1464780[17]1937007   3575969[45]9446755   2441300[16]0322767  2 4 1 2 32441300[16]0322849 4 (4)A>
== Executing  PA-CTR  5, V(1)=0, V(2)=2441300[16]0322846, repcount=1220650[16]0161424, factor=3/2
2197170[17]2905551   8045931[45]4184323   3661951[16]0484191  2 4 1 2 3 43661951[16]0484273 (4)A>
== Executing PPA-CTR 30 (once), V(1)=3661951[16]0484270
2197170[17]2905560   8045931[45]5152884   3661951[16]0484192  2 4 1 3 2 33661951[16]0484273 4 (4)A>
== Executing  PA-CTR 23, V(1)=0, V(2)=3661951[16]0484270, repcount=1830975[16]5242136, factor=3/2
3295755[17]4358376   1810334[46]7101732   5492926[16]5726328  2 4 1 3 2 3 45492926[16]5726409 (4)A>
== Executing PPA-CTR 24 (once), V(1)=5492926[16]5726406, V(2)=0
3295755[17]4358385   1810334[46]8554565   5492926[16]5726329  2 4 1 32 2 35492926[16]5726409 4 (4)A>
== Executing  PA-CTR 23, V(1)=0, V(2)=5492926[16]5726406, repcount=2746463[16]7863204, factor=3/2
4943633[17]1537609   4073252[46]8623453   8239389[16]3589533  2 4 1 32 2 3 48239389[16]3589613 (4)A>
== Executing PPA-CTR 24 (once), V(1)=8239389[16]3589610, V(2)=1
4943633[17]1537618   4073252[46]5802694   8239389[16]3589534  2 4 1 33 2 38239389[16]3589613 4 (4)A>
== Executing  PA-CTR 23, V(1)=0, V(2)=8239389[16]3589610, repcount=4119694[16]6794806, factor=3/2
7415450[17]2306454   9164818[46]9483662   1235908[17]0384340  2 4 1 33 2 3 41235908[17]0384419 (4)A>
== Executing PPA-CTR 24 (once), V(1)=1235908[17]0384416, V(2)=2
7415450[17]2306463   9164818[46]0252515   1235908[17]0384341  2 4 1 34 2 31235908[17]0384419 4 (4)A>
== Executing  PA-CTR 23, V(1)=0, V(2)=1235908[17]0384416, repcount=6179542[16]0192209, factor=3/2
1112317[18]3459717   2062084[47]5073648   1853862[17]0576550  2 4 1 34 2 3 41853862[17]0576628 (4)A>
== Executing PPA-CTR 24 (once), V(1)=1853862[17]0576625, V(2)=3
1112317[18]3459726   2062084[47]6226919   1853862[17]0576551  2 4 1 35 2 31853862[17]0576628 4 (4)A>
== Executing  PA-CTR 23, V(1)=0, V(2)=1853862[17]0576625, repcount=9269313[16]0288313, factor=3/2
1668476[18]5189604   4639689[47]2267956   2780794[17]0864864  2 4 1 35 2 32 42780794[17]0864940 (4)A>
== Executing PPA-CTR 25 (once), V(1)=2780794[17]0864939, V(2)=2
1668476[18]5189615   4639689[47]5727740   2780794[17]0864866  2 4 1 35 42780794[17]0864945 (4)A>
== Executing  PA-CTR  3, V(1)=2780794[17]0864944, V(2)=2, repcount=2, factor=3/2
1668476[18]5189627   4639689[47]9187548   2780794[17]0864868  2 4 1 3 42780794[17]0864951 (4)A>
== Executing PPA-CTR 26 (once), V(1)=2780794[17]0864948
1668476[18]5189636   4639689[47]0917465   2780794[17]0864869  2 4 22 32780794[17]0864951 4 (4)A>
== Executing  PA-CTR  3, V(1)=0, V(2)=2780794[17]0864948, repcount=1390397[17]5432475, factor=3/2
2502714[18]7784486   1043930[48]9119090   4171191[17]6297344  2 4 22 3 44171191[17]6297426 (4)A>
2502714[18]7784487   1043930[48]9119091   4171191[17]6297345  2 4 22 3 44171191[17]6297427 (1)B>
2502714[18]7784488   1043930[48]9119093   4171191[17]6297343  2 4 22 3 44171191[17]6297427 <A(2)
2502714[18]7784489   1043930[48]5416520                  -84  2 4 22 3 <A(2) 24171191[17]6297427
2502714[18]7784490   1043930[48]5416521                  -85  2 4 22 <B(1) 24171191[17]6297428
2502714[18]7784491   1043930[48]5416523                  -83  2 4 2 3 (2)B> 24171191[17]6297428
2502714[18]7784492   1043930[48]5416524                  -82  2 4 2 3 2 (3)B> 24171191[17]6297427
2502714[18]7784493   1043930[48]1713951   4171191[17]6297345  2 4 2 3 2 34171191[17]6297427 (3)B>
2502714[18]7784494   1043930[48]1713953   4171191[17]6297343  2 4 2 3 2 34171191[17]6297427 <B(1)
2502714[18]7784495   1043930[48]1713957   4171191[17]6297345  2 4 2 3 2 34171191[17]6297426 4 (4)A>
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  [*]* [*]* 22+V(2) 3 43+V(1) (4)A>
    1                    1                    1  [*]* [*]* 22+V(2) 3 44+V(1) (1)B>
    2                    3                   -1  [*]* [*]* 22+V(2) 3 44+V(1) <A(2)
    3               7+V(1)           -5+-1*V(1)  [*]* [*]* 22+V(2) 3 <A(2) 24+V(1)
    4               8+V(1)           -6+-1*V(1)  [*]* [*]* 22+V(2) <B(1) 25+V(1)
    5              10+V(1)           -4+-1*V(1)  [*]* [*]* 21+V(2) 3 (2)B> 25+V(1)
    6              11+V(1)           -3+-1*V(1)  [*]* [*]* 21+V(2) 3 2 (3)B> 24+V(1)
    7            15+2*V(1)                    1  [*]* [*]* 21+V(2) 3 2 34+V(1) (3)B>
    8            17+2*V(1)                   -1  [*]* [*]* 21+V(2) 3 2 34+V(1) <B(1)
    9            21+2*V(1)                    1  [*]* [*]* 21+V(2) 3 2 33+V(1) 4 (4)A>
<< Success! ==> defined new CTR 33 (PPA)
2502714[18]7784495   1043930[48]1713957   4171191[17]6297345  2 4 2 3 2 34171191[17]6297426 4 (4)A>
== Executing  PA-CTR 23, V(1)=0, V(2)=4171191[17]6297423, repcount=2085595[17]8148712, factor=3/2
3754072[18]6676767   2348842[48]4977909   6256786[17]4446057  2 4 2 3 2 32 46256786[17]4446137 (4)A>
3754072[18]6676768   2348842[48]4977910   6256786[17]4446058  2 4 2 3 2 32 46256786[17]4446138 (1)B>
3754072[18]6676769   2348842[48]4977912   6256786[17]4446056  2 4 2 3 2 32 46256786[17]4446138 <A(2)
3754072[18]6676770   2348842[48]9424050                  -82  2 4 2 3 2 32 <A(2) 26256786[17]4446138
3754072[18]6676771   2348842[48]9424051                  -83  2 4 2 3 2 3 <B(1) 26256786[17]4446139
3754072[18]6676772   2348842[48]9424055                  -81  2 4 2 3 2 4 (4)A> 26256786[17]4446139
3754072[18]6676773   2348842[48]3870194   6256786[17]4446058  2 4 2 3 2 46256786[17]4446140 (4)A>
3754072[18]6676774   2348842[48]3870195   6256786[17]4446059  2 4 2 3 2 46256786[17]4446141 (1)B>
3754072[18]6676775   2348842[48]3870197   6256786[17]4446057  2 4 2 3 2 46256786[17]4446141 <A(2)
3754072[18]6676776   2348842[48]8316338                  -84  2 4 2 3 2 <A(2) 26256786[17]4446141
3754072[18]6676777   2348842[48]8316340                  -82  2 4 2 3 4 (4)A> 26256786[17]4446141
3754072[18]6676778   2348842[48]2762481   6256786[17]4446059  2 4 2 3 46256786[17]4446142 (4)A>
3754072[18]6676779   2348842[48]2762482   6256786[17]4446060  2 4 2 3 46256786[17]4446143 (1)B>
3754072[18]6676780   2348842[48]2762484   6256786[17]4446058  2 4 2 3 46256786[17]4446143 <A(2)
3754072[18]6676781   2348842[48]7208627                  -85  2 4 2 3 <A(2) 26256786[17]4446143
3754072[18]6676782   2348842[48]7208628                  -86  2 4 2 <B(1) 26256786[17]4446144
3754072[18]6676783   2348842[48]7208630                  -84  2 4 3 (2)B> 26256786[17]4446144
3754072[18]6676784   2348842[48]7208631                  -83  2 4 3 2 (3)B> 26256786[17]4446143
3754072[18]6676785   2348842[48]1654774   6256786[17]4446060  2 4 3 2 36256786[17]4446143 (3)B>
3754072[18]6676786   2348842[48]1654776   6256786[17]4446058  2 4 3 2 36256786[17]4446143 <B(1)
3754072[18]6676787   2348842[48]1654780   6256786[17]4446060  2 4 3 2 36256786[17]4446142 4 (4)A>
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  [*]* [*]* 2 3 2 32 41+V(1) (4)A>
    1                    1                    1  [*]* [*]* 2 3 2 32 42+V(1) (1)B>
    2                    3                   -1  [*]* [*]* 2 3 2 32 42+V(1) <A(2)
    3               5+V(1)           -3+-1*V(1)  [*]* [*]* 2 3 2 32 <A(2) 22+V(1)
    4               6+V(1)           -4+-1*V(1)  [*]* [*]* 2 3 2 3 <B(1) 23+V(1)
    5              10+V(1)           -2+-1*V(1)  [*]* [*]* 2 3 2 4 (4)A> 23+V(1)
    6            13+2*V(1)                    1  [*]* [*]* 2 3 2 44+V(1) (4)A>
    7            14+2*V(1)                    2  [*]* [*]* 2 3 2 45+V(1) (1)B>
    8            16+2*V(1)                    0  [*]* [*]* 2 3 2 45+V(1) <A(2)
    9            21+3*V(1)           -5+-1*V(1)  [*]* [*]* 2 3 2 <A(2) 25+V(1)
   10            23+3*V(1)           -3+-1*V(1)  [*]* [*]* 2 3 4 (4)A> 25+V(1)
   11            28+4*V(1)                    2  [*]* [*]* 2 3 46+V(1) (4)A>
   12            29+4*V(1)                    3  [*]* [*]* 2 3 47+V(1) (1)B>
   13            31+4*V(1)                    1  [*]* [*]* 2 3 47+V(1) <A(2)
   14            38+5*V(1)           -6+-1*V(1)  [*]* [*]* 2 3 <A(2) 27+V(1)
   15            39+5*V(1)           -7+-1*V(1)  [*]* [*]* 2 <B(1) 28+V(1)
   16            41+5*V(1)           -5+-1*V(1)  [*]* [*]* 3 (2)B> 28+V(1)
   17            42+5*V(1)           -4+-1*V(1)  [*]* [*]* 3 2 (3)B> 27+V(1)
   18            49+6*V(1)                    3  [*]* [*]* 3 2 37+V(1) (3)B>
   19            51+6*V(1)                    1  [*]* [*]* 3 2 37+V(1) <B(1)
   20            55+6*V(1)                    3  [*]* [*]* 3 2 36+V(1) 4 (4)A>
<< Success! ==> defined new CTR 34 (PPA)
3754072[18]6676787   2348842[48]1654780   6256786[17]4446060  2 4 3 2 36256786[17]4446142 4 (4)A>
== Executing  PA-CTR  5, V(1)=0, V(2)=6256786[17]4446139, repcount=3128393[17]2223070, factor=3/2
5631108[18]0015207   5284896[48]4560180   9385180[17]6669130  2 4 3 2 32 49385180[17]6669211 (4)A>
5631108[18]0015208   5284896[48]4560181   9385180[17]6669131  2 4 3 2 32 49385180[17]6669212 (1)B>
5631108[18]0015209   5284896[48]4560183   9385180[17]6669129  2 4 3 2 32 49385180[17]6669212 <A(2)
5631108[18]0015210   5284896[48]1229395                  -83  2 4 3 2 32 <A(2) 29385180[17]6669212
5631108[18]0015211   5284896[48]1229396                  -84  2 4 3 2 3 <B(1) 29385180[17]6669213
5631108[18]0015212   5284896[48]1229400                  -82  2 4 3 2 4 (4)A> 29385180[17]6669213
5631108[18]0015213   5284896[48]7898613   9385180[17]6669131  2 4 3 2 49385180[17]6669214 (4)A>
5631108[18]0015214   5284896[48]7898614   9385180[17]6669132  2 4 3 2 49385180[17]6669215 (1)B>
5631108[18]0015215   5284896[48]7898616   9385180[17]6669130  2 4 3 2 49385180[17]6669215 <A(2)
5631108[18]0015216   5284896[48]4567831                  -85  2 4 3 2 <A(2) 29385180[17]6669215
5631108[18]0015217   5284896[48]4567833                  -83  2 4 3 4 (4)A> 29385180[17]6669215
5631108[18]0015218   5284896[48]1237048   9385180[17]6669132  2 4 3 49385180[17]6669216 (4)A>
5631108[18]0015219   5284896[48]1237049   9385180[17]6669133  2 4 3 49385180[17]6669217 (1)B>
5631108[18]0015220   5284896[48]1237051   9385180[17]6669131  2 4 3 49385180[17]6669217 <A(2)
5631108[18]0015221   5284896[48]7906268                  -86  2 4 3 <A(2) 29385180[17]6669217
5631108[18]0015222   5284896[48]7906269                  -87  2 4 <B(1) 29385180[17]6669218
5631108[18]0015223   5284896[48]7906270                  -86  2 1 H> 1 29385180[17]6669218   [stop]

Lines:       909
Top steps:   908
Macro steps: 56311080864886654111667020015223
Basic steps: 52848963802863398154295757589434621786736282921545024067906270
Tape index:  -86
nonzeros:    9385180144147775685277836669221
log10(nonzeros):   30.972
log10(steps   ):   61.723
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-bck-macro machine.

To the BB simulations page of Heiner Marxen.
To the busy beaver page of Heiner Marxen.
To the home page of Heiner Marxen.
Input to awk program:
    gohalt 1
    nbs 5
    T 2-state 5-symbol #k from T.J. & S. Ligocki
    5T  1RB 2LA 4RA 1LB 2LA  0LA 2RB 3RB 2RA 1RH
    : >9.3x10^30  >5.2x10^61
    L 4
    M	950
    pref	sim
    machv Lig25_k  	just simple
    machv Lig25_k-r	with repetitions reduced
    machv Lig25_k-1	with tape symbol exponents
    machv Lig25_k-m	as 1-bck-macro machine
    machv Lig25_k-a	as 1-bck-macro machine with pure additive config-TRs
    iam	Lig25_k-a
    mtype	1 0
    mmtyp	3
    r	1
    H	1
    mac	0
    E	2
    sympr	
    HM	1
    date	Tue Jul  6 22:12:52 CEST 2010
    edate	Tue Jul  6 22:12:56 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:12:52 CEST 2010
Ready: Tue Jul 6 22:12:56 CEST 2010