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/miplib/normalized-mps-v2-20-10-rgn.opb
MD5SUM56e0ae8659c33a6c7b55390a12db116b
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.24
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 3884

Launcher Data

LAUNCH ON wulflinc30 THE 2005-09-19 03:25:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2883 boxname=wulflinc30 idbench=539 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  56e0ae8659c33a6c7b55390a12db116b  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-rgn.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-rgn.opb
IDLAUNCH: 2883
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        904272 kB
Buffers:         32892 kB
Cached:          67716 kB
SwapCached:        780 kB
Active:          45936 kB
Inactive:        57276 kB
HighTotal:      131008 kB
HighFree:        60340 kB
LowTotal:       903652 kB
LowFree:        843932 kB
SwapTotal:     2097892 kB
SwapFree:      2096636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5732 kB
Slab:            21492 kB
Committed_AS:    64172 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 03:45:46 (client local time) WITH STATUS 10 IN 1208.95 SECONDS
stats: 2883 7 1208.95 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/18922/stat): 18922 (minisat+_script) R 18921 18922 5245 0 -1 0 19 0 0 0 0 0 0 0 20 0 1 0 1846627276 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/18922/statm): 174 3 169 147 0 27 0
[pid=18922] 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=18923
New process pid=18924
New process pid=18925
One traced child (pid=18924) 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=18925) exited with status: 0
One traced child (pid=18923) exited with status: 0
New process pid=18926
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-rgn.opb

[startup+10.004 s]
Raw data (loadavg): 0.93 0.96 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) T 18922 18922 5245 0 -1 0 3275 0 0 0 969 13 0 0 25 0 1 0 1846627281 12247040 2667 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/18926/statm): 2990 2667 145 145 0 2845 0
[pid=18926] vsize: 11960
Current children cumulated CPU time (s) 9.82
Current children cumulated vsize (Kb) 14084

