Some explanations

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

General information on the benchmark

Namemps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-tuff.opb
MD5SUM06d4e815794ce4b5deed10c51066684b
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 60
Biggest coefficient in the objective function 524288
Number of bits for the biggest coefficient in the objective function 20
Sum of the numbers in the objective function 3145725
Number of bits of the sum of numbers in the objective function 22
Biggest number in a constraint 6025434365952
Number of bits of the biggest number in a constraint 43
Biggest sum of numbers in a constraint 1078851036553950
Number of bits of the biggest sum of numbers50
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables11495
Total number of constraints320
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints320
Minimum length of a constraint8
Maximum length of a constraint2240

Trace number 6064

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        921060 kB
Buffers:          3524 kB
Cached:          80656 kB
SwapCached:        820 kB
Active:          21284 kB
Inactive:        65552 kB
HighTotal:      131008 kB
HighFree:        46228 kB
LowTotal:       903652 kB
LowFree:        874832 kB
SwapTotal:     2097892 kB
SwapFree:      2096508 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5640 kB
Slab:            21060 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:18:27 (client local time) WITH STATUS 0 IN 1208.42 SECONDS
stats: 3210 7 1208.42 0

Solver Data

c Parsing PB file...
c Converting 553 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ############################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ss
c ---[ 554]---> BDD-cost:   10
c ---[ 553]---> BDD-cost:   10
c ---[ 552]---> BDD-cost:   12
c ---[ 551]---> BDD-cost:   10
c ---[ 550]---> BDD-cost:   11
c ---[ 549]---> BDD-cost:   14
c ---[ 548]---> BDD-cost:   11
c ---[ 547]---> BDD-cost:   11
c ---[ 546]---> BDD-cost:    7
c ---[ 545]---> BDD-cost:    9
c ---[ 541]---> BDD-cost:   11
c ---[ 536]---> BDD-cost:   12
c ---[ 535]---> BDD-cost:   15
c ---[ 533]---> BDD-cost:   12
c ---[ 532]---> BDD-cost:    8
c ---[ 531]---> BDD-cost:   10
c ---[ 530]---> BDD-cost:   10
c ---[ 529]---> BDD-cost:    7
c ---[ 527]---> BDD-cost:  778
c ---[ 525]---> BDD-cost:   64
c ---[ 521]---> Sorter-cost: 2214     Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2
c ---[ 519]---> BDD-cost:   54
c ---[ 517]---> BDD-cost:  863
c ---[ 513]---> BDD-cost:  931
c ---[ 511]---> Sorter-cost:  622     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 509]---> Sorter-cost:  752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 505]---> Sorter-cost:  752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 503]---> Sorter-cost:  752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 501]---> BDD-cost:   40
c ---[ 499]---> BDD-cost:   51
c ---[ 495]---> BDD-cost:   51
c ---[ 493]---> BDD-cost:   40
c ---[ 491]---> BDD-cost:   53
c ---[ 487]---> BDD-cost:  225
c ---[ 485]---> BDD-cost:   40
c ---[ 483]---> BDD-cost:   51
c ---[ 479]---> BDD-cost:   51
c ---[ 477]---> BDD-cost:   51
c ---[ 475]---> Adder-cost: 509   maxlim: 2285382   bits: 23/22
c ---[ 473]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 471]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 469]---> BDD-cost:  114
c ---[ 467]---> BDD-cost:   36
c ---[ 463]---> BDD-cost:   36
c ---[ 461]---> BDD-cost:   36
c ---[ 459]---> BDD-cost:   40
c ---[ 455]---> BDD-cost:   36
c ---[ 451]---> BDD-cost:   36
c ---[ 449]---> Adder-cost: 985   maxlim: 8901434   bits: 25/24
c ---[ 447]---> Adder-cost: 318   maxlim: 350037   bits: 20/19
c ---[ 443]---> Sorter-cost:15513     Base: 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 2 2
c ---[ 441]---> BDD-cost:  159
c ---[ 439]---> Sorter-cost: 2170     Base: 5 5 5 2 2 2 2 2 2 2 2 2 2
c ---[ 437]---> Sorter-cost:  379     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 435]---> BDD-cost:   28
c ---[ 433]---> BDD-cost:   28
c ---[ 431]---> BDD-cost:   46
c ---[ 429]---> Sorter-cost: 3431     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2
c ---[ 423]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 421]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 419]---> Sorter-cost:  506     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 417]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 415]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 413]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 411]---> Sorter-cost:  469     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 409]---> Sorter-cost:  469     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 407]---> Sorter-cost:  469     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 405]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 403]---> Sorter-cost:  506     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 399]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 397]---> Sorter-cost:  506     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 395]---> Sorter-cost:  469     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 393]---> Adder-cost: 552   maxlim: 2866973   bits: 23/22
c ---[ 391]---> Adder-cost: 433   maxlim: 2047827   bits: 22/21
c ---[ 389]---> Sorter-cost: 2471     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 5 2
c ---[ 387]---> Adder-cost: 2098   maxlim: 741739   bits: 20/20
c ---[ 385]---> Adder-cost: 9948   maxlim: 568059429   bits: 31/30
c ---[ 383]---> Sorter-cost: 1247     Base: 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 2
c ---[ 381]---> Adder-cost: 2026   maxlim: 481643   bits: 19/19
c ---[ 379]---> Adder-cost: 9646   maxlim: 368774693   bits: 30/29
c ---[ 377]---> Sorter-cost: 1405     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2
c ---[ 375]---> Adder-cost: 2026   maxlim: 481643   bits: 19/19
c ---[ 373]---> Adder-cost: 9646   maxlim: 368774693   bits: 30/29
c ---[ 371]---> Adder-cost: 2121   maxlim: 334037412   bits: 30/29
c ---[ 369]---> Adder-cost: 2214   maxlim: 105376178425   bits: 38/37
c ---[ 367]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 365]---> Sorter-cost:  428     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 363]---> Sorter-cost: 3132     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[ 361]---> BDD-cost:  327
c ---[ 359]---> Sorter-cost: 4437     Base: 2 2 2 2 5 2 2 2 2 2 2 2 3 2 2 2 2 2
c ---[ 357]---> BDD-cost:   86
c ---[ 355]---> BDD-cost:   25
c ---[ 351]---> Sorter-cost:  459     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 349]---> BDD-cost:  105
c ---[ 347]---> Sorter-cost: 2036     Base: 2 2 2 2 2 2 2 5 2 5 2 2 2 2 2
c ---[ 345]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 343]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 341]---> Sorter-cost:  759     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 339]---> Adder-cost: 1566   maxlim: 274942400   bits: 30/29
c ---[ 337]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 335]---> Sorter-cost:  468     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 333]---> Sorter-cost: 3193     Base: 2 2 2 2 2 2 13 2 2 2 3 2
c ---[ 331]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 329]---> BDD-cost:  116
c ---[ 325]---> BDD-cost:  109
c ---[ 323]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 321]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 319]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 317]---> Adder-cost: 439   maxlim: 1164743   bits: 22/21
c ---[ 315]---> BDD-cost:   43
c ---[ 313]---> BDD-cost:  109
c ---[ 311]---> BDD-cost:  118
c ---[ 309]---> BDD-cost:  109
c ---[ 307]---> BDD-cost:  118
c ---[ 305]---> Sorter-cost:  508     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 303]---> Sorter-cost:  547     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 301]---> Sorter-cost:  508     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 299]---> Sorter-cost:  547     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 297]---> Adder-cost: 1981   maxlim: 449996839   bits: 30/29
c ---[ 295]---> Adder-cost: 2665   maxlim: 727026800   bits: 31/30
c ---[ 293]---> Adder-cost: 620   maxlim: 712644   bits: 21/20
c ---[ 291]---> Adder-cost: 326   maxlim: 270270   bits: 20/19
c ---[ 289]---> Sorter-cost: 1593     Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 287]---> Sorter-cost: 3678     Base: 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2
c ---[ 285]---> Sorter-cost: 2540     Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2
c ---[ 283]---> BDD-cost:  100
c ---[ 281]---> Adder-cost: 2138   maxlim: 1364267409   bits: 32/31
c ---[ 279]---> BDD-cost:   91
c ---[ 273]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 271]---> Sorter-cost:  570     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 269]---> Sorter-cost: 5333     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[ 267]---> Sorter-cost: 5813     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[ 265]---> Adder-cost: 1114   maxlim: 422672800   bits: 30/29
c ---[ 263]---> BDD-cost:  275
c ---[ 261]---> BDD-cost:  301
c ---[ 259]---> Sorter-cost: 1710     Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 3 3 2
c ---[ 257]---> Adder-cost: 1134   maxlim: 422672800   bits: 30/29
c ---[ 255]---> Sorter-cost: 5281     Base: 2 5 5 5 2 2 2 2 2 2 2 2 5 2 2 2 2
c ---[ 253]---> Sorter-cost: 2616     Base: 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[ 251]---> Sorter-cost:  313     Base: 2 2 2 2 2 2 2 2
c ---[ 245]---> Sorter-cost: 2911     Base: 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 243]---> BDD-cost:  397
c ---[ 241]---> Adder-cost: 1004   maxlim: 57748900   bits: 27/26
c ---[ 239]---> Sorter-cost:  796     Base: 2 2 2 2 2 2 2 2 5 2
c ---[ 237]---> Sorter-cost: 1983     Base: 2 2 2 2 2 2 5 2 5 2 2 2 2
c ---[ 235]---> Sorter-cost: 1839     Base: 2 2 2 2 2 2 2 2 2 5 2 2 2 2
c ---[ 233]---> Sorter-cost: 2917     Base: 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 5
c ---[ 231]---> Sorter-cost: 3164     Base: 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2 5
c ---[ 229]---> Sorter-cost: 2027     Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2
c ---[ 227]---> Sorter-cost: 2021     Base: 2 2 2 2 2 2 13 2 2 2 2 3 2
c ---[ 225]---> Adder-cost: 559   maxlim: 1826648   bits: 22/21
c ---[ 223]---> BDD-cost:  171
c ---[ 221]---> BDD-cost:   51
c ---[ 219]---> BDD-cost:   55
c ---[ 217]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 215]---> Sorter-cost:  469     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 213]---> Sorter-cost:  469     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 209]---> Sorter-cost:  506     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 205]---> Sorter-cost:  506     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 203]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 201]---> Sorter-cost:  506     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 199]---> Sorter-cost:  506     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 197]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 195]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 193]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 191]---> Sorter-cost:  506     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 189]---> BDD-cost: 1013
c ---[ 185]---> Sorter-cost: 6016     Base: 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 183]---> Sorter-cost:  506     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost:  506     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 179]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 177]---> Adder-cost: 453   maxlim: 2965198   bits: 23/22
c ---[ 175]---> BDD-cost:   31
c ---[ 173]---> BDD-cost:   40
c ---[ 169]---> BDD-cost:   43
c ---[ 167]---> BDD-cost:   46
c ---[ 165]---> BDD-cost:   91
c ---[ 163]---> BDD-cost:  116
c ---[ 159]---> BDD-cost:  121
c ---[ 157]---> BDD-cost:  126
c ---[ 155]---> Sorter-cost: 2066     Base: 2 2 2 2 2 2 2 2 5 2 2 2 2
c ---[ 153]---> BDD-cost:  116
c ---[ 151]---> Sorter-cost:  988     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 149]---> Sorter-cost: 2593     Base: 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 147]---> Sorter-cost:  389     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 145]---> BDD-cost:  138
c ---[ 143]---> BDD-cost:  138
c ---[ 141]---> BDD-cost:  163
c ---[ 137]---> Adder-cost: 466   maxlim: 16383000   bits: 25/24
c ---[ 135]---> Sorter-cost:  622     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 133]---> BDD-cost:   51
c ---[ 131]---> Sorter-cost:  855     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 129]---> Sorter-cost:  858     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 127]---> Sorter-cost: 2533     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 125]---> Sorter-cost:  879     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 123]---> Sorter-cost: 1512     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 121]---> BDD-cost:   98
c ---[ 119]---> BDD-cost:   34
c ---[ 117]---> BDD-cost:  115
c ---[ 115]---> BDD-cost:   34
c ---[ 113]---> BDD-cost:   34
c ---[ 111]---> BDD-cost:   34
c ---[ 109]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 107]---> Sorter-cost: 2196     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 103]---> BDD-cost:  137
c ---[ 101]---> Adder-cost: 320   maxlim: 262143   bits: 19/18
c ---[  99]---> Sorter-cost: 3786     Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[  97]---> Sorter-cost: 1668     Base: 2 2 2 2 2 2 2 2 5 5 3
c ---[  95]---> BDD-cost:  132
c ---[  93]---> BDD-cost:  132
c ---[  91]---> BDD-cost:  143
c ---[  88]---> Sorter-cost:  331     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  87]---> Sorter-cost:  312     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  86]---> Sorter-cost:  312     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  85]---> Adder-cost: 6656   maxlim: 8191499   bits: 24/23

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/28304/stat): 28304 (minisat+_script) R 28303 28304 2660 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855116962 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/28304/statm): 174 3 169 147 0 27 0
[pid=28304] 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=28305
New process pid=28306
New process pid=28307
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
One traced child (pid=28306) exited with status: 0
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=28307) exited with status: 0
One traced child (pid=28305) exited with status: 0
New process pid=28308
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-tuff.opb

