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-chnl30_40_pb.cnf.cr.opb
MD5SUM6a0000bd3257094a387dbf208b4df8cf
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 41
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.080987
Number of variables2400
Total number of constraints140
Number of constraints which are clauses80
Number of constraints which are cardinality constraints (but not clauses)60
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint30
Maximum length of a constraint40

Trace number 816

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        935112 kB
Buffers:         34060 kB
Cached:          38424 kB
SwapCached:        820 kB
Active:          53484 kB
Inactive:        21696 kB
HighTotal:      131008 kB
HighFree:        90804 kB
LowTotal:       903652 kB
LowFree:        844308 kB
SwapTotal:     2097136 kB
SwapFree:      2095864 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5692 kB
Slab:            18812 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 12:45:22 (client local time) WITH STATUS 0 IN 1208.87 SECONDS
stats: 2355 7 1208.87 0

Solver Data

c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................................................................
c ---[  59]---> BDD-cost:   77
c ---[  58]---> BDD-cost:   77
c ---[  57]---> BDD-cost:   77
c ---[  56]---> BDD-cost:   77
c ---[  55]---> BDD-cost:   77
c ---[  54]---> BDD-cost:   77
c ---[  53]---> BDD-cost:   77
c ---[  52]---> BDD-cost:   77
c ---[  51]---> BDD-cost:   77
c ---[  50]---> BDD-cost:   77
c ---[  49]---> BDD-cost:   77
c ---[  48]---> BDD-cost:   77
c ---[  47]---> BDD-cost:   77
c ---[  46]---> BDD-cost:   77
c ---[  45]---> BDD-cost:   77
c ---[  44]---> BDD-cost:   77
c ---[  43]---> BDD-cost:   77
c ---[  42]---> BDD-cost:   77
c ---[  41]---> BDD-cost:   77
c ---[  40]---> BDD-cost:   77
c ---[  39]---> BDD-cost:   77
c ---[  38]---> BDD-cost:   77
c ---[  37]---> BDD-cost:   77
c ---[  36]---> BDD-cost:   77
c ---[  35]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   77
c ---[  33]---> BDD-cost:   77
c ---[  32]---> BDD-cost:   77
c ---[  31]---> BDD-cost:   77
c ---[  30]---> BDD-cost:   77
c ---[  29]---> BDD-cost:   77
c ---[  28]---> BDD-cost:   77
c ---[  27]---> BDD-cost:   77
c ---[  26]---> BDD-cost:   77
c ---[  25]---> BDD-cost:   77
c ---[  24]---> BDD-cost:   77
c ---[  23]---> BDD-cost:   77
c ---[  22]---> BDD-cost:   77
c ---[  21]---> BDD-cost:   77
c ---[  20]---> BDD-cost:   77
c ---[  19]---> BDD-cost:   77
c ---[  18]---> BDD-cost:   77
c ---[  17]---> BDD-cost:   77
c ---[  16]---> BDD-cost:   77
c ---[  15]---> BDD-cost:   77
c ---[  14]---> BDD-cost:   77
c ---[  13]---> BDD-cost:   77
c ---[  12]---> BDD-cost:   77
c ---[  11]---> BDD-cost:   77
c ---[  10]---> BDD-cost:   77
c ---[   9]---> BDD-cost:   77
c ---[   8]---> BDD-cost:   77
c ---[   7]---> BDD-cost:   77
c ---[   6]---> BDD-cost:   77
c ---[   5]---> BDD-cost:   77
c ---[   4]---> BDD-cost:   77
c ---[   3]---> BDD-cost:   77
c ---[   2]---> BDD-cost:   77
c ---[   1]---> BDD-cost:   77
c ---[   0]---> BDD-cost:   77
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   11540    32220 |    3846       0        0     nan |  0.000 % |
c |       105 |   11540    32220 |    4230     105    11655   111.0 |  0.855 % |
c |       256 |   11540    32220 |    4653     256    29323   114.5 |  0.855 % |
c |       482 |   11540    32220 |    5119     482    59867   124.2 |  0.855 % |
c |       819 |   11540    32220 |    5630     819   119821   146.3 |  0.855 % |
c |      1326 |   11540    32220 |    6194    1326   200884   151.5 |  0.855 % |
c |      2085 |   11540    32220 |    6813    2085   338592   162.4 |  0.855 % |
c |      3224 |   11540    32220 |    7494    3224   573967   178.0 |  0.855 % |
c |      4933 |   11540    32220 |    8244    4933  1020753   206.9 |  0.855 % |
c |      7495 |   11540    32220 |    9068    7495  1644283   219.4 |  0.855 % |
c |     11343 |   11540    32220 |    9975   11343  2620703   231.0 |  0.855 % |
c |     17110 |   11540    32220 |   10973   11439  2978380   260.4 |  0.855 % |
c |     25760 |   11540    32220 |   12070    7811  2675183   342.5 |  0.855 % |
c |     38735 |   11540    32220 |   13277   13643  5459721   400.2 |  0.855 % |
c |     58196 |   11540    32220 |   14605   10980  5555897   506.0 |  0.855 % |
c |     87389 |   11540    32220 |   16065   15223  7944453   521.9 |  0.855 % |
c |    131185 |   11540    32220 |   17672   13326  6647495   498.8 |  0.855 % |
c |    196871 |   11540    32220 |   19439   19364  9746152   503.3 |  0.855 % |

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/7669/stat): 7669 (minisat+_script) R 7668 7669 5299 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841247266 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/7669/statm): 174 3 169 147 0 27 0
[pid=7669] 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=7670
New process pid=7671
New process pid=7672
execve syscall for /bin/sed executable
One traced child (pid=7671) 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=7672) exited with status: 0
One traced child (pid=7670) exited with status: 0
New process pid=7673
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc23/normalized-chnl30_40_pb.cnf.cr.opb

