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/plato.asu.edu/pub/fctp/normalized-mps-v2-20-10-ran14x18.opb
MD5SUM7da782a9a5fff983d0dc41e97459b8ae
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 8215478
Optimality of the best value was proved NO
Number of terms in the objective function 7812
Biggest coefficient in the objective function 5368709120
Number of bits for the biggest coefficient in the objective function 33
Sum of the numbers in the objective function 1450667950777
Number of bits of the sum of numbers in the objective function 41
Biggest number in a constraint 5368709120
Number of bits of the biggest number in a constraint 33
Biggest sum of numbers in a constraint 1450667950777
Number of bits of the biggest sum of numbers41
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1228.55
Number of variables7812
Total number of constraints284
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints284
Minimum length of a constraint31
Maximum length of a constraint540

Trace number 4583

Launcher Data

LAUNCH ON wulflinc3 THE 2005-09-19 18:42:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3043 boxname=wulflinc3 idbench=699 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  7da782a9a5fff983d0dc41e97459b8ae  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-ran14x18.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-ran14x18.opb
IDLAUNCH: 3043
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        895564 kB
Buffers:         36296 kB
Cached:          75864 kB
SwapCached:        856 kB
Active:          69216 kB
Inactive:        45584 kB
HighTotal:      131008 kB
HighFree:        53648 kB
LowTotal:       903652 kB
LowFree:        841916 kB
SwapTotal:     2097136 kB
SwapFree:      2095712 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5720 kB
Slab:            18632 kB
Committed_AS:    72344 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 19:02:49 (client local time) WITH STATUS 0 IN 1208.71 SECONDS
stats: 3043 7 1208.71 0

Solver Data

