Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namesubmitted/aloul/FPGA_SAT05/normalized-chnl40_41_pb.cnf.cr.opb
MD5SUM3c9e81ddaaf37dd621fe2bc839a3f27f
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 42
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.107982
Number of variables3280
Total number of constraints162
Number of constraints which are clauses82
Number of constraints which are cardinality constraints (but not clauses)80
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint40
Maximum length of a constraint41

Trace number 819

Launcher Data

LAUNCH ON wulflinc5 THE 2005-09-18 12:25:41 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2358 boxname=wulflinc5 idbench=14 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3c9e81ddaaf37dd621fe2bc839a3f27f  /oldhome/oroussel/tmp/wulflinc5/normalized-chnl40_41_pb.cnf.cr.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-chnl40_41_pb.cnf.cr.opb
IDLAUNCH: 2358
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        948616 kB
Buffers:         32144 kB
Cached:          30248 kB
SwapCached:        780 kB
Active:          28260 kB
Inactive:        36892 kB
HighTotal:      131008 kB
HighFree:        96572 kB
LowTotal:       903652 kB
LowFree:        852044 kB
SwapTotal:     2097136 kB
SwapFree:      2095888 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5804 kB
Slab:            15140 kB
Committed_AS:    64300 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 12:45:51 (client local time) WITH STATUS 0 IN 1208.71 SECONDS
stats: 2358 7 1208.71 0

Solver Data

c Parsing PB file...
c Converting 162 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................................................
c ---[  79]---> BDD-cost:   79
c ---[  78]---> BDD-cost:   79
c ---[  77]---> BDD-cost:   79
c ---[  76]---> BDD-cost:   79
c ---[  75]---> BDD-cost:   79
c ---[  74]---> BDD-cost:   79
c ---[  73]---> BDD-cost:   79
c ---[  72]---> BDD-cost:   79
c ---[  71]---> BDD-cost:   79
c ---[  70]---> BDD-cost:   79
c ---[  69]---> BDD-cost:   79
c ---[  68]---> BDD-cost:   79
c ---[  67]---> BDD-cost:   79
c ---[  66]---> BDD-cost:   79
c ---[  65]---> BDD-cost:   79
c ---[  64]---> BDD-cost:   79
c ---[  63]---> BDD-cost:   79
c ---[  62]---> BDD-cost:   79
c ---[  61]---> BDD-cost:   79
c ---[  60]---> BDD-cost:   79
c ---[  59]---> BDD-cost:   79
c ---[  58]---> BDD-cost:   79
c ---[  57]---> BDD-cost:   79
c ---[  56]---> BDD-cost:   79
c ---[  55]---> BDD-cost:   79
c ---[  54]---> BDD-cost:   79
c ---[  53]---> BDD-cost:   79
c ---[  52]---> BDD-cost:   79
c ---[  51]---> BDD-cost:   79
c ---[  50]---> BDD-cost:   79
c ---[  49]---> BDD-cost:   79
c ---[  48]---> BDD-cost:   79
c ---[  47]---> BDD-cost:   79
c ---[  46]---> BDD-cost:   79
c ---[  45]---> BDD-cost:   79
c ---[  44]---> BDD-cost:   79
c ---[  43]---> BDD-cost:   79
c ---[  42]---> BDD-cost:   79
c ---[  41]---> BDD-cost:   79
c ---[  40]---> BDD-cost:   79
c ---[  39]---> BDD-cost:   79
c ---[  38]---> BDD-cost:   79
c ---[  37]---> BDD-cost:   79
c ---[  36]---> BDD-cost:   79
c ---[  35]---> BDD-cost:   79
c ---[  34]---> BDD-cost:   79
c ---[  33]---> BDD-cost:   79
c ---[  32]---> BDD-cost:   79
c ---[  31]---> BDD-cost:   79
c ---[  30]---> BDD-cost:   79
c ---[  29]---> BDD-cost:   79
c ---[  28]---> BDD-cost:   79
c ---[  27]---> BDD-cost:   79
c ---[  26]---> BDD-cost:   79
c ---[  25]---> BDD-cost:   79
c ---[  24]---> BDD-cost:   79
c ---[  23]---> BDD-cost:   79
c ---[  22]---> BDD-cost:   79
c ---[  21]---> BDD-cost:   79
c ---[  20]---> BDD-cost:   79
c ---[  19]---> BDD-cost:   79
c ---[  18]---> BDD-cost:   79
c ---[  17]---> BDD-cost:   79
c ---[  16]---> BDD-cost:   79
c ---[  15]---> BDD-cost:   79
c ---[  14]---> BDD-cost:   79
c ---[  13]---> BDD-cost:   79
c ---[  12]---> BDD-cost:   79
c ---[  11]---> BDD-cost:   79
c ---[  10]---> BDD-cost:   79
c ---[   9]---> BDD-cost:   79
c ---[   8]---> BDD-cost:   79
c ---[   7]---> BDD-cost:   79
c ---[   6]---> BDD-cost:   79
c ---[   5]---> BDD-cost:   79
c ---[   4]---> BDD-cost:   79
c ---[   3]---> BDD-cost:   79
c ---[   2]---> BDD-cost:   79
c ---[   1]---> BDD-cost:   79
c ---[   0]---> BDD-cost:   79
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   15762    44080 |    5254       0        0     nan |  0.000 % |
c |       101 |   15762    44080 |    5779     101    14280   141.4 |  0.833 % |
c |       256 |   15762    44080 |    6357     256    40852   159.6 |  0.833 % |
c |       482 |   15762    44080 |    6993     482    80226   166.4 |  0.833 % |
c |       819 |   15762    44080 |    7692     819   132593   161.9 |  0.833 % |
c |      1325 |   15762    44080 |    8461    1325   250938   189.4 |  0.833 % |
c |      2086 |   15762    44080 |    9307    2086   455746   218.5 |  0.833 % |
c |      3227 |   15762    44080 |   10238    3227   774769   240.1 |  0.833 % |
c |      4940 |   15762    44080 |   11262    4940  1219231   246.8 |  0.833 % |
c |      7503 |   15762    44080 |   12388    7503  1857014   247.5 |  0.833 % |
c |     11351 |   15762    44080 |   13627   11351  3536314   311.5 |  0.833 % |
c |     17117 |   15762    44080 |   14990    8595  3448950   401.3 |  0.833 % |
c |     25767 |   15762    44080 |   16489   17245  7911433   458.8 |  0.833 % |
c |     38741 |   15762    44080 |   18138   11355  3551431   312.8 |  0.833 % |
c |     58203 |   15762    44080 |   19952   18809  7096779   377.3 |  0.833 % |
c |     87395 |   15762    44080 |   21947   20922  8373757   400.2 |  0.833 % |
c |    131188 |   15762    44080 |   24141   19495  9878054   506.7 |  0.833 % |
c |    196873 |   15762    44080 |   26556   21140  8523475   403.2 |  0.833 % |

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/6857/stat): 6857 (minisat+_script) R 6856 6857 824 0 -1 0 19 0 0 0 0 0 0 0 20 0 1 0 1783017191 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/6857/statm): 174 3 169 147 0 27 0
[pid=6857] 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=6858
New process pid=6859
New process pid=6860
execve syscall for /bin/sed executable
One traced child (pid=6859) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=6860) exited with status: 0
One traced child (pid=6858) exited with status: 0
New process pid=6861
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-chnl40_41_pb.cnf.cr.opb

