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

Namesubmitted/manquinho/primes-dimacs-cnf/normalized-par32-4.opb
MD5SUM4ad922a0ad53056b410be6ab5caa6b5b
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 6352
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 6352
Number of bits of the sum of numbers in the objective function 13
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 6352
Number of bits of the biggest sum of numbers13
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables6352
Total number of constraints13489
Number of constraints which are clauses13489
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint3

Trace number 1541

Launcher Data

LAUNCH ON wulflinc18 THE 2005-09-18 15:33:25 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2540 boxname=wulflinc18 idbench=196 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4ad922a0ad53056b410be6ab5caa6b5b  /oldhome/oroussel/tmp/wulflinc18/normalized-par32-4.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc18/normalized-par32-4.opb
IDLAUNCH: 2540
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
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:        917928 kB
Buffers:         34984 kB
Cached:          46792 kB
SwapCached:        844 kB
Active:          65056 kB
Inactive:        19372 kB
HighTotal:      131008 kB
HighFree:        81228 kB
LowTotal:       903652 kB
LowFree:        836700 kB
SwapTotal:     2097892 kB
SwapFree:      2096548 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5764 kB
Slab:            26640 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 15:53:25 (client local time) WITH STATUS 0 IN 1200.15 SECONDS
stats: 2540 7 1200.15 0

Solver Data

c Parsing PB file...
c Converting 13075 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    9815    24584 |    3271       0        0     nan |  0.000 % |
c |       100 |    9815    24584 |    3598     100     1175    11.8 | 24.906 % |
c |       250 |    9815    24584 |    3957     250     4761    19.0 | 24.906 % |
c |       476 |    9815    24584 |    4353     476     8036    16.9 | 24.906 % |
c |       814 |    9805    24562 |    4789     813    16099    19.8 | 24.969 % |
c |      1321 |    9805    24562 |    5267    1320    31268    23.7 | 24.969 % |
c |      2080 |    9805    24562 |    5794    2079    42787    20.6 | 24.969 % |
c |      3220 |    9805    24562 |    6374    3219    75648    23.5 | 24.969 % |
c |      4928 |    9805    24562 |    7011    4927   107201    21.8 | 24.969 % |
c |      7490 |    9805    24562 |    7712    7489   180306    24.1 | 24.969 % |
c |     11334 |    9805    24562 |    8484    6526   158927    24.4 | 24.969 % |
c |     17101 |    9805    24562 |    9332    7165   174694    24.4 | 24.969 % |
c |     25751 |    9805    24562 |   10265   10288   256474    24.9 | 24.969 % |
c |     38726 |    9805    24562 |   11292   11339   271909    24.0 | 24.969 % |
c |     58189 |    9805    24562 |   12421   11405   270262    23.7 | 24.969 % |
c |     87381 |    9805    24562 |   13663   12378   287949    23.3 | 24.969 % |
c |    131171 |    9805    24562 |   15030   10244   241970    23.6 | 24.969 % |
c |    196856 |    9805    24562 |   16533    8936   193461    21.6 | 24.969 % |
c |    295383 |    9805    24562 |   18186   16303   374771    23.0 | 24.969 % |
c |    443174 |    9805    24562 |   20005   15022   328559    21.9 | 24.969 % |

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/3831/stat): 3831 (minisat+_script) R 3830 3831 31027 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1842332430 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/3831/statm): 174 3 169 147 0 27 0
[pid=3831] 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=3832
New process pid=3833
New process pid=3834
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
One traced child (pid=3833) exited with status: 0
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=3834) exited with status: 0
One traced child (pid=3832) exited with status: 0
New process pid=3835
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-par32-4.opb

[startup+10.0032 s]
Raw data (loadavg): 0.93 0.96 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1325 0 0 0 985 5 0 0 25 0 1 0 1842332435 5627904 1274 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1374 1274 145 145 0 1229 0
[pid=3835] vsize: 5496
Current children cumulated CPU time (s) 9.91
Current children cumulated vsize (Kb) 7620

[startup+20.0052 s]
Raw data (loadavg): 0.94 0.96 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1325 0 0 0 1984 6 0 0 25 0 1 0 1842332435 5627904 1274 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1374 1274 145 145 0 1229 0
[pid=3835] vsize: 5496
Current children cumulated CPU time (s) 19.91
Current children cumulated vsize (Kb) 7620

[startup+30.0061 s]
Raw data (loadavg): 0.95 0.96 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1325 0 0 0 2985 6 0 0 25 0 1 0 1842332435 5627904 1274 4294967295 134512640 135094434 3221224448 3221223088 134558264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1374 1274 145 145 0 1229 0
[pid=3835] vsize: 5496
Current children cumulated CPU time (s) 29.92
Current children cumulated vsize (Kb) 7620

[startup+40.006 s]
Raw data (loadavg): 0.96 0.96 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1325 0 0 0 3985 6 0 0 25 0 1 0 1842332435 5627904 1274 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1374 1274 145 145 0 1229 0
[pid=3835] vsize: 5496
Current children cumulated CPU time (s) 39.92
Current children cumulated vsize (Kb) 7620

[startup+50.0069 s]
Raw data (loadavg): 0.96 0.96 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1325 0 0 0 4985 6 0 0 25 0 1 0 1842332435 5627904 1274 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1374 1274 145 145 0 1229 0
[pid=3835] vsize: 5496
Current children cumulated CPU time (s) 49.92
Current children cumulated vsize (Kb) 7620

