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

Comment: This TM produces >4.0x10^3860 nonzeros in >3.9x10^7721 steps.

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

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

Steps             BasSteps              BasTpos  Tape contents
    0                    0                    0  (00)A>
    1                    5                   -3  <A(22) 02
    2                   12                    0  01 (01)D> 02
    3                   14                    2  012 (20)D>
    4                   23                   -1  012 <A(20)
    5                   28                    2  01 10 (12)C>
    6                   37                   -1  01 10 <C(20) 20
    7                   39                   -3  01 <A(12) 202
    8                   46                    0  11 (01)D> 202
    9                   49                   -3  11 <C(20) 00 20
   10                   58                    0  01 (01)B> 00 20
   11                   61                   -3  01 <C(20) 202
   12                   63                   -5  <C(20) 203
   13                   72                   -2  10 (12)C> 203
   14                   74                    0  10 12 (02)C> 202
   15                   78                    4  10 12 022 (02)C>
   16                   83                    1  10 12 022 <C(20)
   17                   97                   -1  10 12 02 <B(02) 02
   18                   99                   -3  10 12 <C(21) 022
   19                  103                   -5  10 <A(12) 01 022
   20                  106                   -2  11 (01)D> 01 022
   21                  114                    0  11 01 (01)B> 022
   22                  117                   -3  11 01 <C(20) 22 02
   23                  119                   -5  11 <C(20) 20 22 02
   24                  128                   -2  01 (01)B> 20 22 02
   25                  134                    0  012 (01)B> 22 02
   26                  140                    2  013 (01)D> 02
   27                  142                    4  014 (20)D>
   28                  151                    1  014 <A(20)
   29                  156                    4  013 10 (12)C>
   30                  165                    1  013 10 <C(20) 20
   31                  167                   -1  013 <A(12) 202
   32                  174                    2  012 11 (01)D> 202
   33                  177                   -1  012 11 <C(20) 00 20
   34                  186                    2  013 (01)B> 00 20
   35                  189                   -1  013 <C(20) 202
   36                  195                   -7  <C(20) 205
   37                  204                   -4  10 (12)C> 205
   38                  206                   -2  10 12 (02)C> 204
   39                  214                    6  10 12 024 (02)C>
   40                  219                    3  10 12 024 <C(20)
   41                  233                    1  10 12 023 <B(02) 02
   42                  235                   -1  10 12 022 <C(21) 022
   43                  246                    2  10 12 02 10 (10)A> 022
   44                  258                    6  10 12 02 103 (10)A>
   45                  263                    3  10 12 02 103 <B(02) 02
   46                  269                   -3  10 12 02 <B(02) 024
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  [*]* [*]* 023+V(1) <B(02) 021+V(2)
    1                    2                   -2  [*]* [*]* 022+V(1) <C(21) 022+V(2)
    2                   13                    1  [*]* [*]* 021+V(1) 10 (10)A> 022+V(2)
    3            25+6*V(2)             5+2*V(2)  [*]* [*]* 021+V(1) 103+V(2) (10)A>
    4            30+6*V(2)             2+2*V(2)  [*]* [*]* 021+V(1) 103+V(2) <B(02) 02
    5            36+8*V(2)                   -4  [*]* [*]* 021+V(1) <B(02) 024+V(2)
<< Success! ==> defined new CTR 1 (PA)
   47                  271                   -5  10 12 <C(21) 025
   48                  275                   -7  10 <A(12) 01 025
   49                  278                   -4  11 (01)D> 01 025
   50                  286                   -2  11 01 (01)B> 025
   51                  289                   -5  11 01 <C(20) 22 024
   52                  291                   -7  11 <C(20) 20 22 024
   53                  300                   -4  01 (01)B> 20 22 024
   54                  306                   -2  012 (01)B> 22 024
   55                  312                    0  013 (01)D> 024
   56                  314                    2  014 (20)D> 023
   57                  320                    8  014 203 (20)D>
   58                  329                    5  014 203 <A(20)
   59                  336                    8  014 202 21 (01)B>
   60                  339                    5  014 202 21 <C(20) 20
   61                  341                    3  014 202 <B(10) 202
   62                  345                    1  014 20 <A(20) 10 202
   63                  352                    4  014 21 (01)B> 10 202
   64                  354                    6  014 21 01 (01)B> 202
   65                  366                   10  014 21 013 (01)B>
   66                  369                    7  014 21 013 <C(20) 20
   67                  375                    1  014 21 <C(20) 204
   68                  377                   -1  014 <B(10) 205
   69                  382                    2  014 (01)B> 205
   70                  412                   12  019 (01)B>
   71                  415                    9  019 <C(20) 20
   72                  433                   -9  <C(20) 2010
   73                  442                   -6  10 (12)C> 2010
   74                  444                   -4  10 12 (02)C> 209
   75                  462                   14  10 12 029 (02)C>
   76                  467                   11  10 12 029 <C(20)
   77                  481                    9  10 12 028 <B(02) 02
>> Try to prove a PPA-CTR with 0 Vars...
    0                    0                    0  10 12 02 <B(02) 024
    1                    2                   -2  10 12 <C(21) 025
    2                    6                   -4  10 <A(12) 01 025
    3                    9                   -1  11 (01)D> 01 025
    4                   17                    1  11 01 (01)B> 025
    5                   20                   -2  11 01 <C(20) 22 024
    6                   22                   -4  11 <C(20) 20 22 024
    7                   31                   -1  01 (01)B> 20 22 024
    8                   37                    1  012 (01)B> 22 024
    9                   43                    3  013 (01)D> 024
   10                   45                    5  014 (20)D> 023
   11                   51                   11  014 203 (20)D>
   12                   60                    8  014 203 <A(20)
   13                   67                   11  014 202 21 (01)B>
   14                   70                    8  014 202 21 <C(20) 20
   15                   72                    6  014 202 <B(10) 202
   16                   76                    4  014 20 <A(20) 10 202
   17                   83                    7  014 21 (01)B> 10 202
   18                   85                    9  014 21 01 (01)B> 202
   19                   97                   13  014 21 013 (01)B>
   20                  100                   10  014 21 013 <C(20) 20
   21                  106                    4  014 21 <C(20) 204
   22                  108                    2  014 <B(10) 205
   23                  113                    5  014 (01)B> 205
   24                  143                   15  019 (01)B>
   25                  146                   12  019 <C(20) 20
   26                  164                   -6  <C(20) 2010
   27                  173                   -3  10 (12)C> 2010
   28                  175                   -1  10 12 (02)C> 209
   29                  193                   17  10 12 029 (02)C>
   30                  198                   14  10 12 029 <C(20)
   31                  212                   12  10 12 028 <B(02) 02
<< Success! ==> defined new CTR 2 (PPA)
   77                  481                    9  10 12 028 <B(02) 02
== Executing  PA-CTR  1, V(1)=5, V(2)=0, repcount=3, factor=3/2
   92                  661                   -3  10 12 022 <B(02) 0210
   93                  663                   -5  10 12 02 <C(21) 0211
   94                  674                   -2  10 12 10 (10)A> 0211
   95                  740                   20  10 12 1012 (10)A>
   96                  745                   17  10 12 1012 <B(02) 02
   97                  769                   -7  10 12 <B(02) 0213
   98                  780                   -4  102 (10)A> 0213
   99                  858                   22  1015 (10)A>
  100                  863                   19  1015 <B(02) 02
  101                  893                  -11  <B(02) 0216
  102                  895                  -13  <A(22) 0217
  103                  902                  -10  01 (01)D> 0217
  104                  904                   -8  012 (20)D> 0216
  105                  936                   24  012 2016 (20)D>
  106                  945                   21  012 2016 <A(20)
  107                  952                   24  012 2015 21 (01)B>
  108                  955                   21  012 2015 21 <C(20) 20
  109                  957                   19  012 2015 <B(10) 202
  110                  961                   17  012 2014 <A(20) 10 202
  111                  968                   20  012 2013 21 (01)B> 10 202
  112                  970                   22  012 2013 21 01 (01)B> 202
  113                  982                   26  012 2013 21 013 (01)B>
  114                  985                   23  012 2013 21 013 <C(20) 20
  115                  991                   17  012 2013 21 <C(20) 204
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  [*]* 203+V(1) 21 <C(20) 201+V(2)
    1                    2                   -2  [*]* 203+V(1) <B(10) 202+V(2)
    2                    6                   -4  [*]* 202+V(1) <A(20) 10 202+V(2)
    3                   13                   -1  [*]* 201+V(1) 21 (01)B> 10 202+V(2)
    4                   15                    1  [*]* 201+V(1) 21 01 (01)B> 202+V(2)
    5            27+6*V(2)             5+2*V(2)  [*]* 201+V(1) 21 013+V(2) (01)B>
    6            30+6*V(2)             2+2*V(2)  [*]* 201+V(1) 21 013+V(2) <C(20) 20
    7            36+8*V(2)                   -4  [*]* 201+V(1) 21 <C(20) 204+V(2)
<< Success! ==> defined new CTR 3 (PA)
  115                  991                   17  012 2013 21 <C(20) 204
