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

Comment: This TM produces >1.4x10^2355 nonzeros in >3.4x10^4710 steps.

State on
0
on
1
on
2
on
3
on 0 on 1 on 2 on 3
Print Move Goto Print Move Goto Print Move Goto Print Move Goto
A 1RB 2LB 2RA 1LA 1 right B 2 left B 2 right A 1 left A
B 2LA 1RC 0LB 2RA 2 left A 1 right C 0 left B 2 right A
C 1RB 3LC 1LA 1RH 1 right B 3 left C 1 left A 1 right H
Transition table
The same TM just simple.
The same TM with repetitions reduced.
The same TM with tape symbol exponents.
The same TM as 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                   14                    2  11 (11)B>
    2                   19                   -1  11 <B(21) 20
    3                   25                   -3  <B(21) 11 20
    4                   34                    0  11 (11)C> 11 20
    5                   37                   -3  11 <C(33) 31 20
    6                   39                   -5  <C(33) 33 31 20
    7                   50                   -2  01 (11)B> 33 31 20
    8                   60                    0  01 11 (11)B> 31 20
    9                   68                    2  01 112 (11)B> 20
   10                   79                   -1  01 112 <B(21) 12
   11                   91                   -5  01 <B(21) 112 12
   12                   95                   -7  <A(22) 113 12
   13                  102                   -4  01 (11)B> 113 12
   14                  107                   -7  01 <C(33) 33 112 12
   15                  120                   -4  11 (12)A> 33 112 12
   16                  130                   -2  112 (12)A> 112 12
   17                  138                    0  113 (11)C> 11 12
   18                  141                   -3  113 <C(33) 31 12
   19                  147                   -9  <C(33) 333 31 12
   20                  158                   -6  01 (11)B> 333 31 12
   21                  188                    0  01 113 (11)B> 31 12
   22                  196                    2  01 114 (11)B> 12
   23                  205                   -1  01 114 <B(21) 11
   24                  229                   -9  01 <B(21) 115
   25                  233                  -11  <A(22) 116
   26                  240                   -8  01 (11)B> 116
   27                  245                  -11  01 <C(33) 33 115
   28                  258                   -8  11 (12)A> 33 115
   29                  268                   -6  112 (12)A> 115
   30                  276                   -4  113 (11)C> 114
   31                  279                   -7  113 <C(33) 31 113
   32                  285                  -13  <C(33) 333 31 113
   33                  296                  -10  01 (11)B> 333 31 113
   34                  326                   -4  01 113 (11)B> 31 113
   35                  334                   -2  01 114 (11)B> 113
   36                  339                   -5  01 114 <C(33) 33 112
   37                  347                  -13  01 <C(33) 335 112
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  01 <C(33) 331+V(2) 114+V(1)
    1                   13                    3  11 (12)A> 331+V(2) 114+V(1)
    2           23+10*V(2)             5+2*V(2)  112+V(2) (12)A> 114+V(1)
    3           31+10*V(2)             7+2*V(2)  113+V(2) (11)C> 113+V(1)
    4           34+10*V(2)             4+2*V(2)  113+V(2) <C(33) 31 112+V(1)
    5           40+12*V(2)                   -2  <C(33) 333+V(2) 31 112+V(1)
    6           51+12*V(2)                    1  01 (11)B> 333+V(2) 31 112+V(1)
    7           81+22*V(2)             7+2*V(2)  01 113+V(2) (11)B> 31 112+V(1)
    8           89+22*V(2)             9+2*V(2)  01 114+V(2) (11)B> 112+V(1)
    9           94+22*V(2)             6+2*V(2)  01 114+V(2) <C(33) 33 111+V(1)
   10          102+24*V(2)                   -2  01 <C(33) 335+V(2) 111+V(1)
<< Success! ==> defined new CTR 1 (PA)
   38                  360                  -10  11 (12)A> 335 112
   39                  410                    0  116 (12)A> 112
   40                  418                    2  117 (11)C> 11
   41                  421                   -1  117 <C(33) 31
   42                  435                  -15  <C(33) 337 31
   43                  446                  -12  01 (11)B> 337 31
   44                  516                    2  01 117 (11)B> 31
   45                  524                    4  01 118 (11)B>
   46                  529                    1  01 118 <B(21) 20
   47                  577                  -15  01 <B(21) 118 20
   48                  581                  -17  <A(22) 119 20
   49                  588                  -14  01 (11)B> 119 20
   50                  593                  -17  01 <C(33) 33 118 20
   51                  606                  -14  11 (12)A> 33 118 20
   52                  616                  -12  112 (12)A> 118 20
   53                  624                  -10  113 (11)C> 117 20
   54                  627                  -13  113 <C(33) 31 116 20
   55                  633                  -19  <C(33) 333 31 116 20
   56                  644                  -16  01 (11)B> 333 31 116 20
   57                  674                  -10  01 113 (11)B> 31 116 20
   58                  682                   -8  01 114 (11)B> 116 20
   59                  687                  -11  01 114 <C(33) 33 115 20
   60                  695                  -19  01 <C(33) 335 115 20
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  01 <C(33) 331+V(2) 114+V(1) [*]*
    1                   13                    3  11 (12)A> 331+V(2) 114+V(1) [*]*
    2           23+10*V(2)             5+2*V(2)  112+V(2) (12)A> 114+V(1) [*]*
    3           31+10*V(2)             7+2*V(2)  113+V(2) (11)C> 113+V(1) [*]*
    4           34+10*V(2)             4+2*V(2)  113+V(2) <C(33) 31 112+V(1) [*]*
    5           40+12*V(2)                   -2  <C(33) 333+V(2) 31 112+V(1) [*]*
    6           51+12*V(2)                    1  01 (11)B> 333+V(2) 31 112+V(1) [*]*
    7           81+22*V(2)             7+2*V(2)  01 113+V(2) (11)B> 31 112+V(1) [*]*
    8           89+22*V(2)             9+2*V(2)  01 114+V(2) (11)B> 112+V(1) [*]*
    9           94+22*V(2)             6+2*V(2)  01 114+V(2) <C(33) 33 111+V(1) [*]*
   10          102+24*V(2)                   -2  01 <C(33) 335+V(2) 111+V(1) [*]*
<< Success! ==> defined new CTR 2 (PA)
   60                  695                  -19  01 <C(33) 335 115 20
== Executing  PA-CTR  2, V(1)=1, V(2)=4, repcount=1, factor=4/3
   70                  893                  -21  01 <C(33) 339 112 20
   71                  906                  -18  11 (12)A> 339 112 20
   72                  996                    0  1110 (12)A> 112 20
   73                 1004                    2  1111 (11)C> 11 20
   74                 1007                   -1  1111 <C(33) 31 20
   75                 1029                  -23  <C(33) 3311 31 20
   76                 1040                  -20  01 (11)B> 3311 31 20
   77                 1150                    2  01 1111 (11)B> 31 20
   78                 1158                    4  01 1112 (11)B> 20
   79                 1169                    1  01 1112 <B(21) 12
   80                 1241                  -23  01 <B(21) 1112 12
   81                 1245                  -25  <A(22) 1113 12
   82                 1252                  -22  01 (11)B> 1113 12
   83                 1257                  -25  01 <C(33) 33 1112 12
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 <C(33) 331+V(1) 112 20
    1                   13                    3  11 (12)A> 331+V(1) 112 20
    2           23+10*V(1)             5+2*V(1)  112+V(1) (12)A> 112 20
    3           31+10*V(1)             7+2*V(1)  113+V(1) (11)C> 11 20
    4           34+10*V(1)             4+2*V(1)  113+V(1) <C(33) 31 20
    5           40+12*V(1)                   -2  <C(33) 333+V(1) 31 20
    6           51+12*V(1)                    1  01 (11)B> 333+V(1) 31 20
    7           81+22*V(1)             7+2*V(1)  01 113+V(1) (11)B> 31 20
    8           89+22*V(1)             9+2*V(1)  01 114+V(1) (11)B> 20
    9          100+22*V(1)             6+2*V(1)  01 114+V(1) <B(21) 12
   10          124+28*V(1)                   -2  01 <B(21) 114+V(1) 12
   11          128+28*V(1)                   -4  <A(22) 115+V(1) 12
   12          135+28*V(1)                   -1  01 (11)B> 115+V(1) 12
   13          140+28*V(1)                   -4  01 <C(33) 33 114+V(1) 12
<< Success! ==> defined new CTR 3 (PPA)
   83                 1257                  -25  01 <C(33) 33 1112 12
