Some explanations

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

General information on the benchmark

Namemps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-scrs8.opb
MD5SUMf909afc4ad4c57b225953e69f0f7b926
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 16500
Biggest coefficient in the objective function 278154827530240000
Number of bits for the biggest coefficient in the objective function 58
Sum of the numbers in the objective function 7024858555092325200
Number of bits of the sum of numbers in the objective function 63
Biggest number in a constraint 278154827530240000
Number of bits of the biggest number in a constraint 58
Biggest sum of numbers in a constraint 7024858555092325200
Number of bits of the biggest sum of numbers63
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark891.822
Number of variables23380
Total number of constraints490
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints490
Minimum length of a constraint20
Maximum length of a constraint740

Trace number 6050

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        879248 kB
Buffers:         33084 kB
Cached:          95800 kB
SwapCached:        860 kB
Active:          37712 kB
Inactive:        93688 kB
HighTotal:      131008 kB
HighFree:        36764 kB
LowTotal:       903652 kB
LowFree:        842484 kB
SwapTotal:     2097136 kB
SwapFree:      2095644 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5520 kB
Slab:            18376 kB
Committed_AS:    72332 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 03:13:18 (client local time) WITH STATUS 0 IN 1209.81 SECONDS
stats: 3190 7 1209.81 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 1173] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 809 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ####################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssss
c ---[ 821]---> Sorter-cost:  425     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 819]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 817]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 815]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 813]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 811]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 809]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 807]---> Sorter-cost:  425     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 805]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 803]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 801]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 799]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 797]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 795]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 793]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 791]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 789]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 787]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 785]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 783]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 781]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 779]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 777]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 775]---> Sorter-cost:  425     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 773]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 771]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 769]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 767]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 765]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 763]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 761]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 759]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 757]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 755]---> Sorter-cost: 4368     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 753]---> Sorter-cost:  284     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 751]---> Sorter-cost: 2678     Base: 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 749]---> Sorter-cost: 3391     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 747]---> Sorter-cost: 4120     Base: 2 2 2 5

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/8447/stat): 8447 (minisat+_script) R 8446 8447 6847 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1796844275 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/8447/statm): 174 3 169 147 0 27 0
[pid=8447] 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=8448
New process pid=8449
New process pid=8450
One traced child (pid=8449) exited with status: 0
execve syscall for /bin/sed executable
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=8450) exited with status: 0
One traced child (pid=8448) exited with status: 0
New process pid=8451
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-scrs8.opb
One traced child (pid=8451) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=8452
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-scrs8.opb

[startup+10.0034 s]
Raw data (loadavg): 0.15 0.03 0.01 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 2685 0 3 0 946 16 0 0 25 0 1 0 1796844282 10919936 2453 4294967295 134512640 135167914 3221224448 3221220560 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8452/statm): 2666 2453 162 162 0 2504 0
[pid=8452] vsize: 10664
Current children cumulated CPU time (s) 9.64
Current children cumulated vsize (Kb) 12792

[startup+20.0042 s]
Raw data (loadavg): 0.28 0.06 0.02 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 2685 0 3 0 1945 16 0 0 25 0 1 0 1796844282 10919936 2453 4294967295 134512640 135167914 3221224448 3221219968 134696395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 2666 2453 162 162 0 2504 0
[pid=8452] vsize: 10664
Current children cumulated CPU time (s) 19.63
Current children cumulated vsize (Kb) 12792

[startup+30.005 s]
Raw data (loadavg): 0.39 0.09 0.03 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 2685 0 3 0 2945 16 0 0 25 0 1 0 1796844282 10919936 2453 4294967295 134512640 135167914 3221224448 3221222192 134629402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 2666 2453 162 162 0 2504 0
[pid=8452] vsize: 10664
Current children cumulated CPU time (s) 29.63
Current children cumulated vsize (Kb) 12792

[startup+40.0058 s]
Raw data (loadavg): 0.49 0.12 0.04 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 2808 0 3 0 3945 16 0 0 25 0 1 0 1796844282 11276288 2534 4294967295 134512640 135167914 3221224448 3221220720 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 2753 2534 162 162 0 2591 0
[pid=8452] vsize: 11012
Current children cumulated CPU time (s) 39.63
Current children cumulated vsize (Kb) 13140

[startup+50.0066 s]
Raw data (loadavg): 0.56 0.15 0.05 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 2808 0 3 0 4945 16 0 0 25 0 1 0 1796844282 11276288 2534 4294967295 134512640 135167914 3221224448 3221220908 134722208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 2753 2534 162 162 0 2591 0
[pid=8452] vsize: 11012
Current children cumulated CPU time (s) 49.63
Current children cumulated vsize (Kb) 13140

[startup+60.0065 s]
Raw data (loadavg): 0.63 0.18 0.06 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 2886 0 3 0 5945 17 0 0 25 0 1 0 1796844282 11472896 2570 4294967295 134512640 135167914 3221224448 3221220256 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 2801 2570 162 162 0 2639 0
[pid=8452] vsize: 11204
Current children cumulated CPU time (s) 59.64
Current children cumulated vsize (Kb) 13332

[startup+70.0073 s]
Raw data (loadavg): 0.69 0.21 0.07 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 2886 0 3 0 6946 17 0 0 25 0 1 0 1796844282 11472896 2570 4294967295 134512640 135167914 3221224448 3221220352 134693576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 2801 2570 162 162 0 2639 0
[pid=8452] vsize: 11204
Current children cumulated CPU time (s) 69.65
Current children cumulated vsize (Kb) 13332

[startup+80.0081 s]
Raw data (loadavg): 0.73 0.23 0.08 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 2886 0 3 0 7946 17 0 0 25 0 1 0 1796844282 11472896 2570 4294967295 134512640 135167914 3221224448 3221222080 134696691 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 2801 2570 162 162 0 2639 0
[pid=8452] vsize: 11204
Current children cumulated CPU time (s) 79.65
Current children cumulated vsize (Kb) 13332

[startup+90.0089 s]
Raw data (loadavg): 0.77 0.26 0.09 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 2983 0 3 0 8945 17 0 0 25 0 1 0 1796844282 11644928 2625 4294967295 134512640 135167914 3221224448 3221220888 134845939 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 2843 2625 162 162 0 2681 0
[pid=8452] vsize: 11372
Current children cumulated CPU time (s) 89.64
Current children cumulated vsize (Kb) 13500

[startup+100.01 s]
Raw data (loadavg): 0.81 0.28 0.10 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 2983 0 3 0 9946 17 0 0 25 0 1 0 1796844282 11644928 2625 4294967295 134512640 135167914 3221224448 3221220768 134629037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 2843 2625 162 162 0 2681 0
[pid=8452] vsize: 11372
Current children cumulated CPU time (s) 99.65
Current children cumulated vsize (Kb) 13500

