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-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-rgn.opb
MD5SUM4cc62e621e04c5a4e55edc3240fa3357
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 537600
Optimality of the best value was proved NO
Number of terms in the objective function 1160
Biggest coefficient in the objective function 196608
Number of bits for the biggest coefficient in the objective function 18
Sum of the numbers in the objective function 15892320
Number of bits of the sum of numbers in the objective function 24
Biggest number in a constraint 25600000000
Number of bits of the biggest number in a constraint 35
Biggest sum of numbers in a constraint 232836875088
Number of bits of the biggest sum of numbers38
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1249.96
Number of variables1260
Total number of constraints204
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)104
Number of constraints which are nor clauses,nor cardinality constraints100
Minimum length of a constraint1
Maximum length of a constraint127

Trace number 4547

Launcher Data

LAUNCH ON wulflinc20 THE 2005-09-19 18:08:23 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3006 boxname=wulflinc20 idbench=662 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4cc62e621e04c5a4e55edc3240fa3357  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-rgn.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-rgn.opb
IDLAUNCH: 3006
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 3
cpu MHz		: 451.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        878052 kB
Buffers:         40572 kB
Cached:          84940 kB
SwapCached:        832 kB
Active:          71068 kB
Inactive:        57112 kB
HighTotal:      131008 kB
HighFree:        42728 kB
LowTotal:       903652 kB
LowFree:        835324 kB
SwapTotal:     2097892 kB
SwapFree:      2096604 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5736 kB
Slab:            22772 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 18:28:33 (client local time) WITH STATUS 10 IN 1209.11 SECONDS
stats: 3006 7 1209.11 10

Solver Data

