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/unibo/normalized-mps-v2-13-7-rail507.opb
MD5SUM323cdddd9985e43f8e7199c63ad6de47
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 35456000000000
Optimality of the best value was proved NO
Number of terms in the objective function 63209
Biggest coefficient in the objective function 52428800000000000
Number of bits for the biggest coefficient in the objective function 56
Sum of the numbers in the objective function 226433975012582900
Number of bits of the sum of numbers in the objective function 58
Biggest number in a constraint 52428800000000000
Number of bits of the biggest number in a constraint 56
Biggest sum of numbers in a constraint 226433975012582900
Number of bits of the biggest sum of numbers58
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1204.1
Number of variables63009
Total number of constraints63518
Number of constraints which are clauses507
Number of constraints which are cardinality constraints (but not clauses)63011
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint59416

Trace number 6334

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        899432 kB
Buffers:         22004 kB
Cached:          85132 kB
SwapCached:        848 kB
Active:          32720 kB
Inactive:        76972 kB
HighTotal:      131008 kB
HighFree:        44828 kB
LowTotal:       903652 kB
LowFree:        854604 kB
SwapTotal:     2097892 kB
SwapFree:      2096432 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5508 kB
Slab:            19972 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 06:00:34 (client local time) WITH STATUS 0 IN 1208.32 SECONDS
stats: 3496 7 1208.32 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 63023] 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/1244/stat): 1244 (minisat+_script) R 1243 1244 5929 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1856073853 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/1244/statm): 174 3 169 147 0 27 0
[pid=1244] 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=1245
New process pid=1246
New process pid=1247
execve syscall for /bin/sed executable
One traced child (pid=1246) 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=1247) exited with status: 0
One traced child (pid=1245) exited with status: 0
New process pid=1248
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-rail507.opb
One traced child (pid=1248) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=1249
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-rail507.opb