[startup+10.0042 s]
Raw data (loadavg): 0.87 0.94 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 10827 0 0 0 932 38 0 0 25 0 1 0 1855116967 17661952 3993 4294967295 134512640 135094434 3221224432 3221215344 134594905 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 4312 3993 145 145 0 4167 0
[pid=28308] vsize: 17248
Current children cumulated CPU time (s) 9.7
Current children cumulated vsize (Kb) 19372

[startup+20.0049 s]
Raw data (loadavg): 0.89 0.94 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 11084 0 0 0 1931 39 0 0 25 0 1 0 1855116967 19410944 4250 4294967295 134512640 135094434 3221224432 3221220280 134676461 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 4739 4250 145 145 0 4594 0
[pid=28308] vsize: 18956
Current children cumulated CPU time (s) 19.7
Current children cumulated vsize (Kb) 21080

[startup+30.0057 s]
Raw data (loadavg): 0.90 0.94 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 11084 0 0 0 2931 39 0 0 25 0 1 0 1855116967 19410944 4250 4294967295 134512640 135094434 3221224432 3221220928 134677327 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 4739 4250 145 145 0 4594 0
[pid=28308] vsize: 18956
Current children cumulated CPU time (s) 29.7
Current children cumulated vsize (Kb) 21080

[startup+40.0064 s]
Raw data (loadavg): 0.92 0.94 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 11084 0 0 0 3932 39 0 0 25 0 1 0 1855116967 19410944 4250 4294967295 134512640 135094434 3221224432 3221221104 134677363 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 4739 4250 145 145 0 4594 0
[pid=28308] vsize: 18956
Current children cumulated CPU time (s) 39.71
Current children cumulated vsize (Kb) 21080

