6-state TM #3 from MaBu-List

Comment: This TM produces 2,537,699,363,594,175,843,063 ones in >5.3*10^42 steps.

State on
0
on
1
on 0 on 1
Print Move Goto Print Move Goto
A B1R C0R 1 right B 0 right C
B A0L D0R 0 left A 0 right D
C D1R H1R 1 right D 1 right H
D E1L D0L 1 left E 0 left D
E F1R B1L 1 right F 1 left B
F A1R E1R 1 right A 1 right E
Transition table
The same TM just simple.
The same TM with repetitions reduced.
The same TM with tape symbol exponents.
The same TM as 2-bck-macro machine.
Simulation is done as 2-bck-macro machine with pure additive config-TRs.

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

Steps             BasSteps              BasTpos  Tape contents
    0                    0                    0  (00)A>
    1                    4                    2  (01)D>
    2                    7                   -1  <A(01) 10
    3                   18                    2  11 (11)A> 10
    4                   20                    4  112 (01)D>
    5                   23                    1  112 <A(01) 10
    6                   29                   -1  11 <B(11) 00 10
    7                   33                   -3  <B(11) 01 00 10
    8                   41                   -5  <E(10) 012 00 10
    9                   44                   -2  01 (11)F> 012 00 10
   10                   46                    0  01 11 (10)C> 01 00 10
   11                   51                   -3  01 11 <B(11) 002 10
   12                   55                   -5  01 <B(11) 01 002 10
   13                   62                   -2  11 (11)E> 01 002 10
   14                   64                    0  112 (11)E> 002 10
   15                   66                    2  113 (11)A> 00 10
   16                   70                    4  114 (01)D> 10
   17                   73                    1  114 <E(10)
   18                   89                   -7  <E(10) 104
   19                   92                   -4  01 (11)F> 104
   20                  100                    4  01 114 (11)F>
   21                  102                    6  01 115 (11)B>
   22                  113                    3  01 115 <E(10) 01
   23                  133                   -7  01 <E(10) 105 01
   24                  135                   -9  <A(01) 106 01
   25                  146                   -6  11 (11)A> 106 01
   26                  148                   -4  112 (01)D> 105 01
   27                  151                   -7  112 <E(10) 00 104 01
   28                  159                  -11  <E(10) 102 00 104 01
   29                  162                   -8  01 (11)F> 102 00 104 01
   30                  166                   -4  01 112 (11)F> 00 104 01
   31                  168                   -2  01 113 (11)B> 104 01
   32                  172                    0  01 114 (11)E> 103 01
   33                  177                   -3  01 114 <B(11) 00 102 01
   34                  193                  -11  01 <B(11) 014 00 102 01
   35                  200                   -8  11 (11)E> 014 00 102 01
   36                  208                    0  115 (11)E> 00 102 01
   37                  210                    2  116 (11)A> 102 01
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  111+V(1) (11)A> 105+V(2) [*]*
    1                    2                    2  112+V(1) (01)D> 104+V(2) [*]*
    2                    5                   -1  112+V(1) <E(10) 00 103+V(2) [*]*
    3            13+4*V(1)           -5+-2*V(1)  <E(10) 102+V(1) 00 103+V(2) [*]*
    4            16+4*V(1)           -2+-2*V(1)  01 (11)F> 102+V(1) 00 103+V(2) [*]*
    5            20+6*V(1)                    2  01 112+V(1) (11)F> 00 103+V(2) [*]*
    6            22+6*V(1)                    4  01 113+V(1) (11)B> 103+V(2) [*]*
    7            26+6*V(1)                    6  01 114+V(1) (11)E> 102+V(2) [*]*
    8            31+6*V(1)                    3  01 114+V(1) <B(11) 00 101+V(2) [*]*
    9           47+10*V(1)           -5+-2*V(1)  01 <B(11) 014+V(1) 00 101+V(2) [*]*
   10           54+10*V(1)           -2+-2*V(1)  11 (11)E> 014+V(1) 00 101+V(2) [*]*
   11           62+12*V(1)                    6  115+V(1) (11)E> 00 101+V(2) [*]*
   12           64+12*V(1)                    8  116+V(1) (11)A> 101+V(2) [*]*
<< Success! ==> defined new CTR 1 (PA)
   38                  212                    4  117 (01)D> 10 01
   39                  215                    1  117 <E(10) 00 01
   40                  243                  -13  <E(10) 107 00 01
   41                  246                  -10  01 (11)F> 107 00 01
   42                  260                    4  01 117 (11)F> 00 01
   43                  262                    6  01 118 (11)B> 01
   44                  269                    3  01 118 <B(11)
   45                  301                  -13  01 <B(11) 018
   46                  308                  -10  11 (11)E> 018
   47                  324                    6  119 (11)E>
   48                  326                    8  1110 (11)A>
   49                  330                   10  1111 (01)D>
   50                  333                    7  1111 <A(01) 10
   51                  339                    5  1110 <B(11) 00 10
   52                  379                  -15  <B(11) 0110 00 10
   53                  387                  -17  <E(10) 0111 00 10
   54                  390                  -14  01 (11)F> 0111 00 10
   55                  392                  -12  01 11 (10)C> 0110 00 10
   56                  397                  -15  01 11 <B(11) 00 019 00 10
   57                  401                  -17  01 <B(11) 01 00 019 00 10
   58                  408                  -14  11 (11)E> 01 00 019 00 10
   59                  410                  -12  112 (11)E> 00 019 00 10
   60                  412                  -10  113 (11)A> 019 00 10
   61                  414                   -8  114 (10)D> 018 00 10
   62                  425                  -11  114 <E(10) 10 017 00 10
   63                  441                  -19  <E(10) 105 017 00 10
   64                  444                  -16  01 (11)F> 105 017 00 10
   65                  454                   -6  01 115 (11)F> 017 00 10
   66                  456                   -4  01 116 (10)C> 016 00 10
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  01 111+V(1) (10)C> 015+V(2) [*]* [*]*
    1                    5                   -3  01 111+V(1) <B(11) 00 014+V(2) [*]* [*]*
    2             9+4*V(1)           -5+-2*V(1)  01 <B(11) 011+V(1) 00 014+V(2) [*]* [*]*
    3            16+4*V(1)           -2+-2*V(1)  11 (11)E> 011+V(1) 00 014+V(2) [*]* [*]*
    4            18+6*V(1)                    0  112+V(1) (11)E> 00 014+V(2) [*]* [*]*
    5            20+6*V(1)                    2  113+V(1) (11)A> 014+V(2) [*]* [*]*
    6            22+6*V(1)                    4  114+V(1) (10)D> 013+V(2) [*]* [*]*
    7            33+6*V(1)                    1  114+V(1) <E(10) 10 012+V(2) [*]* [*]*
    8           49+10*V(1)           -7+-2*V(1)  <E(10) 105+V(1) 012+V(2) [*]* [*]*
    9           52+10*V(1)           -4+-2*V(1)  01 (11)F> 105+V(1) 012+V(2) [*]* [*]*
   10           62+12*V(1)                    6  01 115+V(1) (11)F> 012+V(2) [*]* [*]*
   11           64+12*V(1)                    8  01 116+V(1) (10)C> 011+V(2) [*]* [*]*
<< Success! ==> defined new CTR 2 (PA)
   66                  456                   -4  01 116 (10)C> 016 00 10
== Executing  PA-CTR  2, V(1)=5, V(2)=1, repcount=1, factor=5/4
   77                  580                    4  01 1111 (10)C> 012 00 10
   78                  585                    1  01 1111 <B(11) 00 01 00 10
   79                  629                  -21  01 <B(11) 0111 00 01 00 10
   80                  636                  -18  11 (11)E> 0111 00 01 00 10
   81                  658                    4  1112 (11)E> 00 01 00 10
   82                  660                    6  1113 (11)A> 01 00 10
   83                  662                    8  1114 (10)D> 00 10
   84                  666                   10  1115 (11)F> 10
   85                  668                   12  1116 (11)F>
   86                  670                   14  1117 (11)B>
   87                  681                   11  1117 <E(10) 01
   88                  749                  -23  <E(10) 1017 01
   89                  752                  -20  01 (11)F> 1017 01
   90                  786                   14  01 1117 (11)F> 01
   91                  788                   16  01 1118 (10)C>
   92                  797                   13  01 1118 <E(10) 01
   93                  869                  -23  01 <E(10) 1018 01
   94                  871                  -25  <A(01) 1019 01
   95                  882                  -22  11 (11)A> 1019 01
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  01 111+V(1) (10)C> 012 00 101+V(2)
    1                    5                   -3  01 111+V(1) <B(11) 00 01 00 101+V(2)
    2             9+4*V(1)           -5+-2*V(1)  01 <B(11) 011+V(1) 00 01 00 101+V(2)
    3            16+4*V(1)           -2+-2*V(1)  11 (11)E> 011+V(1) 00 01 00 101+V(2)
    4            18+6*V(1)                    0  112+V(1) (11)E> 00 01 00 101+V(2)
    5            20+6*V(1)                    2  113+V(1) (11)A> 01 00 101+V(2)
    6            22+6*V(1)                    4  114+V(1) (10)D> 00 101+V(2)
    7            26+6*V(1)                    6  115+V(1) (11)F> 101+V(2)
    8     28+6*V(1)+2*V(2)             8+2*V(2)  116+V(1)+V(2) (11)F>
    9     30+6*V(1)+2*V(2)            10+2*V(2)  117+V(1)+V(2) (11)B>
   10     41+6*V(1)+2*V(2)             7+2*V(2)  117+V(1)+V(2) <E(10) 01
   11    69+10*V(1)+6*V(2)           -7+-2*V(1)  <E(10) 107+V(1)+V(2) 01
   12    72+10*V(1)+6*V(2)           -4+-2*V(1)  01 (11)F> 107+V(1)+V(2) 01
   13    86+12*V(1)+8*V(2)            10+2*V(2)  01 117+V(1)+V(2) (11)F> 01
   14    88+12*V(1)+8*V(2)            12+2*V(2)  01 118+V(1)+V(2) (10)C>
   15    97+12*V(1)+8*V(2)             9+2*V(2)  01 118+V(1)+V(2) <E(10) 01
   16  129+16*V(1)+12*V(2)           -7+-2*V(1)  01 <E(10) 108+V(1)+V(2) 01
   17  131+16*V(1)+12*V(2)           -9+-2*V(1)  <A(01) 109+V(1)+V(2) 01
   18  142+16*V(1)+12*V(2)           -6+-2*V(1)  11 (11)A> 109+V(1)+V(2) 01
<< Success! ==> defined new CTR 3 (PPA)
   95                  882                  -22  11 (11)A> 1019 01
== Executing  PA-CTR  1, V(1)=0, V(2)=14, repcount=4, factor=5/4
  143                 1498                   10  1121 (11)A> 103 01
  144                 1500                   12  1122 (01)D> 102 01
  145                 1503                    9  1122 <E(10) 00 10 01
  146                 1591                  -35  <E(10) 1022 00 10 01
  147                 1594                  -32  01 (11)F> 1022 00 10 01
  148                 1638                   12  01 1122 (11)F> 00 10 01
  149                 1640                   14  01 1123 (11)B> 10 01
  150                 1644                   16  01 1124 (11)E> 01
  151                 1646                   18  01 1125 (11)E>
  152                 1648                   20  01 1126 (11)A>
  153                 1652                   22  01 1127 (01)D>
  154                 1655                   19  01 1127 <A(01) 10
  155                 1661                   17  01 1126 <B(11) 00 10
  156                 1765                  -35  01 <B(11) 0126 00 10
  157                 1772                  -32  11 (11)E> 0126 00 10
  158                 1824                   20  1127 (11)E> 00 10
  159                 1826                   22  1128 (11)A> 10
  160                 1828                   24  1129 (01)D>
  161                 1831                   21  1129 <A(01) 10
  162                 1837                   19  1128 <B(11) 00 10
  163                 1949                  -37  <B(11) 0128 00 10
  164                 1957                  -39  <E(10) 0129 00 10
  165                 1960                  -36  01 (11)F> 0129 00 10
  166                 1962                  -34  01 11 (10)C> 0128 00 10
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  111+V(1) (11)A> 103 011+V(2)
    1                    2                    2  112+V(1) (01)D> 102 011+V(2)
    2                    5                   -1  112+V(1) <E(10) 00 10 011+V(2)
    3            13+4*V(1)           -5+-2*V(1)  <E(10) 102+V(1) 00 10 011+V(2)
    4            16+4*V(1)           -2+-2*V(1)  01 (11)F> 102+V(1) 00 10 011+V(2)
    5            20+6*V(1)                    2  01 112+V(1) (11)F> 00 10 011+V(2)
    6            22+6*V(1)                    4  01 113+V(1) (11)B> 10 011+V(2)
    7            26+6*V(1)                    6  01 114+V(1) (11)E> 011+V(2)
    8     28+6*V(1)+2*V(2)             8+2*V(2)  01 115+V(1)+V(2) (11)E>
    9     30+6*V(1)+2*V(2)            10+2*V(2)  01 116+V(1)+V(2) (11)A>
   10     34+6*V(1)+2*V(2)            12+2*V(2)  01 117+V(1)+V(2) (01)D>
   11     37+6*V(1)+2*V(2)             9+2*V(2)  01 117+V(1)+V(2) <A(01) 10
   12     43+6*V(1)+2*V(2)             7+2*V(2)  01 116+V(1)+V(2) <B(11) 00 10
   13    67+10*V(1)+6*V(2)           -5+-2*V(1)  01 <B(11) 016+V(1)+V(2) 00 10
   14    74+10*V(1)+6*V(2)           -2+-2*V(1)  11 (11)E> 016+V(1)+V(2) 00 10
   15    86+12*V(1)+8*V(2)            10+2*V(2)  117+V(1)+V(2) (11)E> 00 10
   16    88+12*V(1)+8*V(2)            12+2*V(2)  118+V(1)+V(2) (11)A> 10
   17    90+12*V(1)+8*V(2)            14+2*V(2)  119+V(1)+V(2) (01)D>
   18    93+12*V(1)+8*V(2)            11+2*V(2)  119+V(1)+V(2) <A(01) 10
   19    99+12*V(1)+8*V(2)             9+2*V(2)  118+V(1)+V(2) <B(11) 00 10
   20  131+16*V(1)+12*V(2)           -7+-2*V(1)  <B(11) 018+V(1)+V(2) 00 10
   21  139+16*V(1)+12*V(2)           -9+-2*V(1)  <E(10) 019+V(1)+V(2) 00 10
   22  142+16*V(1)+12*V(2)           -6+-2*V(1)  01 (11)F> 019+V(1)+V(2) 00 10
   23  144+16*V(1)+12*V(2)           -4+-2*V(1)  01 11 (10)C> 018+V(1)+V(2) 00 10
<< Success! ==> defined new CTR 4 (PPA)
  166                 1962                  -34  01 11 (10)C> 0128 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=23, repcount=6, factor=5/4
  232                 3246                   14  01 1131 (10)C> 014 00 10
  233                 3251                   11  01 1131 <B(11) 00 013 00 10
  234                 3375                  -51  01 <B(11) 0131 00 013 00 10
  235                 3382                  -48  11 (11)E> 0131 00 013 00 10
  236                 3444                   14  1132 (11)E> 00 013 00 10
  237                 3446                   16  1133 (11)A> 013 00 10
  238                 3448                   18  1134 (10)D> 012 00 10
  239                 3459                   15  1134 <E(10) 10 01 00 10
  240                 3595                  -53  <E(10) 1035 01 00 10
  241                 3598                  -50  01 (11)F> 1035 01 00 10
  242                 3668                   20  01 1135 (11)F> 01 00 10
  243                 3670                   22  01 1136 (10)C> 00 10
  244                 3679                   19  01 1136 <E(10) 01 10
  245                 3823                  -53  01 <E(10) 1036 01 10
  246                 3825                  -55  <A(01) 1037 01 10
  247                 3836                  -52  11 (11)A> 1037 01 10
  248                 3838                  -50  112 (01)D> 1036 01 10
  249                 3841                  -53  112 <E(10) 00 1035 01 10
  250                 3849                  -57  <E(10) 102 00 1035 01 10
  251                 3852                  -54  01 (11)F> 102 00 1035 01 10
  252                 3856                  -50  01 112 (11)F> 00 1035 01 10
  253                 3858                  -48  01 113 (11)B> 1035 01 10
  254                 3862                  -46  01 114 (11)E> 1034 01 10
  255                 3867                  -49  01 114 <B(11) 00 1033 01 10
  256                 3883                  -57  01 <B(11) 014 00 1033 01 10
  257                 3890                  -54  11 (11)E> 014 00 1033 01 10
  258                 3898                  -46  115 (11)E> 00 1033 01 10
  259                 3900                  -44  116 (11)A> 1033 01 10
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  111+V(1) (11)A> 105+V(2) [*]* [*]*
    1                    2                    2  112+V(1) (01)D> 104+V(2) [*]* [*]*
    2                    5                   -1  112+V(1) <E(10) 00 103+V(2) [*]* [*]*
    3            13+4*V(1)           -5+-2*V(1)  <E(10) 102+V(1) 00 103+V(2) [*]* [*]*
    4            16+4*V(1)           -2+-2*V(1)  01 (11)F> 102+V(1) 00 103+V(2) [*]* [*]*
    5            20+6*V(1)                    2  01 112+V(1) (11)F> 00 103+V(2) [*]* [*]*
    6            22+6*V(1)                    4  01 113+V(1) (11)B> 103+V(2) [*]* [*]*
    7            26+6*V(1)                    6  01 114+V(1) (11)E> 102+V(2) [*]* [*]*
    8            31+6*V(1)                    3  01 114+V(1) <B(11) 00 101+V(2) [*]* [*]*
    9           47+10*V(1)           -5+-2*V(1)  01 <B(11) 014+V(1) 00 101+V(2) [*]* [*]*
   10           54+10*V(1)           -2+-2*V(1)  11 (11)E> 014+V(1) 00 101+V(2) [*]* [*]*
   11           62+12*V(1)                    6  115+V(1) (11)E> 00 101+V(2) [*]* [*]*
   12           64+12*V(1)                    8  116+V(1) (11)A> 101+V(2) [*]* [*]*
<< Success! ==> defined new CTR 5 (PA)
  259                 3900                  -44  116 (11)A> 1033 01 10
== Executing  PA-CTR  5, V(1)=5, V(2)=28, repcount=8, factor=5/4
  355                 6572                   20  1146 (11)A> 10 01 10
  356                 6574                   22  1147 (01)D> 01 10
  357                 6577                   19  1147 <A(01) 11 10
  358                 6583                   17  1146 <B(11) 00 11 10
  359                 6767                  -75  <B(11) 0146 00 11 10
  360                 6775                  -77  <E(10) 0147 00 11 10
  361                 6778                  -74  01 (11)F> 0147 00 11 10
  362                 6780                  -72  01 11 (10)C> 0146 00 11 10
  363                 6785                  -75  01 11 <B(11) 00 0145 00 11 10
  364                 6789                  -77  01 <B(11) 01 00 0145 00 11 10
  365                 6796                  -74  11 (11)E> 01 00 0145 00 11 10
  366                 6798                  -72  112 (11)E> 00 0145 00 11 10
  367                 6800                  -70  113 (11)A> 0145 00 11 10
  368                 6802                  -68  114 (10)D> 0144 00 11 10
  369                 6813                  -71  114 <E(10) 10 0143 00 11 10
  370                 6829                  -79  <E(10) 105 0143 00 11 10
  371                 6832                  -76  01 (11)F> 105 0143 00 11 10
  372                 6842                  -66  01 115 (11)F> 0143 00 11 10
  373                 6844                  -64  01 116 (10)C> 0142 00 11 10
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  01 111+V(1) (10)C> 015+V(2) [*]* [*]* [*]*
    1                    5                   -3  01 111+V(1) <B(11) 00 014+V(2) [*]* [*]* [*]*
    2             9+4*V(1)           -5+-2*V(1)  01 <B(11) 011+V(1) 00 014+V(2) [*]* [*]* [*]*
    3            16+4*V(1)           -2+-2*V(1)  11 (11)E> 011+V(1) 00 014+V(2) [*]* [*]* [*]*
    4            18+6*V(1)                    0  112+V(1) (11)E> 00 014+V(2) [*]* [*]* [*]*
    5            20+6*V(1)                    2  113+V(1) (11)A> 014+V(2) [*]* [*]* [*]*
    6            22+6*V(1)                    4  114+V(1) (10)D> 013+V(2) [*]* [*]* [*]*
    7            33+6*V(1)                    1  114+V(1) <E(10) 10 012+V(2) [*]* [*]* [*]*
    8           49+10*V(1)           -7+-2*V(1)  <E(10) 105+V(1) 012+V(2) [*]* [*]* [*]*
    9           52+10*V(1)           -4+-2*V(1)  01 (11)F> 105+V(1) 012+V(2) [*]* [*]* [*]*
   10           62+12*V(1)                    6  01 115+V(1) (11)F> 012+V(2) [*]* [*]* [*]*
   11           64+12*V(1)                    8  01 116+V(1) (10)C> 011+V(2) [*]* [*]* [*]*
