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/aloul/FPGA_SAT05/normalized-chnl20_25_pb.cnf.cr.opb
MD5SUM6c328ef6f9d8d5a179eec9bf3550b7fd
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 26
Number of bits of the biggest sum of numbers5
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.028994
Number of variables1000
Total number of constraints90
Number of constraints which are clauses50
Number of constraints which are cardinality constraints (but not clauses)40
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint20
Maximum length of a constraint25

Trace number 810

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        932420 kB
Buffers:         36744 kB
Cached:          35364 kB
SwapCached:        788 kB
Active:          53652 kB
Inactive:        21048 kB
HighTotal:      131008 kB
HighFree:        94920 kB
LowTotal:       903652 kB
LowFree:        837500 kB
SwapTotal:     2097892 kB
SwapFree:      2096636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5732 kB
Slab:            21900 kB
Committed_AS:    64136 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 12:44:05 (client local time) WITH STATUS 0 IN 1209.65 SECONDS
stats: 2351 7 1209.65 0

Solver Data

c Parsing PB file...
c Converting 90 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................
c ---[  39]---> BDD-cost:   47
c ---[  38]---> BDD-cost:   47
c ---[  37]---> BDD-cost:   47
c ---[  36]---> BDD-cost:   47
c ---[  35]---> BDD-cost:   47
c ---[  34]---> BDD-cost:   47
c ---[  33]---> BDD-cost:   47
c ---[  32]---> BDD-cost:   47
c ---[  31]---> BDD-cost:   47
c ---[  30]---> BDD-cost:   47
c ---[  29]---> BDD-cost:   47
c ---[  28]---> BDD-cost:   47
c ---[  27]---> BDD-cost:   47
c ---[  26]---> BDD-cost:   47
c ---[  25]---> BDD-cost:   47
c ---[  24]---> BDD-cost:   47
c ---[  23]---> BDD-cost:   47
c ---[  22]---> BDD-cost:   47
c ---[  21]---> BDD-cost:   47
c ---[  20]---> BDD-cost:   47
c ---[  19]---> BDD-cost:   47
c ---[  18]---> BDD-cost:   47
c ---[  17]---> BDD-cost:   47
c ---[  16]---> BDD-cost:   47
c ---[  15]---> BDD-cost:   47
c ---[  14]---> BDD-cost:   47
c ---[  13]---> BDD-cost:   47
c ---[  12]---> BDD-cost:   47
c ---[  11]---> BDD-cost:   47
c ---[  10]---> BDD-cost:   47
c ---[   9]---> BDD-cost:   47
c ---[   8]---> BDD-cost:   47
c ---[   7]---> BDD-cost:   47
c ---[   6]---> BDD-cost:   47
c ---[   5]---> BDD-cost:   47
c ---[   4]---> BDD-cost:   47
c ---[   3]---> BDD-cost:   47
c ---[   2]---> BDD-cost:   47
c ---[   1]---> BDD-cost:   47
c ---[   0]---> BDD-cost:   47
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    4690    13080 |    1563       0        0     nan |  0.000 % |
c |       100 |    4690    13080 |    1719     100     6902    69.0 |  1.389 % |
c |       251 |    4690    13080 |    1891     251    20396    81.3 |  1.389 % |
c |       478 |    4690    13080 |    2080     478    46287    96.8 |  1.389 % |
c |       821 |    4690    13080 |    2288     821    81704    99.5 |  1.389 % |
c |      1327 |    4690    13080 |    2517    1327   146172   110.2 |  1.389 % |
c |      2087 |    4690    13080 |    2768    2087   249403   119.5 |  1.389 % |
c |      3227 |    4690    13080 |    3045    3227   373256   115.7 |  1.389 % |
c |      4936 |    4690    13080 |    3350    3323   444218   133.7 |  1.389 % |
c |      7498 |    4690    13080 |    3685    3680   506490   137.6 |  1.389 % |
c |     11342 |    4690    13080 |    4054    2775   386580   139.3 |  1.389 % |
c |     17109 |    4690    13080 |    4459    3425   492300   143.7 |  1.389 % |
c |     25762 |    4690    13080 |    4905    3891   549706   141.3 |  1.389 % |
c |     38739 |    4690    13080 |    5395    5144  1059065   205.9 |  1.389 % |
c |     58201 |    4690    13080 |    5935    3757   878997   234.0 |  1.389 % |
c |     87393 |    4690    13080 |    6529    3337   680756   204.0 |  1.389 % |
c |    131182 |    4690    13080 |    7181    4075   849512   208.5 |  1.389 % |
c |    196867 |    4690    13080 |    7900    6042   961736   159.2 |  1.389 % |
c |    295397 |    4690    13080 |    8690    8012  1389547   173.4 |  1.389 % |
c |    443187 |    4690    13080 |    9559    4859  1092280   224.8 |  1.389 % |
c |    664873 |    4690    13080 |   10515    6850  1659355   242.2 |  1.389 % |

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/8655/stat): 8655 (minisat+_script) R 8654 8655 5245 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841216431 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/8655/statm): 174 3 169 147 0 27 0
[pid=8655] 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=8656
New process pid=8657
New process pid=8658
execve syscall for /bin/sed executable
One traced child (pid=8657) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=8658) exited with status: 0
One traced child (pid=8656) exited with status: 0
New process pid=8659
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc30/normalized-chnl20_25_pb.cnf.cr.opb

[startup+10.0058 s]
Raw data (loadavg): 0.60 0.87 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 1144 0 2 0 977 6 0 0 25 0 1 0 1841216437 4980736 1133 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 1216 1133 145 145 0 1071 0
[pid=8659] vsize: 4864
Current children cumulated CPU time (s) 9.84
Current children cumulated vsize (Kb) 6988