c Parsing PB file...
c Converting 124 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 123]---> BDD-cost:   16
c ---[ 122]---> BDD-cost:   16
c ---[ 121]---> BDD-cost:   16
c ---[ 120]---> BDD-cost:   16
c ---[ 119]---> BDD-cost:   16
c ---[ 118]---> BDD-cost:   16
c ---[ 117]---> BDD-cost:   16
c ---[ 116]---> BDD-cost:   16
c ---[ 115]---> BDD-cost:   16
c ---[ 114]---> BDD-cost:   16
c ---[ 113]---> BDD-cost:   16
c ---[ 112]---> BDD-cost:   16
c ---[ 111]---> BDD-cost:   16
c ---[ 110]---> BDD-cost:   16
c ---[ 109]---> BDD-cost:   16
c ---[ 108]---> BDD-cost:   16
c ---[ 107]---> BDD-cost:   16
c ---[ 106]---> BDD-cost:   16
c ---[ 105]---> BDD-cost:   16
c ---[ 104]---> BDD-cost:   16
c ---[ 103]---> BDD-cost:   11
c ---[ 102]---> BDD-cost:   11
c ---[ 101]---> BDD-cost:   11
c ---[ 100]---> BDD-cost:   11
c ---[  99]---> BDD-cost:   11
c ---[  98]---> BDD-cost:   11
c ---[  97]---> BDD-cost:   11
c ---[  96]---> BDD-cost:   11
c ---[  95]---> BDD-cost:   11
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:   11
c ---[  89]---> BDD-cost:   11
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   11
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   11
c ---[  84]---> BDD-cost:   11
c ---[  83]---> BDD-cost:   11
c ---[  82]---> BDD-cost:   11
c ---[  81]---> BDD-cost:   11
c ---[  80]---> BDD-cost:   11
c ---[  79]---> BDD-cost:   11
c ---[  78]---> BDD-cost:   11
c ---[  77]---> BDD-cost:   11
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   11
c ---[  74]---> BDD-cost:   11
c ---[  73]---> BDD-cost:   11
c ---[  72]---> BDD-cost:   11
c ---[  71]---> BDD-cost:   11
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:   11
c ---[  67]---> BDD-cost:   11
c ---[  66]---> BDD-cost:   11
c ---[  65]---> BDD-cost:   11
c ---[  64]---> BDD-cost:   11
c ---[  63]---> BDD-cost:   16
c ---[  62]---> BDD-cost:   16
c ---[  61]---> BDD-cost:   16
c ---[  60]---> BDD-cost:   16
c ---[  59]---> BDD-cost:   16
c ---[  58]---> BDD-cost:   16
c ---[  57]---> BDD-cost:   16
c ---[  56]---> BDD-cost:   16
c ---[  55]---> BDD-cost:   16
c ---[  54]---> BDD-cost:   16
c ---[  53]---> BDD-cost:   16
c ---[  52]---> BDD-cost:   16
c ---[  51]---> BDD-cost:   16
c ---[  50]---> BDD-cost:   16
c ---[  49]---> BDD-cost:   16
c ---[  48]---> BDD-cost:   16
c ---[  47]---> BDD-cost:   16
c ---[  46]---> BDD-cost:   16
c ---[  45]---> BDD-cost:   16
c ---[  44]---> BDD-cost:   16
c ---[  42]---> BDD-cost:  282
c ---[  40]---> BDD-cost: 1158
c ---[  38]---> BDD-cost: 1158
c ---[  36]---> BDD-cost: 1158
c ---[  34]---> BDD-cost: 1158
c ---[  32]---> BDD-cost: 1158
c ---[  30]---> BDD-cost: 1158
c ---[  28]---> BDD-cost: 1158
c ---[  26]---> BDD-cost: 1158
c ---[  24]---> BDD-cost: 1158
c ---[  23]---> BDD-cost:   47
c ---[  21]---> BDD-cost: 1158
c ---[  19]---> BDD-cost: 1158
c ---[  17]---> BDD-cost: 1158
c ---[  15]---> BDD-cost: 1158
c ---[  13]---> BDD-cost: 1158
c ---[  11]---> BDD-cost: 1158
c ---[  10]---> BDD-cost:   47
c ---[   9]---> BDD-cost:   47
c ---[   8]---> BDD-cost:   47
c ---[   6]---> BDD-cost:  282
c ---[   4]---> BDD-cost:  282
c ---[   2]---> BDD-cost:  282
c ---[   0]---> BDD-cost:  282
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   51929   146608 |   17309       0        0     nan |  0.000 % |
c |       101 |   51803   146356 |   19039      95      929     9.8 |  0.701 % |
c |       252 |   51803   146356 |   20943     246     3473    14.1 |  0.701 % |
c |       478 |   51797   146344 |   23038     470     6416    13.7 |  0.716 % |
c |       816 |   51786   146322 |   25342     807    11680    14.5 |  0.743 % |
c |      1322 |   51782   146314 |   27876    1311    19267    14.7 |  0.753 % |
c |      2081 |   51779   146308 |   30663    2069    41329    20.0 |  0.758 % |
c |      3221 |   51779   146308 |   33730    3209    66423    20.7 |  0.758 % |
c |      4929 |   51704   146143 |   37103    4901    95170    19.4 |  0.910 % |
c |      7491 |   51616   145961 |   40813    7431   151211    20.3 |  1.093 % |
c |     11337 |   51616   145961 |   44895   11277   333507    29.6 |  1.093 % |
c |     17107 |   51552   145821 |   49384   17006   628732    37.0 |  1.218 % |
c |     25757 |   51541   145799 |   54323   25655   872406    34.0 |  1.245 % |
c |     38731 |   51522   145760 |   59755   38628  1305809    33.8 |  1.250 % |
c |     58192 |   51511   145738 |   65730   58087  1868829    32.2 |  1.276 % |
c |     87384 |   51427   145551 |   72303   34293  1556116    45.4 |  1.401 % |
c |    131175 |   51333   145357 |   79534   78072  2859918    36.6 |  1.579 % |
c |    196861 |   51073   144802 |   87487   78021  2211324    28.3 |  1.951 % |
c |    295387 |   50937   144521 |   96236   25221   977684    38.8 |  2.222 % |
c |    443176 |   50760   144132 |  105860   90350  4545381    50.3 |  2.473 % |
c |    664859 |   50511   143593 |  116446   39851  1295851    32.5 |  2.939 % |
c |    997385 |   49929   142324 |  128090   58636  1675081    28.6 |  4.095 % |
c ==============================================================================
c Found solution: 6092816
c ---[   0]---> Sorter-cost:87749     Base: 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1045219 |  295362   715160 |   98454  106413  2710054    25.5 |  4.095 % |
c |   1045320 |  295362   715160 |  108299   14479   316331    21.8 |  0.814 % |
c |   1045470 |  295362   715160 |  119129   14629   317171    21.7 |  0.814 % |
c |   1045697 |  295362   715160 |  131042   14856   319402    21.5 |  0.814 % |
c |   1046035 |  295362   715160 |  144146   15194   322833    21.2 |  0.814 % |
c |   1046541 |  295362   715160 |  158561   15700   329947    21.0 |  0.814 % |
c |   1047303 |  295331   715095 |  174417   16447   337990    20.6 |  0.829 % |
c |   1048442 |  295331   715095 |  191858   17586   362087    20.6 |  0.829 % |
c |   1050151 |  295254   714917 |  211044   19193   380991    19.9 |  0.862 % |
c |   1052714 |  295254   714917 |  232149   21756   450886    20.7 |  0.862 % |
c |   1056558 |  295203   714806 |  255364   25582   511723    20.0 |  0.885 % |
c |   1062324 |  295203   714806 |  280900   31348   704532    22.5 |  0.885 % |
c |   1070973 |  295169   714731 |  308990   39967  1166896    29.2 |  0.896 % |
c |   1083947 |  295169   714731 |  339889   52941  1766041    33.4 |  0.896 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -TA1_bit_10 TA1_bit_9 TA1_bit_8 -TA1_bit_7 TA1_bit_6 -TA1_bit_5 TA1_bit_4 TA1_bit_3 TA1_bit_2 -TA1_bit_1 TA1_bit0 -TA1_bit1 TA1_bit2 TA1_bit3 TA1_bit4 TA1_bit5 -TA1_bit6 -TA2_bit_10 TA2_bit_9 -TA2_bit_8 TA2_bit_7 -TA2_bit_6 -TA2_bit_5 -TA2_bit_4 -TA2_bit_3 -TA2_bit_2 TA2_bit_1 TA2_bit0 TA2_bit1 TA2_bit2 TA2_bit3 -TA2_bit4 -TA2_bit5 TA2_bit6 -TA3_bit_10 -TA3_bit_9 -TA3_bit_8 -TA3_bit_7 TA3_bit_6 TA3_bit_5 TA3_bit_4 -TA3_bit_3 TA3_bit_2 TA3_bit_1 TA3_bit0 -TA3_bit1 -TA3_bit2 TA3_bit3 TA3_bit4 TA3_bit5 -TA3_bit6 -TA4_bit_10 -TA4_bit_9 -TA4_bit_8 -TA4_bit_7 TA4_bit_6 TA4_bit_5 TA4_bit_4 TA4_bit_3 TA4_bit_2 -TA4_bit_1 -TA4_bit0 TA4_bit1 -TA4_bit2 -TA4_bit3 TA4_bit4 TA4_bit5 -TA4_bit6 TB1_bit_10 TB1_bit_9 TB1_bit_8 TB1_bit_7 TB1_bit_6 TB1_bit_5 -TB1_bit_4 -TB1_bit_3 -TB1_bit_2 -TB1_bit_1 TB1_bit0 -TB1_bit1 -TB1_bit2 -TB1_bit3 TB1_bit4 TB1_bit5 -TB1_bit6 TB2_bit_10 TB2_bit_9 TB2_bit_8 TB2_bit_7 TB2_bit_6 TB2_bit_5 TB2_bit_4 TB2_bit_3 TB2_bit_2 TB2_bit_1 -TB2_bit0 -TB2_bit1 -TB2_bit2 TB2_bit3 -TB2_bit4 -TB2_bit5 -TB2_bit6 -TB3_bit_10 -TB3_bit_9 -TB3_bit_8 -TB3_bit_7 -TB3_bit_6 -TB3_bit_5 -TB3_bit_4 -TB3_bit_3 -TB3_bit_2 -TB3_bit_1 -TB3_bit0 -TB3_bit1 -TB3_bit2 -TB3_bit3 TB3_bit4 TB3_bit5 -TB3_bit6 -TB4_bit_10 -TB4_bit_9 TB4_bit_8 TB4_bit_7 TB4_bit_6 TB4_bit_5 -TB4_bit_4 -TB4_bit_3 TB4_bit_2 -TB4_bit_1 TB4_bit0 -TB4_bit1 TB4_bit2 -TB4_bit3 TB4_bit4 -TB4_bit5 -TB4_bit6 -TC1_bit_10 TC1_bit_9 -TC1_bit_8 -TC1_bit_7 -TC1_bit_6 -TC1_bit_5 -TC1_bit_4 -TC1_bit_3 -TC1_bit_2 -TC1_bit_1 -TC1_bit0 TC1_bit1 -TC1_bit2 -TC1_bit3 -TC1_bit4 TC1_bit5 -TC1_bit6 TC2_bit_10 TC2_bit_9 TC2_bit_8 -TC2_bit_7 TC2_bit_6 TC2_bit_5 -TC2_bit_4 -TC2_bit_3 -TC2_bit_2 -TC2_bit_1 TC2_bit0 -TC2_bit1 -TC2_bit2 TC2_bit3 TC2_bit4 -TC2_bit5 TC2_bit6 TC3_bit_10 -TC3_bit_9 TC3_bit_8 -TC3_bit_7 -TC3_bit_6 -TC3_bit_5 TC3_bit_4 -TC3_bit_3 TC3_bit_2 -TC3_bit_1 -TC3_bit0 TC3_bit1 -TC3_bit2 -TC3_bit3 -TC3_bit4 TC3_bit5 -TC3_bit6 -TC4_bit_10 -TC4_bit_9 -TC4_bit_8 -TC4_bit_7 -TC4_bit_6 TC4_bit_5 -TC4_bit_4 TC4_bit_3 TC4_bit_2 -TC4_bit_1 -TC4_bit0 TC4_bit1 TC4_bit2 -TC4_bit3 TC4_bit4 TC4_bit5 -TC4_bit6 -TD1_bit_10 -TD1_bit_9 TD1_bit_8 -TD1_bit_7 TD1_bit_6 TD1_bit_5 TD1_bit_4 -TD1_bit_3 TD1_bit_2 TD1_bit_1 -TD1_bit0 TD1_bit1 TD1_bit2 -TD1_bit3 TD1_bit4 -TD1_bit5 TD1_bit6 -TD2_bit_10 -TD2_bit_9 -TD2_bit_8 -TD2_bit_7 -TD2_bit_6 TD2_bit_5 -TD2_bit_4 TD2_bit_3 TD2_bit_2 -TD2_bit_1 -TD2_bit0 -TD2_bit1 -TD2_bit2 -TD2_bit3 -TD2_bit4 -TD2_bit5 TD2_bit6 -TD3_bit_10 -TD3_bit_9 TD3_bit_8 TD3_bit_7 -TD3_bit_6 TD3_bit_5 -TD3_bit_4 -TD3_bit_3 TD3_bit_2 TD3_bit_1 -TD3_bit0 -TD3_bit1 -TD3_bit2 TD3_bit3 -TD3_bit4 -TD3_bit5 -TD3_bit6 -TD4_bit_10 TD4_bit_9 -TD4_bit_8 TD4_bit_7 TD4_bit_6 -TD4_bit_5 TD4_bit_4 -TD4_bit_3 TD4_bit_2 TD4_bit_1 TD4_bit0 -TD4_bit1 TD4_bit2 TD4_bit3 -TD4_bit4 -TD4_bit5 -TD4_bit6 -TE1_bit_10 -TE1_bit_9 -TE1_bit_8 TE1_bit_7 TE1_bit_6 -TE1_bit_5 -TE1_bit_4 -TE1_bit_3 -TE1_bit_2 TE1_bit_1 -TE1_bit0 TE1_bit1 TE1_bit2 TE1_bit3 TE1_bit4 TE1_bit5 -TE1_bit6 -TE2_bit_10 -TE2_bit_9 -TE2_bit_8 -TE2_bit_7 TE2_bit_6 TE2_bit_5 -TE2_bit_4 -TE2_bit_3 -TE2_bit_2 -TE2_bit_1 TE2_bit0 -TE2_bit1 -TE2_bit2 TE2_bit3 TE2_bit4 -TE2_bit5 -TE2_bit6 TE3_bit_10 -TE3_bit_9 TE3_bit_8 TE3_bit_7 -TE3_bit_6 -TE3_bit_5 -TE3_bit_4 -TE3_bit_3 -TE3_bit_2 -TE3_bit_1 TE3_bit0 -TE3_bit1 -TE3_bit2 TE3_bit3 TE3_bit4 -TE3_bit5 -TE3_bit6 TE4_bit_10 -TE4_bit_9 -TE4_bit_8 TE4_bit_7 TE4_bit_6 -TE4_bit_5 -TE4_bit_4 TE4_bit_3 -TE4_bit_2 -TE4_bit_1 TE4_bit0 -TE4_bit1 -TE4_bit2 TE4_bit3 TE4_bit4 -TE4_bit5 -TE4_bit6 -UA1_bit_10 UA1_bit_9 UA1_bit_8 UA1_bit_7 -UA1_bit_6 UA1_bit_5 -UA1_bit_4 -UA1_bit_3 -UA1_bit_2 -UA1_bit_1 UA1_bit0 -UA1_bit1 -UA2_bit_10 -UA2_bit_9 -UA2_bit_8 -UA2_bit_7 -UA2_bit_6 -UA2_bit_5 -UA2_bit_4 -UA2_bit_3 -UA2_bit_2 -UA2_bit_1 -UA2_bit0 UA2_bit1 -UA3_bit_10 -UA3_bit_9 -UA3_bit_8 -UA3_bit_7 UA3_bit_6 UA3_bit_5 -UA3_bit_4 UA3_bit_3 UA3_bit_2 UA3_bit_1 -UA3_bit0 -UA3_bit1 -UA4_bit_10 -UA4_bit_9 -UA4_bit_8 -UA4_bit_7 -UA4_bit_6 UA4_bit_5 UA4_bit_4 UA4_bit_3 UA4_bit_2 -UA4_bit_1 UA4_bit0 -UA4_bit1 UB1_bit_10 -UB1_bit_9 -UB1_bit_8 -UB1_bit_7 -UB1_bit_6 -UB1_bit_5 -UB1_bit_4 -UB1_bit_3 UB1_bit_2 -UB1_bit_1 -UB1_bit0 -UB1_bit1 UB2_bit_10 -UB2_bit_9 -UB2_bit_8 -UB2_bit_7 -UB2_bit_6 -UB2_bit_5 -UB2_bit_4 -UB2_bit_3 -UB2_bit_2 -UB2_bit_1 -UB2_bit0 -UB2_bit1 -UB3_bit_10 -UB3_bit_9 -UB3_bit_8 -UB3_bit_7 -UB3_bit_6 -UB3_bit_5 -UB3_bit_4 -UB3_bit_3 -UB3_bit_2 -UB3_bit_1 -UB3_bit0 -UB3_bit1 -UB4_bit_10 -UB4_bit_9 UB4_bit_8 UB4_bit_7 UB4_bit_6 UB4_bit_5 UB4_bit_4 -UB4_bit_3 -UB4_bit_2 -UB4_bit_1 -UB4_bit0 -UB4_bit1 -UC1_bit_10 -UC1_bit_9 -UC1_bit_8 -UC1_bit_7 -UC1_bit_6 -UC1_bit_5 -UC1_bit_4 -UC1_bit_3 -UC1_bit_2 -UC1_bit_1 -UC1_bit0 -UC1_bit1 UC2_bit_10 -UC2_bit_9 -UC2_bit_8 -UC2_bit_7 -UC2_bit_6 -UC2_bit_5 -UC2_bit_4 -UC2_bit_3 -UC2_bit_2 -UC2_bit_1 UC2_bit0 -UC2_bit1 UC3_bit_10 UC3_bit_9 -UC3_bit_8 -UC3_bit_7 -UC3_bit_6 -UC3_bit_5 -UC3_bit_4 UC3_bit_3 UC3_bit_2 -UC3_bit_1 UC3_bit0 -UC3_bit1 -UC4_bit_10 UC4_bit_9 -UC4_bit_8 UC4_bit_7 -UC4_bit_6 -UC4_bit_5 UC4_bit_4 -UC4_bit_3 -UC4_bit_2 -UC4_bit_1 -UC4_bit0 -UC4_bit1 -UD1_bit_10 -UD1_bit_9 -UD1_bit_8 UD1_bit_7 UD1_bit_6 -UD1_bit_5 -UD1_bit_4 -UD1_bit_3 -UD1_bit_2 -UD1_bit_1 -UD1_bit0 -UD1_bit1 -UD2_bit_10 -UD2_bit_9 -UD2_bit_8 -UD2_bit_7 -UD2_bit_6 -UD2_bit_5 -UD2_bit_4 UD2_bit_3 -UD2_bit_2 UD2_bit_1 -UD2_bit0 -UD2_bit1 -UD3_bit_10 -UD3_bit_9 -UD3_bit_8 -UD3_bit_7 -UD3_bit_6 -UD3_bit_5 -UD3_bit_4 -UD3_bit_3 UD3_bit_2 UD3_bit_1 -UD3_bit0 -UD3_bit1 UD4_bit_10 UD4_bit_9 -UD4_bit_8 UD4_bit_7 UD4_bit_6 UD4_bit_5 UD4_bit_4 UD4_bit_3 -UD4_bit_2 -UD4_bit_1 -UD4_bit0 -UD4_bit1 -UE1_bit_10 -UE1_bit_9 -UE1_bit_8 UE1_bit_7 UE1_bit_6 -UE1_bit_5 -UE1_bit_4 -UE1_bit_3 UE1_bit_2 -UE1_bit_1 UE1_bit0 -UE1_bit1 -UE2_bit_10 -UE2_bit_9 -UE2_bit_8 -UE2_bit_7 -UE2_bit_6 -UE2_bit_5 -UE2_bit_4 -UE2_bit_3 UE2_bit_2 -UE2_bit_1 -UE2_bit0 -UE2_bit1 UE3_bit_10 -UE3_bit_9 -UE3_bit_8 -UE3_bit_7 -UE3_bit_6 -UE3_bit_5 -UE3_bit_4 -UE3_bit_3 -UE3_bit_2 -UE3_bit_1 UE3_bit0 -UE3_bit1 UE4_bit_10 -UE4_bit_9 -UE4_bit_8 UE4_bit_7 UE4_bit_6 UE4_bit_5 UE4_bit_4 UE4_bit_3 -UE4_bit_2 -UE4_bit_1 -UE4_bit0 -UE4_bit1 -VA1_bit_10 -VA1_bit_9 -VA1_bit_8 -VA1_bit_7 -VA1_bit_6 -VA1_bit_5 -VA1_bit_4 -VA1_bit_3 -VA1_bit_2 -VA1_bit_1 -VA1_bit0 VA1_bit1 VA2_bit_10 -VA2_bit_9 VA2_bit_8 VA2_bit_7 VA2_bit_6 VA2_bit_5 VA2_bit_4 VA2_bit_3 -VA2_bit_2 -VA2_bit_1 -VA2_bit0 -VA2_bit1 -VA3_bit_10 -VA3_bit_9 -VA3_bit_8 -VA3_bit_7 -VA3_bit_6 -VA3_bit_5 -VA3_bit_4 -VA3_bit_3 -VA3_bit_2 -VA3_bit_1 -VA3_bit0 VA3_bit1 -VA4_bit_10 VA4_bit_9 -VA4_bit_8 -VA4_bit_7 VA4_bit_6 -VA4_bit_5 -VA4_bit_4 VA4_bit_3 -VA4_bit_2 -VA4_bit_1 -VA4_bit0 -VA4_bit1 -VB1_bit_10 -VB1_bit_9 -VB1_bit_8 -VB1_bit_7 -VB1_bit_6 -VB1_bit_5 -VB1_bit_4 -VB1_bit_3 VB1_bit_2 -VB1_bit_1 -VB1_bit0 -VB1_bit1 -VB2_bit_10 -VB2_bit_9 -VB2_bit_8 -VB2_bit_7 -VB2_bit_6 -VB2_bit_5 -VB2_bit_4 -VB2_bit_3 -VB2_bit_2 -VB2_bit_1 -VB2_bit0 -VB2_bit1 VB3_bit_10 -VB3_bit_9 -VB3_bit_8 -VB3_bit_7 -VB3_bit_6 -VB3_bit_5 -VB3_bit_4 -VB3_bit_3 -VB3_bit_2 -VB3_bit_1 VB3_bit0 -VB3_bit1 VB4_bit_10 VB4_bit_9 VB4_bit_8 VB4_bit_7 -VB4_bit_6 VB4_bit_5 VB4_bit_4 VB4_bit_3 VB4_bit_2 -VB4_bit_1 -VB4_bit0 -VB4_bit1 VC1_bit_10 VC1_bit_9 VC1_bit_8 VC1_bit_7 -VC1_bit_6 VC1_bit_5 -VC1_bit_4 VC1_bit_3 -VC1_bit_2 VC1_bit_1 VC1_bit0 -VC1_bit1 -VC2_bit_10 -VC2_bit_9 -VC2_bit_8 -VC2_bit_7 -VC2_bit_6 VC2_bit_5 VC2_bit_4 -VC2_bit_3 -VC2_bit_2 -VC2_bit_1 -VC2_bit0 -VC2_bit1 -VC3_bit_10 -VC3_bit_9 -VC3_bit_8 -VC3_bit_7 -VC3_bit_6 VC3_bit_5 -VC3_bit_4 VC3_bit_3 -VC3_bit_2 -VC3_bit_1 -VC3_bit0 -VC3_bit1 VC4_bit_10 -VC4_bit_9 VC4_bit_8 VC4_bit_7 -VC4_bit_6 VC4_bit_5 -VC4_bit_4 VC4_bit_3 -VC4_bit_2 VC4_bit_1 VC4_bit0 -VC4_bit1 VD1_bit_10 -VD1_bit_9 VD1_bit_8 -VD1_bit_7 -VD1_bit_6 -VD1_bit_5 VD1_bit_4 -VD1_bit_3 VD1_bit_2 -VD1_bit_1 -VD1_bit0 -VD1_bit1 -VD2_bit_10 -VD2_bit_9 -VD2_bit_8 VD2_bit_7 -VD2_bit_6 -VD2_bit_5 -VD2_bit_4 -VD2_bit_3 -VD2_bit_2 -VD2_bit_1 -VD2_bit0 -VD2_bit1 -VD3_bit_10 VD3_bit_9 VD3_bit_8 VD3_bit_7 VD3_bit_6 -VD3_bit_5 -VD3_bit_4 -VD3_bit_3 -VD3_bit_2 -VD3_bit_1 -VD3_bit0 -VD3_bit1 -VD4_bit_10 -VD4_bit_9 -VD4_bit_8 -VD4_bit_7 -VD4_bit_6 -VD4_bit_5 -VD4_bit_4 -VD4_bit_3 -VD4_bit_2 -VD4_bit_1 -VD4_bit0 VD4_bit1 -VE1_bit_10 -VE1_bit_9 -VE1_bit_8 -VE1_bit_7 VE1_bit_6 -VE1_bit_5 -VE1_bit_4 VE1_bit_3 -VE1_bit_2 VE1_bit_1 -VE1_bit0 -VE1_bit1 -VE2_bit_10 -VE2_bit_9 -VE2_bit_8 -VE2_bit_7 -VE2_bit_6 -VE2_bit_5 -VE2_bit_4 VE2_bit_3 -VE2_bit_2 -VE2_bit_1 -VE2_bit0 -VE2_bit1 -VE3_bit_10 -VE3_bit_9 -VE3_bit_8 -VE3_bit_7 -VE3_bit_6 VE3_bit_5 -VE3_bit_4 -VE3_bit_3 VE3_bit_2 -VE3_bit_1 -VE3_bit0 -VE3_bit1 -VE4_bit_10 -VE4_bit_9 -VE4_bit_8 -VE4_bit_7 -VE4_bit_6 -VE4_bit_5 -VE4_bit_4 -VE4_bit_3 -VE4_bit_2 -VE4_bit_1 -VE4_bit0 -VE4_bit1 -WA1_bit_10 -WA1_bit_9 WA1_bit_8 -WA1_bit_7 -WA1_bit_6 -WA1_bit_5 -WA1_bit_4 -WA1_bit_3 -WA1_bit_2 -WA1_bit_1 -WA1_bit0 -WA1_bit1 -WA1_bit2 -WA1_bit3 -WA1_bit4 -WA1_bit5 WA1_bit6 WA2_bit_10 -WA2_bit_9 WA2_bit_8 WA2_bit_7 -WA2_bit_6 -WA2_bit_5 -WA2_bit_4 -WA2_bit_3 WA2_bit_2 -WA2_bit_1 -WA2_bit0 -WA2_bit1 -WA2_bit2 WA2_bit3 WA2_bit4 -WA2_bit5 WA2_bit6 -WA3_bit_10 -WA3_bit_9 -WA3_bit_8 -WA3_bit_7 -WA3_bit_6 WA3_bit_5 -WA3_bit_4 -WA3_bit_3 WA3_bit_2 -WA3_bit_1 WA3_bit0 WA3_bit1 -WA3_bit2 -WA3_bit3 -WA3_bit4 -WA3_bit5 WA3_bit6 -WA4_bit_10 WA4_bit_9 WA4_bit_8 WA4_bit_7 WA4_bit_6 WA4_bit_5 -WA4_bit_4 -WA4_bit_3 WA4_bit_2 WA4_bit_1 WA4_bit0 -WA4_bit1 -WA4_bit2 -WA4_bit3 -WA4_bit4 -WA4_bit5 WA4_bit6 -WB1_bit_10 -WB1_bit_9 -WB1_bit_8 -WB1_bit_7 -WB1_bit_6 -WB1_bit_5 WB1_bit_4 -WB1_bit_3 -WB1_bit_2 WB1_bit_1 -WB1_bit0 -WB1_bit1 WB1_bit2 -WB1_bit3 WB1_bit4 WB1_bit5 -WB1_bit6 -WB2_bit_10 -WB2_bit_9 -WB2_bit_8 -WB2_bit_7 -WB2_bit_6 -WB2_bit_5 -WB2_bit_4 -WB2_bit_3 -WB2_bit_2 -WB2_bit_1 -WB2_bit0 -WB2_bit1 -WB2_bit2 -WB2_bit3 WB2_bit4 -WB2_bit5 -WB2_bit6 WB3_bit_10 WB3_bit_9 WB3_bit_8 WB3_bit_7 WB3_bit_6 WB3_bit_5 WB3_bit_4 WB3_bit_3 WB3_bit_2 -WB3_bit_1 WB3_bit0 -WB3_bit1 -WB3_bit2 WB3_bit3 WB3_bit4 WB3_bit5 -WB3_bit6 WB4_bit_10 -WB4_bit_9 -WB4_bit_8 WB4_bit_7 -WB4_bit_6 -WB4_bit_5 WB4_bit_4 WB4_bit_3 WB4_bit_2 WB4_bit_1 -WB4_bit0 WB4_bit1 -WB4_bit2 -WB4_bit3 -WB4_bit4 WB4_bit5 -WB4_bit6 WC1_bit_10 WC1_bit_9 -WC1_bit_8 -WC1_bit_7 WC1_bit_6 -WC1_bit_5 WC1_bit_4 -WC1_bit_3 WC1_bit_2 WC1_bit_1 WC1_bit0 WC1_bit1 -WC1_bit2 -WC1_bit3 -WC1_bit4 WC1_bit5 -WC1_bit6 -WC2_bit_10 -WC2_bit_9 -WC2_bit_8 WC2_bit_7 WC2_bit_6 -WC2_bit_5 WC2_bit_4 WC2_bit_3 WC2_bit_2 WC2_bit_1 -WC2_bit0 -WC2_bit1 -WC2_bit2 -WC2_bit3 -WC2_bit4 WC2_bit5 WC2_bit6 -WC3_bit_10 -WC3_bit_9 -WC3_bit_8 WC3_bit_7 -WC3_bit_6 WC3_bit_5 -WC3_bit_4 -WC3_bit_3 -WC3_bit_2 -WC3_bit_1 -WC3_bit0 WC3_bit1 WC3_bit2 WC3_bit3 -WC3_bit4 WC3_bit5 -WC3_bit6 WC4_bit_10 -WC4_bit_9 WC4_bit_8 WC4_bit_7 WC4_bit_6 WC4_bit_5 -WC4_bit_4 -WC4_bit_3 WC4_bit_2 WC4_bit_1 -WC4_bit0 WC4_bit1 -WC4_bit2 -WC4_bit3 -WC4_bit4 -WC4_bit5 WC4_bit6 WD1_bit_10 WD1_bit_9 WD1_bit_8 -WD1_bit_7 -WD1_bit_6 -WD1_bit_5 WD1_bit_4 -WD1_bit_3 -WD1_bit_2 -WD1_bit_1 -WD1_bit0 WD1_bit1 -WD1_bit2 WD1_bit3 WD1_bit4 -WD1_bit5 WD1_bit6 -WD2_bit_10 -WD2_bit_9 -WD2_bit_8 WD2_bit_7 WD2_bit_6 -WD2_bit_5 -WD2_bit_4 -WD2_bit_3 -WD2_bit_2 -WD2_bit_1 -WD2_bit0 -WD2_bit1 -WD2_bit2 WD2_bit3 -WD2_bit4 -WD2_bit5 WD2_bit6 -WD3_bit_10 WD3_bit_9 WD3_bit_8 WD3_bit_7 -WD3_bit_6 -WD3_bit_5 -WD3_bit_4 -WD3_bit_3 -WD3_bit_2 -WD3_bit_1 -WD3_bit0 -WD3_bit1 WD3_bit2 -WD3_bit3 WD3_bit4 -WD3_bit5 -WD3_bit6 WD4_bit_10 -WD4_bit_9 WD4_bit_8 -WD4_bit_7 WD4_bit_6 -WD4_bit_5 WD4_bit_4 -WD4_bit_3 -WD4_bit_2 -WD4_bit_1 -WD4_bit0 WD4_bit1 -WD4_bit2 WD4_bit3 WD4_bit4 -WD4_bit5 -WD4_bit6 -WE1_bit_10 -WE1_bit_9 -WE1_bit_8 -WE1_bit_7 -WE1_bit_6 WE1_bit_5 -WE1_bit_4 WE1_bit_3 -WE1_bit_2 WE1_bit_1 -WE1_bit0 WE1_bit1 -WE1_bit2 -WE1_bit3 -WE1_bit4 -WE1_bit5 WE1_bit6 -WE2_bit_10 -WE2_bit_9 -WE2_bit_8 -WE2_bit_7 WE2_bit_6 WE2_bit_5 -WE2_bit_4 WE2_bit_3 -WE2_bit_2 -WE2_bit_1 -WE2_bit0 -WE2_bit1 -WE2_bit2 -WE2_bit3 -WE2_bit4 WE2_bit5 -WE2_bit6 -WE3_bit_10 WE3_bit_9 WE3_bit_8 WE3_bit_7 -WE3_bit_6 WE3_bit_5 WE3_bit_4 WE3_bit_3 -WE3_bit_2 -WE3_bit_1 -WE3_bit0 -WE3_bit1 WE3_bit2 -WE3_bit3 -WE3_bit4 WE3_bit5 -WE3_bit6 -WE4_bit_10 WE4_bit_9 -WE4_bit_8 -WE4_bit_7 WE4_bit_6 -WE4_bit_5 -WE4_bit_4 WE4_bit_3 WE4_bit_2 -WE4_bit_1 WE4_bit0 WE4_bit1 WE4_bit2 -WE4_bit3 -WE4_bit4 WE4_bit5 -WE4_bit6 -A1_bit0 -B1_bit0 -C1_bit0 -D1_bit0 -E1_bit0 -AB1_bit0 -AC1_bit0 -AD1_bit0 -AE1_bit0 -BC1_bit0 -BD1_bit0 -BE1_bit0 -CD1_bit0 -CE1_bit0 -DE1_bit0 -ABC1_bit0 -ABD1_b

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/23047/stat): 23047 (minisat+_script) R 23046 23047 2660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1851937187 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/23047/statm): 174 3 169 147 0 27 0
[pid=23047] 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=23048
New process pid=23049
New process pid=23050
One traced child (pid=23049) exited with status: 0
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
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=23050) exited with status: 0
One traced child (pid=23048) exited with status: 0
New process pid=23051
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-rgn.opb