[startup+10.0035 s]
Raw data (loadavg): 0.84 0.69 0.82 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 2810 0 0 0 967 12 0 0 25 0 1 0 1783017196 12124160 2793 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 2960 2793 145 145 0 2815 0
[pid=6861] vsize: 11840
Current children cumulated CPU time (s) 9.8
Current children cumulated vsize (Kb) 13964

[startup+20.0052 s]
Raw data (loadavg): 0.87 0.70 0.82 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 4796 0 0 0 1943 21 0 0 25 0 1 0 1783017196 20271104 4779 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 4949 4779 145 145 0 4804 0
[pid=6861] vsize: 19796
Current children cumulated CPU time (s) 19.65
Current children cumulated vsize (Kb) 21920

[startup+30.0059 s]
Raw data (loadavg): 0.89 0.71 0.82 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 6256 0 0 0 2921 31 0 0 25 0 1 0 1783017196 26238976 6239 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 6406 6239 145 145 0 6261 0
[pid=6861] vsize: 25624
Current children cumulated CPU time (s) 29.53
Current children cumulated vsize (Kb) 27748

[startup+40.0057 s]
Raw data (loadavg): 0.90 0.72 0.82 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 6837 0 0 0 3913 34 0 0 25 0 1 0 1783017196 28684288 6820 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 7003 6820 145 145 0 6858 0
[pid=6861] vsize: 28012
Current children cumulated CPU time (s) 39.48
Current children cumulated vsize (Kb) 30136

[startup+50.0075 s]
Raw data (loadavg): 0.92 0.73 0.82 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 7543 0 0 0 4903 39 0 0 25 0 1 0 1783017196 31576064 7526 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6861/statm): 7709 7526 145 145 0 7564 0
[pid=6861] vsize: 30836
Current children cumulated CPU time (s) 49.43
Current children cumulated vsize (Kb) 32960

[startup+60.0082 s]
Raw data (loadavg): 0.93 0.73 0.82 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 8622 0 0 0 5886 47 0 0 25 0 1 0 1783017196 36016128 8605 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 8793 8605 145 145 0 8648 0
[pid=6861] vsize: 35172
Current children cumulated CPU time (s) 59.34
Current children cumulated vsize (Kb) 37296

[startup+70.0089 s]
Raw data (loadavg): 0.94 0.74 0.82 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 9192 0 0 0 6877 50 0 0 25 0 1 0 1783017196 38350848 9175 4294967295 134512640 135094434 3221224432 3221223024 134557020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6861/statm): 9363 9175 145 145 0 9218 0
[pid=6861] vsize: 37452
Current children cumulated CPU time (s) 69.28
Current children cumulated vsize (Kb) 39576