== Executing  PA-CTR  2, V(1)=8, V(2)=0, repcount=3, factor=4/3
  113                 1851                  -31  01 <C(33) 3313 113 12
  114                 1864                  -28  11 (12)A> 3313 113 12
  115                 1994                   -2  1114 (12)A> 113 12
  116                 2002                    0  1115 (11)C> 112 12
  117                 2005                   -3  1115 <C(33) 31 11 12
  118                 2035                  -33  <C(33) 3315 31 11 12
  119                 2046                  -30  01 (11)B> 3315 31 11 12
  120                 2196                    0  01 1115 (11)B> 31 11 12
  121                 2204                    2  01 1116 (11)B> 11 12
  122                 2209                   -1  01 1116 <C(33) 33 12
  123                 2241                  -33  01 <C(33) 3317 12
  124                 2254                  -30  11 (12)A> 3317 12
  125                 2424                    4  1118 (12)A> 12
  126                 2434                    6  1119 (11)B>
  127                 2439                    3  1119 <B(21) 20
  128                 2553                  -35  <B(21) 1119 20
  129                 2562                  -32  11 (11)C> 1119 20
  130                 2565                  -35  11 <C(33) 31 1118 20
  131                 2567                  -37  <C(33) 33 31 1118 20
  132                 2578                  -34  01 (11)B> 33 31 1118 20
  133                 2588                  -32  01 11 (11)B> 31 1118 20
  134                 2596                  -30  01 112 (11)B> 1118 20
  135                 2601                  -33  01 112 <C(33) 33 1117 20
  136                 2605                  -37  01 <C(33) 333 1117 20
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 <C(33) 331+V(1) 113 12
    1                   13                    3  11 (12)A> 331+V(1) 113 12
    2           23+10*V(1)             5+2*V(1)  112+V(1) (12)A> 113 12
    3           31+10*V(1)             7+2*V(1)  113+V(1) (11)C> 112 12
    4           34+10*V(1)             4+2*V(1)  113+V(1) <C(33) 31 11 12
    5           40+12*V(1)                   -2  <C(33) 333+V(1) 31 11 12
    6           51+12*V(1)                    1  01 (11)B> 333+V(1) 31 11 12
    7           81+22*V(1)             7+2*V(1)  01 113+V(1) (11)B> 31 11 12
    8           89+22*V(1)             9+2*V(1)  01 114+V(1) (11)B> 11 12
    9           94+22*V(1)             6+2*V(1)  01 114+V(1) <C(33) 33 12
   10          102+24*V(1)                   -2  01 <C(33) 335+V(1) 12
   11          115+24*V(1)                    1  11 (12)A> 335+V(1) 12
   12          165+34*V(1)            11+2*V(1)  116+V(1) (12)A> 12
   13          175+34*V(1)            13+2*V(1)  117+V(1) (11)B>
   14          180+34*V(1)            10+2*V(1)  117+V(1) <B(21) 20
   15          222+40*V(1)                   -4  <B(21) 117+V(1) 20
   16          231+40*V(1)                   -1  11 (11)C> 117+V(1) 20
   17          234+40*V(1)                   -4  11 <C(33) 31 116+V(1) 20
   18          236+40*V(1)                   -6  <C(33) 33 31 116+V(1) 20
   19          247+40*V(1)                   -3  01 (11)B> 33 31 116+V(1) 20
   20          257+40*V(1)                   -1  01 11 (11)B> 31 116+V(1) 20
   21          265+40*V(1)                    1  01 112 (11)B> 116+V(1) 20
   22          270+40*V(1)                   -2  01 112 <C(33) 33 115+V(1) 20
   23          274+40*V(1)                   -6  01 <C(33) 333 115+V(1) 20
<< Success! ==> defined new CTR 4 (PPA)
  136                 2605                  -37  01 <C(33) 333 1117 20
== Executing  PA-CTR  2, V(1)=13, V(2)=2, repcount=5, factor=4/3
  186                 4315                  -47  01 <C(33) 3323 112 20
== Executing PPA-CTR  3 (once), V(1)=22
  199                 5071                  -51  01 <C(33) 33 1126 12
== Executing  PA-CTR  2, V(1)=22, V(2)=0, repcount=8, factor=4/3
  279                 8575                  -67  01 <C(33) 3333 112 12
  280                 8588                  -64  11 (12)A> 3333 112 12
  281                 8918                    2  1134 (12)A> 112 12
  282                 8926                    4  1135 (11)C> 11 12
  283                 8929                    1  1135 <C(33) 31 12
  284                 8999                  -69  <C(33) 3335 31 12
  285                 9010                  -66  01 (11)B> 3335 31 12
  286                 9360                    4  01 1135 (11)B> 31 12
  287                 9368                    6  01 1136 (11)B> 12
  288                 9377                    3  01 1136 <B(21) 11
  289                 9593                  -69  01 <B(21) 1137
  290                 9597                  -71  <A(22) 1138
  291                 9604                  -68  01 (11)B> 1138
  292                 9609                  -71  01 <C(33) 33 1137
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 <C(33) 331+V(1) 112 12
    1                   13                    3  11 (12)A> 331+V(1) 112 12
    2           23+10*V(1)             5+2*V(1)  112+V(1) (12)A> 112 12
    3           31+10*V(1)             7+2*V(1)  113+V(1) (11)C> 11 12
    4           34+10*V(1)             4+2*V(1)  113+V(1) <C(33) 31 12
    5           40+12*V(1)                   -2  <C(33) 333+V(1) 31 12
    6           51+12*V(1)                    1  01 (11)B> 333+V(1) 31 12
    7           81+22*V(1)             7+2*V(1)  01 113+V(1) (11)B> 31 12
    8           89+22*V(1)             9+2*V(1)  01 114+V(1) (11)B> 12
    9           98+22*V(1)             6+2*V(1)  01 114+V(1) <B(21) 11
   10          122+28*V(1)                   -2  01 <B(21) 115+V(1)
   11          126+28*V(1)                   -4  <A(22) 116+V(1)
   12          133+28*V(1)                   -1  01 (11)B> 116+V(1)
   13          138+28*V(1)                   -4  01 <C(33) 33 115+V(1)
<< Success! ==> defined new CTR 5 (PPA)
  292                 9609                  -71  01 <C(33) 33 1137
== Executing  PA-CTR  1, V(1)=33, V(2)=0, repcount=12, factor=4/3
  412                17169                  -95  01 <C(33) 3349 11
  413                17182                  -92  11 (12)A> 3349 11
  414                17672                    6  1150 (12)A> 11
  415                17680                    8  1151 (11)C>
  416                17689                    5  1151 <B(21) 12
  417                17995                  -97  <B(21) 1151 12
  418                18004                  -94  11 (11)C> 1151 12
  419                18007                  -97  11 <C(33) 31 1150 12
  420                18009                  -99  <C(33) 33 31 1150 12
  421                18020                  -96  01 (11)B> 33 31 1150 12
  422                18030                  -94  01 11 (11)B> 31 1150 12
  423                18038                  -92  01 112 (11)B> 1150 12
  424                18043                  -95  01 112 <C(33) 33 1149 12
  425                18047                  -99  01 <C(33) 333 1149 12
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 <C(33) 334+V(1) 11
    1                   13                    3  11 (12)A> 334+V(1) 11
    2           53+10*V(1)            11+2*V(1)  115+V(1) (12)A> 11
    3           61+10*V(1)            13+2*V(1)  116+V(1) (11)C>
    4           70+10*V(1)            10+2*V(1)  116+V(1) <B(21) 12
    5          106+16*V(1)                   -2  <B(21) 116+V(1) 12
    6          115+16*V(1)                    1  11 (11)C> 116+V(1) 12
    7          118+16*V(1)                   -2  11 <C(33) 31 115+V(1) 12
    8          120+16*V(1)                   -4  <C(33) 33 31 115+V(1) 12
    9          131+16*V(1)                   -1  01 (11)B> 33 31 115+V(1) 12
   10          141+16*V(1)                    1  01 11 (11)B> 31 115+V(1) 12
   11          149+16*V(1)                    3  01 112 (11)B> 115+V(1) 12
   12          154+16*V(1)                    0  01 112 <C(33) 33 114+V(1) 12
   13          158+16*V(1)                   -4  01 <C(33) 333 114+V(1) 12
<< Success! ==> defined new CTR 6 (PPA)
  425                18047                  -99  01 <C(33) 333 1149 12
== Executing  PA-CTR  2, V(1)=45, V(2)=2, repcount=16, factor=4/3
  585                31967                 -131  01 <C(33) 3367 11 12
  586                31980                 -128  11 (12)A> 3367 11 12
  587                32650                    6  1168 (12)A> 11 12
  588                32658                    8  1169 (11)C> 12
  589                32661                    5  1169 <C(33) 32
  590                32799                 -133  <C(33) 3369 32
  591                32810                 -130  01 (11)B> 3369 32
  592                33500                    8  01 1169 (11)B> 32
  593                33502                   10  01 1170 (22)A>
  594                33507                    7  01 1170 <B(00) 22
  595                33517                    5  01 1169 <B(21) 12 22
  596                33931                 -133  01 <B(21) 1169 12 22
  597                33935                 -135  <A(22) 1170 12 22
  598                33942                 -132  01 (11)B> 1170 12 22
  599                33947                 -135  01 <C(33) 33 1169 12 22
  600                33960                 -132  11 (12)A> 33 1169 12 22
  601                33970                 -130  112 (12)A> 1169 12 22
  602                33978                 -128  113 (11)C> 1168 12 22
  603                33981                 -131  113 <C(33) 31 1167 12 22
  604                33987                 -137  <C(33) 333 31 1167 12 22
  605                33998                 -134  01 (11)B> 333 31 1167 12 22
  606                34028                 -128  01 113 (11)B> 31 1167 12 22
  607                34036                 -126  01 114 (11)B> 1167 12 22
  608                34041                 -129  01 114 <C(33) 33 1166 12 22
  609                34049                 -137  01 <C(33) 335 1166 12 22
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  01 <C(33) 331+V(2) 114+V(1) [*]* [*]*
    1                   13                    3  11 (12)A> 331+V(2) 114+V(1) [*]* [*]*
    2           23+10*V(2)             5+2*V(2)  112+V(2) (12)A> 114+V(1) [*]* [*]*
    3           31+10*V(2)             7+2*V(2)  113+V(2) (11)C> 113+V(1) [*]* [*]*
    4           34+10*V(2)             4+2*V(2)  113+V(2) <C(33) 31 112+V(1) [*]* [*]*
    5           40+12*V(2)                   -2  <C(33) 333+V(2) 31 112+V(1) [*]* [*]*
    6           51+12*V(2)                    1  01 (11)B> 333+V(2) 31 112+V(1) [*]* [*]*
    7           81+22*V(2)             7+2*V(2)  01 113+V(2) (11)B> 31 112+V(1) [*]* [*]*
    8           89+22*V(2)             9+2*V(2)  01 114+V(2) (11)B> 112+V(1) [*]* [*]*
    9           94+22*V(2)             6+2*V(2)  01 114+V(2) <C(33) 33 111+V(1) [*]* [*]*
   10          102+24*V(2)                   -2  01 <C(33) 335+V(2) 111+V(1) [*]* [*]*
<< Success! ==> defined new CTR 7 (PA)
  609                34049                 -137  01 <C(33) 335 1166 12 22
