6-state TM #d from MaBu-List

Comment: This TM produces 5234513991 ones in 93943325529148987897 steps.

State on
0
on
1
on 0 on 1
Print Move Goto Print Move Goto
A B1R B0L 1 right B 0 left B
B A1L C1L 1 left A 1 left C
C B1L D0R 1 left B 0 right D
D Z1R E1R 1 right Z 1 right E
E F1R A0R 1 right F 0 right A
F C0R C1L 0 right C 1 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-bck-macro machine.
Simulation is done as 2-bck-bck-macro machine with pure additive config-TRs.

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

Steps             BasSteps              BasTpos  Tape contents
    0                    0                    0  (00)(00)A>
    1                   12                    2  (01)(01)E>
    2                   14                    4  01 (01)(10)C>
    3                   19                   -1  01 <B(11)(01) 10
    4                   21                   -3  <B(11)(11) 01 10
    5                   31                   -5  <A(10)(10) 11 01 10
    6                   40                    0  (10)(11)F> 11 01 10
    7                   44                    2  10 (10)(10)A> 01 10
    8                   48                    4  102 (10)(01)E> 10
    9                   50                    6  103 (01)(01)B>
   10                   55                    1  103 <A(10)(10) 10
   11                   64                    6  103 (10)(11)F> 10
   12                   68                    8  104 (10)(11)F>
   13                   75                    3  104 <C(11)(10) 11
   14                   77                    1  103 <C(11)(11) 10 11
   15                   83                   -5  <C(11)(11) 113 10 11
   16                   85                   -7  <A(11)(11) 114 10 11
   17                  106                   -2  01 (01)(01)E> 114 10 11
   18                  113                   -7  01 <A(10)(10) 10 113 10 11
   19                  115                   -9  <A(10)(10) 102 113 10 11
   20                  124                   -4  (10)(11)F> 102 113 10 11
   21                  132                    0  102 (10)(11)F> 113 10 11
   22                  136                    2  103 (10)(10)A> 112 10 11
   23                  141                   -3  103 <B(01)(01) 01 11 10 11
   24                  147                   -9  <B(01)(01) 014 11 10 11
   25                  160                   -4  01 (01)(01)E> 014 11 10 11
   26                  176                    4  015 (01)(01)E> 11 10 11
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  011+V(1) (01)(01)E> 114+V(2) [*]* [*]*
    1                    7                   -5  011+V(1) <A(10)(10) 10 113+V(2) [*]* [*]*
    2             9+2*V(1)           -7+-2*V(1)  <A(10)(10) 102+V(1) 113+V(2) [*]* [*]*
    3            18+2*V(1)           -2+-2*V(1)  (10)(11)F> 102+V(1) 113+V(2) [*]* [*]*
    4            26+6*V(1)                    2  102+V(1) (10)(11)F> 113+V(2) [*]* [*]*
    5            30+6*V(1)                    4  103+V(1) (10)(10)A> 112+V(2) [*]* [*]*
    6            35+6*V(1)                   -1  103+V(1) <B(01)(01) 01 111+V(2) [*]* [*]*
    7            41+8*V(1)           -7+-2*V(1)  <B(01)(01) 014+V(1) 111+V(2) [*]* [*]*
    8            54+8*V(1)           -2+-2*V(1)  01 (01)(01)E> 014+V(1) 111+V(2) [*]* [*]*
    9           70+12*V(1)                    6  015+V(1) (01)(01)E> 111+V(2) [*]* [*]*
<< Success! ==> defined new CTR 1 (PA)
   27                  183                   -1  015 <A(10)(10) 102 11
   28                  193                  -11  <A(10)(10) 107 11
   29                  202                   -6  (10)(11)F> 107 11
   30                  230                    8  107 (10)(11)F> 11
   31                  234                   10  108 (10)(10)A>
   32                  241                    5  108 <B(01)(01) 01
   33                  257                  -11  <B(01)(01) 019
   34                  270                   -6  01 (01)(01)E> 019
   35                  306                   12  0110 (01)(01)E>
   36                  308                   14  0111 (01)(10)C>
   37                  313                    9  0111 <B(11)(01) 10
   38                  315                    7  0110 <B(11)(11) 01 10
   39                  335                  -13  <B(11)(11) 1110 01 10
   40                  345                  -15  <A(10)(10) 1111 01 10
   41                  354                  -10  (10)(11)F> 1111 01 10
   42                  358                   -8  10 (10)(10)A> 1110 01 10
   43                  363                  -13  10 <B(01)(01) 01 119 01 10
   44                  365                  -15  <B(01)(01) 012 119 01 10
   45                  378                  -10  01 (01)(01)E> 012 119 01 10
   46                  386                   -6  013 (01)(01)E> 119 01 10
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  011+V(1) (01)(01)E> 11 101+V(2) 11
    1                    7                   -5  011+V(1) <A(10)(10) 102+V(2) 11
    2             9+2*V(1)           -7+-2*V(1)  <A(10)(10) 103+V(1)+V(2) 11
    3            18+2*V(1)           -2+-2*V(1)  (10)(11)F> 103+V(1)+V(2) 11
    4     30+6*V(1)+4*V(2)             4+2*V(2)  103+V(1)+V(2) (10)(11)F> 11
    5     34+6*V(1)+4*V(2)             6+2*V(2)  104+V(1)+V(2) (10)(10)A>
    6     41+6*V(1)+4*V(2)             1+2*V(2)  104+V(1)+V(2) <B(01)(01) 01
    7     49+8*V(1)+6*V(2)           -7+-2*V(1)  <B(01)(01) 015+V(1)+V(2)
    8     62+8*V(1)+6*V(2)           -2+-2*V(1)  01 (01)(01)E> 015+V(1)+V(2)
    9   82+12*V(1)+10*V(2)             8+2*V(2)  016+V(1)+V(2) (01)(01)E>
   10   84+12*V(1)+10*V(2)            10+2*V(2)  017+V(1)+V(2) (01)(10)C>
   11   89+12*V(1)+10*V(2)             5+2*V(2)  017+V(1)+V(2) <B(11)(01) 10
   12   91+12*V(1)+10*V(2)             3+2*V(2)  016+V(1)+V(2) <B(11)(11) 01 10
   13  103+14*V(1)+12*V(2)           -9+-2*V(1)  <B(11)(11) 116+V(1)+V(2) 01 10
   14  113+14*V(1)+12*V(2)          -11+-2*V(1)  <A(10)(10) 117+V(1)+V(2) 01 10
   15  122+14*V(1)+12*V(2)           -6+-2*V(1)  (10)(11)F> 117+V(1)+V(2) 01 10
   16  126+14*V(1)+12*V(2)           -4+-2*V(1)  10 (10)(10)A> 116+V(1)+V(2) 01 10
   17  131+14*V(1)+12*V(2)           -9+-2*V(1)  10 <B(01)(01) 01 115+V(1)+V(2) 01 10
   18  133+14*V(1)+12*V(2)          -11+-2*V(1)  <B(01)(01) 012 115+V(1)+V(2) 01 10
   19  146+14*V(1)+12*V(2)           -6+-2*V(1)  01 (01)(01)E> 012 115+V(1)+V(2) 01 10
   20  154+14*V(1)+12*V(2)           -2+-2*V(1)  013 (01)(01)E> 115+V(1)+V(2) 01 10
<< Success! ==> defined new CTR 2 (PPA)
   46                  386                   -6  013 (01)(01)E> 119 01 10
== Executing  PA-CTR  1, V(1)=2, V(2)=5, repcount=2, factor=4/3
   64                  622                    6  0111 (01)(01)E> 113 01 10
   65                  629                    1  0111 <A(10)(10) 10 112 01 10
   66                  651                  -21  <A(10)(10) 1012 112 01 10
   67                  660                  -16  (10)(11)F> 1012 112 01 10
   68                  708                    8  1012 (10)(11)F> 112 01 10
   69                  712                   10  1013 (10)(10)A> 11 01 10
   70                  717                    5  1013 <B(01)(01) 012 10
   71                  743                  -21  <B(01)(01) 0115 10
   72                  756                  -16  01 (01)(01)E> 0115 10
   73                  816                   14  0116 (01)(01)E> 10
   74                  818                   16  0117 (01)(01)B>
   75                  823                   11  0117 <A(10)(10) 10
   76                  857                  -23  <A(10)(10) 1018
   77                  866                  -18  (10)(11)F> 1018
   78                  938                   18  1018 (10)(11)F>
   79                  945                   13  1018 <C(11)(10) 11
   80                  947                   11  1017 <C(11)(11) 10 11
   81                  981                  -23  <C(11)(11) 1117 10 11
   82                  983                  -25  <A(11)(11) 1118 10 11
   83                 1004                  -20  01 (01)(01)E> 1118 10 11
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  011+V(1) (01)(01)E> 113 011+V(2) 10
    1                    7                   -5  011+V(1) <A(10)(10) 10 112 011+V(2) 10
    2             9+2*V(1)           -7+-2*V(1)  <A(10)(10) 102+V(1) 112 011+V(2) 10
    3            18+2*V(1)           -2+-2*V(1)  (10)(11)F> 102+V(1) 112 011+V(2) 10
    4            26+6*V(1)                    2  102+V(1) (10)(11)F> 112 011+V(2) 10
    5            30+6*V(1)                    4  103+V(1) (10)(10)A> 11 011+V(2) 10
    6            35+6*V(1)                   -1  103+V(1) <B(01)(01) 012+V(2) 10
    7            41+8*V(1)           -7+-2*V(1)  <B(01)(01) 015+V(1)+V(2) 10
    8            54+8*V(1)           -2+-2*V(1)  01 (01)(01)E> 015+V(1)+V(2) 10
    9    74+12*V(1)+4*V(2)             8+2*V(2)  016+V(1)+V(2) (01)(01)E> 10
   10    76+12*V(1)+4*V(2)            10+2*V(2)  017+V(1)+V(2) (01)(01)B>
   11    81+12*V(1)+4*V(2)             5+2*V(2)  017+V(1)+V(2) <A(10)(10) 10
   12    95+14*V(1)+6*V(2)           -9+-2*V(1)  <A(10)(10) 108+V(1)+V(2)
   13   104+14*V(1)+6*V(2)           -4+-2*V(1)  (10)(11)F> 108+V(1)+V(2)
   14  136+18*V(1)+10*V(2)            12+2*V(2)  108+V(1)+V(2) (10)(11)F>
   15  143+18*V(1)+10*V(2)             7+2*V(2)  108+V(1)+V(2) <C(11)(10) 11
   16  145+18*V(1)+10*V(2)             5+2*V(2)  107+V(1)+V(2) <C(11)(11) 10 11
   17  159+20*V(1)+12*V(2)           -9+-2*V(1)  <C(11)(11) 117+V(1)+V(2) 10 11
   18  161+20*V(1)+12*V(2)          -11+-2*V(1)  <A(11)(11) 118+V(1)+V(2) 10 11
   19  182+20*V(1)+12*V(2)           -6+-2*V(1)  01 (01)(01)E> 118+V(1)+V(2) 10 11
<< Success! ==> defined new CTR 3 (PPA)
   83                 1004                  -20  01 (01)(01)E> 1118 10 11
== Executing  PA-CTR  1, V(1)=0, V(2)=14, repcount=5, factor=4/3
  128                 1834                   10  0121 (01)(01)E> 113 10 11
  129                 1841                    5  0121 <A(10)(10) 10 112 10 11
  130                 1883                  -37  <A(10)(10) 1022 112 10 11
  131                 1892                  -32  (10)(11)F> 1022 112 10 11
  132                 1980                   12  1022 (10)(11)F> 112 10 11
  133                 1984                   14  1023 (10)(10)A> 11 10 11
  134                 1989                    9  1023 <B(01)(01) 01 10 11
  135                 2035                  -37  <B(01)(01) 0124 10 11
  136                 2048                  -32  01 (01)(01)E> 0124 10 11
  137                 2144                   16  0125 (01)(01)E> 10 11
  138                 2146                   18  0126 (01)(01)B> 11
  139                 2150                   20  0127 (00)(10)A>
  140                 2168                   22  0128 (01)(01)E>
  141                 2170                   24  0129 (01)(10)C>
  142                 2175                   19  0129 <B(11)(01) 10
  143                 2177                   17  0128 <B(11)(11) 01 10
  144                 2233                  -39  <B(11)(11) 1128 01 10
  145                 2243                  -41  <A(10)(10) 1129 01 10
  146                 2252                  -36  (10)(11)F> 1129 01 10
  147                 2256                  -34  10 (10)(10)A> 1128 01 10
  148                 2261                  -39  10 <B(01)(01) 01 1127 01 10
  149                 2263                  -41  <B(01)(01) 012 1127 01 10
  150                 2276                  -36  01 (01)(01)E> 012 1127 01 10
  151                 2284                  -32  013 (01)(01)E> 1127 01 10
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  011+V(1) (01)(01)E> 113 10 11
    1                    7                   -5  011+V(1) <A(10)(10) 10 112 10 11
    2             9+2*V(1)           -7+-2*V(1)  <A(10)(10) 102+V(1) 112 10 11
    3            18+2*V(1)           -2+-2*V(1)  (10)(11)F> 102+V(1) 112 10 11
    4            26+6*V(1)                    2  102+V(1) (10)(11)F> 112 10 11
    5            30+6*V(1)                    4  103+V(1) (10)(10)A> 11 10 11
    6            35+6*V(1)                   -1  103+V(1) <B(01)(01) 01 10 11
    7            41+8*V(1)           -7+-2*V(1)  <B(01)(01) 014+V(1) 10 11
    8            54+8*V(1)           -2+-2*V(1)  01 (01)(01)E> 014+V(1) 10 11
    9           70+12*V(1)                    6  015+V(1) (01)(01)E> 10 11
   10           72+12*V(1)                    8  016+V(1) (01)(01)B> 11
   11           76+12*V(1)                   10  017+V(1) (00)(10)A>
   12           94+12*V(1)                   12  018+V(1) (01)(01)E>
   13           96+12*V(1)                   14  019+V(1) (01)(10)C>
   14          101+12*V(1)                    9  019+V(1) <B(11)(01) 10
   15          103+12*V(1)                    7  018+V(1) <B(11)(11) 01 10
   16          119+14*V(1)           -9+-2*V(1)  <B(11)(11) 118+V(1) 01 10
   17          129+14*V(1)          -11+-2*V(1)  <A(10)(10) 119+V(1) 01 10
   18          138+14*V(1)           -6+-2*V(1)  (10)(11)F> 119+V(1) 01 10
   19          142+14*V(1)           -4+-2*V(1)  10 (10)(10)A> 118+V(1) 01 10
   20          147+14*V(1)           -9+-2*V(1)  10 <B(01)(01) 01 117+V(1) 01 10
   21          149+14*V(1)          -11+-2*V(1)  <B(01)(01) 012 117+V(1) 01 10
   22          162+14*V(1)           -6+-2*V(1)  01 (01)(01)E> 012 117+V(1) 01 10
   23          170+14*V(1)           -2+-2*V(1)  013 (01)(01)E> 117+V(1) 01 10
