TM #7 from MaBu90-Paper

Comment: This TM produces 136612 ones in 13122572797 steps.

State on
0
on
1
on 0 on 1
Print Move Goto Print Move Goto
A B1L A1L 1 left B 1 left A
B C1R B1R 1 right C 1 right B
C F0R D1R 0 right F 1 right D
D A1L E0R 1 left A 0 right E
E A0L C1R 0 left A 1 right C
F E1L H1L 1 left E 1 left H
Transition table
The same TM just simple.
The same TM with repetitions reduced.
The same TM with tape symbol exponents.
The same TM as 3-macro machine.
Simulation is done as 3-macro machine with pure additive config-TRs.

Pushing initial machine.
Pushing macro factor 3.

Steps             BasSteps              BasTpos  Tape contents
    0                    0                    0  A>
    1                    1                   -1  <B 100
    2                    2                    0  001 C> 100
    3                    5                   -1  001 <A 110
    4                   10                    0  110 E> 110
    5                   15                   -1  110 <A 111
    6                   18                    0  111 B> 111
    7                   21                    3  1112 B>
    8                   26                    2  1112 <A 101
    9                   32                   -4  <A 1112 101
   10                   35                   -3  011 D> 1112 101
   11                   41                    3  0113 D> 101
   12                   44                    2  0113 <B 101
   13                   45                    3  0113 B> 101
   14                   48                    6  0113 111 D>
   15                   49                    5  0113 111 <A 100
   16                   52                    2  0113 <A 111 100
   17                   55                   -1  0112 <B 1112 100
   18                   56                    0  0112 B> 1112 100
   19                   62                    6  0112 1112 B> 100
   20                   65                    9  0112 1112 110 F>
   21                   66                    8  0112 1112 110 <E 100
   22                   69                    5  0112 1112 <A 110 100
   23                   75                   -1  0112 <A 1112 110 100
   24                   78                   -4  011 <B 1113 110 100
   25                   79                   -3  011 B> 1113 110 100
   26                   88                    6  011 1113 B> 110 100
   27                   91                    9  011 1114 C> 100
   28                   94                    8  011 1114 <A 110
   29                  106                   -4  011 <A 1114 110
   30                  109                   -7  <B 1115 110
   31                  110                   -6  001 C> 1115 110
   32                  125                    9  001 1015 C> 110
   33                  132                   12  001 1015 111 C>
   34                  135                   11  001 1015 111 <A 010
   35                  138                    8  001 1015 <A 111 010
   36                  143                    9  001 1014 111 B> 111 010
   37                  146                   12  001 1014 1112 B> 010
   38                  151                   11  001 1014 1112 <A 111
   39                  157                    5  001 1014 <A 1113
   40                  162                    6  001 1013 111 B> 1113
   41                  171                   15  001 1013 1114 B>
   42                  176                   14  001 1013 1114 <A 101
   43                  188                    2  001 1013 <A 1114 101
   44                  193                    3  001 1012 111 B> 1114 101
   45                  205                   15  001 1012 1115 B> 101
   46                  208                   18  001 1012 1116 D>
   47                  209                   17  001 1012 1116 <A 100
   48                  227                   -1  001 1012 <A 1116 100
   49                  232                    0  001 101 111 B> 1116 100
   50                  250                   18  001 101 1117 B> 100
   51                  253                   21  001 101 1117 110 F>
   52                  254                   20  001 101 1117 110 <E 100
   53                  257                   17  001 101 1117 <A 110 100
   54                  278                   -4  001 101 <A 1117 110 100
   55                  283                   -3  001 111 B> 1117 110 100
   56                  304                   18  001 1118 B> 110 100
   57                  307                   21  001 1119 C> 100
   58                  310                   20  001 1119 <A 110
   59                  337                   -7  001 <A 1119 110
   60                  342                   -6  110 E> 1119 110
   61                  369                   21  11010 E> 110
   62                  374                   20  11010 <A 111
   63                  377                   21  1109 111 B> 111
   64                  380                   24  1109 1112 B>
   65                  385                   23  1109 1112 <A 101
   66                  391                   17  1109 <A 1112 101
   67                  394                   18  1108 111 B> 1112 101
   68                  400                   24  1108 1113 B> 101
   69                  403                   27  1108 1114 D>
   70                  404                   26  1108 1114 <A 100
   71                  416                   14  1108 <A 1114 100
   72                  419                   15  1107 111 B> 1114 100
   73                  431                   27  1107 1115 B> 100
   74                  434                   30  1107 1115 110 F>
   75                  435                   29  1107 1115 110 <E 100
   76                  438                   26  1107 1115 <A 110 100
   77                  453                   11  1107 <A 1115 110 100
   78                  456                   12  1106 111 B> 1115 110 100
   79                  471                   27  1106 1116 B> 110 100
   80                  474                   30  1106 1117 C> 100
   81                  477                   29  1106 1117 <A 110
   82                  498                    8  1106 <A 1117 110
   83                  501                    9  1105 111 B> 1117 110
   84                  522                   30  1105 1118 B> 110
   85                  525                   33  1105 1119 C>
   86                  528                   32  1105 1119 <A 010
   87                  555                    5  1105 <A 1119 010
   88                  558                    6  1104 111 B> 1119 010
   89                  585                   33  1104 11110 B> 010
   90                  590                   32  1104 11110 <A 111
   91                  620                    2  1104 <A 11111
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  1107+V(1) <A 1111+V(2)
    1                    3                    1  1106+V(1) 111 B> 1111+V(2)
    2             6+3*V(2)             4+3*V(2)  1106+V(1) 1112+V(2) B>
    3            11+3*V(2)             3+3*V(2)  1106+V(1) 1112+V(2) <A 101
    4            17+6*V(2)                   -3  1106+V(1) <A 1112+V(2) 101
    5            20+6*V(2)                   -2  1105+V(1) 111 B> 1112+V(2) 101
    6            26+9*V(2)             4+3*V(2)  1105+V(1) 1113+V(2) B> 101
    7            29+9*V(2)             7+3*V(2)  1105+V(1) 1114+V(2) D>
    8            30+9*V(2)             6+3*V(2)  1105+V(1) 1114+V(2) <A 100
    9           42+12*V(2)                   -6  1105+V(1) <A 1114+V(2) 100
   10           45+12*V(2)                   -5  1104+V(1) 111 B> 1114+V(2) 100
   11           57+15*V(2)             7+3*V(2)  1104+V(1) 1115+V(2) B> 100
   12           60+15*V(2)            10+3*V(2)  1104+V(1) 1115+V(2) 110 F>
   13           61+15*V(2)             9+3*V(2)  1104+V(1) 1115+V(2) 110 <E 100
   14           64+15*V(2)             6+3*V(2)  1104+V(1) 1115+V(2) <A 110 100
   15           79+18*V(2)                   -9  1104+V(1) <A 1115+V(2) 110 100
   16           82+18*V(2)                   -8  1103+V(1) 111 B> 1115+V(2) 110 100
   17           97+21*V(2)             7+3*V(2)  1103+V(1) 1116+V(2) B> 110 100
   18          100+21*V(2)            10+3*V(2)  1103+V(1) 1117+V(2) C> 100
   19          103+21*V(2)             9+3*V(2)  1103+V(1) 1117+V(2) <A 110
   20          124+24*V(2)                  -12  1103+V(1) <A 1117+V(2) 110
   21          127+24*V(2)                  -11  1102+V(1) 111 B> 1117+V(2) 110
   22          148+27*V(2)            10+3*V(2)  1102+V(1) 1118+V(2) B> 110
   23          151+27*V(2)            13+3*V(2)  1102+V(1) 1119+V(2) C>
   24          154+27*V(2)            12+3*V(2)  1102+V(1) 1119+V(2) <A 010
   25          181+30*V(2)                  -15  1102+V(1) <A 1119+V(2) 010
   26          184+30*V(2)                  -14  1101+V(1) 111 B> 1119+V(2) 010
   27          211+33*V(2)            13+3*V(2)  1101+V(1) 11110+V(2) B> 010
   28          216+33*V(2)            12+3*V(2)  1101+V(1) 11110+V(2) <A 111
   29          246+36*V(2)                  -18  1101+V(1) <A 11111+V(2)