<< Success! ==> defined new CTR 6 (PA)
  373                 6844                  -64  01 116 (10)C> 0142 00 11 10
== Executing  PA-CTR  6, V(1)=5, V(2)=37, repcount=10, factor=5/4
  483                10784                   16  01 1156 (10)C> 012 00 11 10
  484                10789                   13  01 1156 <B(11) 00 01 00 11 10
  485                11013                  -99  01 <B(11) 0156 00 01 00 11 10
  486                11020                  -96  11 (11)E> 0156 00 01 00 11 10
  487                11132                   16  1157 (11)E> 00 01 00 11 10
  488                11134                   18  1158 (11)A> 01 00 11 10
  489                11136                   20  1159 (10)D> 00 11 10
  490                11140                   22  1160 (11)F> 11 10
  491                11149                   19  1160 <E(10) 102
  492                11389                 -101  <E(10) 1062
  493                11392                  -98  01 (11)F> 1062
  494                11516                   26  01 1162 (11)F>
  495                11518                   28  01 1163 (11)B>
  496                11529                   25  01 1163 <E(10) 01
  497                11781                 -101  01 <E(10) 1063 01
  498                11783                 -103  <A(01) 1064 01
  499                11794                 -100  11 (11)A> 1064 01
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  01 111+V(1) (10)C> 012 00 11 101+V(2)
    1                    5                   -3  01 111+V(1) <B(11) 00 01 00 11 101+V(2)
    2             9+4*V(1)           -5+-2*V(1)  01 <B(11) 011+V(1) 00 01 00 11 101+V(2)
    3            16+4*V(1)           -2+-2*V(1)  11 (11)E> 011+V(1) 00 01 00 11 101+V(2)
    4            18+6*V(1)                    0  112+V(1) (11)E> 00 01 00 11 101+V(2)
    5            20+6*V(1)                    2  113+V(1) (11)A> 01 00 11 101+V(2)
    6            22+6*V(1)                    4  114+V(1) (10)D> 00 11 101+V(2)
    7            26+6*V(1)                    6  115+V(1) (11)F> 11 101+V(2)
    8            35+6*V(1)                    3  115+V(1) <E(10) 102+V(2)
    9           55+10*V(1)           -7+-2*V(1)  <E(10) 107+V(1)+V(2)
   10           58+10*V(1)           -4+-2*V(1)  01 (11)F> 107+V(1)+V(2)
   11    72+12*V(1)+2*V(2)            10+2*V(2)  01 117+V(1)+V(2) (11)F>
   12    74+12*V(1)+2*V(2)            12+2*V(2)  01 118+V(1)+V(2) (11)B>
   13    85+12*V(1)+2*V(2)             9+2*V(2)  01 118+V(1)+V(2) <E(10) 01
   14   117+16*V(1)+6*V(2)           -7+-2*V(1)  01 <E(10) 108+V(1)+V(2) 01
   15   119+16*V(1)+6*V(2)           -9+-2*V(1)  <A(01) 109+V(1)+V(2) 01
   16   130+16*V(1)+6*V(2)           -6+-2*V(1)  11 (11)A> 109+V(1)+V(2) 01
<< Success! ==> defined new CTR 7 (PPA)
  499                11794                 -100  11 (11)A> 1064 01
== Executing  PA-CTR  1, V(1)=0, V(2)=59, repcount=15, factor=5/4
  679                19054                   20  1176 (11)A> 104 01
  680                19056                   22  1177 (01)D> 103 01
  681                19059                   19  1177 <E(10) 00 102 01
  682                19367                 -135  <E(10) 1077 00 102 01
  683                19370                 -132  01 (11)F> 1077 00 102 01
  684                19524                   22  01 1177 (11)F> 00 102 01
  685                19526                   24  01 1178 (11)B> 102 01
  686                19530                   26  01 1179 (11)E> 10 01
  687                19535                   23  01 1179 <B(11) 00 01
  688                19851                 -135  01 <B(11) 0179 00 01
  689                19858                 -132  11 (11)E> 0179 00 01
  690                20016                   26  1180 (11)E> 00 01
  691                20018                   28  1181 (11)A> 01
  692                20020                   30  1182 (10)D>
  693                20024                   32  1183 (11)F>
  694                20026                   34  1184 (11)B>
  695                20037                   31  1184 <E(10) 01
  696                20373                 -137  <E(10) 1084 01
  697                20376                 -134  01 (11)F> 1084 01
  698                20544                   34  01 1184 (11)F> 01
  699                20546                   36  01 1185 (10)C>
  700                20555                   33  01 1185 <E(10) 01
  701                20895                 -137  01 <E(10) 1085 01
  702                20897                 -139  <A(01) 1086 01
  703                20908                 -136  11 (11)A> 1086 01
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  111+V(1) (11)A> 104 01
    1                    2                    2  112+V(1) (01)D> 103 01
    2                    5                   -1  112+V(1) <E(10) 00 102 01
    3            13+4*V(1)           -5+-2*V(1)  <E(10) 102+V(1) 00 102 01
    4            16+4*V(1)           -2+-2*V(1)  01 (11)F> 102+V(1) 00 102 01
    5            20+6*V(1)                    2  01 112+V(1) (11)F> 00 102 01
    6            22+6*V(1)                    4  01 113+V(1) (11)B> 102 01
    7            26+6*V(1)                    6  01 114+V(1) (11)E> 10 01
    8            31+6*V(1)                    3  01 114+V(1) <B(11) 00 01
    9           47+10*V(1)           -5+-2*V(1)  01 <B(11) 014+V(1) 00 01
   10           54+10*V(1)           -2+-2*V(1)  11 (11)E> 014+V(1) 00 01
   11           62+12*V(1)                    6  115+V(1) (11)E> 00 01
   12           64+12*V(1)                    8  116+V(1) (11)A> 01
   13           66+12*V(1)                   10  117+V(1) (10)D>
   14           70+12*V(1)                   12  118+V(1) (11)F>
   15           72+12*V(1)                   14  119+V(1) (11)B>
   16           83+12*V(1)                   11  119+V(1) <E(10) 01
   17          119+16*V(1)           -7+-2*V(1)  <E(10) 109+V(1) 01
   18          122+16*V(1)           -4+-2*V(1)  01 (11)F> 109+V(1) 01
   19          140+18*V(1)                   14  01 119+V(1) (11)F> 01
   20          142+18*V(1)                   16  01 1110+V(1) (10)C>
   21          151+18*V(1)                   13  01 1110+V(1) <E(10) 01
   22          191+22*V(1)           -7+-2*V(1)  01 <E(10) 1010+V(1) 01
   23          193+22*V(1)           -9+-2*V(1)  <A(01) 1011+V(1) 01
   24          204+22*V(1)           -6+-2*V(1)  11 (11)A> 1011+V(1) 01
<< Success! ==> defined new CTR 8 (PPA)
  703                20908                 -136  11 (11)A> 1086 01
== Executing  PA-CTR  1, V(1)=0, V(2)=81, repcount=21, factor=5/4
  955                34852                   32  11106 (11)A> 102 01
  956                34854                   34  11107 (01)D> 10 01
  957                34857                   31  11107 <E(10) 00 01
  958                35285                 -183  <E(10) 10107 00 01
  959                35288                 -180  01 (11)F> 10107 00 01
  960                35502                   34  01 11107 (11)F> 00 01
  961                35504                   36  01 11108 (11)B> 01
  962                35511                   33  01 11108 <B(11)
  963                35943                 -183  01 <B(11) 01108
  964                35950                 -180  11 (11)E> 01108
  965                36166                   36  11109 (11)E>
  966                36168                   38  11110 (11)A>
  967                36172                   40  11111 (01)D>
  968                36175                   37  11111 <A(01) 10
  969                36181                   35  11110 <B(11) 00 10
  970                36621                 -185  <B(11) 01110 00 10
  971                36629                 -187  <E(10) 01111 00 10
  972                36632                 -184  01 (11)F> 01111 00 10
  973                36634                 -182  01 11 (10)C> 01110 00 10
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  111+V(1) (11)A> 102 01
    1                    2                    2  112+V(1) (01)D> 10 01
    2                    5                   -1  112+V(1) <E(10) 00 01
    3            13+4*V(1)           -5+-2*V(1)  <E(10) 102+V(1) 00 01
    4            16+4*V(1)           -2+-2*V(1)  01 (11)F> 102+V(1) 00 01
    5            20+6*V(1)                    2  01 112+V(1) (11)F> 00 01
    6            22+6*V(1)                    4  01 113+V(1) (11)B> 01
    7            29+6*V(1)                    1  01 113+V(1) <B(11)
    8           41+10*V(1)           -5+-2*V(1)  01 <B(11) 013+V(1)
    9           48+10*V(1)           -2+-2*V(1)  11 (11)E> 013+V(1)
   10           54+12*V(1)                    4  114+V(1) (11)E>
   11           56+12*V(1)                    6  115+V(1) (11)A>
   12           60+12*V(1)                    8  116+V(1) (01)D>
   13           63+12*V(1)                    5  116+V(1) <A(01) 10
   14           69+12*V(1)                    3  115+V(1) <B(11) 00 10
   15           89+16*V(1)           -7+-2*V(1)  <B(11) 015+V(1) 00 10
   16           97+16*V(1)           -9+-2*V(1)  <E(10) 016+V(1) 00 10
   17          100+16*V(1)           -6+-2*V(1)  01 (11)F> 016+V(1) 00 10
   18          102+16*V(1)           -4+-2*V(1)  01 11 (10)C> 015+V(1) 00 10
<< Success! ==> defined new CTR 9 (PPA)
  973                36634                 -182  01 11 (10)C> 01110 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=105, repcount=27, factor=5/4
 1270                59422                   34  01 11136 (10)C> 012 00 10
== Executing PPA-CTR  3 (once), V(1)=135, V(2)=0
 1288                61724                 -242  11 (11)A> 10144 01
== Executing  PA-CTR  1, V(1)=0, V(2)=139, repcount=35, factor=5/4
 1708                99664                   38  11176 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=175
 1732               103718                 -318  11 (11)A> 10186 01
== Executing  PA-CTR  1, V(1)=0, V(2)=181, repcount=46, factor=5/4
 2284               168762                   50  11231 (11)A> 102 01
== Executing PPA-CTR  9 (once), V(1)=230
 2302               172544                 -414  01 11 (10)C> 01235 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=230, repcount=58, factor=5/4
 2940               275436                   50  01 11291 (10)C> 013 00 10
 2941               275441                   47  01 11291 <B(11) 00 012 00 10
 2942               276605                 -535  01 <B(11) 01291 00 012 00 10
 2943               276612                 -532  11 (11)E> 01291 00 012 00 10
 2944               277194                   50  11292 (11)E> 00 012 00 10
 2945               277196                   52  11293 (11)A> 012 00 10
 2946               277198                   54  11294 (10)D> 01 00 10
 2947               277209                   51  11294 <E(10) 10 00 10
 2948               278385                 -537  <E(10) 10295 00 10
 2949               278388                 -534  01 (11)F> 10295 00 10
 2950               278978                   56  01 11295 (11)F> 00 10
 2951               278980                   58  01 11296 (11)B> 10
 2952               278984                   60  01 11297 (11)E>
 2953               278986                   62  01 11298 (11)A>
 2954               278990                   64  01 11299 (01)D>
 2955               278993                   61  01 11299 <A(01) 10
 2956               278999                   59  01 11298 <B(11) 00 10
 2957               280191                 -537  01 <B(11) 01298 00 10
 2958               280198                 -534  11 (11)E> 01298 00 10
 2959               280794                   62  11299 (11)E> 00 10
 2960               280796                   64  11300 (11)A> 10
 2961               280798                   66  11301 (01)D>
 2962               280801                   63  11301 <A(01) 10
 2963               280807                   61  11300 <B(11) 00 10
 2964               282007                 -539  <B(11) 01300 00 10
 2965               282015                 -541  <E(10) 01301 00 10
 2966               282018                 -538  01 (11)F> 01301 00 10
 2967               282020                 -536  01 11 (10)C> 01300 00 10
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 111+V(1) (10)C> 013 00 10
    1                    5                   -3  01 111+V(1) <B(11) 00 012 00 10
    2             9+4*V(1)           -5+-2*V(1)  01 <B(11) 011+V(1) 00 012 00 10
    3            16+4*V(1)           -2+-2*V(1)  11 (11)E> 011+V(1) 00 012 00 10
    4            18+6*V(1)                    0  112+V(1) (11)E> 00 012 00 10
    5            20+6*V(1)                    2  113+V(1) (11)A> 012 00 10
    6            22+6*V(1)                    4  114+V(1) (10)D> 01 00 10
    7            33+6*V(1)                    1  114+V(1) <E(10) 10 00 10
    8           49+10*V(1)           -7+-2*V(1)  <E(10) 105+V(1) 00 10
    9           52+10*V(1)           -4+-2*V(1)  01 (11)F> 105+V(1) 00 10
   10           62+12*V(1)                    6  01 115+V(1) (11)F> 00 10
   11           64+12*V(1)                    8  01 116+V(1) (11)B> 10
   12           68+12*V(1)                   10  01 117+V(1) (11)E>
   13           70+12*V(1)                   12  01 118+V(1) (11)A>
   14           74+12*V(1)                   14  01 119+V(1) (01)D>
   15           77+12*V(1)                   11  01 119+V(1) <A(01) 10
   16           83+12*V(1)                    9  01 118+V(1) <B(11) 00 10
   17          115+16*V(1)           -7+-2*V(1)  01 <B(11) 018+V(1) 00 10
   18          122+16*V(1)           -4+-2*V(1)  11 (11)E> 018+V(1) 00 10
   19          138+18*V(1)                   12  119+V(1) (11)E> 00 10
   20          140+18*V(1)                   14  1110+V(1) (11)A> 10
   21          142+18*V(1)                   16  1111+V(1) (01)D>
   22          145+18*V(1)                   13  1111+V(1) <A(01) 10
   23          151+18*V(1)                   11  1110+V(1) <B(11) 00 10
   24          191+22*V(1)           -9+-2*V(1)  <B(11) 0110+V(1) 00 10
   25          199+22*V(1)          -11+-2*V(1)  <E(10) 0111+V(1) 00 10
   26          202+22*V(1)           -8+-2*V(1)  01 (11)F> 0111+V(1) 00 10
   27          204+22*V(1)           -6+-2*V(1)  01 11 (10)C> 0110+V(1) 00 10
<< Success! ==> defined new CTR 10 (PPA)
 2967               282020                 -536  01 11 (10)C> 01300 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=295, repcount=74, factor=5/4
 3781               448816                   56  01 11371 (10)C> 014 00 10
 3782               448821                   53  01 11371 <B(11) 00 013 00 10
 3783               450305                 -689  01 <B(11) 01371 00 013 00 10
 3784               450312                 -686  11 (11)E> 01371 00 013 00 10
 3785               451054                   56  11372 (11)E> 00 013 00 10
 3786               451056                   58  11373 (11)A> 013 00 10
 3787               451058                   60  11374 (10)D> 012 00 10
 3788               451069                   57  11374 <E(10) 10 01 00 10
 3789               452565                 -691  <E(10) 10375 01 00 10
 3790               452568                 -688  01 (11)F> 10375 01 00 10
 3791               453318                   62  01 11375 (11)F> 01 00 10
 3792               453320                   64  01 11376 (10)C> 00 10
 3793               453329                   61  01 11376 <E(10) 01 10
 3794               454833                 -691  01 <E(10) 10376 01 10
 3795               454835                 -693  <A(01) 10377 01 10
 3796               454846                 -690  11 (11)A> 10377 01 10
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 111+V(1) (10)C> 014 00 [*]*
    1                    5                   -3  01 111+V(1) <B(11) 00 013 00 [*]*
    2             9+4*V(1)           -5+-2*V(1)  01 <B(11) 011+V(1) 00 013 00 [*]*
    3            16+4*V(1)           -2+-2*V(1)  11 (11)E> 011+V(1) 00 013 00 [*]*
    4            18+6*V(1)                    0  112+V(1) (11)E> 00 013 00 [*]*
    5            20+6*V(1)                    2  113+V(1) (11)A> 013 00 [*]*
    6            22+6*V(1)                    4  114+V(1) (10)D> 012 00 [*]*
    7            33+6*V(1)                    1  114+V(1) <E(10) 10 01 00 [*]*
    8           49+10*V(1)           -7+-2*V(1)  <E(10) 105+V(1) 01 00 [*]*
    9           52+10*V(1)           -4+-2*V(1)  01 (11)F> 105+V(1) 01 00 [*]*
   10           62+12*V(1)                    6  01 115+V(1) (11)F> 01 00 [*]*
   11           64+12*V(1)                    8  01 116+V(1) (10)C> 00 [*]*
   12           73+12*V(1)                    5  01 116+V(1) <E(10) 01 [*]*
   13           97+16*V(1)           -7+-2*V(1)  01 <E(10) 106+V(1) 01 [*]*
   14           99+16*V(1)           -9+-2*V(1)  <A(01) 107+V(1) 01 [*]*
   15          110+16*V(1)           -6+-2*V(1)  11 (11)A> 107+V(1) 01 [*]*
<< Success! ==> defined new CTR 11 (PPA)
 3796               454846                 -690  11 (11)A> 10377 01 10
== Executing  PA-CTR  5, V(1)=0, V(2)=372, repcount=94, factor=5/4
 4924               723122                   62  11471 (11)A> 10 01 10
 4925               723124                   64  11472 (01)D> 01 10
 4926               723127                   61  11472 <A(01) 11 10
 4927               723133                   59  11471 <B(11) 00 11 10
 4928               725017                 -883  <B(11) 01471 00 11 10
 4929               725025                 -885  <E(10) 01472 00 11 10
 4930               725028                 -882  01 (11)F> 01472 00 11 10
 4931               725030                 -880  01 11 (10)C> 01471 00 11 10
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  115+V(1) (11)A> 10 01 [*]*
    1                    2                    2  116+V(1) (01)D> 01 [*]*
    2                    5                   -1  116+V(1) <A(01) 11 [*]*
    3                   11                   -3  115+V(1) <B(11) 00 11 [*]*
    4            31+4*V(1)          -13+-2*V(1)  <B(11) 015+V(1) 00 11 [*]*
    5            39+4*V(1)          -15+-2*V(1)  <E(10) 016+V(1) 00 11 [*]*
    6            42+4*V(1)          -12+-2*V(1)  01 (11)F> 016+V(1) 00 11 [*]*
    7            44+4*V(1)          -10+-2*V(1)  01 11 (10)C> 015+V(1) 00 11 [*]*
<< Success! ==> defined new CTR 12 (PPA)
 4931               725030                 -880  01 11 (10)C> 01471 00 11 10
== Executing  PA-CTR  6, V(1)=0, V(2)=466, repcount=117, factor=5/4
 6218              1139678                   56  01 11586 (10)C> 013 00 11 10
 6219              1139683                   53  01 11586 <B(11) 00 012 00 11 10
 6220              1142027                -1119  01 <B(11) 01586 00 012 00 11 10
 6221              1142034                -1116  11 (11)E> 01586 00 012 00 11 10
 6222              1143206                   56  11587 (11)E> 00 012 00 11 10
 6223              1143208                   58  11588 (11)A> 012 00 11 10
 6224              1143210                   60  11589 (10)D> 01 00 11 10
 6225              1143221                   57  11589 <E(10) 10 00 11 10
 6226              1145577                -1121  <E(10) 10590 00 11 10
 6227              1145580                -1118  01 (11)F> 10590 00 11 10
 6228              1146760                   62  01 11590 (11)F> 00 11 10
 6229              1146762                   64  01 11591 (11)B> 11 10
 6230              1146769                   61  01 11591 <E(10) 102
 6231              1149133                -1121  01 <E(10) 10593
 6232              1149135                -1123  <A(01) 10594
 6233              1149146                -1120  11 (11)A> 10594
 6234              1149148                -1118  112 (01)D> 10593
 6235              1149151                -1121  112 <E(10) 00 10592
 6236              1149159                -1125  <E(10) 102 00 10592
 6237              1149162                -1122  01 (11)F> 102 00 10592
 6238              1149166                -1118  01 112 (11)F> 00 10592
 6239              1149168                -1116  01 113 (11)B> 10592
 6240              1149172                -1114  01 114 (11)E> 10591
 6241              1149177                -1117  01 114 <B(11) 00 10590
 6242              1149193                -1125  01 <B(11) 014 00 10590
 6243              1149200                -1122  11 (11)E> 014 00 10590
 6244              1149208                -1114  115 (11)E> 00 10590
 6245              1149210                -1112  116 (11)A> 10590
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  111+V(1) (11)A> 105+V(2)
    1                    2                    2  112+V(1) (01)D> 104+V(2)
    2                    5                   -1  112+V(1) <E(10) 00 103+V(2)
    3            13+4*V(1)           -5+-2*V(1)  <E(10) 102+V(1) 00 103+V(2)
    4            16+4*V(1)           -2+-2*V(1)  01 (11)F> 102+V(1) 00 103+V(2)
    5            20+6*V(1)                    2  01 112+V(1) (11)F> 00 103+V(2)
    6            22+6*V(1)                    4  01 113+V(1) (11)B> 103+V(2)
    7            26+6*V(1)                    6  01 114+V(1) (11)E> 102+V(2)
    8            31+6*V(1)                    3  01 114+V(1) <B(11) 00 101+V(2)
    9           47+10*V(1)           -5+-2*V(1)  01 <B(11) 014+V(1) 00 101+V(2)
   10           54+10*V(1)           -2+-2*V(1)  11 (11)E> 014+V(1) 00 101+V(2)
   11           62+12*V(1)                    6  115+V(1) (11)E> 00 101+V(2)
   12           64+12*V(1)                    8  116+V(1) (11)A> 101+V(2)
