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/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-blp-ir98.opb
MD5SUMfb418db515bc70c21d294b6cce4dc63f
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 31
Biggest coefficient in the objective function 1073741824
Number of bits for the biggest coefficient in the objective function 31
Sum of the numbers in the objective function 2147483647
Number of bits of the sum of numbers in the objective function 31
Biggest number in a constraint 83886080000000
Number of bits of the biggest number in a constraint 47
Biggest sum of numbers in a constraint 400587756783443
Number of bits of the biggest sum of numbers49
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables7287
Total number of constraints6560
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)6451
Number of constraints which are nor clauses,nor cardinality constraints109
Minimum length of a constraint1
Maximum length of a constraint6062

Trace number 5907

Launcher Data

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        888864 kB
Buffers:         25032 kB
Cached:          91468 kB
SwapCached:        868 kB
Active:          33440 kB
Inactive:        85664 kB
HighTotal:      131008 kB
HighFree:        36260 kB
LowTotal:       903652 kB
LowFree:        852604 kB
SwapTotal:     2097892 kB
SwapFree:      2096524 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5724 kB
Slab:            20892 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 02:08:06 (client local time) WITH STATUS 0 IN 538.755 SECONDS
stats: 3098 7 538.755 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 12220] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 595 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 594]---> BDD-cost:   13
c ---[ 593]---> BDD-cost:   13
c ---[ 592]---> BDD-cost:   13
c ---[ 591]---> BDD-cost:   13
c ---[ 590]---> BDD-cost:   13
c ---[ 589]---> BDD-cost:   12
c ---[ 588]---> BDD-cost:   12
c ---[ 587]---> BDD-cost:   13
c ---[ 586]---> BDD-cost:   12
c ---[ 585]---> BDD-cost:   12
c ---[ 584]---> BDD-cost:   12
c ---[ 583]---> BDD-cost:   13
c ---[ 582]---> BDD-cost:   13
c ---[ 581]---> BDD-cost:   13
c ---[ 580]---> BDD-cost:   13
c ---[ 579]---> BDD-cost:   13
c ---[ 578]---> BDD-cost:   13
c ---[ 577]---> BDD-cost:   13
c ---[ 576]---> BDD-cost:   13
c ---[ 575]---> BDD-cost:   13
c ---[ 574]---> BDD-cost:   13
c ---[ 573]---> BDD-cost:   13
c ---[ 572]---> BDD-cost:   13
c ---[ 571]---> BDD-cost:   13
c ---[ 570]---> BDD-cost:   13
c ---[ 569]---> BDD-cost:   13
c ---[ 568]---> BDD-cost:   13
c ---[ 567]---> BDD-cost:   13
c ---[ 566]---> BDD-cost:   12
c ---[ 565]---> BDD-cost:   13
c ---[ 564]---> BDD-cost:   13
c ---[ 563]---> BDD-cost:   13
c ---[ 562]---> BDD-cost:   13
c ---[ 561]---> BDD-cost:   13
c ---[ 559]---> BDD-cost:   13
c ---[ 558]---> BDD-cost:   13
c ---[ 557]---> BDD-cost:   13
c ---[ 556]---> BDD-cost:   13
c ---[ 555]---> BDD-cost:   12
c ---[ 553]---> BDD-cost:   13
c ---[ 552]---> BDD-cost:   13
c ---[ 550]---> Adder-cost: 2746   maxlim: 2016256   bits: 21/21
c ---[ 548]---> Adder-cost: 1572   maxlim: 1411072   bits: 21/21
c ---[ 546]---> Adder-cost: 1058   maxlim: 774144   bits: 20/20
c ---[ 544]---> Adder-cost: 2140   maxlim: 1574912   bits: 21/21
c ---[ 542]---> Adder-cost: 1068   maxlim: 774144   bits: 20/20
c ---[ 540]---> Adder-cost: 1464   maxlim: 1126400   bits: 21/21
c ---[ 538]---> Adder-cost: 868   maxlim: 768000   bits: 20/20
c ---[ 536]---> Adder-cost: 4790   maxlim: 3856   bits: 12/12
c ---[ 534]---> Adder-cost: 4484   maxlim: 3897344   bits: 22/22
c ---[ 532]---> Adder-cost: 3172   maxlim: 2772992   bits: 22/22
c ---[ 530]---> Adder-cost: 1998   maxlim: 1849344   bits: 21/21
c ---[ 528]---> Adder-cost: 2086   maxlim: 2099200   bits: 22/22
c ---[ 526]---> Adder-cost: 1392   maxlim: 1105920   bits: 21/21
c ---[ 524]---> Adder-cost: 542   maxlim: 446464   bits: 19/19
c ---[ 522]---> Adder-cost: 1530   maxlim: 1665024   bits: 21/21
c ---[ 520]---> Adder-cost: 1464   maxlim: 1197056   bits: 21/21
c ---[ 518]---> Adder-cost: 958   maxlim: 817152   bits: 20/20
c ---[ 516]---> Sorter-cost:  186     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 514]---> Sorter-cost:  186     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 512]---> Adder-cost: 1184   maxlim: 1048576   bits: 21/21
c ---[ 510]---> Adder-cost: 880   maxlim: 885760   bits: 20/20
c ---[ 508]---> Adder-cost: 1420   maxlim: 1622016   bits: 21/21
c ---[ 506]---> Adder-cost: 1164   maxlim: 1024000   bits: 20/20
c ---[ 504]---> Adder-cost: 710   maxlim: 592896   bits: 20/20
c ---[ 502]---> Adder-cost: 878   maxlim: 840704   bits: 20/20
c ---[ 500]---> Adder-cost: 610   maxlim: 606208   bits: 20/20
c ---[ 498]---> Adder-cost: 178   maxlim: 163840   bits: 18/18
c ---[ 496]---> Adder-cost: 3768   maxlim: 3709952   bits: 22/22
c ---[ 494]---> Adder-cost: 3484   maxlim: 3786752   bits: 22/22
c ---[ 492]---> Adder-cost: 1354   maxlim: 1294336   bits: 21/21
c ---[ 490]---> Adder-cost: 1116   maxlim: 1150976   bits: 21/21
c ---[ 488]---> Adder-cost: 418   maxlim: 422912   bits: 19/19
c ---[ 486]---> Adder-cost: 888   maxlim: 872448   bits: 20/20
c ---[ 484]---> Adder-cost: 382   maxlim: 438272   bits: 19/19
c ---[ 482]---> Adder-cost: 480   maxlim: 477184   bits: 19/19
c ---[ 480]---> BDD-cost:   37
c ---[ 478]---> Adder-cost: 3226   maxlim: 3408896   bits: 22/22
c ---[ 476]---> Adder-cost: 1816   maxlim: 1841152   bits: 21/21
c ---[ 474]---> Adder-cost: 1052   maxlim: 1198080   bits: 21/21
c ---[ 472]---> Adder-cost: 328   maxlim: 348160   bits: 19/19
c ---[ 470]---> Adder-cost: 160

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/26315/stat): 26315 (minisat+_script) R 26314 26315 4419 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1854784185 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/26315/statm): 174 3 169 147 0 27 0
[pid=26315] 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=26316
New process pid=26317
New process pid=26318
execve syscall for /bin/sed executable
One traced child (pid=26317) 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=26318) exited with status: 0
One traced child (pid=26316) exited with status: 0
New process pid=26319
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-blp-ir98.opb

