Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-dcmulti.opb
MD5SUM2c1654041c7ed087aa8883df6d85cbf7
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 14235
Biggest coefficient in the objective function 714038312960
Number of bits for the biggest coefficient in the objective function 40
Sum of the numbers in the objective function 68224730472397
Number of bits of the sum of numbers in the objective function 46
Biggest number in a constraint 714038312960
Number of bits of the biggest number in a constraint 40
Biggest sum of numbers in a constraint 68224730472397
Number of bits of the biggest sum of numbers46
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables14265
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 constraint420

Trace number 3850

Launcher Data

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        835460 kB
Buffers:         40256 kB
Cached:         128428 kB
SwapCached:        908 kB
Active:         105820 kB
Inactive:        65700 kB
HighTotal:      131008 kB
HighFree:         9800 kB
LowTotal:       903652 kB
LowFree:        825660 kB
SwapTotal:     2097136 kB
SwapFree:      2095620 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5992 kB
Slab:            21948 kB
Committed_AS:    93168 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 03:25:44 (client local time) WITH STATUS 0 IN 1207.43 SECONDS
stats: 2850 7 1207.43 0

Solver Data

c Parsing PB file...
c Converting 368 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################################################################
c   -- Clauses(.)/Splits(s): s....s.....sssssssssssssssssss....s.....ssssssssssssssssss....s.....sssssssssssssssssss
c ---[ 427]---> BDD-cost:   17
c ---[ 426]---> Sorter-cost: 1377     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 425]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 424]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 422]---> BDD-cost:   18
c ---[ 421]---> BDD-cost:   17
c ---[ 420]---> BDD-cost:   17
c ---[ 419]---> BDD-cost:   16
c ---[ 418]---> BDD-cost:   17
c ---[ 416]---> Adder-cost: 523   maxlim: 2097148   bits: 22/21
c ---[ 415]---> BDD-cost:   17
c ---[ 413]---> Adder-cost: 523   maxlim: 1703932   bits: 22/21
c ---[ 411]---> Adder-cost: 523   maxlim: 2097148   bits: 22/21
c ---[ 409]---> Adder-cost: 523   maxlim: 1703932   bits: 22/21
c ---[ 407]---> Adder-cost: 523   maxlim: 2097148   bits: 22/21
c ---[ 405]---> Adder-cost: 523   maxlim: 1703932   bits: 22/21
c ---[ 403]---> Adder-cost: 523   maxlim: 2097148   bits: 22/21
c ---[ 401]---> Adder-cost: 523   maxlim: 1703932   bits: 22/21
c ---[ 399]---> Adder-cost: 523   maxlim: 2097148   bits: 22/21
c ---[ 397]---> Adder-cost: 523   maxlim: 1703932   bits: 22/21
c ---[ 395]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 394]---> BDD-cost:   16
c ---[ 392]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 391]---> BDD-cost:   19
c ---[ 390]---> BDD-cost:    7
c ---[ 389]---> BDD-cost:   18
c ---[ 388]---> BDD-cost:    4
c ---[ 386]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 385]---> BDD-cost:   27
c ---[ 384]---> BDD-cost:    6
c ---[ 381]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 380]---> BDD-cost:   17
c ---[ 378]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 377]---> BDD-cost:   19
c ---[ 376]---> BDD-cost:    7
c ---[ 375]---> BDD-cost:   18
c ---[ 374]---> BDD-cost:    4
c ---[ 372]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 371]---> BDD-cost:   26
c ---[ 370]---> BDD-cost:    8
c ---[ 367]---> Sorter-cost: 1113     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 365]---> Adder-cost: 463   maxlim: 1048573   bits: 21/20
c ---[ 363]---> Sorter-cost: 1067     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 362]---> BDD-cost:   18
c ---[ 361]---> BDD-cost:    6
c ---[ 360]---> BDD-cost:   17
c ---[ 359]---> BDD-cost:    3
c ---[ 357]---> Sorter-cost: 1054     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 356]---> BDD-cost:   26
c ---[ 355]---> BDD-cost:    6
c ---[ 352]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 350]---> Adder-cost: 463   maxlim: 655357   bits: 21/20
c ---[ 348]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 347]---> BDD-cost:   19
c ---[ 346]---> BDD-cost:    7
c ---[ 345]---> BDD-cost:   18
c ---[ 344]---> BDD-cost:    4
c ---[ 342]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 341]---> BDD-cost:   27
c ---[ 340]---> BDD-cost:    6
c ---[ 337]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 335]---> Adder-cost: 463   maxlim: 1048573   bits: 21/20
c ---[ 333]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 332]---> BDD-cost:   19
c ---[ 331]---> BDD-cost:    7
c ---[ 330]---> BDD-cost:   18
c ---[ 329]---> BDD-cost:    4
c ---[ 327]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 326]---> BDD-cost:   22
c ---[ 322]---> BDD-cost:   33
c ---[ 320]---> Adder-cost: 463   maxlim: 655357   bits: 21/20
c ---[ 308]---> Adder-cost: 463   maxlim: 1048573   bits: 21/20
c ---[ 296]---> Adder-cost: 463   maxlim: 655357   bits: 21/20
c ---[ 293]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 292]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 291]---> Sorter-cost: 1551     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 290]---> Sorter-cost: 1377     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 289]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 288]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 286]---> BDD-cost:   18
c ---[ 285]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 283]---> Adder-cost: 463   maxlim: 1048573   bits: 21/20
c ---[ 282]---> BDD-cost:   17
c ---[ 281]---> BDD-cost:   17
c ---[ 280]---> BDD-cost:   16
c ---[ 279]---> BDD-cost:   17
c ---[ 277]---> Adder-cost: 500   maxlim: 3145724   bits: 23/22
c ---[ 275]---> Adder-cost: 500   maxlim: 2752508   bits: 23/22
c ---[ 273]---> Adder-cost: 500   maxlim: 3145724   bits: 23/22
c ---[ 271]---> Adder-cost: 500   maxlim: 2752508   bits: 23/22
c ---[ 269]---> Adder-cost: 500   maxlim: 3145724   bits: 23/22
c ---[ 267]---> Adder-cost: 500   maxlim: 2752508   bits: 23/22
c ---[ 265]---> Adder-cost: 463   maxlim: 655357   bits: 21/20
c ---[ 263]---> Adder-cost: 500   maxlim: 3145724   bits: 23/22
c ---[ 261]---> Adder-cost: 500   maxlim: 2752508   bits: 23/22
c ---[ 259]---> Adder-cost: 500   maxlim: 3145724   bits: 23/22
c ---[ 257]---> Adder-cost: 500   maxlim: 2752508   bits: 23/22
c ---[ 255]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 253]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 252]---> BDD-cost:   19
c ---[ 251]---> BDD-cost:    7
c ---[ 250]---> BDD-cost:   18
c ---[ 249]---> BDD-cost:    4
c ---[ 247]---> Adder-cost: 463   maxlim: 1048573   bits: 21/20
c ---[ 245]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 244]---> BDD-cost:   27
c ---[ 243]---> BDD-cost:    6
c ---[ 240]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 238]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 237]---> BDD-cost:   19
c ---[ 236]---> BDD-cost:    7
c ---[ 235]---> BDD-cost:   18
c ---[ 234]---> BDD-cost:    4
c ---[ 232]---> Adder-cost: 463   maxlim: 655357   bits: 21/20
c ---[ 230]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 229]---> BDD-cost:   26
c ---[ 228]---> BDD-cost:    8
c ---[ 225]---> Sorter-cost: 1113     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 223]---> Sorter-cost: 1067     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 222]---> BDD-cost:   18
c ---[ 221]---> BDD-cost:    6
c ---[ 220]---> BDD-cost:   17
c ---[ 219]---> BDD-cost:    3
c ---[ 217]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 215]---> Sorter-cost: 1054     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 214]---> BDD-cost:   26
c ---[ 213]---> BDD-cost:    6
c ---[ 210]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 208]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 207]---> BDD-cost:   19
c ---[ 206]---> BDD-cost:    7
c ---[ 205]---> BDD-cost:   18
c ---[ 204]---> BDD-cost:    4
c ---[ 202]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 200]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 199]---> BDD-cost:   27
c ---[ 198]---> BDD-cost:    6
c ---[ 195]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 193]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 192]---> BDD-cost:   19
c ---[ 191]---> BDD-cost:    7
c ---[ 190]---> BDD-cost:   18
c ---[ 189]---> BDD-cost:    4
c ---[ 188]---> BDD-cost:   19
c ---[ 186]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 185]---> BDD-cost:   22
c ---[ 181]---> BDD-cost:   33
c ---[ 175]---> BDD-cost:    7
c ---[ 164]---> BDD-cost:   18
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: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 148]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 147]---> BDD-cost:   27
c ---[ 146]---> BDD-cost:    6
c ---[ 143]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 141]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 140]---> BDD-cost:   19
c ---[ 139]---> BDD-cost:    7
c ---[ 138]---> BDD-cost:   18
c ---[ 137]---> BDD-cost:    4
c ---[ 136]---> Sorter-cost: 1551     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 133]---> BDD-cost:   26
c ---[ 132]---> BDD-cost:    8
c ---[ 129]---> Sorter-cost: 1113     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 127]---> Sorter-cost: 1067     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 126]---> BDD-cost:   18
c ---[ 125]---> BDD-cost:    6
c ---[ 124]---> BDD-cost:   17
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> Sorter-cost: 1377     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost: 1054     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 119]---> BDD-cost:   26
c ---[ 118]---> BDD-cost:    6
c ---[ 115]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 113]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 112]---> BDD-cost:   19
c ---[ 111]---> BDD-cost:    7
c ---[ 110]---> BDD-cost:   18
c ---[ 109]---> BDD-cost:    4
c ---[ 108]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 105]---> BDD-cost:   27
c ---[ 104]---> BDD-cost:    6
c ---[ 101]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  99]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  98]---> BDD-cost:   19
c ---[  97]---> BDD-cost:    7
c ---[  96]---> BDD-cost:   18
c ---[  95]---> BDD-cost:    4
c ---[  94]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  92]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  91]---> BDD-cost:   22
c ---[  87]---> BDD-cost:   33
c ---[  70]---> BDD-cost:   18
c ---[  62]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  61]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  60]---> Sorter-cost: 1551     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  59]---> BDD-cost:   15
c ---[  58]---> BDD-cost:    5
c ---[  57]---> Sorter-cost: 1000     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  56]---> Sorter-cost:  939     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost: 1039     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  54]---> Sorter-cost:  942     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  53]---> Sorter-cost: 1054     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  52]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  51]---> Sorter-cost:  952     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  50]---> Sorter-cost:  906     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  49]---> Sorter-cost:  965     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  48]---> Sorter-cost:  878     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  47]---> Sorter-cost: 1067     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  46]---> Sorter-cost:  965     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> Sorter-cost: 1026     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  44]---> Sorter-cost:  939     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost:  886     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  855     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  41]---> Sorter-cost: 1100     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost: 1000     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:    5
c ---[  37]---> Sorter-cost: 1003     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost:  929     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  35]---> Sorter-cost:  993     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  33]---> Sorter-cost: 1087     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost: 1016     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  31]---> Sorter-cost:  990     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> Sorter-cost:  939     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  29]---> Sorter-cost:  980     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  28]---> Sorter-cost:  906     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  27]---> Sorter-cost: 1087     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  26]---> Sorter-cost:  980     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  25]---> Sorter-cost:  993     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  24]---> Sorter-cost:  929     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  23]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  22]---> Sorter-cost:  939     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> Sorter-cost: 1067     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  20]---> Sorter-cost: 1003     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  19]---> BDD-cost:    5
c ---[  18]---> Sorter-cost:  919     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  17]---> BDD-cost:   15
c ---[  16]---> Sorter-cost:  822     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  15]---> Sorter-cost: 1003     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  14]---> Sorter-cost:  939     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  13]---> Sorter-cost: 1052     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  12]---> Sorter-cost:  980     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  11]---> Sorter-cost:  896     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  10]---> Sorter-cost:  878     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   9]---> Sorter-cost:  980     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost:  842     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   7]---> Sorter-cost: 1100     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   6]---> Sorter-cost:  929     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   5]---> Sorter-cost:  990     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost:  822     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   3]---> Sorter-cost:  952     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost:  852     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   1]---> Sorter-cost: 1064     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost:  919     Base: 2 2 2 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 |  407659  1078157 |  135886       0        0     nan |  0.000 % |
c |       100 |  407640  1078115 |  149474      99      275     2.8 |  6.241 % |
c |       250 |  407421  1077629 |  164422     214      597     2.8 |  6.288 % |
c |       476 |  407230  1077203 |  180864     417     1295     3.1 |  6.331 % |
c |       814 |  407010  1076714 |  198950     728     2340     3.2 |  6.410 % |
c |      1320 |  406574  1075744 |  218845    1162     3846     3.3 |  6.475 % |
c |      2079 |  405501  1073358 |  240730    1770     6153     3.5 |  6.717 % |
c |      3218 |  404456  1071032 |  264803    2786     9745     3.5 |  6.951 % |
c |      4926 |  403134  1068083 |  291283    4259    14929     3.5 |  7.237 % |
c |      7488 |  401682  1064841 |  320412    6633    24359     3.7 |  7.552 % |
c |     11333 |  400157  1061429 |  352453   10286    45629     4.4 |  7.886 % |
c |     17104 |  399646  1060290 |  387698   15961   163733    10.3 |  7.996 % |
c |     25753 |  399275  1059467 |  426468   24558   453474    18.5 |  8.080 % |
c |     38730 |  398228  1057131 |  469115   37369   866938    23.2 |  8.307 % |
c |     58192 |  397042  1054454 |  516026   56692  1511359    26.7 |  8.577 % |
c |     87384 |  396904  1054146 |  567629   85866  2730385    31.8 |  8.607 % |
c |    131173 |  396253  1052687 |  624392  129572  4392719    33.9 |  8.750 % |
c |    196857 |  395205  1050318 |  686831  195116  7086771    36.3 |  8.981 % |
c |    295385 |  393580  1046653 |  755514  293406 11407186    38.9 |  9.345 % |

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/7644/stat): 7644 (minisat+_script) R 7643 7644 17733 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1731436297 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/7644/statm): 174 3 169 147 0 27 0
[pid=7644] 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=7645
New process pid=7646
New process pid=7647
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
One traced child (pid=7646) exited with status: 0
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=7647) exited with status: 0
One traced child (pid=7645) exited with status: 0
New process pid=7648
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-dcmulti.opb

