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-3.opb
MD5SUM3d08363a486acbc90a149ca8c58297b8
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 constraints13473
Number of constraints which are clauses13473
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 1537

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        916164 kB
Buffers:         32740 kB
Cached:          58404 kB
SwapCached:        792 kB
Active:          33944 kB
Inactive:        59860 kB
HighTotal:      131008 kB
HighFree:        68936 kB
LowTotal:       903652 kB
LowFree:        847228 kB
SwapTotal:     2097136 kB
SwapFree:      2095868 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5692 kB
Slab:            18980 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 15:50:22 (client local time) WITH STATUS 0 IN 1200.12 SECONDS
stats: 2538 7 1200.12 0

Solver Data

c Parsing PB file...
c Converting 13063 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
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 |    9829    24580 |    3276       0        0     nan |  0.000 % |
c |       101 |    9829    24580 |    3603     101     1984    19.6 | 24.591 % |
c |       251 |    9829    24580 |    3963     251     3855    15.4 | 24.591 % |
c |       477 |    9829    24580 |    4360     477    11273    23.6 | 24.591 % |
c |       814 |    9829    24580 |    4796     814    15937    19.6 | 24.591 % |
c |      1321 |    9829    24580 |    5276    1321    31940    24.2 | 24.591 % |
c |      2081 |    9819    24558 |    5803    2080    47902    23.0 | 24.654 % |
c |      3220 |    9819    24558 |    6383    3219    76879    23.9 | 24.654 % |
c |      4930 |    9819    24558 |    7022    4929   124463    25.3 | 24.654 % |
c |      7492 |    9819    24558 |    7724    7491   193897    25.9 | 24.654 % |
c |     11336 |    9819    24558 |    8497    6666   165567    24.8 | 24.654 % |
c |     17102 |    9819    24558 |    9346    7321   192064    26.2 | 24.654 % |
c |     25751 |    9819    24558 |   10281   10435   254160    24.4 | 24.654 % |
c |     38726 |    9819    24558 |   11309   11433   268668    23.5 | 24.654 % |
c |     58187 |    9819    24558 |   12440   11477   264672    23.1 | 24.654 % |
c |     87379 |    9819    24558 |   13684   12371   274649    22.2 | 24.654 % |
c |    131169 |    9819    24558 |   15053   10129   219378    21.7 | 24.654 % |
c |    196853 |    9819    24558 |   16558    8870   182958    20.6 | 24.654 % |
c |    295381 |    9819    24558 |   18214   16209   376666    23.2 | 24.654 % |
c |    443170 |    9819    24558 |   20035   14819   321798    21.7 | 24.654 % |

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/8775/stat): 8775 (minisat+_script) R 8774 8775 5299 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1842358470 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/8775/statm): 174 3 169 147 0 27 0
[pid=8775] 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=8776
New process pid=8777
New process pid=8778
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
One traced child (pid=8777) exited with status: 0
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=8778) exited with status: 0
One traced child (pid=8776) exited with status: 0
New process pid=8779
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc23/normalized-par32-3.opb

[startup+10.0035 s]
Raw data (loadavg): 0.94 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1320 0 0 0 987 4 0 0 25 0 1 0 1842358475 5627904 1269 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1374 1269 145 145 0 1229 0
[pid=8779] vsize: 5496
Current children cumulated CPU time (s) 9.92
Current children cumulated vsize (Kb) 7620

[startup+20.0042 s]
Raw data (loadavg): 0.95 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1325 0 0 0 1986 5 0 0 25 0 1 0 1842358475 5627904 1274 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1374 1274 145 145 0 1229 0
[pid=8779] vsize: 5496
Current children cumulated CPU time (s) 19.92
Current children cumulated vsize (Kb) 7620

[startup+30.0058 s]
Raw data (loadavg): 0.95 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1325 0 0 0 2985 6 0 0 25 0 1 0 1842358475 5627904 1274 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1374 1274 145 145 0 1229 0
[pid=8779] vsize: 5496
Current children cumulated CPU time (s) 29.92
Current children cumulated vsize (Kb) 7620

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