[startup+80.0107 s]
Raw data (loadavg): 0.95 0.75 0.83 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 9192 0 0 0 7876 50 0 0 25 0 1 0 1783017196 38350848 9175 4294967295 134512640 135094434 3221224432 3221223104 134555673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6861/statm): 9363 9175 145 145 0 9218 0
[pid=6861] vsize: 37452
Current children cumulated CPU time (s) 79.27
Current children cumulated vsize (Kb) 39576

[startup+90.0104 s]
Raw data (loadavg): 0.96 0.76 0.83 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 9192 0 0 0 8875 50 0 0 25 0 1 0 1783017196 38350848 9175 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 9363 9175 145 145 0 9218 0
[pid=6861] vsize: 37452
Current children cumulated CPU time (s) 89.26
Current children cumulated vsize (Kb) 39576

[startup+100.011 s]
Raw data (loadavg): 0.96 0.77 0.83 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 9493 0 0 0 9870 52 0 0 25 0 1 0 1783017196 39600128 9476 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 9668 9476 145 145 0 9523 0
[pid=6861] vsize: 38672
Current children cumulated CPU time (s) 99.23
Current children cumulated vsize (Kb) 40796

[startup+110.012 s]
Raw data (loadavg): 0.97 0.77 0.83 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 9669 0 0 0 10868 54 0 0 25 0 1 0 1783017196 40329216 9652 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 9846 9652 145 145 0 9701 0
[pid=6861] vsize: 39384
Current children cumulated CPU time (s) 109.23
Current children cumulated vsize (Kb) 41508

[startup+120.013 s]
Raw data (loadavg): 0.97 0.78 0.83 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 9669 0 0 0 11868 54 0 0 25 0 1 0 1783017196 40329216 9652 4294967295 134512640 135094434 3221224432 3221222896 134780778 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 9846 9652 145 145 0 9701 0
[pid=6861] vsize: 39384
Current children cumulated CPU time (s) 119.23
Current children cumulated vsize (Kb) 41508

[startup+130.013 s]
Raw data (loadavg): 0.98 0.79 0.83 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 9670 0 0 0 12869 54 0 0 25 0 1 0 1783017196 40329216 9653 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 9846 9653 145 145 0 9701 0
[pid=6861] vsize: 39384
Current children cumulated CPU time (s) 129.24
Current children cumulated vsize (Kb) 41508

[startup+140.014 s]
Raw data (loadavg): 0.98 0.79 0.83 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 9672 0 0 0 13869 54 0 0 25 0 1 0 1783017196 40329216 9655 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 9846 9655 145 145 0 9701 0
[pid=6861] vsize: 39384
Current children cumulated CPU time (s) 139.24
Current children cumulated vsize (Kb) 41508

[startup+150.015 s]
Raw data (loadavg): 0.98 0.80 0.83 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 9672 0 0 0 14869 54 0 0 25 0 1 0 1783017196 40329216 9655 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 9846 9655 145 145 0 9701 0
[pid=6861] vsize: 39384
Current children cumulated CPU time (s) 149.24
Current children cumulated vsize (Kb) 41508

[startup+160.015 s]
Raw data (loadavg): 0.98 0.81 0.83 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 9672 0 0 0 15869 54 0 0 25 0 1 0 1783017196 40329216 9655 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 9846 9655 145 145 0 9701 0
[pid=6861] vsize: 39384
Current children cumulated CPU time (s) 159.24
Current children cumulated vsize (Kb) 41508

[startup+170.015 s]
Raw data (loadavg): 0.99 0.81 0.83 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 9672 0 0 0 16869 54 0 0 25 0 1 0 1783017196 40329216 9655 4294967295 134512640 135094434 3221224432 3221223024 134557137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6861/statm): 9846 9655 145 145 0 9701 0
[pid=6861] vsize: 39384
Current children cumulated CPU time (s) 169.24
Current children cumulated vsize (Kb) 41508

[startup+180.016 s]
Raw data (loadavg): 0.99 0.82 0.83 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 10641 0 0 0 17855 60 0 0 25 0 1 0 1783017196 44302336 10624 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 10816 10624 145 145 0 10671 0
[pid=6861] vsize: 43264
Current children cumulated CPU time (s) 179.16
Current children cumulated vsize (Kb) 45388

[startup+190.016 s]
Raw data (loadavg): 0.99 0.82 0.84 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 11435 0 0 0 18844 65 0 0 25 0 1 0 1783017196 47558656 11418 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 11611 11418 145 145 0 11466 0
[pid=6861] vsize: 46444
Current children cumulated CPU time (s) 189.1
Current children cumulated vsize (Kb) 48568

[startup+200.017 s]
Raw data (loadavg): 0.99 0.83 0.84 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 11437 0 0 0 19844 65 0 0 25 0 1 0 1783017196 47558656 11420 4294967295 134512640 135094434 3221224432 3221223024 134551906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 11611 11420 145 145 0 11466 0
[pid=6861] vsize: 46444
Current children cumulated CPU time (s) 199.1
Current children cumulated vsize (Kb) 48568

[startup+210.017 s]
Raw data (loadavg): 0.99 0.83 0.84 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 11438 0 0 0 20844 65 0 0 25 0 1 0 1783017196 47558656 11421 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 11611 11421 145 145 0 11466 0
[pid=6861] vsize: 46444
Current children cumulated CPU time (s) 209.1
Current children cumulated vsize (Kb) 48568