[startup+10.0034 s]
Raw data (loadavg): 0.54 0.76 0.90 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 11554 0 0 0 902 41 0 0 25 0 1 0 1731436302 56516608 11160 4294967295 134512640 135094434 3221224432 3221223116 134553526 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7648/statm): 13798 11160 145 145 0 13653 0
[pid=7648] vsize: 55192
Current children cumulated CPU time (s) 9.44
Current children cumulated vsize (Kb) 57316

[startup+20.0051 s]
Raw data (loadavg): 0.61 0.77 0.90 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 11595 0 0 0 1902 42 0 0 25 0 1 0 1731436302 56672256 11201 4294967295 134512640 135094434 3221224432 3221223104 134553523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 13836 11201 145 145 0 13691 0
[pid=7648] vsize: 55344
Current children cumulated CPU time (s) 19.45
Current children cumulated vsize (Kb) 57468

[startup+30.0059 s]
Raw data (loadavg): 0.67 0.77 0.90 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 11615 0 0 0 2901 42 0 0 25 0 1 0 1731436302 56741888 11221 4294967295 134512640 135094434 3221224432 3221223092 134553444 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7648/statm): 13853 11221 145 145 0 13708 0
[pid=7648] vsize: 55412
Current children cumulated CPU time (s) 29.44
Current children cumulated vsize (Kb) 57536