<< Success! ==> defined new CTR 13 (PA)
 6245              1149210                -1112  116 (11)A> 10590
== Executing  PA-CTR 13, V(1)=5, V(2)=585, repcount=147, factor=5/4
 8009              1811298                   64  11741 (11)A> 102
 8010              1811300                   66  11742 (01)D> 10
 8011              1811303                   63  11742 <E(10)
 8012              1814271                -1421  <E(10) 10742
 8013              1814274                -1418  01 (11)F> 10742
 8014              1815758                   66  01 11742 (11)F>
 8015              1815760                   68  01 11743 (11)B>
 8016              1815771                   65  01 11743 <E(10) 01
 8017              1818743                -1421  01 <E(10) 10743 01
 8018              1818745                -1423  <A(01) 10744 01
 8019              1818756                -1420  11 (11)A> 10744 01
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  112+V(1) (11)A> 102
    1                    2                    2  113+V(1) (01)D> 10
    2                    5                   -1  113+V(1) <E(10)
    3            17+4*V(1)           -7+-2*V(1)  <E(10) 103+V(1)
    4            20+4*V(1)           -4+-2*V(1)  01 (11)F> 103+V(1)
    5            26+6*V(1)                    2  01 113+V(1) (11)F>
    6            28+6*V(1)                    4  01 114+V(1) (11)B>
    7            39+6*V(1)                    1  01 114+V(1) <E(10) 01
    8           55+10*V(1)           -7+-2*V(1)  01 <E(10) 104+V(1) 01
    9           57+10*V(1)           -9+-2*V(1)  <A(01) 105+V(1) 01
   10           68+10*V(1)           -6+-2*V(1)  11 (11)A> 105+V(1) 01
<< Success! ==> defined new CTR 14 (PPA)
 8019              1818756                -1420  11 (11)A> 10744 01
== Executing  PA-CTR  1, V(1)=0, V(2)=739, repcount=185, factor=5/4
10239              2851796                   60  11926 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=925
10263              2872350                -1796  11 (11)A> 10936 01
== Executing  PA-CTR  1, V(1)=0, V(2)=931, repcount=233, factor=5/4
13059              4508942                   68  111166 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=1165
13083              4534776                -2268  11 (11)A> 101176 01
== Executing  PA-CTR  1, V(1)=0, V(2)=1171, repcount=293, factor=5/4
16599              7120208                   76  111466 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=1465
16623              7152642                -2860  11 (11)A> 101476 01
== Executing  PA-CTR  1, V(1)=0, V(2)=1471, repcount=368, factor=5/4
21039             11227874                   84  111841 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=1840
21063             11268558                -3602  11 (11)A> 101851 01
== Executing  PA-CTR  1, V(1)=0, V(2)=1846, repcount=462, factor=5/4
26607             17687586                   94  112311 (11)A> 103 01
== Executing PPA-CTR  4 (once), V(1)=2310, V(2)=0
26630             17724690                -4530  01 11 (10)C> 012318 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=2313, repcount=579, factor=5/4
32999             27801606                  102  01 112896 (10)C> 012 00 10
== Executing PPA-CTR  3 (once), V(1)=2895, V(2)=0
33017             27848068                -5694  11 (11)A> 102904 01
== Executing  PA-CTR  1, V(1)=0, V(2)=2899, repcount=725, factor=5/4
41717             43641468                  106  113626 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=3625
41741             43721422                -7150  11 (11)A> 103636 01
== Executing  PA-CTR  1, V(1)=0, V(2)=3631, repcount=908, factor=5/4
52637             68486214                  114  114541 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=4540
52661             68586298                -8972  11 (11)A> 104551 01
== Executing  PA-CTR  1, V(1)=0, V(2)=4546, repcount=1137, factor=5/4
66305            107408026                  124  115686 (11)A> 103 01
== Executing PPA-CTR  4 (once), V(1)=5685, V(2)=0
66328            107499130               -11250  01 11 (10)C> 015693 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=5688, repcount=1423, factor=5/4
81981            168295382                  134  01 117116 (10)C> 01 00 10
81982            168295387                  131  01 117116 <B(11) 002 10
81983            168323851               -14101  01 <B(11) 017116 002 10
81984            168323858               -14098  11 (11)E> 017116 002 10
81985            168338090                  134  117117 (11)E> 002 10
81986            168338092                  136  117118 (11)A> 00 10
81987            168338096                  138  117119 (01)D> 10
81988            168338099                  135  117119 <E(10)
81989            168366575               -14103  <E(10) 107119
81990            168366578               -14100  01 (11)F> 107119
81991            168380816                  138  01 117119 (11)F>
81992            168380818                  140  01 117120 (11)B>
81993            168380829                  137  01 117120 <E(10) 01
81994            168409309               -14103  01 <E(10) 107120 01
81995            168409311               -14105  <A(01) 107121 01
81996            168409322               -14102  11 (11)A> 107121 01
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 111+V(1) (10)C> 01 00 10
    1                    5                   -3  01 111+V(1) <B(11) 002 10
    2             9+4*V(1)           -5+-2*V(1)  01 <B(11) 011+V(1) 002 10
    3            16+4*V(1)           -2+-2*V(1)  11 (11)E> 011+V(1) 002 10
    4            18+6*V(1)                    0  112+V(1) (11)E> 002 10
    5            20+6*V(1)                    2  113+V(1) (11)A> 00 10
    6            24+6*V(1)                    4  114+V(1) (01)D> 10
    7            27+6*V(1)                    1  114+V(1) <E(10)
    8           43+10*V(1)           -7+-2*V(1)  <E(10) 104+V(1)
    9           46+10*V(1)           -4+-2*V(1)  01 (11)F> 104+V(1)
   10           54+12*V(1)                    4  01 114+V(1) (11)F>
   11           56+12*V(1)                    6  01 115+V(1) (11)B>
   12           67+12*V(1)                    3  01 115+V(1) <E(10) 01
   13           87+16*V(1)           -7+-2*V(1)  01 <E(10) 105+V(1) 01
   14           89+16*V(1)           -9+-2*V(1)  <A(01) 106+V(1) 01
   15          100+16*V(1)           -6+-2*V(1)  11 (11)A> 106+V(1) 01
<< Success! ==> defined new CTR 15 (PPA)
81996            168409322               -14102  11 (11)A> 107121 01
== Executing  PA-CTR  1, V(1)=0, V(2)=7116, repcount=1780, factor=5/4
103356            263521842                  138  118901 (11)A> 10 01
103357            263521844                  140  118902 (01)D> 01
103358            263521847                  137  118902 <A(01) 11
103359            263521853                  135  118901 <B(11) 00 11
103360            263557457               -17667  <B(11) 018901 00 11
103361            263557465               -17669  <E(10) 018902 00 11
103362            263557468               -17666  01 (11)F> 018902 00 11
103363            263557470               -17664  01 11 (10)C> 018901 00 11
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  115+V(1) (11)A> 10 01
    1                    2                    2  116+V(1) (01)D> 01
    2                    5                   -1  116+V(1) <A(01) 11
    3                   11                   -3  115+V(1) <B(11) 00 11
    4            31+4*V(1)          -13+-2*V(1)  <B(11) 015+V(1) 00 11
    5            39+4*V(1)          -15+-2*V(1)  <E(10) 016+V(1) 00 11
    6            42+4*V(1)          -12+-2*V(1)  01 (11)F> 016+V(1) 00 11
    7            44+4*V(1)          -10+-2*V(1)  01 11 (10)C> 015+V(1) 00 11
<< Success! ==> defined new CTR 16 (PPA)
103363            263557470               -17664  01 11 (10)C> 018901 00 11
== Executing  PA-CTR  2, V(1)=0, V(2)=8896, repcount=2225, factor=5/4
127838            412151870                  136  01 1111126 (10)C> 01 00 11
127839            412151875                  133  01 1111126 <B(11) 002 11
127840            412196379               -22119  01 <B(11) 0111126 002 11
127841            412196386               -22116  11 (11)E> 0111126 002 11
127842            412218638                  136  1111127 (11)E> 002 11
127843            412218640                  138  1111128 (11)A> 00 11
127844            412218644                  140  1111129 (01)D> 11
127845            412218647                  137  1111129 <E(10) 01
127846            412263163               -22121  <E(10) 1011129 01
127847            412263166               -22118  01 (11)F> 1011129 01
127848            412285424                  140  01 1111129 (11)F> 01
127849            412285426                  142  01 1111130 (10)C>
127850            412285435                  139  01 1111130 <E(10) 01
127851            412329955               -22121  01 <E(10) 1011130 01
127852            412329957               -22123  <A(01) 1011131 01
127853            412329968               -22120  11 (11)A> 1011131 01
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 111+V(1) (10)C> 01 00 11
    1                    5                   -3  01 111+V(1) <B(11) 002 11
    2             9+4*V(1)           -5+-2*V(1)  01 <B(11) 011+V(1) 002 11
    3            16+4*V(1)           -2+-2*V(1)  11 (11)E> 011+V(1) 002 11
    4            18+6*V(1)                    0  112+V(1) (11)E> 002 11
    5            20+6*V(1)                    2  113+V(1) (11)A> 00 11
    6            24+6*V(1)                    4  114+V(1) (01)D> 11
    7            27+6*V(1)                    1  114+V(1) <E(10) 01
    8           43+10*V(1)           -7+-2*V(1)  <E(10) 104+V(1) 01
    9           46+10*V(1)           -4+-2*V(1)  01 (11)F> 104+V(1) 01
   10           54+12*V(1)                    4  01 114+V(1) (11)F> 01
   11           56+12*V(1)                    6  01 115+V(1) (10)C>
   12           65+12*V(1)                    3  01 115+V(1) <E(10) 01
   13           85+16*V(1)           -7+-2*V(1)  01 <E(10) 105+V(1) 01
   14           87+16*V(1)           -9+-2*V(1)  <A(01) 106+V(1) 01
   15           98+16*V(1)           -6+-2*V(1)  11 (11)A> 106+V(1) 01
<< Success! ==> defined new CTR 17 (PPA)
127853            412329968               -22120  11 (11)A> 1011131 01
== Executing  PA-CTR  1, V(1)=0, V(2)=11126, repcount=2782, factor=5/4
161237            644610276                  136  1113911 (11)A> 103 01
== Executing PPA-CTR  4 (once), V(1)=13910, V(2)=0
161260            644832980               -27688  01 11 (10)C> 0113918 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=13913, repcount=3479, factor=5/4
199529           1008054496                  144  01 1117396 (10)C> 012 00 10
== Executing PPA-CTR  3 (once), V(1)=17395, V(2)=0
199547           1008332958               -34652  11 (11)A> 1017404 01
== Executing  PA-CTR  1, V(1)=0, V(2)=17399, repcount=4350, factor=5/4
251747           1576155858                  148  1121751 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=21750
251771           1576634562               -43358  11 (11)A> 1021761 01
== Executing  PA-CTR  1, V(1)=0, V(2)=21756, repcount=5440, factor=5/4
317051           2464627522                  162  1127201 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=27196
317058           2464736350               -54240  01 11 (10)C> 0127201 00 11
== Executing  PA-CTR  2, V(1)=0, V(2)=27196, repcount=6800, factor=5/4
391858           3852167550                  160  01 1134001 (10)C> 01 00 11
== Executing PPA-CTR 17 (once), V(1)=34000
391873           3852711648               -67846  11 (11)A> 1034006 01
== Executing  PA-CTR  1, V(1)=0, V(2)=34001, repcount=8501, factor=5/4
493885           6021010712                  162  1142506 (11)A> 102 01
== Executing PPA-CTR  9 (once), V(1)=42505
493903           6021690894               -84852  01 11 (10)C> 0142510 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=42505, repcount=10627, factor=5/4
610800           9410046082                  164  01 1153136 (10)C> 012 00 10
== Executing PPA-CTR  3 (once), V(1)=53135, V(2)=0
610818           9410896384              -106112  11 (11)A> 1053144 01
== Executing  PA-CTR  1, V(1)=0, V(2)=53139, repcount=13285, factor=5/4
770238          14706084824                  168  1166426 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=66425
770262          14707546378              -132688  11 (11)A> 1066436 01
== Executing  PA-CTR  1, V(1)=0, V(2)=66431, repcount=16608, factor=5/4
969558          22982880970                  176  1183041 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=83040
969582          22984708054              -165910  11 (11)A> 1083051 01
== Executing  PA-CTR  1, V(1)=0, V(2)=83046, repcount=20762, factor=5/4
1218726          35917233282                  186  11103811 (11)A> 103 01
== Executing PPA-CTR  4 (once), V(1)=103810, V(2)=0
1218749          35918894386              -207438  01 11 (10)C> 01103818 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=103813, repcount=25954, factor=5/4
1504243          56128080302                  194  01 11129771 (10)C> 012 00 10
== Executing PPA-CTR  3 (once), V(1)=129770, V(2)=0
1504261          56130156764              -259352  11 (11)A> 10129779 01
== Executing  PA-CTR  1, V(1)=0, V(2)=129774, repcount=32444, factor=5/4
1893589          87709653940                  200  11162221 (11)A> 103 01
== Executing PPA-CTR  4 (once), V(1)=162220, V(2)=0
1893612          87712249604              -324244  01 11 (10)C> 01162228 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=162223, repcount=40556, factor=5/4
2339728         137057302588                  204  01 11202781 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=202780
2339743         137060547178              -405362  11 (11)A> 10202787 01 10
== Executing  PA-CTR  5, V(1)=0, V(2)=202782, repcount=50696, factor=5/4
2948095         214164803322                  206  11253481 (11)A> 103 01 10
2948096         214164803324                  208  11253482 (01)D> 102 01 10
2948097         214164803327                  205  11253482 <E(10) 00 10 01 10
2948098         214165817255              -506759  <E(10) 10253482 00 10 01 10
2948099         214165817258              -506756  01 (11)F> 10253482 00 10 01 10
2948100         214166324222                  208  01 11253482 (11)F> 00 10 01 10
2948101         214166324224                  210  01 11253483 (11)B> 10 01 10
2948102         214166324228                  212  01 11253484 (11)E> 01 10
2948103         214166324230                  214  01 11253485 (11)E> 10
2948104         214166324235                  211  01 11253485 <B(11)
2948105         214167338175              -506759  01 <B(11) 01253485
2948106         214167338182              -506756  11 (11)E> 01253485
2948107         214167845152                  214  11253486 (11)E>
2948108         214167845154                  216  11253487 (11)A>
2948109         214167845158                  218  11253488 (01)D>
2948110         214167845161                  215  11253488 <A(01) 10
2948111         214167845167                  213  11253487 <B(11) 00 10
2948112         214168859115              -506761  <B(11) 01253487 00 10
2948113         214168859123              -506763  <E(10) 01253488 00 10
2948114         214168859126              -506760  01 (11)F> 01253488 00 10
2948115         214168859128              -506758  01 11 (10)C> 01253487 00 10
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  111+V(1) (11)A> 103 011+V(2) 10
    1                    2                    2  112+V(1) (01)D> 102 011+V(2) 10
    2                    5                   -1  112+V(1) <E(10) 00 10 011+V(2) 10
    3            13+4*V(1)           -5+-2*V(1)  <E(10) 102+V(1) 00 10 011+V(2) 10
    4            16+4*V(1)           -2+-2*V(1)  01 (11)F> 102+V(1) 00 10 011+V(2) 10
    5            20+6*V(1)                    2  01 112+V(1) (11)F> 00 10 011+V(2) 10
    6            22+6*V(1)                    4  01 113+V(1) (11)B> 10 011+V(2) 10
    7            26+6*V(1)                    6  01 114+V(1) (11)E> 011+V(2) 10
    8     28+6*V(1)+2*V(2)             8+2*V(2)  01 115+V(1)+V(2) (11)E> 10
    9     33+6*V(1)+2*V(2)             5+2*V(2)  01 115+V(1)+V(2) <B(11)
   10    53+10*V(1)+6*V(2)           -5+-2*V(1)  01 <B(11) 015+V(1)+V(2)
   11    60+10*V(1)+6*V(2)           -2+-2*V(1)  11 (11)E> 015+V(1)+V(2)
   12    70+12*V(1)+8*V(2)             8+2*V(2)  116+V(1)+V(2) (11)E>
   13    72+12*V(1)+8*V(2)            10+2*V(2)  117+V(1)+V(2) (11)A>
   14    76+12*V(1)+8*V(2)            12+2*V(2)  118+V(1)+V(2) (01)D>
   15    79+12*V(1)+8*V(2)             9+2*V(2)  118+V(1)+V(2) <A(01) 10
   16    85+12*V(1)+8*V(2)             7+2*V(2)  117+V(1)+V(2) <B(11) 00 10
   17  113+16*V(1)+12*V(2)           -7+-2*V(1)  <B(11) 017+V(1)+V(2) 00 10
   18  121+16*V(1)+12*V(2)           -9+-2*V(1)  <E(10) 018+V(1)+V(2) 00 10
   19  124+16*V(1)+12*V(2)           -6+-2*V(1)  01 (11)F> 018+V(1)+V(2) 00 10
   20  126+16*V(1)+12*V(2)           -4+-2*V(1)  01 11 (10)C> 017+V(1)+V(2) 00 10