[startup+220.018 s]
Raw data (loadavg): 0.99 0.84 0.84 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 11438 0 0 0 21844 65 0 0 25 0 1 0 1783017196 47558656 11421 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 11611 11421 145 145 0 11466 0
[pid=6861] vsize: 46444
Current children cumulated CPU time (s) 219.1
Current children cumulated vsize (Kb) 48568

[startup+230.019 s]
Raw data (loadavg): 0.99 0.84 0.84 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 11438 0 0 0 22845 65 0 0 25 0 1 0 1783017196 47558656 11421 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 11611 11421 145 145 0 11466 0
[pid=6861] vsize: 46444
Current children cumulated CPU time (s) 229.11
Current children cumulated vsize (Kb) 48568

[startup+240.02 s]
Raw data (loadavg): 0.99 0.85 0.84 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 11626 0 0 0 23842 66 0 0 25 0 1 0 1783017196 48332800 11609 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 11800 11609 145 145 0 11655 0
[pid=6861] vsize: 47200
Current children cumulated CPU time (s) 239.09
Current children cumulated vsize (Kb) 49324

[startup+250.02 s]
Raw data (loadavg): 0.99 0.85 0.84 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 11626 0 0 0 24842 66 0 0 25 0 1 0 1783017196 48332800 11609 4294967295 134512640 135094434 3221224432 3221223024 134557137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 11800 11609 145 145 0 11655 0
[pid=6861] vsize: 47200
Current children cumulated CPU time (s) 249.09
Current children cumulated vsize (Kb) 49324

[startup+260.021 s]
Raw data (loadavg): 0.99 0.86 0.84 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 11626 0 0 0 25842 66 0 0 25 0 1 0 1783017196 48332800 11609 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 11800 11609 145 145 0 11655 0
[pid=6861] vsize: 47200
Current children cumulated CPU time (s) 259.09
Current children cumulated vsize (Kb) 49324

[startup+270.022 s]
Raw data (loadavg): 0.99 0.86 0.84 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 11626 0 0 0 26842 66 0 0 25 0 1 0 1783017196 48332800 11609 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 11800 11609 145 145 0 11655 0
[pid=6861] vsize: 47200
Current children cumulated CPU time (s) 269.09
Current children cumulated vsize (Kb) 49324

[startup+280.023 s]
Raw data (loadavg): 0.99 0.86 0.84 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 11729 0 0 0 27841 67 0 0 25 0 1 0 1783017196 48758784 11712 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 11904 11712 145 145 0 11759 0
[pid=6861] vsize: 47616
Current children cumulated CPU time (s) 279.09
Current children cumulated vsize (Kb) 49740

[startup+290.023 s]
Raw data (loadavg): 0.99 0.87 0.85 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 12269 0 0 0 28833 71 0 0 25 0 1 0 1783017196 50982912 12252 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 12447 12252 145 145 0 12302 0
[pid=6861] vsize: 49788
Current children cumulated CPU time (s) 289.05
Current children cumulated vsize (Kb) 51912

[startup+300.024 s]
Raw data (loadavg): 0.99 0.87 0.85 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 12836 0 0 0 29823 75 0 0 25 0 1 0 1783017196 53313536 12819 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 13016 12819 145 145 0 12871 0
[pid=6861] vsize: 52064
Current children cumulated CPU time (s) 298.99
Current children cumulated vsize (Kb) 54188

[startup+310.025 s]
Raw data (loadavg): 0.99 0.88 0.85 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13066 0 0 0 30820 76 0 0 25 0 1 0 1783017196 54251520 13049 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 13245 13049 145 145 0 13100 0
[pid=6861] vsize: 52980
Current children cumulated CPU time (s) 308.97
Current children cumulated vsize (Kb) 55104

[startup+320.026 s]
Raw data (loadavg): 0.99 0.88 0.85 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13067 0 0 0 31820 76 0 0 25 0 1 0 1783017196 54251520 13050 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 13245 13050 145 145 0 13100 0
[pid=6861] vsize: 52980
Current children cumulated CPU time (s) 318.97
Current children cumulated vsize (Kb) 55104

[startup+330.027 s]
Raw data (loadavg): 0.99 0.88 0.85 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13067 0 0 0 32820 76 0 0 25 0 1 0 1783017196 54251520 13050 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 13245 13050 145 145 0 13100 0
[pid=6861] vsize: 52980
Current children cumulated CPU time (s) 328.97
Current children cumulated vsize (Kb) 55104

[startup+340.027 s]
Raw data (loadavg): 0.99 0.89 0.85 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13069 0 0 0 33821 76 0 0 25 0 1 0 1783017196 54251520 13052 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 13245 13052 145 145 0 13100 0
[pid=6861] vsize: 52980
Current children cumulated CPU time (s) 338.98
Current children cumulated vsize (Kb) 55104

[startup+350.028 s]
Raw data (loadavg): 0.99 0.89 0.85 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13069 0 0 0 34821 76 0 0 25 0 1 0 1783017196 54251520 13052 4294967295 134512640 135094434 3221224432 3221223104 134556421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 13245 13052 145 145 0 13100 0
[pid=6861] vsize: 52980
Current children cumulated CPU time (s) 348.98
Current children cumulated vsize (Kb) 55104