[startup+40.0067 s]
Raw data (loadavg): 0.72 0.78 0.90 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 11650 0 0 0 3894 42 0 0 25 0 1 0 1731436302 56827904 11256 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7648/statm): 13874 11256 145 145 0 13729 0
[pid=7648] vsize: 55496
Current children cumulated CPU time (s) 39.37
Current children cumulated vsize (Kb) 57620

[startup+50.0075 s]
Raw data (loadavg): 0.76 0.79 0.90 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 11690 0 0 0 4894 42 0 0 25 0 1 0 1731436302 56975360 11296 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7648/statm): 13910 11296 145 145 0 13765 0
[pid=7648] vsize: 55640
Current children cumulated CPU time (s) 49.37
Current children cumulated vsize (Kb) 57764

[startup+60.0083 s]
Raw data (loadavg): 0.80 0.79 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 11718 0 0 0 5894 43 0 0 25 0 1 0 1731436302 57065472 11324 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7648/statm): 13932 11324 145 145 0 13787 0
[pid=7648] vsize: 55728
Current children cumulated CPU time (s) 59.38
Current children cumulated vsize (Kb) 57852

[startup+70.0101 s]
Raw data (loadavg): 0.83 0.80 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 11736 0 0 0 6893 43 0 0 25 0 1 0 1731436302 57135104 11342 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7648/statm): 13949 11342 145 145 0 13804 0
[pid=7648] vsize: 55796
Current children cumulated CPU time (s) 69.37
Current children cumulated vsize (Kb) 57920

[startup+80.0109 s]
Raw data (loadavg): 0.85 0.81 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 11770 0 0 0 7892 44 0 0 25 0 1 0 1731436302 57266176 11376 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7648/statm): 13981 11376 145 145 0 13836 0
[pid=7648] vsize: 55924
Current children cumulated CPU time (s) 79.37
Current children cumulated vsize (Kb) 58048

[startup+90.0117 s]
Raw data (loadavg): 0.88 0.81 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 11791 0 0 0 8891 45 0 0 25 0 1 0 1731436302 57344000 11397 4294967295 134512640 135094434 3221224432 3221223092 134553450 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7648/statm): 14000 11397 145 145 0 13855 0
[pid=7648] vsize: 56000
Current children cumulated CPU time (s) 89.37
Current children cumulated vsize (Kb) 58124

[startup+100.012 s]
Raw data (loadavg): 0.89 0.82 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 11908 0 0 0 9889 46 0 0 25 0 1 0 1731436302 57806848 11514 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7648/statm): 14113 11514 145 145 0 13968 0
[pid=7648] vsize: 56452
Current children cumulated CPU time (s) 99.36
Current children cumulated vsize (Kb) 58576

[startup+110.014 s]
Raw data (loadavg): 0.91 0.82 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 12214 0 0 0 10885 48 0 0 25 0 1 0 1731436302 59092992 11820 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 14427 11820 145 145 0 14282 0
[pid=7648] vsize: 57708
Current children cumulated CPU time (s) 109.34
Current children cumulated vsize (Kb) 59832

[startup+120.015 s]
Raw data (loadavg): 0.92 0.83 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 12437 0 0 0 11881 50 0 0 25 0 1 0 1731436302 59985920 12043 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 14645 12043 145 145 0 14500 0
[pid=7648] vsize: 58580
Current children cumulated CPU time (s) 119.32
Current children cumulated vsize (Kb) 60704

[startup+130.016 s]
Raw data (loadavg): 0.93 0.83 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 12765 0 0 0 12876 52 0 0 25 0 1 0 1731436302 61431808 12371 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 14998 12371 145 145 0 14853 0
[pid=7648] vsize: 59992
Current children cumulated CPU time (s) 129.29
Current children cumulated vsize (Kb) 62116

[startup+140.017 s]
Raw data (loadavg): 0.94 0.84 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 13051 0 0 0 13870 55 0 0 25 0 1 0 1731436302 62578688 12657 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 15278 12657 145 145 0 15133 0
[pid=7648] vsize: 61112
Current children cumulated CPU time (s) 139.26
Current children cumulated vsize (Kb) 63236

[startup+150.017 s]
Raw data (loadavg): 0.95 0.84 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 13313 0 0 0 14866 57 0 0 25 0 1 0 1731436302 63627264 12919 4294967295 134512640 135094434 3221224432 3221223024 134557435 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 15534 12919 145 145 0 15389 0
[pid=7648] vsize: 62136
Current children cumulated CPU time (s) 149.24
Current children cumulated vsize (Kb) 64260

[startup+160.018 s]
Raw data (loadavg): 0.96 0.85 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 13466 0 0 0 15864 57 0 0 25 0 1 0 1731436302 64237568 13072 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 15683 13072 145 145 0 15538 0
[pid=7648] vsize: 62732
Current children cumulated CPU time (s) 159.22
Current children cumulated vsize (Kb) 64856

[startup+170.019 s]
Raw data (loadavg): 0.97 0.85 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 13775 0 0 0 16860 59 0 0 25 0 1 0 1731436302 65478656 13381 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 15986 13381 145 145 0 15841 0
[pid=7648] vsize: 63944
Current children cumulated CPU time (s) 169.2
Current children cumulated vsize (Kb) 66068