[startup+10.0035 s]
Raw data (loadavg): 0.93 0.96 0.94 2/57 26319
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854784185 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 531 226 485 147 0 384 0
[pid=26315] vsize: 2124
Raw data (/proc/26319/stat): 26319 (minisat+_64-bit) R 26315 26315 4419 0 -1 0 452 0 0 0 986 4 0 0 25 0 1 0 1854784190 2277376 438 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26319/statm): 556 438 145 145 0 411 0
[pid=26319] vsize: 2224
Current children cumulated CPU time (s) 9.9
Current children cumulated vsize (Kb) 4348

[startup+20.0051 s]
Raw data (loadavg): 0.94 0.96 0.94 2/57 26319
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854784185 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 531 226 485 147 0 384 0
[pid=26315] vsize: 2124
Raw data (/proc/26319/stat): 26319 (minisat+_64-bit) R 26315 26315 4419 0 -1 0 861 0 0 0 1980 7 0 0 25 0 1 0 1854784190 3723264 710 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26319/statm): 909 710 145 145 0 764 0
[pid=26319] vsize: 3636
Current children cumulated CPU time (s) 19.87
Current children cumulated vsize (Kb) 5760

[startup+30.0057 s]
Raw data (loadavg): 0.95 0.96 0.94 2/57 26319
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854784185 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 531 226 485 147 0 384 0
[pid=26315] vsize: 2124
Raw data (/proc/26319/stat): 26319 (minisat+_64-bit) R 26315 26315 4419 0 -1 0 1171 0 0 0 2973 10 0 0 25 0 1 0 1854784190 5062656 917 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26319/statm): 1236 917 145 145 0 1091 0
[pid=26319] vsize: 4944
Current children cumulated CPU time (s) 29.83
Current children cumulated vsize (Kb) 7068
One traced child (pid=26319) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=26320
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-blp-ir98.opb