[startup+50.0071 s]
Raw data (loadavg): 0.93 0.94 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 11084 0 0 0 4932 39 0 0 25 0 1 0 1855116967 19410944 4250 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 4739 4250 145 145 0 4594 0
[pid=28308] vsize: 18956
Current children cumulated CPU time (s) 49.71
Current children cumulated vsize (Kb) 21080

[startup+60.0079 s]
Raw data (loadavg): 0.94 0.95 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 11084 0 0 0 5932 39 0 0 25 0 1 0 1855116967 19410944 4250 4294967295 134512640 135094434 3221224432 3221221808 134600267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 4739 4250 145 145 0 4594 0
[pid=28308] vsize: 18956
Current children cumulated CPU time (s) 59.71
Current children cumulated vsize (Kb) 21080

[startup+70.0086 s]
Raw data (loadavg): 0.95 0.95 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 11084 0 0 0 6932 39 0 0 25 0 1 0 1855116967 19410944 4250 4294967295 134512640 135094434 3221224432 3221221984 134677327 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 4739 4250 145 145 0 4594 0
[pid=28308] vsize: 18956
Current children cumulated CPU time (s) 69.71
Current children cumulated vsize (Kb) 21080

[startup+80.0093 s]
Raw data (loadavg): 0.96 0.95 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 11084 0 0 0 7932 39 0 0 25 0 1 0 1855116967 19410944 4250 4294967295 134512640 135094434 3221224432 3221221756 134519600 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 4739 4250 145 145 0 4594 0
[pid=28308] vsize: 18956
Current children cumulated CPU time (s) 79.71
Current children cumulated vsize (Kb) 21080

