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/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-neos2.opb
MD5SUMb7400535246fc2c2b54a52ae77322df5
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 84
Biggest coefficient in the objective function 1048576
Number of bits for the biggest coefficient in the objective function 21
Sum of the numbers in the objective function 8388604
Number of bits of the sum of numbers in the objective function 23
Biggest number in a constraint 2396687647113216000
Number of bits of the biggest number in a constraint 62
Biggest sum of numbers in a constraint 282492798299765243904
Number of bits of the biggest sum of numbers68
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables21894
Total number of constraints2173
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)1053
Number of constraints which are nor clauses,nor cardinality constraints1120
Minimum length of a constraint1
Maximum length of a constraint3188

Trace number 6298

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        897076 kB
Buffers:         19012 kB
Cached:          90400 kB
SwapCached:        612 kB
Active:          33448 kB
Inactive:        78468 kB
HighTotal:      131008 kB
HighFree:        40936 kB
LowTotal:       903652 kB
LowFree:        856140 kB
SwapTotal:     2097892 kB
SwapFree:      2096676 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5676 kB
Slab:            20036 kB
Committed_AS:    64280 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 05:39:26 (client local time) WITH STATUS 0 IN 1207.12 SECONDS
stats: 3457 7 1207.12 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 3179] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...

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/7481/stat): 7481 (minisat+_script) R 7480 7481 19316 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855988004 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/7481/statm): 174 3 169 147 0 27 0
[pid=7481] 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=7482
New process pid=7483
New process pid=7484
execve syscall for /bin/sed executable
One traced child (pid=7483) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=7484) exited with status: 0
One traced child (pid=7482) exited with status: 0
New process pid=7485
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-neos2.opb
One traced child (pid=7485) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=7486
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-neos2.opb

[startup+10.004 s]
Raw data (loadavg): 0.82 0.94 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 2710 0 0 0 957 16 0 0 25 0 1 0 1855988013 10915840 2440 4294967295 134512640 135167914 3221224448 3221223296 134594194 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7486/statm): 2665 2440 162 162 0 2503 0
[pid=7486] vsize: 10660
Current children cumulated CPU time (s) 9.78
Current children cumulated vsize (Kb) 12788

[startup+20.0046 s]
Raw data (loadavg): 0.85 0.94 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 4968 0 0 0 1940 25 0 0 25 0 1 0 1855988013 18481152 4279 4294967295 134512640 135167914 3221224448 3221092172 134842996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7486/statm): 4512 4279 162 162 0 4350 0
[pid=7486] vsize: 18048
Current children cumulated CPU time (s) 19.7
Current children cumulated vsize (Kb) 20176

[startup+30.0052 s]
Raw data (loadavg): 0.87 0.94 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 12054 0 0 0 2874 56 0 0 25 0 1 0 1855988013 43446272 10376 4294967295 134512640 135167914 3221224448 3221091808 134844745 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 10607 10376 162 162 0 10445 0
[pid=7486] vsize: 42428
Current children cumulated CPU time (s) 29.35
Current children cumulated vsize (Kb) 44556

[startup+40.0058 s]
Raw data (loadavg): 0.89 0.94 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 19598 0 0 0 3815 88 0 0 25 0 1 0 1855988013 69099520 16602 4294967295 134512640 135167914 3221224448 3221091708 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 16870 16602 162 162 0 16708 0
[pid=7486] vsize: 67480
Current children cumulated CPU time (s) 39.08
Current children cumulated vsize (Kb) 69608

[startup+50.0074 s]
Raw data (loadavg): 0.91 0.95 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 29201 0 0 0 4760 117 0 0 25 0 1 0 1855988013 108400640 26205 4294967295 134512640 135167914 3221224448 3221091856 134845921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 26465 26205 162 162 0 26303 0
[pid=7486] vsize: 105860
Current children cumulated CPU time (s) 48.82
Current children cumulated vsize (Kb) 107988

[startup+60.008 s]
Raw data (loadavg): 0.92 0.95 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) T 7481 7481 19316 0 -1 0 34760 0 0 0 5700 143 0 0 25 0 1 0 1855988013 120164352 29085 4294967295 134512640 135167914 3221224448 3221091580 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7486/statm): 29337 29085 162 162 0 29175 0
[pid=7486] vsize: 117348
Current children cumulated CPU time (s) 58.48
Current children cumulated vsize (Kb) 119476