[startup+110.011 s]
Raw data (loadavg): 0.84 0.30 0.11 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 3047 0 3 0 10946 17 0 0 25 0 1 0 1796844282 11878400 2647 4294967295 134512640 135167914 3221224448 3221220912 134843064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 2900 2647 162 162 0 2738 0
[pid=8452] vsize: 11600
Current children cumulated CPU time (s) 109.65
Current children cumulated vsize (Kb) 13728

[startup+120.011 s]
Raw data (loadavg): 0.86 0.33 0.12 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 3047 0 3 0 11946 17 0 0 25 0 1 0 1796844282 11878400 2647 4294967295 134512640 135167914 3221224448 3221220880 134693563 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 2900 2647 162 162 0 2738 0
[pid=8452] vsize: 11600
Current children cumulated CPU time (s) 119.65
Current children cumulated vsize (Kb) 13728

[startup+130.011 s]
Raw data (loadavg): 0.88 0.35 0.12 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 3047 0 3 0 12946 17 0 0 25 0 1 0 1796844282 11878400 2647 4294967295 134512640 135167914 3221224448 3221221532 134844632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 2900 2647 162 162 0 2738 0
[pid=8452] vsize: 11600
Current children cumulated CPU time (s) 129.65
Current children cumulated vsize (Kb) 13728

[startup+140.012 s]
Raw data (loadavg): 0.90 0.37 0.13 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 3193 0 3 0 13946 18 0 0 25 0 1 0 1796844282 12083200 2709 4294967295 134512640 135167914 3221224448 3221220716 134844675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 2950 2709 162 162 0 2788 0
[pid=8452] vsize: 11800
Current children cumulated CPU time (s) 139.66
Current children cumulated vsize (Kb) 13928

[startup+150.013 s]
Raw data (loadavg): 0.92 0.39 0.14 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 3193 0 3 0 14946 18 0 0 25 0 1 0 1796844282 12083200 2709 4294967295 134512640 135167914 3221224448 3221220672 134845906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 2950 2709 162 162 0 2788 0
[pid=8452] vsize: 11800
Current children cumulated CPU time (s) 149.66
Current children cumulated vsize (Kb) 13928

[startup+160.013 s]
Raw data (loadavg): 0.93 0.41 0.15 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 3272 0 3 0 15946 18 0 0 25 0 1 0 1796844282 12173312 2746 4294967295 134512640 135167914 3221224448 3221220560 134849082 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 2972 2746 162 162 0 2810 0
[pid=8452] vsize: 11888
Current children cumulated CPU time (s) 159.66
Current children cumulated vsize (Kb) 14016

[startup+170.013 s]
Raw data (loadavg): 0.94 0.43 0.16 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 3272 0 3 0 16947 18 0 0 25 0 1 0 1796844282 12173312 2746 4294967295 134512640 135167914 3221224448 3221221760 134720503 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 2972 2746 162 162 0 2810 0
[pid=8452] vsize: 11888
Current children cumulated CPU time (s) 169.67
Current children cumulated vsize (Kb) 14016

[startup+180.014 s]
Raw data (loadavg): 0.95 0.45 0.17 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 3272 0 3 0 17947 18 0 0 25 0 1 0 1796844282 12173312 2746 4294967295 134512640 135167914 3221224448 3221221120 134629270 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 2972 2746 162 162 0 2810 0
[pid=8452] vsize: 11888
Current children cumulated CPU time (s) 179.67
Current children cumulated vsize (Kb) 14016

[startup+190.015 s]
Raw data (loadavg): 0.95 0.46 0.18 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 3348 0 3 0 18947 18 0 0 25 0 1 0 1796844282 12263424 2780 4294967295 134512640 135167914 3221224448 3221220656 134845888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 2994 2780 162 162 0 2832 0
[pid=8452] vsize: 11976
Current children cumulated CPU time (s) 189.67
Current children cumulated vsize (Kb) 14104

[startup+200.016 s]
Raw data (loadavg): 0.96 0.48 0.19 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 3348 0 3 0 19947 18 0 0 25 0 1 0 1796844282 12263424 2780 4294967295 134512640 135167914 3221224448 3221221440 134843160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 2994 2780 162 162 0 2832 0
[pid=8452] vsize: 11976
Current children cumulated CPU time (s) 199.67
Current children cumulated vsize (Kb) 14104

[startup+210.016 s]
Raw data (loadavg): 0.97 0.50 0.19 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 3424 0 3 0 20947 18 0 0 25 0 1 0 1796844282 12742656 2814 4294967295 134512640 135167914 3221224448 3221220000 134722532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3111 2814 162 162 0 2949 0
[pid=8452] vsize: 12444
Current children cumulated CPU time (s) 209.67
Current children cumulated vsize (Kb) 14572

[startup+220.016 s]
Raw data (loadavg): 0.97 0.51 0.20 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 3424 0 3 0 21947 18 0 0 25 0 1 0 1796844282 12742656 2814 4294967295 134512640 135167914 3221224448 3221221396 134843031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3111 2814 162 162 0 2949 0
[pid=8452] vsize: 12444
Current children cumulated CPU time (s) 219.67
Current children cumulated vsize (Kb) 14572

[startup+230.017 s]
Raw data (loadavg): 0.98 0.53 0.21 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 3424 0 3 0 22947 18 0 0 25 0 1 0 1796844282 12742656 2814 4294967295 134512640 135167914 3221224448 3221220332 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3111 2814 162 162 0 2949 0
[pid=8452] vsize: 12444
Current children cumulated CPU time (s) 229.67
Current children cumulated vsize (Kb) 14572

[startup+240.018 s]
Raw data (loadavg): 0.98 0.54 0.22 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 3530 0 3 0 23947 18 0 0 25 0 1 0 1796844282 12808192 2843 4294967295 134512640 135167914 3221224448 3221220400 134849113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3127 2843 162 162 0 2965 0
[pid=8452] vsize: 12508
Current children cumulated CPU time (s) 239.67
Current children cumulated vsize (Kb) 14636

[startup+250.019 s]
Raw data (loadavg): 0.98 0.56 0.22 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 3530 0 3 0 24947 18 0 0 25 0 1 0 1796844282 12808192 2843 4294967295 134512640 135167914 3221224448 3221220756 134696180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3127 2843 162 162 0 2965 0
[pid=8452] vsize: 12508
Current children cumulated CPU time (s) 249.67
Current children cumulated vsize (Kb) 14636

[startup+260.019 s]
Raw data (loadavg): 0.98 0.57 0.23 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 3781 0 3 0 25947 19 0 0 25 0 1 0 1796844282 13271040 2969 4294967295 134512640 135167914 3221224448 3221220408 134693553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3240 2969 162 162 0 3078 0
[pid=8452] vsize: 12960
Current children cumulated CPU time (s) 259.68
Current children cumulated vsize (Kb) 15088