<< Success! ==> defined new CTR 1 (PA)
   92                  623                    3  1103 111 B> 11111
   93                  656                   36  1103 11112 B>
   94                  661                   35  1103 11112 <A 101
   95                  697                   -1  1103 <A 11112 101
   96                  700                    0  1102 111 B> 11112 101
   97                  736                   36  1102 11113 B> 101
   98                  739                   39  1102 11114 D>
   99                  740                   38  1102 11114 <A 100
  100                  782                   -4  1102 <A 11114 100
  101                  785                   -3  110 111 B> 11114 100
  102                  827                   39  110 11115 B> 100
  103                  830                   42  110 11115 110 F>
  104                  831                   41  110 11115 110 <E 100
  105                  834                   38  110 11115 <A 110 100
  106                  879                   -7  110 <A 11115 110 100
  107                  882                   -6  111 B> 11115 110 100
  108                  927                   39  11116 B> 110 100
  109                  930                   42  11117 C> 100
  110                  933                   41  11117 <A 110
  111                  984                  -10  <A 11117 110
  112                  987                   -9  011 D> 11117 110
  113                 1038                   42  01118 D> 110
  114                 1041                   45  01118 010 F>
  115                 1042                   44  01118 010 <E 100
  116                 1045                   41  01118 <B 110 100
  117                 1046                   42  01118 B> 110 100
  118                 1049                   45  01118 111 C> 100
  119                 1052                   44  01118 111 <A 110
  120                 1055                   41  01118 <A 111 110
  121                 1058                   38  01117 <B 1112 110
  122                 1059                   39  01117 B> 1112 110
  123                 1065                   45  01117 1112 B> 110
  124                 1068                   48  01117 1113 C>
  125                 1071                   47  01117 1113 <A 010
  126                 1080                   38  01117 <A 1113 010
  127                 1083                   35  01116 <B 1114 010
  128                 1084                   36  01116 B> 1114 010
  129                 1096                   48  01116 1114 B> 010
  130                 1101                   47  01116 1114 <A 111
  131                 1113                   35  01116 <A 1115
  132                 1116                   32  01115 <B 1116
  133                 1117                   33  01115 B> 1116
  134                 1135                   51  01115 1116 B>
  135                 1140                   50  01115 1116 <A 101
  136                 1158                   32  01115 <A 1116 101
  137                 1161                   29  01114 <B 1117 101
  138                 1162                   30  01114 B> 1117 101
  139                 1183                   51  01114 1117 B> 101
  140                 1186                   54  01114 1118 D>
  141                 1187                   53  01114 1118 <A 100
  142                 1211                   29  01114 <A 1118 100
  143                 1214                   26  01113 <B 1119 100
  144                 1215                   27  01113 B> 1119 100
  145                 1242                   54  01113 1119 B> 100
  146                 1245                   57  01113 1119 110 F>
  147                 1246                   56  01113 1119 110 <E 100
  148                 1249                   53  01113 1119 <A 110 100
  149                 1276                   26  01113 <A 1119 110 100
  150                 1279                   23  01112 <B 11110 110 100
  151                 1280                   24  01112 B> 11110 110 100
  152                 1310                   54  01112 11110 B> 110 100
  153                 1313                   57  01112 11111 C> 100
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  0117+V(2) 1111+V(1) C> 100
    1                    3                   -1  0117+V(2) 1111+V(1) <A 110
    2             6+3*V(1)           -4+-3*V(1)  0117+V(2) <A 1111+V(1) 110
    3             9+3*V(1)           -7+-3*V(1)  0116+V(2) <B 1112+V(1) 110
    4            10+3*V(1)           -6+-3*V(1)  0116+V(2) B> 1112+V(1) 110
    5            16+6*V(1)                    0  0116+V(2) 1112+V(1) B> 110
    6            19+6*V(1)                    3  0116+V(2) 1113+V(1) C>
    7            22+6*V(1)                    2  0116+V(2) 1113+V(1) <A 010
    8            31+9*V(1)           -7+-3*V(1)  0116+V(2) <A 1113+V(1) 010
    9            34+9*V(1)          -10+-3*V(1)  0115+V(2) <B 1114+V(1) 010
   10            35+9*V(1)           -9+-3*V(1)  0115+V(2) B> 1114+V(1) 010
   11           47+12*V(1)                    3  0115+V(2) 1114+V(1) B> 010
   12           52+12*V(1)                    2  0115+V(2) 1114+V(1) <A 111
   13           64+15*V(1)          -10+-3*V(1)  0115+V(2) <A 1115+V(1)
   14           67+15*V(1)          -13+-3*V(1)  0114+V(2) <B 1116+V(1)
   15           68+15*V(1)          -12+-3*V(1)  0114+V(2) B> 1116+V(1)
   16           86+18*V(1)                    6  0114+V(2) 1116+V(1) B>
   17           91+18*V(1)                    5  0114+V(2) 1116+V(1) <A 101
   18          109+21*V(1)          -13+-3*V(1)  0114+V(2) <A 1116+V(1) 101
   19          112+21*V(1)          -16+-3*V(1)  0113+V(2) <B 1117+V(1) 101
   20          113+21*V(1)          -15+-3*V(1)  0113+V(2) B> 1117+V(1) 101
   21          134+24*V(1)                    6  0113+V(2) 1117+V(1) B> 101
   22          137+24*V(1)                    9  0113+V(2) 1118+V(1) D>
   23          138+24*V(1)                    8  0113+V(2) 1118+V(1) <A 100
   24          162+27*V(1)          -16+-3*V(1)  0113+V(2) <A 1118+V(1) 100
   25          165+27*V(1)          -19+-3*V(1)  0112+V(2) <B 1119+V(1) 100
   26          166+27*V(1)          -18+-3*V(1)  0112+V(2) B> 1119+V(1) 100
   27          193+30*V(1)                    9  0112+V(2) 1119+V(1) B> 100
   28          196+30*V(1)                   12  0112+V(2) 1119+V(1) 110 F>
   29          197+30*V(1)                   11  0112+V(2) 1119+V(1) 110 <E 100
   30          200+30*V(1)                    8  0112+V(2) 1119+V(1) <A 110 100
   31          227+33*V(1)          -19+-3*V(1)  0112+V(2) <A 1119+V(1) 110 100
   32          230+33*V(1)          -22+-3*V(1)  0111+V(2) <B 11110+V(1) 110 100
   33          231+33*V(1)          -21+-3*V(1)  0111+V(2) B> 11110+V(1) 110 100
   34          261+36*V(1)                    9  0111+V(2) 11110+V(1) B> 110 100
   35          264+36*V(1)                   12  0111+V(2) 11111+V(1) C> 100
<< Success! ==> defined new CTR 2 (PA)
  153                 1313                   57  01112 11111 C> 100
== Executing  PA-CTR  2, V(1)=10, V(2)=5, repcount=1, factor=10/6
  188                 1937                   69  0116 11121 C> 100
  189                 1940                   68  0116 11121 <A 110
  190                 2003                    5  0116 <A 11121 110
  191                 2006                    2  0115 <B 11122 110
  192                 2007                    3  0115 B> 11122 110
  193                 2073                   69  0115 11122 B> 110
  194                 2076                   72  0115 11123 C>
  195                 2079                   71  0115 11123 <A 010
  196                 2148                    2  0115 <A 11123 010
  197                 2151                   -1  0114 <B 11124 010
  198                 2152                    0  0114 B> 11124 010
  199                 2224                   72  0114 11124 B> 010
  200                 2229                   71  0114 11124 <A 111
  201                 2301                   -1  0114 <A 11125
  202                 2304                   -4  0113 <B 11126
  203                 2305                   -3  0113 B> 11126
  204                 2383                   75  0113 11126 B>
  205                 2388                   74  0113 11126 <A 101
  206                 2466                   -4  0113 <A 11126 101
  207                 2469                   -7  0112 <B 11127 101
  208                 2470                   -6  0112 B> 11127 101
  209                 2551                   75  0112 11127 B> 101
  210                 2554                   78  0112 11128 D>
  211                 2555                   77  0112 11128 <A 100
  212                 2639                   -7  0112 <A 11128 100
  213                 2642                  -10  011 <B 11129 100
  214                 2643                   -9  011 B> 11129 100
  215                 2730                   78  011 11129 B> 100
  216                 2733                   81  011 11129 110 F>
  217                 2734                   80  011 11129 110 <E 100
  218                 2737                   77  011 11129 <A 110 100
  219                 2824                  -10  011 <A 11129 110 100
  220                 2827                  -13  <B 11130 110 100
  221                 2828                  -12  001 C> 11130 110 100
  222                 2918                   78  001 10130 C> 110 100
  223                 2925                   81  001 10130 111 C> 100
  224                 2928                   80  001 10130 111 <A 110
  225                 2931                   77  001 10130 <A 111 110
  226                 2936                   78  001 10129 111 B> 111 110
  227                 2939                   81  001 10129 1112 B> 110
  228                 2942                   84  001 10129 1113 C>
  229                 2945                   83  001 10129 1113 <A 010
  230                 2954                   74  001 10129 <A 1113 010
  231                 2959                   75  001 10128 111 B> 1113 010
  232                 2968                   84  001 10128 1114 B> 010
  233                 2973                   83  001 10128 1114 <A 111
  234                 2985                   71  001 10128 <A 1115
  235                 2990                   72  001 10127 111 B> 1115
  236                 3005                   87  001 10127 1116 B>
  237                 3010                   86  001 10127 1116 <A 101
  238                 3028                   68  001 10127 <A 1116 101
  239                 3033                   69  001 10126 111 B> 1116 101
  240                 3051                   87  001 10126 1117 B> 101
  241                 3054                   90  001 10126 1118 D>
  242                 3055                   89  001 10126 1118 <A 100
  243                 3079                   65  001 10126 <A 1118 100
  244                 3084                   66  001 10125 111 B> 1118 100
  245                 3108                   90  001 10125 1119 B> 100
  246                 3111                   93  001 10125 1119 110 F>
  247                 3112                   92  001 10125 1119 110 <E 100
  248                 3115                   89  001 10125 1119 <A 110 100
  249                 3142                   62  001 10125 <A 1119 110 100
  250                 3147                   63  001 10124 111 B> 1119 110 100
  251                 3174                   90  001 10124 11110 B> 110 100
  252                 3177                   93  001 10124 11111 C> 100
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  [*]* 1017+V(2) 1111+V(1) C> 100
    1                    3                   -1  [*]* 1017+V(2) 1111+V(1) <A 110
    2             6+3*V(1)           -4+-3*V(1)  [*]* 1017+V(2) <A 1111+V(1) 110
    3            11+3*V(1)           -3+-3*V(1)  [*]* 1016+V(2) 111 B> 1111+V(1) 110
    4            14+6*V(1)                    0  [*]* 1016+V(2) 1112+V(1) B> 110
    5            17+6*V(1)                    3  [*]* 1016+V(2) 1113+V(1) C>
    6            20+6*V(1)                    2  [*]* 1016+V(2) 1113+V(1) <A 010
    7            29+9*V(1)           -7+-3*V(1)  [*]* 1016+V(2) <A 1113+V(1) 010
    8            34+9*V(1)           -6+-3*V(1)  [*]* 1015+V(2) 111 B> 1113+V(1) 010
    9           43+12*V(1)                    3  [*]* 1015+V(2) 1114+V(1) B> 010
   10           48+12*V(1)                    2  [*]* 1015+V(2) 1114+V(1) <A 111
   11           60+15*V(1)          -10+-3*V(1)  [*]* 1015+V(2) <A 1115+V(1)
   12           65+15*V(1)           -9+-3*V(1)  [*]* 1014+V(2) 111 B> 1115+V(1)
   13           80+18*V(1)                    6  [*]* 1014+V(2) 1116+V(1) B>
   14           85+18*V(1)                    5  [*]* 1014+V(2) 1116+V(1) <A 101
   15          103+21*V(1)          -13+-3*V(1)  [*]* 1014+V(2) <A 1116+V(1) 101
   16          108+21*V(1)          -12+-3*V(1)  [*]* 1013+V(2) 111 B> 1116+V(1) 101
   17          126+24*V(1)                    6  [*]* 1013+V(2) 1117+V(1) B> 101
   18          129+24*V(1)                    9  [*]* 1013+V(2) 1118+V(1) D>
   19          130+24*V(1)                    8  [*]* 1013+V(2) 1118+V(1) <A 100
   20          154+27*V(1)          -16+-3*V(1)  [*]* 1013+V(2) <A 1118+V(1) 100
   21          159+27*V(1)          -15+-3*V(1)  [*]* 1012+V(2) 111 B> 1118+V(1) 100
   22          183+30*V(1)                    9  [*]* 1012+V(2) 1119+V(1) B> 100
   23          186+30*V(1)                   12  [*]* 1012+V(2) 1119+V(1) 110 F>
   24          187+30*V(1)                   11  [*]* 1012+V(2) 1119+V(1) 110 <E 100
   25          190+30*V(1)                    8  [*]* 1012+V(2) 1119+V(1) <A 110 100
   26          217+33*V(1)          -19+-3*V(1)  [*]* 1012+V(2) <A 1119+V(1) 110 100
   27          222+33*V(1)          -18+-3*V(1)  [*]* 1011+V(2) 111 B> 1119+V(1) 110 100
   28          249+36*V(1)                    9  [*]* 1011+V(2) 11110+V(1) B> 110 100
   29          252+36*V(1)                   12  [*]* 1011+V(2) 11111+V(1) C> 100