== Executing  PA-CTR  7, V(1)=62, V(2)=4, repcount=21, factor=4/3
  819                58367                 -179  01 <C(33) 3389 113 12 22
  820                58380                 -176  11 (12)A> 3389 113 12 22
  821                59270                    2  1190 (12)A> 113 12 22
  822                59278                    4  1191 (11)C> 112 12 22
  823                59281                    1  1191 <C(33) 31 11 12 22
  824                59463                 -181  <C(33) 3391 31 11 12 22
  825                59474                 -178  01 (11)B> 3391 31 11 12 22
  826                60384                    4  01 1191 (11)B> 31 11 12 22
  827                60392                    6  01 1192 (11)B> 11 12 22
  828                60397                    3  01 1192 <C(33) 33 12 22
  829                60581                 -181  01 <C(33) 3393 12 22
  830                60594                 -178  11 (12)A> 3393 12 22
  831                61524                    8  1194 (12)A> 12 22
  832                61534                   10  1195 (11)B> 22
  833                61540                   12  1196 (11)B>
  834                61545                    9  1196 <B(21) 20
  835                62121                 -183  <B(21) 1196 20
  836                62130                 -180  11 (11)C> 1196 20
  837                62133                 -183  11 <C(33) 31 1195 20
  838                62135                 -185  <C(33) 33 31 1195 20
  839                62146                 -182  01 (11)B> 33 31 1195 20
  840                62156                 -180  01 11 (11)B> 31 1195 20
  841                62164                 -178  01 112 (11)B> 1195 20
  842                62169                 -181  01 112 <C(33) 33 1194 20
  843                62173                 -185  01 <C(33) 333 1194 20
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  01 <C(33) 331+V(2) 113 12 221+V(1)
    1                   13                    3  11 (12)A> 331+V(2) 113 12 221+V(1)
    2           23+10*V(2)             5+2*V(2)  112+V(2) (12)A> 113 12 221+V(1)
    3           31+10*V(2)             7+2*V(2)  113+V(2) (11)C> 112 12 221+V(1)
    4           34+10*V(2)             4+2*V(2)  113+V(2) <C(33) 31 11 12 221+V(1)
    5           40+12*V(2)                   -2  <C(33) 333+V(2) 31 11 12 221+V(1)
    6           51+12*V(2)                    1  01 (11)B> 333+V(2) 31 11 12 221+V(1)
    7           81+22*V(2)             7+2*V(2)  01 113+V(2) (11)B> 31 11 12 221+V(1)
    8           89+22*V(2)             9+2*V(2)  01 114+V(2) (11)B> 11 12 221+V(1)
    9           94+22*V(2)             6+2*V(2)  01 114+V(2) <C(33) 33 12 221+V(1)
   10          102+24*V(2)                   -2  01 <C(33) 335+V(2) 12 221+V(1)
   11          115+24*V(2)                    1  11 (12)A> 335+V(2) 12 221+V(1)
   12          165+34*V(2)            11+2*V(2)  116+V(2) (12)A> 12 221+V(1)
   13          175+34*V(2)            13+2*V(2)  117+V(2) (11)B> 221+V(1)
   14   181+6*V(1)+34*V(2)     15+2*V(1)+2*V(2)  118+V(1)+V(2) (11)B>
   15   186+6*V(1)+34*V(2)     12+2*V(1)+2*V(2)  118+V(1)+V(2) <B(21) 20
   16  234+12*V(1)+40*V(2)                   -4  <B(21) 118+V(1)+V(2) 20
   17  243+12*V(1)+40*V(2)                   -1  11 (11)C> 118+V(1)+V(2) 20
   18  246+12*V(1)+40*V(2)                   -4  11 <C(33) 31 117+V(1)+V(2) 20
   19  248+12*V(1)+40*V(2)                   -6  <C(33) 33 31 117+V(1)+V(2) 20
   20  259+12*V(1)+40*V(2)                   -3  01 (11)B> 33 31 117+V(1)+V(2) 20
   21  269+12*V(1)+40*V(2)                   -1  01 11 (11)B> 31 117+V(1)+V(2) 20
   22  277+12*V(1)+40*V(2)                    1  01 112 (11)B> 117+V(1)+V(2) 20
   23  282+12*V(1)+40*V(2)                   -2  01 112 <C(33) 33 116+V(1)+V(2) 20
   24  286+12*V(1)+40*V(2)                   -6  01 <C(33) 333 116+V(1)+V(2) 20
<< Success! ==> defined new CTR 8 (PPA)
  843                62173                 -185  01 <C(33) 333 1194 20
== Executing  PA-CTR  2, V(1)=90, V(2)=2, repcount=31, factor=4/3
 1153               111463                 -247  01 <C(33) 33127 11 20
 1154               111476                 -244  11 (12)A> 33127 11 20
 1155               112746                   10  11128 (12)A> 11 20
 1156               112754                   12  11129 (11)C> 20
 1157               112759                    9  11129 <B(21) 10
 1158               113533                 -249  <B(21) 11129 10
 1159               113542                 -246  11 (11)C> 11129 10
 1160               113545                 -249  11 <C(33) 31 11128 10
 1161               113547                 -251  <C(33) 33 31 11128 10
 1162               113558                 -248  01 (11)B> 33 31 11128 10
 1163               113568                 -246  01 11 (11)B> 31 11128 10
 1164               113576                 -244  01 112 (11)B> 11128 10
 1165               113581                 -247  01 112 <C(33) 33 11127 10
 1166               113585                 -251  01 <C(33) 333 11127 10
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 <C(33) 334+V(1) 11 20
    1                   13                    3  11 (12)A> 334+V(1) 11 20
    2           53+10*V(1)            11+2*V(1)  115+V(1) (12)A> 11 20
    3           61+10*V(1)            13+2*V(1)  116+V(1) (11)C> 20
    4           66+10*V(1)            10+2*V(1)  116+V(1) <B(21) 10
    5          102+16*V(1)                   -2  <B(21) 116+V(1) 10
    6          111+16*V(1)                    1  11 (11)C> 116+V(1) 10
    7          114+16*V(1)                   -2  11 <C(33) 31 115+V(1) 10
    8          116+16*V(1)                   -4  <C(33) 33 31 115+V(1) 10
    9          127+16*V(1)                   -1  01 (11)B> 33 31 115+V(1) 10
   10          137+16*V(1)                    1  01 11 (11)B> 31 115+V(1) 10
   11          145+16*V(1)                    3  01 112 (11)B> 115+V(1) 10
   12          150+16*V(1)                    0  01 112 <C(33) 33 114+V(1) 10
   13          154+16*V(1)                   -4  01 <C(33) 333 114+V(1) 10
<< Success! ==> defined new CTR 9 (PPA)
 1166               113585                 -251  01 <C(33) 333 11127 10
== Executing  PA-CTR  2, V(1)=123, V(2)=2, repcount=42, factor=4/3
 1586               202541                 -335  01 <C(33) 33171 11 10
 1587               202554                 -332  11 (12)A> 33171 11 10
 1588               204264                   10  11172 (12)A> 11 10
 1589               204272                   12  11173 (11)C> 10
 1590               204275                    9  11173 <C(33) 30
 1591               204621                 -337  <C(33) 33173 30
 1592               204632                 -334  01 (11)B> 33173 30
 1593               206362                   12  01 11173 (11)B> 30
 1594               206364                   14  01 11174 (21)B>
 1595               206367                   11  01 11174 <B(02) 20
 1596               206372                   14  01 11174 (11)B> 20
 1597               206383                   11  01 11174 <B(21) 12
 1598               207427                 -337  01 <B(21) 11174 12
 1599               207431                 -339  <A(22) 11175 12
 1600               207438                 -336  01 (11)B> 11175 12
 1601               207443                 -339  01 <C(33) 33 11174 12
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 <C(33) 331+V(1) 11 10
    1                   13                    3  11 (12)A> 331+V(1) 11 10
    2           23+10*V(1)             5+2*V(1)  112+V(1) (12)A> 11 10
    3           31+10*V(1)             7+2*V(1)  113+V(1) (11)C> 10
    4           34+10*V(1)             4+2*V(1)  113+V(1) <C(33) 30
    5           40+12*V(1)                   -2  <C(33) 333+V(1) 30
    6           51+12*V(1)                    1  01 (11)B> 333+V(1) 30
    7           81+22*V(1)             7+2*V(1)  01 113+V(1) (11)B> 30
    8           83+22*V(1)             9+2*V(1)  01 114+V(1) (21)B>
    9           86+22*V(1)             6+2*V(1)  01 114+V(1) <B(02) 20
   10           91+22*V(1)             9+2*V(1)  01 114+V(1) (11)B> 20
   11          102+22*V(1)             6+2*V(1)  01 114+V(1) <B(21) 12
   12          126+28*V(1)                   -2  01 <B(21) 114+V(1) 12
   13          130+28*V(1)                   -4  <A(22) 115+V(1) 12
   14          137+28*V(1)                   -1  01 (11)B> 115+V(1) 12
   15          142+28*V(1)                   -4  01 <C(33) 33 114+V(1) 12
<< Success! ==> defined new CTR 10 (PPA)
 1601               207443                 -339  01 <C(33) 33 11174 12
== Executing  PA-CTR  2, V(1)=170, V(2)=0, repcount=57, factor=4/3
 2171               366473                 -453  01 <C(33) 33229 113 12
== Executing PPA-CTR  4 (once), V(1)=228
 2194               375867                 -459  01 <C(33) 333 11233 20
== Executing  PA-CTR  2, V(1)=229, V(2)=2, repcount=77, factor=4/3
 2964               668313                 -613  01 <C(33) 33311 112 20
== Executing PPA-CTR  3 (once), V(1)=310
 2977               677133                 -617  01 <C(33) 33 11314 12
== Executing  PA-CTR  2, V(1)=310, V(2)=0, repcount=104, factor=4/3
 4017              1201917                 -825  01 <C(33) 33417 112 12
== Executing PPA-CTR  5 (once), V(1)=416
 4030              1213703                 -829  01 <C(33) 33 11421
== Executing  PA-CTR  1, V(1)=417, V(2)=0, repcount=140, factor=4/3
 5430              2162063                -1109  01 <C(33) 33561 11
== Executing PPA-CTR  6 (once), V(1)=557
 5443              2171133                -1113  01 <C(33) 333 11561 12
== Executing  PA-CTR  2, V(1)=557, V(2)=2, repcount=186, factor=4/3
 7303              3850713                -1485  01 <C(33) 33747 113 12