c Parsing PB file...
c Converting 316 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 314]---> Adder-cost: 488   maxlim: 379886   bits: 19/19
c ---[ 312]---> Adder-cost: 488   maxlim: 381934   bits: 19/19
c ---[ 310]---> Adder-cost: 488   maxlim: 378862   bits: 19/19
c ---[ 308]---> Adder-cost: 490   maxlim: 465902   bits: 19/19
c ---[ 306]---> Adder-cost: 488   maxlim: 378862   bits: 19/19
c ---[ 304]---> Adder-cost: 488   maxlim: 374766   bits: 19/19
c ---[ 302]---> Adder-cost: 488   maxlim: 376814   bits: 19/19
c ---[ 300]---> Adder-cost: 474   maxlim: 260078   bits: 19/18
c ---[ 298]---> Adder-cost: 488   maxlim: 373742   bits: 19/19
c ---[ 296]---> Adder-cost: 488   maxlim: 375790   bits: 19/19
c ---[ 294]---> Adder-cost: 474   maxlim: 260078   bits: 19/18
c ---[ 292]---> Adder-cost: 488   maxlim: 385006   bits: 19/19
c ---[ 290]---> Adder-cost: 488   maxlim: 383982   bits: 19/19
c ---[ 288]---> Adder-cost: 490   maxlim: 460782   bits: 19/19
c ---[ 286]---> Adder-cost: 338   maxlim: 108530   bits: 17/17
c ---[ 284]---> Adder-cost: 364   maxlim: 216050   bits: 18/18
c ---[ 282]---> Adder-cost: 338   maxlim: 107506   bits: 17/17
c ---[ 280]---> Adder-cost: 388   maxlim: 407538   bits: 19/19
c ---[ 278]---> Adder-cost: 364   maxlim: 215026   bits: 18/18
c ---[ 276]---> Adder-cost: 388   maxlim: 403442   bits: 19/19
c ---[ 274]---> Adder-cost: 390   maxlim: 457714   bits: 19/19
c ---[ 272]---> Adder-cost: 390   maxlim: 445426   bits: 19/19
c ---[ 270]---> Adder-cost: 364   maxlim: 218098   bits: 18/18
c ---[ 268]---> Adder-cost: 364   maxlim: 221170   bits: 18/18
c ---[ 266]---> Adder-cost: 388   maxlim: 404466   bits: 19/19
c ---[ 264]---> Adder-cost: 364   maxlim: 218098   bits: 18/18
c ---[ 262]---> Adder-cost: 388   maxlim: 405490   bits: 19/19
c ---[ 260]---> Adder-cost: 338   maxlim: 110578   bits: 17/17
c ---[ 258]---> Adder-cost: 390   maxlim: 455666   bits: 19/19
c ---[ 256]---> Adder-cost: 364   maxlim: 216050   bits: 18/18
c ---[ 254]---> Adder-cost: 388   maxlim: 405490   bits: 19/19
c ---[ 252]---> Adder-cost: 364   maxlim: 220146   bits: 18/18
c ---[ 251]---> BDD-cost:   15
c ---[ 250]---> BDD-cost:   18
c ---[ 249]---> BDD-cost:   16
c ---[ 248]---> BDD-cost:   16
c ---[ 247]---> BDD-cost:   19
c ---[ 246]---> BDD-cost:   17
c ---[ 245]---> BDD-cost:   19
c ---[ 244]---> BDD-cost:   20
c ---[ 243]---> BDD-cost:   20
c ---[ 242]---> BDD-cost:   18
c ---[ 241]---> BDD-cost:   15
c ---[ 240]---> BDD-cost:   15
c ---[ 239]---> BDD-cost:   17
c ---[ 238]---> BDD-cost:   19
c ---[ 237]---> BDD-cost:   17
c ---[ 236]---> BDD-cost:   17
c ---[ 235]---> BDD-cost:   17
c ---[ 234]---> BDD-cost:   14
c ---[ 233]---> BDD-cost:   17
c ---[ 232]---> BDD-cost:   17
c ---[ 231]---> BDD-cost:   17
c ---[ 230]---> BDD-cost:   18
c ---[ 229]---> BDD-cost:   16
c ---[ 228]---> BDD-cost:   17
c ---[ 227]---> BDD-cost:   17
c ---[ 226]---> BDD-cost:   17
c ---[ 225]---> BDD-cost:   17
c ---[ 224]---> BDD-cost:   17
c ---[ 223]---> BDD-cost:   17
c ---[ 222]---> BDD-cost:   17
c ---[ 221]---> BDD-cost:   15
c ---[ 220]---> BDD-cost:   15
c ---[ 219]---> BDD-cost:   18
c ---[ 218]---> BDD-cost:   16
c ---[ 217]---> BDD-cost:   18
c ---[ 216]---> BDD-cost:   20
c ---[ 215]---> BDD-cost:   16
c ---[ 214]---> BDD-cost:   14
c ---[ 213]---> BDD-cost:   16
c ---[ 212]---> BDD-cost:   18
c ---[ 211]---> BDD-cost:   16
c ---[ 210]---> BDD-cost:   18
c ---[ 209]---> BDD-cost:   16
c ---[ 208]---> BDD-cost:   16
c ---[ 207]---> BDD-cost:   17
c ---[ 206]---> BDD-cost:   16
c ---[ 205]---> BDD-cost:   20
c ---[ 204]---> BDD-cost:   16
c ---[ 203]---> BDD-cost:   16
c ---[ 202]---> BDD-cost:   18
c ---[ 201]---> BDD-cost:   15
c ---[ 200]---> BDD-cost:   15
c ---[ 199]---> BDD-cost:   18
c ---[ 198]---> BDD-cost:   20
c ---[ 197]---> BDD-cost:   18
c ---[ 196]---> BDD-cost:   20
c ---[ 195]---> BDD-cost:   14
c ---[ 194]---> BDD-cost:   20
c ---[ 193]---> BDD-cost:   20
c ---[ 192]---> BDD-cost:   18
c ---[ 191]---> BDD-cost:   20
c ---[ 190]---> BDD-cost:   18
c ---[ 189]---> BDD-cost:   16
c ---[ 188]---> BDD-cost:   20
c ---[ 187]---> BDD-cost:   17
c ---[ 186]---> BDD-cost:   20
c ---[ 185]---> BDD-cost:   20
c ---[ 184]---> BDD-cost:   20
c ---[ 183]---> BDD-cost:   18
c ---[ 182]---> BDD-cost:   18
c ---[ 181]---> BDD-cost:   15
c ---[ 180]---> BDD-cost:   15
c ---[ 179]---> BDD-cost:   18
c ---[ 178]---> BDD-cost:   20
c ---[ 177]---> BDD-cost:   18
c ---[ 176]---> BDD-cost:   18
c ---[ 175]---> BDD-cost:   14
c ---[ 174]---> BDD-cost:   22
c ---[ 173]---> BDD-cost:   18
c ---[ 172]---> BDD-cost:   15
c ---[ 171]---> BDD-cost:   18
c ---[ 170]---> BDD-cost:   18
c ---[ 169]---> BDD-cost:   16
c ---[ 168]---> BDD-cost:   19
c ---[ 167]---> BDD-cost:   17
c ---[ 166]---> BDD-cost:   19
c ---[ 165]---> BDD-cost:   22
c ---[ 164]---> BDD-cost:   21
c ---[ 163]---> BDD-cost:   18
c ---[ 162]---> BDD-cost:   15
c ---[ 161]---> BDD-cost:   15
c ---[ 160]---> BDD-cost:   15
c ---[ 159]---> BDD-cost:   18
c ---[ 158]---> BDD-cost:   20
c ---[ 157]---> BDD-cost:   18
c ---[ 156]---> BDD-cost:   18
c ---[ 155]---> BDD-cost:   14
c ---[ 154]---> BDD-cost:   19
c ---[ 153]---> BDD-cost:   18
c ---[ 152]---> BDD-cost:   18
c ---[ 151]---> BDD-cost:   18
c ---[ 150]---> BDD-cost:   18
c ---[ 149]---> BDD-cost:   16
c ---[ 148]---> BDD-cost:   19
c ---[ 147]---> BDD-cost:   17
c ---[ 146]---> BDD-cost:   19
c ---[ 145]---> BDD-cost:   19
c ---[ 144]---> BDD-cost:   19
c ---[ 143]---> BDD-cost:   18
c ---[ 142]---> BDD-cost:   15
c ---[ 141]---> BDD-cost:   15
c ---[ 140]---> BDD-cost:   18
c ---[ 139]---> BDD-cost:   20
c ---[ 138]---> BDD-cost:   20
c ---[ 137]---> BDD-cost:   20
c ---[ 136]---> BDD-cost:   18
c ---[ 135]---> BDD-cost:   18
c ---[ 134]---> BDD-cost:   14
c ---[ 133]---> BDD-cost:   22
c ---[ 132]---> BDD-cost:   18
c ---[ 131]---> BDD-cost:   18
c ---[ 130]---> BDD-cost:   18
c ---[ 129]---> BDD-cost:   16
c ---[ 128]---> BDD-cost:   19
c ---[ 127]---> BDD-cost:   18
c ---[ 126]---> BDD-cost:   17
c ---[ 125]---> BDD-cost:   19
c ---[ 124]---> BDD-cost:   22
c ---[ 123]---> BDD-cost:   22
c ---[ 122]---> BDD-cost:   18
c ---[ 121]---> BDD-cost:   15
c ---[ 120]---> BDD-cost:   15
c ---[ 119]---> BDD-cost:   18
c ---[ 118]---> BDD-cost:   20
c ---[ 117]---> BDD-cost:   18
c ---[ 116]---> BDD-cost:   20
c ---[ 115]---> BDD-cost:   18
c ---[ 114]---> BDD-cost:   14
c ---[ 113]---> BDD-cost:   19
c ---[ 112]---> BDD-cost:   18
c ---[ 111]---> BDD-cost:   18
c ---[ 110]---> BDD-cost:   18
c ---[ 109]---> BDD-cost:   16
c ---[ 108]---> BDD-cost:   19
c ---[ 107]---> BDD-cost:   17
c ---[ 106]---> BDD-cost:   19
c ---[ 105]---> BDD-cost:   14
c ---[ 104]---> BDD-cost:   19
c ---[ 103]---> BDD-cost:   19
c ---[ 102]---> BDD-cost:   18
c ---[ 101]---> BDD-cost:   15
c ---[ 100]---> BDD-cost:   15
c ---[  99]---> BDD-cost:   18
c ---[  98]---> BDD-cost:   20
c ---[  97]---> BDD-cost:   18
c ---[  96]---> BDD-cost:   18
c ---[  95]---> BDD-cost:   14
c ---[  94]---> BDD-cost:   20
c ---[  93]---> BDD-cost:   19
c ---[  92]---> BDD-cost:   18
c ---[  91]---> BDD-cost:   18
c ---[  90]---> BDD-cost:   18
c ---[  89]---> BDD-cost:   16
c ---[  88]---> BDD-cost:   19
c ---[  87]---> BDD-cost:   17
c ---[  86]---> BDD-cost:   19
c ---[  85]---> BDD-cost:   19
c ---[  84]---> BDD-cost:   19
c ---[  83]---> BDD-cost:   18
c ---[  82]---> BDD-cost:   18
c ---[  81]---> BDD-cost:   15
c ---[  80]---> BDD-cost:   20
c ---[  79]---> BDD-cost:   18
c ---[  78]---> BDD-cost:   16
c ---[  77]---> BDD-cost:   19
c ---[  76]---> BDD-cost:   18
c ---[  75]---> BDD-cost:   17
c ---[  74]---> BDD-cost:   20
c ---[  73]---> BDD-cost:   20
c ---[  72]---> BDD-cost:   20
c ---[  71]---> BDD-cost:   18
c ---[  70]---> BDD-cost:   15
c ---[  69]---> BDD-cost:   15
c ---[  68]---> BDD-cost:   18
c ---[  67]---> BDD-cost:   20
c ---[  66]---> BDD-cost:   18
c ---[  65]---> BDD-cost:   18
c ---[  64]---> BDD-cost:   18
c ---[  63]---> BDD-cost:   14
c ---[  62]---> BDD-cost:   17
c ---[  61]---> BDD-cost:   18
c ---[  60]---> BDD-cost:   18
c ---[  59]---> BDD-cost:   18
c ---[  58]---> BDD-cost:   16
c ---[  57]---> BDD-cost:   19
c ---[  56]---> BDD-cost:   17
c ---[  55]---> BDD-cost:   19
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:   17
c ---[  52]---> BDD-cost:   17
c ---[  51]---> BDD-cost:   18
c ---[  50]---> BDD-cost:   15
c ---[  49]---> BDD-cost:   15
c ---[  48]---> BDD-cost:   17
c ---[  47]---> BDD-cost:   17
c ---[  46]---> BDD-cost:   17
c ---[  45]---> BDD-cost:   17
c ---[  44]---> BDD-cost:   14
c ---[  43]---> BDD-cost:   20
c ---[  42]---> BDD-cost:   17
c ---[  41]---> BDD-cost:   17
c ---[  40]---> BDD-cost:   17
c ---[  39]---> BDD-cost:   18
c ---[  38]---> BDD-cost:   16
c ---[  37]---> BDD-cost:   17
c ---[  36]---> BDD-cost:   17
c ---[  35]---> BDD-cost:   17
c ---[  34]---> BDD-cost:   17
c ---[  33]---> BDD-cost:   17
c ---[  32]---> BDD-cost:   18
c ---[  31]---> BDD-cost:   17
c ---[  30]---> BDD-cost:   15
c ---[  29]---> BDD-cost:   15
c ---[  28]---> BDD-cost:   18
c ---[  27]---> BDD-cost:   20
c ---[  26]---> BDD-cost:   18
c ---[  25]---> BDD-cost:   18
c ---[  24]---> BDD-cost:   14
c ---[  23]---> BDD-cost:   20
c ---[  22]---> BDD-cost:   18
c ---[  21]---> BDD-cost:   18
c ---[  20]---> BDD-cost:   18
c ---[  19]---> BDD-cost:   18
c ---[  18]---> BDD-cost:   16
c ---[  17]---> BDD-cost:   19
c ---[  16]---> BDD-cost:   17
c ---[  15]---> BDD-cost:   19
c ---[  14]---> BDD-cost:   20
c ---[  13]---> BDD-cost:   20
c ---[  12]---> BDD-cost:   18
c ---[  11]---> BDD-cost:   15
c ---[  10]---> BDD-cost:   18
c ---[   9]---> BDD-cost:   15
c ---[   8]---> BDD-cost:   18
c ---[   7]---> BDD-cost:   20
c ---[   6]---> BDD-cost:   18
c ---[   5]---> BDD-cost:   18
c ---[   4]---> BDD-cost:   14
c ---[   3]---> BDD-cost:   20
c ---[   2]---> BDD-cost:   18
c ---[   1]---> BDD-cost:   18
c ---[   0]---> BDD-cost:   18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   96690   336663 |   32230       0        0     nan |  0.000 % |
c |       100 |   96690   336663 |   35453     100      300     3.0 | 23.163 % |
c |       250 |   96574   336273 |   38998     239      755     3.2 | 23.254 % |
c |       476 |   96441   335830 |   42898     450     1687     3.7 | 23.361 % |
c |       813 |   96242   335165 |   47187     762     2721     3.6 | 23.525 % |
c |      1319 |   95861   333868 |   51906    1225     4240     3.5 | 23.805 % |
c |      2078 |   95410   332345 |   57097    1932     6743     3.5 | 24.149 % |
c |      3217 |   95169   331534 |   62807    3049    10918     3.6 | 24.334 % |
c |      4925 |   94720   330009 |   69087    4704    17181     3.7 | 24.674 % |
c |      7487 |   94342   328719 |   75996    7229    27644     3.8 | 24.967 % |
c |     11331 |   93939   327342 |   83596   11022    45750     4.2 | 25.272 % |
c |     17097 |   93871   327116 |   91955   16778    84252     5.0 | 25.324 % |
c |     25746 |   93767   326756 |  101151   25415   157264     6.2 | 25.406 % |
c |     38721 |   93758   326727 |  111266   38389   892899    23.3 | 25.414 % |
c |     58182 |   93670   326437 |  122393   57836  1275075    22.0 | 25.483 % |
c |     87374 |   93643   326342 |  134632   87025  3022181    34.7 | 25.505 % |
c |    131163 |   93533   325964 |  148095  130802  3948762    30.2 | 25.599 % |
c |    196848 |   93472   325767 |  162905   54334  6963951   128.2 | 25.655 % |
c |    295374 |   93456   325715 |  179196  152856  9924068    64.9 | 25.668 % |
c |    443164 |   93413   325576 |  197115  136015  6072781    44.6 | 25.707 % |
c |    664847 |   93236   324975 |  216827  167030  9204342    55.1 | 25.840 % |
c |    997374 |   93056   324355 |  238510   87522  5644580    64.5 | 25.991 % |

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/31434/stat): 31434 (minisat+_script) R 31433 31434 31915 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1793903284 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/31434/statm): 174 3 169 147 0 27 0
[pid=31434] 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=31435
New process pid=31436
New process pid=31437
execve syscall for /bin/sed executable
One traced child (pid=31436) exited with status: 0
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=31437) exited with status: 0
One traced child (pid=31435) exited with status: 0
New process pid=31438
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-ran14x18.opb

