Some explanations

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

General information on the benchmark

Namemps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-van.opb
MD5SUMd28d6112d880a2aec142bea33a4150fb
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 29268441542
Optimality of the best value was proved NO
Number of terms in the objective function 192
Biggest coefficient in the objective function 2427002644
Number of bits for the biggest coefficient in the objective function 32
Sum of the numbers in the objective function 319999999936
Number of bits of the sum of numbers in the objective function 39
Biggest number in a constraint 226795425792
Number of bits of the biggest number in a constraint 38
Biggest sum of numbers in a constraint 973128929893
Number of bits of the biggest sum of numbers40
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1284.91
Number of variables135360
Total number of constraints39811
Number of constraints which are clauses128
Number of constraints which are cardinality constraints (but not clauses)195
Number of constraints which are nor clauses,nor cardinality constraints39488
Minimum length of a constraint1
Maximum length of a constraint496

Trace number 5959

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        743232 kB
Buffers:         12772 kB
Cached:         250484 kB
SwapCached:        516 kB
Active:         190840 kB
Inactive:        74792 kB
HighTotal:      131008 kB
HighFree:         3780 kB
LowTotal:       903652 kB
LowFree:        739452 kB
SwapTotal:     2097892 kB
SwapFree:      2096676 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5664 kB
Slab:            20064 kB
Committed_AS:    64316 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 02:45:26 (client local time) WITH STATUS 0 IN 1206.6 SECONDS
stats: 3122 7 1206.6 0

Solver Data



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/6293/stat): 6293 (minisat+_script) R 6292 6293 19316 0 -1 0 19 0 0 0 0 0 0 0 20 0 1 0 1854943918 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/6293/statm): 174 3 169 147 0 27 0
[pid=6293] 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=6294
New process pid=6295
New process pid=6296
execve syscall for /bin/sed executable
One traced child (pid=6295) 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=6296) exited with status: 0
One traced child (pid=6294) exited with status: 0
New process pid=6297
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-van.opb

[startup+10.0045 s]
Raw data (loadavg): 1.02 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 1259 0 0 0 980 8 0 0 25 0 1 0 1854943923 5795840 1193 4294967295 134512640 135094434 3221224432 3221223328 134587994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 1415 1193 145 145 0 1270 0
[pid=6297] vsize: 5660
Current children cumulated CPU time (s) 9.89
Current children cumulated vsize (Kb) 7784

[startup+20.0061 s]
Raw data (loadavg): 1.02 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 2223 0 0 0 1973 12 0 0 25 0 1 0 1854943923 10313728 2059 4294967295 134512640 135094434 3221224432 3221223316 134796009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 2518 2059 145 145 0 2373 0
[pid=6297] vsize: 10072
Current children cumulated CPU time (s) 19.86
Current children cumulated vsize (Kb) 12196