<< Success! ==> defined new CTR 18 (PPA)
2948115         214168859128              -506758  01 11 (10)C> 01253487 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=253482, repcount=63371, factor=5/4
3645196         334647522972                  210  01 11316856 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=316855
3645223         334654493986              -633506  01 11 (10)C> 01316865 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=316860, repcount=79216, factor=5/4
4516599         522912427010                  222  01 11396081 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=396080
4516614         522918764390              -791944  11 (11)A> 10396086 01
== Executing  PA-CTR  1, V(1)=0, V(2)=396081, repcount=99021, factor=5/4
5704866         817076884334                  224  11495106 (11)A> 102 01
== Executing PPA-CTR  9 (once), V(1)=495105
5704884         817084806116              -989990  01 11 (10)C> 01495110 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=495105, repcount=123777, factor=5/4
7066431        1276711386404                  226  01 11618886 (10)C> 012 00 10
== Executing PPA-CTR  3 (once), V(1)=618885, V(2)=0
7066449        1276721288706             -1237550  11 (11)A> 10618894 01
== Executing  PA-CTR  1, V(1)=0, V(2)=618889, repcount=154723, factor=5/4
8923125        1994902751158                  234  11773616 (11)A> 102 01
== Executing PPA-CTR  9 (once), V(1)=773615
8923143        1994915129100             -1547000  01 11 (10)C> 01773620 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=773615, repcount=193404, factor=5/4
11050587        3117074921316                  232  01 11967021 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=967020
11050602        3117090393746             -1933814  11 (11)A> 10967027 01 10
== Executing  PA-CTR  5, V(1)=0, V(2)=967022, repcount=241756, factor=5/4
13951674        4870477519530                  234  111208781 (11)A> 103 01 10
== Executing PPA-CTR 18 (once), V(1)=1208780, V(2)=0
13951694        4870496860136             -2417330  01 11 (10)C> 011208787 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=1208782, repcount=302196, factor=5/4
17275850        7610179807280                  238  01 111510981 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=1510980
17275877        7610213049044             -3021728  01 11 (10)C> 011510990 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=1510985, repcount=377747, factor=5/4
21431094       11891009772712                  248  01 111888736 (10)C> 012 00 10
== Executing PPA-CTR  3 (once), V(1)=1888735, V(2)=0
21431112       11891039992614             -3777228  11 (11)A> 101888744 01
== Executing  PA-CTR  1, V(1)=0, V(2)=1888739, repcount=472185, factor=5/4
27097332       18579816273654                  252  112360926 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=2360925
27097356       18579868214208             -4721604  11 (11)A> 102360936 01
== Executing  PA-CTR  1, V(1)=0, V(2)=2360931, repcount=590233, factor=5/4
34180152       29031138110800                  260  112951166 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=2951165
34180176       29031203036634             -5902076  11 (11)A> 102951176 01
== Executing  PA-CTR  1, V(1)=0, V(2)=2951171, repcount=737793, factor=5/4
43033692       45361383447066                  268  113688966 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=3688965
43033716       45361464604500             -7377668  11 (11)A> 103688976 01
== Executing  PA-CTR  1, V(1)=0, V(2)=3688971, repcount=922243, factor=5/4
54100632       70877460492232                  276  114611216 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=4611215
54100656       70877561939166             -9222160  11 (11)A> 104611226 01
== Executing  PA-CTR  1, V(1)=0, V(2)=4611221, repcount=1152806, factor=5/4
67934328      110746451343650                  288  115764031 (11)A> 102 01
== Executing PPA-CTR  9 (once), V(1)=5764030
67934346      110746543568232            -11527776  01 11 (10)C> 015764035 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=5764030, repcount=1441008, factor=5/4
83785434      173041714244424                  288  01 117205041 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=7205040
83785461      173041872755508            -14409798  01 11 (10)C> 017205050 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=7205045, repcount=1801262, factor=5/4
103599343      270378277777736                  298  01 119006311 (10)C> 012 00 10
== Executing PPA-CTR  3 (once), V(1)=9006310, V(2)=0
103599361      270378421878838            -18012328  11 (11)A> 109006319 01
== Executing  PA-CTR  1, V(1)=0, V(2)=9006314, repcount=2251579, factor=5/4
130618309      422466738229754                  304  1111257896 (11)A> 103 01
== Executing PPA-CTR  4 (once), V(1)=11257895, V(2)=0
130618332      422466918356218            -22515490  01 11 (10)C> 0111257903 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=11257898, repcount=2814475, factor=5/4
161577557      660105099817118                  310  01 1114072376 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=14072375
161577584      660105409409572            -28144446  01 11 (10)C> 0114072385 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=14072380, repcount=3518096, factor=5/4
200276640     1031415512981316                  322  01 1117590481 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=17590480
200276655     1031415794429096            -35180644  11 (11)A> 1017590486 01
== Executing  PA-CTR  1, V(1)=0, V(2)=17590481, repcount=4397621, factor=5/4
253048107     1611588057737440                  324  1121988106 (11)A> 102 01
== Executing PPA-CTR  9 (once), V(1)=21988105
253048125     1611588409547222            -43975890  01 11 (10)C> 0121988110 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=21988105, repcount=5497027, factor=5/4
313515422     2518107771608010                  326  01 1127485136 (10)C> 012 00 10
== Executing PPA-CTR  3 (once), V(1)=27485135, V(2)=0
313515440     2518108211370312            -54969950  11 (11)A> 1027485144 01
== Executing  PA-CTR  1, V(1)=0, V(2)=27485139, repcount=6871285, factor=5/4
395970860     3934545171530752                  330  1134356426 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=34356425
395970884     3934545927372306            -68712526  11 (11)A> 1034356436 01
== Executing  PA-CTR  1, V(1)=0, V(2)=34356431, repcount=8589108, factor=5/4
499040180     6147729506471898                  338  1142945541 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=42945540
499040204     6147730451273982            -85890748  11 (11)A> 1042945551 01
== Executing  PA-CTR  1, V(1)=0, V(2)=42945546, repcount=10736387, factor=5/4
627876848     9605830990724210                  348  1153681936 (11)A> 103 01
== Executing PPA-CTR  4 (once), V(1)=53681935, V(2)=0
627876871     9605831849635314           -107363526  01 11 (10)C> 0153681943 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=53681938, repcount=13420485, factor=5/4
775502206    15009114834988554                  354  01 1167102426 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=67102425
775502233    15009116311242108           -134204502  01 11 (10)C> 0167102435 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=67102430, repcount=16775608, factor=5/4
960033921    23451747594702700                  362  01 1183878041 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=83878040
960033948    23451749440019784           -167755724  01 11 (10)C> 0183878050 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=83878045, repcount=20969512, factor=5/4
1190698580    36643363158527512                  372  01 11104847561 (10)C> 012 00 10
== Executing PPA-CTR  3 (once), V(1)=104847560, V(2)=0
1190698598    36643364836088614           -209694754  11 (11)A> 10104847569 01
== Executing  PA-CTR  1, V(1)=0, V(2)=104847564, repcount=26211892, factor=5/4
1505241302    57255264193882862                  382  11131059461 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=131059456
1505241309    57255264718120730           -262118540  01 11 (10)C> 01131059461 00 11
== Executing  PA-CTR  2, V(1)=0, V(2)=131059456, repcount=32764865, factor=5/4
1865654824    89461357186172890                  380  01 11163824326 (10)C> 01 00 11
== Executing PPA-CTR 17 (once), V(1)=163824325
1865654839    89461359807362188           -327648276  11 (11)A> 10163824331 01
== Executing  PA-CTR  1, V(1)=0, V(2)=163824326, repcount=40956082, factor=5/4
2357127823    1397833[4]3590696                  380  11204780411 (11)A> 103 01
== Executing PPA-CTR  4 (once), V(1)=204780410, V(2)=0
2357127846    1397833[4]0077400           -409560444  01 11 (10)C> 01204780418 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=204780413, repcount=51195104, factor=5/4
2920273990    2184115[4]7835416                  388  01 11255975521 (10)C> 012 00 10
== Executing PPA-CTR  3 (once), V(1)=255975520, V(2)=0
2920274008    2184115[4]3443878           -511950658  11 (11)A> 10255975529 01
== Executing  PA-CTR  1, V(1)=0, V(2)=255975524, repcount=63993882, factor=5/4
3688200592    3412680[4]2133586                  398  11319969411 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=319969406
3688200599    3412680[4]2011254           -639938424  01 11 (10)C> 01319969411 00 11
== Executing  PA-CTR  2, V(1)=0, V(2)=319969406, repcount=79992352, factor=5/4
4568116471    5332313[4]6508342                  392  01 11399961761 (10)C> 013 00 11
4568116472    5332313[4]6508347                  389  01 11399961761 <B(11) 00 012 00 11
4568116473    5332313[4]6355391           -799923133  01 <B(11) 01399961761 00 012 00 11
4568116474    5332313[4]6355398           -799923130  11 (11)E> 01399961761 00 012 00 11
4568116475    5332313[4]6278920                  392  11399961762 (11)E> 00 012 00 11
4568116476    5332313[4]6278922                  394  11399961763 (11)A> 012 00 11
4568116477    5332313[4]6278924                  396  11399961764 (10)D> 01 00 11
4568116478    5332313[4]6278935                  393  11399961764 <E(10) 10 00 11
4568116479    5332313[4]6125991           -799923135  <E(10) 10399961765 00 11
4568116480    5332313[4]6125994           -799923132  01 (11)F> 10399961765 00 11
4568116481    5332313[4]6049524                  398  01 11399961765 (11)F> 00 11
4568116482    5332313[4]6049526                  400  01 11399961766 (11)B> 11
4568116483    5332313[4]6049533                  397  01 11399961766 <E(10) 10
4568116484    5332313[4]5896597           -799923135  01 <E(10) 10399961767
4568116485    5332313[4]5896599           -799923137  <A(01) 10399961768
4568116486    5332313[4]5896610           -799923134  11 (11)A> 10399961768
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 111+V(1) (10)C> 013 00 11
    1                    5                   -3  01 111+V(1) <B(11) 00 012 00 11
    2             9+4*V(1)           -5+-2*V(1)  01 <B(11) 011+V(1) 00 012 00 11
    3            16+4*V(1)           -2+-2*V(1)  11 (11)E> 011+V(1) 00 012 00 11
    4            18+6*V(1)                    0  112+V(1) (11)E> 00 012 00 11
    5            20+6*V(1)                    2  113+V(1) (11)A> 012 00 11
    6            22+6*V(1)                    4  114+V(1) (10)D> 01 00 11
    7            33+6*V(1)                    1  114+V(1) <E(10) 10 00 11
    8           49+10*V(1)           -7+-2*V(1)  <E(10) 105+V(1) 00 11
    9           52+10*V(1)           -4+-2*V(1)  01 (11)F> 105+V(1) 00 11
   10           62+12*V(1)                    6  01 115+V(1) (11)F> 00 11
   11           64+12*V(1)                    8  01 116+V(1) (11)B> 11
   12           71+12*V(1)                    5  01 116+V(1) <E(10) 10
   13           95+16*V(1)           -7+-2*V(1)  01 <E(10) 107+V(1)
   14           97+16*V(1)           -9+-2*V(1)  <A(01) 108+V(1)
   15          108+16*V(1)           -6+-2*V(1)  11 (11)A> 108+V(1)
<< Success! ==> defined new CTR 19 (PPA)
4568116486    5332313[4]5896610           -799923134  11 (11)A> 10399961768
== Executing  PA-CTR 13, V(1)=0, V(2)=399961763, repcount=99990441, factor=5/4
5768001778    8331740[4]6806034                  394  11499952206 (11)A> 104
5768001779    8331740[4]6806036                  396  11499952207 (01)D> 103
5768001780    8331740[4]6806039                  393  11499952207 <E(10) 00 102
5768001781    8331740[4]6614867           -999904021  <E(10) 10499952207 00 102
5768001782    8331740[4]6614870           -999904018  01 (11)F> 10499952207 00 102
5768001783    8331740[4]6519284                  396  01 11499952207 (11)F> 00 102
5768001784    8331740[4]6519286                  398  01 11499952208 (11)B> 102
5768001785    8331740[4]6519290                  400  01 11499952209 (11)E> 10
5768001786    8331740[4]6519295                  397  01 11499952209 <B(11)
5768001787    8331740[4]6328131           -999904021  01 <B(11) 01499952209
5768001788    8331740[4]6328138           -999904018  11 (11)E> 01499952209
5768001789    8331740[4]6232556                  400  11499952210 (11)E>
5768001790    8331740[4]6232558                  402  11499952211 (11)A>
5768001791    8331740[4]6232562                  404  11499952212 (01)D>
5768001792    8331740[4]6232565                  401  11499952212 <A(01) 10
5768001793    8331740[4]6232571                  399  11499952211 <B(11) 00 10
5768001794    8331740[4]6041415           -999904023  <B(11) 01499952211 00 10
5768001795    8331740[4]6041423           -999904025  <E(10) 01499952212 00 10
5768001796    8331740[4]6041426           -999904022  01 (11)F> 01499952212 00 10
5768001797    8331740[4]6041428           -999904020  01 11 (10)C> 01499952211 00 10
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  111+V(1) (11)A> 104
    1                    2                    2  112+V(1) (01)D> 103
    2                    5                   -1  112+V(1) <E(10) 00 102
    3            13+4*V(1)           -5+-2*V(1)  <E(10) 102+V(1) 00 102
    4            16+4*V(1)           -2+-2*V(1)  01 (11)F> 102+V(1) 00 102
    5            20+6*V(1)                    2  01 112+V(1) (11)F> 00 102
    6            22+6*V(1)                    4  01 113+V(1) (11)B> 102
    7            26+6*V(1)                    6  01 114+V(1) (11)E> 10
    8            31+6*V(1)                    3  01 114+V(1) <B(11)
    9           47+10*V(1)           -5+-2*V(1)  01 <B(11) 014+V(1)
   10           54+10*V(1)           -2+-2*V(1)  11 (11)E> 014+V(1)
   11           62+12*V(1)                    6  115+V(1) (11)E>
   12           64+12*V(1)                    8  116+V(1) (11)A>
   13           68+12*V(1)                   10  117+V(1) (01)D>
   14           71+12*V(1)                    7  117+V(1) <A(01) 10
   15           77+12*V(1)                    5  116+V(1) <B(11) 00 10
   16          101+16*V(1)           -7+-2*V(1)  <B(11) 016+V(1) 00 10
   17          109+16*V(1)           -9+-2*V(1)  <E(10) 017+V(1) 00 10
   18          112+16*V(1)           -6+-2*V(1)  01 (11)F> 017+V(1) 00 10
   19          114+16*V(1)           -4+-2*V(1)  01 11 (10)C> 016+V(1) 00 10
<< Success! ==> defined new CTR 20 (PPA)
5768001797    8331740[4]6041428           -999904020  01 11 (10)C> 01499952211 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=499952206, repcount=124988052, factor=5/4
7142870369    1301834[5]8276316                  396  01 11624940261 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=624940260
7142870396    1301834[5]6962240          -1249880130  01 11 (10)C> 01624940270 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=624940265, repcount=156235067, factor=5/4
8861456133    2034116[5]3789188                  406  01 11781175336 (10)C> 012 00 10
== Executing PPA-CTR  3 (once), V(1)=781175335, V(2)=0
8861456151    2034116[5]2594690          -1562350270  11 (11)A> 10781175344 01
== Executing  PA-CTR  1, V(1)=0, V(2)=781175339, repcount=195293835, factor=5/4
11204982171    3178306[5]2801830                  410  11976469176 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=976469175
11204982195    3178306[5]5123884          -1952937946  11 (11)A> 10976469186 01
== Executing  PA-CTR  1, V(1)=0, V(2)=976469181, repcount=244117296, factor=5/4
14134389747    4966104[5]5660428                  422  111220586481 (11)A> 102 01
== Executing PPA-CTR  9 (once), V(1)=1220586480
14134389765    4966104[5]5044210          -2441172542  01 11 (10)C> 011220586485 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=1220586480, repcount=305146621, factor=5/4
17491002596    7759538[5]1558554                  426  01 111525733106 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=1525733105
17491002611    7759538[5]3288334          -3051465790  11 (11)A> 101525733111 01
== Executing  PA-CTR  1, V(1)=0, V(2)=1525733106, repcount=381433277, factor=5/4
22068201935    1212427[6]0781622                  426  111907166386 (11)A> 103 01
== Executing PPA-CTR  4 (once), V(1)=1907166385, V(2)=0
22068201958    1212427[6]5443926          -3814332348  01 11 (10)C> 011907166393 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=1907166388, repcount=476791598, factor=5/4
27312909536    1894418[6]8166378                  436  01 112383957991 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=2383957990
27312909551    1894418[6]1494318          -4767915550  11 (11)A> 102383957996 01
== Executing  PA-CTR  1, V(1)=0, V(2)=2383957991, repcount=595989498, factor=5/4
34464783527    2960029[6]3897370                  434  112979947491 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=2979947490
34464783551    2960029[6]2742354          -5959894552  11 (11)A> 102979947501 01
== Executing  PA-CTR  1, V(1)=0, V(2)=2979947496, repcount=744986875, factor=5/4
43404626051    4625045[6]0264854                  448  113724934376 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=3724934371
43404626058    4625045[6]0002382          -7449868304  01 11 (10)C> 013724934376 00 11
== Executing  PA-CTR  2, V(1)=0, V(2)=3724934371, repcount=931233593, factor=5/4
53648195581    7226633[6]2634014                  440  01 114656167966 (10)C> 014 00 11
== Executing PPA-CTR 11 (once), V(1)=4656167965
53648195596    7226633[6]1321564          -9312335496  11 (11)A> 104656167972 01 11
== Executing  PA-CTR  5, V(1)=0, V(2)=4656167967, repcount=1164041992, factor=5/4
67616699500    1129161[7]8591212                  440  115820209961 (11)A> 104 01 11
67616699501    1129161[7]8591214                  442  115820209962 (01)D> 103 01 11
67616699502    1129161[7]8591217                  439  115820209962 <E(10) 00 102 01 11
67616699503    1129161[7]9431065         -11640419485  <E(10) 105820209962 00 102 01 11
67616699504    1129161[7]9431068         -11640419482  01 (11)F> 105820209962 00 102 01 11
67616699505    1129161[7]9850992                  442  01 115820209962 (11)F> 00 102 01 11
67616699506    1129161[7]9850994                  444  01 115820209963 (11)B> 102 01 11
67616699507    1129161[7]9850998                  446  01 115820209964 (11)E> 10 01 11
67616699508    1129161[7]9851003                  443  01 115820209964 <B(11) 00 01 11
67616699509    1129161[7]0690859         -11640419485  01 <B(11) 015820209964 00 01 11
67616699510    1129161[7]0690866         -11640419482  11 (11)E> 015820209964 00 01 11
67616699511    1129161[7]1110794                  446  115820209965 (11)E> 00 01 11
67616699512    1129161[7]1110796                  448  115820209966 (11)A> 01 11
67616699513    1129161[7]1110798                  450  115820209967 (10)D> 11
67616699514    1129161[7]1110801                  447  115820209967 <B(11) 01
67616699515    1129161[7]1950669         -11640419487  <B(11) 015820209968
67616699516    1129161[7]1950677         -11640419489  <E(10) 015820209969
67616699517    1129161[7]1950680         -11640419486  01 (11)F> 015820209969
67616699518    1129161[7]1950682         -11640419484  01 11 (10)C> 015820209968
67616699519    1129161[7]1950687         -11640419487  01 11 <B(11) 00 015820209967
67616699520    1129161[7]1950691         -11640419489  01 <B(11) 01 00 015820209967
67616699521    1129161[7]1950698         -11640419486  11 (11)E> 01 00 015820209967
67616699522    1129161[7]1950700         -11640419484  112 (11)E> 00 015820209967
67616699523    1129161[7]1950702         -11640419482  113 (11)A> 015820209967
67616699524    1129161[7]1950704         -11640419480  114 (10)D> 015820209966
67616699525    1129161[7]1950715         -11640419483  114 <E(10) 10 015820209965
67616699526    1129161[7]1950731         -11640419491  <E(10) 105 015820209965
67616699527    1129161[7]1950734         -11640419488  01 (11)F> 105 015820209965
67616699528    1129161[7]1950744         -11640419478  01 115 (11)F> 015820209965
67616699529    1129161[7]1950746         -11640419476  01 116 (10)C> 015820209964
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  01 111+V(1) (10)C> 015+V(2)
    1                    5                   -3  01 111+V(1) <B(11) 00 014+V(2)
    2             9+4*V(1)           -5+-2*V(1)  01 <B(11) 011+V(1) 00 014+V(2)
    3            16+4*V(1)           -2+-2*V(1)  11 (11)E> 011+V(1) 00 014+V(2)
    4            18+6*V(1)                    0  112+V(1) (11)E> 00 014+V(2)
    5            20+6*V(1)                    2  113+V(1) (11)A> 014+V(2)
    6            22+6*V(1)                    4  114+V(1) (10)D> 013+V(2)
    7            33+6*V(1)                    1  114+V(1) <E(10) 10 012+V(2)
    8           49+10*V(1)           -7+-2*V(1)  <E(10) 105+V(1) 012+V(2)
    9           52+10*V(1)           -4+-2*V(1)  01 (11)F> 105+V(1) 012+V(2)
   10           62+12*V(1)                    6  01 115+V(1) (11)F> 012+V(2)
   11           64+12*V(1)                    8  01 116+V(1) (10)C> 011+V(2)
<< Success! ==> defined new CTR 21 (PA)
67616699529    1129161[7]1950746         -11640419476  01 116 (10)C> 015820209964
== Executing  PA-CTR 21, V(1)=5, V(2)=5820209959, repcount=1455052490, factor=5/4
83622276919    1764314[7]2887806                  444  01 117275262456 (10)C> 014
83622276920    1764314[7]2887811                  441  01 117275262456 <B(11) 00 013
83622276921    1764314[7]3937635         -14550524471  01 <B(11) 017275262456 00 013
83622276922    1764314[7]3937642         -14550524468  11 (11)E> 017275262456 00 013
83622276923    1764314[7]4462554                  444  117275262457 (11)E> 00 013
83622276924    1764314[7]4462556                  446  117275262458 (11)A> 013
83622276925    1764314[7]4462558                  448  117275262459 (10)D> 012
83622276926    1764314[7]4462569                  445  117275262459 <E(10) 10 01
83622276927    1764314[7]5512405         -14550524473  <E(10) 107275262460 01
83622276928    1764314[7]5512408         -14550524470  01 (11)F> 107275262460 01
83622276929    1764314[7]6037328                  450  01 117275262460 (11)F> 01
83622276930    1764314[7]6037330                  452  01 117275262461 (10)C>
83622276931    1764314[7]6037339                  449  01 117275262461 <E(10) 01
83622276932    1764314[7]7087183         -14550524473  01 <E(10) 107275262461 01
83622276933    1764314[7]7087185         -14550524475  <A(01) 107275262462 01
83622276934    1764314[7]7087196         -14550524472  11 (11)A> 107275262462 01
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 111+V(1) (10)C> 014
    1                    5                   -3  01 111+V(1) <B(11) 00 013
    2             9+4*V(1)           -5+-2*V(1)  01 <B(11) 011+V(1) 00 013
    3            16+4*V(1)           -2+-2*V(1)  11 (11)E> 011+V(1) 00 013
    4            18+6*V(1)                    0  112+V(1) (11)E> 00 013
    5            20+6*V(1)                    2  113+V(1) (11)A> 013
    6            22+6*V(1)                    4  114+V(1) (10)D> 012
    7            33+6*V(1)                    1  114+V(1) <E(10) 10 01
    8           49+10*V(1)           -7+-2*V(1)  <E(10) 105+V(1) 01
    9           52+10*V(1)           -4+-2*V(1)  01 (11)F> 105+V(1) 01
   10           62+12*V(1)                    6  01 115+V(1) (11)F> 01
   11           64+12*V(1)                    8  01 116+V(1) (10)C>
   12           73+12*V(1)                    5  01 116+V(1) <E(10) 01
   13           97+16*V(1)           -7+-2*V(1)  01 <E(10) 106+V(1) 01
   14           99+16*V(1)           -9+-2*V(1)  <A(01) 107+V(1) 01
   15          110+16*V(1)           -6+-2*V(1)  11 (11)A> 107+V(1) 01