[startup+10.0037 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 3399 0 0 0 870 23 0 0 25 0 1 0 1856073933 13750272 3166 4294967295 134512640 135167914 3221224448 3221223008 134844866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 3357 3166 162 162 0 3195 0
[pid=1249] vsize: 13428
Current children cumulated CPU time (s) 9.57
Current children cumulated vsize (Kb) 15556

[startup+20.0045 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 6859 0 0 0 1830 41 0 0 25 0 1 0 1856073933 23855104 5602 4294967295 134512640 135167914 3221224448 3221219732 134581188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1249/statm): 5824 5602 162 162 0 5662 0
[pid=1249] vsize: 23296
Current children cumulated CPU time (s) 19.35
Current children cumulated vsize (Kb) 25424

[startup+30.0043 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 11074 0 0 0 2783 61 0 0 25 0 1 0 1856073933 33779712 7983 4294967295 134512640 135167914 3221224448 3221222672 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 8247 7983 162 162 0 8085 0
[pid=1249] vsize: 32988
Current children cumulated CPU time (s) 29.08
Current children cumulated vsize (Kb) 35116

[startup+40.0051 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 16521 0 0 0 3728 86 0 0 25 0 1 0 1856073933 44953600 10717 4294967295 134512640 135167914 3221224448 3221223200 134691231 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 10975 10717 162 162 0 10813 0
[pid=1249] vsize: 43900
Current children cumulated CPU time (s) 38.78
Current children cumulated vsize (Kb) 46028

[startup+50.0059 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 21920 0 0 0 4697 105 0 0 25 0 1 0 1856073933 67076096 16116 4294967295 134512640 135167914 3221224448 3208653984 134844647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1249/statm): 16376 16116 162 162 0 16214 0
[pid=1249] vsize: 65504
Current children cumulated CPU time (s) 48.66
Current children cumulated vsize (Kb) 67632

[startup+60.0067 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 21940 0 0 0 5696 105 0 0 25 0 1 0 1856073933 67186688 16136 4294967295 134512640 135167914 3221224448 3208986064 134624577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16403 16136 162 162 0 16241 0
[pid=1249] vsize: 65612
Current children cumulated CPU time (s) 58.65
Current children cumulated vsize (Kb) 67740

[startup+70.0075 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 21984 0 0 0 6696 105 0 0 25 0 1 0 1856073933 67354624 16180 4294967295 134512640 135167914 3221224448 3209228768 134845890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16444 16180 162 162 0 16282 0
[pid=1249] vsize: 65776
Current children cumulated CPU time (s) 68.65
Current children cumulated vsize (Kb) 67904

[startup+80.0083 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 21987 0 0 0 7696 105 0 0 25 0 1 0 1856073933 67354624 16183 4294967295 134512640 135167914 3221224448 3209429232 134845895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16444 16183 162 162 0 16282 0
[pid=1249] vsize: 65776
Current children cumulated CPU time (s) 78.65
Current children cumulated vsize (Kb) 67904

[startup+90.0091 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 21989 0 0 0 8697 105 0 0 25 0 1 0 1856073933 67354624 16185 4294967295 134512640 135167914 3221224448 3209602688 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16444 16185 162 162 0 16282 0
[pid=1249] vsize: 65776
Current children cumulated CPU time (s) 88.66
Current children cumulated vsize (Kb) 67904

[startup+100.01 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22019 0 0 0 9697 105 0 0 25 0 1 0 1856073933 67567616 16215 4294967295 134512640 135167914 3221224448 3209757696 134694394 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16496 16215 162 162 0 16334 0
[pid=1249] vsize: 65984
Current children cumulated CPU time (s) 98.66
Current children cumulated vsize (Kb) 68112

[startup+110.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22020 0 0 0 10697 105 0 0 25 0 1 0 1856073933 67567616 16216 4294967295 134512640 135167914 3221224448 3209899504 134693561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16496 16216 162 162 0 16334 0
[pid=1249] vsize: 65984
Current children cumulated CPU time (s) 108.66
Current children cumulated vsize (Kb) 68112

[startup+120.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22022 0 0 0 11697 106 0 0 25 0 1 0 1856073933 67567616 16218 4294967295 134512640 135167914 3221224448 3210030964 134845938 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16496 16218 162 162 0 16334 0
[pid=1249] vsize: 65984
Current children cumulated CPU time (s) 118.67
Current children cumulated vsize (Kb) 68112

[startup+130.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22024 0 0 0 12697 106 0 0 25 0 1 0 1856073933 67567616 16220 4294967295 134512640 135167914 3221224448 3210153932 134844675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16496 16220 162 162 0 16334 0
[pid=1249] vsize: 65984
Current children cumulated CPU time (s) 128.67
Current children cumulated vsize (Kb) 68112

[startup+140.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22109 0 0 0 13697 106 0 0 25 0 1 0 1856073933 67911680 16305 4294967295 134512640 135167914 3221224448 3210269788 134693585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16580 16305 162 162 0 16418 0
[pid=1249] vsize: 66320
Current children cumulated CPU time (s) 138.67
Current children cumulated vsize (Kb) 68448

[startup+150.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22111 0 0 0 14696 107 0 0 25 0 1 0 1856073933 67911680 16307 4294967295 134512640 135167914 3221224448 3210379776 134624627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16580 16307 162 162 0 16418 0
[pid=1249] vsize: 66320
Current children cumulated CPU time (s) 148.67
Current children cumulated vsize (Kb) 68448

[startup+160.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22112 0 0 0 15695 108 0 0 25 0 1 0 1856073933 67911680 16308 4294967295 134512640 135167914 3221224448 3210484960 134845901 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16580 16308 162 162 0 16418 0
[pid=1249] vsize: 66320
Current children cumulated CPU time (s) 158.67
Current children cumulated vsize (Kb) 68448

[startup+170.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22113 0 0 0 16695 109 0 0 25 0 1 0 1856073933 67911680 16309 4294967295 134512640 135167914 3221224448 3210585920 134844697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16580 16309 162 162 0 16418 0
[pid=1249] vsize: 66320
Current children cumulated CPU time (s) 168.68
Current children cumulated vsize (Kb) 68448

[startup+180.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22115 0 0 0 17695 109 0 0 25 0 1 0 1856073933 67911680 16311 4294967295 134512640 135167914 3221224448 3210683072 134624796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16580 16311 162 162 0 16418 0
[pid=1249] vsize: 66320
Current children cumulated CPU time (s) 178.68
Current children cumulated vsize (Kb) 68448

[startup+190.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22116 0 0 0 18695 110 0 0 25 0 1 0 1856073933 67911680 16312 4294967295 134512640 135167914 3221224448 3210776608 134843113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16580 16312 162 162 0 16418 0
[pid=1249] vsize: 66320
Current children cumulated CPU time (s) 188.69
Current children cumulated vsize (Kb) 68448

[startup+200.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22117 0 0 0 19695 110 0 0 25 0 1 0 1856073933 67911680 16313 4294967295 134512640 135167914 3221224448 3210867164 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16580 16313 162 162 0 16418 0
[pid=1249] vsize: 66320
Current children cumulated CPU time (s) 198.69
Current children cumulated vsize (Kb) 68448

[startup+210.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22118 0 0 0 20695 110 0 0 25 0 1 0 1856073933 67911680 16314 4294967295 134512640 135167914 3221224448 3210954748 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16580 16314 162 162 0 16418 0
[pid=1249] vsize: 66320
Current children cumulated CPU time (s) 208.69
Current children cumulated vsize (Kb) 68448

[startup+220.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22119 0 0 0 21695 110 0 0 25 0 1 0 1856073933 67911680 16315 4294967295 134512640 135167914 3221224448 3211040032 134845901 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16580 16315 162 162 0 16418 0
[pid=1249] vsize: 66320
Current children cumulated CPU time (s) 218.69
Current children cumulated vsize (Kb) 68448

[startup+230.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22120 0 0 0 22695 110 0 0 25 0 1 0 1856073933 67911680 16316 4294967295 134512640 135167914 3221224448 3211122800 134624423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16580 16316 162 162 0 16418 0
[pid=1249] vsize: 66320
Current children cumulated CPU time (s) 228.69
Current children cumulated vsize (Kb) 68448

[startup+240.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22122 0 0 0 23695 110 0 0 25 0 1 0 1856073933 67911680 16318 4294967295 134512640 135167914 3221224448 3211203420 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16580 16318 162 162 0 16418 0
[pid=1249] vsize: 66320
Current children cumulated CPU time (s) 238.69
Current children cumulated vsize (Kb) 68448

[startup+250.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22123 0 0 0 24695 110 0 0 25 0 1 0 1856073933 67911680 16319 4294967295 134512640 135167914 3221224448 3211282064 134624545 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16580 16319 162 162 0 16418 0
[pid=1249] vsize: 66320
Current children cumulated CPU time (s) 248.69
Current children cumulated vsize (Kb) 68448

[startup+260.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22124 0 0 0 25695 111 0 0 25 0 1 0 1856073933 67911680 16320 4294967295 134512640 135167914 3221224448 3211358988 134844632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16580 16320 162 162 0 16418 0
[pid=1249] vsize: 66320
Current children cumulated CPU time (s) 258.7
Current children cumulated vsize (Kb) 68448

[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22127 0 0 0 26695 111 0 0 25 0 1 0 1856073933 67919872 16323 4294967295 134512640 135167914 3221224448 3211434112 134843107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16582 16323 162 162 0 16420 0
[pid=1249] vsize: 66328
Current children cumulated CPU time (s) 268.7
Current children cumulated vsize (Kb) 68456

[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22130 0 0 0 27695 111 0 0 25 0 1 0 1856073933 67932160 16326 4294967295 134512640 135167914 3221224448 3211507848 134624787 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16585 16326 162 162 0 16423 0
[pid=1249] vsize: 66340
Current children cumulated CPU time (s) 278.7
Current children cumulated vsize (Kb) 68468

[startup+290.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22134 0 0 0 28695 111 0 0 25 0 1 0 1856073933 67944448 16330 4294967295 134512640 135167914 3221224448 3211579856 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16588 16330 162 162 0 16426 0
[pid=1249] vsize: 66352
Current children cumulated CPU time (s) 288.7
Current children cumulated vsize (Kb) 68480

[startup+300.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22138 0 0 0 29695 111 0 0 25 0 1 0 1856073933 68153344 16334 4294967295 134512640 135167914 3221224448 3211650720 134694394 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16639 16334 162 162 0 16477 0
[pid=1249] vsize: 66556
Current children cumulated CPU time (s) 298.7
Current children cumulated vsize (Kb) 68684

[startup+310.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22142 0 0 0 30696 111 0 0 25 0 1 0 1856073933 68165632 16338 4294967295 134512640 135167914 3221224448 3211719872 134843404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16642 16338 162 162 0 16480 0
[pid=1249] vsize: 66568
Current children cumulated CPU time (s) 308.71
Current children cumulated vsize (Kb) 68696

[startup+320.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22145 0 0 0 31696 111 0 0 25 0 1 0 1856073933 68173824 16341 4294967295 134512640 135167914 3221224448 3211788032 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16644 16341 162 162 0 16482 0
[pid=1249] vsize: 66576
Current children cumulated CPU time (s) 318.71
Current children cumulated vsize (Kb) 68704

[startup+330.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22149 0 0 0 32696 112 0 0 25 0 1 0 1856073933 68186112 16345 4294967295 134512640 135167914 3221224448 3211855008 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16647 16345 162 162 0 16485 0
[pid=1249] vsize: 66588
Current children cumulated CPU time (s) 328.72
Current children cumulated vsize (Kb) 68716

[startup+340.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22153 0 0 0 33696 112 0 0 25 0 1 0 1856073933 68198400 16349 4294967295 134512640 135167914 3221224448 3211920896 134624627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16650 16349 162 162 0 16488 0
[pid=1249] vsize: 66600
Current children cumulated CPU time (s) 338.72
Current children cumulated vsize (Kb) 68728

[startup+350.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22156 0 0 0 34696 112 0 0 25 0 1 0 1856073933 68206592 16352 4294967295 134512640 135167914 3221224448 3211985564 134844638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16652 16352 162 162 0 16490 0
[pid=1249] vsize: 66608
Current children cumulated CPU time (s) 348.72
Current children cumulated vsize (Kb) 68736

[startup+360.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22160 0 0 0 35696 112 0 0 25 0 1 0 1856073933 68218880 16356 4294967295 134512640 135167914 3221224448 3212049264 134624545 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16655 16356 162 162 0 16493 0
[pid=1249] vsize: 66620
Current children cumulated CPU time (s) 358.72
Current children cumulated vsize (Kb) 68748

[startup+370.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22163 0 0 0 36696 112 0 0 25 0 1 0 1856073933 68231168 16359 4294967295 134512640 135167914 3221224448 3212111872 134844725 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16658 16359 162 162 0 16496 0
[pid=1249] vsize: 66632
Current children cumulated CPU time (s) 368.72
Current children cumulated vsize (Kb) 68760

[startup+380.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22166 0 0 0 37696 112 0 0 25 0 1 0 1856073933 68239360 16362 4294967295 134512640 135167914 3221224448 3212173756 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16660 16362 162 162 0 16498 0
[pid=1249] vsize: 66640
Current children cumulated CPU time (s) 378.72
Current children cumulated vsize (Kb) 68768

[startup+390.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22169 0 0 0 38696 112 0 0 25 0 1 0 1856073933 68247552 16365 4294967295 134512640 135167914 3221224448 3212234624 134844718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16662 16365 162 162 0 16500 0
[pid=1249] vsize: 66648
Current children cumulated CPU time (s) 388.72
Current children cumulated vsize (Kb) 68776

[startup+400.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22173 0 0 0 39696 112 0 0 25 0 1 0 1856073933 68259840 16369 4294967295 134512640 135167914 3221224448 3212294688 134845937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16665 16369 162 162 0 16503 0
[pid=1249] vsize: 66660
Current children cumulated CPU time (s) 398.72
Current children cumulated vsize (Kb) 68788

[startup+410.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22176 0 0 0 40697 112 0 0 25 0 1 0 1856073933 68268032 16372 4294967295 134512640 135167914 3221224448 3212354100 134849060 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16667 16372 162 162 0 16505 0
[pid=1249] vsize: 66668
Current children cumulated CPU time (s) 408.73
Current children cumulated vsize (Kb) 68796

[startup+420.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22178 0 0 0 41697 112 0 0 25 0 1 0 1856073933 68276224 16374 4294967295 134512640 135167914 3221224448 3212412480 134843107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16669 16374 162 162 0 16507 0
[pid=1249] vsize: 66676
Current children cumulated CPU time (s) 418.73
Current children cumulated vsize (Kb) 68804

[startup+430.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22182 0 0 0 42697 113 0 0 25 0 1 0 1856073933 68288512 16378 4294967295 134512640 135167914 3221224448 3212470272 134845901 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16672 16378 162 162 0 16510 0
[pid=1249] vsize: 66688
Current children cumulated CPU time (s) 428.74
Current children cumulated vsize (Kb) 68816

[startup+440.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22184 0 0 0 43697 113 0 0 25 0 1 0 1856073933 68292608 16380 4294967295 134512640 135167914 3221224448 3212527168 134843139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16673 16380 162 162 0 16511 0
[pid=1249] vsize: 66692
Current children cumulated CPU time (s) 438.74
Current children cumulated vsize (Kb) 68820

[startup+450.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22188 0 0 0 44697 113 0 0 25 0 1 0 1856073933 68304896 16384 4294967295 134512640 135167914 3221224448 3212583456 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16676 16384 162 162 0 16514 0
[pid=1249] vsize: 66704
Current children cumulated CPU time (s) 448.74
Current children cumulated vsize (Kb) 68832

[startup+460.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22357 0 0 0 45697 113 0 0 25 0 1 0 1856073933 68653056 16469 4294967295 134512640 135167914 3221224448 3212638880 134844703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16761 16469 162 162 0 16599 0
[pid=1249] vsize: 67044
Current children cumulated CPU time (s) 458.74
Current children cumulated vsize (Kb) 69172

[startup+470.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22360 0 0 0 46697 113 0 0 25 0 1 0 1856073933 68661248 16472 4294967295 134512640 135167914 3221224448 3212693824 134844689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16763 16472 162 162 0 16601 0
[pid=1249] vsize: 67052
Current children cumulated CPU time (s) 468.74
Current children cumulated vsize (Kb) 69180

[startup+480.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22362 0 0 0 47697 113 0 0 25 0 1 0 1856073933 68665344 16474 4294967295 134512640 135167914 3221224448 3212748344 134843032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16764 16474 162 162 0 16602 0
[pid=1249] vsize: 67056
Current children cumulated CPU time (s) 478.74
Current children cumulated vsize (Kb) 69184

[startup+490.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22365 0 0 0 48697 113 0 0 25 0 1 0 1856073933 68677632 16477 4294967295 134512640 135167914 3221224448 3212802092 134843002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16767 16477 162 162 0 16605 0
[pid=1249] vsize: 67068
Current children cumulated CPU time (s) 488.74
Current children cumulated vsize (Kb) 69196

[startup+500.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22368 0 0 0 49697 113 0 0 25 0 1 0 1856073933 68685824 16480 4294967295 134512640 135167914 3221224448 3212855164 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16769 16480 162 162 0 16607 0
[pid=1249] vsize: 67076
Current children cumulated CPU time (s) 498.74
Current children cumulated vsize (Kb) 69204

[startup+510.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22371 0 0 0 50697 113 0 0 25 0 1 0 1856073933 68694016 16483 4294967295 134512640 135167914 3221224448 3212907836 134693552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16771 16483 162 162 0 16609 0
[pid=1249] vsize: 67084
Current children cumulated CPU time (s) 508.74
Current children cumulated vsize (Kb) 69212

[startup+520.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22373 0 0 0 51698 113 0 0 25 0 1 0 1856073933 68702208 16485 4294967295 134512640 135167914 3221224448 3212960048 134624420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16773 16485 162 162 0 16611 0
[pid=1249] vsize: 67092
Current children cumulated CPU time (s) 518.75
Current children cumulated vsize (Kb) 69220

[startup+530.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22376 0 0 0 52698 113 0 0 25 0 1 0 1856073933 68710400 16488 4294967295 134512640 135167914 3221224448 3213011512 134845877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16775 16488 162 162 0 16613 0
[pid=1249] vsize: 67100
Current children cumulated CPU time (s) 528.75
Current children cumulated vsize (Kb) 69228

[startup+540.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22380 0 0 0 53698 113 0 0 25 0 1 0 1856073933 68722688 16492 4294967295 134512640 135167914 3221224448 3213062396 134694368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16778 16492 162 162 0 16616 0
[pid=1249] vsize: 67112
Current children cumulated CPU time (s) 538.75
Current children cumulated vsize (Kb) 69240

[startup+550.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22381 0 0 0 54698 113 0 0 25 0 1 0 1856073933 68726784 16493 4294967295 134512640 135167914 3221224448 3213112992 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16779 16493 162 162 0 16617 0
[pid=1249] vsize: 67116
Current children cumulated CPU time (s) 548.75
Current children cumulated vsize (Kb) 69244

[startup+560.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22384 0 0 0 55698 114 0 0 25 0 1 0 1856073933 68734976 16496 4294967295 134512640 135167914 3221224448 3213162864 134845903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16781 16496 162 162 0 16619 0
[pid=1249] vsize: 67124
Current children cumulated CPU time (s) 558.76
Current children cumulated vsize (Kb) 69252

[startup+570.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22387 0 0 0 56698 114 0 0 25 0 1 0 1856073933 68743168 16499 4294967295 134512640 135167914 3221224448 3213212672 134694394 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16783 16499 162 162 0 16621 0
[pid=1249] vsize: 67132
Current children cumulated CPU time (s) 568.76
Current children cumulated vsize (Kb) 69260

[startup+580.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22389 0 0 0 57699 114 0 0 25 0 1 0 1856073933 68751360 16501 4294967295 134512640 135167914 3221224448 3213261728 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16785 16501 162 162 0 16623 0
[pid=1249] vsize: 67140
Current children cumulated CPU time (s) 578.77
Current children cumulated vsize (Kb) 69268

[startup+590.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22392 0 0 0 58699 114 0 0 25 0 1 0 1856073933 68759552 16504 4294967295 134512640 135167914 3221224448 3213310308 134845938 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16787 16504 162 162 0 16625 0
[pid=1249] vsize: 67148
Current children cumulated CPU time (s) 588.77
Current children cumulated vsize (Kb) 69276

[startup+600.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22395 0 0 0 59699 114 0 0 25 0 1 0 1856073933 68767744 16507 4294967295 134512640 135167914 3221224448 3213358544 134624545 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16789 16507 162 162 0 16627 0
[pid=1249] vsize: 67156
Current children cumulated CPU time (s) 598.77
Current children cumulated vsize (Kb) 69284

[startup+610.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22397 0 0 0 60699 114 0 0 25 0 1 0 1856073933 68775936 16509 4294967295 134512640 135167914 3221224448 3213406480 134624420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16791 16509 162 162 0 16629 0
[pid=1249] vsize: 67164
Current children cumulated CPU time (s) 608.77
Current children cumulated vsize (Kb) 69292

[startup+620.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22400 0 0 0 61699 114 0 0 25 0 1 0 1856073933 68784128 16512 4294967295 134512640 135167914 3221224448 3213453724 134694368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16793 16512 162 162 0 16631 0
[pid=1249] vsize: 67172
Current children cumulated CPU time (s) 618.77
Current children cumulated vsize (Kb) 69300

[startup+630.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22402 0 0 0 62700 114 0 0 25 0 1 0 1856073933 68788224 16514 4294967295 134512640 135167914 3221224448 3213500704 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16794 16514 162 162 0 16632 0
[pid=1249] vsize: 67176
Current children cumulated CPU time (s) 628.78
Current children cumulated vsize (Kb) 69304

[startup+640.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22404 0 0 0 63699 114 0 0 25 0 1 0 1856073933 68796416 16516 4294967295 134512640 135167914 3221224448 3213547328 134843400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16796 16516 162 162 0 16634 0
[pid=1249] vsize: 67184
Current children cumulated CPU time (s) 638.77
Current children cumulated vsize (Kb) 69312

[startup+650.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22408 0 0 0 64699 114 0 0 25 0 1 0 1856073933 68808704 16520 4294967295 134512640 135167914 3221224448 3213593408 134844736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16799 16520 162 162 0 16637 0
[pid=1249] vsize: 67196
Current children cumulated CPU time (s) 648.77
Current children cumulated vsize (Kb) 69324

[startup+660.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22409 0 0 0 65700 114 0 0 25 0 1 0 1856073933 68812800 16521 4294967295 134512640 135167914 3221224448 3213639088 134845921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16800 16521 162 162 0 16638 0
[pid=1249] vsize: 67200
Current children cumulated CPU time (s) 658.78
Current children cumulated vsize (Kb) 69328

[startup+670.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22412 0 0 0 66700 114 0 0 25 0 1 0 1856073933 68820992 16524 4294967295 134512640 135167914 3221224448 3213684892 134694368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16802 16524 162 162 0 16640 0
[pid=1249] vsize: 67208
Current children cumulated CPU time (s) 668.78
Current children cumulated vsize (Kb) 69336

[startup+680.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22415 0 0 0 67700 114 0 0 25 0 1 0 1856073933 68829184 16527 4294967295 134512640 135167914 3221224448 3213729936 134624420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16804 16527 162 162 0 16642 0
[pid=1249] vsize: 67216
Current children cumulated CPU time (s) 678.78
Current children cumulated vsize (Kb) 69344

[startup+690.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22417 0 0 0 68700 114 0 0 25 0 1 0 1856073933 68837376 16529 4294967295 134512640 135167914 3221224448 3213774624 134844736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16806 16529 162 162 0 16644 0
[pid=1249] vsize: 67224
Current children cumulated CPU time (s) 688.78
Current children cumulated vsize (Kb) 69352

[startup+700.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22420 0 0 0 69701 114 0 0 25 0 1 0 1856073933 68845568 16532 4294967295 134512640 135167914 3221224448 3213818976 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16808 16532 162 162 0 16646 0
[pid=1249] vsize: 67232
Current children cumulated CPU time (s) 698.79
Current children cumulated vsize (Kb) 69360

[startup+710.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22421 0 0 0 70701 114 0 0 25 0 1 0 1856073933 68849664 16533 4294967295 134512640 135167914 3221224448 3213863104 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16809 16533 162 162 0 16647 0
[pid=1249] vsize: 67236
Current children cumulated CPU time (s) 708.79
Current children cumulated vsize (Kb) 69364

[startup+720.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22424 0 0 0 71701 115 0 0 25 0 1 0 1856073933 68857856 16536 4294967295 134512640 135167914 3221224448 3213906816 134722532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16811 16536 162 162 0 16649 0
[pid=1249] vsize: 67244
Current children cumulated CPU time (s) 718.8
Current children cumulated vsize (Kb) 69372

[startup+730.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22426 0 0 0 72701 115 0 0 25 0 1 0 1856073933 68866048 16538 4294967295 134512640 135167914 3221224448 3213950276 134845938 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16813 16538 162 162 0 16651 0
[pid=1249] vsize: 67252
Current children cumulated CPU time (s) 728.8
Current children cumulated vsize (Kb) 69380

[startup+740.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22429 0 0 0 73701 115 0 0 25 0 1 0 1856073933 68874240 16541 4294967295 134512640 135167914 3221224448 3213993552 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16815 16541 162 162 0 16653 0
[pid=1249] vsize: 67260
Current children cumulated CPU time (s) 738.8
Current children cumulated vsize (Kb) 69388

[startup+750.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22431 0 0 0 74700 116 0 0 25 0 1 0 1856073933 68878336 16543 4294967295 134512640 135167914 3221224448 3214036288 134722532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16816 16543 162 162 0 16654 0
[pid=1249] vsize: 67264
Current children cumulated CPU time (s) 748.8
Current children cumulated vsize (Kb) 69392

[startup+760.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22432 0 0 0 75699 117 0 0 25 0 1 0 1856073933 68882432 16544 4294967295 134512640 135167914 3221224448 3214078816 134844697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16817 16544 162 162 0 16655 0
[pid=1249] vsize: 67268
Current children cumulated CPU time (s) 758.8
Current children cumulated vsize (Kb) 69396

[startup+770.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22435 0 0 0 76699 117 0 0 25 0 1 0 1856073933 68890624 16547 4294967295 134512640 135167914 3221224448 3214120864 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16819 16547 162 162 0 16657 0
[pid=1249] vsize: 67276
Current children cumulated CPU time (s) 768.8
Current children cumulated vsize (Kb) 69404

[startup+780.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22437 0 0 0 77699 118 0 0 25 0 1 0 1856073933 68898816 16549 4294967295 134512640 135167914 3221224448 3214162892 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16821 16549 162 162 0 16659 0
[pid=1249] vsize: 67284
Current children cumulated CPU time (s) 778.81
Current children cumulated vsize (Kb) 69412

[startup+790.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22440 0 0 0 78699 118 0 0 25 0 1 0 1856073933 68907008 16552 4294967295 134512640 135167914 3221224448 3214204576 134624742 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16823 16552 162 162 0 16661 0
[pid=1249] vsize: 67292
Current children cumulated CPU time (s) 788.81
Current children cumulated vsize (Kb) 69420

[startup+800.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22441 0 0 0 79699 118 0 0 25 0 1 0 1856073933 68911104 16553 4294967295 134512640 135167914 3221224448 3214245980 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16824 16553 162 162 0 16662 0
[pid=1249] vsize: 67296
Current children cumulated CPU time (s) 798.81
Current children cumulated vsize (Kb) 69424

[startup+810.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22444 0 0 0 80699 119 0 0 25 0 1 0 1856073933 68919296 16556 4294967295 134512640 135167914 3221224448 3214287072 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16826 16556 162 162 0 16664 0
[pid=1249] vsize: 67304
Current children cumulated CPU time (s) 808.82
Current children cumulated vsize (Kb) 69432

[startup+820.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22446 0 0 0 81699 119 0 0 25 0 1 0 1856073933 68927488 16558 4294967295 134512640 135167914 3221224448 3214328000 134624796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16828 16558 162 162 0 16666 0
[pid=1249] vsize: 67312
Current children cumulated CPU time (s) 818.82
Current children cumulated vsize (Kb) 69440

[startup+830.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22449 0 0 0 82699 119 0 0 25 0 1 0 1856073933 68935680 16561 4294967295 134512640 135167914 3221224448 3214368736 134843074 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16830 16561 162 162 0 16668 0
[pid=1249] vsize: 67320
Current children cumulated CPU time (s) 828.82
Current children cumulated vsize (Kb) 69448

[startup+840.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22450 0 0 0 83699 119 0 0 25 0 1 0 1856073933 68939776 16562 4294967295 134512640 135167914 3221224448 3214409056 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16831 16562 162 162 0 16669 0
[pid=1249] vsize: 67324
Current children cumulated CPU time (s) 838.82
Current children cumulated vsize (Kb) 69452

[startup+850.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22452 0 0 0 84699 119 0 0 25 0 1 0 1856073933 68943872 16564 4294967295 134512640 135167914 3221224448 3214449168 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16832 16564 162 162 0 16670 0
[pid=1249] vsize: 67328
Current children cumulated CPU time (s) 848.82
Current children cumulated vsize (Kb) 69456

[startup+860.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22454 0 0 0 85699 120 0 0 25 0 1 0 1856073933 68952064 16566 4294967295 134512640 135167914 3221224448 3214489040 134849179 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16834 16566 162 162 0 16672 0
[pid=1249] vsize: 67336
Current children cumulated CPU time (s) 858.83
Current children cumulated vsize (Kb) 69464

[startup+870.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22457 0 0 0 86699 120 0 0 25 0 1 0 1856073933 68960256 16569 4294967295 134512640 135167914 3221224448 3214528608 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16836 16569 162 162 0 16674 0
[pid=1249] vsize: 67344
Current children cumulated CPU time (s) 868.83
Current children cumulated vsize (Kb) 69472

[startup+880.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22459 0 0 0 87700 120 0 0 25 0 1 0 1856073933 68964352 16571 4294967295 134512640 135167914 3221224448 3214568032 134845924 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16837 16571 162 162 0 16675 0
[pid=1249] vsize: 67348
Current children cumulated CPU time (s) 878.84
Current children cumulated vsize (Kb) 69476

[startup+890.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22460 0 0 0 88699 120 0 0 25 0 1 0 1856073933 68968448 16572 4294967295 134512640 135167914 3221224448 3214607320 134843032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16838 16572 162 162 0 16676 0
[pid=1249] vsize: 67352
Current children cumulated CPU time (s) 888.83
Current children cumulated vsize (Kb) 69480

[startup+900.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22463 0 0 0 89700 120 0 0 25 0 1 0 1856073933 68976640 16575 4294967295 134512640 135167914 3221224448 3214646036 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16840 16575 162 162 0 16678 0
[pid=1249] vsize: 67360
Current children cumulated CPU time (s) 898.84
Current children cumulated vsize (Kb) 69488

[startup+910.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22465 0 0 0 90700 120 0 0 25 0 1 0 1856073933 68984832 16577 4294967295 134512640 135167914 3221224448 3214684800 134843012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16842 16577 162 162 0 16680 0
[pid=1249] vsize: 67368
Current children cumulated CPU time (s) 908.84
Current children cumulated vsize (Kb) 69496

[startup+920.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22467 0 0 0 91700 120 0 0 25 0 1 0 1856073933 68988928 16579 4294967295 134512640 135167914 3221224448 3214723264 134844647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16843 16579 162 162 0 16681 0
[pid=1249] vsize: 67372
Current children cumulated CPU time (s) 918.84
Current children cumulated vsize (Kb) 69500

[startup+930.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22469 0 0 0 92700 121 0 0 25 0 1 0 1856073933 68997120 16581 4294967295 134512640 135167914 3221224448 3214761628 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16845 16581 162 162 0 16683 0
[pid=1249] vsize: 67380
Current children cumulated CPU time (s) 928.85
Current children cumulated vsize (Kb) 69508

[startup+940.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22471 0 0 0 93700 121 0 0 25 0 1 0 1856073933 69001216 16583 4294967295 134512640 135167914 3221224448 3214799700 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16846 16583 162 162 0 16684 0
[pid=1249] vsize: 67384
Current children cumulated CPU time (s) 938.85
Current children cumulated vsize (Kb) 69512

[startup+950.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22473 0 0 0 94701 121 0 0 25 0 1 0 1856073933 69009408 16585 4294967295 134512640 135167914 3221224448 3214837568 134849096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16848 16585 162 162 0 16686 0
[pid=1249] vsize: 67392
Current children cumulated CPU time (s) 948.86
Current children cumulated vsize (Kb) 69520

[startup+960.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22475 0 0 0 95701 121 0 0 25 0 1 0 1856073933 69013504 16587 4294967295 134512640 135167914 3221224448 3214875196 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16849 16587 162 162 0 16687 0
[pid=1249] vsize: 67396
Current children cumulated CPU time (s) 958.86
Current children cumulated vsize (Kb) 69524

[startup+970.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22477 0 0 0 96701 121 0 0 25 0 1 0 1856073933 69021696 16589 4294967295 134512640 135167914 3221224448 3214912480 134844641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16851 16589 162 162 0 16689 0
[pid=1249] vsize: 67404
Current children cumulated CPU time (s) 968.86
Current children cumulated vsize (Kb) 69532

[startup+980.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22480 0 0 0 97701 121 0 0 25 0 1 0 1856073933 69029888 16592 4294967295 134512640 135167914 3221224448 3214949808 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16853 16592 162 162 0 16691 0
[pid=1249] vsize: 67412
Current children cumulated CPU time (s) 978.86
Current children cumulated vsize (Kb) 69540

[startup+990.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22480 0 0 0 98701 121 0 0 25 0 1 0 1856073933 69029888 16592 4294967295 134512640 135167914 3221224448 3214986896 134845921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16853 16592 162 162 0 16691 0
[pid=1249] vsize: 67412
Current children cumulated CPU time (s) 988.86
Current children cumulated vsize (Kb) 69540

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22482 0 0 0 99701 121 0 0 25 0 1 0 1856073933 69038080 16594 4294967295 134512640 135167914 3221224448 3215023760 134624577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16855 16594 162 162 0 16693 0
[pid=1249] vsize: 67420
Current children cumulated CPU time (s) 998.86
Current children cumulated vsize (Kb) 69548

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22485 0 0 0 100701 121 0 0 25 0 1 0 1856073933 69046272 16597 4294967295 134512640 135167914 3221224448 3215060360 134844633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16857 16597 162 162 0 16695 0
[pid=1249] vsize: 67428
Current children cumulated CPU time (s) 1008.86
Current children cumulated vsize (Kb) 69556

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22486 0 0 0 101701 121 0 0 25 0 1 0 1856073933 69050368 16598 4294967295 134512640 135167914 3221224448 3215096960 134843132 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16858 16598 162 162 0 16696 0
[pid=1249] vsize: 67432
Current children cumulated CPU time (s) 1018.86
Current children cumulated vsize (Kb) 69560

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22489 0 0 0 102701 122 0 0 25 0 1 0 1856073933 69058560 16601 4294967295 134512640 135167914 3221224448 3215133248 134694419 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16860 16601 162 162 0 16698 0
[pid=1249] vsize: 67440
Current children cumulated CPU time (s) 1028.87
Current children cumulated vsize (Kb) 69568

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22490 0 0 0 103702 122 0 0 25 0 1 0 1856073933 69062656 16602 4294967295 134512640 135167914 3221224448 3215169280 134722527 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16861 16602 162 162 0 16699 0
[pid=1249] vsize: 67444
Current children cumulated CPU time (s) 1038.88
Current children cumulated vsize (Kb) 69572

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22492 0 0 0 104702 122 0 0 25 0 1 0 1856073933 69066752 16604 4294967295 134512640 135167914 3221224448 3215205152 134694428 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16862 16604 162 162 0 16700 0
[pid=1249] vsize: 67448
Current children cumulated CPU time (s) 1048.88
Current children cumulated vsize (Kb) 69576

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22494 0 0 0 105702 122 0 0 25 0 1 0 1856073933 69074944 16606 4294967295 134512640 135167914 3221224448 3215240992 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16864 16606 162 162 0 16702 0
[pid=1249] vsize: 67456
Current children cumulated CPU time (s) 1058.88
Current children cumulated vsize (Kb) 69584

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22496 0 0 0 106702 122 0 0 25 0 1 0 1856073933 69472256 16608 4294967295 134512640 135167914 3221224448 3215276576 134722532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16961 16608 162 162 0 16799 0
[pid=1249] vsize: 67844
Current children cumulated CPU time (s) 1068.88
Current children cumulated vsize (Kb) 69972

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22498 0 0 0 107703 122 0 0 25 0 1 0 1856073933 69480448 16610 4294967295 134512640 135167914 3221224448 3215312024 134693553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16963 16610 162 162 0 16801 0
[pid=1249] vsize: 67852
Current children cumulated CPU time (s) 1078.89
Current children cumulated vsize (Kb) 69980

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22500 0 0 0 108702 122 0 0 25 0 1 0 1856073933 69484544 16612 4294967295 134512640 135167914 3221224448 3215347104 134844713 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16964 16612 162 162 0 16802 0
[pid=1249] vsize: 67856
Current children cumulated CPU time (s) 1088.88
Current children cumulated vsize (Kb) 69984

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22501 0 0 0 109703 122 0 0 25 0 1 0 1856073933 69488640 16613 4294967295 134512640 135167914 3221224448 3215382208 134844703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16965 16613 162 162 0 16803 0
[pid=1249] vsize: 67860
Current children cumulated CPU time (s) 1098.89
Current children cumulated vsize (Kb) 69988

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22504 0 0 0 110703 122 0 0 25 0 1 0 1856073933 69496832 16616 4294967295 134512640 135167914 3221224448 3215417216 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16967 16616 162 162 0 16805 0
[pid=1249] vsize: 67868
Current children cumulated CPU time (s) 1108.89
Current children cumulated vsize (Kb) 69996

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22505 0 0 0 111703 122 0 0 25 0 1 0 1856073933 69500928 16617 4294967295 134512640 135167914 3221224448 3215452004 134849086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16968 16617 162 162 0 16806 0
[pid=1249] vsize: 67872
Current children cumulated CPU time (s) 1118.89
Current children cumulated vsize (Kb) 70000

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22508 0 0 0 112703 122 0 0 25 0 1 0 1856073933 69509120 16620 4294967295 134512640 135167914 3221224448 3215486368 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16970 16620 162 162 0 16808 0
[pid=1249] vsize: 67880
Current children cumulated CPU time (s) 1128.89
Current children cumulated vsize (Kb) 70008

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22509 0 0 0 113704 122 0 0 25 0 1 0 1856073933 69513216 16621 4294967295 134512640 135167914 3221224448 3215520908 134844675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16971 16621 162 162 0 16809 0
[pid=1249] vsize: 67884
Current children cumulated CPU time (s) 1138.9
Current children cumulated vsize (Kb) 70012

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22510 0 0 0 114704 122 0 0 25 0 1 0 1856073933 69517312 16622 4294967295 134512640 135167914 3221224448 3215555296 134624742 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16972 16622 162 162 0 16810 0
[pid=1249] vsize: 67888
Current children cumulated CPU time (s) 1148.9
Current children cumulated vsize (Kb) 70016

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22513 0 0 0 115704 122 0 0 25 0 1 0 1856073933 69525504 16625 4294967295 134512640 135167914 3221224448 3215589312 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16974 16625 162 162 0 16812 0
[pid=1249] vsize: 67896
Current children cumulated CPU time (s) 1158.9
Current children cumulated vsize (Kb) 70024

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22514 0 0 0 116704 122 0 0 25 0 1 0 1856073933 69529600 16626 4294967295 134512640 135167914 3221224448 3215623280 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16975 16626 162 162 0 16813 0
[pid=1249] vsize: 67900
Current children cumulated CPU time (s) 1168.9
Current children cumulated vsize (Kb) 70028

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22517 0 0 0 117704 122 0 0 25 0 1 0 1856073933 69537792 16629 4294967295 134512640 135167914 3221224448 3215657184 134694392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16977 16629 162 162 0 16815 0
[pid=1249] vsize: 67908
Current children cumulated CPU time (s) 1178.9
Current children cumulated vsize (Kb) 70036

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22518 0 0 0 118704 122 0 0 25 0 1 0 1856073933 69541888 16630 4294967295 134512640 135167914 3221224448 3215690796 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16978 16630 162 162 0 16816 0
[pid=1249] vsize: 67912
Current children cumulated CPU time (s) 1188.9
Current children cumulated vsize (Kb) 70040

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22520 0 0 0 119704 122 0 0 25 0 1 0 1856073933 69545984 16632 4294967295 134512640 135167914 3221224448 3215724424 134624784 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16979 16632 162 162 0 16817 0
[pid=1249] vsize: 67916
Current children cumulated CPU time (s) 1198.9
Current children cumulated vsize (Kb) 70044

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22521 0 0 0 120705 122 0 0 25 0 1 0 1856073933 69550080 16633 4294967295 134512640 135167914 3221224448 3215757808 134624577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16980 16633 162 162 0 16818 0
[pid=1249] vsize: 67920
Current children cumulated CPU time (s) 1208.91
Current children cumulated vsize (Kb) 70048



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1249
Raw data (/proc/1244/stat): 1244 (minisat+_script) S 1243 1244 5929 0 -1 0 314 2351 0 0 0 1 49 14 20 0 1 0 1856073853 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1244/statm): 532 234 485 147 0 385 0
[pid=1244] vsize: 2128
Raw data (/proc/1249/stat): 1249 (minisat+_bignum) R 1244 1244 5929 0 -1 0 22521 0 0 0 120705 122 0 0 25 0 1 0 1856073933 69550080 16633 4294967295 134512640 135167914 3221224448 3215757776 134849143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1249/statm): 16980 16633 162 162 0 16818 0
[pid=1249] vsize: 67920
Current children cumulated CPU time (s) 1208.91
Current children cumulated vsize (Kb) 70048

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

Child status: 0
Real time (s): 1210.13
CPU time (s): 1208.32
CPU user time (s): 1207.05
CPU system time (s): 1.26181
CPU usage (%): 99.8499
Max. virtual memory (cumulated for all children) (Kb): 70048

Verifier Data

ERROR: no interpretation found !