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/miplib3/normalized-mps-v2-20-10-dcmulti.opb
MD5SUM659e380dd1d6168ad99a794b3190043f
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 4508

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        889704 kB
Buffers:         32852 kB
Cached:          84588 kB
SwapCached:        812 kB
Active:          63244 kB
Inactive:        56808 kB
HighTotal:      131008 kB
HighFree:        46116 kB
LowTotal:       903652 kB
LowFree:        843588 kB
SwapTotal:     2097892 kB
SwapFree:      2096456 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5708 kB
Slab:            19192 kB
Committed_AS:    64368 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 18:06:03 (client local time) WITH STATUS 0 IN 1207.33 SECONDS
stats: 2967 7 1207.33 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/4648/stat): 4648 (minisat+_script) R 4647 4648 20602 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1729072121 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/4648/statm): 174 3 169 147 0 27 0
[pid=4648] 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=4649
New process pid=4650
New process pid=4651
execve syscall for /bin/sed executable
One traced child (pid=4650) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=4651) exited with status: 0
One traced child (pid=4649) exited with status: 0
New process pid=4652
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-dcmulti.opb

[startup+10.0038 s]
Raw data (loadavg): 0.93 0.95 0.71 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 11550 0 4 0 888 50 0 0 25 0 1 0 1729072126 56516608 11160 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4652/statm): 13798 11160 145 145 0 13653 0
[pid=4652] vsize: 55192
Current children cumulated CPU time (s) 9.4
Current children cumulated vsize (Kb) 57316

[startup+20.0045 s]
Raw data (loadavg): 0.94 0.96 0.71 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 11590 0 4 0 1888 50 0 0 25 0 1 0 1729072126 56668160 11200 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4652/statm): 13835 11200 145 145 0 13690 0
[pid=4652] vsize: 55340
Current children cumulated CPU time (s) 19.4
Current children cumulated vsize (Kb) 57464

[startup+30.0051 s]
Raw data (loadavg): 0.95 0.96 0.71 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 11611 0 4 0 2887 50 0 0 25 0 1 0 1729072126 56741888 11221 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4652/statm): 13853 11221 145 145 0 13708 0
[pid=4652] vsize: 55412
Current children cumulated CPU time (s) 29.39
Current children cumulated vsize (Kb) 57536

[startup+40.0058 s]
Raw data (loadavg): 0.96 0.96 0.71 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 11645 0 4 0 3887 51 0 0 25 0 1 0 1729072126 56823808 11255 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4652/statm): 13873 11255 145 145 0 13728 0
[pid=4652] vsize: 55492
Current children cumulated CPU time (s) 39.4
Current children cumulated vsize (Kb) 57616

[startup+50.0065 s]
Raw data (loadavg): 0.96 0.96 0.72 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 11686 0 4 0 4886 52 0 0 25 0 1 0 1729072126 56975360 11296 4294967295 134512640 135094434 3221224432 3221223044 134563043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4652/statm): 13910 11296 145 145 0 13765 0
[pid=4652] vsize: 55640
Current children cumulated CPU time (s) 49.4
Current children cumulated vsize (Kb) 57764

[startup+60.0072 s]
Raw data (loadavg): 0.97 0.96 0.72 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 11713 0 4 0 5885 52 0 0 25 0 1 0 1729072126 57061376 11323 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 13931 11323 145 145 0 13786 0
[pid=4652] vsize: 55724
Current children cumulated CPU time (s) 59.39
Current children cumulated vsize (Kb) 57848

[startup+70.0079 s]
Raw data (loadavg): 0.97 0.96 0.72 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 11732 0 4 0 6885 52 0 0 25 0 1 0 1729072126 57135104 11342 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 13949 11342 145 145 0 13804 0
[pid=4652] vsize: 55796
Current children cumulated CPU time (s) 69.39
Current children cumulated vsize (Kb) 57920

[startup+80.0086 s]
Raw data (loadavg): 0.98 0.96 0.73 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 11766 0 4 0 7885 53 0 0 25 0 1 0 1729072126 57266176 11376 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 13981 11376 145 145 0 13836 0
[pid=4652] vsize: 55924
Current children cumulated CPU time (s) 79.4
Current children cumulated vsize (Kb) 58048

[startup+90.0093 s]
Raw data (loadavg): 0.98 0.96 0.73 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 11785 0 4 0 8885 53 0 0 25 0 1 0 1729072126 57335808 11395 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 13998 11395 145 145 0 13853 0
[pid=4652] vsize: 55992
Current children cumulated CPU time (s) 89.4
Current children cumulated vsize (Kb) 58116

[startup+100.009 s]
Raw data (loadavg): 0.98 0.96 0.73 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 11890 0 4 0 9883 54 0 0 25 0 1 0 1729072126 57749504 11500 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 14099 11500 145 145 0 13954 0
[pid=4652] vsize: 56396
Current children cumulated CPU time (s) 99.39
Current children cumulated vsize (Kb) 58520

[startup+110.01 s]
Raw data (loadavg): 0.98 0.96 0.73 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 12173 0 4 0 10879 55 0 0 25 0 1 0 1729072126 58945536 11783 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 14391 11783 145 145 0 14246 0
[pid=4652] vsize: 57564
Current children cumulated CPU time (s) 109.36
Current children cumulated vsize (Kb) 59688

[startup+120.01 s]
Raw data (loadavg): 0.99 0.97 0.73 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 12417 0 4 0 11874 57 0 0 25 0 1 0 1729072126 59924480 12027 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 14630 12027 145 145 0 14485 0
[pid=4652] vsize: 58520
Current children cumulated CPU time (s) 119.33
Current children cumulated vsize (Kb) 60644