[startup+20.0066 s]
Raw data (loadavg): 0.66 0.87 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 1392 0 2 0 1973 8 0 0 25 0 1 0 1841216437 5996544 1381 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8659/statm): 1464 1381 145 145 0 1319 0
[pid=8659] vsize: 5856
Current children cumulated CPU time (s) 19.82
Current children cumulated vsize (Kb) 7980

[startup+30.0084 s]
Raw data (loadavg): 0.71 0.87 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 1580 0 2 0 2969 10 0 0 25 0 1 0 1841216437 6782976 1569 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8659/statm): 1656 1569 145 145 0 1511 0
[pid=8659] vsize: 6624
Current children cumulated CPU time (s) 29.8
Current children cumulated vsize (Kb) 8748

[startup+40.0092 s]
Raw data (loadavg): 0.75 0.88 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 2147 0 2 0 3962 13 0 0 25 0 1 0 1841216437 9117696 2136 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8659/statm): 2226 2136 145 145 0 2081 0
[pid=8659] vsize: 8904
Current children cumulated CPU time (s) 39.76
Current children cumulated vsize (Kb) 11028

[startup+50.01 s]
Raw data (loadavg): 0.79 0.88 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 2261 0 2 0 4961 13 0 0 25 0 1 0 1841216437 9584640 2250 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 2340 2250 145 145 0 2195 0
[pid=8659] vsize: 9360
Current children cumulated CPU time (s) 49.75
Current children cumulated vsize (Kb) 11484

[startup+60.0108 s]
Raw data (loadavg): 0.82 0.88 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 2261 0 2 0 5961 13 0 0 25 0 1 0 1841216437 9584640 2250 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8659/statm): 2340 2250 145 145 0 2195 0
[pid=8659] vsize: 9360
Current children cumulated CPU time (s) 59.75
Current children cumulated vsize (Kb) 11484

[startup+70.0116 s]
Raw data (loadavg): 0.85 0.89 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 2425 0 2 0 6959 14 0 0 25 0 1 0 1841216437 10256384 2414 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 2504 2414 145 145 0 2359 0
[pid=8659] vsize: 10016
Current children cumulated CPU time (s) 69.74
Current children cumulated vsize (Kb) 12140

[startup+80.0124 s]
Raw data (loadavg): 0.87 0.89 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 2425 0 2 0 7959 14 0 0 25 0 1 0 1841216437 10256384 2414 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 2504 2414 145 145 0 2359 0
[pid=8659] vsize: 10016
Current children cumulated CPU time (s) 79.74
Current children cumulated vsize (Kb) 12140

[startup+90.0132 s]
Raw data (loadavg): 0.89 0.89 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 2433 0 2 0 8959 14 0 0 25 0 1 0 1841216437 10289152 2422 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 2512 2422 145 145 0 2367 0
[pid=8659] vsize: 10048
Current children cumulated CPU time (s) 89.74
Current children cumulated vsize (Kb) 12172

[startup+100.013 s]
Raw data (loadavg): 0.91 0.90 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 2546 0 2 0 9957 15 0 0 25 0 1 0 1841216437 10747904 2535 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8659/statm): 2624 2535 145 145 0 2479 0
[pid=8659] vsize: 10496
Current children cumulated CPU time (s) 99.73
Current children cumulated vsize (Kb) 12620

[startup+110.015 s]
Raw data (loadavg): 0.92 0.90 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 2588 0 2 0 10956 16 0 0 25 0 1 0 1841216437 10919936 2577 4294967295 134512640 135094434 3221224432 3221223024 134556847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8659/statm): 2666 2577 145 145 0 2521 0
[pid=8659] vsize: 10664
Current children cumulated CPU time (s) 109.73
Current children cumulated vsize (Kb) 12788

[startup+120.016 s]
Raw data (loadavg): 0.93 0.90 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 2637 0 2 0 11955 17 0 0 25 0 1 0 1841216437 11124736 2626 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8659/statm): 2716 2626 145 145 0 2571 0
[pid=8659] vsize: 10864
Current children cumulated CPU time (s) 119.73
Current children cumulated vsize (Kb) 12988

[startup+130.016 s]
Raw data (loadavg): 0.94 0.90 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 2873 0 2 0 12950 19 0 0 25 0 1 0 1841216437 12095488 2862 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8659/statm): 2953 2862 145 145 0 2808 0
[pid=8659] vsize: 11812
Current children cumulated CPU time (s) 129.7
Current children cumulated vsize (Kb) 13936

[startup+140.017 s]
Raw data (loadavg): 0.95 0.91 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 2873 0 2 0 13950 19 0 0 25 0 1 0 1841216437 12095488 2862 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8659/statm): 2953 2862 145 145 0 2808 0
[pid=8659] vsize: 11812
Current children cumulated CPU time (s) 139.7
Current children cumulated vsize (Kb) 13936

[startup+150.018 s]
Raw data (loadavg): 0.96 0.91 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 2873 0 2 0 14950 19 0 0 25 0 1 0 1841216437 12095488 2862 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8659/statm): 2953 2862 145 145 0 2808 0
[pid=8659] vsize: 11812
Current children cumulated CPU time (s) 149.7
Current children cumulated vsize (Kb) 13936

[startup+160.019 s]
Raw data (loadavg): 0.96 0.91 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 2873 0 2 0 15949 19 0 0 25 0 1 0 1841216437 12095488 2862 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8659/statm): 2953 2862 145 145 0 2808 0
[pid=8659] vsize: 11812
Current children cumulated CPU time (s) 159.69
Current children cumulated vsize (Kb) 13936