[startup+180.019 s]
Raw data (loadavg): 0.97 0.86 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 14148 0 0 0 17853 62 0 0 25 0 1 0 1731436302 66977792 13754 4294967295 134512640 135094434 3221224432 3221223072 134558043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 16352 13754 145 145 0 16207 0
[pid=7648] vsize: 65408
Current children cumulated CPU time (s) 179.16
Current children cumulated vsize (Kb) 67532

[startup+190.02 s]
Raw data (loadavg): 0.97 0.86 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 14562 0 0 0 18846 64 0 0 25 0 1 0 1731436302 68898816 14168 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7648/statm): 16821 14168 145 145 0 16676 0
[pid=7648] vsize: 67284
Current children cumulated CPU time (s) 189.11
Current children cumulated vsize (Kb) 69408

[startup+200.02 s]
Raw data (loadavg): 0.98 0.86 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 15029 0 0 0 19838 67 0 0 25 0 1 0 1731436302 70787072 14635 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 17282 14635 145 145 0 17137 0
[pid=7648] vsize: 69128
Current children cumulated CPU time (s) 199.06
Current children cumulated vsize (Kb) 71252

[startup+210.021 s]
Raw data (loadavg): 0.98 0.87 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 15506 0 0 0 20831 69 0 0 25 0 1 0 1731436302 72708096 15112 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 17751 15112 145 145 0 17606 0
[pid=7648] vsize: 71004
Current children cumulated CPU time (s) 209.01
Current children cumulated vsize (Kb) 73128

[startup+220.022 s]
Raw data (loadavg): 0.98 0.87 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 15926 0 0 0 21823 73 0 0 25 0 1 0 1731436302 74399744 15532 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 18164 15532 145 145 0 18019 0
[pid=7648] vsize: 72656
Current children cumulated CPU time (s) 218.97
Current children cumulated vsize (Kb) 74780

[startup+230.022 s]
Raw data (loadavg): 0.98 0.88 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 16153 0 0 0 22819 75 0 0 25 0 1 0 1731436302 75304960 15759 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 18385 15759 145 145 0 18240 0
[pid=7648] vsize: 73540
Current children cumulated CPU time (s) 228.95
Current children cumulated vsize (Kb) 75664

[startup+240.023 s]
Raw data (loadavg): 0.99 0.88 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 16396 0 0 0 23817 76 0 0 25 0 1 0 1731436302 76279808 16002 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 18623 16002 145 145 0 18478 0
[pid=7648] vsize: 74492
Current children cumulated CPU time (s) 238.94
Current children cumulated vsize (Kb) 76616

[startup+250.023 s]
Raw data (loadavg): 0.99 0.88 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 16658 0 0 0 24812 78 0 0 25 0 1 0 1731436302 77328384 16264 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 18879 16264 145 145 0 18734 0
[pid=7648] vsize: 75516
Current children cumulated CPU time (s) 248.91
Current children cumulated vsize (Kb) 77640

[startup+260.024 s]
Raw data (loadavg): 0.99 0.89 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 16886 0 0 0 25808 80 0 0 25 0 1 0 1731436302 78237696 16492 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 19101 16492 145 145 0 18956 0
[pid=7648] vsize: 76404
Current children cumulated CPU time (s) 258.89
Current children cumulated vsize (Kb) 78528

[startup+270.025 s]
Raw data (loadavg): 0.99 0.89 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 17266 0 0 0 26802 83 0 0 25 0 1 0 1731436302 79769600 16872 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 19475 16872 145 145 0 19330 0
[pid=7648] vsize: 77900
Current children cumulated CPU time (s) 268.86
Current children cumulated vsize (Kb) 80024

[startup+280.025 s]
Raw data (loadavg): 0.99 0.89 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 17535 0 0 0 27798 85 0 0 25 0 1 0 1731436302 81395712 17141 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 19872 17141 145 145 0 19727 0
[pid=7648] vsize: 79488
Current children cumulated CPU time (s) 278.84
Current children cumulated vsize (Kb) 81612

[startup+290.025 s]
Raw data (loadavg): 0.99 0.90 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 17752 0 0 0 28794 87 0 0 25 0 1 0 1731436302 82268160 17358 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 20085 17358 145 145 0 19940 0
[pid=7648] vsize: 80340
Current children cumulated CPU time (s) 288.82
Current children cumulated vsize (Kb) 82464

[startup+300.026 s]
Raw data (loadavg): 0.99 0.90 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 17871 0 0 0 29792 88 0 0 25 0 1 0 1731436302 82743296 17477 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 20201 17477 145 145 0 20056 0
[pid=7648] vsize: 80804
Current children cumulated CPU time (s) 298.81
Current children cumulated vsize (Kb) 82928

[startup+310.028 s]
Raw data (loadavg): 0.99 0.90 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 18075 0 0 0 30789 89 0 0 25 0 1 0 1731436302 83562496 17681 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 20401 17681 145 145 0 20256 0
[pid=7648] vsize: 81604
Current children cumulated CPU time (s) 308.79
Current children cumulated vsize (Kb) 83728

[startup+320.029 s]
Raw data (loadavg): 0.99 0.90 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) T 7644 7644 17733 0 -1 0 18345 0 0 0 31785 91 0 0 25 0 1 0 1731436302 84647936 17951 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7648/statm): 20666 17951 145 145 0 20521 0
[pid=7648] vsize: 82664
Current children cumulated CPU time (s) 318.77
Current children cumulated vsize (Kb) 84788

[startup+330.029 s]
Raw data (loadavg): 0.99 0.91 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 18670 0 0 0 32779 94 0 0 25 0 1 0 1731436302 85966848 18276 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 20988 18276 145 145 0 20843 0
[pid=7648] vsize: 83952
Current children cumulated CPU time (s) 328.74
Current children cumulated vsize (Kb) 86076

[startup+340.029 s]
Raw data (loadavg): 0.99 0.91 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 18817 0 0 0 33776 95 0 0 25 0 1 0 1731436302 86548480 18423 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 21130 18423 145 145 0 20985 0
[pid=7648] vsize: 84520
Current children cumulated CPU time (s) 338.72
Current children cumulated vsize (Kb) 86644

[startup+350.03 s]
Raw data (loadavg): 0.99 0.91 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 19127 0 0 0 34772 97 0 0 25 0 1 0 1731436302 87793664 18733 4294967295 134512640 135094434 3221224432 3221223072 134562110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 21434 18733 145 145 0 21289 0
[pid=7648] vsize: 85736
Current children cumulated CPU time (s) 348.7
Current children cumulated vsize (Kb) 87860

[startup+360.031 s]
Raw data (loadavg): 0.99 0.91 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) T 7644 7644 17733 0 -1 0 19372 0 0 0 35767 98 0 0 25 0 1 0 1731436302 88776704 18978 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7648/statm): 21674 18978 145 145 0 21529 0
[pid=7648] vsize: 86696
Current children cumulated CPU time (s) 358.66
Current children cumulated vsize (Kb) 88820

[startup+370.032 s]
Raw data (loadavg): 0.99 0.92 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 19681 0 0 0 36762 101 0 0 25 0 1 0 1731436302 90021888 19287 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 21978 19287 145 145 0 21833 0
[pid=7648] vsize: 87912
Current children cumulated CPU time (s) 368.64
Current children cumulated vsize (Kb) 90036