<< Success! ==> defined new CTR 4 (PPA)
  151                 2284                  -32  013 (01)(01)E> 1127 01 10
== Executing  PA-CTR  1, V(1)=2, V(2)=23, repcount=8, factor=4/3
  223                 4380                   16  0135 (01)(01)E> 113 01 10
== Executing PPA-CTR  3 (once), V(1)=34, V(2)=0
  242                 5242                  -58  01 (01)(01)E> 1142 10 11
== Executing  PA-CTR  1, V(1)=0, V(2)=38, repcount=13, factor=4/3
  359                 9896                   20  0153 (01)(01)E> 113 10 11
== Executing PPA-CTR  4 (once), V(1)=52
  382                10794                  -86  013 (01)(01)E> 1159 01 10
== Executing  PA-CTR  1, V(1)=2, V(2)=55, repcount=19, factor=4/3
  553                20788                   28  0179 (01)(01)E> 112 01 10
  554                20795                   23  0179 <A(10)(10) 10 11 01 10
  555                20953                 -135  <A(10)(10) 1080 11 01 10
  556                20962                 -130  (10)(11)F> 1080 11 01 10
  557                21282                   30  1080 (10)(11)F> 11 01 10
  558                21286                   32  1081 (10)(10)A> 01 10
  559                21290                   34  1082 (10)(01)E> 10
  560                21292                   36  1083 (01)(01)B>
  561                21297                   31  1083 <A(10)(10) 10
  562                21306                   36  1083 (10)(11)F> 10
  563                21310                   38  1084 (10)(11)F>
  564                21317                   33  1084 <C(11)(10) 11
  565                21319                   31  1083 <C(11)(11) 10 11
  566                21485                 -135  <C(11)(11) 1183 10 11
  567                21487                 -137  <A(11)(11) 1184 10 11
  568                21508                 -132  01 (01)(01)E> 1184 10 11
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  011+V(1) (01)(01)E> 112 01 10
    1                    7                   -5  011+V(1) <A(10)(10) 10 11 01 10
    2             9+2*V(1)           -7+-2*V(1)  <A(10)(10) 102+V(1) 11 01 10
    3            18+2*V(1)           -2+-2*V(1)  (10)(11)F> 102+V(1) 11 01 10
    4            26+6*V(1)                    2  102+V(1) (10)(11)F> 11 01 10
    5            30+6*V(1)                    4  103+V(1) (10)(10)A> 01 10
    6            34+6*V(1)                    6  104+V(1) (10)(01)E> 10
    7            36+6*V(1)                    8  105+V(1) (01)(01)B>
    8            41+6*V(1)                    3  105+V(1) <A(10)(10) 10
    9            50+6*V(1)                    8  105+V(1) (10)(11)F> 10
   10            54+6*V(1)                   10  106+V(1) (10)(11)F>
   11            61+6*V(1)                    5  106+V(1) <C(11)(10) 11
   12            63+6*V(1)                    3  105+V(1) <C(11)(11) 10 11
   13            73+8*V(1)           -7+-2*V(1)  <C(11)(11) 115+V(1) 10 11
   14            75+8*V(1)           -9+-2*V(1)  <A(11)(11) 116+V(1) 10 11
   15            96+8*V(1)           -4+-2*V(1)  01 (01)(01)E> 116+V(1) 10 11
<< Success! ==> defined new CTR 5 (PPA)
  568                21508                 -132  01 (01)(01)E> 1184 10 11
== Executing  PA-CTR  1, V(1)=0, V(2)=80, repcount=27, factor=4/3
  811                40246                   30  01109 (01)(01)E> 113 10 11
== Executing PPA-CTR  4 (once), V(1)=108
  834                41928                 -188  013 (01)(01)E> 11115 01 10
== Executing  PA-CTR  1, V(1)=2, V(2)=111, repcount=38, factor=4/3
 1176                79244                   40  01155 (01)(01)E> 11 01 10
 1177                79251                   35  01155 <A(10)(10) 10 01 10
 1178                79561                 -275  <A(10)(10) 10156 01 10
 1179                79570                 -270  (10)(11)F> 10156 01 10
 1180                80194                   42  10156 (10)(11)F> 01 10
 1181                80196                   44  10157 (11)(00)D> 10
 1182                80198                   46  10157 11 (00)(11)F>
 1183                80205                   41  10157 11 <A(11)(10) 11
 1184                80207                   39  10157 <C(10)(11) 10 11
 1185                80209                   37  10156 <C(11)(10) 11 10 11
 1186                80211                   35  10155 <C(11)(11) 10 11 10 11
 1187                80521                 -275  <C(11)(11) 11155 10 11 10 11
 1188                80523                 -277  <A(11)(11) 11156 10 11 10 11
 1189                80544                 -272  01 (01)(01)E> 11156 10 11 10 11
 1190                80551                 -277  01 <A(10)(10) 10 11155 10 11 10 11
 1191                80553                 -279  <A(10)(10) 102 11155 10 11 10 11
 1192                80562                 -274  (10)(11)F> 102 11155 10 11 10 11
 1193                80570                 -270  102 (10)(11)F> 11155 10 11 10 11
 1194                80574                 -268  103 (10)(10)A> 11154 10 11 10 11
 1195                80579                 -273  103 <B(01)(01) 01 11153 10 11 10 11
 1196                80585                 -279  <B(01)(01) 014 11153 10 11 10 11
 1197                80598                 -274  01 (01)(01)E> 014 11153 10 11 10 11
 1198                80614                 -266  015 (01)(01)E> 11153 10 11 10 11
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  011+V(1) (01)(01)E> 114+V(2) [*]* [*]* [*]* [*]*
    1                    7                   -5  011+V(1) <A(10)(10) 10 113+V(2) [*]* [*]* [*]* [*]*
    2             9+2*V(1)           -7+-2*V(1)  <A(10)(10) 102+V(1) 113+V(2) [*]* [*]* [*]* [*]*
    3            18+2*V(1)           -2+-2*V(1)  (10)(11)F> 102+V(1) 113+V(2) [*]* [*]* [*]* [*]*
    4            26+6*V(1)                    2  102+V(1) (10)(11)F> 113+V(2) [*]* [*]* [*]* [*]*
    5            30+6*V(1)                    4  103+V(1) (10)(10)A> 112+V(2) [*]* [*]* [*]* [*]*
    6            35+6*V(1)                   -1  103+V(1) <B(01)(01) 01 111+V(2) [*]* [*]* [*]* [*]*
    7            41+8*V(1)           -7+-2*V(1)  <B(01)(01) 014+V(1) 111+V(2) [*]* [*]* [*]* [*]*
    8            54+8*V(1)           -2+-2*V(1)  01 (01)(01)E> 014+V(1) 111+V(2) [*]* [*]* [*]* [*]*
    9           70+12*V(1)                    6  015+V(1) (01)(01)E> 111+V(2) [*]* [*]* [*]* [*]*
<< Success! ==> defined new CTR 6 (PA)
 1198                80614                 -266  015 (01)(01)E> 11153 10 11 10 11
== Executing  PA-CTR  6, V(1)=4, V(2)=149, repcount=50, factor=4/3
 1648               145314                   34  01205 (01)(01)E> 113 10 11 10 11
 1649               145321                   29  01205 <A(10)(10) 10 112 10 11 10 11
 1650               145731                 -381  <A(10)(10) 10206 112 10 11 10 11
 1651               145740                 -376  (10)(11)F> 10206 112 10 11 10 11
 1652               146564                   36  10206 (10)(11)F> 112 10 11 10 11
 1653               146568                   38  10207 (10)(10)A> 11 10 11 10 11
 1654               146573                   33  10207 <B(01)(01) 01 10 11 10 11
 1655               146987                 -381  <B(01)(01) 01208 10 11 10 11
 1656               147000                 -376  01 (01)(01)E> 01208 10 11 10 11
 1657               147832                   40  01209 (01)(01)E> 10 11 10 11
 1658               147834                   42  01210 (01)(01)B> 11 10 11
 1659               147838                   44  01211 (00)(10)A> 10 11
 1660               147852                   46  01212 (01)(10)C> 11
 1661               147854                   48  01213 (10)(01)E>
 1662               147856                   50  01213 10 (01)(10)C>
 1663               147861                   45  01213 10 <B(11)(01) 10
 1664               147863                   43  01213 <B(01)(11) 01 10
 1665               147865                   41  01212 <B(11)(01) 11 01 10
 1666               147867                   39  01211 <B(11)(11) 01 11 01 10
 1667               148289                 -383  <B(11)(11) 11211 01 11 01 10
 1668               148299                 -385  <A(10)(10) 11212 01 11 01 10
 1669               148308                 -380  (10)(11)F> 11212 01 11 01 10
 1670               148312                 -378  10 (10)(10)A> 11211 01 11 01 10
 1671               148317                 -383  10 <B(01)(01) 01 11210 01 11 01 10
 1672               148319                 -385  <B(01)(01) 012 11210 01 11 01 10
 1673               148332                 -380  01 (01)(01)E> 012 11210 01 11 01 10
 1674               148340                 -376  013 (01)(01)E> 11210 01 11 01 10
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  011+V(1) (01)(01)E> 113 10 11 10 11
    1                    7                   -5  011+V(1) <A(10)(10) 10 112 10 11 10 11
    2             9+2*V(1)           -7+-2*V(1)  <A(10)(10) 102+V(1) 112 10 11 10 11
    3            18+2*V(1)           -2+-2*V(1)  (10)(11)F> 102+V(1) 112 10 11 10 11
    4            26+6*V(1)                    2  102+V(1) (10)(11)F> 112 10 11 10 11
    5            30+6*V(1)                    4  103+V(1) (10)(10)A> 11 10 11 10 11
    6            35+6*V(1)                   -1  103+V(1) <B(01)(01) 01 10 11 10 11
    7            41+8*V(1)           -7+-2*V(1)  <B(01)(01) 014+V(1) 10 11 10 11
    8            54+8*V(1)           -2+-2*V(1)  01 (01)(01)E> 014+V(1) 10 11 10 11
    9           70+12*V(1)                    6  015+V(1) (01)(01)E> 10 11 10 11
   10           72+12*V(1)                    8  016+V(1) (01)(01)B> 11 10 11
   11           76+12*V(1)                   10  017+V(1) (00)(10)A> 10 11
   12           90+12*V(1)                   12  018+V(1) (01)(10)C> 11
   13           92+12*V(1)                   14  019+V(1) (10)(01)E>
   14           94+12*V(1)                   16  019+V(1) 10 (01)(10)C>
   15           99+12*V(1)                   11  019+V(1) 10 <B(11)(01) 10
   16          101+12*V(1)                    9  019+V(1) <B(01)(11) 01 10
   17          103+12*V(1)                    7  018+V(1) <B(11)(01) 11 01 10
   18          105+12*V(1)                    5  017+V(1) <B(11)(11) 01 11 01 10
   19          119+14*V(1)           -9+-2*V(1)  <B(11)(11) 117+V(1) 01 11 01 10
   20          129+14*V(1)          -11+-2*V(1)  <A(10)(10) 118+V(1) 01 11 01 10
   21          138+14*V(1)           -6+-2*V(1)  (10)(11)F> 118+V(1) 01 11 01 10
   22          142+14*V(1)           -4+-2*V(1)  10 (10)(10)A> 117+V(1) 01 11 01 10
   23          147+14*V(1)           -9+-2*V(1)  10 <B(01)(01) 01 116+V(1) 01 11 01 10
   24          149+14*V(1)          -11+-2*V(1)  <B(01)(01) 012 116+V(1) 01 11 01 10
   25          162+14*V(1)           -6+-2*V(1)  01 (01)(01)E> 012 116+V(1) 01 11 01 10
   26          170+14*V(1)           -2+-2*V(1)  013 (01)(01)E> 116+V(1) 01 11 01 10
<< Success! ==> defined new CTR 7 (PPA)
 1674               148340                 -376  013 (01)(01)E> 11210 01 11 01 10
== Executing  PA-CTR  6, V(1)=2, V(2)=206, repcount=69, factor=4/3
 2295               267434                   38  01279 (01)(01)E> 113 01 11 01 10
 2296               267441                   33  01279 <A(10)(10) 10 112 01 11 01 10
 2297               267999                 -525  <A(10)(10) 10280 112 01 11 01 10
 2298               268008                 -520  (10)(11)F> 10280 112 01 11 01 10
 2299               269128                   40  10280 (10)(11)F> 112 01 11 01 10
 2300               269132                   42  10281 (10)(10)A> 11 01 11 01 10
 2301               269137                   37  10281 <B(01)(01) 012 11 01 10
 2302               269699                 -525  <B(01)(01) 01283 11 01 10
 2303               269712                 -520  01 (01)(01)E> 01283 11 01 10
 2304               270844                   46  01284 (01)(01)E> 11 01 10
 2305               270851                   41  01284 <A(10)(10) 10 01 10
 2306               271419                 -527  <A(10)(10) 10285 01 10
 2307               271428                 -522  (10)(11)F> 10285 01 10
 2308               272568                   48  10285 (10)(11)F> 01 10
 2309               272570                   50  10286 (11)(00)D> 10
 2310               272572                   52  10286 11 (00)(11)F>
 2311               272579                   47  10286 11 <A(11)(10) 11
 2312               272581                   45  10286 <C(10)(11) 10 11
 2313               272583                   43  10285 <C(11)(10) 11 10 11
 2314               272585                   41  10284 <C(11)(11) 10 11 10 11
 2315               273153                 -527  <C(11)(11) 11284 10 11 10 11
 2316               273155                 -529  <A(11)(11) 11285 10 11 10 11
 2317               273176                 -524  01 (01)(01)E> 11285 10 11 10 11
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  011+V(1) (01)(01)E> 113 011+V(2) 11 01 10
    1                    7                   -5  011+V(1) <A(10)(10) 10 112 011+V(2) 11 01 10
    2             9+2*V(1)           -7+-2*V(1)  <A(10)(10) 102+V(1) 112 011+V(2) 11 01 10
    3            18+2*V(1)           -2+-2*V(1)  (10)(11)F> 102+V(1) 112 011+V(2) 11 01 10
    4            26+6*V(1)                    2  102+V(1) (10)(11)F> 112 011+V(2) 11 01 10
    5            30+6*V(1)                    4  103+V(1) (10)(10)A> 11 011+V(2) 11 01 10
    6            35+6*V(1)                   -1  103+V(1) <B(01)(01) 012+V(2) 11 01 10
    7            41+8*V(1)           -7+-2*V(1)  <B(01)(01) 015+V(1)+V(2) 11 01 10
    8            54+8*V(1)           -2+-2*V(1)  01 (01)(01)E> 015+V(1)+V(2) 11 01 10
    9    74+12*V(1)+4*V(2)             8+2*V(2)  016+V(1)+V(2) (01)(01)E> 11 01 10
   10    81+12*V(1)+4*V(2)             3+2*V(2)  016+V(1)+V(2) <A(10)(10) 10 01 10
   11    93+14*V(1)+6*V(2)           -9+-2*V(1)  <A(10)(10) 107+V(1)+V(2) 01 10
   12   102+14*V(1)+6*V(2)           -4+-2*V(1)  (10)(11)F> 107+V(1)+V(2) 01 10
   13  130+18*V(1)+10*V(2)            10+2*V(2)  107+V(1)+V(2) (10)(11)F> 01 10
   14  132+18*V(1)+10*V(2)            12+2*V(2)  108+V(1)+V(2) (11)(00)D> 10
   15  134+18*V(1)+10*V(2)            14+2*V(2)  108+V(1)+V(2) 11 (00)(11)F>
   16  141+18*V(1)+10*V(2)             9+2*V(2)  108+V(1)+V(2) 11 <A(11)(10) 11
   17  143+18*V(1)+10*V(2)             7+2*V(2)  108+V(1)+V(2) <C(10)(11) 10 11
   18  145+18*V(1)+10*V(2)             5+2*V(2)  107+V(1)+V(2) <C(11)(10) 11 10 11
   19  147+18*V(1)+10*V(2)             3+2*V(2)  106+V(1)+V(2) <C(11)(11) 10 11 10 11
   20  159+20*V(1)+12*V(2)           -9+-2*V(1)  <C(11)(11) 116+V(1)+V(2) 10 11 10 11
   21  161+20*V(1)+12*V(2)          -11+-2*V(1)  <A(11)(11) 117+V(1)+V(2) 10 11 10 11
   22  182+20*V(1)+12*V(2)           -6+-2*V(1)  01 (01)(01)E> 117+V(1)+V(2) 10 11 10 11