[startup+360.028 s]
Raw data (loadavg): 0.99 0.89 0.85 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13069 0 0 0 35821 76 0 0 25 0 1 0 1783017196 54251520 13052 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 13245 13052 145 145 0 13100 0
[pid=6861] vsize: 52980
Current children cumulated CPU time (s) 358.98
Current children cumulated vsize (Kb) 55104

[startup+370.029 s]
Raw data (loadavg): 0.99 0.90 0.85 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13069 0 0 0 36821 77 0 0 25 0 1 0 1783017196 54251520 13052 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 13245 13052 145 145 0 13100 0
[pid=6861] vsize: 52980
Current children cumulated CPU time (s) 368.99
Current children cumulated vsize (Kb) 55104

[startup+380.03 s]
Raw data (loadavg): 0.99 0.90 0.85 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13175 0 0 0 37820 77 0 0 25 0 1 0 1783017196 54685696 13158 4294967295 134512640 135094434 3221224432 3221223024 134556978 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 13351 13158 145 145 0 13206 0
[pid=6861] vsize: 53404
Current children cumulated CPU time (s) 378.98
Current children cumulated vsize (Kb) 55528

[startup+390.03 s]
Raw data (loadavg): 0.99 0.90 0.86 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13175 0 0 0 38820 77 0 0 25 0 1 0 1783017196 54685696 13158 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 13351 13158 145 145 0 13206 0
[pid=6861] vsize: 53404
Current children cumulated CPU time (s) 388.98
Current children cumulated vsize (Kb) 55528

[startup+400.03 s]
Raw data (loadavg): 0.99 0.90 0.86 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13175 0 0 0 39821 77 0 0 25 0 1 0 1783017196 54685696 13158 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 13351 13158 145 145 0 13206 0
[pid=6861] vsize: 53404
Current children cumulated CPU time (s) 398.99
Current children cumulated vsize (Kb) 55528

[startup+410.031 s]
Raw data (loadavg): 0.99 0.91 0.86 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13175 0 0 0 40821 77 0 0 25 0 1 0 1783017196 54685696 13158 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 13351 13158 145 145 0 13206 0
[pid=6861] vsize: 53404
Current children cumulated CPU time (s) 408.99
Current children cumulated vsize (Kb) 55528

[startup+420.032 s]
Raw data (loadavg): 0.99 0.91 0.86 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13175 0 0 0 41821 77 0 0 25 0 1 0 1783017196 54685696 13158 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 13351 13158 145 145 0 13206 0
[pid=6861] vsize: 53404
Current children cumulated CPU time (s) 418.99
Current children cumulated vsize (Kb) 55528

[startup+430.033 s]
Raw data (loadavg): 0.99 0.91 0.86 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 13879 0 0 0 42811 80 0 0 25 0 1 0 1783017196 57593856 13862 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 14061 13862 145 145 0 13916 0
[pid=6861] vsize: 56244
Current children cumulated CPU time (s) 428.92
Current children cumulated vsize (Kb) 58368

[startup+440.033 s]
Raw data (loadavg): 0.99 0.91 0.86 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 14543 0 0 0 43798 86 0 0 25 0 1 0 1783017196 60305408 14526 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 14723 14526 145 145 0 14578 0
[pid=6861] vsize: 58892
Current children cumulated CPU time (s) 438.85
Current children cumulated vsize (Kb) 61016

[startup+450.034 s]
Raw data (loadavg): 0.99 0.92 0.86 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 14707 0 0 0 44795 87 0 0 25 0 1 0 1783017196 60977152 14690 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 14887 14690 145 145 0 14742 0
[pid=6861] vsize: 59548
Current children cumulated CPU time (s) 448.83
Current children cumulated vsize (Kb) 61672

[startup+460.035 s]
Raw data (loadavg): 0.99 0.92 0.86 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 14707 0 0 0 45795 87 0 0 25 0 1 0 1783017196 60977152 14690 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 14887 14690 145 145 0 14742 0
[pid=6861] vsize: 59548
Current children cumulated CPU time (s) 458.83
Current children cumulated vsize (Kb) 61672

[startup+470.036 s]
Raw data (loadavg): 0.99 0.92 0.86 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 14707 0 0 0 46795 87 0 0 25 0 1 0 1783017196 60977152 14690 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 14887 14690 145 145 0 14742 0
[pid=6861] vsize: 59548
Current children cumulated CPU time (s) 468.83
Current children cumulated vsize (Kb) 61672

[startup+480.036 s]
Raw data (loadavg): 0.99 0.92 0.86 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 14707 0 0 0 47795 87 0 0 25 0 1 0 1783017196 60977152 14690 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 14887 14690 145 145 0 14742 0
[pid=6861] vsize: 59548
Current children cumulated CPU time (s) 478.83
Current children cumulated vsize (Kb) 61672