[startup+90.01 s]
Raw data (loadavg): 0.96 0.95 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12044 0 0 0 8930 41 0 0 25 0 1 0 1855116967 23683072 5210 4294967295 134512640 135094434 3221224432 3221220576 134600228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5210 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 89.71
Current children cumulated vsize (Kb) 25252

[startup+100.01 s]
Raw data (loadavg): 0.97 0.95 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12044 0 0 0 9930 41 0 0 25 0 1 0 1855116967 23683072 5210 4294967295 134512640 135094434 3221224432 3221221432 134676989 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5210 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 99.71
Current children cumulated vsize (Kb) 25252

[startup+110.011 s]
Raw data (loadavg): 0.97 0.95 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12044 0 0 0 10931 41 0 0 25 0 1 0 1855116967 23683072 5210 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5210 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 109.72
Current children cumulated vsize (Kb) 25252

[startup+120.012 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12044 0 0 0 11930 42 0 0 25 0 1 0 1855116967 23683072 5210 4294967295 134512640 135094434 3221224432 3221221280 134677333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5210 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 119.72
Current children cumulated vsize (Kb) 25252

[startup+130.012 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12044 0 0 0 12930 43 0 0 25 0 1 0 1855116967 23683072 5210 4294967295 134512640 135094434 3221224432 3221221632 134677300 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5210 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 129.73
Current children cumulated vsize (Kb) 25252

[startup+140.013 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12085 0 0 0 13929 43 0 0 25 0 1 0 1855116967 23683072 5251 4294967295 134512640 135094434 3221224432 3221219872 134677346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5251 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 139.72
Current children cumulated vsize (Kb) 25252

[startup+150.012 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12085 0 0 0 14929 44 0 0 25 0 1 0 1855116967 23683072 5251 4294967295 134512640 135094434 3221224432 3221220468 134676335 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5251 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 149.73
Current children cumulated vsize (Kb) 25252

[startup+160.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12085 0 0 0 15929 44 0 0 25 0 1 0 1855116967 23683072 5251 4294967295 134512640 135094434 3221224432 3221221376 134676280 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5251 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 159.73
Current children cumulated vsize (Kb) 25252

[startup+170.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12085 0 0 0 16929 44 0 0 25 0 1 0 1855116967 23683072 5251 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5251 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 169.73
Current children cumulated vsize (Kb) 25252

[startup+180.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12085 0 0 0 17929 44 0 0 25 0 1 0 1855116967 23683072 5251 4294967295 134512640 135094434 3221224432 3221221440 134600246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5251 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 179.73
Current children cumulated vsize (Kb) 25252

[startup+190.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12085 0 0 0 18929 44 0 0 25 0 1 0 1855116967 23683072 5251 4294967295 134512640 135094434 3221224432 3221221520 134676336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5251 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 189.73
Current children cumulated vsize (Kb) 25252

[startup+200.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12125 0 0 0 19929 45 0 0 25 0 1 0 1855116967 23683072 5291 4294967295 134512640 135094434 3221224432 3221220576 134600310 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5291 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 199.74
Current children cumulated vsize (Kb) 25252

[startup+210.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12125 0 0 0 20930 45 0 0 25 0 1 0 1855116967 23683072 5291 4294967295 134512640 135094434 3221224432 3221221696 134677086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5291 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 209.75
Current children cumulated vsize (Kb) 25252

[startup+220.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12125 0 0 0 21930 45 0 0 25 0 1 0 1855116967 23683072 5291 4294967295 134512640 135094434 3221224432 3221221808 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5291 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 219.75
Current children cumulated vsize (Kb) 25252

[startup+230.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12125 0 0 0 22930 45 0 0 25 0 1 0 1855116967 23683072 5291 4294967295 134512640 135094434 3221224432 3221221808 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5291 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 229.75
Current children cumulated vsize (Kb) 25252

[startup+240.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12126 0 0 0 23930 45 0 0 25 0 1 0 1855116967 23683072 5292 4294967295 134512640 135094434 3221224432 3221221280 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5292 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 239.75
Current children cumulated vsize (Kb) 25252

[startup+250.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12126 0 0 0 24930 45 0 0 25 0 1 0 1855116967 23683072 5292 4294967295 134512640 135094434 3221224432 3221221104 134600310 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5292 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 249.75
Current children cumulated vsize (Kb) 25252

[startup+260.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12126 0 0 0 25930 45 0 0 25 0 1 0 1855116967 23683072 5292 4294967295 134512640 135094434 3221224432 3221220752 134676489 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5292 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 259.75
Current children cumulated vsize (Kb) 25252

[startup+270.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12126 0 0 0 26930 45 0 0 25 0 1 0 1855116967 23683072 5292 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5292 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 269.75
Current children cumulated vsize (Kb) 25252

[startup+280.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12126 0 0 0 27930 45 0 0 25 0 1 0 1855116967 23683072 5292 4294967295 134512640 135094434 3221224432 3221221024 134677042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5292 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 279.75
Current children cumulated vsize (Kb) 25252

[startup+290.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12126 0 0 0 28931 45 0 0 25 0 1 0 1855116967 23683072 5292 4294967295 134512640 135094434 3221224432 3221221788 134676988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5292 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 289.76
Current children cumulated vsize (Kb) 25252

[startup+300.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12126 0 0 0 29931 46 0 0 25 0 1 0 1855116967 23683072 5292 4294967295 134512640 135094434 3221224432 3221184800 134596854 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5292 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 299.77
Current children cumulated vsize (Kb) 25252

[startup+310.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12126 0 0 0 30931 46 0 0 25 0 1 0 1855116967 23683072 5292 4294967295 134512640 135094434 3221224432 3221220576 134600225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5292 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 309.77
Current children cumulated vsize (Kb) 25252

[startup+320.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12126 0 0 0 31931 46 0 0 25 0 1 0 1855116967 23683072 5292 4294967295 134512640 135094434 3221224432 3221220848 134677021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5292 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 319.77
Current children cumulated vsize (Kb) 25252

[startup+330.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12126 0 0 0 32931 46 0 0 25 0 1 0 1855116967 23683072 5292 4294967295 134512640 135094434 3221224432 3221221456 134676595 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5292 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 329.77
Current children cumulated vsize (Kb) 25252

[startup+340.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 12126 0 0 0 33932 46 0 0 25 0 1 0 1855116967 23683072 5292 4294967295 134512640 135094434 3221224432 3221221984 134600295 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5782 5292 145 145 0 5637 0
[pid=28308] vsize: 23128
Current children cumulated CPU time (s) 339.78
Current children cumulated vsize (Kb) 25252

[startup+350.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 20607 0 0 0 34880 76 0 0 25 0 1 0 1855116967 23793664 5319 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5809 5319 145 145 0 5664 0
[pid=28308] vsize: 23236
Current children cumulated CPU time (s) 349.56
Current children cumulated vsize (Kb) 25360

[startup+360.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 20607 0 0 0 35880 76 0 0 25 0 1 0 1855116967 23793664 5319 4294967295 134512640 135094434 3221224432 3221220848 134677056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5809 5319 145 145 0 5664 0
[pid=28308] vsize: 23236
Current children cumulated CPU time (s) 359.56
Current children cumulated vsize (Kb) 25360

[startup+370.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 20607 0 0 0 36881 76 0 0 25 0 1 0 1855116967 23793664 5319 4294967295 134512640 135094434 3221224432 3221220320 134677021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5809 5319 145 145 0 5664 0
[pid=28308] vsize: 23236
Current children cumulated CPU time (s) 369.57
Current children cumulated vsize (Kb) 25360

[startup+380.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 20607 0 0 0 37881 76 0 0 25 0 1 0 1855116967 23793664 5319 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5809 5319 145 145 0 5664 0
[pid=28308] vsize: 23236
Current children cumulated CPU time (s) 379.57
Current children cumulated vsize (Kb) 25360

[startup+390.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 20607 0 0 0 38881 76 0 0 25 0 1 0 1855116967 23793664 5319 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5809 5319 145 145 0 5664 0
[pid=28308] vsize: 23236
Current children cumulated CPU time (s) 389.57
Current children cumulated vsize (Kb) 25360

[startup+400.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 20607 0 0 0 39881 76 0 0 25 0 1 0 1855116967 23793664 5319 4294967295 134512640 135094434 3221224432 3221221200 134677065 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5809 5319 145 145 0 5664 0
[pid=28308] vsize: 23236
Current children cumulated CPU time (s) 399.57
Current children cumulated vsize (Kb) 25360

[startup+410.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 20607 0 0 0 40881 76 0 0 25 0 1 0 1855116967 23793664 5319 4294967295 134512640 135094434 3221224432 3221220912 134600246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5809 5319 145 145 0 5664 0
[pid=28308] vsize: 23236
Current children cumulated CPU time (s) 409.57
Current children cumulated vsize (Kb) 25360

[startup+420.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 20607 0 0 0 41882 76 0 0 25 0 1 0 1855116967 23793664 5319 4294967295 134512640 135094434 3221224432 3221221952 134677147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5809 5319 145 145 0 5664 0
[pid=28308] vsize: 23236
Current children cumulated CPU time (s) 419.58
Current children cumulated vsize (Kb) 25360

[startup+430.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 39574 0 0 0 42757 146 0 0 25 0 1 0 1855116967 23773184 5314 4294967295 134512640 135094434 3221224432 3221220048 134600186 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5804 5314 145 145 0 5659 0
[pid=28308] vsize: 23216
Current children cumulated CPU time (s) 429.03
Current children cumulated vsize (Kb) 25340

[startup+440.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 39574 0 0 0 43758 146 0 0 25 0 1 0 1855116967 23773184 5314 4294967295 134512640 135094434 3221224432 3221220224 134677327 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5804 5314 145 145 0 5659 0
[pid=28308] vsize: 23216
Current children cumulated CPU time (s) 439.04
Current children cumulated vsize (Kb) 25340

[startup+450.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 39574 0 0 0 44758 146 0 0 25 0 1 0 1855116967 23773184 5314 4294967295 134512640 135094434 3221224432 3221221024 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5804 5314 145 145 0 5659 0
[pid=28308] vsize: 23216
Current children cumulated CPU time (s) 449.04
Current children cumulated vsize (Kb) 25340

[startup+460.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 39574 0 0 0 45758 146 0 0 25 0 1 0 1855116967 23773184 5314 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5804 5314 145 145 0 5659 0
[pid=28308] vsize: 23216
Current children cumulated CPU time (s) 459.04
Current children cumulated vsize (Kb) 25340

[startup+470.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) T 28304 28304 2660 0 -1 0 43412 0 0 0 46739 158 0 0 24 0 1 0 1855116967 33701888 7738 4294967295 134512640 135094434 3221224432 3221208252 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/28308/statm): 8228 7738 145 145 0 8083 0
[pid=28308] vsize: 32912
Current children cumulated CPU time (s) 468.97
Current children cumulated vsize (Kb) 35036

[startup+480.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 58871 0 0 0 47635 217 0 0 25 0 1 0 1855116967 23715840 5300 4294967295 134512640 135094434 3221224432 3221220576 134600301 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5790 5300 145 145 0 5645 0
[pid=28308] vsize: 23160
Current children cumulated CPU time (s) 478.52
Current children cumulated vsize (Kb) 25284

[startup+490.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 58871 0 0 0 48635 217 0 0 25 0 1 0 1855116967 23715840 5300 4294967295 134512640 135094434 3221224432 3221220048 134601016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5790 5300 145 145 0 5645 0
[pid=28308] vsize: 23160
Current children cumulated CPU time (s) 488.52
Current children cumulated vsize (Kb) 25284

[startup+500.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 58871 0 0 0 49635 217 0 0 25 0 1 0 1855116967 23715840 5300 4294967295 134512640 135094434 3221224432 3221221876 134676335 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5790 5300 145 145 0 5645 0
[pid=28308] vsize: 23160
Current children cumulated CPU time (s) 498.52
Current children cumulated vsize (Kb) 25284

[startup+510.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 58871 0 0 0 50636 217 0 0 25 0 1 0 1855116967 23715840 5300 4294967295 134512640 135094434 3221224432 3221220400 134677290 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5790 5300 145 145 0 5645 0
[pid=28308] vsize: 23160
Current children cumulated CPU time (s) 508.53
Current children cumulated vsize (Kb) 25284

[startup+520.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 59675 0 0 0 51632 219 0 0 25 0 1 0 1855116967 23785472 5317 4294967295 134512640 135094434 3221224432 3221220576 134677366 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28308/statm): 5807 5317 145 145 0 5662 0
[pid=28308] vsize: 23228
Current children cumulated CPU time (s) 518.51
Current children cumulated vsize (Kb) 25352

[startup+530.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 59675 0 0 0 52632 219 0 0 25 0 1 0 1855116967 23785472 5317 4294967295 134512640 135094434 3221224432 3221220928 134676510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5807 5317 145 145 0 5662 0
[pid=28308] vsize: 23228
Current children cumulated CPU time (s) 528.51
Current children cumulated vsize (Kb) 25352

[startup+540.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 66033 0 0 0 53597 239 0 0 25 0 1 0 1855116967 23805952 5322 4294967295 134512640 135094434 3221224432 3221221280 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5812 5322 145 145 0 5667 0
[pid=28308] vsize: 23248
Current children cumulated CPU time (s) 538.36
Current children cumulated vsize (Kb) 25372

[startup+550.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 66141 0 0 0 54597 240 0 0 25 0 1 0 1855116967 23805952 5430 4294967295 134512640 135094434 3221224432 3221220648 134677084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5812 5430 145 145 0 5667 0
[pid=28308] vsize: 23248
Current children cumulated CPU time (s) 548.37
Current children cumulated vsize (Kb) 25372

[startup+560.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 66141 0 0 0 55597 240 0 0 25 0 1 0 1855116967 23805952 5430 4294967295 134512640 135094434 3221224432 3221221104 134677248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5812 5430 145 145 0 5667 0
[pid=28308] vsize: 23248
Current children cumulated CPU time (s) 558.37
Current children cumulated vsize (Kb) 25372

[startup+570.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 66141 0 0 0 56598 240 0 0 25 0 1 0 1855116967 23805952 5430 4294967295 134512640 135094434 3221224432 3221221176 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5812 5430 145 145 0 5667 0
[pid=28308] vsize: 23248
Current children cumulated CPU time (s) 568.38
Current children cumulated vsize (Kb) 25372

[startup+580.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 66141 0 0 0 57598 240 0 0 25 0 1 0 1855116967 23805952 5430 4294967295 134512640 135094434 3221224432 3221221512 134676609 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5812 5430 145 145 0 5667 0
[pid=28308] vsize: 23248
Current children cumulated CPU time (s) 578.38
Current children cumulated vsize (Kb) 25372

[startup+590.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 66141 0 0 0 58598 240 0 0 25 0 1 0 1855116967 23805952 5430 4294967295 134512640 135094434 3221224432 3221222160 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5812 5430 145 145 0 5667 0
[pid=28308] vsize: 23248
Current children cumulated CPU time (s) 588.38
Current children cumulated vsize (Kb) 25372

[startup+600.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 66141 0 0 0 59598 240 0 0 25 0 1 0 1855116967 23805952 5430 4294967295 134512640 135094434 3221224432 3221222392 134676609 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 5812 5430 145 145 0 5667 0
[pid=28308] vsize: 23248
Current children cumulated CPU time (s) 598.38
Current children cumulated vsize (Kb) 25372

[startup+610.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 68325 0 0 0 60592 246 0 0 25 0 1 0 1855116967 29560832 6396 4294967295 134512640 135094434 3221224432 3221221156 134676608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7217 6396 145 145 0 7072 0
[pid=28308] vsize: 28868
Current children cumulated CPU time (s) 608.38
Current children cumulated vsize (Kb) 30992

[startup+620.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 68325 0 0 0 61592 246 0 0 25 0 1 0 1855116967 29560832 6396 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7217 6396 145 145 0 7072 0
[pid=28308] vsize: 28868
Current children cumulated CPU time (s) 618.38
Current children cumulated vsize (Kb) 30992

[startup+630.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 68325 0 0 0 62592 246 0 0 25 0 1 0 1855116967 29560832 6396 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7217 6396 145 145 0 7072 0
[pid=28308] vsize: 28868
Current children cumulated CPU time (s) 628.38
Current children cumulated vsize (Kb) 30992

[startup+640.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 68325 0 0 0 63592 246 0 0 25 0 1 0 1855116967 29560832 6396 4294967295 134512640 135094434 3221224432 3221221800 134600234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7217 6396 145 145 0 7072 0
[pid=28308] vsize: 28868
Current children cumulated CPU time (s) 638.38
Current children cumulated vsize (Kb) 30992

[startup+650.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 68325 0 0 0 64592 246 0 0 25 0 1 0 1855116967 29560832 6396 4294967295 134512640 135094434 3221224432 3221221984 134677346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7217 6396 145 145 0 7072 0
[pid=28308] vsize: 28868
Current children cumulated CPU time (s) 648.38
Current children cumulated vsize (Kb) 30992

[startup+660.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 68938 0 0 0 65590 248 0 0 25 0 1 0 1855116967 29569024 6418 4294967295 134512640 135094434 3221224432 3221221084 134677150 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7219 6418 145 145 0 7074 0
[pid=28308] vsize: 28876
Current children cumulated CPU time (s) 658.38
Current children cumulated vsize (Kb) 31000

[startup+670.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 68938 0 0 0 66590 248 0 0 25 0 1 0 1855116967 29569024 6418 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7219 6418 145 145 0 7074 0
[pid=28308] vsize: 28876
Current children cumulated CPU time (s) 668.38
Current children cumulated vsize (Kb) 31000

[startup+680.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 68938 0 0 0 67591 248 0 0 25 0 1 0 1855116967 29569024 6418 4294967295 134512640 135094434 3221224432 3221221456 134676516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7219 6418 145 145 0 7074 0
[pid=28308] vsize: 28876
Current children cumulated CPU time (s) 678.39
Current children cumulated vsize (Kb) 31000

[startup+690.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 68938 0 0 0 68590 248 0 0 25 0 1 0 1855116967 29569024 6418 4294967295 134512640 135094434 3221224432 3221221808 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7219 6418 145 145 0 7074 0
[pid=28308] vsize: 28876
Current children cumulated CPU time (s) 688.38
Current children cumulated vsize (Kb) 31000

[startup+700.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 68938 0 0 0 69591 248 0 0 25 0 1 0 1855116967 29569024 6418 4294967295 134512640 135094434 3221224432 3221221984 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7219 6418 145 145 0 7074 0
[pid=28308] vsize: 28876
Current children cumulated CPU time (s) 698.39
Current children cumulated vsize (Kb) 31000

[startup+710.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) T 28304 28304 2660 0 -1 0 72942 0 0 0 70568 261 0 0 25 0 1 0 1855116967 41160704 9268 4294967295 134512640 135094434 3221224432 3221160204 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/28308/statm): 10049 9268 145 145 0 9904 0
[pid=28308] vsize: 40196
Current children cumulated CPU time (s) 708.29
Current children cumulated vsize (Kb) 42320

[startup+720.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 71565 264 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221219696 134677248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 718.29
Current children cumulated vsize (Kb) 30980

[startup+730.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 72565 264 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221219520 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 728.29
Current children cumulated vsize (Kb) 30980

[startup+740.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 73564 264 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221219520 134600274 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 738.28
Current children cumulated vsize (Kb) 30980

[startup+750.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 74564 265 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221219616 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 748.29
Current children cumulated vsize (Kb) 30980

[startup+760.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 75564 265 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221220108 134677378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 758.29
Current children cumulated vsize (Kb) 30980

[startup+770.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 76565 265 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221220096 134677233 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 768.3
Current children cumulated vsize (Kb) 30980

[startup+780.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 77564 265 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221219520 134677271 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 778.29
Current children cumulated vsize (Kb) 30980

[startup+790.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 78565 265 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221219872 134600008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 788.3
Current children cumulated vsize (Kb) 30980

[startup+800.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 79565 266 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221220400 134600254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 798.31
Current children cumulated vsize (Kb) 30980

[startup+810.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 80565 266 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221219764 134677085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 808.31
Current children cumulated vsize (Kb) 30980

[startup+820.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 81565 266 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221219792 134676280 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 818.31
Current children cumulated vsize (Kb) 30980

[startup+830.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 82565 266 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221220296 134677084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 828.31
Current children cumulated vsize (Kb) 30980

[startup+840.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 83565 266 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221220128 134676328 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 838.31
Current children cumulated vsize (Kb) 30980

[startup+850.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 84565 266 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 848.31
Current children cumulated vsize (Kb) 30980

[startup+860.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 85565 266 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221220576 134677346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 858.31
Current children cumulated vsize (Kb) 30980

[startup+870.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 86566 266 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221220496 134676259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 868.32
Current children cumulated vsize (Kb) 30980

[startup+880.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 87566 266 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 878.32
Current children cumulated vsize (Kb) 30980

[startup+890.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 88566 266 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 888.32
Current children cumulated vsize (Kb) 30980

[startup+900.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 89566 267 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221221104 134676601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 898.33
Current children cumulated vsize (Kb) 30980

[startup+910.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 90566 267 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221220648 134677084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 908.33
Current children cumulated vsize (Kb) 30980

[startup+920.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 91566 267 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 918.33
Current children cumulated vsize (Kb) 30980

[startup+930.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 92567 267 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 928.34
Current children cumulated vsize (Kb) 30980

[startup+940.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 93567 267 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221221080 134600694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 938.34
Current children cumulated vsize (Kb) 30980

[startup+950.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 94567 267 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221220752 134677366 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 948.34
Current children cumulated vsize (Kb) 30980

[startup+960.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 95567 267 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221220928 134601029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 958.34
Current children cumulated vsize (Kb) 30980

[startup+970.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 96567 267 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221220848 134676311 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 968.34
Current children cumulated vsize (Kb) 30980

[startup+980.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 97567 267 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221220496 134676251 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 978.34
Current children cumulated vsize (Kb) 30980

[startup+990.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 98568 267 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221220928 134677351 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 988.35
Current children cumulated vsize (Kb) 30980

[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 99568 267 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 998.35
Current children cumulated vsize (Kb) 30980

[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 100568 267 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221221328 134677375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 1008.35
Current children cumulated vsize (Kb) 30980

[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 101568 267 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221221000 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 1018.35
Current children cumulated vsize (Kb) 30980

[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 102568 267 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 1028.35
Current children cumulated vsize (Kb) 30980

[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 103569 267 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221221176 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 1038.36
Current children cumulated vsize (Kb) 30980

[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 104569 267 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221221808 134677239 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 1048.36
Current children cumulated vsize (Kb) 30980

[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 105569 267 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221220928 134677346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 1058.36
Current children cumulated vsize (Kb) 30980

[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 106569 267 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221221268 134600238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 1068.36
Current children cumulated vsize (Kb) 30980

[startup+1080.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 107569 267 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221221456 134600204 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 1078.36
Current children cumulated vsize (Kb) 30980

[startup+1090.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 108570 267 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221220988 134676460 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 1088.37
Current children cumulated vsize (Kb) 30980

[startup+1100.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 109570 267 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221221104 134676589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 1098.37
Current children cumulated vsize (Kb) 30980

[startup+1110.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 110570 267 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221221248 134676245 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 1108.37
Current children cumulated vsize (Kb) 30980

[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 111570 267 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 1118.37
Current children cumulated vsize (Kb) 30980

[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 112570 268 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221221520 134677091 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 1128.38
Current children cumulated vsize (Kb) 30980

[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 113571 268 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 1138.39
Current children cumulated vsize (Kb) 30980

[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 114571 268 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221220648 134677084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 1148.39
Current children cumulated vsize (Kb) 30980

[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 115571 268 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 1158.39
Current children cumulated vsize (Kb) 30980

[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 116571 268 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221221104 134676589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 1168.39
Current children cumulated vsize (Kb) 30980

[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 117572 268 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 1178.4
Current children cumulated vsize (Kb) 30980

[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 118572 268 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 1188.4
Current children cumulated vsize (Kb) 30980

[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 119572 268 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 1198.4
Current children cumulated vsize (Kb) 30980

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 120572 268 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221222132 134676244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 1208.4
Current children cumulated vsize (Kb) 30980



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 28308
Raw data (/proc/28304/stat): 28304 (minisat+_script) S 28303 28304 2660 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116962 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28304/statm): 531 226 485 147 0 384 0
[pid=28304] vsize: 2124
Raw data (/proc/28308/stat): 28308 (minisat+_64-bit) R 28304 28304 2660 0 -1 0 73089 0 0 0 120572 268 0 0 25 0 1 0 1855116967 29548544 6433 4294967295 134512640 135094434 3221224432 3221222256 134677007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28308/statm): 7214 6433 145 145 0 7069 0
[pid=28308] vsize: 28856
Current children cumulated CPU time (s) 1208.4
Current children cumulated vsize (Kb) 30980

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

Child status: 0
Real time (s): 1210.09
CPU time (s): 1208.42
CPU user time (s): 1205.73
CPU system time (s): 2.69759
CPU usage (%): 99.8622
Max. virtual memory (cumulated for all children) (Kb): 42320

Verifier Data

ERROR: no interpretation found !