[startup+70.0086 s]
Raw data (loadavg): 0.93 0.95 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) T 7481 7481 19316 0 -1 0 40286 0 0 0 6637 171 0 0 25 0 1 0 1855988013 142774272 34611 4294967295 134512640 135167914 3221224448 3221091132 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7486/statm): 34857 34611 162 162 0 34695 0
[pid=7486] vsize: 139428
Current children cumulated CPU time (s) 68.13
Current children cumulated vsize (Kb) 141556

[startup+80.0092 s]
Raw data (loadavg): 0.94 0.95 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 55783 0 0 0 7558 221 0 0 25 0 1 0 1855988013 206225408 50108 4294967295 134512640 135167914 3221224448 3221091712 134693576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 50348 50108 162 162 0 50186 0
[pid=7486] vsize: 201392
Current children cumulated CPU time (s) 77.84
Current children cumulated vsize (Kb) 203520

[startup+90.0098 s]
Raw data (loadavg): 0.95 0.95 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 59246 0 0 0 8522 237 0 0 25 0 1 0 1855988013 198795264 48298 4294967295 134512640 135167914 3221224448 3221091440 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 48534 48298 162 162 0 48372 0
[pid=7486] vsize: 194136
Current children cumulated CPU time (s) 87.64
Current children cumulated vsize (Kb) 196264

[startup+100.01 s]
Raw data (loadavg): 0.96 0.95 0.98 1/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) T 7481 7481 19316 0 -1 0 64864 0 0 0 9463 263 0 0 25 0 1 0 1855988013 221786112 53916 4294967295 134512640 135167914 3221224448 3221091068 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7486/statm): 54147 53916 162 162 0 53985 0
[pid=7486] vsize: 216588
Current children cumulated CPU time (s) 97.31
Current children cumulated vsize (Kb) 218716

[startup+110.011 s]
Raw data (loadavg): 0.96 0.95 0.98 1/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) T 7481 7481 19316 0 -1 0 70394 0 0 0 10399 290 0 0 25 0 1 0 1855988013 244420608 59446 4294967295 134512640 135167914 3221224448 3221091356 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7486/statm): 59673 59446 162 162 0 59511 0
[pid=7486] vsize: 238692
Current children cumulated CPU time (s) 106.94
Current children cumulated vsize (Kb) 240820

[startup+120.012 s]
Raw data (loadavg): 0.97 0.95 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 11372 301 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221222984 134846971 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 116.78
Current children cumulated vsize (Kb) 208908

[startup+130.012 s]
Raw data (loadavg): 0.97 0.95 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 12372 302 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216448 134844718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 126.79
Current children cumulated vsize (Kb) 208908

[startup+140.013 s]
Raw data (loadavg): 0.98 0.95 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 13373 302 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216336 134694495 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 136.8
Current children cumulated vsize (Kb) 208908

[startup+150.014 s]
Raw data (loadavg): 0.98 0.95 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 14373 302 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216356 134843031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 146.8
Current children cumulated vsize (Kb) 208908