[startup+380.032 s]
Raw data (loadavg): 0.99 0.92 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 20000 0 0 0 37757 103 0 0 25 0 1 0 1731436302 91324416 19606 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 22296 19606 145 145 0 22151 0
[pid=7648] vsize: 89184
Current children cumulated CPU time (s) 378.61
Current children cumulated vsize (Kb) 91308

[startup+390.032 s]
Raw data (loadavg): 0.99 0.92 0.91 1/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) T 7644 7644 17733 0 -1 0 20284 0 0 0 38753 105 0 0 25 0 1 0 1731436302 92475392 19890 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7648/statm): 22577 19890 145 145 0 22432 0
[pid=7648] vsize: 90308
Current children cumulated CPU time (s) 388.59
Current children cumulated vsize (Kb) 92432

[startup+400.033 s]
Raw data (loadavg): 0.99 0.92 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 20554 0 0 0 39749 106 0 0 25 0 1 0 1731436302 93601792 20160 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 22852 20160 145 145 0 22707 0
[pid=7648] vsize: 91408
Current children cumulated CPU time (s) 398.56
Current children cumulated vsize (Kb) 93532

[startup+410.034 s]
Raw data (loadavg): 0.99 0.92 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 20814 0 0 0 40744 108 0 0 25 0 1 0 1731436302 94646272 20420 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 23107 20420 145 145 0 22962 0
[pid=7648] vsize: 92428
Current children cumulated CPU time (s) 408.53
Current children cumulated vsize (Kb) 94552

[startup+420.035 s]
Raw data (loadavg): 0.99 0.93 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 20853 0 0 0 41743 108 0 0 25 0 1 0 1731436302 94826496 20459 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7648/statm): 23151 20459 145 145 0 23006 0
[pid=7648] vsize: 92604
Current children cumulated CPU time (s) 418.52
Current children cumulated vsize (Kb) 94728

[startup+430.036 s]
Raw data (loadavg): 0.99 0.93 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 20957 0 0 0 42742 109 0 0 25 0 1 0 1731436302 95268864 20563 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7648/statm): 23259 20563 145 145 0 23114 0
[pid=7648] vsize: 93036
Current children cumulated CPU time (s) 428.52
Current children cumulated vsize (Kb) 95160

[startup+440.036 s]
Raw data (loadavg): 0.99 0.93 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 21198 0 0 0 43737 111 0 0 25 0 1 0 1731436302 96272384 20804 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 23504 20804 145 145 0 23359 0
[pid=7648] vsize: 94016
Current children cumulated CPU time (s) 438.49
Current children cumulated vsize (Kb) 96140

[startup+450.037 s]
Raw data (loadavg): 0.99 0.93 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 21402 0 0 0 44735 111 0 0 25 0 1 0 1731436302 97091584 21008 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 23704 21008 145 145 0 23559 0
[pid=7648] vsize: 94816
Current children cumulated CPU time (s) 448.47
Current children cumulated vsize (Kb) 96940

[startup+460.038 s]
Raw data (loadavg): 0.99 0.93 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 21637 0 0 0 45730 113 0 0 25 0 1 0 1731436302 98041856 21243 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 23936 21243 145 145 0 23791 0
[pid=7648] vsize: 95744
Current children cumulated CPU time (s) 458.44
Current children cumulated vsize (Kb) 97868

[startup+470.039 s]
Raw data (loadavg): 0.99 0.94 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 21814 0 0 0 46728 115 0 0 25 0 1 0 1731436302 98750464 21420 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 24109 21420 145 145 0 23964 0
[pid=7648] vsize: 96436
Current children cumulated CPU time (s) 468.44
Current children cumulated vsize (Kb) 98560

[startup+480.038 s]
Raw data (loadavg): 0.99 0.94 0.91 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 22021 0 0 0 47724 117 0 0 25 0 1 0 1731436302 99594240 21627 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 24315 21627 145 145 0 24170 0
[pid=7648] vsize: 97260
Current children cumulated CPU time (s) 478.42
Current children cumulated vsize (Kb) 99384

[startup+490.04 s]
Raw data (loadavg): 1.15 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 22235 0 0 0 48720 119 0 0 25 0 1 0 1731436302 100474880 21841 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 24530 21841 145 145 0 24385 0
[pid=7648] vsize: 98120
Current children cumulated CPU time (s) 488.4
Current children cumulated vsize (Kb) 100244

[startup+500.041 s]
Raw data (loadavg): 1.12 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 22386 0 0 0 49719 120 0 0 25 0 1 0 1731436302 101097472 21992 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 24682 21992 145 145 0 24537 0
[pid=7648] vsize: 98728
Current children cumulated CPU time (s) 498.4
Current children cumulated vsize (Kb) 100852

[startup+510.041 s]
Raw data (loadavg): 1.10 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 22638 0 0 0 50713 122 0 0 25 0 1 0 1731436302 102109184 22244 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 24929 22244 145 145 0 24784 0
[pid=7648] vsize: 99716
Current children cumulated CPU time (s) 508.36
Current children cumulated vsize (Kb) 101840

[startup+520.042 s]
Raw data (loadavg): 1.09 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 22918 0 0 0 51709 125 0 0 25 0 1 0 1731436302 103231488 22524 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 25203 22524 145 145 0 25058 0
[pid=7648] vsize: 100812
Current children cumulated CPU time (s) 518.35
Current children cumulated vsize (Kb) 102936

[startup+530.042 s]
Raw data (loadavg): 1.07 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 23068 0 0 0 52706 126 0 0 25 0 1 0 1731436302 103849984 22674 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 25354 22674 145 145 0 25209 0
[pid=7648] vsize: 101416
Current children cumulated CPU time (s) 528.33
Current children cumulated vsize (Kb) 103540

[startup+540.043 s]
Raw data (loadavg): 1.06 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 23361 0 0 0 53700 128 0 0 25 0 1 0 1731436302 105037824 22967 4294967295 134512640 135094434 3221224432 3221223056 134562068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 25644 22967 145 145 0 25499 0
[pid=7648] vsize: 102576
Current children cumulated CPU time (s) 538.29
Current children cumulated vsize (Kb) 104700

[startup+550.044 s]
Raw data (loadavg): 1.05 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 23564 0 0 0 54697 130 0 0 25 0 1 0 1731436302 105852928 23170 4294967295 134512640 135094434 3221224432 3221223088 134558141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 25843 23170 145 145 0 25698 0
[pid=7648] vsize: 103372
Current children cumulated CPU time (s) 548.28
Current children cumulated vsize (Kb) 105496

[startup+560.045 s]
Raw data (loadavg): 1.04 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 23836 0 0 0 55692 132 0 0 25 0 1 0 1731436302 106950656 23442 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 26111 23442 145 145 0 25966 0
[pid=7648] vsize: 104444
Current children cumulated CPU time (s) 558.25
Current children cumulated vsize (Kb) 106568

[startup+570.046 s]
Raw data (loadavg): 1.04 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 24156 0 0 0 56687 134 0 0 25 0 1 0 1731436302 108240896 23762 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 26426 23762 145 145 0 26281 0
[pid=7648] vsize: 105704
Current children cumulated CPU time (s) 568.22
Current children cumulated vsize (Kb) 107828