[startup+270.02 s]
Raw data (loadavg): 0.99 0.59 0.24 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 3781 0 3 0 26947 19 0 0 25 0 1 0 1796844282 13271040 2969 4294967295 134512640 135167914 3221224448 3221220360 134845877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3240 2969 162 162 0 3078 0
[pid=8452] vsize: 12960
Current children cumulated CPU time (s) 269.68
Current children cumulated vsize (Kb) 15088

[startup+280.019 s]
Raw data (loadavg): 0.99 0.60 0.25 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 3781 0 3 0 27947 19 0 0 25 0 1 0 1796844282 13271040 2969 4294967295 134512640 135167914 3221224448 3221221728 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3240 2969 162 162 0 3078 0
[pid=8452] vsize: 12960
Current children cumulated CPU time (s) 279.68
Current children cumulated vsize (Kb) 15088

[startup+290.02 s]
Raw data (loadavg): 0.99 0.61 0.26 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 3856 0 3 0 28946 19 0 0 25 0 1 0 1796844282 13357056 3002 4294967295 134512640 135167914 3221224448 3221220292 134844636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3261 3002 162 162 0 3099 0
[pid=8452] vsize: 13044
Current children cumulated CPU time (s) 289.67
Current children cumulated vsize (Kb) 15172

[startup+300.021 s]
Raw data (loadavg): 0.99 0.62 0.26 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 3856 0 3 0 29947 19 0 0 25 0 1 0 1796844282 13357056 3002 4294967295 134512640 135167914 3221224448 3221221996 134696410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3261 3002 162 162 0 3099 0
[pid=8452] vsize: 13044
Current children cumulated CPU time (s) 299.68
Current children cumulated vsize (Kb) 15172

[startup+310.021 s]
Raw data (loadavg): 0.99 0.64 0.27 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 3933 0 3 0 30947 19 0 0 25 0 1 0 1796844282 13447168 3037 4294967295 134512640 135167914 3221224448 3221220396 134722656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3283 3037 162 162 0 3121 0
[pid=8452] vsize: 13132
Current children cumulated CPU time (s) 309.68
Current children cumulated vsize (Kb) 15260

[startup+320.022 s]
Raw data (loadavg): 0.99 0.65 0.28 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 3933 0 3 0 31947 19 0 0 25 0 1 0 1796844282 13447168 3037 4294967295 134512640 135167914 3221224448 3221220832 134845906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3283 3037 162 162 0 3121 0
[pid=8452] vsize: 13132
Current children cumulated CPU time (s) 319.68
Current children cumulated vsize (Kb) 15260

[startup+330.022 s]
Raw data (loadavg): 0.99 0.66 0.29 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 3933 0 3 0 32947 19 0 0 25 0 1 0 1796844282 13447168 3037 4294967295 134512640 135167914 3221224448 3221219968 134844706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3283 3037 162 162 0 3121 0
[pid=8452] vsize: 13132
Current children cumulated CPU time (s) 329.68
Current children cumulated vsize (Kb) 15260

[startup+340.023 s]
Raw data (loadavg): 0.99 0.67 0.29 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 4009 0 3 0 33947 20 0 0 25 0 1 0 1796844282 13533184 3071 4294967295 134512640 135167914 3221224448 3221220336 134843068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3304 3071 162 162 0 3142 0
[pid=8452] vsize: 13216
Current children cumulated CPU time (s) 339.69
Current children cumulated vsize (Kb) 15344

[startup+350.024 s]
Raw data (loadavg): 0.99 0.68 0.30 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 4009 0 3 0 34947 20 0 0 25 0 1 0 1796844282 13533184 3071 4294967295 134512640 135167914 3221224448 3221221200 134845888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3304 3071 162 162 0 3142 0
[pid=8452] vsize: 13216
Current children cumulated CPU time (s) 349.69
Current children cumulated vsize (Kb) 15344

[startup+360.025 s]
Raw data (loadavg): 0.99 0.69 0.31 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 4086 0 3 0 35947 20 0 0 25 0 1 0 1796844282 13623296 3106 4294967295 134512640 135167914 3221224448 3221220752 134694329 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3326 3106 162 162 0 3164 0
[pid=8452] vsize: 13304
Current children cumulated CPU time (s) 359.69
Current children cumulated vsize (Kb) 15432

[startup+370.026 s]
Raw data (loadavg): 0.99 0.70 0.31 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 4086 0 3 0 36947 20 0 0 25 0 1 0 1796844282 13623296 3106 4294967295 134512640 135167914 3221224448 3221220784 134844676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3326 3106 162 162 0 3164 0
[pid=8452] vsize: 13304
Current children cumulated CPU time (s) 369.69
Current children cumulated vsize (Kb) 15432

[startup+380.026 s]
Raw data (loadavg): 0.99 0.71 0.32 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 4086 0 3 0 37948 20 0 0 25 0 1 0 1796844282 13623296 3106 4294967295 134512640 135167914 3221224448 3221222256 134844653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3326 3106 162 162 0 3164 0
[pid=8452] vsize: 13304
Current children cumulated CPU time (s) 379.7
Current children cumulated vsize (Kb) 15432

[startup+390.027 s]
Raw data (loadavg): 0.99 0.72 0.33 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 4162 0 3 0 38948 20 0 0 25 0 1 0 1796844282 14495744 3140 4294967295 134512640 135167914 3221224448 3221220400 134693570 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3539 3140 162 162 0 3377 0
[pid=8452] vsize: 14156
Current children cumulated CPU time (s) 389.7
Current children cumulated vsize (Kb) 16284

[startup+400.027 s]
Raw data (loadavg): 0.99 0.73 0.33 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 4162 0 3 0 39948 20 0 0 25 0 1 0 1796844282 14495744 3140 4294967295 134512640 135167914 3221224448 3221220448 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3539 3140 162 162 0 3377 0
[pid=8452] vsize: 14156
Current children cumulated CPU time (s) 399.7
Current children cumulated vsize (Kb) 16284

[startup+410.027 s]
Raw data (loadavg): 0.99 0.74 0.34 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 4266 0 3 0 40947 20 0 0 25 0 1 0 1796844282 14553088 3166 4294967295 134512640 135167914 3221224448 3221220576 134849163 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3553 3166 162 162 0 3391 0
[pid=8452] vsize: 14212
Current children cumulated CPU time (s) 409.69
Current children cumulated vsize (Kb) 16340

