6-state TM #l from MaBu-List

Comment: This TM produces >6.7*10^47 ones in >2.0*10^95 steps.

State on
0
on
1
on 0 on 1
Print Move Goto Print Move Goto
A B1R C0L 1 right B 0 left C
B A1L D1R 1 left A 1 right D
C B0L E0L 0 left B 0 left E
D A1R B0R 1 right A 0 right B
E F1L C1L 1 left F 1 left C
F D1R Z1R 1 right D 1 right Z
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-2-macro machine.
Simulation is done as 1-bck-2-macro machine with pure additive config-TRs.

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

Steps             BasSteps              BasTpos  Tape contents
    0                    0                    0  (0)A>
    1                    4                   -2  <B(0) 01
    2                    8                    0  11 (1)A> 01
    3                   10                    2  112 (1)D>
    4                   12                    4  113 (1)B>
    5                   14                    2  113 <C(0) 10
    6                   16                    0  112 <C(1) 00 10
    7                   20                   -4  <C(1) 012 00 10
    8                   22                   -6  <A(1) 013 00 10
    9                   24                   -4  01 (1)D> 013 00 10
   10                   28                   -6  01 <C(1) 00 012 00 10
   11                   30                   -8  <F(1) 01 00 012 00 10
   12                   32                   -6  01 (0)B> 01 00 012 00 10
   13                   36                   -4  01 11 (0)B> 00 012 00 10
   14                   40                   -2  01 112 (1)A> 012 00 10
   15                   42                    0  01 113 (1)D> 01 00 10
   16                   46                   -2  01 113 <C(1) 002 10
   17                   52                   -8  01 <C(1) 013 002 10
   18                   54                  -10  <F(1) 014 002 10
   19                   56                   -8  01 (0)B> 014 002 10
   20                   72                    0  01 114 (0)B> 002 10
   21                   76                    2  01 115 (1)A> 00 10
   22                   80                    0  01 115 <E(0) 01 10
   23                   90                  -10  01 <E(0) 105 01 10
   24                   92                  -12  <B(0) 106 01 10
   25                   96                  -10  11 (1)A> 106 01 10
   26                   98                  -12  11 <E(0) 00 105 01 10
   27                  100                  -14  <E(0) 10 00 105 01 10
   28                  106                  -12  11 (1)D> 10 00 105 01 10
   29                  110                  -10  112 (1)D> 00 105 01 10
   30                  112                   -8  113 (1)B> 105 01 10
   31                  114                   -6  114 (1)A> 104 01 10
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  111+V(1) (1)A> 103+V(2) [*]* [*]*
    1                    2                   -2  111+V(1) <E(0) 00 102+V(2) [*]* [*]*
    2             4+2*V(1)           -4+-2*V(1)  <E(0) 101+V(1) 00 102+V(2) [*]* [*]*
    3            10+2*V(1)           -2+-2*V(1)  11 (1)D> 101+V(1) 00 102+V(2) [*]* [*]*
    4            14+6*V(1)                    0  112+V(1) (1)D> 00 102+V(2) [*]* [*]*
    5            16+6*V(1)                    2  113+V(1) (1)B> 102+V(2) [*]* [*]*
    6            18+6*V(1)                    4  114+V(1) (1)A> 101+V(2) [*]* [*]*
<< Success! ==> defined new CTR 1 (PA)
   31                  114                   -6  114 (1)A> 104 01 10
== Executing  PA-CTR  1, V(1)=3, V(2)=1, repcount=1, factor=3/2
   37                  150                   -2  117 (1)A> 102 01 10
   38                  152                   -4  117 <E(0) 00 10 01 10
   39                  166                  -18  <E(0) 107 00 10 01 10
   40                  172                  -16  11 (1)D> 107 00 10 01 10
   41                  200                   -2  118 (1)D> 00 10 01 10
   42                  202                    0  119 (1)B> 10 01 10
   43                  204                    2  1110 (1)A> 01 10
   44                  206                    4  1111 (1)D> 10
   45                  210                    6  1112 (1)D>
   46                  212                    8  1113 (1)B>
   47                  214                    6  1113 <C(0) 10
   48                  216                    4  1112 <C(1) 00 10
   49                  240                  -20  <C(1) 0112 00 10
   50                  242                  -22  <A(1) 0113 00 10
   51                  244                  -20  01 (1)D> 0113 00 10
   52                  248                  -22  01 <C(1) 00 0112 00 10
   53                  250                  -24  <F(1) 01 00 0112 00 10
   54                  252                  -22  01 (0)B> 01 00 0112 00 10
   55                  256                  -20  01 11 (0)B> 00 0112 00 10
   56                  260                  -18  01 112 (1)A> 0112 00 10
   57                  262                  -16  01 113 (1)D> 0111 00 10
   58                  266                  -18  01 113 <C(1) 00 0110 00 10
   59                  272                  -24  01 <C(1) 013 00 0110 00 10
   60                  274                  -26  <F(1) 014 00 0110 00 10
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  <F(1) 011+V(2) 00 013+V(1) [*]* [*]*
    1                    2                    2  01 (0)B> 011+V(2) 00 013+V(1) [*]* [*]*
    2             6+4*V(2)             4+2*V(2)  01 111+V(2) (0)B> 00 013+V(1) [*]* [*]*
    3            10+4*V(2)             6+2*V(2)  01 112+V(2) (1)A> 013+V(1) [*]* [*]*
    4            12+4*V(2)             8+2*V(2)  01 113+V(2) (1)D> 012+V(1) [*]* [*]*
    5            16+4*V(2)             6+2*V(2)  01 113+V(2) <C(1) 00 011+V(1) [*]* [*]*
    6            22+6*V(2)                    0  01 <C(1) 013+V(2) 00 011+V(1) [*]* [*]*
    7            24+6*V(2)                   -2  <F(1) 014+V(2) 00 011+V(1) [*]* [*]*
<< Success! ==> defined new CTR 2 (PA)
   60                  274                  -26  <F(1) 014 00 0110 00 10
== Executing  PA-CTR  2, V(1)=7, V(2)=3, repcount=4, factor=3/2
   88                  550                  -34  <F(1) 0116 00 012 00 10
   89                  552                  -32  01 (0)B> 0116 00 012 00 10
   90                  616                    0  01 1116 (0)B> 00 012 00 10
   91                  620                    2  01 1117 (1)A> 012 00 10
   92                  622                    4  01 1118 (1)D> 01 00 10
   93                  626                    2  01 1118 <C(1) 002 10
   94                  662                  -34  01 <C(1) 0118 002 10
   95                  664                  -36  <F(1) 0119 002 10
   96                  666                  -34  01 (0)B> 0119 002 10
   97                  742                    4  01 1119 (0)B> 002 10
   98                  746                    6  01 1120 (1)A> 00 10
   99                  750                    4  01 1120 <E(0) 01 10
  100                  790                  -36  01 <E(0) 1020 01 10
  101                  792                  -38  <B(0) 1021 01 10
  102                  796                  -36  11 (1)A> 1021 01 10
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  <F(1) 011+V(1) 00 012 00 [*]*
    1                    2                    2  01 (0)B> 011+V(1) 00 012 00 [*]*
    2             6+4*V(1)             4+2*V(1)  01 111+V(1) (0)B> 00 012 00 [*]*
    3            10+4*V(1)             6+2*V(1)  01 112+V(1) (1)A> 012 00 [*]*
    4            12+4*V(1)             8+2*V(1)  01 113+V(1) (1)D> 01 00 [*]*
    5            16+4*V(1)             6+2*V(1)  01 113+V(1) <C(1) 002 [*]*
    6            22+6*V(1)                    0  01 <C(1) 013+V(1) 002 [*]*
    7            24+6*V(1)                   -2  <F(1) 014+V(1) 002 [*]*
    8            26+6*V(1)                    0  01 (0)B> 014+V(1) 002 [*]*
    9           42+10*V(1)             8+2*V(1)  01 114+V(1) (0)B> 002 [*]*
   10           46+10*V(1)            10+2*V(1)  01 115+V(1) (1)A> 00 [*]*
   11           50+10*V(1)             8+2*V(1)  01 115+V(1) <E(0) 01 [*]*
   12           60+12*V(1)                   -2  01 <E(0) 105+V(1) 01 [*]*
   13           62+12*V(1)                   -4  <B(0) 106+V(1) 01 [*]*
   14           66+12*V(1)                   -2  11 (1)A> 106+V(1) 01 [*]*
<< Success! ==> defined new CTR 3 (PPA)
  102                  796                  -36  11 (1)A> 1021 01 10
== Executing  PA-CTR  1, V(1)=0, V(2)=18, repcount=10, factor=3/2
  162                 1786                    4  1131 (1)A> 10 01 10
  163                 1788                    2  1131 <E(0) 00 01 10
  164                 1850                  -60  <E(0) 1031 00 01 10
  165                 1856                  -58  11 (1)D> 1031 00 01 10
  166                 1980                    4  1132 (1)D> 00 01 10
  167                 1982                    6  1133 (1)B> 01 10
  168                 1984                    4  1133 <C(0) 11 10
  169                 1986                    2  1132 <C(1) 00 11 10
  170                 2050                  -62  <C(1) 0132 00 11 10
  171                 2052                  -64  <A(1) 0133 00 11 10
  172                 2054                  -62  01 (1)D> 0133 00 11 10
  173                 2058                  -64  01 <C(1) 00 0132 00 11 10
  174                 2060                  -66  <F(1) 01 00 0132 00 11 10
  175                 2062                  -64  01 (0)B> 01 00 0132 00 11 10
  176                 2066                  -62  01 11 (0)B> 00 0132 00 11 10
  177                 2070                  -60  01 112 (1)A> 0132 00 11 10
  178                 2072                  -58  01 113 (1)D> 0131 00 11 10
  179                 2076                  -60  01 113 <C(1) 00 0130 00 11 10
  180                 2082                  -66  01 <C(1) 013 00 0130 00 11 10
  181                 2084                  -68  <F(1) 014 00 0130 00 11 10
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  <F(1) 011+V(2) 00 013+V(1) [*]* [*]* [*]*
    1                    2                    2  01 (0)B> 011+V(2) 00 013+V(1) [*]* [*]* [*]*
    2             6+4*V(2)             4+2*V(2)  01 111+V(2) (0)B> 00 013+V(1) [*]* [*]* [*]*
    3            10+4*V(2)             6+2*V(2)  01 112+V(2) (1)A> 013+V(1) [*]* [*]* [*]*
    4            12+4*V(2)             8+2*V(2)  01 113+V(2) (1)D> 012+V(1) [*]* [*]* [*]*
    5            16+4*V(2)             6+2*V(2)  01 113+V(2) <C(1) 00 011+V(1) [*]* [*]* [*]*
    6            22+6*V(2)                    0  01 <C(1) 013+V(2) 00 011+V(1) [*]* [*]* [*]*
    7            24+6*V(2)                   -2  <F(1) 014+V(2) 00 011+V(1) [*]* [*]* [*]*
