Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-fixnet3.opb
MD5SUM349f4f626fe64dc0e2f8461de6820c95
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 563784272
Optimality of the best value was proved NO
Number of terms in the objective function 13946
Biggest coefficient in the objective function 53687091200
Number of bits for the biggest coefficient in the objective function 36
Sum of the numbers in the objective function 23716479945956
Number of bits of the sum of numbers in the objective function 45
Biggest number in a constraint 53687091200
Number of bits of the biggest number in a constraint 36
Biggest sum of numbers in a constraint 23716479945956
Number of bits of the biggest sum of numbers45
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1242.41
Number of variables14036
Total number of constraints978
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)378
Number of constraints which are nor clauses,nor cardinality constraints600
Minimum length of a constraint1
Maximum length of a constraint1523

Trace number 3853

Launcher Data

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        912088 kB
Buffers:         34736 kB
Cached:          60560 kB
SwapCached:        516 kB
Active:          57788 kB
Inactive:        39936 kB
HighTotal:      131008 kB
HighFree:        66472 kB
LowTotal:       903652 kB
LowFree:        845616 kB
SwapTotal:     2097892 kB
SwapFree:      2096672 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5680 kB
Slab:            19036 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 03:26:01 (client local time) WITH STATUS 0 IN 1207.77 SECONDS
stats: 2853 7 1207.77 0

Solver Data