[startup+420.028 s]
Raw data (loadavg): 0.99 0.74 0.35 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 4266 0 3 0 41948 20 0 0 25 0 1 0 1796844282 14553088 3166 4294967295 134512640 135167914 3221224448 3221220912 134849179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3553 3166 162 162 0 3391 0
[pid=8452] vsize: 14212
Current children cumulated CPU time (s) 419.7
Current children cumulated vsize (Kb) 16340

[startup+430.029 s]
Raw data (loadavg): 0.99 0.75 0.35 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 4289 0 3 0 42948 21 0 0 25 0 1 0 1796844282 14602240 3189 4294967295 134512640 135167914 3221224448 3221210976 134694401 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3565 3189 162 162 0 3403 0
[pid=8452] vsize: 14260
Current children cumulated CPU time (s) 429.71
Current children cumulated vsize (Kb) 16388

[startup+440.03 s]
Raw data (loadavg): 0.99 0.76 0.36 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 4379 0 3 0 43947 21 0 0 25 0 1 0 1796844282 14643200 3201 4294967295 134512640 135167914 3221224448 3221220416 134629248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3575 3201 162 162 0 3413 0
[pid=8452] vsize: 14300
Current children cumulated CPU time (s) 439.7
Current children cumulated vsize (Kb) 16428

[startup+450.031 s]
Raw data (loadavg): 0.99 0.77 0.37 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 4379 0 3 0 44948 21 0 0 25 0 1 0 1796844282 14643200 3201 4294967295 134512640 135167914 3221224448 3221220004 134849060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3575 3201 162 162 0 3413 0
[pid=8452] vsize: 14300
Current children cumulated CPU time (s) 449.71
Current children cumulated vsize (Kb) 16428

[startup+460.031 s]
Raw data (loadavg): 0.99 0.77 0.37 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 4492 0 3 0 45947 21 0 0 25 0 1 0 1796844282 14733312 3236 4294967295 134512640 135167914 3221224448 3221220144 134844718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3597 3236 162 162 0 3435 0
[pid=8452] vsize: 14388
Current children cumulated CPU time (s) 459.7
Current children cumulated vsize (Kb) 16516

[startup+470.032 s]
Raw data (loadavg): 0.99 0.78 0.38 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 4492 0 3 0 46948 21 0 0 25 0 1 0 1796844282 14733312 3236 4294967295 134512640 135167914 3221224448 3221221220 134849060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3597 3236 162 162 0 3435 0
[pid=8452] vsize: 14388
Current children cumulated CPU time (s) 469.71
Current children cumulated vsize (Kb) 16516

[startup+480.033 s]
Raw data (loadavg): 0.99 0.79 0.38 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 4869 0 3 0 47947 22 0 0 25 0 1 0 1796844282 15552512 3448 4294967295 134512640 135167914 3221224448 3221211744 134844725 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3797 3448 162 162 0 3635 0
[pid=8452] vsize: 15188
Current children cumulated CPU time (s) 479.71
Current children cumulated vsize (Kb) 17316

[startup+490.035 s]
Raw data (loadavg): 0.99 0.79 0.39 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 4935 0 3 0 48947 22 0 0 25 0 1 0 1796844282 15499264 3436 4294967295 134512640 135167914 3221224448 3221220572 134722656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3784 3436 162 162 0 3622 0
[pid=8452] vsize: 15136
Current children cumulated CPU time (s) 489.71
Current children cumulated vsize (Kb) 17264

[startup+500.036 s]
Raw data (loadavg): 0.99 0.80 0.40 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 4935 0 3 0 49947 22 0 0 25 0 1 0 1796844282 15499264 3436 4294967295 134512640 135167914 3221224448 3221220384 134843420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3784 3436 162 162 0 3622 0
[pid=8452] vsize: 15136
Current children cumulated CPU time (s) 499.71
Current children cumulated vsize (Kb) 17264

[startup+510.036 s]
Raw data (loadavg): 0.99 0.81 0.40 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 5049 0 3 0 50947 23 0 0 25 0 1 0 1796844282 15585280 3470 4294967295 134512640 135167914 3221224448 3221219968 134843420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3805 3470 162 162 0 3643 0
[pid=8452] vsize: 15220
Current children cumulated CPU time (s) 509.72
Current children cumulated vsize (Kb) 17348

[startup+520.036 s]
Raw data (loadavg): 0.99 0.81 0.41 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 5049 0 3 0 51947 23 0 0 25 0 1 0 1796844282 15585280 3470 4294967295 134512640 135167914 3221224448 3221220908 134722512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3805 3470 162 162 0 3643 0
[pid=8452] vsize: 15220
Current children cumulated CPU time (s) 519.72
Current children cumulated vsize (Kb) 17348

[startup+530.037 s]
Raw data (loadavg): 0.99 0.82 0.41 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) T 8447 8447 6847 0 -1 0 5149 0 3 0 52947 23 0 0 25 0 1 0 1796844282 15785984 3532 4294967295 134512640 135167914 3221224448 3221213468 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3854 3532 162 162 0 3692 0
[pid=8452] vsize: 15416
Current children cumulated CPU time (s) 529.72
Current children cumulated vsize (Kb) 17544

[startup+540.038 s]
Raw data (loadavg): 0.99 0.82 0.42 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 5167 0 3 0 53947 23 0 0 25 0 1 0 1796844282 15683584 3508 4294967295 134512640 135167914 3221224448 3221220928 134843030 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3829 3508 162 162 0 3667 0
[pid=8452] vsize: 15316
Current children cumulated CPU time (s) 539.72
Current children cumulated vsize (Kb) 17444

[startup+550.039 s]
Raw data (loadavg): 0.99 0.83 0.43 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 5167 0 3 0 54948 23 0 0 25 0 1 0 1796844282 15683584 3508 4294967295 134512640 135167914 3221224448 3221221640 134842997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3829 3508 162 162 0 3667 0
[pid=8452] vsize: 15316
Current children cumulated CPU time (s) 549.73
Current children cumulated vsize (Kb) 17444

[startup+560.04 s]
Raw data (loadavg): 0.99 0.83 0.43 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 5282 0 3 0 55947 23 0 0 25 0 1 0 1796844282 15773696 3543 4294967295 134512640 135167914 3221224448 3221220016 134522462 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3851 3543 162 162 0 3689 0
[pid=8452] vsize: 15404
Current children cumulated CPU time (s) 559.72
Current children cumulated vsize (Kb) 17532

[startup+570.041 s]
Raw data (loadavg): 0.99 0.84 0.44 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 5282 0 3 0 56948 23 0 0 25 0 1 0 1796844282 15773696 3543 4294967295 134512640 135167914 3221224448 3221221464 134693553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3851 3543 162 162 0 3689 0
[pid=8452] vsize: 15404
Current children cumulated CPU time (s) 569.73
Current children cumulated vsize (Kb) 17532