<< Success! ==> defined new CTR 3 (PA)
  252                 3177                   93  001 10124 11111 C> 100
== Executing  PA-CTR  3, V(1)=10, V(2)=17, repcount=3, factor=10/6
  339                 6093                  129  001 1016 11141 C> 100
  340                 6096                  128  001 1016 11141 <A 110
  341                 6219                    5  001 1016 <A 11141 110
  342                 6224                    6  001 1015 111 B> 11141 110
  343                 6347                  129  001 1015 11142 B> 110
  344                 6350                  132  001 1015 11143 C>
  345                 6353                  131  001 1015 11143 <A 010
  346                 6482                    2  001 1015 <A 11143 010
  347                 6487                    3  001 1014 111 B> 11143 010
  348                 6616                  132  001 1014 11144 B> 010
  349                 6621                  131  001 1014 11144 <A 111
  350                 6753                   -1  001 1014 <A 11145
  351                 6758                    0  001 1013 111 B> 11145
  352                 6893                  135  001 1013 11146 B>
  353                 6898                  134  001 1013 11146 <A 101
  354                 7036                   -4  001 1013 <A 11146 101
  355                 7041                   -3  001 1012 111 B> 11146 101
  356                 7179                  135  001 1012 11147 B> 101
  357                 7182                  138  001 1012 11148 D>
  358                 7183                  137  001 1012 11148 <A 100
  359                 7327                   -7  001 1012 <A 11148 100
  360                 7332                   -6  001 101 111 B> 11148 100
  361                 7476                  138  001 101 11149 B> 100
  362                 7479                  141  001 101 11149 110 F>
  363                 7480                  140  001 101 11149 110 <E 100
  364                 7483                  137  001 101 11149 <A 110 100
  365                 7630                  -10  001 101 <A 11149 110 100
  366                 7635                   -9  001 111 B> 11149 110 100
  367                 7782                  138  001 11150 B> 110 100
  368                 7785                  141  001 11151 C> 100
  369                 7788                  140  001 11151 <A 110
  370                 7941                  -13  001 <A 11151 110
  371                 7946                  -12  110 E> 11151 110
  372                 8099                  141  11052 E> 110
  373                 8104                  140  11052 <A 111
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  001 1016 1111+V(1) C> 100
    1                    3                   -1  001 1016 1111+V(1) <A 110
    2             6+3*V(1)           -4+-3*V(1)  001 1016 <A 1111+V(1) 110
    3            11+3*V(1)           -3+-3*V(1)  001 1015 111 B> 1111+V(1) 110
    4            14+6*V(1)                    0  001 1015 1112+V(1) B> 110
    5            17+6*V(1)                    3  001 1015 1113+V(1) C>
    6            20+6*V(1)                    2  001 1015 1113+V(1) <A 010
    7            29+9*V(1)           -7+-3*V(1)  001 1015 <A 1113+V(1) 010
    8            34+9*V(1)           -6+-3*V(1)  001 1014 111 B> 1113+V(1) 010
    9           43+12*V(1)                    3  001 1014 1114+V(1) B> 010
   10           48+12*V(1)                    2  001 1014 1114+V(1) <A 111
   11           60+15*V(1)          -10+-3*V(1)  001 1014 <A 1115+V(1)
   12           65+15*V(1)           -9+-3*V(1)  001 1013 111 B> 1115+V(1)
   13           80+18*V(1)                    6  001 1013 1116+V(1) B>
   14           85+18*V(1)                    5  001 1013 1116+V(1) <A 101
   15          103+21*V(1)          -13+-3*V(1)  001 1013 <A 1116+V(1) 101
   16          108+21*V(1)          -12+-3*V(1)  001 1012 111 B> 1116+V(1) 101
   17          126+24*V(1)                    6  001 1012 1117+V(1) B> 101
   18          129+24*V(1)                    9  001 1012 1118+V(1) D>
   19          130+24*V(1)                    8  001 1012 1118+V(1) <A 100
   20          154+27*V(1)          -16+-3*V(1)  001 1012 <A 1118+V(1) 100
   21          159+27*V(1)          -15+-3*V(1)  001 101 111 B> 1118+V(1) 100
   22          183+30*V(1)                    9  001 101 1119+V(1) B> 100
   23          186+30*V(1)                   12  001 101 1119+V(1) 110 F>
   24          187+30*V(1)                   11  001 101 1119+V(1) 110 <E 100
   25          190+30*V(1)                    8  001 101 1119+V(1) <A 110 100
   26          217+33*V(1)          -19+-3*V(1)  001 101 <A 1119+V(1) 110 100
   27          222+33*V(1)          -18+-3*V(1)  001 111 B> 1119+V(1) 110 100
   28          249+36*V(1)                    9  001 11110+V(1) B> 110 100
   29          252+36*V(1)                   12  001 11111+V(1) C> 100
   30          255+36*V(1)                   11  001 11111+V(1) <A 110
   31          288+39*V(1)          -22+-3*V(1)  001 <A 11111+V(1) 110
   32          293+39*V(1)          -21+-3*V(1)  110 E> 11111+V(1) 110
   33          326+42*V(1)                   12  11012+V(1) E> 110
   34          331+42*V(1)                   11  11012+V(1) <A 111
<< Success! ==> defined new CTR 4 (PPA)
  373                 8104                  140  11052 <A 111
== Executing  PA-CTR  1, V(1)=45, V(2)=0, repcount=8, factor=10/6
  605                20152                   -4  1104 <A 11181
  606                20155                   -3  1103 111 B> 11181
  607                20398                  240  1103 11182 B>
  608                20403                  239  1103 11182 <A 101
  609                20649                   -7  1103 <A 11182 101
  610                20652                   -6  1102 111 B> 11182 101
  611                20898                  240  1102 11183 B> 101
  612                20901                  243  1102 11184 D>
  613                20902                  242  1102 11184 <A 100
  614                21154                  -10  1102 <A 11184 100
  615                21157                   -9  110 111 B> 11184 100
  616                21409                  243  110 11185 B> 100
  617                21412                  246  110 11185 110 F>
  618                21413                  245  110 11185 110 <E 100
  619                21416                  242  110 11185 <A 110 100
  620                21671                  -13  110 <A 11185 110 100
  621                21674                  -12  111 B> 11185 110 100
  622                21929                  243  11186 B> 110 100
  623                21932                  246  11187 C> 100
  624                21935                  245  11187 <A 110
  625                22196                  -16  <A 11187 110
  626                22199                  -15  011 D> 11187 110
  627                22460                  246  01188 D> 110
  628                22463                  249  01188 010 F>
  629                22464                  248  01188 010 <E 100
  630                22467                  245  01188 <B 110 100
  631                22468                  246  01188 B> 110 100
  632                22471                  249  01188 111 C> 100
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  1104 <A 1111+V(1)
    1                    3                    1  1103 111 B> 1111+V(1)
    2             6+3*V(1)             4+3*V(1)  1103 1112+V(1) B>
    3            11+3*V(1)             3+3*V(1)  1103 1112+V(1) <A 101
    4            17+6*V(1)                   -3  1103 <A 1112+V(1) 101
    5            20+6*V(1)                   -2  1102 111 B> 1112+V(1) 101
    6            26+9*V(1)             4+3*V(1)  1102 1113+V(1) B> 101
    7            29+9*V(1)             7+3*V(1)  1102 1114+V(1) D>
    8            30+9*V(1)             6+3*V(1)  1102 1114+V(1) <A 100
    9           42+12*V(1)                   -6  1102 <A 1114+V(1) 100
   10           45+12*V(1)                   -5  110 111 B> 1114+V(1) 100
   11           57+15*V(1)             7+3*V(1)  110 1115+V(1) B> 100
   12           60+15*V(1)            10+3*V(1)  110 1115+V(1) 110 F>
   13           61+15*V(1)             9+3*V(1)  110 1115+V(1) 110 <E 100
   14           64+15*V(1)             6+3*V(1)  110 1115+V(1) <A 110 100
   15           79+18*V(1)                   -9  110 <A 1115+V(1) 110 100
   16           82+18*V(1)                   -8  111 B> 1115+V(1) 110 100
   17           97+21*V(1)             7+3*V(1)  1116+V(1) B> 110 100
   18          100+21*V(1)            10+3*V(1)  1117+V(1) C> 100
   19          103+21*V(1)             9+3*V(1)  1117+V(1) <A 110
   20          124+24*V(1)                  -12  <A 1117+V(1) 110
   21          127+24*V(1)                  -11  011 D> 1117+V(1) 110
   22          148+27*V(1)            10+3*V(1)  0118+V(1) D> 110
   23          151+27*V(1)            13+3*V(1)  0118+V(1) 010 F>
   24          152+27*V(1)            12+3*V(1)  0118+V(1) 010 <E 100
   25          155+27*V(1)             9+3*V(1)  0118+V(1) <B 110 100
   26          156+27*V(1)            10+3*V(1)  0118+V(1) B> 110 100
   27          159+27*V(1)            13+3*V(1)  0118+V(1) 111 C> 100