[startup+30.0067 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 2821 0 0 0 2964 17 0 0 25 0 1 0 1854943923 11841536 2657 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 2891 2657 145 145 0 2746 0
[pid=6297] vsize: 11564
Current children cumulated CPU time (s) 29.82
Current children cumulated vsize (Kb) 13688

[startup+40.0093 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 3694 0 0 0 3953 23 0 0 25 0 1 0 1854943923 18620416 3530 4294967295 134512640 135094434 3221224432 3221223300 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 4546 3530 145 145 0 4401 0
[pid=6297] vsize: 18184
Current children cumulated CPU time (s) 39.77
Current children cumulated vsize (Kb) 20308

[startup+50.0099 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 4373 0 0 0 4948 26 0 0 25 0 1 0 1854943923 20156416 4044 4294967295 134512640 135094434 3221224432 3221223328 134587994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 4921 4044 145 145 0 4776 0
[pid=6297] vsize: 19684
Current children cumulated CPU time (s) 49.75
Current children cumulated vsize (Kb) 21808

[startup+60.0105 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 4606 0 0 0 5945 28 0 0 25 0 1 0 1854943923 20766720 4277 4294967295 134512640 135094434 3221224432 3221223328 134587880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 5070 4277 145 145 0 4925 0
[pid=6297] vsize: 20280
Current children cumulated CPU time (s) 59.74
Current children cumulated vsize (Kb) 22404

[startup+70.0111 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 4883 0 0 0 6940 30 0 0 25 0 1 0 1854943923 21467136 4554 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 5241 4554 145 145 0 5096 0
[pid=6297] vsize: 20964
Current children cumulated CPU time (s) 69.71
Current children cumulated vsize (Kb) 23088

[startup+80.0127 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 5131 0 0 0 7937 32 0 0 25 0 1 0 1854943923 22097920 4802 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 5395 4802 145 145 0 5250 0
[pid=6297] vsize: 21580
Current children cumulated CPU time (s) 79.7
Current children cumulated vsize (Kb) 23704

[startup+90.0133 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 5538 0 0 0 8932 35 0 0 25 0 1 0 1854943923 23097344 5209 4294967295 134512640 135094434 3221224432 3221223344 134587903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 5639 5209 145 145 0 5494 0
[pid=6297] vsize: 22556
Current children cumulated CPU time (s) 89.68
Current children cumulated vsize (Kb) 24680

[startup+100.014 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 5887 0 0 0 9927 37 0 0 25 0 1 0 1854943923 23957504 5558 4294967295 134512640 135094434 3221224432 3221223316 134796010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 5849 5558 145 145 0 5704 0
[pid=6297] vsize: 23396
Current children cumulated CPU time (s) 99.65
Current children cumulated vsize (Kb) 25520

[startup+110.016 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 6259 0 0 0 10923 39 0 0 25 0 1 0 1854943923 34324480 5930 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 8380 5930 145 145 0 8235 0
[pid=6297] vsize: 33520
Current children cumulated CPU time (s) 109.63
Current children cumulated vsize (Kb) 35644

[startup+120.017 s]
Raw data (loadavg): 1.00 1.00 0.97 1/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) T 6293 6293 19316 0 -1 0 6388 0 0 0 11920 41 0 0 25 0 1 0 1854943923 34574336 6059 4294967295 134512640 135094434 3221224432 3221223352 134801661 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6297/statm): 8441 6059 145 145 0 8296 0
[pid=6297] vsize: 33764
Current children cumulated CPU time (s) 119.62
Current children cumulated vsize (Kb) 35888

[startup+130.018 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 6600 0 0 0 12914 44 0 0 25 0 1 0 1854943923 35442688 6271 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 8653 6271 145 145 0 8508 0
[pid=6297] vsize: 34612
Current children cumulated CPU time (s) 129.59
Current children cumulated vsize (Kb) 36736

[startup+140.018 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 6750 0 0 0 13908 47 0 0 25 0 1 0 1854943923 36057088 6421 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 8803 6421 145 145 0 8658 0
[pid=6297] vsize: 35212
Current children cumulated CPU time (s) 139.56
Current children cumulated vsize (Kb) 37336

[startup+150.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 6895 0 0 0 14904 50 0 0 25 0 1 0 1854943923 36651008 6566 4294967295 134512640 135094434 3221224432 3221223324 134796030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 8948 6566 145 145 0 8803 0
[pid=6297] vsize: 35792
Current children cumulated CPU time (s) 149.55
Current children cumulated vsize (Kb) 37916

[startup+160.021 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 7092 0 0 0 15898 53 0 0 25 0 1 0 1854943923 37457920 6763 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 9145 6763 145 145 0 9000 0
[pid=6297] vsize: 36580
Current children cumulated CPU time (s) 159.52
Current children cumulated vsize (Kb) 38704

[startup+170.021 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 7268 0 0 0 16892 56 0 0 25 0 1 0 1854943923 38178816 6939 4294967295 134512640 135094434 3221224432 3221223344 134587868 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 9321 6939 145 145 0 9176 0
[pid=6297] vsize: 37284
Current children cumulated CPU time (s) 169.49
Current children cumulated vsize (Kb) 39408

[startup+180.023 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 7412 0 0 0 17887 58 0 0 25 0 1 0 1854943923 38768640 7083 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 9465 7083 145 145 0 9320 0
[pid=6297] vsize: 37860
Current children cumulated CPU time (s) 179.46
Current children cumulated vsize (Kb) 39984

[startup+190.022 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 7576 0 0 0 18881 61 0 0 25 0 1 0 1854943923 39440384 7247 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 9629 7247 145 145 0 9484 0
[pid=6297] vsize: 38516
Current children cumulated CPU time (s) 189.43
Current children cumulated vsize (Kb) 40640

[startup+200.023 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 7778 0 0 0 19875 64 0 0 25 0 1 0 1854943923 40267776 7449 4294967295 134512640 135094434 3221224432 3221223324 134795992 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 9831 7449 145 145 0 9686 0
[pid=6297] vsize: 39324
Current children cumulated CPU time (s) 199.4
Current children cumulated vsize (Kb) 41448

[startup+210.024 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 7943 0 0 0 20870 66 0 0 25 0 1 0 1854943923 40943616 7614 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 9996 7614 145 145 0 9851 0
[pid=6297] vsize: 39984
Current children cumulated CPU time (s) 209.37
Current children cumulated vsize (Kb) 42108

[startup+220.024 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 8088 0 0 0 21866 69 0 0 25 0 1 0 1854943923 41537536 7759 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 10141 7759 145 145 0 9996 0
[pid=6297] vsize: 40564
Current children cumulated CPU time (s) 219.36
Current children cumulated vsize (Kb) 42688

[startup+230.025 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 8271 0 0 0 22859 72 0 0 25 0 1 0 1854943923 42287104 7942 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 10324 7942 145 145 0 10179 0
[pid=6297] vsize: 41296
Current children cumulated CPU time (s) 229.32
Current children cumulated vsize (Kb) 43420

[startup+240.025 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 8456 0 0 0 23851 76 0 0 25 0 1 0 1854943923 43044864 8127 4294967295 134512640 135094434 3221224432 3221223316 134796009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 10509 8127 145 145 0 10364 0
[pid=6297] vsize: 42036
Current children cumulated CPU time (s) 239.28
Current children cumulated vsize (Kb) 44160

[startup+250.026 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 8614 0 0 0 24846 78 0 0 25 0 1 0 1854943923 43692032 8285 4294967295 134512640 135094434 3221224432 3221223316 134795999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 10667 8285 145 145 0 10522 0
[pid=6297] vsize: 42668
Current children cumulated CPU time (s) 249.25
Current children cumulated vsize (Kb) 44792

[startup+260.027 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 8765 0 0 0 25840 81 0 0 25 0 1 0 1854943923 44306432 8436 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 10817 8436 145 145 0 10672 0
[pid=6297] vsize: 43268
Current children cumulated CPU time (s) 259.22
Current children cumulated vsize (Kb) 45392

[startup+270.028 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 8968 0 0 0 26835 83 0 0 25 0 1 0 1854943923 45137920 8639 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 11020 8639 145 145 0 10875 0
[pid=6297] vsize: 44080
Current children cumulated CPU time (s) 269.19
Current children cumulated vsize (Kb) 46204

[startup+280.029 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 9133 0 0 0 27831 85 0 0 25 0 1 0 1854943923 45813760 8804 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 11185 8804 145 145 0 11040 0
[pid=6297] vsize: 44740
Current children cumulated CPU time (s) 279.17
Current children cumulated vsize (Kb) 46864

[startup+290.029 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 9277 0 0 0 28825 87 0 0 25 0 1 0 1854943923 46403584 8948 4294967295 134512640 135094434 3221224432 3221223328 134587885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 11329 8948 145 145 0 11184 0
[pid=6297] vsize: 45316
Current children cumulated CPU time (s) 289.13
Current children cumulated vsize (Kb) 47440

[startup+300.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 9455 0 0 0 29819 90 0 0 25 0 1 0 1854943923 47132672 9126 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 11507 9126 145 145 0 11362 0
[pid=6297] vsize: 46028
Current children cumulated CPU time (s) 299.1
Current children cumulated vsize (Kb) 48152

[startup+310.031 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 9647 0 0 0 30812 93 0 0 25 0 1 0 1854943923 47919104 9318 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 11699 9318 145 145 0 11554 0
[pid=6297] vsize: 46796
Current children cumulated CPU time (s) 309.06
Current children cumulated vsize (Kb) 48920

[startup+320.032 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 9807 0 0 0 31808 95 0 0 25 0 1 0 1854943923 48574464 9478 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 11859 9478 145 145 0 11714 0
[pid=6297] vsize: 47436
Current children cumulated CPU time (s) 319.04
Current children cumulated vsize (Kb) 49560

[startup+330.033 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 9955 0 0 0 32804 97 0 0 25 0 1 0 1854943923 49180672 9626 4294967295 134512640 135094434 3221224432 3221223316 134796010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 12007 9626 145 145 0 11862 0
[pid=6297] vsize: 48028
Current children cumulated CPU time (s) 329.02
Current children cumulated vsize (Kb) 50152

[startup+340.033 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 10162 0 0 0 33798 100 0 0 25 0 1 0 1854943923 50028544 9833 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 12214 9833 145 145 0 12069 0
[pid=6297] vsize: 48856
Current children cumulated CPU time (s) 338.99
Current children cumulated vsize (Kb) 50980

[startup+350.034 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 10328 0 0 0 34795 101 0 0 25 0 1 0 1854943923 50708480 9999 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 12380 9999 145 145 0 12235 0
[pid=6297] vsize: 49520
Current children cumulated CPU time (s) 348.97
Current children cumulated vsize (Kb) 51644

[startup+360.035 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 10471 0 0 0 35787 105 0 0 25 0 1 0 1854943923 51294208 10142 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 12523 10142 145 145 0 12378 0
[pid=6297] vsize: 50092
Current children cumulated CPU time (s) 358.93
Current children cumulated vsize (Kb) 52216

[startup+370.036 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 10647 0 0 0 36781 109 0 0 25 0 1 0 1854943923 52015104 10318 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 12699 10318 145 145 0 12554 0
[pid=6297] vsize: 50796
Current children cumulated CPU time (s) 368.91
Current children cumulated vsize (Kb) 52920

[startup+380.037 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 10842 0 0 0 37775 111 0 0 25 0 1 0 1854943923 52813824 10513 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 12894 10513 145 145 0 12749 0
[pid=6297] vsize: 51576
Current children cumulated CPU time (s) 378.87
Current children cumulated vsize (Kb) 53700

[startup+390.037 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 11007 0 0 0 38771 113 0 0 25 0 1 0 1854943923 53489664 10678 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 13059 10678 145 145 0 12914 0
[pid=6297] vsize: 52236
Current children cumulated CPU time (s) 388.85
Current children cumulated vsize (Kb) 54360

[startup+400.038 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 11155 0 0 0 39766 116 0 0 25 0 1 0 1854943923 54095872 10826 4294967295 134512640 135094434 3221224432 3221223316 134796010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 13207 10826 145 145 0 13062 0
[pid=6297] vsize: 52828
Current children cumulated CPU time (s) 398.83
Current children cumulated vsize (Kb) 54952

[startup+410.039 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 11360 0 0 0 40759 119 0 0 25 0 1 0 1854943923 54935552 11031 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 13412 11031 145 145 0 13267 0
[pid=6297] vsize: 53648
Current children cumulated CPU time (s) 408.79
Current children cumulated vsize (Kb) 55772

[startup+420.04 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 11535 0 0 0 41754 121 0 0 25 0 1 0 1854943923 55652352 11206 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 13587 11206 145 145 0 13442 0
[pid=6297] vsize: 54348
Current children cumulated CPU time (s) 418.76
Current children cumulated vsize (Kb) 56472

[startup+430.041 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 11688 0 0 0 42750 123 0 0 25 0 1 0 1854943923 56279040 11359 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 13740 11359 145 145 0 13595 0
[pid=6297] vsize: 54960
Current children cumulated CPU time (s) 428.74
Current children cumulated vsize (Kb) 57084

[startup+440.041 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 11865 0 0 0 43744 126 0 0 25 0 1 0 1854943923 57004032 11536 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 13917 11536 145 145 0 13772 0
[pid=6297] vsize: 55668
Current children cumulated CPU time (s) 438.71
Current children cumulated vsize (Kb) 57792

[startup+450.042 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 12061 0 0 0 44737 129 0 0 25 0 1 0 1854943923 57806848 11732 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 14113 11732 145 145 0 13968 0
[pid=6297] vsize: 56452
Current children cumulated CPU time (s) 448.67
Current children cumulated vsize (Kb) 58576

[startup+460.043 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 12218 0 0 0 45733 131 0 0 25 0 1 0 1854943923 58449920 11889 4294967295 134512640 135094434 3221224432 3221223316 134796002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 14270 11889 145 145 0 14125 0
[pid=6297] vsize: 57080
Current children cumulated CPU time (s) 458.65
Current children cumulated vsize (Kb) 59204

[startup+470.044 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 12368 0 0 0 46726 134 0 0 25 0 1 0 1854943923 59064320 12039 4294967295 134512640 135094434 3221224432 3221223328 134587885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 14420 12039 145 145 0 14275 0
[pid=6297] vsize: 57680
Current children cumulated CPU time (s) 468.61
Current children cumulated vsize (Kb) 59804

[startup+480.046 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 12570 0 0 0 47720 137 0 0 25 0 1 0 1854943923 59891712 12241 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 14622 12241 145 145 0 14477 0
[pid=6297] vsize: 58488
Current children cumulated CPU time (s) 478.58
Current children cumulated vsize (Kb) 60612

[startup+490.045 s]
Raw data (loadavg): 1.00 1.00 0.97 1/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) T 6293 6293 19316 0 -1 0 12741 0 0 0 48714 139 0 0 25 0 1 0 1854943923 60592128 12412 4294967295 134512640 135094434 3221224432 3221223368 134801661 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6297/statm): 14793 12412 145 145 0 14648 0
[pid=6297] vsize: 59172
Current children cumulated CPU time (s) 488.54
Current children cumulated vsize (Kb) 61296

[startup+500.047 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 12895 0 0 0 49710 142 0 0 25 0 1 0 1854943923 61222912 12566 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 14947 12566 145 145 0 14802 0
[pid=6297] vsize: 59788
Current children cumulated CPU time (s) 498.53
Current children cumulated vsize (Kb) 61912

[startup+510.048 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 13065 0 0 0 50705 145 0 0 25 0 1 0 1854943923 61919232 12736 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 15117 12736 145 145 0 14972 0
[pid=6297] vsize: 60468
Current children cumulated CPU time (s) 508.51
Current children cumulated vsize (Kb) 62592

[startup+520.048 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 13262 0 0 0 51700 149 0 0 25 0 1 0 1854943923 62726144 12933 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 15314 12933 145 145 0 15169 0
[pid=6297] vsize: 61256
Current children cumulated CPU time (s) 518.5
Current children cumulated vsize (Kb) 63380

[startup+530.049 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 13419 0 0 0 52696 150 0 0 25 0 1 0 1854943923 63369216 13090 4294967295 134512640 135094434 3221224432 3221223344 134587875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 15471 13090 145 145 0 15326 0
[pid=6297] vsize: 61884
Current children cumulated CPU time (s) 528.47
Current children cumulated vsize (Kb) 64008

[startup+540.049 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 13574 0 0 0 53691 153 0 0 25 0 1 0 1854943923 64004096 13245 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 15626 13245 145 145 0 15481 0
[pid=6297] vsize: 62504
Current children cumulated CPU time (s) 538.45
Current children cumulated vsize (Kb) 64628

[startup+550.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 13773 0 0 0 54684 156 0 0 25 0 1 0 1854943923 64819200 13444 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 15825 13444 145 145 0 15680 0
[pid=6297] vsize: 63300
Current children cumulated CPU time (s) 548.41
Current children cumulated vsize (Kb) 65424

[startup+560.051 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 13947 0 0 0 55678 158 0 0 25 0 1 0 1854943923 65531904 13618 4294967295 134512640 135094434 3221224432 3221223316 134796010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 15999 13618 145 145 0 15854 0
[pid=6297] vsize: 63996
Current children cumulated CPU time (s) 558.37
Current children cumulated vsize (Kb) 66120

[startup+570.052 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 14092 0 0 0 56674 160 0 0 25 0 1 0 1854943923 66125824 13763 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 16144 13763 145 145 0 15999 0
[pid=6297] vsize: 64576
Current children cumulated CPU time (s) 568.35
Current children cumulated vsize (Kb) 66700

[startup+580.053 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 14258 0 0 0 57669 162 0 0 25 0 1 0 1854943923 66801664 13929 4294967295 134512640 135094434 3221224432 3221223344 134587903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 16309 13929 145 145 0 16164 0
[pid=6297] vsize: 65236
Current children cumulated CPU time (s) 578.32
Current children cumulated vsize (Kb) 67360

[startup+590.053 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 14460 0 0 0 58663 165 0 0 25 0 1 0 1854943923 67629056 14131 4294967295 134512640 135094434 3221224432 3221223316 134796009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 16511 14131 145 145 0 16366 0
[pid=6297] vsize: 66044
Current children cumulated CPU time (s) 588.29
Current children cumulated vsize (Kb) 68168

[startup+600.055 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 14612 0 0 0 59656 169 0 0 25 0 1 0 1854943923 68251648 14283 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 16663 14283 145 145 0 16518 0
[pid=6297] vsize: 66652
Current children cumulated CPU time (s) 598.26
Current children cumulated vsize (Kb) 68776

[startup+610.056 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 14774 0 0 0 60651 171 0 0 25 0 1 0 1854943923 68915200 14445 4294967295 134512640 135094434 3221224432 3221223316 134796009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 16825 14445 145 145 0 16680 0
[pid=6297] vsize: 67300
Current children cumulated CPU time (s) 608.23
Current children cumulated vsize (Kb) 69424

[startup+620.057 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) T 6293 6293 19316 0 -1 0 14969 0 0 0 61647 174 0 0 25 0 1 0 1854943923 69713920 14640 4294967295 134512640 135094434 3221224432 3221223368 134801661 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6297/statm): 17020 14640 145 145 0 16875 0
[pid=6297] vsize: 68080
Current children cumulated CPU time (s) 618.22
Current children cumulated vsize (Kb) 70204

[startup+630.058 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 15143 0 0 0 62641 176 0 0 25 0 1 0 1854943923 70426624 14814 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 17194 14814 145 145 0 17049 0
[pid=6297] vsize: 68776
Current children cumulated CPU time (s) 628.18
Current children cumulated vsize (Kb) 70900

[startup+640.058 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 15300 0 0 0 63635 179 0 0 25 0 1 0 1854943923 71069696 14971 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 17351 14971 145 145 0 17206 0
[pid=6297] vsize: 69404
Current children cumulated CPU time (s) 638.15
Current children cumulated vsize (Kb) 71528

[startup+650.059 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 15471 0 0 0 64630 182 0 0 25 0 1 0 1854943923 71770112 15142 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 17522 15142 145 145 0 17377 0
[pid=6297] vsize: 70088
Current children cumulated CPU time (s) 648.13
Current children cumulated vsize (Kb) 72212

[startup+660.06 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 15667 0 0 0 65621 187 0 0 25 0 1 0 1854943923 72572928 15338 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 17718 15338 145 145 0 17573 0
[pid=6297] vsize: 70872
Current children cumulated CPU time (s) 658.09
Current children cumulated vsize (Kb) 72996

[startup+670.061 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 15833 0 0 0 66617 189 0 0 25 0 1 0 1854943923 73252864 15504 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 17884 15504 145 145 0 17739 0
[pid=6297] vsize: 71536
Current children cumulated CPU time (s) 668.07
Current children cumulated vsize (Kb) 73660

[startup+680.062 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 15992 0 0 0 67611 192 0 0 25 0 1 0 1854943923 73904128 15663 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 18043 15663 145 145 0 17898 0
[pid=6297] vsize: 72172
Current children cumulated CPU time (s) 678.04
Current children cumulated vsize (Kb) 74296

[startup+690.062 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 16190 0 0 0 68606 195 0 0 25 0 1 0 1854943923 74715136 15861 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 18241 15861 145 145 0 18096 0
[pid=6297] vsize: 72964
Current children cumulated CPU time (s) 688.02
Current children cumulated vsize (Kb) 75088

[startup+700.063 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 16362 0 0 0 69600 198 0 0 25 0 1 0 1854943923 75419648 16033 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 18413 16033 145 145 0 18268 0
[pid=6297] vsize: 73652
Current children cumulated CPU time (s) 697.99
Current children cumulated vsize (Kb) 75776

[startup+710.064 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 16518 0 0 0 70596 199 0 0 25 0 1 0 1854943923 76058624 16189 4294967295 134512640 135094434 3221224432 3221223344 134587903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 18569 16189 145 145 0 18424 0
[pid=6297] vsize: 74276
Current children cumulated CPU time (s) 707.96
Current children cumulated vsize (Kb) 76400

[startup+720.065 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 16690 0 0 0 71589 202 0 0 25 0 1 0 1854943923 76763136 16361 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 18741 16361 145 145 0 18596 0
[pid=6297] vsize: 74964
Current children cumulated CPU time (s) 717.92
Current children cumulated vsize (Kb) 77088

[startup+730.066 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 16902 0 0 0 72582 206 0 0 25 0 1 0 1854943923 77631488 16573 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 18953 16573 145 145 0 18808 0
[pid=6297] vsize: 75812
Current children cumulated CPU time (s) 727.89
Current children cumulated vsize (Kb) 77936

[startup+740.066 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 17053 0 0 0 73578 209 0 0 25 0 1 0 1854943923 78249984 16724 4294967295 134512640 135094434 3221224432 3221223344 134587873 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 19104 16724 145 145 0 18959 0
[pid=6297] vsize: 76416
Current children cumulated CPU time (s) 737.88
Current children cumulated vsize (Kb) 78540

[startup+750.067 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 17193 0 0 0 74572 211 0 0 25 0 1 0 1854943923 78823424 16864 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 19244 16864 145 145 0 19099 0
[pid=6297] vsize: 76976
Current children cumulated CPU time (s) 747.84
Current children cumulated vsize (Kb) 79100

[startup+760.068 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 17394 0 0 0 75565 215 0 0 25 0 1 0 1854943923 79646720 17065 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 19445 17065 145 145 0 19300 0
[pid=6297] vsize: 77780
Current children cumulated CPU time (s) 757.81
Current children cumulated vsize (Kb) 79904

[startup+770.068 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 17574 0 0 0 76560 217 0 0 25 0 1 0 1854943923 80384000 17245 4294967295 134512640 135094434 3221224432 3221223344 134587903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 19625 17245 145 145 0 19480 0
[pid=6297] vsize: 78500
Current children cumulated CPU time (s) 767.78
Current children cumulated vsize (Kb) 80624

[startup+780.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 17722 0 0 0 77555 219 0 0 25 0 1 0 1854943923 80990208 17393 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 19773 17393 145 145 0 19628 0
[pid=6297] vsize: 79092
Current children cumulated CPU time (s) 777.75
Current children cumulated vsize (Kb) 81216

[startup+790.069 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) T 6293 6293 19316 0 -1 0 17875 0 0 0 78550 221 0 0 25 0 1 0 1854943923 81616896 17546 4294967295 134512640 135094434 3221224432 3221223352 134801661 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6297/statm): 19926 17546 145 145 0 19781 0
[pid=6297] vsize: 79704
Current children cumulated CPU time (s) 787.72
Current children cumulated vsize (Kb) 81828

[startup+800.07 s]
Raw data (loadavg): 1.00 1.00 0.97 1/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) T 6293 6293 19316 0 -1 0 18080 0 0 0 79544 225 0 0 25 0 1 0 1854943923 82456576 17751 4294967295 134512640 135094434 3221224432 3221223368 134801661 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6297/statm): 20131 17751 145 145 0 19986 0
[pid=6297] vsize: 80524
Current children cumulated CPU time (s) 797.7
Current children cumulated vsize (Kb) 82648

[startup+810.071 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 18240 0 0 0 80540 227 0 0 25 0 1 0 1854943923 83111936 17911 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 20291 17911 145 145 0 20146 0
[pid=6297] vsize: 81164
Current children cumulated CPU time (s) 807.68
Current children cumulated vsize (Kb) 83288

[startup+820.07 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 18388 0 0 0 81535 229 0 0 25 0 1 0 1854943923 83718144 18059 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 20439 18059 145 145 0 20294 0
[pid=6297] vsize: 81756
Current children cumulated CPU time (s) 817.65
Current children cumulated vsize (Kb) 83880

[startup+830.071 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 18564 0 0 0 82529 232 0 0 25 0 1 0 1854943923 84439040 18235 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 20615 18235 145 145 0 20470 0
[pid=6297] vsize: 82460
Current children cumulated CPU time (s) 827.62
Current children cumulated vsize (Kb) 84584

[startup+840.071 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 18745 0 0 0 83523 234 0 0 25 0 1 0 1854943923 85180416 18416 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 20796 18416 145 145 0 20651 0
[pid=6297] vsize: 83184
Current children cumulated CPU time (s) 837.58
Current children cumulated vsize (Kb) 85308

[startup+850.072 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 18905 0 0 0 84518 236 0 0 25 0 1 0 1854943923 85835776 18576 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 20956 18576 145 145 0 20811 0
[pid=6297] vsize: 83824
Current children cumulated CPU time (s) 847.55
Current children cumulated vsize (Kb) 85948

[startup+860.073 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 19055 0 0 0 85513 238 0 0 25 0 1 0 1854943923 86450176 18726 4294967295 134512640 135094434 3221224432 3221223344 134587903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 21106 18726 145 145 0 20961 0
[pid=6297] vsize: 84424
Current children cumulated CPU time (s) 857.52
Current children cumulated vsize (Kb) 86548

[startup+870.073 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 19260 0 0 0 86507 241 0 0 25 0 1 0 1854943923 87293952 18931 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 21312 18931 145 145 0 21167 0
[pid=6297] vsize: 85248
Current children cumulated CPU time (s) 867.49
Current children cumulated vsize (Kb) 87372

[startup+880.074 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 19429 0 0 0 87502 244 0 0 25 0 1 0 1854943923 87982080 19100 4294967295 134512640 135094434 3221224432 3221223344 134587839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 21480 19100 145 145 0 21335 0
[pid=6297] vsize: 85920
Current children cumulated CPU time (s) 877.47
Current children cumulated vsize (Kb) 88044

[startup+890.074 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 19575 0 0 0 88498 246 0 0 25 0 1 0 1854943923 88576000 19246 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 21625 19246 145 145 0 21480 0
[pid=6297] vsize: 86500
Current children cumulated CPU time (s) 887.45
Current children cumulated vsize (Kb) 88624

[startup+900.076 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 19739 0 0 0 89493 248 0 0 25 0 1 0 1854943923 89251840 19410 4294967295 134512640 135094434 3221224432 3221223316 134796010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 21790 19410 145 145 0 21645 0
[pid=6297] vsize: 87160
Current children cumulated CPU time (s) 897.42
Current children cumulated vsize (Kb) 89284

[startup+910.077 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 19936 0 0 0 90486 252 0 0 25 0 1 0 1854943923 90054656 19607 4294967295 134512640 135094434 3221224432 3221223344 134587868 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 21986 19607 145 145 0 21841 0
[pid=6297] vsize: 87944
Current children cumulated CPU time (s) 907.39
Current children cumulated vsize (Kb) 90068

[startup+920.077 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 20093 0 0 0 91481 254 0 0 25 0 1 0 1854943923 90697728 19764 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 22143 19764 145 145 0 21998 0
[pid=6297] vsize: 88572
Current children cumulated CPU time (s) 917.36
Current children cumulated vsize (Kb) 90696

[startup+930.078 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 20243 0 0 0 92476 256 0 0 25 0 1 0 1854943923 91312128 19914 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 22293 19914 145 145 0 22148 0
[pid=6297] vsize: 89172
Current children cumulated CPU time (s) 927.33
Current children cumulated vsize (Kb) 91296

[startup+940.077 s]
Raw data (loadavg): 1.00 1.00 0.97 1/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) T 6293 6293 19316 0 -1 0 20434 0 0 0 93471 258 0 0 25 0 1 0 1854943923 92094464 20105 4294967295 134512640 135094434 3221224432 3221223368 134801661 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/6297/statm): 22484 20105 145 145 0 22339 0
[pid=6297] vsize: 89936
Current children cumulated CPU time (s) 937.3
Current children cumulated vsize (Kb) 92060

[startup+950.079 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 20611 0 0 0 94466 261 0 0 25 0 1 0 1854943923 92819456 20282 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 22661 20282 145 145 0 22516 0
[pid=6297] vsize: 90644
Current children cumulated CPU time (s) 947.28
Current children cumulated vsize (Kb) 92768

[startup+960.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 20759 0 0 0 95461 263 0 0 25 0 1 0 1854943923 93425664 20430 4294967295 134512640 135094434 3221224432 3221223344 134587868 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 22809 20430 145 145 0 22664 0
[pid=6297] vsize: 91236
Current children cumulated CPU time (s) 957.25
Current children cumulated vsize (Kb) 93360

[startup+970.079 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 20919 0 0 0 96455 266 0 0 25 0 1 0 1854943923 94081024 20590 4294967295 134512640 135094434 3221224432 3221223316 134796004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 22969 20590 145 145 0 22824 0
[pid=6297] vsize: 91876
Current children cumulated CPU time (s) 967.22
Current children cumulated vsize (Kb) 94000

[startup+980.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 21121 0 0 0 97448 269 0 0 25 0 1 0 1854943923 94908416 20792 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 23171 20792 145 145 0 23026 0
[pid=6297] vsize: 92684
Current children cumulated CPU time (s) 977.18
Current children cumulated vsize (Kb) 94808

[startup+990.079 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 21278 0 0 0 98444 272 0 0 25 0 1 0 1854943923 95551488 20949 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 23328 20949 145 145 0 23183 0
[pid=6297] vsize: 93312
Current children cumulated CPU time (s) 987.17
Current children cumulated vsize (Kb) 95436

[startup+1000.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 21423 0 0 0 99439 273 0 0 25 0 1 0 1854943923 96145408 21094 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 23473 21094 145 145 0 23328 0
[pid=6297] vsize: 93892
Current children cumulated CPU time (s) 997.13
Current children cumulated vsize (Kb) 96016

[startup+1010.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 21608 0 0 0 100433 276 0 0 25 0 1 0 1854943923 96903168 21279 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 23658 21279 145 145 0 23513 0
[pid=6297] vsize: 94632
Current children cumulated CPU time (s) 1007.1
Current children cumulated vsize (Kb) 96756

[startup+1020.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 21789 0 0 0 101426 279 0 0 25 0 1 0 1854943923 97644544 21460 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 23839 21460 145 145 0 23694 0
[pid=6297] vsize: 95356
Current children cumulated CPU time (s) 1017.06
Current children cumulated vsize (Kb) 97480

[startup+1030.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 21946 0 0 0 102421 282 0 0 25 0 1 0 1854943923 98287616 21617 4294967295 134512640 135094434 3221224432 3221223316 134796010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 23996 21617 145 145 0 23851 0
[pid=6297] vsize: 95984
Current children cumulated CPU time (s) 1027.04
Current children cumulated vsize (Kb) 98108

[startup+1040.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 22094 0 0 0 103416 284 0 0 25 0 1 0 1854943923 98893824 21765 4294967295 134512640 135094434 3221224432 3221223316 134796016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 24144 21765 145 145 0 23999 0
[pid=6297] vsize: 96576
Current children cumulated CPU time (s) 1037.01
Current children cumulated vsize (Kb) 98700

[startup+1050.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 22303 0 0 0 104409 288 0 0 25 0 1 0 1854943923 99749888 21974 4294967295 134512640 135094434 3221224432 3221223316 134796010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 24353 21974 145 145 0 24208 0
[pid=6297] vsize: 97412
Current children cumulated CPU time (s) 1046.98
Current children cumulated vsize (Kb) 99536

[startup+1060.08 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 22452 0 0 0 105404 290 0 0 25 0 1 0 1854943923 100364288 22123 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 24503 22123 145 145 0 24358 0
[pid=6297] vsize: 98012
Current children cumulated CPU time (s) 1056.95
Current children cumulated vsize (Kb) 100136

[startup+1070.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 22597 0 0 0 106399 293 0 0 25 0 1 0 1854943923 100954112 22268 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 24647 22268 145 145 0 24502 0
[pid=6297] vsize: 98588
Current children cumulated CPU time (s) 1066.93
Current children cumulated vsize (Kb) 100712

[startup+1080.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 22761 0 0 0 107393 296 0 0 25 0 1 0 1854943923 101625856 22432 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 24811 22432 145 145 0 24666 0
[pid=6297] vsize: 99244
Current children cumulated CPU time (s) 1076.9
Current children cumulated vsize (Kb) 101368

[startup+1090.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 22942 0 0 0 108386 300 0 0 25 0 1 0 1854943923 102367232 22613 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 24992 22613 145 145 0 24847 0
[pid=6297] vsize: 99968
Current children cumulated CPU time (s) 1086.87
Current children cumulated vsize (Kb) 102092

[startup+1100.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 23093 0 0 0 109382 301 0 0 25 0 1 0 1854943923 102985728 22764 4294967295 134512640 135094434 3221224432 3221223344 134587903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 25143 22764 145 145 0 24998 0
[pid=6297] vsize: 100572
Current children cumulated CPU time (s) 1096.84
Current children cumulated vsize (Kb) 102696

[startup+1110.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 23236 0 0 0 110378 304 0 0 25 0 1 0 1854943923 103571456 22907 4294967295 134512640 135094434 3221224432 3221223316 134796009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 25286 22907 145 145 0 25141 0
[pid=6297] vsize: 101144
Current children cumulated CPU time (s) 1106.83
Current children cumulated vsize (Kb) 103268

[startup+1120.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 23412 0 0 0 111372 308 0 0 25 0 1 0 1854943923 104292352 23083 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 25462 23083 145 145 0 25317 0
[pid=6297] vsize: 101848
Current children cumulated CPU time (s) 1116.81
Current children cumulated vsize (Kb) 103972

[startup+1130.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 23578 0 0 0 112366 311 0 0 25 0 1 0 1854943923 104972288 23249 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 25628 23249 145 145 0 25483 0
[pid=6297] vsize: 102512
Current children cumulated CPU time (s) 1126.78
Current children cumulated vsize (Kb) 104636

[startup+1140.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 23730 0 0 0 113361 313 0 0 25 0 1 0 1854943923 105594880 23401 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 25780 23401 145 145 0 25635 0
[pid=6297] vsize: 103120
Current children cumulated CPU time (s) 1136.75
Current children cumulated vsize (Kb) 105244

[startup+1150.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 23868 0 0 0 114357 314 0 0 25 0 1 0 1854943923 106160128 23539 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 25918 23539 145 145 0 25773 0
[pid=6297] vsize: 103672
Current children cumulated CPU time (s) 1146.72
Current children cumulated vsize (Kb) 105796

[startup+1160.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 24060 0 0 0 115352 317 0 0 25 0 1 0 1854943923 106946560 23731 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 26110 23731 145 145 0 25965 0
[pid=6297] vsize: 104440
Current children cumulated CPU time (s) 1156.7
Current children cumulated vsize (Kb) 106564

[startup+1170.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 24222 0 0 0 116347 319 0 0 25 0 1 0 1854943923 107610112 23893 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 26272 23893 145 145 0 26127 0
[pid=6297] vsize: 105088
Current children cumulated CPU time (s) 1166.67
Current children cumulated vsize (Kb) 107212

[startup+1180.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 24371 0 0 0 117342 322 0 0 25 0 1 0 1854943923 108220416 24042 4294967295 134512640 135094434 3221224432 3221223344 134587903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 26421 24042 145 145 0 26276 0
[pid=6297] vsize: 105684
Current children cumulated CPU time (s) 1176.65
Current children cumulated vsize (Kb) 107808

[startup+1190.09 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 24510 0 0 0 118337 324 0 0 25 0 1 0 1854943923 108789760 24181 4294967295 134512640 135094434 3221224432 3221223376 134564788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6297/statm): 26560 24181 145 145 0 26415 0
[pid=6297] vsize: 106240
Current children cumulated CPU time (s) 1186.62
Current children cumulated vsize (Kb) 108364

[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 24713 0 0 0 119329 328 0 0 25 0 1 0 1854943923 109621248 24384 4294967295 134512640 135094434 3221224432 3221223324 134795992 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 26763 24384 145 145 0 26618 0
[pid=6297] vsize: 107052
Current children cumulated CPU time (s) 1196.58
Current children cumulated vsize (Kb) 109176

[startup+1210.1 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 24864 0 0 0 120324 330 0 0 25 0 1 0 1854943923 110239744 24535 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 26914 24535 145 145 0 26769 0
[pid=6297] vsize: 107656
Current children cumulated CPU time (s) 1206.55
Current children cumulated vsize (Kb) 109780



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 6297
Raw data (/proc/6293/stat): 6293 (minisat+_script) S 6292 6293 19316 0 -1 0 289 239 0 0 0 1 0 0 19 0 1 0 1854943918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6293/statm): 531 226 485 147 0 384 0
[pid=6293] vsize: 2124
Raw data (/proc/6297/stat): 6297 (minisat+_64-bit) R 6293 6293 19316 0 -1 0 24864 0 0 0 120324 330 0 0 25 0 1 0 1854943923 110239744 24535 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6297/statm): 26914 24535 145 145 0 26769 0
[pid=6297] vsize: 107656
Current children cumulated CPU time (s) 1206.55
Current children cumulated vsize (Kb) 109780

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

Child status: 0
Real time (s): 1210.15
CPU time (s): 1206.6
CPU user time (s): 1203.24
CPU system time (s): 3.35149
CPU usage (%): 99.7066
Max. virtual memory (cumulated for all children) (Kb): 109780



Verifier Data




ERROR: no interpretation found !