[startup+60.0068 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1325 0 0 0 5985 6 0 0 25 0 1 0 1842332435 5627904 1274 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1374 1274 145 145 0 1229 0
[pid=3835] vsize: 5496
Current children cumulated CPU time (s) 59.92
Current children cumulated vsize (Kb) 7620

[startup+70.0088 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1325 0 0 0 6985 6 0 0 25 0 1 0 1842332435 5627904 1274 4294967295 134512640 135094434 3221224448 3221223040 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1374 1274 145 145 0 1229 0
[pid=3835] vsize: 5496
Current children cumulated CPU time (s) 69.92
Current children cumulated vsize (Kb) 7620

[startup+80.0097 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1325 0 0 0 7985 6 0 0 25 0 1 0 1842332435 5627904 1274 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1374 1274 145 145 0 1229 0
[pid=3835] vsize: 5496
Current children cumulated CPU time (s) 79.92
Current children cumulated vsize (Kb) 7620

[startup+90.0096 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1325 0 0 0 8985 6 0 0 25 0 1 0 1842332435 5627904 1274 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1374 1274 145 145 0 1229 0
[pid=3835] vsize: 5496
Current children cumulated CPU time (s) 89.92
Current children cumulated vsize (Kb) 7620

[startup+100.011 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1325 0 0 0 9985 6 0 0 25 0 1 0 1842332435 5627904 1274 4294967295 134512640 135094434 3221224448 3221223120 134555945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3835/statm): 1374 1274 145 145 0 1229 0
[pid=3835] vsize: 5496
Current children cumulated CPU time (s) 99.92
Current children cumulated vsize (Kb) 7620

[startup+110.011 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1325 0 0 0 10985 6 0 0 25 0 1 0 1842332435 5627904 1274 4294967295 134512640 135094434 3221224448 3221223092 134558040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1374 1274 145 145 0 1229 0
[pid=3835] vsize: 5496
Current children cumulated CPU time (s) 109.92
Current children cumulated vsize (Kb) 7620

[startup+120.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1325 0 0 0 11985 6 0 0 25 0 1 0 1842332435 5627904 1274 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1374 1274 145 145 0 1229 0
[pid=3835] vsize: 5496
Current children cumulated CPU time (s) 119.92
Current children cumulated vsize (Kb) 7620

[startup+130.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1331 0 0 0 12985 6 0 0 25 0 1 0 1842332435 5660672 1280 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1382 1280 145 145 0 1237 0
[pid=3835] vsize: 5528
Current children cumulated CPU time (s) 129.92
Current children cumulated vsize (Kb) 7652

[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1332 0 0 0 13985 7 0 0 25 0 1 0 1842332435 5660672 1281 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1382 1281 145 145 0 1237 0
[pid=3835] vsize: 5528
Current children cumulated CPU time (s) 139.93
Current children cumulated vsize (Kb) 7652

[startup+150.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1338 0 0 0 14986 7 0 0 25 0 1 0 1842332435 5693440 1287 4294967295 134512640 135094434 3221224448 3221223076 134557564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1390 1287 145 145 0 1245 0
[pid=3835] vsize: 5560
Current children cumulated CPU time (s) 149.94
Current children cumulated vsize (Kb) 7684

[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1378 0 0 0 15985 7 0 0 25 0 1 0 1842332435 5861376 1327 4294967295 134512640 135094434 3221224448 3221223104 134558135 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1431 1327 145 145 0 1286 0
[pid=3835] vsize: 5724
Current children cumulated CPU time (s) 159.93
Current children cumulated vsize (Kb) 7848

[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1395 0 0 0 16984 8 0 0 25 0 1 0 1842332435 5931008 1344 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1448 1344 145 145 0 1303 0
[pid=3835] vsize: 5792
Current children cumulated CPU time (s) 169.93
Current children cumulated vsize (Kb) 7916

[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1415 0 0 0 17984 9 0 0 25 0 1 0 1842332435 6033408 1364 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1473 1364 145 145 0 1328 0
[pid=3835] vsize: 5892
Current children cumulated CPU time (s) 179.94
Current children cumulated vsize (Kb) 8016

[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1423 0 0 0 18984 9 0 0 25 0 1 0 1842332435 6045696 1372 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1476 1372 145 145 0 1331 0
[pid=3835] vsize: 5904
Current children cumulated CPU time (s) 189.94
Current children cumulated vsize (Kb) 8028

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1430 0 0 0 19983 9 0 0 25 0 1 0 1842332435 6078464 1379 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1484 1379 145 145 0 1339 0
[pid=3835] vsize: 5936
Current children cumulated CPU time (s) 199.93
Current children cumulated vsize (Kb) 8060

[startup+210.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1437 0 0 0 20983 10 0 0 25 0 1 0 1842332435 6111232 1386 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1492 1386 145 145 0 1347 0
[pid=3835] vsize: 5968
Current children cumulated CPU time (s) 209.94
Current children cumulated vsize (Kb) 8092

[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1437 0 0 0 21984 10 0 0 25 0 1 0 1842332435 6111232 1386 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1492 1386 145 145 0 1347 0
[pid=3835] vsize: 5968
Current children cumulated CPU time (s) 219.95
Current children cumulated vsize (Kb) 8092

[startup+230.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1437 0 0 0 22984 10 0 0 25 0 1 0 1842332435 6111232 1386 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1492 1386 145 145 0 1347 0
[pid=3835] vsize: 5968
Current children cumulated CPU time (s) 229.95
Current children cumulated vsize (Kb) 8092

[startup+240.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1448 0 0 0 23984 10 0 0 25 0 1 0 1842332435 6164480 1397 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1505 1397 145 145 0 1360 0
[pid=3835] vsize: 6020
Current children cumulated CPU time (s) 239.95
Current children cumulated vsize (Kb) 8144

[startup+250.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1502 0 0 0 24983 10 0 0 25 0 1 0 1842332435 6471680 1451 4294967295 134512640 135094434 3221224448 3221223104 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1580 1451 145 145 0 1435 0
[pid=3835] vsize: 6320
Current children cumulated CPU time (s) 249.94
Current children cumulated vsize (Kb) 8444

[startup+260.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1508 0 0 0 25983 10 0 0 25 0 1 0 1842332435 6537216 1457 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1596 1457 145 145 0 1451 0
[pid=3835] vsize: 6384
Current children cumulated CPU time (s) 259.94
Current children cumulated vsize (Kb) 8508

[startup+270.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1516 0 0 0 26984 10 0 0 25 0 1 0 1842332435 6557696 1465 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1601 1465 145 145 0 1456 0
[pid=3835] vsize: 6404
Current children cumulated CPU time (s) 269.95
Current children cumulated vsize (Kb) 8528

[startup+280.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1516 0 0 0 27984 11 0 0 25 0 1 0 1842332435 6557696 1465 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1601 1465 145 145 0 1456 0
[pid=3835] vsize: 6404
Current children cumulated CPU time (s) 279.96
Current children cumulated vsize (Kb) 8528

[startup+290.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1521 0 0 0 28984 11 0 0 25 0 1 0 1842332435 6590464 1470 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1609 1470 145 145 0 1464 0
[pid=3835] vsize: 6436
Current children cumulated CPU time (s) 289.96
Current children cumulated vsize (Kb) 8560

[startup+300.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1523 0 0 0 29984 11 0 0 25 0 1 0 1842332435 6590464 1472 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1609 1472 145 145 0 1464 0
[pid=3835] vsize: 6436
Current children cumulated CPU time (s) 299.96
Current children cumulated vsize (Kb) 8560

[startup+310.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1523 0 0 0 30984 11 0 0 25 0 1 0 1842332435 6590464 1472 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1609 1472 145 145 0 1464 0
[pid=3835] vsize: 6436
Current children cumulated CPU time (s) 309.96
Current children cumulated vsize (Kb) 8560

[startup+320.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1531 0 0 0 31984 11 0 0 25 0 1 0 1842332435 6623232 1480 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1617 1480 145 145 0 1472 0
[pid=3835] vsize: 6468
Current children cumulated CPU time (s) 319.96
Current children cumulated vsize (Kb) 8592

[startup+330.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1534 0 0 0 32985 11 0 0 25 0 1 0 1842332435 6623232 1483 4294967295 134512640 135094434 3221224448 3221223136 134554751 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1617 1483 145 145 0 1472 0
[pid=3835] vsize: 6468
Current children cumulated CPU time (s) 329.97
Current children cumulated vsize (Kb) 8592

[startup+340.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1536 0 0 0 33985 11 0 0 25 0 1 0 1842332435 6623232 1485 4294967295 134512640 135094434 3221224448 3221223072 134557669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1617 1485 145 145 0 1472 0
[pid=3835] vsize: 6468
Current children cumulated CPU time (s) 339.97
Current children cumulated vsize (Kb) 8592

[startup+350.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1537 0 0 0 34985 11 0 0 25 0 1 0 1842332435 6623232 1486 4294967295 134512640 135094434 3221224448 3221223072 134557711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1617 1486 145 145 0 1472 0
[pid=3835] vsize: 6468
Current children cumulated CPU time (s) 349.97
Current children cumulated vsize (Kb) 8592

[startup+360.034 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1538 0 0 0 35985 11 0 0 25 0 1 0 1842332435 6623232 1487 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1617 1487 145 145 0 1472 0
[pid=3835] vsize: 6468
Current children cumulated CPU time (s) 359.97
Current children cumulated vsize (Kb) 8592

[startup+370.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1538 0 0 0 36985 12 0 0 25 0 1 0 1842332435 6623232 1487 4294967295 134512640 135094434 3221224448 3221223120 134555560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1617 1487 145 145 0 1472 0
[pid=3835] vsize: 6468
Current children cumulated CPU time (s) 369.98
Current children cumulated vsize (Kb) 8592

[startup+380.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1539 0 0 0 37985 12 0 0 25 0 1 0 1842332435 6623232 1488 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1617 1488 145 145 0 1472 0
[pid=3835] vsize: 6468
Current children cumulated CPU time (s) 379.98
Current children cumulated vsize (Kb) 8592

[startup+390.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1555 0 0 0 38985 12 0 0 25 0 1 0 1842332435 6684672 1504 4294967295 134512640 135094434 3221224448 3221223080 134557638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1632 1504 145 145 0 1487 0
[pid=3835] vsize: 6528
Current children cumulated CPU time (s) 389.98
Current children cumulated vsize (Kb) 8652

[startup+400.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1555 0 0 0 39985 12 0 0 25 0 1 0 1842332435 6684672 1504 4294967295 134512640 135094434 3221224448 3221223104 134558254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1632 1504 145 145 0 1487 0
[pid=3835] vsize: 6528
Current children cumulated CPU time (s) 399.98
Current children cumulated vsize (Kb) 8652

[startup+410.038 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1558 0 0 0 40985 12 0 0 25 0 1 0 1842332435 6696960 1507 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1635 1507 145 145 0 1490 0
[pid=3835] vsize: 6540
Current children cumulated CPU time (s) 409.98
Current children cumulated vsize (Kb) 8664

[startup+420.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1558 0 0 0 41985 12 0 0 25 0 1 0 1842332435 6696960 1507 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1635 1507 145 145 0 1490 0
[pid=3835] vsize: 6540
Current children cumulated CPU time (s) 419.98
Current children cumulated vsize (Kb) 8664

[startup+430.04 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1558 0 0 0 42986 12 0 0 25 0 1 0 1842332435 6696960 1507 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1635 1507 145 145 0 1490 0
[pid=3835] vsize: 6540
Current children cumulated CPU time (s) 429.99
Current children cumulated vsize (Kb) 8664

[startup+440.041 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1558 0 0 0 43986 12 0 0 25 0 1 0 1842332435 6696960 1507 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1635 1507 145 145 0 1490 0
[pid=3835] vsize: 6540
Current children cumulated CPU time (s) 439.99
Current children cumulated vsize (Kb) 8664

[startup+450.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1558 0 0 0 44986 12 0 0 25 0 1 0 1842332435 6696960 1507 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1635 1507 145 145 0 1490 0
[pid=3835] vsize: 6540
Current children cumulated CPU time (s) 449.99
Current children cumulated vsize (Kb) 8664

[startup+460.043 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1558 0 0 0 45986 12 0 0 25 0 1 0 1842332435 6696960 1507 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1635 1507 145 145 0 1490 0
[pid=3835] vsize: 6540
Current children cumulated CPU time (s) 459.99
Current children cumulated vsize (Kb) 8664

[startup+470.044 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1558 0 0 0 46986 12 0 0 25 0 1 0 1842332435 6696960 1507 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1635 1507 145 145 0 1490 0
[pid=3835] vsize: 6540
Current children cumulated CPU time (s) 469.99
Current children cumulated vsize (Kb) 8664

[startup+480.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1558 0 0 0 47987 12 0 0 25 0 1 0 1842332435 6696960 1507 4294967295 134512640 135094434 3221224448 3221223080 134557638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1635 1507 145 145 0 1490 0
[pid=3835] vsize: 6540
Current children cumulated CPU time (s) 480
Current children cumulated vsize (Kb) 8664

[startup+490.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1558 0 0 0 48987 12 0 0 25 0 1 0 1842332435 6696960 1507 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1635 1507 145 145 0 1490 0
[pid=3835] vsize: 6540
Current children cumulated CPU time (s) 490
Current children cumulated vsize (Kb) 8664

[startup+500.046 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1562 0 0 0 49987 12 0 0 25 0 1 0 1842332435 6721536 1511 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1641 1511 145 145 0 1496 0
[pid=3835] vsize: 6564
Current children cumulated CPU time (s) 500
Current children cumulated vsize (Kb) 8688

[startup+510.046 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1562 0 0 0 50987 13 0 0 25 0 1 0 1842332435 6721536 1511 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1641 1511 145 145 0 1496 0
[pid=3835] vsize: 6564
Current children cumulated CPU time (s) 510.01
Current children cumulated vsize (Kb) 8688

[startup+520.048 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1562 0 0 0 51987 13 0 0 25 0 1 0 1842332435 6721536 1511 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1641 1511 145 145 0 1496 0
[pid=3835] vsize: 6564
Current children cumulated CPU time (s) 520.01
Current children cumulated vsize (Kb) 8688

[startup+530.049 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1562 0 0 0 52987 13 0 0 25 0 1 0 1842332435 6721536 1511 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1641 1511 145 145 0 1496 0
[pid=3835] vsize: 6564
Current children cumulated CPU time (s) 530.01
Current children cumulated vsize (Kb) 8688

[startup+540.05 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1562 0 0 0 53987 13 0 0 25 0 1 0 1842332435 6721536 1511 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1641 1511 145 145 0 1496 0
[pid=3835] vsize: 6564
Current children cumulated CPU time (s) 540.01
Current children cumulated vsize (Kb) 8688

[startup+550.051 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1562 0 0 0 54987 13 0 0 25 0 1 0 1842332435 6721536 1511 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1641 1511 145 145 0 1496 0
[pid=3835] vsize: 6564
Current children cumulated CPU time (s) 550.01
Current children cumulated vsize (Kb) 8688

[startup+560.051 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1568 0 0 0 55988 13 0 0 25 0 1 0 1842332435 6754304 1517 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1649 1517 145 145 0 1504 0
[pid=3835] vsize: 6596
Current children cumulated CPU time (s) 560.02
Current children cumulated vsize (Kb) 8720

[startup+570.053 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1581 0 0 0 56988 13 0 0 25 0 1 0 1842332435 6819840 1530 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3835/statm): 1665 1530 145 145 0 1520 0
[pid=3835] vsize: 6660
Current children cumulated CPU time (s) 570.02
Current children cumulated vsize (Kb) 8784

[startup+580.055 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1621 0 0 0 57987 13 0 0 25 0 1 0 1842332435 6971392 1570 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1702 1570 145 145 0 1557 0
[pid=3835] vsize: 6808
Current children cumulated CPU time (s) 580.01
Current children cumulated vsize (Kb) 8932

[startup+590.055 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1621 0 0 0 58987 13 0 0 25 0 1 0 1842332435 6971392 1570 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1702 1570 145 145 0 1557 0
[pid=3835] vsize: 6808
Current children cumulated CPU time (s) 590.01
Current children cumulated vsize (Kb) 8932

[startup+600.056 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1630 0 0 0 59987 13 0 0 25 0 1 0 1842332435 7012352 1579 4294967295 134512640 135094434 3221224448 3221223136 134554676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1712 1579 145 145 0 1567 0
[pid=3835] vsize: 6848
Current children cumulated CPU time (s) 600.01
Current children cumulated vsize (Kb) 8972

[startup+610.057 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1633 0 0 0 60987 13 0 0 25 0 1 0 1842332435 7045120 1582 4294967295 134512640 135094434 3221224448 3221223104 134557917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1720 1582 145 145 0 1575 0
[pid=3835] vsize: 6880
Current children cumulated CPU time (s) 610.01
Current children cumulated vsize (Kb) 9004

[startup+620.058 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1643 0 0 0 61987 13 0 0 25 0 1 0 1842332435 7073792 1592 4294967295 134512640 135094434 3221224448 3221223104 134557823 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1727 1592 145 145 0 1582 0
[pid=3835] vsize: 6908
Current children cumulated CPU time (s) 620.01
Current children cumulated vsize (Kb) 9032

[startup+630.059 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1643 0 0 0 62987 13 0 0 25 0 1 0 1842332435 7073792 1592 4294967295 134512640 135094434 3221224448 3221223104 134557893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1727 1592 145 145 0 1582 0
[pid=3835] vsize: 6908
Current children cumulated CPU time (s) 630.01
Current children cumulated vsize (Kb) 9032

[startup+640.059 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1653 0 0 0 63987 13 0 0 25 0 1 0 1842332435 7139328 1602 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1743 1602 145 145 0 1598 0
[pid=3835] vsize: 6972
Current children cumulated CPU time (s) 640.01
Current children cumulated vsize (Kb) 9096

[startup+650.06 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1653 0 0 0 64988 13 0 0 25 0 1 0 1842332435 7139328 1602 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1743 1602 145 145 0 1598 0
[pid=3835] vsize: 6972
Current children cumulated CPU time (s) 650.02
Current children cumulated vsize (Kb) 9096

[startup+660.061 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1653 0 0 0 65988 13 0 0 25 0 1 0 1842332435 7139328 1602 4294967295 134512640 135094434 3221224448 3221223120 134555957 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1743 1602 145 145 0 1598 0
[pid=3835] vsize: 6972
Current children cumulated CPU time (s) 660.02
Current children cumulated vsize (Kb) 9096

[startup+670.063 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1653 0 0 0 66988 13 0 0 25 0 1 0 1842332435 7139328 1602 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1743 1602 145 145 0 1598 0
[pid=3835] vsize: 6972
Current children cumulated CPU time (s) 670.02
Current children cumulated vsize (Kb) 9096

[startup+680.064 s]
Raw data (loadavg): 1.15 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1653 0 0 0 67988 13 0 0 25 0 1 0 1842332435 7139328 1602 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1743 1602 145 145 0 1598 0
[pid=3835] vsize: 6972
Current children cumulated CPU time (s) 680.02
Current children cumulated vsize (Kb) 9096

[startup+690.065 s]
Raw data (loadavg): 1.12 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1653 0 0 0 68989 13 0 0 25 0 1 0 1842332435 7139328 1602 4294967295 134512640 135094434 3221224448 3221223060 134563069 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1743 1602 145 145 0 1598 0
[pid=3835] vsize: 6972
Current children cumulated CPU time (s) 690.03
Current children cumulated vsize (Kb) 9096

[startup+700.066 s]
Raw data (loadavg): 1.10 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1654 0 0 0 69989 13 0 0 25 0 1 0 1842332435 7139328 1603 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1743 1603 145 145 0 1598 0
[pid=3835] vsize: 6972
Current children cumulated CPU time (s) 700.03
Current children cumulated vsize (Kb) 9096

[startup+710.067 s]
Raw data (loadavg): 1.09 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1654 0 0 0 70989 13 0 0 25 0 1 0 1842332435 7139328 1603 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1743 1603 145 145 0 1598 0
[pid=3835] vsize: 6972
Current children cumulated CPU time (s) 710.03
Current children cumulated vsize (Kb) 9096

[startup+720.068 s]
Raw data (loadavg): 1.07 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1665 0 0 0 71989 13 0 0 25 0 1 0 1842332435 7204864 1614 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1759 1614 145 145 0 1614 0
[pid=3835] vsize: 7036
Current children cumulated CPU time (s) 720.03
Current children cumulated vsize (Kb) 9160

[startup+730.069 s]
Raw data (loadavg): 1.06 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1665 0 0 0 72990 13 0 0 25 0 1 0 1842332435 7204864 1614 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1759 1614 145 145 0 1614 0
[pid=3835] vsize: 7036
Current children cumulated CPU time (s) 730.04
Current children cumulated vsize (Kb) 9160

[startup+740.07 s]
Raw data (loadavg): 1.05 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1665 0 0 0 73990 14 0 0 25 0 1 0 1842332435 7204864 1614 4294967295 134512640 135094434 3221224448 3221223040 134551448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1759 1614 145 145 0 1614 0
[pid=3835] vsize: 7036
Current children cumulated CPU time (s) 740.05
Current children cumulated vsize (Kb) 9160

[startup+750.071 s]
Raw data (loadavg): 1.04 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1665 0 0 0 74990 14 0 0 25 0 1 0 1842332435 7204864 1614 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1759 1614 145 145 0 1614 0
[pid=3835] vsize: 7036
Current children cumulated CPU time (s) 750.05
Current children cumulated vsize (Kb) 9160

[startup+760.072 s]
Raw data (loadavg): 1.04 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1665 0 0 0 75990 14 0 0 25 0 1 0 1842332435 7204864 1614 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1759 1614 145 145 0 1614 0
[pid=3835] vsize: 7036
Current children cumulated CPU time (s) 760.05
Current children cumulated vsize (Kb) 9160

[startup+770.072 s]
Raw data (loadavg): 1.03 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1665 0 0 0 76989 15 0 0 25 0 1 0 1842332435 7204864 1614 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1759 1614 145 145 0 1614 0
[pid=3835] vsize: 7036
Current children cumulated CPU time (s) 770.05
Current children cumulated vsize (Kb) 9160

[startup+780.073 s]
Raw data (loadavg): 1.03 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1665 0 0 0 77989 15 0 0 25 0 1 0 1842332435 7204864 1614 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1759 1614 145 145 0 1614 0
[pid=3835] vsize: 7036
Current children cumulated CPU time (s) 780.05
Current children cumulated vsize (Kb) 9160

[startup+790.074 s]
Raw data (loadavg): 1.02 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1665 0 0 0 78989 15 0 0 25 0 1 0 1842332435 7204864 1614 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1759 1614 145 145 0 1614 0
[pid=3835] vsize: 7036
Current children cumulated CPU time (s) 790.05
Current children cumulated vsize (Kb) 9160

[startup+800.075 s]
Raw data (loadavg): 1.02 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1665 0 0 0 79989 16 0 0 25 0 1 0 1842332435 7204864 1614 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1759 1614 145 145 0 1614 0
[pid=3835] vsize: 7036
Current children cumulated CPU time (s) 800.06
Current children cumulated vsize (Kb) 9160

[startup+810.076 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1665 0 0 0 80989 16 0 0 25 0 1 0 1842332435 7204864 1614 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1759 1614 145 145 0 1614 0
[pid=3835] vsize: 7036
Current children cumulated CPU time (s) 810.06
Current children cumulated vsize (Kb) 9160

[startup+820.078 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1665 0 0 0 81989 16 0 0 25 0 1 0 1842332435 7204864 1614 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1759 1614 145 145 0 1614 0
[pid=3835] vsize: 7036
Current children cumulated CPU time (s) 820.06
Current children cumulated vsize (Kb) 9160

[startup+830.079 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1665 0 0 0 82989 16 0 0 25 0 1 0 1842332435 7204864 1614 4294967295 134512640 135094434 3221224448 3221223104 134557917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1759 1614 145 145 0 1614 0
[pid=3835] vsize: 7036
Current children cumulated CPU time (s) 830.06
Current children cumulated vsize (Kb) 9160

[startup+840.08 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1665 0 0 0 83989 16 0 0 25 0 1 0 1842332435 7204864 1614 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1759 1614 145 145 0 1614 0
[pid=3835] vsize: 7036
Current children cumulated CPU time (s) 840.06
Current children cumulated vsize (Kb) 9160

[startup+850.081 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1674 0 0 0 84989 17 0 0 25 0 1 0 1842332435 7270400 1623 4294967295 134512640 135094434 3221224448 3221223088 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1775 1623 145 145 0 1630 0
[pid=3835] vsize: 7100
Current children cumulated CPU time (s) 850.07
Current children cumulated vsize (Kb) 9224

[startup+860.081 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1676 0 0 0 85989 17 0 0 25 0 1 0 1842332435 7270400 1625 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1775 1625 145 145 0 1630 0
[pid=3835] vsize: 7100
Current children cumulated CPU time (s) 860.07
Current children cumulated vsize (Kb) 9224

[startup+870.082 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1676 0 0 0 86990 17 0 0 25 0 1 0 1842332435 7270400 1625 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1775 1625 145 145 0 1630 0
[pid=3835] vsize: 7100
Current children cumulated CPU time (s) 870.08
Current children cumulated vsize (Kb) 9224

[startup+880.083 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1676 0 0 0 87989 17 0 0 25 0 1 0 1842332435 7270400 1625 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1775 1625 145 145 0 1630 0
[pid=3835] vsize: 7100
Current children cumulated CPU time (s) 880.07
Current children cumulated vsize (Kb) 9224

[startup+890.083 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1688 0 0 0 88989 17 0 0 25 0 1 0 1842332435 7315456 1637 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1786 1637 145 145 0 1641 0
[pid=3835] vsize: 7144
Current children cumulated CPU time (s) 890.07
Current children cumulated vsize (Kb) 9268

[startup+900.084 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1712 0 0 0 89989 17 0 0 25 0 1 0 1842332435 7409664 1661 4294967295 134512640 135094434 3221224448 3221223104 134557804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1809 1661 145 145 0 1664 0
[pid=3835] vsize: 7236
Current children cumulated CPU time (s) 900.07
Current children cumulated vsize (Kb) 9360

[startup+910.085 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1720 0 0 0 90988 18 0 0 25 0 1 0 1842332435 7458816 1669 4294967295 134512640 135094434 3221224448 3221223120 134555563 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1821 1669 145 145 0 1676 0
[pid=3835] vsize: 7284
Current children cumulated CPU time (s) 910.07
Current children cumulated vsize (Kb) 9408

[startup+920.085 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1733 0 0 0 91989 18 0 0 25 0 1 0 1842332435 7495680 1682 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1830 1682 145 145 0 1685 0
[pid=3835] vsize: 7320
Current children cumulated CPU time (s) 920.08
Current children cumulated vsize (Kb) 9444

[startup+930.086 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1733 0 0 0 92989 18 0 0 25 0 1 0 1842332435 7495680 1682 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1830 1682 145 145 0 1685 0
[pid=3835] vsize: 7320
Current children cumulated CPU time (s) 930.08
Current children cumulated vsize (Kb) 9444

[startup+940.087 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1734 0 0 0 93989 18 0 0 25 0 1 0 1842332435 7495680 1683 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1830 1683 145 145 0 1685 0
[pid=3835] vsize: 7320
Current children cumulated CPU time (s) 940.08
Current children cumulated vsize (Kb) 9444

[startup+950.088 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1737 0 0 0 94989 18 0 0 25 0 1 0 1842332435 7512064 1686 4294967295 134512640 135094434 3221224448 3221223104 134557984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1834 1686 145 145 0 1689 0
[pid=3835] vsize: 7336
Current children cumulated CPU time (s) 950.08
Current children cumulated vsize (Kb) 9460

[startup+960.089 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1745 0 0 0 95989 18 0 0 25 0 1 0 1842332435 7561216 1694 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1846 1694 145 145 0 1701 0
[pid=3835] vsize: 7384
Current children cumulated CPU time (s) 960.08
Current children cumulated vsize (Kb) 9508

[startup+970.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1746 0 0 0 96990 18 0 0 25 0 1 0 1842332435 7561216 1695 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1846 1695 145 145 0 1701 0
[pid=3835] vsize: 7384
Current children cumulated CPU time (s) 970.09
Current children cumulated vsize (Kb) 9508

[startup+980.091 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1746 0 0 0 97990 18 0 0 25 0 1 0 1842332435 7561216 1695 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1846 1695 145 145 0 1701 0
[pid=3835] vsize: 7384
Current children cumulated CPU time (s) 980.09
Current children cumulated vsize (Kb) 9508

[startup+990.092 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1746 0 0 0 98990 18 0 0 25 0 1 0 1842332435 7561216 1695 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1846 1695 145 145 0 1701 0
[pid=3835] vsize: 7384
Current children cumulated CPU time (s) 990.09
Current children cumulated vsize (Kb) 9508

[startup+1000.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1746 0 0 0 99990 18 0 0 25 0 1 0 1842332435 7561216 1695 4294967295 134512640 135094434 3221224448 3221223152 134554398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1846 1695 145 145 0 1701 0
[pid=3835] vsize: 7384
Current children cumulated CPU time (s) 1000.09
Current children cumulated vsize (Kb) 9508

[startup+1010.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1746 0 0 0 100990 18 0 0 25 0 1 0 1842332435 7561216 1695 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1846 1695 145 145 0 1701 0
[pid=3835] vsize: 7384
Current children cumulated CPU time (s) 1010.09
Current children cumulated vsize (Kb) 9508

[startup+1020.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1746 0 0 0 101990 18 0 0 25 0 1 0 1842332435 7561216 1695 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1846 1695 145 145 0 1701 0
[pid=3835] vsize: 7384
Current children cumulated CPU time (s) 1020.09
Current children cumulated vsize (Kb) 9508

[startup+1030.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1746 0 0 0 102991 18 0 0 25 0 1 0 1842332435 7561216 1695 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1846 1695 145 145 0 1701 0
[pid=3835] vsize: 7384
Current children cumulated CPU time (s) 1030.1
Current children cumulated vsize (Kb) 9508

[startup+1040.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1746 0 0 0 103991 18 0 0 25 0 1 0 1842332435 7561216 1695 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1846 1695 145 145 0 1701 0
[pid=3835] vsize: 7384
Current children cumulated CPU time (s) 1040.1
Current children cumulated vsize (Kb) 9508

[startup+1050.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1746 0 0 0 104991 19 0 0 25 0 1 0 1842332435 7561216 1695 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1846 1695 145 145 0 1701 0
[pid=3835] vsize: 7384
Current children cumulated CPU time (s) 1050.11
Current children cumulated vsize (Kb) 9508

[startup+1060.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1746 0 0 0 105991 19 0 0 25 0 1 0 1842332435 7561216 1695 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1846 1695 145 145 0 1701 0
[pid=3835] vsize: 7384
Current children cumulated CPU time (s) 1060.11
Current children cumulated vsize (Kb) 9508

[startup+1070.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1756 0 0 0 106991 19 0 0 25 0 1 0 1842332435 7626752 1705 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1862 1705 145 145 0 1717 0
[pid=3835] vsize: 7448
Current children cumulated CPU time (s) 1070.11
Current children cumulated vsize (Kb) 9572

[startup+1080.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1756 0 0 0 107992 19 0 0 25 0 1 0 1842332435 7626752 1705 4294967295 134512640 135094434 3221224448 3221223072 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1862 1705 145 145 0 1717 0
[pid=3835] vsize: 7448
Current children cumulated CPU time (s) 1080.12
Current children cumulated vsize (Kb) 9572

[startup+1090.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1757 0 0 0 108992 19 0 0 25 0 1 0 1842332435 7626752 1706 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1862 1706 145 145 0 1717 0
[pid=3835] vsize: 7448
Current children cumulated CPU time (s) 1090.12
Current children cumulated vsize (Kb) 9572

[startup+1100.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1757 0 0 0 109992 19 0 0 25 0 1 0 1842332435 7626752 1706 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1862 1706 145 145 0 1717 0
[pid=3835] vsize: 7448
Current children cumulated CPU time (s) 1100.12
Current children cumulated vsize (Kb) 9572

[startup+1110.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1757 0 0 0 110992 19 0 0 25 0 1 0 1842332435 7626752 1706 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1862 1706 145 145 0 1717 0
[pid=3835] vsize: 7448
Current children cumulated CPU time (s) 1110.12
Current children cumulated vsize (Kb) 9572

[startup+1120.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1767 0 0 0 111992 19 0 0 25 0 1 0 1842332435 7692288 1716 4294967295 134512640 135094434 3221224448 3221223084 134557639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1878 1716 145 145 0 1733 0
[pid=3835] vsize: 7512
Current children cumulated CPU time (s) 1120.12
Current children cumulated vsize (Kb) 9636

[startup+1130.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1768 0 0 0 112992 19 0 0 25 0 1 0 1842332435 7692288 1717 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1878 1717 145 145 0 1733 0
[pid=3835] vsize: 7512
Current children cumulated CPU time (s) 1130.12
Current children cumulated vsize (Kb) 9636

[startup+1140.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1773 0 0 0 113993 19 0 0 25 0 1 0 1842332435 7712768 1722 4294967295 134512640 135094434 3221224448 3221223040 134556712 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1883 1722 145 145 0 1738 0
[pid=3835] vsize: 7532
Current children cumulated CPU time (s) 1140.13
Current children cumulated vsize (Kb) 9656

[startup+1150.11 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1773 0 0 0 114993 19 0 0 25 0 1 0 1842332435 7712768 1722 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1883 1722 145 145 0 1738 0
[pid=3835] vsize: 7532
Current children cumulated CPU time (s) 1150.13
Current children cumulated vsize (Kb) 9656

[startup+1160.11 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1773 0 0 0 115993 19 0 0 25 0 1 0 1842332435 7712768 1722 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1883 1722 145 145 0 1738 0
[pid=3835] vsize: 7532
Current children cumulated CPU time (s) 1160.13
Current children cumulated vsize (Kb) 9656

[startup+1170.11 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1774 0 0 0 116993 19 0 0 25 0 1 0 1842332435 7712768 1723 4294967295 134512640 135094434 3221224448 3221223120 134556033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1883 1723 145 145 0 1738 0
[pid=3835] vsize: 7532
Current children cumulated CPU time (s) 1170.13
Current children cumulated vsize (Kb) 9656

[startup+1180.11 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1774 0 0 0 117993 19 0 0 25 0 1 0 1842332435 7712768 1723 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1883 1723 145 145 0 1738 0
[pid=3835] vsize: 7532
Current children cumulated CPU time (s) 1180.13
Current children cumulated vsize (Kb) 9656

[startup+1190.11 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1783 0 0 0 118994 19 0 0 25 0 1 0 1842332435 7778304 1732 4294967295 134512640 135094434 3221224448 3221223120 134555265 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1899 1732 145 145 0 1754 0
[pid=3835] vsize: 7596
Current children cumulated CPU time (s) 1190.14
Current children cumulated vsize (Kb) 9720

[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1783 0 0 0 119994 19 0 0 25 0 1 0 1842332435 7778304 1732 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1899 1732 145 145 0 1754 0
[pid=3835] vsize: 7596
Current children cumulated CPU time (s) 1200.14
Current children cumulated vsize (Kb) 9720



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 3835
Raw data (/proc/3831/stat): 3831 (minisat+_script) S 3830 3831 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842332430 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3831/statm): 531 226 485 147 0 384 0
[pid=3831] vsize: 2124
Raw data (/proc/3835/stat): 3835 (minisat+_64-bit) R 3831 3831 31027 0 -1 0 1783 0 0 0 119994 19 0 0 25 0 1 0 1842332435 7778304 1732 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3835/statm): 1899 1732 145 145 0 1754 0
[pid=3835] vsize: 7596
Current children cumulated CPU time (s) 1200.14
Current children cumulated vsize (Kb) 9720

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

Child status: 0
Real time (s): 1200.12
CPU time (s): 1200.15
CPU user time (s): 1199.95
CPU system time (s): 0.204968
CPU usage (%): 100.003
Max. virtual memory (cumulated for all children) (Kb): 9720

Verifier Data

ERROR: no interpretation found !