[startup+580.041 s]
Raw data (loadavg): 0.99 0.84 0.44 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 5397 0 3 0 57947 23 0 0 25 0 1 0 1796844282 15863808 3577 4294967295 134512640 135167914 3221224448 3221219232 134844637 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3873 3577 162 162 0 3711 0
[pid=8452] vsize: 15492
Current children cumulated CPU time (s) 579.72
Current children cumulated vsize (Kb) 17620

[startup+590.042 s]
Raw data (loadavg): 0.99 0.85 0.45 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 5397 0 3 0 58948 23 0 0 25 0 1 0 1796844282 15863808 3577 4294967295 134512640 135167914 3221224448 3221220412 134849088 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3873 3577 162 162 0 3711 0
[pid=8452] vsize: 15492
Current children cumulated CPU time (s) 589.73
Current children cumulated vsize (Kb) 17620

[startup+600.043 s]
Raw data (loadavg): 0.99 0.85 0.45 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 5397 0 3 0 59948 23 0 0 25 0 1 0 1796844282 15863808 3577 4294967295 134512640 135167914 3221224448 3221221468 134693792 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3873 3577 162 162 0 3711 0
[pid=8452] vsize: 15492
Current children cumulated CPU time (s) 599.73
Current children cumulated vsize (Kb) 17620

[startup+610.044 s]
Raw data (loadavg): 0.99 0.86 0.46 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 5512 0 3 0 60947 24 0 0 25 0 1 0 1796844282 15953920 3612 4294967295 134512640 135167914 3221224448 3221220696 134843032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3895 3612 162 162 0 3733 0
[pid=8452] vsize: 15580
Current children cumulated CPU time (s) 609.73
Current children cumulated vsize (Kb) 17708

[startup+620.045 s]
Raw data (loadavg): 0.99 0.86 0.46 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 5512 0 3 0 61947 24 0 0 25 0 1 0 1796844282 15953920 3612 4294967295 134512640 135167914 3221224448 3221220496 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3895 3612 162 162 0 3733 0
[pid=8452] vsize: 15580
Current children cumulated CPU time (s) 619.73
Current children cumulated vsize (Kb) 17708

[startup+630.046 s]
Raw data (loadavg): 0.99 0.86 0.47 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 5627 0 3 0 62947 24 0 0 25 0 1 0 1796844282 16039936 3646 4294967295 134512640 135167914 3221224448 3221219696 134849092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3916 3646 162 162 0 3754 0
[pid=8452] vsize: 15664
Current children cumulated CPU time (s) 629.73
Current children cumulated vsize (Kb) 17792

[startup+640.047 s]
Raw data (loadavg): 0.99 0.87 0.47 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 5627 0 3 0 63947 24 0 0 25 0 1 0 1796844282 16039936 3646 4294967295 134512640 135167914 3221224448 3221220672 134696710 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3916 3646 162 162 0 3754 0
[pid=8452] vsize: 15664
Current children cumulated CPU time (s) 639.73
Current children cumulated vsize (Kb) 17792

[startup+650.047 s]
Raw data (loadavg): 0.99 0.87 0.48 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 5627 0 3 0 64948 24 0 0 25 0 1 0 1796844282 16039936 3646 4294967295 134512640 135167914 3221224448 3221219856 134843130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3916 3646 162 162 0 3754 0
[pid=8452] vsize: 15664
Current children cumulated CPU time (s) 649.74
Current children cumulated vsize (Kb) 17792

[startup+660.048 s]
Raw data (loadavg): 0.99 0.88 0.48 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 5742 0 3 0 65948 24 0 0 25 0 1 0 1796844282 16130048 3681 4294967295 134512640 135167914 3221224448 3221220320 134844725 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3938 3681 162 162 0 3776 0
[pid=8452] vsize: 15752
Current children cumulated CPU time (s) 659.74
Current children cumulated vsize (Kb) 17880

[startup+670.05 s]
Raw data (loadavg): 0.99 0.88 0.49 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 5742 0 3 0 66948 24 0 0 25 0 1 0 1796844282 16130048 3681 4294967295 134512640 135167914 3221224448 3221221376 134844725 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3938 3681 162 162 0 3776 0
[pid=8452] vsize: 15752
Current children cumulated CPU time (s) 669.74
Current children cumulated vsize (Kb) 17880

[startup+680.05 s]
Raw data (loadavg): 0.99 0.88 0.49 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 5856 0 3 0 67948 25 0 0 25 0 1 0 1796844282 16220160 3715 4294967295 134512640 135167914 3221224448 3221219328 134843404 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3960 3715 162 162 0 3798 0
[pid=8452] vsize: 15840
Current children cumulated CPU time (s) 679.75
Current children cumulated vsize (Kb) 17968

[startup+690.051 s]
Raw data (loadavg): 0.99 0.89 0.50 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 5856 0 3 0 68948 25 0 0 25 0 1 0 1796844282 16220160 3715 4294967295 134512640 135167914 3221224448 3221219996 134849056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3960 3715 162 162 0 3798 0
[pid=8452] vsize: 15840
Current children cumulated CPU time (s) 689.75
Current children cumulated vsize (Kb) 17968

[startup+700.052 s]
Raw data (loadavg): 0.99 0.89 0.50 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 5856 0 3 0 69948 25 0 0 25 0 1 0 1796844282 16220160 3715 4294967295 134512640 135167914 3221224448 3221221624 134722657 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3960 3715 162 162 0 3798 0
[pid=8452] vsize: 15840
Current children cumulated CPU time (s) 699.75
Current children cumulated vsize (Kb) 17968

[startup+710.051 s]
Raw data (loadavg): 0.99 0.89 0.51 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 5970 0 3 0 70948 25 0 0 25 0 1 0 1796844282 16306176 3749 4294967295 134512640 135167914 3221224448 3221219792 134696403 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3981 3749 162 162 0 3819 0
[pid=8452] vsize: 15924
Current children cumulated CPU time (s) 709.75
Current children cumulated vsize (Kb) 18052

[startup+720.052 s]
Raw data (loadavg): 0.99 0.90 0.51 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 5970 0 3 0 71948 25 0 0 25 0 1 0 1796844282 16306176 3749 4294967295 134512640 135167914 3221224448 3221221292 134694459 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 3981 3749 162 162 0 3819 0
[pid=8452] vsize: 15924
Current children cumulated CPU time (s) 719.75
Current children cumulated vsize (Kb) 18052

[startup+730.053 s]
Raw data (loadavg): 0.99 0.90 0.52 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 6084 0 3 0 72947 26 0 0 25 0 1 0 1796844282 16396288 3784 4294967295 134512640 135167914 3221224448 3221219852 134722512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4003 3784 162 162 0 3841 0
[pid=8452] vsize: 16012
Current children cumulated CPU time (s) 729.75
Current children cumulated vsize (Kb) 18140

