Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-dcmulti.opb
MD5SUM6ffc4ed72f4dd993b121ae0a2045731e
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 9505
Biggest coefficient in the objective function 697303040
Number of bits for the biggest coefficient in the objective function 30
Sum of the numbers in the objective function 66656504525
Number of bits of the sum of numbers in the objective function 36
Biggest number in a constraint 697303040
Number of bits of the biggest number in a constraint 30
Biggest sum of numbers in a constraint 66656504525
Number of bits of the biggest sum of numbers36
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables9535
Total number of constraints365
Number of constraints which are clauses27
Number of constraints which are cardinality constraints (but not clauses)80
Number of constraints which are nor clauses,nor cardinality constraints258
Minimum length of a constraint1
Maximum length of a constraint280

Trace number 6081

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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:        858412 kB
Buffers:         24440 kB
Cached:         118796 kB
SwapCached:        856 kB
Active:          33124 kB
Inactive:       112732 kB
HighTotal:      131008 kB
HighFree:        26768 kB
LowTotal:       903652 kB
LowFree:        831644 kB
SwapTotal:     2097892 kB
SwapFree:      2096528 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5732 kB
Slab:            24836 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:28:27 (client local time) WITH STATUS 0 IN 1206.68 SECONDS
stats: 3233 7 1206.68 0

Solver Data