<< Success! ==> defined new CTR 4 (PA)
  181                 2084                  -68  <F(1) 014 00 0130 00 11 10
== Executing  PA-CTR  4, V(1)=27, V(2)=3, repcount=14, factor=3/2
  279                 4310                  -96  <F(1) 0146 00 012 00 11 10
  280                 4312                  -94  01 (0)B> 0146 00 012 00 11 10
  281                 4496                   -2  01 1146 (0)B> 00 012 00 11 10
  282                 4500                    0  01 1147 (1)A> 012 00 11 10
  283                 4502                    2  01 1148 (1)D> 01 00 11 10
  284                 4506                    0  01 1148 <C(1) 002 11 10
  285                 4602                  -96  01 <C(1) 0148 002 11 10
  286                 4604                  -98  <F(1) 0149 002 11 10
  287                 4606                  -96  01 (0)B> 0149 002 11 10
  288                 4802                    2  01 1149 (0)B> 002 11 10
  289                 4806                    4  01 1150 (1)A> 00 11 10
  290                 4810                    2  01 1150 <E(0) 01 11 10
  291                 4910                  -98  01 <E(0) 1050 01 11 10
  292                 4912                 -100  <B(0) 1051 01 11 10
  293                 4916                  -98  11 (1)A> 1051 01 11 10
  294                 4918                 -100  11 <E(0) 00 1050 01 11 10
  295                 4920                 -102  <E(0) 10 00 1050 01 11 10
  296                 4926                 -100  11 (1)D> 10 00 1050 01 11 10
  297                 4930                  -98  112 (1)D> 00 1050 01 11 10
  298                 4932                  -96  113 (1)B> 1050 01 11 10
  299                 4934                  -94  114 (1)A> 1049 01 11 10
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  111+V(1) (1)A> 103+V(2) [*]* [*]* [*]*
    1                    2                   -2  111+V(1) <E(0) 00 102+V(2) [*]* [*]* [*]*
    2             4+2*V(1)           -4+-2*V(1)  <E(0) 101+V(1) 00 102+V(2) [*]* [*]* [*]*
    3            10+2*V(1)           -2+-2*V(1)  11 (1)D> 101+V(1) 00 102+V(2) [*]* [*]* [*]*
    4            14+6*V(1)                    0  112+V(1) (1)D> 00 102+V(2) [*]* [*]* [*]*
    5            16+6*V(1)                    2  113+V(1) (1)B> 102+V(2) [*]* [*]* [*]*
    6            18+6*V(1)                    4  114+V(1) (1)A> 101+V(2) [*]* [*]* [*]*
<< Success! ==> defined new CTR 5 (PA)
  299                 4934                  -94  114 (1)A> 1049 01 11 10
== Executing  PA-CTR  5, V(1)=3, V(2)=46, repcount=24, factor=3/2
  443                10766                    2  1176 (1)A> 10 01 11 10
  444                10768                    0  1176 <E(0) 00 01 11 10
  445                10920                 -152  <E(0) 1076 00 01 11 10
  446                10926                 -150  11 (1)D> 1076 00 01 11 10
  447                11230                    2  1177 (1)D> 00 01 11 10
  448                11232                    4  1178 (1)B> 01 11 10
  449                11234                    2  1178 <C(0) 112 10
  450                11236                    0  1177 <C(1) 00 112 10
  451                11390                 -154  <C(1) 0177 00 112 10
  452                11392                 -156  <A(1) 0178 00 112 10
  453                11394                 -154  01 (1)D> 0178 00 112 10
  454                11398                 -156  01 <C(1) 00 0177 00 112 10
  455                11400                 -158  <F(1) 01 00 0177 00 112 10
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  112+V(1) (1)A> 10 01 111+V(2) [*]*
    1                    2                   -2  112+V(1) <E(0) 00 01 111+V(2) [*]*
    2             6+2*V(1)           -6+-2*V(1)  <E(0) 102+V(1) 00 01 111+V(2) [*]*
    3            12+2*V(1)           -4+-2*V(1)  11 (1)D> 102+V(1) 00 01 111+V(2) [*]*
    4            20+6*V(1)                    0  113+V(1) (1)D> 00 01 111+V(2) [*]*
    5            22+6*V(1)                    2  114+V(1) (1)B> 01 111+V(2) [*]*
    6            24+6*V(1)                    0  114+V(1) <C(0) 112+V(2) [*]*
    7            26+6*V(1)                   -2  113+V(1) <C(1) 00 112+V(2) [*]*
    8            32+8*V(1)           -8+-2*V(1)  <C(1) 013+V(1) 00 112+V(2) [*]*
    9            34+8*V(1)          -10+-2*V(1)  <A(1) 014+V(1) 00 112+V(2) [*]*
   10            36+8*V(1)           -8+-2*V(1)  01 (1)D> 014+V(1) 00 112+V(2) [*]*
   11            40+8*V(1)          -10+-2*V(1)  01 <C(1) 00 013+V(1) 00 112+V(2) [*]*
   12            42+8*V(1)          -12+-2*V(1)  <F(1) 01 00 013+V(1) 00 112+V(2) [*]*
<< Success! ==> defined new CTR 6 (PPA)
  455                11400                 -158  <F(1) 01 00 0177 00 112 10
== Executing  PA-CTR  4, V(1)=74, V(2)=0, repcount=38, factor=3/2
  721                24966                 -234  <F(1) 01115 00 01 00 112 10
  722                24968                 -232  01 (0)B> 01115 00 01 00 112 10
  723                25428                   -2  01 11115 (0)B> 00 01 00 112 10
  724                25432                    0  01 11116 (1)A> 01 00 112 10
  725                25434                    2  01 11117 (1)D> 00 112 10
  726                25436                    4  01 11118 (1)B> 112 10
  727                25438                    6  01 11119 (0)B> 11 10
  728                25440                    8  01 11119 01 (0)B> 10
  729                25442                   10  01 11119 012 (1)A>
  730                25446                    8  01 11119 012 <E(0) 01
  731                25448                    6  01 11119 01 <B(0) 10 01
  732                25450                    8  01 11119 01 (1)A> 10 01
  733                25452                    6  01 11119 01 <E(0) 00 01
  734                25454                    4  01 11119 <B(0) 10 00 01
  735                25456                    6  01 11119 (1)A> 10 00 01
  736                25458                    4  01 11119 <E(0) 002 01
  737                25696                 -234  01 <E(0) 10119 002 01
  738                25698                 -236  <B(0) 10120 002 01
  739                25702                 -234  11 (1)A> 10120 002 01
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  <F(1) 011+V(1) 00 01 00 112 10
    1                    2                    2  01 (0)B> 011+V(1) 00 01 00 112 10
    2             6+4*V(1)             4+2*V(1)  01 111+V(1) (0)B> 00 01 00 112 10
    3            10+4*V(1)             6+2*V(1)  01 112+V(1) (1)A> 01 00 112 10
    4            12+4*V(1)             8+2*V(1)  01 113+V(1) (1)D> 00 112 10
    5            14+4*V(1)            10+2*V(1)  01 114+V(1) (1)B> 112 10
    6            16+4*V(1)            12+2*V(1)  01 115+V(1) (0)B> 11 10
    7            18+4*V(1)            14+2*V(1)  01 115+V(1) 01 (0)B> 10
    8            20+4*V(1)            16+2*V(1)  01 115+V(1) 012 (1)A>
    9            24+4*V(1)            14+2*V(1)  01 115+V(1) 012 <E(0) 01
   10            26+4*V(1)            12+2*V(1)  01 115+V(1) 01 <B(0) 10 01
   11            28+4*V(1)            14+2*V(1)  01 115+V(1) 01 (1)A> 10 01
   12            30+4*V(1)            12+2*V(1)  01 115+V(1) 01 <E(0) 00 01
   13            32+4*V(1)            10+2*V(1)  01 115+V(1) <B(0) 10 00 01
   14            34+4*V(1)            12+2*V(1)  01 115+V(1) (1)A> 10 00 01
   15            36+4*V(1)            10+2*V(1)  01 115+V(1) <E(0) 002 01
   16            46+6*V(1)                    0  01 <E(0) 105+V(1) 002 01
   17            48+6*V(1)                   -2  <B(0) 106+V(1) 002 01
   18            52+6*V(1)                    0  11 (1)A> 106+V(1) 002 01
<< Success! ==> defined new CTR 7 (PPA)
  739                25702                 -234  11 (1)A> 10120 002 01