<< Success! ==> defined new CTR 5 (PPA)
  632                22471                  249  01188 111 C> 100
== Executing  PA-CTR  2, V(1)=0, V(2)=81, repcount=14, factor=10/6
 1122                58927                  417  0114 111141 C> 100
 1123                58930                  416  0114 111141 <A 110
 1124                59353                   -7  0114 <A 111141 110
 1125                59356                  -10  0113 <B 111142 110
 1126                59357                   -9  0113 B> 111142 110
 1127                59783                  417  0113 111142 B> 110
 1128                59786                  420  0113 111143 C>
 1129                59789                  419  0113 111143 <A 010
 1130                60218                  -10  0113 <A 111143 010
 1131                60221                  -13  0112 <B 111144 010
 1132                60222                  -12  0112 B> 111144 010
 1133                60654                  420  0112 111144 B> 010
 1134                60659                  419  0112 111144 <A 111
 1135                61091                  -13  0112 <A 111145
 1136                61094                  -16  011 <B 111146
 1137                61095                  -15  011 B> 111146
 1138                61533                  423  011 111146 B>
 1139                61538                  422  011 111146 <A 101
 1140                61976                  -16  011 <A 111146 101
 1141                61979                  -19  <B 111147 101
 1142                61980                  -18  001 C> 111147 101
 1143                62421                  423  001 101147 C> 101
 1144                62424                  422  001 101147 <A 111
 1145                62429                  423  001 101146 111 B> 111
 1146                62432                  426  001 101146 1112 B>
 1147                62437                  425  001 101146 1112 <A 101
 1148                62443                  419  001 101146 <A 1112 101
 1149                62448                  420  001 101145 111 B> 1112 101
 1150                62454                  426  001 101145 1113 B> 101
 1151                62457                  429  001 101145 1114 D>
 1152                62458                  428  001 101145 1114 <A 100
 1153                62470                  416  001 101145 <A 1114 100
 1154                62475                  417  001 101144 111 B> 1114 100
 1155                62487                  429  001 101144 1115 B> 100
 1156                62490                  432  001 101144 1115 110 F>
 1157                62491                  431  001 101144 1115 110 <E 100
 1158                62494                  428  001 101144 1115 <A 110 100
 1159                62509                  413  001 101144 <A 1115 110 100
 1160                62514                  414  001 101143 111 B> 1115 110 100
 1161                62529                  429  001 101143 1116 B> 110 100
 1162                62532                  432  001 101143 1117 C> 100
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  0114 1115+V(1) C> 100
    1                    3                   -1  0114 1115+V(1) <A 110
    2            18+3*V(1)          -16+-3*V(1)  0114 <A 1115+V(1) 110
    3            21+3*V(1)          -19+-3*V(1)  0113 <B 1116+V(1) 110
    4            22+3*V(1)          -18+-3*V(1)  0113 B> 1116+V(1) 110
    5            40+6*V(1)                    0  0113 1116+V(1) B> 110
    6            43+6*V(1)                    3  0113 1117+V(1) C>
    7            46+6*V(1)                    2  0113 1117+V(1) <A 010
    8            67+9*V(1)          -19+-3*V(1)  0113 <A 1117+V(1) 010
    9            70+9*V(1)          -22+-3*V(1)  0112 <B 1118+V(1) 010
   10            71+9*V(1)          -21+-3*V(1)  0112 B> 1118+V(1) 010
   11           95+12*V(1)                    3  0112 1118+V(1) B> 010
   12          100+12*V(1)                    2  0112 1118+V(1) <A 111
   13          124+15*V(1)          -22+-3*V(1)  0112 <A 1119+V(1)
   14          127+15*V(1)          -25+-3*V(1)  011 <B 11110+V(1)
   15          128+15*V(1)          -24+-3*V(1)  011 B> 11110+V(1)
   16          158+18*V(1)                    6  011 11110+V(1) B>
   17          163+18*V(1)                    5  011 11110+V(1) <A 101
   18          193+21*V(1)          -25+-3*V(1)  011 <A 11110+V(1) 101
   19          196+21*V(1)          -28+-3*V(1)  <B 11111+V(1) 101
   20          197+21*V(1)          -27+-3*V(1)  001 C> 11111+V(1) 101
   21          230+24*V(1)                    6  001 10111+V(1) C> 101
   22          233+24*V(1)                    5  001 10111+V(1) <A 111
   23          238+24*V(1)                    6  001 10110+V(1) 111 B> 111
   24          241+24*V(1)                    9  001 10110+V(1) 1112 B>
   25          246+24*V(1)                    8  001 10110+V(1) 1112 <A 101
   26          252+24*V(1)                    2  001 10110+V(1) <A 1112 101
   27          257+24*V(1)                    3  001 1019+V(1) 111 B> 1112 101
   28          263+24*V(1)                    9  001 1019+V(1) 1113 B> 101
   29          266+24*V(1)                   12  001 1019+V(1) 1114 D>
   30          267+24*V(1)                   11  001 1019+V(1) 1114 <A 100
   31          279+24*V(1)                   -1  001 1019+V(1) <A 1114 100
   32          284+24*V(1)                    0  001 1018+V(1) 111 B> 1114 100
   33          296+24*V(1)                   12  001 1018+V(1) 1115 B> 100
   34          299+24*V(1)                   15  001 1018+V(1) 1115 110 F>
   35          300+24*V(1)                   14  001 1018+V(1) 1115 110 <E 100
   36          303+24*V(1)                   11  001 1018+V(1) 1115 <A 110 100
   37          318+24*V(1)                   -4  001 1018+V(1) <A 1115 110 100
   38          323+24*V(1)                   -3  001 1017+V(1) 111 B> 1115 110 100
   39          338+24*V(1)                   12  001 1017+V(1) 1116 B> 110 100
   40          341+24*V(1)                   15  001 1017+V(1) 1117 C> 100
<< Success! ==> defined new CTR 6 (PPA)
 1162                62532                  432  001 101143 1117 C> 100
== Executing  PA-CTR  3, V(1)=6, V(2)=136, repcount=23, factor=10/6
 1829               164376                  708  001 1015 111237 C> 100
 1830               164379                  707  001 1015 111237 <A 110
 1831               165090                   -4  001 1015 <A 111237 110
 1832               165095                   -3  001 1014 111 B> 111237 110
 1833               165806                  708  001 1014 111238 B> 110
 1834               165809                  711  001 1014 111239 C>
 1835               165812                  710  001 1014 111239 <A 010
 1836               166529                   -7  001 1014 <A 111239 010
 1837               166534                   -6  001 1013 111 B> 111239 010
 1838               167251                  711  001 1013 111240 B> 010
 1839               167256                  710  001 1013 111240 <A 111
 1840               167976                  -10  001 1013 <A 111241
 1841               167981                   -9  001 1012 111 B> 111241
 1842               168704                  714  001 1012 111242 B>
 1843               168709                  713  001 1012 111242 <A 101
 1844               169435                  -13  001 1012 <A 111242 101
 1845               169440                  -12  001 101 111 B> 111242 101
 1846               170166                  714  001 101 111243 B> 101
 1847               170169                  717  001 101 111244 D>
 1848               170170                  716  001 101 111244 <A 100
 1849               170902                  -16  001 101 <A 111244 100
 1850               170907                  -15  001 111 B> 111244 100
 1851               171639                  717  001 111245 B> 100
 1852               171642                  720  001 111245 110 F>
 1853               171643                  719  001 111245 110 <E 100
 1854               171646                  716  001 111245 <A 110 100
 1855               172381                  -19  001 <A 111245 110 100
 1856               172386                  -18  110 E> 111245 110 100
 1857               173121                  717  110246 E> 110 100
 1858               173126                  716  110246 <A 111 100
 1859               173129                  717  110245 111 B> 111 100
 1860               173132                  720  110245 1112 B> 100
 1861               173135                  723  110245 1112 110 F>
 1862               173136                  722  110245 1112 110 <E 100
 1863               173139                  719  110245 1112 <A 110 100
 1864               173145                  713  110245 <A 1112 110 100
 1865               173148                  714  110244 111 B> 1112 110 100
 1866               173154                  720  110244 1113 B> 110 100
 1867               173157                  723  110244 1114 C> 100
 1868               173160                  722  110244 1114 <A 110
 1869               173172                  710  110244 <A 1114 110
 1870               173175                  711  110243 111 B> 1114 110
 1871               173187                  723  110243 1115 B> 110
 1872               173190                  726  110243 1116 C>
 1873               173193                  725  110243 1116 <A 010
 1874               173211                  707  110243 <A 1116 010
 1875               173214                  708  110242 111 B> 1116 010
 1876               173232                  726  110242 1117 B> 010
 1877               173237                  725  110242 1117 <A 111
 1878               173258                  704  110242 <A 1118
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  001 1015 1112+V(1) C> 100
    1                    3                   -1  001 1015 1112+V(1) <A 110
    2             9+3*V(1)           -7+-3*V(1)  001 1015 <A 1112+V(1) 110
    3            14+3*V(1)           -6+-3*V(1)  001 1014 111 B> 1112+V(1) 110
    4            20+6*V(1)                    0  001 1014 1113+V(1) B> 110
    5            23+6*V(1)                    3  001 1014 1114+V(1) C>
    6            26+6*V(1)                    2  001 1014 1114+V(1) <A 010
    7            38+9*V(1)          -10+-3*V(1)  001 1014 <A 1114+V(1) 010
    8            43+9*V(1)           -9+-3*V(1)  001 1013 111 B> 1114+V(1) 010
    9           55+12*V(1)                    3  001 1013 1115+V(1) B> 010
   10           60+12*V(1)                    2  001 1013 1115+V(1) <A 111
   11           75+15*V(1)          -13+-3*V(1)  001 1013 <A 1116+V(1)
   12           80+15*V(1)          -12+-3*V(1)  001 1012 111 B> 1116+V(1)
   13           98+18*V(1)                    6  001 1012 1117+V(1) B>
   14          103+18*V(1)                    5  001 1012 1117+V(1) <A 101
   15          124+21*V(1)          -16+-3*V(1)  001 1012 <A 1117+V(1) 101
   16          129+21*V(1)          -15+-3*V(1)  001 101 111 B> 1117+V(1) 101
   17          150+24*V(1)                    6  001 101 1118+V(1) B> 101
   18          153+24*V(1)                    9  001 101 1119+V(1) D>
   19          154+24*V(1)                    8  001 101 1119+V(1) <A 100
   20          181+27*V(1)          -19+-3*V(1)  001 101 <A 1119+V(1) 100
   21          186+27*V(1)          -18+-3*V(1)  001 111 B> 1119+V(1) 100
   22          213+30*V(1)                    9  001 11110+V(1) B> 100
   23          216+30*V(1)                   12  001 11110+V(1) 110 F>
   24          217+30*V(1)                   11  001 11110+V(1) 110 <E 100
   25          220+30*V(1)                    8  001 11110+V(1) <A 110 100
   26          250+33*V(1)          -22+-3*V(1)  001 <A 11110+V(1) 110 100
   27          255+33*V(1)          -21+-3*V(1)  110 E> 11110+V(1) 110 100
   28          285+36*V(1)                    9  11011+V(1) E> 110 100
   29          290+36*V(1)                    8  11011+V(1) <A 111 100
   30          293+36*V(1)                    9  11010+V(1) 111 B> 111 100
   31          296+36*V(1)                   12  11010+V(1) 1112 B> 100
   32          299+36*V(1)                   15  11010+V(1) 1112 110 F>
   33          300+36*V(1)                   14  11010+V(1) 1112 110 <E 100
   34          303+36*V(1)                   11  11010+V(1) 1112 <A 110 100
   35          309+36*V(1)                    5  11010+V(1) <A 1112 110 100
   36          312+36*V(1)                    6  1109+V(1) 111 B> 1112 110 100
   37          318+36*V(1)                   12  1109+V(1) 1113 B> 110 100
   38          321+36*V(1)                   15  1109+V(1) 1114 C> 100
   39          324+36*V(1)                   14  1109+V(1) 1114 <A 110
   40          336+36*V(1)                    2  1109+V(1) <A 1114 110
   41          339+36*V(1)                    3  1108+V(1) 111 B> 1114 110
   42          351+36*V(1)                   15  1108+V(1) 1115 B> 110
   43          354+36*V(1)                   18  1108+V(1) 1116 C>
   44          357+36*V(1)                   17  1108+V(1) 1116 <A 010
   45          375+36*V(1)                   -1  1108+V(1) <A 1116 010
   46          378+36*V(1)                    0  1107+V(1) 111 B> 1116 010
   47          396+36*V(1)                   18  1107+V(1) 1117 B> 010
   48          401+36*V(1)                   17  1107+V(1) 1117 <A 111
   49          422+36*V(1)                   -4  1107+V(1) <A 1118