c Parsing PB file...
c Converting 368 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################################################################
c   -- Clauses(.)/Splits(s): s....s.....sssssssssssssssssss....s.....ssssssssssssssssss....s.....sssssssssssssssssss
c ---[ 427]---> BDD-cost:   14
c ---[ 426]---> Sorter-cost: 1116     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 425]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 424]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 422]---> BDD-cost:   15
c ---[ 421]---> BDD-cost:   14
c ---[ 420]---> BDD-cost:   14
c ---[ 419]---> BDD-cost:   13
c ---[ 418]---> BDD-cost:   14
c ---[ 416]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 415]---> BDD-cost:   14
c ---[ 413]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 411]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 409]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 407]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 405]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 403]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 401]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 399]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 397]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 395]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 394]---> BDD-cost:   13
c ---[ 392]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 391]---> BDD-cost:   16
c ---[ 390]---> BDD-cost:    7
c ---[ 389]---> BDD-cost:   15
c ---[ 388]---> BDD-cost:    4
c ---[ 386]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 385]---> BDD-cost:   24
c ---[ 384]---> BDD-cost:    6
c ---[ 381]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 380]---> BDD-cost:   14
c ---[ 378]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 377]---> BDD-cost:   16
c ---[ 376]---> BDD-cost:    7
c ---[ 375]---> BDD-cost:   15
c ---[ 374]---> BDD-cost:    4
c ---[ 372]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 371]---> BDD-cost:   23
c ---[ 370]---> BDD-cost:    8
c ---[ 367]---> Sorter-cost:  915     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 365]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 363]---> Sorter-cost:  869     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 362]---> BDD-cost:   15
c ---[ 361]---> BDD-cost:    6
c ---[ 360]---> BDD-cost:   14
c ---[ 359]---> BDD-cost:    3
c ---[ 357]---> Sorter-cost:  859     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 356]---> BDD-cost:   23
c ---[ 355]---> BDD-cost:    6
c ---[ 352]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 350]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 348]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 347]---> BDD-cost:   16
c ---[ 346]---> BDD-cost:    7
c ---[ 345]---> BDD-cost:   15
c ---[ 344]---> BDD-cost:    4
c ---[ 342]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 341]---> BDD-cost:   24
c ---[ 340]---> BDD-cost:    6
c ---[ 337]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 335]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 333]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 332]---> BDD-cost:   16
c ---[ 331]---> BDD-cost:    7
c ---[ 330]---> BDD-cost:   15
c ---[ 329]---> BDD-cost:    4
c ---[ 327]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 326]---> BDD-cost:   19
c ---[ 322]---> BDD-cost:   33
c ---[ 320]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 308]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 296]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 293]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 292]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 291]---> Sorter-cost: 1290     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 290]---> Sorter-cost: 1116     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 289]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 288]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 286]---> BDD-cost:   15
c ---[ 285]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 283]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 282]---> BDD-cost:   14
c ---[ 281]---> BDD-cost:   14
c ---[ 280]---> BDD-cost:   13
c ---[ 279]---> BDD-cost:   14
c ---[ 277]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 275]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 273]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 271]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 269]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 267]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 265]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 263]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 261]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 259]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 257]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 255]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 253]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 252]---> BDD-cost:   16
c ---[ 251]---> BDD-cost:    7
c ---[ 250]---> BDD-cost:   15
c ---[ 249]---> BDD-cost:    4
c ---[ 247]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 245]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 244]---> BDD-cost:   24
c ---[ 243]---> BDD-cost:    6
c ---[ 240]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 238]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 237]---> BDD-cost:   16
c ---[ 236]---> BDD-cost:    7
c ---[ 235]---> BDD-cost:   15
c ---[ 234]---> BDD-cost:    4
c ---[ 232]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 230]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 229]---> BDD-cost:   23
c ---[ 228]---> BDD-cost:    8
c ---[ 225]---> Sorter-cost:  915     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 223]---> Sorter-cost:  869     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 222]---> BDD-cost:   15
c ---[ 221]---> BDD-cost:    6
c ---[ 220]---> BDD-cost:   14
c ---[ 219]---> BDD-cost:    3
c ---[ 217]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 215]---> Sorter-cost:  859     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 214]---> BDD-cost:   23
c ---[ 213]---> BDD-cost:    6
c ---[ 210]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 208]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 207]---> BDD-cost:   16
c ---[ 206]---> BDD-cost:    7
c ---[ 205]---> BDD-cost:   15
c ---[ 204]---> BDD-cost:    4
c ---[ 202]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 200]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 199]---> BDD-cost:   24
c ---[ 198]---> BDD-cost:    6
c ---[ 195]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 193]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 192]---> BDD-cost:   16
c ---[ 191]---> BDD-cost:    7
c ---[ 190]---> BDD-cost:   15
c ---[ 189]---> BDD-cost:    4
c ---[ 188]---> BDD-cost:   16
c ---[ 186]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 185]---> BDD-cost:   19
c ---[ 181]---> BDD-cost:   33
c ---[ 175]---> BDD-cost:    7
c ---[ 164]---> BDD-cost:   15
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    4
c ---[ 152]---> BDD-cost:    3
c ---[ 151]---> BDD-cost:    3
c ---[ 150]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 148]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 147]---> BDD-cost:   24
c ---[ 146]---> BDD-cost:    6
c ---[ 143]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 141]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 140]---> BDD-cost:   16
c ---[ 139]---> BDD-cost:    7
c ---[ 138]---> BDD-cost:   15
c ---[ 137]---> BDD-cost:    4
c ---[ 136]---> Sorter-cost: 1290     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 133]---> BDD-cost:   23
c ---[ 132]---> BDD-cost:    8
c ---[ 129]---> Sorter-cost:  915     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 127]---> Sorter-cost:  869     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 126]---> BDD-cost:   15
c ---[ 125]---> BDD-cost:    6
c ---[ 124]---> BDD-cost:   14
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> Sorter-cost: 1116     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost:  859     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 119]---> BDD-cost:   23
c ---[ 118]---> BDD-cost:    6
c ---[ 115]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 113]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 112]---> BDD-cost:   16
c ---[ 111]---> BDD-cost:    7
c ---[ 110]---> BDD-cost:   15
c ---[ 109]---> BDD-cost:    4
c ---[ 108]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 105]---> BDD-cost:   24
c ---[ 104]---> BDD-cost:    6
c ---[ 101]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  99]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  98]---> BDD-cost:   16
c ---[  97]---> BDD-cost:    7
c ---[  96]---> BDD-cost:   15
c ---[  95]---> BDD-cost:    4
c ---[  94]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  92]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  91]---> BDD-cost:   19
c ---[  87]---> BDD-cost:   33
c ---[  70]---> BDD-cost:   15
c ---[  62]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  61]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  60]---> Sorter-cost: 1290     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  59]---> BDD-cost:   12
c ---[  58]---> BDD-cost:    5
c ---[  57]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  56]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost:  847     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  54]---> Sorter-cost:  750     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  53]---> Sorter-cost:  862     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  52]---> Sorter-cost:  821     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  51]---> Sorter-cost:  760     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  50]---> Sorter-cost:  714     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  49]---> Sorter-cost:  773     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  48]---> Sorter-cost:  686     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  47]---> Sorter-cost:  875     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  46]---> Sorter-cost:  773     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> Sorter-cost:  834     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  44]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost:  694     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  663     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  41]---> Sorter-cost:  908     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  39]---> BDD-cost:   12
c ---[  38]---> BDD-cost:    5
c ---[  37]---> Sorter-cost:  811     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  35]---> Sorter-cost:  801     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost:  821     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  33]---> Sorter-cost:  895     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost:  824     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  31]---> Sorter-cost:  798     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  29]---> Sorter-cost:  788     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  28]---> Sorter-cost:  714     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  27]---> Sorter-cost:  895     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  26]---> Sorter-cost:  788     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  25]---> Sorter-cost:  801     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  24]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  23]---> Sorter-cost:  821     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  22]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> Sorter-cost:  875     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  20]---> Sorter-cost:  811     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  19]---> BDD-cost:    5
c ---[  18]---> Sorter-cost:  727     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  17]---> BDD-cost:   12
c ---[  16]---> Sorter-cost:  630     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  15]---> Sorter-cost:  811     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  14]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  13]---> Sorter-cost:  860     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  12]---> Sorter-cost:  788     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  11]---> Sorter-cost:  704     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  10]---> Sorter-cost:  686     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   9]---> Sorter-cost:  788     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost:  650     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   7]---> Sorter-cost:  908     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   6]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[   5]---> Sorter-cost:  798     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost:  630     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   3]---> Sorter-cost:  760     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost:  660     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   1]---> Sorter-cost:  872     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost:  727     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  333790   886289 |  111263       0        0     nan |  0.000 % |
c |       100 |  333689   886069 |  122389      82      264     3.2 |  4.481 % |
c |       250 |  333597   885869 |  134628     210      689     3.3 |  4.507 % |
c |       475 |  333435   885515 |  148091     408     1295     3.2 |  4.555 % |
c |       812 |  333059   884679 |  162900     700     2234     3.2 |  4.662 % |
c |      1318 |  332410   883226 |  179190    1143     3825     3.3 |  4.838 % |
c |      2077 |  331562   881336 |  197109    1802     6121     3.4 |  5.075 % |
c |      3216 |  330950   879975 |  216820    2845     9983     3.5 |  5.238 % |
c |      4924 |  329404   876535 |  238502    4329    15698     3.6 |  5.665 % |
c |      7486 |  328443   874392 |  262352    6713    48826     7.3 |  5.924 % |
c |     11330 |  326869   870869 |  288587   10302    92482     9.0 |  6.350 % |
c |     17097 |  325584   867960 |  317446   15919   219879    13.8 |  6.707 % |
c |     25747 |  324551   865655 |  349190   24424   431973    17.7 |  6.984 % |
c |     38721 |  323989   864389 |  384110   37319   890114    23.9 |  7.138 % |
c |     58186 |  323535   863367 |  422521   56730  1652421    29.1 |  7.264 % |
c |     87378 |  322070   860086 |  464773   85698  2899355    33.8 |  7.675 % |
c |    131168 |  320907   857454 |  511250  129348  4534053    35.1 |  7.995 % |
c |    196852 |  319545   854363 |  562375  194804  7383330    37.9 |  8.366 % |
c |    295380 |  318648   852328 |  618613  293155 11490253    39.2 |  8.620 % |
c |    443173 |  317986   850831 |  680474  440861 18651400    42.3 |  8.807 % |

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/27721/stat): 27721 (minisat+_script) R 27720 27721 31027 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855143117 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/27721/statm): 174 3 169 147 0 27 0
[pid=27721] 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=27722
New process pid=27723
New process pid=27724
execve syscall for /bin/sed executable
One traced child (pid=27723) 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=27724) exited with status: 0
One traced child (pid=27722) exited with status: 0
New process pid=27725
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-dcmulti.opb

[startup+10.0043 s]
Raw data (loadavg): 0.93 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 9482 0 0 0 917 42 0 0 25 0 1 0 1855143122 40001536 9101 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27725/statm): 9766 9101 145 145 0 9621 0
[pid=27725] vsize: 39064
Current children cumulated CPU time (s) 9.59
Current children cumulated vsize (Kb) 41188

