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-chnl40_45_pb.cnf.cr.opb
MD5SUMdf5f31774bab40070962f7d0b16d093c
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 46
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.117981
Number of variables3600
Total number of constraints170
Number of constraints which are clauses90
Number of constraints which are cardinality constraints (but not clauses)80
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint40
Maximum length of a constraint45

Trace number 822

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        904864 kB
Buffers:         33564 kB
Cached:          69836 kB
SwapCached:        708 kB
Active:          53560 kB
Inactive:        52460 kB
HighTotal:      131008 kB
HighFree:        88172 kB
LowTotal:       903652 kB
LowFree:        816692 kB
SwapTotal:     2097136 kB
SwapFree:      2095936 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5740 kB
Slab:            18096 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 12:47:24 (client local time) WITH STATUS 0 IN 1208.53 SECONDS
stats: 2359 7 1208.53 0

Solver Data

c Parsing PB file...
c Converting 170 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................................................................
c ---[  79]---> BDD-cost:   87
c ---[  78]---> BDD-cost:   87
c ---[  77]---> BDD-cost:   87
c ---[  76]---> BDD-cost:   87
c ---[  75]---> BDD-cost:   87
c ---[  74]---> BDD-cost:   87
c ---[  73]---> BDD-cost:   87
c ---[  72]---> BDD-cost:   87
c ---[  71]---> BDD-cost:   87
c ---[  70]---> BDD-cost:   87
c ---[  69]---> BDD-cost:   87
c ---[  68]---> BDD-cost:   87
c ---[  67]---> BDD-cost:   87
c ---[  66]---> BDD-cost:   87
c ---[  65]---> BDD-cost:   87
c ---[  64]---> BDD-cost:   87
c ---[  63]---> BDD-cost:   87
c ---[  62]---> BDD-cost:   87
c ---[  61]---> BDD-cost:   87
c ---[  60]---> BDD-cost:   87
c ---[  59]---> BDD-cost:   87
c ---[  58]---> BDD-cost:   87
c ---[  57]---> BDD-cost:   87
c ---[  56]---> BDD-cost:   87
c ---[  55]---> BDD-cost:   87
c ---[  54]---> BDD-cost:   87
c ---[  53]---> BDD-cost:   87
c ---[  52]---> BDD-cost:   87
c ---[  51]---> BDD-cost:   87
c ---[  50]---> BDD-cost:   87
c ---[  49]---> BDD-cost:   87
c ---[  48]---> BDD-cost:   87
c ---[  47]---> BDD-cost:   87
c ---[  46]---> BDD-cost:   87
c ---[  45]---> BDD-cost:   87
c ---[  44]---> BDD-cost:   87
c ---[  43]---> BDD-cost:   87
c ---[  42]---> BDD-cost:   87
c ---[  41]---> BDD-cost:   87
c ---[  40]---> BDD-cost:   87
c ---[  39]---> BDD-cost:   87
c ---[  38]---> BDD-cost:   87
c ---[  37]---> BDD-cost:   87
c ---[  36]---> BDD-cost:   87
c ---[  35]---> BDD-cost:   87
c ---[  34]---> BDD-cost:   87
c ---[  33]---> BDD-cost:   87
c ---[  32]---> BDD-cost:   87
c ---[  31]---> BDD-cost:   87
c ---[  30]---> BDD-cost:   87
c ---[  29]---> BDD-cost:   87
c ---[  28]---> BDD-cost:   87
c ---[  27]---> BDD-cost:   87
c ---[  26]---> BDD-cost:   87
c ---[  25]---> BDD-cost:   87
c ---[  24]---> BDD-cost:   87
c ---[  23]---> BDD-cost:   87
c ---[  22]---> BDD-cost:   87
c ---[  21]---> BDD-cost:   87
c ---[  20]---> BDD-cost:   87
c ---[  19]---> BDD-cost:   87
c ---[  18]---> BDD-cost:   87
c ---[  17]---> BDD-cost:   87
c ---[  16]---> BDD-cost:   87
c ---[  15]---> BDD-cost:   87
c ---[  14]---> BDD-cost:   87
c ---[  13]---> BDD-cost:   87
c ---[  12]---> BDD-cost:   87
c ---[  11]---> BDD-cost:   87
c ---[  10]---> BDD-cost:   87
c ---[   9]---> BDD-cost:   87
c ---[   8]---> BDD-cost:   87
c ---[   7]---> BDD-cost:   87
c ---[   6]---> BDD-cost:   87
c ---[   5]---> BDD-cost:   87
c ---[   4]---> BDD-cost:   87
c ---[   3]---> BDD-cost:   87
c ---[   2]---> BDD-cost:   87
c ---[   1]---> BDD-cost:   87
c ---[   0]---> BDD-cost:   87
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   17370    48560 |    5790       0        0     nan |  0.000 % |
c |       100 |   17370    48560 |    6369     100    13678   136.8 |  0.758 % |
c |       250 |   17370    48560 |    7005     250    44432   177.7 |  0.758 % |
c |       476 |   17370    48560 |    7706     476    78934   165.8 |  0.758 % |
c |       815 |   17370    48560 |    8477     815   166719   204.6 |  0.758 % |
c |      1322 |   17370    48560 |    9324    1322   270822   204.9 |  0.758 % |
c |      2081 |   17370    48560 |   10257    2081   450367   216.4 |  0.758 % |
c |      3221 |   17370    48560 |   11283    3221   951336   295.4 |  0.758 % |
c |      4932 |   17370    48560 |   12411    4932  1382762   280.4 |  0.758 % |
c |      7494 |   17370    48560 |   13652    7494  2446849   326.5 |  0.758 % |
c |     11339 |   17370    48560 |   15017   11339  3685323   325.0 |  0.758 % |
c |     17106 |   17370    48560 |   16519   17106  6082234   355.6 |  0.758 % |
c |     25757 |   17370    48560 |   18171   17204  6681076   388.3 |  0.758 % |
c |     38731 |   17370    48560 |   19988   18866  7860099   416.6 |  0.758 % |
c |     58193 |   17370    48560 |   21987   13621  5958485   437.4 |  0.758 % |
c |     87388 |   17370    48560 |   24186   13260  6072457   458.0 |  0.758 % |
c |    131178 |   17370    48560 |   26604   24656 11587869   470.0 |  0.758 % |
c |    196863 |   17370    48560 |   29265   18059  8590700   475.7 |  0.758 % |

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/3699/stat): 3699 (minisat+_script) R 3698 3699 1333 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1783040796 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/3699/statm): 174 3 169 147 0 27 0
[pid=3699] 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=3700
New process pid=3701
New process pid=3702
One traced child (pid=3701) exited with status: 0
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
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=3702) exited with status: 0
One traced child (pid=3700) exited with status: 0
New process pid=3703
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc13/normalized-chnl40_45_pb.cnf.cr.opb