== Executing  PA-CTR  1, V(1)=0, V(2)=117, repcount=59, factor=3/2
 1093                57562                    2  11178 (1)A> 102 002 01
 1094                57564                    0  11178 <E(0) 00 10 002 01
 1095                57920                 -356  <E(0) 10178 00 10 002 01
 1096                57926                 -354  11 (1)D> 10178 00 10 002 01
 1097                58638                    2  11179 (1)D> 00 10 002 01
 1098                58640                    4  11180 (1)B> 10 002 01
 1099                58642                    6  11181 (1)A> 002 01
 1100                58646                    4  11181 <E(0) 01 00 01
 1101                59008                 -358  <E(0) 10181 01 00 01
 1102                59014                 -356  11 (1)D> 10181 01 00 01
 1103                59738                    6  11182 (1)D> 01 00 01
 1104                59742                    4  11182 <C(1) 002 01
 1105                60106                 -360  <C(1) 01182 002 01
 1106                60108                 -362  <A(1) 01183 002 01
 1107                60110                 -360  01 (1)D> 01183 002 01
 1108                60114                 -362  01 <C(1) 00 01182 002 01
 1109                60116                 -364  <F(1) 01 00 01182 002 01
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  111+V(1) (1)A> 102 001+V(2) [*]*
    1                    2                   -2  111+V(1) <E(0) 00 10 001+V(2) [*]*
    2             4+2*V(1)           -4+-2*V(1)  <E(0) 101+V(1) 00 10 001+V(2) [*]*
    3            10+2*V(1)           -2+-2*V(1)  11 (1)D> 101+V(1) 00 10 001+V(2) [*]*
    4            14+6*V(1)                    0  112+V(1) (1)D> 00 10 001+V(2) [*]*
    5            16+6*V(1)                    2  113+V(1) (1)B> 10 001+V(2) [*]*
    6            18+6*V(1)                    4  114+V(1) (1)A> 001+V(2) [*]*
    7            22+6*V(1)                    2  114+V(1) <E(0) 01 000+V(2) [*]*
    8            30+8*V(1)           -6+-2*V(1)  <E(0) 104+V(1) 01 000+V(2) [*]*
    9            36+8*V(1)           -4+-2*V(1)  11 (1)D> 104+V(1) 01 000+V(2) [*]*
   10           52+12*V(1)                    4  115+V(1) (1)D> 01 000+V(2) [*]*
   11           56+12*V(1)                    2  115+V(1) <C(1) 001+V(2) [*]*
   12           66+14*V(1)           -8+-2*V(1)  <C(1) 015+V(1) 001+V(2) [*]*
   13           68+14*V(1)          -10+-2*V(1)  <A(1) 016+V(1) 001+V(2) [*]*
   14           70+14*V(1)           -8+-2*V(1)  01 (1)D> 016+V(1) 001+V(2) [*]*
   15           74+14*V(1)          -10+-2*V(1)  01 <C(1) 00 015+V(1) 001+V(2) [*]*
   16           76+14*V(1)          -12+-2*V(1)  <F(1) 01 00 015+V(1) 001+V(2) [*]*
<< Success! ==> defined new CTR 8 (PPA)
 1109                60116                 -364  <F(1) 01 00 01182 002 01
== Executing  PA-CTR  2, V(1)=179, V(2)=0, repcount=90, factor=3/2
 1739               134366                 -544  <F(1) 01271 00 012 002 01
 1740               134368                 -542  01 (0)B> 01271 00 012 002 01
 1741               135452                    0  01 11271 (0)B> 00 012 002 01
 1742               135456                    2  01 11272 (1)A> 012 002 01
 1743               135458                    4  01 11273 (1)D> 01 002 01
 1744               135462                    2  01 11273 <C(1) 003 01
 1745               136008                 -544  01 <C(1) 01273 003 01
 1746               136010                 -546  <F(1) 01274 003 01
 1747               136012                 -544  01 (0)B> 01274 003 01
 1748               137108                    4  01 11274 (0)B> 003 01
 1749               137112                    6  01 11275 (1)A> 002 01
 1750               137116                    4  01 11275 <E(0) 01 00 01
 1751               137666                 -546  01 <E(0) 10275 01 00 01
 1752               137668                 -548  <B(0) 10276 01 00 01
 1753               137672                 -546  11 (1)A> 10276 01 00 01
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  <F(1) 011+V(2) 00 012 002+V(1) [*]*
    1                    2                    2  01 (0)B> 011+V(2) 00 012 002+V(1) [*]*
    2             6+4*V(2)             4+2*V(2)  01 111+V(2) (0)B> 00 012 002+V(1) [*]*
    3            10+4*V(2)             6+2*V(2)  01 112+V(2) (1)A> 012 002+V(1) [*]*
    4            12+4*V(2)             8+2*V(2)  01 113+V(2) (1)D> 01 002+V(1) [*]*
    5            16+4*V(2)             6+2*V(2)  01 113+V(2) <C(1) 003+V(1) [*]*
    6            22+6*V(2)                    0  01 <C(1) 013+V(2) 003+V(1) [*]*
    7            24+6*V(2)                   -2  <F(1) 014+V(2) 003+V(1) [*]*
    8            26+6*V(2)                    0  01 (0)B> 014+V(2) 003+V(1) [*]*
    9           42+10*V(2)             8+2*V(2)  01 114+V(2) (0)B> 003+V(1) [*]*
   10           46+10*V(2)            10+2*V(2)  01 115+V(2) (1)A> 002+V(1) [*]*
   11           50+10*V(2)             8+2*V(2)  01 115+V(2) <E(0) 01 001+V(1) [*]*
   12           60+12*V(2)                   -2  01 <E(0) 105+V(2) 01 001+V(1) [*]*
   13           62+12*V(2)                   -4  <B(0) 106+V(2) 01 001+V(1) [*]*
   14           66+12*V(2)                   -2  11 (1)A> 106+V(2) 01 001+V(1) [*]*
<< Success! ==> defined new CTR 9 (PPA)
 1753               137672                 -546  11 (1)A> 10276 01 00 01
== Executing  PA-CTR  5, V(1)=0, V(2)=273, repcount=137, factor=3/2
 2575               307826                    2  11412 (1)A> 102 01 00 01
 2576               307828                    0  11412 <E(0) 00 10 01 00 01
 2577               308652                 -824  <E(0) 10412 00 10 01 00 01
 2578               308658                 -822  11 (1)D> 10412 00 10 01 00 01
 2579               310306                    2  11413 (1)D> 00 10 01 00 01
 2580               310308                    4  11414 (1)B> 10 01 00 01
 2581               310310                    6  11415 (1)A> 01 00 01
 2582               310312                    8  11416 (1)D> 00 01
 2583               310314                   10  11417 (1)B> 01
 2584               310316                    8  11417 <C(0) 11
 2585               310318                    6  11416 <C(1) 00 11
 2586               311150                 -826  <C(1) 01416 00 11
 2587               311152                 -828  <A(1) 01417 00 11
 2588               311154                 -826  01 (1)D> 01417 00 11
 2589               311158                 -828  01 <C(1) 00 01416 00 11
 2590               311160                 -830  <F(1) 01 00 01416 00 11
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  111+V(1) (1)A> 102 01 00 01
    1                    2                   -2  111+V(1) <E(0) 00 10 01 00 01
    2             4+2*V(1)           -4+-2*V(1)  <E(0) 101+V(1) 00 10 01 00 01
    3            10+2*V(1)           -2+-2*V(1)  11 (1)D> 101+V(1) 00 10 01 00 01
    4            14+6*V(1)                    0  112+V(1) (1)D> 00 10 01 00 01
    5            16+6*V(1)                    2  113+V(1) (1)B> 10 01 00 01
    6            18+6*V(1)                    4  114+V(1) (1)A> 01 00 01
    7            20+6*V(1)                    6  115+V(1) (1)D> 00 01
    8            22+6*V(1)                    8  116+V(1) (1)B> 01
    9            24+6*V(1)                    6  116+V(1) <C(0) 11
   10            26+6*V(1)                    4  115+V(1) <C(1) 00 11
   11            36+8*V(1)           -6+-2*V(1)  <C(1) 015+V(1) 00 11
   12            38+8*V(1)           -8+-2*V(1)  <A(1) 016+V(1) 00 11
   13            40+8*V(1)           -6+-2*V(1)  01 (1)D> 016+V(1) 00 11
   14            44+8*V(1)           -8+-2*V(1)  01 <C(1) 00 015+V(1) 00 11
   15            46+8*V(1)          -10+-2*V(1)  <F(1) 01 00 015+V(1) 00 11
<< Success! ==> defined new CTR 10 (PPA)
 2590               311160                 -830  <F(1) 01 00 01416 00 11
== Executing  PA-CTR  2, V(1)=413, V(2)=0, repcount=207, factor=3/2
 4039               699906                -1244  <F(1) 01622 00 012 00 11
== Executing PPA-CTR  3 (once), V(1)=621
 4053               707424                -1246  11 (1)A> 10627 01 11