[startup+10.0038 s]
Raw data (loadavg): 0.82 0.93 0.88 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 3284 0 0 0 966 14 0 0 22 0 1 0 1851937192 12279808 2676 4294967295 134512640 135094434 3221224432 3221223088 134558232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 2998 2676 145 145 0 2853 0
[pid=23051] vsize: 11992
Current children cumulated CPU time (s) 9.8
Current children cumulated vsize (Kb) 14116

[startup+20.0056 s]
Raw data (loadavg): 0.85 0.93 0.88 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 4189 0 0 0 1954 19 0 0 25 0 1 0 1851937192 16060416 3581 4294967295 134512640 135094434 3221224432 3221223104 134556166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23051/statm): 3921 3581 145 145 0 3776 0
[pid=23051] vsize: 15684
Current children cumulated CPU time (s) 19.73
Current children cumulated vsize (Kb) 17808

[startup+30.0073 s]
Raw data (loadavg): 0.87 0.93 0.88 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 4843 0 0 0 2943 24 0 0 25 0 1 0 1851937192 18694144 4235 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23051/statm): 4564 4235 145 145 0 4419 0
[pid=23051] vsize: 18256
Current children cumulated CPU time (s) 29.67
Current children cumulated vsize (Kb) 20380

[startup+40.008 s]
Raw data (loadavg): 0.89 0.93 0.88 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 5425 0 0 0 3935 28 0 0 25 0 1 0 1851937192 21331968 4817 4294967295 134512640 135094434 3221224432 3221223184 134559163 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23051/statm): 5208 4817 145 145 0 5063 0
[pid=23051] vsize: 20832
Current children cumulated CPU time (s) 39.63
Current children cumulated vsize (Kb) 22956