== Executing PPA-CTR  4 (once), V(1)=746
 7326              3880827                -1491  01 <C(33) 333 11751 20
== Executing  PA-CTR  2, V(1)=747, V(2)=2, repcount=250, factor=4/3
 9826              6906327                -1991  01 <C(33) 331003 11 20
== Executing PPA-CTR  9 (once), V(1)=999
 9839              6922465                -1995  01 <C(33) 333 111003 10
== Executing  PA-CTR  2, V(1)=999, V(2)=2, repcount=334, factor=4/3
13179             12311221                -2663  01 <C(33) 331339 11 10
== Executing PPA-CTR 10 (once), V(1)=1338
13194             12348827                -2667  01 <C(33) 33 111342 12
== Executing  PA-CTR  2, V(1)=1338, V(2)=0, repcount=447, factor=4/3
17664             21963797                -3561  01 <C(33) 331789 11 12
17665             21963810                -3558  11 (12)A> 331789 11 12
17666             21981700                   20  111790 (12)A> 11 12
17667             21981708                   22  111791 (11)C> 12
17668             21981711                   19  111791 <C(33) 32
17669             21985293                -3563  <C(33) 331791 32
17670             21985304                -3560  01 (11)B> 331791 32
17671             22003214                   22  01 111791 (11)B> 32
17672             22003216                   24  01 111792 (22)A>
17673             22003221                   21  01 111792 <B(00) 22
17674             22003231                   19  01 111791 <B(21) 12 22
17675             22013977                -3563  01 <B(21) 111791 12 22
17676             22013981                -3565  <A(22) 111792 12 22
17677             22013988                -3562  01 (11)B> 111792 12 22
17678             22013993                -3565  01 <C(33) 33 111791 12 22
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 <C(33) 332+V(1) 11 12
    1                   13                    3  11 (12)A> 332+V(1) 11 12
    2           33+10*V(1)             7+2*V(1)  113+V(1) (12)A> 11 12
    3           41+10*V(1)             9+2*V(1)  114+V(1) (11)C> 12
    4           44+10*V(1)             6+2*V(1)  114+V(1) <C(33) 32
    5           52+12*V(1)                   -2  <C(33) 334+V(1) 32
    6           63+12*V(1)                    1  01 (11)B> 334+V(1) 32
    7          103+22*V(1)             9+2*V(1)  01 114+V(1) (11)B> 32
    8          105+22*V(1)            11+2*V(1)  01 115+V(1) (22)A>
    9          110+22*V(1)             8+2*V(1)  01 115+V(1) <B(00) 22
   10          120+22*V(1)             6+2*V(1)  01 114+V(1) <B(21) 12 22
   11          144+28*V(1)                   -2  01 <B(21) 114+V(1) 12 22
   12          148+28*V(1)                   -4  <A(22) 115+V(1) 12 22
   13          155+28*V(1)                   -1  01 (11)B> 115+V(1) 12 22
   14          160+28*V(1)                   -4  01 <C(33) 33 114+V(1) 12 22
<< Success! ==> defined new CTR 11 (PPA)
17678             22013993                -3565  01 <C(33) 33 111791 12 22
== Executing  PA-CTR  7, V(1)=1787, V(2)=0, repcount=596, factor=4/3
23638             39096545                -4757  01 <C(33) 332385 113 12 22
== Executing PPA-CTR  8 (once), V(1)=0, V(2)=2384
23662             39192191                -4763  01 <C(33) 333 112390 20
== Executing  PA-CTR  2, V(1)=2386, V(2)=2, repcount=796, factor=4/3
31622             69686951                -6355  01 <C(33) 333187 112 20
== Executing PPA-CTR  3 (once), V(1)=3186
31635             69776299                -6359  01 <C(33) 33 113190 12
== Executing  PA-CTR  2, V(1)=3186, V(2)=0, repcount=1063, factor=4/3
42265            124072213                -8485  01 <C(33) 334253 11 12
== Executing PPA-CTR 11 (once), V(1)=4251
42279            124191401                -8489  01 <C(33) 33 114255 12 22
== Executing  PA-CTR  7, V(1)=4251, V(2)=0, repcount=1418, factor=4/3
56459            220782725               -11325  01 <C(33) 335673 11 12 22
56460            220782738               -11322  11 (12)A> 335673 11 12 22
56461            220839468                   24  115674 (12)A> 11 12 22
56462            220839476                   26  115675 (11)C> 12 22
56463            220839479                   23  115675 <C(33) 32 22
56464            220850829               -11327  <C(33) 335675 32 22
56465            220850840               -11324  01 (11)B> 335675 32 22
56466            220907590                   26  01 115675 (11)B> 32 22
56467            220907592                   28  01 115676 (22)A> 22
56468            220907594                   30  01 115676 22 (22)A>
56469            220907599                   27  01 115676 22 <B(00) 22
56470            220907601                   25  01 115676 <B(00) 00 22
56471            220907611                   23  01 115675 <B(21) 12 00 22
56472            220941661               -11327  01 <B(21) 115675 12 00 22
56473            220941665               -11329  <A(22) 115676 12 00 22
56474            220941672               -11326  01 (11)B> 115676 12 00 22
56475            220941677               -11329  01 <C(33) 33 115675 12 00 22
56476            220941690               -11326  11 (12)A> 33 115675 12 00 22
56477            220941700               -11324  112 (12)A> 115675 12 00 22
56478            220941708               -11322  113 (11)C> 115674 12 00 22
56479            220941711               -11325  113 <C(33) 31 115673 12 00 22
56480            220941717               -11331  <C(33) 333 31 115673 12 00 22
56481            220941728               -11328  01 (11)B> 333 31 115673 12 00 22
56482            220941758               -11322  01 113 (11)B> 31 115673 12 00 22
56483            220941766               -11320  01 114 (11)B> 115673 12 00 22
56484            220941771               -11323  01 114 <C(33) 33 115672 12 00 22
56485            220941779               -11331  01 <C(33) 335 115672 12 00 22
>> Try to prove a PA-CTR with 2 Vars...
    0                    0                    0  01 <C(33) 331+V(2) 114+V(1) [*]* [*]* [*]*
    1                   13                    3  11 (12)A> 331+V(2) 114+V(1) [*]* [*]* [*]*
    2           23+10*V(2)             5+2*V(2)  112+V(2) (12)A> 114+V(1) [*]* [*]* [*]*
    3           31+10*V(2)             7+2*V(2)  113+V(2) (11)C> 113+V(1) [*]* [*]* [*]*
    4           34+10*V(2)             4+2*V(2)  113+V(2) <C(33) 31 112+V(1) [*]* [*]* [*]*
    5           40+12*V(2)                   -2  <C(33) 333+V(2) 31 112+V(1) [*]* [*]* [*]*
    6           51+12*V(2)                    1  01 (11)B> 333+V(2) 31 112+V(1) [*]* [*]* [*]*
    7           81+22*V(2)             7+2*V(2)  01 113+V(2) (11)B> 31 112+V(1) [*]* [*]* [*]*
    8           89+22*V(2)             9+2*V(2)  01 114+V(2) (11)B> 112+V(1) [*]* [*]* [*]*
    9           94+22*V(2)             6+2*V(2)  01 114+V(2) <C(33) 33 111+V(1) [*]* [*]* [*]*
   10          102+24*V(2)                   -2  01 <C(33) 335+V(2) 111+V(1) [*]* [*]* [*]*
<< Success! ==> defined new CTR 12 (PA)
56485            220941779               -11331  01 <C(33) 335 115672 12 00 22
== Executing  PA-CTR 12, V(1)=5668, V(2)=4, repcount=1890, factor=4/3
75385            392686079               -15111  01 <C(33) 337565 112 12 00 22
75386            392686092               -15108  11 (12)A> 337565 112 12 00 22
75387            392761742                   22  117566 (12)A> 112 12 00 22
75388            392761750                   24  117567 (11)C> 11 12 00 22
75389            392761753                   21  117567 <C(33) 31 12 00 22
75390            392776887               -15113  <C(33) 337567 31 12 00 22
75391            392776898               -15110  01 (11)B> 337567 31 12 00 22
75392            392852568                   24  01 117567 (11)B> 31 12 00 22
75393            392852576                   26  01 117568 (11)B> 12 00 22
75394            392852585                   23  01 117568 <B(21) 11 00 22
75395            392897993               -15113  01 <B(21) 117569 00 22
75396            392897997               -15115  <A(22) 117570 00 22
75397            392898004               -15112  01 (11)B> 117570 00 22
75398            392898009               -15115  01 <C(33) 33 117569 00 22
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 <C(33) 331+V(1) 112 12 [*]* [*]*
    1                   13                    3  11 (12)A> 331+V(1) 112 12 [*]* [*]*
    2           23+10*V(1)             5+2*V(1)  112+V(1) (12)A> 112 12 [*]* [*]*
    3           31+10*V(1)             7+2*V(1)  113+V(1) (11)C> 11 12 [*]* [*]*
    4           34+10*V(1)             4+2*V(1)  113+V(1) <C(33) 31 12 [*]* [*]*
    5           40+12*V(1)                   -2  <C(33) 333+V(1) 31 12 [*]* [*]*
    6           51+12*V(1)                    1  01 (11)B> 333+V(1) 31 12 [*]* [*]*
    7           81+22*V(1)             7+2*V(1)  01 113+V(1) (11)B> 31 12 [*]* [*]*
    8           89+22*V(1)             9+2*V(1)  01 114+V(1) (11)B> 12 [*]* [*]*
    9           98+22*V(1)             6+2*V(1)  01 114+V(1) <B(21) 11 [*]* [*]*
   10          122+28*V(1)                   -2  01 <B(21) 115+V(1) [*]* [*]*
   11          126+28*V(1)                   -4  <A(22) 116+V(1) [*]* [*]*
   12          133+28*V(1)                   -1  01 (11)B> 116+V(1) [*]* [*]*
   13          138+28*V(1)                   -4  01 <C(33) 33 115+V(1) [*]* [*]*
