PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran10x10c.opb
MD5SUM	31a8734340f0544712ef974997c104b2
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2677632
Optimality of the best value was proved	NO
Number of terms in the objective function	2100
Biggest coefficient in the objective function	4718592
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	515723936
Number of bits of the sum of numbers in the objective function	29
Biggest number in a constraint	4718592
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	515723936
Number of bits of the biggest sum of numbers	29
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.05
Number of variables	2100
Total number of constraints	120
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	120
Minimum length of a constraint	21
Maximum length of a constraint	200
Trace number 14816

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-04-21 01:34:52 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19219 boxname=wulflinc4 idbench=1479 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  31a8734340f0544712ef974997c104b2  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-ran10x10c.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-ran10x10c.opb
IDLAUNCH: 19219
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        808960 kB
Buffers:         32260 kB
Cached:         170720 kB
SwapCached:          0 kB
Active:          14780 kB
Inactive:       191024 kB
HighTotal:      131008 kB
HighFree:        30940 kB
LowTotal:       903652 kB
LowFree:        778020 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            14244 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 01:54:54 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 19219 7 1200.23 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 138]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost: 1972     Base: 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost: 2017     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 132]---> Sorter-cost: 1972     Base: 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 1972     Base: 2 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost: 1442     Base: 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost: 1972     Base: 2 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost: 1934     Base: 2 2 2 2 2 2 2 2
c ---[ 122]---> Sorter-cost: 1972     Base: 2 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost: 2017     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 118]---> Sorter-cost: 1780     Base: 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost: 2045     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Sorter-cost: 1780     Base: 2 2 2 2 2 2 2
c ---[ 112]---> Sorter-cost: 2045     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Adder-cost: 178   maxlim: 8182   bits: 14/13
c ---[ 108]---> Adder-cost: 178   maxlim: 8438   bits: 14/14
c ---[ 106]---> Sorter-cost: 2013     Base: 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 2013     Base: 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 2045     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 100]---> Sorter-cost: 1780     Base: 2 2 2 2 2 2 2
c ---[  99]---> BDD-cost:   10
c ---[  98]---> BDD-cost:   11
c ---[  97]---> BDD-cost:   10
c ---[  96]---> BDD-cost:   15
c ---[  95]---> BDD-cost:   10
c ---[  94]---> BDD-cost:   15
c ---[  93]---> BDD-cost:   12
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   15
c ---[  90]---> BDD-cost:   15
c ---[  89]---> BDD-cost:   15
c ---[  88]---> BDD-cost:   10
c ---[  87]---> BDD-cost:   10
c ---[  86]---> BDD-cost:   10
c ---[  85]---> BDD-cost:   13
c ---[  84]---> BDD-cost:   10
c ---[  83]---> BDD-cost:   13
c ---[  82]---> BDD-cost:   12
c ---[  81]---> BDD-cost:   11
c ---[  80]---> BDD-cost:   15
c ---[  79]---> BDD-cost:   13
c ---[  78]---> BDD-cost:   13
c ---[  77]---> BDD-cost:   10
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   10
c ---[  74]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   10
c ---[  72]---> BDD-cost:   15
c ---[  71]---> BDD-cost:   12
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   15
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:   15
c ---[  66]---> BDD-cost:   10
c ---[  65]---> BDD-cost:   11
c ---[  64]---> BDD-cost:   10
c ---[  63]---> BDD-cost:   14
c ---[  62]---> BDD-cost:   10
c ---[  61]---> BDD-cost:   14
c ---[  60]---> BDD-cost:   12
c ---[  59]---> BDD-cost:   11
c ---[  58]---> BDD-cost:   14
c ---[  57]---> BDD-cost:   14
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   10
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:    9
c ---[  52]---> BDD-cost:    9
c ---[  51]---> BDD-cost:    9
c ---[  50]---> BDD-cost:    9
c ---[  49]---> BDD-cost:    9
c ---[  48]---> BDD-cost:    9
c ---[  47]---> BDD-cost:    9
c ---[  46]---> BDD-cost:    9
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:   11
c ---[  42]---> BDD-cost:   10
c ---[  41]---> BDD-cost:   15
c ---[  40]---> BDD-cost:   10
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   12
c ---[  37]---> BDD-cost:   11
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   13
c ---[  34]---> BDD-cost:   15
c ---[  33]---> BDD-cost:   10
c ---[  32]---> BDD-cost:   11
c ---[  31]---> BDD-cost:   10
c ---[  30]---> BDD-cost:   13
c ---[  29]---> BDD-cost:   10
c ---[  28]---> BDD-cost:   13
c ---[  27]---> BDD-cost:   12
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:   13
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   13
c ---[  22]---> BDD-cost:   10
c ---[  21]---> BDD-cost:   11
c ---[  20]---> BDD-cost:   10
c ---[  19]---> BDD-cost:   15
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   12
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   15
c ---[  13]---> BDD-cost:   15
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   10
c ---[  10]---> BDD-cost:   10
c ---[   9]---> BDD-cost:   10
c ---[   8]---> BDD-cost:   17
c ---[   7]---> BDD-cost:   10
c ---[   6]---> BDD-cost:   17
c ---[   5]---> BDD-cost:   12
c ---[   4]---> BDD-cost:   11
c ---[   3]---> BDD-cost:   15
c ---[   2]---> BDD-cost:   13
c ---[   1]---> BDD-cost:   17
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   91521   218607 |   30507       0        0     nan |  0.000 % |
c |       101 |   91521   218607 |   33557     101      642     6.4 |  6.867 % |
c |       252 |   91175   217815 |   36913     235     1183     5.0 |  7.174 % |
c |       477 |   91099   217646 |   40604     453     2086     4.6 |  7.238 % |
c |       814 |   90963   217336 |   44665     781     3761     4.8 |  7.358 % |
c |      1320 |   90963   217336 |   49131    1287     6695     5.2 |  7.358 % |
c |      2081 |   90952   217312 |   54045    2046    15341     7.5 |  7.367 % |
c |      3220 |   90899   217192 |   59449    3181    23553     7.4 |  7.416 % |
c ==============================================================================
c [1mFound solution: 10107013[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4060   maxlim: 2874907   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4823 |  119071   317977 |   39690    4758    65984    13.9 |  7.416 % |
c |      4923 |  119038   317866 |   43659    4854    66482    13.7 |  6.730 % |
c |      5074 |  119022   317831 |   48024    5000    67119    13.4 |  6.744 % |
c |      5300 |  119022   317831 |   52827    5226    68603    13.1 |  6.744 % |
c |      5637 |  119006   317779 |   58110    5561    70687    12.7 |  6.752 % |
c |      6143 |  119006   317779 |   63921    6067    73554    12.1 |  6.752 % |
c |      6902 |  118895   317524 |   70313    6819    78215    11.5 |  6.839 % |
c |      8043 |  118868   317444 |   77344    7957    84971    10.7 |  6.855 % |
c |      9752 |  118826   317342 |   85079    9661   166486    17.2 |  6.888 % |
c |     12314 |  118774   317217 |   93586   12218   198346    16.2 |  6.929 % |
c ==============================================================================
c [1mFound solution: 9973742[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3008178   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12622 |  118807   317467 |   39602   12526   200724    16.0 |  6.929 % |
c |     12722 |  118807   317467 |   43562   12626   201414    16.0 |  6.959 % |
c |     12872 |  118727   317283 |   47918   12775   202250    15.8 |  7.029 % |
c |     13098 |  118727   317283 |   52710   13001   203741    15.7 |  7.029 % |
c |     13435 |  118727   317283 |   57981   13338   206757    15.5 |  7.029 % |
c |     13941 |  118727   317283 |   63779   13844   216461    15.6 |  7.029 % |
c |     14700 |  118579   316932 |   70157   14591   220462    15.1 |  7.157 % |
c |     15839 |  118579   316932 |   77173   15730   251933    16.0 |  7.157 % |
c |     17547 |  118453   316649 |   84890   17430   287900    16.5 |  7.258 % |
c |     20110 |  118445   316623 |   93379   19992   497092    24.9 |  7.261 % |
c ==============================================================================
c [1mFound solution: 3754669[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 9227251   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22201 |  118431   316761 |   39477   22082   604335    27.4 |  7.261 % |
c |     22301 |  118380   316647 |   43424   22179   604829    27.3 |  7.364 % |
c |     22452 |  118380   316647 |   47767   22330   605695    27.1 |  7.364 % |
c |     22677 |  118380   316647 |   52543   22555   606999    26.9 |  7.364 % |
c |     23016 |  118380   316647 |   57798   22894   612429    26.8 |  7.364 % |
c |     23522 |  118380   316647 |   63578   23400   627934    26.8 |  7.364 % |
c |     24281 |  118380   316647 |   69935   24159   647058    26.8 |  7.364 % |
c |     25422 |  118337   316552 |   76929   25296   724008    28.6 |  7.397 % |
c |     27130 |  118290   316447 |   84622   26995   832379    30.8 |  7.435 % |
c |     29693 |  118290   316447 |   93084   29558   999206    33.8 |  7.435 % |
c |     33537 |  118067   315927 |  102393   33358  1167125    35.0 |  7.617 % |
c |     39304 |  117853   315435 |  112632   39096  1385920    35.4 |  7.783 % |
c |     47954 |  117382   314355 |  123895   47676  2119946    44.5 |  8.151 % |
c |     60928 |  117349   314282 |  136285   60647  3114519    51.4 |  8.175 % |
c ==============================================================================
c [1mFound solution: 3341769[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 9640151   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     68046 |  117346   314353 |   39115   67760  4697785    69.3 |  8.175 % |
c |     68146 |  117346   314353 |   43026   19524  1884623    96.5 |  8.203 % |
c |     68296 |  117346   314353 |   47329   19674  1886618    95.9 |  8.203 % |
c |     68521 |  117346   314353 |   52062   19899  1907836    95.9 |  8.203 % |
c |     68858 |  117346   314353 |   57268   20236  1934374    95.6 |  8.203 % |
c |     69364 |  117299   314243 |   62995   20741  1951395    94.1 |  8.244 % |
c |     70124 |  117234   314088 |   69294   21495  1978182    92.0 |  8.293 % |
c |     71264 |  117234   314088 |   76224   22635  2111894    93.3 |  8.293 % |
c |     72975 |  117234   314088 |   83846   24346  2175908    89.4 |  8.293 % |
c |     75537 |  117171   313941 |   92231   26905  2305933    85.7 |  8.347 % |
c |     79383 |  117080   313725 |  101454   30737  2463292    80.1 |  8.415 % |
c |     85150 |  116913   313349 |  111599   36478  2960182    81.1 |  8.554 % |
c |     93799 |  116731   312932 |  122759   45116  3509007    77.8 |  8.701 % |
c |    106774 |  116354   312072 |  135035   58049  5225991    90.0 |  8.995 % |
c |    126235 |  116292   311920 |  148539   77502  6497502    83.8 |  9.044 % |
c |    155427 |  115462   309992 |  163393  106636  8534876    80.0 |  9.751 % |
c |    199217 |  115170   309319 |  179732  150390 18763913   124.8 |  9.999 % |
c |    264901 |  114897   308683 |  197705   46705  2023468    43.3 | 10.211 % |
c ==============================================================================
c [1mFound solution: 3338727[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 9643193   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    281774 |  114900   308789 |   38300   63575  4054558    63.8 | 10.211 % |
c |    281877 |  114872   308725 |   42130   18625  1713766    92.0 | 10.254 % |
c |    282027 |  114759   308467 |   46343   18770  1714454    91.3 | 10.352 % |
c |    282252 |  114759   308467 |   50977   18995  1715684    90.3 | 10.352 % |
c |    282591 |  114759   308467 |   56075   19334  1720040    89.0 | 10.352 % |
c |    283098 |  114759   308467 |   61682   19841  1776974    89.6 | 10.352 % |
c |    283857 |  114759   308467 |   67850   20600  1790487    86.9 | 10.352 % |
c |    284996 |  114740   308424 |   74635   21738  1854893    85.3 | 10.369 % |
c |    286704 |  114642   308199 |   82099   23433  1893368    80.8 | 10.450 % |
c |    289269 |  114515   307900 |   90309   25990  2036394    78.4 | 10.559 % |
c |    293113 |  114515   307900 |   99340   29834  2704748    90.7 | 10.559 % |
c |    298880 |  114468   307790 |  109274   35600  2976593    83.6 | 10.600 % |
c |    307529 |  114260   307305 |  120201   44230  3855098    87.2 | 10.782 % |
c |    320504 |  114187   307138 |  132221   57182  4619114    80.8 | 10.837 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 -X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 X8_bit0 X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X12_bit_7 -X12_bit_6 -X12_bit_5 -X12_bit_4 -X12_bit_3 -X12_bit_2 -X12_bit_1 -X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X13_bit_7 -X13_bit_6 -X13_bit_5 -X13_bit_4 -X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 -X14_bit_3 -X14_bit_2 -X14_bit_1 -X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X15_bit_7 -X15_bit_6 -X15_bit_5 -X15_bit_4 -X15_bit_3 -X15_bit_2 -X15_bit_1 -X15_bit0 -X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 -X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 -X16_bit_2 -X16_bit_1 -X16_bit0 -X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X17_bit_7 -X17_bit_6 -X17_bit_5 -X17_bit_4 -X17_bit_3 -X17_bit_2 -X17_bit_1 X17_bit0 -X17_bit1 -X17_bit2 X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 -X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 -X19_bit_7 -X19_bit_6 -X19_bit_5 -X19_bit_4 -X19_bit_3 -X19_bit_2 -X19_bit_1 -X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 X20_bit_7 -X20_bit_6 X20_bit_5 X20_bit_4 X20_bit_3 X20_bit_2 X20_bit_1 X20_bit0 -X20_bit1 -X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 -X21_bit_7 -X21_bit_6 -X21_bit_5 -X21_bit_4 -X21_bit_3 -X21_bit_2 -X21_bit_1 -X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X22_bit_7 -X22_bit_6 -X22_bit_5 -X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X23_bit_7 -X23_bit_6 -X23_bit_5 -X23_bit_4 -X23_bit_3 -X23_bit_2 -X23_bit_1 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 X24_bit_7 X24_bit_6 X24_bit_5 -X24_bit_4 X24_bit_3 X24_bit_2 X24_bit_1 X24_bit0 X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 X25_bit_7 X25_bit_6 X25_bit_5 X25_bit_4 X25_bit_3 -X25_bit_2 -X25_bit_1 X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 X26_bit_7 X26_bit_6 X26_bit_5 X26_bit_4 -X26_bit_3 X26_bit_2 X26_bit_1 X26_bit0 X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 X27_bit_7 X27_bit_6 X27_bit_5 X27_bit_4 X27_bit_3 X27_bit_2 X27_bit_1 X27_bit0 -X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 -X28_bit_7 -X28_bit_6 -X28_bit_5 -X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 -X28_bit0 -X28_bit1 -X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 X29_bit_7 X29_bit_6 X29_bit_5 X29_bit_4 X29_bit_3 X29_bit_2 X29_bit_1 X29_bit0 -X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 X30_bit_7 -X30_bit_6 -X30_bit_5 -X30_bit_4 -X30_bit_3 -X30_bit_2 -X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X31_bit_7 -X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 -X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X32_bit_7 -X32_bit_6 -X32_bit_5 -X32_bit_4 -X32_bit_3 -X32_bit_2 -X32_bit_1 -X32_bit0 -X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 -X33_bit_7 -X33_bit_6 -X33_bit_5 -X33_bit_4 -X33_bit_3 -X33_bit_2 -X33_bit_1 -X33_bit0 -X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 X34_bit_7 -X34_bit_6 X34_bit_5 X34_bit_4 X34_bit_3 X34_bit_2 X34_bit_1 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X35_bit_7 -X35_bit_6 -X35_bit_5 -X35_bit_4 -X35_bit_3 -X35_bit_2 -X35_bit_1 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 -X36_bit_7 -X36_bit_6 -X36_bit_5 -X36_bit_4 -X36_bit_3 -X36_bit_2 -X36_bit_1 -X36_bit0 -X36_bit1 -X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 -X37_bit_7 -X37_bit_6 -X37_bit_5 -X37_bit_4 -X37_bit_3 -X37_bit_2 -X37_bit_1 -X37_bit0 -X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 -X38_bit_7 X38_bit_6 -X38_bit_5 -X38_bit_4 -X38_bit_3 -X38_bit_2 -X38_bit_1 -X38_bit0 X38_bit1 -X38_bit2 X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 -X39_bit_7 -X39_bit_6 -X39_bit_5 -X39_bit_4 -X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X40_bit_7 X40_bit_6 -X40_bit_5 -X40_bit_4 -X40_bit_3 -X40_bit_2 -X40_bit_1 -X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 -X41_bit_7 -X41_bit_6 -X41_bit_5 -X41_bit_4 -X41_bit_3 -X41_bit_2 -X41_bit_1 -X41_bit0 -X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X42_bit_7 -X42_bit_6 -X42_bit_5 -X42_bit_4 -X42_bit_3 -X42_bit_2 -X42_bit_1 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 -X43_bit_7 -X43_bit_6 -X43_bit_5 -X43_bit_4 -X43_bit_3 -X43_bit_2 -X43_bit_1 -X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 -X44_bit_7 -X44_bit_6 -X44_bit_5 -X44_bit_4 -X44_bit_3 -X44_bit_2 -X44_bit_1 -X44_bit0 -X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X45_bit_7 -X45_bit_6 -X45_bit_5 -X45_bit_4 -X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X46_bit_7 -X46_bit_6 -X46_bit_5 -X46_bit_4 -X46_bit_3 -X46_bit_2 -X46_bit_1 -X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 -X47_bit_7 -X47_bit_6 -X47_bit_5 -X47_bit_4 -X47_bit_3 -X47_bit_2 -X47_bit_1 -X47_bit0 -X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X48_bit_7 X48_bit_6 X48_bit_5 X48_bit_4 X48_bit_3 X48_bit_2 X48_bit_1 X48_bit0 -X48_bit1 -X48_bit2 X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X49_bit_7 -X49_bit_6 -X49_bit_5 -X49_bit_4 -X49_bit_3 -X49_bit_2 -X49_bit_1 -X49_bit0 -X49_bit1 -X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 -X50_bit_7 -X50_bit_6 -X50_bit_5 -X50_bit_4 -X50_bit_3 -X50_bit_2 -X50_bit_1 -X50_bit0 -X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 -X51_bit_7 -X51_bit_6 -X51_bit_5 -X51_bit_4 -X51_bit_3 -X51_bit_2 -X51_bit_1 -X51_bit0 -X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 -X52_bit_7 -X52_bit_6 -X52_bit_5 -X52_bit_4 -X52_bit_3 -X52_bit_2 -X52_bit_1 X52_bit0 -X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 -X53_bit_7 -X53_bit_6 -X53_bit_5 -X53_bit_4 -X53_bit_3 -X53_bit_2 -X53_bit_1 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X54_bit_7 -X54_bit_6 -X54_bit_5 -X54_bit_4 -X54_bit_3 -X54_bit_2 -X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X55_bit_7 -X55_bit_6 -X55_bit_5 -X55_bit_4 -X55_bit_3 -X55_bit_2 -X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 -X56_bit_7 -X56_bit_6 -X56_bit_5 -X56_bit_4 -X56_bit_3 -X56_bit_2 -X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X57_bit_7 -X57_bit_6 -X57_bit_5 -X57_bit_4 -X57_bit_3 -X57_bit_2 -X57_bit_1 -X57_bit0 -X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 -X58_bit_7 -X58_bit_6 -X58_bit_5 -X58_bit_4 -X58_bit_3 -X58_bit_2 -X58_bit_1 -X58_bit0 -X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 -X59_bit_7 -X59_bit_6 -X59_bit_5 -X59_bit_4 -X59_bit_3 -X59_bit_2 -X59_bit_1 -X59_bit0 -X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 -X60_bit_7 -X60_bit_6 -X60_bit_5 -X60_bit_4 -X60_bit_3 -X60_bit_2 -X60_bit_1 -X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 -X61_bit_7 -X61_bit_6 -X61_bit_5 -X61_bit_4 -X61_bit_3 -X61_bit_2 -X61_bit_1 -X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 -X62_bit_7 -X62_bit_6 -X62_bit_5 -X62_bit_4 -X62_bit_3 -X62_bit_2 -X62_bit_1 -X62_bit0 -X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 -X63_bit_7 -X63_bit_6 X63_bit_5 X63_bit_4 -X63_bit_3 -X63_bit_2 -X63_bit_1 -X63_bit0 -X63_bit1 X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 -X64_bit_7 -X64_bit_6 -X64_bit_5 -X64_bit_4 -X64_bit_3 -X64_bit_2 -X64_bit_1 -X64_bit0 -X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 X65_bit_7 -X65_bit_6 -X65_bit_5 -X65_bit_4 -X65_bit_3 X65_bit_2 X65_bit_1 -X65_bit0 X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 X66_bit_7 -X66_bit_6 -X66_bit_5 -X66_bit_4 X66_bit_3 -X66_bit_2 -X66_bit_1 X66_bit0 X66_bit1 X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 X67_bit_7 -X67_bit_6 -X67_bit_5 -X67_bit_4 -X67_bit_3 -X67_bit_2 -X67_bit_1 X67_bit0 -X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 -X68_bit_7 -X68_bit_6 -X68_bit_5 -X68_bit_4 -X68_bit_3 -X68_bit_2 -X68_bit_1 -X68_bit0 -X68_bit1 -X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 X69_bit_7 -X69_bit_6 -X69_bit_5 -X69_bit_4 -X69_bit_3 -X69_bit_2 -X69_bit_1 -X69_bit0 -X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 -X70_bit_7 -X70_bit_6 -X70_bit_5 -X70_bit_4 -X70_bit_3 -X70_bit_2 -X70_bit_1 -X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 -X71_bit_7 -X71_bit_6 -X71_bit_5 -X71_bit_4 -X71_bit_3 -X71_bit_2 -X71_bit_1 -X71_bit0 X71_bit1 X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 -X72_bit_7 -X72_bit_6 -X72_bit_5 -X72_bit_4 -X72_bit_3 -X72_bit_2 -X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 -X73_bit_7 -X73_bit_6 -X73_bit_5 -X73_bit_4 -X73_bit_3 -X73_bit_2 -X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 -X74_bit_7 -X74_bit_6 -X74_bit_5 -X74_bit_4 -X74_bit_3 -X74_bit_2 -X74_bit_1 -X74_bit0 -X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 -X75_bit_7 -X75_bit_6 -X75_bit_5 -X75_bit_4 -X75_bit_3 -X75_bit_2 -X75_bit_1 -X75_bit0 -X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 -X76_bit_7 -X76_bit_6 -X76_bit_5 -X76_bit_4 -X76_bit_3 -X76_bit_2 -X76_bit_1 -X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 -X77_bit_7 -X77_bit_6 -X77_bit_5 -X77_bit_4 -X77_bit_3 -X77_bit_2 -X77_bit_1 -X77_bit0 -X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 -X78_bit_7 -X78_bit_6 -X78_bit_5 -X78_bit_4 -X78_bit_3 -X78_bit_2 -X78_bit_1 X78_bit0 -X78_bit1 -X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 -X79_bit_7 -X79_bit_6 -X79_bit_5 -X79_bit_4 -X79_bit_3 -X79_bit_2 -X79_bit_1 -X79_bit0 -X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 -X80_bit_7 -X80_bit_6 -X80_bit_5 -X80_bit_4 -X80_bit_3 -X80_bit_2 -X80_bit_1 -X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 -X81_bit_7 -X81_bit_6 -X81_bit_5 -X81_bit_4 -X81_bit_3 -X81_bit_2 -X81_bit_1 X81_bit0 X81_bit1 -X81_bit2 X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 -X82_bit_7 -X82_bit_6 -X82_bit_5 -X82_bit_4 -X82_bit_3 -X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 -X83_bit_7 -X83_bit_6 -X83_bit_5 -X83_bit_4 -X83_bit_3 -X83_bit_2 -X83_bit_1 -X83_bit0 -X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 -X84_bit_7 -X84_bit_6 -X84_bit_5 -X84_bit_4 -X84_bit_3 -X84_bit_2 -X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 -X85_bit_7 -X85_bit_6 -X85_bit_5 -X85_bit_4 -X85_bit_3 -X85_bit_2 -X85_bit_1 -X85_bit0 -X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 -X86_bit_7 -X86_bit_6 -X86_bit_5 -X86_bit_4 -X86_bit_3 -X86_bit_2 -X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X87_bit_7 -X87_bit_6 -X87_bit_5 -X87_bit_4 -X87_bit_3 -X87_bit_2 -X87_bit_1 -X87_bit0 -X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 -X88_bit_7 -X88_bit_6 -X88_bit_5 -X88_bit_4 -X88_bit_3 -X88_bit_2 -X88_bit_1 -X88_bit0 -X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 -X89_bit_7 -X89_bit_6 -X89_bit_5 -X89_bit_4 -X89_bit_3 -X89_bit_2 -X89_bit_1 -X89_bit0 -X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 -X90_bit_7 -X90_bit_6 -X90_bit_5 -X90_bit_4 -X90_bit_3 -X90_bit_2 -X90_bit_1 -X90_bit0 -X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 -X91_bit_7 -X91_bit_6 -X91_bit_5 -X91_bit_4 -X91_bit_3 -X91_bit_2 -X91_bit_1 -X91_bit0 -X91_bit1 -X91_bit2 -X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 -X92_bit_7 -X92_bit_6 -X92_bit_5 -X92_bit_4 -X92_bit_3 -X92_bit_2 -X92_bit_1 -X92_bit0 -X92_bit1 -X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 -X93_bit_7 -X93_bit_6 X93_bit_5 -X93_bit_4 X93_bit_3 X93_bit_2 X93_bit_1 X93_bit0 X93_bit1 X93_bit2 X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 -X94_bit_7 -X94_bit_6 X94_bit_5 X94_bit_4 -X94_bit_3 -X94_bit_2 -X94_bit_1 X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 -X95_bit_7 -X95_bit_6 -X95_bit_5 -X95_bit_4 -X95_bit_3 -X95_bit_2 -X95_bit_1 -X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 -X96_bit_7 -X96_bit_6 -X96_bit_5 -X96_bit_4 -X96_bit_3 -X96_bit_2 -X96_bit_1 -X96_bit0 -X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 -X97_bit_7 -X97_bit_6 -X97_bit_5 -X97_bit_4 -X97_bit_3 -X97_bit_2 -X97_bit_1 -X97_bit0 -X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 -X98_bit_7 -X98_bit_6 -X98_bit_5 -X98_bit_4 -X98_bit_3 -X98_bit_2 -X98_bit_1 -X98_bit0 -X98_bit1 -X98_bit2 -X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.90 2/54 30448
Raw data (stat): 30448 (runsolver) R 30447 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482933279 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 5863 0 0 0 985 13 0 0 25 0 1 0 482933279 25718784 5202 4294967295 134512640 134672761 3221224624 3221223768 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6279 5202 603 41 0 6238 0
vsize: 25116
[startup+20.0024 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 6101 0 0 0 1983 14 0 0 25 0 1 0 482933279 26652672 5440 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6507 5440 603 41 0 6466 0
vsize: 26028
[startup+30.0024 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 6437 0 0 0 2982 14 0 0 25 0 1 0 482933279 28028928 5776 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6843 5776 603 41 0 6802 0
vsize: 27372
[startup+40.0025 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 6654 0 0 0 3981 15 0 0 25 0 1 0 482933279 28856320 5972 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7045 5972 603 41 0 7004 0
vsize: 28180
[startup+50.003 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 6973 0 0 0 4980 16 0 0 25 0 1 0 482933279 30195712 6291 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7372 6291 603 41 0 7331 0
vsize: 29488
[startup+60.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 7212 0 0 0 5979 17 0 0 25 0 1 0 482933279 31260672 6530 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7632 6530 603 41 0 7591 0
vsize: 30528
[startup+70.0041 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 7438 0 0 0 6978 18 0 0 25 0 1 0 482933279 32198656 6756 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7861 6756 603 41 0 7820 0
vsize: 31444
[startup+80.0046 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 7716 0 0 0 7977 19 0 0 25 0 1 0 482933279 33280000 7034 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8125 7034 603 41 0 8084 0
vsize: 32500
[startup+90.0044 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 8215 0 0 0 8975 21 0 0 25 0 1 0 482933279 35291136 7533 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8616 7533 603 41 0 8575 0
vsize: 34464
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 8554 0 0 0 9974 22 0 0 25 0 1 0 482933279 36638720 7872 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8945 7872 603 41 0 8904 0
vsize: 35780
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 8845 0 0 0 10974 23 0 0 25 0 1 0 482933279 37838848 8163 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9238 8163 603 41 0 9197 0
vsize: 36952
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 9196 0 0 0 11973 24 0 0 25 0 1 0 482933279 39309312 8514 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9597 8514 603 41 0 9556 0
vsize: 38388
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 9426 0 0 0 12972 25 0 0 25 0 1 0 482933279 40251392 8744 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9827 8744 603 41 0 9786 0
vsize: 39308
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 9950 0 0 0 13971 26 0 0 25 0 1 0 482933279 42274816 9268 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10321 9268 603 41 0 10280 0
vsize: 41284
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 10968 0 0 0 14970 28 0 0 25 0 1 0 482933279 46821376 10286 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11431 10286 603 41 0 11390 0
vsize: 45724
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 11097 0 0 0 15969 28 0 0 25 0 1 0 482933279 47198208 10395 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11523 10395 603 41 0 11482 0
vsize: 46092
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 11097 0 0 0 16970 28 0 0 25 0 1 0 482933279 47198208 10395 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11523 10395 603 41 0 11482 0
vsize: 46092
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 11097 0 0 0 17970 28 0 0 25 0 1 0 482933279 47198208 10395 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11523 10395 603 41 0 11482 0
vsize: 46092
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 11098 0 0 0 18970 28 0 0 25 0 1 0 482933279 47198208 10396 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11523 10396 603 41 0 11482 0
vsize: 46092
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 11098 0 0 0 19970 28 0 0 25 0 1 0 482933279 47198208 10396 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11523 10396 603 41 0 11482 0
vsize: 46092
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 11098 0 0 0 20970 28 0 0 25 0 1 0 482933279 47198208 10396 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11523 10396 603 41 0 11482 0
vsize: 46092
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 11098 0 0 0 21970 28 0 0 25 0 1 0 482933279 47198208 10396 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11523 10396 603 41 0 11482 0
vsize: 46092
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 11098 0 0 0 22971 28 0 0 25 0 1 0 482933279 47198208 10396 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11523 10396 603 41 0 11482 0
vsize: 46092
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 11098 0 0 0 23971 28 0 0 25 0 1 0 482933279 47198208 10396 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11523 10396 603 41 0 11482 0
vsize: 46092
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 11098 0 0 0 24971 28 0 0 25 0 1 0 482933279 47198208 10396 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11523 10396 603 41 0 11482 0
vsize: 46092
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 11098 0 0 0 25971 28 0 0 25 0 1 0 482933279 47198208 10396 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11523 10396 603 41 0 11482 0
vsize: 46092
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 11098 0 0 0 26971 28 0 0 25 0 1 0 482933279 47198208 10396 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11523 10396 603 41 0 11482 0
vsize: 46092
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 11354 0 0 0 27971 29 0 0 25 0 1 0 482933279 48279552 10652 4294967295 134512640 134672761 3221224624 3221223808 134558903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11787 10652 603 41 0 11746 0
vsize: 47148
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 11696 0 0 0 28970 29 0 0 25 0 1 0 482933279 49627136 10994 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12116 10994 603 41 0 12075 0
vsize: 48464
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 11836 0 0 0 29970 30 0 0 25 0 1 0 482933279 50159616 11134 4294967295 134512640 134672761 3221224624 3221223760 134560625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12246 11134 603 41 0 12205 0
vsize: 48984
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 12017 0 0 0 30970 31 0 0 25 0 1 0 482933279 50962432 11315 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12442 11315 603 41 0 12401 0
vsize: 49768
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 12172 0 0 0 31970 31 0 0 25 0 1 0 482933279 51638272 11470 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12607 11470 603 41 0 12566 0
vsize: 50428
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 12323 0 0 0 32969 32 0 0 25 0 1 0 482933279 52166656 11621 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12736 11621 603 41 0 12695 0
vsize: 50944
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 12478 0 0 0 33969 32 0 0 25 0 1 0 482933279 52834304 11776 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12899 11776 603 41 0 12858 0
vsize: 51596
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 12717 0 0 0 34969 32 0 0 25 0 1 0 482933279 53817344 12015 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13139 12015 603 41 0 13098 0
vsize: 52556
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 12919 0 0 0 35968 33 0 0 25 0 1 0 482933279 54620160 12217 4294967295 134512640 134672761 3221224624 3221223728 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13335 12217 603 41 0 13294 0
vsize: 53340
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 13101 0 0 0 36968 34 0 0 25 0 1 0 482933279 55418880 12399 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13530 12399 603 41 0 13489 0
vsize: 54120
[startup+380.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 13279 0 0 0 37967 35 0 0 25 0 1 0 482933279 56094720 12577 4294967295 134512640 134672761 3221224624 3221223792 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13695 12577 603 41 0 13654 0
vsize: 54780
[startup+390.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 13493 0 0 0 38967 35 0 0 25 0 1 0 482933279 56905728 12791 4294967295 134512640 134672761 3221224624 3221223760 134560613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13893 12791 603 41 0 13852 0
vsize: 55572
[startup+400.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 13708 0 0 0 39966 36 0 0 25 0 1 0 482933279 57835520 13006 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14120 13006 603 41 0 14079 0
vsize: 56480
[startup+410.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 13871 0 0 0 40966 37 0 0 25 0 1 0 482933279 58511360 13169 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14285 13169 603 41 0 14244 0
vsize: 57140
[startup+420.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 14078 0 0 0 41965 37 0 0 25 0 1 0 482933279 59322368 13376 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14483 13376 603 41 0 14442 0
vsize: 57932
[startup+430.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 14304 0 0 0 42965 38 0 0 25 0 1 0 482933279 60268544 13602 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14714 13602 603 41 0 14673 0
vsize: 58856
[startup+440.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 14534 0 0 0 43964 39 0 0 25 0 1 0 482933279 61235200 13832 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14950 13832 603 41 0 14909 0
vsize: 59800
[startup+450.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 14670 0 0 0 44964 39 0 0 25 0 1 0 482933279 61767680 13968 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15080 13968 603 41 0 15039 0
vsize: 60320
[startup+460.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 15029 0 0 0 45964 40 0 0 25 0 1 0 482933279 63242240 14327 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15440 14327 603 41 0 15399 0
vsize: 61760
[startup+470.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 15234 0 0 0 46963 41 0 0 25 0 1 0 482933279 64053248 14532 4294967295 134512640 134672761 3221224624 3221223728 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15638 14532 603 41 0 15597 0
vsize: 62552
[startup+480.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 15426 0 0 0 47963 41 0 0 25 0 1 0 482933279 64847872 14724 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15832 14724 603 41 0 15791 0
vsize: 63328
[startup+490.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 15727 0 0 0 48962 42 0 0 25 0 1 0 482933279 66043904 15025 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16124 15025 603 41 0 16083 0
vsize: 64496
[startup+500.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 16108 0 0 0 49962 42 0 0 25 0 1 0 482933279 67629056 15406 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16511 15406 603 41 0 16470 0
vsize: 66044
[startup+510.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 16459 0 0 0 50961 43 0 0 25 0 1 0 482933279 69107712 15757 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16872 15757 603 41 0 16831 0
vsize: 67488
[startup+520.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 16774 0 0 0 51961 44 0 0 25 0 1 0 482933279 70311936 16072 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17166 16072 603 41 0 17125 0
vsize: 68664
[startup+530.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 16888 0 0 0 52961 44 0 0 25 0 1 0 482933279 70852608 16186 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17298 16186 603 41 0 17257 0
vsize: 69192
[startup+540.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 17014 0 0 0 53961 44 0 0 25 0 1 0 482933279 71385088 16312 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17428 16313 603 41 0 17387 0
vsize: 69712
[startup+550.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 17163 0 0 0 54960 45 0 0 25 0 1 0 482933279 71917568 16461 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17558 16461 603 41 0 17517 0
vsize: 70232
[startup+560.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 17289 0 0 0 55960 45 0 0 25 0 1 0 482933279 72458240 16587 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17690 16587 603 41 0 17649 0
vsize: 70760
[startup+570.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 17418 0 0 0 56960 46 0 0 25 0 1 0 482933279 72994816 16716 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17821 16716 603 41 0 17780 0
vsize: 71284
[startup+580.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 17827 0 0 0 57959 47 0 0 25 0 1 0 482933279 74596352 17125 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18212 17125 603 41 0 18171 0
vsize: 72848
[startup+590.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 18907 0 0 0 58957 49 0 0 25 0 1 0 482933279 79032320 18205 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19295 18205 603 41 0 19254 0
vsize: 77180
[startup+600.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 19814 0 0 0 59956 51 0 0 25 0 1 0 482933279 83320832 19112 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20342 19112 603 41 0 20301 0
vsize: 81368
[startup+610.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 20639 0 0 0 60954 52 0 0 25 0 1 0 482933279 86564864 19937 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21134 19937 603 41 0 21093 0
vsize: 84536
[startup+620.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 21438 0 0 0 61953 54 0 0 25 0 1 0 482933279 89944064 20736 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21959 20736 603 41 0 21918 0
vsize: 87836
[startup+630.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 22202 0 0 0 62951 56 0 0 25 0 1 0 482933279 93089792 21500 4294967295 134512640 134672761 3221224624 3221223728 134559969 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22727 21500 603 41 0 22686 0
vsize: 90908
[startup+640.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 22909 0 0 0 63949 58 0 0 25 0 1 0 482933279 95940608 22207 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23423 22207 603 41 0 23382 0
vsize: 93692
[startup+650.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 23587 0 0 0 64948 59 0 0 25 0 1 0 482933279 98648064 22885 4294967295 134512640 134672761 3221224624 3221223728 134560408 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24084 22885 603 41 0 24043 0
vsize: 96336
[startup+660.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 24276 0 0 0 65946 61 0 0 25 0 1 0 482933279 101486592 23574 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24777 23574 603 41 0 24736 0
vsize: 99108
[startup+670.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 24961 0 0 0 66945 62 0 0 25 0 1 0 482933279 104312832 24259 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25467 24259 603 41 0 25426 0
vsize: 101868
[startup+680.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 25616 0 0 0 67943 65 0 0 25 0 1 0 482933279 107012096 24914 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26126 24914 603 41 0 26085 0
vsize: 104504
[startup+690.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 26003 0 0 0 68941 66 0 0 25 0 1 0 482933279 108621824 25301 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26519 25301 603 41 0 26478 0
vsize: 106076
[startup+700.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 26176 0 0 0 69941 67 0 0 25 0 1 0 482933279 109297664 25474 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26684 25474 603 41 0 26643 0
vsize: 106736
[startup+710.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 26301 0 0 0 70941 67 0 0 25 0 1 0 482933279 109834240 25599 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26815 25599 603 41 0 26774 0
vsize: 107260
[startup+720.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 26411 0 0 0 71941 67 0 0 25 0 1 0 482933279 110235648 25709 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26913 25709 603 41 0 26872 0
vsize: 107652
[startup+730.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 26532 0 0 0 72941 68 0 0 25 0 1 0 482933279 110641152 25830 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27012 25830 603 41 0 26971 0
vsize: 108048
[startup+740.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 26658 0 0 0 73940 68 0 0 25 0 1 0 482933279 111177728 25956 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27143 25956 603 41 0 27102 0
vsize: 108572
[startup+750.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 26796 0 0 0 74940 69 0 0 25 0 1 0 482933279 111706112 26094 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27272 26094 603 41 0 27231 0
vsize: 109088
[startup+760.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 26931 0 0 0 75940 69 0 0 25 0 1 0 482933279 112377856 26229 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27436 26229 603 41 0 27395 0
vsize: 109744
[startup+770.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 27053 0 0 0 76940 69 0 0 25 0 1 0 482933279 112775168 26351 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27533 26351 603 41 0 27492 0
vsize: 110132
[startup+780.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 27151 0 0 0 77940 70 0 0 25 0 1 0 482933279 113188864 26449 4294967295 134512640 134672761 3221224624 3221223776 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27634 26449 603 41 0 27593 0
vsize: 110536
[startup+790.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 27266 0 0 0 78939 70 0 0 25 0 1 0 482933279 113729536 26564 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27766 26564 603 41 0 27725 0
vsize: 111064
[startup+800.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 27383 0 0 0 79940 70 0 0 25 0 1 0 482933279 114143232 26681 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27867 26681 603 41 0 27826 0
vsize: 111468
[startup+810.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 27551 0 0 0 80939 71 0 0 25 0 1 0 482933279 114831360 26849 4294967295 134512640 134672761 3221224624 3221223580 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28035 26849 603 41 0 27994 0
vsize: 112140
[startup+820.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 27802 0 0 0 81939 71 0 0 25 0 1 0 482933279 115900416 27100 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28296 27100 603 41 0 28255 0
vsize: 113184
[startup+830.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 27965 0 0 0 82938 72 0 0 25 0 1 0 482933279 116580352 27263 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28462 27263 603 41 0 28421 0
vsize: 113848
[startup+840.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28107 0 0 0 83938 72 0 0 25 0 1 0 482933279 117121024 27405 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28594 27405 603 41 0 28553 0
vsize: 114376
[startup+850.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28271 0 0 0 84938 73 0 0 25 0 1 0 482933279 117800960 27569 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28760 27569 603 41 0 28719 0
vsize: 115040
[startup+860.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28465 0 0 0 85938 73 0 0 25 0 1 0 482933279 118603776 27763 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28956 27763 603 41 0 28915 0
vsize: 115824
[startup+870.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 86938 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223184 134565745 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+880.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 87938 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+890.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 88938 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+900.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 89939 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+910.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 90939 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+920.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 91939 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+930.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 92939 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+940.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 93938 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+950.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 94938 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+960.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 95939 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+970.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 96939 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223760 134560632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+980.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 97939 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223808 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+990.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 98939 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 99939 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 100939 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223792 134561256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 101939 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 102940 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 103940 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 104940 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223808 134558332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 105940 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 106940 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 107941 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 108941 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 109941 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 110941 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 111941 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 112942 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 113942 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 114942 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223768 134560555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 115942 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 116942 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 117942 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 118942 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30448
Raw data (stat): 30448 (minisat+) R 30447 5897 5896 0 -1 0 28627 0 0 0 119943 73 0 0 25 0 1 0 482933279 119271424 27925 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29119 27925 603 41 0 29078 0
vsize: 116476
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 30448
Raw data (stat): 30448 (minisat+) Z 30447 5897 5896 0 -1 12 28630 0 0 0 119943 79 0 0 25 0 1 0 482933279 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.11
CPU time (s): 1200.23
CPU user time (s): 1199.44
CPU system time (s): 0.791879
CPU usage (%): 100.01
Max. virtual memory (Kb): 116476
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####