[startup+160.015 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 15373 302 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217056 134849163 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 156.8
Current children cumulated vsize (Kb) 208908

[startup+170.016 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 16373 302 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216512 134849061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 166.8
Current children cumulated vsize (Kb) 208908

[startup+180.016 s]
Raw data (loadavg): 0.99 0.96 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 17374 302 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216512 134694517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 176.81
Current children cumulated vsize (Kb) 208908

[startup+190.017 s]
Raw data (loadavg): 0.99 0.96 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 18374 302 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216880 134693570 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 186.81
Current children cumulated vsize (Kb) 208908

[startup+200.017 s]
Raw data (loadavg): 0.99 0.96 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 19374 302 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216848 134845937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 196.81
Current children cumulated vsize (Kb) 208908

[startup+210.018 s]
Raw data (loadavg): 0.99 0.96 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 20374 302 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216784 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 206.81
Current children cumulated vsize (Kb) 208908

[startup+220.019 s]
Raw data (loadavg): 0.99 0.96 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 21374 302 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216272 134844725 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 216.81
Current children cumulated vsize (Kb) 208908

[startup+230.019 s]
Raw data (loadavg): 0.99 0.96 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 22375 302 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216864 134843012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 226.82
Current children cumulated vsize (Kb) 208908

[startup+240.02 s]
Raw data (loadavg): 0.99 0.96 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 23375 302 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216524 134843002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 236.82
Current children cumulated vsize (Kb) 208908

[startup+250.02 s]
Raw data (loadavg): 0.99 0.96 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 24375 302 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216544 134628768 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 246.82
Current children cumulated vsize (Kb) 208908

[startup+260.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 25375 302 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216824 134842997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 256.82
Current children cumulated vsize (Kb) 208908

[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 26375 302 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217584 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 266.82
Current children cumulated vsize (Kb) 208908

[startup+280.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 27375 302 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216736 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 276.82
Current children cumulated vsize (Kb) 208908

[startup+290.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 28376 302 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217072 134629138 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 286.83
Current children cumulated vsize (Kb) 208908

[startup+300.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 29376 302 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216624 134844866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 296.83
Current children cumulated vsize (Kb) 208908

[startup+310.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 30376 302 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216448 134844689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 306.83
Current children cumulated vsize (Kb) 208908

[startup+320.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 31376 302 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216528 134696565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 316.83
Current children cumulated vsize (Kb) 208908

[startup+330.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 32377 302 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216896 134629270 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 326.84
Current children cumulated vsize (Kb) 208908

[startup+340.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 33377 302 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217328 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 336.84
Current children cumulated vsize (Kb) 208908

[startup+350.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 34377 302 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216528 134693561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 346.84
Current children cumulated vsize (Kb) 208908

[startup+360.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 35377 303 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217024 134722521 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 356.85
Current children cumulated vsize (Kb) 208908

[startup+370.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 36377 303 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216812 134723236 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 366.85
Current children cumulated vsize (Kb) 208908

[startup+380.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 37378 303 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216624 134843160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 376.86
Current children cumulated vsize (Kb) 208908

[startup+390.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 38377 304 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216720 134630795 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 386.86
Current children cumulated vsize (Kb) 208908

[startup+400.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 39377 304 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216720 134629290 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 396.86
Current children cumulated vsize (Kb) 208908

[startup+410.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 40377 304 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216800 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 406.86
Current children cumulated vsize (Kb) 208908

[startup+420.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 41377 305 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217424 134630940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 416.87
Current children cumulated vsize (Kb) 208908

[startup+430.034 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 42377 305 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217028 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 426.87
Current children cumulated vsize (Kb) 208908

[startup+440.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 43377 305 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216688 134694495 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 436.87
Current children cumulated vsize (Kb) 208908

[startup+450.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 44377 305 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217152 134843160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 446.87
Current children cumulated vsize (Kb) 208908

[startup+460.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 45377 305 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216692 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 456.87
Current children cumulated vsize (Kb) 208908

[startup+470.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 46377 306 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217200 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 466.88
Current children cumulated vsize (Kb) 208908

[startup+480.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 47377 306 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216832 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 476.88
Current children cumulated vsize (Kb) 208908

[startup+490.038 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 48378 306 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216832 134720464 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 486.89
Current children cumulated vsize (Kb) 208908

[startup+500.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 49378 306 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216868 134849060 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 496.89
Current children cumulated vsize (Kb) 208908

[startup+510.04 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 50378 306 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216688 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 506.89
Current children cumulated vsize (Kb) 208908

[startup+520.041 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 51378 306 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216208 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 516.89
Current children cumulated vsize (Kb) 208908

[startup+530.041 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 52378 306 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217184 134718188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 526.89
Current children cumulated vsize (Kb) 208908

[startup+540.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 53378 306 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217264 134844653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 536.89
Current children cumulated vsize (Kb) 208908

[startup+550.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 54379 306 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216704 134849082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 546.9
Current children cumulated vsize (Kb) 208908

[startup+560.043 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 55379 306 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216976 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 556.9
Current children cumulated vsize (Kb) 208908

[startup+570.043 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 56379 307 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216652 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 566.91
Current children cumulated vsize (Kb) 208908

[startup+580.044 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 57379 307 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217328 134844720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 576.91
Current children cumulated vsize (Kb) 208908

[startup+590.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 58379 307 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217340 134843002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 586.91
Current children cumulated vsize (Kb) 208908

[startup+600.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 59380 307 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217020 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 596.92
Current children cumulated vsize (Kb) 208908

[startup+610.046 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 60380 307 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216672 134849153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 606.92
Current children cumulated vsize (Kb) 208908

[startup+620.047 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 61380 307 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217216 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 616.92
Current children cumulated vsize (Kb) 208908

[startup+630.047 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 62380 307 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217548 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 626.92
Current children cumulated vsize (Kb) 208908

[startup+640.048 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 63380 307 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216888 134843032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 636.92
Current children cumulated vsize (Kb) 208908

[startup+650.048 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 64381 307 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216664 134845877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 646.93
Current children cumulated vsize (Kb) 208908

[startup+660.049 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 65381 307 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216992 134696572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 656.93
Current children cumulated vsize (Kb) 208908

[startup+670.048 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 66381 307 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216448 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 666.93
Current children cumulated vsize (Kb) 208908

[startup+680.05 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 67381 307 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216508 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 676.93
Current children cumulated vsize (Kb) 208908

[startup+690.051 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 68381 307 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216904 134629086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 686.93
Current children cumulated vsize (Kb) 208908

[startup+700.051 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 69381 307 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216288 134843400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 696.93
Current children cumulated vsize (Kb) 208908

[startup+710.052 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 70382 307 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216832 134720470 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 706.94
Current children cumulated vsize (Kb) 208908

[startup+720.053 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 71382 307 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217068 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 716.94
Current children cumulated vsize (Kb) 208908

[startup+730.053 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 72382 307 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216524 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 726.94
Current children cumulated vsize (Kb) 208908

[startup+740.054 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 73382 307 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216704 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 736.94
Current children cumulated vsize (Kb) 208908

[startup+750.055 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 74382 307 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217072 134630795 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 746.94
Current children cumulated vsize (Kb) 208908

[startup+760.056 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 75383 307 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216844 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 756.95
Current children cumulated vsize (Kb) 208908

[startup+770.057 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 76383 307 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216816 134696273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 766.95
Current children cumulated vsize (Kb) 208908

[startup+780.058 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 77383 307 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217008 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 776.95
Current children cumulated vsize (Kb) 208908

[startup+790.059 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 78384 307 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216448 134844720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 786.96
Current children cumulated vsize (Kb) 208908

[startup+800.059 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 79383 308 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217152 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 796.96
Current children cumulated vsize (Kb) 208908

[startup+810.06 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 80384 308 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216608 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 806.97
Current children cumulated vsize (Kb) 208908

[startup+820.061 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 81384 308 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216864 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 816.97
Current children cumulated vsize (Kb) 208908

[startup+830.061 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 82384 308 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217056 134849193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 826.97
Current children cumulated vsize (Kb) 208908

[startup+840.062 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 83385 308 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216284 134723251 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 836.98
Current children cumulated vsize (Kb) 208908

[startup+850.063 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 84385 308 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216484 134845938 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 846.98
Current children cumulated vsize (Kb) 208908

[startup+860.064 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 85385 308 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217060 134843000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 856.98
Current children cumulated vsize (Kb) 208908

[startup+870.063 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 86385 308 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217028 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 866.98
Current children cumulated vsize (Kb) 208908

[startup+880.064 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 87385 308 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217136 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 876.98
Current children cumulated vsize (Kb) 208908

[startup+890.065 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 88385 308 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217564 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 886.98
Current children cumulated vsize (Kb) 208908

[startup+900.065 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 89386 308 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217136 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 896.99
Current children cumulated vsize (Kb) 208908

[startup+910.066 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 90386 308 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216800 134845906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 906.99
Current children cumulated vsize (Kb) 208908

[startup+920.067 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 91386 308 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217212 134722208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 916.99
Current children cumulated vsize (Kb) 208908

[startup+930.067 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 92386 308 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216640 134849108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 926.99
Current children cumulated vsize (Kb) 208908

[startup+940.068 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 93387 308 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217328 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 937
Current children cumulated vsize (Kb) 208908

[startup+950.068 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 94387 308 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217616 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 947
Current children cumulated vsize (Kb) 208908

[startup+960.069 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 95387 308 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217552 134722539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 957
Current children cumulated vsize (Kb) 208908

[startup+970.069 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 96387 308 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216752 134844689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 967
Current children cumulated vsize (Kb) 208908

[startup+980.07 s]
Raw data (loadavg): 1.07 0.99 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 97387 308 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216888 134696561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 977
Current children cumulated vsize (Kb) 208908

[startup+990.071 s]
Raw data (loadavg): 1.06 0.99 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 98387 309 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217180 134844638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 987.01
Current children cumulated vsize (Kb) 208908

[startup+1000.07 s]
Raw data (loadavg): 1.05 0.99 0.98 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 99386 310 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216512 134849068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 997.01
Current children cumulated vsize (Kb) 208908

[startup+1010.07 s]
Raw data (loadavg): 1.12 1.00 0.99 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 100386 310 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217040 134522732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 1007.01
Current children cumulated vsize (Kb) 208908

[startup+1020.07 s]
Raw data (loadavg): 1.10 1.00 0.99 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 101386 311 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217328 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 1017.02
Current children cumulated vsize (Kb) 208908

[startup+1030.07 s]
Raw data (loadavg): 1.09 1.00 0.99 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 102386 311 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216860 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 1027.02
Current children cumulated vsize (Kb) 208908

[startup+1040.07 s]
Raw data (loadavg): 1.07 1.00 0.99 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 103386 311 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216536 134849057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 1037.02
Current children cumulated vsize (Kb) 208908

[startup+1050.07 s]
Raw data (loadavg): 1.06 1.00 0.99 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 104386 311 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217216 134843400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 1047.02
Current children cumulated vsize (Kb) 208908

[startup+1060.07 s]
Raw data (loadavg): 1.05 1.00 0.99 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 105387 311 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216800 134844718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 1057.03
Current children cumulated vsize (Kb) 208908

[startup+1070.08 s]
Raw data (loadavg): 1.04 1.00 0.99 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 106387 311 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216752 134844723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 1067.03
Current children cumulated vsize (Kb) 208908

[startup+1080.08 s]
Raw data (loadavg): 1.04 1.00 0.99 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 107387 311 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217036 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 1077.03
Current children cumulated vsize (Kb) 208908

[startup+1090.08 s]
Raw data (loadavg): 1.03 1.00 0.99 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 108387 311 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216624 134843012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 1087.03
Current children cumulated vsize (Kb) 208908

[startup+1100.08 s]
Raw data (loadavg): 1.02 1.00 0.99 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 109387 312 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217152 134696342 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 1097.04
Current children cumulated vsize (Kb) 208908

[startup+1110.08 s]
Raw data (loadavg): 1.02 1.00 0.99 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 110387 312 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217212 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 1107.04
Current children cumulated vsize (Kb) 208908

[startup+1120.08 s]
Raw data (loadavg): 1.02 1.00 0.99 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 111387 312 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217760 134694345 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 1117.04
Current children cumulated vsize (Kb) 208908

[startup+1130.08 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 112387 312 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217056 134693570 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 1127.04
Current children cumulated vsize (Kb) 208908

[startup+1140.08 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 113388 312 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217360 134722532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 1137.05
Current children cumulated vsize (Kb) 208908

[startup+1150.08 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 114388 312 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217152 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 1147.05
Current children cumulated vsize (Kb) 208908

[startup+1160.08 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 115388 312 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216596 134844636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 1157.05
Current children cumulated vsize (Kb) 208908

[startup+1170.08 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 116388 312 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221216852 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 1167.05
Current children cumulated vsize (Kb) 208908

[startup+1180.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 117388 312 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217424 134629045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 1177.05
Current children cumulated vsize (Kb) 208908

[startup+1190.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 118389 312 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217504 134845890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 1187.06
Current children cumulated vsize (Kb) 208908

[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 119388 312 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217392 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 1197.05
Current children cumulated vsize (Kb) 208908

[startup+1210.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 120389 312 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217420 134522184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 1207.06
Current children cumulated vsize (Kb) 208908



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 7486
Raw data (/proc/7481/stat): 7481 (minisat+_script) S 7480 7481 19316 0 -1 0 314 389 0 0 0 1 2 2 20 0 1 0 1855988004 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7481/statm): 532 234 485 147 0 385 0
[pid=7481] vsize: 2128
Raw data (/proc/7486/stat): 7486 (minisat+_bignum) R 7481 7481 19316 0 -1 0 72965 0 0 0 120389 312 0 0 25 0 1 0 1855988013 211742720 51471 4294967295 134512640 135167914 3221224448 3221217568 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7486/statm): 51695 51471 162 162 0 51533 0
[pid=7486] vsize: 206780
Current children cumulated CPU time (s) 1207.06
Current children cumulated vsize (Kb) 208908

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

Child status: 0
Real time (s): 1210.18
CPU time (s): 1207.12
CPU user time (s): 1203.89
CPU system time (s): 3.22451
CPU usage (%): 99.7466
Max. virtual memory (cumulated for all children) (Kb): 240820

Verifier Data

ERROR: no interpretation found !