[startup+740.054 s]
Raw data (loadavg): 0.99 0.90 0.52 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 6084 0 3 0 73948 26 0 0 25 0 1 0 1796844282 16396288 3784 4294967295 134512640 135167914 3221224448 3221221068 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4003 3784 162 162 0 3841 0
[pid=8452] vsize: 16012
Current children cumulated CPU time (s) 739.76
Current children cumulated vsize (Kb) 18140

[startup+750.055 s]
Raw data (loadavg): 0.99 0.90 0.53 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 6084 0 3 0 74948 26 0 0 25 0 1 0 1796844282 16396288 3784 4294967295 134512640 135167914 3221224448 3221222632 134843032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4003 3784 162 162 0 3841 0
[pid=8452] vsize: 16012
Current children cumulated CPU time (s) 749.76
Current children cumulated vsize (Kb) 18140

[startup+760.056 s]
Raw data (loadavg): 0.99 0.91 0.53 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 6199 0 3 0 75947 26 0 0 25 0 1 0 1796844282 18059264 3819 4294967295 134512640 135167914 3221224448 3221220400 134522199 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4409 3819 162 162 0 4247 0
[pid=8452] vsize: 17636
Current children cumulated CPU time (s) 759.75
Current children cumulated vsize (Kb) 19764

[startup+770.056 s]
Raw data (loadavg): 0.99 0.91 0.54 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 6199 0 3 0 76948 26 0 0 25 0 1 0 1796844282 18059264 3819 4294967295 134512640 135167914 3221224448 3221220656 134845927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4409 3819 162 162 0 4247 0
[pid=8452] vsize: 17636
Current children cumulated CPU time (s) 769.76
Current children cumulated vsize (Kb) 19764

[startup+780.057 s]
Raw data (loadavg): 0.99 0.91 0.54 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 6305 0 3 0 77947 26 0 0 25 0 1 0 1796844282 18116608 3846 4294967295 134512640 135167914 3221224448 3221220032 134843026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4423 3846 162 162 0 4261 0
[pid=8452] vsize: 17692
Current children cumulated CPU time (s) 779.75
Current children cumulated vsize (Kb) 19820

[startup+790.058 s]
Raw data (loadavg): 0.99 0.91 0.55 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 6407 0 3 0 78947 27 0 0 25 0 1 0 1796844282 18178048 3869 4294967295 134512640 135167914 3221224448 3221220384 134843012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4438 3869 162 162 0 4276 0
[pid=8452] vsize: 17752
Current children cumulated CPU time (s) 789.76
Current children cumulated vsize (Kb) 19880

[startup+800.059 s]
Raw data (loadavg): 0.99 0.92 0.55 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 6407 0 3 0 79947 27 0 0 25 0 1 0 1796844282 18178048 3869 4294967295 134512640 135167914 3221224448 3221221104 134694361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4438 3869 162 162 0 4276 0
[pid=8452] vsize: 17752
Current children cumulated CPU time (s) 799.76
Current children cumulated vsize (Kb) 19880

[startup+810.059 s]
Raw data (loadavg): 0.99 0.92 0.56 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 6521 0 3 0 80947 27 0 0 25 0 1 0 1796844282 18280448 3904 4294967295 134512640 135167914 3221224448 3221220408 134842997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4463 3904 162 162 0 4301 0
[pid=8452] vsize: 17852
Current children cumulated CPU time (s) 809.76
Current children cumulated vsize (Kb) 19980

[startup+820.059 s]
Raw data (loadavg): 0.99 0.92 0.56 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 6521 0 3 0 81947 27 0 0 25 0 1 0 1796844282 18280448 3904 4294967295 134512640 135167914 3221224448 3221221792 134843406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4463 3904 162 162 0 4301 0
[pid=8452] vsize: 17852
Current children cumulated CPU time (s) 819.76
Current children cumulated vsize (Kb) 19980

[startup+830.059 s]
Raw data (loadavg): 0.99 0.92 0.56 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 6633 0 3 0 82946 27 0 0 25 0 1 0 1796844282 18362368 3936 4294967295 134512640 135167914 3221224448 3221220160 134849148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4483 3936 162 162 0 4321 0
[pid=8452] vsize: 17932
Current children cumulated CPU time (s) 829.75
Current children cumulated vsize (Kb) 20060

[startup+840.06 s]
Raw data (loadavg): 0.99 0.92 0.57 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 6633 0 3 0 83946 27 0 0 25 0 1 0 1796844282 18362368 3936 4294967295 134512640 135167914 3221224448 3221220336 134843400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4483 3936 162 162 0 4321 0
[pid=8452] vsize: 17932
Current children cumulated CPU time (s) 839.75
Current children cumulated vsize (Kb) 20060

[startup+850.061 s]
Raw data (loadavg): 0.99 0.93 0.57 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 6633 0 3 0 84946 27 0 0 25 0 1 0 1796844282 18362368 3936 4294967295 134512640 135167914 3221224448 3221221728 134845901 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4483 3936 162 162 0 4321 0
[pid=8452] vsize: 17932
Current children cumulated CPU time (s) 849.75
Current children cumulated vsize (Kb) 20060

[startup+860.061 s]
Raw data (loadavg): 0.99 0.93 0.58 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 6747 0 3 0 85946 28 0 0 25 0 1 0 1796844282 18452480 3971 4294967295 134512640 135167914 3221224448 3221221088 134849066 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4505 3971 162 162 0 4343 0
[pid=8452] vsize: 18020
Current children cumulated CPU time (s) 859.76
Current children cumulated vsize (Kb) 20148

[startup+870.062 s]
Raw data (loadavg): 0.99 0.93 0.58 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 6747 0 3 0 86946 28 0 0 25 0 1 0 1796844282 18452480 3971 4294967295 134512640 135167914 3221224448 3221220400 134843001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4505 3971 162 162 0 4343 0
[pid=8452] vsize: 18020
Current children cumulated CPU time (s) 869.76
Current children cumulated vsize (Kb) 20148

[startup+880.063 s]
Raw data (loadavg): 0.99 0.93 0.58 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 6861 0 3 0 87946 28 0 0 25 0 1 0 1796844282 18542592 4006 4294967295 134512640 135167914 3221224448 3221220048 134849196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4527 4006 162 162 0 4365 0
[pid=8452] vsize: 18108
Current children cumulated CPU time (s) 879.76
Current children cumulated vsize (Kb) 20236

[startup+890.063 s]
Raw data (loadavg): 0.99 0.93 0.59 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 6861 0 3 0 88946 28 0 0 25 0 1 0 1796844282 18542592 4006 4294967295 134512640 135167914 3221224448 3221221292 134842996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4527 4006 162 162 0 4365 0
[pid=8452] vsize: 18108
Current children cumulated CPU time (s) 889.76
Current children cumulated vsize (Kb) 20236