<< Success! ==> defined new CTR 13 (PPA)
75398            392898009               -15115  01 <C(33) 33 117569 00 22
== Executing  PA-CTR  7, V(1)=7565, V(2)=0, repcount=2522, factor=4/3
100618            698337429               -20159  01 <C(33) 3310089 113 00 22
100619            698337442               -20156  11 (12)A> 3310089 113 00 22
100620            698438332                   22  1110090 (12)A> 113 00 22
100621            698438340                   24  1110091 (11)C> 112 00 22
100622            698438343                   21  1110091 <C(33) 31 11 00 22
100623            698458525               -20161  <C(33) 3310091 31 11 00 22
100624            698458536               -20158  01 (11)B> 3310091 31 11 00 22
100625            698559446                   24  01 1110091 (11)B> 31 11 00 22
100626            698559454                   26  01 1110092 (11)B> 11 00 22
100627            698559459                   23  01 1110092 <C(33) 33 00 22
100628            698579643               -20161  01 <C(33) 3310093 00 22
100629            698579656               -20158  11 (12)A> 3310093 00 22
100630            698680586                   28  1110094 (12)A> 00 22
100631            698680598                   30  1110095 (11)B> 22
100632            698680604                   32  1110096 (11)B>
100633            698680609                   29  1110096 <B(21) 20
100634            698741185               -20163  <B(21) 1110096 20
100635            698741194               -20160  11 (11)C> 1110096 20
100636            698741197               -20163  11 <C(33) 31 1110095 20
100637            698741199               -20165  <C(33) 33 31 1110095 20
100638            698741210               -20162  01 (11)B> 33 31 1110095 20
100639            698741220               -20160  01 11 (11)B> 31 1110095 20
100640            698741228               -20158  01 112 (11)B> 1110095 20
100641            698741233               -20161  01 112 <C(33) 33 1110094 20
100642            698741237               -20165  01 <C(33) 333 1110094 20
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  01 <C(33) 331+V(2) 113 00 221+V(1)
    1                   13                    3  11 (12)A> 331+V(2) 113 00 221+V(1)
    2           23+10*V(2)             5+2*V(2)  112+V(2) (12)A> 113 00 221+V(1)
    3           31+10*V(2)             7+2*V(2)  113+V(2) (11)C> 112 00 221+V(1)
    4           34+10*V(2)             4+2*V(2)  113+V(2) <C(33) 31 11 00 221+V(1)
    5           40+12*V(2)                   -2  <C(33) 333+V(2) 31 11 00 221+V(1)
    6           51+12*V(2)                    1  01 (11)B> 333+V(2) 31 11 00 221+V(1)
    7           81+22*V(2)             7+2*V(2)  01 113+V(2) (11)B> 31 11 00 221+V(1)
    8           89+22*V(2)             9+2*V(2)  01 114+V(2) (11)B> 11 00 221+V(1)
    9           94+22*V(2)             6+2*V(2)  01 114+V(2) <C(33) 33 00 221+V(1)
   10          102+24*V(2)                   -2  01 <C(33) 335+V(2) 00 221+V(1)
   11          115+24*V(2)                    1  11 (12)A> 335+V(2) 00 221+V(1)
   12          165+34*V(2)            11+2*V(2)  116+V(2) (12)A> 00 221+V(1)
   13          177+34*V(2)            13+2*V(2)  117+V(2) (11)B> 221+V(1)
   14   183+6*V(1)+34*V(2)     15+2*V(1)+2*V(2)  118+V(1)+V(2) (11)B>
   15   188+6*V(1)+34*V(2)     12+2*V(1)+2*V(2)  118+V(1)+V(2) <B(21) 20
   16  236+12*V(1)+40*V(2)                   -4  <B(21) 118+V(1)+V(2) 20
   17  245+12*V(1)+40*V(2)                   -1  11 (11)C> 118+V(1)+V(2) 20
   18  248+12*V(1)+40*V(2)                   -4  11 <C(33) 31 117+V(1)+V(2) 20
   19  250+12*V(1)+40*V(2)                   -6  <C(33) 33 31 117+V(1)+V(2) 20
   20  261+12*V(1)+40*V(2)                   -3  01 (11)B> 33 31 117+V(1)+V(2) 20
   21  271+12*V(1)+40*V(2)                   -1  01 11 (11)B> 31 117+V(1)+V(2) 20
   22  279+12*V(1)+40*V(2)                    1  01 112 (11)B> 117+V(1)+V(2) 20
   23  284+12*V(1)+40*V(2)                   -2  01 112 <C(33) 33 116+V(1)+V(2) 20
   24  288+12*V(1)+40*V(2)                   -6  01 <C(33) 333 116+V(1)+V(2) 20
<< Success! ==> defined new CTR 14 (PPA)
100642            698741237               -20165  01 <C(33) 333 1110094 20
== Executing  PA-CTR  2, V(1)=10090, V(2)=2, repcount=3364, factor=4/3
134282           1242276173               -26893  01 <C(33) 3313459 112 20
== Executing PPA-CTR  3 (once), V(1)=13458
134295           1242653137               -26897  01 <C(33) 33 1113462 12
== Executing  PA-CTR  2, V(1)=13458, V(2)=0, repcount=4487, factor=4/3
179165           2209287547               -35871  01 <C(33) 3317949 11 12
== Executing PPA-CTR 11 (once), V(1)=17947
179179           2209790223               -35875  01 <C(33) 33 1117951 12 22
== Executing  PA-CTR  7, V(1)=17947, V(2)=0, repcount=5983, factor=4/3
239009           3928335177               -47841  01 <C(33) 3323933 112 12 22
239010           3928335190               -47838  11 (12)A> 3323933 112 12 22
239011           3928574520                   28  1123934 (12)A> 112 12 22
239012           3928574528                   30  1123935 (11)C> 11 12 22
239013           3928574531                   27  1123935 <C(33) 31 12 22
239014           3928622401               -47843  <C(33) 3323935 31 12 22
239015           3928622412               -47840  01 (11)B> 3323935 31 12 22
239016           3928861762                   30  01 1123935 (11)B> 31 12 22
239017           3928861770                   32  01 1123936 (11)B> 12 22
239018           3928861779                   29  01 1123936 <B(21) 11 22
239019           3929005395               -47843  01 <B(21) 1123937 22
239020           3929005399               -47845  <A(22) 1123938 22
239021           3929005406               -47842  01 (11)B> 1123938 22
239022           3929005411               -47845  01 <C(33) 33 1123937 22
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 <C(33) 331+V(1) 112 12 [*]*
    1                   13                    3  11 (12)A> 331+V(1) 112 12 [*]*
    2           23+10*V(1)             5+2*V(1)  112+V(1) (12)A> 112 12 [*]*
    3           31+10*V(1)             7+2*V(1)  113+V(1) (11)C> 11 12 [*]*
    4           34+10*V(1)             4+2*V(1)  113+V(1) <C(33) 31 12 [*]*
    5           40+12*V(1)                   -2  <C(33) 333+V(1) 31 12 [*]*
    6           51+12*V(1)                    1  01 (11)B> 333+V(1) 31 12 [*]*
    7           81+22*V(1)             7+2*V(1)  01 113+V(1) (11)B> 31 12 [*]*
    8           89+22*V(1)             9+2*V(1)  01 114+V(1) (11)B> 12 [*]*
    9           98+22*V(1)             6+2*V(1)  01 114+V(1) <B(21) 11 [*]*
   10          122+28*V(1)                   -2  01 <B(21) 115+V(1) [*]*
   11          126+28*V(1)                   -4  <A(22) 116+V(1) [*]*
   12          133+28*V(1)                   -1  01 (11)B> 116+V(1) [*]*
   13          138+28*V(1)                   -4  01 <C(33) 33 115+V(1) [*]*
<< Success! ==> defined new CTR 15 (PPA)
239022           3929005411               -47845  01 <C(33) 33 1123937 22
== Executing  PA-CTR  2, V(1)=23933, V(2)=0, repcount=7978, factor=4/3
318802           6984563455               -63801  01 <C(33) 3331913 113 22
318803           6984563468               -63798  11 (12)A> 3331913 113 22
318804           6984882598                   28  1131914 (12)A> 113 22
318805           6984882606                   30  1131915 (11)C> 112 22
318806           6984882609                   27  1131915 <C(33) 31 11 22
318807           6984946439               -63803  <C(33) 3331915 31 11 22
318808           6984946450               -63800  01 (11)B> 3331915 31 11 22
318809           6985265600                   30  01 1131915 (11)B> 31 11 22
318810           6985265608                   32  01 1131916 (11)B> 11 22
318811           6985265613                   29  01 1131916 <C(33) 33 22
318812           6985329445               -63803  01 <C(33) 3331917 22
318813           6985329458               -63800  11 (12)A> 3331917 22
318814           6985648628                   34  1131918 (12)A> 22
318815           6985648630                   36  1131918 12 (22)A>
318816           6985648635                   33  1131918 12 <B(00) 22
318817           6985648643                   31  1131918 <B(21) 20 22
318818           6985840151               -63805  <B(21) 1131918 20 22
318819           6985840160               -63802  11 (11)C> 1131918 20 22
318820           6985840163               -63805  11 <C(33) 31 1131917 20 22
318821           6985840165               -63807  <C(33) 33 31 1131917 20 22
318822           6985840176               -63804  01 (11)B> 33 31 1131917 20 22
318823           6985840186               -63802  01 11 (11)B> 31 1131917 20 22
318824           6985840194               -63800  01 112 (11)B> 1131917 20 22
318825           6985840199               -63803  01 112 <C(33) 33 1131916 20 22
318826           6985840203               -63807  01 <C(33) 333 1131916 20 22
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 <C(33) 331+V(1) 113 22
    1                   13                    3  11 (12)A> 331+V(1) 113 22
    2           23+10*V(1)             5+2*V(1)  112+V(1) (12)A> 113 22
    3           31+10*V(1)             7+2*V(1)  113+V(1) (11)C> 112 22
    4           34+10*V(1)             4+2*V(1)  113+V(1) <C(33) 31 11 22
    5           40+12*V(1)                   -2  <C(33) 333+V(1) 31 11 22
    6           51+12*V(1)                    1  01 (11)B> 333+V(1) 31 11 22
    7           81+22*V(1)             7+2*V(1)  01 113+V(1) (11)B> 31 11 22
    8           89+22*V(1)             9+2*V(1)  01 114+V(1) (11)B> 11 22
    9           94+22*V(1)             6+2*V(1)  01 114+V(1) <C(33) 33 22
   10          102+24*V(1)                   -2  01 <C(33) 335+V(1) 22
   11          115+24*V(1)                    1  11 (12)A> 335+V(1) 22
   12          165+34*V(1)            11+2*V(1)  116+V(1) (12)A> 22
   13          167+34*V(1)            13+2*V(1)  116+V(1) 12 (22)A>
   14          172+34*V(1)            10+2*V(1)  116+V(1) 12 <B(00) 22
   15          180+34*V(1)             8+2*V(1)  116+V(1) <B(21) 20 22
   16          216+40*V(1)                   -4  <B(21) 116+V(1) 20 22
   17          225+40*V(1)                   -1  11 (11)C> 116+V(1) 20 22
   18          228+40*V(1)                   -4  11 <C(33) 31 115+V(1) 20 22
   19          230+40*V(1)                   -6  <C(33) 33 31 115+V(1) 20 22
   20          241+40*V(1)                   -3  01 (11)B> 33 31 115+V(1) 20 22
   21          251+40*V(1)                   -1  01 11 (11)B> 31 115+V(1) 20 22
   22          259+40*V(1)                    1  01 112 (11)B> 115+V(1) 20 22
   23          264+40*V(1)                   -2  01 112 <C(33) 33 114+V(1) 20 22
   24          268+40*V(1)                   -6  01 <C(33) 333 114+V(1) 20 22