[startup+130.01 s]
Raw data (loadavg): 0.99 0.97 0.74 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 12746 0 4 0 12869 60 0 0 25 0 1 0 1729072126 61374464 12356 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 14984 12356 145 145 0 14839 0
[pid=4652] vsize: 59936
Current children cumulated CPU time (s) 129.31
Current children cumulated vsize (Kb) 62060

[startup+140.011 s]
Raw data (loadavg): 0.99 0.97 0.74 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 13029 0 4 0 13865 61 0 0 25 0 1 0 1729072126 62504960 12639 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 15260 12639 145 145 0 15115 0
[pid=4652] vsize: 61040
Current children cumulated CPU time (s) 139.28
Current children cumulated vsize (Kb) 63164

[startup+150.011 s]
Raw data (loadavg): 0.99 0.97 0.74 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 13298 0 4 0 14860 63 0 0 25 0 1 0 1729072126 63582208 12908 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 15523 12908 145 145 0 15378 0
[pid=4652] vsize: 62092
Current children cumulated CPU time (s) 149.25
Current children cumulated vsize (Kb) 64216

[startup+160.011 s]
Raw data (loadavg): 0.99 0.97 0.74 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 13454 0 4 0 15857 66 0 0 25 0 1 0 1729072126 64204800 13064 4294967295 134512640 135094434 3221224432 3221223024 134551780 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 15675 13064 145 145 0 15530 0
[pid=4652] vsize: 62700
Current children cumulated CPU time (s) 159.25
Current children cumulated vsize (Kb) 64824

[startup+170.012 s]
Raw data (loadavg): 0.99 0.97 0.74 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 13748 0 4 0 16851 69 0 0 25 0 1 0 1729072126 65384448 13358 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 15963 13358 145 145 0 15818 0
[pid=4652] vsize: 63852
Current children cumulated CPU time (s) 169.22
Current children cumulated vsize (Kb) 65976

[startup+180.012 s]
Raw data (loadavg): 0.99 0.97 0.75 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 14124 0 4 0 17845 72 0 0 25 0 1 0 1729072126 66899968 13734 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 16333 13734 145 145 0 16188 0
[pid=4652] vsize: 65332
Current children cumulated CPU time (s) 179.19
Current children cumulated vsize (Kb) 67456

[startup+190.012 s]
Raw data (loadavg): 0.99 0.97 0.75 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 14504 0 4 0 18838 75 0 0 25 0 1 0 1729072126 68681728 14114 4294967295 134512640 135094434 3221224432 3221223104 134555310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 16768 14114 145 145 0 16623 0
[pid=4652] vsize: 67072
Current children cumulated CPU time (s) 189.15
Current children cumulated vsize (Kb) 69196

[startup+200.013 s]
Raw data (loadavg): 0.99 0.97 0.75 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 14924 0 4 0 19831 78 0 0 25 0 1 0 1729072126 70377472 14534 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 17182 14534 145 145 0 17037 0
[pid=4652] vsize: 68728
Current children cumulated CPU time (s) 199.11
Current children cumulated vsize (Kb) 70852

[startup+210.014 s]
Raw data (loadavg): 0.99 0.97 0.75 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 15452 0 4 0 20822 82 0 0 25 0 1 0 1729072126 72503296 15062 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 17701 15062 145 145 0 17556 0
[pid=4652] vsize: 70804
Current children cumulated CPU time (s) 209.06
Current children cumulated vsize (Kb) 72928

[startup+220.014 s]
Raw data (loadavg): 0.99 0.97 0.75 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 15889 0 4 0 21815 84 0 0 25 0 1 0 1729072126 74264576 15499 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 18131 15499 145 145 0 17986 0
[pid=4652] vsize: 72524
Current children cumulated CPU time (s) 219.01
Current children cumulated vsize (Kb) 74648

[startup+230.015 s]
Raw data (loadavg): 0.99 0.97 0.76 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 16100 0 4 0 22813 85 0 0 25 0 1 0 1729072126 75108352 15710 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 18337 15710 145 145 0 18192 0
[pid=4652] vsize: 73348
Current children cumulated CPU time (s) 229
Current children cumulated vsize (Kb) 75472

[startup+240.016 s]
Raw data (loadavg): 0.99 0.97 0.76 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 16360 0 4 0 23809 87 0 0 25 0 1 0 1729072126 76148736 15970 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 18591 15970 145 145 0 18446 0
[pid=4652] vsize: 74364
Current children cumulated CPU time (s) 238.98
Current children cumulated vsize (Kb) 76488

[startup+250.016 s]
Raw data (loadavg): 0.99 0.97 0.76 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 16619 0 4 0 24805 89 0 0 25 0 1 0 1729072126 77189120 16229 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 18845 16229 145 145 0 18700 0
[pid=4652] vsize: 75380
Current children cumulated CPU time (s) 248.96
Current children cumulated vsize (Kb) 77504

[startup+260.016 s]
Raw data (loadavg): 0.99 0.97 0.76 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 16818 0 4 0 25801 90 0 0 25 0 1 0 1729072126 77983744 16428 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 19039 16428 145 145 0 18894 0
[pid=4652] vsize: 76156
Current children cumulated CPU time (s) 258.93
Current children cumulated vsize (Kb) 78280

[startup+270.017 s]
Raw data (loadavg): 0.99 0.97 0.76 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 17201 0 4 0 26795 93 0 0 25 0 1 0 1729072126 79523840 16811 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 19415 16811 145 145 0 19270 0
[pid=4652] vsize: 77660
Current children cumulated CPU time (s) 268.9
Current children cumulated vsize (Kb) 79784

[startup+280.018 s]
Raw data (loadavg): 0.99 0.97 0.77 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 17491 0 4 0 27789 95 0 0 25 0 1 0 1729072126 81231872 17101 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4652/statm): 19832 17101 145 145 0 19687 0
[pid=4652] vsize: 79328
Current children cumulated CPU time (s) 278.86
Current children cumulated vsize (Kb) 81452