c Parsing PB file...
c Converting 700 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssss
c ---[ 593]---> Sorter-cost:  572     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 591]---> Adder-cost: 1136   maxlim: 3938265   bits: 23/22
c ---[ 589]---> Sorter-cost: 2802     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 587]---> Adder-cost: 1356   maxlim: 2449365   bits: 23/22
c ---[ 585]---> Adder-cost: 674   maxlim: 1730540   bits: 22/21
c ---[ 583]---> Adder-cost: 1210   maxlim: 3473369   bits: 23/22
c ---[ 581]---> Adder-cost: 638   maxlim: 2177010   bits: 23/22
c ---[ 579]---> Adder-cost: 1040   maxlim: 2314209   bits: 23/22
c ---[ 577]---> Adder-cost: 776   maxlim: 2775017   bits: 23/22
c ---[ 575]---> Adder-cost: 1090   maxlim: 2873312   bits: 23/22
c ---[ 573]---> Adder-cost: 825   maxlim: 1757161   bits: 22/21
c ---[ 571]---> Adder-cost: 420   maxlim: 600056   bits: 21/20
c ---[ 569]---> Adder-cost: 1624   maxlim: 5140428   bits: 23/23
c ---[ 567]---> Adder-cost: 644   maxlim: 2281451   bits: 22/22
c ---[ 565]---> Adder-cost: 645   maxlim: 1726447   bits: 22/21
c ---[ 563]---> Adder-cost: 582   maxlim: 1734640   bits: 22/21
c ---[ 561]---> Sorter-cost: 1992     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 559]---> Adder-cost: 1536   maxlim: 6610898   bits: 24/23
c ---[ 557]---> Adder-cost: 1458   maxlim: 4601807   bits: 23/23
c ---[ 555]---> Adder-cost: 486   maxlim: 638964   bits: 21/20
c ---[ 553]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 551]---> Sorter-cost:  471     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 549]---> Sorter-cost: 1032     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 547]---> Sorter-cost:  687     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 545]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 543]---> Sorter-cost:  275     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 541]---> Sorter-cost:  252     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 539]---> Sorter-cost: 1290     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 537]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 535]---> Sorter-cost: 1448     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 533]---> Sorter-cost: 1071     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 531]---> Sorter-cost: 1031     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 529]---> Sorter-cost:  299     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 527]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 525]---> Sorter-cost: 1290     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 523]---> Sorter-cost: 1291     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 521]---> Sorter-cost:  471     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 519]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 517]---> Sorter-cost:  884     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 515]---> Sorter-cost: 1289     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 513]---> Sorter-cost: 2119     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 511]---> Sorter-cost: 1033     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 509]---> Sorter-cost:  275     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 507]---> Sorter-cost: 1071     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 505]---> Sorter-cost: 1033     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 503]---> Sorter-cost:  469     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 501]---> Sorter-cost:  754     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 499]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 497]---> Sorter-cost:  945     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 495]---> Sorter-cost:  820     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 493]---> Sorter-cost:  469     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 491]---> Sorter-cost:  471     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 489]---> Sorter-cost:  431     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 487]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 485]---> Sorter-cost:  471     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 483]---> Sorter-cost: 1071     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 481]---> Sorter-cost:  752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 479]---> Sorter-cost: 1033     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 477]---> Sorter-cost:  882     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 475]---> Sorter-cost:  300     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 473]---> Sorter-cost:  471     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 471]---> Sorter-cost: 1716     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 469]---> Sorter-cost:  817     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 467]---> Sorter-cost: 1289     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 465]---> Sorter-cost: 1291     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 463]---> Sorter-cost: 1121     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 461]---> Sorter-cost:  818     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 459]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 457]---> Sorter-cost:  754     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 455]---> Sorter-cost: 1031     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 453]---> Sorter-cost:  819     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 451]---> Sorter-cost:  275     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 449]---> Sorter-cost: 1118     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 447]---> Sorter-cost:  470     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 445]---> Sorter-cost:  470     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 443]---> Sorter-cost:  470     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 441]---> BDD-cost:   55
c ---[ 439]---> Sorter-cost:  857     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 437]---> Sorter-cost:  469     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 435]---> Sorter-cost:  687     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 433]---> Sorter-cost: 2726     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 431]---> Sorter-cost:  857     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 429]---> Sorter-cost:  471     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 427]---> Sorter-cost:  471     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 425]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 423]---> Sorter-cost: 1033     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 421]---> Sorter-cost:  945     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 419]---> Sorter-cost: 1291     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 417]---> Sorter-cost:  431     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 415]---> Sorter-cost: 1031     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 413]---> Sorter-cost:  471     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 411]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 409]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 407]---> Sorter-cost: 1032     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 405]---> Sorter-cost: 1033     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 403]---> Sorter-cost:  817     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 401]---> Sorter-cost:  622     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 399]---> Sorter-cost: 1291     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 397]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 395]---> Sorter-cost:  753     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 394]---> BDD-cost:   26
c ---[ 393]---> BDD-cost:   26
c ---[ 392]---> BDD-cost:   11
c ---[ 391]---> BDD-cost:   26
c ---[ 390]---> BDD-cost:   26
c ---[ 389]---> BDD-cost:   26
c ---[ 388]---> BDD-cost:   26
c ---[ 387]---> BDD-cost:   26
c ---[ 386]---> BDD-cost:   12
c ---[ 385]---> BDD-cost:   13
c ---[ 384]---> BDD-cost:   13
c ---[ 383]---> BDD-cost:   13
c ---[ 382]---> BDD-cost:   11
c ---[ 381]---> BDD-cost:   13
c ---[ 380]---> BDD-cost:   13
c ---[ 379]---> BDD-cost:   13
c ---[ 378]---> BDD-cost:   13
c ---[ 377]---> BDD-cost:   14
c ---[ 376]---> BDD-cost:   14
c ---[ 375]---> BDD-cost:   14
c ---[ 374]---> BDD-cost:   13
c ---[ 373]---> BDD-cost:   11
c ---[ 372]---> BDD-cost:   12
c ---[ 371]---> BDD-cost:   13
c ---[ 370]---> BDD-cost:   12
c ---[ 369]---> BDD-cost:   13
c ---[ 368]---> BDD-cost:   26
c ---[ 367]---> BDD-cost:   26
c ---[ 366]---> BDD-cost:   13
c ---[ 365]---> BDD-cost:   15
c ---[ 364]---> BDD-cost:   14
c ---[ 363]---> BDD-cost:   14
c ---[ 362]---> BDD-cost:   26
c ---[ 361]---> BDD-cost:   26
c ---[ 360]---> BDD-cost:   26
c ---[ 359]---> BDD-cost:   13
c ---[ 358]---> BDD-cost:   14
c ---[ 357]---> BDD-cost:   12
c ---[ 356]---> BDD-cost:   13
c ---[ 355]---> BDD-cost:   13
c ---[ 354]---> BDD-cost:   13
c ---[ 353]---> BDD-cost:   11
c ---[ 352]---> BDD-cost:   13
c ---[ 351]---> BDD-cost:   13
c ---[ 350]---> BDD-cost:   13
c ---[ 349]---> BDD-cost:   14
c ---[ 348]---> BDD-cost:   11
c ---[ 347]---> BDD-cost:   13
c ---[ 346]---> BDD-cost:   13
c ---[ 345]---> BDD-cost:   12
c ---[ 344]---> BDD-cost:   14
c ---[ 343]---> BDD-cost:   14
c ---[ 342]---> BDD-cost:   11
c ---[ 341]---> BDD-cost:   13
c ---[ 340]---> BDD-cost:   14
c ---[ 339]---> BDD-cost:   13
c ---[ 338]---> BDD-cost:   13
c ---[ 337]---> BDD-cost:   13
c ---[ 336]---> BDD-cost:   13
c ---[ 335]---> BDD-cost:   14
c ---[ 334]---> BDD-cost:   11
c ---[ 333]---> BDD-cost:   13
c ---[ 332]---> BDD-cost:   26
c ---[ 331]---> BDD-cost:   26
c ---[ 330]---> BDD-cost:   12
c ---[ 329]---> BDD-cost:   12
c ---[ 328]---> BDD-cost:   12
c ---[ 327]---> BDD-cost:   14
c ---[ 326]---> BDD-cost:   13
c ---[ 325]---> BDD-cost:   15
c ---[ 324]---> BDD-cost:   13
c ---[ 323]---> BDD-cost:   11
c ---[ 322]---> BDD-cost:   13
c ---[ 321]---> BDD-cost:   13
c ---[ 320]---> BDD-cost:   14
c ---[ 319]---> BDD-cost:   14
c ---[ 318]---> BDD-cost:   13
c ---[ 317]---> BDD-cost:   13
c ---[ 316]---> BDD-cost:   26
c ---[ 315]---> BDD-cost:   26
c ---[ 314]---> BDD-cost:   26
c ---[ 313]---> BDD-cost:   26
c ---[ 312]---> BDD-cost:   13
c ---[ 311]---> BDD-cost:   12
c ---[ 310]---> BDD-cost:   13
c ---[ 309]---> BDD-cost:   13
c ---[ 308]---> BDD-cost:   13
c ---[ 307]---> BDD-cost:   13
c ---[ 306]---> BDD-cost:   13
c ---[ 305]---> BDD-cost:   13
c ---[ 304]---> BDD-cost:   12
c ---[ 303]---> BDD-cost:   13
c ---[ 302]---> BDD-cost:   13
c ---[ 301]---> BDD-cost:   14
c ---[ 300]---> BDD-cost:   13
c ---[ 299]---> BDD-cost:   13
c ---[ 298]---> BDD-cost:   14
c ---[ 297]---> BDD-cost:   11
c ---[ 296]---> BDD-cost:   14
c ---[ 295]---> BDD-cost:   12
c ---[ 294]---> BDD-cost:   13
c ---[ 293]---> BDD-cost:   13
c ---[ 292]---> BDD-cost:   13
c ---[ 291]---> BDD-cost:   13
c ---[ 290]---> BDD-cost:   26
c ---[ 289]---> BDD-cost:   26
c ---[ 288]---> BDD-cost:   14
c ---[ 287]---> BDD-cost:   11
c ---[ 286]---> BDD-cost:   14
c ---[ 285]---> BDD-cost:   12
c ---[ 284]---> BDD-cost:   13
c ---[ 283]---> BDD-cost:   13
c ---[ 282]---> BDD-cost:   11
c ---[ 281]---> BDD-cost:   11
c ---[ 280]---> BDD-cost:   26
c ---[ 279]---> BDD-cost:   26
c ---[ 278]---> BDD-cost:   26
c ---[ 277]---> BDD-cost:   26
c ---[ 276]---> BDD-cost:   14
c ---[ 275]---> BDD-cost:   14
c ---[ 274]---> BDD-cost:   12
c ---[ 273]---> BDD-cost:   13
c ---[ 272]---> BDD-cost:   13
c ---[ 271]---> BDD-cost:   13
c ---[ 270]---> BDD-cost:   13
c ---[ 269]---> BDD-cost:   13
c ---[ 268]---> BDD-cost:   13
c ---[ 267]---> BDD-cost:   12
c ---[ 266]---> BDD-cost:   13
c ---[ 265]---> BDD-cost:   13
c ---[ 264]---> BDD-cost:   12
c ---[ 263]---> BDD-cost:   13
c ---[ 262]---> BDD-cost:   12
c ---[ 261]---> BDD-cost:   11
c ---[ 260]---> BDD-cost:   13
c ---[ 259]---> BDD-cost:   12
c ---[ 258]---> BDD-cost:   11
c ---[ 257]---> BDD-cost:   26
c ---[ 256]---> BDD-cost:   26
c ---[ 255]---> BDD-cost:   26
c ---[ 254]---> BDD-cost:   26
c ---[ 253]---> BDD-cost:   13
c ---[ 252]---> BDD-cost:   13
c ---[ 251]---> BDD-cost:   13
c ---[ 250]---> BDD-cost:   11
c ---[ 249]---> BDD-cost:   13
c ---[ 248]---> BDD-cost:   12
c ---[ 247]---> BDD-cost:   11
c ---[ 246]---> BDD-cost:   14
c ---[ 245]---> BDD-cost:   14
c ---[ 244]---> BDD-cost:   13
c ---[ 243]---> BDD-cost:   11
c ---[ 242]---> BDD-cost:   13
c ---[ 241]---> BDD-cost:   14
c ---[ 240]---> BDD-cost:   13
c ---[ 239]---> BDD-cost:   26
c ---[ 238]---> BDD-cost:   26
c ---[ 237]---> BDD-cost:   26
c ---[ 236]---> BDD-cost:   26
c ---[ 235]---> BDD-cost:   26
c ---[ 234]---> BDD-cost:   13
c ---[ 233]---> BDD-cost:   12
c ---[ 232]---> BDD-cost:   14
c ---[ 231]---> BDD-cost:   13
c ---[ 230]---> BDD-cost:   14
c ---[ 229]---> BDD-cost:   14
c ---[ 228]---> BDD-cost:   13
c ---[ 227]---> BDD-cost:   13
c ---[ 226]---> BDD-cost:   13
c ---[ 225]---> BDD-cost:   13
c ---[ 224]---> BDD-cost:   13
c ---[ 223]---> BDD-cost:   14
c ---[ 222]---> BDD-cost:   14
c ---[ 221]---> BDD-cost:   13
c ---[ 220]---> BDD-cost:   13
c ---[ 219]---> BDD-cost:   13
c ---[ 218]---> BDD-cost:   14
c ---[ 217]---> BDD-cost:   12
c ---[ 216]---> BDD-cost:   13
c ---[ 215]---> BDD-cost:   13
c ---[ 214]---> BDD-cost:   26
c ---[ 213]---> BDD-cost:   26
c ---[ 212]---> BDD-cost:   26
c ---[ 211]---> BDD-cost:   14
c ---[ 210]---> BDD-cost:   13
c ---[ 209]---> BDD-cost:   12
c ---[ 208]---> BDD-cost:   11
c ---[ 207]---> BDD-cost:   13
c ---[ 206]---> BDD-cost:   13
c ---[ 205]---> BDD-cost:   12
c ---[ 204]---> BDD-cost:   13
c ---[ 203]---> BDD-cost:   14
c ---[ 202]---> BDD-cost:   13
c ---[ 201]---> BDD-cost:   13
c ---[ 200]---> BDD-cost:   12
c ---[ 199]---> BDD-cost:   12
c ---[ 198]---> BDD-cost:   12
c ---[ 197]---> BDD-cost:   13
c ---[ 196]---> BDD-cost:   26
c ---[ 195]---> BDD-cost:   14
c ---[ 194]---> BDD-cost:   11
c ---[ 193]---> BDD-cost:   12
c ---[ 192]---> BDD-cost:   15
c ---[ 191]---> BDD-cost:   13
c ---[ 190]---> BDD-cost:   13
c ---[ 189]---> BDD-cost:   26
c ---[ 188]---> BDD-cost:   26
c ---[ 187]---> BDD-cost:   26
c ---[ 186]---> BDD-cost:   26
c ---[ 185]---> BDD-cost:   26
c ---[ 184]---> BDD-cost:   26
c ---[ 183]---> BDD-cost:   13
c ---[ 182]---> BDD-cost:   13
c ---[ 181]---> BDD-cost:   11
c ---[ 180]---> BDD-cost:   14
c ---[ 179]---> BDD-cost:   13
c ---[ 178]---> BDD-cost:   13
c ---[ 177]---> BDD-cost:   13
c ---[ 176]---> BDD-cost:   11
c ---[ 175]---> BDD-cost:   14
c ---[ 174]---> BDD-cost:   12
c ---[ 173]---> BDD-cost:   13
c ---[ 172]---> BDD-cost:   11
c ---[ 171]---> BDD-cost:   13
c ---[ 170]---> BDD-cost:   13
c ---[ 169]---> BDD-cost:   14
c ---[ 168]---> BDD-cost:   14
c ---[ 167]---> BDD-cost:   13
c ---[ 166]---> BDD-cost:   14
c ---[ 165]---> BDD-cost:   14
c ---[ 164]---> BDD-cost:   13
c ---[ 163]---> BDD-cost:   13
c ---[ 162]---> BDD-cost:   13
c ---[ 161]---> BDD-cost:   13
c ---[ 160]---> BDD-cost:   13
c ---[ 159]---> BDD-cost:   14
c ---[ 158]---> BDD-cost:   13
c ---[ 157]---> BDD-cost:   14
c ---[ 156]---> BDD-cost:   13
c ---[ 155]---> BDD-cost:   13
c ---[ 154]---> BDD-cost:   14
c ---[ 153]---> BDD-cost:   11
c ---[ 152]---> BDD-cost:   26
c ---[ 151]---> BDD-cost:   26
c ---[ 150]---> BDD-cost:   26
c ---[ 149]---> BDD-cost:   13
c ---[ 148]---> BDD-cost:   11
c ---[ 147]---> BDD-cost:   13
c ---[ 146]---> BDD-cost:   14
c ---[ 145]---> BDD-cost:   14
c ---[ 144]---> BDD-cost:   15
c ---[ 143]---> BDD-cost:   13
c ---[ 142]---> BDD-cost:   13
c ---[ 141]---> BDD-cost:   14
c ---[ 140]---> BDD-cost:   14
c ---[ 139]---> BDD-cost:   13
c ---[ 138]---> BDD-cost:   13
c ---[ 137]---> BDD-cost:   11
c ---[ 136]---> BDD-cost:   12
c ---[ 135]---> BDD-cost:   14
c ---[ 134]---> BDD-cost:   13
c ---[ 133]---> BDD-cost:   26
c ---[ 132]---> BDD-cost:   26
c ---[ 131]---> BDD-cost:   26
c ---[ 130]---> BDD-cost:   12
c ---[ 129]---> BDD-cost:   13
c ---[ 128]---> BDD-cost:   15
c ---[ 127]---> BDD-cost:   11
c ---[ 126]---> BDD-cost:   13
c ---[ 125]---> BDD-cost:   13
c ---[ 124]---> BDD-cost:   14
c ---[ 123]---> BDD-cost:   12
c ---[ 122]---> BDD-cost:   14
c ---[ 121]---> BDD-cost:   14
c ---[ 120]---> BDD-cost:   14
c ---[ 119]---> BDD-cost:   12
c ---[ 118]---> BDD-cost:   26
c ---[ 117]---> BDD-cost:   26
c ---[ 116]---> BDD-cost:   26
c ---[ 115]---> BDD-cost:   13
c ---[ 114]---> BDD-cost:   13
c ---[ 113]---> BDD-cost:   14
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   15
c ---[ 110]---> BDD-cost:   14
c ---[ 109]---> BDD-cost:   13
c ---[ 108]---> BDD-cost:   14
c ---[ 107]---> BDD-cost:   13
c ---[ 106]---> BDD-cost:   12
c ---[ 105]---> BDD-cost:   14
c ---[ 104]---> BDD-cost:   26
c ---[ 103]---> BDD-cost:   12
c ---[ 102]---> BDD-cost:   14
c ---[ 101]---> BDD-cost:   13
c ---[ 100]---> BDD-cost:   26
c ---[  99]---> BDD-cost:   26
c ---[  98]---> BDD-cost:   26
c ---[  97]---> BDD-cost:   26
c ---[  96]---> BDD-cost:   26
c ---[  95]---> BDD-cost:   26
c ---[  94]---> BDD-cost:   26
c ---[  93]---> BDD-cost:   26
c ---[  92]---> BDD-cost:   26
c ---[  91]---> BDD-cost:   26
c ---[  90]---> BDD-cost:   12
c ---[  89]---> BDD-cost:   14
c ---[  88]---> BDD-cost:   12
c ---[  87]---> BDD-cost:   13
c ---[  86]---> BDD-cost:   14
c ---[  85]---> BDD-cost:   13
c ---[  84]---> BDD-cost:   12
c ---[  83]---> BDD-cost:   13
c ---[  82]---> BDD-cost:   13
c ---[  81]---> BDD-cost:   13
c ---[  80]---> BDD-cost:   13
c ---[  79]---> BDD-cost:   13
c ---[  78]---> BDD-cost:   12
c ---[  77]---> BDD-cost:   11
c ---[  76]---> BDD-cost:   13
c ---[  75]---> BDD-cost:   15
c ---[  74]---> BDD-cost:   14
c ---[  73]---> BDD-cost:   13
c ---[  72]---> BDD-cost:   14
c ---[  71]---> BDD-cost:   12
c ---[  70]---> BDD-cost:   13
c ---[  69]---> BDD-cost:   12
c ---[  68]---> BDD-cost:   14
c ---[  67]---> BDD-cost:   14
c ---[  66]---> BDD-cost:   13
c ---[  65]---> BDD-cost:   13
c ---[  64]---> BDD-cost:   12
c ---[  63]---> BDD-cost:   26
c ---[  62]---> BDD-cost:   26
c ---[  61]---> BDD-cost:   26
c ---[  60]---> BDD-cost:   26
c ---[  59]---> BDD-cost:   26
c ---[  58]---> BDD-cost:   26
c ---[  57]---> BDD-cost:   14
c ---[  56]---> BDD-cost:   13
c ---[  55]---> BDD-cost:   14
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:   13
c ---[  52]---> BDD-cost:   13
c ---[  51]---> BDD-cost:   13
c ---[  50]---> BDD-cost:   13
c ---[  49]---> BDD-cost:   14
c ---[  48]---> BDD-cost:   12
c ---[  47]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   13
c ---[  45]---> BDD-cost:   12
c ---[  44]---> BDD-cost:   14
c ---[  43]---> BDD-cost:   11
c ---[  42]---> BDD-cost:   13
c ---[  41]---> BDD-cost:   15
c ---[  40]---> BDD-cost:   14
c ---[  39]---> BDD-cost:   13
c ---[  38]---> BDD-cost:   14
c ---[  37]---> BDD-cost:   13
c ---[  36]---> BDD-cost:   14
c ---[  35]---> BDD-cost:   13
c ---[  34]---> BDD-cost:   14
c ---[  33]---> BDD-cost:   13
c ---[  32]---> BDD-cost:   13
c ---[  31]---> BDD-cost:   13
c ---[  30]---> BDD-cost:   13
c ---[  29]---> BDD-cost:   13
c ---[  28]---> BDD-cost:   14
c ---[  27]---> BDD-cost:   13
c ---[  26]---> BDD-cost:   12
c ---[  25]---> BDD-cost:   26
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   13
c ---[  22]---> BDD-cost:   13
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   13
c ---[  19]---> BDD-cost:   13
c ---[  18]---> BDD-cost:   14
c ---[  17]---> BDD-cost:   14
c ---[  16]---> BDD-cost:   14
c ---[  15]---> BDD-cost:   14
c ---[  14]---> BDD-cost:   14
c ---[  13]---> BDD-cost:   14
c ---[  12]---> BDD-cost:   14
c ---[  11]---> BDD-cost:   14
c ---[  10]---> BDD-cost:   14
c ---[   9]---> BDD-cost:   14
c ---[   8]---> BDD-cost:   14
c ---[   7]---> BDD-cost:   14
c ---[   6]---> BDD-cost:   14
c ---[   5]---> BDD-cost:   14
c ---[   4]---> BDD-cost:   14
c ---[   3]---> BDD-cost:   14
c ---[   2]---> BDD-cost:   14
c ---[   1]---> BDD-cost:   14
c ---[   0]---> BDD-cost:   14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  280325   795242 |   93441       0        0     nan |  0.000 % |
c |       100 |  279967   794402 |  102785      87      262     3.0 | 16.150 % |
c |       250 |  279967   794402 |  113063     237      722     3.0 | 16.150 % |
c |       475 |  279859   794149 |  124369     458     1538     3.4 | 16.187 % |
c |       812 |  279693   793762 |  136806     790     2695     3.4 | 16.244 % |
c |      1318 |  278584   791186 |  150487    1238     4214     3.4 | 16.624 % |
c |      2077 |  278036   789910 |  165536    1964     6661     3.4 | 16.816 % |
c |      3216 |  277841   789461 |  182090    3091    10679     3.5 | 16.880 % |
c |      4924 |  276895   787285 |  200299    4737    17022     3.6 | 17.190 % |
c |      7486 |  276264   785807 |  220328    7267    26973     3.7 | 17.405 % |
c |     11330 |  274730   782244 |  242361   11030    42106     3.8 | 17.926 % |
c |     17096 |  272415   776825 |  266598   16686    64469     3.9 | 18.757 % |
c |     25746 |  270857   773193 |  293257   25187    98925     3.9 | 19.296 % |
c |     38720 |  269371   769698 |  322583   38002   153877     4.0 | 19.802 % |
c |     58181 |  268425   767459 |  354842   57342   260487     4.5 | 20.123 % |
c |     87373 |  268094   766645 |  390326   86456   683034     7.9 | 20.230 % |
c |    131162 |  267900   766194 |  429358  130198  1275642     9.8 | 20.294 % |
c |    196846 |  267839   766052 |  472294  195871  3912345    20.0 | 20.315 % |
c |    295372 |  267772   765898 |  519524  294384 10840815    36.8 | 20.338 % |

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/30649/stat): 30649 (minisat+_script) R 30648 30649 19316 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1846546148 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/30649/statm): 174 3 169 147 0 27 0
[pid=30649] 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=30650
New process pid=30651
New process pid=30652
execve syscall for /bin/sed executable
One traced child (pid=30651) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=30652) exited with status: 0
One traced child (pid=30650) exited with status: 0
New process pid=30653
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-fixnet3.opb

