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-chnl35_45_pb.cnf.cr.opb
MD5SUM1f5fb3c191c2c77719f10f35e4f5f992
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.105983
Number of variables3150
Total number of constraints160
Number of constraints which are clauses90
Number of constraints which are cardinality constraints (but not clauses)70
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint35
Maximum length of a constraint45

Trace number 900

Launcher Data

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        948964 kB
Buffers:         31812 kB
Cached:          30388 kB
SwapCached:       1040 kB
Active:          19004 kB
Inactive:        45856 kB
HighTotal:      131008 kB
HighFree:        97104 kB
LowTotal:       903652 kB
LowFree:        851860 kB
SwapTotal:     2097136 kB
SwapFree:      2095568 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5696 kB
Slab:            15076 kB
Committed_AS:    72360 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 12:59:30 (client local time) WITH STATUS 0 IN 1208.53 SECONDS
stats: 2398 7 1208.53 0

Solver Data

c Parsing PB file...
c Converting 160 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................................................................
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 |   15210    42490 |    5070       0        0     nan |  0.000 % |
c |       101 |   15210    42490 |    5577     101    13595   134.6 |  0.758 % |
c |       253 |   15210    42490 |    6134     253    41155   162.7 |  0.758 % |
c |       480 |   15210    42490 |    6748     480    87737   182.8 |  0.758 % |
c |       819 |   15210    42490 |    7422     819   152105   185.7 |  0.758 % |
c |      1328 |   15210    42490 |    8165    1328   233504   175.8 |  0.758 % |
c |      2088 |   15210    42490 |    8981    2088   381775   182.8 |  0.758 % |
c |      3227 |   15210    42490 |    9879    3227   722388   223.9 |  0.758 % |
c |      4937 |   15210    42490 |   10867    4937  1190498   241.1 |  0.758 % |
c |      7499 |   15210    42490 |   11954    7499  1875349   250.1 |  0.758 % |
c |     11348 |   15210    42490 |   13150   11348  2998324   264.2 |  0.758 % |
c |     17114 |   15210    42490 |   14465    8729  2872831   329.1 |  0.758 % |
c |     25764 |   15210    42490 |   15911   17379  5578930   321.0 |  0.758 % |
c |     38739 |   15210    42490 |   17503   11971  5497632   459.2 |  0.758 % |
c |     58200 |   15210    42490 |   19253   10805  3533507   327.0 |  0.758 % |
c |     87395 |   15210    42490 |   21178   25607  7805831   304.8 |  0.758 % |
c |    131185 |   15210    42490 |   23296   15826  7858090   496.5 |  0.758 % |
c |    196870 |   15210    42490 |   25626   23958 10195199   425.5 |  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/9610/stat): 9610 (minisat+_script) R 9609 9610 6872 0 -1 0 18 0 1 0 0 0 0 0 21 0 1 0 1783106121 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/9610/statm): 174 3 169 147 0 27 0
[pid=9610] 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=9611
New process pid=9612
New process pid=9613
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
One traced child (pid=9612) exited with status: 0
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=9613) exited with status: 0
One traced child (pid=9611) exited with status: 0
New process pid=9614
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc2/normalized-chnl35_45_pb.cnf.cr.opb

[startup+10.0205 s]
Raw data (loadavg): 0.93 0.95 0.90 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 2668 0 2 0 946 14 0 0 25 0 1 0 1783106131 11526144 2653 4294967295 134512640 135094434 3221224432 3221223024 134557396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 2814 2653 145 145 0 2669 0
[pid=9614] vsize: 11256
Current children cumulated CPU time (s) 9.61
Current children cumulated vsize (Kb) 13380

[startup+20.0212 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) T 9610 9610 6872 0 -1 0 4463 0 2 0 1919 24 0 0 25 0 1 0 1783106131 18894848 4448 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/9614/statm): 4613 4448 145 145 0 4468 0
[pid=9614] vsize: 18452
Current children cumulated CPU time (s) 19.44
Current children cumulated vsize (Kb) 20576

[startup+30.0229 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 5871 0 2 0 2897 34 0 0 25 0 1 0 1783106131 24649728 5856 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9614/statm): 6018 5856 145 145 0 5873 0
[pid=9614] vsize: 24072
Current children cumulated CPU time (s) 29.32
Current children cumulated vsize (Kb) 26196