<< Success! ==> defined new CTR 8 (PPA)
 2317               273176                 -524  01 (01)(01)E> 11285 10 11 10 11
== Executing  PA-CTR  6, V(1)=0, V(2)=281, repcount=94, factor=4/3
 3163               489564                   40  01377 (01)(01)E> 113 10 11 10 11
== Executing PPA-CTR  7 (once), V(1)=376
 3189               494998                 -714  013 (01)(01)E> 11382 01 11 01 10
== Executing  PA-CTR  6, V(1)=2, V(2)=378, repcount=127, factor=4/3
 4332               890984                   48  01511 (01)(01)E> 11 01 11 01 10
 4333               890991                   43  01511 <A(10)(10) 10 01 11 01 10
 4334               892013                 -979  <A(10)(10) 10512 01 11 01 10
 4335               892022                 -974  (10)(11)F> 10512 01 11 01 10
 4336               894070                   50  10512 (10)(11)F> 01 11 01 10
 4337               894072                   52  10513 (11)(00)D> 11 01 10
 4338               894074                   54  10513 11 (00)(10)A> 01 10
 4339               894078                   56  10513 11 00 (10)(01)E> 10
 4340               894080                   58  10513 11 00 10 (01)(01)B>
 4341               894085                   53  10513 11 00 10 <A(10)(10) 10
 4342               894094                   58  10513 11 00 10 (10)(11)F> 10
 4343               894098                   60  10513 11 00 102 (10)(11)F>
 4344               894105                   55  10513 11 00 102 <C(11)(10) 11
 4345               894107                   53  10513 11 00 10 <C(11)(11) 10 11
 4346               894109                   51  10513 11 00 <C(11)(11) 11 10 11
 4347               894111                   49  10513 11 <A(11)(11) 112 10 11
 4348               894113                   47  10513 <C(10)(11) 113 10 11
 4349               894115                   45  10512 <C(11)(10) 114 10 11
 4350               894117                   43  10511 <C(11)(11) 10 114 10 11
 4351               895139                 -979  <C(11)(11) 11511 10 114 10 11
 4352               895141                 -981  <A(11)(11) 11512 10 114 10 11
 4353               895162                 -976  01 (01)(01)E> 11512 10 114 10 11
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  013+V(1) (01)(01)E> 11 01 11 01 10
    1                    7                   -5  013+V(1) <A(10)(10) 10 01 11 01 10
    2            13+2*V(1)          -11+-2*V(1)  <A(10)(10) 104+V(1) 01 11 01 10
    3            22+2*V(1)           -6+-2*V(1)  (10)(11)F> 104+V(1) 01 11 01 10
    4            38+6*V(1)                    2  104+V(1) (10)(11)F> 01 11 01 10
    5            40+6*V(1)                    4  105+V(1) (11)(00)D> 11 01 10
    6            42+6*V(1)                    6  105+V(1) 11 (00)(10)A> 01 10
    7            46+6*V(1)                    8  105+V(1) 11 00 (10)(01)E> 10
    8            48+6*V(1)                   10  105+V(1) 11 00 10 (01)(01)B>
    9            53+6*V(1)                    5  105+V(1) 11 00 10 <A(10)(10) 10
   10            62+6*V(1)                   10  105+V(1) 11 00 10 (10)(11)F> 10
   11            66+6*V(1)                   12  105+V(1) 11 00 102 (10)(11)F>
   12            73+6*V(1)                    7  105+V(1) 11 00 102 <C(11)(10) 11
   13            75+6*V(1)                    5  105+V(1) 11 00 10 <C(11)(11) 10 11
   14            77+6*V(1)                    3  105+V(1) 11 00 <C(11)(11) 11 10 11
   15            79+6*V(1)                    1  105+V(1) 11 <A(11)(11) 112 10 11
   16            81+6*V(1)                   -1  105+V(1) <C(10)(11) 113 10 11
   17            83+6*V(1)                   -3  104+V(1) <C(11)(10) 114 10 11
   18            85+6*V(1)                   -5  103+V(1) <C(11)(11) 10 114 10 11
   19            91+8*V(1)          -11+-2*V(1)  <C(11)(11) 113+V(1) 10 114 10 11
   20            93+8*V(1)          -13+-2*V(1)  <A(11)(11) 114+V(1) 10 114 10 11
   21           114+8*V(1)           -8+-2*V(1)  01 (01)(01)E> 114+V(1) 10 114 10 11
<< Success! ==> defined new CTR 9 (PPA)
 4353               895162                 -976  01 (01)(01)E> 11512 10 114 10 11
== Executing  PA-CTR  6, V(1)=0, V(2)=508, repcount=170, factor=4/3
 5883              1596582                   44  01681 (01)(01)E> 112 10 114 10 11
 5884              1596589                   39  01681 <A(10)(10) 10 11 10 114 10 11
 5885              1597951                -1323  <A(10)(10) 10682 11 10 114 10 11
 5886              1597960                -1318  (10)(11)F> 10682 11 10 114 10 11
 5887              1600688                   46  10682 (10)(11)F> 11 10 114 10 11
 5888              1600692                   48  10683 (10)(10)A> 10 114 10 11
 5889              1600697                   43  10683 <B(01)(01) 00 114 10 11
 5890              1602063                -1323  <B(01)(01) 01683 00 114 10 11
 5891              1602076                -1318  01 (01)(01)E> 01683 00 114 10 11
 5892              1604808                   48  01684 (01)(01)E> 00 114 10 11
 5893              1604810                   50  01685 (01)(10)C> 114 10 11
 5894              1604812                   52  01686 (10)(01)E> 113 10 11
 5895              1604826                   54  01686 10 (10)(11)F> 112 10 11
 5896              1604830                   56  01686 102 (10)(10)A> 11 10 11
 5897              1604835                   51  01686 102 <B(01)(01) 01 10 11
 5898              1604839                   47  01686 <B(01)(01) 013 10 11
 5899              1604841                   45  01685 <B(11)(01) 014 10 11
 5900              1604843                   43  01684 <B(11)(11) 015 10 11
 5901              1606211                -1325  <B(11)(11) 11684 015 10 11
 5902              1606221                -1327  <A(10)(10) 11685 015 10 11
 5903              1606230                -1322  (10)(11)F> 11685 015 10 11
 5904              1606234                -1320  10 (10)(10)A> 11684 015 10 11
 5905              1606239                -1325  10 <B(01)(01) 01 11683 015 10 11
 5906              1606241                -1327  <B(01)(01) 012 11683 015 10 11
 5907              1606254                -1322  01 (01)(01)E> 012 11683 015 10 11
 5908              1606262                -1318  013 (01)(01)E> 11683 015 10 11
 5909              1606269                -1323  013 <A(10)(10) 10 11682 015 10 11
 5910              1606275                -1329  <A(10)(10) 104 11682 015 10 11
 5911              1606284                -1324  (10)(11)F> 104 11682 015 10 11
 5912              1606300                -1316  104 (10)(11)F> 11682 015 10 11
 5913              1606304                -1314  105 (10)(10)A> 11681 015 10 11
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  101+V(1) (10)(10)A> 114+V(2) [*]* [*]* [*]*
    1                    5                   -5  101+V(1) <B(01)(01) 01 113+V(2) [*]* [*]* [*]*
    2             7+2*V(1)           -7+-2*V(1)  <B(01)(01) 012+V(1) 113+V(2) [*]* [*]* [*]*
    3            20+2*V(1)           -2+-2*V(1)  01 (01)(01)E> 012+V(1) 113+V(2) [*]* [*]* [*]*
    4            28+6*V(1)                    2  013+V(1) (01)(01)E> 113+V(2) [*]* [*]* [*]*
    5            35+6*V(1)                   -3  013+V(1) <A(10)(10) 10 112+V(2) [*]* [*]* [*]*
    6            41+8*V(1)           -9+-2*V(1)  <A(10)(10) 104+V(1) 112+V(2) [*]* [*]* [*]*
    7            50+8*V(1)           -4+-2*V(1)  (10)(11)F> 104+V(1) 112+V(2) [*]* [*]* [*]*
    8           66+12*V(1)                    4  104+V(1) (10)(11)F> 112+V(2) [*]* [*]* [*]*
    9           70+12*V(1)                    6  105+V(1) (10)(10)A> 111+V(2) [*]* [*]* [*]*
<< Success! ==> defined new CTR 10 (PA)
 5913              1606304                -1314  105 (10)(10)A> 11681 015 10 11
== Executing  PA-CTR 10, V(1)=4, V(2)=677, repcount=226, factor=4/3
 7947              2853372                   42  10909 (10)(10)A> 113 015 10 11
 7948              2853377                   37  10909 <B(01)(01) 01 112 015 10 11
 7949              2855195                -1781  <B(01)(01) 01910 112 015 10 11
 7950              2855208                -1776  01 (01)(01)E> 01910 112 015 10 11
 7951              2858848                   44  01911 (01)(01)E> 112 015 10 11
 7952              2858855                   39  01911 <A(10)(10) 10 11 015 10 11
 7953              2860677                -1783  <A(10)(10) 10912 11 015 10 11
 7954              2860686                -1778  (10)(11)F> 10912 11 015 10 11
 7955              2864334                   46  10912 (10)(11)F> 11 015 10 11
 7956              2864338                   48  10913 (10)(10)A> 015 10 11
 7957              2864342                   50  10914 (10)(01)E> 014 10 11
 7958              2864346                   52  10915 (01)(01)E> 013 10 11
 7959              2864358                   58  10915 013 (01)(01)E> 10 11
 7960              2864360                   60  10915 014 (01)(01)B> 11
 7961              2864364                   62  10915 015 (00)(10)A>
 7962              2864382                   64  10915 016 (01)(01)E>
 7963              2864384                   66  10915 017 (01)(10)C>
 7964              2864389                   61  10915 017 <B(11)(01) 10
 7965              2864391                   59  10915 016 <B(11)(11) 01 10
 7966              2864403                   47  10915 <B(11)(11) 116 01 10
 7967              2864405                   45  10914 <B(01)(11) 117 01 10
 7968              2864407                   43  10913 <B(01)(01) 118 01 10
 7969              2866233                -1783  <B(01)(01) 01913 118 01 10
 7970              2866246                -1778  01 (01)(01)E> 01913 118 01 10
 7971              2869898                   48  01914 (01)(01)E> 118 01 10
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  101+V(1) (10)(10)A> 113 013+V(2) 10 11
    1                    5                   -5  101+V(1) <B(01)(01) 01 112 013+V(2) 10 11
    2             7+2*V(1)           -7+-2*V(1)  <B(01)(01) 012+V(1) 112 013+V(2) 10 11
    3            20+2*V(1)           -2+-2*V(1)  01 (01)(01)E> 012+V(1) 112 013+V(2) 10 11
    4            28+6*V(1)                    2  013+V(1) (01)(01)E> 112 013+V(2) 10 11
    5            35+6*V(1)                   -3  013+V(1) <A(10)(10) 10 11 013+V(2) 10 11
    6            41+8*V(1)           -9+-2*V(1)  <A(10)(10) 104+V(1) 11 013+V(2) 10 11
    7            50+8*V(1)           -4+-2*V(1)  (10)(11)F> 104+V(1) 11 013+V(2) 10 11
    8           66+12*V(1)                    4  104+V(1) (10)(11)F> 11 013+V(2) 10 11
    9           70+12*V(1)                    6  105+V(1) (10)(10)A> 013+V(2) 10 11
   10           74+12*V(1)                    8  106+V(1) (10)(01)E> 012+V(2) 10 11
   11           78+12*V(1)                   10  107+V(1) (01)(01)E> 011+V(2) 10 11
   12    82+12*V(1)+4*V(2)            12+2*V(2)  107+V(1) 011+V(2) (01)(01)E> 10 11
   13    84+12*V(1)+4*V(2)            14+2*V(2)  107+V(1) 012+V(2) (01)(01)B> 11
   14    88+12*V(1)+4*V(2)            16+2*V(2)  107+V(1) 013+V(2) (00)(10)A>
   15   106+12*V(1)+4*V(2)            18+2*V(2)  107+V(1) 014+V(2) (01)(01)E>
   16   108+12*V(1)+4*V(2)            20+2*V(2)  107+V(1) 015+V(2) (01)(10)C>
   17   113+12*V(1)+4*V(2)            15+2*V(2)  107+V(1) 015+V(2) <B(11)(01) 10
   18   115+12*V(1)+4*V(2)            13+2*V(2)  107+V(1) 014+V(2) <B(11)(11) 01 10
   19   123+12*V(1)+6*V(2)                    5  107+V(1) <B(11)(11) 114+V(2) 01 10
   20   125+12*V(1)+6*V(2)                    3  106+V(1) <B(01)(11) 115+V(2) 01 10
   21   127+12*V(1)+6*V(2)                    1  105+V(1) <B(01)(01) 116+V(2) 01 10
   22   137+14*V(1)+6*V(2)           -9+-2*V(1)  <B(01)(01) 015+V(1) 116+V(2) 01 10
   23   150+14*V(1)+6*V(2)           -4+-2*V(1)  01 (01)(01)E> 015+V(1) 116+V(2) 01 10
   24   170+18*V(1)+6*V(2)                    6  016+V(1) (01)(01)E> 116+V(2) 01 10