[startup+170.02 s]
Raw data (loadavg): 0.97 0.91 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 2873 0 2 0 16949 20 0 0 25 0 1 0 1841216437 12095488 2862 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8659/statm): 2953 2862 145 145 0 2808 0
[pid=8659] vsize: 11812
Current children cumulated CPU time (s) 169.7
Current children cumulated vsize (Kb) 13936

[startup+180.021 s]
Raw data (loadavg): 0.97 0.92 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 2873 0 2 0 17949 20 0 0 25 0 1 0 1841216437 12095488 2862 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8659/statm): 2953 2862 145 145 0 2808 0
[pid=8659] vsize: 11812
Current children cumulated CPU time (s) 179.7
Current children cumulated vsize (Kb) 13936

[startup+190.022 s]
Raw data (loadavg): 0.98 0.92 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 2874 0 2 0 18948 20 0 0 25 0 1 0 1841216437 11882496 2811 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8659/statm): 2901 2811 145 145 0 2756 0
[pid=8659] vsize: 11604
Current children cumulated CPU time (s) 189.69
Current children cumulated vsize (Kb) 13728

[startup+200.023 s]
Raw data (loadavg): 0.98 0.92 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 2874 0 2 0 19948 21 0 0 25 0 1 0 1841216437 11882496 2811 4294967295 134512640 135094434 3221224432 3221223088 134557823 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8659/statm): 2901 2811 145 145 0 2756 0
[pid=8659] vsize: 11604
Current children cumulated CPU time (s) 199.7
Current children cumulated vsize (Kb) 13728

[startup+210.025 s]
Raw data (loadavg): 0.98 0.92 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 2874 0 2 0 20948 21 0 0 25 0 1 0 1841216437 11882496 2811 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8659/statm): 2901 2811 145 145 0 2756 0
[pid=8659] vsize: 11604
Current children cumulated CPU time (s) 209.7
Current children cumulated vsize (Kb) 13728

[startup+220.026 s]
Raw data (loadavg): 0.98 0.92 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 2874 0 2 0 21948 21 0 0 25 0 1 0 1841216437 11882496 2811 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8659/statm): 2901 2811 145 145 0 2756 0
[pid=8659] vsize: 11604
Current children cumulated CPU time (s) 219.7
Current children cumulated vsize (Kb) 13728

[startup+230.027 s]
Raw data (loadavg): 0.99 0.93 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 2874 0 2 0 22948 21 0 0 25 0 1 0 1841216437 11882496 2811 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 2901 2811 145 145 0 2756 0
[pid=8659] vsize: 11604
Current children cumulated CPU time (s) 229.7
Current children cumulated vsize (Kb) 13728

[startup+240.028 s]
Raw data (loadavg): 0.99 0.93 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 2879 0 2 0 23948 21 0 0 25 0 1 0 1841216437 11911168 2816 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 2908 2816 145 145 0 2763 0
[pid=8659] vsize: 11632
Current children cumulated CPU time (s) 239.7
Current children cumulated vsize (Kb) 13756

[startup+250.028 s]
Raw data (loadavg): 0.99 0.93 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 2889 0 2 0 24948 21 0 0 25 0 1 0 1841216437 11976704 2826 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 2924 2826 145 145 0 2779 0
[pid=8659] vsize: 11696
Current children cumulated CPU time (s) 249.7
Current children cumulated vsize (Kb) 13820

[startup+260.029 s]
Raw data (loadavg): 0.99 0.93 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 3079 0 2 0 25946 22 0 0 25 0 1 0 1841216437 12754944 3016 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 3114 3016 145 145 0 2969 0
[pid=8659] vsize: 12456
Current children cumulated CPU time (s) 259.69
Current children cumulated vsize (Kb) 14580

[startup+270.029 s]
Raw data (loadavg): 0.99 0.93 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 3106 0 2 0 26945 23 0 0 25 0 1 0 1841216437 12902400 3043 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 3150 3043 145 145 0 3005 0
[pid=8659] vsize: 12600
Current children cumulated CPU time (s) 269.69
Current children cumulated vsize (Kb) 14724

[startup+280.03 s]
Raw data (loadavg): 0.99 0.94 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 3106 0 2 0 27945 23 0 0 25 0 1 0 1841216437 12902400 3043 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 3150 3043 145 145 0 3005 0
[pid=8659] vsize: 12600
Current children cumulated CPU time (s) 279.69
Current children cumulated vsize (Kb) 14724

[startup+290.031 s]
Raw data (loadavg): 0.99 0.94 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 3116 0 2 0 28945 23 0 0 25 0 1 0 1841216437 12939264 3053 4294967295 134512640 135094434 3221224432 3221223024 134551925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 3159 3053 145 145 0 3014 0
[pid=8659] vsize: 12636
Current children cumulated CPU time (s) 289.69
Current children cumulated vsize (Kb) 14760

[startup+300.032 s]
Raw data (loadavg): 0.99 0.94 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 3139 0 2 0 29945 23 0 0 25 0 1 0 1841216437 13070336 3076 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 3191 3076 145 145 0 3046 0
[pid=8659] vsize: 12764
Current children cumulated CPU time (s) 299.69
Current children cumulated vsize (Kb) 14888

[startup+310.033 s]
Raw data (loadavg): 0.99 0.94 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 3483 0 2 0 30940 26 0 0 25 0 1 0 1841216437 14487552 3420 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 3537 3420 145 145 0 3392 0
[pid=8659] vsize: 14148
Current children cumulated CPU time (s) 309.67
Current children cumulated vsize (Kb) 16272

[startup+320.034 s]
Raw data (loadavg): 0.99 0.94 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 3613 0 2 0 31938 27 0 0 25 0 1 0 1841216437 15032320 3550 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 3670 3550 145 145 0 3525 0
[pid=8659] vsize: 14680
Current children cumulated CPU time (s) 319.66
Current children cumulated vsize (Kb) 16804