== Executing  PA-CTR  1, V(1)=0, V(2)=624, repcount=313, factor=3/2
 5931              1591962                    6  11940 (1)A> 10 01 11
 5932              1591964                    4  11940 <E(0) 00 01 11
 5933              1593844                -1876  <E(0) 10940 00 01 11
 5934              1593850                -1874  11 (1)D> 10940 00 01 11
 5935              1597610                    6  11941 (1)D> 00 01 11
 5936              1597612                    8  11942 (1)B> 01 11
 5937              1597614                    6  11942 <C(0) 112
 5938              1597616                    4  11941 <C(1) 00 112
 5939              1599498                -1878  <C(1) 01941 00 112
 5940              1599500                -1880  <A(1) 01942 00 112
 5941              1599502                -1878  01 (1)D> 01942 00 112
 5942              1599506                -1880  01 <C(1) 00 01941 00 112
 5943              1599508                -1882  <F(1) 01 00 01941 00 112
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  112+V(1) (1)A> 10 01 111+V(2)
    1                    2                   -2  112+V(1) <E(0) 00 01 111+V(2)
    2             6+2*V(1)           -6+-2*V(1)  <E(0) 102+V(1) 00 01 111+V(2)
    3            12+2*V(1)           -4+-2*V(1)  11 (1)D> 102+V(1) 00 01 111+V(2)
    4            20+6*V(1)                    0  113+V(1) (1)D> 00 01 111+V(2)
    5            22+6*V(1)                    2  114+V(1) (1)B> 01 111+V(2)
    6            24+6*V(1)                    0  114+V(1) <C(0) 112+V(2)
    7            26+6*V(1)                   -2  113+V(1) <C(1) 00 112+V(2)
    8            32+8*V(1)           -8+-2*V(1)  <C(1) 013+V(1) 00 112+V(2)
    9            34+8*V(1)          -10+-2*V(1)  <A(1) 014+V(1) 00 112+V(2)
   10            36+8*V(1)           -8+-2*V(1)  01 (1)D> 014+V(1) 00 112+V(2)
   11            40+8*V(1)          -10+-2*V(1)  01 <C(1) 00 013+V(1) 00 112+V(2)
   12            42+8*V(1)          -12+-2*V(1)  <F(1) 01 00 013+V(1) 00 112+V(2)
<< Success! ==> defined new CTR 11 (PPA)
 5943              1599508                -1882  <F(1) 01 00 01941 00 112
== Executing  PA-CTR  2, V(1)=938, V(2)=0, repcount=470, factor=3/2
 9233              3594658                -2822  <F(1) 011411 00 01 00 112
 9234              3594660                -2820  01 (0)B> 011411 00 01 00 112
 9235              3600304                    2  01 111411 (0)B> 00 01 00 112
 9236              3600308                    4  01 111412 (1)A> 01 00 112
 9237              3600310                    6  01 111413 (1)D> 00 112
 9238              3600312                    8  01 111414 (1)B> 112
 9239              3600314                   10  01 111415 (0)B> 11
 9240              3600316                   12  01 111415 01 (0)B>
 9241              3600320                   14  01 111415 01 11 (1)A>
 9242              3600324                   12  01 111415 01 11 <E(0) 01
 9243              3600326                   10  01 111415 01 <E(0) 10 01
 9244              3600328                    8  01 111415 <B(0) 102 01
 9245              3600330                   10  01 111415 (1)A> 102 01
 9246              3600332                    8  01 111415 <E(0) 00 10 01
 9247              3603162                -2822  01 <E(0) 101415 00 10 01
 9248              3603164                -2824  <B(0) 101416 00 10 01
 9249              3603168                -2822  11 (1)A> 101416 00 10 01
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  <F(1) 011+V(1) 00 01 00 112
    1                    2                    2  01 (0)B> 011+V(1) 00 01 00 112
    2             6+4*V(1)             4+2*V(1)  01 111+V(1) (0)B> 00 01 00 112
    3            10+4*V(1)             6+2*V(1)  01 112+V(1) (1)A> 01 00 112
    4            12+4*V(1)             8+2*V(1)  01 113+V(1) (1)D> 00 112
    5            14+4*V(1)            10+2*V(1)  01 114+V(1) (1)B> 112
    6            16+4*V(1)            12+2*V(1)  01 115+V(1) (0)B> 11
    7            18+4*V(1)            14+2*V(1)  01 115+V(1) 01 (0)B>
    8            22+4*V(1)            16+2*V(1)  01 115+V(1) 01 11 (1)A>
    9            26+4*V(1)            14+2*V(1)  01 115+V(1) 01 11 <E(0) 01
   10            28+4*V(1)            12+2*V(1)  01 115+V(1) 01 <E(0) 10 01
   11            30+4*V(1)            10+2*V(1)  01 115+V(1) <B(0) 102 01
   12            32+4*V(1)            12+2*V(1)  01 115+V(1) (1)A> 102 01
   13            34+4*V(1)            10+2*V(1)  01 115+V(1) <E(0) 00 10 01
   14            44+6*V(1)                    0  01 <E(0) 105+V(1) 00 10 01
   15            46+6*V(1)                   -2  <B(0) 106+V(1) 00 10 01
   16            50+6*V(1)                    0  11 (1)A> 106+V(1) 00 10 01
<< Success! ==> defined new CTR 12 (PPA)
 9249              3603168                -2822  11 (1)A> 101416 00 10 01
== Executing  PA-CTR  5, V(1)=0, V(2)=1413, repcount=707, factor=3/2
13491              8108172                    6  112122 (1)A> 102 00 10 01
13492              8108174                    4  112122 <E(0) 00 10 00 10 01
13493              8112418                -4240  <E(0) 102122 00 10 00 10 01
13494              8112424                -4238  11 (1)D> 102122 00 10 00 10 01
13495              8120912                    6  112123 (1)D> 00 10 00 10 01
13496              8120914                    8  112124 (1)B> 10 00 10 01
13497              8120916                   10  112125 (1)A> 00 10 01
13498              8120920                    8  112125 <E(0) 01 10 01
13499              8125170                -4242  <E(0) 102125 01 10 01
13500              8125176                -4240  11 (1)D> 102125 01 10 01
13501              8133676                   10  112126 (1)D> 01 10 01
13502              8133680                    8  112126 <C(1) 00 10 01
13503              8137932                -4244  <C(1) 012126 00 10 01
13504              8137934                -4246  <A(1) 012127 00 10 01
13505              8137936                -4244  01 (1)D> 012127 00 10 01
13506              8137940                -4246  01 <C(1) 00 012126 00 10 01
13507              8137942                -4248  <F(1) 01 00 012126 00 10 01
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  111+V(1) (1)A> 102 00 [*]* [*]*
    1                    2                   -2  111+V(1) <E(0) 00 10 00 [*]* [*]*
    2             4+2*V(1)           -4+-2*V(1)  <E(0) 101+V(1) 00 10 00 [*]* [*]*
    3            10+2*V(1)           -2+-2*V(1)  11 (1)D> 101+V(1) 00 10 00 [*]* [*]*
    4            14+6*V(1)                    0  112+V(1) (1)D> 00 10 00 [*]* [*]*
    5            16+6*V(1)                    2  113+V(1) (1)B> 10 00 [*]* [*]*
    6            18+6*V(1)                    4  114+V(1) (1)A> 00 [*]* [*]*
    7            22+6*V(1)                    2  114+V(1) <E(0) 01 [*]* [*]*
    8            30+8*V(1)           -6+-2*V(1)  <E(0) 104+V(1) 01 [*]* [*]*
    9            36+8*V(1)           -4+-2*V(1)  11 (1)D> 104+V(1) 01 [*]* [*]*
   10           52+12*V(1)                    4  115+V(1) (1)D> 01 [*]* [*]*
   11           56+12*V(1)                    2  115+V(1) <C(1) 00 [*]* [*]*
   12           66+14*V(1)           -8+-2*V(1)  <C(1) 015+V(1) 00 [*]* [*]*
   13           68+14*V(1)          -10+-2*V(1)  <A(1) 016+V(1) 00 [*]* [*]*
   14           70+14*V(1)           -8+-2*V(1)  01 (1)D> 016+V(1) 00 [*]* [*]*
   15           74+14*V(1)          -10+-2*V(1)  01 <C(1) 00 015+V(1) 00 [*]* [*]*
   16           76+14*V(1)          -12+-2*V(1)  <F(1) 01 00 015+V(1) 00 [*]* [*]*
<< Success! ==> defined new CTR 13 (PPA)
13507              8137942                -4248  <F(1) 01 00 012126 00 10 01
== Executing  PA-CTR  4, V(1)=2123, V(2)=0, repcount=1062, factor=3/2
20941             18304468                -6372  <F(1) 013187 00 012 00 10 01
20942             18304470                -6370  01 (0)B> 013187 00 012 00 10 01
20943             18317218                    4  01 113187 (0)B> 00 012 00 10 01
20944             18317222                    6  01 113188 (1)A> 012 00 10 01
20945             18317224                    8  01 113189 (1)D> 01 00 10 01
20946             18317228                    6  01 113189 <C(1) 002 10 01
20947             18323606                -6372  01 <C(1) 013189 002 10 01
20948             18323608                -6374  <F(1) 013190 002 10 01
20949             18323610                -6372  01 (0)B> 013190 002 10 01
20950             18336370                    8  01 113190 (0)B> 002 10 01
20951             18336374                   10  01 113191 (1)A> 00 10 01
20952             18336378                    8  01 113191 <E(0) 01 10 01
20953             18342760                -6374  01 <E(0) 103191 01 10 01
20954             18342762                -6376  <B(0) 103192 01 10 01
20955             18342766                -6374  11 (1)A> 103192 01 10 01
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  <F(1) 011+V(1) 00 012 00 [*]* [*]*
    1                    2                    2  01 (0)B> 011+V(1) 00 012 00 [*]* [*]*
    2             6+4*V(1)             4+2*V(1)  01 111+V(1) (0)B> 00 012 00 [*]* [*]*
    3            10+4*V(1)             6+2*V(1)  01 112+V(1) (1)A> 012 00 [*]* [*]*
    4            12+4*V(1)             8+2*V(1)  01 113+V(1) (1)D> 01 00 [*]* [*]*
    5            16+4*V(1)             6+2*V(1)  01 113+V(1) <C(1) 002 [*]* [*]*
    6            22+6*V(1)                    0  01 <C(1) 013+V(1) 002 [*]* [*]*
    7            24+6*V(1)                   -2  <F(1) 014+V(1) 002 [*]* [*]*
    8            26+6*V(1)                    0  01 (0)B> 014+V(1) 002 [*]* [*]*
    9           42+10*V(1)             8+2*V(1)  01 114+V(1) (0)B> 002 [*]* [*]*
   10           46+10*V(1)            10+2*V(1)  01 115+V(1) (1)A> 00 [*]* [*]*
   11           50+10*V(1)             8+2*V(1)  01 115+V(1) <E(0) 01 [*]* [*]*
   12           60+12*V(1)                   -2  01 <E(0) 105+V(1) 01 [*]* [*]*
   13           62+12*V(1)                   -4  <B(0) 106+V(1) 01 [*]* [*]*
   14           66+12*V(1)                   -2  11 (1)A> 106+V(1) 01 [*]* [*]*
