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/miplib3/normalized-mps-v2-13-7-dcmulti.opb
MD5SUM28123830d5f7e3646d18978bb347487c
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 6187

Launcher Data

LAUNCH ON wulflinc31 THE 2005-09-20 04:13:24 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3351 boxname=wulflinc31 idbench=1007 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  28123830d5f7e3646d18978bb347487c  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-dcmulti.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-dcmulti.opb
IDLAUNCH: 3351
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        921344 kB
Buffers:          7212 kB
Cached:          78444 kB
SwapCached:       1180 kB
Active:          14388 kB
Inactive:        74016 kB
HighTotal:      131008 kB
HighFree:        49644 kB
LowTotal:       903652 kB
LowFree:        871700 kB
SwapTotal:     2097892 kB
SwapFree:      2096228 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5672 kB
Slab:            19332 kB
Committed_AS:    64340 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 04:33:34 (client local time) WITH STATUS 0 IN 1206.77 SECONDS
stats: 3351 7 1206.77 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/1099/stat): 1099 (minisat+_script) R 1098 1099 9102 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855527677 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/1099/statm): 174 3 169 147 0 27 0
[pid=1099] 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=1100
New process pid=1101
New process pid=1102
execve syscall for /bin/sed executable
One traced child (pid=1101) 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=1102) exited with status: 0
One traced child (pid=1100) exited with status: 0
New process pid=1103
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-dcmulti.opb

[startup+10.0043 s]
Raw data (loadavg): 0.93 0.97 0.96 2/58 1103
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 9482 0 0 0 917 41 0 0 25 0 1 0 1855527682 40001536 9101 4294967295 134512640 135094434 3221224432 3221223128 134558980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 9766 9101 145 145 0 9621 0
[pid=1103] vsize: 39064
Current children cumulated CPU time (s) 9.59
Current children cumulated vsize (Kb) 41188

[startup+20.0053 s]
Raw data (loadavg): 0.94 0.97 0.96 2/58 1103
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 9514 0 0 0 1915 42 0 0 25 0 1 0 1855527682 40128512 9133 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1103/statm): 9797 9133 145 145 0 9652 0
[pid=1103] vsize: 39188
Current children cumulated CPU time (s) 19.58
Current children cumulated vsize (Kb) 41312

[startup+30.0062 s]
Raw data (loadavg): 0.95 0.97 0.96 2/58 1103
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 9549 0 0 0 2914 42 0 0 25 0 1 0 1855527682 40235008 9168 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 9823 9168 145 145 0 9678 0
[pid=1103] vsize: 39292
Current children cumulated CPU time (s) 29.57
Current children cumulated vsize (Kb) 41416

[startup+40.0071 s]
Raw data (loadavg): 0.96 0.97 0.96 2/58 1103
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 9592 0 0 0 3914 43 0 0 25 0 1 0 1855527682 40378368 9211 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 9858 9211 145 145 0 9713 0
[pid=1103] vsize: 39432
Current children cumulated CPU time (s) 39.58
Current children cumulated vsize (Kb) 41556

[startup+50.0081 s]
Raw data (loadavg): 0.96 0.97 0.96 2/58 1103
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 9651 0 0 0 4913 43 0 0 25 0 1 0 1855527682 40603648 9270 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 9913 9270 145 145 0 9768 0
[pid=1103] vsize: 39652
Current children cumulated CPU time (s) 49.57
Current children cumulated vsize (Kb) 41776

[startup+60.009 s]
Raw data (loadavg): 0.97 0.97 0.96 2/58 1105
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 9700 0 0 0 5913 43 0 0 25 0 1 0 1855527682 40804352 9319 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 9962 9319 145 145 0 9817 0
[pid=1103] vsize: 39848
Current children cumulated CPU time (s) 59.57
Current children cumulated vsize (Kb) 41972

[startup+70.01 s]
Raw data (loadavg): 0.97 0.97 0.96 2/58 1105
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 9745 0 0 0 6911 44 0 0 25 0 1 0 1855527682 40976384 9364 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1103/statm): 10004 9364 145 145 0 9859 0
[pid=1103] vsize: 40016
Current children cumulated CPU time (s) 69.56
Current children cumulated vsize (Kb) 42140

[startup+80.0109 s]
Raw data (loadavg): 0.98 0.97 0.96 2/58 1105
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 9998 0 0 0 7908 45 0 0 25 0 1 0 1855527682 42041344 9617 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 10264 9617 145 145 0 10119 0
[pid=1103] vsize: 41056
Current children cumulated CPU time (s) 79.54
Current children cumulated vsize (Kb) 43180

[startup+90.0118 s]
Raw data (loadavg): 0.98 0.97 0.96 2/58 1105
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 10054 0 0 0 8907 46 0 0 25 0 1 0 1855527682 42258432 9673 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 10317 9673 145 145 0 10172 0
[pid=1103] vsize: 41268
Current children cumulated CPU time (s) 89.54
Current children cumulated vsize (Kb) 43392

[startup+100.013 s]
Raw data (loadavg): 0.98 0.97 0.96 2/58 1105
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 10346 0 0 0 9902 48 0 0 25 0 1 0 1855527682 43421696 9965 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 10601 9965 145 145 0 10456 0
[pid=1103] vsize: 42404
Current children cumulated CPU time (s) 99.51
Current children cumulated vsize (Kb) 44528