<< Success! ==> defined new CTR 11 (PPA)
 7971              2869898                   48  01914 (01)(01)E> 118 01 10
== Executing  PA-CTR  1, V(1)=913, V(2)=4, repcount=2, factor=4/3
 7989              2891998                   60  01922 (01)(01)E> 112 01 10
== Executing PPA-CTR  5 (once), V(1)=921
 8004              2899462                -1786  01 (01)(01)E> 11927 10 11
== Executing  PA-CTR  1, V(1)=0, V(2)=923, repcount=308, factor=4/3
10776              5190366                   62  011233 (01)(01)E> 113 10 11
== Executing PPA-CTR  4 (once), V(1)=1232
10799              5207784                -2404  013 (01)(01)E> 111239 01 10
== Executing  PA-CTR  1, V(1)=2, V(2)=1235, repcount=412, factor=4/3
14507              9310480                   68  011651 (01)(01)E> 113 01 10
== Executing PPA-CTR  3 (once), V(1)=1650, V(2)=0
14526              9343662                -3238  01 (01)(01)E> 111658 10 11
== Executing  PA-CTR  1, V(1)=0, V(2)=1654, repcount=552, factor=4/3
19494             16681950                   74  012209 (01)(01)E> 112 10 11
19495             16681957                   69  012209 <A(10)(10) 10 11 10 11
19496             16686375                -4349  <A(10)(10) 102210 11 10 11
19497             16686384                -4344  (10)(11)F> 102210 11 10 11
19498             16695224                   76  102210 (10)(11)F> 11 10 11
19499             16695228                   78  102211 (10)(10)A> 10 11
19500             16695233                   73  102211 <B(01)(01) 00 11
19501             16699655                -4349  <B(01)(01) 012211 00 11
19502             16699668                -4344  01 (01)(01)E> 012211 00 11
19503             16708512                   78  012212 (01)(01)E> 00 11
19504             16708514                   80  012213 (01)(10)C> 11
19505             16708516                   82  012214 (10)(01)E>
19506             16708518                   84  012214 10 (01)(10)C>
19507             16708523                   79  012214 10 <B(11)(01) 10
19508             16708525                   77  012214 <B(01)(11) 01 10
19509             16708527                   75  012213 <B(11)(01) 11 01 10
19510             16708529                   73  012212 <B(11)(11) 01 11 01 10
19511             16712953                -4351  <B(11)(11) 112212 01 11 01 10
19512             16712963                -4353  <A(10)(10) 112213 01 11 01 10
19513             16712972                -4348  (10)(11)F> 112213 01 11 01 10
19514             16712976                -4346  10 (10)(10)A> 112212 01 11 01 10
19515             16712981                -4351  10 <B(01)(01) 01 112211 01 11 01 10
19516             16712983                -4353  <B(01)(01) 012 112211 01 11 01 10
19517             16712996                -4348  01 (01)(01)E> 012 112211 01 11 01 10
19518             16713004                -4344  013 (01)(01)E> 112211 01 11 01 10
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  012+V(1) (01)(01)E> 112 10 11
    1                    7                   -5  012+V(1) <A(10)(10) 10 11 10 11
    2            11+2*V(1)           -9+-2*V(1)  <A(10)(10) 103+V(1) 11 10 11
    3            20+2*V(1)           -4+-2*V(1)  (10)(11)F> 103+V(1) 11 10 11
    4            32+6*V(1)                    2  103+V(1) (10)(11)F> 11 10 11
    5            36+6*V(1)                    4  104+V(1) (10)(10)A> 10 11
    6            41+6*V(1)                   -1  104+V(1) <B(01)(01) 00 11
    7            49+8*V(1)           -9+-2*V(1)  <B(01)(01) 014+V(1) 00 11
    8            62+8*V(1)           -4+-2*V(1)  01 (01)(01)E> 014+V(1) 00 11
    9           78+12*V(1)                    4  015+V(1) (01)(01)E> 00 11
   10           80+12*V(1)                    6  016+V(1) (01)(10)C> 11
   11           82+12*V(1)                    8  017+V(1) (10)(01)E>
   12           84+12*V(1)                   10  017+V(1) 10 (01)(10)C>
   13           89+12*V(1)                    5  017+V(1) 10 <B(11)(01) 10
   14           91+12*V(1)                    3  017+V(1) <B(01)(11) 01 10
   15           93+12*V(1)                    1  016+V(1) <B(11)(01) 11 01 10
   16           95+12*V(1)                   -1  015+V(1) <B(11)(11) 01 11 01 10
   17          105+14*V(1)          -11+-2*V(1)  <B(11)(11) 115+V(1) 01 11 01 10
   18          115+14*V(1)          -13+-2*V(1)  <A(10)(10) 116+V(1) 01 11 01 10
   19          124+14*V(1)           -8+-2*V(1)  (10)(11)F> 116+V(1) 01 11 01 10
   20          128+14*V(1)           -6+-2*V(1)  10 (10)(10)A> 115+V(1) 01 11 01 10
   21          133+14*V(1)          -11+-2*V(1)  10 <B(01)(01) 01 114+V(1) 01 11 01 10
   22          135+14*V(1)          -13+-2*V(1)  <B(01)(01) 012 114+V(1) 01 11 01 10
   23          148+14*V(1)           -8+-2*V(1)  01 (01)(01)E> 012 114+V(1) 01 11 01 10
   24          156+14*V(1)           -4+-2*V(1)  013 (01)(01)E> 114+V(1) 01 11 01 10
<< Success! ==> defined new CTR 12 (PPA)
19518             16713004                -4344  013 (01)(01)E> 112211 01 11 01 10
== Executing  PA-CTR  6, V(1)=2, V(2)=2207, repcount=736, factor=4/3
26142             29765228                   72  012947 (01)(01)E> 113 01 11 01 10
== Executing PPA-CTR  8 (once), V(1)=2946, V(2)=0
26164             29824330                -5826  01 (01)(01)E> 112953 10 11 10 11
== Executing  PA-CTR  6, V(1)=0, V(2)=2949, repcount=984, factor=4/3
35020             53107738                   78  013937 (01)(01)E> 11 10 11 10 11
35021             53107745                   73  013937 <A(10)(10) 102 11 10 11
35022             53115619                -7801  <A(10)(10) 103939 11 10 11
35023             53115628                -7796  (10)(11)F> 103939 11 10 11
35024             53131384                   82  103939 (10)(11)F> 11 10 11
35025             53131388                   84  103940 (10)(10)A> 10 11
35026             53131393                   79  103940 <B(01)(01) 00 11
35027             53139273                -7801  <B(01)(01) 013940 00 11
35028             53139286                -7796  01 (01)(01)E> 013940 00 11
35029             53155046                   84  013941 (01)(01)E> 00 11
35030             53155048                   86  013942 (01)(10)C> 11
35031             53155050                   88  013943 (10)(01)E>
35032             53155052                   90  013943 10 (01)(10)C>
35033             53155057                   85  013943 10 <B(11)(01) 10
35034             53155059                   83  013943 <B(01)(11) 01 10
35035             53155061                   81  013942 <B(11)(01) 11 01 10
35036             53155063                   79  013941 <B(11)(11) 01 11 01 10
35037             53162945                -7803  <B(11)(11) 113941 01 11 01 10
35038             53162955                -7805  <A(10)(10) 113942 01 11 01 10
35039             53162964                -7800  (10)(11)F> 113942 01 11 01 10
35040             53162968                -7798  10 (10)(10)A> 113941 01 11 01 10
35041             53162973                -7803  10 <B(01)(01) 01 113940 01 11 01 10
35042             53162975                -7805  <B(01)(01) 012 113940 01 11 01 10
35043             53162988                -7800  01 (01)(01)E> 012 113940 01 11 01 10
35044             53162996                -7796  013 (01)(01)E> 113940 01 11 01 10
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  011+V(1) (01)(01)E> 11 101+V(2) 11 10 11
    1                    7                   -5  011+V(1) <A(10)(10) 102+V(2) 11 10 11
    2             9+2*V(1)           -7+-2*V(1)  <A(10)(10) 103+V(1)+V(2) 11 10 11
    3            18+2*V(1)           -2+-2*V(1)  (10)(11)F> 103+V(1)+V(2) 11 10 11
    4     30+6*V(1)+4*V(2)             4+2*V(2)  103+V(1)+V(2) (10)(11)F> 11 10 11
    5     34+6*V(1)+4*V(2)             6+2*V(2)  104+V(1)+V(2) (10)(10)A> 10 11
    6     39+6*V(1)+4*V(2)             1+2*V(2)  104+V(1)+V(2) <B(01)(01) 00 11
    7     47+8*V(1)+6*V(2)           -7+-2*V(1)  <B(01)(01) 014+V(1)+V(2) 00 11
    8     60+8*V(1)+6*V(2)           -2+-2*V(1)  01 (01)(01)E> 014+V(1)+V(2) 00 11
    9   76+12*V(1)+10*V(2)             6+2*V(2)  015+V(1)+V(2) (01)(01)E> 00 11
   10   78+12*V(1)+10*V(2)             8+2*V(2)  016+V(1)+V(2) (01)(10)C> 11
   11   80+12*V(1)+10*V(2)            10+2*V(2)  017+V(1)+V(2) (10)(01)E>
   12   82+12*V(1)+10*V(2)            12+2*V(2)  017+V(1)+V(2) 10 (01)(10)C>
   13   87+12*V(1)+10*V(2)             7+2*V(2)  017+V(1)+V(2) 10 <B(11)(01) 10
   14   89+12*V(1)+10*V(2)             5+2*V(2)  017+V(1)+V(2) <B(01)(11) 01 10
   15   91+12*V(1)+10*V(2)             3+2*V(2)  016+V(1)+V(2) <B(11)(01) 11 01 10
   16   93+12*V(1)+10*V(2)             1+2*V(2)  015+V(1)+V(2) <B(11)(11) 01 11 01 10
   17  103+14*V(1)+12*V(2)           -9+-2*V(1)  <B(11)(11) 115+V(1)+V(2) 01 11 01 10
   18  113+14*V(1)+12*V(2)          -11+-2*V(1)  <A(10)(10) 116+V(1)+V(2) 01 11 01 10
   19  122+14*V(1)+12*V(2)           -6+-2*V(1)  (10)(11)F> 116+V(1)+V(2) 01 11 01 10
   20  126+14*V(1)+12*V(2)           -4+-2*V(1)  10 (10)(10)A> 115+V(1)+V(2) 01 11 01 10
   21  131+14*V(1)+12*V(2)           -9+-2*V(1)  10 <B(01)(01) 01 114+V(1)+V(2) 01 11 01 10
   22  133+14*V(1)+12*V(2)          -11+-2*V(1)  <B(01)(01) 012 114+V(1)+V(2) 01 11 01 10
   23  146+14*V(1)+12*V(2)           -6+-2*V(1)  01 (01)(01)E> 012 114+V(1)+V(2) 01 11 01 10
   24  154+14*V(1)+12*V(2)           -2+-2*V(1)  013 (01)(01)E> 114+V(1)+V(2) 01 11 01 10