[startup+40.0073 s]
Raw data (loadavg): 0.96 0.96 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 332 0 0 0 688 2 0 0 25 0 1 0 1854787492 1851392 317 4294967295 134512640 135167914 3221224448 3221223284 134860181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26320/statm): 452 317 162 162 0 290 0
[pid=26320] vsize: 1808
Current children cumulated CPU time (s) 39.8
Current children cumulated vsize (Kb) 3936

[startup+50.0079 s]
Raw data (loadavg): 0.96 0.96 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 777 0 0 0 1678 7 0 0 25 0 1 0 1854787492 3616768 762 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 883 762 162 162 0 721 0
[pid=26320] vsize: 3532
Current children cumulated CPU time (s) 49.75
Current children cumulated vsize (Kb) 5660

[startup+60.0085 s]
Raw data (loadavg): 0.97 0.96 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 1339 0 0 0 2669 11 0 0 25 0 1 0 1854787492 5095424 1126 4294967295 134512640 135167914 3221224448 3221223284 134860174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26320/statm): 1244 1126 162 162 0 1082 0
[pid=26320] vsize: 4976
Current children cumulated CPU time (s) 59.7
Current children cumulated vsize (Kb) 7104

[startup+70.0101 s]
Raw data (loadavg): 0.97 0.96 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 1973 0 0 0 3659 16 0 0 25 0 1 0 1854787492 6774784 1536 4294967295 134512640 135167914 3221224448 3221221432 134722657 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 1654 1536 162 162 0 1492 0
[pid=26320] vsize: 6616
Current children cumulated CPU time (s) 69.65
Current children cumulated vsize (Kb) 8744

[startup+80.0107 s]
Raw data (loadavg): 0.98 0.96 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 2924 0 0 0 4648 22 0 0 25 0 1 0 1854787492 8462336 1879 4294967295 134512640 135167914 3221224448 3221223312 134608296 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 2066 1879 162 162 0 1904 0
[pid=26320] vsize: 8264
Current children cumulated CPU time (s) 79.6
Current children cumulated vsize (Kb) 10392

[startup+90.0113 s]
Raw data (loadavg): 0.98 0.96 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 3305 0 0 0 5640 26 0 0 25 0 1 0 1854787492 10014720 2260 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26320/statm): 2445 2260 162 162 0 2283 0
[pid=26320] vsize: 9780
Current children cumulated CPU time (s) 89.56
Current children cumulated vsize (Kb) 11908