<< Success! ==> defined new CTR 22 (PPA)
83622276934    1764314[7]7087196         -14550524472  11 (11)A> 107275262462 01
== Executing  PA-CTR  1, V(1)=0, V(2)=7275262457, repcount=1818815615, factor=5/4
105448064314    2756741[7]1664856                  448  119094078076 (11)A> 102 01
== Executing PPA-CTR  9 (once), V(1)=9094078075
105448064332    2756741[7]6914158         -18188155706  01 11 (10)C> 019094078080 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=9094078075, repcount=2273519519, factor=5/4
130456779041    4307409[7]6318634                  446  01 1111367597596 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=11367597595
130456779056    4307409[7]7880264         -22735194750  11 (11)A> 1011367597602 01 10
== Executing  PA-CTR  5, V(1)=0, V(2)=11367597597, repcount=2841899400, factor=5/4
164559571856    6730326[7]3259864                  450  1114209497001 (11)A> 102 01 10
164559571857    6730326[7]3259866                  452  1114209497002 (01)D> 10 01 10
164559571858    6730326[7]3259869                  449  1114209497002 <E(10) 00 01 10
164559571859    6730326[7]1247877         -28418993555  <E(10) 1014209497002 00 01 10
164559571860    6730326[7]1247880         -28418993552  01 (11)F> 1014209497002 00 01 10
164559571861    6730326[7]0241884                  452  01 1114209497002 (11)F> 00 01 10
164559571862    6730326[7]0241886                  454  01 1114209497003 (11)B> 01 10
164559571863    6730326[7]0241893                  451  01 1114209497003 <B(11) 00 10
164559571864    6730326[7]8229905         -28418993555  01 <B(11) 0114209497003 00 10
164559571865    6730326[7]8229912         -28418993552  11 (11)E> 0114209497003 00 10
164559571866    6730326[7]7223918                  454  1114209497004 (11)E> 00 10
164559571867    6730326[7]7223920                  456  1114209497005 (11)A> 10
164559571868    6730326[7]7223922                  458  1114209497006 (01)D>
164559571869    6730326[7]7223925                  455  1114209497006 <A(01) 10
164559571870    6730326[7]7223931                  453  1114209497005 <B(11) 00 10
164559571871    6730326[7]5211951         -28418993557  <B(11) 0114209497005 00 10
164559571872    6730326[7]5211959         -28418993559  <E(10) 0114209497006 00 10
164559571873    6730326[7]5211962         -28418993556  01 (11)F> 0114209497006 00 10
164559571874    6730326[7]5211964         -28418993554  01 11 (10)C> 0114209497005 00 10
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  111+V(1) (11)A> 102 01 10
    1                    2                    2  112+V(1) (01)D> 10 01 10
    2                    5                   -1  112+V(1) <E(10) 00 01 10
    3            13+4*V(1)           -5+-2*V(1)  <E(10) 102+V(1) 00 01 10
    4            16+4*V(1)           -2+-2*V(1)  01 (11)F> 102+V(1) 00 01 10
    5            20+6*V(1)                    2  01 112+V(1) (11)F> 00 01 10
    6            22+6*V(1)                    4  01 113+V(1) (11)B> 01 10
    7            29+6*V(1)                    1  01 113+V(1) <B(11) 00 10
    8           41+10*V(1)           -5+-2*V(1)  01 <B(11) 013+V(1) 00 10
    9           48+10*V(1)           -2+-2*V(1)  11 (11)E> 013+V(1) 00 10
   10           54+12*V(1)                    4  114+V(1) (11)E> 00 10
   11           56+12*V(1)                    6  115+V(1) (11)A> 10
   12           58+12*V(1)                    8  116+V(1) (01)D>
   13           61+12*V(1)                    5  116+V(1) <A(01) 10
   14           67+12*V(1)                    3  115+V(1) <B(11) 00 10
   15           87+16*V(1)           -7+-2*V(1)  <B(11) 015+V(1) 00 10
   16           95+16*V(1)           -9+-2*V(1)  <E(10) 016+V(1) 00 10
   17           98+16*V(1)           -6+-2*V(1)  01 (11)F> 016+V(1) 00 10
   18          100+16*V(1)           -4+-2*V(1)  01 11 (10)C> 015+V(1) 00 10
<< Success! ==> defined new CTR 23 (PPA)
164559571874    6730326[7]5211964         -28418993554  01 11 (10)C> 0114209497005 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=14209497000, repcount=3552374251, factor=5/4
203635688635    1051613[8]0266528                  454  01 1117761871256 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=17761871255
203635688650    1051613[8]0206708         -35523742062  11 (11)A> 1017761871261 01
== Executing  PA-CTR  1, V(1)=0, V(2)=17761871256, repcount=4440467815, factor=5/4
256921302430    1643146[8]2339168                  458  1122202339076 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=22202339071
256921302437    1643146[8]1695496         -44404677694  01 11 (10)C> 0122202339076 00 11
== Executing  PA-CTR  2, V(1)=0, V(2)=22202339071, repcount=5550584768, factor=5/4
317977734885    2567415[8]9992328                  450  01 1127752923841 (10)C> 014 00 11
== Executing PPA-CTR 11 (once), V(1)=27752923840
317977734900    2567415[8]6773878         -55505847236  11 (11)A> 1027752923847 01 11
== Executing  PA-CTR  5, V(1)=0, V(2)=27752923842, repcount=6938230961, factor=5/4
401236506432    4011587[8]6132182                  452  1134691154806 (11)A> 103 01 11
401236506433    4011587[8]6132184                  454  1134691154807 (01)D> 102 01 11
401236506434    4011587[8]6132187                  451  1134691154807 <E(10) 00 10 01 11
401236506435    4011587[8]0751415         -69382309163  <E(10) 1034691154807 00 10 01 11
401236506436    4011587[8]0751418         -69382309160  01 (11)F> 1034691154807 00 10 01 11
401236506437    4011587[8]3061032                  454  01 1134691154807 (11)F> 00 10 01 11
401236506438    4011587[8]3061034                  456  01 1134691154808 (11)B> 10 01 11
401236506439    4011587[8]3061038                  458  01 1134691154809 (11)E> 01 11
401236506440    4011587[8]3061040                  460  01 1134691154810 (11)E> 11
401236506441    4011587[8]3061045                  457  01 1134691154810 <B(11) 01
401236506442    4011587[8]7680285         -69382309163  01 <B(11) 0134691154811
401236506443    4011587[8]7680292         -69382309160  11 (11)E> 0134691154811
401236506444    4011587[8]9989914                  462  1134691154812 (11)E>
401236506445    4011587[8]9989916                  464  1134691154813 (11)A>
401236506446    4011587[8]9989920                  466  1134691154814 (01)D>
401236506447    4011587[8]9989923                  463  1134691154814 <A(01) 10
401236506448    4011587[8]9989929                  461  1134691154813 <B(11) 00 10
401236506449    4011587[8]4609181         -69382309165  <B(11) 0134691154813 00 10
401236506450    4011587[8]4609189         -69382309167  <E(10) 0134691154814 00 10
401236506451    4011587[8]4609192         -69382309164  01 (11)F> 0134691154814 00 10
401236506452    4011587[8]4609194         -69382309162  01 11 (10)C> 0134691154813 00 10
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  111+V(1) (11)A> 103 011+V(2) 11
    1                    2                    2  112+V(1) (01)D> 102 011+V(2) 11
    2                    5                   -1  112+V(1) <E(10) 00 10 011+V(2) 11
    3            13+4*V(1)           -5+-2*V(1)  <E(10) 102+V(1) 00 10 011+V(2) 11
    4            16+4*V(1)           -2+-2*V(1)  01 (11)F> 102+V(1) 00 10 011+V(2) 11
    5            20+6*V(1)                    2  01 112+V(1) (11)F> 00 10 011+V(2) 11
    6            22+6*V(1)                    4  01 113+V(1) (11)B> 10 011+V(2) 11
    7            26+6*V(1)                    6  01 114+V(1) (11)E> 011+V(2) 11
    8     28+6*V(1)+2*V(2)             8+2*V(2)  01 115+V(1)+V(2) (11)E> 11
    9     33+6*V(1)+2*V(2)             5+2*V(2)  01 115+V(1)+V(2) <B(11) 01
   10    53+10*V(1)+6*V(2)           -5+-2*V(1)  01 <B(11) 016+V(1)+V(2)
   11    60+10*V(1)+6*V(2)           -2+-2*V(1)  11 (11)E> 016+V(1)+V(2)
   12    72+12*V(1)+8*V(2)            10+2*V(2)  117+V(1)+V(2) (11)E>
   13    74+12*V(1)+8*V(2)            12+2*V(2)  118+V(1)+V(2) (11)A>
   14    78+12*V(1)+8*V(2)            14+2*V(2)  119+V(1)+V(2) (01)D>
   15    81+12*V(1)+8*V(2)            11+2*V(2)  119+V(1)+V(2) <A(01) 10
   16    87+12*V(1)+8*V(2)             9+2*V(2)  118+V(1)+V(2) <B(11) 00 10
   17  119+16*V(1)+12*V(2)           -7+-2*V(1)  <B(11) 018+V(1)+V(2) 00 10
   18  127+16*V(1)+12*V(2)           -9+-2*V(1)  <E(10) 019+V(1)+V(2) 00 10
   19  130+16*V(1)+12*V(2)           -6+-2*V(1)  01 (11)F> 019+V(1)+V(2) 00 10
   20  132+16*V(1)+12*V(2)           -4+-2*V(1)  01 11 (10)C> 018+V(1)+V(2) 00 10
<< Success! ==> defined new CTR 24 (PPA)
401236506452    4011587[8]4609194         -69382309162  01 11 (10)C> 0134691154813 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=34691154808, repcount=8672788703, factor=5/4
496637182185    6268105[8]2091366                  462  01 1143363943516 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=43363943515
496637182200    6268105[8]5187706         -86727886574  11 (11)A> 1043363943521 01
== Executing  PA-CTR  1, V(1)=0, V(2)=43363943516, repcount=10840985880, factor=5/4
626729012760    9793914[8]9939626                  466  1154204929401 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=54204929396
626729012767    9793914[8]9657254        -108409858336  01 11 (10)C> 0154204929401 00 11
== Executing  PA-CTR  2, V(1)=0, V(2)=54204929396, repcount=13551232350, factor=5/4
775792568617    1530299[9]7232154                  464  01 1167756161751 (10)C> 01 00 11
== Executing PPA-CTR 17 (once), V(1)=67756161750
775792568632    1530299[9]5820252        -135512323042  11 (11)A> 1067756161756 01
== Executing  PA-CTR  1, V(1)=0, V(2)=67756161751, repcount=16939040438, factor=5/4
979061053888    2391092[9]0150464                  462  1184695202191 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=84695202190
979061053912    2391092[9]4598848        -169390403924  11 (11)A> 1084695202201 01
== Executing  PA-CTR  1, V(1)=0, V(2)=84695202196, repcount=21173800550, factor=5/4
1233146660512    3736081[9]2892548                  476  11105869002751 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=105869002746
1233146660519    3736081[9]8903576        -211738005026  01 11 (10)C> 01105869002751 00 11
== Executing  PA-CTR  2, V(1)=0, V(2)=105869002746, repcount=26467250687, factor=5/4
1524286418076    5837627[9]4586004                  470  01 11132336253436 (10)C> 013 00 11
== Executing PPA-CTR 19 (once), V(1)=132336253435
1524286418091    5837627[9]4641072        -264672506406  11 (11)A> 10132336253443
== Executing  PA-CTR 13, V(1)=0, V(2)=132336253438, repcount=33084063360, factor=5/4
1921295178411    9121293[9]7483312                  474  11165420316801 (11)A> 103
1921295178412    9121293[9]7483314                  476  11165420316802 (01)D> 102
1921295178413    9121293[9]7483317                  473  11165420316802 <E(10) 00 10
1921295178414    9121293[9]8750525        -330840633131  <E(10) 10165420316802 00 10
1921295178415    9121293[9]8750528        -330840633128  01 (11)F> 10165420316802 00 10
1921295178416    9121293[9]9384132                  476  01 11165420316802 (11)F> 00 10
1921295178417    9121293[9]9384134                  478  01 11165420316803 (11)B> 10
1921295178418    9121293[9]9384138                  480  01 11165420316804 (11)E>
1921295178419    9121293[9]9384140                  482  01 11165420316805 (11)A>
1921295178420    9121293[9]9384144                  484  01 11165420316806 (01)D>
1921295178421    9121293[9]9384147                  481  01 11165420316806 <A(01) 10
1921295178422    9121293[9]9384153                  479  01 11165420316805 <B(11) 00 10
1921295178423    9121293[9]0651373        -330840633131  01 <B(11) 01165420316805 00 10
1921295178424    9121293[9]0651380        -330840633128  11 (11)E> 01165420316805 00 10
1921295178425    9121293[9]1284990                  482  11165420316806 (11)E> 00 10
1921295178426    9121293[9]1284992                  484  11165420316807 (11)A> 10
1921295178427    9121293[9]1284994                  486  11165420316808 (01)D>
1921295178428    9121293[9]1284997                  483  11165420316808 <A(01) 10
1921295178429    9121293[9]1285003                  481  11165420316807 <B(11) 00 10
1921295178430    9121293[9]2552231        -330840633133  <B(11) 01165420316807 00 10
1921295178431    9121293[9]2552239        -330840633135  <E(10) 01165420316808 00 10
1921295178432    9121293[9]2552242        -330840633132  01 (11)F> 01165420316808 00 10
1921295178433    9121293[9]2552244        -330840633130  01 11 (10)C> 01165420316807 00 10
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  111+V(1) (11)A> 103
    1                    2                    2  112+V(1) (01)D> 102
    2                    5                   -1  112+V(1) <E(10) 00 10
    3            13+4*V(1)           -5+-2*V(1)  <E(10) 102+V(1) 00 10
    4            16+4*V(1)           -2+-2*V(1)  01 (11)F> 102+V(1) 00 10
    5            20+6*V(1)                    2  01 112+V(1) (11)F> 00 10
    6            22+6*V(1)                    4  01 113+V(1) (11)B> 10
    7            26+6*V(1)                    6  01 114+V(1) (11)E>
    8            28+6*V(1)                    8  01 115+V(1) (11)A>
    9            32+6*V(1)                   10  01 116+V(1) (01)D>
   10            35+6*V(1)                    7  01 116+V(1) <A(01) 10
   11            41+6*V(1)                    5  01 115+V(1) <B(11) 00 10
   12           61+10*V(1)           -5+-2*V(1)  01 <B(11) 015+V(1) 00 10
   13           68+10*V(1)           -2+-2*V(1)  11 (11)E> 015+V(1) 00 10
   14           78+12*V(1)                    8  116+V(1) (11)E> 00 10
   15           80+12*V(1)                   10  117+V(1) (11)A> 10
   16           82+12*V(1)                   12  118+V(1) (01)D>
   17           85+12*V(1)                    9  118+V(1) <A(01) 10
   18           91+12*V(1)                    7  117+V(1) <B(11) 00 10
   19          119+16*V(1)           -7+-2*V(1)  <B(11) 017+V(1) 00 10
   20          127+16*V(1)           -9+-2*V(1)  <E(10) 018+V(1) 00 10
   21          130+16*V(1)           -6+-2*V(1)  01 (11)F> 018+V(1) 00 10
   22          132+16*V(1)           -4+-2*V(1)  01 11 (10)C> 017+V(1) 00 10
<< Success! ==> defined new CTR 25 (PPA)
1921295178433    9121293[9]2552244        -330840633130  01 11 (10)C> 01165420316807 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=165420316802, repcount=41355079201, factor=5/4
2376201049644   1425202[10]9197108                  478  01 11206775396006 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=206775396005
2376201049671   1425202[10]7909422        -413550791538  01 11 (10)C> 01206775396015 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=206775396010, repcount=51693849003, factor=5/4
2944833388704   2226878[10]1595794                  486  01 11258469245016 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=258469245015
2944833388731   2226878[10]4986328        -516938489550  01 11 (10)C> 01258469245025 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=258469245020, repcount=64617311256, factor=5/4
3655623812547   3479497[10]2495112                  498  01 11323086556281 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=323086556280
3655623812562   3479497[10]7395692        -646173112068  11 (11)A> 10323086556286 01
== Executing  PA-CTR  1, V(1)=0, V(2)=323086556281, repcount=80771639071, factor=5/4
4624883481414   5436714[10]5415336                  500  11403858195356 (11)A> 102 01
== Executing PPA-CTR  9 (once), V(1)=403858195355
4624883481432   5436714[10]6541118        -807716390214  01 11 (10)C> 01403858195360 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=403858195355, repcount=100964548839, factor=5/4
5735493518661   8494866[10]8639274                  498  01 11504822744196 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=504822744195
5735493518676   8494866[10]2546504       -1009645487898  11 (11)A> 10504822744202 01 10
== Executing  PA-CTR  5, V(1)=0, V(2)=504822744197, repcount=126205686050, factor=5/4
7249961751276   1327322[11]3947204                  502  11631028430251 (11)A> 102 01 10
== Executing PPA-CTR 23 (once), V(1)=631028430250
7249961751294   1327322[11]8831304       -1262056860002  01 11 (10)C> 01631028430255 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=631028430250, repcount=157757107563, factor=5/4
8985289934487   2073942[11]4457516                  502  01 11788785537816 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=788785537815
8985289934514   2073942[11]6289650       -1577571075134  01 11 (10)C> 01788785537825 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=788785537820, repcount=197196384456, factor=5/4
11154450163530   3240534[11]5839234                  514  01 11985981922281 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=985981922280
11154450163545   3240534[11]6595814       -1971963844052  11 (11)A> 10985981922286 01
== Executing  PA-CTR  1, V(1)=0, V(2)=985981922281, repcount=246495480571, factor=5/4
14112395930397   5063335[11]7516458                  516  111232477402856 (11)A> 102 01
== Executing PPA-CTR  9 (once), V(1)=1232477402855
14112395930415   5063335[11]5962240       -2464954805198  01 11 (10)C> 011232477402860 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=1232477402855, repcount=308119350714, factor=5/4
17501708788269   7911461[11]3180396                  514  01 111540596753571 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=1540596753570
17501708788284   7911461[11]1237626       -3081193506632  11 (11)A> 101540596753577 01 10
== Executing  PA-CTR  5, V(1)=0, V(2)=1540596753572, repcount=385149188394, factor=5/4
22123499049012   1236165[12]2620102                  520  111925745941971 (11)A> 10 01 10
== Executing PPA-CTR 12 (once), V(1)=1925745941966
22123499049019   1236165[12]6388010       -3851491883422  01 11 (10)C> 011925745941971 00 11 10
== Executing  PA-CTR  6, V(1)=0, V(2)=1925745941966, repcount=481436485492, factor=5/4
27419300389431   1931509[12]1356658                  514  01 112407182427461 (10)C> 013 00 11 10
27419300389432   1931509[12]1356663                  511  01 112407182427461 <B(11) 00 012 00 11 10
27419300389433   1931509[12]1066507       -4814364854411  01 <B(11) 012407182427461 00 012 00 11 10
27419300389434   1931509[12]1066514       -4814364854408  11 (11)E> 012407182427461 00 012 00 11 10
27419300389435   1931509[12]5921436                  514  112407182427462 (11)E> 00 012 00 11 10
27419300389436   1931509[12]5921438                  516  112407182427463 (11)A> 012 00 11 10
27419300389437   1931509[12]5921440                  518  112407182427464 (10)D> 01 00 11 10
27419300389438   1931509[12]5921451                  515  112407182427464 <E(10) 10 00 11 10
27419300389439   1931509[12]5631307       -4814364854413  <E(10) 102407182427465 00 11 10
27419300389440   1931509[12]5631310       -4814364854410  01 (11)F> 102407182427465 00 11 10
27419300389441   1931509[12]0486240                  520  01 112407182427465 (11)F> 00 11 10
27419300389442   1931509[12]0486242                  522  01 112407182427466 (11)B> 11 10
27419300389443   1931509[12]0486249                  519  01 112407182427466 <E(10) 102
27419300389444   1931509[12]0196113       -4814364854413  01 <E(10) 102407182427468
27419300389445   1931509[12]0196115       -4814364854415  <A(01) 102407182427469
27419300389446   1931509[12]0196126       -4814364854412  11 (11)A> 102407182427469
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  01 111+V(1) (10)C> 013 00 11 101+V(2)
    1                    5                   -3  01 111+V(1) <B(11) 00 012 00 11 101+V(2)
    2             9+4*V(1)           -5+-2*V(1)  01 <B(11) 011+V(1) 00 012 00 11 101+V(2)
    3            16+4*V(1)           -2+-2*V(1)  11 (11)E> 011+V(1) 00 012 00 11 101+V(2)
    4            18+6*V(1)                    0  112+V(1) (11)E> 00 012 00 11 101+V(2)
    5            20+6*V(1)                    2  113+V(1) (11)A> 012 00 11 101+V(2)
    6            22+6*V(1)                    4  114+V(1) (10)D> 01 00 11 101+V(2)
    7            33+6*V(1)                    1  114+V(1) <E(10) 10 00 11 101+V(2)
    8           49+10*V(1)           -7+-2*V(1)  <E(10) 105+V(1) 00 11 101+V(2)
    9           52+10*V(1)           -4+-2*V(1)  01 (11)F> 105+V(1) 00 11 101+V(2)
   10           62+12*V(1)                    6  01 115+V(1) (11)F> 00 11 101+V(2)
   11           64+12*V(1)                    8  01 116+V(1) (11)B> 11 101+V(2)
   12           71+12*V(1)                    5  01 116+V(1) <E(10) 102+V(2)
   13           95+16*V(1)           -7+-2*V(1)  01 <E(10) 108+V(1)+V(2)
   14           97+16*V(1)           -9+-2*V(1)  <A(01) 109+V(1)+V(2)
   15          108+16*V(1)           -6+-2*V(1)  11 (11)A> 109+V(1)+V(2)