[startup+10.0043 s]
Raw data (loadavg): 1.14 1.19 1.12 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8114 0 0 0 926 36 0 0 25 0 1 0 1846546153 35926016 7717 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30653/statm): 8771 7717 145 145 0 8626 0
[pid=30653] vsize: 35084
Current children cumulated CPU time (s) 9.64
Current children cumulated vsize (Kb) 37208

[startup+20.0049 s]
Raw data (loadavg): 1.11 1.18 1.12 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8187 0 0 0 1923 37 0 0 25 0 1 0 1846546153 36233216 7790 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30653/statm): 8846 7790 145 145 0 8701 0
[pid=30653] vsize: 35384
Current children cumulated CPU time (s) 19.62
Current children cumulated vsize (Kb) 37508

[startup+30.0075 s]
Raw data (loadavg): 1.10 1.17 1.12 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8233 0 0 0 2921 39 0 0 25 0 1 0 1846546153 36442112 7836 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30653/statm): 8897 7836 145 145 0 8752 0
[pid=30653] vsize: 35588
Current children cumulated CPU time (s) 29.62
Current children cumulated vsize (Kb) 37712

[startup+40.0091 s]
Raw data (loadavg): 1.08 1.17 1.12 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8259 0 0 0 3920 40 0 0 25 0 1 0 1846546153 36519936 7862 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 8916 7862 145 145 0 8771 0
[pid=30653] vsize: 35664
Current children cumulated CPU time (s) 39.62
Current children cumulated vsize (Kb) 37788