<< Success! ==> defined new CTR 14 (PPA)
20955             18342766                -6374  11 (1)A> 103192 01 10 01
== Executing  PA-CTR  5, V(1)=0, V(2)=3189, repcount=1595, factor=3/2
30525             41253346                    6  114786 (1)A> 102 01 10 01
30526             41253348                    4  114786 <E(0) 00 10 01 10 01
30527             41262920                -9568  <E(0) 104786 00 10 01 10 01
30528             41262926                -9566  11 (1)D> 104786 00 10 01 10 01
30529             41282070                    6  114787 (1)D> 00 10 01 10 01
30530             41282072                    8  114788 (1)B> 10 01 10 01
30531             41282074                   10  114789 (1)A> 01 10 01
30532             41282076                   12  114790 (1)D> 10 01
30533             41282080                   14  114791 (1)D> 01
30534             41282084                   12  114791 <C(1)
30535             41291666                -9570  <C(1) 014791
30536             41291668                -9572  <A(1) 014792
30537             41291670                -9570  01 (1)D> 014792
30538             41291674                -9572  01 <C(1) 00 014791
30539             41291676                -9574  <F(1) 01 00 014791
30540             41291678                -9572  01 (0)B> 01 00 014791
30541             41291682                -9570  01 11 (0)B> 00 014791
30542             41291686                -9568  01 112 (1)A> 014791
30543             41291688                -9566  01 113 (1)D> 014790
30544             41291692                -9568  01 113 <C(1) 00 014789
30545             41291698                -9574  01 <C(1) 013 00 014789
30546             41291700                -9576  <F(1) 014 00 014789
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  <F(1) 011+V(2) 00 013+V(1)
    1                    2                    2  01 (0)B> 011+V(2) 00 013+V(1)
    2             6+4*V(2)             4+2*V(2)  01 111+V(2) (0)B> 00 013+V(1)
    3            10+4*V(2)             6+2*V(2)  01 112+V(2) (1)A> 013+V(1)
    4            12+4*V(2)             8+2*V(2)  01 113+V(2) (1)D> 012+V(1)
    5            16+4*V(2)             6+2*V(2)  01 113+V(2) <C(1) 00 011+V(1)
    6            22+6*V(2)                    0  01 <C(1) 013+V(2) 00 011+V(1)
    7            24+6*V(2)                   -2  <F(1) 014+V(2) 00 011+V(1)
<< Success! ==> defined new CTR 15 (PA)
30546             41291700                -9576  <F(1) 014 00 014789
== Executing  PA-CTR 15, V(1)=4786, V(2)=3, repcount=2394, factor=3/2
47304             92951826               -14364  <F(1) 017186 00 01
47305             92951828               -14362  01 (0)B> 017186 00 01
47306             92980572                   10  01 117186 (0)B> 00 01
47307             92980576                   12  01 117187 (1)A> 01
47308             92980578                   14  01 117188 (1)D>
47309             92980580                   16  01 117189 (1)B>
47310             92980582                   14  01 117189 <C(0) 10
47311             92980584                   12  01 117188 <C(1) 00 10
47312             92994960               -14364  01 <C(1) 017188 00 10
47313             92994962               -14366  <F(1) 017189 00 10
47314             92994964               -14364  01 (0)B> 017189 00 10
47315             93023720                   14  01 117189 (0)B> 00 10
47316             93023724                   16  01 117190 (1)A> 10
47317             93023726                   14  01 117190 <E(0)
47318             93038106               -14366  01 <E(0) 107190
47319             93038108               -14368  <B(0) 107191
47320             93038112               -14366  11 (1)A> 107191
47321             93038114               -14368  11 <E(0) 00 107190
47322             93038116               -14370  <E(0) 10 00 107190
47323             93038122               -14368  11 (1)D> 10 00 107190
47324             93038126               -14366  112 (1)D> 00 107190
47325             93038128               -14364  113 (1)B> 107190
47326             93038130               -14362  114 (1)A> 107189
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  111+V(1) (1)A> 103+V(2)
    1                    2                   -2  111+V(1) <E(0) 00 102+V(2)
    2             4+2*V(1)           -4+-2*V(1)  <E(0) 101+V(1) 00 102+V(2)
    3            10+2*V(1)           -2+-2*V(1)  11 (1)D> 101+V(1) 00 102+V(2)
    4            14+6*V(1)                    0  112+V(1) (1)D> 00 102+V(2)
    5            16+6*V(1)                    2  113+V(1) (1)B> 102+V(2)
    6            18+6*V(1)                    4  114+V(1) (1)A> 101+V(2)
<< Success! ==> defined new CTR 16 (PA)
47326             93038130               -14362  114 (1)A> 107189
== Executing  PA-CTR 16, V(1)=3, V(2)=7186, repcount=3594, factor=3/2
68890            209386692                   14  1110786 (1)A> 10
68891            209386694                   12  1110786 <E(0)
68892            209408266               -21560  <E(0) 1010786
68893            209408272               -21558  11 (1)D> 1010786
68894            209451416                   14  1110787 (1)D>
68895            209451418                   16  1110788 (1)B>
68896            209451420                   14  1110788 <C(0) 10
68897            209451422                   12  1110787 <C(1) 00 10
68898            209472996               -21562  <C(1) 0110787 00 10
68899            209472998               -21564  <A(1) 0110788 00 10
68900            209473000               -21562  01 (1)D> 0110788 00 10
68901            209473004               -21564  01 <C(1) 00 0110787 00 10
68902            209473006               -21566  <F(1) 01 00 0110787 00 10
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  112+V(1) (1)A> 10
    1                    2                   -2  112+V(1) <E(0)
    2             6+2*V(1)           -6+-2*V(1)  <E(0) 102+V(1)
    3            12+2*V(1)           -4+-2*V(1)  11 (1)D> 102+V(1)
    4            20+6*V(1)                    0  113+V(1) (1)D>
    5            22+6*V(1)                    2  114+V(1) (1)B>
    6            24+6*V(1)                    0  114+V(1) <C(0) 10
    7            26+6*V(1)                   -2  113+V(1) <C(1) 00 10
    8            32+8*V(1)           -8+-2*V(1)  <C(1) 013+V(1) 00 10
    9            34+8*V(1)          -10+-2*V(1)  <A(1) 014+V(1) 00 10
   10            36+8*V(1)           -8+-2*V(1)  01 (1)D> 014+V(1) 00 10
   11            40+8*V(1)          -10+-2*V(1)  01 <C(1) 00 013+V(1) 00 10
   12            42+8*V(1)          -12+-2*V(1)  <F(1) 01 00 013+V(1) 00 10
<< Success! ==> defined new CTR 17 (PPA)
68902            209473006               -21566  <F(1) 01 00 0110787 00 10
== Executing  PA-CTR  2, V(1)=10784, V(2)=0, repcount=5393, factor=3/2
106653            471313942               -32352  <F(1) 0116180 00 01 00 10
106654            471313944               -32350  01 (0)B> 0116180 00 01 00 10
106655            471378664                   10  01 1116180 (0)B> 00 01 00 10
106656            471378668                   12  01 1116181 (1)A> 01 00 10
106657            471378670                   14  01 1116182 (1)D> 00 10
106658            471378672                   16  01 1116183 (1)B> 10
106659            471378674                   18  01 1116184 (1)A>
106660            471378678                   16  01 1116184 <E(0) 01
106661            471411046               -32352  01 <E(0) 1016184 01
106662            471411048               -32354  <B(0) 1016185 01
106663            471411052               -32352  11 (1)A> 1016185 01
106664            471411054               -32354  11 <E(0) 00 1016184 01
106665            471411056               -32356  <E(0) 10 00 1016184 01
106666            471411062               -32354  11 (1)D> 10 00 1016184 01
106667            471411066               -32352  112 (1)D> 00 1016184 01
106668            471411068               -32350  113 (1)B> 1016184 01
106669            471411070               -32348  114 (1)A> 1016183 01
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  111+V(1) (1)A> 103+V(2) [*]*
    1                    2                   -2  111+V(1) <E(0) 00 102+V(2) [*]*
    2             4+2*V(1)           -4+-2*V(1)  <E(0) 101+V(1) 00 102+V(2) [*]*
    3            10+2*V(1)           -2+-2*V(1)  11 (1)D> 101+V(1) 00 102+V(2) [*]*
    4            14+6*V(1)                    0  112+V(1) (1)D> 00 102+V(2) [*]*
    5            16+6*V(1)                    2  113+V(1) (1)B> 102+V(2) [*]*
    6            18+6*V(1)                    4  114+V(1) (1)A> 101+V(2) [*]*