[startup+110.014 s]
Raw data (loadavg): 0.98 0.97 0.96 2/58 1105
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) T 1099 1099 9102 0 -1 0 10734 0 0 0 10896 51 0 0 25 0 1 0 1855527682 45113344 10353 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/1103/statm): 11014 10353 145 145 0 10869 0
[pid=1103] vsize: 44056
Current children cumulated CPU time (s) 109.48
Current children cumulated vsize (Kb) 46180

[startup+120.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1107
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 11078 0 0 0 11890 53 0 0 25 0 1 0 1855527682 46489600 10697 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 11350 10697 145 145 0 11205 0
[pid=1103] vsize: 45400
Current children cumulated CPU time (s) 119.44
Current children cumulated vsize (Kb) 47524

[startup+130.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1107
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 11401 0 0 0 12885 55 0 0 25 0 1 0 1855527682 47783936 11020 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 11666 11020 145 145 0 11521 0
[pid=1103] vsize: 46664
Current children cumulated CPU time (s) 129.41
Current children cumulated vsize (Kb) 48788

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1107
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 11825 0 0 0 13879 58 0 0 25 0 1 0 1855527682 49491968 11444 4294967295 134512640 135094434 3221224432 3221223136 134558968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 12083 11444 145 145 0 11938 0
[pid=1103] vsize: 48332
Current children cumulated CPU time (s) 139.38
Current children cumulated vsize (Kb) 50456

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1107
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 12265 0 0 0 14872 61 0 0 25 0 1 0 1855527682 51269632 11884 4294967295 134512640 135094434 3221224432 3221223076 134562166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 12517 11884 145 145 0 12372 0
[pid=1103] vsize: 50068
Current children cumulated CPU time (s) 149.34
Current children cumulated vsize (Kb) 52192

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1107
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 12589 0 0 0 15865 63 0 0 25 0 1 0 1855527682 52834304 12208 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 12899 12208 145 145 0 12754 0
[pid=1103] vsize: 51596
Current children cumulated CPU time (s) 159.29
Current children cumulated vsize (Kb) 53720

[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1107
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 12844 0 0 0 16862 64 0 0 25 0 1 0 1855527682 53858304 12463 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 13149 12463 145 145 0 13004 0
[pid=1103] vsize: 52596
Current children cumulated CPU time (s) 169.27
Current children cumulated vsize (Kb) 54720

[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1109
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 12965 0 0 0 17860 65 0 0 25 0 1 0 1855527682 54341632 12584 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 13267 12584 145 145 0 13122 0
[pid=1103] vsize: 53068
Current children cumulated CPU time (s) 179.26
Current children cumulated vsize (Kb) 55192

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1109
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 13265 0 0 0 18854 67 0 0 25 0 1 0 1855527682 55554048 12884 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 13563 12884 145 145 0 13418 0
[pid=1103] vsize: 54252
Current children cumulated CPU time (s) 189.22
Current children cumulated vsize (Kb) 56376

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1109
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 13419 0 0 0 19852 68 0 0 25 0 1 0 1855527682 56168448 13038 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 13713 13038 145 145 0 13568 0
[pid=1103] vsize: 54852
Current children cumulated CPU time (s) 199.21
Current children cumulated vsize (Kb) 56976

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1109
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 13652 0 0 0 20848 70 0 0 25 0 1 0 1855527682 57102336 13271 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 13941 13271 145 145 0 13796 0
[pid=1103] vsize: 55764
Current children cumulated CPU time (s) 209.19
Current children cumulated vsize (Kb) 57888

[startup+220.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1109
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 13790 0 0 0 21846 72 0 0 25 0 1 0 1855527682 57651200 13409 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 14075 13409 145 145 0 13930 0
[pid=1103] vsize: 56300
Current children cumulated CPU time (s) 219.19
Current children cumulated vsize (Kb) 58424

[startup+230.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1109
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) T 1099 1099 9102 0 -1 0 14003 0 0 0 22842 73 0 0 25 0 1 0 1855527682 58499072 13622 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/1103/statm): 14282 13622 145 145 0 14137 0
[pid=1103] vsize: 57128
Current children cumulated CPU time (s) 229.16
Current children cumulated vsize (Kb) 59252

[startup+240.025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1111
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 14474 0 0 0 23834 77 0 0 25 0 1 0 1855527682 60399616 14093 4294967295 134512640 135094434 3221224432 3221223072 134558048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 14746 14093 145 145 0 14601 0
[pid=1103] vsize: 58984
Current children cumulated CPU time (s) 239.12
Current children cumulated vsize (Kb) 61108

[startup+250.026 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1111
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) T 1099 1099 9102 0 -1 0 14755 0 0 0 24830 78 0 0 25 0 1 0 1855527682 61526016 14374 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/1103/statm): 15021 14374 145 145 0 14876 0
[pid=1103] vsize: 60084
Current children cumulated CPU time (s) 249.09
Current children cumulated vsize (Kb) 62208

[startup+260.028 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1111
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 15079 0 0 0 25824 80 0 0 25 0 1 0 1855527682 62828544 14698 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 15339 14698 145 145 0 15194 0
[pid=1103] vsize: 61356
Current children cumulated CPU time (s) 259.05
Current children cumulated vsize (Kb) 63480

[startup+270.029 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1111
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 15271 0 0 0 26822 81 0 0 25 0 1 0 1855527682 63602688 14890 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 15528 14890 145 145 0 15383 0
[pid=1103] vsize: 62112
Current children cumulated CPU time (s) 269.04
Current children cumulated vsize (Kb) 64236

[startup+280.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1111
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 15618 0 0 0 27817 83 0 0 25 0 1 0 1855527682 65519616 15237 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 15996 15237 145 145 0 15851 0
[pid=1103] vsize: 63984
Current children cumulated CPU time (s) 279.01
Current children cumulated vsize (Kb) 66108

[startup+290.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1111
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 16073 0 0 0 28809 88 0 0 25 0 1 0 1855527682 67354624 15692 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 16444 15692 145 145 0 16299 0
[pid=1103] vsize: 65776
Current children cumulated CPU time (s) 288.98
Current children cumulated vsize (Kb) 67900

[startup+300.031 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1113
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 16498 0 0 0 29803 90 0 0 25 0 1 0 1855527682 69066752 16117 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 16862 16117 145 145 0 16717 0
[pid=1103] vsize: 67448
Current children cumulated CPU time (s) 298.94
Current children cumulated vsize (Kb) 69572

[startup+310.032 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1113
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 16803 0 0 0 30798 93 0 0 25 0 1 0 1855527682 70299648 16422 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 17163 16422 145 145 0 17018 0
[pid=1103] vsize: 68652
Current children cumulated CPU time (s) 308.92
Current children cumulated vsize (Kb) 70776

[startup+320.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1113
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 17096 0 0 0 31794 95 0 0 25 0 1 0 1855527682 71475200 16715 4294967295 134512640 135094434 3221224432 3221223104 134556401 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 17450 16715 145 145 0 17305 0
[pid=1103] vsize: 69800
Current children cumulated CPU time (s) 318.9
Current children cumulated vsize (Kb) 71924

[startup+330.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1113
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 17342 0 0 0 32789 97 0 0 25 0 1 0 1855527682 72458240 16961 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 17690 16961 145 145 0 17545 0
[pid=1103] vsize: 70760
Current children cumulated CPU time (s) 328.87
Current children cumulated vsize (Kb) 72884

[startup+340.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1113
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 17564 0 0 0 33785 99 0 0 25 0 1 0 1855527682 73347072 17183 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 17907 17183 145 145 0 17762 0
[pid=1103] vsize: 71628
Current children cumulated CPU time (s) 338.85
Current children cumulated vsize (Kb) 73752

[startup+350.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1113
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 17769 0 0 0 34781 101 0 0 25 0 1 0 1855527682 74170368 17388 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 18108 17388 145 145 0 17963 0
[pid=1103] vsize: 72432
Current children cumulated CPU time (s) 348.83
Current children cumulated vsize (Kb) 74556

[startup+360.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1115
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 18083 0 0 0 35775 103 0 0 25 0 1 0 1855527682 75436032 17702 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1103/statm): 18417 17702 145 145 0 18272 0
[pid=1103] vsize: 73668
Current children cumulated CPU time (s) 358.79
Current children cumulated vsize (Kb) 75792

[startup+370.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1115
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 18202 0 0 0 36774 104 0 0 25 0 1 0 1855527682 75919360 17821 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1103/statm): 18535 17821 145 145 0 18390 0
[pid=1103] vsize: 74140
Current children cumulated CPU time (s) 368.79
Current children cumulated vsize (Kb) 76264

[startup+380.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1115
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 18376 0 0 0 37770 106 0 0 25 0 1 0 1855527682 76615680 17995 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1103/statm): 18705 17995 145 145 0 18560 0
[pid=1103] vsize: 74820
Current children cumulated CPU time (s) 378.77
Current children cumulated vsize (Kb) 76944

[startup+390.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1115
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 18785 0 0 0 38763 109 0 0 25 0 1 0 1855527682 78262272 18404 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1103/statm): 19107 18404 145 145 0 18962 0
[pid=1103] vsize: 76428
Current children cumulated CPU time (s) 388.73
Current children cumulated vsize (Kb) 78552

[startup+400.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1115
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 19092 0 0 0 39758 111 0 0 25 0 1 0 1855527682 79499264 18711 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1103/statm): 19409 18711 145 145 0 19264 0
[pid=1103] vsize: 77636
Current children cumulated CPU time (s) 398.7
Current children cumulated vsize (Kb) 79760

[startup+410.045 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1115
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 19389 0 0 0 40754 114 0 0 25 0 1 0 1855527682 80699392 19008 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1103/statm): 19702 19008 145 145 0 19557 0
[pid=1103] vsize: 78808
Current children cumulated CPU time (s) 408.69
Current children cumulated vsize (Kb) 80932

[startup+420.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1117
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 19714 0 0 0 41747 117 0 0 25 0 1 0 1855527682 82010112 19333 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 20022 19333 145 145 0 19877 0
[pid=1103] vsize: 80088
Current children cumulated CPU time (s) 418.65
Current children cumulated vsize (Kb) 82212

[startup+430.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1117
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 19916 0 0 0 42743 119 0 0 25 0 1 0 1855527682 82821120 19535 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 20220 19535 145 145 0 20075 0
[pid=1103] vsize: 80880
Current children cumulated CPU time (s) 428.63
Current children cumulated vsize (Kb) 83004

[startup+440.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1117
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 20269 0 0 0 43737 122 0 0 25 0 1 0 1855527682 84242432 19888 4294967295 134512640 135094434 3221224432 3221222960 134780607 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 20567 19888 145 145 0 20422 0
[pid=1103] vsize: 82268
Current children cumulated CPU time (s) 438.6
Current children cumulated vsize (Kb) 84392

[startup+450.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1117
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 20617 0 0 0 44730 125 0 0 25 0 1 0 1855527682 85635072 20236 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 20907 20236 145 145 0 20762 0
[pid=1103] vsize: 83628
Current children cumulated CPU time (s) 448.56
Current children cumulated vsize (Kb) 85752

[startup+460.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1117
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 20907 0 0 0 45725 127 0 0 25 0 1 0 1855527682 86806528 20526 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 21193 20526 145 145 0 21048 0
[pid=1103] vsize: 84772
Current children cumulated CPU time (s) 458.53
Current children cumulated vsize (Kb) 86896

[startup+470.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1117
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 21067 0 0 0 46722 128 0 0 25 0 1 0 1855527682 87445504 20686 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 21349 20686 145 145 0 21204 0
[pid=1103] vsize: 85396
Current children cumulated CPU time (s) 468.51
Current children cumulated vsize (Kb) 87520

[startup+480.051 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1119
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 21309 0 0 0 47718 130 0 0 25 0 1 0 1855527682 88416256 20928 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 21586 20928 145 145 0 21441 0
[pid=1103] vsize: 86344
Current children cumulated CPU time (s) 478.49
Current children cumulated vsize (Kb) 88468

[startup+490.052 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1119
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 21656 0 0 0 48711 132 0 0 25 0 1 0 1855527682 89808896 21275 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 21926 21275 145 145 0 21781 0
[pid=1103] vsize: 87704
Current children cumulated CPU time (s) 488.44
Current children cumulated vsize (Kb) 89828

[startup+500.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1119
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) T 1099 1099 9102 0 -1 0 21940 0 0 0 49706 134 0 0 25 0 1 0 1855527682 90963968 21559 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/1103/statm): 22208 21559 145 145 0 22063 0
[pid=1103] vsize: 88832
Current children cumulated CPU time (s) 498.41
Current children cumulated vsize (Kb) 90956

[startup+510.055 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1119
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 22215 0 0 0 50701 136 0 0 25 0 1 0 1855527682 92061696 21834 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 22476 21834 145 145 0 22331 0
[pid=1103] vsize: 89904
Current children cumulated CPU time (s) 508.38
Current children cumulated vsize (Kb) 92028

[startup+520.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1119
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 22505 0 0 0 51696 138 0 0 25 0 1 0 1855527682 94277632 22124 4294967295 134512640 135094434 3221224432 3221223056 134557642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 23017 22124 145 145 0 22872 0
[pid=1103] vsize: 92068
Current children cumulated CPU time (s) 518.35
Current children cumulated vsize (Kb) 94192

[startup+530.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1119
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 22741 0 0 0 52693 140 0 0 25 0 1 0 1855527682 95227904 22360 4294967295 134512640 135094434 3221224432 3221223136 134558999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 23249 22360 145 145 0 23104 0
[pid=1103] vsize: 92996
Current children cumulated CPU time (s) 528.34
Current children cumulated vsize (Kb) 95120

[startup+540.057 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1121
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 22923 0 0 0 53689 142 0 0 25 0 1 0 1855527682 95973376 22542 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 23431 22542 145 145 0 23286 0
[pid=1103] vsize: 93724
Current children cumulated CPU time (s) 538.32
Current children cumulated vsize (Kb) 95848

[startup+550.058 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1121
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 23229 0 0 0 54685 144 0 0 25 0 1 0 1855527682 97206272 22848 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 23732 22848 145 145 0 23587 0
[pid=1103] vsize: 94928
Current children cumulated CPU time (s) 548.3
Current children cumulated vsize (Kb) 97052

[startup+560.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1121
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 23588 0 0 0 55678 147 0 0 25 0 1 0 1855527682 98656256 23207 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 24086 23207 145 145 0 23941 0
[pid=1103] vsize: 96344
Current children cumulated CPU time (s) 558.26
Current children cumulated vsize (Kb) 98468

[startup+570.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1121
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 23878 0 0 0 56673 149 0 0 25 0 1 0 1855527682 99844096 23497 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 24376 23497 145 145 0 24231 0
[pid=1103] vsize: 97504
Current children cumulated CPU time (s) 568.23
Current children cumulated vsize (Kb) 99628

[startup+580.061 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1121
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 24103 0 0 0 57669 151 0 0 25 0 1 0 1855527682 100757504 23722 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 24599 23722 145 145 0 24454 0
[pid=1103] vsize: 98396
Current children cumulated CPU time (s) 578.21
Current children cumulated vsize (Kb) 100520

[startup+590.062 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1121
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 24216 0 0 0 58668 152 0 0 25 0 1 0 1855527682 101216256 23835 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1103/statm): 24711 23835 145 145 0 24566 0
[pid=1103] vsize: 98844
Current children cumulated CPU time (s) 588.21
Current children cumulated vsize (Kb) 100968

[startup+600.062 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1123
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 24483 0 0 0 59662 154 0 0 25 0 1 0 1855527682 102289408 24102 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1103/statm): 24973 24102 145 145 0 24828 0
[pid=1103] vsize: 99892
Current children cumulated CPU time (s) 598.17
Current children cumulated vsize (Kb) 102016

[startup+610.064 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1123
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 24801 0 0 0 60656 157 0 0 25 0 1 0 1855527682 103575552 24420 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 25287 24420 145 145 0 25142 0
[pid=1103] vsize: 101148
Current children cumulated CPU time (s) 608.14
Current children cumulated vsize (Kb) 103272

[startup+620.065 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1123
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 25184 0 0 0 61649 160 0 0 25 0 1 0 1855527682 105127936 24803 4294967295 134512640 135094434 3221224432 3221223104 134556505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 25666 24803 145 145 0 25521 0
[pid=1103] vsize: 102664
Current children cumulated CPU time (s) 618.1
Current children cumulated vsize (Kb) 104788

[startup+630.065 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1123
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 25465 0 0 0 62644 162 0 0 25 0 1 0 1855527682 106262528 25084 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 25943 25084 145 145 0 25798 0
[pid=1103] vsize: 103772
Current children cumulated CPU time (s) 628.07
Current children cumulated vsize (Kb) 105896

[startup+640.066 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1123
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 25629 0 0 0 63641 163 0 0 25 0 1 0 1855527682 106930176 25248 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 26106 25248 145 145 0 25961 0
[pid=1103] vsize: 104424
Current children cumulated CPU time (s) 638.05
Current children cumulated vsize (Kb) 106548

[startup+650.067 s]
Raw data (loadavg): 0.99 0.97 0.96 1/58 1123
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) T 1099 1099 9102 0 -1 0 25833 0 0 0 64637 165 0 0 25 0 1 0 1855527682 107745280 25452 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/1103/statm): 26305 25452 145 145 0 26160 0
[pid=1103] vsize: 105220
Current children cumulated CPU time (s) 648.03
Current children cumulated vsize (Kb) 107344

[startup+660.069 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1125
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 26116 0 0 0 65632 168 0 0 25 0 1 0 1855527682 108896256 25735 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 26586 25735 145 145 0 26441 0
[pid=1103] vsize: 106344
Current children cumulated CPU time (s) 658.01
Current children cumulated vsize (Kb) 108468

[startup+670.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1125
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 26310 0 0 0 66628 170 0 0 25 0 1 0 1855527682 109678592 25929 4294967295 134512640 135094434 3221224432 3221223024 134557283 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 26777 25929 145 145 0 26632 0
[pid=1103] vsize: 107108
Current children cumulated CPU time (s) 667.99
Current children cumulated vsize (Kb) 109232

[startup+680.071 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1125
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 26583 0 0 0 67623 172 0 0 25 0 1 0 1855527682 110780416 26202 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 27046 26202 145 145 0 26901 0
[pid=1103] vsize: 108184
Current children cumulated CPU time (s) 677.96
Current children cumulated vsize (Kb) 110308

[startup+690.072 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1125
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 26915 0 0 0 68617 175 0 0 25 0 1 0 1855527682 112128000 26534 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 27375 26534 145 145 0 27230 0
[pid=1103] vsize: 109500
Current children cumulated CPU time (s) 687.93
Current children cumulated vsize (Kb) 111624

[startup+700.073 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1125
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 27306 0 0 0 69610 178 0 0 25 0 1 0 1855527682 113664000 26925 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 27750 26925 145 145 0 27605 0
[pid=1103] vsize: 111000
Current children cumulated CPU time (s) 697.89
Current children cumulated vsize (Kb) 113124

[startup+710.075 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1125
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 27494 0 0 0 70608 179 0 0 25 0 1 0 1855527682 114417664 27113 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 27934 27113 145 145 0 27789 0
[pid=1103] vsize: 111736
Current children cumulated CPU time (s) 707.88
Current children cumulated vsize (Kb) 113860

[startup+720.076 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1127
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 27642 0 0 0 71605 180 0 0 25 0 1 0 1855527682 115019776 27261 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 28081 27261 145 145 0 27936 0
[pid=1103] vsize: 112324
Current children cumulated CPU time (s) 717.86
Current children cumulated vsize (Kb) 114448

[startup+730.077 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1127
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 27894 0 0 0 72601 182 0 0 25 0 1 0 1855527682 116039680 27513 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 28330 27513 145 145 0 28185 0
[pid=1103] vsize: 113320
Current children cumulated CPU time (s) 727.84
Current children cumulated vsize (Kb) 115444

[startup+740.078 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1127
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 28163 0 0 0 73597 184 0 0 25 0 1 0 1855527682 117133312 27782 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1103/statm): 28597 27782 145 145 0 28452 0
[pid=1103] vsize: 114388
Current children cumulated CPU time (s) 737.82
Current children cumulated vsize (Kb) 116512

[startup+750.079 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1127
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 28421 0 0 0 74591 187 0 0 25 0 1 0 1855527682 118181888 28040 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1103/statm): 28853 28040 145 145 0 28708 0
[pid=1103] vsize: 115412
Current children cumulated CPU time (s) 747.79
Current children cumulated vsize (Kb) 117536

[startup+760.081 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1127
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 28710 0 0 0 75585 190 0 0 25 0 1 0 1855527682 119341056 28329 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1103/statm): 29136 28329 145 145 0 28991 0
[pid=1103] vsize: 116544
Current children cumulated CPU time (s) 757.76
Current children cumulated vsize (Kb) 118668

[startup+770.082 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1127
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 28913 0 0 0 76580 193 0 0 25 0 1 0 1855527682 120152064 28532 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1103/statm): 29334 28532 145 145 0 29189 0
[pid=1103] vsize: 117336
Current children cumulated CPU time (s) 767.74
Current children cumulated vsize (Kb) 119460

[startup+780.083 s]
Raw data (loadavg): 0.99 0.97 0.96 2/58 1129
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 29148 0 0 0 77575 195 0 0 25 0 1 0 1855527682 121114624 28767 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1103/statm): 29569 28767 145 145 0 29424 0
[pid=1103] vsize: 118276
Current children cumulated CPU time (s) 777.71
Current children cumulated vsize (Kb) 120400

[startup+790.084 s]
Raw data (loadavg): 1.07 0.99 0.97 2/58 1129
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 29402 0 0 0 78571 197 0 0 25 0 1 0 1855527682 122150912 29021 4294967295 134512640 135094434 3221224432 3221223044 134563115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 29822 29021 145 145 0 29677 0
[pid=1103] vsize: 119288
Current children cumulated CPU time (s) 787.69
Current children cumulated vsize (Kb) 121412

[startup+800.085 s]
Raw data (loadavg): 1.06 0.99 0.97 2/58 1129
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 29553 0 0 0 79569 198 0 0 25 0 1 0 1855527682 122773504 29172 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 29974 29172 145 145 0 29829 0
[pid=1103] vsize: 119896
Current children cumulated CPU time (s) 797.68
Current children cumulated vsize (Kb) 122020

[startup+810.087 s]
Raw data (loadavg): 1.05 0.99 0.97 2/58 1129
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 29720 0 0 0 80566 200 0 0 25 0 1 0 1855527682 123437056 29339 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 30136 29339 145 145 0 29991 0
[pid=1103] vsize: 120544
Current children cumulated CPU time (s) 807.67
Current children cumulated vsize (Kb) 122668

[startup+820.091 s]
Raw data (loadavg): 1.04 0.99 0.97 2/58 1129
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 29966 0 0 0 81562 202 0 0 25 0 1 0 1855527682 124424192 29585 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 30377 29585 145 145 0 30232 0
[pid=1103] vsize: 121508
Current children cumulated CPU time (s) 817.65
Current children cumulated vsize (Kb) 123632

[startup+830.091 s]
Raw data (loadavg): 1.04 0.99 0.97 2/58 1129
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 30212 0 0 0 82557 205 0 0 25 0 1 0 1855527682 125415424 29831 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 30619 29831 145 145 0 30474 0
[pid=1103] vsize: 122476
Current children cumulated CPU time (s) 827.63
Current children cumulated vsize (Kb) 124600

[startup+840.092 s]
Raw data (loadavg): 1.03 0.99 0.97 2/58 1131
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 30455 0 0 0 83554 206 0 0 25 0 1 0 1855527682 126390272 30074 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 30857 30074 145 145 0 30712 0
[pid=1103] vsize: 123428
Current children cumulated CPU time (s) 837.61
Current children cumulated vsize (Kb) 125552

[startup+850.093 s]
Raw data (loadavg): 1.03 0.99 0.97 2/58 1131
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 30699 0 0 0 84551 207 0 0 25 0 1 0 1855527682 127365120 30318 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 31095 30318 145 145 0 30950 0
[pid=1103] vsize: 124380
Current children cumulated CPU time (s) 847.59
Current children cumulated vsize (Kb) 126504

[startup+860.094 s]
Raw data (loadavg): 1.02 0.99 0.97 2/58 1131
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 30839 0 0 0 85548 208 0 0 25 0 1 0 1855527682 127922176 30458 4294967295 134512640 135094434 3221224432 3221223088 134558174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 31231 30458 145 145 0 31086 0
[pid=1103] vsize: 124924
Current children cumulated CPU time (s) 857.57
Current children cumulated vsize (Kb) 127048

[startup+870.095 s]
Raw data (loadavg): 1.02 0.99 0.97 2/58 1131
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 31082 0 0 0 86544 209 0 0 25 0 1 0 1855527682 128901120 30701 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 31470 30701 145 145 0 31325 0
[pid=1103] vsize: 125880
Current children cumulated CPU time (s) 867.54
Current children cumulated vsize (Kb) 128004

[startup+880.096 s]
Raw data (loadavg): 1.01 0.99 0.97 2/58 1131
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 31390 0 0 0 87538 212 0 0 25 0 1 0 1855527682 130162688 31009 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 31778 31009 145 145 0 31633 0
[pid=1103] vsize: 127112
Current children cumulated CPU time (s) 877.51
Current children cumulated vsize (Kb) 129236

[startup+890.097 s]
Raw data (loadavg): 1.01 0.99 0.97 2/58 1131
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 31704 0 0 0 88533 214 0 0 25 0 1 0 1855527682 131424256 31323 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1103/statm): 32086 31323 145 145 0 31941 0
[pid=1103] vsize: 128344
Current children cumulated CPU time (s) 887.48
Current children cumulated vsize (Kb) 130468

[startup+900.097 s]
Raw data (loadavg): 1.01 0.99 0.97 2/58 1133
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 32020 0 0 0 89526 216 0 0 25 0 1 0 1855527682 132714496 31639 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 32401 31639 145 145 0 32256 0
[pid=1103] vsize: 129604
Current children cumulated CPU time (s) 897.43
Current children cumulated vsize (Kb) 131728

[startup+910.099 s]
Raw data (loadavg): 1.01 0.99 0.97 2/58 1133
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 32329 0 0 0 90522 218 0 0 25 0 1 0 1855527682 133996544 31948 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 32714 31948 145 145 0 32569 0
[pid=1103] vsize: 130856
Current children cumulated CPU time (s) 907.41
Current children cumulated vsize (Kb) 132980

[startup+920.1 s]
Raw data (loadavg): 1.01 0.99 0.97 2/58 1133
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 32539 0 0 0 91519 219 0 0 25 0 1 0 1855527682 134848512 32158 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 32922 32158 145 145 0 32777 0
[pid=1103] vsize: 131688
Current children cumulated CPU time (s) 917.39
Current children cumulated vsize (Kb) 133812

[startup+930.101 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1133
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 32761 0 0 0 92515 221 0 0 25 0 1 0 1855527682 135745536 32380 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 33141 32380 145 145 0 32996 0
[pid=1103] vsize: 132564
Current children cumulated CPU time (s) 927.37
Current children cumulated vsize (Kb) 134688

[startup+940.102 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1133
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 32962 0 0 0 93512 223 0 0 25 0 1 0 1855527682 136556544 32581 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 33339 32581 145 145 0 33194 0
[pid=1103] vsize: 133356
Current children cumulated CPU time (s) 937.36
Current children cumulated vsize (Kb) 135480

[startup+950.103 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1133
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 33128 0 0 0 94509 224 0 0 25 0 1 0 1855527682 137244672 32747 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1103/statm): 33507 32747 145 145 0 33362 0
[pid=1103] vsize: 134028
Current children cumulated CPU time (s) 947.34
Current children cumulated vsize (Kb) 136152

[startup+960.104 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1135
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 33271 0 0 0 95506 226 0 0 25 0 1 0 1855527682 137822208 32890 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 33648 32890 145 145 0 33503 0
[pid=1103] vsize: 134592
Current children cumulated CPU time (s) 957.33
Current children cumulated vsize (Kb) 136716

[startup+970.105 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1135
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 33431 0 0 0 96503 228 0 0 25 0 1 0 1855527682 138498048 33050 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 33813 33050 145 145 0 33668 0
[pid=1103] vsize: 135252
Current children cumulated CPU time (s) 967.32
Current children cumulated vsize (Kb) 137376

[startup+980.105 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1135
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 33542 0 0 0 97500 229 0 0 25 0 1 0 1855527682 138948608 33161 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 33923 33161 145 145 0 33778 0
[pid=1103] vsize: 135692
Current children cumulated CPU time (s) 977.3
Current children cumulated vsize (Kb) 137816

[startup+990.107 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1135
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 33892 0 0 0 98495 232 0 0 25 0 1 0 1855527682 140357632 33511 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 34267 33511 145 145 0 34122 0
[pid=1103] vsize: 137068
Current children cumulated CPU time (s) 987.28
Current children cumulated vsize (Kb) 139192

[startup+1000.11 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1135
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 34140 0 0 0 99491 235 0 0 25 0 1 0 1855527682 141348864 33759 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 34509 33759 145 145 0 34364 0
[pid=1103] vsize: 138036
Current children cumulated CPU time (s) 997.27
Current children cumulated vsize (Kb) 140160

[startup+1010.11 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1135
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 34349 0 0 0 100488 236 0 0 25 0 1 0 1855527682 142188544 33968 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 34714 33968 145 145 0 34569 0
[pid=1103] vsize: 138856
Current children cumulated CPU time (s) 1007.25
Current children cumulated vsize (Kb) 140980

[startup+1020.11 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1137
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 34443 0 0 0 101486 237 0 0 25 0 1 0 1855527682 142561280 34062 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 34805 34062 145 145 0 34660 0
[pid=1103] vsize: 139220
Current children cumulated CPU time (s) 1017.24
Current children cumulated vsize (Kb) 141344

[startup+1030.11 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1137
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 34648 0 0 0 102484 238 0 0 25 0 1 0 1855527682 143388672 34267 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 35007 34267 145 145 0 34862 0
[pid=1103] vsize: 140028
Current children cumulated CPU time (s) 1027.23
Current children cumulated vsize (Kb) 142152

[startup+1040.11 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1137
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 35034 0 0 0 103479 240 0 0 25 0 1 0 1855527682 144961536 34653 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 35391 34653 145 145 0 35246 0
[pid=1103] vsize: 141564
Current children cumulated CPU time (s) 1037.2
Current children cumulated vsize (Kb) 143688

[startup+1050.11 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1137
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 35370 0 0 0 104472 242 0 0 25 0 1 0 1855527682 146329600 34989 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 35725 34989 145 145 0 35580 0
[pid=1103] vsize: 142900
Current children cumulated CPU time (s) 1047.15
Current children cumulated vsize (Kb) 145024

[startup+1060.11 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1137
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 35718 0 0 0 105467 244 0 0 25 0 1 0 1855527682 147730432 35337 4294967295 134512640 135094434 3221224432 3221223056 134557722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 36067 35337 145 145 0 35922 0
[pid=1103] vsize: 144268
Current children cumulated CPU time (s) 1057.12
Current children cumulated vsize (Kb) 146392

[startup+1070.11 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1137
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 36122 0 0 0 106461 247 0 0 25 0 1 0 1855527682 149364736 35741 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 36466 35741 145 145 0 36321 0
[pid=1103] vsize: 145864
Current children cumulated CPU time (s) 1067.09
Current children cumulated vsize (Kb) 147988

[startup+1080.12 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1139
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 36279 0 0 0 107458 249 0 0 25 0 1 0 1855527682 150007808 35898 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 36623 35898 145 145 0 36478 0
[pid=1103] vsize: 146492
Current children cumulated CPU time (s) 1077.08
Current children cumulated vsize (Kb) 148616

[startup+1090.12 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1139
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 36711 0 0 0 108450 252 0 0 25 0 1 0 1855527682 151756800 36330 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1103/statm): 37050 36330 145 145 0 36905 0
[pid=1103] vsize: 148200
Current children cumulated CPU time (s) 1087.03
Current children cumulated vsize (Kb) 150324

[startup+1100.12 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1139
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 37257 0 0 0 109440 257 0 0 25 0 1 0 1855527682 153976832 36876 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 37592 36876 145 145 0 37447 0
[pid=1103] vsize: 150368
Current children cumulated CPU time (s) 1096.98
Current children cumulated vsize (Kb) 152492

[startup+1110.12 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1139
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 37705 0 0 0 110433 260 0 0 25 0 1 0 1855527682 155791360 37324 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 38035 37324 145 145 0 37890 0
[pid=1103] vsize: 152140
Current children cumulated CPU time (s) 1106.94
Current children cumulated vsize (Kb) 154264

[startup+1120.12 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1139
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 37919 0 0 0 111429 262 0 0 25 0 1 0 1855527682 156651520 37538 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 38245 37538 145 145 0 38100 0
[pid=1103] vsize: 152980
Current children cumulated CPU time (s) 1116.92
Current children cumulated vsize (Kb) 155104

[startup+1130.12 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1139
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 38099 0 0 0 112427 262 0 0 25 0 1 0 1855527682 157368320 37718 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 38420 37718 145 145 0 38275 0
[pid=1103] vsize: 153680
Current children cumulated CPU time (s) 1126.9
Current children cumulated vsize (Kb) 155804

[startup+1140.12 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1141
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 38271 0 0 0 113424 264 0 0 25 0 1 0 1855527682 158052352 37890 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 38587 37890 145 145 0 38442 0
[pid=1103] vsize: 154348
Current children cumulated CPU time (s) 1136.89
Current children cumulated vsize (Kb) 156472

[startup+1150.12 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1141
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 38648 0 0 0 114416 267 0 0 25 0 1 0 1855527682 161669120 38267 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 39470 38267 145 145 0 39325 0
[pid=1103] vsize: 157880
Current children cumulated CPU time (s) 1146.84
Current children cumulated vsize (Kb) 160004

[startup+1160.12 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1141
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 38890 0 0 0 115411 269 0 0 25 0 1 0 1855527682 162639872 38509 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1103/statm): 39707 38509 145 145 0 39562 0
[pid=1103] vsize: 158828
Current children cumulated CPU time (s) 1156.81
Current children cumulated vsize (Kb) 160952

[startup+1170.12 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1141
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 39054 0 0 0 116408 270 0 0 25 0 1 0 1855527682 163295232 38673 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 39867 38673 145 145 0 39722 0
[pid=1103] vsize: 159468
Current children cumulated CPU time (s) 1166.79
Current children cumulated vsize (Kb) 161592

[startup+1180.13 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1141
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 39277 0 0 0 117403 272 0 0 25 0 1 0 1855527682 164192256 38896 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 40086 38896 145 145 0 39941 0
[pid=1103] vsize: 160344
Current children cumulated CPU time (s) 1176.76
Current children cumulated vsize (Kb) 162468

[startup+1190.13 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1141
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 39516 0 0 0 118399 274 0 0 25 0 1 0 1855527682 165158912 39135 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 40322 39135 145 145 0 40177 0
[pid=1103] vsize: 161288
Current children cumulated CPU time (s) 1186.74
Current children cumulated vsize (Kb) 163412

[startup+1200.13 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1143
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 39744 0 0 0 119395 276 0 0 25 0 1 0 1855527682 166084608 39363 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 40548 39363 145 145 0 40403 0
[pid=1103] vsize: 162192
Current children cumulated CPU time (s) 1196.72
Current children cumulated vsize (Kb) 164316

[startup+1210.13 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1143
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 39972 0 0 0 120391 277 0 0 25 0 1 0 1855527682 167010304 39591 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 40774 39591 145 145 0 40629 0
[pid=1103] vsize: 163096
Current children cumulated CPU time (s) 1206.69
Current children cumulated vsize (Kb) 165220



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.13 s]
Raw data (loadavg): 1.00 0.99 0.97 2/58 1143
Raw data (/proc/1099/stat): 1099 (minisat+_script) S 1098 1099 9102 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855527677 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1099/statm): 531 226 485 147 0 384 0
[pid=1099] vsize: 2124
Raw data (/proc/1103/stat): 1103 (minisat+_64-bit) R 1099 1099 9102 0 -1 0 39972 0 0 0 120391 277 0 0 25 0 1 0 1855527682 167010304 39591 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1103/statm): 40774 39591 145 145 0 40629 0
[pid=1103] vsize: 163096
Current children cumulated CPU time (s) 1206.69
Current children cumulated vsize (Kb) 165220

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

Child status: 0
Real time (s): 1210.21
CPU time (s): 1206.77
CPU user time (s): 1203.92
CPU system time (s): 2.84657
CPU usage (%): 99.7157
Max. virtual memory (cumulated for all children) (Kb): 165220

Verifier Data

ERROR: no interpretation found !