[startup+490.037 s]
Raw data (loadavg): 0.99 0.92 0.87 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 14707 0 0 0 48794 87 0 0 25 0 1 0 1783017196 60977152 14690 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6861/statm): 14887 14690 145 145 0 14742 0
[pid=6861] vsize: 59548
Current children cumulated CPU time (s) 488.82
Current children cumulated vsize (Kb) 61672

[startup+500.039 s]
Raw data (loadavg): 0.99 0.93 0.87 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 14830 0 0 0 49792 89 0 0 25 0 1 0 1783017196 61480960 14813 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6861/statm): 15010 14813 145 145 0 14865 0
[pid=6861] vsize: 60040
Current children cumulated CPU time (s) 498.82
Current children cumulated vsize (Kb) 62164

[startup+510.04 s]
Raw data (loadavg): 0.99 0.93 0.87 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 15919 0 0 0 50775 95 0 0 25 0 1 0 1783017196 65957888 15902 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 16103 15902 145 145 0 15958 0
[pid=6861] vsize: 64412
Current children cumulated CPU time (s) 508.71
Current children cumulated vsize (Kb) 66536

[startup+520.04 s]
Raw data (loadavg): 0.99 0.93 0.87 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 16804 0 0 0 51763 99 0 0 25 0 1 0 1783017196 69595136 16787 4294967295 134512640 135094434 3221224432 3221223104 134555815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 16991 16787 145 145 0 16846 0
[pid=6861] vsize: 67964
Current children cumulated CPU time (s) 518.63
Current children cumulated vsize (Kb) 70088

[startup+530.041 s]
Raw data (loadavg): 0.99 0.93 0.87 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17269 0 0 0 52755 103 0 0 25 0 1 0 1783017196 71503872 17252 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17457 17252 145 145 0 17312 0
[pid=6861] vsize: 69828
Current children cumulated CPU time (s) 528.59
Current children cumulated vsize (Kb) 71952

[startup+540.041 s]
Raw data (loadavg): 0.99 0.93 0.87 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17269 0 0 0 53755 103 0 0 25 0 1 0 1783017196 71503872 17252 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17457 17252 145 145 0 17312 0
[pid=6861] vsize: 69828
Current children cumulated CPU time (s) 538.59
Current children cumulated vsize (Kb) 71952

[startup+550.042 s]
Raw data (loadavg): 0.99 0.94 0.87 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17270 0 0 0 54756 103 0 0 25 0 1 0 1783017196 71503872 17253 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17457 17253 145 145 0 17312 0
[pid=6861] vsize: 69828
Current children cumulated CPU time (s) 548.6
Current children cumulated vsize (Kb) 71952

[startup+560.042 s]
Raw data (loadavg): 0.99 0.94 0.87 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17270 0 0 0 55756 103 0 0 25 0 1 0 1783017196 71503872 17253 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17457 17253 145 145 0 17312 0
[pid=6861] vsize: 69828
Current children cumulated CPU time (s) 558.6
Current children cumulated vsize (Kb) 71952

[startup+570.043 s]
Raw data (loadavg): 0.99 0.94 0.87 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17270 0 0 0 56756 103 0 0 25 0 1 0 1783017196 71503872 17253 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17457 17253 145 145 0 17312 0
[pid=6861] vsize: 69828
Current children cumulated CPU time (s) 568.6
Current children cumulated vsize (Kb) 71952

[startup+580.044 s]
Raw data (loadavg): 0.99 0.94 0.87 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17270 0 0 0 57756 103 0 0 25 0 1 0 1783017196 71503872 17253 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17457 17253 145 145 0 17312 0
[pid=6861] vsize: 69828
Current children cumulated CPU time (s) 578.6
Current children cumulated vsize (Kb) 71952

[startup+590.044 s]
Raw data (loadavg): 0.99 0.94 0.87 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17270 0 0 0 58757 103 0 0 25 0 1 0 1783017196 71503872 17253 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17457 17253 145 145 0 17312 0
[pid=6861] vsize: 69828
Current children cumulated CPU time (s) 588.61
Current children cumulated vsize (Kb) 71952

[startup+600.044 s]
Raw data (loadavg): 0.99 0.94 0.88 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17270 0 0 0 59757 103 0 0 25 0 1 0 1783017196 71503872 17253 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17457 17253 145 145 0 17312 0
[pid=6861] vsize: 69828
Current children cumulated CPU time (s) 598.61
Current children cumulated vsize (Kb) 71952

[startup+610.045 s]
Raw data (loadavg): 0.99 0.94 0.88 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17270 0 0 0 60757 103 0 0 25 0 1 0 1783017196 71503872 17253 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17457 17253 145 145 0 17312 0
[pid=6861] vsize: 69828
Current children cumulated CPU time (s) 608.61
Current children cumulated vsize (Kb) 71952

[startup+620.046 s]
Raw data (loadavg): 0.99 0.95 0.88 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17270 0 0 0 61757 103 0 0 25 0 1 0 1783017196 71503872 17253 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17457 17253 145 145 0 17312 0
[pid=6861] vsize: 69828
Current children cumulated CPU time (s) 618.61
Current children cumulated vsize (Kb) 71952

[startup+630.047 s]
Raw data (loadavg): 0.99 0.95 0.88 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 62754 105 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0
[pid=6861] vsize: 70316
Current children cumulated CPU time (s) 628.6
Current children cumulated vsize (Kb) 72440