[startup+50.0097 s]
Raw data (loadavg): 1.07 1.16 1.11 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8280 0 0 0 4920 40 0 0 25 0 1 0 1846546153 36593664 7883 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 8934 7883 145 145 0 8789 0
[pid=30653] vsize: 35736
Current children cumulated CPU time (s) 49.62
Current children cumulated vsize (Kb) 37860

[startup+60.0113 s]
Raw data (loadavg): 1.06 1.16 1.11 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8298 0 0 0 5920 40 0 0 25 0 1 0 1846546153 36651008 7901 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 8948 7901 145 145 0 8803 0
[pid=30653] vsize: 35792
Current children cumulated CPU time (s) 59.62
Current children cumulated vsize (Kb) 37916

[startup+70.0119 s]
Raw data (loadavg): 1.05 1.15 1.11 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8327 0 0 0 6919 41 0 0 25 0 1 0 1846546153 36810752 7930 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30653/statm): 8987 7930 145 145 0 8842 0
[pid=30653] vsize: 35948
Current children cumulated CPU time (s) 69.62
Current children cumulated vsize (Kb) 38072

[startup+80.0125 s]
Raw data (loadavg): 1.04 1.14 1.11 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8336 0 0 0 7918 41 0 0 25 0 1 0 1846546153 36843520 7939 4294967295 134512640 135094434 3221224432 3221223092 134553444 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 8995 7939 145 145 0 8850 0
[pid=30653] vsize: 35980
Current children cumulated CPU time (s) 79.61
Current children cumulated vsize (Kb) 38104

[startup+90.0131 s]
Raw data (loadavg): 1.03 1.14 1.11 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8352 0 0 0 8918 41 0 0 25 0 1 0 1846546153 36900864 7955 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9009 7955 145 145 0 8864 0
[pid=30653] vsize: 36036
Current children cumulated CPU time (s) 89.61
Current children cumulated vsize (Kb) 38160

[startup+100.014 s]
Raw data (loadavg): 1.03 1.13 1.10 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8372 0 0 0 9918 41 0 0 25 0 1 0 1846546153 36962304 7975 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9024 7975 145 145 0 8879 0
[pid=30653] vsize: 36096
Current children cumulated CPU time (s) 99.61
Current children cumulated vsize (Kb) 38220

[startup+110.015 s]
Raw data (loadavg): 1.02 1.13 1.10 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8385 0 0 0 10918 41 0 0 25 0 1 0 1846546153 37011456 7988 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9036 7988 145 145 0 8891 0
[pid=30653] vsize: 36144
Current children cumulated CPU time (s) 109.61
Current children cumulated vsize (Kb) 38268

[startup+120.016 s]
Raw data (loadavg): 1.02 1.12 1.10 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8400 0 0 0 11918 42 0 0 25 0 1 0 1846546153 37060608 8003 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9048 8003 145 145 0 8903 0
[pid=30653] vsize: 36192
Current children cumulated CPU time (s) 119.62
Current children cumulated vsize (Kb) 38316

[startup+130.017 s]
Raw data (loadavg): 1.02 1.12 1.10 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8414 0 0 0 12918 42 0 0 25 0 1 0 1846546153 37113856 8017 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9061 8017 145 145 0 8916 0
[pid=30653] vsize: 36244
Current children cumulated CPU time (s) 129.62
Current children cumulated vsize (Kb) 38368

[startup+140.017 s]
Raw data (loadavg): 1.01 1.12 1.10 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8429 0 0 0 13918 42 0 0 25 0 1 0 1846546153 37167104 8032 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9074 8032 145 145 0 8929 0
[pid=30653] vsize: 36296
Current children cumulated CPU time (s) 139.62
Current children cumulated vsize (Kb) 38420

[startup+150.018 s]
Raw data (loadavg): 1.01 1.11 1.10 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8444 0 0 0 14918 42 0 0 25 0 1 0 1846546153 37224448 8047 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9088 8047 145 145 0 8943 0
[pid=30653] vsize: 36352
Current children cumulated CPU time (s) 149.62
Current children cumulated vsize (Kb) 38476

[startup+160.019 s]
Raw data (loadavg): 1.01 1.11 1.09 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8455 0 0 0 15918 42 0 0 25 0 1 0 1846546153 37261312 8058 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9097 8058 145 145 0 8952 0
[pid=30653] vsize: 36388
Current children cumulated CPU time (s) 159.62
Current children cumulated vsize (Kb) 38512

[startup+170.02 s]
Raw data (loadavg): 1.01 1.10 1.09 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8499 0 0 0 16918 42 0 0 25 0 1 0 1846546153 37572608 8102 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9173 8102 145 145 0 9028 0
[pid=30653] vsize: 36692
Current children cumulated CPU time (s) 169.62
Current children cumulated vsize (Kb) 38816

[startup+180.021 s]
Raw data (loadavg): 1.00 1.10 1.09 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8500 0 0 0 17918 43 0 0 25 0 1 0 1846546153 37572608 8103 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9173 8103 145 145 0 9028 0
[pid=30653] vsize: 36692
Current children cumulated CPU time (s) 179.63
Current children cumulated vsize (Kb) 38816

[startup+190.022 s]
Raw data (loadavg): 1.00 1.10 1.09 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8504 0 0 0 18918 43 0 0 25 0 1 0 1846546153 37572608 8107 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9173 8107 145 145 0 9028 0
[pid=30653] vsize: 36692
Current children cumulated CPU time (s) 189.63
Current children cumulated vsize (Kb) 38816

[startup+200.023 s]
Raw data (loadavg): 1.00 1.09 1.09 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8506 0 0 0 19918 43 0 0 25 0 1 0 1846546153 37576704 8109 4294967295 134512640 135094434 3221224432 3221223044 134563101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9174 8109 145 145 0 9029 0
[pid=30653] vsize: 36696
Current children cumulated CPU time (s) 199.63
Current children cumulated vsize (Kb) 38820

[startup+210.022 s]
Raw data (loadavg): 1.00 1.09 1.09 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8520 0 0 0 20918 43 0 0 25 0 1 0 1846546153 37625856 8123 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9186 8123 145 145 0 9041 0
[pid=30653] vsize: 36744
Current children cumulated CPU time (s) 209.63
Current children cumulated vsize (Kb) 38868

[startup+220.023 s]
Raw data (loadavg): 1.00 1.08 1.09 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8533 0 0 0 21918 43 0 0 25 0 1 0 1846546153 37675008 8136 4294967295 134512640 135094434 3221224432 3221223044 134563092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9198 8136 145 145 0 9053 0
[pid=30653] vsize: 36792
Current children cumulated CPU time (s) 219.63
Current children cumulated vsize (Kb) 38916

[startup+230.023 s]
Raw data (loadavg): 1.00 1.08 1.08 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8546 0 0 0 22918 43 0 0 25 0 1 0 1846546153 37724160 8149 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9210 8149 145 145 0 9065 0
[pid=30653] vsize: 36840
Current children cumulated CPU time (s) 229.63
Current children cumulated vsize (Kb) 38964

[startup+240.023 s]
Raw data (loadavg): 1.00 1.08 1.08 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8563 0 0 0 23918 43 0 0 25 0 1 0 1846546153 37785600 8166 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9225 8166 145 145 0 9080 0
[pid=30653] vsize: 36900
Current children cumulated CPU time (s) 239.63
Current children cumulated vsize (Kb) 39024

