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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Namemps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran10x10c.opb
MD5SUM31a8734340f0544712ef974997c104b2
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 2523648
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 numbers29
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.08
Number of variables2100
Total number of constraints120
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints120
Minimum length of a constraint21
Maximum length of a constraint200

Trace number 6255

Launcher Data

LAUNCH ON wulflinc11 THE 2005-09-20 04:55:41 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3422 boxname=wulflinc11 idbench=1078 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  31a8734340f0544712ef974997c104b2  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-ran10x10c.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-ran10x10c.opb
IDLAUNCH: 3422
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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:        871112 kB
Buffers:         27020 kB
Cached:         110172 kB
SwapCached:        916 kB
Active:          41152 kB
Inactive:        98596 kB
HighTotal:      131008 kB
HighFree:        21140 kB
LowTotal:       903652 kB
LowFree:        849972 kB
SwapTotal:     2097136 kB
SwapFree:      2095640 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5660 kB
Slab:            18244 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 05:15:51 (client local time) WITH STATUS 10 IN 1208.06 SECONDS
stats: 3422 7 1208.06 10

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 Found solution: 10107013
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 Found solution: 9973742
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 Found solution: 3754669
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 Found solution: 3341769
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 Found solution: 3338727
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_

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/524/stat): 524 (minisat+_script) R 523 524 9854 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797590299 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/524/statm): 174 3 169 147 0 27 0
[pid=524] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=525
New process pid=526
New process pid=527
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
One traced child (pid=526) exited with status: 0
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=527) exited with status: 0
One traced child (pid=525) exited with status: 0
New process pid=528
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-ran10x10c.opb

[startup+10.0037 s]
Raw data (loadavg): 0.94 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 5720 0 0 0 956 21 0 0 25 0 1 0 1797590304 23719936 5039 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 5791 5039 145 145 0 5646 0
[pid=528] vsize: 23164
Current children cumulated CPU time (s) 9.77
Current children cumulated vsize (Kb) 25288

[startup+20.0056 s]
Raw data (loadavg): 0.95 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 5980 0 0 0 1951 23 0 0 25 0 1 0 1797590304 24870912 5299 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/528/statm): 6072 5299 145 145 0 5927 0
[pid=528] vsize: 24288
Current children cumulated CPU time (s) 19.74
Current children cumulated vsize (Kb) 26412

[startup+30.0073 s]
Raw data (loadavg): 0.95 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 6267 0 0 0 2945 25 0 0 25 0 1 0 1797590304 26066944 5586 4294967295 134512640 135094434 3221224432 3221223088 134561746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 6364 5586 145 145 0 6219 0
[pid=528] vsize: 25456
Current children cumulated CPU time (s) 29.7
Current children cumulated vsize (Kb) 27580

[startup+40.0071 s]
Raw data (loadavg): 0.96 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 6509 0 0 0 3942 26 0 0 25 0 1 0 1797590304 26886144 5791 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 6564 5791 145 145 0 6419 0
[pid=528] vsize: 26256
Current children cumulated CPU time (s) 39.68
Current children cumulated vsize (Kb) 28380

[startup+50.0089 s]
Raw data (loadavg): 0.97 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 6690 0 0 0 4939 28 0 0 25 0 1 0 1797590304 27619328 5972 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 6743 5972 145 145 0 6598 0
[pid=528] vsize: 26972
Current children cumulated CPU time (s) 49.67
Current children cumulated vsize (Kb) 29096

[startup+60.0097 s]
Raw data (loadavg): 0.97 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 7028 0 0 0 5933 30 0 0 25 0 1 0 1797590304 28983296 6310 4294967295 134512640 135094434 3221224432 3221223088 134558284 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 7076 6310 145 145 0 6931 0
[pid=528] vsize: 28304
Current children cumulated CPU time (s) 59.63
Current children cumulated vsize (Kb) 30428

[startup+70.0115 s]
Raw data (loadavg): 0.97 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 7274 0 0 0 6928 33 0 0 22 0 1 0 1797590304 30101504 6556 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 7349 6556 145 145 0 7204 0
[pid=528] vsize: 29396
Current children cumulated CPU time (s) 69.61
Current children cumulated vsize (Kb) 31520