[startup+290.019 s]
Raw data (loadavg): 0.99 0.97 0.77 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 17714 0 4 0 28785 96 0 0 25 0 1 0 1729072126 82128896 17324 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4652/statm): 20051 17324 145 145 0 19906 0
[pid=4652] vsize: 80204
Current children cumulated CPU time (s) 288.83
Current children cumulated vsize (Kb) 82328

[startup+300.019 s]
Raw data (loadavg): 0.99 0.97 0.77 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 17866 0 4 0 29781 98 0 0 25 0 1 0 1729072126 82739200 17476 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 20200 17476 145 145 0 20055 0
[pid=4652] vsize: 80800
Current children cumulated CPU time (s) 298.81
Current children cumulated vsize (Kb) 82924

[startup+310.02 s]
Raw data (loadavg): 0.99 0.97 0.77 1/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) T 4648 4648 20602 0 -1 0 17979 0 4 0 30779 99 0 0 25 0 1 0 1729072126 83189760 17589 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/4652/statm): 20310 17589 145 145 0 20165 0
[pid=4652] vsize: 81240
Current children cumulated CPU time (s) 308.8
Current children cumulated vsize (Kb) 83364

[startup+320.021 s]
Raw data (loadavg): 0.99 0.97 0.77 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 18279 0 4 0 31774 101 0 0 25 0 1 0 1729072126 84402176 17889 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 20606 17889 145 145 0 20461 0
[pid=4652] vsize: 82424
Current children cumulated CPU time (s) 318.77
Current children cumulated vsize (Kb) 84548

[startup+330.021 s]
Raw data (loadavg): 0.99 0.97 0.78 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 18567 0 4 0 32770 103 0 0 25 0 1 0 1729072126 85565440 18177 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 20890 18177 145 145 0 20745 0
[pid=4652] vsize: 83560
Current children cumulated CPU time (s) 328.75
Current children cumulated vsize (Kb) 85684

[startup+340.022 s]
Raw data (loadavg): 0.99 0.97 0.78 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 18808 0 4 0 33766 105 0 0 25 0 1 0 1729072126 86528000 18418 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 21125 18418 145 145 0 20980 0
[pid=4652] vsize: 84500
Current children cumulated CPU time (s) 338.73
Current children cumulated vsize (Kb) 86624

[startup+350.022 s]
Raw data (loadavg): 0.99 0.97 0.78 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 19037 0 4 0 34763 106 0 0 25 0 1 0 1729072126 87449600 18647 4294967295 134512640 135094434 3221224432 3221223120 134554796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 21350 18647 145 145 0 21205 0
[pid=4652] vsize: 85400
Current children cumulated CPU time (s) 348.71
Current children cumulated vsize (Kb) 87524

[startup+360.023 s]
Raw data (loadavg): 0.99 0.97 0.78 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 19315 0 4 0 35759 108 0 0 25 0 1 0 1729072126 88563712 18925 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 21622 18925 145 145 0 21477 0
[pid=4652] vsize: 86488
Current children cumulated CPU time (s) 358.69
Current children cumulated vsize (Kb) 88612

[startup+370.023 s]
Raw data (loadavg): 0.99 0.97 0.78 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 19598 0 4 0 36753 110 0 0 25 0 1 0 1729072126 89702400 19208 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 21900 19208 145 145 0 21755 0
[pid=4652] vsize: 87600
Current children cumulated CPU time (s) 368.65
Current children cumulated vsize (Kb) 89724

[startup+380.023 s]
Raw data (loadavg): 0.99 0.97 0.79 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 19917 0 4 0 37748 112 0 0 25 0 1 0 1729072126 90996736 19527 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 22216 19527 145 145 0 22071 0
[pid=4652] vsize: 88864
Current children cumulated CPU time (s) 378.62
Current children cumulated vsize (Kb) 90988

[startup+390.024 s]
Raw data (loadavg): 0.99 0.97 0.79 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 20206 0 4 0 38743 114 0 0 25 0 1 0 1729072126 92168192 19816 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 22502 19816 145 145 0 22357 0
[pid=4652] vsize: 90008
Current children cumulated CPU time (s) 388.59
Current children cumulated vsize (Kb) 92132

[startup+400.024 s]
Raw data (loadavg): 0.99 0.97 0.79 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 20470 0 4 0 39739 115 0 0 25 0 1 0 1729072126 93253632 20080 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 22767 20080 145 145 0 22622 0
[pid=4652] vsize: 91068
Current children cumulated CPU time (s) 398.56
Current children cumulated vsize (Kb) 93192

[startup+410.025 s]
Raw data (loadavg): 0.99 0.97 0.79 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 20740 0 4 0 40734 117 0 0 25 0 1 0 1729072126 94367744 20350 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 23039 20350 145 145 0 22894 0
[pid=4652] vsize: 92156
Current children cumulated CPU time (s) 408.53
Current children cumulated vsize (Kb) 94280

[startup+420.026 s]
Raw data (loadavg): 0.99 0.97 0.79 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 20840 0 4 0 41732 118 0 0 25 0 1 0 1729072126 94785536 20450 4294967295 134512640 135094434 3221224432 3221223092 134553528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4652/statm): 23141 20450 145 145 0 22996 0
[pid=4652] vsize: 92564
Current children cumulated CPU time (s) 418.52
Current children cumulated vsize (Kb) 94688

[startup+430.027 s]
Raw data (loadavg): 0.99 0.97 0.80 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 20896 0 4 0 42732 118 0 0 25 0 1 0 1729072126 95031296 20506 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4652/statm): 23201 20506 145 145 0 23056 0
[pid=4652] vsize: 92804
Current children cumulated CPU time (s) 428.52
Current children cumulated vsize (Kb) 94928