<< Success! ==> defined new CTR 16 (PPA)
318826           6985840203               -63807  01 <C(33) 333 1131916 20 22
== Executing  PA-CTR  7, V(1)=31912, V(2)=2, repcount=10638, factor=4/3
425206          12418943391               -85083  01 <C(33) 3342555 112 20 22
425207          12418943404               -85080  11 (12)A> 3342555 112 20 22
425208          12419368954                   30  1142556 (12)A> 112 20 22
425209          12419368962                   32  1142557 (11)C> 11 20 22
425210          12419368965                   29  1142557 <C(33) 31 20 22
425211          12419454079               -85085  <C(33) 3342557 31 20 22
425212          12419454090               -85082  01 (11)B> 3342557 31 20 22
425213          12419879660                   32  01 1142557 (11)B> 31 20 22
425214          12419879668                   34  01 1142558 (11)B> 20 22
425215          12419879679                   31  01 1142558 <B(21) 12 22
425216          12420135027               -85085  01 <B(21) 1142558 12 22
425217          12420135031               -85087  <A(22) 1142559 12 22
425218          12420135038               -85084  01 (11)B> 1142559 12 22
425219          12420135043               -85087  01 <C(33) 33 1142558 12 22
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 <C(33) 331+V(1) 112 20 [*]*
    1                   13                    3  11 (12)A> 331+V(1) 112 20 [*]*
    2           23+10*V(1)             5+2*V(1)  112+V(1) (12)A> 112 20 [*]*
    3           31+10*V(1)             7+2*V(1)  113+V(1) (11)C> 11 20 [*]*
    4           34+10*V(1)             4+2*V(1)  113+V(1) <C(33) 31 20 [*]*
    5           40+12*V(1)                   -2  <C(33) 333+V(1) 31 20 [*]*
    6           51+12*V(1)                    1  01 (11)B> 333+V(1) 31 20 [*]*
    7           81+22*V(1)             7+2*V(1)  01 113+V(1) (11)B> 31 20 [*]*
    8           89+22*V(1)             9+2*V(1)  01 114+V(1) (11)B> 20 [*]*
    9          100+22*V(1)             6+2*V(1)  01 114+V(1) <B(21) 12 [*]*
   10          124+28*V(1)                   -2  01 <B(21) 114+V(1) 12 [*]*
   11          128+28*V(1)                   -4  <A(22) 115+V(1) 12 [*]*
   12          135+28*V(1)                   -1  01 (11)B> 115+V(1) 12 [*]*
   13          140+28*V(1)                   -4  01 <C(33) 33 114+V(1) 12 [*]*
<< Success! ==> defined new CTR 17 (PPA)
425219          12420135043               -85087  01 <C(33) 33 1142558 12 22
== Executing  PA-CTR  7, V(1)=42554, V(2)=0, repcount=14185, factor=4/3
567069          22079183833              -113457  01 <C(33) 3356741 113 12 22
== Executing PPA-CTR  8 (once), V(1)=0, V(2)=56740
567093          22081453719              -113463  01 <C(33) 333 1156746 20
== Executing  PA-CTR  2, V(1)=56742, V(2)=2, repcount=18915, factor=4/3
756243          39256689849              -151293  01 <C(33) 3375663 11 20
== Executing PPA-CTR  9 (once), V(1)=75659
756256          39257900547              -151297  01 <C(33) 333 1175663 10
== Executing  PA-CTR  2, V(1)=75659, V(2)=2, repcount=25220, factor=4/3
1008456          69790796187              -201737  01 <C(33) 33100883 113 10
1008457          69790796200              -201734  11 (12)A> 33100883 113 10
1008458          69791805030                   32  11100884 (12)A> 113 10
1008459          69791805038                   34  11100885 (11)C> 112 10
1008460          69791805041                   31  11100885 <C(33) 31 11 10
1008461          69792006811              -201739  <C(33) 33100885 31 11 10
1008462          69792006822              -201736  01 (11)B> 33100885 31 11 10
1008463          69793015672                   34  01 11100885 (11)B> 31 11 10
1008464          69793015680                   36  01 11100886 (11)B> 11 10
1008465          69793015685                   33  01 11100886 <C(33) 33 10
1008466          69793217457              -201739  01 <C(33) 33100887 10
1008467          69793217470              -201736  11 (12)A> 33100887 10
1008468          69794226340                   38  11100888 (12)A> 10
1008469          69794226355                   35  11100888 <B(21) 12
1008470          69794831683              -201741  <B(21) 11100888 12
1008471          69794831692              -201738  11 (11)C> 11100888 12
1008472          69794831695              -201741  11 <C(33) 31 11100887 12
1008473          69794831697              -201743  <C(33) 33 31 11100887 12
1008474          69794831708              -201740  01 (11)B> 33 31 11100887 12
1008475          69794831718              -201738  01 11 (11)B> 31 11100887 12
1008476          69794831726              -201736  01 112 (11)B> 11100887 12
1008477          69794831731              -201739  01 112 <C(33) 33 11100886 12
1008478          69794831735              -201743  01 <C(33) 333 11100886 12
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 <C(33) 331+V(1) 113 10
    1                   13                    3  11 (12)A> 331+V(1) 113 10
    2           23+10*V(1)             5+2*V(1)  112+V(1) (12)A> 113 10
    3           31+10*V(1)             7+2*V(1)  113+V(1) (11)C> 112 10
    4           34+10*V(1)             4+2*V(1)  113+V(1) <C(33) 31 11 10
    5           40+12*V(1)                   -2  <C(33) 333+V(1) 31 11 10
    6           51+12*V(1)                    1  01 (11)B> 333+V(1) 31 11 10
    7           81+22*V(1)             7+2*V(1)  01 113+V(1) (11)B> 31 11 10
    8           89+22*V(1)             9+2*V(1)  01 114+V(1) (11)B> 11 10
    9           94+22*V(1)             6+2*V(1)  01 114+V(1) <C(33) 33 10
   10          102+24*V(1)                   -2  01 <C(33) 335+V(1) 10
   11          115+24*V(1)                    1  11 (12)A> 335+V(1) 10
   12          165+34*V(1)            11+2*V(1)  116+V(1) (12)A> 10
   13          180+34*V(1)             8+2*V(1)  116+V(1) <B(21) 12
   14          216+40*V(1)                   -4  <B(21) 116+V(1) 12
   15          225+40*V(1)                   -1  11 (11)C> 116+V(1) 12
   16          228+40*V(1)                   -4  11 <C(33) 31 115+V(1) 12
   17          230+40*V(1)                   -6  <C(33) 33 31 115+V(1) 12
   18          241+40*V(1)                   -3  01 (11)B> 33 31 115+V(1) 12
   19          251+40*V(1)                   -1  01 11 (11)B> 31 115+V(1) 12
   20          259+40*V(1)                    1  01 112 (11)B> 115+V(1) 12
   21          264+40*V(1)                   -2  01 112 <C(33) 33 114+V(1) 12
   22          268+40*V(1)                   -6  01 <C(33) 333 114+V(1) 12
<< Success! ==> defined new CTR 18 (PPA)
1008478          69794831735              -201743  01 <C(33) 333 11100886 12
== Executing  PA-CTR  2, V(1)=100882, V(2)=2, repcount=33628, factor=4/3
1344758         124078696223              -268999  01 <C(33) 33134515 112 12
== Executing PPA-CTR  5 (once), V(1)=134514
1344771         124082462753              -269003  01 <C(33) 33 11134519
== Executing  PA-CTR  1, V(1)=134515, V(2)=0, repcount=44839, factor=4/3
1793161         220590608267              -358681  01 <C(33) 33179357 112
1793162         220590608280              -358678  11 (12)A> 33179357 112
1793163         220592401850                   36  11179358 (12)A> 112
1793164         220592401858                   38  11179359 (11)C> 11
1793165         220592401861                   35  11179359 <C(33) 31
1793166         220592760579              -358683  <C(33) 33179359 31
1793167         220592760590              -358680  01 (11)B> 33179359 31
1793168         220594554180                   38  01 11179359 (11)B> 31
1793169         220594554188                   40  01 11179360 (11)B>
1793170         220594554193                   37  01 11179360 <B(21) 20
1793171         220595630353              -358683  01 <B(21) 11179360 20
1793172         220595630357              -358685  <A(22) 11179361 20
1793173         220595630364              -358682  01 (11)B> 11179361 20
1793174         220595630369              -358685  01 <C(33) 33 11179360 20
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 <C(33) 331+V(1) 112
    1                   13                    3  11 (12)A> 331+V(1) 112
    2           23+10*V(1)             5+2*V(1)  112+V(1) (12)A> 112
    3           31+10*V(1)             7+2*V(1)  113+V(1) (11)C> 11
    4           34+10*V(1)             4+2*V(1)  113+V(1) <C(33) 31
    5           40+12*V(1)                   -2  <C(33) 333+V(1) 31
    6           51+12*V(1)                    1  01 (11)B> 333+V(1) 31
    7           81+22*V(1)             7+2*V(1)  01 113+V(1) (11)B> 31
    8           89+22*V(1)             9+2*V(1)  01 114+V(1) (11)B>
    9           94+22*V(1)             6+2*V(1)  01 114+V(1) <B(21) 20
   10          118+28*V(1)                   -2  01 <B(21) 114+V(1) 20
   11          122+28*V(1)                   -4  <A(22) 115+V(1) 20
   12          129+28*V(1)                   -1  01 (11)B> 115+V(1) 20
   13          134+28*V(1)                   -4  01 <C(33) 33 114+V(1) 20