[startup+80.0122 s]
Raw data (loadavg): 0.98 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 7449 0 0 0 7924 34 0 0 25 0 1 0 1797590304 30806016 6731 4294967295 134512640 135094434 3221224432 3221223104 134555323 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 7521 6731 145 145 0 7376 0
[pid=528] vsize: 30084
Current children cumulated CPU time (s) 79.58
Current children cumulated vsize (Kb) 32208

[startup+90.013 s]
Raw data (loadavg): 0.98 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 7973 0 0 0 8917 37 0 0 25 0 1 0 1797590304 32935936 7255 4294967295 134512640 135094434 3221224432 3221223088 134558002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 8041 7255 145 145 0 7896 0
[pid=528] vsize: 32164
Current children cumulated CPU time (s) 89.54
Current children cumulated vsize (Kb) 34288

[startup+100.014 s]
Raw data (loadavg): 0.98 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 8336 0 0 0 9912 39 0 0 25 0 1 0 1797590304 34398208 7618 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 8398 7618 145 145 0 8253 0
[pid=528] vsize: 33592
Current children cumulated CPU time (s) 99.51
Current children cumulated vsize (Kb) 35716

[startup+110.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 8641 0 0 0 10906 42 0 0 25 0 1 0 1797590304 35635200 7923 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 8700 7923 145 145 0 8555 0
[pid=528] vsize: 34800
Current children cumulated CPU time (s) 109.48
Current children cumulated vsize (Kb) 36924

[startup+120.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 8987 0 0 0 11901 43 0 0 25 0 1 0 1797590304 37040128 8269 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 9043 8269 145 145 0 8898 0
[pid=528] vsize: 36172
Current children cumulated CPU time (s) 119.44
Current children cumulated vsize (Kb) 38296

[startup+130.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 9258 0 0 0 12897 45 0 0 25 0 1 0 1797590304 38133760 8540 4294967295 134512640 135094434 3221224432 3221223120 134554788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 9310 8540 145 145 0 9165 0
[pid=528] vsize: 37240
Current children cumulated CPU time (s) 129.42
Current children cumulated vsize (Kb) 39364

[startup+140.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 9481 0 0 0 13893 47 0 0 25 0 1 0 1797590304 39034880 8763 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 9530 8763 145 145 0 9385 0
[pid=528] vsize: 38120
Current children cumulated CPU time (s) 139.4
Current children cumulated vsize (Kb) 40244

[startup+150.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 10496 0 0 0 14880 53 0 0 25 0 1 0 1797590304 43442176 9778 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 10606 9778 145 145 0 10461 0
[pid=528] vsize: 42424
Current children cumulated CPU time (s) 149.33
Current children cumulated vsize (Kb) 44548

[startup+160.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 11031 0 0 0 15876 55 0 0 25 0 1 0 1797590304 45461504 10274 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 11099 10274 145 145 0 10954 0
[pid=528] vsize: 44396
Current children cumulated CPU time (s) 159.31
Current children cumulated vsize (Kb) 46520

[startup+170.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 11031 0 0 0 16876 55 0 0 25 0 1 0 1797590304 45461504 10274 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 11099 10274 145 145 0 10954 0
[pid=528] vsize: 44396
Current children cumulated CPU time (s) 169.31
Current children cumulated vsize (Kb) 46520

[startup+180.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 11031 0 0 0 17875 56 0 0 25 0 1 0 1797590304 45461504 10274 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 11099 10274 145 145 0 10954 0
[pid=528] vsize: 44396
Current children cumulated CPU time (s) 179.31
Current children cumulated vsize (Kb) 46520

[startup+190.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 11031 0 0 0 18875 56 0 0 25 0 1 0 1797590304 45461504 10274 4294967295 134512640 135094434 3221224432 3221223024 134556847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 11099 10274 145 145 0 10954 0
[pid=528] vsize: 44396
Current children cumulated CPU time (s) 189.31
Current children cumulated vsize (Kb) 46520

[startup+200.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 11032 0 0 0 19875 56 0 0 25 0 1 0 1797590304 45461504 10275 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 11099 10275 145 145 0 10954 0
[pid=528] vsize: 44396
Current children cumulated CPU time (s) 199.31
Current children cumulated vsize (Kb) 46520

[startup+210.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 11032 0 0 0 20876 56 0 0 25 0 1 0 1797590304 45461504 10275 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 11099 10275 145 145 0 10954 0
[pid=528] vsize: 44396
Current children cumulated CPU time (s) 209.32
Current children cumulated vsize (Kb) 46520

[startup+220.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 11032 0 0 0 21876 56 0 0 25 0 1 0 1797590304 45461504 10275 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 11099 10275 145 145 0 10954 0
[pid=528] vsize: 44396
Current children cumulated CPU time (s) 219.32
Current children cumulated vsize (Kb) 46520

[startup+230.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 11032 0 0 0 22876 56 0 0 25 0 1 0 1797590304 45461504 10275 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 11099 10275 145 145 0 10954 0
[pid=528] vsize: 44396
Current children cumulated CPU time (s) 229.32
Current children cumulated vsize (Kb) 46520

[startup+240.025 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 11032 0 0 0 23876 56 0 0 25 0 1 0 1797590304 45461504 10275 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 11099 10275 145 145 0 10954 0
[pid=528] vsize: 44396
Current children cumulated CPU time (s) 239.32
Current children cumulated vsize (Kb) 46520

[startup+250.026 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 11032 0 0 0 24877 56 0 0 25 0 1 0 1797590304 45461504 10275 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 11099 10275 145 145 0 10954 0
[pid=528] vsize: 44396
Current children cumulated CPU time (s) 249.33
Current children cumulated vsize (Kb) 46520

[startup+260.026 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 11032 0 0 0 25877 56 0 0 25 0 1 0 1797590304 45461504 10275 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 11099 10275 145 145 0 10954 0
[pid=528] vsize: 44396
Current children cumulated CPU time (s) 259.33
Current children cumulated vsize (Kb) 46520

[startup+270.027 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 11032 0 0 0 26877 56 0 0 25 0 1 0 1797590304 45461504 10275 4294967295 134512640 135094434 3221224432 3221223064 134557638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 11099 10275 145 145 0 10954 0
[pid=528] vsize: 44396
Current children cumulated CPU time (s) 269.33
Current children cumulated vsize (Kb) 46520

[startup+280.028 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 11032 0 0 0 27877 56 0 0 25 0 1 0 1797590304 45461504 10275 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 11099 10275 145 145 0 10954 0
[pid=528] vsize: 44396
Current children cumulated CPU time (s) 279.33
Current children cumulated vsize (Kb) 46520

[startup+290.029 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 11493 0 0 0 28873 58 0 0 25 0 1 0 1797590304 47353856 10736 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 11561 10736 145 145 0 11416 0
[pid=528] vsize: 46244
Current children cumulated CPU time (s) 289.31
Current children cumulated vsize (Kb) 48368

[startup+300.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 11657 0 0 0 29870 60 0 0 25 0 1 0 1797590304 48025600 10900 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 11725 10900 145 145 0 11580 0
[pid=528] vsize: 46900
Current children cumulated CPU time (s) 299.3
Current children cumulated vsize (Kb) 49024

[startup+310.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 11820 0 0 0 30867 61 0 0 25 0 1 0 1797590304 48697344 11063 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 11889 11063 145 145 0 11744 0
[pid=528] vsize: 47556
Current children cumulated CPU time (s) 309.28
Current children cumulated vsize (Kb) 49680

[startup+320.031 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 11979 0 0 0 31865 62 0 0 25 0 1 0 1797590304 49344512 11222 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 12047 11222 145 145 0 11902 0
[pid=528] vsize: 48188
Current children cumulated CPU time (s) 319.27
Current children cumulated vsize (Kb) 50312

[startup+330.032 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 12148 0 0 0 32862 63 0 0 25 0 1 0 1797590304 50036736 11391 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 12216 11391 145 145 0 12071 0
[pid=528] vsize: 48864
Current children cumulated CPU time (s) 329.25
Current children cumulated vsize (Kb) 50988

[startup+340.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 12274 0 0 0 33860 64 0 0 25 0 1 0 1797590304 50552832 11517 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 12342 11517 145 145 0 12197 0
[pid=528] vsize: 49368
Current children cumulated CPU time (s) 339.24
Current children cumulated vsize (Kb) 51492

[startup+350.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 12464 0 0 0 34857 65 0 0 25 0 1 0 1797590304 51318784 11707 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 12529 11707 145 145 0 12384 0
[pid=528] vsize: 50116
Current children cumulated CPU time (s) 349.22
Current children cumulated vsize (Kb) 52240

[startup+360.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 12682 0 0 0 35853 67 0 0 25 0 1 0 1797590304 52207616 11925 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 12746 11925 145 145 0 12601 0
[pid=528] vsize: 50984
Current children cumulated CPU time (s) 359.2
Current children cumulated vsize (Kb) 53108

[startup+370.036 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 12892 0 0 0 36850 68 0 0 25 0 1 0 1797590304 53059584 12135 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 12954 12135 145 145 0 12809 0
[pid=528] vsize: 51816
Current children cumulated CPU time (s) 369.18
Current children cumulated vsize (Kb) 53940

[startup+380.037 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 13052 0 0 0 37848 69 0 0 25 0 1 0 1797590304 53710848 12295 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 13113 12295 145 145 0 12968 0
[pid=528] vsize: 52452
Current children cumulated CPU time (s) 379.17
Current children cumulated vsize (Kb) 54576

[startup+390.038 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 13252 0 0 0 38844 71 0 0 25 0 1 0 1797590304 54513664 12495 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 13309 12495 145 145 0 13164 0
[pid=528] vsize: 53236
Current children cumulated CPU time (s) 389.15
Current children cumulated vsize (Kb) 55360

[startup+400.038 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 13455 0 0 0 39841 72 0 0 25 0 1 0 1797590304 55341056 12698 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 13511 12698 145 145 0 13366 0
[pid=528] vsize: 54044
Current children cumulated CPU time (s) 399.13
Current children cumulated vsize (Kb) 56168

[startup+410.038 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 13664 0 0 0 40838 73 0 0 25 0 1 0 1797590304 56188928 12907 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 13718 12907 145 145 0 13573 0
[pid=528] vsize: 54872
Current children cumulated CPU time (s) 409.11
Current children cumulated vsize (Kb) 56996

[startup+420.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 13838 0 0 0 41836 75 0 0 25 0 1 0 1797590304 56893440 13081 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 13890 13081 145 145 0 13745 0
[pid=528] vsize: 55560
Current children cumulated CPU time (s) 419.11
Current children cumulated vsize (Kb) 57684

[startup+430.041 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 14050 0 0 0 42832 77 0 0 25 0 1 0 1797590304 57737216 13293 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 14096 13293 145 145 0 13951 0
[pid=528] vsize: 56384
Current children cumulated CPU time (s) 429.09
Current children cumulated vsize (Kb) 58508

[startup+440.041 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 14283 0 0 0 43827 79 0 0 25 0 1 0 1797590304 58736640 13526 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 14340 13526 145 145 0 14195 0
[pid=528] vsize: 57360
Current children cumulated CPU time (s) 439.06
Current children cumulated vsize (Kb) 59484

[startup+450.041 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 14480 0 0 0 44824 80 0 0 25 0 1 0 1797590304 59531264 13723 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 14534 13723 145 145 0 14389 0
[pid=528] vsize: 58136
Current children cumulated CPU time (s) 449.04
Current children cumulated vsize (Kb) 60260

[startup+460.042 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 14621 0 0 0 45822 81 0 0 25 0 1 0 1797590304 60104704 13864 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 14674 13864 145 145 0 14529 0
[pid=528] vsize: 58696
Current children cumulated CPU time (s) 459.03
Current children cumulated vsize (Kb) 60820

[startup+470.043 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 14980 0 0 0 46816 83 0 0 25 0 1 0 1797590304 61562880 14223 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 15030 14223 145 145 0 14885 0
[pid=528] vsize: 60120
Current children cumulated CPU time (s) 468.99
Current children cumulated vsize (Kb) 62244

[startup+480.044 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 15198 0 0 0 47811 85 0 0 25 0 1 0 1797590304 62447616 14441 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 15246 14441 145 145 0 15101 0
[pid=528] vsize: 60984
Current children cumulated CPU time (s) 478.96
Current children cumulated vsize (Kb) 63108

[startup+490.044 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 15367 0 0 0 48808 87 0 0 25 0 1 0 1797590304 63131648 14610 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 15413 14610 145 145 0 15268 0
[pid=528] vsize: 61652
Current children cumulated CPU time (s) 488.95
Current children cumulated vsize (Kb) 63776

[startup+500.045 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 15702 0 0 0 49802 90 0 0 25 0 1 0 1797590304 64495616 14945 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 15746 14945 145 145 0 15601 0
[pid=528] vsize: 62984
Current children cumulated CPU time (s) 498.92
Current children cumulated vsize (Kb) 65108

[startup+510.046 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 16078 0 0 0 50795 93 0 0 25 0 1 0 1797590304 66035712 15321 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 16122 15321 145 145 0 15977 0
[pid=528] vsize: 64488
Current children cumulated CPU time (s) 508.88
Current children cumulated vsize (Kb) 66612

[startup+520.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 16448 0 0 0 51789 95 0 0 25 0 1 0 1797590304 67543040 15691 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 16490 15691 145 145 0 16345 0
[pid=528] vsize: 65960
Current children cumulated CPU time (s) 518.84
Current children cumulated vsize (Kb) 68084

[startup+530.048 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 16697 0 0 0 52786 96 0 0 25 0 1 0 1797590304 68554752 15940 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 16737 15940 145 145 0 16592 0
[pid=528] vsize: 66948
Current children cumulated CPU time (s) 528.82
Current children cumulated vsize (Kb) 69072

[startup+540.048 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 16808 0 0 0 53784 97 0 0 25 0 1 0 1797590304 69009408 16051 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 16848 16051 145 145 0 16703 0
[pid=528] vsize: 67392
Current children cumulated CPU time (s) 538.81
Current children cumulated vsize (Kb) 69516

[startup+550.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 16940 0 0 0 54782 98 0 0 25 0 1 0 1797590304 69562368 16183 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 16983 16183 145 145 0 16838 0
[pid=528] vsize: 67932
Current children cumulated CPU time (s) 548.8
Current children cumulated vsize (Kb) 70056

[startup+560.051 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 17083 0 0 0 55780 99 0 0 25 0 1 0 1797590304 70144000 16326 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 17125 16326 145 145 0 16980 0
[pid=528] vsize: 68500
Current children cumulated CPU time (s) 558.79
Current children cumulated vsize (Kb) 70624

[startup+570.053 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 17208 0 0 0 56778 100 0 0 25 0 1 0 1797590304 70647808 16451 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 17248 16451 145 145 0 17103 0
[pid=528] vsize: 68992
Current children cumulated CPU time (s) 568.78
Current children cumulated vsize (Kb) 71116

[startup+580.053 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 17342 0 0 0 57775 102 0 0 25 0 1 0 1797590304 71188480 16585 4294967295 134512640 135094434 3221224432 3221223024 134557514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 17380 16585 145 145 0 17235 0
[pid=528] vsize: 69520
Current children cumulated CPU time (s) 578.77
Current children cumulated vsize (Kb) 71644

[startup+590.053 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 17810 0 0 0 58769 104 0 0 25 0 1 0 1797590304 73093120 17053 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 17845 17053 145 145 0 17700 0
[pid=528] vsize: 71380
Current children cumulated CPU time (s) 588.73
Current children cumulated vsize (Kb) 73504

[startup+600.054 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 18843 0 0 0 59755 110 0 0 25 0 1 0 1797590304 77307904 18086 4294967295 134512640 135094434 3221224432 3221223024 134556843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 18874 18086 145 145 0 18729 0
[pid=528] vsize: 75496
Current children cumulated CPU time (s) 598.65
Current children cumulated vsize (Kb) 77620

[startup+610.055 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 19716 0 0 0 60745 115 0 0 25 0 1 0 1797590304 81395712 18959 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 19872 18959 145 145 0 19727 0
[pid=528] vsize: 79488
Current children cumulated CPU time (s) 608.6
Current children cumulated vsize (Kb) 81612

[startup+620.056 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 20521 0 0 0 61734 119 0 0 25 0 1 0 1797590304 84676608 19764 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 20673 19764 145 145 0 20528 0
[pid=528] vsize: 82692
Current children cumulated CPU time (s) 618.53
Current children cumulated vsize (Kb) 84816

[startup+630.056 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 21301 0 0 0 62723 125 0 0 25 0 1 0 1797590304 87863296 20544 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 21451 20544 145 145 0 21306 0
[pid=528] vsize: 85804
Current children cumulated CPU time (s) 628.48
Current children cumulated vsize (Kb) 87928

[startup+640.057 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 22055 0 0 0 63713 129 0 0 25 0 1 0 1797590304 90959872 21298 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 22207 21298 145 145 0 22062 0
[pid=528] vsize: 88828
Current children cumulated CPU time (s) 638.42
Current children cumulated vsize (Kb) 90952

[startup+650.058 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 22740 0 0 0 64704 133 0 0 25 0 1 0 1797590304 93761536 21983 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 22891 21983 145 145 0 22746 0
[pid=528] vsize: 91564
Current children cumulated CPU time (s) 648.37
Current children cumulated vsize (Kb) 93688

[startup+660.059 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 23400 0 0 0 65695 137 0 0 25 0 1 0 1797590304 96456704 22643 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 23549 22643 145 145 0 23404 0
[pid=528] vsize: 94196
Current children cumulated CPU time (s) 658.32
Current children cumulated vsize (Kb) 96320

[startup+670.061 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 24080 0 0 0 66686 141 0 0 25 0 1 0 1797590304 99233792 23323 4294967295 134512640 135094434 3221224432 3221223024 134557025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 24227 23323 145 145 0 24082 0
[pid=528] vsize: 96908
Current children cumulated CPU time (s) 668.27
Current children cumulated vsize (Kb) 99032

[startup+680.061 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 24740 0 0 0 67676 146 0 0 25 0 1 0 1797590304 101928960 23983 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 24885 23983 145 145 0 24740 0
[pid=528] vsize: 99540
Current children cumulated CPU time (s) 678.22
Current children cumulated vsize (Kb) 101664

[startup+690.062 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 25405 0 0 0 68667 150 0 0 25 0 1 0 1797590304 104640512 24648 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 25547 24648 145 145 0 25402 0
[pid=528] vsize: 102188
Current children cumulated CPU time (s) 688.17
Current children cumulated vsize (Kb) 104312

[startup+700.063 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 25874 0 0 0 69662 153 0 0 25 0 1 0 1797590304 106565632 25117 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 26017 25117 145 145 0 25872 0
[pid=528] vsize: 104068
Current children cumulated CPU time (s) 698.15
Current children cumulated vsize (Kb) 106192

[startup+710.064 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 26043 0 0 0 70659 154 0 0 25 0 1 0 1797590304 107245568 25286 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 26183 25286 145 145 0 26038 0
[pid=528] vsize: 104732
Current children cumulated CPU time (s) 708.13
Current children cumulated vsize (Kb) 106856

[startup+720.066 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 26180 0 0 0 71657 155 0 0 25 0 1 0 1797590304 107794432 25423 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 26317 25423 145 145 0 26172 0
[pid=528] vsize: 105268
Current children cumulated CPU time (s) 718.12
Current children cumulated vsize (Kb) 107392

[startup+730.066 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 26296 0 0 0 72655 156 0 0 25 0 1 0 1797590304 108257280 25539 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 26430 25539 145 145 0 26285 0
[pid=528] vsize: 105720
Current children cumulated CPU time (s) 728.11
Current children cumulated vsize (Kb) 107844

[startup+740.067 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 26411 0 0 0 73654 157 0 0 25 0 1 0 1797590304 108724224 25654 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 26544 25654 145 145 0 26399 0
[pid=528] vsize: 106176
Current children cumulated CPU time (s) 738.11
Current children cumulated vsize (Kb) 108300

[startup+750.068 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 26531 0 0 0 74652 157 0 0 25 0 1 0 1797590304 109207552 25774 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 26662 25774 145 145 0 26517 0
[pid=528] vsize: 106648
Current children cumulated CPU time (s) 748.09
Current children cumulated vsize (Kb) 108772

[startup+760.069 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 26674 0 0 0 75649 158 0 0 25 0 1 0 1797590304 109793280 25917 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 26805 25917 145 145 0 26660 0
[pid=528] vsize: 107220
Current children cumulated CPU time (s) 758.07
Current children cumulated vsize (Kb) 109344

[startup+770.069 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 26809 0 0 0 76648 159 0 0 25 0 1 0 1797590304 110350336 26052 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 26941 26052 145 145 0 26796 0
[pid=528] vsize: 107764
Current children cumulated CPU time (s) 768.07
Current children cumulated vsize (Kb) 109888

[startup+780.07 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 26926 0 0 0 77646 159 0 0 25 0 1 0 1797590304 110837760 26169 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 27060 26169 145 145 0 26915 0
[pid=528] vsize: 108240
Current children cumulated CPU time (s) 778.05
Current children cumulated vsize (Kb) 110364

[startup+790.071 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 27028 0 0 0 78644 160 0 0 25 0 1 0 1797590304 111259648 26271 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 27163 26271 145 145 0 27018 0
[pid=528] vsize: 108652
Current children cumulated CPU time (s) 788.04
Current children cumulated vsize (Kb) 110776

[startup+800.072 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 27138 0 0 0 79642 161 0 0 25 0 1 0 1797590304 111706112 26381 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 27272 26381 145 145 0 27127 0
[pid=528] vsize: 109088
Current children cumulated CPU time (s) 798.03
Current children cumulated vsize (Kb) 111212

[startup+810.073 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 27260 0 0 0 80640 162 0 0 25 0 1 0 1797590304 112201728 26503 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 27393 26503 145 145 0 27248 0
[pid=528] vsize: 109572
Current children cumulated CPU time (s) 808.02
Current children cumulated vsize (Kb) 111696

[startup+820.073 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 27360 0 0 0 81638 163 0 0 25 0 1 0 1797590304 112607232 26603 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 27492 26603 145 145 0 27347 0
[pid=528] vsize: 109968
Current children cumulated CPU time (s) 818.01
Current children cumulated vsize (Kb) 112092

[startup+830.074 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 27598 0 0 0 82634 165 0 0 25 0 1 0 1797590304 113586176 26841 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 27731 26841 145 145 0 27586 0
[pid=528] vsize: 110924
Current children cumulated CPU time (s) 827.99
Current children cumulated vsize (Kb) 113048

[startup+840.075 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 27824 0 0 0 83631 167 0 0 25 0 1 0 1797590304 114491392 27067 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 27952 27067 145 145 0 27807 0
[pid=528] vsize: 111808
Current children cumulated CPU time (s) 837.98
Current children cumulated vsize (Kb) 113932

[startup+850.077 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 27958 0 0 0 84630 168 0 0 25 0 1 0 1797590304 115032064 27201 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28084 27201 145 145 0 27939 0
[pid=528] vsize: 112336
Current children cumulated CPU time (s) 847.98
Current children cumulated vsize (Kb) 114460

[startup+860.078 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28106 0 0 0 85627 169 0 0 25 0 1 0 1797590304 115621888 27349 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28228 27349 145 145 0 28083 0
[pid=528] vsize: 112912
Current children cumulated CPU time (s) 857.96
Current children cumulated vsize (Kb) 115036

[startup+870.078 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28288 0 0 0 86624 170 0 0 25 0 1 0 1797590304 116387840 27531 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28415 27531 145 145 0 28270 0
[pid=528] vsize: 113660
Current children cumulated CPU time (s) 867.94
Current children cumulated vsize (Kb) 115784

[startup+880.079 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28484 0 0 0 87621 172 0 0 25 0 1 0 1797590304 117182464 27727 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28609 27727 145 145 0 28464 0
[pid=528] vsize: 114436
Current children cumulated CPU time (s) 877.93
Current children cumulated vsize (Kb) 116560

[startup+890.079 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 88620 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 887.92
Current children cumulated vsize (Kb) 116752

[startup+900.08 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 89620 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 897.92
Current children cumulated vsize (Kb) 116752

[startup+910.082 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 90620 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223104 134555579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 907.92
Current children cumulated vsize (Kb) 116752

[startup+920.082 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 91621 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 917.93
Current children cumulated vsize (Kb) 116752

[startup+930.083 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 92621 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 927.93
Current children cumulated vsize (Kb) 116752

[startup+940.084 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 93621 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 937.93
Current children cumulated vsize (Kb) 116752

[startup+950.085 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 94621 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223120 134554733 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 947.93
Current children cumulated vsize (Kb) 116752

[startup+960.085 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 95620 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 957.92
Current children cumulated vsize (Kb) 116752

[startup+970.087 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 96621 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 967.93
Current children cumulated vsize (Kb) 116752

[startup+980.088 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 97621 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 977.93
Current children cumulated vsize (Kb) 116752

[startup+990.089 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 98621 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 987.93
Current children cumulated vsize (Kb) 116752

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 99622 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 997.94
Current children cumulated vsize (Kb) 116752

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 100622 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 1007.94
Current children cumulated vsize (Kb) 116752

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 101622 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 1017.94
Current children cumulated vsize (Kb) 116752

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 102622 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 1027.94
Current children cumulated vsize (Kb) 116752

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 103622 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 1037.94
Current children cumulated vsize (Kb) 116752

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 104623 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 1047.95
Current children cumulated vsize (Kb) 116752

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 105623 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 1057.95
Current children cumulated vsize (Kb) 116752

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 106623 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 1067.95
Current children cumulated vsize (Kb) 116752

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 107624 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223088 134558284 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 1077.96
Current children cumulated vsize (Kb) 116752

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 108624 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 1087.96
Current children cumulated vsize (Kb) 116752

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 109624 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 1097.96
Current children cumulated vsize (Kb) 116752

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 110624 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 1107.96
Current children cumulated vsize (Kb) 116752

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 111625 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 1117.97
Current children cumulated vsize (Kb) 116752

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 112625 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 1127.97
Current children cumulated vsize (Kb) 116752

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 113625 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 1137.97
Current children cumulated vsize (Kb) 116752

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 114625 172 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 1147.97
Current children cumulated vsize (Kb) 116752

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 115626 173 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 1157.99
Current children cumulated vsize (Kb) 116752

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 116626 173 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223088 134557804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 1167.99
Current children cumulated vsize (Kb) 116752

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 117626 173 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 1177.99
Current children cumulated vsize (Kb) 116752

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 118626 173 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223056 134557642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 1187.99
Current children cumulated vsize (Kb) 116752

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 119627 173 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 1198
Current children cumulated vsize (Kb) 116752

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 120627 173 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 1208
Current children cumulated vsize (Kb) 116752



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.98 0.94 2/57 528
Raw data (/proc/524/stat): 524 (minisat+_script) S 523 524 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797590299 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/524/statm): 531 226 485 147 0 384 0
[pid=524] vsize: 2124
Raw data (/proc/528/stat): 528 (minisat+_64-bit) R 524 524 9854 0 -1 0 28532 0 0 0 120627 173 0 0 25 0 1 0 1797590304 117379072 27775 4294967295 134512640 135094434 3221224432 3221223088 134557829 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/528/statm): 28657 27775 145 145 0 28512 0
[pid=528] vsize: 114628
Current children cumulated CPU time (s) 1208
Current children cumulated vsize (Kb) 116752

Sending SIGTERM to -524
Sleeping 2 seconds
One traced child (pid=524) ended because it received signal 15 (SIGTERM)
One traced child (pid=528) exited with status: 10
All traced children have exited ! Game is over.

Child status: 10
Real time (s): 1210.17
CPU time (s): 1208.06
CPU user time (s): 1206.28
CPU system time (s): 1.78173
CPU usage (%): 99.8254
Max. virtual memory (cumulated for all children) (Kb): 116752

Verifier Data

ERROR: no interpretation found !