[startup+440.027 s]
Raw data (loadavg): 0.99 0.97 0.80 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 21126 0 4 0 43727 121 0 0 25 0 1 0 1729072126 95989760 20736 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 23435 20736 145 145 0 23290 0
[pid=4652] vsize: 93740
Current children cumulated CPU time (s) 438.5
Current children cumulated vsize (Kb) 95864

[startup+450.028 s]
Raw data (loadavg): 0.99 0.97 0.80 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 21335 0 4 0 44724 122 0 0 25 0 1 0 1729072126 96845824 20945 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 23644 20945 145 145 0 23499 0
[pid=4652] vsize: 94576
Current children cumulated CPU time (s) 448.48
Current children cumulated vsize (Kb) 96700

[startup+460.029 s]
Raw data (loadavg): 0.99 0.97 0.80 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 21567 0 4 0 45721 123 0 0 25 0 1 0 1729072126 97771520 21177 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 23870 21177 145 145 0 23725 0
[pid=4652] vsize: 95480
Current children cumulated CPU time (s) 458.46
Current children cumulated vsize (Kb) 97604

[startup+470.029 s]
Raw data (loadavg): 0.99 0.97 0.80 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 21779 0 4 0 46717 124 0 0 25 0 1 0 1729072126 98631680 21389 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 24080 21389 145 145 0 23935 0
[pid=4652] vsize: 96320
Current children cumulated CPU time (s) 468.43
Current children cumulated vsize (Kb) 98444

[startup+480.029 s]
Raw data (loadavg): 0.99 0.97 0.81 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 21957 0 4 0 47715 125 0 0 25 0 1 0 1729072126 99344384 21567 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 24254 21567 145 145 0 24109 0
[pid=4652] vsize: 97016
Current children cumulated CPU time (s) 478.42
Current children cumulated vsize (Kb) 99140

[startup+490.03 s]
Raw data (loadavg): 0.99 0.97 0.81 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 22180 0 4 0 48712 126 0 0 25 0 1 0 1729072126 100274176 21790 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 24481 21790 145 145 0 24336 0
[pid=4652] vsize: 97924
Current children cumulated CPU time (s) 488.4
Current children cumulated vsize (Kb) 100048

[startup+500.031 s]
Raw data (loadavg): 0.99 0.97 0.81 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 22356 0 4 0 49709 128 0 0 25 0 1 0 1729072126 100990976 21966 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 24656 21966 145 145 0 24511 0
[pid=4652] vsize: 98624
Current children cumulated CPU time (s) 498.39
Current children cumulated vsize (Kb) 100748

[startup+510.031 s]
Raw data (loadavg): 0.99 0.97 0.81 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 22525 0 4 0 50706 129 0 0 25 0 1 0 1729072126 101670912 22135 4294967295 134512640 135094434 3221224432 3221223024 134557133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 24822 22135 145 145 0 24677 0
[pid=4652] vsize: 99288
Current children cumulated CPU time (s) 508.37
Current children cumulated vsize (Kb) 101412

[startup+520.032 s]
Raw data (loadavg): 0.99 0.97 0.81 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 22815 0 4 0 51700 131 0 0 25 0 1 0 1729072126 102834176 22425 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 25106 22425 145 145 0 24961 0
[pid=4652] vsize: 100424
Current children cumulated CPU time (s) 518.33
Current children cumulated vsize (Kb) 102548

[startup+530.032 s]
Raw data (loadavg): 0.99 0.97 0.81 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 23032 0 4 0 52696 133 0 0 25 0 1 0 1729072126 103706624 22642 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 25319 22642 145 145 0 25174 0
[pid=4652] vsize: 101276
Current children cumulated CPU time (s) 528.31
Current children cumulated vsize (Kb) 103400

[startup+540.032 s]
Raw data (loadavg): 0.99 0.97 0.82 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 23326 0 4 0 53690 136 0 0 25 0 1 0 1729072126 104910848 22936 4294967295 134512640 135094434 3221224432 3221223088 134558172 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 25613 22936 145 145 0 25468 0
[pid=4652] vsize: 102452
Current children cumulated CPU time (s) 538.28
Current children cumulated vsize (Kb) 104576

[startup+550.032 s]
Raw data (loadavg): 0.99 0.97 0.82 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 23470 0 4 0 54688 137 0 0 25 0 1 0 1729072126 105492480 23080 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 25755 23080 145 145 0 25610 0
[pid=4652] vsize: 103020
Current children cumulated CPU time (s) 548.27
Current children cumulated vsize (Kb) 105144

[startup+560.033 s]
Raw data (loadavg): 0.99 0.97 0.82 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) T 4648 4648 20602 0 -1 0 23754 0 4 0 55682 138 0 0 25 0 1 0 1729072126 106631168 23364 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/4652/statm): 26033 23364 145 145 0 25888 0
[pid=4652] vsize: 104132
Current children cumulated CPU time (s) 558.22
Current children cumulated vsize (Kb) 106256

[startup+570.033 s]
Raw data (loadavg): 0.99 0.97 0.82 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 24019 0 4 0 56678 141 0 0 25 0 1 0 1729072126 107704320 23629 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 26295 23629 145 145 0 26150 0
[pid=4652] vsize: 105180
Current children cumulated CPU time (s) 568.21
Current children cumulated vsize (Kb) 107304

[startup+580.034 s]
Raw data (loadavg): 0.99 0.97 0.82 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 24398 0 4 0 57671 144 0 0 25 0 1 0 1729072126 109252608 24008 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 26673 24008 145 145 0 26528 0
[pid=4652] vsize: 106692
Current children cumulated CPU time (s) 578.17
Current children cumulated vsize (Kb) 108816