[startup+580.045 s]
Raw data (loadavg): 1.03 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 24458 0 0 0 57683 136 0 0 25 0 1 0 1731436302 109486080 24064 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 26730 24064 145 145 0 26585 0
[pid=7648] vsize: 106920
Current children cumulated CPU time (s) 578.2
Current children cumulated vsize (Kb) 109044

[startup+590.046 s]
Raw data (loadavg): 1.03 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 24600 0 0 0 58681 137 0 0 25 0 1 0 1731436302 110063616 24206 4294967295 134512640 135094434 3221224432 3221223024 134557168 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 26871 24206 145 145 0 26726 0
[pid=7648] vsize: 107484
Current children cumulated CPU time (s) 588.19
Current children cumulated vsize (Kb) 109608

[startup+600.047 s]
Raw data (loadavg): 1.02 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 24757 0 0 0 59678 139 0 0 25 0 1 0 1731436302 111751168 24363 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 27283 24363 145 145 0 27138 0
[pid=7648] vsize: 109132
Current children cumulated CPU time (s) 598.18
Current children cumulated vsize (Kb) 111256

[startup+610.048 s]
Raw data (loadavg): 1.02 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 24901 0 0 0 60676 140 0 0 25 0 1 0 1731436302 112353280 24507 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 27430 24507 145 145 0 27285 0
[pid=7648] vsize: 109720
Current children cumulated CPU time (s) 608.17
Current children cumulated vsize (Kb) 111844

[startup+620.048 s]
Raw data (loadavg): 1.01 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 24967 0 0 0 61675 141 0 0 25 0 1 0 1731436302 112603136 24573 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 27491 24573 145 145 0 27346 0
[pid=7648] vsize: 109964
Current children cumulated CPU time (s) 618.17
Current children cumulated vsize (Kb) 112088

[startup+630.049 s]
Raw data (loadavg): 1.01 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 25085 0 0 0 62673 141 0 0 25 0 1 0 1731436302 113090560 24691 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 27610 24691 145 145 0 27465 0
[pid=7648] vsize: 110440
Current children cumulated CPU time (s) 628.15
Current children cumulated vsize (Kb) 112564

[startup+640.05 s]
Raw data (loadavg): 1.01 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 25300 0 0 0 63670 143 0 0 25 0 1 0 1731436302 113954816 24906 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 27821 24906 145 145 0 27676 0
[pid=7648] vsize: 111284
Current children cumulated CPU time (s) 638.14
Current children cumulated vsize (Kb) 113408

[startup+650.051 s]
Raw data (loadavg): 1.01 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 25514 0 0 0 64666 145 0 0 25 0 1 0 1731436302 114810880 25120 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 28030 25120 145 145 0 27885 0
[pid=7648] vsize: 112120
Current children cumulated CPU time (s) 648.12
Current children cumulated vsize (Kb) 114244

[startup+660.051 s]
Raw data (loadavg): 1.01 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 25755 0 0 0 65661 147 0 0 25 0 1 0 1731436302 115789824 25361 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 28269 25361 145 145 0 28124 0
[pid=7648] vsize: 113076
Current children cumulated CPU time (s) 658.09
Current children cumulated vsize (Kb) 115200