<< Success! ==> defined new CTR 13 (PPA)
35044             53162996                -7796  013 (01)(01)E> 113940 01 11 01 10
== Executing  PA-CTR  6, V(1)=2, V(2)=3936, repcount=1313, factor=4/3
46861             94630162                   82  015255 (01)(01)E> 11 01 11 01 10
== Executing PPA-CTR  9 (once), V(1)=5252
46882             94672292               -10430  01 (01)(01)E> 115256 10 114 10 11
== Executing  PA-CTR  6, V(1)=0, V(2)=5252, repcount=1751, factor=4/3
62641            168336862                   76  017005 (01)(01)E> 113 10 114 10 11
62642            168336869                   71  017005 <A(10)(10) 10 112 10 114 10 11
62643            168350879               -13939  <A(10)(10) 107006 112 10 114 10 11
62644            168350888               -13934  (10)(11)F> 107006 112 10 114 10 11
62645            168378912                   78  107006 (10)(11)F> 112 10 114 10 11
62646            168378916                   80  107007 (10)(10)A> 11 10 114 10 11
62647            168378921                   75  107007 <B(01)(01) 01 10 114 10 11
62648            168392935               -13939  <B(01)(01) 017008 10 114 10 11
62649            168392948               -13934  01 (01)(01)E> 017008 10 114 10 11
62650            168420980                   82  017009 (01)(01)E> 10 114 10 11
62651            168420982                   84  017010 (01)(01)B> 114 10 11
62652            168420986                   86  017011 (00)(10)A> 113 10 11
62653            168421002                   88  017012 (01)(01)E> 112 10 11
62654            168421009                   83  017012 <A(10)(10) 10 11 10 11
62655            168435033               -13941  <A(10)(10) 107013 11 10 11
62656            168435042               -13936  (10)(11)F> 107013 11 10 11
62657            168463094                   90  107013 (10)(11)F> 11 10 11
62658            168463098                   92  107014 (10)(10)A> 10 11
62659            168463103                   87  107014 <B(01)(01) 00 11
62660            168477131               -13941  <B(01)(01) 017014 00 11
62661            168477144               -13936  01 (01)(01)E> 017014 00 11
62662            168505200                   92  017015 (01)(01)E> 00 11
62663            168505202                   94  017016 (01)(10)C> 11
62664            168505204                   96  017017 (10)(01)E>
62665            168505206                   98  017017 10 (01)(10)C>
62666            168505211                   93  017017 10 <B(11)(01) 10
62667            168505213                   91  017017 <B(01)(11) 01 10
62668            168505215                   89  017016 <B(11)(01) 11 01 10
62669            168505217                   87  017015 <B(11)(11) 01 11 01 10
62670            168519247               -13943  <B(11)(11) 117015 01 11 01 10
62671            168519257               -13945  <A(10)(10) 117016 01 11 01 10
62672            168519266               -13940  (10)(11)F> 117016 01 11 01 10
62673            168519270               -13938  10 (10)(10)A> 117015 01 11 01 10
62674            168519275               -13943  10 <B(01)(01) 01 117014 01 11 01 10
62675            168519277               -13945  <B(01)(01) 012 117014 01 11 01 10
62676            168519290               -13940  01 (01)(01)E> 012 117014 01 11 01 10
62677            168519298               -13936  013 (01)(01)E> 117014 01 11 01 10
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  011+V(1) (01)(01)E> 113 10 114 10 11
    1                    7                   -5  011+V(1) <A(10)(10) 10 112 10 114 10 11
    2             9+2*V(1)           -7+-2*V(1)  <A(10)(10) 102+V(1) 112 10 114 10 11
    3            18+2*V(1)           -2+-2*V(1)  (10)(11)F> 102+V(1) 112 10 114 10 11
    4            26+6*V(1)                    2  102+V(1) (10)(11)F> 112 10 114 10 11
    5            30+6*V(1)                    4  103+V(1) (10)(10)A> 11 10 114 10 11
    6            35+6*V(1)                   -1  103+V(1) <B(01)(01) 01 10 114 10 11
    7            41+8*V(1)           -7+-2*V(1)  <B(01)(01) 014+V(1) 10 114 10 11
    8            54+8*V(1)           -2+-2*V(1)  01 (01)(01)E> 014+V(1) 10 114 10 11
    9           70+12*V(1)                    6  015+V(1) (01)(01)E> 10 114 10 11
   10           72+12*V(1)                    8  016+V(1) (01)(01)B> 114 10 11
   11           76+12*V(1)                   10  017+V(1) (00)(10)A> 113 10 11
   12           92+12*V(1)                   12  018+V(1) (01)(01)E> 112 10 11
   13           99+12*V(1)                    7  018+V(1) <A(10)(10) 10 11 10 11
   14          115+14*V(1)           -9+-2*V(1)  <A(10)(10) 109+V(1) 11 10 11
   15          124+14*V(1)           -4+-2*V(1)  (10)(11)F> 109+V(1) 11 10 11
   16          160+18*V(1)                   14  109+V(1) (10)(11)F> 11 10 11
   17          164+18*V(1)                   16  1010+V(1) (10)(10)A> 10 11
   18          169+18*V(1)                   11  1010+V(1) <B(01)(01) 00 11
   19          189+20*V(1)           -9+-2*V(1)  <B(01)(01) 0110+V(1) 00 11
   20          202+20*V(1)           -4+-2*V(1)  01 (01)(01)E> 0110+V(1) 00 11
   21          242+24*V(1)                   16  0111+V(1) (01)(01)E> 00 11
   22          244+24*V(1)                   18  0112+V(1) (01)(10)C> 11
   23          246+24*V(1)                   20  0113+V(1) (10)(01)E>
   24          248+24*V(1)                   22  0113+V(1) 10 (01)(10)C>
   25          253+24*V(1)                   17  0113+V(1) 10 <B(11)(01) 10
   26          255+24*V(1)                   15  0113+V(1) <B(01)(11) 01 10
   27          257+24*V(1)                   13  0112+V(1) <B(11)(01) 11 01 10
   28          259+24*V(1)                   11  0111+V(1) <B(11)(11) 01 11 01 10
   29          281+26*V(1)          -11+-2*V(1)  <B(11)(11) 1111+V(1) 01 11 01 10
   30          291+26*V(1)          -13+-2*V(1)  <A(10)(10) 1112+V(1) 01 11 01 10
   31          300+26*V(1)           -8+-2*V(1)  (10)(11)F> 1112+V(1) 01 11 01 10
   32          304+26*V(1)           -6+-2*V(1)  10 (10)(10)A> 1111+V(1) 01 11 01 10
   33          309+26*V(1)          -11+-2*V(1)  10 <B(01)(01) 01 1110+V(1) 01 11 01 10
   34          311+26*V(1)          -13+-2*V(1)  <B(01)(01) 012 1110+V(1) 01 11 01 10
   35          324+26*V(1)           -8+-2*V(1)  01 (01)(01)E> 012 1110+V(1) 01 11 01 10
   36          332+26*V(1)           -4+-2*V(1)  013 (01)(01)E> 1110+V(1) 01 11 01 10
<< Success! ==> defined new CTR 14 (PPA)
62677            168519298               -13936  013 (01)(01)E> 117014 01 11 01 10
== Executing  PA-CTR  6, V(1)=2, V(2)=7010, repcount=2337, factor=4/3
83710            299760544                   86  019351 (01)(01)E> 113 01 11 01 10
== Executing PPA-CTR  8 (once), V(1)=9350, V(2)=0
83732            299947726               -18620  01 (01)(01)E> 119357 10 11 10 11
== Executing  PA-CTR  6, V(1)=0, V(2)=9353, repcount=3118, factor=4/3
111794            533417330                   88  0112473 (01)(01)E> 113 10 11 10 11
== Executing PPA-CTR  7 (once), V(1)=12472
111820            533592108               -24858  013 (01)(01)E> 1112478 01 11 01 10
== Executing  PA-CTR  6, V(1)=2, V(2)=12474, repcount=4159, factor=4/3
149251            949017982                   96  0116639 (01)(01)E> 11 01 11 01 10
== Executing PPA-CTR  9 (once), V(1)=16636
149272            949151184               -33184  01 (01)(01)E> 1116640 10 114 10 11
== Executing  PA-CTR  6, V(1)=0, V(2)=16636, repcount=5546, factor=4/3
199186           1687601084                   92  0122185 (01)(01)E> 112 10 114 10 11
199187           1687601091                   87  0122185 <A(10)(10) 10 11 10 114 10 11
199188           1687645461               -44283  <A(10)(10) 1022186 11 10 114 10 11
199189           1687645470               -44278  (10)(11)F> 1022186 11 10 114 10 11
199190           1687734214                   94  1022186 (10)(11)F> 11 10 114 10 11
199191           1687734218                   96  1022187 (10)(10)A> 10 114 10 11
199192           1687734223                   91  1022187 <B(01)(01) 00 114 10 11
199193           1687778597               -44283  <B(01)(01) 0122187 00 114 10 11
199194           1687778610               -44278  01 (01)(01)E> 0122187 00 114 10 11
199195           1687867358                   96  0122188 (01)(01)E> 00 114 10 11
199196           1687867360                   98  0122189 (01)(10)C> 114 10 11
199197           1687867362                  100  0122190 (10)(01)E> 113 10 11
199198           1687867376                  102  0122190 10 (10)(11)F> 112 10 11
199199           1687867380                  104  0122190 102 (10)(10)A> 11 10 11
199200           1687867385                   99  0122190 102 <B(01)(01) 01 10 11
199201           1687867389                   95  0122190 <B(01)(01) 013 10 11
199202           1687867391                   93  0122189 <B(11)(01) 014 10 11
199203           1687867393                   91  0122188 <B(11)(11) 015 10 11
199204           1687911769               -44285  <B(11)(11) 1122188 015 10 11
199205           1687911779               -44287  <A(10)(10) 1122189 015 10 11
199206           1687911788               -44282  (10)(11)F> 1122189 015 10 11
199207           1687911792               -44280  10 (10)(10)A> 1122188 015 10 11
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  011+V(1) (01)(01)E> 112 10 114 [*]* [*]*
    1                    7                   -5  011+V(1) <A(10)(10) 10 11 10 114 [*]* [*]*
    2             9+2*V(1)           -7+-2*V(1)  <A(10)(10) 102+V(1) 11 10 114 [*]* [*]*
    3            18+2*V(1)           -2+-2*V(1)  (10)(11)F> 102+V(1) 11 10 114 [*]* [*]*
    4            26+6*V(1)                    2  102+V(1) (10)(11)F> 11 10 114 [*]* [*]*
    5            30+6*V(1)                    4  103+V(1) (10)(10)A> 10 114 [*]* [*]*
    6            35+6*V(1)                   -1  103+V(1) <B(01)(01) 00 114 [*]* [*]*
    7            41+8*V(1)           -7+-2*V(1)  <B(01)(01) 013+V(1) 00 114 [*]* [*]*
    8            54+8*V(1)           -2+-2*V(1)  01 (01)(01)E> 013+V(1) 00 114 [*]* [*]*
    9           66+12*V(1)                    4  014+V(1) (01)(01)E> 00 114 [*]* [*]*
   10           68+12*V(1)                    6  015+V(1) (01)(10)C> 114 [*]* [*]*
   11           70+12*V(1)                    8  016+V(1) (10)(01)E> 113 [*]* [*]*
   12           84+12*V(1)                   10  016+V(1) 10 (10)(11)F> 112 [*]* [*]*
   13           88+12*V(1)                   12  016+V(1) 102 (10)(10)A> 11 [*]* [*]*
   14           93+12*V(1)                    7  016+V(1) 102 <B(01)(01) 01 [*]* [*]*
   15           97+12*V(1)                    3  016+V(1) <B(01)(01) 013 [*]* [*]*
   16           99+12*V(1)                    1  015+V(1) <B(11)(01) 014 [*]* [*]*
   17          101+12*V(1)                   -1  014+V(1) <B(11)(11) 015 [*]* [*]*
   18          109+14*V(1)           -9+-2*V(1)  <B(11)(11) 114+V(1) 015 [*]* [*]*
   19          119+14*V(1)          -11+-2*V(1)  <A(10)(10) 115+V(1) 015 [*]* [*]*
   20          128+14*V(1)           -6+-2*V(1)  (10)(11)F> 115+V(1) 015 [*]* [*]*
   21          132+14*V(1)           -4+-2*V(1)  10 (10)(10)A> 114+V(1) 015 [*]* [*]*
<< Success! ==> defined new CTR 15 (PPA)
199207           1687911792               -44280  10 (10)(10)A> 1122188 015 10 11
== Executing  PA-CTR 10, V(1)=0, V(2)=22184, repcount=7395, factor=4/3
265762           3000716562                   90  1029581 (10)(10)A> 113 015 10 11
== Executing PPA-CTR 11 (once), V(1)=29580, V(2)=2
265786           3001249184                   96  0129586 (01)(01)E> 118 01 10
== Executing  PA-CTR  1, V(1)=29585, V(2)=4, repcount=2, factor=4/3
265804           3001959412                  108  0129594 (01)(01)E> 112 01 10
== Executing PPA-CTR  5 (once), V(1)=29593
265819           3002196252               -59082  01 (01)(01)E> 1129599 10 11
== Executing  PA-CTR  1, V(1)=0, V(2)=29595, repcount=9866, factor=4/3
354613           5338761032                  114  0139465 (01)(01)E> 11 10 11
== Executing PPA-CTR  2 (once), V(1)=39464, V(2)=0
354633           5339313682               -78816  013 (01)(01)E> 1139469 01 10
== Executing  PA-CTR  1, V(1)=2, V(2)=39465, repcount=13156, factor=4/3
473037           9494162666                  120  0152627 (01)(01)E> 11 01 10
473038           9494162673                  115  0152627 <A(10)(10) 10 01 10
473039           9494267927              -105139  <A(10)(10) 1052628 01 10
473040           9494267936              -105134  (10)(11)F> 1052628 01 10
473041           9494478448                  122  1052628 (10)(11)F> 01 10
473042           9494478450                  124  1052629 (11)(00)D> 10
473043           9494478452                  126  1052629 11 (00)(11)F>
473044           9494478459                  121  1052629 11 <A(11)(10) 11
473045           9494478461                  119  1052629 <C(10)(11) 10 11
473046           9494478463                  117  1052628 <C(11)(10) 11 10 11
473047           9494478465                  115  1052627 <C(11)(11) 10 11 10 11
473048           9494583719              -105139  <C(11)(11) 1152627 10 11 10 11
473049           9494583721              -105141  <A(11)(11) 1152628 10 11 10 11
473050           9494583742              -105136  01 (01)(01)E> 1152628 10 11 10 11
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  013+V(1) (01)(01)E> 11 01 10
    1                    7                   -5  013+V(1) <A(10)(10) 10 01 10
    2            13+2*V(1)          -11+-2*V(1)  <A(10)(10) 104+V(1) 01 10
    3            22+2*V(1)           -6+-2*V(1)  (10)(11)F> 104+V(1) 01 10
    4            38+6*V(1)                    2  104+V(1) (10)(11)F> 01 10
    5            40+6*V(1)                    4  105+V(1) (11)(00)D> 10
    6            42+6*V(1)                    6  105+V(1) 11 (00)(11)F>
    7            49+6*V(1)                    1  105+V(1) 11 <A(11)(10) 11
    8            51+6*V(1)                   -1  105+V(1) <C(10)(11) 10 11
    9            53+6*V(1)                   -3  104+V(1) <C(11)(10) 11 10 11
   10            55+6*V(1)                   -5  103+V(1) <C(11)(11) 10 11 10 11
   11            61+8*V(1)          -11+-2*V(1)  <C(11)(11) 113+V(1) 10 11 10 11
   12            63+8*V(1)          -13+-2*V(1)  <A(11)(11) 114+V(1) 10 11 10 11
   13            84+8*V(1)           -8+-2*V(1)  01 (01)(01)E> 114+V(1) 10 11 10 11