[startup+50.0097 s]
Raw data (loadavg): 0.91 0.93 0.88 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 5426 0 0 0 4935 28 0 0 25 0 1 0 1851937192 21331968 4818 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23051/statm): 5208 4818 145 145 0 5063 0
[pid=23051] vsize: 20832
Current children cumulated CPU time (s) 49.63
Current children cumulated vsize (Kb) 22956

[startup+60.0104 s]
Raw data (loadavg): 0.92 0.94 0.88 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 5462 0 0 0 5934 29 0 0 25 0 1 0 1851937192 21528576 4854 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23051/statm): 5256 4854 145 145 0 5111 0
[pid=23051] vsize: 21024
Current children cumulated CPU time (s) 59.63
Current children cumulated vsize (Kb) 23148

[startup+70.0122 s]
Raw data (loadavg): 0.93 0.94 0.89 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 5681 0 0 0 6930 30 0 0 25 0 1 0 1851937192 22433792 5073 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23051/statm): 5477 5073 145 145 0 5332 0
[pid=23051] vsize: 21908
Current children cumulated CPU time (s) 69.6
Current children cumulated vsize (Kb) 24032

[startup+80.0129 s]
Raw data (loadavg): 0.94 0.94 0.89 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6329 0 0 0 7920 34 0 0 25 0 1 0 1851937192 25079808 5721 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23051/statm): 6123 5721 145 145 0 5978 0
[pid=23051] vsize: 24492
Current children cumulated CPU time (s) 79.54
Current children cumulated vsize (Kb) 26616