[startup+10.0037 s]
Raw data (loadavg): 0.93 0.96 0.91 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 2430 0 0 0 976 9 0 0 25 0 1 0 1793903289 10371072 2285 4294967295 134512640 135094434 3221224432 3221223088 134561460 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 2532 2285 145 145 0 2387 0
[pid=31438] vsize: 10128
Current children cumulated CPU time (s) 9.86
Current children cumulated vsize (Kb) 12252

[startup+20.0055 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 2469 0 0 0 1974 9 0 0 25 0 1 0 1793903289 10526720 2324 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31438/statm): 2570 2324 145 145 0 2425 0
[pid=31438] vsize: 10280
Current children cumulated CPU time (s) 19.84
Current children cumulated vsize (Kb) 12404

[startup+30.0064 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 2539 0 0 0 2973 10 0 0 25 0 1 0 1793903289 10817536 2394 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31438/statm): 2641 2394 145 145 0 2496 0
[pid=31438] vsize: 10564
Current children cumulated CPU time (s) 29.84
Current children cumulated vsize (Kb) 12688

[startup+40.0072 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 2694 0 0 0 3970 12 0 0 25 0 1 0 1793903289 11485184 2549 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 2804 2549 145 145 0 2659 0
[pid=31438] vsize: 11216
Current children cumulated CPU time (s) 39.83
Current children cumulated vsize (Kb) 13340

[startup+50.008 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 2842 0 0 0 4967 14 0 0 25 0 1 0 1793903289 12058624 2697 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 2944 2697 145 145 0 2799 0
[pid=31438] vsize: 11776
Current children cumulated CPU time (s) 49.82
Current children cumulated vsize (Kb) 13900

[startup+60.0089 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 3755 0 0 0 5955 18 0 0 25 0 1 0 1793903289 15880192 3610 4294967295 134512640 135094434 3221224432 3221223120 134554739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 3877 3610 145 145 0 3732 0
[pid=31438] vsize: 15508
Current children cumulated CPU time (s) 59.74
Current children cumulated vsize (Kb) 17632

[startup+70.0107 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 4077 0 0 0 6950 21 0 0 25 0 1 0 1793903289 17154048 3932 4294967295 134512640 135094434 3221224432 3221223088 134561463 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 4188 3932 145 145 0 4043 0
[pid=31438] vsize: 16752
Current children cumulated CPU time (s) 69.72
Current children cumulated vsize (Kb) 18876

[startup+80.0115 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 4403 0 0 0 7945 23 0 0 25 0 1 0 1793903289 18444288 4258 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 4503 4258 145 145 0 4358 0
[pid=31438] vsize: 18012
Current children cumulated CPU time (s) 79.69
Current children cumulated vsize (Kb) 20136

[startup+90.0114 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 5495 0 0 0 8928 29 0 0 25 0 1 0 1793903289 23134208 5350 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31438/statm): 5648 5350 145 145 0 5503 0
[pid=31438] vsize: 22592
Current children cumulated CPU time (s) 89.58
Current children cumulated vsize (Kb) 24716

[startup+100.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 6322 0 0 0 9915 36 0 0 25 0 1 0 1793903289 26476544 6177 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31438/statm): 6464 6177 145 145 0 6319 0
[pid=31438] vsize: 25856
Current children cumulated CPU time (s) 99.52
Current children cumulated vsize (Kb) 27980

[startup+110.013 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 6510 0 0 0 10911 38 0 0 25 0 1 0 1793903289 27213824 6365 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31438/statm): 6644 6365 145 145 0 6499 0
[pid=31438] vsize: 26576
Current children cumulated CPU time (s) 109.5
Current children cumulated vsize (Kb) 28700

[startup+120.015 s]
Raw data (loadavg): 1.07 0.98 0.91 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 6795 0 0 0 11906 41 0 0 25 0 1 0 1793903289 28344320 6650 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31438/statm): 6920 6650 145 145 0 6775 0
[pid=31438] vsize: 27680
Current children cumulated CPU time (s) 119.48
Current children cumulated vsize (Kb) 29804

[startup+130.016 s]
Raw data (loadavg): 1.13 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 7348 0 0 0 12899 44 0 0 25 0 1 0 1793903289 30564352 7203 4294967295 134512640 135094434 3221224432 3221223056 134557642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31438/statm): 7462 7203 145 145 0 7317 0
[pid=31438] vsize: 29848
Current children cumulated CPU time (s) 129.44
Current children cumulated vsize (Kb) 31972

[startup+140.016 s]
Raw data (loadavg): 1.11 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 7545 0 0 0 13895 46 0 0 25 0 1 0 1793903289 31338496 7400 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31438/statm): 7651 7400 145 145 0 7506 0
[pid=31438] vsize: 30604
Current children cumulated CPU time (s) 139.42
Current children cumulated vsize (Kb) 32728

[startup+150.017 s]
Raw data (loadavg): 1.09 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 7736 0 0 0 14891 48 0 0 25 0 1 0 1793903289 32096256 7591 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31438/statm): 7836 7591 145 145 0 7691 0
[pid=31438] vsize: 31344
Current children cumulated CPU time (s) 149.4
Current children cumulated vsize (Kb) 33468

[startup+160.018 s]
Raw data (loadavg): 1.08 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 7937 0 0 0 15887 49 0 0 25 0 1 0 1793903289 33411072 7792 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31438/statm): 8157 7792 145 145 0 8012 0
[pid=31438] vsize: 32628
Current children cumulated CPU time (s) 159.37
Current children cumulated vsize (Kb) 34752