[startup+900.064 s]
Raw data (loadavg): 0.99 0.94 0.59 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 6861 0 3 0 89947 28 0 0 25 0 1 0 1796844282 18542592 4006 4294967295 134512640 135167914 3221224448 3221222080 134844653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4527 4006 162 162 0 4365 0
[pid=8452] vsize: 18108
Current children cumulated CPU time (s) 899.77
Current children cumulated vsize (Kb) 20236

[startup+910.065 s]
Raw data (loadavg): 0.99 0.94 0.59 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 6976 0 3 0 90946 29 0 0 25 0 1 0 1796844282 18632704 4041 4294967295 134512640 135167914 3221224448 3221220448 134844718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4549 4041 162 162 0 4387 0
[pid=8452] vsize: 18196
Current children cumulated CPU time (s) 909.77
Current children cumulated vsize (Kb) 20324

[startup+920.066 s]
Raw data (loadavg): 0.99 0.94 0.60 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 6976 0 3 0 91946 29 0 0 25 0 1 0 1796844282 18632704 4041 4294967295 134512640 135167914 3221224448 3221221100 134722656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4549 4041 162 162 0 4387 0
[pid=8452] vsize: 18196
Current children cumulated CPU time (s) 919.77
Current children cumulated vsize (Kb) 20324

[startup+930.067 s]
Raw data (loadavg): 0.99 0.94 0.60 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 7091 0 3 0 92946 29 0 0 25 0 1 0 1796844282 18722816 4076 4294967295 134512640 135167914 3221224448 3221219440 134843113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4571 4076 162 162 0 4409 0
[pid=8452] vsize: 18284
Current children cumulated CPU time (s) 929.77
Current children cumulated vsize (Kb) 20412

[startup+940.069 s]
Raw data (loadavg): 0.99 0.94 0.61 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 7091 0 3 0 93947 29 0 0 25 0 1 0 1796844282 18722816 4076 4294967295 134512640 135167914 3221224448 3221221088 134849153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4571 4076 162 162 0 4409 0
[pid=8452] vsize: 18284
Current children cumulated CPU time (s) 939.78
Current children cumulated vsize (Kb) 20412

[startup+950.069 s]
Raw data (loadavg): 0.99 0.94 0.61 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 7778 0 3 0 94945 30 0 0 25 0 1 0 1796844282 20144128 4433 4294967295 134512640 135167914 3221224448 3221211648 134843153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4918 4433 162 162 0 4756 0
[pid=8452] vsize: 19672
Current children cumulated CPU time (s) 949.77
Current children cumulated vsize (Kb) 21800

[startup+960.07 s]
Raw data (loadavg): 0.99 0.94 0.61 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 7862 0 3 0 95945 31 0 0 25 0 1 0 1796844282 20156416 4438 4294967295 134512640 135167914 3221224448 3221220144 134696366 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4921 4438 162 162 0 4759 0
[pid=8452] vsize: 19684
Current children cumulated CPU time (s) 959.78
Current children cumulated vsize (Kb) 21812

[startup+970.072 s]
Raw data (loadavg): 0.99 0.95 0.62 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 7862 0 3 0 96945 31 0 0 25 0 1 0 1796844282 20156416 4438 4294967295 134512640 135167914 3221224448 3221219956 134843117 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4921 4438 162 162 0 4759 0
[pid=8452] vsize: 19684
Current children cumulated CPU time (s) 969.78
Current children cumulated vsize (Kb) 21812

[startup+980.072 s]
Raw data (loadavg): 0.99 0.95 0.62 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 7976 0 3 0 97945 31 0 0 25 0 1 0 1796844282 20246528 4473 4294967295 134512640 135167914 3221224448 3221220236 134849056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4943 4473 162 162 0 4781 0
[pid=8452] vsize: 19772
Current children cumulated CPU time (s) 979.78
Current children cumulated vsize (Kb) 21900