[startup+90.0136 s]
Raw data (loadavg): 0.95 0.94 0.89 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6376 0 0 0 8919 35 0 0 25 0 1 0 1851937192 25264128 5768 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23051/statm): 6168 5768 145 145 0 6023 0
[pid=23051] vsize: 24672
Current children cumulated CPU time (s) 89.54
Current children cumulated vsize (Kb) 26796

[startup+100.015 s]
Raw data (loadavg): 0.96 0.94 0.89 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6376 0 0 0 9918 36 0 0 25 0 1 0 1851937192 25264128 5768 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23051/statm): 6168 5768 145 145 0 6023 0
[pid=23051] vsize: 24672
Current children cumulated CPU time (s) 99.54
Current children cumulated vsize (Kb) 26796

[startup+110.016 s]
Raw data (loadavg): 0.96 0.94 0.89 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6376 0 0 0 10918 36 0 0 25 0 1 0 1851937192 25264128 5768 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23051/statm): 6168 5768 145 145 0 6023 0
[pid=23051] vsize: 24672
Current children cumulated CPU time (s) 109.54
Current children cumulated vsize (Kb) 26796

[startup+120.018 s]
Raw data (loadavg): 0.97 0.94 0.89 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6390 0 0 0 11917 37 0 0 25 0 1 0 1851937192 25329664 5782 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23051/statm): 6184 5782 145 145 0 6039 0
[pid=23051] vsize: 24736
Current children cumulated CPU time (s) 119.54
Current children cumulated vsize (Kb) 26860

[startup+130.019 s]
Raw data (loadavg): 0.97 0.95 0.89 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6426 0 0 0 12916 38 0 0 25 0 1 0 1851937192 25493504 5818 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23051/statm): 6224 5818 145 145 0 6079 0
[pid=23051] vsize: 24896
Current children cumulated CPU time (s) 129.54
Current children cumulated vsize (Kb) 27020

[startup+140.019 s]
Raw data (loadavg): 0.98 0.95 0.89 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6432 0 0 0 13916 38 0 0 25 0 1 0 1851937192 25493504 5824 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23051/statm): 6224 5824 145 145 0 6079 0
[pid=23051] vsize: 24896
Current children cumulated CPU time (s) 139.54
Current children cumulated vsize (Kb) 27020

[startup+150.021 s]
Raw data (loadavg): 0.98 0.95 0.89 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6432 0 0 0 14915 39 0 0 25 0 1 0 1851937192 25493504 5824 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23051/statm): 6224 5824 145 145 0 6079 0
[pid=23051] vsize: 24896
Current children cumulated CPU time (s) 149.54
Current children cumulated vsize (Kb) 27020

[startup+160.022 s]
Raw data (loadavg): 0.98 0.95 0.89 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6447 0 0 0 15915 39 0 0 25 0 1 0 1851937192 25591808 5839 4294967295 134512640 135094434 3221224432 3221223088 134558240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23051/statm): 6248 5839 145 145 0 6103 0
[pid=23051] vsize: 24992
Current children cumulated CPU time (s) 159.54
Current children cumulated vsize (Kb) 27116

[startup+170.022 s]
Raw data (loadavg): 0.98 0.95 0.89 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6460 0 0 0 16914 40 0 0 25 0 1 0 1851937192 25657344 5852 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23051/statm): 6264 5852 145 145 0 6119 0
[pid=23051] vsize: 25056
Current children cumulated CPU time (s) 169.54
Current children cumulated vsize (Kb) 27180

[startup+180.023 s]
Raw data (loadavg): 0.99 0.95 0.90 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6750 0 0 0 17909 42 0 0 25 0 1 0 1851937192 26869760 6142 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23051/statm): 6560 6142 145 145 0 6415 0
[pid=23051] vsize: 26240
Current children cumulated CPU time (s) 179.51
Current children cumulated vsize (Kb) 28364

[startup+190.024 s]
Raw data (loadavg): 0.99 0.95 0.90 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6957 0 0 0 18907 43 0 0 25 0 1 0 1851937192 27783168 6349 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 6783 6349 145 145 0 6638 0
[pid=23051] vsize: 27132
Current children cumulated CPU time (s) 189.5
Current children cumulated vsize (Kb) 29256

[startup+200.025 s]
Raw data (loadavg): 0.99 0.95 0.90 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6959 0 0 0 19907 43 0 0 25 0 1 0 1851937192 27783168 6351 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23051/statm): 6783 6351 145 145 0 6638 0
[pid=23051] vsize: 27132
Current children cumulated CPU time (s) 199.5
Current children cumulated vsize (Kb) 29256

[startup+210.025 s]
Raw data (loadavg): 0.99 0.95 0.90 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6968 0 0 0 20907 43 0 0 25 0 1 0 1851937192 27832320 6360 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 6795 6360 145 145 0 6650 0
[pid=23051] vsize: 27180
Current children cumulated CPU time (s) 209.5
Current children cumulated vsize (Kb) 29304

[startup+220.027 s]
Raw data (loadavg): 0.99 0.95 0.90 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 7017 0 0 0 21907 43 0 0 25 0 1 0 1851937192 28061696 6409 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 6851 6409 145 145 0 6706 0
[pid=23051] vsize: 27404
Current children cumulated CPU time (s) 219.5
Current children cumulated vsize (Kb) 29528

[startup+230.028 s]
Raw data (loadavg): 0.99 0.95 0.90 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 7065 0 0 0 22906 43 0 0 25 0 1 0 1851937192 28258304 6457 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 6899 6457 145 145 0 6754 0
[pid=23051] vsize: 27596
Current children cumulated CPU time (s) 229.49
Current children cumulated vsize (Kb) 29720

[startup+240.029 s]
Raw data (loadavg): 0.99 0.96 0.90 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 7174 0 0 0 23906 44 0 0 25 0 1 0 1851937192 28790784 6566 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 7029 6566 145 145 0 6884 0
[pid=23051] vsize: 28116
Current children cumulated CPU time (s) 239.5
Current children cumulated vsize (Kb) 30240

[startup+250.029 s]
Raw data (loadavg): 0.99 0.96 0.90 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 7395 0 0 0 24902 45 0 0 25 0 1 0 1851937192 29704192 6787 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 7252 6787 145 145 0 7107 0
[pid=23051] vsize: 29008
Current children cumulated CPU time (s) 249.47
Current children cumulated vsize (Kb) 31132

[startup+260.03 s]
Raw data (loadavg): 0.99 0.96 0.90 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 7646 0 0 0 25898 47 0 0 25 0 1 0 1851937192 30732288 7038 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 7503 7038 145 145 0 7358 0
[pid=23051] vsize: 30012
Current children cumulated CPU time (s) 259.45
Current children cumulated vsize (Kb) 32136

[startup+270.031 s]
Raw data (loadavg): 0.99 0.96 0.90 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 7824 0 0 0 26895 49 0 0 25 0 1 0 1851937192 31477760 7216 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 7685 7216 145 145 0 7540 0
[pid=23051] vsize: 30740
Current children cumulated CPU time (s) 269.44
Current children cumulated vsize (Kb) 32864