<< Success! ==> defined new CTR 26 (PPA)
27419300389446   1931509[12]0196126       -4814364854412  11 (11)A> 102407182427469
== Executing  PA-CTR 13, V(1)=0, V(2)=2407182427464, repcount=601795606867, factor=5/4
34640847671850   3017982[12]7500274                  524  113008978034336 (11)A> 10
34640847671851   3017982[12]7500276                  526  113008978034337 (01)D>
34640847671852   3017982[12]7500279                  523  113008978034337 <A(01) 10
34640847671853   3017982[12]7500285                  521  113008978034336 <B(11) 00 10
34640847671854   3017982[12]9637629       -6017956068151  <B(11) 013008978034336 00 10
34640847671855   3017982[12]9637637       -6017956068153  <E(10) 013008978034337 00 10
34640847671856   3017982[12]9637640       -6017956068150  01 (11)F> 013008978034337 00 10
34640847671857   3017982[12]9637642       -6017956068148  01 11 (10)C> 013008978034336 00 10
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  115+V(1) (11)A> 10
    1                    2                    2  116+V(1) (01)D>
    2                    5                   -1  116+V(1) <A(01) 10
    3                   11                   -3  115+V(1) <B(11) 00 10
    4            31+4*V(1)          -13+-2*V(1)  <B(11) 015+V(1) 00 10
    5            39+4*V(1)          -15+-2*V(1)  <E(10) 016+V(1) 00 10
    6            42+4*V(1)          -12+-2*V(1)  01 (11)F> 016+V(1) 00 10
    7            44+4*V(1)          -10+-2*V(1)  01 11 (10)C> 015+V(1) 00 10
<< Success! ==> defined new CTR 27 (PPA)
34640847671857   3017982[12]9637642       -6017956068148  01 11 (10)C> 013008978034336 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=3008978034331, repcount=752244508583, factor=5/4
42915537266270   4715598[12]2966134                  516  01 113761222542916 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=3761222542915
42915537266285   4715598[12]3652884       -7522445085320  11 (11)A> 103761222542922 01 10
== Executing  PA-CTR  5, V(1)=0, V(2)=3761222542917, repcount=940305635730, factor=5/4
54199204895045   7368122[12]4254704                  520  114701528178651 (11)A> 102 01 10
== Executing PPA-CTR 23 (once), V(1)=4701528178650
54199204895063   7368122[12]5113204       -9403056356784  01 11 (10)C> 014701528178655 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=4701528178650, repcount=1175382044663, factor=5/4
67128407386356   1151269[13]8138816                  520  01 115876910223316 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=5876910223315
67128407386383   1151269[13]3051950      -11753820446116  01 11 (10)C> 015876910223325 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=5876910223320, repcount=1469227555831, factor=5/4
83289910500524   1798858[13]2967034                  532  01 117346137779156 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=7346137779155
83289910500539   1798858[13]7433614      -14692275557784  11 (11)A> 107346137779161 01
== Executing  PA-CTR  1, V(1)=0, V(2)=7346137779156, repcount=1836534444790, factor=5/4
105328323838019   2810715[13]2879474                  536  119182672223951 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=9182672223946
105328323838026   2810715[13]1775302      -18365344447366  01 11 (10)C> 019182672223951 00 11
== Executing  PA-CTR  2, V(1)=0, V(2)=9182672223946, repcount=2295668055987, factor=5/4
130580672453883   4391743[13]2003930                  530  01 1111478340279936 (10)C> 013 00 11
== Executing PPA-CTR 19 (once), V(1)=11478340279935
130580672453898   4391743[13]6482998      -22956680559346  11 (11)A> 1011478340279943
== Executing  PA-CTR 13, V(1)=0, V(2)=11478340279938, repcount=2869585069985, factor=5/4
165015693293718   6862098[13]5869238                  534  1114347925349926 (11)A> 103
== Executing PPA-CTR 25 (once), V(1)=14347925349925
165015693293740   6862098[13]1468170      -28695850699320  01 11 (10)C> 0114347925349932 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=14347925349927, repcount=3586981337482, factor=5/4
204472488006042   1072202[14]9952278                  536  01 1117934906687411 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=17934906687410
204472488006057   1072202[14]6950948      -35869813374290  11 (11)A> 1017934906687417 01 10
== Executing  PA-CTR  5, V(1)=0, V(2)=17934906687412, repcount=4483726671854, factor=5/4
258277208068305   1675317[14]7713464                  542  1122418633359271 (11)A> 10 01 10
== Executing PPA-CTR 12 (once), V(1)=22418633359266
258277208068312   1675317[14]1150572      -44837266718000  01 11 (10)C> 0122418633359271 00 11 10
== Executing  PA-CTR  6, V(1)=0, V(2)=22418633359266, repcount=5604658339817, factor=5/4
319928449806299   2617682[14]2509020                  536  01 1128023291699086 (10)C> 013 00 11 10
== Executing PPA-CTR 26 (once), V(1)=28023291699085, V(2)=0
319928449806314   2617682[14]9694488      -56046583397640  11 (11)A> 1028023291699094
== Executing  PA-CTR 13, V(1)=0, V(2)=28023291699089, repcount=7005822924773, factor=5/4
403998324903590   4090129[14]2182640                  544  1135029114623866 (11)A> 102
== Executing PPA-CTR 14 (once), V(1)=35029114623864
403998324903600   4090129[14]8421348      -70058229247190  11 (11)A> 1035029114623869 01
== Executing  PA-CTR  1, V(1)=0, V(2)=35029114623864, repcount=8757278655967, factor=5/4
509085668775204   6390827[14]3876896                  546  1143786393279836 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=43786393279831
509085668775211   6390827[14]6996264      -87572786559126  01 11 (10)C> 0143786393279836 00 11
== Executing  PA-CTR  2, V(1)=0, V(2)=43786393279831, repcount=10946598319958, factor=5/4
629498250294749   9985667[14]3527756                  538  01 1154732991599791 (10)C> 014 00 11
== Executing PPA-CTR 11 (once), V(1)=54732991599790
629498250294764   9985667[14]9124506     -109465983199048  11 (11)A> 1054732991599797 01 11
== Executing  PA-CTR  5, V(1)=0, V(2)=54732991599792, repcount=13683247899949, factor=5/4
793697225094152   1560260[15]3800802                  544  1168416239499746 (11)A> 10 01 11
== Executing PPA-CTR 12 (once), V(1)=68416239499741
793697225094159   1560260[15]1799810     -136832478998948  01 11 (10)C> 0168416239499746 00 11 11
== Executing  PA-CTR  6, V(1)=0, V(2)=68416239499741, repcount=17104059874936, factor=5/4
981841883718455   2437907[15]7670514                  540  01 1185520299374681 (10)C> 012 00 11 11
981841883718456   2437907[15]7670519                  537  01 1185520299374681 <B(11) 00 01 00 11 11
981841883718457   2437907[15]5169243     -171040598748825  01 <B(11) 0185520299374681 00 01 00 11 11
981841883718458   2437907[15]5169250     -171040598748822  11 (11)E> 0185520299374681 00 01 00 11 11
981841883718459   2437907[15]3918612                  540  1185520299374682 (11)E> 00 01 00 11 11
981841883718460   2437907[15]3918614                  542  1185520299374683 (11)A> 01 00 11 11
981841883718461   2437907[15]3918616                  544  1185520299374684 (10)D> 00 11 11
981841883718462   2437907[15]3918620                  546  1185520299374685 (11)F> 11 11
981841883718463   2437907[15]3918629                  543  1185520299374685 <E(10) 10 11
981841883718464   2437907[15]1417369     -171040598748827  <E(10) 1085520299374686 11
981841883718465   2437907[15]1417372     -171040598748824  01 (11)F> 1085520299374686 11
981841883718466   2437907[15]0166744                  548  01 1185520299374686 (11)F> 11
981841883718467   2437907[15]0166753                  545  01 1185520299374686 <E(10) 10
981841883718468   2437907[15]7665497     -171040598748827  01 <E(10) 1085520299374687
981841883718469   2437907[15]7665499     -171040598748829  <A(01) 1085520299374688
981841883718470   2437907[15]7665510     -171040598748826  11 (11)A> 1085520299374688
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 111+V(1) (10)C> 012 00 11 11
    1                    5                   -3  01 111+V(1) <B(11) 00 01 00 11 11
    2             9+4*V(1)           -5+-2*V(1)  01 <B(11) 011+V(1) 00 01 00 11 11
    3            16+4*V(1)           -2+-2*V(1)  11 (11)E> 011+V(1) 00 01 00 11 11
    4            18+6*V(1)                    0  112+V(1) (11)E> 00 01 00 11 11
    5            20+6*V(1)                    2  113+V(1) (11)A> 01 00 11 11
    6            22+6*V(1)                    4  114+V(1) (10)D> 00 11 11
    7            26+6*V(1)                    6  115+V(1) (11)F> 11 11
    8            35+6*V(1)                    3  115+V(1) <E(10) 10 11
    9           55+10*V(1)           -7+-2*V(1)  <E(10) 106+V(1) 11
   10           58+10*V(1)           -4+-2*V(1)  01 (11)F> 106+V(1) 11
   11           70+12*V(1)                    8  01 116+V(1) (11)F> 11
   12           79+12*V(1)                    5  01 116+V(1) <E(10) 10
   13          103+16*V(1)           -7+-2*V(1)  01 <E(10) 107+V(1)
   14          105+16*V(1)           -9+-2*V(1)  <A(01) 108+V(1)
   15          116+16*V(1)           -6+-2*V(1)  11 (11)A> 108+V(1)
<< Success! ==> defined new CTR 28 (PPA)
981841883718470   2437907[15]7665510     -171040598748826  11 (11)A> 1085520299374688
== Executing  PA-CTR 13, V(1)=0, V(2)=85520299374683, repcount=21380074843671, factor=5/4
1238402781842522   3809230[15]5037554                  542  11106900374218356 (11)A> 104
== Executing PPA-CTR 20 (once), V(1)=106900374218355
1238402781842541   3809230[15]2531348     -213800748436172  01 11 (10)C> 01106900374218361 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=106900374218356, repcount=26725093554590, factor=5/4
1532378810943031   5951921[15]5430408                  548  01 11133625467772951 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=133625467772950
1532378810943046   5951921[15]9797708     -267250935545358  11 (11)A> 10133625467772956 01
== Executing  PA-CTR  1, V(1)=0, V(2)=133625467772951, repcount=33406366943238, factor=5/4
1933255214261902   9299877[15]3607120                  546  11167031834716191 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=167031834716190
1933255214261926   9299877[15]7363504     -334063669431840  11 (11)A> 10167031834716201 01
== Executing  PA-CTR  1, V(1)=0, V(2)=167031834716196, repcount=41757958679050, factor=5/4
2434350718410526   1453105[16]9526204                  560  11208789793395251 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=208789793395246
2434350718410533   1453105[16]3107232     -417579586789942  01 11 (10)C> 01208789793395251 00 11
== Executing  PA-CTR  2, V(1)=0, V(2)=208789793395246, repcount=52197448348812, factor=5/4
3008522650247465   2270478[16]1307160                  554  01 11260987241744061 (10)C> 013 00 11
== Executing PPA-CTR 19 (once), V(1)=260987241744060
3008522650247480   2270478[16]9212228     -521974483487572  11 (11)A> 10260987241744068
== Executing  PA-CTR 13, V(1)=0, V(2)=260987241744063, repcount=65246810436016, factor=5/4
3791484375479672   3547621[16]2604452                  556  11326234052180081 (11)A> 104
== Executing PPA-CTR 20 (once), V(1)=326234052180080
3791484375479691   3547621[16]7485846     -652468104359608  01 11 (10)C> 01326234052180086 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=326234052180081, repcount=81558513045021, factor=5/4
4688628018974922   5543159[16]7729790                  560  01 11407792565225106 (10)C> 012 00 10
== Executing PPA-CTR  3 (once), V(1)=407792565225105, V(2)=0
4688628018974940   5543159[16]1331612     -815585130449656  11 (11)A> 10407792565225114 01
== Executing  PA-CTR  1, V(1)=0, V(2)=407792565225109, repcount=101948141306278, factor=5/4
5912005714650276   8661186[16]2143584                  568  11509740706531391 (11)A> 102 01
== Executing PPA-CTR  9 (once), V(1)=509740706531390
5912005714650294   8661186[16]6645926    -1019481413062216  01 11 (10)C> 01509740706531395 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=509740706531390, repcount=127435176632848, factor=5/4
7313792657611622   1353310[17]9895878                  568  01 11637175883164241 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=637175883164240
7313792657611649   1353310[17]9509362    -1274351766327918  01 11 (10)C> 01637175883164250 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=637175883164245, repcount=159293970791062, factor=5/4
9066026336313331   2114547[17]9040790                  578  01 11796469853955311 (10)C> 012 00 10
== Executing PPA-CTR  3 (once), V(1)=796469853955310, V(2)=0
9066026336313349   2114547[17]2325892    -1592939707910048  11 (11)A> 10796469853955319 01
== Executing  PA-CTR  1, V(1)=0, V(2)=796469853955314, repcount=199117463488829, factor=5/4
11455435898179297   3303980[17]4683308                  584  11995587317444146 (11)A> 103 01
== Executing PPA-CTR  4 (once), V(1)=995587317444145, V(2)=0
11455435898179320   3303980[17]3789772    -1991174634887710  01 11 (10)C> 01995587317444153 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=995587317444148, repcount=248896829361038, factor=5/4
14193301021150738   5162469[17]5188384                  594  01 111244484146805191 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=1244484146805190
14193301021150753   5162469[17]4071524    -2488968293609792  11 (11)A> 101244484146805196 01
== Executing  PA-CTR  1, V(1)=0, V(2)=1244484146805191, repcount=311121036701298, factor=5/4
17926753461566329   8066358[17]8459776                  592  111555605183506491 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=1555605183506490
17926753461566353   8066358[17]5602760    -3111210367012394  11 (11)A> 101555605183506501 01
== Executing  PA-CTR  1, V(1)=0, V(2)=1555605183506496, repcount=388901295876625, factor=5/4
22593569012085853   1260368[18]7126760                  606  111944506479383126 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=1944506479383121
22593569012085860   1260368[18]4659288    -3889012958765646  01 11 (10)C> 011944506479383126 00 11
== Executing  PA-CTR  2, V(1)=0, V(2)=1944506479383121, repcount=486126619845781, factor=5/4
27940961830389451   1969325[18]4414672                  602  01 112430633099228906 (10)C> 012 00 11
27940961830389452   1969325[18]4414677                  599  01 112430633099228906 <B(11) 00 01 00 11
27940961830389453   1969325[18]1330301    -4861266198457213  01 <B(11) 012430633099228906 00 01 00 11
27940961830389454   1969325[18]1330308    -4861266198457210  11 (11)E> 012430633099228906 00 01 00 11
27940961830389455   1969325[18]9788120                  602  112430633099228907 (11)E> 00 01 00 11
27940961830389456   1969325[18]9788122                  604  112430633099228908 (11)A> 01 00 11
27940961830389457   1969325[18]9788124                  606  112430633099228909 (10)D> 00 11
27940961830389458   1969325[18]9788128                  608  112430633099228910 (11)F> 11
27940961830389459   1969325[18]9788137                  605  112430633099228910 <E(10) 10
27940961830389460   1969325[18]6703777    -4861266198457215  <E(10) 102430633099228911
27940961830389461   1969325[18]6703780    -4861266198457212  01 (11)F> 102430633099228911
27940961830389462   1969325[18]5161602                  610  01 112430633099228911 (11)F>
27940961830389463   1969325[18]5161604                  612  01 112430633099228912 (11)B>
27940961830389464   1969325[18]5161615                  609  01 112430633099228912 <E(10) 01
27940961830389465   1969325[18]2077263    -4861266198457215  01 <E(10) 102430633099228912 01
27940961830389466   1969325[18]2077265    -4861266198457217  <A(01) 102430633099228913 01
27940961830389467   1969325[18]2077276    -4861266198457214  11 (11)A> 102430633099228913 01
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 111+V(1) (10)C> 012 00 11
    1                    5                   -3  01 111+V(1) <B(11) 00 01 00 11
    2             9+4*V(1)           -5+-2*V(1)  01 <B(11) 011+V(1) 00 01 00 11
    3            16+4*V(1)           -2+-2*V(1)  11 (11)E> 011+V(1) 00 01 00 11
    4            18+6*V(1)                    0  112+V(1) (11)E> 00 01 00 11
    5            20+6*V(1)                    2  113+V(1) (11)A> 01 00 11
    6            22+6*V(1)                    4  114+V(1) (10)D> 00 11
    7            26+6*V(1)                    6  115+V(1) (11)F> 11
    8            35+6*V(1)                    3  115+V(1) <E(10) 10
    9           55+10*V(1)           -7+-2*V(1)  <E(10) 106+V(1)
   10           58+10*V(1)           -4+-2*V(1)  01 (11)F> 106+V(1)
   11           70+12*V(1)                    8  01 116+V(1) (11)F>
   12           72+12*V(1)                   10  01 117+V(1) (11)B>
   13           83+12*V(1)                    7  01 117+V(1) <E(10) 01
   14          111+16*V(1)           -7+-2*V(1)  01 <E(10) 107+V(1) 01
   15          113+16*V(1)           -9+-2*V(1)  <A(01) 108+V(1) 01
   16          124+16*V(1)           -6+-2*V(1)  11 (11)A> 108+V(1) 01