[startup+20.0052 s]
Raw data (loadavg): 0.94 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 9514 0 0 0 1916 43 0 0 25 0 1 0 1855143122 40128512 9133 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 9797 9133 145 145 0 9652 0
[pid=27725] vsize: 39188
Current children cumulated CPU time (s) 19.59
Current children cumulated vsize (Kb) 41312

[startup+30.0062 s]
Raw data (loadavg): 0.95 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 9551 0 0 0 2915 43 0 0 25 0 1 0 1855143122 40243200 9170 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27725/statm): 9825 9170 145 145 0 9680 0
[pid=27725] vsize: 39300
Current children cumulated CPU time (s) 29.58
Current children cumulated vsize (Kb) 41424

[startup+40.0071 s]
Raw data (loadavg): 0.96 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 9598 0 0 0 3914 44 0 0 25 0 1 0 1855143122 40394752 9217 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 9862 9217 145 145 0 9717 0
[pid=27725] vsize: 39448
Current children cumulated CPU time (s) 39.58
Current children cumulated vsize (Kb) 41572

[startup+50.008 s]
Raw data (loadavg): 0.96 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 9654 0 0 0 4913 45 0 0 25 0 1 0 1855143122 40611840 9273 4294967295 134512640 135094434 3221224432 3221223136 134558999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 9915 9273 145 145 0 9770 0
[pid=27725] vsize: 39660
Current children cumulated CPU time (s) 49.58
Current children cumulated vsize (Kb) 41784

[startup+60.0089 s]
Raw data (loadavg): 0.97 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 9715 0 0 0 5912 45 0 0 25 0 1 0 1855143122 40861696 9334 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 9976 9334 145 145 0 9831 0
[pid=27725] vsize: 39904
Current children cumulated CPU time (s) 59.57
Current children cumulated vsize (Kb) 42028

[startup+70.0098 s]
Raw data (loadavg): 0.97 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 9809 0 0 0 6910 46 0 0 25 0 1 0 1855143122 41234432 9428 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 10067 9428 145 145 0 9922 0
[pid=27725] vsize: 40268
Current children cumulated CPU time (s) 69.56
Current children cumulated vsize (Kb) 42392

[startup+80.0108 s]
Raw data (loadavg): 0.98 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 10031 0 0 0 7907 47 0 0 25 0 1 0 1855143122 42172416 9650 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 10296 9650 145 145 0 10151 0
[pid=27725] vsize: 41184
Current children cumulated CPU time (s) 79.54
Current children cumulated vsize (Kb) 43308

[startup+90.0117 s]
Raw data (loadavg): 0.98 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 10136 0 0 0 8906 47 0 0 25 0 1 0 1855143122 42586112 9755 4294967295 134512640 135094434 3221224432 3221223024 134557221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 10397 9755 145 145 0 10252 0
[pid=27725] vsize: 41588
Current children cumulated CPU time (s) 89.53
Current children cumulated vsize (Kb) 43712

[startup+100.013 s]
Raw data (loadavg): 0.98 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 10451 0 0 0 9901 49 0 0 25 0 1 0 1855143122 43843584 10070 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 10704 10070 145 145 0 10559 0
[pid=27725] vsize: 42816
Current children cumulated CPU time (s) 99.5
Current children cumulated vsize (Kb) 44940

[startup+110.014 s]
Raw data (loadavg): 0.98 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 10816 0 0 0 10895 52 0 0 25 0 1 0 1855143122 45441024 10435 4294967295 134512640 135094434 3221224432 3221223096 134550365 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 11094 10435 145 145 0 10949 0
[pid=27725] vsize: 44376
Current children cumulated CPU time (s) 109.47
Current children cumulated vsize (Kb) 46500