[startup+250.024 s]
Raw data (loadavg): 1.00 1.08 1.08 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8580 0 0 0 24918 43 0 0 25 0 1 0 1846546153 37851136 8183 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9241 8183 145 145 0 9096 0
[pid=30653] vsize: 36964
Current children cumulated CPU time (s) 249.63
Current children cumulated vsize (Kb) 39088

[startup+260.023 s]
Raw data (loadavg): 1.00 1.07 1.08 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8595 0 0 0 25918 43 0 0 25 0 1 0 1846546153 37904384 8198 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9254 8198 145 145 0 9109 0
[pid=30653] vsize: 37016
Current children cumulated CPU time (s) 259.63
Current children cumulated vsize (Kb) 39140

[startup+270.024 s]
Raw data (loadavg): 1.00 1.07 1.08 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8611 0 0 0 26918 44 0 0 25 0 1 0 1846546153 37965824 8214 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9269 8214 145 145 0 9124 0
[pid=30653] vsize: 37076
Current children cumulated CPU time (s) 269.64
Current children cumulated vsize (Kb) 39200

[startup+280.025 s]
Raw data (loadavg): 1.00 1.07 1.08 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8628 0 0 0 27918 44 0 0 25 0 1 0 1846546153 38027264 8231 4294967295 134512640 135094434 3221224432 3221223088 134558289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9284 8231 145 145 0 9139 0
[pid=30653] vsize: 37136
Current children cumulated CPU time (s) 279.64
Current children cumulated vsize (Kb) 39260

[startup+290.025 s]
Raw data (loadavg): 1.00 1.06 1.08 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8648 0 0 0 28918 44 0 0 25 0 1 0 1846546153 38092800 8251 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9300 8251 145 145 0 9155 0
[pid=30653] vsize: 37200
Current children cumulated CPU time (s) 289.64
Current children cumulated vsize (Kb) 39324

[startup+300.026 s]
Raw data (loadavg): 1.00 1.06 1.08 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8674 0 0 0 29917 44 0 0 25 0 1 0 1846546153 38191104 8277 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9324 8277 145 145 0 9179 0
[pid=30653] vsize: 37296
Current children cumulated CPU time (s) 299.63
Current children cumulated vsize (Kb) 39420

[startup+310.025 s]
Raw data (loadavg): 1.00 1.06 1.08 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8698 0 0 0 30917 44 0 0 25 0 1 0 1846546153 38281216 8301 4294967295 134512640 135094434 3221224432 3221223044 134563148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9346 8301 145 145 0 9201 0
[pid=30653] vsize: 37384
Current children cumulated CPU time (s) 309.63
Current children cumulated vsize (Kb) 39508

[startup+320.026 s]
Raw data (loadavg): 1.00 1.06 1.08 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8723 0 0 0 31917 44 0 0 25 0 1 0 1846546153 38379520 8326 4294967295 134512640 135094434 3221224432 3221223088 134561746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9370 8326 145 145 0 9225 0
[pid=30653] vsize: 37480
Current children cumulated CPU time (s) 319.63
Current children cumulated vsize (Kb) 39604

[startup+330.026 s]
Raw data (loadavg): 1.00 1.05 1.08 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8752 0 0 0 32916 45 0 0 25 0 1 0 1846546153 38490112 8355 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9397 8355 145 145 0 9252 0
[pid=30653] vsize: 37588
Current children cumulated CPU time (s) 329.63
Current children cumulated vsize (Kb) 39712

[startup+340.026 s]
Raw data (loadavg): 1.00 1.05 1.07 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8772 0 0 0 33915 45 0 0 25 0 1 0 1846546153 38563840 8375 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30653/statm): 9415 8375 145 145 0 9270 0
[pid=30653] vsize: 37660
Current children cumulated CPU time (s) 339.62
Current children cumulated vsize (Kb) 39784

[startup+350.027 s]
Raw data (loadavg): 1.00 1.05 1.07 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8799 0 0 0 34914 45 0 0 25 0 1 0 1846546153 38670336 8402 4294967295 134512640 135094434 3221224432 3221223080 134558260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9441 8402 145 145 0 9296 0
[pid=30653] vsize: 37764
Current children cumulated CPU time (s) 349.61
Current children cumulated vsize (Kb) 39888

[startup+360.027 s]
Raw data (loadavg): 1.00 1.05 1.07 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8825 0 0 0 35914 46 0 0 25 0 1 0 1846546153 38768640 8428 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9465 8428 145 145 0 9320 0
[pid=30653] vsize: 37860
Current children cumulated CPU time (s) 359.62
Current children cumulated vsize (Kb) 39984

[startup+370.028 s]
Raw data (loadavg): 1.00 1.05 1.07 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8865 0 0 0 36914 46 0 0 25 0 1 0 1846546153 38924288 8468 4294967295 134512640 135094434 3221224432 3221223072 134562066 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9503 8468 145 145 0 9358 0
[pid=30653] vsize: 38012
Current children cumulated CPU time (s) 369.62
Current children cumulated vsize (Kb) 40136

[startup+380.029 s]
Raw data (loadavg): 1.00 1.04 1.07 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8892 0 0 0 37914 46 0 0 25 0 1 0 1846546153 39288832 8495 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9592 8495 145 145 0 9447 0
[pid=30653] vsize: 38368
Current children cumulated CPU time (s) 379.62
Current children cumulated vsize (Kb) 40492

[startup+390.029 s]
Raw data (loadavg): 1.00 1.04 1.07 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8930 0 0 0 38913 47 0 0 25 0 1 0 1846546153 39436288 8533 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9628 8533 145 145 0 9483 0
[pid=30653] vsize: 38512
Current children cumulated CPU time (s) 389.62
Current children cumulated vsize (Kb) 40636

[startup+400.03 s]
Raw data (loadavg): 1.00 1.04 1.07 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 8971 0 0 0 39913 47 0 0 25 0 1 0 1846546153 39596032 8574 4294967295 134512640 135094434 3221224432 3221223088 134561505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9667 8574 145 145 0 9522 0
[pid=30653] vsize: 38668
Current children cumulated CPU time (s) 399.62
Current children cumulated vsize (Kb) 40792

[startup+410.029 s]
Raw data (loadavg): 1.00 1.04 1.07 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 9003 0 0 0 40912 47 0 0 25 0 1 0 1846546153 39731200 8606 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9700 8606 145 145 0 9555 0
[pid=30653] vsize: 38800
Current children cumulated CPU time (s) 409.61
Current children cumulated vsize (Kb) 40924

[startup+420.03 s]
Raw data (loadavg): 1.00 1.04 1.07 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 9156 0 0 0 41911 47 0 0 25 0 1 0 1846546153 40345600 8759 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9850 8759 145 145 0 9705 0
[pid=30653] vsize: 39400
Current children cumulated CPU time (s) 419.6
Current children cumulated vsize (Kb) 41524

[startup+430.03 s]
Raw data (loadavg): 1.00 1.04 1.07 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 9283 0 0 0 42909 48 0 0 25 0 1 0 1846546153 40853504 8886 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 9974 8886 145 145 0 9829 0
[pid=30653] vsize: 39896
Current children cumulated CPU time (s) 429.59
Current children cumulated vsize (Kb) 42020

[startup+440.03 s]
Raw data (loadavg): 1.00 1.03 1.06 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 9345 0 0 0 43908 49 0 0 25 0 1 0 1846546153 41095168 8948 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 10033 8948 145 145 0 9888 0
[pid=30653] vsize: 40132
Current children cumulated CPU time (s) 439.59
Current children cumulated vsize (Kb) 42256

[startup+450.031 s]
Raw data (loadavg): 1.00 1.03 1.06 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 9392 0 0 0 44907 50 0 0 25 0 1 0 1846546153 41279488 8995 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 10078 8995 145 145 0 9933 0
[pid=30653] vsize: 40312
Current children cumulated CPU time (s) 449.59
Current children cumulated vsize (Kb) 42436

[startup+460.03 s]
Raw data (loadavg): 1.00 1.03 1.06 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 9445 0 0 0 45906 50 0 0 25 0 1 0 1846546153 41488384 9048 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 10129 9048 145 145 0 9984 0
[pid=30653] vsize: 40516
Current children cumulated CPU time (s) 459.58
Current children cumulated vsize (Kb) 42640

[startup+470.031 s]
Raw data (loadavg): 1.00 1.03 1.06 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 9491 0 0 0 46905 51 0 0 25 0 1 0 1846546153 41668608 9094 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30653/statm): 10173 9094 145 145 0 10028 0
[pid=30653] vsize: 40692
Current children cumulated CPU time (s) 469.58
Current children cumulated vsize (Kb) 42816

[startup+480.032 s]
Raw data (loadavg): 1.00 1.03 1.06 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 9522 0 0 0 47903 52 0 0 25 0 1 0 1846546153 41783296 9125 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 10201 9125 145 145 0 10056 0
[pid=30653] vsize: 40804
Current children cumulated CPU time (s) 479.57
Current children cumulated vsize (Kb) 42928