[startup+170.019 s]
Raw data (loadavg): 1.07 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 8456 0 0 0 16881 53 0 0 25 0 1 0 1793903289 35500032 8311 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31438/statm): 8667 8311 145 145 0 8522 0
[pid=31438] vsize: 34668
Current children cumulated CPU time (s) 169.35
Current children cumulated vsize (Kb) 36792

[startup+180.02 s]
Raw data (loadavg): 1.06 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 8663 0 0 0 17877 55 0 0 25 0 1 0 1793903289 36319232 8518 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31438/statm): 8867 8518 145 145 0 8722 0
[pid=31438] vsize: 35468
Current children cumulated CPU time (s) 179.33
Current children cumulated vsize (Kb) 37592

[startup+190.021 s]
Raw data (loadavg): 1.05 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 9908 0 0 0 18858 64 0 0 25 0 1 0 1793903289 41377792 9763 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31438/statm): 10102 9763 145 145 0 9957 0
[pid=31438] vsize: 40408
Current children cumulated CPU time (s) 189.23
Current children cumulated vsize (Kb) 42532

[startup+200.022 s]
Raw data (loadavg): 1.04 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 9908 0 0 0 19857 64 0 0 25 0 1 0 1793903289 41377792 9763 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31438/statm): 10102 9763 145 145 0 9957 0
[pid=31438] vsize: 40408
Current children cumulated CPU time (s) 199.22
Current children cumulated vsize (Kb) 42532

[startup+210.022 s]
Raw data (loadavg): 1.03 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 9908 0 0 0 20857 65 0 0 25 0 1 0 1793903289 41377792 9763 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31438/statm): 10102 9763 145 145 0 9957 0
[pid=31438] vsize: 40408
Current children cumulated CPU time (s) 209.23
Current children cumulated vsize (Kb) 42532

[startup+220.024 s]
Raw data (loadavg): 1.03 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 10582 0 0 0 21844 70 0 0 25 0 1 0 1793903289 44142592 10437 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31438/statm): 10777 10437 145 145 0 10632 0
[pid=31438] vsize: 43108
Current children cumulated CPU time (s) 219.15
Current children cumulated vsize (Kb) 45232