<< Success! ==> defined new CTR 19 (PPA)
1793174         220595630369              -358685  01 <C(33) 33 11179360 20
== Executing  PA-CTR  2, V(1)=179356, V(2)=0, repcount=59786, factor=4/3
2391034         392168417021              -478257  01 <C(33) 33239145 112 20
== Executing PPA-CTR  3 (once), V(1)=239144
2391047         392175113193              -478261  01 <C(33) 33 11239148 12
== Executing  PA-CTR  2, V(1)=239144, V(2)=0, repcount=79715, factor=4/3
3188197         697194516603              -637691  01 <C(33) 33318861 113 12
== Executing PPA-CTR  4 (once), V(1)=318860
3188220         697207271277              -637697  01 <C(33) 333 11318865 20
== Executing  PA-CTR  2, V(1)=318861, V(2)=2, repcount=106288, factor=4/3
4251100        1239480781965              -850273  01 <C(33) 33425155 11 20
== Executing PPA-CTR  9 (once), V(1)=425151
4251113        1239487584535              -850277  01 <C(33) 333 11425155 10
== Executing  PA-CTR  2, V(1)=425151, V(2)=2, repcount=141718, factor=4/3
5668293        2203533632923             -1133713  01 <C(33) 33566875 11 10
== Executing PPA-CTR 10 (once), V(1)=566874
5668308        2203549505537             -1133717  01 <C(33) 33 11566878 12
== Executing  PA-CTR  2, V(1)=566874, V(2)=0, repcount=188959, factor=4/3
7557898        3917423886011             -1511635  01 <C(33) 33755837 11 12
== Executing PPA-CTR 11 (once), V(1)=755835
7557912        3917445049551             -1511639  01 <C(33) 33 11755839 12 22
== Executing  PA-CTR  7, V(1)=755835, V(2)=0, repcount=251946, factor=4/3
10077372        6964344426603             -2015531  01 <C(33) 331007785 11 12 22
10077373        6964344426616             -2015528  11 (12)A> 331007785 11 12 22
10077374        6964354504466                   42  111007786 (12)A> 11 12 22
10077375        6964354504474                   44  111007787 (11)C> 12 22
10077376        6964354504477                   41  111007787 <C(33) 32 22
10077377        6964356520051             -2015533  <C(33) 331007787 32 22
10077378        6964356520062             -2015530  01 (11)B> 331007787 32 22
10077379        6964366597932                   44  01 111007787 (11)B> 32 22
10077380        6964366597934                   46  01 111007788 (22)A> 22
10077381        6964366597936                   48  01 111007788 22 (22)A>
10077382        6964366597941                   45  01 111007788 22 <B(00) 22
10077383        6964366597943                   43  01 111007788 <B(00) 00 22
10077384        6964366597953                   41  01 111007787 <B(21) 12 00 22
10077385        6964372644675             -2015533  01 <B(21) 111007787 12 00 22
10077386        6964372644679             -2015535  <A(22) 111007788 12 00 22
10077387        6964372644686             -2015532  01 (11)B> 111007788 12 00 22
10077388        6964372644691             -2015535  01 <C(33) 33 111007787 12 00 22
>> Try to prove a PPA-CTR with 2 Vars...
    0                    0                    0  01 <C(33) 332+V(2) 11 12 221+V(1)
    1                   13                    3  11 (12)A> 332+V(2) 11 12 221+V(1)
    2           33+10*V(2)             7+2*V(2)  113+V(2) (12)A> 11 12 221+V(1)
    3           41+10*V(2)             9+2*V(2)  114+V(2) (11)C> 12 221+V(1)
    4           44+10*V(2)             6+2*V(2)  114+V(2) <C(33) 32 221+V(1)
    5           52+12*V(2)                   -2  <C(33) 334+V(2) 32 221+V(1)
    6           63+12*V(2)                    1  01 (11)B> 334+V(2) 32 221+V(1)
    7          103+22*V(2)             9+2*V(2)  01 114+V(2) (11)B> 32 221+V(1)
    8          105+22*V(2)            11+2*V(2)  01 115+V(2) (22)A> 221+V(1)
    9   107+2*V(1)+22*V(2)     13+2*V(1)+2*V(2)  01 115+V(2) 221+V(1) (22)A>
   10   112+2*V(1)+22*V(2)     10+2*V(1)+2*V(2)  01 115+V(2) 221+V(1) <B(00) 22
   11   114+4*V(1)+22*V(2)             8+2*V(2)  01 115+V(2) <B(00) 001+V(1) 22
   12   124+4*V(1)+22*V(2)             6+2*V(2)  01 114+V(2) <B(21) 12 001+V(1) 22
   13   148+4*V(1)+28*V(2)                   -2  01 <B(21) 114+V(2) 12 001+V(1) 22
   14   152+4*V(1)+28*V(2)                   -4  <A(22) 115+V(2) 12 001+V(1) 22
   15   159+4*V(1)+28*V(2)                   -1  01 (11)B> 115+V(2) 12 001+V(1) 22
   16   164+4*V(1)+28*V(2)                   -4  01 <C(33) 33 114+V(2) 12 001+V(1) 22
<< Success! ==> defined new CTR 20 (PPA)
10077388        6964372644691             -2015535  01 <C(33) 33 111007787 12 00 22
== Executing  PA-CTR 12, V(1)=1007783, V(2)=0, repcount=335928, factor=4/3
13436668       12381076601635             -2687391  01 <C(33) 331343713 113 12 00 22
13436669       12381076601648             -2687388  11 (12)A> 331343713 113 12 00 22
13436670       12381090038778                   38  111343714 (12)A> 113 12 00 22
13436671       12381090038786                   40  111343715 (11)C> 112 12 00 22
13436672       12381090038789                   37  111343715 <C(33) 31 11 12 00 22
13436673       12381092726219             -2687393  <C(33) 331343715 31 11 12 00 22
13436674       12381092726230             -2687390  01 (11)B> 331343715 31 11 12 00 22
13436675       12381106163380                   40  01 111343715 (11)B> 31 11 12 00 22
13436676       12381106163388                   42  01 111343716 (11)B> 11 12 00 22
13436677       12381106163393                   39  01 111343716 <C(33) 33 12 00 22
13436678       12381108850825             -2687393  01 <C(33) 331343717 12 00 22
13436679       12381108850838             -2687390  11 (12)A> 331343717 12 00 22
13436680       12381122288008                   44  111343718 (12)A> 12 00 22
13436681       12381122288018                   46  111343719 (11)B> 00 22
13436682       12381122288023                   43  111343719 <B(21) 20 22
13436683       12381130350337             -2687395  <B(21) 111343719 20 22
13436684       12381130350346             -2687392  11 (11)C> 111343719 20 22
13436685       12381130350349             -2687395  11 <C(33) 31 111343718 20 22
13436686       12381130350351             -2687397  <C(33) 33 31 111343718 20 22
13436687       12381130350362             -2687394  01 (11)B> 33 31 111343718 20 22
13436688       12381130350372             -2687392  01 11 (11)B> 31 111343718 20 22
13436689       12381130350380             -2687390  01 112 (11)B> 111343718 20 22
13436690       12381130350385             -2687393  01 112 <C(33) 33 111343717 20 22
13436691       12381130350389             -2687397  01 <C(33) 333 111343717 20 22
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 <C(33) 331+V(1) 113 12 00 [*]*
    1                   13                    3  11 (12)A> 331+V(1) 113 12 00 [*]*
    2           23+10*V(1)             5+2*V(1)  112+V(1) (12)A> 113 12 00 [*]*
    3           31+10*V(1)             7+2*V(1)  113+V(1) (11)C> 112 12 00 [*]*
    4           34+10*V(1)             4+2*V(1)  113+V(1) <C(33) 31 11 12 00 [*]*
    5           40+12*V(1)                   -2  <C(33) 333+V(1) 31 11 12 00 [*]*
    6           51+12*V(1)                    1  01 (11)B> 333+V(1) 31 11 12 00 [*]*
    7           81+22*V(1)             7+2*V(1)  01 113+V(1) (11)B> 31 11 12 00 [*]*
    8           89+22*V(1)             9+2*V(1)  01 114+V(1) (11)B> 11 12 00 [*]*
    9           94+22*V(1)             6+2*V(1)  01 114+V(1) <C(33) 33 12 00 [*]*
   10          102+24*V(1)                   -2  01 <C(33) 335+V(1) 12 00 [*]*
   11          115+24*V(1)                    1  11 (12)A> 335+V(1) 12 00 [*]*
   12          165+34*V(1)            11+2*V(1)  116+V(1) (12)A> 12 00 [*]*
   13          175+34*V(1)            13+2*V(1)  117+V(1) (11)B> 00 [*]*
   14          180+34*V(1)            10+2*V(1)  117+V(1) <B(21) 20 [*]*
   15          222+40*V(1)                   -4  <B(21) 117+V(1) 20 [*]*
   16          231+40*V(1)                   -1  11 (11)C> 117+V(1) 20 [*]*
   17          234+40*V(1)                   -4  11 <C(33) 31 116+V(1) 20 [*]*
   18          236+40*V(1)                   -6  <C(33) 33 31 116+V(1) 20 [*]*
   19          247+40*V(1)                   -3  01 (11)B> 33 31 116+V(1) 20 [*]*
   20          257+40*V(1)                   -1  01 11 (11)B> 31 116+V(1) 20 [*]*
   21          265+40*V(1)                    1  01 112 (11)B> 116+V(1) 20 [*]*
   22          270+40*V(1)                   -2  01 112 <C(33) 33 115+V(1) 20 [*]*
   23          274+40*V(1)                   -6  01 <C(33) 333 115+V(1) 20 [*]*