[startup+490.032 s]
Raw data (loadavg): 1.00 1.03 1.06 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 9569 0 0 0 48903 52 0 0 25 0 1 0 1846546153 41967616 9172 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 10246 9172 145 145 0 10101 0
[pid=30653] vsize: 40984
Current children cumulated CPU time (s) 489.57
Current children cumulated vsize (Kb) 43108

[startup+500.033 s]
Raw data (loadavg): 1.00 1.03 1.06 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 9618 0 0 0 49902 53 0 0 25 0 1 0 1846546153 42160128 9221 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 10293 9221 145 145 0 10148 0
[pid=30653] vsize: 41172
Current children cumulated CPU time (s) 499.57
Current children cumulated vsize (Kb) 43296

[startup+510.032 s]
Raw data (loadavg): 1.00 1.02 1.06 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 9672 0 0 0 50901 54 0 0 25 0 1 0 1846546153 42369024 9275 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 10344 9275 145 145 0 10199 0
[pid=30653] vsize: 41376
Current children cumulated CPU time (s) 509.57
Current children cumulated vsize (Kb) 43500

[startup+520.033 s]
Raw data (loadavg): 1.00 1.02 1.06 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 9719 0 0 0 51900 54 0 0 25 0 1 0 1846546153 42553344 9322 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 10389 9322 145 145 0 10244 0
[pid=30653] vsize: 41556
Current children cumulated CPU time (s) 519.56
Current children cumulated vsize (Kb) 43680

[startup+530.033 s]
Raw data (loadavg): 1.00 1.02 1.06 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 9767 0 0 0 52899 55 0 0 25 0 1 0 1846546153 42741760 9370 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 10435 9370 145 145 0 10290 0
[pid=30653] vsize: 41740
Current children cumulated CPU time (s) 529.56
Current children cumulated vsize (Kb) 43864

[startup+540.033 s]
Raw data (loadavg): 1.00 1.02 1.05 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 9838 0 0 0 53898 56 0 0 25 0 1 0 1846546153 43020288 9441 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 10503 9441 145 145 0 10358 0
[pid=30653] vsize: 42012
Current children cumulated CPU time (s) 539.56
Current children cumulated vsize (Kb) 44136

[startup+550.034 s]
Raw data (loadavg): 1.00 1.02 1.05 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 9900 0 0 0 54897 56 0 0 25 0 1 0 1846546153 43261952 9503 4294967295 134512640 135094434 3221224432 3221223084 134561517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 10562 9503 145 145 0 10417 0
[pid=30653] vsize: 42248
Current children cumulated CPU time (s) 549.55
Current children cumulated vsize (Kb) 44372

[startup+560.034 s]
Raw data (loadavg): 1.00 1.02 1.05 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 9944 0 0 0 55896 56 0 0 25 0 1 0 1846546153 43429888 9547 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 10603 9547 145 145 0 10458 0
[pid=30653] vsize: 42412
Current children cumulated CPU time (s) 559.54
Current children cumulated vsize (Kb) 44536

[startup+570.035 s]
Raw data (loadavg): 1.00 1.02 1.05 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 9996 0 0 0 56895 57 0 0 25 0 1 0 1846546153 43630592 9599 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 10652 9599 145 145 0 10507 0
[pid=30653] vsize: 42608
Current children cumulated CPU time (s) 569.54
Current children cumulated vsize (Kb) 44732

[startup+580.035 s]
Raw data (loadavg): 1.00 1.02 1.05 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 10043 0 0 0 57895 57 0 0 25 0 1 0 1846546153 43814912 9646 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 10697 9646 145 145 0 10552 0
[pid=30653] vsize: 42788
Current children cumulated CPU time (s) 579.54
Current children cumulated vsize (Kb) 44912

[startup+590.035 s]
Raw data (loadavg): 1.00 1.02 1.05 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 10100 0 0 0 58894 58 0 0 25 0 1 0 1846546153 44040192 9703 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 10752 9703 145 145 0 10607 0
[pid=30653] vsize: 43008
Current children cumulated CPU time (s) 589.54
Current children cumulated vsize (Kb) 45132

[startup+600.036 s]
Raw data (loadavg): 1.00 1.02 1.05 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 10174 0 0 0 59893 58 0 0 25 0 1 0 1846546153 44331008 9777 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 10823 9777 145 145 0 10678 0
[pid=30653] vsize: 43292
Current children cumulated CPU time (s) 599.53
Current children cumulated vsize (Kb) 45416

[startup+610.035 s]
Raw data (loadavg): 1.00 1.01 1.05 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 10258 0 0 0 60891 59 0 0 25 0 1 0 1846546153 44658688 9861 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 10903 9861 145 145 0 10758 0
[pid=30653] vsize: 43612
Current children cumulated CPU time (s) 609.52
Current children cumulated vsize (Kb) 45736

[startup+620.036 s]
Raw data (loadavg): 1.00 1.01 1.05 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 10313 0 0 0 61891 59 0 0 25 0 1 0 1846546153 44875776 9916 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 10956 9916 145 145 0 10811 0
[pid=30653] vsize: 43824
Current children cumulated CPU time (s) 619.52
Current children cumulated vsize (Kb) 45948

[startup+630.037 s]
Raw data (loadavg): 1.00 1.01 1.05 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 10358 0 0 0 62891 59 0 0 25 0 1 0 1846546153 45051904 9961 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 10999 9961 145 145 0 10854 0
[pid=30653] vsize: 43996
Current children cumulated CPU time (s) 629.52
Current children cumulated vsize (Kb) 46120

[startup+640.037 s]
Raw data (loadavg): 1.00 1.01 1.04 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 10521 0 0 0 63888 61 0 0 25 0 1 0 1846546153 45703168 10124 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 11158 10124 145 145 0 11013 0
[pid=30653] vsize: 44632
Current children cumulated CPU time (s) 639.51
Current children cumulated vsize (Kb) 46756

[startup+650.038 s]
Raw data (loadavg): 1.00 1.01 1.04 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 10595 0 0 0 64885 62 0 0 25 0 1 0 1846546153 46518272 10198 4294967295 134512640 135094434 3221224432 3221223160 134561657 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 11357 10198 145 145 0 11212 0
[pid=30653] vsize: 45428
Current children cumulated CPU time (s) 649.49
Current children cumulated vsize (Kb) 47552

[startup+660.038 s]
Raw data (loadavg): 1.00 1.01 1.04 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 10655 0 0 0 65885 62 0 0 25 0 1 0 1846546153 46755840 10258 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 11415 10258 145 145 0 11270 0
[pid=30653] vsize: 45660
Current children cumulated CPU time (s) 659.49
Current children cumulated vsize (Kb) 47784

[startup+670.039 s]
Raw data (loadavg): 1.00 1.01 1.04 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 10824 0 0 0 66883 63 0 0 25 0 1 0 1846546153 47427584 10427 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 11579 10427 145 145 0 11434 0
[pid=30653] vsize: 46316
Current children cumulated CPU time (s) 669.48
Current children cumulated vsize (Kb) 48440

[startup+680.04 s]
Raw data (loadavg): 1.00 1.01 1.04 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 11047 0 0 0 67879 64 0 0 25 0 1 0 1846546153 48316416 10650 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 11796 10650 145 145 0 11651 0
[pid=30653] vsize: 47184
Current children cumulated CPU time (s) 679.45
Current children cumulated vsize (Kb) 49308

[startup+690.04 s]
Raw data (loadavg): 1.00 1.01 1.04 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 11148 0 0 0 68877 65 0 0 25 0 1 0 1846546153 48717824 10751 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 11894 10751 145 145 0 11749 0
[pid=30653] vsize: 47576
Current children cumulated CPU time (s) 689.44
Current children cumulated vsize (Kb) 49700

[startup+700.041 s]
Raw data (loadavg): 1.00 1.01 1.04 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 11209 0 0 0 69876 65 0 0 25 0 1 0 1846546153 48955392 10812 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 11952 10812 145 145 0 11807 0
[pid=30653] vsize: 47808
Current children cumulated CPU time (s) 699.43
Current children cumulated vsize (Kb) 49932

[startup+710.04 s]
Raw data (loadavg): 1.00 1.00 1.04 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 12083 0 0 0 70862 71 0 0 25 0 1 0 1846546153 52506624 11686 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 12819 11686 145 145 0 12674 0
[pid=30653] vsize: 51276
Current children cumulated CPU time (s) 709.35
Current children cumulated vsize (Kb) 53400

[startup+720.041 s]
Raw data (loadavg): 1.00 1.00 1.04 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 12381 0 0 0 71857 74 0 0 25 0 1 0 1846546153 53710848 11984 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 13113 11984 145 145 0 12968 0
[pid=30653] vsize: 52452
Current children cumulated CPU time (s) 719.33
Current children cumulated vsize (Kb) 54576

[startup+730.042 s]
Raw data (loadavg): 1.00 1.00 1.04 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 12500 0 0 0 72855 74 0 0 25 0 1 0 1846546153 54185984 12103 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 13229 12103 145 145 0 13084 0
[pid=30653] vsize: 52916
Current children cumulated CPU time (s) 729.31
Current children cumulated vsize (Kb) 55040