== Executing  PA-CTR  3, V(1)=10, V(2)=3, repcount=6, factor=3/2
  157                 1711                   -7  012 20 21 <C(20) 2022
  158                 1713                   -9  012 20 <B(10) 2023
  159                 1717                  -11  012 <A(20) 10 2023
  160                 1722                   -8  01 10 (12)C> 10 2023
  161                 1733                  -11  01 10 <B(02) 02 2023
  162                 1735                  -13  01 <B(02) 022 2023
  163                 1742                  -10  (10)A> 022 2023
  164                 1754                   -6  102 (10)A> 2023
  165                 1756                   -4  103 (12)C> 2022
  166                 1758                   -2  103 12 (02)C> 2021
  167                 1800                   40  103 12 0221 (02)C>
  168                 1805                   37  103 12 0221 <C(20)
  169                 1819                   35  103 12 0220 <B(02) 02
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  012 20 21 <C(20) 205+V(1)
    1                    2                   -2  012 20 <B(10) 206+V(1)
    2                    6                   -4  012 <A(20) 10 206+V(1)
    3                   11                   -1  01 10 (12)C> 10 206+V(1)
    4                   22                   -4  01 10 <B(02) 02 206+V(1)
    5                   24                   -6  01 <B(02) 022 206+V(1)
    6                   31                   -3  (10)A> 022 206+V(1)
    7                   43                    1  102 (10)A> 206+V(1)
    8                   45                    3  103 (12)C> 205+V(1)
    9                   47                    5  103 12 (02)C> 204+V(1)
   10            55+2*V(1)            13+2*V(1)  103 12 024+V(1) (02)C>
   11            60+2*V(1)            10+2*V(1)  103 12 024+V(1) <C(20)
   12            74+2*V(1)             8+2*V(1)  103 12 023+V(1) <B(02) 02
<< Success! ==> defined new CTR 4 (PPA)
  169                 1819                   35  103 12 0220 <B(02) 02
== Executing  PA-CTR  1, V(1)=17, V(2)=0, repcount=9, factor=3/2
  214                 3007                   -1  103 12 022 <B(02) 0228
  215                 3009                   -3  103 12 02 <C(21) 0229
  216                 3020                    0  103 12 10 (10)A> 0229
  217                 3194                   58  103 12 1030 (10)A>
  218                 3199                   55  103 12 1030 <B(02) 02
  219                 3259                   -5  103 12 <B(02) 0231
  220                 3270                   -2  104 (10)A> 0231
  221                 3456                   60  1035 (10)A>
  222                 3461                   57  1035 <B(02) 02
  223                 3531                  -13  <B(02) 0236
  224                 3533                  -15  <A(22) 0237
  225                 3540                  -12  01 (01)D> 0237
  226                 3542                  -10  012 (20)D> 0236
  227                 3614                   62  012 2036 (20)D>
  228                 3623                   59  012 2036 <A(20)
  229                 3630                   62  012 2035 21 (01)B>
  230                 3633                   59  012 2035 21 <C(20) 20
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  101+V(1) 12 022 <B(02) 021+V(2)
    1                    2                   -2  101+V(1) 12 02 <C(21) 022+V(2)
    2                   13                    1  101+V(1) 12 10 (10)A> 022+V(2)
    3            25+6*V(2)             5+2*V(2)  101+V(1) 12 103+V(2) (10)A>
    4            30+6*V(2)             2+2*V(2)  101+V(1) 12 103+V(2) <B(02) 02
    5            36+8*V(2)                   -4  101+V(1) 12 <B(02) 024+V(2)
    6            47+8*V(2)                   -1  102+V(1) (10)A> 024+V(2)
    7           71+14*V(2)             7+2*V(2)  106+V(1)+V(2) (10)A>
    8           76+14*V(2)             4+2*V(2)  106+V(1)+V(2) <B(02) 02
    9    88+2*V(1)+16*V(2)           -8+-2*V(1)  <B(02) 027+V(1)+V(2)
   10    90+2*V(1)+16*V(2)          -10+-2*V(1)  <A(22) 028+V(1)+V(2)
   11    97+2*V(1)+16*V(2)           -7+-2*V(1)  01 (01)D> 028+V(1)+V(2)
   12    99+2*V(1)+16*V(2)           -5+-2*V(1)  012 (20)D> 027+V(1)+V(2)
   13   113+4*V(1)+18*V(2)             9+2*V(2)  012 207+V(1)+V(2) (20)D>
   14   122+4*V(1)+18*V(2)             6+2*V(2)  012 207+V(1)+V(2) <A(20)
   15   129+4*V(1)+18*V(2)             9+2*V(2)  012 206+V(1)+V(2) 21 (01)B>
   16   132+4*V(1)+18*V(2)             6+2*V(2)  012 206+V(1)+V(2) 21 <C(20) 20
<< Success! ==> defined new CTR 5 (PPA)
  230                 3633                   59  012 2035 21 <C(20) 20
== Executing  PA-CTR  3, V(1)=32, V(2)=0, repcount=17, factor=3/2
  349                 7509                   -9  012 20 21 <C(20) 2052
== Executing PPA-CTR  4 (once), V(1)=47
  361                 7677                   93  103 12 0250 <B(02) 02
== Executing  PA-CTR  1, V(1)=47, V(2)=0, repcount=24, factor=3/2
  481                15165                   -3  103 12 022 <B(02) 0273
== Executing PPA-CTR  5 (once), V(1)=2, V(2)=72
  497                16601                  147  012 2080 21 <C(20) 20
== Executing  PA-CTR  3, V(1)=77, V(2)=0, repcount=39, factor=3/2
  770                35789                   -9  012 202 21 <C(20) 20118
  771                35791                  -11  012 202 <B(10) 20119
  772                35795                  -13  012 20 <A(20) 10 20119
  773                35802                  -10  012 21 (01)B> 10 20119
  774                35804                   -8  012 21 01 (01)B> 20119
  775                36518                  230  012 21 01120 (01)B>
  776                36521                  227  012 21 01120 <C(20) 20
  777                36761                  -13  012 21 <C(20) 20121
  778                36763                  -15  012 <B(10) 20122
  779                36768                  -12  012 (01)B> 20122
  780                37500                  232  01124 (01)B>
  781                37503                  229  01124 <C(20) 20
  782                37751                  -19  <C(20) 20125
  783                37760                  -16  10 (12)C> 20125
  784                37762                  -14  10 12 (02)C> 20124
  785                38010                  234  10 12 02124 (02)C>
  786                38015                  231  10 12 02124 <C(20)
  787                38029                  229  10 12 02123 <B(02) 02
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  011+V(1) 202 21 <C(20) 201+V(2)
    1                    2                   -2  011+V(1) 202 <B(10) 202+V(2)
    2                    6                   -4  011+V(1) 20 <A(20) 10 202+V(2)
    3                   13                   -1  011+V(1) 21 (01)B> 10 202+V(2)
    4                   15                    1  011+V(1) 21 01 (01)B> 202+V(2)
    5            27+6*V(2)             5+2*V(2)  011+V(1) 21 013+V(2) (01)B>
    6            30+6*V(2)             2+2*V(2)  011+V(1) 21 013+V(2) <C(20) 20
    7            36+8*V(2)                   -4  011+V(1) 21 <C(20) 204+V(2)
    8            38+8*V(2)                   -6  011+V(1) <B(10) 205+V(2)
    9            43+8*V(2)                   -3  011+V(1) (01)B> 205+V(2)
   10           73+14*V(2)             7+2*V(2)  016+V(1)+V(2) (01)B>
   11           76+14*V(2)             4+2*V(2)  016+V(1)+V(2) <C(20) 20
   12    88+2*V(1)+16*V(2)           -8+-2*V(1)  <C(20) 207+V(1)+V(2)
   13    97+2*V(1)+16*V(2)           -5+-2*V(1)  10 (12)C> 207+V(1)+V(2)
   14    99+2*V(1)+16*V(2)           -3+-2*V(1)  10 12 (02)C> 206+V(1)+V(2)
   15   111+4*V(1)+18*V(2)             9+2*V(2)  10 12 026+V(1)+V(2) (02)C>
   16   116+4*V(1)+18*V(2)             6+2*V(2)  10 12 026+V(1)+V(2) <C(20)
   17   130+4*V(1)+18*V(2)             4+2*V(2)  10 12 025+V(1)+V(2) <B(02) 02
<< Success! ==> defined new CTR 6 (PPA)
  787                38029                  229  10 12 02123 <B(02) 02