<< Success! ==> defined new CTR 29 (PPA)
27940961830389467   1969325[18]2077276    -4861266198457214  11 (11)A> 102430633099228913 01
== Executing  PA-CTR  1, V(1)=0, V(2)=2430633099228908, repcount=607658274807228, factor=5/4
35232861128076203   3077071[18]6842548                  610  113038291374036141 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=3038291374036136
35232861128076210   3077071[18]2987136    -6076582748071672  01 11 (10)C> 013038291374036141 00 11
== Executing  PA-CTR  2, V(1)=0, V(2)=3038291374036136, repcount=759572843509035, factor=5/4
43588162406675595   4807924[18]1231076                  608  01 113797864217545176 (10)C> 01 00 11
== Executing PPA-CTR 17 (once), V(1)=3797864217545175
43588162406675610   4807924[18]1953974    -7595728435089748  11 (11)A> 103797864217545181 01
== Executing  PA-CTR  1, V(1)=0, V(2)=3797864217545176, repcount=949466054386295, factor=5/4
54981755059311150   7512381[18]5898754                  612  114747330271931476 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=4747330271931471
54981755059311157   7512381[18]3624682    -9494660543862340  01 11 (10)C> 014747330271931476 00 11
== Executing  PA-CTR  2, V(1)=0, V(2)=4747330271931471, repcount=1186832567982868, factor=5/4
68036913307122705   1173809[19]0204914                  604  01 115934162839914341 (10)C> 014 00 11
== Executing PPA-CTR 11 (once), V(1)=5934162839914340
68036913307122720   1173809[19]8834464    -118683[4]9828082  11 (11)A> 105934162839914347 01 11
== Executing  PA-CTR  5, V(1)=0, V(2)=5934162839914342, repcount=1483540709978586, factor=5/4
85839401826865752   1834077[19]4888268                  606  117417703549892931 (11)A> 103 01 11
== Executing PPA-CTR 24 (once), V(1)=7417703549892930, V(2)=0
85839401826865772   1834077[19]3175280    -148354[4]9785258  01 11 (10)C> 017417703549892938 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=7417703549892933, repcount=1854425887473234, factor=5/4
1062380[4]9071346   2865746[19]9827916                  614  01 119272129437366171 (10)C> 012 00 10
== Executing PPA-CTR  3 (once), V(1)=9272129437366170, V(2)=0
1062380[4]9071364   2865746[19]7686778    -185442[4]4731732  11 (11)A> 109272129437366179 01
== Executing  PA-CTR  1, V(1)=0, V(2)=9272129437366174, repcount=2318032359341544, factor=5/4
1340544[4]1169892   4477728[19]4417354                  620  1111590161796707721 (11)A> 103 01
== Executing PPA-CTR  4 (once), V(1)=11590161796707720, V(2)=0
1340544[4]1169915   4477728[19]1741018    -231803[4]3414824  01 11 (10)C> 0111590161796707728 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=11590161796707723, repcount=2897540449176931, factor=5/4
1659274[4]2116156   6996450[19]1119502                  624  01 1114487702245884656 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=14487702245884655
1659274[4]2116171   6996450[19]5274092    -289754[4]1768692  11 (11)A> 1014487702245884662 01 10
== Executing  PA-CTR  5, V(1)=0, V(2)=14487702245884657, repcount=3621925561471165, factor=5/4
2093905[4]9770151   1093195[20]9010452                  628  1118109627807355826 (11)A> 102 01 10
== Executing PPA-CTR 23 (once), V(1)=18109627807355825
2093905[4]9770169   1093195[20]6703752    -362192[4]4711026  01 11 (10)C> 0118109627807355830 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=18109627807355825, repcount=4527406951838957, factor=5/4
2591920[4]9998696   1708117[20]4663760                  630  01 1122637034759194786 (10)C> 012 00 10
== Executing PPA-CTR  3 (once), V(1)=22637034759194785, V(2)=0
2591920[4]9998714   1708117[20]1780462    -452740[4]8388946  11 (11)A> 1022637034759194794 01
== Executing  PA-CTR  1, V(1)=0, V(2)=22637034759194789, repcount=5659258689798698, factor=5/4
3271031[4]7583090   2668934[20]9792314                  638  1128296293448993491 (11)A> 102 01
== Executing PPA-CTR  9 (once), V(1)=28296293448993490
3271031[4]7583108   2668934[20]3688256    -565925[4]7986346  01 11 (10)C> 0128296293448993495 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=28296293448993490, repcount=7074073362248373, factor=5/4
4049179[4]2315211   4170209[20]4546808                  638  01 1135370366811241866 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=35370366811241865
4049179[4]2315238   4170209[20]1868042    -707407[4]2483098  01 11 (10)C> 0135370366811241875 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=35370366811241870, repcount=8842591702810468, factor=5/4
5021864[4]3230386   6515952[20]8794674                  646  01 1144212958514052341 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=44212958514052340
5021864[4]3230413   6515952[20]7946358    -884259[4]8104040  01 11 (10)C> 0144212958514052350 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=44212958514052345, repcount=11053239628513087, factor=5/4
6237720[4]6874370   1018117[21]5478386                  656  01 1155266198142565436 (10)C> 012 00 10
== Executing PPA-CTR  3 (once), V(1)=55266198142565435, V(2)=0
6237720[4]6874388   1018117[21]6525488    -110532[5]5130220  11 (11)A> 1055266198142565444 01
== Executing  PA-CTR  1, V(1)=0, V(2)=55266198142565439, repcount=13816549535641360, factor=5/4
7895706[4]4570708   1590808[21]7819728                  660  1169082747678206801 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=69082747678206800
7895706[4]4570732   1590808[21]8369532    -138165[5]6412946  11 (11)A> 1069082747678206811 01
== Executing  PA-CTR  1, V(1)=0, V(2)=69082747678206806, repcount=17270686919551702, factor=5/4
9968188[4]9191156   2485638[21]6031520                  670  1186353434597758511 (11)A> 103 01
== Executing PPA-CTR  4 (once), V(1)=86353434597758510, V(2)=0
9968188[4]9191179   2485638[21]0167824    -172706[5]5516354  01 11 (10)C> 0186353434597758518 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=86353434597758513, repcount=21588358649439629, factor=5/4
1234290[5]3027098   3883810[21]0844440                  678  01 111079417[4]7198146 (10)C> 012 00 10
== Executing PPA-CTR  3 (once), V(1)=1079417[4]7198145, V(2)=0
1234290[5]3027116   3883810[21]6014902    -215883[5]4395618  11 (11)A> 101079417[4]7198154 01
== Executing  PA-CTR  1, V(1)=0, V(2)=1079417[4]7198149, repcount=26985448311799538, factor=5/4
1558116[5]4621572   6068453[21]7602514                  686  111349272[4]8997691 (11)A> 102 01
== Executing PPA-CTR  9 (once), V(1)=1349272[4]8997690
1558116[5]4621590   6068453[21]1565656    -269854[5]7994698  01 11 (10)C> 011349272[4]8997695 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=1349272[4]8997690, repcount=33731810389749423, factor=5/4
1929166[5]1865243   9481958[21]8033908                  686  01 111686590[4]8747116 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=1686590[4]8747115
1929166[5]1865270   9481958[21]0470642    -337318[5]7493550  01 11 (10)C> 011686590[4]8747125 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=1686590[4]8747120, repcount=42164762987186781, factor=5/4
2392978[5]0919861   1481556[22]9080026                  698  01 112108238[4]5933906 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=2108238[4]5933905
2392978[5]0919876   1481556[22]4022606    -421647[5]1867118  11 (11)A> 102108238[4]5933911 01
== Executing  PA-CTR  1, V(1)=0, V(2)=2108238[4]5933906, repcount=52705953733983477, factor=5/4
3025449[5]8721600   2314931[22]9746694                  698  112635297[4]9917386 (11)A> 103 01
== Executing PPA-CTR  4 (once), V(1)=2635297[4]9917385, V(2)=0
3025449[5]8721623   2314931[22]8424998    -527059[5]9834076  01 11 (10)C> 012635297[4]9917393 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=2635297[4]9917388, repcount=65882442167479348, factor=5/4
3750156[5]0994451   3617080[22]7875950                  708  01 113294122[4]7396741 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=3294122[4]7396740
3750156[5]0994466   3617080[22]6223890    -658824[5]4792778  11 (11)A> 103294122[4]7396746 01
== Executing  PA-CTR  1, V(1)=0, V(2)=3294122[4]7396741, repcount=82353052709349186, factor=5/4
4738393[5]3184698   5651687[22]9974094                  710  114117652[4]6745931 (11)A> 102 01
== Executing PPA-CTR  9 (once), V(1)=4117652[4]6745930
4738393[5]3184716   5651687[22]7909076    -823530[5]3491154  01 11 (10)C> 014117652[4]6745935 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=4117652[4]6745930, repcount=1029413[4]6686483, factor=5/4
5870747[5]6736029   8830762[22]2528168                  710  01 115147065[4]3432416 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=5147065[4]3432415
5870747[5]6736056   8830762[22]8041502    -102941[6]6864126  01 11 (10)C> 015147065[4]3432425 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=5147065[4]3432420, repcount=1286766[4]8358106, factor=5/4
7286191[5]8675222   1379806[23]9434186                  722  01 116433832[4]1790531 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=6433832[4]1790530
7286191[5]8675237   1379806[23]8082766    -128676[6]3580344  11 (11)A> 106433832[4]1790536 01
== Executing  PA-CTR  1, V(1)=0, V(2)=6433832[4]1790531, repcount=1608458[4]2947633, factor=5/4
9216340[5]4046833   2155947[23]7382958                  720  118042290[4]4738166 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=8042290[4]4738165
9216340[5]4046857   2155947[23]1622792    -160845[6]9475616  11 (11)A> 108042290[4]4738176 01
== Executing  PA-CTR  1, V(1)=0, V(2)=8042290[4]4738171, repcount=2010572[4]1184543, factor=5/4
1162902[6]8261373   3368668[23]5462724                  728  111005286[5]5922716 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=1005286[5]5922715
1162902[6]8261397   3368668[23]5762658    -201057[6]1844708  11 (11)A> 101005286[5]5922726 01
== Executing  PA-CTR  1, V(1)=0, V(2)=1005286[5]5922721, repcount=2513215[4]8980681, factor=5/4
1464488[6]6029569   5263544[23]7818642                  740  111256607[5]4903406 (11)A> 102 01
== Executing PPA-CTR  9 (once), V(1)=1256607[5]4903405
1464488[6]6029587   5263544[23]6273224    -251321[6]9806074  01 11 (10)C> 011256607[5]4903410 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=1256607[5]4903405, repcount=3141519[4]6225852, factor=5/4
1810055[6]4513959   8224288[23]1729312                  742  01 111570759[5]1129261 (10)C> 012 00 10
== Executing PPA-CTR  3 (once), V(1)=1570759[5]1129260, V(2)=0
1810055[6]4513977   8224288[23]9797614    -314151[6]2257784  11 (11)A> 101570759[5]1129269 01
== Executing  PA-CTR  1, V(1)=0, V(2)=1570759[5]1129264, repcount=3926899[4]2782317, factor=5/4
2281283[6]7901781   1285045[24]1051062                  752  111963449[5]3911586 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=1963449[5]3911581
2281283[6]7901788   1285045[24]6697430    -392689[6]7822420  01 11 (10)C> 011963449[5]3911586 00 11
== Executing  PA-CTR  2, V(1)=0, V(2)=1963449[5]3911581, repcount=4908624[4]0977896, factor=5/4
2821232[6]8658644   2007882[24]7550374                  748  01 112454312[5]4889481 (10)C> 012 00 11
== Executing PPA-CTR 29 (once), V(1)=2454312[5]4889480
2821232[6]8658660   2007882[24]5782178    -490862[6]9778218  11 (11)A> 102454312[5]4889488 01
== Executing  PA-CTR  1, V(1)=0, V(2)=2454312[5]4889483, repcount=6135780[4]3722371, factor=5/4
3557526[6]3327112   3137316[24]8192022                  750  113067890[5]8611856 (11)A> 104 01
== Executing PPA-CTR  8 (once), V(1)=3067890[5]8611855
3557526[6]3327136   3137316[24]7653036    -613578[6]7222966  11 (11)A> 103067890[5]8611866 01
== Executing  PA-CTR  1, V(1)=0, V(2)=3067890[5]8611861, repcount=7669725[4]7152966, factor=5/4
4477893[6]9162728   4902057[24]8768560                  762  113834862[5]5764831 (11)A> 102 01
== Executing PPA-CTR  9 (once), V(1)=3834862[5]5764830
4477893[6]9162746   4902057[24]1005942    -766972[6]1528902  01 11 (10)C> 013834862[5]5764835 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=3834862[5]5764830, repcount=9587157[4]8941208, factor=5/4
5532480[6]7516034   7659465[24]9984934                  762  01 114793578[5]4706041 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=4793578[5]4706040
5532480[6]7516061   7659465[24]3518018    -958715[6]9411324  01 11 (10)C> 014793578[5]4706050 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=4793578[5]4706045, repcount=1198394[5]3676512, factor=5/4
6850714[6]7957693   1196791[25]3103746                  772  01 115991973[5]8382561 (10)C> 012 00 10
== Executing PPA-CTR  3 (once), V(1)=5991973[5]8382560, V(2)=0
6850714[6]7957711   1196791[25]7224848    -119839[7]6764354  11 (11)A> 105991973[5]8382569 01
== Executing  PA-CTR  1, V(1)=0, V(2)=5991973[5]8382564, repcount=1497993[5]9595642, factor=5/4
8648306[6]3105415   1869986[25]5241596                  782  117489966[5]7978211 (11)A> 10 01
== Executing PPA-CTR 16 (once), V(1)=7489966[5]7978206
8648306[6]3105422   1869986[25]7154464    -149799[7]5955640  01 11 (10)C> 017489966[5]7978211 00 11
== Executing  PA-CTR  2, V(1)=0, V(2)=7489966[5]7978206, repcount=1872491[5]9494552, factor=5/4
1070804[7]7545494   2921854[25]0390352                  776  01 119362458[5]7472761 (10)C> 013 00 11
== Executing PPA-CTR 19 (once), V(1)=9362458[5]7472760
1070804[7]7545509   2921854[25]9954620    -187249[7]4944750  11 (11)A> 109362458[5]7472768
== Executing  PA-CTR 13, V(1)=0, V(2)=9362458[5]7472763, repcount=2340614[5]1868191, factor=5/4
1351678[7]9963801   4565397[25]1847544                  778  111170307[6]9340956 (11)A> 104
== Executing PPA-CTR 20 (once), V(1)=1170307[6]9340955
1351678[7]9963820   4565397[25]1302938    -234061[7]8681136  01 11 (10)C> 011170307[6]9340961 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=1170307[6]9340956, repcount=2925768[5]4835240, factor=5/4
1673512[7]3151460   7133432[25]1429098                  784  01 111462884[6]4176201 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=1462884[6]4176200
1673512[7]3151475   7133432[25]8248398    -292576[7]8351622  11 (11)A> 101462884[6]4176206 01
== Executing  PA-CTR  1, V(1)=0, V(2)=1462884[6]4176201, repcount=3657210[5]3544051, factor=5/4
2112378[7]5680087   1114598[26]3464162                  786  111828605[6]7720256 (11)A> 102 01
== Executing PPA-CTR  9 (once), V(1)=1828605[6]7720255
2112378[7]5680105   1114598[26]6988344    -365721[7]5439728  01 11 (10)C> 011828605[6]7720260 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=1828605[6]7720255, repcount=4571512[5]4430064, factor=5/4
2615244[7]4410809   1741560[26]8933400                  784  01 112285756[6]2150321 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=2285756[6]2150320
2615244[7]4410824   1741560[26]3338630    -457151[7]4299862  11 (11)A> 102285756[6]2150327 01 10
== Executing  PA-CTR  5, V(1)=0, V(2)=2285756[6]2150322, repcount=5714390[5]0537581, factor=5/4
3300971[7]0861796   2721188[26]1563214                  786  112857195[6]2687906 (11)A> 103 01 10
== Executing PPA-CTR 18 (once), V(1)=2857195[6]2687905, V(2)=0
3300971[7]0861816   2721188[26]4569820    -571439[7]5375028  01 11 (10)C> 012857195[6]2687912 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=2857195[6]2687907, repcount=7142988[5]3171977, factor=5/4
4086700[7]5753563   4251857[26]5072908                  788  01 113571494[6]5859886 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=3571494[6]5859885
4086700[7]5753578   4251857[26]8831178    -714298[7]1718988  11 (11)A> 103571494[6]5859892 01 10
== Executing  PA-CTR  5, V(1)=0, V(2)=3571494[6]5859887, repcount=8928735[5]8964972, factor=5/4
5158148[7]3333242   6643527[26]2463746                  788  114464367[6]4824861 (11)A> 104 01 10
5158148[7]3333243   6643527[26]2463748                  790  114464367[6]4824862 (01)D> 103 01 10
5158148[7]3333244   6643527[26]2463751                  787  114464367[6]4824862 <E(10) 00 102 01 10
5158148[7]3333245   6643527[26]1763199    -892873[7]9648937  <E(10) 104464367[6]4824862 00 102 01 10
5158148[7]3333246   6643527[26]1763202    -892873[7]9648934  01 (11)F> 104464367[6]4824862 00 102 01 10
5158148[7]3333247   6643527[26]1412926                  790  01 114464367[6]4824862 (11)F> 00 102 01 10
5158148[7]3333248   6643527[26]1412928                  792  01 114464367[6]4824863 (11)B> 102 01 10
5158148[7]3333249   6643527[26]1412932                  794  01 114464367[6]4824864 (11)E> 10 01 10
5158148[7]3333250   6643527[26]1412937                  791  01 114464367[6]4824864 <B(11) 00 01 10
5158148[7]3333251   6643527[26]0712393    -892873[7]9648937  01 <B(11) 014464367[6]4824864 00 01 10
5158148[7]3333252   6643527[26]0712400    -892873[7]9648934  11 (11)E> 014464367[6]4824864 00 01 10
5158148[7]3333253   6643527[26]0362128                  794  114464367[6]4824865 (11)E> 00 01 10
5158148[7]3333254   6643527[26]0362130                  796  114464367[6]4824866 (11)A> 01 10
5158148[7]3333255   6643527[26]0362132                  798  114464367[6]4824867 (10)D> 10
5158148[7]3333256   6643527[26]0362135                  795  114464367[6]4824867 <B(11)
5158148[7]3333257   6643527[26]9661603    -892873[7]9648939  <B(11) 014464367[6]4824867
5158148[7]3333258   6643527[26]9661611    -892873[7]9648941  <E(10) 014464367[6]4824868
5158148[7]3333259   6643527[26]9661614    -892873[7]9648938  01 (11)F> 014464367[6]4824868
5158148[7]3333260   6643527[26]9661616    -892873[7]9648936  01 11 (10)C> 014464367[6]4824867
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  111+V(1) (11)A> 104 01 10
    1                    2                    2  112+V(1) (01)D> 103 01 10
    2                    5                   -1  112+V(1) <E(10) 00 102 01 10
    3            13+4*V(1)           -5+-2*V(1)  <E(10) 102+V(1) 00 102 01 10
    4            16+4*V(1)           -2+-2*V(1)  01 (11)F> 102+V(1) 00 102 01 10
    5            20+6*V(1)                    2  01 112+V(1) (11)F> 00 102 01 10
    6            22+6*V(1)                    4  01 113+V(1) (11)B> 102 01 10
    7            26+6*V(1)                    6  01 114+V(1) (11)E> 10 01 10
    8            31+6*V(1)                    3  01 114+V(1) <B(11) 00 01 10
    9           47+10*V(1)           -5+-2*V(1)  01 <B(11) 014+V(1) 00 01 10
   10           54+10*V(1)           -2+-2*V(1)  11 (11)E> 014+V(1) 00 01 10
   11           62+12*V(1)                    6  115+V(1) (11)E> 00 01 10
   12           64+12*V(1)                    8  116+V(1) (11)A> 01 10
   13           66+12*V(1)                   10  117+V(1) (10)D> 10
   14           69+12*V(1)                    7  117+V(1) <B(11)
   15           97+16*V(1)           -7+-2*V(1)  <B(11) 017+V(1)
   16          105+16*V(1)           -9+-2*V(1)  <E(10) 018+V(1)
   17          108+16*V(1)           -6+-2*V(1)  01 (11)F> 018+V(1)
   18          110+16*V(1)           -4+-2*V(1)  01 11 (10)C> 017+V(1)
<< Success! ==> defined new CTR 30 (PPA)
5158148[7]3333260   6643527[26]9661616    -892873[7]9648936  01 11 (10)C> 014464367[6]4824867
== Executing  PA-CTR 21, V(1)=0, V(2)=4464367[6]4824862, repcount=1116091[6]6206216, factor=5/4
6385849[7]1601636   1038051[27]1832640                  792  01 115580459[6]1031081 (10)C> 013
6385849[7]1601637   1038051[27]1832645                  789  01 115580459[6]1031081 <B(11) 00 012
6385849[7]1601638   1038051[27]5956969    -111609[8]2061373  01 <B(11) 015580459[6]1031081 00 012
6385849[7]1601639   1038051[27]5956976    -111609[8]2061370  11 (11)E> 015580459[6]1031081 00 012
6385849[7]1601640   1038051[27]8019138                  792  115580459[6]1031082 (11)E> 00 012
6385849[7]1601641   1038051[27]8019140                  794  115580459[6]1031083 (11)A> 012
6385849[7]1601642   1038051[27]8019142                  796  115580459[6]1031084 (10)D> 01
6385849[7]1601643   1038051[27]8019153                  793  115580459[6]1031084 <E(10) 10
6385849[7]1601644   1038051[27]2143489    -111609[8]2061375  <E(10) 105580459[6]1031085
6385849[7]1601645   1038051[27]2143492    -111609[8]2061372  01 (11)F> 105580459[6]1031085
6385849[7]1601646   1038051[27]4205662                  798  01 115580459[6]1031085 (11)F>
6385849[7]1601647   1038051[27]4205664                  800  01 115580459[6]1031086 (11)B>
6385849[7]1601648   1038051[27]4205675                  797  01 115580459[6]1031086 <E(10) 01
6385849[7]1601649   1038051[27]8330019    -111609[8]2061375  01 <E(10) 105580459[6]1031086 01
6385849[7]1601650   1038051[27]8330021    -111609[8]2061377  <A(01) 105580459[6]1031087 01
6385849[7]1601651   1038051[27]8330032    -111609[8]2061374  11 (11)A> 105580459[6]1031087 01
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 111+V(1) (10)C> 013
    1                    5                   -3  01 111+V(1) <B(11) 00 012
    2             9+4*V(1)           -5+-2*V(1)  01 <B(11) 011+V(1) 00 012
    3            16+4*V(1)           -2+-2*V(1)  11 (11)E> 011+V(1) 00 012
    4            18+6*V(1)                    0  112+V(1) (11)E> 00 012
    5            20+6*V(1)                    2  113+V(1) (11)A> 012
    6            22+6*V(1)                    4  114+V(1) (10)D> 01
    7            33+6*V(1)                    1  114+V(1) <E(10) 10
    8           49+10*V(1)           -7+-2*V(1)  <E(10) 105+V(1)
    9           52+10*V(1)           -4+-2*V(1)  01 (11)F> 105+V(1)
   10           62+12*V(1)                    6  01 115+V(1) (11)F>
   11           64+12*V(1)                    8  01 116+V(1) (11)B>
   12           75+12*V(1)                    5  01 116+V(1) <E(10) 01
   13           99+16*V(1)           -7+-2*V(1)  01 <E(10) 106+V(1) 01
   14          101+16*V(1)           -9+-2*V(1)  <A(01) 107+V(1) 01
   15          112+16*V(1)           -6+-2*V(1)  11 (11)A> 107+V(1) 01