[startup+10.0047 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 2638 0 2 0 944 12 0 0 25 0 1 0 1841247271 11190272 2626 4294967295 134512640 135094434 3221224432 3221223024 134556866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 2732 2626 145 145 0 2587 0
[pid=7673] vsize: 10928
Current children cumulated CPU time (s) 9.58
Current children cumulated vsize (Kb) 13052

[startup+20.0063 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 3481 0 2 0 1931 17 0 0 25 0 1 0 1841247271 14630912 3469 4294967295 134512640 135094434 3221224432 3221223088 134558135 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 3572 3469 145 145 0 3427 0
[pid=7673] vsize: 14288
Current children cumulated CPU time (s) 19.5
Current children cumulated vsize (Kb) 16412

[startup+30.007 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 3913 0 2 0 2925 19 0 0 25 0 1 0 1841247271 16400384 3901 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 4004 3901 145 145 0 3859 0
[pid=7673] vsize: 16016
Current children cumulated CPU time (s) 29.46
Current children cumulated vsize (Kb) 18140

[startup+40.0076 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 4975 0 2 0 3907 26 0 0 24 0 1 0 1841247271 20742144 4963 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 5064 4963 145 145 0 4919 0
[pid=7673] vsize: 20256
Current children cumulated CPU time (s) 39.35
Current children cumulated vsize (Kb) 22380

[startup+50.0082 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 4975 0 2 0 4907 27 0 0 25 0 1 0 1841247271 20742144 4963 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 5064 4963 145 145 0 4919 0
[pid=7673] vsize: 20256
Current children cumulated CPU time (s) 49.36
Current children cumulated vsize (Kb) 22380

[startup+60.0089 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 5997 0 2 0 5892 33 0 0 25 0 1 0 1841247271 24928256 5985 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 6086 5985 145 145 0 5941 0
[pid=7673] vsize: 24344
Current children cumulated CPU time (s) 59.27
Current children cumulated vsize (Kb) 26468

[startup+70.0095 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 5997 0 2 0 6892 33 0 0 25 0 1 0 1841247271 24928256 5985 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 6086 5985 145 145 0 5941 0
[pid=7673] vsize: 24344
Current children cumulated CPU time (s) 69.27
Current children cumulated vsize (Kb) 26468

[startup+80.0102 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 6289 0 2 0 7887 36 0 0 25 0 1 0 1841247271 26124288 6277 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 6378 6277 145 145 0 6233 0
[pid=7673] vsize: 25512
Current children cumulated CPU time (s) 79.25
Current children cumulated vsize (Kb) 27636

[startup+90.0108 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 6647 0 2 0 8881 39 0 0 25 0 1 0 1841247271 27590656 6635 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 6736 6635 145 145 0 6591 0
[pid=7673] vsize: 26944
Current children cumulated CPU time (s) 89.22
Current children cumulated vsize (Kb) 29068

[startup+100.011 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 7276 0 2 0 9872 42 0 0 25 0 1 0 1841247271 30175232 7264 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 7367 7264 145 145 0 7222 0
[pid=7673] vsize: 29468
Current children cumulated CPU time (s) 99.16
Current children cumulated vsize (Kb) 31592

[startup+110.012 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 7901 0 2 0 10865 45 0 0 25 0 1 0 1841247271 32780288 7889 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 8003 7889 145 145 0 7858 0
[pid=7673] vsize: 32012
Current children cumulated CPU time (s) 109.12
Current children cumulated vsize (Kb) 34136

[startup+120.013 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 7901 0 2 0 11864 46 0 0 25 0 1 0 1841247271 32780288 7889 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 8003 7889 145 145 0 7858 0
[pid=7673] vsize: 32012
Current children cumulated CPU time (s) 119.12
Current children cumulated vsize (Kb) 34136

[startup+130.013 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 7901 0 2 0 12865 46 0 0 25 0 1 0 1841247271 32780288 7889 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 8003 7889 145 145 0 7858 0
[pid=7673] vsize: 32012
Current children cumulated CPU time (s) 129.13
Current children cumulated vsize (Kb) 34136

[startup+140.015 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 8036 0 2 0 13863 47 0 0 25 0 1 0 1841247271 33333248 8024 4294967295 134512640 135094434 3221224432 3221223104 134556329 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 8138 8024 145 145 0 7993 0
[pid=7673] vsize: 32552
Current children cumulated CPU time (s) 139.12
Current children cumulated vsize (Kb) 34676

[startup+150.016 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 8036 0 2 0 14863 47 0 0 25 0 1 0 1841247271 33333248 8024 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 8138 8024 145 145 0 7993 0
[pid=7673] vsize: 32552
Current children cumulated CPU time (s) 149.12
Current children cumulated vsize (Kb) 34676

[startup+160.016 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 8517 0 2 0 15855 51 0 0 25 0 1 0 1841247271 35303424 8505 4294967295 134512640 135094434 3221224432 3221223024 134556975 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7673/statm): 8619 8505 145 145 0 8474 0
[pid=7673] vsize: 34476
Current children cumulated CPU time (s) 159.08
Current children cumulated vsize (Kb) 36600

[startup+170.018 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) T 7669 7669 5299 0 -1 0 9647 0 2 0 16837 58 0 0 25 0 1 0 1841247271 39989248 9635 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7673/statm): 9763 9635 145 145 0 9618 0
[pid=7673] vsize: 39052
Current children cumulated CPU time (s) 168.97
Current children cumulated vsize (Kb) 41176

[startup+180.019 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 9763 0 2 0 17835 59 0 0 25 0 1 0 1841247271 40464384 9751 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 9879 9751 145 145 0 9734 0
[pid=7673] vsize: 39516
Current children cumulated CPU time (s) 178.96
Current children cumulated vsize (Kb) 41640

[startup+190.019 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 9763 0 2 0 18835 59 0 0 25 0 1 0 1841247271 40464384 9751 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 9879 9751 145 145 0 9734 0
[pid=7673] vsize: 39516
Current children cumulated CPU time (s) 188.96
Current children cumulated vsize (Kb) 41640

[startup+200.02 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 9763 0 2 0 19836 59 0 0 25 0 1 0 1841247271 40464384 9751 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 9879 9751 145 145 0 9734 0
[pid=7673] vsize: 39516
Current children cumulated CPU time (s) 198.97
Current children cumulated vsize (Kb) 41640

[startup+210.02 s]
Raw data (loadavg): 0.99 1.00 0.98 1/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) T 7669 7669 5299 0 -1 0 9854 0 2 0 20833 60 0 0 25 0 1 0 1841247271 40837120 9842 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/7673/statm): 9970 9842 145 145 0 9825 0
[pid=7673] vsize: 39880
Current children cumulated CPU time (s) 208.95
Current children cumulated vsize (Kb) 42004

[startup+220.021 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 10140 0 2 0 21829 63 0 0 25 0 1 0 1841247271 42008576 10128 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 10256 10128 145 145 0 10111 0
[pid=7673] vsize: 41024
Current children cumulated CPU time (s) 218.94
Current children cumulated vsize (Kb) 43148

[startup+230.022 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 10140 0 2 0 22829 63 0 0 25 0 1 0 1841247271 42008576 10128 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 10256 10128 145 145 0 10111 0
[pid=7673] vsize: 41024
Current children cumulated CPU time (s) 228.94
Current children cumulated vsize (Kb) 43148

[startup+240.022 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 10140 0 2 0 23827 65 0 0 25 0 1 0 1841247271 42008576 10128 4294967295 134512640 135094434 3221224432 3221223024 134552006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 10256 10128 145 145 0 10111 0
[pid=7673] vsize: 41024
Current children cumulated CPU time (s) 238.94
Current children cumulated vsize (Kb) 43148

[startup+250.023 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 10140 0 2 0 24827 65 0 0 25 0 1 0 1841247271 42008576 10128 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 10256 10128 145 145 0 10111 0
[pid=7673] vsize: 41024
Current children cumulated CPU time (s) 248.94
Current children cumulated vsize (Kb) 43148

[startup+260.024 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 10433 0 2 0 25823 67 0 0 25 0 1 0 1841247271 43208704 10421 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 10549 10421 145 145 0 10404 0
[pid=7673] vsize: 42196
Current children cumulated CPU time (s) 258.92
Current children cumulated vsize (Kb) 44320

[startup+270.024 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 10433 0 2 0 26823 67 0 0 25 0 1 0 1841247271 43208704 10421 4294967295 134512640 135094434 3221224432 3221223024 134556993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 10549 10421 145 145 0 10404 0
[pid=7673] vsize: 42196
Current children cumulated CPU time (s) 268.92
Current children cumulated vsize (Kb) 44320

[startup+280.025 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 10433 0 2 0 27823 68 0 0 25 0 1 0 1841247271 43208704 10421 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 10549 10421 145 145 0 10404 0
[pid=7673] vsize: 42196
Current children cumulated CPU time (s) 278.93
Current children cumulated vsize (Kb) 44320

[startup+290.027 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 10433 0 2 0 28823 68 0 0 25 0 1 0 1841247271 43208704 10421 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 10549 10421 145 145 0 10404 0
[pid=7673] vsize: 42196
Current children cumulated CPU time (s) 288.93
Current children cumulated vsize (Kb) 44320

[startup+300.027 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 10433 0 2 0 29823 68 0 0 25 0 1 0 1841247271 43208704 10421 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 10549 10421 145 145 0 10404 0
[pid=7673] vsize: 42196
Current children cumulated CPU time (s) 298.93
Current children cumulated vsize (Kb) 44320

[startup+310.028 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 10517 0 2 0 30821 70 0 0 25 0 1 0 1841247271 43556864 10505 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 10634 10505 145 145 0 10489 0
[pid=7673] vsize: 42536
Current children cumulated CPU time (s) 308.93
Current children cumulated vsize (Kb) 44660

[startup+320.03 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11060 0 2 0 31812 73 0 0 25 0 1 0 1841247271 45776896 11048 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11176 11048 145 145 0 11031 0
[pid=7673] vsize: 44704
Current children cumulated CPU time (s) 318.87
Current children cumulated vsize (Kb) 46828

[startup+330.03 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11060 0 2 0 32813 73 0 0 25 0 1 0 1841247271 45776896 11048 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11176 11048 145 145 0 11031 0
[pid=7673] vsize: 44704
Current children cumulated CPU time (s) 328.88
Current children cumulated vsize (Kb) 46828

[startup+340.031 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11060 0 2 0 33813 73 0 0 25 0 1 0 1841247271 45776896 11048 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11176 11048 145 145 0 11031 0
[pid=7673] vsize: 44704
Current children cumulated CPU time (s) 338.88
Current children cumulated vsize (Kb) 46828

[startup+350.033 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11060 0 2 0 34813 74 0 0 25 0 1 0 1841247271 45776896 11048 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11176 11048 145 145 0 11031 0
[pid=7673] vsize: 44704
Current children cumulated CPU time (s) 348.89
Current children cumulated vsize (Kb) 46828

[startup+360.033 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11060 0 2 0 35813 74 0 0 25 0 1 0 1841247271 45776896 11048 4294967295 134512640 135094434 3221224432 3221223024 134557157 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11176 11048 145 145 0 11031 0
[pid=7673] vsize: 44704
Current children cumulated CPU time (s) 358.89
Current children cumulated vsize (Kb) 46828

[startup+370.034 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11060 0 2 0 36813 74 0 0 25 0 1 0 1841247271 45776896 11048 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11176 11048 145 145 0 11031 0
[pid=7673] vsize: 44704
Current children cumulated CPU time (s) 368.89
Current children cumulated vsize (Kb) 46828

[startup+380.034 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11060 0 2 0 37813 74 0 0 25 0 1 0 1841247271 45776896 11048 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11176 11048 145 145 0 11031 0
[pid=7673] vsize: 44704
Current children cumulated CPU time (s) 378.89
Current children cumulated vsize (Kb) 46828

[startup+390.036 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11061 0 2 0 38813 74 0 0 25 0 1 0 1841247271 45776896 11049 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11176 11049 145 145 0 11031 0
[pid=7673] vsize: 44704
Current children cumulated CPU time (s) 388.89
Current children cumulated vsize (Kb) 46828

[startup+400.037 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11061 0 2 0 39814 74 0 0 25 0 1 0 1841247271 45776896 11049 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11176 11049 145 145 0 11031 0
[pid=7673] vsize: 44704
Current children cumulated CPU time (s) 398.9
Current children cumulated vsize (Kb) 46828

[startup+410.037 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11061 0 2 0 40814 74 0 0 25 0 1 0 1841247271 45776896 11049 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11176 11049 145 145 0 11031 0
[pid=7673] vsize: 44704
Current children cumulated CPU time (s) 408.9
Current children cumulated vsize (Kb) 46828

[startup+420.039 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11061 0 2 0 41814 75 0 0 25 0 1 0 1841247271 45776896 11049 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11176 11049 145 145 0 11031 0
[pid=7673] vsize: 44704
Current children cumulated CPU time (s) 418.91
Current children cumulated vsize (Kb) 46828

[startup+430.04 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11061 0 2 0 42814 75 0 0 25 0 1 0 1841247271 45776896 11049 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11176 11049 145 145 0 11031 0
[pid=7673] vsize: 44704
Current children cumulated CPU time (s) 428.91
Current children cumulated vsize (Kb) 46828

[startup+440.04 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11061 0 2 0 43814 75 0 0 25 0 1 0 1841247271 45776896 11049 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11176 11049 145 145 0 11031 0
[pid=7673] vsize: 44704
Current children cumulated CPU time (s) 438.91
Current children cumulated vsize (Kb) 46828

[startup+450.041 s]
Raw data (loadavg): 0.99 1.00 0.98 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11061 0 2 0 44815 75 0 0 25 0 1 0 1841247271 45776896 11049 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11176 11049 145 145 0 11031 0
[pid=7673] vsize: 44704
Current children cumulated CPU time (s) 448.92
Current children cumulated vsize (Kb) 46828

[startup+460.042 s]
Raw data (loadavg): 1.15 1.03 0.99 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11061 0 2 0 45814 75 0 0 25 0 1 0 1841247271 45776896 11049 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11176 11049 145 145 0 11031 0
[pid=7673] vsize: 44704
Current children cumulated CPU time (s) 458.91
Current children cumulated vsize (Kb) 46828

[startup+470.042 s]
Raw data (loadavg): 1.12 1.03 0.99 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11061 0 2 0 46815 75 0 0 25 0 1 0 1841247271 45776896 11049 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11176 11049 145 145 0 11031 0
[pid=7673] vsize: 44704
Current children cumulated CPU time (s) 468.92
Current children cumulated vsize (Kb) 46828

[startup+480.043 s]
Raw data (loadavg): 1.10 1.03 0.99 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11061 0 2 0 47815 75 0 0 25 0 1 0 1841247271 45776896 11049 4294967295 134512640 135094434 3221224432 3221223088 134558135 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11176 11049 145 145 0 11031 0
[pid=7673] vsize: 44704
Current children cumulated CPU time (s) 478.92
Current children cumulated vsize (Kb) 46828

[startup+490.044 s]
Raw data (loadavg): 1.24 1.06 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11061 0 2 0 48815 75 0 0 25 0 1 0 1841247271 45776896 11049 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11176 11049 145 145 0 11031 0
[pid=7673] vsize: 44704
Current children cumulated CPU time (s) 488.92
Current children cumulated vsize (Kb) 46828

[startup+500.045 s]
Raw data (loadavg): 1.20 1.06 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11061 0 2 0 49816 75 0 0 25 0 1 0 1841247271 45776896 11049 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11176 11049 145 145 0 11031 0
[pid=7673] vsize: 44704
Current children cumulated CPU time (s) 498.93
Current children cumulated vsize (Kb) 46828

[startup+510.046 s]
Raw data (loadavg): 1.17 1.06 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11061 0 2 0 50816 75 0 0 25 0 1 0 1841247271 45776896 11049 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11176 11049 145 145 0 11031 0
[pid=7673] vsize: 44704
Current children cumulated CPU time (s) 508.93
Current children cumulated vsize (Kb) 46828

[startup+520.046 s]
Raw data (loadavg): 1.15 1.05 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11061 0 2 0 51816 75 0 0 25 0 1 0 1841247271 45776896 11049 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11176 11049 145 145 0 11031 0
[pid=7673] vsize: 44704
Current children cumulated CPU time (s) 518.93
Current children cumulated vsize (Kb) 46828

[startup+530.047 s]
Raw data (loadavg): 1.12 1.05 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11061 0 2 0 52816 75 0 0 25 0 1 0 1841247271 45776896 11049 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11176 11049 145 145 0 11031 0
[pid=7673] vsize: 44704
Current children cumulated CPU time (s) 528.93
Current children cumulated vsize (Kb) 46828

[startup+540.048 s]
Raw data (loadavg): 1.10 1.05 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11130 0 2 0 53815 76 0 0 25 0 1 0 1841247271 46059520 11118 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11245 11118 145 145 0 11100 0
[pid=7673] vsize: 44980
Current children cumulated CPU time (s) 538.93
Current children cumulated vsize (Kb) 47104

[startup+550.048 s]
Raw data (loadavg): 1.09 1.05 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11649 0 2 0 54808 79 0 0 25 0 1 0 1841247271 48214016 11637 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11771 11637 145 145 0 11626 0
[pid=7673] vsize: 47084
Current children cumulated CPU time (s) 548.89
Current children cumulated vsize (Kb) 49208

[startup+560.049 s]
Raw data (loadavg): 1.07 1.05 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11649 0 2 0 55808 79 0 0 25 0 1 0 1841247271 48214016 11637 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11771 11637 145 145 0 11626 0
[pid=7673] vsize: 47084
Current children cumulated CPU time (s) 558.89
Current children cumulated vsize (Kb) 49208

[startup+570.05 s]
Raw data (loadavg): 1.06 1.04 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11649 0 2 0 56808 79 0 0 25 0 1 0 1841247271 48214016 11637 4294967295 134512640 135094434 3221224432 3221223104 134556327 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7673/statm): 11771 11637 145 145 0 11626 0
[pid=7673] vsize: 47084
Current children cumulated CPU time (s) 568.89
Current children cumulated vsize (Kb) 49208

[startup+580.05 s]
Raw data (loadavg): 1.05 1.04 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11650 0 2 0 57808 79 0 0 25 0 1 0 1841247271 48214016 11638 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11771 11638 145 145 0 11626 0
[pid=7673] vsize: 47084
Current children cumulated CPU time (s) 578.89
Current children cumulated vsize (Kb) 49208

[startup+590.052 s]
Raw data (loadavg): 1.04 1.04 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11651 0 2 0 58808 79 0 0 25 0 1 0 1841247271 48214016 11639 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11771 11639 145 145 0 11626 0
[pid=7673] vsize: 47084
Current children cumulated CPU time (s) 588.89
Current children cumulated vsize (Kb) 49208

[startup+600.053 s]
Raw data (loadavg): 1.04 1.04 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11651 0 2 0 59808 79 0 0 25 0 1 0 1841247271 48214016 11639 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11771 11639 145 145 0 11626 0
[pid=7673] vsize: 47084
Current children cumulated CPU time (s) 598.89
Current children cumulated vsize (Kb) 49208

[startup+610.053 s]
Raw data (loadavg): 1.03 1.04 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11651 0 2 0 60808 79 0 0 25 0 1 0 1841247271 48214016 11639 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11771 11639 145 145 0 11626 0
[pid=7673] vsize: 47084
Current children cumulated CPU time (s) 608.89
Current children cumulated vsize (Kb) 49208

[startup+620.054 s]
Raw data (loadavg): 1.02 1.03 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11651 0 2 0 61809 79 0 0 25 0 1 0 1841247271 48214016 11639 4294967295 134512640 135094434 3221224432 3221223024 134551925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11771 11639 145 145 0 11626 0
[pid=7673] vsize: 47084
Current children cumulated CPU time (s) 618.9
Current children cumulated vsize (Kb) 49208

[startup+630.054 s]
Raw data (loadavg): 1.02 1.03 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11651 0 2 0 62809 79 0 0 25 0 1 0 1841247271 48214016 11639 4294967295 134512640 135094434 3221224432 3221223088 134555980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11771 11639 145 145 0 11626 0
[pid=7673] vsize: 47084
Current children cumulated CPU time (s) 628.9
Current children cumulated vsize (Kb) 49208

[startup+640.055 s]
Raw data (loadavg): 1.02 1.03 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11651 0 2 0 63809 79 0 0 25 0 1 0 1841247271 48214016 11639 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11771 11639 145 145 0 11626 0
[pid=7673] vsize: 47084
Current children cumulated CPU time (s) 638.9
Current children cumulated vsize (Kb) 49208

[startup+650.056 s]
Raw data (loadavg): 1.01 1.03 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11651 0 2 0 64809 79 0 0 25 0 1 0 1841247271 48214016 11639 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11771 11639 145 145 0 11626 0
[pid=7673] vsize: 47084
Current children cumulated CPU time (s) 648.9
Current children cumulated vsize (Kb) 49208

[startup+660.056 s]
Raw data (loadavg): 1.01 1.03 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11651 0 2 0 65809 79 0 0 25 0 1 0 1841247271 48214016 11639 4294967295 134512640 135094434 3221224432 3221223104 134555224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11771 11639 145 145 0 11626 0
[pid=7673] vsize: 47084
Current children cumulated CPU time (s) 658.9
Current children cumulated vsize (Kb) 49208

[startup+670.057 s]
Raw data (loadavg): 1.01 1.03 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11651 0 2 0 66809 79 0 0 25 0 1 0 1841247271 48214016 11639 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11771 11639 145 145 0 11626 0
[pid=7673] vsize: 47084
Current children cumulated CPU time (s) 668.9
Current children cumulated vsize (Kb) 49208

[startup+680.058 s]
Raw data (loadavg): 1.01 1.03 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11651 0 2 0 67810 79 0 0 25 0 1 0 1841247271 48214016 11639 4294967295 134512640 135094434 3221224432 3221223024 134556843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11771 11639 145 145 0 11626 0
[pid=7673] vsize: 47084
Current children cumulated CPU time (s) 678.91
Current children cumulated vsize (Kb) 49208

[startup+690.058 s]
Raw data (loadavg): 1.01 1.02 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11651 0 2 0 68810 79 0 0 25 0 1 0 1841247271 48214016 11639 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11771 11639 145 145 0 11626 0
[pid=7673] vsize: 47084
Current children cumulated CPU time (s) 688.91
Current children cumulated vsize (Kb) 49208

[startup+700.059 s]
Raw data (loadavg): 1.00 1.02 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11651 0 2 0 69810 79 0 0 25 0 1 0 1841247271 48214016 11639 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11771 11639 145 145 0 11626 0
[pid=7673] vsize: 47084
Current children cumulated CPU time (s) 698.91
Current children cumulated vsize (Kb) 49208

[startup+710.06 s]
Raw data (loadavg): 1.00 1.02 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11651 0 2 0 70811 79 0 0 25 0 1 0 1841247271 48214016 11639 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11771 11639 145 145 0 11626 0
[pid=7673] vsize: 47084
Current children cumulated CPU time (s) 708.92
Current children cumulated vsize (Kb) 49208

[startup+720.06 s]
Raw data (loadavg): 1.00 1.02 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11651 0 2 0 71810 80 0 0 25 0 1 0 1841247271 48214016 11639 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11771 11639 145 145 0 11626 0
[pid=7673] vsize: 47084
Current children cumulated CPU time (s) 718.92
Current children cumulated vsize (Kb) 49208

[startup+730.061 s]
Raw data (loadavg): 1.00 1.02 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11762 0 2 0 72808 81 0 0 25 0 1 0 1841247271 48668672 11750 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11882 11750 145 145 0 11737 0
[pid=7673] vsize: 47528
Current children cumulated CPU time (s) 728.91
Current children cumulated vsize (Kb) 49652

[startup+740.062 s]
Raw data (loadavg): 1.00 1.02 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11762 0 2 0 73809 81 0 0 25 0 1 0 1841247271 48668672 11750 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 11882 11750 145 145 0 11737 0
[pid=7673] vsize: 47528
Current children cumulated CPU time (s) 738.92
Current children cumulated vsize (Kb) 49652

[startup+750.062 s]
Raw data (loadavg): 1.00 1.02 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11762 0 2 0 74809 81 0 0 25 0 1 0 1841247271 48668672 11750 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7673/statm): 11882 11750 145 145 0 11737 0
[pid=7673] vsize: 47528
Current children cumulated CPU time (s) 748.92
Current children cumulated vsize (Kb) 49652

[startup+760.063 s]
Raw data (loadavg): 1.00 1.02 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11762 0 2 0 75807 81 0 0 25 0 1 0 1841247271 48668672 11750 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7673/statm): 11882 11750 145 145 0 11737 0
[pid=7673] vsize: 47528
Current children cumulated CPU time (s) 758.9
Current children cumulated vsize (Kb) 49652

[startup+770.064 s]
Raw data (loadavg): 1.00 1.02 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 11834 0 2 0 76806 82 0 0 25 0 1 0 1841247271 48963584 11822 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7673/statm): 11954 11822 145 145 0 11809 0
[pid=7673] vsize: 47816
Current children cumulated CPU time (s) 768.9
Current children cumulated vsize (Kb) 49940

[startup+780.065 s]
Raw data (loadavg): 1.00 1.02 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 12481 0 2 0 77795 86 0 0 25 0 1 0 1841247271 51650560 12469 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 12610 12469 145 145 0 12465 0
[pid=7673] vsize: 50440
Current children cumulated CPU time (s) 778.83
Current children cumulated vsize (Kb) 52564

[startup+790.066 s]
Raw data (loadavg): 1.00 1.02 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 12481 0 2 0 78795 86 0 0 25 0 1 0 1841247271 51650560 12469 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 12610 12469 145 145 0 12465 0
[pid=7673] vsize: 50440
Current children cumulated CPU time (s) 788.83
Current children cumulated vsize (Kb) 52564

[startup+800.066 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 12481 0 2 0 79796 86 0 0 25 0 1 0 1841247271 51650560 12469 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 12610 12469 145 145 0 12465 0
[pid=7673] vsize: 50440
Current children cumulated CPU time (s) 798.84
Current children cumulated vsize (Kb) 52564

[startup+810.067 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 12481 0 2 0 80796 86 0 0 25 0 1 0 1841247271 51650560 12469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 12610 12469 145 145 0 12465 0
[pid=7673] vsize: 50440
Current children cumulated CPU time (s) 808.84
Current children cumulated vsize (Kb) 52564

[startup+820.068 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 12568 0 2 0 81794 88 0 0 25 0 1 0 1841247271 52006912 12556 4294967295 134512640 135094434 3221224432 3221223024 134557528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 12697 12556 145 145 0 12552 0
[pid=7673] vsize: 50788
Current children cumulated CPU time (s) 818.84
Current children cumulated vsize (Kb) 52912

[startup+830.068 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 12568 0 2 0 82794 88 0 0 25 0 1 0 1841247271 52006912 12556 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 12697 12556 145 145 0 12552 0
[pid=7673] vsize: 50788
Current children cumulated CPU time (s) 828.84
Current children cumulated vsize (Kb) 52912

[startup+840.069 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 12568 0 2 0 83793 89 0 0 25 0 1 0 1841247271 52006912 12556 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 12697 12556 145 145 0 12552 0
[pid=7673] vsize: 50788
Current children cumulated CPU time (s) 838.84
Current children cumulated vsize (Kb) 52912

[startup+850.07 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 12568 0 2 0 84792 90 0 0 25 0 1 0 1841247271 52006912 12556 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 12697 12556 145 145 0 12552 0
[pid=7673] vsize: 50788
Current children cumulated CPU time (s) 848.84
Current children cumulated vsize (Kb) 52912

[startup+860.069 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 12812 0 2 0 85789 91 0 0 25 0 1 0 1841247271 53022720 12800 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7673/statm): 12945 12800 145 145 0 12800 0
[pid=7673] vsize: 51780
Current children cumulated CPU time (s) 858.82
Current children cumulated vsize (Kb) 53904

[startup+870.071 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13438 0 2 0 86780 94 0 0 25 0 1 0 1841247271 55582720 13426 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13426 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 868.76
Current children cumulated vsize (Kb) 56404

[startup+880.072 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13438 0 2 0 87780 95 0 0 25 0 1 0 1841247271 55582720 13426 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13426 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 878.77
Current children cumulated vsize (Kb) 56404

[startup+890.072 s]
Raw data (loadavg): 1.00 1.01 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13438 0 2 0 88780 95 0 0 25 0 1 0 1841247271 55582720 13426 4294967295 134512640 135094434 3221224432 3221223024 134557199 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13426 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 888.77
Current children cumulated vsize (Kb) 56404

[startup+900.073 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 89780 95 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 898.77
Current children cumulated vsize (Kb) 56404

[startup+910.073 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 90780 95 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 908.77
Current children cumulated vsize (Kb) 56404

[startup+920.074 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 91780 95 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 918.77
Current children cumulated vsize (Kb) 56404

[startup+930.075 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 92780 95 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 928.77
Current children cumulated vsize (Kb) 56404

[startup+940.076 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 93781 95 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 938.78
Current children cumulated vsize (Kb) 56404

[startup+950.077 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 94781 96 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 948.79
Current children cumulated vsize (Kb) 56404

[startup+960.078 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 95781 96 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223024 134556908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 958.79
Current children cumulated vsize (Kb) 56404

[startup+970.079 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 96781 96 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 968.79
Current children cumulated vsize (Kb) 56404

[startup+980.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 97781 96 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 978.79
Current children cumulated vsize (Kb) 56404

[startup+990.081 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 98781 96 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 988.79
Current children cumulated vsize (Kb) 56404

[startup+1000.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 99782 96 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 998.8
Current children cumulated vsize (Kb) 56404

[startup+1010.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 100782 96 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 1008.8
Current children cumulated vsize (Kb) 56404

[startup+1020.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 101782 97 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 1018.81
Current children cumulated vsize (Kb) 56404

[startup+1030.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 102782 97 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 1028.81
Current children cumulated vsize (Kb) 56404

[startup+1040.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 103782 97 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 1038.81
Current children cumulated vsize (Kb) 56404

[startup+1050.08 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 104782 97 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 1048.81
Current children cumulated vsize (Kb) 56404

[startup+1060.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 105782 97 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 1058.81
Current children cumulated vsize (Kb) 56404

[startup+1070.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 106782 97 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 1068.81
Current children cumulated vsize (Kb) 56404

[startup+1080.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 107783 97 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 1078.82
Current children cumulated vsize (Kb) 56404

[startup+1090.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 108783 97 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 1088.82
Current children cumulated vsize (Kb) 56404

[startup+1100.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 109783 97 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 1098.82
Current children cumulated vsize (Kb) 56404

[startup+1110.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 110783 97 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 1108.82
Current children cumulated vsize (Kb) 56404

[startup+1120.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 111783 97 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223068 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 1118.82
Current children cumulated vsize (Kb) 56404

[startup+1130.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 112784 97 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 1128.83
Current children cumulated vsize (Kb) 56404

[startup+1140.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 113784 97 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 1138.83
Current children cumulated vsize (Kb) 56404

[startup+1150.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 114784 97 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 1148.83
Current children cumulated vsize (Kb) 56404

[startup+1160.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 115784 97 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223104 134555842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 1158.83
Current children cumulated vsize (Kb) 56404

[startup+1170.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 116784 97 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 1168.83
Current children cumulated vsize (Kb) 56404

[startup+1180.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 117784 98 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 1178.84
Current children cumulated vsize (Kb) 56404

[startup+1190.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 118785 98 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 1188.85
Current children cumulated vsize (Kb) 56404

[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 119785 98 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 1198.85
Current children cumulated vsize (Kb) 56404

[startup+1210.09 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 120785 98 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 1208.85
Current children cumulated vsize (Kb) 56404



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 1.00 1.00 3/57 7673
Raw data (/proc/7669/stat): 7669 (minisat+_script) S 7668 7669 5299 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841247266 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/7669/statm): 531 226 485 147 0 384 0
[pid=7669] vsize: 2124
Raw data (/proc/7673/stat): 7673 (minisat+_64-bit) R 7669 7669 5299 0 -1 0 13439 0 2 0 120785 98 0 0 25 0 1 0 1841247271 55582720 13427 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7673/statm): 13570 13427 145 145 0 13425 0
[pid=7673] vsize: 54280
Current children cumulated CPU time (s) 1208.85
Current children cumulated vsize (Kb) 56404

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

Child status: 0
Real time (s): 1210.13
CPU time (s): 1208.87
CPU user time (s): 1207.86
CPU system time (s): 1.00785
CPU usage (%): 99.896
Max. virtual memory (cumulated for all children) (Kb): 56404

Verifier Data

ERROR: no interpretation found !