[startup+10.0057 s]
Raw data (loadavg): 0.94 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 2825 0 2 0 952 12 0 0 25 0 1 0 1783040801 12210176 2813 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 2981 2813 145 145 0 2836 0
[pid=3703] vsize: 11924
Current children cumulated CPU time (s) 9.65
Current children cumulated vsize (Kb) 14048

[startup+20.0064 s]
Raw data (loadavg): 0.95 0.97 0.91 1/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) T 3699 3699 1333 0 -1 0 4916 0 2 0 1924 24 0 0 25 0 1 0 1783040801 20787200 4904 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3703/statm): 5075 4904 145 145 0 4930 0
[pid=3703] vsize: 20300
Current children cumulated CPU time (s) 19.49
Current children cumulated vsize (Kb) 22424

[startup+30.007 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 6433 0 2 0 2903 32 0 0 20 0 1 0 1783040801 26984448 6421 4294967295 134512640 135094434 3221224432 3221223024 134556751 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 6588 6421 145 145 0 6443 0
[pid=3703] vsize: 26352
Current children cumulated CPU time (s) 29.36
Current children cumulated vsize (Kb) 28476

[startup+40.0077 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 7375 0 2 0 3890 38 0 0 25 0 1 0 1783040801 30924800 7363 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 7550 7363 145 145 0 7405 0
[pid=3703] vsize: 30200
Current children cumulated CPU time (s) 39.29
Current children cumulated vsize (Kb) 32324

[startup+50.0083 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 7375 0 2 0 4890 38 0 0 25 0 1 0 1783040801 30924800 7363 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 7550 7363 145 145 0 7405 0
[pid=3703] vsize: 30200
Current children cumulated CPU time (s) 49.29
Current children cumulated vsize (Kb) 32324

[startup+60.009 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 7530 0 2 0 5889 38 0 0 25 0 1 0 1783040801 31559680 7518 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 7705 7518 145 145 0 7560 0
[pid=3703] vsize: 30820
Current children cumulated CPU time (s) 59.28
Current children cumulated vsize (Kb) 32944

[startup+70.0097 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 8938 0 2 0 6870 45 0 0 25 0 1 0 1783040801 37335040 8926 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 9115 8926 145 145 0 8970 0
[pid=3703] vsize: 36460
Current children cumulated CPU time (s) 69.16
Current children cumulated vsize (Kb) 38584

[startup+80.0103 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 10455 0 2 0 7851 54 0 0 25 0 1 0 1783040801 43536384 10443 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 10629 10443 145 145 0 10484 0
[pid=3703] vsize: 42516
Current children cumulated CPU time (s) 79.06
Current children cumulated vsize (Kb) 44640

[startup+90.011 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 10809 0 2 0 8846 56 0 0 25 0 1 0 1783040801 44986368 10797 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 10983 10797 145 145 0 10838 0
[pid=3703] vsize: 43932
Current children cumulated CPU time (s) 89.03
Current children cumulated vsize (Kb) 46056

[startup+100.012 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 10809 0 2 0 9846 56 0 0 25 0 1 0 1783040801 44986368 10797 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 10983 10797 145 145 0 10838 0
[pid=3703] vsize: 43932
Current children cumulated CPU time (s) 99.03
Current children cumulated vsize (Kb) 46056

[startup+110.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 10809 0 2 0 10845 57 0 0 25 0 1 0 1783040801 44986368 10797 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3703/statm): 10983 10797 145 145 0 10838 0
[pid=3703] vsize: 43932
Current children cumulated CPU time (s) 109.03
Current children cumulated vsize (Kb) 46056

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) T 3699 3699 1333 0 -1 0 11102 0 2 0 11840 59 0 0 19 0 1 0 1783040801 46186496 11090 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3703/statm): 11276 11090 145 145 0 11131 0
[pid=3703] vsize: 45104
Current children cumulated CPU time (s) 119
Current children cumulated vsize (Kb) 47228

[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 11665 0 2 0 12831 62 0 0 25 0 1 0 1783040801 48496640 11653 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 11840 11653 145 145 0 11695 0
[pid=3703] vsize: 47360
Current children cumulated CPU time (s) 128.94
Current children cumulated vsize (Kb) 49484

[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 11666 0 2 0 13832 62 0 0 25 0 1 0 1783040801 48496640 11654 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 11840 11654 145 145 0 11695 0
[pid=3703] vsize: 47360
Current children cumulated CPU time (s) 138.95
Current children cumulated vsize (Kb) 49484

[startup+150.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 11668 0 2 0 14832 62 0 0 25 0 1 0 1783040801 48496640 11656 4294967295 134512640 135094434 3221224432 3221223104 134555683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 11840 11656 145 145 0 11695 0
[pid=3703] vsize: 47360
Current children cumulated CPU time (s) 148.95
Current children cumulated vsize (Kb) 49484

[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 11668 0 2 0 15832 62 0 0 25 0 1 0 1783040801 48496640 11656 4294967295 134512640 135094434 3221224432 3221223024 134556843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 11840 11656 145 145 0 11695 0
[pid=3703] vsize: 47360
Current children cumulated CPU time (s) 158.95
Current children cumulated vsize (Kb) 49484

[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 11668 0 2 0 16832 62 0 0 25 0 1 0 1783040801 48496640 11656 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 11840 11656 145 145 0 11695 0
[pid=3703] vsize: 47360
Current children cumulated CPU time (s) 168.95
Current children cumulated vsize (Kb) 49484

[startup+180.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 11668 0 2 0 17832 62 0 0 25 0 1 0 1783040801 48496640 11656 4294967295 134512640 135094434 3221224432 3221223024 134552003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 11840 11656 145 145 0 11695 0
[pid=3703] vsize: 47360
Current children cumulated CPU time (s) 178.95
Current children cumulated vsize (Kb) 49484

[startup+190.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 11668 0 2 0 18833 62 0 0 25 0 1 0 1783040801 48496640 11656 4294967295 134512640 135094434 3221224432 3221223024 134557020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 11840 11656 145 145 0 11695 0
[pid=3703] vsize: 47360
Current children cumulated CPU time (s) 188.96
Current children cumulated vsize (Kb) 49484

[startup+200.017 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 12240 0 2 0 19824 66 0 0 25 0 1 0 1783040801 50860032 12228 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 12417 12228 145 145 0 12272 0
[pid=3703] vsize: 49668
Current children cumulated CPU time (s) 198.91
Current children cumulated vsize (Kb) 51792

[startup+210.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 12337 0 2 0 20822 66 0 0 25 0 1 0 1783040801 51257344 12325 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3703/statm): 12514 12325 145 145 0 12369 0
[pid=3703] vsize: 50056
Current children cumulated CPU time (s) 208.89
Current children cumulated vsize (Kb) 52180

[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 12337 0 2 0 21822 66 0 0 25 0 1 0 1783040801 51257344 12325 4294967295 134512640 135094434 3221224432 3221223024 134556996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 12514 12325 145 145 0 12369 0
[pid=3703] vsize: 50056
Current children cumulated CPU time (s) 218.89
Current children cumulated vsize (Kb) 52180

[startup+230.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 12337 0 2 0 22822 66 0 0 25 0 1 0 1783040801 51257344 12325 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 12514 12325 145 145 0 12369 0
[pid=3703] vsize: 50056
Current children cumulated CPU time (s) 228.89
Current children cumulated vsize (Kb) 52180

[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 12946 0 2 0 23813 70 0 0 25 0 1 0 1783040801 53760000 12934 4294967295 134512640 135094434 3221224432 3221223024 134557119 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 13125 12934 145 145 0 12980 0
[pid=3703] vsize: 52500
Current children cumulated CPU time (s) 238.84
Current children cumulated vsize (Kb) 54624

[startup+250.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 13888 0 2 0 24802 75 0 0 25 0 1 0 1783040801 57626624 13876 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 14069 13876 145 145 0 13924 0
[pid=3703] vsize: 56276
Current children cumulated CPU time (s) 248.78
Current children cumulated vsize (Kb) 58400

[startup+260.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 13888 0 2 0 25802 75 0 0 25 0 1 0 1783040801 57626624 13876 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 14069 13876 145 145 0 13924 0
[pid=3703] vsize: 56276
Current children cumulated CPU time (s) 258.78
Current children cumulated vsize (Kb) 58400

[startup+270.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 13888 0 2 0 26802 75 0 0 25 0 1 0 1783040801 57626624 13876 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 14069 13876 145 145 0 13924 0
[pid=3703] vsize: 56276
Current children cumulated CPU time (s) 268.78
Current children cumulated vsize (Kb) 58400

[startup+280.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 13888 0 2 0 27803 75 0 0 25 0 1 0 1783040801 57626624 13876 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 14069 13876 145 145 0 13924 0
[pid=3703] vsize: 56276
Current children cumulated CPU time (s) 278.79
Current children cumulated vsize (Kb) 58400

[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 13888 0 2 0 28803 75 0 0 25 0 1 0 1783040801 57626624 13876 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 14069 13876 145 145 0 13924 0
[pid=3703] vsize: 56276
Current children cumulated CPU time (s) 288.79
Current children cumulated vsize (Kb) 58400

[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 13888 0 2 0 29803 75 0 0 25 0 1 0 1783040801 57626624 13876 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 14069 13876 145 145 0 13924 0
[pid=3703] vsize: 56276
Current children cumulated CPU time (s) 298.79
Current children cumulated vsize (Kb) 58400

[startup+310.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 13888 0 2 0 30803 75 0 0 25 0 1 0 1783040801 57626624 13876 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 14069 13876 145 145 0 13924 0
[pid=3703] vsize: 56276
Current children cumulated CPU time (s) 308.79
Current children cumulated vsize (Kb) 58400

[startup+320.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 13888 0 2 0 31804 75 0 0 25 0 1 0 1783040801 57626624 13876 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 14069 13876 145 145 0 13924 0
[pid=3703] vsize: 56276
Current children cumulated CPU time (s) 318.8
Current children cumulated vsize (Kb) 58400

[startup+330.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 13888 0 2 0 32804 75 0 0 25 0 1 0 1783040801 57626624 13876 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 14069 13876 145 145 0 13924 0
[pid=3703] vsize: 56276
Current children cumulated CPU time (s) 328.8
Current children cumulated vsize (Kb) 58400

[startup+340.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 14396 0 2 0 33797 79 0 0 25 0 1 0 1783040801 59719680 14384 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 14580 14384 145 145 0 14435 0
[pid=3703] vsize: 58320
Current children cumulated CPU time (s) 338.77
Current children cumulated vsize (Kb) 60444

[startup+350.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 14862 0 2 0 34788 82 0 0 25 0 1 0 1783040801 61636608 14850 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 15048 14850 145 145 0 14903 0
[pid=3703] vsize: 60192
Current children cumulated CPU time (s) 348.71
Current children cumulated vsize (Kb) 62316

[startup+360.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 15168 0 2 0 35783 84 0 0 25 0 1 0 1783040801 62889984 15156 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 15354 15156 145 145 0 15209 0
[pid=3703] vsize: 61416
Current children cumulated CPU time (s) 358.68
Current children cumulated vsize (Kb) 63540

[startup+370.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 15168 0 2 0 36783 84 0 0 25 0 1 0 1783040801 62889984 15156 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 15354 15156 145 145 0 15209 0
[pid=3703] vsize: 61416
Current children cumulated CPU time (s) 368.68
Current children cumulated vsize (Kb) 63540

[startup+380.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 15168 0 2 0 37783 84 0 0 25 0 1 0 1783040801 62889984 15156 4294967295 134512640 135094434 3221224432 3221223024 134557111 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 15354 15156 145 145 0 15209 0
[pid=3703] vsize: 61416
Current children cumulated CPU time (s) 378.68
Current children cumulated vsize (Kb) 63540

[startup+390.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 15168 0 2 0 38783 84 0 0 25 0 1 0 1783040801 62889984 15156 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 15354 15156 145 145 0 15209 0
[pid=3703] vsize: 61416
Current children cumulated CPU time (s) 388.68
Current children cumulated vsize (Kb) 63540

[startup+400.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 15170 0 2 0 39784 84 0 0 25 0 1 0 1783040801 62889984 15158 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 15354 15158 145 145 0 15209 0
[pid=3703] vsize: 61416
Current children cumulated CPU time (s) 398.69
Current children cumulated vsize (Kb) 63540

[startup+410.036 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 15170 0 2 0 40784 84 0 0 25 0 1 0 1783040801 62889984 15158 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 15354 15158 145 145 0 15209 0
[pid=3703] vsize: 61416
Current children cumulated CPU time (s) 408.69
Current children cumulated vsize (Kb) 63540

[startup+420.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 15170 0 2 0 41784 84 0 0 25 0 1 0 1783040801 62889984 15158 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 15354 15158 145 145 0 15209 0
[pid=3703] vsize: 61416
Current children cumulated CPU time (s) 418.69
Current children cumulated vsize (Kb) 63540

[startup+430.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 15170 0 2 0 42784 84 0 0 25 0 1 0 1783040801 62889984 15158 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 15354 15158 145 145 0 15209 0
[pid=3703] vsize: 61416
Current children cumulated CPU time (s) 428.69
Current children cumulated vsize (Kb) 63540

[startup+440.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 15170 0 2 0 43785 84 0 0 25 0 1 0 1783040801 62889984 15158 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 15354 15158 145 145 0 15209 0
[pid=3703] vsize: 61416
Current children cumulated CPU time (s) 438.7
Current children cumulated vsize (Kb) 63540

[startup+450.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 15170 0 2 0 44785 84 0 0 25 0 1 0 1783040801 62889984 15158 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 15354 15158 145 145 0 15209 0
[pid=3703] vsize: 61416
Current children cumulated CPU time (s) 448.7
Current children cumulated vsize (Kb) 63540

[startup+460.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 15170 0 2 0 45785 84 0 0 25 0 1 0 1783040801 62889984 15158 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 15354 15158 145 145 0 15209 0
[pid=3703] vsize: 61416
Current children cumulated CPU time (s) 458.7
Current children cumulated vsize (Kb) 63540

[startup+470.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 15170 0 2 0 46785 84 0 0 25 0 1 0 1783040801 62889984 15158 4294967295 134512640 135094434 3221224432 3221223104 134556236 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 15354 15158 145 145 0 15209 0
[pid=3703] vsize: 61416
Current children cumulated CPU time (s) 468.7
Current children cumulated vsize (Kb) 63540

[startup+480.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) T 3699 3699 1333 0 -1 0 15209 0 2 0 47785 85 0 0 25 0 1 0 1783040801 63049728 15197 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3703/statm): 15393 15197 145 145 0 15248 0
[pid=3703] vsize: 61572
Current children cumulated CPU time (s) 478.71
Current children cumulated vsize (Kb) 63696

[startup+490.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 15752 0 2 0 48776 88 0 0 25 0 1 0 1783040801 65277952 15740 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 15937 15740 145 145 0 15792 0
[pid=3703] vsize: 63748
Current children cumulated CPU time (s) 488.65
Current children cumulated vsize (Kb) 65872

[startup+500.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 15752 0 2 0 49776 88 0 0 25 0 1 0 1783040801 65277952 15740 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 15937 15740 145 145 0 15792 0
[pid=3703] vsize: 63748
Current children cumulated CPU time (s) 498.65
Current children cumulated vsize (Kb) 65872

[startup+510.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 15752 0 2 0 50776 88 0 0 25 0 1 0 1783040801 65277952 15740 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 15937 15740 145 145 0 15792 0
[pid=3703] vsize: 63748
Current children cumulated CPU time (s) 508.65
Current children cumulated vsize (Kb) 65872

[startup+520.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 15752 0 2 0 51776 88 0 0 25 0 1 0 1783040801 65277952 15740 4294967295 134512640 135094434 3221224432 3221223104 134556549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 15937 15740 145 145 0 15792 0
[pid=3703] vsize: 63748
Current children cumulated CPU time (s) 518.65
Current children cumulated vsize (Kb) 65872

[startup+530.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 15752 0 2 0 52777 88 0 0 25 0 1 0 1783040801 65277952 15740 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 15937 15740 145 145 0 15792 0
[pid=3703] vsize: 63748
Current children cumulated CPU time (s) 528.66
Current children cumulated vsize (Kb) 65872

[startup+540.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 16136 0 2 0 53771 90 0 0 25 0 1 0 1783040801 66846720 16124 4294967295 134512640 135094434 3221224432 3221223024 134556880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 16320 16124 145 145 0 16175 0
[pid=3703] vsize: 65280
Current children cumulated CPU time (s) 538.62
Current children cumulated vsize (Kb) 67404

[startup+550.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 17243 0 2 0 54758 97 0 0 25 0 1 0 1783040801 71372800 17231 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 17425 17231 145 145 0 17280 0
[pid=3703] vsize: 69700
Current children cumulated CPU time (s) 548.56
Current children cumulated vsize (Kb) 71824

[startup+560.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 17243 0 2 0 55758 97 0 0 25 0 1 0 1783040801 71372800 17231 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 17425 17231 145 145 0 17280 0
[pid=3703] vsize: 69700
Current children cumulated CPU time (s) 558.56
Current children cumulated vsize (Kb) 71824

[startup+570.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 17243 0 2 0 56758 97 0 0 25 0 1 0 1783040801 71372800 17231 4294967295 134512640 135094434 3221224432 3221223024 134557238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 17425 17231 145 145 0 17280 0
[pid=3703] vsize: 69700
Current children cumulated CPU time (s) 568.56
Current children cumulated vsize (Kb) 71824

[startup+580.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 17243 0 2 0 57758 97 0 0 25 0 1 0 1783040801 71372800 17231 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 17425 17231 145 145 0 17280 0
[pid=3703] vsize: 69700
Current children cumulated CPU time (s) 578.56
Current children cumulated vsize (Kb) 71824

[startup+590.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 17243 0 2 0 58758 97 0 0 25 0 1 0 1783040801 71372800 17231 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 17425 17231 145 145 0 17280 0
[pid=3703] vsize: 69700
Current children cumulated CPU time (s) 588.56
Current children cumulated vsize (Kb) 71824

[startup+600.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 17243 0 2 0 59759 97 0 0 25 0 1 0 1783040801 71372800 17231 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 17425 17231 145 145 0 17280 0
[pid=3703] vsize: 69700
Current children cumulated CPU time (s) 598.57
Current children cumulated vsize (Kb) 71824

[startup+610.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 17243 0 2 0 60759 97 0 0 25 0 1 0 1783040801 71372800 17231 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 17425 17231 145 145 0 17280 0
[pid=3703] vsize: 69700
Current children cumulated CPU time (s) 608.57
Current children cumulated vsize (Kb) 71824

[startup+620.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 17243 0 2 0 61759 97 0 0 25 0 1 0 1783040801 71372800 17231 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 17425 17231 145 145 0 17280 0
[pid=3703] vsize: 69700
Current children cumulated CPU time (s) 618.57
Current children cumulated vsize (Kb) 71824

[startup+630.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 17243 0 2 0 62759 97 0 0 25 0 1 0 1783040801 71372800 17231 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 17425 17231 145 145 0 17280 0
[pid=3703] vsize: 69700
Current children cumulated CPU time (s) 628.57
Current children cumulated vsize (Kb) 71824

[startup+640.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 17692 0 2 0 63753 100 0 0 25 0 1 0 1783040801 73216000 17680 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 17875 17680 145 145 0 17730 0
[pid=3703] vsize: 71500
Current children cumulated CPU time (s) 638.54
Current children cumulated vsize (Kb) 73624

[startup+650.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 17692 0 2 0 64753 100 0 0 25 0 1 0 1783040801 73216000 17680 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 17875 17680 145 145 0 17730 0
[pid=3703] vsize: 71500
Current children cumulated CPU time (s) 648.54
Current children cumulated vsize (Kb) 73624

[startup+660.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 17692 0 2 0 65754 100 0 0 25 0 1 0 1783040801 73216000 17680 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 17875 17680 145 145 0 17730 0
[pid=3703] vsize: 71500
Current children cumulated CPU time (s) 658.55
Current children cumulated vsize (Kb) 73624

[startup+670.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 17692 0 2 0 66754 100 0 0 25 0 1 0 1783040801 73216000 17680 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 17875 17680 145 145 0 17730 0
[pid=3703] vsize: 71500
Current children cumulated CPU time (s) 668.55
Current children cumulated vsize (Kb) 73624

[startup+680.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 17692 0 2 0 67754 100 0 0 25 0 1 0 1783040801 73216000 17680 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 17875 17680 145 145 0 17730 0
[pid=3703] vsize: 71500
Current children cumulated CPU time (s) 678.55
Current children cumulated vsize (Kb) 73624

[startup+690.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 17692 0 2 0 68754 100 0 0 25 0 1 0 1783040801 73216000 17680 4294967295 134512640 135094434 3221224432 3221223024 134556815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 17875 17680 145 145 0 17730 0
[pid=3703] vsize: 71500
Current children cumulated CPU time (s) 688.55
Current children cumulated vsize (Kb) 73624

[startup+700.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 17692 0 2 0 69755 100 0 0 25 0 1 0 1783040801 73216000 17680 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 17875 17680 145 145 0 17730 0
[pid=3703] vsize: 71500
Current children cumulated CPU time (s) 698.56
Current children cumulated vsize (Kb) 73624

[startup+710.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 17692 0 2 0 70755 100 0 0 25 0 1 0 1783040801 73216000 17680 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 17875 17680 145 145 0 17730 0
[pid=3703] vsize: 71500
Current children cumulated CPU time (s) 708.56
Current children cumulated vsize (Kb) 73624

[startup+720.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 17692 0 2 0 71755 100 0 0 25 0 1 0 1783040801 73216000 17680 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 17875 17680 145 145 0 17730 0
[pid=3703] vsize: 71500
Current children cumulated CPU time (s) 718.56
Current children cumulated vsize (Kb) 73624

[startup+730.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 17692 0 2 0 72755 100 0 0 25 0 1 0 1783040801 73216000 17680 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 17875 17680 145 145 0 17730 0
[pid=3703] vsize: 71500
Current children cumulated CPU time (s) 728.56
Current children cumulated vsize (Kb) 73624

[startup+740.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) T 3699 3699 1333 0 -1 0 18023 0 2 0 73749 104 0 0 25 0 1 0 1783040801 74571776 18011 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3703/statm): 18206 18011 145 145 0 18061 0
[pid=3703] vsize: 72824
Current children cumulated CPU time (s) 738.54
Current children cumulated vsize (Kb) 74948

[startup+750.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 18738 0 2 0 74737 108 0 0 25 0 1 0 1783040801 77516800 18726 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 18925 18726 145 145 0 18780 0
[pid=3703] vsize: 75700
Current children cumulated CPU time (s) 748.46
Current children cumulated vsize (Kb) 77824

[startup+760.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19315 0 2 0 75729 111 0 0 25 0 1 0 1783040801 79904768 19303 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19508 19303 145 145 0 19363 0
[pid=3703] vsize: 78032
Current children cumulated CPU time (s) 758.41
Current children cumulated vsize (Kb) 80156

[startup+770.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19545 0 2 0 76726 113 0 0 25 0 1 0 1783040801 80846848 19533 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19738 19533 145 145 0 19593 0
[pid=3703] vsize: 78952
Current children cumulated CPU time (s) 768.4
Current children cumulated vsize (Kb) 81076

[startup+780.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19545 0 2 0 77726 113 0 0 25 0 1 0 1783040801 80846848 19533 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19738 19533 145 145 0 19593 0
[pid=3703] vsize: 78952
Current children cumulated CPU time (s) 778.4
Current children cumulated vsize (Kb) 81076

[startup+790.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19545 0 2 0 78726 113 0 0 25 0 1 0 1783040801 80846848 19533 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19738 19533 145 145 0 19593 0
[pid=3703] vsize: 78952
Current children cumulated CPU time (s) 788.4
Current children cumulated vsize (Kb) 81076

[startup+800.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19545 0 2 0 79727 113 0 0 25 0 1 0 1783040801 80846848 19533 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19738 19533 145 145 0 19593 0
[pid=3703] vsize: 78952
Current children cumulated CPU time (s) 798.41
Current children cumulated vsize (Kb) 81076

[startup+810.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19545 0 2 0 80727 113 0 0 25 0 1 0 1783040801 80846848 19533 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19738 19533 145 145 0 19593 0
[pid=3703] vsize: 78952
Current children cumulated CPU time (s) 808.41
Current children cumulated vsize (Kb) 81076

[startup+820.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19545 0 2 0 81727 113 0 0 25 0 1 0 1783040801 80846848 19533 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19738 19533 145 145 0 19593 0
[pid=3703] vsize: 78952
Current children cumulated CPU time (s) 818.41
Current children cumulated vsize (Kb) 81076

[startup+830.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19545 0 2 0 82727 113 0 0 25 0 1 0 1783040801 80846848 19533 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19738 19533 145 145 0 19593 0
[pid=3703] vsize: 78952
Current children cumulated CPU time (s) 828.41
Current children cumulated vsize (Kb) 81076

[startup+840.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19545 0 2 0 83728 113 0 0 25 0 1 0 1783040801 80846848 19533 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19738 19533 145 145 0 19593 0
[pid=3703] vsize: 78952
Current children cumulated CPU time (s) 838.42
Current children cumulated vsize (Kb) 81076

[startup+850.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19545 0 2 0 84728 113 0 0 25 0 1 0 1783040801 80846848 19533 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19738 19533 145 145 0 19593 0
[pid=3703] vsize: 78952
Current children cumulated CPU time (s) 848.42
Current children cumulated vsize (Kb) 81076

[startup+860.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19564 0 2 0 85728 113 0 0 25 0 1 0 1783040801 80977920 19552 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19770 19552 145 145 0 19625 0
[pid=3703] vsize: 79080
Current children cumulated CPU time (s) 858.42
Current children cumulated vsize (Kb) 81204

[startup+870.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19566 0 2 0 86728 113 0 0 25 0 1 0 1783040801 80977920 19554 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19770 19554 145 145 0 19625 0
[pid=3703] vsize: 79080
Current children cumulated CPU time (s) 868.42
Current children cumulated vsize (Kb) 81204

[startup+880.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19742 0 2 0 87725 114 0 0 25 0 1 0 1783040801 81723392 19730 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19730 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 878.4
Current children cumulated vsize (Kb) 81932

[startup+890.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19742 0 2 0 88725 114 0 0 25 0 1 0 1783040801 81723392 19730 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19730 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 888.4
Current children cumulated vsize (Kb) 81932

[startup+900.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19742 0 2 0 89726 114 0 0 25 0 1 0 1783040801 81723392 19730 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19730 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 898.41
Current children cumulated vsize (Kb) 81932

[startup+910.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19742 0 2 0 90726 114 0 0 25 0 1 0 1783040801 81723392 19730 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19730 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 908.41
Current children cumulated vsize (Kb) 81932

[startup+920.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19742 0 2 0 91726 114 0 0 25 0 1 0 1783040801 81723392 19730 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19730 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 918.41
Current children cumulated vsize (Kb) 81932

[startup+930.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19742 0 2 0 92726 114 0 0 25 0 1 0 1783040801 81723392 19730 4294967295 134512640 135094434 3221224432 3221223024 134556975 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19730 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 928.41
Current children cumulated vsize (Kb) 81932

[startup+940.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19742 0 2 0 93726 114 0 0 25 0 1 0 1783040801 81723392 19730 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19730 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 938.41
Current children cumulated vsize (Kb) 81932

[startup+950.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19742 0 2 0 94726 114 0 0 25 0 1 0 1783040801 81723392 19730 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19730 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 948.41
Current children cumulated vsize (Kb) 81932

[startup+960.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19742 0 2 0 95727 114 0 0 25 0 1 0 1783040801 81723392 19730 4294967295 134512640 135094434 3221224432 3221223024 134556884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19730 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 958.42
Current children cumulated vsize (Kb) 81932

[startup+970.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19742 0 2 0 96727 114 0 0 25 0 1 0 1783040801 81723392 19730 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19730 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 968.42
Current children cumulated vsize (Kb) 81932

[startup+980.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19742 0 2 0 97727 114 0 0 25 0 1 0 1783040801 81723392 19730 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19730 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 978.42
Current children cumulated vsize (Kb) 81932

[startup+990.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19742 0 2 0 98728 114 0 0 25 0 1 0 1783040801 81723392 19730 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19730 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 988.43
Current children cumulated vsize (Kb) 81932

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19742 0 2 0 99728 114 0 0 25 0 1 0 1783040801 81723392 19730 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19730 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 998.43
Current children cumulated vsize (Kb) 81932

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19742 0 2 0 100728 114 0 0 25 0 1 0 1783040801 81723392 19730 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19730 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 1008.43
Current children cumulated vsize (Kb) 81932

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19742 0 2 0 101728 114 0 0 25 0 1 0 1783040801 81723392 19730 4294967295 134512640 135094434 3221224432 3221222992 134550329 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19730 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 1018.43
Current children cumulated vsize (Kb) 81932

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19742 0 2 0 102729 114 0 0 25 0 1 0 1783040801 81723392 19730 4294967295 134512640 135094434 3221224432 3221223104 134555755 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19730 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 1028.44
Current children cumulated vsize (Kb) 81932

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19743 0 2 0 103729 114 0 0 25 0 1 0 1783040801 81723392 19731 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19731 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 1038.44
Current children cumulated vsize (Kb) 81932

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19743 0 2 0 104729 114 0 0 25 0 1 0 1783040801 81723392 19731 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19731 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 1048.44
Current children cumulated vsize (Kb) 81932

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19743 0 2 0 105730 114 0 0 25 0 1 0 1783040801 81723392 19731 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19731 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 1058.45
Current children cumulated vsize (Kb) 81932

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19743 0 2 0 106730 114 0 0 25 0 1 0 1783040801 81723392 19731 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19731 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 1068.45
Current children cumulated vsize (Kb) 81932

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19743 0 2 0 107730 114 0 0 25 0 1 0 1783040801 81723392 19731 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19731 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 1078.45
Current children cumulated vsize (Kb) 81932

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19743 0 2 0 108730 114 0 0 25 0 1 0 1783040801 81723392 19731 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19731 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 1088.45
Current children cumulated vsize (Kb) 81932

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19743 0 2 0 109731 114 0 0 25 0 1 0 1783040801 81723392 19731 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19731 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 1098.46
Current children cumulated vsize (Kb) 81932

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19743 0 2 0 110731 114 0 0 25 0 1 0 1783040801 81723392 19731 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19731 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 1108.46
Current children cumulated vsize (Kb) 81932

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19743 0 2 0 111731 114 0 0 25 0 1 0 1783040801 81723392 19731 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19731 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 1118.46
Current children cumulated vsize (Kb) 81932

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19743 0 2 0 112731 114 0 0 25 0 1 0 1783040801 81723392 19731 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19731 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 1128.46
Current children cumulated vsize (Kb) 81932

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19743 0 2 0 113732 114 0 0 25 0 1 0 1783040801 81723392 19731 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19731 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 1138.47
Current children cumulated vsize (Kb) 81932

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19743 0 2 0 114732 114 0 0 25 0 1 0 1783040801 81723392 19731 4294967295 134512640 135094434 3221224432 3221223088 134557820 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19731 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 1148.47
Current children cumulated vsize (Kb) 81932

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19743 0 2 0 115732 114 0 0 25 0 1 0 1783040801 81723392 19731 4294967295 134512640 135094434 3221224432 3221223024 134557040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19731 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 1158.47
Current children cumulated vsize (Kb) 81932

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19743 0 2 0 116732 114 0 0 25 0 1 0 1783040801 81723392 19731 4294967295 134512640 135094434 3221224432 3221223024 134551463 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19731 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 1168.47
Current children cumulated vsize (Kb) 81932

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19743 0 2 0 117733 114 0 0 25 0 1 0 1783040801 81723392 19731 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19731 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 1178.48
Current children cumulated vsize (Kb) 81932

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19743 0 2 0 118733 114 0 0 25 0 1 0 1783040801 81723392 19731 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19731 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 1188.48
Current children cumulated vsize (Kb) 81932

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19743 0 2 0 119733 114 0 0 25 0 1 0 1783040801 81723392 19731 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19731 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 1198.48
Current children cumulated vsize (Kb) 81932

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19743 0 2 0 120734 114 0 0 25 0 1 0 1783040801 81723392 19731 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19731 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 1208.49
Current children cumulated vsize (Kb) 81932



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 3703
Raw data (/proc/3699/stat): 3699 (minisat+_script) S 3698 3699 1333 0 -1 0 289 239 0 0 0 0 0 1 16 0 1 0 1783040796 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3699/statm): 531 226 485 147 0 384 0
[pid=3699] vsize: 2124
Raw data (/proc/3703/stat): 3703 (minisat+_64-bit) R 3699 3699 1333 0 -1 0 19743 0 2 0 120734 114 0 0 25 0 1 0 1783040801 81723392 19731 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3703/statm): 19952 19731 145 145 0 19807 0
[pid=3703] vsize: 79808
Current children cumulated CPU time (s) 1208.49
Current children cumulated vsize (Kb) 81932

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

Child status: 0
Real time (s): 1210.14
CPU time (s): 1208.53
CPU user time (s): 1207.34
CPU system time (s): 1.18482
CPU usage (%): 99.8668
Max. virtual memory (cumulated for all children) (Kb): 81932

Verifier Data

ERROR: no interpretation found !