<< Success! ==> defined new CTR 16 (PPA)
473050           9494583742              -105136  01 (01)(01)E> 1152628 10 11 10 11
== Executing  PA-CTR  6, V(1)=0, V(2)=52624, repcount=17542, factor=4/3
630928          16880713010                  116  0170169 (01)(01)E> 112 10 11 10 11
630929          16880713017                  111  0170169 <A(10)(10) 10 11 10 11 10 11
630930          16880853355              -140227  <A(10)(10) 1070170 11 10 11 10 11
630931          16880853364              -140222  (10)(11)F> 1070170 11 10 11 10 11
630932          16881134044                  118  1070170 (10)(11)F> 11 10 11 10 11
630933          16881134048                  120  1070171 (10)(10)A> 10 11 10 11
630934          16881134053                  115  1070171 <B(01)(01) 00 11 10 11
630935          16881274395              -140227  <B(01)(01) 0170171 00 11 10 11
630936          16881274408              -140222  01 (01)(01)E> 0170171 00 11 10 11
630937          16881555092                  120  0170172 (01)(01)E> 00 11 10 11
630938          16881555094                  122  0170173 (01)(10)C> 11 10 11
630939          16881555096                  124  0170174 (10)(01)E> 10 11
630940          16881555098                  126  0170174 10 (01)(01)B> 11
630941          16881555102                  128  0170174 10 01 (00)(10)A>
630942          16881555120                  130  0170174 10 012 (01)(01)E>
630943          16881555122                  132  0170174 10 013 (01)(10)C>
630944          16881555127                  127  0170174 10 013 <B(11)(01) 10
630945          16881555129                  125  0170174 10 012 <B(11)(11) 01 10
630946          16881555133                  121  0170174 10 <B(11)(11) 112 01 10
630947          16881555135                  119  0170174 <B(01)(11) 113 01 10
630948          16881555137                  117  0170173 <B(11)(01) 114 01 10
630949          16881555139                  115  0170172 <B(11)(11) 01 114 01 10
630950          16881695483              -140229  <B(11)(11) 1170172 01 114 01 10
630951          16881695493              -140231  <A(10)(10) 1170173 01 114 01 10
630952          16881695502              -140226  (10)(11)F> 1170173 01 114 01 10
630953          16881695506              -140224  10 (10)(10)A> 1170172 01 114 01 10
630954          16881695511              -140229  10 <B(01)(01) 01 1170171 01 114 01 10
630955          16881695513              -140231  <B(01)(01) 012 1170171 01 114 01 10
630956          16881695526              -140226  01 (01)(01)E> 012 1170171 01 114 01 10
630957          16881695534              -140222  013 (01)(01)E> 1170171 01 114 01 10
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  012+V(1) (01)(01)E> 112 10 11 10 11
    1                    7                   -5  012+V(1) <A(10)(10) 10 11 10 11 10 11
    2            11+2*V(1)           -9+-2*V(1)  <A(10)(10) 103+V(1) 11 10 11 10 11
    3            20+2*V(1)           -4+-2*V(1)  (10)(11)F> 103+V(1) 11 10 11 10 11
    4            32+6*V(1)                    2  103+V(1) (10)(11)F> 11 10 11 10 11
    5            36+6*V(1)                    4  104+V(1) (10)(10)A> 10 11 10 11
    6            41+6*V(1)                   -1  104+V(1) <B(01)(01) 00 11 10 11
    7            49+8*V(1)           -9+-2*V(1)  <B(01)(01) 014+V(1) 00 11 10 11
    8            62+8*V(1)           -4+-2*V(1)  01 (01)(01)E> 014+V(1) 00 11 10 11
    9           78+12*V(1)                    4  015+V(1) (01)(01)E> 00 11 10 11
   10           80+12*V(1)                    6  016+V(1) (01)(10)C> 11 10 11
   11           82+12*V(1)                    8  017+V(1) (10)(01)E> 10 11
   12           84+12*V(1)                   10  017+V(1) 10 (01)(01)B> 11
   13           88+12*V(1)                   12  017+V(1) 10 01 (00)(10)A>
   14          106+12*V(1)                   14  017+V(1) 10 012 (01)(01)E>
   15          108+12*V(1)                   16  017+V(1) 10 013 (01)(10)C>
   16          113+12*V(1)                   11  017+V(1) 10 013 <B(11)(01) 10
   17          115+12*V(1)                    9  017+V(1) 10 012 <B(11)(11) 01 10
   18          119+12*V(1)                    5  017+V(1) 10 <B(11)(11) 112 01 10
   19          121+12*V(1)                    3  017+V(1) <B(01)(11) 113 01 10
   20          123+12*V(1)                    1  016+V(1) <B(11)(01) 114 01 10
   21          125+12*V(1)                   -1  015+V(1) <B(11)(11) 01 114 01 10
   22          135+14*V(1)          -11+-2*V(1)  <B(11)(11) 115+V(1) 01 114 01 10
   23          145+14*V(1)          -13+-2*V(1)  <A(10)(10) 116+V(1) 01 114 01 10
   24          154+14*V(1)           -8+-2*V(1)  (10)(11)F> 116+V(1) 01 114 01 10
   25          158+14*V(1)           -6+-2*V(1)  10 (10)(10)A> 115+V(1) 01 114 01 10
   26          163+14*V(1)          -11+-2*V(1)  10 <B(01)(01) 01 114+V(1) 01 114 01 10
   27          165+14*V(1)          -13+-2*V(1)  <B(01)(01) 012 114+V(1) 01 114 01 10
   28          178+14*V(1)           -8+-2*V(1)  01 (01)(01)E> 012 114+V(1) 01 114 01 10
   29          186+14*V(1)           -4+-2*V(1)  013 (01)(01)E> 114+V(1) 01 114 01 10
<< Success! ==> defined new CTR 17 (PPA)
630957          16881695534              -140222  013 (01)(01)E> 1170171 01 114 01 10
== Executing  PA-CTR  6, V(1)=2, V(2)=70167, repcount=23390, factor=4/3
841467          30013543234                  118  0193563 (01)(01)E> 11 01 114 01 10
841468          30013543241                  113  0193563 <A(10)(10) 10 01 114 01 10
841469          30013730367              -187013  <A(10)(10) 1093564 01 114 01 10
841470          30013730376              -187008  (10)(11)F> 1093564 01 114 01 10
841471          30014104632                  120  1093564 (10)(11)F> 01 114 01 10
841472          30014104634                  122  1093565 (11)(00)D> 114 01 10
841473          30014104636                  124  1093565 11 (00)(10)A> 113 01 10
841474          30014104652                  126  1093565 11 01 (01)(01)E> 112 01 10
841475          30014104659                  121  1093565 11 01 <A(10)(10) 10 11 01 10
841476          30014104661                  119  1093565 11 <A(10)(10) 102 11 01 10
841477          30014104663                  117  1093565 <C(10)(10) 103 11 01 10
841478          30014104665                  115  1093564 <C(11)(10) 104 11 01 10
841479          30014104667                  113  1093563 <C(11)(11) 105 11 01 10
841480          30014291793              -187013  <C(11)(11) 1193563 105 11 01 10
841481          30014291795              -187015  <A(11)(11) 1193564 105 11 01 10
841482          30014291816              -187010  01 (01)(01)E> 1193564 105 11 01 10
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  013+V(1) (01)(01)E> 11 01 114+V(2) [*]* [*]*
    1                    7                   -5  013+V(1) <A(10)(10) 10 01 114+V(2) [*]* [*]*
    2            13+2*V(1)          -11+-2*V(1)  <A(10)(10) 104+V(1) 01 114+V(2) [*]* [*]*
    3            22+2*V(1)           -6+-2*V(1)  (10)(11)F> 104+V(1) 01 114+V(2) [*]* [*]*
    4            38+6*V(1)                    2  104+V(1) (10)(11)F> 01 114+V(2) [*]* [*]*
    5            40+6*V(1)                    4  105+V(1) (11)(00)D> 114+V(2) [*]* [*]*
    6            42+6*V(1)                    6  105+V(1) 11 (00)(10)A> 113+V(2) [*]* [*]*
    7            58+6*V(1)                    8  105+V(1) 11 01 (01)(01)E> 112+V(2) [*]* [*]*
    8            65+6*V(1)                    3  105+V(1) 11 01 <A(10)(10) 10 111+V(2) [*]* [*]*
    9            67+6*V(1)                    1  105+V(1) 11 <A(10)(10) 102 111+V(2) [*]* [*]*
   10            69+6*V(1)                   -1  105+V(1) <C(10)(10) 103 111+V(2) [*]* [*]*
   11            71+6*V(1)                   -3  104+V(1) <C(11)(10) 104 111+V(2) [*]* [*]*
   12            73+6*V(1)                   -5  103+V(1) <C(11)(11) 105 111+V(2) [*]* [*]*
   13            79+8*V(1)          -11+-2*V(1)  <C(11)(11) 113+V(1) 105 111+V(2) [*]* [*]*
   14            81+8*V(1)          -13+-2*V(1)  <A(11)(11) 114+V(1) 105 111+V(2) [*]* [*]*
   15           102+8*V(1)           -8+-2*V(1)  01 (01)(01)E> 114+V(1) 105 111+V(2) [*]* [*]*
<< Success! ==> defined new CTR 18 (PPA)
841482          30014291816              -187010  01 (01)(01)E> 1193564 105 11 01 10
== Executing  PA-CTR  6, V(1)=0, V(2)=93560, repcount=31187, factor=4/3
1122165          53358821674                  112  01124749 (01)(01)E> 113 105 11 01 10
1122166          53358821681                  107  01124749 <A(10)(10) 10 112 105 11 01 10
1122167          53359071179              -249391  <A(10)(10) 10124750 112 105 11 01 10
1122168          53359071188              -249386  (10)(11)F> 10124750 112 105 11 01 10
1122169          53359570188                  114  10124750 (10)(11)F> 112 105 11 01 10
1122170          53359570192                  116  10124751 (10)(10)A> 11 105 11 01 10
1122171          53359570197                  111  10124751 <B(01)(01) 01 105 11 01 10
1122172          53359819699              -249391  <B(01)(01) 01124752 105 11 01 10
1122173          53359819712              -249386  01 (01)(01)E> 01124752 105 11 01 10
1122174          53360318720                  118  01124753 (01)(01)E> 105 11 01 10
1122175          53360318722                  120  01124754 (01)(01)B> 104 11 01 10
1122176          53360318726                  122  01124755 (00)(11)F> 103 11 01 10
1122177          53360318730                  124  01124755 00 (10)(11)F> 102 11 01 10
1122178          53360318738                  128  01124755 00 102 (10)(11)F> 11 01 10
1122179          53360318742                  130  01124755 00 103 (10)(10)A> 01 10
1122180          53360318746                  132  01124755 00 104 (10)(01)E> 10
1122181          53360318748                  134  01124755 00 105 (01)(01)B>
1122182          53360318753                  129  01124755 00 105 <A(10)(10) 10
1122183          53360318762                  134  01124755 00 105 (10)(11)F> 10
1122184          53360318766                  136  01124755 00 106 (10)(11)F>
1122185          53360318773                  131  01124755 00 106 <C(11)(10) 11
1122186          53360318775                  129  01124755 00 105 <C(11)(11) 10 11
1122187          53360318785                  119  01124755 00 <C(11)(11) 115 10 11
1122188          53360318787                  117  01124755 <A(11)(11) 116 10 11
1122189          53360318789                  115  01124754 <A(10)(11) 117 10 11
1122190          53360318791                  113  01124753 <A(10)(10) 118 10 11
1122191          53360568297              -249393  <A(10)(10) 10124753 118 10 11
1122192          53360568306              -249388  (10)(11)F> 10124753 118 10 11
1122193          53361067318                  118  10124753 (10)(11)F> 118 10 11
1122194          53361067322                  120  10124754 (10)(10)A> 117 10 11
1122195          53361067327                  115  10124754 <B(01)(01) 01 116 10 11
1122196          53361316835              -249393  <B(01)(01) 01124755 116 10 11
1122197          53361316848              -249388  01 (01)(01)E> 01124755 116 10 11
1122198          53361815868                  122  01124756 (01)(01)E> 116 10 11
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  011+V(1) (01)(01)E> 113 104+V(2) 11 01 10
    1                    7                   -5  011+V(1) <A(10)(10) 10 112 104+V(2) 11 01 10
    2             9+2*V(1)           -7+-2*V(1)  <A(10)(10) 102+V(1) 112 104+V(2) 11 01 10
    3            18+2*V(1)           -2+-2*V(1)  (10)(11)F> 102+V(1) 112 104+V(2) 11 01 10
    4            26+6*V(1)                    2  102+V(1) (10)(11)F> 112 104+V(2) 11 01 10
    5            30+6*V(1)                    4  103+V(1) (10)(10)A> 11 104+V(2) 11 01 10
    6            35+6*V(1)                   -1  103+V(1) <B(01)(01) 01 104+V(2) 11 01 10
    7            41+8*V(1)           -7+-2*V(1)  <B(01)(01) 014+V(1) 104+V(2) 11 01 10
    8            54+8*V(1)           -2+-2*V(1)  01 (01)(01)E> 014+V(1) 104+V(2) 11 01 10
    9           70+12*V(1)                    6  015+V(1) (01)(01)E> 104+V(2) 11 01 10
   10           72+12*V(1)                    8  016+V(1) (01)(01)B> 103+V(2) 11 01 10
   11           76+12*V(1)                   10  017+V(1) (00)(11)F> 102+V(2) 11 01 10
   12           80+12*V(1)                   12  017+V(1) 00 (10)(11)F> 101+V(2) 11 01 10
   13    84+12*V(1)+4*V(2)            14+2*V(2)  017+V(1) 00 101+V(2) (10)(11)F> 11 01 10
   14    88+12*V(1)+4*V(2)            16+2*V(2)  017+V(1) 00 102+V(2) (10)(10)A> 01 10
   15    92+12*V(1)+4*V(2)            18+2*V(2)  017+V(1) 00 103+V(2) (10)(01)E> 10
   16    94+12*V(1)+4*V(2)            20+2*V(2)  017+V(1) 00 104+V(2) (01)(01)B>
   17    99+12*V(1)+4*V(2)            15+2*V(2)  017+V(1) 00 104+V(2) <A(10)(10) 10
   18   108+12*V(1)+4*V(2)            20+2*V(2)  017+V(1) 00 104+V(2) (10)(11)F> 10
   19   112+12*V(1)+4*V(2)            22+2*V(2)  017+V(1) 00 105+V(2) (10)(11)F>
   20   119+12*V(1)+4*V(2)            17+2*V(2)  017+V(1) 00 105+V(2) <C(11)(10) 11
   21   121+12*V(1)+4*V(2)            15+2*V(2)  017+V(1) 00 104+V(2) <C(11)(11) 10 11
   22   129+12*V(1)+6*V(2)                    7  017+V(1) 00 <C(11)(11) 114+V(2) 10 11
   23   131+12*V(1)+6*V(2)                    5  017+V(1) <A(11)(11) 115+V(2) 10 11
   24   133+12*V(1)+6*V(2)                    3  016+V(1) <A(10)(11) 116+V(2) 10 11
   25   135+12*V(1)+6*V(2)                    1  015+V(1) <A(10)(10) 117+V(2) 10 11
   26   145+14*V(1)+6*V(2)           -9+-2*V(1)  <A(10)(10) 105+V(1) 117+V(2) 10 11
   27   154+14*V(1)+6*V(2)           -4+-2*V(1)  (10)(11)F> 105+V(1) 117+V(2) 10 11
   28   174+18*V(1)+6*V(2)                    6  105+V(1) (10)(11)F> 117+V(2) 10 11
   29   178+18*V(1)+6*V(2)                    8  106+V(1) (10)(10)A> 116+V(2) 10 11
   30   183+18*V(1)+6*V(2)                    3  106+V(1) <B(01)(01) 01 115+V(2) 10 11
   31   195+20*V(1)+6*V(2)           -9+-2*V(1)  <B(01)(01) 017+V(1) 115+V(2) 10 11
   32   208+20*V(1)+6*V(2)           -4+-2*V(1)  01 (01)(01)E> 017+V(1) 115+V(2) 10 11
   33   236+24*V(1)+6*V(2)                   10  018+V(1) (01)(01)E> 115+V(2) 10 11