<< Success! ==> defined new CTR 31 (PPA)
6385849[7]1601651   1038051[27]8330032    -111609[8]2061374  11 (11)A> 105580459[6]1031087 01
== Executing  PA-CTR  1, V(1)=0, V(2)=5580459[6]1031082, repcount=1395114[6]7757771, factor=5/4
8059987[7]4694903   1621954[27]8747476                  794  116975574[6]8788856 (11)A> 103 01
== Executing PPA-CTR  4 (once), V(1)=6975574[6]8788855, V(2)=0
8059987[7]4694926   1621954[27]9369300    -139511[8]7576920  01 11 (10)C> 016975574[6]8788863 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=6975574[6]8788858, repcount=1743893[6]7197215, factor=5/4
9978270[7]3864291   2534304[27]6761360                  800  01 118719468[6]5986076 (10)C> 013 00 10
== Executing PPA-CTR 10 (once), V(1)=8719468[6]5986075
9978270[7]3864318   2534304[27]8455214    -174389[8]1971356  01 11 (10)C> 018719468[6]5986085 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=8719468[6]5986080, repcount=2179867[6]3996521, factor=5/4
1237612[8]7826049   3959850[27]7440158                  812  01 111089933[7]9982606 (10)C> 01 00 10
== Executing PPA-CTR 15 (once), V(1)=1089933[7]9982605
1237612[8]7826064   3959850[27]7161938    -217986[8]9964404  11 (11)A> 101089933[7]9982611 01
== Executing  PA-CTR  1, V(1)=0, V(2)=1089933[7]9982606, repcount=2724833[6]2495652, factor=5/4
1564592[8]7773888   6187266[27]9167226                  812  111362416[7]2478261 (11)A> 103 01
== Executing PPA-CTR  4 (once), V(1)=1362416[7]2478260, V(2)=0
1564592[8]7773911   6187266[27]8819530    -272483[8]4955712  01 11 (10)C> 011362416[7]2478268 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=1362416[7]2478263, repcount=3406042[6]5619566, factor=5/4
1939257[8]9589137   9667604[27]0735454                  816  01 111703021[7]8097831 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=1703021[7]8097830
1939257[8]9589152   9667604[27]0300844    -340604[8]6194850  11 (11)A> 101703021[7]8097837 01 10
== Executing  PA-CTR  5, V(1)=0, V(2)=1703021[7]8097832, repcount=4257553[6]2024459, factor=5/4
2450163[8]3882660   1510563[28]6412880                  822  112128776[7]0122296 (11)A> 10 01 10
== Executing PPA-CTR 12 (once), V(1)=2128776[7]0122291
2450163[8]3882667   1510563[28]6902088    -425755[8]0243770  01 11 (10)C> 012128776[7]0122296 00 11 10
== Executing  PA-CTR  6, V(1)=0, V(2)=2128776[7]0122291, repcount=5321941[6]2530573, factor=5/4
3035577[8]1718970   2360254[28]4191440                  814  01 112660970[7]2652866 (10)C> 014 00 11 10
3035577[8]1718971   2360254[28]4191445                  811  01 112660970[7]2652866 <B(11) 00 013 00 11 10
3035577[8]1718972   2360254[28]4802909    -532194[8]5304921  01 <B(11) 012660970[7]2652866 00 013 00 11 10
3035577[8]1718973   2360254[28]4802916    -532194[8]5304918  11 (11)E> 012660970[7]2652866 00 013 00 11 10
3035577[8]1718974   2360254[28]0108648                  814  112660970[7]2652867 (11)E> 00 013 00 11 10
3035577[8]1718975   2360254[28]0108650                  816  112660970[7]2652868 (11)A> 013 00 11 10
3035577[8]1718976   2360254[28]0108652                  818  112660970[7]2652869 (10)D> 012 00 11 10
3035577[8]1718977   2360254[28]0108663                  815  112660970[7]2652869 <E(10) 10 01 00 11 10
3035577[8]1718978   2360254[28]0720139    -532194[8]5304923  <E(10) 102660970[7]2652870 01 00 11 10
3035577[8]1718979   2360254[28]0720142    -532194[8]5304920  01 (11)F> 102660970[7]2652870 01 00 11 10
3035577[8]1718980   2360254[28]6025882                  820  01 112660970[7]2652870 (11)F> 01 00 11 10
3035577[8]1718981   2360254[28]6025884                  822  01 112660970[7]2652871 (10)C> 00 11 10
3035577[8]1718982   2360254[28]6025893                  819  01 112660970[7]2652871 <E(10) 01 11 10
3035577[8]1718983   2360254[28]6637377    -532194[8]5304923  01 <E(10) 102660970[7]2652871 01 11 10
3035577[8]1718984   2360254[28]6637379    -532194[8]5304925  <A(01) 102660970[7]2652872 01 11 10
3035577[8]1718985   2360254[28]6637390    -532194[8]5304922  11 (11)A> 102660970[7]2652872 01 11 10
3035577[8]1718986   2360254[28]6637392    -532194[8]5304920  112 (01)D> 102660970[7]2652871 01 11 10
3035577[8]1718987   2360254[28]6637395    -532194[8]5304923  112 <E(10) 00 102660970[7]2652870 01 11 10
3035577[8]1718988   2360254[28]6637403    -532194[8]5304927  <E(10) 102 00 102660970[7]2652870 01 11 10
3035577[8]1718989   2360254[28]6637406    -532194[8]5304924  01 (11)F> 102 00 102660970[7]2652870 01 11 10
3035577[8]1718990   2360254[28]6637410    -532194[8]5304920  01 112 (11)F> 00 102660970[7]2652870 01 11 10
3035577[8]1718991   2360254[28]6637412    -532194[8]5304918  01 113 (11)B> 102660970[7]2652870 01 11 10
3035577[8]1718992   2360254[28]6637416    -532194[8]5304916  01 114 (11)E> 102660970[7]2652869 01 11 10
3035577[8]1718993   2360254[28]6637421    -532194[8]5304919  01 114 <B(11) 00 102660970[7]2652868 01 11 10
3035577[8]1718994   2360254[28]6637437    -532194[8]5304927  01 <B(11) 014 00 102660970[7]2652868 01 11 10
3035577[8]1718995   2360254[28]6637444    -532194[8]5304924  11 (11)E> 014 00 102660970[7]2652868 01 11 10
3035577[8]1718996   2360254[28]6637452    -532194[8]5304916  115 (11)E> 00 102660970[7]2652868 01 11 10
3035577[8]1718997   2360254[28]6637454    -532194[8]5304914  116 (11)A> 102660970[7]2652868 01 11 10
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  111+V(1) (11)A> 105+V(2) [*]* [*]* [*]*
    1                    2                    2  112+V(1) (01)D> 104+V(2) [*]* [*]* [*]*
    2                    5                   -1  112+V(1) <E(10) 00 103+V(2) [*]* [*]* [*]*
    3            13+4*V(1)           -5+-2*V(1)  <E(10) 102+V(1) 00 103+V(2) [*]* [*]* [*]*
    4            16+4*V(1)           -2+-2*V(1)  01 (11)F> 102+V(1) 00 103+V(2) [*]* [*]* [*]*
    5            20+6*V(1)                    2  01 112+V(1) (11)F> 00 103+V(2) [*]* [*]* [*]*
    6            22+6*V(1)                    4  01 113+V(1) (11)B> 103+V(2) [*]* [*]* [*]*
    7            26+6*V(1)                    6  01 114+V(1) (11)E> 102+V(2) [*]* [*]* [*]*
    8            31+6*V(1)                    3  01 114+V(1) <B(11) 00 101+V(2) [*]* [*]* [*]*
    9           47+10*V(1)           -5+-2*V(1)  01 <B(11) 014+V(1) 00 101+V(2) [*]* [*]* [*]*
   10           54+10*V(1)           -2+-2*V(1)  11 (11)E> 014+V(1) 00 101+V(2) [*]* [*]* [*]*
   11           62+12*V(1)                    6  115+V(1) (11)E> 00 101+V(2) [*]* [*]* [*]*
   12           64+12*V(1)                    8  116+V(1) (11)A> 101+V(2) [*]* [*]* [*]*
<< Success! ==> defined new CTR 32 (PA)
3035577[8]1718997   2360254[28]6637454    -532194[8]5304914  116 (11)A> 102660970[7]2652868 01 11 10
== Executing  PA-CTR 32, V(1)=5, V(2)=2660970[7]2652863, repcount=6652426[6]3163216, factor=5/4
3833868[8]9677589   3687898[28]7859438                  814  113326213[7]5816086 (11)A> 104 01 11 10
3833868[8]9677590   3687898[28]7859440                  816  113326213[7]5816087 (01)D> 103 01 11 10
3833868[8]9677591   3687898[28]7859443                  813  113326213[7]5816087 <E(10) 00 102 01 11 10
3833868[8]9677592   3687898[28]1123791    -665242[8]1631361  <E(10) 103326213[7]5816087 00 102 01 11 10
3833868[8]9677593   3687898[28]1123794    -665242[8]1631358  01 (11)F> 103326213[7]5816087 00 102 01 11 10
3833868[8]9677594   3687898[28]2755968                  816  01 113326213[7]5816087 (11)F> 00 102 01 11 10
3833868[8]9677595   3687898[28]2755970                  818  01 113326213[7]5816088 (11)B> 102 01 11 10
3833868[8]9677596   3687898[28]2755974                  820  01 113326213[7]5816089 (11)E> 10 01 11 10
3833868[8]9677597   3687898[28]2755979                  817  01 113326213[7]5816089 <B(11) 00 01 11 10
3833868[8]9677598   3687898[28]6020335    -665242[8]1631361  01 <B(11) 013326213[7]5816089 00 01 11 10
3833868[8]9677599   3687898[28]6020342    -665242[8]1631358  11 (11)E> 013326213[7]5816089 00 01 11 10
3833868[8]9677600   3687898[28]7652520                  820  113326213[7]5816090 (11)E> 00 01 11 10
3833868[8]9677601   3687898[28]7652522                  822  113326213[7]5816091 (11)A> 01 11 10
3833868[8]9677602   3687898[28]7652524                  824  113326213[7]5816092 (10)D> 11 10
3833868[8]9677603   3687898[28]7652527                  821  113326213[7]5816092 <B(11) 01 10
3833868[8]9677604   3687898[28]0916895    -665242[8]1631363  <B(11) 013326213[7]5816093 10
3833868[8]9677605   3687898[28]0916903    -665242[8]1631365  <E(10) 013326213[7]5816094 10
3833868[8]9677606   3687898[28]0916906    -665242[8]1631362  01 (11)F> 013326213[7]5816094 10
3833868[8]9677607   3687898[28]0916908    -665242[8]1631360  01 11 (10)C> 013326213[7]5816093 10
3833868[8]9677608   3687898[28]0916913    -665242[8]1631363  01 11 <B(11) 00 013326213[7]5816092 10
3833868[8]9677609   3687898[28]0916917    -665242[8]1631365  01 <B(11) 01 00 013326213[7]5816092 10
3833868[8]9677610   3687898[28]0916924    -665242[8]1631362  11 (11)E> 01 00 013326213[7]5816092 10
3833868[8]9677611   3687898[28]0916926    -665242[8]1631360  112 (11)E> 00 013326213[7]5816092 10
3833868[8]9677612   3687898[28]0916928    -665242[8]1631358  113 (11)A> 013326213[7]5816092 10
3833868[8]9677613   3687898[28]0916930    -665242[8]1631356  114 (10)D> 013326213[7]5816091 10
3833868[8]9677614   3687898[28]0916941    -665242[8]1631359  114 <E(10) 10 013326213[7]5816090 10
3833868[8]9677615   3687898[28]0916957    -665242[8]1631367  <E(10) 105 013326213[7]5816090 10
3833868[8]9677616   3687898[28]0916960    -665242[8]1631364  01 (11)F> 105 013326213[7]5816090 10
3833868[8]9677617   3687898[28]0916970    -665242[8]1631354  01 115 (11)F> 013326213[7]5816090 10
3833868[8]9677618   3687898[28]0916972    -665242[8]1631352  01 116 (10)C> 013326213[7]5816089 10
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  01 111+V(1) (10)C> 015+V(2) [*]*
    1                    5                   -3  01 111+V(1) <B(11) 00 014+V(2) [*]*
    2             9+4*V(1)           -5+-2*V(1)  01 <B(11) 011+V(1) 00 014+V(2) [*]*
    3            16+4*V(1)           -2+-2*V(1)  11 (11)E> 011+V(1) 00 014+V(2) [*]*
    4            18+6*V(1)                    0  112+V(1) (11)E> 00 014+V(2) [*]*
    5            20+6*V(1)                    2  113+V(1) (11)A> 014+V(2) [*]*
    6            22+6*V(1)                    4  114+V(1) (10)D> 013+V(2) [*]*
    7            33+6*V(1)                    1  114+V(1) <E(10) 10 012+V(2) [*]*
    8           49+10*V(1)           -7+-2*V(1)  <E(10) 105+V(1) 012+V(2) [*]*
    9           52+10*V(1)           -4+-2*V(1)  01 (11)F> 105+V(1) 012+V(2) [*]*
   10           62+12*V(1)                    6  01 115+V(1) (11)F> 012+V(2) [*]*
   11           64+12*V(1)                    8  01 116+V(1) (10)C> 011+V(2) [*]*
<< Success! ==> defined new CTR 33 (PA)
3833868[8]9677618   3687898[28]0916972    -665242[8]1631352  01 116 (10)C> 013326213[7]5816089 10
== Executing  PA-CTR 33, V(1)=5, V(2)=3326213[7]5816084, repcount=8315533[6]3954022, factor=5/4
4748576[8]3171860   5762341[28]1889560                  824  01 114157766[7]9770116 (10)C> 01 10
4748576[8]3171861   5762341[28]1889565                  821  01 114157766[7]9770116 <B(11) 00 10
4748576[8]3171862   5762341[28]0970029    -831553[8]9539411  01 <B(11) 014157766[7]9770116 00 10
4748576[8]3171863   5762341[28]0970036    -831553[8]9539408  11 (11)E> 014157766[7]9770116 00 10
4748576[8]3171864   5762341[28]0510268                  824  114157766[7]9770117 (11)E> 00 10
4748576[8]3171865   5762341[28]0510270                  826  114157766[7]9770118 (11)A> 10
4748576[8]3171866   5762341[28]0510272                  828  114157766[7]9770119 (01)D>
4748576[8]3171867   5762341[28]0510275                  825  114157766[7]9770119 <A(01) 10
4748576[8]3171868   5762341[28]0510281                  823  114157766[7]9770118 <B(11) 00 10
4748576[8]3171869   5762341[28]9590753    -831553[8]9539413  <B(11) 014157766[7]9770118 00 10
4748576[8]3171870   5762341[28]9590761    -831553[8]9539415  <E(10) 014157766[7]9770119 00 10
4748576[8]3171871   5762341[28]9590764    -831553[8]9539412  01 (11)F> 014157766[7]9770119 00 10
4748576[8]3171872   5762341[28]9590766    -831553[8]9539410  01 11 (10)C> 014157766[7]9770118 00 10
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 113+V(1) (10)C> 01 10
    1                    5                   -3  01 113+V(1) <B(11) 00 10
    2            17+4*V(1)           -9+-2*V(1)  01 <B(11) 013+V(1) 00 10
    3            24+4*V(1)           -6+-2*V(1)  11 (11)E> 013+V(1) 00 10
    4            30+6*V(1)                    0  114+V(1) (11)E> 00 10
    5            32+6*V(1)                    2  115+V(1) (11)A> 10
    6            34+6*V(1)                    4  116+V(1) (01)D>
    7            37+6*V(1)                    1  116+V(1) <A(01) 10
    8            43+6*V(1)                   -1  115+V(1) <B(11) 00 10
    9           63+10*V(1)          -11+-2*V(1)  <B(11) 015+V(1) 00 10
   10           71+10*V(1)          -13+-2*V(1)  <E(10) 016+V(1) 00 10
   11           74+10*V(1)          -10+-2*V(1)  01 (11)F> 016+V(1) 00 10
   12           76+10*V(1)           -8+-2*V(1)  01 11 (10)C> 015+V(1) 00 10
<< Success! ==> defined new CTR 34 (PPA)
4748576[8]3171872   5762341[28]9590766    -831553[8]9539410  01 11 (10)C> 014157766[7]9770118 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=4157766[7]9770113, repcount=1039441[7]7442529, factor=5/4
5891962[8]5039691   9003658[28]0111982                  822  01 115197208[7]7212646 (10)C> 012 00 10
== Executing PPA-CTR  3 (once), V(1)=5197208[7]7212645, V(2)=0
5891962[8]5039709   9003658[28]5514444    -103944[9]4424474  11 (11)A> 105197208[7]7212654 01
== Executing  PA-CTR  1, V(1)=0, V(2)=5197208[7]7212649, repcount=1299302[7]1803163, factor=5/4
7451125[8]6677665   1406821[29]0959056                  830  116496510[7]9015816 (11)A> 102 01
== Executing PPA-CTR  9 (once), V(1)=6496510[7]9015815
7451125[8]6677683   1406821[29]5212198    -129930[9]8030804  01 11 (10)C> 016496510[7]9015820 00 10
== Executing  PA-CTR  2, V(1)=0, V(2)=6496510[7]9015815, repcount=1624127[7]7253954, factor=5/4
9237665[8]6471177   2198158[29]0870114                  828  01 118120637[7]6269771 (10)C> 014 00 10
== Executing PPA-CTR 11 (once), V(1)=8120637[7]6269770
9237665[8]6471192   2198158[29]1186544    -162412[9]2538718  11 (11)A> 108120637[7]6269777 01 10
== Executing  PA-CTR  5, V(1)=0, V(2)=8120637[7]6269772, repcount=2030159[7]4067444, factor=5/4
1167385[9]5280520   3434622[29]0273720                  834  111015079[8]0337221 (11)A> 10 01 10
== Executing PPA-CTR 12 (once), V(1)=1015079[8]0337216
1167385[9]5280527   3434622[29]1622628    -203015[9]0673608  01 11 (10)C> 011015079[8]0337221 00 11 10
== Executing  PA-CTR  6, V(1)=0, V(2)=1015079[8]0337216, repcount=2537699[7]7584305, factor=5/4
1446532[9]8707882   5366598[29]9479748                  832  01 111268849[8]7921526 (10)C> 01 00 11 10
1446532[9]8707883   5366598[29]9479753                  829  01 111268849[8]7921526 <B(11) 002 11 10
1446532[9]8707884   5366598[29]1165857    -253769[9]5842223  01 <B(11) 011268849[8]7921526 002 11 10
1446532[9]8707885   5366598[29]1165864    -253769[9]5842220  11 (11)E> 011268849[8]7921526 002 11 10
1446532[9]8707886   5366598[29]7008916                  832  111268849[8]7921527 (11)E> 002 11 10
1446532[9]8707887   5366598[29]7008918                  834  111268849[8]7921528 (11)A> 00 11 10
1446532[9]8707888   5366598[29]7008922                  836  111268849[8]7921529 (01)D> 11 10
1446532[9]8707889   5366598[29]7008925                  833  111268849[8]7921529 <E(10) 01 10
1446532[9]8707890   5366598[29]8695041    -253769[9]5842225  <E(10) 101268849[8]7921529 01 10
1446532[9]8707891   5366598[29]8695044    -253769[9]5842222  01 (11)F> 101268849[8]7921529 01 10
1446532[9]8707892   5366598[29]4538102                  836  01 111268849[8]7921529 (11)F> 01 10
1446532[9]8707893   5366598[29]4538104                  838  01 111268849[8]7921530 (10)C> 10
1446532[9]8707894   5366598[29]4538105                  839  01 111268849[8]7921530 101 H> 0   [stop]

Lines:       1031
Top steps:   1030
Macro steps: 14465326327716818707894
Basic steps: 5366598383321904238506234609927865294538105
Tape index:  839
ones:        2537699363594175843063
log10(ones    ):   21.404
log10(steps   ):   42.730
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-macro machine.

To the BB simulations page of Heiner Marxen.
To the busy beaver page of Heiner Marxen.
To the home page of Heiner Marxen.
Input to awk program:
    gohalt 1
    5T B1R C0R A0L D0R D1R H1R E1L D0L F1R B1L A1R E1R : 2,537,699,363,594,175,843,063 >5.3*10^42
    T 6-state TM #3 from MaBu-List
    M	1050
    pref	sim
    machv mbL6_3  	just simple
    machv mbL6_3-r	with repetitions reduced
    machv mbL6_3-1	with tape symbol exponents
    machv mbL6_3-m	as 2-bck-macro machine
    machv mbL6_3-a	as 2-bck-macro machine with pure additive config-TRs
    iam	mbL6_3-a
    mtype	2 0
    mmtyp	3
    r	1
    H	1
    mac	0
    E	2
    sympr	
    HM	1
    date	Tue Jul  6 22:10:32 CEST 2010
    edate	Tue Jul  6 22:10:36 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:32 CEST 2010
Ready: Tue Jul 6 22:10:36 CEST 2010