== Executing  PA-CTR  1, V(1)=120, V(2)=0, repcount=61, factor=3/2
 1092                84145                  -15  10 12 02 <B(02) 02184
 1093                84147                  -17  10 12 <C(21) 02185
 1094                84151                  -19  10 <A(12) 01 02185
 1095                84154                  -16  11 (01)D> 01 02185
 1096                84162                  -14  11 01 (01)B> 02185
 1097                84165                  -17  11 01 <C(20) 22 02184
 1098                84167                  -19  11 <C(20) 20 22 02184
 1099                84176                  -16  01 (01)B> 20 22 02184
 1100                84182                  -14  012 (01)B> 22 02184
 1101                84188                  -12  013 (01)D> 02184
 1102                84190                  -10  014 (20)D> 02183
 1103                84556                  356  014 20183 (20)D>
 1104                84565                  353  014 20183 <A(20)
 1105                84572                  356  014 20182 21 (01)B>
 1106                84575                  353  014 20182 21 <C(20) 20
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  10 12 02 <B(02) 025+V(1)
    1                    2                   -2  10 12 <C(21) 026+V(1)
    2                    6                   -4  10 <A(12) 01 026+V(1)
    3                    9                   -1  11 (01)D> 01 026+V(1)
    4                   17                    1  11 01 (01)B> 026+V(1)
    5                   20                   -2  11 01 <C(20) 22 025+V(1)
    6                   22                   -4  11 <C(20) 20 22 025+V(1)
    7                   31                   -1  01 (01)B> 20 22 025+V(1)
    8                   37                    1  012 (01)B> 22 025+V(1)
    9                   43                    3  013 (01)D> 025+V(1)
   10                   45                    5  014 (20)D> 024+V(1)
   11            53+2*V(1)            13+2*V(1)  014 204+V(1) (20)D>
   12            62+2*V(1)            10+2*V(1)  014 204+V(1) <A(20)
   13            69+2*V(1)            13+2*V(1)  014 203+V(1) 21 (01)B>
   14            72+2*V(1)            10+2*V(1)  014 203+V(1) 21 <C(20) 20
<< Success! ==> defined new CTR 7 (PPA)
 1106                84575                  353  014 20182 21 <C(20) 20
== Executing  PA-CTR  3, V(1)=179, V(2)=0, repcount=90, factor=3/2
 1736               183935                   -7  014 202 21 <C(20) 20271
== Executing PPA-CTR  6 (once), V(1)=3, V(2)=270
 1753               188937                  537  10 12 02278 <B(02) 02
== Executing  PA-CTR  1, V(1)=275, V(2)=0, repcount=138, factor=3/2
 2443               420777                  -15  10 12 022 <B(02) 02415
== Executing PPA-CTR  5 (once), V(1)=0, V(2)=414
 2459               428361                  819  012 20420 21 <C(20) 20
== Executing  PA-CTR  3, V(1)=417, V(2)=0, repcount=209, factor=3/2
 3922               957549                  -17  012 202 21 <C(20) 20628
== Executing PPA-CTR  6 (once), V(1)=1, V(2)=627
 3939               968969                 1241  10 12 02633 <B(02) 02
== Executing  PA-CTR  1, V(1)=630, V(2)=0, repcount=316, factor=3/2
 5519              2174825                  -23  10 12 02 <B(02) 02949
== Executing PPA-CTR  7 (once), V(1)=944
 5533              2176785                 1875  014 20947 21 <C(20) 20
== Executing  PA-CTR  3, V(1)=944, V(2)=0, repcount=473, factor=3/2
 8844              4872885                  -17  014 20 21 <C(20) 201420
 8845              4872887                  -19  014 20 <B(10) 201421
 8846              4872891                  -21  014 <A(20) 10 201421
 8847              4872896                  -18  013 10 (12)C> 10 201421
 8848              4872907                  -21  013 10 <B(02) 02 201421
 8849              4872909                  -23  013 <B(02) 022 201421
 8850              4872916                  -20  012 00 (10)A> 022 201421
 8851              4872928                  -16  012 00 102 (10)A> 201421
 8852              4872930                  -14  012 00 103 (12)C> 201420
 8853              4872932                  -12  012 00 103 12 (02)C> 201419
 8854              4875770                 2826  012 00 103 12 021419 (02)C>
 8855              4875775                 2823  012 00 103 12 021419 <C(20)
 8856              4875789                 2821  012 00 103 12 021418 <B(02) 02
 8857              4875791                 2819  012 00 103 12 021417 <C(21) 022
 8858              4875802                 2822  012 00 103 12 021416 10 (10)A> 022
 8859              4875814                 2826  012 00 103 12 021416 103 (10)A>
 8860              4875819                 2823  012 00 103 12 021416 103 <B(02) 02
 8861              4875825                 2817  012 00 103 12 021416 <B(02) 024
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  [*]* [*]* [*]* [*]* 023+V(1) <B(02) 021+V(2)
    1                    2                   -2  [*]* [*]* [*]* [*]* 022+V(1) <C(21) 022+V(2)
    2                   13                    1  [*]* [*]* [*]* [*]* 021+V(1) 10 (10)A> 022+V(2)
    3            25+6*V(2)             5+2*V(2)  [*]* [*]* [*]* [*]* 021+V(1) 103+V(2) (10)A>
    4            30+6*V(2)             2+2*V(2)  [*]* [*]* [*]* [*]* 021+V(1) 103+V(2) <B(02) 02
    5            36+8*V(2)                   -4  [*]* [*]* [*]* [*]* 021+V(1) <B(02) 024+V(2)
<< Success! ==> defined new CTR 8 (PA)
 8861              4875825                 2817  012 00 103 12 021416 <B(02) 024
== Executing  PA-CTR  8, V(1)=1413, V(2)=3, repcount=707, factor=3/2
12396             10907949                  -11  012 00 103 12 022 <B(02) 022125
12397             10907951                  -13  012 00 103 12 02 <C(21) 022126
12398             10907962                  -10  012 00 103 12 10 (10)A> 022126
12399             10920718                 4242  012 00 103 12 102127 (10)A>
12400             10920723                 4239  012 00 103 12 102127 <B(02) 02
12401             10924977                  -15  012 00 103 12 <B(02) 022128
12402             10924988                  -12  012 00 104 (10)A> 022128
12403             10937756                 4244  012 00 102132 (10)A>
12404             10937761                 4241  012 00 102132 <B(02) 02
12405             10942025                  -23  012 00 <B(02) 022133
12406             10942027                  -25  012 <A(22) 022134
12407             10942035                  -27  01 <B(02) 00 022134
12408             10942042                  -24  (10)A> 00 022134
12409             10942047                  -27  <B(02) 022135
12410             10942049                  -29  <A(22) 022136
12411             10942056                  -26  01 (01)D> 022136
12412             10942058                  -24  012 (20)D> 022135
12413             10946328                 4246  012 202135 (20)D>
12414             10946337                 4243  012 202135 <A(20)
12415             10946344                 4246  012 202134 21 (01)B>
12416             10946347                 4243  012 202134 21 <C(20) 20
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  012 00 101+V(1) 12 022 <B(02) 021+V(2)
    1                    2                   -2  012 00 101+V(1) 12 02 <C(21) 022+V(2)
    2                   13                    1  012 00 101+V(1) 12 10 (10)A> 022+V(2)
    3            25+6*V(2)             5+2*V(2)  012 00 101+V(1) 12 103+V(2) (10)A>
    4            30+6*V(2)             2+2*V(2)  012 00 101+V(1) 12 103+V(2) <B(02) 02
    5            36+8*V(2)                   -4  012 00 101+V(1) 12 <B(02) 024+V(2)
    6            47+8*V(2)                   -1  012 00 102+V(1) (10)A> 024+V(2)
    7           71+14*V(2)             7+2*V(2)  012 00 106+V(1)+V(2) (10)A>
    8           76+14*V(2)             4+2*V(2)  012 00 106+V(1)+V(2) <B(02) 02
    9    88+2*V(1)+16*V(2)           -8+-2*V(1)  012 00 <B(02) 027+V(1)+V(2)
   10    90+2*V(1)+16*V(2)          -10+-2*V(1)  012 <A(22) 028+V(1)+V(2)
   11    98+2*V(1)+16*V(2)          -12+-2*V(1)  01 <B(02) 00 028+V(1)+V(2)
   12   105+2*V(1)+16*V(2)           -9+-2*V(1)  (10)A> 00 028+V(1)+V(2)
   13   110+2*V(1)+16*V(2)          -12+-2*V(1)  <B(02) 029+V(1)+V(2)
   14   112+2*V(1)+16*V(2)          -14+-2*V(1)  <A(22) 0210+V(1)+V(2)
   15   119+2*V(1)+16*V(2)          -11+-2*V(1)  01 (01)D> 0210+V(1)+V(2)
   16   121+2*V(1)+16*V(2)           -9+-2*V(1)  012 (20)D> 029+V(1)+V(2)
   17   139+4*V(1)+18*V(2)             9+2*V(2)  012 209+V(1)+V(2) (20)D>
   18   148+4*V(1)+18*V(2)             6+2*V(2)  012 209+V(1)+V(2) <A(20)
   19   155+4*V(1)+18*V(2)             9+2*V(2)  012 208+V(1)+V(2) 21 (01)B>
   20   158+4*V(1)+18*V(2)             6+2*V(2)  012 208+V(1)+V(2) 21 <C(20) 20