<< Success! ==> defined new CTR 7 (PPA)
 1878               173258                  704  110242 <A 1118
== Executing  PA-CTR  1, V(1)=235, V(2)=7, repcount=40, factor=10/6
 3038               473978                  -16  1102 <A 111408
 3039               473981                  -15  110 111 B> 111408
 3040               475205                 1209  110 111409 B>
 3041               475210                 1208  110 111409 <A 101
 3042               476437                  -19  110 <A 111409 101
 3043               476440                  -18  111 B> 111409 101
 3044               477667                 1209  111410 B> 101
 3045               477670                 1212  111411 D>
 3046               477671                 1211  111411 <A 100
 3047               478904                  -22  <A 111411 100
 3048               478907                  -21  011 D> 111411 100
 3049               480140                 1212  011412 D> 100
 3050               480143                 1211  011412 <B 100
 3051               480144                 1212  011412 B> 100
 3052               480147                 1215  011412 110 F>
 3053               480148                 1214  011412 110 <E 100
 3054               480151                 1211  011412 <A 110 100
 3055               480154                 1208  011411 <B 111 110 100
 3056               480155                 1209  011411 B> 111 110 100
 3057               480158                 1212  011411 111 B> 110 100
 3058               480161                 1215  011411 1112 C> 100
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  1102 <A 1114+V(1)
    1                    3                    1  110 111 B> 1114+V(1)
    2            15+3*V(1)            13+3*V(1)  110 1115+V(1) B>
    3            20+3*V(1)            12+3*V(1)  110 1115+V(1) <A 101
    4            35+6*V(1)                   -3  110 <A 1115+V(1) 101
    5            38+6*V(1)                   -2  111 B> 1115+V(1) 101
    6            53+9*V(1)            13+3*V(1)  1116+V(1) B> 101
    7            56+9*V(1)            16+3*V(1)  1117+V(1) D>
    8            57+9*V(1)            15+3*V(1)  1117+V(1) <A 100
    9           78+12*V(1)                   -6  <A 1117+V(1) 100
   10           81+12*V(1)                   -5  011 D> 1117+V(1) 100
   11          102+15*V(1)            16+3*V(1)  0118+V(1) D> 100
   12          105+15*V(1)            15+3*V(1)  0118+V(1) <B 100
   13          106+15*V(1)            16+3*V(1)  0118+V(1) B> 100
   14          109+15*V(1)            19+3*V(1)  0118+V(1) 110 F>
   15          110+15*V(1)            18+3*V(1)  0118+V(1) 110 <E 100
   16          113+15*V(1)            15+3*V(1)  0118+V(1) <A 110 100
   17          116+15*V(1)            12+3*V(1)  0117+V(1) <B 111 110 100
   18          117+15*V(1)            13+3*V(1)  0117+V(1) B> 111 110 100
   19          120+15*V(1)            16+3*V(1)  0117+V(1) 111 B> 110 100
   20          123+15*V(1)            19+3*V(1)  0117+V(1) 1112 C> 100
<< Success! ==> defined new CTR 8 (PPA)
 3058               480161                 1215  011411 1112 C> 100
== Executing  PA-CTR  2, V(1)=1, V(2)=404, repcount=68, factor=10/6
 5438              1320641                 2031  0113 111682 C> 100
 5439              1320644                 2030  0113 111682 <A 110
 5440              1322690                  -16  0113 <A 111682 110
 5441              1322693                  -19  0112 <B 111683 110
 5442              1322694                  -18  0112 B> 111683 110
 5443              1324743                 2031  0112 111683 B> 110
 5444              1324746                 2034  0112 111684 C>
 5445              1324749                 2033  0112 111684 <A 010
 5446              1326801                  -19  0112 <A 111684 010
 5447              1326804                  -22  011 <B 111685 010
 5448              1326805                  -21  011 B> 111685 010
 5449              1328860                 2034  011 111685 B> 010
 5450              1328865                 2033  011 111685 <A 111
 5451              1330920                  -22  011 <A 111686
 5452              1330923                  -25  <B 111687
 5453              1330924                  -24  001 C> 111687
 5454              1332985                 2037  001 101687 C>
 5455              1332988                 2036  001 101687 <A 010
 5456              1332993                 2037  001 101686 111 B> 010
 5457              1332998                 2036  001 101686 111 <A 111
 5458              1333001                 2033  001 101686 <A 1112
 5459              1333006                 2034  001 101685 111 B> 1112
 5460              1333012                 2040  001 101685 1113 B>
 5461              1333017                 2039  001 101685 1113 <A 101
 5462              1333026                 2030  001 101685 <A 1113 101
 5463              1333031                 2031  001 101684 111 B> 1113 101
 5464              1333040                 2040  001 101684 1114 B> 101
 5465              1333043                 2043  001 101684 1115 D>
 5466              1333044                 2042  001 101684 1115 <A 100
 5467              1333059                 2027  001 101684 <A 1115 100
 5468              1333064                 2028  001 101683 111 B> 1115 100
 5469              1333079                 2043  001 101683 1116 B> 100
 5470              1333082                 2046  001 101683 1116 110 F>
 5471              1333083                 2045  001 101683 1116 110 <E 100
 5472              1333086                 2042  001 101683 1116 <A 110 100
 5473              1333104                 2024  001 101683 <A 1116 110 100
 5474              1333109                 2025  001 101682 111 B> 1116 110 100
 5475              1333127                 2043  001 101682 1117 B> 110 100
 5476              1333130                 2046  001 101682 1118 C> 100
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  0113 1117+V(1) C> 100
    1                    3                   -1  0113 1117+V(1) <A 110
    2            24+3*V(1)          -22+-3*V(1)  0113 <A 1117+V(1) 110
    3            27+3*V(1)          -25+-3*V(1)  0112 <B 1118+V(1) 110
    4            28+3*V(1)          -24+-3*V(1)  0112 B> 1118+V(1) 110
    5            52+6*V(1)                    0  0112 1118+V(1) B> 110
    6            55+6*V(1)                    3  0112 1119+V(1) C>
    7            58+6*V(1)                    2  0112 1119+V(1) <A 010
    8            85+9*V(1)          -25+-3*V(1)  0112 <A 1119+V(1) 010
    9            88+9*V(1)          -28+-3*V(1)  011 <B 11110+V(1) 010
   10            89+9*V(1)          -27+-3*V(1)  011 B> 11110+V(1) 010
   11          119+12*V(1)                    3  011 11110+V(1) B> 010
   12          124+12*V(1)                    2  011 11110+V(1) <A 111
   13          154+15*V(1)          -28+-3*V(1)  011 <A 11111+V(1)
   14          157+15*V(1)          -31+-3*V(1)  <B 11112+V(1)
   15          158+15*V(1)          -30+-3*V(1)  001 C> 11112+V(1)
   16          194+18*V(1)                    6  001 10112+V(1) C>
   17          197+18*V(1)                    5  001 10112+V(1) <A 010
   18          202+18*V(1)                    6  001 10111+V(1) 111 B> 010
   19          207+18*V(1)                    5  001 10111+V(1) 111 <A 111
   20          210+18*V(1)                    2  001 10111+V(1) <A 1112
   21          215+18*V(1)                    3  001 10110+V(1) 111 B> 1112
   22          221+18*V(1)                    9  001 10110+V(1) 1113 B>
   23          226+18*V(1)                    8  001 10110+V(1) 1113 <A 101
   24          235+18*V(1)                   -1  001 10110+V(1) <A 1113 101
   25          240+18*V(1)                    0  001 1019+V(1) 111 B> 1113 101
   26          249+18*V(1)                    9  001 1019+V(1) 1114 B> 101
   27          252+18*V(1)                   12  001 1019+V(1) 1115 D>
   28          253+18*V(1)                   11  001 1019+V(1) 1115 <A 100
   29          268+18*V(1)                   -4  001 1019+V(1) <A 1115 100
   30          273+18*V(1)                   -3  001 1018+V(1) 111 B> 1115 100
   31          288+18*V(1)                   12  001 1018+V(1) 1116 B> 100
   32          291+18*V(1)                   15  001 1018+V(1) 1116 110 F>
   33          292+18*V(1)                   14  001 1018+V(1) 1116 110 <E 100
   34          295+18*V(1)                   11  001 1018+V(1) 1116 <A 110 100
   35          313+18*V(1)                   -7  001 1018+V(1) <A 1116 110 100
   36          318+18*V(1)                   -6  001 1017+V(1) 111 B> 1116 110 100
   37          336+18*V(1)                   12  001 1017+V(1) 1117 B> 110 100
   38          339+18*V(1)                   15  001 1017+V(1) 1118 C> 100