[startup+100.012 s]
Raw data (loadavg): 0.98 0.96 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 3844 0 0 0 6631 29 0 0 25 0 1 0 1854787492 11657216 2663 4294967295 134512640 135167914 3221224448 3221223312 134608335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 2846 2663 162 162 0 2684 0
[pid=26320] vsize: 11384
Current children cumulated CPU time (s) 99.5
Current children cumulated vsize (Kb) 13512

[startup+110.012 s]
Raw data (loadavg): 0.98 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 4695 0 0 0 7624 33 0 0 25 0 1 0 1854787492 15073280 3429 4294967295 134512640 135167914 3221224448 3220885564 134722512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 3680 3429 162 162 0 3518 0
[pid=26320] vsize: 14720
Current children cumulated CPU time (s) 109.47
Current children cumulated vsize (Kb) 16848

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 6156 0 0 0 8614 39 0 0 25 0 1 0 1854787492 18919424 4372 4294967295 134512640 135167914 3221224448 3221221024 134843420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 4619 4372 162 162 0 4457 0
[pid=26320] vsize: 18476
Current children cumulated CPU time (s) 119.43
Current children cumulated vsize (Kb) 20604

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 6338 0 0 0 9613 40 0 0 25 0 1 0 1854787492 19369984 4554 4294967295 134512640 135167914 3221224448 3221222928 134844672 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 4729 4554 162 162 0 4567 0
[pid=26320] vsize: 18916
Current children cumulated CPU time (s) 129.43
Current children cumulated vsize (Kb) 21044

[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 6673 0 0 0 10612 41 0 0 25 0 1 0 1854787492 22237184 4889 4294967295 134512640 135167914 3221224448 3220091580 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26320/statm): 5429 4889 162 162 0 5267 0
[pid=26320] vsize: 21716
Current children cumulated CPU time (s) 139.43
Current children cumulated vsize (Kb) 23844

[startup+150.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 11600 0 0 0 11565 63 0 0 25 0 1 0 1854787492 39878656 9196 4294967295 134512640 135167914 3221224448 3220013948 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26320/statm): 9736 9196 162 162 0 9574 0
[pid=26320] vsize: 38944
Current children cumulated CPU time (s) 149.18
Current children cumulated vsize (Kb) 41072

[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 16978 0 0 0 12511 89 0 0 25 0 1 0 1854787492 59207680 13915 4294967295 134512640 135167914 3221224448 3219869084 134722576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 14455 13915 162 162 0 14293 0
[pid=26320] vsize: 57820
Current children cumulated CPU time (s) 158.9
Current children cumulated vsize (Kb) 59948

[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 23655 0 0 0 13462 114 0 0 19 0 1 0 1854787492 81158144 19274 4294967295 134512640 135167914 3221224448 3219876640 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26320/statm): 19814 19274 162 162 0 19652 0
[pid=26320] vsize: 79256
Current children cumulated CPU time (s) 168.66
Current children cumulated vsize (Kb) 81384

[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 32975 0 0 0 14410 144 0 0 25 0 1 0 1854787492 119332864 28594 4294967295 134512640 135167914 3221224448 3219891532 134722542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 29134 28594 162 162 0 28972 0
[pid=26320] vsize: 116536
Current children cumulated CPU time (s) 178.44
Current children cumulated vsize (Kb) 118664

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 36911 0 0 0 15366 162 0 0 25 0 1 0 1854787492 124653568 29893 4294967295 134512640 135167914 3221224448 3219917472 134844720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 30433 29893 162 162 0 30271 0
[pid=26320] vsize: 121732
Current children cumulated CPU time (s) 188.18
Current children cumulated vsize (Kb) 123860

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 41364 0 0 0 16314 188 0 0 25 0 1 0 1854787492 142893056 34346 4294967295 134512640 135167914 3221224448 3219866684 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26320/statm): 34886 34346 162 162 0 34724 0
[pid=26320] vsize: 139544
Current children cumulated CPU time (s) 197.92
Current children cumulated vsize (Kb) 141672

[startup+210.021 s]
Raw data (loadavg): 0.99 0.97 0.94 1/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 45763 0 0 0 17261 211 0 0 25 0 1 0 1854787492 160911360 38745 4294967295 134512640 135167914 3221224448 3219869164 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26320/statm): 39285 38745 162 162 0 39123 0
[pid=26320] vsize: 157140
Current children cumulated CPU time (s) 207.62
Current children cumulated vsize (Kb) 159268