<< Success! ==> defined new CTR 21 (PPA)
13436691       12381130350389             -2687397  01 <C(33) 333 111343717 20 22
== Executing  PA-CTR  7, V(1)=1343713, V(2)=2, repcount=447905, factor=4/3
17915741       22010882709899             -3583207  01 <C(33) 331791623 112 20 22
== Executing PPA-CTR 17 (once), V(1)=1791622
17915754       22010932875455             -3583211  01 <C(33) 33 111791626 12 22
== Executing  PA-CTR  7, V(1)=1791622, V(2)=0, repcount=597208, factor=4/3
23887834       39130520097359             -4777627  01 <C(33) 332388833 112 12 22
== Executing PPA-CTR 15 (once), V(1)=2388832
23887847       39130586984793             -4777631  01 <C(33) 33 112388837 22
== Executing  PA-CTR  2, V(1)=2388833, V(2)=0, repcount=796278, factor=4/3
31850627       69565445341437             -6370187  01 <C(33) 333185113 113 22
== Executing PPA-CTR 16 (once), V(1)=3185112
31850651       69565572746185             -6370193  01 <C(33) 333 113185116 20 22
== Executing  PA-CTR  7, V(1)=3185112, V(2)=2, repcount=1061705, factor=4/3
42467701      123672121377295             -8493603  01 <C(33) 334246823 11 20 22
42467702      123672121377308             -8493600  11 (12)A> 334246823 11 20 22
42467703      123672163845538                   46  114246824 (12)A> 11 20 22
42467704      123672163845546                   48  114246825 (11)C> 20 22
42467705      123672163845551                   45  114246825 <B(21) 10 22
42467706      123672189326501             -8493605  <B(21) 114246825 10 22
42467707      123672189326510             -8493602  11 (11)C> 114246825 10 22
42467708      123672189326513             -8493605  11 <C(33) 31 114246824 10 22
42467709      123672189326515             -8493607  <C(33) 33 31 114246824 10 22
42467710      123672189326526             -8493604  01 (11)B> 33 31 114246824 10 22
42467711      123672189326536             -8493602  01 11 (11)B> 31 114246824 10 22
42467712      123672189326544             -8493600  01 112 (11)B> 114246824 10 22
42467713      123672189326549             -8493603  01 112 <C(33) 33 114246823 10 22
42467714      123672189326553             -8493607  01 <C(33) 333 114246823 10 22
>> Try to prove a PPA-CTR with 1 Vars...
    0                    0                    0  01 <C(33) 334+V(1) 11 20 [*]*
    1                   13                    3  11 (12)A> 334+V(1) 11 20 [*]*
    2           53+10*V(1)            11+2*V(1)  115+V(1) (12)A> 11 20 [*]*
    3           61+10*V(1)            13+2*V(1)  116+V(1) (11)C> 20 [*]*
    4           66+10*V(1)            10+2*V(1)  116+V(1) <B(21) 10 [*]*
    5          102+16*V(1)                   -2  <B(21) 116+V(1) 10 [*]*
    6          111+16*V(1)                    1  11 (11)C> 116+V(1) 10 [*]*
    7          114+16*V(1)                   -2  11 <C(33) 31 115+V(1) 10 [*]*
    8          116+16*V(1)                   -4  <C(33) 33 31 115+V(1) 10 [*]*
    9          127+16*V(1)                   -1  01 (11)B> 33 31 115+V(1) 10 [*]*
   10          137+16*V(1)                    1  01 11 (11)B> 31 115+V(1) 10 [*]*
   11          145+16*V(1)                    3  01 112 (11)B> 115+V(1) 10 [*]*
   12          150+16*V(1)                    0  01 112 <C(33) 33 114+V(1) 10 [*]*
   13          154+16*V(1)                   -4  01 <C(33) 333 114+V(1) 10 [*]*
<< Success! ==> defined new CTR 22 (PPA)
42467714      123672189326553             -8493607  01 <C(33) 333 114246823 10 22
== Executing  PA-CTR  7, V(1)=4246819, V(2)=2, repcount=1415607, factor=4/3
56623784      219861606284019            -11324821  01 <C(33) 335662431 112 10 22
56623785      219861606284032            -11324818  11 (12)A> 335662431 112 10 22
56623786      219861662908342                   44  115662432 (12)A> 112 10 22
56623787      219861662908350                   46  115662433 (11)C> 11 10 22
56623788      219861662908353                   43  115662433 <C(33) 31 10 22
56623789      219861674233219            -11324823  <C(33) 335662433 31 10 22
56623790      219861674233230            -11324820  01 (11)B> 335662433 31 10 22
56623791      219861730857560                   46  01 115662433 (11)B> 31 10 22
56623792      219861730857568                   48  01 115662434 (11)B> 10 22
56623793      219861730857570                   50  01 115662435 (11)B> 22
56623794      219861730857576                   52  01 115662436 (11)B>
56623795      219861730857581                   49  01 115662436 <B(21) 20
56623796      219861764832197            -11324823  01 <B(21) 115662436 20
56623797      219861764832201            -11324825  <A(22) 115662437 20
56623798      219861764832208            -11324822  01 (11)B> 115662437 20
56623799      219861764832213            -11324825  01 <C(33) 33 115662436 20
>> Try to prove a PPA-CTR with 3 Vars...
    0                    0                    0  01 <C(33) 331+V(3) 112 101+V(2) 221+V(1)
    1                   13                    3  11 (12)A> 331+V(3) 112 101+V(2) 221+V(1)
    2           23+10*V(3)             5+2*V(3)  112+V(3) (12)A> 112 101+V(2) 221+V(1)
    3           31+10*V(3)             7+2*V(3)  113+V(3) (11)C> 11 101+V(2) 221+V(1)
    4           34+10*V(3)             4+2*V(3)  113+V(3) <C(33) 31 101+V(2) 221+V(1)
    5           40+12*V(3)                   -2  <C(33) 333+V(3) 31 101+V(2) 221+V(1)
    6           51+12*V(3)                    1  01 (11)B> 333+V(3) 31 101+V(2) 221+V(1)
    7           81+22*V(3)             7+2*V(3)  01 113+V(3) (11)B> 31 101+V(2) 221+V(1)
    8           89+22*V(3)             9+2*V(3)  01 114+V(3) (11)B> 101+V(2) 221+V(1)
    9    91+2*V(2)+22*V(3)     11+2*V(2)+2*V(3)  01 115+V(2)+V(3) (11)B> 221+V(1)
   10 97+6*V(1)+2*V(2)+22*V(3) 13+2*V(1)+2*V(2)+2*V(3)  01 116+V(1)+V(2)+V(3) (11)B>
   11 102+6*V(1)+2*V(2)+22*V(3) 10+2*V(1)+2*V(2)+2*V(3)  01 116+V(1)+V(2)+V(3) <B(21) 20
   12 138+12*V(1)+8*V(2)+28*V(3)                   -2  01 <B(21) 116+V(1)+V(2)+V(3) 20
   13 142+12*V(1)+8*V(2)+28*V(3)                   -4  <A(22) 117+V(1)+V(2)+V(3) 20
   14 149+12*V(1)+8*V(2)+28*V(3)                   -1  01 (11)B> 117+V(1)+V(2)+V(3) 20
   15 154+12*V(1)+8*V(2)+28*V(3)                   -4  01 <C(33) 33 116+V(1)+V(2)+V(3) 20
<< Success! ==> defined new CTR 23 (PPA)
56623799      219861764832213            -11324825  01 <C(33) 33 115662436 20
== Executing  PA-CTR  2, V(1)=5662432, V(2)=0, repcount=1887478, factor=4/3
75498579      390865380379257            -15099781  01 <C(33) 337549913 112 20
== Executing PPA-CTR  3 (once), V(1)=7549912
75498592      390865591776933            -15099785  01 <C(33) 33 117549916 12
== Executing  PA-CTR  2, V(1)=7549912, V(2)=0, repcount=2516638, factor=4/3
100664972      694872135181497            -20133061  01 <C(33) 3310066553 112 12

Lines:       500
Top steps:   499
Macro steps: 100664972
Basic steps: 694872135181497
Tape index:  -20133061
nonzeros:    20133115
log10(nonzeros):    7.304
log10(steps   ):   14.842

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

To the BB simulations page of Heiner Marxen.
To the busy beaver page of Heiner Marxen.
To the home page of Heiner Marxen.
Input to awk program:
    gohalt 1
    nbs 4
    T 3-state 4-symbol #g (T.J. & S. Ligocki)
    : >1.4x10^2355 >3.4x10^4710
    5T  1RB 2LB 2RA 1LA  2LA 1RC 0LB 2RA  1RB 3LC 1LA 1RH
    L 10
    M	500
    pref	sim
    machv Lig34_g  	just simple
    machv Lig34_g-r	with repetitions reduced
    machv Lig34_g-1	with tape symbol exponents
    machv Lig34_g-m	as 2-bck-macro machine
    machv Lig34_g-a	as 2-bck-macro machine with pure additive config-TRs
    iam	Lig34_g-a
    mtype	2 0
    mmtyp	3
    r	1
    H	1
    mac	0
    E	2
    sympr	
    HM	1
    date	Tue Jul  6 22:13:52 CEST 2010
    edate	Tue Jul  6 22:13:54 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:13:52 CEST 2010
Ready: Tue Jul 6 22:13:54 CEST 2010