<< Success! ==> defined new CTR 9 (PPA)
 5476              1333130                 2046  001 101682 1118 C> 100
== Executing  PA-CTR  3, V(1)=7, V(2)=675, repcount=113, factor=10/6
 8753              3668162                 3402  001 1014 1111138 C> 100
 8754              3668165                 3401  001 1014 1111138 <A 110
 8755              3671579                  -13  001 1014 <A 1111138 110
 8756              3671584                  -12  001 1013 111 B> 1111138 110
 8757              3674998                 3402  001 1013 1111139 B> 110
 8758              3675001                 3405  001 1013 1111140 C>
 8759              3675004                 3404  001 1013 1111140 <A 010
 8760              3678424                  -16  001 1013 <A 1111140 010
 8761              3678429                  -15  001 1012 111 B> 1111140 010
 8762              3681849                 3405  001 1012 1111141 B> 010
 8763              3681854                 3404  001 1012 1111141 <A 111
 8764              3685277                  -19  001 1012 <A 1111142
 8765              3685282                  -18  001 101 111 B> 1111142
 8766              3688708                 3408  001 101 1111143 B>
 8767              3688713                 3407  001 101 1111143 <A 101
 8768              3692142                  -22  001 101 <A 1111143 101
 8769              3692147                  -21  001 111 B> 1111143 101
 8770              3695576                 3408  001 1111144 B> 101
 8771              3695579                 3411  001 1111145 D>
 8772              3695580                 3410  001 1111145 <A 100
 8773              3699015                  -25  001 <A 1111145 100
 8774              3699020                  -24  110 E> 1111145 100
 8775              3702455                 3411  1101146 E> 100
 8776              3702460                 3410  1101146 <A 101
 8777              3702463                 3411  1101145 111 B> 101
 8778              3702466                 3414  1101145 1112 D>
 8779              3702467                 3413  1101145 1112 <A 100
 8780              3702473                 3407  1101145 <A 1112 100
 8781              3702476                 3408  1101144 111 B> 1112 100
 8782              3702482                 3414  1101144 1113 B> 100
 8783              3702485                 3417  1101144 1113 110 F>
 8784              3702486                 3416  1101144 1113 110 <E 100
 8785              3702489                 3413  1101144 1113 <A 110 100
 8786              3702498                 3404  1101144 <A 1113 110 100
 8787              3702501                 3405  1101143 111 B> 1113 110 100
 8788              3702510                 3414  1101143 1114 B> 110 100
 8789              3702513                 3417  1101143 1115 C> 100
 8790              3702516                 3416  1101143 1115 <A 110
 8791              3702531                 3401  1101143 <A 1115 110
 8792              3702534                 3402  1101142 111 B> 1115 110
 8793              3702549                 3417  1101142 1116 B> 110
 8794              3702552                 3420  1101142 1117 C>
 8795              3702555                 3419  1101142 1117 <A 010
 8796              3702576                 3398  1101142 <A 1117 010
 8797              3702579                 3399  1101141 111 B> 1117 010
 8798              3702600                 3420  1101141 1118 B> 010
 8799              3702605                 3419  1101141 1118 <A 111
 8800              3702629                 3395  1101141 <A 1119
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  001 1014 1114+V(1) C> 100
    1                    3                   -1  001 1014 1114+V(1) <A 110
    2            15+3*V(1)          -13+-3*V(1)  001 1014 <A 1114+V(1) 110
    3            20+3*V(1)          -12+-3*V(1)  001 1013 111 B> 1114+V(1) 110
    4            32+6*V(1)                    0  001 1013 1115+V(1) B> 110
    5            35+6*V(1)                    3  001 1013 1116+V(1) C>
    6            38+6*V(1)                    2  001 1013 1116+V(1) <A 010
    7            56+9*V(1)          -16+-3*V(1)  001 1013 <A 1116+V(1) 010
    8            61+9*V(1)          -15+-3*V(1)  001 1012 111 B> 1116+V(1) 010
    9           79+12*V(1)                    3  001 1012 1117+V(1) B> 010
   10           84+12*V(1)                    2  001 1012 1117+V(1) <A 111
   11          105+15*V(1)          -19+-3*V(1)  001 1012 <A 1118+V(1)
   12          110+15*V(1)          -18+-3*V(1)  001 101 111 B> 1118+V(1)
   13          134+18*V(1)                    6  001 101 1119+V(1) B>
   14          139+18*V(1)                    5  001 101 1119+V(1) <A 101
   15          166+21*V(1)          -22+-3*V(1)  001 101 <A 1119+V(1) 101
   16          171+21*V(1)          -21+-3*V(1)  001 111 B> 1119+V(1) 101
   17          198+24*V(1)                    6  001 11110+V(1) B> 101
   18          201+24*V(1)                    9  001 11111+V(1) D>
   19          202+24*V(1)                    8  001 11111+V(1) <A 100
   20          235+27*V(1)          -25+-3*V(1)  001 <A 11111+V(1) 100
   21          240+27*V(1)          -24+-3*V(1)  110 E> 11111+V(1) 100
   22          273+30*V(1)                    9  11012+V(1) E> 100
   23          278+30*V(1)                    8  11012+V(1) <A 101
   24          281+30*V(1)                    9  11011+V(1) 111 B> 101
   25          284+30*V(1)                   12  11011+V(1) 1112 D>
   26          285+30*V(1)                   11  11011+V(1) 1112 <A 100
   27          291+30*V(1)                    5  11011+V(1) <A 1112 100
   28          294+30*V(1)                    6  11010+V(1) 111 B> 1112 100
   29          300+30*V(1)                   12  11010+V(1) 1113 B> 100
   30          303+30*V(1)                   15  11010+V(1) 1113 110 F>
   31          304+30*V(1)                   14  11010+V(1) 1113 110 <E 100
   32          307+30*V(1)                   11  11010+V(1) 1113 <A 110 100
   33          316+30*V(1)                    2  11010+V(1) <A 1113 110 100
   34          319+30*V(1)                    3  1109+V(1) 111 B> 1113 110 100
   35          328+30*V(1)                   12  1109+V(1) 1114 B> 110 100
   36          331+30*V(1)                   15  1109+V(1) 1115 C> 100
   37          334+30*V(1)                   14  1109+V(1) 1115 <A 110
   38          349+30*V(1)                   -1  1109+V(1) <A 1115 110
   39          352+30*V(1)                    0  1108+V(1) 111 B> 1115 110
   40          367+30*V(1)                   15  1108+V(1) 1116 B> 110
   41          370+30*V(1)                   18  1108+V(1) 1117 C>
   42          373+30*V(1)                   17  1108+V(1) 1117 <A 010
   43          394+30*V(1)                   -4  1108+V(1) <A 1117 010
   44          397+30*V(1)                   -3  1107+V(1) 111 B> 1117 010
   45          418+30*V(1)                   18  1107+V(1) 1118 B> 010
   46          423+30*V(1)                   17  1107+V(1) 1118 <A 111
   47          447+30*V(1)                   -7  1107+V(1) <A 1119
<< Success! ==> defined new CTR 10 (PPA)
 8800              3702629                 3395  1101141 <A 1119
== Executing  PA-CTR  1, V(1)=1134, V(2)=8, repcount=190, factor=10/6
14310             10267889                  -25  110 <A 1111909
14311             10267892                  -24  111 B> 1111909
14312             10273619                 5703  1111910 B>
14313             10273624                 5702  1111910 <A 101
14314             10279354                  -28  <A 1111910 101
14315             10279357                  -27  011 D> 1111910 101
14316             10285087                 5703  0111911 D> 101
14317             10285090                 5702  0111911 <B 101
14318             10285091                 5703  0111911 B> 101
14319             10285094                 5706  0111911 111 D>
14320             10285095                 5705  0111911 111 <A 100
14321             10285098                 5702  0111911 <A 111 100
14322             10285101                 5699  0111910 <B 1112 100
14323             10285102                 5700  0111910 B> 1112 100
14324             10285108                 5706  0111910 1112 B> 100
14325             10285111                 5709  0111910 1112 110 F>
14326             10285112                 5708  0111910 1112 110 <E 100
14327             10285115                 5705  0111910 1112 <A 110 100
14328             10285121                 5699  0111910 <A 1112 110 100
14329             10285124                 5696  0111909 <B 1113 110 100
14330             10285125                 5697  0111909 B> 1113 110 100
14331             10285134                 5706  0111909 1113 B> 110 100
14332             10285137                 5709  0111909 1114 C> 100
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  110 <A 1117+V(1)
    1                    3                    1  111 B> 1117+V(1)
    2            24+3*V(1)            22+3*V(1)  1118+V(1) B>
    3            29+3*V(1)            21+3*V(1)  1118+V(1) <A 101
    4            53+6*V(1)                   -3  <A 1118+V(1) 101
    5            56+6*V(1)                   -2  011 D> 1118+V(1) 101
    6            80+9*V(1)            22+3*V(1)  0119+V(1) D> 101
    7            83+9*V(1)            21+3*V(1)  0119+V(1) <B 101
    8            84+9*V(1)            22+3*V(1)  0119+V(1) B> 101
    9            87+9*V(1)            25+3*V(1)  0119+V(1) 111 D>
   10            88+9*V(1)            24+3*V(1)  0119+V(1) 111 <A 100
   11            91+9*V(1)            21+3*V(1)  0119+V(1) <A 111 100
   12            94+9*V(1)            18+3*V(1)  0118+V(1) <B 1112 100
   13            95+9*V(1)            19+3*V(1)  0118+V(1) B> 1112 100
   14           101+9*V(1)            25+3*V(1)  0118+V(1) 1112 B> 100
   15           104+9*V(1)            28+3*V(1)  0118+V(1) 1112 110 F>
   16           105+9*V(1)            27+3*V(1)  0118+V(1) 1112 110 <E 100
   17           108+9*V(1)            24+3*V(1)  0118+V(1) 1112 <A 110 100
   18           114+9*V(1)            18+3*V(1)  0118+V(1) <A 1112 110 100
   19           117+9*V(1)            15+3*V(1)  0117+V(1) <B 1113 110 100
   20           118+9*V(1)            16+3*V(1)  0117+V(1) B> 1113 110 100
   21           127+9*V(1)            25+3*V(1)  0117+V(1) 1113 B> 110 100
   22           130+9*V(1)            28+3*V(1)  0117+V(1) 1114 C> 100