<< Success! ==> defined new CTR 19 (PPA)
1122198          53361815868                  122  01124756 (01)(01)E> 116 10 11
== Executing  PA-CTR  1, V(1)=124755, V(2)=2, repcount=1, factor=4/3
1122207          53363312998                  128  01124760 (01)(01)E> 113 10 11
== Executing PPA-CTR  4 (once), V(1)=124759
1122230          53365059794              -249392  013 (01)(01)E> 11124766 01 10
== Executing  PA-CTR  1, V(1)=2, V(2)=124762, repcount=41588, factor=4/3
1496522          94877452810                  136  01166355 (01)(01)E> 112 01 10
== Executing PPA-CTR  5 (once), V(1)=166354
1496537          94878783738              -332576  01 (01)(01)E> 11166360 10 11
== Executing  PA-CTR  1, V(1)=0, V(2)=166356, repcount=55453, factor=4/3
1995614         168682179592                  142  01221813 (01)(01)E> 11 10 11
== Executing PPA-CTR  2 (once), V(1)=221812, V(2)=0
1995634         168685285114              -443484  013 (01)(01)E> 11221817 01 10
== Executing  PA-CTR  1, V(1)=2, V(2)=221813, repcount=73938, factor=4/3
2661076         299894329030                  144  01295755 (01)(01)E> 113 01 10
== Executing PPA-CTR  3 (once), V(1)=295754, V(2)=0
2661095         299900244292              -591370  01 (01)(01)E> 11295762 10 11
== Executing  PA-CTR  1, V(1)=0, V(2)=295758, repcount=98587, factor=4/3
3548378         533170296950                  152  01394349 (01)(01)E> 11 10 11
== Executing PPA-CTR  2 (once), V(1)=394348, V(2)=0
3548398         533175817976              -788546  013 (01)(01)E> 11394353 01 10
== Executing  PA-CTR  1, V(1)=2, V(2)=394349, repcount=131450, factor=4/3
4731448         947883479476                  154  01525803 (01)(01)E> 113 01 10
== Executing PPA-CTR  3 (once), V(1)=525802, V(2)=0
4731467         947893995698             -1051456  01 (01)(01)E> 11525810 10 11
== Executing  PA-CTR  1, V(1)=0, V(2)=525806, repcount=175269, factor=4/3
6308888        1685163394736                  158  01701077 (01)(01)E> 113 10 11
== Executing PPA-CTR  4 (once), V(1)=701076
6308911        1685173209970             -1401996  013 (01)(01)E> 11701083 01 10
== Executing  PA-CTR  1, V(1)=2, V(2)=701079, repcount=233694, factor=4/3
8412157        2995898823814                  168  01934779 (01)(01)E> 11 01 10
== Executing PPA-CTR 16 (once), V(1)=934776
8412170        2995906302106             -1869392  01 (01)(01)E> 11934780 10 11 10 11
== Executing  PA-CTR  6, V(1)=0, V(2)=934776, repcount=311593, factor=4/3
11216507        5326085378960                  166  011246373 (01)(01)E> 11 10 11 10 11
== Executing PPA-CTR 13 (once), V(1)=1246372, V(2)=0
11216531        5326102828322             -2492580  013 (01)(01)E> 111246376 01 11 01 10
== Executing  PA-CTR  6, V(1)=2, V(2)=1246372, repcount=415458, factor=4/3
14955653        9468660304718                  168  011661835 (01)(01)E> 112 01 11 01 10
14955654        9468660304725                  163  011661835 <A(10)(10) 10 11 01 11 01 10
14955655        9468663628395             -3323507  <A(10)(10) 101661836 11 01 11 01 10
14955656        9468663628404             -3323502  (10)(11)F> 101661836 11 01 11 01 10
14955657        9468670275748                  170  101661836 (10)(11)F> 11 01 11 01 10
14955658        9468670275752                  172  101661837 (10)(10)A> 01 11 01 10
14955659        9468670275756                  174  101661838 (10)(01)E> 11 01 10
14955660        9468670275770                  176  101661839 (10)(11)F> 01 10
14955661        9468670275772                  178  101661840 (11)(00)D> 10
14955662        9468670275774                  180  101661840 11 (00)(11)F>
14955663        9468670275781                  175  101661840 11 <A(11)(10) 11
14955664        9468670275783                  173  101661840 <C(10)(11) 10 11
14955665        9468670275785                  171  101661839 <C(11)(10) 11 10 11
14955666        9468670275787                  169  101661838 <C(11)(11) 10 11 10 11
14955667        9468673599463             -3323507  <C(11)(11) 111661838 10 11 10 11
14955668        9468673599465             -3323509  <A(11)(11) 111661839 10 11 10 11
14955669        9468673599486             -3323504  01 (01)(01)E> 111661839 10 11 10 11
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  011+V(1) (01)(01)E> 112 01 11 01 10
    1                    7                   -5  011+V(1) <A(10)(10) 10 11 01 11 01 10
    2             9+2*V(1)           -7+-2*V(1)  <A(10)(10) 102+V(1) 11 01 11 01 10
    3            18+2*V(1)           -2+-2*V(1)  (10)(11)F> 102+V(1) 11 01 11 01 10
    4            26+6*V(1)                    2  102+V(1) (10)(11)F> 11 01 11 01 10
    5            30+6*V(1)                    4  103+V(1) (10)(10)A> 01 11 01 10
    6            34+6*V(1)                    6  104+V(1) (10)(01)E> 11 01 10
    7            48+6*V(1)                    8  105+V(1) (10)(11)F> 01 10
    8            50+6*V(1)                   10  106+V(1) (11)(00)D> 10
    9            52+6*V(1)                   12  106+V(1) 11 (00)(11)F>
   10            59+6*V(1)                    7  106+V(1) 11 <A(11)(10) 11
   11            61+6*V(1)                    5  106+V(1) <C(10)(11) 10 11
   12            63+6*V(1)                    3  105+V(1) <C(11)(10) 11 10 11
   13            65+6*V(1)                    1  104+V(1) <C(11)(11) 10 11 10 11
   14            73+8*V(1)           -7+-2*V(1)  <C(11)(11) 114+V(1) 10 11 10 11
   15            75+8*V(1)           -9+-2*V(1)  <A(11)(11) 115+V(1) 10 11 10 11
   16            96+8*V(1)           -4+-2*V(1)  01 (01)(01)E> 115+V(1) 10 11 10 11
<< Success! ==> defined new CTR 20 (PPA)
14955669        9468673599486             -3323504  01 (01)(01)E> 111661839 10 11 10 11
== Executing  PA-CTR  6, V(1)=0, V(2)=1661835, repcount=553946, factor=4/3
19941183       16833247182986                  172  012215785 (01)(01)E> 11 10 11 10 11
== Executing PPA-CTR 13 (once), V(1)=2215784, V(2)=0
19941207       16833278204116             -4431398  013 (01)(01)E> 112215788 01 11 01 10
== Executing  PA-CTR  6, V(1)=2, V(2)=2215784, repcount=738595, factor=4/3
26588562       29925871682366                  172  012954383 (01)(01)E> 113 01 11 01 10
== Executing PPA-CTR  8 (once), V(1)=2954382, V(2)=0
26588584       29925930770188             -5908598  01 (01)(01)E> 112954389 10 11 10 11
== Executing  PA-CTR  6, V(1)=0, V(2)=2954385, repcount=984796, factor=4/3
35451748       53201731949588                  178  013939185 (01)(01)E> 11 10 11 10 11
== Executing PPA-CTR 13 (once), V(1)=3939184, V(2)=0
35451772       53201787098318             -7878192  013 (01)(01)E> 113939188 01 11 01 10
== Executing  PA-CTR  6, V(1)=2, V(2)=3939184, repcount=1313062, factor=4/3
47269330       94581042592914                  180  015252251 (01)(01)E> 112 01 11 01 10
== Executing PPA-CTR 20 (once), V(1)=5252250
47269346       94581084611010            -10504324  01 (01)(01)E> 115252255 10 11 10 11
== Executing  PA-CTR  6, V(1)=0, V(2)=5252251, repcount=1750751, factor=4/3
63026105      168144262681580                  182  017003005 (01)(01)E> 112 10 11 10 11
== Executing PPA-CTR 17 (once), V(1)=7003003
63026134      168144360723808            -14005828  013 (01)(01)E> 117003007 01 114 01 10
== Executing  PA-CTR  6, V(1)=2, V(2)=7003003, repcount=2334335, factor=4/3
84035149      298923401540658                  182  019337343 (01)(01)E> 112 01 114 01 10
84035150      298923401540665                  177  019337343 <A(10)(10) 10 11 01 114 01 10
84035151      298923420215351            -18674509  <A(10)(10) 109337344 11 01 114 01 10
84035152      298923420215360            -18674504  (10)(11)F> 109337344 11 01 114 01 10
84035153      298923457564736                  184  109337344 (10)(11)F> 11 01 114 01 10
84035154      298923457564740                  186  109337345 (10)(10)A> 01 114 01 10
84035155      298923457564744                  188  109337346 (10)(01)E> 114 01 10
84035156      298923457564758                  190  109337347 (10)(11)F> 113 01 10
84035157      298923457564762                  192  109337348 (10)(10)A> 112 01 10
84035158      298923457564767                  187  109337348 <B(01)(01) 01 11 01 10
84035159      298923476239463            -18674509  <B(01)(01) 019337349 11 01 10
84035160      298923476239476            -18674504  01 (01)(01)E> 019337349 11 01 10
84035161      298923513588872                  194  019337350 (01)(01)E> 11 01 10
84035162      298923513588879                  189  019337350 <A(10)(10) 10 01 10
84035163      298923532263579            -18674511  <A(10)(10) 109337351 01 10
84035164      298923532263588            -18674506  (10)(11)F> 109337351 01 10
84035165      298923569612992                  196  109337351 (10)(11)F> 01 10
84035166      298923569612994                  198  109337352 (11)(00)D> 10
84035167      298923569612996                  200  109337352 11 (00)(11)F>
84035168      298923569613003                  195  109337352 11 <A(11)(10) 11
84035169      298923569613005                  193  109337352 <C(10)(11) 10 11
84035170      298923569613007                  191  109337351 <C(11)(10) 11 10 11
84035171      298923569613009                  189  109337350 <C(11)(11) 10 11 10 11
84035172      298923588287709            -18674511  <C(11)(11) 119337350 10 11 10 11
84035173      298923588287711            -18674513  <A(11)(11) 119337351 10 11 10 11
84035174      298923588287732            -18674508  01 (01)(01)E> 119337351 10 11 10 11
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  011+V(1) (01)(01)E> 112 01 114 01 10
    1                    7                   -5  011+V(1) <A(10)(10) 10 11 01 114 01 10
    2             9+2*V(1)           -7+-2*V(1)  <A(10)(10) 102+V(1) 11 01 114 01 10
    3            18+2*V(1)           -2+-2*V(1)  (10)(11)F> 102+V(1) 11 01 114 01 10
    4            26+6*V(1)                    2  102+V(1) (10)(11)F> 11 01 114 01 10
    5            30+6*V(1)                    4  103+V(1) (10)(10)A> 01 114 01 10
    6            34+6*V(1)                    6  104+V(1) (10)(01)E> 114 01 10
    7            48+6*V(1)                    8  105+V(1) (10)(11)F> 113 01 10
    8            52+6*V(1)                   10  106+V(1) (10)(10)A> 112 01 10
    9            57+6*V(1)                    5  106+V(1) <B(01)(01) 01 11 01 10
   10            69+8*V(1)           -7+-2*V(1)  <B(01)(01) 017+V(1) 11 01 10
   11            82+8*V(1)           -2+-2*V(1)  01 (01)(01)E> 017+V(1) 11 01 10
   12          110+12*V(1)                   12  018+V(1) (01)(01)E> 11 01 10
   13          117+12*V(1)                    7  018+V(1) <A(10)(10) 10 01 10
   14          133+14*V(1)           -9+-2*V(1)  <A(10)(10) 109+V(1) 01 10
   15          142+14*V(1)           -4+-2*V(1)  (10)(11)F> 109+V(1) 01 10
   16          178+18*V(1)                   14  109+V(1) (10)(11)F> 01 10
   17          180+18*V(1)                   16  1010+V(1) (11)(00)D> 10
   18          182+18*V(1)                   18  1010+V(1) 11 (00)(11)F>
   19          189+18*V(1)                   13  1010+V(1) 11 <A(11)(10) 11
   20          191+18*V(1)                   11  1010+V(1) <C(10)(11) 10 11
   21          193+18*V(1)                    9  109+V(1) <C(11)(10) 11 10 11
   22          195+18*V(1)                    7  108+V(1) <C(11)(11) 10 11 10 11
   23          211+20*V(1)           -9+-2*V(1)  <C(11)(11) 118+V(1) 10 11 10 11
   24          213+20*V(1)          -11+-2*V(1)  <A(11)(11) 119+V(1) 10 11 10 11
   25          234+20*V(1)           -6+-2*V(1)  01 (01)(01)E> 119+V(1) 10 11 10 11