[startup+280.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 7824 0 0 0 27895 49 0 0 25 0 1 0 1851937192 31477760 7216 4294967295 134512640 135094434 3221224432 3221223088 134558174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 7685 7216 145 145 0 7540 0
[pid=23051] vsize: 30740
Current children cumulated CPU time (s) 279.44
Current children cumulated vsize (Kb) 32864

[startup+290.032 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 7824 0 0 0 28895 49 0 0 25 0 1 0 1851937192 31477760 7216 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 7685 7216 145 145 0 7540 0
[pid=23051] vsize: 30740
Current children cumulated CPU time (s) 289.44
Current children cumulated vsize (Kb) 32864

[startup+300.033 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 7824 0 0 0 29896 49 0 0 25 0 1 0 1851937192 31477760 7216 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 7685 7216 145 145 0 7540 0
[pid=23051] vsize: 30740
Current children cumulated CPU time (s) 299.45
Current children cumulated vsize (Kb) 32864

[startup+310.034 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 7824 0 0 0 30896 49 0 0 25 0 1 0 1851937192 31477760 7216 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 7685 7216 145 145 0 7540 0
[pid=23051] vsize: 30740
Current children cumulated CPU time (s) 309.45
Current children cumulated vsize (Kb) 32864

[startup+320.034 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 8236 0 0 0 31890 51 0 0 25 0 1 0 1851937192 33218560 7628 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 8110 7628 145 145 0 7965 0
[pid=23051] vsize: 32440
Current children cumulated CPU time (s) 319.41
Current children cumulated vsize (Kb) 34564

[startup+330.035 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 8616 0 0 0 32884 54 0 0 25 0 1 0 1851937192 34893824 8008 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 8519 8008 145 145 0 8374 0
[pid=23051] vsize: 34076
Current children cumulated CPU time (s) 329.38
Current children cumulated vsize (Kb) 36200

[startup+340.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 8893 0 0 0 33881 55 0 0 25 0 1 0 1851937192 36110336 8285 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 8816 8285 145 145 0 8671 0
[pid=23051] vsize: 35264
Current children cumulated CPU time (s) 339.36
Current children cumulated vsize (Kb) 37388

[startup+350.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 9203 0 0 0 34876 58 0 0 25 0 1 0 1851937192 37462016 8595 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 9146 8595 145 145 0 9001 0
[pid=23051] vsize: 36584
Current children cumulated CPU time (s) 349.34
Current children cumulated vsize (Kb) 38708

[startup+360.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 9477 0 0 0 35871 60 0 0 25 0 1 0 1851937192 38645760 8869 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 9435 8869 145 145 0 9290 0
[pid=23051] vsize: 37740
Current children cumulated CPU time (s) 359.31
Current children cumulated vsize (Kb) 39864

[startup+370.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 9757 0 0 0 36867 62 0 0 25 0 1 0 1851937192 39817216 9149 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 9721 9149 145 145 0 9576 0
[pid=23051] vsize: 38884
Current children cumulated CPU time (s) 369.29
Current children cumulated vsize (Kb) 41008

[startup+380.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10195 0 0 0 37860 64 0 0 25 0 1 0 1851937192 41603072 9587 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10157 9587 145 145 0 10012 0
[pid=23051] vsize: 40628
Current children cumulated CPU time (s) 379.24
Current children cumulated vsize (Kb) 42752

[startup+390.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10195 0 0 0 38861 64 0 0 25 0 1 0 1851937192 41603072 9587 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10157 9587 145 145 0 10012 0
[pid=23051] vsize: 40628
Current children cumulated CPU time (s) 389.25
Current children cumulated vsize (Kb) 42752

[startup+400.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10196 0 0 0 39860 64 0 0 25 0 1 0 1851937192 41603072 9588 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10157 9588 145 145 0 10012 0
[pid=23051] vsize: 40628
Current children cumulated CPU time (s) 399.24
Current children cumulated vsize (Kb) 42752

[startup+410.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10196 0 0 0 40861 64 0 0 25 0 1 0 1851937192 41603072 9588 4294967295 134512640 135094434 3221224432 3221223024 134557297 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10157 9588 145 145 0 10012 0
[pid=23051] vsize: 40628
Current children cumulated CPU time (s) 409.25
Current children cumulated vsize (Kb) 42752

[startup+420.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10219 0 0 0 41861 64 0 0 25 0 1 0 1851937192 41734144 9611 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10189 9611 145 145 0 10044 0
[pid=23051] vsize: 40756
Current children cumulated CPU time (s) 419.25
Current children cumulated vsize (Kb) 42880

[startup+430.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10220 0 0 0 42861 64 0 0 25 0 1 0 1851937192 41734144 9612 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10189 9612 145 145 0 10044 0
[pid=23051] vsize: 40756
Current children cumulated CPU time (s) 429.25
Current children cumulated vsize (Kb) 42880

[startup+440.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10240 0 0 0 43861 64 0 0 25 0 1 0 1851937192 41865216 9632 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10221 9632 145 145 0 10076 0
[pid=23051] vsize: 40884
Current children cumulated CPU time (s) 439.25
Current children cumulated vsize (Kb) 43008

[startup+450.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10242 0 0 0 44862 64 0 0 25 0 1 0 1851937192 41865216 9634 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10221 9634 145 145 0 10076 0
[pid=23051] vsize: 40884
Current children cumulated CPU time (s) 449.26
Current children cumulated vsize (Kb) 43008

[startup+460.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10264 0 0 0 45861 65 0 0 25 0 1 0 1851937192 41996288 9656 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10253 9656 145 145 0 10108 0
[pid=23051] vsize: 41012
Current children cumulated CPU time (s) 459.26
Current children cumulated vsize (Kb) 43136

[startup+470.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10306 0 0 0 46861 65 0 0 25 0 1 0 1851937192 42258432 9698 4294967295 134512640 135094434 3221224432 3221223088 134558144 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10317 9698 145 145 0 10172 0
[pid=23051] vsize: 41268
Current children cumulated CPU time (s) 469.26
Current children cumulated vsize (Kb) 43392

[startup+480.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10328 0 0 0 47862 65 0 0 25 0 1 0 1851937192 42389504 9720 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10349 9720 145 145 0 10204 0
[pid=23051] vsize: 41396
Current children cumulated CPU time (s) 479.27
Current children cumulated vsize (Kb) 43520

[startup+490.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10334 0 0 0 48862 65 0 0 25 0 1 0 1851937192 42389504 9726 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10349 9726 145 145 0 10204 0
[pid=23051] vsize: 41396
Current children cumulated CPU time (s) 489.27
Current children cumulated vsize (Kb) 43520

[startup+500.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10362 0 0 0 49862 65 0 0 25 0 1 0 1851937192 42520576 9754 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10381 9754 145 145 0 10236 0
[pid=23051] vsize: 41524
Current children cumulated CPU time (s) 499.27
Current children cumulated vsize (Kb) 43648

[startup+510.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10385 0 0 0 50862 65 0 0 25 0 1 0 1851937192 42651648 9777 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10413 9777 145 145 0 10268 0
[pid=23051] vsize: 41652
Current children cumulated CPU time (s) 509.27
Current children cumulated vsize (Kb) 43776

[startup+520.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10410 0 0 0 51862 65 0 0 25 0 1 0 1851937192 42782720 9802 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10445 9802 145 145 0 10300 0
[pid=23051] vsize: 41780
Current children cumulated CPU time (s) 519.27
Current children cumulated vsize (Kb) 43904

[startup+530.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10430 0 0 0 52862 66 0 0 25 0 1 0 1851937192 42913792 9822 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10477 9822 145 145 0 10332 0
[pid=23051] vsize: 41908
Current children cumulated CPU time (s) 529.28
Current children cumulated vsize (Kb) 44032

[startup+540.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10433 0 0 0 53862 66 0 0 25 0 1 0 1851937192 42913792 9825 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10477 9825 145 145 0 10332 0
[pid=23051] vsize: 41908
Current children cumulated CPU time (s) 539.28
Current children cumulated vsize (Kb) 44032

[startup+550.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10433 0 0 0 54863 66 0 0 25 0 1 0 1851937192 42913792 9825 4294967295 134512640 135094434 3221224432 3221223024 134551463 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10477 9825 145 145 0 10332 0
[pid=23051] vsize: 41908
Current children cumulated CPU time (s) 549.29
Current children cumulated vsize (Kb) 44032

[startup+560.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10433 0 0 0 55863 66 0 0 25 0 1 0 1851937192 42913792 9825 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10477 9825 145 145 0 10332 0
[pid=23051] vsize: 41908
Current children cumulated CPU time (s) 559.29
Current children cumulated vsize (Kb) 44032

[startup+570.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10433 0 0 0 56863 66 0 0 25 0 1 0 1851937192 42913792 9825 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10477 9825 145 145 0 10332 0
[pid=23051] vsize: 41908
Current children cumulated CPU time (s) 569.29
Current children cumulated vsize (Kb) 44032

[startup+580.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10437 0 0 0 57863 66 0 0 25 0 1 0 1851937192 42913792 9829 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10477 9829 145 145 0 10332 0
[pid=23051] vsize: 41908
Current children cumulated CPU time (s) 579.29
Current children cumulated vsize (Kb) 44032

[startup+590.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10437 0 0 0 58864 66 0 0 25 0 1 0 1851937192 42913792 9829 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10477 9829 145 145 0 10332 0
[pid=23051] vsize: 41908
Current children cumulated CPU time (s) 589.3
Current children cumulated vsize (Kb) 44032

[startup+600.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10437 0 0 0 59864 66 0 0 25 0 1 0 1851937192 42913792 9829 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10477 9829 145 145 0 10332 0
[pid=23051] vsize: 41908
Current children cumulated CPU time (s) 599.3
Current children cumulated vsize (Kb) 44032

[startup+610.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10437 0 0 0 60864 66 0 0 25 0 1 0 1851937192 42913792 9829 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10477 9829 145 145 0 10332 0
[pid=23051] vsize: 41908
Current children cumulated CPU time (s) 609.3
Current children cumulated vsize (Kb) 44032

[startup+620.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10437 0 0 0 61864 66 0 0 25 0 1 0 1851937192 42913792 9829 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10477 9829 145 145 0 10332 0
[pid=23051] vsize: 41908
Current children cumulated CPU time (s) 619.3
Current children cumulated vsize (Kb) 44032

[startup+630.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10437 0 0 0 62864 66 0 0 25 0 1 0 1851937192 42913792 9829 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10477 9829 145 145 0 10332 0
[pid=23051] vsize: 41908
Current children cumulated CPU time (s) 629.3
Current children cumulated vsize (Kb) 44032

[startup+640.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10437 0 0 0 63865 66 0 0 25 0 1 0 1851937192 42913792 9829 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10477 9829 145 145 0 10332 0
[pid=23051] vsize: 41908
Current children cumulated CPU time (s) 639.31
Current children cumulated vsize (Kb) 44032

[startup+650.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10437 0 0 0 64865 66 0 0 25 0 1 0 1851937192 42913792 9829 4294967295 134512640 135094434 3221224432 3221223024 134557357 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10477 9829 145 145 0 10332 0
[pid=23051] vsize: 41908
Current children cumulated CPU time (s) 649.31
Current children cumulated vsize (Kb) 44032

[startup+660.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10437 0 0 0 65865 66 0 0 25 0 1 0 1851937192 42913792 9829 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10477 9829 145 145 0 10332 0
[pid=23051] vsize: 41908
Current children cumulated CPU time (s) 659.31
Current children cumulated vsize (Kb) 44032

[startup+670.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10471 0 0 0 66865 66 0 0 25 0 1 0 1851937192 43175936 9863 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10541 9863 145 145 0 10396 0
[pid=23051] vsize: 42164
Current children cumulated CPU time (s) 669.31
Current children cumulated vsize (Kb) 44288

[startup+680.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10473 0 0 0 67866 66 0 0 25 0 1 0 1851937192 43175936 9865 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10541 9865 145 145 0 10396 0
[pid=23051] vsize: 42164
Current children cumulated CPU time (s) 679.32
Current children cumulated vsize (Kb) 44288

[startup+690.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10473 0 0 0 68866 67 0 0 25 0 1 0 1851937192 43175936 9865 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10541 9865 145 145 0 10396 0
[pid=23051] vsize: 42164
Current children cumulated CPU time (s) 689.33
Current children cumulated vsize (Kb) 44288

[startup+700.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10473 0 0 0 69865 67 0 0 25 0 1 0 1851937192 43175936 9865 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23051/statm): 10541 9865 145 145 0 10396 0
[pid=23051] vsize: 42164
Current children cumulated CPU time (s) 699.32
Current children cumulated vsize (Kb) 44288

[startup+710.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10473 0 0 0 70864 67 0 0 25 0 1 0 1851937192 43175936 9865 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/23051/statm): 10541 9865 145 145 0 10396 0
[pid=23051] vsize: 42164
Current children cumulated CPU time (s) 709.31
Current children cumulated vsize (Kb) 44288

[startup+720.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10473 0 0 0 71863 68 0 0 25 0 1 0 1851937192 43175936 9865 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10541 9865 145 145 0 10396 0
[pid=23051] vsize: 42164
Current children cumulated CPU time (s) 719.31
Current children cumulated vsize (Kb) 44288

[startup+730.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10473 0 0 0 72863 69 0 0 25 0 1 0 1851937192 43175936 9865 4294967295 134512640 135094434 3221224432 3221223104 134555795 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10541 9865 145 145 0 10396 0
[pid=23051] vsize: 42164
Current children cumulated CPU time (s) 729.32
Current children cumulated vsize (Kb) 44288

[startup+740.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10476 0 0 0 73863 69 0 0 25 0 1 0 1851937192 43175936 9868 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10541 9868 145 145 0 10396 0
[pid=23051] vsize: 42164
Current children cumulated CPU time (s) 739.32
Current children cumulated vsize (Kb) 44288

[startup+750.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10683 0 0 0 74860 71 0 0 25 0 1 0 1851937192 44027904 10075 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10749 10075 145 145 0 10604 0
[pid=23051] vsize: 42996
Current children cumulated CPU time (s) 749.31
Current children cumulated vsize (Kb) 45120

[startup+760.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10800 0 0 0 75858 71 0 0 25 0 1 0 1851937192 44498944 10192 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10864 10192 145 145 0 10719 0
[pid=23051] vsize: 43456
Current children cumulated CPU time (s) 759.29
Current children cumulated vsize (Kb) 45580

[startup+770.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10826 0 0 0 76858 72 0 0 25 0 1 0 1851937192 44630016 10218 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10896 10218 145 145 0 10751 0
[pid=23051] vsize: 43584
Current children cumulated CPU time (s) 769.3
Current children cumulated vsize (Kb) 45708

[startup+780.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10835 0 0 0 77858 72 0 0 25 0 1 0 1851937192 44756992 10227 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10927 10227 145 145 0 10782 0
[pid=23051] vsize: 43708
Current children cumulated CPU time (s) 779.3
Current children cumulated vsize (Kb) 45832

[startup+790.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10855 0 0 0 78858 72 0 0 25 0 1 0 1851937192 44822528 10247 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 10943 10247 145 145 0 10798 0
[pid=23051] vsize: 43772
Current children cumulated CPU time (s) 789.3
Current children cumulated vsize (Kb) 45896

[startup+800.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10906 0 0 0 79858 73 0 0 25 0 1 0 1851937192 45215744 10298 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 11039 10298 145 145 0 10894 0
[pid=23051] vsize: 44156
Current children cumulated CPU time (s) 799.31
Current children cumulated vsize (Kb) 46280

[startup+810.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10988 0 0 0 80857 73 0 0 25 0 1 0 1851937192 45674496 10380 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 11151 10380 145 145 0 11006 0
[pid=23051] vsize: 44604
Current children cumulated CPU time (s) 809.3
Current children cumulated vsize (Kb) 46728

[startup+820.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 11015 0 0 0 81857 73 0 0 25 0 1 0 1851937192 45740032 10407 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 11167 10407 145 145 0 11022 0
[pid=23051] vsize: 44668
Current children cumulated CPU time (s) 819.3
Current children cumulated vsize (Kb) 46792

[startup+830.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 11021 0 0 0 82857 74 0 0 25 0 1 0 1851937192 45740032 10413 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 11167 10413 145 145 0 11022 0
[pid=23051] vsize: 44668
Current children cumulated CPU time (s) 829.31
Current children cumulated vsize (Kb) 46792

[startup+840.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 11040 0 0 0 83857 74 0 0 25 0 1 0 1851937192 45805568 10432 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 11183 10432 145 145 0 11038 0
[pid=23051] vsize: 44732
Current children cumulated CPU time (s) 839.31
Current children cumulated vsize (Kb) 46856

[startup+850.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 11104 0 0 0 84857 74 0 0 25 0 1 0 1851937192 46084096 10496 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 11251 10496 145 145 0 11106 0
[pid=23051] vsize: 45004
Current children cumulated CPU time (s) 849.31
Current children cumulated vsize (Kb) 47128

[startup+860.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 11365 0 0 0 85853 76 0 0 25 0 1 0 1851937192 47140864 10757 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 11509 10757 145 145 0 11364 0
[pid=23051] vsize: 46036
Current children cumulated CPU time (s) 859.29
Current children cumulated vsize (Kb) 48160

[startup+870.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 11588 0 0 0 86849 78 0 0 25 0 1 0 1851937192 48111616 10980 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 11746 10980 145 145 0 11601 0
[pid=23051] vsize: 46984
Current children cumulated CPU time (s) 869.27
Current children cumulated vsize (Kb) 49108

[startup+880.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 11810 0 0 0 87846 79 0 0 25 0 1 0 1851937192 48967680 11202 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 11955 11202 145 145 0 11810 0
[pid=23051] vsize: 47820
Current children cumulated CPU time (s) 879.25
Current children cumulated vsize (Kb) 49944

[startup+890.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 12009 0 0 0 88843 81 0 0 25 0 1 0 1851937192 49774592 11401 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 12152 11401 145 145 0 12007 0
[pid=23051] vsize: 48608
Current children cumulated CPU time (s) 889.24
Current children cumulated vsize (Kb) 50732

[startup+900.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 12254 0 0 0 89839 82 0 0 25 0 1 0 1851937192 50982912 11646 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 12447 11646 145 145 0 12302 0
[pid=23051] vsize: 49788
Current children cumulated CPU time (s) 899.21
Current children cumulated vsize (Kb) 51912

[startup+910.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 12475 0 0 0 90836 84 0 0 25 0 1 0 1851937192 51879936 11867 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 12666 11867 145 145 0 12521 0
[pid=23051] vsize: 50664
Current children cumulated CPU time (s) 909.2
Current children cumulated vsize (Kb) 52788

[startup+920.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 12657 0 0 0 91834 85 0 0 25 0 1 0 1851937192 52744192 12049 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 12877 12049 145 145 0 12732 0
[pid=23051] vsize: 51508
Current children cumulated CPU time (s) 919.19
Current children cumulated vsize (Kb) 53632

[startup+930.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 12835 0 0 0 92831 86 0 0 25 0 1 0 1851937192 53465088 12227 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 13053 12227 145 145 0 12908 0
[pid=23051] vsize: 52212
Current children cumulated CPU time (s) 929.17
Current children cumulated vsize (Kb) 54336

[startup+940.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13015 0 0 0 93828 88 0 0 25 0 1 0 1851937192 54198272 12407 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 13232 12407 145 145 0 13087 0
[pid=23051] vsize: 52928
Current children cumulated CPU time (s) 939.16
Current children cumulated vsize (Kb) 55052

[startup+950.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13197 0 0 0 94825 89 0 0 25 0 1 0 1851937192 54951936 12589 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 13416 12589 145 145 0 13271 0
[pid=23051] vsize: 53664
Current children cumulated CPU time (s) 949.14
Current children cumulated vsize (Kb) 55788

[startup+960.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13283 0 0 0 95825 89 0 0 25 0 1 0 1851937192 55300096 12675 4294967295 134512640 135094434 3221224432 3221223024 134551469 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 13501 12675 145 145 0 13356 0
[pid=23051] vsize: 54004
Current children cumulated CPU time (s) 959.14
Current children cumulated vsize (Kb) 56128

[startup+970.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13283 0 0 0 96825 89 0 0 25 0 1 0 1851937192 55300096 12675 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 13501 12675 145 145 0 13356 0
[pid=23051] vsize: 54004
Current children cumulated CPU time (s) 969.14
Current children cumulated vsize (Kb) 56128

[startup+980.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13283 0 0 0 97825 89 0 0 25 0 1 0 1851937192 55300096 12675 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 13501 12675 145 145 0 13356 0
[pid=23051] vsize: 54004
Current children cumulated CPU time (s) 979.14
Current children cumulated vsize (Kb) 56128

[startup+990.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13283 0 0 0 98826 89 0 0 25 0 1 0 1851937192 55300096 12675 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 13501 12675 145 145 0 13356 0
[pid=23051] vsize: 54004
Current children cumulated CPU time (s) 989.15
Current children cumulated vsize (Kb) 56128

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13283 0 0 0 99825 89 0 0 25 0 1 0 1851937192 55300096 12675 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 13501 12675 145 145 0 13356 0
[pid=23051] vsize: 54004
Current children cumulated CPU time (s) 999.14
Current children cumulated vsize (Kb) 56128

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13283 0 0 0 100826 89 0 0 25 0 1 0 1851937192 55300096 12675 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 13501 12675 145 145 0 13356 0
[pid=23051] vsize: 54004
Current children cumulated CPU time (s) 1009.15
Current children cumulated vsize (Kb) 56128

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13283 0 0 0 101826 89 0 0 25 0 1 0 1851937192 55300096 12675 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 13501 12675 145 145 0 13356 0
[pid=23051] vsize: 54004
Current children cumulated CPU time (s) 1019.15
Current children cumulated vsize (Kb) 56128

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13302 0 0 0 102826 90 0 0 25 0 1 0 1851937192 55398400 12694 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 13525 12694 145 145 0 13380 0
[pid=23051] vsize: 54100
Current children cumulated CPU time (s) 1029.16
Current children cumulated vsize (Kb) 56224

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13302 0 0 0 103826 90 0 0 25 0 1 0 1851937192 55398400 12694 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 13525 12694 145 145 0 13380 0
[pid=23051] vsize: 54100
Current children cumulated CPU time (s) 1039.16
Current children cumulated vsize (Kb) 56224

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13302 0 0 0 104827 90 0 0 25 0 1 0 1851937192 55398400 12694 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 13525 12694 145 145 0 13380 0
[pid=23051] vsize: 54100
Current children cumulated CPU time (s) 1049.17
Current children cumulated vsize (Kb) 56224

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13302 0 0 0 105826 90 0 0 25 0 1 0 1851937192 55398400 12694 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 13525 12694 145 145 0 13380 0
[pid=23051] vsize: 54100
Current children cumulated CPU time (s) 1059.16
Current children cumulated vsize (Kb) 56224

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13302 0 0 0 106827 90 0 0 25 0 1 0 1851937192 55398400 12694 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 13525 12694 145 145 0 13380 0
[pid=23051] vsize: 54100
Current children cumulated CPU time (s) 1069.17
Current children cumulated vsize (Kb) 56224

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 14593 0 0 0 107823 93 0 0 25 0 1 0 1851937192 59613184 13695 4294967295 134512640 135094434 3221224432 3221128704 134522857 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 14554 13695 145 145 0 14409 0
[pid=23051] vsize: 58216
Current children cumulated CPU time (s) 1079.16
Current children cumulated vsize (Kb) 60340

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18084 0 0 0 108796 107 0 0 25 0 1 0 1851937192 76156928 17174 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 18593 17174 145 145 0 18448 0
[pid=23051] vsize: 74372
Current children cumulated CPU time (s) 1089.03
Current children cumulated vsize (Kb) 76496

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18084 0 0 0 109797 107 0 0 25 0 1 0 1851937192 76156928 17174 4294967295 134512640 135094434 3221224432 3221223104 134556288 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 18593 17174 145 145 0 18448 0
[pid=23051] vsize: 74372
Current children cumulated CPU time (s) 1099.04
Current children cumulated vsize (Kb) 76496

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18088 0 0 0 110797 107 0 0 25 0 1 0 1851937192 76173312 17178 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 18597 17178 145 145 0 18452 0
[pid=23051] vsize: 74388
Current children cumulated CPU time (s) 1109.04
Current children cumulated vsize (Kb) 76512

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18102 0 0 0 111797 107 0 0 25 0 1 0 1851937192 76238848 17192 4294967295 134512640 135094434 3221224432 3221223120 134554793 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 18613 17192 145 145 0 18468 0
[pid=23051] vsize: 74452
Current children cumulated CPU time (s) 1119.04
Current children cumulated vsize (Kb) 76576

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18107 0 0 0 112797 107 0 0 25 0 1 0 1851937192 76255232 17197 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 18617 17197 145 145 0 18472 0
[pid=23051] vsize: 74468
Current children cumulated CPU time (s) 1129.04
Current children cumulated vsize (Kb) 76592

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18114 0 0 0 113797 107 0 0 25 0 1 0 1851937192 76255232 17204 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 18617 17204 145 145 0 18472 0
[pid=23051] vsize: 74468
Current children cumulated CPU time (s) 1139.04
Current children cumulated vsize (Kb) 76592

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18117 0 0 0 114798 107 0 0 25 0 1 0 1851937192 76255232 17207 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 18617 17207 145 145 0 18472 0
[pid=23051] vsize: 74468
Current children cumulated CPU time (s) 1149.05
Current children cumulated vsize (Kb) 76592

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18117 0 0 0 115798 107 0 0 25 0 1 0 1851937192 76255232 17207 4294967295 134512640 135094434 3221224432 3221223088 134558289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 18617 17207 145 145 0 18472 0
[pid=23051] vsize: 74468
Current children cumulated CPU time (s) 1159.05
Current children cumulated vsize (Kb) 76592

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18117 0 0 0 116798 107 0 0 25 0 1 0 1851937192 76255232 17207 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 18617 17207 145 145 0 18472 0
[pid=23051] vsize: 74468
Current children cumulated CPU time (s) 1169.05
Current children cumulated vsize (Kb) 76592

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18117 0 0 0 117798 107 0 0 25 0 1 0 1851937192 76255232 17207 4294967295 134512640 135094434 3221224432 3221223024 134557398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 18617 17207 145 145 0 18472 0
[pid=23051] vsize: 74468
Current children cumulated CPU time (s) 1179.05
Current children cumulated vsize (Kb) 76592

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18117 0 0 0 118799 107 0 0 25 0 1 0 1851937192 76255232 17207 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 18617 17207 145 145 0 18472 0
[pid=23051] vsize: 74468
Current children cumulated CPU time (s) 1189.06
Current children cumulated vsize (Kb) 76592

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18117 0 0 0 119799 107 0 0 25 0 1 0 1851937192 76255232 17207 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 18617 17207 145 145 0 18472 0
[pid=23051] vsize: 74468
Current children cumulated CPU time (s) 1199.06
Current children cumulated vsize (Kb) 76592

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18117 0 0 0 120799 107 0 0 25 0 1 0 1851937192 76255232 17207 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 18617 17207 145 145 0 18472 0
[pid=23051] vsize: 74468
Current children cumulated CPU time (s) 1209.06
Current children cumulated vsize (Kb) 76592



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 23051
Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/23047/statm): 531 226 485 147 0 384 0
[pid=23047] vsize: 2124
Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18117 0 0 0 120799 107 0 0 25 0 1 0 1851937192 76255232 17207 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/23051/statm): 18617 17207 145 145 0 18472 0
[pid=23051] vsize: 74468
Current children cumulated CPU time (s) 1209.06
Current children cumulated vsize (Kb) 76592

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

Child status: 10
Real time (s): 1210.15
CPU time (s): 1209.11
CPU user time (s): 1208
CPU system time (s): 1.11383
CPU usage (%): 99.9142
Max. virtual memory (cumulated for all children) (Kb): 76592

Verifier Data

ERROR: no interpretation found !