<< Success! ==> defined new CTR 9 (PPA)
12416             10946347                 4243  012 202134 21 <C(20) 20
== Executing  PA-CTR  3, V(1)=2131, V(2)=0, repcount=1066, factor=3/2
19878             24608203                  -21  012 202 21 <C(20) 203199
== Executing PPA-CTR  6 (once), V(1)=1, V(2)=3198
19895             24665901                 6379  10 12 023204 <B(02) 02
== Executing  PA-CTR  1, V(1)=3201, V(2)=0, repcount=1601, factor=3/2
27900             55462737                  -25  10 12 022 <B(02) 024804
== Executing PPA-CTR  5 (once), V(1)=0, V(2)=4803
27916             55549323                 9587  012 204809 21 <C(20) 20
== Executing  PA-CTR  3, V(1)=4806, V(2)=0, repcount=2404, factor=3/2
44744            124957611                  -29  012 20 21 <C(20) 207213
== Executing PPA-CTR  4 (once), V(1)=7208
44756            124972101                14395  103 12 027211 <B(02) 02
== Executing  PA-CTR  1, V(1)=7208, V(2)=0, repcount=3605, factor=3/2
62781            281010921                  -25  103 12 02 <B(02) 0210816
62782            281010923                  -27  103 12 <C(21) 0210817
62783            281010927                  -29  103 <A(12) 01 0210817
62784            281010930                  -26  102 11 (01)D> 01 0210817
62785            281010938                  -24  102 11 01 (01)B> 0210817
62786            281010941                  -27  102 11 01 <C(20) 22 0210816
62787            281010943                  -29  102 11 <C(20) 20 22 0210816
62788            281010952                  -26  102 01 (01)B> 20 22 0210816
62789            281010958                  -24  102 012 (01)B> 22 0210816
62790            281010964                  -22  102 013 (01)D> 0210816
62791            281010966                  -20  102 014 (20)D> 0210815
62792            281032596                21610  102 014 2010815 (20)D>
62793            281032605                21607  102 014 2010815 <A(20)
62794            281032612                21610  102 014 2010814 21 (01)B>
62795            281032615                21607  102 014 2010814 21 <C(20) 20
62796            281032617                21605  102 014 2010814 <B(10) 202
62797            281032621                21603  102 014 2010813 <A(20) 10 202
62798            281032628                21606  102 014 2010812 21 (01)B> 10 202
62799            281032630                21608  102 014 2010812 21 01 (01)B> 202
62800            281032642                21612  102 014 2010812 21 013 (01)B>
62801            281032645                21609  102 014 2010812 21 013 <C(20) 20
62802            281032651                21603  102 014 2010812 21 <C(20) 204
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  [*]* [*]* 203+V(1) 21 <C(20) 201+V(2)
    1                    2                   -2  [*]* [*]* 203+V(1) <B(10) 202+V(2)
    2                    6                   -4  [*]* [*]* 202+V(1) <A(20) 10 202+V(2)
    3                   13                   -1  [*]* [*]* 201+V(1) 21 (01)B> 10 202+V(2)
    4                   15                    1  [*]* [*]* 201+V(1) 21 01 (01)B> 202+V(2)
    5            27+6*V(2)             5+2*V(2)  [*]* [*]* 201+V(1) 21 013+V(2) (01)B>
    6            30+6*V(2)             2+2*V(2)  [*]* [*]* 201+V(1) 21 013+V(2) <C(20) 20
    7            36+8*V(2)                   -4  [*]* [*]* 201+V(1) 21 <C(20) 204+V(2)
<< Success! ==> defined new CTR 10 (PA)
62802            281032651                21603  102 014 2010812 21 <C(20) 204
== Executing  PA-CTR 10, V(1)=10809, V(2)=3, repcount=5405, factor=3/2
100637            631860391                  -17  102 014 202 21 <C(20) 2016219
100638            631860393                  -19  102 014 202 <B(10) 2016220
100639            631860397                  -21  102 014 20 <A(20) 10 2016220
100640            631860404                  -18  102 014 21 (01)B> 10 2016220
100641            631860406                  -16  102 014 21 01 (01)B> 2016220
100642            631957726                32424  102 014 21 0116221 (01)B>
100643            631957729                32421  102 014 21 0116221 <C(20) 20
100644            631990171                  -21  102 014 21 <C(20) 2016222
100645            631990173                  -23  102 014 <B(10) 2016223
100646            631990178                  -20  102 014 (01)B> 2016223
100647            632087516                32426  102 0116227 (01)B>
100648            632087519                32423  102 0116227 <C(20) 20
100649            632119973                  -31  102 <C(20) 2016228
100650            632119975                  -33  10 <A(12) 2016229
100651            632119978                  -30  11 (01)D> 2016229
100652            632119981                  -33  11 <C(20) 00 2016228
100653            632119990                  -30  01 (01)B> 00 2016228
100654            632119993                  -33  01 <C(20) 2016229
100655            632119995                  -35  <C(20) 2016230
100656            632120004                  -32  10 (12)C> 2016230
100657            632120006                  -30  10 12 (02)C> 2016229
100658            632152464                32428  10 12 0216229 (02)C>
100659            632152469                32425  10 12 0216229 <C(20)
100660            632152483                32423  10 12 0216228 <B(02) 02
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  102 011+V(1) 202 21 <C(20) 201+V(2)
    1                    2                   -2  102 011+V(1) 202 <B(10) 202+V(2)
    2                    6                   -4  102 011+V(1) 20 <A(20) 10 202+V(2)
    3                   13                   -1  102 011+V(1) 21 (01)B> 10 202+V(2)
    4                   15                    1  102 011+V(1) 21 01 (01)B> 202+V(2)
    5            27+6*V(2)             5+2*V(2)  102 011+V(1) 21 013+V(2) (01)B>
    6            30+6*V(2)             2+2*V(2)  102 011+V(1) 21 013+V(2) <C(20) 20
    7            36+8*V(2)                   -4  102 011+V(1) 21 <C(20) 204+V(2)
    8            38+8*V(2)                   -6  102 011+V(1) <B(10) 205+V(2)
    9            43+8*V(2)                   -3  102 011+V(1) (01)B> 205+V(2)
   10           73+14*V(2)             7+2*V(2)  102 016+V(1)+V(2) (01)B>
   11           76+14*V(2)             4+2*V(2)  102 016+V(1)+V(2) <C(20) 20
   12    88+2*V(1)+16*V(2)           -8+-2*V(1)  102 <C(20) 207+V(1)+V(2)
   13    90+2*V(1)+16*V(2)          -10+-2*V(1)  10 <A(12) 208+V(1)+V(2)
   14    93+2*V(1)+16*V(2)           -7+-2*V(1)  11 (01)D> 208+V(1)+V(2)
   15    96+2*V(1)+16*V(2)          -10+-2*V(1)  11 <C(20) 00 207+V(1)+V(2)
   16   105+2*V(1)+16*V(2)           -7+-2*V(1)  01 (01)B> 00 207+V(1)+V(2)
   17   108+2*V(1)+16*V(2)          -10+-2*V(1)  01 <C(20) 208+V(1)+V(2)
   18   110+2*V(1)+16*V(2)          -12+-2*V(1)  <C(20) 209+V(1)+V(2)
   19   119+2*V(1)+16*V(2)           -9+-2*V(1)  10 (12)C> 209+V(1)+V(2)
   20   121+2*V(1)+16*V(2)           -7+-2*V(1)  10 12 (02)C> 208+V(1)+V(2)
   21   137+4*V(1)+18*V(2)             9+2*V(2)  10 12 028+V(1)+V(2) (02)C>
   22   142+4*V(1)+18*V(2)             6+2*V(2)  10 12 028+V(1)+V(2) <C(20)
   23   156+4*V(1)+18*V(2)             4+2*V(2)  10 12 027+V(1)+V(2) <B(02) 02
<< Success! ==> defined new CTR 11 (PPA)
100660            632152483                32423  10 12 0216228 <B(02) 02
== Executing  PA-CTR  1, V(1)=16225, V(2)=0, repcount=8113, factor=3/2
141225           1422196423                  -29  10 12 022 <B(02) 0224340
== Executing PPA-CTR  5 (once), V(1)=0, V(2)=24339
141241           1422634657                48655  012 2024345 21 <C(20) 20
== Executing  PA-CTR  3, V(1)=24342, V(2)=0, repcount=12172, factor=3/2
226445           3200817793                  -33  012 20 21 <C(20) 2036517
== Executing PPA-CTR  4 (once), V(1)=36512
226457           3200890891                72999  103 12 0236515 <B(02) 02
== Executing  PA-CTR  1, V(1)=36512, V(2)=0, repcount=18257, factor=3/2
317742           7201145647                  -29  103 12 02 <B(02) 0254772
317743           7201145649                  -31  103 12 <C(21) 0254773
317744           7201145653                  -33  103 <A(12) 01 0254773
317745           7201145656                  -30  102 11 (01)D> 01 0254773
317746           7201145664                  -28  102 11 01 (01)B> 0254773
317747           7201145667                  -31  102 11 01 <C(20) 22 0254772
317748           7201145669                  -33  102 11 <C(20) 20 22 0254772
317749           7201145678                  -30  102 01 (01)B> 20 22 0254772
317750           7201145684                  -28  102 012 (01)B> 22 0254772
317751           7201145690                  -26  102 013 (01)D> 0254772
317752           7201145692                  -24  102 014 (20)D> 0254771
317753           7201255234               109518  102 014 2054771 (20)D>
317754           7201255243               109515  102 014 2054771 <A(20)
317755           7201255250               109518  102 014 2054770 21 (01)B>
317756           7201255253               109515  102 014 2054770 21 <C(20) 20
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  102+V(1) 12 02 <B(02) 025+V(2)
    1                    2                   -2  102+V(1) 12 <C(21) 026+V(2)
    2                    6                   -4  102+V(1) <A(12) 01 026+V(2)
    3                    9                   -1  101+V(1) 11 (01)D> 01 026+V(2)
    4                   17                    1  101+V(1) 11 01 (01)B> 026+V(2)
    5                   20                   -2  101+V(1) 11 01 <C(20) 22 025+V(2)
    6                   22                   -4  101+V(1) 11 <C(20) 20 22 025+V(2)
    7                   31                   -1  101+V(1) 01 (01)B> 20 22 025+V(2)
    8                   37                    1  101+V(1) 012 (01)B> 22 025+V(2)
    9                   43                    3  101+V(1) 013 (01)D> 025+V(2)
   10                   45                    5  101+V(1) 014 (20)D> 024+V(2)
   11            53+2*V(2)            13+2*V(2)  101+V(1) 014 204+V(2) (20)D>
   12            62+2*V(2)            10+2*V(2)  101+V(1) 014 204+V(2) <A(20)
   13            69+2*V(2)            13+2*V(2)  101+V(1) 014 203+V(2) 21 (01)B>
   14            72+2*V(2)            10+2*V(2)  101+V(1) 014 203+V(2) 21 <C(20) 20