<< Success! ==> defined new CTR 11 (PPA)
14332             10285137                 5709  0111909 1114 C> 100
== Executing  PA-CTR  2, V(1)=3, V(2)=1902, repcount=318, factor=10/6
25462             28548513                 9525  011 1113184 C> 100
25463             28548516                 9524  011 1113184 <A 110
25464             28558068                  -28  011 <A 1113184 110
25465             28558071                  -31  <B 1113185 110
25466             28558072                  -30  001 C> 1113185 110
25467             28567627                 9525  001 1013185 C> 110
25468             28567634                 9528  001 1013185 111 C>
25469             28567637                 9527  001 1013185 111 <A 010
25470             28567640                 9524  001 1013185 <A 111 010
25471             28567645                 9525  001 1013184 111 B> 111 010
25472             28567648                 9528  001 1013184 1112 B> 010
25473             28567653                 9527  001 1013184 1112 <A 111
25474             28567659                 9521  001 1013184 <A 1113
25475             28567664                 9522  001 1013183 111 B> 1113
25476             28567673                 9531  001 1013183 1114 B>
25477             28567678                 9530  001 1013183 1114 <A 101
25478             28567690                 9518  001 1013183 <A 1114 101
25479             28567695                 9519  001 1013182 111 B> 1114 101
25480             28567707                 9531  001 1013182 1115 B> 101
25481             28567710                 9534  001 1013182 1116 D>
25482             28567711                 9533  001 1013182 1116 <A 100
25483             28567729                 9515  001 1013182 <A 1116 100
25484             28567734                 9516  001 1013181 111 B> 1116 100
25485             28567752                 9534  001 1013181 1117 B> 100
25486             28567755                 9537  001 1013181 1117 110 F>
25487             28567756                 9536  001 1013181 1117 110 <E 100
25488             28567759                 9533  001 1013181 1117 <A 110 100
25489             28567780                 9512  001 1013181 <A 1117 110 100
25490             28567785                 9513  001 1013180 111 B> 1117 110 100
25491             28567806                 9534  001 1013180 1118 B> 110 100
25492             28567809                 9537  001 1013180 1119 C> 100
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  011 11111+V(1) C> 100
    1                    3                   -1  011 11111+V(1) <A 110
    2            36+3*V(1)          -34+-3*V(1)  011 <A 11111+V(1) 110
    3            39+3*V(1)          -37+-3*V(1)  <B 11112+V(1) 110
    4            40+3*V(1)          -36+-3*V(1)  001 C> 11112+V(1) 110
    5            76+6*V(1)                    0  001 10112+V(1) C> 110
    6            83+6*V(1)                    3  001 10112+V(1) 111 C>
    7            86+6*V(1)                    2  001 10112+V(1) 111 <A 010
    8            89+6*V(1)                   -1  001 10112+V(1) <A 111 010
    9            94+6*V(1)                    0  001 10111+V(1) 111 B> 111 010
   10            97+6*V(1)                    3  001 10111+V(1) 1112 B> 010
   11           102+6*V(1)                    2  001 10111+V(1) 1112 <A 111
   12           108+6*V(1)                   -4  001 10111+V(1) <A 1113
   13           113+6*V(1)                   -3  001 10110+V(1) 111 B> 1113
   14           122+6*V(1)                    6  001 10110+V(1) 1114 B>
   15           127+6*V(1)                    5  001 10110+V(1) 1114 <A 101
   16           139+6*V(1)                   -7  001 10110+V(1) <A 1114 101
   17           144+6*V(1)                   -6  001 1019+V(1) 111 B> 1114 101
   18           156+6*V(1)                    6  001 1019+V(1) 1115 B> 101
   19           159+6*V(1)                    9  001 1019+V(1) 1116 D>
   20           160+6*V(1)                    8  001 1019+V(1) 1116 <A 100
   21           178+6*V(1)                  -10  001 1019+V(1) <A 1116 100
   22           183+6*V(1)                   -9  001 1018+V(1) 111 B> 1116 100
   23           201+6*V(1)                    9  001 1018+V(1) 1117 B> 100
   24           204+6*V(1)                   12  001 1018+V(1) 1117 110 F>
   25           205+6*V(1)                   11  001 1018+V(1) 1117 110 <E 100
   26           208+6*V(1)                    8  001 1018+V(1) 1117 <A 110 100
   27           229+6*V(1)                  -13  001 1018+V(1) <A 1117 110 100
   28           234+6*V(1)                  -12  001 1017+V(1) 111 B> 1117 110 100
   29           255+6*V(1)                    9  001 1017+V(1) 1118 B> 110 100
   30           258+6*V(1)                   12  001 1017+V(1) 1119 C> 100
<< Success! ==> defined new CTR 12 (PPA)
25492             28567809                 9537  001 1013180 1119 C> 100
== Executing  PA-CTR  3, V(1)=8, V(2)=3173, repcount=529, factor=10/6
40833             79129629                15885  001 1016 1115299 C> 100
== Executing PPA-CTR  4 (once), V(1)=5298
40867             79352476                15896  1105310 <A 111
== Executing  PA-CTR  1, V(1)=5303, V(2)=0, repcount=884, factor=10/6
66503            220072900                  -16  1106 <A 1118841
66504            220072903                  -15  1105 111 B> 1118841
66505            220099426                26508  1105 1118842 B>
66506            220099431                26507  1105 1118842 <A 101
66507            220125957                  -19  1105 <A 1118842 101
66508            220125960                  -18  1104 111 B> 1118842 101
66509            220152486                26508  1104 1118843 B> 101
66510            220152489                26511  1104 1118844 D>
66511            220152490                26510  1104 1118844 <A 100
66512            220179022                  -22  1104 <A 1118844 100
66513            220179025                  -21  1103 111 B> 1118844 100
66514            220205557                26511  1103 1118845 B> 100
66515            220205560                26514  1103 1118845 110 F>
66516            220205561                26513  1103 1118845 110 <E 100
66517            220205564                26510  1103 1118845 <A 110 100
66518            220232099                  -25  1103 <A 1118845 110 100
66519            220232102                  -24  1102 111 B> 1118845 110 100
66520            220258637                26511  1102 1118846 B> 110 100
66521            220258640                26514  1102 1118847 C> 100
66522            220258643                26513  1102 1118847 <A 110
66523            220285184                  -28  1102 <A 1118847 110
66524            220285187                  -27  110 111 B> 1118847 110
66525            220311728                26514  110 1118848 B> 110
66526            220311731                26517  110 1118849 C>
66527            220311734                26516  110 1118849 <A 010
66528            220338281                  -31  110 <A 1118849 010
66529            220338284                  -30  111 B> 1118849 010
66530            220364831                26517  1118850 B> 010
66531            220364836                26516  1118850 <A 111
66532            220391386                  -34  <A 1118851
66533            220391389                  -33  011 D> 1118851
66534            220417942                26520  0118852 D>
66535            220417943                26519  0118852 <A 100
66536            220417946                26516  0118851 <B 111 100
66537            220417947                26517  0118851 B> 111 100
66538            220417950                26520  0118851 111 B> 100
66539            220417953                26523  0118851 111 110 F>
66540            220417954                26522  0118851 111 110 <E 100
66541            220417957                26519  0118851 111 <A 110 100
66542            220417960                26516  0118851 <A 111 110 100
66543            220417963                26513  0118850 <B 1112 110 100
66544            220417964                26514  0118850 B> 1112 110 100
66545            220417970                26520  0118850 1112 B> 110 100
66546            220417973                26523  0118850 1113 C> 100
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  1106 <A 1111+V(1)
    1                    3                    1  1105 111 B> 1111+V(1)
    2             6+3*V(1)             4+3*V(1)  1105 1112+V(1) B>
    3            11+3*V(1)             3+3*V(1)  1105 1112+V(1) <A 101
    4            17+6*V(1)                   -3  1105 <A 1112+V(1) 101
    5            20+6*V(1)                   -2  1104 111 B> 1112+V(1) 101
    6            26+9*V(1)             4+3*V(1)  1104 1113+V(1) B> 101
    7            29+9*V(1)             7+3*V(1)  1104 1114+V(1) D>
    8            30+9*V(1)             6+3*V(1)  1104 1114+V(1) <A 100
    9           42+12*V(1)                   -6  1104 <A 1114+V(1) 100
   10           45+12*V(1)                   -5  1103 111 B> 1114+V(1) 100
   11           57+15*V(1)             7+3*V(1)  1103 1115+V(1) B> 100
   12           60+15*V(1)            10+3*V(1)  1103 1115+V(1) 110 F>
   13           61+15*V(1)             9+3*V(1)  1103 1115+V(1) 110 <E 100
   14           64+15*V(1)             6+3*V(1)  1103 1115+V(1) <A 110 100
   15           79+18*V(1)                   -9  1103 <A 1115+V(1) 110 100
   16           82+18*V(1)                   -8  1102 111 B> 1115+V(1) 110 100
   17           97+21*V(1)             7+3*V(1)  1102 1116+V(1) B> 110 100
   18          100+21*V(1)            10+3*V(1)  1102 1117+V(1) C> 100
   19          103+21*V(1)             9+3*V(1)  1102 1117+V(1) <A 110
   20          124+24*V(1)                  -12  1102 <A 1117+V(1) 110
   21          127+24*V(1)                  -11  110 111 B> 1117+V(1) 110
   22          148+27*V(1)            10+3*V(1)  110 1118+V(1) B> 110
   23          151+27*V(1)            13+3*V(1)  110 1119+V(1) C>
   24          154+27*V(1)            12+3*V(1)  110 1119+V(1) <A 010
   25          181+30*V(1)                  -15  110 <A 1119+V(1) 010
   26          184+30*V(1)                  -14  111 B> 1119+V(1) 010
   27          211+33*V(1)            13+3*V(1)  11110+V(1) B> 010
   28          216+33*V(1)            12+3*V(1)  11110+V(1) <A 111
   29          246+36*V(1)                  -18  <A 11111+V(1)
   30          249+36*V(1)                  -17  011 D> 11111+V(1)
   31          282+39*V(1)            16+3*V(1)  01112+V(1) D>
   32          283+39*V(1)            15+3*V(1)  01112+V(1) <A 100
   33          286+39*V(1)            12+3*V(1)  01111+V(1) <B 111 100
   34          287+39*V(1)            13+3*V(1)  01111+V(1) B> 111 100
   35          290+39*V(1)            16+3*V(1)  01111+V(1) 111 B> 100
   36          293+39*V(1)            19+3*V(1)  01111+V(1) 111 110 F>
   37          294+39*V(1)            18+3*V(1)  01111+V(1) 111 110 <E 100
   38          297+39*V(1)            15+3*V(1)  01111+V(1) 111 <A 110 100
   39          300+39*V(1)            12+3*V(1)  01111+V(1) <A 111 110 100
   40          303+39*V(1)             9+3*V(1)  01110+V(1) <B 1112 110 100
   41          304+39*V(1)            10+3*V(1)  01110+V(1) B> 1112 110 100
   42          310+39*V(1)            16+3*V(1)  01110+V(1) 1112 B> 110 100
   43          313+39*V(1)            19+3*V(1)  01110+V(1) 1113 C> 100