[startup+990.073 s]
Raw data (loadavg): 0.99 0.95 0.63 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 7976 0 3 0 98946 31 0 0 25 0 1 0 1796844282 20246528 4473 4294967295 134512640 135167914 3221224448 3221221592 134842997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4943 4473 162 162 0 4781 0
[pid=8452] vsize: 19772
Current children cumulated CPU time (s) 989.79
Current children cumulated vsize (Kb) 21900

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.95 0.63 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 8082 0 3 0 99945 31 0 0 25 0 1 0 1796844282 20307968 4501 4294967295 134512640 135167914 3221224448 3221219628 134723260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4958 4501 162 162 0 4796 0
[pid=8452] vsize: 19832
Current children cumulated CPU time (s) 999.78
Current children cumulated vsize (Kb) 21960

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.95 0.63 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 8182 0 3 0 100945 31 0 0 25 0 1 0 1796844282 20361216 4522 4294967295 134512640 135167914 3221224448 3221220224 134849092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4971 4522 162 162 0 4809 0
[pid=8452] vsize: 19884
Current children cumulated CPU time (s) 1009.78
Current children cumulated vsize (Kb) 22012

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.95 0.64 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 8182 0 3 0 101946 31 0 0 25 0 1 0 1796844282 20361216 4522 4294967295 134512640 135167914 3221224448 3221220944 134630830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4971 4522 162 162 0 4809 0
[pid=8452] vsize: 19884
Current children cumulated CPU time (s) 1019.79
Current children cumulated vsize (Kb) 22012

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.95 0.64 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 8290 0 3 0 102945 32 0 0 25 0 1 0 1796844282 20434944 4550 4294967295 134512640 135167914 3221224448 3221220772 134629364 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 4989 4550 162 162 0 4827 0
[pid=8452] vsize: 19956
Current children cumulated CPU time (s) 1029.79
Current children cumulated vsize (Kb) 22084

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.95 0.64 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 8331 0 3 0 103945 32 0 0 25 0 1 0 1796844282 20566016 4591 4294967295 134512640 135167914 3221224448 3221211440 134849565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 5021 4591 162 162 0 4859 0
[pid=8452] vsize: 20084
Current children cumulated CPU time (s) 1039.79
Current children cumulated vsize (Kb) 22212

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.95 0.65 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 8399 0 3 0 104945 32 0 0 25 0 1 0 1796844282 20512768 4580 4294967295 134512640 135167914 3221224448 3221220800 134844703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 5008 4580 162 162 0 4846 0
[pid=8452] vsize: 20032
Current children cumulated CPU time (s) 1049.79
Current children cumulated vsize (Kb) 22160

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.95 0.65 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 8399 0 3 0 105945 32 0 0 25 0 1 0 1796844282 20512768 4580 4294967295 134512640 135167914 3221224448 3221221284 134849086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 5008 4580 162 162 0 4846 0
[pid=8452] vsize: 20032
Current children cumulated CPU time (s) 1059.79
Current children cumulated vsize (Kb) 22160

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.96 0.65 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 8513 0 3 0 106945 32 0 0 25 0 1 0 1796844282 20606976 4615 4294967295 134512640 135167914 3221224448 3221221280 134849092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 5031 4615 162 162 0 4869 0
[pid=8452] vsize: 20124
Current children cumulated CPU time (s) 1069.79
Current children cumulated vsize (Kb) 22252

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.96 0.66 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 8513 0 3 0 107945 32 0 0 25 0 1 0 1796844282 20606976 4615 4294967295 134512640 135167914 3221224448 3221221292 134696176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 5031 4615 162 162 0 4869 0
[pid=8452] vsize: 20124
Current children cumulated CPU time (s) 1079.79
Current children cumulated vsize (Kb) 22252

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.96 0.66 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 8627 0 3 0 108945 33 0 0 25 0 1 0 1796844282 20697088 4649 4294967295 134512640 135167914 3221224448 3221220756 134843000 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 5053 4649 162 162 0 4891 0
[pid=8452] vsize: 20212
Current children cumulated CPU time (s) 1089.8
Current children cumulated vsize (Kb) 22340

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.96 0.66 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 8627 0 3 0 109945 33 0 0 25 0 1 0 1796844282 20697088 4649 4294967295 134512640 135167914 3221224448 3221220912 134694495 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 5053 4649 162 162 0 4891 0
[pid=8452] vsize: 20212
Current children cumulated CPU time (s) 1099.8
Current children cumulated vsize (Kb) 22340

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.96 0.66 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 8740 0 3 0 110945 33 0 0 25 0 1 0 1796844282 20783104 4683 4294967295 134512640 135167914 3221224448 3221220412 134849056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 5074 4683 162 162 0 4912 0
[pid=8452] vsize: 20296
Current children cumulated CPU time (s) 1109.8
Current children cumulated vsize (Kb) 22424

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.96 0.67 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 8740 0 3 0 111945 33 0 0 25 0 1 0 1796844282 20783104 4683 4294967295 134512640 135167914 3221224448 3221220592 134630912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 5074 4683 162 162 0 4912 0
[pid=8452] vsize: 20296
Current children cumulated CPU time (s) 1119.8
Current children cumulated vsize (Kb) 22424

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.96 0.67 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 8740 0 3 0 112945 33 0 0 25 0 1 0 1796844282 20783104 4683 4294967295 134512640 135167914 3221224448 3221220860 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 5074 4683 162 162 0 4912 0
[pid=8452] vsize: 20296
Current children cumulated CPU time (s) 1129.8
Current children cumulated vsize (Kb) 22424

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.96 0.67 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 8854 0 3 0 113945 33 0 0 25 0 1 0 1796844282 20873216 4718 4294967295 134512640 135167914 3221224448 3221221464 134843032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 5096 4718 162 162 0 4934 0
[pid=8452] vsize: 20384
Current children cumulated CPU time (s) 1139.8
Current children cumulated vsize (Kb) 22512

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.96 0.68 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 8854 0 3 0 114945 33 0 0 25 0 1 0 1796844282 20873216 4718 4294967295 134512640 135167914 3221224448 3221221740 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 5096 4718 162 162 0 4934 0
[pid=8452] vsize: 20384
Current children cumulated CPU time (s) 1149.8
Current children cumulated vsize (Kb) 22512

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.96 0.68 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 8969 0 3 0 115944 34 0 0 25 0 1 0 1796844282 20963328 4753 4294967295 134512640 135167914 3221224448 3221221108 134843000 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 5118 4753 162 162 0 4956 0
[pid=8452] vsize: 20472
Current children cumulated CPU time (s) 1159.8
Current children cumulated vsize (Kb) 22600

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.68 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 8969 0 3 0 116945 34 0 0 25 0 1 0 1796844282 20963328 4753 4294967295 134512640 135167914 3221224448 3221220496 134844715 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 5118 4753 162 162 0 4956 0
[pid=8452] vsize: 20472
Current children cumulated CPU time (s) 1169.81
Current children cumulated vsize (Kb) 22600

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.68 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 9036 0 3 0 117945 34 0 0 25 0 1 0 1796844282 21037056 4783 4294967295 134512640 135167914 3221224448 3221221212 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 5136 4783 162 162 0 4974 0
[pid=8452] vsize: 20544
Current children cumulated CPU time (s) 1179.81
Current children cumulated vsize (Kb) 22672

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.69 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 9142 0 3 0 118944 35 0 0 25 0 1 0 1796844282 21114880 4814 4294967295 134512640 135167914 3221224448 3221222624 134843030 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 5155 4814 162 162 0 4993 0
[pid=8452] vsize: 20620
Current children cumulated CPU time (s) 1189.81
Current children cumulated vsize (Kb) 22748

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.69 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 9249 0 3 0 119944 35 0 0 25 0 1 0 1796844282 21200896 4847 4294967295 134512640 135167914 3221224448 3221221104 134693582 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 5176 4847 162 162 0 5014 0
[pid=8452] vsize: 20704
Current children cumulated CPU time (s) 1199.81
Current children cumulated vsize (Kb) 22832

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.69 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 9399 0 3 0 120944 35 0 0 25 0 1 0 1796844282 21282816 4879 4294967295 134512640 135167914 3221224448 3221221212 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 5196 4879 162 162 0 5034 0
[pid=8452] vsize: 20784
Current children cumulated CPU time (s) 1209.81
Current children cumulated vsize (Kb) 22912



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.69 2/57 8452
Raw data (/proc/8447/stat): 8447 (minisat+_script) S 8446 8447 6847 0 -1 0 313 331 1 0 0 1 0 1 22 0 1 0 1796844275 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8447/statm): 532 234 485 147 0 385 0
[pid=8447] vsize: 2128
Raw data (/proc/8452/stat): 8452 (minisat+_bignum) R 8447 8447 6847 0 -1 0 9399 0 3 0 120944 35 0 0 25 0 1 0 1796844282 21282816 4879 4294967295 134512640 135167914 3221224448 3221221392 134843010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8452/statm): 5196 4879 162 162 0 5034 0
[pid=8452] vsize: 20784
Current children cumulated CPU time (s) 1209.81
Current children cumulated vsize (Kb) 22912

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

Child status: 0
Real time (s): 1210.11
CPU time (s): 1209.81
CPU user time (s): 1209.44
CPU system time (s): 0.367944
CPU usage (%): 99.9757
Max. virtual memory (cumulated for all children) (Kb): 22912

Verifier Data

ERROR: no interpretation found !