[startup+220.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 59418 0 0 0 18201 250 0 0 25 0 1 0 1854787492 216842240 52400 4294967295 134512640 135167914 3221224448 3219918412 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 52940 52400 162 162 0 52778 0
[pid=26320] vsize: 211760
Current children cumulated CPU time (s) 217.41
Current children cumulated vsize (Kb) 213888

[startup+230.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 63356 0 0 0 19155 269 0 0 25 0 1 0 1854787492 211374080 51065 4294967295 134512640 135167914 3221224448 3219870144 134844703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26320/statm): 51605 51065 162 162 0 51443 0
[pid=26320] vsize: 206420
Current children cumulated CPU time (s) 227.14
Current children cumulated vsize (Kb) 208548

[startup+240.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 67807 0 0 0 20099 295 0 0 25 0 1 0 1854787492 229605376 55516 4294967295 134512640 135167914 3221224448 3219881264 134693570 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 56056 55516 162 162 0 55894 0
[pid=26320] vsize: 224224
Current children cumulated CPU time (s) 236.84
Current children cumulated vsize (Kb) 226352

[startup+250.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 72330 0 0 0 21045 316 0 0 19 0 1 0 1854787492 248131584 60039 4294967295 134512640 135167914 3221224448 3219870848 134694419 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26320/statm): 60579 60039 162 162 0 60417 0
[pid=26320] vsize: 242316
Current children cumulated CPU time (s) 246.51
Current children cumulated vsize (Kb) 244444

[startup+260.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 76870 0 0 0 21996 338 0 0 25 0 1 0 1854787492 266727424 64579 4294967295 134512640 135167914 3221224448 3219869564 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26320/statm): 65119 64579 162 162 0 64957 0
[pid=26320] vsize: 260476
Current children cumulated CPU time (s) 256.24
Current children cumulated vsize (Kb) 262604

[startup+270.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 81437 0 0 0 22942 360 0 0 25 0 1 0 1854787492 285433856 69146 4294967295 134512640 135167914 3221224448 3219868316 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26320/statm): 69686 69146 162 162 0 69524 0
[pid=26320] vsize: 278744
Current children cumulated CPU time (s) 265.92
Current children cumulated vsize (Kb) 280872

[startup+280.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 86029 0 0 0 23893 381 0 0 19 0 1 0 1854787492 304242688 73738 4294967295 134512640 135167914 3221224448 3219875380 134697403 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26320/statm): 74278 73738 162 162 0 74116 0
[pid=26320] vsize: 297112
Current children cumulated CPU time (s) 275.64
Current children cumulated vsize (Kb) 299240

[startup+290.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 90601 0 0 0 24841 402 0 0 25 0 1 0 1854787492 322969600 78310 4294967295 134512640 135167914 3221224448 3219870528 134621365 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 78850 78310 162 162 0 78688 0
[pid=26320] vsize: 315400
Current children cumulated CPU time (s) 285.33
Current children cumulated vsize (Kb) 317528

[startup+300.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 112532 0 0 0 25785 453 0 0 25 0 1 0 1854787492 369602560 89695 4294967295 134512640 135167914 3221224448 3219979900 134934490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 90235 89695 162 162 0 90073 0
[pid=26320] vsize: 360940
Current children cumulated CPU time (s) 295.28
Current children cumulated vsize (Kb) 363068

[startup+310.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 116535 0 0 0 26733 475 0 0 25 0 1 0 1854787492 385998848 93698 4294967295 134512640 135167914 3221224448 3219970044 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/26320/statm): 94238 93698 162 162 0 94076 0
[pid=26320] vsize: 376952
Current children cumulated CPU time (s) 304.98
Current children cumulated vsize (Kb) 379080

[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 120996 0 0 0 27687 494 0 0 25 0 1 0 1854787492 404271104 98159 4294967295 134512640 135167914 3221224448 3219879164 134842996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 98699 98159 162 162 0 98537 0
[pid=26320] vsize: 394796
Current children cumulated CPU time (s) 314.71
Current children cumulated vsize (Kb) 396924

[startup+330.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 125492 0 0 0 28634 519 0 0 25 0 1 0 1854787492 422690816 102655 4294967295 134512640 135167914 3221224448 3219870608 134845442 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26320/statm): 103196 102655 162 162 0 103034 0
[pid=26320] vsize: 412784
Current children cumulated CPU time (s) 324.43
Current children cumulated vsize (Kb) 414912

[startup+340.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 129954 0 0 0 29584 542 0 0 25 0 1 0 1854787492 440963072 107117 4294967295 134512640 135167914 3221224448 3219896168 134846971 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26320/statm): 107657 107117 162 162 0 107495 0
[pid=26320] vsize: 430628
Current children cumulated CPU time (s) 334.16
Current children cumulated vsize (Kb) 432756

[startup+350.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 134440 0 0 0 30533 563 0 0 25 0 1 0 1854787492 459337728 111603 4294967295 134512640 135167914 3221224448 3219890432 134843113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 112143 111603 162 162 0 111981 0
[pid=26320] vsize: 448572
Current children cumulated CPU time (s) 343.86
Current children cumulated vsize (Kb) 450700

[startup+360.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 138907 0 0 0 31482 585 0 0 25 0 1 0 1854787492 477634560 116070 4294967295 134512640 135167914 3221224448 3219881368 134849258 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 116610 116070 162 162 0 116448 0
[pid=26320] vsize: 466440
Current children cumulated CPU time (s) 353.57
Current children cumulated vsize (Kb) 468568

[startup+370.032 s]
Raw data (loadavg): 0.99 0.97 0.94 1/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 143358 0 0 0 32430 608 0 0 25 0 1 0 1854787492 495865856 120521 4294967295 134512640 135167914 3221224448 3219869164 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26320/statm): 121061 120521 162 162 0 120899 0
[pid=26320] vsize: 484244
Current children cumulated CPU time (s) 363.28
Current children cumulated vsize (Kb) 486372

[startup+380.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 147793 0 0 0 33380 628 0 0 25 0 1 0 1854787492 514031616 124956 4294967295 134512640 135167914 3221224448 3219869920 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26320/statm): 125496 124956 162 162 0 125334 0
[pid=26320] vsize: 501984
Current children cumulated CPU time (s) 372.98
Current children cumulated vsize (Kb) 504112

[startup+390.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 152221 0 0 0 34329 649 0 0 19 0 1 0 1854787492 532168704 129384 4294967295 134512640 135167914 3221224448 3219897396 134619959 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26320/statm): 129924 129384 162 162 0 129762 0
[pid=26320] vsize: 519696
Current children cumulated CPU time (s) 382.68
Current children cumulated vsize (Kb) 521824

[startup+400.036 s]
Raw data (loadavg): 0.99 0.97 0.94 1/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 156696 0 0 0 35280 670 0 0 25 0 1 0 1854787492 550498304 133859 4294967295 134512640 135167914 3221224448 3219867868 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26320/statm): 134399 133859 162 162 0 134237 0
[pid=26320] vsize: 537596
Current children cumulated CPU time (s) 392.4
Current children cumulated vsize (Kb) 539724

[startup+410.037 s]
Raw data (loadavg): 0.99 0.97 0.94 1/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 161208 0 0 0 36231 690 0 0 25 0 1 0 1854787492 568979456 138371 4294967295 134512640 135167914 3221224448 3219872060 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26320/statm): 138911 138371 162 162 0 138749 0
[pid=26320] vsize: 555644
Current children cumulated CPU time (s) 402.11
Current children cumulated vsize (Kb) 557772

[startup+420.037 s]
Raw data (loadavg): 0.99 0.97 0.94 1/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 165786 0 0 0 37179 711 0 0 25 0 1 0 1854787492 587730944 142949 4294967295 134512640 135167914 3221224448 3219879324 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26320/statm): 143489 142949 162 162 0 143327 0
[pid=26320] vsize: 573956
Current children cumulated CPU time (s) 411.8
Current children cumulated vsize (Kb) 576084

[startup+430.038 s]
Raw data (loadavg): 0.99 0.97 0.94 1/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 170348 0 0 0 38127 734 0 0 25 0 1 0 1854787492 606416896 147511 4294967295 134512640 135167914 3221224448 3219866748 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/26320/statm): 148051 147511 162 162 0 147889 0
[pid=26320] vsize: 592204
Current children cumulated CPU time (s) 421.51
Current children cumulated vsize (Kb) 594332

[startup+440.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 174297 0 0 0 39080 755 0 0 25 0 1 0 1854787492 622592000 151460 4294967295 134512640 135167914 3221224448 3219965060 134620508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 152000 151460 162 162 0 151838 0
[pid=26320] vsize: 608000
Current children cumulated CPU time (s) 431.25
Current children cumulated vsize (Kb) 610128

[startup+450.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 218074 0 0 0 39964 858 0 0 25 0 1 0 1854787492 801902592 195237 4294967295 134512640 135167914 3221224448 3220053040 134694392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 195777 195237 162 162 0 195615 0
[pid=26320] vsize: 783108
Current children cumulated CPU time (s) 441.12
Current children cumulated vsize (Kb) 785236

[startup+460.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 218074 0 0 0 40964 858 0 0 25 0 1 0 1854787492 801902592 195237 4294967295 134512640 135167914 3221224448 3220053088 134625423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 195777 195237 162 162 0 195615 0
[pid=26320] vsize: 783108
Current children cumulated CPU time (s) 451.12
Current children cumulated vsize (Kb) 785236

[startup+470.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 222426 0 0 0 41909 884 0 0 25 0 1 0 1854787492 733339648 178498 4294967295 134512640 135167914 3221224448 3219869344 134522502 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26320/statm): 179038 178498 162 162 0 178876 0
[pid=26320] vsize: 716152
Current children cumulated CPU time (s) 460.83
Current children cumulated vsize (Kb) 718280

[startup+480.043 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 226876 0 0 0 42853 908 0 0 25 0 1 0 1854787492 751566848 182948 4294967295 134512640 135167914 3221224448 3219890800 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 183488 182948 162 162 0 183326 0
[pid=26320] vsize: 733952
Current children cumulated CPU time (s) 470.51
Current children cumulated vsize (Kb) 736080

[startup+490.043 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 231344 0 0 0 43803 927 0 0 25 0 1 0 1854787492 769867776 187416 4294967295 134512640 135167914 3221224448 3219915996 134619797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 187956 187416 162 162 0 187794 0
[pid=26320] vsize: 751824
Current children cumulated CPU time (s) 480.2
Current children cumulated vsize (Kb) 753952

[startup+500.044 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 235806 0 0 0 44754 948 0 0 25 0 1 0 1854787492 788144128 191878 4294967295 134512640 135167914 3221224448 3219866476 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26320/statm): 192418 191878 162 162 0 192256 0
[pid=26320] vsize: 769672
Current children cumulated CPU time (s) 489.92
Current children cumulated vsize (Kb) 771800

[startup+510.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 240187 0 0 0 45706 967 0 0 25 0 1 0 1854787492 806088704 196259 4294967295 134512640 135167914 3221224448 3219875852 134845882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 196799 196259 162 162 0 196637 0
[pid=26320] vsize: 787196
Current children cumulated CPU time (s) 499.63
Current children cumulated vsize (Kb) 789324

[startup+520.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 244571 0 0 0 46657 990 0 0 25 0 1 0 1854787492 824045568 200643 4294967295 134512640 135167914 3221224448 3219913040 134722521 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 201183 200643 162 162 0 201021 0
[pid=26320] vsize: 804732
Current children cumulated CPU time (s) 509.37
Current children cumulated vsize (Kb) 806860

[startup+530.046 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 248995 0 0 0 47603 1014 0 0 25 0 1 0 1854787492 842166272 205067 4294967295 134512640 135167914 3221224448 3219868992 134843026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 205607 205067 162 162 0 205445 0
[pid=26320] vsize: 822428
Current children cumulated CPU time (s) 519.07
Current children cumulated vsize (Kb) 824556

[startup+540.046 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 253481 0 0 0 48552 1034 0 0 25 0 1 0 1854787492 860540928 209553 4294967295 134512640 135167914 3221224448 3219907248 134693582 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 210093 209553 162 162 0 209931 0
[pid=26320] vsize: 840372
Current children cumulated CPU time (s) 528.76
Current children cumulated vsize (Kb) 842500

[startup+550.047 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 258003 0 0 0 49501 1057 0 0 25 0 1 0 1854787492 879063040 214075 4294967295 134512640 135167914 3221224448 3219867584 134694405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26320/statm): 214615 214075 162 162 0 214453 0
[pid=26320] vsize: 858460
Current children cumulated CPU time (s) 538.48
Current children cumulated vsize (Kb) 860588

[startup+560.048 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 262515 0 0 0 50444 1080 0 0 25 0 1 0 1854787492 897544192 218587 4294967295 134512640 135167914 3221224448 3219901660 134693552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26320/statm): 219127 218587 162 162 0 218965 0
[pid=26320] vsize: 876508
Current children cumulated CPU time (s) 548.14
Current children cumulated vsize (Kb) 878636

[startup+570.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 267069 0 1 0 51395 1099 0 0 25 0 1 0 1854787492 916045824 222990 4294967295 134512640 135167914 3221224448 3219867260 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26320/statm): 223644 222990 162 162 0 223482 0
[pid=26320] vsize: 894576
Current children cumulated CPU time (s) 557.84
Current children cumulated vsize (Kb) 896704

[startup+580.05 s]
Raw data (loadavg): 1.07 0.99 0.94 2/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 271095 0 162 0 52153 1123 0 0 18 0 1 0 1854787492 930910208 225321 4294967295 134512640 135167914 3221224448 3219869600 134694405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26320/statm): 227273 225321 162 162 0 227111 0
[pid=26320] vsize: 909092
Current children cumulated CPU time (s) 565.66
Current children cumulated vsize (Kb) 911220



Mem limit exceeded: sending SIGTERM then SIGKILL

[startup+588.796 s]
Raw data (loadavg): 1.06 0.99 0.94 1/57 26320
Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26315/statm): 532 234 485 147 0 385 0
[pid=26315] vsize: 2128
Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 274379 0 407 0 52687 1145 0 0 19 0 1 0 1854787492 941543424 227408 4294967295 134512640 135167914 3221224448 3219868540 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26320/statm): 229869 227408 162 162 0 229707 0
[pid=26320] vsize: 919476
Current children cumulated CPU time (s) 571.22
Current children cumulated vsize (Kb) 921604

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

Child status: 0
Real time (s): 589.226
CPU time (s): 538.755
CPU user time (s): 526.876
CPU system time (s): 11.8792
CPU usage (%): 91.4344
Max. virtual memory (cumulated for all children) (Kb): 921604

Verifier Data

ERROR: no interpretation found !