<< Success! ==> defined new CTR 12 (PPA)
317756           7201255253               109515  102 014 2054770 21 <C(20) 20
== Executing  PA-CTR 10, V(1)=54767, V(2)=0, repcount=27384, factor=3/2
509444          16200513941                  -21  102 014 202 21 <C(20) 2082153
== Executing PPA-CTR 11 (once), V(1)=3, V(2)=82152
509467          16201992845               164287  10 12 0282162 <B(02) 02
== Executing  PA-CTR  1, V(1)=82159, V(2)=0, repcount=41080, factor=3/2
714867          36453775565                  -33  10 12 022 <B(02) 02123241
== Executing PPA-CTR  5 (once), V(1)=0, V(2)=123240
714883          36455994017               246453  012 20123246 21 <C(20) 20
== Executing  PA-CTR  3, V(1)=123243, V(2)=0, repcount=61622, factor=3/2
1146237          82024723553                  -35  012 202 21 <C(20) 20184867
== Executing PPA-CTR  6 (once), V(1)=1, V(2)=184866
1146254          82028051275               369701  10 12 02184872 <B(02) 02
== Executing  PA-CTR  1, V(1)=184869, V(2)=0, repcount=92435, factor=3/2
1608429         184561020415                  -39  10 12 022 <B(02) 02277306
== Executing PPA-CTR  5 (once), V(1)=0, V(2)=277305
1608445         184566012037               554577  012 20277311 21 <C(20) 20
== Executing  PA-CTR  3, V(1)=277308, V(2)=0, repcount=138655, factor=3/2
2579030         415271848057                  -43  012 20 21 <C(20) 20415966
== Executing PPA-CTR  4 (once), V(1)=415961
2579042         415272680053               831887  103 12 02415964 <B(02) 02
== Executing  PA-CTR  1, V(1)=415961, V(2)=0, repcount=207981, factor=3/2
3618947         934350827929                  -37  103 12 022 <B(02) 02623944
== Executing PPA-CTR  5 (once), V(1)=2, V(2)=623943
3618963         934362059043              1247855  012 20623951 21 <C(20) 20
== Executing  PA-CTR  3, V(1)=623948, V(2)=0, repcount=311975, factor=3/2
5802788        2102310353943                  -45  012 20 21 <C(20) 20935926
== Executing PPA-CTR  4 (once), V(1)=935921
5802800        2102312225859              1871805  103 12 02935924 <B(02) 02
== Executing  PA-CTR  1, V(1)=935921, V(2)=0, repcount=467961, factor=3/2
8142605        4730173427175                  -39  103 12 022 <B(02) 021403884
== Executing PPA-CTR  5 (once), V(1)=2, V(2)=1403883
8142621        4730198697209              2807733  012 201403891 21 <C(20) 20
== Executing  PA-CTR  3, V(1)=1403888, V(2)=0, repcount=701945, factor=3/2
13056236       10642936940189                  -47  012 20 21 <C(20) 202105836
== Executing PPA-CTR  4 (once), V(1)=2105831
13056248       10642941151925              4211623  103 12 022105834 <B(02) 02
== Executing  PA-CTR  1, V(1)=2105831, V(2)=0, repcount=1052916, factor=3/2
18320828       23946551658581                  -41  103 12 022 <B(02) 023158749
== Executing PPA-CTR  5 (once), V(1)=2, V(2)=3158748
18320844       23946608516185              6317461  012 203158756 21 <C(20) 20
== Executing  PA-CTR  3, V(1)=3158753, V(2)=0, repcount=1579377, factor=3/2
29376483       53879826918781                  -47  012 202 21 <C(20) 204738132
== Executing PPA-CTR  6 (once), V(1)=1, V(2)=4738131
29376500       53879912205273              9476219  10 12 024738137 <B(02) 02
== Executing  PA-CTR  1, V(1)=4738134, V(2)=0, repcount=2369068, factor=3/2
41221840      121229767326393                  -53  10 12 02 <B(02) 027107205
== Executing PPA-CTR  7 (once), V(1)=7107200
41221854      121229781540865             14214357  014 207107203 21 <C(20) 20
== Executing  PA-CTR  3, V(1)=7107200, V(2)=0, repcount=3553601, factor=3/2
66097061      272766827633701                  -47  014 20 21 <C(20) 2010660804
66097062      272766827633703                  -49  014 20 <B(10) 2010660805
66097063      272766827633707                  -51  014 <A(20) 10 2010660805
66097064      272766827633712                  -48  013 10 (12)C> 10 2010660805
66097065      272766827633723                  -51  013 10 <B(02) 02 2010660805
66097066      272766827633725                  -53  013 <B(02) 022 2010660805
66097067      272766827633732                  -50  012 00 (10)A> 022 2010660805
66097068      272766827633744                  -46  012 00 102 (10)A> 2010660805
66097069      272766827633746                  -44  012 00 103 (12)C> 2010660804
66097070      272766827633748                  -42  012 00 103 12 (02)C> 2010660803
66097071      272766848955354             21321564  012 00 103 12 0210660803 (02)C>
66097072      272766848955359             21321561  012 00 103 12 0210660803 <C(20)
66097073      272766848955373             21321559  012 00 103 12 0210660802 <B(02) 02
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  013+V(1) 20 21 <C(20) 205+V(2)
    1                    2                   -2  013+V(1) 20 <B(10) 206+V(2)
    2                    6                   -4  013+V(1) <A(20) 10 206+V(2)
    3                   11                   -1  012+V(1) 10 (12)C> 10 206+V(2)
    4                   22                   -4  012+V(1) 10 <B(02) 02 206+V(2)
    5                   24                   -6  012+V(1) <B(02) 022 206+V(2)
    6                   31                   -3  011+V(1) 00 (10)A> 022 206+V(2)
    7                   43                    1  011+V(1) 00 102 (10)A> 206+V(2)
    8                   45                    3  011+V(1) 00 103 (12)C> 205+V(2)
    9                   47                    5  011+V(1) 00 103 12 (02)C> 204+V(2)
   10            55+2*V(2)            13+2*V(2)  011+V(1) 00 103 12 024+V(2) (02)C>
   11            60+2*V(2)            10+2*V(2)  011+V(1) 00 103 12 024+V(2) <C(20)
   12            74+2*V(2)             8+2*V(2)  011+V(1) 00 103 12 023+V(2) <B(02) 02