[startup+20.0048 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 4174 0 0 0 1955 18 0 0 25 0 1 0 1846627281 15998976 3566 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 3906 3566 145 145 0 3761 0
[pid=18926] vsize: 15624
Current children cumulated CPU time (s) 19.73
Current children cumulated vsize (Kb) 17748

[startup+30.0066 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 4822 0 0 0 2944 24 0 0 25 0 1 0 1846627281 18608128 4214 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 4543 4214 145 145 0 4398 0
[pid=18926] vsize: 18172
Current children cumulated CPU time (s) 29.68
Current children cumulated vsize (Kb) 20296

[startup+40.0074 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 5425 0 0 0 3935 27 0 0 25 0 1 0 1846627281 21331968 4817 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 5208 4817 145 145 0 5063 0
[pid=18926] vsize: 20832
Current children cumulated CPU time (s) 39.62
Current children cumulated vsize (Kb) 22956

[startup+50.0092 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 5426 0 0 0 4934 27 0 0 25 0 1 0 1846627281 21331968 4818 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 5208 4818 145 145 0 5063 0
[pid=18926] vsize: 20832
Current children cumulated CPU time (s) 49.61
Current children cumulated vsize (Kb) 22956

[startup+60.01 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 5462 0 0 0 5935 27 0 0 25 0 1 0 1846627281 21528576 4854 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 5256 4854 145 145 0 5111 0
[pid=18926] vsize: 21024
Current children cumulated CPU time (s) 59.62
Current children cumulated vsize (Kb) 23148

[startup+70.0108 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 5659 0 0 0 6931 29 0 0 25 0 1 0 1846627281 22343680 5051 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 5455 5051 145 145 0 5310 0
[pid=18926] vsize: 21820
Current children cumulated CPU time (s) 69.6
Current children cumulated vsize (Kb) 23944

[startup+80.0116 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 6299 0 0 0 7922 33 0 0 25 0 1 0 1846627281 24973312 5691 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 6097 5691 145 145 0 5952 0
[pid=18926] vsize: 24388
Current children cumulated CPU time (s) 79.55
Current children cumulated vsize (Kb) 26512

[startup+90.0124 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 6376 0 0 0 8921 33 0 0 25 0 1 0 1846627281 25264128 5768 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 6168 5768 145 145 0 6023 0
[pid=18926] vsize: 24672
Current children cumulated CPU time (s) 89.54
Current children cumulated vsize (Kb) 26796

[startup+100.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 6376 0 0 0 9921 33 0 0 25 0 1 0 1846627281 25264128 5768 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 6168 5768 145 145 0 6023 0
[pid=18926] vsize: 24672
Current children cumulated CPU time (s) 99.54
Current children cumulated vsize (Kb) 26796

[startup+110.013 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 6376 0 0 0 10921 33 0 0 25 0 1 0 1846627281 25264128 5768 4294967295 134512640 135094434 3221224432 3221223088 134557934 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 6168 5768 145 145 0 6023 0
[pid=18926] vsize: 24672
Current children cumulated CPU time (s) 109.54
Current children cumulated vsize (Kb) 26796

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 6389 0 0 0 11921 33 0 0 25 0 1 0 1846627281 25329664 5781 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 6184 5781 145 145 0 6039 0
[pid=18926] vsize: 24736
Current children cumulated CPU time (s) 119.54
Current children cumulated vsize (Kb) 26860

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 6423 0 0 0 12921 33 0 0 25 0 1 0 1846627281 25493504 5815 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 6224 5815 145 145 0 6079 0
[pid=18926] vsize: 24896
Current children cumulated CPU time (s) 129.54
Current children cumulated vsize (Kb) 27020

[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 6432 0 0 0 13920 34 0 0 25 0 1 0 1846627281 25493504 5824 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 6224 5824 145 145 0 6079 0
[pid=18926] vsize: 24896
Current children cumulated CPU time (s) 139.54
Current children cumulated vsize (Kb) 27020

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 6432 0 0 0 14920 34 0 0 25 0 1 0 1846627281 25493504 5824 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 6224 5824 145 145 0 6079 0
[pid=18926] vsize: 24896
Current children cumulated CPU time (s) 149.54
Current children cumulated vsize (Kb) 27020

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 6432 0 0 0 15920 34 0 0 25 0 1 0 1846627281 25493504 5824 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 6224 5824 145 145 0 6079 0
[pid=18926] vsize: 24896
Current children cumulated CPU time (s) 159.54
Current children cumulated vsize (Kb) 27020

[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 6460 0 0 0 16920 34 0 0 25 0 1 0 1846627281 25657344 5852 4294967295 134512640 135094434 3221224432 3221223104 134555566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 6264 5852 145 145 0 6119 0
[pid=18926] vsize: 25056
Current children cumulated CPU time (s) 169.54
Current children cumulated vsize (Kb) 27180

[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 6649 0 0 0 17917 36 0 0 25 0 1 0 1846627281 26456064 6041 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 6459 6041 145 145 0 6314 0
[pid=18926] vsize: 25836
Current children cumulated CPU time (s) 179.53
Current children cumulated vsize (Kb) 27960

[startup+190.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 6957 0 0 0 18912 38 0 0 25 0 1 0 1846627281 27783168 6349 4294967295 134512640 135094434 3221224432 3221223024 134551448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 6783 6349 145 145 0 6638 0
[pid=18926] vsize: 27132
Current children cumulated CPU time (s) 189.5
Current children cumulated vsize (Kb) 29256

[startup+200.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 6958 0 0 0 19912 38 0 0 25 0 1 0 1846627281 27783168 6350 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 6783 6350 145 145 0 6638 0
[pid=18926] vsize: 27132
Current children cumulated CPU time (s) 199.5
Current children cumulated vsize (Kb) 29256

[startup+210.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 6959 0 0 0 20911 39 0 0 25 0 1 0 1846627281 27783168 6351 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 6783 6351 145 145 0 6638 0
[pid=18926] vsize: 27132
Current children cumulated CPU time (s) 209.5
Current children cumulated vsize (Kb) 29256

[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 7016 0 0 0 21911 39 0 0 25 0 1 0 1846627281 28061696 6408 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 6851 6408 145 145 0 6706 0
[pid=18926] vsize: 27404
Current children cumulated CPU time (s) 219.5
Current children cumulated vsize (Kb) 29528

[startup+230.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 7065 0 0 0 22910 40 0 0 25 0 1 0 1846627281 28258304 6457 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 6899 6457 145 145 0 6754 0
[pid=18926] vsize: 27596
Current children cumulated CPU time (s) 229.5
Current children cumulated vsize (Kb) 29720

[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 7112 0 0 0 23910 40 0 0 25 0 1 0 1846627281 28520448 6504 4294967295 134512640 135094434 3221224432 3221223104 134556071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 6963 6504 145 145 0 6818 0
[pid=18926] vsize: 27852
Current children cumulated CPU time (s) 239.5
Current children cumulated vsize (Kb) 29976

[startup+250.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 7361 0 0 0 24906 42 0 0 25 0 1 0 1846627281 29564928 6753 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 7218 6753 145 145 0 7073 0
[pid=18926] vsize: 28872
Current children cumulated CPU time (s) 249.48
Current children cumulated vsize (Kb) 30996

[startup+260.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 7621 0 0 0 25902 44 0 0 25 0 1 0 1846627281 30633984 7013 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 7479 7013 145 145 0 7334 0
[pid=18926] vsize: 29916
Current children cumulated CPU time (s) 259.46
Current children cumulated vsize (Kb) 32040

[startup+270.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 7824 0 0 0 26898 46 0 0 25 0 1 0 1846627281 31477760 7216 4294967295 134512640 135094434 3221224432 3221223024 134551465 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 7685 7216 145 145 0 7540 0
[pid=18926] vsize: 30740
Current children cumulated CPU time (s) 269.44
Current children cumulated vsize (Kb) 32864

[startup+280.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 7824 0 0 0 27897 46 0 0 25 0 1 0 1846627281 31477760 7216 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 7685 7216 145 145 0 7540 0
[pid=18926] vsize: 30740
Current children cumulated CPU time (s) 279.43
Current children cumulated vsize (Kb) 32864

[startup+290.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 7824 0 0 0 28897 46 0 0 25 0 1 0 1846627281 31477760 7216 4294967295 134512640 135094434 3221224432 3221223104 134555967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 7685 7216 145 145 0 7540 0
[pid=18926] vsize: 30740
Current children cumulated CPU time (s) 289.43
Current children cumulated vsize (Kb) 32864

[startup+300.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 7824 0 0 0 29897 46 0 0 25 0 1 0 1846627281 31477760 7216 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 7685 7216 145 145 0 7540 0
[pid=18926] vsize: 30740
Current children cumulated CPU time (s) 299.43
Current children cumulated vsize (Kb) 32864

[startup+310.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 7824 0 0 0 30897 47 0 0 25 0 1 0 1846627281 31477760 7216 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 7685 7216 145 145 0 7540 0
[pid=18926] vsize: 30740
Current children cumulated CPU time (s) 309.44
Current children cumulated vsize (Kb) 32864

[startup+320.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 8210 0 0 0 31888 50 0 0 25 0 1 0 1846627281 33116160 7602 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 8085 7602 145 145 0 7940 0
[pid=18926] vsize: 32340
Current children cumulated CPU time (s) 319.38
Current children cumulated vsize (Kb) 34464

[startup+330.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 8604 0 0 0 32882 53 0 0 25 0 1 0 1846627281 34844672 7996 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 8507 7996 145 145 0 8362 0
[pid=18926] vsize: 34028
Current children cumulated CPU time (s) 329.35
Current children cumulated vsize (Kb) 36152

[startup+340.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 8878 0 0 0 33878 54 0 0 25 0 1 0 1846627281 36044800 8270 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 8800 8270 145 145 0 8655 0
[pid=18926] vsize: 35200
Current children cumulated CPU time (s) 339.32
Current children cumulated vsize (Kb) 37324

[startup+350.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 9191 0 0 0 34872 57 0 0 25 0 1 0 1846627281 37412864 8583 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 9134 8583 145 145 0 8989 0
[pid=18926] vsize: 36536
Current children cumulated CPU time (s) 349.29
Current children cumulated vsize (Kb) 38660

[startup+360.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 9466 0 0 0 35867 59 0 0 25 0 1 0 1846627281 38608896 8858 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 9426 8858 145 145 0 9281 0
[pid=18926] vsize: 37704
Current children cumulated CPU time (s) 359.26
Current children cumulated vsize (Kb) 39828

[startup+370.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 9753 0 0 0 36862 61 0 0 25 0 1 0 1846627281 39800832 9145 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 9717 9145 145 145 0 9572 0
[pid=18926] vsize: 38868
Current children cumulated CPU time (s) 369.23
Current children cumulated vsize (Kb) 40992

[startup+380.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10195 0 0 0 37856 63 0 0 25 0 1 0 1846627281 41603072 9587 4294967295 134512640 135094434 3221224432 3221223024 134551448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 10157 9587 145 145 0 10012 0
[pid=18926] vsize: 40628
Current children cumulated CPU time (s) 379.19
Current children cumulated vsize (Kb) 42752

[startup+390.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10195 0 0 0 38856 64 0 0 25 0 1 0 1846627281 41603072 9587 4294967295 134512640 135094434 3221224432 3221223104 134556454 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 10157 9587 145 145 0 10012 0
[pid=18926] vsize: 40628
Current children cumulated CPU time (s) 389.2
Current children cumulated vsize (Kb) 42752

[startup+400.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10196 0 0 0 39856 64 0 0 25 0 1 0 1846627281 41603072 9588 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 10157 9588 145 145 0 10012 0
[pid=18926] vsize: 40628
Current children cumulated CPU time (s) 399.2
Current children cumulated vsize (Kb) 42752

[startup+410.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10196 0 0 0 40855 64 0 0 25 0 1 0 1846627281 41603072 9588 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 10157 9588 145 145 0 10012 0
[pid=18926] vsize: 40628
Current children cumulated CPU time (s) 409.19
Current children cumulated vsize (Kb) 42752

[startup+420.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10219 0 0 0 41855 64 0 0 25 0 1 0 1846627281 41734144 9611 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 10189 9611 145 145 0 10044 0
[pid=18926] vsize: 40756
Current children cumulated CPU time (s) 419.19
Current children cumulated vsize (Kb) 42880

[startup+430.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10220 0 0 0 42854 65 0 0 25 0 1 0 1846627281 41734144 9612 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 10189 9612 145 145 0 10044 0
[pid=18926] vsize: 40756
Current children cumulated CPU time (s) 429.19
Current children cumulated vsize (Kb) 42880

[startup+440.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10240 0 0 0 43854 65 0 0 25 0 1 0 1846627281 41865216 9632 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 10221 9632 145 145 0 10076 0
[pid=18926] vsize: 40884
Current children cumulated CPU time (s) 439.19
Current children cumulated vsize (Kb) 43008

[startup+450.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10242 0 0 0 44853 65 0 0 25 0 1 0 1846627281 41865216 9634 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 10221 9634 145 145 0 10076 0
[pid=18926] vsize: 40884
Current children cumulated CPU time (s) 449.18
Current children cumulated vsize (Kb) 43008

[startup+460.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10265 0 0 0 45853 66 0 0 25 0 1 0 1846627281 41996288 9657 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 10253 9657 145 145 0 10108 0
[pid=18926] vsize: 41012
Current children cumulated CPU time (s) 459.19
Current children cumulated vsize (Kb) 43136

[startup+470.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10309 0 0 0 46852 66 0 0 25 0 1 0 1846627281 42258432 9701 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 10317 9701 145 145 0 10172 0
[pid=18926] vsize: 41268
Current children cumulated CPU time (s) 469.18
Current children cumulated vsize (Kb) 43392

[startup+480.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10329 0 0 0 47851 67 0 0 25 0 1 0 1846627281 42389504 9721 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 10349 9721 145 145 0 10204 0
[pid=18926] vsize: 41396
Current children cumulated CPU time (s) 479.18
Current children cumulated vsize (Kb) 43520

[startup+490.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10334 0 0 0 48851 67 0 0 25 0 1 0 1846627281 42389504 9726 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 10349 9726 145 145 0 10204 0
[pid=18926] vsize: 41396
Current children cumulated CPU time (s) 489.18
Current children cumulated vsize (Kb) 43520

[startup+500.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10364 0 0 0 49850 68 0 0 25 0 1 0 1846627281 42520576 9756 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 10381 9756 145 145 0 10236 0
[pid=18926] vsize: 41524
Current children cumulated CPU time (s) 499.18
Current children cumulated vsize (Kb) 43648

[startup+510.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10386 0 0 0 50850 68 0 0 25 0 1 0 1846627281 42651648 9778 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 10413 9778 145 145 0 10268 0
[pid=18926] vsize: 41652
Current children cumulated CPU time (s) 509.18
Current children cumulated vsize (Kb) 43776

[startup+520.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10410 0 0 0 51850 68 0 0 25 0 1 0 1846627281 42782720 9802 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 10445 9802 145 145 0 10300 0
[pid=18926] vsize: 41780
Current children cumulated CPU time (s) 519.18
Current children cumulated vsize (Kb) 43904

[startup+530.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10430 0 0 0 52849 69 0 0 25 0 1 0 1846627281 42913792 9822 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 10477 9822 145 145 0 10332 0
[pid=18926] vsize: 41908
Current children cumulated CPU time (s) 529.18
Current children cumulated vsize (Kb) 44032

[startup+540.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10433 0 0 0 53849 69 0 0 25 0 1 0 1846627281 42913792 9825 4294967295 134512640 135094434 3221224432 3221223024 134551448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 10477 9825 145 145 0 10332 0
[pid=18926] vsize: 41908
Current children cumulated CPU time (s) 539.18
Current children cumulated vsize (Kb) 44032

[startup+550.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10433 0 0 0 54849 69 0 0 25 0 1 0 1846627281 42913792 9825 4294967295 134512640 135094434 3221224432 3221223088 134558238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 10477 9825 145 145 0 10332 0
[pid=18926] vsize: 41908
Current children cumulated CPU time (s) 549.18
Current children cumulated vsize (Kb) 44032

[startup+560.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10433 0 0 0 55848 70 0 0 25 0 1 0 1846627281 42913792 9825 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 10477 9825 145 145 0 10332 0
[pid=18926] vsize: 41908
Current children cumulated CPU time (s) 559.18
Current children cumulated vsize (Kb) 44032

[startup+570.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10434 0 0 0 56848 70 0 0 25 0 1 0 1846627281 42913792 9826 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 10477 9826 145 145 0 10332 0
[pid=18926] vsize: 41908
Current children cumulated CPU time (s) 569.18
Current children cumulated vsize (Kb) 44032

[startup+580.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10437 0 0 0 57849 70 0 0 25 0 1 0 1846627281 42913792 9829 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 10477 9829 145 145 0 10332 0
[pid=18926] vsize: 41908
Current children cumulated CPU time (s) 579.19
Current children cumulated vsize (Kb) 44032

[startup+590.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10437 0 0 0 58849 70 0 0 25 0 1 0 1846627281 42913792 9829 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 10477 9829 145 145 0 10332 0
[pid=18926] vsize: 41908
Current children cumulated CPU time (s) 589.19
Current children cumulated vsize (Kb) 44032

[startup+600.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10437 0 0 0 59849 70 0 0 25 0 1 0 1846627281 42913792 9829 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 10477 9829 145 145 0 10332 0
[pid=18926] vsize: 41908
Current children cumulated CPU time (s) 599.19
Current children cumulated vsize (Kb) 44032

[startup+610.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10437 0 0 0 60849 70 0 0 25 0 1 0 1846627281 42913792 9829 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 10477 9829 145 145 0 10332 0
[pid=18926] vsize: 41908
Current children cumulated CPU time (s) 609.19
Current children cumulated vsize (Kb) 44032

[startup+620.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10437 0 0 0 61849 70 0 0 25 0 1 0 1846627281 42913792 9829 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 10477 9829 145 145 0 10332 0
[pid=18926] vsize: 41908
Current children cumulated CPU time (s) 619.19
Current children cumulated vsize (Kb) 44032

[startup+630.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10437 0 0 0 62849 70 0 0 25 0 1 0 1846627281 42913792 9829 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 10477 9829 145 145 0 10332 0
[pid=18926] vsize: 41908
Current children cumulated CPU time (s) 629.19
Current children cumulated vsize (Kb) 44032

[startup+640.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10437 0 0 0 63849 70 0 0 25 0 1 0 1846627281 42913792 9829 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 10477 9829 145 145 0 10332 0
[pid=18926] vsize: 41908
Current children cumulated CPU time (s) 639.19
Current children cumulated vsize (Kb) 44032

[startup+650.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10437 0 0 0 64849 70 0 0 25 0 1 0 1846627281 42913792 9829 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 10477 9829 145 145 0 10332 0
[pid=18926] vsize: 41908
Current children cumulated CPU time (s) 649.19
Current children cumulated vsize (Kb) 44032

[startup+660.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10437 0 0 0 65850 70 0 0 25 0 1 0 1846627281 42913792 9829 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 10477 9829 145 145 0 10332 0
[pid=18926] vsize: 41908
Current children cumulated CPU time (s) 659.2
Current children cumulated vsize (Kb) 44032

[startup+670.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10471 0 0 0 66850 70 0 0 25 0 1 0 1846627281 43175936 9863 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 10541 9863 145 145 0 10396 0
[pid=18926] vsize: 42164
Current children cumulated CPU time (s) 669.2
Current children cumulated vsize (Kb) 44288

[startup+680.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10473 0 0 0 67850 70 0 0 25 0 1 0 1846627281 43175936 9865 4294967295 134512640 135094434 3221224432 3221223024 134551469 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 10541 9865 145 145 0 10396 0
[pid=18926] vsize: 42164
Current children cumulated CPU time (s) 679.2
Current children cumulated vsize (Kb) 44288

[startup+690.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10473 0 0 0 68850 71 0 0 25 0 1 0 1846627281 43175936 9865 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 10541 9865 145 145 0 10396 0
[pid=18926] vsize: 42164
Current children cumulated CPU time (s) 689.21
Current children cumulated vsize (Kb) 44288

[startup+700.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10473 0 0 0 69849 71 0 0 25 0 1 0 1846627281 43175936 9865 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 10541 9865 145 145 0 10396 0
[pid=18926] vsize: 42164
Current children cumulated CPU time (s) 699.2
Current children cumulated vsize (Kb) 44288

[startup+710.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10473 0 0 0 70849 71 0 0 25 0 1 0 1846627281 43175936 9865 4294967295 134512640 135094434 3221224432 3221223088 134558184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 10541 9865 145 145 0 10396 0
[pid=18926] vsize: 42164
Current children cumulated CPU time (s) 709.2
Current children cumulated vsize (Kb) 44288

[startup+720.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10473 0 0 0 71849 71 0 0 25 0 1 0 1846627281 43175936 9865 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 10541 9865 145 145 0 10396 0
[pid=18926] vsize: 42164
Current children cumulated CPU time (s) 719.2
Current children cumulated vsize (Kb) 44288

[startup+730.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10473 0 0 0 72849 71 0 0 25 0 1 0 1846627281 43175936 9865 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 10541 9865 145 145 0 10396 0
[pid=18926] vsize: 42164
Current children cumulated CPU time (s) 729.2
Current children cumulated vsize (Kb) 44288

[startup+740.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10478 0 0 0 73849 72 0 0 25 0 1 0 1846627281 43175936 9870 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 10541 9870 145 145 0 10396 0
[pid=18926] vsize: 42164
Current children cumulated CPU time (s) 739.21
Current children cumulated vsize (Kb) 44288

[startup+750.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10777 0 0 0 74845 74 0 0 25 0 1 0 1846627281 44404736 10169 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 10841 10169 145 145 0 10696 0
[pid=18926] vsize: 43364
Current children cumulated CPU time (s) 749.19
Current children cumulated vsize (Kb) 45488

[startup+760.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10800 0 0 0 75845 75 0 0 25 0 1 0 1846627281 44498944 10192 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 10864 10192 145 145 0 10719 0
[pid=18926] vsize: 43456
Current children cumulated CPU time (s) 759.2
Current children cumulated vsize (Kb) 45580

[startup+770.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10828 0 0 0 76845 75 0 0 25 0 1 0 1846627281 44630016 10220 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 10896 10220 145 145 0 10751 0
[pid=18926] vsize: 43584
Current children cumulated CPU time (s) 769.2
Current children cumulated vsize (Kb) 45708

[startup+780.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10835 0 0 0 77845 75 0 0 25 0 1 0 1846627281 44756992 10227 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 10927 10227 145 145 0 10782 0
[pid=18926] vsize: 43708
Current children cumulated CPU time (s) 779.2
Current children cumulated vsize (Kb) 45832

[startup+790.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10855 0 0 0 78845 75 0 0 25 0 1 0 1846627281 44822528 10247 4294967295 134512640 135094434 3221224432 3221223088 134557934 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 10943 10247 145 145 0 10798 0
[pid=18926] vsize: 43772
Current children cumulated CPU time (s) 789.2
Current children cumulated vsize (Kb) 45896

[startup+800.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10927 0 0 0 79845 75 0 0 25 0 1 0 1846627281 45346816 10319 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 11071 10319 145 145 0 10926 0
[pid=18926] vsize: 44284
Current children cumulated CPU time (s) 799.2
Current children cumulated vsize (Kb) 46408

[startup+810.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 10988 0 0 0 80845 75 0 0 25 0 1 0 1846627281 45674496 10380 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 11151 10380 145 145 0 11006 0
[pid=18926] vsize: 44604
Current children cumulated CPU time (s) 809.2
Current children cumulated vsize (Kb) 46728

[startup+820.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 11015 0 0 0 81845 76 0 0 25 0 1 0 1846627281 45740032 10407 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 11167 10407 145 145 0 11022 0
[pid=18926] vsize: 44668
Current children cumulated CPU time (s) 819.21
Current children cumulated vsize (Kb) 46792

[startup+830.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 11038 0 0 0 82845 76 0 0 25 0 1 0 1846627281 45805568 10430 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 11183 10430 145 145 0 11038 0
[pid=18926] vsize: 44732
Current children cumulated CPU time (s) 829.21
Current children cumulated vsize (Kb) 46856

[startup+840.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 11065 0 0 0 83845 76 0 0 25 0 1 0 1846627281 45936640 10457 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 11215 10457 145 145 0 11070 0
[pid=18926] vsize: 44860
Current children cumulated CPU time (s) 839.21
Current children cumulated vsize (Kb) 46984

[startup+850.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 11149 0 0 0 84843 76 0 0 25 0 1 0 1846627281 46264320 10541 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 11295 10541 145 145 0 11150 0
[pid=18926] vsize: 45180
Current children cumulated CPU time (s) 849.19
Current children cumulated vsize (Kb) 47304

[startup+860.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 11410 0 0 0 85840 78 0 0 25 0 1 0 1846627281 47378432 10802 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 11567 10802 145 145 0 11422 0
[pid=18926] vsize: 46268
Current children cumulated CPU time (s) 859.18
Current children cumulated vsize (Kb) 48392

[startup+870.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 11624 0 0 0 86837 79 0 0 25 0 1 0 1846627281 48250880 11016 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 11780 11016 145 145 0 11635 0
[pid=18926] vsize: 47120
Current children cumulated CPU time (s) 869.16
Current children cumulated vsize (Kb) 49244

[startup+880.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 11853 0 0 0 87832 81 0 0 25 0 1 0 1846627281 49139712 11245 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 11997 11245 145 145 0 11852 0
[pid=18926] vsize: 47988
Current children cumulated CPU time (s) 879.13
Current children cumulated vsize (Kb) 50112

[startup+890.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 12090 0 0 0 88829 82 0 0 25 0 1 0 1846627281 50343936 11482 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 12291 11482 145 145 0 12146 0
[pid=18926] vsize: 49164
Current children cumulated CPU time (s) 889.11
Current children cumulated vsize (Kb) 51288

[startup+900.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 12282 0 0 0 89827 83 0 0 25 0 1 0 1846627281 51109888 11674 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 12478 11674 145 145 0 12333 0
[pid=18926] vsize: 49912
Current children cumulated CPU time (s) 899.1
Current children cumulated vsize (Kb) 52036

[startup+910.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 12504 0 0 0 90824 84 0 0 25 0 1 0 1846627281 51990528 11896 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 12693 11896 145 145 0 12548 0
[pid=18926] vsize: 50772
Current children cumulated CPU time (s) 909.08
Current children cumulated vsize (Kb) 52896

[startup+920.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 12685 0 0 0 91822 85 0 0 25 0 1 0 1846627281 52862976 12077 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 12906 12077 145 145 0 12761 0
[pid=18926] vsize: 51624
Current children cumulated CPU time (s) 919.07
Current children cumulated vsize (Kb) 53748

[startup+930.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 12857 0 0 0 92819 86 0 0 25 0 1 0 1846627281 53563392 12249 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 13077 12249 145 145 0 12932 0
[pid=18926] vsize: 52308
Current children cumulated CPU time (s) 929.05
Current children cumulated vsize (Kb) 54432

[startup+940.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 13045 0 0 0 93817 87 0 0 25 0 1 0 1846627281 54317056 12437 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 13261 12437 145 145 0 13116 0
[pid=18926] vsize: 53044
Current children cumulated CPU time (s) 939.04
Current children cumulated vsize (Kb) 55168

[startup+950.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 13219 0 0 0 94813 89 0 0 25 0 1 0 1846627281 55037952 12611 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 13437 12611 145 145 0 13292 0
[pid=18926] vsize: 53748
Current children cumulated CPU time (s) 949.02
Current children cumulated vsize (Kb) 55872

[startup+960.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 13283 0 0 0 95812 89 0 0 25 0 1 0 1846627281 55300096 12675 4294967295 134512640 135094434 3221224432 3221223024 134551465 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 13501 12675 145 145 0 13356 0
[pid=18926] vsize: 54004
Current children cumulated CPU time (s) 959.01
Current children cumulated vsize (Kb) 56128

[startup+970.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 13283 0 0 0 96812 89 0 0 25 0 1 0 1846627281 55300096 12675 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 13501 12675 145 145 0 13356 0
[pid=18926] vsize: 54004
Current children cumulated CPU time (s) 969.01
Current children cumulated vsize (Kb) 56128

[startup+980.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 13283 0 0 0 97812 90 0 0 25 0 1 0 1846627281 55300096 12675 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 13501 12675 145 145 0 13356 0
[pid=18926] vsize: 54004
Current children cumulated CPU time (s) 979.02
Current children cumulated vsize (Kb) 56128

[startup+990.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 13283 0 0 0 98813 90 0 0 25 0 1 0 1846627281 55300096 12675 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 13501 12675 145 145 0 13356 0
[pid=18926] vsize: 54004
Current children cumulated CPU time (s) 989.03
Current children cumulated vsize (Kb) 56128

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 13283 0 0 0 99813 90 0 0 25 0 1 0 1846627281 55300096 12675 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 13501 12675 145 145 0 13356 0
[pid=18926] vsize: 54004
Current children cumulated CPU time (s) 999.03
Current children cumulated vsize (Kb) 56128

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 13283 0 0 0 100812 91 0 0 25 0 1 0 1846627281 55300096 12675 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 13501 12675 145 145 0 13356 0
[pid=18926] vsize: 54004
Current children cumulated CPU time (s) 1009.03
Current children cumulated vsize (Kb) 56128

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 13283 0 0 0 101811 91 0 0 25 0 1 0 1846627281 55300096 12675 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 13501 12675 145 145 0 13356 0
[pid=18926] vsize: 54004
Current children cumulated CPU time (s) 1019.02
Current children cumulated vsize (Kb) 56128

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 13302 0 0 0 102811 92 0 0 25 0 1 0 1846627281 55398400 12694 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 13525 12694 145 145 0 13380 0
[pid=18926] vsize: 54100
Current children cumulated CPU time (s) 1029.03
Current children cumulated vsize (Kb) 56224

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 13302 0 0 0 103811 92 0 0 25 0 1 0 1846627281 55398400 12694 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 13525 12694 145 145 0 13380 0
[pid=18926] vsize: 54100
Current children cumulated CPU time (s) 1039.03
Current children cumulated vsize (Kb) 56224

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 13302 0 0 0 104811 92 0 0 25 0 1 0 1846627281 55398400 12694 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 13525 12694 145 145 0 13380 0
[pid=18926] vsize: 54100
Current children cumulated CPU time (s) 1049.03
Current children cumulated vsize (Kb) 56224

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 13302 0 0 0 105810 93 0 0 25 0 1 0 1846627281 55398400 12694 4294967295 134512640 135094434 3221224432 3221223024 134557393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 13525 12694 145 145 0 13380 0
[pid=18926] vsize: 54100
Current children cumulated CPU time (s) 1059.03
Current children cumulated vsize (Kb) 56224

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 13302 0 0 0 106809 93 0 0 25 0 1 0 1846627281 55398400 12694 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 13525 12694 145 145 0 13380 0
[pid=18926] vsize: 54100
Current children cumulated CPU time (s) 1069.02
Current children cumulated vsize (Kb) 56224

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 18081 0 0 0 107776 112 0 0 19 0 1 0 1846627281 76156928 17171 4294967295 134512640 135094434 3221224432 3221223220 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/18926/statm): 18593 17171 145 145 0 18448 0
[pid=18926] vsize: 74372
Current children cumulated CPU time (s) 1078.88
Current children cumulated vsize (Kb) 76496

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 18084 0 0 0 108776 112 0 0 25 0 1 0 1846627281 76156928 17174 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 18593 17174 145 145 0 18448 0
[pid=18926] vsize: 74372
Current children cumulated CPU time (s) 1088.88
Current children cumulated vsize (Kb) 76496

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 18084 0 0 0 109775 113 0 0 25 0 1 0 1846627281 76156928 17174 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 18593 17174 145 145 0 18448 0
[pid=18926] vsize: 74372
Current children cumulated CPU time (s) 1098.88
Current children cumulated vsize (Kb) 76496

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 18088 0 0 0 110775 113 0 0 25 0 1 0 1846627281 76173312 17178 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 18597 17178 145 145 0 18452 0
[pid=18926] vsize: 74388
Current children cumulated CPU time (s) 1108.88
Current children cumulated vsize (Kb) 76512

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 18102 0 0 0 111775 113 0 0 25 0 1 0 1846627281 76238848 17192 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 18613 17192 145 145 0 18468 0
[pid=18926] vsize: 74452
Current children cumulated CPU time (s) 1118.88
Current children cumulated vsize (Kb) 76576

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 18107 0 0 0 112775 113 0 0 25 0 1 0 1846627281 76255232 17197 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 18617 17197 145 145 0 18472 0
[pid=18926] vsize: 74468
Current children cumulated CPU time (s) 1128.88
Current children cumulated vsize (Kb) 76592

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 18114 0 0 0 113776 113 0 0 25 0 1 0 1846627281 76255232 17204 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 18617 17204 145 145 0 18472 0
[pid=18926] vsize: 74468
Current children cumulated CPU time (s) 1138.89
Current children cumulated vsize (Kb) 76592

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 18117 0 0 0 114776 113 0 0 25 0 1 0 1846627281 76255232 17207 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 18617 17207 145 145 0 18472 0
[pid=18926] vsize: 74468
Current children cumulated CPU time (s) 1148.89
Current children cumulated vsize (Kb) 76592

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 18117 0 0 0 115776 113 0 0 25 0 1 0 1846627281 76255232 17207 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 18617 17207 145 145 0 18472 0
[pid=18926] vsize: 74468
Current children cumulated CPU time (s) 1158.89
Current children cumulated vsize (Kb) 76592

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 18117 0 0 0 116776 113 0 0 25 0 1 0 1846627281 76255232 17207 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 18617 17207 145 145 0 18472 0
[pid=18926] vsize: 74468
Current children cumulated CPU time (s) 1168.89
Current children cumulated vsize (Kb) 76592

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 18117 0 0 0 117776 113 0 0 25 0 1 0 1846627281 76255232 17207 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 18617 17207 145 145 0 18472 0
[pid=18926] vsize: 74468
Current children cumulated CPU time (s) 1178.89
Current children cumulated vsize (Kb) 76592

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 18117 0 0 0 118777 113 0 0 25 0 1 0 1846627281 76255232 17207 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 18617 17207 145 145 0 18472 0
[pid=18926] vsize: 74468
Current children cumulated CPU time (s) 1188.9
Current children cumulated vsize (Kb) 76592

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 18117 0 0 0 119777 114 0 0 25 0 1 0 1846627281 76255232 17207 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 18617 17207 145 145 0 18472 0
[pid=18926] vsize: 74468
Current children cumulated CPU time (s) 1198.91
Current children cumulated vsize (Kb) 76592

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 18117 0 0 0 120777 114 0 0 25 0 1 0 1846627281 76255232 17207 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 18617 17207 145 145 0 18472 0
[pid=18926] vsize: 74468
Current children cumulated CPU time (s) 1208.91
Current children cumulated vsize (Kb) 76592



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 18926
Raw data (/proc/18922/stat): 18922 (minisat+_script) S 18921 18922 5245 0 -1 0 289 239 0 0 0 0 0 0 19 0 1 0 1846627276 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/18922/statm): 531 226 485 147 0 384 0
[pid=18922] vsize: 2124
Raw data (/proc/18926/stat): 18926 (minisat+_64-bit) R 18922 18922 5245 0 -1 0 18117 0 0 0 120777 114 0 0 25 0 1 0 1846627281 76255232 17207 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/18926/statm): 18617 17207 145 145 0 18472 0
[pid=18926] vsize: 74468
Current children cumulated CPU time (s) 1208.91
Current children cumulated vsize (Kb) 76592

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

Child status: 10
Real time (s): 1210.13
CPU time (s): 1208.95
CPU user time (s): 1207.78
CPU system time (s): 1.17582
CPU usage (%): 99.9026
Max. virtual memory (cumulated for all children) (Kb): 76592

Verifier Data

ERROR: no interpretation found !