<< Success! ==> defined new CTR 13 (PPA)
66546            220417973                26523  0118850 1113 C> 100
== Executing  PA-CTR  2, V(1)=2, V(2)=8843, repcount=1474, factor=10/6
118136            611729597                44211  0116 11114743 C> 100
118137            611729600                44210  0116 11114743 <A 110
118138            611773829                  -19  0116 <A 11114743 110
118139            611773832                  -22  0115 <B 11114744 110
118140            611773833                  -21  0115 B> 11114744 110
118141            611818065                44211  0115 11114744 B> 110
118142            611818068                44214  0115 11114745 C>
118143            611818071                44213  0115 11114745 <A 010
118144            611862306                  -22  0115 <A 11114745 010
118145            611862309                  -25  0114 <B 11114746 010
118146            611862310                  -24  0114 B> 11114746 010
118147            611906548                44214  0114 11114746 B> 010
118148            611906553                44213  0114 11114746 <A 111
118149            611950791                  -25  0114 <A 11114747
118150            611950794                  -28  0113 <B 11114748
118151            611950795                  -27  0113 B> 11114748
118152            611995039                44217  0113 11114748 B>
118153            611995044                44216  0113 11114748 <A 101
118154            612039288                  -28  0113 <A 11114748 101
118155            612039291                  -31  0112 <B 11114749 101
118156            612039292                  -30  0112 B> 11114749 101
118157            612083539                44217  0112 11114749 B> 101
118158            612083542                44220  0112 11114750 D>
118159            612083543                44219  0112 11114750 <A 100
118160            612127793                  -31  0112 <A 11114750 100
118161            612127796                  -34  011 <B 11114751 100
118162            612127797                  -33  011 B> 11114751 100
118163            612172050                44220  011 11114751 B> 100
118164            612172053                44223  011 11114751 110 F>
118165            612172054                44222  011 11114751 110 <E 100
118166            612172057                44219  011 11114751 <A 110 100
118167            612216310                  -34  011 <A 11114751 110 100
118168            612216313                  -37  <B 11114752 110 100
118169            612216314                  -36  001 C> 11114752 110 100
118170            612260570                44220  001 10114752 C> 110 100
118171            612260577                44223  001 10114752 111 C> 100
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  0116 1111+V(1) C> 100
    1                    3                   -1  0116 1111+V(1) <A 110
    2             6+3*V(1)           -4+-3*V(1)  0116 <A 1111+V(1) 110
    3             9+3*V(1)           -7+-3*V(1)  0115 <B 1112+V(1) 110
    4            10+3*V(1)           -6+-3*V(1)  0115 B> 1112+V(1) 110
    5            16+6*V(1)                    0  0115 1112+V(1) B> 110
    6            19+6*V(1)                    3  0115 1113+V(1) C>
    7            22+6*V(1)                    2  0115 1113+V(1) <A 010
    8            31+9*V(1)           -7+-3*V(1)  0115 <A 1113+V(1) 010
    9            34+9*V(1)          -10+-3*V(1)  0114 <B 1114+V(1) 010
   10            35+9*V(1)           -9+-3*V(1)  0114 B> 1114+V(1) 010
   11           47+12*V(1)                    3  0114 1114+V(1) B> 010
   12           52+12*V(1)                    2  0114 1114+V(1) <A 111
   13           64+15*V(1)          -10+-3*V(1)  0114 <A 1115+V(1)
   14           67+15*V(1)          -13+-3*V(1)  0113 <B 1116+V(1)
   15           68+15*V(1)          -12+-3*V(1)  0113 B> 1116+V(1)
   16           86+18*V(1)                    6  0113 1116+V(1) B>
   17           91+18*V(1)                    5  0113 1116+V(1) <A 101
   18          109+21*V(1)          -13+-3*V(1)  0113 <A 1116+V(1) 101
   19          112+21*V(1)          -16+-3*V(1)  0112 <B 1117+V(1) 101
   20          113+21*V(1)          -15+-3*V(1)  0112 B> 1117+V(1) 101
   21          134+24*V(1)                    6  0112 1117+V(1) B> 101
   22          137+24*V(1)                    9  0112 1118+V(1) D>
   23          138+24*V(1)                    8  0112 1118+V(1) <A 100
   24          162+27*V(1)          -16+-3*V(1)  0112 <A 1118+V(1) 100
   25          165+27*V(1)          -19+-3*V(1)  011 <B 1119+V(1) 100
   26          166+27*V(1)          -18+-3*V(1)  011 B> 1119+V(1) 100
   27          193+30*V(1)                    9  011 1119+V(1) B> 100
   28          196+30*V(1)                   12  011 1119+V(1) 110 F>
   29          197+30*V(1)                   11  011 1119+V(1) 110 <E 100
   30          200+30*V(1)                    8  011 1119+V(1) <A 110 100
   31          227+33*V(1)          -19+-3*V(1)  011 <A 1119+V(1) 110 100
   32          230+33*V(1)          -22+-3*V(1)  <B 11110+V(1) 110 100
   33          231+33*V(1)          -21+-3*V(1)  001 C> 11110+V(1) 110 100
   34          261+36*V(1)                    9  001 10110+V(1) C> 110 100
   35          268+36*V(1)                   12  001 10110+V(1) 111 C> 100
<< Success! ==> defined new CTR 14 (PPA)
118171            612260577                44223  001 10114752 111 C> 100
== Executing  PA-CTR  3, V(1)=0, V(2)=14745, repcount=2458, factor=10/6
189453           1699955073                73719  001 1014 11124581 C> 100
== Executing PPA-CTR 10 (once), V(1)=24577
189500           1700692830                73712  11024584 <A 1119
== Executing  PA-CTR  1, V(1)=24577, V(2)=8, repcount=4097, factor=10/6
308313           4723516788                  -34  1102 <A 11140979
== Executing PPA-CTR  8 (once), V(1)=40975
308333           4724131536               122910  01140982 1112 C> 100
== Executing  PA-CTR  2, V(1)=1, V(2)=40975, repcount=6830, factor=10/6
547383          13121753136               204870  0112 11168302 C> 100
547384          13121753139               204869  0112 11168302 <A 110
547385          13121958045                  -37  0112 <A 11168302 110
547386          13121958048                  -40  011 <B 11168303 110
547387          13121958049                  -39  011 B> 11168303 110
547388          13122162958               204870  011 11168303 B> 110
547389          13122162961               204873  011 11168304 C>
547390          13122162964               204872  011 11168304 <A 010
547391          13122367876                  -40  011 <A 11168304 010
547392          13122367879                  -43  <B 11168305 010
547393          13122367880                  -42  001 C> 11168305 010
547394          13122572795               204873  001 10168305 C> 010
547395          13122572797               204873  001 10168305 H> 010   [stop]

Lines:       634
Top steps:   633
Macro steps: 547395
Basic steps: 13122572797
Tape index:  204873
ones:        136612
log10(ones    ):    5.135
log10(steps   ):   10.118
Run state:   stop

The same TM just simple.
The same TM with repetitions reduced.
The same TM with tape symbol exponents.
The same TM as 3-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
    5T B1L A1L C1R B1R F0R D1R A1L E0R A0L C1R E1L H1L :   136612      13122572797
    T TM #7 from MaBu90-Paper
    M	740
    pref	sim
    machv mbP_7  	just simple
    machv mbP_7-r	with repetitions reduced
    machv mbP_7-1	with tape symbol exponents
    machv mbP_7-m	as 3-macro machine
    machv mbP_7-a	as 3-macro machine with pure additive config-TRs
    iam	mbP_7-a
    mtype	3
    mmtyp	3
    r	1
    H	1
    mac	0
    E	2
    sympr	
    HM	1
    date	Tue Jul  6 22:10:11 CEST 2010
    edate	Tue Jul  6 22:10:14 CEST 2010
    bnspeed	1

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