[startup+740.042 s]
Raw data (loadavg): 1.00 1.00 1.04 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 12721 0 0 0 73851 76 0 0 25 0 1 0 1846546153 55074816 12324 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 13446 12324 145 145 0 13301 0
[pid=30653] vsize: 53784
Current children cumulated CPU time (s) 739.29
Current children cumulated vsize (Kb) 55908

[startup+750.043 s]
Raw data (loadavg): 1.00 1.00 1.03 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 12817 0 0 0 74849 77 0 0 25 0 1 0 1846546153 55455744 12420 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 13539 12420 145 145 0 13394 0
[pid=30653] vsize: 54156
Current children cumulated CPU time (s) 749.28
Current children cumulated vsize (Kb) 56280

[startup+760.043 s]
Raw data (loadavg): 1.00 1.00 1.03 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 12951 0 0 0 75847 78 0 0 25 0 1 0 1846546153 55988224 12554 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 13669 12554 145 145 0 13524 0
[pid=30653] vsize: 54676
Current children cumulated CPU time (s) 759.27
Current children cumulated vsize (Kb) 56800

[startup+770.044 s]
Raw data (loadavg): 1.00 1.00 1.03 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 13548 0 0 0 76838 82 0 0 25 0 1 0 1846546153 58392576 13151 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 14256 13151 145 145 0 14111 0
[pid=30653] vsize: 57024
Current children cumulated CPU time (s) 769.22
Current children cumulated vsize (Kb) 59148

[startup+780.045 s]
Raw data (loadavg): 1.00 1.00 1.03 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 13801 0 0 0 77832 85 0 0 25 0 1 0 1846546153 59404288 13404 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 14503 13404 145 145 0 14358 0
[pid=30653] vsize: 58012
Current children cumulated CPU time (s) 779.19
Current children cumulated vsize (Kb) 60136

[startup+790.045 s]
Raw data (loadavg): 1.00 1.00 1.03 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 13848 0 0 0 78832 85 0 0 25 0 1 0 1846546153 59588608 13451 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 14548 13451 145 145 0 14403 0
[pid=30653] vsize: 58192
Current children cumulated CPU time (s) 789.19
Current children cumulated vsize (Kb) 60316

[startup+800.046 s]
Raw data (loadavg): 1.00 1.00 1.03 1/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) T 30649 30649 19316 0 -1 0 14329 0 0 0 79822 88 0 0 25 0 1 0 1846546153 61530112 13932 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30653/statm): 15022 13932 145 145 0 14877 0
[pid=30653] vsize: 60088
Current children cumulated CPU time (s) 799.12
Current children cumulated vsize (Kb) 62212

[startup+810.045 s]
Raw data (loadavg): 1.00 1.00 1.03 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 14653 0 0 0 80816 91 0 0 25 0 1 0 1846546153 62836736 14256 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 15341 14256 145 145 0 15196 0
[pid=30653] vsize: 61364
Current children cumulated CPU time (s) 809.09
Current children cumulated vsize (Kb) 63488

[startup+820.046 s]
Raw data (loadavg): 1.00 1.00 1.03 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 14804 0 0 0 81813 92 0 0 25 0 1 0 1846546153 63438848 14407 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 15488 14407 145 145 0 15343 0
[pid=30653] vsize: 61952
Current children cumulated CPU time (s) 819.07
Current children cumulated vsize (Kb) 64076

[startup+830.047 s]
Raw data (loadavg): 1.00 1.00 1.03 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 14875 0 0 0 82812 92 0 0 25 0 1 0 1846546153 63721472 14478 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 15557 14478 145 145 0 15412 0
[pid=30653] vsize: 62228
Current children cumulated CPU time (s) 829.06
Current children cumulated vsize (Kb) 64352

[startup+840.047 s]
Raw data (loadavg): 1.00 1.00 1.03 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 15556 0 0 0 83801 96 0 0 25 0 1 0 1846546153 66461696 15159 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 16226 15159 145 145 0 16081 0
[pid=30653] vsize: 64904
Current children cumulated CPU time (s) 838.99
Current children cumulated vsize (Kb) 67028

[startup+850.048 s]
Raw data (loadavg): 1.00 1.00 1.02 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 15859 0 0 0 84795 99 0 0 25 0 1 0 1846546153 67674112 15462 4294967295 134512640 135094434 3221224432 3221223072 134558048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 16522 15462 145 145 0 16377 0
[pid=30653] vsize: 66088
Current children cumulated CPU time (s) 848.96
Current children cumulated vsize (Kb) 68212

[startup+860.048 s]
Raw data (loadavg): 1.00 1.00 1.02 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 16171 0 0 0 85791 101 0 0 25 0 1 0 1846546153 68927488 15774 4294967295 134512640 135094434 3221224432 3221223024 134556969 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 16828 15774 145 145 0 16683 0
[pid=30653] vsize: 67312
Current children cumulated CPU time (s) 858.94
Current children cumulated vsize (Kb) 69436

[startup+870.049 s]
Raw data (loadavg): 1.00 1.00 1.02 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 16770 0 0 0 86780 106 0 0 20 0 1 0 1846546153 71356416 16373 4294967295 134512640 135094434 3221224432 3221223136 134555072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 17421 16373 145 145 0 17276 0
[pid=30653] vsize: 69684
Current children cumulated CPU time (s) 868.88
Current children cumulated vsize (Kb) 71808

[startup+880.049 s]
Raw data (loadavg): 1.00 1.00 1.02 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 17287 0 0 0 87770 109 0 0 25 0 1 0 1846546153 73457664 16890 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 17934 16890 145 145 0 17789 0
[pid=30653] vsize: 71736
Current children cumulated CPU time (s) 878.81
Current children cumulated vsize (Kb) 73860

[startup+890.049 s]
Raw data (loadavg): 1.00 1.00 1.02 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 17753 0 0 0 88763 112 0 0 25 0 1 0 1846546153 75358208 17356 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 18398 17356 145 145 0 18253 0
[pid=30653] vsize: 73592
Current children cumulated CPU time (s) 888.77
Current children cumulated vsize (Kb) 75716

[startup+900.05 s]
Raw data (loadavg): 1.00 1.00 1.02 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 18182 0 0 0 89754 116 0 0 25 0 1 0 1846546153 77123584 17785 4294967295 134512640 135094434 3221224432 3221223024 134557310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 18829 17785 145 145 0 18684 0
[pid=30653] vsize: 75316
Current children cumulated CPU time (s) 898.72
Current children cumulated vsize (Kb) 77440

[startup+910.05 s]
Raw data (loadavg): 1.00 1.00 1.02 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 18350 0 0 0 90752 117 0 0 25 0 1 0 1846546153 78843904 17953 4294967295 134512640 135094434 3221224432 3221223044 134563148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 19249 17953 145 145 0 19104 0
[pid=30653] vsize: 76996
Current children cumulated CPU time (s) 908.71
Current children cumulated vsize (Kb) 79120

[startup+920.05 s]
Raw data (loadavg): 1.00 1.00 1.02 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 18751 0 0 0 91745 120 0 0 25 0 1 0 1846546153 80457728 18354 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 19643 18354 145 145 0 19498 0
[pid=30653] vsize: 78572
Current children cumulated CPU time (s) 918.67
Current children cumulated vsize (Kb) 80696

[startup+930.051 s]
Raw data (loadavg): 1.00 1.00 1.02 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 18984 0 0 0 92743 121 0 0 25 0 1 0 1846546153 81391616 18587 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 19871 18587 145 145 0 19726 0
[pid=30653] vsize: 79484
Current children cumulated CPU time (s) 928.66
Current children cumulated vsize (Kb) 81608

[startup+940.051 s]
Raw data (loadavg): 1.00 1.00 1.02 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 20161 0 0 0 93724 129 0 0 25 0 1 0 1846546153 86183936 19764 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 21041 19764 145 145 0 20896 0
[pid=30653] vsize: 84164
Current children cumulated CPU time (s) 938.55
Current children cumulated vsize (Kb) 86288

[startup+950.052 s]
Raw data (loadavg): 1.00 1.00 1.01 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 21248 0 0 0 94707 135 0 0 25 0 1 0 1846546153 90624000 20851 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 22125 20851 145 145 0 21980 0
[pid=30653] vsize: 88500
Current children cumulated CPU time (s) 948.44
Current children cumulated vsize (Kb) 90624

[startup+960.053 s]
Raw data (loadavg): 1.00 1.00 1.01 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 21936 0 0 0 95697 139 0 0 25 0 1 0 1846546153 93421568 21539 4294967295 134512640 135094434 3221224432 3221223088 134561460 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 22808 21539 145 145 0 22663 0
[pid=30653] vsize: 91232
Current children cumulated CPU time (s) 958.38
Current children cumulated vsize (Kb) 93356

[startup+970.053 s]
Raw data (loadavg): 1.00 1.00 1.01 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 22087 0 0 0 96696 140 0 0 25 0 1 0 1846546153 94023680 21690 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 22955 21690 145 145 0 22810 0
[pid=30653] vsize: 91820
Current children cumulated CPU time (s) 968.38
Current children cumulated vsize (Kb) 93944