[startup+590.035 s]
Raw data (loadavg): 0.99 0.97 0.82 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 24538 0 4 0 58668 145 0 0 25 0 1 0 1729072126 109821952 24148 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 26812 24148 145 145 0 26667 0
[pid=4652] vsize: 107248
Current children cumulated CPU time (s) 588.15
Current children cumulated vsize (Kb) 109372

[startup+600.035 s]
Raw data (loadavg): 0.99 0.97 0.82 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 24699 0 4 0 59666 146 0 0 25 0 1 0 1729072126 111525888 24309 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 27228 24309 145 145 0 27083 0
[pid=4652] vsize: 108912
Current children cumulated CPU time (s) 598.14
Current children cumulated vsize (Kb) 111036

[startup+610.036 s]
Raw data (loadavg): 0.99 0.97 0.83 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 24839 0 4 0 60663 147 0 0 25 0 1 0 1729072126 112115712 24449 4294967295 134512640 135094434 3221224432 3221222912 134780630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 27372 24449 145 145 0 27227 0
[pid=4652] vsize: 109488
Current children cumulated CPU time (s) 608.12
Current children cumulated vsize (Kb) 111612

[startup+620.037 s]
Raw data (loadavg): 0.99 0.97 0.83 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 24930 0 4 0 61663 147 0 0 25 0 1 0 1729072126 112480256 24540 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 27461 24540 145 145 0 27316 0
[pid=4652] vsize: 109844
Current children cumulated CPU time (s) 618.12
Current children cumulated vsize (Kb) 111968

[startup+630.037 s]
Raw data (loadavg): 0.99 0.97 0.83 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 25064 0 4 0 62661 148 0 0 25 0 1 0 1729072126 113020928 24674 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 27593 24674 145 145 0 27448 0
[pid=4652] vsize: 110372
Current children cumulated CPU time (s) 628.11
Current children cumulated vsize (Kb) 112496

[startup+640.038 s]
Raw data (loadavg): 0.99 0.97 0.83 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 25195 0 4 0 63659 149 0 0 25 0 1 0 1729072126 113549312 24805 4294967295 134512640 135094434 3221224432 3221223088 134558284 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 27722 24805 145 145 0 27577 0
[pid=4652] vsize: 110888
Current children cumulated CPU time (s) 638.1
Current children cumulated vsize (Kb) 113012

[startup+650.039 s]
Raw data (loadavg): 0.99 0.97 0.83 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 25410 0 4 0 64654 151 0 0 25 0 1 0 1729072126 114413568 25020 4294967295 134512640 135094434 3221224432 3221223056 134557630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 27933 25020 145 145 0 27788 0
[pid=4652] vsize: 111732
Current children cumulated CPU time (s) 648.07
Current children cumulated vsize (Kb) 113856

[startup+660.04 s]
Raw data (loadavg): 0.99 0.97 0.83 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 25681 0 4 0 65650 153 0 0 25 0 1 0 1729072126 115494912 25291 4294967295 134512640 135094434 3221224432 3221223088 134558289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 28197 25291 145 145 0 28052 0
[pid=4652] vsize: 112788
Current children cumulated CPU time (s) 658.05
Current children cumulated vsize (Kb) 114912

[startup+670.04 s]
Raw data (loadavg): 0.99 0.97 0.83 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 25858 0 4 0 66647 155 0 0 25 0 1 0 1729072126 116228096 25468 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 28376 25468 145 145 0 28231 0
[pid=4652] vsize: 113504
Current children cumulated CPU time (s) 668.04
Current children cumulated vsize (Kb) 115628

[startup+680.041 s]
Raw data (loadavg): 0.99 0.97 0.83 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 26057 0 4 0 67643 156 0 0 25 0 1 0 1729072126 117018624 25667 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 28569 25667 145 145 0 28424 0
[pid=4652] vsize: 114276
Current children cumulated CPU time (s) 678.01
Current children cumulated vsize (Kb) 116400

[startup+690.042 s]
Raw data (loadavg): 0.99 0.97 0.83 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 26223 0 4 0 68640 158 0 0 25 0 1 0 1729072126 117690368 25833 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 28733 25833 145 145 0 28588 0
[pid=4652] vsize: 114932
Current children cumulated CPU time (s) 688
Current children cumulated vsize (Kb) 117056

[startup+700.043 s]
Raw data (loadavg): 0.99 0.97 0.83 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 26392 0 4 0 69637 160 0 0 25 0 1 0 1729072126 118378496 26002 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 28901 26002 145 145 0 28756 0
[pid=4652] vsize: 115604
Current children cumulated CPU time (s) 697.99
Current children cumulated vsize (Kb) 117728

[startup+710.043 s]
Raw data (loadavg): 0.99 0.97 0.83 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 26515 0 4 0 70634 160 0 0 25 0 1 0 1729072126 118874112 26125 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 29022 26125 145 145 0 28877 0
[pid=4652] vsize: 116088
Current children cumulated CPU time (s) 707.96
Current children cumulated vsize (Kb) 118212

[startup+720.044 s]
Raw data (loadavg): 0.99 0.97 0.84 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 26674 0 4 0 71631 161 0 0 25 0 1 0 1729072126 119508992 26284 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 29177 26284 145 145 0 29032 0
[pid=4652] vsize: 116708
Current children cumulated CPU time (s) 717.94
Current children cumulated vsize (Kb) 118832

[startup+730.044 s]
Raw data (loadavg): 0.99 0.97 0.84 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 26869 0 4 0 72628 163 0 0 25 0 1 0 1729072126 120295424 26479 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 29369 26479 145 145 0 29224 0
[pid=4652] vsize: 117476
Current children cumulated CPU time (s) 727.93
Current children cumulated vsize (Kb) 119600

[startup+740.044 s]
Raw data (loadavg): 0.99 0.97 0.84 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) T 4648 4648 20602 0 -1 0 27063 0 4 0 73625 164 0 0 25 0 1 0 1729072126 121065472 26673 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/4652/statm): 29557 26673 145 145 0 29412 0
[pid=4652] vsize: 118228
Current children cumulated CPU time (s) 737.91
Current children cumulated vsize (Kb) 120352