[startup+640.047 s]
Raw data (loadavg): 0.99 0.95 0.88 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 63754 106 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0
[pid=6861] vsize: 70316
Current children cumulated CPU time (s) 638.61
Current children cumulated vsize (Kb) 72440

[startup+650.048 s]
Raw data (loadavg): 0.99 0.95 0.88 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 64754 106 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0
[pid=6861] vsize: 70316
Current children cumulated CPU time (s) 648.61
Current children cumulated vsize (Kb) 72440

[startup+660.049 s]
Raw data (loadavg): 0.99 0.95 0.88 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 65754 106 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0
[pid=6861] vsize: 70316
Current children cumulated CPU time (s) 658.61
Current children cumulated vsize (Kb) 72440

[startup+670.051 s]
Raw data (loadavg): 0.99 0.95 0.88 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 66754 107 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0
[pid=6861] vsize: 70316
Current children cumulated CPU time (s) 668.62
Current children cumulated vsize (Kb) 72440

[startup+680.051 s]
Raw data (loadavg): 0.99 0.95 0.88 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 67754 107 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0
[pid=6861] vsize: 70316
Current children cumulated CPU time (s) 678.62
Current children cumulated vsize (Kb) 72440

[startup+690.051 s]
Raw data (loadavg): 0.99 0.95 0.88 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 68754 107 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0
[pid=6861] vsize: 70316
Current children cumulated CPU time (s) 688.62
Current children cumulated vsize (Kb) 72440

[startup+700.052 s]
Raw data (loadavg): 0.99 0.95 0.89 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 69755 107 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0
[pid=6861] vsize: 70316
Current children cumulated CPU time (s) 698.63
Current children cumulated vsize (Kb) 72440

[startup+710.052 s]
Raw data (loadavg): 0.99 0.95 0.89 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 70754 107 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0
[pid=6861] vsize: 70316
Current children cumulated CPU time (s) 708.62
Current children cumulated vsize (Kb) 72440