[startup+50.0081 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1325 0 0 0 4984 7 0 0 25 0 1 0 1842358475 5627904 1274 4294967295 134512640 135094434 3221224448 3221223040 134556870 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1374 1274 145 145 0 1229 0
[pid=8779] vsize: 5496
Current children cumulated CPU time (s) 49.92
Current children cumulated vsize (Kb) 7620

[startup+60.0087 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1325 0 0 0 5984 7 0 0 25 0 1 0 1842358475 5627904 1274 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1374 1274 145 145 0 1229 0
[pid=8779] vsize: 5496
Current children cumulated CPU time (s) 59.92
Current children cumulated vsize (Kb) 7620

[startup+70.0094 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1325 0 0 0 6983 8 0 0 25 0 1 0 1842358475 5627904 1274 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1374 1274 145 145 0 1229 0
[pid=8779] vsize: 5496
Current children cumulated CPU time (s) 69.92
Current children cumulated vsize (Kb) 7620

[startup+80.011 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1325 0 0 0 7983 9 0 0 25 0 1 0 1842358475 5627904 1274 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1374 1274 145 145 0 1229 0
[pid=8779] vsize: 5496
Current children cumulated CPU time (s) 79.93
Current children cumulated vsize (Kb) 7620

[startup+90.0116 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1325 0 0 0 8982 9 0 0 25 0 1 0 1842358475 5627904 1274 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1374 1274 145 145 0 1229 0
[pid=8779] vsize: 5496
Current children cumulated CPU time (s) 89.92
Current children cumulated vsize (Kb) 7620

[startup+100.012 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1325 0 0 0 9982 9 0 0 25 0 1 0 1842358475 5627904 1274 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1374 1274 145 145 0 1229 0
[pid=8779] vsize: 5496
Current children cumulated CPU time (s) 99.92
Current children cumulated vsize (Kb) 7620

[startup+110.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1325 0 0 0 10982 10 0 0 25 0 1 0 1842358475 5627904 1274 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1374 1274 145 145 0 1229 0
[pid=8779] vsize: 5496
Current children cumulated CPU time (s) 109.93
Current children cumulated vsize (Kb) 7620

[startup+120.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1325 0 0 0 11981 11 0 0 25 0 1 0 1842358475 5627904 1274 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1374 1274 145 145 0 1229 0
[pid=8779] vsize: 5496
Current children cumulated CPU time (s) 119.93
Current children cumulated vsize (Kb) 7620

[startup+130.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1325 0 0 0 12981 11 0 0 25 0 1 0 1842358475 5627904 1274 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1374 1274 145 145 0 1229 0
[pid=8779] vsize: 5496
Current children cumulated CPU time (s) 129.93
Current children cumulated vsize (Kb) 7620

[startup+140.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1325 0 0 0 13981 12 0 0 25 0 1 0 1842358475 5627904 1274 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1374 1274 145 145 0 1229 0
[pid=8779] vsize: 5496
Current children cumulated CPU time (s) 139.94
Current children cumulated vsize (Kb) 7620

[startup+150.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1325 0 0 0 14980 12 0 0 25 0 1 0 1842358475 5627904 1274 4294967295 134512640 135094434 3221224448 3221223072 134562146 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1374 1274 145 145 0 1229 0
[pid=8779] vsize: 5496
Current children cumulated CPU time (s) 149.93
Current children cumulated vsize (Kb) 7620

[startup+160.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1325 0 0 0 15980 13 0 0 25 0 1 0 1842358475 5627904 1274 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1374 1274 145 145 0 1229 0
[pid=8779] vsize: 5496
Current children cumulated CPU time (s) 159.94
Current children cumulated vsize (Kb) 7620

[startup+170.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1325 0 0 0 16979 13 0 0 25 0 1 0 1842358475 5627904 1274 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1374 1274 145 145 0 1229 0
[pid=8779] vsize: 5496
Current children cumulated CPU time (s) 169.93
Current children cumulated vsize (Kb) 7620

[startup+180.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1325 0 0 0 17979 14 0 0 25 0 1 0 1842358475 5627904 1274 4294967295 134512640 135094434 3221224448 3221223120 134555447 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1374 1274 145 145 0 1229 0
[pid=8779] vsize: 5496
Current children cumulated CPU time (s) 179.94
Current children cumulated vsize (Kb) 7620

[startup+190.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1325 0 0 0 18979 14 0 0 25 0 1 0 1842358475 5627904 1274 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1374 1274 145 145 0 1229 0
[pid=8779] vsize: 5496
Current children cumulated CPU time (s) 189.94
Current children cumulated vsize (Kb) 7620

[startup+200.023 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1331 0 0 0 19978 15 0 0 25 0 1 0 1842358475 5660672 1280 4294967295 134512640 135094434 3221224448 3221223104 134556043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1382 1280 145 145 0 1237 0
[pid=8779] vsize: 5528
Current children cumulated CPU time (s) 199.94
Current children cumulated vsize (Kb) 7652

[startup+210.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1331 0 0 0 20977 16 0 0 25 0 1 0 1842358475 5660672 1280 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1382 1280 145 145 0 1237 0
[pid=8779] vsize: 5528
Current children cumulated CPU time (s) 209.94
Current children cumulated vsize (Kb) 7652

[startup+220.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1342 0 0 0 21977 16 0 0 25 0 1 0 1842358475 5709824 1291 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1394 1291 145 145 0 1249 0
[pid=8779] vsize: 5576
Current children cumulated CPU time (s) 219.94
Current children cumulated vsize (Kb) 7700

[startup+230.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1342 0 0 0 22976 17 0 0 25 0 1 0 1842358475 5709824 1291 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1394 1291 145 145 0 1249 0
[pid=8779] vsize: 5576
Current children cumulated CPU time (s) 229.94
Current children cumulated vsize (Kb) 7700

[startup+240.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1342 0 0 0 23976 17 0 0 25 0 1 0 1842358475 5709824 1291 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1394 1291 145 145 0 1249 0
[pid=8779] vsize: 5576
Current children cumulated CPU time (s) 239.94
Current children cumulated vsize (Kb) 7700

[startup+250.028 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1342 0 0 0 24976 18 0 0 25 0 1 0 1842358475 5709824 1291 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1394 1291 145 145 0 1249 0
[pid=8779] vsize: 5576
Current children cumulated CPU time (s) 249.95
Current children cumulated vsize (Kb) 7700

[startup+260.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1346 0 0 0 25975 19 0 0 25 0 1 0 1842358475 5726208 1295 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1398 1295 145 145 0 1253 0
[pid=8779] vsize: 5592
Current children cumulated CPU time (s) 259.95
Current children cumulated vsize (Kb) 7716

[startup+270.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1390 0 0 0 26974 19 0 0 25 0 1 0 1842358475 5976064 1339 4294967295 134512640 135094434 3221224448 3221223136 134554793 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1459 1339 145 145 0 1314 0
[pid=8779] vsize: 5836
Current children cumulated CPU time (s) 269.94
Current children cumulated vsize (Kb) 7960

[startup+280.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1395 0 0 0 27974 20 0 0 25 0 1 0 1842358475 6008832 1344 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1467 1344 145 145 0 1322 0
[pid=8779] vsize: 5868
Current children cumulated CPU time (s) 279.95
Current children cumulated vsize (Kb) 7992

[startup+290.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1406 0 0 0 28974 20 0 0 25 0 1 0 1842358475 6074368 1355 4294967295 134512640 135094434 3221224448 3221223072 134562161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1483 1355 145 145 0 1338 0
[pid=8779] vsize: 5932
Current children cumulated CPU time (s) 289.95
Current children cumulated vsize (Kb) 8056

[startup+300.034 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1406 0 0 0 29974 20 0 0 25 0 1 0 1842358475 6074368 1355 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1483 1355 145 145 0 1338 0
[pid=8779] vsize: 5932
Current children cumulated CPU time (s) 299.95
Current children cumulated vsize (Kb) 8056

[startup+310.035 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1406 0 0 0 30974 21 0 0 25 0 1 0 1842358475 6074368 1355 4294967295 134512640 135094434 3221224448 3221223120 134555323 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1483 1355 145 145 0 1338 0
[pid=8779] vsize: 5932
Current children cumulated CPU time (s) 309.96
Current children cumulated vsize (Kb) 8056

[startup+320.035 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1411 0 0 0 31973 21 0 0 25 0 1 0 1842358475 6107136 1360 4294967295 134512640 135094434 3221224448 3221223072 134557658 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1491 1360 145 145 0 1346 0
[pid=8779] vsize: 5964
Current children cumulated CPU time (s) 319.95
Current children cumulated vsize (Kb) 8088

[startup+330.037 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1411 0 0 0 32973 21 0 0 25 0 1 0 1842358475 6107136 1360 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1491 1360 145 145 0 1346 0
[pid=8779] vsize: 5964
Current children cumulated CPU time (s) 329.95
Current children cumulated vsize (Kb) 8088

[startup+340.038 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1411 0 0 0 33973 22 0 0 25 0 1 0 1842358475 6107136 1360 4294967295 134512640 135094434 3221224448 3221222992 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1491 1360 145 145 0 1346 0
[pid=8779] vsize: 5964
Current children cumulated CPU time (s) 339.96
Current children cumulated vsize (Kb) 8088

[startup+350.039 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1414 0 0 0 34973 22 0 0 25 0 1 0 1842358475 6123520 1363 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1495 1363 145 145 0 1350 0
[pid=8779] vsize: 5980
Current children cumulated CPU time (s) 349.96
Current children cumulated vsize (Kb) 8104

[startup+360.041 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1414 0 0 0 35972 23 0 0 25 0 1 0 1842358475 6123520 1363 4294967295 134512640 135094434 3221224448 3221223072 134557585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1495 1363 145 145 0 1350 0
[pid=8779] vsize: 5980
Current children cumulated CPU time (s) 359.96
Current children cumulated vsize (Kb) 8104

[startup+370.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1414 0 0 0 36972 23 0 0 25 0 1 0 1842358475 6123520 1363 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1495 1363 145 145 0 1350 0
[pid=8779] vsize: 5980
Current children cumulated CPU time (s) 369.96
Current children cumulated vsize (Kb) 8104

[startup+380.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1414 0 0 0 37972 24 0 0 25 0 1 0 1842358475 6123520 1363 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1495 1363 145 145 0 1350 0
[pid=8779] vsize: 5980
Current children cumulated CPU time (s) 379.97
Current children cumulated vsize (Kb) 8104

[startup+390.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1415 0 0 0 38971 24 0 0 25 0 1 0 1842358475 6123520 1364 4294967295 134512640 135094434 3221224448 3221223120 134556434 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1495 1364 145 145 0 1350 0
[pid=8779] vsize: 5980
Current children cumulated CPU time (s) 389.96
Current children cumulated vsize (Kb) 8104

[startup+400.045 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1416 0 0 0 39971 24 0 0 25 0 1 0 1842358475 6123520 1365 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1495 1365 145 145 0 1350 0
[pid=8779] vsize: 5980
Current children cumulated CPU time (s) 399.96
Current children cumulated vsize (Kb) 8104

[startup+410.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1416 0 0 0 40971 25 0 0 25 0 1 0 1842358475 6123520 1365 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1495 1365 145 145 0 1350 0
[pid=8779] vsize: 5980
Current children cumulated CPU time (s) 409.97
Current children cumulated vsize (Kb) 8104

[startup+420.047 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1449 0 0 0 41970 26 0 0 25 0 1 0 1842358475 6254592 1398 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1527 1398 145 145 0 1382 0
[pid=8779] vsize: 6108
Current children cumulated CPU time (s) 419.97
Current children cumulated vsize (Kb) 8232

[startup+430.048 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1457 0 0 0 42969 26 0 0 25 0 1 0 1842358475 6303744 1406 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1539 1406 145 145 0 1394 0
[pid=8779] vsize: 6156
Current children cumulated CPU time (s) 429.96
Current children cumulated vsize (Kb) 8280

[startup+440.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1464 0 0 0 43969 26 0 0 25 0 1 0 1842358475 6320128 1413 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1543 1413 145 145 0 1398 0
[pid=8779] vsize: 6172
Current children cumulated CPU time (s) 439.96
Current children cumulated vsize (Kb) 8296

[startup+450.051 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1465 0 0 0 44969 27 0 0 25 0 1 0 1842358475 6320128 1414 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1543 1414 145 145 0 1398 0
[pid=8779] vsize: 6172
Current children cumulated CPU time (s) 449.97
Current children cumulated vsize (Kb) 8296

[startup+460.051 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1465 0 0 0 45969 27 0 0 25 0 1 0 1842358475 6320128 1414 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1543 1414 145 145 0 1398 0
[pid=8779] vsize: 6172
Current children cumulated CPU time (s) 459.97
Current children cumulated vsize (Kb) 8296

[startup+470.052 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1465 0 0 0 46969 27 0 0 25 0 1 0 1842358475 6320128 1414 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1543 1414 145 145 0 1398 0
[pid=8779] vsize: 6172
Current children cumulated CPU time (s) 469.97
Current children cumulated vsize (Kb) 8296

[startup+480.054 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1468 0 0 0 47969 28 0 0 25 0 1 0 1842358475 6320128 1417 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1543 1417 145 145 0 1398 0
[pid=8779] vsize: 6172
Current children cumulated CPU time (s) 479.98
Current children cumulated vsize (Kb) 8296

[startup+490.054 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1470 0 0 0 48968 28 0 0 25 0 1 0 1842358475 6340608 1419 4294967295 134512640 135094434 3221224448 3221223096 134558258 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1548 1419 145 145 0 1403 0
[pid=8779] vsize: 6192
Current children cumulated CPU time (s) 489.97
Current children cumulated vsize (Kb) 8316

[startup+500.056 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1473 0 0 0 49968 29 0 0 25 0 1 0 1842358475 6340608 1422 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1548 1422 145 145 0 1403 0
[pid=8779] vsize: 6192
Current children cumulated CPU time (s) 499.98
Current children cumulated vsize (Kb) 8316

[startup+510.057 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1479 0 0 0 50967 29 0 0 25 0 1 0 1842358475 6373376 1428 4294967295 134512640 135094434 3221224448 3221223040 134557028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1556 1428 145 145 0 1411 0
[pid=8779] vsize: 6224
Current children cumulated CPU time (s) 509.97
Current children cumulated vsize (Kb) 8348

[startup+520.058 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1479 0 0 0 51966 30 0 0 25 0 1 0 1842358475 6373376 1428 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1556 1428 145 145 0 1411 0
[pid=8779] vsize: 6224
Current children cumulated CPU time (s) 519.97
Current children cumulated vsize (Kb) 8348

[startup+530.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1479 0 0 0 52967 30 0 0 25 0 1 0 1842358475 6373376 1428 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1556 1428 145 145 0 1411 0
[pid=8779] vsize: 6224
Current children cumulated CPU time (s) 529.98
Current children cumulated vsize (Kb) 8348

[startup+540.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1479 0 0 0 53967 30 0 0 25 0 1 0 1842358475 6373376 1428 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1556 1428 145 145 0 1411 0
[pid=8779] vsize: 6224
Current children cumulated CPU time (s) 539.98
Current children cumulated vsize (Kb) 8348

[startup+550.061 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1479 0 0 0 54967 31 0 0 25 0 1 0 1842358475 6373376 1428 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1556 1428 145 145 0 1411 0
[pid=8779] vsize: 6224
Current children cumulated CPU time (s) 549.99
Current children cumulated vsize (Kb) 8348

[startup+560.062 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1479 0 0 0 55967 31 0 0 25 0 1 0 1842358475 6373376 1428 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1556 1428 145 145 0 1411 0
[pid=8779] vsize: 6224
Current children cumulated CPU time (s) 559.99
Current children cumulated vsize (Kb) 8348

[startup+570.062 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1479 0 0 0 56967 31 0 0 25 0 1 0 1842358475 6373376 1428 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1556 1428 145 145 0 1411 0
[pid=8779] vsize: 6224
Current children cumulated CPU time (s) 569.99
Current children cumulated vsize (Kb) 8348

[startup+580.063 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1479 0 0 0 57968 31 0 0 25 0 1 0 1842358475 6373376 1428 4294967295 134512640 135094434 3221224448 3221223120 134555583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1556 1428 145 145 0 1411 0
[pid=8779] vsize: 6224
Current children cumulated CPU time (s) 580
Current children cumulated vsize (Kb) 8348

[startup+590.064 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1479 0 0 0 58968 31 0 0 25 0 1 0 1842358475 6373376 1428 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1556 1428 145 145 0 1411 0
[pid=8779] vsize: 6224
Current children cumulated CPU time (s) 590
Current children cumulated vsize (Kb) 8348

[startup+600.065 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1479 0 0 0 59968 31 0 0 25 0 1 0 1842358475 6373376 1428 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1556 1428 145 145 0 1411 0
[pid=8779] vsize: 6224
Current children cumulated CPU time (s) 600
Current children cumulated vsize (Kb) 8348

[startup+610.066 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1479 0 0 0 60968 31 0 0 25 0 1 0 1842358475 6373376 1428 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1556 1428 145 145 0 1411 0
[pid=8779] vsize: 6224
Current children cumulated CPU time (s) 610
Current children cumulated vsize (Kb) 8348

[startup+620.067 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1550 0 0 0 61967 32 0 0 25 0 1 0 1842358475 6656000 1499 4294967295 134512640 135094434 3221224448 3221223136 134554726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1625 1499 145 145 0 1480 0
[pid=8779] vsize: 6500
Current children cumulated CPU time (s) 620
Current children cumulated vsize (Kb) 8624

[startup+630.067 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1550 0 0 0 62967 32 0 0 25 0 1 0 1842358475 6656000 1499 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1625 1499 145 145 0 1480 0
[pid=8779] vsize: 6500
Current children cumulated CPU time (s) 630
Current children cumulated vsize (Kb) 8624

[startup+640.068 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1550 0 0 0 63967 32 0 0 25 0 1 0 1842358475 6656000 1499 4294967295 134512640 135094434 3221224448 3221223120 134555556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1625 1499 145 145 0 1480 0
[pid=8779] vsize: 6500
Current children cumulated CPU time (s) 640
Current children cumulated vsize (Kb) 8624

[startup+650.068 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1556 0 0 0 64967 32 0 0 25 0 1 0 1842358475 6705152 1505 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1637 1505 145 145 0 1492 0
[pid=8779] vsize: 6548
Current children cumulated CPU time (s) 650
Current children cumulated vsize (Kb) 8672

[startup+660.069 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1557 0 0 0 65968 32 0 0 25 0 1 0 1842358475 6705152 1506 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1637 1506 145 145 0 1492 0
[pid=8779] vsize: 6548
Current children cumulated CPU time (s) 660.01
Current children cumulated vsize (Kb) 8672

[startup+670.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1559 0 0 0 66968 32 0 0 25 0 1 0 1842358475 6705152 1508 4294967295 134512640 135094434 3221224448 3221223104 134558398 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1637 1508 145 145 0 1492 0
[pid=8779] vsize: 6548
Current children cumulated CPU time (s) 670.01
Current children cumulated vsize (Kb) 8672

[startup+680.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1569 0 0 0 67968 32 0 0 25 0 1 0 1842358475 6770688 1518 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1653 1518 145 145 0 1508 0
[pid=8779] vsize: 6612
Current children cumulated CPU time (s) 680.01
Current children cumulated vsize (Kb) 8736

[startup+690.071 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1572 0 0 0 68968 32 0 0 25 0 1 0 1842358475 6782976 1521 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1656 1521 145 145 0 1511 0
[pid=8779] vsize: 6624
Current children cumulated CPU time (s) 690.01
Current children cumulated vsize (Kb) 8748

[startup+700.072 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1572 0 0 0 69968 32 0 0 25 0 1 0 1842358475 6782976 1521 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1656 1521 145 145 0 1511 0
[pid=8779] vsize: 6624
Current children cumulated CPU time (s) 700.01
Current children cumulated vsize (Kb) 8748

[startup+710.072 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1572 0 0 0 70969 32 0 0 25 0 1 0 1842358475 6782976 1521 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1656 1521 145 145 0 1511 0
[pid=8779] vsize: 6624
Current children cumulated CPU time (s) 710.02
Current children cumulated vsize (Kb) 8748

[startup+720.073 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1574 0 0 0 71969 32 0 0 25 0 1 0 1842358475 6782976 1523 4294967295 134512640 135094434 3221224448 3221223120 134555274 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1656 1523 145 145 0 1511 0
[pid=8779] vsize: 6624
Current children cumulated CPU time (s) 720.02
Current children cumulated vsize (Kb) 8748

[startup+730.073 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1581 0 0 0 72969 32 0 0 25 0 1 0 1842358475 6836224 1530 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1669 1530 145 145 0 1524 0
[pid=8779] vsize: 6676
Current children cumulated CPU time (s) 730.02
Current children cumulated vsize (Kb) 8800

[startup+740.074 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1581 0 0 0 73969 32 0 0 25 0 1 0 1842358475 6836224 1530 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1669 1530 145 145 0 1524 0
[pid=8779] vsize: 6676
Current children cumulated CPU time (s) 740.02
Current children cumulated vsize (Kb) 8800

[startup+750.076 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1581 0 0 0 74970 32 0 0 25 0 1 0 1842358475 6836224 1530 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1669 1530 145 145 0 1524 0
[pid=8779] vsize: 6676
Current children cumulated CPU time (s) 750.03
Current children cumulated vsize (Kb) 8800

[startup+760.076 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1581 0 0 0 75970 32 0 0 25 0 1 0 1842358475 6836224 1530 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1669 1530 145 145 0 1524 0
[pid=8779] vsize: 6676
Current children cumulated CPU time (s) 760.03
Current children cumulated vsize (Kb) 8800

[startup+770.077 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1590 0 0 0 76970 32 0 0 25 0 1 0 1842358475 6901760 1539 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1685 1539 145 145 0 1540 0
[pid=8779] vsize: 6740
Current children cumulated CPU time (s) 770.03
Current children cumulated vsize (Kb) 8864

[startup+780.078 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1591 0 0 0 77970 32 0 0 25 0 1 0 1842358475 6901760 1540 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1685 1540 145 145 0 1540 0
[pid=8779] vsize: 6740
Current children cumulated CPU time (s) 780.03
Current children cumulated vsize (Kb) 8864

[startup+790.078 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1601 0 0 0 78970 32 0 0 25 0 1 0 1842358475 6967296 1550 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1701 1550 145 145 0 1556 0
[pid=8779] vsize: 6804
Current children cumulated CPU time (s) 790.03
Current children cumulated vsize (Kb) 8928

[startup+800.079 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1601 0 0 0 79971 32 0 0 25 0 1 0 1842358475 6967296 1550 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1701 1550 145 145 0 1556 0
[pid=8779] vsize: 6804
Current children cumulated CPU time (s) 800.04
Current children cumulated vsize (Kb) 8928

[startup+810.081 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1601 0 0 0 80970 32 0 0 25 0 1 0 1842358475 6967296 1550 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1701 1550 145 145 0 1556 0
[pid=8779] vsize: 6804
Current children cumulated CPU time (s) 810.03
Current children cumulated vsize (Kb) 8928

[startup+820.081 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1610 0 0 0 81970 32 0 0 25 0 1 0 1842358475 7032832 1559 4294967295 134512640 135094434 3221224448 3221223084 134557639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1717 1559 145 145 0 1572 0
[pid=8779] vsize: 6868
Current children cumulated CPU time (s) 820.03
Current children cumulated vsize (Kb) 8992

[startup+830.083 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1610 0 0 0 82969 33 0 0 25 0 1 0 1842358475 7032832 1559 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1717 1559 145 145 0 1572 0
[pid=8779] vsize: 6868
Current children cumulated CPU time (s) 830.03
Current children cumulated vsize (Kb) 8992

[startup+840.084 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1620 0 0 0 83969 33 0 0 25 0 1 0 1842358475 7098368 1569 4294967295 134512640 135094434 3221224448 3221223040 134778881 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1733 1569 145 145 0 1588 0
[pid=8779] vsize: 6932
Current children cumulated CPU time (s) 840.03
Current children cumulated vsize (Kb) 9056

[startup+850.084 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1620 0 0 0 84970 33 0 0 25 0 1 0 1842358475 7098368 1569 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1733 1569 145 145 0 1588 0
[pid=8779] vsize: 6932
Current children cumulated CPU time (s) 850.04
Current children cumulated vsize (Kb) 9056

[startup+860.085 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1622 0 0 0 85970 33 0 0 25 0 1 0 1842358475 7098368 1571 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1733 1571 145 145 0 1588 0
[pid=8779] vsize: 6932
Current children cumulated CPU time (s) 860.04
Current children cumulated vsize (Kb) 9056

[startup+870.086 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1622 0 0 0 86970 33 0 0 25 0 1 0 1842358475 7098368 1571 4294967295 134512640 135094434 3221224448 3221223104 134558033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1733 1571 145 145 0 1588 0
[pid=8779] vsize: 6932
Current children cumulated CPU time (s) 870.04
Current children cumulated vsize (Kb) 9056

[startup+880.086 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1631 0 0 0 87970 33 0 0 25 0 1 0 1842358475 7163904 1580 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1749 1580 145 145 0 1604 0
[pid=8779] vsize: 6996
Current children cumulated CPU time (s) 880.04
Current children cumulated vsize (Kb) 9120

[startup+890.087 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1631 0 0 0 88970 33 0 0 25 0 1 0 1842358475 7163904 1580 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1749 1580 145 145 0 1604 0
[pid=8779] vsize: 6996
Current children cumulated CPU time (s) 890.04
Current children cumulated vsize (Kb) 9120

[startup+900.087 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1631 0 0 0 89970 33 0 0 25 0 1 0 1842358475 7163904 1580 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1749 1580 145 145 0 1604 0
[pid=8779] vsize: 6996
Current children cumulated CPU time (s) 900.04
Current children cumulated vsize (Kb) 9120

[startup+910.088 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1632 0 0 0 90971 33 0 0 25 0 1 0 1842358475 7163904 1581 4294967295 134512640 135094434 3221224448 3221223072 134562110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1749 1581 145 145 0 1604 0
[pid=8779] vsize: 6996
Current children cumulated CPU time (s) 910.05
Current children cumulated vsize (Kb) 9120

[startup+920.089 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1632 0 0 0 91971 33 0 0 25 0 1 0 1842358475 7163904 1581 4294967295 134512640 135094434 3221224448 3221223120 134555315 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1749 1581 145 145 0 1604 0
[pid=8779] vsize: 6996
Current children cumulated CPU time (s) 920.05
Current children cumulated vsize (Kb) 9120

[startup+930.089 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1632 0 0 0 92971 33 0 0 25 0 1 0 1842358475 7163904 1581 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1749 1581 145 145 0 1604 0
[pid=8779] vsize: 6996
Current children cumulated CPU time (s) 930.05
Current children cumulated vsize (Kb) 9120

[startup+940.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1632 0 0 0 93971 34 0 0 25 0 1 0 1842358475 7163904 1581 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8779/statm): 1749 1581 145 145 0 1604 0
[pid=8779] vsize: 6996
Current children cumulated CPU time (s) 940.06
Current children cumulated vsize (Kb) 9120

[startup+950.092 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1645 0 0 0 94970 34 0 0 25 0 1 0 1842358475 7208960 1594 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1760 1594 145 145 0 1615 0
[pid=8779] vsize: 7040
Current children cumulated CPU time (s) 950.05
Current children cumulated vsize (Kb) 9164

[startup+960.092 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1653 0 0 0 95970 34 0 0 25 0 1 0 1842358475 7241728 1602 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1768 1602 145 145 0 1623 0
[pid=8779] vsize: 7072
Current children cumulated CPU time (s) 960.05
Current children cumulated vsize (Kb) 9196

[startup+970.093 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1664 0 0 0 96971 34 0 0 25 0 1 0 1842358475 7307264 1613 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1784 1613 145 145 0 1639 0
[pid=8779] vsize: 7136
Current children cumulated CPU time (s) 970.06
Current children cumulated vsize (Kb) 9260

[startup+980.093 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1664 0 0 0 97971 34 0 0 25 0 1 0 1842358475 7307264 1613 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1784 1613 145 145 0 1639 0
[pid=8779] vsize: 7136
Current children cumulated CPU time (s) 980.06
Current children cumulated vsize (Kb) 9260

[startup+990.094 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1664 0 0 0 98971 34 0 0 25 0 1 0 1842358475 7307264 1613 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1784 1613 145 145 0 1639 0
[pid=8779] vsize: 7136
Current children cumulated CPU time (s) 990.06
Current children cumulated vsize (Kb) 9260

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1664 0 0 0 99971 34 0 0 25 0 1 0 1842358475 7307264 1613 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1784 1613 145 145 0 1639 0
[pid=8779] vsize: 7136
Current children cumulated CPU time (s) 1000.06
Current children cumulated vsize (Kb) 9260

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1671 0 0 0 100971 34 0 0 25 0 1 0 1842358475 7340032 1620 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1792 1620 145 145 0 1647 0
[pid=8779] vsize: 7168
Current children cumulated CPU time (s) 1010.06
Current children cumulated vsize (Kb) 9292

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1676 0 0 0 101972 34 0 0 25 0 1 0 1842358475 7405568 1625 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1808 1625 145 145 0 1663 0
[pid=8779] vsize: 7232
Current children cumulated CPU time (s) 1020.07
Current children cumulated vsize (Kb) 9356

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1676 0 0 0 102972 34 0 0 25 0 1 0 1842358475 7405568 1625 4294967295 134512640 135094434 3221224448 3221223104 134558392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1808 1625 145 145 0 1663 0
[pid=8779] vsize: 7232
Current children cumulated CPU time (s) 1030.07
Current children cumulated vsize (Kb) 9356

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1676 0 0 0 103972 34 0 0 25 0 1 0 1842358475 7405568 1625 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1808 1625 145 145 0 1663 0
[pid=8779] vsize: 7232
Current children cumulated CPU time (s) 1040.07
Current children cumulated vsize (Kb) 9356

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1684 0 0 0 104972 34 0 0 25 0 1 0 1842358475 7438336 1633 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1816 1633 145 145 0 1671 0
[pid=8779] vsize: 7264
Current children cumulated CPU time (s) 1050.07
Current children cumulated vsize (Kb) 9388

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1684 0 0 0 105973 34 0 0 25 0 1 0 1842358475 7438336 1633 4294967295 134512640 135094434 3221224448 3221223104 134558232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1816 1633 145 145 0 1671 0
[pid=8779] vsize: 7264
Current children cumulated CPU time (s) 1060.08
Current children cumulated vsize (Kb) 9388

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1684 0 0 0 106973 34 0 0 25 0 1 0 1842358475 7438336 1633 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1816 1633 145 145 0 1671 0
[pid=8779] vsize: 7264
Current children cumulated CPU time (s) 1070.08
Current children cumulated vsize (Kb) 9388

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1684 0 0 0 107973 34 0 0 25 0 1 0 1842358475 7438336 1633 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1816 1633 145 145 0 1671 0
[pid=8779] vsize: 7264
Current children cumulated CPU time (s) 1080.08
Current children cumulated vsize (Kb) 9388

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1686 0 0 0 108973 34 0 0 25 0 1 0 1842358475 7438336 1635 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1816 1635 145 145 0 1671 0
[pid=8779] vsize: 7264
Current children cumulated CPU time (s) 1090.08
Current children cumulated vsize (Kb) 9388

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1687 0 0 0 109974 34 0 0 25 0 1 0 1842358475 7438336 1636 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1816 1636 145 145 0 1671 0
[pid=8779] vsize: 7264
Current children cumulated CPU time (s) 1100.09
Current children cumulated vsize (Kb) 9388

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1698 0 0 0 110974 34 0 0 25 0 1 0 1842358475 7503872 1647 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1832 1647 145 145 0 1687 0
[pid=8779] vsize: 7328
Current children cumulated CPU time (s) 1110.09
Current children cumulated vsize (Kb) 9452

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1698 0 0 0 111974 34 0 0 25 0 1 0 1842358475 7503872 1647 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1832 1647 145 145 0 1687 0
[pid=8779] vsize: 7328
Current children cumulated CPU time (s) 1120.09
Current children cumulated vsize (Kb) 9452

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1698 0 0 0 112974 34 0 0 25 0 1 0 1842358475 7503872 1647 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1832 1647 145 145 0 1687 0
[pid=8779] vsize: 7328
Current children cumulated CPU time (s) 1130.09
Current children cumulated vsize (Kb) 9452

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1698 0 0 0 113974 34 0 0 25 0 1 0 1842358475 7503872 1647 4294967295 134512640 135094434 3221224448 3221223120 134555288 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1832 1647 145 145 0 1687 0
[pid=8779] vsize: 7328
Current children cumulated CPU time (s) 1140.09
Current children cumulated vsize (Kb) 9452

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1698 0 0 0 114975 35 0 0 25 0 1 0 1842358475 7503872 1647 4294967295 134512640 135094434 3221224448 3221223120 134555457 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1832 1647 145 145 0 1687 0
[pid=8779] vsize: 7328
Current children cumulated CPU time (s) 1150.11
Current children cumulated vsize (Kb) 9452

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1698 0 0 0 115975 35 0 0 25 0 1 0 1842358475 7503872 1647 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1832 1647 145 145 0 1687 0
[pid=8779] vsize: 7328
Current children cumulated CPU time (s) 1160.11
Current children cumulated vsize (Kb) 9452

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1698 0 0 0 116975 35 0 0 25 0 1 0 1842358475 7503872 1647 4294967295 134512640 135094434 3221224448 3221223072 134557705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1832 1647 145 145 0 1687 0
[pid=8779] vsize: 7328
Current children cumulated CPU time (s) 1170.11
Current children cumulated vsize (Kb) 9452

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1698 0 0 0 117975 35 0 0 25 0 1 0 1842358475 7503872 1647 4294967295 134512640 135094434 3221224448 3221223104 134558292 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1832 1647 145 145 0 1687 0
[pid=8779] vsize: 7328
Current children cumulated CPU time (s) 1180.11
Current children cumulated vsize (Kb) 9452

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1698 0 0 0 118975 35 0 0 25 0 1 0 1842358475 7503872 1647 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1832 1647 145 145 0 1687 0
[pid=8779] vsize: 7328
Current children cumulated CPU time (s) 1190.11
Current children cumulated vsize (Kb) 9452

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1698 0 0 0 119975 35 0 0 25 0 1 0 1842358475 7503872 1647 4294967295 134512640 135094434 3221224448 3221223072 134557598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1832 1647 145 145 0 1687 0
[pid=8779] vsize: 7328
Current children cumulated CPU time (s) 1200.11
Current children cumulated vsize (Kb) 9452



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 8779
Raw data (/proc/8775/stat): 8775 (minisat+_script) S 8774 8775 5299 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842358470 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8775/statm): 531 226 485 147 0 384 0
[pid=8775] vsize: 2124
Raw data (/proc/8779/stat): 8779 (minisat+_64-bit) R 8775 8775 5299 0 -1 0 1698 0 0 0 119975 35 0 0 25 0 1 0 1842358475 7503872 1647 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8779/statm): 1832 1647 145 145 0 1687 0
[pid=8779] vsize: 7328
Current children cumulated CPU time (s) 1200.11
Current children cumulated vsize (Kb) 9452

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

Child status: 0
Real time (s): 1200.12
CPU time (s): 1200.12
CPU user time (s): 1199.76
CPU system time (s): 0.361944
CPU usage (%): 99.9999
Max. virtual memory (cumulated for all children) (Kb): 9452

Verifier Data

ERROR: no interpretation found !