[startup+750.045 s]
Raw data (loadavg): 0.99 0.97 0.84 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 27210 0 4 0 74623 165 0 0 25 0 1 0 1729072126 121659392 26820 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 29702 26820 145 145 0 29557 0
[pid=4652] vsize: 118808
Current children cumulated CPU time (s) 747.9
Current children cumulated vsize (Kb) 120932

[startup+760.046 s]
Raw data (loadavg): 0.99 0.97 0.84 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 27352 0 4 0 75620 167 0 0 25 0 1 0 1729072126 122273792 26962 4294967295 134512640 135094434 3221224432 3221223080 134558258 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 29852 26962 145 145 0 29707 0
[pid=4652] vsize: 119408
Current children cumulated CPU time (s) 757.89
Current children cumulated vsize (Kb) 121532

[startup+770.046 s]
Raw data (loadavg): 0.99 0.97 0.84 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 27485 0 4 0 76617 168 0 0 25 0 1 0 1729072126 122798080 27095 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 29980 27095 145 145 0 29835 0
[pid=4652] vsize: 119920
Current children cumulated CPU time (s) 767.87
Current children cumulated vsize (Kb) 122044

[startup+780.047 s]
Raw data (loadavg): 0.99 0.97 0.84 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 27615 0 4 0 77615 169 0 0 25 0 1 0 1729072126 123322368 27225 4294967295 134512640 135094434 3221224432 3221223056 134557711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 30108 27225 145 145 0 29963 0
[pid=4652] vsize: 120432
Current children cumulated CPU time (s) 777.86
Current children cumulated vsize (Kb) 122556

[startup+790.048 s]
Raw data (loadavg): 0.99 0.97 0.84 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 27732 0 4 0 78613 171 0 0 25 0 1 0 1729072126 123809792 27342 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 30227 27342 145 145 0 30082 0
[pid=4652] vsize: 120908
Current children cumulated CPU time (s) 787.86
Current children cumulated vsize (Kb) 123032

[startup+800.048 s]
Raw data (loadavg): 0.99 0.97 0.84 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 27908 0 4 0 79610 172 0 0 25 0 1 0 1729072126 124534784 27518 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 30404 27518 145 145 0 30259 0
[pid=4652] vsize: 121616
Current children cumulated CPU time (s) 797.84
Current children cumulated vsize (Kb) 123740

[startup+810.05 s]
Raw data (loadavg): 0.99 0.97 0.84 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 28056 0 4 0 80609 173 0 0 25 0 1 0 1729072126 125132800 27666 4294967295 134512640 135094434 3221224432 3221223088 134558284 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 30550 27666 145 145 0 30405 0
[pid=4652] vsize: 122200
Current children cumulated CPU time (s) 807.84
Current children cumulated vsize (Kb) 124324

[startup+820.052 s]
Raw data (loadavg): 0.99 0.97 0.85 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 28216 0 4 0 81606 174 0 0 25 0 1 0 1729072126 125775872 27826 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 30707 27826 145 145 0 30562 0
[pid=4652] vsize: 122828
Current children cumulated CPU time (s) 817.82
Current children cumulated vsize (Kb) 124952

[startup+830.052 s]
Raw data (loadavg): 0.99 0.97 0.85 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 28332 0 4 0 82605 174 0 0 25 0 1 0 1729072126 126259200 27942 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 30825 27942 145 145 0 30680 0
[pid=4652] vsize: 123300
Current children cumulated CPU time (s) 827.81
Current children cumulated vsize (Kb) 125424

[startup+840.052 s]
Raw data (loadavg): 0.99 0.97 0.85 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 28464 0 4 0 83603 176 0 0 25 0 1 0 1729072126 126791680 28074 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 30955 28074 145 145 0 30810 0
[pid=4652] vsize: 123820
Current children cumulated CPU time (s) 837.81
Current children cumulated vsize (Kb) 125944

[startup+850.053 s]
Raw data (loadavg): 0.99 0.97 0.85 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 28660 0 4 0 84599 177 0 0 25 0 1 0 1729072126 127586304 28270 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 31149 28270 145 145 0 31004 0
[pid=4652] vsize: 124596
Current children cumulated CPU time (s) 847.78
Current children cumulated vsize (Kb) 126720

[startup+860.054 s]
Raw data (loadavg): 0.99 0.97 0.85 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 28839 0 4 0 85597 178 0 0 25 0 1 0 1729072126 128307200 28449 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 31325 28449 145 145 0 31180 0
[pid=4652] vsize: 125300
Current children cumulated CPU time (s) 857.77
Current children cumulated vsize (Kb) 127424

[startup+870.054 s]
Raw data (loadavg): 0.99 0.97 0.85 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 28989 0 4 0 86594 179 0 0 25 0 1 0 1729072126 128925696 28599 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 31476 28599 145 145 0 31331 0
[pid=4652] vsize: 125904
Current children cumulated CPU time (s) 867.75
Current children cumulated vsize (Kb) 128028

[startup+880.055 s]
Raw data (loadavg): 0.99 0.97 0.85 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 29118 0 4 0 87592 180 0 0 25 0 1 0 1729072126 129454080 28728 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 31605 28728 145 145 0 31460 0
[pid=4652] vsize: 126420
Current children cumulated CPU time (s) 877.74
Current children cumulated vsize (Kb) 128544

[startup+890.056 s]
Raw data (loadavg): 0.99 0.97 0.85 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 29327 0 4 0 88588 181 0 0 25 0 1 0 1729072126 130293760 28937 4294967295 134512640 135094434 3221224432 3221223092 134553466 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 31810 28937 145 145 0 31665 0
[pid=4652] vsize: 127240
Current children cumulated CPU time (s) 887.71
Current children cumulated vsize (Kb) 129364