[startup+720.053 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 71755 107 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0
[pid=6861] vsize: 70316
Current children cumulated CPU time (s) 718.63
Current children cumulated vsize (Kb) 72440

[startup+730.054 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 72755 107 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0
[pid=6861] vsize: 70316
Current children cumulated CPU time (s) 728.63
Current children cumulated vsize (Kb) 72440

[startup+740.055 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 73755 107 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0
[pid=6861] vsize: 70316
Current children cumulated CPU time (s) 738.63
Current children cumulated vsize (Kb) 72440

[startup+750.055 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 74755 107 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0
[pid=6861] vsize: 70316
Current children cumulated CPU time (s) 748.63
Current children cumulated vsize (Kb) 72440

[startup+760.056 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 75755 107 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0
[pid=6861] vsize: 70316
Current children cumulated CPU time (s) 758.63
Current children cumulated vsize (Kb) 72440

[startup+770.057 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 76755 108 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0
[pid=6861] vsize: 70316
Current children cumulated CPU time (s) 768.64
Current children cumulated vsize (Kb) 72440

[startup+780.058 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17392 0 0 0 77756 108 0 0 25 0 1 0 1783017196 72003584 17375 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 17579 17375 145 145 0 17434 0
[pid=6861] vsize: 70316
Current children cumulated CPU time (s) 778.65
Current children cumulated vsize (Kb) 72440

[startup+790.058 s]
Raw data (loadavg): 0.99 0.96 0.89 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17575 0 0 0 78753 109 0 0 18 0 1 0 1783017196 72753152 17558 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6861/statm): 17762 17558 145 145 0 17617 0
[pid=6861] vsize: 71048
Current children cumulated CPU time (s) 788.63
Current children cumulated vsize (Kb) 73172

[startup+800.059 s]
Raw data (loadavg): 0.99 0.96 0.90 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 17934 0 0 0 79747 112 0 0 25 0 1 0 1783017196 74248192 17917 4294967295 134512640 135094434 3221224432 3221223024 134557157 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6861/statm): 18127 17917 145 145 0 17982 0
[pid=6861] vsize: 72508
Current children cumulated CPU time (s) 798.6
Current children cumulated vsize (Kb) 74632

[startup+810.06 s]
Raw data (loadavg): 0.99 0.96 0.90 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18094 0 0 0 80744 113 0 0 25 0 1 0 1783017196 74911744 18077 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18077 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 808.58
Current children cumulated vsize (Kb) 75280

[startup+820.062 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18094 0 0 0 81745 113 0 0 25 0 1 0 1783017196 74911744 18077 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18077 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 818.59
Current children cumulated vsize (Kb) 75280

[startup+830.062 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18094 0 0 0 82745 113 0 0 25 0 1 0 1783017196 74911744 18077 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18077 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 828.59
Current children cumulated vsize (Kb) 75280

[startup+840.063 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18094 0 0 0 83745 113 0 0 25 0 1 0 1783017196 74911744 18077 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18077 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 838.59
Current children cumulated vsize (Kb) 75280

[startup+850.064 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18094 0 0 0 84745 113 0 0 25 0 1 0 1783017196 74911744 18077 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18077 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 848.59
Current children cumulated vsize (Kb) 75280

[startup+860.065 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18094 0 0 0 85745 113 0 0 25 0 1 0 1783017196 74911744 18077 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18077 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 858.59
Current children cumulated vsize (Kb) 75280

[startup+870.065 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18095 0 0 0 86746 113 0 0 25 0 1 0 1783017196 74911744 18078 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18078 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 868.6
Current children cumulated vsize (Kb) 75280

[startup+880.066 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18095 0 0 0 87746 113 0 0 25 0 1 0 1783017196 74911744 18078 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18078 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 878.6
Current children cumulated vsize (Kb) 75280

[startup+890.066 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18095 0 0 0 88746 113 0 0 25 0 1 0 1783017196 74911744 18078 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18078 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 888.6
Current children cumulated vsize (Kb) 75280

[startup+900.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18095 0 0 0 89746 113 0 0 25 0 1 0 1783017196 74911744 18078 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18078 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 898.6
Current children cumulated vsize (Kb) 75280

[startup+910.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18095 0 0 0 90746 114 0 0 25 0 1 0 1783017196 74911744 18078 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18078 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 908.61
Current children cumulated vsize (Kb) 75280

[startup+920.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18095 0 0 0 91747 114 0 0 25 0 1 0 1783017196 74911744 18078 4294967295 134512640 135094434 3221224432 3221223104 134555553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18078 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 918.62
Current children cumulated vsize (Kb) 75280

[startup+930.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18095 0 0 0 92747 114 0 0 25 0 1 0 1783017196 74911744 18078 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6861/statm): 18289 18078 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 928.62
Current children cumulated vsize (Kb) 75280

[startup+940.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18095 0 0 0 93746 114 0 0 25 0 1 0 1783017196 74911744 18078 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18078 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 938.61
Current children cumulated vsize (Kb) 75280

[startup+950.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18095 0 0 0 94746 114 0 0 25 0 1 0 1783017196 74911744 18078 4294967295 134512640 135094434 3221224432 3221223024 134551989 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18078 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 948.61
Current children cumulated vsize (Kb) 75280

[startup+960.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 95747 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 958.62
Current children cumulated vsize (Kb) 75280

[startup+970.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 96747 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 968.62
Current children cumulated vsize (Kb) 75280

[startup+980.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 97747 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 978.62
Current children cumulated vsize (Kb) 75280

[startup+990.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 98747 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 988.62
Current children cumulated vsize (Kb) 75280

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 99747 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223024 134556834 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 998.62
Current children cumulated vsize (Kb) 75280

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 100748 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 1008.63
Current children cumulated vsize (Kb) 75280

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 101748 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 1018.63
Current children cumulated vsize (Kb) 75280

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 102748 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 1028.63
Current children cumulated vsize (Kb) 75280

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 103748 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 1038.63
Current children cumulated vsize (Kb) 75280

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 104748 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 1048.63
Current children cumulated vsize (Kb) 75280

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 105749 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 1058.64
Current children cumulated vsize (Kb) 75280

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 106749 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223024 134557398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 1068.64
Current children cumulated vsize (Kb) 75280

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 107749 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 1078.64
Current children cumulated vsize (Kb) 75280

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 108749 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 1088.64
Current children cumulated vsize (Kb) 75280

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 109750 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 1098.65
Current children cumulated vsize (Kb) 75280

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 110750 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 1108.65
Current children cumulated vsize (Kb) 75280

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 111750 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 1118.65
Current children cumulated vsize (Kb) 75280

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 112750 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 1128.65
Current children cumulated vsize (Kb) 75280

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 113750 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 1138.65
Current children cumulated vsize (Kb) 75280

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 114751 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 1148.66
Current children cumulated vsize (Kb) 75280

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 115751 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 1158.66
Current children cumulated vsize (Kb) 75280

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 116751 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 1168.66
Current children cumulated vsize (Kb) 75280

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 117751 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 1178.66
Current children cumulated vsize (Kb) 75280

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 118752 114 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 1188.67
Current children cumulated vsize (Kb) 75280

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 119752 115 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223104 134555768 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 1198.68
Current children cumulated vsize (Kb) 75280

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 120752 115 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 1208.68
Current children cumulated vsize (Kb) 75280



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 6861
Raw data (/proc/6857/stat): 6857 (minisat+_script) S 6856 6857 824 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1783017191 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/6857/statm): 531 226 485 147 0 384 0
[pid=6857] vsize: 2124
Raw data (/proc/6861/stat): 6861 (minisat+_64-bit) R 6857 6857 824 0 -1 0 18097 0 0 0 120752 115 0 0 25 0 1 0 1783017196 74911744 18080 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6861/statm): 18289 18080 145 145 0 18144 0
[pid=6861] vsize: 73156
Current children cumulated CPU time (s) 1208.68
Current children cumulated vsize (Kb) 75280

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

Child status: 0
Real time (s): 1210.13
CPU time (s): 1208.71
CPU user time (s): 1207.53
CPU system time (s): 1.18582
CPU usage (%): 99.8828
Max. virtual memory (cumulated for all children) (Kb): 75280

Verifier Data

ERROR: no interpretation found !