[startup+230.025 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 11447 0 0 0 22830 76 0 0 25 0 1 0 1793903289 47710208 11302 4294967295 134512640 135094434 3221224432 3221223072 134562110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31438/statm): 11648 11302 145 145 0 11503 0
[pid=31438] vsize: 46592
Current children cumulated CPU time (s) 229.07
Current children cumulated vsize (Kb) 48716

[startup+240.026 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 11523 0 0 0 23829 77 0 0 25 0 1 0 1793903289 48037888 11378 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31438/statm): 11728 11378 145 145 0 11583 0
[pid=31438] vsize: 46912
Current children cumulated CPU time (s) 239.07
Current children cumulated vsize (Kb) 49036

[startup+250.028 s]
Raw data (loadavg): 1.02 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 11563 0 0 0 24829 77 0 0 25 0 1 0 1793903289 48214016 11418 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31438/statm): 11771 11418 145 145 0 11626 0
[pid=31438] vsize: 47084
Current children cumulated CPU time (s) 249.07
Current children cumulated vsize (Kb) 49208

[startup+260.029 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 11584 0 0 0 25828 78 0 0 25 0 1 0 1793903289 48308224 11439 4294967295 134512640 135094434 3221224432 3221223088 134558172 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31438/statm): 11794 11439 145 145 0 11649 0
[pid=31438] vsize: 47176
Current children cumulated CPU time (s) 259.07
Current children cumulated vsize (Kb) 49300