<< Success! ==> defined new CTR 18 (PA)
106669            471411070               -32348  114 (1)A> 1016183 01
== Executing  PA-CTR 18, V(1)=3, V(2)=16180, repcount=8091, factor=3/2
155215           1060808056                   16  1124277 (1)A> 10 01
155216           1060808058                   14  1124277 <E(0) 00 01
155217           1060856612               -48540  <E(0) 1024277 00 01
155218           1060856618               -48538  11 (1)D> 1024277 00 01
155219           1060953726                   16  1124278 (1)D> 00 01
155220           1060953728                   18  1124279 (1)B> 01
155221           1060953730                   16  1124279 <C(0) 11
155222           1060953732                   14  1124278 <C(1) 00 11
155223           1061002288               -48542  <C(1) 0124278 00 11
155224           1061002290               -48544  <A(1) 0124279 00 11
155225           1061002292               -48542  01 (1)D> 0124279 00 11
155226           1061002296               -48544  01 <C(1) 00 0124278 00 11
155227           1061002298               -48546  <F(1) 01 00 0124278 00 11
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  112+V(1) (1)A> 10 01
    1                    2                   -2  112+V(1) <E(0) 00 01
    2             6+2*V(1)           -6+-2*V(1)  <E(0) 102+V(1) 00 01
    3            12+2*V(1)           -4+-2*V(1)  11 (1)D> 102+V(1) 00 01
    4            20+6*V(1)                    0  113+V(1) (1)D> 00 01
    5            22+6*V(1)                    2  114+V(1) (1)B> 01
    6            24+6*V(1)                    0  114+V(1) <C(0) 11
    7            26+6*V(1)                   -2  113+V(1) <C(1) 00 11
    8            32+8*V(1)           -8+-2*V(1)  <C(1) 013+V(1) 00 11
    9            34+8*V(1)          -10+-2*V(1)  <A(1) 014+V(1) 00 11
   10            36+8*V(1)           -8+-2*V(1)  01 (1)D> 014+V(1) 00 11
   11            40+8*V(1)          -10+-2*V(1)  01 <C(1) 00 013+V(1) 00 11
   12            42+8*V(1)          -12+-2*V(1)  <F(1) 01 00 013+V(1) 00 11
<< Success! ==> defined new CTR 19 (PPA)
155227           1061002298               -48546  <F(1) 01 00 0124278 00 11
== Executing  PA-CTR  2, V(1)=24275, V(2)=0, repcount=12138, factor=3/2
240193           2387163764               -72822  <F(1) 0136415 00 012 00 11
== Executing PPA-CTR  3 (once), V(1)=36414
240207           2387600798               -72824  11 (1)A> 1036420 01 11
== Executing  PA-CTR  1, V(1)=0, V(2)=36417, repcount=18209, factor=3/2
349461           5371873808                   12  1154628 (1)A> 102 01 11
349462           5371873810                   10  1154628 <E(0) 00 10 01 11
349463           5371983066              -109246  <E(0) 1054628 00 10 01 11
349464           5371983072              -109244  11 (1)D> 1054628 00 10 01 11
349465           5372201584                   12  1154629 (1)D> 00 10 01 11
349466           5372201586                   14  1154630 (1)B> 10 01 11
349467           5372201588                   16  1154631 (1)A> 01 11
349468           5372201590                   18  1154632 (1)D> 11
349469           5372201592                   20  1154632 10 (1)D>
349470           5372201594                   22  1154632 10 11 (1)B>
349471           5372201596                   20  1154632 10 11 <C(0) 10
349472           5372201598                   18  1154632 10 <C(1) 00 10
349473           5372201604                   16  1154632 <C(1) 002 10
349474           5372310868              -109248  <C(1) 0154632 002 10
349475           5372310870              -109250  <A(1) 0154633 002 10
349476           5372310872              -109248  01 (1)D> 0154633 002 10
349477           5372310876              -109250  01 <C(1) 00 0154632 002 10
349478           5372310878              -109252  <F(1) 01 00 0154632 002 10
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  111+V(1) (1)A> 102 01 111+V(2)
    1                    2                   -2  111+V(1) <E(0) 00 10 01 111+V(2)
    2             4+2*V(1)           -4+-2*V(1)  <E(0) 101+V(1) 00 10 01 111+V(2)
    3            10+2*V(1)           -2+-2*V(1)  11 (1)D> 101+V(1) 00 10 01 111+V(2)
    4            14+6*V(1)                    0  112+V(1) (1)D> 00 10 01 111+V(2)
    5            16+6*V(1)                    2  113+V(1) (1)B> 10 01 111+V(2)
    6            18+6*V(1)                    4  114+V(1) (1)A> 01 111+V(2)
    7            20+6*V(1)                    6  115+V(1) (1)D> 111+V(2)
    8     22+6*V(1)+2*V(2)             8+2*V(2)  115+V(1) 101+V(2) (1)D>
    9     24+6*V(1)+2*V(2)            10+2*V(2)  115+V(1) 101+V(2) 11 (1)B>
   10     26+6*V(1)+2*V(2)             8+2*V(2)  115+V(1) 101+V(2) 11 <C(0) 10
   11     28+6*V(1)+2*V(2)             6+2*V(2)  115+V(1) 101+V(2) <C(1) 00 10
   12     34+6*V(1)+8*V(2)                    4  115+V(1) <C(1) 002+V(2) 10
   13     44+8*V(1)+8*V(2)           -6+-2*V(1)  <C(1) 015+V(1) 002+V(2) 10
   14     46+8*V(1)+8*V(2)           -8+-2*V(1)  <A(1) 016+V(1) 002+V(2) 10
   15     48+8*V(1)+8*V(2)           -6+-2*V(1)  01 (1)D> 016+V(1) 002+V(2) 10
   16     52+8*V(1)+8*V(2)           -8+-2*V(1)  01 <C(1) 00 015+V(1) 002+V(2) 10
   17     54+8*V(1)+8*V(2)          -10+-2*V(1)  <F(1) 01 00 015+V(1) 002+V(2) 10