[startup+330.034 s]
Raw data (loadavg): 0.99 0.94 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 3613 0 2 0 32938 27 0 0 25 0 1 0 1841216437 15032320 3550 4294967295 134512640 135094434 3221224432 3221223104 134555855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 3670 3550 145 145 0 3525 0
[pid=8659] vsize: 14680
Current children cumulated CPU time (s) 329.66
Current children cumulated vsize (Kb) 16804

[startup+340.035 s]
Raw data (loadavg): 0.99 0.94 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 3613 0 2 0 33938 27 0 0 25 0 1 0 1841216437 15032320 3550 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 3670 3550 145 145 0 3525 0
[pid=8659] vsize: 14680
Current children cumulated CPU time (s) 339.66
Current children cumulated vsize (Kb) 16804

[startup+350.035 s]
Raw data (loadavg): 0.99 0.95 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 3613 0 2 0 34939 27 0 0 25 0 1 0 1841216437 15032320 3550 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 3670 3550 145 145 0 3525 0
[pid=8659] vsize: 14680
Current children cumulated CPU time (s) 349.67
Current children cumulated vsize (Kb) 16804

[startup+360.036 s]
Raw data (loadavg): 0.99 0.95 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 3613 0 2 0 35939 27 0 0 25 0 1 0 1841216437 15032320 3550 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 3670 3550 145 145 0 3525 0
[pid=8659] vsize: 14680
Current children cumulated CPU time (s) 359.67
Current children cumulated vsize (Kb) 16804

[startup+370.036 s]
Raw data (loadavg): 0.99 0.95 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 3613 0 2 0 36939 27 0 0 25 0 1 0 1841216437 15032320 3550 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 3670 3550 145 145 0 3525 0
[pid=8659] vsize: 14680
Current children cumulated CPU time (s) 369.67
Current children cumulated vsize (Kb) 16804

[startup+380.037 s]
Raw data (loadavg): 0.99 0.95 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 3613 0 2 0 37939 27 0 0 25 0 1 0 1841216437 15032320 3550 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 3670 3550 145 145 0 3525 0
[pid=8659] vsize: 14680
Current children cumulated CPU time (s) 379.67
Current children cumulated vsize (Kb) 16804

[startup+390.038 s]
Raw data (loadavg): 0.99 0.95 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 3615 0 2 0 38939 27 0 0 25 0 1 0 1841216437 15032320 3552 4294967295 134512640 135094434 3221224432 3221223024 134557297 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 3670 3552 145 145 0 3525 0
[pid=8659] vsize: 14680
Current children cumulated CPU time (s) 389.67
Current children cumulated vsize (Kb) 16804

[startup+400.039 s]
Raw data (loadavg): 0.99 0.95 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 3615 0 2 0 39939 27 0 0 25 0 1 0 1841216437 15032320 3552 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 3670 3552 145 145 0 3525 0
[pid=8659] vsize: 14680
Current children cumulated CPU time (s) 399.67
Current children cumulated vsize (Kb) 16804

[startup+410.04 s]
Raw data (loadavg): 0.99 0.95 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 3666 0 2 0 40939 27 0 0 25 0 1 0 1841216437 15249408 3603 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 3723 3603 145 145 0 3578 0
[pid=8659] vsize: 14892
Current children cumulated CPU time (s) 409.67
Current children cumulated vsize (Kb) 17016

[startup+420.04 s]
Raw data (loadavg): 0.99 0.95 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 3796 0 2 0 41937 28 0 0 25 0 1 0 1841216437 15781888 3733 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 3853 3733 145 145 0 3708 0
[pid=8659] vsize: 15412
Current children cumulated CPU time (s) 419.66
Current children cumulated vsize (Kb) 17536

[startup+430.041 s]
Raw data (loadavg): 0.99 0.95 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4137 0 2 0 42932 31 0 0 25 0 1 0 1841216437 17186816 4074 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4196 4074 145 145 0 4051 0
[pid=8659] vsize: 16784
Current children cumulated CPU time (s) 429.64
Current children cumulated vsize (Kb) 18908

[startup+440.042 s]
Raw data (loadavg): 0.99 0.95 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4231 0 2 0 43931 31 0 0 25 0 1 0 1841216437 17575936 4168 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4291 4168 145 145 0 4146 0
[pid=8659] vsize: 17164
Current children cumulated CPU time (s) 439.63
Current children cumulated vsize (Kb) 19288