[startup+670.051 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 25975 0 0 0 66656 150 0 0 25 0 1 0 1731436302 116678656 25581 4294967295 134512640 135094434 3221224432 3221223104 134555553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 28486 25581 145 145 0 28341 0
[pid=7648] vsize: 113944
Current children cumulated CPU time (s) 668.07
Current children cumulated vsize (Kb) 116068

[startup+680.051 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 26128 0 0 0 67654 150 0 0 25 0 1 0 1731436302 117293056 25734 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 28636 25734 145 145 0 28491 0
[pid=7648] vsize: 114544
Current children cumulated CPU time (s) 678.05
Current children cumulated vsize (Kb) 116668

[startup+690.052 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 26290 0 0 0 68650 151 0 0 25 0 1 0 1731436302 117952512 25896 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7648/statm): 28797 25896 145 145 0 28652 0
[pid=7648] vsize: 115188
Current children cumulated CPU time (s) 688.02
Current children cumulated vsize (Kb) 117312

[startup+700.053 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 26428 0 0 0 69647 153 0 0 25 0 1 0 1731436302 118505472 26034 4294967295 134512640 135094434 3221224432 3221223072 134562068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 28932 26034 145 145 0 28787 0
[pid=7648] vsize: 115728
Current children cumulated CPU time (s) 698.01
Current children cumulated vsize (Kb) 117852

[startup+710.053 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 26584 0 0 0 70644 154 0 0 25 0 1 0 1731436302 119136256 26190 4294967295 134512640 135094434 3221224432 3221223088 134558184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 29086 26190 145 145 0 28941 0
[pid=7648] vsize: 116344
Current children cumulated CPU time (s) 707.99
Current children cumulated vsize (Kb) 118468

[startup+720.053 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 26759 0 0 0 71641 156 0 0 25 0 1 0 1731436302 119836672 26365 4294967295 134512640 135094434 3221224432 3221223088 134557792 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 29257 26365 145 145 0 29112 0
[pid=7648] vsize: 117028
Current children cumulated CPU time (s) 717.98
Current children cumulated vsize (Kb) 119152

[startup+730.054 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 26952 0 0 0 72637 156 0 0 25 0 1 0 1731436302 120606720 26558 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 29445 26558 145 145 0 29300 0
[pid=7648] vsize: 117780
Current children cumulated CPU time (s) 727.94
Current children cumulated vsize (Kb) 119904

[startup+740.055 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 27104 0 0 0 73635 158 0 0 25 0 1 0 1731436302 121217024 26710 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 29594 26710 145 145 0 29449 0
[pid=7648] vsize: 118376
Current children cumulated CPU time (s) 737.94
Current children cumulated vsize (Kb) 120500

[startup+750.056 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 27262 0 0 0 74633 159 0 0 25 0 1 0 1731436302 121896960 26868 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 29760 26868 145 145 0 29615 0
[pid=7648] vsize: 119040
Current children cumulated CPU time (s) 747.93
Current children cumulated vsize (Kb) 121164

[startup+760.056 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 27415 0 0 0 75631 160 0 0 25 0 1 0 1731436302 122507264 27021 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 29909 27021 145 145 0 29764 0
[pid=7648] vsize: 119636
Current children cumulated CPU time (s) 757.92
Current children cumulated vsize (Kb) 121760

[startup+770.056 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 27546 0 0 0 76628 161 0 0 25 0 1 0 1731436302 123027456 27152 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 30036 27152 145 145 0 29891 0
[pid=7648] vsize: 120144
Current children cumulated CPU time (s) 767.9
Current children cumulated vsize (Kb) 122268

[startup+780.056 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 27703 0 0 0 77626 162 0 0 25 0 1 0 1731436302 123686912 27309 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 30197 27309 145 145 0 30052 0
[pid=7648] vsize: 120788
Current children cumulated CPU time (s) 777.89
Current children cumulated vsize (Kb) 122912

[startup+790.057 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 27830 0 0 0 78624 163 0 0 25 0 1 0 1731436302 124207104 27436 4294967295 134512640 135094434 3221224432 3221223088 134558292 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 30324 27436 145 145 0 30179 0
[pid=7648] vsize: 121296
Current children cumulated CPU time (s) 787.88
Current children cumulated vsize (Kb) 123420

[startup+800.058 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 27957 0 0 0 79622 164 0 0 25 0 1 0 1731436302 124723200 27563 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 30450 27563 145 145 0 30305 0
[pid=7648] vsize: 121800
Current children cumulated CPU time (s) 797.87
Current children cumulated vsize (Kb) 123924

[startup+810.058 s]
Raw data (loadavg): 1.00 0.97 0.92 1/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) T 7644 7644 17733 0 -1 0 28161 0 0 0 80619 166 0 0 25 0 1 0 1731436302 125542400 27767 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7648/statm): 30650 27767 145 145 0 30505 0
[pid=7648] vsize: 122600
Current children cumulated CPU time (s) 807.86
Current children cumulated vsize (Kb) 124724

[startup+820.059 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 28272 0 0 0 81617 166 0 0 25 0 1 0 1731436302 126005248 27878 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 30763 27878 145 145 0 30618 0
[pid=7648] vsize: 123052
Current children cumulated CPU time (s) 817.84
Current children cumulated vsize (Kb) 125176

[startup+830.059 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 28385 0 0 0 82616 167 0 0 25 0 1 0 1731436302 126451712 27991 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 30872 27991 145 145 0 30727 0
[pid=7648] vsize: 123488
Current children cumulated CPU time (s) 827.84
Current children cumulated vsize (Kb) 125612

[startup+840.06 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 28573 0 0 0 83614 168 0 0 25 0 1 0 1731436302 127221760 28179 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 31060 28179 145 145 0 30915 0
[pid=7648] vsize: 124240
Current children cumulated CPU time (s) 837.83
Current children cumulated vsize (Kb) 126364

[startup+850.061 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 28746 0 0 0 84611 169 0 0 25 0 1 0 1731436302 127913984 28352 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 31229 28352 145 145 0 31084 0
[pid=7648] vsize: 124916
Current children cumulated CPU time (s) 847.81
Current children cumulated vsize (Kb) 127040

[startup+860.06 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 28913 0 0 0 85608 170 0 0 25 0 1 0 1731436302 128581632 28519 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 31392 28519 145 145 0 31247 0
[pid=7648] vsize: 125568
Current children cumulated CPU time (s) 857.79
Current children cumulated vsize (Kb) 127692

[startup+870.061 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 29051 0 0 0 86606 171 0 0 25 0 1 0 1731436302 129167360 28657 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 31535 28657 145 145 0 31390 0
[pid=7648] vsize: 126140
Current children cumulated CPU time (s) 867.78
Current children cumulated vsize (Kb) 128264

[startup+880.062 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 29225 0 0 0 87603 172 0 0 25 0 1 0 1731436302 129871872 28831 4294967295 134512640 135094434 3221224432 3221223104 134555274 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 31707 28831 145 145 0 31562 0
[pid=7648] vsize: 126828
Current children cumulated CPU time (s) 877.76
Current children cumulated vsize (Kb) 128952

[startup+890.063 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 29375 0 0 0 88600 173 0 0 25 0 1 0 1731436302 130473984 28981 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 31854 28981 145 145 0 31709 0
[pid=7648] vsize: 127416
Current children cumulated CPU time (s) 887.74
Current children cumulated vsize (Kb) 129540

[startup+900.064 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 29511 0 0 0 89598 174 0 0 25 0 1 0 1731436302 131010560 29117 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 31985 29117 145 145 0 31840 0
[pid=7648] vsize: 127940
Current children cumulated CPU time (s) 897.73
Current children cumulated vsize (Kb) 130064

[startup+910.064 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 29622 0 0 0 90597 175 0 0 25 0 1 0 1731436302 131469312 29228 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 32097 29228 145 145 0 31952 0
[pid=7648] vsize: 128388
Current children cumulated CPU time (s) 907.73
Current children cumulated vsize (Kb) 130512

[startup+920.065 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 29753 0 0 0 91594 176 0 0 25 0 1 0 1731436302 131997696 29359 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 32226 29359 145 145 0 32081 0
[pid=7648] vsize: 128904
Current children cumulated CPU time (s) 917.71
Current children cumulated vsize (Kb) 131028

[startup+930.065 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 29873 0 0 0 92592 177 0 0 25 0 1 0 1731436302 132485120 29479 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 32345 29479 145 145 0 32200 0
[pid=7648] vsize: 129380
Current children cumulated CPU time (s) 927.7
Current children cumulated vsize (Kb) 131504

[startup+940.066 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 30006 0 0 0 93590 178 0 0 25 0 1 0 1731436302 133013504 29612 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 32474 29612 145 145 0 32329 0
[pid=7648] vsize: 129896
Current children cumulated CPU time (s) 937.69
Current children cumulated vsize (Kb) 132020

[startup+950.067 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 30141 0 0 0 94588 179 0 0 25 0 1 0 1731436302 133554176 29747 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 32606 29747 145 145 0 32461 0
[pid=7648] vsize: 130424
Current children cumulated CPU time (s) 947.68
Current children cumulated vsize (Kb) 132548

[startup+960.066 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 30300 0 0 0 95585 180 0 0 25 0 1 0 1731436302 134197248 29906 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 32763 29906 145 145 0 32618 0
[pid=7648] vsize: 131052
Current children cumulated CPU time (s) 957.66
Current children cumulated vsize (Kb) 133176

[startup+970.067 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 30437 0 0 0 96583 181 0 0 25 0 1 0 1731436302 134746112 30043 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 32897 30043 145 145 0 32752 0
[pid=7648] vsize: 131588
Current children cumulated CPU time (s) 967.65
Current children cumulated vsize (Kb) 133712

[startup+980.068 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 30597 0 0 0 97580 182 0 0 25 0 1 0 1731436302 135397376 30203 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 33056 30203 145 145 0 32911 0
[pid=7648] vsize: 132224
Current children cumulated CPU time (s) 977.63
Current children cumulated vsize (Kb) 134348

[startup+990.069 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 30754 0 0 0 98578 183 0 0 25 0 1 0 1731436302 136056832 30360 4294967295 134512640 135094434 3221224432 3221223168 134559644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 33217 30360 145 145 0 33072 0
[pid=7648] vsize: 132868
Current children cumulated CPU time (s) 987.62
Current children cumulated vsize (Kb) 134992

[startup+1000.07 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 30900 0 0 0 99576 184 0 0 25 0 1 0 1731436302 136679424 30506 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 33369 30506 145 145 0 33224 0
[pid=7648] vsize: 133476
Current children cumulated CPU time (s) 997.61
Current children cumulated vsize (Kb) 135600

[startup+1010.07 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 30987 0 0 0 100574 185 0 0 25 0 1 0 1731436302 137027584 30593 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 33454 30593 145 145 0 33309 0
[pid=7648] vsize: 133816
Current children cumulated CPU time (s) 1007.6
Current children cumulated vsize (Kb) 135940

[startup+1020.07 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 31214 0 0 0 101570 187 0 0 25 0 1 0 1731436302 137945088 30820 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 33678 30820 145 145 0 33533 0
[pid=7648] vsize: 134712
Current children cumulated CPU time (s) 1017.58
Current children cumulated vsize (Kb) 136836

[startup+1030.07 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 31427 0 0 0 102568 188 0 0 25 0 1 0 1731436302 138801152 31033 4294967295 134512640 135094434 3221224432 3221223088 134558123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 33887 31033 145 145 0 33742 0
[pid=7648] vsize: 135548
Current children cumulated CPU time (s) 1027.57
Current children cumulated vsize (Kb) 137672

[startup+1040.07 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 31676 0 0 0 103564 190 0 0 25 0 1 0 1731436302 139890688 31282 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 34153 31282 145 145 0 34008 0
[pid=7648] vsize: 136612
Current children cumulated CPU time (s) 1037.55
Current children cumulated vsize (Kb) 138736

[startup+1050.07 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 31910 0 0 0 104562 191 0 0 25 0 1 0 1731436302 140840960 31516 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 34385 31516 145 145 0 34240 0
[pid=7648] vsize: 137540
Current children cumulated CPU time (s) 1047.54
Current children cumulated vsize (Kb) 139664

[startup+1060.07 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 32195 0 0 0 105557 194 0 0 25 0 1 0 1731436302 141991936 31801 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 34666 31801 145 145 0 34521 0
[pid=7648] vsize: 138664
Current children cumulated CPU time (s) 1057.52
Current children cumulated vsize (Kb) 140788

[startup+1070.07 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 32469 0 0 0 106552 196 0 0 25 0 1 0 1731436302 143101952 32075 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 34937 32075 145 145 0 34792 0
[pid=7648] vsize: 139748
Current children cumulated CPU time (s) 1067.49
Current children cumulated vsize (Kb) 141872

[startup+1080.07 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 32647 0 0 0 107549 197 0 0 25 0 1 0 1731436302 143835136 32253 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 35116 32253 145 145 0 34971 0
[pid=7648] vsize: 140464
Current children cumulated CPU time (s) 1077.47
Current children cumulated vsize (Kb) 142588

[startup+1090.07 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 32777 0 0 0 108548 198 0 0 25 0 1 0 1731436302 144347136 32383 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 35241 32383 145 145 0 35096 0
[pid=7648] vsize: 140964
Current children cumulated CPU time (s) 1087.47
Current children cumulated vsize (Kb) 143088

[startup+1100.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 32982 0 0 0 109544 200 0 0 25 0 1 0 1731436302 145174528 32588 4294967295 134512640 135094434 3221224432 3221223104 134555797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 35443 32588 145 145 0 35298 0
[pid=7648] vsize: 141772
Current children cumulated CPU time (s) 1097.45
Current children cumulated vsize (Kb) 143896

[startup+1110.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 33169 0 0 0 110540 202 0 0 25 0 1 0 1731436302 145915904 32775 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 35624 32775 145 145 0 35479 0
[pid=7648] vsize: 142496
Current children cumulated CPU time (s) 1107.43
Current children cumulated vsize (Kb) 144620

[startup+1120.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 33349 0 0 0 111536 204 0 0 25 0 1 0 1731436302 146640896 32955 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 35801 32955 145 145 0 35656 0
[pid=7648] vsize: 143204
Current children cumulated CPU time (s) 1117.41
Current children cumulated vsize (Kb) 145328

[startup+1130.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 33427 0 0 0 112534 205 0 0 25 0 1 0 1731436302 146952192 33033 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 35877 33033 145 145 0 35732 0
[pid=7648] vsize: 143508
Current children cumulated CPU time (s) 1127.4
Current children cumulated vsize (Kb) 145632

[startup+1140.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 33497 0 0 0 113533 206 0 0 25 0 1 0 1731436302 147279872 33103 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 35957 33103 145 145 0 35812 0
[pid=7648] vsize: 143828
Current children cumulated CPU time (s) 1137.4
Current children cumulated vsize (Kb) 145952

[startup+1150.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 33577 0 0 0 114532 206 0 0 25 0 1 0 1731436302 147652608 33183 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 36048 33183 145 145 0 35903 0
[pid=7648] vsize: 144192
Current children cumulated CPU time (s) 1147.39
Current children cumulated vsize (Kb) 146316

[startup+1160.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 33680 0 0 0 115532 207 0 0 25 0 1 0 1731436302 148111360 33286 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 36160 33286 145 145 0 36015 0
[pid=7648] vsize: 144640
Current children cumulated CPU time (s) 1157.4
Current children cumulated vsize (Kb) 146764

[startup+1170.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 33773 0 0 0 116530 207 0 0 25 0 1 0 1731436302 148508672 33379 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 36257 33379 145 145 0 36112 0
[pid=7648] vsize: 145028
Current children cumulated CPU time (s) 1167.38
Current children cumulated vsize (Kb) 147152

[startup+1180.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 33865 0 0 0 117529 208 0 0 25 0 1 0 1731436302 148889600 33471 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 36350 33471 145 145 0 36205 0
[pid=7648] vsize: 145400
Current children cumulated CPU time (s) 1177.38
Current children cumulated vsize (Kb) 147524

[startup+1190.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 33960 0 0 0 118528 209 0 0 25 0 1 0 1731436302 149274624 33566 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 36444 33566 145 145 0 36299 0
[pid=7648] vsize: 145776
Current children cumulated CPU time (s) 1187.38
Current children cumulated vsize (Kb) 147900

[startup+1200.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 34047 0 0 0 119527 209 0 0 25 0 1 0 1731436302 149602304 33653 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 36524 33653 145 145 0 36379 0
[pid=7648] vsize: 146096
Current children cumulated CPU time (s) 1197.37
Current children cumulated vsize (Kb) 148220

[startup+1210.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 34145 0 0 0 120526 210 0 0 25 0 1 0 1731436302 150007808 33751 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 36623 33751 145 145 0 36478 0
[pid=7648] vsize: 146492
Current children cumulated CPU time (s) 1207.37
Current children cumulated vsize (Kb) 148616



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/58 7648
Raw data (/proc/7644/stat): 7644 (minisat+_script) S 7643 7644 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1731436297 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7644/statm): 531 226 485 147 0 384 0
[pid=7644] vsize: 2124
Raw data (/proc/7648/stat): 7648 (minisat+_64-bit) R 7644 7644 17733 0 -1 0 34145 0 0 0 120526 210 0 0 25 0 1 0 1731436302 150007808 33751 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7648/statm): 36623 33751 145 145 0 36478 0
[pid=7648] vsize: 146492
Current children cumulated CPU time (s) 1207.37
Current children cumulated vsize (Kb) 148616

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

Child status: 0
Real time (s): 1210.15
CPU time (s): 1207.43
CPU user time (s): 1205.27
CPU system time (s): 2.16267
CPU usage (%): 99.7754
Max. virtual memory (cumulated for all children) (Kb): 148616

Verifier Data

ERROR: no interpretation found !