[startup+270.03 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 11737 0 0 0 26825 79 0 0 25 0 1 0 1793903289 48947200 11592 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 11950 11592 145 145 0 11805 0
[pid=31438] vsize: 47800
Current children cumulated CPU time (s) 269.05
Current children cumulated vsize (Kb) 49924

[startup+280.031 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 11880 0 0 0 27824 80 0 0 25 0 1 0 1793903289 49537024 11735 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 12094 11735 145 145 0 11949 0
[pid=31438] vsize: 48376
Current children cumulated CPU time (s) 279.05
Current children cumulated vsize (Kb) 50500

[startup+290.032 s]
Raw data (loadavg): 1.01 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 12015 0 0 0 28822 80 0 0 25 0 1 0 1793903289 50102272 11870 4294967295 134512640 135094434 3221224432 3221223044 134562998 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 12232 11870 145 145 0 12087 0
[pid=31438] vsize: 48928
Current children cumulated CPU time (s) 289.03
Current children cumulated vsize (Kb) 51052

[startup+300.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 12172 0 0 0 29820 81 0 0 25 0 1 0 1793903289 50745344 12027 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 12389 12027 145 145 0 12244 0
[pid=31438] vsize: 49556
Current children cumulated CPU time (s) 299.02
Current children cumulated vsize (Kb) 51680

[startup+310.034 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 12948 0 0 0 30810 85 0 0 25 0 1 0 1793903289 53923840 12803 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 13165 12803 145 145 0 13020 0
[pid=31438] vsize: 52660
Current children cumulated CPU time (s) 308.96
Current children cumulated vsize (Kb) 54784

[startup+320.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 14204 0 0 0 31793 93 0 0 25 0 1 0 1793903289 59072512 14059 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 14422 14059 145 145 0 14277 0
[pid=31438] vsize: 57688
Current children cumulated CPU time (s) 318.87
Current children cumulated vsize (Kb) 59812

[startup+330.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 14414 0 0 0 32790 95 0 0 25 0 1 0 1793903289 59932672 14269 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 14632 14269 145 145 0 14487 0
[pid=31438] vsize: 58528
Current children cumulated CPU time (s) 328.86
Current children cumulated vsize (Kb) 60652

[startup+340.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 14605 0 0 0 33786 97 0 0 25 0 1 0 1793903289 60715008 14460 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 14823 14460 145 145 0 14678 0
[pid=31438] vsize: 59292
Current children cumulated CPU time (s) 338.84
Current children cumulated vsize (Kb) 61416

[startup+350.036 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 14717 0 0 0 34783 99 0 0 25 0 1 0 1793903289 61169664 14572 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 14934 14572 145 145 0 14789 0
[pid=31438] vsize: 59736
Current children cumulated CPU time (s) 348.83
Current children cumulated vsize (Kb) 61860

[startup+360.037 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 15102 0 0 0 35777 101 0 0 25 0 1 0 1793903289 62734336 14957 4294967295 134512640 135094434 3221224432 3221223024 134557300 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 15316 14957 145 145 0 15171 0
[pid=31438] vsize: 61264
Current children cumulated CPU time (s) 358.79
Current children cumulated vsize (Kb) 63388

[startup+370.038 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 16018 0 0 0 36763 107 0 0 25 0 1 0 1793903289 66453504 15873 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 16224 15873 145 145 0 16079 0
[pid=31438] vsize: 64896
Current children cumulated CPU time (s) 368.71
Current children cumulated vsize (Kb) 67020

[startup+380.039 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 16639 0 0 0 37754 110 0 0 25 0 1 0 1793903289 68968448 16494 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 16838 16494 145 145 0 16693 0
[pid=31438] vsize: 67352
Current children cumulated CPU time (s) 378.65
Current children cumulated vsize (Kb) 69476

[startup+390.039 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17139 0 0 0 38745 115 0 0 25 0 1 0 1793903289 70995968 16994 4294967295 134512640 135094434 3221224432 3221223044 134563066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 16994 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 388.61
Current children cumulated vsize (Kb) 71456

[startup+400.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17139 0 0 0 39746 115 0 0 25 0 1 0 1793903289 70995968 16994 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 16994 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 398.62
Current children cumulated vsize (Kb) 71456

[startup+410.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17139 0 0 0 40746 115 0 0 25 0 1 0 1793903289 70995968 16994 4294967295 134512640 135094434 3221224432 3221223044 134563074 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 16994 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 408.62
Current children cumulated vsize (Kb) 71456

[startup+420.041 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17139 0 0 0 41746 115 0 0 25 0 1 0 1793903289 70995968 16994 4294967295 134512640 135094434 3221224432 3221223088 134558414 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 16994 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 418.62
Current children cumulated vsize (Kb) 71456

[startup+430.042 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17139 0 0 0 42746 116 0 0 25 0 1 0 1793903289 70995968 16994 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 16994 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 428.63
Current children cumulated vsize (Kb) 71456

[startup+440.042 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17139 0 0 0 43746 116 0 0 25 0 1 0 1793903289 70995968 16994 4294967295 134512640 135094434 3221224432 3221223104 134556156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 16994 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 438.63
Current children cumulated vsize (Kb) 71456

[startup+450.042 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17139 0 0 0 44746 116 0 0 25 0 1 0 1793903289 70995968 16994 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 16994 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 448.63
Current children cumulated vsize (Kb) 71456

[startup+460.043 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17139 0 0 0 45746 116 0 0 25 0 1 0 1793903289 70995968 16994 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 16994 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 458.63
Current children cumulated vsize (Kb) 71456

[startup+470.044 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17139 0 0 0 46746 116 0 0 25 0 1 0 1793903289 70995968 16994 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 16994 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 468.63
Current children cumulated vsize (Kb) 71456

[startup+480.046 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17139 0 0 0 47747 116 0 0 25 0 1 0 1793903289 70995968 16994 4294967295 134512640 135094434 3221224432 3221223024 134557377 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 16994 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 478.64
Current children cumulated vsize (Kb) 71456

[startup+490.047 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17139 0 0 0 48746 116 0 0 25 0 1 0 1793903289 70995968 16994 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 16994 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 488.63
Current children cumulated vsize (Kb) 71456

[startup+500.048 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17139 0 0 0 49747 116 0 0 25 0 1 0 1793903289 70995968 16994 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 16994 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 498.64
Current children cumulated vsize (Kb) 71456

[startup+510.048 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17139 0 0 0 50747 116 0 0 25 0 1 0 1793903289 70995968 16994 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 16994 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 508.64
Current children cumulated vsize (Kb) 71456

[startup+520.049 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17139 0 0 0 51747 116 0 0 25 0 1 0 1793903289 70995968 16994 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 16994 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 518.64
Current children cumulated vsize (Kb) 71456

[startup+530.05 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17139 0 0 0 52746 117 0 0 25 0 1 0 1793903289 70995968 16994 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 16994 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 528.64
Current children cumulated vsize (Kb) 71456

[startup+540.051 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17139 0 0 0 53746 117 0 0 25 0 1 0 1793903289 70995968 16994 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 16994 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 538.64
Current children cumulated vsize (Kb) 71456

[startup+550.052 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17139 0 0 0 54747 117 0 0 25 0 1 0 1793903289 70995968 16994 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 16994 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 548.65
Current children cumulated vsize (Kb) 71456

[startup+560.053 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17139 0 0 0 55747 117 0 0 25 0 1 0 1793903289 70995968 16994 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 16994 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 558.65
Current children cumulated vsize (Kb) 71456

[startup+570.053 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17139 0 0 0 56747 117 0 0 25 0 1 0 1793903289 70995968 16994 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 16994 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 568.65
Current children cumulated vsize (Kb) 71456

[startup+580.054 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17139 0 0 0 57747 117 0 0 25 0 1 0 1793903289 70995968 16994 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 16994 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 578.65
Current children cumulated vsize (Kb) 71456

[startup+590.054 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17139 0 0 0 58747 117 0 0 25 0 1 0 1793903289 70995968 16994 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 16994 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 588.65
Current children cumulated vsize (Kb) 71456

[startup+600.055 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17147 0 0 0 59748 117 0 0 25 0 1 0 1793903289 70995968 17002 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 17002 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 598.66
Current children cumulated vsize (Kb) 71456

[startup+610.056 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17153 0 0 0 60748 117 0 0 25 0 1 0 1793903289 70995968 17008 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 17008 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 608.66
Current children cumulated vsize (Kb) 71456

[startup+620.057 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17158 0 0 0 61748 117 0 0 25 0 1 0 1793903289 70995968 17013 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 17013 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 618.66
Current children cumulated vsize (Kb) 71456

[startup+630.057 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17159 0 0 0 62748 117 0 0 25 0 1 0 1793903289 70995968 17014 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 17014 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 628.66
Current children cumulated vsize (Kb) 71456

[startup+640.058 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17159 0 0 0 63748 117 0 0 25 0 1 0 1793903289 70995968 17014 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 17014 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 638.66
Current children cumulated vsize (Kb) 71456

[startup+650.059 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17159 0 0 0 64748 117 0 0 25 0 1 0 1793903289 70995968 17014 4294967295 134512640 135094434 3221224432 3221223044 134563137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 17014 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 648.66
Current children cumulated vsize (Kb) 71456

[startup+660.059 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17159 0 0 0 65749 117 0 0 25 0 1 0 1793903289 70995968 17014 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 17014 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 658.67
Current children cumulated vsize (Kb) 71456

[startup+670.061 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17159 0 0 0 66749 117 0 0 25 0 1 0 1793903289 70995968 17014 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 17014 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 668.67
Current children cumulated vsize (Kb) 71456

[startup+680.062 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17159 0 0 0 67749 117 0 0 25 0 1 0 1793903289 70995968 17014 4294967295 134512640 135094434 3221224432 3221223088 134561766 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 17014 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 678.67
Current children cumulated vsize (Kb) 71456

[startup+690.061 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17159 0 0 0 68749 118 0 0 25 0 1 0 1793903289 70995968 17014 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 17014 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 688.68
Current children cumulated vsize (Kb) 71456

[startup+700.063 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17159 0 0 0 69749 118 0 0 25 0 1 0 1793903289 70995968 17014 4294967295 134512640 135094434 3221224432 3221223056 134557648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 17014 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 698.68
Current children cumulated vsize (Kb) 71456

[startup+710.063 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17159 0 0 0 70750 118 0 0 25 0 1 0 1793903289 70995968 17014 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 17014 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 708.69
Current children cumulated vsize (Kb) 71456

[startup+720.064 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17159 0 0 0 71750 118 0 0 25 0 1 0 1793903289 70995968 17014 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 17014 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 718.69
Current children cumulated vsize (Kb) 71456

[startup+730.065 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17159 0 0 0 72750 118 0 0 25 0 1 0 1793903289 70995968 17014 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 17014 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 728.69
Current children cumulated vsize (Kb) 71456

[startup+740.066 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17159 0 0 0 73750 118 0 0 25 0 1 0 1793903289 70995968 17014 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 17014 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 738.69
Current children cumulated vsize (Kb) 71456

[startup+750.066 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17160 0 0 0 74751 118 0 0 25 0 1 0 1793903289 70995968 17015 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 17015 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 748.7
Current children cumulated vsize (Kb) 71456

[startup+760.067 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17160 0 0 0 75751 118 0 0 25 0 1 0 1793903289 70995968 17015 4294967295 134512640 135094434 3221224432 3221223072 134562149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 17015 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 758.7
Current children cumulated vsize (Kb) 71456

[startup+770.068 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17160 0 0 0 76750 118 0 0 25 0 1 0 1793903289 70995968 17015 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 17015 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 768.69
Current children cumulated vsize (Kb) 71456

[startup+780.069 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17160 0 0 0 77751 118 0 0 25 0 1 0 1793903289 70995968 17015 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 17015 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 778.7
Current children cumulated vsize (Kb) 71456

[startup+790.07 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17160 0 0 0 78751 118 0 0 25 0 1 0 1793903289 70995968 17015 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 17015 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 788.7
Current children cumulated vsize (Kb) 71456

[startup+800.071 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17160 0 0 0 79751 118 0 0 25 0 1 0 1793903289 70995968 17015 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 17015 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 798.7
Current children cumulated vsize (Kb) 71456

[startup+810.072 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17160 0 0 0 80751 118 0 0 25 0 1 0 1793903289 70995968 17015 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 17015 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 808.7
Current children cumulated vsize (Kb) 71456

[startup+820.072 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17162 0 0 0 81751 118 0 0 25 0 1 0 1793903289 70995968 17017 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17333 17017 145 145 0 17188 0
[pid=31438] vsize: 69332
Current children cumulated CPU time (s) 818.7
Current children cumulated vsize (Kb) 71456

[startup+830.073 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17241 0 0 0 82750 119 0 0 25 0 1 0 1793903289 71323648 17096 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17413 17096 145 145 0 17268 0
[pid=31438] vsize: 69652
Current children cumulated CPU time (s) 828.7
Current children cumulated vsize (Kb) 71776

[startup+840.074 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17498 0 0 0 83745 121 0 0 25 0 1 0 1793903289 72343552 17353 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17662 17353 145 145 0 17517 0
[pid=31438] vsize: 70648
Current children cumulated CPU time (s) 838.67
Current children cumulated vsize (Kb) 72772

[startup+850.075 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17518 0 0 0 84745 121 0 0 25 0 1 0 1793903289 72421376 17373 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17681 17373 145 145 0 17536 0
[pid=31438] vsize: 70724
Current children cumulated CPU time (s) 848.67
Current children cumulated vsize (Kb) 72848

[startup+860.076 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17518 0 0 0 85745 121 0 0 25 0 1 0 1793903289 72421376 17373 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17681 17373 145 145 0 17536 0
[pid=31438] vsize: 70724
Current children cumulated CPU time (s) 858.67
Current children cumulated vsize (Kb) 72848

[startup+870.077 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17518 0 0 0 86745 121 0 0 25 0 1 0 1793903289 72421376 17373 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17681 17373 145 145 0 17536 0
[pid=31438] vsize: 70724
Current children cumulated CPU time (s) 868.67
Current children cumulated vsize (Kb) 72848

[startup+880.077 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17518 0 0 0 87746 121 0 0 25 0 1 0 1793903289 72421376 17373 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17681 17373 145 145 0 17536 0
[pid=31438] vsize: 70724
Current children cumulated CPU time (s) 878.68
Current children cumulated vsize (Kb) 72848

[startup+890.077 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17518 0 0 0 88746 121 0 0 25 0 1 0 1793903289 72421376 17373 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17681 17373 145 145 0 17536 0
[pid=31438] vsize: 70724
Current children cumulated CPU time (s) 888.68
Current children cumulated vsize (Kb) 72848

[startup+900.078 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17518 0 0 0 89746 121 0 0 25 0 1 0 1793903289 72421376 17373 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17681 17373 145 145 0 17536 0
[pid=31438] vsize: 70724
Current children cumulated CPU time (s) 898.68
Current children cumulated vsize (Kb) 72848

[startup+910.079 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17518 0 0 0 90746 121 0 0 25 0 1 0 1793903289 72421376 17373 4294967295 134512640 135094434 3221224432 3221223044 134563066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17681 17373 145 145 0 17536 0
[pid=31438] vsize: 70724
Current children cumulated CPU time (s) 908.68
Current children cumulated vsize (Kb) 72848

[startup+920.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17518 0 0 0 91746 121 0 0 25 0 1 0 1793903289 72421376 17373 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17681 17373 145 145 0 17536 0
[pid=31438] vsize: 70724
Current children cumulated CPU time (s) 918.68
Current children cumulated vsize (Kb) 72848

[startup+930.081 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17518 0 0 0 92747 121 0 0 25 0 1 0 1793903289 72421376 17373 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17681 17373 145 145 0 17536 0
[pid=31438] vsize: 70724
Current children cumulated CPU time (s) 928.69
Current children cumulated vsize (Kb) 72848

[startup+940.081 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17518 0 0 0 93747 121 0 0 25 0 1 0 1793903289 72421376 17373 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17681 17373 145 145 0 17536 0
[pid=31438] vsize: 70724
Current children cumulated CPU time (s) 938.69
Current children cumulated vsize (Kb) 72848

[startup+950.082 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17518 0 0 0 94746 123 0 0 25 0 1 0 1793903289 72421376 17373 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17681 17373 145 145 0 17536 0
[pid=31438] vsize: 70724
Current children cumulated CPU time (s) 948.7
Current children cumulated vsize (Kb) 72848

[startup+960.082 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17518 0 0 0 95746 123 0 0 25 0 1 0 1793903289 72421376 17373 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17681 17373 145 145 0 17536 0
[pid=31438] vsize: 70724
Current children cumulated CPU time (s) 958.7
Current children cumulated vsize (Kb) 72848

[startup+970.084 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17518 0 0 0 96746 123 0 0 25 0 1 0 1793903289 72421376 17373 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17681 17373 145 145 0 17536 0
[pid=31438] vsize: 70724
Current children cumulated CPU time (s) 968.7
Current children cumulated vsize (Kb) 72848

[startup+980.085 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17518 0 0 0 97745 124 0 0 25 0 1 0 1793903289 72421376 17373 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17681 17373 145 145 0 17536 0
[pid=31438] vsize: 70724
Current children cumulated CPU time (s) 978.7
Current children cumulated vsize (Kb) 72848

[startup+990.085 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17518 0 0 0 98745 124 0 0 25 0 1 0 1793903289 72421376 17373 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17681 17373 145 145 0 17536 0
[pid=31438] vsize: 70724
Current children cumulated CPU time (s) 988.7
Current children cumulated vsize (Kb) 72848

[startup+1000.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17518 0 0 0 99746 124 0 0 25 0 1 0 1793903289 72421376 17373 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17681 17373 145 145 0 17536 0
[pid=31438] vsize: 70724
Current children cumulated CPU time (s) 998.71
Current children cumulated vsize (Kb) 72848

[startup+1010.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17518 0 0 0 100746 124 0 0 25 0 1 0 1793903289 72421376 17373 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17681 17373 145 145 0 17536 0
[pid=31438] vsize: 70724
Current children cumulated CPU time (s) 1008.71
Current children cumulated vsize (Kb) 72848

[startup+1020.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17518 0 0 0 101746 124 0 0 25 0 1 0 1793903289 72421376 17373 4294967295 134512640 135094434 3221224432 3221223044 134563080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17681 17373 145 145 0 17536 0
[pid=31438] vsize: 70724
Current children cumulated CPU time (s) 1018.71
Current children cumulated vsize (Kb) 72848

[startup+1030.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17518 0 0 0 102746 125 0 0 25 0 1 0 1793903289 72421376 17373 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17681 17373 145 145 0 17536 0
[pid=31438] vsize: 70724
Current children cumulated CPU time (s) 1028.72
Current children cumulated vsize (Kb) 72848

[startup+1040.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17518 0 0 0 103746 125 0 0 25 0 1 0 1793903289 72421376 17373 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17681 17373 145 145 0 17536 0
[pid=31438] vsize: 70724
Current children cumulated CPU time (s) 1038.72
Current children cumulated vsize (Kb) 72848

[startup+1050.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 17523 0 0 0 104746 125 0 0 25 0 1 0 1793903289 72421376 17378 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 17681 17378 145 145 0 17536 0
[pid=31438] vsize: 70724
Current children cumulated CPU time (s) 1048.72
Current children cumulated vsize (Kb) 72848

[startup+1060.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 18208 0 0 0 105736 129 0 0 25 0 1 0 1793903289 75218944 18063 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 18364 18063 145 145 0 18219 0
[pid=31438] vsize: 73456
Current children cumulated CPU time (s) 1058.66
Current children cumulated vsize (Kb) 75580

[startup+1070.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 18208 0 0 0 106736 129 0 0 25 0 1 0 1793903289 75218944 18063 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 18364 18063 145 145 0 18219 0
[pid=31438] vsize: 73456
Current children cumulated CPU time (s) 1068.66
Current children cumulated vsize (Kb) 75580

[startup+1080.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 18209 0 0 0 107737 129 0 0 25 0 1 0 1793903289 75218944 18064 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 18364 18064 145 145 0 18219 0
[pid=31438] vsize: 73456
Current children cumulated CPU time (s) 1078.67
Current children cumulated vsize (Kb) 75580

[startup+1090.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 18209 0 0 0 108736 129 0 0 25 0 1 0 1793903289 75218944 18064 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 18364 18064 145 145 0 18219 0
[pid=31438] vsize: 73456
Current children cumulated CPU time (s) 1088.66
Current children cumulated vsize (Kb) 75580

[startup+1100.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 18209 0 0 0 109737 129 0 0 25 0 1 0 1793903289 75218944 18064 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 18364 18064 145 145 0 18219 0
[pid=31438] vsize: 73456
Current children cumulated CPU time (s) 1098.67
Current children cumulated vsize (Kb) 75580

[startup+1110.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 18209 0 0 0 110737 129 0 0 25 0 1 0 1793903289 75218944 18064 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 18364 18064 145 145 0 18219 0
[pid=31438] vsize: 73456
Current children cumulated CPU time (s) 1108.67
Current children cumulated vsize (Kb) 75580

[startup+1120.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 18209 0 0 0 111737 129 0 0 25 0 1 0 1793903289 75218944 18064 4294967295 134512640 135094434 3221224432 3221223024 134556760 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 18364 18064 145 145 0 18219 0
[pid=31438] vsize: 73456
Current children cumulated CPU time (s) 1118.67
Current children cumulated vsize (Kb) 75580

[startup+1130.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 18209 0 0 0 112736 129 0 0 25 0 1 0 1793903289 75218944 18064 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31438/statm): 18364 18064 145 145 0 18219 0
[pid=31438] vsize: 73456
Current children cumulated CPU time (s) 1128.66
Current children cumulated vsize (Kb) 75580

[startup+1140.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 18209 0 0 0 113736 130 0 0 25 0 1 0 1793903289 75218944 18064 4294967295 134512640 135094434 3221224432 3221223072 134562088 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31438/statm): 18364 18064 145 145 0 18219 0
[pid=31438] vsize: 73456
Current children cumulated CPU time (s) 1138.67
Current children cumulated vsize (Kb) 75580

[startup+1150.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 18209 0 0 0 114736 130 0 0 25 0 1 0 1793903289 75218944 18064 4294967295 134512640 135094434 3221224432 3221223088 134561502 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 18364 18064 145 145 0 18219 0
[pid=31438] vsize: 73456
Current children cumulated CPU time (s) 1148.67
Current children cumulated vsize (Kb) 75580

[startup+1160.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 18209 0 0 0 115736 130 0 0 25 0 1 0 1793903289 75218944 18064 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 18364 18064 145 145 0 18219 0
[pid=31438] vsize: 73456
Current children cumulated CPU time (s) 1158.67
Current children cumulated vsize (Kb) 75580

[startup+1170.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 18209 0 0 0 116736 130 0 0 25 0 1 0 1793903289 75218944 18064 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 18364 18064 145 145 0 18219 0
[pid=31438] vsize: 73456
Current children cumulated CPU time (s) 1168.67
Current children cumulated vsize (Kb) 75580

[startup+1180.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 18209 0 0 0 117736 130 0 0 25 0 1 0 1793903289 75218944 18064 4294967295 134512640 135094434 3221224432 3221223024 134557407 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 18364 18064 145 145 0 18219 0
[pid=31438] vsize: 73456
Current children cumulated CPU time (s) 1178.67
Current children cumulated vsize (Kb) 75580

[startup+1190.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 18209 0 0 0 118736 130 0 0 25 0 1 0 1793903289 75218944 18064 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 18364 18064 145 145 0 18219 0
[pid=31438] vsize: 73456
Current children cumulated CPU time (s) 1188.67
Current children cumulated vsize (Kb) 75580

[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 18209 0 0 0 119737 130 0 0 25 0 1 0 1793903289 75218944 18064 4294967295 134512640 135094434 3221224432 3221223052 134562986 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 18364 18064 145 145 0 18219 0
[pid=31438] vsize: 73456
Current children cumulated CPU time (s) 1198.68
Current children cumulated vsize (Kb) 75580

[startup+1210.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 18209 0 0 0 120737 130 0 0 25 0 1 0 1793903289 75218944 18064 4294967295 134512640 135094434 3221224432 3221223092 134553487 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 18364 18064 145 145 0 18219 0
[pid=31438] vsize: 73456
Current children cumulated CPU time (s) 1208.68
Current children cumulated vsize (Kb) 75580



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/57 31438
Raw data (/proc/31434/stat): 31434 (minisat+_script) S 31433 31434 31915 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1793903284 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31434/statm): 531 226 485 147 0 384 0
[pid=31434] vsize: 2124
Raw data (/proc/31438/stat): 31438 (minisat+_64-bit) R 31434 31434 31915 0 -1 0 18209 0 0 0 120737 130 0 0 25 0 1 0 1793903289 75218944 18064 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31438/statm): 18364 18064 145 145 0 18219 0
[pid=31438] vsize: 73456
Current children cumulated CPU time (s) 1208.68
Current children cumulated vsize (Kb) 75580

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

Child status: 0
Real time (s): 1210.14
CPU time (s): 1208.71
CPU user time (s): 1207.38
CPU system time (s): 1.3378
CPU usage (%): 99.882
Max. virtual memory (cumulated for all children) (Kb): 75580

Verifier Data

ERROR: no interpretation found !