[startup+980.054 s]
Raw data (loadavg): 1.00 1.00 1.01 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 22199 0 0 0 97694 141 0 0 25 0 1 0 1846546153 94470144 21802 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 23064 21802 145 145 0 22919 0
[pid=30653] vsize: 92256
Current children cumulated CPU time (s) 978.37
Current children cumulated vsize (Kb) 94380

[startup+990.054 s]
Raw data (loadavg): 1.00 1.00 1.01 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 22659 0 0 0 98688 143 0 0 25 0 1 0 1846546153 96329728 22262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 23518 22262 145 145 0 23373 0
[pid=30653] vsize: 94072
Current children cumulated CPU time (s) 988.33
Current children cumulated vsize (Kb) 96196

[startup+1000.05 s]
Raw data (loadavg): 1.00 1.00 1.01 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 22755 0 0 0 99686 144 0 0 25 0 1 0 1846546153 96710656 22358 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 23611 22358 145 145 0 23466 0
[pid=30653] vsize: 94444
Current children cumulated CPU time (s) 998.32
Current children cumulated vsize (Kb) 96568

[startup+1010.05 s]
Raw data (loadavg): 1.00 1.00 1.01 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 23159 0 0 0 100680 147 0 0 25 0 1 0 1846546153 98332672 22762 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 24007 22762 145 145 0 23862 0
[pid=30653] vsize: 96028
Current children cumulated CPU time (s) 1008.29
Current children cumulated vsize (Kb) 98152

[startup+1020.06 s]
Raw data (loadavg): 1.00 1.00 1.01 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 23396 0 0 0 101676 149 0 0 25 0 1 0 1846546153 99282944 22999 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 24239 22999 145 145 0 24094 0
[pid=30653] vsize: 96956
Current children cumulated CPU time (s) 1018.27
Current children cumulated vsize (Kb) 99080

[startup+1030.06 s]
Raw data (loadavg): 1.00 1.00 1.01 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 23856 0 0 0 102666 153 0 0 25 0 1 0 1846546153 101142528 23459 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 24693 23459 145 145 0 24548 0
[pid=30653] vsize: 98772
Current children cumulated CPU time (s) 1028.21
Current children cumulated vsize (Kb) 100896

[startup+1040.06 s]
Raw data (loadavg): 1.00 1.00 1.01 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 24150 0 0 0 103661 155 0 0 25 0 1 0 1846546153 102334464 23753 4294967295 134512640 135094434 3221224432 3221223088 134558286 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 24984 23753 145 145 0 24839 0
[pid=30653] vsize: 99936
Current children cumulated CPU time (s) 1038.18
Current children cumulated vsize (Kb) 102060

[startup+1050.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 24372 0 0 0 104658 156 0 0 25 0 1 0 1846546153 103227392 23975 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 25202 23975 145 145 0 25057 0
[pid=30653] vsize: 100808
Current children cumulated CPU time (s) 1048.16
Current children cumulated vsize (Kb) 102932

[startup+1060.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 24605 0 0 0 105654 158 0 0 25 0 1 0 1846546153 104161280 24208 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 25430 24208 145 145 0 25285 0
[pid=30653] vsize: 101720
Current children cumulated CPU time (s) 1058.14
Current children cumulated vsize (Kb) 103844

[startup+1070.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 24880 0 0 0 106649 160 0 0 25 0 1 0 1846546153 105263104 24483 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 25699 24483 145 145 0 25554 0
[pid=30653] vsize: 102796
Current children cumulated CPU time (s) 1068.11
Current children cumulated vsize (Kb) 104920

[startup+1080.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 24966 0 0 0 107648 161 0 0 25 0 1 0 1846546153 105607168 24569 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 25783 24569 145 145 0 25638 0
[pid=30653] vsize: 103132
Current children cumulated CPU time (s) 1078.11
Current children cumulated vsize (Kb) 105256

[startup+1090.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 25036 0 0 0 108647 161 0 0 25 0 1 0 1846546153 105881600 24639 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 25850 24639 145 145 0 25705 0
[pid=30653] vsize: 103400
Current children cumulated CPU time (s) 1088.1
Current children cumulated vsize (Kb) 105524

[startup+1100.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 25134 0 0 0 109646 162 0 0 25 0 1 0 1846546153 106274816 24737 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 25946 24737 145 145 0 25801 0
[pid=30653] vsize: 103784
Current children cumulated CPU time (s) 1098.1
Current children cumulated vsize (Kb) 105908

[startup+1110.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 25503 0 0 0 110639 164 0 0 25 0 1 0 1846546153 107757568 25106 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 26308 25106 145 145 0 26163 0
[pid=30653] vsize: 105232
Current children cumulated CPU time (s) 1108.05
Current children cumulated vsize (Kb) 107356

[startup+1120.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 25662 0 0 0 111637 165 0 0 25 0 1 0 1846546153 108392448 25265 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 26463 25265 145 145 0 26318 0
[pid=30653] vsize: 105852
Current children cumulated CPU time (s) 1118.04
Current children cumulated vsize (Kb) 107976

[startup+1130.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 26210 0 0 0 112628 169 0 0 25 0 1 0 1846546153 110596096 25813 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30653/statm): 27001 25813 145 145 0 26856 0
[pid=30653] vsize: 108004
Current children cumulated CPU time (s) 1127.99
Current children cumulated vsize (Kb) 110128

[startup+1140.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 26807 0 0 0 113617 173 0 0 25 0 1 0 1846546153 113004544 26410 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30653/statm): 27589 26410 145 145 0 27444 0
[pid=30653] vsize: 110356
Current children cumulated CPU time (s) 1137.92
Current children cumulated vsize (Kb) 112480

[startup+1150.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 27336 0 0 0 114608 179 0 0 25 0 1 0 1846546153 115150848 26939 4294967295 134512640 135094434 3221224432 3221223024 134557244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30653/statm): 28113 26939 145 145 0 27968 0
[pid=30653] vsize: 112452
Current children cumulated CPU time (s) 1147.89
Current children cumulated vsize (Kb) 114576

[startup+1160.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 27741 0 0 0 115599 182 0 0 25 0 1 0 1846546153 116785152 27344 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30653/statm): 28512 27344 145 145 0 28367 0
[pid=30653] vsize: 114048
Current children cumulated CPU time (s) 1157.83
Current children cumulated vsize (Kb) 116172

[startup+1170.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 27848 0 0 0 116597 183 0 0 25 0 1 0 1846546153 117211136 27451 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30653/statm): 28616 27451 145 145 0 28471 0
[pid=30653] vsize: 114464
Current children cumulated CPU time (s) 1167.82
Current children cumulated vsize (Kb) 116588

[startup+1180.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 27993 0 0 0 117594 185 0 0 25 0 1 0 1846546153 117792768 27596 4294967295 134512640 135094434 3221224432 3221223088 134557934 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30653/statm): 28758 27596 145 145 0 28613 0
[pid=30653] vsize: 115032
Current children cumulated CPU time (s) 1177.81
Current children cumulated vsize (Kb) 117156

[startup+1190.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 28109 0 0 0 118592 185 0 0 25 0 1 0 1846546153 118255616 27712 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30653/statm): 28871 27712 145 145 0 28726 0
[pid=30653] vsize: 115484
Current children cumulated CPU time (s) 1187.79
Current children cumulated vsize (Kb) 117608

[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 28382 0 0 0 119587 188 0 0 25 0 1 0 1846546153 119341056 27985 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30653/statm): 29136 27985 145 145 0 28991 0
[pid=30653] vsize: 116544
Current children cumulated CPU time (s) 1197.77
Current children cumulated vsize (Kb) 118668

[startup+1210.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 28753 0 0 0 120581 189 0 0 25 0 1 0 1846546153 120832000 28356 4294967295 134512640 135094434 3221224432 3221223072 134558043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30653/statm): 29500 28356 145 145 0 29355 0
[pid=30653] vsize: 118000
Current children cumulated CPU time (s) 1207.72
Current children cumulated vsize (Kb) 120124



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 30653
Raw data (/proc/30649/stat): 30649 (minisat+_script) S 30648 30649 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1846546148 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30649/statm): 531 226 485 147 0 384 0
[pid=30649] vsize: 2124
Raw data (/proc/30653/stat): 30653 (minisat+_64-bit) R 30649 30649 19316 0 -1 0 28753 0 0 0 120581 189 0 0 25 0 1 0 1846546153 120832000 28356 4294967295 134512640 135094434 3221224432 3221223072 134558043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30653/statm): 29500 28356 145 145 0 29355 0
[pid=30653] vsize: 118000
Current children cumulated CPU time (s) 1207.72
Current children cumulated vsize (Kb) 120124

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

Child status: 0
Real time (s): 1210.12
CPU time (s): 1207.77
CPU user time (s): 1205.81
CPU system time (s): 1.9527
CPU usage (%): 99.805
Max. virtual memory (cumulated for all children) (Kb): 120124

Verifier Data

ERROR: no interpretation found !