<< Success! ==> defined new CTR 20 (PPA)
349478           5372310878              -109252  <F(1) 01 00 0154632 002 10
== Executing  PA-CTR  2, V(1)=54629, V(2)=0, repcount=27315, factor=3/2
540683          12087703628              -163882  <F(1) 0181946 00 012 002 10
== Executing PPA-CTR  9 (once), V(1)=0, V(2)=81945
540697          12088687034              -163884  11 (1)A> 1081951 01 00 10
== Executing  PA-CTR  5, V(1)=0, V(2)=81948, repcount=40975, factor=3/2
786547          27199611434                   16  11122926 (1)A> 10 01 00 10
786548          27199611436                   14  11122926 <E(0) 00 01 00 10
786549          27199857288              -245838  <E(0) 10122926 00 01 00 10
786550          27199857294              -245836  11 (1)D> 10122926 00 01 00 10
786551          27200348998                   16  11122927 (1)D> 00 01 00 10
786552          27200349000                   18  11122928 (1)B> 01 00 10
786553          27200349002                   16  11122928 <C(0) 11 00 10
786554          27200349004                   14  11122927 <C(1) 00 11 00 10
786555          27200594858              -245840  <C(1) 01122927 00 11 00 10
786556          27200594860              -245842  <A(1) 01122928 00 11 00 10
786557          27200594862              -245840  01 (1)D> 01122928 00 11 00 10
786558          27200594866              -245842  01 <C(1) 00 01122927 00 11 00 10
786559          27200594868              -245844  <F(1) 01 00 01122927 00 11 00 10
786560          27200594870              -245842  01 (0)B> 01 00 01122927 00 11 00 10
786561          27200594874              -245840  01 11 (0)B> 00 01122927 00 11 00 10
786562          27200594878              -245838  01 112 (1)A> 01122927 00 11 00 10
786563          27200594880              -245836  01 113 (1)D> 01122926 00 11 00 10
786564          27200594884              -245838  01 113 <C(1) 00 01122925 00 11 00 10
786565          27200594890              -245844  01 <C(1) 013 00 01122925 00 11 00 10
786566          27200594892              -245846  <F(1) 014 00 01122925 00 11 00 10
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  <F(1) 011+V(2) 00 013+V(1) [*]* [*]* [*]* [*]*
    1                    2                    2  01 (0)B> 011+V(2) 00 013+V(1) [*]* [*]* [*]* [*]*
    2             6+4*V(2)             4+2*V(2)  01 111+V(2) (0)B> 00 013+V(1) [*]* [*]* [*]* [*]*
    3            10+4*V(2)             6+2*V(2)  01 112+V(2) (1)A> 013+V(1) [*]* [*]* [*]* [*]*
    4            12+4*V(2)             8+2*V(2)  01 113+V(2) (1)D> 012+V(1) [*]* [*]* [*]* [*]*
    5            16+4*V(2)             6+2*V(2)  01 113+V(2) <C(1) 00 011+V(1) [*]* [*]* [*]* [*]*
    6            22+6*V(2)                    0  01 <C(1) 013+V(2) 00 011+V(1) [*]* [*]* [*]* [*]*
    7            24+6*V(2)                   -2  <F(1) 014+V(2) 00 011+V(1) [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 21 (PA)
786566          27200594892              -245846  <F(1) 014 00 01122925 00 11 00 10
== Executing  PA-CTR 21, V(1)=122922, V(2)=3, repcount=61462, factor=3/2
1216800          61200820134              -368770  <F(1) 01184390 00 01 00 11 00 10
1216801          61200820136              -368768  01 (0)B> 01184390 00 01 00 11 00 10
1216802          61201557696                   12  01 11184390 (0)B> 00 01 00 11 00 10
1216803          61201557700                   14  01 11184391 (1)A> 01 00 11 00 10
1216804          61201557702                   16  01 11184392 (1)D> 00 11 00 10
1216805          61201557704                   18  01 11184393 (1)B> 11 00 10
1216806          61201557706                   20  01 11184394 (0)B> 00 10
1216807          61201557710                   22  01 11184395 (1)A> 10
1216808          61201557712                   20  01 11184395 <E(0)
1216809          61201926502              -368770  01 <E(0) 10184395
1216810          61201926504              -368772  <B(0) 10184396
1216811          61201926508              -368770  11 (1)A> 10184396
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  <F(1) 011+V(1) 00 01 00 11 00 10
    1                    2                    2  01 (0)B> 011+V(1) 00 01 00 11 00 10
    2             6+4*V(1)             4+2*V(1)  01 111+V(1) (0)B> 00 01 00 11 00 10
    3            10+4*V(1)             6+2*V(1)  01 112+V(1) (1)A> 01 00 11 00 10
    4            12+4*V(1)             8+2*V(1)  01 113+V(1) (1)D> 00 11 00 10
    5            14+4*V(1)            10+2*V(1)  01 114+V(1) (1)B> 11 00 10
    6            16+4*V(1)            12+2*V(1)  01 115+V(1) (0)B> 00 10
    7            20+4*V(1)            14+2*V(1)  01 116+V(1) (1)A> 10
    8            22+4*V(1)            12+2*V(1)  01 116+V(1) <E(0)
    9            34+6*V(1)                    0  01 <E(0) 106+V(1)
   10            36+6*V(1)                   -2  <B(0) 107+V(1)
   11            40+6*V(1)                    0  11 (1)A> 107+V(1)
<< Success! ==> defined new CTR 22 (PPA)
1216811          61201926508              -368770  11 (1)A> 10184396
== Executing  PA-CTR 16, V(1)=0, V(2)=184393, repcount=92197, factor=3/2
1769993         137705337562                   18  11276592 (1)A> 102
1769994         137705337564                   16  11276592 <E(0) 00 10
1769995         137705890748              -553168  <E(0) 10276592 00 10
1769996         137705890754              -553166  11 (1)D> 10276592 00 10
1769997         137706997122                   18  11276593 (1)D> 00 10
1769998         137706997124                   20  11276594 (1)B> 10
1769999         137706997126                   22  11276595 (1)A>
1770000         137706997130                   20  11276595 <E(0) 01
1770001         137707550320              -553170  <E(0) 10276595 01
1770002         137707550326              -553168  11 (1)D> 10276595 01
1770003         137708656706                   22  11276596 (1)D> 01
1770004         137708656710                   20  11276596 <C(1)
1770005         137709209902              -553172  <C(1) 01276596
1770006         137709209904              -553174  <A(1) 01276597
1770007         137709209906              -553172  01 (1)D> 01276597
1770008         137709209910              -553174  01 <C(1) 00 01276596
1770009         137709209912              -553176  <F(1) 01 00 01276596
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  111+V(1) (1)A> 102
    1                    2                   -2  111+V(1) <E(0) 00 10
    2             4+2*V(1)           -4+-2*V(1)  <E(0) 101+V(1) 00 10
    3            10+2*V(1)           -2+-2*V(1)  11 (1)D> 101+V(1) 00 10
    4            14+6*V(1)                    0  112+V(1) (1)D> 00 10
    5            16+6*V(1)                    2  113+V(1) (1)B> 10
    6            18+6*V(1)                    4  114+V(1) (1)A>
    7            22+6*V(1)                    2  114+V(1) <E(0) 01
    8            30+8*V(1)           -6+-2*V(1)  <E(0) 104+V(1) 01
    9            36+8*V(1)           -4+-2*V(1)  11 (1)D> 104+V(1) 01
   10           52+12*V(1)                    4  115+V(1) (1)D> 01
   11           56+12*V(1)                    2  115+V(1) <C(1)
   12           66+14*V(1)           -8+-2*V(1)  <C(1) 015+V(1)
   13           68+14*V(1)          -10+-2*V(1)  <A(1) 016+V(1)
   14           70+14*V(1)           -8+-2*V(1)  01 (1)D> 016+V(1)
   15           74+14*V(1)          -10+-2*V(1)  01 <C(1) 00 015+V(1)
   16           76+14*V(1)          -12+-2*V(1)  <F(1) 01 00 015+V(1)
<< Success! ==> defined new CTR 23 (PPA)
1770009         137709209912              -553176  <F(1) 01 00 01276596
== Executing  PA-CTR 15, V(1)=276593, V(2)=0, repcount=138297, factor=3/2
2738088         309845826248              -829770  <F(1) 01414892 00 012
2738089         309845826250              -829768  01 (0)B> 01414892 00 012
2738090         309847485818                   16  01 11414892 (0)B> 00 012
2738091         309847485822                   18  01 11414893 (1)A> 012
2738092         309847485824                   20  01 11414894 (1)D> 01
2738093         309847485828                   18  01 11414894 <C(1)
2738094         309848315616              -829770  01 <C(1) 01414894
2738095         309848315618              -829772  <F(1) 01414895
2738096         309848315620              -829770  01 (0)B> 01414895
2738097         309849975200                   20  01 11414895 (0)B>
2738098         309849975204                   22  01 11414896 (1)A>
2738099         309849975208                   20  01 11414896 <E(0) 01
2738100         309850805000              -829772  01 <E(0) 10414896 01
2738101         309850805002              -829774  <B(0) 10414897 01
2738102         309850805006              -829772  11 (1)A> 10414897 01
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  <F(1) 011+V(1) 00 012
    1                    2                    2  01 (0)B> 011+V(1) 00 012
    2             6+4*V(1)             4+2*V(1)  01 111+V(1) (0)B> 00 012
    3            10+4*V(1)             6+2*V(1)  01 112+V(1) (1)A> 012
    4            12+4*V(1)             8+2*V(1)  01 113+V(1) (1)D> 01
    5            16+4*V(1)             6+2*V(1)  01 113+V(1) <C(1)
    6            22+6*V(1)                    0  01 <C(1) 013+V(1)
    7            24+6*V(1)                   -2  <F(1) 014+V(1)
    8            26+6*V(1)                    0  01 (0)B> 014+V(1)
    9           42+10*V(1)             8+2*V(1)  01 114+V(1) (0)B>
   10           46+10*V(1)            10+2*V(1)  01 115+V(1) (1)A>
   11           50+10*V(1)             8+2*V(1)  01 115+V(1) <E(0) 01
   12           60+12*V(1)                   -2  01 <E(0) 105+V(1) 01
   13           62+12*V(1)                   -4  <B(0) 106+V(1) 01
   14           66+12*V(1)                   -2  11 (1)A> 106+V(1) 01
<< Success! ==> defined new CTR 24 (PPA)
2738102         309850805006              -829772  11 (1)A> 10414897 01
== Executing  PA-CTR 18, V(1)=0, V(2)=414894, repcount=207448, factor=3/2
3982790         697164726374                   20  11622345 (1)A> 10 01
== Executing PPA-CTR 19 (once), V(1)=622343
3982802         697169705160             -1244678  <F(1) 01 00 01622346 00 11
== Executing  PA-CTR  2, V(1)=622343, V(2)=0, repcount=311172, factor=3/2
6161006        1568626494996             -1867022  <F(1) 01933517 00 012 00 11
== Executing PPA-CTR  3 (once), V(1)=933516
6161020        1568637697254             -1867024  11 (1)A> 10933522 01 11
== Executing  PA-CTR  1, V(1)=0, V(2)=933519, repcount=466760, factor=3/2
8961580        3529425976494                   16  111400281 (1)A> 102 01 11
== Executing PPA-CTR 20 (once), V(1)=1400280, V(2)=0
8961597        3529437178788             -2800554  <F(1) 01 00 011400285 002 10
== Executing  PA-CTR  2, V(1)=1400282, V(2)=0, repcount=700142, factor=3/2
13862591        7941237062394             -4200838  <F(1) 012100427 00 01 002 10
13862592        7941237062396             -4200836  01 (0)B> 012100427 00 01 002 10
13862593        7941245464104                   18  01 112100427 (0)B> 00 01 002 10
13862594        7941245464108                   20  01 112100428 (1)A> 01 002 10
13862595        7941245464110                   22  01 112100429 (1)D> 002 10
13862596        7941245464112                   24  01 112100430 (1)B> 00 10
13862597        7941245464114                   22  01 112100430 <C(0) 102
13862598        7941245464116                   20  01 112100429 <C(1) 00 102
13862599        7941249664974             -4200838  01 <C(1) 012100429 00 102
13862600        7941249664976             -4200840  <F(1) 012100430 00 102
13862601        7941249664978             -4200838  01 (0)B> 012100430 00 102
13862602        7941258066698                   22  01 112100430 (0)B> 00 102
13862603        7941258066702                   24  01 112100431 (1)A> 102
13862604        7941258066704                   22  01 112100431 <E(0) 00 10
13862605        7941262267566             -4200840  01 <E(0) 102100431 00 10
13862606        7941262267568             -4200842  <B(0) 102100432 00 10
13862607        7941262267572             -4200840  11 (1)A> 102100432 00 10
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  <F(1) 011+V(2) 00 01 002 101+V(1)
    1                    2                    2  01 (0)B> 011+V(2) 00 01 002 101+V(1)
    2             6+4*V(2)             4+2*V(2)  01 111+V(2) (0)B> 00 01 002 101+V(1)
    3            10+4*V(2)             6+2*V(2)  01 112+V(2) (1)A> 01 002 101+V(1)
    4            12+4*V(2)             8+2*V(2)  01 113+V(2) (1)D> 002 101+V(1)
    5            14+4*V(2)            10+2*V(2)  01 114+V(2) (1)B> 00 101+V(1)
    6            16+4*V(2)             8+2*V(2)  01 114+V(2) <C(0) 102+V(1)
    7            18+4*V(2)             6+2*V(2)  01 113+V(2) <C(1) 00 102+V(1)
    8            24+6*V(2)                    0  01 <C(1) 013+V(2) 00 102+V(1)
    9            26+6*V(2)                   -2  <F(1) 014+V(2) 00 102+V(1)
   10            28+6*V(2)                    0  01 (0)B> 014+V(2) 00 102+V(1)
   11           44+10*V(2)             8+2*V(2)  01 114+V(2) (0)B> 00 102+V(1)
   12           48+10*V(2)            10+2*V(2)  01 115+V(2) (1)A> 102+V(1)
   13           50+10*V(2)             8+2*V(2)  01 115+V(2) <E(0) 00 101+V(1)
   14           60+12*V(2)                   -2  01 <E(0) 105+V(2) 00 101+V(1)
   15           62+12*V(2)                   -4  <B(0) 106+V(2) 00 101+V(1)
   16           66+12*V(2)                   -2  11 (1)A> 106+V(2) 00 101+V(1)
<< Success! ==> defined new CTR 25 (PPA)
13862607        7941262267572             -4200840  11 (1)A> 102100432 00 10
== Executing  PA-CTR  1, V(1)=0, V(2)=2100429, repcount=1050215, factor=3/2
20163897       17867835635532                   20  113150646 (1)A> 102 00 10
== Executing PPA-CTR  8 (once), V(1)=3150645, V(2)=0
20163913       17867879744638             -6301282  <F(1) 01 00 013150650 00 10
== Executing  PA-CTR  2, V(1)=3150647, V(2)=0, repcount=1575324, factor=3/2
31191181       40202714719282             -9451930  <F(1) 014725973 00 012 00 10
== Executing PPA-CTR  3 (once), V(1)=4725972
31191195       40202771431012             -9451932  11 (1)A> 104725978 01 10
== Executing  PA-CTR  1, V(1)=0, V(2)=4725975, repcount=2362988, factor=3/2
45369123       90456203291200                   20  117088965 (1)A> 102 01 10
45369124       90456203291202                   18  117088965 <E(0) 00 10 01 10
45369125       90456217469132            -14177912  <E(0) 107088965 00 10 01 10
45369126       90456217469138            -14177910  11 (1)D> 107088965 00 10 01 10
45369127       90456245824998                   20  117088966 (1)D> 00 10 01 10
45369128       90456245825000                   22  117088967 (1)B> 10 01 10
45369129       90456245825002                   24  117088968 (1)A> 01 10
45369130       90456245825004                   26  117088969 (1)D> 10
45369131       90456245825008                   28  117088970 (1)D>
45369132       90456245825010                   30  117088971 (1)B>
45369133       90456245825012                   28  117088971 <C(0) 10
45369134       90456245825014                   26  117088970 <C(1) 00 10
45369135       90456260002954            -14177914  <C(1) 017088970 00 10
45369136       90456260002956            -14177916  <A(1) 017088971 00 10
45369137       90456260002958            -14177914  01 (1)D> 017088971 00 10
45369138       90456260002962            -14177916  01 <C(1) 00 017088970 00 10
45369139       90456260002964            -14177918  <F(1) 01 00 017088970 00 10
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  111+V(1) (1)A> 102 01 101+V(2)
    1                    2                   -2  111+V(1) <E(0) 00 10 01 101+V(2)
    2             4+2*V(1)           -4+-2*V(1)  <E(0) 101+V(1) 00 10 01 101+V(2)
    3            10+2*V(1)           -2+-2*V(1)  11 (1)D> 101+V(1) 00 10 01 101+V(2)
    4            14+6*V(1)                    0  112+V(1) (1)D> 00 10 01 101+V(2)
    5            16+6*V(1)                    2  113+V(1) (1)B> 10 01 101+V(2)
    6            18+6*V(1)                    4  114+V(1) (1)A> 01 101+V(2)
    7            20+6*V(1)                    6  115+V(1) (1)D> 101+V(2)
    8     24+6*V(1)+4*V(2)             8+2*V(2)  116+V(1)+V(2) (1)D>
    9     26+6*V(1)+4*V(2)            10+2*V(2)  117+V(1)+V(2) (1)B>
   10     28+6*V(1)+4*V(2)             8+2*V(2)  117+V(1)+V(2) <C(0) 10
   11     30+6*V(1)+4*V(2)             6+2*V(2)  116+V(1)+V(2) <C(1) 00 10
   12     42+8*V(1)+6*V(2)           -6+-2*V(1)  <C(1) 016+V(1)+V(2) 00 10
   13     44+8*V(1)+6*V(2)           -8+-2*V(1)  <A(1) 017+V(1)+V(2) 00 10
   14     46+8*V(1)+6*V(2)           -6+-2*V(1)  01 (1)D> 017+V(1)+V(2) 00 10
   15     50+8*V(1)+6*V(2)           -8+-2*V(1)  01 <C(1) 00 016+V(1)+V(2) 00 10
   16     52+8*V(1)+6*V(2)          -10+-2*V(1)  <F(1) 01 00 016+V(1)+V(2) 00 10
<< Success! ==> defined new CTR 26 (PPA)
45369139       90456260002964            -14177918  <F(1) 01 00 017088970 00 10
== Executing  PA-CTR  2, V(1)=7088967, V(2)=0, repcount=3544484, factor=3/2
70180527      203526614606528            -21266886  <F(1) 0110633453 00 012 00 10
== Executing PPA-CTR  3 (once), V(1)=10633452
70180541      203526742208018            -21266888  11 (1)A> 1010633458 01 10
== Executing  PA-CTR  1, V(1)=0, V(2)=10633455, repcount=5316728, factor=3/2
102080909      457935159692426                   24  1115950185 (1)A> 102 01 10
== Executing PPA-CTR 26 (once), V(1)=15950184, V(2)=0
102080925      457935287293950            -31900354  <F(1) 01 00 0115950190 00 10
== Executing  PA-CTR  2, V(1)=15950187, V(2)=0, repcount=7975094, factor=3/2
157906583     1030354525699884            -47850542  <F(1) 0123925283 00 012 00 10
== Executing PPA-CTR  3 (once), V(1)=23925282
157906597     1030354812803334            -47850544  11 (1)A> 1023925288 01 10
== Executing  PA-CTR  1, V(1)=0, V(2)=23925285, repcount=11962643, factor=3/2
229682455     2318298368376162                   28  1135887930 (1)A> 102 01 10
== Executing PPA-CTR 26 (once), V(1)=35887929, V(2)=0
229682471     2318298655479646            -71775840  <F(1) 01 00 0135887935 00 10
== Executing  PA-CTR  2, V(1)=35887932, V(2)=0, repcount=17943967, factor=3/2
355290240     5216172489912952           -107663774  <F(1) 0153831902 00 01 00 10
355290241     5216172489912954           -107663772  01 (0)B> 0153831902 00 01 00 10
355290242     5216172705240562                   32  01 1153831902 (0)B> 00 01 00 10
355290243     5216172705240566                   34  01 1153831903 (1)A> 01 00 10
355290244     5216172705240568                   36  01 1153831904 (1)D> 00 10
355290245     5216172705240570                   38  01 1153831905 (1)B> 10
355290246     5216172705240572                   40  01 1153831906 (1)A>
355290247     5216172705240576                   38  01 1153831906 <E(0) 01
355290248     5216172812904388           -107663774  01 <E(0) 1053831906 01
355290249     5216172812904390           -107663776  <B(0) 1053831907 01
355290250     5216172812904394           -107663774  11 (1)A> 1053831907 01
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  <F(1) 011+V(1) 00 01 00 10
    1                    2                    2  01 (0)B> 011+V(1) 00 01 00 10
    2             6+4*V(1)             4+2*V(1)  01 111+V(1) (0)B> 00 01 00 10
    3            10+4*V(1)             6+2*V(1)  01 112+V(1) (1)A> 01 00 10
    4            12+4*V(1)             8+2*V(1)  01 113+V(1) (1)D> 00 10
    5            14+4*V(1)            10+2*V(1)  01 114+V(1) (1)B> 10
    6            16+4*V(1)            12+2*V(1)  01 115+V(1) (1)A>
    7            20+4*V(1)            10+2*V(1)  01 115+V(1) <E(0) 01
    8            30+6*V(1)                    0  01 <E(0) 105+V(1) 01
    9            32+6*V(1)                   -2  <B(0) 106+V(1) 01
   10            36+6*V(1)                    0  11 (1)A> 106+V(1) 01
<< Success! ==> defined new CTR 27 (PPA)
355290250     5216172812904394           -107663774  11 (1)A> 1053831907 01
== Executing  PA-CTR 18, V(1)=0, V(2)=53831904, repcount=26915953, factor=3/2
516785968    11736389788231852                   38  1180747860 (1)A> 10 01
== Executing PPA-CTR 19 (once), V(1)=80747858
516785980    11736390434214758           -161495690  <F(1) 01 00 0180747861 00 11
== Executing  PA-CTR  2, V(1)=80747858, V(2)=0, repcount=40373930, factor=3/2
799403490    26406879052627808           -242243550  <F(1) 01121121791 00 01 00 11
799403491    26406879052627810           -242243548  01 (0)B> 01121121791 00 01 00 11
799403492    26406879537114974                   34  01 11121121791 (0)B> 00 01 00 11
799403493    26406879537114978                   36  01 11121121792 (1)A> 01 00 11
799403494    26406879537114980                   38  01 11121121793 (1)D> 00 11
799403495    26406879537114982                   40  01 11121121794 (1)B> 11

Lines:       501
Top steps:   500
Macro steps: 799403495
Basic steps: 26406879537114982
Tape index:  40
ones:        242243592
log10(ones    ):    8.384
log10(steps   ):   16.422

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

To the BB simulations page of Heiner Marxen.
To the busy beaver page of Heiner Marxen.
To the home page of Heiner Marxen.
Input to awk program:
    gohalt 1
    L 26
    5T B1R C0L A1L D1R B0L E0L A1R B0R F1L C1L D1R Z1R :  >6.7*10^47 >2.0*10^95
    T 6-state TM #l from MaBu-List
    M	501
    pref	sim
    machv mbL6_l  	just simple
    machv mbL6_l-r	with repetitions reduced
    machv mbL6_l-1	with tape symbol exponents
    machv mbL6_l-m	as 1-bck-2-macro machine
    machv mbL6_l-a	as 1-bck-2-macro machine with pure additive config-TRs
    iam	mbL6_l-a
    mtype	1 0 2
    mmtyp	3
    r	1
    H	1
    mac	0
    E	2
    sympr	
    HM	1
    date	Tue Jul  6 22:11:02 CEST 2010
    edate	Tue Jul  6 22:11:04 CEST 2010
    bnspeed	1

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