<< Success! ==> defined new CTR 13 (PPA)
66097073      272766848955373             21321559  012 00 103 12 0210660802 <B(02) 02
== Executing  PA-CTR  8, V(1)=10660799, V(2)=0, repcount=5330400, factor=3/2
92749073      613724946804973                  -41  012 00 103 12 022 <B(02) 0215991201
== Executing PPA-CTR  9 (once), V(1)=2, V(2)=15991200
92749093      613725234646739             31982365  012 2015991210 21 <C(20) 20
== Executing  PA-CTR  3, V(1)=15991207, V(2)=0, repcount=7995604, factor=3/2
148718321     1380881626439027                  -51  012 202 21 <C(20) 2023986813
== Executing PPA-CTR  6 (once), V(1)=1, V(2)=23986812
148718338     1380882058201777             47973577  10 12 0223986818 <B(02) 02
== Executing  PA-CTR  1, V(1)=23986815, V(2)=0, repcount=11993408, factor=3/2
208685378     3106984371497137                  -55  10 12 022 <B(02) 0235980225
== Executing PPA-CTR  5 (once), V(1)=0, V(2)=35980224
208685394     3106985019141301             71960399  012 2035980230 21 <C(20) 20
== Executing  PA-CTR  3, V(1)=35980227, V(2)=0, repcount=17990114, factor=3/2
334616192     6990715871699989                  -57  012 202 21 <C(20) 2053970343
== Executing PPA-CTR  6 (once), V(1)=1, V(2)=53970342
334616209     6990716843166279            107940631  10 12 0253970348 <B(02) 02
== Executing  PA-CTR  1, V(1)=53970345, V(2)=0, repcount=26985173, factor=3/2
469542074    15729112232889579                  -61  10 12 022 <B(02) 0280955520
== Executing PPA-CTR  5 (once), V(1)=0, V(2)=80955519
469542090    15729113690089053            161910983  012 2080955525 21 <C(20) 20
== Executing  PA-CTR  3, V(1)=80955522, V(2)=0, repcount=40477762, factor=3/2
752886424    35390505259899069                  -65  012 20 21 <C(20) 20121433287
== Executing PPA-CTR  4 (once), V(1)=121433282
752886436    35390505502765707            242866507  103 12 02121433285 <B(02) 02
== Executing  PA-CTR  1, V(1)=121433282, V(2)=0, repcount=60716642, factor=3/2
1056469646    79628634349039083                  -61  103 12 02 <B(02) 02182149927
== Executing PPA-CTR 12 (once), V(1)=1, V(2)=182149922
1056469660    79628634713338999            364299793  102 014 20182149925 21 <C(20) 20
== Executing  PA-CTR 10, V(1)=182149922, V(2)=0, repcount=91074962, factor=3/2
1693994394    1791644[4]8755415                  -55  102 014 20 21 <C(20) 20273224887
1693994395    1791644[4]8755417                  -57  102 014 20 <B(10) 20273224888
1693994396    1791644[4]8755421                  -59  102 014 <A(20) 10 20273224888
1693994397    1791644[4]8755426                  -56  102 013 10 (12)C> 10 20273224888
1693994398    1791644[4]8755437                  -59  102 013 10 <B(02) 02 20273224888
1693994399    1791644[4]8755439                  -61  102 013 <B(02) 022 20273224888
1693994400    1791644[4]8755446                  -58  102 012 00 (10)A> 022 20273224888
1693994401    1791644[4]8755458                  -54  102 012 00 102 (10)A> 20273224888
1693994402    1791644[4]8755460                  -52  102 012 00 103 (12)C> 20273224887
1693994403    1791644[4]8755462                  -50  102 012 00 103 12 (02)C> 20273224886
1693994404    1791644[4]5205234            546449722  102 012 00 103 12 02273224886 (02)C>
1693994405    1791644[4]5205239            546449719  102 012 00 103 12 02273224886 <C(20)
1693994406    1791644[4]5205253            546449717  102 012 00 103 12 02273224885 <B(02) 02
1693994407    1791644[4]5205255            546449715  102 012 00 103 12 02273224884 <C(21) 022
1693994408    1791644[4]5205266            546449718  102 012 00 103 12 02273224883 10 (10)A> 022
1693994409    1791644[4]5205278            546449722  102 012 00 103 12 02273224883 103 (10)A>
1693994410    1791644[4]5205283            546449719  102 012 00 103 12 02273224883 103 <B(02) 02
1693994411    1791644[4]5205289            546449713  102 012 00 103 12 02273224883 <B(02) 024
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  [*]* [*]* [*]* [*]* [*]* 023+V(1) <B(02) 021+V(2)
    1                    2                   -2  [*]* [*]* [*]* [*]* [*]* 022+V(1) <C(21) 022+V(2)
    2                   13                    1  [*]* [*]* [*]* [*]* [*]* 021+V(1) 10 (10)A> 022+V(2)
    3            25+6*V(2)             5+2*V(2)  [*]* [*]* [*]* [*]* [*]* 021+V(1) 103+V(2) (10)A>
    4            30+6*V(2)             2+2*V(2)  [*]* [*]* [*]* [*]* [*]* 021+V(1) 103+V(2) <B(02) 02
    5            36+8*V(2)                   -4  [*]* [*]* [*]* [*]* [*]* 021+V(1) <B(02) 024+V(2)
<< Success! ==> defined new CTR 14 (PA)
1693994411    1791644[4]5205289            546449713  102 012 00 103 12 02273224883 <B(02) 024
== Executing  PA-CTR 14, V(1)=273224880, V(2)=3, repcount=136612441, factor=3/2
2377056616    4031199[4]4344229                  -51  102 012 00 103 12 02 <B(02) 02409837327
2377056617    4031199[4]4344231                  -53  102 012 00 103 12 <C(21) 02409837328
2377056618    4031199[4]4344235                  -55  102 012 00 103 <A(12) 01 02409837328
2377056619    4031199[4]4344238                  -52  102 012 00 102 11 (01)D> 01 02409837328
2377056620    4031199[4]4344246                  -50  102 012 00 102 11 01 (01)B> 02409837328
2377056621    4031199[4]4344249                  -53  102 012 00 102 11 01 <C(20) 22 02409837327
2377056622    4031199[4]4344251                  -55  102 012 00 102 11 <C(20) 20 22 02409837327
2377056623    4031199[4]4344260                  -52  102 012 00 102 01 (01)B> 20 22 02409837327
2377056624    4031199[4]4344266                  -50  102 012 00 102 012 (01)B> 22 02409837327
2377056625    4031199[4]4344272                  -48  102 012 00 102 013 (01)D> 02409837327
2377056626    4031199[4]4344274                  -46  102 012 00 102 014 (20)D> 02409837326
2377056627    4031199[4]4018926            819674606  102 012 00 102 014 20409837326 (20)D>
2377056628    4031199[4]4018935            819674603  102 012 00 102 014 20409837326 <A(20)
2377056629    4031199[4]4018942            819674606  102 012 00 102 014 20409837325 21 (01)B>
2377056630    4031199[4]4018945            819674603  102 012 00 102 014 20409837325 21 <C(20) 20
2377056631    4031199[4]4018947            819674601  102 012 00 102 014 20409837325 <B(10) 202
2377056632    4031199[4]4018951            819674599  102 012 00 102 014 20409837324 <A(20) 10 202
2377056633    4031199[4]4018958            819674602  102 012 00 102 014 20409837323 21 (01)B> 10 202
2377056634    4031199[4]4018960            819674604  102 012 00 102 014 20409837323 21 01 (01)B> 202
2377056635    4031199[4]4018972            819674608  102 012 00 102 014 20409837323 21 013 (01)B>
2377056636    4031199[4]4018975            819674605  102 012 00 102 014 20409837323 21 013 <C(20) 20
2377056637    4031199[4]4018981            819674599  102 012 00 102 014 20409837323 21 <C(20) 204
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  [*]* [*]* [*]* [*]* [*]* 203+V(1) 21 <C(20) 201+V(2)
    1                    2                   -2  [*]* [*]* [*]* [*]* [*]* 203+V(1) <B(10) 202+V(2)
    2                    6                   -4  [*]* [*]* [*]* [*]* [*]* 202+V(1) <A(20) 10 202+V(2)
    3                   13                   -1  [*]* [*]* [*]* [*]* [*]* 201+V(1) 21 (01)B> 10 202+V(2)
    4                   15                    1  [*]* [*]* [*]* [*]* [*]* 201+V(1) 21 01 (01)B> 202+V(2)
    5            27+6*V(2)             5+2*V(2)  [*]* [*]* [*]* [*]* [*]* 201+V(1) 21 013+V(2) (01)B>
    6            30+6*V(2)             2+2*V(2)  [*]* [*]* [*]* [*]* [*]* 201+V(1) 21 013+V(2) <C(20) 20
    7            36+8*V(2)                   -4  [*]* [*]* [*]* [*]* [*]* 201+V(1) 21 <C(20) 204+V(2)
<< Success! ==> defined new CTR 15 (PA)
2377056637    4031199[4]4018981            819674599  102 012 00 102 014 20409837323 21 <C(20) 204
== Executing  PA-CTR 15, V(1)=409837320, V(2)=3, repcount=204918661, factor=3/2
3811487264    9070198[4]2509761                  -45  102 012 00 102 014 20 21 <C(20) 20614755987
3811487265    9070198[4]2509763                  -47  102 012 00 102 014 20 <B(10) 20614755988
3811487266    9070198[4]2509767                  -49  102 012 00 102 014 <A(20) 10 20614755988
3811487267    9070198[4]2509772                  -46  102 012 00 102 013 10 (12)C> 10 20614755988
3811487268    9070198[4]2509783                  -49  102 012 00 102 013 10 <B(02) 02 20614755988
3811487269    9070198[4]2509785                  -51  102 012 00 102 013 <B(02) 022 20614755988
3811487270    9070198[4]2509792                  -48  102 012 00 102 012 00 (10)A> 022 20614755988
3811487271    9070198[4]2509804                  -44  102 012 00 102 012 00 102 (10)A> 20614755988
3811487272    9070198[4]2509806                  -42  102 012 00 102 012 00 103 (12)C> 20614755987
3811487273    9070198[4]2509808                  -40  102 012 00 102 012 00 103 12 (02)C> 20614755986
3811487274    9070198[4]2021780           1229511932  102 012 00 102 012 00 103 12 02614755986 (02)C>
3811487275    9070198[4]2021785           1229511929  102 012 00 102 012 00 103 12 02614755986 <C(20)
3811487276    9070198[4]2021799           1229511927  102 012 00 102 012 00 103 12 02614755985 <B(02) 02
3811487277    9070198[4]2021801           1229511925  102 012 00 102 012 00 103 12 02614755984 <C(21) 022
3811487278    9070198[4]2021812           1229511928  102 012 00 102 012 00 103 12 02614755983 10 (10)A> 022
3811487279    9070198[4]2021824           1229511932  102 012 00 102 012 00 103 12 02614755983 103 (10)A>
3811487280    9070198[4]2021829           1229511929  102 012 00 102 012 00 103 12 02614755983 103 <B(02) 02
3811487281    9070198[4]2021835           1229511923  102 012 00 102 012 00 103 12 02614755983 <B(02) 024
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 023+V(1) <B(02) 021+V(2)
    1                    2                   -2  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 022+V(1) <C(21) 022+V(2)
    2                   13                    1  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 021+V(1) 10 (10)A> 022+V(2)
    3            25+6*V(2)             5+2*V(2)  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 021+V(1) 103+V(2) (10)A>
    4            30+6*V(2)             2+2*V(2)  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 021+V(1) 103+V(2) <B(02) 02
    5            36+8*V(2)                   -4  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 021+V(1) <B(02) 024+V(2)