[startup+120.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 11194 0 0 0 11888 56 0 0 25 0 1 0 1855143122 46956544 10813 4294967295 134512640 135094434 3221224432 3221223112 134553433 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 11464 10813 145 145 0 11319 0
[pid=27725] vsize: 45856
Current children cumulated CPU time (s) 119.44
Current children cumulated vsize (Kb) 47980

[startup+130.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 11584 0 0 0 12882 58 0 0 25 0 1 0 1855143122 48521216 11203 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 11846 11203 145 145 0 11701 0
[pid=27725] vsize: 47384
Current children cumulated CPU time (s) 129.4
Current children cumulated vsize (Kb) 49508

[startup+140.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 11968 0 0 0 13875 61 0 0 25 0 1 0 1855143122 50069504 11587 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 12224 11587 145 145 0 12079 0
[pid=27725] vsize: 48896
Current children cumulated CPU time (s) 139.36
Current children cumulated vsize (Kb) 51020

[startup+150.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 12423 0 0 0 14868 63 0 0 25 0 1 0 1855143122 52166656 12042 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 12736 12042 145 145 0 12591 0
[pid=27725] vsize: 50944
Current children cumulated CPU time (s) 149.31
Current children cumulated vsize (Kb) 53068

[startup+160.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 12738 0 0 0 15863 65 0 0 25 0 1 0 1855143122 53432320 12357 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 13045 12357 145 145 0 12900 0
[pid=27725] vsize: 52180
Current children cumulated CPU time (s) 159.28
Current children cumulated vsize (Kb) 54304

[startup+170.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 12884 0 0 0 16861 67 0 0 25 0 1 0 1855143122 54018048 12503 4294967295 134512640 135094434 3221224432 3221223024 134557248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 13188 12503 145 145 0 13043 0
[pid=27725] vsize: 52752
Current children cumulated CPU time (s) 169.28
Current children cumulated vsize (Kb) 54876

[startup+180.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 13038 0 0 0 17859 67 0 0 25 0 1 0 1855143122 54632448 12657 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 13338 12657 145 145 0 13193 0
[pid=27725] vsize: 53352
Current children cumulated CPU time (s) 179.26
Current children cumulated vsize (Kb) 55476

[startup+190.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 13307 0 0 0 18854 69 0 0 25 0 1 0 1855143122 55717888 12926 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27725/statm): 13603 12926 145 145 0 13458 0
[pid=27725] vsize: 54412
Current children cumulated CPU time (s) 189.23
Current children cumulated vsize (Kb) 56536

[startup+200.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 13538 0 0 0 19850 70 0 0 25 0 1 0 1855143122 56643584 13157 4294967295 134512640 135094434 3221224432 3221223044 134563052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 13829 13157 145 145 0 13684 0
[pid=27725] vsize: 55316
Current children cumulated CPU time (s) 199.2
Current children cumulated vsize (Kb) 57440

[startup+210.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 13741 0 0 0 20846 71 0 0 25 0 1 0 1855143122 57458688 13360 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 14028 13360 145 145 0 13883 0
[pid=27725] vsize: 56112
Current children cumulated CPU time (s) 209.17
Current children cumulated vsize (Kb) 58236

[startup+220.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 13943 0 0 0 21843 73 0 0 25 0 1 0 1855143122 58261504 13562 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 14224 13562 145 145 0 14079 0
[pid=27725] vsize: 56896
Current children cumulated CPU time (s) 219.16
Current children cumulated vsize (Kb) 59020

[startup+230.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 14236 0 0 0 22837 74 0 0 25 0 1 0 1855143122 59437056 13855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 14511 13855 145 145 0 14366 0
[pid=27725] vsize: 58044
Current children cumulated CPU time (s) 229.11
Current children cumulated vsize (Kb) 60168

[startup+240.026 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 14644 0 0 0 23829 76 0 0 25 0 1 0 1855143122 61079552 14263 4294967295 134512640 135094434 3221224432 3221223088 134561688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 14912 14263 145 145 0 14767 0
[pid=27725] vsize: 59648
Current children cumulated CPU time (s) 239.05
Current children cumulated vsize (Kb) 61772

[startup+250.026 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 14948 0 0 0 24824 78 0 0 25 0 1 0 1855143122 62300160 14567 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 15210 14567 145 145 0 15065 0
[pid=27725] vsize: 60840
Current children cumulated CPU time (s) 249.02
Current children cumulated vsize (Kb) 62964

[startup+260.026 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 15236 0 0 0 25819 80 0 0 25 0 1 0 1855143122 63459328 14855 4294967295 134512640 135094434 3221224432 3221223024 134557407 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 15493 14855 145 145 0 15348 0
[pid=27725] vsize: 61972
Current children cumulated CPU time (s) 258.99
Current children cumulated vsize (Kb) 64096

[startup+270.027 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 15481 0 0 0 26814 82 0 0 25 0 1 0 1855143122 64446464 15100 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 15734 15100 145 145 0 15589 0
[pid=27725] vsize: 62936
Current children cumulated CPU time (s) 268.96
Current children cumulated vsize (Kb) 65060

[startup+280.027 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 15894 0 0 0 27808 84 0 0 25 0 1 0 1855143122 66633728 15513 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 16268 15513 145 145 0 16123 0
[pid=27725] vsize: 65072
Current children cumulated CPU time (s) 278.92
Current children cumulated vsize (Kb) 67196

[startup+290.028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 16402 0 0 0 28800 88 0 0 25 0 1 0 1855143122 68685824 16021 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 16769 16021 145 145 0 16624 0
[pid=27725] vsize: 67076
Current children cumulated CPU time (s) 288.88
Current children cumulated vsize (Kb) 69200

[startup+300.029 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 16724 0 0 0 29794 90 0 0 25 0 1 0 1855143122 69980160 16343 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 17085 16343 145 145 0 16940 0
[pid=27725] vsize: 68340
Current children cumulated CPU time (s) 298.84
Current children cumulated vsize (Kb) 70464

[startup+310.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 16990 0 0 0 30790 92 0 0 25 0 1 0 1855143122 71049216 16609 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 17346 16609 145 145 0 17201 0
[pid=27725] vsize: 69384
Current children cumulated CPU time (s) 308.82
Current children cumulated vsize (Kb) 71508

[startup+320.031 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 17278 0 0 0 31784 94 0 0 25 0 1 0 1855143122 72204288 16897 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 17628 16897 145 145 0 17483 0
[pid=27725] vsize: 70512
Current children cumulated CPU time (s) 318.78
Current children cumulated vsize (Kb) 72636

[startup+330.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 17465 0 0 0 32781 96 0 0 25 0 1 0 1855143122 72949760 17084 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 17810 17084 145 145 0 17665 0
[pid=27725] vsize: 71240
Current children cumulated CPU time (s) 328.77
Current children cumulated vsize (Kb) 73364

[startup+340.033 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 17691 0 0 0 33777 98 0 0 25 0 1 0 1855143122 73854976 17310 4294967295 134512640 135094434 3221224432 3221223024 134557393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 18031 17310 145 145 0 17886 0
[pid=27725] vsize: 72124
Current children cumulated CPU time (s) 338.75
Current children cumulated vsize (Kb) 74248

[startup+350.034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) T 27721 27721 31027 0 -1 0 18016 0 0 0 34773 99 0 0 25 0 1 0 1855143122 75169792 17635 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27725/statm): 18352 17635 145 145 0 18207 0
[pid=27725] vsize: 73408
Current children cumulated CPU time (s) 348.72
Current children cumulated vsize (Kb) 75532

[startup+360.036 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 18178 0 0 0 35771 100 0 0 25 0 1 0 1855143122 75821056 17797 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 18511 17797 145 145 0 18366 0
[pid=27725] vsize: 74044
Current children cumulated CPU time (s) 358.71
Current children cumulated vsize (Kb) 76168

[startup+370.037 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 18345 0 0 0 36768 102 0 0 25 0 1 0 1855143122 76492800 17964 4294967295 134512640 135094434 3221224432 3221223072 134562165 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 18675 17964 145 145 0 18530 0
[pid=27725] vsize: 74700
Current children cumulated CPU time (s) 368.7
Current children cumulated vsize (Kb) 76824

[startup+380.038 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 18749 0 0 0 37761 105 0 0 25 0 1 0 1855143122 78114816 18368 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 19071 18368 145 145 0 18926 0
[pid=27725] vsize: 76284
Current children cumulated CPU time (s) 378.66
Current children cumulated vsize (Kb) 78408

[startup+390.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 19072 0 0 0 38755 107 0 0 25 0 1 0 1855143122 79421440 18691 4294967295 134512640 135094434 3221224432 3221223088 134557818 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 19390 18691 145 145 0 19245 0
[pid=27725] vsize: 77560
Current children cumulated CPU time (s) 388.62
Current children cumulated vsize (Kb) 79684

[startup+400.039 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 19375 0 0 0 39749 110 0 0 25 0 1 0 1855143122 80642048 18994 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 19688 18994 145 145 0 19543 0
[pid=27725] vsize: 78752
Current children cumulated CPU time (s) 398.59
Current children cumulated vsize (Kb) 80876

[startup+410.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 19714 0 0 0 40743 113 0 0 25 0 1 0 1855143122 82010112 19333 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 20022 19333 145 145 0 19877 0
[pid=27725] vsize: 80088
Current children cumulated CPU time (s) 408.56
Current children cumulated vsize (Kb) 82212

[startup+420.041 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 19923 0 0 0 41741 114 0 0 25 0 1 0 1855143122 82849792 19542 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 20227 19542 145 145 0 20082 0
[pid=27725] vsize: 80908
Current children cumulated CPU time (s) 418.55
Current children cumulated vsize (Kb) 83032

[startup+430.042 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 20294 0 0 0 42734 116 0 0 25 0 1 0 1855143122 84340736 19913 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 20591 19913 145 145 0 20446 0
[pid=27725] vsize: 82364
Current children cumulated CPU time (s) 428.5
Current children cumulated vsize (Kb) 84488

[startup+440.043 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 20638 0 0 0 43728 120 0 0 25 0 1 0 1855143122 85721088 20257 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 20928 20257 145 145 0 20783 0
[pid=27725] vsize: 83712
Current children cumulated CPU time (s) 438.48
Current children cumulated vsize (Kb) 85836

[startup+450.044 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 20908 0 0 0 44724 122 0 0 25 0 1 0 1855143122 86810624 20527 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 21194 20527 145 145 0 21049 0
[pid=27725] vsize: 84776
Current children cumulated CPU time (s) 448.46
Current children cumulated vsize (Kb) 86900

[startup+460.045 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 21073 0 0 0 45722 123 0 0 25 0 1 0 1855143122 87470080 20692 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 21355 20692 145 145 0 21210 0
[pid=27725] vsize: 85420
Current children cumulated CPU time (s) 458.45
Current children cumulated vsize (Kb) 87544

[startup+470.046 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 21351 0 0 0 46717 124 0 0 25 0 1 0 1855143122 88584192 20970 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 21627 20970 145 145 0 21482 0
[pid=27725] vsize: 86508
Current children cumulated CPU time (s) 468.41
Current children cumulated vsize (Kb) 88632

[startup+480.047 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 21698 0 0 0 47711 127 0 0 25 0 1 0 1855143122 89980928 21317 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 21968 21317 145 145 0 21823 0
[pid=27725] vsize: 87872
Current children cumulated CPU time (s) 478.38
Current children cumulated vsize (Kb) 89996

[startup+490.048 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 21984 0 0 0 48706 130 0 0 25 0 1 0 1855143122 91140096 21603 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 22251 21603 145 145 0 22106 0
[pid=27725] vsize: 89004
Current children cumulated CPU time (s) 488.36
Current children cumulated vsize (Kb) 91128

[startup+500.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 22272 0 0 0 49701 133 0 0 25 0 1 0 1855143122 92291072 21891 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 22532 21891 145 145 0 22387 0
[pid=27725] vsize: 90128
Current children cumulated CPU time (s) 498.34
Current children cumulated vsize (Kb) 92252

[startup+510.052 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 22544 0 0 0 50696 135 0 0 25 0 1 0 1855143122 94437376 22163 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 23056 22163 145 145 0 22911 0
[pid=27725] vsize: 92224
Current children cumulated CPU time (s) 508.31
Current children cumulated vsize (Kb) 94348

[startup+520.053 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 22817 0 0 0 51693 136 0 0 25 0 1 0 1855143122 95535104 22436 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 23324 22436 145 145 0 23179 0
[pid=27725] vsize: 93296
Current children cumulated CPU time (s) 518.29
Current children cumulated vsize (Kb) 95420

[startup+530.053 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 22985 0 0 0 52690 137 0 0 25 0 1 0 1855143122 96223232 22604 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 23492 22604 145 145 0 23347 0
[pid=27725] vsize: 93968
Current children cumulated CPU time (s) 528.27
Current children cumulated vsize (Kb) 96092

[startup+540.054 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 23340 0 0 0 53683 140 0 0 25 0 1 0 1855143122 97652736 22959 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 23841 22959 145 145 0 23696 0
[pid=27725] vsize: 95364
Current children cumulated CPU time (s) 538.23
Current children cumulated vsize (Kb) 97488

[startup+550.054 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 23676 0 0 0 54678 142 0 0 25 0 1 0 1855143122 99028992 23295 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 24177 23295 145 145 0 24032 0
[pid=27725] vsize: 96708
Current children cumulated CPU time (s) 548.2
Current children cumulated vsize (Kb) 98832

[startup+560.055 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 23973 0 0 0 55673 145 0 0 25 0 1 0 1855143122 100229120 23592 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 24470 23592 145 145 0 24325 0
[pid=27725] vsize: 97880
Current children cumulated CPU time (s) 558.18
Current children cumulated vsize (Kb) 100004

[startup+570.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 24112 0 0 0 56670 146 0 0 25 0 1 0 1855143122 100798464 23731 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 24609 23731 145 145 0 24464 0
[pid=27725] vsize: 98436
Current children cumulated CPU time (s) 568.16
Current children cumulated vsize (Kb) 100560

[startup+580.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 24299 0 0 0 57668 148 0 0 25 0 1 0 1855143122 101548032 23918 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 24792 23918 145 145 0 24647 0
[pid=27725] vsize: 99168
Current children cumulated CPU time (s) 578.16
Current children cumulated vsize (Kb) 101292

[startup+590.058 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 24610 0 0 0 58663 150 0 0 25 0 1 0 1855143122 102801408 24229 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 25098 24229 145 145 0 24953 0
[pid=27725] vsize: 100392
Current children cumulated CPU time (s) 588.13
Current children cumulated vsize (Kb) 102516

[startup+600.059 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 24968 0 0 0 59656 152 0 0 25 0 1 0 1855143122 104247296 24587 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 25451 24587 145 145 0 25306 0
[pid=27725] vsize: 101804
Current children cumulated CPU time (s) 598.08
Current children cumulated vsize (Kb) 103928

[startup+610.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 25355 0 0 0 60648 156 0 0 25 0 1 0 1855143122 105824256 24974 4294967295 134512640 135094434 3221224432 3221223056 134557642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 25836 24974 145 145 0 25691 0
[pid=27725] vsize: 103344
Current children cumulated CPU time (s) 608.04
Current children cumulated vsize (Kb) 105468

[startup+620.061 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 25552 0 0 0 61645 157 0 0 25 0 1 0 1855143122 106622976 25171 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 26031 25171 145 145 0 25886 0
[pid=27725] vsize: 104124
Current children cumulated CPU time (s) 618.02
Current children cumulated vsize (Kb) 106248

[startup+630.062 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 25734 0 0 0 62643 157 0 0 25 0 1 0 1855143122 107352064 25353 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 26209 25353 145 145 0 26064 0
[pid=27725] vsize: 104836
Current children cumulated CPU time (s) 628
Current children cumulated vsize (Kb) 106960

[startup+640.063 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 26016 0 0 0 63638 160 0 0 25 0 1 0 1855143122 108490752 25635 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 26487 25635 145 145 0 26342 0
[pid=27725] vsize: 105948
Current children cumulated CPU time (s) 637.98
Current children cumulated vsize (Kb) 108072

[startup+650.064 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 26199 0 0 0 64635 161 0 0 25 0 1 0 1855143122 109228032 25818 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 26667 25818 145 145 0 26522 0
[pid=27725] vsize: 106668
Current children cumulated CPU time (s) 647.96
Current children cumulated vsize (Kb) 108792

[startup+660.064 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 26485 0 0 0 65630 163 0 0 25 0 1 0 1855143122 110387200 26104 4294967295 134512640 135094434 3221224432 3221223088 134558184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 26950 26104 145 145 0 26805 0
[pid=27725] vsize: 107800
Current children cumulated CPU time (s) 657.93
Current children cumulated vsize (Kb) 109924

[startup+670.065 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 26808 0 0 0 66624 165 0 0 25 0 1 0 1855143122 111693824 26427 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 27269 26427 145 145 0 27124 0
[pid=27725] vsize: 109076
Current children cumulated CPU time (s) 667.89
Current children cumulated vsize (Kb) 111200

[startup+680.066 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 27177 0 0 0 67619 167 0 0 25 0 1 0 1855143122 113147904 26796 4294967295 134512640 135094434 3221224432 3221223056 134562060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 27624 26796 145 145 0 27479 0
[pid=27725] vsize: 110496
Current children cumulated CPU time (s) 677.86
Current children cumulated vsize (Kb) 112620

[startup+690.067 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 27455 0 0 0 68615 168 0 0 25 0 1 0 1855143122 114266112 27074 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 27897 27074 145 145 0 27752 0
[pid=27725] vsize: 111588
Current children cumulated CPU time (s) 687.83
Current children cumulated vsize (Kb) 113712

[startup+700.067 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 27595 0 0 0 69613 170 0 0 25 0 1 0 1855143122 114819072 27214 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 28032 27214 145 145 0 27887 0
[pid=27725] vsize: 112128
Current children cumulated CPU time (s) 697.83
Current children cumulated vsize (Kb) 114252

[startup+710.069 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 27838 0 0 0 70608 171 0 0 22 0 1 0 1855143122 115810304 27457 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 28274 27457 145 145 0 28129 0
[pid=27725] vsize: 113096
Current children cumulated CPU time (s) 707.79
Current children cumulated vsize (Kb) 115220

[startup+720.07 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 28118 0 0 0 71604 173 0 0 25 0 1 0 1855143122 116948992 27737 4294967295 134512640 135094434 3221224432 3221223056 134557734 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 28552 27737 145 145 0 28407 0
[pid=27725] vsize: 114208
Current children cumulated CPU time (s) 717.77
Current children cumulated vsize (Kb) 116332

[startup+730.07 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 28383 0 0 0 72600 175 0 0 25 0 1 0 1855143122 118030336 28002 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 28816 28002 145 145 0 28671 0
[pid=27725] vsize: 115264
Current children cumulated CPU time (s) 727.75
Current children cumulated vsize (Kb) 117388

[startup+740.072 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 28687 0 0 0 73594 177 0 0 25 0 1 0 1855143122 119246848 28306 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 29113 28306 145 145 0 28968 0
[pid=27725] vsize: 116452
Current children cumulated CPU time (s) 737.71
Current children cumulated vsize (Kb) 118576

[startup+750.073 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 28903 0 0 0 74591 179 0 0 25 0 1 0 1855143122 120115200 28522 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 29325 28522 145 145 0 29180 0
[pid=27725] vsize: 117300
Current children cumulated CPU time (s) 747.7
Current children cumulated vsize (Kb) 119424

[startup+760.074 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 29145 0 0 0 75587 180 0 0 25 0 1 0 1855143122 121102336 28764 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 29566 28764 145 145 0 29421 0
[pid=27725] vsize: 118264
Current children cumulated CPU time (s) 757.67
Current children cumulated vsize (Kb) 120388

[startup+770.075 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 29402 0 0 0 76582 182 0 0 25 0 1 0 1855143122 122150912 29021 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 29822 29021 145 145 0 29677 0
[pid=27725] vsize: 119288
Current children cumulated CPU time (s) 767.64
Current children cumulated vsize (Kb) 121412

[startup+780.076 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 29557 0 0 0 77579 184 0 0 25 0 1 0 1855143122 122789888 29176 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 29978 29176 145 145 0 29833 0
[pid=27725] vsize: 119912
Current children cumulated CPU time (s) 777.63
Current children cumulated vsize (Kb) 122036

[startup+790.077 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 29734 0 0 0 78577 185 0 0 25 0 1 0 1855143122 123494400 29353 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 30150 29353 145 145 0 30005 0
[pid=27725] vsize: 120600
Current children cumulated CPU time (s) 787.62
Current children cumulated vsize (Kb) 122724

[startup+800.077 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 29989 0 0 0 79573 187 0 0 25 0 1 0 1855143122 124518400 29608 4294967295 134512640 135094434 3221224432 3221223056 134557642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 30400 29608 145 145 0 30255 0
[pid=27725] vsize: 121600
Current children cumulated CPU time (s) 797.6
Current children cumulated vsize (Kb) 123724

[startup+810.079 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 30244 0 0 0 80569 189 0 0 25 0 1 0 1855143122 125546496 29863 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 30651 29863 145 145 0 30506 0
[pid=27725] vsize: 122604
Current children cumulated CPU time (s) 807.58
Current children cumulated vsize (Kb) 124728

[startup+820.08 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 30490 0 0 0 81566 190 0 0 25 0 1 0 1855143122 126533632 30109 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 30892 30109 145 145 0 30747 0
[pid=27725] vsize: 123568
Current children cumulated CPU time (s) 817.56
Current children cumulated vsize (Kb) 125692

[startup+830.08 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 30737 0 0 0 82562 191 0 0 25 0 1 0 1855143122 127516672 30356 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 31132 30356 145 145 0 30987 0
[pid=27725] vsize: 124528
Current children cumulated CPU time (s) 827.53
Current children cumulated vsize (Kb) 126652

[startup+840.081 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 30853 0 0 0 83560 192 0 0 25 0 1 0 1855143122 127975424 30472 4294967295 134512640 135094434 3221224432 3221223128 134558980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 31244 30472 145 145 0 31099 0
[pid=27725] vsize: 124976
Current children cumulated CPU time (s) 837.52
Current children cumulated vsize (Kb) 127100

[startup+850.082 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 31150 0 0 0 84556 193 0 0 24 0 1 0 1855143122 129179648 30769 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 31538 30769 145 145 0 31393 0
[pid=27725] vsize: 126152
Current children cumulated CPU time (s) 847.49
Current children cumulated vsize (Kb) 128276

[startup+860.083 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 31482 0 0 0 85550 195 0 0 25 0 1 0 1855143122 130539520 31101 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 31870 31101 145 145 0 31725 0
[pid=27725] vsize: 127480
Current children cumulated CPU time (s) 857.45
Current children cumulated vsize (Kb) 129604

[startup+870.084 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 31791 0 0 0 86545 198 0 0 25 0 1 0 1855143122 131780608 31410 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 32173 31410 145 145 0 32028 0
[pid=27725] vsize: 128692
Current children cumulated CPU time (s) 867.43
Current children cumulated vsize (Kb) 130816

[startup+880.085 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 32123 0 0 0 87539 200 0 0 25 0 1 0 1855143122 133148672 31742 4294967295 134512640 135094434 3221224432 3221223024 134557404 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 32507 31742 145 145 0 32362 0
[pid=27725] vsize: 130028
Current children cumulated CPU time (s) 877.39
Current children cumulated vsize (Kb) 132152

[startup+890.086 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 32402 0 0 0 88533 203 0 0 25 0 1 0 1855143122 134295552 32021 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 32787 32021 145 145 0 32642 0
[pid=27725] vsize: 131148
Current children cumulated CPU time (s) 887.36
Current children cumulated vsize (Kb) 133272

[startup+900.087 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 32628 0 0 0 89529 205 0 0 25 0 1 0 1855143122 135204864 32247 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 33009 32247 145 145 0 32864 0
[pid=27725] vsize: 132036
Current children cumulated CPU time (s) 897.34
Current children cumulated vsize (Kb) 134160

[startup+910.089 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 32874 0 0 0 90523 207 0 0 25 0 1 0 1855143122 136200192 32493 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 33252 32493 145 145 0 33107 0
[pid=27725] vsize: 133008
Current children cumulated CPU time (s) 907.3
Current children cumulated vsize (Kb) 135132

[startup+920.09 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 32988 0 0 0 91522 209 0 0 25 0 1 0 1855143122 136679424 32607 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 33369 32607 145 145 0 33224 0
[pid=27725] vsize: 133476
Current children cumulated CPU time (s) 917.31
Current children cumulated vsize (Kb) 135600

[startup+930.091 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 33225 0 0 0 92518 210 0 0 25 0 1 0 1855143122 137629696 32844 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 33601 32844 145 145 0 33456 0
[pid=27725] vsize: 134404
Current children cumulated CPU time (s) 927.28
Current children cumulated vsize (Kb) 136528

[startup+940.091 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 33362 0 0 0 93517 211 0 0 25 0 1 0 1855143122 138215424 32981 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 33744 32981 145 145 0 33599 0
[pid=27725] vsize: 134976
Current children cumulated CPU time (s) 937.28
Current children cumulated vsize (Kb) 137100

[startup+950.092 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 33502 0 0 0 94515 212 0 0 25 0 1 0 1855143122 138788864 33121 4294967295 134512640 135094434 3221224432 3221223044 134563041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 33884 33121 145 145 0 33739 0
[pid=27725] vsize: 135536
Current children cumulated CPU time (s) 947.27
Current children cumulated vsize (Kb) 137660

[startup+960.093 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 33696 0 0 0 95512 213 0 0 25 0 1 0 1855143122 139575296 33315 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 34076 33315 145 145 0 33931 0
[pid=27725] vsize: 136304
Current children cumulated CPU time (s) 957.25
Current children cumulated vsize (Kb) 138428

[startup+970.094 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 34073 0 0 0 96507 216 0 0 25 0 1 0 1855143122 141082624 33692 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 34444 33692 145 145 0 34299 0
[pid=27725] vsize: 137776
Current children cumulated CPU time (s) 967.23
Current children cumulated vsize (Kb) 139900

[startup+980.095 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 34341 0 0 0 97503 218 0 0 25 0 1 0 1855143122 142155776 33960 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 34706 33960 145 145 0 34561 0
[pid=27725] vsize: 138824
Current children cumulated CPU time (s) 977.21
Current children cumulated vsize (Kb) 140948

[startup+990.096 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 34388 0 0 0 98502 218 0 0 25 0 1 0 1855143122 142340096 34007 4294967295 134512640 135094434 3221224432 3221223092 134553528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 34751 34007 145 145 0 34606 0
[pid=27725] vsize: 139004
Current children cumulated CPU time (s) 987.2
Current children cumulated vsize (Kb) 141128

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 34576 0 0 0 99499 220 0 0 25 0 1 0 1855143122 143097856 34195 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 34936 34195 145 145 0 34791 0
[pid=27725] vsize: 139744
Current children cumulated CPU time (s) 997.19
Current children cumulated vsize (Kb) 141868

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 34904 0 0 0 100492 222 0 0 25 0 1 0 1855143122 144424960 34523 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 35260 34523 145 145 0 35115 0
[pid=27725] vsize: 141040
Current children cumulated CPU time (s) 1007.14
Current children cumulated vsize (Kb) 143164

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 35269 0 0 0 101486 225 0 0 25 0 1 0 1855143122 145924096 34888 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 35626 34888 145 145 0 35481 0
[pid=27725] vsize: 142504
Current children cumulated CPU time (s) 1017.11
Current children cumulated vsize (Kb) 144628

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 35586 0 0 0 102481 226 0 0 25 0 1 0 1855143122 147197952 35205 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 35937 35205 145 145 0 35792 0
[pid=27725] vsize: 143748
Current children cumulated CPU time (s) 1027.07
Current children cumulated vsize (Kb) 145872

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.98 0.92 1/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) T 27721 27721 31027 0 -1 0 36084 0 0 0 103472 231 0 0 25 0 1 0 1855143122 149209088 35703 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27725/statm): 36428 35703 145 145 0 36283 0
[pid=27725] vsize: 145712
Current children cumulated CPU time (s) 1037.03
Current children cumulated vsize (Kb) 147836

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 36239 0 0 0 104469 232 0 0 25 0 1 0 1855143122 149843968 35858 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 36583 35858 145 145 0 36438 0
[pid=27725] vsize: 146332
Current children cumulated CPU time (s) 1047.01
Current children cumulated vsize (Kb) 148456

[startup+1060.11 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 36589 0 0 0 105462 235 0 0 25 0 1 0 1855143122 151261184 36208 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 36929 36208 145 145 0 36784 0
[pid=27725] vsize: 147716
Current children cumulated CPU time (s) 1056.97
Current children cumulated vsize (Kb) 149840

[startup+1070.11 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 37163 0 0 0 106452 238 0 0 25 0 1 0 1855143122 153595904 36782 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 37499 36782 145 145 0 37354 0
[pid=27725] vsize: 149996
Current children cumulated CPU time (s) 1066.9
Current children cumulated vsize (Kb) 152120

[startup+1080.11 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 37629 0 0 0 107443 242 0 0 24 0 1 0 1855143122 155484160 37248 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 37960 37248 145 145 0 37815 0
[pid=27725] vsize: 151840
Current children cumulated CPU time (s) 1076.85
Current children cumulated vsize (Kb) 153964

[startup+1090.11 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 37893 0 0 0 108440 244 0 0 25 0 1 0 1855143122 156549120 37512 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 38220 37512 145 145 0 38075 0
[pid=27725] vsize: 152880
Current children cumulated CPU time (s) 1086.84
Current children cumulated vsize (Kb) 155004

[startup+1100.11 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 38083 0 0 0 109436 245 0 0 25 0 1 0 1855143122 157298688 37702 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 38403 37702 145 145 0 38258 0
[pid=27725] vsize: 153612
Current children cumulated CPU time (s) 1096.81
Current children cumulated vsize (Kb) 155736

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 38252 0 0 0 110434 246 0 0 22 0 1 0 1855143122 157974528 37871 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 38568 37871 145 145 0 38423 0
[pid=27725] vsize: 154272
Current children cumulated CPU time (s) 1106.8
Current children cumulated vsize (Kb) 156396

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 38634 0 0 0 111428 249 0 0 25 0 1 0 1855143122 161611776 38253 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 39456 38253 145 145 0 39311 0
[pid=27725] vsize: 157824
Current children cumulated CPU time (s) 1116.77
Current children cumulated vsize (Kb) 159948

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 38890 0 0 0 112423 251 0 0 25 0 1 0 1855143122 162639872 38509 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 39707 38509 145 145 0 39562 0
[pid=27725] vsize: 158828
Current children cumulated CPU time (s) 1126.74
Current children cumulated vsize (Kb) 160952

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 39061 0 0 0 113420 252 0 0 25 0 1 0 1855143122 163323904 38680 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 39874 38680 145 145 0 39729 0
[pid=27725] vsize: 159496
Current children cumulated CPU time (s) 1136.72
Current children cumulated vsize (Kb) 161620

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 39290 0 0 0 114416 254 0 0 25 0 1 0 1855143122 164245504 38909 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 40099 38909 145 145 0 39954 0
[pid=27725] vsize: 160396
Current children cumulated CPU time (s) 1146.7
Current children cumulated vsize (Kb) 162520

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 39535 0 0 0 115412 256 0 0 25 0 1 0 1855143122 165236736 39154 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 40341 39154 145 145 0 40196 0
[pid=27725] vsize: 161364
Current children cumulated CPU time (s) 1156.68
Current children cumulated vsize (Kb) 163488

[startup+1170.12 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 39769 0 0 0 116409 258 0 0 25 0 1 0 1855143122 166187008 39388 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 40573 39388 145 145 0 40428 0
[pid=27725] vsize: 162292
Current children cumulated CPU time (s) 1166.67
Current children cumulated vsize (Kb) 164416

[startup+1180.12 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 40005 0 0 0 117405 259 0 0 25 0 1 0 1855143122 167145472 39624 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 40807 39624 145 145 0 40662 0
[pid=27725] vsize: 163228
Current children cumulated CPU time (s) 1176.64
Current children cumulated vsize (Kb) 165352

[startup+1190.12 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 40234 0 0 0 118402 261 0 0 25 0 1 0 1855143122 168079360 39853 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 41035 39853 145 145 0 40890 0
[pid=27725] vsize: 164140
Current children cumulated CPU time (s) 1186.63
Current children cumulated vsize (Kb) 166264

[startup+1200.12 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 40468 0 0 0 119399 262 0 0 25 0 1 0 1855143122 169041920 40087 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 41270 40087 145 145 0 41125 0
[pid=27725] vsize: 165080
Current children cumulated CPU time (s) 1196.61
Current children cumulated vsize (Kb) 167204

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 40692 0 0 0 120396 264 0 0 25 0 1 0 1855143122 169943040 40311 4294967295 134512640 135094434 3221224432 3221223024 134556958 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 41490 40311 145 145 0 41345 0
[pid=27725] vsize: 165960
Current children cumulated CPU time (s) 1206.6
Current children cumulated vsize (Kb) 168084



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 27725
Raw data (/proc/27721/stat): 27721 (minisat+_script) S 27720 27721 31027 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855143117 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27721/statm): 531 226 485 147 0 384 0
[pid=27721] vsize: 2124
Raw data (/proc/27725/stat): 27725 (minisat+_64-bit) R 27721 27721 31027 0 -1 0 40692 0 0 0 120396 264 0 0 25 0 1 0 1855143122 169943040 40311 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27725/statm): 41490 40311 145 145 0 41345 0
[pid=27725] vsize: 165960
Current children cumulated CPU time (s) 1206.6
Current children cumulated vsize (Kb) 168084

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

Child status: 0
Real time (s): 1210.2
CPU time (s): 1206.68
CPU user time (s): 1203.96
CPU system time (s): 2.72059
CPU usage (%): 99.7095
Max. virtual memory (cumulated for all children) (Kb): 168084

Verifier Data

ERROR: no interpretation found !