[startup+900.056 s]
Raw data (loadavg): 0.99 0.97 0.85 2/58 4652
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 29477 0 4 0 89585 182 0 0 25 0 1 0 1729072126 130891776 29087 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 31956 29087 145 145 0 31811 0
[pid=4652] vsize: 127824
Current children cumulated CPU time (s) 897.69
Current children cumulated vsize (Kb) 129948

[startup+910.057 s]
Raw data (loadavg): 0.99 0.97 0.85 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 29562 0 4 0 90585 183 0 0 25 0 1 0 1729072126 131244032 29172 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 32042 29172 145 145 0 31897 0
[pid=4652] vsize: 128168
Current children cumulated CPU time (s) 907.7
Current children cumulated vsize (Kb) 130292

[startup+920.058 s]
Raw data (loadavg): 0.99 0.97 0.86 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 29681 0 4 0 91583 183 0 0 25 0 1 0 1729072126 131723264 29291 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 32159 29291 145 145 0 32014 0
[pid=4652] vsize: 128636
Current children cumulated CPU time (s) 917.68
Current children cumulated vsize (Kb) 130760

[startup+930.058 s]
Raw data (loadavg): 0.99 0.97 0.86 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 29811 0 4 0 92580 184 0 0 25 0 1 0 1729072126 132251648 29421 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 32288 29421 145 145 0 32143 0
[pid=4652] vsize: 129152
Current children cumulated CPU time (s) 927.66
Current children cumulated vsize (Kb) 131276

[startup+940.058 s]
Raw data (loadavg): 0.99 0.97 0.86 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 29934 0 4 0 93578 186 0 0 25 0 1 0 1729072126 132743168 29544 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 32408 29544 145 145 0 32263 0
[pid=4652] vsize: 129632
Current children cumulated CPU time (s) 937.66
Current children cumulated vsize (Kb) 131756

[startup+950.059 s]
Raw data (loadavg): 0.99 0.97 0.86 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 30070 0 4 0 94575 186 0 0 25 0 1 0 1729072126 133279744 29680 4294967295 134512640 135094434 3221224432 3221223076 134558040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 32539 29680 145 145 0 32394 0
[pid=4652] vsize: 130156
Current children cumulated CPU time (s) 947.63
Current children cumulated vsize (Kb) 132280

[startup+960.06 s]
Raw data (loadavg): 0.99 0.97 0.86 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 30211 0 4 0 95573 188 0 0 25 0 1 0 1729072126 133861376 29821 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 32681 29821 145 145 0 32536 0
[pid=4652] vsize: 130724
Current children cumulated CPU time (s) 957.63
Current children cumulated vsize (Kb) 132848

[startup+970.06 s]
Raw data (loadavg): 0.99 0.97 0.86 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 30366 0 4 0 96570 189 0 0 25 0 1 0 1729072126 134475776 29976 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 32831 29976 145 145 0 32686 0
[pid=4652] vsize: 131324
Current children cumulated CPU time (s) 967.61
Current children cumulated vsize (Kb) 133448

[startup+980.06 s]
Raw data (loadavg): 0.99 0.97 0.86 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 30512 0 4 0 97567 190 0 0 25 0 1 0 1729072126 135065600 30122 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 32975 30122 145 145 0 32830 0
[pid=4652] vsize: 131900
Current children cumulated CPU time (s) 977.59
Current children cumulated vsize (Kb) 134024

[startup+990.061 s]
Raw data (loadavg): 0.99 0.97 0.86 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 30666 0 4 0 98564 192 0 0 25 0 1 0 1729072126 135720960 30276 4294967295 134512640 135094434 3221224432 3221223024 134556791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 33135 30276 145 145 0 32990 0
[pid=4652] vsize: 132540
Current children cumulated CPU time (s) 987.58
Current children cumulated vsize (Kb) 134664