[startup+450.043 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4255 0 2 0 44931 31 0 0 25 0 1 0 1841216437 17674240 4192 4294967295 134512640 135094434 3221224432 3221223024 134551890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4315 4192 145 145 0 4170 0
[pid=8659] vsize: 17260
Current children cumulated CPU time (s) 449.63
Current children cumulated vsize (Kb) 19384

[startup+460.044 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4256 0 2 0 45931 31 0 0 25 0 1 0 1841216437 17674240 4193 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4315 4193 145 145 0 4170 0
[pid=8659] vsize: 17260
Current children cumulated CPU time (s) 459.63
Current children cumulated vsize (Kb) 19384

[startup+470.044 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4334 0 2 0 46931 32 0 0 25 0 1 0 1841216437 18018304 4271 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4399 4271 145 145 0 4254 0
[pid=8659] vsize: 17596
Current children cumulated CPU time (s) 469.64
Current children cumulated vsize (Kb) 19720

[startup+480.046 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4348 0 2 0 47931 32 0 0 25 0 1 0 1841216437 18075648 4285 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4413 4285 145 145 0 4268 0
[pid=8659] vsize: 17652
Current children cumulated CPU time (s) 479.64
Current children cumulated vsize (Kb) 19776

[startup+490.047 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4350 0 2 0 48931 32 0 0 25 0 1 0 1841216437 18083840 4287 4294967295 134512640 135094434 3221224432 3221223024 134551463 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4415 4287 145 145 0 4270 0
[pid=8659] vsize: 17660
Current children cumulated CPU time (s) 489.64
Current children cumulated vsize (Kb) 19784

[startup+500.047 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4350 0 2 0 49931 32 0 0 25 0 1 0 1841216437 18083840 4287 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4415 4287 145 145 0 4270 0
[pid=8659] vsize: 17660
Current children cumulated CPU time (s) 499.64
Current children cumulated vsize (Kb) 19784

[startup+510.049 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4365 0 2 0 50931 32 0 0 25 0 1 0 1841216437 18161664 4302 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4434 4302 145 145 0 4289 0
[pid=8659] vsize: 17736
Current children cumulated CPU time (s) 509.64
Current children cumulated vsize (Kb) 19860

[startup+520.049 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4539 0 2 0 51929 33 0 0 25 0 1 0 1841216437 18874368 4476 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4608 4476 145 145 0 4463 0
[pid=8659] vsize: 18432
Current children cumulated CPU time (s) 519.63
Current children cumulated vsize (Kb) 20556

[startup+530.049 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4539 0 2 0 52927 35 0 0 25 0 1 0 1841216437 18874368 4476 4294967295 134512640 135094434 3221224432 3221223088 134556046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4608 4476 145 145 0 4463 0
[pid=8659] vsize: 18432
Current children cumulated CPU time (s) 529.63
Current children cumulated vsize (Kb) 20556

[startup+540.051 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4628 0 2 0 53926 36 0 0 25 0 1 0 1841216437 19238912 4565 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4697 4565 145 145 0 4552 0
[pid=8659] vsize: 18788
Current children cumulated CPU time (s) 539.63
Current children cumulated vsize (Kb) 20912

[startup+550.052 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4628 0 2 0 54926 36 0 0 25 0 1 0 1841216437 19238912 4565 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4697 4565 145 145 0 4552 0
[pid=8659] vsize: 18788
Current children cumulated CPU time (s) 549.63
Current children cumulated vsize (Kb) 20912

[startup+560.053 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4628 0 2 0 55925 37 0 0 25 0 1 0 1841216437 19238912 4565 4294967295 134512640 135094434 3221224432 3221223056 134557702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4697 4565 145 145 0 4552 0
[pid=8659] vsize: 18788
Current children cumulated CPU time (s) 559.63
Current children cumulated vsize (Kb) 20912

[startup+570.053 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4628 0 2 0 56925 37 0 0 25 0 1 0 1841216437 19238912 4565 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4697 4565 145 145 0 4552 0
[pid=8659] vsize: 18788
Current children cumulated CPU time (s) 569.63
Current children cumulated vsize (Kb) 20912

[startup+580.054 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4628 0 2 0 57925 37 0 0 25 0 1 0 1841216437 19238912 4565 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4697 4565 145 145 0 4552 0
[pid=8659] vsize: 18788
Current children cumulated CPU time (s) 579.63
Current children cumulated vsize (Kb) 20912

[startup+590.055 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4628 0 2 0 58925 37 0 0 25 0 1 0 1841216437 19238912 4565 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4697 4565 145 145 0 4552 0
[pid=8659] vsize: 18788
Current children cumulated CPU time (s) 589.63
Current children cumulated vsize (Kb) 20912

[startup+600.056 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4628 0 2 0 59925 38 0 0 25 0 1 0 1841216437 19238912 4565 4294967295 134512640 135094434 3221224432 3221223024 134557413 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8659/statm): 4697 4565 145 145 0 4552 0
[pid=8659] vsize: 18788
Current children cumulated CPU time (s) 599.64
Current children cumulated vsize (Kb) 20912

[startup+610.058 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4628 0 2 0 60924 38 0 0 25 0 1 0 1841216437 19238912 4565 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4697 4565 145 145 0 4552 0
[pid=8659] vsize: 18788
Current children cumulated CPU time (s) 609.63
Current children cumulated vsize (Kb) 20912

[startup+620.058 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4628 0 2 0 61924 38 0 0 25 0 1 0 1841216437 19238912 4565 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4697 4565 145 145 0 4552 0
[pid=8659] vsize: 18788
Current children cumulated CPU time (s) 619.63
Current children cumulated vsize (Kb) 20912

[startup+630.058 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4629 0 2 0 62925 38 0 0 25 0 1 0 1841216437 19238912 4566 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4697 4566 145 145 0 4552 0
[pid=8659] vsize: 18788
Current children cumulated CPU time (s) 629.64
Current children cumulated vsize (Kb) 20912

[startup+640.059 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4629 0 2 0 63924 38 0 0 25 0 1 0 1841216437 19238912 4566 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4697 4566 145 145 0 4552 0
[pid=8659] vsize: 18788
Current children cumulated CPU time (s) 639.63
Current children cumulated vsize (Kb) 20912

[startup+650.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4629 0 2 0 64925 38 0 0 25 0 1 0 1841216437 19238912 4566 4294967295 134512640 135094434 3221224432 3221223008 134785405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4697 4566 145 145 0 4552 0
[pid=8659] vsize: 18788
Current children cumulated CPU time (s) 649.64
Current children cumulated vsize (Kb) 20912

[startup+660.062 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4630 0 2 0 65925 38 0 0 25 0 1 0 1841216437 19238912 4567 4294967295 134512640 135094434 3221224432 3221223088 134557976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4697 4567 145 145 0 4552 0
[pid=8659] vsize: 18788
Current children cumulated CPU time (s) 659.64
Current children cumulated vsize (Kb) 20912

[startup+670.062 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4630 0 2 0 66924 39 0 0 25 0 1 0 1841216437 19238912 4567 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4697 4567 145 145 0 4552 0
[pid=8659] vsize: 18788
Current children cumulated CPU time (s) 669.64
Current children cumulated vsize (Kb) 20912

[startup+680.062 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4630 0 2 0 67925 39 0 0 25 0 1 0 1841216437 19238912 4567 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4697 4567 145 145 0 4552 0
[pid=8659] vsize: 18788
Current children cumulated CPU time (s) 679.65
Current children cumulated vsize (Kb) 20912

[startup+690.063 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4630 0 2 0 68925 39 0 0 25 0 1 0 1841216437 19238912 4567 4294967295 134512640 135094434 3221224432 3221223024 134552006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4697 4567 145 145 0 4552 0
[pid=8659] vsize: 18788
Current children cumulated CPU time (s) 689.65
Current children cumulated vsize (Kb) 20912

[startup+700.064 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4634 0 2 0 69925 39 0 0 25 0 1 0 1841216437 19267584 4571 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4704 4571 145 145 0 4559 0
[pid=8659] vsize: 18816
Current children cumulated CPU time (s) 699.65
Current children cumulated vsize (Kb) 20940

[startup+710.065 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4654 0 2 0 70924 39 0 0 25 0 1 0 1841216437 19349504 4591 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4724 4591 145 145 0 4579 0
[pid=8659] vsize: 18896
Current children cumulated CPU time (s) 709.64
Current children cumulated vsize (Kb) 21020

[startup+720.065 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4654 0 2 0 71925 39 0 0 25 0 1 0 1841216437 19349504 4591 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4724 4591 145 145 0 4579 0
[pid=8659] vsize: 18896
Current children cumulated CPU time (s) 719.65
Current children cumulated vsize (Kb) 21020

[startup+730.065 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4680 0 2 0 72925 40 0 0 25 0 1 0 1841216437 19460096 4617 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4751 4617 145 145 0 4606 0
[pid=8659] vsize: 19004
Current children cumulated CPU time (s) 729.66
Current children cumulated vsize (Kb) 21128

[startup+740.066 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4769 0 2 0 73924 40 0 0 25 0 1 0 1841216437 19836928 4706 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4843 4706 145 145 0 4698 0
[pid=8659] vsize: 19372
Current children cumulated CPU time (s) 739.65
Current children cumulated vsize (Kb) 21496

[startup+750.067 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4769 0 2 0 74924 40 0 0 25 0 1 0 1841216437 19836928 4706 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4843 4706 145 145 0 4698 0
[pid=8659] vsize: 19372
Current children cumulated CPU time (s) 749.65
Current children cumulated vsize (Kb) 21496

[startup+760.067 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4818 0 2 0 75923 41 0 0 25 0 1 0 1841216437 20094976 4755 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4906 4755 145 145 0 4761 0
[pid=8659] vsize: 19624
Current children cumulated CPU time (s) 759.65
Current children cumulated vsize (Kb) 21748

[startup+770.068 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4818 0 2 0 76924 41 0 0 25 0 1 0 1841216437 20094976 4755 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4906 4755 145 145 0 4761 0
[pid=8659] vsize: 19624
Current children cumulated CPU time (s) 769.66
Current children cumulated vsize (Kb) 21748

[startup+780.069 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4818 0 2 0 77924 41 0 0 25 0 1 0 1841216437 20094976 4755 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4906 4755 145 145 0 4761 0
[pid=8659] vsize: 19624
Current children cumulated CPU time (s) 779.66
Current children cumulated vsize (Kb) 21748

[startup+790.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4818 0 2 0 78924 41 0 0 25 0 1 0 1841216437 20094976 4755 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4906 4755 145 145 0 4761 0
[pid=8659] vsize: 19624
Current children cumulated CPU time (s) 789.66
Current children cumulated vsize (Kb) 21748

[startup+800.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4818 0 2 0 79924 41 0 0 25 0 1 0 1841216437 20094976 4755 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4906 4755 145 145 0 4761 0
[pid=8659] vsize: 19624
Current children cumulated CPU time (s) 799.66
Current children cumulated vsize (Kb) 21748

[startup+810.071 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4818 0 2 0 80924 41 0 0 25 0 1 0 1841216437 20094976 4755 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4906 4755 145 145 0 4761 0
[pid=8659] vsize: 19624
Current children cumulated CPU time (s) 809.66
Current children cumulated vsize (Kb) 21748

[startup+820.071 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4818 0 2 0 81924 41 0 0 25 0 1 0 1841216437 20094976 4755 4294967295 134512640 135094434 3221224432 3221223024 134556928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4906 4755 145 145 0 4761 0
[pid=8659] vsize: 19624
Current children cumulated CPU time (s) 819.66
Current children cumulated vsize (Kb) 21748

[startup+830.071 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4818 0 2 0 82925 41 0 0 25 0 1 0 1841216437 20094976 4755 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4906 4755 145 145 0 4761 0
[pid=8659] vsize: 19624
Current children cumulated CPU time (s) 829.67
Current children cumulated vsize (Kb) 21748

[startup+840.072 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4818 0 2 0 83925 41 0 0 25 0 1 0 1841216437 20094976 4755 4294967295 134512640 135094434 3221224432 3221223024 134556996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4906 4755 145 145 0 4761 0
[pid=8659] vsize: 19624
Current children cumulated CPU time (s) 839.67
Current children cumulated vsize (Kb) 21748

[startup+850.073 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4841 0 2 0 84925 41 0 0 25 0 1 0 1841216437 20189184 4778 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4929 4778 145 145 0 4784 0
[pid=8659] vsize: 19716
Current children cumulated CPU time (s) 849.67
Current children cumulated vsize (Kb) 21840

[startup+860.073 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4841 0 2 0 85925 41 0 0 25 0 1 0 1841216437 20189184 4778 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4929 4778 145 145 0 4784 0
[pid=8659] vsize: 19716
Current children cumulated CPU time (s) 859.67
Current children cumulated vsize (Kb) 21840

[startup+870.074 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4841 0 2 0 86925 42 0 0 25 0 1 0 1841216437 20189184 4778 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4929 4778 145 145 0 4784 0
[pid=8659] vsize: 19716
Current children cumulated CPU time (s) 869.68
Current children cumulated vsize (Kb) 21840

[startup+880.074 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4842 0 2 0 87925 42 0 0 25 0 1 0 1841216437 20189184 4779 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4929 4779 145 145 0 4784 0
[pid=8659] vsize: 19716
Current children cumulated CPU time (s) 879.68
Current children cumulated vsize (Kb) 21840

[startup+890.075 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4842 0 2 0 88925 42 0 0 25 0 1 0 1841216437 20189184 4779 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4929 4779 145 145 0 4784 0
[pid=8659] vsize: 19716
Current children cumulated CPU time (s) 889.68
Current children cumulated vsize (Kb) 21840

[startup+900.076 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4842 0 2 0 89925 42 0 0 25 0 1 0 1841216437 20189184 4779 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4929 4779 145 145 0 4784 0
[pid=8659] vsize: 19716
Current children cumulated CPU time (s) 899.68
Current children cumulated vsize (Kb) 21840

[startup+910.076 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4842 0 2 0 90925 42 0 0 25 0 1 0 1841216437 20189184 4779 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4929 4779 145 145 0 4784 0
[pid=8659] vsize: 19716
Current children cumulated CPU time (s) 909.68
Current children cumulated vsize (Kb) 21840

[startup+920.077 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 4843 0 2 0 91926 42 0 0 25 0 1 0 1841216437 20189184 4780 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 4929 4780 145 145 0 4784 0
[pid=8659] vsize: 19716
Current children cumulated CPU time (s) 919.69
Current children cumulated vsize (Kb) 21840

[startup+930.078 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5174 0 2 0 92922 43 0 0 25 0 1 0 1841216437 21606400 5111 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5275 5111 145 145 0 5130 0
[pid=8659] vsize: 21100
Current children cumulated CPU time (s) 929.66
Current children cumulated vsize (Kb) 23224

[startup+940.079 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5175 0 2 0 93921 44 0 0 25 0 1 0 1841216437 21606400 5112 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5275 5112 145 145 0 5130 0
[pid=8659] vsize: 21100
Current children cumulated CPU time (s) 939.66
Current children cumulated vsize (Kb) 23224

[startup+950.079 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5175 0 2 0 94922 44 0 0 25 0 1 0 1841216437 21606400 5112 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5275 5112 145 145 0 5130 0
[pid=8659] vsize: 21100
Current children cumulated CPU time (s) 949.67
Current children cumulated vsize (Kb) 23224

[startup+960.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5175 0 2 0 95922 44 0 0 25 0 1 0 1841216437 21606400 5112 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5275 5112 145 145 0 5130 0
[pid=8659] vsize: 21100
Current children cumulated CPU time (s) 959.67
Current children cumulated vsize (Kb) 23224

[startup+970.081 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5176 0 2 0 96922 44 0 0 25 0 1 0 1841216437 21606400 5113 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5275 5113 145 145 0 5130 0
[pid=8659] vsize: 21100
Current children cumulated CPU time (s) 969.67
Current children cumulated vsize (Kb) 23224

[startup+980.081 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5176 0 2 0 97922 44 0 0 25 0 1 0 1841216437 21606400 5113 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5275 5113 145 145 0 5130 0
[pid=8659] vsize: 21100
Current children cumulated CPU time (s) 979.67
Current children cumulated vsize (Kb) 23224

[startup+990.082 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5223 0 2 0 98922 44 0 0 25 0 1 0 1841216437 21798912 5160 4294967295 134512640 135094434 3221224432 3221223104 134556549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5322 5160 145 145 0 5177 0
[pid=8659] vsize: 21288
Current children cumulated CPU time (s) 989.67
Current children cumulated vsize (Kb) 23412

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5295 0 2 0 99921 44 0 0 25 0 1 0 1841216437 22102016 5232 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5396 5232 145 145 0 5251 0
[pid=8659] vsize: 21584
Current children cumulated CPU time (s) 999.66
Current children cumulated vsize (Kb) 23708

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5295 0 2 0 100921 45 0 0 25 0 1 0 1841216437 22102016 5232 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5396 5232 145 145 0 5251 0
[pid=8659] vsize: 21584
Current children cumulated CPU time (s) 1009.67
Current children cumulated vsize (Kb) 23708

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5295 0 2 0 101922 45 0 0 25 0 1 0 1841216437 22102016 5232 4294967295 134512640 135094434 3221224432 3221223088 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5396 5232 145 145 0 5251 0
[pid=8659] vsize: 21584
Current children cumulated CPU time (s) 1019.68
Current children cumulated vsize (Kb) 23708

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5295 0 2 0 102921 45 0 0 25 0 1 0 1841216437 22102016 5232 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5396 5232 145 145 0 5251 0
[pid=8659] vsize: 21584
Current children cumulated CPU time (s) 1029.67
Current children cumulated vsize (Kb) 23708

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5437 0 2 0 103919 46 0 0 25 0 1 0 1841216437 22679552 5374 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5537 5374 145 145 0 5392 0
[pid=8659] vsize: 22148
Current children cumulated CPU time (s) 1039.66
Current children cumulated vsize (Kb) 24272

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5437 0 2 0 104920 46 0 0 25 0 1 0 1841216437 22679552 5374 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5537 5374 145 145 0 5392 0
[pid=8659] vsize: 22148
Current children cumulated CPU time (s) 1049.67
Current children cumulated vsize (Kb) 24272

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5437 0 2 0 105920 46 0 0 25 0 1 0 1841216437 22679552 5374 4294967295 134512640 135094434 3221224432 3221223024 134556982 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5537 5374 145 145 0 5392 0
[pid=8659] vsize: 22148
Current children cumulated CPU time (s) 1059.67
Current children cumulated vsize (Kb) 24272

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5437 0 2 0 106920 46 0 0 25 0 1 0 1841216437 22679552 5374 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5537 5374 145 145 0 5392 0
[pid=8659] vsize: 22148
Current children cumulated CPU time (s) 1069.67
Current children cumulated vsize (Kb) 24272

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5437 0 2 0 107920 46 0 0 25 0 1 0 1841216437 22413312 5309 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5472 5309 145 145 0 5327 0
[pid=8659] vsize: 21888
Current children cumulated CPU time (s) 1079.67
Current children cumulated vsize (Kb) 24012

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5437 0 2 0 108921 46 0 0 25 0 1 0 1841216437 22413312 5309 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5472 5309 145 145 0 5327 0
[pid=8659] vsize: 21888
Current children cumulated CPU time (s) 1089.68
Current children cumulated vsize (Kb) 24012

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5437 0 2 0 109921 46 0 0 25 0 1 0 1841216437 22413312 5309 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5472 5309 145 145 0 5327 0
[pid=8659] vsize: 21888
Current children cumulated CPU time (s) 1099.68
Current children cumulated vsize (Kb) 24012

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5437 0 2 0 110921 46 0 0 25 0 1 0 1841216437 22413312 5309 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5472 5309 145 145 0 5327 0
[pid=8659] vsize: 21888
Current children cumulated CPU time (s) 1109.68
Current children cumulated vsize (Kb) 24012

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5455 0 2 0 111921 46 0 0 25 0 1 0 1841216437 22487040 5327 4294967295 134512640 135094434 3221224432 3221223024 134557413 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5490 5327 145 145 0 5345 0
[pid=8659] vsize: 21960
Current children cumulated CPU time (s) 1119.68
Current children cumulated vsize (Kb) 24084

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5719 0 2 0 112915 50 0 0 25 0 1 0 1841216437 23584768 5591 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5758 5591 145 145 0 5613 0
[pid=8659] vsize: 23032
Current children cumulated CPU time (s) 1129.66
Current children cumulated vsize (Kb) 25156

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5719 0 2 0 113915 50 0 0 25 0 1 0 1841216437 23584768 5591 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5758 5591 145 145 0 5613 0
[pid=8659] vsize: 23032
Current children cumulated CPU time (s) 1139.66
Current children cumulated vsize (Kb) 25156

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5868 0 2 0 114912 52 0 0 25 0 1 0 1841216437 24190976 5740 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5906 5740 145 145 0 5761 0
[pid=8659] vsize: 23624
Current children cumulated CPU time (s) 1149.65
Current children cumulated vsize (Kb) 25748

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 5926 0 2 0 115910 53 0 0 25 0 1 0 1841216437 24428544 5798 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 5964 5798 145 145 0 5819 0
[pid=8659] vsize: 23856
Current children cumulated CPU time (s) 1159.64
Current children cumulated vsize (Kb) 25980

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 6124 0 2 0 116907 55 0 0 25 0 1 0 1841216437 25235456 5996 4294967295 134512640 135094434 3221224432 3221223024 134551876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 6161 5996 145 145 0 6016 0
[pid=8659] vsize: 24644
Current children cumulated CPU time (s) 1169.63
Current children cumulated vsize (Kb) 26768

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 6125 0 2 0 117907 55 0 0 25 0 1 0 1841216437 25235456 5997 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 6161 5997 145 145 0 6016 0
[pid=8659] vsize: 24644
Current children cumulated CPU time (s) 1179.63
Current children cumulated vsize (Kb) 26768

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 6125 0 2 0 118907 55 0 0 25 0 1 0 1841216437 25235456 5997 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 6161 5997 145 145 0 6016 0
[pid=8659] vsize: 24644
Current children cumulated CPU time (s) 1189.63
Current children cumulated vsize (Kb) 26768

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 6125 0 2 0 119907 55 0 0 25 0 1 0 1841216437 25235456 5997 4294967295 134512640 135094434 3221224432 3221223024 134551469 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 6161 5997 145 145 0 6016 0
[pid=8659] vsize: 24644
Current children cumulated CPU time (s) 1199.63
Current children cumulated vsize (Kb) 26768

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 6125 0 2 0 120907 55 0 0 25 0 1 0 1841216437 25235456 5997 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 6161 5997 145 145 0 6016 0
[pid=8659] vsize: 24644
Current children cumulated CPU time (s) 1209.63
Current children cumulated vsize (Kb) 26768



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8659
Raw data (/proc/8655/stat): 8655 (minisat+_script) S 8654 8655 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841216431 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8655/statm): 531 226 485 147 0 384 0
[pid=8655] vsize: 2124
Raw data (/proc/8659/stat): 8659 (minisat+_64-bit) R 8655 8655 5245 0 -1 0 6125 0 2 0 120907 55 0 0 25 0 1 0 1841216437 25235456 5997 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8659/statm): 6161 5997 145 145 0 6016 0
[pid=8659] vsize: 24644
Current children cumulated CPU time (s) 1209.63
Current children cumulated vsize (Kb) 26768

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

Child status: 0
Real time (s): 1210.11
CPU time (s): 1209.65
CPU user time (s): 1209.08
CPU system time (s): 0.571913
CPU usage (%): 99.9617
Max. virtual memory (cumulated for all children) (Kb): 26768

Verifier Data

ERROR: no interpretation found !