[startup+40.0237 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 6099 0 2 0 3892 37 0 0 25 0 1 0 1783106131 25649152 6084 4294967295 134512640 135094434 3221224432 3221223104 134556242 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9614/statm): 6262 6084 145 145 0 6117 0
[pid=9614] vsize: 25048
Current children cumulated CPU time (s) 39.3
Current children cumulated vsize (Kb) 27172

[startup+50.0244 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 6099 0 2 0 4891 37 0 0 25 0 1 0 1783106131 25649152 6084 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9614/statm): 6262 6084 145 145 0 6117 0
[pid=9614] vsize: 25048
Current children cumulated CPU time (s) 49.29
Current children cumulated vsize (Kb) 27172

[startup+60.0251 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 6825 0 2 0 5880 40 0 0 25 0 1 0 1783106131 28643328 6810 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9614/statm): 6993 6810 145 145 0 6848 0
[pid=9614] vsize: 27972
Current children cumulated CPU time (s) 59.21
Current children cumulated vsize (Kb) 30096

[startup+70.0257 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 6825 0 2 0 6880 40 0 0 25 0 1 0 1783106131 28643328 6810 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 6993 6810 145 145 0 6848 0
[pid=9614] vsize: 27972
Current children cumulated CPU time (s) 69.21
Current children cumulated vsize (Kb) 30096

[startup+80.0274 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 7243 0 2 0 7874 43 0 0 25 0 1 0 1783106131 30359552 7228 4294967295 134512640 135094434 3221224432 3221223104 134556242 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 7412 7228 145 145 0 7267 0
[pid=9614] vsize: 29648
Current children cumulated CPU time (s) 79.18
Current children cumulated vsize (Kb) 31772

[startup+90.0281 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 8225 0 2 0 8860 48 0 0 25 0 1 0 1783106131 34390016 8210 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 8396 8210 145 145 0 8251 0
[pid=9614] vsize: 33584
Current children cumulated CPU time (s) 89.09
Current children cumulated vsize (Kb) 35708

[startup+100.029 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 8636 0 2 0 9855 50 0 0 25 0 1 0 1783106131 36085760 8621 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 8810 8621 145 145 0 8665 0
[pid=9614] vsize: 35240
Current children cumulated CPU time (s) 99.06
Current children cumulated vsize (Kb) 37364

[startup+110.031 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 8636 0 2 0 10855 50 0 0 25 0 1 0 1783106131 36085760 8621 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 8810 8621 145 145 0 8665 0
[pid=9614] vsize: 35240
Current children cumulated CPU time (s) 109.06
Current children cumulated vsize (Kb) 37364

[startup+120.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 8753 0 2 0 11854 51 0 0 25 0 1 0 1783106131 36573184 8738 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 8929 8738 145 145 0 8784 0
[pid=9614] vsize: 35716
Current children cumulated CPU time (s) 119.06
Current children cumulated vsize (Kb) 37840

[startup+130.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 9718 0 2 0 12839 57 0 0 25 0 1 0 1783106131 40525824 9703 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 9894 9703 145 145 0 9749 0
[pid=9614] vsize: 39576
Current children cumulated CPU time (s) 128.97
Current children cumulated vsize (Kb) 41700

[startup+140.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10177 0 2 0 13831 60 0 0 25 0 1 0 1783106131 42418176 10162 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10356 10162 145 145 0 10211 0
[pid=9614] vsize: 41424
Current children cumulated CPU time (s) 138.92
Current children cumulated vsize (Kb) 43548

[startup+150.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10179 0 2 0 14831 61 0 0 25 0 1 0 1783106131 42418176 10164 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10356 10164 145 145 0 10211 0
[pid=9614] vsize: 41424
Current children cumulated CPU time (s) 148.93
Current children cumulated vsize (Kb) 43548

[startup+160.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10180 0 2 0 15831 61 0 0 25 0 1 0 1783106131 42418176 10165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10356 10165 145 145 0 10211 0
[pid=9614] vsize: 41424
Current children cumulated CPU time (s) 158.93
Current children cumulated vsize (Kb) 43548

[startup+170.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10181 0 2 0 16831 61 0 0 25 0 1 0 1783106131 42418176 10166 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10356 10166 145 145 0 10211 0
[pid=9614] vsize: 41424
Current children cumulated CPU time (s) 168.93
Current children cumulated vsize (Kb) 43548

[startup+180.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10181 0 2 0 17831 61 0 0 25 0 1 0 1783106131 42418176 10166 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10356 10166 145 145 0 10211 0
[pid=9614] vsize: 41424
Current children cumulated CPU time (s) 178.93
Current children cumulated vsize (Kb) 43548

[startup+190.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10181 0 2 0 18832 61 0 0 25 0 1 0 1783106131 42418176 10166 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10356 10166 145 145 0 10211 0
[pid=9614] vsize: 41424
Current children cumulated CPU time (s) 188.94
Current children cumulated vsize (Kb) 43548

[startup+200.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10181 0 2 0 19832 61 0 0 25 0 1 0 1783106131 42418176 10166 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10356 10166 145 145 0 10211 0
[pid=9614] vsize: 41424
Current children cumulated CPU time (s) 198.94
Current children cumulated vsize (Kb) 43548

[startup+210.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10184 0 2 0 20832 61 0 0 25 0 1 0 1783106131 42418176 10169 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10356 10169 145 145 0 10211 0
[pid=9614] vsize: 41424
Current children cumulated CPU time (s) 208.94
Current children cumulated vsize (Kb) 43548

[startup+220.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10186 0 2 0 21832 61 0 0 25 0 1 0 1783106131 42418176 10171 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10356 10171 145 145 0 10211 0
[pid=9614] vsize: 41424
Current children cumulated CPU time (s) 218.94
Current children cumulated vsize (Kb) 43548

[startup+230.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10186 0 2 0 22832 61 0 0 25 0 1 0 1783106131 42418176 10171 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10356 10171 145 145 0 10211 0
[pid=9614] vsize: 41424
Current children cumulated CPU time (s) 228.94
Current children cumulated vsize (Kb) 43548

[startup+240.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10186 0 2 0 23832 61 0 0 25 0 1 0 1783106131 42418176 10171 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10356 10171 145 145 0 10211 0
[pid=9614] vsize: 41424
Current children cumulated CPU time (s) 238.94
Current children cumulated vsize (Kb) 43548

[startup+250.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10186 0 2 0 24833 61 0 0 25 0 1 0 1783106131 42418176 10171 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10356 10171 145 145 0 10211 0
[pid=9614] vsize: 41424
Current children cumulated CPU time (s) 248.95
Current children cumulated vsize (Kb) 43548

[startup+260.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10186 0 2 0 25833 61 0 0 25 0 1 0 1783106131 42418176 10171 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10356 10171 145 145 0 10211 0
[pid=9614] vsize: 41424
Current children cumulated CPU time (s) 258.95
Current children cumulated vsize (Kb) 43548

[startup+270.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10186 0 2 0 26833 61 0 0 25 0 1 0 1783106131 42418176 10171 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10356 10171 145 145 0 10211 0
[pid=9614] vsize: 41424
Current children cumulated CPU time (s) 268.95
Current children cumulated vsize (Kb) 43548

[startup+280.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10186 0 2 0 27833 61 0 0 25 0 1 0 1783106131 42418176 10171 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10356 10171 145 145 0 10211 0
[pid=9614] vsize: 41424
Current children cumulated CPU time (s) 278.95
Current children cumulated vsize (Kb) 43548

[startup+290.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10186 0 2 0 28834 61 0 0 25 0 1 0 1783106131 42418176 10171 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10356 10171 145 145 0 10211 0
[pid=9614] vsize: 41424
Current children cumulated CPU time (s) 288.96
Current children cumulated vsize (Kb) 43548

[startup+300.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10231 0 2 0 29833 61 0 0 25 0 1 0 1783106131 42602496 10216 4294967295 134512640 135094434 3221224432 3221223024 134556791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10401 10216 145 145 0 10256 0
[pid=9614] vsize: 41604
Current children cumulated CPU time (s) 298.95
Current children cumulated vsize (Kb) 43728

[startup+310.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10231 0 2 0 30833 62 0 0 25 0 1 0 1783106131 42602496 10216 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10401 10216 145 145 0 10256 0
[pid=9614] vsize: 41604
Current children cumulated CPU time (s) 308.96
Current children cumulated vsize (Kb) 43728

[startup+320.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10231 0 2 0 31833 62 0 0 25 0 1 0 1783106131 42602496 10216 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10401 10216 145 145 0 10256 0
[pid=9614] vsize: 41604
Current children cumulated CPU time (s) 318.96
Current children cumulated vsize (Kb) 43728

[startup+330.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10430 0 2 0 32830 63 0 0 25 0 1 0 1783106131 43417600 10415 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10600 10415 145 145 0 10455 0
[pid=9614] vsize: 42400
Current children cumulated CPU time (s) 328.94
Current children cumulated vsize (Kb) 44524

[startup+340.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10512 0 2 0 33828 65 0 0 25 0 1 0 1783106131 43753472 10497 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10682 10497 145 145 0 10537 0
[pid=9614] vsize: 42728
Current children cumulated CPU time (s) 338.94
Current children cumulated vsize (Kb) 44852

[startup+350.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10512 0 2 0 34828 65 0 0 25 0 1 0 1783106131 43753472 10497 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10682 10497 145 145 0 10537 0
[pid=9614] vsize: 42728
Current children cumulated CPU time (s) 348.94
Current children cumulated vsize (Kb) 44852

[startup+360.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10512 0 2 0 35828 66 0 0 25 0 1 0 1783106131 43753472 10497 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10682 10497 145 145 0 10537 0
[pid=9614] vsize: 42728
Current children cumulated CPU time (s) 358.95
Current children cumulated vsize (Kb) 44852

[startup+370.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10512 0 2 0 36828 66 0 0 25 0 1 0 1783106131 43753472 10497 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10682 10497 145 145 0 10537 0
[pid=9614] vsize: 42728
Current children cumulated CPU time (s) 368.95
Current children cumulated vsize (Kb) 44852

[startup+380.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 10770 0 2 0 37823 68 0 0 25 0 1 0 1783106131 44814336 10755 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 10941 10755 145 145 0 10796 0
[pid=9614] vsize: 43764
Current children cumulated CPU time (s) 378.92
Current children cumulated vsize (Kb) 45888

[startup+390.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 11320 0 2 0 38813 72 0 0 25 0 1 0 1783106131 47095808 11305 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 11498 11305 145 145 0 11353 0
[pid=9614] vsize: 45992
Current children cumulated CPU time (s) 388.86
Current children cumulated vsize (Kb) 48116

[startup+400.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 11932 0 2 0 39803 76 0 0 25 0 1 0 1783106131 49610752 11917 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 12112 11917 145 145 0 11967 0
[pid=9614] vsize: 48448
Current children cumulated CPU time (s) 398.8
Current children cumulated vsize (Kb) 50572

[startup+410.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 12559 0 2 0 40793 81 0 0 25 0 1 0 1783106131 52178944 12544 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 12739 12544 145 145 0 12594 0
[pid=9614] vsize: 50956
Current children cumulated CPU time (s) 408.75
Current children cumulated vsize (Kb) 53080

[startup+420.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 13116 0 2 0 41785 85 0 0 25 0 1 0 1783106131 54476800 13101 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 13300 13101 145 145 0 13155 0
[pid=9614] vsize: 53200
Current children cumulated CPU time (s) 418.71
Current children cumulated vsize (Kb) 55324

[startup+430.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 13718 0 2 0 42775 89 0 0 25 0 1 0 1783106131 56950784 13703 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 13904 13703 145 145 0 13759 0
[pid=9614] vsize: 55616
Current children cumulated CPU time (s) 428.65
Current children cumulated vsize (Kb) 57740

[startup+440.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 14260 0 2 0 43765 93 0 0 25 0 1 0 1783106131 59195392 14245 4294967295 134512640 135094434 3221224432 3221223024 134551469 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 14452 14245 145 145 0 14307 0
[pid=9614] vsize: 57808
Current children cumulated CPU time (s) 438.59
Current children cumulated vsize (Kb) 59932

[startup+450.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 14260 0 2 0 44765 93 0 0 25 0 1 0 1783106131 59195392 14245 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 14452 14245 145 145 0 14307 0
[pid=9614] vsize: 57808
Current children cumulated CPU time (s) 448.59
Current children cumulated vsize (Kb) 59932

[startup+460.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 14260 0 2 0 45766 93 0 0 25 0 1 0 1783106131 59195392 14245 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 14452 14245 145 145 0 14307 0
[pid=9614] vsize: 57808
Current children cumulated CPU time (s) 458.6
Current children cumulated vsize (Kb) 59932

[startup+470.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 14261 0 2 0 46766 93 0 0 25 0 1 0 1783106131 59195392 14246 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 14452 14246 145 145 0 14307 0
[pid=9614] vsize: 57808
Current children cumulated CPU time (s) 468.6
Current children cumulated vsize (Kb) 59932

[startup+480.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 14273 0 2 0 47766 93 0 0 25 0 1 0 1783106131 59260928 14258 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 14468 14258 145 145 0 14323 0
[pid=9614] vsize: 57872
Current children cumulated CPU time (s) 478.6
Current children cumulated vsize (Kb) 59996

[startup+490.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 14285 0 2 0 48766 93 0 0 25 0 1 0 1783106131 59326464 14270 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 14484 14270 145 145 0 14339 0
[pid=9614] vsize: 57936
Current children cumulated CPU time (s) 488.6
Current children cumulated vsize (Kb) 60060

[startup+500.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 14298 0 2 0 49766 93 0 0 25 0 1 0 1783106131 59392000 14283 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 14500 14283 145 145 0 14355 0
[pid=9614] vsize: 58000
Current children cumulated CPU time (s) 498.6
Current children cumulated vsize (Kb) 60124

[startup+510.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 14300 0 2 0 50766 93 0 0 25 0 1 0 1783106131 59392000 14285 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 14500 14285 145 145 0 14355 0
[pid=9614] vsize: 58000
Current children cumulated CPU time (s) 508.6
Current children cumulated vsize (Kb) 60124

[startup+520.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 14313 0 2 0 51766 94 0 0 25 0 1 0 1783106131 59457536 14298 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 14516 14298 145 145 0 14371 0
[pid=9614] vsize: 58064
Current children cumulated CPU time (s) 518.61
Current children cumulated vsize (Kb) 60188

[startup+530.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 14792 0 2 0 52758 97 0 0 25 0 1 0 1783106131 61415424 14777 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 14994 14777 145 145 0 14849 0
[pid=9614] vsize: 59976
Current children cumulated CPU time (s) 528.56
Current children cumulated vsize (Kb) 62100

[startup+540.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 15280 0 2 0 53750 101 0 0 25 0 1 0 1783106131 63418368 15265 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 15483 15265 145 145 0 15338 0
[pid=9614] vsize: 61932
Current children cumulated CPU time (s) 538.52
Current children cumulated vsize (Kb) 64056

[startup+550.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 15802 0 2 0 54742 104 0 0 25 0 1 0 1783106131 65552384 15787 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 16004 15787 145 145 0 15859 0
[pid=9614] vsize: 64016
Current children cumulated CPU time (s) 548.47
Current children cumulated vsize (Kb) 66140

[startup+560.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16497 0 2 0 55731 108 0 0 25 0 1 0 1783106131 68403200 16482 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 16700 16482 145 145 0 16555 0
[pid=9614] vsize: 66800
Current children cumulated CPU time (s) 558.4
Current children cumulated vsize (Kb) 68924

[startup+570.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16924 0 2 0 56724 111 0 0 25 0 1 0 1783106131 70156288 16909 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16909 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 568.36
Current children cumulated vsize (Kb) 70636

[startup+580.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16924 0 2 0 57724 111 0 0 25 0 1 0 1783106131 70156288 16909 4294967295 134512640 135094434 3221224432 3221223104 134555570 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16909 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 578.36
Current children cumulated vsize (Kb) 70636

[startup+590.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16924 0 2 0 58724 111 0 0 25 0 1 0 1783106131 70156288 16909 4294967295 134512640 135094434 3221224432 3221223104 134555842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16909 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 588.36
Current children cumulated vsize (Kb) 70636

[startup+600.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16924 0 2 0 59724 111 0 0 25 0 1 0 1783106131 70156288 16909 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16909 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 598.36
Current children cumulated vsize (Kb) 70636

[startup+610.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 60724 111 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 608.36
Current children cumulated vsize (Kb) 70636

[startup+620.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 61724 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 618.37
Current children cumulated vsize (Kb) 70636

[startup+630.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 62725 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 628.38
Current children cumulated vsize (Kb) 70636

[startup+640.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 63725 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 638.38
Current children cumulated vsize (Kb) 70636

[startup+650.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 64725 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 648.38
Current children cumulated vsize (Kb) 70636

[startup+660.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 65725 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 658.38
Current children cumulated vsize (Kb) 70636

[startup+670.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 66726 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 668.39
Current children cumulated vsize (Kb) 70636

[startup+680.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 67726 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 678.39
Current children cumulated vsize (Kb) 70636

[startup+690.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 68726 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 688.39
Current children cumulated vsize (Kb) 70636

[startup+700.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 69726 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 698.39
Current children cumulated vsize (Kb) 70636

[startup+710.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 70726 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 708.39
Current children cumulated vsize (Kb) 70636

[startup+720.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 71726 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 718.39
Current children cumulated vsize (Kb) 70636

[startup+730.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 72727 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 728.4
Current children cumulated vsize (Kb) 70636

[startup+740.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 73727 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 738.4
Current children cumulated vsize (Kb) 70636

[startup+750.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 74727 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 748.4
Current children cumulated vsize (Kb) 70636

[startup+760.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 75727 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 758.4
Current children cumulated vsize (Kb) 70636

[startup+770.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 76727 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 768.4
Current children cumulated vsize (Kb) 70636

[startup+780.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 77728 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 778.41
Current children cumulated vsize (Kb) 70636

[startup+790.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 78728 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 788.41
Current children cumulated vsize (Kb) 70636

[startup+800.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 79728 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223024 134551448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 798.41
Current children cumulated vsize (Kb) 70636

[startup+810.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 80728 112 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 808.41
Current children cumulated vsize (Kb) 70636

[startup+820.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 81728 113 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 818.42
Current children cumulated vsize (Kb) 70636

[startup+830.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 82729 113 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 828.43
Current children cumulated vsize (Kb) 70636

[startup+840.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 83729 113 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 838.43
Current children cumulated vsize (Kb) 70636

[startup+850.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 84729 113 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 848.43
Current children cumulated vsize (Kb) 70636

[startup+860.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 85729 113 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 858.43
Current children cumulated vsize (Kb) 70636

[startup+870.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 86730 113 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 868.44
Current children cumulated vsize (Kb) 70636

[startup+880.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 87730 113 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 878.44
Current children cumulated vsize (Kb) 70636

[startup+890.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 88730 113 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 888.44
Current children cumulated vsize (Kb) 70636

[startup+900.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 89730 113 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 898.44
Current children cumulated vsize (Kb) 70636

[startup+910.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16925 0 2 0 90730 113 0 0 25 0 1 0 1783106131 70156288 16910 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16910 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 908.44
Current children cumulated vsize (Kb) 70636

[startup+920.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16927 0 2 0 91730 113 0 0 25 0 1 0 1783106131 70156288 16912 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16912 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 918.44
Current children cumulated vsize (Kb) 70636

[startup+930.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16927 0 2 0 92730 113 0 0 25 0 1 0 1783106131 70156288 16912 4294967295 134512640 135094434 3221224432 3221223088 134558172 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16912 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 928.44
Current children cumulated vsize (Kb) 70636

[startup+940.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16928 0 2 0 93729 114 0 0 25 0 1 0 1783106131 70156288 16913 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16913 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 938.44
Current children cumulated vsize (Kb) 70636

[startup+950.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16928 0 2 0 94728 115 0 0 25 0 1 0 1783106131 70156288 16913 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9614/statm): 17128 16913 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 948.44
Current children cumulated vsize (Kb) 70636

[startup+960.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 95727 115 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 958.43
Current children cumulated vsize (Kb) 70636

[startup+970.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 96727 115 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 968.43
Current children cumulated vsize (Kb) 70636

[startup+980.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 97727 115 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 978.43
Current children cumulated vsize (Kb) 70636

[startup+990.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 98727 115 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 988.43
Current children cumulated vsize (Kb) 70636

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 99727 116 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 998.44
Current children cumulated vsize (Kb) 70636

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 100727 116 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 1008.44
Current children cumulated vsize (Kb) 70636

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 101727 116 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 1018.44
Current children cumulated vsize (Kb) 70636

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 102728 116 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 1028.45
Current children cumulated vsize (Kb) 70636

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 103728 116 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 1038.45
Current children cumulated vsize (Kb) 70636

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 104728 116 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 1048.45
Current children cumulated vsize (Kb) 70636

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 105728 116 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 1058.45
Current children cumulated vsize (Kb) 70636

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 106728 116 0 0 25 0 1 0 1783106131 70156288 16914 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17128 16914 145 145 0 16983 0
[pid=9614] vsize: 68512
Current children cumulated CPU time (s) 1068.45
Current children cumulated vsize (Kb) 70636

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 107728 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0
[pid=9614] vsize: 68312
Current children cumulated CPU time (s) 1078.46
Current children cumulated vsize (Kb) 70436

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 108729 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223024 134556906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0
[pid=9614] vsize: 68312
Current children cumulated CPU time (s) 1088.47
Current children cumulated vsize (Kb) 70436

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 109729 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0
[pid=9614] vsize: 68312
Current children cumulated CPU time (s) 1098.47
Current children cumulated vsize (Kb) 70436

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 110729 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223024 134551868 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0
[pid=9614] vsize: 68312
Current children cumulated CPU time (s) 1108.47
Current children cumulated vsize (Kb) 70436

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 111729 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0
[pid=9614] vsize: 68312
Current children cumulated CPU time (s) 1118.47
Current children cumulated vsize (Kb) 70436

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 112729 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0
[pid=9614] vsize: 68312
Current children cumulated CPU time (s) 1128.47
Current children cumulated vsize (Kb) 70436

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 113730 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0
[pid=9614] vsize: 68312
Current children cumulated CPU time (s) 1138.48
Current children cumulated vsize (Kb) 70436

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 114730 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223104 134556192 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0
[pid=9614] vsize: 68312
Current children cumulated CPU time (s) 1148.48
Current children cumulated vsize (Kb) 70436

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 115730 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0
[pid=9614] vsize: 68312
Current children cumulated CPU time (s) 1158.48
Current children cumulated vsize (Kb) 70436

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 116730 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0
[pid=9614] vsize: 68312
Current children cumulated CPU time (s) 1168.48
Current children cumulated vsize (Kb) 70436

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 117730 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0
[pid=9614] vsize: 68312
Current children cumulated CPU time (s) 1178.48
Current children cumulated vsize (Kb) 70436

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 118730 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0
[pid=9614] vsize: 68312
Current children cumulated CPU time (s) 1188.48
Current children cumulated vsize (Kb) 70436

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 119731 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223104 134556329 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0
[pid=9614] vsize: 68312
Current children cumulated CPU time (s) 1198.49
Current children cumulated vsize (Kb) 70436

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 120731 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0
[pid=9614] vsize: 68312
Current children cumulated CPU time (s) 1208.49
Current children cumulated vsize (Kb) 70436



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9614
Raw data (/proc/9610/stat): 9610 (minisat+_script) S 9609 9610 6872 0 -1 0 276 238 13 1 0 1 0 0 20 0 1 0 1783106121 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9610/statm): 531 226 485 147 0 384 0
[pid=9610] vsize: 2124
Raw data (/proc/9614/stat): 9614 (minisat+_64-bit) R 9610 9610 6872 0 -1 0 16929 0 2 0 120731 117 0 0 25 0 1 0 1783106131 69951488 16864 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9614/statm): 17078 16864 145 145 0 16933 0
[pid=9614] vsize: 68312
Current children cumulated CPU time (s) 1208.49
Current children cumulated vsize (Kb) 70436

Sending SIGTERM to -9610
Sleeping 2 seconds
One traced child (pid=9610) ended because it received signal 15 (SIGTERM)
One traced child (pid=9614) 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.32
CPU system time (s): 1.20982
CPU usage (%): 99.8667
Max. virtual memory (cumulated for all children) (Kb): 70636

Verifier Data

ERROR: no interpretation found !