[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.86 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 30821 0 4 0 99561 193 0 0 25 0 1 0 1729072126 136372224 30431 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 33294 30431 145 145 0 33149 0
[pid=4652] vsize: 133176
Current children cumulated CPU time (s) 997.56
Current children cumulated vsize (Kb) 135300

[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.86 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 30952 0 4 0 100559 194 0 0 25 0 1 0 1729072126 136900608 30562 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 33423 30562 145 145 0 33278 0
[pid=4652] vsize: 133692
Current children cumulated CPU time (s) 1007.55
Current children cumulated vsize (Kb) 135816

[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.87 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 31083 0 4 0 101557 195 0 0 25 0 1 0 1729072126 137433088 30693 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 33553 30693 145 145 0 33408 0
[pid=4652] vsize: 134212
Current children cumulated CPU time (s) 1017.54
Current children cumulated vsize (Kb) 136336

[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.87 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 31314 0 4 0 102553 197 0 0 25 0 1 0 1729072126 138362880 30924 4294967295 134512640 135094434 3221224432 3221223088 134558026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 33780 30924 145 145 0 33635 0
[pid=4652] vsize: 135120
Current children cumulated CPU time (s) 1027.52
Current children cumulated vsize (Kb) 137244

[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.87 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 31545 0 4 0 103548 199 0 0 25 0 1 0 1729072126 139292672 31155 4294967295 134512640 135094434 3221224432 3221223104 134555566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 34007 31155 145 145 0 33862 0
[pid=4652] vsize: 136028
Current children cumulated CPU time (s) 1037.49
Current children cumulated vsize (Kb) 138152

[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.87 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 31768 0 4 0 104544 200 0 0 25 0 1 0 1729072126 140283904 31378 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 34249 31378 145 145 0 34104 0
[pid=4652] vsize: 136996
Current children cumulated CPU time (s) 1047.46
Current children cumulated vsize (Kb) 139120

[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.87 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 32037 0 4 0 105539 202 0 0 25 0 1 0 1729072126 141369344 31647 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 34514 31647 145 145 0 34369 0
[pid=4652] vsize: 138056
Current children cumulated CPU time (s) 1057.43
Current children cumulated vsize (Kb) 140180

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.87 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 32323 0 4 0 106535 203 0 0 25 0 1 0 1729072126 142528512 31933 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 34797 31933 145 145 0 34652 0
[pid=4652] vsize: 139188
Current children cumulated CPU time (s) 1067.4
Current children cumulated vsize (Kb) 141312

[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.87 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 32574 0 4 0 107531 204 0 0 25 0 1 0 1729072126 143552512 32184 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 35047 32184 145 145 0 34902 0
[pid=4652] vsize: 140188
Current children cumulated CPU time (s) 1077.37
Current children cumulated vsize (Kb) 142312

[startup+1090.07 s]
Raw data (loadavg): 0.99 0.97 0.87 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 32708 0 4 0 108529 206 0 0 25 0 1 0 1729072126 144084992 32318 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 35177 32318 145 145 0 35032 0
[pid=4652] vsize: 140708
Current children cumulated CPU time (s) 1087.37
Current children cumulated vsize (Kb) 142832

[startup+1100.07 s]
Raw data (loadavg): 0.99 0.97 0.87 1/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) T 4648 4648 20602 0 -1 0 32850 0 4 0 109527 207 0 0 25 0 1 0 1729072126 144666624 32460 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/4652/statm): 35319 32460 145 145 0 35174 0
[pid=4652] vsize: 141276
Current children cumulated CPU time (s) 1097.36
Current children cumulated vsize (Kb) 143400

[startup+1110.07 s]
Raw data (loadavg): 0.99 0.97 0.87 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 33107 0 4 0 110522 209 0 0 25 0 1 0 1729072126 145694720 32717 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 35570 32717 145 145 0 35425 0
[pid=4652] vsize: 142280
Current children cumulated CPU time (s) 1107.33
Current children cumulated vsize (Kb) 144404

[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.87 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 33252 0 4 0 111521 210 0 0 25 0 1 0 1729072126 146264064 32862 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 35709 32862 145 145 0 35564 0
[pid=4652] vsize: 142836
Current children cumulated CPU time (s) 1117.33
Current children cumulated vsize (Kb) 144960

[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.88 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 33389 0 4 0 112518 211 0 0 25 0 1 0 1729072126 146817024 32999 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 35844 32999 145 145 0 35699 0
[pid=4652] vsize: 143376
Current children cumulated CPU time (s) 1127.31
Current children cumulated vsize (Kb) 145500

[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.88 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 33448 0 4 0 113518 211 0 0 25 0 1 0 1729072126 147091456 33058 4294967295 134512640 135094434 3221224432 3221223044 134563092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 35911 33058 145 145 0 35766 0
[pid=4652] vsize: 143644
Current children cumulated CPU time (s) 1137.31
Current children cumulated vsize (Kb) 145768

[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.88 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 33539 0 4 0 114517 212 0 0 25 0 1 0 1729072126 147501056 33149 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 36011 33149 145 145 0 35866 0
[pid=4652] vsize: 144044
Current children cumulated CPU time (s) 1147.31
Current children cumulated vsize (Kb) 146168

[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.88 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 33617 0 4 0 115516 213 0 0 25 0 1 0 1729072126 147857408 33227 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 36098 33227 145 145 0 35953 0
[pid=4652] vsize: 144392
Current children cumulated CPU time (s) 1157.31
Current children cumulated vsize (Kb) 146516

[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.88 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 33708 0 4 0 116515 214 0 0 25 0 1 0 1729072126 148262912 33318 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 36197 33318 145 145 0 36052 0
[pid=4652] vsize: 144788
Current children cumulated CPU time (s) 1167.31
Current children cumulated vsize (Kb) 146912

[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.88 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 33807 0 4 0 117514 214 0 0 25 0 1 0 1729072126 148652032 33417 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 36292 33417 145 145 0 36147 0
[pid=4652] vsize: 145168
Current children cumulated CPU time (s) 1177.3
Current children cumulated vsize (Kb) 147292

[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.88 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 33902 0 4 0 118512 215 0 0 25 0 1 0 1729072126 149057536 33512 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 36391 33512 145 145 0 36246 0
[pid=4652] vsize: 145564
Current children cumulated CPU time (s) 1187.29
Current children cumulated vsize (Kb) 147688

[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.88 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 33999 0 4 0 119510 216 0 0 25 0 1 0 1729072126 149438464 33609 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 36484 33609 145 145 0 36339 0
[pid=4652] vsize: 145936
Current children cumulated CPU time (s) 1197.28
Current children cumulated vsize (Kb) 148060

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.88 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 34091 0 4 0 120509 216 0 0 25 0 1 0 1729072126 149807104 33701 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 36574 33701 145 145 0 36429 0
[pid=4652] vsize: 146296
Current children cumulated CPU time (s) 1207.27
Current children cumulated vsize (Kb) 148420



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.88 2/58 4654
Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4648/statm): 531 226 485 147 0 384 0
[pid=4648] vsize: 2124
Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 34091 0 4 0 120509 216 0 0 25 0 1 0 1729072126 149807104 33701 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4652/statm): 36574 33701 145 145 0 36429 0
[pid=4652] vsize: 146296
Current children cumulated CPU time (s) 1207.27
Current children cumulated vsize (Kb) 148420

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

Child status: 0
Real time (s): 1210.14
CPU time (s): 1207.33
CPU user time (s): 1205.1
CPU system time (s): 2.23066
CPU usage (%): 99.7678
Max. virtual memory (cumulated for all children) (Kb): 148420

Verifier Data

ERROR: no interpretation found !