<< Success! ==> defined new CTR 16 (PA)
3811487281    9070198[4]2021835           1229511923  102 012 00 102 012 00 103 12 02614755983 <B(02) 024
== Executing  PA-CTR 16, V(1)=614755980, V(2)=3, repcount=307377991, factor=3/2
5348377236    2040794[5]0518375                  -41  102 012 00 102 012 00 103 12 02 <B(02) 02922133977
5348377237    2040794[5]0518377                  -43  102 012 00 102 012 00 103 12 <C(21) 02922133978
5348377238    2040794[5]0518381                  -45  102 012 00 102 012 00 103 <A(12) 01 02922133978
5348377239    2040794[5]0518384                  -42  102 012 00 102 012 00 102 11 (01)D> 01 02922133978
5348377240    2040794[5]0518392                  -40  102 012 00 102 012 00 102 11 01 (01)B> 02922133978
5348377241    2040794[5]0518395                  -43  102 012 00 102 012 00 102 11 01 <C(20) 22 02922133977
5348377242    2040794[5]0518397                  -45  102 012 00 102 012 00 102 11 <C(20) 20 22 02922133977
5348377243    2040794[5]0518406                  -42  102 012 00 102 012 00 102 01 (01)B> 20 22 02922133977
5348377244    2040794[5]0518412                  -40  102 012 00 102 012 00 102 012 (01)B> 22 02922133977
5348377245    2040794[5]0518418                  -38  102 012 00 102 012 00 102 013 (01)D> 02922133977
5348377246    2040794[5]0518420                  -36  102 012 00 102 012 00 102 014 (20)D> 02922133976
5348377247    2040794[5]4786372           1844267916  102 012 00 102 012 00 102 014 20922133976 (20)D>
5348377248    2040794[5]4786381           1844267913  102 012 00 102 012 00 102 014 20922133976 <A(20)
5348377249    2040794[5]4786388           1844267916  102 012 00 102 012 00 102 014 20922133975 21 (01)B>
5348377250    2040794[5]4786391           1844267913  102 012 00 102 012 00 102 014 20922133975 21 <C(20) 20
5348377251    2040794[5]4786393           1844267911  102 012 00 102 012 00 102 014 20922133975 <B(10) 202
5348377252    2040794[5]4786397           1844267909  102 012 00 102 012 00 102 014 20922133974 <A(20) 10 202
5348377253    2040794[5]4786404           1844267912  102 012 00 102 012 00 102 014 20922133973 21 (01)B> 10 202
5348377254    2040794[5]4786406           1844267914  102 012 00 102 012 00 102 014 20922133973 21 01 (01)B> 202
5348377255    2040794[5]4786418           1844267918  102 012 00 102 012 00 102 014 20922133973 21 013 (01)B>
5348377256    2040794[5]4786421           1844267915  102 012 00 102 012 00 102 014 20922133973 21 013 <C(20) 20
5348377257    2040794[5]4786427           1844267909  102 012 00 102 012 00 102 014 20922133973 21 <C(20) 204
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 203+V(1) 21 <C(20) 201+V(2)
    1                    2                   -2  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 203+V(1) <B(10) 202+V(2)
    2                    6                   -4  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 202+V(1) <A(20) 10 202+V(2)
    3                   13                   -1  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 201+V(1) 21 (01)B> 10 202+V(2)
    4                   15                    1  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 201+V(1) 21 01 (01)B> 202+V(2)
    5            27+6*V(2)             5+2*V(2)  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 201+V(1) 21 013+V(2) (01)B>
    6            30+6*V(2)             2+2*V(2)  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 201+V(1) 21 013+V(2) <C(20) 20
    7            36+8*V(2)                   -4  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 201+V(1) 21 <C(20) 204+V(2)
<< Success! ==> defined new CTR 17 (PA)
5348377257    2040794[5]4786427           1844267909  102 012 00 102 012 00 102 014 20922133973 21 <C(20) 204
== Executing  PA-CTR 17, V(1)=922133970, V(2)=3, repcount=461066986, factor=3/2
8575846159    4591787[5]5492107                  -35  102 012 00 102 012 00 102 014 20 21 <C(20) 201383200962
8575846160    4591787[5]5492109                  -37  102 012 00 102 012 00 102 014 20 <B(10) 201383200963
8575846161    4591787[5]5492113                  -39  102 012 00 102 012 00 102 014 <A(20) 10 201383200963
8575846162    4591787[5]5492118                  -36  102 012 00 102 012 00 102 013 10 (12)C> 10 201383200963
8575846163    4591787[5]5492129                  -39  102 012 00 102 012 00 102 013 10 <B(02) 02 201383200963
8575846164    4591787[5]5492131                  -41  102 012 00 102 012 00 102 013 <B(02) 022 201383200963
8575846165    4591787[5]5492138                  -38  102 012 00 102 012 00 102 012 00 (10)A> 022 201383200963
8575846166    4591787[5]5492150                  -34  102 012 00 102 012 00 102 012 00 102 (10)A> 201383200963
8575846167    4591787[5]5492152                  -32  102 012 00 102 012 00 102 012 00 103 (12)C> 201383200962
8575846168    4591787[5]5492154                  -30  102 012 00 102 012 00 102 012 00 103 12 (02)C> 201383200961
8575846169    4591787[5]1894076           2766401892  102 012 00 102 012 00 102 012 00 103 12 021383200961 (02)C>
8575846170    4591787[5]1894081           2766401889  102 012 00 102 012 00 102 012 00 103 12 021383200961 <C(20)
8575846171    4591787[5]1894095           2766401887  102 012 00 102 012 00 102 012 00 103 12 021383200960 <B(02) 02
8575846172    4591787[5]1894097           2766401885  102 012 00 102 012 00 102 012 00 103 12 021383200959 <C(21) 022
8575846173    4591787[5]1894108           2766401888  102 012 00 102 012 00 102 012 00 103 12 021383200958 10 (10)A> 022
8575846174    4591787[5]1894120           2766401892  102 012 00 102 012 00 102 012 00 103 12 021383200958 103 (10)A>
8575846175    4591787[5]1894125           2766401889  102 012 00 102 012 00 102 012 00 103 12 021383200958 103 <B(02) 02
8575846176    4591787[5]1894131           2766401883  102 012 00 102 012 00 102 012 00 103 12 021383200958 <B(02) 024
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 023+V(1) <B(02) 021+V(2)
    1                    2                   -2  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 022+V(1) <C(21) 022+V(2)
    2                   13                    1  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 021+V(1) 10 (10)A> 022+V(2)
    3            25+6*V(2)             5+2*V(2)  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 021+V(1) 103+V(2) (10)A>
    4            30+6*V(2)             2+2*V(2)  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 021+V(1) 103+V(2) <B(02) 02
    5            36+8*V(2)                   -4  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 021+V(1) <B(02) 024+V(2)