<< Success! ==> defined new CTR 21 (PPA)
84035174      298923588287732            -18674508  01 (01)(01)E> 119337351 10 11 10 11
== Executing  PA-CTR  6, V(1)=0, V(2)=9337347, repcount=3112450, factor=4/3
112047224      531420011520432                  192  0112449801 (01)(01)E> 11 10 11 10 11
== Executing PPA-CTR 13 (once), V(1)=12449800, V(2)=0
112047248      531420185817786            -24899410  013 (01)(01)E> 1112449804 01 11 01 10
== Executing  PA-CTR  6, V(1)=2, V(2)=12449800, repcount=4149934, factor=4/3
149396654      944747329217710                  194  0116599739 (01)(01)E> 112 01 11 01 10
== Executing PPA-CTR 20 (once), V(1)=16599738
149396670      944747462015710            -33199286  01 (01)(01)E> 1116599743 10 11 10 11
== Executing  PA-CTR  6, V(1)=0, V(2)=16599739, repcount=5533247, factor=4/3
199195893     1679551453257288                  196  0122132989 (01)(01)E> 112 10 11 10 11
== Executing PPA-CTR 17 (once), V(1)=22132987
199195922     1679551763119292            -44265782  013 (01)(01)E> 1122132991 01 114 01 10
== Executing  PA-CTR  6, V(1)=2, V(2)=22132987, repcount=7377663, factor=4/3
265594889     2985870151753358                  196  0129510655 (01)(01)E> 112 01 114 01 10
== Executing PPA-CTR 21 (once), V(1)=29510654
265594914     2985870741966672            -59021118  01 (01)(01)E> 1129510663 10 11 10 11
== Executing  PA-CTR  6, V(1)=0, V(2)=29510659, repcount=9836887, factor=4/3
354126897     5308215494881930                  204  0139347549 (01)(01)E> 112 10 11 10 11
== Executing PPA-CTR 17 (once), V(1)=39347547
354126926     5308216045747774            -78694894  013 (01)(01)E> 1139347551 01 114 01 10
== Executing  PA-CTR  6, V(1)=2, V(2)=39347547, repcount=13115850, factor=4/3
472169576     9436829473197274                  206  0152463403 (01)(01)E> 11 01 114 01 10
== Executing PPA-CTR 18 (once), V(1)=52463400, V(2)=0
472169591     9436829892904576           -104926602  01 (01)(01)E> 1152463404 105 11 01 10
== Executing  PA-CTR  6, V(1)=0, V(2)=52463400, repcount=17487801, factor=4/3
629559800    16776587108917846                  204  0169951205 (01)(01)E> 11 105 11 01 10
629559801    16776587108917853                  199  0169951205 <A(10)(10) 106 11 01 10
629559802    16776587248820263           -139902211  <A(10)(10) 1069951211 11 01 10
629559803    16776587248820272           -139902206  (10)(11)F> 1069951211 11 01 10
629559804    16776587528625116                  216  1069951211 (10)(11)F> 11 01 10
629559805    16776587528625120                  218  1069951212 (10)(10)A> 01 10
629559806    16776587528625124                  220  1069951213 (10)(01)E> 10
629559807    16776587528625126                  222  1069951214 (01)(01)B>
629559808    16776587528625131                  217  1069951214 <A(10)(10) 10
629559809    16776587528625140                  222  1069951214 (10)(11)F> 10
629559810    16776587528625144                  224  1069951215 (10)(11)F>
629559811    16776587528625151                  219  1069951215 <C(11)(10) 11
629559812    16776587528625153                  217  1069951214 <C(11)(11) 10 11
629559813    16776587668527581           -139902211  <C(11)(11) 1169951214 10 11
629559814    16776587668527583           -139902213  <A(11)(11) 1169951215 10 11
629559815    16776587668527604           -139902208  01 (01)(01)E> 1169951215 10 11
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  011+V(1) (01)(01)E> 11 101+V(2) 11 01 10
    1                    7                   -5  011+V(1) <A(10)(10) 102+V(2) 11 01 10
    2             9+2*V(1)           -7+-2*V(1)  <A(10)(10) 103+V(1)+V(2) 11 01 10
    3            18+2*V(1)           -2+-2*V(1)  (10)(11)F> 103+V(1)+V(2) 11 01 10
    4     30+6*V(1)+4*V(2)             4+2*V(2)  103+V(1)+V(2) (10)(11)F> 11 01 10
    5     34+6*V(1)+4*V(2)             6+2*V(2)  104+V(1)+V(2) (10)(10)A> 01 10
    6     38+6*V(1)+4*V(2)             8+2*V(2)  105+V(1)+V(2) (10)(01)E> 10
    7     40+6*V(1)+4*V(2)            10+2*V(2)  106+V(1)+V(2) (01)(01)B>
    8     45+6*V(1)+4*V(2)             5+2*V(2)  106+V(1)+V(2) <A(10)(10) 10
    9     54+6*V(1)+4*V(2)            10+2*V(2)  106+V(1)+V(2) (10)(11)F> 10
   10     58+6*V(1)+4*V(2)            12+2*V(2)  107+V(1)+V(2) (10)(11)F>
   11     65+6*V(1)+4*V(2)             7+2*V(2)  107+V(1)+V(2) <C(11)(10) 11
   12     67+6*V(1)+4*V(2)             5+2*V(2)  106+V(1)+V(2) <C(11)(11) 10 11
   13     79+8*V(1)+6*V(2)           -7+-2*V(1)  <C(11)(11) 116+V(1)+V(2) 10 11
   14     81+8*V(1)+6*V(2)           -9+-2*V(1)  <A(11)(11) 117+V(1)+V(2) 10 11
   15    102+8*V(1)+6*V(2)           -4+-2*V(1)  01 (01)(01)E> 117+V(1)+V(2) 10 11
<< Success! ==> defined new CTR 22 (PPA)
629559815    16776587668527604           -139902208  01 (01)(01)E> 1169951215 10 11
== Executing  PA-CTR  1, V(1)=0, V(2)=69951211, repcount=23317071, factor=4/3
839413454    29825047941569854                  218  0193268285 (01)(01)E> 112 10 11
== Executing PPA-CTR 12 (once), V(1)=93268283
839413478    29825049247325972           -186536352  013 (01)(01)E> 1193268287 01 11 01 10
== Executing  PA-CTR  6, V(1)=2, V(2)=93268283, repcount=31089428, factor=4/3
1119218330    53022312224398348                  216  01124357715 (01)(01)E> 113 01 11 01 10
== Executing PPA-CTR  8 (once), V(1)=124357714, V(2)=0
1119218352    53022314711552810           -248715218  01 (01)(01)E> 11124357721 10 11 10 11
== Executing  PA-CTR  6, V(1)=0, V(2)=124357717, repcount=41452573, factor=4/3
1492291509    94261896018059064                  220  01165810293 (01)(01)E> 112 10 11 10 11
== Executing PPA-CTR 17 (once), V(1)=165810291
1492291538    94261898339403324           -331620366  013 (01)(01)E> 11165810295 01 114 01 10
== Executing  PA-CTR  6, V(1)=2, V(2)=165810291, repcount=55270098, factor=4/3
1989722420    1675767[4]8620680                  222  01221080395 (01)(01)E> 11 01 114 01 10
== Executing PPA-CTR 18 (once), V(1)=221080392, V(2)=0
1989722435    1675767[4]7263918           -442160570  01 (01)(01)E> 11221080396 105 11 01 10
== Executing  PA-CTR  6, V(1)=0, V(2)=221080392, repcount=73693465, factor=4/3
2652963620    2979141[4]6112708                  220  01294773861 (01)(01)E> 11 105 11 01 10
== Executing PPA-CTR 22 (once), V(1)=294773860, V(2)=4
2652963635    2979141[4]4303714           -589547504  01 (01)(01)E> 11294773871 10 11
== Executing  PA-CTR  1, V(1)=0, V(2)=294773867, repcount=98257956, factor=4/3
3537285239    5296251[4]9320154                  232  01393031825 (01)(01)E> 113 10 11
== Executing PPA-CTR  4 (once), V(1)=393031824
3537285262    5296251[4]1765860           -786063418  013 (01)(01)E> 11393031831 01 10
== Executing  PA-CTR  1, V(1)=2, V(2)=393031827, repcount=131010610, factor=4/3
4716380752    9415559[4]4238960                  242  01524042443 (01)(01)E> 11 01 10
== Executing PPA-CTR 16 (once), V(1)=524042440
4716380765    9415559[4]6578564          -1048084646  01 (01)(01)E> 11524042444 10 11 10 11
== Executing  PA-CTR  6, V(1)=0, V(2)=524042440, repcount=174680814, factor=4/3
6288508091    1673877[5]4758312                  238  01698723257 (01)(01)E> 112 10 11 10 11
== Executing PPA-CTR 17 (once), V(1)=698723255
6288508120    1673877[5]6884068          -1397446276  013 (01)(01)E> 11698723259 01 114 01 10
== Executing  PA-CTR  6, V(1)=2, V(2)=698723255, repcount=232907752, factor=4/3
8384677888    2975781[5]1070804                  236  01931631011 (01)(01)E> 113 01 114 01 10
8384677889    2975781[5]1070811                  231  01931631011 <A(10)(10) 10 112 01 114 01 10
8384677890    2975781[5]4332833          -1863261791  <A(10)(10) 10931631012 112 01 114 01 10
8384677891    2975781[5]4332842          -1863261786  (10)(11)F> 10931631012 112 01 114 01 10
8384677892    2975781[5]0856890                  238  10931631012 (10)(11)F> 112 01 114 01 10
8384677893    2975781[5]0856894                  240  10931631013 (10)(10)A> 11 01 114 01 10
8384677894    2975781[5]0856899                  235  10931631013 <B(01)(01) 012 114 01 10
8384677895    2975781[5]4118925          -1863261791  <B(01)(01) 01931631015 114 01 10
8384677896    2975781[5]4118938          -1863261786  01 (01)(01)E> 01931631015 114 01 10
8384677897    2975781[5]0642998                  244  01931631016 (01)(01)E> 114 01 10
>> Try to prove a PPA-CTR with 3 Vars...
    0                    0                    0  011+V(1) (01)(01)E> 113 011+V(3) 114+V(2) [*]* [*]*
    1                    7                   -5  011+V(1) <A(10)(10) 10 112 011+V(3) 114+V(2) [*]* [*]*
    2             9+2*V(1)           -7+-2*V(1)  <A(10)(10) 102+V(1) 112 011+V(3) 114+V(2) [*]* [*]*
    3            18+2*V(1)           -2+-2*V(1)  (10)(11)F> 102+V(1) 112 011+V(3) 114+V(2) [*]* [*]*
    4            26+6*V(1)                    2  102+V(1) (10)(11)F> 112 011+V(3) 114+V(2) [*]* [*]*
    5            30+6*V(1)                    4  103+V(1) (10)(10)A> 11 011+V(3) 114+V(2) [*]* [*]*
    6            35+6*V(1)                   -1  103+V(1) <B(01)(01) 012+V(3) 114+V(2) [*]* [*]*
    7            41+8*V(1)           -7+-2*V(1)  <B(01)(01) 015+V(1)+V(3) 114+V(2) [*]* [*]*
    8            54+8*V(1)           -2+-2*V(1)  01 (01)(01)E> 015+V(1)+V(3) 114+V(2) [*]* [*]*
    9    74+12*V(1)+4*V(3)             8+2*V(3)  016+V(1)+V(3) (01)(01)E> 114+V(2) [*]* [*]*
<< Success! ==> defined new CTR 23 (PPA)
8384677897    2975781[5]0642998                  244  01931631016 (01)(01)E> 114 01 10
== Executing  PA-CTR  1, V(1)=931631015, V(2)=0, repcount=1, factor=4/3
8384677906    2975781[5]0215248                  250  01931631020 (01)(01)E> 11 01 10
== Executing PPA-CTR 16 (once), V(1)=931631017
8384677919    2975781[5]3263468          -1863261792  01 (01)(01)E> 11931631021 10 11 10 11
== Executing  PA-CTR  6, V(1)=0, V(2)=931631017, repcount=310543673, factor=4/3
11179570976    5290278[5]6214722                  246  011242174693 (01)(01)E> 112 10 11 10 11
== Executing PPA-CTR 17 (once), V(1)=1242174691
11179571005    5290278[5]6660582          -2484349140  013 (01)(01)E> 111242174695 01 114 01 10
== Executing  PA-CTR  6, V(1)=2, V(2)=1242174691, repcount=414058231, factor=4/3
14906095084    9404940[5]3121416                  246  011656232927 (01)(01)E> 112 01 114 01 10
== Executing PPA-CTR 21 (once), V(1)=1656232926
14906095109    9404940[5]7780170          -3312465612  01 (01)(01)E> 111656232935 10 11 10 11
== Executing  PA-CTR  6, V(1)=0, V(2)=1656232931, repcount=552077644, factor=4/3
19874793905    1671989[6]3529458                  252  012208310577 (01)(01)E> 113 10 11 10 11
== Executing PPA-CTR  7 (once), V(1)=2208310576
19874793931    1671989[6]9877692          -4416620902  013 (01)(01)E> 112208310582 01 11 01 10
== Executing  PA-CTR  6, V(1)=2, V(2)=2208310578, repcount=736103527, factor=4/3
26499725674    2972425[6]1278078                  260  012944414111 (01)(01)E> 11 01 11 01 10
== Executing PPA-CTR  9 (once), V(1)=2944414108
26499725695    2972425[6]6591056          -5888827964  01 (01)(01)E> 112944414112 10 114 10 11
== Executing  PA-CTR  6, V(1)=0, V(2)=2944414108, repcount=981471370, factor=4/3
35332968025    5284312[6]6519676                  256  013925885481 (01)(01)E> 112 10 114 10 11
== Executing PPA-CTR 15 (once), V(1)=3925885480
35332968046    5284312[6]8916528          -7851770708  10 (10)(10)A> 113925885484 015 10 11
== Executing  PA-CTR 10, V(1)=0, V(2)=3925885480, repcount=1308628494, factor=4/3
47110624492    9394332[6]4820116                  256  105234513977 (10)(10)A> 112 015 10 11
47110624493    9394332[6]4820121                  251  105234513977 <B(01)(01) 01 11 015 10 11
47110624494    9394332[6]3848075         -10469027703  <B(01)(01) 015234513978 11 015 10 11
47110624495    9394332[6]3848088         -10469027698  01 (01)(01)E> 015234513978 11 015 10 11
47110624496    9394332[6]1904000                  258  015234513979 (01)(01)E> 11 015 10 11
47110624497    9394332[6]1904007                  253  015234513979 <A(10)(10) 10 015 10 11
47110624498    9394332[6]0931965         -10469027705  <A(10)(10) 105234513980 015 10 11
47110624499    9394332[6]0931974         -10469027700  (10)(11)F> 105234513980 015 10 11
47110624500    9394332[6]8987894                  260  105234513980 (10)(11)F> 015 10 11
47110624501    9394332[6]8987896                  262  105234513981 (11)(00)D> 014 10 11
47110624502    9394332[6]8987897                  263  105234513981 11001 Z> 1 013 10 11   [stop]

Lines:       639
Top steps:   638
Macro steps: 47110624502
Basic steps: 93943325529148987897
Tape index:  263
ones:        5234513991
log10(ones    ):    9.719
log10(steps   ):   19.973
Run state:   stop

Some long numbers above are shortened: #(omitted digits) shown in "[]".

The same TM just simple.
The same TM with repetitions reduced.
The same TM with tape symbol exponents.
The same TM as 2-bck-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
    L 12
    5T B1R B0L A1L C1L B1L D0R Z1R E1R F1R A0R C0R C1L : 5234513991 93943325529148987897
    T 6-state TM #d from MaBu-List
    M	650
    pref	sim
    machv mbL6_d  	just simple
    machv mbL6_d-r	with repetitions reduced
    machv mbL6_d-1	with tape symbol exponents
    machv mbL6_d-m	as 2-bck-bck-macro machine
    machv mbL6_d-a	as 2-bck-bck-macro machine with pure additive config-TRs
    iam	mbL6_d-a
    mtype	2 0 0
    mmtyp	3
    r	1
    H	1
    mac	0
    E	2
    sympr	
    HM	1
    date	Tue Jul  6 22:10:44 CEST 2010
    edate	Tue Jul  6 22:10:47 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:10:44 CEST 2010
Ready: Tue Jul 6 22:10:47 CEST 2010