<< Success! ==> defined new CTR 18 (PA)
8575846176    4591787[5]1894131           2766401883  102 012 00 102 012 00 102 012 00 103 12 021383200958 <B(02) 024
== Executing  PA-CTR 18, V(1)=1383200955, V(2)=3, repcount=691600478, factor=3/2
12033848566    1033152[6]6658883                  -29  102 012 00 102 012 00 102 012 00 103 12 022 <B(02) 022074801438
12033848567    1033152[6]6658885                  -31  102 012 00 102 012 00 102 012 00 103 12 02 <C(21) 022074801439
12033848568    1033152[6]6658896                  -28  102 012 00 102 012 00 102 012 00 103 12 10 (10)A> 022074801439
12033848569    1033152[6]5467530           4149602850  102 012 00 102 012 00 102 012 00 103 12 102074801440 (10)A>
12033848570    1033152[6]5467535           4149602847  102 012 00 102 012 00 102 012 00 103 12 102074801440 <B(02) 02
12033848571    1033152[6]5070415                  -33  102 012 00 102 012 00 102 012 00 103 12 <B(02) 022074801441
12033848572    1033152[6]5070426                  -30  102 012 00 102 012 00 102 012 00 104 (10)A> 022074801441
12033848573    1033152[6]3879072           4149602852  102 012 00 102 012 00 102 012 00 102074801445 (10)A>
12033848574    1033152[6]3879077           4149602849  102 012 00 102 012 00 102 012 00 102074801445 <B(02) 02
12033848575    1033152[6]3481967                  -41  102 012 00 102 012 00 102 012 00 <B(02) 022074801446
12033848576    1033152[6]3481969                  -43  102 012 00 102 012 00 102 012 <A(22) 022074801447
12033848577    1033152[6]3481977                  -45  102 012 00 102 012 00 102 01 <B(02) 00 022074801447
12033848578    1033152[6]3481984                  -42  102 012 00 102 012 00 102 00 (10)A> 00 022074801447
12033848579    1033152[6]3481989                  -45  102 012 00 102 012 00 102 00 <B(02) 022074801448
12033848580    1033152[6]3481991                  -47  102 012 00 102 012 00 102 <A(22) 022074801449
12033848581    1033152[6]3481998                  -44  102 012 00 102 012 00 10 11 (01)D> 022074801449
12033848582    1033152[6]3482000                  -42  102 012 00 102 012 00 10 11 01 (20)D> 022074801448
12033848583    1033152[6]3084896           4149602854  102 012 00 102 012 00 10 11 01 202074801448 (20)D>
12033848584    1033152[6]3084905           4149602851  102 012 00 102 012 00 10 11 01 202074801448 <A(20)
12033848585    1033152[6]3084912           4149602854  102 012 00 102 012 00 10 11 01 202074801447 21 (01)B>
12033848586    1033152[6]3084915           4149602851  102 012 00 102 012 00 10 11 01 202074801447 21 <C(20) 20
12033848587    1033152[6]3084917           4149602849  102 012 00 102 012 00 10 11 01 202074801447 <B(10) 202
12033848588    1033152[6]3084921           4149602847  102 012 00 102 012 00 10 11 01 202074801446 <A(20) 10 202
12033848589    1033152[6]3084928           4149602850  102 012 00 102 012 00 10 11 01 202074801445 21 (01)B> 10 202
12033848590    1033152[6]3084930           4149602852  102 012 00 102 012 00 10 11 01 202074801445 21 01 (01)B> 202
12033848591    1033152[6]3084942           4149602856  102 012 00 102 012 00 10 11 01 202074801445 21 013 (01)B>
12033848592    1033152[6]3084945           4149602853  102 012 00 102 012 00 10 11 01 202074801445 21 013 <C(20) 20
12033848593    1033152[6]3084951           4149602847  102 012 00 102 012 00 10 11 01 202074801445 21 <C(20) 204
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 203+V(1) 21 <C(20) 201+V(2)
    1                    2                   -2  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 203+V(1) <B(10) 202+V(2)
    2                    6                   -4  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 202+V(1) <A(20) 10 202+V(2)
    3                   13                   -1  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 201+V(1) 21 (01)B> 10 202+V(2)
    4                   15                    1  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 201+V(1) 21 01 (01)B> 202+V(2)
    5            27+6*V(2)             5+2*V(2)  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 201+V(1) 21 013+V(2) (01)B>
    6            30+6*V(2)             2+2*V(2)  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 201+V(1) 21 013+V(2) <C(20) 20
    7            36+8*V(2)                   -4  [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* [*]* 201+V(1) 21 <C(20) 204+V(2)
<< Success! ==> defined new CTR 19 (PA)
12033848593    1033152[6]3084951           4149602847  102 012 00 102 012 00 10 11 01 202074801445 21 <C(20) 204
== Executing  PA-CTR 19, V(1)=2074801442, V(2)=3, repcount=1037400722, factor=3/2
19295653647    2324592[6]1775015                  -41  102 012 00 102 012 00 10 11 01 20 21 <C(20) 203112202170
19295653648    2324592[6]1775017                  -43  102 012 00 102 012 00 10 11 01 20 <B(10) 203112202171
19295653649    2324592[6]1775021                  -45  102 012 00 102 012 00 10 11 01 <A(20) 10 203112202171
19295653650    2324592[6]1775026                  -42  102 012 00 102 012 00 10 11 10 (12)C> 10 203112202171
19295653651    2324592[6]1775037                  -45  102 012 00 102 012 00 10 11 10 <B(02) 02 203112202171
19295653652    2324592[6]1775039                  -47  102 012 00 102 012 00 10 11 <B(02) 022 203112202171
19295653653    2324592[6]1775046                  -44  102 012 00 102 012 00 102 (10)A> 022 203112202171
19295653654    2324592[6]1775058                  -40  102 012 00 102 012 00 104 (10)A> 203112202171
19295653655    2324592[6]1775060                  -38  102 012 00 102 012 00 105 (12)C> 203112202170
19295653656    2324592[6]1775062                  -36  102 012 00 102 012 00 105 12 (02)C> 203112202169
19295653657    2324592[6]6179400           6224404302  102 012 00 102 012 00 105 12 023112202169 (02)C>
19295653658    2324592[6]6179405           6224404299  102 012 00 102 012 00 105 12 023112202169 <C(20)
19295653659    2324592[6]6179419           6224404297  102 012 00 102 012 00 105 12 023112202168 <B(02) 02
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  [*]* [*]* [*]* [*]* [*]* [*]* 101+V(1) 11 01 20 21 <C(20) 205+V(2)
    1                    2                   -2  [*]* [*]* [*]* [*]* [*]* [*]* 101+V(1) 11 01 20 <B(10) 206+V(2)
    2                    6                   -4  [*]* [*]* [*]* [*]* [*]* [*]* 101+V(1) 11 01 <A(20) 10 206+V(2)
    3                   11                   -1  [*]* [*]* [*]* [*]* [*]* [*]* 101+V(1) 11 10 (12)C> 10 206+V(2)
    4                   22                   -4  [*]* [*]* [*]* [*]* [*]* [*]* 101+V(1) 11 10 <B(02) 02 206+V(2)
    5                   24                   -6  [*]* [*]* [*]* [*]* [*]* [*]* 101+V(1) 11 <B(02) 022 206+V(2)
    6                   31                   -3  [*]* [*]* [*]* [*]* [*]* [*]* 102+V(1) (10)A> 022 206+V(2)
    7                   43                    1  [*]* [*]* [*]* [*]* [*]* [*]* 104+V(1) (10)A> 206+V(2)
    8                   45                    3  [*]* [*]* [*]* [*]* [*]* [*]* 105+V(1) (12)C> 205+V(2)
    9                   47                    5  [*]* [*]* [*]* [*]* [*]* [*]* 105+V(1) 12 (02)C> 204+V(2)
   10            55+2*V(2)            13+2*V(2)  [*]* [*]* [*]* [*]* [*]* [*]* 105+V(1) 12 024+V(2) (02)C>
   11            60+2*V(2)            10+2*V(2)  [*]* [*]* [*]* [*]* [*]* [*]* 105+V(1) 12 024+V(2) <C(20)
   12            74+2*V(2)             8+2*V(2)  [*]* [*]* [*]* [*]* [*]* [*]* 105+V(1) 12 023+V(2) <B(02) 02
<< Success! ==> defined new CTR 20 (PPA)
19295653659    2324592[6]6179419           6224404297  102 012 00 102 012 00 105 12 023112202168 <B(02) 02
== Executing  PA-CTR 16, V(1)=3112202165, V(2)=0, repcount=1556101083, factor=3/2
27076159074    5230333[6]7880079                  -35  102 012 00 102 012 00 105 12 022 <B(02) 024668303250
27076159075    5230333[6]7880081                  -37  102 012 00 102 012 00 105 12 02 <C(21) 024668303251
27076159076    5230333[6]7880092                  -34  102 012 00 102 012 00 105 12 10 (10)A> 024668303251
27076159077    5230333[6]7699598           9336606468  102 012 00 102 012 00 105 12 104668303252 (10)A>
27076159078    5230333[6]7699603           9336606465  102 012 00 102 012 00 105 12 104668303252 <B(02) 02
27076159079    5230333[6]4306107                  -39  102 012 00 102 012 00 105 12 <B(02) 024668303253
27076159080    5230333[6]4306118                  -36  102 012 00 102 012 00 106 (10)A> 024668303253
27076159081    5230333[6]4125636           9336606470  102 012 00 102 012 00 104668303259 (10)A>
27076159082    5230333[6]4125641           9336606467  102 012 00 102 012 00 104668303259 <B(02) 02
27076159083    5230333[6]0732159                  -51  102 012 00 102 012 00 <B(02) 024668303260
27076159084    5230333[6]0732161                  -53  102 012 00 102 012 <A(22) 024668303261
27076159085    5230333[6]0732169                  -55  102 012 00 102 01 <B(02) 00 024668303261
27076159086    5230333[6]0732176                  -52  102 012 00 102 00 (10)A> 00 024668303261
27076159087    5230333[6]0732181                  -55  102 012 00 102 00 <B(02) 024668303262
27076159088    5230333[6]0732183                  -57  102 012 00 102 <A(22) 024668303263
27076159089    5230333[6]0732190                  -54  102 012 00 10 11 (01)D> 024668303263
27076159090    5230333[6]0732192                  -52  102 012 00 10 11 01 (20)D> 024668303262
27076159091    5230333[6]7338716           9336606472  102 012 00 10 11 01 204668303262 (20)D>
27076159092    5230333[6]7338725           9336606469  102 012 00 10 11 01 204668303262 <A(20)
27076159093    5230333[6]7338732           9336606472  102 012 00 10 11 01 204668303261 21 (01)B>
27076159094    5230333[6]7338735           9336606469  102 012 00 10 11 01 204668303261 21 <C(20) 20
27076159095    5230333[6]7338737           9336606467  102 012 00 10 11 01 204668303261 <B(10) 202
27076159096    5230333[6]7338741           9336606465  102 012 00 10 11 01 204668303260 <A(20) 10 202

Lines:       500
Top steps:   499
Macro steps: 27076159096
Basic steps: 52303332785147338741
Tape index:  9336606465
nonzeros:    4668303272
log10(nonzeros):    9.669
log10(steps   ):   19.719

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 2-bck-macro machine.

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

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